| Copyright | (c) 2017-2019 Rudy Matela |
|---|---|
| License | 3-Clause BSD (see the file LICENSE) |
| Maintainer | Rudy Matela <rudy@matela.com.br> |
| Safe Haskell | None |
| Language | Haskell2010 |
Test.Extrapolate.Generalizable
Description
This module is part of Extrapolate, a library for generalization of counter-examples.
This defines the Generalizable typeclass
and utilities involving it.
You are probably better off importing Test.Extrapolate.
Synopsis
- class (Listable a, Express a, Name a, Show a) => Generalizable a where
- background :: a -> [Expr]
- subInstances :: a -> Instances -> Instances
- instances :: Generalizable a => a -> Instances -> Instances
- mkEq1 :: (Generalizable a, Generalizable b) => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
- mkEq2 :: (Generalizable a, Generalizable b, Generalizable c) => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
- mkEq3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool) -> [Expr]
- mkEq4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (e -> e -> Bool) -> a -> a -> Bool) -> [Expr]
- mkOrd1 :: (Generalizable a, Generalizable b) => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
- mkOrd2 :: (Generalizable a, Generalizable b, Generalizable c) => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
- mkOrd3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool) -> [Expr]
- mkOrd4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (e -> e -> Bool) -> a -> a -> Bool) -> [Expr]
- (*==*) :: Generalizable a => a -> a -> Bool
- (*/=*) :: Generalizable a => a -> a -> Bool
- (*<=*) :: Generalizable a => a -> a -> Bool
- (*<*) :: Generalizable a => a -> a -> Bool
- class Listable a where
- module Test.Extrapolate.Expr
Documentation
class (Listable a, Express a, Name a, Show a) => Generalizable a where Source #
Extrapolate can generalize counter-examples of any types that are
Generalizable.
Generalizable types must first be instances of
Listable, so Extrapolate knows how to enumerate values;Express, so Extrapolate can represent then manipulate values;Name, so Extrapolate knows how to name variables.
There are no required functions, so we can define instances with:
instance Generalizable OurType
However, it is desirable to define both background and subInstances.
The following example shows a datatype and its instance:
data Stack a = Stack a (Stack a) | Empty
instance Generalizable a => Generalizable (Stack a) where subInstances s = instances (argTy1of1 s)
To declare instances it may be useful to use type binding
operators such as: argTy1of1, argTy1of2 and argTy2of2.
Instances can be automatically derived using
deriveGeneralizable
which will also automatically derivate
Listable, Express and Name when needed.
Minimal complete definition
Nothing
Methods
background :: a -> [Expr] Source #
List of symbols allowed to appear in side-conditions.
Defaults to []. See value.
subInstances :: a -> Instances -> Instances Source #
Instances
instances :: Generalizable a => a -> Instances -> Instances Source #
Used in the definition of subInstances
in Generalizable typeclass instances.
mkEq1 :: (Generalizable a, Generalizable b) => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr] Source #
mkEq2 :: (Generalizable a, Generalizable b, Generalizable c) => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr] Source #
mkEq3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool) -> [Expr] Source #
mkEq4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (e -> e -> Bool) -> a -> a -> Bool) -> [Expr] Source #
mkOrd1 :: (Generalizable a, Generalizable b) => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr] Source #
mkOrd2 :: (Generalizable a, Generalizable b, Generalizable c) => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr] Source #
mkOrd3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool) -> [Expr] Source #
mkOrd4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (e -> e -> Bool) -> a -> a -> Bool) -> [Expr] Source #
(*==*) :: Generalizable a => a -> a -> Bool Source #
(*/=*) :: Generalizable a => a -> a -> Bool Source #
(*<=*) :: Generalizable a => a -> a -> Bool Source #
(*<*) :: Generalizable a => a -> a -> Bool Source #
A type is Listable when there exists a function that
is able to list (ideally all of) its values.
Ideally, instances should be defined by a tiers function that
returns a (potentially infinite) list of finite sub-lists (tiers):
the first sub-list contains elements of size 0,
the second sub-list contains elements of size 1
and so on.
Size here is defined by the implementor of the type-class instance.
For algebraic data types, the general form for tiers is
tiers = cons<N> ConstructorA
\/ cons<N> ConstructorB
\/ ...
\/ cons<N> ConstructorZwhere N is the number of arguments of each constructor A...Z.
Here is a datatype with 4 constructors and its listable instance:
data MyType = MyConsA
| MyConsB Int
| MyConsC Int Char
| MyConsD String
instance Listable MyType where
tiers = cons0 MyConsA
\/ cons1 MyConsB
\/ cons2 MyConsC
\/ cons1 MyConsDThe instance for Hutton's Razor is given by:
data Expr = Val Int
| Add Expr Expr
instance Listable Expr where
tiers = cons1 Val
\/ cons2 AddInstances can be alternatively defined by list.
In this case, each sub-list in tiers is a singleton list
(each succeeding element of list has +1 size).
The function deriveListable from Test.LeanCheck.Derive
can automatically derive instances of this typeclass.
A Listable instance for functions is also available but is not exported by
default. Import Test.LeanCheck.Function if you need to test higher-order
properties.
Instances
| Listable Bool | tiers :: [[Bool]] = [[False,True]] list :: [[Bool]] = [False,True] |
| Listable Char | list :: [Char] = ['a', ' ', 'b', 'A', 'c', '\', 'n', 'd', ...] |
| Listable Double |
list :: [Double] = [0.0, 1.0, -1.0, Infinity, 0.5, 2.0, ...] |
| Listable Float |
list :: [Float] = [ 0.0 , 1.0, -1.0, Infinity , 0.5, 2.0, -Infinity, -0.5, -2.0 , 0.33333334, 3.0, -0.33333334, -3.0 , 0.25, 0.6666667, 1.5, 4.0, -0.25, -0.6666667, -1.5, -4.0 , ... ] |
| Listable Int | tiers :: [[Int]] = [[0], [1], [-1], [2], [-2], [3], [-3], ...] list :: [Int] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...] |
| Listable Integer | list :: [Int] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...] |
| Listable Ordering | list :: [Ordering] = [LT, EQ, GT] |
| Listable () | list :: [()] = [()] tiers :: [[()]] = [[()]] |
Defined in Test.LeanCheck.Core | |
| Listable Int1 | |
| Listable Int2 | |
| Listable Int3 | |
| Listable Int4 | |
| Listable Word1 | |
| Listable Word2 | |
| Listable Word3 | |
| Listable Word4 | |
| Listable Natural | |
| Listable Nat | |
| Listable Nat1 | |
| Listable Nat2 | |
| Listable Nat3 | |
| Listable Nat4 | |
| Listable Nat5 | |
| Listable Nat6 | |
| Listable Nat7 | |
| Listable Space | |
| Listable Lower | |
| Listable Upper | |
| Listable Alpha | |
| Listable Digit | |
| Listable AlphaNum | |
| Listable Letter | |
| Listable Spaces | |
| Listable Lowers | |
| Listable Uppers | |
| Listable Alphas | |
| Listable Digits | |
| Listable AlphaNums | |
| Listable Letters | |
| Listable a => Listable [a] | tiers :: [[ [Int] ]] = [ [ [] ]
, [ [0] ]
, [ [0,0], [1] ]
, [ [0,0,0], [0,1], [1,0], [-1] ]
, ... ]
list :: [ [Int] ] = [ [], [0], [0,0], [1], [0,0,0], ... ] |
Defined in Test.LeanCheck.Core | |
| Listable a => Listable (Maybe a) | tiers :: [[Maybe Int]] = [[Nothing], [Just 0], [Just 1], ...] tiers :: [[Maybe Bool]] = [[Nothing], [Just False, Just True]] |
| Listable a => Listable (NoDup a) | |
| Listable a => Listable (Bag a) | |
| Listable a => Listable (Set a) | |
| (Integral a, Bounded a) => Listable (X a) | Extremily large integers are intercalated with small integers. list :: [X Int] = map X
[ 0, 1, -1, maxBound, minBound
, 2, -2, maxBound-1, minBound+1
, 3, -3, maxBound-2, minBound+2
, ... ] |
| (Integral a, Bounded a) => Listable (Xs a) | Lists with elements of the |
| (Listable a, Listable b) => Listable (Either a b) | tiers :: [[Either Bool Bool]] =
[[Left False, Right False, Left True, Right True]]
tiers :: [[Either Int Int]] = [ [Left 0, Right 0]
, [Left 1, Right 1]
, [Left (-1), Right (-1)]
, [Left 2, Right 2]
, ... ] |
| (Listable a, Listable b) => Listable (a, b) | tiers :: [[(Int,Int)]] = [ [(0,0)] , [(0,1),(1,0)] , [(0,-1),(1,1),(-1,0)] , ...] list :: [(Int,Int)] = [ (0,0), (0,1), (1,0), (0,-1), (1,1), ...] |
Defined in Test.LeanCheck.Core | |
| (Listable a, Listable b) => Listable (Map a b) | |
| (Listable a, Listable b, Listable c) => Listable (a, b, c) | list :: [(Int,Int,Int)] = [ (0,0,0), (0,0,1), (0,1,0), ...] |
Defined in Test.LeanCheck.Core | |
| (Listable a, Listable b, Listable c, Listable d) => Listable (a, b, c, d) | |
Defined in Test.LeanCheck.Core | |
| (Listable a, Listable b, Listable c, Listable d, Listable e) => Listable (a, b, c, d, e) | |
Defined in Test.LeanCheck.Core | |
module Test.Extrapolate.Expr