-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | For testing partial and infinite values.
--
-- 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.
@package ChasingBottoms
@version 1.2.2
-- | 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
data Result a
Value :: a -> Result a
NonTermination :: Result a
Exception :: Exception -> 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
-- 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' is a variant which can be used for pure computations.
-- The definition,
--
--
-- timeOut' n = timeOut n . evaluate
--
--
-- ensures that timeOut' 1
-- Test.ChasingBottoms.IsBottom.bottom usually returns
-- Exception <something>. (timeOut 1
-- (return Test.ChasingBottoms.IsBottom.bottom) usually
-- returns Value Test.ChasingBottoms.IsBottom.bottom; in
-- other words, the computation reaches whnf almost immediately,
-- defeating the purpose of the time-out.)
timeOut' :: Int -> 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 -> IO a -> IO (Result a)
-- | timeOutMicro' is the equivalent variant of timeOutMicro:
--
--
-- timeOutMicro' n = timeOutMicro n . evaluate
--
timeOutMicro' :: Int -> a -> IO (Result a)
instance Typeable Die
instance Typeable1 Result
instance (Eq a) => Eq (Result a)
instance (Show a) => Show (Result a)
-- | 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.
module Test.ChasingBottoms.Nat
-- | Natural numbers.
--
-- No Data.Generics.Basics.Data instance is provided since the
-- implementation should be abstract.
data Nat
-- | isSucc 0 == False, for other total natural
-- numbers it is True.
isSucc :: Nat -> Bool
-- | fromSucc 0 == Nothing, fromSucc
-- (n+1) == Just n for a total natural number n.
fromSucc :: Nat -> Maybe Nat
-- | natrec performs primitive recursion on natural numbers.
natrec :: a -> (Nat -> a -> a) -> Nat -> a
-- | foldN is a fold on natural numbers:
--
--
-- foldN g h = natrec g (curry $ h . snd)
--
foldN :: a -> (a -> a) -> Nat -> a
instance Typeable Nat
instance Eq Nat
instance Ord Nat
instance Arbitrary Nat
instance Show Nat
instance Enum Nat
instance Integral Nat
instance Real Nat
instance Num Nat
module Test.ChasingBottoms.IsBottom
-- | 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).
isBottom :: a -> Bool
-- | bottom generates a bottom that is suitable for testing using
-- isBottom.
bottom :: a
-- | nonBottomError s raises an exception
-- (AssertionFailed) that is not caught by isBottom. Use
-- s to describe the exception.
nonBottomError :: String -> a
-- | 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
-- | 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.
--
--
-- - 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.
-- - 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
-- | 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)
-- | functionTo specialises function:
--
--
-- functionTo = function match
--
functionTo :: (Data a) => MakeResult b -> Gen (a -> b)
-- | 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.
data PatternMatch
PatternMatch :: GenTransformer -> Seq PatternMatch -> PatternMatch
-- | A generator transformer, in the style of coarbitrary.
apply :: PatternMatch -> GenTransformer
-- | Further pattern matches made possible by this match.
more :: PatternMatch -> Seq PatternMatch
-- | The type of a generator transformer.
type GenTransformer = forall a. Gen a -> Gen a
-- | The type of a PatternMatch generator.
type MakePM a = a -> PatternMatch
-- | 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.
data MakeResult a
-- | transform makes sure that the pattern matches get to influence
-- the generated value. See MakeResult.
transform :: MakeResult a -> MakeResult a
-- | Lifting of a Gen.
lift' :: Gen a -> MakeResult a
-- | Lifting of arbitrary.
arbitrary' :: (Arbitrary a) => MakeResult a
-- | Lifting of choose.
choose' :: (Random a) => (a, a) -> MakeResult a
-- | Lifting of elements.
elements' :: [a] -> MakeResult a
-- | Lifting of oneof.
oneof' :: [MakeResult a] -> MakeResult a
-- | Lifting of frequency.
frequency' :: [(Int, MakeResult a)] -> MakeResult a
-- | Lifting of sized.
sized' :: (Int -> MakeResult a) -> MakeResult a
-- | Lifting of resize.
resize' :: Int -> MakeResult a -> MakeResult a
-- | Generic implementation of PatternMatch construction.
match :: (Data a) => MakePM 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.
flat :: (Arbitrary a) => MakeResult a
-- | This MakeResult yields finite partial lists.
finiteListOf :: MakeResult a -> MakeResult [a]
-- | This MakeResult yields infinite partial lists.
infiniteListOf :: MakeResult a -> MakeResult [a]
-- | This MakeResult yields finite or infinite partial lists.
listOf :: MakeResult a -> MakeResult [a]
instance Typeable1 Tree
instance Functor MakeResult
instance Monad MakeResult
instance (Show a) => Show (Tree a)
instance (Data a) => Data (Tree a)
-- | Functions for converting arbitrary (non-function, partial, possibly
-- infinite) values into strings.
module Test.ChasingBottoms.ApproxShow
-- | Precedence level.
type Prec = Int
class ApproxShow a
approxShowsPrec :: (ApproxShow a) => Nat -> Prec -> a -> ShowS
approxShows :: (ApproxShow a) => Nat -> a -> ShowS
approxShow :: (ApproxShow a) => Nat -> a -> String
instance (Data a) => ApproxShow a
module Test.ChasingBottoms.Approx
-- | 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.
class Approx a
approxAll :: (Approx a) => Nat -> a -> a
approx :: (Approx a) => Nat -> a -> a
instance Eq DataType
instance (Data a) => Approx a
-- | 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
-- | The behaviour of some of the functions below can be tweaked.
data Tweak
Tweak :: Maybe Nat -> Maybe Int -> Tweak
-- | If equal to Just n, an approxAll n is
-- performed on all arguments before doing whatever the function is
-- supposed to be doing.
approxDepth :: Tweak -> Maybe Nat
-- | 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.
timeOutLimit :: Tweak -> Maybe Int
-- | No tweak (both fields are Nothing).
noTweak :: Tweak
-- | SemanticEq contains methods for testing whether two terms are
-- semantically equal.
class SemanticEq a
(==!) :: (SemanticEq a) => a -> a -> Bool
(/=!) :: (SemanticEq a) => a -> a -> Bool
semanticEq :: (SemanticEq a) => Tweak -> a -> a -> Bool
-- | SemanticOrd contains methods for testing whether two terms are
-- related according to the semantic domain ordering.
class (SemanticEq a) => SemanticOrd a
( a -> a -> Bool
(>!) :: (SemanticOrd a) => a -> a -> Bool
(>=!) :: (SemanticOrd a) => a -> a -> Bool
(<=!) :: (SemanticOrd a) => a -> a -> Bool
semanticCompare :: (SemanticOrd a) => Tweak -> a -> a -> Maybe Ordering
(\/!) :: (SemanticOrd a) => a -> a -> Maybe a
(/\!) :: (SemanticOrd a) => a -> a -> a
semanticJoin :: (SemanticOrd a) => Tweak -> a -> a -> Maybe a
semanticMeet :: (SemanticOrd a) => Tweak -> a -> a -> a
instance Eq Tweak
instance Ord Tweak
instance Show Tweak
instance (Data a) => SemanticOrd a
instance (Data a) => SemanticEq a
-- | This module just re-exports all the other modules.
module Test.ChasingBottoms