Copyright	(c) 2016-2024 Rudy Matela
License	3-Clause BSD (see the file LICENSE)
Maintainer	Rudy Matela <rudy@matela.com.br>
Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.Speculate

Contents

The constants list
The instances list
Misc.

Description

Speculate: discovery of properties by reasoning from test results

Speculate automatically discovers laws about Haskell functions. Those laws involve:

equations, such as id x == x ;
inequalities, such as 0 <= x * x ;
conditional equations, such as x <= 0 ==> x + abs x == 0 .

_Example:_ the following program prints laws about 0, 1, + and abs.

import Test.Speculate

main :: IO ()
main = speculate args
  { constants =
      [ showConstant (0::Int)
      , showConstant (1::Int)
      , constant "+"   ((+)  :: Int -> Int -> Int)
      , constant "abs" (abs  :: Int -> Int)
      , background
      , constant "<="  ((<=) :: Int -> Int -> Bool)
      ]
  }

Synopsis

speculate :: Args -> IO ()
data Args = Args {
- maxSize :: Int
- maxTests :: Int
- constants :: [Expr]
- instances :: [Instances]
- maxSemiSize :: Int
- maxCondSize :: Int
- maxVars :: Int
- showConstants :: Bool
- showEquations :: Bool
- showSemiequations :: Bool
- showConditions :: Bool
- showConstantLaws :: Bool
- autoConstants :: Bool
- minTests :: Int -> Int
- maxConstants :: Maybe Int
- maxDepth :: Maybe Int
- showCounts :: Bool
- showTheory :: Bool
- showArgs :: Bool
- showHelp :: Bool
- evalTimeout :: Maybe Double
- force :: Bool
- extra :: [String]
- exclude :: [String]
- onlyTypes :: [String]
- showClassesFor :: [Int]
- showDot :: Bool
- quietDot :: Bool
}
args :: Args
data Expr
constant :: Typeable a => String -> a -> Expr
showConstant :: (Typeable a, Show a) => a -> Expr
hole :: Typeable a => a -> Expr
foreground :: Expr
background :: Expr
type Instances = [Expr]
reifyInstances :: (Typeable a, Listable a, Show a, Eq a, Ord a, Name a) => a -> Instances
reifyEq :: (Typeable a, Eq a) => a -> [Expr]
reifyOrd :: (Typeable a, Ord a) => a -> [Expr]
reifyEqOrd :: (Typeable a, Ord a) => a -> [Expr]
reifyListable :: (Typeable a, Show a, Listable a) => a -> Instances
reifyName :: (Typeable a, Name a) => a -> [Expr]
mkEq :: Typeable a => (a -> a -> Bool) -> [Expr]
mkOrd :: Typeable a => (a -> a -> Ordering) -> [Expr]
mkOrdLessEqual :: Typeable a => (a -> a -> Bool) -> [Expr]
mkListable :: (Typeable a, Show a) => [[a]] -> [Expr]
mkNameWith :: Typeable a => String -> a -> [Expr]
class Name a where
- name :: a -> String
report :: Args -> IO ()
getArgs :: Args -> IO Args
module Test.LeanCheck
module Test.LeanCheck.Utils
module Data.Typeable

Documentation

speculate :: Args -> IO () Source #

Calls Speculate. See the example above (at the top of the file). Its only argument is an Args structure.

data Args Source #

Arguments to Speculate

Constructors

Args

Fields

maxSize :: Int
maximum size of considered expressions
maxTests :: Int
maximum number of test for each law
constants :: [Expr]
constants considered when generating expressions
instances :: [Instances]
typeclass instance information for Eq, Ord and Listable
maxSemiSize :: Int
maximum size of inqualities RHS/LHS
maxCondSize :: Int
maximum size of considered condition
maxVars :: Int
maximum number of variables allowed in inequalities and conditional equations
showConstants :: Bool
repeat constants on output
showEquations :: Bool
whether to show equations
showSemiequations :: Bool
whether to show inequalties
showConditions :: Bool
whether to show conditional equations
showConstantLaws :: Bool
whether to show laws with no variables
autoConstants :: Bool
automatically include constants taken from tiers of values
minTests :: Int -> Int
(intermediary) minimum number of tests for passing postconditions in function of maximum number of tests
maxConstants :: Maybe Int
(intermediary) maximum nubmer of constants allowed when considering expressions
maxDepth :: Maybe Int
(intermediary) maximum depth of considered expressions
showCounts :: Bool
(intermediary) show counts of equations, inequalities and conditional equations
showTheory :: Bool
(debug) whether to show raw theory
showArgs :: Bool
(debug) show _this_ args before running
showHelp :: Bool
(advanced) whether to show the command line help
evalTimeout :: Maybe Double
(advanced) timeout when evaluating ground expressions
force :: Bool
(advanced) ignore errors
extra :: [String]
(advanced) unused, user-defined meaning
exclude :: [String]
(advanced) exclude this symbols from signature before running
onlyTypes :: [String]
(advanced) only allow those types at top-level equations / semi-equations
showClassesFor :: [Int]
(advanced) show equivalence classes of expressions
showDot :: Bool
(advanced) whether to show a Graphviz dotfile with an Ord lattice
quietDot :: Bool
(advanced) whether to show a Graphviz dotfiel with an Ord lattice (less verbose)

