diff --git a/ChasingBottoms.cabal b/ChasingBottoms.cabal new file mode 100644 --- /dev/null +++ b/ChasingBottoms.cabal @@ -0,0 +1,46 @@ +name: ChasingBottoms +version: 1.2.2 +license: OtherLicense +license-file: LICENCE +copyright: Copyright (c) Nils Anders Danielsson 2004-2007. +author: Nils Anders Danielsson +maintainer: http://www.cs.chalmers.se/~nad/contact.html +stability: experimental +homepage: http://www.cs.chalmers.se/~nad/software/#Chasing Bottoms +package-url: http://www.cs.chalmers.se/~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 the error function), or code involving infinite values? Then this + library could be useful for you. +category: Test +tested-with: GHC == 6.8.1 +cabal-version: >= 1.2 && < 2 + +flag small_base + description: Choose the new smaller, split-up base package. + +library + exposed-modules: + Test.ChasingBottoms, + Test.ChasingBottoms.Approx, + Test.ChasingBottoms.ApproxShow, + Test.ChasingBottoms.ContinuousFunctions, + Test.ChasingBottoms.IsBottom, + Test.ChasingBottoms.Nat, + Test.ChasingBottoms.SemanticOrd, + Test.ChasingBottoms.TimeOut + + 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 + +-- 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. diff --git a/Header b/Header new file mode 100644 --- /dev/null +++ b/Header @@ -0,0 +1,96 @@ +Do you ever feel the need to test code involving bottoms (e.g. calls to +the @error@ function), or code involving infinite values? Then this +library could be useful for you. + +It is usually easy to get a grip on bottoms by showing a value and +waiting to see how much gets printed before the first exception is +encountered. However, that quickly gets tiresome and is hard to automate +using e.g. QuickCheck +(). With this library you +can do the tests as simply as the following examples show. + +Testing explicitly for bottoms: + + [@> isBottom (head [\])@] @True@ + + [@> isBottom bottom@] @True@ + + [@> isBottom (\\_ -> bottom)@] @False@ + + [@> isBottom (bottom, bottom)@] @False@ + +Comparing finite, partial values: + + [@> ((bottom, 3) :: (Bool, Int)) ==! (bottom, 2+5-4)@] @True@ + + [@> ((bottom, bottom) :: (Bool, Int)) approxShow 4 $ (True, bottom) \\\/! (bottom, \'b\')@] @\"Just (True, \'b\')\"@ + + [@> approxShow 4 $ (True, bottom) \/\\! (bottom, \'b\')@] @\"(_|_, _|_)\"@ + + [@> approxShow 4 $ ([1..\] :: [Int\])@] @\"[1, 2, 3, _\"@ + + [@> approxShow 4 $ (cycle [bottom\] :: [Bool\])@] @\"[_|_, _|_, _|_, _\"@ + +Approximately comparing infinite, partial values: + + [@> approx 100 [2,4..\] ==! approx 100 (filter even [1..\] :: [Int\])@] @True@ + + [@> approx 100 [2,4..\] \/=! approx 100 (filter even [bottom..\] :: [Int\])@] @True@ + +The code above relies on the fact that @bottom@, just as @error +\"...\"@, @undefined@ and pattern match failures, yield +exceptions. Sometimes we are dealing with properly non-terminating +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..\]) >>= print@] @NonTermination@ + +The time-out functionality can be used to treat \"slow\" computations as +bottoms: + + [@> let tweak = Tweak { approxDepth = Just 5, timeOutLimit = Just 2 }@] + + [@> semanticEq tweak (reverse [1..\], [1..\]) (bottom :: [Int\], [1..\] :: [Int\])@] @True@ + + [@> let tweak = noTweak { timeOutLimit = Just 2 }@] + + [@> semanticJoin tweak (reverse [1..\], True) ([\] :: [Int\], bottom)@] @Just ([],True)@ + +This can of course be dangerous: + + [@> let tweak = noTweak { timeOutLimit = Just 0 }@] + + [@> semanticEq tweak (reverse [1..100000000\]) (bottom :: [Integer\])@] @True@ + +Timeouts can also be applied to @IO@ computations: + + [@> 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 $ take 4 $ filter ((== 1) . (\`mod\` 83)) primes) >>= print@] @[167,499,997NonTermination@ + + [@> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (\`mod\` 83)) primes) >>= print@] @[167,499,997,1163]@ + + [@ @] @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\" +(). + +The code has been tested under GHC 6.8. 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. + +Source code: . diff --git a/LICENCE b/LICENCE new file mode 100644 --- /dev/null +++ b/LICENCE @@ -0,0 +1,23 @@ +I have chosen to distribute this library under the MIT/Expat licence: +--------------------------------------------------------------------- + +Copyright (c) 2004-2007 Nils Anders Danielsson + +Permission is hereby granted, free of charge, to any person obtaining a +copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS +OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/Makefile b/Makefile new file mode 100644 --- /dev/null +++ b/Makefile @@ -0,0 +1,73 @@ +# This Makefile is currently only used to build the documentation and +# to run a test suite automatically using darcs. + +######################################################################## +# You may need to edit the following variables: + +# Path to Haddock. +HADDOCK ?= haddock + +# URL prefix leading to Haddock documentation for the hierarchical +# libraries. +GHC_DOC_URL ?= http://www.haskell.org/ghc/docs/latest/html/libraries + +# Path prefix leading to Haddock interface files for the hierarchical +# libraries. These files should be compiled using a Haddock program +# which is interface compatible with the one listed above (same +# version). +GHC_DOC_PATH ?= /chalmers/sw/unsup/ghc-6.8.1/share/doc/ghc/libraries + +# Documentation is stored in this directory. Note that the directory +# is emptied first. +DOCDIR = docs + +# Path to GHC 6.8, used to run the tests. +GHC_68 ?= _ghc_6.8.1 + +# GHC packages necessary for building and testing the library. +PACKAGES = base-3.0.0.0 containers-0.1.0.0 random-1.0.0.0 mtl-1.1.0.0 \ +QuickCheck-1.1.0.0 array-0.1.0.0 + +######################################################################## + +EXPOSED_SOURCES = ChasingBottoms.hs ChasingBottoms/Approx.hs \ +ChasingBottoms/ApproxShow.hs ChasingBottoms/ContinuousFunctions.hs \ +ChasingBottoms/IsBottom.hs ChasingBottoms/Nat.hs \ +ChasingBottoms/SemanticOrd.hs ChasingBottoms/TimeOut.hs + +HIDDEN_SOURCES = ChasingBottoms/IsType.hs ChasingBottoms/Tests.hs \ +ChasingBottoms/Approx/Tests.hs ChasingBottoms/ApproxShow/Tests.hs \ +ChasingBottoms/ContinuousFunctions/Tests.hs \ +ChasingBottoms/IsBottom/Tests.hs ChasingBottoms/IsType/Tests.hs \ +ChasingBottoms/Nat/Tests.hs ChasingBottoms/SemanticOrd/Tests.hs \ +ChasingBottoms/TimeOut/Tests.hs ChasingBottoms/TestUtilities.hs \ +ChasingBottoms/TestUtilities/Generators.hs \ +ChasingBottoms/TestLibraryWhenCompiling.hs + +FILES_TO_BE_EXCLUDED = .boring + +$(DOCDIR) : $(DOCDIR)/index.html +$(DOCDIR)/index.html : $(addprefix Test/,$(EXPOSED_SOURCES)) Header + -rm -rf $(DOCDIR) + mkdir -p $(DOCDIR) + $(HADDOCK) -h --title="Chasing Bottoms" --prologue=Header -o$(DOCDIR) \ + $(foreach pkg,$(PACKAGES),\ + -i$(GHC_DOC_URL)/$(pkg),$(GHC_DOC_PATH)/$(pkg)/`echo $(pkg) | sed -r -e 's/-.*//'`.haddock) \ + $(filter Test/%,$^) + +# Target used by darcs dist. +# After building the documentation we remove the generated files. We +# do not want them included in the tar ball generated by darcs. +# We also remove some other files. +dist: $(DOCDIR) + -rm $(FILES_TO_BE_EXCLUDED) + +# 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)) diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,28 @@ +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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,3 @@ +import Distribution.Simple + +main = defaultMain diff --git a/Test/ChasingBottoms.hs b/Test/ChasingBottoms.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms.hs @@ -0,0 +1,40 @@ +-- | +-- Module : Test.ChasingBottoms +-- Copyright : (c) Nils Anders Danielsson 2004-2007 +-- License : See the file LICENCE. +-- +-- Maintainer : http://www.cs.chalmers.se/~nad/ +-- Stability : experimental +-- Portability : non-portable (GHC-specific) +-- +-- This module just re-exports all the other modules. + +module Test.ChasingBottoms + ( module Test.ChasingBottoms.Approx + , module Test.ChasingBottoms.ApproxShow + , module Test.ChasingBottoms.ContinuousFunctions + , module Test.ChasingBottoms.IsBottom + , module Test.ChasingBottoms.Nat + , module Test.ChasingBottoms.SemanticOrd + , module Test.ChasingBottoms.TimeOut + ) where + +import Test.ChasingBottoms.Approx +import Test.ChasingBottoms.ApproxShow +import Test.ChasingBottoms.ContinuousFunctions +import Test.ChasingBottoms.IsBottom +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 + +-} diff --git a/Test/ChasingBottoms/Approx.hs b/Test/ChasingBottoms/Approx.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/Approx.hs @@ -0,0 +1,106 @@ +{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} + +-- | +-- Module : Test.ChasingBottoms.Approx +-- Copyright : (c) Nils Anders Danielsson 2004-2007 +-- License : See the file LICENCE. +-- +-- Maintainer : http://www.cs.chalmers.se/~nad/ +-- Stability : experimental +-- Portability : non-portable (GHC-specific) +-- + +module Test.ChasingBottoms.Approx + ( Approx(..) + ) where + +import Test.ChasingBottoms.Nat +import Data.Generics +import qualified Data.List as List + +{-| +'Approx' is a class for approximation functions as described +in The generic approximation lemma, Graham Hutton and Jeremy +Gibbons, Information Processing Letters, 79(4):197-201, Elsevier +Science, August 2001, . + +Instances are provided for all members of the 'Data' type class. Due +to the limitations of the "Data.Generics" approach to generic +programming, which is not really aimed at this kind of application, +the implementation is only guaranteed to perform correctly, with +respect to the paper (and modulo any bugs), on non-mutually-recursive +sum-of-products datatypes. In particular, nested and mutually +recursive types are not handled correctly with respect to the +paper. The specification below is correct, though (if we assume that +the 'Data' instances are well-behaved). + +In practice the 'approxAll' function can probably be more useful than +'approx'. It traverses down /all/ subterms, and it should be possible +to prove a variant of the approximation lemma which 'approxAll' +satisfies. +-} + +class Approx a where + -- | @'approxAll' n x@ traverses @n@ levels down in @x@ and replaces all + -- values at that level with bottoms. + approxAll :: Nat -> a -> a + + -- | 'approx' works like 'approxAll', but the traversal and + -- replacement is only performed at subterms of the same monomorphic + -- type as the original term. For polynomial datatypes this is + -- exactly what the version of @approx@ described in the paper above + -- does. + approx :: Nat -> a -> a + +instance Data a => Approx a where + approxAll = approxAllGen + approx = approxGen + +-- From The generic approximation lemma (Hutton, Gibbons): + +-- Generic definition for arbitrary datatype \mu F: +-- approx (n+1) = in . F (approx n) . out + +-- Approximation lemma (valid if F is locally continuous), +-- for x, y :: \mu F: +-- x = y <=> forall n in Nat corresponding to natural numbers. +-- approx n x = approx n y + +approxGen :: Data a => Nat -> a -> a +approxGen n | n == 0 = error "approx 0 = _|_" + | otherwise = + \(x :: a) -> gmapT (mkT (approxGen (pred n) :: a -> a)) x + +-- We use mkT to only recurse on the original type. This solution is +-- actually rather nice! But sadly it doesn't work for nested or +-- mutually recursive types... + +-- Note that the function is defined in the \n -> \x -> style, not +-- \n x -> which would mean something subtly different. + +------------------------------------------------------------------------ + +-- Recurses on everything... + +approxAllGen :: Data a => Nat -> a -> a +approxAllGen n | n == 0 = error "approx 0 = _|_" + | otherwise = \x -> gmapT (approxAllGen (pred n)) x + +------------------------------------------------------------------------ + +-- Behaves exactly like approxGen. (?) + +approxGen' :: Data a => Nat -> a -> a +approxGen' n + | n == 0 = error "approx 0 = _|_" + | otherwise = \x -> + let d = dataTypeOf x + n' = pred n + 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 diff --git a/Test/ChasingBottoms/Approx/Tests.hs b/Test/ChasingBottoms/Approx/Tests.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/Approx/Tests.hs @@ -0,0 +1,200 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- | Tests of the functions in "Test.ChasingBottoms.Approx". + +module Test.ChasingBottoms.Approx.Tests (tests) where + +-- Improve the testing here. (Use QuickCheck when there is some proper +-- infrastructure for testing bottoms and infinite stuff. Hmm... This +-- module is part of that infrastructure, so be careful.) + +import Test.ChasingBottoms.Approx +import Test.ChasingBottoms.IsBottom +import Test.ChasingBottoms.SemanticOrd +import Test.ChasingBottoms.Nat +import Data.Generics + +data Tree = Lf | Br Tree Tree deriving (Typeable, Data) + +leftInfinite = Br leftInfinite Lf +twoLevels = Br (Br bottom bottom) Lf +threeLevels = Br (Br (Br bottom bottom) Lf) Lf + +-- A nested type: +data PerfectTree t = PL t | PB (PerfectTree (t, t)) + deriving (Show, Typeable, Data) + +pTree :: PerfectTree Int +pTree = PB (PB (PL ((1, 2), (3, 4)))) + +-- Full form of PerfectTree: PT A = Lift (A + PT (Lift (A x A))). +-- Define F G A = Lift (A + G (Lift (A x A))). + +type F g a = Either a (g (a, a)) + +-- Assume that F is locally continuous. We have PT = mu F = F (mu F), +-- i.e. PT a = F PT a, with operations +-- in :: F PT a -> PT a +-- out :: PT a -> F PT a +-- map :: (forall a . G a -> G' a) -> F G a -> F G' a + +in_PT :: F PerfectTree t -> PerfectTree t +in_PT x = case x of + Left t -> PL t + Right tt -> PB tt + +out_PT :: PerfectTree t -> F PerfectTree t +out_PT x = case x of + PL t -> Left t + PB tt -> Right tt + +-- Pattern type signature added just for clarity. +map_PT :: (forall t . g t -> g' t) -> F g t' -> F g' t' +map_PT f x = case x of + Left t -> Left t + Right (tt :: g (t, t)) -> Right (f tt) + +-- Note that we get a boring map using this kind of functor for nested +-- types: +fullMap_PT :: (forall a . a -> a) -> PerfectTree a -> PerfectTree a +fullMap_PT f = in_PT . map_PT (fullMap_PT f) . out_PT + +-- And now we can define approx for this type: + +approx_PT :: Nat -> PerfectTree a -> PerfectTree a +approx_PT n | n == 0 = error "approx 0 == _|_" + | otherwise = in_PT . map_PT (approx_PT (pred n)) . out_PT + +-- Some types with several parameters. +data A a b = A0 a | A1 b deriving (Typeable, Data) +data C a b = C0 (C a b) | C1 a b deriving (Typeable, Data) + +-- Mutually recursive types: +data G a = G1 a | G2 (H a) deriving (Typeable, Data) +data H a = H1 (G a) | H2 a deriving (Typeable, Data) + +{- + +GH a (r1, r2) = (Lift (a + r2), Lift (r1 + a)) + +G a = fst (mu (GH a)) +H a = snd (mu (GH a)) + +--> is used for arrows in the product category: +(a1, a2) --> (b1, b2) = (a1 -> b1, a2 -> b2) + +in :: GH a (mu (GH a)) --> mu (GH a) +out :: GH a (mu (GH a)) <-- mu (GH a) + +map_GH :: (p1 --> p2) -> (GH a p1 --> GH a p2) + +-} + +-- The following is an approximation, since we don't have proper +-- products. However, if no one breaks the abstraction this won't be a +-- problem. + +-- Sadly I cannot write "type GH a (r1, r2) = (Either a r2, Either r1 a)". +type GH a r1 r2 = (Either a r2, Either r1 a) +type M a = (G a, H a) +-- And "type (a1, a2) :--> (b1, b2) = (a1 -> b1, a2 -> b2)" doesn't +-- work either... +type ProdArr a1 a2 b1 b2 = (a1 -> b1, a2 -> b2) + +-- in_GH :: GH a (M a) :--> M a +in_GH :: ProdArr (Either a (H a)) (Either (G a) a) (G a) (H a) +in_GH = (in_G, in_H) + where + in_G e = case e of + Left a -> G1 a + Right m -> G2 m + in_H e = case e of + Left m -> H1 m + Right a -> H2 a + +-- out_GH :: M a :--> GH a (M a) +out_GH :: ProdArr (G a) (H a) (Either a (H a)) (Either (G a) a) +out_GH = (out_G, out_H) + where + out_G m = case m of + G1 a -> Left a + G2 m -> Right m + out_H m = case m of + H1 m -> Left m + H2 a -> Right a + +-- map_GH :: ((a1, a2) :--> (b1, b2)) -> (GH a a1 a2 :--> GH a b1 b2) +map_GH :: ProdArr a1 a2 b1 b2 -> ProdArr (Either a a2) (Either a1 a) + (Either a b2) (Either b1 a) +map_GH gh = (map_G, map_H) + where + (g, h) = gh + map_G e = case e of + Left a -> Left a + Right a2 -> Right (h a2) + map_H e = case e of + Left a1 -> Left (g a1) + Right a -> Right a + +(.*.) :: ProdArr b1 b2 c1 c2 -> ProdArr a1 a2 b1 b2 -> ProdArr a1 a2 c1 c2 +(g1, h1) .*. (g2, h2) = (g1 . g2, h1 . h2) + +-- approx_GH :: Nat -> (M a :--> M a) +approx_GH :: Nat -> ProdArr (G a) (H a) (G a) (H a) +approx_GH n | n == 0 = error "approx 0 == _|_" + | otherwise = in_GH .*. map_GH (approx_GH (pred n)) .*. out_GH + +approx_G :: Nat -> G a -> G a +approx_G = fst . approx_GH + +approx_H :: Nat -> H a -> H a +approx_H = snd . approx_GH + +g1 = G2 (H1 (G2 (H2 'a'))) +h1 = H1 (G2 (H1 (G1 'b'))) + +tests :: [Bool] +tests = + -- approx 0 = bottom. + [ approx 0 ==! (bottom :: Int -> Int) + , approx 0 ==! (bottom :: Char -> Char) + , approx 0 True ==! (bottom :: Bool) + + -- approx (Succ n) /= bottom. + , approx 1 /=! (bottom :: Int -> Int) + , approx 1 /=! (bottom :: Char -> Char) + + -- approx n descends n levels. + , approx 3 "test" ==! "tes" ++ bottom + , approx 3 "tes" ==! "tes" ++ bottom + , approx 3 "te" ==! "te" + , approx 3 "t" ==! "t" + + -- This also works for infinite and multiply branching + -- structures. + , approx 2 leftInfinite ==! twoLevels + , approx 3 leftInfinite ==! threeLevels + + -- Multiple parameter data types shouldn't pose a problem. + , approx 1 (A0 (A1 True) :: A (A Char Bool) Char) ==! A0 (A1 True) + , approx 2 (C0 (C1 'a' True)) ==! C0 (C1 'a' True) + , approx 1 (C0 (C1 'a' True)) ==! C0 bottom + + -- Multiple parameter data types shouldn't pose a problem for + -- approxAll either. + , approxAll 1 (A0 (A1 True) :: A (A Char Bool) Char) ==! A0 bottom + , approxAll 1 (C0 (C1 'a' True)) ==! C0 bottom + + -- approxAll doesn't descend only on the original type... + , approxAll 1 (Just (Just (Just True))) ==! (Just bottom) + , approxAll 2 pTree ==! approx_PT 2 pTree + , approxAll 2 g1 ==! approx_G 2 g1 + + -- ...but approx does... + , approx 1 (Just (Just (Just True))) ==! (Just (Just (Just True))) + + -- ...more or less: + , approx 2 pTree /=! approx_PT 2 pTree + , approx 2 g1 /=! approx_G 2 g1 + -- Note that a perfect implementation would have equalities here. + ] diff --git a/Test/ChasingBottoms/ApproxShow.hs b/Test/ChasingBottoms/ApproxShow.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/ApproxShow.hs @@ -0,0 +1,138 @@ +{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} + +-- | +-- Module : Test.ChasingBottoms.ApproxShow +-- Copyright : (c) Nils Anders Danielsson 2004-2007 +-- License : See the file LICENCE. +-- +-- Maintainer : http://www.cs.chalmers.se/~nad/ +-- Stability : experimental +-- Portability : non-portable (GHC-specific) +-- +-- Functions for converting arbitrary (non-function, partial, +-- possibly infinite) values into strings. + +module Test.ChasingBottoms.ApproxShow + ( Prec + , ApproxShow(..) + ) where + +import Data.Generics +import Test.ChasingBottoms.IsBottom +import Test.ChasingBottoms.Nat +import Test.ChasingBottoms.IsType +import qualified Data.List as List + +-- | Precedence level. +type Prec = Int + +class ApproxShow a where + -- | The 'Data' instance of 'ApproxShow' makes sure that + -- @'approxShowsPrec' n@ behaves (more or less) like the derived + -- version of 'showsPrec', with the following differences: + -- + -- * After @n@ levels of descent into a term the output is + -- replaced by @\"_\"@. + -- + -- * All detectable occurences of bottoms are replaced by @\"_|_\"@. + -- + -- * Non-bottom functions are displayed as @\"\\"@. + -- + approxShowsPrec :: Nat -> Prec -> a -> ShowS + approxShows :: Nat -> a -> ShowS + approxShow :: Nat -> a -> String + + approxShows n a = approxShowsPrec n 0 a + approxShow n a = approxShowsPrec n 0 a "" + +instance Data a => ApproxShow a where + approxShowsPrec n p = gShowsPrec False n p + +-- This is a gigantic hack (due to special treatment of lists and +-- strings). Now I realise how I should have written it: +-- A wrapper taking care of n == 0 and bottoms. +-- A generic case treating ordinary data types +-- Special cases (type specific extensions) for tuples, functions, +-- lists and strings. +-- I'm not sure if it's possible to have a type specific extension that +-- works for, for instance, all list types, though. I guess that it +-- would have to be monomorphic. +-- +-- Anyway, I don't have time improving this right now. All tests go +-- through, so this should be fine. + +gShowsPrec :: Data a => Bool -> Nat -> Prec -> a -> ShowS +gShowsPrec insideList n p (a :: a) + | n == 0 = showString "_" + | isBottom a = showString "_|_" + | isFunction a = showString "" + | isTuple a = showParen True $ drive $ + List.intersperse (showString ", ") $ + (continueR (:) [] minPrec a) + | isString a && isAtom a = when' (not insideList) (showString "\"") $ + showString "\"" -- End of string. + | isString a = when' (not insideList) (showString "\"") $ + gmapQr (.) id + ( id -- Dummy. + `mkQ` + (\c -> if n == 1 then showString "_" else + if isBottom c then showString "_|_" + else showChar c) + `extQ` + (\(a :: String) -> if n == 1 then id else + if isBottom a then showString "_|_" + else gShowsPrec True (pred n) minPrec a + ) + ) a + | isList a && isAtom a = when' (not insideList) (showString "[") $ + showString "]" -- End of list. + | isList a = when' (not insideList) (showString "[") $ + gmapQr (.) id + ( gShowsPrec False (pred n) minPrec + `extQ` + (\(a :: a) -> + if n == 1 then id + else if isBottom a then showString "_|_" + else (if not (isAtom a) then showString ", " + else id) . + gShowsPrec True (pred n) minPrec a + ) + ) a + | isInfix a = showParen (not (isAtom a) && p > appPrec) $ + -- We know that we have at least two args, + -- because otherwise we would have a function. + let (arg1:arg2:rest) = + continueR (:) [] (succ appPrec) a + in (showParen (not (null rest)) $ + arg1 .^. showCon a .^. arg2 + ) . drive rest + | 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) + +drive = foldr (.) id +nil = showString "" +f .^. g = f . showChar ' ' . g +appPrec = 10 +minPrec = 0 +-- 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 +isAtom a = glength a == 0 +isPrimitive a = not $ isAlgType (dataTypeOf a) +isInfix a = if isPrimitive a then + False + else + constrFixity (toConstr a) == Infix +wrap s = \s' -> s . s' . s +when' b s = if b then (s .) else (id .) diff --git a/Test/ChasingBottoms/ApproxShow/Tests.hs b/Test/ChasingBottoms/ApproxShow/Tests.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/ApproxShow/Tests.hs @@ -0,0 +1,52 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- | Tests of the functions in "Test.ChasingBottoms.ApproxShow". + +module Test.ChasingBottoms.ApproxShow.Tests (tests) where + +import Test.ChasingBottoms.ApproxShow +import Test.ChasingBottoms.IsBottom +import Data.Generics + +data T = L | B T T deriving (Typeable, Data) + +left = B left L + +data Q a = Q a ::: a | Q deriving (Typeable, Data) + +pr n x template = do + let s = approxShow n x + putStr $ show (s == template) + putStr " |" + putStr s + putStrLn "|" + +tst n x template = approxShow n x == template + +tests :: [Bool] +tests = + [ tst 4 left "B (B (B (B _ _) L) L) L" + , tst 4 (bottom :: Bool) "_|_" + , tst 4 not "" + , tst 4 ('a','b') "('a', 'b')" + , tst 1 ('a','b') "(_, _)" + , tst 4 (Q ::: 'a' ::: 'b' ::: 'c') "((Q ::: 'a') ::: 'b') ::: 'c'" + , tst 2 (Q ::: 'a' ::: 'b' ::: 'c') "(_ ::: _) ::: 'c'" + , tst 4 "abc" "\"abc\"" + , tst 4 [True, False, False] "[True, False, False]" + , tst 2 "abc" "\"a_" + , tst 2 [True, False, False] "[True, _" + , tst 1 "" "\"\"" + , tst 1 ([] :: [Bool]) "[]" + , tst 0 "" "_" + , tst 0 ([] :: [Bool]) "_" + , tst 4 ('a' : bottom : bottom) "\"a_|__|_" + , tst 4 ('a' : bottom : bottom : []) "\"a_|__|_\"" + , tst 4 [True, bottom] "[True, _|_]" + , tst 4 (True : bottom : bottom) "[True, _|__|_" + , tst 4 (bottom ::: bottom ::: 'b' ::: 'c') "((_|_ ::: _|_) ::: 'b') ::: 'c'" + , tst 2 ('a' : bottom : bottom) "\"a_" + , tst 2 [True, bottom] "[True, _" + , tst 2 (True : bottom : bottom) "[True, _" + , tst 2 (bottom ::: bottom ::: 'b' ::: 'c') "(_ ::: _) ::: 'c'" + ] diff --git a/Test/ChasingBottoms/ContinuousFunctions.hs b/Test/ChasingBottoms/ContinuousFunctions.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/ContinuousFunctions.hs @@ -0,0 +1,463 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- TODO: Can we pattern match on functions? +-- What about functions of several arguments? Can we have interleaved +-- pattern matching? Do we need to use currying to achieve this? What +-- limitations does that lead to? +-- TODO: getMatches: What happens with infinite input? Hmm... We do want the +-- possibility of non-termination, right? +-- TODO: getMatches: Frequencies? +-- TODO: match: Document limitations. Can functions be handled? + +-- | +-- Module : Test.ChasingBottoms.ContinuousFunctions +-- Copyright : (c) Nils Anders Danielsson 2005-2007 +-- License : See the file LICENCE. +-- +-- Maintainer : http://www.cs.chalmers.se/~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./ +-- +-- 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 +-- than if more general functions are used, though. +-- +-- Using 'isBottom' it is relatively easy to generate possibly +-- non-strict functions that are, in general, not monotone. For +-- 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) +-- +-- we can generate possibly non-strict functions from 'Bool' to +-- 'Integer' using @function coBool integer@. There is a high +-- likelihood that the functions generated are not monotone, though. +-- The reason that we can get non-monotone functions in a language +-- like Haskell is that we are using the impure function 'isBottom'. +-- +-- 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. +-- +-- By avoiding 'isBottom' and, unlike the standard 'coarbitrary' +-- functions, deferring some pattern matches, we can generate +-- continuous, possibly non-strict functions. There are two steps +-- involved in generating a continuous function using the framework +-- defined here. +-- +-- (1) First the argument to the function is turned into a +-- 'PatternMatch'. A 'PatternMatch' wraps up the pattern match on +-- the top-level constructor of the argument, plus all further +-- pattern matches on the children of the argument. Just like when +-- 'coarbitrary' is used a pattern match is represented as a +-- generator transformer. The difference here is that there is not +-- 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 +-- transformation application is wrapped up in the function +-- 'transform'. +-- +-- The net result of this is that some pattern matches are performed +-- later, or not at all, so functions can be lazy. +-- +-- Here is an example illustrating typical use of this framework: +-- +-- > data Tree a +-- > = Branch (Tree a) (Tree a) +-- > | Leaf a +-- > deriving (Show, Typeable, Data) +-- > +-- > finiteTreeOf :: MakeResult a -> MakeResult (Tree a) +-- > finiteTreeOf makeResult = sized' tree +-- > where +-- > tree size = transform $ +-- > if size == 0 then +-- > baseCase +-- > else +-- > frequency' [ (1, baseCase) +-- > , (1, liftM2 Branch tree' tree') +-- > ] +-- > where +-- > tree' = tree (size `div` 2) +-- > +-- > baseCase = +-- > frequency' [ (1, return bottom) +-- > , (2, liftM Leaf makeResult) +-- > ] +-- +-- Note the use of 'transform'. To use this function to generate +-- functions of type @Bool -> Tree Integer@ we can use +-- +-- > forAll (functionTo (finiteTreeOf flat)) $ +-- > \(f :: Bool -> Tree Integer) -> +-- > ... + +module Test.ChasingBottoms.ContinuousFunctions + ( -- * Basic framework + function + , functionTo + , PatternMatch(..) + , GenTransformer + , MakePM + , MakeResult + , transform + -- * Liftings of some QuickCheck functionality + , lift' + , arbitrary' + , choose' + , elements' + , oneof' + , frequency' + , sized' + , resize' + -- * Generic @MakePM@ + , match + -- * Some @MakeResult@s + , flat + , finiteListOf + , infiniteListOf + , listOf + ) where + +import Test.QuickCheck +import Data.Sequence as Seq +import Data.Foldable as Seq (foldr) +import Prelude as P hiding (concat) +import Test.ChasingBottoms.IsBottom +import Control.Monad +import Control.Monad.Reader +import Control.Arrow +import System.Random +import Data.Generics +import qualified Data.List as L + +------------------------------------------------------------------------ +-- Generation of functions + +-- | Generator for continuous, not necessarily strict functions. +-- Functions are generated by first generating pattern matches, and +-- then generating a result. + +function :: MakePM a -> MakeResult b -> Gen (a -> b) +function makePM makeResult = + promote $ \a -> run makeResult (singleton $ makePM a) + +-- | 'functionTo' specialises 'function': +-- +-- @ +-- 'functionTo' = 'function' 'match' +-- @ + +functionTo :: Data a => MakeResult b -> Gen (a -> b) +functionTo = function match + +------------------------------------------------------------------------ +-- Pattern matching + +-- | 'PatternMatch' packages up the possible outcomes of a pattern +-- match in a style suitable for generating functions. A pattern match +-- is a generator ('Gen') transformer based on the top-level +-- constructor, and a sequence (see +-- ) of +-- 'PatternMatch'es based on the children of that constructor. + +data PatternMatch + = PatternMatch { apply :: GenTransformer + -- ^ A generator transformer, in the style of 'coarbitrary'. + , more :: Seq PatternMatch + -- ^ Further pattern matches made possible by this + -- match. + } + +-- | The type of a generator transformer. + +type GenTransformer = forall a. Gen a -> Gen a + +-- | This newtype is (currently) necessary if we want to use +-- 'GenTransformer' as an argument to a type constructor. + +newtype GenTransformer' = GenT GenTransformer + +-- | The type of a 'PatternMatch' generator. + +type MakePM a = a -> PatternMatch + +------------------------------------------------------------------------ +-- Generic MakePM + +-- These functions provided inspiration for the generic one below. + +matchFlat :: Arbitrary a => MakePM a +matchFlat a = PatternMatch { apply = coarbitrary a, more = empty } + +data Tree a + = Branch (Tree a) (Tree a) + | Leaf a + deriving (Show, Typeable, Data) + +matchTree :: MakePM a -> MakePM (Tree a) +matchTree match t = PatternMatch { apply = toVariant t, more = moreT t } + where + toVariant (Branch {}) = variant 1 + toVariant (Leaf {}) = variant 0 + + moreT (Branch l r) = fromList [matchTree match l, matchTree match r] + moreT (Leaf x) = singleton (match x) + +-- | Generic implementation of 'PatternMatch' construction. + +match :: forall a. Data a => MakePM a +match x = PatternMatch + { apply = toVariant x + , 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." + + more :: forall a. Data a => a -> Seq PatternMatch + more = gmapQr (<|) empty match + +------------------------------------------------------------------------ +-- MakeResult monad + +-- | Monad for generating results given previously generated pattern +-- matches. +-- +-- A @'MakeResult' a@ should be implemented almost as other generators for +-- the type @a@, with the difference that 'transform' should be +-- used wherever the resulting function should be allowed to pattern +-- match (typically for each constructor emitted). See example above. + +-- Note that we do not want to export a 'MonadReader' instance, so we +-- cannot define one... + +newtype MakeResult a + = MR { unMR :: ReaderT PatternMatches Gen a } + deriving (Functor, Monad) + +type PatternMatches = Seq PatternMatch + +-- | Lowering of a 'MakeResult'. + +run :: MakeResult a -> PatternMatches -> Gen a +run mr pms = runReaderT (unMR mr) pms + +-- | Lifting of a 'Gen'. + +lift' :: Gen a -> MakeResult a +lift' gen = MR $ lift gen + +-- | Returns the 'PatternMatches' in scope. + +getPMs :: MakeResult PatternMatches +getPMs = MR ask + +withPMs :: (PatternMatches -> Gen a) -> MakeResult a +withPMs f = do + pms <- getPMs + lift' $ f pms + +-- | 'transform' makes sure that the pattern matches get to influence +-- the generated value. See 'MakeResult'. + +transform :: MakeResult a -> MakeResult a +transform makeResult = withPMs $ \pms -> do + (GenT trans, keep) <- getMatches pms + trans (run makeResult keep) + +-- | Extracts some pattern matches to trigger right away. These +-- triggered pattern matches may result in new pattern matches which +-- may in turn also be triggered, and so on. + +getMatches :: Seq PatternMatch -> Gen (GenTransformer', Seq PatternMatch) +getMatches pms = do + -- Throw away pattern matches with probability 0.1. + (_, pms') <- partition 9 pms + -- Use pattern matches with probability 0.33. + (use, keep) <- partition 2 pms' + let transform = compose $ fmap apply use + further = concat $ fmap more use + if Seq.null further then + return (GenT transform, keep) + else do + (GenT transform', keep') <- getMatches further + return (GenT (transform . transform'), keep >< keep') + +------------------------------------------------------------------------ +-- Sequence helpers + +-- | Concatenates arguments. + +concat :: Seq (Seq a) -> Seq a +concat = Seq.foldr (><) empty + +-- | Composes arguments. + +compose :: Seq (a -> a) -> a -> a +compose = Seq.foldr (.) id + +-- | Partitions a 'Seq'. The first argument (a positive integer) is +-- 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 + EmptyL -> return (empty, empty) + x :< xs -> do + (ys, zs) <- partition freq xs + frequency [ (1, return (x <| ys, zs)) + , (freq, return (ys, x <| zs)) + ] + +------------------------------------------------------------------------ +-- Lifting of QuickCheck's Gen monad + +-- | Lifting of 'arbitrary'. + +arbitrary' :: Arbitrary a => MakeResult a +arbitrary' = lift' arbitrary + +-- | Lifting of 'choose'. + +choose' :: Random a => (a, a) -> MakeResult a +choose' = lift' . choose + +-- | Lifting of 'elements'. + +elements' :: [a] -> MakeResult a +elements' = lift' . elements + +-- | Lifting of 'oneof'. + +oneof' :: [MakeResult a] -> MakeResult a +oneof' mrs = withPMs $ \pms -> oneof $ map (\mr -> run mr pms) mrs + +-- | Lifting of 'frequency'. + +frequency' :: [(Int, MakeResult a)] -> MakeResult a +frequency' freqs = withPMs $ \pms -> + frequency $ map (id *** flip run pms) freqs + +-- | Lifting of 'sized'. + +sized' :: (Int -> MakeResult a) -> MakeResult a +sized' mr = withPMs $ \pms -> sized (\size -> run (mr size) pms) + +-- | Lifting of 'resize'. + +resize' :: Int -> MakeResult a -> MakeResult a +resize' n mr = withPMs $ \pms -> resize n (run mr pms) + +------------------------------------------------------------------------ +-- Some predefined generators + +-- | An implementation of @'MakeResult' a@ which is suitable when @a@ +-- is flat and has an 'Arbitrary' instance. Yields bottoms around 10% +-- of the time. + +flat :: Arbitrary a => MakeResult a +flat = transform $ + frequency' [ (1, return bottom) + , (9, arbitrary') + ] + +-- | This 'MakeResult' yields finite partial lists. + +finiteListOf :: MakeResult a -> MakeResult [a] +finiteListOf makeResult = sized' list + where + list size = transform $ + if size == 0 then + baseCase + else + frequency' [ (1, baseCase) + , (9, liftM2 (:) makeResult (list (size - 1))) + ] + + baseCase = + frequency' [(1, return bottom), (1, return [])] + +-- | This 'MakeResult' yields infinite partial lists. + +infiniteListOf :: MakeResult a -> MakeResult [a] +infiniteListOf makeResult = transform $ + liftM2 (:) makeResult (infiniteListOf makeResult) + +-- | This 'MakeResult' yields finite or infinite partial lists. + +listOf :: MakeResult a -> MakeResult [a] + -- Not really necessary to have a transform here... +listOf makeResult = transform $ + oneof' [ finiteListOf makeResult + , infiniteListOf makeResult + ] + +------------------------------------------------------------------------ +-- Failed attempt at a generic implementation of MakeResult + +-- Main problem: Getting the frequencies right. Lists are very short +-- right now. + +-- Other problem: Int and Float. + +-- Further remark: We need finite and infinite versions of this +-- function. + +makeResult :: forall a. Data a => MakeResult a +makeResult = transform (frequency' $ (1, return bottom) : others) + where + others = case dataTypeRep (dataTypeOf (undefined :: a)) of + AlgRep constrs -> + map (handle (L.genericLength constrs)) constrs + IntRep -> [(9, cast' (arbitrary' :: MakeResult Integer))] + FloatRep -> [(9, cast' (arbitrary' :: MakeResult Double))] + StringRep -> nonBottomError "makeResult: StringRep." + NoRep -> nonBottomError "makeResult: NoRep." + + handle noConstrs con = + (freq, fromConstrM makeResult con :: MakeResult a) + where noArgs = glength (fromConstr con :: a) + -- Aim for at most 10% bottoms (on average). + freq = 1 `max` ceiling (9 / noConstrs) + + cast' gen = flip fmap gen $ \x -> case cast x of + Just x' -> x' + Nothing -> nonBottomError $ + "makeResult: Cannot handle Int and Float." ++ + " Use Integer or Double instead." diff --git a/Test/ChasingBottoms/ContinuousFunctions/Tests.hs b/Test/ChasingBottoms/ContinuousFunctions/Tests.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/ContinuousFunctions/Tests.hs @@ -0,0 +1,219 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- TODO: Tests passed even though for finiteTreeOf and finiteListOf +-- transform was only applied once at the top-level! + +-- | Tests for "Test.ChasingBottoms.ContinuousFunctions". So far the +-- tests are rather weak. + +module Test.ChasingBottoms.ContinuousFunctions.Tests (tests) where + +import Test.ChasingBottoms.ContinuousFunctions +import Test.ChasingBottoms.IsBottom +import Test.ChasingBottoms.SemanticOrd +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.Monad +import Data.List +import Data.Ratio + +------------------------------------------------------------------------ +-- Example data type + +finiteTreeOf :: MakeResult a -> MakeResult (Tree a) +finiteTreeOf makeResult = sized' tree + where + tree size = transform $ + if size == 0 then + baseCase + else + frequency' [ (1, baseCase) + , (1, liftM2 Branch tree' tree') + ] + where + tree' = tree (size `div` 2) + + baseCase = + frequency' [ (1, return bottom) + , (2, liftM Leaf makeResult) + ] + +------------------------------------------------------------------------ +-- Helpers + +integer :: Gen Integer +integer = frequency [ (1, return bottom) + , (9, arbitrary) + ] + +length' :: Num b => [a] -> b +length' xs | isBottom xs = 0 +length' [] = 1 +length' (x:xs) = 1 + length' xs + +depth :: (Ord b, Num b) => Tree a -> b +depth t | isBottom t = 0 +depth (Leaf {}) = 1 +depth (Branch l r) = 1 + (depth l `max` depth r) + +------------------------------------------------------------------------ +-- Tests + +-- Interesting properties for the function generators: +-- +-- * Surjectivity. +-- +-- * Decent distribution. +-- +-- How do we test these properties? + +testDistribution test t = do + result <- run t testOptions + 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 + } + + +spread n args = (uniqueShare >= 3%4, "uniqueShare: " ++ show uniqueShare) + where noUniqueArgs = length . group . sort $ args + uniqueShare = noUniqueArgs % n + +len max avg short n args = + ( 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 + +-- | We want to make sure that we can generate many different kinds of +-- lazy functions. + +prop_many_functions_rather_lazy = testDistribution spread $ + forAll (functionTo (finiteTreeOf (finiteTreeOf flat))) $ + \(f :: Tree Integer -> Tree (Tree Bool)) -> + f bottom /=! bottom && f (Leaf bottom) + collect (map (approxShow 100 . f) [bottom, Leaf bottom, Leaf 1]) $ + True + +-- | The generated lists should not be too short. + +prop_lists_have_decent_length = testDistribution (len 20 6 5) $ + forAll (functionTo (finiteListOf flat)) $ \(f :: Integer -> [Bool]) -> + forAll integer $ \(i :: Integer) -> + collect (length' (f i) :: Integer) $ + True + +-- | The generated trees should not be too shallow. + +prop_trees_have_decent_depth = testDistribution (len 6 2 2) $ + forAll (functionTo (finiteTreeOf flat)) $ \(f :: Integer -> Tree Bool) -> + forAll integer $ \(i :: Integer) -> + collect (depth (f i) :: Integer) $ + True + +-- | In one version of Data.Generics the following equations were +-- valid: +-- +-- * @'toConstr' ('bottom' :: ()) = 'toConstr' ()@ +-- +-- * @'toConstr' ('bottom' :: One) = _|_@ +-- +-- 'toConstr' should be strict. There is a workaround for this (using +-- seq) in "Test.ChasingBottoms.ContinuousFunctions", and the +-- following two tests check that this workaround works. + +data One + = One + deriving (Typeable, Data) + +prop_some_lazy_unit = + forAll (functionTo (finiteTreeOf flat)) $ \(f :: () -> Tree Bool) -> + f bottom + True + +prop_some_lazy_One = + forAll (functionTo (finiteTreeOf flat)) $ \(f :: One -> Tree Bool) -> + f bottom + True + +-- | Example from documentation. Here mostly to check that it type +-- checks. + +prop_example_works = + forAll (functionTo (finiteTreeOf flat)) $ + \(f :: Bool -> Tree Integer) -> + f bottom <=! f True && f bottom <=! f False + +-- | Generated functions should be monotone. + +prop_functions_monotone = + forAll (functionTo (finiteListOf flat)) + $ \(f :: Tree Integer -> [Bool]) -> + forAll (pair (Gen.finiteTreeOf Gen.integer) + (Gen.geTreeOf Gen.integer Gen.geInteger Gen.finiteTreeOf)) + $ \(x, y) -> + x <=! y && f x <=! f y + +------------------------------------------------------------------------ +-- | All tests collected together. + +tests :: IO Bool +tests = do + b1 <- fmap and $ sequence theIOTests + b2 <- runQuickCheckTests $ map run $ concat theTests + return (b1 && b2) + where + theIOTests :: [IO Bool] + theIOTests = [ prop_many_functions_rather_lazy + , prop_lists_have_decent_length + , prop_trees_have_decent_depth + ] + + theTests :: [[Property]] + theTests = [ [ prop_example_works + , prop_some_lazy_unit + , prop_some_lazy_One + , prop_functions_monotone + ] + ] + +------------------------------------------------------------------------ +-- Manual inspection of function tables + +viewFun :: (ApproxShow b, Data a) => MakeResult b -> [a] -> IO () +viewFun (makeResult :: MakeResult b) (inputs :: [a]) = test $ + forAll (functionTo makeResult) $ \(f :: a -> b) -> + collect (map (approxShow 5 . f) inputs) $ True + +bool = undefined :: Bool +int = undefined :: Int +float = undefined :: Float +treeOfBool = undefined :: Tree Bool + +test0 = viewFun (flat :: MakeResult Bool) [bottom, False, True] +test1 = viewFun (finiteTreeOf flat :: MakeResult (Tree Bool)) + [bottom, False, True] +test2 = viewFun (finiteTreeOf flat :: MakeResult (Tree Bool)) + [bottom, Leaf bottom, Leaf False] + +test4 = viewFun (flat :: MakeResult Int) [bottom, False, True] +test5 = viewFun (flat :: MakeResult Float) [bottom, False, True] diff --git a/Test/ChasingBottoms/IsBottom.hs b/Test/ChasingBottoms/IsBottom.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/IsBottom.hs @@ -0,0 +1,103 @@ +-- | +-- Module : Test.ChasingBottoms.IsBottom +-- Copyright : (c) Nils Anders Danielsson 2004-2007 +-- License : See the file LICENCE. +-- +-- Maintainer : http://www.cs.chalmers.se/~nad/ +-- Stability : experimental +-- Portability : non-portable (exceptions) +-- + +module Test.ChasingBottoms.IsBottom + ( isBottom + , bottom + , nonBottomError + , isBottomTimeOut + ) where + +import Prelude hiding (catch) +import Control.Exception (catch, throw, Exception(..), evaluate) +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. +-- +-- 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). + +-- Should we use throw or throwIO below? +-- It doesn't seem to matter, and I don't think it matters, but +-- using throw won't give us any problems. + +-- Check out a discussion about evaluate around +-- http://www.haskell.org/pipermail/glasgow-haskell-users/2002-May/003393.html. + +-- From the docs: +-- evaluate undefined `seq` return () ==> return () +-- catch (evaluate undefined) (\e -> return ()) ==> return () + +isBottom :: a -> Bool +isBottom = isBottomTimeOut Nothing + +-- | 'bottom' generates a bottom that is suitable for testing using +-- 'isBottom'. +bottom :: a +bottom = error "_|_" + +-- | @'nonBottomError' s@ raises an exception ('AssertionFailed') that +-- is not caught by 'isBottom'. Use @s@ to describe the exception. + +nonBottomError :: String -> a +nonBottomError = throw . AssertionFailed + +-- | @'isBottomTimeOut' timeOutLimit@ works like 'isBottom', but if +-- @timeOutLimit@ is @'Just' lim@, then computations taking more than +-- @lim@ seconds are also considered to be equal to bottom. Note that +-- this is a very crude approximation of what a bottom is. Also note +-- 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 :: 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 + where + maybeTimeOut io = case timeOutLimit of + Nothing -> do + io + return False + Just lim -> do + result <- T.timeOut lim io + 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. diff --git a/Test/ChasingBottoms/IsBottom/Tests.hs b/Test/ChasingBottoms/IsBottom/Tests.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/IsBottom/Tests.hs @@ -0,0 +1,79 @@ +-- | Tests of the functions in "Test.ChasingBottoms.IsBottom". +-- +-- Note that the warnings given when compiling this module are +-- intentional. See the internal comments for more information. + +module Test.ChasingBottoms.IsBottom.Tests (tests) where + +import Test.ChasingBottoms.IsBottom +import System.IO.Unsafe +import Data.Array +import System.Exit +import qualified Control.Exception as E + +isException f = unsafePerformIO $ + (E.evaluate f >> return False) `E.catch` const (return True) + +bot = bot +notbot x = notbot x + +data T' a = L' | B' (T' a) (T' a) deriving Eq + +instance Monad T' + +leftInfinite' = B' leftInfinite' L' + +infiniteRecursion = leftInfinite' == leftInfinite' + +data A2 = A2 { aaa :: A2 } | C { ccc :: A2 } + +tests :: [Bool] +tests = + -- Basic cases. + [ isBottom bottom + , isBottom undefined + , isBottom (error "...") + -- This sometimes leads to a stack overflow. + -- , isBottom bot + + -- const bottom /= bottom. + , not (isBottom notbot) + , not (isBottom (const bottom)) + + -- Other types also lifted. + , not (isBottom (bottom, bottom)) + , not (isBottom (Just bottom)) + + -- Pattern match failure. + , isBottom (let (x, y) = bottom in x :: Bool) + , isBottom (let Just x = Nothing in x :: Char) + + -- Nonterminating, but not bottom. + , not (isBottom [1..]) + + -- Missing methods. + -- Skip this test to avoid compiler warnings. + , isBottom (L' >> L') + + -- Array stuff. + , isBottom (array (1,0) [] ! 0) + , isBottom (array (0,0) [] ! 0) + + -- Record stuff. + -- Skip the first one to avoid compiler warnings. + , isBottom (let x = A2 {} in aaa x) + , isBottom (let x = A2 { aaa = x } in ccc x) + , isBottom (let x = A2 { aaa = x } in x { ccc = x }) + + -- Infinite recursion, no data produced, should yield stack + -- overflow... + -- Not a quick test (on some machines, anyway). And the result + -- might be optimisation dependent. + -- , isException (isBottom infiniteRecursion) + + -- Some other exceptions that are not caught, including + -- nonBottomError. + , isException (isBottom (unsafePerformIO $ exitWith ExitSuccess)) + , isException (isBottom (1 `div` 0)) + , isException (nonBottomError "...") + ] diff --git a/Test/ChasingBottoms/IsType.hs b/Test/ChasingBottoms/IsType.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/IsType.hs @@ -0,0 +1,41 @@ +-- | +-- Module : Test.ChasingBottoms.IsType +-- Copyright : (c) Nils Anders Danielsson 2004-2007 +-- License : See the file LICENCE. +-- +-- Maintainer : http://www.cs.chalmers.se/~nad/ +-- Stability : experimental +-- Portability : non-portable (GHC-specific) +-- +-- Internal helper functions. + +module Test.ChasingBottoms.IsType + ( isFunction + , isTuple + , isList + , isString + ) where + +import Data.Typeable + +-- | '@isFunction@ f' returns 'True' iff the top level \"constructor\" +-- of @f@ is a function arrow. +isFunction :: Typeable a => a -> Bool +isFunction f = con f == con not -- TyCon is abstract. + +con :: Typeable a => a -> TyCon +con = typeRepTyCon . typeOf + +-- | This function is rather fragile, but should be OK. It is only +-- used by "Test.ChasingBottoms.ApproxShow", which should only be used +-- 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) + +isString :: Typeable a => a -> Bool +isString x = isList x && typeRepArgs (typeOf x) == typeRepArgs (typeOf "") + +isList :: Typeable a => a -> Bool +isList x = con x == con "" diff --git a/Test/ChasingBottoms/IsType/Tests.hs b/Test/ChasingBottoms/IsType/Tests.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/IsType/Tests.hs @@ -0,0 +1,26 @@ +-- | Tests of the functions in "Test.ChasingBottoms.IsType". + +module Test.ChasingBottoms.IsType.Tests (tests) where + +import Test.ChasingBottoms.IsType + +tests :: [Bool] +tests = + -- isFunction identifies functions. + [ isFunction (id :: Char -> Char) == True + , isFunction ((==) :: Char -> Char -> Bool) == True + , isFunction 'c' == False + , isFunction [not] == False + + , isTuple [not] == False + , isTuple () == False + , isTuple ('a', 'c') == True + + , isList "" == True + , isList [not] == True + , isList ('a', 'c') == False + + , isString "" == True + , isString [not] == False + , isString ('a', 'c') == False + ] diff --git a/Test/ChasingBottoms/Nat.hs b/Test/ChasingBottoms/Nat.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/Nat.hs @@ -0,0 +1,109 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- | +-- Module : Test.ChasingBottoms.Nat +-- Copyright : (c) Nils Anders Danielsson 2004-2007 +-- License : See the file LICENCE. +-- +-- Maintainer : http://www.cs.chalmers.se/~nad/ +-- Stability : experimental +-- Portability : non-portable (GHC-specific) +-- +-- A simple implementation of natural numbers on top of 'Integer's. +-- Note that since 'Integer's are used there is no infinite natural +-- number; in other words, 'succ' is strict. + +module Test.ChasingBottoms.Nat(Nat, isSucc, fromSucc, natrec, foldN) where + +import Test.QuickCheck +import Data.Ratio ((%)) +import Data.Typeable + +default () + +-- | Natural numbers. +-- +-- No 'Data.Generics.Basics.Data' instance is provided since 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. +newtype Nat = Nat { nat2int :: Integer } deriving (Eq, Ord, Typeable) + +-- | @'isSucc' 0 == 'False'@, for other total natural numbers it is 'True'. +isSucc :: Nat -> Bool +isSucc (Nat 0) = False +isSucc _ = True + +-- | @'fromSucc' 0 == 'Nothing'@, @'fromSucc' (n+1) == 'Just' n@ for a +-- total natural number @n@. +fromSucc :: Nat -> Maybe Nat +fromSucc (Nat 0) = Nothing +fromSucc n = Just $ pred n + +-- | 'natrec' performs primitive recursion on natural numbers. +natrec :: a -> (Nat -> a -> a) -> Nat -> a +natrec g _ (Nat 0) = g +natrec g h n = let p = pred n in h p (natrec g h p) + +-- | 'foldN' is a fold on natural numbers: +-- +-- @ +-- 'foldN' g h = 'natrec' g ('curry' '$' h . 'snd') +-- @ +foldN :: a -> (a -> a) -> Nat -> a +foldN g h = natrec g (curry $ h . snd) + +steal :: (Integer -> Integer -> Integer) -> Nat -> Nat -> Nat +steal op x y = fromInteger $ (nat2int x) `op` (nat2int y) + +instance Num Nat where + (+) = steal (+) + (*) = steal (*) + x - y = let x' = nat2int x; y' = nat2int y + in if x' < y' then + error "Nat: x - y undefined if y > x." + else + fromInteger $ x' - y' + negate = error "Nat: negate undefined." + signum n = if isSucc n then 1 else 0 + abs = id + fromInteger i | i < 0 = error "Nat: No negative natural numbers." + | otherwise = Nat i + +instance Real Nat where + toRational = (%1) . nat2int + +steal2 :: (Integer -> Integer -> (Integer, Integer)) + -> Nat -> Nat -> (Nat, Nat) +steal2 op x y = let (x', y') = (nat2int x) `op` (nat2int y) + in (fromInteger x', fromInteger y') + +instance Integral Nat where + toInteger = toInteger . fromEnum + a `quotRem` b = if b == 0 then + error "Nat: quotRem undefined for zero divisors." + else + steal2 quotRem a b + a `divMod` b = if b == 0 then + error "Nat: divMod undefined for zero divisors." + else + steal2 divMod a b + +instance Enum Nat where + succ = (+ 1) + pred = subtract 1 + toEnum = fromInteger . toInteger + fromEnum = fromInteger . nat2int + -- Add tests for enumFrom and friends if the default definitions are + -- overridden. + +instance Show Nat where + showsPrec _ = showString . show . nat2int + +instance Arbitrary Nat where + arbitrary = do + n <- arbitrary :: Gen Integer + return $ fromInteger $ abs n + coarbitrary n = coarbitrary (toInteger n) diff --git a/Test/ChasingBottoms/Nat/Tests.hs b/Test/ChasingBottoms/Nat/Tests.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/Nat/Tests.hs @@ -0,0 +1,239 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- | Tests for "Test.ChasingBottoms.Nat". + +-- The automatically derived 'Typeable' instance is not tested. + +module Test.ChasingBottoms.Nat.Tests (tests) where + +import Test.ChasingBottoms.Nat +import Test.ChasingBottoms.SemanticOrd +import Test.ChasingBottoms.TestUtilities +import Test.QuickCheck +import Test.QuickCheck.Batch +import Data.Maybe +import Data.List +import Data.Ratio + +default () + +-- The default versions of succ and pred go via Ints, and hence +-- perform incorrectly in the presence of large natural numbers. Hence +-- this generator is needed. Other tests can possibly also fail in the +-- presence of large natural numbers, but QuickCheck does not handle +-- large numbers very well, especially not when coarbitrary is used, +-- so we do not use this generator for all tests. Furthermore +-- defaulting is turned off here and in Test.ChasingBottoms.Nat, and +-- that should minimise surprises. + +largeNat :: Gen Nat +largeNat = do + n <- choose (0, 2 * toInteger (maxBound :: Int)) + return (fromInteger n) + +-- Testing isSucc. + +prop_isSucc n = isSucc n == (n > 0) + +-- Testing fromSucc. + +prop_fromSucc n | n == 0 = fromSucc n == Nothing + | otherwise = fromSucc n == Just (n-1) + +-- Testing natrec. + +-- How do you test something as versatile as natrec? Well, at least we +-- can verify that we can use it to implement addition. + +prop_natrec_add m n = natrec m (\_ o -> succ o) n == m + n + +-- There is no need to test foldN, since it is specified by its +-- definition. + +-- Testing Enum. + +prop_Nat_Enum_succ = + forAll largeNat $ \n -> + succ n == n + 1 +prop_Nat_Enum_pred = + forAll largeNat $ \n -> + n > 0 ==> pred n == n - 1 + +prop_Nat_Enum_toEnum (n :: Int) = + n >= 0 ==> (toEnum n :: Nat) == fromInteger (toInteger n) +prop_Nat_Enum_fromEnum (n :: Nat) = + n <= fromInteger (toInteger (maxBound :: Int)) ==> + toInteger (fromEnum n) == toInteger n + +-- enumFrom and friends have default definitions. + +-- Testing Eq. + +prop_Nat_Eq_congruence = + eqIsCongruence arbitrary equalTo notEqualTo + (arbitrary :: Gen (Nat -> Integer)) + +equalTo (n :: Nat) = return n + +notEqualTo (n :: Nat) = do + m <- fmap succ arbitrary -- m >= 1. + if m <= n then + elements [n - m, n + m] + else + return (n + m) + +-- Testing Show. + +prop_Nat_Show (m :: Nat) = show m == show (toInteger m) + +-- Testing Ord. + +prop_Nat_Ord_total_order = ordIsTotalOrder arbitrary + equalTo notEqualTo greaterThanOrEqual + +greaterThanOrEqual (n :: Nat) = do + m <- arbitrary + return (n + m) + +-- Testing Num. + +prop_Nat_mul_iterated_sum (m :: Nat) n = + m * n == foldr (+) 0 (genericReplicate m n) + +prop_Nat_plus_assoc (m :: Nat) n o = m + (n + o) == (m + n) + o +prop_Nat_plus_comm (m :: Nat) n = m + n == n + m + +prop_Nat_mul_assoc (m :: Nat) n o = m * (n * o) == (m * n) * o +prop_Nat_mul_comm (m :: Nat) n = m * n == n * m + +prop_Nat_mul_plus_left_dist (m :: Nat) n o = m * (n + o) == m * n + m * o + +prop_Nat_mul_plus_zero (m :: Nat) = m + 0 == m +prop_Nat_mul_mul_unit (m :: Nat) = m * 1 == m + +prop_Nat_minus n = + forAll (greaterThanOrEqual n) $ \m -> + (m - n) + n == m + +prop_Nat_signum_abs (m :: Nat) = signum m * abs m == m +prop_Nat_signum_zero = (signum 0 :: Nat) == 0 + +prop_Nat_fromInteger_plus m n = + m >= 0 && n >= 0 ==> + fromInteger m + fromInteger n == (fromInteger (m + n) :: Nat) +prop_Nat_fromInteger_mul m n = + m >= 0 && n >= 0 ==> + fromInteger m * fromInteger n == (fromInteger (m * n) :: Nat) + +-- negate is undefined. + +-- Testing Integral. + +prop_Nat_to_from (m :: Nat) = fromInteger (toInteger m) == m +prop_Nat_from_to i = i >= 0 ==> toInteger (fromInteger i :: Nat) == i + +prop_Nat_quotRem (m :: Nat) n = + n /= 0 ==> m `quotRem` n == (m `quot` n, m `rem` n) +prop_Nat_divMod (m :: Nat) n = + n /= 0 ==> m `divMod` n == (m `div` n, m `mod` n) + +prop_Nat_quot_rem (m :: Nat) n = + n /= 0 ==> (m `quot` n) * n + m `rem` n == m +prop_Nat_div_mod (m :: Nat) n = + n /= 0 ==> (m `div` n) * n + m `mod` n == m + +-- Testing Real. + +prop_Nat_toRational (m :: Nat) = toRational m == toInteger m % 1 + +-- Since the implementation is based on Integers I'd like to test that +-- we can't construct values of the form "Nat i" where i is a negative +-- Integer. (This can be seen as a test of the observation function +-- toInteger.) + +prop_Nat_closed = [ unary (fromJust . fromSucc) + -- Ord + , binary max + , binary min + -- Enum + -- enumFrom and friends have default definitions. + , unary succ + , unary pred + , unary' toEnum + -- Num + , binary (+) + , binary (-) + , binary (*) + , unary negate + , unary abs + , unary signum + , unary' fromInteger + -- Integral + , binary quot + , binary rem + , binary div + , binary mod + , binary (fst .^^ quotRem) + , binary (snd .^^ quotRem) + , binary (fst .^^ divMod) + , binary (snd .^^ divMod) + ] + where + ok (n :: Nat) = (toInteger n >= 0) <=! True + + unary (f :: Nat -> Nat) = unary' f + + unary' f = + forAll arbitrary $ \x -> + ok (f x) + + binary f = + forAll arbitrary $ \(m :: Nat) -> + forAll arbitrary $ \(n :: Nat) -> + ok (f m n) + + f .^^ g = \x y -> f (g x y) + +-- | All tests collected together. + +tests :: IO Bool +tests = runQuickCheckTests theTests + where + theTests = map run (concat testLists) ++ singleTests + + singleTests = + [ run prop_isSucc + , run prop_fromSucc + , run prop_natrec_add + , run prop_Nat_Enum_succ + , run prop_Nat_Enum_pred + , run prop_Nat_Enum_toEnum + , run prop_Nat_Enum_fromEnum + , run prop_Nat_Show + , run prop_Nat_mul_iterated_sum + , run prop_Nat_plus_assoc + , run prop_Nat_plus_comm + , run prop_Nat_mul_assoc + , run prop_Nat_mul_comm + , run prop_Nat_mul_plus_left_dist + , run prop_Nat_mul_plus_zero + , run prop_Nat_mul_mul_unit + , run prop_Nat_minus + , run prop_Nat_signum_abs + , run prop_Nat_signum_zero + , run prop_Nat_fromInteger_plus + , run prop_Nat_fromInteger_mul + , run prop_Nat_to_from + , run prop_Nat_from_to + , run prop_Nat_quotRem + , run prop_Nat_divMod + , run prop_Nat_quot_rem + , run prop_Nat_div_mod + , run prop_Nat_toRational + ] + + testLists = + [ prop_Nat_Eq_congruence + , prop_Nat_Ord_total_order + , prop_Nat_closed + ] diff --git a/Test/ChasingBottoms/SemanticOrd.hs b/Test/ChasingBottoms/SemanticOrd.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/SemanticOrd.hs @@ -0,0 +1,253 @@ +{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} + +-- | +-- Module : Test.ChasingBottoms.SemanticOrd +-- Copyright : (c) Nils Anders Danielsson 2004-2007 +-- License : See the file LICENCE. +-- +-- Maintainer : http://www.cs.chalmers.se/~nad/ +-- Stability : experimental +-- Portability : non-portable (GHC-specific) +-- +-- Generic semantic equality and order. The semantic order referred +-- to is that of a typical CPO for Haskell types, where e.g. @('True', +-- 'bottom') '<=!' ('True', 'False')@, but where @('True', 'True')@ +-- and @('True', 'False')@ are incomparable. +-- +-- The implementation is based on 'isBottom', and has the same +-- limitations. Note that non-bottom functions are not handled by any +-- of the functions described below. +-- +-- One could imagine using QuickCheck for testing equality of +-- functions, but I have not managed to tweak the type system so that +-- it can be done transparently. + +module Test.ChasingBottoms.SemanticOrd + ( Tweak(..) + , noTweak + , SemanticEq(..) + , SemanticOrd(..) + ) where + +import Data.Generics +import Test.ChasingBottoms.IsBottom +import Test.ChasingBottoms.IsType +import qualified Data.Maybe as Maybe +import Test.ChasingBottoms.Nat +import Test.ChasingBottoms.Approx + +infix 4 =!, >!, /=! +infix 5 \/! +infixl 5 /\! + +-- | The behaviour of some of the functions below can be tweaked. + +data Tweak = Tweak + { approxDepth :: Maybe Nat + -- ^ If equal to @'Just' n@, an @'approxAll' n@ is performed on + -- all arguments before doing whatever the function is supposed to + -- be doing. + , timeOutLimit :: Maybe Int + -- ^ If equal to @'Just' n@, then all computations that take more + -- than @n@ seconds to complete are considered to be equal to + -- 'bottom'. This functionality is implemented using + -- 'isBottomTimeOut'. + } + deriving (Eq, Ord, Show) + +-- | No tweak (both fields are 'Nothing'). + +noTweak :: Tweak +noTweak = Tweak + { approxDepth = Nothing + , timeOutLimit = Nothing + } + +-- | 'SemanticEq' contains methods for testing whether two terms are +-- semantically equal. + +-- Note that we only allow a -> a -> Bool here, not a -> b -> +-- Bool. Otherwise we would allow behaviour like the following: +-- > (bottom : bottom :: [Int]) <=!! ("tr" :: String) +-- True + +class SemanticEq a where + (==!), (/=!) :: a -> a -> Bool + semanticEq :: Tweak -> a -> a -> Bool + + (/=!) = \x y -> not (x ==! y) + (==!) = semanticEq noTweak + +-- | 'SemanticOrd' contains methods for testing whether two terms are +-- related according to the semantic domain ordering. + +class SemanticEq a => SemanticOrd a where + (=!), (>!) :: a -> a -> Bool + + semanticCompare :: Tweak -> a -> a -> Maybe Ordering + -- ^ @'semanticCompare' tweak x y@ returns 'Nothing' if @x@ and @y@ are + -- incomparable, and @'Just' o@ otherwise, where @o :: 'Ordering'@ + -- represents the relation between @x@ and @y@. + + (\/!) :: a -> a -> Maybe a + (/\!) :: a -> a -> a + semanticJoin :: Tweak -> a -> a -> Maybe a + semanticMeet :: Tweak -> a -> a -> a + -- ^ @x '\/!' y@ and @x '/\!' y@ compute the least upper and greatest + -- lower bounds, respectively, of @x@ and @y@ in the semantical + -- domain ordering. Note that the least upper bound may not always + -- exist. + -- This functionality was implemented just because it was + -- possible (and to provide analogues of 'max' and 'min' in the 'Ord' + -- class). If anyone finds any use for it, please let me know. + + (>=!) = flip (<=!) + ( x <=! y && x /=! y + (>!) = \x y -> x >=! y && x /=! y + + x <=! y = case semanticCompare noTweak x y of + Just LT -> True + Just EQ -> True + _ -> False + + (\/!) = semanticJoin noTweak + (/\!) = semanticMeet noTweak + +instance Data a => SemanticEq a where + semanticEq tweak = liftAppr tweak semanticEq' + +instance Data a => SemanticOrd a where + semanticCompare tweak = liftAppr tweak semanticCompare' + where + semanticCompare' tweak x y = + case ( semanticEq' tweak x y + , semanticLE' tweak x y + , semanticLE' tweak y x ) of + (True, _, _) -> Just EQ + (_, True, _) -> Just LT + (_, _, True) -> Just Prelude.GT + (_, _, _) -> Nothing + semanticJoin tweak = liftAppr tweak semanticJoin' + semanticMeet tweak = liftAppr tweak semanticMeet' + +liftAppr :: (Data a, Data b) => Tweak -> (Tweak -> a -> a -> b) -> a -> a -> b +liftAppr tweak op x y = op tweak (appr x) (appr y) + where appr = maybe id approxAll (approxDepth tweak) + +------------------------------------------------------------------------ + +type Rel' = (Data a, Data b) => Tweak -> a -> b -> Bool +type Rel = (Data a, Data b) => a -> b -> Bool + +semanticEq', semanticLE' :: Rel' + +semanticEq' tweak a b = case ( isBottomTimeOut (timeOutLimit tweak) a + , isBottomTimeOut (timeOutLimit tweak) b ) of + (True, True) -> True + (False, False) -> allOK (semanticEq' tweak) a b + _ -> False + +semanticLE' tweak a b = case ( isBottomTimeOut (timeOutLimit tweak) a + , isBottomTimeOut (timeOutLimit tweak) b ) of + (True, _) -> True + (False, False) -> allOK (semanticLE' tweak) a b + _ -> False + +allOK :: Rel -> Rel +allOK op a b = + -- It's really enough to test just a, since we restrict the types + -- above, but why complicate things? + if isFunction a || isFunction b then + -- cast' a `fop` cast' b + nonBottomError + "The generic versions of (==!) and friends do not accept non-bottom \ + \functions." + else + a =^= b && childrenOK op a b + +-- Check top-level. Note that this test always fails for "function +-- constructors". +(=^=) :: Rel +a =^= b = toConstr a == toConstr b + +-- Check children. +childrenOK :: Rel -> Rel +childrenOK op = and .|.. gzipWithQ (\x y -> op x y) + where f .|.. g = \x y -> f (g x y) + +------------------------------------------------------------------------ + +semanticMeet' :: (Data a, Data b) => Tweak -> a -> b -> b +semanticMeet' tweak a (b :: b) = + if isBottomTimeOut (timeOutLimit tweak) a || + isBottomTimeOut (timeOutLimit tweak) b then + bottom + else if isFunction a || isFunction b then + nonBottomError "/\\! does not handle non-bottom functions." + else if not (a =^= b) then + 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 + , isBottomTimeOut (timeOutLimit tweak) b ) of + (True, True) -> Just bottom + (True, False) -> Just b + (False, True) -> cast a + (False, False) + | isFunction a || isFunction b -> + nonBottomError "\\/! does not handle non-bottom functions." + | not (a =^= b) -> Nothing + | otherwise -> gzipWithM (\x y -> semanticJoin' tweak x y) a b + +------------------------------------------------------------------------ + +-- Variant of cast. + +-- cast' :: (Typeable a, Typeable b) => a -> b +-- cast' = Maybe.fromJust . cast + +------------------------------------------------------------------------ + +-- TODO: Implement a comparison operator which also works for functions. + +-- newtype EqFun = EqFun { unEqFun :: +-- forall a b . (Data a, Data b) => a -> b -> Bool } + +-- class SemanticFunEq a where +-- (!==!), (!/=!) :: a -> a -> Bool + +-- (!/=!) = \x y -> not (x !==! y) + +-- instance Data a => SemanticFunEq a where +-- x !==! y = +-- let test :: (Arbitrary b, Show b, Data c) => +-- (b -> c1) -> (b -> c2) -> Bool +-- test f g = testIt (forAll arbitrary $ \(x :: b) -> f x !==!! g x) +-- in let ?funTest = EqFun test +-- in x !==!! y + +-- (!==!!) :: (Data a, Data b, ?funTest :: EqFun) => a -> b -> Bool +-- x !==!! y = case (isBottom x, isBottom y) of +-- (True, True) -> True +-- (False, False) | isFunction x -> unEqFun ?funTest x y +-- | otherwise -> x =^= y && tmapQl (&&) True (!==!!) x y +-- _ -> False + +-- This one works, but it only handles functions on the top level, not +-- functions inside e.g. lists. + +-- instance (Show a, Arbitrary a, SemanticFunEq b) => SemanticFunEq (a -> b) where +-- f !==! g = case (isBottom f, isBottom g) of +-- (True, True) -> True +-- (False, False) -> testIt (forAll arbitrary $ \x -> f x !==! g x) +-- _ -> False + +-- instance SemanticEq a => SemanticFunEq a where +-- a !==! b = case (isBottom a, isBottom b) of +-- (True, True) -> True +-- (False, False) -> -- We know that we are not dealing with functions. +-- a ==! b +-- _ -> False diff --git a/Test/ChasingBottoms/SemanticOrd/Tests.hs b/Test/ChasingBottoms/SemanticOrd/Tests.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/SemanticOrd/Tests.hs @@ -0,0 +1,118 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- | Tests for "Test.ChasingBottoms.SemanticOrd". The functions using +-- tweaks are currently not tested. + +module Test.ChasingBottoms.SemanticOrd.Tests (tests) where + +import Test.ChasingBottoms.SemanticOrd +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 + +------------------------------------------------------------------------ +-- The actual tests + +prop_SemanticEq_congruence :: (Data a, Show a) + => Gen a + -> NotEqualGen a + -> Cogen a + -> [Property] +prop_SemanticEq_congruence element notEqualTo coGen = + isCongruence element return notEqualTo (==!) (/=!) + (function coGen integer) (==!) + +prop_SemanticOrd_partial_order :: (Data a, Show a) + => Gen a + -> NotEqualGen a + -> GreaterEqualGen a + -> JoinableGen a + -> [Property] +prop_SemanticOrd_partial_order element notEqualTo greaterThan joinable = + isPartialOrder element return notEqualTo greaterThan (==!) (<=!) ++ + isPartialOrderOperators element greaterThan (==!) (<=!) (=!) (>!) ++ + [ compare + , meet_associative, meet_commutative, meet_idempotent, meet_lt + , join_associative, join_commutative, join_idempotent, join_lt + , join_meet_absorption, meet_join_absorption + ] + where + twoElems = pair3 element greaterThan + + compare = + forAll twoElems $ \(x, y) -> + case semanticCompare noTweak x y of + Nothing -> not (x <=! y) && not (x >=! y) + Just LT -> x x ==! y + Just Prelude.GT -> x >! y + + meet_associative = isAssociative (oneof [ liftM3 (,,) element element element + , triple element joinable joinable + ] + ) + (==!) (/\!) + meet_commutative = isCommutative (oneof [ liftM2 (,) element element + , pair element joinable + ] + ) + (==!) (/\!) + meet_idempotent = isIdempotent element (==!) (/\!) + + join_associative = + forAll (triple element joinable joinable) $ \(x, y, z) -> + (x \/! y >>= (\/! z)) ==! ((x \/!) =<< y \/! z) + join_commutative = isCommutative (pair element joinable) (==!) (\/!) + join_idempotent = + forAll element $ \x -> + x \/! x ==! Just x + + join_meet_absorption = + forAll jmPair $ \(x, y) -> + x \/! (x /\! y) ==! Just x + where jmPair = oneof [ liftM2 (,) element element + , pair element joinable + ] + meet_join_absorption = + forAll (pair element joinable) $ \(x, y) -> + x /\! fromJust (x \/! y) ==! x + + twoElems' = frequency [ (2, twoElems), (1, pair element joinable) ] + + meet_lt = + forAll twoElems' $ \(x, y) -> + (x <=! y) == (x /\! y ==! x) + join_lt = + forAll twoElems' $ \(x, y) -> + (x <=! y) == (x \/! y ==! Just y) + +-- | All tests collected together. + +tests :: IO Bool +tests = runQuickCheckTests $ map run $ concat theTests + where + theTests = + [ prop_SemanticEq_congruence bool neBool coBool + , prop_SemanticEq_congruence integer neInteger coInteger + , prop_SemanticEq_congruence (finiteListOf bool) + (neListOf bool neBool finiteListOf) + (coListOf coBool) + , prop_SemanticEq_congruence (finiteTreeOf integer) + (neTreeOf integer neInteger finiteTreeOf) + (coTreeOf coInteger) + , prop_SemanticOrd_partial_order bool neBool geBool joinBool + , prop_SemanticOrd_partial_order integer neInteger geInteger joinInteger + , prop_SemanticOrd_partial_order (finiteListOf bool) + (neListOf bool neBool finiteListOf) + (geListOf bool geBool finiteListOf) + (joinListOf bool joinBool finiteListOf) + , prop_SemanticOrd_partial_order (finiteTreeOf integer) + (neTreeOf integer neInteger finiteTreeOf) + (geTreeOf integer geInteger finiteTreeOf) + (joinTreeOf integer joinInteger + finiteTreeOf) + ] diff --git a/Test/ChasingBottoms/TestLibraryWhenCompiling.hs b/Test/ChasingBottoms/TestLibraryWhenCompiling.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/TestLibraryWhenCompiling.hs @@ -0,0 +1,21 @@ +{-# 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 [] + ) diff --git a/Test/ChasingBottoms/TestUtilities.hs b/Test/ChasingBottoms/TestUtilities.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/TestUtilities.hs @@ -0,0 +1,433 @@ +-- | Some utilities that are part of the testing framework. + +module Test.ChasingBottoms.TestUtilities + ( -- * Batch execution of QuickCheck tests + runQuickCheckTests + -- * Various algebraic properties + , isAssociative + , isCommutative + , isIdempotent + -- ** Equivalence and congruence + , isEquivalenceRelation + , isCongruence + , eqIsCongruence + -- ** Partial and total orders + , isPartialOrder + , isTotalOrder + , isPartialOrderOperators + , isTotalOrderOperators + , ordIsTotalOrder + -- * Helper functions + , pair + , triple + , pair3 + ) where + +import Test.QuickCheck +import Test.QuickCheck.Batch +import Data.List +import Control.Arrow +import Control.Monad +import Text.Show.Functions + +------------------------------------------------------------------------ +-- Batch execution of QuickCheck tests + +-- | 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] + -- ^ 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 + 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" + + 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 ": " + +------------------------------------------------------------------------ +-- Testing various algebraic properties + +-- | Test for associativity. + +isAssociative + :: Show a + => Gen (a, a, a) + -- ^ Generator for arbitrary elements, possibly related in some + -- way to make the test more meaningful. + -> (a -> a -> Bool) + -- ^ Equality test. + -> (a -> a -> a) + -- ^ The operation. + -> Property +isAssociative triple (==.) (+.) = + forAll triple $ \(x, y, z) -> + ((x +. y) +. z) ==. (x +. (y +. z)) + +-- | Test for commutativity. + +isCommutative + :: Show a + => Gen (a, a) + -- ^ Generator for arbitrary elements, possibly related in some + -- way to make the test more meaningful. + -> (b -> b -> Bool) + -- ^ Equality test. + -> (a -> a -> b) + -- ^ The operation. + -> Property +isCommutative pair (==.) (+.) = + forAll pair $ \(x, y) -> + (x +. y) ==. (y +. x) + +-- | Test for idempotence. + +isIdempotent + :: Show a + => Gen a + -- ^ Generator for arbitrary element. + -> (a -> a -> Bool) + -- ^ Equality test. + -> (a -> a -> a) + -- ^ The operation. + -> Property +isIdempotent element (==.) (+.) = + forAll element $ \x -> + (x +. x) ==. x + +-- | Tests for an equivalence relation. Requires that the relation is +-- neither always false nor always true. + +isEquivalenceRelation + :: Show a + => Gen a + -- ^ Generator for arbitrary element. + -> (a -> Gen a) + -- ^ Generator for element equivalent to argument. + -> (a -> Gen a) + -- ^ Generator for element not equivalent to argument. + -> (a -> a -> Bool) + -- ^ The relation. + -> [Property] +isEquivalenceRelation element equalTo notEqualTo (===) = + [reflexive, symmetric1, symmetric2, transitive] + where + x /== y = not (x === y) + + reflexive = forAll element $ \x -> + x === x + + symmetric1 = forAll (pair element equalTo) $ \(x, y) -> + x === y && y === x + + symmetric2 = forAll (pair element notEqualTo) $ \(x, y) -> + x /== y && y /== x + + transitive = forAll (pair element equalTo) $ \(x, y) -> + forAll (equalTo y) $ \z -> + x === z + +-- | Tests for a congruence. Also tests that the negated relation is +-- the negation of the relation. + +isCongruence + :: (Show a, Eq b) + => Gen a + -- ^ Generator for arbitrary element. + -> (a -> Gen a) + -- ^ Generator for element equivalent to argument. + -> (a -> Gen a) + -- ^ Generator for element not equivalent to argument. + -> (a -> a -> Bool) + -- ^ The relation. + -> (a -> a -> Bool) + -- ^ The negated relation. + -> Gen (a -> b) + -- ^ Generator for functions. + -> (b -> b -> Bool) + -- ^ Equality for function result type. + -> [Property] +isCongruence element equalTo notEqualTo (===) (/==) function (.===) = + isEquivalenceRelation element equalTo notEqualTo (===) + ++ [cong, eq_neq1, eq_neq2] + where + cong = forAll function $ \f -> + forAll (pair element equalTo) $ \(x, y) -> + f x .=== f y + eq_neq1 = forAll (pair element equalTo) $ \(x, y) -> + x === y && not (x /== y) + eq_neq2 = forAll (pair element notEqualTo) $ \(x, y) -> + not (x === y) && x /== y + +-- | Test that an 'Eq' instance is a congruence. + +eqIsCongruence + :: (Show a, Eq a, Eq b) + => Gen a + -- ^ Generator for arbitrary element. + -> (a -> Gen a) + -- ^ Generator for element equivalent to argument. + -> (a -> Gen a) + -- ^ Generator for element not equivalent to argument. + -> Gen (a -> b) + -- ^ Generator for functions. + -> [Property] +eqIsCongruence element equalTo notEqualTo function = + isCongruence element equalTo notEqualTo (==) (/=) function (==) + +-- | Tests for a partial order. + +isPartialOrder + :: Show a + => Gen a + -- ^ Generator for arbitrary element. + -> (a -> Gen a) + -- ^ Generator for element equal to argument, according to + -- underlying equality relation. + -> (a -> Gen a) + -- ^ Generator for element different from argument, according to + -- underlying equality relation. + -> (a -> Gen a) + -- ^ Generator for element greater than or equal to argument. + -> (a -> a -> Bool) + -- ^ Underlying equality relation. + -> (a -> a -> Bool) + -- ^ The relation. + -> [Property] +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 + + antisymmetric2 = + forAll (pair element differentFrom) $ \(x, y) -> + not (x <=. y && y <=. x) && not (x ==. y) + + transitive = forAll (pair element greaterThan) $ \(x, y) -> + forAll (greaterThan y) $ \z -> + x <=. z + +-- | Tests for a total order. + +isTotalOrder + :: Show a + => Gen a + -- ^ Generator for arbitrary element. + -> (a -> Gen a) + -- ^ Generator for element equal to argument, according to + -- underlying equality relation. + -> (a -> Gen a) + -- ^ Generator for element different from argument, according to + -- underlying equality relation. + -> (a -> Gen a) + -- ^ Generator for element greater than or equal to argument. + -> (a -> a -> Bool) + -- ^ Underlying equality relation. + -> (a -> a -> Bool) + -- ^ The relation. + -> [Property] +isTotalOrder element equalTo differentFrom greaterThan (==.) (<=.) = + isPartialOrder element equalTo differentFrom greaterThan (==.) (<=.) + ++ [total] + where + infix 4 <=. + + total = + forAll element $ \x -> + forAll element $ \y -> + x <=. y || y <=. x + +-- | Tests relating various partial order operators. Does not include +-- any tests from 'isPartialOrder'. + +isPartialOrderOperators + :: Show a + => Gen a + -- ^ Generator for arbitrary element. + -> (a -> Gen a) + -- ^ Generator for element greater than or equal to argument. + -> (a -> a -> Bool) + -- ^ Equal. + -> (a -> a -> Bool) + -- ^ Less than or equal. + -> (a -> a -> Bool) + -- ^ Less than. + -> (a -> a -> Bool) + -- ^ Greater than or equal. + -> (a -> a -> Bool) + -- ^ Greater than. + -> [Property] +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)) + + gt_ge = + forAll twoElems $ \(x, y) -> + (x >. y) == (x >=. y && not (x ==. y)) + + ge_le = + forAll twoElems $ \(x, y) -> + (x >=. y) == (y <=. x) + + lt_gt = + forAll twoElems $ \(x, y) -> + (x <. y) == (y >. x) + +-- | Tests relating various total order operators and functions. Does +-- not include any tests from 'isTotalOrder'. + +isTotalOrderOperators + :: Show a + => Gen a + -- ^ Generator for arbitrary element. + -> (a -> Gen a) + -- ^ Generator for element greater than or equal to argument. + -> (a -> a -> Bool) + -- ^ Equal. + -> (a -> a -> Bool) + -- ^ Less than or equal. + -> (a -> a -> Bool) + -- ^ Less than. + -> (a -> a -> Bool) + -- ^ Greater than or equal. + -> (a -> a -> Bool) + -- ^ Greater than. + -> (a -> a -> Ordering) + -- ^ Compare. + -> (a -> a -> a) + -- ^ Minimum. + -> (a -> a -> a) + -- ^ Maximum. + -> [Property] +isTotalOrderOperators element greaterThan + (==.) (<=.) (<.) (>=.) (>.) cmp mn mx = + isPartialOrderOperators element greaterThan (==.) (<=.) (<.) (>=.) (>.) + ++ [compare_lt_eq_gt, compare_max, compare_min] + where + twoElems = pair3 element greaterThan + + compare_lt_eq_gt = + forAll twoElems $ \(x, y) -> + case cmp x y of + LT -> x <. y + EQ -> x ==. y + GT -> x >. y + + compare_max = + forAll twoElems $ \(x, y) -> + case cmp x y of + LT -> x `mx` y ==. y + GT -> x `mx` y ==. x + EQ -> elemBy (==.) (x `mx` y) [x, y] + + compare_min = + forAll twoElems $ \(x, y) -> + case cmp x y of + LT -> x `mn` y ==. x + GT -> x `mn` y ==. y + EQ -> elemBy (==.) (x `mn` y) [x, y] + + elemBy op x xs = any (`op` x) xs + +-- | Tests that an 'Ord' instance should satisfy to be a total order. + +ordIsTotalOrder + :: (Show a, Ord a) + => Gen a + -- ^ Generator for arbitrary element. + -> (a -> Gen a) + -- ^ Generator for element equal to argument. + -> (a -> Gen a) + -- ^ Generator for element different from argument. + -> (a -> Gen a) + -- ^ Generator for element greater than or equal to argument. + -> [Property] +ordIsTotalOrder element equalTo differentFrom greaterThan = + isTotalOrderOperators element greaterThan + (==) (<=) (<) (>=) (>) compare min max + ++ isTotalOrder element equalTo differentFrom greaterThan (==) (<=) + +------------------------------------------------------------------------ +-- Helper functions + +-- | Given two generators, generates a pair where the second component +-- depends on the first. + +pair :: Gen a -> (a -> Gen b) -> Gen (a, b) +pair gen1 gen2 = do + x <- gen1 + y <- gen2 x + return (x, y) + +-- | 'triple' works like 'pair', but for triples. + +triple :: Gen a -> (a -> Gen b) -> (b -> Gen c) -> Gen (a, b, c) +triple gen1 gen2 gen3 = do + x <- gen1 + y <- gen2 x + z <- gen3 y + return (x, y, z) + +-- | Given two generators, where the second one depends on elements +-- generated by the first one, 'pair3' generates three kinds of pairs: +-- +-- 1. Containing two elements from the first generator. +-- +-- 2. Containing one element from the first and one from the second. +-- +-- 3. Containing one element from the second and one from the first. + +pair3 :: Gen a -> (a -> Gen a) -> Gen (a, a) +pair3 gen1 gen2 = + oneof [ liftM2 (,) gen1 gen1 + , pair gen1 gen2 + , fmap (snd &&& fst) $ pair gen1 gen2 + ] diff --git a/Test/ChasingBottoms/TestUtilities/Generators.hs b/Test/ChasingBottoms/TestUtilities/Generators.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/TestUtilities/Generators.hs @@ -0,0 +1,386 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- | Generators that are part of the testing framework. + +-- This module contains _many_ generators. Maybe they should be +-- exported, not just from this module, but from the library as well. + +module Test.ChasingBottoms.TestUtilities.Generators + ( -- * Basic types and functions + Cogen + , function + , NotEqualGen + , GreaterEqualGen + , JoinableGen + -- ** @Bool@ generators + , bool + , coBool + , neBool + , geBool + , joinBool + -- ** @Integer@ generators + , integer + , coInteger + , neInteger + , geInteger + , joinInteger + -- ** @[]@ generators + , finiteListOf + , infiniteListOf + , coListOf + , neListOf + , geListOf + , joinListOf + -- ** @Tree@ generators + , Tree(..) + , finiteTreeOf + , infiniteTreeOf + , coTreeOf + , neTreeOf + , geTreeOf + , joinTreeOf + -- * Tests of the generators + , tests + ) where + +import Test.ChasingBottoms.IsBottom +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 + +import Test.ChasingBottoms.ApproxShow +import Test.ChasingBottoms.Nat + +------------------------------------------------------------------------ +-- Data types + +-- | Binary trees with information in the leaves. + +data Tree a + = Branch (Tree a) (Tree a) + | Leaf a + deriving (Show, Typeable, Data) + +------------------------------------------------------------------------ +-- Basic generators + +integer :: Gen Integer +integer = frequency [ (1, return bottom), (10, arbitrary) ] + +bool :: Gen Bool +bool = elements [bottom, False, True] + +finiteListOf :: Gen a -> Gen [a] +finiteListOf gen = sized finList + where + finList size | size == 0 = baseCase + | otherwise = + frequency [ (1, baseCase) + , (10, do elem <- gen + l <- finList (size - 1) + return (elem : l) + ) + ] + + baseCase = elements [bottom, []] + +finiteTreeOf :: Gen a -> Gen (Tree a) +finiteTreeOf gen = sized finTree + where + finTree size | size == 0 = baseCase + | otherwise = + frequency [ (1, baseCase) + , (2, do left <- finTree (size `div` 2) + right <- finTree (size `div` 2) + return (Branch left right) + ) + ] + + baseCase = frequency [(1, bottom), (3, liftM Leaf gen)] + +-- | Definitely infinite lists. + +infiniteListOf :: Gen a -> Gen [a] +infiniteListOf gen = liftM2 (:) gen (infiniteListOf gen) + +-- | Possibly infinite trees. + +infiniteTreeOf :: Gen a -> Gen (Tree a) +infiniteTreeOf gen = infTree + where + infTree = frequency [ (1, return bottom) + , (1, liftM Leaf gen) + , (3, liftM2 Branch infTree infTree) + ] + +testGen :: (Show a, Data a) => Nat -> Gen a -> IO () +testGen depth gen = test $ forAll gen $ \n -> + collect (approxShow depth n) $ True + +------------------------------------------------------------------------ +-- Cogenerators + +-- | A mapping from an argument to a generator transformer, like the +-- 'coarbitrary' function. +-- +-- Note that the functions generated by the cogenerators in this +-- module are not necessarily monotone. + +type Cogen a = forall b. a -> Gen b -> Gen b + +coBool :: Cogen Bool +coBool b | isBottom b = variant 0 +coBool False = variant 1 +coBool True = variant 2 + +coInteger :: Cogen Integer +coInteger i | isBottom i = variant 0 + | otherwise = variant 1 . coarbitrary i + +coListOf :: Cogen a -> Cogen [a] +coListOf cog xs | isBottom xs = variant 0 +coListOf cog [] = variant 1 +coListOf cog (x:xs) = variant 2 . cog x . coListOf cog xs + +coTreeOf :: Cogen a -> Cogen (Tree a) +coTreeOf cog xs | isBottom xs = variant 0 +coTreeOf cog (Leaf x) = variant 1 . cog x +coTreeOf cog (Branch l r) = variant 2 . coTreeOf cog l . coTreeOf cog r + +-- | Given a 'Cogen' and a 'Gen', generate a function. + +-- Note that the functions generated by 'promote' below are all +-- non-bottom. + +function :: Cogen a -> Gen b -> Gen (a -> b) +function coGen gen = frequency [ (1, return bottom) + , (50, promote (\a -> coGen a gen)) + ] + +testFunction :: (Data a, Data b) => Nat -> Cogen a -> Gen b -> [a] -> IO () +testFunction depth coGen gen inputs = + test $ forAll (function coGen gen) $ \f -> + collect (map (\x -> approxShow depth (x, f x)) inputs) $ True + +------------------------------------------------------------------------ +-- Generators for element not equal to argument + +-- | Mapping from argument to generator of elements not equal to +-- argument. + +type NotEqualGen a = a -> Gen a + +neBool :: NotEqualGen Bool +neBool b | isBottom b = elements [False, True] +neBool False = elements [bottom, True] +neBool True = elements [bottom, False] + +neInteger :: NotEqualGen Integer +neInteger i | isBottom i = arbitrary + | otherwise = + frequency [ (1, return bottom) + , (10, do j <- arbitrary + let j' = if j >= 0 then j + 1 else j - 1 + return (i + j') + ) + ] + +neListOf :: Gen a -> NotEqualGen a -> (Gen a -> Gen [a]) -> NotEqualGen [a] +neListOf gen neg listOf xs = neList xs + where + neList xs + | isBottom xs = frequency [ (1, return []), (10, nonEmpty gen) ] + | otherwise = case xs of + [] -> frequency [ (1, return bottom), (10, nonEmpty gen) ] + (y:ys) -> frequency [ (1, return bottom) + , (1, return []) + , (5, nonEmpty (neg y)) + , (5, do y' <- neg y + return (y':ys) + ) + , (5, do ys' <- neList ys + return (y:ys') + ) + ] + + nonEmpty headGen = do x <- headGen + xs <- listOf gen + return (x:xs) + +neTreeOf :: Gen a + -> NotEqualGen a + -> (Gen a -> Gen (Tree a)) + -> NotEqualGen (Tree a) +neTreeOf gen neg treeOf t = neTree t + where + neTree t + | isBottom t = frequency [ (1, leaf gen), (10, node) ] + | otherwise = case t of + Leaf x -> frequency [ (1, smallTreeNE x), (2, node) ] + Branch l r -> frequency [ (1, return bottom) + , (2, leaf gen) + , (2, do l' <- neTree l + return (Branch l' r) + ) + , (2, do r' <- neTree r + return (Branch l r') + ) + , (2, do l' <- neTree l + r' <- node + return (Branch l' r') + ) + , (2, do l' <- node + r' <- neTree r + return (Branch l' r') + ) + ] + + leaf g = liftM Leaf g + smallTreeNE x = frequency [(1, return bottom), (3, leaf (neg x))] + + node = do l <- treeOf gen + r <- treeOf gen + return (Branch l r) + +prop_notEqualGen element gen = + forAll (pair element gen) $ \(x, y) -> + x /=! y + +testGenPair :: (Show a, Data a) => Nat -> Gen a -> (a -> Gen a) -> IO () +testGenPair depth gen gen' = test $ + forAll (pair gen gen') $ \(x, y) -> + collect (approxShow depth (x, y)) $ True + +------------------------------------------------------------------------ +-- Generators for element greater than or equal to argument + +-- | Mapping from argument to generator of elements greater than or +-- equal to argument. + +type GreaterEqualGen a = a -> Gen a + +-- | 'GreaterEqualGen' for flat CPOs. + +flatGEGen :: Gen a -> GreaterEqualGen a +flatGEGen gen x | isBottom x = gen + | otherwise = return x + +geBool :: GreaterEqualGen Bool +geBool = flatGEGen bool + +geInteger :: GreaterEqualGen Integer +geInteger = flatGEGen integer + +geListOf :: Gen a + -> GreaterEqualGen a + -> (Gen a -> Gen [a]) + -> GreaterEqualGen [a] +geListOf gen geGen listOf xs + | isBottom xs = listOf gen + | otherwise = case xs of + [] -> return [] + y:ys -> do y' <- geGen y + ys' <- geListOf gen geGen listOf ys + return (y':ys') + +geTreeOf :: Gen a + -> GreaterEqualGen a + -> (Gen a -> Gen (Tree a)) + -> GreaterEqualGen (Tree a) +geTreeOf gen geGen treeOf t + | isBottom t = treeOf gen + | otherwise = case t of + Leaf x -> liftM Leaf (geGen x) + Branch l r -> do l' <- geTreeOf gen geGen treeOf l + r' <- geTreeOf gen geGen treeOf r + return (Branch l' r') + +prop_greaterEqualGen element gen = + forAll (pair element gen) $ \(x, y) -> + x <=! y + +------------------------------------------------------------------------ +-- Generators for pairs whose components' join exists + +-- | Mapping from argument to generator of elements whose join with +-- the argument is likely to exist. +-- +-- Note that the meet of these elements is also likely to be +-- \"interesting\". + +type JoinableGen a = a -> Gen a + +-- | 'JoinableGen' for flat CPOs. + +flatJoinGen :: Gen a -> JoinableGen a +flatJoinGen gen x | isBottom x = gen + | otherwise = frequency [(1, return bottom), (4, return x)] + +joinBool :: JoinableGen Bool +joinBool = flatJoinGen bool + +joinInteger :: JoinableGen Integer +joinInteger = flatJoinGen integer + +joinListOf :: Gen a -> JoinableGen a -> (Gen a -> Gen [a]) -> JoinableGen [a] +joinListOf gen joinGen listOf xs + | isBottom xs = listOf gen + | otherwise = case xs of + [] -> frequency [(1, return bottom), (4, return [])] + y:ys -> frequency [ (1, return bottom) + , (10, do y' <- joinGen y + ys' <- joinListOf gen joinGen listOf ys + return (y':ys') + ) + ] + +joinTreeOf :: Gen a + -> JoinableGen a + -> (Gen a -> Gen (Tree a)) + -> JoinableGen (Tree a) +joinTreeOf gen joinGen treeOf t + | isBottom t = treeOf gen + | otherwise = case t of + Leaf x -> frequency [(1, return bottom), (4, liftM Leaf (joinGen x))] + Branch l r -> frequency [ (1, return bottom) + , (5, do l' <- joinTreeOf gen joinGen treeOf l + r' <- joinTreeOf gen joinGen treeOf r + return (Branch l' r') + ) + ] + +prop_joinableGen element gen = + forAll (pair element gen) $ \(x, y) -> + isJust (x \/! y) + +------------------------------------------------------------------------ + +-- | All tests collected together. + +tests :: IO Bool +tests = runQuickCheckTests $ map run theTests + where + theTests = + [ prop_notEqualGen bool neBool + , prop_notEqualGen integer neInteger + , prop_notEqualGen (finiteListOf bool) + (neListOf bool neBool finiteListOf) + , prop_notEqualGen (finiteTreeOf integer) + (neTreeOf integer neInteger finiteTreeOf) + , prop_greaterEqualGen bool geBool + , prop_greaterEqualGen integer geInteger + , prop_greaterEqualGen (finiteListOf bool) + (geListOf bool geBool finiteListOf) + , prop_greaterEqualGen (finiteTreeOf integer) + (geTreeOf integer geInteger finiteTreeOf) + , prop_joinableGen bool joinBool + , prop_joinableGen integer joinInteger + , prop_joinableGen (finiteListOf bool) + (joinListOf bool joinBool finiteListOf) + , prop_joinableGen (finiteTreeOf integer) + (joinTreeOf integer joinInteger finiteTreeOf) + ] diff --git a/Test/ChasingBottoms/Tests.hs b/Test/ChasingBottoms/Tests.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/Tests.hs @@ -0,0 +1,75 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- | Tests of almost everything related to "Test.ChasingBottoms". + +module Test.ChasingBottoms.Tests (main) where + +import qualified Test.ChasingBottoms.Approx.Tests as Approx +import qualified Test.ChasingBottoms.ApproxShow.Tests as ApproxShow +import qualified Test.ChasingBottoms.ContinuousFunctions.Tests as ContinuousFunctions +import qualified Test.ChasingBottoms.IsBottom.Tests as IsBottom +import qualified Test.ChasingBottoms.IsType.Tests as IsType +import qualified Test.ChasingBottoms.Nat.Tests as Nat +import qualified Test.ChasingBottoms.SemanticOrd.Tests as SemanticOrd +import qualified Test.ChasingBottoms.TestUtilities.Generators as Generators +import qualified Test.ChasingBottoms.TimeOut.Tests as TimeOut +import System.Exit + +-- | A class for things that can be tested. +class Test a where + test :: String -- ^ Description of test. + -> a -- ^ Test. + -> IO Bool -- ^ True if the test succeeded. + +-- | @'indent' a@ shows @a@ and indents the output by two spaces. A +-- trailing newline is added if necessary. + +-- This function could be more efficient. + +indent :: (Show a) => a -> IO () +indent a = putStr . maybeNL . unlines . map (" " ++) . lines $ show a + where maybeNL s | null s = "\n" + | last s == '\n' = s + | otherwise = s ++ "\n" + +instance Test Bool where + test desc b = do + putStrLn desc + indent b + return b + +instance Test [Bool] where + test desc bs = do + putStrLn desc + indent bs + return $ and bs + +instance Test (IO Bool) where + test desc io = do + putStrLn desc + b <- io + indent b + return b + +-- | This function runs all the tests, and prints out a message +-- indicating whether any failures were encountered. + +main :: IO () +main = do + ok <- fmap and $ sequence theTests + putStrLn "" + if ok then + putStrLn "All tests succeeded." + else do + putStrLn "At least one test failed." + exitFailure + where theTests = [ test "Approx:" Approx.tests + , test "ApproxShow:" ApproxShow.tests + , test "ContinuousFunctions:" ContinuousFunctions.tests + , test "Generators:" Generators.tests + , test "IsBottom:" IsBottom.tests + , test "IsType:" IsType.tests + , test "Nat:" Nat.tests + , test "SemanticOrd:" SemanticOrd.tests + , test "TimeOut:" TimeOut.tests + ] diff --git a/Test/ChasingBottoms/TimeOut.hs b/Test/ChasingBottoms/TimeOut.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/TimeOut.hs @@ -0,0 +1,130 @@ +{-# OPTIONS -fglasgow-exts #-} + +-- | +-- Module : Test.ChasingBottoms.TimeOut +-- Copyright : (c) Nils Anders Danielsson 2004-2007 +-- License : See the file LICENCE. +-- +-- Maintainer : http://www.cs.chalmers.se/~nad/ +-- Stability : experimental +-- Portability : non-portable (preemptive scheduling) +-- +-- When dealing with \"hard bottoms\", i.e. non-terminating +-- computations that do not result in exceptions, the following functions +-- may be handy. +-- +-- Note that a computation is considered to have terminated when it +-- has reached weak head normal form (i.e. something distinct from +-- bottom). + +module Test.ChasingBottoms.TimeOut + ( Result(..) + , timeOut + , timeOut' + , timeOutMicro + , timeOutMicro' + ) where + +import Control.Concurrent +import Data.Dynamic +import qualified Control.Exception as E + +data Result a + = Value a + | NonTermination + | Exception E.Exception + deriving (Eq, 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 does not terminate, then 'NonTermination' is +-- returned. +-- +-- * If the computation raises an exception, then @'Exception' e@ is +-- returned, where @e@ is the exception. + +timeOut :: Int -> IO a -> IO (Result a) +timeOut = timeOutMicro . (* 10^6) + +-- | 'timeOutMicro' takes a delay in microseconds. Note that the +-- resolution is not necessarily very high (the last time I checked it +-- was 0.02 seconds when using the standard runtime system settings +-- for GHC). + +timeOutMicro :: Int -> IO a -> IO (Result a) +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) + reaper <- forkIO $ do + threadDelay delay + putMVar mv NonTermination + result <- takeMVar mv + killThread' ioThread + killThread reaper + 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. + +data Die = Die deriving Typeable + +killThread' threadId = E.throwDynTo threadId Die + +-- | 'timeOut'' is a variant which can be used for pure +-- computations. The definition, +-- +-- @ +-- 'timeOut'' n = 'timeOut' n . 'E.evaluate' +-- @ +-- +-- ensures that @'timeOut'' 1 'Test.ChasingBottoms.IsBottom.bottom'@ +-- usually returns @'Exception' \@. (@'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.) + +timeOut' :: Int -> a -> IO (Result a) +timeOut' n = timeOut n . E.evaluate + +-- | 'timeOutMicro'' is the equivalent variant of 'timeOutMicro': +-- +-- @ +-- 'timeOutMicro'' n = 'timeOutMicro' n . 'E.evaluate' +-- @ + +timeOutMicro' :: Int -> a -> IO (Result a) +timeOutMicro' n = timeOutMicro n . E.evaluate + +------------------------------------------------------------------------ + +-- There shouldn't be any memory leaks in the code above. Profiling +-- the code below also seems to suggest that there aren't any +-- problems. However, GHCi (with :set +r) eats up more and more memory +-- if the computation below is rerun a couple of times. Hmm, that +-- seems to be the case also when running simply (reverse [1..]). It +-- probably means that GHCi never releases any memory. + +main = do + let n = 1; d = 000000 + {-# SCC "a" #-} timeOut' n (reverse [1..]) >>= print + threadDelay d + {-# SCC "b" #-} timeOut' n (reverse [1..]) >>= print + threadDelay d + {-# SCC "c" #-} timeOut' n (reverse [1..]) >>= print + threadDelay d + {-# SCC "d" #-} timeOut' n (reverse [1..]) >>= print diff --git a/Test/ChasingBottoms/TimeOut/Tests.hs b/Test/ChasingBottoms/TimeOut/Tests.hs new file mode 100644 --- /dev/null +++ b/Test/ChasingBottoms/TimeOut/Tests.hs @@ -0,0 +1,31 @@ +-- | Tests of the functions in "Test.ChasingBottoms.TimeOut". + +module Test.ChasingBottoms.TimeOut.Tests (tests) where + +-- The "Micro" variants are not tested directly, but they are used +-- internally by the functions below. + +import Test.ChasingBottoms.TimeOut +import Test.ChasingBottoms.Approx +import Test.ChasingBottoms.IsBottom +import Test.ChasingBottoms.SemanticOrd + +tests :: IO Bool +tests = do + r1 <- timeOut n bottom + r1b <- timeOut n $ return bottom + r2 <- timeOut' n bottom + r3 <- timeOut n $ return list + r4 <- timeOut' n list + r5 <- timeOut n $ return $ reverse list + r6 <- timeOut' n $ reverse list + let result = case (r1, r1b, r2, r3, r4, r5, r6) of + ( Exception _, Value b, Exception _, Value xs, Value ys + , Value _nt, NonTermination) + -> isBottom b && xs =~= list && ys =~= list + _ -> False + return result + where n = 1 + list = [1..] :: [Integer] + xs =~= ys = appr xs ==! appr ys + appr = approxAll 20 diff --git a/docs/Test-ChasingBottoms-Approx.html b/docs/Test-ChasingBottoms-Approx.html new file mode 100644 --- /dev/null +++ b/docs/Test-ChasingBottoms-Approx.html @@ -0,0 +1,339 @@ + + +Test.ChasingBottoms.Approx
Chasing BottomsContentsIndex
Test.ChasingBottoms.Approx
Portabilitynon-portable (GHC-specific)
Stabilityexperimental
Maintainerhttp://www.cs.chalmers.se/~nad/
Description
Synopsis
class Approx a where
approxAll :: Nat -> a -> a
approx :: Nat -> a -> a
Documentation
class Approx a where

