-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Helper functions to create SMTLib expressions in QuickCheck
--   
--   Helper functions to create SMTLib expressions in QuickCheck
@package smtlib2-quickcheck
@version 1.0

module Language.SMTLib2.QuickCheck
data ExprGen m b var qvar fun farg lvar e tp
ExprGen :: ((forall t. Expression var qvar fun farg lvar e t -> b -> m (e t, b)) -> b -> m (e tp, b)) -> ExprGen m b var qvar fun farg lvar e tp
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 :: Type)
VarSet :: (Set (v tp)) -> VarSet v
data GenContext var qvar fun
GenCtx :: DMap Repr (VarSet var) -> DMap Repr (VarSet qvar) -> DMap Repr (VarSet (AnyFunction fun)) -> GenContext var qvar fun
[allVars] :: GenContext var qvar fun -> DMap Repr (VarSet var)
[allQVars] :: GenContext var qvar fun -> DMap Repr (VarSet qvar)
[allFuns] :: GenContext var qvar fun -> DMap Repr (VarSet (AnyFunction fun))
data AnyFunction f (tp :: Type)
AnyFunction :: (f '(arg, tp)) -> AnyFunction f
data AnyType
AnyType :: (Repr tp) -> AnyType
data AnyTypes
AnyTypes :: (List Repr tps) -> AnyTypes
data AnyNatural
AnyNatural :: (Natural n) -> AnyNatural
data TestExpr var qvar fun farg lvar tp
TestExpr :: (Expression var qvar fun farg lvar (TestExpr var qvar fun farg lvar) tp) -> TestExpr var qvar fun farg lvar tp
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
instance (Data.GADT.Show.GShow var, Data.GADT.Show.GShow qvar, Data.GADT.Show.GShow fun, Data.GADT.Show.GShow farg, Data.GADT.Show.GShow lvar) => Data.GADT.Show.GShow (Language.SMTLib2.QuickCheck.TestExpr var qvar fun farg lvar)
instance (Data.GADT.Show.GShow var, Data.GADT.Show.GShow qvar, Data.GADT.Show.GShow fun, Data.GADT.Show.GShow farg, Data.GADT.Show.GShow lvar) => GHC.Show.Show (Language.SMTLib2.QuickCheck.TestExpr var qvar fun farg lvar tp)
instance GHC.Show.Show Language.SMTLib2.QuickCheck.AnyType
instance (Data.GADT.Compare.GEq var, Data.GADT.Compare.GEq qvar, Data.GADT.Compare.GEq fun, Data.GADT.Compare.GEq farg, Data.GADT.Compare.GEq lvar) => Data.GADT.Compare.GEq (Language.SMTLib2.QuickCheck.TestExpr var qvar fun farg lvar)
instance (Data.GADT.Compare.GEq var, Data.GADT.Compare.GEq qvar, Data.GADT.Compare.GEq fun, Data.GADT.Compare.GEq farg, Data.GADT.Compare.GEq lvar) => GHC.Classes.Eq (Language.SMTLib2.QuickCheck.TestExpr var qvar fun farg lvar tp)