Language.SMTLib2.Internals.Embed

Documentation

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

class (Applicative m, GCompare (EmVar m e), GCompare (EmQVar m e), GCompare (EmFun m e), GCompare (EmFunArg m e), GCompare (EmLVar m e)) => Embed m e where

A class of Monads that can be used to form SMTLib expressions. The default instance of this class is the SMT monad, together with its associated Expr type. An interesting instance is the Identity monad with the Value type, which allows evaluation of SMTLib expressions.

Minimal complete definition

embed, embedQuantifier, embedTypeOf

Associated Types

type EmVar m e :: Type -> *

type EmQVar m e :: Type -> *

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

type EmFunArg m e :: Type -> *

type EmLVar m e :: Type -> *

Methods

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

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

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

Instances

Embed Identity Repr

Associated Types

type EmVar (Identity :: * -> *) (Repr :: Type -> *) :: Type -> *

type EmQVar (Identity :: * -> *) (Repr :: Type -> *) :: Type -> *

type EmFun (Identity :: * -> *) (Repr :: Type -> *) :: ([Type], Type) -> *

type EmFunArg (Identity :: * -> *) (Repr :: Type -> *) :: Type -> *

type EmLVar (Identity :: * -> *) (Repr :: Type -> *) :: Type -> *

Methods

embed :: Identity (EmbedExpr Identity Repr tp) -> Identity (Repr tp)

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

embedTypeOf :: Identity (Repr tp -> Repr tp)

Embed Identity Value

Associated Types

type EmVar (Identity :: * -> *) (Value :: Type -> *) :: Type -> *

type EmQVar (Identity :: * -> *) (Value :: Type -> *) :: Type -> *

type EmFun (Identity :: * -> *) (Value :: Type -> *) :: ([Type], Type) -> *

type EmFunArg (Identity :: * -> *) (Value :: Type -> *) :: Type -> *

type EmLVar (Identity :: * -> *) (Value :: Type -> *) :: Type -> *

Methods

embed :: Identity (EmbedExpr Identity Value tp) -> Identity (Value tp)

embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (Value BoolType)

embedTypeOf :: Identity (Value tp -> Repr tp)

Embed Identity (ValueExt Identity)

Associated Types