Approx is a class for approximation functions as described +in The generic approximation lemma, Graham Hutton and Jeremy +Gibbons, Information Processing Letters, 79(4):197-201, Elsevier +Science, August 2001, http://www.cs.nott.ac.uk/~gmh/bib.html. +

Instances are provided for all members of the Data type class. Due +to the limitations of the Data.Generics approach to generic +programming, which is not really aimed at this kind of application, +the implementation is only guaranteed to perform correctly, with +respect to the paper (and modulo any bugs), on non-mutually-recursive +sum-of-products datatypes. In particular, nested and mutually +recursive types are not handled correctly with respect to the +paper. The specification below is correct, though (if we assume that +the Data instances are well-behaved). +

In practice the approxAll function can probably be more useful than +approx. It traverses down all subterms, and it should be possible +to prove a variant of the approximation lemma which approxAll +satisfies. +

Methods
approxAll :: Nat -> a -> a
approxAll n x traverses n levels down in x and replaces all + values at that level with bottoms. +
approx :: Nat -> a -> a
approx works like approxAll, but the traversal and + replacement is only performed at subterms of the same monomorphic + type as the original term. For polynomial datatypes this is + exactly what the version of approx described in the paper above + does. +
show/hide Instances
Data a => Approx a
Produced by Haddock version 0.7
diff --git a/docs/Test-ChasingBottoms-ApproxShow.html b/docs/Test-ChasingBottoms-ApproxShow.html new file mode 100644 --- /dev/null +++ b/docs/Test-ChasingBottoms-ApproxShow.html @@ -0,0 +1,369 @@ + + +Test.ChasingBottoms.ApproxShow
Chasing BottomsContentsIndex
Test.ChasingBottoms.ApproxShow
Portabilitynon-portable (GHC-specific)
Stabilityexperimental
Maintainerhttp://www.cs.chalmers.se/~nad/
Description
Functions for converting arbitrary (non-function, partial, + possibly infinite) values into strings. +
Synopsis
type Prec = Int
class ApproxShow a where
approxShowsPrec :: Nat -> Prec -> a -> ShowS
approxShows :: Nat -> a -> ShowS
approxShow :: Nat -> a -> String
Documentation
type Prec = Int
Precedence level. +
class ApproxShow a where
Methods
approxShowsPrec :: Nat -> Prec -> a -> ShowS

