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


-- | Equational laws for free!
--   
--   QuickSpec takes your Haskell code and, as if by magic, discovers laws
--   about it. You give QuickSpec a collection of Haskell functions;
--   QuickSpec tests your functions with QuickCheck and prints out laws
--   which seem to hold.
--   
--   For example, give QuickSpec the functions <tt>reverse</tt>,
--   <tt>++</tt> and <tt>[]</tt>, and it will find six laws:
--   
--   <pre>
--   reverse [] == []
--   xs ++ [] == xs
--   [] ++ xs == xs
--   reverse (reverse xs) == xs
--   (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
--   reverse xs ++ reverse ys == reverse (ys ++ xs)
--   </pre>
--   
--   QuickSpec can find equational laws as well as conditional equations.
--   All you need to supply are the functions to test, as well as
--   <tt>Ord</tt> and <tt>Arbitrary</tt> instances for QuickSpec to use in
--   testing; the rest is automatic.
--   
--   For information on how to use QuickSpec, see the documentation in the
--   main module, <a>QuickSpec</a>. You can also look in the
--   <tt><a>examples</a></tt> directory, for example at
--   <tt><a>Lists.hs</a></tt>, <tt><a>IntSet.hs</a></tt>, or
--   <tt><a>Parsing.hs</a></tt>. To read about how QuickSpec works, see our
--   paper, <a>Quick specifications for the busy programmer</a>.
@package quickspec
@version 2.2


-- | This module is internal to QuickSpec.
--   
--   Polymorphic types and dynamic values.
module QuickSpec.Internal.Type

-- | The class <a>Typeable</a> allows a concrete representation of a type
--   to be calculated.
class Typeable (a :: k)
class Arity f

-- | Measure the arity.
arity :: Arity f => f -> Int

-- | A (possibly polymorphic) type.
type Type = Term TyCon

-- | A type constructor.
data TyCon

-- | The function type constructor <tt>(-&gt;)</tt>.
Arrow :: TyCon

-- | An ordinary Haskell type constructor.
TyCon :: TyCon -> TyCon

-- | A string. Can be used to represent miscellaneous types that do not
--   really exist in Haskell.
String :: String -> TyCon

-- | Get the outermost <a>TyCon</a> of a <a>Typeable</a>.
tyCon :: Typeable a => proxy a -> TyCon

-- | Construct a <a>TyCon</a> type from a <a>Data.Typeable</a>
--   <a>TyCon</a>.
fromTyCon :: TyCon -> TyCon
data A
data B
data C
data D
data E
class ClassA
class ClassB
class ClassC
class ClassD
class ClassE
class ClassF

-- | A polymorphic type of kind Symbol.
type SymA = "__polymorphic_symbol__"

-- | A type variable.
typeVar :: Type

-- | Check if a type is a type variable.
isTypeVar :: Type -> Bool

-- | Construct a type from a <a>Typeable</a>.
typeOf :: Typeable a => a -> Type

-- | Construct a type from a <a>Typeable</a>.
typeRep :: Typeable (a :: k) => proxy a -> Type

-- | Turn a <a>TyCon</a> into a type.
typeFromTyCon :: TyCon -> Type

-- | Function application for type constructors.
--   
--   For example, <tt>applyType (typeRep (Proxy :: Proxy [])) (typeRep
--   (Proxy :: Proxy Int)) == typeRep (Proxy :: Proxy [Int])</tt>.
applyType :: Type -> Type -> Type

-- | Construct a type from a <a>TypeRep</a>.
fromTypeRep :: TypeRep -> Type

-- | Construct a function type.
arrowType :: [Type] -> Type -> Type

-- | Is a given type a function type?
isArrowType :: Type -> Bool

-- | Decompose a function type into (argument, result).
--   
--   For multiple-argument functions, unpacks one argument.
unpackArrow :: Type -> Maybe (Type, Type)

-- | The arguments of a function type.
typeArgs :: Type -> [Type]

-- | The result of a function type.
typeRes :: Type -> Type

-- | Given the type of a function, returns the type of applying that
--   function to <tt>n</tt> arguments. Crashes if the type does not have
--   enough arguments.
typeDrop :: Int -> Type -> Type

-- | How many arguments does a function take?
typeArity :: Type -> Int

-- | Check if a type is of the form <tt><a>Dict</a> c</tt>.
isDictionary :: Type -> Bool

-- | Check if a type is of the form <tt><a>Dict</a> c</tt>, and if so,
--   return <tt>c</tt>.
getDictionary :: Type -> Maybe Type

-- | Split a type into constraints and normal type.
splitConstrainedType :: Type -> ([Type], Type)

-- | Count how many dictionary arguments a type has.
dictArity :: Type -> Int

-- | Pretty-print a type. Differs from the <a>Pretty</a> instance by
--   printing type variables in lowercase.
pPrintType :: Type -> Doc

-- | A class for things that have a type.
class Typed a

-- | The type.
typ :: Typed a => a -> Type

-- | Types that appear elsewhere in the <a>Typed</a>, for example, types of
--   subterms. Should return everything which is affected by
--   <a>typeSubst</a>.
otherTypesDL :: Typed a => a -> DList Type

-- | Substitute for all type variables.
typeSubst_ :: Typed a => (Var -> Builder TyCon) -> a -> a

-- | Substitute for all type variables in a <a>Typed</a>.
typeSubst :: (Typed a, Substitution s, SubstFun s ~ TyCon) => s -> a -> a

-- | All types that occur in a <a>Typed</a>.
typesDL :: Typed a => a -> DList Type

-- | All type variables that occur in a <a>Typed</a>.
tyVars :: Typed a => a -> [Var]

-- | Cast a <a>Typed</a> to a target type. Succeeds if the target type is
--   an instance of the current type.
cast :: Typed a => Type -> a -> Maybe a

-- | Check if the second argument is an instance of the first argument.
matchType :: Type -> Type -> Maybe (Subst TyCon)

-- | A wrapper for using the <a>Symbolic</a> machinery on types.
newtype TypeView a
TypeView :: a -> TypeView a
[unTypeView] :: TypeView a -> a

-- | Typed things that support function application.
class Typed a => Apply a

-- | Apply a function to its argument.
--   
--   For most instances of <a>Typed</a>, the type of the argument must be
--   exactly equal to the function's argument type. If you want unification
--   to happen, use the <a>Typed</a> instance of <a>Poly</a>.
tryApply :: Apply a => a -> a -> Maybe a

-- | Apply a function to its argument, crashing on failure.
--   
--   For most instances of <a>Typed</a>, the type of the argument must be
--   exactly equal to the function's argument type. If you want unification
--   to happen, use the <a>Typed</a> instance of <a>Poly</a>.
apply :: Apply a => a -> a -> a
infixl 9 `apply`

-- | Check if a function can be applied to its argument.
canApply :: Apply a => a -> a -> Bool

-- | Unify all type variables in a type.
oneTypeVar :: Typed a => a -> a

-- | Replace all type variables with a particular type.
defaultTo :: Typed a => Type -> a -> a

-- | Make a type ground by replacing all type variables with Skolem
--   constants.
skolemiseTypeVars :: Typed a => a -> a

-- | Alpha-rename type variables in a canonical way.
canonicaliseType :: Typed a => a -> a

-- | Represents a forall-quantifier over all the type variables in a type.
--   Wrapping a term in <tt>Poly</tt> normalises the type by alpha-renaming
--   type variables canonically.
--   
--   The <a>Apply</a> instance for <a>Poly</a> does unification to handle
--   applying a polymorphic function.
data Poly a

-- | Convert an ordinary value to a dynamic value.
toPolyValue :: (Applicative f, Typeable a) => a -> Poly (Value f)

-- | Build a <a>Poly</a>.
poly :: Typed a => a -> Poly a
unPoly :: Poly a -> a

-- | Get the polymorphic type of a polymorphic value.
polyTyp :: Typed a => Poly a -> Poly Type

-- | Rename the type variables of the second argument so that they don't
--   overlap with those of the first argument.
polyRename :: (Typed a, Typed b) => a -> Poly b -> b

-- | Rename the type variables of both arguments so that they don't
--   overlap.
polyApply :: (Typed a, Typed b, Typed c) => (a -> b -> c) -> Poly a -> Poly b -> Poly c

-- | Rename the type variables of both arguments so that they don't
--   overlap.
polyPair :: (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)

-- | Rename the type variables of all arguments so that they don't overlap.
polyList :: Typed a => [Poly a] -> Poly [a]

-- | Find the most general unifier of two types.
polyMgu :: Poly Type -> Poly Type -> Maybe (Poly Type)
polyFunctionMgu :: Apply a => Poly a -> Poly a -> Maybe (Poly (a, a))

-- | Dynamic values inside an applicative functor.
--   
--   For example, a value of type <tt>Value Maybe</tt> represents a
--   <tt>Maybe something</tt>.
data Value f

-- | Construct a <a>Value</a>.
toValue :: forall f (a :: *). Typeable a => f a -> Value f

-- | Deconstruct a <a>Value</a>.
fromValue :: forall f (a :: *). Typeable a => Value f -> Maybe (f a)
valueType :: Value f -> Type

-- | Unwrap a value to get at the thing inside, with an existential type.
unwrap :: Value f -> Unwrapped f

-- | The unwrapped value. Consists of the value itself (with an existential
--   type) and functions to wrap it up again.
data Unwrapped f
[In] :: f a -> Wrapper a -> Unwrapped f

-- | Functions for re-wrapping an <a>Unwrapped</a> value.
data Wrapper a
Wrapper :: (forall g. g a -> Value g) -> (forall g. Value g -> g a) -> Wrapper a

-- | Wrap up a value which has the same existential type as this one.
[wrap] :: Wrapper a -> forall g. g a -> Value g

-- | Unwrap a value which has the same existential type as this one.
[reunwrap] :: Wrapper a -> forall g. Value g -> g a

-- | Apply a polymorphic function to a <a>Value</a>.
mapValue :: (forall a. f a -> g a) -> Value f -> Value g

-- | Apply a polymorphic function to a <a>Value</a>.
forValue :: Value f -> (forall a. f a -> g a) -> Value g

-- | Apply a polymorphic function that returns a non-<a>Value</a> result to
--   a <a>Value</a>.
ofValue :: (forall a. f a -> b) -> Value f -> b

-- | Apply a polymorphic function that returns a non-<a>Value</a> result to
--   a <a>Value</a>.
withValue :: Value f -> (forall a. f a -> b) -> b

-- | Apply a polymorphic function to a pair of <a>Value</a>s.
pairValues :: forall f g. Typeable g => (forall a b. f a -> f b -> f (g a b)) -> Value f -> Value f -> Value f
wrapFunctor :: forall f g h. Typeable h => (forall a. f a -> g (h a)) -> Value f -> Value g
unwrapFunctor :: forall f g h. Typeable g => (forall a. f (g a) -> h a) -> Value f -> Value h
bringFunctor :: Functor f => Value f -> f (Value Identity)
instance GHC.Show.Show QuickSpec.Internal.Type.TyCon
instance GHC.Classes.Ord QuickSpec.Internal.Type.TyCon
instance GHC.Classes.Eq QuickSpec.Internal.Type.TyCon
instance Text.PrettyPrint.HughesPJClass.Pretty a => Text.PrettyPrint.HughesPJClass.Pretty (QuickSpec.Internal.Type.Poly a)
instance GHC.Show.Show a => GHC.Show.Show (QuickSpec.Internal.Type.Poly a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (QuickSpec.Internal.Type.Poly a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (QuickSpec.Internal.Type.Poly a)
instance forall k (f :: k -> *). GHC.Show.Show (QuickSpec.Internal.Type.Value f)
instance forall k (f :: k -> *). QuickSpec.Internal.Type.Typed (QuickSpec.Internal.Type.Value f)
instance GHC.Base.Applicative f => QuickSpec.Internal.Type.Apply (QuickSpec.Internal.Type.Value f)
instance QuickSpec.Internal.Type.Typed a => QuickSpec.Internal.Type.Typed (QuickSpec.Internal.Type.Poly a)
instance QuickSpec.Internal.Type.Apply a => QuickSpec.Internal.Type.Apply (QuickSpec.Internal.Type.Poly a)
instance QuickSpec.Internal.Type.Apply QuickSpec.Internal.Type.Type
instance QuickSpec.Internal.Type.Typed a => Twee.Base.Symbolic (QuickSpec.Internal.Type.TypeView a)
instance QuickSpec.Internal.Type.Typed a => Twee.Base.Has (QuickSpec.Internal.Type.TypeView a) QuickSpec.Internal.Type.Type
instance QuickSpec.Internal.Type.Typed QuickSpec.Internal.Type.Type
instance (QuickSpec.Internal.Type.Typed a, QuickSpec.Internal.Type.Typed b) => QuickSpec.Internal.Type.Typed (a, b)
instance (QuickSpec.Internal.Type.Typed a, QuickSpec.Internal.Type.Typed b) => QuickSpec.Internal.Type.Typed (Data.Either.Either a b)
instance QuickSpec.Internal.Type.Typed a => QuickSpec.Internal.Type.Typed [a]
instance Test.QuickCheck.Arbitrary.CoArbitrary QuickSpec.Internal.Type.Type
instance Twee.Term.Labelled QuickSpec.Internal.Type.TyCon
instance Text.PrettyPrint.HughesPJClass.Pretty QuickSpec.Internal.Type.TyCon
instance Twee.Pretty.PrettyTerm QuickSpec.Internal.Type.TyCon
instance Test.QuickCheck.Arbitrary.CoArbitrary (Twee.Term.Core.TermList QuickSpec.Internal.Type.TyCon)


-- | This module is internal to QuickSpec.
--   
--   Typed terms and operations on them.
module QuickSpec.Internal.Term

-- | A sum type. Intended to be used to build the type of function symbols.
--   Comes with instances that are useful for QuickSpec.
data a :+: b
Inl :: a -> (:+:) a b
Inr :: b -> (:+:) a b

-- | A helper for <a>Measure</a>.
newtype MeasureFuns f
MeasureFuns :: Term f -> MeasureFuns f

-- | A standard term ordering - size, skeleton, generality. Satisfies the
--   property: if measure (schema t) &lt; measure (schema u) then t &lt; u.
type Measure f = (Int, Int, Int, Int, MeasureFuns f, Int, [Var])

-- | A type representing functions which may be the identity.
data OrId f
Id :: OrId f
NotId :: f -> OrId f
class Sized a
size :: Sized a => a -> Int

-- | A class for things that contain terms.
class Symbolic f a | a -> f

-- | A different list of all terms contained in the thing.
termsDL :: Symbolic f a => a -> DList (Term f)

-- | Apply a substitution to all terms in the thing.
subst :: Symbolic f a => (Var -> Term f) -> a -> a

-- | A variable, which has a type and a number.
data Var
V :: !Type -> {-# UNPACK #-} !Int -> Var
[var_ty] :: Var -> !Type
[var_id] :: Var -> {-# UNPACK #-} !Int

-- | A typed term.
data Term f
Var :: {-# UNPACK #-} !Var -> Term f
Fun :: !f -> Term f
(:$:) :: !Term f -> !Term f -> Term f

-- | Decompose a term into a head and a list of arguments.
pattern (:@:) :: Term f -> [Term f] -> Term f
match :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
unify :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))

-- | All terms contained in a <a>Symbolic</a>.
terms :: Symbolic f a => a -> [Term f]

-- | All function symbols appearing in a <a>Symbolic</a>, in order of
--   appearance, with duplicates included.
funs :: Symbolic f a => a -> [f]

-- | All variables appearing in a <a>Symbolic</a>, in order of appearance,
--   with duplicates included.
vars :: Symbolic f a => a -> [Var]
getApp :: Term f -> (Term f, [Term f])

-- | Compute the number of a variable which does <i>not</i> appear in the
--   <a>Symbolic</a>.
freeVar :: Symbolic f a => a -> Int

-- | Count how many times a given function symbol occurs.
occ :: (Eq f, Symbolic f a) => f -> a -> Int

-- | Count how many times a given variable occurs.
occVar :: Symbolic f a => Var -> a -> Int

-- | Map a function over variables.
mapVar :: (Var -> Var) -> Term f -> Term f

-- | Map a function over function symbols.
mapFun :: (f -> g) -> Term f -> Term g

-- | Map a function over function symbols.
flatMapFun :: (f -> Term g) -> Term f -> Term g

-- | Eliminate the identity function from a term.
eliminateId :: Term (OrId f) -> Maybe (Term f)

-- | Find all subterms of a term. Includes the term itself.
subterms :: Term f -> [Term f]

-- | Find all subterms of a term. Does not include the term itself.
properSubterms :: Term f -> [Term f]
subtermsFO :: Term f -> [Term f]
properSubtermsFO :: Term f -> [Term f]

-- | Renames variables so that they appear in a canonical order. Also makes
--   sure that variables of different types have different numbers.
canonicalise :: Symbolic fun a => a -> a

-- | Evaluate a term, given a valuation for variables and function symbols.
evalTerm :: (Typed fun, Apply a, Monad m) => (Var -> m a) -> (fun -> m a) -> Term fun -> m a
depth :: Term f -> Int

-- | Compute the term ordering for a term.
measure :: (Sized f, Typed f) => Term f -> Measure f

-- | A helper for <a>Measure</a>.
compareFuns :: Ord f => Term f -> Term f -> Ordering

-- | Pretty printing class. The precedence level is used in a similar way
--   as in the <a>Show</a> class. Minimal complete definition is either
--   <a>pPrintPrec</a> or <a>pPrint</a>.
class Pretty a
pPrintPrec :: Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrint :: Pretty a => a -> Doc
pPrintList :: Pretty a => PrettyLevel -> [a] -> Doc

-- | A hack for encoding Horn clauses. See <a>Score</a>. The default
--   implementation of <a>hasEqualsBonus</a> should work OK.
class EqualsBonus f

-- | Print a value to the console.
prettyPrint :: Pretty a => a -> IO ()

-- | A class for customising the printing of function symbols.
class Pretty f => PrettyTerm f

-- | The style of the function symbol. Defaults to <a>curried</a>.
termStyle :: PrettyTerm f => f -> TermStyle

-- | Defines how to print out a function symbol.
newtype TermStyle
TermStyle :: (forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc) -> TermStyle

-- | Renders a function application. Takes the following arguments in this
--   order: Pretty-printing level, current precedence, pretty-printed
--   function symbol and list of arguments to the function.
[pPrintTerm] :: TermStyle -> forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc
instance GHC.Generics.Generic QuickSpec.Internal.Term.Var
instance GHC.Show.Show QuickSpec.Internal.Term.Var
instance GHC.Classes.Ord QuickSpec.Internal.Term.Var
instance GHC.Classes.Eq QuickSpec.Internal.Term.Var
instance Data.Traversable.Traversable QuickSpec.Internal.Term.Term
instance Data.Foldable.Foldable QuickSpec.Internal.Term.Term
instance GHC.Base.Functor QuickSpec.Internal.Term.Term
instance GHC.Show.Show f => GHC.Show.Show (QuickSpec.Internal.Term.Term f)
instance GHC.Classes.Ord f => GHC.Classes.Ord (QuickSpec.Internal.Term.Term f)
instance GHC.Classes.Eq f => GHC.Classes.Eq (QuickSpec.Internal.Term.Term f)
instance (GHC.Classes.Ord a, GHC.Classes.Ord b) => GHC.Classes.Ord (a QuickSpec.Internal.Term.:+: b)
instance (GHC.Classes.Eq a, GHC.Classes.Eq b) => GHC.Classes.Eq (a QuickSpec.Internal.Term.:+: b)
instance (QuickSpec.Internal.Term.Sized fun1, QuickSpec.Internal.Term.Sized fun2) => QuickSpec.Internal.Term.Sized (fun1 QuickSpec.Internal.Term.:+: fun2)
instance (QuickSpec.Internal.Type.Typed fun1, QuickSpec.Internal.Type.Typed fun2) => QuickSpec.Internal.Type.Typed (fun1 QuickSpec.Internal.Term.:+: fun2)
instance (Text.PrettyPrint.HughesPJClass.Pretty fun1, Text.PrettyPrint.HughesPJClass.Pretty fun2) => Text.PrettyPrint.HughesPJClass.Pretty (fun1 QuickSpec.Internal.Term.:+: fun2)
instance (Twee.Pretty.PrettyTerm fun1, Twee.Pretty.PrettyTerm fun2) => Twee.Pretty.PrettyTerm (fun1 QuickSpec.Internal.Term.:+: fun2)
instance GHC.Classes.Ord f => GHC.Classes.Eq (QuickSpec.Internal.Term.MeasureFuns f)
instance GHC.Classes.Ord f => GHC.Classes.Ord (QuickSpec.Internal.Term.MeasureFuns f)
instance QuickSpec.Internal.Term.Sized f => QuickSpec.Internal.Term.Sized (QuickSpec.Internal.Term.Term f)
instance QuickSpec.Internal.Term.Symbolic f (QuickSpec.Internal.Term.Term f)
instance QuickSpec.Internal.Term.Symbolic f a => QuickSpec.Internal.Term.Symbolic f [a]
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (QuickSpec.Internal.Term.Term f)
instance QuickSpec.Internal.Type.Typed f => QuickSpec.Internal.Type.Typed (QuickSpec.Internal.Term.Term f)
instance (Twee.Pretty.PrettyTerm f, QuickSpec.Internal.Type.Typed f) => QuickSpec.Internal.Type.Apply (QuickSpec.Internal.Term.Term f)
instance Test.QuickCheck.Arbitrary.CoArbitrary QuickSpec.Internal.Term.Var
instance QuickSpec.Internal.Type.Typed QuickSpec.Internal.Term.Var
instance Text.PrettyPrint.HughesPJClass.Pretty QuickSpec.Internal.Term.Var


-- | The main QuickSpec module, with internal stuff exported. For QuickSpec
--   hackers only.
module QuickSpec.Internal

-- | Run QuickSpec. See the documentation at the top of this file.
quickSpec :: Signature sig => sig -> IO ()

-- | Run QuickSpec, returning the list of discovered properties.
quickSpecResult :: Signature sig => sig -> IO [Prop (Term Constant)]

-- | Add some properties to the background theory.
addBackground :: [Prop (Term Constant)] -> Sig

-- | A signature.
newtype Sig
Sig :: (Context -> Config -> Config) -> Sig
[unSig] :: Sig -> Context -> Config -> Config
data Context
Context :: Int -> [String] -> Context

-- | A class of things that can be used as a QuickSpec signature.
class Signature sig

-- | Convert the thing to a signature.
signature :: Signature sig => sig -> Sig
runSig :: Signature sig => sig -> Context -> Config -> Config

-- | Declare a constant with a given name and value. If the constant you
--   want to use is polymorphic, you can use the types <a>A</a>, <a>B</a>,
--   <a>C</a>, <a>D</a>, <a>E</a> to monomorphise it, for example:
--   
--   <pre>
--   constant "reverse" (reverse :: [A] -&gt; [A])
--   </pre>
--   
--   QuickSpec will then understand that the constant is really
--   polymorphic.
con :: Typeable a => String -> a -> Sig

-- | Add a custom constant.
customConstant :: Constant -> Sig

-- | Type class constraints as first class citizens
type c ==> t = Dict c -> t

-- | Lift a constrained type to a <a>==&gt;</a> type which QuickSpec can
--   work with
liftC :: (c => a) -> c ==> a

-- | Add an instance of a type class to the signature
instanceOf :: forall c. (Typeable c, c) => Sig

-- | Declare a predicate with a given name and value. The predicate should
--   be a function which returns <a>Bool</a>. It will appear in equations
--   just like any other constant, but will also be allowed to appear as a
--   condition.
--   
--   Warning: if the predicate is unlikely to be true for a
--   randomly-generated value, you will get bad-quality test data. In that
--   case, use <a>predicateGen</a> instead.
--   
--   For example:
--   
--   <pre>
--   sig = [
--     <a>con</a> "delete" (<a>delete</a> :: Int -&gt; [Int] -&gt; [Int]),
--     <a>con</a> "insert" (<a>insert</a> :: Int -&gt; [Int] -&gt; [Int]),
--     predicate "member" (member :: Int -&gt; [Int] -&gt; Bool) ]
--   </pre>
predicate :: (Predicateable a, PredicateResult a ~ Bool, Typeable a, Typeable (PredicateTestCase a)) => String -> a -> Sig

-- | Declare a predicate with a given name and value. The predicate should
--   be a function which returns <a>Bool</a>. It will appear in equations
--   just like any other constant, but will also be allowed to appear as a
--   condition. The third argument is a generator for values satisfying the
--   predicate.
--   
--   For example, this declares a predicate that checks if a list is
--   sorted:
--   
--   <pre>
--   predicateGen "sorted" sorted genSortedList
--   </pre>
--   
--   where
--   
--   <pre>
--   sorted :: [a] -&gt; Bool
--   sorted xs = sort xs == xs
--   genSortedList :: Gen [a]
--   genSortedList = sort &lt;$&gt; arbitrary
--   </pre>
predicateGen :: (Predicateable a, Typeable a, Typeable (PredicateTestCase a), HasFriendly (PredicateTestCase a)) => String -> a -> Gen (FriendlyPredicateTestCase a) -> Sig

-- | Declare a new monomorphic type. The type must implement <a>Ord</a> and
--   <a>Arbitrary</a>.
--   
--   If the type does not implement <a>Ord</a>, you can use
--   <a>monoTypeObserve</a> to declare an observational equivalence
--   function. If the type does not implement <a>Arbitrary</a>, you can use
--   <a>generator</a> to declare a custom QuickCheck generator.
--   
--   You do not necessarily need <a>Ord</a> and <a>Arbitrary</a> instances
--   for every type. If there is no <a>Ord</a> (or <a>Observe</a> instance)
--   for a type, you will not get equations between terms of that type. If
--   there is no <a>Arbitrary</a> instance (or generator), you will not get
--   variables of that type.
monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig

-- | Like <a>monoType</a>, but designed to be used with TypeApplications
--   directly.
--   
--   For example, you can add <tt>Foo</tt> to your signature via:
--   
--   <pre>
--   <a>mono</a> @Foo
--   </pre>
mono :: forall a. (Ord a, Arbitrary a, Typeable a) => Sig

-- | Declare a new monomorphic type using observational equivalence. The
--   type must implement <a>Observe</a> and <a>Arbitrary</a>.
monoTypeObserve :: forall proxy test outcome a. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => proxy a -> Sig

-- | Like <a>monoTypeObserve</a>, but designed to be used with
--   TypeApplications directly.
--   
--   For example, you can add <tt>Foo</tt> to your signature via:
--   
--   <pre>
--   <a>monoObserve</a> @Foo
--   </pre>
monoObserve :: forall a test outcome. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => Sig

-- | Declare a new monomorphic type using observational equivalence, saying
--   how you want variables of that type to be named.
monoTypeObserveWithVars :: forall proxy test outcome a. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => [String] -> proxy a -> Sig

-- | Like <a>monoTypeObserveWithVars</a>, but designed to be used with
--   TypeApplications directly.
--   
--   For example, you can add <tt>Foo</tt> to your signature via:
--   
--   <pre>
--   <a>monoObserveVars</a> @Foo ["foo"]
--   </pre>
monoObserveVars :: forall a test outcome. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => [String] -> Sig

-- | Declare a new monomorphic type, saying how you want variables of that
--   type to be named.
monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig

-- | Like <a>monoTypeWithVars</a> designed to be used with TypeApplications
--   directly.
--   
--   For example, you can add <tt>Foo</tt> to your signature via:
--   
--   <pre>
--   <a>monoVars</a> @Foo ["foo"]
--   </pre>
monoVars :: forall a. (Ord a, Arbitrary a, Typeable a) => [String] -> Sig

-- | Customize how variables of a particular type are named.
vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig

-- | Constrain how variables of a particular type may occur in a term. The
--   default value is <tt><a>UpTo</a> 4</tt>.
variableUse :: forall proxy a. Typeable a => VariableUse -> proxy a -> Sig

-- | Declare a typeclass instance. QuickSpec needs to have an <a>Ord</a>
--   and <a>Arbitrary</a> instance for each type you want it to test.
--   
--   For example, if you are testing <tt><a>Map</a> k v</tt>, you will need
--   to add the following two declarations to your signature:
--   
--   <pre>
--   <a>inst</a> (<a>Sub</a> <a>Dict</a> :: (Ord A, Ord B) <a>:-</a> Ord (Map A B))
--   <a>inst</a> (<a>Sub</a> <a>Dict</a> :: (Arbitrary A, Arbitrary B) <a>:-</a> Arbitrary (Map A B))
--   </pre>
--   
--   For a monomorphic type <tt>T</tt>, you can use <a>monoType</a>
--   instead, but if you want to use <a>inst</a>, you can do it like this:
--   
--   <pre>
--   <a>inst</a> (<a>Sub</a> <a>Dict</a> :: () <a>:-</a> Ord T)
--   <a>inst</a> (<a>Sub</a> <a>Dict</a> :: () <a>:-</a> Arbitrary T)
--   </pre>
inst :: (Typeable c1, Typeable c2) => (c1 :- c2) -> Sig

-- | Declare a generator to be used to produce random values of a given
--   type. This will take precedence over any <a>Arbitrary</a> instance.
generator :: Typeable a => Gen a -> Sig

-- | Declare an arbitrary value to be used by instance resolution.
instFun :: Typeable a => a -> Sig
addInstances :: Instances -> Sig
withPrintFilter :: (Prop (Term Constant) -> Bool) -> Sig

-- | Declare some functions as being background functions. These are
--   functions which are not interesting on their own, but which may appear
--   in interesting laws with non-background functions. Declaring
--   background functions may improve the laws you get out.
--   
--   Here is an example, which tests <tt>++</tt> and <tt>length</tt>,
--   giving <tt>0</tt> and <tt>+</tt> as background functions:
--   
--   <pre>
--   main = quickSpec [
--     con "++" ((++) :: [A] -&gt; [A] -&gt; [A]),
--     con "length" (length :: [A] -&gt; Int),
--   
--     background [
--       con "0" (0 :: Int),
--       con "+" ((+) :: Int -&gt; Int -&gt; Int) ] ]
--   </pre>
background :: Signature sig => sig -> Sig

-- | Remove a function or predicate from the signature. Useful in
--   combination with <a>prelude</a> and friends.
without :: Signature sig => sig -> [String] -> Sig

-- | Run QuickCheck on a series of signatures. Tests the functions in the
--   first signature, then adds the functions in the second signature, then
--   adds the functions in the third signature, and so on.
--   
--   This can be useful when you have a core API you want to test first,
--   and a larger API you want to test later. The laws for the core API
--   will be printed separately from the laws for the larger API.
--   
--   Here is an example which first tests <tt>0</tt> and <tt>+</tt> and
--   then adds <tt>++</tt> and <tt>length</tt>:
--   
--   <pre>
--   main = quickSpec (series [sig1, sig2])
--     where
--       sig1 = [
--         con "0" (0 :: Int),
--         con "+" ((+) :: Int -&gt; Int -&gt; Int) ]
--       sig2 = [
--         con "++" ((++) :: [A] -&gt; [A] -&gt; [A]),
--         con "length" (length :: [A] -&gt; Int) ]
--   </pre>
series :: Signature sig => [sig] -> Sig

-- | Set the maximum size of terms to explore (default: 7).
withMaxTermSize :: Int -> Sig
withMaxCommutativeSize :: Int -> Sig

-- | Limit how many different function symbols can occur in a term.
withMaxFunctions :: Int -> Sig

-- | Set how many times to test each discovered law (default: 1000).
withMaxTests :: Int -> Sig

-- | Set the maximum value for QuickCheck's size parameter when generating
--   test data (default: 20).
withMaxTestSize :: Int -> Sig

-- | Set which type polymorphic terms are tested at.
defaultTo :: Typeable a => proxy a -> Sig

-- | Set how QuickSpec should display its discovered equations (default:
--   <tt>ForHumans</tt>).
--   
--   If you'd instead like to turn QuickSpec's output into QuickCheck
--   tests, set this to <tt>ForQuickCheck</tt>.
withPrintStyle :: PrintStyle -> Sig

-- | Set how hard QuickSpec tries to filter out redundant equations
--   (default: no limit).
--   
--   If you experience long pauses when running QuickSpec, try setting this
--   number to 2 or 3.
withPruningDepth :: Int -> Sig

-- | Set the maximum term size QuickSpec will reason about when it filters
--   out redundant equations (default: same as maximum term size).
--   
--   If you get laws you believe are redundant, try increasing this number
--   to 1 or 2 more than the maximum term size.
withPruningTermSize :: Int -> Sig

-- | Set the random number seed used for test case generation. Useful if
--   you want repeatable results.
withFixedSeed :: Int -> Sig

-- | Automatically infer types to add to the universe from available type
--   class instances
withInferInstanceTypes :: Sig

-- | (Experimental) Check that the discovered laws do not imply any false
--   laws
withConsistencyCheck :: Sig

-- | A signature containing boolean functions: <tt>(<a>||</a>)</tt>,
--   <tt>(<a>&amp;&amp;</a>)</tt>, <a>not</a>, <a>True</a>, <a>False</a>.
bools :: Sig

-- | A signature containing arithmetic operations: <tt>0</tt>, <tt>1</tt>,
--   <tt>(<a>+</a>)</tt>. Instantiate it with e.g. <tt>arith (<a>Proxy</a>
--   :: <a>Proxy</a> <a>Int</a>)</tt>.
arith :: forall proxy a. (Typeable a, Ord a, Num a, Arbitrary a) => proxy a -> Sig

-- | A signature containing list operations: <tt>[]</tt>, <tt>(:)</tt>,
--   <tt>(<a>++</a>)</tt>.
lists :: Sig

-- | A signature containing higher-order functions: <tt>(<a>.</a>)</tt> and
--   <a>id</a>. Useful for testing <a>map</a> and similar.
funs :: Sig

-- | The QuickSpec prelude. Contains boolean, arithmetic and list
--   functions, and function composition. For more precise control over
--   what gets included, see <a>bools</a>, <a>arith</a>, <a>lists</a>,
--   <a>funs</a> and <a>without</a>.
prelude :: Sig
instance QuickSpec.Internal.Signature QuickSpec.Internal.Sig
instance QuickSpec.Internal.Signature sig => QuickSpec.Internal.Signature [sig]
instance GHC.Base.Semigroup QuickSpec.Internal.Sig
instance GHC.Base.Monoid QuickSpec.Internal.Sig


-- | The main QuickSpec module. Everything you need to run QuickSpec lives
--   here.
--   
--   To run QuickSpec, you need to tell it which functions to test. We call
--   the list of functions the <i>signature</i>. Here is an example
--   signature, which tells QuickSpec to test the <tt>++</tt>,
--   <tt>reverse</tt> and <tt>[]</tt> functions:
--   
--   <pre>
--   sig = [
--     <a>con</a> "++"      ((++) :: [<a>A</a>] -&gt; [<a>A</a>] -&gt; [<a>A</a>]),
--     <a>con</a> "reverse" (reverse :: [<a>A</a>] -&gt; [<a>A</a>]),
--     <a>con</a> "[]"      ([] :: [<a>A</a>]) ]
--   </pre>
--   
--   The <a>con</a> function, used above, adds a function to the signature,
--   given its name and its value. When declaring polymorphic functions in
--   the signature, we use the types <a>A</a> to <a>E</a> to represent type
--   variables. Having defined this signature, we can say
--   <tt><a>quickSpec</a> sig</tt> to test it and see the discovered
--   equations.
--   
--   If you want to test functions over your own datatypes, those types
--   need to implement <a>Arbitrary</a> and <a>Ord</a> (if the <a>Ord</a>
--   instance is a problem, see <a>Observe</a>). You must also declare
--   those instances to QuickSpec, by including them in the signature. For
--   monomorphic types you can do this using <a>monoType</a>:
--   
--   <pre>
--   data T = ...
--   main = quickSpec [
--     ...,
--     <a>monoType</a> (Proxy :: Proxy T)]
--   </pre>
--   
--   You can only declare monomorphic types with <a>monoType</a>. If you
--   want to test your own polymorphic types, you must explicitly declare
--   <a>Arbitrary</a> and <a>Ord</a> instances using the <a>inst</a>
--   function. You can also use the <a>generator</a> function to use a
--   custom generator instead of the <a>Arbitrary</a> instance for a given
--   type.
--   
--   You can also use QuickSpec to find conditional equations. To do so,
--   you need to include some <i>predicates</i> in the signature. These are
--   functions returning <a>Bool</a> which can appear as conditions in
--   other equations. Declaring a predicate works just like declaring a
--   function, except that you declare it using <a>predicate</a> instead of
--   <a>con</a>.
--   
--   You can also put certain options in the signature. The most useful is
--   <a>withMaxTermSize</a>, which you can use to tell QuickSpec to
--   generate larger equations.
--   
--   The <tt><a>examples</a></tt> directory contains many examples. Here
--   are some interesting ones:
--   
--   <ul>
--   <li><tt><a>Arith.hs</a></tt>: a simple arithmetic example.
--   Demonstrates basic use of QuickSpec.</li>
--   <li><tt><a>Lists.hs</a></tt>: list functions. Demonstrates testing
--   polymorphic functions.</li>
--   <li><tt><a>Sorted.hs</a></tt>: sorting. Demonstrates finding
--   conditional equations.</li>
--   <li><tt><a>IntSet.hs</a></tt>: a few functions from
--   <a>Data.IntSet</a>. Demonstrates testing user-defined datatypes and
--   finding conditional equations.</li>
--   <li><tt><a>PrettyPrinting.hs</a></tt>: pretty printing combinators.
--   Demonstrates testing user-defined datatypes and using observational
--   equality.</li>
--   <li><tt><a>Parsing.hs</a></tt>: parser combinators. Demonstrates
--   testing polymorphic datatypes and using observational equality.</li>
--   </ul>
--   
--   You can also find some larger case studies in our paper, <a>Quick
--   specifications for the busy programmer</a>.
module QuickSpec

-- | Run QuickSpec. See the documentation at the top of this file.
quickSpec :: Signature sig => sig -> IO ()

-- | A signature.
data Sig

-- | A class of things that can be used as a QuickSpec signature.
class Signature sig

-- | Convert the thing to a signature.
signature :: Signature sig => sig -> Sig

-- | Declare a constant with a given name and value. If the constant you
--   want to use is polymorphic, you can use the types <a>A</a>, <a>B</a>,
--   <a>C</a>, <a>D</a>, <a>E</a> to monomorphise it, for example:
--   
--   <pre>
--   constant "reverse" (reverse :: [A] -&gt; [A])
--   </pre>
--   
--   QuickSpec will then understand that the constant is really
--   polymorphic.
con :: Typeable a => String -> a -> Sig

-- | Declare a predicate with a given name and value. The predicate should
--   be a function which returns <a>Bool</a>. It will appear in equations
--   just like any other constant, but will also be allowed to appear as a
--   condition.
--   
--   Warning: if the predicate is unlikely to be true for a
--   randomly-generated value, you will get bad-quality test data. In that
--   case, use <a>predicateGen</a> instead.
--   
--   For example:
--   
--   <pre>
--   sig = [
--     <a>con</a> "delete" (<a>delete</a> :: Int -&gt; [Int] -&gt; [Int]),
--     <a>con</a> "insert" (<a>insert</a> :: Int -&gt; [Int] -&gt; [Int]),
--     predicate "member" (member :: Int -&gt; [Int] -&gt; Bool) ]
--   </pre>
predicate :: (Predicateable a, PredicateResult a ~ Bool, Typeable a, Typeable (PredicateTestCase a)) => String -> a -> Sig

-- | Declare a predicate with a given name and value. The predicate should
--   be a function which returns <a>Bool</a>. It will appear in equations
--   just like any other constant, but will also be allowed to appear as a
--   condition. The third argument is a generator for values satisfying the
--   predicate.
--   
--   For example, this declares a predicate that checks if a list is
--   sorted:
--   
--   <pre>
--   predicateGen "sorted" sorted genSortedList
--   </pre>
--   
--   where
--   
--   <pre>
--   sorted :: [a] -&gt; Bool
--   sorted xs = sort xs == xs
--   genSortedList :: Gen [a]
--   genSortedList = sort &lt;$&gt; arbitrary
--   </pre>
predicateGen :: (Predicateable a, Typeable a, Typeable (PredicateTestCase a), HasFriendly (PredicateTestCase a)) => String -> a -> Gen (FriendlyPredicateTestCase a) -> Sig
data A
data B
data C
data D
data E

-- | Declare a new monomorphic type. The type must implement <a>Ord</a> and
--   <a>Arbitrary</a>.
--   
--   If the type does not implement <a>Ord</a>, you can use
--   <a>monoTypeObserve</a> to declare an observational equivalence
--   function. If the type does not implement <a>Arbitrary</a>, you can use
--   <a>generator</a> to declare a custom QuickCheck generator.
--   
--   You do not necessarily need <a>Ord</a> and <a>Arbitrary</a> instances
--   for every type. If there is no <a>Ord</a> (or <a>Observe</a> instance)
--   for a type, you will not get equations between terms of that type. If
--   there is no <a>Arbitrary</a> instance (or generator), you will not get
--   variables of that type.
monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig

-- | Declare a new monomorphic type using observational equivalence. The
--   type must implement <a>Observe</a> and <a>Arbitrary</a>.
monoTypeObserve :: forall proxy test outcome a. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => proxy a -> Sig

-- | A typeclass for types which support observational equality, typically
--   used for types that have no <a>Ord</a> instance.
--   
--   An instance <tt>Observe test outcome a</tt> declares that values of
--   type <tt>a</tt> can be <i>tested</i> for equality by random testing.
--   You supply a function <tt>observe :: test -&gt; outcome -&gt; a</tt>.
--   Then, two values <tt>x</tt> and <tt>y</tt> are considered equal, if
--   for many random values of type <tt>test</tt>, <tt>observe test x ==
--   observe test y</tt>.
--   
--   The function <a>monoTypeObserve</a> declares a monomorphic type with
--   an observation function. For polymorphic types, use <a>inst</a> to
--   declare the <a>Observe</a> instance.
--   
--   For an example of using observational equality, see
--   <tt><a>PrettyPrinting.hs</a></tt>.
class (Arbitrary test, Ord outcome) => Observe test outcome a | a -> test outcome

-- | Make an observation on a value. Should satisfy the following law: if
--   <tt>x /= y</tt>, then there exists a value of <tt>test</tt> such that
--   <tt>observe test x /= observe test y</tt>.
observe :: Observe test outcome a => test -> a -> outcome

-- | Make an observation on a value. Should satisfy the following law: if
--   <tt>x /= y</tt>, then there exists a value of <tt>test</tt> such that
--   <tt>observe test x /= observe test y</tt>.
observe :: (Observe test outcome a, test ~ (), outcome ~ a) => test -> a -> outcome

-- | Declare a typeclass instance. QuickSpec needs to have an <a>Ord</a>
--   and <a>Arbitrary</a> instance for each type you want it to test.
--   
--   For example, if you are testing <tt><a>Map</a> k v</tt>, you will need
--   to add the following two declarations to your signature:
--   
--   <pre>
--   <a>inst</a> (<a>Sub</a> <a>Dict</a> :: (Ord A, Ord B) <a>:-</a> Ord (Map A B))
--   <a>inst</a> (<a>Sub</a> <a>Dict</a> :: (Arbitrary A, Arbitrary B) <a>:-</a> Arbitrary (Map A B))
--   </pre>
--   
--   For a monomorphic type <tt>T</tt>, you can use <a>monoType</a>
--   instead, but if you want to use <a>inst</a>, you can do it like this:
--   
--   <pre>
--   <a>inst</a> (<a>Sub</a> <a>Dict</a> :: () <a>:-</a> Ord T)
--   <a>inst</a> (<a>Sub</a> <a>Dict</a> :: () <a>:-</a> Arbitrary T)
--   </pre>
inst :: (Typeable c1, Typeable c2) => (c1 :- c2) -> Sig

-- | Declare a generator to be used to produce random values of a given
--   type. This will take precedence over any <a>Arbitrary</a> instance.
generator :: Typeable a => Gen a -> Sig

-- | Customize how variables of a particular type are named.
vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig

-- | Declare a new monomorphic type, saying how you want variables of that
--   type to be named.
monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig

-- | Declare a new monomorphic type using observational equivalence, saying
--   how you want variables of that type to be named.
monoTypeObserveWithVars :: forall proxy test outcome a. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => [String] -> proxy a -> Sig

-- | Constrain how variables of a particular type may occur in a term. The
--   default value is <tt><a>UpTo</a> 4</tt>.
variableUse :: forall proxy a. Typeable a => VariableUse -> proxy a -> Sig

-- | Constrains how variables of a particular type may occur in a term.
data VariableUse

-- | <tt>UpTo n</tt>: terms may contain up to <tt>n</tt> distinct variables
--   of this type (in some cases, laws with more variables may still be
--   found)
UpTo :: Int -> VariableUse

-- | Each variable in the term must be distinct
Linear :: VariableUse

-- | Like <a>monoType</a>, but designed to be used with TypeApplications
--   directly.
--   
--   For example, you can add <tt>Foo</tt> to your signature via:
--   
--   <pre>
--   <a>mono</a> @Foo
--   </pre>
mono :: forall a. (Ord a, Arbitrary a, Typeable a) => Sig

-- | Like <a>monoTypeObserve</a>, but designed to be used with
--   TypeApplications directly.
--   
--   For example, you can add <tt>Foo</tt> to your signature via:
--   
--   <pre>
--   <a>monoObserve</a> @Foo
--   </pre>
monoObserve :: forall a test outcome. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => Sig

-- | Like <a>monoTypeWithVars</a> designed to be used with TypeApplications
--   directly.
--   
--   For example, you can add <tt>Foo</tt> to your signature via:
--   
--   <pre>
--   <a>monoVars</a> @Foo ["foo"]
--   </pre>
monoVars :: forall a. (Ord a, Arbitrary a, Typeable a) => [String] -> Sig

-- | Like <a>monoTypeObserveWithVars</a>, but designed to be used with
--   TypeApplications directly.
--   
--   For example, you can add <tt>Foo</tt> to your signature via:
--   
--   <pre>
--   <a>monoObserveVars</a> @Foo ["foo"]
--   </pre>
monoObserveVars :: forall a test outcome. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => [String] -> Sig

-- | A signature containing list operations: <tt>[]</tt>, <tt>(:)</tt>,
--   <tt>(<a>++</a>)</tt>.
lists :: Sig

-- | A signature containing arithmetic operations: <tt>0</tt>, <tt>1</tt>,
--   <tt>(<a>+</a>)</tt>. Instantiate it with e.g. <tt>arith (<a>Proxy</a>
--   :: <a>Proxy</a> <a>Int</a>)</tt>.
arith :: forall proxy a. (Typeable a, Ord a, Num a, Arbitrary a) => proxy a -> Sig

-- | A signature containing higher-order functions: <tt>(<a>.</a>)</tt> and
--   <a>id</a>. Useful for testing <a>map</a> and similar.
funs :: Sig

-- | A signature containing boolean functions: <tt>(<a>||</a>)</tt>,
--   <tt>(<a>&amp;&amp;</a>)</tt>, <a>not</a>, <a>True</a>, <a>False</a>.
bools :: Sig

-- | The QuickSpec prelude. Contains boolean, arithmetic and list
--   functions, and function composition. For more precise control over
--   what gets included, see <a>bools</a>, <a>arith</a>, <a>lists</a>,
--   <a>funs</a> and <a>without</a>.
prelude :: Sig

-- | Remove a function or predicate from the signature. Useful in
--   combination with <a>prelude</a> and friends.
without :: Signature sig => sig -> [String] -> Sig

-- | Declare some functions as being background functions. These are
--   functions which are not interesting on their own, but which may appear
--   in interesting laws with non-background functions. Declaring
--   background functions may improve the laws you get out.
--   
--   Here is an example, which tests <tt>++</tt> and <tt>length</tt>,
--   giving <tt>0</tt> and <tt>+</tt> as background functions:
--   
--   <pre>
--   main = quickSpec [
--     con "++" ((++) :: [A] -&gt; [A] -&gt; [A]),
--     con "length" (length :: [A] -&gt; Int),
--   
--     background [
--       con "0" (0 :: Int),
--       con "+" ((+) :: Int -&gt; Int -&gt; Int) ] ]
--   </pre>
background :: Signature sig => sig -> Sig

-- | Run QuickCheck on a series of signatures. Tests the functions in the
--   first signature, then adds the functions in the second signature, then
--   adds the functions in the third signature, and so on.
--   
--   This can be useful when you have a core API you want to test first,
--   and a larger API you want to test later. The laws for the core API
--   will be printed separately from the laws for the larger API.
--   
--   Here is an example which first tests <tt>0</tt> and <tt>+</tt> and
--   then adds <tt>++</tt> and <tt>length</tt>:
--   
--   <pre>
--   main = quickSpec (series [sig1, sig2])
--     where
--       sig1 = [
--         con "0" (0 :: Int),
--         con "+" ((+) :: Int -&gt; Int -&gt; Int) ]
--       sig2 = [
--         con "++" ((++) :: [A] -&gt; [A] -&gt; [A]),
--         con "length" (length :: [A] -&gt; Int) ]
--   </pre>
series :: Signature sig => [sig] -> Sig

-- | Type class constraints as first class citizens
type c ==> t = Dict c -> t

-- | Lift a constrained type to a <a>==&gt;</a> type which QuickSpec can
--   work with
liftC :: (c => a) -> c ==> a

-- | Add an instance of a type class to the signature
instanceOf :: forall c. (Typeable c, c) => Sig

-- | Set the maximum size of terms to explore (default: 7).
withMaxTermSize :: Int -> Sig

-- | Set how many times to test each discovered law (default: 1000).
withMaxTests :: Int -> Sig

-- | Set the maximum value for QuickCheck's size parameter when generating
--   test data (default: 20).
withMaxTestSize :: Int -> Sig

-- | Limit how many different function symbols can occur in a term.
withMaxFunctions :: Int -> Sig

-- | Set which type polymorphic terms are tested at.
defaultTo :: Typeable a => proxy a -> Sig

-- | Set how hard QuickSpec tries to filter out redundant equations
--   (default: no limit).
--   
--   If you experience long pauses when running QuickSpec, try setting this
--   number to 2 or 3.
withPruningDepth :: Int -> Sig

-- | Set the maximum term size QuickSpec will reason about when it filters
--   out redundant equations (default: same as maximum term size).
--   
--   If you get laws you believe are redundant, try increasing this number
--   to 1 or 2 more than the maximum term size.
withPruningTermSize :: Int -> Sig

-- | Set the random number seed used for test case generation. Useful if
--   you want repeatable results.
withFixedSeed :: Int -> Sig

-- | Automatically infer types to add to the universe from available type
--   class instances
withInferInstanceTypes :: Sig

-- | Set how QuickSpec should display its discovered equations (default:
--   <tt>ForHumans</tt>).
--   
--   If you'd instead like to turn QuickSpec's output into QuickCheck
--   tests, set this to <tt>ForQuickCheck</tt>.
withPrintStyle :: PrintStyle -> Sig

-- | How QuickSpec should style equations.
data PrintStyle
ForHumans :: PrintStyle
ForQuickCheck :: PrintStyle

-- | (Experimental) Check that the discovered laws do not imply any false
--   laws
withConsistencyCheck :: Sig

-- | Like <a>===</a>, but using the <a>Observe</a> typeclass instead of
--   <a>Eq</a>.
(=~=) :: (Show test, Show outcome, Observe test outcome a) => a -> a -> Property
infix 4 =~=

-- | The class <a>Typeable</a> allows a concrete representation of a type
--   to be calculated.
class Typeable (a :: k)

-- | This is the type of entailment.
--   
--   <tt>a <a>:-</a> b</tt> is read as <tt>a</tt> "entails" <tt>b</tt>.
--   
--   With this we can actually build a category for <a>Constraint</a>
--   resolution.
--   
--   e.g.
--   
--   Because <tt><a>Eq</a> a</tt> is a superclass of <tt><a>Ord</a> a</tt>,
--   we can show that <tt><a>Ord</a> a</tt> entails <tt><a>Eq</a> a</tt>.
--   
--   Because <tt>instance <a>Ord</a> a =&gt; <a>Ord</a> [a]</tt> exists, we
--   can show that <tt><a>Ord</a> a</tt> entails <tt><a>Ord</a> [a]</tt> as
--   well.
--   
--   This relationship is captured in the <a>:-</a> entailment type here.
--   
--   Since <tt>p <a>:-</a> p</tt> and entailment composes, <a>:-</a> forms
--   the arrows of a <a>Category</a> of constraints. However,
--   <a>Category</a> only became sufficiently general to support this
--   instance in GHC 7.8, so prior to 7.8 this instance is unavailable.
--   
--   But due to the coherence of instance resolution in Haskell, this
--   <a>Category</a> has some very interesting properties. Notably, in the
--   absence of <tt>IncoherentInstances</tt>, this category is "thin",
--   which is to say that between any two objects (constraints) there is at
--   most one distinguishable arrow.
--   
--   This means that for instance, even though there are two ways to derive
--   <tt><a>Ord</a> a <a>:-</a> <a>Eq</a> [a]</tt>, the answers from these
--   two paths _must_ by construction be equal. This is a property that
--   Haskell offers that is pretty much unique in the space of languages
--   with things they call "type classes".
--   
--   What are the two ways?
--   
--   Well, we can go from <tt><a>Ord</a> a <a>:-</a> <a>Eq</a> a</tt> via
--   the superclass relationship, and then from <tt><a>Eq</a> a <a>:-</a>
--   <a>Eq</a> [a]</tt> via the instance, or we can go from <tt><a>Ord</a>
--   a <a>:-</a> <a>Ord</a> [a]</tt> via the instance then from
--   <tt><a>Ord</a> [a] <a>:-</a> <a>Eq</a> [a]</tt> through the superclass
--   relationship and this diagram by definition must "commute".
--   
--   Diagrammatically,
--   
--   <pre>
--          Ord a
--      ins /     \ cls
--         v       v
--   Ord [a]     Eq a
--      cls \     / ins
--           v   v
--          Eq [a]
--   </pre>
--   
--   This safety net ensures that pretty much anything you can write with
--   this library is sensible and can't break any assumptions on the behalf
--   of library authors.
newtype a :- b
Sub :: (a => Dict b) -> (:-) a b
infixr 9 :-

-- | Values of type <tt><a>Dict</a> p</tt> capture a dictionary for a
--   constraint of type <tt>p</tt>.
--   
--   e.g.
--   
--   <pre>
--   <a>Dict</a> :: <a>Dict</a> (<a>Eq</a> <a>Int</a>)
--   </pre>
--   
--   captures a dictionary that proves we have an:
--   
--   <pre>
--   instance <a>Eq</a> <a>Int</a>
--   </pre>
--   
--   Pattern matching on the <a>Dict</a> constructor will bring this
--   instance into scope.
data Dict a
[Dict] :: forall a. a => Dict a

-- | <a>Proxy</a> is a type that holds no data, but has a phantom parameter
--   of arbitrary type (or even kind). Its use is to provide type
--   information, even though there is no value available of that type (or
--   it may be too costly to create one).
--   
--   Historically, <tt><a>Proxy</a> :: <a>Proxy</a> a</tt> is a safer
--   alternative to the <tt><a>undefined</a> :: a</tt> idiom.
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy (Void, Int -&gt; Int)
--   Proxy
--   </pre>
--   
--   Proxy can even hold types of higher kinds,
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy Either
--   Proxy
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy Functor
--   Proxy
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy complicatedStructure
--   Proxy
--   </pre>
data Proxy (t :: k)
Proxy :: Proxy (t :: k)

-- | Random generation and shrinking of values.
--   
--   QuickCheck provides <tt>Arbitrary</tt> instances for most types in
--   <tt>base</tt>, except those which incur extra dependencies. For a
--   wider range of <tt>Arbitrary</tt> instances see the
--   <a>quickcheck-instances</a> package.
class Arbitrary a