ChasingBottoms 1.2.4 → 1.3.0

raw patch · 25 files changed

+275/−352 lines, 25 filesdep +arraydep +sybdep ~QuickCheckdep ~basedep ~containersnew-component:exe:ChasingBottomsTestSuitePVP ok

version bump matches the API change (PVP)

Dependencies added: array, syb

Dependency ranges changed: QuickCheck, base, containers, mtl, random

API changes (from Hackage documentation)

Files

• .boring +0/−9
• ChasingBottoms.cabal +45/−29
• LICENCE +1/−1
• Makefile +0/−24
• README +0/−28
• Test/ChasingBottoms.hs +3/−15
• Test/ChasingBottoms/Approx.hs +8/−8
• Test/ChasingBottoms/Approx/Tests.hs +2/−1
• Test/ChasingBottoms/ApproxShow.hs +8/−12
• Test/ChasingBottoms/ApproxShow/Tests.hs +1/−1
• Test/ChasingBottoms/ContinuousFunctions.hs +32/−37
• Test/ChasingBottoms/ContinuousFunctions/Tests.hs +21/−23
• Test/ChasingBottoms/IsBottom.hs +52/−40
• Test/ChasingBottoms/IsBottom.hs-boot +3/−0
• Test/ChasingBottoms/IsBottom/Tests.hs +4/−1
• Test/ChasingBottoms/IsType.hs +5/−5
• Test/ChasingBottoms/Nat.hs +14/−9
• Test/ChasingBottoms/Nat/Tests.hs +1/−2
• Test/ChasingBottoms/SemanticOrd.hs +6/−5
• Test/ChasingBottoms/SemanticOrd/Tests.hs +1/−2
• Test/ChasingBottoms/TestLibraryWhenCompiling.hs +0/−21
• Test/ChasingBottoms/TestUtilities.hs +27/−45
• Test/ChasingBottoms/TestUtilities/Generators.hs +4/−5
• Test/ChasingBottoms/Tests.hs +2/−2
• Test/ChasingBottoms/TimeOut.hs +35/−27

@@ -1,9 +0,0 @@-(^|/)_darcs($|/)-^docs$-^dist$-^ChasingBottoms\.tar\.gz$-\..*-config$-\.hi$-\.o$-(^|/)#.*#$-\.processed$

@@ -1,13 +1,10 @@ name:               ChasingBottoms-version:            1.2.4+version:            1.3.0 license:            OtherLicense license-file:       LICENCE-copyright:          Copyright (c) Nils Anders Danielsson 2004-2008.+copyright:          Copyright (c) Nils Anders Danielsson 2004-2010. author:             Nils Anders Danielsson maintainer:         http://www.cs.nott.ac.uk/~nad/contact.html-stability:          experimental-homepage:           http://www.cs.nott.ac.uk/~nad/software/#Chasing Bottoms-package-url:        http://www.cs.nott.ac.uk/~nad/software/ChasingBottoms/ChasingBottoms.tgz synopsis:           For testing partial and infinite values. description:   Do you ever feel the need to test code involving bottoms (e.g. calls to@@ -59,9 +56,9 @@   computations, such as the following example, and then it can be nice to   be able to apply a time-out:   .-    [@> timeOut' 1 (reverse [1..5\]) >>= print@] @Value [5,4,3,2,1]@+    [@> timeOut' 1 (reverse [1..5\])@] @Value [5,4,3,2,1]@   .-    [@> timeOut' 1 (reverse [1..\]) >>= print@] @NonTermination@+    [@> timeOut' 1 (reverse [1..\])@] @NonTermination@   .   The time-out functionality can be used to treat \"slow\" computations as   bottoms:@@ -84,34 +81,29 @@   .     [@> let primes = unfoldr (\\(x:xs) -> Just (x, filter ((\/= 0) . (\`mod\` x)) xs)) [2..\]@]   .-    [@> timeOutMicro 100 (print $ filter ((== 1) . (\`mod\` 83)) primes) >>= print@] @[167,499NonTermination@+    [@> timeOutMicro 100 (print $ filter ((== 1) . (\`mod\` 83)) primes)@] @[167,499,9NonTermination@   .-    [@> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (\`mod\` 83)) primes) >>= print@] @[167,499,997NonTermination@+    [@> timeOutMicro 100 (print $ take 6 $ filter ((== 1) . (\`mod\` 83)) primes)@] @[167,499,997,1163,1993NonTermination@   .-    [@> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (\`mod\` 83)) primes) >>= print@] @[167,499,997,1163]@+    [@> timeOutMicro 100 (print $ take 6 $ filter ((== 1) . (\`mod\` 83)) primes)@] @[167,499,997,1163,1993,2657]@   .     [@ @] @Value ()@   .-  All the type annotations above are required.-  .   For the underlying theory and a larger example involving use of   QuickCheck, see the article \"Chasing Bottoms, A Case Study in Program   Verification in the Presence of Partial and Infinite Values\"   (<http://www.cs.nott.ac.uk/~nad/publications/danielsson-jansson-mpc2004.html>).   .-  The code has been tested under GHC 6.8. Most parts can probably be+  The code has been tested under GHC 6.12. Most parts can probably be   ported to other Haskell compilers, but that would require some work.   The @TimeOut@ functions require preemptive scheduling, and most of the   rest requires @Data.Generics@; @isBottom@ only requires exceptions,   though. category:           Testing-tested-with:        GHC == 6.8.2-cabal-version:      >= 1.2 && < 2+tested-with:        GHC == 6.12.1+cabal-version:      == 1.8.* build-type:         Simple -flag small_base-    description: Choose the new smaller, split-up base package.- library     exposed-modules:         Test.ChasingBottoms,@@ -125,15 +117,39 @@      other-modules: Test.ChasingBottoms.IsType -    build-depends: QuickCheck >= 1.1 && < 2,-                   mtl >= 1.1 && < 2-    if flag(small_base)-        build-depends: base >= 3 && < 4,-                       containers >= 0.1 && < 1,-                       random >= 1 && < 2-    else-        build-depends: base >= 2 && < 3+    build-depends: QuickCheck == 2.1.*,+                   mtl == 1.1.*,+                   base == 4.*,+                   containers == 0.3.*,+                   random == 1.0.*,+                   syb >= 0.1.0.2 && < 0.2 --- It would be nice if the tests that can be accessed through--- Test.ChasingBottoms.Tests.main could be run automatically using--- Cabal (in a simple way). See make test.+flag build-tests+    description: Build the test suite.+    default:     False+    manual:      True++executable ChasingBottomsTestSuite+    if !flag(build-tests)+      buildable:   False++    main-is:       Test/ChasingBottoms/Tests.hs++    other-modules: Test.ChasingBottoms.Approx.Tests,+                   Test.ChasingBottoms.ApproxShow.Tests,+                   Test.ChasingBottoms.ContinuousFunctions.Tests,+                   Test.ChasingBottoms.IsBottom.Tests,+                   Test.ChasingBottoms.IsType.Tests,+                   Test.ChasingBottoms.Nat.Tests,+                   Test.ChasingBottoms.SemanticOrd.Tests,+                   Test.ChasingBottoms.TestUtilities,+                   Test.ChasingBottoms.TestUtilities.Generators,+                   Test.ChasingBottoms.TimeOut.Tests++    build-depends: QuickCheck == 2.1.*,+                   mtl == 1.1.*,+                   base == 4.*,+                   containers == 0.3.*,+                   random == 1.0.*,+                   syb >= 0.1.0.2 && < 0.2,+                   array == 0.3.*

