From 148227dc4e67d89a2036251ef3ad72fed1e44c0f Mon Sep 17 00:00:00 2001 From: andy Date: Mon, 25 Oct 1999 05:19:22 +0000 Subject: [PATCH] [project @ 1999-10-25 05:19:22 by andy] Adding a axiomatic testing framework library to help test Hugs and GHC libraries. Here is the example for the test of concat. test_concat = testRules "concat" [ do (xss :: [[ALPHA]]) <- var "xss" concat xss <==> foldr (++) [] xss ] xss here ranges over various rendering of list of list, including bottom and lists containing bottom. <==> uses a small piece of compiler/interpreter specifics to allow testing for error "" ... <==> ... error "" ===> Pass --- ghc/lib/exts/AxiomTesting.lhs | 493 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 493 insertions(+) create mode 100644 ghc/lib/exts/AxiomTesting.lhs diff --git a/ghc/lib/exts/AxiomTesting.lhs b/ghc/lib/exts/AxiomTesting.lhs new file mode 100644 index 0000000..e9b6721 --- /dev/null +++ b/ghc/lib/exts/AxiomTesting.lhs @@ -0,0 +1,493 @@ +% ----------------------------------------------------------------------------- +% $Id: AxiomTesting.lhs,v 1.1 1999/10/25 05:19:22 andy Exp $ +% +% (c) The Hugs/GHC Team 1999 +% + +This is a testing framework for using axiomatic like specifications +of equalities. + +\begin{code} +module AxiomTesting ( + TestM, -- abstract + (&&&), + (|||), + funVar, + displayVars, + testRules, + var, + vars, + ALPHA, BETA, GAMMA, + EqALPHA, OrdALPHA, + testAssoc, + -- advanced user functions below + Example(..), + testComplete, + testFail, + bottom, + bottomExample, + ) where + +import Monad +import IO +import List +import IOExts +import Exception (tryAll) +import IOExts (unsafePtrEq) + +infix 4 <==> +infixl 3 &&& +infixl 2 ||| + +------------------------------------------------------------------------------ + +newtype TestM a = TestM { runTestM :: TestMState -> IO (TestMResult a) } + +data TestMState = TestMState { + uniqIds :: IORef Int, + bindingPairs :: [(String,String)] + } + +initTestMState ref = TestMState { + uniqIds = ref, + bindingPairs = [] + } + +data TestMResult a + = TestMComplete !Int + | TestMFail TestMState + | TestMOk [(a,TestMState)] + +runTestsM :: (a -> TestM b) -> [(a,TestMState)] + -> [(b,TestMState)] -> Int -> IO (TestMResult b) +runTestsM f [] [] n = return (TestMComplete n) +runTestsM f [] xs n = return (TestMOk xs) +runTestsM f ((a,s):as) ys n = + do r <- runTestM (f a) s + case r of + (TestMFail _) -> return r + (TestMComplete m) -> runTestsM f as ys (n+m) + (TestMOk xs) -> runTestsM f as (xs++ys) n + +instance Monad TestM where + return v = TestM (\ b -> return (TestMOk [(v,b)])) + p >>= f = TestM (\ b -> + do res <- runTestM p b + case res of + (TestMComplete m) -> return (TestMComplete m) + (TestMFail f) -> return (TestMFail f) + -- The following pattern is an optimization + TestMOk [(x,s)] -> runTestM (f x) s + TestMOk xs -> runTestsM f xs [] 0) + +runIOTestM :: IO a -> TestM a +runIOTestM m = TestM (\ b -> do { r <- m ; return (TestMOk [(r,b)]) }) + +testComplete = TestM (\ b -> return (TestMComplete 1)) +testFail = TestM (\ b -> return (TestMFail b)) + + +oneTest :: TestM () -> TestM () +oneTest p = + TestM (\ b -> do r <- runTestM p b + case r of + (TestMComplete n) -> return (TestMComplete 1) + other -> return other) + +{- + - This also has the nice effect of stoping the bindings + - of vars escaping for each side of the test. + - This is why (>>=) does not have this semantics. + - + -} + +(&&&) :: TestM () -> TestM () -> TestM () +(&&&) p q = + TestM (\ b -> do r <- runTestM p b + case r of + (TestMComplete n) -> + do r2 <- runTestM q b + case r2 of + (TestMComplete m) -> return (TestMComplete (n+m)) + other -> return other + (TestMFail _) -> return r + _ -> return (error "&&& failed")) + + +(|||) :: TestM () -> TestM () -> TestM () +(|||) p q = + TestM (\ b -> do r <- runTestM p b + case r of + (TestMComplete n) -> return r + (TestMFail _) -> runTestM q b + _ -> return (error "||| failed")) + +pairUp :: String -> [(a,String)] -> TestM a +pairUp name pairs = + TestM (\ b -> + do return (TestMOk [ + (a,b { bindingPairs = (name,r) : bindingPairs b }) + | (a,r) <- pairs ])) + +funVar :: String -> String -> TestM () +funVar name r = pairUp name [((),r)] + +uniqId :: TestM Int +uniqId = TestM (\ s -> + do v <- readIORef (uniqIds s) + let v' = v + 1 + writeIORef (uniqIds s) v' + return (TestMOk [(v',s)])) +{- + - For debugging, you can make the monad display each binding + - it is using. + -} +displayVars :: TestM () +displayVars = TestM (\ s -> + do putStr "\n" + sequence_ [putStr (" ** " ++ k ++ " = " ++ v ++ "\n") + | (k,v) <- reverse (bindingPairs s) ] + return (TestMOk [((),s)])) + +------------------------------------------------------------------------------ +{- + - This function lets you test a list of rules + - about a specific function. + -} + +testRules :: String -> [TestM ()] -> IO () +testRules name actions = + do putStr (rjustify 25 name ++ " : ") + f <- tr 1 actions [] 0 + mapM fa f + return () + where + rjustify n s = replicate (max 0 (n - length s)) ' ' ++ s + + tr n [] [] c = do { + putStr (rjustify (45 - n) (" (" ++ show c ++ ")\n")) ; + return [] } + tr n [] xs c = do { putStr ("\n") ; return xs } + tr n (action:actions) others c = + do ref <- newIORef 0 + r <- runTestM action (initTestMState ref) + case r of + (TestMComplete m) + -> do { putStr "." ; + tr (n+1) actions others (c+m) } + TestMFail f -> do { putStr "#" ; + tr (n+1) actions ((n,f):others) c} + _ -> do { putStr "?" ; tr (n+1) actions others c} + + + fa (n,f) = + do putStr "\n" + putStr (" ** test " + ++ show n + ++ " of " + ++ name + ++ " failed with the binding(s)\n") + sequence_ [putStr (" ** " ++ k ++ " = " ++ v ++ "\n") + | (k,v) <- reverse (bindingPairs f) ] + putStr "\n" + +var :: (Example a) => String -> TestM a +var name = + do pairs <- getVars + pairUp name pairs + +vars :: (Example a,Show a) => String -> [a] -> TestM a +vars name as = + do pairUp name [(a,show a) | a <- as ] + +------------------------------------------------------------------------------ + +class Example a where + -- A list of examples of values at this type. + getVars :: TestM [(a,String)] + + -- A version of equality, where _|_ == _|_ ==> True, not _|_ + + (<==>) :: a -> a -> TestM () + (<==>) a b = + do r <- runIOTestM (magicTest a b) + case r of + Same -> testComplete + PerhapsSame -> oneTest (a `equ` b) + Different -> testFail + + isFinite :: a -> TestM () + isFinite a = + do r <- runIOTestM (magicTest a bottom) + case r of + -- If this is _|_, then this check + -- is over, because this guard is not met. + -- but we return success, because the + -- overall problem was ok. + -- returning "return ()" whould + -- continue the test. + -- (A bit like F => ? ==> T) + Same -> testComplete + _ -> isFiniteSpine a + + -- protected, use only for defintions of things. + equ :: a -> a -> TestM () + equ _ _ = testFail + + isFiniteSpine :: a -> TestM () + isFiniteSpine _ = return () + +data BotCmp = Same | PerhapsSame | Different + +------------------------------------------------------------------------------ +-- All the compile specific parts are captured inside +-- the function magicTest. + +#if __HUGS__ + +-- Old, Classic Hugs version +primitive catchError :: a -> Maybe a + +magicTest :: a -> a -> IO BotCmp +magicTest a b = + if unsafePtrEq a b then return Same + else case (catchError a,catchError b) of + (Nothing,Nothing) -> return Same + (Just a,Just b) -> return PerhapsSame + _ -> return Different + + +#else + +magicTest :: a -> a -> IO BotCmp +magicTest a b = + if unsafePtrEq a b then return Same + else do a' <- tryAll a + b' <- tryAll b + case (a',b') of + (Left _,Left _) -> return Same + (Right _,Right _) -> return PerhapsSame + _ -> return Different + +#endif +------------------------------------------------------------------------------ + +bottom = error "bottom" +bottomExample = [(bottom,"_|_")] + +cmp a b = if (a == b) then testComplete else testFail + +render :: (Show a) => [a] -> [(a,String)] +render as = [ (a,show a) | a <- as ] + +instance Example Char where + getVars = return (render ['a','z'] ++ bottomExample) + equ a b = cmp a b + +instance Example Float where + getVars = return (render [0.0,1.0,999.0] ++ bottomExample) + equ a b = cmp a b + +instance Example Double where + getVars = return (render [0.0,1.0,999.0] ++ bottomExample) + equ a b = cmp a b + +instance Example Integer where + getVars = return (render [-1,1,1] ++ bottomExample) + equ a b = cmp a b + +instance Example () where + getVars = return (render [()] ++ bottomExample) + equ a b = cmp a b + +instance Example Int where + getVars = return (render [0,1,2,minBound,maxBound] ++ bottomExample) + equ a b = cmp a b + +instance Example Bool where + getVars = return (render [True,False] ++ bottomExample) + equ a b = cmp a b + +instance Example a => Example [a] where + getVars = + do e1 <- getVars + e2 <- getVars + return ( + concat [ [ ([e],"[" ++ t ++ "]"), + (e:bottom,t ++ ":_|_") ] + | (e,t) <- e1 ] + ++ [ ([e1,e2], + "[" ++ t1 ++ "," ++ t2 ++ "]") + | (e1,t1) <- e1, (e2,t2) <- e2 ] + ++ [ ([e1,e2,e1], + "[" ++ t1 ++ "," ++ t2 ++ "," ++ t1 ++ "]") + | (e1,t1) <- e1, (e2,t2) <- e2 ] + ++ [ ([],"[]")] + ++ bottomExample) + + equ [] [] = testComplete + equ (a:as) (b:bs) = (a <==> b) &&& (as <==> bs) + equ _ _ = testFail + + isFiniteSpine [] = return () + isFiniteSpine (_:xs) = isFinite xs + +instance Example a => Example (Maybe a) where + getVars = + do e1 <- getVars + return ( + [ (Just e,"Just " ++ t) + | (e,t) <- e1 ] + ++ [ (Nothing,"Nothing")] + ++ bottomExample) + + equ Nothing Nothing = testComplete + equ (Just a) (Just b) = a <==> b + equ _ _ = testFail + + isFiniteSpine Nothing = return () + isFiniteSpine (Just _) = return () + +------------------------------------------------------------------------------ + +{- We pick something isomorphic to ints because of the + - shape of the domain. + - + - ... -1 0 1 ... + - \ | / + - \ / + - _|_ + -} + +class PolyExample a where + mkPoly :: Int -> a + unPoly :: a -> Int + namePoly :: a -> String + + equPoly :: a -> a -> TestM () + equPoly a b = (unPoly a) <==> (unPoly b) + + getPolyVars :: TestM [(a,String)] + getPolyVars = + do n <- uniqId + return ([mkPair (mkPoly 0) 0, + mkPair (mkPoly n) n] ++ bottomExample) + where + mkPair a n = (a,namePoly a ++ "_" ++ show n) + +------------------------------------------------------------------------------ + +newtype ALPHA = ALPHA { unALPHA :: Int } + +instance PolyExample ALPHA where + mkPoly = ALPHA + unPoly = unALPHA + namePoly = const "a" + +instance Example ALPHA where { equ = equPoly ; getVars = getPolyVars } + +newtype BETA = BETA { unBETA :: Int } + +instance PolyExample BETA where + mkPoly = BETA + unPoly = unBETA + namePoly = const "b" + +instance Example BETA where { equ = equPoly ; getVars = getPolyVars } + +newtype GAMMA = GAMMA { unGAMMA :: Int } + +instance PolyExample GAMMA where + mkPoly = GAMMA + unPoly = unGAMMA + namePoly = const "c" + +instance Example GAMMA where { equ = equPoly ; getVars = getPolyVars } + +newtype EqALPHA = EqALPHA { unEqALPHA :: Int } + deriving (Eq) + +instance PolyExample EqALPHA where + mkPoly = EqALPHA + unPoly = unEqALPHA + namePoly = const "a" + +instance Example EqALPHA where { equ = equPoly ; getVars = getPolyVars } + +newtype OrdALPHA = OrdALPHA { unOrdALPHA :: Int } + deriving (Eq,Ord) + +instance PolyExample OrdALPHA where + mkPoly = OrdALPHA + unPoly = unOrdALPHA + namePoly = const "b" + +instance Example OrdALPHA where { equ = equPoly ; getVars = getPolyVars } + +------------------------------------------------------------------------------ +-- More Utilities + +testAssoc :: (Example a) => (a -> a -> a) -> TestM () +testAssoc fn = + do x <- var "x" + y <- var "y" + z <- var "z" + ((x `fn` (y `fn` z)) <==> ((x `fn` y) `fn` z)) + +------------------------------------------------------------------------------ +\end{code} + +Example specifications. They all have type IO (). + +test_concat = testRules "concat" [ + do (xss :: [[ALPHA]]) <- var "xss" + concat xss <==> foldr (++) [] xss + ] + +test_head = testRules "head" [ + let def_head (x:_) = x + def_head [] = error "" + in do (xs :: [ALPHA]) <- var "xs" + head xs <==> def_head xs + ] + +test_sort = testRules "sort" [ + do (xs :: [OrdALPHA]) <- var "xs" + sort xs <==> sortBy compare xs, + do (xs :: [OrdALPHA]) <- var "xs" + head (sort xs) <==> minimum xs, + do (xs :: [OrdALPHA]) <- var "xs" + last (sort xs) <==> maximum xs, + do (xs :: [OrdALPHA]) <- var "xs" + (ys :: [OrdALPHA]) <- var "ys" + (null xs <==> True) + ||| (null ys <==> True) + ||| (head (sort (xs ++ ys)) <==> min (minimum xs) (minimum ys)), + do (xs :: [OrdALPHA]) <- var "xs" + (ys :: [OrdALPHA]) <- var "ys" + (null xs <==> True) + ||| (null ys <==> True) + ||| (last (sort (xs ++ ys)) <==> max (maximum xs) (maximum ys)) + ] + +test_map = testRules "map" [ + let def_map f [] = [] + def_map f (x:xs) = f x : def_map f xs + test f fn = + do funVar "f" fn + xs <- var "xs" + map f xs <==> def_map f xs + in + test (id :: ALPHA -> ALPHA) + "id" + &&& test ((\ a -> a + 1) :: Int -> Int) + "\\ a -> a + 1" + &&& test ((\ a -> bottom) :: Int -> Int) + "\\ a -> _|_", + do (xs :: [ALPHA]) <- var "xs" + xs <==> map id xs + ] + +test_int_plus = testRules "(+)::Int->Int->Int" [ + testAssoc ((+) :: Int -> Int -> Int) + ] -- 1.7.10.4