------------------------------------------------------------------------
-- |
-- 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(..)
  , groundToSym
  , GroundArray(..)
  , lookupArray
  , GroundEvalFn(..)
  , ExprRangeBindings

    -- * Internal operations
  , tryEvalGroundExpr
  , evalGroundExpr
  , evalGroundApp
  , evalGroundNonceApp
  , defaultValueForType
  , groundEq
  ) where

import           Control.Monad
import           Control.Monad.Trans.Class
import           Control.Monad.Trans.Maybe
import qualified Data.BitVector.Sized as BV
import           Data.List.NonEmpty (NonEmpty(..))
import           Data.Foldable
import qualified Data.Map.Strict as Map
import           Data.Maybe ( fromMaybe )
import           Data.Parameterized.Ctx
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.NatRepr
import           Data.Parameterized.TraversableFC
import           Data.Ratio
import           LibBF (BigFloat)
import qualified LibBF as BF

import           What4.BaseTypes
import           What4.Interface
import qualified What4.SemiRing as SR
import qualified What4.SpecialFunctions as SFn
import qualified What4.Expr.ArrayUpdateMap as AUM
import qualified What4.Expr.BoolMap as BM
import           What4.Expr.Builder
import qualified What4.Expr.StringSeq as SSeq
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.Expr.UnaryBV as UnaryBV

import           What4.Utils.Arithmetic ( roundAway )
import           What4.Utils.Complex
import           What4.Utils.FloatHelpers
import           What4.Utils.StringLiteral


type family GroundValue (tp :: BaseType) where
  GroundValue BaseBoolType          = Bool
  GroundValue BaseIntegerType       = Integer
  GroundValue BaseRealType          = Rational
  GroundValue (BaseBVType w)        = BV.BV w
  GroundValue (BaseFloatType fpp)   = BigFloat
  GroundValue BaseComplexType       = Complex Rational
  GroundValue (BaseStringType si)   = StringLiteral si
  GroundValue (BaseArrayType idx b) = GroundArray idx b
  GroundValue (BaseStructType ctx)  = Ctx.Assignment GroundValueWrapper ctx

-- | Inject a 'GroundValue' back into a 'SymExpr'.
--
-- c.f. 'What4.Interface.concreteToSym'.
groundToSym ::
  IsExprBuilder sym =>
  sym ->
  BaseTypeRepr tp ->
  GroundValue tp ->
  IO (SymExpr sym tp)
groundToSym :: forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
groundToSym sym
sym BaseTypeRepr tp
tpr GroundValue tp
val =
  case BaseTypeRepr tp
tpr of
    BaseTypeRepr tp
