Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module defines a variety of specifications for functions on lists,
demonstrating the specification interface of StrictCheck. See the
documentation of Test.StrictCheck (specifically strictCheckSpecExact
)
for details on how to test these specifications.
This module's primary utility is to teach how specifications work. Because Haddock omits the definitions of values, you'll learn the most by viewing the source of this module.
Synopsis
- length_spec :: Spec '[[a]] Int
- take_spec_too_easy :: Spec '[Int, [a]] [a]
- take_spec :: Spec '[Int, [a]] [a]
- take' :: Int -> [a] -> [a]
- append_spec :: Shaped a => Spec '[[a], [a]] [a]
- reverse_spec :: Shaped a => Spec '[[a]] [a]
- zip_spec :: (Shaped a, Shaped b) => Spec '[[a], [b]] [(a, b)]
- zip' :: [a] -> [b] -> [(a, b)]
- map_spec :: forall a b. (Shaped a, Shaped b) => Spec '[a -> b, [a]] [b]
- rotate :: [a] -> [a] -> [a] -> [a]
- rot :: [a] -> [a] -> [a]
- rot' :: [a] -> [a] -> [a]
- rot_spec :: Shaped a => Spec '[[a], [a]] [a]
- rot_spec' :: Shaped a => Spec '[[a], [a]] [a]
- rot_simple_spec :: Shaped a => Spec '[[a], [a]] [a]
- test_rot :: [Int] -> [Int] -> [Int] -> IO ()
- replaceThunk :: Shaped a => [a] -> [a] -> [a]
- cap :: Shaped a => [a] -> [a]
- (%$) :: (Shaped a, Shaped b) => (a -> b) -> Demand a -> Demand b
- (%*) :: (Shaped a, Shaped b) => Demand (a -> b) -> Demand a -> Demand b
- specify1 :: forall a b. (Shaped a, Shaped b) => (a -> b) -> b -> a -> a
- toContext :: Shaped b => b -> b -> ()
- expectTotal :: Shaped a => a -> a
Specifying some simple functions on lists
append_spec :: Shaped a => Spec '[[a], [a]] [a] Source #
A correct specification of '(++)'
zip_spec :: (Shaped a, Shaped b) => Spec '[[a], [b]] [(a, b)] Source #
A correct specification for zip
map_spec :: forall a b. (Shaped a, Shaped b) => Spec '[a -> b, [a]] [b] Source #
A correct specification for map
, demonstrating specifications for
higher-order functions
Specifying the productive rotate function from Okasaki's purely functional
rotate :: [a] -> [a] -> [a] -> [a] Source #
Given three lists xs
, ys
, and zs
, compute xs ++ reverse ys ++ zs
,
but with more uniform strictness
Specifically, if ys
is shorter than xs
, the work necessary to reverse it
will have already occurred by the time xs
is traversed.
rot_spec :: Shaped a => Spec '[[a], [a]] [a] Source #
A previous iteration of rot_spec'
, this one is also correct, but may be
less readable.
rot_spec' :: Shaped a => Spec '[[a], [a]] [a] Source #
A correct specification of rot
, this is also the version we presented in
the paper.
rot_simple_spec :: Shaped a => Spec '[[a], [a]] [a] Source #
An incorrect specification for rot
that miscalculates the number of cells
forced.
Utilities for working with demands over lists
replaceThunk :: Shaped a => [a] -> [a] -> [a] Source #
If the tail of the second list is thunk
, replace it with the first list
cap :: Shaped a => [a] -> [a] Source #
If the tail of the list is thunk
, replace it with []
This is a special case of replaceThunk
.
specify1 :: forall a b. (Shaped a, Shaped b) => (a -> b) -> b -> a -> a Source #
Given a unary function, an implicit demand on its result, and its input, compute its actual demand on its input in that context
This demand is calculated using observe1
, so it is guaranteed to be
correct.
toContext :: Shaped b => b -> b -> () Source #
Given an implicit demand, convert it to an evaluation context
That is, toContext d a
evaluates a
to the degree that d
is a defined
value. This uses the function evaluateDemand
; refer to its documentation
for details about how demands are used to evaluate values.
expectTotal :: Shaped a => a -> a Source #
Assert at runtime that a value is not a thunk
, failing with an error
if it is