module IEEE754.Rounding where

open import IEEE754.Prelude
open import IEEE754.Format

data RoundingDirection : Type₀ where
  roundTiesToEven : RoundingDirection
  roundTowardZero : RoundingDirection
  roundTowardPositive : RoundingDirection
  roundTowardNegative : RoundingDirection
  roundTiesToAway : RoundingDirection

data TininessDetection : Type₀ where
  tininessBeforeRounding : TininessDetection
  tininessAfterRounding : TininessDetection

record FloatingPointContext : Type₀ where
  constructor floating-point-context
  field
    format : BinaryInterchangeFormat
    rounding : RoundingDirection
    tininess : TininessDetection

defaultContext : BinaryInterchangeFormat → FloatingPointContext
defaultContext F =
  floating-point-context F roundTiesToEven tininessAfterRounding