-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Core.Floating
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Implementation of floating-point operations mapping to SMT-Lib2 floats
-----------------------------------------------------------------------------

{-# LANGUAGE DefaultSignatures    #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE Rank2Types           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans -Wno-incomplete-uni-patterns #-}

module Data.SBV.Core.Floating (
         IEEEFloating(..), IEEEFloatConvertible(..)
       , sFloatAsSWord32, sDoubleAsSWord64, sFloatingPointAsSWord
       , sWord32AsSFloat, sWord64AsSDouble, sWordAsSFloatingPoint
       , blastSFloat, blastSDouble,  blastSFloatingPoint
       , sFloatAsComparableSWord32,  sDoubleAsComparableSWord64,  sFloatingPointAsComparableSWord
       , sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint
       ) where

import Data.Bits (testBit)
import Data.Int  (Int8,  Int16,  Int32,  Int64)
import Data.Word (Word8, Word16, Word32, Word64)

import Data.Proxy

import Data.SBV.Core.AlgReals (isExactRational)
import Data.SBV.Core.Sized
import Data.SBV.Core.SizedFloats

import Data.SBV.Core.Data
import Data.SBV.Core.Kind
import Data.SBV.Core.Model
import Data.SBV.Core.Symbolic (addSValOptGoal)

import Data.SBV.Utils.Numeric

import Data.Ratio

import GHC.TypeLits

import LibBF

import Data.SBV.Core.Operations

-- | A class of floating-point (IEEE754) operations, some of
-- which behave differently based on rounding modes. Note that unless
-- the rounding mode is concretely RoundNearestTiesToEven, we will
-- not concretely evaluate these, but rather pass down to the SMT solver.
class (SymVal a, RealFloat a) => IEEEFloating a where
  -- | Compute the floating point absolute value.
  fpAbs             ::                  SBV a -> SBV a

  -- | Compute the unary negation. Note that @0 - x@ is not equivalent to @-x@ for floating-point, since @-0@ and @0@ are different.
  fpNeg             ::                  SBV a -> SBV a

  -- | Add two floating point values, using the given rounding mode
  fpAdd             :: SRoundingMode -> SBV a -> SBV a -> SBV a

  -- | Subtract two floating point values, using the given rounding mode
  fpSub             :: SRoundingMode -> SBV a -> SBV a -> SBV a

  -- | Multiply two floating point values, using the given rounding mode
  fpMul             :: SRoundingMode -> SBV a -> SBV a -> SBV a

  -- | Divide two floating point values, using the given rounding mode
  fpDiv             :: SRoundingMode -> SBV a -> SBV a -> SBV a

  -- | Fused-multiply-add three floating point values, using the given rounding mode. @fpFMA x y z = x*y+z@ but with only
  -- one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since
  -- Haskell lacks an FMA implementation.
  fpFMA             :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a

  -- | Compute the square-root of a float, using the given rounding mode
  fpSqrt            :: SRoundingMode -> SBV a -> SBV a

  -- | Compute the remainder: @x - y * n@, where @n@ is the truncated integer nearest to x/y. The rounding mode
  -- is implicitly assumed to be @RoundNearestTiesToEven@.
  fpRem             ::                  SBV a -> SBV a -> SBV a

  -- | Round to the nearest integral value, using the given rounding mode.
  fpRoundToIntegral :: SRoundingMode -> SBV a -> SBV a

  -- | Compute the minimum of two floats, respects @infinity@ and @NaN@ values
  fpMin             ::                  SBV a -> SBV a -> SBV a

  -- | Compute the maximum of two floats, respects @infinity@ and @NaN@ values
  fpMax             ::                  SBV a -> SBV a -> SBV a

  -- | Are the two given floats exactly the same. That is, @NaN@ will compare equal to itself, @+0@ will /not/ compare
  -- equal to @-0@ etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use '.=='.)
  fpIsEqualObject   ::                  SBV a -> SBV a -> SBool

  -- | Is the floating-point number a normal value. (i.e., not denormalized.)
  fpIsNormal :: SBV a -> SBool

  -- | Is the floating-point number a subnormal value. (Also known as denormal.)
  fpIsSubnormal :: SBV a -> SBool

  -- | Is the floating-point number 0? (Note that both +0 and -0 will satisfy this predicate.)
  fpIsZero :: SBV a -> SBool

  -- | Is the floating-point number infinity? (Note that both +oo and -oo will satisfy this predicate.)
  fpIsInfinite :: SBV a -> SBool

  -- | Is the floating-point number a NaN value?
  fpIsNaN ::  SBV a -> SBool

  -- | Is the floating-point number negative? Note that -0 satisfies this predicate but +0 does not.
  fpIsNegative :: SBV a -> SBool

  -- | Is the floating-point number positive? Note that +0 satisfies this predicate but -0 does not.
  fpIsPositive :: SBV a -> SBool

  -- | Is the floating point number -0?
  fpIsNegativeZero :: SBV a -> SBool

  -- | Is the floating point number +0?
  fpIsPositiveZero :: SBV a -> SBool

  -- | Is the floating-point number a regular floating point, i.e., not NaN, nor +oo, nor -oo. Normals or denormals are allowed.
  fpIsPoint :: SBV a -> SBool

  -- Default definitions. Minimal complete definition: None! All should be taken care by defaults
  -- Note that we never evaluate FMA concretely, as there's no fma operator in Haskell
  fpAbs              = forall a.
SymVal a =>
FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
lift1  FPOp
FP_Abs             (forall a. a -> Maybe a
Just forall a. Num a => a -> a
abs)                forall a. Maybe a
Nothing
  fpNeg              = forall a.
SymVal a =>
FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
lift1  FPOp
FP_Neg             (forall a. a -> Maybe a
Just forall a. Num a => a -> a
negate)             forall a. Maybe a
Nothing
  fpAdd              = forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2  FPOp
FP_Add             (forall a. a -> Maybe a
Just forall a. Num a => a -> a -> a
(+))                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
  fpSub              = forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2  FPOp
FP_Sub             (forall a. a -> Maybe a
Just (-))                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
  fpMul              = forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2  FPOp
FP_Mul             (forall a. a -> Maybe a
Just forall a. Num a => a -> a -> a
(*))                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
  fpDiv              = forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2  FPOp
FP_Div             (forall a. a -> Maybe a
Just forall a. Fractional a => a -> a -> a
(/))                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
  fpFMA              = forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
-> SBV a
lift3  FPOp
FP_FMA             forall a. Maybe a
Nothing                   forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
  fpSqrt             = forall a.
SymVal a =>
FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
lift1  FPOp
FP_Sqrt            (forall a. a -> Maybe a
Just forall a. Floating a => a -> a
sqrt)               forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
  fpRem              = forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2  FPOp
FP_Rem             (forall a. a -> Maybe a
Just forall a. RealFloat a => a -> a -> a
fpRemH)             forall a. Maybe a
Nothing
  fpRoundToIntegral  = forall a.
SymVal a =>
FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
lift1  FPOp
FP_RoundToIntegral (forall a. a -> Maybe a
Just forall a. RealFloat a => a -> a
fpRoundToIntegralH) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
  fpMin              = forall a.
(SymVal a, RealFloat a) =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
liftMM FPOp
FP_Min             (forall a. a -> Maybe a
Just forall a. RealFloat a => a -> a -> a
fpMinH)             forall a. Maybe a
Nothing
  fpMax              = forall a.
(SymVal a, RealFloat a) =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
liftMM FPOp
FP_Max             (forall a. a -> Maybe a
Just forall a. RealFloat a => a -> a -> a
fpMaxH)             forall a. Maybe a
Nothing
  fpIsEqualObject    = forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> Bool)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBool
lift2B FPOp
FP_ObjEqual        (forall a. a -> Maybe a
Just forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH)   forall a. Maybe a
Nothing
  fpIsNormal         = forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
lift1B FPOp
FP_IsNormal        forall a. RealFloat a => a -> Bool
fpIsNormalizedH
  fpIsSubnormal      = forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
