{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{- HLINT ignore "Unused LANGUAGE pragma" -}

-- |
-- Module      :   Grisette.Internal.SymPrim.FP
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.FP
  ( ValidFP,
    FP (..),
    FP16,
    FP32,
    FP64,
    withValidFPProofs,
    FPRoundingMode (..),
    allFPRoundingMode,
    NotRepresentableFPError (..),
    ConvertibleBound (..),
    nextFP,
    prevFP,
    withUnsafeValidFP,
    checkDynamicValidFP,
    invalidFPMessage,
  )
where

import Control.DeepSeq (NFData (rnf))
import Control.Exception (Exception, throw)
import qualified Data.Binary as Binary
import Data.Bits (Bits (complement, shiftL, shiftR, xor, (.&.)))
import Data.Bytes.Serial (Serial (deserialize, serialize))
import Data.Hashable (Hashable (hashWithSalt))
import Data.Int (Int16, Int32, Int64)
import Data.Maybe (fromJust)
import Data.Proxy (Proxy (Proxy))
import Data.Ratio (numerator)
import Data.SBV
  ( BVIsNonZero,
    FloatingPoint,
    SWord,
    SymVal (literal, unliteral),
    ValidFloat,
    Word16,
    Word32,
    Word64,
    denominator,
    infinity,
    nan,
    sFloatingPointAsSWord,
    sWordAsSFloatingPoint,
  )
import Data.SBV.Float (fpEncodeFloat)
import qualified Data.SBV.Float as SBVF
import qualified Data.SBV.Internals as SBVI
import qualified Data.Serialize as Cereal
import Data.Type.Bool (type (&&), type (||))
import Data.Type.Equality (type (:~:) (Refl), type (==))
import GHC.Exception (Exception (displayException))
import GHC.Generics (Generic)
import GHC.Natural (Natural)
import GHC.TypeNats
  ( CmpNat,
    KnownNat,
    Nat,
    natVal,
    type (+),
    type (<=),
  )
import Grisette.Internal.Core.Data.Class.BitCast
  ( BitCast (bitCast),
    BitCastCanonical (bitCastCanonicalValue),
    BitCastOr (bitCastOr),
    bitCastOrCanonical,
  )
import Grisette.Internal.Core.Data.Class.BitVector (SizedBV (sizedBVConcat))
import Grisette.Internal.Core.Data.Class.Function (Apply (FunType, apply))
import Grisette.Internal.Core.Data.Class.IEEEFP
  ( IEEEFPConstants
      ( fpMaxNormalized,
        fpMaxSubnormal,
        fpMinNormalized,
        fpMinSubnormal,
        fpNaN,
        fpNegativeInfinite,
        fpNegativeZero,
        fpPositiveInfinite,
        fpPositiveZero
      ),
    IEEEFPConvertible (fromFPOr, toFP),
    IEEEFPOp
      ( fpAbs,
        fpMaximum,
        fpMaximumNumber,
        fpMinimum,
        fpMinimumNumber,
        fpNeg,
        fpRem
      ),
    IEEEFPRoundingMode (rna, rne, rtn, rtp, rtz),
    IEEEFPRoundingOp (fpAdd, fpDiv, fpFMA, fpMul, fpRoundToIntegral, fpSqrt, fpSub),
    IEEEFPToAlgReal,
    fpIsInfinite,
    fpIsNaN,
    fpIsNegativeInfinite,
    fpIsNegativeZero,
    fpIsPositiveInfinite,
    fpIsPositiveZero,
    fpIsZero,
  )
import Grisette.Internal.SymPrim.AlgReal
  ( AlgReal (AlgExactRational),
    UnsupportedAlgRealOperation (UnsupportedAlgRealOperation, msg, op),
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN, WordN16, WordN32, WordN64)
import Grisette.Internal.Utils.Parameterized
  ( KnownProof (KnownProof),
    knownAdd,
    unsafeAxiom,
    unsafeLeqProof,
    withKnownProof,
    withLeqProof,
  )
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import LibBF
  ( BFOpts,
    BigFloat,
    RoundMode,
    Status,
    allowSubnormal,
    bfAdd,
    bfDiv,
    bfFMA,
    bfFromInteger,
    bfIsInf,
    bfIsNaN,
    bfIsNeg,
    bfIsPos,
    bfIsZero,
    bfMul,
    bfNaN,
    bfNegInf,
    bfNegZero,
    bfPosInf,
    bfPosZero,
    bfRoundFloat,
    bfRoundInt,
    bfSqrt,
    bfSub,
    expBits,
    precBits,
    rnd,
    pattern NearAway,
    pattern NearEven,
    pattern ToNegInf,
    pattern ToPosInf,
    pattern ToZero,
  )
import Test.QuickCheck (frequency, oneof)
import qualified Test.QuickCheck as QC

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend
-- >>> import Data.Proxy

bvIsNonZeroFromGEq1 ::
  forall w r proxy.
  (1 <= w) =>
  proxy w ->
  ((BVIsNonZero w) => r) ->
  r
bvIsNonZeroFromGEq1 :: forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 proxy w
_ BVIsNonZero w => r
r1 = case w :~: 1
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
  w :~: 1
Refl -> r
BVIsNonZero w => r
r1

-- | A type-level proof that the given bit-widths are valid for a floating-point
-- number.
type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb

-- | Check if the given floating-point type is valid.
checkDynamicValidFP :: Natural -> Natural -> Bool
checkDynamicValidFP :: Natural -> Natural -> Bool
checkDynamicValidFP Natural
eb Natural
sb =
  Natural
eb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
2 Bool -> Bool -> Bool
&& Natural
eb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
61 Bool -> Bool -> Bool
&& Natural
sb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
2 Bool -> Bool -> Bool
&& Natural
sb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
4611686018427387902

-- | A message thrown when the floating-point type is invalid.
invalidFPMessage :: String
invalidFPMessage :: String
invalidFPMessage =
  String
"Invalid floating point type `SFloatingPoint eb sb'\n`n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"  A valid float of type 'SFloatingPoint eb sb' must satisfy:\n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"        eb `elem` [2 .. 61]\n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"        sb `elem` [2 .. 4611686018427387902]\n\n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"  Given type falls outside of this range, or the sizes are not known naturals."

-- | Provide an (unsafe) type-level proof that the given floating-point type is
-- valid.
withUnsafeValidFP ::
  forall eb sb r. (KnownNat eb, KnownNat sb) => ((ValidFP eb sb) => r) -> r
withUnsafeValidFP :: forall (eb :: Natural) (sb :: Natural) r.
(KnownNat eb, KnownNat sb) =>
(ValidFP eb sb => r) -> r
withUnsafeValidFP ValidFP eb sb => r
r =
  let eb :: Natural
eb = Proxy eb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb)
      sb :: Natural
sb = Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb)
   in if Natural -> Natural -> Bool