The Data instance of ApproxShow makes sure that + approxShowsPrec n behaves (more or less) like the derived + version of showsPrec, with the following differences: +

  • After n levels of descent into a term the output is + replaced by "_". +
  • All detectable occurences of bottoms are replaced by "_|_". +
  • Non-bottom functions are displayed as "<function /= _|_>". +
approxShows :: Nat -> a -> ShowS
approxShow :: Nat -> a -> String
show/hide Instances
Produced by Haddock version 0.7
diff --git a/docs/Test-ChasingBottoms-ContinuousFunctions.html b/docs/Test-ChasingBottoms-ContinuousFunctions.html new file mode 100644 --- /dev/null +++ b/docs/Test-ChasingBottoms-ContinuousFunctions.html @@ -0,0 +1,1390 @@ + + +Test.ChasingBottoms.ContinuousFunctions
Chasing BottomsContentsIndex
Test.ChasingBottoms.ContinuousFunctions
Portabilitynon-portable (GHC-specific)
Stabilityexperimental
Maintainerhttp://www.cs.chalmers.se/~nad/
Contents
Basic framework +
Liftings of some QuickCheck functionality +
Generic MakePM +
Some MakeResults +
Description

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 + than if more general functions are used, though. +

Using isBottom it is relatively easy to generate possibly + non-strict functions that are, in general, not monotone. For + 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)
+

