module Compiler.MachineX86 family X86ValueClass : Type 0 constructor X86UndefinedValue constructor X86Word64Value constructor X86AddressValue end-family family X86MachineState : Type 0 constructor X86MachineStateValue field erased x86StateRAX : (family X86ValueClass) field erased x86StateRDI : (family X86ValueClass) field erased x86StateRSI : (family X86ValueClass) field erased x86StateRDX : (family X86ValueClass) end-family family X86EffectTrace : Type 0 constructor X86NoEffects constructor X86SystemCallEffect recursive erased x86RemainingEffects end-family family X86Immediate32 : Type 0 constructor X86Immediate32Value field unrestricted x86ImmediateByte0 : Byte field unrestricted x86ImmediateByte1 : Byte field unrestricted x86ImmediateByte2 : Byte field unrestricted x86ImmediateByte3 : Byte end-family family X86Instruction : Type 0 index erased x86InstructionInput : (family X86MachineState) index erased x86InstructionOutput : (family X86MachineState) index erased x86InstructionEffects : (family X86EffectTrace) constructor X86ZeroEDI32 field erased x86ZeroInputRAX : (family X86ValueClass) field erased x86ZeroInputRDI : (family X86ValueClass) field erased x86ZeroInputRSI : (family X86ValueClass) field erased x86ZeroInputRDX : (family X86ValueClass) result (constructor X86MachineState X86MachineStateValue x86ZeroInputRAX x86ZeroInputRDI x86ZeroInputRSI x86ZeroInputRDX) result (constructor X86MachineState X86MachineStateValue x86ZeroInputRAX (constructor X86ValueClass X86Word64Value) x86ZeroInputRSI x86ZeroInputRDX) result (constructor X86EffectTrace X86NoEffects) constructor X86IncrementRDI64 field erased x86IncrementInputRAX : (family X86ValueClass) field erased x86IncrementInputRSI : (family X86ValueClass) field erased x86IncrementInputRDX : (family X86ValueClass) result (constructor X86MachineState X86MachineStateValue x86IncrementInputRAX (constructor X86ValueClass X86Word64Value) x86IncrementInputRSI x86IncrementInputRDX) result (constructor X86MachineState X86MachineStateValue x86IncrementInputRAX (constructor X86ValueClass X86Word64Value) x86IncrementInputRSI x86IncrementInputRDX) result (constructor X86EffectTrace X86NoEffects) constructor X86MoveEAXImmediate32 field erased x86MoveEAXInputRAX : (family X86ValueClass) field erased x86MoveEAXInputRDI : (family X86ValueClass) field erased x86MoveEAXInputRSI : (family X86ValueClass) field erased x86MoveEAXInputRDX : (family X86ValueClass) field unrestricted x86MoveEAXImmediate : (family X86Immediate32) result (constructor X86MachineState X86MachineStateValue x86MoveEAXInputRAX x86MoveEAXInputRDI x86MoveEAXInputRSI x86MoveEAXInputRDX) result (constructor X86MachineState X86MachineStateValue (constructor X86ValueClass X86Word64Value) x86MoveEAXInputRDI x86MoveEAXInputRSI x86MoveEAXInputRDX) result (constructor X86EffectTrace X86NoEffects) constructor X86MoveEDIImmediate32 field erased x86MoveEDIInputRAX : (family X86ValueClass) field erased x86MoveEDIInputRDI : (family X86ValueClass) field erased x86MoveEDIInputRSI : (family X86ValueClass) field erased x86MoveEDIInputRDX : (family X86ValueClass) field unrestricted x86MoveEDIImmediate : (family X86Immediate32) result (constructor X86MachineState X86MachineStateValue x86MoveEDIInputRAX x86MoveEDIInputRDI x86MoveEDIInputRSI x86MoveEDIInputRDX) result (constructor X86MachineState X86MachineStateValue x86MoveEDIInputRAX (constructor X86ValueClass X86Word64Value) x86MoveEDIInputRSI x86MoveEDIInputRDX) result (constructor X86EffectTrace X86NoEffects) constructor X86MoveEDXImmediate32 field erased x86MoveEDXInputRAX : (family X86ValueClass) field erased x86MoveEDXInputRDI : (family X86ValueClass) field erased x86MoveEDXInputRSI : (family X86ValueClass) field erased x86MoveEDXInputRDX : (family X86ValueClass) field unrestricted x86MoveEDXImmediate : (family X86Immediate32) result (constructor X86MachineState X86MachineStateValue x86MoveEDXInputRAX x86MoveEDXInputRDI x86MoveEDXInputRSI x86MoveEDXInputRDX) result (constructor X86MachineState X86MachineStateValue x86MoveEDXInputRAX x86MoveEDXInputRDI x86MoveEDXInputRSI (constructor X86ValueClass X86Word64Value)) result (constructor X86EffectTrace X86NoEffects) constructor X86LoadRSIRIPRelative field erased x86LoadRSIInputRAX : (family X86ValueClass) field erased x86LoadRSIInputRDI : (family X86ValueClass) field erased x86LoadRSIInputRSI : (family X86ValueClass) field erased x86LoadRSIInputRDX : (family X86ValueClass) field unrestricted x86LoadRSIDisplacement : (family X86Immediate32) result (constructor X86MachineState X86MachineStateValue x86LoadRSIInputRAX x86LoadRSIInputRDI x86LoadRSIInputRSI x86LoadRSIInputRDX) result (constructor X86MachineState X86MachineStateValue x86LoadRSIInputRAX x86LoadRSIInputRDI (constructor X86ValueClass X86AddressValue) x86LoadRSIInputRDX) result (constructor X86EffectTrace X86NoEffects) constructor X86SystemCall field erased x86SystemCallInputRDI : (family X86ValueClass) field erased x86SystemCallInputRSI : (family X86ValueClass) field erased x86SystemCallInputRDX : (family X86ValueClass) result (constructor X86MachineState X86MachineStateValue (constructor X86ValueClass X86Word64Value) x86SystemCallInputRDI x86SystemCallInputRSI x86SystemCallInputRDX) result (constructor X86MachineState X86MachineStateValue (constructor X86ValueClass X86Word64Value) x86SystemCallInputRDI x86SystemCallInputRSI x86SystemCallInputRDX) result (constructor X86EffectTrace X86SystemCallEffect (constructor X86EffectTrace X86NoEffects)) end-family family X86Program : Type 0 index erased x86ProgramInput : (family X86MachineState) index erased x86ProgramOutput : (family X86MachineState) index erased x86ProgramEffects : (family X86EffectTrace) constructor X86ProgramEnd field erased x86ProgramEndState : (family X86MachineState) result x86ProgramEndState result x86ProgramEndState result (constructor X86EffectTrace X86NoEffects) constructor X86ProgramPureNext field erased x86ProgramStartState : (family X86MachineState) field erased x86ProgramMiddleState : (family X86MachineState) field erased x86ProgramFinishState : (family X86MachineState) field erased x86ProgramTailEffects : (family X86EffectTrace) field unrestricted x86ProgramHead : (family X86Instruction x86ProgramStartState x86ProgramMiddleState (constructor X86EffectTrace X86NoEffects)) recursive unrestricted x86ProgramTail recursive-index x86ProgramMiddleState recursive-index x86ProgramFinishState recursive-index x86ProgramTailEffects result x86ProgramStartState result x86ProgramFinishState result x86ProgramTailEffects constructor X86ProgramSystemCallNext field erased x86SystemCallProgramStartState : (family X86MachineState) field erased x86SystemCallProgramMiddleState : (family X86MachineState) field erased x86SystemCallProgramFinishState : (family X86MachineState) field erased x86SystemCallProgramTailEffects : (family X86EffectTrace) field unrestricted x86SystemCallProgramHead : (family X86Instruction x86SystemCallProgramStartState x86SystemCallProgramMiddleState (constructor X86EffectTrace X86SystemCallEffect (constructor X86EffectTrace X86NoEffects))) recursive unrestricted x86SystemCallProgramTail recursive-index x86SystemCallProgramMiddleState recursive-index x86SystemCallProgramFinishState recursive-index x86SystemCallProgramTailEffects result x86SystemCallProgramStartState result x86SystemCallProgramFinishState result (constructor X86EffectTrace X86SystemCallEffect x86SystemCallProgramTailEffects) end-family def x86Immediate32 = (lambda unrestricted lowByte : Byte . (constructor X86Immediate32 X86Immediate32Value lowByte (byte 0) (byte 0) (byte 0))) def x86EncodeImmediate32 = (lambda unrestricted immediate : (family X86Immediate32) . (eliminate X86Immediate32 (lambda unrestricted value : (family X86Immediate32) . Bytes) immediate (branch X86Immediate32Value byte0 byte1 byte2 byte3 . (bytes-cons byte0 (bytes-cons byte1 (bytes-cons byte2 (bytes-cons byte3 b""))))))) def x86EncodeInstruction = (lambda erased input : (family X86MachineState) . (lambda erased output : (family X86MachineState) . (lambda erased effects : (family X86EffectTrace) . (lambda unrestricted instruction : (family X86Instruction input output effects) . (eliminate X86Instruction (lambda erased motiveInput : (family X86MachineState) . (lambda erased motiveOutput : (family X86MachineState) . (lambda erased motiveEffects : (family X86EffectTrace) . (lambda unrestricted value : (family X86Instruction motiveInput motiveOutput motiveEffects) . Bytes)))) instruction (branch X86ZeroEDI32 inputRAX inputRDI inputRSI inputRDX . (bytes 49 255)) (branch X86IncrementRDI64 inputRAX inputRSI inputRDX . (bytes 72 255 199)) (branch X86MoveEAXImmediate32 inputRAX inputRDI inputRSI inputRDX immediate . (bytes-append (bytes 184) (x86EncodeImmediate32 immediate))) (branch X86MoveEDIImmediate32 inputRAX inputRDI inputRSI inputRDX immediate . (bytes-append (bytes 191) (x86EncodeImmediate32 immediate))) (branch X86MoveEDXImmediate32 inputRAX inputRDI inputRSI inputRDX immediate . (bytes-append (bytes 186) (x86EncodeImmediate32 immediate))) (branch X86LoadRSIRIPRelative inputRAX inputRDI inputRSI inputRDX displacement . (bytes-append (bytes 72 141 53) (x86EncodeImmediate32 displacement))) (branch X86SystemCall inputRDI inputRSI inputRDX . (bytes 15 5))))))) def x86EncodeProgramBuilder = (lambda erased input : (family X86MachineState) . (lambda erased output : (family X86MachineState) . (lambda erased effects : (family X86EffectTrace) . (lambda unrestricted program : (family X86Program input output effects) . (eliminate X86Program (lambda erased motiveInput : (family X86MachineState) . (lambda erased motiveOutput : (family X86MachineState) . (lambda erased motiveEffects : (family X86EffectTrace) . (lambda unrestricted value : (family X86Program motiveInput motiveOutput motiveEffects) . BytesBuilder)))) program (branch X86ProgramEnd state . (bytes-builder-empty)) (branch X86ProgramPureNext start middle finish tailEffects head tail ih_tail . (bytes-builder-append (bytes-builder-chunk (x86EncodeInstruction start middle (constructor X86EffectTrace X86NoEffects) head)) ih_tail)) (branch X86ProgramSystemCallNext start middle finish tailEffects head tail ih_tail . (bytes-builder-append (bytes-builder-chunk (x86EncodeInstruction start middle (constructor X86EffectTrace X86SystemCallEffect (constructor X86EffectTrace X86NoEffects)) head)) ih_tail))))))) def x86EncodeProgram = (lambda erased input : (family X86MachineState) . (lambda erased output : (family X86MachineState) . (lambda erased effects : (family X86EffectTrace) . (lambda unrestricted program : (family X86Program input output effects) . (bytes-builder-build (x86EncodeProgramBuilder input output effects program)))))) def x86UndefinedClass : (family X86ValueClass) = (constructor X86ValueClass X86UndefinedValue) def x86Word64Class : (family X86ValueClass) = (constructor X86ValueClass X86Word64Value) def x86AddressClass : (family X86ValueClass) = (constructor X86ValueClass X86AddressValue) def x86NoEffects : (family X86EffectTrace) = (constructor X86EffectTrace X86NoEffects) def x86OneSystemCall : (family X86EffectTrace) = (constructor X86EffectTrace X86SystemCallEffect x86NoEffects)