Documentation

A quantified type representation.

Is an expression ALWAYS false? This is *NOT* the same as not true

Under a maximum number of tests, returns the ratio for which an expression holds true.

List variable bindings for which an expression holds true.

Is a boolean expression true for all variable assignments?

Are two expressions inequal for *all* variable assignments? Note this is different than not . equal.

Are two expressions less-than for a given number of tests?

Are two expressions less-than-or-equal for a given number of tests?

Are two expressions equal under a given condition for a given number of tests and a minimum amount of tests

Are two expressions equal under a given condition for a given number of tests?

Are two expressions equal for a given number of tests?

List all possible variable bindings and valuations to an expression

groundAndBinds ti e == zipWith (,) (grounds ti e) (groundBinds ti e)

List all possible variable bindings to an expression

take 3 $ groundBinds preludeInstances ((x + x) + y)
  == [ [("x",0),("y",0)]
     , [("x",0),("y",1)]
     , [("x",1),("y",0)] ]

Given an equation encoded as an Expr. Checks if both sides of an equation are the same. If the Expr is not an equation, this raises an error.

Type information needed to Speculate expressions (single type / single class).

Type information needed to Speculate expressions.

List matches with preexisting bindings:

0 + 1 `matchWith [(x,0)]` x + y = Just [x=0, y=1]
0 + 1 `matchWith [(x,1)]` x + y = Nothing

List matches of pairs of expressions if possible

(0,1)   `match2` (x,y)   = Just [x=0, y=1]
(0,1+2) `match2` (x,y+y) = Nothing

List matches if possible

0 + 1       `match` x + y       = Just [x=0, y=1]
0 + (1 + 2) `match` x + y       = Just [x=0, y=1 + 2]
0 + (1 + 2) `match` x + (y + y) = Nothing
(x + x) + (1 + 2) `match` x + (y + y) = Nothing

Primeify variable names in an expression.

renameBy (++ "'") (x + y) = (x' + y')
renameBy (++ "'") (y + (z + x)) = (y' + (z' + x'))
renameBy (++ "1") abs x = abs x1
renameBy (++ "2") abs (x + y) = abs (x2 + y2)

Note this will affect holes!

Substitute matching subexpressios.

sub (x + y) 0 ((x + y) + z) == (0 + z) sub (x + y) 0 (x + (y + z)) == (x + (y + z))

Assign all occurrences of several variables in an expression.

For single variables, this works as assign:

x + y `assigning` [("x",10)] = (10 + y)
((x + y) + (y + z)) `assigning` [("y",y+z)] = (x + (y + z)) + ((y + z) + z)

Note this is not equivalent to foldr (uncurry assign). Variables inside expressions being assigned will not be assigned.

Assign all occurences of a variable in an expression.

Examples in pseudo-Haskell:

assign "x" (10) (x + y) = (10 + y)
assign "y" (y + z) ((x + y) + (y + z)) = (x + (y + z)) + ((y + z) + z)

This respects the type (won't change occurrences of a similarly named variable of a different type).

Fill holes in an expression. Silently skips holes that are not of the right type. Silently discard remaining expressions.

Unfold function application:

(((f :$ e1) :$ e2) :$ e3) = [f,e1,e2,e3]

Is a subexpression of.

Sub-expressions of an expression including variables and the expression itself.

Non-variable sub-expressions of an expression

This includes the expression itself

Number of occurrences of a given variable name. In term rewriting terms: |s|_x

Number of occurrences of holes with a given type.

Returns the maximum depth of an expression.

Returns the length of an expression. In term rewriting terms: |s|

List terminal constants in an expression. This does not repeat values.

List types holes (unamed variables) in an expression

Type arity of an Expr

etyp returns either: the Right type a Left expression with holes with the structure of the I'll typed expression

The type of an expression. This raises errors, but those should not happen if expressions are smart-constructed.

Evaluates an expression when possible (correct type, no holes). Returns a default value otherwise.

Just the value of an expression when possible (correct type, no holes), Nothing otherwise.

Compares two expressions first by their complexity: 1st length; 2nd number of variables (more variables is less complex); 3nd sum of number of variable occurrences; 4th their depth; 5th lexicompare.

Compares two expressions first by their complexity: 1st length; 2nd number of variables (more variables is less complex); 3nd sum of number of variable occurrences; 4th their depth; 5th normal compare.

Compare two expressiosn lexicographically

1st their type arity; 2nd their type; 3rd var < constants < apps 4th lexicographic order on names

Just an Expr application if the types match, Nothing otherwise.

(intended for advanced users)

hole (undefined :: Ty) returns a hole of type Ty

By convention, a Hole is a variable named with the empty string.

var "x" (undefined :: Ty) returns a variable of type Ty named "x"

A shorthand for constant to be used on values that are Show instances. Examples:

showConstant 0     =  constant "0" 0
showConstant 'a'   =  constant "'a'" 'a' 
showConstant True  =  constant "True" True

Encode a constant Haskell expression for use by Speculate. It takes a string representation of a value and a value, returning an Expr. Examples:

constant "0" 0
constant "'a'" 'a'
constant "True" True
constant "id" (id :: Int -> Int)
constant "(+)" ((+) :: Int -> Int -> Int)
constant "sort" (sort :: [Bool] -> [Bool])

An encoded Haskell functional-application expression for use by Speculate.