we can generate possibly non-strict functions from Bool to + Integer using function coBool integer. There is a high + likelihood that the functions generated are not monotone, though. + The reason that we can get non-monotone functions in a language + like Haskell is that we are using the impure function isBottom. +

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 + <=! y implies that f x + <=! 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 + continuous, possibly non-strict functions. There are two steps + involved in generating a continuous function using the framework + defined here. +

  1. First the argument to the function is turned into a + PatternMatch. A PatternMatch wraps up the pattern match on + the top-level constructor of the argument, plus all further + pattern matches on the children of the argument. Just like when + coarbitrary is used a pattern match is represented as a + generator transformer. The difference here is that there is not + just one transformation per input, but one transformation per + constructor in the input. PatternMatches 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 + transformation application is wrapped up in the function + transform. +

The net result of this is that some pattern matches are performed + later, or not at all, so functions can be lazy. +

Here is an example illustrating typical use of this framework: +

 data Tree a
+   = Branch (Tree a) (Tree a)
+   | Leaf a
+     deriving (Show, Typeable, Data)
+ 
+ finiteTreeOf :: MakeResult a -> MakeResult (Tree a)
+ finiteTreeOf makeResult = sized' tree
+   where
+   tree size = transform $
+     if size == 0 then
+       baseCase
+      else
+       frequency' [ (1, baseCase)
+                  , (1, liftM2 Branch tree' tree')
+                  ]
+     where
+     tree' = tree (size `div` 2)
+ 
+     baseCase =
+       frequency' [ (1, return bottom)
+                  , (2, liftM Leaf makeResult)
+                  ]
+

