module Data.Float32Bits

import Data.Bytes
import Model.Config
import Std.Flag
import Std.Natural

-- The IEEE-754 binary32 bit pattern as four bytes (little-endian: byte3 holds
-- the sign bit) with its sign / zero / finite predicates as Nat flags. Lifted
-- VERBATIM out of Inference.Candidate by the R4b reroute (2026-09-09,
-- tools/refactor/extract_contract.py, reconstruction proof): the SM86 sampling
-- realization consumes a temperature as this pattern and the sampling-mode
-- contract carries it, so it belongs in foundation (RFC S2 standard = numbers),
-- next to ModelFloat64Bits. The `InferenceFloat32`/`inferenceFloat32*` names are
-- the lifted identity — renaming is the later namespace chunk.
-- Inference.Candidate imports this module (its comparison defs eliminate the
-- family here) and never redeclares it. Imports only Std.Flag.
family InferenceFloat32 : Type 0
constructor InferenceFloat32Bits
field unrestricted inferenceFloat32Byte0 : Byte
field unrestricted inferenceFloat32Byte1 : Byte
field unrestricted inferenceFloat32Byte2 : Byte
field unrestricted inferenceFloat32Byte3 : Byte

end-family

def inferenceFloat32 =
  (lambda unrestricted byte0 : Byte .
    (lambda unrestricted byte1 : Byte .
      (lambda unrestricted byte2 : Byte .
        (lambda unrestricted byte3 : Byte .
          (constructor InferenceFloat32 InferenceFloat32Bits byte0 byte1 byte2 byte3)))))

def inferenceFloat32Negative =
  (lambda unrestricted value : (family InferenceFloat32) .
    (eliminate
      InferenceFloat32
      (lambda unrestricted current : (family InferenceFloat32) . Nat)
      value
      (branch
        InferenceFloat32Bits
        byte0
        byte1
        byte2
        byte3
        .
        (inferenceFlagNot (byte-less-than byte3 (byte 128))))))

def inferenceFloat32Zero =
  (lambda unrestricted value : (family InferenceFloat32) .
    (eliminate
      InferenceFloat32
      (lambda unrestricted current : (family InferenceFloat32) . Nat)
      value
      (branch
        InferenceFloat32Bits
        byte0
        byte1
        byte2
        byte3
        .
        (inferenceFlagAnd
          (inferenceFlagAnd
            (inferenceFlagAnd
              (inferenceByteEqual byte0 (byte 0))
              (inferenceByteEqual byte1 (byte 0)))
            (inferenceByteEqual byte2 (byte 0)))
          (inferenceFlagOr
            (inferenceByteEqual byte3 (byte 0))
            (inferenceByteEqual byte3 (byte 128)))))))

def inferenceFloat32Finite =
  (lambda unrestricted value : (family InferenceFloat32) .
    (eliminate
      InferenceFloat32
      (lambda unrestricted current : (family InferenceFloat32) . Nat)
      value
      (branch
        InferenceFloat32Bits
        byte0
        byte1
        byte2
        byte3
        .
        (inferenceFlagNot
          (inferenceFlagAnd
            (inferenceFlagOr
              (inferenceByteEqual byte3 (byte 127))
              (inferenceByteEqual byte3 (byte 255)))
            (inferenceFlagNot (byte-less-than byte2 (byte 128))))))))

-- CODECS (NUM-008). InferenceFloat32 and ModelWord32 are structurally the
-- same 4-byte record (this family's own docstring: "lifted VERBATIM ...
-- next to ModelFloat64Bits"), but Alpha families are nominal, so the two
-- conversions below are the only glue needed to reuse Data.Bytes' single,
-- KAT-proven Word32 codec (evidence/language-testing/L11n-codec-owner-audit.md)
-- for float bits -- never a second byte-assembly/decode implementation.
def inferenceFloat32AsModelWord32 =
  (lambda unrestricted value : (family InferenceFloat32) .
    (eliminate
      InferenceFloat32
      (lambda unrestricted current : (family InferenceFloat32) . (family ModelWord32))
      value
      (branch InferenceFloat32Bits byte0 byte1 byte2 byte3 . (modelWord32 byte0 byte1 byte2 byte3))))

def modelWord32AsInferenceFloat32 =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family InferenceFloat32))
      value
      (branch ModelWord32Value byte0 byte1 byte2 byte3 . (inferenceFloat32 byte0 byte1 byte2 byte3))))

-- Encode*: value -> Bytes (byte assembly; LE = byte 0 first, BE = last).
def dataFloat32EncodeLE =
  (lambda unrestricted value : (family InferenceFloat32) .
    (dataBytesWord32LE (inferenceFloat32AsModelWord32 value)))

def dataFloat32EncodeBE =
  (lambda unrestricted value : (family InferenceFloat32) .
    (dataBytesWord32BE (inferenceFloat32AsModelWord32 value)))

-- Decode*Exact: canonical decode -> value only when the input is EXACTLY 4
-- bytes (short AND trailing input rejected). Same result family as
-- stdU32DecodeLEExact (DataBytesWord32ExactDecodeResult, carrying a
-- ModelWord32 on success) -- callers needing an InferenceFloat32 value
-- apply modelWord32AsInferenceFloat32 to the decoded value, the same way a
-- caller of stdU32DecodeLEExact already gets a ModelWord32 back.
def dataFloat32DecodeLEExact =
  dataBytesDecodeWord32LEExact

def dataFloat32DecodeBEExact =
  dataBytesDecodeWord32BEExact

-- Bounded integer ordering for already-admitted finite binary32 words.
-- Positive encodings increase with magnitude; negative encodings reverse
-- that order. This total order places -0 below +0, useful for extrema. It
-- does not specify NaN comparison and is not IEEE's signed-zero equality.
-- Unlike an exact rational reference comparator, it needs no large integers
-- or float instruction, so both the checker and native code can execute it.
def dataFloat32FiniteWordBelow =
  (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
    (let unrestricted leftSign = (nat-divide left 2147483648) in
      (let unrestricted rightSign = (nat-divide right 2147483648) in
        (naturalSelect (naturalEqual leftSign rightSign)
          (naturalSelect leftSign (nat-less-than right left) (nat-less-than left right))
          leftSign)))))
def dataFloat32FiniteWordMaximum =
  (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
    (naturalSelect (dataFloat32FiniteWordBelow left right) right left)))