Safe Haskell | None |
---|

The main QuickSpec module.

Look at the introduction (https://github.com/nick8325/quickspec/blob/master/README.asciidoc), read the examples (http://github.com/nick8325/quickspec/tree/master/examples), or read the paper (http://www.cse.chalmers.se/~nicsma/quickspec.pdf) before venturing in here.

- quickSpec :: Signature a => a -> IO ()
- sampleTerms :: Signature a => a -> IO ()
- data Sig
- class Signature a where
- con :: (Ord a, Typeable a) => String -> a -> Sig
- fun0 :: (Ord a, Typeable a) => String -> a -> Sig
- fun1 :: (Typeable a, Typeable b, Ord b) => String -> (a -> b) -> Sig
- fun2 :: (Typeable a, Typeable b, Typeable c, Ord c) => String -> (a -> b -> c) -> Sig
- fun3 :: (Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => String -> (a -> b -> c -> d) -> Sig
- fun4 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Ord e) => String -> (a -> b -> c -> d -> e) -> Sig
- fun5 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f, Ord f) => String -> (a -> b -> c -> d -> e -> f) -> Sig
- blind0 :: forall a. Typeable a => String -> a -> Sig
- blind1 :: forall a b. (Typeable a, Typeable b) => String -> (a -> b) -> Sig
- blind2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => String -> (a -> b -> c) -> Sig
- blind3 :: forall a b c d. (Typeable a, Typeable b, Typeable c, Typeable d) => String -> (a -> b -> c -> d) -> Sig
- blind4 :: forall a b c d e. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => String -> (a -> b -> c -> d -> e) -> Sig
- blind5 :: forall a b c d e f. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f) => String -> (a -> b -> c -> d -> e -> f) -> Sig
- vars :: forall a. (Arbitrary a, Typeable a) => [String] -> a -> Sig
- gvars :: forall a. Typeable a => [String] -> Gen a -> Sig
- observer1 :: (Typeable a, Typeable b, Ord b) => (a -> b) -> Sig
- observer2 :: (Arbitrary a, Typeable a, Typeable b, Typeable c, Ord c) => (a -> b -> c) -> Sig
- observer3 :: (Arbitrary a, Arbitrary b, Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => (a -> b -> c -> d) -> Sig
- 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
- background :: Signature a => a -> Sig
- withDepth :: Int -> Sig
- withSize :: Int -> Sig
- withTests :: Int -> Sig
- withQuickCheckSize :: Int -> Sig
- without :: Signature a => a -> [String] -> Sig
- data A
- data B
- data C
- data Two
- prelude :: (Typeable a, Ord a, Arbitrary a) => a -> Sig
- bools :: Sig
- arith :: forall a. (Typeable a, Ord a, Num a, Arbitrary a) => a -> Sig
- lists :: forall a. (Typeable a, Ord a, Arbitrary a) => a -> Sig
- funs :: forall a. (Typeable a, Ord a, Arbitrary a, CoArbitrary a) => a -> Sig

# Running QuickSpec

sampleTerms :: Signature a => a -> IO ()Source

Generate random terms from a signature. Useful when QuickSpec is generating too many terms and you want to know what they look like.

# The Signature class

The class of things that can be used as a signature.

# Adding functions to a signature

You can add `f`

to the signature by using `"f" `funN` f`

,
where `N`

is the arity of the function. For example,

"&&" `fun2` (&&)

will add the binary function `(`

to the signature.
`&&`

)

If f is polymorphic, you must explicitly give it a monomorphic type.
This module exports types `A`

, `B`

and `C`

for that purpose.

For example:

"++" `fun2` ((++) :: [A] -> [A] -> [A])

The result type of the function must be a member of `Ord`

.
If it isn't, use the `blindN`

family of functions (below) instead.
If you want to get equations over a type that isn't in `Ord`

,
you must use the `observerN`

family of functions (below)
to define an observation function for that type.

fun2 :: (Typeable a, Typeable b, Typeable c, Ord c) => String -> (a -> b -> c) -> SigSource

A binary function.

