module IEEE754.RoundingSpec where

open import IEEE754.Prelude
open import IEEE754.Sign
open import IEEE754.Format
open import IEEE754.Rounding
open import IEEE754.Exception
open import IEEE754.Semantics
open import IEEE754.Exact
open import IEEE754.FiniteSpec
open import IEEE754.FiniteDecode
open import IEEE754.Representable
open import IEEE754.SignedValue
open import IEEE754.RationalOrder

import Cubical.Data.Empty as ⊥
import Cubical.Data.Rationals as ℚ

record ExactRationalInput
  (F : BinaryInterchangeFormat) : Type₀ where
  constructor exact-rational-input
  field
    rounding : RoundingDirection
    tininess : TininessDetection
    exactValue : ℚ.ℚ

contextInput :
  (context : FloatingPointContext) →
  ℚ.ℚ →
  ExactRationalInput (FloatingPointContext.format context)
contextInput context exact =
  exact-rational-input
    (FloatingPointContext.rounding context)
    (FloatingPointContext.tininess context)
    exact

record FiniteCandidateEncoding {F : BinaryInterchangeFormat}
  (bias : PositiveExponentBias F) : Type₀ where
  constructor finite-candidate-encoding
  field
    encoding : BinaryEncoding F
    sign : Sign
    magnitude : ℚ.ℚ
    finiteSpec :
      TextbookDecodedValueSpec
        bias
        encoding
        (finiteValue sign magnitude)

finiteCandidateValue :
  ∀ {F} →
  {bias : PositiveExponentBias F} →
  FiniteCandidateEncoding bias →
  ℚ.ℚ
finiteCandidateValue candidate =
  signedMagnitude
    (FiniteCandidateEncoding.sign candidate)
    (FiniteCandidateEncoding.magnitude candidate)

finiteCandidateRepresentable :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (candidate : FiniteCandidateEncoding bias) →
  FiniteTextbookMagnitude
    bias
    (FiniteCandidateEncoding.magnitude candidate)
finiteCandidateRepresentable bias candidate =
  textbookFiniteValue→representableMagnitude
    bias
    (FiniteCandidateEncoding.finiteSpec candidate)

finiteCandidateSignedRational :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (candidate : FiniteCandidateEncoding bias) →
  SignedRationalValue
    (decodeValue (FiniteCandidateEncoding.encoding candidate))
    (finiteCandidateValue candidate)
finiteCandidateSignedRational bias candidate =
  textbookFiniteValue→signedRational
    bias
    {encoding = FiniteCandidateEncoding.encoding candidate}
    {sign = FiniteCandidateEncoding.sign candidate}
    {magnitude = FiniteCandidateEncoding.magnitude candidate}
    (FiniteCandidateEncoding.finiteSpec candidate)

finiteCandidateDecodes :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (candidate : FiniteCandidateEncoding bias) →
  decodeValue (FiniteCandidateEncoding.encoding candidate) ≡
  finiteValue
    (FiniteCandidateEncoding.sign candidate)
    (FiniteCandidateEncoding.magnitude candidate)
finiteCandidateDecodes bias candidate =
  sym
    (textbookDecodedValueSpec-complete
      bias
      (FiniteCandidateEncoding.finiteSpec candidate))

record InfinityCandidateEncoding {F : BinaryInterchangeFormat}
  (bias : PositiveExponentBias F) : Type₀ where
  constructor infinity-candidate-encoding
  field
    encoding : BinaryEncoding F
    sign : Sign
    infinitySpec :
      TextbookDecodedValueSpec
        bias
        encoding
        (infinityValue sign)

infinityCandidateDecodes :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (candidate : InfinityCandidateEncoding bias) →
  decodeValue (InfinityCandidateEncoding.encoding candidate) ≡
  infinityValue (InfinityCandidateEncoding.sign candidate)
infinityCandidateDecodes bias candidate =
  sym
    (textbookDecodedValueSpec-complete
      bias
      (InfinityCandidateEncoding.infinitySpec candidate))

data CandidateEncoding {F : BinaryInterchangeFormat}
  (bias : PositiveExponentBias F) : Type₀ where
  finite-candidate :
    FiniteCandidateEncoding bias →
    CandidateEncoding bias
  infinity-candidate :
    InfinityCandidateEncoding bias →
    CandidateEncoding bias

candidateEncoding :
  ∀ {F} →
  {bias : PositiveExponentBias F} →
  CandidateEncoding bias →
  BinaryEncoding F
candidateEncoding (finite-candidate candidate) =
  FiniteCandidateEncoding.encoding candidate
candidateEncoding (infinity-candidate candidate) =
  InfinityCandidateEncoding.encoding candidate

record FiniteLowerSelection {F : BinaryInterchangeFormat}
  (bias : PositiveExponentBias F)
  (exact : ℚ.ℚ)
  (candidate : FiniteCandidateEncoding bias) : Type₀ where
  constructor finite-lower-selection
  field
    candidate≤exact : finiteCandidateValue candidate ≤ℚ exact
    greatestFiniteBelow :
      (other : FiniteCandidateEncoding bias) →
      finiteCandidateValue other ≤ℚ exact →
      finiteCandidateValue other ≤ℚ finiteCandidateValue candidate