lift1B FPOp
FP_IsSubnormal     forall a. RealFloat a => a -> Bool
isDenormalized
  fpIsZero           = forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
lift1B FPOp
FP_IsZero          (forall a. Eq a => a -> a -> Bool
== a
0)
  fpIsInfinite       = forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
lift1B FPOp
FP_IsInfinite      forall a. RealFloat a => a -> Bool
isInfinite
  fpIsNaN            = forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
lift1B FPOp
FP_IsNaN           forall a. RealFloat a => a -> Bool
isNaN
  fpIsNegative       = forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
lift1B FPOp
FP_IsNegative      (\a
x -> a
x forall a. Ord a => a -> a -> Bool
< a
0 Bool -> Bool -> Bool
||       forall a. RealFloat a => a -> Bool
isNegativeZero a
x)
  fpIsPositive       = forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
lift1B FPOp
FP_IsPositive      (\a
x -> a
x forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. RealFloat a => a -> Bool
isNegativeZero a
x))
  fpIsNegativeZero SBV a
x = forall a. IEEEFloating a => SBV a -> SBool
fpIsZero SBV a
x SBool -> SBool -> SBool
.&& forall a. IEEEFloating a => SBV a -> SBool
fpIsNegative SBV a
x
  fpIsPositiveZero SBV a
x = forall a. IEEEFloating a => SBV a -> SBool
fpIsZero SBV a
x SBool -> SBool -> SBool
.&& forall a. IEEEFloating a => SBV a -> SBool
fpIsPositive SBV a
x
  fpIsPoint        SBV a
x = SBool -> SBool
sNot (forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SBV a
x SBool -> SBool -> SBool
.|| forall a. IEEEFloating a => SBV a -> SBool
fpIsInfinite SBV a
x)

-- | SFloat instance
instance IEEEFloating Float

-- | SDouble instance
instance IEEEFloating Double

-- | Conversion to and from floats
class SymVal a => IEEEFloatConvertible a where
  -- | Convert from an IEEE74 single precision float.
  fromSFloat :: SRoundingMode -> SFloat -> SBV a
  fromSFloat = forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat

  -- | Convert to an IEEE-754 Single-precision float.
  toSFloat :: SRoundingMode -> SBV a -> SFloat

  -- default definition if we have an integral like
  default toSFloat :: Integral a => SRoundingMode -> SBV a -> SFloat
  toSFloat = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
onlyWhenRNE (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral))

  -- | Convert from an IEEE74 double precision float.
  fromSDouble :: SRoundingMode -> SDouble -> SBV a
  fromSDouble = forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat

  -- | Convert to an IEEE-754 Double-precision float.
  toSDouble :: SRoundingMode -> SBV a -> SDouble

  -- default definition if we have an integral like
  default toSDouble :: Integral a => SRoundingMode -> SBV a -> SDouble
  toSDouble = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
onlyWhenRNE (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral))

  -- | Convert from an arbitrary floating point.
  fromSFloatingPoint :: ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV a
  fromSFloatingPoint = forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat

  -- | Convert to an arbitrary floating point.
  toSFloatingPoint :: ValidFloat eb sb => SRoundingMode -> SBV a -> SFloatingPoint eb sb

  -- -- default definition if we have an integral like
  default toSFloatingPoint :: (Integral a, ValidFloat eb sb) => SRoundingMode -> SBV a -> SFloatingPoint eb sb
  toSFloatingPoint = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (forall a b. a -> b -> a
const (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral))

-- Run the function if the conversion is in RNE. Otherwise return Nothing.
onlyWhenRNE :: (a -> Maybe b) -> RoundingMode -> a -> Maybe b
onlyWhenRNE :: forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
onlyWhenRNE a -> Maybe b
f RoundingMode
RoundNearestTiesToEven a
v = a -> Maybe b
f a
v
onlyWhenRNE a -> Maybe b
_ RoundingMode
_                      a
_ = forall a. Maybe a
Nothing

-- | A generic from-float converter. Note that this function does no constant folding since
-- it's behavior is undefined when the input float is out-of-bounds or not a point.
genericFromFloat :: forall a r. (IEEEFloating a, IEEEFloatConvertible r)
                 => SRoundingMode            -- Rounding mode
                 -> SBV a                    -- Input float/double
                 -> SBV r
genericFromFloat :: forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat SRoundingMode
rm SBV a
f = forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kTo (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r)))
  where kFrom :: Kind
kFrom = forall a. HasKind a => a -> Kind
kindOf SBV a
f
        kTo :: Kind
kTo   = forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @r)
        r :: State -> IO SV
r State
st  = do SV
msv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SRoundingMode
rm
                   SV
xsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
f
                   State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kTo (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> SV -> FPOp
FP_Cast Kind
kFrom Kind
kTo SV
msv)) [SV
xsv])

-- | A generic to-float converter, which will constant-fold as necessary, but only in the sRNE mode for regular floats.
genericToFloat :: forall a r. (IEEEFloatConvertible a, IEEEFloating r)
               => (RoundingMode -> a -> Maybe r)     -- How to convert concretely, if possible
               -> SRoundingMode                      -- Rounding mode
               -> SBV a                              -- Input convertible
               -> SBV r
genericToFloat :: forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat RoundingMode -> a -> Maybe r
converter SRoundingMode
rm SBV a
i
  | Just a
w <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
i, Just RoundingMode
crm <- forall a. SymVal a => SBV a -> Maybe a
unliteral SRoundingMode
rm, Just r
result <- RoundingMode -> a -> Maybe r
converter RoundingMode
crm a
w
  = forall a. SymVal a => a -> SBV a
literal r
result
  | Bool
True
  = forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kTo (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r)))
  where kFrom :: Kind
kFrom = forall a. HasKind a => a -> Kind
kindOf SBV a
i
        kTo :: Kind
kTo   = forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @r)
        r :: State -> IO SV
r State
st  = do SV
msv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SRoundingMode
rm
                   SV
xsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
i
                   State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kTo (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> SV -> FPOp
FP_Cast Kind
kFrom Kind
kTo SV
msv)) [SV
xsv])

instance IEEEFloatConvertible Int8
instance IEEEFloatConvertible Int16
instance IEEEFloatConvertible Int32
instance IEEEFloatConvertible Int64
instance IEEEFloatConvertible Word8
instance IEEEFloatConvertible Word16
instance IEEEFloatConvertible Word32
instance IEEEFloatConvertible Word64
instance IEEEFloatConvertible Integer

-- For float and double, skip the conversion if the same and do the constant folding, unlike all others.
instance IEEEFloatConvertible Float where
  toSFloat :: SRoundingMode -> SFloat -> SFloat
toSFloat  SRoundingMode
_ SFloat
f = SFloat
f
  toSDouble :: SRoundingMode -> SFloat -> SDouble
toSDouble     = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
onlyWhenRNE (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (RealFloat a, RealFloat b) => a -> b
fp2fp))

  toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SFloat -> SFloatingPoint eb sb
toSFloatingPoint SRoundingMode
rm SFloat
f = forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SBV a -> SFloatingPoint eb sb
toSFloatingPoint SRoundingMode
rm forall a b. (a -> b) -> a -> b
$ forall a.
IEEEFloatConvertible a =>
SRoundingMode -> SBV a -> SDouble
toSDouble SRoundingMode
rm SFloat
f

  fromSFloat :: SRoundingMode -> SFloat -> SFloat
fromSFloat  SRoundingMode
_  SFloat
f = SFloat
f
  fromSDouble :: SRoundingMode -> SDouble -> SFloat
fromSDouble SRoundingMode
rm SDouble
f
    | Just RoundingMode
RoundNearestTiesToEven <- forall a. SymVal a => SBV a -> Maybe a
unliteral SRoundingMode
rm
    , Just Double
fv                     <- forall a. SymVal a => SBV a -> Maybe a
unliteral SDouble
f
    = forall a. SymVal a => a -> SBV a
