module Compiler.Codegen

import Compiler.AST
import Compiler.Lexer
import Compiler.Parser
import Compiler.Elaborator
import Compiler.MachineX86

family CodegenResult : Type 0
constructor CodeGenerated
field unrestricted machineCode : Bytes
constructor CodegenUnboundVariable
field unrestricted codegenUnboundSpelling : Bytes
constructor CodegenUnsupportedTerm
field unrestricted codegenUnsupportedCode : Nat

end-family

def codegenInitialState : (family X86MachineState) =
  (constructor
    X86MachineState
    X86MachineStateValue
    x86UndefinedClass
    x86UndefinedClass
    x86UndefinedClass
    x86UndefinedClass)

def codegenExitArgumentState : (family X86MachineState) =
  (constructor
    X86MachineState
    X86MachineStateValue
    x86UndefinedClass
    x86Word64Class
    x86UndefinedClass
    x86UndefinedClass)

def codegenExitState : (family X86MachineState) =
  (constructor
    X86MachineState
    X86MachineStateValue
    x86Word64Class
    x86Word64Class
    x86UndefinedClass
    x86UndefinedClass)

def codegenExitTail :
  (family X86Program codegenExitArgumentState codegenExitState x86OneSystemCall) =
  (constructor
    X86Program
    X86ProgramPureNext
    codegenExitArgumentState
    codegenExitState
    codegenExitState
    x86OneSystemCall
    (constructor
      X86Instruction
      X86MoveEAXImmediate32
      x86UndefinedClass
      x86Word64Class
      x86UndefinedClass
      x86UndefinedClass
      (x86Immediate32 (byte 60)))
    (constructor
      X86Program
      X86ProgramSystemCallNext
      codegenExitState
      codegenExitState
      codegenExitState
      x86NoEffects
      (constructor X86Instruction X86SystemCall x86Word64Class x86UndefinedClass x86UndefinedClass)
      (constructor X86Program X86ProgramEnd codegenExitState)))

def lowerClosedNaturalProgram =
  (lambda unrestricted value : (family ClosedNatural) .
    (app
      (eliminate
        ClosedNatural
        (lambda unrestricted term : (family ClosedNatural) .
          (pi unrestricted tail : (family X86Program codegenExitArgumentState codegenExitState x86OneSystemCall) .
            (family X86Program codegenInitialState codegenExitState x86OneSystemCall)))
        value
        (branch
          ClosedZero
          .
          (lambda unrestricted tail : (family X86Program codegenExitArgumentState codegenExitState x86OneSystemCall) .
            (constructor
              X86Program
              X86ProgramPureNext
              codegenInitialState
              codegenExitArgumentState
              codegenExitState
              x86OneSystemCall
              (constructor
                X86Instruction
                X86ZeroEDI32
                x86UndefinedClass
                x86UndefinedClass
                x86UndefinedClass
                x86UndefinedClass)
              tail)))
        (branch
          ClosedSuccessor
          closedPredecessor
          ih_closedPredecessor
          .
          (lambda unrestricted tail : (family X86Program codegenExitArgumentState codegenExitState x86OneSystemCall) .
            (ih_closedPredecessor
              (constructor
                X86Program
                X86ProgramPureNext
                codegenExitArgumentState
                codegenExitArgumentState
                codegenExitState
                x86OneSystemCall
                (constructor
                  X86Instruction
                  X86IncrementRDI64
                  x86UndefinedClass
                  x86UndefinedClass
                  x86UndefinedClass)
                tail)))))
      codegenExitTail))

def lowerClosedNaturalValue =
  (lambda unrestricted value : (family ClosedNatural) .
    (x86EncodeProgram
      codegenInitialState
      codegenExitState
      x86OneSystemCall
      (lowerClosedNaturalProgram value)))

def fixedZeroMachineCode : Bytes =
  (lowerClosedNaturalValue (constructor ClosedNatural ClosedZero))