checkDynamicValidFP Natural
eb Natural
sb
        then case forall (a :: Bool) (b :: Bool). a :~: b
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @True
          @( ((CmpNat eb 2 == 'EQ) || (CmpNat eb 2 == 'GT))
               && ( ((CmpNat eb 61 == 'EQ) || (CmpNat eb 61 == 'LT))
                      && ( ((CmpNat sb 2 == 'EQ) || (CmpNat sb 2 == 'GT))
                             && ( (CmpNat sb 4611686018427387902 == 'EQ)
                                    || (CmpNat sb 4611686018427387902 == 'LT)
                                )
                         )
                  )
           ) of
          'True
:~: (((CmpNat eb 2 == 'EQ) || (CmpNat eb 2 == 'GT))
     && (((CmpNat eb 61 == 'EQ) || (CmpNat eb 61 == 'LT))
         && (((CmpNat sb 2 == 'EQ) || (CmpNat sb 2 == 'GT))
             && ((CmpNat sb 4611686018427387902 == 'EQ)
                 || (CmpNat sb 4611686018427387902 == 'LT)))))
Refl -> r
ValidFP eb sb => r
r
        else String -> r
forall a. HasCallStack => String -> a
error String
invalidFPMessage

-- | IEEE 754 floating-point number with @eb@ exponent bits and @sb@ significand
-- bits.
--
-- >>> 1.0 + 2.0 :: FP 11 53
-- 3.0
--
-- More operations are available. Please refer to "Grisette.Core#g:symops" for
-- more information.
newtype FP (eb :: Nat) (sb :: Nat) = FP {forall (eb :: Natural) (sb :: Natural).
FP eb sb -> FloatingPoint eb sb
unFP :: FloatingPoint eb sb}
  deriving newtype (FP eb sb -> FP eb sb -> Bool
(FP eb sb -> FP eb sb -> Bool)
-> (FP eb sb -> FP eb sb -> Bool) -> Eq (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
FP eb sb -> FP eb sb -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (eb :: Natural) (sb :: Natural).
FP eb sb -> FP eb sb -> Bool
== :: FP eb sb -> FP eb sb -> Bool
$c/= :: forall (eb :: Natural) (sb :: Natural).
FP eb sb -> FP eb sb -> Bool
/= :: FP eb sb -> FP eb sb -> Bool
Eq, Int -> FP eb sb -> String -> String
[FP eb sb] -> String -> String
FP eb sb -> String
(Int -> FP eb sb -> String -> String)
-> (FP eb sb -> String)
-> ([FP eb sb] -> String -> String)
-> Show (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
Int -> FP eb sb -> String -> String
forall (eb :: Natural) (sb :: Natural).
[FP eb sb] -> String -> String
forall (eb :: Natural) (sb :: Natural). FP eb sb -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: forall (eb :: Natural) (sb :: Natural).
Int -> FP eb sb -> String -> String
showsPrec :: Int -> FP eb sb -> String -> String
$cshow :: forall (eb :: Natural) (sb :: Natural). FP eb sb -> String
show :: FP eb sb -> String
$cshowList :: forall (eb :: Natural) (sb :: Natural).
[FP eb sb] -> String -> String
showList :: [FP eb sb] -> String -> String
Show)

-- Workaround for https://github.com/GaloisInc/libBF-hs/pull/32, which affects
-- the correctness of the Ord instance for 'Data.SBV.FloatingPoint'.
instance (ValidFP eb sb) => Ord (FP eb sb) where
  FP FloatingPoint eb sb
x < :: FP eb sb -> FP eb sb -> Bool
< FP FloatingPoint eb sb
y | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
x Bool -> Bool -> Bool
|| FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
y = Bool
False
  FP FloatingPoint eb sb
x < FP FloatingPoint eb sb
y = FloatingPoint eb sb
x FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall a. Ord a => a -> a -> Bool
< FloatingPoint eb sb
y
  FP FloatingPoint eb sb
x <= :: FP eb sb -> FP eb sb -> Bool
<= FP FloatingPoint eb sb
y | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
x Bool -> Bool -> Bool
|| FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
y = Bool
False
  FP FloatingPoint eb sb
x <= FP FloatingPoint eb sb
y = FloatingPoint eb sb
x FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall a. Ord a => a -> a -> Bool
<= FloatingPoint eb sb
y
  FP FloatingPoint eb sb
x > :: FP eb sb -> FP eb sb -> Bool
> FP FloatingPoint eb sb
y | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
x Bool -> Bool -> Bool
|| FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
y = Bool
False
  FP FloatingPoint eb sb
x > FP FloatingPoint eb sb
y = FloatingPoint eb sb
x FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall a. Ord a => a -> a -> Bool
> FloatingPoint eb sb
y
  FP FloatingPoint eb sb
x >= :: FP eb sb -> FP eb sb -> Bool
>= FP FloatingPoint eb sb
y | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
x Bool -> Bool -> Bool
|| FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
y = Bool
False
  FP FloatingPoint eb sb
x >= FP FloatingPoint eb sb
y = FloatingPoint eb sb
x FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall a. Ord a => a -> a -> Bool
>= FloatingPoint eb sb
y

-- | IEEE 754 half-precision floating-point number.
type FP16 = FP 5 11

-- | IEEE 754 single-precision floating-point number.
type FP32 = FP 8 24

-- | IEEE 754 double-precision floating-point number.
type FP64 = FP 11 53

-- | Some type-level witnesses that could be derived from 'ValidFP'.
withValidFPProofs ::
  forall eb sb r.
  (ValidFP eb sb) =>
  ( ( KnownNat (eb + sb),
      BVIsNonZero (eb + sb),
      1 <= eb + sb,
      1 <= eb,
      1 <= sb
    ) =>
    r
  ) ->
  r
withValidFPProofs :: forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs (KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
r
r =
  KnownProof (eb + sb) -> (KnownNat (eb + sb) => r) -> r
forall (n :: Natural) r. KnownProof n -> (KnownNat n => r) -> r
withKnownProof (KnownProof eb -> KnownProof sb -> KnownProof (eb + sb)
forall (m :: Natural) (n :: Natural).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd (forall (n :: Natural). KnownNat n => KnownProof n
KnownProof @eb) (forall (n :: Natural). KnownNat n => KnownProof n
KnownProof @sb)) ((KnownNat (eb + sb) => r) -> r) -> (KnownNat (eb + sb) => r) -> r
forall a b. (a -> b) -> a -> b
$
    LeqProof 1 (eb + sb) -> ((1 <= (eb + sb)) => r) -> r
forall (m :: Natural) (n :: Natural) r.
LeqProof m n -> ((m <= n) => r) -> r
withLeqProof (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @(eb + sb)) (((1 <= (eb + sb)) => r) -> r) -> ((1 <= (eb + sb)) => r) -> r
forall a b. (a -> b) -> a -> b
$
      LeqProof 1 eb -> ((1 <= eb) => r) -> r
forall (m :: Natural) (n :: Natural) r.
LeqProof m n -> ((m <= n) => r) -> r
withLeqProof (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @eb) (((1 <= eb) => r) -> r) -> ((1 <= eb) => r) -> r
forall a b. (a -> b) -> a -> b
$
        LeqProof 1 sb -> ((1 <= sb) => r) -> r
forall (m :: Natural) (n :: Natural) r.
LeqProof m n -> ((m <= n) => r) -> r
withLeqProof (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @sb) (((1 <= sb) => r) -> r) -> ((1 <= sb) => r) -> r
forall a b. (a -> b) -> a -> b
$
          Proxy (eb + sb) -> (BVIsNonZero (eb + sb) => r) -> r
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(eb + sb)) r
(KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
r
BVIsNonZero (eb + sb) => r
r

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (WordN r) (FP eb sb) where
  bitCast :: WordN r -> FP eb sb
bitCast WordN r
v = FloatingPoint eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
FloatingPoint eb sb -> FP eb sb
FP FloatingPoint eb sb
fp
    where
      sword :: SWord r
      sword :: SWord r
sword = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
WordN r -> SWord r
WordN r -> SWord r
forall a b. (Integral a, Num b) => a -> b
fromIntegral WordN r
v
      fp :: FloatingPoint eb sb
      fp :: FloatingPoint eb sb
fp =
        forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FloatingPoint eb sb)
 -> FloatingPoint eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FloatingPoint eb sb)
-> FloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
          Maybe (FloatingPoint eb sb) -> FloatingPoint eb sb
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (FloatingPoint eb sb) -> FloatingPoint eb sb)
-> Maybe (FloatingPoint eb sb) -> FloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
            SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$
              SWord (eb + sb) -> SBV (FloatingPoint eb sb)
forall (eb :: Natural) (sb :: Natural).
(KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
SWord (eb + sb) -> SFloatingPoint eb sb
sWordAsSFloatingPoint SWord r
SWord (eb + sb)
sword

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (IntN r) (FP eb sb) where
  bitCast :: IntN r -> FP eb sb
bitCast IntN r
x = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$ WordN r -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast (IntN r -> WordN r
forall from to. BitCast from to => from -> to
bitCast IntN r
x :: WordN (eb + sb))

#define BITCAST_VIA_INTERMEDIATE(from, to, intermediate) \
  instance BitCast (from) (to) where \
    bitCast x = bitCast (bitCast x :: intermediate)

#if 1
BITCAST_VIA_INTERMEDIATE(Double, FP64, WordN 64)
BITCAST_VIA_INTERMEDIATE(Int64, FP64, WordN 64)
BITCAST_VIA_INTERMEDIATE(Word64, FP64, WordN 64)

BITCAST_VIA_INTERMEDIATE(Float, FP32, WordN 32)
BITCAST_VIA_INTERMEDIATE(Int32, FP32, WordN 32)
BITCAST_VIA_INTERMEDIATE(Word32, FP32, WordN 32)

BITCAST_VIA_INTERMEDIATE(Word16, FP16, WordN 16)
BITCAST_VIA_INTERMEDIATE(Int16, FP16, WordN 16)
#endif
instance NFData (FP eb sb) where
  rnf :: FP eb sb -> ()
rnf (FP FloatingPoint eb sb
x) = FloatingPoint eb sb
x FloatingPoint eb sb -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance (ValidFP eb sb) => Lift (FP eb sb) where
  liftTyped :: forall (m :: * -> *). Quote m => FP eb sb -> Code m (FP eb sb)
liftTyped FP eb sb
fp = [||from -> to
forall from to. BitCast from to => from -> to
bitCast from
WordN (eb + sb)
wordnValue||]
    where
      wordnValue :: WordN (eb + sb)
wordnValue = FP eb sb -> WordN (eb + sb)
forall from to. BitCastOrCanonical from to => from -> to
bitCastOrCanonical FP eb sb
fp :: WordN (eb + sb)

instance (ValidFP eb sb) => Hashable (FP eb sb) where
  hashWithSalt :: Int -> FP eb sb -> Int
hashWithSalt Int
salt FP eb sb
x =
    Int -> WordN (eb + sb) -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (FP eb sb -> WordN (eb + sb)
forall from to. BitCastOrCanonical from to => from -> to
bitCastOrCanonical FP eb sb
x :: WordN (eb + sb))

deriving newtype instance (ValidFloat eb sb) => Num (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => Fractional (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => Floating (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => Real (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => RealFrac (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => RealFloat (FP eb sb)

instance (ValidFloat eb sb) => QC.Arbitrary (FP eb sb) where
  arbitrary :: Gen (FP eb sb)
arbitrary = do
    [(Int, Gen (FP eb sb))] -> Gen (FP eb sb)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ ( Int
3,
          forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (FP eb sb))
 -> Gen (FP eb sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (FP eb sb))
-> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$
            WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast
              (WordN (eb + sb) -> FP eb sb)
-> Gen (WordN (eb + sb)) -> Gen (FP eb sb)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Gen (WordN (eb + sb))
forall a. Arbitrary a => Gen a
QC.arbitrary :: QC.Gen (WordN (eb + sb)))
        ),
        ( Int
5,
          -- mostly normalized numbers
          forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (FP eb sb))
 -> Gen (FP eb sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (FP eb sb))
-> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$ do
            WordN eb
e <- Gen (WordN eb)
egen
            WordN sb
s <- Gen (WordN sb)
sgen
            WordN (eb + sb)
msb <- Gen (WordN (eb + sb))
msbGen
            WordN (eb + sb)
smsb <- Gen (WordN (eb + sb))
smsbGen
            FP eb sb -> Gen (FP eb sb)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (FP eb sb -> Gen (FP eb sb)) -> FP eb sb -> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$ WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast (WordN eb -> WordN sb -> WordN (eb + sb)
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat WordN eb
e WordN sb
s WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a -> a
`xor` WordN (eb + sb)
msb WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a -> a
`xor` WordN (eb + sb)
smsb)
        ),
        ( Int
4,
          -- mostly denormalized numbers
          forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (FP eb sb))
 -> Gen (FP eb sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (FP eb sb))
-> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$ do
            WordN sb
s <- Gen (WordN sb)
sgen
            WordN (eb + sb)
msb <- Gen (WordN (eb + sb))
msbGen
            WordN (eb + sb)
smsb <- Gen (WordN (eb + sb))
smsbGen
            FP eb sb -> Gen (FP eb sb)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (FP eb sb -> Gen (FP eb sb)) -> FP eb sb -> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$
              WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast (WordN eb -> WordN sb -> WordN (eb + sb)
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat WordN eb
0 WordN sb
s WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a -> a
`xor` WordN (eb + sb)
msb WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a -> a
.&. WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a
complement WordN (eb + sb)
smsb)
        ),
        (Int
1, [Gen (FP eb sb)] -> Gen (FP eb sb)
forall a. HasCallStack => [Gen a] -> Gen a
oneof ([Gen (FP eb sb)] -> Gen (FP eb sb))
-> [Gen (FP eb sb)] -> Gen (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FP eb sb -> Gen (FP eb sb)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (FP eb sb -> Gen (FP eb sb)) -> [FP eb sb] -> [Gen (FP eb sb)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FP eb sb
forall a. Floating a => a
nan, FP eb sb
0, -FP eb sb
0, FP eb sb
forall a. Floating a => a
infinity, -FP eb sb
forall a. Floating a => a
infinity])
      ]
    where
      eb :: Int
eb = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy eb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb) :: Int
      sb :: Int
sb = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) :: Int
      egen :: Gen (WordN eb)
egen = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (WordN eb))
 -> Gen (WordN eb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (WordN eb))
-> Gen (WordN eb)
forall a b. (a -> b) -> a -> b
$ Gen (WordN eb)
(KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
Gen (WordN eb)
forall a. Arbitrary a => Gen a
QC.arbitrary :: QC.Gen (WordN eb)
      sgen :: Gen (WordN sb)
sgen = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (WordN sb))
 -> Gen (WordN sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (WordN sb))
-> Gen (WordN sb)
forall a b. (a -> b) -> a -> b
$ Gen (WordN sb)
(KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
Gen (WordN sb)
forall a. Arbitrary a => Gen a
QC.arbitrary :: QC.Gen (WordN sb)
      msbGen :: Gen (WordN (eb + sb))
msbGen =
        forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (WordN (eb + sb)))
 -> Gen (WordN (eb + sb)))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (WordN (eb + sb)))
-> Gen (WordN (eb + sb))
forall a b. (a -> b) -> a -> b
$
          [Gen (WordN (eb + sb))] -> Gen (WordN (eb + sb))
forall a. HasCallStack => [Gen a] -> Gen a
oneof [WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return WordN (eb + sb)
0, WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (WordN (eb + sb) -> Gen (WordN (eb + sb)))
-> WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a b. (a -> b) -> a -> b
$ WordN (eb + sb)
1 WordN (eb + sb) -> Int -> WordN (eb + sb)
forall a. Bits a => a -> Int -> a
`shiftL` (Int
eb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)] ::
          QC.Gen (WordN (eb + sb))
      smsbGen :: Gen (WordN (eb + sb))
smsbGen =
        forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  Gen (WordN (eb + sb)))
 -> Gen (WordN (eb + sb)))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    Gen (WordN (eb + sb)))
-> Gen (WordN (eb + sb))
forall a b. (a -> b) -> a -> b
$
          [Gen (WordN (eb + sb))] -> Gen (WordN (eb + sb))
forall a. HasCallStack => [Gen a] -> Gen a
oneof [WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return WordN (eb + sb)
0, WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (WordN (eb + sb) -> Gen (WordN (eb + sb)))
-> WordN (eb + sb) -> Gen (WordN (eb + sb))
forall a b. (a -> b) -> a -> b
$ WordN (eb + sb)
1 WordN (eb + sb) -> Int -> WordN (eb + sb)
forall a. Bits a => a -> Int -> a
`shiftL` (Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)] ::
          QC.Gen (WordN (eb + sb))

-- | Rounding mode for floating-point operations.
data FPRoundingMode
  = -- | Round to nearest, ties to even.
    RNE
  | -- | Round to nearest, ties to away from zero.
    RNA
  | -- | Round towards positive infinity.
    RTP
  | -- | Round towards negative infinity.
    RTN
  | -- | Round towards zero.
    RTZ
  deriving (FPRoundingMode -> FPRoundingMode -> Bool
(FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> Bool) -> Eq FPRoundingMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FPRoundingMode -> FPRoundingMode -> Bool
== :: FPRoundingMode -> FPRoundingMode -> Bool
$c/= :: FPRoundingMode -> FPRoundingMode -> Bool
/= :: FPRoundingMode -> FPRoundingMode -> Bool
Eq, Eq FPRoundingMode
Eq FPRoundingMode =>
(FPRoundingMode -> FPRoundingMode -> Ordering)
-> (FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> Bool)
-> (FPRoundingMode -> FPRoundingMode -> FPRoundingMode)
-> (FPRoundingMode -> FPRoundingMode -> FPRoundingMode)
-> Ord FPRoundingMode
FPRoundingMode -> FPRoundingMode -> Bool
FPRoundingMode -> FPRoundingMode -> Ordering
FPRoundingMode -> FPRoundingMode -> FPRoundingMode
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FPRoundingMode -> FPRoundingMode -> Ordering
compare :: FPRoundingMode -> FPRoundingMode -> Ordering
$c< :: FPRoundingMode -> FPRoundingMode -> Bool
< :: FPRoundingMode -> FPRoundingMode -> Bool
$c<= :: FPRoundingMode -> FPRoundingMode -> Bool
<= :: FPRoundingMode -> FPRoundingMode -> Bool
$c> :: FPRoundingMode -> FPRoundingMode -> Bool
> :: FPRoundingMode -> FPRoundingMode -> Bool
$c>= :: FPRoundingMode -> FPRoundingMode -> Bool
>= :: FPRoundingMode -> FPRoundingMode -> Bool
$cmax :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode
max :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode
$cmin :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode
min :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode
Ord, (forall x. FPRoundingMode -> Rep FPRoundingMode x)
-> (forall x. Rep FPRoundingMode x -> FPRoundingMode)
-> Generic FPRoundingMode
forall x. Rep FPRoundingMode x -> FPRoundingMode
forall x. FPRoundingMode -> Rep FPRoundingMode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FPRoundingMode -> Rep FPRoundingMode x
from :: forall x. FPRoundingMode -> Rep FPRoundingMode x
$cto :: forall x. Rep FPRoundingMode x -> FPRoundingMode
to :: forall x. Rep FPRoundingMode x -> FPRoundingMode
Generic, (forall (m :: * -> *). Quote m => FPRoundingMode -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    FPRoundingMode -> Code m FPRoundingMode)
-> Lift FPRoundingMode
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FPRoundingMode -> m Exp
forall (m :: * -> *).
Quote m =>
FPRoundingMode -> Code m FPRoundingMode
$clift :: forall (m :: * -> *). Quote m => FPRoundingMode -> m Exp
lift :: forall (m :: * -> *). Quote m => FPRoundingMode -> m Exp
$cliftTyped :: forall (m :: * -> *).
Quote m =>
FPRoundingMode -> Code m FPRoundingMode
liftTyped :: forall (m :: * -> *).
Quote m =>
FPRoundingMode -> Code m FPRoundingMode
Lift)
  deriving anyclass (Eq FPRoundingMode
Eq FPRoundingMode =>
(Int -> FPRoundingMode -> Int)
-> (FPRoundingMode -> Int) -> Hashable FPRoundingMode
Int -> FPRoundingMode -> Int
FPRoundingMode -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FPRoundingMode -> Int
hashWithSalt :: Int -> FPRoundingMode -> Int
$chash :: FPRoundingMode -> Int
hash :: FPRoundingMode -> Int
Hashable, FPRoundingMode -> ()
(FPRoundingMode -> ()) -> NFData FPRoundingMode
forall a. (a -> ()) -> NFData a
$crnf :: FPRoundingMode -> ()
rnf :: FPRoundingMode -> ()
NFData, (forall (m :: * -> *). MonadPut m => FPRoundingMode -> m ())
-> (forall (m :: * -> *). MonadGet m => m FPRoundingMode)
-> Serial FPRoundingMode
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m FPRoundingMode
forall (m :: * -> *). MonadPut m => FPRoundingMode -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => FPRoundingMode -> m ()
serialize :: forall (m :: * -> *). MonadPut m => FPRoundingMode -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m FPRoundingMode
deserialize :: forall (m :: * -> *). MonadGet m => m FPRoundingMode
Serial)

instance Show FPRoundingMode where
  show :: FPRoundingMode -> String
show FPRoundingMode
RNE = String
"rne"
  show FPRoundingMode
RNA = String
"rna"
  show FPRoundingMode
RTP = String
"rtp"
  show FPRoundingMode
RTN = String
"rtn"
  show FPRoundingMode
RTZ = String
"rtz"

-- | All IEEE 754 rounding modes.
allFPRoundingMode :: [FPRoundingMode]
allFPRoundingMode :: [FPRoundingMode]
allFPRoundingMode = [FPRoundingMode
RNE, FPRoundingMode
RNA, FPRoundingMode
RTP, FPRoundingMode
RTN, FPRoundingMode
RTZ]

instance QC.Arbitrary FPRoundingMode where
  arbitrary :: Gen FPRoundingMode
arbitrary = [FPRoundingMode] -> Gen FPRoundingMode
forall a. HasCallStack => [a] -> Gen a
QC.elements [FPRoundingMode
RNE, FPRoundingMode
RNA, FPRoundingMode
RTP, FPRoundingMode
RTN, FPRoundingMode
RTZ]

instance
  (ValidFP eb sb, n ~ (eb + sb)) =>
  BitCastCanonical (FP eb sb) (WordN n)
  where
  bitCastCanonicalValue :: forall (proxy :: * -> *). proxy (FP eb sb) -> WordN n
bitCastCanonicalValue proxy (FP eb sb)
_ =
    forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  WordN n)
 -> WordN n)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    WordN n)
