module IEEE754.Representation where

open import IEEE754.Prelude
open import IEEE754.Format
open import IEEE754.Classification
open import IEEE754.BitVec
open import IEEE754.Exact

import Cubical.Data.Nat.Order as ℕOrder

record HalfOpenPowerOfTwoInterval (p x : ℕ) : Type₀ where
  constructor in-half-open-power-interval
  field
    lower : (2 ^ p) ℕOrder.≤ x
    upper : x ℕOrder.< (2 ^ suc p)

subnormalSignificand-bound :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  bitsToℕ trailing ℕOrder.< (2 ^ trailingSignificandBits F)
subnormalSignificand-bound trailing = bitsToℕ-bound trailing

trailingSignificand≤allOnes :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  bitsToℕ trailing ℕOrder.≤
  bitsToℕ (replicate {n = trailingSignificandBits F} bit1)
trailingSignificand≤allOnes trailing =
  bitsToℕ≤allOnes trailing

normalSignificand-invariant :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  HalfOpenPowerOfTwoInterval
    (trailingSignificandBits F)
    (normalSignificand {F = F} trailing)
normalSignificand-invariant {F} trailing =
  in-half-open-power-interval
    (normalSignificand-lower {F = F} trailing)
    (normalSignificand-upper {F = F} trailing)

data NumericExponentEvidence {n : ℕ}
  (exponent : BitVec (suc n)) : ExponentClass → Type₀ where
  numeric-all-zero :
    bitsToℕ exponent ≡ 0 →
    NumericExponentEvidence exponent all-zero-exponent
  numeric-finite :
    0 ℕOrder.< bitsToℕ exponent →
    suc (bitsToℕ exponent) ℕOrder.< 2 ^ suc n →
    NumericExponentEvidence exponent finite-exponent
  numeric-all-one :
    suc (bitsToℕ exponent) ≡ 2 ^ suc n →
    NumericExponentEvidence exponent all-one-exponent

classifyExponent-sound :
  ∀ {n} →
  (exponent : BitVec (suc n)) →
  NumericExponentEvidence exponent (classifyExponent exponent)
classifyExponent-sound exponent
  with allZeros exponent UsingEq | allOnes exponent UsingEq
... | true , zeros≡true | _ =
  numeric-all-zero
    (allZeros→bitsToℕ≡0
      exponent
      (subst Bool→Type (sym zeros≡true) tt))
... | false , zeros≡false | true , ones≡true =
  numeric-all-one
    (allOnes→suc-bitsToℕ≡2^n
      exponent
      (subst Bool→Type (sym ones≡true) tt))
... | false , zeros≡false | false , ones≡false =
  numeric-finite
    (notAllZeros→positive
      exponent
      (subst Bool→Type (sym (cong not zeros≡false)) tt))
    (notAllOnes→below-reserved
      exponent
      (subst Bool→Type (sym (cong not ones≡false)) tt))

data NumericBinaryClassEvidence {F : BinaryInterchangeFormat}
  (encoding : BinaryEncoding F) : BinaryClass → Type₀ where
  numeric-zero-class :
    bitsToℕ (BinaryEncoding.exponent encoding) ≡ 0 →
    bitsToℕ (BinaryEncoding.trailingSignificand encoding) ≡ 0 →
    NumericBinaryClassEvidence encoding zero-class
  numeric-subnormal-class :
    bitsToℕ (BinaryEncoding.exponent encoding) ≡ 0 →
    0 ℕOrder.< bitsToℕ (BinaryEncoding.trailingSignificand encoding) →
    NumericBinaryClassEvidence encoding subnormal-class
  numeric-normal-class :
    0 ℕOrder.< bitsToℕ (BinaryEncoding.exponent encoding) →
    suc (bitsToℕ (BinaryEncoding.exponent encoding)) ℕOrder.<
      2 ^ exponentWidth F →
    HalfOpenPowerOfTwoInterval
      (trailingSignificandBits F)
      (normalSignificand
        {F = F}
        (BinaryEncoding.trailingSignificand encoding)) →
    NumericBinaryClassEvidence encoding normal-class
  numeric-infinity-class :
    suc (bitsToℕ (BinaryEncoding.exponent encoding)) ≡
      2 ^ exponentWidth F →
    bitsToℕ (BinaryEncoding.trailingSignificand encoding) ≡ 0 →
    NumericBinaryClassEvidence encoding infinity-class
  numeric-nan-class :
    suc (bitsToℕ (BinaryEncoding.exponent encoding)) ≡
      2 ^ exponentWidth F →
    0 ℕOrder.< bitsToℕ (BinaryEncoding.trailingSignificand encoding) →
    NumericBinaryClassEvidence encoding nan-class

classifyBinary-sound :
  ∀ {F} →
  (encoding : BinaryEncoding F) →
  NumericBinaryClassEvidence encoding (classifyBinary encoding)
classifyBinary-sound {F} encoding
  with allZeros (BinaryEncoding.exponent encoding) UsingEq
     | allOnes (BinaryEncoding.exponent encoding) UsingEq
     | allZeros (BinaryEncoding.trailingSignificand encoding) UsingEq
... | true , exponentZeros≡true | _ | true , trailingZeros≡true =
  numeric-zero-class
    (allZeros→bitsToℕ≡0
      (BinaryEncoding.exponent encoding)
      (subst Bool→Type (sym exponentZeros≡true) tt))
    (allZeros→bitsToℕ≡0
      (BinaryEncoding.trailingSignificand encoding)
      (subst Bool→Type (sym trailingZeros≡true) tt))
... | true , exponentZeros≡true | _ | false , trailingZeros≡false =
  numeric-subnormal-class
    (allZeros→bitsToℕ≡0
      (BinaryEncoding.exponent encoding)
      (subst Bool→Type (sym exponentZeros≡true) tt))
    (notAllZeros→positive
      (BinaryEncoding.trailingSignificand encoding)
      (subst Bool→Type (sym (cong not trailingZeros≡false)) tt))
... | false , _ | true , exponentOnes≡true | true , trailingZeros≡true =
  numeric-infinity-class
    (allOnes→suc-bitsToℕ≡2^n
      (BinaryEncoding.exponent encoding)
      (subst Bool→Type (sym exponentOnes≡true) tt))
    (allZeros→bitsToℕ≡0
      (BinaryEncoding.trailingSignificand encoding)
      (subst Bool→Type (sym trailingZeros≡true) tt))
... | false , _ | true , exponentOnes≡true | false , trailingZeros≡false =
  numeric-nan-class
    (allOnes→suc-bitsToℕ≡2^n
      (BinaryEncoding.exponent encoding)
      (subst Bool→Type (sym exponentOnes≡true) tt))
    (notAllZeros→positive
      (BinaryEncoding.trailingSignificand encoding)
      (subst Bool→Type (sym (cong not trailingZeros≡false)) tt))
... | false , exponentZeros≡false | false , exponentOnes≡false | _ =
  numeric-normal-class
    (notAllZeros→positive
      (BinaryEncoding.exponent encoding)
      (subst Bool→Type (sym (cong not exponentZeros≡false)) tt))
    (notAllOnes→below-reserved
      (BinaryEncoding.exponent encoding)
      (subst Bool→Type (sym (cong not exponentOnes≡false)) tt))
    (normalSignificand-invariant
      {F = F}
      (BinaryEncoding.trailingSignificand encoding))