IEEE754.Range

module IEEE754.Range where

open import IEEE754.Prelude
open import IEEE754.Sign
open import IEEE754.Format
open import IEEE754.BitVec
open import IEEE754.Exact
open import IEEE754.Representation
open import IEEE754.FiniteSpec
open import IEEE754.FiniteDecode
open import IEEE754.Representable
open import IEEE754.RationalOrder

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

leastPositiveBits : (n : ℕ) → BitVec (suc n)
leastPositiveBits zero = bit1 ∷ []
leastPositiveBits (suc n) = bit0 ∷ leastPositiveBits n

leastPositiveBits-value :
  (n : ℕ) →
  bitsToℕ (leastPositiveBits n) ≡ 1
leastPositiveBits-value zero = refl
leastPositiveBits-value (suc n) = leastPositiveBits-value n

leastPositiveBits-positive :
  (n : ℕ) →
  0 ℕOrder.< bitsToℕ (leastPositiveBits n)
leastPositiveBits-positive n =
  subst
    (0 ℕOrder.<_)
    (sym (leastPositiveBits-value n))
    (0 , refl)

leastPositiveBits-notAllOnes :
  (n : ℕ) →
  Bool→Type (not (allOnes (leastPositiveBits (suc n))))
leastPositiveBits-notAllOnes n = tt

leastPositiveBits-belowReserved :
  (n : ℕ) →
  suc (bitsToℕ (leastPositiveBits (suc n))) ℕOrder.<
  2 ^ suc (suc n)
leastPositiveBits-belowReserved n =
  notAllOnes→below-reserved
    (leastPositiveBits (suc n))
    (leastPositiveBits-notAllOnes n)

maxFiniteExponentBits : (n : ℕ) → BitVec (suc n)
maxFiniteExponentBits zero = bit0 ∷ []
maxFiniteExponentBits (suc n) = bit1 ∷ maxFiniteExponentBits n

maxFiniteExponentBits-notAllOnes :
  (n : ℕ) →
  Bool→Type (not (allOnes (maxFiniteExponentBits n)))
maxFiniteExponentBits-notAllOnes zero = tt
maxFiniteExponentBits-notAllOnes (suc n) =
  maxFiniteExponentBits-notAllOnes n

maxFiniteExponentBits-notAllZeros :
  (n : ℕ) →
  Bool→Type (not (allZeros (maxFiniteExponentBits (suc n))))
maxFiniteExponentBits-notAllZeros n = tt

maxFiniteExponentBits-positive :
  (n : ℕ) →
  0 ℕOrder.< bitsToℕ (maxFiniteExponentBits (suc n))
maxFiniteExponentBits-positive n =
  notAllZeros→positive
    (maxFiniteExponentBits (suc n))
    (maxFiniteExponentBits-notAllZeros n)

allOnesBits-notAllZeros :
  (n : ℕ) →
  Bool→Type (not (allZeros (replicate {n = suc n} bit1)))
allOnesBits-notAllZeros n = tt

allOnesBits-positive :
  (n : ℕ) →
  0 ℕOrder.< bitsToℕ (replicate {n = suc n} bit1)
allOnesBits-positive n =
  notAllZeros→positive
    (replicate {n = suc n} bit1)
    (allOnesBits-notAllZeros n)

maxFiniteExponentBits-belowReserved :
  (n : ℕ) →
  suc (bitsToℕ (maxFiniteExponentBits n)) ℕOrder.<
  2 ^ suc n
maxFiniteExponentBits-belowReserved n =
  notAllOnes→below-reserved
    (maxFiniteExponentBits n)
    (maxFiniteExponentBits-notAllOnes n)

record NondegenerateExponentRange
  (F : BinaryInterchangeFormat) : Type₀ where
  constructor nondegenerate-exponent-range
  field
    exponentTail : ℕ
    exponentBitsMinusOne≡suc :
      BinaryInterchangeFormat.exponentBitsMinusOne F ≡ suc exponentTail

