{-# Language DataKinds #-}
{-# Language FlexibleContexts #-}
{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language TypeOperators #-}

-- | Working with floats of dynamic sizes.
module What4.SFloat
  ( -- * Interface
    SFloat(..)
  , fpReprOf
  , fpSize
  , fpRepr
  , fpAsLit
  , fpIte

    -- * Constants
  , fpFresh
  , fpNaN
  , fpPosInf
  , fpNegInf
  , fpFromLit
  , fpFromRationalLit

    -- * Interchange formats
  , fpFromBinary
  , fpToBinary

    -- * Relations
  , SFloatRel
  , fpEq
  , fpEqIEEE
  , fpLtIEEE
  , fpGtIEEE

    -- * Arithmetic
  , SFloatBinArith
  , fpNeg
  , fpAbs
  , fpSqrt
  , fpAdd
  , fpSub
  , fpMul
  , fpDiv
  , fpMin
  , fpMax
  , fpFMA

    -- * Conversions
  , fpRound
  , fpToReal
  , fpFromReal
  , fpFromRational
  , fpToRational
  , fpFromInteger

    -- * Queries
  , fpIsInf
  , fpIsNaN
  , fpIsZero
  , fpIsNeg
  , fpIsSubnorm
  , fpIsNorm

  -- * Exceptions
  , UnsupportedFloat(..)
  , FPTypeError(..)
  ) where

import Control.Exception
import LibBF (BigFloat)

import Data.Parameterized.Some
import Data.Parameterized.NatRepr

import What4.BaseTypes
import What4.Panic(panic)
import What4.SWord
import What4.Interface

-- | Symbolic floating point numbers.
data SFloat sym where
  SFloat :: IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym



--------------------------------------------------------------------------------

-- | This exception is thrown if the operations try to create a
-- floating point value we do not support
data UnsupportedFloat =
  UnsupportedFloat { UnsupportedFloat -> String
fpWho :: String, UnsupportedFloat -> Integer
exponentBits, UnsupportedFloat -> Integer
precisionBits :: Integer }
  deriving Int -> UnsupportedFloat -> ShowS
[UnsupportedFloat] -> ShowS
UnsupportedFloat -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnsupportedFloat] -> ShowS
$cshowList :: [UnsupportedFloat] -> ShowS
show :: UnsupportedFloat -> String
$cshow :: UnsupportedFloat -> String
showsPrec :: Int -> UnsupportedFloat -> ShowS
$cshowsPrec :: Int -> UnsupportedFloat -> ShowS
Show


-- | Throw 'UnsupportedFloat' exception
unsupported ::
  String  {- ^ Label -} ->
  Integer {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  IO a
unsupported :: forall a. String -> Integer -> Integer -> IO a
unsupported String
l Integer
e Integer
p =
  forall e a. Exception e => e -> IO a
throwIO UnsupportedFloat { fpWho :: String
fpWho         = String
l
                           , exponentBits :: Integer
exponentBits  = Integer
e
                           , precisionBits :: Integer
precisionBits = Integer
p }

instance Exception UnsupportedFloat

-- | This exceptoin is throws if the types don't match.
data FPTypeError =
  FPTypeError { FPTypeError -> Some BaseTypeRepr
fpExpected :: Some BaseTypeRepr
              , FPTypeError -> Some BaseTypeRepr
fpActual   :: Some BaseTypeRepr
              }
    deriving Int -> FPTypeError -> ShowS
[FPTypeError] -> ShowS
FPTypeError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FPTypeError] -> ShowS
$cshowList :: [FPTypeError] -> ShowS
show :: FPTypeError -> String
$cshow :: FPTypeError -> String
showsPrec :: Int -> FPTypeError -> ShowS
$cshowsPrec :: Int -> FPTypeError -> ShowS
Show

instance Exception FPTypeError

fpTypeMismatch :: BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
fpTypeMismatch :: forall (t1 :: BaseType) (t2 :: BaseType) a.
BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
fpTypeMismatch BaseTypeRepr t1
expect BaseTypeRepr t2
actual =
  forall e a. Exception e => e -> IO a
throwIO FPTypeError { fpExpected :: Some BaseTypeRepr
fpExpected = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr t1
expect
                      , fpActual :: Some BaseTypeRepr
fpActual   = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr t2
actual
                      }
fpTypeError :: FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError :: forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError FloatPrecisionRepr t1
t1 FloatPrecisionRepr t2
t2 =
  forall (t1 :: BaseType) (t2 :: BaseType) a.
BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
fpTypeMismatch (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr t1
t1) (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr t2
t2)


--------------------------------------------------------------------------------
-- | Construct the 'FloatPrecisionRepr' with the given parameters.
fpRepr ::
  Integer {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  Maybe (Some FloatPrecisionRepr)
fpRepr :: Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpRepr Integer
iE Integer
iP =
  do Some NatRepr x
e    <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
iE
     LeqProof 2 x
LeqProof  <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @2) NatRepr x
e
     Some NatRepr x
p    <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
iP
     LeqProof 2 x
LeqProof  <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @2) NatRepr x
p
     forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (eb :: Nat) (sb :: Nat).
(2 <= eb, 2 <= sb) =>
NatRepr eb
-> NatRepr sb -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
FloatingPointPrecisionRepr NatRepr x
e NatRepr x
p))

