module IEEE754.SignedValue where

open import IEEE754.Prelude
open import IEEE754.Sign
open import IEEE754.Format
open import IEEE754.Semantics
open import IEEE754.Exact
open import IEEE754.Representation
open import IEEE754.FiniteSpec
open import IEEE754.FiniteDecode
open import IEEE754.Representable

import Cubical.Data.Rationals as ℚ

signedMagnitude : Sign → ℚ.ℚ → ℚ.ℚ
signedMagnitude = applySignℚ

signedMagnitude-positive :
  (q : ℚ.ℚ) →
  signedMagnitude positive q ≡ q
signedMagnitude-positive q = refl

signedMagnitude-negative :
  (q : ℚ.ℚ) →
  signedMagnitude negative q ≡ ℚ.- q
signedMagnitude-negative q = refl

data SignedRationalValue {F : BinaryInterchangeFormat}
  : IEEEValue F → ℚ.ℚ → Type₀ where
  signed-finite :
    (sign : Sign) →
    (magnitude : ℚ.ℚ) →
    SignedRationalValue
      (finiteValue sign magnitude)
      (signedMagnitude sign magnitude)

finiteValue-signedRational :
  ∀ {F} →
  (sign : Sign) →
  (magnitude : ℚ.ℚ) →
  SignedRationalValue
    {F = F}
    (finiteValue sign magnitude)
    (signedMagnitude sign magnitude)
finiteValue-signedRational = signed-finite

decodedFiniteValue→signedRational :
  ∀ {F} →
  (encoding : BinaryEncoding F) →
  {sign : Sign} →
  {magnitude : ℚ.ℚ} →
  decodeValue encoding ≡ finiteValue sign magnitude →
  SignedRationalValue
    (decodeValue encoding)
    (signedMagnitude sign magnitude)
decodedFiniteValue→signedRational encoding {sign} {magnitude} decode≡finite =
  subst
    (λ value →
      SignedRationalValue value (signedMagnitude sign magnitude))
    (sym decode≡finite)
    (signed-finite sign magnitude)

textbookFiniteValue→signedRational :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  {encoding : BinaryEncoding F} →
  {sign : Sign} →
  {magnitude : ℚ.ℚ} →
  TextbookDecodedValueSpec
    bias
    encoding
    (finiteValue sign magnitude) →
  SignedRationalValue
    (decodeValue encoding)
    (signedMagnitude sign magnitude)
textbookFiniteValue→signedRational bias {sign = sign} {magnitude} spec =
  subst
    (λ value →
      SignedRationalValue value (signedMagnitude sign magnitude))
    (textbookDecodedValueSpec-complete bias spec)
    (signed-finite sign magnitude)

representableMagnitude→signedRational :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (sign : Sign) →
  {magnitude : ℚ.ℚ} →
  FiniteTextbookMagnitude bias magnitude →
  Σ
    (BinaryEncoding F)
    (λ encoding →
      SignedRationalValue
        (decodeValue encoding)
        (signedMagnitude sign magnitude))
representableMagnitude→signedRational bias sign representable
  with representableMagnitude→textbookFiniteValue bias sign representable
... | encoding , textbookSpec =
  encoding ,
  textbookFiniteValue→signedRational bias textbookSpec

decodeFiniteValue→representableSignedRational :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (encoding : BinaryEncoding F) →
  {sign : Sign} →
  {magnitude : ℚ.ℚ} →
  decodeValue encoding ≡ finiteValue sign magnitude →
  FiniteTextbookMagnitude bias magnitude ×
  SignedRationalValue
    (decodeValue encoding)
    (signedMagnitude sign magnitude)
decodeFiniteValue→representableSignedRational
  bias
  encoding
  decode≡finite =
  decodeFiniteValue→representableMagnitude bias encoding decode≡finite ,
  decodedFiniteValue→signedRational encoding decode≡finite