def lowerByteProgram =
  (lambda unrestricted value : Byte .
    (constructor
      X86Program
      X86ProgramPureNext
      codegenInitialState
      codegenExitArgumentState
      codegenExitState
      x86OneSystemCall
      (constructor
        X86Instruction
        X86MoveEDIImmediate32
        x86UndefinedClass
        x86UndefinedClass
        x86UndefinedClass
        x86UndefinedClass
        (x86Immediate32 value))
      codegenExitTail))

def lowerByteValue =
  (lambda unrestricted value : Byte .
    (x86EncodeProgram
      codegenInitialState
      codegenExitState
      x86OneSystemCall
      (lowerByteProgram value)))

def codegenStdoutRAXState : (family X86MachineState) =
  (constructor
    X86MachineState
    X86MachineStateValue
    x86Word64Class
    x86UndefinedClass
    x86UndefinedClass
    x86UndefinedClass)

def codegenStdoutRDIState : (family X86MachineState) =
  (constructor
    X86MachineState
    X86MachineStateValue
    x86Word64Class
    x86Word64Class
    x86UndefinedClass
    x86UndefinedClass)

def codegenStdoutRSIState : (family X86MachineState) =
  (constructor
    X86MachineState
    X86MachineStateValue
    x86Word64Class
    x86Word64Class
    x86AddressClass
    x86UndefinedClass)

def codegenStdoutReadyState : (family X86MachineState) =
  (constructor
    X86MachineState
    X86MachineStateValue
    x86Word64Class
    x86Word64Class
    x86AddressClass
    x86Word64Class)

def codegenTwoSystemCalls : (family X86EffectTrace) =
  (constructor X86EffectTrace X86SystemCallEffect x86OneSystemCall)

def lowerBytesProgram =
  (lambda unrestricted value : Bytes .
    (constructor
      X86Program
      X86ProgramPureNext
      codegenInitialState
      codegenStdoutRAXState
      codegenStdoutReadyState
      codegenTwoSystemCalls
      (constructor
        X86Instruction
        X86MoveEAXImmediate32
        x86UndefinedClass
        x86UndefinedClass
        x86UndefinedClass
        x86UndefinedClass
        (x86Immediate32 (byte 1)))
      (constructor
        X86Program
        X86ProgramPureNext
        codegenStdoutRAXState
        codegenStdoutRDIState
        codegenStdoutReadyState
        codegenTwoSystemCalls
        (constructor
          X86Instruction
          X86MoveEDIImmediate32
          x86Word64Class
          x86UndefinedClass
          x86UndefinedClass
          x86UndefinedClass
          (x86Immediate32 (byte 1)))
        (constructor
          X86Program
          X86ProgramPureNext
          codegenStdoutRDIState
          codegenStdoutRSIState
          codegenStdoutReadyState
          codegenTwoSystemCalls
          (constructor
            X86Instruction
            X86LoadRSIRIPRelative
            x86Word64Class
            x86Word64Class
            x86UndefinedClass
            x86UndefinedClass
            (x86Immediate32 (byte 16)))
          (constructor
            X86Program
            X86ProgramPureNext
            codegenStdoutRSIState
            codegenStdoutReadyState
            codegenStdoutReadyState
            codegenTwoSystemCalls
            (constructor
              X86Instruction
              X86MoveEDXImmediate32
              x86Word64Class
              x86Word64Class
              x86AddressClass
              x86UndefinedClass
              (x86Immediate32 (nat-to-byte (bytes-length value))))
            (constructor
              X86Program
              X86ProgramSystemCallNext
              codegenStdoutReadyState
              codegenStdoutReadyState
              codegenStdoutReadyState
              x86OneSystemCall
              (constructor
                X86Instruction
                X86SystemCall
                x86Word64Class
                x86AddressClass
                x86Word64Class)
              (constructor
                X86Program
                X86ProgramPureNext
                codegenStdoutReadyState
                codegenStdoutReadyState
                codegenStdoutReadyState
                x86OneSystemCall
                (constructor
                  X86Instruction
                  X86ZeroEDI32
                  x86Word64Class
                  x86Word64Class
                  x86AddressClass
                  x86Word64Class)
                (constructor
                  X86Program
                  X86ProgramPureNext
                  codegenStdoutReadyState
                  codegenStdoutReadyState
                  codegenStdoutReadyState
                  x86OneSystemCall
                  (constructor
                    X86Instruction
                    X86MoveEAXImmediate32
                    x86Word64Class
                    x86Word64Class
                    x86AddressClass
                    x86Word64Class
                    (x86Immediate32 (byte 60)))
                  (constructor
                    X86Program
                    X86ProgramSystemCallNext
                    codegenStdoutReadyState
                    codegenStdoutReadyState
                    codegenStdoutReadyState
                    x86NoEffects
                    (constructor
                      X86Instruction
                      X86SystemCall
                      x86Word64Class
                      x86AddressClass
                      x86Word64Class)
                    (constructor X86Program X86ProgramEnd codegenStdoutReadyState))))))))))