args :: Args Source #

Default arguments to Speculate

The constants list

The following combinators are used to build the constants list from Args.

data Expr #

Values of type Expr represent objects or applications between objects. Each object is encapsulated together with its type and string representation. Values encoded in Exprs are always monomorphic.

An Expr can be constructed using:

val, for values that are Show instances;
value, for values that are not Show instances, like functions;
:$, for applications between Exprs.

> val False
False :: Bool

> value "not" not :$ val False
not False :: Bool

An Expr can be evaluated using evaluate, eval or evl.

> evl $ val (1 :: Int) :: Int
1

> evaluate $ val (1 :: Int) :: Maybe Bool
Nothing

> eval 'a' (val 'b')
'b'

Showing a value of type Expr will return a pretty-printed representation of the expression together with its type.

> show (value "not" not :$ val False)
"not False :: Bool"

Expr is like Dynamic but has support for applications and variables (:$, var).

The var underscore convention: Functions that manipulate Exprs usually follow the convention where a value whose String representation starts with '_' represents a variable.

Instances

Instances details

Show Expr	Shows `Expr`s with their types. > show (value "not" not :$ val False) "not False :: Bool"
Instance details Defined in Data.Express.Core Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
Eq Expr	O(n). Does not evaluate values when comparing, but rather uses their representation as strings and their types. This instance works for ill-typed expressions.
Instance details Defined in Data.Express.Core Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
Ord Expr	O(n). Does not evaluate values when comparing, but rather uses their representation as strings and their types. This instance works for ill-typed expressions. Expressions come first when they have smaller complexity (`compareComplexity`) or when they come first lexicographically (`compareLexicographically`).
Instance details Defined in Data.Express.Core Methods compare :: Expr -> Expr -> Ordering # (<) :: Expr -> Expr -> Bool # (<=) :: Expr -> Expr -> Bool # (>) :: Expr -> Expr -> Bool # (>=) :: Expr -> Expr -> Bool # max :: Expr -> Expr -> Expr # min :: Expr -> Expr -> Expr #

constant :: Typeable a => String -> a -> Expr Source #

showConstant :: (Typeable a, Show a) => a -> Expr Source #

hole :: Typeable a => a -> Expr #

O(1). Creates an Expr representing a typed hole of the given argument type.

> hole (undefined :: Int)
_ :: Int

> hole (undefined :: Maybe String)
_ :: Maybe [Char]

A hole is represented as a variable with no name or a value named "_":

hole x = var "" x
hole x = value "_" x

foreground :: Expr Source #

A special Expr value. When provided on the constants list, makes all the following constants foreground constants.

background :: Expr Source #

A special Expr value. When provided on the constants list, makes all the following constants background constants. Background constants can appear in laws about other constants, but not by themselves.

The instances list

The following combinators are used to build the instances list from Args.

type Instances = [Expr] Source #

reifyInstances :: (Typeable a, Listable a, Show a, Eq a, Ord a, Name a) => a -> Instances Source #

reifyEq :: (Typeable a, Eq a) => a -> [Expr] #

O(1). Reifies an Eq instance into a list of Exprs. The list will contain == and /= for the given type. (cf. mkEq, mkEquation)

> reifyEq (undefined :: Int)
[ (==) :: Int -> Int -> Bool
, (/=) :: Int -> Int -> Bool ]

> reifyEq (undefined :: Bool)
[ (==) :: Bool -> Bool -> Bool
, (/=) :: Bool -> Bool -> Bool ]

> reifyEq (undefined :: String)
[ (==) :: [Char] -> [Char] -> Bool
, (/=) :: [Char] -> [Char] -> Bool ]

reifyOrd :: (Typeable a, Ord a) => a -> [Expr] #

O(1). Reifies an Ord instance into a list of Exprs. The list will contain compare, <= and < for the given type. (cf. mkOrd, mkOrdLessEqual, mkComparisonLE, mkComparisonLT)

> reifyOrd (undefined :: Int)
[ (<=) :: Int -> Int -> Bool
, (<) :: Int -> Int -> Bool ]

> reifyOrd (undefined :: Bool)
[ (<=) :: Bool -> Bool -> Bool
, (<) :: Bool -> Bool -> Bool ]

