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


-- | Equational laws for free
--   
--   QuickSpec automatically finds equational properties of your program.
--   
--   Give it an API, i.e. a collection of functions, and it will spit out
--   equations about those functions. For example, given <tt>reverse</tt>,
--   <tt>++</tt> and <tt>[]</tt>, QuickSpec finds six laws:
--   
--   <pre>
--   xs++[] == xs
--   []++xs == xs
--   reverse [] == []
--   (xs++ys)++zs == xs++(ys++zs)
--   reverse (reverse xs) == xs
--   reverse xs++reverse ys == reverse (ys++xs)
--   </pre>
--   
--   All you have to provide is:
--   
--   <ul>
--   <li>Some functions and constants to test. These are the <i>only</i>
--   functions that will appear in the equations.</li>
--   <li>A collection of variables that can appear in the equations
--   (<tt>xs</tt>, <tt>ys</tt> and <tt>zs</tt> in the example above).</li>
--   <li><a>Test.QuickCheck.Arbitrary</a> and <a>Data.Typeable.Typeable</a>
--   instances for the types you want to test.</li>
--   </ul>
--   
--   Consider this a pre-release. Everything is complete but undocumented
--   :) The best place to start is the examples at
--   <a>http://github.com/nick8325/quickspec/tree/master/examples</a>.
--   There is also a paper at
--   <a>http://www.cse.chalmers.se/~nicsma/quickspec.pdf</a>. Everything
--   you need should be in the module <a>Test.QuickSpec</a>.
--   
--   If you want help, email me!
@package quickspec
@version 0.9.2


-- | A union-find data structure.
module Test.QuickSpec.Reasoning.UnionFind
type UF = State S
data Replacement
(:>) :: Int -> Int -> Replacement
newSym :: UF Int
(=:=) :: Int -> Int -> UF (Maybe Replacement)
rep :: Int -> UF Int
evalUF :: S -> UF a -> a
execUF :: S -> UF a -> S
runUF :: S -> UF a -> (a, S)
data S
isRep :: Int -> UF Bool
initial :: Int -> S


-- | A decision procedure for ground equality, based on the paper
--   <a>Proof-producing Congruence Closure</a>.
module Test.QuickSpec.Reasoning.CongruenceClosure
type CC = State S
newSym :: CC Int
(=:=) :: Int -> Int -> CC Bool
(=?=) :: Int -> Int -> CC Bool
rep :: Int -> CC Int
evalCC :: S -> CC a -> a
execCC :: S -> CC a -> S
runCC :: S -> CC a -> (a, S)
($$) :: Int -> Int -> CC Int
data S
funUse :: S -> (IntMap [(Int, Int)])
argUse :: S -> (IntMap [(Int, Int)])
lookup :: S -> IntMap (IntMap Int)
initial :: Int -> S
frozen :: CC a -> CC a
instance Eq FlatEqn
instance Ord FlatEqn


-- | A wrapper around <a>Typeable</a>, to work around:
--   
--   <ol>
--   <li>The lack of an <a>Ord</a> instance in older GHCs,</li>
--   <li>bug #5962 in new GHCs.</li>
--   </ol>
module Test.QuickSpec.Utils.Typeable
data TypeRep

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

-- | Variant for unary type constructors
class Typeable1 (t :: * -> *)

-- | Variant for binary type constructors
class Typeable2 (t :: * -> * -> *)
typeOf :: Typeable a => a -> TypeRep
typeOf1 :: Typeable1 t => t a -> TypeRep
cast :: (Typeable a, Typeable b) => a -> Maybe b
gcast :: (Typeable a, Typeable b) => c a -> Maybe (c b)
mkTyConApp :: TyCon -> [TypeRep] -> TypeRep
typeRepTyCon :: TypeRep -> TyCon
splitTyConApp :: TypeRep -> (TyCon, [TypeRep])
mkFunTy :: TypeRep -> TypeRep -> TypeRep
unTypeRep :: TypeRep -> TypeRep
instance Show TypeRep
instance Ord TypeRep
instance Eq TypeRep


-- | Miscellaneous utility functions.
module Test.QuickSpec.Utils
repeatM :: Monad m => m a -> m [a]
partitionBy :: Ord b => (a -> b) -> [a] -> [[a]]
isSorted :: Ord a => [a] -> Bool
isSortedBy :: Ord b => (a -> b) -> [a] -> Bool
usort :: Ord a => [a] -> [a]
merge :: Ord b => (a -> a -> a) -> (a -> b) -> [a] -> [a] -> [a]
orElse :: Ordering -> Ordering -> Ordering
unbuffered :: IO a -> IO a
spoony :: Eq a => a -> Maybe a


