{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module What4.Interface
(
SymExpr
, BoundVar
, SymFn
, SymAnnotation
, IsExpr(..)
, IsSymFn(..)
, SomeSymFn(..)
, SymFnWrapper(..)
, UnfoldPolicy(..)
, shouldUnfold
, IsExprBuilder(..)
, IsSymExprBuilder(..)
, SolverEvent(..)
, SolverStartSATQuery(..)
, SolverEndSATQuery(..)
, bvJoinVector
, bvSplitVector
, bvSwap
, bvBitreverse
, RoundingMode(..)
, Statistics(..)
, zeroStatistics
, Pred
, SymInteger
, SymReal
, SymFloat
, SymString
, SymCplx
, SymStruct
, SymBV
, SymArray
, SymNat
, asNat
, natLit
, natAdd
, natSub
, natMul
, natDiv
, natMod
, natIte
, natEq
, natLe
, natLt
, natToInteger
, natToIntegerPure
, bvToNat
, natToReal
, integerToNat
, realToNat
, freshBoundedNat
, freshNat
, printSymNat
, IndexLit(..)
, indexLit
, ArrayResultWrapper(..)
, asConcrete
, concreteToSym
, baseIsConcrete
, baseDefaultValue
, realExprAsInteger
, rationalAsInteger
, cplxExprAsRational
, cplxExprAsInteger
, SymEncoder(..)
, backendPred
, andAllOf
, orOneOf
, itePredM
, iteM
, iteList
, predToReal
, cplxDiv
, cplxLog
, cplxLogBase
, mkRational
, mkReal
, isNonZero
, isReal
, muxRange
, InvalidRange(..)
, module Data.Parameterized.NatRepr
, module What4.BaseTypes
, HasAbsValue
, What4.Symbol.SolverSymbol
, What4.Symbol.emptySymbol
, What4.Symbol.userSymbol
, What4.Symbol.safeSymbol
, ValueRange(..)
, StringLiteral(..)
, stringLiteralInfo
) where
#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail( MonadFail )
#endif
import Control.Exception (assert, Exception)
import Control.Lens
import Control.Monad
import Control.Monad.IO.Class
import qualified Data.BitVector.Sized as BV
import Data.Coerce (coerce)
import Data.Foldable
import Data.Kind ( Type )
import qualified Data.Map as Map
import Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Ctx
import Data.Parameterized.Utils.Endian (Endian(..))
import Data.Parameterized.Map (MapF)
import Data.Parameterized.NatRepr
import Data.Parameterized.TraversableFC
import qualified Data.Parameterized.Vector as Vector
import Data.Ratio
import Data.Scientific (Scientific)
import Data.Set (Set)
import GHC.Generics (Generic)
import Numeric.Natural
import LibBF (BigFloat)
import Prettyprinter (Doc)
import What4.BaseTypes
import What4.Config
import qualified What4.Expr.ArrayUpdateMap as AUM
import What4.IndexLit
import What4.ProgramLoc
import What4.Concrete
import What4.SatResult
import What4.SpecialFunctions
import What4.Symbol
import What4.Utils.AbstractDomains
import What4.Utils.Arithmetic
import What4.Utils.Complex
import What4.Utils.FloatHelpers (RoundingMode(..))
import What4.Utils.StringLiteral
type Pred sym = SymExpr sym BaseBoolType
type SymInteger sym = SymExpr sym BaseIntegerType
type SymReal sym = SymExpr sym BaseRealType
type SymFloat sym fpp = SymExpr sym (BaseFloatType fpp)
type SymCplx sym = SymExpr sym BaseComplexType
type SymStruct sym flds = SymExpr sym (BaseStructType flds)
type SymArray sym idx b = SymExpr sym (BaseArrayType idx b)
type SymBV sym n = SymExpr sym (BaseBVType n)
type SymString sym si = SymExpr sym (BaseStringType si)
type family SymExpr (sym :: Type) :: BaseType -> Type
type family BoundVar (sym :: Type) :: BaseType -> Type
type family SymAnnotation (sym :: Type) :: BaseType -> Type
itePredM :: (IsExpr (SymExpr sym), IsExprBuilder sym, MonadIO m)
=> sym
-> Pred sym
-> m (Pred sym)
-> m (Pred sym)
-> m (Pred sym)
itePredM :: forall sym (m :: Type -> Type).
(IsExpr (SymExpr sym), IsExprBuilder sym, MonadIO m) =>
sym -> Pred sym -> m (Pred sym) -> m (Pred sym) -> m (Pred sym)
itePredM sym
sym Pred sym
c m (Pred sym)
mx m (Pred sym)
my =
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
c of
Just Bool
True -> m (Pred sym)
mx
Just Bool
False -> m (Pred sym)
my
Maybe Bool
Nothing -> do
Pred sym
x <- m (Pred sym)
mx
Pred sym
y <- m (Pred sym)
my
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
c Pred sym
x Pred sym
y
class HasAbsValue e => IsExpr e where
asConstantPred :: e BaseBoolType -> Maybe Bool
asConstantPred e BaseBoolType
_ = forall a. Maybe a
Nothing
asInteger :: e BaseIntegerType -> Maybe Integer
asInteger e BaseIntegerType
_ = forall a. Maybe a
Nothing
integerBounds :: e BaseIntegerType -> ValueRange Integer
asRational :: e BaseRealType -> Maybe Rational
asRational e BaseRealType
_ = forall a. Maybe a
Nothing
asFloat :: e (BaseFloatType fpp) -> Maybe BigFloat
rationalBounds :: e BaseRealType -> ValueRange Rational
asComplex :: e BaseComplexType -> Maybe (Complex Rational)
asComplex e BaseComplexType
_ = forall a. Maybe a
Nothing
asBV :: e (BaseBVType w) -> Maybe (BV.BV w)
asBV e (BaseBVType w)
_ = forall a. Maybe a
Nothing
unsignedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)
signedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)
asAffineVar :: e tp -> Maybe (ConcreteVal tp, e tp, ConcreteVal tp)
asString :: e (BaseStringType si) -> Maybe (StringLiteral si)
asString e (BaseStringType si)
_ = forall a. Maybe a
Nothing
stringInfo :: e (BaseStringType si) -> StringInfoRepr si
stringInfo e (BaseStringType si)
e =
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType e (BaseStringType si)
e of
BaseStringRepr StringInfoRepr si
si -> StringInfoRepr si
si
asConstantArray :: e (BaseArrayType idx bt) -> Maybe (e bt)
asConstantArray e (BaseArrayType idx bt)
_ = forall a. Maybe a
Nothing
asStruct :: e (BaseStructType flds) -> Maybe (Ctx.Assignment e flds)
asStruct e (BaseStructType flds)
_ = forall a. Maybe a
Nothing
exprType :: e tp -> BaseTypeRepr tp
bvWidth :: e (BaseBVType w) -> NatRepr w
bvWidth e (BaseBVType w)
e =
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType e (BaseBVType w)
e of
BaseBVRepr NatRepr w
w -> NatRepr w
w
floatPrecision :: e (BaseFloatType fpp) -> FloatPrecisionRepr fpp
floatPrecision e (BaseFloatType fpp)
e =
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType e (BaseFloatType fpp)
e of
BaseFloatRepr FloatPrecisionRepr fpp
fpp -> FloatPrecisionRepr fpp
fpp
printSymExpr :: e tp -> Doc ann
unsafeSetAbstractValue :: AbstractValue tp -> e tp -> e tp
newtype ArrayResultWrapper f idx tp =
ArrayResultWrapper { forall (f :: BaseType -> Type) (idx :: Ctx BaseType)
(tp :: BaseType).
ArrayResultWrapper f idx tp -> f (BaseArrayType idx tp)
unwrapArrayResult :: f (BaseArrayType idx tp) }
instance TestEquality f => TestEquality (ArrayResultWrapper f idx) where
testEquality :: forall (a :: BaseType) (b :: BaseType).
ArrayResultWrapper f idx a
-> ArrayResultWrapper f idx b -> Maybe (a :~: b)
testEquality (ArrayResultWrapper f (BaseArrayType idx a)
x) (ArrayResultWrapper f (BaseArrayType idx b)
y) = do
BaseArrayType idx a :~: BaseArrayType idx b
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f (BaseArrayType idx a)
x f (BaseArrayType idx b)
y
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
instance HashableF e => HashableF (ArrayResultWrapper e idx) where
hashWithSaltF :: forall (tp :: BaseType). Int -> ArrayResultWrapper e idx tp -> Int
hashWithSaltF Int
s (ArrayResultWrapper e (BaseArrayType idx tp)
v) = forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF Int
s e (BaseArrayType idx tp)
v
data SolverEvent
= SolverStartSATQuery SolverStartSATQuery
| SolverEndSATQuery SolverEndSATQuery
deriving (Int -> SolverEvent -> ShowS
[SolverEvent] -> ShowS
SolverEvent -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolverEvent] -> ShowS
$cshowList :: [SolverEvent] -> ShowS
show :: SolverEvent -> String
$cshow :: SolverEvent -> String
showsPrec :: Int -> SolverEvent -> ShowS
$cshowsPrec :: Int -> SolverEvent -> ShowS
Show, forall x. Rep SolverEvent x -> SolverEvent
forall x. SolverEvent -> Rep SolverEvent x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SolverEvent x -> SolverEvent
$cfrom :: forall x. SolverEvent -> Rep SolverEvent x
Generic)
data SolverStartSATQuery = SolverStartSATQueryRec
{ SolverStartSATQuery -> String
satQuerySolverName :: !String
, SolverStartSATQuery -> String
satQueryReason :: !String
}
deriving (Int -> SolverStartSATQuery -> ShowS
[SolverStartSATQuery] -> ShowS
SolverStartSATQuery -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolverStartSATQuery] -> ShowS
$cshowList :: [SolverStartSATQuery] -> ShowS
show :: SolverStartSATQuery -> String
$cshow :: SolverStartSATQuery -> String
showsPrec :: Int -> SolverStartSATQuery -> ShowS
$cshowsPrec :: Int -> SolverStartSATQuery -> ShowS
Show, forall x. Rep SolverStartSATQuery x -> SolverStartSATQuery
forall x. SolverStartSATQuery -> Rep SolverStartSATQuery x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SolverStartSATQuery x -> SolverStartSATQuery
$cfrom :: forall x. SolverStartSATQuery -> Rep SolverStartSATQuery x
Generic)
data SolverEndSATQuery = SolverEndSATQueryRec
{ SolverEndSATQuery -> SatResult () ()
satQueryResult :: !(SatResult () ())
, SolverEndSATQuery -> Maybe String
satQueryError :: !(Maybe String)
}
deriving (Int -> SolverEndSATQuery -> ShowS
[SolverEndSATQuery] -> ShowS
SolverEndSATQuery -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolverEndSATQuery] -> ShowS
$cshowList :: [SolverEndSATQuery] -> ShowS
show :: SolverEndSATQuery -> String
$cshow :: SolverEndSATQuery -> String
showsPrec :: Int -> SolverEndSATQuery -> ShowS
$cshowsPrec :: Int -> SolverEndSATQuery -> ShowS
Show, forall x. Rep SolverEndSATQuery x -> SolverEndSATQuery
forall x. SolverEndSATQuery -> Rep SolverEndSATQuery x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SolverEndSATQuery x -> SolverEndSATQuery
$cfrom :: forall x. SolverEndSATQuery -> Rep SolverEndSATQuery x
Generic)
newtype SymNat sym =
SymNat
{
forall sym. SymNat sym -> SymExpr sym BaseIntegerType
_symNat :: SymExpr sym BaseIntegerType
}
asNat :: IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat :: forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Nat
asNat (SymNat SymExpr sym BaseIntegerType
x) = forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> a
max Integer
0 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
asInteger SymExpr sym BaseIntegerType
x
natLit :: IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit :: forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
x = forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym (forall a. Integral a => a -> Integer
toInteger Nat
x)
natAdd :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natAdd :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natAdd sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intAdd sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y
natSub :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natSub :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natSub sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) =
do SymExpr sym BaseIntegerType
z <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intSub sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y
forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMax sym
sym SymExpr sym BaseIntegerType
z forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
0)
natMul :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMul :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMul sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMul sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y
natDiv :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natDiv :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natDiv sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intDiv sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y
natMod :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMod :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMod sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMod sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y
natIte :: IsExprBuilder sym => sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte :: forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte sym
sym Pred sym
p (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym Pred sym
p SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y
natEq :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intEq sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y
natLe :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe sym
sym (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y
natLt :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLt :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLt sym
sym SymNat sym
x SymNat sym
y = forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe sym
sym SymNat sym
y SymNat sym
x
natToInteger :: IsExprBuilder sym => sym -> SymNat sym -> IO (SymInteger sym)
natToInteger :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> IO (SymInteger sym)
natToInteger sym
_sym (SymNat SymExpr sym BaseIntegerType
x) = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymExpr sym BaseIntegerType
x
natToIntegerPure :: SymNat sym -> SymInteger sym
natToIntegerPure :: forall sym. SymNat sym -> SymExpr sym BaseIntegerType
natToIntegerPure (SymNat SymExpr sym BaseIntegerType
x) = SymExpr sym BaseIntegerType
x
bvToNat :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymNat sym)
bvToNat :: forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymNat sym)
bvToNat sym
sym SymBV sym w
x = forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
bvToInteger sym
sym SymBV sym w
x
natToReal :: IsExprBuilder sym => sym -> SymNat sym -> IO (SymReal sym)
natToReal :: forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> IO (SymReal sym)
natToReal sym
sym = forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> IO (SymInteger sym)
natToInteger sym
sym forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym
integerToNat :: IsExprBuilder sym => sym -> SymInteger sym -> IO (SymNat sym)
integerToNat :: forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymNat sym)
integerToNat sym
sym SymInteger sym
x = forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMax sym
sym SymInteger sym
x forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
0)
realToNat :: IsExprBuilder sym => sym -> SymReal sym -> IO (SymNat sym)
realToNat :: forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymNat sym)
realToNat sym
sym SymReal sym
r = forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realToInteger sym
sym SymReal sym
r forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymNat sym)
integerToNat sym
sym
freshBoundedNat ::
IsSymExprBuilder sym =>
sym ->
SolverSymbol ->
Maybe Natural ->
Maybe Natural ->
IO (SymNat sym)
freshBoundedNat :: forall sym.
IsSymExprBuilder sym =>
sym -> SolverSymbol -> Maybe Nat -> Maybe Nat -> IO (SymNat sym)
freshBoundedNat sym
sym SolverSymbol
s Maybe Nat
lo Maybe Nat
hi = forall sym. SymExpr sym BaseIntegerType -> SymNat sym
SymNat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Maybe Integer
-> Maybe Integer
-> IO (SymInteger sym)
freshBoundedInt sym
sym SolverSymbol
s Maybe Integer
lo' Maybe Integer
hi')
where
lo' :: Maybe Integer
lo' = forall a. a -> Maybe a
Just (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Integer
0 forall a. Integral a => a -> Integer
toInteger Maybe Nat
lo)
hi' :: Maybe Integer
hi' = forall a. Integral a => a -> Integer
toInteger forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Nat
hi
freshNat :: IsSymExprBuilder sym => sym -> SolverSymbol -> IO (SymNat sym)
freshNat :: forall sym.
IsSymExprBuilder sym =>
sym -> SolverSymbol -> IO (SymNat sym)
freshNat sym
sym SolverSymbol
s = forall sym.
IsSymExprBuilder sym =>
sym -> SolverSymbol -> Maybe Nat -> Maybe Nat -> IO (SymNat sym)
freshBoundedNat sym
sym SolverSymbol
s (forall a. a -> Maybe a
Just Nat
0) forall a. Maybe a
Nothing
printSymNat :: IsExpr (SymExpr sym) => SymNat sym -> Doc ann
printSymNat :: forall sym ann. IsExpr (SymExpr sym) => SymNat sym -> Doc ann
printSymNat (SymNat SymExpr sym BaseIntegerType
x) = forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym BaseIntegerType
x
instance TestEquality (SymExpr sym) => Eq (SymNat sym) where
SymNat SymExpr sym BaseIntegerType
x == :: SymNat sym -> SymNat sym -> Bool
== SymNat SymExpr sym BaseIntegerType
y = forall a. Maybe a -> Bool
isJust (forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y)
instance OrdF (SymExpr sym) => Ord (SymNat sym) where
compare :: SymNat sym -> SymNat sym -> Ordering
compare (SymNat SymExpr sym BaseIntegerType
x) (SymNat SymExpr sym BaseIntegerType
y) = forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF SymExpr sym BaseIntegerType
x SymExpr sym BaseIntegerType
y)
instance (HashableF (SymExpr sym), TestEquality (SymExpr sym)) => Hashable (SymNat sym) where
hashWithSalt :: Int -> SymNat sym -> Int
hashWithSalt Int
s (SymNat SymExpr sym BaseIntegerType
x) = forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF Int
s SymExpr sym BaseIntegerType
x
class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
, TestEquality (SymAnnotation sym), OrdF (SymAnnotation sym)
, HashableF (SymAnnotation sym)
) => IsExprBuilder sym where
getConfiguration :: sym -> Config
setSolverLogListener :: sym -> Maybe (SolverEvent -> IO ()) -> IO ()
getSolverLogListener :: sym -> IO (Maybe (SolverEvent -> IO ()))
logSolverEvent :: sym -> SolverEvent -> IO ()
getStatistics :: sym -> IO Statistics
getStatistics sym
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return Statistics
zeroStatistics
getCurrentProgramLoc :: sym -> IO ProgramLoc
setCurrentProgramLoc :: sym -> ProgramLoc -> IO ()
isEq :: sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
isEq sym
sym SymExpr sym tp
x SymExpr sym tp
y =
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymExpr sym tp
x of
BaseTypeRepr tp
BaseBoolRepr -> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
eqPred sym
sym SymExpr sym tp
x SymExpr sym tp
y
BaseBVRepr{} -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym tp
x SymExpr sym tp
y
BaseTypeRepr tp
BaseIntegerRepr -> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intEq sym
sym SymExpr sym tp
x SymExpr sym tp
y
BaseTypeRepr tp
BaseRealRepr -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymExpr sym tp
x SymExpr sym tp
y
BaseFloatRepr{} -> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
floatEq sym
sym SymExpr sym tp
x SymExpr sym tp
y
BaseTypeRepr tp
BaseComplexRepr -> forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
cplxEq sym
sym SymExpr sym tp
x SymExpr sym tp
y
BaseStringRepr{} -> forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
stringEq sym
sym SymExpr sym tp
x SymExpr sym tp
y
BaseStructRepr{} -> forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> SymStruct sym flds -> IO (Pred sym)
structEq sym
sym SymExpr sym tp
x SymExpr sym tp
y
BaseArrayRepr{} -> forall sym (idx :: Ctx BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym -> SymArray sym idx b -> SymArray sym idx b -> IO (Pred sym)
arrayEq sym
sym SymExpr sym tp
x SymExpr sym tp
y
baseTypeIte :: sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
baseTypeIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y =
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymExpr sym tp
x of
BaseTypeRepr tp
BaseBoolRepr -> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y
BaseBVRepr{} -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y
BaseTypeRepr tp
BaseIntegerRepr -> forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y
BaseTypeRepr tp
BaseRealRepr -> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y
BaseFloatRepr{} -> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y
BaseStringRepr{} -> forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymString sym si
-> SymString sym si
-> IO (SymString sym si)
stringIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y
BaseTypeRepr tp
BaseComplexRepr -> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y
BaseStructRepr{} -> forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymStruct sym flds
-> SymStruct sym flds
-> IO (SymStruct sym flds)
structIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y
BaseArrayRepr{} -> forall sym (idx :: Ctx BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymArray sym idx b
-> SymArray sym idx b
-> IO (SymArray sym idx b)
arrayIte sym
sym Pred sym
c SymExpr sym tp
x SymExpr sym tp
y
annotateTerm :: sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
getAnnotation :: sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp)
getUnannotatedTerm :: sym -> SymExpr sym tp -> Maybe (SymExpr sym tp)
truePred :: sym -> Pred sym
falsePred :: sym -> Pred sym
notPred :: sym -> Pred sym -> IO (Pred sym)
andPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
impliesPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
impliesPred sym
sym Pred sym
x Pred sym
y = do
Pred sym
nx <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
x
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
y Pred sym
nx
xorPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
eqPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred :: sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
intLit :: sym -> Integer -> IO (SymInteger sym)
intNeg :: sym -> SymInteger sym -> IO (SymInteger sym)
intAdd :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intSub :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intSub sym
sym SymInteger sym
x SymInteger sym
y = forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intAdd sym
sym SymInteger sym
x forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
intNeg sym
sym SymInteger sym
y
intMul :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMin :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMin sym
sym SymInteger sym
x SymInteger sym
y =
do Pred sym
x_le_y <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
x SymInteger sym
y
Pred sym
y_le_x <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
y SymInteger sym
x
case (forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
x_le_y, forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
y_le_x) of
(Just Bool
True, Maybe Bool
_) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymInteger sym
x
(Maybe Bool
_, Just Bool
False) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymInteger sym
x
(Just Bool
False, Maybe Bool
_) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymInteger sym
y
(Maybe Bool
_, Just Bool
True) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymInteger sym
y
(Maybe Bool, Maybe Bool)
_ ->
do let rng_x :: ValueRange Integer
rng_x = forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> ValueRange Integer
integerBounds SymInteger sym
x
let rng_y :: ValueRange Integer
rng_y = forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> ValueRange Integer
integerBounds SymInteger sym
y
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
AbstractValue tp -> e tp -> e tp
unsafeSetAbstractValue (forall a. Ord a => ValueRange a -> ValueRange a -> ValueRange a
rangeMin ValueRange Integer
rng_x ValueRange Integer
rng_y) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym Pred sym
x_le_y SymInteger sym
x SymInteger sym
y
intMax :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMax sym
sym SymInteger sym
x SymInteger sym
y =
do Pred sym
x_le_y <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
x SymInteger sym
y
Pred sym
y_le_x <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
y SymInteger sym
x
case (forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
x_le_y, forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
y_le_x) of
(Just Bool
True, Maybe Bool
_) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymInteger sym
y
(Maybe Bool
_, Just Bool
False) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymInteger sym
y
(Just Bool
False, Maybe Bool
_) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymInteger sym
x
(Maybe Bool
_, Just Bool
True) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymInteger sym
x
(Maybe Bool, Maybe Bool)
_ ->
do let rng_x :: ValueRange Integer
rng_x = forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> ValueRange Integer
integerBounds SymInteger sym
x
let rng_y :: ValueRange Integer
rng_y = forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> ValueRange Integer
integerBounds SymInteger sym
y
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
AbstractValue tp -> e tp -> e tp
unsafeSetAbstractValue (forall a. Ord a => ValueRange a -> ValueRange a -> ValueRange a
rangeMax ValueRange Integer
rng_x ValueRange Integer
rng_y) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym Pred sym
x_le_y SymInteger sym
y SymInteger sym
x
intIte :: sym -> Pred sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intEq :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
x SymInteger sym
y = forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
y SymInteger sym
x
intAbs :: sym -> SymInteger sym -> IO (SymInteger sym)
intDiv :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMod :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intDivisible :: sym -> SymInteger sym -> Natural -> IO (Pred sym)
bvLit :: (1 <= w) => sym -> NatRepr w -> BV.BV w -> IO (SymBV sym w)
bvConcat :: (1 <= u, 1 <= v)
=> sym
-> SymBV sym u
-> SymBV sym v
-> IO (SymBV sym (u+v))
bvSelect :: forall idx n w. (1 <= n, idx + n <= w)
=> sym
-> NatRepr idx
-> NatRepr n
-> SymBV sym w
-> IO (SymBV sym n)
bvNeg :: (1 <= w)
=> sym
-> SymBV sym w
-> IO (SymBV sym w)
bvAdd :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvSub :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvSub sym
sym SymBV sym w
x SymBV sym w
y = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymBV sym w
x forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvNeg sym
sym SymBV sym w
y
bvMul :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvUdiv :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvUrem :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvSdiv :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvSrem :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
testBitBV :: (1 <= w)
=> sym
-> Natural
-> SymBV sym w
-> IO (Pred sym)
bvIsNeg :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
x = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym w
x forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym (forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x) (forall (w :: Nat). NatRepr w -> BV w
BV.zero (forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x))
bvIte :: (1 <= w)
=> sym
-> Pred sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvEq :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym)
bvNe :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym)
bvNe sym
sym SymBV sym w
x SymBV sym w
y = forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
x SymBV sym w
y
bvUlt :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym)
bvUle :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym)
bvUle sym
sym SymBV sym w
x SymBV sym w
y = forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
y SymBV sym w
x
bvUge :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUge sym
sym SymBV sym w
x SymBV sym w
y = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymBV sym w
y SymBV sym w
x
bvUgt :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUgt sym
sym SymBV sym w
x SymBV sym w
y = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
y SymBV sym w
x
bvSlt :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt sym
sym SymBV sym w
x SymBV sym w
y = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym w
y SymBV sym w
x
bvSle :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSle sym
sym SymBV sym w
x SymBV sym w
y = forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym w
y SymBV sym w
x
bvSge :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSge sym
sym SymBV sym w
x SymBV sym w
y = forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym w
x SymBV sym w
y
bvIsNonzero :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)
bvShl :: (1 <= w) => sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvLshr :: (1 <= w) => sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvAshr :: (1 <= w) => sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvRol :: (1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvRor :: (1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvZext :: (1 <= u, u+1 <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext :: (1 <= u, u+1 <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvTrunc :: (1 <= r, r+1 <= w)
=> sym
-> NatRepr r
-> SymBV sym w
-> IO (SymBV sym r)
bvTrunc sym
sym NatRepr r
w SymBV sym w
x
| LeqProof r w
LeqProof <- forall (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans
(forall (f :: Nat -> Type) (n :: Nat) (g :: Nat -> Type) (m :: Nat).
f n -> g m -> LeqProof n (n + m)
addIsLeq NatRepr r
w (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1))
(forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (forall (n :: Nat). NatRepr n -> NatRepr (n + 1)
incNat NatRepr r
w) (forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x))
= forall sym (idx :: Nat) (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
bvSelect sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @0) NatRepr r
w SymBV sym w
x
bvAndBits :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvOrBits :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvXorBits :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvNotBits :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
bvSet :: forall w
. (1 <= w)
=> sym
-> SymBV sym w
-> Natural
-> Pred sym
-> IO (SymBV sym w)
bvSet sym
sym SymBV sym w
v Nat
i Pred sym
p = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Nat
i forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). NatRepr n -> Nat
natValue (forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
v)) forall a b. (a -> b) -> a -> b
$
do let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
v
let mask :: BV w
mask = forall (w :: Nat). NatRepr w -> Nat -> BV w
BV.bit' NatRepr w
w Nat
i
SymBV sym w
pbits <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> Pred sym -> IO (SymBV sym w)
bvFill sym
sym NatRepr w
w Pred sym
p
SymBV sym w
vbits <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAndBits sym
sym SymBV sym w
v forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Nat). NatRepr w -> BV w -> BV w
BV.complement NatRepr w
w BV w
mask)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvXorBits sym
sym SymBV sym w
vbits forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAndBits sym
sym SymBV sym w
pbits forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
mask
bvFill :: forall w. (1 <= w) =>
sym ->
NatRepr w ->
Pred sym ->
IO (SymBV sym w)
minUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
minUnsignedBV sym
sym NatRepr w
w = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w)
maxUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym
sym NatRepr w
w = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w)
maxSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr w
w = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr w
w)
minSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
minSignedBV sym
sym NatRepr w
w = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w)
bvPopcount :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
bvCountLeadingZeros :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
bvCountTrailingZeros :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
addUnsignedOF :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym, SymBV sym w)
addUnsignedOF sym
sym SymBV sym w
x SymBV sym w
y = do
SymBV sym w
r <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymBV sym w
x SymBV sym w
y
Pred sym
ovx <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
r SymBV sym w
x
Pred sym
ovy <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
r SymBV sym w
y
Pred sym
ov <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
ovx Pred sym
ovy
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
r)
addSignedOF :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym, SymBV sym w)
addSignedOF sym
sym SymBV sym w
x SymBV sym w
y = do
SymBV sym w
xy <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymBV sym w
x SymBV sym w
y
Pred sym
sx <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
x
Pred sym
sy <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
y
Pred sym
sxy <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
xy
Pred sym
not_sx <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
sx
Pred sym
not_sy <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
sy
Pred sym
not_sxy <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
sxy
Pred sym
ov1 <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
not_sxy forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
sx Pred sym
sy
Pred sym
ov2 <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
sxy forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
not_sx Pred sym
not_sy
Pred sym
ov <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
ov1 Pred sym
ov2
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
xy)
subUnsignedOF ::
(1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (Pred sym, SymBV sym w)
subUnsignedOF sym
sym SymBV sym w
x SymBV sym w
y = do
SymBV sym w
xy <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSub sym
sym SymBV sym w
x SymBV sym w
y
Pred sym
ov <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymBV sym w
x SymBV sym w
y
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
xy)
subSignedOF :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym, SymBV sym w)
subSignedOF sym
sym SymBV sym w
x SymBV sym w
y = do
SymBV sym w
xy <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSub sym
sym SymBV sym w
x SymBV sym w
y
Pred sym
sx <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
x
Pred sym
sy <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
y
Pred sym
sxy <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
xy
Pred sym
ov <- forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym) forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
xorPred sym
sym Pred sym
sx Pred sym
sxy forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
xorPred sym
sym Pred sym
sx Pred sym
sy)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
xy)
carrylessMultiply ::
(1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym (w+w))
carrylessMultiply sym
sym SymBV sym w
x0 SymBV sym w
y0
| Just Integer
_ <- forall (w :: Nat). BV w -> Integer
BV.asUnsigned forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
x0
, Maybe Integer
Nothing <- forall (w :: Nat). BV w -> Integer
BV.asUnsigned forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
y0
= forall (w :: Nat).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
go SymBV sym w
y0 SymBV sym w
x0
| Bool
otherwise
= forall (w :: Nat).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
go SymBV sym w
x0 SymBV sym w
y0
where
go :: (1 <= w) => SymBV sym w -> SymBV sym w -> IO (SymBV sym (w+w))
go :: forall (w :: Nat).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
go SymBV sym w
x SymBV sym w
y =
do let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
let w2 :: NatRepr (w + w)
w2 = forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
LeqProof 1 (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
LeqProof (w + 1) (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
SymBV sym (w + w)
z <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
w2 (forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr (w + w)
w2)
SymBV sym (w + w)
x' <- forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
w2 SymBV sym w
x
[SymBV sym (w + w)]
xs <- forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ do Pred sym
p <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Nat -> SymBV sym w -> IO (Pred sym)
testBitBV sym
sym (forall (w :: Nat). BV w -> Nat
BV.asNatural BV (w + w)
i) SymBV sym w
y
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym
Pred sym
p
(forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvShl sym
sym SymBV sym (w + w)
x' forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
w2 BV (w + w)
i)
(forall (m :: Type -> Type) a. Monad m => a -> m a
return SymBV sym (w + w)
z)
| BV (w + w)
i <- forall (w :: Nat). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned (forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr (w + w)
w2) (forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr (w + w)
w2 (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w forall a. Num a => a -> a -> a
- Integer
1))
]
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvXorBits sym
sym) SymBV sym (w + w)
z [SymBV sym (w + w)]
xs
unsignedWideMultiplyBV :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w, SymBV sym w)
unsignedWideMultiplyBV sym
sym SymBV sym w
x SymBV sym w
y = do
let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
let dbl_w :: NatRepr (w + w)
dbl_w = forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
LeqProof 1 (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
LeqProof (w + 1) (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
SymExpr sym (BaseBVType (w + w))
x' <- forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
x
SymExpr sym (BaseBVType (w + w))
y' <- forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
y
SymExpr sym (BaseBVType (w + w))
s <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType (w + w))
x' SymExpr sym (BaseBVType (w + w))
y'
SymBV sym w
lo <- forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + w))
s
SymExpr sym (BaseBVType (w + w))
n <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (forall (w :: Nat) (w' :: Nat).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext NatRepr (w + w)
dbl_w (forall (w :: Nat). NatRepr w -> BV w
BV.width NatRepr w
w))
SymBV sym w
hi <- forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvLshr sym
sym SymExpr sym (BaseBVType (w + w))
s SymExpr sym (BaseBVType (w + w))
n
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymBV sym w
hi, SymBV sym w
lo)
mulUnsignedOF ::
(1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (Pred sym, SymBV sym w)
mulUnsignedOF sym
sym SymBV sym w
x SymBV sym w
y =
do let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
let dbl_w :: NatRepr (w + w)
dbl_w = forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
LeqProof 1 (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
LeqProof (w + 1) (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
SymExpr sym (BaseBVType (w + w))
x' <- forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
x
SymExpr sym (BaseBVType (w + w))
y' <- forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
y
SymExpr sym (BaseBVType (w + w))
s <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType (w + w))
x' SymExpr sym (BaseBVType (w + w))
y'
SymBV sym w
lo <- forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + w))
s
Pred sym
ov <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUgt sym
sym SymExpr sym (BaseBVType (w + w))
s forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (forall (w :: Nat) (w' :: Nat).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext NatRepr (w + w)
dbl_w (forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
lo)
signedWideMultiplyBV :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w, SymBV sym w)
signedWideMultiplyBV sym
sym SymBV sym w
x SymBV sym w
y = do
let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
let dbl_w :: NatRepr (w + w)
dbl_w = forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
LeqProof 1 (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
LeqProof (w + 1) (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
SymExpr sym (BaseBVType (w + w))
x' <- forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
x
SymExpr sym (BaseBVType (w + w))
y' <- forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
y
SymExpr sym (BaseBVType (w + w))
s <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType (w + w))
x' SymExpr sym (BaseBVType (w + w))
y'
SymBV sym w
lo <- forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + w))
s
SymExpr sym (BaseBVType (w + w))
n <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (forall (w :: Nat) (w' :: Nat).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext NatRepr (w + w)
dbl_w (forall (w :: Nat). NatRepr w -> BV w
BV.width NatRepr w
w))
SymBV sym w
hi <- forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvLshr sym
sym SymExpr sym (BaseBVType (w + w))
s SymExpr sym (BaseBVType (w + w))
n
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymBV sym w
hi, SymBV sym w
lo)
mulSignedOF ::
(1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (Pred sym, SymBV sym w)
mulSignedOF sym
sym SymBV sym w
x SymBV sym w
y =
do let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
let dbl_w :: NatRepr (w + w)
dbl_w = forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w
w
one_leq_w :: LeqProof 1 w
one_leq_w@LeqProof 1 w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr w
w)
LeqProof 1 (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
one_leq_w NatRepr w
w)
w_leq_w :: LeqProof w w
w_leq_w@LeqProof w w
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr w
w NatRepr w
w)
LeqProof (w + 1) (w + w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 LeqProof w w
w_leq_w LeqProof 1 w
one_leq_w)
SymExpr sym (BaseBVType (w + w))
x' <- forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
x
SymExpr sym (BaseBVType (w + w))
y' <- forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + w)
dbl_w SymBV sym w
y
SymExpr sym (BaseBVType (w + w))
s <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType (w + w))
x' SymExpr sym (BaseBVType (w + w))
y'
SymBV sym w
lo <- forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + w))
s
Pred sym
ov1 <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymExpr sym (BaseBVType (w + w))
s forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext NatRepr w
w NatRepr (w + w)
dbl_w (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w))
Pred sym
ov2 <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt sym
sym SymExpr sym (BaseBVType (w + w))
s forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + w)
dbl_w (forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext NatRepr w
w NatRepr (w + w)
dbl_w (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr w
w))
Pred sym
ov <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
ov1 Pred sym
ov2
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
ov, SymBV sym w
lo)
mkStruct :: sym
-> Ctx.Assignment (SymExpr sym) flds
-> IO (SymStruct sym flds)
structField :: sym
-> SymStruct sym flds
-> Ctx.Index flds tp
-> IO (SymExpr sym tp)
structEq :: forall flds
. sym
-> SymStruct sym flds
-> SymStruct sym flds
-> IO (Pred sym)
structEq sym
sym SymStruct sym flds
x SymStruct sym flds
y = do
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymStruct sym flds
x of
BaseStructRepr Assignment BaseTypeRepr ctx
fld_types -> do
let sz :: Size ctx
sz = forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment BaseTypeRepr ctx
fld_types
let f :: IO (Pred sym) -> Ctx.Index flds tp -> IO (Pred sym)
f :: forall (tp :: BaseType).
IO (Pred sym) -> Index flds tp -> IO (Pred sym)
f IO (Pred sym)
mp Index flds tp
i = do
SymExpr sym tp
xi <- forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
structField sym
sym SymStruct sym flds
x Index flds tp
i
SymExpr sym tp
yi <- forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
structField sym
sym SymStruct sym flds
y Index flds tp
i
Pred sym
i_eq <- forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
isEq sym
sym SymExpr sym tp
xi SymExpr sym tp
yi
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
i_eq of
Just Bool
True -> IO (Pred sym)
mp
Just Bool
False -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
Maybe Bool
_ -> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
i_eq forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (Pred sym)
mp
forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex Size ctx
sz forall (tp :: BaseType).
IO (Pred sym) -> Index flds tp -> IO (Pred sym)
f (forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym))
structIte :: sym
-> Pred sym
-> SymStruct sym flds
-> SymStruct sym flds
-> IO (SymStruct sym flds)
constantArray :: sym
-> Ctx.Assignment BaseTypeRepr (idx::>tp)
-> SymExpr sym b
-> IO (SymArray sym (idx::>tp) b)
arrayFromFn :: sym
-> SymFn sym (idx ::> itp) ret
-> IO (SymArray sym (idx ::> itp) ret)
arrayMap :: sym
-> SymFn sym (ctx::>d) r
-> Ctx.Assignment (ArrayResultWrapper (SymExpr sym) (idx ::> itp)) (ctx::>d)
-> IO (SymArray sym (idx ::> itp) r)
arrayUpdate :: sym
-> SymArray sym (idx::>tp) b
-> Ctx.Assignment (SymExpr sym) (idx::>tp)
-> SymExpr sym b
-> IO (SymArray sym (idx::>tp) b)
arrayLookup :: sym
-> SymArray sym (idx::>tp) b
-> Ctx.Assignment (SymExpr sym) (idx::>tp)
-> IO (SymExpr sym b)
arrayCopy ::
(1 <= w) =>
sym ->
SymArray sym (SingleCtx (BaseBVType w)) a ->
SymBV sym w ->
SymArray sym (SingleCtx (BaseBVType w)) a ->
SymBV sym w ->
SymBV sym w ->
IO (SymArray sym (SingleCtx (BaseBVType w)) a)
arraySet ::
(1 <= w) =>
sym ->
SymArray sym (SingleCtx (BaseBVType w)) a ->
SymBV sym w ->
SymExpr sym a ->
SymBV sym w ->
IO (SymArray sym (SingleCtx (BaseBVType w)) a)
arrayRangeEq ::
(1 <= w) =>
sym ->
SymArray sym (SingleCtx (BaseBVType w)) a ->
SymBV sym w ->
SymArray sym (SingleCtx (BaseBVType w)) a ->
SymBV sym w ->
SymBV sym w ->
IO (Pred sym)
arrayFromMap :: sym
-> Ctx.Assignment BaseTypeRepr (idx ::> itp)
-> AUM.ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
-> SymExpr sym tp
-> IO (SymArray sym (idx ::> itp) tp)
arrayFromMap sym
sym Assignment BaseTypeRepr (idx ::> itp)
idx_tps ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
m SymExpr sym tp
default_value = do
SymArray sym (idx ::> itp) tp
a0 <- forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
constantArray sym
sym Assignment BaseTypeRepr (idx ::> itp)
idx_tps SymExpr sym tp
default_value
forall sym (idx :: Ctx BaseType) (itp :: BaseType)
(tp :: BaseType).
IsExprBuilder sym =>
sym
-> ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
-> SymArray sym (idx ::> itp) tp
-> IO (SymArray sym (idx ::> itp) tp)
arrayUpdateAtIdxLits sym
sym ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
m SymArray sym (idx ::> itp) tp
a0
arrayUpdateAtIdxLits :: sym
-> AUM.ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
-> SymArray sym (idx ::> itp) tp
-> IO (SymArray sym (idx ::> itp) tp)
arrayUpdateAtIdxLits sym
sym ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
m SymArray sym (idx ::> itp) tp
a0 = do
let updateAt :: SymArray sym (idx ::> itp) tp
-> (Assignment IndexLit (idx ::> itp), SymExpr sym tp)
-> IO (SymArray sym (idx ::> itp) tp)
updateAt SymArray sym (idx ::> itp) tp
a (Assignment IndexLit (idx ::> itp)
i,SymExpr sym tp
v) = do
Assignment (SymExpr sym) (idx ::> itp)
idx <- forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC (forall sym (idx :: BaseType).
IsExprBuilder sym =>
sym -> IndexLit idx -> IO (SymExpr sym idx)
indexLit sym
sym) Assignment IndexLit (idx ::> itp)
i
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
arrayUpdate sym
sym SymArray sym (idx ::> itp) tp
a Assignment (SymExpr sym) (idx ::> itp)
idx SymExpr sym tp
v
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM SymArray sym (idx ::> itp) tp
-> (Assignment IndexLit (idx ::> itp), SymExpr sym tp)
-> IO (SymArray sym (idx ::> itp) tp)
updateAt SymArray sym (idx ::> itp) tp
a0 (forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
(tp :: BaseType).
ArrayUpdateMap e ctx tp -> [(Assignment IndexLit ctx, e tp)]
AUM.toList ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
m)
arrayIte :: sym
-> Pred sym
-> SymArray sym idx b
-> SymArray sym idx b
-> IO (SymArray sym idx b)
arrayEq :: sym
-> SymArray sym idx b
-> SymArray sym idx b
-> IO (Pred sym)
allTrueEntries :: sym -> SymArray sym idx BaseBoolType -> IO (Pred sym)
allTrueEntries sym
sym SymArray sym idx BaseBoolType
a = do
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType SymArray sym idx BaseBoolType
a of
BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx_tps BaseTypeRepr xs
_ ->
forall sym (idx :: Ctx BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym -> SymArray sym idx b -> SymArray sym idx b -> IO (Pred sym)
arrayEq sym
sym SymArray sym idx BaseBoolType
a forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
constantArray sym
sym Assignment BaseTypeRepr (idx ::> tp)
idx_tps (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym)
arrayTrueOnEntries
:: sym
-> SymFn sym (idx::>itp) BaseBoolType
-> SymArray sym (idx ::> itp) BaseBoolType
-> IO (Pred sym)
integerToReal :: sym -> SymInteger sym -> IO (SymReal sym)
bvToInteger :: (1 <= w) => sym -> SymBV sym w -> IO (SymInteger sym)
sbvToInteger :: (1 <= w) => sym -> SymBV sym w -> IO (SymInteger sym)
predToBV :: (1 <= w) => sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
uintToReal :: (1 <= w) => sym -> SymBV sym w -> IO (SymReal sym)
uintToReal sym
sym = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
bvToInteger sym
sym forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym
sbvToReal :: (1 <= w) => sym -> SymBV sym w -> IO (SymReal sym)
sbvToReal sym
sym = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
sbvToInteger sym
sym forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym
realRound :: sym -> SymReal sym -> IO (SymInteger sym)
realRoundEven :: sym -> SymReal sym -> IO (SymInteger sym)
realFloor :: sym -> SymReal sym -> IO (SymInteger sym)
realCeil :: sym -> SymReal sym -> IO (SymInteger sym)
realTrunc :: sym -> SymReal sym -> IO (SymInteger sym)
realTrunc sym
sym SymReal sym
x =
do Pred sym
pneg <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLt sym
sym SymReal sym
x forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
0
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym Pred sym
pneg (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realCeil sym
sym SymReal sym
x) (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realFloor sym
sym SymReal sym
x)
integerToBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
realToInteger :: sym -> SymReal sym -> IO (SymInteger sym)
realToBV :: (1 <= w) => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
realToBV sym
sym SymReal sym
r NatRepr w
w = do
SymInteger sym
i <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realRound sym
sym SymReal sym
r
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToBV sym
sym SymInteger sym
i NatRepr w
w
realToSBV :: (1 <= w) => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
realToSBV sym
sym SymReal sym
r NatRepr w
w = do
SymInteger sym
i <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realRound sym
sym SymReal sym
r
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToSBV sym
sym SymInteger sym
i NatRepr w
w
clampedIntToSBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToSBV sym
sym SymInteger sym
i NatRepr w
w
| Just Integer
v <- forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
asInteger SymInteger sym
i = do
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> BV w
BV.signedClamp NatRepr w
w Integer
v
| Bool
otherwise = do
let min_val :: Integer
min_val = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr w
w
min_val_bv :: BV w
min_val_bv = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w
SymInteger sym
min_sym <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
min_val
Pred sym
is_lt <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
i SymInteger sym
min_sym
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
is_lt (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
min_val_bv) forall a b. (a -> b) -> a -> b
$ do
let max_val :: Integer
max_val = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w
max_val_bv :: BV w
max_val_bv = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr w
w
SymInteger sym
max_sym <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
max_val
Pred sym
is_gt <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
max_sym SymInteger sym
i
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
is_gt (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
max_val_bv) forall a b. (a -> b) -> a -> b
$ do
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
integerToBV sym
sym SymInteger sym
i NatRepr w
w
clampedIntToBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToBV sym
sym SymInteger sym
i NatRepr w
w
| Just Integer
v <- forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
asInteger SymInteger sym
i = do
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.unsignedClamp NatRepr w
w Integer
v
| Bool
otherwise = do
SymInteger sym
min_sym <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
0
Pred sym
is_lt <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
i SymInteger sym
min_sym
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
is_lt (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w)) forall a b. (a -> b) -> a -> b
$ do
let max_val :: Integer
max_val = forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr w
w
max_val_bv :: BV w
max_val_bv = forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w
SymInteger sym
max_sym <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
max_val
Pred sym
is_gt <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
max_sym SymInteger sym
i
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
is_gt (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
max_val_bv) forall a b. (a -> b) -> a -> b
$
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
integerToBV sym
sym SymInteger sym
i NatRepr w
w
intSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
intSetWidth sym
sym SymBV sym m
e NatRepr n
n = do
let m :: NatRepr m
m = forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym m
e
case NatRepr n
n forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
`testNatCases` NatRepr m
m of
NatCaseLT LeqProof (n + 1) m
LeqProof -> do
Pred sym
does_underflow <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymBV sym m
e forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr m
m (forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext NatRepr n
n NatRepr m
m (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr n
n))
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
does_underflow (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr n
n (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr n
n)) forall a b. (a -> b) -> a -> b
$ do
Pred sym
does_overflow <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt sym
sym SymBV sym m
e forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr m
m (forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr m
m (forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr n
n))
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
does_overflow (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr n
n (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr n
n)) forall a b. (a -> b) -> a -> b
$ do
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr n
n SymBV sym m
e
NatCases n m
NatCaseEQ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymBV sym m
e
NatCaseGT LeqProof (m + 1) n
LeqProof -> forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr n
n SymBV sym m
e
uintSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintSetWidth sym
sym SymBV sym m
e NatRepr n
n = do
let m :: NatRepr m
m = forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym m
e
case NatRepr n
n forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
`testNatCases` NatRepr m
m of
NatCaseLT LeqProof (n + 1) m
LeqProof -> do
Pred sym
does_overflow <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUgt sym
sym SymBV sym m
e forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr m
m (forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr m
m (forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n))
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
does_overflow (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr n
n (forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr n
n)) forall a b. (a -> b) -> a -> b
$ forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr n
n SymBV sym m
e
NatCases n m
NatCaseEQ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymBV sym m
e
NatCaseGT LeqProof (m + 1) n
LeqProof -> forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr n
n SymBV sym m
e
intToUInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
intToUInt sym
sym SymBV sym m
e NatRepr n
w = do
Pred sym
p <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym m
e
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
p (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr n
w (forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr n
w)) (forall sym (m :: Nat) (n :: Nat).
(IsExprBuilder sym, 1 <= m, 1 <= n) =>
sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintSetWidth sym
sym SymBV sym m
e NatRepr n
w)
uintToInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintToInt sym
sym SymBV sym m
e NatRepr n
n = do
let m :: NatRepr m
m = forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym m
e
case NatRepr n
n forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
`testNatCases` NatRepr m
m of
NatCaseLT LeqProof (n + 1) m
LeqProof -> do
SymBV sym m
max_val <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr m
m (forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext NatRepr n
n NatRepr m
m (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr n
n))
Pred sym
p <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymBV sym m
e SymBV sym m
max_val
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr n
n forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
p SymBV sym m
e SymBV sym m
max_val
NatCases n m
NatCaseEQ -> do
SymBV sym n
max_val <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr n
n
Pred sym
p <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymBV sym m
e SymBV sym n
max_val
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
p SymBV sym m
e SymBV sym n
max_val
NatCaseGT LeqProof (m + 1) n
LeqProof -> do
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr n
n SymBV sym m
e
stringEmpty :: sym -> StringInfoRepr si -> IO (SymString sym si)
stringLit :: sym -> StringLiteral si -> IO (SymString sym si)
stringEq :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
stringIte :: sym -> Pred sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)
stringConcat :: sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)
stringContains ::
sym ->
SymString sym si ->
SymString sym si ->
IO (Pred sym)
stringIsPrefixOf ::
sym ->
SymString sym si ->
SymString sym si ->
IO (Pred sym)
stringIsSuffixOf ::
sym ->
SymString sym si ->
SymString sym si ->
IO (Pred sym)
stringIndexOf ::
sym ->
SymString sym si ->
SymString sym si ->
SymInteger sym ->
IO (SymInteger sym)
stringLength :: sym -> SymString sym si -> IO (SymInteger sym)
stringSubstring ::
sym ->
SymString sym si ->
SymInteger sym ->
SymInteger sym ->
IO (SymString sym si)
realZero :: sym -> SymReal sym
realLit :: sym -> Rational -> IO (SymReal sym)
sciLit :: sym -> Scientific -> IO (SymReal sym)
sciLit sym
sym Scientific
s = forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym (forall a. Real a => a -> Rational
toRational Scientific
s)
realEq :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realNe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realNe sym
sym SymReal sym
x SymReal sym
y = forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymReal sym
x SymReal sym
y
realLe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLt sym
sym SymReal sym
x SymReal sym
y = forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym SymReal sym
y SymReal sym
x
realGe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realGe sym
sym SymReal sym
x SymReal sym
y = forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym SymReal sym
y SymReal sym
x
realGt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realGt sym
sym SymReal sym
x SymReal sym
y = forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLt sym
sym SymReal sym
y SymReal sym
x
realIte :: sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMin :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMin sym
sym SymReal sym
x SymReal sym
y =
do Pred sym
p <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym SymReal sym
x SymReal sym
y
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
p SymReal sym
x SymReal sym
y
realMax :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMax sym
sym SymReal sym
x SymReal sym
y =
do Pred sym
p <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym SymReal sym
x SymReal sym
y
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
p SymReal sym
y SymReal sym
x
realNeg :: sym -> SymReal sym -> IO (SymReal sym)
realAdd :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym
sym SymReal sym
x SymReal sym
y = forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
x forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym SymReal sym
y
realSq :: sym -> SymReal sym -> IO (SymReal sym)
realSq sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
x SymReal sym
x
realDiv :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMod :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMod sym
sym SymReal sym
x SymReal sym
y = do
Pred sym
isZero <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymReal sym
y (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
isZero (forall (m :: Type -> Type) a. Monad m => a -> m a
return SymReal sym
x) forall a b. (a -> b) -> a -> b
$ do
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym
sym SymReal sym
x forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
y
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realFloor sym
sym
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymReal sym
x SymReal sym
y
isInteger :: sym -> SymReal sym -> IO (Pred sym)
realIsNonNeg :: sym -> SymReal sym -> IO (Pred sym)
realIsNonNeg sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym) SymReal sym
x
realSqrt :: sym -> SymReal sym -> IO (SymReal sym)
realPi :: sym -> IO (SymReal sym)
realPi sym
sym = forall sym.
IsExprBuilder sym =>
sym -> SpecialFunction EmptyCtx -> IO (SymReal sym)
realSpecialFunction0 sym
sym SpecialFunction EmptyCtx
Pi
realLog :: sym -> SymReal sym -> IO (SymReal sym)
realLog sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym
-> SpecialFunction (EmptyCtx ::> R)
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction1 sym
sym SpecialFunction (EmptyCtx ::> R)
Log SymReal sym
x
realExp :: sym -> SymReal sym -> IO (SymReal sym)
realExp sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym
-> SpecialFunction (EmptyCtx ::> R)
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction1 sym
sym SpecialFunction (EmptyCtx ::> R)
Exp SymReal sym
x
realSin :: sym -> SymReal sym -> IO (SymReal sym)
realSin sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym
-> SpecialFunction (EmptyCtx ::> R)
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction1 sym
sym SpecialFunction (EmptyCtx ::> R)
Sin SymReal sym
x
realCos :: sym -> SymReal sym -> IO (SymReal sym)
realCos sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym
-> SpecialFunction (EmptyCtx ::> R)
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction1 sym
sym SpecialFunction (EmptyCtx ::> R)
Cos SymReal sym
x
realTan :: sym -> SymReal sym -> IO (SymReal sym)
realTan sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym
-> SpecialFunction (EmptyCtx ::> R)
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction1 sym
sym SpecialFunction (EmptyCtx ::> R)
Tan SymReal sym
x
realSinh :: sym -> SymReal sym -> IO (SymReal sym)
realSinh sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym
-> SpecialFunction (EmptyCtx ::> R)
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction1 sym
sym SpecialFunction (EmptyCtx ::> R)
Sinh SymReal sym
x
realCosh :: sym -> SymReal sym -> IO (SymReal sym)
realCosh sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym
-> SpecialFunction (EmptyCtx ::> R)
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction1 sym
sym SpecialFunction (EmptyCtx ::> R)
Cosh SymReal sym
x
realTanh :: sym -> SymReal sym -> IO (SymReal sym)
realTanh sym
sym SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym
-> SpecialFunction (EmptyCtx ::> R)
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction1 sym
sym SpecialFunction (EmptyCtx ::> R)
Tanh SymReal sym
x
realAbs :: sym -> SymReal sym -> IO (SymReal sym)
realAbs sym
sym SymReal sym
x = do
Pred sym
c <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realGe sym
sym SymReal sym
x (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
c SymReal sym
x forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym SymReal sym
x
realHypot :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realHypot sym
sym SymReal sym
x SymReal sym
y = do
case (forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational SymReal sym
x, forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational SymReal sym
y) of
(Just Rational
0, Maybe Rational
_) -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realAbs sym
sym SymReal sym
y
(Maybe Rational
_, Just Rational
0) -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realAbs sym
sym SymReal sym
x
(Maybe Rational, Maybe Rational)
_ -> do
SymReal sym
x2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSq sym
sym SymReal sym
x
SymReal sym
y2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSq sym
sym SymReal sym
y
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSqrt sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
x2 SymReal sym
y2
realAtan2 :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAtan2 sym
sym SymReal sym
y SymReal sym
x = forall sym.
IsExprBuilder sym =>
sym
-> SpecialFunction ((EmptyCtx ::> R) ::> R)
-> SymReal sym
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction2 sym
sym SpecialFunction ((EmptyCtx ::> R) ::> R)
Arctan2 SymReal sym
y SymReal sym
x
realSpecialFunction
:: sym
-> SpecialFunction args
-> Ctx.Assignment (SpecialFnArg (SymExpr sym) BaseRealType) args
-> IO (SymReal sym)
realSpecialFunction0
:: sym
-> SpecialFunction EmptyCtx
-> IO (SymReal sym)
realSpecialFunction0 sym
sym SpecialFunction EmptyCtx
fn =
forall sym (args :: Ctx Type).
IsExprBuilder sym =>
sym
-> SpecialFunction args
-> Assignment (SpecialFnArg (SymExpr sym) BaseRealType) args
-> IO (SymReal sym)
realSpecialFunction sym
sym SpecialFunction EmptyCtx
fn forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
realSpecialFunction1
:: sym
-> SpecialFunction (EmptyCtx ::> R)
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction1 sym
sym SpecialFunction (EmptyCtx ::> R)
fn SymReal sym
x =
forall sym (args :: Ctx Type).
IsExprBuilder sym =>
sym
-> SpecialFunction args
-> Assignment (SpecialFnArg (SymExpr sym) BaseRealType) args
-> IO (SymReal sym)
realSpecialFunction sym
sym SpecialFunction (EmptyCtx ::> R)
fn (forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
SpecialFnArg SymReal sym
x)
realSpecialFunction2
:: sym
-> SpecialFunction (EmptyCtx ::> R ::> R)
-> SymReal sym
-> SymReal sym
-> IO (SymReal sym)
realSpecialFunction2 sym
sym SpecialFunction ((EmptyCtx ::> R) ::> R)
fn SymReal sym
x SymReal sym
y =
forall sym (args :: Ctx Type).
IsExprBuilder sym =>
sym
-> SpecialFunction args
-> Assignment (SpecialFnArg (SymExpr sym) BaseRealType) args
-> IO (SymReal sym)
realSpecialFunction sym
sym SpecialFunction ((EmptyCtx ::> R) ::> R)
fn (forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
SpecialFnArg SymReal sym
x forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
SpecialFnArg SymReal sym
y)
floatPZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatNZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatNaN :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatPInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatNInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatLitRational
:: sym -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat sym fpp)
floatLitRational sym
sym FloatPrecisionRepr fpp
fpp Rational
x = forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
realToFloat sym
sym FloatPrecisionRepr fpp
fpp RoundingMode
RNE forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
x
floatLit :: sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
floatNeg
:: sym
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatAbs
:: sym
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatSqrt
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatAdd
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatSub
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatMul
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatDiv
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatRem
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatMin
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatMax
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatFMA
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatEq
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatNe
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatFpEq
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatFpApart
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatFpApart sym
sym SymFloat sym fpp
x SymFloat sym fpp
y =
do Pred sym
l <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
floatLt sym
sym SymFloat sym fpp
x SymFloat sym fpp
y
Pred sym
g <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
floatGt sym
sym SymFloat sym fpp
x SymFloat sym fpp
y
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
l Pred sym
g
floatFpUnordered
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatFpUnordered sym
sym SymFloat sym fpp
x SymFloat sym fpp
y =
do Pred sym
xnan <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNaN sym
sym SymFloat sym fpp
x
Pred sym
ynan <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNaN sym
sym SymFloat sym fpp
y
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
xnan Pred sym
ynan
floatLe
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatLt
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatGe
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatGt
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatIsNaN :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsInf :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsZero :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsPos :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNeg :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsSubnorm :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNorm :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIte
:: sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatCast
:: sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymFloat sym fpp'
-> IO (SymFloat sym fpp)
floatRound
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatFromBinary
:: (2 <= eb, 2 <= sb)
=> sym
-> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> SymBV sym (eb + sb)
-> IO (SymFloat sym (FloatingPointPrecision eb sb))
floatToBinary
:: (2 <= eb, 2 <= sb)
=> sym
-> SymFloat sym (FloatingPointPrecision eb sb)
-> IO (SymBV sym (eb + sb))
bvToFloat
:: (1 <= w)
=> sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
sbvToFloat
:: (1 <= w)
=> sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
realToFloat
:: sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
floatToBV
:: (1 <= w)
=> sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
floatToSBV
:: (1 <= w)
=> sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
floatToReal :: sym -> SymFloat sym fpp -> IO (SymReal sym)
floatSpecialFunction
:: sym
-> FloatPrecisionRepr fpp
-> SpecialFunction args
-> Ctx.Assignment (SpecialFnArg (SymExpr sym) (BaseFloatType fpp)) args
-> IO (SymFloat sym fpp)
mkComplex :: sym -> Complex (SymReal sym) -> IO (SymCplx sym)
getRealPart :: sym -> SymCplx sym -> IO (SymReal sym)
getImagPart :: sym -> SymCplx sym -> IO (SymReal sym)
cplxGetParts :: sym -> SymCplx sym -> IO (Complex (SymReal sym))
mkComplexLit :: sym -> Complex Rational -> IO (SymCplx sym)
mkComplexLit sym
sym Complex Rational
d = forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym) Complex Rational
d
cplxFromReal :: sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym SymReal sym
r = forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
r forall a. a -> a -> Complex a
:+ forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
cplxIte :: sym -> Pred sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxIte sym
sym Pred sym
c SymCplx sym
x SymCplx sym
y = do
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
c of
Just Bool
True -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymCplx sym
x
Just Bool
False -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SymCplx sym
y
Maybe Bool
_ -> do
SymReal sym
xr :+ SymReal sym
xi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
SymReal sym
yr :+ SymReal sym
yi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
y
SymReal sym
zr <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
c SymReal sym
xr SymReal sym
yr
SymReal sym
zi <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
c SymReal sym
xi SymReal sym
yi
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
zr forall a. a -> a -> Complex a
:+ SymReal sym
zi)
cplxNeg :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxNeg sym
sym SymCplx sym
x = forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym) forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
cplxAdd :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxAdd sym
sym SymCplx sym
x SymCplx sym
y = do
SymReal sym
xr :+ SymReal sym
xi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
SymReal sym
yr :+ SymReal sym
yi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
y
SymReal sym
zr <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
xr SymReal sym
yr
SymReal sym
zi <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
xi SymReal sym
yi
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
zr forall a. a -> a -> Complex a
:+ SymReal sym
zi)
cplxSub :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxSub sym
sym SymCplx sym
x SymCplx sym
y = do
SymReal sym
xr :+ SymReal sym
xi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
SymReal sym
yr :+ SymReal sym
yi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
y
SymReal sym
zr <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym
sym SymReal sym
xr SymReal sym
yr
SymReal sym
zi <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym
sym SymReal sym
xi SymReal sym
yi
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
zr forall a. a -> a -> Complex a
:+ SymReal sym
zi)
cplxMul :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxMul sym
sym SymCplx sym
x SymCplx sym
y = do
SymReal sym
xr :+ SymReal sym
xi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
SymReal sym
yr :+ SymReal sym
yi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
y
SymReal sym
rz0 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
xr SymReal sym
yr
SymReal sym
rz <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym
sym SymReal sym
rz0 forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
xi SymReal sym
yi
SymReal sym
iz0 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
xi SymReal sym
yr
SymReal sym
iz <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
iz0 forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
xr SymReal sym
yi
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
rz forall a. a -> a -> Complex a
:+ SymReal sym
iz)
cplxMag :: sym -> SymCplx sym -> IO (SymReal sym)
cplxMag sym
sym SymCplx sym
x = do
(SymReal sym
xr :+ SymReal sym
xi) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realHypot sym
sym SymReal sym
xr SymReal sym
xi
cplxSqrt :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxSqrt sym
sym SymCplx sym
x = do
(SymReal sym
r_part :+ SymReal sym
i_part) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
case (forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational SymReal sym
r_part forall a. a -> a -> Complex a
:+ forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational SymReal sym
i_part)of
(Just Rational
r :+ Just Rational
i) | Just Complex Rational
z <- forall a (m :: Type -> Type).
(Ord a, Fractional a, Monad m) =>
(a -> m a) -> Complex a -> m (Complex a)
tryComplexSqrt Rational -> Maybe Rational
tryRationalSqrt (Rational
r forall a. a -> a -> Complex a
:+ Rational
i) ->
forall sym.
IsExprBuilder sym =>
sym -> Complex Rational -> IO (SymCplx sym)
mkComplexLit sym
sym Complex Rational
z
(Maybe Rational
_ :+ Just Rational
0) -> do
Pred sym
c <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realGe sym
sym SymReal sym
r_part (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
SymReal sym
u <- forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
c
(forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSqrt sym
sym SymReal sym
r_part)
(forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
0)
SymReal sym
v <- forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
c
(forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
0)
(forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSqrt sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym SymReal sym
r_part)
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
u forall a. a -> a -> Complex a
:+ SymReal sym
v)
Complex (Maybe Rational)
_ -> do
SymReal sym
m <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realHypot sym
sym SymReal sym
r_part SymReal sym
i_part
SymReal sym
m_plus_r <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
m SymReal sym
r_part
SymReal sym
m_sub_r <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym
sym SymReal sym
m SymReal sym
r_part
SymReal sym
two <- forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
2
SymReal sym
u <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSqrt sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymReal sym
m_plus_r SymReal sym
two
SymReal sym
v <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSqrt sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymReal sym
m_sub_r SymReal sym
two
SymReal sym
neg_v <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym SymReal sym
v
Pred sym
i_part_nonneg <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
realIsNonNeg sym
sym SymReal sym
i_part
SymReal sym
v' <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
i_part_nonneg SymReal sym
v SymReal sym
neg_v
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
u forall a. a -> a -> Complex a
:+ SymReal sym
v')
cplxSin :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxSin sym
sym SymCplx sym
arg = do
c :: Complex (SymReal sym)
c@(SymReal sym
x :+ SymReal sym
y) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
arg
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Complex (SymReal sym)
c of
(Just Rational
0 :+ Just Rational
0) -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
(Maybe Rational
_ :+ Just Rational
0) -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSin sym
sym SymReal sym
x
(Just Rational
0 :+ Maybe Rational
_) -> do
SymReal sym
sinh_y <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSinh sym
sym SymReal sym
y
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym forall a. a -> a -> Complex a
:+ SymReal sym
sinh_y)
Complex (Maybe Rational)
_ -> do
SymReal sym
sin_x <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSin sym
sym SymReal sym
x
SymReal sym
cos_x <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCos sym
sym SymReal sym
x
SymReal sym
sinh_y <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSinh sym
sym SymReal sym
y
SymReal sym
cosh_y <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCosh sym
sym SymReal sym
y
SymReal sym
r_part <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
sin_x SymReal sym
cosh_y
SymReal sym
i_part <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
cos_x SymReal sym
sinh_y
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
r_part forall a. a -> a -> Complex a
:+ SymReal sym
i_part)
cplxCos :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxCos sym
sym SymCplx sym
arg = do
c :: Complex (SymReal sym)
c@(SymReal sym
x :+ SymReal sym
y) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
arg
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Complex (SymReal sym)
c of
(Just Rational
0 :+ Just Rational
0) -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
1
(Maybe Rational
_ :+ Just Rational
0) -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCos sym
sym SymReal sym
x
(Just Rational
0 :+ Maybe Rational
_) -> do
SymReal sym
cosh_y <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCosh sym
sym SymReal sym
y
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym SymReal sym
cosh_y
Complex (Maybe Rational)
_ -> do
SymReal sym
neg_sin_x <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSin sym
sym SymReal sym
x
SymReal sym
cos_x <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCos sym
sym SymReal sym
x
SymReal sym
sinh_y <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSinh sym
sym SymReal sym
y
SymReal sym
cosh_y <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCosh sym
sym SymReal sym
y
SymReal sym
r_part <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
cos_x SymReal sym
cosh_y
SymReal sym
i_part <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
neg_sin_x SymReal sym
sinh_y
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
r_part forall a. a -> a -> Complex a
:+ SymReal sym
i_part)
cplxTan :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxTan sym
sym SymCplx sym
arg = do
c :: Complex (SymReal sym)
c@(SymReal sym
x :+ SymReal sym
y) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
arg
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Complex (SymReal sym)
c of
(Just Rational
0 :+ Just Rational
0) -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
(Maybe Rational
_ :+ Just Rational
0) -> do
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realTan sym
sym SymReal sym
x
(Just Rational
0 :+ Maybe Rational
_) -> do
SymReal sym
i_part <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realTanh sym
sym SymReal sym
y
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym forall a. a -> a -> Complex a
:+ SymReal sym
i_part)
Complex (Maybe Rational)
_ -> do
SymReal sym
sin_x <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSin sym
sym SymReal sym
x
SymReal sym
cos_x <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCos sym
sym SymReal sym
x
SymReal sym
sinh_y <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSinh sym
sym SymReal sym
y
SymReal sym
cosh_y <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCosh sym
sym SymReal sym
y
SymReal sym
u <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
cos_x SymReal sym
cosh_y
SymReal sym
v <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
sin_x SymReal sym
sinh_y
SymReal sym
u2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
u SymReal sym
u
SymReal sym
v2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
v SymReal sym
v
SymReal sym
m <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
u2 SymReal sym
v2
SymReal sym
sin_x_cos_x <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
sin_x SymReal sym
cos_x
SymReal sym
sinh_y_cosh_y <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
sinh_y SymReal sym
cosh_y
SymReal sym
r_part <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymReal sym
sin_x_cos_x SymReal sym
m
SymReal sym
i_part <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymReal sym
sinh_y_cosh_y SymReal sym
m
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
r_part forall a. a -> a -> Complex a
:+ SymReal sym
i_part)
cplxHypot :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxHypot sym
sym SymCplx sym
x SymCplx sym
y = do
(SymReal sym
xr :+ SymReal sym
xi) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
(SymReal sym
yr :+ SymReal sym
yi) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
y
SymReal sym
xr2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSq sym
sym SymReal sym
xr
SymReal sym
xi2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSq sym
sym SymReal sym
xi
SymReal sym
yr2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSq sym
sym SymReal sym
yr
SymReal sym
yi2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSq sym
sym SymReal sym
yi
SymReal sym
r2 <- forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym) SymReal sym
xr2 [SymReal sym
xi2, SymReal sym
yr2, SymReal sym
yi2]
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSqrt sym
sym SymReal sym
r2
cplxRound :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxRound sym
sym SymCplx sym
x = do
Complex (SymReal sym)
c <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym forall (m :: Type -> Type) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realRound sym
sym) Complex (SymReal sym)
c
cplxFloor :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxFloor sym
sym SymCplx sym
x =
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym forall (m :: Type -> Type) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realFloor sym
sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
cplxCeil :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxCeil sym
sym SymCplx sym
x =
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym forall (m :: Type -> Type) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realCeil sym
sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
cplxConj :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxConj sym
sym SymCplx sym
x = do
SymReal sym
r :+ SymReal sym
i <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
SymReal sym
ic <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym SymReal sym
i
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
r forall a. a -> a -> Complex a
:+ SymReal sym
ic)
cplxExp :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxExp sym
sym SymCplx sym
x = do
(SymReal sym
rx :+ SymReal sym
i_part) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
SymReal sym
expx <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realExp sym
sym SymReal sym
rx
SymReal sym
cosx <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCos sym
sym SymReal sym
i_part
SymReal sym
sinx <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSin sym
sym SymReal sym
i_part
SymReal sym
rz <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
expx SymReal sym
cosx
SymReal sym
iz <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
expx SymReal sym
sinx
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
rz forall a. a -> a -> Complex a
:+ SymReal sym
iz)
cplxEq :: sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
cplxEq sym
sym SymCplx sym
x SymCplx sym
y = do
SymReal sym
xr :+ SymReal sym
xi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
SymReal sym
yr :+ SymReal sym
yi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
y
Pred sym
pr <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymReal sym
xr SymReal sym
yr
Pred sym
pj <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymReal sym
xi SymReal sym
yi
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
pr Pred sym
pj
cplxNe :: sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
cplxNe sym
sym SymCplx sym
x SymCplx sym
y = do
SymReal sym
xr :+ SymReal sym
xi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
SymReal sym
yr :+ SymReal sym
yi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
y
Pred sym
pr <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realNe sym
sym SymReal sym
xr SymReal sym
yr
Pred sym
pj <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realNe sym
sym SymReal sym
xi SymReal sym
yi
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
pr Pred sym
pj
newtype SymBV' sym w = MkSymBV' (SymBV sym w)
bvJoinVector :: forall sym n w. (1 <= w, IsExprBuilder sym)
=> sym
-> NatRepr w
-> Vector.Vector n (SymBV sym w)
-> IO (SymBV sym (n * w))
bvJoinVector :: forall sym (n :: Nat) (w :: Nat).
(1 <= w, IsExprBuilder sym) =>
sym
-> NatRepr w -> Vector n (SymBV sym w) -> IO (SymBV sym (n * w))
bvJoinVector sym
sym NatRepr w
w =
coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) (f :: Nat -> Type) (n :: Nat)
(w :: Nat).
(1 <= w, Monad m) =>
(forall (l :: Nat).
(1 <= l) =>
NatRepr l -> f w -> f l -> m (f (w + l)))
-> NatRepr w -> Vector n (f w) -> m (f (n * w))
Vector.joinWithM @IO @(SymBV' sym) @n forall (l :: Nat).
(1 <= l) =>
NatRepr l
-> SymBV' sym w -> SymBV' sym l -> IO (SymBV' sym (w + l))
bvConcat' NatRepr w
w
where bvConcat' :: forall l. (1 <= l)
=> NatRepr l
-> SymBV' sym w
-> SymBV' sym l
-> IO (SymBV' sym (w + l))
bvConcat' :: forall (l :: Nat).
(1 <= l) =>
NatRepr l
-> SymBV' sym w -> SymBV' sym l -> IO (SymBV' sym (w + l))
bvConcat' NatRepr l
_ (MkSymBV' SymBV sym w
x) (MkSymBV' SymBV sym l
y) = forall sym (w :: Nat). SymBV sym w -> SymBV' sym w
MkSymBV' forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Nat) (v :: Nat).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
bvConcat sym
sym SymBV sym w
x SymBV sym l
y
bvSplitVector :: forall sym n w. (IsExprBuilder sym, 1 <= w, 1 <= n)
=> sym
-> NatRepr n
-> NatRepr w
-> SymBV sym (n * w)
-> IO (Vector.Vector n (SymBV sym w))
bvSplitVector :: forall sym (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= w, 1 <= n) =>
sym
-> NatRepr n
-> NatRepr w
-> SymBV sym (n * w)
-> IO (Vector n (SymBV sym w))
bvSplitVector sym
sym NatRepr n
n NatRepr w
w SymBV sym (n * w)
x =
coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (g :: Nat -> Type) (w :: Nat)
(n :: Nat).
(Applicative f, 1 <= w, 1 <= n) =>
Endian
-> (forall (i :: Nat).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w))
-> NatRepr n
-> NatRepr w
-> g (n * w)
-> f (Vector n (g w))
Vector.splitWithA @IO Endian
BigEndian forall (i :: Nat).
((i + w) <= (n * w)) =>
NatRepr (n * w)
-> NatRepr i -> SymBV' sym (n * w) -> IO (SymBV' sym w)
bvSelect' NatRepr n
n NatRepr w
w (forall sym (w :: Nat). SymBV sym w -> SymBV' sym w
MkSymBV' @sym SymBV sym (n * w)
x)
where
bvSelect' :: forall i. (i + w <= n * w)
=> NatRepr (n * w)
-> NatRepr i
-> SymBV' sym (n * w)
-> IO (SymBV' sym w)
bvSelect' :: forall (i :: Nat).
((i + w) <= (n * w)) =>
NatRepr (n * w)
-> NatRepr i -> SymBV' sym (n * w) -> IO (SymBV' sym w)
bvSelect' NatRepr (n * w)
_ NatRepr i
i (MkSymBV' SymBV sym (n * w)
y) =
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall sym (w :: Nat). SymBV sym w -> SymBV' sym w
MkSymBV' forall a b. (a -> b) -> a -> b
$ forall sym (idx :: Nat) (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
bvSelect @_ @i @w sym
sym NatRepr i
i NatRepr w
w SymBV sym (n * w)
y
bvSwap :: forall sym n. (1 <= n, IsExprBuilder sym)
=> sym
-> NatRepr n
-> SymBV sym (n*8)
-> IO (SymBV sym (n*8))
bvSwap :: forall sym (n :: Nat).
(1 <= n, IsExprBuilder sym) =>
sym -> NatRepr n -> SymBV sym (n * 8) -> IO (SymBV sym (n * 8))
bvSwap sym
sym NatRepr n
n SymBV sym (n * 8)
v = do
forall sym (n :: Nat) (w :: Nat).
(1 <= w, IsExprBuilder sym) =>
sym
-> NatRepr w -> Vector n (SymBV sym w) -> IO (SymBV sym (n * w))
bvJoinVector sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @8) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (n :: Nat). (1 <= n) => Vector n a -> Vector n a
Vector.reverse
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= w, 1 <= n) =>
sym
-> NatRepr n
-> NatRepr w
-> SymBV sym (n * w)
-> IO (Vector n (SymBV sym w))
bvSplitVector sym
sym NatRepr n
n (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @8) SymBV sym (n * 8)
v
bvBitreverse :: forall sym w.
(1 <= w, IsExprBuilder sym) =>
sym ->
SymBV sym w ->
IO (SymBV sym w)
bvBitreverse :: forall sym (w :: Nat).
(1 <= w, IsExprBuilder sym) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvBitreverse sym
sym SymBV sym w
v = do
forall sym (n :: Nat) (w :: Nat).
(1 <= w, IsExprBuilder sym) =>
sym
-> NatRepr w -> Vector n (SymBV sym w) -> IO (SymBV sym (n * w))
bvJoinVector sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (n :: Nat). (1 <= n) => Vector n a -> Vector n a
Vector.reverse
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= w, 1 <= n) =>
sym
-> NatRepr n
-> NatRepr w
-> SymBV sym (n * w)
-> IO (Vector n (SymBV sym w))
bvSplitVector sym
sym (forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
v) (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) SymBV sym w
v
indexLit :: IsExprBuilder sym => sym -> IndexLit idx -> IO (SymExpr sym idx)
indexLit :: forall sym (idx :: BaseType).
IsExprBuilder sym =>
sym -> IndexLit idx -> IO (SymExpr sym idx)
indexLit sym
sym (IntIndexLit Integer
i) = forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
i
indexLit sym
sym (BVIndexLit NatRepr w
w BV w
v) = forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
v
iteM :: IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v) ->
sym -> Pred sym -> IO v -> IO v -> IO v
iteM :: forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> v -> v -> IO v
ite sym
sym Pred sym
p IO v
mx IO v
my = do
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
p of
Just Bool
True -> IO v
mx
Just Bool
False -> IO v
my
Maybe Bool
Nothing -> forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ sym -> Pred sym -> v -> v -> IO v
ite sym
sym Pred sym
p forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IO v
mx forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> IO v
my
iteList :: IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v) ->
sym ->
[(IO (Pred sym), IO v)] ->
(IO v) ->
IO v
iteList :: forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> [(IO (Pred sym), IO v)] -> IO v -> IO v
iteList sym -> Pred sym -> v -> v -> IO v
_ite sym
_sym [] IO v
def = IO v
def
iteList sym -> Pred sym -> v -> v -> IO v
ite sym
sym ((IO (Pred sym)
mp,IO v
mx):[(IO (Pred sym), IO v)]
xs) IO v
def =
do Pred sym
p <- IO (Pred sym)
mp
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym -> Pred sym -> v -> v -> IO v
ite sym
sym Pred sym
p IO v
mx (forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> [(IO (Pred sym), IO v)] -> IO v -> IO v
iteList sym -> Pred sym -> v -> v -> IO v
ite sym
sym [(IO (Pred sym), IO v)]
xs IO v
def)
type family SymFn sym :: Ctx BaseType -> BaseType -> Type
data SomeSymFn sym = forall args ret . SomeSymFn (SymFn sym args ret)
data SymFnWrapper sym ctx where
SymFnWrapper :: forall sym args ret . SymFn sym args ret -> SymFnWrapper sym (args ::> ret)
instance IsSymFn (SymFn sym) => TestEquality (SymFnWrapper sym) where
testEquality :: forall (a :: Ctx BaseType) (b :: Ctx BaseType).
SymFnWrapper sym a -> SymFnWrapper sym b -> Maybe (a :~: b)
testEquality (SymFnWrapper SymFn sym args ret
fn1) (SymFnWrapper SymFn sym args ret
fn2) = forall (fn :: Ctx BaseType -> BaseType -> Type)
(args1 :: Ctx BaseType) (ret1 :: BaseType) (args2 :: Ctx BaseType)
(ret2 :: BaseType).
IsSymFn fn =>
fn args1 ret1
-> fn args2 ret2 -> Maybe ((args1 ::> ret1) :~: (args2 ::> ret2))
fnTestEquality SymFn sym args ret
fn1 SymFn sym args ret
fn2
instance IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym) where
compareF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType).
SymFnWrapper sym x -> SymFnWrapper sym y -> OrderingF x y
compareF (SymFnWrapper SymFn sym args ret
fn1) (SymFnWrapper SymFn sym args ret
fn2) = forall (fn :: Ctx BaseType -> BaseType -> Type)
(args1 :: Ctx BaseType) (ret1 :: BaseType) (args2 :: Ctx BaseType)
(ret2 :: BaseType).
IsSymFn fn =>
fn args1 ret1
-> fn args2 ret2 -> OrderingF (args1 ::> ret1) (args2 ::> ret2)
fnCompare SymFn sym args ret
fn1 SymFn sym args ret
fn2
class IsSymFn (fn :: Ctx BaseType -> BaseType -> Type) where
fnArgTypes :: fn args ret -> Ctx.Assignment BaseTypeRepr args
fnReturnType :: fn args ret -> BaseTypeRepr ret
fnTestEquality :: fn args1 ret1 -> fn args2 ret2 -> Maybe ((args1 ::> ret1) :~: (args2 ::> ret2))
fnCompare :: fn args1 ret1 -> fn args2 ret2 -> OrderingF (args1 ::> ret1) (args2 ::> ret2)
data UnfoldPolicy
= NeverUnfold
| AlwaysUnfold
| UnfoldConcrete
deriving (UnfoldPolicy -> UnfoldPolicy -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UnfoldPolicy -> UnfoldPolicy -> Bool
$c/= :: UnfoldPolicy -> UnfoldPolicy -> Bool
== :: UnfoldPolicy -> UnfoldPolicy -> Bool
$c== :: UnfoldPolicy -> UnfoldPolicy -> Bool
Eq, Eq UnfoldPolicy
UnfoldPolicy -> UnfoldPolicy -> Bool
UnfoldPolicy -> UnfoldPolicy -> Ordering
UnfoldPolicy -> UnfoldPolicy -> UnfoldPolicy
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: UnfoldPolicy -> UnfoldPolicy -> UnfoldPolicy
$cmin :: UnfoldPolicy -> UnfoldPolicy -> UnfoldPolicy
max :: UnfoldPolicy -> UnfoldPolicy -> UnfoldPolicy
$cmax :: UnfoldPolicy -> UnfoldPolicy -> UnfoldPolicy
>= :: UnfoldPolicy -> UnfoldPolicy -> Bool
$c>= :: UnfoldPolicy -> UnfoldPolicy -> Bool
> :: UnfoldPolicy -> UnfoldPolicy -> Bool
$c> :: UnfoldPolicy -> UnfoldPolicy -> Bool
<= :: UnfoldPolicy -> UnfoldPolicy -> Bool
$c<= :: UnfoldPolicy -> UnfoldPolicy -> Bool
< :: UnfoldPolicy -> UnfoldPolicy -> Bool
$c< :: UnfoldPolicy -> UnfoldPolicy -> Bool
compare :: UnfoldPolicy -> UnfoldPolicy -> Ordering
$ccompare :: UnfoldPolicy -> UnfoldPolicy -> Ordering
Ord, Int -> UnfoldPolicy -> ShowS
[UnfoldPolicy] -> ShowS
UnfoldPolicy -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnfoldPolicy] -> ShowS
$cshowList :: [UnfoldPolicy] -> ShowS
show :: UnfoldPolicy -> String
$cshow :: UnfoldPolicy -> String
showsPrec :: Int -> UnfoldPolicy -> ShowS
$cshowsPrec :: Int -> UnfoldPolicy -> ShowS
Show)
shouldUnfold :: IsExpr e => UnfoldPolicy -> Ctx.Assignment e args -> Bool
shouldUnfold :: forall (e :: BaseType -> Type) (args :: Ctx BaseType).
IsExpr e =>
UnfoldPolicy -> Assignment e args -> Bool
shouldUnfold UnfoldPolicy
AlwaysUnfold Assignment e args
_ = Bool
True
shouldUnfold UnfoldPolicy
NeverUnfold Assignment e args
_ = Bool
False
shouldUnfold UnfoldPolicy
UnfoldConcrete Assignment e args
args = forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type).
FoldableFC t =>
(forall (x :: k). f x -> Bool) -> forall (x :: l). t f x -> Bool
allFC forall (e :: BaseType -> Type) (bt :: BaseType).
IsExpr e =>
e bt -> Bool
baseIsConcrete Assignment e args
args
data InvalidRange where
InvalidRange ::
BaseTypeRepr bt ->
Maybe (ConcreteValue bt) ->
Maybe (ConcreteValue bt) ->
InvalidRange
instance Exception InvalidRange
instance Show InvalidRange where
show :: InvalidRange -> String
show (InvalidRange BaseTypeRepr bt
bt Maybe (ConcreteValue bt)
mlo Maybe (ConcreteValue bt)
mhi) =
case BaseTypeRepr bt
bt of
BaseTypeRepr bt
BaseIntegerRepr -> [String] -> String
unwords [String
"invalid integer range", forall a. Show a => a -> String
show Maybe (ConcreteValue bt)
mlo, forall a. Show a => a -> String
show Maybe (ConcreteValue bt)
mhi]
BaseTypeRepr bt
BaseRealRepr -> [String] -> String
unwords [String
"invalid real range", forall a. Show a => a -> String
show Maybe (ConcreteValue bt)
mlo, forall a. Show a => a -> String
show Maybe (ConcreteValue bt)
mhi]
BaseBVRepr NatRepr w
w -> [String] -> String
unwords [String
"invalid bitvector range", forall a. Show a => a -> String
show NatRepr w
w forall a. [a] -> [a] -> [a]
++ String
"-bit", forall a. Show a => a -> String
show Maybe (ConcreteValue bt)
mlo, forall a. Show a => a -> String
show Maybe (ConcreteValue bt)
mhi]
BaseTypeRepr bt
_ -> [String] -> String
unwords [String
"invalid range for type", forall a. Show a => a -> String
show BaseTypeRepr bt
bt]
class ( IsExprBuilder sym
, IsSymFn (SymFn sym)
, OrdF (SymExpr sym)
, OrdF (BoundVar sym)
) => IsSymExprBuilder sym where
freshConstant :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshLatch :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshBoundedBV :: (1 <= w) =>
sym ->
SolverSymbol ->
NatRepr w ->
Maybe Natural ->
Maybe Natural ->
IO (SymBV sym w)
freshBoundedSBV :: (1 <= w) =>
sym ->
SolverSymbol ->
NatRepr w ->
Maybe Integer ->
Maybe Integer ->
IO (SymBV sym w)
freshBoundedInt ::
sym ->
SolverSymbol ->
Maybe Integer ->
Maybe Integer ->
IO (SymInteger sym)
freshBoundedReal ::
sym ->
SolverSymbol ->
Maybe Rational ->
Maybe Rational ->
IO (SymReal sym)
exprUninterpConstants :: sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
freshBoundVar :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
varExpr :: sym -> BoundVar sym tp -> SymExpr sym tp
forallPred :: sym
-> BoundVar sym tp
-> Pred sym
-> IO (Pred sym)
existsPred :: sym
-> BoundVar sym tp
-> Pred sym
-> IO (Pred sym)
definedFn :: sym
-> SolverSymbol
-> Ctx.Assignment (BoundVar sym) args
-> SymExpr sym ret
-> UnfoldPolicy
-> IO (SymFn sym args ret)
inlineDefineFun :: Ctx.CurryAssignmentClass args
=> sym
-> SolverSymbol
-> Ctx.Assignment BaseTypeRepr args
-> UnfoldPolicy
-> Ctx.CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
-> IO (SymFn sym args ret)
inlineDefineFun sym
sym SolverSymbol
nm Assignment BaseTypeRepr args
tps UnfoldPolicy
policy CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
f = do
Assignment (BoundVar sym) args
vars <- forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC (forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
freshBoundVar sym
sym SolverSymbol
emptySymbol) Assignment BaseTypeRepr args
tps
SymExpr sym ret
r <- forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
f (forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC (forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
varExpr sym
sym) Assignment (BoundVar sym) args
vars)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment (BoundVar sym) args
-> SymExpr sym ret
-> UnfoldPolicy
-> IO (SymFn sym args ret)
definedFn sym
sym SolverSymbol
nm Assignment (BoundVar sym) args
vars SymExpr sym ret
r UnfoldPolicy
policy
freshTotalUninterpFn :: forall args ret
. sym
-> SolverSymbol
-> Ctx.Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
applySymFn :: sym
-> SymFn sym args ret
-> Ctx.Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
substituteBoundVars ::
sym ->
MapF (BoundVar sym) (SymExpr sym) ->
SymExpr sym tp ->
IO (SymExpr sym tp)
substituteSymFns ::
sym ->
MapF (SymFnWrapper sym) (SymFnWrapper sym) ->
SymExpr sym tp ->
IO (SymExpr sym tp)
baseIsConcrete :: forall e bt
. IsExpr e
=> e bt
-> Bool
baseIsConcrete :: forall (e :: BaseType -> Type) (bt :: BaseType).
IsExpr e =>
e bt -> Bool
baseIsConcrete e bt
x =
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType e bt
x of
BaseTypeRepr bt
BaseBoolRepr -> forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred e bt
x
BaseTypeRepr bt
BaseIntegerRepr -> forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
asInteger e bt
x
BaseBVRepr NatRepr w
_ -> forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV e bt
x
BaseTypeRepr bt
BaseRealRepr -> forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational e bt
x
BaseFloatRepr FloatPrecisionRepr fpp
_ -> Bool
False
BaseStringRepr{} -> forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString e bt
x
BaseTypeRepr bt
BaseComplexRepr -> forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall (e :: BaseType -> Type).
IsExpr e =>
e BaseComplexType -> Maybe (Complex Rational)
asComplex e bt
x
BaseStructRepr Assignment BaseTypeRepr ctx
_ -> case forall (e :: BaseType -> Type) (flds :: Ctx BaseType).
IsExpr e =>
e (BaseStructType flds) -> Maybe (Assignment e flds)
asStruct e bt
x of
Just Assignment e ctx
flds -> forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type).
FoldableFC t =>
(forall (x :: k). f x -> Bool) -> forall (x :: l). t f x -> Bool
allFC forall (e :: BaseType -> Type) (bt :: BaseType).
IsExpr e =>
e bt -> Bool
baseIsConcrete Assignment e ctx
flds
Maybe (Assignment e ctx)
Nothing -> Bool
False
BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_ BaseTypeRepr xs
_bt' -> do
case forall (e :: BaseType -> Type) (idx :: Ctx BaseType)
(bt :: BaseType).
IsExpr e =>
e (BaseArrayType idx bt) -> Maybe (e bt)
asConstantArray e bt
x of
Just e xs
x' -> forall (e :: BaseType -> Type) (bt :: BaseType).
IsExpr e =>
e bt -> Bool
baseIsConcrete e xs
x'
Maybe (e xs)
Nothing -> Bool
False
baseDefaultValue :: forall sym bt
. IsExprBuilder sym
=> sym
-> BaseTypeRepr bt
-> IO (SymExpr sym bt)
baseDefaultValue :: forall sym (bt :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr bt -> IO (SymExpr sym bt)
baseDefaultValue sym
sym BaseTypeRepr bt
bt =
case BaseTypeRepr bt
bt of
BaseTypeRepr bt
BaseBoolRepr -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym
BaseTypeRepr bt
BaseIntegerRepr -> forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
0
BaseBVRepr NatRepr w
w -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w)
BaseTypeRepr bt
BaseRealRepr -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym
BaseFloatRepr FloatPrecisionRepr fpp
fpp -> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatPZero sym
sym FloatPrecisionRepr fpp
fpp
BaseTypeRepr bt
BaseComplexRepr -> forall sym.
IsExprBuilder sym =>
sym -> Complex Rational -> IO (SymCplx sym)
mkComplexLit sym
sym (Rational
0 forall a. a -> a -> Complex a
:+ Rational
0)
BaseStringRepr StringInfoRepr si
si -> forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringInfoRepr si -> IO (SymString sym si)
stringEmpty sym
sym StringInfoRepr si
si
BaseStructRepr Assignment BaseTypeRepr ctx
flds -> do
let f :: BaseTypeRepr tp -> IO (SymExpr sym tp)
f :: forall (tp :: BaseType). BaseTypeRepr tp -> IO (SymExpr sym tp)
f BaseTypeRepr tp
v = forall sym (bt :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr bt -> IO (SymExpr sym bt)
baseDefaultValue sym
sym BaseTypeRepr tp
v
forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
mkStruct sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC forall (tp :: BaseType). BaseTypeRepr tp -> IO (SymExpr sym tp)
f Assignment BaseTypeRepr ctx
flds
BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx BaseTypeRepr xs
bt' -> do
SymExpr sym xs
elt <- forall sym (bt :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr bt -> IO (SymExpr sym bt)
baseDefaultValue sym
sym BaseTypeRepr xs
bt'
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
constantArray sym
sym Assignment BaseTypeRepr (idx ::> tp)
idx SymExpr sym xs
elt
backendPred :: IsExprBuilder sym => sym -> Bool -> Pred sym
backendPred :: forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
backendPred sym
sym Bool
True = forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym
backendPred sym
sym Bool
False = forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym
mkRational :: IsExprBuilder sym => sym -> Rational -> IO (SymCplx sym)
mkRational :: forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymCplx sym)
mkRational sym
sym Rational
v = forall sym.
IsExprBuilder sym =>
sym -> Complex Rational -> IO (SymCplx sym)
mkComplexLit sym
sym (Rational
v forall a. a -> a -> Complex a
:+ Rational
0)
mkReal :: (IsExprBuilder sym, Real a) => sym -> a -> IO (SymCplx sym)
mkReal :: forall sym a.
(IsExprBuilder sym, Real a) =>
sym -> a -> IO (SymCplx sym)
mkReal sym
sym a
v = forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymCplx sym)
mkRational sym
sym (forall a. Real a => a -> Rational
toRational a
v)
predToReal :: IsExprBuilder sym => sym -> Pred sym -> IO (SymReal sym)
predToReal :: forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> IO (SymReal sym)
predToReal sym
sym Pred sym
p = do
SymReal sym
r1 <- forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
1
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
sym Pred sym
p SymReal sym
r1 (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
realExprAsRational :: (MonadFail m, IsExpr e) => e BaseRealType -> m Rational
realExprAsRational :: forall (m :: Type -> Type) (e :: BaseType -> Type).
(MonadFail m, IsExpr e) =>
e BaseRealType -> m Rational
realExprAsRational e BaseRealType
x = do
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational e BaseRealType
x of
Just Rational
r -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
r
Maybe Rational
Nothing -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Value is not a constant expression."
cplxExprAsRational :: (MonadFail m, IsExpr e) => e BaseComplexType -> m Rational
cplxExprAsRational :: forall (m :: Type -> Type) (e :: BaseType -> Type).
(MonadFail m, IsExpr e) =>
e BaseComplexType -> m Rational
cplxExprAsRational e BaseComplexType
x = do
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseComplexType -> Maybe (Complex Rational)
asComplex e BaseComplexType
x of
Just (Rational
r :+ Rational
i) -> do
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Rational
i forall a. Eq a => a -> a -> Bool
/= Rational
0) forall a b. (a -> b) -> a -> b
$
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Complex value has an imaginary part."
forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
r
Maybe (Complex Rational)
Nothing -> do
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Complex value is not a constant expression."
cplxExprAsInteger :: (MonadFail m, IsExpr e) => e BaseComplexType -> m Integer
cplxExprAsInteger :: forall (m :: Type -> Type) (e :: BaseType -> Type).
(MonadFail m, IsExpr e) =>
e BaseComplexType -> m Integer
cplxExprAsInteger e BaseComplexType
x = forall (m :: Type -> Type). MonadFail m => Rational -> m Integer
rationalAsInteger forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: Type -> Type) (e :: BaseType -> Type).
(MonadFail m, IsExpr e) =>
e BaseComplexType -> m Rational
cplxExprAsRational e BaseComplexType
x
rationalAsInteger :: MonadFail m => Rational -> m Integer
rationalAsInteger :: forall (m :: Type -> Type). MonadFail m => Rational -> m Integer
rationalAsInteger Rational
r = do
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (forall a. Ratio a -> a
denominator Rational
r forall a. Eq a => a -> a -> Bool
/= Integer
1) forall a b. (a -> b) -> a -> b
$ do
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Value is not an integer."
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall a. Ratio a -> a
numerator Rational
r)
realExprAsInteger :: (IsExpr e, MonadFail m) => e BaseRealType -> m Integer
realExprAsInteger :: forall (e :: BaseType -> Type) (m :: Type -> Type).
(IsExpr e, MonadFail m) =>
e BaseRealType -> m Integer
realExprAsInteger e BaseRealType
x =
forall (m :: Type -> Type). MonadFail m => Rational -> m Integer
rationalAsInteger forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: Type -> Type) (e :: BaseType -> Type).
(MonadFail m, IsExpr e) =>
e BaseRealType -> m Rational
realExprAsRational e BaseRealType
x
andAllOf :: IsExprBuilder sym
=> sym
-> Fold s (Pred sym)
-> s
-> IO (Pred sym)
andAllOf :: forall sym s.
IsExprBuilder sym =>
sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
andAllOf sym
sym Fold s (SymExpr sym BaseBoolType)
f s
s = forall (m :: Type -> Type) r s a.
Monad m =>
Getting (Endo (r -> m r)) s a -> (r -> a -> m r) -> r -> s -> m r
foldlMOf Fold s (SymExpr sym BaseBoolType)
f (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym) (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) s
s
orOneOf :: IsExprBuilder sym
=> sym
-> Fold s (Pred sym)
-> s
-> IO (Pred sym)
orOneOf :: forall sym s.
IsExprBuilder sym =>
sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
orOneOf sym
sym Fold s (SymExpr sym BaseBoolType)
f s
s = forall (m :: Type -> Type) r s a.
Monad m =>
Getting (Endo (r -> m r)) s a -> (r -> a -> m r) -> r -> s -> m r
foldlMOf Fold s (SymExpr sym BaseBoolType)
f (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym) (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) s
s
isNonZero :: IsExprBuilder sym => sym -> SymCplx sym -> IO (Pred sym)
isNonZero :: forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Pred sym)
isNonZero sym
sym SymCplx sym
v = forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
cplxNe sym
sym SymCplx sym
v forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymCplx sym)
mkRational sym
sym Rational
0
isReal :: IsExprBuilder sym => sym -> SymCplx sym -> IO (Pred sym)
isReal :: forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Pred sym)
isReal sym
sym SymCplx sym
v = do
SymExpr sym BaseRealType
i <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymReal sym)
getImagPart sym
sym SymCplx sym
v
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realEq sym
sym SymExpr sym BaseRealType
i (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
cplxDiv :: IsExprBuilder sym
=> sym
-> SymCplx sym
-> SymCplx sym
-> IO (SymCplx sym)
cplxDiv :: forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxDiv sym
sym SymCplx sym
x SymCplx sym
y = do
SymExpr sym BaseRealType
xr :+ SymExpr sym BaseRealType
xi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
yc :: Complex (SymExpr sym BaseRealType)
yc@(SymExpr sym BaseRealType
yr :+ SymExpr sym BaseRealType
yi) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
y
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Complex (SymExpr sym BaseRealType)
yc of
(Maybe Rational
_ :+ Just Rational
0) -> do
Complex (SymExpr sym BaseRealType)
zc <- forall a. a -> a -> Complex a
(:+) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym BaseRealType
xr SymExpr sym BaseRealType
yr forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym BaseRealType
xi SymExpr sym BaseRealType
yr
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym Complex (SymExpr sym BaseRealType)
zc
(Just Rational
0 :+ Maybe Rational
_) -> do
Complex (SymExpr sym BaseRealType)
zc <- forall a. a -> a -> Complex a
(:+) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym BaseRealType
xi SymExpr sym BaseRealType
yi forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym BaseRealType
xr SymExpr sym BaseRealType
yi
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym Complex (SymExpr sym BaseRealType)
zc
Complex (Maybe Rational)
_ -> do
SymExpr sym BaseRealType
yr_abs <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymExpr sym BaseRealType
yr SymExpr sym BaseRealType
yr
SymExpr sym BaseRealType
yi_abs <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymExpr sym BaseRealType
yi SymExpr sym BaseRealType
yi
SymExpr sym BaseRealType
y_abs <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymExpr sym BaseRealType
yr_abs SymExpr sym BaseRealType
yi_abs
SymExpr sym BaseRealType
zr_1 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymExpr sym BaseRealType
xr SymExpr sym BaseRealType
yr
SymExpr sym BaseRealType
zr_2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymExpr sym BaseRealType
xi SymExpr sym BaseRealType
yi
SymExpr sym BaseRealType
zr <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymExpr sym BaseRealType
zr_1 SymExpr sym BaseRealType
zr_2
SymExpr sym BaseRealType
zi_1 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymExpr sym BaseRealType
xi SymExpr sym BaseRealType
yr
SymExpr sym BaseRealType
zi_2 <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymExpr sym BaseRealType
xr SymExpr sym BaseRealType
yi
SymExpr sym BaseRealType
zi <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym
sym SymExpr sym BaseRealType
zi_1 SymExpr sym BaseRealType
zi_2
Complex (SymExpr sym BaseRealType)
zc <- forall a. a -> a -> Complex a
(:+) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym BaseRealType
zr SymExpr sym BaseRealType
y_abs forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym BaseRealType
zi SymExpr sym BaseRealType
y_abs
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym Complex (SymExpr sym BaseRealType)
zc
cplxLog' :: IsExprBuilder sym
=> sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxLog' :: forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxLog' sym
sym SymCplx sym
x = do
SymReal sym
xr :+ SymReal sym
xi <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymCplx sym
x
SymReal sym
xm <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realHypot sym
sym SymReal sym
xr SymReal sym
xi
SymReal sym
xa <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAtan2 sym
sym SymReal sym
xi SymReal sym
xr
SymReal sym
zr <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realLog sym
sym SymReal sym
xm
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! SymReal sym
zr forall a. a -> a -> Complex a
:+ SymReal sym
xa
cplxLog :: IsExprBuilder sym
=> sym -> SymCplx sym -> IO (SymCplx sym)
cplxLog :: forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxLog sym
sym SymCplx sym
x = forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxLog' sym
sym SymCplx sym
x
cplxLogBase :: IsExprBuilder sym
=> Rational
-> sym
-> SymCplx sym
-> IO (SymCplx sym)
cplxLogBase :: forall sym.
IsExprBuilder sym =>
Rational -> sym -> SymCplx sym -> IO (SymCplx sym)
cplxLogBase Rational
base sym
sym SymCplx sym
x = do
SymExpr sym BaseRealType
b <- forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realLog sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
base
Complex (SymExpr sym BaseRealType)
z <- forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\SymExpr sym BaseRealType
r -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymExpr sym BaseRealType
r SymExpr sym BaseRealType
b) forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxLog' sym
sym SymCplx sym
x
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym Complex (SymExpr sym BaseRealType)
z
asConcrete :: IsExpr e => e tp -> Maybe (ConcreteVal tp)
asConcrete :: forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> Maybe (ConcreteVal tp)
asConcrete e tp
x =
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType e tp
x of
BaseTypeRepr tp
BaseBoolRepr -> Bool -> ConcreteVal BaseBoolType
ConcreteBool forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred e tp
x
BaseTypeRepr tp
BaseIntegerRepr -> Integer -> ConcreteVal BaseIntegerType
ConcreteInteger forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
asInteger e tp
x
BaseTypeRepr tp
BaseRealRepr -> Rational -> ConcreteVal BaseRealType
ConcreteReal forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational e tp
x
BaseStringRepr StringInfoRepr si
_si -> forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString e tp
x
BaseTypeRepr tp
BaseComplexRepr -> Complex Rational -> ConcreteVal BaseComplexType
ConcreteComplex forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type).
IsExpr e =>
e BaseComplexType -> Maybe (Complex Rational)
asComplex e tp
x
BaseBVRepr NatRepr w
w -> forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> ConcreteVal ('BaseBVType w)
ConcreteBV NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV e tp
x
BaseFloatRepr FloatPrecisionRepr fpp
fpp -> forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp
-> BigFloat -> ConcreteVal ('BaseFloatType fpp)
ConcreteFloat FloatPrecisionRepr fpp
fpp forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type) (fpp :: FloatPrecision).
IsExpr e =>
e (BaseFloatType fpp) -> Maybe BigFloat
asFloat e tp
x
BaseStructRepr Assignment BaseTypeRepr ctx
_ -> forall (ctx :: Ctx BaseType).
Assignment ConcreteVal ctx -> ConcreteVal ('BaseStructType ctx)
ConcreteStruct forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (e :: BaseType -> Type) (flds :: Ctx BaseType).
IsExpr e =>
e (BaseStructType flds) -> Maybe (Assignment e flds)
asStruct e tp
x forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> Maybe (ConcreteVal tp)
asConcrete)
BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx BaseTypeRepr xs
_tp -> do
e xs
def <- forall (e :: BaseType -> Type) (idx :: Ctx BaseType)
(bt :: BaseType).
IsExpr e =>
e (BaseArrayType idx bt) -> Maybe (e bt)
asConstantArray e tp
x
ConcreteVal xs
c_def <- forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> Maybe (ConcreteVal tp)
asConcrete e xs
def
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (idx :: Ctx BaseType) (i :: BaseType) (b :: BaseType).
Assignment BaseTypeRepr (idx ::> i)
-> ConcreteVal b
-> Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b)
-> ConcreteVal ('BaseArrayType (idx ::> i) b)
ConcreteArray Assignment BaseTypeRepr (idx ::> tp)
idx ConcreteVal xs
c_def forall k a. Map k a
Map.empty)
concreteToSym :: IsExprBuilder sym => sym -> ConcreteVal tp -> IO (SymExpr sym tp)
concreteToSym :: forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> ConcreteVal tp -> IO (SymExpr sym tp)
concreteToSym sym
sym = \case
ConcreteBool Bool
True -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym)
ConcreteBool Bool
False -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
ConcreteInteger Integer
x -> forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
x
ConcreteReal Rational
x -> forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
x
ConcreteFloat FloatPrecisionRepr fpp
fpp BigFloat
bf -> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
floatLit sym
sym FloatPrecisionRepr fpp
fpp BigFloat
bf
ConcreteString StringLiteral si
x -> forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
stringLit sym
sym StringLiteral si
x
ConcreteComplex Complex Rational
x -> forall sym.
IsExprBuilder sym =>
sym -> Complex Rational -> IO (SymCplx sym)
mkComplexLit sym
sym Complex Rational
x
ConcreteBV NatRepr w
w BV w
x -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
x
ConcreteStruct Assignment ConcreteVal ctx
xs -> forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
mkStruct sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC (forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> ConcreteVal tp -> IO (SymExpr sym tp)
concreteToSym sym
sym) Assignment ConcreteVal ctx
xs
ConcreteArray Assignment BaseTypeRepr (idx ::> i)
idxTy ConcreteVal b
def Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b)
xs0 -> [(Assignment ConcreteVal (idx ::> i), ConcreteVal b)]
-> SymExpr sym ('BaseArrayType (idx ::> i) b)
-> IO (SymExpr sym ('BaseArrayType (idx ::> i) b))
go (forall k a. Map k a -> [(k, a)]
Map.toAscList Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b)
xs0) forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
constantArray sym
sym Assignment BaseTypeRepr (idx ::> i)
idxTy forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> ConcreteVal tp -> IO (SymExpr sym tp)
concreteToSym sym
sym ConcreteVal b
def
where
go :: [(Assignment ConcreteVal (idx ::> i), ConcreteVal b)]
-> SymExpr sym ('BaseArrayType (idx ::> i) b)
-> IO (SymExpr sym ('BaseArrayType (idx ::> i) b))
go [] SymExpr sym ('BaseArrayType (idx ::> i) b)
arr = forall (m :: Type -> Type) a. Monad m => a -> m a
return SymExpr sym ('BaseArrayType (idx ::> i) b)
arr
go ((Assignment ConcreteVal (idx ::> i)
i,ConcreteVal b
x):[(Assignment ConcreteVal (idx ::> i), ConcreteVal b)]
xs) SymExpr sym ('BaseArrayType (idx ::> i) b)
arr =
do SymExpr sym ('BaseArrayType (idx ::> i) b)
arr' <- [(Assignment ConcreteVal (idx ::> i), ConcreteVal b)]
-> SymExpr sym ('BaseArrayType (idx ::> i) b)
-> IO (SymExpr sym ('BaseArrayType (idx ::> i) b))
go [(Assignment ConcreteVal (idx ::> i), ConcreteVal b)]
xs SymExpr sym ('BaseArrayType (idx ::> i) b)
arr
Assignment (SymExpr sym) (idx ::> i)
i' <- forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC (forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> ConcreteVal tp -> IO (SymExpr sym tp)
concreteToSym sym
sym) Assignment ConcreteVal (idx ::> i)
i
SymExpr sym b
x' <- forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> ConcreteVal tp -> IO (SymExpr sym tp)
concreteToSym sym
sym ConcreteVal b
x
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
arrayUpdate sym
sym SymExpr sym ('BaseArrayType (idx ::> i) b)
arr' Assignment (SymExpr sym) (idx ::> i)
i' SymExpr sym b
x'
{-# INLINABLE muxRange #-}
muxRange :: (IsExpr e, Monad m) =>
(Natural -> m (e BaseBoolType))
->
(e BaseBoolType -> a -> a -> m a) ->
(Natural -> m a) ->
Natural ->
Natural ->
m a
muxRange :: forall (e :: BaseType -> Type) (m :: Type -> Type) a.
(IsExpr e, Monad m) =>
(Nat -> m (e BaseBoolType))
-> (e BaseBoolType -> a -> a -> m a)
-> (Nat -> m a)
-> Nat
-> Nat
-> m a
muxRange Nat -> m (e BaseBoolType)
predFn e BaseBoolType -> a -> a -> m a
iteFn Nat -> m a
f Nat
l Nat
h
| Nat
l forall a. Ord a => a -> a -> Bool
< Nat
h = do
e BaseBoolType
c <- Nat -> m (e BaseBoolType)
predFn Nat
l
case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred e BaseBoolType
c of
Just Bool
True -> Nat -> m a
f Nat
l
Just Bool
False -> forall (e :: BaseType -> Type) (m :: Type -> Type) a.
(IsExpr e, Monad m) =>
(Nat -> m (e BaseBoolType))
-> (e BaseBoolType -> a -> a -> m a)
-> (Nat -> m a)
-> Nat
-> Nat
-> m a
muxRange Nat -> m (e BaseBoolType)
predFn e BaseBoolType -> a -> a -> m a
iteFn Nat -> m a
f (forall a. Enum a => a -> a
succ Nat
l) Nat
h
Maybe Bool
Nothing ->
do a
match_branch <- Nat -> m a
f Nat
l
a
other_branch <- forall (e :: BaseType -> Type) (m :: Type -> Type) a.
(IsExpr e, Monad m) =>
(Nat -> m (e BaseBoolType))
-> (e BaseBoolType -> a -> a -> m a)
-> (Nat -> m a)
-> Nat
-> Nat
-> m a
muxRange Nat -> m (e BaseBoolType)
predFn e BaseBoolType -> a -> a -> m a
iteFn Nat -> m a
f (forall a. Enum a => a -> a
succ Nat
l) Nat
h
e BaseBoolType -> a -> a -> m a
iteFn e BaseBoolType
c a
match_branch a
other_branch
| Bool
otherwise = Nat -> m a
f Nat
h
data SymEncoder sym v tp
= SymEncoder { forall sym v (tp :: BaseType).
SymEncoder sym v tp -> BaseTypeRepr tp
symEncoderType :: !(BaseTypeRepr tp)
, forall sym v (tp :: BaseType).
SymEncoder sym v tp -> sym -> SymExpr sym tp -> IO v
symFromExpr :: !(sym -> SymExpr sym tp -> IO v)
, forall sym v (tp :: BaseType).
SymEncoder sym v tp -> sym -> v -> IO (SymExpr sym tp)
symToExpr :: !(sym -> v -> IO (SymExpr sym tp))
}
data Statistics
= Statistics { Statistics -> Integer
statAllocs :: !Integer
, Statistics -> Integer
statNonLinearOps :: !Integer
}
deriving ( Int -> Statistics -> ShowS
[Statistics] -> ShowS
Statistics -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Statistics] -> ShowS
$cshowList :: [Statistics] -> ShowS
show :: Statistics -> String
$cshow :: Statistics -> String
showsPrec :: Int -> Statistics -> ShowS
$cshowsPrec :: Int -> Statistics -> ShowS
Show )
zeroStatistics :: Statistics
zeroStatistics :: Statistics
zeroStatistics = Statistics { statAllocs :: Integer
statAllocs = Integer
0
, statNonLinearOps :: Integer
statNonLinearOps = Integer
0 }