> reifyOrd (undefined :: [Bool])
[ (<=) :: [Bool] -> [Bool] -> Bool
, (<) :: [Bool] -> [Bool] -> Bool ]

reifyEqOrd :: (Typeable a, Ord a) => a -> [Expr] #

O(1). Reifies Eq and Ord instances into a list of Expr.

reifyListable :: (Typeable a, Show a, Listable a) => a -> Instances Source #

reifyName :: (Typeable a, Name a) => a -> [Expr] #

O(1). Reifies a Name instance into a list of Exprs. The list will contain name for the given type. (cf. mkName, lookupName, lookupNames)

> reifyName (undefined :: Int)
[name :: Int -> [Char]]

> reifyName (undefined :: Bool)
[name :: Bool -> [Char]]

mkEq :: Typeable a => (a -> a -> Bool) -> [Expr] #

O(1). Builds a reified Eq instance from the given == function. (cf. reifyEq)

> mkEq ((==) :: Int -> Int -> Bool)
[ (==) :: Int -> Int -> Bool
, (/=) :: Int -> Int -> Bool ]

mkOrd :: Typeable a => (a -> a -> Ordering) -> [Expr] #

O(1). Builds a reified Ord instance from the given compare function. (cf. reifyOrd, mkOrdLessEqual)

mkOrdLessEqual :: Typeable a => (a -> a -> Bool) -> [Expr] #

O(1). Builds a reified Ord instance from the given <= function. (cf. reifyOrd, mkOrd)

mkListable :: (Typeable a, Show a) => [[a]] -> [Expr] Source #

mkNameWith :: Typeable a => String -> a -> [Expr] #

O(1). Builds a reified Name instance from the given String and type. (cf. reifyName, mkName)

class Name a where #

If we were to come up with a variable name for the given type what name would it be?

An instance for a given type Ty is simply given by:

instance Name Ty where name _ = "x"

Examples:

> name (undefined :: Int)
"x"

> name (undefined :: Bool)
"p"

> name (undefined :: [Int])
"xs"

This is then used to generate an infinite list of variable names:

> names (undefined :: Int)
["x", "y", "z", "x'", "y'", "z'", "x''", "y''", "z''", ...]

> names (undefined :: Bool)
["p", "q", "r", "p'", "q'", "r'", "p''", "q''", "r''", ...]

> names (undefined :: [Int])
["xs", "ys", "zs", "xs'", "ys'", "zs'", "xs''", "ys''", ...]

Minimal complete definition

Nothing

Methods

name :: a -> String #

O(1).

Returns a name for a variable of the given argument's type.

> name (undefined :: Int)
"x"

> name (undefined :: [Bool])
"ps"

> name (undefined :: [Maybe Integer])
"mxs"

The default definition is:

name _ = "x"

Instances

Instances details

