module Platform.AArch64.RoutineEmitter

import Compiler.MachineAArch64
import Compiler.MachineAArch64Assembly
import Std.Natural

-- Shared instruction builders for small inline host routines. Logical registers
-- are supplied by each caller. x16 and x17 are reserved scratch registers: no
-- input, output or live value may use them. Signed imm32 conversion is explicit
-- so decrements and private-frame offsets mean the same on both host ISAs.
-- These builders do not provide a calling convention or preserve registers;
-- the routine's entry/return and its caller contract own that responsibility.
def ahrX0 = (constructor AArch64Register AArch64X0)
def ahrX1 = (constructor AArch64Register AArch64X1)
def ahrX2 = (constructor AArch64Register AArch64X2)
def ahrX3 = (constructor AArch64Register AArch64X3)
def ahrX4 = (constructor AArch64Register AArch64X4)
def ahrX5 = (constructor AArch64Register AArch64X5)
def ahrX6 = (constructor AArch64Register AArch64X6)
def ahrX7 = (constructor AArch64Register AArch64X7)
def ahrX8 = (constructor AArch64Register AArch64X8)
def ahrX9 = (constructor AArch64Register AArch64X9)
def ahrX10 = (constructor AArch64Register AArch64X10)
def ahrX11 = (constructor AArch64Register AArch64X11)
def ahrX12 = (constructor AArch64Register AArch64X12)
def ahrX13 = (constructor AArch64Register AArch64X13)
def ahrX14 = (constructor AArch64Register AArch64X14)
def ahrX15 = (constructor AArch64Register AArch64X15)
def ahrX16 = (constructor AArch64Register AArch64X16)
def ahrX17 = (constructor AArch64Register AArch64X17)

def ahrEmit = (lambda unrestricted instruction : (family AArch64Instruction) .
  (lambda unrestricted rest : (family AArch64Assembly) .
    (constructor AArch64Assembly AArch64AssemblyEmit instruction rest)))
def ahrAddress = (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted at : Nat .
  (ahrEmit (constructor AArch64Instruction AArch64AddImmediate ahrX16 base at))))
def ahrLoad32 = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted at : Nat .
    (lambda unrestricted rest : (family AArch64Assembly) .
      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64LoadMemory32ZeroExtend destination ahrX16 0) rest))))))
def ahrLoad64 = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted at : Nat .
    (lambda unrestricted rest : (family AArch64Assembly) .
      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64LoadMemory64 destination ahrX16 0) rest))))))
def ahrLoad8 = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted at : Nat .
    (lambda unrestricted rest : (family AArch64Assembly) .
      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64LoadMemory8ZeroExtend destination ahrX16 0) rest))))))
def ahrStore32 = (lambda unrestricted base : (family AArch64Register) .
  (lambda unrestricted at : Nat . (lambda unrestricted source : (family AArch64Register) .
    (lambda unrestricted rest : (family AArch64Assembly) .
      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64StoreMemory32 ahrX16 0 source) rest))))))
def ahrStore64 = (lambda unrestricted base : (family AArch64Register) .
  (lambda unrestricted at : Nat . (lambda unrestricted source : (family AArch64Register) .
    (lambda unrestricted rest : (family AArch64Assembly) .
      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64StoreMemory64 ahrX16 0 source) rest))))))
def ahrStore8 = (lambda unrestricted base : (family AArch64Register) .
  (lambda unrestricted at : Nat . (lambda unrestricted source : (family AArch64Register) .
    (lambda unrestricted rest : (family AArch64Assembly) .
      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64StoreMemory8 ahrX16 0 source) rest))))))

def ahrMov = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted source : (family AArch64Register) .
    (ahrEmit (constructor AArch64Instruction AArch64MoveRegister destination source))))
def ahrAdd = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted source : (family AArch64Register) .
    (ahrEmit (constructor AArch64Instruction AArch64AddRegister destination destination source))))
def ahrAnd = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted source : (family AArch64Register) .
    (ahrEmit (constructor AArch64Instruction AArch64AndRegister destination destination source))))
