Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

## Synopsis

- quickSpec :: Signature sig => sig -> IO ()
- quickSpecResult :: Signature sig => sig -> IO [Prop (Term Constant)]
- addBackground :: [Prop (Term Constant)] -> Sig
- newtype Sig = Sig {}
- data Context = Context Int [String]
- class Signature sig where
- runSig :: Signature sig => sig -> Context -> Config -> Config
- con :: Typeable a => String -> a -> Sig
- customConstant :: Constant -> Sig
- type (==>) c t = Dict c -> t
- liftC :: (c => a) -> c ==> a
- instanceOf :: forall c. (Typeable c, c) => Sig
- predicate :: (Predicateable a, Typeable a, Typeable (PredicateTestCase a)) => String -> a -> Sig
- predicateGen :: (Predicateable a, Typeable a, Typeable b, Typeable (PredicateTestCase a)) => String -> a -> (b -> Gen (PredicateTestCase a)) -> Sig
- monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig
- mono :: forall a. (Ord a, Arbitrary a, Typeable a) => Sig
- 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
- monoObserve :: forall a test outcome. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => Sig
- 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
- monoObserveVars :: forall a test outcome. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => [String] -> Sig
- monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig
- monoVars :: forall a. (Ord a, Arbitrary a, Typeable a) => [String] -> Sig
- vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig
- variableUse :: forall proxy a. Typeable a => VariableUse -> proxy a -> Sig
- inst :: (Typeable c1, Typeable c2) => (c1 :- c2) -> Sig
- instFun :: Typeable a => a -> Sig
- addInstances :: Instances -> Sig
- withPrintFilter :: (Prop (Term Constant) -> Bool) -> Sig
- background :: Signature sig => sig -> Sig
- without :: Signature sig => sig -> [String] -> Sig
- series :: Signature sig => [sig] -> Sig
- withMaxTermSize :: Int -> Sig
- withMaxCommutativeSize :: Int -> Sig
- withMaxTests :: Int -> Sig
- withMaxTestSize :: Int -> Sig
- defaultTo :: Typeable a => proxy a -> Sig
- withPrintStyle :: PrintStyle -> Sig
- withPruningDepth :: Int -> Sig
- withPruningTermSize :: Int -> Sig
- withFixedSeed :: Int -> Sig
- withInferInstanceTypes :: Sig
- bools :: Sig
- arith :: forall proxy a. (Typeable a, Ord a, Num a, Arbitrary a) => proxy a -> Sig
- lists :: Sig
- funs :: Sig
- prelude :: Sig

# Documentation

quickSpec :: Signature sig => sig -> IO () Source #

Run QuickSpec. See the documentation at the top of this file.

quickSpecResult :: Signature sig => sig -> IO [Prop (Term Constant)] Source #

Run QuickSpec, returning the list of discovered properties.

addBackground :: [Prop (Term Constant)] -> Sig Source #

Add some properties to the background theory.

customConstant :: Constant -> Sig Source #

Add a custom constant.

liftC :: (c => a) -> c ==> a Source #

Lift a constrained type to a `==>`

type which QuickSpec
can work with

instanceOf :: forall c. (Typeable c, c) => Sig Source #

Add an instance of a type class to the signature

predicate :: (Predicateable a, Typeable a, Typeable (PredicateTestCase a)) => String -> a -> Sig Source #

Declare a predicate with a given name and value.
The predicate should be a function which returns `Bool`

.
It will appear in equations just like any other constant,
but will also be allowed to appear as a condition.

For example:

sig = [`con`

"delete" (`delete`

:: Int -> [Int] -> [Int]),`con`

"insert" (`insert`

:: Int -> [Int] -> [Int]), predicate "member" (member :: Int -> [Int] -> Bool) ]

predicateGen :: (Predicateable a, Typeable a, Typeable b, Typeable (PredicateTestCase a)) => String -> a -> (b -> Gen (PredicateTestCase a)) -> Sig Source #

