Copyright	(c) 2017-2019 Rudy Matela
License	3-Clause BSD (see the file LICENSE)
Maintainer	Rudy Matela <[email protected]>
Safe Haskell	None
Language	Haskell2010

Test.Extrapolate.Speculation

Description

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

This defines utilities for speculation about side conditions.

You are probably better off importing Test.Extrapolate.

Synopsis

theoryAndReprConds :: Int -> (Expr -> Expr -> Bool) -> [[Expr]] -> (Thy, [Expr])
data Thy
data Expr
classesFromSchemasAndVariables :: Thy -> [Expr] -> [Expr] -> [Class Expr]

Documentation

theoryAndReprConds :: Int -> (Expr -> Expr -> Bool) -> [[Expr]] -> (Thy, [Expr]) Source #

data Thy #

Instances

Eq Thy	This instance is as efficient as it gets, but, this function will not detect equality when rules and equations are in a different order (or repeated). See `\|==\|`.
Instance details Defined in Test.Speculate.Reason Methods (==) :: Thy -> Thy -> Bool # (/=) :: Thy -> Thy -> Bool #

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

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
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 #
Show Expr
Instance details Defined in Data.Express.Core Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #

classesFromSchemasAndVariables :: Thy -> [Expr] -> [Expr] -> [Class Expr] #