module IEEE754.Classification where

open import IEEE754.Prelude
open import IEEE754.Sign
open import IEEE754.Format

data ExponentClass : Type₀ where
  all-zero-exponent : ExponentClass
  finite-exponent : ExponentClass
  all-one-exponent : ExponentClass

classifyExponent : ∀ {n} → BitVec (suc n) → ExponentClass
classifyExponent bits with allZeros bits UsingEq | allOnes bits UsingEq
... | true , _ | _ = all-zero-exponent
... | false , _ | true , _ = all-one-exponent
... | false , _ | false , _ = finite-exponent

data NaNKind : Type₀ where
  signalingNaN : NaNKind
  quietNaN : NaNKind

data BinaryClass : Type₀ where
  zero-class : BinaryClass
  subnormal-class : BinaryClass
  normal-class : BinaryClass
  infinity-class : BinaryClass
  nan-class : BinaryClass

nanKindFromQuietBit : Bit → NaNKind
nanKindFromQuietBit false = signalingNaN
nanKindFromQuietBit true = quietNaN

nanKind : ∀ {F} → BinaryEncoding F → NaNKind
nanKind encoding =
  nanKindFromQuietBit
    (head (BinaryEncoding.trailingSignificand encoding))

classifyBinary : ∀ {F} → BinaryEncoding F → BinaryClass
classifyBinary encoding
  with allZeros (BinaryEncoding.exponent encoding) UsingEq
     | allOnes (BinaryEncoding.exponent encoding) UsingEq
     | allZeros (BinaryEncoding.trailingSignificand encoding) UsingEq
... | true , _ | _ | true , _ = zero-class
... | true , _ | _ | false , _ = subnormal-class
... | false , _ | true , _ | true , _ = infinity-class
... | false , _ | true , _ | false , _ = nan-class
... | false , _ | false , _ | _ = normal-class

isFiniteClass : BinaryClass → Bool
isFiniteClass zero-class = true
isFiniteClass subnormal-class = true
isFiniteClass normal-class = true
isFiniteClass infinity-class = false
isFiniteClass nan-class = false

isNaNClass : BinaryClass → Bool
isNaNClass zero-class = false
isNaNClass subnormal-class = false
isNaNClass normal-class = false
isNaNClass infinity-class = false
isNaNClass nan-class = true