[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

1 files changed, 493 insertions, 0 deletions

diff --git a/ghc/lib/exts/AxiomTesting.lhs b/ghc/lib/exts/AxiomTesting.lhs
new file mode 100644
index 0000000000..e9b672149d
--- /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)
+	]