diff --git a/.boring b/.boring new file mode 100644 --- /dev/null +++ b/.boring @@ -0,0 +1,9 @@ +(^|/)_darcs($|/) +^docs$ +^dist$ +^ChasingBottoms\.tar\.gz$ +\..*-config$ +\.hi$ +\.o$ +(^|/)#.*#$ +\.processed$ diff --git a/ChasingBottoms.cabal b/ChasingBottoms.cabal --- a/ChasingBottoms.cabal +++ b/ChasingBottoms.cabal @@ -1,20 +1,113 @@ name: ChasingBottoms -version: 1.2.2 +version: 1.2.4 license: OtherLicense license-file: LICENCE -copyright: Copyright (c) Nils Anders Danielsson 2004-2007. +copyright: Copyright (c) Nils Anders Danielsson 2004-2008. author: Nils Anders Danielsson -maintainer: http://www.cs.chalmers.se/~nad/contact.html +maintainer: http://www.cs.nott.ac.uk/~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 +homepage: http://www.cs.nott.ac.uk/~nad/software/#Chasing Bottoms +package-url: http://www.cs.nott.ac.uk/~nad/software/ChasingBottoms/ChasingBottoms.tgz synopsis: For testing partial and infinite values. -description: Do you ever feel the need to test code involving bottoms (e.g. calls - to the error function), or code involving infinite values? Then this - library could be useful for you. -category: Test -tested-with: GHC == 6.8.1 +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. + . + 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. +category: Testing +tested-with: GHC == 6.8.2 cabal-version: >= 1.2 && < 2 +build-type: Simple flag small_base description: Choose the new smaller, split-up base package. diff --git a/Header b/Header deleted file mode 100644 --- a/Header +++ /dev/null @@ -1,96 +0,0 @@ -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 --- a/LICENCE +++ b/LICENCE @@ -1,7 +1,7 @@ I have chosen to distribute this library under the MIT/Expat licence: --------------------------------------------------------------------- -Copyright (c) 2004-2007 Nils Anders Danielsson +Copyright (c) 2004-2008 Nils Anders Danielsson Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -1,66 +1,17 @@ -# This Makefile is currently only used to build the documentation and -# to run a test suite automatically using darcs. +# This Makefile is currently only used 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_68 ?= ghc # 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 \ +PACKAGES = base-3.0.1.0 containers-0.1.0.1 random-1.0.0.0 mtl-1.1.0.0 \ QuickCheck-1.1.0.0 array-0.1.0.0 ######################################################################## - -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 \ diff --git a/docs/Test-ChasingBottoms-Approx.html b/docs/Test-ChasingBottoms-Approx.html deleted file mode 100644 --- a/docs/Test-ChasingBottoms-Approx.html +++ /dev/null @@ -1,339 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/Test-ChasingBottoms-ApproxShow.html +++ /dev/null @@ -1,369 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/Test-ChasingBottoms-ContinuousFunctions.html +++ /dev/null @@ -1,1390 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/Test-ChasingBottoms-IsBottom.html +++ /dev/null @@ -1,380 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/Test-ChasingBottoms-Nat.html +++ /dev/null @@ -1,484 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/Test-ChasingBottoms-SemanticOrd.html +++ /dev/null @@ -1,940 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/Test-ChasingBottoms-TimeOut.html +++ /dev/null @@ -1,612 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/Test-ChasingBottoms.html +++ /dev/null @@ -1,187 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-47.html +++ /dev/null @@ -1,154 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-60.html +++ /dev/null @@ -1,154 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-61.html +++ /dev/null @@ -1,146 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-62.html +++ /dev/null @@ -1,154 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-92.html +++ /dev/null @@ -1,146 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-A.html +++ /dev/null @@ -1,218 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-B.html +++ /dev/null @@ -1,146 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-C.html +++ /dev/null @@ -1,146 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-E.html +++ /dev/null @@ -1,154 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-F.html +++ /dev/null @@ -1,194 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-G.html +++ /dev/null @@ -1,146 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-I.html +++ /dev/null @@ -1,170 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-L.html +++ /dev/null @@ -1,154 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-M.html +++ /dev/null @@ -1,170 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-N.html +++ /dev/null @@ -1,178 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-O.html +++ /dev/null @@ -1,146 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-P.html +++ /dev/null @@ -1,166 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-R.html +++ /dev/null @@ -1,154 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-S.html +++ /dev/null @@ -1,194 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-T.html +++ /dev/null @@ -1,206 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index-V.html +++ /dev/null @@ -1,146 +0,0 @@ - - -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 deleted file mode 100644 --- a/docs/doc-index.html +++ /dev/null @@ -1,132 +0,0 @@ - - -Chasing Bottoms (Index)
Chasing BottomsContentsIndex
Index
ABCEFGILMNOPRSTV/<=>\
diff --git a/docs/haddock.css b/docs/haddock.css deleted file mode 100644 --- a/docs/haddock.css +++ /dev/null @@ -1,235 +0,0 @@ -/* -------- 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 deleted file mode 100644 --- a/docs/haddock.js +++ /dev/null @@ -1,15 +0,0 @@ -// 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 deleted file mode 100644 Binary files a/docs/haskell_icon.gif and /dev/null differ diff --git a/docs/index.html b/docs/index.html deleted file mode 100644 --- a/docs/index.html +++ /dev/null @@ -1,488 +0,0 @@ - - -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 deleted file mode 100644 Binary files a/docs/minus.gif and /dev/null differ diff --git a/docs/plus.gif b/docs/plus.gif deleted file mode 100644 Binary files a/docs/plus.gif and /dev/null differ