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