Conjure.Engine

An internal module of Conjure, a library for Conjuring function implementations from tests or partial definitions. (a.k.a.: functional inductive programming)

Documentation

conjure :: Conjurable f => String -> f -> [Prim] -> IO ()

Conjures an implementation of a partially defined function.

Takes a String with the name of a function, a partially-defined function from a conjurable type, and a list of building blocks encoded as Exprs.

For example, given:

square :: Int -> Int
square 0  =  0
square 1  =  1
square 2  =  4

primitives :: [Prim]
primitives =
  [ pr (0::Int)
  , pr (1::Int)
  , prim "+" ((+) :: Int -> Int -> Int)
  , prim "*" ((*) :: Int -> Int -> Int)
  ]

The conjure function does the following:

> conjure "square" square primitives
square :: Int -> Int
-- pruning with 14/25 rules
-- testing 3 combinations of argument values
-- looking through 3 candidates of size 1
-- looking through 3 candidates of size 2
-- looking through 5 candidates of size 3
square x  =  x * x

The primitives list is defined with pr and prim.

conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()

Like conjure but allows setting the maximum size of considered expressions instead of the default value of 12.

conjureWithMaxSize 10 "function" function [...]

data Args

Arguments to be passed to conjureWith or conjpureWith. See args for the defaults.

Constructors

Args

Fields

• maxTests :: Int

  maximum number of tests to each candidate

• maxSize :: Int

  maximum size of candidate bodies

• maxEvalRecursions :: Int

  maximum number of recursive evaluations when testing candidates

• maxEquationSize :: Int

  maximum size of equation operands

• maxSearchTests :: Int

  maximum number of tests to search for defined values

• maxDeconstructionSize :: Int

  maximum size of deconstructions (e.g.: _ - 1)

• requireDescent :: Bool

  require recursive calls to deconstruct arguments

• usePatterns :: Bool

  use pattern matching to create (recursive) candidates

• copyBindings :: Bool

  copy partial definition bindings in candidates

• atomicNumbers :: Bool

  restrict constant/ground numeric expressions to atoms

• showTheory :: Bool

  show theory discovered by Speculate used in pruning

• uniqueCandidates :: Bool

  unique-modulo-testing candidates

args :: Args

Default arguments to conjure.

• 60 tests
• functions of up to 12 symbols
• maximum of one recursive call allowed in candidate bodies
• maximum evaluation of up to 60 recursions
• pruning with equations up to size 5
• search for defined applications for up to 100000 combinations
• require recursive calls to deconstruct arguments
• don't show the theory used in pruning
• do not make candidates unique module testing

conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()

Like conjure but allows setting options through Args/args.

conjureWith args{maxSize = 11} "function" function [...]

conjureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> IO ()

Conjures an implementation from a function specification.

This function works like conjure but instead of receiving a partial definition it receives a boolean filter / property about the function.

For example, given:

squareSpec :: (Int -> Int) -> Bool
squareSpec square  =  square 0 == 0
                   && square 1 == 1
                   && square 2 == 4

Then:

> conjureFromSpec "square" squareSpec primitives
square :: Int -> Int
-- pruning with 14/25 rules
-- looking through 3 candidates of size 1
-- looking through 4 candidates of size 2
-- looking through 9 candidates of size 3
square x  =  x * x

This allows users to specify QuickCheck-style properties, here is an example using LeanCheck:

import Test.LeanCheck (holds, exists)

squarePropertySpec :: (Int -> Int) -> Bool
squarePropertySpec square  =  and
  [ holds n $ \x -> square x >= x
  , holds n $ \x -> square x >= 0
  , exists n $ \x -> square x > x
  ]  where  n = 60

conjureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> IO ()

Like conjureFromSpec but allows setting options through Args/args.

conjureFromSpecWith args{maxSize = 11} "function" spec [...]

conjure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> IO ()

Synthesizes an implementation from both a partial definition and a function specification.

This works like the functions conjure and conjureFromSpec combined.

conjure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()

Like conjure0 but allows setting options through Args/args.

conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)

Like conjure but in the pure world.

Returns a quadruple with:

1. tiers of implementations
2. tiers of candidates
3. a list of tests
4. the underlying theory

conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)

Like conjpure but allows setting options through Args and args.

conjpureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)

Like conjureFromSpec but in the pure world. (cf. conjpure)

conjpureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)

Like conjureFromSpecWith but in the pure world. (cf. conjpure)

conjpure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)

Like conjure0 but in the pure world. (cf. conjpure)

conjpure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)

Like conjpure0 but allows setting options through Args and args.

This is where the actual implementation resides. The functions conjpure, conjpureWith, conjpureFromSpec, conjpureFromSpecWith, conjure, conjureWith, conjureFromSpec, conjureFromSpecWith and conjure0 all refer to this.

candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy)

Return apparently unique candidate bodies.

candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)

Return apparently unique candidate definitions.

candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)

Return apparently unique candidate definitions where there is a single body.

candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)

Return apparently unique candidate definitions using pattern matching.

conjureTheory :: Conjurable f => String -> f -> [Prim] -> IO ()

Just prints the underlying theory found by Test.Speculate without actually synthesizing a function.

conjureTheoryWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()

Like conjureTheory but allows setting options through Args/args.

module Data.Express

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

Name Int16

Defined in Data.Express.Name

Methods

name :: Int16 -> String

Name Int32

Defined in Data.Express.Name

Methods

name :: Int32 -> String

Name Int64

Defined in Data.Express.Name

Methods

name :: Int64 -> String

Name Int8

Defined in Data.Express.Name

Methods

name :: Int8 -> String

Name GeneralCategory

Defined in Data.Express.Name

Methods

name :: GeneralCategory -> String

Name Word16

Defined in Data.Express.Name

Methods

name :: Word16 -> String

Name Word32

Defined in Data.Express.Name

Methods

name :: Word32 -> String

Name Word64

Defined in Data.Express.Name

Methods

name :: Word64 -> String

Name Word8

Defined in Data.Express.Name

Methods

name :: Word8 -> String

Name Ordering

name (undefined :: Ordering) = "o"
names (undefined :: Ordering) = ["o", "p", "q", "o'", ...]

Defined in Data.Express.Name

Methods

name :: Ordering -> String

Name A

Defined in Conjure.Conjurable

Methods

name :: A -> String

Name B

Defined in Conjure.Conjurable

Methods

name :: B -> String

Name C

Defined in Conjure.Conjurable

Methods

name :: C -> String

Name D

Defined in Conjure.Conjurable

Methods

name :: D -> String

Name E

Defined in Conjure.Conjurable

Methods

name :: E -> String

Name F

Defined in Conjure.Conjurable

Methods

name :: F -> String

Name Integer

name (undefined :: Integer) = "x"
names (undefined :: Integer) = ["x", "y", "z", "x'", ...]

Defined in Data.Express.Name

Methods

name :: Integer -> String

Name ()

name (undefined :: ()) = "u"
names (undefined :: ()) = ["u", "v", "w", "u'", "v'", ...]

Defined in Data.Express.Name

Methods

name :: () -> String

Name Bool

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

Defined in Data.Express.Name

Methods

name :: Bool -> String

Name Char

name (undefined :: Char) = "c"
names (undefined :: Char) = ["c", "d", "e", "c'", "d'", ...]

Defined in Data.Express.Name

Methods

name :: Char -> String

Name Double

name (undefined :: Double) = "x"
names (undefined :: Double) = ["x", "y", "z", "x'", ...]

Defined in Data.Express.Name

Methods

name :: Double -> String

Name Float

name (undefined :: Float) = "x"
names (undefined :: Float) = ["x", "y", "z", "x'", ...]

Defined in Data.Express.Name

Methods

name :: Float -> String

Name Int

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

Defined in Data.Express.Name

Methods

name :: Int -> String

Name Word

Defined in Data.Express.Name

Methods

name :: Word -> String

Name (Complex a)

name (undefined :: Complex) = "x"
names (undefined :: Complex) = ["x", "y", "z", "x'", ...]

Defined in Data.Express.Name

Methods

name :: Complex a -> String

Name (Ratio a)

name (undefined :: Rational) = "q"
names (undefined :: Rational) = ["q", "r", "s", "q'", ...]

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", ...]

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'", ...]

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", ...]

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'", ...]

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", ...]

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", ...]

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", ...]

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Express.Name

Methods

name :: (a, b, c, d, e, f, g, h, i, j, k, l) -> String

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.

Constructors

Value String Dynamic

a value enconded as String and Dynamic

Expr :$ Expr

function application between expressions

Instances

Show Expr

Shows Exprs with their types.

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

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.

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).

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

class (Show a, Typeable a) => Express a where

Express typeclass instances provide an expr function that allows values to be deeply encoded as applications of Exprs.

expr False  =  val False
expr (Just True)  =  value "Just" (Just :: Bool -> Maybe Bool) :$ val True

The function expr can be contrasted with the function val:

• val always encodes values as atomic Value Exprs -- shallow encoding.
• expr ideally encodes expressions as applications (:$) between Value Exprs -- deep encoding.

Depending on the situation, one or the other may be desirable.

Instances can be automatically derived using the TH function deriveExpress.

The following example shows a datatype and its instance:

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

instance Express a => Express (Stack a) where
  expr s@(Stack x y) = value "Stack" (Stack ->>: s) :$ expr x :$ expr y
  expr s@Empty       = value "Empty" (Empty   -: s)

To declare expr it may be useful to use auxiliary type binding operators: -:, ->:, ->>:, ->>>:, ->>>>:, ->>>>>:, ...

For types with atomic values, just declare expr = val

Methods

expr :: a -> Expr

Instances

Express Int16

Defined in Data.Express.Express

Methods

expr :: Int16 -> Expr

Express Int32

Defined in Data.Express.Express

Methods

expr :: Int32 -> Expr

Express Int64

Defined in Data.Express.Express

Methods

expr :: Int64 -> Expr

Express Int8

Defined in Data.Express.Express

Methods

expr :: Int8 -> Expr

Express GeneralCategory

Defined in Data.Express.Express

Methods

expr :: GeneralCategory -> Expr

Express Word16

Defined in Data.Express.Express

Methods

expr :: Word16 -> Expr

Express Word32

Defined in Data.Express.Express

Methods

expr :: Word32 -> Expr

Express Word64

Defined in Data.Express.Express

Methods

expr :: Word64 -> Expr

Express Word8

Defined in Data.Express.Express

Methods

expr :: Word8 -> Expr

Express Ordering

Defined in Data.Express.Express

Methods

expr :: Ordering -> Expr

Express A

Defined in Conjure.Expr

Methods

expr :: A -> Expr

Express B

Defined in Conjure.Expr

Methods

expr :: B -> Expr

Express C

Defined in Conjure.Expr

Methods

expr :: C -> Expr

Express D

Defined in Conjure.Expr

Methods

expr :: D -> Expr

Express E

Defined in Conjure.Expr

Methods

expr :: E -> Expr

Express F

Defined in Conjure.Expr

Methods

expr :: F -> Expr

Express Integer

Defined in Data.Express.Express

Methods

expr :: Integer -> Expr

Express ()

Defined in Data.Express.Express

Methods

expr :: () -> Expr

Express Bool

Defined in Data.Express.Express

Methods

expr :: Bool -> Expr

Express Char

Defined in Data.Express.Express

Methods

expr :: Char -> Expr

Express Double

Defined in Data.Express.Express

Methods

expr :: Double -> Expr

Express Float

Defined in Data.Express.Express

Methods

expr :: Float -> Expr

Express Int

Defined in Data.Express.Express

Methods

expr :: Int -> Expr

Express Word

Defined in Data.Express.Express

Methods

expr :: Word -> Expr

