------------------------------------------------------------------------
-- |
-- 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

#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail( MonadFail )
#endif

import           Control.Monad
import           Control.Monad.Trans.Class
import           Control.Monad.Trans.Maybe
import qualified Data.BitVector.Sized as BV
import           Data.List (foldl')
import           Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Map.Strict as Map
import           Data.Maybe ( fromMaybe )
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.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 { 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 { 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 :: 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 = GroundValue b -> IO (GroundValue b)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundValue b -> IO (GroundValue b))
-> GroundValue b -> IO (GroundValue b)
forall a b. (a -> b) -> a -> b
$ GroundValue b -> Maybe (GroundValue b) -> GroundValue b
forall a. a -> Maybe a -> a
fromMaybe GroundValue b
base (Assignment IndexLit idx
-> Map (Assignment IndexLit idx) (GroundValue b)
-> Maybe (GroundValue b)
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' = Assignment IndexLit idx
-> Maybe (Assignment IndexLit idx) -> Assignment IndexLit idx
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> Assignment IndexLit idx
forall a. HasCallStack => [Char] -> a
error [Char]
"lookupArray: not valid indexLits") (Maybe (Assignment IndexLit idx) -> Assignment IndexLit idx)
-> Maybe (Assignment IndexLit idx) -> Assignment IndexLit idx
forall a b. (a -> b) -> a -> b
$ (forall (x :: BaseType).
 BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x))
-> Assignment BaseTypeRepr idx
-> Assignment GroundValueWrapper idx
-> Maybe (Assignment IndexLit idx)
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 (x :: BaseType).
BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x)
asIndexLit Assignment BaseTypeRepr idx
tps Assignment GroundValueWrapper idx
i