-- | Functions for working with existentially-quantified types and similar.
module Test.QuickSpec.Utils.Typed
data Some f
Some :: (f a) -> Some f
newtype O f g a
O :: f (g a) -> O f g a
unO :: O f g a -> f (g a)
type List = []
type Several f = Some (List O f)
newtype Witnessed a
Witness :: a -> Witnessed a
witness :: Witnessed a -> a
type Witness = Some Witnessed
witnessType :: Witness -> TypeRep
data Tagged a
Tagged :: Witness -> a -> Tagged a
tag :: Tagged a -> Witness
erase :: Tagged a -> a
tagged :: Typeable a => (f a -> b) -> f a -> Tagged b
some :: (forall a. Typeable a => f a -> b) -> Some f -> b
several :: (forall a. Typeable a => [f a] -> b) -> Several f -> b
some2 :: (forall a. Typeable a => f (g a) -> b) -> Some (f O g) -> b
mapSome :: (forall a. Typeable a => f a -> g a) -> Some f -> Some g
mapSome2 :: (forall a. Typeable a => f (g a) -> h (i a)) -> Some (f O g) -> Some (h O i)
mapSomeM :: Monad m => (forall a. Typeable a => f a -> m (g a)) -> Some f -> m (Some g)
someType :: Some f -> TypeRep
someWitness :: Some f -> Witness
splitArrow :: TypeRep -> Maybe (TypeRep, TypeRep)
rightArrow :: TypeRep -> TypeRep
typeRepTyCons :: TypeRep -> [TyCon]
instance Show Witness
instance Ord Witness
instance Eq Witness


-- | A map from types to values. <tt><a>TypeMap</a> f</tt> maps each type
--   <tt>a</tt> to a value of type <tt>f a</tt>.
module Test.QuickSpec.Utils.TypeMap
type TypeMap f = Map TypeRep (Some f)
empty :: TypeMap f
singleton :: Typeable a => f a -> TypeMap f
fromList :: [Some f] -> TypeMap f
toList :: TypeMap f -> [Some f]
lookup :: Typeable a => f a -> a -> TypeMap f -> f a
mapValues :: (forall a. Typeable a => f a -> g a) -> TypeMap f -> TypeMap g
mapValues2 :: (forall a. Typeable a => f (g a) -> h (i a)) -> TypeMap (f O g) -> TypeMap (h O i)


-- | A relation between types and values. <tt><a>TypeRel</a> f</tt> relates
--   each type <tt>a</tt> to a set of values of type <tt>f a</tt>.
module Test.QuickSpec.Utils.TypeRel
type TypeRel f = TypeMap (List O f)
empty :: TypeRel f
singleton :: Typeable a => f a -> TypeRel f
fromList :: [Some f] -> TypeRel f
toList :: TypeRel f -> [Some f]
lookup :: Typeable a => a -> TypeRel f -> [f a]
mapValues :: (forall a. Typeable a => f a -> g a) -> TypeRel f -> TypeRel g
gather :: [Some f] -> Some (List O f)
disperse :: Some (List O f) -> [Some f]
classify :: [Some f] -> [Some (List O f)]


