module Runtime.NativeFloatPlan

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Runtime.NativePhysicalProgram
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativeMemoryPlan
import Std.Numeric.Profile

-- Numerical semantics of the guarded host commands below. This names a command
-- contract, not a new measurement of any device. Each host executor owes the
-- declared nearest-even, preserved-subnormal behavior; qualification checks
-- its rounding and tiny-value cases separately. No device operation inherits
-- this profile by falling back to host arithmetic.
def nativeFiniteFloat64Profile : (family StdNumericProfile) =
  (constructor
    StdNumericProfile
    StdNumericProfileOf
    (constructor
      StdNumericProfileIdentity
      StdProfileIdentityNamed
      b"native-f64-finite-separate-rne-v1")
    (constructor StdNumericFormat StdFormatBinary64)
    (constructor StdNumericFormat StdFormatBinary64)
    (constructor StdRounding StdRoundNearestEven)
    (constructor StdContraction StdContractionForbidden)
    (constructor StdReductionOrder StdReductionDeclaredTree)
    (constructor StdSubnormalHandling StdSubnormalsPreserved)
    (constructor StdExceptionalValues StdExceptionalFiniteOrRefuse)
    (stdTableCons
      (stdEntry stdOpAdd stdExact)
      (stdTableCons
        (stdEntry stdOpSubtract stdExact)
        (stdTableCons
          (stdEntry stdOpMultiply stdExact)
          (stdTableCons
            (stdEntry stdOpDivide stdExact)
            (stdTableCons (stdEntry stdOpSquareRoot stdExact) stdTableEmpty))))))

-- Explicit host arithmetic commands. No device operation selects this path as
-- a fallback. The caller owns scalar representation and state arena bounds.
def nativeFloat64 =
  (lambda unrestricted error : Bytes .
    (lambda unrestricted op : (family NativePhysicalFloat64Operation) .
      (lambda unrestricted destination : Nat .
        (lambda unrestricted left : (family NativePhysicalOperand) .
          (lambda unrestricted right : (family NativePhysicalOperand) .
            (nativeLaunchRecipeCommand
              (constructor
                NativePhysicalOperation
                NativePhysicalFloat64
                op
                (nativeMemoryState destination)
                left
                right)
              error))))))

def nativeFloat64Natural =
  (lambda unrestricted error : Bytes .
    (lambda unrestricted destination : Nat .
      (lambda unrestricted value : Nat .
        (nativeFloat64
          error
          (constructor NativePhysicalFloat64Operation NativePhysicalFloat64FromNatural)
          destination
          (nativeLaunchRecipeImmediate value)
          (nativeLaunchRecipeImmediate 0)))))

def nativeFloat64Binary =
  (lambda unrestricted error : Bytes .
    (lambda unrestricted op : (family NativePhysicalFloat64Operation) .
      (lambda unrestricted destination : Nat .
        (lambda unrestricted left : Nat .
          (lambda unrestricted right : Nat .
            (nativeFloat64 error op destination (nativeMemoryLoad left) (nativeMemoryLoad right)))))))

-- One typed format boundary, realized by the maintained host float commands.
-- Values occupy admitted word slots; binary32 words use the low half. Identity
-- copies bits. Narrowing is visible in the source program and is never inserted
-- by framing. The enclosing planner checks the producer/consumer endpoints.
def nativeNumericConvert =
  (lambda unrestricted error : Bytes .
    (lambda unrestricted conversion : (family StdNumericConversion) .
      (lambda unrestricted destination : Nat .
        (lambda unrestricted source : (family NativePhysicalOperand) .
          (eliminate
            StdNumericConversion
            (lambda unrestricted current : (family StdNumericConversion) .
              (pi unrestricted tail : (family NativePhysicalCommands) .
                (family NativePhysicalCommands)))
            conversion
            (branch
              StdNumericKeepFormat
              format
              .
              (nativeMemoryStoreWord64 error destination source))
            (branch
              StdNumericWidenBinary32
              .
              (nativeFloat64
                error
                (constructor NativePhysicalFloat64Operation NativePhysicalFloat64FromBinary32)
                destination
                source
                (nativeLaunchRecipeImmediate 0)))
            (branch
              StdNumericRoundBinary64
              .
              (nativeFloat64
                error
                (constructor NativePhysicalFloat64Operation NativePhysicalFloat64ToBinary32)
                destination
                source
                (nativeLaunchRecipeImmediate 0))))))))