asIndexLit :: BaseTypeRepr tp -> GroundValueWrapper tp -> Maybe (IndexLit tp)
asIndexLit :: BaseTypeRepr tp -> GroundValueWrapper tp -> Maybe (IndexLit tp)
asIndexLit BaseTypeRepr tp
BaseIntegerRepr (GVW GroundValue tp
v) = IndexLit BaseIntegerType -> Maybe (IndexLit BaseIntegerType)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (IndexLit BaseIntegerType -> Maybe (IndexLit BaseIntegerType))
-> IndexLit BaseIntegerType -> Maybe (IndexLit BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ Integer -> IndexLit BaseIntegerType
IntIndexLit Integer
GroundValue tp
v
asIndexLit (BaseBVRepr NatRepr w
w)  (GVW GroundValue tp
v) = IndexLit (BaseBVType w) -> Maybe (IndexLit (BaseBVType w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (IndexLit (BaseBVType w) -> Maybe (IndexLit (BaseBVType w)))
-> IndexLit (BaseBVType w) -> Maybe (IndexLit (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> IndexLit (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> IndexLit (BaseBVType w)
BVIndexLit NatRepr w
w BV w
GroundValue tp
v
asIndexLit BaseTypeRepr tp
_ GroundValueWrapper tp
_ = Maybe (IndexLit tp)
forall a. Maybe a
Nothing

-- | Convert a real standardmodel val to a double.
toDouble :: Rational -> Double
toDouble :: Rational -> Double
toDouble = Rational -> Double
forall a. Fractional a => Rational -> a
fromRational

fromDouble :: Double -> Rational
fromDouble :: Double -> Rational
fromDouble = Double -> Rational
forall a. Real a => a -> Rational
toRational

-- | Construct a default value for a given base type.
defaultValueForType :: BaseTypeRepr tp -> GroundValue tp
defaultValueForType :: BaseTypeRepr tp -> GroundValue tp
defaultValueForType BaseTypeRepr tp
tp =
  case BaseTypeRepr tp
tp of
    BaseTypeRepr tp
BaseBoolRepr    -> Bool
GroundValue tp
False
    BaseBVRepr NatRepr w
w    -> NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w
    BaseTypeRepr tp
BaseIntegerRepr -> GroundValue tp
0
    BaseTypeRepr tp
BaseRealRepr    -> GroundValue tp
0
    BaseTypeRepr tp
BaseComplexRepr -> Rational
0 Rational -> Rational -> Complex Rational
forall a. a -> a -> Complex a
:+ Rational
0
    BaseStringRepr StringInfoRepr si
si -> StringInfoRepr si -> StringLiteral si
forall (si :: StringInfo). StringInfoRepr si -> StringLiteral si
stringLitEmpty StringInfoRepr si
si
    BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_ BaseTypeRepr xs
b -> GroundValue xs
-> Map (Assignment IndexLit (idx ::> tp)) (GroundValue xs)
-> GroundArray (idx ::> tp) xs
forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete (BaseTypeRepr xs -> GroundValue xs
forall (tp :: BaseType). BaseTypeRepr tp -> GroundValue tp
defaultValueForType BaseTypeRepr xs
b) Map (Assignment IndexLit (idx ::> tp)) (GroundValue xs)
forall k a. Map k a
Map.empty
    BaseStructRepr Assignment BaseTypeRepr ctx
ctx -> (forall (x :: BaseType). BaseTypeRepr x -> GroundValueWrapper x)
-> Assignment BaseTypeRepr ctx -> Assignment GroundValueWrapper 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 (GroundValue x -> GroundValueWrapper x
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW (GroundValue x -> GroundValueWrapper x)
-> (BaseTypeRepr x -> GroundValue x)
-> BaseTypeRepr x
-> GroundValueWrapper x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseTypeRepr x -> GroundValue x
forall (tp :: BaseType). BaseTypeRepr tp -> GroundValue tp
defaultValueForType) Assignment BaseTypeRepr ctx
ctx
    BaseFloatRepr FloatPrecisionRepr fpp
_fpp -> BigFloat
GroundValue tp
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 (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 =
 MaybeT IO (GroundValue tp) -> IO (Maybe (GroundValue tp))
forall (m :: Type -> Type) a. MaybeT m a -> m (Maybe a)
runMaybeT ((forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> Expr t tp -> MaybeT IO (GroundValue tp)
forall t (tp :: BaseType).
(forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> Expr t tp -> MaybeT IO (GroundValue tp)
tryEvalGroundExpr (IO (GroundValue u) -> MaybeT IO (GroundValue u)
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (GroundValue u) -> MaybeT IO (GroundValue u))
-> (Expr t u -> IO (GroundValue u))
-> Expr t u
-> MaybeT IO (GroundValue u)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr t u -> IO (GroundValue u)
forall (u :: BaseType). Expr t u -> IO (GroundValue u)
f) Expr t tp
e) IO (Maybe (GroundValue tp))
-> (Maybe (GroundValue tp) -> IO (GroundValue tp))
-> IO (GroundValue tp)
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just GroundValue tp
x -> GroundValue tp -> IO (GroundValue tp)
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 ExprBoundVar t tp -> VarKind
forall t (tp :: BaseType). ExprBoundVar t tp -> VarKind
bvarKind ExprBoundVar t tp
v of
            VarKind
QuantifierVarKind -> [Char] -> IO (GroundValue tp)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO (GroundValue tp)) -> [Char] -> IO (GroundValue tp)
forall a b. (a -> b) -> a -> b
$ [Char]
"The ground evaluator does not support bound variables."
            VarKind
LatchVarKind      -> GroundValue tp -> IO (GroundValue tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundValue tp -> IO (GroundValue tp))
-> GroundValue tp -> IO (GroundValue tp)
forall a b. (a -> b) -> a -> b
$! BaseTypeRepr tp -> GroundValue tp
forall (tp :: BaseType). BaseTypeRepr tp -> GroundValue tp
defaultValueForType (ExprBoundVar t tp -> BaseTypeRepr tp
forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar t tp
v)
            VarKind
UninterpVarKind   -> GroundValue tp -> IO (GroundValue tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundValue tp -> IO (GroundValue tp))
-> GroundValue tp -> IO (GroundValue tp)
forall a b. (a -> b) -> a -> b
$! BaseTypeRepr tp -> GroundValue tp
forall (tp :: BaseType). BaseTypeRepr tp -> GroundValue tp
defaultValueForType (ExprBoundVar t tp -> BaseTypeRepr tp
forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar t tp
v)
      | Bool
otherwise -> [Char] -> IO (GroundValue tp)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO (GroundValue tp)) -> [Char] -> IO (GroundValue tp)
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
"evalGroundExpr: could not evaluate expression:", Expr t tp -> [Char]
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 (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
_) = Integer -> MaybeT IO Integer
forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
Coefficient sr
c
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (SemiRingLiteral SemiRingRepr sr
SR.SemiRingRealRepr Coefficient sr
c ProgramLoc
_) = Rational -> MaybeT IO Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
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
_) = BV w -> MaybeT IO (BV w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV w
Coefficient sr
c
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (StringExpr StringLiteral si
x ProgramLoc
_)  = StringLiteral si -> MaybeT IO (StringLiteral si)
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
_)    = Bool -> MaybeT IO Bool
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
_) = BigFloat -> MaybeT IO BigFloat
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 (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> NonceApp t (Expr t) tp -> MaybeT IO (GroundValue tp)
forall (m :: Type -> Type) t (tp :: BaseType).
MonadFail 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 (NonceAppExpr t tp -> NonceApp t (Expr t) tp
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 (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> App (Expr t) tp -> MaybeT IO (GroundValue tp)
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 (AppExpr t tp -> App (Expr t) tp
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
_)  = MaybeT IO (GroundValue 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 :: MonadFail m
                   => (forall u . 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))
-> 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 -> Expr t tp -> MaybeT m (GroundValue tp)
forall (u :: BaseType). Expr t u -> MaybeT m (GroundValue u)
fn Expr t tp
t
    Forall{} ->  m Bool -> MaybeT m Bool
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> MaybeT m Bool) -> m Bool -> MaybeT m Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> m Bool
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> m Bool) -> [Char] -> m Bool
forall a b. (a -> b) -> a -> b
$ [Char]
"The ground evaluator does not support quantifiers."
    Exists{} ->  m Bool -> MaybeT m Bool
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> MaybeT m Bool) -> m Bool -> MaybeT m Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> m Bool
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> m Bool) -> [Char] -> m Bool
forall a b. (a -> b) -> a -> b
$ [Char]
"The ground evaluator does not support quantifiers."
    MapOverArrays{} ->  m (GroundArray (idx '::> itp) r)
-> MaybeT m (GroundArray (idx '::> itp) r)
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (GroundArray (idx '::> itp) r)
 -> MaybeT m (GroundArray (idx '::> itp) r))
-> m (GroundArray (idx '::> itp) r)
-> MaybeT m (GroundArray (idx '::> itp) r)
forall a b. (a -> b) -> a -> b
$ [Char] -> m (GroundArray (idx '::> itp) r)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> m (GroundArray (idx '::> itp) r))
-> [Char] -> m (GroundArray (idx '::> itp) r)
forall a b. (a -> b) -> a -> b
$ [Char]
"The ground evaluator does not support mapping arrays from arbitrary functions."
    ArrayFromFn{} ->  m (GroundArray (idx '::> itp) ret)
-> MaybeT m (GroundArray (idx '::> itp) ret)
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (GroundArray (idx '::> itp) ret)
 -> MaybeT m (GroundArray (idx '::> itp) ret))
-> m (GroundArray (idx '::> itp) ret)
-> MaybeT m (GroundArray (idx '::> itp) ret)
forall a b. (a -> b) -> a -> b
$ [Char] -> m (GroundArray (idx '::> itp) ret)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> m (GroundArray (idx '::> itp) ret))
-> [Char] -> m (GroundArray (idx '::> itp) ret)
forall a b. (a -> b) -> a -> b
$ [Char]
"The ground evaluator does not support arrays from arbitrary functions."
    ArrayTrueOnEntries{} ->  m Bool -> MaybeT m Bool
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> MaybeT m Bool) -> m Bool -> MaybeT m Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> m Bool
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> m Bool) -> [Char] -> m Bool
forall a b. (a -> b) -> a -> b
$ [Char]
"The ground evaluator does not support arrayTrueOnEntries."
    FnApp{} -> m (GroundValue tp) -> MaybeT m (GroundValue tp)
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (GroundValue tp) -> MaybeT m (GroundValue tp))
-> m (GroundValue tp) -> MaybeT m (GroundValue tp)
forall a b. (a -> b) -> a -> b
$ [Char] -> m (GroundValue tp)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> m (GroundValue tp)) -> [Char] -> m (GroundValue tp)
forall a b. (a -> b) -> a -> b
$ [Char]
"The ground evaluator does not support function applications."

{-# INLINABLE evalGroundApp #-}

forallIndex :: Ctx.Size (ctx :: Ctx.Ctx k) -> (forall tp . Ctx.Index ctx tp -> Bool) -> Bool
forallIndex :: Size ctx -> (forall (tp :: k). Index ctx tp -> Bool) -> Bool
forallIndex Size ctx
sz forall (tp :: k). Index ctx tp -> Bool
f = Size ctx
-> (forall (tp :: k). Bool -> Index ctx tp -> Bool) -> Bool -> Bool
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 -> Index ctx tp -> Bool
forall (tp :: k). Index ctx tp -> Bool
f Index ctx tp
j Bool -> Bool -> Bool
&& Bool
b) Bool
True


newtype MAnd x = MAnd { MAnd x -> Maybe Bool
unMAnd :: Maybe Bool }
instance Functor MAnd where
  fmap :: (a -> b) -> MAnd a -> MAnd b
fmap a -> b
_f (MAnd Maybe Bool
x) = Maybe Bool -> MAnd b
forall k (x :: k). Maybe Bool -> MAnd x
MAnd Maybe Bool
x
instance Applicative MAnd where
  pure :: a -> MAnd a
pure a
_ = Maybe Bool -> MAnd a
forall k (x :: k). Maybe Bool -> MAnd x
MAnd (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)
  MAnd (Just Bool
a) <*> :: MAnd (a -> b) -> MAnd a -> MAnd b
<*> MAnd (Just Bool
b) = Maybe Bool -> MAnd b
forall k (x :: k). Maybe Bool -> MAnd x
MAnd (Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$! (Bool
a Bool -> Bool -> Bool
&& Bool
b))
  MAnd (a -> b)
_ <*> MAnd a
_ = Maybe Bool -> MAnd b
forall k (x :: k). Maybe Bool -> MAnd x
MAnd Maybe Bool
forall a. Maybe a
Nothing

mand :: Bool -> MAnd z
mand :: Bool -> MAnd z
mand = Maybe Bool -> MAnd z
forall k (x :: k). Maybe Bool -> MAnd x
MAnd (Maybe Bool -> MAnd z) -> (Bool -> Maybe Bool) -> Bool -> MAnd z
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Maybe Bool
forall a. a -> Maybe a
Just

coerceMAnd :: MAnd a -> MAnd b
coerceMAnd :: MAnd a -> MAnd b
coerceMAnd (MAnd Maybe Bool
x) = Maybe Bool -> MAnd b
forall k (x :: k). Maybe Bool -> MAnd x
MAnd Maybe Bool
x

groundEq :: BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
groundEq :: BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
groundEq BaseTypeRepr tp
bt0 GroundValue tp
x0 GroundValue tp
y0 = MAnd Any -> Maybe Bool
forall k (x :: k). MAnd x -> Maybe Bool
unMAnd (BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> MAnd Any
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 :: 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     -> Bool -> MAnd z
forall k (z :: k). Bool -> MAnd z
mand (Bool -> MAnd z) -> Bool -> MAnd z
forall a b. (a -> b) -> a -> b
$ Bool
GroundValue tp
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
GroundValue tp
y
      BaseTypeRepr tp
BaseRealRepr     -> Bool -> MAnd z
forall k (z :: k). Bool -> MAnd z
mand (Bool -> MAnd z) -> Bool -> MAnd z
forall a b. (a -> b) -> a -> b
$ Rational
GroundValue tp
x Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
GroundValue tp
y
      BaseTypeRepr tp
BaseIntegerRepr  -> Bool -> MAnd z
forall k (z :: k). Bool -> MAnd z
mand (Bool -> MAnd z) -> Bool -> MAnd z
forall a b. (a -> b) -> a -> b
$ Integer
GroundValue tp
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
GroundValue tp
y
      BaseBVRepr NatRepr w
_     -> Bool -> MAnd z
forall k (z :: k). Bool -> MAnd z
mand (Bool -> MAnd z) -> Bool -> MAnd z
forall a b. (a -> b) -> a -> b
$ BV w
GroundValue tp
x BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== BV w
GroundValue tp
y
      -- NB, don't use (==) for BigFloat, which is the wrong equality
      BaseFloatRepr FloatPrecisionRepr fpp
_  -> Bool -> MAnd z
forall k (z :: k). Bool -> MAnd z
mand (Bool -> MAnd z) -> Bool -> MAnd z
forall a b. (a -> b) -> a -> b
$ BigFloat -> BigFloat -> Ordering
BF.bfCompare BigFloat
GroundValue tp
x BigFloat
GroundValue tp
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ
      BaseStringRepr StringInfoRepr si
_ -> Bool -> MAnd z
forall k (z :: k). Bool -> MAnd z
mand (Bool -> MAnd z) -> Bool -> MAnd z
forall a b. (a -> b) -> a -> b
$ StringLiteral si
GroundValue tp
x StringLiteral si -> StringLiteral si -> Bool
forall a. Eq a => a -> a -> Bool
== StringLiteral si
GroundValue tp
y
      BaseTypeRepr tp
BaseComplexRepr  -> Bool -> MAnd z
forall k (z :: k). Bool -> MAnd z
mand (Bool -> MAnd z) -> Bool -> MAnd z
forall a b. (a -> b) -> a -> b
$ Complex Rational
GroundValue tp
x Complex Rational -> Complex Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Complex Rational
GroundValue tp
y
      BaseStructRepr Assignment BaseTypeRepr ctx
flds ->
        MAnd (Assignment Any ctx) -> MAnd z
forall k k (a :: k) (b :: k). MAnd a -> MAnd b
coerceMAnd ((forall (tp :: BaseType).
 Index ctx tp -> BaseTypeRepr tp -> MAnd (Any tp))
-> Assignment BaseTypeRepr ctx -> MAnd (Assignment Any ctx)
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 -> BaseTypeRepr tp
-> GroundValue tp -> GroundValue tp -> MAnd (Any tp)
forall k (tp :: BaseType) (z :: k).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> MAnd z
f BaseTypeRepr tp
tp (GroundValueWrapper tp -> GroundValue tp
forall (tp :: BaseType). GroundValueWrapper tp -> GroundValue tp
unGVW (Assignment GroundValueWrapper ctx
GroundValue tp
x Assignment GroundValueWrapper ctx
-> Index ctx tp -> GroundValueWrapper tp
forall k (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i)) (GroundValueWrapper tp -> GroundValue tp
forall (tp :: BaseType). GroundValueWrapper tp -> GroundValue tp
unGVW (Assignment GroundValueWrapper ctx
GroundValue tp
y Assignment GroundValueWrapper ctx
-> Index ctx tp -> GroundValueWrapper tp
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{} -> Maybe Bool -> MAnd z
forall k (x :: k). Maybe Bool -> MAnd x
MAnd Maybe Bool
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 (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 tp
bt Expr t tp
x Expr t tp
y ->
      do GroundValue tp
x' <- Expr t tp -> MaybeT IO (GroundValue tp)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp
x
         GroundValue tp
y' <- Expr t tp -> MaybeT IO (GroundValue tp)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp
y
         IO (Maybe Bool) -> MaybeT IO Bool
forall (m :: Type -> Type) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe Bool -> IO (Maybe Bool)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
groundEq BaseTypeRepr tp
bt GroundValue tp
x' GroundValue tp
y'))

    BaseIte BaseTypeRepr tp
_ Integer
_ Expr t BaseBoolType
x Expr t tp
y Expr t tp
z -> do
      Bool
xv <- Expr t BaseBoolType -> MaybeT IO (GroundValue BaseBoolType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseBoolType
x
      if Bool
xv then Expr t tp -> MaybeT IO (GroundValue tp)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp
y else Expr t tp -> MaybeT IO (GroundValue tp)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp
z

    NotPred Expr t BaseBoolType
x -> Bool -> Bool
not (Bool -> Bool) -> MaybeT IO Bool -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseBoolType -> MaybeT IO (GroundValue BaseBoolType)
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 Bool
pol (Expr t BaseBoolType
x,Polarity
Positive) = Expr t BaseBoolType -> MaybeT IO (GroundValue BaseBoolType)
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 (Bool -> Bool) -> MaybeT IO Bool -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseBoolType -> MaybeT IO (GroundValue BaseBoolType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseBoolType
x
      in
      case BoolMap (Expr t) -> BoolMapView (Expr t)
forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
BM.viewBoolMap BoolMap (Expr t)
xs of
        BoolMapView (Expr t)
BM.BoolMapUnit -> Bool -> MaybeT IO Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
True
        BoolMapView (Expr t)
BM.BoolMapDualUnit -> Bool -> MaybeT IO Bool
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) ->
          (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Bool -> Bool -> Bool
(&&) (Bool -> [Bool] -> Bool)
-> MaybeT IO Bool -> MaybeT IO ([Bool] -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t BaseBoolType, Polarity) -> MaybeT IO Bool
pol (Expr t BaseBoolType, Polarity)
t MaybeT IO ([Bool] -> Bool) -> MaybeT IO [Bool] -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ((Expr t BaseBoolType, Polarity) -> MaybeT IO Bool)
-> [(Expr t BaseBoolType, Polarity)] -> MaybeT IO [Bool]
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 Bool
pol [(Expr t BaseBoolType, Polarity)]
ts

    RealIsInteger Expr t BaseRealType
x -> (\Rational
xv -> Rational -> Integer
forall a. Ratio a -> a
denominator Rational
xv Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) (Rational -> Bool) -> MaybeT IO Rational -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
    BVTestBit Natural
i Expr t (BaseBVType w)
x ->
        Natural -> BV w -> Bool
forall (w :: Nat). Natural -> BV w -> Bool
BV.testBit' Natural
i (BV w -> Bool) -> MaybeT IO (BV w) -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 -> NatRepr w -> BV w -> BV w -> Bool
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
BV.slt NatRepr w
w (BV w -> BV w -> Bool)
-> MaybeT IO (BV w) -> MaybeT IO (BV w -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (BV w -> Bool) -> MaybeT IO (BV w) -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
y
      where w :: NatRepr w
w = Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x
    BVUlt Expr t (BaseBVType w)
x Expr t (BaseBVType w)
y -> BV w -> BV w -> Bool
forall (w :: Nat). BV w -> BV w -> Bool
BV.ult (BV w -> BV w -> Bool)
-> MaybeT IO (BV w) -> MaybeT IO (BV w -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (BV w -> Bool) -> MaybeT IO (BV w) -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 -> Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
g (Integer -> Integer -> Integer)
-> MaybeT IO Integer -> MaybeT IO (Integer -> Integer)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseIntegerType
x MaybeT IO (Integer -> Integer)
-> MaybeT IO Integer -> MaybeT IO Integer
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0    = a
0
            | a
v a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>  a
0    = a
u a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
v
            | Bool
otherwise = a -> a
forall a. Num a => a -> a
negate (a
u a -> a -> a
forall a. Integral a => a -> a -> a
`div` a -> a
forall a. Num a => a -> a
negate a
v)

    IntMod Expr t BaseIntegerType
x Expr t BaseIntegerType
y -> Integer -> Integer -> Integer
forall p. Num p => Integer -> Integer -> p
intModu (Integer -> Integer -> Integer)
-> MaybeT IO Integer -> MaybeT IO (Integer -> Integer)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseIntegerType
x MaybeT IO (Integer -> Integer)
-> MaybeT IO Integer -> MaybeT IO Integer
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseIntegerType
y
      where intModu :: Integer -> Integer -> p
intModu Integer
_ Integer
0 = p
0
            intModu Integer
i Integer
v = Integer -> p
forall a. Num a => Integer -> a
fromInteger (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer -> Integer
forall a. Num a => a -> a
abs Integer
v)

    IntAbs Expr t BaseIntegerType
x -> Integer -> Integer
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
abs (Integer -> Integer) -> MaybeT IO Integer -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
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 (Integer -> Bool) -> MaybeT IO Integer -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseIntegerType
x
      where
      g :: Integer -> Bool
g Integer
u | Natural
k Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0    = Integer
u Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
          | Bool
otherwise = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
u (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
k) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0

    SemiRingLe OrderedSemiRingRepr sr
SR.OrderedSemiRingRealRepr    Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y -> Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
(<=) (Rational -> Rational -> Bool)
-> MaybeT IO Rational -> MaybeT IO (Rational -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
Expr t (SemiRingBase sr)
x MaybeT IO (Rational -> Bool)
-> MaybeT IO Rational -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
Expr t (SemiRingBase sr)
y
    SemiRingLe OrderedSemiRingRepr sr
SR.OrderedSemiRingIntegerRepr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y -> Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<=) (Integer -> Integer -> Bool)
-> MaybeT IO Integer -> MaybeT IO (Integer -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseIntegerType
Expr t (SemiRingBase sr)
x MaybeT IO (Integer -> Bool) -> MaybeT IO Integer -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseIntegerType
Expr t (SemiRingBase sr)
y

    SemiRingSum WeightedSum (Expr t) sr
s ->
      case WeightedSum (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum (Expr t) sr
s of
        SemiRingRepr sr
SR.SemiRingIntegerRepr -> (Integer -> Integer -> MaybeT IO Integer)
-> (Coefficient sr
    -> Expr t (SemiRingBase sr) -> MaybeT IO Integer)
-> (Coefficient sr -> MaybeT IO Integer)
-> WeightedSum (Expr t) sr
-> MaybeT IO Integer
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 (\Integer
x Integer
y -> Integer -> MaybeT IO Integer
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
y)) Integer -> Expr t BaseIntegerType -> MaybeT IO Integer
Coefficient sr -> Expr t (SemiRingBase sr) -> MaybeT IO Integer
smul Coefficient sr -> MaybeT IO Integer
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure WeightedSum (Expr t) sr
s
           where smul :: Integer -> Expr t BaseIntegerType -> MaybeT IO Integer
smul Integer
sm Expr t BaseIntegerType
e = (Integer
sm Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*) (Integer -> Integer) -> MaybeT IO Integer -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseIntegerType
e
        SemiRingRepr sr
SR.SemiRingRealRepr -> (Rational -> Rational -> MaybeT IO Rational)
-> (Coefficient sr
    -> Expr t (SemiRingBase sr) -> MaybeT IO Rational)
-> (Coefficient sr -> MaybeT IO Rational)
-> WeightedSum (Expr t) sr
-> MaybeT IO Rational
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 (\Rational
x Rational
y -> Rational -> MaybeT IO Rational
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Rational
xRational -> Rational -> Rational
forall a. Num a => a -> a -> a
+Rational
y)) Rational -> Expr t BaseRealType -> MaybeT IO Rational
Coefficient sr -> Expr t (SemiRingBase sr) -> MaybeT IO Rational
smul Coefficient sr -> MaybeT IO Rational
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure WeightedSum (Expr t) sr
s
           where smul :: Rational -> Expr t BaseRealType -> MaybeT IO Rational
smul Rational
sm Expr t BaseRealType
e = (Rational
sm Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
*) (Rational -> Rational) -> MaybeT IO Rational -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
e
        SR.SemiRingBVRepr BVFlavorRepr fv
SR.BVArithRepr NatRepr w
w -> (BV w -> BV w -> MaybeT IO (BV w))
-> (Coefficient sr -> Expr t (SemiRingBase sr) -> MaybeT IO (BV w))
-> (Coefficient sr -> MaybeT IO (BV w))
-> WeightedSum (Expr t) sr
-> MaybeT IO (BV 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)
Coefficient sr -> Expr t (SemiRingBase sr) -> MaybeT IO (BV w)
smul Coefficient sr -> MaybeT IO (BV w)
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 = NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
w BV w
sm (BV w -> BV w) -> MaybeT IO (BV w) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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  = BV w -> MaybeT IO (BV w)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). 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 -> (BV w -> BV w -> MaybeT IO (BV w))
-> (Coefficient sr -> Expr t (SemiRingBase sr) -> MaybeT IO (BV w))
-> (Coefficient sr -> MaybeT IO (BV w))
-> WeightedSum (Expr t) sr
-> MaybeT IO (BV 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)
forall (f :: Type -> Type) (w :: Nat).
Applicative f =>
BV w -> BV w -> f (BV w)
sadd BV w -> Expr t (BaseBVType w) -> MaybeT IO (BV w)
Coefficient sr -> Expr t (SemiRingBase sr) -> MaybeT IO (BV w)
smul Coefficient sr -> MaybeT IO (BV w)
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 = BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
BV.and BV w
sm (BV w -> BV w) -> MaybeT IO (BV w) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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  = BV w -> f (BV w)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
BV.xor BV w
x BV w
y)

    SemiRingProd SemiRingProduct (Expr t) sr
pd ->
      case SemiRingProduct (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct (Expr t) sr
pd of
        SemiRingRepr sr
SR.SemiRingIntegerRepr -> Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe Integer
1 (Maybe Integer -> Integer)
-> MaybeT IO (Maybe Integer) -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> Integer -> MaybeT IO Integer)
-> (Expr t (SemiRingBase sr) -> MaybeT IO Integer)
-> SemiRingProduct (Expr t) sr
-> MaybeT IO (Maybe Integer)
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 -> Integer -> MaybeT IO Integer
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
y)) Expr t (SemiRingBase sr) -> MaybeT IO Integer
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f SemiRingProduct (Expr t) sr
pd
        SemiRingRepr sr
SR.SemiRingRealRepr    -> Rational -> Maybe Rational -> Rational
forall a. a -> Maybe a -> a
fromMaybe Rational
1 (Maybe Rational -> Rational)
-> MaybeT IO (Maybe Rational) -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Rational -> Rational -> MaybeT IO Rational)
-> (Expr t (SemiRingBase sr) -> MaybeT IO Rational)
-> SemiRingProduct (Expr t) sr
-> MaybeT IO (Maybe Rational)
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 -> Rational -> MaybeT IO Rational
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Rational
xRational -> Rational -> Rational
forall a. Num a => a -> a -> a
*Rational
y)) Expr t (SemiRingBase sr) -> MaybeT IO Rational
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 ->
          BV w -> Maybe (BV w) -> BV w
forall a. a -> Maybe a -> a
fromMaybe (NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr w
w) (Maybe (BV w) -> BV w)
-> MaybeT IO (Maybe (BV w)) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BV w -> BV w -> MaybeT IO (BV w))
-> (Expr t (SemiRingBase sr) -> MaybeT IO (BV w))
-> SemiRingProduct (Expr t) sr
-> MaybeT IO (Maybe (BV w))
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 -> BV w -> MaybeT IO (BV w)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
w BV w
x BV w
y)) Expr t (SemiRingBase sr) -> MaybeT IO (BV w)
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 ->
          BV w -> Maybe (BV w) -> BV w
forall a. a -> Maybe a -> a
fromMaybe (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w) (Maybe (BV w) -> BV w)
-> MaybeT IO (Maybe (BV w)) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BV w -> BV w -> MaybeT IO (BV w))
-> (Expr t (SemiRingBase sr) -> MaybeT IO (BV w))
-> SemiRingProduct (Expr t) sr
-> MaybeT IO (Maybe (BV w))
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 -> BV w -> MaybeT IO (BV w)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
BV.and BV w
x BV w
y)) Expr t (SemiRingBase sr) -> MaybeT IO (BV w)
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 <- Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
      Rational
yv <- Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
y
      Rational -> MaybeT IO Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Rational -> MaybeT IO Rational) -> Rational -> MaybeT IO Rational
forall a b. (a -> b) -> a -> b
$!
        if Rational
yv Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0 then Rational
0 else Rational
xv Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
yv
    RealSqrt Expr t BaseRealType
x -> do
      Rational
xv <- Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
      Bool -> MaybeT IO () -> MaybeT IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Rational
xv Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0) (MaybeT IO () -> MaybeT IO ()) -> MaybeT IO () -> MaybeT IO ()
forall a b. (a -> b) -> a -> b
$ do
        IO () -> MaybeT IO ()
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> MaybeT IO ()) -> IO () -> MaybeT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Model returned sqrt of negative number."
      Rational -> MaybeT IO Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Rational -> MaybeT IO Rational) -> Rational -> MaybeT IO Rational
forall a b. (a -> b) -> a -> b
$ Double -> Rational
fromDouble (Double -> Double
forall a. Floating a => a -> a
sqrt (Rational -> Double
toDouble Rational
xv))

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

    App (Expr t) tp
Pi -> Rational -> MaybeT IO Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Rational -> MaybeT IO Rational) -> Rational -> MaybeT IO Rational
forall a b. (a -> b) -> a -> b
$ Double -> Rational
fromDouble Double
forall a. Floating a => a
pi
    RealSin Expr t BaseRealType
x -> Double -> Rational
fromDouble (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
sin (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
toDouble (Rational -> Rational) -> MaybeT IO Rational -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
    RealCos Expr t BaseRealType
x -> Double -> Rational
fromDouble (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
cos (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
toDouble (Rational -> Rational) -> MaybeT IO Rational -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
    RealATan2 Expr t BaseRealType
x Expr t BaseRealType
y -> do
      Rational
xv <- Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
      Rational
yv <- Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
y
      Rational -> MaybeT IO Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Rational -> MaybeT IO Rational) -> Rational -> MaybeT IO Rational
forall a b. (a -> b) -> a -> b
$ Double -> Rational
fromDouble (Double -> Double -> Double
forall a. RealFloat a => a -> a -> a
atan2 (Rational -> Double
toDouble Rational
xv) (Rational -> Double
toDouble Rational
yv))
    RealSinh Expr t BaseRealType
x -> Double -> Rational
fromDouble (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
sinh (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
toDouble (Rational -> Rational) -> MaybeT IO Rational -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
    RealCosh Expr t BaseRealType
x -> Double -> Rational
fromDouble (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
cosh (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
toDouble (Rational -> Rational) -> MaybeT IO Rational -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x

    RealExp Expr t BaseRealType
x -> Double -> Rational
fromDouble (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
exp (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
toDouble (Rational -> Rational) -> MaybeT IO Rational -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
    RealLog Expr t BaseRealType
x -> Double -> Rational
fromDouble (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
log (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
toDouble (Rational -> Rational) -> MaybeT IO Rational -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x

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

    BVOrBits NatRepr w
w BVOrSet (Expr t) w
bs -> (BV w -> BV w -> BV w) -> BV w -> [BV w] -> BV w
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
BV.or (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w) ([BV w] -> BV w) -> MaybeT IO [BV w] -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t (BaseBVType w) -> MaybeT IO (BV w))
-> [Expr t (BaseBVType w)] -> MaybeT IO [BV w]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr t (BaseBVType w) -> MaybeT IO (BV w)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f (BVOrSet (Expr t) w -> [Expr t (BaseBVType w)]
forall (e :: BaseType -> Type) (w :: Nat).
BVOrSet e w -> [e (BaseBVType w)]
bvOrToList BVOrSet (Expr t) w
bs)
    BVUnaryTerm UnaryBV (Expr t BaseBoolType) n
u ->
      NatRepr n -> Integer -> BV n
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV (UnaryBV (Expr t BaseBoolType) n -> NatRepr n
forall p (n :: Nat). UnaryBV p n -> NatRepr n
UnaryBV.width UnaryBV (Expr t BaseBoolType) n
u) (Integer -> BV n) -> MaybeT IO Integer -> MaybeT IO (BV n)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t BaseBoolType -> MaybeT IO Bool)
-> UnaryBV (Expr t BaseBoolType) n -> MaybeT IO Integer
forall (m :: Type -> Type) p (n :: Nat).
Monad m =>
(p -> m Bool) -> UnaryBV p n -> m Integer
UnaryBV.evaluate Expr t BaseBoolType -> MaybeT IO Bool
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 -> NatRepr u -> NatRepr v -> BV u -> BV v -> BV (u + v)
forall (w :: Nat) (w' :: Nat).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
BV.concat (Expr t (BaseBVType u) -> NatRepr u
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType u)
x) (Expr t (BaseBVType v) -> NatRepr v
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType v)
y) (BV u -> BV v -> BV (u + v))
-> MaybeT IO (BV u) -> MaybeT IO (BV v -> BV (u + v))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType u) -> MaybeT IO (GroundValue (BaseBVType u))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType u)
x MaybeT IO (BV v -> BV (u + v))
-> MaybeT IO (BV v) -> MaybeT IO (BV (u + v))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseBVType v) -> MaybeT IO (GroundValue (BaseBVType v))
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 -> NatRepr idx -> NatRepr n -> BV w -> BV n
forall (ix :: Nat) (w' :: Nat) (w :: Nat).
((ix + w') <= w) =>
NatRepr ix -> NatRepr w' -> BV w -> BV w'
BV.select NatRepr idx
idx NatRepr n
n (BV w -> BV n) -> MaybeT IO (BV w) -> MaybeT IO (BV n)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 (BV w -> BV w -> BV w)
-> MaybeT IO (BV w) -> MaybeT IO (BV w -> BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (BV w -> BV w) -> MaybeT IO (BV w) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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) = NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w
            myDiv BV w
u BV w
v = BV w -> BV w -> BV w
forall (w :: Nat). 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 -> BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
myRem (BV w -> BV w -> BV w)
-> MaybeT IO (BV w) -> MaybeT IO (BV w -> BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (BV w -> BV w) -> MaybeT IO (BV w) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 = BV w -> BV w -> BV w
forall (w :: Nat). 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 (BV w -> BV w -> BV w)
-> MaybeT IO (BV w) -> MaybeT IO (BV w -> BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (BV w -> BV w) -> MaybeT IO (BV w) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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) = NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w
            myDiv BV w
u BV w
v = NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). (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 (BV w -> BV w -> BV w)
-> MaybeT IO (BV w) -> MaybeT IO (BV w -> BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (BV w -> BV w) -> MaybeT IO (BV w) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 = NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). (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  -> NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
BV.shl NatRepr w
w  (BV w -> Natural -> BV w)
-> MaybeT IO (BV w) -> MaybeT IO (Natural -> BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (Natural -> BV w)
-> MaybeT IO Natural -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Nat). BV w -> Natural
BV.asNatural (BV w -> Natural) -> MaybeT IO (BV w) -> MaybeT IO Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 -> NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
BV.lshr NatRepr w
w (BV w -> Natural -> BV w)
-> MaybeT IO (BV w) -> MaybeT IO (Natural -> BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (Natural -> BV w)
-> MaybeT IO Natural -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Nat). BV w -> Natural
BV.asNatural (BV w -> Natural) -> MaybeT IO (BV w) -> MaybeT IO Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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  -> NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Natural -> BV w
BV.ashr NatRepr w
w (BV w -> Natural -> BV w)
-> MaybeT IO (BV w) -> MaybeT IO (Natural -> BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (Natural -> BV w)
-> MaybeT IO Natural -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Nat). BV w -> Natural
BV.asNatural (BV w -> Natural) -> MaybeT IO (BV w) -> MaybeT IO Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 -> NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
BV.rotateL NatRepr w
w (BV w -> Natural -> BV w)
-> MaybeT IO (BV w) -> MaybeT IO (Natural -> BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (Natural -> BV w)
-> MaybeT IO Natural -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Nat). BV w -> Natural
BV.asNatural (BV w -> Natural) -> MaybeT IO (BV w) -> MaybeT IO Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 -> NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
BV.rotateR NatRepr w
w (BV w -> Natural -> BV w)
-> MaybeT IO (BV w) -> MaybeT IO (Natural -> BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x MaybeT IO (Natural -> BV w)
-> MaybeT IO Natural -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Nat). BV w -> Natural
BV.asNatural (BV w -> Natural) -> MaybeT IO (BV w) -> MaybeT IO Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 -> NatRepr r -> BV w -> BV r
forall (w :: Nat) (w' :: Nat).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext NatRepr r
w (BV w -> BV r) -> MaybeT IO (BV w) -> MaybeT IO (BV r)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 NatRepr r -> Maybe (LeqProof 1 r)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr r
w of
        Just LeqProof 1 r
LeqProof -> NatRepr w -> NatRepr r -> BV w -> BV r
forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext (Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x) NatRepr r
w (BV w -> BV r) -> MaybeT IO (BV w) -> MaybeT IO (BV r)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
        Maybe (LeqProof 1 r)
Nothing -> [Char] -> MaybeT IO (BV r)
forall a. HasCallStack => [Char] -> a
error [Char]
"BVSext given bad width"

    BVFill NatRepr w
w Expr t BaseBoolType
p ->
      do Bool
b <- Expr t BaseBoolType -> MaybeT IO (GroundValue BaseBoolType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseBoolType
p
         BV w -> MaybeT IO (BV w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BV w -> MaybeT IO (BV w)) -> BV w -> MaybeT IO (BV w)
forall a b. (a -> b) -> a -> b
$! if Bool
b then NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w else NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w

    BVPopcount NatRepr w
_w Expr t (BaseBVType w)
x ->
      BV w -> BV w
forall (w :: Nat). BV w -> BV w
BV.popCount (BV w -> BV w) -> MaybeT IO (BV w) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 ->
      NatRepr w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w
BV.clz NatRepr w
w (BV w -> BV w) -> MaybeT IO (BV w) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 ->
      NatRepr w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w
BV.ctz NatRepr w
w (BV w -> BV w) -> MaybeT IO (BV w) -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 (BigFloat -> BigFloat) -> MaybeT IO BigFloat -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 (BigFloat -> BigFloat) -> MaybeT IO BigFloat -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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  -> (BigFloat, Status) -> BigFloat
forall a. HasCallStack => (a, Status) -> a
bfStatus ((BigFloat, Status) -> BigFloat)
-> (BigFloat -> (BigFloat, Status)) -> BigFloat -> BigFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BFOpts -> BigFloat -> (BigFloat, Status)
BF.bfSqrt (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (BigFloat -> BigFloat) -> MaybeT IO BigFloat -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 -> FloatPrecisionRepr fpp -> RoundingMode -> BigFloat -> BigFloat
forall (fpp :: FloatPrecision).
HasCallStack =>
FloatPrecisionRepr fpp -> RoundingMode -> BigFloat -> BigFloat
floatRoundToInt FloatPrecisionRepr fpp
fpp RoundingMode
r (BigFloat -> BigFloat) -> MaybeT IO BigFloat -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 -> (BigFloat, Status) -> BigFloat
forall a. HasCallStack => (a, Status) -> a
bfStatus ((BigFloat, Status) -> BigFloat)
-> MaybeT IO (BigFloat, Status) -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfAdd (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (BigFloat -> BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat -> (BigFloat, Status))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x MaybeT IO (BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat, Status)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 -> (BigFloat, Status) -> BigFloat
forall a. HasCallStack => (a, Status) -> a
bfStatus ((BigFloat, Status) -> BigFloat)
-> MaybeT IO (BigFloat, Status) -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfSub (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (BigFloat -> BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat -> (BigFloat, Status))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x MaybeT IO (BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat, Status)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 -> (BigFloat, Status) -> BigFloat
forall a. HasCallStack => (a, Status) -> a
bfStatus ((BigFloat, Status) -> BigFloat)
-> MaybeT IO (BigFloat, Status) -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfMul (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (BigFloat -> BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat -> (BigFloat, Status))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x MaybeT IO (BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat, Status)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 -> (BigFloat, Status) -> BigFloat
forall a. HasCallStack => (a, Status) -> a
bfStatus ((BigFloat, Status) -> BigFloat)
-> MaybeT IO (BigFloat, Status) -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfDiv (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (BigFloat -> BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat -> (BigFloat, Status))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x MaybeT IO (BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat, Status)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 -> (BigFloat, Status) -> BigFloat
forall a. HasCallStack => (a, Status) -> a
bfStatus ((BigFloat, Status) -> BigFloat)
-> MaybeT IO (BigFloat, Status) -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfRem (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
RNE) (BigFloat -> BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat -> (BigFloat, Status))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x MaybeT IO (BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat, Status)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 -> (BigFloat, Status) -> BigFloat
forall a. HasCallStack => (a, Status) -> a
bfStatus ((BigFloat, Status) -> BigFloat)
-> MaybeT IO (BigFloat, Status) -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfFMA (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat
-> MaybeT IO (BigFloat -> BigFloat -> (BigFloat, Status))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x MaybeT IO (BigFloat -> BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat -> (BigFloat, Status))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
y MaybeT IO (BigFloat -> (BigFloat, Status))
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat, Status)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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      -> BigFloat -> BigFloat -> Bool
forall a. Eq a => a -> a -> Bool
(==) (BigFloat -> BigFloat -> Bool)
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x MaybeT IO (BigFloat -> Bool)
-> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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      -> BigFloat -> BigFloat -> Bool
forall a. Ord a => a -> a -> Bool
(<=) (BigFloat -> BigFloat -> Bool)
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x MaybeT IO (BigFloat -> Bool)
-> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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      -> BigFloat -> BigFloat -> Bool
forall a. Ord a => a -> a -> Bool
(<)  (BigFloat -> BigFloat -> Bool)
-> MaybeT IO BigFloat -> MaybeT IO (BigFloat -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x MaybeT IO (BigFloat -> Bool)
-> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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  (BigFloat -> Bool) -> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 (BigFloat -> Bool) -> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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  (BigFloat -> Bool) -> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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  (BigFloat -> Bool) -> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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  (BigFloat -> Bool) -> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x

    FloatIsNorm Expr t (BaseFloatType fpp)
x ->
      case Expr t (BaseFloatType fpp) -> BaseTypeRepr (BaseFloatType fpp)
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 (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
RNE) (BigFloat -> Bool) -> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x

    FloatIsSubnorm Expr t (BaseFloatType fpp)
x ->
      case Expr t (BaseFloatType fpp) -> BaseTypeRepr (BaseFloatType fpp)
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 (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
RNE) (BigFloat -> Bool) -> MaybeT IO BigFloat -> MaybeT IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 (FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp RoundingMode
RNE) (Integer -> BigFloat)
-> (BV (eb + sb) -> Integer) -> BV (eb + sb) -> BigFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV (eb + sb) -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV (eb + sb) -> BigFloat)
-> MaybeT IO (BV (eb + sb)) -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType (eb + sb))
-> MaybeT IO (GroundValue (BaseBVType (eb + sb)))
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 ->
      NatRepr (eb + sb) -> Integer -> BV (eb + sb)
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV (NatRepr eb -> NatRepr sb -> NatRepr (eb + sb)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr eb
eb NatRepr sb
sb) (Integer -> BV (eb + sb))
-> (BigFloat -> Integer) -> BigFloat -> BV (eb + sb)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BFOpts -> BigFloat -> Integer
BF.bfToBits (FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp RoundingMode
RNE) (BigFloat -> BV (eb + sb))
-> MaybeT IO BigFloat -> MaybeT IO (BV (eb + sb))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType (FloatingPointPrecision eb sb))
-> MaybeT
     IO (GroundValue (BaseFloatType (FloatingPointPrecision eb sb)))
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 -> (BigFloat, Status) -> BigFloat
forall a. HasCallStack => (a, Status) -> a
bfStatus ((BigFloat, Status) -> BigFloat)
-> (BigFloat -> (BigFloat, Status)) -> BigFloat -> BigFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BFOpts -> BigFloat -> (BigFloat, Status)
BF.bfRoundFloat (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (BigFloat -> BigFloat) -> MaybeT IO BigFloat -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp')
-> MaybeT IO (GroundValue (BaseFloatType fpp'))
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 (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (Rational -> BigFloat) -> MaybeT IO Rational -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
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 (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (Integer -> BigFloat) -> (BV w -> Integer) -> BV w -> BigFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV w -> BigFloat) -> MaybeT IO (BV w) -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
r) (Integer -> BigFloat) -> (BV w -> Integer) -> BV w -> BigFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x) (BV w -> BigFloat) -> MaybeT IO (BV w) -> MaybeT IO BigFloat
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x

    FloatToReal Expr t (BaseFloatType fpp)
x -> IO (Maybe Rational) -> MaybeT IO Rational
forall (m :: Type -> Type) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe Rational) -> MaybeT IO Rational)
-> (BigFloat -> IO (Maybe Rational))
-> BigFloat
-> MaybeT IO Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Rational -> IO (Maybe Rational)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe Rational -> IO (Maybe Rational))
-> (BigFloat -> Maybe Rational) -> BigFloat -> IO (Maybe Rational)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BigFloat -> Maybe Rational
floatToRational (BigFloat -> MaybeT IO Rational)
-> MaybeT IO BigFloat -> MaybeT IO Rational
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 (BigFloat -> Maybe Integer)
-> MaybeT IO BigFloat -> MaybeT IO (Maybe Integer)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w -> BV w -> MaybeT IO (BV w)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
i)
           Maybe Integer
_ -> MaybeT IO (BV w)
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 (BigFloat -> Maybe Integer)
-> MaybeT IO BigFloat -> MaybeT IO (Maybe Integer)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType fpp)
-> MaybeT IO (GroundValue (BaseFloatType fpp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseFloatType fpp)
x
         case Maybe Integer
z of
           Just Integer
i | NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr w
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w -> BV w -> MaybeT IO (BV w)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
i)
           Maybe Integer
_ -> MaybeT IO (BV w)
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero

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

    ArrayMap Assignment BaseTypeRepr (i ::> itp)
idx_types BaseTypeRepr tp
_ ArrayUpdateMap (Expr t) (i ::> itp) tp
m Expr t (BaseArrayType (i ::> itp) tp)
def -> do
      Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
m' <- (Expr t tp -> MaybeT IO (GroundValue tp))
-> Map (Assignment IndexLit (i ::> itp)) (Expr t tp)
-> MaybeT
     IO (Map (Assignment IndexLit (i ::> itp)) (GroundValue tp))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr t tp -> MaybeT IO (GroundValue tp)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f (ArrayUpdateMap (Expr t) (i ::> itp) tp
-> Map (Assignment IndexLit (i ::> itp)) (Expr t tp)
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) tp
m)
      GroundArray (i ::> itp) tp
h <- Expr t (BaseArrayType (i ::> itp) tp)
-> MaybeT IO (GroundValue (BaseArrayType (i ::> itp) tp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseArrayType (i ::> itp) tp)
def
      GroundArray (i ::> itp) tp
-> MaybeT IO (GroundArray (i ::> itp) tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundArray (i ::> itp) tp
 -> MaybeT IO (GroundArray (i ::> itp) tp))
-> GroundArray (i ::> itp) tp
-> MaybeT IO (GroundArray (i ::> itp) tp)
forall a b. (a -> b) -> a -> b
$ case GroundArray (i ::> itp) tp
h of
        ArrayMapping Assignment GroundValueWrapper (i ::> itp) -> IO (GroundValue tp)
h' -> (Assignment GroundValueWrapper (i ::> itp) -> IO (GroundValue tp))
-> GroundArray (i ::> itp) tp
forall (idx :: Ctx BaseType) (b :: BaseType).
(Assignment GroundValueWrapper idx -> IO (GroundValue b))
-> GroundArray idx b
ArrayMapping ((Assignment GroundValueWrapper (i ::> itp) -> IO (GroundValue tp))
 -> GroundArray (i ::> itp) tp)
-> (Assignment GroundValueWrapper (i ::> itp)
    -> IO (GroundValue tp))
-> GroundArray (i ::> itp) tp
forall a b. (a -> b) -> a -> b
$ \Assignment GroundValueWrapper (i ::> itp)
idx ->
          case (Assignment IndexLit (i ::> itp)
-> Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
-> Maybe (GroundValue tp)
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
m') (Assignment IndexLit (i ::> itp) -> Maybe (GroundValue tp))
-> Maybe (Assignment IndexLit (i ::> itp))
-> Maybe (GroundValue tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (x :: BaseType).
 BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x))
-> Assignment BaseTypeRepr (i ::> itp)
-> Assignment GroundValueWrapper (i ::> itp)
-> Maybe (Assignment IndexLit (i ::> itp))
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 (x :: BaseType).
BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x)
asIndexLit Assignment BaseTypeRepr (i ::> itp)
idx_types Assignment GroundValueWrapper (i ::> itp)
idx of
            Just GroundValue tp
r ->  GroundValue tp -> IO (GroundValue tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return GroundValue tp
r
            Maybe (GroundValue tp)
Nothing -> Assignment GroundValueWrapper (i ::> itp) -> IO (GroundValue tp)
h' Assignment GroundValueWrapper (i ::> itp)
idx
        ArrayConcrete GroundValue tp
d Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
m'' ->
          -- Map.union is left-biased
          GroundValue tp
-> Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
-> GroundArray (i ::> itp) tp
forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete GroundValue tp
d (Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
-> Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
-> Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
m' Map (Assignment IndexLit (i ::> itp)) (GroundValue tp)
m'')

    ConstantArray Assignment BaseTypeRepr (i ::> tp)
_ BaseTypeRepr b
_ Expr t b
v -> do
      GroundValue b
val <- Expr t b -> MaybeT IO (GroundValue b)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t b
v
      GroundArray (i ::> tp) b -> MaybeT IO (GroundArray (i ::> tp) b)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundArray (i ::> tp) b -> MaybeT IO (GroundArray (i ::> tp) b))
-> GroundArray (i ::> tp) b -> MaybeT IO (GroundArray (i ::> tp) b)
forall a b. (a -> b) -> a -> b
$ GroundValue b
-> Map (Assignment IndexLit (i ::> tp)) (GroundValue b)
-> GroundArray (i ::> tp) b
forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete GroundValue b
val Map (Assignment IndexLit (i ::> tp)) (GroundValue b)
forall k a. Map k a
Map.empty

    SelectArray BaseTypeRepr tp
_ Expr t (BaseArrayType (i ::> tp) tp)
a Assignment (Expr t) (i ::> tp)
i -> do
      GroundArray (i ::> tp) tp
arr <- Expr t (BaseArrayType (i ::> tp) tp)
-> MaybeT IO (GroundValue (BaseArrayType (i ::> tp) tp))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseArrayType (i ::> tp) tp)
a
      let arrIdxTps :: Assignment BaseTypeRepr (i ::> tp)
arrIdxTps = case Expr t (BaseArrayType (i ::> tp) tp)
-> BaseTypeRepr (BaseArrayType (i ::> tp) tp)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType Expr t (BaseArrayType (i ::> tp) tp)
a of
                        BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx BaseTypeRepr xs
_ -> Assignment BaseTypeRepr (i ::> tp)
Assignment BaseTypeRepr (idx ::> tp)
idx
      Assignment GroundValueWrapper (i ::> tp)
idx <- (forall (x :: BaseType).
 Expr t x -> MaybeT IO (GroundValueWrapper x))
-> Assignment (Expr t) (i ::> tp)
-> MaybeT IO (Assignment GroundValueWrapper (i ::> tp))
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 -> GroundValue x -> GroundValueWrapper x
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW (GroundValue x -> GroundValueWrapper x)
-> MaybeT IO (GroundValue x) -> MaybeT IO (GroundValueWrapper x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t x -> MaybeT IO (GroundValue x)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t x
e) Assignment (Expr t) (i ::> tp)
i
      IO (GroundValue tp) -> MaybeT IO (GroundValue tp)
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (GroundValue tp) -> MaybeT IO (GroundValue tp))
-> IO (GroundValue tp) -> MaybeT IO (GroundValue tp)
forall a b. (a -> b) -> a -> b
$ Assignment BaseTypeRepr (i ::> tp)
-> GroundArray (i ::> tp) tp
-> Assignment GroundValueWrapper (i ::> tp)
-> IO (GroundValue tp)
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray Assignment BaseTypeRepr (i ::> tp)
arrIdxTps GroundArray (i ::> tp) tp
arr Assignment GroundValueWrapper (i ::> tp)
idx

    UpdateArray BaseTypeRepr b
_ Assignment BaseTypeRepr (i ::> tp)
idx_tps Expr t (BaseArrayType (i ::> tp) b)
a Assignment (Expr t) (i ::> tp)
i Expr t b
v -> do
      GroundArray (i ::> tp) b
arr <- Expr t (BaseArrayType (i ::> tp) b)
-> MaybeT IO (GroundValue (BaseArrayType (i ::> tp) b))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseArrayType (i ::> tp) b)
a
      Assignment GroundValueWrapper (i ::> tp)
idx <- (forall (x :: BaseType).
 Expr t x -> MaybeT IO (GroundValueWrapper x))
-> Assignment (Expr t) (i ::> tp)
-> MaybeT IO (Assignment GroundValueWrapper (i ::> tp))
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 -> GroundValue x -> GroundValueWrapper x
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW (GroundValue x -> GroundValueWrapper x)
-> MaybeT IO (GroundValue x) -> MaybeT IO (GroundValueWrapper x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t x -> MaybeT IO (GroundValue x)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t x
e) Assignment (Expr t) (i ::> tp)
i
      GroundValue b
v'  <- Expr t b -> MaybeT IO (GroundValue b)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t b
v
      case GroundArray (i ::> tp) b
arr of
        ArrayMapping Assignment GroundValueWrapper (i ::> tp) -> IO (GroundValue b)
arr' -> GroundArray (i ::> tp) b -> MaybeT IO (GroundArray (i ::> tp) b)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundArray (i ::> tp) b -> MaybeT IO (GroundArray (i ::> tp) b))
-> ((Assignment GroundValueWrapper (i ::> tp)
     -> IO (GroundValue b))
    -> GroundArray (i ::> tp) b)
-> (Assignment GroundValueWrapper (i ::> tp) -> IO (GroundValue b))
-> MaybeT IO (GroundArray (i ::> tp) b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assignment GroundValueWrapper (i ::> tp) -> IO (GroundValue b))
-> GroundArray (i ::> tp) b
forall (idx :: Ctx BaseType) (b :: BaseType).
(Assignment GroundValueWrapper idx -> IO (GroundValue b))
-> GroundArray idx b
ArrayMapping ((Assignment GroundValueWrapper (i ::> tp) -> IO (GroundValue b))
 -> MaybeT IO (GroundArray (i ::> tp) b))
-> (Assignment GroundValueWrapper (i ::> tp) -> IO (GroundValue b))
-> MaybeT IO (GroundArray (i ::> tp) b)
forall a b. (a -> b) -> a -> b
$ \Assignment GroundValueWrapper (i ::> tp)
x ->
          if Assignment BaseTypeRepr (i ::> tp)
-> Assignment GroundValueWrapper (i ::> tp)
-> Assignment GroundValueWrapper (i ::> tp)
-> Bool
forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx
-> Assignment GroundValueWrapper ctx
-> Assignment GroundValueWrapper ctx
-> Bool
indicesEq Assignment BaseTypeRepr (i ::> tp)
idx_tps Assignment GroundValueWrapper (i ::> tp)
idx Assignment GroundValueWrapper (i ::> tp)
x then GroundValue b -> IO (GroundValue b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GroundValue b
v' else Assignment GroundValueWrapper (i ::> tp) -> IO (GroundValue b)
arr' Assignment GroundValueWrapper (i ::> tp)
x
        ArrayConcrete GroundValue b
d Map (Assignment IndexLit (i ::> tp)) (GroundValue b)
m -> do
          GroundValue b
val <- Expr t b -> MaybeT IO (GroundValue b)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t b
v
          let idx' :: Assignment IndexLit (i ::> tp)
idx' = Assignment IndexLit (i ::> tp)
-> Maybe (Assignment IndexLit (i ::> tp))
-> Assignment IndexLit (i ::> tp)
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> Assignment IndexLit (i ::> tp)
forall a. HasCallStack => [Char] -> a
error [Char]
"UpdateArray only supported on Nat and BV") (Maybe (Assignment IndexLit (i ::> tp))
 -> Assignment IndexLit (i ::> tp))
-> Maybe (Assignment IndexLit (i ::> tp))
-> Assignment IndexLit (i ::> tp)
forall a b. (a -> b) -> a -> b
$ (forall (x :: BaseType).
 BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x))
-> Assignment BaseTypeRepr (i ::> tp)
-> Assignment GroundValueWrapper (i ::> tp)
-> Maybe (Assignment IndexLit (i ::> tp))
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 (x :: BaseType).
BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x)
asIndexLit Assignment BaseTypeRepr (i ::> tp)
idx_tps Assignment GroundValueWrapper (i ::> tp)
idx
          GroundArray (i ::> tp) b -> MaybeT IO (GroundArray (i ::> tp) b)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundArray (i ::> tp) b -> MaybeT IO (GroundArray (i ::> tp) b))
-> GroundArray (i ::> tp) b -> MaybeT IO (GroundArray (i ::> tp) b)
forall a b. (a -> b) -> a -> b
$ GroundValue b
-> Map (Assignment IndexLit (i ::> tp)) (GroundValue b)
-> GroundArray (i ::> tp) b
forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete GroundValue b
d (Assignment IndexLit (i ::> tp)
-> GroundValue b
-> Map (Assignment IndexLit (i ::> tp)) (GroundValue b)
-> Map (Assignment IndexLit (i ::> tp)) (GroundValue b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Assignment IndexLit (i ::> tp)
idx' GroundValue b
val Map (Assignment IndexLit (i ::> tp)) (GroundValue b)
m)

     where indicesEq :: Ctx.Assignment BaseTypeRepr ctx
                     -> Ctx.Assignment GroundValueWrapper ctx
                     -> Ctx.Assignment GroundValueWrapper ctx
                     -> Bool
           indicesEq :: Assignment BaseTypeRepr ctx
-> Assignment GroundValueWrapper ctx
-> Assignment GroundValueWrapper ctx
-> Bool
indicesEq Assignment BaseTypeRepr ctx
tps Assignment GroundValueWrapper ctx
x Assignment GroundValueWrapper ctx
y =
             Size ctx -> (forall (tp :: BaseType). Index ctx tp -> Bool) -> Bool
forall k (ctx :: Ctx k).
Size ctx -> (forall (tp :: k). Index ctx tp -> Bool) -> Bool
forallIndex (Assignment GroundValueWrapper ctx -> Size ctx
forall k (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment GroundValueWrapper ctx
x) ((forall (tp :: BaseType). Index ctx tp -> Bool) -> Bool)
-> (forall (tp :: BaseType). Index ctx tp -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
j ->
               let GVW GroundValue tp
xj = Assignment GroundValueWrapper ctx
x Assignment GroundValueWrapper ctx
-> Index ctx tp -> GroundValueWrapper tp
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 Assignment GroundValueWrapper ctx
-> Index ctx tp -> GroundValueWrapper tp
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 Assignment BaseTypeRepr ctx -> Index ctx tp -> BaseTypeRepr tp
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 -> Integer
GroundValue tp
xj Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
GroundValue tp
yj
                    BaseBVRepr NatRepr w
_    -> BV w
GroundValue tp
xj BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== BV w
GroundValue tp
yj
                    BaseTypeRepr tp
_ -> [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error ([Char] -> Bool) -> [Char] -> Bool
forall a b. (a -> b) -> a -> b
$ [Char]
"We do not yet support UpdateArray on " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BaseTypeRepr tp -> [Char]
forall a. Show a => a -> [Char]
show BaseTypeRepr tp
tp [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" indices."

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

    IntegerToReal Expr t BaseIntegerType
x -> Integer -> Rational
forall a. Real a => a -> Rational
toRational (Integer -> Rational) -> MaybeT IO Integer -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseIntegerType
x
    BVToInteger Expr t (BaseBVType w)
x  -> BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV w -> Integer) -> MaybeT IO (BV w) -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x
    SBVToInteger Expr t (BaseBVType w)
x -> NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x) (BV w -> Integer) -> MaybeT IO (BV w) -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
x

    RoundReal Expr t BaseRealType
x -> Rational -> Integer
forall a. RealFrac a => a -> Integer
roundAway (Rational -> Integer) -> MaybeT IO Rational -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
    RoundEvenReal Expr t BaseRealType
x -> Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
round (Rational -> Integer) -> MaybeT IO Rational -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
    FloorReal Expr t BaseRealType
x -> Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor (Rational -> Integer) -> MaybeT IO Rational -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x
    CeilReal  Expr t BaseRealType
x -> Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Rational -> Integer) -> MaybeT IO Rational -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x

    RealToInteger Expr t BaseRealType
x -> Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor (Rational -> Integer) -> MaybeT IO Rational -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x

    IntegerToBV Expr t BaseIntegerType
x NatRepr w
w -> NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (Integer -> BV w) -> MaybeT IO Integer -> MaybeT IO (BV w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
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) -> Rational -> Rational -> Complex Rational
forall a. a -> a -> Complex a
(:+) (Rational -> Rational -> Complex Rational)
-> MaybeT IO Rational -> MaybeT IO (Rational -> Complex Rational)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
x MaybeT IO (Rational -> Complex Rational)
-> MaybeT IO Rational -> MaybeT IO (Complex Rational)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t BaseRealType -> MaybeT IO (GroundValue BaseRealType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseRealType
y
    RealPart Expr t BaseComplexType
x -> Complex Rational -> Rational
forall a. Complex a -> a
realPart (Complex Rational -> Rational)
-> MaybeT IO (Complex Rational) -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseComplexType -> MaybeT IO (GroundValue BaseComplexType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseComplexType
x
    ImagPart Expr t BaseComplexType
x -> Complex Rational -> Rational
forall a. Complex a -> a
imagPart (Complex Rational -> Rational)
-> MaybeT IO (Complex Rational) -> MaybeT IO Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t BaseComplexType -> MaybeT IO (GroundValue BaseComplexType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseComplexType
x

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

    StringLength Expr t (BaseStringType si)
x -> StringLiteral si -> Integer
forall (si :: StringInfo). StringLiteral si -> Integer
stringLitLength (StringLiteral si -> Integer)
-> MaybeT IO (StringLiteral si) -> MaybeT IO Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
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 -> StringLiteral si -> StringLiteral si -> Bool
forall (si :: StringInfo).
StringLiteral si -> StringLiteral si -> Bool
stringLitContains (StringLiteral si -> StringLiteral si -> Bool)
-> MaybeT IO (StringLiteral si)
-> MaybeT IO (StringLiteral si -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x MaybeT IO (StringLiteral si -> Bool)
-> MaybeT IO (StringLiteral si) -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
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 -> StringLiteral si -> StringLiteral si -> Bool
forall (si :: StringInfo).
StringLiteral si -> StringLiteral si -> Bool
stringLitIsSuffixOf (StringLiteral si -> StringLiteral si -> Bool)
-> MaybeT IO (StringLiteral si)
-> MaybeT IO (StringLiteral si -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x MaybeT IO (StringLiteral si -> Bool)
-> MaybeT IO (StringLiteral si) -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
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 -> StringLiteral si -> StringLiteral si -> Bool
forall (si :: StringInfo).
StringLiteral si -> StringLiteral si -> Bool
stringLitIsPrefixOf (StringLiteral si -> StringLiteral si -> Bool)
-> MaybeT IO (StringLiteral si)
-> MaybeT IO (StringLiteral si -> Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x MaybeT IO (StringLiteral si -> Bool)
-> MaybeT IO (StringLiteral si) -> MaybeT IO Bool
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
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 -> StringLiteral si -> StringLiteral si -> Integer -> Integer
forall (si :: StringInfo).
StringLiteral si -> StringLiteral si -> Integer -> Integer
stringLitIndexOf (StringLiteral si -> StringLiteral si -> Integer -> Integer)
-> MaybeT IO (StringLiteral si)
-> MaybeT IO (StringLiteral si -> Integer -> Integer)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x MaybeT IO (StringLiteral si -> Integer -> Integer)
-> MaybeT IO (StringLiteral si) -> MaybeT IO (Integer -> Integer)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
y MaybeT IO (Integer -> Integer)
-> MaybeT IO Integer -> MaybeT IO Integer
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
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 -> StringLiteral si -> Integer -> Integer -> StringLiteral si
forall (si :: StringInfo).
StringLiteral si -> Integer -> Integer -> StringLiteral si
stringLitSubstring (StringLiteral si -> Integer -> Integer -> StringLiteral si)
-> MaybeT IO (StringLiteral si)
-> MaybeT IO (Integer -> Integer -> StringLiteral si)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
x MaybeT IO (Integer -> Integer -> StringLiteral si)
-> MaybeT IO Integer -> MaybeT IO (Integer -> StringLiteral si)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t BaseIntegerType
off MaybeT IO (Integer -> StringLiteral si)
-> MaybeT IO Integer -> MaybeT IO (StringLiteral si)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t BaseIntegerType -> MaybeT IO (GroundValue BaseIntegerType)
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) = StringLiteral si -> MaybeT IO (StringLiteral si)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StringLiteral si
x StringLiteral si -> StringLiteral si -> StringLiteral si
forall a. Semigroup a => a -> a -> a
<> StringLiteral si
l)
             g StringLiteral si
x (SSeq.StringSeqTerm Expr t (BaseStringType si)
t)    = (StringLiteral si
x StringLiteral si -> StringLiteral si -> StringLiteral si
forall a. Semigroup a => a -> a -> a
<>) (StringLiteral si -> StringLiteral si)
-> MaybeT IO (StringLiteral si) -> MaybeT IO (StringLiteral si)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseStringType si)
-> MaybeT IO (GroundValue (BaseStringType si))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStringType si)
t
         (StringLiteral si
 -> StringSeqEntry (Expr t) si -> MaybeT IO (StringLiteral si))
-> StringLiteral si
-> [StringSeqEntry (Expr t) si]
-> MaybeT IO (StringLiteral si)
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 (StringInfoRepr si -> StringLiteral si
forall (si :: StringInfo). StringInfoRepr si -> StringLiteral si
stringLitEmpty StringInfoRepr si
si) (StringSeq (Expr t) si -> [StringSeqEntry (Expr t) 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 (x :: BaseType).
 Expr t x -> MaybeT IO (GroundValueWrapper x))
-> Assignment (Expr t) flds
-> MaybeT IO (Assignment GroundValueWrapper flds)
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 -> GroundValue x -> GroundValueWrapper x
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW (GroundValue x -> GroundValueWrapper x)
-> MaybeT IO (GroundValue x) -> MaybeT IO (GroundValueWrapper x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t x -> MaybeT IO (GroundValue x)
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 <- Expr t (BaseStructType flds)
-> MaybeT IO (GroundValue (BaseStructType flds))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseStructType flds)
s
      GroundValue tp -> MaybeT IO (GroundValue tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundValue tp -> MaybeT IO (GroundValue tp))
-> GroundValue tp -> MaybeT IO (GroundValue tp)
forall a b. (a -> b) -> a -> b
$! GroundValueWrapper tp -> GroundValue tp
forall (tp :: BaseType). GroundValueWrapper tp -> GroundValue tp
unGVW (Assignment GroundValueWrapper flds
sv Assignment GroundValueWrapper flds
-> Index flds tp -> GroundValueWrapper tp
forall k (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index flds tp
i)