fun3 :: (Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => String -> (a -> b -> c -> d) -> SigSource

A ternary function.

fun4 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Ord e) => String -> (a -> b -> c -> d -> e) -> SigSource

A function of four arguments.

fun5 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f, Ord f) => String -> (a -> b -> c -> d -> e -> f) -> SigSource

A function of five arguments.

# Adding functions whose results are not in `Ord`

These functions work the same as `funN`

(above),
but don't use `Ord`

to compare the results of the functions.
Instead you can use the `observerN`

family of functions (below)
to define an observation function.

blind2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => String -> (a -> b -> c) -> SigSource

A binary function.

blind3 :: forall a b c d. (Typeable a, Typeable b, Typeable c, Typeable d) => String -> (a -> b -> c -> d) -> SigSource

A ternary function.

blind4 :: forall a b c d e. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => String -> (a -> b -> c -> d -> e) -> SigSource

A function of arity 4.

blind5 :: forall a b c d e f. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f) => String -> (a -> b -> c -> d -> e -> f) -> SigSource

A function of arity 5.

# Adding variables to a signature

vars :: forall a. (Arbitrary a, Typeable a) => [String] -> a -> SigSource

Declare a set of variables of a particular type.

For example, `vars ["x","y","z"] (undefined :: Int)`

defines three variables, `x`

, `y`

and `z`

, of type `Int`

.

gvars :: forall a. Typeable a => [String] -> Gen a -> SigSource

Similar to `vars`

, but takes a generator as a parameter.

`gvars xs (arbitrary :: Gen a)`

is the same as
`vars xs (undefined :: a)`

.

# Observational equality

Use this to define comparison operators for types that have
no `Ord`

instance.

For example, suppose we have a type `Regex`

of regular expressions,
and a matching function `match :: String -> Regex -> Bool`

.
We want our equations to talk about semantic equality of regular
expressions, but we probably won't have an `Ord`

instance that does that.
Instead, we can use `blindN`

to add the regular expression operators
to the signature, and then write

observer2 match

(the `2`

is because `match`

has arity two).
Then, when QuickSpec wants to compare two `Regex`

es, `r1`

and `r2`

, it will generate a random
`String`

`xs`

, and compare `match xs r1`

with `match xs r2`

.

Thus you can use `observerN`

to get laws about things that can't
be directly compared for equality but can be tested.

observer1 :: (Typeable a, Typeable b, Ord b) => (a -> b) -> SigSource

An observation function of arity 1.

observer2 :: (Arbitrary a, Typeable a, Typeable b, Typeable c, Ord c) => (a -> b -> c) -> SigSource

An observation function of arity 2.

observer3 :: (Arbitrary a, Arbitrary b, Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => (a -> b -> c -> d) -> SigSource

An observation function of arity 3.

observer4 :: (Arbitrary a, Arbitrary b, Arbitrary c, Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Ord e) => (a -> b -> c -> d -> e) -> SigSource

An observation function of arity 4.

# Modifying a signature

background :: Signature a => a -> SigSource

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. `prelude`

are declared as background functions.

If `withDepth n`

is in your signature,
QuickSpec will consider terms of up to depth `n`

(the default is 3).

If `withSize n`

is in your signature,
QuickSpec will consider terms of up to size `n`

(the default is 100).

If `withTests n`

is in your signature,
QuickSpec will run at least `n`

tests
(the default is 500).

withQuickCheckSize :: Int -> SigSource

If `withQuickCheckSize n`

is in your signature,
QuickSpec will generate test data of up to size `n`

(the default is 20).

without :: Signature a => a -> [String] -> SigSource

`sig `without` xs`

will remove the functions
in `xs`

from the signature `sig`

.
Useful when you want to use `prelude`

but exclude some functions.
Example:

.
`prelude`

(undefined :: A) `without` ["head", "tail"]

# The standard QuickSpec prelude, to include in your own signatures

Just a type. You can instantiate your polymorphic functions at this type to include them in a signature.

A type with two elements.
Use this instead of `A`

if testing doesn't work well because
the domain of `A`

is too large.