Generation remains pure and byte-identical, but is requested by the
actual lowering consumer rather than performed when this module is loaded.
176def nativeMemoryGenerateCopyRoutine :
177 (pi unrestricted request : Nat . (family NativeMemoryRoutineResult)) =
178 (lambda unrestricted request : Nat .
179 (eliminate
180 X86NativeAssemblyResult
181 (lambda unrestricted current : (family X86NativeAssemblyResult) .
182 (family NativeMemoryRoutineResult))
183 (x86NativeAssemble nativeMemoryCopyAssembly)
184 (branch
185 X86NativeAssemblyEncoded
186 code
187 .
188 (app
189 (lambda unrestricted digest : Bytes .
190 (app
191 (lambda unrestricted telemetry : (family NativeMemoryRoutineTelemetry) .
192 (constructor
193 NativeMemoryRoutineResult
194 NativeMemoryRoutineGenerated
195 (constructor
196 NativeMemoryRoutine
197 NativeMemoryRoutineValue
198 code
199 digest
200 nativeMemoryCopyInstructionCount
201 telemetry)
202 telemetry))
203 (nativeMemoryRoutineTelemetrySuccess code digest)))
204 (sha256HexBytesOrEmpty (sha256Hex code))))
205 (branch
206 X86NativeAssemblyEncodeDuplicateLabel
207 duplicateName
208 .
209 (nativeMemoryRoutineFail
210 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineDuplicateLabel duplicateName)))
211 (branch
212 X86NativeAssemblyEncodeOffsetOverflow
213 .
214 (nativeMemoryRoutineFail
215 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineOffsetOverflow)))
216 (branch
217 X86NativeAssemblyMissingLabel
218 missingName
219 .
220 (nativeMemoryRoutineFail
221 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineMissingLabel missingName)))
222 (branch
223 X86NativeAssemblyDisplacementOutOfRange
224 distantName
225 .
226 (nativeMemoryRoutineFail
227 (constructor
228 NativeMemoryRoutineErrorCode
229 NativeMemoryRoutineDisplacementOutOfRange
230 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.