(RealFloat a, Express a) => Express (Complex a)

Defined in Data.Express.Express

Methods

expr :: Complex a -> Expr

(Integral a, Express a) => Express (Ratio a)

Defined in Data.Express.Express

Methods

expr :: Ratio a -> Expr

Express a => Express (Maybe a)

Defined in Data.Express.Express

Methods

expr :: Maybe a -> Expr

Express a => Express [a]

Defined in Data.Express.Express

Methods

expr :: [a] -> Expr

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

Defined in Data.Express.Express

Methods

expr :: Either a b -> Expr

(Express a, Express b) => Express (a, b)

Defined in Data.Express.Express

Methods

expr :: (a, b) -> Expr

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

Defined in Data.Express.Express

Methods

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

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

Defined in Data.Express.Express

Methods

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

(Express a, Express b, Express c, Express d, Express e) => Express (a, b, c, d, e)

Defined in Data.Express.Express

Methods

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

(Express a, Express b, Express c, Express d, Express e, Express f) => Express (a, b, c, d, e, f)

Defined in Data.Express.Express

Methods

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

(Express a, Express b, Express c, Express d, Express e, Express f, Express g) => Express (a, b, c, d, e, f, g)

Defined in Data.Express.Express

Methods

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

(Express a, Express b, Express c, Express d, Express e, Express f, Express g, Express h) => Express (a, b, c, d, e, f, g, h)

Defined in Data.Express.Express

Methods

expr :: (a, b, c, d, e, f, g, h) -> Expr

(Express a, Express b, Express c, Express d, Express e, Express f, Express g, Express h, Express i) => Express (a, b, c, d, e, f, g, h, i)

Defined in Data.Express.Express

Methods

expr :: (a, b, c, d, e, f, g, h, i) -> Expr

(Express a, Express b, Express c, Express d, Express e, Express f, Express g, Express h, Express i, Express j) => Express (a, b, c, d, e, f, g, h, i, j)

Defined in Data.Express.Express

Methods

expr :: (a, b, c, d, e, f, g, h, i, j) -> Expr

(Express a, Express b, Express c, Express d, Express e, Express f, Express g, Express h, Express i, Express j, Express k) => Express (a, b, c, d, e, f, g, h, i, j, k)

Defined in Data.Express.Express

Methods

expr :: (a, b, c, d, e, f, g, h, i, j, k) -> Expr

(Express a, Express b, Express c, Express d, Express e, Express f, Express g, Express h, Express i, Express j, Express k, Express l) => Express (a, b, c, d, e, f, g, h, i, j, k, l)

Defined in Data.Express.Express

Methods

expr :: (a, b, c, d, e, f, g, h, i, j, k, l) -> Expr