literal (forall a b. (RealFloat a, RealFloat b) => a -> b
fp2fp Double
fv)
    | Bool
True
    = forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat SRoundingMode
rm SDouble
f

instance IEEEFloatConvertible Double where
  toSFloat :: SRoundingMode -> SDouble -> SFloat
toSFloat      = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
onlyWhenRNE (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (RealFloat a, RealFloat b) => a -> b
fp2fp))
  toSDouble :: SRoundingMode -> SDouble -> SDouble
toSDouble SRoundingMode
_ SDouble
d = SDouble
d

  toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SDouble -> SFloatingPoint eb sb
toSFloatingPoint SRoundingMode
rm SDouble
sd
    | Just Double
d <- forall a. SymVal a => SBV a -> Maybe a
unliteral SDouble
sd, Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
    = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint forall a b. (a -> b) -> a -> b
$ Int -> Int -> BigFloat -> FP
FP Int
ei Int
si forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst (BFOpts -> BigFloat -> (BigFloat, Status)
bfRoundFloat (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
ei Int
si RoundMode
brm) (Double -> BigFloat
bfFromDouble Double
d))
    | Bool
True
    = SBV (FloatingPoint eb sb)
res
    where (Kind
k, Int
ei, Int
si) = case forall a. HasKind a => a -> Kind
kindOf SBV (FloatingPoint eb sb)
res of
                         kr :: Kind
kr@(KFP Int
eb Int
sb) -> (Kind
kr, Int
eb, Int
sb)
                         Kind
kr             -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Unexpected kind in toSFloatingPoint: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Kind
kr, SRoundingMode
rm, SDouble
sd)
          res :: SBV (FloatingPoint eb sb)
res = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
          r :: State -> IO SV
r State
st = do SV
msv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SRoundingMode
rm
                    SV
xsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SDouble
sd
                    State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> SV -> FPOp
FP_Cast Kind
KDouble Kind
k SV
msv)) [SV
xsv])

  fromSDouble :: SRoundingMode -> SDouble -> SDouble
fromSDouble SRoundingMode
_  SDouble
d = SDouble
d
  fromSFloat :: SRoundingMode -> SFloat -> SDouble
fromSFloat  SRoundingMode
rm SFloat
d
    | Just RoundingMode
RoundNearestTiesToEven <- forall a. SymVal a => SBV a -> Maybe a
unliteral SRoundingMode
rm
    , Just Float
dv                     <- forall a. SymVal a => SBV a -> Maybe a
unliteral SFloat
d
    = forall a. SymVal a => a -> SBV a
literal (forall a b. (RealFloat a, RealFloat b) => a -> b
fp2fp Float
dv)
    | Bool
True
    = forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat SRoundingMode
rm SFloat
d

convertWhenExactRational :: Fractional a => AlgReal -> Maybe a
convertWhenExactRational :: forall a. Fractional a => AlgReal -> Maybe a
convertWhenExactRational AlgReal
r
  | AlgReal -> Bool
isExactRational AlgReal
r = forall a. a -> Maybe a
Just (forall a. Fractional a => Rational -> a
fromRational (forall a. Real a => a -> Rational
toRational AlgReal
r))
  | Bool
True              = forall a. Maybe a
Nothing

-- For AlgReal; be careful to only process exact rationals concretely
instance IEEEFloatConvertible AlgReal where
  toSFloat :: SRoundingMode -> SBV AlgReal -> SFloat
toSFloat         = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
onlyWhenRNE forall a. Fractional a => AlgReal -> Maybe a
convertWhenExactRational)
  toSDouble :: SRoundingMode -> SBV AlgReal -> SDouble
toSDouble        = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
onlyWhenRNE forall a. Fractional a => AlgReal -> Maybe a
convertWhenExactRational)
  toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SBV AlgReal -> SFloatingPoint eb sb
toSFloatingPoint = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (forall a b. a -> b -> a
const       forall a. Fractional a => AlgReal -> Maybe a
convertWhenExactRational)

-- Arbitrary floats can handle all rounding modes in concrete mode
instance ValidFloat eb sb => IEEEFloatConvertible (FloatingPoint eb sb) where
  toSFloat :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloat
toSFloat SRoundingMode
rm SBV (FloatingPoint eb sb)
i
    | Just (FloatingPoint (FP Int
_ Int
_ BigFloat
v)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV (FloatingPoint eb sb)
i, Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
    = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a b. (RealFloat a, RealFloat b) => a -> b
fp2fp forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst (RoundMode -> BigFloat -> (Double, Status)
bfToDouble RoundMode
brm (forall a b. (a, b) -> a
fst (BFOpts -> BigFloat -> (BigFloat, Status)
bfRoundFloat (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
ei Int
si RoundMode
brm) BigFloat
v)))
    | Bool
True
    = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (\RoundingMode
_ FloatingPoint eb sb
_ -> forall a. Maybe a
Nothing) SRoundingMode
rm SBV (FloatingPoint eb sb)
i
    where ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
          si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)

  fromSFloat :: SRoundingMode -> SFloat -> SBV (FloatingPoint eb sb)
fromSFloat SRoundingMode
rm SFloat
i
    | Just Float
f <- forall a. SymVal a => SBV a -> Maybe a
unliteral SFloat
i, Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
    = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint forall a b. (a -> b) -> a -> b
$ Int -> Int -> BigFloat -> FP
FP Int
ei Int
si forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst (BFOpts -> BigFloat -> (BigFloat, Status)
bfRoundFloat (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
ei Int
si RoundMode
brm) (Double -> BigFloat
bfFromDouble (forall a b. (RealFloat a, RealFloat b) => a -> b
fp2fp Float
f :: Double)))
    | Bool
True
    = forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat SRoundingMode
rm SFloat
i
    where ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
          si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)

  toSDouble :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SDouble
toSDouble SRoundingMode
rm SBV (FloatingPoint eb sb)
i
    | Just (FloatingPoint (FP Int
_ Int
_ BigFloat
v)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV (FloatingPoint eb sb)
i, Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
    = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst (RoundMode -> BigFloat -> (Double, Status)
bfToDouble RoundMode
brm (forall a b. (a, b) -> a
fst (BFOpts -> BigFloat -> (BigFloat, Status)
bfRoundFloat (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
ei Int
si RoundMode
brm) BigFloat
v)))
    | Bool
True
    = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (\RoundingMode
_ FloatingPoint eb sb
_ -> forall a. Maybe a
Nothing) SRoundingMode
rm SBV (FloatingPoint eb sb)
i
    where ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
          si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)

  fromSDouble :: SRoundingMode -> SDouble -> SBV (FloatingPoint eb sb)
fromSDouble SRoundingMode
rm SDouble
i
    | Just Double
f <- forall a. SymVal a => SBV a -> Maybe a
unliteral SDouble
i, Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
    = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint forall a b. (a -> b) -> a -> b
$ Int -> Int -> BigFloat -> FP
FP Int
ei Int
si forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst (BFOpts -> BigFloat -> (BigFloat, Status)
bfRoundFloat (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
ei Int
si RoundMode
brm) (Double -> BigFloat
bfFromDouble Double
f))
    | Bool
True
    = forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat SRoundingMode
rm SDouble
i
    where ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
          si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)

  toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloatingPoint eb sb
toSFloatingPoint SRoundingMode
rm SBV (FloatingPoint eb sb)
i
    | Just (FloatingPoint (FP Int
_ Int
_ BigFloat
v)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV (FloatingPoint eb sb)
i, Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
    = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint forall a b. (a -> b) -> a -> b
$ Int -> Int -> BigFloat -> FP
FP Int
ei Int
si forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst (BFOpts -> BigFloat -> (BigFloat, Status)
bfRoundFloat (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
ei Int
si RoundMode
brm) BigFloat
v)
    | Bool
True
    = forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat (\RoundingMode
_ FloatingPoint eb sb
_ -> forall a. Maybe a
Nothing) SRoundingMode
rm SBV (FloatingPoint eb sb)
i
    where ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
          si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)

  -- From and To are the same when the source is an arbitrary float!
  fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SFloatingPoint eb sb -> SBV (FloatingPoint eb sb)