@@ -1,7 +1,7 @@ I have chosen to distribute this library under the MIT/Expat licence: --------------------------------------------------------------------- -Copyright (c) 2004-2008 Nils Anders Danielsson+Copyright (c) 2004-2010 Nils Anders Danielsson  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the

@@ -1,24 +0,0 @@-# This Makefile is currently only used to run a test suite-# automatically using darcs.--########################################################################-# You may need to edit the following variables:--# Path to GHC 6.8, used to run the tests.-GHC_68 ?= ghc--# GHC packages necessary for building and testing the library.-PACKAGES = base-3.0.1.0 containers-0.1.0.1 random-1.0.0.0 mtl-1.1.0.0	\-QuickCheck-1.1.0.0 array-0.1.0.0--########################################################################--# Runs all tests using GHC 6.8.-compile = $(1) -ignore-dot-ghci -no-recomp -hide-all-packages \-	  $(foreach pkg,$(PACKAGES),-package $(pkg)) --make $(2)-testWithCompiler = $(call compile,$(1),Test.ChasingBottoms) && $(call	\-compile,$(1),Test.ChasingBottoms.Tests -main-is				\-Test.ChasingBottoms.Tests.main -o tests) && ./tests-.PHONY : test-test:-	$(call testWithCompiler,$(GHC_68))

@@ -1,28 +0,0 @@-ChasingBottoms-----------------Building-----------To build: Use Cabal, or use ghc --make Test.ChasingBottoms. (If-Test.ChasingBottoms is already installed you may need to add something-like -ignore-package ChasingBottoms.)--Do not use Cabal to build the documentation. Use make docs instead.-You may need to edit the Makefile first.--To run through the test suite, execute Test.ChasingBottoms.Tests.main.--Possible future work-----------------------* Making it easier to test equality etc. of functions. (This may be-  easier using the new version of Scrap your boilerplate, Scrap your-  boilerplate with class.)--* More custom generators for partial and infinite values.--Known bugs-------------None.

@@ -1,9 +1,9 @@ -- | -- Module      :  Test.ChasingBottoms--- Copyright   :  (c) Nils Anders Danielsson 2004-2007+-- Copyright   :  (c) Nils Anders Danielsson 2004-2010 -- License     :  See the file LICENCE.--- --- Maintainer  :  http://www.cs.chalmers.se/~nad/+--+-- Maintainer  :  http://www.cs.nott.ac.uk/~nad/ -- Stability   :  experimental -- Portability :  non-portable (GHC-specific) --@@ -26,15 +26,3 @@ import Test.ChasingBottoms.Nat import Test.ChasingBottoms.SemanticOrd import Test.ChasingBottoms.TimeOut--{----- If this module is imported the library refuses to be built whenever--- the tests fail. Doing this adds a dependency on Template Haskell,--- though, and the compilation takes considerably longer, plus some--- (intended) warnings are emitted. Furthermore, if some test should--- fail, then the emitted error message is rather unreadable.--import Test.ChasingBottoms.TestLibraryWhenCompiling---}

