module IEEE754.Representable where

open import IEEE754.Prelude
open import IEEE754.Sign
open import IEEE754.Format
open import IEEE754.BitVec
open import IEEE754.Semantics
open import IEEE754.Exact
open import IEEE754.Representation
open import IEEE754.FiniteSpec
open import IEEE754.FiniteDecode

import Cubical.Data.Nat.Order as ℕOrder
import Cubical.Data.Rationals as ℚ

data FiniteTextbookMagnitude {F : BinaryInterchangeFormat}
  (bias : PositiveExponentBias F) : ℚ.ℚ → Type₀ where
  representable-zero :
    FiniteTextbookMagnitude bias rationalZero
  representable-subnormal :
    (trailing : BitVec (trailingSignificandBits F)) →
     ℕOrder.< bitsToℕ trailing →
    FiniteTextbookMagnitude
      bias
      (subnormalProductMagnitude {F = F} trailing)
  representable-normal :
    (exponent : BitVec (exponentWidth F)) →
    (trailing : BitVec (trailingSignificandBits F)) →
     ℕOrder.< bitsToℕ exponent →
    suc (bitsToℕ exponent) ℕOrder.<  ^ exponentWidth F →
    HalfOpenPowerOfTwoInterval
      (trailingSignificandBits F)
      (normalSignificand {F = F} trailing) →
    FiniteTextbookMagnitude
      bias
      (normalProductMagnitude {F = F} exponent trailing)

textbookFiniteValue→representableMagnitude :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  {encoding : BinaryEncoding F} →
  {sign : Sign} →
  {magnitude : ℚ.ℚ} →
  TextbookDecodedValueSpec bias encoding (finiteValue sign magnitude) →
  FiniteTextbookMagnitude bias magnitude
textbookFiniteValue→representableMagnitude
  bias
  (textbook-zero exponent≡0 trailing≡0) =
  representable-zero
textbookFiniteValue→representableMagnitude {F} bias {encoding}
  (textbook-subnormal exponent≡0 trailing>0) =
  representable-subnormal
    (BinaryEncoding.trailingSignificand encoding)
    trailing>0
textbookFiniteValue→representableMagnitude {F} bias {encoding}
  (textbook-normal exponent>0 exponent<max significandInterval) =
  representable-normal
    (BinaryEncoding.exponent encoding)
    (BinaryEncoding.trailingSignificand encoding)
    exponent>0
    exponent<max
    significandInterval

representableMagnitude→textbookFiniteValue :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (sign : Sign) →
  {magnitude : ℚ.ℚ} →
  FiniteTextbookMagnitude bias magnitude →
  Σ
    (BinaryEncoding F)
    (λ encoding →
      TextbookDecodedValueSpec bias encoding (finiteValue sign magnitude))
representableMagnitude→textbookFiniteValue {F} bias sign representable-zero =
  binary-encoding
    sign
    (replicate {n = exponentWidth F} bit0)
    (replicate {n = trailingSignificandBits F} bit0)
  ,
  textbook-zero
    (bitsToℕ-zeroes {n = exponentWidth F})
    (bitsToℕ-zeroes {n = trailingSignificandBits F})
representableMagnitude→textbookFiniteValue {F} bias sign
  (representable-subnormal trailing trailing>0) =
  binary-encoding
    sign
    (replicate {n = exponentWidth F} bit0)
    trailing
  ,
  textbook-subnormal
    (bitsToℕ-zeroes {n = exponentWidth F})
    trailing>0
representableMagnitude→textbookFiniteValue bias sign
  (representable-normal exponent trailing exponent>0 exponent<max interval) =
  binary-encoding sign exponent trailing ,
  textbook-normal exponent>0 exponent<max interval

representableMagnitude-decodes :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (sign : Sign) →
  {magnitude : ℚ.ℚ} →
  FiniteTextbookMagnitude bias magnitude →
  Σ
    (BinaryEncoding F)
    (λ encoding → decodeValue encoding ≡ finiteValue sign magnitude)
representableMagnitude-decodes bias sign representable
  with representableMagnitude→textbookFiniteValue bias sign representable
... | encoding , textbookSpec =
  encoding , sym (textbookDecodedValueSpec-complete bias textbookSpec)

decodeFiniteValue→representableMagnitude :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (encoding : BinaryEncoding F) →
  {sign : Sign} →
  {magnitude : ℚ.ℚ} →
  decodeValue encoding ≡ finiteValue sign magnitude →
  FiniteTextbookMagnitude bias magnitude
decodeFiniteValue→representableMagnitude bias encoding decode≡finite =
  textbookFiniteValue→representableMagnitude
    bias
    (subst
      (TextbookDecodedValueSpec bias encoding)
      decode≡finite
      (decodeValue-satisfies-textbook-spec bias encoding))