fpReprOf ::
  IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
fpReprOf :: forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
fpReprOf sym
_ SymFloat sym fpp
e =
  case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymFloat sym fpp
e of
    BaseFloatRepr FloatPrecisionRepr fpp
r -> FloatPrecisionRepr fpp
r

fpSize :: SFloat sym -> (Integer,Integer)
fpSize :: forall sym. SFloat sym -> (Integer, Integer)
fpSize (SFloat SymFloat sym fpp
f) =
  case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymFloat sym fpp
f of
    BaseFloatRepr (FloatingPointPrecisionRepr NatRepr eb
e NatRepr sb
p) -> (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr eb
e, forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr sb
p)

fpAsLit :: SFloat sym -> Maybe BigFloat
fpAsLit :: forall sym. SFloat sym -> Maybe BigFloat
fpAsLit (SFloat SymFloat sym fpp
f) = forall (e :: BaseType -> Type) (fpp :: FloatPrecision).
IsExpr e =>
e (BaseFloatType fpp) -> Maybe BigFloat
asFloat SymFloat sym fpp
f

--------------------------------------------------------------------------------
-- Constants

-- | A fresh variable of the given type.
fpFresh ::
  IsSymExprBuilder sym =>
  sym ->
  Integer ->
  Integer ->
  IO (SFloat sym)
