Safe Haskell | None |
---|

- data AxiomResult a
- (===>) :: Bool -> AxiomResult a -> AxiomResult a
- (=!=) :: a -> a -> AxiomResult a
- data Axiom
- axiom :: Name -> Axiom
- type Arg = Int
- data Op
- op :: Name -> Op
- arg :: Int -> Arg
- but :: Op -> Arg -> Op
- only :: Op -> Arg -> Op
- withConstraint :: Op -> Name -> Op
- withGens :: HasGens a => a -> [Name] -> a
- generate_oi_tests :: [Axiom] -> [Op] -> ExpQ
- generate_axiom's_tests :: Axiom -> [Op] -> ExpQ
- generate_single_test :: Axiom -> Op -> ExpQ
- generate_basic_tests :: [Axiom] -> ExpQ
- show_all_tests :: Maybe (String -> Int -> String -> String) -> [Name] -> [Name] -> ExpQ

# Documentation

data AxiomResult a Source

(===>) :: Bool -> AxiomResult a -> AxiomResult aSource

Adds a condition to an axiom. If the `Bool`

argument is `False`

, the axiom
won't be evaluated. The test will neither count as a failed test, nor as
a successful test. It translates to QuickChecks `==>`

operator.

Example usage:

q4 :: Int -> IntQueue -> AxiomResult Int q4 x q = not (isEmpty q) ===> front (enqueue x q) =!= front q

(=!=) :: a -> a -> AxiomResult aSource

Combine the results of the left- and right-hand sides of an axiom. A simple example is

q1 :: AxiomResult Bool q1 = isEmpty empty =!= True

while an axiom with variables would be written as a function like this:

q2 :: Int -> IntQueue -> AxiomResult Bool q2 x q = isEmpty (enqueue x q) =!= False

An operation. Contains information about the operation's name, which
arguments may be tested (all by default), which generators should be used for
each argument (`arbitrary`

by default) and possibly a constraint function.

`but o i`

excludes the `i`

-th argument from `o`

when generating tests.

Example:

op 'dequeue `but` arg 1

`only o i`

excludes all but the `i`

-th argument from `o`

when generating tests.

Example:

op 'dequeue `only` arg 1

withConstraint :: Op -> Name -> OpSource

`op `

adds a constraint function `withConstraint`

f`f`

to `op`

. `f`

must
take arguments of the same type as `op`

and return a `Bool`

.

withGens :: HasGens a => a -> [Name] -> aSource

Use to specify custom generators for the given operation or axiom. The
`i`

-th element of the list corresponds to the `i`

-th argument. All
generators must be specified. Not using a custom generator for specific
arguments can be achieved by passing `arbitrary`

.

generate_oi_tests :: [Axiom] -> [Op] -> ExpQSource

Generate all operation invariance tests that typecheck. For example, given an operation

f :: A -> A -> B -> C

and an axiom

ax :: D -> AxiomResult A ax x = lhs x =!= rhs x

the following tests are generated:

property $ \y2 y3 -> f (lhs x) y2 y3 == f (rhs x) y2 y3 property $ \y1 y3 -> f y1 (lhs x) y3 == f y1 (rhs x) y3

but not

property $ \y1 y2 -> f y1 y2 (lhs x) == f y1 y2 (rhs x)

because of the types.

All combinations of operations, their respective arguments and axioms are tried.

It returns an expression of type `[Property]`

, i.e.

$(generate_oi_tests axs ops) :: [Property]

generate_axiom's_tests :: Axiom -> [Op] -> ExpQSource

A convenience function for calling `generate_oi_tests`

with only one axiom.

It returns an expression of type `[Property]`

, i.e.

$(generate_axiom's_tests ax ops) :: [Property]

generate_single_test :: Axiom -> Op -> ExpQSource

Calls `generate_oi_tests`

with only the given `Axiom`

and `Op`

. It checks
if there is exactly one test that can be generated and throws an error
otherwise. If multiple applications of the given operation to the given
axioms are possible (i.e. it has multiple arguments with a matching type),
the allowed arguments have to be restricted using `but`

or `only`

.

It returns an expression of type `Property`

, i.e.

$(generate_single_test ax op) :: Property

generate_basic_tests :: [Axiom] -> ExpQSource

show_all_tests :: Maybe (String -> Int -> String -> String) -> [Name] -> [Name] -> ExpQSource

`show_all_tests Nothing axs ops`

returns a `String`

typed expression. Print
the resulting string to get a piece of code, containing one property for each
possible operation invariance test, defined via `generate_single_test`

.

The first argument can replace the default function generating a name for each test, which is

\opn argi ax -> opn ++ show argi ++ "_" ++ ax

. An example output looks like this:

enqueue1_q3 :: Property enqueue1_q3 = $(generate_single_test (axiom 'q3) (op 'enqueue `only` 1))