Language.SMTLib2.QuickCheck

Documentation

data ExprGen m b var qvar fun farg lvar e tp

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

newtype VarSet v tp

Constructors

VarSet (Set (v tp))

data GenContext var qvar fun

Constructors

GenCtx

Fields

• allVars :: DMap Repr (VarSet var)
• allQVars :: DMap Repr (VarSet qvar)
• allFuns :: DMap Repr (VarSet (AnyFunction fun))

data AnyFunction f tp

Constructors

AnyFunction (f '(arg, tp))

data AnyType

Constructors

AnyType (Repr tp)

Instances

Show AnyType

Methods

showsPrec :: Int -> AnyType -> ShowS

show :: AnyType -> String

showList :: [AnyType] -> ShowS

data AnyTypes

Constructors

AnyTypes (List Repr tps)

data AnyNatural

Constructors

AnyNatural (Natural n)

data TestExpr var qvar fun farg lvar tp

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)

Methods

geq :: f a -> f b -> Maybe ((TestExpr var qvar fun farg lvar := a) b)

(GShow Type var, GShow Type qvar, GShow ([Type], Type) fun, GShow Type farg, GShow Type lvar) => GShow Type (TestExpr var qvar fun farg lvar)

Methods

gshowsPrec :: Int -> t a -> ShowS

(GEq Type var, GEq Type qvar, GEq ([Type], Type) fun, GEq Type farg, GEq Type lvar) => Eq (TestExpr var qvar fun farg lvar tp)

Methods

(==) :: TestExpr var qvar fun farg lvar tp -> TestExpr var qvar fun farg lvar tp -> Bool

(/=) :: TestExpr var qvar fun farg lvar tp -> TestExpr var qvar fun farg lvar tp -> Bool

(GShow Type var, GShow Type qvar, GShow ([Type], Type) fun, GShow Type farg, GShow Type lvar) => Show (TestExpr var qvar fun farg lvar tp)

Methods

showsPrec :: Int -> TestExpr var qvar fun farg lvar tp -> ShowS

show :: TestExpr var qvar fun farg lvar tp -> String

showList :: [TestExpr var qvar fun farg lvar tp] -> ShowS

type TestExprGen var qvar fun farg lvar tp = ExprGen Identity () var qvar fun farg lvar (TestExpr var qvar fun farg lvar) tp

emptyContext :: GenContext var qvar fun

roundTripTest :: (Backend b, SMTMonad b ~ IO) => GenContext (Var b) (QVar b) (Fun b) -> IO b -> Property

encodeTestExpr :: Backend b => TestExpr (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) tp -> b -> SMTMonad b (Expr b tp, b)

decodeTestExpr :: Backend b => Expr b tp -> b -> TestExpr (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) tp

genTestExpr :: GetFunType fun => Repr tp -> GenContext var qvar fun -> Gen (TestExpr var qvar fun farg lvar tp)

genExpr :: (Monad m, GetFunType fun) => Repr t -> GenContext var qvar fun -> Gen (ExprGen m b var qvar fun farg lvar e t)

genFunction :: Repr tp -> GenContext var qvar fun -> Gen (AnyFunction (Function fun) tp)

genType :: Gen AnyType

genTypes :: Gen AnyTypes

genNatural :: Gen AnyNatural

withAllEqLen :: Repr tp -> Int -> (forall tps. List Repr (tp ': tps) -> a) -> a