Name Int16
Instance details Defined in Data.Express.Name Methods name :: Int16 -> String #
Name Int32
Instance details Defined in Data.Express.Name Methods name :: Int32 -> String #
Name Int64
Instance details Defined in Data.Express.Name Methods name :: Int64 -> String #
Name Int8
Instance details Defined in Data.Express.Name Methods name :: Int8 -> String #
Name GeneralCategory
Instance details Defined in Data.Express.Name Methods name :: GeneralCategory -> String #
Name Word16
Instance details Defined in Data.Express.Name Methods name :: Word16 -> String #
Name Word32
Instance details Defined in Data.Express.Name Methods name :: Word32 -> String #
Name Word64
Instance details Defined in Data.Express.Name Methods name :: Word64 -> String #
Name Word8
Instance details Defined in Data.Express.Name Methods name :: Word8 -> String #
Name Ordering	name (undefined :: Ordering) = "o" names (undefined :: Ordering) = ["o", "p", "q", "o'", ...]
Instance details Defined in Data.Express.Name Methods name :: Ordering -> String #
Name Integer	name (undefined :: Integer) = "x" names (undefined :: Integer) = ["x", "y", "z", "x'", ...]
Instance details Defined in Data.Express.Name Methods name :: Integer -> String #
Name ()	name (undefined :: ()) = "u" names (undefined :: ()) = ["u", "v", "w", "u'", "v'", ...]
Instance details Defined in Data.Express.Name Methods name :: () -> String #
Name Bool	name (undefined :: Bool) = "p" names (undefined :: Bool) = ["p", "q", "r", "p'", "q'", ...]
Instance details Defined in Data.Express.Name Methods name :: Bool -> String #
Name Char	name (undefined :: Char) = "c" names (undefined :: Char) = ["c", "d", "e", "c'", "d'", ...]
Instance details Defined in Data.Express.Name Methods name :: Char -> String #
Name Double	name (undefined :: Double) = "x" names (undefined :: Double) = ["x", "y", "z", "x'", ...]
Instance details Defined in Data.Express.Name Methods name :: Double -> String #
Name Float	name (undefined :: Float) = "x" names (undefined :: Float) = ["x", "y", "z", "x'", ...]
Instance details Defined in Data.Express.Name Methods name :: Float -> String #
Name Int	name (undefined :: Int) = "x" names (undefined :: Int) = ["x", "y", "z", "x'", "y'", ...]
Instance details Defined in Data.Express.Name Methods name :: Int -> String #
Name Word
Instance details Defined in Data.Express.Name Methods name :: Word -> String #
Name (Complex a)	name (undefined :: Complex) = "x" names (undefined :: Complex) = ["x", "y", "z", "x'", ...]
Instance details Defined in Data.Express.Name Methods name :: Complex a -> String #
Name (Ratio a)	name (undefined :: Rational) = "q" names (undefined :: Rational) = ["q", "r", "s", "q'", ...]
Instance details Defined in Data.Express.Name Methods name :: Ratio a -> String #
Name a => Name (Maybe a)	names (undefined :: Maybe Int) = ["mx", "mx1", "mx2", ...] nemes (undefined :: Maybe Bool) = ["mp", "mp1", "mp2", ...]
Instance details Defined in Data.Express.Name Methods name :: Maybe a -> String #
Name a => Name [a]	names (undefined :: [Int]) = ["xs", "ys", "zs", "xs'", ...] names (undefined :: [Bool]) = ["ps", "qs", "rs", "ps'", ...]
Instance details Defined in Data.Express.Name Methods name :: [a] -> String #
(Name a, Name b) => Name (Either a b)	names (undefined :: Either Int Int) = ["exy", "exy1", ...] names (undefined :: Either Int Bool) = ["exp", "exp1", ...]
Instance details Defined in Data.Express.Name Methods name :: Either a b -> String #
(Name a, Name b) => Name (a, b)	names (undefined :: (Int,Int)) = ["xy", "zw", "xy'", ...] names (undefined :: (Bool,Bool)) = ["pq", "rs", "pq'", ...]
Instance details Defined in Data.Express.Name Methods name :: (a, b) -> String #
Name (a -> b)	names (undefined :: ()->()) = ["f", "g", "h", "f'", ...] names (undefined :: Int->Int) = ["f", "g", "h", ...]
Instance details Defined in Data.Express.Name Methods name :: (a -> b) -> String #
(Name a, Name b, Name c) => Name (a, b, c)	names (undefined :: (Int,Int,Int)) = ["xyz","uvw", ...] names (undefined :: (Int,Bool,Char)) = ["xpc", "xpc1", ...]
Instance details Defined in Data.Express.Name Methods name :: (a, b, c) -> String #
(Name a, Name b, Name c, Name d) => Name (a, b, c, d)	names (undefined :: ((),(),(),())) = ["uuuu", "uuuu1", ...] names (undefined :: (Int,Int,Int,Int)) = ["xxxx", ...]
Instance details Defined in Data.Express.Name Methods name :: (a, b, c, d) -> String #
(Name a, Name b, Name c, Name d, Name e) => Name (a, b, c, d, e)
Instance details Defined in Data.Express.Name Methods name :: (a, b, c, d, e) -> String #
(Name a, Name b, Name c, Name d, Name e, Name f) => Name (a, b, c, d, e, f)
Instance details Defined in Data.Express.Name Methods name :: (a, b, c, d, e, f) -> String #
(Name a, Name b, Name c, Name d, Name e, Name f, Name g) => Name (a, b, c, d, e, f, g)
Instance details Defined in Data.Express.Name Methods name :: (a, b, c, d, e, f, g) -> String #
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h) => Name (a, b, c, d, e, f, g, h)
Instance details Defined in Data.Express.Name Methods name :: (a, b, c, d, e, f, g, h) -> String #
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i) => Name (a, b, c, d, e, f, g, h, i)
Instance details Defined in Data.Express.Name Methods name :: (a, b, c, d, e, f, g, h, i) -> String #
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i, Name j) => Name (a, b, c, d, e, f, g, h, i, j)
Instance details Defined in Data.Express.Name Methods name :: (a, b, c, d, e, f, g, h, i, j) -> String #
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i, Name j, Name k) => Name (a, b, c, d, e, f, g, h, i, j, k)
Instance details Defined in Data.Express.Name Methods name :: (a, b, c, d, e, f, g, h, i, j, k) -> String #
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i, Name j, Name k, Name l) => Name (a, b, c, d, e, f, g, h, i, j, k, l)
Instance details Defined in Data.Express.Name Methods name :: (a, b, c, d, e, f, g, h, i, j, k, l) -> String #

Misc.

report :: Args -> IO () Source #

getArgs :: Args -> IO Args Source #

module Test.LeanCheck

module Test.LeanCheck.Utils

module Data.Typeable