Language.SMTLib2.Internals.Embed

Documentation

type EmbedExpr m e tp = Expression (EmVar m e) (EmQVar m e) (EmFun m e) (EmConstr m e) (EmField m e) (EmFunArg m e) (EmLVar m e) e tp

class (Monad m, GCompare (EmVar m e), GCompare (EmQVar m e), GCompare (EmFun m e), GCompare (EmConstr m e), GCompare (EmField m e), GCompare (EmFunArg m e), GCompare (EmLVar m e), Typeable (EmConstr m e)) => Embed m e where

Associated Types

type EmVar m e :: Type -> *

type EmQVar m e :: Type -> *

type EmFun m e :: ([Type], Type) -> *

type EmConstr m e :: ([Type], *) -> *

type EmField m e :: (*, Type) -> *

type EmFunArg m e :: Type -> *

type EmLVar m e :: Type -> *

Methods

embed :: EmbedExpr m e tp -> m (e tp)

embedQuantifier :: Quantifier -> List Repr arg -> (forall m e. Embed m e => List (EmQVar m e) arg -> m (e BoolType)) -> m (e BoolType)

embedConstrTest :: IsDatatype dt => String -> Proxy dt -> e (DataType dt) -> m (e BoolType)

embedGetField :: IsDatatype dt => String -> String -> Proxy dt -> Repr tp -> e (DataType dt) -> m (e tp)

embedConst :: ConcreteValue tp -> m (e tp)

embedTypeOf :: e tp -> m (Repr tp)

Instances

(GCompare Type var, GetType var, GCompare Type qvar, GetType qvar, GCompare ((,) [Type] Type) fun, GetFunType fun, GCompare ((,) [Type] *) con, GetConType con, GCompare ((,) * Type) field, GetFieldType field, GCompare Type farg, GetType farg, GCompare Type lvar, GetType lvar, Typeable ((,) [Type] * -> *) con) => Embed Identity (SMTExpr var qvar fun con field farg lvar)

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

class (GCompare (ExVar i e), GCompare (ExQVar i e), GCompare (ExFun i e), GCompare (ExConstr i e), GCompare (ExField i e), GCompare (ExFunArg i e), GCompare (ExLVar i e), Typeable (ExConstr i e)) => Extract i e where

Associated Types

type ExVar i e :: Type -> *

type ExQVar i e :: Type -> *

type ExFun i e :: ([Type], Type) -> *

type ExConstr i e :: ([Type], *) -> *

type ExField i e :: (*, Type) -> *

type ExFunArg i e :: Type -> *

type ExLVar i e :: Type -> *

Methods

extract :: i -> e tp -> Maybe (Expression (ExVar i e) (ExQVar i e) (ExFun i e) (ExConstr i e) (ExField i e) (ExFunArg i e) (ExLVar i e) e tp)

Instances

(GCompare Type var, GCompare Type qvar, GCompare ((,) [Type] Type) fun, GCompare ((,) [Type] *) con, GCompare ((,) * Type) field, GCompare Type farg, GCompare Type lvar, Typeable ((,) [Type] * -> *) con) => Extract () (SMTExpr var qvar fun con field farg lvar)

(Backend b, (~) (Type -> *) e (Expr b)) => Extract (BackendInfo b) e

newtype BackendInfo b

Constructors

BackendInfo b

Instances

(Backend b, (~) (Type -> *) e (Expr b)) => Extract (BackendInfo b) e

type ExVar (BackendInfo b) e = Var b

type ExQVar (BackendInfo b) e = QVar b

type ExFun (BackendInfo b) e = Fun b

type ExConstr (BackendInfo b) e = Constr b

type ExField (BackendInfo b) e = Field b

type ExFunArg (BackendInfo b) e = FunArg b

type ExLVar (BackendInfo b) e = LVar b

data SMTExpr var qvar fun con field farg lvar tp where

Constructors

