Safe Haskell	None
Language	Haskell2010

Control.Search

Contents

Searching
Testing properties
Options for parallel conjunction
Deep embedded boolean type
Re-exported

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

search :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [a]
sat :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> Bool
ctrex :: (Coolean cool, Enumerable a) => Int -> (a -> cool) -> IO (Either Integer a)
searchRaw :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [(Bool, a)]
usearch :: Enumerable a => Int -> (a -> Bool) -> [a]
test :: (Coolean cool, Enumerable a, Show a) => (a -> cool) -> IO ()
testTime :: (Coolean cool, Enumerable a, Show a) => Int -> (a -> cool) -> IO ()
data Options
- = D
- | O
- | F
- | OF
- | OS
- | OSF
sat' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> Bool
search' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> IO [a]
ctrex' :: (Coolean cool, Enumerable a) => Options -> Int -> (a -> cool) -> IO (Either Integer a)
searchRaw' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> IO [(Bool, a)]
test' :: (Coolean cool, Enumerable a, Show a) => Options -> (a -> cool) -> IO ()
testTime' :: (Coolean cool, Enumerable a, Show a) => Options -> Int -> (a -> cool) -> IO ()
(&&&) :: (Coolean a, Coolean b) => a -> b -> Cool
(|||) :: (Coolean a, Coolean b) => a -> b -> Cool
(==>) :: (Coolean a, Coolean b) => a -> b -> Cool
nott :: Coolean a => a -> Cool
true :: Cool
false :: Cool
data Cool
- = Atom Bool
- | Not Cool
- | And Cool Cool
- | Seq Cool Cool
class Coolean b
module Control.Enumerable

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

Instances

Enum Options Source #
Instance details Defined in Control.Search Methods succ :: Options -> Options # pred :: Options -> Options # toEnum :: Int -> Options # fromEnum :: Options -> Int # enumFrom :: Options -> [Options] # enumFromThen :: Options -> Options -> [Options] # enumFromTo :: Options -> Options -> [Options] # enumFromThenTo :: Options -> Options -> Options -> [Options] #
Eq Options Source #
Instance details Defined in Control.Search Methods (==) :: Options -> Options -> Bool # (/=) :: Options -> Options -> Bool #
Read Options Source #
Instance details Defined in Control.Search Methods readsPrec :: Int -> ReadS Options # readList :: ReadS [Options] # readPrec :: ReadPrec Options # readListPrec :: ReadPrec [Options] #
Show Options Source #
Instance details Defined in Control.Search Methods showsPrec :: Int -> Options -> ShowS # show :: Options -> String # showList :: [Options] -> ShowS #

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 infixr 0 Source #

Parallel implication

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

Negation

true :: Cool Source #

false :: Cool Source #

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.

Instances

Show Cool Source #
Instance details Defined in Data.Coolean Methods showsPrec :: Int -> Cool -> ShowS # show :: Cool -> String # showList :: [Cool] -> ShowS #
Coolean Cool Source #
Instance details Defined in Data.Coolean Methods toCool :: Cool -> Cool Source # toBool :: Cool -> Bool Source # isCool :: (a -> Cool) -> Bool Source #

class Coolean b Source #

Provides better interoperability between Bool and Cool by overloading operators.

Minimal complete definition

toCool, toBool, isCool

Instances

Coolean Bool Source #
Instance details Defined in Data.Coolean Methods toCool :: Bool -> Cool Source # toBool :: Bool -> Bool Source # isCool :: (a -> Bool) -> Bool Source #
Coolean Cool Source #
Instance details Defined in Data.Coolean Methods toCool :: Cool -> Cool Source # toBool :: Cool -> Bool Source # isCool :: (a -> Cool) -> Bool Source #

Re-exported

module Control.Enumerable