fromSFloatingPoint = forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SBV a -> SFloatingPoint eb sb
toSFloatingPoint

-- | Concretely evaluate one arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data
concEval1 :: SymVal a => Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)
concEval1 :: forall a.
SymVal a =>
Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)
concEval1 Maybe (a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a = do a -> a
op <- Maybe (a -> a)
mbOp
                           a
v  <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a
                           case forall a. SymVal a => SBV a -> Maybe a
unliteral forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe SRoundingMode
mbRm of
                                   Maybe RoundingMode
Nothing                     -> (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => a -> SBV a
literal) (a -> a
op a
v)
                                   Just RoundingMode
RoundNearestTiesToEven -> (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => a -> SBV a
literal) (a -> a
op a
v)
                                   Maybe RoundingMode
_                           -> forall a. Maybe a
Nothing

-- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data
concEval2 :: SymVal a => Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
concEval2 :: forall a.
SymVal a =>
Maybe (a -> a -> a)
-> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
concEval2 Maybe (a -> a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b = do a -> a -> a
op <- Maybe (a -> a -> a)
mbOp
                             a
v1 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a
                             a
v2 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
b
                             case forall a. SymVal a => SBV a -> Maybe a
unliteral forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe SRoundingMode
mbRm of
                                     Maybe RoundingMode
Nothing                     -> (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => a -> SBV a
literal) (a
v1 a -> a -> a
`op` a
v2)
                                     Just RoundingMode
RoundNearestTiesToEven -> (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => a -> SBV a
literal) (a
v1 a -> a -> a
`op` a
v2)
                                     Maybe RoundingMode
_                           -> forall a. Maybe a
Nothing

-- | Concretely evaluate a bool producing two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data
concEval2B :: SymVal a => Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool
concEval2B :: forall a.
SymVal a =>
Maybe (a -> a -> Bool)
-> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool
concEval2B Maybe (a -> a -> Bool)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b = do a -> a -> Bool
op <- Maybe (a -> a -> Bool)
mbOp
                              a
v1 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a
                              a
v2 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
b
                              case forall a. SymVal a => SBV a -> Maybe a
unliteral forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe SRoundingMode
mbRm of
                                      Maybe RoundingMode
Nothing                     -> (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => a -> SBV a
literal) (a
v1 a -> a -> Bool
`op` a
v2)
                                      Just RoundingMode
RoundNearestTiesToEven -> (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => a -> SBV a
literal) (a
v1 a -> a -> Bool
`op` a
v2)
                                      Maybe RoundingMode
_                           -> forall a. Maybe a
Nothing

-- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data
concEval3 :: SymVal a => Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)
concEval3 :: forall a.
SymVal a =>
Maybe (a -> a -> a -> a)
-> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)
concEval3 Maybe (a -> a -> a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b SBV a
c = do a -> a -> a -> a
op <- Maybe (a -> a -> a -> a)
mbOp
                               a
v1 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a
                               a
v2 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
b
                               a
v3 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
c
                               case forall a. SymVal a => SBV a -> Maybe a
unliteral forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe SRoundingMode
mbRm of
                                       Maybe RoundingMode
Nothing                     -> (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => a -> SBV a
literal) (a -> a -> a -> a
op a
v1 a
v2 a
v3)
                                       Just RoundingMode
RoundNearestTiesToEven -> (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => a -> SBV a
literal) (a -> a -> a -> a
op a
v1 a
v2 a
v3)
                                       Maybe RoundingMode
_                           -> forall a. Maybe a
Nothing

-- | Add the converted rounding mode if given as an argument
addRM :: State -> Maybe SRoundingMode -> [SV] -> IO [SV]
addRM :: State -> Maybe SRoundingMode -> [SV] -> IO [SV]
addRM State
_  Maybe SRoundingMode
Nothing   [SV]
as = forall (m :: * -> *) a. Monad m => a -> m a
return [SV]
as
addRM State
st (Just SRoundingMode
rm) [SV]
as = do SV
svm <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SRoundingMode
rm
                           forall (m :: * -> *) a. Monad m => a -> m a
return (SV
svm forall a. a -> [a] -> [a]
: [SV]
as)

-- | Lift a 1 arg FP-op
lift1 :: SymVal a => FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
lift1 :: forall a.
SymVal a =>
FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
lift1 FPOp
w Maybe (a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a
  | Just SBV a
cv <- forall a.
SymVal a =>
Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)
concEval1 Maybe (a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a
  = SBV a
cv
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k    = forall a. HasKind a => a -> Kind
kindOf SBV a
a
        r :: State -> IO SV
r State
st = do SV
sva  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  [SV]
args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
addRM State
st Maybe SRoundingMode
mbRm [SV
sva]
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP FPOp
w) [SV]
args)

-- | Lift an FP predicate
lift1B :: SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
lift1B :: forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
lift1B FPOp
w a -> Bool
f SBV a
a
   | Just a
v <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ a -> Bool
f a
v
   | Bool
True                  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
   where r :: State -> IO SV
r State
st = do SV
sva <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                   State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP FPOp
w) [SV
sva])


-- | Lift a 2 arg FP-op
lift2 :: SymVal a => FPOp -> Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a
lift2 :: forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2 FPOp
w Maybe (a -> a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b
  | Just SBV a
cv <- forall a.
SymVal a =>
Maybe (a -> a -> a)
-> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
concEval2 Maybe (a -> a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b
  = SBV a
cv
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k    = forall a. HasKind a => a -> Kind
kindOf SBV a
a
        r :: State -> IO SV
r State
st = do SV
sva  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  SV
svb  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
b
                  [SV]
args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
addRM State
st Maybe SRoundingMode
mbRm [SV
sva, SV
svb]
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP FPOp
w) [SV]
args)

-- | Lift min/max: Note that we protect against constant folding if args are alternating sign 0's, since
-- SMTLib is deliberately nondeterministic in this case
liftMM :: (SymVal a, RealFloat a) => FPOp -> Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a
liftMM :: forall a.
(SymVal a, RealFloat a) =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
liftMM FPOp
w Maybe (a -> a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b
  | Just a
v1 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a
  , Just a
v2 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
b
  , Bool -> Bool
not ((a -> Bool
isN0 a
v1 Bool -> Bool -> Bool
&& a -> Bool
isP0 a
v2) Bool -> Bool -> Bool
|| (a -> Bool
isP0 a
v1 Bool -> Bool -> Bool
&& a -> Bool
isN0 a
v2))          -- If not +0/-0 or -0/+0
  , Just SBV a
cv <- forall a.
SymVal a =>
Maybe (a -> a -> a)
-> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
concEval2 Maybe (a -> a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b
  = SBV a
cv
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where isN0 :: a -> Bool
isN0   = forall a. RealFloat a => a -> Bool
isNegativeZero
        isP0 :: a -> Bool
isP0 a
x = a
x forall a. Eq a => a -> a -> Bool
== a
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Bool
isN0 a
x)
        k :: Kind
k    = forall a. HasKind a => a -> Kind
kindOf SBV a
a
        r :: State -> IO SV
r State
st = do SV
sva  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  SV
svb  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
b
                  [SV]
args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
addRM State
st Maybe SRoundingMode
mbRm [SV
sva, SV
svb]
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP FPOp
w) [SV]
args)

-- | Lift a 2 arg FP-op, producing bool
lift2B :: SymVal a => FPOp -> Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBool
lift2B :: forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> Bool)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBool
lift2B FPOp
w Maybe (a -> a -> Bool)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b
  | Just SBool
cv <- forall a.
SymVal a =>
Maybe (a -> a -> Bool)
-> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool
concEval2B Maybe (a -> a -> Bool)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b
  = SBool