fpFresh :: forall sym.
IsSymExprBuilder sym =>
sym -> Integer -> Integer -> IO (SFloat sym)
fpFresh sym
sym Integer
e Integer
p
  | Just (Some FloatPrecisionRepr x
fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpRepr Integer
e Integer
p =
    forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
emptySymbol (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr x
fpp)
  | Bool
otherwise = forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpFresh" Integer
e Integer
p

-- | Not a number
fpNaN ::
  IsExprBuilder sym =>
  sym ->
  Integer {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  IO (SFloat sym)
fpNaN :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SFloat sym)
fpNaN sym
sym Integer
e Integer
p
  | Just (Some FloatPrecisionRepr x
fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpRepr Integer
e Integer
p = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatNaN sym
sym FloatPrecisionRepr x
fpp
  | Bool
otherwise = forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpNaN" Integer
e Integer
p


-- | Positive infinity
fpPosInf ::
  IsExprBuilder sym =>
  sym ->
  Integer {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  IO (SFloat sym)
fpPosInf :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SFloat sym)
fpPosInf sym
sym Integer
e Integer
p
  | Just (Some FloatPrecisionRepr x
fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpRepr Integer
e Integer
p = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatPInf sym
sym FloatPrecisionRepr x
fpp
  | Bool
otherwise = forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpPosInf" Integer
e Integer
p

-- | Negative infinity
fpNegInf ::
  IsExprBuilder sym =>
  sym ->
  Integer {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  IO (SFloat sym)
fpNegInf :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SFloat sym)
fpNegInf sym
sym Integer
e Integer
p
  | Just (Some FloatPrecisionRepr x
fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpRepr Integer
e Integer
p = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatNInf sym
sym FloatPrecisionRepr x
fpp
  | Bool
otherwise = forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpNegInf" Integer
e Integer
p


-- | A floating point number corresponding to the given BigFloat.
fpFromLit ::
  IsExprBuilder sym =>
  sym ->
  Integer {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  BigFloat ->
  IO (SFloat sym)
fpFromLit :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> BigFloat -> IO (SFloat sym)
fpFromLit sym
sym Integer
e Integer
p BigFloat
f
  | Just (Some FloatPrecisionRepr x
fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpRepr Integer
e Integer
p = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
floatLit sym
sym FloatPrecisionRepr x
fpp BigFloat
f
  | Bool
otherwise = forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpFromLit" Integer
e Integer
p

-- | A floating point number corresponding to the given rational.
fpFromRationalLit ::
  IsExprBuilder sym =>
  sym ->
  Integer {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  Rational ->
  IO (SFloat sym)
fpFromRationalLit :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> Rational -> IO (SFloat sym)
fpFromRationalLit sym
sym Integer
e Integer
p Rational
r
  | Just (Some FloatPrecisionRepr x
fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpRepr Integer
e Integer
p = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat sym fpp)
floatLitRational sym
sym FloatPrecisionRepr x
fpp Rational
r
  | Bool
otherwise = forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpFromRationalLit" Integer
e Integer
p


-- | Make a floating point number with the given bit representation.
fpFromBinary ::
  IsExprBuilder sym =>
  sym ->
  Integer {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  SWord sym ->
  IO (SFloat sym)
fpFromBinary :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
fpFromBinary sym
sym Integer
e Integer
p SWord sym
swe
  | DBV SymBV sym w
sw <- SWord sym
swe
  , Just (Some FloatPrecisionRepr x
fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpRepr Integer
e Integer
p
  , FloatingPointPrecisionRepr NatRepr eb
ew NatRepr sb
pw <- FloatPrecisionRepr x
fpp
  , let expectW :: NatRepr (eb + sb)
expectW = forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr eb
ew NatRepr sb
pw
  , actual :: BaseTypeRepr (BaseBVType w)
actual@(BaseBVRepr NatRepr w
actualW)  <- forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymBV sym w
sw =
    case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr (eb + sb)
expectW NatRepr w
actualW of
      Just (eb + sb) :~: w
Refl -> forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> SymBV sym (eb + sb)
-> IO (SymFloat sym (FloatingPointPrecision eb sb))
floatFromBinary sym
sym FloatPrecisionRepr x
fpp SymBV sym w
sw
      Maybe ((eb + sb) :~: w)
Nothing -- we want to report type correct type errors! :-)
        | Just LeqProof 1 (eb + sb)
LeqProof <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr (eb + sb)
expectW ->
                forall (t1 :: BaseType) (t2 :: BaseType) a.
BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
fpTypeMismatch (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr (eb + sb)
expectW) BaseTypeRepr (BaseBVType w)
actual
        | Bool
otherwise -> forall a. HasCallStack => String -> [String] -> a
panic String
"fpFromBits" [ String
"1 >= 2" ]
  | Bool
otherwise = forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpFromBits" Integer
e Integer
p

fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym)
fpToBinary :: forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SWord sym)
fpToBinary sym
sym (SFloat SymFloat sym fpp
f)
  | FloatingPointPrecisionRepr NatRepr eb
e NatRepr sb
p <- forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
fpReprOf sym
sym SymFloat sym fpp
f
  , Just LeqProof 1 (eb + sb)
LeqProof <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) (forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr eb
e NatRepr sb
p)
    = forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> SymFloat sym (FloatingPointPrecision eb sb)
-> IO (SymBV sym (eb + sb))
floatToBinary sym
sym SymFloat sym fpp
f
  | Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"fpToBinary" [ String
"we messed up the types" ]


--------------------------------------------------------------------------------
-- Arithmetic

fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
fpNeg :: forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SFloat sym)
fpNeg sym
sym (SFloat SymFloat sym fpp
fl) = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
floatNeg sym
sym SymFloat sym fpp
fl

fpAbs :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
fpAbs :: forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SFloat sym)
fpAbs sym
sym (SFloat SymFloat sym fpp
fl) = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
floatAbs sym
sym SymFloat sym fpp
fl

fpSqrt :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpSqrt :: forall sym.
IsExprBuilder sym =>
sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpSqrt sym
sym RoundingMode
r (SFloat SymFloat sym fpp
fl) = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
floatSqrt sym
sym RoundingMode
r SymFloat sym fpp
fl

fpBinArith ::
  IsExprBuilder sym =>
  (forall t.
      sym ->
      RoundingMode ->
      SymFloat sym t ->
      SymFloat sym t ->
      IO (SymFloat sym t)
  ) ->
  sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpBinArith :: forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym
 -> RoundingMode
 -> SymFloat sym t
 -> SymFloat sym t
 -> IO (SymFloat sym t))
-> sym
-> RoundingMode
-> SFloat sym
-> SFloat sym
-> IO (SFloat sym)
fpBinArith forall (t :: FloatPrecision).
sym
-> RoundingMode
-> SymFloat sym t
-> SymFloat sym t
-> IO (SymFloat sym t)
fun sym
sym RoundingMode
r (SFloat SymFloat sym fpp
x) (SFloat SymFloat sym fpp
y) =
  let t1 :: FloatPrecisionRepr fpp
t1 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
x
      t2 :: FloatPrecisionRepr fpp
t2 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
y
  in
  case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2 of
    Just fpp :~: fpp
Refl -> forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: FloatPrecision).
sym
-> RoundingMode
-> SymFloat sym t
-> SymFloat sym t
-> IO (SymFloat sym t)
fun sym
sym RoundingMode
r SymFloat sym fpp
x SymFloat sym fpp
y
    Maybe (fpp :~: fpp)
_         -> forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2

type SFloatBinArith sym =
  sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)

