diff --git a/Test/QuickSpec.hs b/Test/QuickSpec.hs deleted file mode 100644 --- a/Test/QuickSpec.hs +++ /dev/null @@ -1,87 +0,0 @@ --- | The main QuickSpec module. --- --- This will not make sense if you haven't seen some examples! --- Look at , --- or read the paper at . - -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 diff --git a/Test/QuickSpec/Approximate.hs b/Test/QuickSpec/Approximate.hs deleted file mode 100644 --- a/Test/QuickSpec/Approximate.hs +++ /dev/null @@ -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) diff --git a/Test/QuickSpec/Equation.hs b/Test/QuickSpec/Equation.hs deleted file mode 100644 --- a/Test/QuickSpec/Equation.hs +++ /dev/null @@ -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] diff --git a/Test/QuickSpec/Generate.hs b/Test/QuickSpec/Generate.hs deleted file mode 100644 --- a/Test/QuickSpec/Generate.hs +++ /dev/null @@ -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 diff --git a/Test/QuickSpec/Main.hs b/Test/QuickSpec/Main.hs deleted file mode 100644 --- a/Test/QuickSpec/Main.hs +++ /dev/null @@ -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 "" diff --git a/Test/QuickSpec/Prelude.hs b/Test/QuickSpec/Prelude.hs deleted file mode 100644 --- a/Test/QuickSpec/Prelude.hs +++ /dev/null @@ -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 ] diff --git a/Test/QuickSpec/Reasoning/CongruenceClosure.hs b/Test/QuickSpec/Reasoning/CongruenceClosure.hs deleted file mode 100644 --- a/Test/QuickSpec/Reasoning/CongruenceClosure.hs +++ /dev/null @@ -1,167 +0,0 @@ --- | A decision procedure for ground equality, --- based on the paper "Proof-producing Congruence Closure". - -module Test.QuickSpec.Reasoning.CongruenceClosure(CC, newSym, (=:=), (=?=), rep, evalCC, execCC, runCC, ($$), S, funUse, argUse, lookup, initial, frozen) where - -import Prelude hiding (lookup) -import Control.Monad -import Control.Monad.Trans.State.Strict -import Data.IntMap(IntMap) -import qualified Data.IntMap as IntMap -import Test.QuickSpec.Reasoning.UnionFind(UF, Replacement((:>))) -import qualified Test.QuickSpec.Reasoning.UnionFind as UF -import Data.Maybe -import Data.List(foldl') --- import Test.QuickCheck --- import Test.QuickCheck.Arbitrary --- import Test.QuickCheck.Monadic -import Text.Printf - -lookup2 :: Int -> Int -> IntMap (IntMap a) -> Maybe a -lookup2 k1 k2 m = IntMap.lookup k2 (IntMap.findWithDefault IntMap.empty k1 m) - -insert2 :: Int -> Int -> a -> IntMap (IntMap a) -> IntMap (IntMap a) -insert2 k1 k2 v m = IntMap.insertWith IntMap.union k1 (IntMap.singleton k2 v) m - -delete2 :: Int -> Int -> IntMap (IntMap a) -> IntMap (IntMap a) -delete2 k1 k2 m = IntMap.adjust (IntMap.delete k2) k1 m - -data FlatEqn = (Int, Int) := Int deriving (Eq, Ord) - -data S = S { - -- in all these maps, the keys are representatives, the values may not be - funUse :: !(IntMap [(Int, Int)]), - argUse :: !(IntMap [(Int, Int)]), - lookup :: IntMap (IntMap Int), - uf :: UF.S - } - -type CC = State S - -liftUF :: UF a -> CC a -liftUF m = do - s <- get - let (x, uf') = UF.runUF (uf s) m - put s { uf = uf' } - return x - -invariant :: String -> CC () -invariant _ = return () --- invariant str = do --- S funUse argUse lookup <- get --- -- keys of all maps are representatives --- let check phase x = do --- b <- liftUF (UF.isRep x) --- if b then return () else error (printf "%s, %s appears as a key in %s but is not a rep in:\nfunUse=%s\nargUse=%s\nlookup=%s" str (show x) phase (show funUse) (show argUse) (show lookup)) --- mapM_ (check "funUse") (IntMap.keys funUse) --- mapM_ (check "argUse") (IntMap.keys argUse) --- mapM_ (check "lookup") (IntMap.keys lookup) --- mapM_ (mapM_ (check "inner lookup") . IntMap.keys) (IntMap.elems lookup) - -modifyFunUse f = modify (\s -> s { funUse = f (funUse s) }) -modifyArgUse f = modify (\s -> s { argUse = f (argUse s) }) -addFunUses xs s = modifyFunUse (IntMap.insertWith (++) s xs) -addArgUses xs s = modifyArgUse (IntMap.insertWith (++) s xs) -modifyLookup f = modify (\s -> s { lookup = f (lookup s) }) -putLookup l = modifyLookup (const l) - -newSym :: CC Int -newSym = liftUF UF.newSym - -($$) :: Int -> Int -> CC Int -f $$ x = do - invariant (printf "before %s$$%s" (show f) (show x)) - m <- gets lookup - f' <- rep f - x' <- rep x - invariant (printf "at %s$$%s:1" (show f) (show x)) - case lookup2 x' f' m of - Nothing -> do - c <- newSym - invariant (printf "at %s$$%s:2" (show f) (show x)) - putLookup (insert2 x' f' c m) - addFunUses [(x', c)] f' - addArgUses [(f', c)] x' - invariant (printf "after %s$$%s" (show f) (show x)) - return c - Just k -> return k - -(=:=) :: Int -> Int -> CC Bool -a =:= b = propagate (a, b) - -(=?=) :: Int -> Int -> CC Bool -t =?= u = liftM2 (==) (rep t) (rep u) - -propagate (a, b) = do - (unified, pending) <- propagate1 (a, b) - mapM_ propagate pending - return unified - -propagate1 (a, b) = do - invariant (printf "before propagate (%s, %s)" (show a) (show b)) - res <- liftUF (a UF.=:= b) - case res of - Nothing -> return (False, []) - Just (r :> r') -> do - funUses <- gets (IntMap.lookup r . funUse) - argUses <- gets (IntMap.lookup r . argUse) - case (funUses, argUses) of - (Nothing, Nothing) -> return (True, []) - _ -> fmap (\x -> (True, x)) (updateUses r r' (fromMaybe [] funUses) (fromMaybe [] argUses)) - -updateUses r r' funUses argUses = do - modifyFunUse (IntMap.delete r) - modifyArgUse (IntMap.delete r) - modifyLookup (IntMap.delete r) - forM_ funUses $ \(x, _) -> do - x' <- rep x - modifyLookup (delete2 x' r) - invariant (printf "after deleting %s" (show r)) - let repPair (x, c) = do - x' <- rep x - return (x', c) - funUses' <- mapM repPair funUses - argUses' <- mapM repPair argUses - - m <- gets lookup - - let foldUses insert lookup pending m uses = foldl' op e uses - where op (pending, newUses, m) (x', c) = - case lookup x' m of - Just k -> ((c, k):pending, newUses, m) - Nothing -> (pending, (x', c):newUses, insert x' c m) - e = (pending, [], m) - - (funPending, funNewUses, m') = foldUses (\x' c m -> insert2 x' r' c m) - (\x' m -> lookup2 x' r' m) - [] m funUses' - - (pending, argNewUses, argM) = foldUses IntMap.insert IntMap.lookup funPending - (IntMap.findWithDefault IntMap.empty r' m') - argUses' - - addFunUses funNewUses r' - addArgUses argNewUses r' - - putLookup (if IntMap.null argM then m' else IntMap.insert r' argM m') - invariant (printf "after updateUses (%s, %s)" (show r) (show r')) - - return pending - -rep :: Int -> CC Int -rep s = liftUF (UF.rep s) - -runCC :: S -> CC a -> (a, S) -runCC s m = runState m s - -evalCC :: S -> CC a -> a -evalCC s m = fst (runCC s m) - -execCC :: S -> CC a -> S -execCC s m = snd (runCC s m) - -initial :: Int -> S -initial n = S IntMap.empty IntMap.empty IntMap.empty (UF.initial n) - -frozen :: CC a -> CC a -frozen x = fmap (evalState x) get diff --git a/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs b/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs deleted file mode 100644 --- a/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs +++ /dev/null @@ -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) diff --git a/Test/QuickSpec/Reasoning/UnionFind.hs b/Test/QuickSpec/Reasoning/UnionFind.hs deleted file mode 100644 --- a/Test/QuickSpec/Reasoning/UnionFind.hs +++ /dev/null @@ -1,64 +0,0 @@ --- | A union-find data structure. - -module Test.QuickSpec.Reasoning.UnionFind(UF, Replacement((:>)), newSym, (=:=), rep, evalUF, execUF, runUF, S, isRep, initial) where - -import Prelude hiding (min) -import Control.Monad -import Control.Monad.Trans.State.Strict -import Data.IntMap(IntMap) -import qualified Data.IntMap as IntMap - -data S = S { - links :: IntMap Int, - sym :: Int - } - -type UF = State S -data Replacement = Int :> Int - -runUF :: S -> UF a -> (a, S) -runUF s m = runState m s - -evalUF :: S -> UF a -> a -evalUF s m = fst (runUF s m) - -execUF :: S -> UF a -> S -execUF s m = snd (runUF s m) - -initial :: Int -> S -initial n = S IntMap.empty n - -modifyLinks f = modify (\s -> s { links = f (links s) }) -modifySym f = modify (\s -> s { sym = f (sym s) }) -putLinks l = modifyLinks (const l) - -newSym :: UF Int -newSym = do - s <- get - modifySym (+1) - return (sym s) - -(=:=) :: Int -> Int -> UF (Maybe Replacement) -s =:= t | s == t = return Nothing -s =:= t = do - rs <- rep s - rt <- rep t - if (rs /= rt) then do - modifyLinks (IntMap.insert rs rt) - return (Just (rs :> rt)) - else return Nothing - -rep :: Int -> UF Int -rep t = do - m <- fmap links get - case IntMap.lookup t m of - Nothing -> return t - Just t' -> do - r <- rep t' - when (t' /= r) $ modifyLinks (IntMap.insert t r) - return r - -isRep :: Int -> UF Bool -isRep t = do - t' <- rep t - return (t == t') diff --git a/Test/QuickSpec/Signature.hs b/Test/QuickSpec/Signature.hs deleted file mode 100644 --- a/Test/QuickSpec/Signature.hs +++ /dev/null @@ -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 ] diff --git a/Test/QuickSpec/Term.hs b/Test/QuickSpec/Term.hs deleted file mode 100644 --- a/Test/QuickSpec/Term.hs +++ /dev/null @@ -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)) diff --git a/Test/QuickSpec/TestTree.hs b/Test/QuickSpec/TestTree.hs deleted file mode 100644 --- a/Test/QuickSpec/TestTree.hs +++ /dev/null @@ -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 diff --git a/Test/QuickSpec/Utils.hs b/Test/QuickSpec/Utils.hs deleted file mode 100644 --- a/Test/QuickSpec/Utils.hs +++ /dev/null @@ -1,50 +0,0 @@ --- | Miscellaneous utility functions. - -module Test.QuickSpec.Utils where - -import Control.Arrow((&&&)) -import Data.List(groupBy, sortBy, group, sort) -import Data.Ord(comparing) -import System.IO -import Control.Exception -import Control.Spoon - -repeatM :: Monad m => m a -> m [a] -repeatM = sequence . repeat - -partitionBy :: Ord b => (a -> b) -> [a] -> [[a]] -partitionBy value = map (map fst) . groupBy (\x y -> snd x == snd y) . sortBy (comparing snd) . map (id &&& value) - -isSorted :: Ord a => [a] -> Bool -isSorted xs = and (zipWith (<=) xs (tail xs)) - -isSortedBy :: Ord b => (a -> b) -> [a] -> Bool -isSortedBy f xs = isSorted (map f xs) - -usort :: Ord a => [a] -> [a] -usort = map head . group . sort - -merge :: Ord b => (a -> a -> a) -> (a -> b) -> [a] -> [a] -> [a] -merge f c = aux - where aux [] ys = ys - aux xs [] = xs - aux (x:xs) (y:ys) = - case comparing c x y of - LT -> x:aux xs (y:ys) - GT -> y:aux (x:xs) ys - EQ -> f x y:aux xs ys - -orElse :: Ordering -> Ordering -> Ordering -EQ `orElse` x = x -x `orElse` _ = x - -unbuffered :: IO a -> IO a -unbuffered x = do - buf <- hGetBuffering stdout - bracket_ - (hSetBuffering stdout NoBuffering) - (hSetBuffering stdout buf) - x - -spoony :: Eq a => a -> Maybe a -spoony x = teaspoon ((x == x) `seq` x) diff --git a/Test/QuickSpec/Utils/MemoValuation.hs b/Test/QuickSpec/Utils/MemoValuation.hs deleted file mode 100644 --- a/Test/QuickSpec/Utils/MemoValuation.hs +++ /dev/null @@ -1,22 +0,0 @@ --- | Memoise the variable valuation function for terms. --- In its own module because it's packed full of dangerous features! - -{-# LANGUAGE Rank2Types #-} -module Test.QuickSpec.Utils.MemoValuation where - -import Test.QuickSpec.Term -import Test.QuickSpec.Signature -import Data.Array hiding (index) -import Data.Array.Base(unsafeAt) -import Unsafe.Coerce -import GHC.Prim -import Test.QuickSpec.Utils.Typed -import Test.QuickSpec.Utils.TypeRel - -memoValuation :: Sig -> (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) diff --git a/Test/QuickSpec/Utils/TypeMap.hs b/Test/QuickSpec/Utils/TypeMap.hs deleted file mode 100644 --- a/Test/QuickSpec/Utils/TypeMap.hs +++ /dev/null @@ -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)) diff --git a/Test/QuickSpec/Utils/TypeRel.hs b/Test/QuickSpec/Utils/TypeRel.hs deleted file mode 100644 --- a/Test/QuickSpec/Utils/TypeRel.hs +++ /dev/null @@ -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) diff --git a/Test/QuickSpec/Utils/Typeable.hs b/Test/QuickSpec/Utils/Typeable.hs deleted file mode 100644 --- a/Test/QuickSpec/Utils/Typeable.hs +++ /dev/null @@ -1,51 +0,0 @@ -{-# LANGUAGE NoMonomorphismRestriction, CPP #-} - --- | A wrapper around 'Data.Typeable', to work around: --- --- (1) The lack of an 'Ord' instance in older GHCs, --- --- (2) bug #5962 in new GHCs. - -module Test.QuickSpec.Utils.Typeable(TypeRep, T.Typeable, T.Typeable1, T.Typeable2, - typeOf, typeOf1, cast, gcast, - mkTyConApp, typeRepTyCon, splitTyConApp, - mkFunTy, unTypeRep) where - -#if __GLASGOW_HASKELL__ >= 702 -#define NEW_TYPEABLE -#endif - -import qualified Data.Typeable as T -import Data.Ord -#ifndef NEW_TYPEABLE -import System.IO.Unsafe -#endif - -newtype TypeRep = TypeRep { unTypeRep :: T.TypeRep } - -instance Eq TypeRep where - ty == ty' = - unTypeRep ty == unTypeRep ty' || - ty `compare` ty' == EQ - -#ifdef NEW_TYPEABLE -instance Ord TypeRep where - compare = comparing splitTyConApp -#else -instance Ord TypeRep where - compare = comparing (unsafePerformIO . T.typeRepKey . unTypeRep) -#endif - -instance Show TypeRep where - showsPrec p = showsPrec p . unTypeRep - -typeOf = TypeRep . T.typeOf -typeOf1 = TypeRep . T.typeOf1 -cast = T.cast -gcast = T.gcast - -mkTyConApp f xs = TypeRep (T.mkTyConApp f (map unTypeRep xs)) -typeRepTyCon = T.typeRepTyCon . unTypeRep -splitTyConApp ty = (c, map TypeRep tys) - where (c, tys) = T.splitTyConApp (unTypeRep ty) -mkFunTy lhs rhs = TypeRep (T.mkFunTy (unTypeRep lhs) (unTypeRep rhs)) diff --git a/Test/QuickSpec/Utils/Typed.hs b/Test/QuickSpec/Utils/Typed.hs deleted file mode 100644 --- a/Test/QuickSpec/Utils/Typed.hs +++ /dev/null @@ -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" diff --git a/examples/Heaps.hs b/examples/Heaps.hs --- a/examples/Heaps.hs +++ b/examples/Heaps.hs @@ -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), diff --git a/examples/Lists.hs b/examples/Lists.hs --- a/examples/Lists.hs +++ b/examples/Lists.hs @@ -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]), diff --git a/quickspec.cabal b/quickspec.cabal --- a/quickspec.cabal +++ b/quickspec.cabal @@ -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, diff --git a/src/Test/QuickSpec.hs b/src/Test/QuickSpec.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec.hs @@ -0,0 +1,87 @@ +-- | The main QuickSpec module. +-- +-- This will not make sense if you haven't seen some examples! +-- Look at , +-- or read the paper at . + +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 diff --git a/src/Test/QuickSpec/Approximate.hs b/src/Test/QuickSpec/Approximate.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Approximate.hs @@ -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 diff --git a/src/Test/QuickSpec/Equation.hs b/src/Test/QuickSpec/Equation.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Equation.hs @@ -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] diff --git a/src/Test/QuickSpec/Generate.hs b/src/Test/QuickSpec/Generate.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Generate.hs @@ -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 diff --git a/src/Test/QuickSpec/Main.hs b/src/Test/QuickSpec/Main.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Main.hs @@ -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 "" diff --git a/src/Test/QuickSpec/Prelude.hs b/src/Test/QuickSpec/Prelude.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Prelude.hs @@ -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 ] diff --git a/src/Test/QuickSpec/Reasoning/CongruenceClosure.hs b/src/Test/QuickSpec/Reasoning/CongruenceClosure.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Reasoning/CongruenceClosure.hs @@ -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 diff --git a/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs b/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs @@ -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) diff --git a/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs b/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Reasoning/PartialEquationalReasoning.hs @@ -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)) diff --git a/src/Test/QuickSpec/Reasoning/UnionFind.hs b/src/Test/QuickSpec/Reasoning/UnionFind.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Reasoning/UnionFind.hs @@ -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') diff --git a/src/Test/QuickSpec/Signature.hs b/src/Test/QuickSpec/Signature.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Signature.hs @@ -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 diff --git a/src/Test/QuickSpec/Term.hs b/src/Test/QuickSpec/Term.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Term.hs @@ -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)) diff --git a/src/Test/QuickSpec/TestTotality.hs b/src/Test/QuickSpec/TestTotality.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/TestTotality.hs @@ -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]) diff --git a/src/Test/QuickSpec/TestTree.hs b/src/Test/QuickSpec/TestTree.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/TestTree.hs @@ -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 diff --git a/src/Test/QuickSpec/Utils.hs b/src/Test/QuickSpec/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Utils.hs @@ -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) diff --git a/src/Test/QuickSpec/Utils/MemoValuation.hs b/src/Test/QuickSpec/Utils/MemoValuation.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Utils/MemoValuation.hs @@ -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) diff --git a/src/Test/QuickSpec/Utils/TypeMap.hs b/src/Test/QuickSpec/Utils/TypeMap.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Utils/TypeMap.hs @@ -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)) diff --git a/src/Test/QuickSpec/Utils/TypeRel.hs b/src/Test/QuickSpec/Utils/TypeRel.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Utils/TypeRel.hs @@ -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) diff --git a/src/Test/QuickSpec/Utils/Typeable.hs b/src/Test/QuickSpec/Utils/Typeable.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Utils/Typeable.hs @@ -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)) diff --git a/src/Test/QuickSpec/Utils/Typed.hs b/src/Test/QuickSpec/Utils/Typed.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/Utils/Typed.hs @@ -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" diff --git a/src/Test/QuickSpec/errors.h b/src/Test/QuickSpec/errors.h new file mode 100644 --- /dev/null +++ b/src/Test/QuickSpec/errors.h @@ -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))