Test.Extrapolate.Core

This module is part of Extrapolate, a library for generalization of counter-examples.

This is the core of extrapolate.

Documentation

module Test.LeanCheck

module Test.LeanCheck.Utils.TypeBinding

module Test.Extrapolate.Exprs

class (Listable a, Typeable a, Show a) => Generalizable a where

Extrapolate can generalize counter-examples of any types that are Generalizable.

The core (and only required functions) of the generalizable typeclass are the expr and instances functions.

The following example shows a datatype and its instance:

data Stack a = Stack a (Stack a) | Empty

instance Generalizable a => Generalizable (Stack a) where
name _ = "s"
expr s@(Stack x y) = constant "Stack" (Stack ->>: s) :$ expr x :$ expr y
expr s@Empty       = constant "Empty" (Empty   -: s)
instances s = this s $ instances (argTy1of1 s)

To declare instances and expr it may be useful to use:

• LeanCheck's Test.LeanCheck.Utils.TypeBinding operators: -:, ->:, ->>:, ...;
• Extrapolate's Test.Extrapolate.TypeBinding operators: argTy1of1, argTy1of2, argTy2of2, ....

Minimal complete definition

expr, instances

Methods

expr :: a -> Expr

Transforms a value into an manipulable expression tree. See constant and :$.

name :: a -> String

Common name for a variable, defaults to "x".

background :: a -> [Expr]

List of symbols allowed to appear in side-conditions. Defaults to []. See constant.

instances :: a -> Instances -> Instances

Computes a list of reified instances. See this.

Instances

Generalizable Bool

Methods

expr :: Bool -> Expr

name :: Bool -> String

background :: Bool -> [Expr]

instances :: Bool -> Instances -> Instances

Generalizable Char

Methods

expr :: Char -> Expr

name :: Char -> String

background :: Char -> [Expr]

instances :: Char -> Instances -> Instances

Generalizable Int

Methods

expr :: Int -> Expr

name :: Int -> String

background :: Int -> [Expr]

instances :: Int -> Instances -> Instances

Generalizable Integer

Methods

expr :: Integer -> Expr

name :: Integer -> String

background :: Integer -> [Expr]

instances :: Integer -> Instances -> Instances

Generalizable Ordering

Methods

expr :: Ordering -> Expr

name :: Ordering -> String

background :: Ordering -> [Expr]

instances :: Ordering -> Instances -> Instances

Generalizable ()

Methods

expr :: () -> Expr

name :: () -> String

background :: () -> [Expr]

instances :: () -> Instances -> Instances

Generalizable a => Generalizable [a]

Methods

expr :: [a] -> Expr

name :: [a] -> String

background :: [a] -> [Expr]

instances :: [a] -> Instances -> Instances

Generalizable a => Generalizable (Maybe a)

Methods

expr :: Maybe a -> Expr

name :: Maybe a -> String

background :: Maybe a -> [Expr]

instances :: Maybe a -> Instances -> Instances

(Generalizable a, Generalizable b) => Generalizable (Either a b)

Methods

expr :: Either a b -> Expr

name :: Either a b -> String

background :: Either a b -> [Expr]

instances :: Either a b -> Instances -> Instances

(Generalizable a, Generalizable b) => Generalizable (a, b)

Methods

expr :: (a, b) -> Expr

name :: (a, b) -> String

background :: (a, b) -> [Expr]

instances :: (a, b) -> Instances -> Instances

(Generalizable a, Generalizable b, Generalizable c) => Generalizable (a, b, c)

Methods

expr :: (a, b, c) -> Expr

name :: (a, b, c) -> String

background :: (a, b, c) -> [Expr]

instances :: (a, b, c) -> Instances -> Instances

(Generalizable a, Generalizable b, Generalizable c, Generalizable d) => Generalizable (a, b, c, d)

Methods

expr :: (a, b, c, d) -> Expr

name :: (a, b, c, d) -> String

background :: (a, b, c, d) -> [Expr]

instances :: (a, b, c, d) -> Instances -> Instances

this :: Generalizable a => a -> (Instances -> Instances) -> Instances -> Instances

backgroundWith :: Typeable a => [Expr] -> a -> Instances

(+++) :: Ord a => [a] -> [a] -> [a] infixr 5

backgroundOf :: Generalizable a => a -> [Expr]