Note the use of transform. To use this function to generate + functions of type Bool -> Tree Integer we can use +

 forAll (functionTo (finiteTreeOf flat)) $
+   \(f :: Bool -> Tree Integer) ->
+     ...
+
Synopsis
function :: MakePM a -> MakeResult b -> Gen (a -> b)
functionTo :: Data a => MakeResult b -> Gen (a -> b)
data PatternMatch = PatternMatch {
apply :: GenTransformer
more :: (Seq PatternMatch)
}
type GenTransformer = forall a . Gen a -> Gen a
type MakePM a = a -> PatternMatch
data MakeResult a
transform :: MakeResult a -> MakeResult a
lift' :: Gen a -> MakeResult a
arbitrary' :: Arbitrary a => MakeResult a
choose' :: Random a => (a, a) -> MakeResult a
elements' :: [a] -> MakeResult a
oneof' :: [MakeResult a] -> MakeResult a
frequency' :: [(Int, MakeResult a)] -> MakeResult a
sized' :: (Int -> MakeResult a) -> MakeResult a
resize' :: Int -> MakeResult a -> MakeResult a
match :: forall a . Data a => MakePM a
flat :: Arbitrary a => MakeResult a
finiteListOf :: MakeResult a -> MakeResult [a]
infiniteListOf :: MakeResult a -> MakeResult [a]
listOf :: MakeResult a -> MakeResult [a]
Basic framework +
function :: MakePM a -> MakeResult b -> Gen (a -> b)
Generator for continuous, not necessarily strict functions. + Functions are generated by first generating pattern matches, and + then generating a result. +
functionTo :: Data a => MakeResult b -> Gen (a -> b)