cv
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where r :: State -> IO SV
r State
st = do SV
sva  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  SV
svb  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
b
                  [SV]
args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
addRM State
st Maybe SRoundingMode
mbRm [SV
sva, SV
svb]
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP FPOp
w) [SV]
args)

-- | Lift a 3 arg FP-op
lift3 :: SymVal a => FPOp -> Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
lift3 :: forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
-> SBV a
lift3 FPOp
w Maybe (a -> a -> a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b SBV a
c
  | Just SBV a
cv <- forall a.
SymVal a =>
Maybe (a -> a -> a -> a)
-> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)
concEval3 Maybe (a -> a -> a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a SBV a
b SBV a
c
  = SBV a
cv
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k    = forall a. HasKind a => a -> Kind
kindOf SBV a
a
        r :: State -> IO SV
r State
st = do SV
sva  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  SV
svb  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
b
                  SV
svc  <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
c
                  [SV]
args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
addRM State
st Maybe SRoundingMode
mbRm [SV
sva, SV
svb, SV
svc]
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP FPOp
w) [SV]
args)

-- | Convert an 'SFloat' to an 'SWord32', preserving the bit-correspondence. Note that since the
-- representation for @NaN@s are not unique, this function will return a symbolic value when given a
-- concrete @NaN@.
--
-- Implementation note: Since there's no corresponding function in SMTLib for conversion to
-- bit-representation due to partiality, we use a translation trick by allocating a new word variable,
-- converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map
-- it to a simple conversion.
sFloatAsSWord32 :: SFloat -> SWord32
sFloatAsSWord32 :: SFloat -> SWord32
sFloatAsSWord32 (SBV SVal
v) = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ SVal -> SVal
svFloatAsSWord32 SVal
v

-- | Convert an 'SDouble' to an 'SWord64', preserving the bit-correspondence. Note that since the
-- representation for @NaN@s are not unique, this function will return a symbolic value when given a
-- concrete @NaN@.
--
-- See the implementation note for 'sFloatAsSWord32', as it applies here as well.
sDoubleAsSWord64 :: SDouble -> SWord64
sDoubleAsSWord64 :: SDouble -> SWord64
sDoubleAsSWord64 (SBV SVal
v) = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ SVal -> SVal
svDoubleAsSWord64 SVal
v

-- | Extract the sign\/exponent\/mantissa of a single-precision float. The output will have
-- 8 bits in the second argument for exponent, and 23 in the third for the mantissa.
blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
blastSFloat = forall {a}. SFiniteBits a => SBV a -> (SBool, [SBool], [SBool])
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. SFloat -> SWord32
sFloatAsSWord32
 where extract :: SBV a -> (SBool, [SBool], [SBool])
extract SBV a
x = (forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SBV a
x Int
31, forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
sExtractBits SBV a
x [Int
30, Int
29 .. Int
23], forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
sExtractBits SBV a
x [Int
22, Int
21 .. Int
0])

-- | Extract the sign\/exponent\/mantissa of a single-precision float. The output will have
-- 11 bits in the second argument for exponent, and 52 in the third for the mantissa.
blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
blastSDouble = forall {a}. SFiniteBits a => SBV a -> (SBool, [SBool], [SBool])
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDouble -> SWord64
sDoubleAsSWord64
 where extract :: SBV a -> (SBool, [SBool], [SBool])
extract SBV a
x = (forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SBV a
x Int
63, forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
sExtractBits SBV a
x [Int
62, Int
61 .. Int
52], forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
sExtractBits SBV a
x [Int
51, Int
50 .. Int
0])

-- | Extract the sign\/exponent\/mantissa of an arbitrary precision float. The output will have
-- @eb@ bits in the second argument for exponent, and @sb-1@ bits in the third for mantissa.
blastSFloatingPoint :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb))
                    => SFloatingPoint eb sb -> (SBool, [SBool], [SBool])
blastSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> (SBool, [SBool], [SBool])
blastSFloatingPoint = SBV (WordN (eb + sb)) -> (SBool, [SBool], [SBool])
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (eb :: Nat) (sb :: Nat).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsSWord
  where ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
        si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)
        extract :: SBV (WordN (eb + sb)) -> (SBool, [SBool], [SBool])
extract SBV (WordN (eb + sb))
x = (forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SBV (WordN (eb + sb))
x (Int
ei forall a. Num a => a -> a -> a
+ Int
si forall a. Num a => a -> a -> a
- Int
1), forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
sExtractBits SBV (WordN (eb + sb))
x [Int
ei forall a. Num a => a -> a -> a
+ Int
si forall a. Num a => a -> a -> a
- Int
2, Int
ei forall a. Num a => a -> a -> a
+ Int
si forall a. Num a => a -> a -> a
- Int
3 .. Int
si forall a. Num a => a -> a -> a
- Int
1], forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
sExtractBits SBV (WordN (eb + sb))
x [Int
si forall a. Num a => a -> a -> a
- Int
2, Int
si forall a. Num a => a -> a -> a
- Int
3 .. Int
0])

-- | Reinterpret the bits in a 32-bit word as a single-precision floating point number
sWord32AsSFloat :: SWord32 -> SFloat
sWord32AsSFloat :: SWord32 -> SFloat
sWord32AsSFloat SWord32
fVal
  | Just Word32
f <- forall a. SymVal a => SBV a -> Maybe a
unliteral SWord32
fVal = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ Word32 -> Float
wordToFloat Word32
f
  | Bool
True                     = forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KFloat (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
y)))
  where y :: State -> IO SV
y State
st = do SV
xsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SWord32
fVal
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KFloat (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret (forall a. HasKind a => a -> Kind
kindOf SWord32
fVal) Kind
KFloat)) [SV
xsv])

-- | Reinterpret the bits in a 32-bit word as a single-precision floating point number
sWord64AsSDouble :: SWord64 -> SDouble
sWord64AsSDouble :: SWord64 -> SDouble
sWord64AsSDouble SWord64
dVal
  | Just Word64
d <- forall a. SymVal a => SBV a -> Maybe a
unliteral SWord64
dVal = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ Word64 -> Double
wordToDouble Word64
d
  | Bool
True                     = forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KDouble (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
y)))
  where y :: State -> IO SV
y State
st = do SV
xsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SWord64
dVal
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KDouble (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret (forall a. HasKind a => a -> Kind
kindOf SWord64
dVal) Kind
KDouble)) [SV
xsv])

-- | Convert a float to a comparable 'SWord32'. The trick is to ignore the
-- sign of -0, and if it's a negative value flip all the bits, and otherwise
-- only flip the sign bit. This is known as the lexicographic ordering on floats
-- and it works as long as you do not have a @NaN@.
sFloatAsComparableSWord32 :: SFloat -> SWord32
sFloatAsComparableSWord32 :: SFloat -> SWord32
sFloatAsComparableSWord32 SFloat
f = forall a. Mergeable a => SBool -> a -> a -> a
ite (forall a. IEEEFloating a => SBV a -> SBool
fpIsNegativeZero SFloat
f) (SFloat -> SWord32
sFloatAsComparableSWord32 SFloat
0) (forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot SBool
sb forall a. a -> [a] -> [a]
: forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
sb (forall a b. (a -> b) -> [a] -> [b]
map SBool -> SBool
sNot [SBool]
rest) [SBool]
rest)
  where (SBool
sb : [SBool]
rest) = forall a. SFiniteBits a => SBV a -> [SBool]
blastBE forall a b. (a -> b) -> a -> b
$ SFloat -> SWord32
sFloatAsSWord32 SFloat
f

-- | Inverse transformation to 'sFloatAsComparableSWord32'.
sComparableSWord32AsSFloat :: SWord32 -> SFloat
sComparableSWord32AsSFloat :: SWord32 -> SFloat
sComparableSWord32AsSFloat SWord32
w = SWord32 -> SFloat
sWord32AsSFloat forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
sb (forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ SBool
sFalse forall a. a -> [a] -> [a]
: [SBool]
rest) (forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map SBool -> SBool
sNot [SBool]
allBits)
  where allBits :: [SBool]