(//) :: Expr -> [(Expr, Expr)] -> Expr

O(n*n*m). Substitute subexpressions in an expression from the given list of substitutions. (cf. mapSubexprs).

Please consider using //- if you are replacing just terminal values as it is faster.

Given that:

> let xx = var "x" (undefined :: Int)
> let yy = var "y" (undefined :: Int)
> let zz = var "z" (undefined :: Int)
> let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy

Then:

> ((xx -+- yy) -+- (yy -+- zz)) // [(xx -+- yy, yy), (yy -+- zz, yy)]
y + y :: Int

> ((xx -+- yy) -+- zz) // [(xx -+- yy, zz), (zz, xx -+- yy)]
z + (x + y) :: Int

Replacement happens only once with outer expressions having more precedence than inner expressions.

> (xx -+- yy) // [(yy,xx), (xx -+- yy,zz), (zz,xx)]
z :: Int

Given that the argument list has length m, this function is O(n*n*m). Remember that since n is the size of an expression, comparing two expressions is O(n) in the worst case, and we may need to compare with n subexpressions in the worst case.

foldr' :: Expr -> Expr -> Expr -> Expr

foldr lifted over Exprs.

> foldr' plus zero (unit one)
foldr (+) zero [1] :: [Int]

fill :: Expr -> [Expr] -> Expr

Fill holes in an expression with the given list.

> let i_  =  hole (undefined :: Int)
> let e1 -+- e2  =  value "+" ((+) :: Int -> Int -> Int) :$ e1 :$ e2
> let xx  =  var "x" (undefined :: Int)
> let yy  =  var "y" (undefined :: Int)

> fill (i_ -+- i_) [xx, yy]
x + y :: Int

> fill (i_ -+- i_) [xx, xx]
x + x :: Int

> let one  =  val (1::Int)

> fill (i_ -+- i_) [one, one -+- one]
1 + (1 + 1) :: Int

This function silently remaining expressions:

> fill i_ [xx, yy]
x :: Int

This function silently keeps remaining holes:

> fill (i_ -+- i_ -+- i_) [xx, yy]
(x + y) + _ :: Int

This function silently skips remaining holes if one is not of the right type:

> fill (i_ -+- i_ -+- i_) [xx, val 'c', yy]
(x + _) + _ :: Int

fold :: [Expr] -> Expr

O(n). Folds a list of Exprs into a single Expr. (cf. unfold)

This always generates an ill-typed expression.

fold [val False, val True, val (1::Int)]
[False,True,1] :: ill-typed # ExprList $ Bool #

This is useful when applying transformations on lists of Exprs, such as canonicalize, mapValues or canonicalVariations.

> let ii = var "i" (undefined::Int)
> let kk = var "k" (undefined::Int)
> let qq = var "q" (undefined::Bool)
> let notE = value "not" not
> unfold . canonicalize . fold $ [ii,kk,notE :$ qq, notE :$ val False]
[x :: Int,y :: Int,not p :: Bool,not False :: Bool]

evaluate :: Typeable a => Expr -> Maybe a

O(n). Just the value of an expression when possible (correct type), Nothing otherwise. This does not catch errors from undefined Dynamic values.

> let one = val (1 :: Int)
> let bee = val 'b'
> let negateE = value "negate" (negate :: Int -> Int)

> evaluate one :: Maybe Int
Just 1

> evaluate one :: Maybe Char
Nothing

> evaluate bee :: Maybe Int
Nothing

> evaluate bee :: Maybe Char
Just 'b'

> evaluate $ negateE :$ one :: Maybe Int
Just (-1)

> evaluate $ negateE :$ bee :: Maybe Int
Nothing

unfold :: Expr -> [Expr]

O(n). Unfolds an Expr representing a list into a list of Exprs. This reverses the effect of fold.

> expr [1,2,3::Int]
[1,2,3] :: [Int]
> unfold $ expr [1,2,3::Int]
[1 :: Int,2 :: Int,3 :: Int]

cons :: Expr

The list constructor with Int as element type encoded as an Expr.

> cons
(:) :: Int -> [Int] -> [Int]

> cons :$ one :$ nil
[1] :: [Int]

Consider using -:- and unit when building lists of Expr.

div' :: Expr -> Expr -> Expr

The function div for the Int type lifted over the Expr type. (See also mod.)

> six `div'` four
6 `div` 4 :: Int

mod' :: Expr -> Expr -> Expr

The function mod for the Int type lifted over the Expr type. (See also div.)

> six `mod'` four
6 `mod` 4 :: Int

(>$$<) :: [Expr] -> [Expr] -> [Expr]

Lists valid applications between lists of Exprs

> [notE, plus] >$$< [false, true, zero]
[not False :: Bool,not True :: Bool,(0 +) :: Int -> Int]

size :: Expr -> Int

O(n). Returns the size of the given expression, i.e. the number of terminal values in it.

zero       =  val (0 :: Int)
one        =  val (1 :: Int)
two        =  val (2 :: Int)
xx -+- yy  =  value "+" ((+) :: Int->Int->Int) :$ xx :$ yy
abs' xx    =  value "abs" (abs :: Int->Int) :$ xx

> size zero
1

> size (one -+- two)
3

> size (abs' one)
2

value :: Typeable a => String -> a -> Expr

O(1). It takes a string representation of a value and a value, returning an Expr with that terminal value. For instances of Show, it is preferable to use val.

> value "0" (0 :: Integer)
0 :: Integer

> value "'a'" 'a'
'a' :: Char

> value "True" True
True :: Bool

> value "id" (id :: Int -> Int)
id :: Int -> Int

> value "(+)" ((+) :: Int -> Int -> Int)
(+) :: Int -> Int -> Int

> value "sort" (sort :: [Bool] -> [Bool])
sort :: [Bool] -> [Bool]

times :: Expr

The operator * for the Int type. (See also -*-.)

> times
(*) :: Int -> Int -> Int

> times :$ two
(2 *) :: Int -> Int

> times :$ xx :$ yy
x * y :: Int

typ :: Expr -> TypeRep

O(n). Computes the type of an expression. This raises errors, but this should not happen if expressions are smart-constructed with $$.

> let one = val (1 :: Int)
> let bee = val 'b'
> let absE = value "abs" (abs :: Int -> Int)

> typ one
Int

> typ bee
Char

> typ absE
Int -> Int

> typ (absE :$ one)
Int

> typ (absE :$ bee)
*** Exception: type mismatch, cannot apply `Int -> Int' to `Char'

> typ ((absE :$ bee) :$ one)
*** Exception: type mismatch, cannot apply `Int -> Int' to `Char'

arity :: Expr -> Int

O(n). Return the arity of the given expression, i.e. the number of arguments that its type takes.

> arity (val (0::Int))
0

> arity (val False)
0

> arity (value "id" (id :: Int -> Int))
1

> arity (value "const" (const :: Int -> Int -> Int))
2

> arity (one -+- two)
0

compose :: Expr

Function composition encoded as an Expr:

> compose
(.) :: (Int -> Int) -> (Int -> Int) -> Int -> Int

unit :: Expr -> Expr

unit constructs a list with a single element. This works for elements of type Int, Char and Bool.

> unit one
[1]

> unit false
[False]

zero :: Expr

The value 0 bound to the Int type encoded as an Expr.

> zero
0 :: Int

match :: Expr -> Expr -> Maybe [(Expr, Expr)]

Given two expressions, returns a Just list of matches of subexpressions of the first expressions to variables in the second expression. Returns Nothing when there is no match.

> let zero = val (0::Int)
> let one  = val (1::Int)
> let xx   = var "x" (undefined :: Int)
> let yy   = var "y" (undefined :: Int)
> let e1 -+- e2  =  value "+" ((+)::Int->Int->Int) :$ e1 :$ e2

> (zero -+- one) `match` (xx -+- yy)
Just [(y :: Int,1 :: Int),(x :: Int,0 :: Int)]

> (zero -+- (one -+- two)) `match` (xx -+- yy)
Just [(y :: Int,1 + 2 :: Int),(x :: Int,0 :: Int)]

> (zero -+- (one -+- two)) `match` (xx -+- (yy -+- yy))
Nothing

In short:

          (zero -+- one) `match` (xx -+- yy)           =  Just [(xx,zero), (yy,one)]
(zero -+- (one -+- two)) `match` (xx -+- yy)           =  Just [(xx,zero), (yy,one-+-two)]
(zero -+- (one -+- two)) `match` (xx -+- (yy -+- yy))  =  Nothing

canonicalize :: Expr -> Expr

Canonicalizes an Expr so that variable names appear in order. Variable names are taken from the preludeNameInstances.

> canonicalize (xx -+- yy)
x + y :: Int

> canonicalize (yy -+- xx)
x + y :: Int

> canonicalize (xx -+- xx)
x + x :: Int

> canonicalize (yy -+- yy)
x + x :: Int

Constants are untouched:

> canonicalize (jj -+- (zero -+- abs' ii))
x + (y + abs y) :: Int

This also works for variable functions:

> canonicalize (gg yy -+- ff xx -+- gg xx)
(f x + g y) + f y :: Int

mapValues :: (Expr -> Expr) -> Expr -> Expr

O(n*m). Applies a function to all terminal values in an expression. (cf. //-)

Given that:

> let zero  = val (0 :: Int)
> let one   = val (1 :: Int)
> let two   = val (2 :: Int)
> let three = val (3 :: Int)
> let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy
> let intToZero e = if typ e == typ zero then zero else e

Then:

> one -+- (two -+- three)
1 + (2 + 3) :: Int

> mapValues intToZero $ one -+- (two -+- three)
0 + (0 + 0) :: Integer

Given that the argument function is O(m), this function is O(n*m).

canonicalVariations :: Expr -> [Expr]

Returns all canonical variations of an Expr by filling holes with variables. Where possible, variations are listed from most general to least general.

> canonicalVariations $ i_
[x :: Int]

> canonicalVariations $ i_ -+- i_
[ x + y :: Int
, x + x :: Int ]

> canonicalVariations $ i_ -+- i_ -+- i_
[ (x + y) + z :: Int
, (x + y) + x :: Int
, (x + y) + y :: Int
, (x + x) + y :: Int
, (x + x) + x :: Int ]

> canonicalVariations $ i_ -+- ord' c_
[x + ord c :: Int]

> canonicalVariations $ i_ -+- i_ -+- ord' c_
[ (x + y) + ord c :: Int
, (x + x) + ord c :: Int ]

> canonicalVariations $ i_ -+- i_ -+- length' (c_ -:- unit c_)
[ (x + y) + length (c:d:"") :: Int
, (x + y) + length (c:c:"") :: Int
, (x + x) + length (c:d:"") :: Int
, (x + x) + length (c:c:"") :: Int ]

In an expression without holes this functions just returns a singleton list with the expression itself:

> canonicalVariations $ val (0 :: Int)
[0 :: Int]

> canonicalVariations $ ord' bee
[ord 'b' :: Int]

When applying this to expressions already containing variables clashes are avoided and these variables are not touched:

> canonicalVariations $ i_ -+- ii -+- jj -+- i_
[ x + i + j + y :: Int
, x + i + j + y :: Int ]

> canonicalVariations $ ii -+- jj
[i + j :: Int]

> canonicalVariations $ xx -+- i_ -+- i_ -+- length' (c_ -:- unit c_) -+- yy
[ (((x + z) + x') + length (c:d:"")) + y :: Int
, (((x + z) + x') + length (c:c:"")) + y :: Int
, (((x + z) + z) + length (c:d:"")) + y :: Int
, (((x + z) + z) + length (c:c:"")) + y :: Int
]

deriveExpress :: Name -> DecsQ

Derives an Express instance for the given type Name.

This function needs the TemplateHaskell extension.

If -:, ->:, ->>:, ->>>:, ... are not in scope, this will derive them as well.

variableNamesFromTemplate :: String -> [String]

Returns an infinite list of variable names based on the given template.

> variableNamesFromTemplate "x"
["x", "y", "z", "x'", "y'", ...]

> variableNamesFromTemplate "p"
["p", "q", "r", "p'", "q'", ...]

> variableNamesFromTemplate "xy"
["xy", "zw", "xy'", "zw'", "xy''", ...]

names :: Name a => a -> [String]

Returns na infinite list of variable names from the given type: the result of variableNamesFromTemplate after name.

> 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''", ...]

isInstanceOf :: Expr -> Expr -> Bool

Given two Exprs, checks if the first expression is an instance of the second in terms of variables. (cf. encompasses, hasInstanceOf)

> let zero = val (0::Int)
> let one  = val (1::Int)
> let xx   = var "x" (undefined :: Int)
> let yy   = var "y" (undefined :: Int)
> let e1 -+- e2  =  value "+" ((+)::Int->Int->Int) :$ e1 :$ e2

 one `isInstanceOf` one   =  True
  xx `isInstanceOf` xx    =  True
  yy `isInstanceOf` xx    =  True
zero `isInstanceOf` xx    =  True
  xx `isInstanceOf` zero  =  False
 one `isInstanceOf` zero  =  False
  (xx -+- (yy -+- xx)) `isInstanceOf`   (xx -+- yy)  =  True
  (yy -+- (yy -+- xx)) `isInstanceOf`   (xx -+- yy)  =  True
(zero -+- (yy -+- xx)) `isInstanceOf` (zero -+- yy)  =  True
 (one -+- (yy -+- xx)) `isInstanceOf` (zero -+- yy)  =  False

deriveName :: Name -> DecsQ

Derives a Name instance for the given type Name.

This function needs the TemplateHaskell extension.

deriveNameIfNeeded :: Name -> DecsQ

Same as deriveName but does not warn when instance already exists (deriveName is preferable).

deriveNameCascading :: Name -> DecsQ

Derives a Name instance for a given type Name cascading derivation of type arguments as well.

val :: (Typeable a, Show a) => a -> Expr

O(1). A shorthand for value for values that are Show instances.

> val (0 :: Int)
0 :: Int

> val 'a'
'a' :: Char

> val True
True :: Bool

Example equivalences to value:

val 0     =  value "0" 0
val 'a'   =  value "'a'" 'a'
val True  =  value "True" True

($$) :: Expr -> Expr -> Maybe Expr

O(n). Creates an Expr representing a function application. Just an Expr application if the types match, Nothing otherwise. (cf. :$)

> value "id" (id :: () -> ()) $$ val ()
Just (id () :: ())

> value "abs" (abs :: Int -> Int) $$ val (1337 :: Int)
Just (abs 1337 :: Int)

> value "abs" (abs :: Int -> Int) $$ val 'a'
Nothing

> value "abs" (abs :: Int -> Int) $$ val ()
Nothing

var :: Typeable a => String -> a -> Expr

O(1). Creates an Expr representing a variable with the given name and argument type.

> var "x" (undefined :: Int)
x :: Int

> var "u" (undefined :: ())
u :: ()

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

This function follows the underscore convention: a variable is just a value whose string representation starts with underscore ('_').

etyp :: Expr -> Either (TypeRep, TypeRep) TypeRep

O(n). Computes the type of an expression returning either the type of the given expression when possible or when there is a type error, the pair of types which produced the error.

> let one = val (1 :: Int)
> let bee = val 'b'
> let absE = value "abs" (abs :: Int -> Int)

> etyp one
Right Int

> etyp bee
Right Char

> etyp absE
Right (Int -> Int)

> etyp (absE :$ one)
Right Int

> etyp (absE :$ bee)
Left (Int -> Int, Char)

> etyp ((absE :$ bee) :$ one)
Left (Int -> Int, Char)

mtyp :: Expr -> Maybe TypeRep

O(n). Returns Just the type of an expression or Nothing when there is an error.

> let one = val (1 :: Int)
> let bee = val 'b'
> let absE = value "abs" (abs :: Int -> Int)

> mtyp one
Just Int

> mtyp (absE :$ bee)
Nothing

isIllTyped :: Expr -> Bool

O(n). Returns whether the given Expr is ill typed. (cf. isWellTyped)

> let one = val (1 :: Int)
> let bee = val 'b'
> let absE = value "abs" (abs :: Int -> Int)

> isIllTyped (absE :$ val (1 :: Int))
False

> isIllTyped (absE :$ val 'b')
True

isWellTyped :: Expr -> Bool

O(n). Returns whether the given Expr is well typed. (cf. isIllTyped)

> isWellTyped (absE :$ val (1 :: Int))
True

> isWellTyped (absE :$ val 'b')
False

isFun :: Expr -> Bool

O(n). Returns whether the given Expr is of a functional type. This is the same as checking if the arity of the given Expr is non-zero.

> isFun (value "abs" (abs :: Int -> Int))
True

> isFun (val (1::Int))
False

> isFun (value "const" (const :: Bool -> Bool -> Bool) :$ val False)
True

eval :: Typeable a => a -> Expr -> a

O(n). Evaluates an expression when possible (correct type). Returns a default value otherwise.

> let two = val (2 :: Int)
> let three = val (3 :: Int)
> let e1 -+- e2 = value "+" ((+) :: Int->Int->Int) :$ e1 :$ e2

> eval 0 $ two -+- three :: Int
5

> eval 'z' $ two -+- three :: Char
'z'

> eval 0 $ two -+- val '3' :: Int
0

evl :: Typeable a => Expr -> a

O(n). Evaluates an expression when possible (correct type). Raises an error otherwise.

> evl $ two -+- three :: Int
5

> evl $ two -+- three :: Bool
*** Exception: evl: cannot evaluate Expr `2 + 3 :: Int' at the Bool type

This may raise errors, please consider using eval or evaluate.

toDynamic :: Expr -> Maybe Dynamic

O(n). Evaluates an expression to a terminal Dynamic value when possible. Returns Nothing otherwise.

> toDynamic $ val (123 :: Int) :: Maybe Dynamic
Just <<Int>>

> toDynamic $ value "abs" (abs :: Int -> Int) :$ val (-1 :: Int)
Just <<Int>>

> toDynamic $ value "abs" (abs :: Int -> Int) :$ val 'a'
Nothing

showOpExpr :: String -> Expr -> String

O(n). Like showPrecExpr but the precedence is taken from the given operator name.

> showOpExpr "*" (two -*- three)
"(2 * 3)"

> showOpExpr "+" (two -*- three)
"2 * 3"

To imply that the surrounding environment is a function application, use " " as the given operator.

> showOpExpr " " (two -*- three)
"(2 * 3)"

showPrecExpr :: Int -> Expr -> String

O(n). Like showExpr but allows specifying the surrounding precedence.

> showPrecExpr 6 (one -+- two)
"1 + 2"

> showPrecExpr 7 (one -+- two)
"(1 + 2)"

showExpr :: Expr -> String

O(n). Returns a string representation of an expression. Differently from show (:: Expr -> String) this function does not include the type in the output.

> putStrLn $ showExpr (one -+- two)
1 + 2

> putStrLn $ showExpr $ (pp -||- true) -&&- (qq -||- false)
(p || True) && (q || False)

compareComplexity :: Expr -> Expr -> Ordering

O(n). Compares the complexity of two Exprs. An expression e1 is strictly simpler than another expression e2 if the first of the following conditions to distingish between them is:

1. e1 is smaller in size/length than e2, e.g.: x + y < x + (y + z);
2. or, e1 has more distinct variables than e2, e.g.: x + y < x + x;
3. or, e1 has more variable occurrences than e2, e.g.: x + x < 1 + x;
4. or, e1 has fewer distinct constants than e2, e.g.: 1 + 1 < 0 + 1.

They're otherwise considered of equal complexity, e.g.: x + y and y + z.

> (xx -+- yy) `compareComplexity` (xx -+- (yy -+- zz))
LT

> (xx -+- yy) `compareComplexity` (xx -+- xx)
LT

> (xx -+- xx) `compareComplexity` (one -+- xx)
LT

> (one -+- one) `compareComplexity` (zero -+- one)
LT

> (xx -+- yy) `compareComplexity` (yy -+- zz)
EQ

> (zero -+- one) `compareComplexity` (one -+- zero)
EQ

This comparison is not a total order.

compareLexicographically :: Expr -> Expr -> Ordering

O(n). Lexicographical structural comparison of Exprs where variables < constants < applications then types are compared before string representations.

> compareLexicographically one (one -+- one)
LT
> compareLexicographically one zero
GT
> compareLexicographically (xx -+- zero) (zero -+- xx)
LT
> compareLexicographically (zero -+- xx) (zero -+- xx)
EQ

(cf. compareTy)

This comparison is a total order.

compareQuickly :: Expr -> Expr -> Ordering

O(n). A fast total order between Exprs that can be used when sorting Expr values.

This is lazier than its counterparts compareComplexity and compareLexicographically and tries to evaluate the given Exprs as least as possible.

unfoldApp :: Expr -> [Expr]

O(n). Unfold a function application Expr into a list of function and arguments.

unfoldApp $ e0                    =  [e0]
unfoldApp $ e0 :$ e1              =  [e0,e1]
unfoldApp $ e0 :$ e1 :$ e2        =  [e0,e1,e2]
unfoldApp $ e0 :$ e1 :$ e2 :$ e3  =  [e0,e1,e2,e3]

Remember :$ is left-associative, so:

unfoldApp e0                          =  [e0]
unfoldApp (e0 :$ e1)                  =  [e0,e1]
unfoldApp ((e0 :$ e1) :$ e2)          =  [e0,e1,e2]
unfoldApp (((e0 :$ e1) :$ e2) :$ e3)  =  [e0,e1,e2,e3]

hasVar :: Expr -> Bool

O(n). Check if an Expr has a variable. (By convention, any value whose String representation starts with '_'.)

> hasVar $ value "not" not :$ val True
False

> hasVar $ value "&&" (&&) :$ var "p" (undefined :: Bool) :$ val True
True

isGround :: Expr -> Bool

O(n). Returns whether a Expr has no variables. This is equivalent to "not . hasVar".

The name "ground" comes from term rewriting.

> isGround $ value "not" not :$ val True
True

> isGround $ value "&&" (&&) :$ var "p" (undefined :: Bool) :$ val True
False

isConst :: Expr -> Bool

O(1). Returns whether an Expr is a terminal constant. (cf. isGround).

> isConst $ var "x" (undefined :: Int)
False

> isConst $ val False
True

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

isVar :: Expr -> Bool

O(1). Returns whether an Expr is a terminal variable (var). (cf. hasVar).

> isVar $ var "x" (undefined :: Int)
True

> isVar $ val False
False

> isVar $ value "not" not :$ var "p" (undefined :: Bool)
False

isValue :: Expr -> Bool

O(1). Returns whether an Expr is a terminal value (Value).

> isValue $ var "x" (undefined :: Int)
True

> isValue $ val False
True

> isValue $ value "not" not :$ var "p" (undefined :: Bool)
False

This is equivalent to pattern matching the Value constructor.

Properties:

•  isValue (Value e)  =  True

•  isValue (e1 :$ e2)  =  False

•  isValue  =  not . isApp

•  isValue e  =  isVar e || isConst e

isApp :: Expr -> Bool

O(1). Returns whether an Expr is an application (:$).

> isApp $ var "x" (undefined :: Int)
False

> isApp $ val False
False

> isApp $ value "not" not :$ var "p" (undefined :: Bool)
True

This is equivalent to pattern matching the :$ constructor.

Properties:

•  isApp (e1 :$ e2)  =  True

•  isApp (Value e)  =  False

•  isApp  =  not . isValue

•  isApp e  =  not (isVar e) && not (isConst e)

subexprs :: Expr -> [Expr]

O(n) for the spine, O(n^2) for full evaluation. Lists subexpressions of a given expression in order and with repetitions. This includes the expression itself and partial function applications. (cf. nubSubexprs)

> subexprs (xx -+- yy)
[ x + y :: Int
, (x +) :: Int -> Int
, (+) :: Int -> Int -> Int
, x :: Int
, y :: Int
]

> subexprs (pp -&&- (pp -&&- true))
[ p && (p && True) :: Bool
, (p &&) :: Bool -> Bool
, (&&) :: Bool -> Bool -> Bool
, p :: Bool
, p && True :: Bool
, (p &&) :: Bool -> Bool
, (&&) :: Bool -> Bool -> Bool
, p :: Bool
, True :: Bool
]

nubSubexprs :: Expr -> [Expr]

O(n^3) for full evaluation. Lists all subexpressions of a given expression without repetitions. This includes the expression itself and partial function applications. (cf. subexprs)

> nubSubexprs (xx -+- yy)
[ x :: Int
, y :: Int
, (+) :: Int -> Int -> Int
, (x +) :: Int -> Int
, x + y :: Int
]

> nubSubexprs (pp -&&- (pp -&&- true))
[ p :: Bool
, True :: Bool
, (&&) :: Bool -> Bool -> Bool
, (p &&) :: Bool -> Bool
, p && True :: Bool
, p && (p && True) :: Bool
]

Runtime averages to O(n^2 log n) on evenly distributed expressions such as (f x + g y) + (h z + f w); and to O(n^3) on deep expressions such as f (g (h (f (g (h x))))).

values :: Expr -> [Expr]

O(n). Lists all terminal values in an expression in order and with repetitions. (cf. nubValues)

> values (xx -+- yy)
[ (+) :: Int -> Int -> Int
, x :: Int
, y :: Int
]

> values (xx -+- (yy -+- zz))
[ (+) :: Int -> Int -> Int
, x :: Int
, (+) :: Int -> Int -> Int
, y :: Int
, z :: Int
]

> values (zero -+- (one -*- two))
[ (+) :: Int -> Int -> Int
, 0 :: Int
, (*) :: Int -> Int -> Int
, 1 :: Int
, 2 :: Int
]

> values (pp -&&- true)
[ (&&) :: Bool -> Bool -> Bool
, p :: Bool
, True :: Bool
]

nubValues :: Expr -> [Expr]

O(n^2). Lists all terminal values in an expression without repetitions. (cf. values)

> nubValues (xx -+- yy)
[ x :: Int
, y :: Int
, (+) :: Int -> Int -> Int

]

> nubValues (xx -+- (yy -+- zz))
[ x :: Int
, y :: Int
, z :: Int
, (+) :: Int -> Int -> Int
]

> nubValues (zero -+- (one -*- two))
[ 0 :: Int
, 1 :: Int
, 2 :: Int
, (*) :: Int -> Int -> Int
, (+) :: Int -> Int -> Int
]

> nubValues (pp -&&- pp)
[ p :: Bool
, (&&) :: Bool -> Bool -> Bool
]

Runtime averages to O(n log n) on evenly distributed expressions such as (f x + g y) + (h z + f w); and to O(n^2) on deep expressions such as f (g (h (f (g (h x))))).

consts :: Expr -> [Expr]

O(n). List terminal constants in an expression in order and with repetitions. (cf. nubConsts)

> consts (xx -+- yy)
[ (+) :: Int -> Int -> Int ]

> consts (xx -+- (yy -+- zz))
[ (+) :: Int -> Int -> Int
, (+) :: Int -> Int -> Int
]

> consts (zero -+- (one -*- two))
[ (+) :: Int -> Int -> Int
, 0 :: Int
, (*) :: Int -> Int -> Int
, 1 :: Int
, 2 :: Int
]

> consts (pp -&&- true)
[ (&&) :: Bool -> Bool -> Bool
, True :: Bool
]

nubConsts :: Expr -> [Expr]

O(n^2). List terminal constants in an expression without repetitions. (cf. consts)

> nubConsts (xx -+- yy)
[ (+) :: Int -> Int -> Int ]

> nubConsts (xx -+- (yy -+- zz))
[ (+) :: Int -> Int -> Int ]

> nubConsts (pp -&&- true)
[ True :: Bool
, (&&) :: Bool -> Bool -> Bool
]

Runtime averages to O(n log n) on evenly distributed expressions such as (f x + g y) + (h z + f w); and to O(n^2) on deep expressions such as f (g (h (f (g (h x))))).

vars :: Expr -> [Expr]

O(n). Lists all variables in an expression in order and with repetitions. (cf. nubVars)

> vars (xx -+- yy)
[ x :: Int
, y :: Int
]

> vars (xx -+- (yy -+- xx))
[ x :: Int
, y :: Int
, x :: Int
]

> vars (zero -+- (one -*- two))
[]

> vars (pp -&&- true)
[p :: Bool]

nubVars :: Expr -> [Expr]

O(n^2). Lists all variables in an expression without repetitions. (cf. vars)

> nubVars (yy -+- xx)
[ x :: Int
, y :: Int
]

> nubVars (xx -+- (yy -+- xx))
[ x :: Int
, y :: Int
]

> nubVars (zero -+- (one -*- two))
[]

> nubVars (pp -&&- true)
[p :: Bool]

Runtime averages to O(n log n) on evenly distributed expressions such as (f x + g y) + (h z + f w); and to O(n^2) on deep expressions such as f (g (h (f (g (h x))))).

depth :: Expr -> Int

O(n). Returns the maximum depth of a given expression given by the maximum number of nested function applications. Curried function application is counted only once, i.e. the application of a two argument function increases the depth of both its arguments by one. (cf. height)

With

zero       =  val (0 :: Int)
one        =  val (1 :: Int)
two        =  val (2 :: Int)
xx -+- yy  =  value "+" ((+) :: Int->Int->Int) :$ xx :$ yy
abs' xx    =  value "abs" (abs :: Int->Int) :$ xx

> depth zero
1

> depth (one -+- two)
2

> depth (abs' one -+- two)
3

Flipping arguments of applications in any of the subterms does not affect the result.

height :: Expr -> Int

O(n). Returns the maximum height of a given expression given by the maximum number of nested function applications. Curried function application is counted each time, i.e. the application of a two argument function increases the depth of its first argument by two and of its second argument by one. (cf. depth)

With:

zero          =  val (0 :: Int)
one           =  val (1 :: Int)
two           =  val (2 :: Int)
const' xx yy  =  value "const" (const :: Int->Int->Int) :$ xx :$ yy
abs' xx       =  value "abs" (abs :: Int->Int) :$ xx

Then:

> height zero
1

> height (abs' one)
2

> height ((const' one) two)
3

> height ((const' (abs' one)) two)
4

> height ((const' one) (abs' two))
3

Flipping arguments of applications in subterms may change the result of the function.

matchWith :: [(Expr, Expr)] -> Expr -> Expr -> Maybe [(Expr, Expr)]

Like match but allowing predefined bindings.

matchWith [(xx,zero)] (zero -+- one) (xx -+- yy)  =  Just [(xx,zero), (yy,one)]
matchWith [(xx,one)]  (zero -+- one) (xx -+- yy)  =  Nothing

encompasses :: Expr -> Expr -> Bool

Given two Exprs, checks if the first expression encompasses the second expression in terms of variables.

This is equivalent to flipping the arguments of isInstanceOf.

zero `encompasses` xx    =  False
  xx `encompasses` zero  =  True

hasInstanceOf :: Expr -> Expr -> Bool

Checks if any of the subexpressions of the first argument Expr is an instance of the second argument Expr.

isSubexprOf :: Expr -> Expr -> Bool

O(n^2). Checks if an Expr is a subexpression of another.

> (xx -+- yy) `isSubexprOf` (zz -+- (xx -+- yy))
True

> (xx -+- yy) `isSubexprOf` abs' (yy -+- xx)
False

> xx `isSubexprOf` yy
False

mapVars :: (Expr -> Expr) -> Expr -> Expr

O(n*m). Applies a function to all variables in an expression.

Given that:

> let primeify e = if isVar e
|                  then case e of (Value n d) -> Value (n ++ "'") d
|                  else e
> let xx = var "x" (undefined :: Int)
> let yy = var "y" (undefined :: Int)
> let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy

Then:

> xx -+- yy
x + y :: Int

> primeify xx
x' :: Int

> mapVars primeify $ xx -+- yy
x' + y' :: Int

> mapVars (primeify . primeify) $ xx -+- yy
x'' + y'' :: Int

Given that the argument function is O(m), this function is O(n*m).

mapConsts :: (Expr -> Expr) -> Expr -> Expr

O(n*m). Applies a function to all terminal constants in an expression.

Given that:

> let one   = val (1 :: Int)
> let two   = val (2 :: Int)
> let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy
> let intToZero e = if typ e == typ zero then zero else e

Then:

> one -+- (two -+- xx)
1 + (2 + x) :: Int

> mapConsts intToZero (one -+- (two -+- xx))
0 + (0 + x) :: Integer

Given that the argument function is O(m), this function is O(n*m).

mapSubexprs :: (Expr -> Maybe Expr) -> Expr -> Expr

O(n*m). Substitute subexpressions of an expression using the given function. Outer expressions have more precedence than inner expressions. (cf. //)

With:

> let xx = var "x" (undefined :: Int)
> let yy = var "y" (undefined :: Int)
> let zz = var "z" (undefined :: Int)
> let plus = value "+" ((+) :: Int->Int->Int)
> let times = value "*" ((*) :: Int->Int->Int)
> let xx -+- yy = plus :$ xx :$ yy
> let xx -*- yy = times :$ xx :$ yy

> let pluswap (o :$ xx :$ yy) | o == plus = Just $ o :$ yy :$ xx
|     pluswap _                           = Nothing

Then:

> mapSubexprs pluswap $ (xx -*- yy) -+- (yy -*- zz)
y * z + x * y :: Int

> mapSubexprs pluswap $ (xx -+- yy) -*- (yy -+- zz)
(y + x) * (z + y) :: Int

Substitutions do not stack, in other words a replaced expression or its subexpressions are not further replaced:

> mapSubexprs pluswap $ (xx -+- yy) -+- (yy -+- zz)
(y + z) + (x + y) :: Int

Given that the argument function is O(m), this function is O(n*m).

(//-) :: Expr -> [(Expr, Expr)] -> Expr

O(n*m). Substitute occurrences of values in an expression from the given list of substitutions. (cf. mapValues)

Given that:

> let xx = var "x" (undefined :: Int)
> let yy = var "y" (undefined :: Int)
> let zz = var "z" (undefined :: Int)
> let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy

Then:

> ((xx -+- yy) -+- (yy -+- zz)) //- [(xx, yy), (zz, yy)]
(y + y) + (y + y) :: Int

> ((xx -+- yy) -+- (yy -+- zz)) //- [(yy, yy -+- zz)]
(x + (y + z)) + ((y + z) + z) :: Int

This function does not work for substituting non-terminal subexpressions:

> (xx -+- yy) //- [(xx -+- yy, zz)]
x + y :: Int

Please use the slower // if you want the above replacement to work.

Replacement happens only once:

> xx //- [(xx,yy), (yy,zz)]
y :: Int

Given that the argument list has length m, this function is O(n*m).

renameVarsBy :: (String -> String) -> Expr -> Expr

Rename variables in an Expr.

> renameVarsBy (++ "'") (xx -+- yy)
x' + y' :: Int

> renameVarsBy (++ "'") (yy -+- (zz -+- xx))
(y' + (z' + x')) :: Int

> renameVarsBy (++ "1") (abs' xx)
abs x1 :: Int

> renameVarsBy (++ "2") $ abs' (xx -+- yy)
abs (x2 + y2) :: Int

NOTE: this will affect holes!

varAsTypeOf :: String -> Expr -> Expr

O(1). Creates a variable with the same type as the given Expr.

> let one = val (1::Int)
> "x" `varAsTypeOf` one
x :: Int

> "p" `varAsTypeOf` val False
p :: Bool

holeAsTypeOf :: Expr -> Expr

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

> val (1::Int)
1 :: Int
> holeAsTypeOf $ val (1::Int)
_ :: Int

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

isHole :: Expr -> Bool

O(1). Checks if an Expr represents a typed hole. (cf. hole)

> isHole $ hole (undefined :: Int)
True

> isHole $ value "not" not :$ val True
False

> isHole $ val 'a'
False

holes :: Expr -> [Expr]

O(n). Lists all holes in an expression, in order and with repetitions. (cf. nubHoles)

> holes $ hole (undefined :: Bool)
[_ :: Bool]

> holes $ value "&&" (&&) :$ hole (undefined :: Bool) :$ hole (undefined :: Bool)
[_ :: Bool,_ :: Bool]

> holes $ hole (undefined :: Bool->Bool) :$ hole (undefined::Bool)
[_ :: Bool -> Bool,_ :: Bool]

nubHoles :: Expr -> [Expr]

O(n^2). Lists all holes in an expression without repetitions. (cf. holes)

> nubHoles $ hole (undefined :: Bool)
[_ :: Bool]

> nubHoles $ value "&&" (&&) :$ hole (undefined :: Bool) :$ hole (undefined :: Bool)
[_ :: Bool]

> nubHoles $ hole (undefined :: Bool->Bool) :$ hole (undefined::Bool)
[_ :: Bool,_ :: Bool -> Bool]

Runtime averages to O(n log n) on evenly distributed expressions such as (f x + g y) + (h z + f w); and to O(n^2) on deep expressions such as f (g (h (f (g (h x))))).

hasHole :: Expr -> Bool

O(n). Returns whether an expression contains a hole

> hasHole $ hole (undefined :: Bool)
True

> hasHole $ value "not" not :$ val True
False

> hasHole $ value "not" not :$ hole (undefined :: Bool)
True

isComplete :: Expr -> Bool

O(n). Returns whether an expression is complete. A complete expression is one without holes.

> isComplete $ hole (undefined :: Bool)
False

> isComplete $ value "not" not :$ val True
True

> isComplete $ value "not" not :$ hole (undefined :: Bool)
False

isComplete is the negation of hasHole.

isComplete  =  not . hasHole

isComplete is to hasHole what isGround is to hasVar.

listVars :: Typeable a => String -> a -> [Expr]

Generate an infinite list of variables based on a template and a given type. (cf. listVarsAsTypeOf)

> putL 10 $ listVars "x" (undefined :: Int)
[ x :: Int
, y :: Int
, z :: Int
, x' :: Int
, y' :: Int
, z' :: Int
, x'' :: Int
, ...
]

> putL 10 $ listVars "p" (undefined :: Bool)
[ p :: Bool
, q :: Bool
, r :: Bool
, p' :: Bool
, q' :: Bool
, r' :: Bool
, p'' :: Bool
, ...
]

listVarsAsTypeOf :: String -> Expr -> [Expr]

Generate an infinite list of variables based on a template and the type of a given Expr. (cf. listVars)

> let one = val (1::Int)
> putL 10 $ "x" `listVarsAsTypeOf` one
[ x :: Int
, y :: Int
, z :: Int
, x' :: Int
, ...
]

> let false = val False
> putL 10 $ "p" `listVarsAsTypeOf` false
[ p :: Bool
, q :: Bool
, r :: Bool
, p' :: Bool
, ...
]

foldApp :: [Expr] -> Expr

O(n). Folds a list of Expr with function application (:$). This reverses the effect of unfoldApp.

foldApp [e0]           =  e0
foldApp [e0,e1]        =  e0 :$ e1
foldApp [e0,e1,e2]     =  e0 :$ e1 :$ e2
foldApp [e0,e1,e2,e3]  =  e0 :$ e1 :$ e2 :$ e3

Remember :$ is left-associative, so:

foldApp [e0]           =    e0
foldApp [e0,e1]        =   (e0 :$ e1)
foldApp [e0,e1,e2]     =  ((e0 :$ e1) :$ e2)
foldApp [e0,e1,e2,e3]  = (((e0 :$ e1) :$ e2) :$ e3)

This function may produce an ill-typed expression.

foldPair :: (Expr, Expr) -> Expr

O(1). Folds a pair of Expr values into a single Expr. (cf. unfoldPair)

This always generates an ill-typed expression, as it uses a fake pair constructor.

> foldPair (val False, val (1::Int))
(False,1) :: ill-typed # ExprPair $ Bool #

> foldPair (val (0::Int), val True)
(0,True) :: ill-typed # ExprPair $ Int #

This is useful when applying transformations on pairs of Exprs, such as canonicalize, mapValues or canonicalVariations.

> let ii = var "i" (undefined::Int)
> let kk = var "k" (undefined::Int)
> unfoldPair $ canonicalize $ foldPair (ii,kk)
(x :: Int,y :: Int)

unfoldPair :: Expr -> (Expr, Expr)

O(1). Unfolds an Expr representing a pair. This reverses the effect of foldPair.

> value "," ((,) :: Bool->Bool->(Bool,Bool)) :$ val True :$ val False
(True,False) :: (Bool,Bool)
> unfoldPair $ value "," ((,) :: Bool->Bool->(Bool,Bool)) :$ val True :$ val False
(True :: Bool,False :: Bool)

foldTrio :: (Expr, Expr, Expr) -> Expr

O(1). Folds a trio/triple of Expr values into a single Expr. (cf. unfoldTrio)

This always generates an ill-typed expression as it uses a fake trio/triple constructor.

> foldTrio (val False, val (1::Int), val 'a')
(False,1,'a') :: ill-typed # ExprTrio $ Bool #

> foldTrio (val (0::Int), val True, val 'b')
(0,True,'b') :: ill-typed # ExprTrio $ Int #

This is useful when applying transformations on pairs of Exprs, such as canonicalize, mapValues or canonicalVariations.

> let ii = var "i" (undefined::Int)
> let kk = var "k" (undefined::Int)
> let zz = var "z" (undefined::Int)
> unfoldPair $ canonicalize $ foldPair (ii,kk,zz)
(x :: Int,y :: Int,z :: Int)

unfoldTrio :: Expr -> (Expr, Expr, Expr)

O(1). Unfolds an Expr representing a trio/triple. This reverses the effect of foldTrio.

> value ",," ((,,) :: Bool->Bool->Bool->(Bool,Bool,Bool)) :$ val True :$ val False :$ val True
(True,False,True) :: (Bool,Bool,Bool)
> unfoldTrio $ value ",," ((,,) :: Bool->Bool->Bool->(Bool,Bool,Bool)) :$ val True :$ val False :$ val True
(True :: Bool,False :: Bool,True :: Bool)

(cf. unfoldPair)

deriveExpressIfNeeded :: Name -> DecsQ

Same as deriveExpress but does not warn when instance already exists (deriveExpress is preferable).

deriveExpressCascading :: Name -> DecsQ

Derives a Express instance for a given type Name cascading derivation of type arguments as well.

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

Lists valid applications between a list of Exprs and an Expr.

> [plus, times] >$$ zero
[(0 +) :: Int -> Int,(0 *) :: Int -> Int]

($$<) :: Expr -> [Expr] -> [Expr]

Lists valid applications between an Expr and a list of Exprs.

> notE >$$< [false, true, zero]
[not False :: Bool,not True :: Bool]

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.

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)

mkName :: Typeable a => (a -> String) -> [Expr]

O(1). Builds a reified Name instance from the given name function. (cf. reifyName, mkNameWith)

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

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

lookupComparison :: String -> TypeRep -> [Expr] -> Maybe Expr

O(n). Lookups for a comparison function (:: a -> a -> Bool) with the given name and argument type.

isEqT :: [Expr] -> TypeRep -> Bool

O(n). Returns whether an Eq instance exists in the given instances list for the given TypeRep.

> isEqT (reifyEqOrd (undefined :: Int)) (typeOf (undefined :: Int))
True

> isEqT (reifyEqOrd (undefined :: Int)) (typeOf (undefined :: [[[Int]]]))
False

Given that the instances list has length n, this function is O(n).

isOrdT :: [Expr] -> TypeRep -> Bool

O(n). Returns whether an Ord instance exists in the given instances list for the given TypeRep.

> isOrdT (reifyEqOrd (undefined :: Int)) (typeOf (undefined :: Int))
True

> isOrdT (reifyEqOrd (undefined :: Int)) (typeOf (undefined :: [[[Int]]]))
False

Given that the instances list has length n, this function is O(n).

isEqOrdT :: [Expr] -> TypeRep -> Bool

O(n). Returns whether both Eq and Ord instance exist in the given list for the given TypeRep.

Given that the instances list has length n, this function is O(n).

isEq :: [Expr] -> Expr -> Bool

O(n+m). Returns whether an Eq instance exists in the given instances list for the given Expr.

> isEq (reifyEqOrd (undefined :: Int)) (val (0::Int))
True

> isEq (reifyEqOrd (undefined :: Int)) (val ([[[0::Int]]]))
False

Given that the instances list has length m and that the given Expr has size n, this function is O(n+m).

isOrd :: [Expr] -> Expr -> Bool

O(n+m). Returns whether an Ord instance exists in the given instances list for the given Expr.

> isOrd (reifyEqOrd (undefined :: Int)) (val (0::Int))
True

> isOrd (reifyEqOrd (undefined :: Int)) (val ([[[0::Int]]]))
False

Given that the instances list has length m and that the given Expr has size n, this function is O(n+m).

isEqOrd :: [Expr] -> Expr -> Bool

O(n+m). Returns whether both Eq and Ord instance exist in the given list for the given Expr.

Given that the instances list has length m and that the given Expr has size n, this function is O(n+m).

mkComparison :: String -> [Expr] -> Expr -> Expr -> Expr

O(n+m). Like mkEquation, mkComparisonLE and mkComparisonLT but allows providing the binary operator name.

When not possible, this function returns False encoded as an Expr.

mkEquation :: [Expr] -> Expr -> Expr -> Expr

O(n+m). Returns an equation between two expressions given that it is possible to do so from == operators given in the argument instances list.

When not possible, this function returns False encoded as an Expr.

mkComparisonLT :: [Expr] -> Expr -> Expr -> Expr

O(n+m). Returns a less-than inequation between two expressions given that it is possible to do so from < operators given in the argument instances list.

When not possible, this function returns False encoded as an Expr.

mkComparisonLE :: [Expr] -> Expr -> Expr -> Expr

O(n+m). Returns a less-than-or-equal-to inequation between two expressions given that it is possible to do so from <= operators given in the argument instances list.

When not possible, this function returns False encoded as an Expr.

lookupName :: [Expr] -> Expr -> String

O(n+m). Like name but lifted over an instance list and an Expr.

> lookupName preludeNameInstances (val False)
"p"

> lookupName preludeNameInstances (val (0::Int))
"x"

This function defaults to "x" when no appropriate name is found.

> lookupName [] (val False)
"x"

lookupNames :: [Expr] -> Expr -> [String]

O(n+m). A mix between lookupName and names: this returns an infinite list of names based on an instances list and an Expr.

listVarsWith :: [Expr] -> Expr -> [Expr]

O(n+m). Like lookupNames but returns a list of variables encoded as Exprs.

validApps :: [Expr] -> Expr -> [Expr]

Given a list of functional expressions and another expression, returns a list of valid applications.

findValidApp :: [Expr] -> Expr -> Maybe Expr

Like validApps but returns a Maybe value.

preludeNameInstances :: [Expr]

A list of reified Name instances for an arbitrary selection of types from the Haskell Prelude.

canonicalizeWith :: (Expr -> [String]) -> Expr -> Expr

Like canonicalize but allows customization of the list of variable names. (cf. lookupNames, variableNamesFromTemplate)

> canonicalizeWith (const ["i","j","k","l",...]) (xx -+- yy)
i + j :: Int

The argument Expr of the argument function allows to provide a different list of names for different types:

> let namesFor e
>   | typ e == typeOf (undefined::Char) = variableNamesFromTemplate "c1"
>   | typ e == typeOf (undefined::Int)  = variableNamesFromTemplate "i"
>   | otherwise                         = variableNamesFromTemplate "x"

> canonicalizeWith namesFor ((xx -+- ord' dd) -+- (ord' cc -+- yy))
(i + ord c1) + (ord c2 + j) :: Int

canonicalizationWith :: (Expr -> [String]) -> Expr -> [(Expr, Expr)]

Like canonicalization but allows customization of the list of variable names. (cf. lookupNames, variableNamesFromTemplate)

isCanonicalWith :: (Expr -> [String]) -> Expr -> Bool

Like isCanonical but allows specifying the list of variable names.

canonicalization :: Expr -> [(Expr, Expr)]

Return a canonicalization of an Expr that makes variable names appear in order using names as provided by preludeNameInstances. By using //- it can canonicalize Exprs.

> canonicalization (gg yy -+- ff xx -+- gg xx)
[ (x :: Int,        y :: Int)
, (f :: Int -> Int, g :: Int -> Int)
, (y :: Int,        x :: Int)
, (g :: Int -> Int, f :: Int -> Int) ]

> canonicalization (yy -+- xx -+- yy)
[ (x :: Int, y :: Int)
, (y :: Int, x :: Int) ]

isCanonical :: Expr -> Bool

Returns whether an Expr is canonical: if applying canonicalize is an identity using names as provided by preludeNameInstances.

mostGeneralCanonicalVariation :: Expr -> Expr

Returns the most general canonical variation of an Expr by filling holes with variables.

> mostGeneralCanonicalVariation $ i_
x :: Int

> mostGeneralCanonicalVariation $ i_ -+- i_
x + y :: Int

> mostGeneralCanonicalVariation $ i_ -+- i_ -+- i_
(x + y) + z :: Int

> mostGeneralCanonicalVariation $ i_ -+- ord' c_
x + ord c :: Int

> mostGeneralCanonicalVariation $ i_ -+- i_ -+- ord' c_
(x + y) + ord c :: Int

> mostGeneralCanonicalVariation $ i_ -+- i_ -+- length' (c_ -:- unit c_)
(x + y) + length (c:d:"") :: Int

In an expression without holes this functions just returns the given expression itself:

> mostGeneralCanonicalVariation $ val (0 :: Int)
0 :: Int

> mostGeneralCanonicalVariation $ ord' bee
ord 'b' :: Int

This function is the same as taking the head of canonicalVariations but a bit faster.

mostSpecificCanonicalVariation :: Expr -> Expr

Returns the most specific canonical variation of an Expr by filling holes with variables.

> mostSpecificCanonicalVariation $ i_
x :: Int

> mostSpecificCanonicalVariation $ i_ -+- i_
x + x :: Int

> mostSpecificCanonicalVariation $ i_ -+- i_ -+- i_
(x + x) + x :: Int

> mostSpecificCanonicalVariation $ i_ -+- ord' c_
x + ord c :: Int

> mostSpecificCanonicalVariation $ i_ -+- i_ -+- ord' c_
(x + x) + ord c :: Int

> mostSpecificCanonicalVariation $ i_ -+- i_ -+- length' (c_ -:- unit c_)
(x + x) + length (c:c:"") :: Int

In an expression without holes this functions just returns the given expression itself:

> mostSpecificCanonicalVariation $ val (0 :: Int)
0 :: Int

> mostSpecificCanonicalVariation $ ord' bee
ord 'b' :: Int

This function is the same as taking the last of canonicalVariations but a bit faster.

fastCanonicalVariations :: Expr -> [Expr]

A faster version of canonicalVariations that disregards name clashes across different types. Results are confusing to the user but fine for Express which differentiates between variables with the same name but different types.

Without applying canonicalize, the following Expr may seem to have only one variable:

> fastCanonicalVariations $ i_ -+- ord' c_
[x + ord x :: Int]

Where in fact it has two, as the second x has a different type. Applying canonicalize disambiguates:

> map canonicalize . fastCanonicalVariations $ i_ -+- ord' c_
[x + ord c :: Int]

This function is useful when resulting Exprs are not intended to be presented to the user but instead to be used by another function. It is simply faster to skip the step where clashes are resolved.

fastMostGeneralVariation :: Expr -> Expr

A faster version of mostGeneralCanonicalVariation that disregards name clashes across different types. Consider using mostGeneralCanonicalVariation instead.

The same caveats of fastCanonicalVariations do apply here.

fastMostSpecificVariation :: Expr -> Expr

A faster version of mostSpecificCanonicalVariation that disregards name clashes across different types. Consider using mostSpecificCanonicalVariation instead.

The same caveats of fastCanonicalVariations do apply here.

b_ :: Expr

Expr representing a hole of Bool type.

> b_
_ :: Bool

pp :: Expr

Expr representing a variable p :: Bool.

> pp
p :: Bool

qq :: Expr

Expr representing a variable q :: Bool.

> qq
q :: Bool

rr :: Expr

Expr representing a variable r :: Bool.

> rr
r :: Bool

pp' :: Expr

Expr representing a variable p' :: Bool.

> pp'
p' :: Bool

false :: Expr

False encoded as an Expr.

> false
False :: Bool

true :: Expr

True encoded as an Expr.

> true
True :: Bool

notE :: Expr

The function not encoded as an Expr.

> notE
not :: Bool -> Bool

andE :: Expr

The function and encoded as an Expr.

> andE
(&&) :: Bool -> Bool -> Bool

orE :: Expr

The function or encoded as an Expr.

> orE
(||) :: Bool -> Bool -> Bool

(-==>-) :: Expr -> Expr -> Expr infixr 0

The function ==> lifted over Exprs.

> false -==>- true
False ==> True :: Bool

> evl $ false -==>- true :: Bool
True

implies :: Expr

The ==> operator encoded as an Expr

not' :: Expr -> Expr

The function not lifted over the Expr type.

> not' false
not False :: Bool

> evalBool $ not' false
True

> not' pp
not p :: Bool

(-&&-) :: Expr -> Expr -> Expr infixr 3

The function && lifted over the Expr type.

> pp -&&- qq
p && q :: Bool

> false -&&- true
False && True :: Bool

> evalBool $ false -&&- true
False

(-||-) :: Expr -> Expr -> Expr infixr 2

The function || lifted over the Expr type.

> pp -||- qq
p || q :: Bool

> false -||- true
False || True :: Bool

> evalBool $ false -||- true
True

i_ :: Expr

A typed hole of Int type.

> i_
_ :: Int

xx :: Expr

A variable x of Int type.

> xx
x :: Int

yy :: Expr

A variable y of Int type.

> yy
y :: Int

zz :: Expr

A variable z of Int type.

> zz
z :: Int

xx' :: Expr

A variable x' of Int type.

> xx'
x' :: Int

ii :: Expr

A variable i of Int type.

> ii
i :: Int

jj :: Expr

A variable j of Int type.

> jj
j :: Int

kk :: Expr

A variable k of Int type.

> kk
k :: Int

ii' :: Expr

A variable i' of Int type.

> ii'
i' :: Int

ll :: Expr

A variable l of Int type.

> ll
l :: Int

mm :: Expr

A variable m of Int type.

> mm
m :: Int

nn :: Expr

A variable n of Int type.

> nn
n :: Int

one :: Expr

The value 1 bound to the Int type encoded as an Expr.

> one
1 :: Int

two :: Expr

The value 2 bound to the Int type encoded as an Expr.

> two
2 :: Int

three :: Expr

The value 3 bound to the Int type encoded as an Expr.

> three
3 :: Int

four :: Expr

The value 4 bound to the Int type encoded as an Expr.

> four
4 :: Int

five :: Expr

The value 5 bound to the Int type encoded as an Expr.

> five
5 :: Int

six :: Expr

The value 6 bound to the Int type encoded as an Expr.

> six
6 :: Int

seven :: Expr

The value 7 bound to the Int type encoded as an Expr.

> seven
7 :: Int

eight :: Expr

The value 8 bound to the Int type encoded as an Expr.

> eight
8 :: Int

nine :: Expr

The value 9 bound to the Int type encoded as an Expr.

> nine
9 :: Int

ten :: Expr

The value 10 bound to the Int type encoded as an Expr.

> ten
10 :: Int

eleven :: Expr

The value 11 bound to the Int type encoded as an Expr.

> eleven
11 :: Int

twelve :: Expr

The value 12 bound to the Int type encoded as an Expr.

> twelve
12 :: Int

minusOne :: Expr

The value -1 bound to the Int type encoded as an Expr.

> minusOne
-1 :: Int

minusTwo :: Expr

The value -2 bound to the Int type encoded as an Expr.

> minusOne
-2 :: Int

ff :: Expr -> Expr

A variable function f of 'a -> a' type lifted over the Expr type. This works for Int, Bool, Char and their lists

> ff xx
f x :: Int

> ff one
f 1 :: Int

ffE :: Expr

A variable f of 'Int -> Int' type encoded as an Expr.

> ffE
f :: Int -> Int

gg :: Expr -> Expr

A variable function g of 'a -> a' type lifted over the Expr type. This works for Int, Bool, Char and their lists.

> gg yy
g y :: Int

> gg minusTwo
gg (-2) :: Int

ggE :: Expr

A variable g of 'Int -> Int' type encoded as an Expr.

> ggE
g :: Int -> Int

hh :: Expr -> Expr

A variable function h of 'Int -> Int' type lifted over the Expr type.

> hh zz
h z :: Int

hhE :: Expr

A variable h of 'Int -> Int' type encoded as an Expr.

> hhE
h :: Int -> Int

ff2 :: Expr -> Expr -> Expr

A variable function f of 'a -> a -> a' type lifted over the Expr type. This works for Int, Bool, Char and their lists

> ff2 xx yy
f x y :: Int

> ff2 one two
f 1 2 :: Int

The result type is bound to the type of the last argument.

ff3 :: Expr -> Expr -> Expr -> Expr

A variable function f of 'a -> a -> a -> a' type lifted over the Expr type. This works for Int, Bool, Char and their lists

> ff3 xx yy zz
f x y z :: Int

> ff3 one two three
f 1 2 3 :: Int

The result type is bound to the type of the last argument.

ff4 :: Expr -> Expr -> Expr -> Expr -> Expr

A variable function f of 'a -> a -> a -> a -> a' type lifted over the Expr type. This works for Int, Bool, Char and their lists

> ff3 xx yy zz xx'
f x y z xx' :: Int

> ff3 one two three four
f 1 2 3 4 :: Int

The result type is bound to the type of the last argument.

(-?-) :: Expr -> Expr -> Expr

A variable binary operator ? lifted over the Expr type. Works for Int, Bool, Char, [Int] and String.

> xx -?- yy
x ? y :: Int

> pp -?- qq
p ? q :: Bool

> xx -?- qq
*** Exception: (-?-): unhandled type: 1 :: Int, False :: Bool
    accepted types are:
    (?) :: Int -> Int -> Int
    (?) :: Bool -> Bool -> Bool
    (?) :: Char -> Char -> Char
    (?) :: [Int] -> [Int] -> [Int]
    (?) :: [Char] -> [Char] -> [Char]
    (?) :: Int -> [Int] -> [Int]
    (?) :: Char -> [Char] -> [Char]

question :: Expr

A variable binary operator ? encoded as an Expr (cf. -?-)

> question :$ xx :$ yy
x ? y :: Int

> question :$ pp :$ qq
p ? q :: Bool

oo :: Expr -> Expr -> Expr

A variable binary operator o lifted over the Expr type. Works for Int, Bool, Char, [Int] and String.

> xx `oo` yy
x `o` y :: Int

> pp `oo` qq
p `o` q :: Bool

> xx `oo` qq
*** Exception: oo: unhandled type: 1 :: Int, False :: Bool
    accepted types are:
    o :: Int -> Int -> Int
    o :: Bool -> Bool -> Bool
    o :: Char -> Char -> Char
    o :: [Int] -> [Int] -> [Int]
    o :: [Char] -> [Char] -> [Char]

ooE :: Expr

A variable binary function o encoded as an Expr (cf. oo)

> ooE :$ xx :$ yy
x `o` y :: Int

> ooE :$ pp :$ qq
p `o` q :: Bool

(-+-) :: Expr -> Expr -> Expr infixl 6

The operator + for the Int type for use on Exprs. (See also plus.)

> two -+- three
2 + 3 :: Int

> minusOne -+- minusTwo -+- zero
((-1) + (-2)) + 0 :: Int

> xx -+- (yy -+- zz)
x + (y + z) :: Int

plus :: Expr

The operator + for the Int type. (See also -+-.)

> plus
(+) :: Int -> Int -> Int

> plus :$ one
(1 +) :: Int -> Int

> plus :$ xx :$ yy
x + y :: Int

(-*-) :: Expr -> Expr -> Expr infixl 7

The operator * for the Int type lifted over the Expr type. (See also times.)

> three -*- three
3 * 3 :: Int

> one -*- two -*- three
(1 * 2) * 3 :: Int

> two -*- xx
2 * x :: Int

minus :: Expr

The subtraction - operator encoded as an Expr.

> minus :$ one
(1 -) :: Int -> Int

> minus :$ one :$ zero
1 - 0 :: Int

divE :: Expr

Integer division div encoded as an Expr.

> divE :$ two
(2 `div`) :: Int -> Int

> divE :$ two :$ three
2 `div` 3 :: Int

modE :: Expr

Integer modulo mod encoded as an Expr.

> modE :$ two
(2 `mod`) :: Int -> Int

> modE :$ two :$ three
2 `mod` 3 :: Int

quot' :: Expr -> Expr -> Expr

The function quot for the Int type lifted over the Expr type. (See also rem.)

> six `quot'` four
6 `quot` 4 :: Int

quotE :: Expr

Integer quotient quot encoded as an Expr.

> quotE :$ two
(2 `quot`) :: Int -> Int

> quotE :$ two :$ three
2 `quot` 3 :: Int

rem' :: Expr -> Expr -> Expr

The function rem for the Int type lifted over the Expr type. (See also quot.)

> six `rem'` four
6 `rem` 4 :: Int

remE :: Expr

Integer remainder rem encoded as an Expr.

> remE :$ two
(2 `rem`) :: Int -> Int

> remE :$ two :$ three
2 `rem` 3 :: Int

id' :: Expr -> Expr

Constructs an application of id as an Expr. Only works for Int, Bool, Char, String, [Int], [Bool].

> id' yy
id yy :: Int

> id' one
id 1 :: Int

> evl (id' one) :: Int
1

> id' pp
id p :: Bool

> id' false
id' False :: Bool

> evl (id' true) :: Bool
True :: Bool

idE :: Expr

The function id for the Int type encoded as an Expr. (See also id'.)

> idE :$ xx
id x :: Int

> idE :$ zero
id 0 :: Int

> evaluate $ idE :$ zero :: Maybe Int
Just 0

idInt :: Expr

The function id encoded as an Expr. (cf. id')

idBool :: Expr

The function id encoded as an Expr. (cf. id')

idChar :: Expr

The function id encoded as an Expr. (cf. id')

idInts :: Expr

The function id encoded as an Expr. (cf. id')

idBools :: Expr

The function id encoded as an Expr. (cf. id')

idString :: Expr

The function id encoded as an Expr. (cf. id')

const' :: Expr -> Expr -> Expr

The const function lifted over the Expr type.

> const' zero one
const 0 1 :: Int

This works for the argument types Int, Char, Bool and their lists.

negate' :: Expr -> Expr

negate over the Int type lifted over the Expr type.

> negate' xx
negate x :: Int

> evl (negate' one) :: Int
-1

negateE :: Expr

negate over the Int type encoded as an Expr

> negateE
negate :: Int -> Int

abs' :: Expr -> Expr

abs over the Int type lifted over the Expr type.

> abs' xx'
abs x' :: Int

> evl (abs' minusTwo) :: Int
2

absE :: Expr

abs over the Int type encoded as an Expr.

> absE
abs :: Int -> Int

signum' :: Expr -> Expr

signum over the Int type lifted over the Expr type.

> signum' xx'
signum x' :: Int

> evl (signum' minusTwo) :: Int
-1

signumE :: Expr

signum over the Int type encoded as an Expr.

> signumE
signum :: Int -> Int

odd' :: Expr -> Expr

odd with an Int argument lifted over the Expr type.

> odd' (xx -+- one)
odd (x + 1) :: Bool

> evl (odd' two) :: Bool
False

even' :: Expr -> Expr

even with an Int argument lifted over the Expr type.

> even' (xx -+- two)
even (x + 2) :: Bool

> evl (even' two) :: Bool
True

c_ :: Expr

A hole of Char type encoded as an Expr.

> c_
_ :: Char

cs_ :: Expr

A hole of String type encoded as an Expr.

> cs_
_ :: [Char]

cc :: Expr

A variable named c of type Char encoded as an Expr.

> cc
c :: Char

dd :: Expr

A variable named c of type Char encoded as an Expr.

> dd
d :: Char

ccs :: Expr

A variable named cs of type String encoded as an Expr.

> ccs
cs :: [Char]

ae :: Expr

The character 'a' encoded as an Expr.

> ae
'a' :: Char

> evl ae :: Char
'a'

bee :: Expr

The character 'b' encoded as an Expr

> bee
'b' :: Char

> evl bee :: Char
'b'

cee :: Expr

The character 'c' encoded as an Expr

> cee
'c' :: Char

> evl cee :: Char
'c'

dee :: Expr

The character 'd' encoded as an Expr

> dee
'd' :: Char

> evl dee :: Char
'd'

zed :: Expr

The character 'z' encoded as an Expr

> zed
'z' :: Char

> evl zed :: Char
'z'

(cf. zee)

zee :: Expr

The character 'z' encoded as an Expr

> zee
'z' :: Char

> evl zee :: Char
'z'

(cf. zed)

space :: Expr

The space character encoded as an Expr

> space
' ' :: Char

lineBreak :: Expr

The line break character encoded as an Expr

> lineBreak
'\n' :: Char

ord' :: Expr -> Expr

The ord function lifted over Expr

> ord' bee
ord 'b' :: Int

> evl (ord' bee)
98

ordE :: Expr

The ord function encoded as an Expr

is_ :: Expr

A typed hole of [Int] type encoded as an Expr.

> is_
_ :: [Int]

xxs :: Expr

A variable named xs of type [Int] encoded as an Expr.

> xxs
xs :: [Int]

yys :: Expr

A variable named ys of type [Int] encoded as an Expr.

> yys
ys :: [Int]

zzs :: Expr

A variable named zs of type [Int] encoded as an Expr.

> yys
ys :: [Int]

nil :: Expr

An empty list of type [Int] encoded as an Expr.

> nil
[] :: [Int]

emptyString :: Expr

An empty String encoded as an Expr.

> emptyString
"" :: String

nilInt :: Expr

The empty list '[]' encoded as an Expr.

nilBool :: Expr

The empty list '[]' encoded as an Expr.

nilChar :: Expr

The empty list '[]' encoded as an Expr.

consInt :: Expr

The list constructor : encoded as an Expr.

consBool :: Expr

The list constructor : encoded as an Expr.

consChar :: Expr

The list constructor : encoded as an Expr.

(-:-) :: Expr -> Expr -> Expr infixr 5

The list constructor lifted over the Expr type. Works for the element types Int, Char and Bool.

> zero -:- one -:- unit two
[0,1,2] :: [Int]

> zero -:- one -:- two -:- nil
[0,1,2] :: [Int]

> bee -:- unit cee
"bc" :: [Char]

appendInt :: Expr

Append for list of Ints encoded as an Expr.

(-++-) :: Expr -> Expr -> Expr infixr 5

List concatenation lifted over the Expr type. Works for the element types Int, Char and Bool.

> (zero -:- one -:- nil) -:- (two -:- three -:- nil)
[0,1] -++- [2,3] :: [Int]

> (bee -:- unit cee) -:- unit dee
"bc" -++- "c" :: [Char]

head' :: Expr -> Expr

List head lifted over the Expr type. Works for the element types Int, Char and Bool.

> head' $ unit one
head [1] :: Int

> head' $ unit bee
head "b" :: Char

> head' $ zero -:- unit two
head [0,2] :: Int

> evl $ head' $ unit one :: Int
1

tail' :: Expr -> Expr

List tail lifted over the Expr type. Works for the element types Int, Char and Bool.

> tail' $ unit one
tail [1] :: [Int]

> tail' $ unit bee
tail "b" :: [Char]

> tail' $ zero -:- unit two
tail [0,2] :: [Int]

> evl $ tail' $ zero -:- unit two :: [Int]
[2]

null' :: Expr -> Expr

List null lifted over the Expr type. Works for the element types Int, Char and Bool.

> null' $ unit one
null [1] :: Bool

> null' $ nil
null [] :: Bool

> evl $ null' nil :: Bool
True

length' :: Expr -> Expr

List length lifted over the Expr type. Works for the element types Int, Char and Bool.

> length' $ unit one
length [1] :: Int

> length' $ unit bee
length "b" :: Int

> length' $ zero -:- unit two
length [0,2] :: Int

> evl $ length' $ unit one :: Int
1

init' :: Expr -> Expr

List init lifted over the Expr type. Works for the element types Int, Char and Bool.

> init' $ unit one
init [1] :: [Int]

> init' $ unit bee
init "b" :: [Char]

> init' $ zero -:- unit two
init [0,2] :: [Int]

> evl $ init' $ zero -:- unit two :: [Int]
[0]

sort' :: Expr -> Expr

List sort lifted over the Expr type. Works for the element types Int, Char and Bool.

> sort' $ unit one
sort [1] :: Int

> sort' $ unit bee
sort "b" :: Int

> sort' $ zero -:- unit two
sort [0,2] :: Int

> evl $ sort' $ two -:- unit one :: [Int]
[1,2]

insert' :: Expr -> Expr -> Expr

List insert lifted over the Expr type. Works for the element types Int, Char and Bool.

> insert' zero nilInt
insert 0 [] :: [Int]

> insert' false (false -:- unit true)
insert False [False,True] :: [Bool]

elem' :: Expr -> Expr -> Expr

List elem lifted over the Expr type. Works for the element types Int, Char and Bool.

> elem' false (false -:- unit true)
elem False [False,True] :: Bool

> evl $ elem' false (false -:- unit true) :: Bool
True

drop' :: Expr -> Expr -> Expr

List drop lifted over the Expr type. Works for the element types Int, Char and Bool.

> drop' zero nilInt
drop 0 [] :: [Int]

> drop' one (false -:- unit true)
drop 1 [False,True] :: [Bool]

take' :: Expr -> Expr -> Expr

List take lifted over the Expr type. Works for the element types Int, Char and Bool.

> take' zero nilInt
take 0 [] :: [Int]

> take' one (false -:- unit true)
take 1 [False,True] :: [Bool]

(-$-) :: Expr -> Expr -> Expr infixl 6

$ lifted over Exprs

> absE -$- one
abs $ 1 :: Int

Works for Int, Bool, Char argument types and their lists.

(-/=-) :: Expr -> Expr -> Expr infix 4

Constructs an inequation between two Exprs.

> xx -/=- zero
x /= 0 :: Bool

> cc -/=- ae
c /= 'a' :: Bool

(-<=-) :: Expr -> Expr -> Expr infix 4

Constructs a less-than-or-equal inequation between two Exprs.

> xx -<=- zero
x <= 0 :: Bool

> cc -<=- ae
c <= 'a' :: Bool

(-<-) :: Expr -> Expr -> Expr infix 4

Constructs a less-than inequation between two Exprs.

> xx -<- zero
x < 0 :: Bool

> cc -<- bee
c < 'b' :: Bool

if' :: Expr -> Expr -> Expr -> Expr

A function if :: Bool -> a -> a -> a lifted over the Expr type that encodes if-then-else functionality. This is properly displayed as an if-then-else.

> if' pp zero xx
(if p then 0 else x) :: Int

> zz -*- if' pp xx yy
z * (if p then x else y) :: Int

> if' pp false true -||- if' qq true false
(if p then False else True) || (if q then True else False) :: Bool

> evl $ if' true (val 't') (val 'f') :: Char
't'

caseBool :: Expr -> Expr -> Expr -> Expr

A function case :: Bool -> a -> a -> a lifted over the Expr type that encodes case-of-False-True functionality. This is properly displayed as a case-of-False-True expression.

> caseBool pp zero xx
(case p of False -> 0; True -> x) :: Int

> zz -*- caseBool pp xx yy
z * (case p of False -> x; True -> y) :: Int

> caseBool pp false true -||- caseBool qq true false
(caseBool p of False -> False; True -> True) || (caseBool q of False -> True; True -> False) :: Bool

> evl $ caseBool true (val 'f') (val 't') :: Char
't'

By convention, the False case comes before True as False < True and data Bool = False | True.

When evaluating, this is equivalent to if with arguments reversed. Instead of using this, you are perhaps better of using if encoded as an expression. This is just here to be consistent with caseOrdering.

caseOrdering :: Expr -> Expr -> Expr -> Expr -> Expr

A function case :: Ordering -> a -> a -> a -> a lifted over the Expr type that encodes case-of-LT-EQ-GT functionality. This is properly displayed as a case-of-LT-EQ-GT expression. (cf. caseBool)

> caseOrdering (xx `compare'` yy) zero one two
(case compare x y of LT -> 0; EQ -> 1; GT -> 2) :: Int

> evl $ caseOrdering (val EQ) (val 'l') (val 'e') (val 'g') :: Char
'e'

By convention cases are given in LT, EQ and GT order as LT < EQ < GT and data Ordering = LT | EQ | GT.

compare' :: Expr -> Expr -> Expr

Constructs an Expr-encoded compare operation between two Exprs.

> xx `compare'` zero
compare x 0 :: Ordering

> compare' ae bee
compare 'a' 'b' :: Ordering

nothing :: Expr

Nothing bound to the Maybe Int type encoded as an Expr.

This is an alias to nothingInt.

nothingInt :: Expr

Nothing bound to the Maybe Int type encoded as an Expr.

nothingBool :: Expr

Nothing bound to the Maybe Bool type encoded as an Expr.

justInt :: Expr

The Just constructor of the Int element type encoded as an Expr.

justBool :: Expr

The Just constructor of the Bool element type encoded as an Expr.

just :: Expr -> Expr

The Just constructor lifted over the Expr type.

This works for the Bool, Int, Char argument types and their lists.

> just zero
Just 0 :: Maybe Int
> just false
Just False :: Maybe Bool

(-|-) :: Expr -> Expr -> Expr

An infix synonym of pair.

> zero -|- xxs

(0,xs) :: (Int,[Int])

> ae -|- (bee -:- unit cee)
('a',"bc") :: (Char,[Char])

pair :: Expr -> Expr -> Expr

The pair constructor lifted over Exprs.

This works for some variations of Int, Bool and Char element types and their lists.

> pair zero xxs

(0,xs) :: (Int,[Int])

Differently from foldPair, when this works,- it always constructs a well-typed expression.

comma :: Expr

The pair constructor ( :: ... -> (Int,Int) ) encoded as an Expr.

triple :: Expr -> Expr -> Expr -> Expr

The triple/trio constructor lifted over Exprs.

This works for some combinations of the Int, Bool and Char element types and their lists.

quadruple :: Expr -> Expr -> Expr -> Expr -> Expr

The quadruple constructor lifted over Exprs.

This works for some combinations of the Int, Bool and Char element types and their lists.

quintuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr

The quintuple constructor lifted over Exprs.

This only works for the Int element type.

sixtuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr

The sixtuple constructor lifted over Exprs.

This only works for the Int element type.

bs_ :: Expr

A typed hole of [Bool] type encoded as an Expr.

> bs_
_ :: [Bool]

pps :: Expr

Expr representing a variable p' :: `[Bool]`.

> pps
ps :: [Bool]

qqs :: Expr

A typed hole of '[Bool]' type

> qqs
qs :: [Bool]

and' :: Expr -> Expr

and lifted over the Expr type.

> and' pps
and ps :: Bool

> evl (and' $ expr [False,True]) :: Bool
False

or' :: Expr -> Expr

or lifted over the Expr type.

> or' pps
or ps :: Bool

> evl (or' $ expr [False,True]) :: Bool
True

sum' :: Expr -> Expr

sum of Int elements lifted over the Expr type.

> sum' xxs
sum xs :: Int

> evl (sum' $ expr [1,2,3::Int]) :: Int
6

product' :: Expr -> Expr

product of Int elements lifted over the Expr type.

> product' xxs
product xs :: Int

> evl (product' $ expr [1,2,3::Int]) :: Int
6

(-%-) :: Expr -> Expr -> Expr

The % constructor lifted over Exprs.

> val (2 :: Integer) -%- val (3 :: Integer)
2 % 3 :: Ratio Integer

This only accepts Exprs bound to the Integer type.

(-.-) :: Expr -> Expr -> Expr

Function composition . lifted over Expr.

> absE -.- negateE
abs . negate :: Int -> Int

> absE -.- negateE :$ one
(abs . negate) 1 :: Int

This works for Int, Bool, Char and their lists.

mapE :: Expr

map over the Int element type encoded as an Expr

> mapE
map :: (Int -> Int) -> [Int] -> [Int]

map' :: Expr -> Expr -> Expr

map lifted over Exprs.

> map' absE (unit one)
map abs [1] :: [Int]

filter' :: Expr -> Expr -> Expr

filter lifted over Exprs.

> filter' absE (unit one)
filter odd [1] :: [Int]

enumFrom' :: Expr -> Expr

enumFrom lifted over Exprs.

> enumFrom' zero
enumFrom 0 :: [Int]

Works for Ints, Bools and Chars.

(-..) :: Expr -> () -> Expr

enumFrom lifted over Exprs named as ".." for pretty-printing.

> one -.. ()
[1..] :: [Int]

Works for Ints, Bools and Chars.

enumFromTo' :: Expr -> Expr -> Expr

enumFromTo lifted over Exprs

> enumFromTo' zero four
enumFromTo 0 4 :: [Int]

(-..-) :: Expr -> Expr -> Expr

enumFromTo lifted over Exprs but named as ".." for pretty-printing.

> zero -..- four
[0..4] :: [Int]

enumFromThen' :: Expr -> Expr -> Expr

enumFromThen lifted over Exprs

> enumFromThen' zero ten
enumFromThen 0 10 :: [Int]

(--..) :: (Expr, Expr) -> () -> Expr

enumFromThen lifted over Exprs but named as ",.." for pretty printing.

> (zero,ten) --.. ()
[0,10..] :: [Int]

enumFromThenTo' :: Expr -> Expr -> Expr -> Expr

enumFromThenTo lifted over Exprs.

> enumFromThenTo' zero two ten
enumFromThenTo 0 2 10 :: [Int]

(--..-) :: (Expr, Expr) -> Expr -> Expr

enumFromThenTo lifted over Exprs but named as ",.." for pretty-printing.

> (zero,two) --..- ten
[0,2..10] :: [Int]

module Conjure.Reason