functionTo specialises function: +

+  functionTo = function match
+
data PatternMatch
PatternMatch packages up the possible outcomes of a pattern + match in a style suitable for generating functions. A pattern match + is a generator (Gen) transformer based on the top-level + constructor, and a sequence (see + http://www.soi.city.ac.uk/~ross/software/html/Data.Sequence.html) of + PatternMatches based on the children of that constructor. +
Constructors
PatternMatch
apply :: GenTransformerA generator transformer, in the style of coarbitrary. +
more :: (Seq PatternMatch)Further pattern matches made possible by this + match. +
type GenTransformer = forall a . Gen a -> Gen a
The type of a generator transformer. +
type MakePM a = a -> PatternMatch
The type of a PatternMatch generator. +
data MakeResult a

Monad for generating results given previously generated pattern + matches. +

A MakeResult a should be implemented almost as other generators for + the type a, with the difference that transform should be + used wherever the resulting function should be allowed to pattern + match (typically for each constructor emitted). See example above. +

show/hide Instances
??? a => Functor (MakeResult a)
??? a => Monad (MakeResult a)
transform :: MakeResult a -> MakeResult a
transform makes sure that the pattern matches get to influence + the generated value. See MakeResult. +
Liftings of some QuickCheck functionality +
lift' :: Gen a -> MakeResult a
Lifting of a Gen. +
arbitrary' :: Arbitrary a => MakeResult a
Lifting of arbitrary. +
choose' :: Random a => (a, a) -> MakeResult a
Lifting of choose. +
elements' :: [a] -> MakeResult a
Lifting of elements. +
oneof' :: [MakeResult a] -> MakeResult a
Lifting of oneof. +
frequency' :: [(Int, MakeResult a)] -> MakeResult a
Lifting of frequency. +
sized' :: (Int -> MakeResult a) -> MakeResult a
Lifting of sized. +
resize' :: Int -> MakeResult a -> MakeResult a
Lifting of resize. +
Generic MakePM +
match :: forall a . Data a => MakePM a
Generic implementation of PatternMatch construction. +
Some MakeResults +
flat :: Arbitrary a => MakeResult a
An implementation of MakeResult a which is suitable when a + is flat and has an Arbitrary instance. Yields bottoms around 10% + of the time. +
finiteListOf :: MakeResult a -> MakeResult [a]
This MakeResult yields finite partial lists. +
infiniteListOf :: MakeResult a -> MakeResult [a]
This MakeResult yields infinite partial lists. +
listOf :: MakeResult a -> MakeResult [a]
This MakeResult yields finite or infinite partial lists. +
Produced by Haddock version 0.7
diff --git a/docs/Test-ChasingBottoms-IsBottom.html b/docs/Test-ChasingBottoms-IsBottom.html new file mode 100644 --- /dev/null +++ b/docs/Test-ChasingBottoms-IsBottom.html @@ -0,0 +1,380 @@ + + +Test.ChasingBottoms.IsBottom
Chasing BottomsContentsIndex
Test.ChasingBottoms.IsBottom
Portabilitynon-portable (exceptions)
Stabilityexperimental
Maintainerhttp://www.cs.chalmers.se/~nad/
Description
Synopsis
isBottom :: a -> Bool
bottom :: a
nonBottomError :: String -> a
isBottomTimeOut :: Maybe Int -> a -> Bool
Documentation
isBottom :: a -> Bool

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. +

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 + DivideByZero, but the value infinity makes that + case unclear as well). +

