module Platform.AArch64.LaunchRecipeRoutine

import Compiler.MachineAArch64
import Compiler.MachineAArch64Assembly
import Platform.AArch64.RoutineEmitter
import Runtime.LaunchRecipe

-- AAPCS64 realization of the shared recipe algorithm. Its four arguments are
-- x0..x3 and its result is x0. Logical temporaries occupy x4..x8; x9 is the
-- private frame base. x12..x15 (the interpreter's persistent image state), x18
-- and every callee-saved register remain untouched. No call changes x30.
-- AArch64 has no red zone, so allocate 64 aligned stack bytes explicitly and
-- release them on BOTH returns, including malformed-input rejection.
def arAddress = (lambda unrestricted base : (family AArch64Register) .
  (lambda unrestricted displacement : Nat . (lambda unrestricted tail : (family AArch64Assembly) .
    (ahrSignedImm ahrX17 displacement
      (ahrEmit (constructor AArch64Instruction AArch64AddRegister ahrX16 base ahrX17) tail)))))
def arLoad64 = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted displacement : Nat .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (arAddress base displacement
        (ahrEmit (constructor AArch64Instruction AArch64LoadMemory64 destination ahrX16 0) tail))))))
def arStore64 = (lambda unrestricted base : (family AArch64Register) .
  (lambda unrestricted displacement : Nat . (lambda unrestricted source : (family AArch64Register) .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (arAddress base displacement
        (ahrEmit (constructor AArch64Instruction AArch64StoreMemory64 ahrX16 0 source) tail))))))
def arLoad8 = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted base : (family AArch64Register) . (ahrLoad8 destination base 0)))
def arStore8 = (lambda unrestricted base : (family AArch64Register) .
  (lambda unrestricted source : (family AArch64Register) . (ahrStore8 base 0 source)))
def arSubtract = (lambda unrestricted destination : (family AArch64Register) .
  (lambda unrestricted source : (family AArch64Register) .
    (ahrEmit (constructor AArch64Instruction AArch64SubtractRegister destination destination source))))
def arCompare = (lambda unrestricted left : (family AArch64Register) .
  (lambda unrestricted right : (family AArch64Register) .
    (ahrEmit (constructor AArch64Instruction AArch64CompareRegister left right))))
def arTest = (lambda unrestricted register : (family AArch64Register) .
  (ahrEmit (constructor AArch64Instruction AArch64CompareImmediate register 0)))
def arClear = (lambda unrestricted register : (family AArch64Register) . (ahrMovImm register 0))
def arJump = (lambda unrestricted label : Bytes . (lambda unrestricted tail : (family AArch64Assembly) .
  (constructor AArch64Assembly AArch64AssemblyBranch label tail)))
def arJumpIf = (lambda unrestricted condition : (family LaunchRecipeCondition) .
  (lambda unrestricted label : Bytes . (lambda unrestricted tail : (family AArch64Assembly) .
    (constructor AArch64Assembly AArch64AssemblyBranchIf
      (eliminate LaunchRecipeCondition (lambda unrestricted current : (family LaunchRecipeCondition) . (family AArch64Condition)) condition
        (branch LaunchRecipeBelow . (constructor AArch64Condition AArch64CarryClear))
        (branch LaunchRecipeAbove . (constructor AArch64Condition AArch64UnsignedHigher))
        (branch LaunchRecipeZero . (constructor AArch64Condition AArch64Equal))
        (branch LaunchRecipeNotZero . (constructor AArch64Condition AArch64NotEqual))) label tail))))
def arReturn = (lambda unrestricted tail : (family AArch64Assembly) .
  (ahrMov ahrX0 ahrX6
    (ahrEmit (constructor AArch64Instruction AArch64AddStackPointer 64
      (constructor AArch64ImmediateShift AArch64Unshifted)) (ahrReturn tail))))

def aarch64LaunchRecipeBackend : (family LaunchRecipeBackend (family AArch64Assembly) (family AArch64Register)) =
  (constructor LaunchRecipeBackend LaunchRecipeBackendValue (family AArch64Assembly) (family AArch64Register)
    ahrMov ahrAdd arSubtract ahrAddImm arCompare ahrCmpImm arTest
    arLoad64 ahrLoad32 arLoad8 arStore64 arStore8 arClear ahrMulImm
    ahrLabel arJump arJumpIf arReturn ahrEnd
    ahrX6 ahrX3 ahrX2 ahrX1 ahrX0 ahrX9 ahrX4 ahrX5 ahrX7 ahrX8)
def aarch64LaunchRecipeAssembly =
  (ahrEmit (constructor AArch64Instruction AArch64SubtractStackPointer 64
    (constructor AArch64ImmediateShift AArch64Unshifted))
    (ahrEmit (constructor AArch64Instruction AArch64AddImmediateFromStackPointer ahrX9 64)
      (launchRecipeAssemblyFor (family AArch64Assembly) (family AArch64Register) aarch64LaunchRecipeBackend)))
def aarch64LaunchRecipeRoutine : Bytes =
  (eliminate AArch64AssemblyResult (lambda unrestricted result : (family AArch64AssemblyResult) . Bytes)
    (aarch64Assemble aarch64LaunchRecipeAssembly)
    (branch AArch64AssemblyEncoded code . code)
    (branch AArch64AssemblyEncodeDuplicateLabel name . b"")
    (branch AArch64AssemblyMissingLabel name . b"")
    (branch AArch64AssemblyDisplacementOutOfRange name . b"")
    (branch AArch64AssemblyOperandRefused value . b""))