Generation remains pure and byte-identical, but is requested by the
actual lowering consumer rather than performed when this module is loaded.
178def nativeMemoryGenerateCopyRoutine :
179 (pi unrestricted request : Nat . (family NativeMemoryRoutineResult)) =
180 (lambda unrestricted request : Nat .
181 (eliminate
182 X86NativeAssemblyResult
183 (lambda unrestricted current : (family X86NativeAssemblyResult) .
184 (family NativeMemoryRoutineResult))
185 (x86NativeAssemble nativeMemoryCopyAssembly)
186 (branch
187 X86NativeAssemblyEncoded
188 code
189 .
190 (app
191 (lambda unrestricted digest : Bytes .
192 (app
193 (lambda unrestricted telemetry : (family NativeMemoryRoutineTelemetry) .
194 (constructor
195 NativeMemoryRoutineResult
196 NativeMemoryRoutineGenerated
197 (constructor
198 NativeMemoryRoutine
199 NativeMemoryRoutineValue
200 code
201 digest
202 nativeMemoryCopyInstructionCount
203 telemetry)
204 telemetry))
205 (nativeMemoryRoutineTelemetrySuccess code digest)))
206 (sha256HexBytesOrEmpty (sha256Hex code))))
207 (branch
208 X86NativeAssemblyEncodeDuplicateLabel
209 duplicateName
210 .
211 (nativeMemoryRoutineFail
212 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineDuplicateLabel duplicateName)))
213 (branch
214 X86NativeAssemblyEncodeOffsetOverflow
215 .
216 (nativeMemoryRoutineFail
217 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineOffsetOverflow)))
218 (branch
219 X86NativeAssemblyMissingLabel
220 missingName
221 .
222 (nativeMemoryRoutineFail
223 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineMissingLabel missingName)))
224 (branch
225 X86NativeAssemblyDisplacementOutOfRange
226 distantName
227 .
228 (nativeMemoryRoutineFail
229 (constructor
230 NativeMemoryRoutineErrorCode
231 NativeMemoryRoutineDisplacementOutOfRange
232 distantName)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.