-> WordN n
forall a b. (a -> b) -> a -> b
$
      WordN eb -> WordN sb -> WordN (eb + sb)
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat (WordN eb -> Int -> WordN eb
forall a. Bits a => a -> Int -> a
shiftR (-WordN eb
1) Int
1 :: WordN eb) WordN sb
highsb
    where
      sb :: Int
sb = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) :: Int
      highsb :: WordN sb
highsb = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  WordN sb)
 -> WordN sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    WordN sb)
-> WordN sb
forall a b. (a -> b) -> a -> b
$ WordN sb -> Int -> WordN sb
forall a. Bits a => a -> Int -> a
shiftL WordN sb
3 (Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) :: WordN sb

instance
  (ValidFP eb sb, n ~ (eb + sb)) =>
  BitCastCanonical (FP eb sb) (IntN n)
  where
  bitCastCanonicalValue :: forall (proxy :: * -> *). proxy (FP eb sb) -> IntN n
bitCastCanonicalValue proxy (FP eb sb)
n =
    forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  IntN n)
 -> IntN n)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    IntN n)
-> IntN n
forall a b. (a -> b) -> a -> b
$
      WordN n -> IntN n
forall from to. BitCast from to => from -> to
bitCast (proxy (FP eb sb) -> WordN n
forall from to (proxy :: * -> *).
BitCastCanonical from to =>
proxy from -> to
forall (proxy :: * -> *). proxy (FP eb sb) -> WordN n
bitCastCanonicalValue proxy (FP eb sb)
n :: WordN n)