def lowerBytesValue =
  (lambda unrestricted value : Bytes .
    (bytes-append
      (x86EncodeProgram
        codegenInitialState
        codegenStdoutReadyState
        codegenTwoSystemCalls
        (lowerBytesProgram value))
      value))

def inlineByteCapacity1 : Bytes =
  (bytes 0)

def inlineByteCapacity2 : Bytes =
  (bytes-append inlineByteCapacity1 inlineByteCapacity1)

def inlineByteCapacity4 : Bytes =
  (bytes-append inlineByteCapacity2 inlineByteCapacity2)

def inlineByteCapacity8 : Bytes =
  (bytes-append inlineByteCapacity4 inlineByteCapacity4)

def inlineByteCapacity16 : Bytes =
  (bytes-append inlineByteCapacity8 inlineByteCapacity8)

def inlineByteCapacity32 : Bytes =
  (bytes-append inlineByteCapacity16 inlineByteCapacity16)

def inlineByteCapacity64 : Bytes =
  (bytes-append inlineByteCapacity32 inlineByteCapacity32)

def inlineByteCapacity128 : Bytes =
  (bytes-append inlineByteCapacity64 inlineByteCapacity64)

def compileBytesValue =
  (lambda unrestricted value : Bytes .
    (nat-eliminate
      (lambda unrestricted fits : Nat . (family CodegenResult))
      (constructor
        CodegenResult
        CodegenUnsupportedTerm
        (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family CodegenResult) .
          (constructor CodegenResult CodeGenerated (lowerBytesValue value))))
      (nat-less-than (bytes-length value) (succ (bytes-length inlineByteCapacity128)))))

def compileClosedNaturalElaboration =
  (lambda unrestricted result : (family ClosedNaturalElaboration) .
    (eliminate
      ClosedNaturalElaboration
      (lambda unrestricted value : (family ClosedNaturalElaboration) . (family CodegenResult))
      result
      (branch
        NaturalElaborated
        elaboratedNatural
        .
        (constructor CodegenResult CodeGenerated (lowerClosedNaturalValue elaboratedNatural)))
      (branch BytesElaborated elaboratedBytes . (compileBytesValue elaboratedBytes))
      (branch
        ByteElaborated
        elaboratedByte
        .
        (constructor CodegenResult CodeGenerated (lowerByteValue elaboratedByte)))
      (branch
        PrimitivePartial
        elaboratedPartial
        .
        (constructor CodegenResult CodegenUnsupportedTerm (succ (succ (succ zero)))))
      (branch
        UnboundVariable
        unboundSpelling
        .
        (constructor CodegenResult CodegenUnboundVariable unboundSpelling))
      (branch
        UnsupportedTerm
        unsupportedCode
        .
        (constructor CodegenResult CodegenUnsupportedTerm unsupportedCode))))

def codegenSample : (family CodegenResult) =
  (compileClosedNaturalElaboration elaboratedParserSample)

def codegenFingerprint : Nat =
  (eliminate
    CodegenResult
    (lambda unrestricted result : (family CodegenResult) . Nat)
    codegenSample
    (branch CodeGenerated machineCode . (bytes-length machineCode))
    (branch CodegenUnboundVariable codegenUnboundSpelling . zero)
    (branch CodegenUnsupportedTerm codegenUnsupportedCode . zero))