lazy-search-0.1.1.0: Finds values satisfying a lazy predicate

Safe HaskellNone
LanguageHaskell2010

Control.Search

Contents

Description

Efficient size-based search for values satisfying/falsifying a lazy boolean predicate. Predicates are typically of type a -> Bool, although an alternative boolean type called Cool is provided and using it may give faster searches.

See Control.Enumerable for defining default enumerations of data types (required for searching).

Synopsis

Searching

search :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [a] Source

Lazily finds all (non-isomorphic) values of or below a given size that satisfy a predicate.

sat :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> Bool Source

Is there a value of or below a given size that satisfies this predicate?

ctrex :: (Coolean cool, Enumerable a) => Int -> (a -> cool) -> IO (Either Integer a) Source

Find a counterexample to the given predicate, of or below a given size. If no counterexample is found, the number of performed executions of the predicate is returned.

searchRaw :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [(Bool, a)] Source

Lazily finds all non-isomorphic (w.r.t. laziness) inputs to a predicate and returns them along with the result of the predicate.

usearch :: Enumerable a => Int -> (a -> Bool) -> [a] Source

Unsafe version of search. Non-deterministic for some predicates.

Testing properties

test :: (Coolean cool, Enumerable a, Show a) => (a -> cool) -> IO () Source

SmallCheck-like test driver. Tests a property with gradually increasing sizes until a conunterexample is found. For each size, it shows the worst case number of tests required (if the predicate is fully eager).

testTime :: (Coolean cool, Enumerable a, Show a) => Int -> (a -> cool) -> IO () Source

Stop testing after a given number of seconds

Options for parallel conjunction

data Options Source

Options for parallel conjunction strategies. Only matters for predicates using the Cool data type instead of Bool.

Constructors

D

Sequential

O

Optimal Short-circuiting

F

Parallel (fair)

OF

Optimal Short-circuiting and fairness

OS

Optimal Short-circuiting and choice-subset detection

OSF

Subset choice short-circuiting

sat' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> Bool Source

search' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> IO [a] Source

ctrex' :: (Coolean cool, Enumerable a) => Options -> Int -> (a -> cool) -> IO (Either Integer a) Source

searchRaw' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> IO [(Bool, a)] Source

test' :: (Coolean cool, Enumerable a, Show a) => Options -> (a -> cool) -> IO () Source

testTime' :: (Coolean cool, Enumerable a, Show a) => Options -> Int -> (a -> cool) -> IO () Source

Deep embedded boolean type

(&&&) :: (Coolean a, Coolean b) => a -> b -> Cool infixr 3 Source

Commutative conjunction

(|||) :: (Coolean a, Coolean b) => a -> b -> Cool infixr 2 Source

Commutative disjunction

(==>) :: (Coolean a, Coolean b) => a -> b -> Cool Source

Parallel implication

nott :: Coolean a => a -> Cool Source

Negation

data Cool Source

Concurrent booleans. Writing properties with the Cool data type often yields faster searches compared to Bool.

Constructors

Atom Bool 
Not Cool 
And Cool Cool 
Seq Cool Cool

Sequential conjunction, the second operator is not evaluated unless the first is true.

class Coolean b Source

Provides better interoperability between Bool and Cool by overloading operators.

Minimal complete definition

toCool, toBool, isCool

Re-exported