binary16-nondegenerateExponentRange : NondegenerateExponentRange binary16
binary16-nondegenerateExponentRange = nondegenerate-exponent-range 3 refl

binary32-nondegenerateExponentRange : NondegenerateExponentRange binary32
binary32-nondegenerateExponentRange = nondegenerate-exponent-range 6 refl

binary64-nondegenerateExponentRange : NondegenerateExponentRange binary64
binary64-nondegenerateExponentRange = nondegenerate-exponent-range 9 refl

binary128-nondegenerateExponentRange : NondegenerateExponentRange binary128
binary128-nondegenerateExponentRange = nondegenerate-exponent-range 13 refl

record FiniteRangeFormat (F : BinaryInterchangeFormat) : Type₀ where
  constructor finite-range-format
  field
    positiveBias : PositiveExponentBias F
    nondegenerateExponentRange : NondegenerateExponentRange F

binary16-finiteRangeFormat : FiniteRangeFormat binary16
binary16-finiteRangeFormat =
  finite-range-format
    binary16-positiveExponentBias
    binary16-nondegenerateExponentRange

binary32-finiteRangeFormat : FiniteRangeFormat binary32
binary32-finiteRangeFormat =
  finite-range-format
    binary32-positiveExponentBias
    binary32-nondegenerateExponentRange

binary64-finiteRangeFormat : FiniteRangeFormat binary64
binary64-finiteRangeFormat =
  finite-range-format
    binary64-positiveExponentBias
    binary64-nondegenerateExponentRange

binary128-finiteRangeFormat : FiniteRangeFormat binary128
binary128-finiteRangeFormat =
  finite-range-format
    binary128-positiveExponentBias
    binary128-nondegenerateExponentRange

leastSubnormalTrailing :
  (F : BinaryInterchangeFormat) →
  BitVec (trailingSignificandBits F)
leastSubnormalTrailing F =
  leastPositiveBits
    (BinaryInterchangeFormat.trailingSignificandBitsMinusOne F)

zeroTrailing :
  (F : BinaryInterchangeFormat) →
  BitVec (trailingSignificandBits F)
zeroTrailing F = replicate {n = trailingSignificandBits F} bit0

maxTrailing :
  (F : BinaryInterchangeFormat) →
  BitVec (trailingSignificandBits F)
maxTrailing F = replicate {n = trailingSignificandBits F} bit1

leastNormalExponent :
  (F : BinaryInterchangeFormat) →
  BitVec (exponentWidth F)
leastNormalExponent F =
  leastPositiveBits
    (BinaryInterchangeFormat.exponentBitsMinusOne F)

maxFiniteExponent :
  (F : BinaryInterchangeFormat) →
  BitVec (exponentWidth F)
maxFiniteExponent F =
  maxFiniteExponentBits
    (BinaryInterchangeFormat.exponentBitsMinusOne F)

maxFiniteExponentField : BinaryInterchangeFormat → ℕ
maxFiniteExponentField F = bitsToℕ (maxFiniteExponent F)

emax : BinaryInterchangeFormat → ℤ.ℤ
emax F = unbiasedExponent F (maxFiniteExponent F)

minPositiveSubnormalMagnitude :
  BinaryInterchangeFormat →
  ℚ.ℚ
minPositiveSubnormalMagnitude F =
  subnormalProductMagnitude {F = F} (leastSubnormalTrailing F)

maxSubnormalMagnitude :
  BinaryInterchangeFormat →
  ℚ.ℚ
maxSubnormalMagnitude F =
  subnormalProductMagnitude {F = F} (maxTrailing F)

minPositiveNormalMagnitude :
  BinaryInterchangeFormat →
  ℚ.ℚ
minPositiveNormalMagnitude F =
  normalProductMagnitude
    {F = F}
    (leastNormalExponent F)
    (zeroTrailing F)

maxFiniteMagnitude :
  BinaryInterchangeFormat →
  ℚ.ℚ
