-- 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.
--   
--   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.cse.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])
--   Value [5,4,3,2,1]
--   
--   
--   
--   > timeOut' 1 (reverse [1..])
--   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 $ primes ())
--   [2,NonTermination
--   > timeOutMicro 10000 (print $ take 10 $ primes ())
--   [2,3,5,7,11,13,17,19,23,29]
--   Value ()
--   
--   
--   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.cse.chalmers.se/~nad/publications/danielsson-jansson-mpc2004.html).
--   
--   The code has been tested using GHC. Most parts can probably be ported
--   to other Haskell compilers, but this would require some work. The
--   TimeOut functions require preemptive scheduling, and most of
--   the rest requires Data.Generics; isBottom only
--   requires exceptions, though.
@package ChasingBottoms
@version 1.3.1.15

-- | 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 instance is provided, because 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 GHC.Classes.Ord Test.ChasingBottoms.Nat.Nat
instance GHC.Classes.Eq Test.ChasingBottoms.Nat.Nat
instance GHC.Num.Num Test.ChasingBottoms.Nat.Nat
instance GHC.Real.Real Test.ChasingBottoms.Nat.Nat
instance GHC.Real.Integral Test.ChasingBottoms.Nat.Nat
instance GHC.Enum.Enum Test.ChasingBottoms.Nat.Nat
instance GHC.Show.Show Test.ChasingBottoms.Nat.Nat
instance Test.QuickCheck.Arbitrary.Arbitrary Test.ChasingBottoms.Nat.Nat
instance Test.QuickCheck.Arbitrary.CoArbitrary Test.ChasingBottoms.Nat.Nat

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 n x traverses n levels down in
--   x and replaces all values at that level with bottoms.
approxAll :: Approx a => 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 :: Approx a => Nat -> a -> a
instance Data.Data.Data a => Test.ChasingBottoms.Approx.Approx a

-- | 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 :: SomeException -> 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.
--   
--   
--   Note that a user-defined exception is used to terminate the
--   computation, so if c catches all exceptions, or blocks
--   asynchronous exceptions, then timeOut may fail to function
--   properly.
timeOut :: Int -> IO a -> IO (Result a)

-- | timeOut' 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.)
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 GHC.Show.Show a => GHC.Show.Show (Test.ChasingBottoms.TimeOut.Result a)
instance GHC.Show.Show Test.ChasingBottoms.TimeOut.Die
instance GHC.Exception.Type.Exception Test.ChasingBottoms.TimeOut.Die

module Test.ChasingBottoms.IsBottom

-- | isBottom a returns False if a is
--   distinct from bottom. If a equals bottom and results in an
--   exception of a certain kind (see below), then isBottom a =
--   True. If a never reaches a weak head normal form
--   and never throws one of these exceptions, then isBottom
--   a never terminates.
--   
--   The exceptions that yield True correspond to "pure bottoms",
--   i.e. bottoms that can originate in pure code:
--   
--   
--   
- ArrayException
--   
- ErrorCall
--   
- NoMethodError
--   
- NonTermination
--   
- PatternMatchFail
--   
- RecConError
--   
- RecSelError
--   
- RecUpdError
--   
--   
--   Assertions are excluded, because their behaviour depends on compiler
--   flags (not pure, and a failed assertion should really yield an
--   exception and nothing else). The same applies to arithmetic exceptions
--   (machine dependent, except possibly for DivideByZero, but the
--   value infinity makes that case unclear as well).
isBottom :: a -> Bool

-- | A variant of isBottom that lives in the IO monad.
isBottomIO :: a -> IO 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 vagaries as
--   timeOut.
isBottomTimeOut :: Maybe Int -> a -> Bool

-- | A variant of isBottomTimeOut that lives in the IO monad.
isBottomTimeOutIO :: Maybe Int -> a -> IO Bool

-- | 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
infix 4 ==!
infix 4 /=!

-- | SemanticOrd contains methods for testing whether two terms are
--   related according to the semantic domain ordering.
class SemanticEq a => SemanticOrd a
(<!) :: SemanticOrd a => a -> a -> Bool
(<=!) :: SemanticOrd a => a -> a -> Bool
(>=!) :: SemanticOrd a => a -> a -> Bool
(>!) :: SemanticOrd a => a -> a -> Bool

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

-- | 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.
semanticMeet :: SemanticOrd a => Tweak -> a -> a -> a
infix 4 <!
infix 4 <=!
infix 4 >=!
infix 4 >!
infix 5 \/!
infixl 5 /\!
instance GHC.Show.Show Test.ChasingBottoms.SemanticOrd.Tweak
instance GHC.Classes.Ord Test.ChasingBottoms.SemanticOrd.Tweak
instance GHC.Classes.Eq Test.ChasingBottoms.SemanticOrd.Tweak
instance Data.Data.Data a => Test.ChasingBottoms.SemanticOrd.SemanticOrd a
instance Data.Data.Data a => Test.ChasingBottoms.SemanticOrd.SemanticEq a

-- | 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.
--   
--   
--   
- 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 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 :: forall a. 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 Data.Data.Data a => Data.Data.Data (Test.ChasingBottoms.ContinuousFunctions.Tree a)
instance GHC.Show.Show a => GHC.Show.Show (Test.ChasingBottoms.ContinuousFunctions.Tree a)
instance GHC.Base.Monad Test.ChasingBottoms.ContinuousFunctions.MakeResult
instance GHC.Base.Applicative Test.ChasingBottoms.ContinuousFunctions.MakeResult
instance GHC.Base.Functor Test.ChasingBottoms.ContinuousFunctions.MakeResult

-- | Functions for converting arbitrary (non-function, partial, possibly
--   infinite) values into strings.
module Test.ChasingBottoms.ApproxShow

-- | Precedence level.
type Prec = Int
class ApproxShow a

-- | 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 /=
--   _|_>".
--   
approxShowsPrec :: ApproxShow a => Nat -> Prec -> a -> ShowS
approxShows :: ApproxShow a => Nat -> a -> ShowS
approxShow :: ApproxShow a => Nat -> a -> String
instance Data.Data.Data a => Test.ChasingBottoms.ApproxShow.ApproxShow a

-- | This module just re-exports all the other modules.
module Test.ChasingBottoms
