module IEEE754.Semantics where

open import IEEE754.Prelude
open import IEEE754.Sign
open import IEEE754.Format
open import IEEE754.Classification
open import IEEE754.Rounding
open import IEEE754.Exception

data DecodedShape (F : BinaryInterchangeFormat) : Type₀ where
  decodedZero : Sign → DecodedShape F
  decodedSubnormal :
    Sign → BitVec (trailingSignificandBits F) → DecodedShape F
  decodedNormal :
    Sign →
    BitVec (exponentWidth F) →
    BitVec (trailingSignificandBits F) →
    DecodedShape F
  decodedInfinity : Sign → DecodedShape F
  decodedNaN :
    Sign →
    NaNKind →
    BitVec (trailingSignificandBits F) →
    DecodedShape F

decodeShape : ∀ {F} → BinaryEncoding F → DecodedShape F
decodeShape encoding with classifyBinary encoding
... | zero-class =
  decodedZero (BinaryEncoding.sign encoding)
... | subnormal-class =
  decodedSubnormal
    (BinaryEncoding.sign encoding)
    (BinaryEncoding.trailingSignificand encoding)
... | normal-class =
  decodedNormal
    (BinaryEncoding.sign encoding)
    (BinaryEncoding.exponent encoding)
    (BinaryEncoding.trailingSignificand encoding)
... | infinity-class =
  decodedInfinity (BinaryEncoding.sign encoding)
... | nan-class =
  decodedNaN
    (BinaryEncoding.sign encoding)
    (nanKind encoding)
    (BinaryEncoding.trailingSignificand encoding)

data IEEEValue (F : BinaryInterchangeFormat) : Type₀ where
  finiteValue : Sign → ℚ → IEEEValue F
  infinityValue : Sign → IEEEValue F
  nanValue :
    Sign →
    NaNKind →
    BitVec (trailingSignificandBits F) →
    IEEEValue F

record OperationSpec
  (arity : Type₀)
  (F : BinaryInterchangeFormat)
  : Type₀ where
  constructor operation-spec
  field
    rounding : RoundingDirection
    operation : arity → Flagged (IEEEValue F)

UnaryOperation : BinaryInterchangeFormat → Type₀
UnaryOperation F = OperationSpec (IEEEValue F) F

BinaryOperation : BinaryInterchangeFormat → Type₀
BinaryOperation F = OperationSpec (IEEEValue F × IEEEValue F) F