maxFiniteMagnitude F =
  normalProductMagnitude
    {F = F}
    (maxFiniteExponent F)
    (maxTrailing F)

minNormal-unbiasedExponent≡emin :
  (F : BinaryInterchangeFormat) →
  unbiasedExponent F (leastNormalExponent F) ≡ emin F
minNormal-unbiasedExponent≡emin F =
  cong
    (λ n → ℤ._ℕ-_ n (exponentBias F))
    (leastPositiveBits-value
      (BinaryInterchangeFormat.exponentBitsMinusOne F))

minPositiveSubnormalMagnitude-textbook :
  (F : BinaryInterchangeFormat) →
  minPositiveSubnormalMagnitude F ≡
  trailingFraction {F = F} (leastSubnormalTrailing F) ℚ.·
  pow2ℚ (emin F)
minPositiveSubnormalMagnitude-textbook F = refl

maxSubnormalMagnitude-textbook :
  (F : BinaryInterchangeFormat) →
  maxSubnormalMagnitude F ≡
  trailingFraction {F = F} (maxTrailing F) ℚ.·
  pow2ℚ (emin F)
maxSubnormalMagnitude-textbook F = refl

minPositiveNormalMagnitude-textbook :
  (F : BinaryInterchangeFormat) →
  minPositiveNormalMagnitude F ≡
  normalCoefficient {F = F} (zeroTrailing F) ℚ.·
  pow2ℚ (emin F)
minPositiveNormalMagnitude-textbook F =
  cong
    (λ exponent →
      normalCoefficient {F = F} (zeroTrailing F) ℚ.·
      pow2ℚ exponent)
    (minNormal-unbiasedExponent≡emin F)

maxFiniteMagnitude-textbook :
  (F : BinaryInterchangeFormat) →
  maxFiniteMagnitude F ≡
  normalCoefficient {F = F} (maxTrailing F) ℚ.·
  pow2ℚ (emax F)
maxFiniteMagnitude-textbook F = refl

subnormalProductMagnitude-nonnegative :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (trailing : BitVec (trailingSignificandBits F)) →
  rationalZero ≤ℚ subnormalProductMagnitude {F = F} trailing
subnormalProductMagnitude-nonnegative {F} bias trailing =
  subst
    (λ magnitude → rationalZero ≤ℚ magnitude)
    (subnormalMagnitude-textbook-product bias trailing)
    (scaleNatByPowerOfTwo-nonnegative
      (bitsToℕ trailing)
      (subnormalShift F))

normalProductMagnitude-nonnegative :
  ∀ {F} →
  (exponent : BitVec (exponentWidth F)) →
  (trailing : BitVec (trailingSignificandBits F)) →
  rationalZero ≤ℚ normalProductMagnitude {F = F} exponent trailing
normalProductMagnitude-nonnegative {F} exponent trailing =
  subst
    (λ magnitude → rationalZero ≤ℚ magnitude)
    (normalMagnitude-textbook-product exponent trailing)
    (scaleNatByPowerOfTwo-nonnegative
      (normalSignificand {F = F} trailing)
      (normalShift F exponent))

normalSignificand≤maxTrailing :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  normalSignificand {F = F} trailing ℕOrder.≤
  normalSignificand {F = F} (maxTrailing F)
normalSignificand≤maxTrailing {F} trailing =
  ℕOrder.≤-k+
    {m = bitsToℕ trailing}
    {n = bitsToℕ (maxTrailing F)}
    {k = 2 ^ trailingSignificandBits F}
    (bitsToℕ≤allOnes trailing)

subnormalProductMagnitude≤maxSubnormalMagnitude :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (trailing : BitVec (trailingSignificandBits F)) →
  subnormalProductMagnitude {F = F} trailing ≤ℚ
  maxSubnormalMagnitude F