Declare a predicate with a given name and value.
The predicate should be a function which returns `Bool`

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

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 Source #

monoObserve :: forall a test outcome. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => Sig Source #

Like `monoTypeObserve`

, but designed to be used with TypeApplications directly.

For example, you can add `Foo`

to your signature via:

`monoObserve`

@Foo

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 Source #

Declare a new monomorphic type using observational equivalence, saying how you want variables of that type to be named.

monoObserveVars :: forall a test outcome. (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) => [String] -> Sig Source #

Like `monoTypeObserveWithVars`

, but designed to be used with TypeApplications directly.

For example, you can add `Foo`

to your signature via:

`monoObserveVars`

@Foo ["foo"]

monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig Source #

Declare a new monomorphic type, saying how you want variables of that type to be named.

monoVars :: forall a. (Ord a, Arbitrary a, Typeable a) => [String] -> Sig Source #

Like `monoTypeWithVars`

designed to be used with TypeApplications directly.

For example, you can add `Foo`

to your signature via:

`monoVars`

@Foo ["foo"]

vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig Source #

Customize how variables of a particular type are named.

variableUse :: forall proxy a. Typeable a => VariableUse -> proxy a -> Sig Source #

Constrain how variables of a particular type may occur in a term.
The default value is

.`UpTo`

4

inst :: (Typeable c1, Typeable c2) => (c1 :- c2) -> Sig Source #

Declare a typeclass instance. QuickSpec needs to have an `Ord`

and
| Declare a typeclass instance. QuickSpec needs to have an `Ord`

and
`Arbitrary`

instance for each type you want it to test.

For example, if you are testing

, you will need to add
the following two declarations to your signature:`Map`

k v

`inst`

(`Sub`

`Dict`

:: (Ord A, Ord B)`:-`

Ord (Map A B))`inst`

(`Sub`

`Dict`

:: (Arbitrary A, Arbitrary B)`:-`

Arbitrary (Map A B))

instFun :: Typeable a => a -> Sig Source #

Declare an arbitrary value to be used by instance resolution.

addInstances :: Instances -> Sig Source #

background :: Signature sig => sig -> Sig Source #

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 `++`

and `length`

, giving `0`

and `+`

as
background functions:

main = quickSpec [ con "++" ((++) :: [A] -> [A] -> [A]), con "length" (length :: [A] -> Int), background [ con "0" (0 :: Int), con "+" ((+) :: Int -> Int -> Int) ] ]

without :: Signature sig => sig -> [String] -> Sig Source #

Remove a function or predicate from the signature.
Useful in combination with `prelude`

and friends.

series :: Signature sig => [sig] -> Sig Source #

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 `0`

and `+`

and then adds `++`

and `length`

:

main = quickSpec (series [sig1, sig2]) where sig1 = [ con "0" (0 :: Int), con "+" ((+) :: Int -> Int -> Int) ] sig2 = [ con "++" ((++) :: [A] -> [A] -> [A]), con "length" (length :: [A] -> Int) ]

withMaxTermSize :: Int -> Sig Source #

Set the maximum size of terms to explore (default: 7).

withMaxCommutativeSize :: Int -> Sig Source #

withMaxTests :: Int -> Sig Source #

Set how many times to test each discovered law (default: 1000).

withMaxTestSize :: Int -> Sig Source #

Set the maximum value for QuickCheck's size parameter when generating test data (default: 20).

withPrintStyle :: PrintStyle -> Sig Source #

Set how QuickSpec should display its discovered equations (default: `ForHumans`

).

If you'd instead like to turn QuickSpec's output into QuickCheck tests, set
this to `ForQuickCheck`

.

withPruningDepth :: Int -> Sig Source #

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.

withPruningTermSize :: Int -> Sig Source #

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.

withFixedSeed :: Int -> Sig Source #

Set the random number seed used for test case generation. Useful if you want repeatable results.

withInferInstanceTypes :: Sig Source #

Automatically infer types to add to the universe from available type class instances