-- Binary64 is finite iff its eleven exponent bits are not all ones.
-- RDI is a value, not an address. Only caller-saved RAX is modified; signed
-- zeros and subnormals are accepted. Platform.AArch64.FloatRoutine supplies
-- the admitted twin; an unknown host lowering still refuses.
def nativeFloat64FiniteAssembly : (family X86NativeAssembly) =
  (constructor
    X86NativeAssembly
    X86NativeAssemblyEmit
    (constructor
      X86NativeInstruction
      X86NativeMoveRegister64
      (constructor X86NativeRegister64 X86NativeRDI)
      (constructor X86NativeRegister64 X86NativeRAX))
    (constructor
      X86NativeAssembly
      X86NativeAssemblyEmit
      (constructor
        X86NativeInstruction
        X86NativeShiftRightImmediate64
        (constructor X86NativeRegister64 X86NativeRAX)
        (constructor X86NativeImmediate8 X86NativeImmediate8Value (nat-to-byte 52)))
      (constructor
        X86NativeAssembly
        X86NativeAssemblyEmit
        (constructor
          X86NativeInstruction
          X86NativeAndImmediate64
          (constructor X86NativeRegister64 X86NativeRAX)
          (x86NativeImmediate32FromNatural 2047))
        (constructor
          X86NativeAssembly
          X86NativeAssemblyEmit
          (constructor
            X86NativeInstruction
            X86NativeCompareImmediate64
            (constructor X86NativeRegister64 X86NativeRAX)
            (x86NativeImmediate32FromNatural 2047))
          (constructor
            X86NativeAssembly
            X86NativeAssemblyJumpCondition
            (constructor X86NativeCondition X86NativeConditionNotZero)
            b"finite"
            (constructor
              X86NativeAssembly
              X86NativeAssemblyEmit
              (constructor
                X86NativeInstruction
                X86NativeMoveImmediate32
                (constructor X86NativeRegister64 X86NativeRAX)
                (x86NativeImmediate32FromNatural 1))
              (constructor
                X86NativeAssembly
                X86NativeAssemblyEmit
                (constructor X86NativeInstruction X86NativeReturn)
                (constructor
                  X86NativeAssembly
                  X86NativeAssemblyLabel
                  b"finite"
                  (constructor
                    X86NativeAssembly
                    X86NativeAssemblyEmit
                    (constructor
                      X86NativeInstruction
                      X86NativeClear32
                      (constructor X86NativeRegister64 X86NativeRAX))
                    (constructor
                      X86NativeAssembly
                      X86NativeAssemblyEmit
                      (constructor X86NativeInstruction X86NativeReturn)
                      (constructor X86NativeAssembly X86NativeAssemblyEnd)))))))))))

def nativeFloat64FiniteCode : Bytes =
  (compiler-native-encode (family X86NativeAssembly) nativeFloat64FiniteAssembly)

def nativeFloat64RequireFinite =
  (lambda unrestricted value : (family NativePhysicalOperand) .
    (lambda unrestricted slot : Nat .
      (lambda unrestricted error : Bytes .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativeLaunchRecipeCommand
            (constructor
              NativePhysicalOperation
              NativePhysicalMachineRoutine
              nativeFloat64FiniteCode
              (nativeLaunchRecipeArguments
                value
                (nativeLaunchRecipeImmediate 0)
                (nativeLaunchRecipeImmediate 0)
                (nativeLaunchRecipeImmediate 0))
              (nativeLaunchRecipeStore slot))
            error
            (nativeLaunchRecipeAssertEqual
              (nativeLaunchRecipeSlotValue slot)
              (nativeLaunchRecipeImmediate 0)
              error
              tail))))))

-- Finite-domain arithmetic has an explicit refusal outcome. This avoids making
-- cross-host equality depend on unspecified NaN payload/default bits. Input
-- and output checks remain in the emitted program, including after overflow.
def nativeFiniteFloat64Binary =
  (lambda unrestricted error : Bytes .
    (lambda unrestricted slot : Nat .
      (lambda unrestricted operation : (family NativePhysicalFloat64Operation) .
        (lambda unrestricted destination : Nat .
          (lambda unrestricted left : Nat .
            (lambda unrestricted right : Nat .
              (lambda unrestricted tail : (family NativePhysicalCommands) .
                (nativeFloat64RequireFinite
                  (nativeMemoryLoad left)
                  slot
                  error
                  (nativeFloat64RequireFinite
                    (nativeMemoryLoad right)
                    slot
                    error
                    (nativeFloat64Binary
                      error
                      operation
                      destination
                      left
                      right
                      (nativeFloat64RequireFinite (nativeMemoryLoad destination) slot error tail)))))))))))