module IEEE754.Exact 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

import Cubical.Data.Int as ℤ
import Cubical.Data.Nat as ℕ
import Cubical.Data.Nat.Order as ℕOrder
import Cubical.Data.NatPlusOne as ℕ₊₁
import Cubical.Data.Rationals as ℚ

exponentBias : BinaryInterchangeFormat → ℕ
exponentBias F =
  (2 ^ BinaryInterchangeFormat.exponentBitsMinusOne F) ℕ.∸ 1

powerOfTwoDenominator : ℕ → ℕ₊₁.ℕ₊₁
powerOfTwoDenominator zero = ℕ₊₁.1+ 0
powerOfTwoDenominator (suc k) =
  ℕ₊₁.1+ 1 ℕ₊₁.·₊₁ powerOfTwoDenominator k

powerOfTwoDenominator-+ :
  (m n : ℕ) →
  powerOfTwoDenominator (m + n) ≡
  powerOfTwoDenominator m ℕ₊₁.·₊₁ powerOfTwoDenominator n
powerOfTwoDenominator-+ zero n =
  sym (ℕ₊₁.·₊₁-identityˡ (powerOfTwoDenominator n))
powerOfTwoDenominator-+ (suc m) n =
  cong (ℕ₊₁.1+ 1 ℕ₊₁.·₊₁_) (powerOfTwoDenominator-+ m n)
  ∙ ℕ₊₁.·₊₁-assoc
      (ℕ₊₁.1+ 1)
      (powerOfTwoDenominator m)
      (powerOfTwoDenominator n)

powerOfTwoDenominator-value :
  (k : ℕ) →
  ℕ₊₁.ℕ₊₁→ℕ (powerOfTwoDenominator k) ≡ 2 ^ k
powerOfTwoDenominator-value zero = refl
powerOfTwoDenominator-value (suc k) =
  cong (2 ·_) (powerOfTwoDenominator-value k)

applySignℚ : Sign → ℚ.ℚ → ℚ.ℚ
applySignℚ positive q = q
applySignℚ negative q = ℚ.- q

rationalZero : ℚ.ℚ
rationalZero = ℚ.[ ℤ.pos 0 / ℕ₊₁.1+ 0 ]

scaleNatByPowerOfTwo : ℕ → ℤ.ℤ → ℚ.ℚ
scaleNatByPowerOfTwo n (ℤ.pos k) =
  ℚ.[ ℤ.pos (n · (2 ^ k)) / ℕ₊₁.1+ 0 ]
scaleNatByPowerOfTwo n (ℤ.negsuc k) =
  ℚ.[ ℤ.pos n / powerOfTwoDenominator (suc k) ]

subnormalShift : (F : BinaryInterchangeFormat) → ℤ.ℤ
subnormalShift F =
  ℤ._ℕ-_ 1 (exponentBias F + trailingSignificandBits F)

normalShift :
  (F : BinaryInterchangeFormat) →
  BitVec (exponentWidth F) →
  ℤ.ℤ
normalShift F exponent =
  ℤ._ℕ-_ (bitsToℕ exponent)
          (exponentBias F + trailingSignificandBits F)

subnormalMagnitude :
  ∀ {F} →
  BitVec (trailingSignificandBits F) →
  ℚ.ℚ
subnormalMagnitude {F} trailing =
  scaleNatByPowerOfTwo
    (bitsToℕ trailing)
    (subnormalShift F)

normalSignificand :
  ∀ {F} →
  BitVec (trailingSignificandBits F) →
  ℕ
normalSignificand {F} trailing =
  (2 ^ trailingSignificandBits F) + bitsToℕ trailing

normalSignificand-lower :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  (2 ^ trailingSignificandBits F) ℕOrder.≤
  normalSignificand {F = F} trailing
normalSignificand-lower {F} trailing =
  ℕOrder.≤SumLeft
    {n = 2 ^ trailingSignificandBits F}
    {k = bitsToℕ trailing}

normalSignificand-upper :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  normalSignificand {F = F} trailing ℕOrder.<
  2 ^ suc (trailingSignificandBits F)
normalSignificand-upper {F} trailing =
  subst
    (normalSignificand {F = F} trailing ℕOrder.<_)
    (sym (pow2-suc-expand (trailingSignificandBits F)))
    (ℕOrder.<-k+
      {m = bitsToℕ trailing}
      {n = 2 ^ trailingSignificandBits F}
      {k = 2 ^ trailingSignificandBits F}
      (bitsToℕ-bound trailing))

normalMagnitude :
  ∀ {F} →
  BitVec (exponentWidth F) →
  BitVec (trailingSignificandBits F) →
  ℚ.ℚ
normalMagnitude {F} exponent trailing =
  scaleNatByPowerOfTwo
    (normalSignificand {F = F} trailing)
    (normalShift F exponent)

decodeValue : ∀ {F} → BinaryEncoding F → IEEEValue F
decodeValue {F} encoding with classifyBinary encoding
... | zero-class =
  finiteValue (BinaryEncoding.sign encoding) rationalZero
... | subnormal-class =
  finiteValue
    (BinaryEncoding.sign encoding)
    (subnormalMagnitude
      {F = F}
      (BinaryEncoding.trailingSignificand encoding))
... | normal-class =
  finiteValue
    (BinaryEncoding.sign encoding)
    (normalMagnitude
      {F = F}
      (BinaryEncoding.exponent encoding)
      (BinaryEncoding.trailingSignificand encoding))
... | infinity-class =
  infinityValue (BinaryEncoding.sign encoding)
... | nan-class =
  nanValue
    (BinaryEncoding.sign encoding)
    (nanKind encoding)
    (BinaryEncoding.trailingSignificand encoding)

binary16-bias : exponentBias binary16 ≡ 15
binary16-bias = refl

binary32-bias : exponentBias binary32 ≡ 127
binary32-bias = refl

binary64-bias : exponentBias binary64 ≡ 1023
binary64-bias = refl

binary128-bias : exponentBias binary128 ≡ 16383
binary128-bias = refl