packages feed

quickspec 0.9 → 0.9.1

raw patch · 42 files changed

+2186/−1854 lines, 42 files

Files

− Test/QuickSpec.hs 
@@ -1,87 +0,0 @@--- | 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 
@@ -1,63 +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.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 
@@ -1,23 +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--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 
@@ -1,88 +0,0 @@--- | 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 
@@ -1,138 +0,0 @@--- | 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 
@@ -1,89 +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.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 
@@ -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
− Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs 
@@ -1,123 +0,0 @@--- | 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 
@@ -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')
− Test/QuickSpec/Signature.hs 
@@ -1,453 +0,0 @@--- | 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 
@@ -1,173 +0,0 @@--- | 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 
@@ -1,98 +0,0 @@--- | 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 
@@ -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)
− 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 -> (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 
@@ -1,40 +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-        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 
@@ -1,46 +0,0 @@--- | 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 
@@ -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))
− Test/QuickSpec/Utils/Typed.hs 
@@ -1,76 +0,0 @@--- | 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/Heaps.hs view
@@ -72,14 +72,18 @@   "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.+  -- 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),
examples/Lists.hs view
@@ -13,8 +13,10 @@   ["x", "y", "z"] `vars` (undefined :: a),   ["xs", "ys", "zs"] `vars` (undefined :: [a]), +  background [   "[]"      `fun0` ([]      :: [a]),-  ":"       `fun2` ((:)     :: a -> [a] -> [a]),+  ":"       `fun2` ((:)     :: a -> [a] -> [a])],+   "head"    `fun1` (head    :: [a] -> a),   "tail"    `fun1` (tail    :: [a] -> [a]),   "unit"    `fun1` (return  :: a -> [a]),
quickspec.cabal view
@@ -1,5 +1,5 @@ Name:                quickspec-Version:             0.9+Version:             0.9.1 Cabal-version:       >=1.6 Build-type:          Simple @@ -55,6 +55,7 @@   examples/Heaps.hs   examples/Lists.hs   examples/TinyWM.hs+  src/Test/QuickSpec/errors.h  source-repository head   type:     git@@ -62,6 +63,7 @@   branch:   master  library+  hs-source-dirs: src   Exposed-modules:     Test.QuickSpec,     Test.QuickSpec.Main,@@ -74,6 +76,8 @@     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,
+ src/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
+ src/Test/QuickSpec/Approximate.hs view
@@ -0,0 +1,71 @@+-- 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.Term+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 => (forall a. Partial a => a -> Maybe a) -> StdGen -> 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` variableSig [ Variable (Atom (symbol x 0 w) (PGen g g')) | x <- xs ]+  `mappend` totalSig g+  `mappend` partialSig g'+  `mappend` typeSig w+  where+    g = arbitrary `asTypeOf` return w+    g' = g >>= genPartial
+ src/Test/QuickSpec/Equation.hs view
@@ -0,0 +1,42 @@+-- | 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 (f t) ++ " == " ++ show (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 view
@@ -0,0 +1,90 @@+-- | 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, 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 :: Strategy -> [(StdGen, Int)] -> Sig ->+        TypeMap (List `O` Expr) -> TypeMap (TestResults `O` Expr)+test strat seeds sig ts = fmap (mapSome2 (test' strat seeds sig)) ts++test' :: forall a. Typeable a =>+         Strategy -> [(StdGen, Int)] -> Sig -> [Expr a] -> TestResults (Expr a)+test' strat 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 strat) g1 n) in+              \x -> spoony . unGen (partialGen 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 :: Int -> IO [(StdGen, Int)]+genSeeds maxSize = do+  rnd <- newStdGen+  let rnds rnd = rnd1 : rnds rnd2 where (rnd1, rnd2) = split rnd+  return (zip (rnds rnd) (concat (repeat [0,2..maxSize])))++generate :: Strategy -> Sig -> IO (TypeMap (TestResults `O` Expr))+generate strat sig | maxDepth sig < 0 =+  ERROR "generate: maxDepth must be positive"+generate strat sig | maxDepth sig == 0 = return TypeMap.empty+generate strat sig = unbuffered $ do+  let d = maxDepth sig+  rs <- fmap (TypeMap.mapValues2 reps) (generate (const partialGen) (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 (maxQuickCheckSize sig)+  let cs = test strat 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
+ src/Test/QuickSpec/Main.hs view
@@ -0,0 +1,157 @@+-- | 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 (const partialGen) sig+  let clss = concatMap (some2 (map (Some . O) . classes)) (TypeMap.toList r)+      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) reps+      pruned = filter (not . all silent . eqnFuns)+                 (prune ctx (map erase reps) id+                   (map (some eraseEquation) eqs))+      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 (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 (disambiguate sig (vars t) t))++  putStrLn ""
+ src/Test/QuickSpec/Prelude.hs view
@@ -0,0 +1,90 @@+-- | 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, Partial)+newtype B = B Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Partial)+newtype C = C Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Partial)++-- | 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 ]
+ src/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
+ src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs view
@@ -0,0 +1,128 @@+-- | 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 view
@@ -0,0 +1,140 @@+-- | 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.State+import qualified Control.Monad.State as S+import Data.List+import Data.Ord+import Test.QuickSpec.Utils+import Test.QuickSpec.Signature hiding (vars)+import Data.Monoid++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 (f t) ++ " == " ++ show (f u) +++  showPre (map (f . Var) 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 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')
+ src/Test/QuickSpec/Signature.hs view
@@ -0,0 +1,480 @@+-- | Functions for constructing and analysing signatures.++{-# LANGUAGE CPP, Rank2Types, ExistentialQuantification, ScopedTypeVariables #-}+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)+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,++  -- Minimum number of tests to run.+  minTests_ :: First Int,++  -- Maximum size parameter to pass to QuickCheck.+  maxQuickCheckSize_ :: 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_++maxQuickCheckSize :: Sig -> Int+maxQuickCheckSize = fromMaybe 20 . getFirst . maxQuickCheckSize_++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 (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++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,+      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,+      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 @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)++-- | 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 (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 }++-- | 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)) (pgen g)) | x <- xs ]+             `mappend` totalSig g+             `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 (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] -> Term -> Term+disambiguate sig ss =+  mapVars (\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 = 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 ]++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 view
@@ -0,0 +1,188 @@+-- | 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 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 == '\'' || 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 }+  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+valuation :: Strategy -> Gen (Variable a -> a)+valuation strat = promote (\(Variable x) -> index (sym x) `variant'` strat (sym x) (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 "oversaturated function"+  | otherwise = Expr (App t u) (a - 1) (\env -> f env (x env))
+ src/Test/QuickSpec/TestTotality.hs view
@@ -0,0 +1,77 @@+-- | 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 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+        -- Hack around "value restriction" for lambdas+        MkGen $ \g n ->+          let v = unGen (valuation strat) g n+          in spoony (obs' (eval e1 v)) == spoony (obs' (eval e2 v))++always :: Sig -> Gen Bool -> IO Bool+always sig x = do+  gens <- replicateM 100 newStdGen+  let sizes = cycle [0,2..maxQuickCheckSize sig]+  return (and [unGen x g n | (g, n) <- zip gens sizes])
+ src/Test/QuickSpec/TestTree.hs view
@@ -0,0 +1,99 @@+-- | 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, 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) 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
+ src/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)
+ src/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)
+ src/Test/QuickSpec/Utils/TypeMap.hs view
@@ -0,0 +1,38 @@+-- | 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 view
@@ -0,0 +1,47 @@+-- | 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 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))
+ src/Test/QuickSpec/Utils/Typed.hs view
@@ -0,0 +1,82 @@+-- | Functions for working with existentially-quantified types+--   and similar.++{-# LANGUAGE CPP, Rank2Types, ExistentialQuantification, TypeOperators, TypeSynonymInstances, FlexibleInstances #-}+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++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"
+ src/Test/QuickSpec/errors.h view
@@ -0,0 +1,3 @@+-- Inspired by Agda's undefined.h+#define __ (ERROR "no error message given")+#define ERROR (\msg -> error ("Error at file " ++ __FILE__ ++ ", line " ++ show __LINE__ ++ ": " ++ msg))