------------------------------------------------------------------------
-- |
-- Module      : What4.Expr.GroundEval
-- Description : Computing ground values for expressions from solver assignments
-- Copyright   : (c) Galois, Inc 2016-2020
-- License     : BSD3
-- Maintainer  : Joe Hendrix <jhendrix@galois.com>
-- Stability   : provisional
--
-- Given a collection of assignments to the symbolic values appearing in
-- an expression, this module computes the ground value.
------------------------------------------------------------------------

{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module What4.Expr.GroundEval
  ( -- * Ground evaluation
    GroundValue
  , GroundValueWrapper(..)
  , GroundArray(..)
  , lookupArray
  , GroundEvalFn(..)
  , ExprRangeBindings

    -- * Internal operations
  , 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

-- | A function that calculates ground values for elements.
--   Clients of solvers should use the @groundEval@ function for computing
--   values in models.
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) }

-- | Function that calculates upper and lower bounds for real-valued elements.
--   This type is used for solvers (e.g., dReal) that give only approximate solutions.
type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)

-- | A newtype wrapper around ground value for use in a cache.
newtype GroundValueWrapper tp = GVW { forall (tp :: BaseType). GroundValueWrapper tp -> GroundValue tp
unGVW :: GroundValue tp }

-- | A representation of a ground-value array.
data GroundArray idx b
  = ArrayMapping (Ctx.Assignment GroundValueWrapper idx -> IO (GroundValue b))
    -- ^ Lookup function for querying by index
  | ArrayConcrete (GroundValue b) (Map.Map (Ctx.Assignment IndexLit idx) (GroundValue b))
    -- ^ Default value and finite map of particular indices

-- | Look up an index in an ground array.
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

-- | Update a ground array.
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

-- | Convert a real standardmodel val to a double.
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

-- | Construct a default value for a given base type.
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 #-}
-- | Helper function for evaluating @Expr@ expressions in a model.
--
--   This function is intended for implementers of symbolic backends.
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 #-}
-- | Evaluate an element, when given an evaluation function for
--   subelements.  Instead of recursing directly, `tryEvalGroundExpr`
--   calls into the given function on sub-elements to allow the caller
--   to cache results if desired.
--
--   However, sometimes we are unable to compute expressions outside
--   the solver.  In these cases, this function will return `Nothing`
--   in the `MaybeT IO` monad.  In these cases, the caller should instead
--   query the solver directly to evaluate the expression, if possible.
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 #-}
-- | Helper function for evaluating @NonceApp@ expressions.
--
--   This function is intended for implementers of symbolic backends.
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
      -- NB, don't use (==) for BigFloat, which is the wrong equality
      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

-- | Helper function for evaluating @App@ expressions.
--
--   This function is intended for implementers of symbolic backends.
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))

    ------------------------------------------------------------------------
    -- Operations that introduce irrational numbers.

    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 -- TODO, other functions as well

    ------------------------------------------------------------------------
    -- Bitvector Operations

    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
    -- BGS: This check can be proven to GHC
    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

    ------------------------------------------------------------------------
    -- Floating point Operations

    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 -- NB, IEEE754 equality
    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 -- TODO? evaluate concretely?

    ------------------------------------------------------------------------
    -- Array Operations

    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'' ->
          -- Map.union is left-biased
          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))))

    ------------------------------------------------------------------------
    -- Conversions

    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

    ------------------------------------------------------------------------
    -- Complex operations.

    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

    ------------------------------------------------------------------------
    -- String operations

    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)

    ------------------------------------------------------------------------
    -- Structs

    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)