module IEEE754.FiniteDecode where

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

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

subnormalProductMagnitude :
  ∀ {F} →
  BitVec (trailingSignificandBits F) →
  ℚ.ℚ
subnormalProductMagnitude {F} trailing =
  trailingFraction {F = F} trailing ℚ.· pow2ℚ (emin F)

normalProductMagnitude :
  ∀ {F} →
  BitVec (exponentWidth F) →
  BitVec (trailingSignificandBits F) →
  ℚ.ℚ
normalProductMagnitude {F} exponent trailing =
  normalCoefficient {F = F} trailing ℚ.·
  pow2ℚ (unbiasedExponent F exponent)

data TextbookDecodedValueSpec {F : BinaryInterchangeFormat}
  (bias : PositiveExponentBias F)
  (encoding : BinaryEncoding F) : IEEEValue F → Type₀ where
  textbook-zero :
    bitsToℕ (BinaryEncoding.exponent encoding) ≡  →
    bitsToℕ (BinaryEncoding.trailingSignificand encoding) ≡  →
    TextbookDecodedValueSpec bias encoding
      (finiteValue (BinaryEncoding.sign encoding) rationalZero)
  textbook-subnormal :
    bitsToℕ (BinaryEncoding.exponent encoding) ≡  →
     ℕOrder.< bitsToℕ (BinaryEncoding.trailingSignificand encoding) →
    TextbookDecodedValueSpec bias encoding
      (finiteValue
        (BinaryEncoding.sign encoding)
        (subnormalProductMagnitude
          {F = F}
          (BinaryEncoding.trailingSignificand encoding)))
  textbook-normal :
     ℕOrder.< bitsToℕ (BinaryEncoding.exponent encoding) →
    suc (bitsToℕ (BinaryEncoding.exponent encoding)) ℕOrder.<
       ^ exponentWidth F →
    HalfOpenPowerOfTwoInterval
      (trailingSignificandBits F)
      (normalSignificand
        {F = F}
        (BinaryEncoding.trailingSignificand encoding)) →
    TextbookDecodedValueSpec bias encoding
      (finiteValue
        (BinaryEncoding.sign encoding)
        (normalProductMagnitude
          {F = F}
          (BinaryEncoding.exponent encoding)
          (BinaryEncoding.trailingSignificand encoding)))
  textbook-infinity :
    suc (bitsToℕ (BinaryEncoding.exponent encoding)) ≡
       ^ exponentWidth F →
    bitsToℕ (BinaryEncoding.trailingSignificand encoding) ≡  →
    TextbookDecodedValueSpec bias encoding
      (infinityValue (BinaryEncoding.sign encoding))
  textbook-nan :
    suc (bitsToℕ (BinaryEncoding.exponent encoding)) ≡
       ^ exponentWidth F →
     ℕOrder.< bitsToℕ (BinaryEncoding.trailingSignificand encoding) →
    TextbookDecodedValueSpec bias encoding
      (nanValue
        (BinaryEncoding.sign encoding)
        (nanKind encoding)
        (BinaryEncoding.trailingSignificand encoding))

decodedSpec→textbookSpec :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  {encoding : BinaryEncoding F} →
  {value : IEEEValue F} →
  DecodedValueSpec encoding value →
  TextbookDecodedValueSpec bias encoding value
decodedSpec→textbookSpec bias (spec-zero exponent≡0 trailing≡0) =
  textbook-zero exponent≡0 trailing≡0
decodedSpec→textbookSpec {F} bias {encoding}
  (spec-subnormal exponent≡0 trailing>0) =
  subst
    (TextbookDecodedValueSpec bias encoding)
    (sym
      (cong
        (finiteValue (BinaryEncoding.sign encoding))
        (subnormalMagnitude-textbook-product
          bias
          (BinaryEncoding.trailingSignificand encoding))))
    (textbook-subnormal exponent≡0 trailing>0)
decodedSpec→textbookSpec {F} bias {encoding}
  (spec-normal exponent>0 exponent<max significandInterval) =
  subst
    (TextbookDecodedValueSpec bias encoding)
    (sym
      (cong
        (finiteValue (BinaryEncoding.sign encoding))
        (normalMagnitude-textbook-product
          (BinaryEncoding.exponent encoding)
          (BinaryEncoding.trailingSignificand encoding))))
    (textbook-normal exponent>0 exponent<max significandInterval)
decodedSpec→textbookSpec bias (spec-infinity exponent≡max trailing≡0) =
  textbook-infinity exponent≡max trailing≡0
decodedSpec→textbookSpec bias (spec-nan exponent≡max trailing>0) =
  textbook-nan exponent≡max trailing>0

textbookSpec→decodedSpec :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  {encoding : BinaryEncoding F} →
  {value : IEEEValue F} →
  TextbookDecodedValueSpec bias encoding value →
  DecodedValueSpec encoding value
textbookSpec→decodedSpec bias (textbook-zero exponent≡0 trailing≡0) =
  spec-zero exponent≡0 trailing≡0
textbookSpec→decodedSpec {F} bias {encoding}
  (textbook-subnormal exponent≡0 trailing>0) =
  subst
    (DecodedValueSpec encoding)
    (cong
      (finiteValue (BinaryEncoding.sign encoding))
      (subnormalMagnitude-textbook-product
        bias
        (BinaryEncoding.trailingSignificand encoding)))
    (spec-subnormal exponent≡0 trailing>0)
textbookSpec→decodedSpec {F} bias {encoding}
  (textbook-normal exponent>0 exponent<max significandInterval) =
  subst
    (DecodedValueSpec encoding)
    (cong
      (finiteValue (BinaryEncoding.sign encoding))
      (normalMagnitude-textbook-product
        (BinaryEncoding.exponent encoding)
        (BinaryEncoding.trailingSignificand encoding)))
    (spec-normal exponent>0 exponent<max significandInterval)
textbookSpec→decodedSpec bias (textbook-infinity exponent≡max trailing≡0) =
  spec-infinity exponent≡max trailing≡0
textbookSpec→decodedSpec bias (textbook-nan exponent≡max trailing>0) =
  spec-nan exponent≡max trailing>0

decodeValue-satisfies-textbook-spec :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (encoding : BinaryEncoding F) →
  TextbookDecodedValueSpec bias encoding (decodeValue encoding)
decodeValue-satisfies-textbook-spec bias encoding =
  decodedSpec→textbookSpec bias (decodeValue-satisfies-spec encoding)

textbookDecodedValueSpec-complete :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  {encoding : BinaryEncoding F} →
  {value : IEEEValue F} →
  TextbookDecodedValueSpec bias encoding value →
  value ≡ decodeValue encoding
textbookDecodedValueSpec-complete bias textbookSpec =
  decodedValueSpec-complete (textbookSpec→decodedSpec bias textbookSpec)

textbookDecodedValueSpec-unique :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  {encoding : BinaryEncoding F} →
  {left right : IEEEValue F} →
  TextbookDecodedValueSpec bias encoding left →
  TextbookDecodedValueSpec bias encoding right →
  left ≡ right
textbookDecodedValueSpec-unique bias leftSpec rightSpec =
  textbookDecodedValueSpec-complete bias leftSpec ∙
  sym (textbookDecodedValueSpec-complete bias rightSpec)