subnormalProductMagnitude≤maxSubnormalMagnitude {F} bias trailing =
  subst2
    _≤ℚ_
    (subnormalMagnitude-textbook-product bias trailing)
    (subnormalMagnitude-textbook-product bias (maxTrailing F))
    (scaleNatByPowerOfTwo-monotone
      (bitsToℕ trailing)
      (bitsToℕ (maxTrailing F))
      (subnormalShift F)
      (bitsToℕ≤allOnes trailing))

normalProductMagnitude≤sameExponentMaxTrailing :
  ∀ {F} →
  (exponent : BitVec (exponentWidth F)) →
  (trailing : BitVec (trailingSignificandBits F)) →
  normalProductMagnitude {F = F} exponent trailing ≤ℚ
  normalProductMagnitude {F = F} exponent (maxTrailing F)
normalProductMagnitude≤sameExponentMaxTrailing {F} exponent trailing =
  subst2
    _≤ℚ_
    (normalMagnitude-textbook-product exponent trailing)
    (normalMagnitude-textbook-product exponent (maxTrailing F))
    (scaleNatByPowerOfTwo-monotone
      (normalSignificand {F = F} trailing)
      (normalSignificand {F = F} (maxTrailing F))
      (normalShift F exponent)
      (normalSignificand≤maxTrailing {F = F} trailing))

minPositiveSubnormalMagnitude≤maxSubnormalMagnitude :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  minPositiveSubnormalMagnitude F ≤ℚ
  maxSubnormalMagnitude F
minPositiveSubnormalMagnitude≤maxSubnormalMagnitude {F} bias =
  subnormalProductMagnitude≤maxSubnormalMagnitude
    bias
    (leastSubnormalTrailing F)

minPositiveSubnormalMagnitude≤subnormalProductMagnitude :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (trailing : BitVec (trailingSignificandBits F)) →
  0 ℕOrder.< bitsToℕ trailing →
  minPositiveSubnormalMagnitude F ≤ℚ
  subnormalProductMagnitude {F = F} trailing
minPositiveSubnormalMagnitude≤subnormalProductMagnitude {F} bias trailing trailing>0 =
  subst2
    _≤ℚ_
    (subnormalMagnitude-textbook-product bias (leastSubnormalTrailing F))
    (subnormalMagnitude-textbook-product bias trailing)
    (scaleNatByPowerOfTwo-monotone
      (bitsToℕ (leastSubnormalTrailing F))
      (bitsToℕ trailing)
      (subnormalShift F)
      (subst
        (λ coefficient → coefficient ℕOrder.≤ bitsToℕ trailing)
        (sym
          (leastPositiveBits-value
            (BinaryInterchangeFormat.trailingSignificandBitsMinusOne F)))
        trailing>0))

subnormalProductMagnitude-positiveInterval :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (trailing : BitVec (trailingSignificandBits F)) →
  0 ℕOrder.< bitsToℕ trailing →
  ℚInterval
    (minPositiveSubnormalMagnitude F)
    (maxSubnormalMagnitude F)
    (subnormalProductMagnitude {F = F} trailing)
subnormalProductMagnitude-positiveInterval bias trailing trailing>0 =
  in-ℚ-interval
    (minPositiveSubnormalMagnitude≤subnormalProductMagnitude
      bias
      trailing
      trailing>0)
    (subnormalProductMagnitude≤maxSubnormalMagnitude bias trailing)

maxTrailing≤zeroNormalSignificand :
  ∀ {F} →
  bitsToℕ (maxTrailing F) ℕOrder.≤
  normalSignificand {F = F} (zeroTrailing F)
maxTrailing≤zeroNormalSignificand {F} =
  ℕOrder.≤-trans
    (ℕOrder.<-weaken (bitsToℕ-bound (maxTrailing F)))
    (ℕOrder.≤SumLeft
      {n = 2 ^ trailingSignificandBits F}
      {k = bitsToℕ (zeroTrailing F)})

trailingFraction≤zeroNormalCoefficient :
  ∀ {F} →
  trailingFraction {F = F} (maxTrailing F) ≤ℚ
  normalCoefficient {F = F} (zeroTrailing F)
