module IEEE754.BitVec where

open import IEEE754.Prelude
import Cubical.Data.Empty as ⊥
import Cubical.Data.Nat as ℕ
import Cubical.Data.Nat.Order as ℕOrder

bitToℕ : Bit → ℕ
bitToℕ false = 0
bitToℕ true = 1

bitsToℕ : ∀ {n} → BitVec n → ℕ
bitsToℕ {zero} [] = 0
bitsToℕ {suc n} (bit ∷ bits) =
  bitToℕ bit · (2 ^ n) + bitsToℕ bits

bitToℕ-bit0 : bitToℕ bit0 ≡ 0
bitToℕ-bit0 = refl

bitToℕ-bit1 : bitToℕ bit1 ≡ 1
bitToℕ-bit1 = refl

pow2-suc-expand : ∀ n → 2 ^ suc n ≡ (2 ^ n) + (2 ^ n)
pow2-suc-expand n =
  cong ((2 ^ n) +_) (ℕ.·-identityˡ (2 ^ n))

pow2-positive : ∀ n → 0 ℕOrder.< 2 ^ n
pow2-positive zero = 0 , refl
pow2-positive (suc n) =
  subst
    (0 ℕOrder.<_)
    (sym (pow2-suc-expand n))
    (ℕOrder.<≤-trans
      (pow2-positive n)
      (ℕOrder.≤SumLeft {n = 2 ^ n} {k = 2 ^ n}))

pow2-strictly-increases : ∀ n → (2 ^ n) ℕOrder.< (2 ^ suc n)
pow2-strictly-increases n =
  subst
    ((2 ^ n) ℕOrder.<_)
    (sym (pow2-suc-expand n))
    (subst
      (λ value → value ℕOrder.< ((2 ^ n) + (2 ^ n)))
      (ℕ.+-zero (2 ^ n))
      (ℕOrder.<-k+
        {m = 0}
        {n = 2 ^ n}
        {k = 2 ^ n}
        (pow2-positive n)))

bitsToℕ-cons-zero :
  ∀ {n} →
  (bits : BitVec n) →
  bitsToℕ (bit0 ∷ bits) ≡ bitsToℕ bits
bitsToℕ-cons-zero bits = refl

bitsToℕ-cons-one :
  ∀ {n} →
  (bits : BitVec n) →
  bitsToℕ (bit1 ∷ bits) ≡ (2 ^ n) + bitsToℕ bits
bitsToℕ-cons-one {n} bits =
  cong (_+ bitsToℕ bits) (ℕ.·-identityˡ (2 ^ n))

bitsToℕ-zeroes : ∀ {n} → bitsToℕ (replicate {n = n} bit0) ≡ 0
bitsToℕ-zeroes {zero} = refl
bitsToℕ-zeroes {suc n} = bitsToℕ-zeroes {n}

bitsToℕ-all-ones-3 : bitsToℕ (bit1 ∷ bit1 ∷ bit1 ∷ []) ≡ 7
bitsToℕ-all-ones-3 = refl

allZeros→bitsToℕ≡0 :
  ∀ {n} →
  (bits : BitVec n) →
  Bool→Type (allZeros bits) →
  bitsToℕ bits ≡ 0
allZeros→bitsToℕ≡0 [] _ = refl
allZeros→bitsToℕ≡0 (false ∷ bits) proof =
  allZeros→bitsToℕ≡0 bits proof
allZeros→bitsToℕ≡0 (true ∷ bits) ()

notAllZeros→positive :
  ∀ {n} →
  (bits : BitVec n) →
  Bool→Type (not (allZeros bits)) →
  0 ℕOrder.< bitsToℕ bits
notAllZeros→positive [] ()
notAllZeros→positive (false ∷ bits) proof =
  notAllZeros→positive bits proof
notAllZeros→positive {suc n} (true ∷ bits) _ =
  subst
    (0 ℕOrder.<_)
    (sym (bitsToℕ-cons-one bits))
    (ℕOrder.<≤-trans
      (pow2-positive n)
      (ℕOrder.≤SumLeft {n = 2 ^ n} {k = bitsToℕ bits}))

bitsToℕ≡0→allZeros :
  ∀ {n} →
  (bits : BitVec n) →
  bitsToℕ bits ≡ 0 →
  allZeros bits ≡ true
bitsToℕ≡0→allZeros [] _ = refl
bitsToℕ≡0→allZeros (false ∷ bits) bits≡0 =
  bitsToℕ≡0→allZeros bits bits≡0
bitsToℕ≡0→allZeros (true ∷ bits) bits≡0 =
  ⊥.rec
    (ℕOrder.¬-<-zero
      (subst
        (0 ℕOrder.<_)
        bits≡0
        (notAllZeros→positive (true ∷ bits) tt)))

positive→allZeros≡false :
  ∀ {n} →
  (bits : BitVec n) →
  0 ℕOrder.< bitsToℕ bits →
  allZeros bits ≡ false
positive→allZeros≡false bits positive with allZeros bits UsingEq
... | false , allZeros≡false = allZeros≡false
... | true , allZeros≡true =
  ⊥.rec
    (ℕOrder.¬-<-zero
      (subst
        (0 ℕOrder.<_)
        (allZeros→bitsToℕ≡0
          bits
          (subst Bool→Type (sym allZeros≡true) tt))
        positive))