@@ -1,11 +1,12 @@-{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}+{-# LANGUAGE ScopedTypeVariables,+             FlexibleInstances, UndecidableInstances #-}  -- | -- Module      :  Test.ChasingBottoms.Approx--- Copyright   :  (c) Nils Anders Danielsson 2004-2007+-- Copyright   :  (c) Nils Anders Danielsson 2004-2010 -- License     :  See the file LICENCE.--- --- Maintainer  :  http://www.cs.chalmers.se/~nad/+--+-- Maintainer  :  http://www.cs.nott.ac.uk/~nad/ -- Stability   :  experimental -- Portability :  non-portable (GHC-specific) --@@ -15,6 +16,7 @@   ) where  import Test.ChasingBottoms.Nat+import Data.Function import Data.Generics import qualified Data.List as List @@ -96,11 +98,9 @@   | otherwise = \x ->      let d = dataTypeOf x          n' = pred n-         fun childTerm = if dataTypeOf childTerm == d then+         fun childTerm = if dataTypeOf childTerm === d then                            approxGen' n' childTerm                           else                            childTerm      in gmapT fun x--instance Eq DataType where-  d1 == d2 = dataTypeRep d1 == dataTypeRep d2+    where (===) = (==) `on` dataTypeRep

@@ -1,4 +1,5 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE ScopedTypeVariables, RankNTypes,+             DeriveDataTypeable #-}  -- | Tests of the functions in "Test.ChasingBottoms.Approx". 

@@ -1,11 +1,12 @@-{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}+{-# LANGUAGE ScopedTypeVariables,+             FlexibleInstances, UndecidableInstances #-}  -- | -- Module      :  Test.ChasingBottoms.ApproxShow--- Copyright   :  (c) Nils Anders Danielsson 2004-2007+-- Copyright   :  (c) Nils Anders Danielsson 2004-2010 -- License     :  See the file LICENCE.--- --- Maintainer  :  http://www.cs.chalmers.se/~nad/+--+-- Maintainer  :  http://www.cs.nott.ac.uk/~nad/ -- Stability   :  experimental -- Portability :  non-portable (GHC-specific) --@@ -37,7 +38,7 @@   --   * All detectable occurences of bottoms are replaced by @\"_|_\"@.   --   --   * Non-bottom functions are displayed as @\"\<function \/= _|_\>\"@.-  -- +  --   approxShowsPrec :: Nat -> Prec -> a -> ShowS   approxShows     :: Nat -> a -> ShowS   approxShow      :: Nat -> a -> String@@ -109,7 +110,7 @@   | otherwise    = showParen (not (isAtom a) && p > appPrec) $                    showCon a .                    continueL (.^.) nil (succ appPrec) a-                   +     where     continueL f x p = gmapQl f x (gShowsPrec False (pred n) p)     continueR f x p = gmapQr f x (gShowsPrec False (pred n) p)@@ -122,12 +123,7 @@ -- Some infix constructors seem to have parentheses around them in -- their conString representations. Maybe something should be done about -- that. See the Q test case, and compare with ordinary lists.-showCon a      = showString $ showConstr' a-  where-  showConstr' a-    | dataTypeRep (dataTypeOf a) == dataTypeRep (dataTypeOf 'c') = -        "'" ++ showConstr (toConstr a) ++ "'"-    | otherwise = showConstr $ toConstr a+showCon a      = showString $ showConstr $ toConstr a isAtom a       = glength a == 0 isPrimitive a  = not $ isAlgType (dataTypeOf a) isInfix a      = if isPrimitive a then

@@ -1,4 +1,4 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE DeriveDataTypeable #-}  -- | Tests of the functions in "Test.ChasingBottoms.ApproxShow". 

@@ -1,4 +1,5 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE RankNTypes, ScopedTypeVariables,+             GeneralizedNewtypeDeriving, DeriveDataTypeable #-}  -- TODO: Can we pattern match on functions? -- What about functions of several arguments? Can we have interleaved@@ -11,22 +12,18 @@  -- | -- Module      :  Test.ChasingBottoms.ContinuousFunctions--- Copyright   :  (c) Nils Anders Danielsson 2005-2007+-- Copyright   :  (c) Nils Anders Danielsson 2005-2010 -- License     :  See the file LICENCE.--- --- Maintainer  :  http://www.cs.chalmers.se/~nad/+--+-- Maintainer  :  http://www.cs.nott.ac.uk/~nad/ -- Stability   :  experimental -- Portability :  non-portable (GHC-specific) ----- Note: /This module is unfinished and experimental. However, I do--- not think that I will ever finish it, so I have released it in its--- current state. The documentation below may not be completely--- correct. The source code lists some things which should be--- addressed./+-- Note: /This module is unfinished and experimental. However, I do not think that I will ever finish it, so I have released it in its current state. The documentation below may not be completely correct. The source code lists some things which should be addressed./ -- -- A framework for generating possibly non-strict, partial, -- continuous functions.--- +-- -- The functions generated using the standard QuickCheck 'Arbitrary' -- instances are all strict. In the presence of partial and infinite -- values testing using only strict functions leads to worse coverage@@ -37,15 +34,15 @@ -- instance, using -- -- > type Cogen a = forall b. a -> Gen b -> Gen b--- > +-- > -- > integer :: Gen Integer -- > integer = frequency [ (1, return bottom), (10, arbitrary) ]--- > +-- > -- > coBool :: CoGen Bool -- > coBool b | isBottom b = variant 0 -- > coBool False          = variant 1 -- > coBool True           = variant 2--- > +-- > -- > function :: Cogen a -> Gen b -> Gen (a -> b) -- > function coGen gen = promote (\a -> coGen a gen) --@@ -57,11 +54,10 @@ -- -- Sometimes using possibly non-monotone functions is good enough, -- since that set of functions is a superset of the continuous--- functions. However, say that we want to test that @x--- 'Test.ChasingBottoms.SemanticOrd.<=!' y@ implies that @f x--- 'Test.ChasingBottoms.SemanticOrd.<=!' f y@ for all functions @f@--- (whenever the latter expression returns a total result). This--- property is not valid in the presence of non-monotone functions.+-- functions. However, say that we want to test that @x 'O.<=!' y@+-- implies that @f x 'O.<=!' f y@ for all functions @f@ (whenever the+-- latter expression returns a total result). This property is not+-- valid in the presence of non-monotone functions. -- -- By avoiding 'isBottom' and, unlike the standard 'coarbitrary' -- functions, deferring some pattern matches, we can generate@@ -78,7 +74,7 @@ --     just one transformation per input, but one transformation per --     constructor in the input. 'PatternMatch'es can be constructed --     generically using 'match'.--- +-- -- (2) Then the result is generated, almost like for a normal --     'Arbitrary' instance. However, for each constructor generated a --     subset of the transformations from step 1 are applied. This@@ -94,7 +90,7 @@ -- >   = Branch (Tree a) (Tree a) -- >   | Leaf a -- >     deriving (Show, Typeable, Data)--- > +-- > -- > finiteTreeOf :: MakeResult a -> MakeResult (Tree a) -- > finiteTreeOf makeResult = sized' tree -- >   where@@ -107,7 +103,7 @@ -- >                  ] -- >     where -- >     tree' = tree (size `div` 2)--- > +-- > -- >     baseCase = -- >       frequency' [ (1, return bottom) -- >                  , (2, liftM Leaf makeResult)@@ -147,7 +143,7 @@   , listOf   ) where -import Test.QuickCheck+import Test.QuickCheck hiding ((><), listOf) import Data.Sequence as Seq import Data.Foldable as Seq (foldr) import Prelude as P hiding (concat)@@ -159,6 +155,8 @@ import Data.Generics import qualified Data.List as L +import qualified Test.ChasingBottoms.SemanticOrd as O+ ------------------------------------------------------------------------ -- Generation of functions @@ -215,7 +213,7 @@  -- These functions provided inspiration for the generic one below. -matchFlat :: Arbitrary a => MakePM a+matchFlat :: CoArbitrary a => MakePM a matchFlat a = PatternMatch { apply = coarbitrary a, more = empty }  data Tree a@@ -240,15 +238,12 @@             , more  = more x             }   where-  -- seq added since toConstr is not strict enough for-  -- one-constructor data types. (Bug reported; should be fixed in the-  -- CVS repository.)   toVariant :: forall a b. Data a => a -> Gen b -> Gen b-  toVariant x = x `seq` case constrRep (toConstr x) of-    AlgConstr n    -> variant (n - 1)  -- n >= 1.-    IntConstr i    -> coarbitrary i-    FloatConstr d  -> coarbitrary d-    StringConstr s -> nonBottomError "match: Encountered StringConstr."+  toVariant x = case constrRep (toConstr x) of+    AlgConstr n   -> variant (n - 1)  -- n >= 1.+    IntConstr i   -> coarbitrary i+    FloatConstr d -> coarbitrary d+    CharConstr s  -> nonBottomError "match: Encountered CharConstr."    more :: forall a. Data a => a -> Seq PatternMatch   more = gmapQr (<|) empty match@@ -308,9 +303,9 @@ getMatches :: Seq PatternMatch -> Gen (GenTransformer', Seq PatternMatch) getMatches pms = do   -- Throw away pattern matches with probability 0.1.-  (_, pms') <- partition 9 pms+  (_, pms') <- partition' 9 pms   -- Use pattern matches with probability 0.33.-  (use, keep) <- partition 2 pms'+  (use, keep) <- partition' 2 pms'   let transform = compose $ fmap apply use       further = concat $ fmap more use   if Seq.null further then@@ -336,11 +331,11 @@ -- the relative probability with which elements end up in the second -- part compared to the first one. -partition :: Int -> Seq a -> Gen (Seq a, Seq a)-partition freq ss = case viewl ss of+partition' :: Int -> Seq a -> Gen (Seq a, Seq a)+partition' freq ss = case viewl ss of   EmptyL  -> return (empty, empty)   x :< xs -> do-    (ys, zs) <- partition freq xs+    (ys, zs) <- partition' freq xs     frequency [ (1,    return (x <| ys, zs))               , (freq, return (ys, x <| zs))               ]@@ -447,7 +442,7 @@                map (handle (L.genericLength constrs)) constrs              IntRep         -> [(9, cast' (arbitrary' :: MakeResult Integer))]              FloatRep       -> [(9, cast' (arbitrary' :: MakeResult Double))]-             StringRep      -> nonBottomError "makeResult: StringRep."+             CharRep        -> nonBottomError "makeResult: CharRep."              NoRep          -> nonBottomError "makeResult: NoRep."    handle noConstrs con =

@@ -1,4 +1,4 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE ScopedTypeVariables, DeriveDataTypeable #-}  -- TODO: Tests passed even though for finiteTreeOf and finiteListOf -- transform was only applied once at the top-level!@@ -11,13 +11,14 @@ import Test.ChasingBottoms.ContinuousFunctions import Test.ChasingBottoms.IsBottom import Test.ChasingBottoms.SemanticOrd+import Test.ChasingBottoms.TestUtilities import qualified Test.ChasingBottoms.TestUtilities.Generators as Gen import Test.ChasingBottoms.TestUtilities.Generators (Tree(..)) import Test.ChasingBottoms.ApproxShow import Data.Generics import Test.QuickCheck-import Test.QuickCheck.Batch (run, TestOptions(..), TestResult(..)) import Test.ChasingBottoms.TestUtilities+import Control.Arrow import Control.Monad import Data.List import Data.Ratio@@ -73,36 +74,33 @@ -- How do we test these properties?  testDistribution test t = do-  result <- run t testOptions+  result <- run t   let (ok, msg) = apply test result   unless ok $ putStrLn msg   return ok   where-  apply test (TestOk _ n args) = test n args-  apply _    _                 = (False, "Test failed.")--  testOptions = TestOptions { no_of_tests     = 1000-                            , length_of_tests = 0      -- No time limit.-                            , debug_tests     = False-                            }-+  apply test (Success labels) = test labels+  apply _    _                = (False, "Test failed.") -spread n args = (uniqueShare >= 3%4, "uniqueShare: " ++ show uniqueShare)-  where noUniqueArgs = length . group . sort $ args-        uniqueShare = noUniqueArgs % n+spread labels = (uniqueShare >= 3%4, "uniqueShare: " ++ show uniqueShare)+  where+  noUniqueArgs = length labels+  noArgs       = sum $ map snd labels+  uniqueShare  = noUniqueArgs % noArgs -len max avg short n args =+len max avg short labels =   ( maxLen >= max && averageLen >= avg && shortShare >= 1%10   , "maxLen: " ++ show maxLen ++     ", averageLen: " ++ show averageLen ++     ", shortShare: " ++ show shortShare   )-  where maxLen = maximum lengths-        averageLen = sum lengths % noArgs-        noShortLists = genericLength (filter (<= short) lengths)-        lengths = map read . concat $ args :: [Integer]-        noArgs = toInteger n-        shortShare = noShortLists % noArgs+  where+  lengths      = map (read *** toInteger) labels :: [(Integer, Integer)]+  noArgs       = sum (map snd lengths)+  maxLen       = maximum $ map fst lengths+  averageLen   = sum (map (uncurry (*)) lengths) % noArgs+  noShortLists = sum . map snd . filter ((<= short) . fst) $ lengths+  shortShare   = noShortLists % noArgs  -- | We want to make sure that we can generate many different kinds of -- lazy functions.@@ -116,7 +114,7 @@  -- | The generated lists should not be too short. -prop_lists_have_decent_length = testDistribution (len 20 6 5) $+prop_lists_have_decent_length = testDistribution (len 20 5 5) $   forAll (functionTo (finiteListOf flat)) $ \(f :: Integer -> [Bool]) ->   forAll integer $ \(i :: Integer) ->     collect (length' (f i) :: Integer) $@@ -200,7 +198,7 @@ -- Manual inspection of function tables  viewFun :: (ApproxShow b, Data a) => MakeResult b -> [a] -> IO ()-viewFun (makeResult :: MakeResult b) (inputs :: [a]) = test $+viewFun (makeResult :: MakeResult b) (inputs :: [a]) = quickCheck $   forAll (functionTo makeResult) $ \(f :: a -> b) ->     collect (map (approxShow 5 . f) inputs) $ True 

@@ -1,9 +1,11 @@+{-# LANGUAGE ScopedTypeVariables #-}+ -- | -- Module      :  Test.ChasingBottoms.IsBottom--- Copyright   :  (c) Nils Anders Danielsson 2004-2007+-- Copyright   :  (c) Nils Anders Danielsson 2004-2010 -- License     :  See the file LICENCE.--- --- Maintainer  :  http://www.cs.chalmers.se/~nad/+--+-- Maintainer  :  http://www.cs.nott.ac.uk/~nad/ -- Stability   :  experimental -- Portability :  non-portable (exceptions) --@@ -16,25 +18,41 @@   ) where  import Prelude hiding (catch)-import Control.Exception (catch, throw, Exception(..), evaluate)+import qualified Control.Exception as E import System.IO.Unsafe (unsafePerformIO) import qualified Test.ChasingBottoms.TimeOut as T  -- | @'isBottom' a@ returns 'False' if @a@ is distinct from bottom. If--- @a@ equals bottom and results in an exception which is caught by--- 'isBottom', and this exception is of a certain kind (see below),--- then @'isBottom' a = 'True'@. Other caught exceptions are--- re-thrown. If @a@ never reaches a weak head normal form and--- never throws an exception, then @'isBottom' a@ never terminates.+-- @a@ equals bottom and results in an exception of a certain kind+-- (see below), then @'isBottom' a = 'True'@. If @a@ never reaches a+-- weak head normal form and never throws one of these exceptions,+-- then @'isBottom' a@ never terminates. ----- The exceptions that yield 'True' are those that correspond to--- \"pure bottoms\", i.e. bottoms that can originate in pure code.--- Assertions are excluded, since their behaviour depends on compiler--- flags (not pure, and a failed assertion should really yield an--- exception and nothing else). The same applies to arithmetic--- exceptions (machine dependent, except possibly for--- 'Control.Exception.DivideByZero', but the value infinity makes that--- case unclear as well).+-- The exceptions that yield 'True' correspond to \"pure bottoms\",+-- i.e. bottoms that can originate in pure code:+--+--   * 'E.ArrayException'+--+--   * 'E.ErrorCall'+--+--   * 'E.NoMethodError'+--+--   * 'E.NonTermination'+--+--   * 'E.PatternMatchFail'+--+--   * 'E.RecConError'+--+--   * 'E.RecSelError'+--+--   * 'E.RecUpdError'+--+-- Assertions are excluded, because their behaviour depends on+-- compiler flags (not pure, and a failed assertion should really+-- yield an exception and nothing else). The same applies to+-- arithmetic exceptions (machine dependent, except possibly for+-- 'E.DivideByZero', but the value infinity makes that case unclear as+-- well).  -- Should we use throw or throwIO below? --   It doesn't seem to matter, and I don't think it matters, but@@ -55,11 +73,12 @@ bottom :: a bottom = error "_|_" --- | @'nonBottomError' s@ raises an exception ('AssertionFailed') that--- is not caught by 'isBottom'. Use @s@ to describe the exception.+-- | @'nonBottomError' s@ raises an exception ('E.AssertionFailed')+-- that is not caught by 'isBottom'. Use @s@ to describe the+-- exception.  nonBottomError :: String -> a-nonBottomError = throw . AssertionFailed+nonBottomError = E.throw . E.AssertionFailed  -- | @'isBottomTimeOut' timeOutLimit@ works like 'isBottom', but if -- @timeOutLimit@ is @'Just' lim@, then computations taking more than@@ -68,28 +87,21 @@ -- that this \"function\" may return different answers upon different -- invocations. Take it for what it is worth. ----- 'isBottomTimeOut' is subject to all the same scheduling vagaries as--- 'Test.ChasingBottoms.TimeOut.timeOut'.+-- 'isBottomTimeOut' is subject to all the same vagaries as+-- 'T.timeOut'.  isBottomTimeOut :: Maybe Int -> a -> Bool isBottomTimeOut timeOutLimit f = unsafePerformIO $-  maybeTimeOut (evaluate f) `catch` \e -> case e of-    ArithException _   -> throw e-    ArrayException _   -> return True-    AssertionFailed _  -> throw e-    AsyncException _   -> throw e-    BlockedOnDeadMVar  -> throw e-    Deadlock           -> throw e-    DynException _     -> throw e-    ErrorCall _        -> return True-    ExitException _    -> throw e-    IOException _      -> throw e-    NoMethodError _    -> return True-    NonTermination     -> return True-    PatternMatchFail _ -> return True-    RecConError _      -> return True-    RecSelError _      -> return True-    RecUpdError _      -> return True+  maybeTimeOut (E.evaluate f) `E.catches`+    [ E.Handler (\(_ :: E.ArrayException)   -> return True)+    , E.Handler (\(_ :: E.ErrorCall)        -> return True)+    , E.Handler (\(_ :: E.NoMethodError)    -> return True)+    , E.Handler (\(_ :: E.NonTermination)   -> return True)+    , E.Handler (\(_ :: E.PatternMatchFail) -> return True)+    , E.Handler (\(_ :: E.RecConError)      -> return True)+    , E.Handler (\(_ :: E.RecSelError)      -> return True)+    , E.Handler (\(_ :: E.RecUpdError)      -> return True)+    ]   where   maybeTimeOut io = case timeOutLimit of     Nothing -> do@@ -100,4 +112,4 @@       case result of               -- Note that evaluate bottom /= bottom.         T.Value _        -> return False         T.NonTermination -> return True-        T.Exception e    -> throw e  -- Catch the exception above.+        T.Exception e    -> E.throw e  -- Catch the exception above.

@@ -0,0 +1,3 @@+module Test.ChasingBottoms.IsBottom where++bottom :: a

@@ -1,3 +1,5 @@+{-# LANGUAGE ScopedTypeVariables #-}+ -- | Tests of the functions in "Test.ChasingBottoms.IsBottom". -- -- Note that the warnings given when compiling this module are@@ -12,7 +14,8 @@ import qualified Control.Exception as E  isException f = unsafePerformIO $-  (E.evaluate f >> return False) `E.catch` const (return True)+  (E.evaluate f >> return False)+    `E.catch` (\(_ :: E.SomeException) -> return True)  bot = bot notbot x = notbot x

@@ -1,9 +1,9 @@ -- | -- Module      :  Test.ChasingBottoms.IsType--- Copyright   :  (c) Nils Anders Danielsson 2004-2007+-- Copyright   :  (c) Nils Anders Danielsson 2004-2010 -- License     :  See the file LICENCE.--- --- Maintainer  :  http://www.cs.chalmers.se/~nad/+--+-- Maintainer  :  http://www.cs.nott.ac.uk/~nad/ -- Stability   :  experimental -- Portability :  non-portable (GHC-specific) --@@ -16,6 +16,7 @@   , isString   ) where +import Data.List import Data.Typeable  -- | '@isFunction@ f' returns 'True' iff the top level \"constructor\"@@ -31,8 +32,7 @@ -- for debugging purposes anyway. The unit type is not considered to -- be a tuple. isTuple :: Typeable a => a -> Bool-isTuple x = if null s then False else head s == ','-  where s = tyConString (con x)+isTuple x = "(," `isPrefixOf` tyConString (con x)  isString :: Typeable a => a -> Bool isString x = isList x && typeRepArgs (typeOf x) == typeRepArgs (typeOf "")

@@ -1,11 +1,11 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE DeriveDataTypeable #-}  -- | -- Module      :  Test.ChasingBottoms.Nat--- Copyright   :  (c) Nils Anders Danielsson 2004-2007+-- Copyright   :  (c) Nils Anders Danielsson 2004-2010 -- License     :  See the file LICENCE.--- --- Maintainer  :  http://www.cs.chalmers.se/~nad/+--+-- Maintainer  :  http://www.cs.nott.ac.uk/~nad/ -- Stability   :  experimental -- Portability :  non-portable (GHC-specific) --@@ -16,6 +16,7 @@ module Test.ChasingBottoms.Nat(Nat, isSucc, fromSucc, natrec, foldN) where  import Test.QuickCheck+import qualified Data.Generics as G import Data.Ratio ((%)) import Data.Typeable @@ -23,12 +24,11 @@  -- | Natural numbers. ----- No 'Data.Generics.Basics.Data' instance is provided since the--- implementation should be abstract.+-- No 'G.Data' instance is provided, because the implementation should+-- be abstract. --- Could add 'Data.Generics.Basics.Data' instance based on unary--- representation of natural numbers, but that would lead to--- inefficiencies.+-- Could add 'G.Data' instance based on unary representation of+-- natural numbers, but that would lead to inefficiencies. newtype Nat = Nat { nat2int :: Integer } deriving (Eq, Ord, Typeable)  -- | @'isSucc' 0 == 'False'@, for other total natural numbers it is 'True'.@@ -106,4 +106,9 @@   arbitrary = do     n <- arbitrary :: Gen Integer     return $ fromInteger $ abs n++  shrink 0 = []+  shrink n = [n - 1]++instance CoArbitrary Nat where   coarbitrary n = coarbitrary (toInteger n)

@@ -1,4 +1,4 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE ScopedTypeVariables #-}  -- | Tests for "Test.ChasingBottoms.Nat". @@ -10,7 +10,6 @@ import Test.ChasingBottoms.SemanticOrd import Test.ChasingBottoms.TestUtilities import Test.QuickCheck-import Test.QuickCheck.Batch import Data.Maybe import Data.List import Data.Ratio

@@ -1,11 +1,12 @@-{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}+{-# LANGUAGE ScopedTypeVariables, RankNTypes,+             FlexibleInstances, UndecidableInstances #-}  -- | -- Module      :  Test.ChasingBottoms.SemanticOrd--- Copyright   :  (c) Nils Anders Danielsson 2004-2007+-- Copyright   :  (c) Nils Anders Danielsson 2004-2010 -- License     :  See the file LICENCE.--- --- Maintainer  :  http://www.cs.chalmers.se/~nad/+--+-- Maintainer  :  http://www.cs.nott.ac.uk/~nad/ -- Stability   :  experimental -- Portability :  non-portable (GHC-specific) --@@ -188,7 +189,7 @@     bottom    else     gzipWithT (\x y -> semanticMeet' tweak x y) a b-    + semanticJoin' :: (Data a, Data b) => Tweak -> a -> b -> Maybe b semanticJoin' tweak a (b :: b) =   case ( isBottomTimeOut (timeOutLimit tweak) a

@@ -1,4 +1,4 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE RankNTypes #-}  -- | Tests for "Test.ChasingBottoms.SemanticOrd". The functions using -- tweaks are currently not tested.@@ -9,7 +9,6 @@ import Test.ChasingBottoms.TestUtilities import Test.ChasingBottoms.TestUtilities.Generators hiding (tests) import Test.QuickCheck-import Test.QuickCheck.Batch (run) import Data.Generics import Control.Monad import Data.Maybe

@@ -1,21 +0,0 @@-{-# OPTIONS -fth #-}---- | By importing this module in e.g. "Test.ChasingBottoms" the--- library refuses to be built if the tests fail.--module Test.ChasingBottoms.TestLibraryWhenCompiling () where--import qualified Test.ChasingBottoms.Tests as Tests-import qualified System.IO as IO-import qualified Language.Haskell.TH as TH--$(do -     b <- TH.runIO $ do putStr "----- Testing the library. -----\n\n"-                        b <- Tests.main-                        IO.hFlush IO.stdout-                        return b-     if not b then-       fail "Tests failed. Refusing to build library."-      else-       return []- )

@@ -2,7 +2,8 @@  module Test.ChasingBottoms.TestUtilities   ( -- * Batch execution of QuickCheck tests-    runQuickCheckTests+    run+  , runQuickCheckTests     -- * Various algebraic properties   , isAssociative   , isCommutative@@ -24,7 +25,6 @@   ) where  import Test.QuickCheck-import Test.QuickCheck.Batch import Data.List import Control.Arrow import Control.Monad@@ -33,50 +33,38 @@ ------------------------------------------------------------------------ -- Batch execution of QuickCheck tests +-- | Runs a single test, using suitable settings.++run :: Testable p => p -> IO Result+run = quickCheckWithResult (stdArgs { maxSuccess = 1000+                                    , maxDiscard = 5000+                                    })+ -- | Runs a bunch of QuickCheck tests, printing suitable information -- to standard output. Returns 'True' if no tests fail. Note that a -- test where the inputs are exhausted is considered to have -- succeeded. -runQuickCheckTests :: [TestOptions -> IO TestResult]+runQuickCheckTests :: [IO Result]                       -- ^ Create the tests in this list from ordinary                       -- QuickCheck tests by using 'run'.                       -> IO Bool runQuickCheckTests tests = do-  results <- mapM ($ testOptions) tests-  mapM_ (putStr . showTR) results+  results <- sequence tests+  mapM_ (putStrLn . showTR) results   return $ all ok $ results   where-  ok (TestOk {})       = True-  ok (TestExausted {}) = True   -- We treat this as OK since the-                                -- distribution of test data is displayed.-  ok (TestFailed {})   = False-  ok (TestAborted {})  = False--  testOptions = TestOptions { no_of_tests     = 1000-                            , length_of_tests = 0      -- No time limit.-                            , debug_tests     = False-                            }--  showTR (TestOk _ n args) =-    "OK, passed " ++ show n ++ " tests.\n" ++ showArgs args-  showTR (TestExausted _ n args) =-    "Arguments exhausted after " ++ show n ++ " tests.\n" ++ showArgs args-  showTR (TestFailed _ _) = "Test failed.\n"-  showTR (TestAborted _) = "Test resulted in exception.\n"+  ok (Success {})           = True+  ok (GaveUp {})            = False+  ok (Failure {})           = False+  ok (NoExpectedFailure {}) = False -  showArgs :: [[String]] -> String-  showArgs args-    | all null args = ""-    | otherwise     =-        unlines-        . map (indent . uncurry (++)-               . (formatNum *** (concat . intersperse ", ")))-        . sortBy (\x y -> compare (fst y) (fst x))-        . map (length &&& head) . group . sort-        $ args-    where indent = ("  " ++)-          formatNum = flip shows ": "+  showTR (Success {})              = "OK."+  showTR (GaveUp { numTests = n }) =+    "Gave up after " ++ show n ++ " tests."+  showTR (Failure {})              = "Test failed."+  showTR (NoExpectedFailure {})    =+    "Test did not fail, but it should have."  ------------------------------------------------------------------------ -- Testing various algebraic properties@@ -230,19 +218,17 @@ isPartialOrder element equalTo differentFrom greaterThan (==.) (<=.) =   [reflexive, antisymmetric1, antisymmetric2, transitive]   where-  infix 4 ==., <=.-   reflexive =     forAll element $ \x ->       x <=. x    antisymmetric1 =     forAll (pair element equalTo) $ \(x, y) ->-      (x <=. y && y <=. x) && x ==. y+      ((x <=. y) && (y <=. x)) && x ==. y    antisymmetric2 =     forAll (pair element differentFrom) $ \(x, y) ->-      not (x <=. y && y <=. x) && not (x ==. y)+      not ((x <=. y) && (y <=. x)) && not (x ==. y)    transitive = forAll (pair element greaterThan) $ \(x, y) ->                  forAll (greaterThan y) $ \z ->@@ -271,12 +257,10 @@   isPartialOrder element equalTo differentFrom greaterThan (==.) (<=.)   ++ [total]   where-  infix 4 <=.-   total =     forAll element $ \x ->     forAll element $ \y ->-      x <=. y || y <=. x+      (x <=. y) || (y <=. x)  -- | Tests relating various partial order operators. Does not include -- any tests from 'isPartialOrder'.@@ -301,17 +285,15 @@ isPartialOrderOperators element greaterThan (==.) (<=.) (<.) (>=.) (>.) =   [lt_le, gt_ge, ge_le, lt_gt]   where-  infix 4 ==., <=., <., >=., >.-   twoElems = pair3 element greaterThan    lt_le =     forAll twoElems $ \(x, y) ->-      (x <. y) == (x <=. y && not (x ==. y))+      (x <. y) == ((x <=. y) && not (x ==. y))    gt_ge =     forAll twoElems $ \(x, y) ->-      (x >. y) == (x >=. y && not (x ==. y))+      (x >. y) == ((x >=. y) && not (x ==. y))    ge_le =     forAll twoElems $ \(x, y) ->

@@ -1,4 +1,4 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE RankNTypes, DeriveDataTypeable #-}  -- | Generators that are part of the testing framework. @@ -47,7 +47,6 @@ import Test.ChasingBottoms.SemanticOrd import Test.ChasingBottoms.TestUtilities import Test.QuickCheck-import Test.QuickCheck.Batch (run) import Data.Generics import Control.Monad import Data.Maybe@@ -118,7 +117,7 @@                       ]  testGen :: (Show a, Data a) => Nat -> Gen a -> IO ()-testGen depth gen = test $ forAll gen $ \n ->+testGen depth gen = quickCheck $ forAll gen $ \n ->                       collect (approxShow depth n) $ True  ------------------------------------------------------------------------@@ -163,7 +162,7 @@  testFunction :: (Data a, Data b) => Nat -> Cogen a -> Gen b -> [a] -> IO () testFunction depth coGen gen inputs =-  test $ forAll (function coGen gen) $ \f ->+  quickCheck $ forAll (function coGen gen) $ \f ->     collect (map (\x -> approxShow depth (x, f x)) inputs) $ True  ------------------------------------------------------------------------@@ -251,7 +250,7 @@     x /=! y  testGenPair :: (Show a, Data a) => Nat -> Gen a -> (a -> Gen a) -> IO ()-testGenPair depth gen gen' = test $+testGenPair depth gen gen' = quickCheck $   forAll (pair gen gen') $ \(x, y) ->     collect (approxShow depth (x, y)) $ True 

@@ -1,8 +1,8 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE FlexibleInstances #-}  -- | Tests of almost everything related to "Test.ChasingBottoms". -module Test.ChasingBottoms.Tests (main) where+module Main (main) where  import qualified Test.ChasingBottoms.Approx.Tests              as Approx import qualified Test.ChasingBottoms.ApproxShow.Tests          as ApproxShow

@@ -1,11 +1,11 @@-{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE ScopedTypeVariables, DeriveDataTypeable #-}  -- | -- Module      :  Test.ChasingBottoms.TimeOut--- Copyright   :  (c) Nils Anders Danielsson 2004-2007+-- Copyright   :  (c) Nils Anders Danielsson 2004-2010 -- License     :  See the file LICENCE.--- --- Maintainer  :  http://www.cs.chalmers.se/~nad/+--+-- Maintainer  :  http://www.cs.nott.ac.uk/~nad/ -- Stability   :  experimental -- Portability :  non-portable (preemptive scheduling) --@@ -29,25 +29,32 @@ import Data.Dynamic import qualified Control.Exception as E +import {-# SOURCE #-} qualified Test.ChasingBottoms.IsBottom as B+ data Result a   = Value a   | NonTermination-  | Exception E.Exception-    deriving (Eq, Show, Typeable)+  | Exception E.SomeException+    deriving (Show, Typeable)  -- | @'timeOut' n c@ runs @c@ for at most @n@ seconds (modulo -- scheduling issues). -----   * If the computation terminates before that, then---     @'Value' v@ is returned, where @v@ is the resulting value. Note---     that this value may be equal to bottom, e.g. if @c = 'return'---     'Test.ChasingBottoms.IsBottom.bottom'@.+--   * If the computation terminates before that, then @'Value' v@ is+--     returned, where @v@ is the resulting value. Note that this+--     value may be equal to bottom, e.g. if @c = 'return'+--     'B.bottom'@. -- --   * If the computation does not terminate, then 'NonTermination' is --     returned. -- --   * If the computation raises an exception, then @'Exception' e@ is --     returned, where @e@ is the exception.+--+-- Note that a user-defined exception is used to terminate the+-- computation, so if @c@ catches all exceptions, or blocks+-- asynchronous exceptions, then 'timeOut' may fail to function+-- properly.  timeOut :: Int -> IO a -> IO (Result a) timeOut = timeOutMicro . (* 10^6)@@ -61,12 +68,12 @@ timeOutMicro delay io = do   mv <- newEmptyMVar   let putException = putMVar mv . Exception-  ioThread <- forkIO $ (io >>= putMVar mv . Value)-                      `E.catch` (\e -> case e of-                        E.DynException d -> case fromDynamic d of-                          Just Die -> return ()  -- Thread properly killed.-                          Nothing -> putException e-                        _ -> putException e)+  ioThread <- forkIO $+    (io >>= putMVar mv . Value)+    `E.catch` (\(e :: E.SomeException) ->+                case E.fromException e of+                  Just Die -> return ()  -- Thread properly killed.+                  Nothing  -> putException e)   reaper <- forkIO $ do     threadDelay delay     putMVar mv NonTermination@@ -76,14 +83,16 @@   return result  -- Since 'ioThread' above should return exceptions raised in the code--- we cannot kill the thread using killThread, which raises--- @'AsyncException' 'ThreadKilled'@. We use the locally defined type--- 'Die' together with a dynamic exception instead.+-- it seems like a bad idea to kill the thread using killThread, which+-- raises @'AsyncException' 'ThreadKilled'@. We use the locally+-- defined type 'Die' instead. -data Die = Die deriving Typeable+data Die = Die deriving (Show, Typeable) -killThread' threadId = E.throwDynTo threadId Die+instance E.Exception Die +killThread' threadId = E.throwTo threadId Die+ -- | 'timeOut'' is a variant which can be used for pure -- computations. The definition, --@@ -91,12 +100,11 @@ --   'timeOut'' n = 'timeOut' n . 'E.evaluate' -- @ ----- ensures that @'timeOut'' 1 'Test.ChasingBottoms.IsBottom.bottom'@--- usually returns @'Exception' \<something\>@. (@'timeOut' 1 ('return'--- 'Test.ChasingBottoms.IsBottom.bottom')@ usually returns @'Value'--- 'Test.ChasingBottoms.IsBottom.bottom'@; in other words, the--- computation reaches whnf almost immediately, defeating the purpose--- of the time-out.)+-- ensures that @'timeOut'' 1 'B.bottom'@ usually returns @'Exception'+-- \<something\>@. (@'timeOut' 1 ('return' 'B.bottom')@ usually+-- returns @'Value' 'B.bottom'@; in other words, the computation+-- reaches whnf almost immediately, defeating the purpose of the+-- time-out.)  timeOut' :: Int -> a -> IO (Result a) timeOut' n = timeOut n . E.evaluate