trailingFraction≤zeroNormalCoefficient {F} =
  subst2
    _≤ℚ_
    (sym (trailingFraction-canonical {F = F} (maxTrailing F)))
    (sym (normalCoefficient-canonical {F = F} (zeroTrailing F)))
    (scaleNatByPowerOfTwo-monotone
      (fractionNumerator {F = F} (maxTrailing F))
      (normalNumerator {F = F} (zeroTrailing F))
      (fractionShift F)
      (maxTrailing≤zeroNormalSignificand {F = F}))

maxSubnormalMagnitude≤minPositiveNormalMagnitude :
  (F : BinaryInterchangeFormat) →
  maxSubnormalMagnitude F ≤ℚ
  minPositiveNormalMagnitude F
maxSubnormalMagnitude≤minPositiveNormalMagnitude F =
  ≤ℚ-subst-right
    {left = maxSubnormalMagnitude F}
    {middle =
      normalCoefficient {F = F} (zeroTrailing F) ℚ.·
      pow2ℚ (emin F)}
    {right = minPositiveNormalMagnitude F}
    (sym (minPositiveNormalMagnitude-textbook F))
    (≤ℚ-mul-right-nonnegative
      (trailingFraction {F = F} (maxTrailing F))
      (normalCoefficient {F = F} (zeroTrailing F))
      (pow2ℚ (emin F))
      (pow2ℚ-nonnegative (emin F))
      (trailingFraction≤zeroNormalCoefficient {F = F}))

minPositiveSubnormalMagnitude≤minPositiveNormalMagnitude :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  minPositiveSubnormalMagnitude F ≤ℚ
  minPositiveNormalMagnitude F
minPositiveSubnormalMagnitude≤minPositiveNormalMagnitude {F} bias =
  ≤ℚ-trans
    (minPositiveSubnormalMagnitude F)
    (maxSubnormalMagnitude F)
    (minPositiveNormalMagnitude F)
    (minPositiveSubnormalMagnitude≤maxSubnormalMagnitude bias)
    (maxSubnormalMagnitude≤minPositiveNormalMagnitude F)

subnormalProductMagnitude≤minPositiveNormalMagnitude :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (trailing : BitVec (trailingSignificandBits F)) →
  subnormalProductMagnitude {F = F} trailing ≤ℚ
  minPositiveNormalMagnitude F
subnormalProductMagnitude≤minPositiveNormalMagnitude {F} bias trailing =
  ≤ℚ-trans
    (subnormalProductMagnitude {F = F} trailing)
    (maxSubnormalMagnitude F)
    (minPositiveNormalMagnitude F)
    (subnormalProductMagnitude≤maxSubnormalMagnitude bias trailing)
    (maxSubnormalMagnitude≤minPositiveNormalMagnitude F)

finiteTextbookMagnitude-nonnegative :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  {magnitude : ℚ.ℚ} →
  FiniteTextbookMagnitude bias magnitude →
  rationalZero ≤ℚ magnitude
finiteTextbookMagnitude-nonnegative bias representable-zero =
  zeroMagnitude-nonnegative
finiteTextbookMagnitude-nonnegative {F} bias
  (representable-subnormal trailing trailing>0) =
  subnormalProductMagnitude-nonnegative bias trailing
finiteTextbookMagnitude-nonnegative {F} bias
  (representable-normal exponent trailing exponent>0 exponent<max interval) =
  normalProductMagnitude-nonnegative exponent trailing

leastNormalExponent-positive :
  ∀ {F} →
  NondegenerateExponentRange F →
  0 ℕOrder.< bitsToℕ (leastNormalExponent F)
leastNormalExponent-positive {F} range =
  subst
    (λ n → 0 ℕOrder.< bitsToℕ (leastPositiveBits n))
    (sym (NondegenerateExponentRange.exponentBitsMinusOne≡suc range))
    (leastPositiveBits-positive
      (suc (NondegenerateExponentRange.exponentTail range)))

