diff --git a/README b/README deleted file mode 100644 --- a/README +++ /dev/null @@ -1,1 +0,0 @@ -cabal install and look at the examples directory. diff --git a/README.asciidoc b/README.asciidoc new file mode 100644 --- /dev/null +++ b/README.asciidoc @@ -0,0 +1,410 @@ +:replacements.DOCS: http://hackage.haskell.org/package/quickspec-0.9.5/docs/Test-QuickSpec.html +:replacements.PAPER: http://www.cse.chalmers.se/~nicsma/papers/quickspec.pdf +:replacements.FUN: http://hackage.haskell.org/package/quickspec-0.9.5/docs/Test-QuickSpec.html#v: +:replacements.TYPE: http://hackage.haskell.org/package/quickspec-0.9.5/docs/Test-QuickSpec.html#t: +:replacements.EXAMPLE: link:examples/ + +QuickSpec: equational laws for free! +==================================== + +Ever get that nagging feeling that your code must satisfy some +algebraic properties, but not sure what they are? Want to write some +QuickCheck properties, but not sure where to start? QuickSpec might be +for you! Give it your program -- QuickSpec will find the laws it obeys. + +QuickSpec takes any hodgepodge of functions, and tests those functions +to work out the relationship between them. It then spits out what it +discovered as a list of equations. + +Give QuickSpec `reverse`, `++` and `[]`, for example, and it will find +six laws: + +------------------------------------------------ +xs++[] == xs +[]++xs == xs +(xs++ys)++zs == xs++(ys++zs) +reverse [] == [] +reverse (reverse xs) == xs +reverse xs++reverse ys == reverse (ys++xs) +------------------------------------------------ + +All the laws you would expect to hold, and nothing more -- and all +discovered automatically! Brill! + +Where's the catch? While QuickSpec is pretty nifty, it isn't magic, +and has a number of limitations: + +* QuickSpec can only discover _equations_, not other kinds of laws. + Luckily, equations cover a lot of what you would normally want to + say about Haskell programs. Often, even if a law you want isn't + equational, QuickSpec will discover equational special cases of that + law which suggest the general case. +* You have to tell QuickSpec exactly which functions and constants it + should consider when generating laws. In the example above, we gave + `reverse`, `++` and `[]`, and those are the _only_ functions that + appear in the six equations. For example, we don't get the equation + `(x:xs)++ys == x:(xs++ys)`, because we didn't include +:+ in the + functions we gave to QuickSpec. A large part of using QuickSpec + effectively is choosing which functions to consider in laws. +* QuickSpec exhaustively enumerates terms, so it will only discover + equations about small(ish) terms -- in fact, terms up to a fixed + depth. You can adjust the maximum depth but, as QuickSpec exhaustively + enumerates terms, there is an exponential blowup as you increase the + depth. Likewise, there is an exponential blowup as you give QuickSpec + more functions to consider (though it doesn't blow up as badly as + you might think!) +* QuickSpec only tests the laws, it doesn't try to prove them. + So while the generated laws are very likely to be true, there is + still a chance that they are false, especially if your test data + generation is not up to scratch. + +Despite these limitations, QuickSpec works well on many examples. + +The rest of this +README+ introduces QuickSpec through a couple of short examples. +You can look at the bottom of this file for links to more examples, Haddock documentation and our paper about QuickSpec. + +Installing +---------- + +Install QuickSpec in the usual way -- `cabal install quickspec`. + +Booleans -- the basics +---------------------- + +Let's start by testing some boolean operators. + +To run QuickSpec, we must define a _signature_, which specifies which +functions we want to test, together with the variables that can appear +in the generated equations. Here is our signature: + +[source,haskell] +------------------------------------------------ +bools = [ + ["x", "y", "z"] `vars` (undefined :: Bool), + + "||" `fun2` (||), + "&&" `fun2` (&&), + "not" `fun1` not, + "True" `fun0` True, + "False" `fun0` False] +------------------------------------------------ + +In the signature, we define three variables (+x+, +y+ and +z+) of type ++Bool+, using the FUNvars[`vars`] combinator, which takes two +parameters: a list of variable names, and the type we want those +variables to have. We also give give QuickSpec the functions +||+, ++&&+, +not+, +True+ and +False+, using the +FUNfun0[`fun0`]/FUNfun1[`fun1`]/FUNfun2[`fun2`] combinators. These +take two parameters: the name of the function, and the function +itself. The integer, +0+, +1+ or +2+ here, is the arity of the +function. + +Having written this signature, we can invoke QuickSpec just by calling +the function FUNquickSpec[`quickSpec`]: + +[source,haskell] +------------------------------------------------ +import Test.QuickSpec hiding (bools) +main = quickSpec bools +------------------------------------------------ + +You can find this code in EXAMPLEBools.hs[examples/Bools.hs] in +the QuickSpec distribution. Go on, run it! (Compile it or else it'll go slow.) +You will see that QuickSpec prints out: + +1. The signature it's testing, i.e. the types of all functions and + variables. If something fishy is happening, check that the + functions and types match up with what you expect! QuickSpec will + also print a warning here if something seems fishy about the + signature, e.g. if there are no variables of a certain type. +2. A summary of how much testing it did. +3. The equations it found -- the exciting bit! + The equations are grouped according to which function they + talk about, with equations that relate several functions at the end. + +Peering through what QuickSpec found, you should see the familiar laws +of Boolean algebra. The only oddity is the equation +x||(y||z) == +y||(x||z)+. This is QuickSpec's rather eccentric way of expressing +that +||+ is associative -- in the presence of the law +x||y == y||x+, +it's equivalent to associativity, and QuickSpec happens to choose this +formulation rather than the more traditional one. All the other laws +are just as we would expect, though. Not bad for 5 minutes' work! + +Lists -- polymorphic functions and the prelude +---------------------------------------------- + +Now let's try testing some list functions -- perhaps just `reverse`, +`++` and `[]`. We might start by writing a signature by analogy with +the earlier booleans example: + +[source,haskell] +---- +lists = [ + ["xs", "ys", "zs"] `vars` (undefined :: [a]), + + "[]" `fun0` [], + "reverse" `fun1` reverse, + "++" `fun2` (++)] +---- + +Unfortunately, QuickSpec only supports _monomorphic_ functions. The +functions and variables in the `lists` signature are polymorphic, +and GHC complains: + +---- +No instance for (Arbitrary a0) arising from a use of `vars' +The type variable `a0' is ambiguous +---- + +The solution is to monomorphise the signature ourselves. QuickSpec +provides types called TYPEA[`A`], TYPEB[`B`] and TYPEC[`C`] for that +purpose, so we simply specialise all type variables to TYPEA[`A`]: + +[source,haskell] +---- +lists = [ + ["xs", "ys", "zs"] `vars` (undefined :: [A]), + + "[]" `fun0` ([] :: [A]), + "reverse" `fun1` (reverse :: [A] -> [A]), + "++" `fun2` ((++) :: [A] -> [A] -> [A])] +---- + +Having done that, we get the six laws from the beginning of this file. + +Perhaps we now decide we want laws about `length` too. We want to keep +our existing list functions in the signature, so that we get laws +relating them to `length`, but on the other hand we only want to see +new laws, i.e. the ones that mention `length`. We can do this by +marking the existing functions as _background functions_, and the +resulting signature looks as follows: + +[source,haskell] +---- +lists = [ + ["xs", "ys", "zs"] `vars` (undefined :: [A]), + + background [ + "[]" `fun0` ([] :: [A]), + "reverse" `fun1` (reverse :: [A] -> [A]), + "++" `fun2` ((++) :: [A] -> [A] -> [A])], + "length" `fun1` (length :: [A] -> Int)] +---- + +QuickSpec will only print an equation if it involves at least one +non-background function, in this case `length`. Running QuickSpec +again we get the following two laws: + +---- +length (reverse xs) == length xs +length (xs++ys) == length (ys++xs) +---- + +The first equation is all very well and good, but the second one is a +bit unsatisfying. Wouldn't we rather get +`length (xs++ys) = length xs + length ys`? To get that equation, we need to add +`(+) :: Int -> Int -> Int` to the signature. Adding it as a background +function gives us the law we want. + +You often need a wide variety of background functions to get good +equations out of QuickSpec, and it gets a bit tedious declaring them +all by hand. To help you with this QuickSpec provides a _prelude_, a +predefined set of background functions which you can import into your +own signature. The prelude is very minimal, but includes basic boolean, +arithmetic and list functions. We can write our lists signature using +the prelude as follows: + +[source,haskell] +---- +lists = [ + prelude (undefined :: A) `without` ["[]", ":"], + + background [ + "reverse" `fun1` (reverse :: [A] -> [A])], + "length" `fun1` (length :: [A] -> Int)] +---- + +A call to FUNprelude[`prelude`] +(undefined :: a)+ will declare the following +background functions: + * The boolean connectives `||`, `&&`, `not`, `True` and `False`. + * The arithmetic operations `0`, `1`, `+` and `*` over type `Int`. + * The list operations `[]`, `:`, `++`, `head` and `tail` over type `[a]`. + * Three variables each of type `Bool`, `Int`, `a` and `[a]`. + +In the example above we used the FUNwithout[`without`] combinator to +leave out `[]` and `:` from the prelude, so as to get fewer laws. +QuickSpec also provides the combinators FUNbools[`bools`], +FUNarith[`arith`] and FUNlists[`lists`], which import only their +respective part of the prelude, for when you want more control -- see +the DOCS[documentation] for more information. + +In EXAMPLELists.hs[Lists.hs] you can find an extended version +of the above example which also tests `map`. + +Advanced: function composition -- testing types with no `Ord` instance +---------------------------------------------------------------------- + +WARNING: this section isn't finished. + +IMPORTANT: You can skip this section unless you need to test a type +with no `Ord` instance. + +Suppose we want to get QuickSpec to discover the laws of function +composition -- things like `id . f == f`. + +If we just define a signature containing `id` and `(.)` (and suitable +variables), the output is rather disappointing: + +---- +(f . g) x == f (g x) +id x == x +---- + +This is because QuickSpec is giving us laws about _fully saturated_ +applications of `(.)` and `id`, that is, `(.)` applied to three +arguments and `id` applied to one argument. In the laws we are after, +we only want to apply `(.)` to two arguments, and we don't want to +apply `id` to an argument at all. To fix this we can declare `(.)` +to have arity 2 and `id` to have arity 1, so that QuickSpec won't +fully apply them: + +---- +composition = [ + vars ["f", "g", "h"] (undefined :: A -> A), + fun2 "." ((.) :: (A -> A) -> (A -> A) -> (A -> A)), + fun0 "id" (id :: A -> A), + ] +---- + +Unfortunately, we get the following error message: + +---- +Could not deduce (Ord (A -> A)) arising from a use of `fun2' +---- + +To test a law like `id . f == f`, QuickSpec generates a random value +for `f` and then just evaluates the expression `id . f == f` to get +either `True` or `False`. + +The error message complains that we are trying to generate laws about +terms of the type `A -> A` (i.e. functions), but as there is no `Ord` +instance for functions QuickSpec has no way of testing the laws. +QuickSpec tests a law like `id . f == f` by generating random values +for `f` and seeing if the resulting left-hand side and right-hand side +evaluate to the same value; it can only do this if it has an `Ord` +instance for the values in question. As there is no way to tell if +two functions are equal, it seems we are stuck! + +Hang on, though. We can still _test_ if two functions are equal: +generate a random argument and apply the two functions to it, and see +if they both give the same result. If they don't, they're certainly +not equal. Repeat the process a few times, for several random +arguments, and if both functions always seem to give the same result +then they're probably equal. + + + +This is a common situation -- we have a type, we cannot directly +compare values of that type, but we can make random _observations_ +and compare those. For our example, observing a function consists +of applying the function to a random argument. QuickSpec supports +finding equations over types that you can observe. The +observations must satisfy the following properties: + +* The observation returns a value of a type that we can directly + compare for equality. +* If two values are different, there is an observation that + distinguishes them. +* If an observation distinguishes two values, they are not equal. + + + +Common pitfalls +--------------- + +WARNING: this section isn't finished. + +*I get laws which seem to be false!* +If a law really is false, it means that QuickCheck didn't discover the +counterexample to it. Possible solutions include: + + * Improve the test data generation. If you can't change the + Arbitrary` instance for your type, you can use the + FUNgvars[`gvars`] combinator, which is like FUNvars[`vars`] + but allows you to specify the generator. + * If you are testing a polymorphic function, try instantiating it + with the QuickSpec type TYPETwo[`Two`] instead of TYPEA[`A`]. + TYPETwo[`Two`] is a type that has only two elements, which may + make it easier to hit counterexamples. + * Use the FUNwithTests[`withTests`] combinator to increase the + number of tests. + +*QuickSpec runs for a very long time without terminating!* +QuickSpec works by enumerating all terms up to a certain depth, +and therefore suffers from exponential blowup. Check the output +where it reports how many terms it generated: + +---- +== Testing == +Depth 1: 6 terms, 4 tests, 18 evaluations, 6 classes, 0 raw equations. +Depth 2: 61 terms, 500 tests, 28568 evaluations, 15 classes, 46 raw equations. +Depth 3: 412 terms, 500 tests, 205912 evaluations, 53 classes, 359 raw equations. +---- + +Here it's generated 412 terms. If the number gets much above 100,000 +then you will probably run into trouble. This can be caused by one of +several things: + * Too many functions in the signature. + +*I only get ground instances of the laws I want!* + +Perhaps you forgot to add + +no variables + +*Law not found* + +Is it true? Is it provable? Are all necessary functions in the signature? +Do the types match up so that the term is well-typed? + +*Get false laws* + +Tweak test data generators + +*Exponential blowup* + +*I want to test a datatype with no `Ord` instance, such as functions* + +see function composition + + + + +A common mistake when using QuickSpec is to forget to define any +variables of a certain type. In that case, you will typically get lots +of special cases instead of the law you really want. For example, + +---- +True||True == True +True||False == True +False||True == True +False||False == False +---- + +Where to go from here? +-------------------- + +Have a look at the examples that come with QuickSpec: + +* link:examples/Bools.hs[Booleans] +* link:examples/Arith.hs[Arithmetic] +* link:examples/Lists.hs[List functions] +* link:examples/Heaps.hs[Binary heaps] +* link:examples/Composition.hs[Function composition] +* link:examples/Arrays.hs[Arrays] +* link:examples/TinyWM.hs[A tiny window manager] +* link:examples/PrettyPrinting.hs[Pretty-printing combinators] + +Read our PAPER[paper]. + +Read the DOCS[Haddock documentation] for things to tweak. diff --git a/examples/Arrays.hs b/examples/Arrays.hs new file mode 100644 --- /dev/null +++ b/examples/Arrays.hs @@ -0,0 +1,44 @@ +-- Arrays. + +{-# LANGUAGE ScopedTypeVariables, FlexibleInstances, DeriveDataTypeable #-} +import Test.QuickCheck +import Test.QuickSpec +import Data.Typeable +import Data.Array + +put :: Ix i => i -> a -> Array i a -> Array i a +put ix v arr = arr // [(ix, v)] + +arrays :: forall a. (Typeable a, Ord a, Arbitrary a) => a -> [Sig] +arrays a = [ + -- Don't include head, or functions on natural numbers---they + -- generate too many irrelevant terms. + prelude (undefined :: a) `without` ["head", "*", "0", "1"], + lists (undefined :: Int) `without` ["head"], + + ["x", "y", "z"] `vars` (undefined :: a), + ["a"] `vars` (undefined :: Array Int a), + -- Generate ranges using a custom generator to improve test data + -- distribution. + ["r"] `gvars` genRange, + + "!" `fun2` ((!) :: Array Int a -> Int -> a), + "put" `fun3` (put :: Int -> a -> Array Int a -> Array Int a), + "listArray" `fun2` (listArray :: (Int, Int) -> [a] -> Array Int a), + "elems" `fun1` (elems :: Array Int a -> [a]), + "indices" `fun1` (indices :: Array Int a -> [Int])] + +instance Arbitrary a => Arbitrary (Array Int a) where + arbitrary = do + (low, high) <- genRange + elems <- arbitrary :: Gen (Int -> Maybe a) + return (array (low, high) [(i, x) | i <- [low..high], Just x <- [elems i]]) + +genRange :: Gen (Int, Int) +genRange = do + low <- choose (-2, 2) + high <- fmap (low +) (choose (-1, 2)) + return (low, high) + +-- Use Two instead of A to improve the chance of getting the right test data. +main = quickSpec (arrays (undefined :: Two)) diff --git a/examples/Lists.hs b/examples/Lists.hs --- a/examples/Lists.hs +++ b/examples/Lists.hs @@ -7,19 +7,11 @@ lists :: forall a. (Typeable a, Ord a, Arbitrary a, CoArbitrary a) => a -> [Sig] lists a = [ - arith (undefined :: Int), + prelude (undefined :: a) `without` ["++"], funs (undefined :: a), - ["x", "y", "z"] `vars` (undefined :: a), - ["xs", "ys", "zs"] `vars` (undefined :: [a]), - - background [ - "[]" `fun0` ([] :: [a]), - ":" `fun2` ((:) :: a -> [a] -> [a])], - - "head" `fun1` (head :: [a] -> a), - "tail" `fun1` (tail :: [a] -> [a]), "unit" `fun1` (return :: a -> [a]), + -- Don't take ++ from the prelude because we want to see laws about it "++" `fun2` ((++) :: [a] -> [a] -> [a]), "length" `fun1` (length :: [a] -> Int), "reverse" `fun1` (reverse :: [a] -> [a]), diff --git a/examples/PrettyPrinting.hs b/examples/PrettyPrinting.hs new file mode 100644 --- /dev/null +++ b/examples/PrettyPrinting.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables #-} +module Main where + +import Control.Monad +import Data.Typeable +import Test.QuickCheck +import Test.QuickSpec + +newtype Layout a = Layout [(Int, [a])] deriving (Typeable, Eq, Ord, Show) + +instance Arbitrary a => Arbitrary (Layout a) where + arbitrary = fmap Layout (liftM2 (:) arbitrary arbitrary) + +text :: [a] -> Layout a +text s = Layout [(0, s)] + +nest :: Int -> Layout a -> Layout a +nest k (Layout l) = Layout [(i+k, s) | (i, s) <- l] + +($$) :: Layout a -> Layout a -> Layout a +Layout xs $$ Layout ys = Layout (xs ++ ys) + +(<>) :: Layout a -> Layout a -> Layout a +Layout xs <> Layout ys = f (init xs) (last xs) (head ys) (tail ys) + where f xs (i, s) (j, t) ys = Layout xs $$ Layout [(i, s ++ t)] $$ nest (i + length s - j) (Layout ys) + +pretty :: forall a. (Typeable a, Ord a, Arbitrary a) => a -> [Sig] +pretty a = [ + ["d","e","f"] `vars` (undefined :: Layout a), + ["s","t","u"] `vars` (undefined :: [a]), + ["n","m","o"] `vars` (undefined :: Int), + "text" `fun1` (text :: [a] -> Layout a), + "nest" `fun2` (nest :: Int -> Layout a -> Layout a), + "$$" `fun2` (($$) :: Layout a -> Layout a -> Layout a), + "<>" `fun2` ((<>) :: Layout a -> Layout a -> Layout a), + background [ + "[]" `fun0` ([] :: [a]), + "++" `fun2` ((++) :: [a] -> [a] -> [a]), + "0" `fun0` (0 :: Int), + "length" `fun1` (length :: [a] -> Int), + "+" `fun2` ((+) :: Int -> Int -> Int)]] + +main = quickSpec (pretty (undefined :: Two)) diff --git a/examples/TinyWM.hs b/examples/TinyWM.hs --- a/examples/TinyWM.hs +++ b/examples/TinyWM.hs @@ -1,8 +1,3 @@ --- This example requires QuickCheck >= 2.5. For older versions, you will --- have to define an Arbitrary Ordering instance, like so: --- instance Arbitrary Ordering where --- arbitrary = elements [LT, EQ, GT] - -- A window manager example, -- taken from http://donsbot.wordpress.com/2007/05/01/roll-your-own-window-manager-part-1-defining-and-testing-a-model diff --git a/quickspec.cabal b/quickspec.cabal --- a/quickspec.cabal +++ b/quickspec.cabal @@ -1,6 +1,6 @@ Name: quickspec -Version: 0.9.5 -Cabal-version: >=1.6 +Version: 0.9.6 +Cabal-version: >= 1.6 Build-type: Simple Homepage: https://github.com/nick8325/quickspec @@ -13,47 +13,37 @@ Category: Testing -Synopsis: Equational laws for free +Synopsis: Equational laws for free! Description: - QuickSpec automatically finds equational properties of your program. + QuickSpec automatically finds equational laws about your program. . Give it an API, i.e. a collection of functions, and it will spit out equations about those functions. For example, given @reverse@, @++@ - and @[]@, QuickSpec finds six laws: + and @[]@, QuickSpec finds six laws, which are exactly the ones you + might write by hand: . > xs++[] == xs > []++xs == xs - > reverse [] == [] > (xs++ys)++zs == xs++(ys++zs) + > reverse [] == [] > reverse (reverse xs) == xs > reverse xs++reverse ys == reverse (ys++xs) . - All you have to provide is: - . - * Some functions and constants to test. These are the /only/ - functions that will appear in the equations. - . - * A collection of variables that can appear in the equations - (@xs@, @ys@ and @zs@ in the example above). - . - * 'Test.QuickCheck.Arbitrary' and 'Data.Typeable.Typeable' instances for the types you want to test. - . - Consider this a pre-release. Everything is complete but undocumented - :) The best place to start is the examples at - . There - is also a paper at - . - Everything you need should be in the module "Test.QuickSpec". + The laws that QuickSpec generates are not proved correct, but have + passed at least 200 QuickCheck tests. . - If you want help, email me! + For more information, see the @README@ file at + https://github.com/nick8325/quickspec/blob/master/README.asciidoc. Extra-source-files: - README + README.asciidoc examples/Arith.hs + examples/Arrays.hs examples/Bools.hs examples/Composition.hs examples/Heaps.hs examples/Lists.hs + examples/PrettyPrinting.hs examples/TinyWM.hs src/Test/QuickSpec/errors.h @@ -91,4 +81,4 @@ Build-depends: base < 5, containers, transformers, QuickCheck >= 2.7, - random, spoon >= 0.2, array, ghc-prim, mtl + random, spoon >= 0.2, array, ghc-prim diff --git a/src/Test/QuickSpec.hs b/src/Test/QuickSpec.hs --- a/src/Test/QuickSpec.hs +++ b/src/Test/QuickSpec.hs @@ -1,8 +1,9 @@ -- | The main QuickSpec module. -- --- This will not make sense if you haven't seen some examples! --- Look at , --- or read the paper at . +-- Look at the introduction (), +-- read the examples (), +-- or read the paper () +-- before venturing in here. module Test.QuickSpec (-- * Running QuickSpec diff --git a/src/Test/QuickSpec/Approximate.hs b/src/Test/QuickSpec/Approximate.hs --- a/src/Test/QuickSpec/Approximate.hs +++ b/src/Test/QuickSpec/Approximate.hs @@ -10,7 +10,7 @@ import Test.QuickSpec.Utils import Test.QuickSpec.Utils.Typeable import Control.Monad -import Control.Monad.Reader +import Control.Monad.Trans.Reader import Control.Spoon import System.Random import Data.Monoid @@ -61,7 +61,7 @@ plug x = frequency [(1, undefined), (3, x)] pvars :: (Ord a, Partial a) => [String] -> a -> Sig -pvars xs w = pobserver w `mappend` primVars0 0 xs (PGen g g') +pvars xs w = pobserver w `mappend` primVars0 0 (zip xs (repeat (PGen g g'))) where g = arbitrary `asTypeOf` return w g' = g >>= genPartial diff --git a/src/Test/QuickSpec/Prelude.hs b/src/Test/QuickSpec/Prelude.hs --- a/src/Test/QuickSpec/Prelude.hs +++ b/src/Test/QuickSpec/Prelude.hs @@ -86,6 +86,8 @@ -- Contains boolean, arithmetic and list functions, -- and some variables. -- Instantiate it as e.g. @prelude (undefined :: `A`)@. +-- For more precise control over what gets included, +-- see 'bools', 'arith', 'lists', 'funs' and 'without'. prelude :: (Typeable a, Ord a, Arbitrary a) => a -> Sig prelude a = background [ ["x", "y", "z"] `vars` a, diff --git a/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs b/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs --- a/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs +++ b/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs @@ -13,13 +13,14 @@ import Test.QuickSpec.Reasoning.NaiveEquationalReasoning(EQ, evalEQ, runEQ) import Data.IntMap(IntMap) import qualified Data.IntMap as IntMap -import Control.Monad.State -import qualified Control.Monad.State as S +import Control.Monad.Trans.State +import qualified Control.Monad.Trans.State as S import Data.List import Data.Ord import Test.QuickSpec.Utils import Test.QuickSpec.Signature hiding (vars) import Data.Monoid +import Control.Monad data PEquation = Precondition :\/: Equation type Precondition = [Symbol] diff --git a/src/Test/QuickSpec/Signature.hs b/src/Test/QuickSpec/Signature.hs --- a/src/Test/QuickSpec/Signature.hs +++ b/src/Test/QuickSpec/Signature.hs @@ -372,19 +372,19 @@ where sig' = signature sig silence1 x = x { silent = True } -primVars0 :: forall a. Typeable a => Int -> [String] -> PGen a -> Sig -primVars0 n xs g = variableSig [ Variable (Atom (symbol x n (undefined :: a)) g) | x <- xs ] - `mappend` totalSig (totalGen g) - `mappend` partialSig (partialGen g) +primVars0 :: forall a. Typeable a => Int -> [(String, PGen a)] -> Sig +primVars0 n xs = variableSig [ Variable (Atom (symbol x n (undefined :: a)) g) | (x, g) <- xs ] + `mappend` mconcat [ totalSig (totalGen g) | (_, g) <- xs ] + `mappend` mconcat [ partialSig (partialGen g) | (_, g) <- xs ] `mappend` typeSig (undefined :: a) -primVars1 :: forall a b. (Typeable a, Typeable b) => Int -> [String] -> PGen (a -> b) -> Sig -primVars1 n xs g = primVars0 n xs g +primVars1 :: forall a b. (Typeable a, Typeable b) => Int -> [(String, PGen (a -> b))] -> Sig +primVars1 n xs = primVars0 n xs `mappend` typeSig (undefined :: a) `mappend` typeSig (undefined :: b) -primVars2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => Int -> [String] -> PGen (a -> b -> c) -> Sig -primVars2 n xs g = primVars1 n xs g +primVars2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => Int -> [(String, PGen (a -> b -> c))] -> Sig +primVars2 n xs = primVars1 n xs `mappend` typeSig (undefined :: b) `mappend` typeSig (undefined :: c) @@ -393,14 +393,18 @@ -- @gvars xs (arbitrary :: Gen a)@ is the same as -- @vars xs (undefined :: a)@. gvars, gvars0 :: forall a. Typeable a => [String] -> Gen a -> Sig -gvars xs g = primVars0 0 xs (pgen g) +gvars xs g = primVars0 0 (zip xs (repeat (pgen g))) gvars0 = gvars gvars1 :: forall a b. (Typeable a, Typeable b) => [String] -> Gen (a -> b) -> Sig -gvars1 xs g = primVars1 1 xs (pgen g) +gvars1 xs g = primVars1 1 (zip xs (repeat (pgen g))) gvars2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => [String] -> Gen (a -> b -> c) -> Sig -gvars2 xs g = primVars2 2 xs (pgen g) +gvars2 xs g = primVars2 2 (zip xs (repeat (pgen g))) + +-- | For Hipsters only :) +gvars' :: forall a. Typeable a => [(String, Gen a)] -> Sig +gvars' xs = primVars0 0 [ (x, pgen g) | (x, g) <- xs ] -- | Declare a set of variables of a particular type. --