bgEq :: (Eq a, Generalizable a) => a -> [Expr]

bgOrd :: (Ord a, Generalizable a) => a -> [Expr]

bgEqWith1 :: (Generalizable a, Generalizable b) => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]

bgEqWith2 :: (Generalizable a, Generalizable b, Generalizable c) => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]

data Option

Constructors

MaxTests Int

ExtraInstances Instances

MaxConditionSize Int

MinFailures (Ratio Int)

MaxSpeculateSize (Maybe Int)

ConditionBound (Maybe Int)

ConstantBound (Maybe Int)

DepthBound (Maybe Int)

Instances

Show Option

Methods

showsPrec :: Int -> Option -> ShowS

show :: Option -> String

showList :: [Option] -> ShowS

data WithOption a

Constructors

With

Fields

• property :: a
• option :: Option

Instances

Testable a => Testable (WithOption a)

Methods

resultiers :: WithOption a -> [[([Expr], Bool)]]

($-|) :: WithOption a -> [Expr] -> Bool

tinstances :: WithOption a -> Instances

options :: WithOption a -> Options

maxTests :: Testable a => a -> Int

extraInstances :: Testable a => a -> Instances

maxConditionSize :: Testable a => a -> Int

hasEq :: Generalizable a => a -> Bool

(*==*) :: Generalizable a => a -> a -> Bool

(*/=*) :: Generalizable a => a -> a -> Bool

(*<=*) :: Generalizable a => a -> a -> Bool

(*<*) :: Generalizable a => a -> a -> Bool

tBackground :: Testable a => a -> [Expr]

counterExamples :: Testable a => Int -> a -> [[Expr]]

counterExampleGen :: Testable a => Int -> a -> Maybe ([Expr], Maybe [Expr])

counterExampleGens :: Testable a => Int -> a -> Maybe ([Expr], [[Expr]])

generalizations :: Instances -> [Expr] -> [[Expr]]

generalizationsCE :: Testable a => Int -> a -> [Expr] -> [[Expr]]

generalizationsCEC :: Testable a => a -> [Expr] -> [(Expr, [Expr])]

generalizationsCounts :: Testable a => Int -> a -> [Expr] -> [([Expr], Int)]

atoms :: Testable a => a -> [[Expr]]

theoryAndReprExprs :: Testable a => a -> (Thy, [Expr])

theoryAndReprConds :: Testable a => a -> (Thy, [Expr])

candidateConditions :: Testable a => (Thy, [Expr]) -> a -> [Expr] -> [Expr]

validConditions :: Testable a => (Thy, [Expr]) -> a -> [Expr] -> [(Expr, Int)]

weakestCondition :: Testable a => (Thy, [Expr]) -> a -> [Expr] -> Expr

getBackground :: Instances -> [Expr]

fullInstances :: Testable a => a -> Instances

matchList :: [Expr] -> [Expr] -> Maybe Binds

List matches of lists of expressions if possible

[0,1]   `matchList` [x,y]   = Just [x=0, y=1]
[0,1+2] `matchList` [x,y+y] = Nothing

newMatches :: [Expr] -> [Expr] -> Maybe Binds

class Testable a where

Minimal complete definition

resultiers, ($-|), tinstances

Methods

resultiers :: a -> [[([Expr], Bool)]]

($-|) :: a -> [Expr] -> Bool

tinstances :: a -> Instances

options :: a -> Options

Instances

Testable Bool

Methods

resultiers :: Bool -> [[([Expr], Bool)]]

($-|) :: Bool -> [Expr] -> Bool

tinstances :: Bool -> Instances

options :: Bool -> Options

Testable a => Testable (WithOption a)

Methods

resultiers :: WithOption a -> [[([Expr], Bool)]]

($-|) :: WithOption a -> [Expr] -> Bool

tinstances :: WithOption a -> Instances

options :: WithOption a -> Options

(Testable b, Generalizable a, Listable a) => Testable (a -> b)

Methods

resultiers :: (a -> b) -> [[([Expr], Bool)]]

($-|) :: (a -> b) -> [Expr] -> Bool

tinstances :: (a -> b) -> Instances

options :: (a -> b) -> Options

results :: Testable a => a -> [([Expr], Bool)]

areInstancesOf :: [Expr] -> [Expr] -> Bool