IEEE754.Format

module IEEE754.Format where

open import IEEE754.Prelude
open import IEEE754.Sign

record BinaryInterchangeFormat : Type₀ where
  constructor binary-interchange-format
  field
    exponentBitsMinusOne : ℕ
    trailingSignificandBitsMinusOne : ℕ

exponentWidth : BinaryInterchangeFormat → ℕ
exponentWidth F = suc (BinaryInterchangeFormat.exponentBitsMinusOne F)

trailingSignificandBits : BinaryInterchangeFormat → ℕ
trailingSignificandBits F =
  suc (BinaryInterchangeFormat.trailingSignificandBitsMinusOne F)

precision : BinaryInterchangeFormat → ℕ
precision F = suc (trailingSignificandBits F)

storageWidth : BinaryInterchangeFormat → ℕ
storageWidth F = suc (exponentWidth F + trailingSignificandBits F)

record BinaryEncoding (F : BinaryInterchangeFormat) : Type₀ where
  constructor binary-encoding
  field
    sign : Sign
    exponent : BitVec (exponentWidth F)
    trailingSignificand : BitVec (trailingSignificandBits F)

binary16 binary32 binary64 binary128 : BinaryInterchangeFormat
binary16 = binary-interchange-format 4 9
binary32 = binary-interchange-format 7 22
binary64 = binary-interchange-format 10 51
binary128 = binary-interchange-format 14 111

binary16-width : storageWidth binary16 ≡ 16
binary16-width = refl

binary32-width : storageWidth binary32 ≡ 32
binary32-width = refl

binary64-width : storageWidth binary64 ≡ 64
binary64-width = refl

binary128-width : storageWidth binary128 ≡ 128
binary128-width = refl