fpAdd :: IsExprBuilder sym => SFloatBinArith sym
fpAdd :: forall sym. IsExprBuilder sym => SFloatBinArith sym
fpAdd = forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym
 -> RoundingMode
 -> SymFloat sym t
 -> SymFloat sym t
 -> IO (SymFloat sym t))
-> sym
-> RoundingMode
-> SFloat sym
-> SFloat sym
-> IO (SFloat sym)
fpBinArith forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatAdd

fpSub :: IsExprBuilder sym => SFloatBinArith sym
fpSub :: forall sym. IsExprBuilder sym => SFloatBinArith sym
fpSub = forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym
 -> RoundingMode
 -> SymFloat sym t
 -> SymFloat sym t
 -> IO (SymFloat sym t))
-> sym
-> RoundingMode
-> SFloat sym
-> SFloat sym
-> IO (SFloat sym)
fpBinArith forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatSub

fpMul :: IsExprBuilder sym => SFloatBinArith sym
fpMul :: forall sym. IsExprBuilder sym => SFloatBinArith sym
fpMul = forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym
 -> RoundingMode
 -> SymFloat sym t
 -> SymFloat sym t
 -> IO (SymFloat sym t))
-> sym
-> RoundingMode
-> SFloat sym
-> SFloat sym
-> IO (SFloat sym)
fpBinArith forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatMul

fpDiv :: IsExprBuilder sym => SFloatBinArith sym
fpDiv :: forall sym. IsExprBuilder sym => SFloatBinArith sym
fpDiv = forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym
 -> RoundingMode
 -> SymFloat sym t
 -> SymFloat sym t
 -> IO (SymFloat sym t))
-> sym
-> RoundingMode
-> SFloat sym
-> SFloat sym
-> IO (SFloat sym)
fpBinArith forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatDiv

fpMin :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpMin :: forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpMin sym
sym (SFloat SymFloat sym fpp
x) (SFloat SymFloat sym fpp
y) =
  let t1 :: FloatPrecisionRepr fpp
t1 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
x
      t2 :: FloatPrecisionRepr fpp
t2 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
y
  in
  case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2 of
    Just fpp :~: fpp
Refl -> forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
floatMin sym
sym SymFloat sym fpp
x SymFloat sym fpp
y
    Maybe (fpp :~: fpp)
_         -> forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2

fpMax :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpMax :: forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpMax sym
sym (SFloat SymFloat sym fpp
x) (SFloat SymFloat sym fpp
y) =
  let t1 :: FloatPrecisionRepr fpp
t1 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
x
      t2 :: FloatPrecisionRepr fpp
t2 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
y
  in
  case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2 of
    Just fpp :~: fpp
Refl -> forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
floatMax sym
sym SymFloat sym fpp
x SymFloat sym fpp
y
    Maybe (fpp :~: fpp)
_         -> forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2

fpFMA :: IsExprBuilder sym =>
  sym -> RoundingMode -> SFloat sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpFMA :: forall sym.
IsExprBuilder sym =>
sym
-> RoundingMode
-> SFloat sym
-> SFloat sym
-> SFloat sym
-> IO (SFloat sym)
fpFMA sym
sym RoundingMode
r (SFloat SymFloat sym fpp
x) (SFloat SymFloat sym fpp
y) (SFloat SymFloat sym fpp
z) =
  let t1 :: FloatPrecisionRepr fpp
