210def x86EncodeProgramBuilder =
211 (lambda erased input : (family X86MachineState) .
212 (lambda erased output : (family X86MachineState) .
213 (lambda erased effects : (family X86EffectTrace) .
214 (lambda unrestricted program : (family X86Program input output effects) .
215 (eliminate
216 X86Program
217 (lambda erased motiveInput : (family X86MachineState) .
218 (lambda erased motiveOutput : (family X86MachineState) .
219 (lambda erased motiveEffects : (family X86EffectTrace) .
220 (lambda unrestricted value : (family X86Program motiveInput motiveOutput motiveEffects) .
221 BytesBuilder))))
222 program
223 (branch X86ProgramEnd state . (bytes-builder-empty))
224 (branch
225 X86ProgramPureNext
226 start
227 middle
228 finish
229 tailEffects
230 head
231 tail
232 ih_tail
233 .
234 (bytes-builder-append
235 (bytes-builder-chunk
236 (x86EncodeInstruction start middle (constructor X86EffectTrace X86NoEffects) head))
237 ih_tail))
238 (branch
239 X86ProgramSystemCallNext
240 start
241 middle
242 finish
243 tailEffects
244 head
245 tail
246 ih_tail
247 .
248 (bytes-builder-append
249 (bytes-builder-chunk
250 (x86EncodeInstruction
251 start
252 middle
253 (constructor
254 X86EffectTrace
255 X86SystemCallEffect
256 (constructor X86EffectTrace X86NoEffects))
257 head))
258 ih_tail)))))))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.