diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2009-2014, Nick Smallbone +Copyright (c) 2009-2018, Nick Smallbone All rights reserved. diff --git a/README.asciidoc b/README.asciidoc deleted file mode 100644 --- a/README.asciidoc +++ /dev/null @@ -1,410 +0,0 @@ -: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/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,28 @@ +QuickSpec: equational laws for free! +==================================== + +QuickSpec takes your Haskell code and, as if by magic, discovers laws about it. +You give QuickSpec a collection of Haskell functions; QuickSpec tests your functions +with QuickCheck and prints out laws which seem to hold. + +For example, give QuickSpec the functions `reverse`, `++` and `[]`, and it will +find six laws: + +```haskell +reverse [] == [] +xs ++ [] == xs +[] ++ xs == xs +reverse (reverse xs) == xs +(xs ++ ys) ++ zs == xs ++ (ys ++ zs) +reverse xs ++ reverse ys == reverse (ys ++ xs) +``` + +QuickSpec can find equational laws as well as conditional equations. All you +need to supply are the functions to test, as well as `Ord` and `Arbitrary` +instances for QuickSpec to use in testing; the rest is automatic. + +For information on how to use QuickSpec, see +[the documentation](http://hackage.haskell.org/package/quickspec/docs/QuickSpec.html). +You can also look in the `examples` directory, for example at +`List.hs`, `IntSet.hs`, or `Parsing.hs`. To read about how QuickSpec works, see +our paper, [Quick specifications for the busy programmer](http://www.cse.chalmers.se/~nicsma/papers/quickspec2.pdf). diff --git a/examples/Arith.hs b/examples/Arith.hs --- a/examples/Arith.hs +++ b/examples/Arith.hs @@ -1,18 +1,8 @@ --- Natural number functions. - -{-# LANGUAGE ScopedTypeVariables #-} - -import Test.QuickSpec hiding (arith) -import Test.QuickCheck -import Data.Typeable - -arith :: forall a. (Typeable a, Ord a, Num a, Arbitrary a) => a -> [Sig] -arith _ = [ - ["x", "y", "z"] `vars` (undefined :: a), - - "0" `fun0` (0 :: a), - "1" `fun0` (1 :: a), - "+" `fun2` ((+) :: a -> a -> a), - "*" `fun2` ((*) :: a -> a -> a)] +-- A simple example testing arithmetic functions. +import QuickSpec -main = quickSpec (arith (undefined :: Int)) +main = quickSpec [ + con "0" (0 :: Int), + con "1" (1 :: Int), + con "+" ((+) :: Int -> Int -> Int), + con "*" ((*) :: Int -> Int -> Int) ] diff --git a/examples/Arrays.hs b/examples/Arrays.hs deleted file mode 100644 --- a/examples/Arrays.hs +++ /dev/null @@ -1,44 +0,0 @@ --- 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/Bools.hs b/examples/Bools.hs --- a/examples/Bools.hs +++ b/examples/Bools.hs @@ -1,14 +1,9 @@ --- A simple booleans example. - -import Test.QuickSpec hiding (bools) - -bools = [ - ["x", "y", "z"] `vars` (undefined :: Bool), - - "||" `fun2` (||), - "&&" `fun2` (&&), - "not" `fun1` not, - "True" `fun0` True, - "False" `fun0` False] +-- Testing functions on booleans. "not x" is used as a condition. +import QuickSpec -main = quickSpec bools +main = quickSpec [ + predicate "not" not, + con "True" True, + con "False" False, + con "||" (||), + con "&&" (&&) ] diff --git a/examples/Composition.hs b/examples/Composition.hs --- a/examples/Composition.hs +++ b/examples/Composition.hs @@ -1,24 +1,6 @@ -{-# LANGUAGE ScopedTypeVariables #-} - -import Test.QuickSpec -import Test.QuickCheck -import Data.Typeable - -composition :: forall a. (Typeable a, Ord a, Arbitrary a, CoArbitrary a) => - a -> [Sig] -composition _ = [ - vars ["f", "g", "h"] (undefined :: a -> a), - - -- We treat . as a function of two arguments here (blind2)---i.e., - -- we do not generate terms of the form (f . g) x. - blind2 "." ((.) :: (a -> a) -> (a -> a) -> (a -> a)), - - -- Similarly, id is not treated as a function. - blind0 "id" (id :: a -> a), - - -- Tell QuickSpec how to compare values of function type: - -- i.e., generate a random argument and apply the function to it. - observer2 $ \x (f :: a -> a) -> f x - ] +-- Function composition. +import QuickSpec -main = quickSpec (composition (undefined :: A)) +main = quickSpec [ + con "id" (id :: A -> A), + con "." ((.) :: (B -> C) -> (A -> B) -> A -> C) ] diff --git a/examples/Geometry.hs b/examples/Geometry.hs new file mode 100644 --- /dev/null +++ b/examples/Geometry.hs @@ -0,0 +1,140 @@ +-- Henderson's functional geometry. See the QuickSpec paper. +-- +-- Illustrates: +-- * Observational equality +-- * Running QuickSpec on a progressively larger set of signatures +{-# LANGUAGE DeriveDataTypeable, TypeOperators, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses #-} +import QuickSpec +import Test.QuickCheck +import qualified Data.Set as Set +import Data.Set(Set) +import Prelude hiding (flip, cycle) +import Data.Monoid +import Control.Monad +import Data.Word +import Data.Constraint + +-- We use our own number type for efficiency purposes. +-- This can represent numbers of the form x/2^e where x and e are integers. +data Rat = Rat { mantissa :: Integer, exponent :: Int } deriving (Eq, Ord, Show, Typeable) +-- Rat x e = x / 2^e + +rat :: Integer -> Int -> Rat +rat x e | e < 0 = error "rat: negative exponent" +rat x 0 = Rat x 0 +rat x e | even x = rat (x `div` 2) (e-1) +rat x e = Rat x e + +instance Arbitrary Rat where + arbitrary = liftM2 rat arbitrary (choose (0, 10)) + shrink (Rat x e) = fmap (uncurry rat) (shrink (x, e)) + +instance CoArbitrary Rat where + coarbitrary (Rat x e) = coarbitrary x . coarbitrary e + +-- A class for types (like Rat) which can be added, subtracted and +-- divided by 2. +class Half a where + zero :: a + neg :: a -> a + plus :: a -> a -> a + half :: a -> a + +instance Half Rat where + zero = rat 0 0 + neg (Rat x e) = Rat (negate x) e + plus (Rat x1 e1) (Rat x2 e2) = + rat (x1 * 2^(e - e1) + x2 * 2^(e - e2)) e + where + e = e1 `max` e2 + half (Rat x e) = Rat x (e+1) + +instance (Half a, Half b) => Half (a, b) where + zero = (zero, zero) + neg (x, y) = (neg x, neg y) + plus (x, y) (z, w) = (plus x z, plus y w) + half (x, y) = (half x, half y) + +-- A vector is a pair of points. +type Vector = (Rat, Rat) + +-- We represent a geometrical object as a triple of vectors. +-- I forget what they mean :) +-- I think two of them represent the direction of the x-axis and y-axis. +-- The word represents an abstract "drawing command". +type Object = (Vector, Vector, Vector, Word) + +-- A drawing takes size and rotation information and returns a set of objects. +newtype Drawing = Drawing (Vector -> Vector -> Vector -> Objs) deriving Typeable +newtype Objs = Objs { unObjs :: Set Object } deriving (Eq, Ord, Typeable, Show) +instance Arbitrary Objs where arbitrary = fmap objs arbitrary + +objs :: Set Object -> Objs +objs = Objs . Set.filter (\(_,b,c,_) -> b /= zero && c /= zero) + +instance Show Drawing where + show (Drawing x) = show (x one one one) + where + one = (Rat 1 0, Rat 1 0) + +instance Arbitrary Drawing where + arbitrary = do + os <- arbitrary + return . Drawing $ \x y z -> objs (Set.fromList [(x, y, z, o) | o <- os]) + shrink (Drawing f) = + [ Drawing $ \x y z -> objs (Set.fromList [(x, y, z, o) | o <- objs']) + | let os = [ o | (_, _, _, o) <- Set.toList (unObjs (f one one one)) ], + objs' <- shrink os ] + where + one = (Rat 1 0, Rat 1 0) + +blank :: Drawing +blank = Drawing (\_ _ _ -> objs Set.empty) + +-- The primed versions of the combinators are buggy +over, beside, above, above' :: Drawing -> Drawing -> Drawing +over (Drawing p) (Drawing q) = Drawing (\a b c -> p a b c `union` q a b c) +beside (Drawing p) (Drawing q) = Drawing (\a b c -> p a (half b) c `union` q (a `plus` half b) (half b) c) +above' (Drawing p) (Drawing q) = Drawing (\a b c -> p a b (half c) `union` q (a `plus` half c) b (half c)) +above (Drawing p) (Drawing q) = Drawing (\a b c -> p (a `plus` half c) b (half c) `union` q a b (half c)) + +union :: Objs -> Objs -> Objs +union (Objs x) (Objs y) = objs (x `Set.union` y) + +rot, flip, rot45 :: Drawing -> Drawing +rot (Drawing p) = Drawing (\a b c -> p (a `plus` b) c (neg b)) +flip (Drawing p) = Drawing (\a b c -> p (a `plus` b) (neg b) c) +rot45 (Drawing p) = Drawing (\a b c -> p (a `plus` half (b `plus` c)) (half (b `plus` c)) (half (c `plus` neg b))) + +quartet, quartet' :: Drawing -> Drawing -> Drawing -> Drawing -> Drawing +quartet a b c d = (a `beside` b) `above` (c `beside` d) +quartet' a b c d = (a `beside` b) `above'` (c `beside` d) + +cycle, cycle' :: Drawing -> Drawing +cycle x = quartet x (rot (rot (rot x))) (rot x) (rot (rot x)) +cycle' x = quartet' x (rot (rot (rot x))) (rot x) (rot (rot x)) + +-- Observational equality for drawings. +instance Observe (Vector, Vector, Vector) Objs Drawing where + observe (a, b, c) (Drawing d) = d a b c + +main = + quickSpec [ + inst (Sub Dict :: () :- Arbitrary Drawing), + inst (Sub Dict :: () :- Observe (Vector, Vector, Vector) Objs Drawing), + series [sig1, sig2, sig3, sig4, sig5, sig6, sig7] ] + where + -- A series of bigger and bigger signatures. + sig1 = [con "over" over] + sig2 = [ + con "beside" beside, + -- con "above" above', + con "above" above] + sig3 = [con "rot" rot] + sig4 = [con "flip" flip] + sig5 = [ + con "cycle" cycle, + -- con "cycle" cycle', + con "quartet" quartet] + sig6 = [con "rot45" rot45] + sig7 = [con "blank" blank] diff --git a/examples/Heaps.hs b/examples/Heaps.hs deleted file mode 100644 --- a/examples/Heaps.hs +++ /dev/null @@ -1,93 +0,0 @@ -{-# LANGUAGE ScopedTypeVariables,DeriveDataTypeable #-} - -import Prelude hiding (null) -import Test.QuickSpec -import Test.QuickCheck -import Data.Typeable -import Data.Ord -import qualified Data.List as L - -data Heap a = Nil | Branch Int a (Heap a) (Heap a) deriving Typeable - -instance Ord a => Eq (Heap a) where - h1 == h2 = toList h1 == toList h2 - -instance Ord a => Ord (Heap a) where - compare = comparing toList - -instance (Ord a, Arbitrary a) => Arbitrary (Heap a) where - arbitrary = fmap fromList arbitrary - -toList :: Ord a => Heap a -> [a] -toList h | null h = [] - | otherwise = findMin h:toList (deleteMin h) - -fromList :: Ord a => [a] -> Heap a -fromList = foldr insert Nil - -null :: Heap a -> Bool -null Nil = True -null _ = False - -findMin :: Heap a -> a -findMin (Branch _ x _ _) = x - -insert :: Ord a => a -> Heap a -> Heap a -insert x h = merge h (branch x Nil Nil) - -deleteMin :: Ord a => Heap a -> Heap a -deleteMin (Branch _ _ l r) = merge l r - -branch :: Ord a => a -> Heap a -> Heap a -> Heap a -branch x l r | npl l <= npl r = Branch (npl l + 1) x l r - | otherwise = Branch (npl r + 1) x r l - -merge :: Ord a => Heap a -> Heap a -> Heap a -merge Nil h = h -merge h Nil = h -merge h1@(Branch _ x1 l1 r1) h2@(Branch _ x2 l2 r2) - | x1 <= x2 = branch x1 (merge l1 h2) r1 - | otherwise = merge h2 h1 - -npl :: Heap a -> Int -npl Nil = 0 -npl (Branch n _ _ _) = n - -mergeLists :: Ord a => [a] -> [a] -> [a] -mergeLists [] xs = xs -mergeLists xs [] = xs -mergeLists (x:xs) (y:ys) - | x < y = x:mergeLists xs (y:ys) - | otherwise = y:mergeLists (x:xs) ys - -heaps :: forall a. (Ord a, Typeable a, Arbitrary a) => a -> [Sig] -heaps a = [ - prelude a, - - ["h", "h1", "h2"] `vars` (undefined :: Heap a), - - "nil" `fun0` (Nil :: Heap a), - "insert" `fun2` (insert :: a -> Heap a -> Heap a), - "findMin" `fun1` (findMin :: Heap a -> a), - "deleteMin" `fun1` (deleteMin :: Heap a -> Heap a), - "merge" `fun2` (merge :: Heap a -> Heap a -> Heap a), - "null" `fun1` (null :: Heap a -> Bool), - "fromList" `fun1` (fromList :: [a] -> Heap a), - - -- A few more list functions that are helpful for getting - -- laws about toList/fromList. - -- We use "background" to mark the functions as background theory, - -- so that we only get laws that involve one of the heap functions. - -- toList is marked as background to make the presentation of the - -- equations a bit prettier: laws about e.g. findMin and toList - -- will appear in QuickSpec's "Equations about findMin" section - -- rather than "Equations about several functions". - background [ - "toList" `fun1` (toList :: Heap a -> [a]), - "sort" `fun1` (L.sort :: [a] -> [a]), - "insertList" `fun2` (L.insert :: a -> [a] -> [a]), - "nullList" `fun1` (L.null :: [a] -> Bool), - "deleteList" `fun2` (L.delete :: a -> [a] -> [a]), - "mergeLists" `fun2` (mergeLists :: [a] -> [a] -> [a])]] - -main = quickSpec (heaps (undefined :: A)) diff --git a/examples/HugeLists.hs b/examples/HugeLists.hs new file mode 100644 --- /dev/null +++ b/examples/HugeLists.hs @@ -0,0 +1,41 @@ +-- A stress test using lots and lots of list functions. +{-# LANGUAGE ScopedTypeVariables, ConstraintKinds, RankNTypes, ConstraintKinds, FlexibleContexts #-} +import QuickSpec +import QuickSpec.Utils +import Data.List +import Control.Monad + +main = quickSpec [ + con "length" (length :: [A] -> Int), + con "sort" (sort :: [Int] -> [Int]), + con "scanr" (scanr :: (A -> B -> B) -> B -> [A] -> [B]), + con "succ" (succ :: Int -> Int), + con ">>=" ((>>=) :: [A] -> (A -> [B]) -> [B]), + con "snd" (snd :: (A, B) -> B), + con "reverse" (reverse :: [A] -> [A]), + con "0" (0 :: Int), + con "," ((,) :: A -> B -> (A, B)), + con ">=>" ((>=>) :: (A -> [B]) -> (B -> [C]) -> A -> [C]), + con ":" ((:) :: A -> [A] -> [A]), + con "break" (break :: (A -> Bool) -> [A] -> ([A], [A])), + con "filter" (filter :: (A -> Bool) -> [A] -> [A]), + con "scanl" (scanl :: (B -> A -> B) -> B -> [A] -> [B]), + con "zipWith" (zipWith :: (A -> B -> C) -> [A] -> [B] -> [C]), + con "concat" (concat :: [[A]] -> [A]), + con "zip" (zip :: [A] -> [B] -> [(A, B)]), + con "usort" (usort :: [Int] -> [Int]), + con "sum" (sum :: [Int] -> Int), + con "++" ((++) :: [A] -> [A] -> [A]), + con "map" (map :: (A -> B) -> [A] -> [B]), + con "foldl" (foldl :: (B -> A -> B) -> B -> [A] -> B), + con "takeWhile" (takeWhile :: (A -> Bool) -> [A] -> [A]), + con "foldr" (foldr :: (A -> B -> B) -> B -> [A] -> B), + con "drop" (drop :: Int -> [A] -> [A]), + con "dropWhile" (dropWhile :: (A -> Bool) -> [A] -> [A]), + con "span" (span :: (A -> Bool) -> [A] -> ([A], [A])), + con "unzip" (unzip :: [(A, B)] -> ([A], [B])), + con "+" ((+) :: Int -> Int -> Int), + con "[]" ([] :: [A]), + con "partition" (partition :: (A -> Bool) -> [A] -> ([A], [A])), + con "fst" (fst :: (A, B) -> A), + con "take" (take :: Int -> [A] -> [A]) ] diff --git a/examples/IntSet.hs b/examples/IntSet.hs new file mode 100644 --- /dev/null +++ b/examples/IntSet.hs @@ -0,0 +1,23 @@ +-- Laws about Data.IntSet. +-- Illustrates user-defined data types. +import QuickSpec +import qualified Data.IntSet as IntSet +import Data.IntSet(IntSet) + +main = quickSpec [ + monoType (Proxy :: Proxy IntSet), + + series [sig1, sig2, sig3]] + where + sig1 = [ + con "union" IntSet.union, + con "intersection" IntSet.intersection, + con "empty" IntSet.empty ] + + sig2 = [ + con "insert" IntSet.insert, + con "delete" IntSet.delete ] + + sig3 = [ + con "False" False, + predicate "member" IntSet.member ] diff --git a/examples/ListMonad.hs b/examples/ListMonad.hs new file mode 100644 --- /dev/null +++ b/examples/ListMonad.hs @@ -0,0 +1,9 @@ +-- The monad laws for lists. +import Control.Monad +import QuickSpec + +main = quickSpec [ + con "return" (return :: A -> [A]), + con ">>=" ((>>=) :: [A] -> (A -> [B]) -> [B]), + con "++" ((++) :: [A] -> [A] -> [A]), + con ">=>" ((>=>) :: (A -> [B]) -> (B -> [C]) -> A -> [C]) ] diff --git a/examples/Lists.hs b/examples/Lists.hs --- a/examples/Lists.hs +++ b/examples/Lists.hs @@ -1,21 +1,17 @@ -{-# LANGUAGE ScopedTypeVariables #-} - -import Test.QuickSpec hiding (lists) -import Test.QuickCheck -import Data.Typeable - -lists :: forall a. (Typeable a, Ord a, Arbitrary a, CoArbitrary a) => - a -> [Sig] -lists a = [ - prelude (undefined :: a) `without` ["++"], - funs (undefined :: a), +-- Some usual list functions. +{-# LANGUAGE ScopedTypeVariables, ConstraintKinds, RankNTypes, ConstraintKinds, FlexibleContexts #-} +import QuickSpec +import Data.List - "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]), - "map" `fun2` (map :: (a -> a) -> [a] -> [a]) - ] +main = quickSpec [ + con "reverse" (reverse :: [A] -> [A]), + con "++" ((++) :: [A] -> [A] -> [A]), + con "[]" ([] :: [A]), + con "map" (map :: (A -> B) -> [A] -> [B]), + con "length" (length :: [A] -> Int), + con "concat" (concat :: [[A]] -> [A]), -main = quickSpec (lists (undefined :: A)) + -- Add some numeric functions to get more laws about length. + background [ + con "0" (0 :: Int), + con "+" ((+) :: Int -> Int -> Int) ] ] diff --git a/examples/Octonions.hs b/examples/Octonions.hs new file mode 100644 --- /dev/null +++ b/examples/Octonions.hs @@ -0,0 +1,60 @@ +-- The octonions, made using the Cayley-Dickson construction. +{-# LANGUAGE GeneralizedNewtypeDeriving, DeriveDataTypeable, FlexibleInstances #-} +import Data.Ratio +import QuickSpec +import Test.QuickCheck +import Twee.Pretty +import Control.Monad +import Data.Proxy + +newtype SmallRational = SmallRational Rational + deriving (Eq, Ord, Num, Typeable, Fractional, Conj, CoArbitrary, Show) +instance Arbitrary SmallRational where + arbitrary = SmallRational <$> liftM2 (%) arbitrary (arbitrary `suchThat` (/= 0)) + +-- A class for types with conjugation, a norm operator and a generator. +class Fractional a => Conj a where + conj :: a -> a + norm :: a -> Rational + it :: Gen a + +instance Conj Rational where + conj x = x + norm x = x*x + -- Only generate small rationals for efficiency. + it = liftM2 (Prelude./) (elements [-10..10]) (elements [1..10]) + +instance Conj a => Conj (a, a) where + conj (x, y) = (conj x, negate y) + norm (x, y) = norm x + norm y + it = liftM2 (,) it it + +instance Conj a => Num (a, a) where + fromInteger n = (fromInteger n, 0) + (x, y) + (z, w) = (x + z, y + w) + (a, b) * (c, d) = (a * c - conj d * b, d * a + b * conj c) + negate (x, y) = (negate x, negate y) + +instance Conj a => Fractional (a, a) where + fromRational x = (fromRational x, 0) + recip x = conj x * fromRational (recip (norm x)) + +newtype Complex = Complex (SmallRational, SmallRational) deriving (Eq, Ord, Num, Typeable, Fractional, Conj, Arbitrary, CoArbitrary, Show) +newtype Quaternion = Quaternion (Complex, Complex) deriving (Eq, Ord, Num, Typeable, Fractional, Conj, Arbitrary, CoArbitrary, Show) +newtype Octonion = Octonion (Quaternion, Quaternion) deriving (Eq, Ord, Num, Typeable, Fractional, Conj, Arbitrary, CoArbitrary, Show) + +newtype It = It Octonion deriving (Eq, Ord, Num, Typeable, Fractional, Conj, CoArbitrary, Show) + +instance Arbitrary It where + -- Division is undefined on zero octonions. + arbitrary = It <$> arbitrary `suchThat` (/= 0) + +main = quickSpec [ + -- Make the pruner more powerful, which is helpful when Doing Maths + withPruningTermSize 9, + -- One test suffices :) + withMaxTests 1, + con "*" ((*) :: It -> It -> It), + (con "inv" (recip :: It -> It)), + con "1" (1 :: It), + monoType (Proxy :: Proxy It)] diff --git a/examples/Parsing.hs b/examples/Parsing.hs new file mode 100644 --- /dev/null +++ b/examples/Parsing.hs @@ -0,0 +1,48 @@ +-- Parser combinators. +-- Illustrates observational equality with polymorphic types. +{-# LANGUAGE DeriveDataTypeable, TypeOperators, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-} +import Control.Monad +import Test.QuickCheck +import QuickSpec +import Data.List +import Text.ParserCombinators.ReadP +import Data.Constraint + +deriving instance Typeable ReadP + +-- Generate random parsers. +instance Arbitrary a => Arbitrary (ReadP a) where + arbitrary = fmap readS_to_P arbReadS + +arbReadS :: Arbitrary a => Gen (String -> [(a, String)]) +arbReadS = fmap convert (liftM2 (,) (elements [0..5]) arbitrary) + where + convert (n, parse) xs = take n [(x, drop n xs) | (x, n) <- parse xs] + +-- Observational equality for parsers. +instance Ord a => Observe String [(a, String)] (ReadP a) where + observe input parser = sort (readP_to_S parser input) + +peek :: ReadP Char +peek = do + (x:_) <- look + return x + +main = quickSpec [ + inst (Sub Dict :: Arbitrary A :- Arbitrary (ReadP A)), + inst (Sub Dict :: Ord A :- Observe String [(A, String)] (ReadP A)), + + background [ + con "return" (return :: A -> ReadP A), + con "()" (), + con "void" (void :: ReadP A -> ReadP ()), + con ">>=" ((>>=) :: ReadP A -> (A -> ReadP B) -> ReadP B), + con ">=>" ((>=>) :: (A -> ReadP B) -> (B -> ReadP C) -> A -> ReadP C) ], + + con "get" get, + con "peek" peek, + con "+++" ((+++) :: ReadP A -> ReadP A -> ReadP A), + con "<++" ((<++) :: ReadP A -> ReadP A -> ReadP A), + con "pfail" (pfail :: ReadP A), + con "eof" eof ] + diff --git a/examples/PrettyPrinting.hs b/examples/PrettyPrinting.hs --- a/examples/PrettyPrinting.hs +++ b/examples/PrettyPrinting.hs @@ -1,43 +1,70 @@ -{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables #-} -module Main where - +-- Pretty-printing combinators. +-- Illustrates observational equality and using custom generators. +-- See the QuickSpec paper for more details. +{-# LANGUAGE DeriveDataTypeable, TypeOperators, StandaloneDeriving, TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-} import Control.Monad -import Data.Typeable import Test.QuickCheck -import Test.QuickSpec +import QuickSpec +import Text.PrettyPrint.HughesPJ hiding (Str) +import Data.Proxy +import Data.Constraint -newtype Layout a = Layout [(Int, [a])] deriving (Typeable, Eq, Ord, Show) +deriving instance Typeable Doc -instance Arbitrary a => Arbitrary (Layout a) where - arbitrary = fmap Layout (liftM2 (:) arbitrary arbitrary) +instance Arbitrary Doc where + arbitrary = + sized $ \n -> + let bin = resize (n `div` 2) arbitrary + un = resize (n-1) arbitrary in + oneof $ + [ liftM2 ($$) bin bin | n > 0 ] ++ + [ liftM2 (<>) bin bin | n > 0 ] ++ + [ liftM2 nest arbitrary un | n > 0 ] ++ + [ fmap text arbitrary ] -text :: [a] -> Layout a -text s = Layout [(0, s)] +-- Observational equality. +instance Observe Context Str Doc where + observe (Context ctx) d = Str (render (ctx d)) +newtype Str = Str String deriving (Eq, Ord) -nest :: Int -> Layout a -> Layout a -nest k (Layout l) = Layout [(i+k, s) | (i, s) <- l] +newtype Context = Context (Doc -> Doc) -($$) :: Layout a -> Layout a -> Layout a -Layout xs $$ Layout ys = Layout (xs ++ ys) +instance Arbitrary Context where + arbitrary = Context <$> ctx + where + ctx = + sized $ \n -> + oneof $ + [ return id ] ++ + [ liftM2 (\x y d -> op (x d) y) (resize (n `div` 2) ctx) (resize (n `div` 2) arbitrary) | n > 0, op <- [(<>), ($$)] ] ++ + [ liftM2 (\x y d -> op x (y d)) (resize (n `div` 2) arbitrary) (resize (n `div` 2) ctx) | n > 0, op <- [(<>), ($$)] ] ++ + [ liftM2 (\x y d -> nest x (y d)) arbitrary (resize (n-1) ctx) | n > 0 ] -(<>) :: 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) +unindented :: Doc -> Bool +unindented d = render (nest 100 (text "" <> d)) == render (nest 100 d) -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), +nesting :: Doc -> Int +nesting d = head [ i | i <- nums, unindented (nest (-i) d) ] + where + nums = 0:concat [ [i, -i] | i <- [1..] ] + +main = quickSpec [ + withMaxTermSize 9, + background [ - "[]" `fun0` ([] :: [a]), - "++" `fun2` ((++) :: [a] -> [a] -> [a]), - "0" `fun0` (0 :: Int), - "length" `fun1` (length :: [a] -> Int), - "+" `fun2` ((+) :: Int -> Int -> Int)]] + con "[]" ([] :: [A]), + con "++" ((++) :: [A] -> [A] -> [A]), + con "0" (0 :: Int), + con "+" ((+) :: Int -> Int -> Int), + con "length" (length :: [A] -> Int) ], -main = quickSpec (pretty (undefined :: Two)) + + con "text" text, + con "nest" nest, + --con "nesting" nesting, + con "<>" (<>), + con "$$" ($$), + + inst (Sub Dict :: () :- Observe Context Str Doc), + inst (Sub Dict :: () :- Arbitrary Doc), + defaultTo (Proxy :: Proxy Bool)] diff --git a/examples/PrettyPrintingModel.hs b/examples/PrettyPrintingModel.hs new file mode 100644 --- /dev/null +++ b/examples/PrettyPrintingModel.hs @@ -0,0 +1,49 @@ +-- Pretty-printing combinators, testing against a model implementation. +-- Illustrates running QuickSpec on a progressively larger set of signatures. +-- See the QuickSpec paper for more details. +{-# LANGUAGE DeriveDataTypeable, TypeOperators #-} +import Control.Monad +import Test.QuickCheck +import QuickSpec +import Data.Proxy + +newtype Layout = Layout [(Int, String)] + deriving (Typeable, Eq, Ord, Show) + +instance Arbitrary Layout where + arbitrary = fmap Layout (liftM2 (:) arbitrary arbitrary) + +text :: String -> Layout +text s = Layout [(0, s)] + +nest :: Int -> Layout -> Layout +nest k (Layout l) = Layout [(i+k, s) | (i, s) <- l] + +($$) :: Layout -> Layout -> Layout +Layout xs $$ Layout ys = Layout (xs ++ ys) + +(<>) :: Layout -> Layout -> Layout +Layout xs <> Layout ys = + combine (init xs) (last xs) (head ys) (tail ys) + where + combine xs (i, s) (j, t) ys = + Layout xs $$ + Layout [(i, s ++ t)] $$ + nest (i + length s - j) (Layout ys) + +nesting :: Layout -> Int +nesting (Layout ((i,_):_)) = i + +main = quickSpec [ + withMaxTermSize 9, + monoType (Proxy :: Proxy Layout), + background [ + con "\"\"" "", + con "++" ((++) :: String -> String -> String), + con "0" (0 :: Int), + con "+" ((+) :: Int -> Int -> Int), + con "length" (length :: String -> Int) ], + con "text" text, + con "nest" nest, + con "$$" ($$), + con "<>" (<>) ] diff --git a/examples/Regex.hs b/examples/Regex.hs new file mode 100644 --- /dev/null +++ b/examples/Regex.hs @@ -0,0 +1,123 @@ +-- Regular expressions. +{-# LANGUAGE GeneralizedNewtypeDeriving,DeriveDataTypeable, FlexibleInstances #-} +import qualified Control.Monad.State as S +import Control.Monad.State hiding (State, state) +import qualified Data.Map as M +import Data.List +import Data.Map(Map) +import Data.Typeable +import QuickSpec +import Test.QuickCheck +import Test.QuickCheck.Random +import Test.QuickCheck.Gen +import Data.Ord +import Data.Monoid + +data Sym = A | B deriving (Eq, Ord, Typeable) + +instance Arbitrary Sym where + arbitrary = elements [A, B] + +newtype State = State Int deriving (Eq, Ord, Num, Show) + +data NFA a = NFA { + epsilons :: Map State [State], + transitions :: Map (State, Maybe a) [State], + initial :: State, + final :: State } deriving Show + +data Regex a = Char a | AnyChar | Epsilon | Zero + | Concat (Regex a) (Regex a) + | Choice (Regex a) (Regex a) + | Plus (Regex a) deriving (Typeable, Show) + +-- This should really use observational equality instead. +vals :: [[Sym]] +vals = unGen (vector 100) (mkQCGen 12345) 10 + +instance Eq (Regex Sym) where x == y = x `compare` y == EQ +instance Ord (Regex Sym) where + compare = comparing (\r -> map (run (compile r)) vals) + +instance Arbitrary (Regex Sym) where + arbitrary = sized arb + where arb 0 = oneof [fmap Char arbitrary, return AnyChar, return Epsilon, return Zero] + arb n = oneof [fmap Char arbitrary, return AnyChar, return Epsilon, return Zero, + liftM2 Concat arb' arb', liftM2 Choice arb' arb', fmap Plus (arb (n-1))] + where arb' = arb (n `div` 2) + +star r = Choice Epsilon (Plus r) + +type M a = S.State ([(State, Maybe a, State)], [(State, State)], State) + +edge :: State -> Maybe a -> State -> M a () +edge start e end = modify (\(edges, epsilons, next) -> ((start, e, end):edges, epsilons, next)) + +epsilon :: State -> State -> M a () +epsilon start end = modify (\(edges, epsilons, next) -> (edges, (start, end):epsilons, next)) + +state :: M a State +state = do + (edges, epsilons, next) <- get + put (edges, epsilons, next+1) + return next + +compile1 :: Regex a -> State -> State -> M a () +compile1 (Char c) start end = edge start (Just c) end +compile1 AnyChar start end = edge start Nothing end +compile1 Zero start end = return () +compile1 Epsilon start end = epsilon start end +compile1 (Concat r s) start end = do + mid <- state + compile1 r start mid + compile1 s mid end +compile1 (Choice r s) start end = do + compile1 r start end + compile1 s start end +compile1 (Plus r) start end = do + start' <- state + end' <- state + epsilon start start' + epsilon end' end + epsilon end' start' + compile1 r start' end' + +compile :: Ord a => Regex a -> NFA a +compile r = NFA (close (foldr enter M.empty epsilons)) (foldr flatten M.empty edges) (State 0) (State 1) + where (edges, epsilons, _) = execState (compile1 r (State 0) (State 1)) ([], [], State 2) + flatten (start, edge, to) edges = M.insertWith (++) (start, edge) [to] edges + enter (from, to) epsilons = M.insertWith (++) from [to] epsilons + +close :: Ord a => Map a [a] -> Map a [a] +close m | xs == [] = m + | otherwise = close (foldr enter m xs) + where enter (from, to) epsilons = M.insertWith (++) from [to] epsilons + xs = nub' (close1 m) + +close1 m = do + (from, tos) <- M.toList m + to <- tos + to' <- M.findWithDefault [] to m + guard (to' `notElem` tos && to' /= to && to' /= from) + return (from, to') + +run :: Ord a => NFA a -> [a] -> Bool +run nfa = runFrom nfa [initial nfa] +runFrom nfa states = runFrom' nfa (nub' (concatMap (epsilonClosed nfa) states)) +runFrom' nfa states [] = final nfa `elem` states +runFrom' nfa states (x:xs) = runFrom nfa (nub' $ concat [ M.findWithDefault [] (s, Just x) (transitions nfa) ++ M.findWithDefault [] (s, Nothing) (transitions nfa) | s <- states ]) xs +epsilonClosed nfa s = s:M.findWithDefault [] s (epsilons nfa) + +nub' :: Ord a => [a] -> [a] +nub' = map head . group . sort + +main = quickSpec [ + con "char" (Char :: Sym -> Regex Sym), + con "any" (AnyChar :: Regex Sym), + con "e" (Epsilon :: Regex Sym), + con "0" (Zero :: Regex Sym), + con ";" (Concat :: Regex Sym -> Regex Sym -> Regex Sym), + con "|" (Choice :: Regex Sym -> Regex Sym -> Regex Sym), + con "*" (star :: Regex Sym -> Regex Sym), + monoType (Proxy :: Proxy (Regex Sym)), + monoType (Proxy :: Proxy Sym) ] diff --git a/examples/Sorted.hs b/examples/Sorted.hs new file mode 100644 --- /dev/null +++ b/examples/Sorted.hs @@ -0,0 +1,18 @@ +-- Sorting and sorted lists. +-- Illustrates testing of conditional laws. +import QuickSpec +import Data.List + +sorted :: Ord a => [a] -> Bool +sorted [] = True +sorted [_] = True +sorted (x:y:xs) = x <= y && sorted (y:xs) + +main = quickSpec [ + background [ + con ":" ((:) :: A -> [A] -> [A]), + con "[]" ([] :: [A]) ], + + con "sort" (sort :: [Int] -> [Int]), + con "insert" (insert :: Int -> [Int] -> [Int]), + predicate "sorted" (sorted :: [Int] -> Bool) ] diff --git a/examples/TinyWM.hs b/examples/TinyWM.hs deleted file mode 100644 --- a/examples/TinyWM.hs +++ /dev/null @@ -1,189 +0,0 @@ --- 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 - -{-# OPTIONS -fglasgow-exts #-} - -import Data.Maybe -import Data.Map (Map) -import Data.Typeable -import qualified Data.Map as M -import qualified Data.List as L -import Test.QuickCheck -import Test.QuickSpec - --- --------------------------------------------------------------------- --- A data structure for multiple workspaces containing stacks of screens --- - -data StackSet a = StackSet - { current :: Int -- the current workspace - , stacks :: Map Int [a] } -- map workspaces to window stacks - deriving (Eq, Ord, Show, Read, Typeable) - --- | /O(n)/. Create a new empty stackset of 'n' workspaces -empty :: Ord a => Int -> StackSet a -empty n = StackSet { current = 0, stacks = ws } - where - ws = M.fromList (zip [0..n-1] (repeat [])) - --- | /O(log n)/. Set the given stack as being visible. If the index is out of --- bounds, the stack is returned unmodified. -view :: Int -> StackSet a -> StackSet a -view n w | M.member n (stacks w) = w { current = n } - | otherwise = w - --- | /O(log s)/. Extract the element on the top of the current stack. --- If no such element exists, Nothing is returned. -peek :: Ord a => StackSet a -> Maybe a -peek w | Just (x:_) <- M.lookup (current w) (stacks w) = Just x - | otherwise = Nothing - --- | /O(log n)/. rotate. cycle the current window list up or down. --- Has the effect of rotating focus. In fullscreen mode this will cause --- a new window to be visible. --- --- rotate EQ --> [5,6,7,8,1,2,3,4] --- rotate GT --> [6,7,8,1,2,3,4,5] --- rotate LT --> [4,5,6,7,8,1,2,3] --- --- where xs = [5..8] ++ [1..4] --- -rotate :: Ordering -> StackSet a -> StackSet a -rotate o w = w { stacks = M.adjust rot (current w) (stacks w) } - where - rot [] = [] - rot xs = case o of - GT -> tail xs ++ [head xs] - LT -> last xs : init xs - _ -> xs - --- --------------------------------------------------------------------- --- operations that affect multiple workspaces - --- | /O(log n)/. Push. Insert an element onto the top of the current stack. --- If the element is already in the current stack, it is moved to the top. --- If the element is managed on another stack, it is removed from that stack. --- -push :: Ord a => a -> StackSet a -> StackSet a -push k w = insert k (current w) w - --- | /O(log n)/. shift. move the client on top of the current stack to --- the top of stack 'n'. If the stack to move to is not valid, and --- exception is thrown. If there's no client on the current stack, the --- stack set is returned unchanged. -shift :: (Ord a) => Int -> StackSet a -> StackSet a -shift n w = maybe w (\k -> insert k n w) (peek w) - --- | /O(log n)/. Insert an element onto the top of stack 'n'. --- If the element is already in the stack 'n', it is moved to the top. --- If the element exists on another stack, it is removed from that stack. --- If the index is wrong an exception is thrown. -insert :: Ord a => a -> Int -> StackSet a -> StackSet a -insert k n old = new { stacks = M.adjust (k:) n (stacks new) } - where new = delete k old - --- | /O(n)/. Delete an element entirely from from the StackSet. --- If the element doesn't exist, the original StackSet is returned unmodified. --- If the current element is focused, focus will change. -delete :: Ord a => a -> StackSet a -> StackSet a -delete k w = maybe w del $ L.find ((k `elem`) . snd) (M.assocs (stacks w)) - where - del (i,_) = w { stacks = M.adjust (L.delete k) i (stacks w) } - --- | /O(log n)/. Index. Extract the stack at workspace 'n'. --- If the index is invalid, an exception is thrown. -index :: Int -> StackSet a -> [a] -index k w = fromJust (M.lookup k (stacks w)) - --- --- Arbitrary instances and helper functions. --- - ------------------------------------------------------------------------- --- --- Building StackSets from lists --- - -fromList :: Ord a => (Int, [[a]]) -> StackSet a -fromList (_,[]) = error "Cannot build a StackSet from an empty list" -fromList (n,xs) | n < 0 || n >= length xs - = error $ "Cursor index is out of range: " ++ show (n, length xs) -fromList (o,xs) = view o $ - foldr (\(i,ys) s -> - foldr (\a t -> insert a i t) s ys) - (empty (length xs)) (zip [0..] xs) - --- flatten a stackset to a list -toList :: StackSet a -> (Int,[[a]]) -toList x = (current x, map snd $ M.toList (stacks x)) - --- --------------------------------------------------------------------- --- --- Some useful predicates and helpers --- - --- a window is a member -member :: Ord a => a -> StackSet a -> Bool -member k w = - case L.find ((k `elem`) . snd) (M.assocs (stacks w)) of - Nothing -> False - _ -> True - --- | /O(n)/. Number of stacks -size :: T -> Int -size = M.size . stacks - --- | Height of stack 'n' -height :: Int -> T -> Int -height i w = length (index i w) - --- --- Generate arbitrary stacksets --- -instance (Ord a, Arbitrary a) => Arbitrary (StackSet a) where - arbitrary = do - sz <- choose (1,5) - n <- choose (0,sz-1) - ls <- vector sz - let s = fromList (fromIntegral n,ls) - return s - -instance (Ord a, CoArbitrary a) => CoArbitrary (StackSet a) where - coarbitrary s = coarbitrary (toList s) - --- --- QuickSpec stuff. --- - -ordering :: Sig -ordering = signature [ - con "LT" LT, - con "GT" GT, - con "EQ" EQ, - vars ["o", "o'"] (undefined :: Ordering)] - --- --- constrain it to a simple element type --- -type T = StackSet A - -tinywm :: [Sig] -tinywm = [ - prelude (undefined :: A) `without` ["+", "*"], - gvars ["x", "y", "q"] (choose (0, 3) :: Gen Int), - ordering, - - ["s"] `vars` (undefined :: T), - - "empty" `fun1` (empty :: Int -> T), - "view" `fun2` (view :: Int -> T -> T), - "peek" `fun1` (fromJust . peek :: T -> A), - "rotate" `fun2` (rotate :: Ordering -> T -> T), - "push" `fun2` (push :: A -> T -> T), - "shift" `fun2` (shift :: Int -> T -> T), - "insert" `fun3` (insert :: A -> Int -> T -> T), - "delete" `fun2` (delete :: A -> T -> T), - "current" `fun1` (current :: T -> Int), - "index" `fun2` (index :: Int -> T -> [A])] - -main = quickSpec tinywm diff --git a/examples/Zip.hs b/examples/Zip.hs new file mode 100644 --- /dev/null +++ b/examples/Zip.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE TypeApplications #-} +-- A test for conditions. +-- Many laws for zip only hold when the arguments have the same +-- length. +import QuickSpec + +eqLen :: [a] -> [b] -> Bool +eqLen xs ys = length xs == length ys + +main = quickSpec [ + -- Explore bigger terms. + withMaxTermSize 8, + withPruningDepth 10, + con "++" ((++) @ Int), + con "zip" (zip @ Int @ Int), + predicate "eqLen" (eqLen @ Int @ Int) ] diff --git a/quickspec.cabal b/quickspec.cabal --- a/quickspec.cabal +++ b/quickspec.cabal @@ -1,5 +1,5 @@ Name: quickspec -Version: 0.9.6 +Version: 2 Cabal-version: >= 1.6 Build-type: Simple @@ -9,43 +9,60 @@ License: BSD3 License-file: LICENSE -Copyright: 2009-2013 Nick Smallbone +Copyright: 2009-2018 Nick Smallbone Category: Testing Synopsis: Equational laws for free! Description: - QuickSpec automatically finds equational laws about your program. + QuickSpec takes your Haskell code and, as if by magic, discovers laws + about it. You give QuickSpec a collection of Haskell functions; + QuickSpec tests your functions with QuickCheck and prints out laws which + seem to hold. . - 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, which are exactly the ones you - might write by hand: + For example, give QuickSpec the functions @reverse@, @++@ and @[]@, and + it will find six laws: . - > xs++[] == xs - > []++xs == xs - > (xs++ys)++zs == xs++(ys++zs) > reverse [] == [] + > xs ++ [] == xs + > [] ++ xs == xs > reverse (reverse xs) == xs - > reverse xs++reverse ys == reverse (ys++xs) + > (xs ++ ys) ++ zs == xs ++ (ys ++ zs) + > reverse xs ++ reverse ys == reverse (ys ++ xs) . - The laws that QuickSpec generates are not proved correct, but have - passed at least 200 QuickCheck tests. + QuickSpec can find equational laws as well as conditional equations. All + you need to supply are the functions to test, as well as @Ord@ and + @Arbitrary@ instances for QuickSpec to use in testing; the rest is + automatic. . - For more information, see the @README@ file at - https://github.com/nick8325/quickspec/blob/master/README.asciidoc. + For information on how to use QuickSpec, see the documentation in the main + module, "QuickSpec". You can also look in the + @@ + directory, for example at + @@, + @@, or + @@. + To read about how + QuickSpec works, see our paper, + . Extra-source-files: - README.asciidoc + README.md examples/Arith.hs - examples/Arrays.hs examples/Bools.hs examples/Composition.hs - examples/Heaps.hs + examples/Geometry.hs + examples/HugeLists.hs + examples/IntSet.hs + examples/ListMonad.hs examples/Lists.hs + examples/Octonions.hs + examples/Parsing.hs examples/PrettyPrinting.hs - examples/TinyWM.hs - src/Test/QuickSpec/errors.h + examples/PrettyPrintingModel.hs + examples/Regex.hs + examples/Sorted.hs + examples/Zip.hs source-repository head type: git @@ -53,32 +70,42 @@ branch: master library + ghc-options: -W hs-source-dirs: src - include-dirs: src/Test/QuickSpec/ Exposed-modules: - Test.QuickSpec, - Test.QuickSpec.Main, - Test.QuickSpec.Signature, - Test.QuickSpec.Prelude, - Test.QuickSpec.Term, - Test.QuickSpec.Equation, - Test.QuickSpec.Generate, - Test.QuickSpec.TestTree, - Test.QuickSpec.Reasoning.UnionFind, - Test.QuickSpec.Reasoning.CongruenceClosure, - Test.QuickSpec.Reasoning.NaiveEquationalReasoning, - Test.QuickSpec.Reasoning.PartialEquationalReasoning, - Test.QuickSpec.TestTotality, - Test.QuickSpec.Utils, - Test.QuickSpec.Utils.Typeable, - Test.QuickSpec.Utils.Typed, - Test.QuickSpec.Utils.TypeMap, - Test.QuickSpec.Utils.TypeRel, - Test.QuickSpec.Approximate - Other-modules: - -- Dangerous! - Test.QuickSpec.Utils.MemoValuation + QuickSpec + QuickSpec.Explore + QuickSpec.Explore.Conditionals + QuickSpec.Explore.PartialApplication + QuickSpec.Explore.Polymorphic + QuickSpec.Explore.Schemas + QuickSpec.Explore.Terms + QuickSpec.Haskell + QuickSpec.Haskell.Resolve + QuickSpec.Prop + QuickSpec.Pruning + QuickSpec.Pruning.Background + QuickSpec.Pruning.Twee + QuickSpec.Pruning.Types + QuickSpec.Pruning.UntypedTwee + QuickSpec.Term + QuickSpec.Terminal + QuickSpec.Testing + QuickSpec.Testing.DecisionTree + QuickSpec.Testing.QuickCheck + QuickSpec.Type + QuickSpec.Utils Build-depends: - base < 5, containers, transformers, QuickCheck >= 2.7, - random, spoon >= 0.2, array, ghc-prim + QuickCheck >= 2.10, + base >= 4 && < 5, + constraints, + containers, + data-lens-light >= 0.1.1, + dlist, + random, + reflection, + template-haskell, + transformers, + twee-lib >= 2.1.2, + uglymemo diff --git a/src/QuickSpec.hs b/src/QuickSpec.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec.hs @@ -0,0 +1,272 @@ +-- | The main QuickSpec module. Everything you need to run QuickSpec lives here. +-- +-- To run QuickSpec, you need to tell it which functions to test. We call the +-- list of functions the /signature/. Here is an example signature, which tells +-- QuickSpec to test the @++@, @reverse@ and @[]@ functions: +-- +-- @ +-- sig = [ +-- `con` "++" ((++) :: [`A`] -> [`A`] -> [`A`]), +-- `con` "reverse" (reverse :: [`A`] -> [`A`]), +-- `con` "[]" ([] :: [`A`]) ] +-- @ +-- +-- The `con` function, used above, adds a function to the signature, given its +-- name and its value. When declaring polymorphic functions in the signature, +-- we use the types `A` to `E` to represent type variables. +-- Having defined this signature, we can say @`quickSpec` sig@ to test it and +-- see the discovered equations. +-- +-- If you want to test functions over your own datatypes, those types need to +-- implement `Arbitrary` and `Ord` (if the `Ord` instance is a problem, see `Observe`). +-- You must also declare those instances to QuickSpec, by including them in the +-- signature. For monomorphic types you can do this using `monoType`: +-- +-- > data T = ... +-- > main = quickSpec [ +-- > ..., +-- > `monoType` (Proxy :: Proxy T)] +-- +-- You can only declare monomorphic types with `monoType`. If you want to test +-- your own polymorphic types, you must explicitly declare `Arbitrary` and `Ord` +-- instances using the `inst` function. +-- +-- You can also use QuickSpec to find conditional equations. To do so, you need +-- to include some /predicates/ in the signature. These are functions returning +-- `Bool` which can appear as conditions in other equations. Declaring a predicate +-- works just like declaring a function, except that you declare it using +-- `predicate` instead of `con`. +-- +-- You can also put certain options in the signature. The most useful is +-- `withMaxTermSize', which you can use to tell QuickSpec to generate larger +-- equations. +-- +-- The @@ +-- directory contains many examples. Here are some interesting ones: +-- +-- * @@: a simple arithmetic example. Demonstrates basic use of QuickSpec. +-- * @@: list functions. Demonstrates testing polymorphic functions. +-- * @@: sorting. Demonstrates finding conditional equations. +-- * @@: a few functions from "Data.IntSet". Demonstrates testing user-defined datatypes and finding conditional equations. +-- * @@: pretty printing combinators. Demonstrates testing user-defined datatypes and using observational equality. +-- * @@: parser combinators. Demonstrates testing polymorphic datatypes and using observational equality. +-- +-- You can also find some larger case studies in our paper, +-- . + +{-# LANGUAGE ScopedTypeVariables, FlexibleContexts, TypeOperators, MultiParamTypeClasses, FunctionalDependencies #-} +module QuickSpec( + -- * Running QuickSpec + quickSpec, Sig, Signature(..), + + -- * Declaring functions and predicates + con, predicate, + -- ** Type variables for polymorphic functions + A, B, C, D, E, + + -- * Declaring types + monoType, vars, monoTypeWithVars, inst, Observe(..), + + -- * Exploring functions in series + background, series, + + -- * Customising QuickSpec + withMaxTermSize, withMaxTests, withMaxTestSize, defaultTo, + withPruningDepth, withPruningTermSize, withFixedSeed, + + -- * Re-exported functionality + Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary) where + +import QuickSpec.Haskell(Predicateable, TestCase, Names(..), Observe(..)) +import qualified QuickSpec.Haskell as Haskell +import qualified QuickSpec.Haskell.Resolve as Haskell +import qualified QuickSpec.Testing.QuickCheck as QuickCheck +import qualified QuickSpec.Pruning.UntypedTwee as Twee +import Test.QuickCheck +import Test.QuickCheck.Random +import Data.Constraint +import Data.Lens.Light +import QuickSpec.Utils +import QuickSpec.Type hiding (defaultTo) +import Data.Proxy + +-- | Run QuickSpec. See the documentation at the top of this file. +quickSpec :: Signature sig => sig -> IO () +quickSpec signature = + Haskell.quickSpec (sig 0 Haskell.defaultConfig) + where + Sig sig = toSig signature + +-- | A signature. +newtype Sig = Sig (Int -> Haskell.Config -> Haskell.Config) + +instance Monoid Sig where + mempty = Sig (\_ -> id) + Sig sig1 `mappend` Sig sig2 = Sig (\n -> sig2 n . sig1 n) + +-- | A class of things that can be used as a QuickSpec signature. +class Signature sig where + -- | Convert the thing to a signature. + toSig :: sig -> Sig + +instance Signature Sig where + toSig = id + +instance Signature sig => Signature [sig] where + toSig = mconcat . map toSig + +-- | Declare a constant with a given name and value. +-- If the constant you want to use is polymorphic, you can use the types +-- `A`, `B`, `C`, `D`, `E` to monomorphise it, for example: +-- +-- > constant "reverse" (reverse :: [A] -> [A]) +-- +-- QuickSpec will then understand that the constant is really polymorphic. +con :: Typeable a => String -> a -> Sig +con name x = + Sig (\n -> modL Haskell.lens_constants (appendAt n (Haskell.con name x))) + +-- | 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" (`Data.List.delete` :: Int -> [Int] -> [Int]), +-- `con` "insert" (`Data.List.insert` :: Int -> [Int] -> [Int]), +-- predicate "member" (member :: Int -> [Int] -> Bool) ] +-- @ +predicate :: ( Predicateable a + , Typeable a + , Typeable (TestCase a)) + => String -> a -> Sig +predicate name x = + Sig (\n -> modL Haskell.lens_predicates (appendAt n (Haskell.predicate name x))) + +appendAt :: Int -> a -> [[a]] -> [[a]] +appendAt n x [] = appendAt n x [[]] +appendAt 0 x (xs:xss) = (xs ++ [x]):xss +appendAt n x (xs:xss) = xs:appendAt (n-1) x xss + +-- | Declare a new monomorphic type. +-- The type must implement `Ord` and `Arbitrary`. +monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig +monoType _ = + mconcat [ + inst (Sub Dict :: () :- Ord a), + inst (Sub Dict :: () :- Arbitrary a)] + +-- | Declare a new monomorphic type, saying how you want variables of that type to be named. +monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig +monoTypeWithVars xs proxy = + monoType proxy `mappend` vars xs proxy + +-- | Customize how variables of a particular type are named. +vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig +vars xs _ = instFun (Names xs :: Names a) + +-- | 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 @`Data.Map.Map` k v@, you will need to add +-- the following two declarations to your signature: +-- +-- @ +-- `inst` (`Sub` `Dict` :: (Ord A, Ord B) `:-` Ord (Map A B)) +-- `inst` (`Sub` `Dict` :: (Arbitrary A, Arbitrary B) `:-` Arbitrary (Map A B)) +-- @ +inst :: (Typeable c1, Typeable c2) => c1 :- c2 -> Sig +inst = instFun + +instFun :: Typeable a => a -> Sig +instFun x = + Sig (\_ -> modL Haskell.lens_instances (`mappend` Haskell.inst x)) + +-- | 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) ] ] +background :: Signature sig => sig -> Sig +background signature = + Sig (\n -> sig (n+1)) + where + Sig sig = toSig signature + +-- | 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 [sig1, sig2] +-- > where +-- > sig1 = [ +-- > con "0" (0 :: Int), +-- > con "+" ((+) :: Int -> Int -> Int) ] +-- > sig2 = [ +-- > con "++" ((++) :: [A] -> [A] -> [A]), +-- > con "length" (length :: [A] -> Int) ] +series :: Signature sig => [sig] -> Sig +series = foldl op mempty . map toSig + where + op sigs sig = toSig [background sigs, sig] + +-- | Set the maximum size of terms to explore (default: 7). +withMaxTermSize :: Int -> Sig +withMaxTermSize n = Sig (\_ -> setL Haskell.lens_max_size n) + +-- | Set how many times to test each discovered law (default: 1000). +withMaxTests :: Int -> Sig +withMaxTests n = + Sig (\_ -> setL (QuickCheck.lens_num_tests # Haskell.lens_quickCheck) n) + +-- | Set the maximum value for QuickCheck's size parameter when generating test +-- data (default: 20). +withMaxTestSize :: Int -> Sig +withMaxTestSize n = + Sig (\_ -> setL (QuickCheck.lens_max_test_size # Haskell.lens_quickCheck) n) + +-- | Set which type polymorphic terms are tested at. +defaultTo :: Typeable a => proxy a -> Sig +defaultTo proxy = Sig (\_ -> setL Haskell.lens_default_to (typeRep proxy)) + +-- | 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. +withPruningDepth :: Int -> Sig +withPruningDepth n = + Sig (\_ -> setL (Twee.lens_max_cp_depth # Haskell.lens_twee) n) + +-- | 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. +withPruningTermSize :: Int -> Sig +withPruningTermSize n = + Sig (\_ -> setL (Twee.lens_max_term_size # Haskell.lens_twee) n) + +-- | Set the random number seed used for test case generation. +-- Useful if you want repeatable results. +withFixedSeed :: Int -> Sig +withFixedSeed s = Sig (\_ -> setL (QuickCheck.lens_fixed_seed # Haskell.lens_quickCheck) (Just . mkQCGen $ s)) diff --git a/src/QuickSpec/Explore.hs b/src/QuickSpec/Explore.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Explore.hs @@ -0,0 +1,64 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE FlexibleContexts #-} +module QuickSpec.Explore where + +import QuickSpec.Explore.Polymorphic +import QuickSpec.Testing +import QuickSpec.Pruning +import QuickSpec.Term +import QuickSpec.Type +import QuickSpec.Utils +import QuickSpec.Prop +import QuickSpec.Terminal +import Control.Monad +import Control.Monad.Trans.Class +import Control.Monad.Trans.State.Strict +import Text.Printf + +moreTerms :: (Ord a, Apply (Term f), Sized f, Typed f) => Universe -> [f] -> (Term f -> a) -> [[Term f]] -> [Term f] +moreTerms univ funs measure tss = + sortBy' measure $ + atomic ++ + [ unPoly v + | i <- [0..n], + t <- uss !! i, + u <- uss !! (n-i), + Just v <- [tryApply (poly t) (poly u)], + unPoly v `usefulForUniverse` univ ] + where + n = length tss + atomic = + [App f [] | f <- funs, size f == n] ++ + [Var (V typeVar 0) | n == 1] + uss = tss ++ [atomic] + +quickSpec :: + (Ord measure, Ord fun, Ord norm, Sized fun, Typed fun, Ord result, Apply (Term fun), PrettyTerm fun, + MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) => + (Prop (Term fun) -> m ()) -> + (Term fun -> measure) -> + (Term fun -> testcase -> result) -> + Int -> Universe -> [fun] -> m () +quickSpec present measure eval maxSize univ funs = do + let + state0 = initialState univ (\t -> size t <= 5) eval + + loop m n _ | m > n = return () + loop m n tss = do + putStatus (printf "enumerating terms of size %d" m) + let + ts = moreTerms univ funs measure tss + total = length ts + consider (i, t) = do + putStatus (printf "testing terms of size %d: %d/%d" m i total) + res <- explore t + putStatus (printf "testing terms of size %d: %d/%d" m i total) + lift $ mapM_ present (result_props res) + case res of + Accepted _ -> return True + Rejected _ -> return False + us <- map snd <$> filterM consider (zip [1 :: Int ..] ts) + clearStatus + loop (m+1) n (tss ++ [us]) + + evalStateT (loop 0 maxSize []) state0 diff --git a/src/QuickSpec/Explore/Conditionals.hs b/src/QuickSpec/Explore/Conditionals.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Explore/Conditionals.hs @@ -0,0 +1,220 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE DeriveFunctor #-} +module QuickSpec.Explore.Conditionals where + +import QuickSpec.Prop +import QuickSpec.Term +import QuickSpec.Type +import QuickSpec.Pruning +import QuickSpec.Pruning.Background(Background(..)) +import QuickSpec.Testing +import QuickSpec.Terminal +import QuickSpec.Utils +import QuickSpec.Explore.PartialApplication +import QuickSpec.Explore.Polymorphic +import qualified Twee.Base as Twee +import Data.List +import Control.Monad +import Control.Monad.Trans.Class +import Control.Monad.IO.Class + +newtype Conditionals m a = Conditionals (m a) + deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal) +instance MonadTrans Conditionals where + lift = Conditionals +instance (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) => + MonadPruner (Term fun) norm (Conditionals m) where + normaliser = lift $ do + norm <- normaliser + return (norm . fmap Normal) + add prop = do + redundant <- conditionallyRedundant prop + if redundant then return False else do + res <- lift (add (mapFun Normal prop)) + when res (considerConditionalising prop) + return res + +conditionalsUniverse :: (Typed fun, Predicate fun) => [fun] -> Universe +conditionalsUniverse funs = + universe $ + map Normal funs ++ + [ Constructor pred clas_test_case | pred <- funs, Predicate{..} <- [classify pred] ] + +runConditionals :: + (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) => + [fun] -> Conditionals m a -> m a +runConditionals preds mx = + run (mapM_ considerPredicate preds >> mx) + where + run (Conditionals mx) = mx + +class Predicate fun where + classify :: fun -> Classification fun + +data Classification fun = + Predicate { clas_selectors :: [fun], clas_test_case :: Type, clas_true :: Term fun } + | Selector { clas_index :: Int, clas_pred :: fun, clas_test_case :: Type } + | Function + deriving (Eq, Ord, Functor) + +instance (Arity fun, Predicate fun) => Predicate (PartiallyApplied fun) where + classify f = + case getTotal f of + Nothing -> Function + Just f -> fmap total (classify f) + +data WithConstructor fun = + Constructor fun Type + | Normal fun + deriving (Eq, Ord) + +instance Sized fun => Sized (WithConstructor fun) where + size Constructor{} = 0 + size (Normal f) = size f + +instance Arity fun => Arity (WithConstructor fun) where + arity Constructor{} = 1 + arity (Normal f) = arity f + +instance Pretty fun => Pretty (WithConstructor fun) where + pPrintPrec l p (Constructor f _) = pPrintPrec l p f <> text "_con" + pPrintPrec l p (Normal f) = pPrintPrec l p f + +instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where + termStyle (Constructor _ _) = curried + termStyle (Normal f) = termStyle f + +instance PrettyArity fun => PrettyArity (WithConstructor fun) where + prettyArity (Constructor _ _) = 1 + prettyArity (Normal f) = prettyArity f + +instance (Predicate fun, Background fun) => Background (WithConstructor fun) where + background (Normal f) = map (mapFun Normal) (background f) + background _ = [] + +instance Typed fun => Typed (WithConstructor fun) where + typ (Constructor pred ty) = + arrowType (typeArgs (typ pred)) ty + typ (Normal f) = typ f + otherTypesDL (Constructor pred _) = typesDL pred + otherTypesDL (Normal f) = otherTypesDL f + typeSubst_ sub (Constructor pred ty) = Constructor (typeSubst_ sub pred) (typeSubst_ sub ty) + typeSubst_ sub (Normal f) = Normal (typeSubst_ sub f) + +predType :: TyCon -> [Type] -> Type +predType name tys = + Twee.build (Twee.app (Twee.fun name) tys) + +considerPredicate :: + (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) => + fun -> Conditionals m () +considerPredicate f = + case classify f of + Predicate sels ty true -> do + let + x = Var (V ty 0) + eqns = + [App (Constructor f ty) [App (Normal sel) [x] | sel <- sels] === x, + App (Normal f) [App (Normal sel) [x] | sel <- sels] === fmap Normal true] + mapM_ (lift . add) eqns + _ -> return () + +considerConditionalising :: + (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) => + Prop (Term fun) -> Conditionals m () +considerConditionalising (lhs :=>: t :=: u) = do + norm <- normaliser + -- If we have discovered that "somePredicate x_1 x_2 ... x_n = True" + -- we should add the axiom "get_x_n (toSomePredicate x_1 x_2 ... x_n) = x_n" + -- to the set of known equations + case t of + App f ts | Predicate{..} <- classify f -> -- It is an interesting predicate, i.e. it was added by the user + when (norm u == norm clas_true) $ + addPredicate lhs f ts + _ -> return () + +conditionallyRedundant :: + (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) => + Prop (Term fun) -> Conditionals m Bool +conditionallyRedundant (lhs :=>: t :=: u) = do + t' <- normalise t + u' <- normalise u + conditionallyRedundant' lhs t u t' u' + +conditionallyRedundant' :: + (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) => + [Equation (Term fun)] -> Term fun -> Term fun -> norm -> norm -> Conditionals m Bool +conditionallyRedundant' lhs t u t' u' = do + forM_ (usort (funs [t, u])) $ \f -> + case classify f of + Selector{..} -> do + let + Predicate{..} = classify clas_pred + tys = typeArgs (typ clas_pred) + argss = sequence [ [ arg | arg <- terms [t, u] >>= subterms, typ arg == ty ] | ty <- tys ] + forM_ argss $ \args -> do + norm <- normaliser + let p = App clas_pred args + when (norm p == norm clas_true) $ do + addPredicate lhs clas_pred args + _ -> return () + + t'' <- normalise t + u'' <- normalise u + if t'' == u'' then + return True + else if t'' == t' && u'' == u' then + return False + else + conditionallyRedundant' lhs t u t'' u'' + +addPredicate :: + (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) => + [Equation (Term fun)] -> fun -> [Term fun] -> Conditionals m () +addPredicate lhs f ts = do + let Predicate{..} = classify f + ts' = map (fmap Normal) ts + lhs' = map (fmap (fmap Normal)) lhs + -- The "to_p x1 x2 ... xm" term + construction = App (Constructor f clas_test_case) ts' + -- The "p_n (to_p x1 x2 ... xn ... xm) = xn" + -- equations + equations = [ lhs' :=>: App (Normal (clas_selectors !! i)) [construction] :=: x | (x, i) <- zip ts' [0..]] + + -- Declare the relevant equations as axioms + mapM_ (lift . add) equations + +conditionalise :: (PrettyTerm fun, Typed fun, Ord fun, Predicate fun) => Prop (Term fun) -> Prop (Term fun) +conditionalise (lhs :=>: t :=: u) = + go lhs t u + where + -- Replace one predicate with a conditional + go lhs t u = + case [ (p, x, clas_selectors, clas_true) | (App f [Var x]) <- subterms t ++ subterms u, Selector _ p _ <- [classify f], Predicate{..} <- [classify p] ] of + [] -> sort lhs :=>: t :=: u + ((p, x, sels, true):_) -> + let + n = freeVar [t, u] + tys = typeArgs (typ p) + xs = map Var (zipWith V tys [n..]) + subs = [(App (sels !! i) [Var x], xs !! i) | i <- [0..length tys-1]] + in + go ((App p xs :=: true):lhs) (replaceMany subs t) (replaceMany subs u) + + replace from to t + | t == from = to + replace from to (App f ts) = + App f (map (replace from to) ts) + replace _ _ (Var x) = Var x + + replaceMany subs t = + foldr (uncurry replace) t subs diff --git a/src/QuickSpec/Explore/PartialApplication.hs b/src/QuickSpec/Explore/PartialApplication.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Explore/PartialApplication.hs @@ -0,0 +1,89 @@ +-- Pruning support for partial application and the like. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances #-} +module QuickSpec.Explore.PartialApplication where + +import QuickSpec.Term +import QuickSpec.Type +import QuickSpec.Pruning.Background +import QuickSpec.Prop +import qualified Twee.Base as Twee +import Data.Maybe + +data PartiallyApplied f = + -- A partially-applied function symbol. + -- The Int describes how many arguments the function expects. + Partial f Int + -- The ($) operator, for oversaturated applications. + -- The type argument is the type of the first argument to ($). + | Apply Type + deriving (Eq, Ord) + +instance Sized f => Sized (PartiallyApplied f) where + size (Partial f _) = size f + size (Apply _) = 0 + +instance Arity (PartiallyApplied f) where + arity (Partial _ n) = n + arity (Apply _) = 2 + +instance Pretty f => Pretty (PartiallyApplied f) where + pPrint (Partial f _) = pPrint f + pPrint (Apply _) = text "$" + +instance PrettyTerm f => PrettyTerm (PartiallyApplied f) where + termStyle (Partial f _) = termStyle f + termStyle (Apply _) = invisible + +instance PrettyArity f => PrettyArity (PartiallyApplied f) where + prettyArity (Partial f _) = prettyArity f + prettyArity (Apply _) = 1 + +instance Typed f => Typed (PartiallyApplied f) where + typ (Apply ty) = Twee.build (Twee.app (Twee.fun Arrow) [ty, ty]) + typ (Partial f _) = typ f + otherTypesDL (Apply _) = mempty + otherTypesDL (Partial f _) = otherTypesDL f + typeSubst_ sub (Apply ty) = Apply (typeSubst_ sub ty) + typeSubst_ sub (Partial f n) = Partial (typeSubst_ sub f) n + +instance (Arity f, Typed f) => Apply (Term (PartiallyApplied f)) where + tryApply t u = do + tryApply (typ t) (typ u) + return $ + case t of + App (Partial f n) ts | n < arity f -> + App (Partial f (n+1)) (ts ++ [u]) + _ -> + simpleApply t u + +getTotal :: Arity f => PartiallyApplied f -> Maybe f +getTotal (Partial f n) | arity f == n = Just f +getTotal _ = Nothing + +total :: Arity f => f -> PartiallyApplied f +total f = Partial f (arity f) + +simpleApply :: + Typed f => + Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f) +simpleApply t u = + App (Apply (typ t)) [t, u] + +instance (Arity f, Typed f, Background f) => Background (PartiallyApplied f) where + background (Partial f _) = + [ simpleApply (partial n) (vs !! n) === partial (n+1) + | n <- [0..arity f-1] ] ++ + map (mapFun (\f -> Partial f (arity f))) (background f) + where + partial i = + App (Partial f i) (take i vs) + vs = map Var (zipWith V (typeArgs (typ f)) [0..]) + background _ = [] + +instance (Applicative f, Eval fun (Value f)) => Eval (PartiallyApplied fun) (Value f) where + eval var (Partial f _) = eval var f + eval _ (Apply ty) = + fromJust $ + cast (Twee.build (Twee.app (Twee.fun Arrow) [ty, ty])) + (toValue (pure (($) :: (A -> B) -> (A -> B)))) diff --git a/src/QuickSpec/Explore/Polymorphic.hs b/src/QuickSpec/Explore/Polymorphic.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Explore/Polymorphic.hs @@ -0,0 +1,263 @@ +-- Theory exploration which handles polymorphism. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE TemplateHaskell, FlexibleContexts, GeneralizedNewtypeDeriving, FlexibleInstances, MultiParamTypeClasses, BangPatterns, UndecidableInstances, RankNTypes, GADTs, RecordWildCards #-} +module QuickSpec.Explore.Polymorphic(module QuickSpec.Explore.Polymorphic, Result(..)) where + +import qualified QuickSpec.Explore.Schemas as Schemas +import QuickSpec.Explore.Schemas(Schemas, Result(..)) +import QuickSpec.Term +import QuickSpec.Type +import QuickSpec.Testing +import QuickSpec.Pruning +import QuickSpec.Utils +import QuickSpec.Prop +import qualified Data.Map.Strict as Map +import Data.Map(Map) +import qualified Data.Set as Set +import Data.Set(Set) +import Data.Lens.Light +import Control.Monad.Trans.State.Strict +import Control.Monad.Trans.Class +import qualified Twee.Base as Twee +import Control.Monad +import Data.Maybe +import qualified Data.DList as DList + +data Polymorphic testcase result fun norm = + Polymorphic { + pm_schemas :: Schemas testcase result (PolyFun fun) norm, + pm_unifiable :: Map (Poly Type) ([Poly Type], [(Poly Type, Poly Type)]), + pm_accepted :: Map (Poly Type) (Set (Term fun)), + pm_universe :: Universe } + +data PolyFun fun = + PolyFun { fun_original :: fun, fun_specialised :: fun } + deriving (Eq, Ord) + +instance Pretty fun => Pretty (PolyFun fun) where + pPrint = pPrint . fun_specialised + +instance PrettyTerm fun => PrettyTerm (PolyFun fun) where + termStyle = termStyle . fun_specialised + +-- univ_inner: the type universe, with all type variables unified +-- univ_root: the set of types allowed for partially applied functions, only at +-- the root of a term +data Universe = Universe { univ_inner :: Set Type, univ_root :: Set Type } + +makeLensAs ''Polymorphic + [("pm_schemas", "schemas"), + ("pm_unifiable", "unifiable"), + ("pm_accepted", "accepted"), + ("pm_universe", "univ")] + +initialState :: + Universe -> + (Term fun -> Bool) -> + (Term fun -> testcase -> result) -> + Polymorphic testcase result fun norm +initialState univ inst eval = + Polymorphic { + pm_schemas = Schemas.initialState (inst . fmap fun_specialised) (eval . fmap fun_specialised), + pm_unifiable = Map.empty, + pm_accepted = Map.empty, + pm_universe = univ } + +polyFun :: Typed fun => fun -> PolyFun fun +polyFun x = PolyFun x (oneTypeVar x) + +polyTerm :: Typed fun => Term fun -> Term (PolyFun fun) +polyTerm = oneTypeVar . fmap polyFun + +instance Typed fun => Typed (PolyFun fun) where + typ = typ . fun_specialised + otherTypesDL = otherTypesDL . fun_specialised + typeSubst_ _ x = x -- because it's supposed to be monomorphic + +newtype PolyM testcase result fun norm m a = PolyM { unPolyM :: StateT (Polymorphic testcase result fun norm) m a } + deriving (Functor, Applicative, Monad) + +explore :: + (PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun, Apply (Term fun), + MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) => + Term fun -> + StateT (Polymorphic testcase result fun norm) m (Result fun) +explore t = do + univ <- access univ + unless (t `usefulForUniverse` univ) $ + error ("Type " ++ prettyShow (typ t) ++ " not in universe for " ++ prettyShow t) + if not (t `inUniverse` univ) then + return (Accepted []) + else do + let ty = polyTyp (poly t) + addPolyType ty + + unif <- access unifiable + let (here, there) = Map.findWithDefault undefined ty unif + acc <- access accepted + ress1 <- + concat <$> + forM there (\(ty', mgu) -> + forM (Set.toList (Map.findWithDefault undefined ty' acc)) (\u -> + exploreNoMGU (u `at` mgu))) + res <- exploreNoMGU t + ress2 <- + forM here (\mgu -> + exploreNoMGU (t `at` mgu)) + return res { result_props = concatMap result_props (ress1 ++ [res] ++ ress2) } + where + t `at` ty = + fromMaybe undefined (cast (unPoly ty) t) + +exploreNoMGU :: + (PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun, Apply (Term fun), + MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) => + Term fun -> + StateT (Polymorphic testcase result fun norm) m (Result fun) +exploreNoMGU t = do + univ <- access univ + let ty = polyTyp (poly t) + acc <- access accepted + if (t `Set.member` Map.findWithDefault Set.empty ty acc || + not (t `inUniverse` univ)) then return (Rejected []) else do + accepted %= Map.insertWith Set.union ty (Set.singleton t) + schemas1 <- access schemas + (res, schemas2) <- unPolyM (runStateT (Schemas.explore (polyTerm t)) schemas1) + schemas ~= schemas2 + return (mapProps (regeneralise . mapFun fun_original) res) + where + mapProps f (Accepted props) = Accepted (map f props) + mapProps f (Rejected props) = Rejected (map f props) + +addPolyType :: Monad m => Poly Type -> StateT (Polymorphic testcase result fun norm) m () +addPolyType ty = do + unif <- access unifiable + univ <- access univ + unless (ty `Map.member` unif) $ do + let + tys = [(ty', mgu) | ty' <- Map.keys unif, Just mgu <- [polyMgu ty ty']] + ok ty mgu = oneTypeVar ty /= mgu && oneTypeVar (unPoly mgu) `Set.member` univ_root univ + here = [mgu | (_, mgu) <- tys, ok mgu ty] + there = [(ty', mgu) | (ty', mgu) <- tys, ok mgu ty'] + key ty # unifiable ~= Just (here, there) + forM_ there $ \(ty', _) -> + sndLens # keyDefault ty' undefined # unifiable %= (there ++) + +instance (PrettyTerm fun, Ord fun, Typed fun, Apply (Term fun), MonadPruner (Term fun) norm m) => + MonadPruner (Term (PolyFun fun)) norm (PolyM testcase result fun norm m) where + normaliser = PolyM $ do + norm <- normaliser + return (norm . fmap fun_specialised) + add prop = PolyM $ do + univ <- access univ + let insts = typeInstances univ (regeneralise (mapFun fun_original prop)) + or <$> mapM add insts + +instance MonadTester testcase (Term fun) m => + MonadTester testcase (Term (PolyFun fun)) (PolyM testcase result fun norm m) where + test prop = PolyM $ lift (test (mapFun fun_original prop)) + +-- Given a property which only contains one type variable, +-- add as much polymorphism to the property as possible. +-- e.g. map (f :: a -> a) (xs++ys) = map f xs++map f ys +-- becomes map (f :: a -> b) (xs++ys) = map f xs++map f ys. +regeneralise :: (PrettyTerm fun, Typed fun, Apply (Term fun)) => Prop (Term fun) -> Prop (Term fun) +regeneralise = + -- First replace each type variable occurrence with a fresh + -- type variable (generalise), then unify type variables + -- where necessary to preserve well-typedness (restrict). + restrict . unPoly . generalise + where + generalise (lhs :=>: rhs) = + polyApply (:=>:) (polyList (map genLit lhs)) (genLit rhs) + genLit (t :=: u) = polyApply (:=:) (genTerm t) (genTerm u) + genTerm (Var (V ty x)) = + -- It's tempting to return Var (V typeVar x) here. + -- But this is wrong! + -- In the case of the type (), we get the law x == y :: (), + -- which we must not generalise to x == y :: a. + poly (Var (V (genType ty) x)) + genTerm (App f ts) = + let + -- Need to polymorphise all of ts together so that type variables which + -- only occur in subterms of ts don't get unified + (f', us) = unPoly (polyPair (poly f) (polyList (map genTerm ts))) + Just ty = fmap unPoly (polyMgu (polyTyp (poly f')) (polyApply arrowType (poly (map typ us)) (poly typeVar))) + tys = take (length us) (typeArgs ty) + Just f'' = cast ty f' + Just us' = sequence (zipWith cast tys us) + in + poly (App f'' us') + + genType = Twee.build . aux 0 . Twee.singleton + where + aux !_ Twee.Empty = mempty + aux n (Twee.Cons (Twee.Var _) ts) = + Twee.var (Twee.V n) `mappend` aux (n+1) ts + aux n (Twee.Cons (Twee.App f ts) us) = + Twee.app f (aux n ts) `mappend` + aux (n+Twee.lenList ts) us + + restrict prop = typeSubst sub prop + where + Just sub = Twee.unifyList (Twee.buildList (map fst cs)) (Twee.buildList (map snd cs)) + cs = [(var_ty x, var_ty y) | x:xs <- vs, y <- xs] ++ concatMap litCs (lhs prop) ++ litCs (rhs prop) + -- Two variables that were equal before generalisation must have the + -- same type afterwards + vs = partitionBy skel (concatMap vars (terms prop >>= subterms)) + skel (V ty x) = V (oneTypeVar ty) x + litCs (t :=: u) = [(typ t, typ u)] + +typeInstances :: (Pretty a, PrettyTerm fun, Symbolic fun a, Ord fun, Typed fun, Typed a) => Universe -> a -> [a] +typeInstances Universe{..} prop = + [ typeSubst (\x -> Map.findWithDefault (error ("not found: " ++ prettyShow x)) x sub) prop + | sub <- cs ] + where + cs = + foldr intersection [Map.empty] + (map (constrain (Set.toList univ_inner)) + (usort (DList.toList (termsDL prop) >>= properSubterms)) ++ + map (constrain (Set.toList univ_root)) + (usort (DList.toList (termsDL prop)))) + + constrain tys t = + usort [ Map.fromList (Twee.substToList sub) | u <- tys, Just sub <- [Twee.match (typ t) u] ] + +intersection :: [Map Twee.Var Type] -> [Map Twee.Var Type] -> [Map Twee.Var Type] +ms1 `intersection` ms2 = usort [ Map.union m1 m2 | m1 <- ms1, m2 <- ms2, ok m1 m2 ] + where + ok m1 m2 = and [ Map.lookup x m1 == Map.lookup x m2 | x <- Map.keys (Map.intersection m1 m2) ] + +universe :: Typed a => [a] -> Universe +universe xs = Universe (Set.fromList base) (Set.fromList (withFunctions base)) + where + -- The universe contains the type variable "a", the argument and + -- result type of every function (with all type variables unified), and all + -- subterms of these types + base = usort $ typeVar:concatMap (oneTypeVar . typs . typ) xs + typs ty = (typeRes ty:typeArgs ty) >>= Twee.subterms + + -- We then add partial applications, according to the rule: + -- if f : A1 -> ... -> An -> B is a function in the signature, + -- and s(A1)...s(An), s(B) are in the universe where s is a substitution, + -- then s(A1 -> ... -> An -> B) is in the universe, together with all subterms + withFunctions tys = + tys ++ + concat [func Twee.emptySubst (typ f) tys >>= Twee.subterms | f <- xs] + + func sub ty tys = + filter (`elem` tys) [oneTypeVar (typeSubst sub ty)] ++ + [ arrowType [t'] u' + | Just (t, u) <- [unpackArrow ty], + t' <- tys, + Just sub <- [Twee.matchIn sub t t'], + u' <- func sub u tys ] + +inUniverse :: Typed fun => Term fun -> Universe -> Bool +t `inUniverse` Universe{..} = + and [oneTypeVar (typ u) `Set.member` univ_inner | u <- subterms t] + +usefulForUniverse :: Typed fun => Term fun -> Universe -> Bool +t `usefulForUniverse` Universe{..} = + oneTypeVar (typ t) `Set.member` univ_root && + and [oneTypeVar (typ u) `Set.member` univ_inner | u <- properSubterms t] diff --git a/src/QuickSpec/Explore/Schemas.hs b/src/QuickSpec/Explore/Schemas.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Explore/Schemas.hs @@ -0,0 +1,157 @@ +-- Theory exploration which works on a schema at a time. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TupleSections, TemplateHaskell, MultiParamTypeClasses, FlexibleInstances #-} +module QuickSpec.Explore.Schemas where + +import qualified Data.Map.Strict as Map +import Data.Map(Map) +import QuickSpec.Prop +import QuickSpec.Pruning +import QuickSpec.Term +import QuickSpec.Type +import QuickSpec.Testing +import QuickSpec.Utils +import qualified QuickSpec.Explore.Terms as Terms +import QuickSpec.Explore.Terms(Terms) +import Control.Monad.Trans.State.Strict hiding (State) +import Data.List +import Data.Ord +import Data.Lens.Light +import qualified Data.Set as Set +import Data.Set(Set) +import Data.Maybe +import Control.Monad + +data Schemas testcase result fun norm = + Schemas { + sc_instantiate_singleton :: Term fun -> Bool, + sc_empty :: Terms testcase result (Term fun) norm, + sc_classes :: Terms testcase result (Term fun) norm, + sc_instantiated :: Set (Term fun), + sc_instances :: Map (Term fun) (Terms testcase result (Term fun) norm) } + +makeLensAs ''Schemas + [("sc_classes", "classes"), + ("sc_instances", "instances"), + ("sc_instantiated", "instantiated")] + +instance_ :: Ord fun => Term fun -> Lens (Schemas testcase result fun norm) (Terms testcase result (Term fun) norm) +instance_ t = reading (\Schemas{..} -> keyDefault t sc_empty # instances) + +initialState :: + (Term fun -> Bool) -> + (Term fun -> testcase -> result) -> + Schemas testcase result fun norm +initialState inst eval = + Schemas { + sc_instantiate_singleton = inst, + sc_empty = Terms.initialState eval, + sc_classes = Terms.initialState eval, + sc_instantiated = Set.empty, + sc_instances = Map.empty } + +data Result fun = + Accepted { result_props :: [Prop (Term fun)] } + | Rejected { result_props :: [Prop (Term fun)] } + +-- The schema is represented as a term where there is only one distinct variable of each type +explore :: + (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun, + MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) => + Term fun -> StateT (Schemas testcase result fun norm) m (Result fun) +explore t0 = do + let t = mostSpecific t0 + res <- zoom classes (Terms.explore t) + case res of + Terms.Singleton -> do + inst <- gets sc_instantiate_singleton + if inst t then + instantiateRep t + else do + -- Add the most general instance of the schema + zoom (instance_ t) (Terms.explore (mostGeneral t0)) + return (Accepted []) + Terms.Discovered ([] :=>: _ :=: u) -> + exploreIn u t + Terms.Knew ([] :=>: _ :=: u) -> + exploreIn u t + _ -> error "term layer returned non-equational property" + +{-# INLINEABLE exploreIn #-} +exploreIn :: + (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun, + MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) => + Term fun -> Term fun -> + StateT (Schemas testcase result fun norm) m (Result fun) +exploreIn rep t = do + -- First check if schema is redundant + res <- zoom (instance_ rep) (Terms.explore (mostGeneral t)) + case res of + Terms.Discovered prop -> do + add prop + return (Rejected [prop]) + Terms.Knew _ -> + return (Rejected []) + Terms.Singleton -> do + -- Instantiate rep too if not already done + inst <- access instantiated + props <- + if Set.notMember rep inst + then result_props <$> instantiateRep rep + else return [] + res <- instantiate rep t + return res { result_props = props ++ result_props res } + +{-# INLINEABLE instantiateRep #-} +instantiateRep :: + (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun, + MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) => + Term fun -> + StateT (Schemas testcase result fun norm) m (Result fun) +instantiateRep t = do + instantiated %= Set.insert t + instantiate t t + +{-# INLINEABLE instantiate #-} +instantiate :: + (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun, + MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) => + Term fun -> Term fun -> + StateT (Schemas testcase result fun norm) m (Result fun) +instantiate rep t = zoom (instance_ rep) $ do + let instances = sortBy (comparing generality) (allUnifications (mostGeneral t)) + Accepted <$> catMaybes <$> forM instances (\t -> do + res <- Terms.explore t + case res of + Terms.Discovered prop -> do + add prop + return (Just prop) + _ -> return Nothing) + +-- sortBy (comparing generality) should give most general instances first. +generality :: Term f -> (Int, [Var]) +generality t = (-length (usort (vars t)), vars t) + +-- | Instantiate a schema by making all the variables different. +mostGeneral :: Term f -> Term f +mostGeneral s = evalState (aux s) Map.empty + where + aux (Var (V ty _)) = do + m <- get + let n = Map.findWithDefault 0 ty m + put $! Map.insert ty (n+1) m + return (Var (V ty n)) + aux (App f xs) = fmap (App f) (mapM aux xs) + +mostSpecific :: Term f -> Term f +mostSpecific = subst (\(V ty _) -> Var (V ty 0)) + +allUnifications :: Term fun -> [Term fun] +allUnifications t = map f ss + where + vs = [ map (x,) (select xs) | xs <- partitionBy typ (usort (vars t)), x <- xs ] + ss = map Map.fromList (sequence vs) + go s x = Map.findWithDefault undefined x s + f s = subst (Var . go s) t + select [V ty x] = [V ty x, V ty (succ x)] + select xs = take 4 xs diff --git a/src/QuickSpec/Explore/Terms.hs b/src/QuickSpec/Explore/Terms.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Explore/Terms.hs @@ -0,0 +1,105 @@ +-- Theory exploration which accepts one term at a time. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TemplateHaskell #-} +module QuickSpec.Explore.Terms where + +import qualified Data.Map.Strict as Map +import Data.Map(Map) +import QuickSpec.Term +import QuickSpec.Prop +import QuickSpec.Type +import QuickSpec.Pruning +import QuickSpec.Testing +import QuickSpec.Testing.DecisionTree hiding (Result, Singleton) +import Control.Monad.Trans.State.Strict hiding (State) +import Data.Lens.Light +import QuickSpec.Utils + +data Terms testcase result term norm = + Terms { + -- Empty decision tree. + tm_empty :: DecisionTree testcase result term, + -- Terms already explored. These are stored in the *values* of the map. + -- The keys are those terms but normalised. + -- We do it like this so that explore can guarantee to always return + -- the same representative for each equivalence class (see below). + tm_terms :: Map norm term, + -- Decision tree mapping test case results to terms. + -- Terms are not stored normalised. + -- Terms of different types must not be equal, because that results in + -- ill-typed equations and bad things happening in the pruner. + tm_tree :: Map Type (DecisionTree testcase result term) } + +makeLensAs ''Terms [("tm_tree", "tree")] + +treeForType :: Type -> Lens (Terms testcase result term norm) (DecisionTree testcase result term) +treeForType ty = reading (\Terms{..} -> keyDefault ty tm_empty # tree) + +initialState :: + (term -> testcase -> result) -> + Terms testcase result term norm +initialState eval = + Terms { + tm_empty = empty eval, + tm_terms = Map.empty, + tm_tree = Map.empty } + +data Result term = + -- Discovered a new law. + Discovered (Prop term) + -- Term is equal to an existing term so redundant. + | Knew (Prop term) + | Singleton + +-- The Prop returned is always t :=: u, where t is the term passed to explore +-- and u is the representative of t's equivalence class, not normalised. +-- The representatives of the equivalence classes are guaranteed not to change. +-- +-- Discovered properties are not added to the pruner. +explore :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) => + term -> StateT (Terms testcase result term norm) m (Result term) +explore t = do + res <- explore' t + -- case res of + -- Discovered prop -> traceM ("discovered " ++ prettyShow prop) + -- Knew prop -> traceM ("knew " ++ prettyShow prop) + -- Singleton -> traceM ("singleton " ++ prettyShow t) + return res +explore' :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) => + term -> StateT (Terms testcase result term norm) m (Result term) +explore' t = do + norm <- normaliser + exp norm $ \prop -> do + res <- test prop + case res of + Nothing -> do + return (Discovered prop) + Just tc -> do + treeForType ty %= addTestCase tc + exp norm $ + error "returned counterexample failed to falsify property" + + where + ty = typ t + exp norm found = do + tm@Terms{..} <- get + case Map.lookup t' tm_terms of + Just u -> return (Knew (t === u)) + Nothing -> + case insert t (tm ^. treeForType ty) of + Distinct tree -> do + put (setL (treeForType ty) tree tm { tm_terms = Map.insert t' t tm_terms }) + return Singleton + EqualTo u + -- tm_terms is not kept normalised wrt the discovered laws; + -- instead, we normalise it lazily like so. + | t' == u' -> do + put tm { tm_terms = Map.insert u' u tm_terms } + return (Knew prop) + -- Ask QuickCheck for a counterexample to the property. + | otherwise -> found prop + where + u' = norm u + prop = t === u + where + t' = norm t diff --git a/src/QuickSpec/Haskell.hs b/src/QuickSpec/Haskell.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Haskell.hs @@ -0,0 +1,470 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ScopedTypeVariables, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, RecordWildCards, TemplateHaskell, UndecidableInstances, DefaultSignatures, FunctionalDependencies #-} +module QuickSpec.Haskell where + +import QuickSpec.Haskell.Resolve +import QuickSpec.Type +import QuickSpec.Prop +import Test.QuickCheck hiding (total) +import Data.Constraint +import Data.Proxy +import qualified Twee.Base as B +import QuickSpec.Term +import Data.Functor.Identity +import Data.Maybe +import Data.MemoUgly +import Test.QuickCheck.Gen +import Test.QuickCheck.Random +import System.Random +import Data.Char +import Data.Ord +import qualified QuickSpec.Testing.QuickCheck as QuickCheck +import qualified QuickSpec.Pruning.Twee as Twee +import qualified QuickSpec.Explore +import QuickSpec.Explore.PartialApplication +import QuickSpec.Pruning.Background(Background) +import Control.Monad +import Control.Monad.Trans.State.Strict +import QuickSpec.Terminal +import Text.Printf +import Data.Reflection hiding (D) +import QuickSpec.Utils +import GHC.TypeLits +import QuickSpec.Explore.Conditionals + +baseInstances :: Instances +baseInstances = + mconcat [ + -- Generate tuple values (pairs and () are built into findInstance) + inst $ \(x :: A) (y :: B) (z :: C) -> (x, y, z), + inst $ \(x :: A) (y :: B) (z :: C) (w :: D) -> (x, y, z, w), + inst $ \(x :: A) (y :: B) (z :: C) (w :: D) (v :: E) -> (x, y, z, w, v), + -- Split conjunctions of typeclasses into individuals + inst $ \() -> Dict :: Dict (), + inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) -> Dict :: Dict (ClassA, ClassB), + inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) -> Dict :: Dict (ClassA, ClassB, ClassC), + inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD), + inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) (Dict :: Dict ClassE) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD, ClassE), + -- Derive typeclass instances using (:-) + -- N.B. flip is there to resolve (:-) first to reduce backtracking + inst $ flip $ \(Dict :: Dict ClassA) (Sub Dict :: ClassA :- ClassB) -> Dict :: Dict ClassB, + -- Standard names + inst $ \(Names names :: Names A) -> + Names (map (++ "s") names) :: Names [A], + inst (Names ["p", "q", "r"] :: Names (A -> Bool)), + inst (Names ["f", "g", "h"] :: Names (A -> B)), + inst (Names ["x", "y", "z", "w"] :: Names A), + -- Standard instances + baseType (Proxy :: Proxy ()), + baseType (Proxy :: Proxy Int), + baseType (Proxy :: Proxy Integer), + baseType (Proxy :: Proxy Bool), + baseType (Proxy :: Proxy Char), + inst (Sub Dict :: () :- CoArbitrary ()), + inst (Sub Dict :: () :- CoArbitrary Int), + inst (Sub Dict :: () :- CoArbitrary Integer), + inst (Sub Dict :: () :- CoArbitrary Bool), + inst (Sub Dict :: () :- CoArbitrary Char), + inst (Sub Dict :: Eq A :- Eq [A]), + inst (Sub Dict :: Ord A :- Ord [A]), + inst (Sub Dict :: Arbitrary A :- Arbitrary [A]), + inst (Sub Dict :: CoArbitrary A :- CoArbitrary [A]), + inst (Sub Dict :: Eq A :- Eq (Maybe A)), + inst (Sub Dict :: Ord A :- Ord (Maybe A)), + inst (Sub Dict :: Arbitrary A :- Arbitrary (Maybe A)), + inst (Sub Dict :: CoArbitrary A :- CoArbitrary (Maybe A)), + inst (Sub Dict :: (Eq A, Eq B) :- Eq (Either A B)), + inst (Sub Dict :: (Ord A, Ord B) :- Ord (Either A B)), + inst (Sub Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (Either A B)), + inst (Sub Dict :: (CoArbitrary A, CoArbitrary B) :- CoArbitrary (Either A B)), + inst (Sub Dict :: (Eq A, Eq B) :- Eq (A, B)), + inst (Sub Dict :: (Ord A, Ord B) :- Ord (A, B)), + inst (Sub Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (A, B)), + inst (Sub Dict :: (CoArbitrary A, CoArbitrary B) :- CoArbitrary (A, B)), + inst (Sub Dict :: (Eq A, Eq B, Eq C) :- Eq (A, B, C)), + inst (Sub Dict :: (Ord A, Ord B, Ord C) :- Ord (A, B, C)), + inst (Sub Dict :: (Arbitrary A, Arbitrary B, Arbitrary C) :- Arbitrary (A, B, C)), + inst (Sub Dict :: (CoArbitrary A, CoArbitrary B, CoArbitrary C) :- CoArbitrary (A, B, C)), + inst (Sub Dict :: (Eq A, Eq B, Eq C, Eq D) :- Eq (A, B, C, D)), + inst (Sub Dict :: (Ord A, Ord B, Ord C, Ord D) :- Ord (A, B, C, D)), + inst (Sub Dict :: (Arbitrary A, Arbitrary B, Arbitrary C, Arbitrary D) :- Arbitrary (A, B, C, D)), + inst (Sub Dict :: (CoArbitrary A, CoArbitrary B, CoArbitrary C, CoArbitrary D) :- CoArbitrary (A, B, C, D)), + inst (Sub Dict :: (CoArbitrary A, Arbitrary B) :- Arbitrary (A -> B)), + inst (Sub Dict :: (Arbitrary A, CoArbitrary B) :- CoArbitrary (A -> B)), + inst (Sub Dict :: Ord A :- Eq A), + -- From Arbitrary to Gen + inst $ \(Dict :: Dict (Arbitrary A)) -> arbitrary :: Gen A, + inst $ \(dict :: Dict ClassA) -> return dict :: Gen (Dict ClassA), + -- Observe + inst (\(Dict :: Dict (Observe A B C)) -> Observe2 (do { env <- arbitrary; return (\x -> observe env (x :: C)) })), + inst (Sub Dict :: (Arbitrary A, Observe B C D) :- Observe (A, B) C (A -> D)), + inst (\(Dict :: Dict (Ord A)) -> Observe2 (return id) :: Observe2 A A), + inst (\(Observe2 obsm :: Observe2 B C) (xm :: Gen A) -> + Observe2 (do {x <- xm; obs <- obsm; return (\f -> obs (f x))}) :: Observe2 (A -> B) C), + inst (\(obs :: Observe2 A B) -> Observe1 (toValue obs))] + +-- | A typeclass for types which support observational equality, typically used +-- for types that have no `Ord` instance. +-- +-- An instance @Observe test outcome a@ declares that values of type @a@ can be +-- /tested/ for equality by random testing. You supply a function +-- @observe :: test -> outcome -> a@. Then, two values @x@ and @y@ are considered +-- equal, if for many random values of type @test@, @observe test x == observe test y@. +-- +-- For an example of using observational equality, see @@. +-- +-- You must use `QuickSpec.inst` to add the @Observe@ instance to your signature. +-- Note that `QuickSpec.monoType` requires an `Ord` instance, so this even applies for +-- monomorphic types. Don't forget to add the `Arbitrary` instance too in that case. +class (Arbitrary test, Ord outcome) => Observe test outcome a | a -> test outcome where + -- | Make an observation on a value. Should satisfy the following law: if + -- @x /= y@, then there exists a value of @test@ such that @observe test x /= observe test y@. + observe :: test -> a -> outcome + + default observe :: (test ~ (), outcome ~ a) => test -> a -> outcome + observe _ x = x + +instance (Arbitrary a, Observe test outcome b) => Observe (a, test) outcome (a -> b) where + observe (x, obs) f = observe obs (f x) + +data Observe2 a b where + Observe2 :: Ord b => Gen (a -> b) -> Observe2 a b + deriving Typeable +data Observe1 a = Observe1 (Value (Observe2 a)) deriving Typeable + +-- | Declare that values of a particular type should be compared by observational equality. +-- +-- See @examples/PrettyPrinting.hs@ for an example. +-- +-- XXX mention what instances must be in scope +-- XXX remove constraints etc +-- observe :: Ord res => Gen env -> (env -> val -> res) -> Observe val res +-- observe gen f = +-- Observe (do { env <- gen; return (\x -> f env x) }) + + +-- data SomeObserve a = forall args res. (Ord res, Arbitrary args) => SomeObserve (a -> args -> res) deriving Typeable + +baseType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Instances +baseType _ = + mconcat [ + inst (Dict :: Dict (Ord a)), + inst (Dict :: Dict (Arbitrary a))] + +-- | Declare what variable names you would like to use for values of a particular type. See also `baseTypeNames`. +newtype Names a = Names { getNames :: [String] } + +names :: Instances -> Type -> [String] +names insts ty = + case findInstance insts (skolemiseTypeVars ty) of + (x:_) -> ofValue getNames x + [] -> error "don't know how to name variables" + +arbitraryVal :: Type -> Instances -> Gen (Var -> Value Maybe, Value Identity -> Maybe (Value Ordy)) +arbitraryVal def insts = + MkGen $ \g n -> + let (g1, g2) = split g in + (memo $ \(V ty x) -> + case genType ty of + Nothing -> + fromJust $ cast (defaultTo def ty) (toValue (Nothing :: Maybe A)) + Just gen -> + forValue gen $ \gen -> + Just (unGen (coarbitrary x gen) g1 n), + ordyVal g2 n) + where + genType :: Type -> Maybe (Value Gen) + genType = memo $ \ty -> + case findInstance insts (defaultTo def ty) of + [] -> Nothing + (gen:_) -> + Just (mapValue (coarbitrary ty) gen) + + ordyVal :: QCGen -> Int -> Value Identity -> Maybe (Value Ordy) + ordyVal g n x = + let ty = defaultTo def (typ x) in + case ordyTy ty of + Nothing -> Nothing + Just f -> Just (unGen f g n x) + + ordyTy :: Type -> Maybe (Gen (Value Identity -> Value Ordy)) + ordyTy = memo $ \ty -> + case findInstance insts ty :: [Value Observe1] of + [] -> Nothing + (val:_) -> + case unwrap val of + Observe1 val `In` w1 -> + case unwrap val of + Observe2 obs `In` w2 -> + Just $ + MkGen $ \g n -> + let observe = unGen obs g n in + \x -> wrap w2 (Ordy (observe (runIdentity (reunwrap w1 x)))) + +data Ordy a where Ordy :: Ord a => a -> Ordy a +instance Eq (Value Ordy) where x == y = compare x y == EQ + +instance Ord (Value Ordy) where + compare x y = + compare (typ x) (typ y) `mappend` + case unwrap x of + Ordy xv `In` w -> + let Ordy yv = reunwrap w y in + compare xv yv + +evalHaskell :: (Given Type, Typed f, PrettyTerm f, Eval f (Value Maybe)) => (Var -> Value Maybe, Value Identity -> Maybe (Value Ordy)) -> Term f -> Either (Value Ordy) (Term f) +evalHaskell (env, obs) t = + case unwrap (eval env t) of + Nothing `In` _ -> Right t + Just val `In` w -> + case obs (wrap w (Identity val)) of + Nothing -> Right t + Just ordy -> Left ordy + +data Constant = + Constant { + con_name :: String, + con_style :: TermStyle, + con_pretty_arity :: Int, + con_value :: Value Identity, + con_size :: Int, + con_classify :: Classification Constant } + +instance Eq Constant where + x == y = + con_name x == con_name y && typ (con_value x) == typ (con_value y) + +instance Ord Constant where + compare = + comparing $ \con -> + (con_name con, twiddle (arity con), typ con) + where + -- This trick comes from Prover9 and improves the ordering somewhat + twiddle 1 = 2 + twiddle 2 = 1 + twiddle x = x + +instance Background Constant + +con :: Typeable a => String -> a -> Constant +con name val = + constant' name (toValue (Identity val)) + +constant' :: String -> Value Identity -> Constant +constant' name val = + Constant { + con_name = name, + con_style = + case () of + _ | name == "()" -> curried + | take 1 name == "," -> fixedArity (length name+1) tupleStyle + | take 2 name == "(," -> fixedArity (length name-1) tupleStyle + | isOp name && typeArity (typ val) >= 2 -> infixStyle 5 + | isOp name -> prefix + | otherwise -> curried, + con_pretty_arity = + case () of + _ | isOp name && typeArity (typ val) >= 2 -> 2 + | isOp name -> 1 + | otherwise -> typeArity (typ val), + con_value = val, + con_size = 1, + con_classify = Function } + +isOp :: String -> Bool +isOp "[]" = False +isOp ('"':_) = False +isOp xs | all (== '.') xs = True +isOp xs = not (all isIdent xs) + where + isIdent x = isAlphaNum x || x == '\'' || x == '_' || x == '.' + +instance Typed Constant where + typ = typ . con_value + otherTypesDL con = + case con_classify con of + Predicate{..} -> + -- Don't call typesDL on clas_selectors because it in turn + -- contains a reference to the predicate + typesDL (map con_value clas_selectors) `mplus` typesDL clas_test_case `mplus` typesDL clas_true + Selector{..} -> + typesDL clas_pred `mplus` typesDL clas_test_case + Function -> mzero + typeSubst_ sub con = + con { con_value = typeSubst_ sub (con_value con), + con_classify = fmap (typeSubst_ sub) (con_classify con) } + +instance Pretty Constant where + pPrint = text . con_name + +instance PrettyTerm Constant where + termStyle = con_style + +instance PrettyArity Constant where + prettyArity = con_pretty_arity + +instance Sized Constant where + size = con_size + +instance Arity Constant where + arity = typeArity . typ + +instance Predicate Constant where + classify = con_classify + +instance (Given Type, Applicative f) => Eval Constant (Value f) where + eval _ = mapValue (pure . runIdentity) . con_value + +class Predicateable a where + uncrry :: a -> TestCase a -> Bool + +instance Predicateable Bool where + uncrry = const + +instance forall a b. (Predicateable b, Typeable a, TestCase (a -> b) ~ (a, TestCase b)) => Predicateable (a -> b) where + uncrry f (a, b) = uncrry (f a) b + +-- Foldr over functions +type family (Foldr f b fun) :: * where + Foldr f def (a -> b) = f a (Foldr f def b) + Foldr f def b = def + +-- A test case for predicates of type a +-- if `a ~ A -> B -> C -> Bool` we get `TestCase a ~ (A, (B, (C, ())))` +-- +-- Some speedup should be possible by using unboxed tuples instead... +type TestCase a = Foldr (,) () a + +data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a } + +-- A `suchThat` generator for a predicate +genSuchThat :: (Predicateable a, Arbitrary (TestCase a)) => a -> Gen (TestCaseWrapped x (TestCase a)) +genSuchThat p = TestCaseWrapped <$> arbitrary `suchThat` uncrry p + +data PredRep = PredRep { predInstances :: Instances + , predCon :: Constant + , predCons :: [Constant] } + +true :: Constant +true = con "True" True + +trueTerm :: Term (PartiallyApplied Constant) +trueTerm = App (total true) [] + +-- | Declare a predicate with a given name and value. +-- The predicate should have type @... -> Bool@. +predicate :: forall a. ( Predicateable a + , Typeable a + , Typeable (TestCase a)) + => String -> a -> PredRep +predicate name pred = + case someSymbolVal name of + SomeSymbol (_ :: Proxy sym) -> + let + instances = + inst (\(dict :: Dict (Arbitrary (TestCase a))) -> (withDict dict genSuchThat) pred :: Gen (TestCaseWrapped sym (TestCase a))) + `mappend` + inst (Names [name ++ "_var"] :: Names (TestCaseWrapped sym (TestCase a))) + + conPred = (con name pred) { con_classify = Predicate conSels ty (App true []) } + conSels = [ (constant' (name ++ "_" ++ show i) (select i)) { con_classify = Selector i conPred ty, con_size = 0 } | i <- [0..typeArity (typeOf pred)-1] ] + + select i = + fromJust (cast (arrowType [ty] (typeArgs (typeOf pred) !! i)) (unPoly (compose (sel i) unwrapV))) + where + compose f g = apply (apply cmpV f) g + sel 0 = fstV + sel n = compose (sel (n-1)) sndV + fstV = toPolyValue (fst :: (A, B) -> A) + sndV = toPolyValue (snd :: (A, B) -> B) + cmpV = toPolyValue ((.) :: (B -> C) -> (A -> B) -> A -> C) + unwrapV = toPolyValue (unTestCaseWrapped :: TestCaseWrapped SymA A -> A) + + ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (TestCase a))) + in + PredRep instances conPred (conPred:conSels) + +data Config = + Config { + cfg_quickCheck :: QuickCheck.Config, + cfg_twee :: Twee.Config, + cfg_max_size :: Int, + cfg_instances :: Instances, + cfg_constants :: [[Constant]], + cfg_predicates :: [[PredRep]], + cfg_default_to :: Type } + +makeLensAs ''Config + [("cfg_quickCheck", "lens_quickCheck"), + ("cfg_twee", "lens_twee"), + ("cfg_max_size", "lens_max_size"), + ("cfg_instances", "lens_instances"), + ("cfg_constants", "lens_constants"), + ("cfg_predicates", "lens_predicates"), + ("cfg_default_to", "lens_default_to")] + +defaultConfig :: Config +defaultConfig = + Config { + cfg_quickCheck = QuickCheck.Config { QuickCheck.cfg_num_tests = 1000, QuickCheck.cfg_max_test_size = 20, QuickCheck.cfg_fixed_seed = Nothing }, + cfg_twee = Twee.Config { Twee.cfg_max_term_size = minBound, Twee.cfg_max_cp_depth = maxBound }, + cfg_max_size = 7, + cfg_instances = mempty, + cfg_constants = [], + cfg_predicates = [], + cfg_default_to = typeRep (Proxy :: Proxy Int) } + +quickSpec :: Config -> IO () +quickSpec Config{..} = give cfg_default_to $ do + let + constantsOf f = true:f cfg_constants ++ f (map (concatMap predCons) cfg_predicates) + constants = constantsOf concat + univ = conditionalsUniverse constants + instances = mconcat (cfg_instances:map predInstances (concat cfg_predicates) ++ [baseInstances]) + + present prop = do + n :: Int <- get + put (n+1) + putLine (printf "%3d. %s" n (show (prettyProp (names instances) (conditionalise prop) <+> maybeType prop))) + + -- Add a type signature when printing the equation x = y. + maybeType (_ :=>: x@(Var _) :=: Var _) = + text "::" <+> pPrintType (typ x) + maybeType _ = pPrintEmpty + + mainOf f g = do + printConstants (f cfg_constants ++ f (map (map predCon) cfg_predicates)) + putLine "" + putLine "== Laws ==" + QuickSpec.Explore.quickSpec present measure (flip evalHaskell) cfg_max_size univ + [ Partial fun 0 | fun <- constantsOf g ] + putLine "" + + main = mapM_ round [1..rounds] + where + round n = mainOf (concat . take 1 . drop (rounds-n)) (concat . drop (rounds-n)) + rounds = max (length cfg_constants) (length cfg_predicates) + + join $ + fmap withStdioTerminal $ + generate $ + QuickCheck.run cfg_quickCheck (arbitraryVal cfg_default_to instances) evalHaskell $ + Twee.run cfg_twee { Twee.cfg_max_term_size = Twee.cfg_max_term_size cfg_twee `max` cfg_max_size } $ + runConditionals (map total constants) $ + flip evalStateT 1 $ + main + +printConstants :: MonadTerminal m => [Constant] -> m () +printConstants cs = do + putLine "== Functions ==" + let + decls = [ (show (pPrint (App (Partial c 0) [])), pPrintType (typ c)) | c <- cs ] + maxWidth = maximum (0:map (length . fst) decls) + pad xs = replicate (maxWidth - length xs) ' ' ++ xs + pPrintDecl (name, ty) = + hang (text (pad name) <+> text "::") 2 ty + + mapM_ (putLine . show . pPrintDecl) decls diff --git a/src/QuickSpec/Haskell/Resolve.hs b/src/QuickSpec/Haskell/Resolve.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Haskell/Resolve.hs @@ -0,0 +1,111 @@ +-- A data structure for resolving typeclass instances and similar at runtime. +-- +-- Takes as input a set of functions ("instances"), and a type, and +-- tries to build a value of that type from the instances given. +-- +-- For example, given the instances +-- ordList :: Dict (Arbitrary a) -> Dict (Arbitrary [a]) +-- ordChar :: Dict (Arbitrary Char) +-- and the target type Dict (Arbitrary [Char]), it will produce the value +-- ordList ordChar :: Dict (Arbitrary [Char]). +-- +-- The instances can in fact be arbitrary Haskell functions - though +-- their types must be such that the instance search will terminate. + +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE RankNTypes, ScopedTypeVariables #-} +module QuickSpec.Haskell.Resolve(Instances, inst, findInstance, findValue) where + +import Twee.Base +import QuickSpec.Type +import Data.MemoUgly +import Data.Functor.Identity +import Data.Maybe +import Data.Proxy +import Control.Monad + +-- A set of instances. +data Instances = + Instances { + -- The available instances. + -- Each instance is a unary function; 'inst' sees to this. + is_instances :: [Poly (Value Identity)], + -- The resulting instance search function (memoised). + is_find :: Type -> [Value Identity] } + +-- A smart constructor for Instances. +makeInstances :: [Poly (Value Identity)] -> Instances +makeInstances is = inst + where + inst = Instances is (memo (find_ inst . canonicaliseType)) + +instance Monoid Instances where + mempty = makeInstances [] + x `mappend` y = makeInstances (is_instances x ++ is_instances y) + +-- Create a single instance. +inst :: Typeable a => a -> Instances +inst x = instValue (toPolyValue x) + where + instValue :: Poly (Value Identity) -> Instances + instValue x = + -- Transform x into a single-argument function + -- (see comment about is_instances). + case typ x of + -- A function of type a -> (b -> c) gets uncurried. + App (F Arrow) (Cons _ (Cons (App (F Arrow) _) Empty)) -> + instValue (apply uncur x) + App (F Arrow) _ -> + makeInstances [x] + -- A plain old value x (not a function) turns into \() -> x. + _ -> + makeInstances [apply delay x] + where + uncur = toPolyValue (uncurry :: (A -> B -> C) -> (A, B) -> C) + delay = toPolyValue ((\x () -> x) :: A -> () -> A) + +-- Construct a value of a particular type. +-- If the type is polymorphic, may return an instance of it. +findValue :: Instances -> Type -> [Value Identity] +findValue = is_find + +-- Given a type a, construct a value of type f a. +-- If the type is polymorphic, may return an instance of it. +findInstance :: forall f. Typeable f => Instances -> Type -> [Value f] +findInstance insts ty = + map (unwrapFunctor runIdentity) (findValue insts ty') + where + ty' = typeRep (Proxy :: Proxy f) `applyType` ty + +-- The unmemoised version of the search algorithm. +-- Knows how to apply unary functions, and also knows how to generate: +-- * The unit type () +-- * Pairs (a, b) - search for a and then for b +-- These two are important because instValue encodes other instances +-- using them. +-- +-- Invariant: the type of the returned value is an instance of the argument type. +find_ :: Instances -> Type -> [Value Identity] +find_ _ (App (F unit) Empty) + | unit == tyCon (Proxy :: Proxy ()) = + return (toValue (Identity ())) +find_ res (App (F pair) (Cons ty1 (Cons ty2 Empty))) + | pair == tyCon (Proxy :: Proxy (,)) = do + x <- findValue res ty1 + sub <- maybeToList (match ty1 (typ x)) + -- N.B.: subst sub ty2 because searching for x may have constrained y's type + y <- findValue res (subst sub ty2) + sub <- maybeToList (match ty2 (typ y)) + return (pairValues (liftM2 (,)) (typeSubst sub x) y) +find_ insts ty = do + -- Find a function whose result type unifies with ty. + -- Rename it to avoid clashes with ty. + fun <- fmap (polyRename ty) (is_instances insts) + App (F Arrow) (Cons arg (Cons res Empty)) <- return (typ fun) + sub <- maybeToList (unify ty res) + fun <- return (typeSubst sub fun) + arg <- return (typeSubst sub arg) + -- Find an argument for that function and apply the function. + val <- findValue insts arg + sub <- maybeToList (match arg (typ val)) + return (apply (typeSubst sub fun) val) diff --git a/src/QuickSpec/Prop.hs b/src/QuickSpec/Prop.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Prop.hs @@ -0,0 +1,135 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators #-} +module QuickSpec.Prop where + +import Control.Monad +import qualified Data.DList as DList +import Data.Ord +import QuickSpec.Type +import QuickSpec.Utils +import QuickSpec.Term +import GHC.Generics(Generic) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set +import Control.Monad.Trans.State.Strict +import Data.List + +data Prop a = + (:=>:) { + lhs :: [Equation a], + rhs :: Equation a } + deriving (Show, Generic, Functor) + +instance Symbolic f a => Symbolic f (Prop a) where + termsDL (lhs :=>: rhs) = + termsDL rhs `mplus` termsDL lhs + subst sub (lhs :=>: rhs) = + subst sub lhs :=>: subst sub rhs + +instance Ord a => Eq (Prop a) where + x == y = x `compare` y == EQ +instance Ord a => Ord (Prop a) where + compare = comparing (\p -> (usort (lhs p), rhs p)) + +infix 4 :=>: + +literals :: Prop a -> [Equation a] +literals p = rhs p:lhs p + +unitProp :: Equation a -> Prop a +unitProp p = [] :=>: p + +mapFun :: (fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2) +mapFun f = fmap (fmap f) + +instance Typed a => Typed (Prop a) where + typ _ = typeOf True + otherTypesDL p = DList.fromList (literals p) >>= typesDL + typeSubst_ sub (lhs :=>: rhs) = + map (typeSubst_ sub) lhs :=>: typeSubst_ sub rhs + +instance Pretty a => Pretty (Prop a) where + pPrint ([] :=>: rhs) = pPrint rhs + pPrint p = + hsep (punctuate (text " &") (map pPrint (lhs p))) <+> text "=>" <+> pPrint (rhs p) + +data Equation a = a :=: a deriving (Show, Eq, Ord, Generic, Functor) + +instance Symbolic f a => Symbolic f (Equation a) where + termsDL (t :=: u) = termsDL t `mplus` termsDL u + subst sub (t :=: u) = subst sub t :=: subst sub u + +infix 5 :=: + +instance Typed a => Typed (Equation a) where + typ (t :=: _) = typ t + otherTypesDL (t :=: u) = otherTypesDL t `mplus` typesDL u + typeSubst_ sub (x :=: y) = typeSubst_ sub x :=: typeSubst_ sub y + +instance Pretty a => Pretty (Equation a) where + pPrintPrec _ _ (x :=: y) + | isTrue x = pPrint y + | isTrue y = pPrint x + | otherwise = pPrint x <+> text "=" <+> pPrint y + where + isTrue x = show (pPrint x) `elem` ["true", "True"] + +infix 4 === +(===) :: a -> a -> Prop a +x === y = [] :=>: x :=: y + +---------------------------------------------------------------------- +-- Making properties look pretty (naming variables, etc.) +---------------------------------------------------------------------- + +class PrettyArity fun where + prettyArity :: fun -> Int + prettyArity _ = 0 + +instance (PrettyArity fun1, PrettyArity fun2) => PrettyArity (fun1 :+: fun2) where + prettyArity (Inl x) = prettyArity x + prettyArity (Inr x) = prettyArity x + +prettyProp :: + (Typed fun, Apply (Term fun), PrettyTerm fun, PrettyArity fun) => + (Type -> [String]) -> Prop (Term fun) -> Doc +prettyProp cands = + pPrint . nameVars cands . eta + where + eta prop = + case filter isPretty (etaExpand prop) of + [] -> last (etaExpand prop) + (prop:_) -> prop + + isPretty (_ :=>: t :=: u) = isPretty1 t && isPretty1 u + isPretty1 (App f ts) = prettyArity f <= length ts + isPretty1 (Var _) = True + + etaExpand prop@(lhs :=>: t :=: u) = + prop: + case (tryApply t x, tryApply u x) of + (Just t', Just u') -> etaExpand (lhs :=>: t' :=: u') + _ -> [] + where + x = Var (V (head (typeArgs (typ t))) n) + n = maximum (0:map (succ . var_id) (vars prop)) + +data Named fun = Name String | Fun fun +instance Pretty fun => Pretty (Named fun) where + pPrintPrec _ _ (Name name) = text name + pPrintPrec l p (Fun fun) = pPrintPrec l p fun +instance PrettyTerm fun => PrettyTerm (Named fun) where + termStyle Name{} = uncurried + termStyle (Fun fun) = termStyle fun + +nameVars :: (Type -> [String]) -> Prop (Term fun) -> Prop (Term (Named fun)) +nameVars cands p = + subst (\x -> Map.findWithDefault undefined x sub) (fmap (fmap Fun) p) + where + sub = Map.fromList (evalState (mapM assign (nub (vars p))) Set.empty) + assign x = do + s <- get + let names = supply (cands (typ x)) + name = head (filter (`Set.notMember` s) names) + modify (Set.insert name) + return (x, App (Name name) []) diff --git a/src/QuickSpec/Pruning.hs b/src/QuickSpec/Pruning.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Pruning.hs @@ -0,0 +1,56 @@ +-- A type of pruners. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, GeneralizedNewtypeDeriving, FlexibleInstances, UndecidableInstances, DefaultSignatures, GADTs #-} +module QuickSpec.Pruning where + +import QuickSpec.Prop +import QuickSpec.Testing +import Control.Monad +import Control.Monad.Trans.Class +import Control.Monad.IO.Class +import Control.Monad.Trans.State.Strict +import Control.Monad.Trans.Reader + +class Monad m => MonadPruner term norm m | m -> term norm where + normaliser :: m (term -> norm) + add :: Prop term -> m Bool + + default normaliser :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => m (term -> norm) + normaliser = lift normaliser + + default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m Bool + add = lift . add + +instance MonadPruner term norm m => MonadPruner term norm (StateT s m) +instance MonadPruner term norm m => MonadPruner term norm (ReaderT r m) + +normalise :: MonadPruner term norm m => term -> m norm +normalise t = do + norm <- normaliser + return (norm t) + +newtype ReadOnlyPruner m a = ReadOnlyPruner { withReadOnlyPruner :: m a } + deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term) + +instance MonadTrans ReadOnlyPruner where + lift = ReadOnlyPruner + +instance MonadPruner term norm m => MonadPruner term norm (ReadOnlyPruner m) where + normaliser = ReadOnlyPruner normaliser + add _ = return True + +newtype WatchPruner term m a = WatchPruner (StateT [Prop term] m a) + deriving (Functor, Applicative, Monad, MonadTrans, MonadIO, MonadTester testcase term) + +instance MonadPruner term norm m => MonadPruner term norm (WatchPruner term m) where + normaliser = lift normaliser + add prop = do + res <- lift (add prop) + when res (WatchPruner (modify (prop:))) + return res + +watchPruner :: Monad m => WatchPruner term m a -> m (a, [Prop term]) +watchPruner (WatchPruner mx) = do + (x, props) <- runStateT mx [] + return (x, reverse props) + diff --git a/src/QuickSpec/Pruning/Background.hs b/src/QuickSpec/Pruning/Background.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Pruning/Background.hs @@ -0,0 +1,46 @@ +-- A pruning layer which automatically adds axioms about functions as they appear. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, TypeOperators #-} +module QuickSpec.Pruning.Background where + +import QuickSpec.Term +import QuickSpec.Testing +import QuickSpec.Pruning +import QuickSpec.Prop +import QuickSpec.Terminal +import qualified Data.Set as Set +import Data.Set(Set) +import Control.Monad +import Control.Monad.IO.Class +import Control.Monad.Trans.Class +import Control.Monad.Trans.State.Strict hiding (State) + +newtype Pruner fun m a = + Pruner (StateT (Set fun) m a) + deriving (Functor, Applicative, Monad, MonadIO, MonadTrans, MonadTester testcase term, MonadTerminal) + +class Background f where + background :: f -> [Prop (Term f)] + background _ = [] + +run :: Monad m => Pruner fun m a -> m a +run (Pruner x) = + evalStateT x Set.empty + +instance (Ord fun, Background fun, MonadPruner (Term fun) norm m) => + MonadPruner (Term fun) norm (Pruner fun m) where + normaliser = lift normaliser + add prop = do + mapM_ addFunction (funs prop) + lift (add prop) + +addFunction :: (Ord fun, Background fun, MonadPruner (Term fun) norm m) => fun -> Pruner fun m () +addFunction f = do + funcs <- Pruner get + unless (f `Set.member` funcs) $ do + Pruner (put (Set.insert f funcs)) + mapM_ add (background f) + +instance (Background fun1, Background fun2) => Background (fun1 :+: fun2) where + background (Inl x) = map (fmap (fmap Inl)) (background x) + background (Inr x) = map (fmap (fmap Inr)) (background x) diff --git a/src/QuickSpec/Pruning/Twee.hs b/src/QuickSpec/Pruning/Twee.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Pruning/Twee.hs @@ -0,0 +1,26 @@ +-- A pruner that uses twee. Supports types and background axioms. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-} +module QuickSpec.Pruning.Twee(Config(..), module QuickSpec.Pruning.Twee) where + +import QuickSpec.Testing +import QuickSpec.Pruning +import QuickSpec.Term +import QuickSpec.Terminal +import qualified QuickSpec.Pruning.Types as Types +import qualified QuickSpec.Pruning.Background as Background +import Control.Monad.Trans.Class +import Control.Monad.IO.Class +import qualified QuickSpec.Pruning.UntypedTwee as Untyped +import QuickSpec.Pruning.UntypedTwee(Config(..)) + +newtype Pruner fun m a = + Pruner (Background.Pruner fun (Types.Pruner fun (Untyped.Pruner (Types.Tagged fun) m)) a) + deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadPruner (Term fun) (Term fun), MonadTerminal) + +instance MonadTrans (Pruner fun) where + lift = Pruner . lift . lift . lift + +run :: Monad m => Config -> Pruner fun m a -> m a +run config (Pruner x) = + Untyped.run config (Types.run (Background.run x)) diff --git a/src/QuickSpec/Pruning/Types.hs b/src/QuickSpec/Pruning/Types.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Pruning/Types.hs @@ -0,0 +1,123 @@ +-- Encode monomorphic types during pruning. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE RecordWildCards, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-} +module QuickSpec.Pruning.Types where + +import QuickSpec.Pruning +import qualified QuickSpec.Pruning.Background as Background +import QuickSpec.Pruning.Background(Background) +import QuickSpec.Testing +import QuickSpec.Term +import QuickSpec.Type +import QuickSpec.Prop +import QuickSpec.Terminal +import Control.Monad.IO.Class +import Control.Monad.Trans.Class + +data Tagged fun = + Func fun + | Tag Type + deriving (Eq, Ord, Show, Typeable) + +instance Arity fun => Arity (Tagged fun) where + arity (Func f) = arity f + arity (Tag _) = 1 + +instance Sized fun => Sized (Tagged fun) where + size (Func f) = size f + size (Tag _) = 0 + +instance Pretty fun => Pretty (Tagged fun) where + pPrint (Func f) = pPrint f + pPrint (Tag ty) = text "tag[" <> pPrint ty <> text "]" + +instance PrettyTerm fun => PrettyTerm (Tagged fun) where + termStyle (Func f) = termStyle f + termStyle (Tag _) = uncurried + +instance EqualsBonus (Tagged fun) where + +type TypedTerm fun = Term fun +type UntypedTerm fun = Term (Tagged fun) + +newtype Pruner fun pruner a = + Pruner { run :: pruner a } + deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal) + +instance MonadTrans (Pruner fun) where + lift = Pruner + +instance (PrettyTerm fun, Typed fun, MonadPruner (UntypedTerm fun) (UntypedTerm fun) pruner) => MonadPruner (TypedTerm fun) (TypedTerm fun) (Pruner fun pruner) where + normaliser = + Pruner $ do + norm <- normaliser :: pruner (UntypedTerm fun -> UntypedTerm fun) + + -- Note that we don't call addFunction on the functions in the term. + -- This is because doing so might be expensive, as adding typing + -- axioms starts the completion algorithm. + -- This is OK because in encode, we tag all functions and variables + -- with their types (i.e. we can fall back to the naive type encoding). + return $ \t -> + decode . norm . encode $ t + + add prop = lift (add (encode <$> canonicalise prop)) + +instance (Typed fun, Arity fun) => Background (Tagged fun) where + background = typingAxioms + +-- Compute the typing axioms for a function or type tag. +typingAxioms :: (Typed fun, Arity fun) => + Tagged fun -> [Prop (UntypedTerm fun)] +typingAxioms (Tag ty) = + [tag ty (tag ty x) === tag ty x] + where + x = Var (V ty 0) +typingAxioms (Func func) = + [tag res t === t] ++ + [tagArg i ty === t | (i, ty) <- zip [0..] args] + where + f = Func func + xs = take n (map (Var . V typeVar) [0..]) + + ty = typ func + -- Use arity rather than typeArity, so that we can support + -- partially-applied functions + n = arity func + args = take n (typeArgs ty) + res = typeDrop n ty + + t = App f xs + + tagArg i ty = + App f $ + take i xs ++ + [tag ty (xs !! i)] ++ + drop (i+1) xs + +tag :: Type -> UntypedTerm fun -> UntypedTerm fun +tag ty t = App (Tag ty) [t] + +encode :: Typed fun => TypedTerm fun -> UntypedTerm fun +-- We always add type tags; see comment in normaliseMono. +-- In the common case, twee will immediately remove these surplus type tags +-- by rewriting using the typing axioms. +encode (Var x) = tag (typ x) (Var x) +encode (App f ts) = + tag (typeDrop (length ts) (typ f)) (App (Func f) (map encode ts)) + +decode :: Typed fun => UntypedTerm fun -> TypedTerm fun +decode = dec Nothing + where + dec _ (App (Tag ty) [t]) = + dec (Just ty) t + dec _ (App Tag{} _) = + error "Tag function applied with wrong arity" + dec (Just ty) (Var (V _ x)) = + Var (V ty x) + dec Nothing (Var _) = + error "Naked variable in type-encoded term" + dec _ (App (Func f) ts) = + App f $ + zipWith dec + (map Just (typeArgs (typ f))) + ts diff --git a/src/QuickSpec/Pruning/UntypedTwee.hs b/src/QuickSpec/Pruning/UntypedTwee.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Pruning/UntypedTwee.hs @@ -0,0 +1,127 @@ +-- A pruner that uses twee. Does not respect types. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances, TemplateHaskell #-} +module QuickSpec.Pruning.UntypedTwee where + +import QuickSpec.Testing +import QuickSpec.Pruning +import QuickSpec.Prop +import QuickSpec.Term +import QuickSpec.Type +import QuickSpec.Utils +import qualified Twee +import qualified Twee.Equation as Twee +import qualified Twee.KBO as KBO +import qualified Twee.Base as Twee +import Twee hiding (Config(..)) +import Twee.Rule hiding (normalForms) +import Twee.Proof hiding (Config, defaultConfig) +import Twee.Base(Ordered(..), Extended(..), EqualsBonus, pattern F, pattern Empty, unpack) +import Control.Monad.Trans.Reader +import Control.Monad.Trans.State.Strict hiding (State) +import Control.Monad.Trans.Class +import Control.Monad.IO.Class +import QuickSpec.Terminal +import qualified Data.Set as Set +import Data.Set(Set) + +data Config = + Config { + cfg_max_term_size :: Int, + cfg_max_cp_depth :: Int } + +makeLensAs ''Config + [("cfg_max_term_size", "lens_max_term_size"), + ("cfg_max_cp_depth", "lens_max_cp_depth")] + +instance (Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Sized fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where + lessEq = KBO.lessEq + lessIn = KBO.lessIn + +newtype Pruner fun m a = + Pruner (ReaderT Twee.Config (StateT (State (Extended fun)) m) a) + deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal) + +instance MonadTrans (Pruner fun) where + lift = Pruner . lift . lift + +run :: Monad m => Config -> Pruner fun m a -> m a +run Config{..} (Pruner x) = + evalStateT (runReaderT x config) initialState + where + config = + defaultConfig { + Twee.cfg_max_term_size = cfg_max_term_size, + Twee.cfg_max_cp_depth = cfg_max_cp_depth } + +instance (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun, Monad m) => + MonadPruner (Term fun) (Term fun) (Pruner fun m) where + normaliser = Pruner $ do + state <- lift get + return $ \t -> + let u = normaliseTwee state t in + u + -- traceShow (text "normalise:" <+> pPrint t <+> text "->" <+> pPrint u) u + + add ([] :=>: t :=: u) = Pruner $ do + state <- lift get + config <- ask + let + t' = normalFormsTwee state t + u' = normalFormsTwee state u + -- Add the property anyway in case it could only be joined + -- by considering all normal forms + lift (put $! addTwee config t u state) + return (Set.null (Set.intersection t' u')) + + add _ = + error "twee pruner doesn't support non-unit equalities" + +normaliseTwee :: (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun) => + State (Extended fun) -> Term fun -> Term fun +normaliseTwee state t = + fromTwee $ + result (normaliseTerm state (simplifyTerm state (skolemise t))) + +normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun) => + State (Extended fun) -> Term fun -> Set (Term fun) +normalFormsTwee state t = + Set.map fromTwee $ + Set.map result (normalForms state (skolemise t)) + +addTwee :: (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun) => + Twee.Config -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun) +addTwee config t u state = + completePure config $ + addAxiom config state axiom + where + axiom = Axiom 0 (prettyShow (t :=: u)) (toTwee t Twee.:=: toTwee u) + +toTwee :: (Ord f, Typeable f) => + Term f -> Twee.Term (Extended f) +toTwee = Twee.build . tt + where + tt (Var (V _ x)) = + Twee.var (Twee.V x) + tt (App f ts) = + Twee.app (Twee.fun (Function f)) (map tt ts) + +skolemise :: (Ord f, Typeable f) => + Term f -> Twee.Term (Extended f) +skolemise = Twee.build . sk + where + sk (Var (V _ x)) = + Twee.con (Twee.fun (Skolem (Twee.V x))) + sk (App f ts) = + Twee.app (Twee.fun (Function f)) (map sk ts) + +fromTwee :: Twee.Term (Extended f) -> Term f +fromTwee = unsk + where + unsk (Twee.App (F Minimal) Empty) = + Var (V typeVar 0) + unsk (Twee.App (F (Skolem (Twee.V x))) Empty) = + Var (V typeVar x) + unsk (Twee.App (F (Function f)) ts) = + App f (map unsk (unpack ts)) + unsk _ = error "variable introduced by rewriting" diff --git a/src/QuickSpec/Term.hs b/src/QuickSpec/Term.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Term.hs @@ -0,0 +1,186 @@ +-- Typed terms. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE PatternSynonyms, ViewPatterns, TypeSynonymInstances, FlexibleInstances, TypeFamilies, ConstraintKinds, DeriveGeneric, DeriveAnyClass, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, TypeOperators, DeriveFunctor, FlexibleContexts #-} +module QuickSpec.Term(module QuickSpec.Term, module Twee.Base, module Twee.Pretty) where + +import QuickSpec.Type +import QuickSpec.Utils +import Control.Monad +import GHC.Generics(Generic) +import Test.QuickCheck(CoArbitrary) +import Data.DList(DList) +import qualified Data.DList as DList +import Twee.Base(Sized(..), Arity(..), Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint) +import Twee.Pretty +import qualified Data.Map.Strict as Map +import Data.List +import Data.Reflection + +data Term f = Var {-# UNPACK #-} !Var | App !f ![Term f] + deriving (Eq, Ord, Show, Functor) + +data Var = V { var_ty :: !Type, var_id :: {-# UNPACK #-} !Int } + deriving (Eq, Ord, Show, Generic, CoArbitrary) + +instance Typed Var where + typ x = var_ty x + otherTypesDL _ = mzero + typeSubst_ sub (V ty x) = V (typeSubst_ sub ty) x + +class Symbolic f a | a -> f where + termsDL :: a -> DList (Term f) + subst :: (Var -> Term f) -> a -> a + +instance Symbolic f (Term f) where + termsDL = return + subst sub (Var x) = sub x + subst sub (App f ts) = App f (map (subst sub) ts) + +instance Symbolic f a => Symbolic f [a] where + termsDL = msum . map termsDL + subst sub = map (subst sub) + +instance Sized f => Sized (Term f) where + size (Var _) = 1 + size (App f ts) = size f + sum (map size ts) + +instance Pretty Var where + --pPrint x = parens $ text "X" <> pPrint (var_id x+1) <+> text "::" <+> pPrint (var_ty x) + pPrint x = text "X" <> pPrint (var_id x+1) + +instance PrettyTerm f => Pretty (Term f) where + pPrintPrec l p (Var x) = pPrintPrec l p x + pPrintPrec l p (App f xs) = + pPrintTerm (termStyle f) l p (pPrint f) xs + +isApp :: Term f -> Bool +isApp App{} = True +isApp Var{} = False + +isVar :: Term f -> Bool +isVar = not . isApp + +terms :: Symbolic f a => a -> [Term f] +terms = DList.toList . termsDL + +funs :: Symbolic f a => a -> [f] +funs x = [ f | t <- terms x, App f _ <- subterms t ] + +vars :: Symbolic f a => a -> [Var] +vars x = [ v | t <- terms x, Var v <- subterms t ] + +freeVar :: Symbolic f a => a -> Int +freeVar x = maximum (0:map (succ . var_id) (vars x)) + +occ :: (Eq f, Symbolic f a) => f -> a -> Int +occ x t = length (filter (== x) (funs t)) + +occVar :: Symbolic f a => Var -> a -> Int +occVar x t = length (filter (== x) (vars t)) + +mapVar :: (Var -> Var) -> Term f -> Term f +mapVar f (Var x) = Var (f x) +mapVar f (App g xs) = App g (map (mapVar f) xs) + +subterms, properSubterms :: Term f -> [Term f] +subterms t = t:properSubterms t +properSubterms (App _ ts) = concatMap subterms ts +properSubterms _ = [] + +-- Introduces variables in a canonical order. +-- Also makes sure that variables of different types have different numbers +canonicalise :: Symbolic fun a => a -> a +canonicalise t = subst (\x -> Map.findWithDefault undefined x sub) t + where + sub = + Map.fromList + [(x, Var (V ty n)) + | (x@(V ty _), n) <- zip (nub (vars t)) [0..]] + +class Eval term val where + eval :: (Var -> val) -> term -> val + +instance (Typed fun, Given Type, Apply a, Eval fun a) => Eval (Term fun) a where + eval env = evaluateTerm (eval env) env + +evaluateTerm :: (Typed fun, Given Type, Apply a) => (fun -> a) -> (Var -> a) -> Term fun -> a +evaluateTerm fun var = eval + where + eval (Var x) = var x + eval (App f ts) = + foldl apply (fun (defaultTo given f)) (map eval ts) + +instance Typed f => Typed (Term f) where + typ (Var x) = typ x + typ (App f ts) = + typeDrop (length ts) (typ f) + + otherTypesDL (Var _) = mempty + otherTypesDL (App f ts) = + typesDL f `mplus` typesDL ts + + typeSubst_ sub = tsub + where + tsub (Var x) = Var (typeSubst_ sub x) + tsub (App f ts) = + App (typeSubst_ sub f) (map tsub ts) + +-- A standard term ordering - size, skeleton, generality. +-- Satisfies the property: +-- if measure (schema t) < measure (schema u) then t < u. +type Measure f = (Int, Int, MeasureFuns f, Int, [Var]) +measure :: Sized f => Term f -> Measure f +measure t = + (size t, -length (vars t), MeasureFuns (skel t), + -length (usort (vars t)), vars t) + where + skel (Var (V ty _)) = Var (V ty 0) + skel (App f ts) = App f (map skel ts) + +newtype MeasureFuns f = MeasureFuns (Term f) +instance Ord f => Eq (MeasureFuns f) where + t == u = compare t u == EQ +instance Ord f => Ord (MeasureFuns f) where + compare (MeasureFuns t) (MeasureFuns u) = compareFuns t u + +compareFuns :: Ord f => Term f -> Term f -> Ordering +compareFuns (Var x) (Var y) = compare x y +compareFuns Var{} App{} = LT +compareFuns App{} Var{} = GT +compareFuns (App f ts) (App g us) = + compare f g `orElse` + compare (map MeasureFuns ts) (map MeasureFuns us) + +---------------------------------------------------------------------- +-- Data types a la carte-ish. +---------------------------------------------------------------------- + +data a :+: b = Inl a | Inr b deriving (Eq, Ord) + +instance (Eval fun1 a, Eval fun2 a) => Eval (fun1 :+: fun2) a where + eval env (Inl x) = eval env x + eval env (Inr x) = eval env x + +instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where + size (Inl x) = size x + size (Inr x) = size x + +instance (Arity fun1, Arity fun2) => Arity (fun1 :+: fun2) where + arity (Inl x) = arity x + arity (Inr x) = arity x + +instance (Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) where + typ (Inl x) = typ x + typ (Inr x) = typ x + otherTypesDL (Inl x) = otherTypesDL x + otherTypesDL (Inr x) = otherTypesDL x + typeSubst_ sub (Inl x) = Inl (typeSubst_ sub x) + typeSubst_ sub (Inr x) = Inr (typeSubst_ sub x) + +instance (Pretty fun1, Pretty fun2) => Pretty (fun1 :+: fun2) where + pPrintPrec l p (Inl x) = pPrintPrec l p x + pPrintPrec l p (Inr x) = pPrintPrec l p x + +instance (PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm (fun1 :+: fun2) where + termStyle (Inl x) = termStyle x + termStyle (Inr x) = termStyle x diff --git a/src/QuickSpec/Terminal.hs b/src/QuickSpec/Terminal.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Terminal.hs @@ -0,0 +1,51 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE GeneralizedNewtypeDeriving, DefaultSignatures, GADTs #-} +module QuickSpec.Terminal where + +import Control.Monad.Trans.Class +import Control.Monad.IO.Class +import Control.Monad.Trans.State.Strict +import Control.Monad.Trans.Reader +import qualified Test.QuickCheck.Text as Text + +class Monad m => MonadTerminal m where + putLine :: String -> m () + putTemp :: String -> m () + + default putLine :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m () + putLine = lift . putLine + + default putTemp :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m () + putTemp = lift . putTemp + +instance MonadTerminal m => MonadTerminal (StateT s m) +instance MonadTerminal m => MonadTerminal (ReaderT r m) + +putStatus :: MonadTerminal m => String -> m () +putStatus str = putTemp ("[" ++ str ++ "...]") + +clearStatus :: MonadTerminal m => m () +clearStatus = putTemp "" + +withStatus :: MonadTerminal m => String -> m a -> m a +withStatus str mx = putStatus str *> mx <* clearStatus + +newtype Terminal a = Terminal (ReaderT Text.Terminal IO a) + deriving (Functor, Applicative, Monad, MonadIO) + +instance MonadTerminal Terminal where + putLine str = Terminal $ do + term <- ask + liftIO $ Text.putLine term str + + putTemp str = Terminal $ do + term <- ask + liftIO $ Text.putTemp term str + +withNullTerminal :: Terminal a -> IO a +withNullTerminal (Terminal mx) = + Text.withNullTerminal (runReaderT mx) + +withStdioTerminal :: Terminal a -> IO a +withStdioTerminal (Terminal mx) = + Text.withStdioTerminal (runReaderT mx) diff --git a/src/QuickSpec/Testing.hs b/src/QuickSpec/Testing.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Testing.hs @@ -0,0 +1,18 @@ +-- A type of test case generators. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DefaultSignatures, GADTs, FlexibleInstances, UndecidableInstances #-} +module QuickSpec.Testing where + +import QuickSpec.Prop +import Control.Monad.Trans.Class +import Control.Monad.Trans.State.Strict +import Control.Monad.Trans.Reader + +class Monad m => MonadTester testcase term m | m -> testcase term where + test :: Prop term -> m (Maybe testcase) + + default test :: (MonadTrans t, MonadTester testcase term m', m ~ t m') => Prop term -> m (Maybe testcase) + test = lift . test + +instance MonadTester testcase term m => MonadTester testcase term (StateT s m) +instance MonadTester testcase term m => MonadTester testcase term (ReaderT r m) diff --git a/src/QuickSpec/Testing/DecisionTree.hs b/src/QuickSpec/Testing/DecisionTree.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Testing/DecisionTree.hs @@ -0,0 +1,95 @@ +-- Decision trees for testing terms for equality. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE RecordWildCards #-} +module QuickSpec.Testing.DecisionTree where + +import qualified Data.Map as Map +import Data.Map(Map) + +data DecisionTree testcase result term = + DecisionTree { + -- A function for evaluating terms on test cases. + dt_evaluate :: term -> testcase -> result, + -- The set of test cases gathered so far. + dt_test_cases :: [testcase], + -- The tree itself. + dt_tree :: !(Maybe (InnerTree result term)) } + +data InnerTree result term = + TestCase !(Map result (InnerTree result term)) + | Singleton !term + +data Result testcase result term = + Distinct (DecisionTree testcase result term) + | EqualTo term + +-- Make a new decision tree. +empty :: (term -> testcase -> result) -> DecisionTree testcase result term +empty eval = + DecisionTree { + dt_evaluate = eval, + dt_test_cases = [], + dt_tree = Nothing } + +-- Add a new test case to a decision tree. +addTestCase :: + testcase -> DecisionTree testcase result term -> + DecisionTree testcase result term +addTestCase tc dt@DecisionTree{..} = + dt{dt_test_cases = dt_test_cases ++ [tc]} + +-- Insert a value into a decision tree. +insert :: Ord result => + term -> DecisionTree testcase result term -> + Result testcase result term +insert x dt@DecisionTree{dt_tree = Nothing, ..} = + Distinct dt{dt_tree = Just (Singleton x)} +insert x dt@DecisionTree{dt_tree = Just dt_tree, ..} = + aux k dt_test_cases dt_tree + where + k tree = dt{dt_tree = Just tree} + aux _ [] (Singleton y) = EqualTo y + aux k (t:ts) (Singleton y) = + aux k (t:ts) $ + TestCase (Map.singleton (dt_evaluate y t) (Singleton y)) + aux k (t:ts) (TestCase res) = + let + val = dt_evaluate x t + k' tree = k (TestCase (Map.insert val tree res)) + in case Map.lookup val res of + Nothing -> + Distinct (k' (Singleton x)) + Just tree -> + aux k' ts tree + aux _ [] (TestCase _) = + error "unexpected node in decision tree" + +data Statistics = + Statistics { + -- Total number of terms in the decision tree + stat_num_terms :: !Int, + -- Total number of tests executed + stat_num_tests :: !Int, + -- Number of distinct test cases used + stat_num_test_cases :: !Int } + deriving (Eq, Show) + +statistics :: DecisionTree testcase result term -> Statistics +statistics DecisionTree{dt_tree = Nothing} = + Statistics 0 0 0 +statistics DecisionTree{dt_tree = Just dt_tree, ..} = + Statistics { + stat_num_terms = x, + stat_num_tests = y, + stat_num_test_cases = length dt_test_cases } + where + (x, y) = stat dt_tree + + -- Returns (number of terms, number of tests) + stat Singleton{} = (1, 0) + -- To calculate the number of test cases, note that each term + -- under res executed one test case on the way through this node. + stat (TestCase res) = + (sum (map fst ss), sum [ x + y | (x, y) <- ss ]) + where + ss = map stat (Map.elems res) diff --git a/src/QuickSpec/Testing/QuickCheck.hs b/src/QuickSpec/Testing/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Testing/QuickCheck.hs @@ -0,0 +1,88 @@ +-- Testing conjectures using QuickCheck. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE FlexibleContexts, FlexibleInstances, RecordWildCards, MultiParamTypeClasses, GeneralizedNewtypeDeriving, TemplateHaskell #-} +module QuickSpec.Testing.QuickCheck where + +import QuickSpec.Testing +import QuickSpec.Prop +import Test.QuickCheck +import Test.QuickCheck.Gen +import Test.QuickCheck.Random +import Control.Monad +import Control.Monad.IO.Class +import Control.Monad.Trans.Class +import Control.Monad.Trans.Reader +import Data.List +import System.Random +import QuickSpec.Terminal +import QuickSpec.Utils + +data Config = + Config { + cfg_num_tests :: Int, + cfg_max_test_size :: Int, + cfg_fixed_seed :: Maybe QCGen} + deriving Show + +makeLensAs ''Config + [("cfg_num_tests", "lens_num_tests"), + ("cfg_max_test_size", "lens_max_test_size"), + ("cfg_fixed_seed", "lens_fixed_seed")] + +data Environment testcase term result = + Environment { + env_config :: Config, + env_tests :: [testcase], + env_eval :: testcase -> term -> result } + +newtype Tester testcase term result m a = + Tester (ReaderT (Environment testcase term result) m a) + deriving (Functor, Applicative, Monad, MonadIO, MonadTerminal) + +instance MonadTrans (Tester testcase term result) where + lift = Tester . lift + +run :: + Config -> Gen testcase -> (testcase -> term -> result) -> + Tester testcase term result m a -> Gen (m a) +run config@Config{..} gen eval (Tester x) = do + seed <- maybe arbitrary return cfg_fixed_seed + let + seeds = unfoldr (Just . split) seed + n = cfg_num_tests + k = cfg_max_test_size + -- Divide tests equally between all sizes. + -- There are n total tests of k+1 different sizes. + -- If it doesn't divide equally, the biggest size gets the + -- left-overs. + sizes = + concat [replicate (n `div` (k+1)) i | i <- [0..k-1]] ++ + replicate (n `divRoundUp` (k+1)) k + m `divRoundUp` n = (m-1) `div` n + 1 + tests = zipWith (unGen gen) seeds sizes + return $ runReaderT x + Environment { + env_config = config, + env_tests = tests, + env_eval = eval } + +instance (MonadTerminal m, Eq result) => MonadTester testcase term (Tester testcase term result m) where + test prop = + Tester $ do + env <- ask + return $! quickCheckTest env prop + +quickCheckTest :: Eq result => + Environment testcase term result -> + Prop term -> Maybe testcase +quickCheckTest Environment{env_config = Config{..}, ..} (lhs :=>: rhs) = + msum (map test env_tests) + where + test testcase = do + guard $ + all (testEq testcase) lhs && + not (testEq testcase rhs) + return testcase + + testEq testcase (t :=: u) = + env_eval testcase t == env_eval testcase u diff --git a/src/QuickSpec/Type.hs b/src/QuickSpec/Type.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Type.hs @@ -0,0 +1,442 @@ +-- Polymorphic types and dynamic values. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, EmptyDataDecls, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, Rank2Types, ExistentialQuantification, PolyKinds, TypeFamilies, FlexibleContexts, StandaloneDeriving, PatternGuards, MultiParamTypeClasses, ConstraintKinds, DataKinds #-} +-- To avoid a warning about TyVarNumber's constructor being unused: +{-# OPTIONS_GHC -fno-warn-unused-binds #-} +module QuickSpec.Type( + -- Types. + Typeable, + Type, TyCon(..), tyCon, fromTyCon, A, B, C, D, E, ClassA, ClassB, ClassC, ClassD, ClassE, SymA, typeVar, isTypeVar, + typeOf, typeRep, applyType, fromTypeRep, + arrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity, oneTypeVar, defaultTo, skolemiseTypeVars, + isDictionary, getDictionary, pPrintType, + -- Things that have types. + Typed(..), typeSubst, typesDL, tyVars, cast, + TypeView(..), + Apply(..), apply, canApply, + -- Polymorphic types. + canonicaliseType, + Poly, toPolyValue, poly, unPoly, polyTyp, polyMap, polyRename, polyApply, polyPair, polyList, polyMgu, + -- Dynamic values. + Value, toValue, fromValue, + Unwrapped(..), unwrap, Wrapper(..), + mapValue, forValue, ofValue, withValue, pairValues, wrapFunctor, unwrapFunctor) where + +import Control.Monad +import Data.DList(DList) +import Data.Maybe +import qualified Data.Typeable as Ty +import Data.Typeable(Typeable) +import GHC.Exts(Any) +import Test.QuickCheck +import Unsafe.Coerce +import Data.Constraint +import Twee.Base +import Data.Proxy +import Data.List +import Data.Char + +-- A (possibly polymorphic) type. +type Type = Term TyCon + +data TyCon = Arrow | String String | TyCon Ty.TyCon deriving (Eq, Ord, Show) + +instance Pretty TyCon where + pPrint Arrow = text "->" + pPrint (String x) = text x + pPrint (TyCon x) = text (show x) +instance PrettyTerm TyCon where + termStyle Arrow = + fixedArity 2 $ + TermStyle $ \l p d [x, y] -> + maybeParens (p > 8) $ + pPrintPrec l 9 x <+> d <+> + pPrintPrec l 0 y + + termStyle (String _) = curried + + termStyle (TyCon con) + | con == listTyCon = + fixedArity 1 $ + TermStyle $ \l _ _ [x] -> brackets (pPrintPrec l 0 x) + | show con == "()" || show con == "(%%)" = + fixedArity 0 tupleStyle -- by analogy with case below + | take 2 (show con) == "(," || + take 3 (show con) == "(%," = + fixedArity (1+length (filter (== ',') (show con))) tupleStyle + | isAlphaNum (head (show con)) = curried + | otherwise = infixStyle 5 + +-- Type and class variables. +newtype A = A Any deriving Typeable +newtype B = B Any deriving Typeable +newtype C = C Any deriving Typeable +newtype D = D Any deriving Typeable +newtype E = E Any deriving Typeable + +class ClassA +deriving instance Typeable ClassA +class ClassB +deriving instance Typeable ClassB +class ClassC +deriving instance Typeable ClassC +class ClassD +deriving instance Typeable ClassD +class ClassE +deriving instance Typeable ClassE + +type SymA = "__polymorphic_symbol__" + +typeVars :: [Ty.TypeRep] +typeVars = + [Ty.typeRep (Proxy :: Proxy A), + Ty.typeRep (Proxy :: Proxy B), + Ty.typeRep (Proxy :: Proxy C), + Ty.typeRep (Proxy :: Proxy D), + Ty.typeRep (Proxy :: Proxy E), + Ty.typeRep (Proxy :: Proxy ClassA), + Ty.typeRep (Proxy :: Proxy ClassB), + Ty.typeRep (Proxy :: Proxy ClassC), + Ty.typeRep (Proxy :: Proxy ClassD), + Ty.typeRep (Proxy :: Proxy ClassE), + Ty.typeRep (Proxy :: Proxy SymA)] + +typeVar :: Type +typeVar = typeRep (Proxy :: Proxy A) + +isTypeVar :: Type -> Bool +isTypeVar = isVar + +typeOf :: Typeable a => a -> Type +typeOf x = fromTypeRep (Ty.typeOf x) + +typeRep :: Typeable (a :: k) => proxy a -> Type +typeRep x = fromTypeRep (Ty.typeRep x) + +applyType :: Type -> Type -> Type +applyType (App f tys) ty = build (app f (unpack tys ++ [ty])) +applyType _ _ = error "tried to apply type variable" + +arrowType :: [Type] -> Type -> Type +arrowType [] res = res +arrowType (arg:args) res = + build (app (fun Arrow) [arg, arrowType args res]) + +unpackArrow :: Type -> Maybe (Type, Type) +unpackArrow (App (F Arrow) (Cons t (Cons u Empty))) = + Just (t, u) +unpackArrow _ = + Nothing + +typeArgs :: Type -> [Type] +typeArgs (App (F Arrow) (Cons arg (Cons res Empty))) = + arg:typeArgs res +typeArgs _ = [] + +typeRes :: Type -> Type +typeRes (App (F Arrow) (Cons _ (Cons res Empty))) = + typeRes res +typeRes ty = ty + +typeDrop :: Int -> Type -> Type +typeDrop 0 ty = ty +typeDrop n (App (F Arrow) (Cons _ (Cons ty Empty))) = + typeDrop (n-1) ty +typeDrop _ _ = + error "typeDrop on non-function type" + +typeArity :: Type -> Int +typeArity = length . typeArgs + +oneTypeVar :: Typed a => a -> a +oneTypeVar = typeSubst (const (var (V 0))) + +defaultTo :: Typed a => Type -> a -> a +defaultTo def = typeSubst (const def) + +skolemiseTypeVars :: Typed a => a -> a +skolemiseTypeVars = typeSubst (const aTy) + where + aTy = build (con (fun (tyCon (Proxy :: Proxy A)))) + +fromTypeRep :: Ty.TypeRep -> Type +fromTypeRep ty + | Just n <- elemIndex ty typeVars = + build (var (V n)) + | otherwise = + let (tyCon, tys) = Ty.splitTyConApp ty in + build (app (fun (fromTyCon tyCon)) (map fromTypeRep tys)) + +fromTyCon :: Ty.TyCon -> TyCon +fromTyCon ty + | ty == arrowTyCon = Arrow + | otherwise = TyCon ty + +arrowTyCon, commaTyCon, listTyCon, dictTyCon :: Ty.TyCon +arrowTyCon = mkCon (Proxy :: Proxy (->)) +commaTyCon = mkCon (Proxy :: Proxy (,)) +listTyCon = mkCon (Proxy :: Proxy []) +dictTyCon = mkCon (Proxy :: Proxy Dict) + +mkCon :: Typeable a => proxy a -> Ty.TyCon +mkCon = fst . Ty.splitTyConApp . Ty.typeRep + +tyCon :: Typeable a => proxy a -> TyCon +tyCon = fromTyCon . mkCon + +getDictionary :: Type -> Maybe Type +getDictionary (App (F (TyCon dict)) (Cons ty Empty)) + | dict == dictTyCon = Just ty +getDictionary _ = Nothing + +isDictionary :: Type -> Bool +isDictionary = isJust . getDictionary + +-- CoArbitrary instances. +instance CoArbitrary Type where + coarbitrary = coarbitrary . singleton +instance CoArbitrary (TermList TyCon) where + coarbitrary Empty = variant 0 + coarbitrary (ConsSym (Var (V x)) ts) = + variant 1 . coarbitrary x . coarbitrary ts + coarbitrary (ConsSym (App f _) ts) = + variant 2 . coarbitrary (fun_id f) . coarbitrary ts + +pPrintType :: Type -> Doc +pPrintType = pPrint . typeSubst (\(V x) -> build (con (fun (String (as !! x))))) . canonicalise + where + as = supply [[x] | x <- ['a'..'z']] + +-- Things with types. +class Typed a where + -- The type. + typ :: a -> Type + -- Any other types that may appear in subterms etc + -- (enough at least to collect all type variables and type constructors). + otherTypesDL :: a -> DList Type + otherTypesDL _ = mzero + -- Substitute for all type variables. + typeSubst_ :: (Var -> Builder TyCon) -> a -> a + +{-# INLINE typeSubst #-} +typeSubst :: (Typed a, Substitution s, SubstFun s ~ TyCon) => s -> a -> a +typeSubst s x = typeSubst_ (evalSubst s) x + +-- Using the normal term machinery on types. +newtype TypeView a = TypeView { unTypeView :: a } +instance Typed a => Symbolic (TypeView a) where + type ConstantOf (TypeView a) = TyCon + termsDL = fmap singleton . typesDL . unTypeView + subst_ sub = TypeView . typeSubst_ sub . unTypeView +instance Typed a => Has (TypeView a) Type where + the = typ . unTypeView + +typesDL :: Typed a => a -> DList Type +typesDL ty = return (typ ty) `mplus` otherTypesDL ty + +tyVars :: Typed a => a -> [Var] +tyVars = vars . TypeView + +cast :: Typed a => Type -> a -> Maybe a +cast ty x = do + s <- match (typ x) ty + return (typeSubst s x) + +-- Typed things that support function application. +class Typed a => Apply a where + -- Apply a function to its argument. + tryApply :: a -> a -> Maybe a + +infixl `apply` +apply :: Apply a => a -> a -> a +apply f x = + case tryApply f x of + Nothing -> + error $ + "apply: ill-typed term: can't apply " ++ + prettyShow (typ f) ++ " to " ++ prettyShow (typ x) + Just y -> y + +canApply :: Apply a => a -> a -> Bool +canApply f x = isJust (tryApply f x) + +-- Instances. +instance Typed Type where + typ = id + typeSubst_ = subst + +instance Apply Type where + tryApply (App (F Arrow) (Cons arg (Cons res Empty))) t + | t == arg = Just res + tryApply _ _ = Nothing + +instance (Typed a, Typed b) => Typed (a, b) where + typ (x, y) = build (app (fun (TyCon commaTyCon)) [typ x, typ y]) + otherTypesDL (x, y) = otherTypesDL x `mplus` otherTypesDL y + typeSubst_ f (x, y) = (typeSubst_ f x, typeSubst_ f y) + +instance (Typed a, Typed b) => Typed (Either a b) where + typ (Left x) = typ x + typ (Right x) = typ x + otherTypesDL (Left x) = otherTypesDL x + otherTypesDL (Right x) = otherTypesDL x + typeSubst_ sub (Left x) = Left (typeSubst_ sub x) + typeSubst_ sub (Right x) = Right (typeSubst_ sub x) + +instance Typed a => Typed [a] where + typ [] = typeOf () + typ (x:_) = typ x + otherTypesDL [] = mzero + otherTypesDL (x:xs) = otherTypesDL x `mplus` msum (map typesDL xs) + typeSubst_ f xs = map (typeSubst_ f) xs + +-- Represents a forall-quantifier over all the type variables in a type. +-- Wrapping a term in Poly normalises the type by alpha-renaming +-- type variables canonically. +newtype Poly a = Poly { unPoly :: a } + deriving (Eq, Ord, Show, Pretty, Typeable) + +poly :: Typed a => a -> Poly a +poly x = Poly (canonicaliseType x) + +canonicaliseType :: Typed a => a -> a +canonicaliseType = unTypeView . canonicalise . TypeView + +polyTyp :: Typed a => Poly a -> Poly Type +polyTyp (Poly x) = Poly (typ x) + +polyMap :: (Typed a, Typed b) => (a -> b) -> Poly a -> Poly b +polyMap f (Poly x) = poly (f x) + +polyRename :: (Typed a, Typed b) => a -> Poly b -> b +polyRename x (Poly y) = + unTypeView (renameAvoiding (TypeView x) (TypeView y)) + +polyApply :: (Typed a, Typed b, Typed c) => (a -> b -> c) -> Poly a -> Poly b -> Poly c +polyApply f (Poly x) y = poly (f x (polyRename x y)) + +polyPair :: (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b) +polyPair = polyApply (,) + +polyList :: Typed a => [Poly a] -> Poly [a] +polyList [] = poly [] +polyList (x:xs) = polyApply (:) x (polyList xs) + +polyMgu :: Poly Type -> Poly Type -> Maybe (Poly Type) +polyMgu ty1 ty2 = do + let (ty1', ty2') = unPoly (polyPair ty1 ty2) + sub <- unify ty1' ty2' + return (poly (typeSubst sub ty1')) + +instance Typed a => Typed (Poly a) where + typ = typ . unPoly + otherTypesDL = otherTypesDL . unPoly + typeSubst_ f (Poly x) = poly (typeSubst_ f x) + +instance Apply a => Apply (Poly a) where + tryApply f x = do + let (f', (x', resType)) = unPoly (polyPair f (polyPair x (poly (build (var (V 0)))))) + s <- unify (typ f') (arrowType [typ x'] resType) + let (f'', x'') = typeSubst s (f', x') + fmap poly (tryApply f'' x'') + +toPolyValue :: (Applicative f, Typeable a) => a -> Poly (Value f) +toPolyValue = poly . toValue . pure + +-- Dynamic values inside an applicative functor. +data Value f = + Value { + valueType :: Type, + value :: f Any } + +instance Show (Value f) where + show x = "<<" ++ prettyShow (typ x) ++ ">>" + +fromAny :: f Any -> f a +fromAny = unsafeCoerce + +toAny :: f a -> f Any +toAny = unsafeCoerce + +toValue :: forall f (a :: *). Typeable a => f a -> Value f +toValue x = Value (typeRep (Proxy :: Proxy a)) (toAny x) + +fromValue :: forall f (a :: *). Typeable a => Value f -> Maybe (f a) +fromValue x = do + guard (typ x == typeRep (Proxy :: Proxy a)) + return (fromAny (value x)) + +instance Typed (Value f) where + typ = valueType + typeSubst_ f (Value ty x) = Value (typeSubst_ f ty) x +instance Applicative f => Apply (Value f) where + tryApply f x = do + ty <- tryApply (typ f) (typ x) + return (Value ty (fromAny (value f) <*> value x)) + +-- Unwrap a value to get at the thing inside, while still being able +-- to wrap it up again. +data Unwrapped f = forall a. f a `In` Wrapper a +data Wrapper a = + Wrapper { + wrap :: forall g. g a -> Value g, + reunwrap :: forall g. Value g -> g a } + +unwrap :: Value f -> Unwrapped f +unwrap x = + value x `In` + Wrapper + (\y -> Value (typ x) y) + (\y -> + if typ x == typ y + then fromAny (value y) + else error "non-matching types") + +mapValue :: (forall a. f a -> g a) -> Value f -> Value g +mapValue f v = + case unwrap v of + x `In` w -> wrap w (f x) + +forValue :: Value f -> (forall a. f a -> g a) -> Value g +forValue x f = mapValue f x + +ofValue :: (forall a. f a -> b) -> Value f -> b +ofValue f v = + case unwrap v of + x `In` _ -> f x + +withValue :: Value f -> (forall a. f a -> b) -> b +withValue x f = ofValue f x + +pairValues :: forall f g. Typeable g => (forall a b. f a -> f b -> f (g a b)) -> Value f -> Value f -> Value f +pairValues f x y = + ty `seq` + Value { + valueType = ty, + value = toAny (f (value x) (value y)) } + where + ty = typeRep (Proxy :: Proxy g) `applyType` typ x `applyType` typ y + +wrapFunctor :: forall f g h. Typeable h => (forall a. f a -> g (h a)) -> Value f -> Value g +wrapFunctor f x = + ty `seq` + Value { + valueType = ty, + value = toAny (f (value x)) } + where + ty = typeRep (Proxy :: Proxy h) `applyType` valueType x + +unwrapFunctor :: forall f g h. Typeable g => (forall a. f (g a) -> h a) -> Value f -> Value h +unwrapFunctor f x = + case typ x of + App _ tys | tys@(_:_) <- unpack tys -> + case ty `applyType` last tys == typ x of + True -> + Value { + valueType = last tys, + value = f (fromAny (value x)) } + False -> + error "non-matching types" + _ -> error "value of type f a had wrong type" + where + ty = typeRep (Proxy :: Proxy g) diff --git a/src/QuickSpec/Utils.hs b/src/QuickSpec/Utils.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Utils.hs @@ -0,0 +1,122 @@ +-- | Miscellaneous utility functions. +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE CPP #-} +module QuickSpec.Utils where + +import Control.Arrow((&&&)) +import Control.Exception +import Data.List(groupBy, sortBy) +#if !MIN_VERSION_base(4,8,0) +import Data.Monoid +#endif +import Data.Ord(comparing) +import System.IO +import qualified Control.Category as Category +import qualified Data.Map.Strict as Map +import Data.Map(Map) +import Language.Haskell.TH.Syntax +import Data.Lens.Light + +(#) :: Category.Category cat => cat b c -> cat a b -> cat a c +(#) = (Category..) + +key :: Ord a => a -> Lens (Map a b) (Maybe b) +key x = lens (Map.lookup x) (\my m -> Map.alter (const my) x m) + +keyDefault :: Ord a => a -> b -> Lens (Map a b) b +keyDefault x y = lens (Map.findWithDefault y x) (\y m -> Map.insert x y m) + +reading :: (a -> Lens a b) -> Lens a b +reading f = lens (\x -> getL (f x) x) (\y x -> setL (f x) y x) + +fstLens :: Lens (a, b) a +fstLens = lens fst (\x (_, y) -> (x, y)) + +sndLens :: Lens (a, b) b +sndLens = lens snd (\y (x, _) -> (x, y)) + +makeLensAs :: Name -> [(String, String)] -> Q [Dec] +makeLensAs ty names = + nameMakeLens ty (\x -> lookup x names) + +repeatM :: Monad m => m a -> m [a] +repeatM = sequence . repeat + +partitionBy :: Ord b => (a -> b) -> [a] -> [[a]] +partitionBy value = + map (map fst) . + groupBy (\x y -> snd x == snd y) . + sortBy (comparing snd) . + map (id &&& value) + +collate :: Ord a => ([b] -> c) -> [(a, b)] -> [(a, c)] +collate f = map g . partitionBy fst + where + g xs = (fst (head xs), f (map snd xs)) + +isSorted :: Ord a => [a] -> Bool +isSorted xs = and (zipWith (<=) xs (tail xs)) + +isSortedBy :: Ord b => (a -> b) -> [a] -> Bool +isSortedBy f xs = isSorted (map f xs) + +usort :: Ord a => [a] -> [a] +usort = usortBy compare + +usortBy :: (a -> a -> Ordering) -> [a] -> [a] +usortBy f = map head . groupBy (\x y -> f x y == EQ) . sortBy f + +sortBy' :: Ord b => (a -> b) -> [a] -> [a] +sortBy' f = map snd . sortBy (comparing fst) . map (\x -> (f x, x)) + +usortBy' :: Ord b => (a -> b) -> [a] -> [a] +usortBy' f = map snd . usortBy (comparing fst) . map (\x -> (f x, x)) + +orElse :: Ordering -> Ordering -> Ordering +EQ `orElse` x = x +x `orElse` _ = x + +unbuffered :: IO a -> IO a +unbuffered x = do + buf <- hGetBuffering stdout + bracket_ + (hSetBuffering stdout NoBuffering) + (hSetBuffering stdout buf) + x + +newtype Max a = Max { getMax :: Maybe a } + +getMaxWith :: Ord a => a -> Max a -> a +getMaxWith x (Max (Just y)) = x `max` y +getMaxWith x (Max Nothing) = x + +instance Ord a => Monoid (Max a) where + mempty = Max Nothing + Max (Just x) `mappend` y = Max (Just (getMaxWith x y)) + Max Nothing `mappend` y = y + +newtype Min a = Min { getMin :: Maybe a } + +getMinWith :: Ord a => a -> Min a -> a +getMinWith x (Min (Just y)) = x `min` y +getMinWith x (Min Nothing) = x + +minimumBy :: (a -> a -> Bool) -> [a] -> a +minimumBy f = foldr1 (\x y -> if f x y then x else y) + +instance Ord a => Monoid (Min a) where + mempty = Min Nothing + Min (Just x) `mappend` y = Min (Just (getMinWith x y)) + Min Nothing `mappend` y = y + +labelM :: Monad m => (a -> m b) -> [a] -> m [(a, b)] +labelM f = mapM (\x -> do { y <- f x; return (x, y) }) + +#if __GLASGOW_HASKELL__ < 710 +isSubsequenceOf :: Ord a => [a] -> [a] -> Bool +[] `isSubsequenceOf` ys = True +(x:xs) `isSubsequenceOf` [] = False +(x:xs) `isSubsequenceOf` (y:ys) + | x == y = xs `isSubsequenceOf` ys + | otherwise = (x:xs) `isSubsequenceOf` ys +#endif diff --git a/src/Test/QuickSpec.hs b/src/Test/QuickSpec.hs deleted file mode 100644 --- a/src/Test/QuickSpec.hs +++ /dev/null @@ -1,90 +0,0 @@ --- | The main QuickSpec module. --- --- Look at the introduction (), --- read the examples (), --- or read the paper () --- before venturing in here. - -module Test.QuickSpec - (-- * Running QuickSpec - quickSpec, - sampleTerms, - - -- * The Signature class - Sig, - 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. - con, fun0, fun1, fun2, fun3, fun4, fun5, - -- * 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. - blind0, blind1, blind2, blind3, blind4, blind5, - -- * Adding variables to a signature - vars, - gvars, - -- * 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, observer2, observer3, observer4, - -- * Modifying a signature - background, - withDepth, - withSize, - withTests, - withQuickCheckSize, - without, - - -- * The standard QuickSpec prelude, to include in your own signatures - A, B, C, - Two, - prelude, - bools, - arith, - lists, - funs) - -where - -import Test.QuickSpec.Main -import Test.QuickSpec.Signature -import Test.QuickSpec.Prelude diff --git a/src/Test/QuickSpec/Approximate.hs b/src/Test/QuickSpec/Approximate.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Approximate.hs +++ /dev/null @@ -1,67 +0,0 @@ --- Utilities for testing functions that return partial results. -{-# LANGUAGE Rank2Types #-} -module Test.QuickSpec.Approximate where - -import Test.QuickCheck -import Test.QuickCheck.Gen -import Test.QuickCheck.Random -import Test.QuickSpec.Signature -import Test.QuickSpec.Term -import Test.QuickSpec.Utils -import Test.QuickSpec.Utils.Typeable -import Control.Monad -import Control.Monad.Trans.Reader -import Control.Spoon -import System.Random -import Data.Monoid - -newtype Plug = Plug { unPlug :: forall a. Partial a => Gen a -> Gen a } -type GP = ReaderT Plug Gen - -plug :: Partial a => GP a -> GP a -plug x = ReaderT (\plug -> unPlug plug (runReaderT x plug)) - -class (Typeable a, Arbitrary a, Eq a) => Partial a where - unlifted :: a -> GP a - unlifted x = return x - -lifted :: Partial a => a -> GP a -lifted x = plug (unlifted x) - -instance Partial () -instance Partial Int -instance Partial Integer -instance Partial Bool - -instance Partial a => Partial [a] where - unlifted [] = return [] - unlifted (x:xs) = liftM2 (:) (lifted x) (lifted xs) - -approximate :: Partial a => (forall a. Partial a => a -> Maybe a) -> QCGen -> Int -> a -> a -approximate eval g n x = unGen (runReaderT (lifted x) (Plug plug)) g n - where - plug :: forall a. Partial a => Gen a -> Gen a - plug x = - sized $ \m -> - if m == 0 then return (unGen arbitrary g 10) - else resize (m-1) $ do - y <- x - case eval y of - Just z -> return z - Nothing -> return (unGen arbitrary g 10) - -pobserver :: (Ord a, Partial a) => a -> Sig -pobserver x = observerSig (Observer (PGen (MkGen tot) (MkGen part))) - where tot g n y = approximate Just g n (y `asTypeOf` x) - part g n y = approximate spoony g n (y `asTypeOf` x) - -genPartial :: Partial a => a -> Gen a -genPartial x = runReaderT (lifted x) (Plug plug) - where - plug x = frequency [(1, undefined), (3, x)] - -pvars :: (Ord a, Partial a) => [String] -> a -> Sig -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/Equation.hs b/src/Test/QuickSpec/Equation.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Equation.hs +++ /dev/null @@ -1,42 +0,0 @@ --- | Equations. - -module Test.QuickSpec.Equation where - -import Test.QuickSpec.Term -import Test.QuickSpec.Signature hiding (vars) -import Test.QuickSpec.Utils.Typed -import Data.Monoid -import Data.List -import Data.Ord - -data Equation = Term :=: Term deriving (Eq, Ord) - -showEquation :: Sig -> Equation -> String -showEquation sig (t :=: u) = - show (mapVars f t) ++ " == " ++ show (mapVars f u) - where f = disambiguate sig (vars t ++ vars u) - -instance Show Equation where - show = showEquation mempty - -data TypedEquation a = Expr a :==: Expr a - -eraseEquation :: TypedEquation a -> Equation -eraseEquation (e1 :==: e2) = term e1 :=: term e2 - -instance Eq (TypedEquation a) where - e1 == e2 = e1 `compare` e2 == EQ - -instance Ord (TypedEquation a) where - compare = comparing eraseEquation - -instance Show (TypedEquation a) where - show = show . eraseEquation - -showTypedEquation :: Sig -> TypedEquation a -> String -showTypedEquation sig e = showEquation sig (eraseEquation e) - -equations :: [Several Expr] -> [Some TypedEquation] -equations = sortBy (comparing (some eraseEquation)) . - concatMap (several toEquations) - where toEquations (x:xs) = [Some (y :==: x) | y <- xs] diff --git a/src/Test/QuickSpec/Generate.hs b/src/Test/QuickSpec/Generate.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Generate.hs +++ /dev/null @@ -1,105 +0,0 @@ --- | The testing loop and term generation of QuickSpec. - -{-# LANGUAGE CPP, Rank2Types, TypeOperators, ScopedTypeVariables #-} -module Test.QuickSpec.Generate where - -#include "errors.h" -import Test.QuickSpec.Signature hiding (con) -import qualified Test.QuickSpec.TestTree as T -import Test.QuickSpec.TestTree(TestResults, reps, classes, numTests, numResults, cutOff, discrete) -import Test.QuickSpec.Utils.Typed -import Test.QuickSpec.Utils.TypeRel(TypeRel) -import qualified Test.QuickSpec.Utils.TypeRel as TypeRel -import Test.QuickSpec.Utils.TypeMap(TypeMap) -import qualified Test.QuickSpec.Utils.TypeMap as TypeMap -import Test.QuickSpec.Term -import Text.Printf -import Test.QuickSpec.Utils.Typeable -import Test.QuickSpec.Utils -import Test.QuickCheck.Gen hiding (generate) -import Test.QuickCheck.Random -import System.Random -import Control.Spoon -import Test.QuickSpec.Utils.MemoValuation - -terms :: Sig -> TypeRel Expr -> TypeRel Expr -terms = termsSatisfying (const True) - -termsSatisfying :: (Term -> Bool) -> Sig -> TypeRel Expr -> TypeRel Expr -termsSatisfying p sig base = - TypeMap.fromList - [ Some (O (terms' p sig base w)) - | Some (Witness w) <- usort (saturatedTypes sig ++ variableTypes sig) ] - -terms' :: Typeable a => (Term -> Bool) -> Sig -> TypeRel Expr -> a -> [Expr a] -terms' p sig base w = - filter (\t -> size 1 (term t) <= maxSize sig && p (term t)) $ - map var (TypeRel.lookup w (variables sig)) ++ - map con (TypeRel.lookup w (constants sig)) ++ - [ app f x - | Some (Witness w') <- lhsWitnesses sig w, - x <- TypeRel.lookup w' base, - not (isUndefined (term x)), - f <- terms' p sig base (const w), - arity f > 0, - not (isUndefined (term f)) ] - -test :: [(Valuation, QCGen, Int)] -> Sig -> - TypeMap (List `O` Expr) -> TypeMap (TestResults `O` Expr) -test vals sig ts = fmap (mapSome2 (test' vals sig)) ts - -test' :: forall a. Typeable a => - [(Valuation, QCGen, Int)] -> Sig -> [Expr a] -> TestResults (Expr a) -test' vals sig ts - | not (testable sig (undefined :: a)) = discrete ts - | otherwise = - case observe undefined sig of - Observer obs -> - let testCase (val, g, n) x = - spoony . unGen (partialGen obs) g n $ eval x val - in cutOff base increment (T.test (map testCase vals) ts) - where - base = minTests sig `div` 2 - increment = minTests sig - base - -genSeeds :: Int -> IO [(QCGen, Int)] -genSeeds maxSize = do - rnd <- newQCGen - let rnds rnd = rnd1 : rnds rnd2 where (rnd1, rnd2) = split rnd - return (zip (rnds rnd) (concat (repeat [0,2..maxSize]))) - -toValuation :: Strategy -> Sig -> (QCGen, Int) -> (Valuation, QCGen, Int) -toValuation strat sig (g, n) = - let (g1, g2) = split g - in (memoValuation sig (unGen (valuation strat) g1 n), g2, n) - -generate :: Bool -> Strategy -> Sig -> IO (TypeMap (TestResults `O` Expr)) -generate shutUp strat sig = generateTermsSatisfying shutUp (const True) strat sig - -generateTermsSatisfying :: Bool -> (Term -> Bool) -> Strategy -> Sig -> IO (TypeMap (TestResults `O` Expr)) -generateTermsSatisfying shutUp p strat sig | maxDepth sig < 0 = - ERROR "generate: maxDepth must be positive" -generateTermsSatisfying shutUp p strat sig | maxDepth sig == 0 = return TypeMap.empty -generateTermsSatisfying shutUp p strat sig = unbuffered $ do - let d = maxDepth sig - quietly x | shutUp = return () - | otherwise = x - rs <- fmap (TypeMap.mapValues2 reps) (generate shutUp (const partialGen) (updateDepth (d-1) sig)) - quietly $ printf "Depth %d: " d - let count :: ([a] -> a) -> (forall b. f (g b) -> a) -> - TypeMap (f `O` g) -> a - count op f = op . map (some2 f) . TypeMap.toList - ts = termsSatisfying p sig rs - quietly $ printf "%d terms, " (count sum length ts) - seeds <- genSeeds (maxQuickCheckSize sig) - let cs = test (map (toValuation strat sig) seeds) sig ts - quietly $ - printf "%d tests, %d evaluations, %d classes, %d raw equations.\n" - (count (maximum . (0:)) numTests cs) - (count sum numResults cs) - (count sum (length . classes) cs) - (count sum (sum . map (subtract 1 . length) . classes) cs) - return cs - -eraseClasses :: TypeMap (TestResults `O` Expr) -> [[Tagged Term]] -eraseClasses = concatMap (some (map (map (tagged term)) . classes . unO)) . TypeMap.toList diff --git a/src/Test/QuickSpec/Main.hs b/src/Test/QuickSpec/Main.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Main.hs +++ /dev/null @@ -1,166 +0,0 @@ --- | The main implementation of QuickSpec. - -{-# LANGUAGE CPP, TypeOperators #-} -module Test.QuickSpec.Main where - -#include "errors.h" - -import Test.QuickSpec.Generate -import Test.QuickSpec.Reasoning.NaiveEquationalReasoning hiding (universe, maxDepth) -import Test.QuickSpec.Utils.Typed -import qualified Test.QuickSpec.Utils.TypeMap as TypeMap -import qualified Test.QuickSpec.Utils.TypeRel as TypeRel -import Test.QuickSpec.Signature hiding (vars) -import Test.QuickSpec.Term hiding (symbols) -import Control.Monad -import Text.Printf -import Data.Monoid -import Test.QuickSpec.TestTree(TestResults, classes, reps) -import Data.List -import System.Random -import Data.Monoid -import Data.Maybe -import Test.QuickSpec.Utils -import Test.QuickSpec.Equation - -undefinedsSig :: Sig -> Sig -undefinedsSig sig = - background - [ undefinedSig "undefined" (undefined `asTypeOf` witness x) - | Some x <- saturatedTypes sig ] - -universe :: [[Tagged Term]] -> [Tagged Term] -universe css = filter (not . isUndefined . erase) (concat css) - -prune :: Context -> [Term] -> (a -> Equation) -> [a] -> [a] -prune ctx reps erase eqs = evalEQ ctx (filterM (fmap not . provable . erase) eqs) - where - provable (t :=: u) = do - res <- t =?= u - if res then return True else do - state <- get - -- Check that we won't unify two representatives---if we do - -- the equation is false - t =:= u - reps' <- mapM rep reps - if sort reps' == usort reps' then return False else do - put state - return True - -defines :: Equation -> Maybe Symbol -defines (t :=: u) = do - let isVar Var{} = True - isVar _ = False - - acyclic t = - all acyclic (args t) && - case functor t == functor u of - True -> usort (map Var (vars t)) `isProperSubsetOf` args u - False -> True - xs `isProperSubsetOf` ys = xs `isSubsetOf` ys && sort xs /= sort ys - xs `isSubsetOf` ys = sort xs `isSublistOf` sort ys - [] `isSublistOf` _ = True - (x:xs) `isSublistOf` [] = False - (x:xs) `isSublistOf` (y:ys) - | x == y = xs `isSublistOf` ys - | otherwise = (x:xs) `isSublistOf` ys - - guard (all isVar (args u) && usort (args u) == args u && - acyclic t && vars t `isSubsetOf` vars u) - - return (functor u) - -definitions :: [Equation] -> [Equation] -definitions es = [ e | e <- es, defines e /= Nothing ] - -runTool :: Signature a => (Sig -> IO ()) -> a -> IO () -runTool tool sig_ = do - putStrLn "== API ==" - putStr (show (signature sig_)) - let sig = signature sig_ `mappend` undefinedsSig (signature sig_) - - tool sig - -data Target = Target Symbol | NoTarget deriving (Eq, Ord) - -target :: Equation -> Target -target (t :=: u) = - case usort (filter p (funs t ++ funs u)) of - [f] -> Target f - _ -> NoTarget - where p x = not (silent x) && symbolArity x > 0 - -innerZip :: [a] -> [[b]] -> [[(a,b)]] -innerZip [] _ = [] -innerZip _ [] = [] -innerZip xs ([]:yss) = []:innerZip xs yss -innerZip (x:xs) ((y:ys):yss) = - let (zs:zss) = innerZip xs (ys:yss) - in ((x,y):zs):zss - --- | Run QuickSpec on a signature. -quickSpec :: Signature a => a -> IO () -quickSpec = runTool $ \sig -> do - putStrLn "== Testing ==" - r <- generate False (const partialGen) sig - let clss = concatMap (some2 (map (Some . O) . classes)) (TypeMap.toList r) - univ = concatMap (some2 (map (tagged term))) clss - reps = map (some2 (tagged term . head)) clss - eqs = equations clss - printf "%d raw equations; %d terms in universe.\n\n" - (length eqs) - (length reps) - - let ctx = initial (maxDepth sig) (symbols sig) univ - allEqs = map (some eraseEquation) eqs - isBackground = all silent . eqnFuns - keep eq = not (isBackground eq) || absurd eq - absurd (t :=: u) = absurd1 t u || absurd1 u t - absurd1 (Var x) t = x `notElem` vars t - absurd1 _ _ = False - (background, foreground) = - partition isBackground allEqs - pruned = filter keep - (prune ctx (filter (not . isUndefined) (map erase reps)) id - (background ++ foreground)) - eqnFuns (t :=: u) = funs t ++ funs u - isGround (t :=: u) = null (vars t) && null (vars u) - byTarget = innerZip [1 :: Int ..] (partitionBy target pruned) - - forM_ byTarget $ \eqs@((_,eq):_) -> do - case target eq of - NoTarget -> putStrLn "== Equations about several functions ==" - Target f -> printf "== Equations about %s ==\n" (show f) - forM_ eqs $ \(i, eq) -> - printf "%3d: %s\n" i (showEquation sig eq) - putStrLn "" - -sampleList :: StdGen -> Int -> [a] -> [a] -sampleList g n xs | n >= length xs = xs - | otherwise = aux g n (length xs) xs - where - aux g 0 _ _ = [] - aux g _ _ [] = ERROR "sampleList: bug in sampling" - aux g size len (x:xs) - | i <= size = x:aux g' (size-1) (len-1) xs - | otherwise = aux g' size (len-1) xs - where (i, g') = randomR (1, len) g - --- | 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 () -sampleTerms = runTool $ \sig -> do - putStrLn "== Testing ==" - r <- generate False (const partialGen) (updateDepth (maxDepth sig - 1) sig) - let univ = sort . concatMap (some2 (map term)) . TypeMap.toList . terms sig . - TypeMap.mapValues2 reps $ r - printf "Universe contains %d terms.\n\n" (length univ) - - let numTerms = 100 - - printf "== Here are %d terms out of a total of %d ==\n" numTerms (length univ) - g <- newStdGen - forM_ (zip [1 :: Int ..] (sampleList g numTerms univ)) $ \(i, t) -> - printf "%d: %s\n" i (show (mapVars (disambiguate sig (vars t)) t)) - - putStrLn "" diff --git a/src/Test/QuickSpec/Prelude.hs b/src/Test/QuickSpec/Prelude.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Prelude.hs +++ /dev/null @@ -1,96 +0,0 @@ --- | The \"prelude\": a standard signature containing useful functions --- like '++', which can be used as background theory. - -{-# LANGUAGE ScopedTypeVariables, DeriveDataTypeable, GeneralizedNewtypeDeriving #-} -module Test.QuickSpec.Prelude where - -import Test.QuickSpec.Signature -import Test.QuickSpec.Approximate -import Test.QuickCheck -import Data.Typeable - --- | Just a type. --- You can instantiate your polymorphic functions at this type --- to include them in a signature. -newtype A = A Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Show) -newtype B = B Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Show) -newtype C = C Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Show) - -instance Partial A where unlifted (A x) = fmap A (unlifted x) -instance Partial B where unlifted (B x) = fmap B (unlifted x) -instance Partial C where unlifted (C x) = fmap C (unlifted x) - --- | A type with two elements. --- Use this instead of @A@ if testing doesn't work well because --- the domain of @A@ is too large. -data Two = One | Two deriving (Eq, Ord, Typeable, Show) - -instance Arbitrary Two where - arbitrary = elements [One, Two] - -instance CoArbitrary Two where - coarbitrary One = variant 0 - coarbitrary Two = variant (-1) - --- | A signature containing boolean functions: --- @(`||`)@, @(`&&`)@, `not`, `True`, `False`. -bools :: Sig -bools = background [ - ["x", "y", "z"] `vars` (undefined :: Bool), - - "||" `fun2` (||), - "&&" `fun2` (&&), - "not" `fun1` not, - "True" `fun0` True, - "False" `fun0` False] - --- | A signature containing arithmetic operations: --- @0@, @1@, @(`+`)@, @(`*`)@. --- Instantiate it with e.g. @arith (undefined :: `Int`)@. -arith :: forall a. (Typeable a, Ord a, Num a, Arbitrary a) => a -> Sig -arith _ = background [ - ["x", "y", "z"] `vars` (undefined :: a), - - "0" `fun0` (0 :: a), - "1" `fun0` (1 :: a), - "+" `fun2` ((+) :: a -> a -> a), - "*" `fun2` ((*) :: a -> a -> a)] - --- | A signature containing list operations: --- @[]@, @(:)@, `head`, `tail`, @(`++`)@. --- Instantiate it with e.g. @lists (undefined :: `A`)@. -lists :: forall a. (Typeable a, Ord a, Arbitrary a) => a -> Sig -lists _ = background [ - ["xs", "ys", "zs"] `vars` (undefined :: [a]), - - "[]" `fun0` ([] :: [a]), - ":" `fun2` ((:) :: a -> [a] -> [a]), - "head" `fun1` (head :: [a] -> a), - "tail" `fun1` (tail :: [a] -> [a]), - "++" `fun2` ((++) :: [a] -> [a] -> [a])] - --- | A signature containing higher-order functions: --- @(`.`)@, `id`, and some function variables. --- Useful for testing `map`. -funs :: forall a. (Typeable a, Ord a, Arbitrary a, CoArbitrary a) => a -> Sig -funs _ = background [ - ["f", "g", "h"] `vars` (undefined :: a -> a), - - "." `blind2` ((.) :: (a -> a) -> (a -> a) -> (a -> a)), - "id" `blind0` (id :: a -> a), - - observer2 (\(x :: a) (f :: a -> a) -> f x) - ] - --- | The QuickSpec prelude. --- 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, - bools, - arith (undefined :: Int), - lists a ] diff --git a/src/Test/QuickSpec/Reasoning/CongruenceClosure.hs b/src/Test/QuickSpec/Reasoning/CongruenceClosure.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Reasoning/CongruenceClosure.hs +++ /dev/null @@ -1,167 +0,0 @@ --- | A decision procedure for ground equality, --- based on the paper "Proof-producing Congruence Closure". - -module Test.QuickSpec.Reasoning.CongruenceClosure(CC, newSym, (=:=), (=?=), rep, evalCC, execCC, runCC, ($$), S, funUse, argUse, lookup, initial, frozen) where - -import Prelude hiding (lookup) -import Control.Monad -import Control.Monad.Trans.State.Strict -import Data.IntMap(IntMap) -import qualified Data.IntMap as IntMap -import Test.QuickSpec.Reasoning.UnionFind(UF, Replacement((:>))) -import qualified Test.QuickSpec.Reasoning.UnionFind as UF -import Data.Maybe -import Data.List(foldl') --- import Test.QuickCheck --- import Test.QuickCheck.Arbitrary --- import Test.QuickCheck.Monadic -import Text.Printf - -lookup2 :: Int -> Int -> IntMap (IntMap a) -> Maybe a -lookup2 k1 k2 m = IntMap.lookup k2 (IntMap.findWithDefault IntMap.empty k1 m) - -insert2 :: Int -> Int -> a -> IntMap (IntMap a) -> IntMap (IntMap a) -insert2 k1 k2 v m = IntMap.insertWith IntMap.union k1 (IntMap.singleton k2 v) m - -delete2 :: Int -> Int -> IntMap (IntMap a) -> IntMap (IntMap a) -delete2 k1 k2 m = IntMap.adjust (IntMap.delete k2) k1 m - -data FlatEqn = (Int, Int) := Int deriving (Eq, Ord) - -data S = S { - -- in all these maps, the keys are representatives, the values may not be - funUse :: !(IntMap [(Int, Int)]), - argUse :: !(IntMap [(Int, Int)]), - lookup :: IntMap (IntMap Int), - uf :: UF.S - } - -type CC = State S - -liftUF :: UF a -> CC a -liftUF m = do - s <- get - let (x, uf') = UF.runUF (uf s) m - put s { uf = uf' } - return x - -invariant :: String -> CC () -invariant _ = return () --- invariant str = do --- S funUse argUse lookup <- get --- -- keys of all maps are representatives --- let check phase x = do --- b <- liftUF (UF.isRep x) --- if b then return () else error (printf "%s, %s appears as a key in %s but is not a rep in:\nfunUse=%s\nargUse=%s\nlookup=%s" str (show x) phase (show funUse) (show argUse) (show lookup)) --- mapM_ (check "funUse") (IntMap.keys funUse) --- mapM_ (check "argUse") (IntMap.keys argUse) --- mapM_ (check "lookup") (IntMap.keys lookup) --- mapM_ (mapM_ (check "inner lookup") . IntMap.keys) (IntMap.elems lookup) - -modifyFunUse f = modify (\s -> s { funUse = f (funUse s) }) -modifyArgUse f = modify (\s -> s { argUse = f (argUse s) }) -addFunUses xs s = modifyFunUse (IntMap.insertWith (++) s xs) -addArgUses xs s = modifyArgUse (IntMap.insertWith (++) s xs) -modifyLookup f = modify (\s -> s { lookup = f (lookup s) }) -putLookup l = modifyLookup (const l) - -newSym :: CC Int -newSym = liftUF UF.newSym - -($$) :: Int -> Int -> CC Int -f $$ x = do - invariant (printf "before %s$$%s" (show f) (show x)) - m <- gets lookup - f' <- rep f - x' <- rep x - invariant (printf "at %s$$%s:1" (show f) (show x)) - case lookup2 x' f' m of - Nothing -> do - c <- newSym - invariant (printf "at %s$$%s:2" (show f) (show x)) - putLookup (insert2 x' f' c m) - addFunUses [(x', c)] f' - addArgUses [(f', c)] x' - invariant (printf "after %s$$%s" (show f) (show x)) - return c - Just k -> return k - -(=:=) :: Int -> Int -> CC Bool -a =:= b = propagate (a, b) - -(=?=) :: Int -> Int -> CC Bool -t =?= u = liftM2 (==) (rep t) (rep u) - -propagate (a, b) = do - (unified, pending) <- propagate1 (a, b) - mapM_ propagate pending - return unified - -propagate1 (a, b) = do - invariant (printf "before propagate (%s, %s)" (show a) (show b)) - res <- liftUF (a UF.=:= b) - case res of - Nothing -> return (False, []) - Just (r :> r') -> do - funUses <- gets (IntMap.lookup r . funUse) - argUses <- gets (IntMap.lookup r . argUse) - case (funUses, argUses) of - (Nothing, Nothing) -> return (True, []) - _ -> fmap (\x -> (True, x)) (updateUses r r' (fromMaybe [] funUses) (fromMaybe [] argUses)) - -updateUses r r' funUses argUses = do - modifyFunUse (IntMap.delete r) - modifyArgUse (IntMap.delete r) - modifyLookup (IntMap.delete r) - forM_ funUses $ \(x, _) -> do - x' <- rep x - modifyLookup (delete2 x' r) - invariant (printf "after deleting %s" (show r)) - let repPair (x, c) = do - x' <- rep x - return (x', c) - funUses' <- mapM repPair funUses - argUses' <- mapM repPair argUses - - m <- gets lookup - - let foldUses insert lookup pending m uses = foldl' op e uses - where op (pending, newUses, m) (x', c) = - case lookup x' m of - Just k -> ((c, k):pending, newUses, m) - Nothing -> (pending, (x', c):newUses, insert x' c m) - e = (pending, [], m) - - (funPending, funNewUses, m') = foldUses (\x' c m -> insert2 x' r' c m) - (\x' m -> lookup2 x' r' m) - [] m funUses' - - (pending, argNewUses, argM) = foldUses IntMap.insert IntMap.lookup funPending - (IntMap.findWithDefault IntMap.empty r' m') - argUses' - - addFunUses funNewUses r' - addArgUses argNewUses r' - - putLookup (if IntMap.null argM then m' else IntMap.insert r' argM m') - invariant (printf "after updateUses (%s, %s)" (show r) (show r')) - - return pending - -rep :: Int -> CC Int -rep s = liftUF (UF.rep s) - -runCC :: S -> CC a -> (a, S) -runCC s m = runState m s - -evalCC :: S -> CC a -> a -evalCC s m = fst (runCC s m) - -execCC :: S -> CC a -> S -execCC s m = snd (runCC s m) - -initial :: Int -> S -initial n = S IntMap.empty IntMap.empty IntMap.empty (UF.initial n) - -frozen :: CC a -> CC a -frozen x = fmap (evalState x) get diff --git a/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs b/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs +++ /dev/null @@ -1,128 +0,0 @@ --- | Equational reasoning built on top of congruence closure. - -{-# LANGUAGE CPP, TupleSections #-} -module Test.QuickSpec.Reasoning.NaiveEquationalReasoning where - -#include "errors.h" - -import Test.QuickSpec.Term -import Test.QuickSpec.Equation -import Test.QuickSpec.Reasoning.CongruenceClosure(CC) -import qualified Test.QuickSpec.Reasoning.CongruenceClosure as CC -import Data.Map(Map) -import qualified Data.Map as Map -import Data.IntMap(IntMap) -import qualified Data.IntMap as IntMap -import Control.Monad -import Control.Monad.Trans.Reader -import Control.Monad.Trans.State.Strict -import qualified Control.Monad.Trans.State.Strict as S -import Test.QuickSpec.Utils -import Test.QuickSpec.Utils.Typed -import Test.QuickSpec.Utils.Typeable -import Data.Ord -import Data.List - -data Context = Context { - rel :: CC.S, - maxDepth :: Int, - universe :: IntMap Universe - } - -type Universe = IntMap [Int] - -type EQ = ReaderT (Int, IntMap Universe) CC - -initial :: Int -> [Symbol] -> [Tagged Term] -> Context -initial d syms ts = - let n = 1+maximum (0:map index syms) - (universe, rel) = - CC.runCC (CC.initial n) $ - forM (partitionBy (witnessType . tag) ts) $ \xs@(x:_) -> - fmap (witnessType (tag x),) (createUniverse (map erase xs)) - univMap = Map.fromList universe - - in Context rel d . IntMap.fromList $ [ - (index sym, - Map.findWithDefault IntMap.empty (symbolType sym) univMap) - | sym <- syms ] - -createUniverse :: [Term] -> CC Universe -createUniverse ts = fmap IntMap.fromList (mapM createTerms tss) - where tss = partitionBy depth ts - createTerms ts@(t:_) = fmap (depth t,) (mapM flatten ts) - -runEQ :: Context -> EQ a -> (a, Context) -runEQ ctx x = (y, ctx { rel = rel' }) - where (y, rel') = runState (runReaderT x (maxDepth ctx, universe ctx)) (rel ctx) - -evalEQ :: Context -> EQ a -> a -evalEQ ctx x = fst (runEQ ctx x) - -execEQ :: Context -> EQ a -> Context -execEQ ctx x = snd (runEQ ctx x) - -liftCC :: CC a -> EQ a -liftCC x = ReaderT (const x) - -(=?=) :: Term -> Term -> EQ Bool -t =?= u = liftCC $ do - x <- flatten t - y <- flatten u - x CC.=?= y - -equal :: Equation -> EQ Bool -equal (t :=: u) = t =?= u - -(=:=) :: Term -> Term -> EQ Bool -t =:= u = unify (t :=: u) - -unify :: Equation -> EQ Bool -unify (t :=: u) = do - (d, ctx) <- ask - b <- t =?= u - unless b $ - forM_ (substs t ctx d ++ substs u ctx d) $ \s -> liftCC $ do - t' <- subst s t - u' <- subst s u - t' CC.=:= u' - return b - -type Subst = Symbol -> Int - -substs :: Term -> IntMap Universe -> Int -> [Subst] -substs t univ d = map lookup (sequence (map choose vars)) - where vars = map (maximumBy (comparing snd)) . - partitionBy fst . - holes $ t - - choose (x, n) = - let m = IntMap.findWithDefault (ERROR "empty universe") - (index x) univ in - [ (x, t) - | d' <- [0..d-n], - t <- IntMap.findWithDefault [] d' m ] - - lookup ss = - let m = IntMap.fromList [ (index x, y) | (x, y) <- ss ] - in \x -> IntMap.findWithDefault (index x) (index x) m - -subst :: Subst -> Term -> CC Int -subst s (Var x) = return (s x) -subst s (Const x) = return (index x) -subst s (App f x) = do - f' <- subst s f - x' <- subst s x - f' CC.$$ x' - -flatten :: Term -> CC Int -flatten = subst index - -get :: EQ CC.S -get = liftCC S.get - -put :: CC.S -> EQ () -put x = liftCC (S.put x) - -rep :: Term -> EQ Int -rep x = liftCC (flatten x >>= CC.rep) diff --git a/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs b/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs +++ /dev/null @@ -1,141 +0,0 @@ --- | Equational reasoning that deals with partial functions. --- Only used in HipSpec at the moment. - -{-# LANGUAGE CPP #-} -module Test.QuickSpec.Reasoning.PartialEquationalReasoning where - -#include "errors.h" -import Test.QuickSpec.Equation -import Test.QuickSpec.Term hiding (Variable, vars) -import qualified Test.QuickSpec.Term as Term -import Test.QuickSpec.Utils.Typed -import qualified Test.QuickSpec.Reasoning.NaiveEquationalReasoning as EQ -import Test.QuickSpec.Reasoning.NaiveEquationalReasoning(EQ, evalEQ, runEQ) -import Data.IntMap(IntMap) -import qualified Data.IntMap as IntMap -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] -data Totality = Partial | Total [Int] | Variable deriving (Eq, Ord, Show) - -instance Eq PEquation where - e1 == e2 = e1 `compare` e2 == EQ - -instance Ord PEquation where - compare = comparing stamp - where stamp (pre :\/: eq) = (eq, length pre, usort pre) - -instance Show PEquation where - show = showPEquation mempty - -showPEquation :: Sig -> PEquation -> String -showPEquation sig (pre :\/: t :=: u) = - show (mapVars f t) ++ " == " ++ show (mapVars f u) ++ - showPre (map f pre) - where f = disambiguate sig (Term.vars t ++ Term.vars u ++ pre) - showPre [] = "" - showPre xs = " when " ++ conjunction (map show xs) ++ " " ++ plural xs "is" "are" ++ " partial" - plural xs x y - | length xs == 1 = x - | otherwise = y - conjunction [x] = x - conjunction xs = - intercalate ", " (init xs) ++ " and " ++ last xs - -infix 5 :\/: - -data Context = Context { - total :: EQ.Context, - partial :: IntMap EQ.Context, - vars :: IntMap Symbol - } - -type PEQ = State Context - -initial :: Int -> [(Symbol, Totality)] -> [Tagged Term] -> Context -initial d syms univ - | ok syms = Context total partial vars - | otherwise = __ - where - ok syms = and (zipWith (==) [0..] (map (index . fst) syms)) - total = EQ.initial d (map fst syms) (filter (isTotal Nothing [] . erase) univ) - partial = IntMap.fromList [ - (i, EQ.initial d (map fst syms) (filter (isTotal (Just i) [] . erase) univ)) - | (i, (sym, Variable)) <- zip [0..] syms - ] - totality = IntMap.fromList [(index sym, tot) | (sym, tot) <- syms] - isTotal ctx args (Var x) = ctx /= Just (index x) && all (isTotal ctx []) args - isTotal ctx args (App f x) = isTotal ctx (x:args) f - isTotal ctx args (Const x) = - case IntMap.findWithDefault - (ERROR "type not found") - (index x) totality of - Partial -> False - Total pre -> and [ isTotal ctx [] arg || i `elem` pre | (i, arg) <- zip [0..] args ] - Variable -> __ - vars = IntMap.fromList [(index s, s) | (s, Variable) <- syms] - -runPEQ :: Context -> PEQ a -> (a, Context) -runPEQ = flip runState - -evalPEQ :: Context -> PEQ a -> a -evalPEQ ctx x = fst (runPEQ ctx x) - -execPEQ :: Context -> PEQ a -> Context -execPEQ ctx x = snd (runPEQ ctx x) - -liftEQ :: [Int] -> (Maybe Int -> EQ a) -> PEQ [a] -liftEQ pre x = do - Context total partial vars <- S.get - let (totalRes, total') = runEQ total (x Nothing) - (partialRes, partial') = IntMap.mapAccumWithKey f [] partial - f rs i ctx - | i `elem` pre = runEQ ctx (fmap (:rs) (x (Just i))) - | otherwise = (rs, ctx) - S.put (Context total' partial' vars) - return (totalRes:partialRes) - -equal :: PEquation -> PEQ Bool -equal (pre :\/: t :=: u) = liftM2 (==) (rep pre t) (rep pre u) - -irrelevant :: Equation -> PEQ Precondition -irrelevant (t :=: u) = do - vs <- gets (IntMap.elems . vars) - return (vs \\ (Term.vars t `intersect` Term.vars u)) - -unify :: PEquation -> PEQ Bool -unify (pre :\/: eq) = do - irr <- irrelevant eq - fmap and . liftEQ (map index (pre ++ irr)) $ \n -> - case n of - Just i | i `notElem` map index pre -> return True - _ -> EQ.unify eq - -precondition :: Equation -> PEQ Precondition -precondition eq = do - Context _ partial vars <- S.get - fmap concat . liftEQ (IntMap.keys partial) $ \n -> - case n of - Nothing -> return [] - Just i -> do - r <- EQ.equal eq - if r then - return [IntMap.findWithDefault (ERROR "precondition: var not found") i vars] - else return [] - -get :: PEQ Context -get = S.get - -put :: Context -> PEQ () -put = S.put - -rep :: Precondition -> Term -> PEQ [Int] -rep pre t = liftEQ (map index pre) (const (EQ.rep t)) diff --git a/src/Test/QuickSpec/Reasoning/UnionFind.hs b/src/Test/QuickSpec/Reasoning/UnionFind.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Reasoning/UnionFind.hs +++ /dev/null @@ -1,64 +0,0 @@ --- | A union-find data structure. - -module Test.QuickSpec.Reasoning.UnionFind(UF, Replacement((:>)), newSym, (=:=), rep, evalUF, execUF, runUF, S, isRep, initial) where - -import Prelude hiding (min) -import Control.Monad -import Control.Monad.Trans.State.Strict -import Data.IntMap(IntMap) -import qualified Data.IntMap as IntMap - -data S = S { - links :: IntMap Int, - sym :: Int - } - -type UF = State S -data Replacement = Int :> Int - -runUF :: S -> UF a -> (a, S) -runUF s m = runState m s - -evalUF :: S -> UF a -> a -evalUF s m = fst (runUF s m) - -execUF :: S -> UF a -> S -execUF s m = snd (runUF s m) - -initial :: Int -> S -initial n = S IntMap.empty n - -modifyLinks f = modify (\s -> s { links = f (links s) }) -modifySym f = modify (\s -> s { sym = f (sym s) }) -putLinks l = modifyLinks (const l) - -newSym :: UF Int -newSym = do - s <- get - modifySym (+1) - return (sym s) - -(=:=) :: Int -> Int -> UF (Maybe Replacement) -s =:= t | s == t = return Nothing -s =:= t = do - rs <- rep s - rt <- rep t - if (rs /= rt) then do - modifyLinks (IntMap.insert rs rt) - return (Just (rs :> rt)) - else return Nothing - -rep :: Int -> UF Int -rep t = do - m <- fmap links get - case IntMap.lookup t m of - Nothing -> return t - Just t' -> do - r <- rep t' - when (t' /= r) $ modifyLinks (IntMap.insert t r) - return r - -isRep :: Int -> UF Bool -isRep t = do - t' <- rep t - return (t == t') diff --git a/src/Test/QuickSpec/Signature.hs b/src/Test/QuickSpec/Signature.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Signature.hs +++ /dev/null @@ -1,590 +0,0 @@ --- | Functions for constructing and analysing signatures. - -{-# LANGUAGE CPP, Rank2Types, ExistentialQuantification, ScopedTypeVariables, DeriveDataTypeable #-} -module Test.QuickSpec.Signature where - -#include "errors.h" -import Control.Applicative hiding (some) -import Test.QuickSpec.Utils.Typeable -import Data.Monoid -import Test.QuickCheck -import Test.QuickSpec.Term hiding (var, vars) -import Test.QuickSpec.Utils.Typed -import qualified Test.QuickSpec.Utils.TypeMap as TypeMap -import Test.QuickSpec.Utils.TypeMap(TypeMap) -import qualified Test.QuickSpec.Utils.TypeRel as TypeRel -import Test.QuickSpec.Utils.TypeRel(TypeRel) -import Data.List -import qualified Data.Map as Map -import Test.QuickSpec.Utils -import Data.Maybe -import Control.Monad - --- | The class of things that can be used as a signature. -class Signature a where - signature :: a -> Sig - -instance Signature Sig where - signature = id - -instance Signature a => Signature [a] where - signature = mconcat . map signature - --- | A signature. -data Sig = Sig { - -- Constants, variables, generators and observation functions. - constants :: TypeRel Constant, - variables :: TypeRel Variable, - total :: TypeMap Gen, - partial :: TypeMap Gen, - observers :: TypeMap Observer, - - -- Ord instances, added whenever the 'fun' family of functions is used. - ords :: TypeMap Observer, - - -- Witnesses for Typeable. The following types must have witnesses: - -- * Any function argument. - -- * Any function result. - -- * Any partially-applied function type. - -- * Any variable type. - witnesses :: TypeMap Witnessed, - - -- Depth of terms in the universe. - maxDepth_ :: First Int, - - -- Size of terms in the universe. - maxSize_ :: First Int, - - -- Minimum number of tests to run. - minTests_ :: First Int, - - -- Maximum size parameter to pass to QuickCheck. - maxQuickCheckSize_ :: First Int - } deriving Typeable - -maxDepth :: Sig -> Int -maxDepth = fromMaybe 3 . getFirst . maxDepth_ - -maxSize :: Sig -> Int -maxSize = fromMaybe 100 . getFirst . maxSize_ - -updateDepth :: Int -> Sig -> Sig -updateDepth n sig = sig { maxDepth_ = First (Just n) } - -updateSize :: Int -> Sig -> Sig -updateSize n sig = sig { maxSize_ = First (Just n) } - -minTests :: Sig -> Int -minTests = fromMaybe 500 . getFirst . minTests_ - -maxQuickCheckSize :: Sig -> Int -maxQuickCheckSize = fromMaybe 20 . getFirst . maxQuickCheckSize_ - -instance Show Sig where show = show . summarise - -data Used = Used Witness [Symbol] -instance Show Used where - show (Used w ks) = - show w ++ " (used in " ++ intercalate ", " (map show ks) ++ ")" - -uses :: Sig -> Witness -> Used -uses sig w = - Used w - [ sym (unConstant k) - | Some k <- TypeRel.toList (constants sig), - w' <- constantArgs sig k, - w == w' ] - -data Summary = Summary { - summaryFunctions :: [Symbol], - summaryBackground :: [Symbol], - summaryVariables :: [Symbol], - summaryObserved :: [TypeRep], - summaryUninhabited :: [Used], - summaryNoVars :: [TypeRep], - summaryUntestable :: [TypeRep], - summaryDepth :: Maybe Int, - summarySize :: Maybe Int, - summaryTests :: Maybe Int, - summaryQuickCheckSize :: Maybe Int - } - -instance Show Summary where - show summary = unlines $ - section ["-- functions --"] (decls (summaryFunctions summary)) ++ - section ["-- background functions --"] (decls (summaryBackground summary)) ++ - section ["-- variables --"] (decls (summaryVariables summary)) ++ - section ["-- the following types are using non-standard equality --"] - (map show (summaryObserved summary)) ++ - section ["-- WARNING: the following types are uninhabited --"] - (map show (summaryUninhabited summary)) ++ - section ["-- WARNING: there are no variables of the following types; consider adding some --"] - (map show (summaryNoVars summary)) ++ - section ["-- WARNING: cannot test the following types; ", - " consider using 'fun' instead of 'blind' or using 'observe' --"] - (map show (summaryUntestable summary)) - where - section _ [] = [] - section msg xs = msg ++ xs ++ [""] - - decls xs = map decl (partitionBy symbolType xs) - - decl xs@(x:_) = - intercalate ", " (map show xs) ++ " :: " ++ show (symbolType x) - -sigToHaskell :: Signature a => a -> String -sigToHaskell sig = "signature [\n" ++ intercalate ",\n" (map (" " ++) ls) ++ "]" - where - summary = summarise (signature sig) - ls = - [ function s | s <- summaryFunctions summary ] ++ - [ background s | s <- summaryBackground summary ] ++ - [ variable ss | ss <- partitionBy symbolType (summaryVariables summary) ] ++ - [ "withDepth " ++ show n | Just n <- [summaryDepth summary] ] ++ - [ "withSize " ++ show n | Just n <- [summarySize summary] ] ++ - [ "withTests " ++ show n | Just n <- [summaryTests summary] ] ++ - [ "withQuickCheckSize " ++ show n | Just n <- [summaryQuickCheckSize summary] ] - function s = "\"" ++ show s ++ "\" `fun" ++ show (symbolArity s) ++ "` (" ++ - show s ++ " :: " ++ show (symbolType s) ++ ")" - background s = "background $ " ++ function s - variable ss@(s:_) = - show (map name ss) ++ " `vars" ++ show (symbolArity s) ++ - "` (undefined :: " ++ show (symbolType s) ++ ")" - -summarise :: Sig -> Summary -summarise sig = - Summary { - summaryFunctions = filter (not . silent) allConstants, - summaryBackground = filter silent allConstants, - summaryVariables = allVariables, - summaryObserved = Map.keys (observers sig), - summaryUninhabited = - [ uses sig ty - | ty <- argumentTypes sig, - ty `notElem` inhabitedTypes sig, - ty `notElem` variableTypes sig ], - summaryNoVars = - [ witnessType ty - | ty <- argumentTypes sig, - -- There is a non-variable term of this type and it appears as the - -- argument to some function - ty `elem` inhabitedTypes sig, - ty `notElem` variableTypes sig ], - summaryUntestable = - [ witnessType ty - | ty@(Some (Witness w)) <- saturatedTypes sig, - -- The type is untestable and is the result type of a constant - not (testable sig w) ], - summaryDepth = getFirst (maxDepth_ sig), - summarySize = getFirst (maxSize_ sig), - summaryTests = getFirst (minTests_ sig), - summaryQuickCheckSize = getFirst (maxQuickCheckSize_ sig) } - - where - symbols :: (Sig -> TypeRel f) -> (forall a. f a -> Symbol) -> [Symbol] - symbols f erase = map (some erase) (TypeRel.toList (f sig)) - - allConstants = symbols constants (sym . unConstant) - allVariables = symbols variables (sym . unVariable) - -data Observer a = forall b. Ord b => Observer (PGen (a -> b)) - -observe x sig = - TypeMap.lookup (TypeMap.lookup (ERROR msg) x (ords sig)) - x (observers sig) - where msg = "no observers found for type " ++ show (typeOf x) - -emptySig :: Sig -emptySig = Sig TypeRel.empty TypeRel.empty TypeMap.empty TypeMap.empty TypeMap.empty TypeMap.empty TypeMap.empty mempty mempty mempty mempty - -instance Monoid Sig where - mempty = emptySig - s1 `mappend` s2 = - Sig { - constants = renumber (mapConstant . alter) (length variables') constants', - variables = renumber (mapVariable . alter) 0 variables', - observers = observers s1 `mappend` observers s2, - total = total s1 `mappend` total s2, - partial = partial s1 `mappend` partial s2, - ords = ords s1 `mappend` ords s2, - witnesses = witnesses s1 `mappend` witnesses s2, - maxDepth_ = maxDepth_ s1 `mappend` maxDepth_ s2, - maxSize_ = maxSize_ s1 `mappend` maxSize_ s2, - minTests_ = minTests_ s1 `mappend` minTests_ s2, - maxQuickCheckSize_ = maxQuickCheckSize_ s1 `mappend` maxQuickCheckSize_ s2 } - where constants' = TypeRel.toList (constants s1) ++ - TypeRel.toList (constants s2) - -- Overwrite variables if they're declared twice! - variables' = TypeRel.toList (variables s1 `combine` variables s2) - - renumber :: (forall a. Int -> f a -> f a) -> - Int -> [Some f] -> TypeRel f - renumber alter n = - TypeRel.fromList . - zipWith (\x -> mapSome (alter x)) [n..] - - alter :: Int -> Symbol -> Symbol - alter n x = x { index = n } - - combine :: TypeRel Variable -> TypeRel Variable -> TypeRel Variable - -- If a signature uses vars several times at the same type, - -- the declaration with the highest number of variables "wins" - -- and all others are discarded - combine = Map.unionWith max_ - where max_ vs1 vs2 - | some2 length vs1 > some2 length vs2 = vs1 - | otherwise = vs2 - -constantSig :: Typeable a => Constant a -> Sig -constantSig x = emptySig { constants = TypeRel.singleton x } - -variableSig :: forall a. Typeable a => [Variable a] -> Sig -variableSig x = emptySig { variables = TypeRel.fromList (map Some x) } - -totalSig :: forall a. Typeable a => Gen a -> Sig -totalSig g = emptySig { total = TypeMap.singleton g } - -partialSig :: forall a. Typeable a => Gen a -> Sig -partialSig g = emptySig { partial = TypeMap.singleton g } - -observerSig :: forall a. Typeable a => Observer a -> Sig -observerSig x = emptySig { observers = TypeMap.singleton x } - -typeSig :: Typeable a => a -> Sig -typeSig x = emptySig { witnesses = TypeMap.singleton (Witness x) } - -ordSig :: Typeable a => Observer a -> Sig -ordSig x = emptySig { ords = TypeMap.singleton x } - --- | If @withDepth n@ is in your signature, --- QuickSpec will consider terms of up to depth @n@ --- (the default is 3). -withDepth :: Int -> Sig -withDepth n = updateDepth n emptySig - --- | If @withSize n@ is in your signature, --- QuickSpec will consider terms of up to size @n@ --- (the default is 100). -withSize :: Int -> Sig -withSize n = updateSize n emptySig - --- | If @withTests n@ is in your signature, --- QuickSpec will run at least @n@ tests --- (the default is 500). -withTests :: Int -> Sig -withTests n = emptySig { minTests_ = First (Just n) } - --- | If @withQuickCheckSize n@ is in your signature, --- QuickSpec will generate test data of up to size @n@ --- (the default is 20). -withQuickCheckSize :: Int -> Sig -withQuickCheckSize n = emptySig { maxQuickCheckSize_ = First (Just n) } - --- | @sig \`without\` xs@ will remove the functions --- in @xs@ from the signature @sig@. --- Useful when you want to use `Test.QuickSpec.prelude` --- but exclude some functions. --- Example: @`prelude` (undefined :: A) \`without\` [\"head\", \"tail\"]@. -without :: Signature a => a -> [String] -> Sig -without sig xs = sig' { constants = f p (constants sig'), variables = f q (variables sig') } - where - sig' = signature sig - f p = TypeRel.fromList . filter p . TypeRel.toList - p (Some (Constant k)) = name (sym k) `notElem` xs - q (Some (Variable v)) = name (sym v) `notElem` xs - -undefinedSig :: forall a. Typeable a => String -> a -> Sig -undefinedSig x u = constantSig (Constant (Atom ((symbol x 0 u) { undef = True }) u)) - -primCon0 :: forall a. Typeable a => Int -> String -> a -> Sig -primCon0 n x f = constantSig (Constant (Atom (symbol x n f) f)) - `mappend` typeSig (undefined :: a) - -primCon1 :: forall a b. (Typeable a, Typeable b) => - Int -> String -> (a -> b) -> Sig -primCon1 n x f = primCon0 n x f - `mappend` typeSig (undefined :: a) - `mappend` typeSig (undefined :: b) - -primCon2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => - Int -> String -> (a -> b -> c) -> Sig -primCon2 n x f = primCon1 n x f - `mappend` typeSig (undefined :: b) - `mappend` typeSig (undefined :: c) - -primCon3 :: forall a b c d. (Typeable a, Typeable b, Typeable c, Typeable d) => - Int -> String -> (a -> b -> c -> d) -> Sig -primCon3 n x f = primCon2 n x f - `mappend` typeSig (undefined :: c) - `mappend` typeSig (undefined :: d) - -primCon4 :: forall a b c d e. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => - Int -> String -> (a -> b -> c -> d -> e) -> Sig -primCon4 n x f = primCon3 n x f - `mappend` typeSig (undefined :: d) - `mappend` typeSig (undefined :: e) - -primCon5 :: forall a b c d e f. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f) => - Int -> String -> (a -> b -> c -> d -> e -> f) -> Sig -primCon5 n x f = primCon4 n x f - `mappend` typeSig (undefined :: e) - `mappend` typeSig (undefined :: f) - --- | A constant. -blind0 :: forall a. Typeable a => String -> a -> Sig -blind0 = primCon0 0 --- | A unary function. -blind1 :: forall a b. (Typeable a, Typeable b) => - String -> (a -> b) -> Sig -blind1 = primCon1 1 --- | A binary function. -blind2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => - String -> (a -> b -> c) -> Sig -blind2 = primCon2 2 --- | A ternary function. -blind3 :: forall a b c d. (Typeable a, Typeable b, Typeable c, Typeable d) => - String -> (a -> b -> c -> d) -> Sig -blind3 = primCon3 3 --- | A function of arity 4. -blind4 :: forall a b c d e. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => - String -> (a -> b -> c -> d -> e) -> Sig -blind4 = primCon4 4 --- | A function of arity 5. -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 -blind5 = primCon5 5 - -ord :: (Ord a, Typeable a) => a -> Sig -ord x = ordSig (Observer (pgen (return id)) `observing` x) - -observing :: Observer a -> a -> Observer a -observing x _ = x - --- | 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. `Test.QuickSpec.prelude` are declared as background functions. -background :: Signature a => a -> Sig -background sig = - sig' { constants = TypeRel.mapValues (mapConstant silence1) (constants sig'), - variables = TypeRel.mapValues (mapVariable silence1) (variables sig') } - where sig' = signature sig - silence1 x = x { silent = True } - -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 = 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 = primVars1 n xs - `mappend` typeSig (undefined :: b) - `mappend` typeSig (undefined :: c) - --- | Similar to `vars`, but takes a generator as a parameter. --- --- @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 (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 (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 (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. --- --- For example, @vars [\"x\",\"y\",\"z\"] (undefined :: Int)@ --- defines three variables, @x@, @y@ and @z@, of type `Int`. -vars, vars0 :: forall a. (Arbitrary a, Typeable a) => [String] -> a -> Sig -vars xs _ = gvars xs (arbitrary :: Gen a) -vars0 = vars - -vars1 :: forall a b. (CoArbitrary a, Typeable a, Arbitrary b, Typeable b) => [String] -> (a -> b) -> Sig -vars1 xs _ = gvars1 xs (arbitrary :: Gen (a -> b)) - -vars2 :: forall a b c. (CoArbitrary a, Typeable a, CoArbitrary b, Typeable b, Arbitrary c, Typeable c) => [String] -> (a -> b -> c) -> Sig -vars2 xs _ = gvars2 xs (arbitrary :: Gen (a -> b -> c)) - -con, fun0 :: (Ord a, Typeable a) => String -> a -> Sig --- | A constant. The same as `fun0`. -con = fun0 --- | A constant. The same as `con`. -fun0 x f = blind0 x f - `mappend` ord f - --- | A unary function. -fun1 :: (Typeable a, - Typeable b, Ord b) => - String -> (a -> b) -> Sig -fun1 x f = blind1 x f - `mappend` ord (f undefined) - --- | A binary function. -fun2 :: (Typeable a, Typeable b, - Typeable c, Ord c) => - String -> (a -> b -> c) -> Sig -fun2 x f = blind2 x f - `mappend` ord (f undefined undefined) - --- | A ternary function. -fun3 :: (Typeable a, Typeable b, Typeable c, - Typeable d, Ord d) => - String -> (a -> b -> c -> d) -> Sig -fun3 x f = blind3 x f - `mappend` ord (f undefined undefined undefined) - --- | 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 -fun4 x f = blind4 x f - `mappend` ord (f undefined undefined undefined undefined) - --- | A function of five arguments. -fun5 :: (Typeable a, Typeable b, Typeable c, Typeable d, - Typeable e, Typeable f, Ord f) => - String -> (a -> b -> c -> d -> e -> f) -> Sig -fun5 x f = blind5 x f - `mappend` ord (f undefined undefined undefined undefined undefined) - --- | An observation function of arity 1. -observer1 :: (Typeable a, Typeable b, Ord b) => (a -> b) -> Sig -observer1 f = observerSig (Observer (pgen (return f))) - --- | An observation function of arity 2. -observer2 :: (Arbitrary a, Typeable a, Typeable b, Typeable c, Ord c) => - (a -> b -> c) -> Sig -observer2 f = observerSig (Observer (pgen (f <$> arbitrary))) - --- | 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 -observer3 f = observerSig (Observer (pgen (f <$> arbitrary <*> arbitrary))) - --- | 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 -observer4 f = observerSig (Observer (pgen (f <$> arbitrary <*> arbitrary <*> arbitrary))) - -testable :: Typeable a => Sig -> a -> Bool -testable sig x = - typeOf x `Map.member` observers sig || - typeOf x `Map.member` ords sig - --- Given a constant, find the types of its partial applications. -constantApplications :: forall a. Typeable a => Sig -> Constant a -> [Witness] -constantApplications sig (Constant (Atom {sym = sym })) = - map (findWitness sig) - (take (symbolArity sym + 1) - (iterate rightArrow (typeOf (undefined :: a)))) - --- Find the argument types of a constant. -constantArgs :: forall a. Typeable a => Sig -> Constant a -> [Witness] -constantArgs sig (Constant (Atom { sym = sym })) = - map (findWitness sig) - (take (symbolArity sym) - (unfoldr splitArrow (typeOf (undefined :: a)))) - --- Find the type of a saturated constant. -constantRes :: forall a. Typeable a => Sig -> Constant a -> Witness -constantRes sig (Constant (Atom { sym = sym })) = - findWitness sig - (iterate (snd . fromMaybe (ERROR msg) . splitArrow) - (typeOf (undefined :: a)) !! symbolArity sym) - where msg = "constantRes: type oversaturated" - --- The set of types returned by saturated constants. -saturatedTypes :: Sig -> [Witness] -saturatedTypes sig = - usort - [ constantRes sig k - | Some k <- TypeRel.toList (constants sig) ] - --- The set of types of which there is a non-variable term. -inhabitedTypes :: Sig -> [Witness] -inhabitedTypes sig = - usort . concat $ - [ constantApplications sig k - | Some k <- TypeRel.toList (constants sig) ] - --- The set of types that appear as arguments to functions. -argumentTypes :: Sig -> [Witness] -argumentTypes sig = - usort . concat $ - [ constantArgs sig k - | Some k <- TypeRel.toList (constants sig) ] - --- The set of types inhabited by variables. -variableTypes :: Sig -> [Witness] -variableTypes sig = - usort (map someWitness (TypeRel.toList (variables sig))) - --- Given a type, find a witness that it's a function. -witnessArrow :: Typeable a => Sig -> a -> Maybe (Witness, Witness) -witnessArrow sig x = do - (lhs, rhs) <- splitArrow (typeOf x) - liftM2 (,) (lookupWitness sig lhs) (lookupWitness sig rhs) - --- lhsWitnesses sig x is the set of witnessed function types that --- might accept x as a parameter. There is no guarantee that --- any particular type is inhabited. -lhsWitnesses :: Typeable a => Sig -> a -> [Witness] -lhsWitnesses sig x = - [ lhs - | Some (Witness w) <- TypeMap.toList (witnesses sig), - Just (lhs, rhs) <- [witnessArrow sig w], - witnessType rhs == typeOf x ] - -findWitness :: Sig -> TypeRep -> Witness -findWitness sig ty = fromMaybe (ERROR "missing type") (lookupWitness sig ty) - -lookupWitness :: Sig -> TypeRep -> Maybe Witness -lookupWitness sig ty = Map.lookup ty (witnesses sig) - -disambiguate :: Sig -> [Symbol] -> Symbol -> Symbol -disambiguate sig ss = - \x -> - fromMaybe (ERROR "variable not found") - (find (\y -> index x == index y) - (aux [] (nub ss))) - where - aux used [] = [] - aux used (x:xs) = x { name = next }:aux (next:used) xs - where next = head (filter (`notElem` used) candidates) - candidates - | null wellTypedNames = ERROR "null allVars" - | otherwise = concat [ map (++ suffix) wellTypedNames | suffix <- suffixes ] - allVars = - map (some (sym . unVariable)) - (TypeRel.toList (variables sig)) ++ - ss - wellTypedNames = - [ name v | v <- allVars, symbolType v == symbolType x ] - suffixes = - concat ([sequence (replicate n ['a'..'z']) | n <- [0..]]) - -constantSymbols, variableSymbols, symbols :: Sig -> [Symbol] -constantSymbols sig = - map (some (sym . unConstant)) (TypeRel.toList (constants sig)) -variableSymbols sig = - map (some (sym . unVariable)) (TypeRel.toList (variables sig)) -symbols sig = constantSymbols sig ++ variableSymbols sig diff --git a/src/Test/QuickSpec/Term.hs b/src/Test/QuickSpec/Term.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Term.hs +++ /dev/null @@ -1,210 +0,0 @@ --- | Terms and evaluation. - -{-# LANGUAGE CPP, RankNTypes, ExistentialQuantification, DeriveFunctor, DeriveDataTypeable #-} -module Test.QuickSpec.Term where - -#include "errors.h" -import Test.QuickSpec.Utils.Typeable -import Test.QuickCheck -import Test.QuickCheck.Gen -import Test.QuickCheck.Gen.Unsafe -import Data.Function -import Data.Ord -import Data.Char -import Data.List -import Test.QuickSpec.Utils - -data Symbol = Symbol { - index :: Int, - name :: String, - symbolArity :: Int, - silent :: Bool, - undef :: Bool, - symbolType :: TypeRep } - -symbol :: Typeable a => String -> Int -> a -> Symbol -symbol x arity v = Symbol 0 x arity False False (typeOf v) - -instance Show Symbol where - show = showOp . name - -instance Eq Symbol where - (==) = (==) `on` index - -instance Ord Symbol where - compare = comparing index - -data Term = - Var Symbol - | Const Symbol - | App Term Term deriving Eq - -infixl 5 `App` - -instance Ord Term where - compare = comparing stamp - where - stamp t = (depth t, size 0 t, -occur t, body t) - - occur t = length (usort (vars t)) - - body (Var x) = Left (Left x) - body (Const x) = Left (Right x) - body (App f x) = Right (f, x) - -instance Show Term where - showsPrec p t = showString (showTerm p (hideImplicit t)) - where - brack s = "(" ++ s ++ ")" - parenFun p s | p < 2 = s - | otherwise = brack s - parenOp p s | p < 1 = s - | otherwise = brack s - - showTerm p (Var v) = show v - showTerm p (Const x) = show x - showTerm p (Const op `App` x) | isOp (name op) = - brack (showTerm 1 x ++ name op) - showTerm p (Const op `App` x `App` y) | isOp (name op) = - parenOp p (showTerm 1 x ++ name op ++ showTerm 1 y) - - showTerm p (f `App` x) = - parenFun p (showTerm 1 f ++ " " ++ showTerm 2 x) - - hideImplicit (f `App` x) - | isImplicit x = f - | otherwise = hideImplicit f `App` hideImplicit x - hideImplicit t = t - - isImplicit (Var v) | "_" `isPrefixOf` name v = True - isImplicit _ = False - -showOp :: String -> String -showOp op | isOp op = "(" ++ op ++ ")" - | otherwise = op - -isOp :: String -> Bool -isOp "[]" = False -isOp xs = not (all isIdent xs) - where isIdent x = isAlphaNum x || x == '\'' || x == '_' - -isUndefined :: Term -> Bool -isUndefined (Const Symbol { undef = True }) = True -isUndefined _ = False - -symbols :: Term -> [Symbol] -symbols t = symbols' t [] - where symbols' (Var x) = (x:) - symbols' (Const x) = (x:) - symbols' (App f x) = symbols' f . symbols' x - -depth :: Term -> Int -depth (App f x) = depth f `max` (1 + depth x) -depth _ = 1 - -size :: Int -> Term -> Int -size v (App f x) = size v f + size v x -size v (Var _) = v -size v (Const _) = 1 - -holes :: Term -> [(Symbol, Int)] -holes t = holes' 0 t [] - where holes' d (Var x) = ((x, d):) - holes' d Const{} = id - holes' d (App f x) = holes' d f . holes' (d+1) x - -functor :: Term -> Symbol -functor (Var x) = x -functor (Const x) = x -functor (App f x) = functor f - -args :: Term -> [Term] -args = reverse . args' - where args' Var{} = [] - args' Const{} = [] - args' (App f x) = x:args' f - -funs :: Term -> [Symbol] -funs t = aux t [] - where aux (Const x) = (x:) - aux Var{} = id - aux (App f x) = aux f . aux x - -vars :: Term -> [Symbol] -vars t = aux t [] - where aux (Var x) = (x:) - aux (App f x) = aux f . aux x - aux Const{} = id - -mapVars :: (Symbol -> Symbol) -> Term -> Term -mapVars f (Var x) = Var (f x) -mapVars f (Const x) = Const x -mapVars f (App t u) = App (mapVars f t) (mapVars f u) - -mapConsts :: (Symbol -> Symbol) -> Term -> Term -mapConsts f (Var x) = Var x -mapConsts f (Const x) = Const (f x) -mapConsts f (App t u) = App (mapConsts f t) (mapConsts f u) - -data Expr a = Expr { - term :: Term, - arity :: {-# UNPACK #-} !Int, - eval :: Valuation -> a } - deriving Typeable - -instance Eq (Expr a) where - (==) = (==) `on` term - -instance Ord (Expr a) where - compare = comparing term - -instance Show (Expr a) where - show = show . term - -data Atom a = Atom { - sym :: Symbol, - value :: a } deriving Functor - -data PGen a = PGen { - totalGen :: Gen a, - partialGen :: Gen a - } - -pgen :: Gen a -> PGen a -pgen g = PGen g g - -type Strategy = forall a. Symbol -> PGen a -> Gen a - -instance Functor PGen where - fmap f (PGen tot par) = PGen (fmap f tot) (fmap f par) - -newtype Variable a = Variable { unVariable :: Atom (PGen a) } deriving Functor -newtype Constant a = Constant { unConstant :: Atom a } deriving Functor - -mapVariable :: (Symbol -> Symbol) -> Variable a -> Variable a -mapVariable f (Variable v) = Variable v { sym = f (sym v) } - -mapConstant :: (Symbol -> Symbol) -> Constant a -> Constant a -mapConstant f (Constant v) = Constant v { sym = f (sym v) } - --- Generate a random variable valuation -newtype Valuation = Valuation { unValuation :: forall a. Variable a -> a } - -promoteVal :: (forall a. Variable a -> Gen a) -> Gen Valuation -promoteVal g = do - Capture eval <- capture - return (Valuation (eval . g)) - -valuation :: Strategy -> Gen Valuation -valuation strat = promoteVal (\(Variable x) -> index (sym x) `variant` strat (sym x) (value x)) - -var :: Variable a -> Expr a -var v@(Variable (Atom x _)) = Expr (Var x) (symbolArity x) (\env -> unValuation env v) - -con :: Constant a -> Expr a -con (Constant (Atom x v)) = Expr (Const x) (symbolArity x) (const v) - -app :: Expr (a -> b) -> Expr a -> Expr b -app (Expr t a f) (Expr u _ x) - | a == 0 = ERROR "oversaturated function" - | otherwise = Expr (App t u) (a - 1) (\env -> f env (x env)) diff --git a/src/Test/QuickSpec/TestTotality.hs b/src/Test/QuickSpec/TestTotality.hs deleted file mode 100644 --- a/src/Test/QuickSpec/TestTotality.hs +++ /dev/null @@ -1,76 +0,0 @@ --- | Test whether functions are total. --- Used by HipSpec. - -{-# LANGUAGE CPP, TupleSections #-} -module Test.QuickSpec.TestTotality where - -#include "errors.h" -import Prelude hiding (lookup) -import Test.QuickSpec.Reasoning.PartialEquationalReasoning hiding (Variable, total, partial) -import qualified Test.QuickSpec.Reasoning.PartialEquationalReasoning as PEQ -import Test.QuickSpec.Utils.TypeRel -import qualified Test.QuickSpec.Utils.TypeMap as TypeMap -import Test.QuickSpec.Utils.Typed -import Test.QuickSpec.Utils.Typeable -import Test.QuickSpec.Utils -import Test.QuickSpec.Signature -import Test.QuickSpec.Term hiding (symbols) -import Test.QuickCheck -import Test.QuickCheck.Gen -import Test.QuickCheck.Random -import System.Random -import Control.Monad -import Data.List hiding (lookup) -import Data.Maybe -import Data.Ord -import qualified Data.Map as Map - -testTotality :: Sig -> IO [(Symbol, Totality)] -testTotality sig = do - consts <- mapM (some constTotality) (toList (constants sig)) - let vars = map (some varTotality) (toList (variables sig)) - return (sortBy (comparing fst) (consts ++ vars)) - where - constTotality :: Typeable a => Constant a -> IO (Symbol, Totality) - constTotality (Constant x) = fmap (sym x,) (isTotal (symbolArity (sym x)) (value x)) - - isTotal :: Typeable a => Int -> a -> IO Totality - isTotal arity x = do - b <- always sig (testTotal x []) - if not b then return Partial - else fmap Total . flip filterM [0..arity-1] $ \i -> always sig (testTotal x [i]) - - testTotal :: Typeable a => a -> [Int] -> Gen Bool - testTotal f args = - case witnessArrow sig f of - Nothing -> - case observe undefined sig of - Observer obs -> - fmap (isJust . spoony) (liftM2 ($) (totalGen obs) (return f)) - Just (Some (Witness arg), Some (Witness res)) -> do - if 0 `elem` args && typeOf res `Map.notMember` partial sig - then return False - else do - x <- TypeMap.lookup __ arg - (if 0 `elem` args then partial sig else total sig) - case cast f `asTypeOf` Just (\x -> (x `asTypeOf` arg) `seq` (undefined `asTypeOf` res)) of - Just g -> testTotal (g x) (map pred args) - - varTotality :: Variable a -> (Symbol, Totality) - varTotality (Variable x) = (sym x, PEQ.Variable) - -testEquation :: Typeable a => Sig -> Expr a -> Expr a -> Symbol -> IO Bool -testEquation sig e1 e2 s = - case observe undefined sig of - Observer obs -> - always sig $ do - let strat s' = if s == s' then partialGen else totalGen - obs' <- partialGen obs - v <- valuation strat - return (spoony (obs' (eval e1 v)) == spoony (obs' (eval e2 v))) - -always :: Sig -> Gen Bool -> IO Bool -always sig x = do - gens <- replicateM 100 newQCGen - let sizes = cycle [0,2..maxQuickCheckSize sig] - return (and [unGen x g n | (g, n) <- zip gens sizes]) diff --git a/src/Test/QuickSpec/TestTree.hs b/src/Test/QuickSpec/TestTree.hs deleted file mode 100644 --- a/src/Test/QuickSpec/TestTree.hs +++ /dev/null @@ -1,112 +0,0 @@ --- | A data structure to represent refining a set of terms into --- equivalence classes by testing. - -{-# LANGUAGE CPP #-} -module Test.QuickSpec.TestTree(TestTree, terms, union, test, - TestResults, cutOff, numTests, numResults, - classes, reps, discrete) where - -#include "errors.h" -import Data.List(sort) -import Test.QuickSpec.Utils -import Control.Exception(assert) - --- Invariant: the children of a TestTree are sorted according to the --- parent's test. We exploit this in defining merge. --- --- A TestTree is always infinite, and branches t is always a --- refinement of t (it may be trivial, so that length (branches t) == 1). --- As a special case, a TestTree may be Nil, but Nil may not appear in --- the branches of a TestTree. -data TestTree a = Nil | NonNil (TestTree' a) -data TestTree' a = Tree { rep :: a, rest :: [a], branches :: [TestTree' a] } - --- Precondition: bs must be sorted according to the TestCase. -tree :: Ord r => [a] -> (a -> r) -> [TestTree' a] -> TestTree' a -tree [] _ _ = ERROR "empty equivalence class" -tree (x:xs) eval bs = - assert (isSortedBy (eval . rep) bs) $ - Tree { rep = x, rest = xs, branches = bs } - -terms :: TestTree a -> [a] -terms Nil = [] -terms (NonNil t) = terms' t - -terms' :: TestTree' a -> [a] -terms' Tree{rep = x, rest = xs} = x:xs - --- Precondition: the sequence of test cases given must be --- that used to generate the two TestTrees. -union :: Ord r => [a -> r] -> TestTree a -> TestTree a -> TestTree a -union _ Nil t = t -union _ t Nil = t -union evals (NonNil t1) (NonNil t2) = NonNil (union' evals t1 t2) - -union' :: Ord r => [a -> r] -> TestTree' a -> TestTree' a -> TestTree' a -union' (eval:evals) t1 t2 = - tree (terms' t1 ++ terms' t2) eval - (merge (union' evals) (eval . rep) (branches t1) (branches t2)) - -test :: Ord r => [a -> r] -> [a] -> TestTree a -test _ [] = Nil -test tcs xs = NonNil (test' tcs xs) - -test' :: Ord r => [a -> r] -> [a] -> TestTree' a -test' [] _ = - error "Test.QuickSpec.TestTree.test': ran out of test cases" -test' (tc:tcs) [] = - error "Test.QuickSpec.TestTree.test': found an empty equivalence class" -test' (tc:tcs) xs@[_] = tree xs tc [test' tcs xs] -test' (tc:tcs) xs = tree xs tc (map (test' tcs) bs) - where bs = partitionBy tc xs - --- A TestTree with finite depth, represented as a TestTree where some --- nodes have no branches. Since this breaks one of the TestTree --- invariants we use a different type. -newtype TestResults a = Results (TestTree a) - -discrete :: Ord a => [a] -> TestResults a -discrete xs = - case sort xs of - [] -> Results Nil - (y:ys) -> - Results (NonNil (Tree y ys (map singleton (y:ys)))) - where singleton x = Tree x [] [] - -cutOff :: Int -> Int -> TestTree a -> TestResults a -cutOff _ _ Nil = Results Nil -cutOff m n (NonNil t) = Results (NonNil (aux m t)) - where aux _ t@Tree{rest = []} = t { branches = [] } - aux 0 t = aux' False n n t - aux m t = t { branches = map (aux (m-1)) (branches t) } - -- Exponential backoff if we carry on refining a class - aux' _ _ _ t@Tree{rest = []} = t { branches = [] } - aux' True 0 n t = t { branches = map (aux' False (n*2-1) (n*2)) (branches t) } - aux' False 0 n t = t { branches = [] } - aux' x m n t@Tree{branches = [t']} = t { branches = [aux' x (m-1) n t'] } - aux' _ m n t = t { branches = map (aux' True (m-1) n) (branches t) } - -numTests :: TestResults a -> Int -numTests (Results Nil) = 0 -numTests (Results (NonNil t)) = aux t - where aux Tree{branches = []} = 0 - aux Tree{branches = bs} = 1 + maximum (map aux bs) - -numResults :: TestResults a -> Int -numResults (Results Nil) = 0 -numResults (Results (NonNil t)) = aux t - where aux Tree{rest = []} = 0 - aux Tree{rest = xs, branches = ts} = - 1 + length xs + sum (map aux ts) - -classes :: Ord a => TestResults a -> [[a]] -classes = sort . map sort . unsortedClasses - -unsortedClasses :: TestResults a -> [[a]] -unsortedClasses (Results Nil) = [] -unsortedClasses (Results (NonNil t)) = aux t - where aux Tree{rep = x, rest = xs, branches = []} = [x:xs] - aux Tree{branches = bs} = concatMap aux bs - -reps :: Ord a => TestResults a -> [a] -reps = map head . classes diff --git a/src/Test/QuickSpec/Utils.hs b/src/Test/QuickSpec/Utils.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Utils.hs +++ /dev/null @@ -1,50 +0,0 @@ --- | Miscellaneous utility functions. - -module Test.QuickSpec.Utils where - -import Control.Arrow((&&&)) -import Data.List(groupBy, sortBy, group, sort) -import Data.Ord(comparing) -import System.IO -import Control.Exception -import Control.Spoon - -repeatM :: Monad m => m a -> m [a] -repeatM = sequence . repeat - -partitionBy :: Ord b => (a -> b) -> [a] -> [[a]] -partitionBy value = map (map fst) . groupBy (\x y -> snd x == snd y) . sortBy (comparing snd) . map (id &&& value) - -isSorted :: Ord a => [a] -> Bool -isSorted xs = and (zipWith (<=) xs (tail xs)) - -isSortedBy :: Ord b => (a -> b) -> [a] -> Bool -isSortedBy f xs = isSorted (map f xs) - -usort :: Ord a => [a] -> [a] -usort = map head . group . sort - -merge :: Ord b => (a -> a -> a) -> (a -> b) -> [a] -> [a] -> [a] -merge f c = aux - where aux [] ys = ys - aux xs [] = xs - aux (x:xs) (y:ys) = - case comparing c x y of - LT -> x:aux xs (y:ys) - GT -> y:aux (x:xs) ys - EQ -> f x y:aux xs ys - -orElse :: Ordering -> Ordering -> Ordering -EQ `orElse` x = x -x `orElse` _ = x - -unbuffered :: IO a -> IO a -unbuffered x = do - buf <- hGetBuffering stdout - bracket_ - (hSetBuffering stdout NoBuffering) - (hSetBuffering stdout buf) - x - -spoony :: Eq a => a -> Maybe a -spoony x = teaspoon ((x == x) `seq` x) diff --git a/src/Test/QuickSpec/Utils/MemoValuation.hs b/src/Test/QuickSpec/Utils/MemoValuation.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Utils/MemoValuation.hs +++ /dev/null @@ -1,22 +0,0 @@ --- | Memoise the variable valuation function for terms. --- In its own module because it's packed full of dangerous features! - -{-# LANGUAGE Rank2Types #-} -module Test.QuickSpec.Utils.MemoValuation where - -import Test.QuickSpec.Term -import Test.QuickSpec.Signature -import Data.Array hiding (index) -import Data.Array.Base(unsafeAt) -import Unsafe.Coerce -import GHC.Prim -import Test.QuickSpec.Utils.Typed -import Test.QuickSpec.Utils.TypeRel - -memoValuation :: Sig -> Valuation -> Valuation -memoValuation sig (Valuation f) = Valuation (unsafeCoerce . unsafeAt arr . index . sym . unVariable) - where arr :: Array Int Any - arr = array (0, maximum (0:map (some (index . sym . unVariable)) vars)) - [(index (sym (unVariable v)), unsafeCoerce (f v)) - | Some v <- vars ] - vars = toList (variables sig) diff --git a/src/Test/QuickSpec/Utils/TypeMap.hs b/src/Test/QuickSpec/Utils/TypeMap.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Utils/TypeMap.hs +++ /dev/null @@ -1,38 +0,0 @@ --- | A map from types to values. --- @'TypeMap' f@ maps each type @a@ to a value of type @f a@. - -{-# LANGUAGE Rank2Types, TypeOperators #-} -module Test.QuickSpec.Utils.TypeMap where - -import qualified Data.Map as Map -import Data.Map(Map) -import Test.QuickSpec.Utils.Typed -import Test.QuickSpec.Utils.Typeable - -type TypeMap f = Map TypeRep (Some f) - -empty :: TypeMap f -empty = fromList [] - -singleton :: Typeable a => f a -> TypeMap f -singleton x = fromList [Some x] - -fromList :: [Some f] -> TypeMap f -fromList xs = Map.fromList [ (someType x, x) | x <- xs ] - -toList :: TypeMap f -> [Some f] -toList = Map.elems - -lookup :: Typeable a => f a -> a -> TypeMap f -> f a -lookup def x m = - case Map.lookup (typeOf x) m of - Nothing -> def - Just (Some y) -> - case gcast y of - Just z -> z - -mapValues :: (forall a. Typeable a => f a -> g a) -> TypeMap f -> TypeMap g -mapValues f = fmap (mapSome f) - -mapValues2 :: (forall a. Typeable a => f (g a) -> h (i a)) -> TypeMap (f `O` g) -> TypeMap (h `O` i) -mapValues2 f = fmap (mapSome (O . f . unO)) diff --git a/src/Test/QuickSpec/Utils/TypeRel.hs b/src/Test/QuickSpec/Utils/TypeRel.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Utils/TypeRel.hs +++ /dev/null @@ -1,47 +0,0 @@ --- | A relation between types and values. --- @'TypeRel' f@ relates each type @a@ to a set of values --- of type @f a@. - -{-# LANGUAGE CPP, Rank2Types, TypeOperators #-} -module Test.QuickSpec.Utils.TypeRel where - -#include "errors.h" -import qualified Test.QuickSpec.Utils.TypeMap as TypeMap -import Test.QuickSpec.Utils.TypeMap(TypeMap) -import Test.QuickSpec.Utils.Typed -import Test.QuickSpec.Utils.Typeable -import Data.Maybe -import Test.QuickSpec.Utils - -type TypeRel f = TypeMap (List `O` f) - -empty :: TypeRel f -empty = TypeMap.empty - -singleton :: Typeable a => f a -> TypeRel f -singleton x = TypeMap.singleton (O [x]) - -fromList :: [Some f] -> TypeRel f -fromList = TypeMap.fromList . classify - -toList :: TypeRel f -> [Some f] -toList = concatMap disperse . TypeMap.toList - -lookup :: Typeable a => a -> TypeRel f -> [f a] -lookup x m = unO (TypeMap.lookup (O []) x m) - -mapValues :: (forall a. Typeable a => f a -> g a) -> TypeRel f -> TypeRel g -mapValues f = TypeMap.mapValues2 (map f) - -gather :: [Some f] -> Some (List `O` f) -gather [] = ERROR "empty list" -gather (Some x:xs) = Some (O (x:map gcast' xs)) - where gcast' (Some y) = - fromMaybe (ERROR msg) (gcast y) - msg = "heterogeneous list" - -disperse :: Some (List `O` f) -> [Some f] -disperse (Some (O xs)) = map Some xs - -classify :: [Some f] -> [Some (List `O` f)] -classify xs = map gather (partitionBy someType xs) diff --git a/src/Test/QuickSpec/Utils/Typeable.hs b/src/Test/QuickSpec/Utils/Typeable.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Utils/Typeable.hs +++ /dev/null @@ -1,51 +0,0 @@ -{-# LANGUAGE NoMonomorphismRestriction, CPP #-} - --- | A wrapper around 'Data.Typeable', to work around: --- --- (1) The lack of an 'Ord' instance in older GHCs, --- --- (2) bug #5962 in new GHCs. - -module Test.QuickSpec.Utils.Typeable(TypeRep, T.Typeable, T.Typeable1, T.Typeable2, - typeOf, typeOf1, cast, gcast, - mkTyConApp, typeRepTyCon, splitTyConApp, - mkFunTy, unTypeRep) where - -#if __GLASGOW_HASKELL__ >= 702 -#define NEW_TYPEABLE -#endif - -import qualified Data.Typeable as T -import Data.Ord -#ifndef NEW_TYPEABLE -import System.IO.Unsafe -#endif - -newtype TypeRep = TypeRep { unTypeRep :: T.TypeRep } - -instance Eq TypeRep where - ty == ty' = - unTypeRep ty == unTypeRep ty' || - ty `compare` ty' == EQ - -#ifdef NEW_TYPEABLE -instance Ord TypeRep where - compare = comparing splitTyConApp -#else -instance Ord TypeRep where - compare = comparing (unsafePerformIO . T.typeRepKey . unTypeRep) -#endif - -instance Show TypeRep where - showsPrec p = showsPrec p . unTypeRep - -typeOf = TypeRep . T.typeOf -typeOf1 = TypeRep . T.typeOf1 -cast = T.cast -gcast = T.gcast - -mkTyConApp f xs = TypeRep (T.mkTyConApp f (map unTypeRep xs)) -typeRepTyCon = T.typeRepTyCon . unTypeRep -splitTyConApp ty = (c, map TypeRep tys) - where (c, tys) = T.splitTyConApp (unTypeRep ty) -mkFunTy lhs rhs = TypeRep (T.mkFunTy (unTypeRep lhs) (unTypeRep rhs)) diff --git a/src/Test/QuickSpec/Utils/Typed.hs b/src/Test/QuickSpec/Utils/Typed.hs deleted file mode 100644 --- a/src/Test/QuickSpec/Utils/Typed.hs +++ /dev/null @@ -1,91 +0,0 @@ --- | Functions for working with existentially-quantified types --- and similar. - -{-# LANGUAGE CPP, Rank2Types, ExistentialQuantification, TypeOperators, TypeSynonymInstances, FlexibleInstances, PatternGuards #-} -module Test.QuickSpec.Utils.Typed where - -#include "errors.h" -import Control.Monad -import Test.QuickSpec.Utils.Typeable -import Data.Ord -import Data.Function -import Data.Maybe -import Data.Typeable (TyCon) -import Test.QuickSpec.Utils (usort) - -data Some f = forall a. Typeable a => Some (f a) - -newtype O f g a = O { unO :: f (g a) } -type List = [] - -type Several f = Some (List `O` f) - -newtype Witnessed a = Witness { witness :: a } -type Witness = Some Witnessed - --- No Typeable (Witnessed a) instance to save accidentally looking up --- Witnessed a instead of a in a TypeMap - -instance Eq Witness where - (==) = (==) `on` witnessType - -instance Ord Witness where - compare = comparing witnessType - -instance Show Witness where - show = show . witnessType - -witnessType :: Witness -> TypeRep -witnessType = some (typeOf . witness) - -data Tagged a = Tagged { tag :: Witness, erase :: a } - -tagged :: Typeable a => (f a -> b) -> f a -> Tagged b -tagged f x = Tagged (Some (Witness (witness x))) (f x) - where witness :: f a -> a - witness = undefined - -some :: (forall a. Typeable a => f a -> b) -> Some f -> b -some f (Some x) = f x - -several :: (forall a. Typeable a => [f a] -> b) -> Several f -> b -several f (Some (O xs)) = f xs - -some2 :: (forall a. Typeable a => f (g a) -> b) -> Some (f `O` g) -> b -some2 f = some (f . unO) - -mapSome :: (forall a. Typeable a => f a -> g a) -> Some f -> Some g -mapSome f (Some x) = Some (f x) - -mapSome2 :: (forall a. Typeable a => f (g a) -> h (i a)) -> Some (f `O` g) -> Some (h `O` i) -mapSome2 f = mapSome (O . f . unO) - -mapSomeM :: Monad m => (forall a. Typeable a => f a -> m (g a)) -> Some f -> m (Some g) -mapSomeM f (Some x) = liftM Some (f x) - -someType :: Some f -> TypeRep -someType (Some x) = typeOf (witness x) - where witness :: f a -> a - witness = undefined - -someWitness :: Some f -> Witness -someWitness = mapSome (const undefined) - -splitArrow :: TypeRep -> Maybe (TypeRep, TypeRep) -splitArrow ty = - case splitTyConApp ty of - (c, [lhs, rhs]) | c == arr -> Just (lhs, rhs) - _ -> Nothing - where (arr, _) = splitTyConApp (typeOf (undefined :: Int -> Int)) - -rightArrow :: TypeRep -> TypeRep -rightArrow ty = snd (fromMaybe (ERROR msg) (splitArrow ty)) - where - msg = "type oversaturated" - -typeRepTyCons :: TypeRep -> [TyCon] -typeRepTyCons = usort . go where - go ty - | Just (t1,t2) <- splitArrow ty = go t1 ++ go t2 - | (ty_con,ts) <- splitTyConApp ty = ty_con:concatMap go ts - diff --git a/src/Test/QuickSpec/errors.h b/src/Test/QuickSpec/errors.h deleted file mode 100644 --- a/src/Test/QuickSpec/errors.h +++ /dev/null @@ -1,3 +0,0 @@ --- Inspired by Agda's undefined.h -#define __ (ERROR "no error message given") -#define ERROR (\msg -> error ("Error at file " ++ __FILE__ ++ ", line " ++ show __LINE__ ++ ": " ++ msg))