module Runtime.NativeMemoryPlan

import Runtime.NativeMemoryRoutine
import Runtime.NativePhysicalProgram
import Runtime.NativeLaunchRecipeLoad
import Model.Word64
import Std.Natural

-- Native commands over admitted host regions. Allocation and nonoverlap are
-- planner obligations; these are shared by frames and durable state staging.
def nativeMemoryState =
  (lambda unrestricted offset : Nat .
    (constructor
      NativePhysicalOperand
      NativePhysicalStateAddress
      (modelWord64FromNaturalTruncated offset)))

def nativeMemoryLoad =
  (lambda unrestricted offset : Nat .
    (constructor
      NativePhysicalOperand
      NativePhysicalStateLoad64
      (modelWord64FromNaturalTruncated offset)))

def nativeMemoryCopyPayload =
  (lambda unrestricted offset : Nat .
    (lambda unrestricted bytes : Bytes .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (nat-eliminate
          (lambda unrestricted count : Nat . (family NativePhysicalCommands))
          tail
          (lambda unrestricted previous : Nat .
            (lambda unrestricted ignored : (family NativePhysicalCommands) .
              (nativeLaunchRecipeCommand
                (constructor
                  NativePhysicalOperation
                  NativePhysicalCopyPayloadToState
                  (modelWord64FromNaturalTruncated offset)
                  (modelWord64FromNaturalTruncated (bytes-length bytes))
                  bytes)
                b"memory-copy"
                tail)))
          (naturalNonzero (bytes-length bytes))))))

def nativeMemoryCopyOperands =
  (lambda unrestricted destination : (family NativePhysicalOperand) .
    (lambda unrestricted source : (family NativePhysicalOperand) .
      (lambda unrestricted extent : Nat .
        (lambda unrestricted slot : Nat .
          (lambda unrestricted error : Bytes .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (nativeLaunchRecipeCommand
                (constructor
                  NativePhysicalOperation
                  NativePhysicalMachineRoutine
                  nativeMemoryCopyCode
                  (nativeLaunchRecipeArguments
                    destination
                    source
                    (nativeLaunchRecipeImmediate extent)
                    (nativeLaunchRecipeImmediate 0))
                  (nativeLaunchRecipeStore slot))
                error
                (nativeLaunchRecipeAssertEqual
                  (nativeLaunchRecipeSlotValue slot)
                  (nativeLaunchRecipeImmediate 0)
                  error
                  tail))))))))

def nativeMemoryCompareOperands =
  (lambda unrestricted left : (family NativePhysicalOperand) .
    (lambda unrestricted right : (family NativePhysicalOperand) .
      (lambda unrestricted extent : Nat .
        (lambda unrestricted slot : Nat .
          (lambda unrestricted error : Bytes .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (nativeLaunchRecipeCommand
                (constructor
                  NativePhysicalOperation
                  NativePhysicalMachineRoutine
                  nativeMemoryEqualCode
                  (nativeLaunchRecipeArguments
                    left
                    right
                    (nativeLaunchRecipeImmediate extent)
                    (nativeLaunchRecipeImmediate 0))
                  (nativeLaunchRecipeStore slot))
                error
                (nativeLaunchRecipeAssertEqual
                  (nativeLaunchRecipeSlotValue slot)
                  (nativeLaunchRecipeImmediate 1)
                  error
                  tail))))))))

def nativeMemoryCompareRegions =
  (lambda unrestricted left : Nat .
    (lambda unrestricted right : Nat .
      (lambda unrestricted extent : Nat .
        (nativeMemoryCompareOperands (nativeMemoryState left) (nativeMemoryState right) extent))))

-- Store one explicit runtime word; caller admission owns the destination.
def nativeMemoryStoreWord64 =
  (lambda unrestricted error : Bytes .
    (lambda unrestricted destination : Nat .
      (lambda unrestricted value : (family NativePhysicalOperand) .
        (nativeLaunchRecipeCommand
          (constructor
            NativePhysicalOperation
            NativePhysicalStoreWord64
            (nativeMemoryState destination)
            value)
          error))))