{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module What4.Expr.GroundEval
(
GroundValue
, GroundValueWrapper(..)
, GroundArray(..)
, lookupArray
, GroundEvalFn(..)
, ExprRangeBindings
, tryEvalGroundExpr
, evalGroundExpr
, evalGroundApp
, evalGroundNonceApp
, defaultValueForType
, groundEq
) where
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
import qualified Data.BitVector.Sized as BV
import Data.List.NonEmpty (NonEmpty(..))
import Data.Foldable
import qualified Data.Map.Strict as Map
import Data.Maybe ( fromMaybe )
import Data.Parameterized.Ctx
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr
import Data.Parameterized.TraversableFC
import Data.Ratio
import LibBF (BigFloat)
import qualified LibBF as BF
import What4.BaseTypes
import What4.Interface
import qualified What4.SemiRing as SR
import qualified What4.SpecialFunctions as SFn
import qualified What4.Expr.ArrayUpdateMap as AUM
import qualified What4.Expr.BoolMap as BM
import What4.Expr.Builder
import qualified What4.Expr.StringSeq as SSeq
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.Expr.UnaryBV as UnaryBV
import What4.Utils.Arithmetic ( roundAway )
import What4.Utils.Complex
import What4.Utils.FloatHelpers
import What4.Utils.StringLiteral
type family GroundValue (tp :: BaseType) where
GroundValue BaseBoolType = Bool
GroundValue BaseIntegerType = Integer
GroundValue BaseRealType = Rational
GroundValue (BaseBVType w) = BV.BV w
GroundValue (BaseFloatType fpp) = BigFloat
GroundValue BaseComplexType = Complex Rational
GroundValue (BaseStringType si) = StringLiteral si
GroundValue (BaseArrayType idx b) = GroundArray idx b
GroundValue (BaseStructType ctx) = Ctx.Assignment GroundValueWrapper ctx
newtype GroundEvalFn t = GroundEvalFn { forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
groundEval :: forall tp . Expr t tp -> IO (GroundValue tp) }
type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)
newtype GroundValueWrapper tp = GVW { forall (tp :: BaseType). GroundValueWrapper tp -> GroundValue tp
unGVW :: GroundValue tp }
data GroundArray idx b
= ArrayMapping (Ctx.Assignment GroundValueWrapper idx -> IO (GroundValue b))
| ArrayConcrete (GroundValue b) (Map.Map (Ctx.Assignment IndexLit idx) (GroundValue b))
lookupArray :: Ctx.Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Ctx.Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray :: forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray Assignment BaseTypeRepr idx
_ (ArrayMapping Assignment GroundValueWrapper idx -> IO (GroundValue b)
f) Assignment GroundValueWrapper idx
i = Assignment GroundValueWrapper idx -> IO (GroundValue b)
f Assignment GroundValueWrapper idx
i
lookupArray Assignment BaseTypeRepr idx
tps (ArrayConcrete GroundValue b
base Map (Assignment IndexLit idx) (GroundValue b)
m) Assignment GroundValueWrapper idx
i = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe GroundValue b
base (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Assignment IndexLit idx
i' Map (Assignment IndexLit idx) (GroundValue b)
m)
where i' :: Assignment IndexLit idx
i' = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => [Char] -> a
error [Char]
"lookupArray: not valid indexLits") forall a b. (a -> b) -> a -> b
$ forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
(h :: k -> Type) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
Ctx.zipWithM forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValueWrapper tp -> Maybe (IndexLit tp)
asIndexLit Assignment BaseTypeRepr idx
tps Assignment GroundValueWrapper idx
i
updateArray ::
Ctx.Assignment BaseTypeRepr idx ->
GroundArray idx b ->
Ctx.Assignment GroundValueWrapper idx ->
GroundValue b ->
IO (GroundArray idx b)
updateArray :: forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> GroundValue b
-> IO (GroundArray idx b)
updateArray Assignment BaseTypeRepr idx
idx_tps GroundArray idx b
arr Assignment GroundValueWrapper idx
idx GroundValue b
val =
case GroundArray idx b
arr of
ArrayMapping Assignment GroundValueWrapper idx -> IO (GroundValue b)
arr' -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (idx :: Ctx BaseType) (b :: BaseType).
(Assignment GroundValueWrapper idx -> IO (GroundValue b))
-> GroundArray idx b
ArrayMapping forall a b. (a -> b) -> a -> b
$ \Assignment GroundValueWrapper idx
x ->
if forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx
-> Assignment GroundValueWrapper ctx
-> Assignment GroundValueWrapper ctx
-> Bool
indicesEq Assignment BaseTypeRepr idx
idx_tps Assignment GroundValueWrapper idx
idx Assignment GroundValueWrapper idx
x then forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GroundValue b
val else Assignment GroundValueWrapper idx -> IO (GroundValue b)
arr' Assignment GroundValueWrapper idx
x
ArrayConcrete GroundValue b
d Map (Assignment IndexLit idx) (GroundValue b)
m -> do
let idx' :: Assignment IndexLit idx
idx' = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => [Char] -> a
error [Char]
"UpdateArray only supported on Nat and BV") forall a b. (a -> b) -> a -> b
$ forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
(h :: k -> Type) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
Ctx.zipWithM forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValueWrapper tp -> Maybe (IndexLit tp)
asIndexLit Assignment BaseTypeRepr idx
idx_tps Assignment GroundValueWrapper idx
idx
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete GroundValue b
d (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Assignment IndexLit idx
idx' GroundValue b
val Map (Assignment IndexLit idx) (GroundValue b)
m)
where indicesEq :: Ctx.Assignment BaseTypeRepr ctx
-> Ctx.Assignment GroundValueWrapper ctx
-> Ctx.Assignment GroundValueWrapper ctx
-> Bool
indicesEq :: forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx
-> Assignment GroundValueWrapper ctx
-> Assignment GroundValueWrapper ctx
-> Bool
indicesEq Assignment BaseTypeRepr ctx
tps Assignment GroundValueWrapper ctx
x Assignment GroundValueWrapper ctx
y =
forall k (ctx :: Ctx k).
Size ctx -> (forall (tp :: k). Index ctx tp -> Bool) -> Bool
forallIndex (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment GroundValueWrapper ctx
x) forall a b. (a -> b) -> a -> b
$ \Index ctx tp
j ->
let GVW GroundValue tp
xj = Assignment GroundValueWrapper ctx
x forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
j
GVW GroundValue tp
yj = Assignment GroundValueWrapper ctx
y forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
j
tp :: BaseTypeRepr tp
tp = Assignment BaseTypeRepr ctx
tps forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
j
in case BaseTypeRepr tp
tp of
BaseTypeRepr tp
BaseIntegerRepr -> GroundValue tp
xj forall a. Eq a => a -> a -> Bool
== GroundValue tp
yj
BaseBVRepr NatRepr w
_ -> GroundValue tp
xj forall a. Eq a => a -> a -> Bool
== GroundValue tp
yj
BaseTypeRepr tp
_ -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"We do not yet support UpdateArray on " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show BaseTypeRepr tp
tp forall a. [a] -> [a] -> [a]
++ [Char]
" indices."
asIndexLit :: BaseTypeRepr tp -> GroundValueWrapper tp -> Maybe (IndexLit tp)
asIndexLit :: forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValueWrapper tp -> Maybe (IndexLit tp)
asIndexLit BaseTypeRepr tp
BaseIntegerRepr (GVW GroundValue tp
v) = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer -> IndexLit 'BaseIntegerType
IntIndexLit GroundValue tp
v
asIndexLit (BaseBVRepr NatRepr w
w) (GVW GroundValue tp
v) = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> IndexLit ('BaseBVType w)
BVIndexLit NatRepr w
w GroundValue tp
v
asIndexLit BaseTypeRepr tp
_ GroundValueWrapper tp
_ = forall a. Maybe a
Nothing
toDouble :: Rational -> Double
toDouble :: Rational -> Double
toDouble = forall a. Fractional a => Rational -> a
fromRational
fromDouble :: Double -> Rational
fromDouble :: Double -> Rational
fromDouble = forall a. Real a => a -> Rational
toRational
defaultValueForType :: BaseTypeRepr tp -> GroundValue tp
defaultValueForType :: forall (tp :: BaseType). BaseTypeRepr tp -> GroundValue tp
defaultValueForType BaseTypeRepr tp
tp =
case BaseTypeRepr tp
tp of
BaseTypeRepr tp
BaseBoolRepr -> Bool
False
BaseBVRepr NatRepr w
w -> forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w
BaseTypeRepr tp
BaseIntegerRepr -> Integer
0
BaseTypeRepr tp
BaseRealRepr -> Rational
0
BaseTypeRepr tp
BaseComplexRepr -> Rational
0 forall a. a -> a -> Complex a
:+ Rational
0
BaseStringRepr StringInfoRepr si
si -> forall (si :: StringInfo). StringInfoRepr si -> StringLiteral si
stringLitEmpty StringInfoRepr si
si
BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_ BaseTypeRepr xs
b -> forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete (forall (tp :: BaseType). BaseTypeRepr tp -> GroundValue tp
defaultValueForType BaseTypeRepr xs
b) forall k a. Map k a
Map.empty
BaseStructRepr Assignment BaseTypeRepr ctx
ctx -> 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 (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (tp :: BaseType). BaseTypeRepr tp -> GroundValue tp
defaultValueForType) Assignment BaseTypeRepr ctx
ctx
BaseFloatRepr FloatPrecisionRepr fpp
_fpp -> BigFloat
BF.bfPosZero
{-# INLINABLE evalGroundExpr #-}
evalGroundExpr :: (forall u . Expr t u -> IO (GroundValue u))
-> Expr t tp
-> IO (GroundValue tp)
evalGroundExpr :: forall t (tp :: BaseType).
(forall (u :: BaseType). Expr t u -> IO (GroundValue u))
-> Expr t tp -> IO (GroundValue tp)
evalGroundExpr forall (u :: BaseType). Expr t u -> IO (GroundValue u)
f Expr t tp
e =
forall (m :: Type -> Type) a. MaybeT m a -> m (Maybe a)
runMaybeT (forall t (tp :: BaseType).
(forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> Expr t tp -> MaybeT IO (GroundValue tp)
tryEvalGroundExpr (forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: BaseType). Expr t u -> IO (GroundValue u)
f) Expr t tp
e) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just GroundValue tp
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return GroundValue tp
x
Maybe (GroundValue tp)
Nothing
| BoundVarExpr ExprBoundVar t tp
v <- Expr t tp
e ->
case forall t (tp :: BaseType). ExprBoundVar t tp -> VarKind
bvarKind ExprBoundVar t tp
v of
VarKind
QuantifierVarKind -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"The ground evaluator does not support bound variables."
VarKind
LatchVarKind -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall (tp :: BaseType). BaseTypeRepr tp -> GroundValue tp
defaultValueForType (forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar t tp
v)
VarKind
UninterpVarKind -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall (tp :: BaseType). BaseTypeRepr tp -> GroundValue tp
defaultValueForType (forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar t tp
v)
| Bool
otherwise -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
"evalGroundExpr: could not evaluate expression:", forall a. Show a => a -> [Char]
show Expr t tp
e]
{-# INLINABLE tryEvalGroundExpr #-}
tryEvalGroundExpr :: (forall u . Expr t u -> MaybeT IO (GroundValue u))
-> Expr t tp
-> MaybeT IO (GroundValue tp)
tryEvalGroundExpr :: forall t (tp :: BaseType).
(forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> Expr t tp -> MaybeT IO (GroundValue tp)
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (SemiRingLiteral SemiRingRepr sr
SR.SemiRingIntegerRepr Coefficient sr
c ProgramLoc
_) = forall (m :: Type -> Type) a. Monad m => a -> m a
return Coefficient sr
c
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (SemiRingLiteral SemiRingRepr sr
SR.SemiRingRealRepr Coefficient sr
c ProgramLoc
_) = forall (m :: Type -> Type) a. Monad m => a -> m a
return Coefficient sr
c
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (SemiRingLiteral (SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
_ ) Coefficient sr
c ProgramLoc
_) = forall (m :: Type -> Type) a. Monad m => a -> m a
return Coefficient sr
c
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (StringExpr StringLiteral si
x ProgramLoc
_) = forall (m :: Type -> Type) a. Monad m => a -> m a
return StringLiteral si
x
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (BoolExpr Bool
b ProgramLoc
_) = forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
b
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (FloatExpr FloatPrecisionRepr fpp
_ BigFloat
f ProgramLoc
_) = forall (m :: Type -> Type) a. Monad m => a -> m a
return BigFloat
f
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f (NonceAppExpr NonceAppExpr t tp
a0) = forall (m :: Type -> Type) t (tp :: BaseType).
Monad m =>
(forall (u :: BaseType). Expr t u -> MaybeT m (GroundValue u))
-> NonceApp t (Expr t) tp -> MaybeT m (GroundValue tp)
evalGroundNonceApp forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f (forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t tp
a0)
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f (AppExpr AppExpr t tp
a0) = forall t (tp :: BaseType).
(forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> App (Expr t) tp -> MaybeT IO (GroundValue tp)
evalGroundApp forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f (forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
a0)
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (BoundVarExpr ExprBoundVar t tp
_) = forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
{-# INLINABLE evalGroundNonceApp #-}
evalGroundNonceApp :: Monad m
=> (forall u . Expr t u -> MaybeT m (GroundValue u))
-> NonceApp t (Expr t) tp
-> MaybeT m (GroundValue tp)
evalGroundNonceApp :: forall (m :: Type -> Type) t (tp :: BaseType).
Monad m =>
(forall (u :: BaseType). Expr t u -> MaybeT m (GroundValue u))
-> NonceApp t (Expr t) tp -> MaybeT m (GroundValue tp)
evalGroundNonceApp forall (u :: BaseType). Expr t u -> MaybeT m (GroundValue u)
fn NonceApp t (Expr t) tp
a0 =
case NonceApp t (Expr t) tp
a0 of
Annotation BaseTypeRepr tp
_ Nonce t tp
_ Expr t tp
t -> forall (u :: BaseType). Expr t u -> MaybeT m (GroundValue u)
fn Expr t tp
t
Forall{} -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
Exists{} -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
MapOverArrays{} -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
ArrayFromFn{} -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
ArrayTrueOnEntries{} -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
FnApp{} -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
{-# INLINABLE evalGroundApp #-}
forallIndex :: Ctx.Size (ctx :: Ctx.Ctx k) -> (forall tp . Ctx.Index ctx tp -> Bool) -> Bool
forallIndex :: forall k (ctx :: Ctx k).
Size ctx -> (forall (tp :: k). Index ctx tp -> Bool) -> Bool
forallIndex Size ctx
sz forall (tp :: k). Index ctx tp -> Bool
f = forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex Size ctx
sz (\Bool
b Index ctx tp
j -> forall (tp :: k). Index ctx tp -> Bool
f Index ctx tp
j Bool -> Bool -> Bool
&& Bool
b) Bool
True
newtype MAnd x = MAnd { forall {k} (x :: k). MAnd x -> Maybe Bool
unMAnd :: Maybe Bool }
instance Functor MAnd where
fmap :: forall a b. (a -> b) -> MAnd a -> MAnd b
fmap a -> b
_f (MAnd Maybe Bool
x) = forall {k} (x :: k). Maybe Bool -> MAnd x
MAnd Maybe Bool
x
instance Applicative MAnd where
pure :: forall a. a -> MAnd a
pure a
_ = forall {k} (x :: k). Maybe Bool -> MAnd x
MAnd (forall a. a -> Maybe a
Just Bool
True)
MAnd (Just Bool
a) <*> :: forall a b. MAnd (a -> b) -> MAnd a -> MAnd b
<*> MAnd (Just Bool
b) = forall {k} (x :: k). Maybe Bool -> MAnd x
MAnd (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! (Bool
a Bool -> Bool -> Bool
&& Bool
b))
MAnd (a -> b)
_ <*> MAnd a
_ = forall {k} (x :: k). Maybe Bool -> MAnd x
MAnd forall a. Maybe a
Nothing
mand :: Bool -> MAnd z
mand :: forall {k} (z :: k). Bool -> MAnd z
mand = forall {k} (x :: k). Maybe Bool -> MAnd x
MAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
coerceMAnd :: MAnd a -> MAnd b
coerceMAnd :: forall {k} {k} (a :: k) (b :: k). MAnd a -> MAnd b
coerceMAnd (MAnd Maybe Bool
x) = forall {k} (x :: k). Maybe Bool -> MAnd x
MAnd Maybe Bool
x
groundEq :: BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
groundEq :: forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
groundEq BaseTypeRepr tp
bt0 GroundValue tp
x0 GroundValue tp
y0 = forall {k} (x :: k). MAnd x -> Maybe Bool
unMAnd (forall {k} (tp :: BaseType) (z :: k).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> MAnd z
f BaseTypeRepr tp
bt0 GroundValue tp
x0 GroundValue tp
y0)
where
f :: BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> MAnd z
f :: forall {k} (tp :: BaseType) (z :: k).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> MAnd z
f BaseTypeRepr tp
bt GroundValue tp
x GroundValue tp
y = case BaseTypeRepr tp
bt of
BaseTypeRepr tp
BaseBoolRepr -> forall {k} (z :: k). Bool -> MAnd z
mand forall a b. (a -> b) -> a -> b
$ GroundValue tp
x forall a. Eq a => a -> a -> Bool
== GroundValue tp
y
BaseTypeRepr tp
BaseRealRepr -> forall {k} (z :: k). Bool -> MAnd z
mand forall a b. (a -> b) -> a -> b
$ GroundValue tp
x forall a. Eq a => a -> a -> Bool
== GroundValue tp
y
BaseTypeRepr tp
BaseIntegerRepr -> forall {k} (z :: k). Bool -> MAnd z
mand forall a b. (a -> b) -> a -> b
$ GroundValue tp
x forall a. Eq a => a -> a -> Bool
== GroundValue tp
y
BaseBVRepr NatRepr w
_ -> forall {k} (z :: k). Bool -> MAnd z
mand forall a b. (a -> b) -> a -> b
$ GroundValue tp
x forall a. Eq a => a -> a -> Bool
== GroundValue tp
y
BaseFloatRepr FloatPrecisionRepr fpp
_ -> forall {k} (z :: k). Bool -> MAnd z
mand forall a b. (a -> b) -> a -> b
$ BigFloat -> BigFloat -> Ordering
BF.bfCompare GroundValue tp
x GroundValue tp
y forall a. Eq a => a -> a -> Bool
== Ordering
EQ
BaseStringRepr StringInfoRepr si
_ -> forall {k} (z :: k). Bool -> MAnd z
mand forall a b. (a -> b) -> a -> b
$ GroundValue tp
x forall a. Eq a => a -> a -> Bool
== GroundValue tp
y
BaseTypeRepr tp
BaseComplexRepr -> forall {k} (z :: k). Bool -> MAnd z
mand forall a b. (a -> b) -> a -> b
$ GroundValue tp
x forall a. Eq a => a -> a -> Bool
== GroundValue tp
y
BaseStructRepr Assignment BaseTypeRepr ctx
flds ->
forall {k} {k} (a :: k) (b :: k). MAnd a -> MAnd b
coerceMAnd (forall {k} (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type)
(g :: k -> Type).
Applicative m =>
(forall (tp :: k). Index ctx tp -> f tp -> m (g tp))
-> Assignment f ctx -> m (Assignment g ctx)
Ctx.traverseWithIndex
(\Index ctx tp
i BaseTypeRepr tp
tp -> forall {k} (tp :: BaseType) (z :: k).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> MAnd z
f BaseTypeRepr tp
tp (forall (tp :: BaseType). GroundValueWrapper tp -> GroundValue tp
unGVW (GroundValue tp
x forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i)) (forall (tp :: BaseType). GroundValueWrapper tp -> GroundValue tp
unGVW (GroundValue tp
y forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i))) Assignment BaseTypeRepr ctx
flds)
BaseArrayRepr{} -> forall {k} (x :: k). Maybe Bool -> MAnd x
MAnd forall a. Maybe a
Nothing
evalGroundApp :: forall t tp
. (forall u . Expr t u -> MaybeT IO (GroundValue u))
-> App (Expr t) tp
-> MaybeT IO (GroundValue tp)
evalGroundApp :: forall t (tp :: BaseType).
(forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> App (Expr t) tp -> MaybeT IO (GroundValue tp)
evalGroundApp forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f App (Expr t) tp
a0 = do
case App (Expr t) tp
a0 of
BaseEq BaseTypeRepr tp1
bt Expr t tp1
x Expr t tp1
y ->
do GroundValue tp1
x' <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp1
x
GroundValue tp1
y' <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp1
y
forall (m :: Type -> Type) a. m (Maybe a) -> MaybeT m a
MaybeT (forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
groundEq BaseTypeRepr tp1
bt GroundValue tp1
x' GroundValue tp1
y'))
BaseIte BaseTypeRepr tp
_ Integer
_ Expr t 'BaseBoolType
x Expr t tp
y Expr t tp
z -> do
Bool
xv <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseBoolType
x
if Bool
xv then forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp
y else forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp
z
NotPred Expr t 'BaseBoolType
x -> Bool -> Bool
not forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseBoolType
x
ConjPred BoolMap (Expr t)
xs ->
let pol :: (Expr t 'BaseBoolType, Polarity)
-> MaybeT IO (GroundValue 'BaseBoolType)
pol (Expr t 'BaseBoolType
x,Polarity
Positive) = forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseBoolType
x
pol (Expr t 'BaseBoolType
x,Polarity
Negative) = Bool -> Bool
not forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseBoolType
x
in
case forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
BM.viewBoolMap BoolMap (Expr t)
xs of
BoolMapView (Expr t)
BM.BoolMapUnit -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
True
BoolMapView (Expr t)
BM.BoolMapDualUnit -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False
BM.BoolMapTerms ((Expr t 'BaseBoolType, Polarity)
t:|[(Expr t 'BaseBoolType, Polarity)]
ts) ->
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Bool -> Bool -> Bool
(&&) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t 'BaseBoolType, Polarity)
-> MaybeT IO (GroundValue 'BaseBoolType)
pol (Expr t 'BaseBoolType, Polarity)
t forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Expr t 'BaseBoolType, Polarity)
-> MaybeT IO (GroundValue 'BaseBoolType)
pol [(Expr t 'BaseBoolType, Polarity)]
ts
RealIsInteger Expr t 'BaseRealType
x -> (\Rational
xv -> forall a. Ratio a -> a
denominator Rational
xv forall a. Eq a => a -> a -> Bool
== Integer
1) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
BVTestBit Natural
i Expr t (BaseBVType w)
x ->
forall (w :: Natural). Natural -> BV w -> Bool
BV.testBit' Natural
i forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
BVSlt Expr t (BaseBVType w)
x Expr t (BaseBVType w)
y -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> Bool
BV.slt NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
y
where w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x
BVUlt Expr t (BaseBVType w)
x Expr t (BaseBVType w)
y -> forall (w :: Natural). BV w -> BV w -> Bool
BV.ult forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
y
IntDiv Expr t 'BaseIntegerType
x Expr t 'BaseIntegerType
y -> forall {a}. Integral a => a -> a -> a
g forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
y
where
g :: a -> a -> a
g a
u a
v | a
v forall a. Eq a => a -> a -> Bool
== a
0 = a
0
| a
v forall a. Ord a => a -> a -> Bool
> a
0 = a
u forall {a}. Integral a => a -> a -> a
`div` a
v
| Bool
otherwise = forall a. Num a => a -> a
negate (a
u forall {a}. Integral a => a -> a -> a
`div` forall a. Num a => a -> a
negate a
v)
IntMod Expr t 'BaseIntegerType
x Expr t 'BaseIntegerType
y -> forall {a}. Num a => Integer -> Integer -> a
intModu forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
y
where intModu :: Integer -> Integer -> a
intModu Integer
_ Integer
0 = a
0
intModu Integer
i Integer
v = forall a. Num a => Integer -> a
fromInteger (Integer
i forall {a}. Integral a => a -> a -> a
`mod` forall a. Num a => a -> a
abs Integer
v)
IntAbs Expr t 'BaseIntegerType
x -> forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
abs forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
x
IntDivisible Expr t 'BaseIntegerType
x Natural
k -> Integer -> Bool
g forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
x
where
g :: Integer -> Bool
g Integer
u | Natural
k forall a. Eq a => a -> a -> Bool
== Natural
0 = Integer
u forall a. Eq a => a -> a -> Bool
== Integer
0
| Bool
otherwise = forall {a}. Integral a => a -> a -> a
mod Integer
u (forall a. Integral a => a -> Integer
toInteger Natural
k) forall a. Eq a => a -> a -> Bool
== Integer
0
SemiRingLe OrderedSemiRingRepr sr
SR.OrderedSemiRingRealRepr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y -> forall a. Ord a => a -> a -> Bool
(<=) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (SemiRingBase sr)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (SemiRingBase sr)
y
SemiRingLe OrderedSemiRingRepr sr
SR.OrderedSemiRingIntegerRepr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y -> forall a. Ord a => a -> a -> Bool
(<=) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (SemiRingBase sr)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (SemiRingBase sr)
y
SemiRingSum WeightedSum (Expr t) sr
s ->
case forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum (Expr t) sr
s of
SemiRingRepr sr
SR.SemiRingIntegerRepr -> forall (m :: Type -> Type) r (sr :: SemiRing)
(f :: BaseType -> Type).
Monad m =>
(r -> r -> m r)
-> (Coefficient sr -> f (SemiRingBase sr) -> m r)
-> (Coefficient sr -> m r)
-> WeightedSum f sr
-> m r
WSum.evalM (\GroundValue 'BaseIntegerType
x GroundValue 'BaseIntegerType
y -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (GroundValue 'BaseIntegerType
xforall a. Num a => a -> a -> a
+GroundValue 'BaseIntegerType
y)) GroundValue 'BaseIntegerType
-> Expr t 'BaseIntegerType
-> MaybeT IO (GroundValue 'BaseIntegerType)
smul forall (f :: Type -> Type) a. Applicative f => a -> f a
pure WeightedSum (Expr t) sr
s
where smul :: GroundValue 'BaseIntegerType
-> Expr t 'BaseIntegerType
-> MaybeT IO (GroundValue 'BaseIntegerType)
smul GroundValue 'BaseIntegerType
sm Expr t 'BaseIntegerType
e = (GroundValue 'BaseIntegerType
sm forall a. Num a => a -> a -> a
*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
e
SemiRingRepr sr
SR.SemiRingRealRepr -> forall (m :: Type -> Type) r (sr :: SemiRing)
(f :: BaseType -> Type).
Monad m =>
(r -> r -> m r)
-> (Coefficient sr -> f (SemiRingBase sr) -> m r)
-> (Coefficient sr -> m r)
-> WeightedSum f sr
-> m r
WSum.evalM (\GroundValue 'BaseRealType
x GroundValue 'BaseRealType
y -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (GroundValue 'BaseRealType
xforall a. Num a => a -> a -> a
+GroundValue 'BaseRealType
y)) GroundValue 'BaseRealType
-> Expr t 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
smul forall (f :: Type -> Type) a. Applicative f => a -> f a
pure WeightedSum (Expr t) sr
s
where smul :: GroundValue 'BaseRealType
-> Expr t 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
smul GroundValue 'BaseRealType
sm Expr t 'BaseRealType
e = (GroundValue 'BaseRealType
sm forall a. Num a => a -> a -> a
*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
e
SR.SemiRingBVRepr BVFlavorRepr fv
SR.BVArithRepr NatRepr w
w -> forall (m :: Type -> Type) r (sr :: SemiRing)
(f :: BaseType -> Type).
Monad m =>
(r -> r -> m r)
-> (Coefficient sr -> f (SemiRingBase sr) -> m r)
-> (Coefficient sr -> m r)
-> WeightedSum f sr
-> m r
WSum.evalM BV w -> BV w -> MaybeT IO (BV w)
sadd BV w -> Expr t (BaseBVType w) -> MaybeT IO (BV w)
smul forall (f :: Type -> Type) a. Applicative f => a -> f a
pure WeightedSum (Expr t) sr
s
where
smul :: BV w -> Expr t (BaseBVType w) -> MaybeT IO (BV w)
smul BV w
sm Expr t (BaseBVType w)
e = forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
w BV w
sm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
e
sadd :: BV w -> BV w -> MaybeT IO (BV w)
sadd BV w
x BV w
y = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
x BV w
y)
SR.SemiRingBVRepr BVFlavorRepr fv
SR.BVBitsRepr NatRepr w
_w -> forall (m :: Type -> Type) r (sr :: SemiRing)
(f :: BaseType -> Type).
Monad m =>
(r -> r -> m r)
-> (Coefficient sr -> f (SemiRingBase sr) -> m r)
-> (Coefficient sr -> m r)
-> WeightedSum f sr
-> m r
WSum.evalM forall {f :: Type -> Type} {w :: Natural}.
Applicative f =>
BV w -> BV w -> f (BV w)
sadd BV w -> Expr t (BaseBVType w) -> MaybeT IO (BV w)
smul forall (f :: Type -> Type) a. Applicative f => a -> f a
pure WeightedSum (Expr t) sr
s
where
smul :: BV w -> Expr t (BaseBVType w) -> MaybeT IO (BV w)
smul BV w
sm Expr t (BaseBVType w)
e = forall (w :: Natural). BV w -> BV w -> BV w
BV.and BV w
sm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
e
sadd :: BV w -> BV w -> f (BV w)
sadd BV w
x BV w
y = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (w :: Natural). BV w -> BV w -> BV w
BV.xor BV w
x BV w
y)
SemiRingProd SemiRingProduct (Expr t) sr
pd ->
case forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct (Expr t) sr
pd of
SemiRingRepr sr
SR.SemiRingIntegerRepr -> forall a. a -> Maybe a -> a
fromMaybe Integer
1 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) r (f :: BaseType -> Type)
(sr :: SemiRing).
Monad m =>
(r -> r -> m r)
-> (f (SemiRingBase sr) -> m r)
-> SemiRingProduct f sr
-> m (Maybe r)
WSum.prodEvalM (\Integer
x Integer
y -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer
xforall a. Num a => a -> a -> a
*Integer
y)) forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f SemiRingProduct (Expr t) sr
pd
SemiRingRepr sr
SR.SemiRingRealRepr -> forall a. a -> Maybe a -> a
fromMaybe Rational
1 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) r (f :: BaseType -> Type)
(sr :: SemiRing).
Monad m =>
(r -> r -> m r)
-> (f (SemiRingBase sr) -> m r)
-> SemiRingProduct f sr
-> m (Maybe r)
WSum.prodEvalM (\Rational
x Rational
y -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Rational
xforall a. Num a => a -> a -> a
*Rational
y)) forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f SemiRingProduct (Expr t) sr
pd
SR.SemiRingBVRepr BVFlavorRepr fv
SR.BVArithRepr NatRepr w
w ->
forall a. a -> Maybe a -> a
fromMaybe (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr w
w) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) r (f :: BaseType -> Type)
(sr :: SemiRing).
Monad m =>
(r -> r -> m r)
-> (f (SemiRingBase sr) -> m r)
-> SemiRingProduct f sr
-> m (Maybe r)
WSum.prodEvalM (\BV w
x BV w
y -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
w BV w
x BV w
y)) forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f SemiRingProduct (Expr t) sr
pd
SR.SemiRingBVRepr BVFlavorRepr fv
SR.BVBitsRepr NatRepr w
w ->
forall a. a -> Maybe a -> a
fromMaybe (forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) r (f :: BaseType -> Type)
(sr :: SemiRing).
Monad m =>
(r -> r -> m r)
-> (f (SemiRingBase sr) -> m r)
-> SemiRingProduct f sr
-> m (Maybe r)
WSum.prodEvalM (\BV w
x BV w
y -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (w :: Natural). BV w -> BV w -> BV w
BV.and BV w
x BV w
y)) forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f SemiRingProduct (Expr t) sr
pd
RealDiv Expr t 'BaseRealType
x Expr t 'BaseRealType
y -> do
Rational
xv <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
Rational
yv <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
y
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$!
if Rational
yv forall a. Eq a => a -> a -> Bool
== Rational
0 then Rational
0 else Rational
xv forall a. Fractional a => a -> a -> a
/ Rational
yv
RealSqrt Expr t 'BaseRealType
x -> do
Rational
xv <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Rational
xv forall a. Ord a => a -> a -> Bool
< Rational
0) forall a b. (a -> b) -> a -> b
$ do
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"Model returned sqrt of negative number."
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> Rational
fromDouble (forall a. Floating a => a -> a
sqrt (Rational -> Double
toDouble Rational
xv))
RealSpecialFunction SpecialFunction args
fn (SFn.SpecialFnArgs Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args) ->
let sf1 :: (Double -> Double) ->
Ctx.Assignment (SFn.SpecialFnArg (Expr t) BaseRealType) (EmptyCtx ::> SFn.R) ->
MaybeT IO (GroundValue BaseRealType)
sf1 :: (Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 Double -> Double
dfn (Assignment (SpecialFnArg (Expr t) 'BaseRealType) ctx
Ctx.Empty Ctx.:> SFn.SpecialFnArg Expr t 'BaseRealType
x) = Double -> Rational
fromDouble forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
dfn forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
toDouble forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
sf2 :: (Double -> Double -> Double) ->
Ctx.Assignment (SFn.SpecialFnArg (Expr t) BaseRealType) (EmptyCtx ::> SFn.R ::> SFn.R) ->
MaybeT IO (GroundValue BaseRealType)
sf2 :: (Double -> Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) ((EmptyCtx ::> R) ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf2 Double -> Double -> Double
dfn (Assignment (SpecialFnArg (Expr t) 'BaseRealType) ctx
Ctx.Empty Ctx.:> SFn.SpecialFnArg Expr t 'BaseRealType
x Ctx.:> SFn.SpecialFnArg Expr t 'BaseRealType
y) =
do Rational
xv <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
Rational
yv <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
y
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> Rational
fromDouble (Double -> Double -> Double
dfn (Rational -> Double
toDouble Rational
xv) (Rational -> Double
toDouble Rational
yv))
in case SpecialFunction args
fn of
SpecialFunction args
SFn.Pi -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> Rational
fromDouble forall a. Floating a => a
pi
SpecialFunction args
SFn.Sin -> (Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 forall a. Floating a => a -> a
sin Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args
SpecialFunction args
SFn.Cos -> (Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 forall a. Floating a => a -> a
cos Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args
SpecialFunction args
SFn.Sinh -> (Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 forall a. Floating a => a -> a
sinh Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args
SpecialFunction args
SFn.Cosh -> (Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 forall a. Floating a => a -> a
cosh Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args
SpecialFunction args
SFn.Exp -> (Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 forall a. Floating a => a -> a
exp Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args
SpecialFunction args
SFn.Log -> (Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 forall a. Floating a => a -> a
log Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args
SpecialFunction args
SFn.Arctan2 -> (Double -> Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) ((EmptyCtx ::> R) ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf2 forall a. RealFloat a => a -> a -> a
atan2 Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args
SpecialFunction args
SFn.Pow -> (Double -> Double -> Double)
-> Assignment
(SpecialFnArg (Expr t) 'BaseRealType) ((EmptyCtx ::> R) ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf2 forall a. Floating a => a -> a -> a
(**) Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args
SpecialFunction args
_ -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
BVOrBits NatRepr w
w BVOrSet (Expr t) w
bs -> forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall (w :: Natural). BV w -> BV w -> BV w
BV.or (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f (forall (e :: BaseType -> Type) (w :: Natural).
BVOrSet e w -> [e (BaseBVType w)]
bvOrToList BVOrSet (Expr t) w
bs)
BVUnaryTerm UnaryBV (Expr t 'BaseBoolType) n
u ->
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV (forall p (n :: Natural). UnaryBV p n -> NatRepr n
UnaryBV.width UnaryBV (Expr t 'BaseBoolType) n
u) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) p (n :: Natural).
Monad m =>
(p -> m Bool) -> UnaryBV p n -> m Integer
UnaryBV.evaluate forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f UnaryBV (Expr t 'BaseBoolType) n
u
BVConcat NatRepr (u + v)
_w Expr t (BaseBVType u)
x Expr t (BaseBVType v)
y -> forall (w :: Natural) (w' :: Natural).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
BV.concat (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType u)
x) (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType v)
y) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType u)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType v)
y
BVSelect NatRepr idx
idx NatRepr n
n Expr t (BaseBVType w)
x -> forall (ix :: Natural) (w' :: Natural) (w :: Natural).
((ix + w') <= w) =>
NatRepr ix -> NatRepr w' -> BV w -> BV w'
BV.select NatRepr idx
idx NatRepr n
n forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
BVUdiv NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> BV w -> BV w -> BV w
myDiv forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
y
where myDiv :: BV w -> BV w -> BV w
myDiv BV w
_ (BV.BV Integer
0) = forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w
myDiv BV w
u BV w
v = forall (w :: Natural). BV w -> BV w -> BV w
BV.uquot BV w
u BV w
v
BVUrem NatRepr w
_w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> forall (w :: Natural). BV w -> BV w -> BV w
myRem forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
y
where myRem :: BV w -> BV w -> BV w
myRem BV w
u (BV.BV Integer
0) = BV w
u
myRem BV w
u BV w
v = forall (w :: Natural). BV w -> BV w -> BV w
BV.urem BV w
u BV w
v
BVSdiv NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> BV w -> BV w -> BV w
myDiv forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
y
where myDiv :: BV w -> BV w -> BV w
myDiv BV w
_ (BV.BV Integer
0) = forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w
myDiv BV w
u BV w
v = forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> BV w
BV.sdiv NatRepr w
w BV w
u BV w
v
BVSrem NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> BV w -> BV w -> BV w
myRem forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
y
where myRem :: BV w -> BV w -> BV w
myRem BV w
u (BV.BV Integer
0) = BV w
u
myRem BV w
u BV w
v = forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> BV w
BV.srem NatRepr w
w BV w
u BV w
v
BVShl NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.shl NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (w :: Natural). BV w -> Natural
BV.asNatural forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
y)
BVLshr NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.lshr NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (w :: Natural). BV w -> Natural
BV.asNatural forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
y)
BVAshr NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> Natural -> BV w
BV.ashr NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (w :: Natural). BV w -> Natural
BV.asNatural forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
y)
BVRol NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.rotateL NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (w :: Natural). BV w -> Natural
BV.asNatural forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
y)
BVRor NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.rotateR NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (w :: Natural). BV w -> Natural
BV.asNatural forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
y)
BVZext NatRepr r
w Expr t (BaseBVType w)
x -> forall (w :: Natural) (w' :: Natural).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext NatRepr r
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
BVSext NatRepr r
w Expr t (BaseBVType w)
x ->
case forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr r
w of
Just LeqProof 1 r
LeqProof -> forall (w :: Natural) (w' :: Natural).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x) NatRepr r
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
Maybe (LeqProof 1 r)
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"BVSext given bad width"
BVFill NatRepr w
w Expr t 'BaseBoolType
p ->
do Bool
b <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseBoolType
p
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! if Bool
b then forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w else forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w
BVPopcount NatRepr w
_w Expr t ('BaseBVType w)
x ->
forall (w :: Natural). BV w -> BV w
BV.popCount forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x
BVCountLeadingZeros NatRepr w
w Expr t ('BaseBVType w)
x ->
forall (w :: Natural). NatRepr w -> BV w -> BV w
BV.clz NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x
BVCountTrailingZeros NatRepr w
w Expr t ('BaseBVType w)
x ->
forall (w :: Natural). NatRepr w -> BV w -> BV w
BV.ctz NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseBVType w)
x
FloatNeg FloatPrecisionRepr fpp
_fpp Expr t ('BaseFloatType fpp)
x -> BigFloat -> BigFloat
BF.bfNeg forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x
FloatAbs FloatPrecisionRepr fpp
_fpp Expr t ('BaseFloatType fpp)
x -> BigFloat -> BigFloat
BF.bfAbs forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x
FloatSqrt FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t ('BaseFloatType fpp)
x -> forall a. HasCallStack => (a, Status) -> a
bfStatus forall b c a. (b -> c) -> (a -> b) -> a -> c
. BFOpts -> BigFloat -> (BigFloat, Status)
BF.bfSqrt (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x
FloatRound FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t ('BaseFloatType fpp)
x -> forall (fpp :: FloatPrecision).
HasCallStack =>
FloatPrecisionRepr fpp -> RoundingMode -> BigFloat -> BigFloat
floatRoundToInt FloatPrecisionRepr fpp
fpp RoundingMode
r forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x
FloatAdd FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t ('BaseFloatType fpp)
x Expr t ('BaseFloatType fpp)
y -> forall a. HasCallStack => (a, Status) -> a
bfStatus forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfAdd (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
y)
FloatSub FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t ('BaseFloatType fpp)
x Expr t ('BaseFloatType fpp)
y -> forall a. HasCallStack => (a, Status) -> a
bfStatus forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfSub (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
y)
FloatMul FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t ('BaseFloatType fpp)
x Expr t ('BaseFloatType fpp)
y -> forall a. HasCallStack => (a, Status) -> a
bfStatus forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfMul (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
y)
FloatDiv FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t ('BaseFloatType fpp)
x Expr t ('BaseFloatType fpp)
y -> forall a. HasCallStack => (a, Status) -> a
bfStatus forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfDiv (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
y)
FloatRem FloatPrecisionRepr fpp
fpp Expr t ('BaseFloatType fpp)
x Expr t ('BaseFloatType fpp)
y -> forall a. HasCallStack => (a, Status) -> a
bfStatus forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfRem (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
RNE) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
y)
FloatFMA FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t ('BaseFloatType fpp)
x Expr t ('BaseFloatType fpp)
y Expr t ('BaseFloatType fpp)
z -> forall a. HasCallStack => (a, Status) -> a
bfStatus forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfFMA (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
y forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseFloatType fpp)
z)
FloatFpEq Expr t (BaseFloatType fpp)
x Expr t (BaseFloatType fpp)
y -> forall a. Eq a => a -> a -> Bool
(==) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
y
FloatLe Expr t (BaseFloatType fpp)
x Expr t (BaseFloatType fpp)
y -> forall a. Ord a => a -> a -> Bool
(<=) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
y
FloatLt Expr t (BaseFloatType fpp)
x Expr t (BaseFloatType fpp)
y -> forall a. Ord a => a -> a -> Bool
(<) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
y
FloatIsNaN Expr t (BaseFloatType fpp)
x -> BigFloat -> Bool
BF.bfIsNaN forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
FloatIsZero Expr t (BaseFloatType fpp)
x -> BigFloat -> Bool
BF.bfIsZero forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
FloatIsInf Expr t (BaseFloatType fpp)
x -> BigFloat -> Bool
BF.bfIsInf forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
FloatIsPos Expr t (BaseFloatType fpp)
x -> BigFloat -> Bool
BF.bfIsPos forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
FloatIsNeg Expr t (BaseFloatType fpp)
x -> BigFloat -> Bool
BF.bfIsNeg forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
FloatIsNorm Expr t (BaseFloatType fpp)
x ->
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType Expr t (BaseFloatType fpp)
x of
BaseFloatRepr FloatPrecisionRepr fpp
fpp ->
BFOpts -> BigFloat -> Bool
BF.bfIsNormal (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
RNE) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
FloatIsSubnorm Expr t (BaseFloatType fpp)
x ->
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType Expr t (BaseFloatType fpp)
x of
BaseFloatRepr FloatPrecisionRepr fpp
fpp ->
BFOpts -> BigFloat -> Bool
BF.bfIsSubnormal (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
RNE) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
FloatFromBinary FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp Expr t (BaseBVType (eb + sb))
x ->
BFOpts -> Integer -> BigFloat
BF.bfFromBits (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp RoundingMode
RNE) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Natural). BV w -> Integer
BV.asUnsigned forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType (eb + sb))
x
FloatToBinary fpp :: FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp@(FloatingPointPrecisionRepr NatRepr eb
eb NatRepr sb
sb) Expr t (BaseFloatType (FloatingPointPrecision eb sb))
x ->
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr eb
eb NatRepr sb
sb) forall b c a. (b -> c) -> (a -> b) -> a -> c
. BFOpts -> BigFloat -> Integer
BF.bfToBits (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp RoundingMode
RNE) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType (FloatingPointPrecision eb sb))
x
FloatCast FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t (BaseFloatType fpp')
x -> forall a. HasCallStack => (a, Status) -> a
bfStatus forall b c a. (b -> c) -> (a -> b) -> a -> c
. BFOpts -> BigFloat -> (BigFloat, Status)
BF.bfRoundFloat (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp')
x
RealToFloat FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t 'BaseRealType
x -> BFOpts -> Rational -> BigFloat
floatFromRational (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
BVToFloat FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t (BaseBVType w)
x -> BFOpts -> Integer -> BigFloat
floatFromInteger (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Natural). BV w -> Integer
BV.asUnsigned forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
SBVToFloat FloatPrecisionRepr fpp
fpp RoundingMode
r Expr t (BaseBVType w)
x -> BFOpts -> Integer -> BigFloat
floatFromInteger (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
FloatToReal Expr t (BaseFloatType fpp)
x -> forall (m :: Type -> Type) a. m (Maybe a) -> MaybeT m a
MaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. BigFloat -> Maybe Rational
floatToRational forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
FloatToBV NatRepr w
w RoundingMode
r Expr t (BaseFloatType fpp)
x ->
do Maybe Integer
z <- RoundingMode -> BigFloat -> Maybe Integer
floatToInteger RoundingMode
r forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
case Maybe Integer
z of
Just Integer
i | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
i Bool -> Bool -> Bool
&& Integer
i forall a. Ord a => a -> a -> Bool
<= forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
i)
Maybe Integer
_ -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
FloatToSBV NatRepr w
w RoundingMode
r Expr t (BaseFloatType fpp)
x ->
do Maybe Integer
z <- RoundingMode -> BigFloat -> Maybe Integer
floatToInteger RoundingMode
r forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
case Maybe Integer
z of
Just Integer
i | forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr w
w forall a. Ord a => a -> a -> Bool
<= Integer
i Bool -> Bool -> Bool
&& Integer
i forall a. Ord a => a -> a -> Bool
<= forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
i)
Maybe Integer
_ -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
FloatSpecialFunction FloatPrecisionRepr fpp
_ SpecialFunction args
_ SpecialFnArgs (Expr t) ('BaseFloatType fpp) args
_ -> forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
ArrayMap Assignment BaseTypeRepr (i ::> itp)
idx_types BaseTypeRepr tp1
_ ArrayUpdateMap (Expr t) (i ::> itp) tp1
m Expr t ('BaseArrayType (i ::> itp) tp1)
def -> do
Map (Assignment IndexLit (i ::> itp)) (GroundValue tp1)
m' <- forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f (forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
(tp :: BaseType).
ArrayUpdateMap e ctx tp -> Map (Assignment IndexLit ctx) (e tp)
AUM.toMap ArrayUpdateMap (Expr t) (i ::> itp) tp1
m)
GroundArray (i ::> itp) tp1
h <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseArrayType (i ::> itp) tp1)
def
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case GroundArray (i ::> itp) tp1
h of
ArrayMapping Assignment GroundValueWrapper (i ::> itp) -> IO (GroundValue tp1)
h' -> forall (idx :: Ctx BaseType) (b :: BaseType).
(Assignment GroundValueWrapper idx -> IO (GroundValue b))
-> GroundArray idx b
ArrayMapping forall a b. (a -> b) -> a -> b
$ \Assignment GroundValueWrapper (i ::> itp)
idx ->
case (forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map (Assignment IndexLit (i ::> itp)) (GroundValue tp1)
m') forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
(h :: k -> Type) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
Ctx.zipWithM forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValueWrapper tp -> Maybe (IndexLit tp)
asIndexLit Assignment BaseTypeRepr (i ::> itp)
idx_types Assignment GroundValueWrapper (i ::> itp)
idx of
Just GroundValue tp1
r -> forall (m :: Type -> Type) a. Monad m => a -> m a
return GroundValue tp1
r
Maybe (GroundValue tp1)
Nothing -> Assignment GroundValueWrapper (i ::> itp) -> IO (GroundValue tp1)
h' Assignment GroundValueWrapper (i ::> itp)
idx
ArrayConcrete GroundValue tp1
d Map (Assignment IndexLit (i ::> itp)) (GroundValue tp1)
m'' ->
forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete GroundValue tp1
d (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map (Assignment IndexLit (i ::> itp)) (GroundValue tp1)
m' Map (Assignment IndexLit (i ::> itp)) (GroundValue tp1)
m'')
ConstantArray Assignment BaseTypeRepr (i ::> tp1)
_ BaseTypeRepr b
_ Expr t b
v -> do
GroundValue b
val <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t b
v
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete GroundValue b
val forall k a. Map k a
Map.empty
SelectArray BaseTypeRepr tp
_ Expr t (BaseArrayType (i ::> tp1) tp)
a Assignment (Expr t) (i ::> tp1)
i -> do
GroundArray (i ::> tp1) tp
arr <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseArrayType (i ::> tp1) tp)
a
let arrIdxTps :: Assignment BaseTypeRepr (i ::> tp1)
arrIdxTps = case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType Expr t (BaseArrayType (i ::> tp1) tp)
a of
BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx BaseTypeRepr xs
_ -> Assignment BaseTypeRepr (idx ::> tp)
idx
Assignment GroundValueWrapper (i ::> tp1)
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 (\Expr t x
e -> forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t x
e) Assignment (Expr t) (i ::> tp1)
i
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray Assignment BaseTypeRepr (i ::> tp1)
arrIdxTps GroundArray (i ::> tp1) tp
arr Assignment GroundValueWrapper (i ::> tp1)
idx
UpdateArray BaseTypeRepr b
_ Assignment BaseTypeRepr (i ::> tp1)
idx_tps Expr t ('BaseArrayType (i ::> tp1) b)
a Assignment (Expr t) (i ::> tp1)
i Expr t b
v -> do
GroundArray (i ::> tp1) b
arr <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseArrayType (i ::> tp1) b)
a
Assignment GroundValueWrapper (i ::> tp1)
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 (\Expr t x
e -> forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t x
e) Assignment (Expr t) (i ::> tp1)
i
GroundValue b
v' <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t b
v
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> GroundValue b
-> IO (GroundArray idx b)
updateArray Assignment BaseTypeRepr (i ::> tp1)
idx_tps GroundArray (i ::> tp1) b
arr Assignment GroundValueWrapper (i ::> tp1)
idx GroundValue b
v'
CopyArray NatRepr w
w BaseTypeRepr a
_ Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
dest_arr Expr t (BaseBVType w)
dest_idx Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
src_arr Expr t (BaseBVType w)
src_idx Expr t (BaseBVType w)
len Expr t (BaseBVType w)
_ Expr t (BaseBVType w)
_ -> do
GroundArray (SingleCtx (BaseBVType w)) a
ground_dest_arr <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
dest_arr
BV w
ground_dest_idx <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
dest_idx
GroundArray (SingleCtx (BaseBVType w)) a
ground_src_arr <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
src_arr
BV w
ground_src_idx <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
src_idx
BV w
ground_len <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
len
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
(\GroundArray (SingleCtx (BaseBVType w)) a
arr_acc (BV w
dest_i, BV w
src_i) ->
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> GroundValue b
-> IO (GroundArray idx b)
updateArray (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
arr_acc (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
dest_i)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
ground_src_arr (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
src_i))
GroundArray (SingleCtx (BaseBVType w)) a
ground_dest_arr
(forall a b. [a] -> [b] -> [(a, b)]
zip
(forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_dest_idx (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_dest_idx BV w
ground_len) (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1)))
(forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_src_idx (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_src_idx BV w
ground_len) (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1))))
SetArray NatRepr w
w BaseTypeRepr a
_ Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
arr Expr t (BaseBVType w)
idx Expr t a
val Expr t (BaseBVType w)
len Expr t (BaseBVType w)
_ -> do
GroundArray (SingleCtx (BaseBVType w)) a
ground_arr <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
arr
BV w
ground_idx <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
idx
GroundValue a
ground_val <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t a
val
BV w
ground_len <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
len
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
(\GroundArray (SingleCtx (BaseBVType w)) a
arr_acc BV w
i ->
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> GroundValue b
-> IO (GroundArray idx b)
updateArray (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
arr_acc (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
i) GroundValue a
ground_val)
GroundArray (SingleCtx (BaseBVType w)) a
ground_arr
(forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_idx (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_idx BV w
ground_len) (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1)))
EqualArrayRange NatRepr w
w BaseTypeRepr a
a_repr Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
lhs_arr Expr t (BaseBVType w)
lhs_idx Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
rhs_arr Expr t (BaseBVType w)
rhs_idx Expr t (BaseBVType w)
len Expr t (BaseBVType w)
_ Expr t (BaseBVType w)
_ -> do
GroundArray (SingleCtx (BaseBVType w)) a
ground_lhs_arr <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
lhs_arr
BV w
ground_lhs_idx <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
lhs_idx
GroundArray (SingleCtx (BaseBVType w)) a
ground_rhs_arr <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
rhs_arr
BV w
ground_rhs_idx <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
rhs_idx
BV w
ground_len <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
len
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
(\Bool
acc (BV w
lhs_i, BV w
rhs_i) -> do
Bool
ground_eq_res <- forall (m :: Type -> Type) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
groundEq BaseTypeRepr a
a_repr forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
ground_lhs_arr (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
lhs_i) forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*>
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
ground_rhs_arr (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
rhs_i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool
acc Bool -> Bool -> Bool
&& Bool
ground_eq_res)
Bool
True
(forall a b. [a] -> [b] -> [(a, b)]
zip
(forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_lhs_idx (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_lhs_idx BV w
ground_len) (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1)))
(forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_rhs_idx (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_rhs_idx BV w
ground_len) (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1))))
IntegerToReal Expr t 'BaseIntegerType
x -> forall a. Real a => a -> Rational
toRational forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
x
BVToInteger Expr t (BaseBVType w)
x -> forall (w :: Natural). BV w -> Integer
BV.asUnsigned forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
SBVToInteger Expr t (BaseBVType w)
x -> forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
RoundReal Expr t 'BaseRealType
x -> forall a. RealFrac a => a -> Integer
roundAway forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
RoundEvenReal Expr t 'BaseRealType
x -> forall a b. (RealFrac a, Integral b) => a -> b
round forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
FloorReal Expr t 'BaseRealType
x -> forall a b. (RealFrac a, Integral b) => a -> b
floor forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
CeilReal Expr t 'BaseRealType
x -> forall a b. (RealFrac a, Integral b) => a -> b
ceiling forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
RealToInteger Expr t 'BaseRealType
x -> forall a b. (RealFrac a, Integral b) => a -> b
floor forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x
IntegerToBV Expr t 'BaseIntegerType
x NatRepr w
w -> forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
x
Cplx (Expr t 'BaseRealType
x :+ Expr t 'BaseRealType
y) -> forall a. a -> a -> Complex a
(:+) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseRealType
y
RealPart Expr t 'BaseComplexType
x -> forall a. Complex a -> a
realPart forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseComplexType
x
ImagPart Expr t 'BaseComplexType
x -> forall a. Complex a -> a
imagPart forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseComplexType
x
StringLength Expr t (BaseStringType si)
x -> forall (si :: StringInfo). StringLiteral si -> Integer
stringLitLength forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x
StringContains Expr t (BaseStringType si)
x Expr t (BaseStringType si)
y -> forall (si :: StringInfo).
StringLiteral si -> StringLiteral si -> Bool
stringLitContains forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
y
StringIsSuffixOf Expr t (BaseStringType si)
x Expr t (BaseStringType si)
y -> forall (si :: StringInfo).
StringLiteral si -> StringLiteral si -> Bool
stringLitIsSuffixOf forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
y
StringIsPrefixOf Expr t (BaseStringType si)
x Expr t (BaseStringType si)
y -> forall (si :: StringInfo).
StringLiteral si -> StringLiteral si -> Bool
stringLitIsPrefixOf forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
y
StringIndexOf Expr t (BaseStringType si)
x Expr t (BaseStringType si)
y Expr t 'BaseIntegerType
k -> forall (si :: StringInfo).
StringLiteral si -> StringLiteral si -> Integer -> Integer
stringLitIndexOf forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
y forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
k
StringSubstring StringInfoRepr si
_ Expr t ('BaseStringType si)
x Expr t 'BaseIntegerType
off Expr t 'BaseIntegerType
len -> forall (si :: StringInfo).
StringLiteral si -> Integer -> Integer -> StringLiteral si
stringLitSubstring forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseStringType si)
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
off forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t 'BaseIntegerType
len
StringAppend StringInfoRepr si
si StringSeq (Expr t) si
xs ->
do let g :: StringLiteral si
-> StringSeqEntry (Expr t) si -> MaybeT IO (StringLiteral si)
g StringLiteral si
x (SSeq.StringSeqLiteral StringLiteral si
l) = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StringLiteral si
x forall a. Semigroup a => a -> a -> a
<> StringLiteral si
l)
g StringLiteral si
x (SSeq.StringSeqTerm Expr t ('BaseStringType si)
t) = (StringLiteral si
x forall a. Semigroup a => a -> a -> a
<>) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseStringType si)
t
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM StringLiteral si
-> StringSeqEntry (Expr t) si -> MaybeT IO (StringLiteral si)
g (forall (si :: StringInfo). StringInfoRepr si -> StringLiteral si
stringLitEmpty StringInfoRepr si
si) (forall (e :: BaseType -> Type) (si :: StringInfo).
StringSeq e si -> [StringSeqEntry e si]
SSeq.toList StringSeq (Expr t) si
xs)
StructCtor Assignment BaseTypeRepr flds
_ Assignment (Expr t) flds
flds -> do
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 (\Expr t x
v -> forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t x
v) Assignment (Expr t) flds
flds
StructField Expr t (BaseStructType flds)
s Index flds tp
i BaseTypeRepr tp
_ -> do
Assignment GroundValueWrapper flds
sv <- forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStructType flds)
s
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall (tp :: BaseType). GroundValueWrapper tp -> GroundValue tp
unGVW (Assignment GroundValueWrapper flds
sv forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index flds tp
i)