{-# Language DataKinds #-}
{-# Language FlexibleContexts #-}
{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language TypeOperators #-}
-- | Working with floats of dynamic sizes.
-- This should probably be moved to What4 one day.
module Cryptol.Backend.What4.SFloat
  ( -- * Interface
    SFloat(..)
  , fpReprOf
  , fpSize
  , fpRepr

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

    -- * Interchange formats
  , fpFromBinary
  , fpToBinary

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

    -- * Arithmetic
  , SFloatBinArith
  , fpNeg
  , fpAdd
  , fpSub
  , fpMul
  , fpDiv

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

    -- * Queries
  , fpIsInf, fpIsNaN

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

import Control.Exception

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
(Int -> UnsupportedFloat -> ShowS)
-> (UnsupportedFloat -> String)
-> ([UnsupportedFloat] -> ShowS)
-> Show UnsupportedFloat
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 :: String -> Integer -> Integer -> IO a
unsupported String
l Integer
e Integer
p =
  UnsupportedFloat -> IO a
forall e a. Exception e => e -> IO a
throwIO UnsupportedFloat :: String -> Integer -> Integer -> UnsupportedFloat
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
(Int -> FPTypeError -> ShowS)
-> (FPTypeError -> String)
-> ([FPTypeError] -> ShowS)
-> Show FPTypeError
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 :: BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
fpTypeMismatch BaseTypeRepr t1
expect BaseTypeRepr t2
actual =
  FPTypeError -> IO a
forall e a. Exception e => e -> IO a
throwIO FPTypeError :: Some BaseTypeRepr -> Some BaseTypeRepr -> FPTypeError
FPTypeError { fpExpected :: Some BaseTypeRepr
fpExpected = BaseTypeRepr t1 -> Some BaseTypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some BaseTypeRepr t1
expect
                      , fpActual :: Some BaseTypeRepr
fpActual   = BaseTypeRepr t2 -> Some BaseTypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some BaseTypeRepr t2
actual
                      }
fpTypeError :: FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError :: FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError FloatPrecisionRepr t1
t1 FloatPrecisionRepr t2
t2 =
  BaseTypeRepr ('BaseFloatType t1)
-> BaseTypeRepr ('BaseFloatType t2) -> IO a
forall (t1 :: BaseType) (t2 :: BaseType) a.
BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
fpTypeMismatch (FloatPrecisionRepr t1 -> BaseTypeRepr ('BaseFloatType t1)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr t1
t1) (FloatPrecisionRepr t2 -> BaseTypeRepr ('BaseFloatType t2)
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    <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
iE
     LeqProof 2 x
LeqProof  <- NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (KnownNat 2 => NatRepr 2
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @2) NatRepr x
e
     Some NatRepr x
p    <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
iP
     LeqProof 2 x
LeqProof  <- NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (KnownNat 2 => NatRepr 2
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @2) NatRepr x
p
     Some FloatPrecisionRepr -> Maybe (Some FloatPrecisionRepr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FloatPrecisionRepr ('FloatingPointPrecision x x)
-> Some FloatPrecisionRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (NatRepr x
-> NatRepr x -> FloatPrecisionRepr ('FloatingPointPrecision x x)
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 :: sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
fpReprOf sym
_ SymFloat sym fpp
e =
  case SymFloat sym fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymFloat sym fpp
e of
    BaseFloatRepr FloatPrecisionRepr fpp
r -> FloatPrecisionRepr fpp
FloatPrecisionRepr fpp
r

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


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

-- | A fresh variable of the given type.
fpFresh ::
  IsSymExprBuilder sym =>
  sym ->
  Integer ->
  Integer ->
  IO (SFloat sym)
fpFresh :: 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 =
    SymExpr sym ('BaseFloatType x) -> SFloat sym
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym fpp -> SFloat sym
SFloat (SymExpr sym ('BaseFloatType x) -> SFloat sym)
-> IO (SymExpr sym ('BaseFloatType x)) -> IO (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SolverSymbol
-> BaseTypeRepr ('BaseFloatType x)
-> IO (SymExpr sym ('BaseFloatType x))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
emptySymbol (FloatPrecisionRepr x -> BaseTypeRepr ('BaseFloatType x)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr x
fpp)
  | Bool
otherwise = String -> Integer -> Integer -> IO (SFloat sym)
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 :: 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 = SymExpr sym ('BaseFloatType x) -> SFloat sym
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym fpp -> SFloat sym
SFloat (SymExpr sym ('BaseFloatType x) -> SFloat sym)
-> IO (SymExpr sym ('BaseFloatType x)) -> IO (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> FloatPrecisionRepr x -> IO (SymExpr sym ('BaseFloatType x))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatNaN sym
sym FloatPrecisionRepr x
fpp
  | Bool
otherwise = String -> Integer -> Integer -> IO (SFloat sym)
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 :: 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 = SymExpr sym ('BaseFloatType x) -> SFloat sym
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym fpp -> SFloat sym
SFloat (SymExpr sym ('BaseFloatType x) -> SFloat sym)
-> IO (SymExpr sym ('BaseFloatType x)) -> IO (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> FloatPrecisionRepr x -> IO (SymExpr sym ('BaseFloatType x))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatPInf sym
sym FloatPrecisionRepr x
fpp
  | Bool
otherwise = String -> Integer -> Integer -> IO (SFloat sym)
forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpPosInf" Integer
e Integer
p

-- | A floating point number corresponding to the given rations.
fpFromRationalLit ::
  IsExprBuilder sym =>
  sym ->
  Integer {- ^ Exponent width -} ->
  Integer {- ^ Precision width -} ->
  Rational ->
  IO (SFloat sym)
fpFromRationalLit :: 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 = SymExpr sym ('BaseFloatType x) -> SFloat sym
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym fpp -> SFloat sym
SFloat (SymExpr sym ('BaseFloatType x) -> SFloat sym)
-> IO (SymExpr sym ('BaseFloatType x)) -> IO (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> FloatPrecisionRepr x
-> Rational
-> IO (SymExpr sym ('BaseFloatType x))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat sym fpp)
floatLit sym
sym FloatPrecisionRepr x
fpp Rational
r
  | Bool
otherwise = String -> Integer -> Integer -> IO (SFloat sym)
forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpFromRational" 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 :: 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 = NatRepr eb -> NatRepr sb -> NatRepr (eb + sb)
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)  <- SymBV sym w -> BaseTypeRepr (BaseBVType w)
forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymBV sym w
sw =
    case NatRepr (eb + sb) -> NatRepr w -> Maybe ((eb + sb) :~: w)
forall k (f :: k -> *) (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 -> SymExpr sym ('BaseFloatType (FloatingPointPrecision eb sb))
-> SFloat sym
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym fpp -> SFloat sym
SFloat (SymExpr sym ('BaseFloatType (FloatingPointPrecision eb sb))
 -> SFloat sym)
-> IO (SymExpr sym ('BaseFloatType (FloatingPointPrecision eb sb)))
-> IO (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> SymBV sym (eb + sb)
-> IO (SymExpr sym ('BaseFloatType (FloatingPointPrecision eb sb)))
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
FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp SymBV sym w
SymBV sym (eb + sb)
sw
      Maybe ((eb + sb) :~: w)
Nothing -- we want to report type correct type errors! :-)
        | Just LeqProof 1 (eb + sb)
LeqProof <- NatRepr 1 -> NatRepr (eb + sb) -> Maybe (LeqProof 1 (eb + sb))
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr (eb + sb)
expectW ->
                BaseTypeRepr ('BaseBVType (eb + sb))
-> BaseTypeRepr (BaseBVType w) -> IO (SFloat sym)
forall (t1 :: BaseType) (t2 :: BaseType) a.
BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
fpTypeMismatch (NatRepr (eb + sb) -> BaseTypeRepr ('BaseBVType (eb + sb))
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr (eb + sb)
expectW) BaseTypeRepr (BaseBVType w)
actual
        | Bool
otherwise -> String -> [String] -> IO (SFloat sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"fpFromBits" [ String
"1 >= 2" ]
  | Bool
otherwise = String -> Integer -> Integer -> IO (SFloat sym)
forall a. String -> Integer -> Integer -> IO a
unsupported String
"fpFromBits" Integer
e Integer
p

fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym)
fpToBinary :: sym -> SFloat sym -> IO (SWord sym)
fpToBinary sym
sym (SFloat SymFloat sym fpp
f)
  | FloatingPointPrecisionRepr NatRepr eb
e NatRepr sb
p <- sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
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 <- NatRepr 1 -> NatRepr (eb + sb) -> Maybe (LeqProof 1 (eb + sb))
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) (NatRepr eb -> NatRepr sb -> NatRepr (eb + sb)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr eb
e NatRepr sb
p)
    = SymExpr sym ('BaseBVType (eb + sb)) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym ('BaseBVType (eb + sb)) -> SWord sym)
-> IO (SymExpr sym ('BaseBVType (eb + sb))) -> IO (SWord sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymFloat sym (FloatingPointPrecision eb sb)
-> IO (SymExpr sym ('BaseBVType (eb + sb)))
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
SymFloat sym (FloatingPointPrecision eb sb)
f
  | Bool
otherwise = String -> [String] -> IO (SWord sym)
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 :: sym -> SFloat sym -> IO (SFloat sym)
fpNeg sym
sym (SFloat SymFloat sym fpp
fl) = SymFloat sym fpp -> SFloat sym
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym fpp -> SFloat sym
SFloat (SymFloat sym fpp -> SFloat sym)
-> IO (SymFloat sym fpp) -> IO (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
floatNeg sym
sym 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 (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 sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
x
      t2 :: FloatPrecisionRepr fpp
t2 = sym
sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
y
  in
  case FloatPrecisionRepr fpp
-> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
forall k (f :: k -> *) (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 -> SymFloat sym fpp -> SFloat sym
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym fpp -> SFloat sym
SFloat (SymFloat sym fpp -> SFloat sym)
-> IO (SymFloat sym fpp) -> IO (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
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
SymFloat sym fpp
y
    Maybe (fpp :~: fpp)
_         -> FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> IO (SFloat sym)
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 :: SFloatBinArith sym
fpAdd = (forall (t :: FloatPrecision).
 sym
 -> RoundingMode
 -> SymFloat sym t
 -> SymFloat sym t
 -> IO (SymFloat sym t))
-> SFloatBinArith sym
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)
forall (t :: FloatPrecision).
sym
-> RoundingMode
-> SymFloat sym t
-> SymFloat sym t
-> IO (SymFloat sym t)
floatAdd

fpSub :: IsExprBuilder sym => SFloatBinArith sym
fpSub :: SFloatBinArith sym
fpSub = (forall (t :: FloatPrecision).
 sym
 -> RoundingMode
 -> SymFloat sym t
 -> SymFloat sym t
 -> IO (SymFloat sym t))
-> SFloatBinArith sym
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)
forall (t :: FloatPrecision).
sym
-> RoundingMode
-> SymFloat sym t
-> SymFloat sym t
-> IO (SymFloat sym t)
floatSub

fpMul :: IsExprBuilder sym => SFloatBinArith sym
fpMul :: SFloatBinArith sym
fpMul = (forall (t :: FloatPrecision).
 sym
 -> RoundingMode
 -> SymFloat sym t
 -> SymFloat sym t
 -> IO (SymFloat sym t))
-> SFloatBinArith sym
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)
forall (t :: FloatPrecision).
sym
-> RoundingMode
-> SymFloat sym t
-> SymFloat sym t
-> IO (SymFloat sym t)
floatMul

fpDiv :: IsExprBuilder sym => SFloatBinArith sym
fpDiv :: SFloatBinArith sym
fpDiv = (forall (t :: FloatPrecision).
 sym
 -> RoundingMode
 -> SymFloat sym t
 -> SymFloat sym t
 -> IO (SymFloat sym t))
-> SFloatBinArith sym
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)
forall (t :: FloatPrecision).
sym
-> RoundingMode
-> SymFloat sym t
-> SymFloat sym t
-> IO (SymFloat sym t)
floatDiv




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

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 (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 sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
x
      t2 :: FloatPrecisionRepr fpp
t2 = sym
sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
`fpReprOf` SymFloat sym fpp
y
  in
  case FloatPrecisionRepr fpp
-> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
forall k (f :: k -> *) (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 -> sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
forall (t :: FloatPrecision).
sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym)
fun sym
sym SymFloat sym fpp
x SymFloat sym fpp
SymFloat sym fpp
y
    Maybe (fpp :~: fpp)
_         -> FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> IO (Pred sym)
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 :: SFloatRel sym
fpEq = (forall (t :: FloatPrecision).
 sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
-> SFloatRel sym
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)
forall (t :: FloatPrecision).
sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym)
floatEq

fpEqIEEE :: IsExprBuilder sym => SFloatRel sym
fpEqIEEE :: SFloatRel sym
fpEqIEEE = (forall (t :: FloatPrecision).
 sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
-> SFloatRel sym
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)
forall (t :: FloatPrecision).
sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym)
floatFpEq

fpLtIEEE :: IsExprBuilder sym => SFloatRel sym
fpLtIEEE :: SFloatRel sym
fpLtIEEE = (forall (t :: FloatPrecision).
 sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
-> SFloatRel sym
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)
forall (t :: FloatPrecision).
sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym)
floatLt

fpGtIEEE :: IsExprBuilder sym => SFloatRel sym
fpGtIEEE :: SFloatRel sym
fpGtIEEE = (forall (t :: FloatPrecision).
 sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
-> SFloatRel sym
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)
forall (t :: FloatPrecision).
sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym)
floatGt


--------------------------------------------------------------------------------
fpRound ::
  IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpRound :: sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpRound sym
sym RoundingMode
r (SFloat SymFloat sym fpp
x) = SymFloat sym fpp -> SFloat sym
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym fpp -> SFloat sym
SFloat (SymFloat sym fpp -> SFloat sym)
-> IO (SymFloat sym fpp) -> IO (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
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 :: sym -> SFloat sym -> IO (SymReal sym)
fpToReal sym
sym (SFloat SymFloat sym fpp
x) = sym -> SymFloat sym fpp -> IO (SymReal sym)
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 :: 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 = SymExpr sym ('BaseFloatType x) -> SFloat sym
forall sym (fpp :: FloatPrecision).
IsExpr (SymExpr sym) =>
SymFloat sym fpp -> SFloat sym
SFloat (SymExpr sym ('BaseFloatType x) -> SFloat sym)
-> IO (SymExpr sym ('BaseFloatType x)) -> IO (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> FloatPrecisionRepr x
-> RoundingMode
-> SymReal sym
-> IO (SymExpr sym ('BaseFloatType x))
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 = String -> Integer -> Integer -> IO (SFloat sym)
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 :: sym
-> Integer
-> Integer
-> RoundingMode
-> SymInteger sym
-> IO (SFloat sym)
fpFromInteger sym
sym Integer
e Integer
p RoundingMode
r SymInteger sym
x = sym
-> Integer
-> Integer
-> RoundingMode
-> SymExpr sym 'BaseRealType
-> IO (SFloat sym)
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 -> IO (SFloat sym))
-> IO (SymExpr sym 'BaseRealType) -> IO (SFloat sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymInteger sym -> IO (SymExpr sym 'BaseRealType)
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 :: 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 <- sym -> SymInteger sym -> IO (SymExpr sym 'BaseRealType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
x
     SymExpr sym 'BaseRealType
den <- sym -> SymInteger sym -> IO (SymExpr sym 'BaseRealType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
y
     SymExpr sym 'BaseRealType
res <- sym
-> SymExpr sym 'BaseRealType
-> SymExpr sym 'BaseRealType
-> IO (SymExpr sym 'BaseRealType)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym 'BaseRealType
num SymExpr sym 'BaseRealType
den
     sym
-> Integer
-> Integer
-> RoundingMode
-> SymExpr sym 'BaseRealType
-> IO (SFloat sym)
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 :: sym -> SFloat sym -> IO (Pred sym, SymInteger sym, SymInteger sym)
fpToRational sym
sym SFloat sym
fp =
  do SymExpr sym 'BaseRealType
r    <- sym -> SFloat sym -> IO (SymExpr sym 'BaseRealType)
forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SymReal sym)
fpToReal sym
sym SFloat sym
fp
     SymInteger sym
x    <- sym
-> SolverSymbol
-> BaseTypeRepr 'BaseIntegerType
-> IO (SymInteger sym)
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    <- sym
-> SolverSymbol
-> BaseTypeRepr 'BaseIntegerType
-> IO (SymInteger sym)
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  <- sym -> SymInteger sym -> IO (SymExpr sym 'BaseRealType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
x
     SymExpr sym 'BaseRealType
den  <- sym -> SymInteger sym -> IO (SymExpr sym 'BaseRealType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
y
     SymExpr sym 'BaseRealType
res  <- sym
-> SymExpr sym 'BaseRealType
-> SymExpr sym 'BaseRealType
-> IO (SymExpr sym 'BaseRealType)
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 <- sym
-> SymExpr sym 'BaseRealType
-> SymExpr sym 'BaseRealType
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymExpr sym 'BaseRealType
r SymExpr sym 'BaseRealType
res
     (Pred sym, SymInteger sym, SymInteger sym)
-> IO (Pred sym, SymInteger sym, SymInteger sym)
forall (f :: * -> *) 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 :: sym -> SFloat sym -> IO (Pred sym)
fpIsInf sym
sym (SFloat SymFloat sym fpp
x) = sym -> SymFloat sym fpp -> IO (Pred sym)
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 :: sym -> SFloat sym -> IO (Pred sym)
fpIsNaN sym
sym (SFloat SymFloat sym fpp
x) = sym -> SymFloat sym fpp -> IO (Pred sym)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNaN sym
sym SymFloat sym fpp
x