Language.SMTLib2.Internals.Monad

Documentation

newtype Backend b => SMT b a

Constructors

SMT

Fields

runSMT :: StateT (SMTState b) (SMTMonad b) a

Instances

Backend b => Monad (SMT b)

Backend b => Functor (SMT b)

Backend b => Applicative (SMT b)

(Backend b, MonadIO (SMTMonad b)) => MonadIO (SMT b)

(Backend b, (~) (Type -> *) e (Expr b)) => Embed (SMT b) e

Backend b => MonadState (SMTState b) (SMT b)

type EmVar (SMT b) e = Var b

type EmQVar (SMT b) e = QVar b

type EmFun (SMT b) e = Fun b

type EmConstr (SMT b) e = Constr b

type EmField (SMT b) e = Field b

type EmFunArg (SMT b) e = FunArg b

type EmLVar (SMT b) e = LVar b

data SMTState b

Constructors

SMTState

Fields

backend :: !b

datatypes :: !(DatatypeInfo (Constr b) (Field b))

Instances

Backend b => MonadState (SMTState b) (SMT b)

withBackend :: Backend b => SMTMonad b b -> SMT b a -> SMTMonad b a

withBackendExitCleanly :: (Backend b, SMTMonad b ~ IO) => IO b -> SMT b a -> IO a

liftSMT :: Backend b => SMTMonad b a -> SMT b a

embedSMT :: Backend b => (b -> SMTMonad b (a, b)) -> SMT b a

embedSMT' :: Backend b => (b -> SMTMonad b b) -> SMT b ()

data DTProxy dt where

Constructors

DTProxy :: IsDatatype dt => DTProxy dt

Instances

GCompare * DTProxy

GEq * DTProxy

GShow * DTProxy

Show (DTProxy dt)

type DatatypeInfo con field = DMap DTProxy (RegisteredDT con field)

newtype RegisteredDT con field dt

Constructors

RegisteredDT (BackendDatatype con field `(DatatypeSig dt, dt)`)

emptyDatatypeInfo :: DatatypeInfo con field

reproxyDT :: IsDatatype dt => Proxy dt -> DTProxy dt

registerDatatype :: (Backend b, IsDatatype dt) => Proxy dt -> SMT b ()

lookupDatatype :: DTProxy dt -> DatatypeInfo con field -> BackendDatatype con field `(DatatypeSig dt, dt)`

lookupConstructor :: String -> BackendDatatype con field `(DatatypeSig dt, dt)` -> (forall arg. BackendConstr con field `(arg, dt)` -> a) -> a

constructDatatype :: GEq con => con `(arg, ret)` -> List ConcreteValue arg -> BackendDatatype con field `(cons, ret)` -> ret

lookupField :: String -> BackendConstr con field `(arg, dt)` -> (forall tp. BackendField field dt tp -> a) -> a

lookupDatatypeCon :: (IsDatatype dt, Typeable con, Typeable field) => DTProxy dt -> String -> DatatypeInfo con field -> (forall arg. BackendConstr con field `(arg, dt)` -> a) -> a

lookupDatatypeField :: (IsDatatype dt, Typeable con, Typeable field) => DTProxy dt -> String -> String -> DatatypeInfo con field -> (forall tp. BackendField field dt tp -> a) -> a

mkConcr :: Backend b => Value (Constr b) t -> SMT b (ConcreteValue t)

mkAbstr :: Backend b => ConcreteValue t -> SMT b (Value (Constr b) t)

defineVar' :: Backend b => Expr b t -> SMT b (Var b t)

defineVarNamed' :: Backend b => String -> Expr b t -> SMT b (Var b t)

declareVar' :: Backend b => Repr t -> SMT b (Var b t)

declareVarNamed' :: Backend b => Repr t -> String -> SMT b (Var b t)