#define BIT_CAST_CANONICAL_VIA_INTERMEDIATE(from, to, intermediate) \
  instance BitCastCanonical (from) (to) where \
    bitCastCanonicalValue x = bitCast (bitCastCanonicalValue x :: intermediate)

#if 1
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP64, Word64, WordN64)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP64, Int64, WordN64)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP64, Double, WordN64)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP32, Word32, WordN32)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP32, Int32, WordN32)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP32, Float, WordN32)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP16, Word16, WordN16)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP16, Int16, WordN16)
#endif

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (FP eb sb) (WordN r) where
  bitCastOr :: WordN r -> FP eb sb -> WordN r
bitCastOr WordN r
d (FP FloatingPoint eb sb
f)
    | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FloatingPoint eb sb
f = WordN r
d
    | Bool
otherwise = WordN r
WordN (eb + sb)
wordn
    where
      wordn :: WordN (eb + sb)
      wordn :: WordN (eb + sb)
wordn =
        forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  WordN (eb + sb))
 -> WordN (eb + sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    WordN (eb + sb))
-> WordN (eb + sb)
forall a b. (a -> b) -> a -> b
$
          WordN r -> WordN (eb + sb)
forall a b. (Integral a, Num b) => a -> b
fromIntegral (WordN r -> WordN (eb + sb)) -> WordN r -> WordN (eb + sb)
forall a b. (a -> b) -> a -> b
$
            Maybe (WordN r) -> WordN r
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WordN r) -> WordN r) -> Maybe (WordN r) -> WordN r
forall a b. (a -> b) -> a -> b
$
              SBV (WordN r) -> Maybe (WordN r)
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBV (WordN r) -> Maybe (WordN r))
-> SBV (WordN r) -> Maybe (WordN r)
forall a b. (a -> b) -> a -> b
$
                SFloatingPoint eb sb -> SWord (eb + sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsSWord (SFloatingPoint eb sb -> SWord (eb + sb))
-> SFloatingPoint eb sb -> SWord (eb + sb)
forall a b. (a -> b) -> a -> b
$
                  FloatingPoint eb sb -> SFloatingPoint eb sb
forall a. SymVal a => a -> SBV a
literal FloatingPoint eb sb
f

instance
  (ValidFP eb sb, n ~ (eb + sb)) =>
  BitCastOr (FP eb sb) (IntN n)
  where
  bitCastOr :: IntN n -> FP eb sb -> IntN n
bitCastOr IntN n
d FP eb sb
n =
    forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  IntN n)
 -> IntN n)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    IntN n)
-> IntN n
forall a b. (a -> b) -> a -> b
$
      WordN n -> IntN n
forall from to. BitCast from to => from -> to
bitCast (WordN n -> FP eb sb -> WordN n
forall from to. BitCastOr from to => to -> from -> to
bitCastOr (IntN n -> WordN n
forall from to. BitCast from to => from -> to
bitCast IntN n
d) FP eb sb
n :: WordN n)

#define BIT_CAST_OR_VIA_INTERMEDIATE(from, to, intermediate) \
  instance BitCastOr (from) (to) where \
    bitCastOr d x = bitCast (bitCastOr (bitCast d) x :: intermediate)

#if 1
BIT_CAST_OR_VIA_INTERMEDIATE(FP64, Word64, WordN64)
BIT_CAST_OR_VIA_INTERMEDIATE(FP64, Int64, WordN64)
BIT_CAST_OR_VIA_INTERMEDIATE(FP64, Double, WordN64)
BIT_CAST_OR_VIA_INTERMEDIATE(FP32, Word32, WordN32)
BIT_CAST_OR_VIA_INTERMEDIATE(FP32, Int32, WordN32)
BIT_CAST_OR_VIA_INTERMEDIATE(FP32, Float, WordN32)
BIT_CAST_OR_VIA_INTERMEDIATE(FP16, Word16, WordN16)
BIT_CAST_OR_VIA_INTERMEDIATE(FP16, Int16, WordN16)
#endif

-- | An error thrown when bitcasting or converting t'FP' NaN to other types.
data NotRepresentableFPError
  = NaNError
  | FPUnderflowError
  | FPOverflowError
  deriving (Int -> NotRepresentableFPError -> String -> String
[NotRepresentableFPError] -> String -> String
NotRepresentableFPError -> String
(Int -> NotRepresentableFPError -> String -> String)
-> (NotRepresentableFPError -> String)
-> ([NotRepresentableFPError] -> String -> String)
-> Show NotRepresentableFPError
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> NotRepresentableFPError -> String -> String
showsPrec :: Int -> NotRepresentableFPError -> String -> String
$cshow :: NotRepresentableFPError -> String
show :: NotRepresentableFPError -> String
$cshowList :: [NotRepresentableFPError] -> String -> String
showList :: [NotRepresentableFPError] -> String -> String
Show, NotRepresentableFPError -> NotRepresentableFPError -> Bool
(NotRepresentableFPError -> NotRepresentableFPError -> Bool)
-> (NotRepresentableFPError -> NotRepresentableFPError -> Bool)
-> Eq NotRepresentableFPError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
== :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
$c/= :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
/= :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
Eq, Eq NotRepresentableFPError
Eq NotRepresentableFPError =>
(NotRepresentableFPError -> NotRepresentableFPError -> Ordering)
-> (NotRepresentableFPError -> NotRepresentableFPError -> Bool)
-> (NotRepresentableFPError -> NotRepresentableFPError -> Bool)
-> (NotRepresentableFPError -> NotRepresentableFPError -> Bool)
-> (NotRepresentableFPError -> NotRepresentableFPError -> Bool)
-> (NotRepresentableFPError
    -> NotRepresentableFPError -> NotRepresentableFPError)
-> (NotRepresentableFPError
    -> NotRepresentableFPError -> NotRepresentableFPError)
-> Ord NotRepresentableFPError
NotRepresentableFPError -> NotRepresentableFPError -> Bool
NotRepresentableFPError -> NotRepresentableFPError -> Ordering
NotRepresentableFPError
-> NotRepresentableFPError -> NotRepresentableFPError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: NotRepresentableFPError -> NotRepresentableFPError -> Ordering
compare :: NotRepresentableFPError -> NotRepresentableFPError -> Ordering
$c< :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
< :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
$c<= :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
<= :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
$c> :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
> :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
$c>= :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
>= :: NotRepresentableFPError -> NotRepresentableFPError -> Bool
$cmax :: NotRepresentableFPError
-> NotRepresentableFPError -> NotRepresentableFPError
max :: NotRepresentableFPError
-> NotRepresentableFPError -> NotRepresentableFPError
$cmin :: NotRepresentableFPError
-> NotRepresentableFPError -> NotRepresentableFPError
min :: NotRepresentableFPError
-> NotRepresentableFPError -> NotRepresentableFPError
Ord, (forall x.
 NotRepresentableFPError -> Rep NotRepresentableFPError x)
-> (forall x.
    Rep NotRepresentableFPError x -> NotRepresentableFPError)
-> Generic NotRepresentableFPError
forall x. Rep NotRepresentableFPError x -> NotRepresentableFPError
forall x. NotRepresentableFPError -> Rep NotRepresentableFPError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NotRepresentableFPError -> Rep NotRepresentableFPError x
from :: forall x. NotRepresentableFPError -> Rep NotRepresentableFPError x
$cto :: forall x. Rep NotRepresentableFPError x -> NotRepresentableFPError
to :: forall x. Rep NotRepresentableFPError x -> NotRepresentableFPError
Generic)

instance Exception NotRepresentableFPError where
  displayException :: NotRepresentableFPError -> String
displayException NotRepresentableFPError
NaNError =
    String
"Converting NaN value cannot be done precisely with SMT-LIB2"
  displayException NotRepresentableFPError
FPUnderflowError =
    String
"Converting FP values that cannot be represented by non-FP types due to "
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"underflowing"
  displayException NotRepresentableFPError