bottom :: a
bottom generates a bottom that is suitable for testing using + isBottom. +
nonBottomError :: String -> a
nonBottomError s raises an exception (AssertionFailed) that + is not caught by isBottom. Use s to describe the exception. +
isBottomTimeOut :: Maybe Int -> a -> Bool

isBottomTimeOut timeOutLimit works like isBottom, but if + timeOutLimit is Just lim, then computations taking more than + lim seconds are also considered to be equal to bottom. Note that + this is a very crude approximation of what a bottom is. Also note + 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 + timeOut. +

Produced by Haddock version 0.7
diff --git a/docs/Test-ChasingBottoms-Nat.html b/docs/Test-ChasingBottoms-Nat.html new file mode 100644 --- /dev/null +++ b/docs/Test-ChasingBottoms-Nat.html @@ -0,0 +1,484 @@ + + +Test.ChasingBottoms.Nat
Chasing BottomsContentsIndex
Test.ChasingBottoms.Nat
Portabilitynon-portable (GHC-specific)
Stabilityexperimental
Maintainerhttp://www.cs.chalmers.se/~nad/
Description
A simple implementation of natural numbers on top of Integers. + Note that since Integers are used there is no infinite natural + number; in other words, succ is strict. +
Synopsis
data Nat
isSucc :: Nat -> Bool
fromSucc :: Nat -> Maybe Nat
natrec :: a -> (Nat -> a -> a) -> Nat -> a
foldN :: a -> (a -> a) -> Nat -> a
Documentation
data Nat

Natural numbers. +

No Data instance is provided since the + implementation should be abstract. +

show/hide Instances
isSucc :: Nat -> Bool
isSucc 0 == False, for other total natural numbers it is True. +
fromSucc :: Nat -> Maybe Nat
fromSucc 0 == Nothing, fromSucc (n+1) == Just n for a + total natural number n. +
natrec :: a -> (Nat -> a -> a) -> Nat -> a
natrec performs primitive recursion on natural numbers. +
foldN :: a -> (a -> a) -> Nat -> a

foldN is a fold on natural numbers: +

+  foldN g h = natrec g (curry $ h . snd)
+
Produced by Haddock version 0.7
diff --git a/docs/Test-ChasingBottoms-SemanticOrd.html b/docs/Test-ChasingBottoms-SemanticOrd.html new file mode 100644 --- /dev/null +++ b/docs/Test-ChasingBottoms-SemanticOrd.html @@ -0,0 +1,940 @@ + + +Test.ChasingBottoms.SemanticOrd
Chasing BottomsContentsIndex
Test.ChasingBottoms.SemanticOrd
Portabilitynon-portable (GHC-specific)
Stabilityexperimental
Maintainerhttp://www.cs.chalmers.se/~nad/
Description

Generic semantic equality and order. The semantic order referred + to is that of a typical CPO for Haskell types, where e.g. (True, + bottom) <=! (True, False), but where (True, True) + and (True, False) are incomparable. +

The implementation is based on isBottom, and has the same + limitations. Note that non-bottom functions are not handled by any + of the functions described below. +

One could imagine using QuickCheck for testing equality of + functions, but I have not managed to tweak the type system so that + it can be done transparently. +

Synopsis
data Tweak = Tweak {
approxDepth :: (Maybe Nat)
timeOutLimit :: (Maybe Int)
}
noTweak :: Tweak
class SemanticEq a where
(==!) :: a -> a -> Bool
(/=!) :: a -> a -> Bool
semanticEq :: Tweak -> a -> a -> Bool
class SemanticEq a => SemanticOrd a where
(<!) :: a -> a -> Bool
(<=!) :: a -> a -> Bool
(>=!) :: a -> a -> Bool
(>!) :: a -> a -> Bool
semanticCompare :: Tweak -> a -> a -> Maybe Ordering
(\/!) :: a -> a -> Maybe a
(/\!) :: a -> a -> a
semanticJoin :: Tweak -> a -> a -> Maybe a
semanticMeet :: Tweak -> a -> a -> a
Documentation
data Tweak
The behaviour of some of the functions below can be tweaked. +
Constructors
Tweak
approxDepth :: (Maybe Nat)If equal to Just n, an approxAll n is performed on + all arguments before doing whatever the function is supposed to + be doing. +
timeOutLimit :: (Maybe Int)If equal to Just n, then all computations that take more + than n seconds to complete are considered to be equal to + bottom. This functionality is implemented using + isBottomTimeOut. +
show/hide Instances
noTweak :: Tweak
No tweak (both fields are Nothing). +
class SemanticEq a where
SemanticEq contains methods for testing whether two terms are + semantically equal. +
Methods
(==!) :: a -> a -> Bool
(/=!) :: a -> a -> Bool
semanticEq :: Tweak -> a -> a -> Bool
show/hide Instances
class SemanticEq a => SemanticOrd a where
SemanticOrd contains methods for testing whether two terms are + related according to the semantic domain ordering. +
Methods
(<!) :: a -> a -> Bool
(<=!) :: a -> a -> Bool
(>=!) :: a -> a -> Bool
(>!) :: a -> a -> Bool
semanticCompare :: Tweak -> a -> a -> Maybe Ordering
semanticCompare tweak x y returns Nothing if x and y are + incomparable, and Just o otherwise, where o :: Ordering + represents the relation between x and y. +
(\/!) :: a -> a -> Maybe a
(/\!) :: a -> a -> a
semanticJoin :: Tweak -> a -> a -> Maybe a
semanticMeet :: Tweak -> a -> a -> a
x \/! y and x /\! y compute the least upper and greatest + lower bounds, respectively, of x and y in the semantical + domain ordering. Note that the least upper bound may not always + exist. + This functionality was implemented just because it was + possible (and to provide analogues of max and min in the Ord + class). If anyone finds any use for it, please let me know. +
show/hide Instances
Produced by Haddock version 0.7
diff --git a/docs/Test-ChasingBottoms-TimeOut.html b/docs/Test-ChasingBottoms-TimeOut.html new file mode 100644 --- /dev/null +++ b/docs/Test-ChasingBottoms-TimeOut.html @@ -0,0 +1,612 @@ + + +Test.ChasingBottoms.TimeOut
Chasing BottomsContentsIndex
Test.ChasingBottoms.TimeOut
Portabilitynon-portable (preemptive scheduling)
Stabilityexperimental
Maintainerhttp://www.cs.chalmers.se/~nad/
Description