allBits@(SBool
sb : [SBool]
rest) = forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SWord32
w

-- | Convert a double to a comparable 'SWord64'. The trick is to ignore the
-- sign of -0, and if it's a negative value flip all the bits, and otherwise
-- only flip the sign bit. This is known as the lexicographic ordering on doubles
-- and it works as long as you do not have a @NaN@.
sDoubleAsComparableSWord64 :: SDouble -> SWord64
sDoubleAsComparableSWord64 :: SDouble -> SWord64
sDoubleAsComparableSWord64 SDouble
d = forall a. Mergeable a => SBool -> a -> a -> a
ite (forall a. IEEEFloating a => SBV a -> SBool
fpIsNegativeZero SDouble
d) (SDouble -> SWord64
sDoubleAsComparableSWord64 SDouble
0) (forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot SBool
sb forall a. a -> [a] -> [a]
: forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
sb (forall a b. (a -> b) -> [a] -> [b]
map SBool -> SBool
sNot [SBool]
rest) [SBool]
rest)
  where (SBool
sb : [SBool]
rest) = forall a. SFiniteBits a => SBV a -> [SBool]
blastBE forall a b. (a -> b) -> a -> b
$ SDouble -> SWord64
sDoubleAsSWord64 SDouble
d

-- | Inverse transformation to 'sDoubleAsComparableSWord64'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@.
-- Otherwise, it's faithful:
sComparableSWord64AsSDouble :: SWord64 -> SDouble
sComparableSWord64AsSDouble :: SWord64 -> SDouble
sComparableSWord64AsSDouble SWord64
w = SWord64 -> SDouble
sWord64AsSDouble forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
sb (forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ SBool
sFalse forall a. a -> [a] -> [a]
: [SBool]
rest) (forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map SBool -> SBool
sNot [SBool]
allBits)
  where allBits :: [SBool]
allBits@(SBool
sb : [SBool]
rest) = forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SWord64
w

-- | 'Float' instance for 'Metric' goes through the lexicographic ordering on 'Word32'.
-- It implicitly makes sure that the value is not @NaN@.
instance Metric Float where

   type MetricSpace Float = Word32
   toMetricSpace :: SFloat -> SBV (MetricSpace Float)
toMetricSpace          = SFloat -> SWord32
sFloatAsComparableSWord32
   fromMetricSpace :: SBV (MetricSpace Float) -> SFloat
fromMetricSpace        = SWord32 -> SFloat
sComparableSWord32AsSFloat

   msMinimize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SFloat -> m ()
msMinimize [Char]
nm SFloat
o = do forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot forall a b. (a -> b) -> a -> b
$ forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SFloat
o
                        forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal forall a b. (a -> b) -> a -> b
$ forall a. SBV a -> SVal
unSBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. [Char] -> a -> Objective a
Minimize [Char]
nm (forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SFloat
o)

   msMaximize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SFloat -> m ()
msMaximize [Char]
nm SFloat
o = do forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot forall a b. (a -> b) -> a -> b
$ forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SFloat
o
                        forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal forall a b. (a -> b) -> a -> b
$ forall a. SBV a -> SVal
unSBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. [Char] -> a -> Objective a
Maximize [Char]
nm (forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SFloat
o)

-- | 'Double' instance for 'Metric' goes through the lexicographic ordering on 'Word64'.
-- It implicitly makes sure that the value is not @NaN@.
instance Metric Double where

   type MetricSpace Double = Word64
   toMetricSpace :: SDouble -> SBV (MetricSpace Double)
toMetricSpace           = SDouble -> SWord64
sDoubleAsComparableSWord64
   fromMetricSpace :: SBV (MetricSpace Double) -> SDouble
fromMetricSpace         = SWord64 -> SDouble
sComparableSWord64AsSDouble

   msMinimize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SDouble -> m ()
msMinimize [Char]
nm SDouble
o = do forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot forall a b. (a -> b) -> a -> b
$ forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SDouble
o
                        forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal forall a b. (a -> b) -> a -> b
$ forall a. SBV a -> SVal
unSBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. [Char] -> a -> Objective a
Minimize [Char]
nm (forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SDouble
o)

   msMaximize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SDouble -> m ()
msMaximize [Char]
nm SDouble
o = do forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot forall a b. (a -> b) -> a -> b
$ forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SDouble
o
                        forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal forall a b. (a -> b) -> a -> b
$ forall a. SBV a -> SVal
unSBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. [Char] -> a -> Objective a
Maximize [Char]
nm (forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SDouble
o)

-- | Real instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here.
instance ValidFloat eb sb => Real (FloatingPoint eb sb) where
  toRational :: FloatingPoint eb sb -> Rational
toRational (FloatingPoint (FP Int
_ Int
_ BigFloat
r)) = case BigFloat -> BFRep
bfToRep BigFloat
r of
                                            BFRep
BFNaN     -> forall a. Real a => a -> Rational
toRational (Double
0forall a. Fractional a => a -> a -> a
/Double
0 :: Double)
                                            BFRep Sign
s BFNum
n -> case BFNum
n of
                                                           BFNum
Zero    -> Integer
0 forall a. Integral a => a -> a -> Ratio a
% Integer
1
                                                           BFNum
Inf     -> (if Sign
s forall a. Eq a => a -> a -> Bool
== Sign
Neg then -Integer
1 else Integer
1) forall a. Integral a => a -> a -> Ratio a
% Integer
0
                                                           Num Integer
x Int64
y -> -- The value here is x * 2^y
                                                                      let v :: Integer
                                                                          v :: Integer
v   = Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ forall a. Num a => a -> a
abs (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
y :: Integer)
                                                                          sgn :: Rational -> Rational
sgn = if Sign
s forall a. Eq a => a -> a -> Bool
== Sign
Neg then ((-Rational
1) forall a. Num a => a -> a -> a
*) else forall a. a -> a
id
                                                                      in if Int64
y forall a. Ord a => a -> a -> Bool
> Int64
0
                                                                            then Rational -> Rational
sgn forall a b. (a -> b) -> a -> b
$ Integer
x forall a. Num a => a -> a -> a
* Integer
v forall a. Integral a => a -> a -> Ratio a
% Integer
1
                                                                            else Rational -> Rational
sgn forall a b. (a -> b) -> a -> b
$ Integer
x forall a. Integral a => a -> a -> Ratio a
% Integer
v

-- | RealFrac instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here.
instance ValidFloat eb sb => RealFrac (FloatingPoint eb sb) where
  properFraction :: forall b.
Integral b =>
FloatingPoint eb sb -> (b, FloatingPoint eb sb)
properFraction (FloatingPoint FP
f) = (b
a, forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint FP
b)
     where (b
a, FP
b) = forall a b. (RealFrac a, Integral b) => a -> (b, a)
properFraction FP
f

-- | RealFloat instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here.
instance ValidFloat eb sb => RealFloat (FloatingPoint eb sb) where
  floatRadix :: FloatingPoint eb sb -> Integer
floatRadix     (FloatingPoint FP
f) = forall a. RealFloat a => a -> Integer
floatRadix     FP
f
  floatDigits :: FloatingPoint eb sb -> Int
floatDigits    (FloatingPoint FP
f) = forall a. RealFloat a => a -> Int
floatDigits    FP
f
  floatRange :: FloatingPoint eb sb -> (Int, Int)
floatRange     (FloatingPoint FP
f) = forall a. RealFloat a => a -> (Int, Int)
floatRange     FP
f
  isNaN :: FloatingPoint eb sb -> Bool
isNaN          (FloatingPoint FP
f) = forall a. RealFloat a => a -> Bool
isNaN          FP
f
  isInfinite :: FloatingPoint eb sb -> Bool
isInfinite     (FloatingPoint FP
f) = forall a. RealFloat a => a -> Bool
isInfinite     FP
f
  isDenormalized :: FloatingPoint eb sb -> Bool
