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

import Cubical.Data.Bool.Properties as Bool
import Cubical.Data.Empty as ⊥
import Cubical.Data.Nat.Order as ℕOrder

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

decodeValue-satisfies-spec :
  ∀ {F} →
  (encoding : BinaryEncoding F) →
  DecodedValueSpec encoding (decodeValue encoding)
decodeValue-satisfies-spec encoding
  with classifyBinary encoding | classifyBinary-sound encoding
... | zero-class | numeric-zero-class exponent≡0 trailing≡0 =
  spec-zero exponent≡0 trailing≡0
... | subnormal-class | numeric-subnormal-class exponent≡0 trailing>0 =
  spec-subnormal exponent≡0 trailing>0
... | normal-class |
      numeric-normal-class exponent>0 exponent<max significandInterval =
  spec-normal exponent>0 exponent<max significandInterval
... | infinity-class | numeric-infinity-class exponent≡max trailing≡0 =
  spec-infinity exponent≡max trailing≡0
... | nan-class | numeric-nan-class exponent≡max trailing>0 =
  spec-nan exponent≡max trailing>0

private
  bool-branch-contradiction :
    ∀ {b : Bool} →
    b ≡ true →
    b ≡ false →
    ⊥.⊥
  bool-branch-contradiction b≡true b≡false =
    Bool.true≢false (sym b≡true ∙ b≡false)

  false-branch-contradiction :
    ∀ {b : Bool} →
    b ≡ false →
    b ≡ true →
    ⊥.⊥
  false-branch-contradiction b≡false b≡true =
    Bool.false≢true (sym b≡false ∙ b≡true)

decodedValueSpec-complete :
  ∀ {F} {encoding : BinaryEncoding F} {value : IEEEValue F} →
  DecodedValueSpec encoding value →
  value ≡ decodeValue encoding
decodedValueSpec-complete {F} {encoding} (spec-zero exponent≡0 trailing≡0)
  with allZeros (BinaryEncoding.exponent encoding) UsingEq
     | allOnes (BinaryEncoding.exponent encoding) UsingEq
     | allZeros (BinaryEncoding.trailingSignificand encoding) UsingEq
... | true , _ | _ | true , _ = refl
... | true , _ | _ | false , trailingZeros≡false =
  ⊥.rec
    (bool-branch-contradiction
      (bitsToℕ≡0→allZeros
        (BinaryEncoding.trailingSignificand encoding)
        trailing≡0)
      trailingZeros≡false)
... | false , exponentZeros≡false | _ | _ =
  ⊥.rec
    (bool-branch-contradiction
      (bitsToℕ≡0→allZeros
        (BinaryEncoding.exponent encoding)
        exponent≡0)
      exponentZeros≡false)
decodedValueSpec-complete {F} {encoding}
  (spec-subnormal exponent≡0 trailing>0)
  with allZeros (BinaryEncoding.exponent encoding) UsingEq
     | allOnes (BinaryEncoding.exponent encoding) UsingEq
     | allZeros (BinaryEncoding.trailingSignificand encoding) UsingEq
... | true , _ | _ | false , _ = refl
... | true , _ | _ | true , trailingZeros≡true =
  ⊥.rec
    (false-branch-contradiction
      (positive→allZeros≡false
        (BinaryEncoding.trailingSignificand encoding)
        trailing>0)
      trailingZeros≡true)
... | false , exponentZeros≡false | _ | _ =
  ⊥.rec
    (bool-branch-contradiction
      (bitsToℕ≡0→allZeros
        (BinaryEncoding.exponent encoding)
        exponent≡0)
      exponentZeros≡false)
decodedValueSpec-complete {F} {encoding}
  (spec-normal exponent>0 exponent<max significandInterval)
  with allZeros (BinaryEncoding.exponent encoding) UsingEq
     | allOnes (BinaryEncoding.exponent encoding) UsingEq
     | allZeros (BinaryEncoding.trailingSignificand encoding) UsingEq
... | false , _ | false , _ | _ = refl
... | true , exponentZeros≡true | _ | _ =
  ⊥.rec
    (false-branch-contradiction
      (positive→allZeros≡false
        (BinaryEncoding.exponent encoding)
        exponent>0)
      exponentZeros≡true)
... | false , _ | true , exponentOnes≡true | _ =
  ⊥.rec
    (false-branch-contradiction
      (below-reserved→allOnes≡false
        (BinaryEncoding.exponent encoding)
        exponent<max)
      exponentOnes≡true)
decodedValueSpec-complete {F} {encoding}
  (spec-infinity exponent≡max trailing≡0)
  with allZeros (BinaryEncoding.exponent encoding) UsingEq
     | allOnes (BinaryEncoding.exponent encoding) UsingEq
     | allZeros (BinaryEncoding.trailingSignificand encoding) UsingEq
... | false , _ | true , _ | true , _ = refl
... | true , exponentZeros≡true | _ | _ =
  ⊥.rec
    (not-allZeros-and-allOnes
      (BinaryEncoding.exponent encoding)
      (subst Bool→Type (sym exponentZeros≡true) tt)
      (subst
        Bool→Type
        (sym
          (suc-bitsToℕ≡2^n→allOnes
            (BinaryEncoding.exponent encoding)
            exponent≡max))
        tt))
... | false , _ | false , exponentOnes≡false | _ =
  ⊥.rec
    (bool-branch-contradiction
      (suc-bitsToℕ≡2^n→allOnes
        (BinaryEncoding.exponent encoding)
        exponent≡max)
      exponentOnes≡false)
... | false , _ | true , _ | false , trailingZeros≡false =
  ⊥.rec
    (bool-branch-contradiction
      (bitsToℕ≡0→allZeros
        (BinaryEncoding.trailingSignificand encoding)
        trailing≡0)
      trailingZeros≡false)
decodedValueSpec-complete {F} {encoding}
  (spec-nan exponent≡max trailing>0)
  with allZeros (BinaryEncoding.exponent encoding) UsingEq
     | allOnes (BinaryEncoding.exponent encoding) UsingEq
     | allZeros (BinaryEncoding.trailingSignificand encoding) UsingEq
... | false , _ | true , _ | false , _ = refl
... | true , exponentZeros≡true | _ | _ =
  ⊥.rec
    (not-allZeros-and-allOnes
      (BinaryEncoding.exponent encoding)
      (subst Bool→Type (sym exponentZeros≡true) tt)
      (subst
        Bool→Type
        (sym
          (suc-bitsToℕ≡2^n→allOnes
            (BinaryEncoding.exponent encoding)
            exponent≡max))
        tt))
... | false , _ | false , exponentOnes≡false | _ =
  ⊥.rec
    (bool-branch-contradiction
      (suc-bitsToℕ≡2^n→allOnes
        (BinaryEncoding.exponent encoding)
        exponent≡max)
      exponentOnes≡false)
... | false , _ | true , _ | true , trailingZeros≡true =
  ⊥.rec
    (false-branch-contradiction
      (positive→allZeros≡false
        (BinaryEncoding.trailingSignificand encoding)
        trailing>0)
      trailingZeros≡true)