leastNormalExponent-belowReserved :
  ∀ {F} →
  NondegenerateExponentRange F →
  suc (bitsToℕ (leastNormalExponent F)) ℕOrder.<
  2 ^ exponentWidth F
leastNormalExponent-belowReserved {F} range =
  subst
    (λ n →
      suc (bitsToℕ (leastPositiveBits n)) ℕOrder.<
      2 ^ suc n)
    (sym (NondegenerateExponentRange.exponentBitsMinusOne≡suc range))
    (leastPositiveBits-belowReserved
      (NondegenerateExponentRange.exponentTail range))

maxFiniteExponent-positive :
  ∀ {F} →
  NondegenerateExponentRange F →
  0 ℕOrder.< bitsToℕ (maxFiniteExponent F)
maxFiniteExponent-positive {F} range =
  subst
    (λ n → 0 ℕOrder.< bitsToℕ (maxFiniteExponentBits n))
    (sym (NondegenerateExponentRange.exponentBitsMinusOne≡suc range))
    (maxFiniteExponentBits-positive
      (NondegenerateExponentRange.exponentTail range))

maxFiniteExponent-belowReserved :
  (F : BinaryInterchangeFormat) →
  suc (bitsToℕ (maxFiniteExponent F)) ℕOrder.<
  2 ^ exponentWidth F
maxFiniteExponent-belowReserved F =
  maxFiniteExponentBits-belowReserved
    (BinaryInterchangeFormat.exponentBitsMinusOne F)

minPositiveSubnormal-representable :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  FiniteTextbookMagnitude bias (minPositiveSubnormalMagnitude F)
minPositiveSubnormal-representable {F} bias =
  representable-subnormal
    (leastSubnormalTrailing F)
    (leastPositiveBits-positive
      (BinaryInterchangeFormat.trailingSignificandBitsMinusOne F))

maxSubnormalMagnitude-representable :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  FiniteTextbookMagnitude bias (maxSubnormalMagnitude F)
maxSubnormalMagnitude-representable {F} bias =
  representable-subnormal
    (maxTrailing F)
    (allOnesBits-positive
      (BinaryInterchangeFormat.trailingSignificandBitsMinusOne F))

minPositiveNormal-representable :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (range : NondegenerateExponentRange F) →
  FiniteTextbookMagnitude bias (minPositiveNormalMagnitude F)
minPositiveNormal-representable {F} bias range =
  representable-normal
    (leastNormalExponent F)
    (zeroTrailing F)
    (leastNormalExponent-positive range)
    (leastNormalExponent-belowReserved range)
    (normalSignificand-invariant {F = F} (zeroTrailing F))

maxFiniteMagnitude-representable :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (range : NondegenerateExponentRange F) →
  FiniteTextbookMagnitude bias (maxFiniteMagnitude F)
maxFiniteMagnitude-representable {F} bias range =
  representable-normal
    (maxFiniteExponent F)
    (maxTrailing F)
    (maxFiniteExponent-positive range)
    (maxFiniteExponent-belowReserved F)
    (normalSignificand-invariant {F = F} (maxTrailing F))

minPositiveNormal-finiteRange-representable :
  ∀ {F} →
  (range : FiniteRangeFormat F) →
  FiniteTextbookMagnitude
    (FiniteRangeFormat.positiveBias range)
    (minPositiveNormalMagnitude F)
minPositiveNormal-finiteRange-representable range =
  minPositiveNormal-representable
    (FiniteRangeFormat.positiveBias range)
    (FiniteRangeFormat.nondegenerateExponentRange range)

maxFiniteMagnitude-finiteRange-representable :
  ∀ {F} →
  (range : FiniteRangeFormat F) →
  FiniteTextbookMagnitude
    (FiniteRangeFormat.positiveBias range)
    (maxFiniteMagnitude F)
maxFiniteMagnitude-finiteRange-representable range =
  maxFiniteMagnitude-representable
    (FiniteRangeFormat.positiveBias range)
    (FiniteRangeFormat.nondegenerateExponentRange range)