isDenormalized (FloatingPoint FP
f) = forall a. RealFloat a => a -> Bool
isDenormalized FP
f
  isNegativeZero :: FloatingPoint eb sb -> Bool
isNegativeZero (FloatingPoint FP
f) = forall a. RealFloat a => a -> Bool
isNegativeZero FP
f
  isIEEE :: FloatingPoint eb sb -> Bool
isIEEE         (FloatingPoint FP
f) = forall a. RealFloat a => a -> Bool
isIEEE         FP
f
  decodeFloat :: FloatingPoint eb sb -> (Integer, Int)
decodeFloat    (FloatingPoint FP
f) = forall a. RealFloat a => a -> (Integer, Int)
decodeFloat    FP
f

  encodeFloat :: Integer -> Int -> FloatingPoint eb sb
encodeFloat Integer
m Int
n = FloatingPoint eb sb
res
     where res :: FloatingPoint eb sb
res = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint forall a b. (a -> b) -> a -> b
$ Int -> Int -> Integer -> Int -> FP
fpEncodeFloat Int
ei Int
si Integer
m Int
n
           ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
           si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)

-- | Convert a float to the word containing the corresponding bit pattern
sFloatingPointAsSWord :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsSWord :: forall (eb :: Nat) (sb :: Nat).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsSWord (SBV SVal
v) = forall a. SVal -> SBV a
SBV (SVal -> SVal
svFloatingPointAsSWord SVal
v)

-- | Convert a float to the correct size word, that can be used in lexicographic ordering. Used in optimization.
sFloatingPointAsComparableSWord :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsComparableSWord :: forall (eb :: Nat) (sb :: Nat).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsComparableSWord SFloatingPoint eb sb
f = forall a. Mergeable a => SBool -> a -> a -> a
ite (forall a. IEEEFloating a => SBV a -> SBool
fpIsNegativeZero SFloatingPoint eb sb
f) SBV (WordN (eb + sb))
posZero (forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot SBool
sb forall a. a -> [a] -> [a]
: forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
sb (forall a b. (a -> b) -> [a] -> [b]
map SBool -> SBool
sNot [SBool]
rest) [SBool]
rest)
  where posZero :: SBV (WordN (eb + sb))
posZero     = forall (eb :: Nat) (sb :: Nat).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsComparableSWord (SFloatingPoint eb sb
0 :: SFloatingPoint eb sb)
        (SBool
sb : [SBool]
rest) = forall a. SFiniteBits a => SBV a -> [SBool]
blastBE (forall (eb :: Nat) (sb :: Nat).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsSWord SFloatingPoint eb sb
f :: SWord (eb + sb))

-- | Inverse transformation to 'sFloatingPointAsComparableSWord'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@.
-- Otherwise, it's faithful:
sComparableSWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb
sComparableSWordAsSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
(KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
SWord (eb + sb) -> SFloatingPoint eb sb
sComparableSWordAsSFloatingPoint SBV (WordN (eb + sb))
w = forall (eb :: Nat) (sb :: Nat).
(KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
SWord (eb + sb) -> SFloatingPoint eb sb
sWordAsSFloatingPoint forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
signBit (forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ SBool
sFalse forall a. a -> [a] -> [a]
: [SBool]
rest) (forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map SBool -> SBool
sNot [SBool]
allBits)
  where allBits :: [SBool]
allBits@(SBool
signBit : [SBool]
rest) = forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SBV (WordN (eb + sb))
w

-- | Convert a word to an arbitrary float, by reinterpreting the bits of the word as the corresponding bits of the float.
sWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb
sWordAsSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
(KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
SWord (eb + sb) -> SFloatingPoint eb sb
sWordAsSFloatingPoint SWord (eb + sb)
sw
   | Just (WordN (eb + sb)
f :: WordN (eb + sb)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SWord (eb + sb)
sw
   = let ext :: Int -> Bool
ext Int
i = WordN (eb + sb)
f forall a. Bits a => a -> Int -> Bool
`testBit` Int
i
         exts :: [Int] -> [Bool]
exts  = forall a b. (a -> b) -> [a] -> [b]
map Int -> Bool
ext
         (Bool
s, [Bool]
ebits, [Bool]
sigbits) = (Int -> Bool
ext (Int
ei forall a. Num a => a -> a -> a
+ Int
si forall a. Num a => a -> a -> a
- Int
1), [Int] -> [Bool]
exts [Int
ei forall a. Num a => a -> a -> a
+ Int
si forall a. Num a => a -> a -> a
- Int
2, Int
ei forall a. Num a => a -> a -> a
+ Int
si forall a. Num a => a -> a -> a
- Int
3 .. Int
si forall a. Num a => a -> a -> a
- Int
1], [Int] -> [Bool]
exts [Int
si forall a. Num a => a -> a -> a
- Int
2, Int
si forall a. Num a => a -> a -> a
- Int
3 .. Int
0])

         cvt :: [Bool] -> Integer
         cvt :: [Bool] -> Integer
cvt = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Bool
b Integer
sofar -> Integer
2 forall a. Num a => a -> a -> a
* Integer
sofar forall a. Num a => a -> a -> a
+ if Bool
b then Integer
1 else Integer
0) Integer
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse

         eIntV :: Integer
eIntV = [Bool] -> Integer
cvt [Bool]
ebits
         sIntV :: Integer
sIntV = [Bool] -> Integer
cvt [Bool]
sigbits
         fp :: FP
fp    = Bool -> (Integer, Int) -> (Integer, Int) -> FP
fpFromRawRep Bool
s (Integer
eIntV, Int
ei) (Integer
sIntV, Int
si)
     in forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint FP
fp
   | Bool
True
   = forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kTo (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
y)))
   where ei :: Int
ei   = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
         si :: Int
si   = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)
         kTo :: Kind
kTo  = Int -> Int -> Kind
KFP Int
ei Int
si
         y :: State -> IO SV
y State
st = do SV
xsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SWord (eb + sb)
sw
                   State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kTo (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret (forall a. HasKind a => a -> Kind
kindOf SWord (eb + sb)
sw) Kind
kTo)) [SV
xsv])

instance (BVIsNonZero (eb + sb), KnownNat (eb + sb), ValidFloat eb sb) => Metric (FloatingPoint eb sb) where

   type MetricSpace (FloatingPoint eb sb) = WordN (eb + sb)
   toMetricSpace :: SBV (FloatingPoint eb sb)