bitsToℕ-bound : ∀ {n} → (bits : BitVec n) → bitsToℕ bits ℕOrder.< 2 ^ n
bitsToℕ-bound [] = 0 , refl
bitsToℕ-bound {suc n} (false ∷ bits) =
  subst
    (bitsToℕ (false ∷ bits) ℕOrder.<_)
    (sym (pow2-suc-expand n))
    (ℕOrder.<≤-trans
      (bitsToℕ-bound bits)
      (ℕOrder.≤SumLeft {n = 2 ^ n} {k = 2 ^ n}))
bitsToℕ-bound {suc n} (true ∷ bits) =
  subst
    (bitsToℕ (true ∷ bits) ℕOrder.<_)
    (sym (pow2-suc-expand n))
    (subst
      (λ value → value ℕOrder.< ((2 ^ n) + (2 ^ n)))
      (sym (bitsToℕ-cons-one bits))
      (ℕOrder.<-k+
        {m = bitsToℕ bits}
        {n = 2 ^ n}
        {k = 2 ^ n}
        (bitsToℕ-bound bits)))

allOnes-suc-bitsToℕ : ∀ {n} → suc (bitsToℕ (replicate {n = n} bit1)) ≡ 2 ^ n
allOnes-suc-bitsToℕ {zero} = refl
allOnes-suc-bitsToℕ {suc n} =
  cong suc (bitsToℕ-cons-one (replicate {n = n} bit1)) ∙
  sym (ℕ.+-suc (2 ^ n) (bitsToℕ (replicate {n = n} bit1))) ∙
  cong ((2 ^ n) +_) (allOnes-suc-bitsToℕ {n}) ∙
  sym (pow2-suc-expand n)

allOnes→suc-bitsToℕ≡2^n :
  ∀ {n} →
  (bits : BitVec n) →
  Bool→Type (allOnes bits) →
  suc (bitsToℕ bits) ≡ 2 ^ n
allOnes→suc-bitsToℕ≡2^n [] _ = refl
allOnes→suc-bitsToℕ≡2^n {suc n} (true ∷ bits) proof =
  cong suc (bitsToℕ-cons-one bits) ∙
  sym (ℕ.+-suc (2 ^ n) (bitsToℕ bits)) ∙
  cong ((2 ^ n) +_) (allOnes→suc-bitsToℕ≡2^n bits proof) ∙
  sym (pow2-suc-expand n)
allOnes→suc-bitsToℕ≡2^n (false ∷ bits) ()

notAllOnes→below-reserved :
  ∀ {n} →
  (bits : BitVec n) →
  Bool→Type (not (allOnes bits)) →
  suc (bitsToℕ bits) ℕOrder.< 2 ^ n
notAllOnes→below-reserved [] ()
notAllOnes→below-reserved {suc n} (false ∷ bits) _ =
  ℕOrder.≤<-trans
    (bitsToℕ-bound bits)
    (pow2-strictly-increases n)
notAllOnes→below-reserved {suc n} (true ∷ bits) proof =
  subst
    (suc (bitsToℕ (true ∷ bits)) ℕOrder.<_)
    (sym (pow2-suc-expand n))
    (subst
      (λ value → value ℕOrder.< ((2 ^ n) + (2 ^ n)))
      (sym
        (cong suc (bitsToℕ-cons-one bits) ∙
         sym (ℕ.+-suc (2 ^ n) (bitsToℕ bits))))
      (ℕOrder.<-k+
        {m = suc (bitsToℕ bits)}
        {n = 2 ^ n}
        {k = 2 ^ n}
        (notAllOnes→below-reserved bits proof)))

suc-bitsToℕ≡2^n→allOnes :
  ∀ {n} →
  (bits : BitVec n) →
  suc (bitsToℕ bits) ≡ 2 ^ n →
  allOnes bits ≡ true
suc-bitsToℕ≡2^n→allOnes {n} bits bits≡max with allOnes bits UsingEq
... | true , allOnes≡true = allOnes≡true
... | false , allOnes≡false =
  ⊥.rec
    (ℕOrder.¬m<m
      (subst
        (λ value → value ℕOrder.< 2 ^ n)
        bits≡max
        (notAllOnes→below-reserved
          bits
          (subst Bool→Type (sym (cong not allOnes≡false)) tt))))

below-reserved→allOnes≡false :
  ∀ {n} →
  (bits : BitVec n) →
  suc (bitsToℕ bits) ℕOrder.< 2 ^ n →
  allOnes bits ≡ false
below-reserved→allOnes≡false {n} bits below with allOnes bits UsingEq
... | false , allOnes≡false = allOnes≡false
... | true , allOnes≡true =
  ⊥.rec
    (ℕOrder.¬m<m
      (subst
        (λ value → value ℕOrder.< 2 ^ n)
        (allOnes→suc-bitsToℕ≡2^n
          bits
          (subst Bool→Type (sym allOnes≡true) tt))
        below))

not-allZeros-and-allOnes :
  ∀ {n} →
  (bits : BitVec (suc n)) →
  Bool→Type (allZeros bits) →
  Bool→Type (allOnes bits) →
  ⊥.⊥
not-allZeros-and-allOnes (false ∷ bits) _ ()
not-allZeros-and-allOnes (true ∷ bits) () _

bitsToℕ≤allOnes :
  ∀ {n} →
  (bits : BitVec n) →
  bitsToℕ bits ℕOrder.≤ bitsToℕ (replicate {n = n} bit1)
bitsToℕ≤allOnes {n} bits =
  ℕOrder.pred-≤-pred
    (subst
      (suc (bitsToℕ bits) ℕOrder.≤_)
      (sym (allOnes-suc-bitsToℕ {n}))
      (bitsToℕ-bound bits))