-- | Terms and evaluation.
module Test.QuickSpec.Term
data Symbol
Symbol :: Int -> String -> Int -> Bool -> Bool -> TypeRep -> Symbol
index :: Symbol -> Int
name :: Symbol -> String
symbolArity :: Symbol -> Int
silent :: Symbol -> Bool
undef :: Symbol -> Bool
symbolType :: Symbol -> TypeRep
symbol :: Typeable a => String -> Int -> a -> Symbol
data Term
Var :: Symbol -> Term
Const :: Symbol -> Term
App :: Term -> Term -> Term
showOp :: String -> String
isOp :: String -> Bool
isUndefined :: Term -> Bool
symbols :: Term -> [Symbol]
depth :: Term -> Int
size :: Int -> Term -> Int
holes :: Term -> [(Symbol, Int)]
functor :: Term -> Symbol
args :: Term -> [Term]
funs :: Term -> [Symbol]
vars :: Term -> [Symbol]
mapVars :: (Symbol -> Symbol) -> Term -> Term
data Expr a
Expr :: Term -> {-# UNPACK #-} !Int -> (Valuation -> a) -> Expr a
term :: Expr a -> Term
arity :: Expr a -> {-# UNPACK #-} !Int
eval :: Expr a -> Valuation -> a
data Atom a
Atom :: Symbol -> a -> Atom a
sym :: Atom a -> Symbol
value :: Atom a -> a
data PGen a
PGen :: Gen a -> Gen a -> PGen a
totalGen :: PGen a -> Gen a
partialGen :: PGen a -> Gen a
pgen :: Gen a -> PGen a
type Strategy = forall a. Symbol -> PGen a -> Gen a
newtype Variable a
Variable :: Atom (PGen a) -> Variable a
unVariable :: Variable a -> Atom (PGen a)
newtype Constant a
Constant :: Atom a -> Constant a
unConstant :: Constant a -> Atom a
mapVariable :: (Symbol -> Symbol) -> Variable a -> Variable a
mapConstant :: (Symbol -> Symbol) -> Constant a -> Constant a
newtype Valuation
Valuation :: (forall a. Variable a -> a) -> Valuation
unValuation :: Valuation -> forall a. Variable a -> a
promoteVal :: (forall a. Gen (Variable a -> a)) -> Gen Valuation
valuation :: Strategy -> Gen Valuation
var :: Variable a -> Expr a
con :: Constant a -> Expr a
app :: Expr (a -> b) -> Expr a -> Expr b
instance Typeable1 Expr
instance Eq Term
instance Functor Atom
instance Functor Variable
instance Functor Constant
instance Functor PGen
instance Show (Expr a)
instance Ord (Expr a)
instance Eq (Expr a)
instance Show Term
instance Ord Term
instance Ord Symbol
instance Eq Symbol
instance Show Symbol


-- | A data structure to represent refining a set of terms into equivalence
--   classes by testing.
module Test.QuickSpec.TestTree
data TestTree a
terms :: TestTree a -> [a]
union :: Ord r => [a -> r] -> TestTree a -> TestTree a -> TestTree a
test :: Ord r => [a -> r] -> [a] -> TestTree a
data TestResults a
cutOff :: Int -> Int -> TestTree a -> TestResults a
numTests :: TestResults a -> Int
numResults :: TestResults a -> Int
classes :: Ord a => TestResults a -> [[a]]
reps :: Ord a => TestResults a -> [a]
discrete :: Ord a => [a] -> TestResults a


-- | Functions for constructing and analysing signatures.
module Test.QuickSpec.Signature

-- | The class of things that can be used as a signature.
class Signature a
signature :: Signature a => a -> Sig

-- | A signature.
data Sig
Sig :: TypeRel Constant -> TypeRel Variable -> TypeMap Gen -> TypeMap Gen -> TypeMap Observer -> TypeMap Observer -> TypeMap Witnessed -> First Int -> First Int -> First Int -> First Int -> Sig
constants :: Sig -> TypeRel Constant
variables :: Sig -> TypeRel Variable
total :: Sig -> TypeMap Gen
partial :: Sig -> TypeMap Gen
observers :: Sig -> TypeMap Observer
ords :: Sig -> TypeMap Observer
witnesses :: Sig -> TypeMap Witnessed
maxDepth_ :: Sig -> First Int
maxSize_ :: Sig -> First Int
minTests_ :: Sig -> First Int
maxQuickCheckSize_ :: Sig -> First Int
maxDepth :: Sig -> Int
maxSize :: Sig -> Int
updateDepth :: Int -> Sig -> Sig
updateSize :: Int -> Sig -> Sig
minTests :: Sig -> Int
maxQuickCheckSize :: Sig -> Int
data Used
Used :: Witness -> [Symbol] -> Used
uses :: Sig -> Witness -> Used
data Summary
Summary :: [Symbol] -> [Symbol] -> [Symbol] -> [TypeRep] -> [Used] -> [TypeRep] -> [TypeRep] -> Maybe Int -> Maybe Int -> Maybe Int -> Maybe Int -> Summary
summaryFunctions :: Summary -> [Symbol]
summaryBackground :: Summary -> [Symbol]
summaryVariables :: Summary -> [Symbol]
summaryObserved :: Summary -> [TypeRep]
summaryUninhabited :: Summary -> [Used]
summaryNoVars :: Summary -> [TypeRep]
summaryUntestable :: Summary -> [TypeRep]
summaryDepth :: Summary -> Maybe Int
summarySize :: Summary -> Maybe Int
summaryTests :: Summary -> Maybe Int
summaryQuickCheckSize :: Summary -> Maybe Int
sigToHaskell :: Signature a => a -> String
summarise :: Sig -> Summary
data Observer a
Observer :: (PGen (a -> b)) -> Observer a
observe :: Typeable a => a -> Sig -> Observer a
emptySig :: Sig
constantSig :: Typeable a => Constant a -> Sig
variableSig :: Typeable a => [Variable a] -> Sig
totalSig :: Typeable a => Gen a -> Sig
partialSig :: Typeable a => Gen a -> Sig
observerSig :: Typeable a => Observer a -> Sig
typeSig :: Typeable a => a -> Sig
ordSig :: Typeable a => Observer a -> Sig

-- | If <tt>withDepth n</tt> is in your signature, QuickSpec will consider
--   terms of up to depth <tt>n</tt> (the default is 3).
withDepth :: Int -> Sig

-- | If <tt>withSize n</tt> is in your signature, QuickSpec will consider
--   terms of up to size <tt>n</tt> (the default is 100).
withSize :: Int -> Sig

-- | If <tt>withTests n</tt> is in your signature, QuickSpec will run at
--   least <tt>n</tt> tests (the default is 500).
withTests :: Int -> Sig

-- | If <tt>withQuickCheckSize n</tt> is in your signature, QuickSpec will
--   generate test data of up to size <tt>n</tt> (the default is 20).
withQuickCheckSize :: Int -> Sig

-- | <tt>sig `without` xs</tt> will remove the functions in <tt>xs</tt>
--   from the signature <tt>sig</tt>. Useful when you want to use
--   <a>prelude</a> but exclude some functions. Example:
--   <tt><tt>prelude</tt> (undefined :: A) `without` ["head", "tail"]</tt>.
without :: Signature a => a -> [String] -> Sig
undefinedSig :: Typeable a => String -> a -> Sig
primCon0 :: Typeable a => Int -> String -> a -> Sig
primCon1 :: (Typeable a, Typeable b) => Int -> String -> (a -> b) -> Sig
primCon2 :: (Typeable a, Typeable b, Typeable c) => Int -> String -> (a -> b -> c) -> Sig
primCon3 :: (Typeable a, Typeable b, Typeable c, Typeable d) => Int -> String -> (a -> b -> c -> d) -> Sig
primCon4 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => Int -> String -> (a -> b -> c -> d -> e) -> Sig

-- | A constant.
blind0 :: Typeable a => String -> a -> Sig

-- | A unary function.
blind1 :: (Typeable a, Typeable b) => String -> (a -> b) -> Sig

-- | A binary function.
blind2 :: (Typeable a, Typeable b, Typeable c) => String -> (a -> b -> c) -> Sig

-- | A ternary function.
blind3 :: (Typeable a, Typeable b, Typeable c, Typeable d) => String -> (a -> b -> c -> d) -> Sig

-- | A function of arity 4.
blind4 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => String -> (a -> b -> c -> d -> e) -> Sig
ord :: (Ord a, Typeable a) => a -> Sig
observing :: Observer a -> a -> Observer a

-- | Mark all the functions in a signature as background functions.
--   
--   QuickSpec will only print a law if it contains at least one
--   non-background function.
--   
--   The functions in e.g. <a>prelude</a> are declared as background
--   functions.
background :: Signature a => a -> Sig
primVars0 :: Typeable a => Int -> [String] -> PGen a -> Sig
primVars1 :: (Typeable a, Typeable b) => Int -> [String] -> PGen (a -> b) -> Sig
primVars2 :: (Typeable a, Typeable b, Typeable c) => Int -> [String] -> PGen (a -> b -> c) -> Sig

-- | Similar to <a>vars</a>, but takes a generator as a parameter.
--   
--   <tt>gvars xs (arbitrary :: Gen a)</tt> is the same as <tt>vars xs
--   (undefined :: a)</tt>.
gvars :: Typeable a => [String] -> Gen a -> Sig

-- | Similar to <a>vars</a>, but takes a generator as a parameter.
--   
--   <tt>gvars xs (arbitrary :: Gen a)</tt> is the same as <tt>vars xs
--   (undefined :: a)</tt>.
gvars0 :: Typeable a => [String] -> Gen a -> Sig
gvars1 :: (Typeable a, Typeable b) => [String] -> Gen (a -> b) -> Sig
gvars2 :: (Typeable a, Typeable b, Typeable c) => [String] -> Gen (a -> b -> c) -> Sig

-- | Declare a set of variables of a particular type.
--   
--   For example, <tt>vars ["x","y","z"] (undefined :: Int)</tt> defines
--   three variables, <tt>x</tt>, <tt>y</tt> and <tt>z</tt>, of type
--   <a>Int</a>.
vars :: (Arbitrary a, Typeable a) => [String] -> a -> Sig

-- | Declare a set of variables of a particular type.
--   
--   For example, <tt>vars ["x","y","z"] (undefined :: Int)</tt> defines
--   three variables, <tt>x</tt>, <tt>y</tt> and <tt>z</tt>, of type
--   <a>Int</a>.
vars0 :: (Arbitrary a, Typeable a) => [String] -> a -> Sig
vars1 :: (CoArbitrary a, Typeable a, Arbitrary b, Typeable b) => [String] -> (a -> b) -> Sig
vars2 :: (CoArbitrary a, Typeable a, CoArbitrary b, Typeable b, Arbitrary c, Typeable c) => [String] -> (a -> b -> c) -> Sig

-- | A constant. The same as <a>fun0</a>.
con :: (Ord a, Typeable a) => String -> a -> Sig

-- | A constant. The same as <a>con</a>.
fun0 :: (Ord a, Typeable a) => String -> a -> Sig

-- | A unary function.
fun1 :: (Typeable a, Typeable b, Ord b) => String -> (a -> b) -> Sig

-- | A binary function.
fun2 :: (Typeable a, Typeable b, Typeable c, Ord c) => String -> (a -> b -> c) -> Sig

-- | A ternary function.
fun3 :: (Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => String -> (a -> b -> c -> d) -> Sig

-- | A function of four arguments.
fun4 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Ord e) => String -> (a -> b -> c -> d -> e) -> Sig

-- | An observation function of arity 1.
observer1 :: (Typeable a, Typeable b, Ord b) => (a -> b) -> Sig

-- | An observation function of arity 2.
observer2 :: (Arbitrary a, Typeable a, Typeable b, Typeable c, Ord c) => (a -> b -> c) -> Sig

-- | An observation function of arity 3.
observer3 :: (Arbitrary a, Arbitrary b, Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => (a -> b -> c -> d) -> Sig

-- | An observation function of arity 4.
observer4 :: (Arbitrary a, Arbitrary b, Arbitrary c, Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Ord e) => (a -> b -> c -> d -> e) -> Sig
testable :: Typeable a => Sig -> a -> Bool
constantApplications :: Typeable a => Sig -> Constant a -> [Witness]
constantArgs :: Typeable a => Sig -> Constant a -> [Witness]
constantRes :: Typeable a => Sig -> Constant a -> Witness
saturatedTypes :: Sig -> [Witness]
inhabitedTypes :: Sig -> [Witness]
argumentTypes :: Sig -> [Witness]
variableTypes :: Sig -> [Witness]
witnessArrow :: Typeable a => Sig -> a -> Maybe (Witness, Witness)
lhsWitnesses :: Typeable a => Sig -> a -> [Witness]
findWitness :: Sig -> TypeRep -> Witness
lookupWitness :: Sig -> TypeRep -> Maybe Witness
disambiguate :: Sig -> [Symbol] -> Symbol -> Symbol
constantSymbols :: Sig -> [Symbol]
symbols :: Sig -> [Symbol]
variableSymbols :: Sig -> [Symbol]
instance Typeable Sig
instance Monoid Sig
instance Show Summary
instance Show Used
instance Show Sig
instance Signature a => Signature [a]
instance Signature Sig


-- | Equations.
module Test.QuickSpec.Equation
data Equation
(:=:) :: Term -> Term -> Equation
showEquation :: Sig -> Equation -> String
data TypedEquation a
(:==:) :: Expr a -> Expr a -> TypedEquation a
eraseEquation :: TypedEquation a -> Equation
showTypedEquation :: Sig -> TypedEquation a -> String
equations :: [Several Expr] -> [Some TypedEquation]
instance Eq Equation
instance Ord Equation
instance Show (TypedEquation a)
instance Ord (TypedEquation a)
instance Eq (TypedEquation a)
instance Show Equation


-- | Equational reasoning built on top of congruence closure.
module Test.QuickSpec.Reasoning.NaiveEquationalReasoning
data Context
Context :: S -> Int -> IntMap Universe -> Context
rel :: Context -> S
maxDepth :: Context -> Int
universe :: Context -> IntMap Universe
type Universe = IntMap [Int]
type EQ = ReaderT (Int, IntMap Universe) CC
initial :: Int -> [Symbol] -> [Tagged Term] -> Context
createUniverse :: [Term] -> CC Universe
runEQ :: Context -> EQ a -> (a, Context)
evalEQ :: Context -> EQ a -> a
execEQ :: Context -> EQ a -> Context
liftCC :: CC a -> EQ a
(=?=) :: Term -> Term -> EQ Bool
equal :: Equation -> EQ Bool
(=:=) :: Term -> Term -> EQ Bool
unify :: Equation -> EQ Bool
type Subst = Symbol -> Int
substs :: Term -> IntMap Universe -> Int -> [Subst]
subst :: Subst -> Term -> CC Int
flatten :: Term -> CC Int
get :: EQ S
put :: S -> EQ ()
rep :: Term -> EQ Int

module Test.QuickSpec.Approximate
newtype Plug
Plug :: (forall a. Partial a => Gen a -> Gen a) -> Plug
unPlug :: Plug -> forall a. Partial a => Gen a -> Gen a
type GP = ReaderT Plug Gen
plug :: Partial a => GP a -> GP a
class (Typeable a, Arbitrary a, Eq a) => Partial a where unlifted x = return x
unlifted :: Partial a => a -> GP a
lifted :: Partial a => a -> GP a
approximate :: Partial a => (forall a. Partial a => a -> Maybe a) -> StdGen -> Int -> a -> a
pobserver :: (Ord a, Partial a) => a -> Sig
genPartial :: Partial a => a -> Gen a
pvars :: (Ord a, Partial a) => [String] -> a -> Sig
instance Partial a => Partial [a]
instance Partial Bool
instance Partial Integer
instance Partial Int
instance Partial ()


-- | The "prelude": a standard signature containing useful functions like
--   <a>++</a>, which can be used as background theory.
module Test.QuickSpec.Prelude

-- | Just a type. You can instantiate your polymorphic functions at this
--   type to include them in a signature.
newtype A
A :: Int -> A
newtype B
B :: Int -> B
newtype C
C :: Int -> C

-- | A type with two elements. Use this instead of <tt>A</tt> if testing
--   doesn't work well because the domain of <tt>A</tt> is too large.
data Two
One :: Two
Two :: Two

-- | 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>, <tt>(<a>*</a>)</tt>. Instantiate it with e.g.
--   <tt>arith (undefined :: <a>Int</a>)</tt>.
arith :: (Typeable a, Ord a, Num a, Arbitrary a) => a -> Sig

-- | A signature containing list operations: <tt>[]</tt>, <tt>(:)</tt>,
--   <a>head</a>, <a>tail</a>, <tt>(<a>++</a>)</tt>. Instantiate it with
--   e.g. <tt>lists (undefined :: <a>A</a>)</tt>.
lists :: (Typeable a, Ord a, Arbitrary a) => a -> Sig

-- | A signature containing higher-order functions: <tt>(<a>.</a>)</tt>,
--   <a>id</a>, and some function variables. Useful for testing <a>map</a>.
funs :: (Typeable a, Ord a, Arbitrary a, CoArbitrary a) => a -> Sig

-- | The QuickSpec prelude. Contains boolean, arithmetic and list
--   functions, and some variables. Instantiate it as e.g. <tt>prelude
--   (undefined :: <a>A</a>)</tt>.
prelude :: (Typeable a, Ord a, Arbitrary a) => a -> Sig
instance Typeable A
instance Typeable B
instance Typeable C
instance Typeable Two
instance Eq A
instance Ord A
instance Arbitrary A
instance CoArbitrary A
instance Partial A
instance Eq B
instance Ord B
instance Arbitrary B
instance CoArbitrary B
instance Partial B
instance Eq C
instance Ord C
instance Arbitrary C
instance CoArbitrary C
instance Partial C
instance Eq Two
instance Ord Two
instance CoArbitrary Two
instance Arbitrary Two


-- | The testing loop and term generation of QuickSpec.
module Test.QuickSpec.Generate
terms :: Sig -> TypeRel Expr -> TypeRel Expr
terms' :: Typeable a => Sig -> TypeRel Expr -> a -> [Expr a]
test :: [(Valuation, StdGen, Int)] -> Sig -> TypeMap (List O Expr) -> TypeMap (TestResults O Expr)
test' :: Typeable a => [(Valuation, StdGen, Int)] -> Sig -> [Expr a] -> TestResults (Expr a)
genSeeds :: Int -> IO [(StdGen, Int)]
toValuation :: Strategy -> Sig -> (StdGen, Int) -> (Valuation, StdGen, Int)
generate :: Strategy -> Sig -> IO (TypeMap (TestResults O Expr))
eraseClasses :: TypeMap (TestResults O Expr) -> [[Tagged Term]]


-- | Equational reasoning that deals with partial functions. Only used in
--   HipSpec at the moment.
module Test.QuickSpec.Reasoning.PartialEquationalReasoning
data PEquation
(:\/:) :: Precondition -> Equation -> PEquation
type Precondition = [Symbol]
data Totality
Partial :: Totality
Total :: [Int] -> Totality
Variable :: Totality
showPEquation :: Sig -> PEquation -> String
data Context
Context :: Context -> IntMap Context -> IntMap Symbol -> Context
total :: Context -> Context
partial :: Context -> IntMap Context
vars :: Context -> IntMap Symbol
type PEQ = State Context
initial :: Int -> [(Symbol, Totality)] -> [Tagged Term] -> Context
runPEQ :: Context -> PEQ a -> (a, Context)
evalPEQ :: Context -> PEQ a -> a
execPEQ :: Context -> PEQ a -> Context
liftEQ :: [Int] -> (Maybe Int -> EQ a) -> PEQ [a]
equal :: PEquation -> PEQ Bool
irrelevant :: Equation -> PEQ Precondition
unify :: PEquation -> PEQ Bool
precondition :: Equation -> PEQ Precondition
get :: PEQ Context
put :: Context -> PEQ ()
rep :: Precondition -> Term -> PEQ [Int]
instance Eq Totality
instance Ord Totality
instance Show Totality
instance Show PEquation
instance Ord PEquation
instance Eq PEquation


-- | Test whether functions are total. Used by HipSpec.
module Test.QuickSpec.TestTotality
testTotality :: Sig -> IO [(Symbol, Totality)]
testEquation :: Typeable a => Sig -> Expr a -> Expr a -> Symbol -> IO Bool
always :: Sig -> Gen Bool -> IO Bool


-- | The main implementation of QuickSpec.
module Test.QuickSpec.Main
undefinedsSig :: Sig -> Sig
universe :: [[Tagged Term]] -> [Tagged Term]
prune :: Context -> [Term] -> (a -> Equation) -> [a] -> [a]
defines :: Equation -> Maybe Symbol
definitions :: [Equation] -> [Equation]
runTool :: Signature a => (Sig -> IO ()) -> a -> IO ()
data Target
Target :: Symbol -> Target
NoTarget :: Target
target :: Equation -> Target
innerZip :: [a] -> [[b]] -> [[(a, b)]]

-- | Run QuickSpec on a signature.
quickSpec :: Signature a => a -> IO ()
sampleList :: StdGen -> Int -> [a] -> [a]

-- | Generate random terms from a signature. Useful when QuickSpec is
--   generating too many terms and you want to know what they look like.
sampleTerms :: Signature a => a -> IO ()
instance Eq Target
instance Ord Target


-- | The main QuickSpec module.
--   
--   This will not make sense if you haven't seen some examples! Look at
--   <a>http://github.com/nick8325/quickspec/tree/master/examples</a>, or
--   read the paper at
--   <a>http://www.cse.chalmers.se/~nicsma/quickspec.pdf</a>.
module Test.QuickSpec

-- | Run QuickSpec on a signature.
quickSpec :: Signature a => a -> IO ()

-- | Generate random terms from a signature. Useful when QuickSpec is
--   generating too many terms and you want to know what they look like.
sampleTerms :: Signature a => a -> IO ()

-- | A signature.
data Sig

-- | The class of things that can be used as a signature.
class Signature a
signature :: Signature a => a -> Sig

-- | A constant. The same as <a>fun0</a>.
con :: (Ord a, Typeable a) => String -> a -> Sig

-- | A constant. The same as <a>con</a>.
fun0 :: (Ord a, Typeable a) => String -> a -> Sig

-- | A unary function.
fun1 :: (Typeable a, Typeable b, Ord b) => String -> (a -> b) -> Sig

-- | A binary function.
fun2 :: (Typeable a, Typeable b, Typeable c, Ord c) => String -> (a -> b -> c) -> Sig

-- | A ternary function.
fun3 :: (Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => String -> (a -> b -> c -> d) -> Sig

-- | A function of four arguments.
fun4 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Ord e) => String -> (a -> b -> c -> d -> e) -> Sig

-- | A constant.
blind0 :: Typeable a => String -> a -> Sig

-- | A unary function.
blind1 :: (Typeable a, Typeable b) => String -> (a -> b) -> Sig

-- | A binary function.
blind2 :: (Typeable a, Typeable b, Typeable c) => String -> (a -> b -> c) -> Sig

-- | A ternary function.
blind3 :: (Typeable a, Typeable b, Typeable c, Typeable d) => String -> (a -> b -> c -> d) -> Sig

-- | A function of arity 4.
blind4 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => String -> (a -> b -> c -> d -> e) -> Sig

-- | Declare a set of variables of a particular type.
--   
--   For example, <tt>vars ["x","y","z"] (undefined :: Int)</tt> defines
--   three variables, <tt>x</tt>, <tt>y</tt> and <tt>z</tt>, of type
--   <a>Int</a>.
vars :: (Arbitrary a, Typeable a) => [String] -> a -> Sig

-- | Similar to <a>vars</a>, but takes a generator as a parameter.
--   
--   <tt>gvars xs (arbitrary :: Gen a)</tt> is the same as <tt>vars xs
--   (undefined :: a)</tt>.
gvars :: Typeable a => [String] -> Gen a -> Sig

-- | An observation function of arity 1.
observer1 :: (Typeable a, Typeable b, Ord b) => (a -> b) -> Sig

-- | An observation function of arity 2.
observer2 :: (Arbitrary a, Typeable a, Typeable b, Typeable c, Ord c) => (a -> b -> c) -> Sig

-- | An observation function of arity 3.
observer3 :: (Arbitrary a, Arbitrary b, Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => (a -> b -> c -> d) -> Sig

-- | An observation function of arity 4.
observer4 :: (Arbitrary a, Arbitrary b, Arbitrary c, Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Ord e) => (a -> b -> c -> d -> e) -> Sig

-- | Mark all the functions in a signature as background functions.
--   
--   QuickSpec will only print a law if it contains at least one
--   non-background function.
--   
--   The functions in e.g. <a>prelude</a> are declared as background
--   functions.
background :: Signature a => a -> Sig

-- | If <tt>withDepth n</tt> is in your signature, QuickSpec will consider
--   terms of up to depth <tt>n</tt> (the default is 3).
withDepth :: Int -> Sig

-- | If <tt>withSize n</tt> is in your signature, QuickSpec will consider
--   terms of up to size <tt>n</tt> (the default is 100).
withSize :: Int -> Sig

-- | If <tt>withTests n</tt> is in your signature, QuickSpec will run at
--   least <tt>n</tt> tests (the default is 500).
withTests :: Int -> Sig

-- | If <tt>withQuickCheckSize n</tt> is in your signature, QuickSpec will
--   generate test data of up to size <tt>n</tt> (the default is 20).
withQuickCheckSize :: Int -> Sig

-- | <tt>sig `without` xs</tt> will remove the functions in <tt>xs</tt>
--   from the signature <tt>sig</tt>. Useful when you want to use
--   <a>prelude</a> but exclude some functions. Example:
--   <tt><tt>prelude</tt> (undefined :: A) `without` ["head", "tail"]</tt>.
without :: Signature a => a -> [String] -> Sig

-- | Just a type. You can instantiate your polymorphic functions at this
--   type to include them in a signature.
data A
data B
data C

-- | A type with two elements. Use this instead of <tt>A</tt> if testing
--   doesn't work well because the domain of <tt>A</tt> is too large.
data Two

-- | The QuickSpec prelude. Contains boolean, arithmetic and list
--   functions, and some variables. Instantiate it as e.g. <tt>prelude
--   (undefined :: <a>A</a>)</tt>.
prelude :: (Typeable a, Ord a, Arbitrary a) => a -> 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>, <tt>(<a>*</a>)</tt>. Instantiate it with e.g.
--   <tt>arith (undefined :: <a>Int</a>)</tt>.
arith :: (Typeable a, Ord a, Num a, Arbitrary a) => a -> Sig

-- | A signature containing list operations: <tt>[]</tt>, <tt>(:)</tt>,
--   <a>head</a>, <a>tail</a>, <tt>(<a>++</a>)</tt>. Instantiate it with
--   e.g. <tt>lists (undefined :: <a>A</a>)</tt>.
lists :: (Typeable a, Ord a, Arbitrary a) => a -> Sig

-- | A signature containing higher-order functions: <tt>(<a>.</a>)</tt>,
--   <a>id</a>, and some function variables. Useful for testing <a>map</a>.
funs :: (Typeable a, Ord a, Arbitrary a, CoArbitrary a) => a -> Sig