-> SBV (MetricSpace (FloatingPoint eb sb))
toMetricSpace                          = forall (eb :: Nat) (sb :: Nat).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsComparableSWord
   fromMetricSpace :: SBV (MetricSpace (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb)
fromMetricSpace                        = forall (eb :: Nat) (sb :: Nat).
(KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
SWord (eb + sb) -> SFloatingPoint eb sb
sComparableSWordAsSFloatingPoint

   msMinimize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SBV (FloatingPoint eb sb) -> m ()
msMinimize [Char]
nm SBV (FloatingPoint eb sb)
o = do forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot forall a b. (a -> b) -> a -> b
$ forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SBV (FloatingPoint eb sb)
o
                        forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal forall a b. (a -> b) -> a -> b
$ forall a. SBV a -> SVal
unSBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. [Char] -> a -> Objective a
Minimize [Char]
nm (forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SBV (FloatingPoint eb sb)
o)

   msMaximize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SBV (FloatingPoint eb sb) -> m ()
msMaximize [Char]
nm SBV (FloatingPoint eb sb)
o = do forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot forall a b. (a -> b) -> a -> b
$ forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SBV (FloatingPoint eb sb)
o
                        forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal forall a b. (a -> b) -> a -> b
$ forall a. SBV a -> SVal
unSBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. [Char] -> a -> Objective a
Maximize [Char]
nm (forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SBV (FloatingPoint eb sb)
o)

-- Map SBV's rounding modes to LibBF's
rmToRM :: SRoundingMode -> Maybe RoundMode
rmToRM :: SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
srm = RoundingMode -> RoundMode
cvt forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => SBV a -> Maybe a
unliteral SRoundingMode
srm
  where cvt :: RoundingMode -> RoundMode
cvt RoundingMode
RoundNearestTiesToEven = RoundMode
NearEven
        cvt RoundingMode
RoundNearestTiesToAway = RoundMode
NearAway
        cvt RoundingMode
RoundTowardPositive    = RoundMode
ToPosInf
        cvt RoundingMode
RoundTowardNegative    = RoundMode
ToNegInf
        cvt RoundingMode
RoundTowardZero        = RoundMode
ToZero

-- | Lift a 1 arg Big-float op
lift1FP :: forall eb sb. ValidFloat eb sb =>
           (BFOpts -> BigFloat -> (BigFloat, Status))
        -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
        -> SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
lift1FP :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
(BFOpts -> BigFloat -> (BigFloat, Status))
-> (Maybe SRoundingMode
    -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
lift1FP BFOpts -> BigFloat -> (BigFloat, Status)
bfOp Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb
mkDef SRoundingMode
rm SFloatingPoint eb sb
a
  | Just (FloatingPoint (FP Int
_ Int
_ BigFloat
v)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SFloatingPoint eb sb
a
  , Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (Int -> Int -> BigFloat -> FP
FP Int
ei Int
si (forall a b. (a, b) -> a
fst (BFOpts -> BigFloat -> (BigFloat, Status)
bfOp (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
ei Int
si RoundMode
brm) BigFloat
v)))
  | Bool
True
  = Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb
mkDef (forall a. a -> Maybe a
Just SRoundingMode
rm) SFloatingPoint eb sb
a
  where ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
        si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)

-- | Lift a 2 arg Big-float op
lift2FP :: forall eb sb. ValidFloat eb sb =>
           (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
        -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
        -> SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
lift2FP :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> (Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb)
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfOp Maybe SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
mkDef SRoundingMode
rm SFloatingPoint eb sb
a SFloatingPoint eb sb
b
  | Just (FloatingPoint (FP Int
_ Int
_ BigFloat
v1)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SFloatingPoint eb sb
a
  , Just (FloatingPoint (FP Int
_ Int
_ BigFloat
v2)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SFloatingPoint eb sb
b
  , Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (Int -> Int -> BigFloat -> FP
FP Int
ei Int
si (forall a b. (a, b) -> a
fst (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfOp (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
ei Int
si RoundMode
brm) BigFloat
v1 BigFloat
v2)))
  | Bool
True
  = Maybe SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
mkDef (forall a. a -> Maybe a
Just SRoundingMode
rm) SFloatingPoint eb sb
a SFloatingPoint eb sb
b
  where ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
        si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)

-- | Lift a 3 arg Big-float op
lift3FP :: forall eb sb. ValidFloat eb sb =>
           (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
        -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
        -> SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
lift3FP :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
(BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
-> (Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb)
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
lift3FP BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
bfOp Maybe SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
mkDef SRoundingMode
rm SFloatingPoint eb sb
a SFloatingPoint eb sb
b SFloatingPoint eb sb
c
  | Just (FloatingPoint (FP Int
_ Int
_ BigFloat
v1)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SFloatingPoint eb sb
a
  , Just (FloatingPoint (FP Int
_ Int
_ BigFloat
v2)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SFloatingPoint eb sb
b
  , Just (FloatingPoint (FP Int
_ Int
_ BigFloat
v3)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SFloatingPoint eb sb
c
  , Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (Int -> Int -> BigFloat -> FP
FP Int
ei Int
si (forall a b. (a, b) -> a
fst (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
bfOp (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
ei Int
si RoundMode
brm) BigFloat
v1 BigFloat
v2 BigFloat
v3)))
  | Bool
True
  = Maybe SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
mkDef (forall a. a -> Maybe a
Just SRoundingMode
rm) SFloatingPoint eb sb
a SFloatingPoint eb sb
b SFloatingPoint eb sb
c
  where ei :: Int
ei = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb)
        si :: Int
si = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb)

-- Sized-floats have a special instance, since it can handle arbitrary rounding modes when it matters.
instance ValidFloat eb sb => IEEEFloating (FloatingPoint eb sb) where
  fpAdd :: SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
fpAdd  = forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> (Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb)
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfAdd      (forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2 FPOp
FP_Add  (forall a. a -> Maybe a
Just forall a. Num a => a -> a -> a
(+)))
  fpSub :: SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
fpSub  = forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> (Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb)
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfSub      (forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2 FPOp
FP_Sub  (forall a. a -> Maybe a
Just (-)))
  fpMul :: SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
fpMul  = forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> (Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb)
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfMul      (forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2 FPOp
FP_Mul  (forall a. a -> Maybe a
Just forall a. Num a => a -> a -> a
(*)))
  fpDiv :: SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
fpDiv  = forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> (Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb)
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfDiv      (forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
lift2 FPOp
FP_Div  (forall a. a -> Maybe a
Just forall a. Fractional a => a -> a -> a
(/)))
  fpFMA :: SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
fpFMA  = forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
(BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
-> (Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb)
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
lift3FP BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
bfFMA      (forall a.
SymVal a =>
FPOp
-> Maybe (a -> a -> a -> a)
-> Maybe SRoundingMode
-> SBV a
-> SBV a
-> SBV a
-> SBV a
lift3 FPOp
FP_FMA  forall a. Maybe a
Nothing)
  fpSqrt :: SRoundingMode
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
fpSqrt = forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
(BFOpts -> BigFloat -> (BigFloat, Status))
-> (Maybe SRoundingMode
    -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
lift1FP BFOpts -> BigFloat -> (BigFloat, Status)
bfSqrt     (forall a.
SymVal a =>
FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
lift1 FPOp
FP_Sqrt (forall a. a -> Maybe a
Just forall a. Floating a => a -> a
sqrt))

  fpRoundToIntegral :: SRoundingMode
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
fpRoundToIntegral SRoundingMode
rm SBV (FloatingPoint eb sb)
a
    | Just (FloatingPoint (FP Int
ei Int
si BigFloat
v)) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV (FloatingPoint eb sb)
a
    , Just RoundMode
brm <- SRoundingMode -> Maybe RoundMode
rmToRM SRoundingMode
rm
    = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (Int -> Int -> BigFloat -> FP
FP Int
ei Int
si (forall a b. (a, b) -> a
fst (RoundMode -> BigFloat -> (BigFloat, Status)
bfRoundInt RoundMode
brm BigFloat
v)))
    | Bool
True
    = forall a.
SymVal a =>
FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
lift1 FPOp
FP_RoundToIntegral (forall a. a -> Maybe a
Just forall a. RealFloat a => a -> a
fpRoundToIntegralH) (forall a. a -> Maybe a
Just SRoundingMode
rm) SBV (FloatingPoint eb sb)
a

  -- All other operations are agnostic to the rounding mode, hence the defaults are sufficient:
  --
  --       fpAbs            :: SBV a -> SBV a
  --       fpNeg            :: SBV a -> SBV a
  --       fpRem            :: SBV a -> SBV a -> SBV a
  --       fpMin            :: SBV a -> SBV a -> SBV a
  --       fpMax            :: SBV a -> SBV a -> SBV a
  --       fpIsEqualObject  :: SBV a -> SBV a -> SBool
  --       fpIsNormal       :: SBV a -> SBool
  --       fpIsSubnormal    :: SBV a -> SBool
  --       fpIsZero         :: SBV a -> SBool
  --       fpIsInfinite     :: SBV a -> SBool
  --       fpIsNaN          :: SBV a -> SBool
  --       fpIsNegative     :: SBV a -> SBool
  --       fpIsPositive     :: SBV a -> SBool
  --       fpIsNegativeZero :: SBV a -> SBool
  --       fpIsPositiveZero :: SBV a -> SBool
  --       fpIsPoint        :: SBV a -> SBool

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}