ghc/lib/exts/AxiomTesting.lhs

   1 % -----------------------------------------------------------------------------
   2 % $Id: AxiomTesting.lhs,v 1.1 1999/10/25 05:19:22 andy Exp $
   3 %
   4 % (c) The Hugs/GHC Team 1999
   5 %
   6
   7 This is a testing framework for using axiomatic like specifications
   8 of equalities.
   9
  10 \begin{code}
  11 module AxiomTesting (
  12         TestM,          -- abstract
  13         (&&&),
  14         (|||),
  15         funVar,
  16         displayVars,
  17         testRules,
  18         var,
  19         vars,
  20         ALPHA, BETA, GAMMA,
  21         EqALPHA, OrdALPHA,
  22         testAssoc,
  23         -- advanced user functions below
  24         Example(..),
  25         testComplete,
  26         testFail,
  27         bottom,
  28         bottomExample,
  29         ) where
  30
  31 import Monad
  32 import IO
  33 import List
  34 import IOExts
  35 import Exception (tryAll)
  36 import IOExts    (unsafePtrEq)
  37
  38 infix  4 <==>
  39 infixl 3 &&&
  40 infixl 2 |||
  41
  42 ------------------------------------------------------------------------------
  43
  44 newtype TestM a = TestM { runTestM :: TestMState -> IO (TestMResult a) }
  45
  46 data TestMState = TestMState {
  47         uniqIds        :: IORef Int,
  48         bindingPairs :: [(String,String)]
  49         }
  50
  51 initTestMState ref = TestMState {
  52         uniqIds = ref,
  53         bindingPairs = []
  54         }
  55
  56 data TestMResult a
  57         = TestMComplete !Int
  58         | TestMFail TestMState
  59         | TestMOk [(a,TestMState)]
  60
  61 runTestsM :: (a -> TestM b) -> [(a,TestMState)]
  62                 -> [(b,TestMState)] -> Int -> IO (TestMResult b)
  63 runTestsM f [] [] n = return (TestMComplete n)
  64 runTestsM f [] xs n = return (TestMOk xs)
  65 runTestsM f ((a,s):as) ys n =
  66     do r <- runTestM (f a) s
  67        case r of
  68           (TestMFail _)     -> return r
  69           (TestMComplete m) -> runTestsM f as ys (n+m)
  70           (TestMOk xs)      -> runTestsM f as (xs++ys) n
  71
  72 instance Monad TestM where
  73    return v  = TestM (\ b -> return (TestMOk [(v,b)]))
  74    p  >>= f  = TestM (\ b ->
  75                   do res <- runTestM p b
  76                      case res of
  77                           (TestMComplete m) -> return (TestMComplete m)
  78                           (TestMFail f) -> return (TestMFail f)
  79                           -- The following pattern is an optimization
  80                           TestMOk [(x,s)] -> runTestM (f x) s
  81                           TestMOk xs -> runTestsM f xs [] 0)
  82
  83 runIOTestM :: IO a -> TestM a
  84 runIOTestM m = TestM (\ b -> do { r <- m ; return (TestMOk [(r,b)]) })
  85
  86 testComplete = TestM (\ b -> return (TestMComplete 1))
  87 testFail     = TestM (\ b -> return (TestMFail b))
  88
  89
  90 oneTest :: TestM () -> TestM ()
  91 oneTest p =
  92   TestM (\ b -> do r <- runTestM p b
  93                    case r of
  94                       (TestMComplete n) -> return (TestMComplete 1)
  95                       other             -> return other)
  96
  97 {-
  98  - This also has the nice effect of stoping the bindings
  99  - of vars escaping for each side of the test.
 100  - This is why (>>=) does not have this semantics.
 101  -
 102  -}
 103
 104 (&&&) :: TestM () -> TestM () -> TestM ()
 105 (&&&) p q =
 106   TestM (\ b -> do r <- runTestM p b
 107                    case r of
 108                       (TestMComplete n) ->
 109                         do r2 <- runTestM q b
 110                            case r2 of
 111                              (TestMComplete m) -> return (TestMComplete (n+m))
 112                              other -> return other
 113                       (TestMFail _) -> return r
 114                       _ -> return (error "&&& failed"))
 115
 116
 117 (|||) :: TestM () -> TestM () -> TestM ()
 118 (|||) p q =
 119   TestM (\ b -> do r <- runTestM p b
 120                    case r of
 121                       (TestMComplete n) -> return r
 122                       (TestMFail _) -> runTestM q b
 123                       _ -> return (error "||| failed"))
 124
 125 pairUp :: String -> [(a,String)] -> TestM a
 126 pairUp name pairs =
 127    TestM (\ b ->
 128         do return (TestMOk [
 129                         (a,b { bindingPairs = (name,r) : bindingPairs b })
 130                                 | (a,r) <- pairs ]))
 131
 132 funVar :: String -> String -> TestM ()
 133 funVar name r = pairUp name [((),r)]
 134
 135 uniqId :: TestM Int
 136 uniqId = TestM (\ s ->
 137         do v <- readIORef (uniqIds s)
 138            let v' = v + 1
 139            writeIORef (uniqIds s) v'
 140            return (TestMOk [(v',s)]))
 141 {-
 142  - For debugging, you can make the monad display each binding
 143  - it is using.
 144  -}
 145 displayVars  :: TestM ()
 146 displayVars = TestM (\ s ->
 147         do putStr "\n"
 148            sequence_ [putStr ("    **    " ++ k ++ " = " ++ v ++ "\n")
 149                         | (k,v) <- reverse (bindingPairs s) ]
 150            return (TestMOk [((),s)]))
 151
 152 ------------------------------------------------------------------------------
 153 {-
 154  - This function lets you test a list of rules
 155  - about a specific function.
 156  -}
 157
 158 testRules :: String -> [TestM ()] -> IO ()
 159 testRules name actions =
 160   do putStr (rjustify 25 name ++ " : ")
 161      f <- tr 1 actions [] 0
 162      mapM fa f
 163      return ()
 164   where
 165         rjustify n s = replicate (max 0 (n - length s)) ' ' ++ s
 166
 167         tr n [] [] c = do {
 168                 putStr (rjustify (45 - n) (" (" ++ show c ++ ")\n")) ;
 169                 return [] }
 170         tr n [] xs c = do { putStr ("\n")  ; return xs }
 171         tr n (action:actions) others c =
 172            do ref <- newIORef 0
 173               r <- runTestM action (initTestMState ref)
 174               case r of
 175                 (TestMComplete m)
 176                             -> do { putStr "." ;
 177                                     tr (n+1) actions others (c+m) }
 178                 TestMFail f -> do { putStr "#" ;
 179                                    tr (n+1) actions ((n,f):others) c}
 180                 _           -> do { putStr "?" ; tr (n+1) actions others  c}
 181
 182
 183         fa (n,f) =
 184           do putStr "\n"
 185              putStr ("    ** test "
 186                         ++ show n
 187                         ++ " of "
 188                         ++ name
 189                         ++ " failed with the binding(s)\n")
 190              sequence_ [putStr ("    **    " ++ k ++ " = " ++ v ++ "\n")
 191                         | (k,v) <- reverse (bindingPairs f) ]
 192              putStr "\n"
 193
 194 var :: (Example a) => String -> TestM a
 195 var name =
 196        do pairs <- getVars
 197           pairUp name pairs
 198
 199 vars :: (Example a,Show a) => String -> [a] -> TestM a
 200 vars name as =
 201        do pairUp name [(a,show a) | a <- as ]
 202
 203 ------------------------------------------------------------------------------
 204
 205 class Example a where
 206         -- A list of examples of values at this type.
 207         getVars :: TestM [(a,String)]
 208
 209         -- A version of equality, where _|_ == _|_ ==> True, not _|_
 210
 211         (<==>) :: a -> a -> TestM ()
 212         (<==>) a b =
 213               do r <- runIOTestM (magicTest a b)
 214                  case r of
 215                    Same        -> testComplete
 216                    PerhapsSame -> oneTest (a `equ` b)
 217                    Different   -> testFail
 218
 219         isFinite :: a -> TestM ()
 220         isFinite a =
 221                do r <- runIOTestM (magicTest a bottom)
 222                   case r of
 223                         -- If this is _|_, then this check
 224                         -- is over, because this guard is not met.
 225                         -- but we return success, because the
 226                         -- overall problem was ok.
 227                         -- returning "return ()" whould
 228                         -- continue the test.
 229                         -- (A bit like F => ? ==> T)
 230                     Same -> testComplete
 231                     _    -> isFiniteSpine a
 232
 233         -- protected, use only for defintions of things.
 234         equ :: a -> a -> TestM ()
 235         equ _ _ = testFail
 236
 237         isFiniteSpine :: a -> TestM ()
 238         isFiniteSpine _ = return ()
 239
 240 data BotCmp = Same | PerhapsSame | Different
 241
 242 ------------------------------------------------------------------------------
 243 -- All the compile specific parts are captured inside
 244 -- the function magicTest.
 245
 246 #if __HUGS__
 247
 248 -- Old, Classic Hugs version
 249 primitive catchError :: a -> Maybe a
 250
 251 magicTest :: a -> a -> IO BotCmp
 252 magicTest a b =
 253    if unsafePtrEq a b then return Same
 254    else case (catchError a,catchError b) of
 255                 (Nothing,Nothing) -> return Same
 256                 (Just a,Just b)   -> return PerhapsSame
 257                 _                 -> return Different
 258
 259
 260 #else
 261
 262 magicTest :: a -> a -> IO BotCmp
 263 magicTest a b =
 264    if unsafePtrEq a b then return Same
 265    else do a' <- tryAll a
 266            b' <- tryAll b
 267            case (a',b') of
 268                 (Left _,Left _)   -> return Same
 269                 (Right _,Right _) -> return PerhapsSame
 270                 _                 -> return Different
 271
 272 #endif
 273 ------------------------------------------------------------------------------
 274
 275 bottom = error "bottom"
 276 bottomExample = [(bottom,"_|_")]
 277
 278 cmp a b = if (a == b) then testComplete else testFail
 279
 280 render :: (Show a) => [a] -> [(a,String)]
 281 render as = [ (a,show a) | a <- as ]
 282
 283 instance Example Char    where
 284         getVars = return (render ['a','z'] ++ bottomExample)
 285         equ a b = cmp a b
 286
 287 instance Example Float   where
 288         getVars = return (render [0.0,1.0,999.0] ++ bottomExample)
 289         equ a b = cmp a b
 290
 291 instance Example Double  where
 292         getVars = return (render [0.0,1.0,999.0] ++ bottomExample)
 293         equ a b = cmp a b
 294
 295 instance Example Integer where
 296         getVars = return (render [-1,1,1] ++ bottomExample)
 297         equ a b = cmp a b
 298
 299 instance Example ()      where
 300         getVars = return (render [()] ++ bottomExample)
 301         equ a b = cmp a b
 302
 303 instance Example Int     where
 304         getVars = return (render [0,1,2,minBound,maxBound] ++ bottomExample)
 305         equ a b = cmp a b
 306
 307 instance Example Bool    where
 308         getVars = return (render [True,False] ++ bottomExample)
 309         equ a b = cmp a b
 310
 311 instance Example a => Example [a] where
 312         getVars =
 313             do e1 <- getVars
 314                e2 <- getVars
 315                return (
 316                   concat [ [ ([e],"[" ++ t ++ "]"),
 317                              (e:bottom,t ++ ":_|_") ]
 318                                          | (e,t) <- e1 ]
 319                 ++ [ ([e1,e2],
 320                       "[" ++ t1 ++ "," ++ t2 ++ "]")
 321                          | (e1,t1) <- e1, (e2,t2) <- e2 ]
 322                 ++ [ ([e1,e2,e1],
 323                       "[" ++ t1 ++ "," ++ t2 ++ "," ++ t1 ++ "]")
 324                          | (e1,t1) <- e1, (e2,t2) <- e2 ]
 325                 ++ [ ([],"[]")]
 326                 ++ bottomExample)
 327
 328         equ []     []     = testComplete
 329         equ (a:as) (b:bs) = (a <==> b) &&& (as <==> bs)
 330         equ _      _      = testFail
 331
 332         isFiniteSpine []     = return ()
 333         isFiniteSpine (_:xs) = isFinite xs
 334
 335 instance Example a => Example (Maybe a) where
 336         getVars =
 337             do e1 <- getVars
 338                return (
 339                   [ (Just e,"Just " ++ t)
 340                                 | (e,t) <- e1 ]
 341                 ++ [ (Nothing,"Nothing")]
 342                 ++ bottomExample)
 343
 344         equ Nothing  Nothing     = testComplete
 345         equ (Just a) (Just b) = a <==> b
 346         equ _      _      = testFail
 347
 348         isFiniteSpine Nothing  = return ()
 349         isFiniteSpine (Just _) = return ()
 350
 351 ------------------------------------------------------------------------------
 352
 353 {- We pick something isomorphic to ints because of the
 354  - shape of the domain.
 355  -
 356  -       ... -1  0  1 ...
 357  -             \ | /
 358  -              \ /
 359  -              _|_
 360  -}
 361
 362 class PolyExample a where
 363         mkPoly   :: Int -> a
 364         unPoly   :: a -> Int
 365         namePoly :: a -> String
 366
 367         equPoly :: a -> a -> TestM ()
 368         equPoly a b = (unPoly a) <==> (unPoly b)
 369
 370         getPolyVars :: TestM [(a,String)]
 371         getPolyVars =
 372           do n <- uniqId
 373              return ([mkPair (mkPoly 0) 0,
 374                      mkPair (mkPoly n) n] ++ bottomExample)
 375           where
 376             mkPair a n = (a,namePoly a ++ "_" ++ show n)
 377
 378 ------------------------------------------------------------------------------
 379
 380 newtype ALPHA = ALPHA { unALPHA :: Int }
 381
 382 instance PolyExample ALPHA where
 383         mkPoly = ALPHA
 384         unPoly = unALPHA
 385         namePoly = const "a"
 386
 387 instance Example ALPHA where { equ = equPoly ; getVars = getPolyVars }
 388
 389 newtype BETA = BETA { unBETA :: Int }
 390
 391 instance PolyExample BETA where
 392         mkPoly = BETA
 393         unPoly = unBETA
 394         namePoly = const "b"
 395
 396 instance Example BETA where { equ = equPoly ; getVars = getPolyVars }
 397
 398 newtype GAMMA = GAMMA { unGAMMA :: Int }
 399
 400 instance PolyExample GAMMA where
 401         mkPoly = GAMMA
 402         unPoly = unGAMMA
 403         namePoly = const "c"
 404
 405 instance Example GAMMA where { equ = equPoly ; getVars = getPolyVars }
 406
 407 newtype EqALPHA = EqALPHA { unEqALPHA :: Int }
 408         deriving (Eq)
 409
 410 instance PolyExample EqALPHA where
 411         mkPoly = EqALPHA
 412         unPoly = unEqALPHA
 413         namePoly = const "a"
 414
 415 instance Example EqALPHA where { equ = equPoly ; getVars = getPolyVars }
 416
 417 newtype OrdALPHA = OrdALPHA { unOrdALPHA :: Int }
 418         deriving (Eq,Ord)
 419
 420 instance PolyExample OrdALPHA where
 421         mkPoly = OrdALPHA
 422         unPoly = unOrdALPHA
 423         namePoly = const "b"
 424
 425 instance Example OrdALPHA where { equ = equPoly ; getVars = getPolyVars }
 426
 427 ------------------------------------------------------------------------------
 428 -- More Utilities
 429
 430 testAssoc :: (Example a) => (a -> a -> a) -> TestM ()
 431 testAssoc fn =
 432    do x <- var "x"
 433       y <- var "y"
 434       z <- var "z"
 435       ((x `fn` (y `fn` z)) <==> ((x `fn` y) `fn` z))
 436
 437 ------------------------------------------------------------------------------
 438 \end{code}
 439
 440 Example specifications. They all have type IO ().
 441
 442 test_concat = testRules "concat" [
 443         do (xss :: [[ALPHA]]) <- var "xss"
 444            concat xss <==> foldr (++) [] xss
 445         ]
 446
 447 test_head = testRules "head" [
 448         let def_head (x:_) = x
 449             def_head []    = error ""
 450         in do (xs  :: [ALPHA]) <- var "xs"
 451               head xs <==> def_head xs
 452         ]
 453
 454 test_sort = testRules "sort" [
 455         do (xs :: [OrdALPHA]) <- var "xs"
 456            sort xs <==> sortBy compare xs,
 457         do (xs :: [OrdALPHA]) <- var "xs"
 458            head (sort xs) <==> minimum xs,
 459         do (xs :: [OrdALPHA]) <- var "xs"
 460            last (sort xs) <==> maximum xs,
 461         do (xs :: [OrdALPHA]) <- var "xs"
 462            (ys :: [OrdALPHA]) <- var "ys"
 463            (null xs <==> True)
 464              ||| (null ys <==> True)
 465              ||| (head (sort (xs ++ ys)) <==> min (minimum xs) (minimum ys)),
 466         do (xs :: [OrdALPHA]) <- var "xs"
 467            (ys :: [OrdALPHA]) <- var "ys"
 468            (null xs <==> True)
 469              ||| (null ys <==> True)
 470              ||| (last (sort (xs ++ ys)) <==> max (maximum xs) (maximum ys))
 471         ]
 472
 473 test_map = testRules "map" [
 474         let def_map f [] = []
 475             def_map f (x:xs) = f x : def_map f xs
 476             test f fn =
 477                 do funVar "f" fn
 478                    xs   <- var "xs"
 479                    map f xs <==> def_map f xs
 480         in
 481                 test (id :: ALPHA -> ALPHA)
 482                     "id"
 483             &&& test ((\ a -> a + 1) :: Int -> Int)
 484                       "\\ a -> a + 1"
 485             &&& test ((\ a -> bottom) :: Int -> Int)
 486                       "\\ a -> _|_",
 487         do (xs :: [ALPHA]) <- var "xs"
 488            xs <==> map id xs
 489         ]
 490
 491 test_int_plus = testRules "(+)::Int->Int->Int" [
 492         testAssoc ((+) :: Int -> Int -> Int)
 493         ]