SMTExpr :: Expression var qvar fun con field farg lvar (SMTExpr var qvar fun con field farg lvar) tp -> SMTExpr var qvar fun con field farg lvar tp

SMTQuant :: Quantifier -> List Repr args -> (List qvar args -> SMTExpr var qvar fun con field farg lvar BoolType) -> SMTExpr var qvar fun con field farg lvar BoolType

SMTTestCon :: IsDatatype dt => String -> Proxy dt -> SMTExpr var qvar fun con field farg lvar (DataType dt) -> SMTExpr var qvar fun con field farg lvar BoolType

SMTGetField :: IsDatatype dt => String -> String -> Proxy dt -> Repr tp -> SMTExpr var qvar fun con field farg lvar (DataType dt) -> SMTExpr var qvar fun con field farg lvar tp

SMTConst :: ConcreteValue tp -> SMTExpr var qvar fun con field farg lvar tp

Instances

(GCompare Type var, GCompare Type qvar, GCompare ((,) [Type] Type) fun, GCompare ((,) [Type] *) con, GCompare ((,) * Type) field, GCompare Type farg, GCompare Type lvar, Typeable ((,) [Type] * -> *) con) => Extract () (SMTExpr var qvar fun con field farg lvar)

(GCompare Type var, GetType var, GCompare Type qvar, GetType qvar, GCompare ((,) [Type] Type) fun, GetFunType fun, GCompare ((,) [Type] *) con, GetConType con, GCompare ((,) * Type) field, GetFieldType field, GCompare Type farg, GetType farg, GCompare Type lvar, GetType lvar, Typeable ((,) [Type] * -> *) con) => Embed Identity (SMTExpr var qvar fun con field farg lvar)

(GetType var, GetType qvar, GetFunType fun, GetConType con, GetFieldType field, GetType farg, GetType lvar) => GetType (SMTExpr var qvar fun con field farg lvar)

type ExVar () (SMTExpr var qvar fun con field farg lvar) = var

type ExQVar () (SMTExpr var qvar fun con field farg lvar) = qvar

type ExFun () (SMTExpr var qvar fun con field farg lvar) = fun

type ExConstr () (SMTExpr var qvar fun con field farg lvar) = con

type ExField () (SMTExpr var qvar fun con field farg lvar) = field

type ExFunArg () (SMTExpr var qvar fun con field farg lvar) = farg

type ExLVar () (SMTExpr var qvar fun con field farg lvar) = lvar

type EmVar Identity (SMTExpr var qvar fun con field farg lvar) = var

type EmQVar Identity (SMTExpr var qvar fun con field farg lvar) = qvar

type EmFun Identity (SMTExpr var qvar fun con field farg lvar) = fun

type EmConstr Identity (SMTExpr var qvar fun con field farg lvar) = con

type EmField Identity (SMTExpr var qvar fun con field farg lvar) = field

type EmFunArg Identity (SMTExpr var qvar fun con field farg lvar) = farg

type EmLVar Identity (SMTExpr var qvar fun con field farg lvar) = lvar

encodeExpr :: Backend b => SMTExpr (Var b) (QVar b) (Fun b) (Constr b) (Field b) (FunArg b) (LVar b) tp -> SMT b (Expr b tp)

decodeExpr :: Backend b => Expr b tp -> SMT b (SMTExpr (Var b) (QVar b) (Fun b) (Constr b) (Field b) (FunArg b) (LVar b) tp)

data AnalyzedExpr i e tp

Constructors

AnalyzedExpr (Maybe (Expression (ExVar i e) (ExQVar i e) (ExFun i e) (ExConstr i e) (ExField i e) (ExFunArg i e) (ExLVar i e) (AnalyzedExpr i e) tp)) (e tp)

analyze' :: Extract i e => i -> e tp -> AnalyzedExpr i e tp

analyze :: Backend b => Expr b tp -> SMT b (AnalyzedExpr (BackendInfo b) (Expr b) tp)