Safe Haskell | None |
---|---|
Language | Haskell98 |
Language.SMTLib2.QuickCheck
Documentation
data ExprGen m b var qvar fun farg lvar e tp Source #
Constructors
ExprGen ((forall t. Expression var qvar fun farg lvar e t -> b -> m (e t, b)) -> b -> m (e tp, b)) |
type BackendExprGen b tp = ExprGen (SMTMonad b) b (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) (Expr b) tp Source #
data GenContext var qvar fun Source #
data AnyFunction f tp Source #
Constructors
AnyFunction (f '(arg, tp)) |
data AnyNatural Source #
Constructors
AnyNatural (Natural n) |
data TestExpr var qvar fun farg lvar tp Source #
Constructors
TestExpr (Expression var qvar fun farg lvar (TestExpr var qvar fun farg lvar) tp) |
Instances
(GEq Type var, GEq Type qvar, GEq ([Type], Type) fun, GEq Type farg, GEq Type lvar) => GEq Type (TestExpr var qvar fun farg lvar) Source # | |
(GShow Type var, GShow Type qvar, GShow ([Type], Type) fun, GShow Type farg, GShow Type lvar) => GShow Type (TestExpr var qvar fun farg lvar) Source # | |
(GEq Type var, GEq Type qvar, GEq ([Type], Type) fun, GEq Type farg, GEq Type lvar) => Eq (TestExpr var qvar fun farg lvar tp) Source # | |
(GShow Type var, GShow Type qvar, GShow ([Type], Type) fun, GShow Type farg, GShow Type lvar) => Show (TestExpr var qvar fun farg lvar tp) Source # | |
type TestExprGen var qvar fun farg lvar tp = ExprGen Identity () var qvar fun farg lvar (TestExpr var qvar fun farg lvar) tp Source #
emptyContext :: GenContext var qvar fun Source #
roundTripTest :: (Backend b, SMTMonad b ~ IO) => GenContext (Var b) (QVar b) (Fun b) -> IO b -> Property Source #
encodeTestExpr :: Backend b => TestExpr (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) tp -> b -> SMTMonad b (Expr b tp, b) Source #
decodeTestExpr :: Backend b => Expr b tp -> b -> TestExpr (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) tp Source #
genTestExpr :: GetFunType fun => Repr tp -> GenContext var qvar fun -> Gen (TestExpr var qvar fun farg lvar tp) Source #
genExpr :: (Monad m, GetFunType fun) => Repr t -> GenContext var qvar fun -> Gen (ExprGen m b var qvar fun farg lvar e t) Source #
genFunction :: Repr tp -> GenContext var qvar fun -> Gen (AnyFunction (Function fun) tp) Source #