record FiniteUpperSelection {F : BinaryInterchangeFormat}
  (bias : PositiveExponentBias F)
  (exact : ℚ.ℚ)
  (candidate : FiniteCandidateEncoding bias) : Type₀ where
  constructor finite-upper-selection
  field
    exact≤candidate : exact ≤ℚ finiteCandidateValue candidate
    leastFiniteAbove :
      (other : FiniteCandidateEncoding bias) →
      exact ≤ℚ finiteCandidateValue other →
      finiteCandidateValue candidate ≤ℚ finiteCandidateValue other

record RoundingMetric : Type₁ where
  constructor rounding-metric
  field
    noFartherThan :
      (exact selected other : ℚ.ℚ) →
      Type₀
    strictlyFartherThan :
      (exact selected other : ℚ.ℚ) →
      Type₀

record NearestEvenSelection {F : BinaryInterchangeFormat}
  (metric : RoundingMetric)
  (bias : PositiveExponentBias F)
  (exact : ℚ.ℚ)
  (candidate : FiniteCandidateEncoding bias) : Type₀ where
  constructor nearest-even-selection
  field
    nearest :
      (other : FiniteCandidateEncoding bias) →
      RoundingMetric.noFartherThan
        metric
        exact
        (finiteCandidateValue candidate)
        (finiteCandidateValue other)
    evenTieBreak :
      (other : FiniteCandidateEncoding bias) →
      RoundingMetric.noFartherThan
        metric
        exact
        (finiteCandidateValue other)
        (finiteCandidateValue candidate) →
      RoundingMetric.noFartherThan
        metric
        exact
        (finiteCandidateValue candidate)
        (finiteCandidateValue other)

record NearestAwaySelection {F : BinaryInterchangeFormat}
  (metric : RoundingMetric)
  (bias : PositiveExponentBias F)
  (exact : ℚ.ℚ)
  (candidate : FiniteCandidateEncoding bias) : Type₀ where
  constructor nearest-away-selection
  field
    nearest :
      (other : FiniteCandidateEncoding bias) →
      RoundingMetric.noFartherThan
        metric
        exact
        (finiteCandidateValue candidate)
        (finiteCandidateValue other)
    awayTieBreak :
      (other : FiniteCandidateEncoding bias) →
      RoundingMetric.noFartherThan
        metric
        exact
        (finiteCandidateValue other)
        (finiteCandidateValue candidate) →
      RoundingMetric.noFartherThan
        metric
        exact
        (finiteCandidateValue candidate)
        (finiteCandidateValue other)

data TowardZeroSelection {F : BinaryInterchangeFormat}
  (bias : PositiveExponentBias F)
  (exact : ℚ.ℚ)
  (candidate : FiniteCandidateEncoding bias) : Type₀ where
  toward-zero-nonnegative :
    rationalZero ≤ℚ exact →
    rationalZero ≤ℚ finiteCandidateValue candidate →
    FiniteLowerSelection bias exact candidate →
    TowardZeroSelection bias exact candidate
  toward-zero-negative :
    exact ≤ℚ rationalZero →
    finiteCandidateValue candidate ≤ℚ rationalZero →
    FiniteUpperSelection bias exact candidate →
    TowardZeroSelection bias exact candidate

data FiniteSelection {F : BinaryInterchangeFormat}
  (metric : RoundingMetric)
  (bias : PositiveExponentBias F) :
  RoundingDirection →
  ℚ.ℚ →
  FiniteCandidateEncoding bias →
  Type₀ where
  finite-exact-selection :
    ∀ {direction exact candidate} →
    finiteCandidateValue candidate ≡ exact →
    FiniteSelection metric bias direction exact candidate
  finite-ties-to-even-selection :
    ∀ {exact candidate} →
    NearestEvenSelection metric bias exact candidate →
    FiniteSelection metric bias roundTiesToEven exact candidate
  finite-toward-zero-selection :
    ∀ {exact candidate} →
    TowardZeroSelection bias exact candidate →
    FiniteSelection metric bias roundTowardZero exact candidate
  finite-toward-positive-selection :
    ∀ {exact candidate} →
    FiniteUpperSelection bias exact candidate →
    FiniteSelection metric bias roundTowardPositive exact candidate
  finite-toward-negative-selection :
    ∀ {exact candidate} →
    FiniteLowerSelection bias exact candidate →
    FiniteSelection metric bias roundTowardNegative exact candidate
  finite-ties-to-away-selection :
    ∀ {exact candidate} →
    NearestAwaySelection metric bias exact candidate →
    FiniteSelection metric bias roundTiesToAway exact candidate

