packages feed

quickspec (empty) → 0.9

raw patch · 28 files changed

+2339/−0 lines, 28 filesdep +QuickCheckdep +arraydep +basesetup-changed

Dependencies added: QuickCheck, array, base, containers, ghc-prim, mtl, random, spoon, transformers

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2009-2012, Nick Smallbone++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Nick Smallbone nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README view
@@ -0,0 +1,1 @@+cabal install and look at the examples directory.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Test/QuickSpec.hs view
@@ -0,0 +1,87 @@+-- | The main QuickSpec module.+--+-- This will not make sense if you haven't seen some examples!+-- Look at <http://github.com/nick8325/quickspec/tree/master/examples>,+-- or read the paper at <http://www.cse.chalmers.se/~nicsma/quickspec.pdf>.++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,+   -- * 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,+   -- * 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,+   withTests,+   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
+ Test/QuickSpec/Approximate.hs view
@@ -0,0 +1,63 @@+-- Utilities for testing functions that return partial results.+{-# LANGUAGE Rank2Types #-}+module Test.QuickSpec.Approximate where++import Test.QuickCheck+import Test.QuickCheck.Gen+import Test.QuickSpec.Signature+import Test.QuickSpec.Utils+import Test.QuickSpec.Utils.Typeable+import Control.Monad+import Control.Monad.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 => (StdGen, Int) -> a -> a+approximate (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 n)+        else resize (m-1) $ do+          y <- x+          case spoony y of+            Just z -> return z+            Nothing -> return (unGen arbitrary g n)++pobserver :: (Ord a, Partial a) => a -> Sig+pobserver x = observerSig (Observer (MkGen f))+  where f g n y = approximate (g, n `max` 50) (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` gvars xs ((arbitrary `asTypeOf` return w) >>= genPartial)
+ Test/QuickSpec/Equation.hs view
@@ -0,0 +1,23 @@+-- | 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++data Equation = Term :=: Term deriving (Eq, Ord)++showEquation :: Sig -> Equation -> String+showEquation sig (t :=: u) =+  show (f t) ++ " == " ++ show (f u)+  where f = disambiguate sig (vars t ++ vars u)++instance Show Equation where+  show = showEquation mempty++equations :: [[Tagged Term]] -> [Equation]+equations = sort . concatMap (toEquations . map erase)+  where toEquations (x:xs) = [y :=: x | y <- xs]
+ Test/QuickSpec/Generate.hs view
@@ -0,0 +1,88 @@+-- | The testing loop and term generation of QuickSpec.++{-# LANGUAGE Rank2Types, TypeOperators, ScopedTypeVariables #-}+module Test.QuickSpec.Generate where++import Test.QuickSpec.Signature hiding (con)+import qualified Test.QuickSpec.TestTree as T+import Test.QuickSpec.TestTree(TestResults, reps, classes, numTests, 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+import System.Random+import Control.Spoon+import Test.QuickSpec.Utils.MemoValuation++terms :: Sig -> TypeRel Expr -> TypeRel Expr+terms sig base =+  TypeMap.fromList+    [ Some (O (terms' sig base w))+    | Some (Witness w) <- usort (saturatedTypes sig ++ variableTypes sig) ]++terms' :: Typeable a => Sig -> TypeRel Expr -> a -> [Expr a]+terms' sig base w =+  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' sig base (const w),+    arity f > 0,+    not (isUndefined (term f)) ]++test :: [(StdGen, Int)] -> Sig ->+        TypeMap (List `O` Expr) -> TypeMap (TestResults `O` Expr)+test seeds sig ts = fmap (mapSome2 (test' seeds sig)) ts++test' :: forall a. Typeable a => [(StdGen, Int)] -> Sig -> [Expr a] -> TestResults (Expr a)+test' seeds sig ts+  | not (testable sig (undefined :: a)) = discrete ts+  | otherwise =+    case observe undefined sig of+      Observer obs ->+        let testCase (g, n) =+              let (g1, g2) = split g+                  val = memoValuation sig (unGen valuation g1 n) in+              \x -> spoony . unGen obs g2 n $ eval x val+        in cutOff base increment (T.test (map testCase seeds) ts)+  where+    base = minTests sig `div` 2+    increment = minTests sig - base++genSeeds :: IO [(StdGen, Int)]+genSeeds = do+  rnd <- newStdGen+  let rnds rnd = rnd1 : rnds rnd2 where (rnd1, rnd2) = split rnd+  return (zip (rnds rnd) (concat (repeat [0,2..100])))++generate :: Sig -> IO (TypeMap (TestResults `O` Expr))+generate sig | maxDepth sig < 0 =+  error "Test.QuickSpec.Generate.generate: maxDepth must be positive"+generate sig | maxDepth sig == 0 = return TypeMap.empty+generate sig = unbuffered $ do+  let d = maxDepth sig+  rs <- fmap (TypeMap.mapValues2 reps) (generate (updateDepth (d-1) sig))+  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 = terms sig rs+  printf "%d terms, " (count sum length ts)+  seeds <- genSeeds+  let cs = test seeds sig ts+  printf "%d tests, %d classes, %d raw equations.\n"+      (count (maximum . (0:)) numTests 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
+ Test/QuickSpec/Main.hs view
@@ -0,0 +1,138 @@+-- | The main implementation of QuickSpec.++{-# LANGUAGE TypeOperators #-}+module Test.QuickSpec.Main where++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 Test.QuickSpec.Signature hiding (vars)+import Test.QuickSpec.Term+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 :: Int -> [Tagged Term] -> [Term] -> [Equation] -> [Equation]+prune d univ reps eqs = evalEQ (initial d univ) (filterM (fmap not . provable) 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++-- | Run QuickSpec on a signature.+quickSpec :: Signature a => a -> IO ()+quickSpec = runTool $ \sig -> do+  putStrLn "== Testing =="+  r <- generate sig+  let clss = eraseClasses r+      reps = map (erase . head) clss+      eqs = equations clss+      univ = universe clss+  printf "%d raw equations; %d terms in universe.\n\n"+    (length eqs)+    (length univ)++  let pruned = filter (not . all silent . eqnFuns)+                 (prune (maxDepth sig) univ reps eqs)+      eqnFuns (t :=: u) = funs t ++ funs u+      isGround (t :=: u) = null (vars t) && null (vars u)+      (ground, nonground) = partition isGround pruned+  putStrLn "== Ground equations =="+  forM_ (zip [1 :: Int ..] ground) $ \(i, eq) ->+    printf "%3d: %s\n" i (showEquation sig eq)+  putStrLn ""++  putStrLn "== Non-ground equations =="+  forM_ (zip [length ground + 1 ..] nonground) $ \(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 "Test.QuickSpec.Main.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 (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 (disambiguate sig (vars t) t))++  putStrLn ""
+ Test/QuickSpec/Prelude.hs view
@@ -0,0 +1,89 @@+-- | 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.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)+newtype B = B Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary)+newtype C = C Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary)++-- | 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)++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`)@.+prelude :: (Typeable a, Ord a, Arbitrary a) => a -> Sig+prelude a = background [+  ["x", "y", "z"] `vars` a,+  bools,+  arith (undefined :: Int),+  lists a ]
+ Test/QuickSpec/Reasoning/CongruenceClosure.hs view
@@ -0,0 +1,167 @@+-- | 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
+ Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs view
@@ -0,0 +1,123 @@+-- | Equational reasoning built on top of congruence closure.++{-# LANGUAGE TupleSections #-}+module Test.QuickSpec.Reasoning.NaiveEquationalReasoning where++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,+  universe :: Map TypeRep Universe,+  maxDepth :: Int+  }++type Universe = IntMap [Int]++type EQ = ReaderT (Map TypeRep Universe, Int) CC++initial :: Int -> [Tagged Term] -> Context+initial d ts =+  let n = 1+maximum (0:concatMap (map index . symbols . erase) ts)+      (universe, rel) =+        CC.runCC (CC.initial n) $+          forM (partitionBy (witnessType . tag) ts) $ \xs@(x:_) ->+            fmap (witnessType (tag x),) (createUniverse (map erase xs))++  in Context rel (Map.fromList universe) d++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 (universe ctx, maxDepth 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++unifiable :: Equation -> EQ Bool+unifiable (t :=: u) = t =?= u++(=:=) :: Term -> Term -> EQ Bool+t =:= u = do+  (ctx, d) <- 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++unify :: Equation -> EQ Bool+unify (t :=: u) = t =:= u++type Subst = Symbol -> Int++substs :: Term -> Map TypeRep 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 = Map.findWithDefault+                  (error "Test.QuickSpec.Reasoning.NaiveEquationalReasoning.substs: empty universe")+                  (symbolType 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)
+ Test/QuickSpec/Reasoning/UnionFind.hs view
@@ -0,0 +1,64 @@+-- | 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')
+ Test/QuickSpec/Signature.hs view
@@ -0,0 +1,453 @@+-- | Functions for constructing and analysing signatures.++{-# LANGUAGE Rank2Types, ExistentialQuantification, ScopedTypeVariables #-}+module Test.QuickSpec.Signature where++import Control.Applicative hiding (some)+import Test.QuickSpec.Utils.Typeable+import Data.Monoid+import Test.QuickCheck+import Test.QuickSpec.Term hiding (var)+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 and observation functions.+  constants :: TypeRel Constant,+  variables :: TypeRel Variable,+  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,++  -- Minimum number of tests to run.+  minTests_ :: First Int+  }++maxDepth :: Sig -> Int+maxDepth = fromMaybe 3 . getFirst . maxDepth_++updateDepth :: Int -> Sig -> Sig+updateDepth n sig = sig { maxDepth_ = First (Just n) }++minTests :: Sig -> Int+minTests = fromMaybe 500 . getFirst . minTests_++updateMinTests :: Int -> Sig -> Sig+updateMinTests n sig = sig { minTests_ = First (Just n) }++instance Show Sig where show = unlines . 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' ]++summarise :: Sig -> [String]+summarise sig =+  section ["-- functions --"]+    (decls (filter (not . silent) allConstants)) +++  section ["-- background functions --"]+    (decls (filter silent allConstants)) +++  section ["-- variables --"]+    (decls allVariables) +++  section ["-- the following types are using non-standard equality --"]+    (map show (Map.keys (observers sig))) ++++  section ["-- WARNING: the following types are uninhabited --"]+    (usort+     [ show (uses sig ty)+     | ty <- argumentTypes sig,+       ty `notElem` inhabitedTypes sig,+       ty `notElem` variableTypes sig ]) ++++  section ["-- WARNING: there are no variables of the following types; consider adding some --"]+    (usort+     [ show 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 ]) +++  section ["-- WARNING: cannot test the following types; ",+        "            consider using 'fun' instead of 'blind' or using 'observe' --"]+    (usort+     [ show ty+     | ty@(Some (Witness w)) <- saturatedTypes sig,+       -- The type is untestable and is the result type of a constant+       not (testable sig w) ])++  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)++    section _ [] = []+    section msg xs = msg ++ xs ++ [""]++    decls xs = map decl (partitionBy symbolType xs)++    decl xs@(x:_) =+      intercalate ", " (map show xs) ++ " :: " ++ show (symbolType x)++data Observer a = forall b. Ord b => Observer (Gen (a -> b))++observe x sig =+  TypeMap.lookup (TypeMap.lookup (error msg) x (ords sig))+               x (observers sig)+  where msg = "Test.QuickSpec.Signature.observe: no observers found for type " ++ show (typeOf x)++emptySig :: Sig+emptySig = Sig TypeRel.empty TypeRel.empty TypeMap.empty TypeMap.empty TypeMap.empty mempty mempty++instance Monoid Sig where+  mempty = emptySig+  s1 `mappend` s2 =+    Sig {+      constants = renumber (mapConstant . alter) 0 constants',+      variables = renumber (mapVariable . alter) (length constants') variables',+      observers = observers s1 `mappend` observers s2,+      ords = ords s1 `mappend` ords s2,+      witnesses = witnesses s1 `mappend` witnesses s2,+      maxDepth_ = maxDepth_ s1 `mappend` maxDepth_ s2,+      minTests_ = minTests_ s1 `mappend` minTests_ 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) }++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 @withTests n@ is in your signature,+--   QuickSpec will run at least @n@ tests+--   (the default is 500).+withTests :: Int -> Sig+withTests n = updateMinTests n emptySig++-- | @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)++-- | 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++ord :: (Ord a, Typeable a) => a -> Sig+ord x = ordSig (Observer (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 }++-- | Similar to `vars`, but takes a generator as a parameter.+--+-- @gvars xs (arbitrary :: Gen a)@ is the same as+-- @vars xs (undefined :: a)@.+gvars :: forall a. Typeable a => [String] -> Gen a -> Sig+gvars xs g = variableSig [ Variable (Atom (symbol x 0 (undefined :: a)) g) | x <- xs ]+            `mappend` typeSig (undefined :: a)++-- | 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 :: forall a. (Arbitrary a, Typeable a) => [String] -> a -> Sig+vars xs _ = gvars xs (arbitrary :: Gen a)++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)++-- | An observation function of arity 1.+observer1 :: (Typeable a, Typeable b, Ord b) => (a -> b) -> Sig+observer1 f = observerSig (Observer (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 (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 (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 (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 = "Test.QuickSpec.Signature.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 "Test.QuickSpec.Signature.findWitness: missing type")+    (lookupWitness sig ty)++lookupWitness :: Sig -> TypeRep -> Maybe Witness+lookupWitness sig ty = Map.lookup ty (witnesses sig)++disambiguate :: Sig -> [Symbol] -> Term -> Term+disambiguate sig ss =+  mapVars (\x ->+    fromMaybe (error "Test.QuickSpec.Term.disambiguate: 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 "Test.QuickSpec.Term.disambiguate: null allVars"+              | otherwise = wellTypedNames ++ concat [ map (++ show i) wellTypedNames | i <- [1.. ] ]+            allVars =+              map (some (sym . unVariable))+                (TypeRel.toList (variables sig)) +++              ss+            wellTypedNames =+              [ name v | v <- allVars, symbolType v == symbolType x ]
+ Test/QuickSpec/Term.hs view
@@ -0,0 +1,173 @@+-- | Terms and evaluation.++{-# LANGUAGE RankNTypes, ExistentialQuantification, DeriveFunctor #-}+module Test.QuickSpec.Term where++import Test.QuickSpec.Utils.Typeable+import Test.QuickCheck+import Data.Function+import Data.Ord+import Data.Char+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 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 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)++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 == '\''++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, size :: Term -> Int+depth (App f x) = depth f `max` (1 + depth x)+depth _ = 1+size (App f x) = size f + size x+size (Var _) = 0+size (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)++data Expr a = Expr {+  term :: Term,+  arity :: {-# UNPACK #-} !Int,+  eval :: (forall b. Variable b -> b) -> a }++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++newtype Variable a = Variable { unVariable :: Atom (Gen 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+valuation :: Gen (Variable a -> a)+valuation = promote (\(Variable x) -> index (sym x) `variant'` value x)+  where -- work around the fact that split doesn't work+        variant' 0 = variant (0 :: Int)+        variant' n = variant (-1 :: Int) . variant' (n-1)++var :: Variable a -> Expr a+var v@(Variable (Atom x _)) = Expr (Var x) 0 (\env -> 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 "Test.QuickSpec.Term.app: oversaturated function"+  | otherwise = Expr (App t u) (a - 1) (\env -> f env (x env))
+ Test/QuickSpec/TestTree.hs view
@@ -0,0 +1,98 @@+-- | A data structure to represent refining a set of terms into+--   equivalence classes by testing.++module Test.QuickSpec.TestTree(TestTree, terms, union, test,+               TestResults, cutOff, numTests, classes, reps, discrete) where++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 "Test.QuickSpec.TestTree.tree: bug: 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) 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 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' 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)++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
+ Test/QuickSpec/Utils.hs view
@@ -0,0 +1,50 @@+-- | 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)
+ Test/QuickSpec/Utils/MemoValuation.hs view
@@ -0,0 +1,22 @@+-- | 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 -> (forall a. Variable a -> a) -> (forall a. Variable a -> a)+memoValuation sig f = 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)
+ Test/QuickSpec/Utils/TypeMap.hs view
@@ -0,0 +1,40 @@+-- | 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+        Nothing ->+          error "Test.QuickSpec.Utils.TypeMap.lookup: type error"+        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))
+ Test/QuickSpec/Utils/TypeRel.hs view
@@ -0,0 +1,46 @@+-- | A relation between types and values.+--   @'TypeRel' f@ relates each type @a@ to a set of values+--   of type @f a@.++{-# LANGUAGE Rank2Types, TypeOperators #-}+module Test.QuickSpec.Utils.TypeRel where++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 "Test.QuickSpec.Utils.TypeRep.sequence: empty list"+gather (Some x:xs) = Some (O (x:map gcast' xs))+  where gcast' (Some y) = fromMaybe (error msg) (gcast y)+        msg = "Test.QuickSpec.Utils.TypeRep.gather: 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)
+ Test/QuickSpec/Utils/Typeable.hs view
@@ -0,0 +1,51 @@+{-# 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))
+ Test/QuickSpec/Utils/Typed.hs view
@@ -0,0 +1,76 @@+-- | Functions for working with existentially-quantified types+--   and similar.++{-# LANGUAGE Rank2Types, ExistentialQuantification, TypeOperators, TypeSynonymInstances, FlexibleInstances #-}+module Test.QuickSpec.Utils.Typed where++import Control.Monad+import Test.QuickSpec.Utils.Typeable+import Data.Ord+import Data.Function+import Data.Maybe++data Some f = forall a. Typeable a => Some (f a)++newtype O f g a = O { unO :: f (g a) }+type List = []++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++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 = "Test.QuickSpec.Utils.Typed.rightArrow: type oversaturated"
+ examples/Arith.hs view
@@ -0,0 +1,18 @@+-- 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)]++main = quickSpec (arith (undefined :: Int))
+ examples/Bools.hs view
@@ -0,0 +1,14 @@+-- 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]++main = quickSpec bools
+ examples/Composition.hs view
@@ -0,0 +1,24 @@+{-# 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+  ]++main = quickSpec (composition (undefined :: A))
+ examples/Heaps.hs view
@@ -0,0 +1,89 @@+{-# 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),+  "toList"     `fun1` (toList     :: Heap a -> [a]),+  "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.+  background [+  "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/Lists.hs view
@@ -0,0 +1,27 @@+{-# 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 = [+  arith (undefined :: Int),+  funs (undefined :: a),++  ["x", "y", "z"] `vars` (undefined :: a),+  ["xs", "ys", "zs"] `vars` (undefined :: [a]),++  "[]"      `fun0` ([]      :: [a]),+  ":"       `fun2` ((:)     :: a -> [a] -> [a]),+  "head"    `fun1` (head    :: [a] -> a),+  "tail"    `fun1` (tail    :: [a] -> [a]),+  "unit"    `fun1` (return  :: a -> [a]),+  "++"      `fun2` ((++)    :: [a] -> [a] -> [a]),+  "length"  `fun1` (length  :: [a] -> Int),+  "reverse" `fun1` (reverse :: [a] -> [a]),+  "map"     `fun2` (map     :: (a -> a) -> [a] -> [a])+  ]++main = quickSpec (lists (undefined :: A))
+ examples/TinyWM.hs view
@@ -0,0 +1,194 @@+-- This example requires QuickCheck >= 2.5. For older versions, you will+-- have to define an Arbitrary Ordering instance, like so:+--   instance Arbitrary Ordering where+--     arbitrary = elements [LT, EQ, GT]++-- A window manager example,+-- taken from http://donsbot.wordpress.com/2007/05/01/roll-your-own-window-manager-part-1-defining-and-testing-a-model++{-# 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
+ quickspec.cabal view
@@ -0,0 +1,89 @@+Name:                quickspec+Version:             0.9+Cabal-version:       >=1.6+Build-type:          Simple++Homepage:            https://github.com/nick8325/quickspec+Author:              Nick Smallbone+Maintainer:          nicsma@chalmers.se++License:             BSD3+License-file:        LICENSE+Copyright:           2009-2013 Nick Smallbone++Category:            Testing++Synopsis:            Equational laws for free+Description:+  QuickSpec automatically finds equational properties of your program.+  .+  Give it an API, i.e. a collection of functions, and it will spit out+  equations about those functions. For example, given @reverse@, @++@+  and @[]@, QuickSpec finds six laws:+  .+  > xs++[] == xs+  > []++xs == xs+  > reverse [] == []+  > (xs++ys)++zs == xs++(ys++zs)+  > reverse (reverse xs) == xs+  > reverse xs++reverse ys == reverse (ys++xs)+  .+  All you have to provide is:+  .+  * Some functions and constants to test. These are the /only/+    functions that will appear in the equations.+  .+  * A collection of variables that can appear in the equations+    (@xs@, @ys@ and @zs@ in the example above).+  .+  * 'Test.QuickCheck.Arbitrary' and 'Data.Typeable.Typeable' instances for the types you want to test.+  .+  Consider this a pre-release. Everything is complete but undocumented+  :) The best place to start is the examples at+  <http://github.com/nick8325/quickspec/tree/master/examples>. There+  is also a paper at+  <http://www.cse.chalmers.se/~nicsma/quickspec.pdf>.+  Everything you need should be in the module "Test.QuickSpec".+  .+  If you want help, email me!++Extra-source-files:+  README+  examples/Arith.hs+  examples/Bools.hs+  examples/Composition.hs+  examples/Heaps.hs+  examples/Lists.hs+  examples/TinyWM.hs++source-repository head+  type:     git+  location: git://github.com/nick8325/quickspec.git+  branch:   master++library+  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.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++  Build-depends:+    base < 5, containers, transformers, QuickCheck,+    random, spoon >= 0.2, array, ghc-prim, mtl