    ------------------------------------------------------------------------
    -- |
    -- 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
              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
              arr <- constantArray sym idxTy def'
              go (Map.toAscList xs0) 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 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
               i' <- traverseFC (indexLit sym) i
               x' <- groundToSym sym tpr' x
               arrayUpdate sym arr' i' 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 (ZonkAny 2) -> Maybe Bool
    forall {k} (x :: k). MAnd x -> Maybe Bool
    unMAnd (BaseTypeRepr tp
    -> GroundValue tp -> GroundValue tp -> MAnd (ZonkAny 2)
    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 (ZonkAny 0) ctx) -> MAnd z
    forall {k} {k} (a :: k) (b :: k). MAnd a -> MAnd b
    coerceMAnd ((forall (tp :: BaseType).
     Index ctx tp -> BaseTypeRepr tp -> MAnd (ZonkAny 0 tp))
    -> Assignment BaseTypeRepr ctx -> MAnd (Assignment (ZonkAny 0) 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 (ZonkAny 0 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 x' <- Expr t tp1 -> MaybeT IO (GroundValue tp1)
    forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
    f Expr t tp1
    x
             y' <- f y
             MaybeT (return (groundEq bt x' y'))

        BaseIte BaseTypeRepr tp
    _ Integer
    _ Expr t 'BaseBoolType
    x Expr t tp
    y Expr t tp
    z -> do
          xv <- Expr t 'BaseBoolType -> MaybeT IO (GroundValue 'BaseBoolType)
    forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
    f Expr t 'BaseBoolType
    x
          if xv then f y else f 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
          xv <- Expr t 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
    forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
    f Expr t 'BaseRealType
    x
          yv <- f y
          return $!
            if yv == 0 then 0 else xv / yv
        RealSqrt Expr t 'BaseRealType
    x -> do
          xv <- Expr t 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
    forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
    f Expr t 'BaseRealType
    x
          when (xv < 0) $ do
            lift $ fail $ "Model returned sqrt of negative number."
          return $ fromDouble (sqrt (toDouble 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 xv <- Expr t 'BaseRealType -> MaybeT IO (GroundValue 'BaseRealType)
    forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
    f Expr t 'BaseRealType
    x
                   yv <- f y
                   return $ fromDouble (dfn (toDouble xv) (toDouble 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 b <- Expr t 'BaseBoolType -> MaybeT IO (GroundValue 'BaseBoolType)
    forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
    f Expr t 'BaseBoolType
    p
             return $! if b then BV.maxUnsigned w else BV.zero 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 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 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 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 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
          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)
          h <- f def
          return $ case 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
          val <- Expr t b -> MaybeT IO (GroundValue b)
    forall (u :: BaseType). Expr t u -> MaybeT IO (GroundValue u)
    f Expr t b
    v
          return $ ArrayConcrete val Map.empty

        SelectArray BaseTypeRepr tp
    _ Expr t (BaseArrayType (i ::> tp1) tp)
    a Assignment (Expr t) (i ::> tp1)
    i -> do
          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 = 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
          idx <- 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) i
          lift $ lookupArray arrIdxTps arr 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
          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
          idx <- 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) i
          v'  <- f v
          lift $ updateArray idx_tps arr idx 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
          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
          ground_dest_idx <- f dest_idx
          ground_src_arr <- f src_arr
          ground_src_idx <- f src_idx
          ground_len <- f len

          lift $ 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))
            ground_dest_arr
            (zip
              (BV.enumFromToUnsigned ground_dest_idx (BV.sub w (BV.add w ground_dest_idx ground_len) (BV.mkBV w 1)))
              (BV.enumFromToUnsigned ground_src_idx (BV.sub w (BV.add w ground_src_idx ground_len) (BV.mkBV w 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
          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
          ground_idx <- f idx
          ground_val <- f val
          ground_len <- f len

          lift $ 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)
            ground_arr
            (BV.enumFromToUnsigned ground_idx (BV.sub w (BV.add w ground_idx ground_len) (BV.mkBV w 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
          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
          ground_lhs_idx <- f lhs_idx
          ground_rhs_arr <- f rhs_arr
          ground_rhs_idx <- f rhs_idx
          ground_len <- f len

          foldlM
            (\Bool
    acc (BV w
    lhs_i, BV w
    rhs_i) -> do
                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)
                return $ acc && ground_eq_res)
            True
            (zip
              (BV.enumFromToUnsigned ground_lhs_idx (BV.sub w (BV.add w ground_lhs_idx ground_len) (BV.mkBV w 1)))
              (BV.enumFromToUnsigned ground_rhs_idx (BV.sub w (BV.add w ground_rhs_idx ground_len) (BV.mkBV w 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
          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
          return $! unGVW (sv Ctx.! i)