BaseBoolRepr -> SymExpr sym 'BaseBoolType -> IO (SymExpr sym 'BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (if Bool
GroundValue tp
val then sym -> SymExpr sym 'BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym else sym -> SymExpr sym 'BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
    BaseBVRepr NatRepr w
w -> sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
GroundValue tp
val
    BaseTypeRepr tp
BaseIntegerRepr -> sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
GroundValue tp
val
    BaseTypeRepr tp
BaseRealRepr -> sym -> Rational -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
GroundValue tp
val
    BaseFloatRepr FloatPrecisionRepr fpp
fpp -> sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
forall (fpp :: FloatPrecision).
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
floatLit sym
sym FloatPrecisionRepr fpp
fpp BigFloat
GroundValue tp
val
    BaseStringRepr StringInfoRepr si
_ -> sym -> StringLiteral si -> IO (SymString sym si)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
stringLit sym
sym StringLiteral si
GroundValue tp
val
    BaseTypeRepr tp
BaseComplexRepr -> sym -> Complex Rational -> IO (SymCplx sym)
forall sym.
IsExprBuilder sym =>
sym -> Complex Rational -> IO (SymCplx sym)
mkComplexLit sym
sym Complex Rational
GroundValue tp
val
    BaseStructRepr Assignment BaseTypeRepr ctx
tps ->
      sym
-> Assignment (SymExpr sym) ctx
-> IO (SymExpr sym ('BaseStructType ctx))
forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
forall (flds :: Ctx BaseType).
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
mkStruct sym
sym (Assignment (SymExpr sym) ctx
 -> IO (SymExpr sym ('BaseStructType ctx)))
-> IO (Assignment (SymExpr sym) ctx)
-> IO (SymExpr sym ('BaseStructType ctx))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (x :: BaseType).
 BaseTypeRepr x -> GroundValueWrapper x -> IO (SymExpr sym x))
-> Assignment BaseTypeRepr ctx
-> Assignment GroundValueWrapper ctx
-> IO (Assignment (SymExpr sym) ctx)
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 (\BaseTypeRepr x
tp (GVW GroundValue x
gv) -> sym -> BaseTypeRepr x -> GroundValue x -> IO (SymExpr sym x)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
groundToSym sym
sym BaseTypeRepr x
tp GroundValue x
gv) Assignment BaseTypeRepr ctx
tps Assignment GroundValueWrapper ctx
GroundValue tp
val
    BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idxTy BaseTypeRepr xs
tpr' ->
      case GroundValue tp
val of
        ArrayConcrete GroundValue xs
def Map (Assignment IndexLit (idx ::> tp)) (GroundValue xs)
xs0 -> do
          SymExpr sym xs
def' <- sym -> BaseTypeRepr xs -> GroundValue xs -> IO (SymExpr sym xs)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
groundToSym sym
sym BaseTypeRepr xs
tpr' GroundValue xs
def
          SymExpr sym ('BaseArrayType (idx ::> tp) xs)
arr <- sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> SymExpr sym xs
-> IO (SymExpr sym ('BaseArrayType (idx ::> tp) xs))
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
sym
-> Assignment BaseTypeRepr (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
constantArray sym
sym Assignment BaseTypeRepr (idx ::> tp)
idxTy SymExpr sym xs
def'
          [(Assignment IndexLit (idx ::> tp), GroundValue xs)]
-> SymExpr sym ('BaseArrayType (idx ::> tp) xs)
-> IO (SymExpr sym ('BaseArrayType (idx ::> tp) xs))
go (Map (Assignment IndexLit (idx ::> tp)) (GroundValue xs)
-> [(Assignment IndexLit (idx ::> tp), GroundValue xs)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map (Assignment IndexLit (idx ::> tp)) (GroundValue xs)
xs0) SymExpr sym ('BaseArrayType (idx ::> tp) xs)
arr
        ArrayMapping Assignment GroundValueWrapper (idx ::> tp) -> IO (GroundValue xs)
_ -> String -> IO (SymExpr sym ('BaseArrayType (idx ::> tp) xs))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Can't evaluate `groundToSym` on `ArrayMapping`"
      where
      go :: [(Assignment IndexLit (idx ::> tp), GroundValue xs)]
-> SymExpr sym ('BaseArrayType (idx ::> tp) xs)
-> IO (SymExpr sym ('BaseArrayType (idx ::> tp) xs))
go [] SymExpr sym ('BaseArrayType (idx ::> tp) xs)
arr = SymExpr sym ('BaseArrayType (idx ::> tp) xs)
-> IO (SymExpr sym ('BaseArrayType (idx ::> tp) xs))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymExpr sym ('BaseArrayType (idx ::> tp) xs)
arr
      go ((Assignment IndexLit (idx ::> tp)
i, GroundValue xs
x) : [(Assignment IndexLit (idx ::> tp), GroundValue xs)]
xs) SymExpr sym ('BaseArrayType (idx ::> tp) xs)
arr =
        do SymExpr sym ('BaseArrayType (idx ::> tp) xs)
arr' <- [(Assignment IndexLit (idx ::> tp), GroundValue xs)]
-> SymExpr sym ('BaseArrayType (idx ::> tp) xs)
-> IO (SymExpr sym ('BaseArrayType (idx ::> tp) xs))
go [(Assignment IndexLit (idx ::> tp), GroundValue xs)]
xs SymExpr sym ('BaseArrayType (idx ::> tp) xs)
arr
           Assignment (SymExpr sym) (idx ::> tp)
i' <- (forall (x :: BaseType). IndexLit x -> IO (SymExpr sym x))
-> forall (x :: Ctx BaseType).
   Assignment IndexLit x -> IO (Assignment (SymExpr sym) x)
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)
forall (f :: BaseType -> Type) (g :: BaseType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: BaseType). f x -> m (g x))
-> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment g x)
traverseFC (sym -> IndexLit x -> IO (SymExpr sym x)
forall sym (idx :: BaseType).
IsExprBuilder sym =>
sym -> IndexLit idx -> IO (SymExpr sym idx)
indexLit sym
sym) Assignment IndexLit (idx ::> tp)
i
           SymExpr sym xs
x' <- sym -> BaseTypeRepr xs -> GroundValue xs -> IO (SymExpr sym xs)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
groundToSym sym
sym BaseTypeRepr xs
tpr' GroundValue xs
x
           sym
-> SymExpr sym ('BaseArrayType (idx ::> tp) xs)
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym xs
-> IO (SymExpr sym ('BaseArrayType (idx ::> tp) xs))
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
arrayUpdate sym
sym SymExpr sym ('BaseArrayType (idx ::> tp) xs)
arr' Assignment (SymExpr sym) (idx ::> tp)
i' SymExpr sym xs
x'

-- | A function that calculates ground values for elements.
--   Clients of solvers should use the @groundEval@ function for computing
--   values in models.
newtype GroundEvalFn t = GroundEvalFn { forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
groundEval :: forall tp . Expr t tp -> IO (GroundValue tp) }

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

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

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

-- | Look up an index in an ground array.
lookupArray :: Ctx.Assignment BaseTypeRepr idx
            -> GroundArray idx b
            -> Ctx.Assignment GroundValueWrapper idx
            -> IO (GroundValue b)
lookupArray :: forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray Assignment BaseTypeRepr idx
_ (ArrayMapping Assignment GroundValueWrapper idx -> IO (GroundValue b)
f) Assignment GroundValueWrapper idx
i = Assignment GroundValueWrapper idx -> IO (GroundValue b)
f Assignment GroundValueWrapper idx
i
lookupArray Assignment BaseTypeRepr idx
tps (ArrayConcrete GroundValue b
base Map (Assignment IndexLit idx) (GroundValue b)
m) Assignment GroundValueWrapper idx
i = GroundValue b -> IO (GroundValue b)
forall a. a -> IO a
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 (String -> Assignment IndexLit idx
forall a. HasCallStack => String -> a
error String
"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 BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x)
forall (x :: BaseType).
BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x)
asIndexLit Assignment BaseTypeRepr idx
tps Assignment GroundValueWrapper idx
i

-- | Update a ground array.
updateArray ::
  Ctx.Assignment BaseTypeRepr idx ->
  GroundArray idx b ->
  Ctx.Assignment GroundValueWrapper idx ->
  GroundValue b ->
  IO (GroundArray idx b)
updateArray :: forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> GroundValue b
-> IO (GroundArray idx b)
updateArray Assignment BaseTypeRepr idx
idx_tps GroundArray idx b
arr Assignment GroundValueWrapper idx
idx GroundValue b
val =
  case GroundArray idx b
arr of
    ArrayMapping Assignment GroundValueWrapper idx -> IO (GroundValue b)
arr' -> GroundArray idx b -> IO (GroundArray idx b)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundArray idx b -> IO (GroundArray idx b))
-> ((Assignment GroundValueWrapper idx -> IO (GroundValue b))
    -> GroundArray idx b)
-> (Assignment GroundValueWrapper idx -> IO (GroundValue b))
-> IO (GroundArray idx b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assignment GroundValueWrapper idx -> IO (GroundValue b))
-> GroundArray idx b
forall (idx :: Ctx BaseType) (b :: BaseType).
(Assignment GroundValueWrapper idx -> IO (GroundValue b))
-> GroundArray idx b
ArrayMapping ((Assignment GroundValueWrapper idx -> IO (GroundValue b))
 -> IO (GroundArray idx b))
-> (Assignment GroundValueWrapper idx -> IO (GroundValue b))
-> IO (GroundArray idx b)
forall a b. (a -> b) -> a -> b
$ \Assignment GroundValueWrapper idx
x ->
      if Assignment BaseTypeRepr idx
-> Assignment GroundValueWrapper idx
-> Assignment GroundValueWrapper idx
-> Bool
forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx
-> Assignment GroundValueWrapper ctx
-> Assignment GroundValueWrapper ctx
-> Bool
indicesEq Assignment BaseTypeRepr idx
idx_tps Assignment GroundValueWrapper idx
idx Assignment GroundValueWrapper idx
x then GroundValue b -> IO (GroundValue b)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GroundValue b
val else Assignment GroundValueWrapper idx -> IO (GroundValue b)
arr' Assignment GroundValueWrapper idx
x
    ArrayConcrete GroundValue b
d Map (Assignment IndexLit idx) (GroundValue b)
m -> do
      let idx' :: Assignment IndexLit idx
idx' = Assignment IndexLit idx
-> Maybe (Assignment IndexLit idx) -> Assignment IndexLit idx
forall a. a -> Maybe a -> a
fromMaybe (String -> Assignment IndexLit idx
forall a. HasCallStack => String -> a
error String
"UpdateArray only supported on Nat and BV") (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 BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x)
forall (x :: BaseType).
BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x)
asIndexLit Assignment BaseTypeRepr idx
idx_tps Assignment GroundValueWrapper idx
idx
      GroundArray idx b -> IO (GroundArray idx b)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundArray idx b -> IO (GroundArray idx b))
-> GroundArray idx b -> IO (GroundArray idx b)
forall a b. (a -> b) -> a -> b
$ GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete GroundValue b
d (Assignment IndexLit idx
-> GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> Map (Assignment IndexLit idx) (GroundValue b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Assignment IndexLit idx
idx' GroundValue b
val Map (Assignment IndexLit idx) (GroundValue b)
m)

 where indicesEq :: Ctx.Assignment BaseTypeRepr ctx
                 -> Ctx.Assignment GroundValueWrapper ctx
                 -> Ctx.Assignment GroundValueWrapper ctx
                 -> Bool
       indicesEq :: forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx
-> Assignment GroundValueWrapper ctx
-> Assignment GroundValueWrapper ctx
-> Bool
indicesEq Assignment BaseTypeRepr ctx
tps Assignment GroundValueWrapper ctx
x Assignment GroundValueWrapper ctx
y =
         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
_ -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"We do not yet support UpdateArray on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BaseTypeRepr tp -> String
forall a. Show a => a -> String
show BaseTypeRepr tp
tp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" indices."

asIndexLit :: BaseTypeRepr tp -> GroundValueWrapper tp -> Maybe (IndexLit tp)
asIndexLit :: forall (x :: BaseType).
BaseTypeRepr x -> GroundValueWrapper x -> Maybe (IndexLit x)
asIndexLit BaseTypeRepr tp
BaseIntegerRepr (GVW GroundValue tp
v) = IndexLit 'BaseIntegerType -> Maybe (IndexLit 'BaseIntegerType)
forall a. a -> Maybe a
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 tp -> Maybe (IndexLit tp)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (IndexLit tp -> Maybe (IndexLit tp))
-> IndexLit tp -> Maybe (IndexLit tp)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> IndexLit ('BaseBVType w)
forall (w :: Natural).
(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 :: forall (tp :: BaseType). 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 :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w
    BaseTypeRepr tp
BaseIntegerRepr -> Integer
GroundValue tp
0
    BaseTypeRepr tp
BaseRealRepr    -> Rational
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)
-> forall (x :: Ctx BaseType).
   Assignment BaseTypeRepr x -> Assignment GroundValueWrapper x
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
forall (f :: BaseType -> Type) (g :: BaseType -> Type).
(forall (x :: BaseType). f x -> g x)
-> forall (x :: Ctx BaseType). Assignment f x -> Assignment 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 t (tp :: BaseType).
(forall (u :: BaseType). Expr t u -> IO (GroundValue u))
-> Expr t tp -> IO (GroundValue tp)
evalGroundExpr forall (u :: BaseType). Expr t u -> IO (GroundValue u)
f Expr t tp
e =
 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 (m :: Type -> Type) a. Monad m => m a -> MaybeT m a
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 a b. IO a -> (a -> IO b) -> IO b
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 a. a -> IO a
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 -> String -> IO (GroundValue tp)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (GroundValue tp)) -> String -> IO (GroundValue tp)
forall a b. (a -> b) -> a -> b
$ String
"The ground evaluator does not support bound variables."
            VarKind
LatchVarKind      -> GroundValue tp -> IO (GroundValue tp)
forall a. a -> IO a
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 a. a -> IO a
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 -> String -> IO (GroundValue tp)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (GroundValue tp)) -> String -> IO (GroundValue tp)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"evalGroundExpr: could not evaluate expression:", Expr t tp -> String
forall a. Show a => a -> String
show Expr t tp
e]


{-# INLINABLE tryEvalGroundExpr #-}
-- | Evaluate an element, when given an evaluation function for
--   subelements.  Instead of recursing directly, `tryEvalGroundExpr`
--   calls into the given function on sub-elements to allow the caller
--   to cache results if desired.
--
--   However, sometimes we are unable to compute expressions outside
--   the solver.  In these cases, this function will return `Nothing`
--   in the `MaybeT IO` monad.  In these cases, the caller should instead
--   query the solver directly to evaluate the expression, if possible.
tryEvalGroundExpr :: (forall u . Expr t u -> MaybeT IO (GroundValue u))
                 -> Expr t tp
                 -> MaybeT IO (GroundValue tp)
tryEvalGroundExpr :: forall t (tp :: BaseType).
(forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> Expr t tp -> MaybeT IO (GroundValue tp)
tryEvalGroundExpr forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
_ (SemiRingLiteral SemiRingRepr sr
SR.SemiRingIntegerRepr Coefficient sr
c ProgramLoc
_) = Integer -> MaybeT IO Integer
forall a. a -> MaybeT IO a
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 a. a -> MaybeT IO a
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 a. a -> MaybeT IO a
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 a. a -> MaybeT IO a
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 a. a -> MaybeT IO a
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 a. a -> MaybeT IO a
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).
Monad m =>
(forall (u :: BaseType). Expr t u -> MaybeT m (GroundValue u))
-> NonceApp t (Expr t) tp -> MaybeT m (GroundValue tp)
evalGroundNonceApp Expr t u -> MaybeT IO (GroundValue u)
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 Expr t u -> MaybeT IO (GroundValue u)
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 a. MaybeT IO a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero

{-# INLINABLE evalGroundNonceApp #-}
-- | Helper function for evaluating @NonceApp@ expressions.
--
--   This function is intended for implementers of symbolic backends.
evalGroundNonceApp :: Monad m
                   => (forall u . Expr t u -> MaybeT m (GroundValue u))
                   -> NonceApp t (Expr t) tp
                   -> MaybeT m (GroundValue tp)
evalGroundNonceApp :: forall (m :: Type -> Type) t (tp :: BaseType).
Monad m =>
(forall (u :: BaseType). Expr t u -> MaybeT m (GroundValue u))
-> NonceApp t (Expr t) tp -> MaybeT m (GroundValue tp)
evalGroundNonceApp forall (u :: BaseType). Expr t u -> MaybeT m (GroundValue u)
fn NonceApp t (Expr t) tp
a0 =
  case NonceApp t (Expr t) tp
a0 of
    Annotation BaseTypeRepr tp
_ Nonce t tp
_ Expr t tp
t -> Expr t tp -> MaybeT m (GroundValue tp)
forall (u :: BaseType). Expr t u -> MaybeT m (GroundValue u)
fn Expr t tp
t
    Forall{} -> MaybeT m Bool
MaybeT m (GroundValue tp)
forall a. MaybeT m a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
    Exists{} -> MaybeT m Bool
MaybeT m (GroundValue tp)
forall a. MaybeT m a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
    MapOverArrays{} -> MaybeT m (GroundArray (idx ::> itp) r)
MaybeT m (GroundValue tp)
forall a. MaybeT m a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
    ArrayFromFn{} -> MaybeT m (GroundArray (idx ::> itp) ret)
MaybeT m (GroundValue tp)
forall a. MaybeT m a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
    ArrayTrueOnEntries{} -> MaybeT m Bool
MaybeT m (GroundValue tp)
forall a. MaybeT m a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero
    FnApp{} -> MaybeT m (GroundValue tp)
forall a. MaybeT m a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero

{-# INLINABLE evalGroundApp #-}

forallIndex :: Ctx.Size (ctx :: Ctx.Ctx k) -> (forall tp . Ctx.Index ctx tp -> Bool) -> Bool
forallIndex :: forall k (ctx :: Ctx k).
Size ctx -> (forall (tp :: k). Index ctx tp -> Bool) -> Bool
forallIndex Size ctx
sz forall (tp :: k). Index ctx tp -> Bool
f = 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 { forall {k} (x :: k). MAnd x -> Maybe Bool
unMAnd :: Maybe Bool }
instance Functor MAnd where
  fmap :: forall a b. (a -> b) -> MAnd a -> MAnd b
fmap a -> b
_f (MAnd Maybe Bool
x) = Maybe Bool -> MAnd b
forall {k} (x :: k). Maybe Bool -> MAnd x
MAnd Maybe Bool
x
instance Applicative MAnd where
  pure :: forall a. 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) <*> :: forall a b. 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 :: forall {k} (z :: k). 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 :: forall {k} {k} (a :: k) (b :: k). 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 :: forall (tp :: BaseType).
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 :: forall {k} (tp :: BaseType) (z :: k).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> MAnd z
f BaseTypeRepr tp
bt GroundValue tp
x GroundValue tp
y = case BaseTypeRepr tp
bt of
      BaseTypeRepr tp
BaseBoolRepr     -> 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 t (tp :: BaseType).
(forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u))
-> App (Expr t) tp -> MaybeT IO (GroundValue tp)
evalGroundApp forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f App (Expr t) tp
a0 = do
  case App (Expr t) tp
a0 of
    BaseEq BaseTypeRepr tp1
bt Expr t tp1
x Expr t tp1
y ->
      do GroundValue tp1
x' <- Expr t tp1 -> MaybeT IO (GroundValue tp1)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp1
x
         GroundValue tp1
y' <- Expr t tp1 -> MaybeT IO (GroundValue tp1)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t tp1
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 a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BaseTypeRepr tp1
-> GroundValue tp1 -> GroundValue tp1 -> Maybe Bool
forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
groundEq BaseTypeRepr tp1
bt GroundValue tp1
x' GroundValue tp1
y'))

    BaseIte BaseTypeRepr tp
_ Integer
_ Expr t 'BaseBoolType
x Expr t tp
y Expr t tp
z -> do
      Bool
xv <- 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 (GroundValue 'BaseBoolType)
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 a. a -> MaybeT IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
True
        BoolMapView (Expr t)
BM.BoolMapDualUnit -> Bool -> MaybeT IO Bool
forall a. a -> MaybeT IO a
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 b a. (b -> a -> b) -> b -> [a] -> b
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 (GroundValue 'BaseBoolType)
pol (Expr t 'BaseBoolType, Polarity)
t MaybeT IO ([Bool] -> Bool) -> MaybeT IO [Bool] -> MaybeT IO Bool
forall a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (Expr t 'BaseBoolType, Polarity) -> MaybeT IO Bool
(Expr t 'BaseBoolType, Polarity)
-> MaybeT IO (GroundValue 'BaseBoolType)
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 :: Natural). 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 :: Natural).
(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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 (w :: Natural). Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x
    BVUlt Expr t (BaseBVType w)
x Expr t (BaseBVType w)
y -> BV w -> BV w -> Bool
forall (w :: Natural). 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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 {a}. Num a => Integer -> Integer -> a
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 -> a
intModu Integer
_ Integer
0 = a
0
            intModu Integer
i Integer
v = Integer -> a
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 -> GroundValue 'BaseRealType -> GroundValue 'BaseRealType -> Bool
forall a. Ord a => a -> a -> Bool
(<=) (GroundValue 'BaseRealType -> GroundValue 'BaseRealType -> Bool)
-> MaybeT IO (GroundValue 'BaseRealType)
-> MaybeT IO (GroundValue 'BaseRealType -> 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 (GroundValue 'BaseRealType -> Bool)
-> MaybeT IO (GroundValue 'BaseRealType) -> MaybeT IO Bool
forall a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 -> GroundValue 'BaseIntegerType
-> GroundValue 'BaseIntegerType -> Bool
forall a. Ord a => a -> a -> Bool
(<=) (GroundValue 'BaseIntegerType
 -> GroundValue 'BaseIntegerType -> Bool)
-> MaybeT IO (GroundValue 'BaseIntegerType)
-> MaybeT IO (GroundValue 'BaseIntegerType -> 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 (GroundValue 'BaseIntegerType -> Bool)
-> MaybeT IO (GroundValue 'BaseIntegerType) -> MaybeT IO Bool
forall a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 -> (GroundValue 'BaseIntegerType
 -> GroundValue 'BaseIntegerType
 -> MaybeT IO (GroundValue 'BaseIntegerType))
-> (Coefficient sr
    -> Expr t (SemiRingBase sr)
    -> MaybeT IO (GroundValue 'BaseIntegerType))
-> (Coefficient sr -> MaybeT IO (GroundValue 'BaseIntegerType))
-> WeightedSum (Expr t) sr
-> MaybeT IO (GroundValue 'BaseIntegerType)
forall (m :: Type -> Type) r (sr :: SemiRing)
       (f :: BaseType -> Type).
Monad m =>
(r -> r -> m r)
-> (Coefficient sr -> f (SemiRingBase sr) -> m r)
-> (Coefficient sr -> m r)
-> WeightedSum f sr
-> m r
WSum.evalM (\GroundValue 'BaseIntegerType
x GroundValue 'BaseIntegerType
y -> GroundValue 'BaseIntegerType
-> MaybeT IO (GroundValue 'BaseIntegerType)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (GroundValue 'BaseIntegerType
xGroundValue 'BaseIntegerType
-> GroundValue 'BaseIntegerType -> GroundValue 'BaseIntegerType
forall a. Num a => a -> a -> a
+GroundValue 'BaseIntegerType
y)) Coefficient sr
-> Expr t (SemiRingBase sr)
-> MaybeT IO (GroundValue 'BaseIntegerType)
GroundValue 'BaseIntegerType
-> Expr t 'BaseIntegerType
-> MaybeT IO (GroundValue 'BaseIntegerType)
smul Coefficient sr -> MaybeT IO (GroundValue 'BaseIntegerType)
GroundValue 'BaseIntegerType
-> MaybeT IO (GroundValue 'BaseIntegerType)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure WeightedSum (Expr t) sr
s
           where smul :: GroundValue 'BaseIntegerType
-> Expr t 'BaseIntegerType
-> MaybeT IO (GroundValue 'BaseIntegerType)
smul GroundValue 'BaseIntegerType
sm Expr t 'BaseIntegerType
e = (GroundValue 'BaseIntegerType
sm GroundValue 'BaseIntegerType
-> GroundValue 'BaseIntegerType -> GroundValue 'BaseIntegerType
forall a. Num a => a -> a -> a
*) (GroundValue 'BaseIntegerType -> GroundValue 'BaseIntegerType)
-> MaybeT IO (GroundValue 'BaseIntegerType)
-> MaybeT IO (GroundValue 'BaseIntegerType)
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 -> (GroundValue 'BaseRealType
 -> GroundValue 'BaseRealType
 -> MaybeT IO (GroundValue 'BaseRealType))
-> (Coefficient sr
    -> Expr t (SemiRingBase sr)
    -> MaybeT IO (GroundValue 'BaseRealType))
-> (Coefficient sr -> MaybeT IO (GroundValue 'BaseRealType))
-> WeightedSum (Expr t) sr
-> MaybeT IO (GroundValue 'BaseRealType)
forall (m :: Type -> Type) r (sr :: SemiRing)
       (f :: BaseType -> Type).
Monad m =>
(r -> r -> m r)
-> (Coefficient sr -> f (SemiRingBase sr) -> m r)
-> (Coefficient sr -> m r)
-> WeightedSum f sr
-> m r
WSum.evalM (\GroundValue 'BaseRealType
x GroundValue 'BaseRealType
y -> GroundValue 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (GroundValue 'BaseRealType
xGroundValue 'BaseRealType
-> GroundValue 'BaseRealType -> GroundValue 'BaseRealType
forall a. Num a => a -> a -> a
+GroundValue 'BaseRealType
y)) Coefficient sr
-> Expr t (SemiRingBase sr)
-> MaybeT IO (GroundValue 'BaseRealType)
GroundValue 'BaseRealType
-> Expr t 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
smul Coefficient sr -> MaybeT IO (GroundValue 'BaseRealType)
GroundValue 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure WeightedSum (Expr t) sr
s
           where smul :: GroundValue 'BaseRealType
-> Expr t 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
smul GroundValue 'BaseRealType
sm Expr t 'BaseRealType
e = (GroundValue 'BaseRealType
sm GroundValue 'BaseRealType
-> GroundValue 'BaseRealType -> GroundValue 'BaseRealType
forall a. Num a => a -> a -> a
*) (GroundValue 'BaseRealType -> GroundValue 'BaseRealType)
-> MaybeT IO (GroundValue 'BaseRealType)
-> MaybeT IO (GroundValue 'BaseRealType)
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 BV w -> MaybeT IO (BV w)
Coefficient sr -> MaybeT IO (BV w)
forall a. a -> MaybeT IO a
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 :: Natural). 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 a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
x BV w
y)
        SR.SemiRingBVRepr BVFlavorRepr fv
SR.BVBitsRepr NatRepr w
_w -> (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 :: Natural}.
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 BV w -> MaybeT IO (BV w)
Coefficient sr -> MaybeT IO (BV w)
forall a. a -> MaybeT IO a
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 :: Natural). 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 a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BV w -> BV w -> BV w
forall (w :: Natural). 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 a. a -> MaybeT IO a
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 'BaseIntegerType -> MaybeT IO (GroundValue 'BaseIntegerType)
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 a. a -> MaybeT IO a
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 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
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 :: Natural). (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 a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
w BV w
x BV w
y)) Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 :: Natural). 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 a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.and BV w
x BV w
y)) Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
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 a. a -> MaybeT IO a
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 (m :: Type -> Type) a. Monad m => m a -> MaybeT m a
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
$ String -> IO ()
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Model returned sqrt of negative number."
      Rational -> MaybeT IO Rational
forall a. a -> MaybeT IO a
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.

    RealSpecialFunction SpecialFunction args
fn (SFn.SpecialFnArgs Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
args) ->
      let sf1 :: (Double -> Double) ->
                 Ctx.Assignment (SFn.SpecialFnArg (Expr t) BaseRealType) (EmptyCtx ::> SFn.R) ->
                 MaybeT IO (GroundValue BaseRealType)
          sf1 :: (Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 Double -> Double
dfn (Assignment (SpecialFnArg (Expr t) 'BaseRealType) ctx
Ctx.Empty Ctx.:> SFn.SpecialFnArg Expr t 'BaseRealType
x) = Double -> Rational
fromDouble (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
dfn (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

          sf2 :: (Double -> Double -> Double) ->
                 Ctx.Assignment (SFn.SpecialFnArg (Expr t) BaseRealType) (EmptyCtx ::> SFn.R ::> SFn.R) ->
                 MaybeT IO (GroundValue BaseRealType)
          sf2 :: (Double -> Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) ((EmptyCtx ::> R) ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf2 Double -> Double -> Double
dfn (Assignment (SpecialFnArg (Expr t) 'BaseRealType) ctx
Ctx.Empty Ctx.:> SFn.SpecialFnArg Expr t 'BaseRealType
x Ctx.:> SFn.SpecialFnArg Expr t 'BaseRealType
y) =
            do Rational
xv <- 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 a. a -> MaybeT IO a
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
dfn (Rational -> Double
toDouble Rational
xv) (Rational -> Double
toDouble Rational
yv))
      in case SpecialFunction args
fn of
        SpecialFunction args
SFn.Pi   -> Rational -> MaybeT IO Rational
forall a. a -> MaybeT IO a
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
        SpecialFunction args
SFn.Sin  -> (Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 Double -> Double
forall a. Floating a => a -> a
sin Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
Assignment (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
args
        SpecialFunction args
SFn.Cos  -> (Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 Double -> Double
forall a. Floating a => a -> a
cos Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
Assignment (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
args
        SpecialFunction args
SFn.Sinh -> (Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 Double -> Double
forall a. Floating a => a -> a
sinh Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
Assignment (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
args
        SpecialFunction args
SFn.Cosh -> (Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 Double -> Double
forall a. Floating a => a -> a
cosh Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
Assignment (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
args
        SpecialFunction args
SFn.Exp  -> (Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 Double -> Double
forall a. Floating a => a -> a
exp Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
Assignment (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
args
        SpecialFunction args
SFn.Log  -> (Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf1 Double -> Double
forall a. Floating a => a -> a
log Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
Assignment (SpecialFnArg (Expr t) 'BaseRealType) (EmptyCtx ::> R)
args
        SpecialFunction args
SFn.Arctan2 -> (Double -> Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) ((EmptyCtx ::> R) ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf2 Double -> Double -> Double
forall a. RealFloat a => a -> a -> a
atan2 Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
Assignment
  (SpecialFnArg (Expr t) 'BaseRealType) ((EmptyCtx ::> R) ::> R)
args
        SpecialFunction args
SFn.Pow     -> (Double -> Double -> Double)
-> Assignment
     (SpecialFnArg (Expr t) 'BaseRealType) ((EmptyCtx ::> R) ::> R)
-> MaybeT IO (GroundValue 'BaseRealType)
sf2 Double -> Double -> Double
forall a. Floating a => a -> a -> a
(**) Assignment (SpecialFnArg (Expr t) 'BaseRealType) args
Assignment
  (SpecialFnArg (Expr t) 'BaseRealType) ((EmptyCtx ::> R) ::> R)
args

        SpecialFunction args
_ -> MaybeT IO Rational
MaybeT IO (GroundValue tp)
forall a. MaybeT IO a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero -- TODO, other functions as well

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

    BVOrBits NatRepr w
w BVOrSet (Expr t) w
bs -> (BV w -> BV w -> BV w) -> BV w -> [BV w] -> BV w
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.or (NatRepr w -> BV w
forall (w :: Natural). 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)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Expr t ('BaseBVType w) -> MaybeT IO (BV w)
Expr t ('BaseBVType w) -> MaybeT IO (GroundValue ('BaseBVType 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 :: Natural).
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 :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV (UnaryBV (Expr t 'BaseBoolType) n -> NatRepr n
forall p (n :: Natural). 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 :: Natural).
Monad m =>
(p -> m Bool) -> UnaryBV p n -> m Integer
UnaryBV.evaluate Expr t 'BaseBoolType -> MaybeT IO Bool
Expr t 'BaseBoolType -> MaybeT IO (GroundValue 'BaseBoolType)
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 :: Natural) (w' :: Natural).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
BV.concat (Expr t (BaseBVType u) -> NatRepr u
forall (w :: Natural). Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType u)
x) (Expr t (BaseBVType v) -> NatRepr v
forall (w :: Natural). Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 :: Natural) (w' :: Natural) (w :: Natural).
((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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w
            myDiv BV w
u BV w
v = BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.uquot BV w
u BV w
v
    BVUrem NatRepr w
_w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> BV w -> BV w -> BV w
forall (w :: Natural). 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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 :: Natural). BV w -> BV w -> BV w
BV.urem BV w
u BV w
v
    BVSdiv NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> BV w -> BV w -> BV w
myDiv (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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 :: Natural). 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 :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> BV w
BV.sdiv NatRepr w
w BV w
u BV w
v
    BVSrem NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y -> BV w -> BV w -> BV w
myRem (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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> BV w
BV.srem NatRepr w
w BV w
u BV w
v
    BVShl  NatRepr w
w Expr t ('BaseBVType w)
x Expr t ('BaseBVType w)
y  -> NatRepr w -> BV w -> Natural -> BV w
forall (w :: Natural). 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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Natural). 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 :: Natural). 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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Natural). 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 :: Natural).
(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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Natural). 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 :: Natural). 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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Natural). 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 :: Natural). 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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (BV w -> Natural
forall (w :: Natural). 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 :: Natural) (w' :: Natural).
((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 :: Natural). 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 :: Natural) (w' :: Natural).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext (Expr t (BaseBVType w) -> NatRepr w
forall (w :: Natural). Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
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 -> String -> MaybeT IO (BV r)
forall a. HasCallStack => String -> a
error String
"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 a. a -> MaybeT IO a
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 :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w else NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w

    BVPopcount NatRepr w
_w Expr t ('BaseBVType w)
x ->
      BV w -> BV w
forall (w :: Natural). 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 :: Natural). 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 :: Natural). 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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
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 (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
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 :: Natural). 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 :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV (NatRepr eb -> NatRepr sb -> NatRepr (eb + sb)
forall (m :: Natural) (n :: Natural).
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 :: Natural). 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 :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (Expr t (BaseBVType w) -> NatRepr w
forall (w :: Natural). Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
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 a. a -> IO a
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 :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr w
w -> BV w -> MaybeT IO (BV w)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
i)
           Maybe Integer
_ -> MaybeT IO (BV w)
forall a. MaybeT IO a
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 :: Natural). (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 :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr w
w -> BV w -> MaybeT IO (BV w)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
i)
           Maybe Integer
_ -> MaybeT IO (BV w)
forall a. MaybeT IO a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero

    FloatSpecialFunction FloatPrecisionRepr fpp
_ SpecialFunction args
_ SpecialFnArgs (Expr t) ('BaseFloatType fpp) args
_ -> MaybeT IO BigFloat
MaybeT IO (GroundValue tp)
forall a. MaybeT IO a
forall (m :: Type -> Type) a. MonadPlus m => m a
mzero -- TODO? evaluate concretely?

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

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

    ConstantArray Assignment BaseTypeRepr (i ::> tp1)
_ BaseTypeRepr b
_ Expr t b
v -> do
      GroundValue b
val <- Expr t b -> MaybeT IO (GroundValue b)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t b
v
      GroundArray (i ::> tp1) b -> MaybeT IO (GroundArray (i ::> tp1) b)
forall a. a -> MaybeT IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GroundArray (i ::> tp1) b
 -> MaybeT IO (GroundArray (i ::> tp1) b))
-> GroundArray (i ::> tp1) b
-> MaybeT IO (GroundArray (i ::> tp1) b)
forall a b. (a -> b) -> a -> b
$ GroundValue b
-> Map (Assignment IndexLit (i ::> tp1)) (GroundValue b)
-> GroundArray (i ::> tp1) 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 ::> tp1)) (GroundValue b)
forall k a. Map k a
Map.empty

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

    UpdateArray BaseTypeRepr b
_ Assignment BaseTypeRepr (i ::> tp1)
idx_tps Expr t ('BaseArrayType (i ::> tp1) b)
a Assignment (Expr t) (i ::> tp1)
i Expr t b
v -> do
      GroundArray (i ::> tp1) b
arr <- Expr t ('BaseArrayType (i ::> tp1) b)
-> MaybeT IO (GroundValue ('BaseArrayType (i ::> tp1) b))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseArrayType (i ::> tp1) b)
a
      Assignment GroundValueWrapper (i ::> tp1)
idx <- (forall (x :: BaseType).
 Expr t x -> MaybeT IO (GroundValueWrapper x))
-> forall (x :: Ctx BaseType).
   Assignment (Expr t) x
   -> MaybeT IO (Assignment GroundValueWrapper x)
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)
forall (f :: BaseType -> Type) (g :: BaseType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: BaseType). f x -> m (g x))
-> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment 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 ::> tp1)
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
      IO (GroundArray (i ::> tp1) b)
-> MaybeT IO (GroundArray (i ::> tp1) b)
forall (m :: Type -> Type) a. Monad m => m a -> MaybeT m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (GroundArray (i ::> tp1) b)
 -> MaybeT IO (GroundArray (i ::> tp1) b))
-> IO (GroundArray (i ::> tp1) b)
-> MaybeT IO (GroundArray (i ::> tp1) b)
forall a b. (a -> b) -> a -> b
$ Assignment BaseTypeRepr (i ::> tp1)
-> GroundArray (i ::> tp1) b
-> Assignment GroundValueWrapper (i ::> tp1)
-> GroundValue b
-> IO (GroundArray (i ::> tp1) b)
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> GroundValue b
-> IO (GroundArray idx b)
updateArray Assignment BaseTypeRepr (i ::> tp1)
idx_tps GroundArray (i ::> tp1) b
arr Assignment GroundValueWrapper (i ::> tp1)
idx GroundValue b
v'

    CopyArray NatRepr w
w BaseTypeRepr a
_ Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
dest_arr Expr t (BaseBVType w)
dest_idx Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
src_arr Expr t (BaseBVType w)
src_idx Expr t (BaseBVType w)
len Expr t (BaseBVType w)
_ Expr t (BaseBVType w)
_ -> do
      GroundArray (SingleCtx (BaseBVType w)) a
ground_dest_arr <- Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
-> MaybeT
     IO (GroundValue ('BaseArrayType (SingleCtx (BaseBVType w)) a))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
dest_arr
      BV w
ground_dest_idx <- Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
dest_idx
      GroundArray (SingleCtx (BaseBVType w)) a
ground_src_arr <- Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
-> MaybeT
     IO (GroundValue ('BaseArrayType (SingleCtx (BaseBVType w)) a))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
src_arr
      BV w
ground_src_idx <- Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
src_idx
      BV w
ground_len <- Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
len

      IO (GroundArray (SingleCtx (BaseBVType w)) a)
-> MaybeT IO (GroundArray (SingleCtx (BaseBVType w)) a)
forall (m :: Type -> Type) a. Monad m => m a -> MaybeT m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (GroundArray (SingleCtx (BaseBVType w)) a)
 -> MaybeT IO (GroundArray (SingleCtx (BaseBVType w)) a))
-> IO (GroundArray (SingleCtx (BaseBVType w)) a)
-> MaybeT IO (GroundArray (SingleCtx (BaseBVType w)) a)
forall a b. (a -> b) -> a -> b
$ (GroundArray (SingleCtx (BaseBVType w)) a
 -> (BV w, BV w) -> IO (GroundArray (SingleCtx (BaseBVType w)) a))
-> GroundArray (SingleCtx (BaseBVType w)) a
-> [(BV w, BV w)]
-> IO (GroundArray (SingleCtx (BaseBVType w)) a)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
        (\GroundArray (SingleCtx (BaseBVType w)) a
arr_acc (BV w
dest_i, BV w
src_i) ->
          Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
-> GroundArray (SingleCtx (BaseBVType w)) a
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
-> GroundValue a
-> IO (GroundArray (SingleCtx (BaseBVType w)) a)
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> GroundValue b
-> IO (GroundArray idx b)
updateArray (BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (BaseTypeRepr (BaseBVType w)
 -> Assignment BaseTypeRepr (SingleCtx (BaseBVType w)))
-> BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
arr_acc (GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (GroundValueWrapper (BaseBVType w)
 -> Assignment GroundValueWrapper (SingleCtx (BaseBVType w)))
-> GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ GroundValue (BaseBVType w) -> GroundValueWrapper (BaseBVType w)
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
GroundValue (BaseBVType w)
dest_i)
            (GroundValue a -> IO (GroundArray (SingleCtx (BaseBVType w)) a))
-> IO (GroundValue a)
-> IO (GroundArray (SingleCtx (BaseBVType w)) a)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
-> GroundArray (SingleCtx (BaseBVType w)) a
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
-> IO (GroundValue a)
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray (BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (BaseTypeRepr (BaseBVType w)
 -> Assignment BaseTypeRepr (SingleCtx (BaseBVType w)))
-> BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
ground_src_arr (GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (GroundValueWrapper (BaseBVType w)
 -> Assignment GroundValueWrapper (SingleCtx (BaseBVType w)))
-> GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ GroundValue (BaseBVType w) -> GroundValueWrapper (BaseBVType w)
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
GroundValue (BaseBVType w)
src_i))
        GroundArray (SingleCtx (BaseBVType w)) a
ground_dest_arr
        ([BV w] -> [BV w] -> [(BV w, BV w)]
forall a b. [a] -> [b] -> [(a, b)]
zip
          (BV w -> BV w -> [BV w]
forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_dest_idx (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_dest_idx BV w
ground_len) (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1)))
          (BV w -> BV w -> [BV w]
forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_src_idx (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_src_idx BV w
ground_len) (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1))))

    SetArray NatRepr w
w BaseTypeRepr a
_ Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
arr Expr t (BaseBVType w)
idx Expr t a
val Expr t (BaseBVType w)
len Expr t (BaseBVType w)
_ -> do
      GroundArray (SingleCtx (BaseBVType w)) a
ground_arr <- Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
-> MaybeT
     IO (GroundValue ('BaseArrayType (SingleCtx (BaseBVType w)) a))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t ('BaseArrayType (SingleCtx (BaseBVType w)) a)
arr
      BV w
ground_idx <- Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
idx
      GroundValue a
ground_val <- Expr t a -> MaybeT IO (GroundValue a)
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t a
val
      BV w
ground_len <- Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
len

      IO (GroundArray (SingleCtx (BaseBVType w)) a)
-> MaybeT IO (GroundArray (SingleCtx (BaseBVType w)) a)
forall (m :: Type -> Type) a. Monad m => m a -> MaybeT m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (GroundArray (SingleCtx (BaseBVType w)) a)
 -> MaybeT IO (GroundArray (SingleCtx (BaseBVType w)) a))
-> IO (GroundArray (SingleCtx (BaseBVType w)) a)
-> MaybeT IO (GroundArray (SingleCtx (BaseBVType w)) a)
forall a b. (a -> b) -> a -> b
$ (GroundArray (SingleCtx (BaseBVType w)) a
 -> BV w -> IO (GroundArray (SingleCtx (BaseBVType w)) a))
-> GroundArray (SingleCtx (BaseBVType w)) a
-> [BV w]
-> IO (GroundArray (SingleCtx (BaseBVType w)) a)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
        (\GroundArray (SingleCtx (BaseBVType w)) a
arr_acc BV w
i ->
          Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
-> GroundArray (SingleCtx (BaseBVType w)) a
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
-> GroundValue a
-> IO (GroundArray (SingleCtx (BaseBVType w)) a)
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> GroundValue b
-> IO (GroundArray idx b)
updateArray (BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (BaseTypeRepr (BaseBVType w)
 -> Assignment BaseTypeRepr (SingleCtx (BaseBVType w)))
-> BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
arr_acc (GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (GroundValueWrapper (BaseBVType w)
 -> Assignment GroundValueWrapper (SingleCtx (BaseBVType w)))
-> GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ GroundValue (BaseBVType w) -> GroundValueWrapper (BaseBVType w)
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
GroundValue (BaseBVType w)
i) GroundValue a
ground_val)
        GroundArray (SingleCtx (BaseBVType w)) a
ground_arr
        (BV w -> BV w -> [BV w]
forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_idx (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_idx BV w
ground_len) (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1)))

    EqualArrayRange NatRepr w
w BaseTypeRepr a
a_repr Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
lhs_arr Expr t (BaseBVType w)
lhs_idx Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
rhs_arr Expr t (BaseBVType w)
rhs_idx Expr t (BaseBVType w)
len Expr t (BaseBVType w)
_ Expr t (BaseBVType w)
_ -> do
      GroundArray (SingleCtx (BaseBVType w)) a
ground_lhs_arr <- Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
-> MaybeT
     IO (GroundValue (BaseArrayType (SingleCtx (BaseBVType w)) a))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
lhs_arr
      BV w
ground_lhs_idx <- Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
lhs_idx
      GroundArray (SingleCtx (BaseBVType w)) a
ground_rhs_arr <- Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
-> MaybeT
     IO (GroundValue (BaseArrayType (SingleCtx (BaseBVType w)) a))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseArrayType (SingleCtx (BaseBVType w)) a)
rhs_arr
      BV w
ground_rhs_idx <- Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
rhs_idx
      BV w
ground_len <- Expr t (BaseBVType w) -> MaybeT IO (GroundValue (BaseBVType w))
forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
f Expr t (BaseBVType w)
len

      (Bool -> (BV w, BV w) -> MaybeT IO Bool)
-> Bool -> [(BV w, BV w)] -> MaybeT IO Bool
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
        (\Bool
acc (BV w
lhs_i, BV w
rhs_i) -> do
            Bool
ground_eq_res <- IO (Maybe Bool) -> MaybeT IO Bool
forall (m :: Type -> Type) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe Bool) -> MaybeT IO Bool)
-> IO (Maybe Bool) -> MaybeT IO Bool
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr a -> GroundValue a -> GroundValue a -> Maybe Bool
forall (tp :: BaseType).
BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool
groundEq BaseTypeRepr a
a_repr (GroundValue a -> GroundValue a -> Maybe Bool)
-> IO (GroundValue a) -> IO (GroundValue a -> Maybe Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
              Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
-> GroundArray (SingleCtx (BaseBVType w)) a
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
-> IO (GroundValue a)
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray (BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (BaseTypeRepr (BaseBVType w)
 -> Assignment BaseTypeRepr (SingleCtx (BaseBVType w)))
-> BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
ground_lhs_arr (GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (GroundValueWrapper (BaseBVType w)
 -> Assignment GroundValueWrapper (SingleCtx (BaseBVType w)))
-> GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ GroundValue (BaseBVType w) -> GroundValueWrapper (BaseBVType w)
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
GroundValue (BaseBVType w)
lhs_i) IO (GroundValue a -> Maybe Bool)
-> IO (GroundValue a) -> IO (Maybe Bool)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*>
              Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
-> GroundArray (SingleCtx (BaseBVType w)) a
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
-> IO (GroundValue a)
forall (idx :: Ctx BaseType) (b :: BaseType).
Assignment BaseTypeRepr idx
-> GroundArray idx b
-> Assignment GroundValueWrapper idx
-> IO (GroundValue b)
lookupArray (BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (BaseTypeRepr (BaseBVType w)
 -> Assignment BaseTypeRepr (SingleCtx (BaseBVType w)))
-> BaseTypeRepr (BaseBVType w)
-> Assignment BaseTypeRepr (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w) GroundArray (SingleCtx (BaseBVType w)) a
ground_rhs_arr (GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (GroundValueWrapper (BaseBVType w)
 -> Assignment GroundValueWrapper (SingleCtx (BaseBVType w)))
-> GroundValueWrapper (BaseBVType w)
-> Assignment GroundValueWrapper (SingleCtx (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ GroundValue (BaseBVType w) -> GroundValueWrapper (BaseBVType w)
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW BV w
GroundValue (BaseBVType w)
rhs_i)
            Bool -> MaybeT IO Bool
forall a. a -> MaybeT IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool -> MaybeT IO Bool) -> Bool -> MaybeT IO Bool
forall a b. (a -> b) -> a -> b
$ Bool
acc Bool -> Bool -> Bool
&& Bool
ground_eq_res)
        Bool
True
        ([BV w] -> [BV w] -> [(BV w, BV w)]
forall a b. [a] -> [b] -> [(a, b)]
zip
          (BV w -> BV w -> [BV w]
forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_lhs_idx (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_lhs_idx BV w
ground_len) (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1)))
          (BV w -> BV w -> [BV w]
forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned BV w
ground_rhs_idx (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
ground_rhs_idx BV w
ground_len) (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1))))

    ------------------------------------------------------------------------
    -- 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 :: Natural). 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 :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (Expr t (BaseBVType w) -> NatRepr w
forall (w :: Natural). Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
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 b. Integral b => Rational -> b
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 b. Integral b => Rational -> b
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 b. Integral b => Rational -> b
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 b. Integral b => Rational -> b
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 :: Natural). 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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
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 a. a -> MaybeT IO a
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))
-> forall (x :: Ctx BaseType).
   Assignment (Expr t) x
   -> MaybeT IO (Assignment GroundValueWrapper x)
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)
forall (f :: BaseType -> Type) (g :: BaseType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: BaseType). f x -> m (g x))
-> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment 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 a. a -> MaybeT IO a
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)