packages feed

quickspec 0.9.6 → 2

raw patch · 65 files changed

+3988/−3242 lines, 65 filesdep +constraintsdep +data-lens-lightdep +dlistdep −arraydep −ghc-primdep −spoondep ~QuickCheckdep ~base

Dependencies added: constraints, data-lens-light, dlist, reflection, template-haskell, twee-lib, uglymemo

Dependencies removed: array, ghc-prim, spoon

Dependency ranges changed: QuickCheck, base

Files

LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2009-2014, Nick Smallbone+Copyright (c) 2009-2018, Nick Smallbone  All rights reserved.
− README.asciidoc 
@@ -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.
+ README.md view
@@ -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).
examples/Arith.hs view
@@ -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) ]
− examples/Arrays.hs 
@@ -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))
examples/Bools.hs view
@@ -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 "&&" (&&) ]
examples/Composition.hs view
@@ -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) ]
+ examples/Geometry.hs view
@@ -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]
− examples/Heaps.hs 
@@ -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))
+ examples/HugeLists.hs view
@@ -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]) ]
+ examples/IntSet.hs view
@@ -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 ]
+ examples/ListMonad.hs view
@@ -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]) ]
examples/Lists.hs view
@@ -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) ] ]
+ examples/Octonions.hs view
@@ -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)]
+ examples/Parsing.hs view
@@ -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 ]+
examples/PrettyPrinting.hs view
@@ -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)]
+ examples/PrettyPrintingModel.hs view
@@ -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 "<>" (<>) ]
+ examples/Regex.hs view
@@ -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) ]
+ examples/Sorted.hs view
@@ -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) ]
− examples/TinyWM.hs 
@@ -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
+ examples/Zip.hs view
@@ -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) ]
quickspec.cabal view
@@ -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+  @<https://github.com/nick8325/quickspec/tree/master/examples examples>@+  directory, for example at+  @<https://github.com/nick8325/quickspec/tree/master/examples/Lists.hs Lists.hs>@,+  @<https://github.com/nick8325/quickspec/tree/master/examples/IntSet.hs IntSet.hs>@, or+  @<https://github.com/nick8325/quickspec/tree/master/examples/Parsing.hs Parsing.hs>@.+  To read about how+  QuickSpec works, see our paper,+  <http://www.cse.chalmers.se/~nicsma/papers/quickspec2.pdf Quick specifications for the busy programmer>.  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
+ src/QuickSpec.hs view
@@ -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 @<https://github.com/nick8325/quickspec/tree/master/examples examples>@+-- directory contains many examples. Here are some interesting ones:+--+-- * @<https://github.com/nick8325/quickspec/tree/master/examples/Arith.hs Arith.hs>@: a simple arithmetic example. Demonstrates basic use of QuickSpec.+-- * @<https://github.com/nick8325/quickspec/tree/master/examples/Lists.hs Lists.hs>@: list functions. Demonstrates testing polymorphic functions.+-- * @<https://github.com/nick8325/quickspec/tree/master/examples/Sorted.hs Sorted.hs>@: sorting. Demonstrates finding conditional equations.+-- * @<https://github.com/nick8325/quickspec/tree/master/examples/IntSet.hs IntSet.hs>@: a few functions from "Data.IntSet". Demonstrates testing user-defined datatypes and finding conditional equations.+-- * @<https://github.com/nick8325/quickspec/tree/master/examples/PrettyPrinting.hs PrettyPrinting.hs>@: pretty printing combinators. Demonstrates testing user-defined datatypes and using observational equality.+-- * @<https://github.com/nick8325/quickspec/tree/master/examples/Parsing.hs Parsing.hs>@: parser combinators. Demonstrates testing polymorphic datatypes and using observational equality.+--+-- You can also find some larger case studies in our paper,+-- <http://www.cse.chalmers.se/~nicsma/papers/quickspec2.pdf Quick+-- specifications for the busy programmer>.++{-# 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))
+ src/QuickSpec/Explore.hs view
@@ -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
+ src/QuickSpec/Explore/Conditionals.hs view
@@ -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
+ src/QuickSpec/Explore/PartialApplication.hs view
@@ -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))))
+ src/QuickSpec/Explore/Polymorphic.hs view
@@ -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]
+ src/QuickSpec/Explore/Schemas.hs view
@@ -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
+ src/QuickSpec/Explore/Terms.hs view
@@ -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
+ src/QuickSpec/Haskell.hs view
@@ -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 @<https://github.com/nick8325/quickspec/tree/master/examples/PrettyPrinting.hs PrettyPrinting.hs>@.+--+-- 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
+ src/QuickSpec/Haskell/Resolve.hs view
@@ -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)
+ src/QuickSpec/Prop.hs view
@@ -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) [])
+ src/QuickSpec/Pruning.hs view
@@ -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)+
+ src/QuickSpec/Pruning/Background.hs view
@@ -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)
+ src/QuickSpec/Pruning/Twee.hs view
@@ -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))
+ src/QuickSpec/Pruning/Types.hs view
@@ -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
+ src/QuickSpec/Pruning/UntypedTwee.hs view
@@ -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"
+ src/QuickSpec/Term.hs view
@@ -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
+ src/QuickSpec/Terminal.hs view
@@ -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)
+ src/QuickSpec/Testing.hs view
@@ -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)
+ src/QuickSpec/Testing/DecisionTree.hs view
@@ -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)
+ src/QuickSpec/Testing/QuickCheck.hs view
@@ -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
+ src/QuickSpec/Type.hs view
@@ -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)
+ src/QuickSpec/Utils.hs view
@@ -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
− src/Test/QuickSpec.hs 
@@ -1,90 +0,0 @@--- | The main QuickSpec module.------ Look at the introduction (<https://github.com/nick8325/quickspec/blob/master/README.asciidoc>),--- read the examples (<http://github.com/nick8325/quickspec/tree/master/examples>),--- or read the paper (<http://www.cse.chalmers.se/~nicsma/quickspec.pdf>)--- before venturing in here.--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
− src/Test/QuickSpec/Approximate.hs 
@@ -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
− src/Test/QuickSpec/Equation.hs 
@@ -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]
− src/Test/QuickSpec/Generate.hs 
@@ -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
− src/Test/QuickSpec/Main.hs 
@@ -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 ""
− src/Test/QuickSpec/Prelude.hs 
@@ -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 ]
− src/Test/QuickSpec/Reasoning/CongruenceClosure.hs 
@@ -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
− src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs 
@@ -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)
− src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs 
@@ -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))
− src/Test/QuickSpec/Reasoning/UnionFind.hs 
@@ -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')
− src/Test/QuickSpec/Signature.hs 
@@ -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
− src/Test/QuickSpec/Term.hs 
@@ -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))
− src/Test/QuickSpec/TestTotality.hs 
@@ -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])
− src/Test/QuickSpec/TestTree.hs 
@@ -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
− src/Test/QuickSpec/Utils.hs 
@@ -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)
− src/Test/QuickSpec/Utils/MemoValuation.hs 
@@ -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)
− src/Test/QuickSpec/Utils/TypeMap.hs 
@@ -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))
− src/Test/QuickSpec/Utils/TypeRel.hs 
@@ -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)
− src/Test/QuickSpec/Utils/Typeable.hs 
@@ -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))
− src/Test/QuickSpec/Utils/Typed.hs 
@@ -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-
− src/Test/QuickSpec/errors.h 
@@ -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))