record InfinitySelection {F : BinaryInterchangeFormat}
  (bias : PositiveExponentBias F)
  (direction : RoundingDirection)
  (exact : ℚ.ℚ)
  (candidate : InfinityCandidateEncoding bias) : Type₀ where
  constructor infinity-selection
  field
    overflowed : Unit

data RoundingSelection {F : BinaryInterchangeFormat}
  (metric : RoundingMetric)
  (bias : PositiveExponentBias F) :
  RoundingDirection →
  ℚ.ℚ →
  CandidateEncoding bias →
  Type₀ where
  finite-rounding-selection :
    ∀ {direction exact} →
    (candidate : FiniteCandidateEncoding bias) →
    FiniteSelection metric bias direction exact candidate →
    RoundingSelection
      metric
      bias
      direction
      exact
      (finite-candidate candidate)
  infinity-rounding-selection :
    ∀ {direction exact} →
    (candidate : InfinityCandidateEncoding bias) →
    InfinitySelection bias direction exact candidate →
    RoundingSelection
      metric
      bias
      direction
      exact
      (infinity-candidate candidate)

data ExactnessClass : Type₀ where
  exact-result : ExactnessClass
  inexact-result : ExactnessClass

data OutcomeExactness {F : BinaryInterchangeFormat}
  {bias : PositiveExponentBias F}
  (exact : ℚ.ℚ) :
  CandidateEncoding bias →
  Type₀ where
  exact-finite-outcome :
    (candidate : FiniteCandidateEncoding bias) →
    finiteCandidateValue candidate ≡ exact →
    OutcomeExactness exact (finite-candidate candidate)
  inexact-finite-outcome :
    (candidate : FiniteCandidateEncoding bias) →
    (finiteCandidateValue candidate ≡ exact → ⊥.⊥) →
    OutcomeExactness exact (finite-candidate candidate)
  inexact-infinity-outcome :
    (candidate : InfinityCandidateEncoding bias) →
    OutcomeExactness exact (infinity-candidate candidate)

exactnessClass :
  ∀ {F} →
  {bias : PositiveExponentBias F} →
  {exact : ℚ.ℚ} →
  {candidate : CandidateEncoding bias} →
  OutcomeExactness exact candidate →
  ExactnessClass
exactnessClass (exact-finite-outcome _ _) = exact-result
exactnessClass (inexact-finite-outcome _ _) = inexact-result
exactnessClass (inexact-infinity-outcome _) = inexact-result

data TininessStatus : Type₀ where
  not-tiny : TininessStatus
  tiny : TininessStatus

data OverflowStatus : Type₀ where
  not-overflowed : OverflowStatus
  overflowed : OverflowStatus

raiseIf : Bool → Exception → Flags → Flags
raiseIf true exception flags = raise exception flags
raiseIf false exception flags = flags

exactnessFlags : ExactnessClass → Flags
exactnessFlags exact-result = noFlags
exactnessFlags inexact-result = raise inexact noFlags

tininessBool : TininessStatus → Bool
tininessBool not-tiny = false
tininessBool tiny = true

overflowBool : OverflowStatus → Bool
overflowBool not-overflowed = false
overflowBool overflowed = true

roundingFlags :
  ExactnessClass →
  TininessStatus →
  OverflowStatus →
  Flags
roundingFlags exactness tininess overflowStatus =
  raiseIf
    (tininessBool tininess)
    underflow
    (raiseIf
      (overflowBool overflowStatus)
      overflow
      (exactnessFlags exactness))

record RoundingOutcome {F : BinaryInterchangeFormat}
  (metric : RoundingMetric)
  (bias : PositiveExponentBias F)
  (input : ExactRationalInput F) : Type₀ where
  constructor rounding-outcome
  field
    candidate : CandidateEncoding bias
    selection :
      RoundingSelection
        metric
        bias
        (ExactRationalInput.rounding input)
        (ExactRationalInput.exactValue input)
        candidate
    exactness :
      OutcomeExactness
        (ExactRationalInput.exactValue input)
        candidate
    tininess : TininessStatus
    overflowStatus : OverflowStatus

roundingOutcomeFlags :
  ∀ {F} →
  {metric : RoundingMetric} →
  {bias : PositiveExponentBias F} →
  {input : ExactRationalInput F} →
  RoundingOutcome metric bias input →
  Flags
roundingOutcomeFlags outcome =
  roundingFlags
    (exactnessClass (RoundingOutcome.exactness outcome))
    (RoundingOutcome.tininess outcome)
    (RoundingOutcome.overflowStatus outcome)

record RoundedRationalRelation {F : BinaryInterchangeFormat}
  (metric : RoundingMetric)
  (bias : PositiveExponentBias F)
  (input : ExactRationalInput F)
  (encoding : BinaryEncoding F)
  (flags : Flags) : Type₀ where
  constructor rounded-rational-relation
  field
    outcome : RoundingOutcome metric bias input
    encoding≡candidate :
      encoding ≡ candidateEncoding (RoundingOutcome.candidate outcome)
    flags≡outcome :
      flags ≡ roundingOutcomeFlags outcome