FPOverflowError =
    String
"Converting FP values that cannot be represented by non-FP types due to "
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"overflowing"

instance (ValidFP eb sb) => IEEEFPConstants (FP eb sb) where
  fpPositiveInfinite :: FP eb sb
fpPositiveInfinite = FloatingPoint eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
FloatingPoint eb sb -> FP eb sb
FP FloatingPoint eb sb
forall a. Floating a => a
infinity
  {-# INLINE fpPositiveInfinite #-}
  fpNegativeInfinite :: FP eb sb
fpNegativeInfinite = FloatingPoint eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
FloatingPoint eb sb -> FP eb sb
FP (FloatingPoint eb sb -> FP eb sb)
-> FloatingPoint eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ -FloatingPoint eb sb
forall a. Floating a => a
infinity
  {-# INLINE fpNegativeInfinite #-}
  fpNaN :: FP eb sb
fpNaN = FloatingPoint eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
FloatingPoint eb sb -> FP eb sb
FP FloatingPoint eb sb
forall a. Floating a => a
nan
  {-# INLINE fpNaN #-}
  fpNegativeZero :: FP eb sb
fpNegativeZero = FloatingPoint eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
FloatingPoint eb sb -> FP eb sb
FP (FloatingPoint eb sb -> FP eb sb)
-> FloatingPoint eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ -FloatingPoint eb sb
0
  {-# INLINE fpNegativeZero #-}
  fpPositiveZero :: FP eb sb
fpPositiveZero = FloatingPoint eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
FloatingPoint eb sb -> FP eb sb
FP FloatingPoint eb sb
0
  {-# INLINE fpPositiveZero #-}

  fpMinNormalized :: FP eb sb
fpMinNormalized =
    forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$
      WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast (WordN (eb + sb) -> FP eb sb) -> WordN (eb + sb) -> FP eb sb
forall a b. (a -> b) -> a -> b
$
        (WordN (eb + sb)
1 :: WordN (eb + sb)) WordN (eb + sb) -> Int -> WordN (eb + sb)
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
  {-# INLINE fpMinNormalized #-}

  fpMaxNormalized :: FP eb sb
fpMaxNormalized =
    forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$
      WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast (WordN (eb + sb) -> FP eb sb) -> WordN (eb + sb) -> FP eb sb
forall a b. (a -> b) -> a -> b
$
        WordN (eb + sb) -> WordN (eb + sb)
forall a. Bits a => a -> a
complement
          ( (WordN (eb + sb)
1 :: WordN (eb + sb))
              WordN (eb + sb) -> Int -> WordN (eb + sb)
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
          )
          WordN (eb + sb) -> Int -> WordN (eb + sb)
forall a. Bits a => a -> Int -> a
`shiftL` Int
1
          WordN (eb + sb) -> Int -> WordN (eb + sb)
forall a. Bits a => a -> Int -> a
`shiftR` Int
1
  {-# INLINE fpMaxNormalized #-}

  fpMinSubnormal :: FP eb sb
fpMinSubnormal = forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$ WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast (WordN (eb + sb)
1 :: WordN (eb + sb))
  {-# INLINE fpMinSubnormal #-}

  fpMaxSubnormal :: FP eb sb
fpMaxSubnormal =
    forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$
      WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast
        ( (WordN (eb + sb)
1 :: WordN (eb + sb))
            WordN (eb + sb) -> Int -> WordN (eb + sb)
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
            WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Num a => a -> a -> a
- WordN (eb + sb)
1
        )
  {-# INLINE fpMaxSubnormal #-}

cmpHandleNegZero :: (ValidFP eb sb) => FP eb sb -> FP eb sb -> Bool
cmpHandleNegZero :: forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> FP eb sb -> Bool
cmpHandleNegZero FP eb sb
x FP eb sb
y =
  if FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsZero FP eb sb
x Bool -> Bool -> Bool
&& FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsZero FP eb sb
y then FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeZero FP eb sb
x else FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Ord a => a -> a -> Bool
< FP eb sb
y

instance (ValidFP eb sb) => IEEEFPOp (FP eb sb) where
  fpAbs :: FP eb sb -> FP eb sb
fpAbs = FP eb sb -> FP eb sb
forall a. Num a => a -> a
abs
  {-# INLINE fpAbs #-}
  fpNeg :: FP eb sb -> FP eb sb
fpNeg = FP eb sb -> FP eb sb
forall a. Num a => a -> a
negate
  {-# INLINE fpNeg #-}
  fpRem :: FP eb sb -> FP eb sb -> FP eb sb
fpRem = FP eb sb -> FP eb sb -> FP eb sb
forall a. RealFloat a => a -> a -> a
SBVI.fpRemH
  {-# INLINE fpRem #-}
  fpMinimum :: FP eb sb -> FP eb sb -> FP eb sb
fpMinimum FP eb sb
a FP eb sb
b
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
a Bool -> Bool -> Bool
|| FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
b = FP eb sb
forall a. IEEEFPConstants a => a
fpNaN
    | FP eb sb -> FP eb sb -> Bool
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> FP eb sb -> Bool
cmpHandleNegZero FP eb sb
a FP eb sb
b = FP eb sb
a
    | Bool
otherwise = FP eb sb
b
  {-# INLINE fpMinimum #-}
  fpMinimumNumber :: FP eb sb -> FP eb sb -> FP eb sb
fpMinimumNumber FP eb sb
a FP eb sb
b
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
a = FP eb sb
b
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
b = FP eb sb
a
    | FP eb sb -> FP eb sb -> Bool
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> FP eb sb -> Bool
cmpHandleNegZero FP eb sb
a FP eb sb
b = FP eb sb
a
    | Bool
otherwise = FP eb sb
b
  {-# INLINE fpMinimumNumber #-}
  fpMaximum :: FP eb sb -> FP eb sb -> FP eb sb
fpMaximum FP eb sb
a FP eb sb
b
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
a Bool -> Bool -> Bool
|| FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
b = FP eb sb
forall a. IEEEFPConstants a => a
fpNaN
    | FP eb sb -> FP eb sb -> Bool
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> FP eb sb -> Bool
cmpHandleNegZero FP eb sb
a FP eb sb
b = FP eb sb
b
    | Bool
otherwise = FP eb sb
a
  {-# INLINE fpMaximum #-}
  fpMaximumNumber :: FP eb sb -> FP eb sb -> FP eb sb
fpMaximumNumber FP eb sb
a FP eb sb
b
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
a = FP eb sb
b
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
b = FP eb sb
a
    | FP eb sb -> FP eb sb -> Bool
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> FP eb sb -> Bool
cmpHandleNegZero FP eb sb
a FP eb sb
b = FP eb sb
b
    | Bool
otherwise = FP eb sb
a
  {-# INLINE fpMaximumNumber #-}

instance IEEEFPRoundingMode FPRoundingMode where
  rne :: FPRoundingMode
rne = FPRoundingMode
RNE
  {-# INLINE rne #-}
  rna :: FPRoundingMode
rna = FPRoundingMode
RNA
  {-# INLINE rna #-}
  rtp :: FPRoundingMode
rtp = FPRoundingMode
RTP
  {-# INLINE rtp #-}
  rtn :: FPRoundingMode
rtn = FPRoundingMode
RTN
  {-# INLINE rtn #-}
  rtz :: FPRoundingMode
rtz = FPRoundingMode
RTZ
  {-# INLINE rtz #-}

libBFRoundingMode :: FPRoundingMode -> RoundMode
libBFRoundingMode :: FPRoundingMode -> RoundMode
libBFRoundingMode FPRoundingMode
RNE = RoundMode
NearEven
libBFRoundingMode FPRoundingMode
RNA = RoundMode
NearAway
libBFRoundingMode FPRoundingMode
RTP = RoundMode
ToPosInf
libBFRoundingMode FPRoundingMode
RTN = RoundMode
ToNegInf
libBFRoundingMode FPRoundingMode
RTZ = RoundMode
ToZero

libBFOpts ::
  forall eb sb. (ValidFP eb sb) => FPRoundingMode -> FP eb sb -> BFOpts
libBFOpts :: forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPRoundingMode -> FP eb sb -> BFOpts
libBFOpts FPRoundingMode
mode FP eb sb
_ = RoundMode -> BFOpts
rnd RoundMode
rd BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> Word -> BFOpts
precBits Word
sb BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> Int -> BFOpts
expBits Int
eb BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> BFOpts
allowSubnormal
  where
    eb :: Int
eb = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy eb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb) :: Int
    sb :: Word
sb = Natural -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) :: Word
    rd :: RoundMode
rd = FPRoundingMode -> RoundMode
libBFRoundingMode FPRoundingMode
mode

toLibBF :: forall eb sb. (ValidFP eb sb) => FP eb sb -> BigFloat
toLibBF :: forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> BigFloat
toLibBF FP eb sb
f
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeZero FP eb sb
f = BigFloat
bfNegZero
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveZero FP eb sb
f = BigFloat
bfPosZero
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite FP eb sb
f = BigFloat
bfPosInf
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite FP eb sb
f = BigFloat
bfNegInf
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
f = BigFloat
bfNaN
  | Bool
otherwise =
      FP -> BigFloat
SBVF.fpValue (FP -> BigFloat) -> FP -> BigFloat
forall a b. (a -> b) -> a -> b
$
        (Integer -> Int -> FP) -> (Integer, Int) -> FP
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Int -> Int -> Integer -> Int -> FP
fpEncodeFloat Int
eb Int
sb) ((Integer, Int) -> FP) -> (Integer, Int) -> FP
forall a b. (a -> b) -> a -> b
$
          FP eb sb -> (Integer, Int)
forall a. RealFloat a => a -> (Integer, Int)
decodeFloat FP eb sb
f
  where
    eb :: Int
eb = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy eb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb) :: Int
    sb :: Int
sb = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) :: Int

fromLibBF :: forall eb sb. (ValidFP eb sb) => BigFloat -> FP eb sb
fromLibBF :: forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
BigFloat -> FP eb sb
fromLibBF BigFloat
f
  | BigFloat -> Bool
bfIsNeg BigFloat
f Bool -> Bool -> Bool
&& BigFloat -> Bool
bfIsZero BigFloat
f = FP eb sb
forall a. IEEEFPConstants a => a
fpNegativeZero
  | BigFloat -> Bool
bfIsPos BigFloat
f Bool -> Bool -> Bool
&& BigFloat -> Bool
bfIsZero BigFloat
f = FP eb sb
forall a. IEEEFPConstants a => a
fpPositiveZero
  | BigFloat -> Bool
bfIsNeg BigFloat
f Bool -> Bool -> Bool
&& BigFloat -> Bool
bfIsInf BigFloat
f = FP eb sb
forall a. IEEEFPConstants a => a
fpNegativeInfinite
  | BigFloat -> Bool
bfIsPos BigFloat
f Bool -> Bool -> Bool
&& BigFloat -> Bool
bfIsInf BigFloat
f = FP eb sb
forall a. IEEEFPConstants a => a
fpPositiveInfinite
  | BigFloat -> Bool
bfIsNaN BigFloat
f = FP eb sb
forall a. IEEEFPConstants a => a
fpNaN
  | Bool
otherwise = (Integer -> Int -> FP eb sb) -> (Integer, Int) -> FP eb sb
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Integer -> Int -> FP eb sb
forall a. RealFloat a => Integer -> Int -> a
encodeFloat ((Integer, Int) -> FP eb sb) -> (Integer, Int) -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FP -> (Integer, Int)
forall a. RealFloat a => a -> (Integer, Int)
decodeFloat FP
fp
  where
    fp :: FP
fp = Int -> Int -> BigFloat -> FP
SBVF.FP Int
eb Int
sb BigFloat
f
    eb :: Int
eb = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy eb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb) :: Int
    sb :: Int
sb = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) :: Int

liftLibBF1 ::
  (ValidFP eb sb) =>
  (BFOpts -> BigFloat -> (BigFloat, Status)) ->
  FPRoundingMode ->
  FP eb sb ->
  FP eb sb
liftLibBF1 :: forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
(BFOpts -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb
liftLibBF1 BFOpts -> BigFloat -> (BigFloat, Status)
f FPRoundingMode
rd FP eb sb
x = BigFloat -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
BigFloat -> FP eb sb
fromLibBF (BigFloat -> FP eb sb) -> BigFloat -> FP eb sb
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> (BigFloat, Status)
f BFOpts
opts BigFloat
xbf
  where
    opts :: BFOpts
opts = FPRoundingMode -> FP eb sb -> BFOpts
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPRoundingMode -> FP eb sb -> BFOpts
libBFOpts FPRoundingMode
rd FP eb sb
x
    xbf :: BigFloat
xbf = FP eb sb -> BigFloat
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> BigFloat
toLibBF FP eb sb
x

liftLibBF2 ::
  (ValidFP eb sb) =>
  (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) ->
  FPRoundingMode ->
  FP eb sb ->
  FP eb sb ->
  FP eb sb
liftLibBF2 :: forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
liftLibBF2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
f FPRoundingMode
rd FP eb sb
l FP eb sb
r = BigFloat -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
BigFloat -> FP eb sb
fromLibBF (BigFloat -> FP eb sb) -> BigFloat -> FP eb sb
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
f BFOpts
opts BigFloat
lbf BigFloat
rbf
  where
    opts :: BFOpts
opts = FPRoundingMode -> FP eb sb -> BFOpts
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPRoundingMode -> FP eb sb -> BFOpts
libBFOpts FPRoundingMode
rd FP eb sb
l
    lbf :: BigFloat
lbf = FP eb sb -> BigFloat
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> BigFloat
toLibBF FP eb sb
l
    rbf :: BigFloat
rbf = FP eb sb -> BigFloat
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> BigFloat
toLibBF FP eb sb
r

liftLibBF3 ::
  (ValidFP eb sb) =>
  (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)) ->
  FPRoundingMode ->
  FP eb sb ->
  FP eb sb ->
  FP eb sb ->
  FP eb sb
liftLibBF3 :: forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
(BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb -> FP eb sb
liftLibBF3 BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
f FPRoundingMode
rd FP eb sb
x FP eb sb
y FP eb sb
z = BigFloat -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
BigFloat -> FP eb sb
fromLibBF (BigFloat -> FP eb sb) -> BigFloat -> FP eb sb
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
f BFOpts
opts BigFloat
xbf BigFloat
ybf BigFloat
zbf
  where
    opts :: BFOpts
opts = FPRoundingMode -> FP eb sb -> BFOpts
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPRoundingMode -> FP eb sb -> BFOpts
libBFOpts FPRoundingMode
rd FP eb sb
x
    xbf :: BigFloat
xbf = FP eb sb -> BigFloat
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> BigFloat
toLibBF FP eb sb
x
    ybf :: BigFloat
ybf = FP eb sb -> BigFloat
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> BigFloat
toLibBF FP eb sb
y
    zbf :: BigFloat
zbf = FP eb sb -> BigFloat
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> BigFloat
toLibBF FP eb sb
z

instance (ValidFP eb sb) => IEEEFPRoundingOp (FP eb sb) FPRoundingMode where
  fpAdd :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
fpAdd = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
liftLibBF2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfAdd
  {-# INLINE fpAdd #-}
  fpSub :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
fpSub = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
liftLibBF2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfSub
  {-# INLINE fpSub #-}
  fpMul :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
fpMul = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
liftLibBF2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfMul
  {-# INLINE fpMul #-}
  fpDiv :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
fpDiv = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
liftLibBF2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfDiv
  {-# INLINE fpDiv #-}
  fpFMA :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb -> FP eb sb
fpFMA = (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
(BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb -> FP eb sb
liftLibBF3 BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
bfFMA
  {-# INLINE fpFMA #-}
  fpSqrt :: FPRoundingMode -> FP eb sb -> FP eb sb
fpSqrt = (BFOpts -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
(BFOpts -> BigFloat -> (BigFloat, Status))
-> FPRoundingMode -> FP eb sb -> FP eb sb
liftLibBF1 BFOpts -> BigFloat -> (BigFloat, Status)
bfSqrt
  {-# INLINE fpSqrt #-}
  fpRoundToIntegral :: FPRoundingMode -> FP eb sb -> FP eb sb
fpRoundToIntegral FPRoundingMode
rd FP eb sb
x =
    BigFloat -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
BigFloat -> FP eb sb
fromLibBF (BigFloat -> FP eb sb) -> BigFloat -> FP eb sb
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ RoundMode -> BigFloat -> (BigFloat, Status)
bfRoundInt (FPRoundingMode -> RoundMode
libBFRoundingMode FPRoundingMode
rd) (BigFloat -> (BigFloat, Status)) -> BigFloat -> (BigFloat, Status)
forall a b. (a -> b) -> a -> b
$ FP eb sb -> BigFloat
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> BigFloat
toLibBF FP eb sb
x
  {-# INLINE fpRoundToIntegral #-}

instance
  (ValidFP eb sb) =>
  IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode
  where
  fromFPOr :: AlgReal -> FPRoundingMode -> FP eb sb -> AlgReal
fromFPOr AlgReal
d FPRoundingMode
_ FP eb sb
fp
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsInfinite FP eb sb
fp = AlgReal
d
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
fp = AlgReal
d
    | Bool
otherwise =
        let (Integer
m, Int
n) = FP eb sb -> (Integer, Int)
forall a. RealFloat a => a -> (Integer, Int)
decodeFloat FP eb sb
fp
         in Rational -> AlgReal
forall a. Fractional a => Rational -> a
fromRational (Integer -> Rational
forall a. Real a => a -> Rational
toRational Integer
m Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* (Rational
2 Rational -> Int -> Rational
forall a b. (Fractional a, Integral b) => a -> b -> a
^^ Int
n))
  toFP :: FPRoundingMode -> AlgReal -> FP eb sb
toFP FPRoundingMode
mode (AlgExactRational Rational
v) = BigFloat -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
BigFloat -> FP eb sb
fromLibBF (BigFloat -> FP eb sb) -> BigFloat -> FP eb sb
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfDiv BFOpts
opts BigFloat
n BigFloat
d
    where
      opts :: BFOpts
opts = FPRoundingMode -> FP eb sb -> BFOpts
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPRoundingMode -> FP eb sb -> BFOpts
libBFOpts FPRoundingMode
mode (FP eb sb
forall a. HasCallStack => a
undefined :: FP eb sb)
      n :: BigFloat
n = Integer -> BigFloat
bfFromInteger (Integer -> BigFloat) -> Integer -> BigFloat
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a. Ratio a -> a
numerator Rational
v
      d :: BigFloat
d = Integer -> BigFloat
bfFromInteger (Integer -> BigFloat) -> Integer -> BigFloat
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a. Ratio a -> a
denominator Rational
v
  toFP FPRoundingMode
_ AlgReal
r =
    UnsupportedAlgRealOperation -> FP eb sb
forall a e. Exception e => e -> a
throw
      UnsupportedAlgRealOperation {op :: String
op = String
"toFP", msg :: String
msg = AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r}

instance
  (ValidFP eb sb) =>
  IEEEFPToAlgReal AlgReal (FP eb sb) FPRoundingMode

roundRationalToInteger :: FPRoundingMode -> Rational -> Integer
roundRationalToInteger :: FPRoundingMode -> Rational -> Integer
roundRationalToInteger FPRoundingMode
mode Rational
r
  | Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 = Integer
n
  | Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
2 = case FPRoundingMode
mode of
      FPRoundingMode
RNE -> if Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
ndivd then Integer
ndivd else Integer
ndivd Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
      FPRoundingMode
RNA -> if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then Integer
ndivd Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 else Integer
ndivd
      FPRoundingMode
RTP -> Integer
ndivd Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
      FPRoundingMode
RTN -> Integer
ndivd
      FPRoundingMode
RTZ -> if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then Integer
ndivd else Integer
ndivd Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
  | Bool
otherwise = case FPRoundingMode
mode of
      FPRoundingMode
RNE -> if Integer
nmodd Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
d Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2 then Integer
ndivd Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 else Integer
ndivd
      FPRoundingMode
RNA -> if Integer
nmodd Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
d Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2 then Integer
ndivd Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 else Integer
ndivd
      FPRoundingMode
RTP -> Integer
ndivd Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
      FPRoundingMode
RTN -> Integer
ndivd
      FPRoundingMode
RTZ -> if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then Integer
ndivd else Integer
ndivd Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
  where
    n :: Integer
n = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r
    d :: Integer
d = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r
    ndivd :: Integer
ndivd = Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d
    nmodd :: Integer
nmodd = Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
d

instance
  (ValidFP eb sb) =>
  IEEEFPConvertible Integer (FP eb sb) FPRoundingMode
  where
  fromFPOr :: Integer -> FPRoundingMode -> FP eb sb -> Integer
fromFPOr Integer
d FPRoundingMode
mode FP eb sb
fp
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsInfinite FP eb sb
fp = Integer
d
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
fp = Integer
d
    | Bool
otherwise =
        let r :: AlgReal
r = AlgReal -> FPRoundingMode -> FP eb sb -> AlgReal
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr (Integer -> AlgReal
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d) FPRoundingMode
mode FP eb sb
fp
         in case AlgReal
r of
              AlgExactRational Rational
v -> FPRoundingMode -> Rational -> Integer
roundRationalToInteger FPRoundingMode
mode Rational
v
              AlgReal
_ -> String -> Integer
forall a. HasCallStack => String -> a
error String
"Should not happen"
  toFP :: FPRoundingMode -> Integer -> FP eb sb
toFP FPRoundingMode
mode Integer
r = FPRoundingMode -> AlgReal -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
mode (Integer -> AlgReal
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
r :: AlgReal)

instance
  (ValidFP eb sb, KnownNat n, 1 <= n) =>
  IEEEFPConvertible (WordN n) (FP eb sb) FPRoundingMode
  where
  fromFPOr :: WordN n -> FPRoundingMode -> FP eb sb -> WordN n
fromFPOr WordN n
d FPRoundingMode
mode FP eb sb
fp
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsInfinite FP eb sb
fp = WordN n
d
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
fp = WordN n
d
    | Bool
otherwise =
        let p :: Integer
p = Integer -> FPRoundingMode -> FP eb sb -> Integer
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr (WordN n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral WordN n
d :: Integer) FPRoundingMode
mode FP eb sb
fp
         in if Integer
p Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< (WordN n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (WordN n
forall a. Bounded a => a
minBound :: WordN n))
              Bool -> Bool -> Bool
|| Integer
p Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> (WordN n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (WordN n
forall a. Bounded a => a
maxBound :: WordN n))
              then WordN n
d
              else Integer -> WordN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
p
  toFP :: FPRoundingMode -> WordN n -> FP eb sb
toFP FPRoundingMode
mode WordN n
r = FPRoundingMode -> AlgReal -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
mode (WordN n -> AlgReal
forall a b. (Integral a, Num b) => a -> b
fromIntegral WordN n
r :: AlgReal)

instance
  (ValidFP eb sb, KnownNat n, 1 <= n) =>
  IEEEFPConvertible (IntN n) (FP eb sb) FPRoundingMode
  where
  fromFPOr :: IntN n -> FPRoundingMode -> FP eb sb -> IntN n
fromFPOr IntN n
d FPRoundingMode
mode FP eb sb
fp
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsInfinite FP eb sb
fp = IntN n
d
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
fp = IntN n
d
    | Bool
otherwise =
        let p :: Integer
p = Integer -> FPRoundingMode -> FP eb sb -> Integer
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr (IntN n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral IntN n
d :: Integer) FPRoundingMode
mode FP eb sb
fp
         in if Integer
p Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< (IntN n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n
forall a. Bounded a => a
minBound :: IntN n))
              Bool -> Bool -> Bool
|| Integer
p Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> (IntN n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n
forall a. Bounded a => a
maxBound :: IntN n))
              then IntN n
d
              else Integer -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
p
  toFP :: FPRoundingMode -> IntN n -> FP eb sb
toFP FPRoundingMode
mode IntN n
r = FPRoundingMode -> AlgReal -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
mode (IntN n -> AlgReal
forall a b. (Integral a, Num b) => a -> b
fromIntegral IntN n
r :: AlgReal)

instance
  (ValidFP eb sb, ValidFP eb' sb') =>
  IEEEFPConvertible (FP eb' sb') (FP eb sb) FPRoundingMode
  where
  fromFPOr :: FP eb' sb' -> FPRoundingMode -> FP eb sb -> FP eb' sb'
fromFPOr FP eb' sb'
_ = FPRoundingMode -> FP eb sb -> FP eb' sb'
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP
  toFP :: FPRoundingMode -> FP eb' sb' -> FP eb sb
toFP FPRoundingMode
mode FP eb' sb'
fp
    | FP eb' sb' -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite FP eb' sb'
fp = FP eb sb
forall a. IEEEFPConstants a => a
fpNegativeInfinite
    | FP eb' sb' -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite FP eb' sb'
fp = FP eb sb
forall a. IEEEFPConstants a => a
fpPositiveInfinite
    | FP eb' sb' -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb' sb'
fp = FP eb sb
forall a. IEEEFPConstants a => a
fpNaN
    | FP eb' sb' -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeZero FP eb' sb'
fp = FP eb sb
forall a. IEEEFPConstants a => a
fpNegativeZero
    | FP eb' sb' -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveZero FP eb' sb'
fp = FP eb sb
forall a. IEEEFPConstants a => a
fpPositiveZero
    | Bool
otherwise =
        let bffp :: BigFloat
bffp = FP eb' sb' -> BigFloat
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FP eb sb -> BigFloat
toLibBF FP eb' sb'
fp
            opts :: BFOpts
opts = FPRoundingMode -> FP eb sb -> BFOpts
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPRoundingMode -> FP eb sb -> BFOpts
libBFOpts FPRoundingMode
mode (FP eb sb
forall a. HasCallStack => a
undefined :: FP eb sb)
         in BigFloat -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
BigFloat -> FP eb sb
fromLibBF (BigFloat -> FP eb sb) -> BigFloat -> FP eb sb
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> (BigFloat, Status)
bfRoundFloat BFOpts
opts BigFloat
bffp

-- | Next representable floating-point number.
--
-- Note:
--
-- > nextFP(+inf) = +inf
-- > nextFP(-inf) = -maxNormalized
-- > nextFP(NaN) = NaN
--
-- The function do not distinguish between -0 and +0.
nextFP :: forall eb sb. (ValidFP eb sb) => FP eb sb -> FP eb sb
nextFP :: forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
nextFP FP eb sb
x
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
x = FP eb sb
forall a. IEEEFPConstants a => a
fpNaN
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite FP eb sb
x = -FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== -FP eb sb
forall a. IEEEFPConstants a => a
fpMinNormalized = -FP eb sb
forall a. IEEEFPConstants a => a
fpMaxSubnormal
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== -FP eb sb
forall a. IEEEFPConstants a => a
fpMinSubnormal = FP eb sb
0
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
0 = FP eb sb
forall a. IEEEFPConstants a => a
fpMinSubnormal
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
forall a. IEEEFPConstants a => a
fpMaxSubnormal = FP eb sb
forall a. IEEEFPConstants a => a
fpMinNormalized
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized = FP eb sb
forall a. IEEEFPConstants a => a
fpPositiveInfinite
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite FP eb sb
x = FP eb sb
forall a. IEEEFPConstants a => a
fpPositiveInfinite
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Ord a => a -> a -> Bool
> FP eb sb
0 =
      forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$
        WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast ((FP eb sb -> WordN (eb + sb)
forall from to. BitCastOrCanonical from to => from -> to
bitCastOrCanonical FP eb sb
x :: WordN (eb + sb)) WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Num a => a -> a -> a
+ WordN (eb + sb)
1)
  | Bool
otherwise =
      forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$
        WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast ((FP eb sb -> WordN (eb + sb)
forall from to. BitCastOrCanonical from to => from -> to
bitCastOrCanonical FP eb sb
x :: WordN (eb + sb)) WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Num a => a -> a -> a
- WordN (eb + sb)
1)

-- | Previous representable floating-point number.
--
-- Note:
--
-- > prevFP(+inf) = +maxNormalized
-- > prevFP(-inf) = -inf
-- > prevFP(NaN) = NaN
--
-- The function do not distinguish between -0 and +0.
prevFP :: forall eb sb. (ValidFP eb sb) => FP eb sb -> FP eb sb
prevFP :: forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP FP eb sb
x
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
x = FP eb sb
forall a. IEEEFPConstants a => a
fpNaN
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite FP eb sb
x = FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
forall a. IEEEFPConstants a => a
fpMinNormalized = FP eb sb
forall a. IEEEFPConstants a => a
fpMaxSubnormal
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
forall a. IEEEFPConstants a => a
fpMinSubnormal = FP eb sb
0
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
0 = -FP eb sb
forall a. IEEEFPConstants a => a
fpMinSubnormal
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== -FP eb sb
forall a. IEEEFPConstants a => a
fpMaxSubnormal = -FP eb sb
forall a. IEEEFPConstants a => a
fpMinNormalized
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== -FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized = FP eb sb
forall a. IEEEFPConstants a => a
fpNegativeInfinite
  | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite FP eb sb
x = FP eb sb
forall a. IEEEFPConstants a => a
fpNegativeInfinite
  | FP eb sb
x FP eb sb -> FP eb sb -> Bool
forall a. Ord a => a -> a -> Bool
> FP eb sb
0 =
      forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$
        WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast ((FP eb sb -> WordN (eb + sb)
forall from to. BitCastOrCanonical from to => from -> to
bitCastOrCanonical FP eb sb
x :: WordN (eb + sb)) WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Num a => a -> a -> a
- WordN (eb + sb)
1)
  | Bool
otherwise =
      forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$
        WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast ((FP eb sb -> WordN (eb + sb)
forall from to. BitCastOrCanonical from to => from -> to
bitCastOrCanonical FP eb sb
x :: WordN (eb + sb)) WordN (eb + sb) -> WordN (eb + sb) -> WordN (eb + sb)
forall a. Num a => a -> a -> a
+ WordN (eb + sb)
1)

-- | Bounds for converting bit vectors to floating-point numbers. Out-of-range
-- FP values cannot be converted to a representable bit-vector.
class ConvertibleBound bv where
  convertibleLowerBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    bv n ->
    FPRoundingMode ->
    FP eb sb
  convertibleUpperBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    bv n ->
    FPRoundingMode ->
    FP eb sb

instance ConvertibleBound WordN where
  convertibleLowerBound :: forall (eb :: Natural) (sb :: Natural) (n :: Natural).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
WordN n -> FPRoundingMode -> FP eb sb
convertibleLowerBound WordN n
_ FPRoundingMode
RTP = FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
nextFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ -FP eb sb
1
  convertibleLowerBound WordN n
_ FPRoundingMode
RTZ = FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
nextFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ -FP eb sb
1
  convertibleLowerBound WordN n
_ FPRoundingMode
RTN = FP eb sb
0
  convertibleLowerBound WordN n
_ FPRoundingMode
RNA = FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
nextFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ -FP eb sb
0.5
  convertibleLowerBound WordN n
_ FPRoundingMode
RNE = -FP eb sb
0.5
  convertibleUpperBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    WordN n ->
    FPRoundingMode ->
    FP eb sb
  convertibleUpperBound :: forall (eb :: Natural) (sb :: Natural) (n :: Natural).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
WordN n -> FPRoundingMode -> FP eb sb
convertibleUpperBound WordN n
_ FPRoundingMode
mode
    | Natural
ebn Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n = FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized
    | Natural
ebn Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n Bool -> Bool -> Bool
&& Natural
sb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
n = FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized
    | Natural
ebn Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
n Bool -> Bool -> Bool
&& Natural
sb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
n = case FPRoundingMode
mode of
        FPRoundingMode
RTP -> FPRoundingMode -> WordN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (WordN n
forall a. Bounded a => a
maxBound :: WordN n)
        FPRoundingMode
RTZ -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> WordN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (WordN n
forall a. Bounded a => a
maxBound :: WordN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
+ FP eb sb
1
        FPRoundingMode
RTN -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> WordN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (WordN n
forall a. Bounded a => a
maxBound :: WordN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
+ FP eb sb
1
        FPRoundingMode
RNA -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> WordN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (WordN n
forall a. Bounded a => a
maxBound :: WordN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
+ FP eb sb
0.5
        FPRoundingMode
RNE -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> WordN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (WordN n
forall a. Bounded a => a
maxBound :: WordN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
+ FP eb sb
0.5
    | Natural
ebn Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
n Bool -> Bool -> Bool
&& Natural
sb Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n = FPRoundingMode -> WordN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (WordN n
forall a. Bounded a => a
maxBound :: WordN n)
    -- ebn > n && sb < n
    | Bool
otherwise =
        FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> WordN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (WordN n
forall a. Bounded a => a
maxBound WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
`div` WordN n
2 WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
+ WordN n
1 :: WordN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
* FP eb sb
2
    where
      n :: Natural
n = Proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      eb :: Natural
eb = Proxy eb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb)
      ebn :: Natural
ebn = Natural
2 Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ (Natural
eb Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
      sb :: Natural
sb = Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb)

instance ConvertibleBound IntN where
  convertibleLowerBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    IntN n ->
    FPRoundingMode ->
    FP eb sb
  convertibleLowerBound :: forall (eb :: Natural) (sb :: Natural) (n :: Natural).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
IntN n -> FPRoundingMode -> FP eb sb
convertibleLowerBound IntN n
_ FPRoundingMode
mode
    | Natural
ebn Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 = -FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized
    | Natural
ebn Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 Bool -> Bool -> Bool
&& Natural
sb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 = FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
minBound :: IntN n)
    -- ebn > n - 1 && sb > n - 1
    | Bool
otherwise = case FPRoundingMode
mode of
        FPRoundingMode
RTP -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
nextFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
minBound :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
- FP eb sb
1
        FPRoundingMode
RTZ -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
nextFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
minBound :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
- FP eb sb
1
        FPRoundingMode
RTN -> FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
minBound :: IntN n)
        FPRoundingMode
RNA ->
          if Natural
sb Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n
            then FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
minBound :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
- FP eb sb
0.5
            else FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
nextFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
minBound :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
- FP eb sb
0.5
        FPRoundingMode
RNE -> FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
minBound :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
- FP eb sb
0.5
    where
      n :: Natural
n = Proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      eb :: Natural
eb = Proxy eb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb)
      ebn :: Natural
ebn = Natural
2 Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ (Natural
eb Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
      sb :: Natural
sb = Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb)
  convertibleUpperBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    IntN n ->
    FPRoundingMode ->
    FP eb sb
  convertibleUpperBound :: forall (eb :: Natural) (sb :: Natural) (n :: Natural).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
IntN n -> FPRoundingMode -> FP eb sb
convertibleUpperBound IntN n
_ FPRoundingMode
mode
    | Natural
ebn Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 = FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized
    | Natural
ebn Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 Bool -> Bool -> Bool
&& Natural
sb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 = FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized
    | Natural
ebn Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 Bool -> Bool -> Bool
&& Natural
sb Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 = case FPRoundingMode
mode of
        FPRoundingMode
RTP -> FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
maxBound :: IntN n)
        FPRoundingMode
RTZ -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
maxBound :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
+ FP eb sb
1
        FPRoundingMode
RTN -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
maxBound :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
+ FP eb sb
1
        FPRoundingMode
RNA -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
maxBound :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
+ FP eb sb
0.5
        FPRoundingMode
RNE -> FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
maxBound :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
+ FP eb sb
0.5
    | Natural
ebn Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 Bool -> Bool -> Bool
&& Natural
sb Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 = FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
maxBound :: IntN n)
    -- ebn > n - 1 && sb < n - 1
    | Bool
otherwise =
        FP eb sb -> FP eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFloat eb sb =>
FP eb sb -> FP eb sb
prevFP (FP eb sb -> FP eb sb) -> FP eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> IntN n -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne (IntN n
forall a. Bounded a => a
maxBound IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
`div` IntN n
2 IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ IntN n
1 :: IntN n) FP eb sb -> FP eb sb -> FP eb sb
forall a. Num a => a -> a -> a
* FP eb sb
2
    where
      n :: Natural
n = Proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      eb :: Natural
eb = Proxy eb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb)
      ebn :: Natural
ebn = Natural
2 Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ (Natural
eb Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
      sb :: Natural
sb = Proxy sb -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb)

instance Apply (FP eb sb) where
  type FunType (FP eb sb) = FP eb sb
  apply :: FP eb sb -> FunType (FP eb sb)
apply = FP eb sb -> FunType (FP eb sb)
FP eb sb -> FP eb sb
forall a. a -> a
id

instance Apply FPRoundingMode where
  type FunType FPRoundingMode = FPRoundingMode
  apply :: FPRoundingMode -> FunType FPRoundingMode
apply = FPRoundingMode -> FunType FPRoundingMode
FPRoundingMode -> FPRoundingMode
forall a. a -> a
id

instance (ValidFP eb sb) => Serial (FP eb sb) where
  serialize :: forall (m :: * -> *). MonadPut m => FP eb sb -> m ()
serialize FP eb sb
x =
    forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  m ())
 -> m ())
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    m ())
-> m ()
forall a b. (a -> b) -> a -> b
$
      WordN (eb + sb) -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => WordN (eb + sb) -> m ()
serialize (FP eb sb -> WordN (eb + sb)
forall from to. BitCastOrCanonical from to => from -> to
bitCastOrCanonical FP eb sb
x :: WordN (eb + sb))
  deserialize :: forall (m :: * -> *). MonadGet m => m (FP eb sb)
deserialize = do
    WordN (eb + sb)
w :: WordN (eb + sb) <- forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb m (WordN (eb + sb))
(KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
 1 <= eb, 1 <= sb) =>
m (WordN (eb + sb))
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (WordN (eb + sb))
deserialize
    FP eb sb -> m (FP eb sb)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FP eb sb -> m (FP eb sb)) -> FP eb sb -> m (FP eb sb)
forall a b. (a -> b) -> a -> b
$ forall (eb :: Natural) (sb :: Natural) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  FP eb sb)
 -> FP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$ WordN (eb + sb) -> FP eb sb
forall from to. BitCast from to => from -> to
bitCast WordN (eb + sb)
w

instance (ValidFP eb sb) => Cereal.Serialize (FP eb sb) where
  put :: Putter (FP eb sb)
put = Putter (FP eb sb)
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FP eb sb -> m ()
serialize
  get :: Get (FP eb sb)
get = Get (FP eb sb)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (FP eb sb)
deserialize

instance (ValidFP eb sb) => Binary.Binary (FP eb sb) where
  put :: FP eb sb -> Put
put = FP eb sb -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => FP eb sb -> m ()
serialize
  get :: Get (FP eb sb)
get = Get (FP eb sb)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (FP eb sb)
deserialize