def ahrOr = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted source : (family AArch64Register) .
    (ahrEmit (constructor AArch64Instruction AArch64OrRegister destination destination source))))
def ahrXor = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted source : (family AArch64Register) .
    (ahrEmit (constructor AArch64Instruction AArch64ExclusiveOrRegister destination destination source))))
def ahrShl = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted amount : Nat .
    (ahrEmit (constructor AArch64Instruction AArch64ShiftLeftImmediate destination destination amount))))
def ahrShr = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted amount : Nat .
    (ahrEmit (constructor AArch64Instruction AArch64ShiftRightImmediate destination destination amount))))

-- MOV imm32 zero-extends, while arithmetic imm32 sign-extends. In particular
-- the shared loop decrement is 0xffffffff, which must become -1, not +2^32-1.
def ahrMovImm = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
    (ahrEmit (constructor AArch64Instruction AArch64MoveWideZero destination
      (naturalModuloUnchecked value 65536) (constructor AArch64HalfwordShift AArch64Shift0))
      (ahrEmit (constructor AArch64Instruction AArch64MoveWideKeep destination
        (naturalModuloUnchecked (naturalDivideUnchecked value 65536) 65536)
        (constructor AArch64HalfwordShift AArch64Shift16)) rest)))))

def ahrSignedImm = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
    (ahrMovImm destination value
      (nat-eliminate (lambda unrestricted sign : Nat . (family AArch64Assembly)) rest
        (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family AArch64Assembly) .
          (ahrEmit (constructor AArch64Instruction AArch64MoveWideKeep destination 65535
            (constructor AArch64HalfwordShift AArch64Shift32))
            (ahrEmit (constructor AArch64Instruction AArch64MoveWideKeep destination 65535
              (constructor AArch64HalfwordShift AArch64Shift48)) rest))))
        (naturalModuloUnchecked (naturalDivideUnchecked value 2147483648) 2))))))

def ahrAddImm = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
    (ahrSignedImm ahrX17 value (ahrAdd destination ahrX17
      (ahrEmit (constructor AArch64Instruction AArch64CompareImmediate destination 0) rest))))))
def ahrAndImm = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
    (ahrSignedImm ahrX17 value (ahrAnd destination ahrX17 rest)))))
def ahrCmpImm = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
    (ahrSignedImm ahrX17 value
      (ahrEmit (constructor AArch64Instruction AArch64CompareRegister destination ahrX17) rest)))))
def ahrMulImm = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
    (ahrSignedImm ahrX17 value
      (ahrEmit (constructor AArch64Instruction AArch64MultiplyRegister destination destination ahrX17) rest)))))

def ahrLabel = (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family AArch64Assembly) .
  (constructor AArch64Assembly AArch64AssemblyLabel name rest)))
def ahrBranch = (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family AArch64Assembly) .
  (constructor AArch64Assembly AArch64AssemblyBranch name rest)))
def ahrBranchIf = (lambda unrestricted condition : (family AArch64Condition) .
  (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family AArch64Assembly) .
    (constructor AArch64Assembly AArch64AssemblyBranchIf condition name rest))))
def ahrReturn = (ahrEmit (constructor AArch64Instruction AArch64Return))
def ahrEnd = (constructor AArch64Assembly AArch64AssemblyEnd)

-- Typed AArch64 assembly is decided by its maintained Alpha assembler. An
-- unresolved label or refused operand remains an empty artifact for the
-- enclosing checked ELF emitter to refuse; no host assembler is consulted.
def aarch64RoutineBytes =
  (lambda unrestricted assembly : (family AArch64Assembly) .
    (eliminate AArch64AssemblyResult
      (lambda unrestricted result : (family AArch64AssemblyResult) . Bytes)
      (aarch64Assemble assembly)
      (branch AArch64AssemblyEncoded code . code)
      (branch AArch64AssemblyEncodeDuplicateLabel name . b"")
      (branch AArch64AssemblyMissingLabel name . b"")
      (branch AArch64AssemblyDisplacementOutOfRange name . b"")
      (branch AArch64AssemblyOperandRefused value . b"")))