module IEEE754.Exception where

open import IEEE754.Prelude

data Exception : Type₀ where
  invalidOperation : Exception
  divisionByZero : Exception
  overflow : Exception
  underflow : Exception
  inexact : Exception

sameException : Exception → Exception → Bool
sameException invalidOperation invalidOperation = true
sameException invalidOperation divisionByZero = false
sameException invalidOperation overflow = false
sameException invalidOperation underflow = false
sameException invalidOperation inexact = false
sameException divisionByZero invalidOperation = false
sameException divisionByZero divisionByZero = true
sameException divisionByZero overflow = false
sameException divisionByZero underflow = false
sameException divisionByZero inexact = false
sameException overflow invalidOperation = false
sameException overflow divisionByZero = false
sameException overflow overflow = true
sameException overflow underflow = false
sameException overflow inexact = false
sameException underflow invalidOperation = false
sameException underflow divisionByZero = false
sameException underflow overflow = false
sameException underflow underflow = true
sameException underflow inexact = false
sameException inexact invalidOperation = false
sameException inexact divisionByZero = false
sameException inexact overflow = false
sameException inexact underflow = false
sameException inexact inexact = true

Flags : Type₀
Flags = Exception → Bool

noFlags : Flags
noFlags _ = false

hasFlag : Exception → Flags → Bool
hasFlag exception flags = flags exception

raise : Exception → Flags → Flags
raise exception flags queried =
  sameException exception queried or flags queried

unionFlags : Flags → Flags → Flags
unionFlags left right exception =
  left exception or right exception

record Flagged {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor flagged
  field
    value : A
    flags : Flags

pureFlagged : ∀ {ℓ} {A : Type ℓ} → A → Flagged A
pureFlagged value = flagged value noFlags