type EmVar (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: Type -> *

type EmQVar (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: Type -> *

type EmFun (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: ([Type], Type) -> *

type EmFunArg (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: Type -> *

type EmLVar (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: Type -> *

Methods

embed :: Identity (EmbedExpr Identity (ValueExt Identity) tp) -> Identity (ValueExt Identity tp)

embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (ValueExt Identity BoolType)

embedTypeOf :: Identity (ValueExt Identity tp -> Repr tp)

(GCompare Type var, GetType var, GCompare Type qvar, GetType qvar, GCompare ([Type], Type) fun, GetFunType fun, GCompare Type farg, GetType farg, GCompare Type lvar, GetType lvar) => Embed Identity (SMTExpr var qvar fun farg lvar)

Associated Types

type EmVar (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type EmQVar (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type EmFun (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: ([Type], Type) -> *

type EmFunArg (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type EmLVar (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

Methods

embed :: Identity (EmbedExpr Identity (SMTExpr var qvar fun farg lvar) tp) -> Identity (SMTExpr var qvar fun farg lvar tp)

embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (SMTExpr var qvar fun farg lvar BoolType)

embedTypeOf :: Identity (SMTExpr var qvar fun farg lvar tp -> Repr tp)

Backend b => Embed (SMT b) (Expr b)

Associated Types

type EmVar (SMT b :: * -> *) (Expr b :: Type -> *) :: Type -> *

type EmQVar (SMT b :: * -> *) (Expr b :: Type -> *) :: Type -> *

type EmFun (SMT b :: * -> *) (Expr b :: Type -> *) :: ([Type], Type) -> *

type EmFunArg (SMT b :: * -> *) (Expr b :: Type -> *) :: Type -> *

type EmLVar (SMT b :: * -> *) (Expr b :: Type -> *) :: Type -> *

Methods

embed :: SMT b (EmbedExpr (SMT b) (Expr b) tp) -> SMT b (Expr b tp)

embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> SMT b (Expr b BoolType)

embedTypeOf :: SMT b (Expr b tp -> Repr tp)

(Embed m e, Monad m) => Embed (ExceptT err m) e

Associated Types

type EmVar (ExceptT err m :: * -> *) (e :: Type -> *) :: Type -> *

type EmQVar (ExceptT err m :: * -> *) (e :: Type -> *) :: Type -> *

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

type EmFunArg (ExceptT err m :: * -> *) (e :: Type -> *) :: Type -> *

type EmLVar (ExceptT err m :: * -> *) (e :: Type -> *) :: Type -> *

Methods

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

embedQuantifier :: Quantifier -> List Type Repr arg -> (forall a b. (Embed a b, Monad a) => List Type (EmQVar a b) arg -> a (b BoolType)) -> ExceptT err m (e BoolType)

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

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

Minimal complete definition

extract

Associated Types

type ExVar i e :: Type -> *

type ExQVar i e :: Type -> *

type ExFun i e :: ([Type], 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) (ExFunArg i e) (ExLVar i e) e tp)

Instances

(GCompare Type var, GCompare Type qvar, GCompare ([Type], Type) fun, GCompare Type farg, GCompare Type lvar) => Extract () (SMTExpr var qvar fun farg lvar)

Associated Types

type ExVar () (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type ExQVar () (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type ExFun () (SMTExpr var qvar fun farg lvar :: Type -> *) :: ([Type], Type) -> *

type ExFunArg () (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type ExLVar () (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

Methods

extract :: () -> SMTExpr var qvar fun farg lvar tp -> Maybe (Expression (ExVar () (SMTExpr var qvar fun farg lvar)) (ExQVar () (SMTExpr var qvar fun farg lvar)) (ExFun () (SMTExpr var qvar fun farg lvar)) (ExFunArg () (SMTExpr var qvar fun farg lvar)) (ExLVar () (SMTExpr var qvar fun farg lvar)) (SMTExpr var qvar fun farg lvar) tp)

Backend b => Extract (BackendInfo b) (Expr b)

Associated Types

type ExVar (BackendInfo b) (Expr b :: Type -> *) :: Type -> *

type ExQVar (BackendInfo b) (Expr b :: Type -> *) :: Type -> *

type ExFun (BackendInfo b) (Expr b :: Type -> *) :: ([Type], Type) -> *

type ExFunArg (BackendInfo b) (Expr b :: Type -> *) :: Type -> *

type ExLVar (BackendInfo b) (Expr b :: Type -> *) :: Type -> *

Methods

extract :: BackendInfo b -> Expr b tp -> Maybe (Expression (ExVar (BackendInfo b) (Expr b)) (ExQVar (BackendInfo b) (Expr b)) (ExFun (BackendInfo b) (Expr b)) (ExFunArg (BackendInfo b) (Expr b)) (ExLVar (BackendInfo b) (Expr b)) (Expr b) tp)

data UserFun m e sig where

A user-supplied function. Can be used in embedding Values or EvalResults. Since we don't have function equality in haskell, an integer is provided to distinguish functions.

Constructors

UserFun :: List Repr arg -> Repr res -> Int -> (List e arg -> m (e res)) -> UserFun m e '(arg, res)

Instances

GetFunType (UserFun m e)

Methods

getFunType :: UserFun m e (([Type], Type) arg res) -> (List Type Repr arg, Repr res)

GCompare ([Type], Type) (UserFun m e)

Methods

gcompare :: f a -> f b -> GOrdering (UserFun m e) a b

GEq ([Type], Type) (UserFun m e)

Methods

geq :: f a -> f b -> Maybe ((UserFun m e := a) b)

GShow ([Type], Type) (UserFun m e)

Methods

gshowsPrec :: Int -> t a -> ShowS

newtype ValueExt m tp

Constructors

ValueExt

Fields

• valueExt :: EvalResult (UserFun m (ValueExt m)) tp

Instances

GCompare Type (ValueExt m)

Methods

gcompare :: f a -> f b -> GOrdering (ValueExt m) a b

GEq Type (ValueExt m)

Methods

geq :: f a -> f b -> Maybe ((ValueExt m := a) b)

GShow Type (ValueExt m)

Methods

gshowsPrec :: Int -> t a -> ShowS

Embed Identity (ValueExt Identity)

Associated Types

type EmVar (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: Type -> *

type EmQVar (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: Type -> *

type EmFun (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: ([Type], Type) -> *

type EmFunArg (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: Type -> *

type EmLVar (Identity :: * -> *) (ValueExt Identity :: Type -> *) :: Type -> *

Methods

embed :: Identity (EmbedExpr Identity (ValueExt Identity) tp) -> Identity (ValueExt Identity tp)

embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (ValueExt Identity BoolType)

embedTypeOf :: Identity (ValueExt Identity tp -> Repr tp)

GetType (ValueExt m)

Methods

getType :: ValueExt m tp -> Repr tp

type EmVar Identity (ValueExt Identity)

type EmVar Identity (ValueExt Identity) = NoVar

type EmQVar Identity (ValueExt Identity)

type EmQVar Identity (ValueExt Identity) = NoVar

type EmFun Identity (ValueExt Identity)

type EmFun Identity (ValueExt Identity) = UserFun Identity (ValueExt Identity)

type EmFunArg Identity (ValueExt Identity)

type EmFunArg Identity (ValueExt Identity) = NoVar

type EmLVar Identity (ValueExt Identity)

type EmLVar Identity (ValueExt Identity) = NoVar

newtype BackendInfo b

Constructors

BackendInfo b

Instances

Backend b => Extract (BackendInfo b) (Expr b)

Associated Types

type ExVar (BackendInfo b) (Expr b :: Type -> *) :: Type -> *

type ExQVar (BackendInfo b) (Expr b :: Type -> *) :: Type -> *

type ExFun (BackendInfo b) (Expr b :: Type -> *) :: ([Type], Type) -> *

type ExFunArg (BackendInfo b) (Expr b :: Type -> *) :: Type -> *

type ExLVar (BackendInfo b) (Expr b :: Type -> *) :: Type -> *

Methods

extract :: BackendInfo b -> Expr b tp -> Maybe (Expression (ExVar (BackendInfo b) (Expr b)) (ExQVar (BackendInfo b) (Expr b)) (ExFun (BackendInfo b) (Expr b)) (ExFunArg (BackendInfo b) (Expr b)) (ExLVar (BackendInfo b) (Expr b)) (Expr b) tp)

type ExVar (BackendInfo b) (Expr b)

type ExVar (BackendInfo b) (Expr b) = Var b

type ExQVar (BackendInfo b) (Expr b)

type ExQVar (BackendInfo b) (Expr b) = QVar b

type ExFun (BackendInfo b) (Expr b)

type ExFun (BackendInfo b) (Expr b) = Fun b

type ExFunArg (BackendInfo b) (Expr b)

type ExFunArg (BackendInfo b) (Expr b) = FunArg b

type ExLVar (BackendInfo b) (Expr b)

type ExLVar (BackendInfo b) (Expr b) = LVar b

data SMTExpr var qvar fun farg lvar tp where

Constructors

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

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

Instances

(GCompare Type var, GCompare Type qvar, GCompare ([Type], Type) fun, GCompare Type farg, GCompare Type lvar) => Extract () (SMTExpr var qvar fun farg lvar)

Associated Types

type ExVar () (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type ExQVar () (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type ExFun () (SMTExpr var qvar fun farg lvar :: Type -> *) :: ([Type], Type) -> *

type ExFunArg () (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type ExLVar () (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

Methods

extract :: () -> SMTExpr var qvar fun farg lvar tp -> Maybe (Expression (ExVar () (SMTExpr var qvar fun farg lvar)) (ExQVar () (SMTExpr var qvar fun farg lvar)) (ExFun () (SMTExpr var qvar fun farg lvar)) (ExFunArg () (SMTExpr var qvar fun farg lvar)) (ExLVar () (SMTExpr var qvar fun farg lvar)) (SMTExpr var qvar fun farg lvar) tp)

(GCompare Type var, GetType var, GCompare Type qvar, GetType qvar, GCompare ([Type], Type) fun, GetFunType fun, GCompare Type farg, GetType farg, GCompare Type lvar, GetType lvar) => Embed Identity (SMTExpr var qvar fun farg lvar)

Associated Types

type EmVar (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type EmQVar (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type EmFun (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: ([Type], Type) -> *

type EmFunArg (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

type EmLVar (Identity :: * -> *) (SMTExpr var qvar fun farg lvar :: Type -> *) :: Type -> *

Methods

embed :: Identity (EmbedExpr Identity (SMTExpr var qvar fun farg lvar) tp) -> Identity (SMTExpr var qvar fun farg lvar tp)

embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (SMTExpr var qvar fun farg lvar BoolType)

embedTypeOf :: Identity (SMTExpr var qvar fun farg lvar tp -> Repr tp)

(GetType var, GetType qvar, GetFunType fun, GetType farg, GetType lvar) => GetType (SMTExpr var qvar fun farg lvar)

Methods

getType :: SMTExpr var qvar fun farg lvar tp -> Repr tp

type ExVar () (SMTExpr var qvar fun farg lvar)

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

type ExQVar () (SMTExpr var qvar fun farg lvar)

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

type ExFun () (SMTExpr var qvar fun farg lvar)

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

type ExFunArg () (SMTExpr var qvar fun farg lvar)

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

type ExLVar () (SMTExpr var qvar fun farg lvar)

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

type EmVar Identity (SMTExpr var qvar fun farg lvar)

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

type EmQVar Identity (SMTExpr var qvar fun farg lvar)

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

type EmFun Identity (SMTExpr var qvar fun farg lvar)

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

type EmFunArg Identity (SMTExpr var qvar fun farg lvar)

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

type EmLVar Identity (SMTExpr var qvar fun farg lvar)

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

encodeExpr :: Backend b => SMTExpr (Var b) (QVar b) (Fun 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) (FunArg b) (LVar b) tp)

data AnalyzedExpr i e tp

Constructors

AnalyzedExpr (Maybe (Expression (ExVar i e) (ExQVar i e) (ExFun 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)