t1 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
x
      t2 :: FloatPrecisionRepr fpp
t2 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
y
      t3 :: FloatPrecisionRepr fpp
t3 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
z
   in
   case (forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2, forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
t2 FloatPrecisionRepr fpp
t3) of
     (Just fpp :~: fpp
Refl, Just fpp :~: fpp
Refl) -> forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatFMA sym
sym RoundingMode
r SymFloat sym fpp
x SymFloat sym fpp
y SymFloat sym fpp
z
     (Maybe (fpp :~: fpp)
Nothing, Maybe (fpp :~: fpp)
_) -> forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2
     (Maybe (fpp :~: fpp)
_, Maybe (fpp :~: fpp)
Nothing) -> forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError FloatPrecisionRepr fpp
t2 FloatPrecisionRepr fpp
t3

fpIte :: IsExprBuilder sym =>
  sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpIte :: forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpIte sym
sym Pred sym
p (SFloat SymFloat sym fpp
x) (SFloat SymFloat sym fpp
y) =
  let t1 :: FloatPrecisionRepr fpp
t1 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
x
      t2 :: FloatPrecisionRepr fpp
t2 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
y
  in
  case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2 of
    Just fpp :~: fpp
Refl -> forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatIte sym
sym Pred sym
p SymFloat sym fpp
x SymFloat sym fpp
y
    Maybe (fpp :~: fpp)
_         -> forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2

--------------------------------------------------------------------------------

fpRel ::
  IsExprBuilder sym =>
  (forall t.
    sym ->
    SymFloat sym t ->
    SymFloat sym t ->
    IO (Pred sym)
  ) ->
  sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
fpRel :: forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
-> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
fpRel forall (t :: FloatPrecision).
sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym)
fun sym
sym (SFloat SymFloat sym fpp
x) (SFloat SymFloat sym fpp
y) =
  let t1 :: FloatPrecisionRepr fpp
t1 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
x
      t2 :: FloatPrecisionRepr fpp
t2 = sym
sym forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
y
  in
  case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2 of
    Just fpp :~: fpp
Refl -> forall (t :: FloatPrecision).
sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym)
fun sym
sym SymFloat sym fpp
x SymFloat sym fpp
y
    Maybe (fpp :~: fpp)
_         -> forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError FloatPrecisionRepr fpp
t1 FloatPrecisionRepr fpp
t2




type SFloatRel sym =
  sym -> SFloat sym -> SFloat sym -> IO (Pred sym)

fpEq :: IsExprBuilder sym => SFloatRel sym
fpEq :: forall sym. IsExprBuilder sym => SFloatRel sym
fpEq = forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
-> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
fpRel forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
floatEq

fpEqIEEE :: IsExprBuilder sym => SFloatRel sym
fpEqIEEE :: forall sym. IsExprBuilder sym => SFloatRel sym
fpEqIEEE = forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
-> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
fpRel forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
floatFpEq

fpLtIEEE :: IsExprBuilder sym => SFloatRel sym
fpLtIEEE :: forall sym. IsExprBuilder sym => SFloatRel sym
fpLtIEEE = forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
-> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
fpRel forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
floatLt

fpGtIEEE :: IsExprBuilder sym => SFloatRel sym
fpGtIEEE :: forall sym. IsExprBuilder sym => SFloatRel sym
fpGtIEEE = forall sym.
IsExprBuilder sym =>
(forall (t :: FloatPrecision).
 sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
-> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
fpRel forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
floatGt


--------------------------------------------------------------------------------
fpRound ::
  IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpRound :: forall sym.
IsExprBuilder sym =>
sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpRound sym
sym RoundingMode
r (SFloat SymFloat sym fpp
x) = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
floatRound sym
sym RoundingMode
r SymFloat sym fpp
x

-- | This is undefined on "special" values (NaN,infinity)
fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym)
fpToReal :: forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SymReal sym)
fpToReal sym
sym (SFloat SymFloat sym fpp
x) = forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
floatToReal sym
sym SymFloat sym fpp
x

fpFromReal ::
  IsExprBuilder sym =>
  sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym)