When dealing with "hard bottoms", i.e. non-terminating + computations that do not result in exceptions, the following functions + may be handy. +

Note that a computation is considered to have terminated when it + has reached weak head normal form (i.e. something distinct from + bottom). +

Synopsis
data Result a
= Value a
| NonTermination
| Exception Exception
timeOut :: Int -> IO a -> IO (Result a)
timeOut' :: Int -> a -> IO (Result a)
timeOutMicro :: Int -> IO a -> IO (Result a)
timeOutMicro' :: Int -> a -> IO (Result a)
Documentation
data Result a
Constructors
Value a
NonTermination
Exception Exception
show/hide Instances
Eq a => Eq (Result a)
Show a => Show (Result a)
Typeable a => Typeable (Result a)
timeOut :: Int -> IO a -> IO (Result a)

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 + 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. +
timeOut' :: Int -> a -> IO (Result a)

timeOut' is a variant which can be used for pure + computations. The definition, +

+   timeOut' n = timeOut n . evaluate
+

ensures that timeOut' 1 bottom + usually returns Exception <something>. (timeOut 1 (return + bottom) usually returns Value + bottom; in other words, the + computation reaches whnf almost immediately, defeating the purpose + of the time-out.) +

timeOutMicro :: Int -> IO a -> IO (Result a)
timeOutMicro takes a delay in microseconds. Note that the + resolution is not necessarily very high (the last time I checked it + was 0.02 seconds when using the standard runtime system settings + for GHC). +
timeOutMicro' :: Int -> a -> IO (Result a)

timeOutMicro' is the equivalent variant of timeOutMicro: +

+  timeOutMicro' n = timeOutMicro n . evaluate
+
Produced by Haddock version 0.7
diff --git a/docs/Test-ChasingBottoms.html b/docs/Test-ChasingBottoms.html new file mode 100644 --- /dev/null +++ b/docs/Test-ChasingBottoms.html @@ -0,0 +1,187 @@ + + +Test.ChasingBottoms
Chasing BottomsContentsIndex
Test.ChasingBottoms
Portabilitynon-portable (GHC-specific)
Stabilityexperimental
Maintainerhttp://www.cs.chalmers.se/~nad/
Description
This module just re-exports all the other modules. +
Documentation
module Test.ChasingBottoms.Approx
module Test.ChasingBottoms.ApproxShow
module Test.ChasingBottoms.ContinuousFunctions
module Test.ChasingBottoms.IsBottom
module Test.ChasingBottoms.Nat
module Test.ChasingBottoms.SemanticOrd
module Test.ChasingBottoms.TimeOut
Produced by Haddock version 0.7
diff --git a/docs/doc-index-47.html b/docs/doc-index-47.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-47.html @@ -0,0 +1,154 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (/)
/=!Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
/\!Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
diff --git a/docs/doc-index-60.html b/docs/doc-index-60.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-60.html @@ -0,0 +1,154 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (<)
<!Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
<=!Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
diff --git a/docs/doc-index-61.html b/docs/doc-index-61.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-61.html @@ -0,0 +1,146 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (=)
==!Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
diff --git a/docs/doc-index-62.html b/docs/doc-index-62.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-62.html @@ -0,0 +1,154 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (>)
>!Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
>=!Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
diff --git a/docs/doc-index-92.html b/docs/doc-index-92.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-92.html @@ -0,0 +1,146 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (\)
\/!Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
diff --git a/docs/doc-index-A.html b/docs/doc-index-A.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-A.html @@ -0,0 +1,218 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (A)
ApproxTest.ChasingBottoms.Approx, Test.ChasingBottoms
ApproxShowTest.ChasingBottoms.ApproxShow, Test.ChasingBottoms
applyTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
approxTest.ChasingBottoms.Approx, Test.ChasingBottoms
approxAllTest.ChasingBottoms.Approx, Test.ChasingBottoms
approxDepthTest.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
approxShowTest.ChasingBottoms.ApproxShow, Test.ChasingBottoms
approxShowsTest.ChasingBottoms.ApproxShow, Test.ChasingBottoms
approxShowsPrecTest.ChasingBottoms.ApproxShow, Test.ChasingBottoms
arbitrary'Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-B.html b/docs/doc-index-B.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-B.html @@ -0,0 +1,146 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (B)
bottomTest.ChasingBottoms.IsBottom, Test.ChasingBottoms
diff --git a/docs/doc-index-C.html b/docs/doc-index-C.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-C.html @@ -0,0 +1,146 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (C)
choose'Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-E.html b/docs/doc-index-E.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-E.html @@ -0,0 +1,154 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (E)
ExceptionTest.ChasingBottoms.TimeOut, Test.ChasingBottoms
elements'Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-F.html b/docs/doc-index-F.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-F.html @@ -0,0 +1,194 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (F)
finiteListOfTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
flatTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
foldNTest.ChasingBottoms.Nat, Test.ChasingBottoms
frequency'Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
fromSuccTest.ChasingBottoms.Nat, Test.ChasingBottoms
functionTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
functionToTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-G.html b/docs/doc-index-G.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-G.html @@ -0,0 +1,146 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (G)
GenTransformerTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-I.html b/docs/doc-index-I.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-I.html @@ -0,0 +1,170 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (I)
infiniteListOfTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
isBottomTest.ChasingBottoms.IsBottom, Test.ChasingBottoms
isBottomTimeOutTest.ChasingBottoms.IsBottom, Test.ChasingBottoms
isSuccTest.ChasingBottoms.Nat, Test.ChasingBottoms
diff --git a/docs/doc-index-L.html b/docs/doc-index-L.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-L.html @@ -0,0 +1,154 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (L)
lift'Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
listOfTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-M.html b/docs/doc-index-M.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-M.html @@ -0,0 +1,170 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (M)
MakePMTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
MakeResultTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
matchTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
moreTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-N.html b/docs/doc-index-N.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-N.html @@ -0,0 +1,178 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (N)
NatTest.ChasingBottoms.Nat, Test.ChasingBottoms
NonTerminationTest.ChasingBottoms.TimeOut, Test.ChasingBottoms
natrecTest.ChasingBottoms.Nat, Test.ChasingBottoms
noTweakTest.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
nonBottomErrorTest.ChasingBottoms.IsBottom, Test.ChasingBottoms
diff --git a/docs/doc-index-O.html b/docs/doc-index-O.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-O.html @@ -0,0 +1,146 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (O)
oneof'Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-P.html b/docs/doc-index-P.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-P.html @@ -0,0 +1,166 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (P)
PatternMatch
1 (Type/Class)Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
2 (Data Constructor)Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
PrecTest.ChasingBottoms.ApproxShow, Test.ChasingBottoms
diff --git a/docs/doc-index-R.html b/docs/doc-index-R.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-R.html @@ -0,0 +1,154 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (R)
ResultTest.ChasingBottoms.TimeOut, Test.ChasingBottoms
resize'Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-S.html b/docs/doc-index-S.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-S.html @@ -0,0 +1,194 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (S)
SemanticEqTest.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
SemanticOrdTest.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
semanticCompareTest.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
semanticEqTest.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
semanticJoinTest.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
semanticMeetTest.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
sized'Test.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-T.html b/docs/doc-index-T.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-T.html @@ -0,0 +1,206 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (T)
Tweak
1 (Type/Class)Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
2 (Data Constructor)Test.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
timeOutTest.ChasingBottoms.TimeOut, Test.ChasingBottoms
timeOut'Test.ChasingBottoms.TimeOut, Test.ChasingBottoms
timeOutLimitTest.ChasingBottoms.SemanticOrd, Test.ChasingBottoms
timeOutMicroTest.ChasingBottoms.TimeOut, Test.ChasingBottoms
timeOutMicro'Test.ChasingBottoms.TimeOut, Test.ChasingBottoms
transformTest.ChasingBottoms.ContinuousFunctions, Test.ChasingBottoms
diff --git a/docs/doc-index-V.html b/docs/doc-index-V.html new file mode 100644 --- /dev/null +++ b/docs/doc-index-V.html @@ -0,0 +1,146 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
ABCEFGILMNOPRSTV/<=>\
Index (V)
ValueTest.ChasingBottoms.TimeOut, Test.ChasingBottoms
diff --git a/docs/doc-index.html b/docs/doc-index.html new file mode 100644 --- /dev/null +++ b/docs/doc-index.html @@ -0,0 +1,132 @@ + + +Chasing Bottoms (Index)
Chasing BottomsContentsIndex
Index
ABCEFGILMNOPRSTV/<=>\
diff --git a/docs/haddock.css b/docs/haddock.css new file mode 100644 --- /dev/null +++ b/docs/haddock.css @@ -0,0 +1,235 @@ +/* -------- Global things --------- */ + +BODY { + background-color: #ffffff; + color: #000000; + font-family: sans-serif; + } + +A:link { color: #0000e0; text-decoration: none } +A:visited { color: #0000a0; text-decoration: none } +A:hover { background-color: #e0e0ff; text-decoration: none } + +TABLE.vanilla { + width: 100%; + border-width: 0px; + /* I can't seem to specify cellspacing or cellpadding properly using CSS... */ +} + +TABLE.vanilla2 { + border-width: 0px; +} + +/* font is a little too small in MSIE */ +TT { font-size: 100%; } +PRE { font-size: 100%; } + +LI P { margin: 0pt } + +TD { + border-width: 0px; +} + +TABLE.narrow { + border-width: 0px; +} + +TD.s8 { height: 8px; } +TD.s15 { height: 15px; } + +SPAN.keyword { text-decoration: underline; } + +/* Resize the buttom image to match the text size */ +IMG.coll { width : 0.75em; height: 0.75em; margin-bottom: 0; margin-right: 0.5em } + +/* --------- Contents page ---------- */ + +DIV.node { + padding-left: 3em; +} + +DIV.cnode { + padding-left: 1.75em; +} + +SPAN.pkg { + position: absolute; + left: 50em; +} + +/* --------- Documentation elements ---------- */ + +TD.children { + padding-left: 25px; + } + +TD.synopsis { + padding: 2px; + background-color: #f0f0f0; + font-family: monospace + } + +TD.decl { + padding: 2px; + background-color: #f0f0f0; + font-family: monospace; + vertical-align: top; + } + +/* + arg is just like decl, except that wrapping is not allowed. It is + used for function and constructor arguments which have a text box + to the right, where if wrapping is allowed the text box squashes up + the declaration by wrapping it. +*/ +TD.arg { + padding: 2px; + background-color: #f0f0f0; + font-family: monospace; + vertical-align: top; + white-space: nowrap; + } + +TD.recfield { padding-left: 20px } + +TD.doc { + padding-top: 2px; + padding-left: 10px; + } + +TD.ndoc { + padding: 2px; + } + +TD.rdoc { + padding: 2px; + padding-left: 10px; + width: 100%; + } + +TD.body { + padding-left: 10px + } + +TD.pkg { + width: 100%; + padding-left: 10px +} + +TD.indexentry { + vertical-align: top; + padding-right: 10px + } + +TD.indexannot { + vertical-align: top; + padding-left: 20px; + white-space: nowrap + } + +TD.indexlinks { + width: 100% + } + +/* ------- Section Headings ------- */ + +TD.section1 { + padding-top: 15px; + font-weight: bold; + font-size: 150% + } + +TD.section2 { + padding-top: 10px; + font-weight: bold; + font-size: 130% + } + +TD.section3 { + padding-top: 5px; + font-weight: bold; + font-size: 110% + } + +TD.section4 { + font-weight: bold; + font-size: 100% + } + +/* -------------- The title bar at the top of the page */ + +TD.infohead { + color: #ffffff; + font-weight: bold; + padding-right: 10px; + text-align: left; +} + +TD.infoval { + color: #ffffff; + padding-right: 10px; + text-align: left; +} + +TD.topbar { + background-color: #000099; + padding: 5px; +} + +TD.title { + color: #ffffff; + padding-left: 10px; + width: 100% + } + +TD.topbut { + padding-left: 5px; + padding-right: 5px; + border-left-width: 1px; + border-left-color: #ffffff; + border-left-style: solid; + white-space: nowrap; + } + +TD.topbut A:link { + color: #ffffff + } + +TD.topbut A:visited { + color: #ffff00 + } + +TD.topbut A:hover { + background-color: #6060ff; + } + +TD.topbut:hover { + background-color: #6060ff + } + +TD.modulebar { + background-color: #0077dd; + padding: 5px; + border-top-width: 1px; + border-top-color: #ffffff; + border-top-style: solid; + } + +/* --------- The page footer --------- */ + +TD.botbar { + background-color: #000099; + color: #ffffff; + padding: 5px + } +TD.botbar A:link { + color: #ffffff; + text-decoration: underline + } +TD.botbar A:visited { + color: #ffff00 + } +TD.botbar A:hover { + background-color: #6060ff + } + diff --git a/docs/haddock.js b/docs/haddock.js new file mode 100644 --- /dev/null +++ b/docs/haddock.js @@ -0,0 +1,15 @@ +// Haddock JavaScript utilities +function toggle(button,id) +{ + var n = document.getElementById(id).style; + if (n.display == "none") + { + button.src = "minus.gif"; + n.display = "block"; + } + else + { + button.src = "plus.gif"; + n.display = "none"; + } +} diff --git a/docs/haskell_icon.gif b/docs/haskell_icon.gif new file mode 100644 Binary files /dev/null and b/docs/haskell_icon.gif differ diff --git a/docs/index.html b/docs/index.html new file mode 100644 --- /dev/null +++ b/docs/index.html @@ -0,0 +1,488 @@ + + +Chasing Bottoms
Chasing BottomsContentsIndex
Chasing Bottoms

Do you ever feel the need to test code involving bottoms (e.g. calls to +the error function), or code involving infinite values? Then this +library could be useful for you. +

It is usually easy to get a grip on bottoms by showing a value and +waiting to see how much gets printed before the first exception is +encountered. However, that quickly gets tiresome and is hard to automate +using e.g. QuickCheck +(http://www.cs.chalmers.se/~rjmh/QuickCheck/). With this library you +can do the tests as simply as the following examples show. +

Testing explicitly for bottoms: +

> isBottom (head [])
True +
> isBottom bottom
True +
> isBottom (\_ -> bottom)
False +
> isBottom (bottom, bottom)
False +

Comparing finite, partial values: +

> ((bottom, 3) :: (Bool, Int)) ==! (bottom, 2+5-4)
True +
> ((bottom, bottom) :: (Bool, Int)) <! (bottom, 8)
True +

Showing partial and infinite values (\/! is join and /\! is meet): +

> approxShow 4 $ (True, bottom) \/! (bottom, 'b')
"Just (True, 'b')" +
> approxShow 4 $ (True, bottom) /\! (bottom, 'b')
"(_|_, _|_)" +
> approxShow 4 $ ([1..] :: [Int])
"[1, 2, 3, _" +
> approxShow 4 $ (cycle [bottom] :: [Bool])
"[_|_, _|_, _|_, _" +

Approximately comparing infinite, partial values: +

> approx 100 [2,4..] ==! approx 100 (filter even [1..] :: [Int])
True +
> approx 100 [2,4..] /=! approx 100 (filter even [bottom..] :: [Int])
True +

The code above relies on the fact that bottom, just as error +"...", undefined and pattern match failures, yield +exceptions. Sometimes we are dealing with properly non-terminating +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..]) >>= print
NonTermination +

The time-out functionality can be used to treat "slow" computations as +bottoms: +

> let tweak = Tweak { approxDepth = Just 5, timeOutLimit = Just 2 }
+
> semanticEq tweak (reverse [1..], [1..]) (bottom :: [Int], [1..] :: [Int])
True +
> let tweak = noTweak { timeOutLimit = Just 2 }
+
> semanticJoin tweak (reverse [1..], True) ([] :: [Int], bottom)
Just ([],True) +

This can of course be dangerous: +

> let tweak = noTweak { timeOutLimit = Just 0 }
+
> semanticEq tweak (reverse [1..100000000]) (bottom :: [Integer])
True +

Timeouts can also be applied to IO computations: +

> 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 $ take 4 $ filter ((== 1) . (`mod` 83)) primes) >>= print
[167,499,997NonTermination +
> timeOutMicro 100 (print $ take 4 $ filter ((== 1) . (`mod` 83)) primes) >>= print
[167,499,997,1163] +
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.chalmers.se/~nad/publications/danielsson-jansson-mpc2004.html). +

The code has been tested under GHC 6.8. 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. +

Source code: http://www.cs.chalmers.se/~nad/software/ChasingBottoms/ChasingBottoms.tar.gz. +

Modules
show/hideTest
show/hideTest.ChasingBottoms
Test.ChasingBottoms.Approx
Test.ChasingBottoms.ApproxShow
Test.ChasingBottoms.ContinuousFunctions
Test.ChasingBottoms.IsBottom
Test.ChasingBottoms.Nat
Test.ChasingBottoms.SemanticOrd
Test.ChasingBottoms.TimeOut
Produced by Haddock version 0.7
diff --git a/docs/minus.gif b/docs/minus.gif new file mode 100644 Binary files /dev/null and b/docs/minus.gif differ diff --git a/docs/plus.gif b/docs/plus.gif new file mode 100644 Binary files /dev/null and b/docs/plus.gif differ