fpFromReal :: forall sym.
IsExprBuilder sym =>
sym
-> Integer
-> Integer
-> RoundingMode
-> SymReal sym
-> IO (SFloat sym)
fpFromReal sym
sym Integer
e Integer
p RoundingMode
r SymReal sym
x
  | Just (Some FloatPrecisionRepr x
repr) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpRepr Integer
e Integer
p = forall sym (w :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym w -> SFloat sym
SFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
realToFloat sym
sym FloatPrecisionRepr x
repr RoundingMode
r SymReal sym
x
  | Bool
otherwise = forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpFromReal" Integer
e Integer
p


fpFromInteger ::
  IsExprBuilder sym =>
  sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym)
fpFromInteger :: forall sym.
IsExprBuilder sym =>
sym
-> Integer
-> Integer
-> RoundingMode
-> SymInteger sym
-> IO (SFloat sym)
fpFromInteger sym
sym Integer
e Integer
p RoundingMode
r SymInteger sym
x = forall sym.
IsExprBuilder sym =>
sym
-> Integer
-> Integer
-> RoundingMode
-> SymReal sym
-> IO (SFloat sym)
fpFromReal sym
sym Integer
e Integer
p RoundingMode
r forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
x


fpFromRational ::
  IsExprBuilder sym =>
  sym -> Integer -> Integer -> RoundingMode ->
  SymInteger sym -> SymInteger sym -> IO (SFloat sym)
fpFromRational :: forall sym.
IsExprBuilder sym =>
sym
-> Integer
-> Integer
-> RoundingMode
-> SymInteger sym
-> SymInteger sym
-> IO (SFloat sym)
fpFromRational sym
sym Integer
e Integer
p RoundingMode
r SymInteger sym
x SymInteger sym
y =
  do SymExpr sym BaseRealType
num <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
x
     SymExpr sym BaseRealType
den <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
y
     SymExpr sym BaseRealType
res <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym BaseRealType
num SymExpr sym BaseRealType
den
     forall sym.
IsExprBuilder sym =>
sym
-> Integer
-> Integer
-> RoundingMode
-> SymReal sym
-> IO (SFloat sym)
fpFromReal sym
sym Integer
e Integer
p RoundingMode
r SymExpr sym BaseRealType
res

{- | Returns a predicate and two integers, @x@ and @y@.
If the the predicate holds, then @x / y@ is a rational representing
the floating point number. Assumes the FP number is not one of the
special ones that has no real representation. -}
fpToRational ::
  IsSymExprBuilder sym =>
  sym ->
  SFloat sym ->
  IO (Pred sym, SymInteger sym, SymInteger sym)
fpToRational :: forall sym.
IsSymExprBuilder sym =>
sym -> SFloat sym -> IO (Pred sym, SymInteger sym, SymInteger sym)
fpToRational sym
sym SFloat sym
fp =
  do SymExpr sym BaseRealType
r    <- forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SymReal sym)
fpToReal sym
sym SFloat sym
fp
     SymInteger sym
x    <- forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
emptySymbol BaseTypeRepr 'BaseIntegerType
BaseIntegerRepr
     SymInteger sym
y    <- forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
emptySymbol BaseTypeRepr 'BaseIntegerType
BaseIntegerRepr
     SymExpr sym BaseRealType
num  <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
x
     SymExpr sym BaseRealType
den  <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
y
     SymExpr sym BaseRealType
res  <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym BaseRealType
num SymExpr sym BaseRealType
den
     Pred sym
same <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymExpr sym BaseRealType
r SymExpr sym BaseRealType
res
     forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym
same, SymInteger sym
x, SymInteger sym
y)



--------------------------------------------------------------------------------
fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsInf :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsInf sym
sym (SFloat SymFloat sym fpp
x) = forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsInf sym
sym SymFloat sym fpp
x

fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNaN :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNaN sym
sym (SFloat SymFloat sym fpp
x) = forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNaN sym
sym SymFloat sym fpp
x

fpIsZero :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsZero :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsZero sym
sym (SFloat SymFloat sym fpp
x) = forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsZero sym
sym SymFloat sym fpp
x

fpIsNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNeg :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNeg sym
sym (SFloat SymFloat sym fpp
x) = forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNeg sym
sym SymFloat sym fpp
x

fpIsSubnorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsSubnorm :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsSubnorm sym
sym (SFloat SymFloat sym fpp
x) = forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsSubnorm sym
sym SymFloat sym fpp
x

fpIsNorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNorm :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNorm sym
sym (SFloat SymFloat sym fpp
x) = forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNorm sym
sym SymFloat sym fpp
x