-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | synthesize Haskell functions out of partial definitions -- -- Conjure is a tool that synthesizes Haskell functions out of partial -- definitions. @package code-conjure @version 0.5.12 -- | An internal module of Conjure. This exports List, -- Maybe, Function and a few other simple utitilites. module Conjure.Utils -- | Counts the number of occurrences on a list. count :: (a -> Bool) -> [a] -> Int -- | Nubs using a given field. nubOn :: Eq b => (a -> b) -> [a] -> [a] -- | Equivalent to nub . sort but running in O(n log n). nubSort :: Ord a => [a] -> [a] -- | Zips Monoid values leaving trailing values. -- --

--   > mzip ["ab","cd"] ["ef"]
--   ["abef","cd"]
--

mzip :: Monoid a => [a] -> [a] -> [a] -- | Group values using a given field selector. groupOn :: Eq b => (a -> b) -> [a] -> [[a]] -- | WARNING: uses unsafePerformIO and should only be used -- for debugging! -- --

--   > idIO print 10
--   10
--   10
--

idIO :: (a -> IO ()) -> a -> a -- | Applies a function to the head of a list. mapHead :: (a -> a) -> [a] -> [a] -- | Return sets of values based on the list. -- -- The values in the list must me unique. sets :: [a] -> [[a]] -- | Like head but allows providing a default value. headOr :: a -> [a] -> a -- | Checks if all elements of a list are equal. allEqual :: Eq a => [a] -> Bool allEqualOn :: Eq b => (a -> b) -> [a] -> Bool -- | Checks if all elements of a list are equal. -- -- Exceptionally this function returns false for an empty or unit list. -- -- This returns true when all elements are equal and the list has a -- length greater than or equal to two. allEqual2 :: Eq a => [a] -> Bool -- | Lists choices of values. choices :: [a] -> [(a, [a])] -- | Lists choices of values that follow a property. choicesThat :: (a -> [a] -> Bool) -> [a] -> [(a, [a])] -- | A variation of foldr that only uses "zero" when the list is empty foldr0 :: (a -> a -> a) -> a -> [a] -> a -- | Indents a block of text by 4 spaces indent :: String -> String -- | Indents a block of text with the provided amount of spaces indentBy :: Int -> String -> String -- | Classify values using their Eq instance. -- --

--   > classify [1,2,3,1,2,1]
--   [[1,1,1],[2,2],[3]]
--

-- -- (cf. classifyBy, classifyOn) classify :: Eq a => [a] -> [[a]] -- | Classify values by a given comparison function. -- --

--   > classifyBy (\(x,_) (y,_) -> x == y) [(1,1),(1,2),(2,1),(2,2)]
--   [[(1,1),(1,2)],[(2,1),(2,2)]]
--

-- -- (cf. classify, classifyOn) classifyBy :: (a -> a -> Bool) -> [a] -> [[a]] -- | Classify values based on the result of a given function. -- --

--   > classifyOn head ["sheep", "chip", "ship", "cheap"]
--   [["sheep","ship"],["chip","cheap"]]
--

-- --

--   > classifyOn odd [1,2,3,4,5,6]
--   [[1,3,5],[2,4,6]]
--

-- -- (cf. classify, classifyBy) classifyOn :: Eq b => (a -> b) -> [a] -> [[a]] none :: (a -> Bool) -> [a] -> Bool -- | Updates the value in a list at a given position. -- --

--   > updateAt 2 (*10) [1,2,3,4]
--   [1,2,30,4]
--

updateAt :: Int -> (a -> a) -> [a] -> [a] -- | Applies a function to the first element of a pair. Often known on the -- wild as mapFst. -- --

--   > first (*10) (1,2)
--   (10,2)
--

first :: (a -> a') -> (a, b) -> (a', b) -- | Applies a function to the second element of a pair. Often known on the -- wild as mapSnd. -- --

--   > second (*100) (1,2)
--   (1,200)
--

second :: (b -> b') -> (a, b) -> (a, b') both :: (a -> b) -> (a, a) -> (b, b) (+++) :: Ord a => [a] -> [a] -> [a] infixr 5 +++ -- | O(n log n). Checks that all elements of the first list are -- elements of the second. isSubsetOf :: Ord a => [a] -> [a] -> Bool -- | This internal module reexports Express along with a few other -- utilities. module Conjure.Expr -- | 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''", ...]
--

class () => Name a -- | 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"
--

name :: Name a => a -> String -- | 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. data () => Expr -- | a value enconded as String and Dynamic Value :: String -> Dynamic -> Expr -- | function application between expressions (:$) :: Expr -> Expr -> Expr -- | 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)
--

--   > 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. (//) :: Expr -> [(Expr, Expr)] -> Expr -- | foldr lifted over Exprs. -- --

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

foldr' :: Expr -> 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
--

fill :: Expr -> [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]
--

fold :: [Expr] -> Expr -- | 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
--

evaluate :: Typeable a => Expr -> Maybe a -- | 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]
--

unfold :: Expr -> [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. cons :: Expr -- | The function div for the Int type lifted over the -- Expr type. (See also mod.) -- --

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

div' :: 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
--

mod' :: Expr -> Expr -> Expr -- | Lists valid applications between lists of Exprs -- --

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

(>$$<) :: [Expr] -> [Expr] -> [Expr] -- | 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
--

size :: Expr -> Int -- | 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]
--

value :: Typeable a => String -> a -> Expr -- | The operator * for the Int type. (See also -*-.) -- --

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

-- --

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

-- --

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

times :: Expr -- | 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'
--

typ :: Expr -> TypeRep -- | 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
--

arity :: Expr -> Int -- | Function composition encoded as an Expr: -- --

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

compose :: 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]
--

unit :: Expr -> Expr -- | The value 0 bound to the Int type encoded as an -- Expr. -- --

--   > zero
--   0 :: Int
--

zero :: 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
--

match :: Expr -> Expr -> Maybe [(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
--

canonicalize :: 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). mapValues :: (Expr -> Expr) -> 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
--   ]
--

canonicalVariations :: Expr -> [Expr] -- | 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. deriveExpress :: Name -> DecsQ -- | 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''", ...]
--

variableNamesFromTemplate :: String -> [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''", ...]
--

names :: Name a => a -> [String] -- | 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
--

isInstanceOf :: Expr -> Expr -> Bool -- | Derives a Name instance for the given type Name. -- -- This function needs the TemplateHaskell extension. deriveName :: Name -> DecsQ -- | Same as deriveName but does not warn when instance already -- exists (deriveName is preferable). deriveNameIfNeeded :: Name -> DecsQ -- | Derives a Name instance for a given type Name cascading -- derivation of type arguments as well. deriveNameCascading :: Name -> DecsQ -- | 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
--

val :: (Typeable a, Show a) => a -> 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
--

($$) :: Expr -> Expr -> Maybe 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 -- ('_'). var :: Typeable a => String -> a -> Expr -- | 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)
--

etyp :: Expr -> Either (TypeRep, TypeRep) 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
--

mtyp :: Expr -> Maybe TypeRep -- | 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
--

isIllTyped :: 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
--

isWellTyped :: 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
--

isFun :: Expr -> Bool -- | 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
--

eval :: Typeable a => 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. evl :: Typeable a => Expr -> a -- | 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
--

toDynamic :: Expr -> Maybe Dynamic -- | 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)"
--

showOpExpr :: String -> Expr -> String -- | O(n). Like showExpr but allows specifying the -- surrounding precedence. -- --

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

-- --

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

showPrecExpr :: Int -> 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)
--

showExpr :: Expr -> String -- | 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: -- --

e1 is smaller in size/length than e2, e.g.: x + -- y < x + (y + z);
or, e1 has more distinct variables than e2, e.g.: -- x + y < x + x;
or, e1 has more variable occurrences than e2, e.g.: -- x + x < 1 + x;
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. compareComplexity :: 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. compareLexicographically :: 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. compareQuickly :: Expr -> Expr -> Ordering -- | 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]
--

unfoldApp :: Expr -> [Expr] -- | 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
--

hasVar :: 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
--

isGround :: 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
--

isConst :: 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
--

isVar :: 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
```

isValue :: 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)

isApp :: Expr -> Bool -- | 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
--   ]
--

subexprs :: 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))))). nubSubexprs :: 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
--   ]
--

values :: 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
--   ]
--

--   > 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
--   ]
--

consts :: 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
--   ]
--

--   > 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]
--

vars :: 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))))). nubVars :: Expr -> [Expr] -- | 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. depth :: 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. height :: Expr -> Int -- | 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
--

matchWith :: [(Expr, Expr)] -> Expr -> Expr -> Maybe [(Expr, Expr)] -- | 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
--

encompasses :: Expr -> Expr -> Bool -- | Checks if any of the subexpressions of the first argument Expr -- is an instance of the second argument Expr. hasInstanceOf :: 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
--

isSubexprOf :: Expr -> Expr -> Bool -- | 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). mapVars :: (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). mapConsts :: (Expr -> 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). mapSubexprs :: (Expr -> Maybe 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). (//-) :: Expr -> [(Expr, 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! renameVarsBy :: (String -> 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
--

varAsTypeOf :: String -> 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
--

holeAsTypeOf :: Expr -> 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
--

hole :: Typeable a => a -> Expr -- | 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
--

isHole :: Expr -> Bool -- | 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]
--

holes :: 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]
--

--   > hasHole $ hole (undefined :: Bool)
--   True
--

-- --

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

-- --

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

hasHole :: 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. isComplete :: Expr -> Bool -- | 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
--   , ...
--   ]
--

listVars :: Typeable a => String -> a -> [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
--   , ...
--   ]
--

listVarsAsTypeOf :: String -> 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. foldApp :: [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)
--

foldPair :: (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)
--

unfoldPair :: 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)
--

foldTrio :: (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) unfoldTrio :: Expr -> (Expr, Expr, Expr) -- | Same as deriveExpress but does not warn when instance already -- exists (deriveExpress is preferable). deriveExpressIfNeeded :: Name -> DecsQ -- | Derives a Express instance for a given type Name -- cascading derivation of type arguments as well. deriveExpressCascading :: Name -> DecsQ -- | 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]
--

($$<) :: Expr -> [Expr] -> [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 ]
--

reifyEq :: (Typeable a, Eq 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 ]
--

reifyOrd :: (Typeable a, Ord a) => a -> [Expr] -- | O(1). Reifies Eq and Ord instances into a list of -- Expr. reifyEqOrd :: (Typeable a, Ord 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]]
--

reifyName :: (Typeable a, Name a) => a -> [Expr] -- | O(1). Builds a reified Eq instance from the given -- == function. (cf. reifyEq) -- --

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

mkEq :: Typeable a => (a -> a -> Bool) -> [Expr] -- | O(1). Builds a reified Ord instance from the given -- compare function. (cf. reifyOrd, mkOrdLessEqual) mkOrd :: Typeable a => (a -> a -> Ordering) -> [Expr] -- | O(1). Builds a reified Ord instance from the given -- <= function. (cf. reifyOrd, mkOrd) mkOrdLessEqual :: Typeable a => (a -> a -> Bool) -> [Expr] -- | O(1). Builds a reified Name instance from the given -- name function. (cf. reifyName, mkNameWith) mkName :: Typeable a => (a -> String) -> [Expr] -- | O(1). Builds a reified Name instance from the given -- String and type. (cf. reifyName, mkName) mkNameWith :: Typeable a => String -> a -> [Expr] -- | O(n). Lookups for a comparison function (:: a -> a -> -- Bool) with the given name and argument type. lookupComparison :: String -> TypeRep -> [Expr] -> Maybe Expr -- | 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). isEqT :: [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). isOrdT :: [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). isEqOrdT :: [Expr] -> TypeRep -> 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). isEq :: [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). isOrd :: [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). isEqOrd :: [Expr] -> Expr -> Bool -- | 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. mkComparison :: String -> [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. mkEquation :: [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. mkComparisonLT :: [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. mkComparisonLE :: [Expr] -> Expr -> Expr -> Expr -- | 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"
--

lookupName :: [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. lookupNames :: [Expr] -> Expr -> [String] -- | O(n+m). Like lookupNames but returns a list of variables -- encoded as Exprs. listVarsWith :: [Expr] -> Expr -> [Expr] -- | Given a list of functional expressions and another expression, returns -- a list of valid applications. validApps :: [Expr] -> Expr -> [Expr] -- | Like validApps but returns a Maybe value. findValidApp :: [Expr] -> Expr -> Maybe Expr -- | A list of reified Name instances for an arbitrary selection of -- types from the Haskell Prelude. preludeNameInstances :: [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
--

canonicalizeWith :: (Expr -> [String]) -> Expr -> Expr -- | Like canonicalization but allows customization of the list of -- variable names. (cf. lookupNames, -- variableNamesFromTemplate) canonicalizationWith :: (Expr -> [String]) -> Expr -> [(Expr, Expr)] -- | Like isCanonical but allows specifying the list of variable -- names. isCanonicalWith :: (Expr -> [String]) -> Expr -> Bool -- | 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) ]
--

canonicalization :: Expr -> [(Expr, Expr)] -- | Returns whether an Expr is canonical: if applying -- canonicalize is an identity using names as provided by -- preludeNameInstances. isCanonical :: Expr -> Bool -- | 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. mostGeneralCanonicalVariation :: 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. mostSpecificCanonicalVariation :: 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. fastCanonicalVariations :: 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. fastMostGeneralVariation :: 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. fastMostSpecificVariation :: Expr -> Expr -- | Expr representing a hole of Bool type. -- --

--   > b_
--   _ :: Bool
--

b_ :: Expr -- | Expr representing a variable p :: Bool. -- --

--   > pp
--   p :: Bool
--

pp :: Expr -- | Expr representing a variable q :: Bool. -- --

--   > qq
--   q :: Bool
--

qq :: Expr -- | Expr representing a variable r :: Bool. -- --

--   > rr
--   r :: Bool
--

rr :: Expr -- | Expr representing a variable p' :: Bool. -- --

--   > pp'
--   p' :: Bool
--

pp' :: Expr -- | False encoded as an Expr. -- --

--   > false
--   False :: Bool
--

false :: Expr -- | True encoded as an Expr. -- --

--   > true
--   True :: Bool
--

true :: Expr -- | The function not encoded as an Expr. -- --

--   > notE
--   not :: Bool -> Bool
--

notE :: Expr -- | The function and encoded as an Expr. -- --

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

andE :: Expr -- | The function or encoded as an Expr. -- --

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

orE :: Expr -- | The function ==> lifted over Exprs. -- --

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

-- --

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

(-==>-) :: Expr -> Expr -> Expr infixr 0 -==>- -- | The ==> operator encoded as an Expr implies :: Expr -- | The function not lifted over the Expr type. -- --

--   > not' false
--   not False :: Bool
--

-- --

--   > evalBool $ not' false
--   True
--

-- --

--   > not' pp
--   not p :: Bool
--

not' :: Expr -> Expr -- | 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 3 -&&- -- | The function || lifted over the Expr type. -- --

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

-- --

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

-- --

--   > evalBool $ false -||- true
--   True
--

(-||-) :: Expr -> Expr -> Expr infixr 2 -||- -- | A typed hole of Int type. -- --

--   > i_
--   _ :: Int
--

i_ :: Expr -- | A variable x of Int type. -- --

--   > xx
--   x :: Int
--

xx :: Expr -- | A variable y of Int type. -- --

--   > yy
--   y :: Int
--

yy :: Expr -- | A variable z of Int type. -- --

--   > zz
--   z :: Int
--

zz :: Expr -- | A variable x' of Int type. -- --

--   > xx'
--   x' :: Int
--

xx' :: Expr -- | A variable i of Int type. -- --

--   > ii
--   i :: Int
--

ii :: Expr -- | A variable j of Int type. -- --

--   > jj
--   j :: Int
--

jj :: Expr -- | A variable k of Int type. -- --

--   > kk
--   k :: Int
--

kk :: Expr -- | A variable i' of Int type. -- --

--   > ii'
--   i' :: Int
--

ii' :: Expr -- | A variable l of Int type. -- --

--   > ll
--   l :: Int
--

ll :: Expr -- | A variable m of Int type. -- --

--   > mm
--   m :: Int
--

mm :: Expr -- | A variable n of Int type. -- --

--   > nn
--   n :: Int
--

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

--   > one
--   1 :: Int
--

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

--   > two
--   2 :: Int
--

two :: Expr -- | The value 3 bound to the Int type encoded as an -- Expr. -- --

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

three :: Expr -- | The value 4 bound to the Int type encoded as an -- Expr. -- --

--   > four
--   4 :: Int
--

four :: Expr -- | The value 5 bound to the Int type encoded as an -- Expr. -- --

--   > five
--   5 :: Int
--

five :: Expr -- | The value 6 bound to the Int type encoded as an -- Expr. -- --

--   > six
--   6 :: Int
--

six :: Expr -- | The value 7 bound to the Int type encoded as an -- Expr. -- --

--   > seven
--   7 :: Int
--

seven :: Expr -- | The value 8 bound to the Int type encoded as an -- Expr. -- --

--   > eight
--   8 :: Int
--

eight :: Expr -- | The value 9 bound to the Int type encoded as an -- Expr. -- --

--   > nine
--   9 :: Int
--

nine :: Expr -- | The value 10 bound to the Int type encoded as an -- Expr. -- --

--   > ten
--   10 :: Int
--

ten :: Expr -- | The value 11 bound to the Int type encoded as an -- Expr. -- --

--   > eleven
--   11 :: Int
--

eleven :: Expr -- | The value 12 bound to the Int type encoded as an -- Expr. -- --

--   > twelve
--   12 :: Int
--

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

--   > minusOne
--   -1 :: Int
--

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

--   > minusOne
--   -2 :: Int
--

minusTwo :: 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
--

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

--   > ffE
--   f :: Int -> Int
--

ffE :: 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
--

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

--   > ggE
--   g :: Int -> Int
--

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

--   > hh zz
--   h z :: Int
--

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

--   > hhE
--   h :: Int -> Int
--

hhE :: 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. ff2 :: 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. ff3 :: 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. ff4 :: Expr -> Expr -> 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]
--

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

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

-- --

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

question :: 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]
--

oo :: Expr -> Expr -> 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
--

ooE :: Expr -- | 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
--

(-+-) :: Expr -> Expr -> Expr infixl 6 -+- -- | The operator + for the Int type. (See also -+-.) -- --

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

-- --

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

-- --

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

plus :: Expr -- | 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
--

(-*-) :: Expr -> Expr -> Expr infixl 7 -*- -- | The subtraction - operator encoded as an Expr. -- --

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

-- --

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

minus :: Expr -- | Integer division div encoded as an Expr. -- --

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

-- --

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

divE :: Expr -- | Integer modulo mod encoded as an Expr. -- --

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

-- --

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

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

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

quot' :: Expr -> Expr -> Expr -- | Integer quotient quot encoded as an Expr. -- --

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

-- --

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

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

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

rem' :: Expr -> Expr -> Expr -- | Integer remainder rem encoded as an Expr. -- --

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

-- --

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

remE :: 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
--

id' :: Expr -> 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
--

idE :: Expr -- | The function id encoded as an Expr. (cf. id') 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 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. const' :: Expr -> Expr -> Expr -- | negate over the Int type lifted over the Expr -- type. -- --

--   > negate' xx
--   negate x :: Int
--

-- --

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

negate' :: Expr -> Expr -- | negate over the Int type encoded as an Expr -- --

--   > negateE
--   negate :: Int -> Int
--

negateE :: Expr -- | abs over the Int type lifted over the Expr type. -- --

--   > abs' xx'
--   abs x' :: Int
--

-- --

--   > evl (abs' minusTwo) :: Int
--   2
--

abs' :: Expr -> Expr -- | abs over the Int type encoded as an Expr. -- --

--   > absE
--   abs :: Int -> Int
--

absE :: Expr -- | signum over the Int type lifted over the Expr -- type. -- --

--   > signum' xx'
--   signum x' :: Int
--

-- --

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

signum' :: Expr -> Expr -- | signum over the Int type encoded as an Expr. -- --

--   > signumE
--   signum :: Int -> Int
--

signumE :: Expr -- | odd with an Int argument lifted over the Expr -- type. -- --

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

-- --

--   > evl (odd' two) :: Bool
--   False
--

odd' :: Expr -> Expr -- | even with an Int argument lifted over the Expr -- type. -- --

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

-- --

--   > evl (even' two) :: Bool
--   True
--

even' :: Expr -> Expr -- | A hole of Char type encoded as an Expr. -- --

--   > c_
--   _ :: Char
--

c_ :: Expr -- | A hole of String type encoded as an Expr. -- --

--   > cs_
--   _ :: [Char]
--

cs_ :: Expr -- | A variable named c of type Char encoded as an -- Expr. -- --

--   > cc
--   c :: Char
--

cc :: Expr -- | A variable named c of type Char encoded as an -- Expr. -- --

--   > dd
--   d :: Char
--

dd :: Expr -- | A variable named cs of type String encoded as an -- Expr. -- --

--   > ccs
--   cs :: [Char]
--

ccs :: Expr -- | The character 'a' encoded as an Expr. -- --

--   > ae
--   'a' :: Char
--

-- --

--   > evl ae :: Char
--   'a'
--

ae :: Expr -- | The character 'b' encoded as an Expr -- --

--   > bee
--   'b' :: Char
--

-- --

--   > evl bee :: Char
--   'b'
--

bee :: Expr -- | The character 'c' encoded as an Expr -- --

--   > cee
--   'c' :: Char
--

-- --

--   > evl cee :: Char
--   'c'
--

cee :: Expr -- | The character 'd' encoded as an Expr -- --

--   > dee
--   'd' :: Char
--

-- --

--   > evl dee :: Char
--   'd'
--

dee :: Expr -- | The character 'z' encoded as an Expr -- --

--   > zed
--   'z' :: Char
--

-- --

--   > evl zed :: Char
--   'z'
--

-- -- (cf. zee) zed :: Expr -- | The character 'z' encoded as an Expr -- --

--   > zee
--   'z' :: Char
--

-- --

--   > evl zee :: Char
--   'z'
--

-- -- (cf. zed) zee :: Expr -- | The space character encoded as an Expr -- --

--   > space
--   ' ' :: Char
--

space :: Expr -- | The line break character encoded as an Expr -- --

--   > lineBreak
--   '\n' :: Char
--

lineBreak :: Expr -- | The ord function lifted over Expr -- --

--   > ord' bee
--   ord 'b' :: Int
--

-- --

--   > evl (ord' bee)
--   98
--

ord' :: Expr -> Expr -- | The ord function encoded as an Expr ordE :: Expr -- | A typed hole of [Int] type encoded as an Expr. -- --

--   > is_
--   _ :: [Int]
--

is_ :: Expr -- | A variable named xs of type [Int] encoded as an -- Expr. -- --

--   > xxs
--   xs :: [Int]
--

xxs :: Expr -- | A variable named ys of type [Int] encoded as an -- Expr. -- --

--   > yys
--   ys :: [Int]
--

yys :: Expr -- | A variable named zs of type [Int] encoded as an -- Expr. -- --

--   > yys
--   ys :: [Int]
--

zzs :: Expr -- | An empty list of type [Int] encoded as an Expr. -- --

--   > nil
--   [] :: [Int]
--

nil :: Expr -- | An empty String encoded as an Expr. -- --

--   > emptyString
--   "" :: String
--

emptyString :: Expr -- | The empty list '[]' encoded as an Expr. nilInt :: Expr -- | The empty list '[]' encoded as an Expr. nilBool :: Expr -- | The empty list '[]' encoded as an Expr. nilChar :: Expr -- | The list constructor : 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 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]
--

(-:-) :: Expr -> Expr -> Expr infixr 5 -:- -- | Append for list of Ints encoded as an Expr. appendInt :: Expr -- | 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]
--

(-++-) :: Expr -> Expr -> Expr infixr 5 -++- -- | 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
--

head' :: 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]
--

tail' :: 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
--

null' :: 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
--

length' :: 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]
--

init' :: 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]
--

sort' :: 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]
--

insert' :: 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
--

elem' :: 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]
--

drop' :: 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]
--

take' :: Expr -> Expr -> Expr -- | $ lifted over Exprs -- --

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

-- -- Works for Int, Bool, Char argument types and -- their lists. (-$-) :: Expr -> Expr -> Expr infixl 6 -$- -- | 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
--

(-<-) :: Expr -> Expr -> Expr infix 4 -<- -- | 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'
--

if' :: 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. caseBool :: 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. caseOrdering :: Expr -> Expr -> 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
--

compare' :: Expr -> Expr -> Expr -- | Nothing bound to the Maybe Int type encoded as an -- Expr. -- -- This is an alias to nothingInt. nothing :: Expr -- | Nothing bound to the Maybe Int type encoded as an -- Expr. nothingInt :: Expr -- | Nothing bound to the Maybe Bool type encoded as -- an Expr. nothingBool :: Expr -- | The Just constructor of the Int element type encoded as -- an Expr. justInt :: Expr -- | The Just constructor of the Bool element type encoded as -- an Expr. justBool :: 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
--

just :: Expr -> Expr -- | An infix synonym of pair. -- --

--   > zero -|- xxs
--

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

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

(-|-) :: 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. pair :: Expr -> Expr -> Expr -- | The pair constructor ( :: ... -> (Int,Int) ) encoded as an -- Expr. comma :: Expr -- | The triple/trio constructor lifted over Exprs. -- -- This works for some combinations of the Int, Bool and -- Char element types and their lists. triple :: 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. quadruple :: Expr -> Expr -> Expr -> Expr -> Expr -- | The quintuple constructor lifted over Exprs. -- -- This only works for the Int element type. quintuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -- | The sixtuple constructor lifted over Exprs. -- -- This only works for the Int element type. sixtuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr -- | A typed hole of [Bool] type encoded as an Expr. -- --

--   > bs_
--   _ :: [Bool]
--

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

--   > pps
--   ps :: [Bool]
--

pps :: Expr -- | A typed hole of '[Bool]' type -- --

--   > qqs
--   qs :: [Bool]
--

qqs :: Expr -- | and lifted over the Expr type. -- --

--   > and' pps
--   and ps :: Bool
--

-- --

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

and' :: Expr -> Expr -- | or lifted over the Expr type. -- --

--   > or' pps
--   or ps :: Bool
--

-- --

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

or' :: 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
--

sum' :: 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
--

product' :: 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. (-.-) :: Expr -> Expr -> Expr -- | map over the Int element type encoded as an Expr -- --

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

mapE :: Expr -- | map lifted over Exprs. -- --

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

map' :: Expr -> Expr -> Expr -- | filter lifted over Exprs. -- --

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

filter' :: Expr -> Expr -> Expr -- | enumFrom lifted over Exprs. -- --

--   > enumFrom' zero
--   enumFrom 0 :: [Int]
--

-- -- Works for Ints, Bools and Chars. enumFrom' :: Expr -> Expr -- | enumFrom lifted over Exprs named as ".." for -- pretty-printing. -- --

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

-- -- Works for Ints, Bools and Chars. (-..) :: Expr -> () -> Expr -- | enumFromTo lifted over Exprs -- --

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

enumFromTo' :: Expr -> Expr -> Expr -- | enumFromTo lifted over Exprs but named as ".." -- for pretty-printing. -- --

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

(-..-) :: Expr -> Expr -> Expr -- | enumFromThen lifted over Exprs -- --

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

enumFromThen' :: Expr -> Expr -> Expr -- | enumFromThen lifted over Exprs but named as -- ",.." for pretty printing. -- --

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

(--..) :: (Expr, Expr) -> () -> Expr -- | enumFromThenTo lifted over Exprs. -- --

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

enumFromThenTo' :: Expr -> Expr -> Expr -> Expr -- | enumFromThenTo lifted over Exprs but named as -- ",.." for pretty-printing. -- --

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

(--..-) :: (Expr, Expr) -> Expr -> Expr -- | Turns all variables of an expression into holes. -- --

--   > rehole (xx -+- yy)
--   _ + _ :: Int
--

rehole :: Expr -> Expr -- | Makes the function in an application a variable funToVar :: Expr -> Expr -- | Expands recursive calls on an expression until the given size limit is -- reached. -- --

--   > recursexpr 6 (ff xx) (ff xx)
--   f x :: Int
--

-- --

--   > recursexpr 6 (ff xx) (one -+- ff xx)
--   1 + (1 + (1 + (1 + f x))) :: Int
--

-- --

--   > recursexpr 6 (ff xx) (if' pp one (xx -*- ff xx))
--   (if p then 1 else x * (if p then 1 else x * f x)) :: Int
--

-- --

--   > recursexpr 6 (ff xx) (if' pp one (xx -*- ff (gg xx)))
--   (if p then 1 else x * (if p then 1 else g x * f (g (g x)))) :: Int
--

recursexpr :: Int -> Expr -> Expr -> Expr -- | Checks if the given recursive call apparently terminates. The first -- argument indicates the functional variable indicating the recursive -- call. -- --

--   > apparentlyTerminates ffE (ff xx)
--   False
--

-- --

--   > apparentlyTerminates ffE (if' pp zero (ff xx))
--   True
--

-- -- This function only allows recursion in the else clause: -- --

--   > apparentlyTerminates ffE (if' pp (ff xx) zero)
--   False
--

-- -- Of course, recursive calls as the condition are not allowed: -- --

--   > apparentlyTerminates ffE (if' (odd' (ff xx)) zero zero)
--   False
--

apparentlyTerminates :: Expr -> Expr -> Bool -- | Checks if the given functional expression may refrain from evaluating -- its next argument. -- --

--   > mayNotEvaluateArgument (plus :$ xx)
--   False
--

-- --

--   > mayNotEvaluateArgument (andE :$ pp)
--   True
--

-- -- This returns false for non-funcional value even if it involves an -- application which may not evaluate its argument. -- --

--   > mayNotEvaluateArgument (andE :$ pp :$ qq)
--   False
--

-- -- This currently works by checking if the function is an if, -- && or ||. mayNotEvaluateArgument :: Expr -> Bool -- | O(n). Compares the simplicity 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: -- --

e1 is smaller in size/length than e2, e.g.: x + -- y < x + (y + z);
or, e1 has less variable occurrences than e2,
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)
--   EQ
--

-- --

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

-- --

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

-- --

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

-- --

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

compareSimplicity :: Expr -> Expr -> Ordering -- | Creates an if Expr of the type of the given proxy. -- --

--   > ifFor (undefined :: Int)
--   if :: Bool -> Int -> Int -> Int
--

-- --

--   > ifFor (undefined :: String)
--   if :: Bool -> [Char] -> [Char] -> [Char]
--

ifFor :: Typeable a => a -> Expr -- | Creates a case Expr of the type of the given proxy. -- --

--   > caseForOrd (undefined :: Int)
--   case :: Ordering -> Int -> Int -> Int -> Int
--

-- --

--   > caseForOrd (undefined :: String)
--   case :: Ordering -> [Char] -> [Char] -> [Char] -> [Char]
--

caseForOrd :: Typeable a => a -> Expr -- | Lists terminal values in BFS order. -- -- (cf. values, holesBFS, fillBFS) valuesBFS :: Expr -> [Expr] -- | Lists holes in BFS order. -- -- (cf. holes, valuesBFS, fillBFS) holesBFS :: Expr -> [Expr] -- | Fills holes in BFS order. -- -- (cf. fill, valuesBFS, fillBFS) fillBFS :: Expr -> Expr -> Expr -- | Like $$ but always works regardless of type. -- -- Warning: just like :$, this may produce ill-typed -- expressions. -- --

--   > zero $$** zero
--   Just (0 0 :: ill-typed # Int $ Int #)
--

-- -- Together with $$|<, this function is unused but is useful -- when experiment with the source to see the effect of type-corrected on -- pruning the search space. -- -- (cf. $$, $$|<) ($$**) :: Expr -> Expr -> Maybe Expr -- | Like $$ but relaxed to work on correct kinds. -- --

--   > ordE $$|< zero
--   Just (ord 0 :: ill-typed # Char -> Int $ Int #)
--

-- --

--   > zero $$|< zero
--   Nothing
--

-- -- Warning: just like :$, this may produce ill-typed -- expressions. -- -- Together with $$**, this function is unused but is useful when -- experiment with the source to see the effect of type-corrected on -- pruning the search space. -- -- (cf. $$, $$**) ($$|<) :: Expr -> Expr -> Maybe Expr -- | Lists all distinct holes that are possible with the given -- Exprs. -- --

--   > possibleHoles [zero, one, plus]
--   [_ :: Int,_ :: Int -> Int,_ :: Int -> Int -> Int]
--

-- --

--   > possibleHoles [ae, ordE]
--   [_ :: Char,_ :: Int,_ :: Char -> Int]
--

possibleHoles :: [Expr] -> [Expr] -- | Evaluates an Expr to a regular Haskell value using the given -- recursive definition and maximum number of recursive calls. If there's -- a type mismatch, this function returns Nothing. -- -- (cf. evaluate, devaluate) revaluate :: Typeable a => (Expr, Expr) -> Int -> Expr -> Maybe a -- | Evaluates an Expr to a regular Haskell value using the given -- recursive definition and maximum number of recursive calls. If there's -- a type mismatch, this function returns the given default value. -- -- (cf. eval, deval) reval :: Typeable a => (Expr, Expr) -> Int -> a -> Expr -> a -- |

--   useMatches [xx,yy] [xx,yy]  =  [[(xx,xx), (yy,yy)]]
--   useMatches [xx,yy] [yy,xx]  =  [[(xx,xx), (yy,yy)]]
--   useMatches [yy,xx] [xx,yy]  =  [[(yy,yy), (xx,xx)]]
--   useMatches [xx,yy] [xx,xx]  =  []
--   useMatches [xx,yy] [abs' xx, abs' yy]  =  [[(xx,abs' xx), (yy, abs' yy)]]
--   useMatches [xx-:-xxs, yy-:-yys] [abs' xx, abs' yy]
--     =  [(xx-:-xxs, abs' xx), (yy-:-yys, abs' yy)]
--

useMatches :: [Expr] -> [Expr] -> [[(Expr, Expr)]] -- | Takes two expressions and returns all possible ways in which the first -- expression can appear once in one of the holes of the second -- expression. -- --

--   > deholings zero (i_ -+- i_ -+- i_)
--   [ (0 + _) + _ :: Int
--   , (_ + 0) + _ :: Int
--   , (_ + _) + 0 :: Int
--   ]
--

-- --

--   > deholings zero (i_ -+- one -+- ord' c_)
--   [(0 + 1) + ord _ :: Int]
--

deholings :: Expr -> Expr -> [Expr] -- | Given a variable, returns a constant with the same name varToConst :: Expr -> Expr -- | Returns whether the first Expr has an application instance of -- the second Expr. hasAppInstanceOf :: Expr -> Expr -> Bool -- | Is the expression encoding a negative number. -- -- This function is sort of a hack. isNegative :: Expr -> Bool -- | Is this a strict subexpression? isStrictSubexprOf :: Expr -> Expr -> Bool -- | Enumerate applications between values of the given list of primitives -- and of the given expressions's type. -- -- Arguments: -- --

an Expr whose type we are interested in
a filtering function, returning True for the expressions to -- keep
a list of primitives to be used in building expression.

-- -- Result: a potentially infinite list of list of enumerated -- expressions -- -- The enumeration here is type-directed for performance reasons. enumerateAppsFor :: Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]] -- | Given an expression whose holes are all of the same type and an -- enumeration of Exprs of this same type, enumerate all possible -- fillings of the original expression with the Exprs in the -- enumeration. enumerateFillings :: Expr -> [[Expr]] -> [[Expr]] -- | Dig a hole in a function application at the given position -- --

--   > digApp 1 (one -+- two)
--   _ + 2 :: Int
--

-- --

--   > digApp 2 (one -+- two)
--   1 + _ :: Int
--

digApp :: Int -> Expr -> Expr -- | Extracts a value in a function application at the given position -- --

--   > extractApp 1 (one -+- two)
--   (_ + 2 :: Int, 1 :: Int)
--

-- --

--   > extractApp 2 (one -+- two)
--   (1 + _ :: Int, 2 :: Int)
--

extractApp :: Int -> Expr -> (Expr, Expr) updateAppAt :: Int -> (Expr -> Expr) -> Expr -> Expr -- | Extracts the argument of a function application at the given position. -- --

--   (one -+- two) $!! 1
--

-- -- 1 :: Int -- --

--   (one -+- two) $!! 2
--

-- -- 2 :: Int ($!!) :: Expr -> Int -> Expr -- | Lists conflicts between two expressions -- --

--   > conflicts (one -+- two) (three -+- four)
--   [(1 :: Int,3 :: Int), (2 :: Int,4 :: Int)]
--

-- --

--   > conflicts (xx -:- nil) (xx -:- yy -:- yys)
--   [(nil, yy -:- yys)]
--

-- --

--   > conflicts  (one -:- one -:- nil) (zero -:- zero -:- xx -:- xxs)
--   [(1 :: Int,0 :: Int),([] :: [Int],x:xs :: [Int])]
--

conflicts :: Expr -> Expr -> [(Expr, Expr)] listConflicts :: [Expr] -> [[Expr]] -- | List all possible valuations of an expression (potentially infinite). -- In pseudo-Haskell: -- --

--   take 3 $ grounds (lookupTiers preludeInstances) ((x + x) + y)
--     == [(0 + 0) + 0, (0 + 0) + 1, (1 + 1) + 0]
--

-- -- Note this function will return an empty list when a Listable -- instance is not found in the Instances list. grounds :: (Expr -> [[Expr]]) -> Expr -> [Expr] -- | List all possible variable bindings to an expression -- --

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

groundBinds :: (Expr -> [[Expr]]) -> Expr -> [Binds] -- | Lists all variables in an expression that are of the same type of the -- expression itself. -- --

--   > rvars (ff xx)
--   [x :: Int]
--

-- --

--   > rvars (xx -:- xxs -++- yys)
--   [xs :: [Int], ys :: [Int]]
--

-- -- They are listed and without repetitions in Expr order: -- --

--   > rvars (xx -:- yys -++- xxs -++- xxs)
--   [xs :: [Int],ys :: [Int]]
--

-- -- (cf. nubVars) rvars :: Expr -> [Expr] instance Data.Express.Express.Express Test.LeanCheck.Utils.Types.A instance Data.Express.Express.Express Test.LeanCheck.Utils.Types.B instance Data.Express.Express.Express Test.LeanCheck.Utils.Types.C instance Data.Express.Express.Express Test.LeanCheck.Utils.Types.D instance Data.Express.Express.Express Test.LeanCheck.Utils.Types.E instance Data.Express.Express.Express Test.LeanCheck.Utils.Types.F -- | An internal module of Conjure, a library for Conjuring function -- implementations from tests or partial definitions. (a.k.a.: functional -- inductive programming) -- -- This module re-exports some functions from Test.Speculate along -- with a few additional utilities. module Conjure.Reason data () => Thy rules :: Thy -> [Rule] equations :: Thy -> [Equation] -- | reserved for rules and equations that were later found to be invalid -- through testing invalid :: Thy -> [Equation] -- | should be compatible with compareE canReduceTo :: Thy -> Expr -> Expr -> Bool -- | Prints a Thy (theory) on the console. (cf. showThy) printThy :: Thy -> IO () closureLimit :: Thy -> Int -- | Double-checks a resulting theory moving untrue rules and equations to -- the invalid list. -- -- As a side-effect of using testing to conjecturing equations, we may -- get smaller equations that are obviously incorrect when we consider a -- bigger (harder-to-test) equation that is incorrect. -- -- For example, given an incorrect large equation, it may follow that -- False=True. -- -- This function can be used to double-check the generated theory. If any -- equation or rule is discarded, that means the number of tests should -- probably be increased. doubleCheck :: (Expr -> Expr -> Bool) -> Thy -> Thy normalize :: Thy -> Expr -> Expr -- | Computes a theory from atomic expressions. Example: -- --

--   > theoryFromAtoms 5 (const True) (equal preludeInstances 100)
--   >   [hole (undefined :: Int),constant "+" ((+) :: Int -> Int -> Int)]
--   Thy { rules = [ (x + y) + z == x + (y + z) ]
--       , equations = [ y + x == x + y
--                     , y + (x + z) == x + (y + z)
--                     , z + (x + y) == x + (y + z)
--                     , z + (y + x) == x + (y + z) ]
--       , canReduceTo = (|>)
--       , closureLimit = 2
--       , keepE = keepUpToLength 5
--       }
--

theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy isRootNormalC :: Thy -> Expr -> Bool isRootNormalE :: Thy -> Expr -> Bool isCommutative :: Thy -> Expr -> Bool commutativeOperators :: Thy -> [Expr] -- | This module is part of Conjure. -- -- This module exports the Defn type synonym and utilities -- involving it. -- -- You are probably better off importing Conjure. module Conjure.Defn -- | A function definition as a list of top-level case bindings -- (Bndn). -- -- Here is an example using the notation from -- Data.Express.Fixtures: -- --

--   sumV :: Expr
--   sumV  =  var "sum" (undefined :: [Int] -> Int)
--   
--   (=-) = (,)
--   infixr 0 =-
--   
--   sumDefn :: Defn
--   sumDefn  =  [ sum' nil           =-  zero
--               , sum' (xx -:- xxs)  =-  xx -+- (sumV :$ xxs)
--               ]  where  sum' e  =  sumV :$ e
--

type Defn = [Bndn] -- | A single binding in a definition (Defn). type Bndn = (Expr, Expr) -- | Evaluates an Expr to a Dynamic value using the given -- Defn as definition when a recursive call is found. -- -- Arguments: -- --

a function that deeply reencodes an expression (cf. -- expr)
the maximum number of recursive evaluations
a Defn to be used when evaluating the given -- Expr
an Expr to be evaluated

-- -- This function cannot be used to evaluate a functional value for the -- given Defn and can only be used when occurrences of the given -- Defn are fully applied. -- -- The function the deeply reencodes an Expr can be defined using -- functionality present in Conjure.Conjurable. Here's a -- quick-and-dirty version that is able to reencode Bools, -- Ints and their lists: -- --

--   exprExpr :: Expr -> Expr
--   exprExpr  =  conjureExpress (undefined :: Bool -> [Bool] -> Int -> [Int] -> ())
--

-- -- The maximum number of recursive evaluations counts in two ways: -- --

the maximum number of entries in the recursive-evaluation memo -- table;
the maximum number of terminal values considered (but in this case -- the limit is multiplied by the _size_ of the given Defn.

-- -- These could be divided into two separate parameters but then there -- would be an extra _dial_ to care about... -- -- (cf. devaluate, deval, devl) toDynamicWithDefn :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic -- | Evaluates an Expr expression into Just a regular Haskell -- value using a Defn definition when it is found. If there's a -- type-mismatch, this function returns Nothing. -- -- This function requires a Expr-deep-reencoding function and a -- limit to the number of recursive evaluations. -- -- (cf. toDynamicWithDefn, deval, devl) devaluate :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a -- | Evaluates an Expr expression into a regular Haskell value using -- a Defn definition when it is found in the given expression. If -- there's a type-mismatch, this function return a default value. -- -- This function requires a Expr-deep-reencoding function and a -- limit to the number of recursive evaluations. -- -- (cf. toDynamicWithDefn, devaluate, devl') deval :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a -- | Evaluates an Expr expression into a regular Haskell value using -- a Defn definition when it is found in the given expression. If -- there's a type-mismatch, this raises an error. -- -- This function requires a Expr-deep-reencoding function and a -- limit to the number of recursive evaluations. -- -- (cf. toDynamicWithDefn, devaluate, deval') devl :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> a -- | Like deval but only works for when the given Defn -- definition has no case breakdowns. -- -- In other words, this only works when the given Defn is a -- singleton list whose first value of the only element is a simple -- application without constructors. devalFast :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a -- | Pretty-prints a Defn as a String: -- --

--   > putStr $ showDefn sumDefn
--   sum []  =  0
--   sum (x:xs)  =  x + sum xs
--

showDefn :: Defn -> String -- | Pretty-prints a Defn to the screen. -- --

--   > printDefn sumDefn
--   sum []  =  0
--   sum (x:xs)  =  x + sum xs
--

printDefn :: Defn -> IO () -- | Returns whether the given definition apparentlyTerminates. defnApparentlyTerminates :: Defn -> Bool -- | Returns whether the definition is complete, i.e., whether it does not -- have any holes in the RHS. isCompleteDefn :: Defn -> Bool -- | Returns whether the binding is complete, i.e., whether it does not -- have any holes in the RHS. isCompleteBndn :: Bndn -> Bool canonicalizeBndn :: Bndn -> Bndn canonicalizeBndnLast :: Int -> Bndn -> Bndn -- | Returns whether a binding has undefined variables, i.e., there are -- variables in the RHS that are not declared in the LHS. -- --

--   > hasUnbound (xx -:- xxs, xxs)
--   False
--

-- --

--   > hasUnbound (xx -:- xxs, yys)
--   True
--

-- -- For Defns, use isUndefined. hasUnbound :: Bndn -> Bool noUnbound :: Bndn -> Bool -- | Returns whether a Defn has undefined variables, i.e., there are -- variables in the RHSs that are not declared in the LHSs. -- --

--   > isUndefined [(nil, nil), (xx -:- xxs, xxs)]
--   False
--

-- --

--   > isUndefined [(nil, xxs), (xx -:- xxs, yys)]
--   True
--

-- -- For single Bndns, use hasUnbound. isUndefined :: Defn -> Bool isDefined :: Defn -> Bool -- | Returns whether a binding is a base case. -- --

--   > isBaseCase (ff (xx -:- nil), xx)
--   True
--

-- --

--   > isBaseCase (ff (xx -:- xxs), ff xxs)
--   False
--

-- -- (cf. isRecursiveCase) isBaseCase :: Bndn -> Bool -- | Returns whether a binding is a base case. -- --

--   > isRecursiveCase (ff (xx -:- nil), xx)
--   False
--

-- --

--   > isRecursiveCase (ff (xx -:- xxs), ff xxs)
--   True
--

-- -- (cf. isBaseCase) isRecursiveCase :: Bndn -> Bool -- | Returns whether a definition is recursive isRecursiveDefn :: Defn -> Bool -- | This module is part of Conjure. -- -- This module exports functions that check redundancy in Defns. -- -- You are probably better off importing Conjure. module Conjure.Defn.Redundancy -- | Returns whether the given Defn is redundant with regards to -- repetitions on RHSs. -- -- Here is an example of a redundant Defn: -- --

--   0 ? 0  =  1
--   0 ? x  =  1
--   x ? 0  =  x
--   x ? y  =  x
--

-- -- It is redundant because it is equivalent to: -- --

--   0 ? _  =  1
--   x ? _  =  x
--

-- -- This function safely handles holes on the RHSs by being conservative -- in cases these are found: nothing can be said before their fillings. isRedundantDefn :: Defn -> Bool -- | Returns whether the given Defn is redundant with regards to -- subsumption by latter patterns -- -- Here is an example of a redundant Defn by this criterium: -- --

--   foo 0  =  0
--   foo x  =  x
--

isRedundantBySubsumption :: Defn -> Bool -- | Returns whether the given Defn is redundant with regards to -- repetitions on RHSs. -- -- Here is an example of a redundant Defn: -- --

--   0 ? 0  =  1
--   0 ? x  =  1
--   x ? 0  =  x
--   x ? y  =  x
--

-- -- It is redundant because it is equivalent to: -- --

--   0 ? _  =  1
--   x ? _  =  x
--

-- -- 1 and x are repeated in the results for when the -- first arguments are 0 and x. isRedundantByRepetition :: Defn -> Bool -- | Returns whether the given Defn is redundant with regards to -- case elimination -- -- The following is redundant according to this criterium: -- --

--   foo []  =  []
--   foo (x:xs)  =  x:xs
--

-- -- It is equivalent to: -- --

--   foo xs = xs
--

-- -- The following is also redundant: -- --

--   [] ?? xs  =  []
--   (x:xs) ?? ys  =  x:xs
--

-- -- as it is equivalent to: -- --

--   xs ?? ys == xs
--

-- -- This function is not used as one of the criteria in -- isRedundantDefn because it does not pay-off in terms of runtime -- vs number of pruned candidates. isRedundantByIntroduction :: Defn -> Bool -- | Returns whether the given Defn is redundant modulo subsumption -- and rewriting. -- -- (cf. subsumedWith) isRedundantModuloRewriting :: (Expr -> Expr) -> Defn -> Bool -- | Returns whether the given Defn is redundant with regards to -- recursions -- -- The following is redundant: -- --

--   xs ?? []  =  []
--   xs ?? (x:ys)  =  xs ?? []
--

-- -- The LHS of a base-case pattern, matches the RHS of a recursive -- pattern. The second RHS may be replaced by simply [] which -- makes it redundant. hasRedundantRecursion :: Defn -> Bool -- | Returns whether a binding is subsumed by another modulo rewriting -- --

--   > let normalize = (// [(zero -+- zero, zero)])
--   > subsumedWith normalize (ff zero, zero) (ff xx, xx -+- xx)
--   True
--

-- --

--   > subsumedWith normalize (ff zero, zero) (ff xx, xx -+- one)
--   False
--

-- --

--   > subsumedWith normalize (zero -?- xx, zero) (xx -?- yy, xx -+- xx)
--   True
--

-- -- (cf. isRedundantModuloRewriting) subsumedWith :: (Expr -> Expr) -> Bndn -> Bndn -> Bool -- | Simplifies a definition by removing redundant patterns -- -- This may be useful in the following case: -- --

--   0 ^^^ 0  =  0
--   0 ^^^ x  =  x
--   x ^^^ 0  =  x
--   _ ^^^ _  =  0
--

-- -- The first pattern is subsumed by the last pattern. simplifyDefn :: Defn -> Defn -- | Introduces a hole at a given position in the binding: -- --

--   > introduceVariableAt 1 (xxs -?- (yy -:- yys), (yy -:- yys) -++- (yy -:- yys))
--   (xs ? (y:ys) :: [Int],(y:ys) ++ (y:ys) :: [Int])
--

-- --

--   > introduceVariableAt 2 (xxs -?- (yy -:- yys), (yy -:- yys) -++- (yy -:- yys))
--   (xs ? x :: [Int],x ++ x :: [Int])
--

-- -- Relevant occurrences are replaced. introduceVariableAt :: Int -> Bndn -> Bndn -- | This module is part of Conjure. -- -- This defines the Conjurable typeclass and utilities involving -- it. -- -- You are probably better off importing Conjure. module Conjure.Conjurable -- | Single reification of some functions over a type as Exprs. -- -- This is a sixtuple, in order: -- --

a hole encoded as an Expr;
the == function encoded as an Expr when -- available;
tiers of enumerated test values encoded as Exprs -- when available;
infinite list of potential variable names;
boolean indicating whether the type is atomic;
the conjureSize function encoded as an Expr.

type Reification1 = (Expr, Maybe Expr, Maybe [[Expr]], [String], Bool, Expr) -- | A reification over a collection of types. -- -- Represented as a transformation of a list to a list. type Reification = [Reification1] -> [Reification1] -- | Class of Conjurable types. Functions are Conjurable if -- all their arguments are Conjurable, Listable and -- Showable. -- -- For atomic types that are Listable, instances are defined as: -- --

--   instance Conjurable Atomic where
--     conjureTiers  =  reifyTiers
--

-- -- For atomic types that are both Listable and Eq, -- instances are defined as: -- --

--   instance Conjurable Atomic where
--     conjureTiers     =  reifyTiers
--     conjureEquality  =  reifyEquality
--

-- -- For types with subtypes, instances are defined as: -- --

--   instance Conjurable Composite where
--     conjureTiers     =  reifyTiers
--     conjureEquality  =  reifyEquality
--     conjureSubTypes x  =  conjureType y
--                        .  conjureType z
--                        .  conjureType w
--       where
--       (Composite ... y ... z ... w ...)  =  x
--

-- -- Above x, y, z and w are just -- proxies. The Proxy type was avoided for backwards -- compatibility. -- -- Please see the source code of Conjure.Conjurable for more -- examples. -- -- (cf. reifyTiers, reifyEquality, conjureType) class (Typeable a, Name a) => Conjurable a conjureArgumentHoles :: Conjurable a => a -> [Expr] -- | Returns Just the == function encoded as an Expr -- when available or Nothing otherwise. -- -- Use reifyEquality when defining this. conjureEquality :: Conjurable a => a -> Maybe Expr -- | Returns Just tiers of values encoded as Exprs -- when possible or Nothing otherwise. -- -- Use reifyTiers when defining this. conjureTiers :: Conjurable a => a -> Maybe [[Expr]] conjureSubTypes :: Conjurable a => a -> Reification -- | Returns an if-function encoded as an Expr. conjureIf :: Conjurable a => a -> Expr -- | Returns a top-level case breakdown. conjureCases :: Conjurable a => a -> [Expr] conjureArgumentCases :: Conjurable a => a -> [[Expr]] -- | Returns the (recursive) size of the given value. conjureSize :: Conjurable a => a -> Int -- | Returns a function that deeply reencodes an expression when possible. -- (id when not available.) -- -- Use reifyExpress when defining this. conjureExpress :: Conjurable a => a -> Expr -> Expr conjureEvaluate :: Conjurable a => (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a -- | To be used in the implementation of conjureSubTypes. -- --

--   instance ... => Conjurable <Type> where
--     ...
--     conjureSubTypes x  =  conjureType (field1 x)
--                        .  conjureType (field2 x)
--                        .  ...
--                        .  conjureType (fieldN x)
--     ...
--

conjureType :: Conjurable a => a -> Reification -- | Reifies equality to be used in a conjurable type. -- -- This is to be used in the definition of conjureTiers of -- Conjurable typeclass instances: -- --

--   instance ... => Conjurable <Type> where
--     ...
--     conjureTiers  =  reifyTiers
--     ...
--

reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]] -- | Reifies equality == in a Conjurable type instance. -- -- This is to be used in the definition of conjureEquality of -- Conjurable typeclass instances: -- --

--   instance ... => Conjurable <Type> where
--     ...
--     conjureEquality  =  reifyEquality
--     ...
--

reifyEquality :: (Eq a, Typeable a) => a -> Maybe Expr -- | Reifies the expr function in a Conjurable type instance. -- -- This is to be used in the definition of conjureExpress of -- Conjurable typeclass instances. -- --

--   instance ... => Conjurable <Type> where
--     ...
--     conjureExpress  =  reifyExpress
--     ...
--

reifyExpress :: (Express a, Show a) => a -> Expr -> Expr -- | Computes a complete application for the given function. -- --

--   > conjureApplication "not" not
--   not p :: Bool
--

-- --

--   > conjureApplication "+" ((+) :: Int -> Int -> Int)
--   x + y :: Int
--

-- -- (cf. conjureVarApplication) conjureApplication :: Conjurable f => String -> f -> Expr -- | Computes a complete application for a variable of the same type of the -- given function. -- --

--   > conjureVarApplication "not" not
--   not p :: Bool
--

-- --

--   > conjureVarApplication "+" ((+) :: Int -> Int -> Int)
--   x + y :: Int
--

-- -- (cf. conjureApplication) conjureVarApplication :: Conjurable f => String -> f -> Expr -- | Computes tiers of sets of patterns for the given function. -- --

--   > conjurePats [zero] "f" (undefined :: Int -> Int)
--   [[[f x :: Int]],[[f 0 :: Int,f x :: Int]]]
--

conjurePats :: Conjurable f => [Expr] -> String -> f -> [[[Expr]]] -- | Computes a list of holes encoded as Exprs from a -- Conjurable functional value. -- -- (cf. cjHoles) conjureHoles :: Conjurable f => f -> [Expr] -- | Compute tiers of values encoded as Exprs of the type of -- the given Expr. conjureTiersFor :: Conjurable f => f -> Expr -> [[Expr]] -- | Compure a list of values encoded as Exprs of the type of -- the given Expr. conjureListFor :: Conjurable f => f -> Expr -> [Expr] -- | Conjures an Expr-encoded size function for the given expression -- type. -- --

--   > conjureSizeFor (undefined :: [Int] -> [Bool]) i_
--   conjureSize :: Int -> Int
--

-- --

--   > conjureSizeFor (undefined :: [Int] -> [Bool]) is_
--   conjureSize :: [Int] -> Int
--

-- --

--   > conjureSizeFor (undefined :: [Int] -> [Bool]) bs_
--   conjureSize :: [Bool] -> Int
--

conjureSizeFor :: Conjurable f => f -> Expr -> Expr conjureGrounds :: Conjurable f => f -> Expr -> [Expr] -- | Given a Conjurable functional value, computes a function that -- checks whether two Exprs are equal up to a given number of -- tests. conjureAreEqual :: Conjurable f => f -> Int -> Expr -> Expr -> Bool -- | Computes a function that makes an equation between two expressions. conjureMkEquation :: Conjurable f => f -> Expr -> Expr -> Expr -- | Generic type A. -- -- Can be used to test polymorphic functions with a type variable such as -- take or sort: -- --

--   take :: Int -> [a] -> [a]
--   sort :: Ord a => [a] -> [a]
--

-- -- by binding them to the following types: -- --

--   take :: Int -> [A] -> [A]
--   sort :: [A] -> [A]
--

-- -- This type is homomorphic to Nat6, B, C, D, -- E and F. -- -- It is instance to several typeclasses so that it can be used to test -- functions with type contexts. data () => A -- | Generic type B. -- -- Can be used to test polymorphic functions with two type variables such -- as map or foldr: -- --

--   map :: (a -> b) -> [a] -> [b]
--   foldr :: (a -> b -> b) -> b -> [a] -> b
--

-- -- by binding them to the following types: -- --

--   map :: (A -> B) -> [A] -> [B]
--   foldr :: (A -> B -> B) -> B -> [A] -> B
--

-- -- This type is homomorphic to A, Nat6, C, D, -- E and F. data () => B -- | Generic type C. -- -- Can be used to test polymorphic functions with three type variables -- such as uncurry or zipWith: -- --

--   uncurry :: (a -> b -> c) -> (a, b) -> c
--   zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
--

-- -- by binding them to the following types: -- --

--   uncurry :: (A -> B -> C) -> (A, B) -> C
--   zipWith :: (A -> B -> C) -> [A] -> [B] -> [C]
--

-- -- This type is homomorphic to A, B, Nat6, D, -- E and F. data () => C -- | Generic type D. -- -- Can be used to test polymorphic functions with four type variables. -- -- This type is homomorphic to A, B, C, Nat6, -- E and F. data () => D -- | Generic type E. -- -- Can be used to test polymorphic functions with five type variables. -- -- This type is homomorphic to A, B, C, D, -- Nat6 and F. data () => E -- | Generic type F. -- -- Can be used to test polymorphic functions with five type variables. -- -- This type is homomorphic to A, B, C, D, -- E and Nat6. data () => F -- | Checks if an Expr is of an unbreakable type. conjureIsUnbreakable :: Conjurable f => f -> Expr -> Bool -- | Conjures a list of Reification1 for a Conjurable type, -- its subtypes and Bool. -- -- This is used in the implementation of conjureHoles, -- conjureMkEquation, conjureAreEqual, -- conjureTiersFor, conjureNamesFor, -- conjureIsUnbreakable, etc. conjureReification :: Conjurable a => a -> [Reification1] -- | Conjures a Reification1 for a Conjurable type. -- -- This is used in the implementation of conjureReification. conjureReification1 :: Conjurable a => a -> Reification1 conjureDynamicEq :: Conjurable f => f -> Dynamic conjureIsNumeric :: Conjurable f => f -> Expr -> Bool -- | Evaluates a Defn into a regular Haskell value returning -- Nothing when there's a type mismatch. -- -- The integer argument indicates the limit of recursive evaluations. cevaluate :: Conjurable f => Int -> Defn -> Maybe f -- | Evaluates a Defn into a regular Haskell value returning the -- given default value when there's a type mismatch. -- -- The integer argument indicates the limit of recursive evaluations. ceval :: Conjurable f => Int -> f -> Defn -> f -- | Evaluates a Defn into a regular Haskell value raising an error -- there's a type mismatch. -- -- The integer argument indicates the limit of recursive evaluations. cevl :: Conjurable f => Int -> Defn -> f -- | 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''", ...]
--

class () => Name a -- | 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"
--

name :: Name a => a -> String -- | 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.

--   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 class (Show a, Typeable a) => Express a expr :: Express a => a -> Expr -- | Returns a list of tiers of possible patterns for each argument. -- -- The outer list has the same number of elements as the number of -- arguments of the given function. -- -- This function is internal and only used in the implementation of -- conjurePats. It may be removed from the API without further -- notice. It has been temporarily promoted to public to help refactor -- conjurePats. conjureArgumentPats :: Conjurable f => [Expr] -> f -> [[[[Expr]]]] conjureMostGeneralCanonicalVariation :: Conjurable f => f -> Expr -> Expr instance Conjure.Conjurable.Conjurable () instance Conjure.Conjurable.Conjurable GHC.Types.Bool instance Conjure.Conjurable.Conjurable GHC.Types.Int instance Conjure.Conjurable.Conjurable GHC.Num.Integer.Integer instance Conjure.Conjurable.Conjurable GHC.Types.Char instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, Data.Express.Express.Express a, GHC.Show.Show a) => Conjure.Conjurable.Conjurable [a] instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b) => Conjure.Conjurable.Conjurable (a, b) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c) => Conjure.Conjurable.Conjurable (a, b, c) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a) => Conjure.Conjurable.Conjurable (GHC.Maybe.Maybe a) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b) => Conjure.Conjurable.Conjurable (Data.Either.Either a b) instance (Conjure.Conjurable.Conjurable a, Conjure.Conjurable.Conjurable b) => Conjure.Conjurable.Conjurable (a -> b) instance Conjure.Conjurable.Conjurable GHC.Types.Ordering instance Conjure.Conjurable.Conjurable GHC.Types.Float instance Conjure.Conjurable.Conjurable GHC.Types.Double instance Conjure.Conjurable.Conjurable GHC.Int.Int8 instance Conjure.Conjurable.Conjurable GHC.Int.Int16 instance Conjure.Conjurable.Conjurable GHC.Int.Int32 instance Conjure.Conjurable.Conjurable GHC.Int.Int64 instance Conjure.Conjurable.Conjurable GHC.Types.Word instance Conjure.Conjurable.Conjurable GHC.Word.Word8 instance Conjure.Conjurable.Conjurable GHC.Word.Word16 instance Conjure.Conjurable.Conjurable GHC.Word.Word32 instance Conjure.Conjurable.Conjurable GHC.Word.Word64 instance (GHC.Real.Integral a, Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, GHC.Classes.Eq a, Data.Express.Express.Express a) => Conjure.Conjurable.Conjurable (GHC.Real.Ratio a) instance (GHC.Float.RealFloat a, Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, GHC.Classes.Eq a, Data.Express.Express.Express a) => Conjure.Conjurable.Conjurable (Data.Complex.Complex a) instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.A instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.B instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.C instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.D instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.E instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.F instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Data.Express.Express.Express d) => Conjure.Conjurable.Conjurable (a, b, c, d) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Data.Express.Express.Express d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Data.Express.Express.Express e) => Conjure.Conjurable.Conjurable (a, b, c, d, e) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Data.Express.Express.Express d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Data.Express.Express.Express e, Conjure.Conjurable.Conjurable f, Test.LeanCheck.Core.Listable f, GHC.Show.Show f, Data.Express.Express.Express f) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Data.Express.Express.Express d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Data.Express.Express.Express e, Conjure.Conjurable.Conjurable f, Test.LeanCheck.Core.Listable f, GHC.Show.Show f, Data.Express.Express.Express f, Conjure.Conjurable.Conjurable g, Test.LeanCheck.Core.Listable g, GHC.Show.Show g, Data.Express.Express.Express g) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f, g) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Data.Express.Express.Express d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Data.Express.Express.Express e, Conjure.Conjurable.Conjurable f, Test.LeanCheck.Core.Listable f, GHC.Show.Show f, Data.Express.Express.Express f, Conjure.Conjurable.Conjurable g, Test.LeanCheck.Core.Listable g, GHC.Show.Show g, Data.Express.Express.Express g, Conjure.Conjurable.Conjurable h, Test.LeanCheck.Core.Listable h, GHC.Show.Show h, Data.Express.Express.Express h) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f, g, h) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Data.Express.Express.Express d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Data.Express.Express.Express e, Conjure.Conjurable.Conjurable f, Test.LeanCheck.Core.Listable f, GHC.Show.Show f, Data.Express.Express.Express f, Conjure.Conjurable.Conjurable g, Test.LeanCheck.Core.Listable g, GHC.Show.Show g, Data.Express.Express.Express g, Conjure.Conjurable.Conjurable h, Test.LeanCheck.Core.Listable h, GHC.Show.Show h, Data.Express.Express.Express h, Conjure.Conjurable.Conjurable i, Test.LeanCheck.Core.Listable i, GHC.Show.Show i, Data.Express.Express.Express i) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f, g, h, i) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Data.Express.Express.Express d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Data.Express.Express.Express e, Conjure.Conjurable.Conjurable f, Test.LeanCheck.Core.Listable f, GHC.Show.Show f, Data.Express.Express.Express f, Conjure.Conjurable.Conjurable g, Test.LeanCheck.Core.Listable g, GHC.Show.Show g, Data.Express.Express.Express g, Conjure.Conjurable.Conjurable h, Test.LeanCheck.Core.Listable h, GHC.Show.Show h, Data.Express.Express.Express h, Conjure.Conjurable.Conjurable i, Test.LeanCheck.Core.Listable i, GHC.Show.Show i, Data.Express.Express.Express i, Conjure.Conjurable.Conjurable j, Test.LeanCheck.Core.Listable j, GHC.Show.Show j, Data.Express.Express.Express j) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f, g, h, i, j) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Data.Express.Express.Express d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Data.Express.Express.Express e, Conjure.Conjurable.Conjurable f, Test.LeanCheck.Core.Listable f, GHC.Show.Show f, Data.Express.Express.Express f, Conjure.Conjurable.Conjurable g, Test.LeanCheck.Core.Listable g, GHC.Show.Show g, Data.Express.Express.Express g, Conjure.Conjurable.Conjurable h, Test.LeanCheck.Core.Listable h, GHC.Show.Show h, Data.Express.Express.Express h, Conjure.Conjurable.Conjurable i, Test.LeanCheck.Core.Listable i, GHC.Show.Show i, Data.Express.Express.Express i, Conjure.Conjurable.Conjurable j, Test.LeanCheck.Core.Listable j, GHC.Show.Show j, Data.Express.Express.Express j, Conjure.Conjurable.Conjurable k, Test.LeanCheck.Core.Listable k, GHC.Show.Show k, Data.Express.Express.Express k) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f, g, h, i, j, k) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Data.Express.Express.Express a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Data.Express.Express.Express b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Data.Express.Express.Express c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Data.Express.Express.Express d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Data.Express.Express.Express e, Conjure.Conjurable.Conjurable f, Test.LeanCheck.Core.Listable f, GHC.Show.Show f, Data.Express.Express.Express f, Conjure.Conjurable.Conjurable g, Test.LeanCheck.Core.Listable g, GHC.Show.Show g, Data.Express.Express.Express g, Conjure.Conjurable.Conjurable h, Test.LeanCheck.Core.Listable h, GHC.Show.Show h, Data.Express.Express.Express h, Conjure.Conjurable.Conjurable i, Test.LeanCheck.Core.Listable i, GHC.Show.Show i, Data.Express.Express.Express i, Conjure.Conjurable.Conjurable j, Test.LeanCheck.Core.Listable j, GHC.Show.Show j, Data.Express.Express.Express j, Conjure.Conjurable.Conjurable k, Test.LeanCheck.Core.Listable k, GHC.Show.Show k, Data.Express.Express.Express k, Conjure.Conjurable.Conjurable l, Test.LeanCheck.Core.Listable l, GHC.Show.Show l, Data.Express.Express.Express l) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f, g, h, i, j, k, l) instance Data.Express.Name.Name Test.LeanCheck.Utils.Types.A instance Data.Express.Name.Name Test.LeanCheck.Utils.Types.B instance Data.Express.Name.Name Test.LeanCheck.Utils.Types.C instance Data.Express.Name.Name Test.LeanCheck.Utils.Types.D instance Data.Express.Name.Name Test.LeanCheck.Utils.Types.E instance Data.Express.Name.Name Test.LeanCheck.Utils.Types.F -- | This module is part of Conjure. -- -- This defines functions that deal with recursive descent and -- deconstructions module Conjure.Red -- | Checks if an expression is a deconstruction. -- -- There should be a single hole in the expression. -- -- It should decrease the size of all arguments that have a size greater -- than 0. conjureIsDeconstruction :: Conjurable f => f -> Int -> Expr -> Bool -- | Returns whether a non-empty subset of arguments descends arguments by -- deconstruction. -- --

--   > descends isDec (xxs -++- yys) (xxs -++- tail' yys)
--   True
--

-- --

--   > descends isDec (xxs -++- yys) (xxs -++- yys)
--   False
--

-- --

--   > descends isDec (xxs -++- yys) (head' xxs -:- tail xxs  -++-  head' yys -:- tail yys)
--   False
--

descends :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool -- | Compute candidate deconstructions from an Expr. -- -- This is used in the implementation of candidateDefnsC followed -- by conjureIsDeconstruction. -- --

--   > candidateDeconstructionsFrom (xx `mod'` yy)
--   [ _ `mod` y
--   , x `mod` _
--   ]
--

-- -- To be constrasted with candidateDeconstructionsFromHoled. candidateDeconstructionsFrom :: Expr -> [Expr] -- | Compute candidate deconstructions from an Expr. -- -- This is used in the implementation of candidateExprs followed -- by conjureIsDeconstruction. -- -- This is similar to canonicalVariations but always leaves a hole -- of the same return type as the given expression. -- --

--   > candidateDeconstructionsFrom (i_ `mod'` i_)
--   [ _ `mod` x
--   , x `mod` _
--   ]
--

-- -- To be contrasted with candidateDeconstructionsFrom candidateDeconstructionsFromHoled :: Expr -> [Expr] -- | This module is part of Conjure. -- -- The Prim type and utilities involving it. -- -- You are probably better off importing Conjure. module Conjure.Prim -- | A primtive expression (paired with instance reification). type Prim = (Expr, Reification) -- | Provides a primitive value to Conjure. To be used on values that are -- not Show instances such as functions. (cf. pr) prim :: Conjurable a => String -> a -> Prim -- | Provides a primitive value to Conjure. To be used on Show -- instances. (cf. prim) pr :: (Conjurable a, Show a) => a -> Prim -- | Provides an if condition bound to the given return type. prif :: Conjurable a => a -> Prim -- | Provides a case condition bound to the given return type. primOrdCaseFor :: Conjurable a => a -> Prim -- | Computes a list of holes encoded as Exprs from a list of -- Prims. -- -- This function mirrors functionality from conjureHoles. cjHoles :: [Prim] -> [Expr] -- | Given a list of Prims, returns a function that given an -- Expr will return tiers of test Expr values. -- -- This is used in cjAreEqual. cjTiersFor :: [Prim] -> Expr -> [[Expr]] -- | Given a list of Prims, computes a function that checks whether -- two Exprs are equal up to a given number of tests. cjAreEqual :: [Prim] -> Int -> Expr -> Expr -> Bool -- | Computes a function that equates two Exprs from a list of -- Prims. -- -- This function mirrors functionality from conjureMkEquation. cjMkEquation :: [Prim] -> Expr -> Expr -> Expr -- | This module is part of Conjure. -- -- This module exports functions that test Defns using ground -- values. -- -- You are probably better off importing Conjure. module Conjure.Defn.Test equalModuloTesting :: Conjurable f => Int -> Int -> String -> f -> Defn -> Defn -> Bool -- | For debugging purposes. -- -- This may be taken out of the API at any moment. erroneousCandidate :: Conjurable f => Int -> Int -> String -> f -> Defn -> Bool -- | For debugging purposes, finds a set of arguments that triggers an -- error in the candidate Defn. -- -- Warning: this is an experimental function which may be taken out of -- the API at any moment. findDefnError :: Conjurable f => Int -> Int -> String -> f -> Defn -> Maybe Expr listDefnErrors :: Conjurable f => Int -> Int -> String -> f -> Defn -> [Expr] -- | An internal module of Conjure, a library for Conjuring function -- implementations from tests or partial definitions. (a.k.a.: functional -- inductive programming) module Conjure.Engine -- | 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. conjure :: Conjurable f => 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 [...]
--

conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO () -- | Arguments to be passed to conjureWith or conjpureWith. -- See args for the defaults. data Args Args :: Int -> Int -> Int -> Int -> Int -> Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Args -- | maximum number of tests to each candidate [maxTests] :: Args -> Int -- | maximum size of candidate bodies [maxSize] :: Args -> Int -- | maximum number of recursive evaluations when testing candidates [maxEvalRecursions] :: Args -> Int -- | maximum size of equation operands [maxEquationSize] :: Args -> Int -- | maximum number of tests to search for defined values [maxSearchTests] :: Args -> Int -- | maximum size of deconstructions (e.g.: _ - 1) [maxDeconstructionSize] :: Args -> Int -- | require recursive calls to deconstruct arguments [requireDescent] :: Args -> Bool -- | use pattern matching to create (recursive) candidates [usePatterns] :: Args -> Bool -- | copy partial definition bindings in candidates [copyBindings] :: Args -> Bool -- | restrict constant/ground numeric expressions to atoms [atomicNumbers] :: Args -> Bool -- | show theory discovered by Speculate used in pruning [showTheory] :: Args -> Bool -- | unique-modulo-testing candidates [uniqueCandidates] :: Args -> Bool -- | 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

args :: Args -- | Like conjure but allows setting options through -- Args/args. -- --

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

conjureWith :: Conjurable f => Args -> String -> f -> [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
--

conjureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> IO () -- | Like conjureFromSpec but allows setting options through -- Args/args. -- --

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

conjureFromSpecWith :: Conjurable f => Args -> String -> (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. conjure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> IO () -- | Like conjure0 but allows setting options through -- Args/args. conjure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> IO () -- | Like conjure but in the pure world. -- -- Returns a quadruple with: -- --

tiers of implementations
tiers of candidates
a list of tests
the underlying theory

conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) -- | Like conjpure but allows setting options through Args -- and args. conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) -- | Like conjureFromSpec but in the pure world. (cf. -- conjpure) conjpureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) -- | Like conjureFromSpecWith but in the pure world. (cf. -- conjpure) conjpureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) -- | Like conjure0 but in the pure world. (cf. conjpure) conjpure0 :: Conjurable f => 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. conjpure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) -- | Return apparently unique candidate bodies. candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy) -- | Return apparently unique candidate definitions. candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy) -- | Return apparently unique candidate definitions where there is a single -- body. candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy) -- | Return apparently unique candidate definitions using pattern matching. candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy) -- | Just prints the underlying theory found by Test.Speculate -- without actually synthesizing a function. conjureTheory :: Conjurable f => String -> f -> [Prim] -> IO () -- | Like conjureTheory but allows setting options through -- Args/args. conjureTheoryWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO () -- | 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''", ...]
--

class () => Name a -- | 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"
--

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

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

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

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

foldr' :: Expr -> 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
--

fill :: Expr -> [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]
--

fold :: [Expr] -> Expr -- | 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
--

evaluate :: Typeable a => Expr -> Maybe a -- | 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]
--

unfold :: Expr -> [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. cons :: Expr -- | The function div for the Int type lifted over the -- Expr type. (See also mod.) -- --

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

div' :: 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
--

mod' :: Expr -> Expr -> Expr -- | Lists valid applications between lists of Exprs -- --

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

(>$$<) :: [Expr] -> [Expr] -> [Expr] -- | 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
--

size :: Expr -> Int -- | 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]
--

value :: Typeable a => String -> a -> Expr -- | The operator * for the Int type. (See also -*-.) -- --

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

-- --

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

-- --

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

times :: Expr -- | 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'
--

typ :: Expr -> TypeRep -- | 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
--

arity :: Expr -> Int -- | Function composition encoded as an Expr: -- --

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

compose :: 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]
--

unit :: Expr -> Expr -- | The value 0 bound to the Int type encoded as an -- Expr. -- --

--   > zero
--   0 :: Int
--

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

match :: Expr -> Expr -> Maybe [(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
--

canonicalize :: 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
--

--   > 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
--   ]
--

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

-- --

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

-- --

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

variableNamesFromTemplate :: String -> [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''", ...]
--

names :: Name a => a -> [String] -- | 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
--

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

val :: (Typeable a, Show a) => a -> 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
--

($$) :: Expr -> Expr -> Maybe 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]
--

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

etyp :: Expr -> Either (TypeRep, TypeRep) 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
--

mtyp :: Expr -> Maybe TypeRep -- | 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
--

isIllTyped :: 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
--

isWellTyped :: 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
--

isFun :: Expr -> Bool -- | 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
--

eval :: Typeable a => 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
--

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

toDynamic :: Expr -> Maybe Dynamic -- | 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)"
--

showOpExpr :: String -> Expr -> String -- | O(n). Like showExpr but allows specifying the -- surrounding precedence. -- --

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

-- --

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

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

-- --

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

e1 is smaller in size/length than e2, e.g.: x + -- y < x + (y + z);
or, e1 has more distinct variables than e2, e.g.: -- x + y < x + x;
or, e1 has more variable occurrences than e2, e.g.: -- x + x < 1 + x;
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
--

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

--   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]
--

unfoldApp :: Expr -> [Expr] -- | 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
--

hasVar :: 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
--

isGround :: 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
--

isConst :: 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
--

isVar :: 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
```

isValue :: 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 (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 (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
--   ]
--

--   > 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
--   ]
--

values :: 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
--   ]
--

--   > 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
--   ]
--

consts :: 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
--   ]
--

--   > 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]
--

vars :: 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]
--

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

--   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. height :: Expr -> Int -- | 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
--

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

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

-- --

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

-- --

--   > xx `isSubexprOf` yy
--   False
--

isSubexprOf :: Expr -> Expr -> Bool -- | 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
--

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

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

--   > 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). (//-) :: Expr -> [(Expr, 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! renameVarsBy :: (String -> 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
--

varAsTypeOf :: String -> 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
--

holeAsTypeOf :: Expr -> 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
--

hole :: Typeable a => a -> Expr -- | 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
--

isHole :: Expr -> Bool -- | 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]
--

holes :: 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]
--

--   > hasHole $ hole (undefined :: Bool)
--   True
--

-- --

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

-- --

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

hasHole :: 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
--

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

listVars :: Typeable a => String -> a -> [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
--   , ...
--   ]
--

listVarsAsTypeOf :: String -> 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)
--

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

foldPair :: (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 (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)
--

foldTrio :: (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)
--

--   > [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]
--

($$<) :: Expr -> [Expr] -> [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 (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 ]
--

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

-- --

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

reifyName :: (Typeable a, Name a) => a -> [Expr] -- | O(1). Builds a reified Eq instance from the given -- == function. (cf. reifyEq) -- --

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

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

-- --

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

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

-- --

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

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

-- --

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

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

-- --

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

--   > 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"
--

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

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

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

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

--   > 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]
--

--   > b_
--   _ :: Bool
--

b_ :: Expr -- | Expr representing a variable p :: Bool. -- --

--   > pp
--   p :: Bool
--

pp :: Expr -- | Expr representing a variable q :: Bool. -- --

--   > qq
--   q :: Bool
--

qq :: Expr -- | Expr representing a variable r :: Bool. -- --

--   > rr
--   r :: Bool
--

rr :: Expr -- | Expr representing a variable p' :: Bool. -- --

--   > pp'
--   p' :: Bool
--

pp' :: Expr -- | False encoded as an Expr. -- --

--   > false
--   False :: Bool
--

false :: Expr -- | True encoded as an Expr. -- --

--   > true
--   True :: Bool
--

true :: Expr -- | The function not encoded as an Expr. -- --

--   > notE
--   not :: Bool -> Bool
--

notE :: Expr -- | The function and encoded as an Expr. -- --

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

andE :: Expr -- | The function or encoded as an Expr. -- --

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

orE :: Expr -- | The function ==> lifted over Exprs. -- --

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

-- --

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

(-==>-) :: Expr -> Expr -> Expr infixr 0 -==>- -- | The ==> operator encoded as an Expr implies :: Expr -- | The function not lifted over the Expr type. -- --

--   > not' false
--   not False :: Bool
--

-- --

--   > evalBool $ not' false
--   True
--

-- --

--   > not' pp
--   not p :: Bool
--

not' :: Expr -> Expr -- | 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 3 -&&- -- | The function || lifted over the Expr type. -- --

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

-- --

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

-- --

--   > evalBool $ false -||- true
--   True
--

(-||-) :: Expr -> Expr -> Expr infixr 2 -||- -- | A typed hole of Int type. -- --

--   > i_
--   _ :: Int
--

i_ :: Expr -- | A variable x of Int type. -- --

--   > xx
--   x :: Int
--

xx :: Expr -- | A variable y of Int type. -- --

--   > yy
--   y :: Int
--

yy :: Expr -- | A variable z of Int type. -- --

--   > zz
--   z :: Int
--

zz :: Expr -- | A variable x' of Int type. -- --

--   > xx'
--   x' :: Int
--

xx' :: Expr -- | A variable i of Int type. -- --

--   > ii
--   i :: Int
--

ii :: Expr -- | A variable j of Int type. -- --

--   > jj
--   j :: Int
--

jj :: Expr -- | A variable k of Int type. -- --

--   > kk
--   k :: Int
--

kk :: Expr -- | A variable i' of Int type. -- --

--   > ii'
--   i' :: Int
--

ii' :: Expr -- | A variable l of Int type. -- --

--   > ll
--   l :: Int
--

ll :: Expr -- | A variable m of Int type. -- --

--   > mm
--   m :: Int
--

mm :: Expr -- | A variable n of Int type. -- --

--   > nn
--   n :: Int
--

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

--   > one
--   1 :: Int
--

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

--   > two
--   2 :: Int
--

two :: Expr -- | The value 3 bound to the Int type encoded as an -- Expr. -- --

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

three :: Expr -- | The value 4 bound to the Int type encoded as an -- Expr. -- --

--   > four
--   4 :: Int
--

four :: Expr -- | The value 5 bound to the Int type encoded as an -- Expr. -- --

--   > five
--   5 :: Int
--

five :: Expr -- | The value 6 bound to the Int type encoded as an -- Expr. -- --

--   > six
--   6 :: Int
--

six :: Expr -- | The value 7 bound to the Int type encoded as an -- Expr. -- --

--   > seven
--   7 :: Int
--

seven :: Expr -- | The value 8 bound to the Int type encoded as an -- Expr. -- --

--   > eight
--   8 :: Int
--

eight :: Expr -- | The value 9 bound to the Int type encoded as an -- Expr. -- --

--   > nine
--   9 :: Int
--

nine :: Expr -- | The value 10 bound to the Int type encoded as an -- Expr. -- --

--   > ten
--   10 :: Int
--

ten :: Expr -- | The value 11 bound to the Int type encoded as an -- Expr. -- --

--   > eleven
--   11 :: Int
--

eleven :: Expr -- | The value 12 bound to the Int type encoded as an -- Expr. -- --

--   > twelve
--   12 :: Int
--

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

--   > minusOne
--   -1 :: Int
--

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

--   > minusOne
--   -2 :: Int
--

minusTwo :: 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
--

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

--   > ffE
--   f :: Int -> Int
--

ffE :: 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
--

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

--   > ggE
--   g :: Int -> Int
--

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

--   > hh zz
--   h z :: Int
--

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

--   > hhE
--   h :: Int -> Int
--

hhE :: 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
--

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

-- --

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

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

-- --

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

--   > 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]
--

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

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

-- --

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

question :: 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]
--

oo :: Expr -> Expr -> 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
--

ooE :: Expr -- | 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
--

(-+-) :: Expr -> Expr -> Expr infixl 6 -+- -- | The operator + for the Int type. (See also -+-.) -- --

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

-- --

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

-- --

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

plus :: Expr -- | 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
--

(-*-) :: Expr -> Expr -> Expr infixl 7 -*- -- | The subtraction - operator encoded as an Expr. -- --

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

-- --

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

minus :: Expr -- | Integer division div encoded as an Expr. -- --

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

-- --

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

divE :: Expr -- | Integer modulo mod encoded as an Expr. -- --

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

-- --

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

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

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

quot' :: Expr -> Expr -> Expr -- | Integer quotient quot encoded as an Expr. -- --

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

-- --

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

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

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

rem' :: Expr -> Expr -> Expr -- | Integer remainder rem encoded as an Expr. -- --

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

-- --

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

remE :: 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
--

id' :: Expr -> 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
--

--   > const' zero one
--   const 0 1 :: Int
--

-- -- This works for the argument types Int, Char, Bool -- and their lists. const' :: Expr -> Expr -> Expr -- | negate over the Int type lifted over the Expr -- type. -- --

--   > negate' xx
--   negate x :: Int
--

-- --

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

negate' :: Expr -> Expr -- | negate over the Int type encoded as an Expr -- --

--   > negateE
--   negate :: Int -> Int
--

negateE :: Expr -- | abs over the Int type lifted over the Expr type. -- --

--   > abs' xx'
--   abs x' :: Int
--

-- --

--   > evl (abs' minusTwo) :: Int
--   2
--

abs' :: Expr -> Expr -- | abs over the Int type encoded as an Expr. -- --

--   > absE
--   abs :: Int -> Int
--

absE :: Expr -- | signum over the Int type lifted over the Expr -- type. -- --

--   > signum' xx'
--   signum x' :: Int
--

-- --

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

signum' :: Expr -> Expr -- | signum over the Int type encoded as an Expr. -- --

--   > signumE
--   signum :: Int -> Int
--

signumE :: Expr -- | odd with an Int argument lifted over the Expr -- type. -- --

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

-- --

--   > evl (odd' two) :: Bool
--   False
--

odd' :: Expr -> Expr -- | even with an Int argument lifted over the Expr -- type. -- --

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

-- --

--   > evl (even' two) :: Bool
--   True
--

even' :: Expr -> Expr -- | A hole of Char type encoded as an Expr. -- --

--   > c_
--   _ :: Char
--

c_ :: Expr -- | A hole of String type encoded as an Expr. -- --

--   > cs_
--   _ :: [Char]
--

cs_ :: Expr -- | A variable named c of type Char encoded as an -- Expr. -- --

--   > cc
--   c :: Char
--

cc :: Expr -- | A variable named c of type Char encoded as an -- Expr. -- --

--   > dd
--   d :: Char
--

dd :: Expr -- | A variable named cs of type String encoded as an -- Expr. -- --

--   > ccs
--   cs :: [Char]
--

ccs :: Expr -- | The character 'a' encoded as an Expr. -- --

--   > ae
--   'a' :: Char
--

-- --

--   > evl ae :: Char
--   'a'
--

ae :: Expr -- | The character 'b' encoded as an Expr -- --

--   > bee
--   'b' :: Char
--

-- --

--   > evl bee :: Char
--   'b'
--

bee :: Expr -- | The character 'c' encoded as an Expr -- --

--   > cee
--   'c' :: Char
--

-- --

--   > evl cee :: Char
--   'c'
--

cee :: Expr -- | The character 'd' encoded as an Expr -- --

--   > dee
--   'd' :: Char
--

-- --

--   > evl dee :: Char
--   'd'
--

dee :: Expr -- | The character 'z' encoded as an Expr -- --

--   > zed
--   'z' :: Char
--

-- --

--   > evl zed :: Char
--   'z'
--

-- -- (cf. zee) zed :: Expr -- | The character 'z' encoded as an Expr -- --

--   > zee
--   'z' :: Char
--

-- --

--   > evl zee :: Char
--   'z'
--

-- -- (cf. zed) zee :: Expr -- | The space character encoded as an Expr -- --

--   > space
--   ' ' :: Char
--

space :: Expr -- | The line break character encoded as an Expr -- --

--   > lineBreak
--   '\n' :: Char
--

lineBreak :: Expr -- | The ord function lifted over Expr -- --

--   > ord' bee
--   ord 'b' :: Int
--

-- --

--   > evl (ord' bee)
--   98
--

ord' :: Expr -> Expr -- | The ord function encoded as an Expr ordE :: Expr -- | A typed hole of [Int] type encoded as an Expr. -- --

--   > is_
--   _ :: [Int]
--

is_ :: Expr -- | A variable named xs of type [Int] encoded as an -- Expr. -- --

--   > xxs
--   xs :: [Int]
--

xxs :: Expr -- | A variable named ys of type [Int] encoded as an -- Expr. -- --

--   > yys
--   ys :: [Int]
--

yys :: Expr -- | A variable named zs of type [Int] encoded as an -- Expr. -- --

--   > yys
--   ys :: [Int]
--

zzs :: Expr -- | An empty list of type [Int] encoded as an Expr. -- --

--   > nil
--   [] :: [Int]
--

nil :: Expr -- | An empty String encoded as an Expr. -- --

--   > emptyString
--   "" :: String
--

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

-- --

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

-- --

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

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

-- --

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

(-++-) :: Expr -> Expr -> Expr infixr 5 -++- -- | 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
--

head' :: 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]
--

tail' :: 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
--

null' :: 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
--

length' :: 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]
--

init' :: 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]
--

sort' :: 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]
--

insert' :: 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
--

elem' :: 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]
--

drop' :: 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]
--

take' :: Expr -> Expr -> Expr -- | $ lifted over Exprs -- --

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

-- -- Works for Int, Bool, Char argument types and -- their lists. (-$-) :: Expr -> Expr -> Expr infixl 6 -$- -- | 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' 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 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'
--

--   > 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'
--

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

-- --

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

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

just :: Expr -> Expr -- | An infix synonym of pair. -- --

--   > zero -|- xxs
--

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

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

(-|-) :: 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
--

--   > bs_
--   _ :: [Bool]
--

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

--   > pps
--   ps :: [Bool]
--

pps :: Expr -- | A typed hole of '[Bool]' type -- --

--   > qqs
--   qs :: [Bool]
--

qqs :: Expr -- | and lifted over the Expr type. -- --

--   > and' pps
--   and ps :: Bool
--

-- --

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

and' :: Expr -> Expr -- | or lifted over the Expr type. -- --

--   > or' pps
--   or ps :: Bool
--

-- --

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

or' :: 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
--

sum' :: 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
--

product' :: 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. (-.-) :: Expr -> Expr -> Expr -- | map over the Int element type encoded as an Expr -- --

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

mapE :: Expr -- | map lifted over Exprs. -- --

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

map' :: Expr -> Expr -> Expr -- | filter lifted over Exprs. -- --

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

filter' :: Expr -> Expr -> Expr -- | enumFrom lifted over Exprs. -- --

--   > enumFrom' zero
--   enumFrom 0 :: [Int]
--

-- -- Works for Ints, Bools and Chars. enumFrom' :: Expr -> Expr -- | enumFrom lifted over Exprs named as ".." for -- pretty-printing. -- --

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

-- -- Works for Ints, Bools and Chars. (-..) :: Expr -> () -> Expr -- | enumFromTo lifted over Exprs -- --

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

enumFromTo' :: Expr -> Expr -> Expr -- | enumFromTo lifted over Exprs but named as ".." -- for pretty-printing. -- --

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

(-..-) :: Expr -> Expr -> Expr -- | enumFromThen lifted over Exprs -- --

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

enumFromThen' :: Expr -> Expr -> Expr -- | enumFromThen lifted over Exprs but named as -- ",.." for pretty printing. -- --

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

(--..) :: (Expr, Expr) -> () -> Expr -- | enumFromThenTo lifted over Exprs. -- --

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

enumFromThenTo' :: Expr -> Expr -> Expr -> Expr -- | enumFromThenTo lifted over Exprs but named as -- ",.." for pretty-printing. -- --

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

(--..-) :: (Expr, Expr) -> Expr -> Expr -- | Allows automatic derivation of Conjurable typeclass instances. module Conjure.Conjurable.Derive -- | Derives an Conjurable instance for the given type Name. -- -- This function needs the TemplateHaskell extension. -- -- If -:, ->:, ->>:, ->>>:, -- ... are not in scope, this will derive them as well. -- -- For now, this function only derives conjureEquality, -- conjureTiers and conjureExpress and does not derive -- conjureSubTypes, conjureArgumentCases and -- conjureSize. These will be added in future versions. If you -- plan to use features that depend on these functionalities, please -- define your instances manually. deriveConjurable :: Name -> DecsQ -- | Derives a Conjurable instance for a given type Name -- cascading derivation of type arguments as well. -- -- For now, this function only derives conjureEquality, -- conjureTiers and conjureExpress and does not derive -- conjureSubTypes, conjureArgumentCases and -- conjureSize. These will be added in future versions. If you -- plan to use features that depend on these functionalities, please -- define your instances manually. deriveConjurableCascading :: Name -> DecsQ -- | Same as deriveConjurable but does not warn when instance -- already exists (deriveConjurable is preferable). -- -- For now, this function only derives conjureEquality, -- conjureTiers and conjureExpress and does not derive -- conjureSubTypes, conjureArgumentCases and -- conjureSize. These will be added in future versions. If you -- plan to use features that depend on these functionalities, please -- define your instances manually. deriveConjurableIfNeeded :: Name -> DecsQ -- | A library for Conjuring function implementations from tests or partial -- definitions. (a.k.a.: functional inductive programming) -- -- This is currently an experimental tool in its early stages, don't -- expect much from its current version. It is just a piece of curiosity -- in its current state. -- -- Step 1: declare your partial function -- --

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

-- -- Step 2: declare a list with the potential building blocks: -- --

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

-- -- Step 3: call conjure and see your generated function: -- --

--   > conjure "square" square primitives
--   square :: Int -> Int
--   -- testing 3 combinations of argument values
--   -- 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
--

module Conjure -- | 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. conjure :: Conjurable f => String -> f -> [Prim] -> IO () -- | A primtive expression (paired with instance reification). type Prim = (Expr, Reification) -- | Provides a primitive value to Conjure. To be used on Show -- instances. (cf. prim) pr :: (Conjurable a, Show a) => a -> Prim -- | Provides a primitive value to Conjure. To be used on values that are -- not Show instances such as functions. (cf. pr) prim :: Conjurable a => String -> a -> Prim -- | Provides an if condition bound to the given return type. prif :: Conjurable a => a -> Prim -- | Provides a case condition bound to the given return type. primOrdCaseFor :: Conjurable a => a -> Prim -- | Like conjure but allows setting the maximum size of considered -- expressions instead of the default value of 12. -- --

--   conjureWithMaxSize 10 "function" function [...]
--

conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO () -- | Like conjure but allows setting options through -- Args/args. -- --

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

conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO () -- | Arguments to be passed to conjureWith or conjpureWith. -- See args for the defaults. data Args Args :: Int -> Int -> Int -> Int -> Int -> Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Args -- | maximum number of tests to each candidate [maxTests] :: Args -> Int -- | maximum size of candidate bodies [maxSize] :: Args -> Int -- | maximum number of recursive evaluations when testing candidates [maxEvalRecursions] :: Args -> Int -- | maximum size of equation operands [maxEquationSize] :: Args -> Int -- | maximum number of tests to search for defined values [maxSearchTests] :: Args -> Int -- | maximum size of deconstructions (e.g.: _ - 1) [maxDeconstructionSize] :: Args -> Int -- | require recursive calls to deconstruct arguments [requireDescent] :: Args -> Bool -- | use pattern matching to create (recursive) candidates [usePatterns] :: Args -> Bool -- | copy partial definition bindings in candidates [copyBindings] :: Args -> Bool -- | restrict constant/ground numeric expressions to atoms [atomicNumbers] :: Args -> Bool -- | show theory discovered by Speculate used in pruning [showTheory] :: Args -> Bool -- | unique-modulo-testing candidates [uniqueCandidates] :: Args -> Bool -- | 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

args :: Args -- | 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"
--

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

val :: (Typeable a, Show a) => 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]
--

value :: Typeable a => String -> a -> Expr -- | 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
--

conjureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> IO () -- | Like conjureFromSpec but allows setting options through -- Args/args. -- --

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

conjureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> IO () -- | Class of Conjurable types. Functions are Conjurable if -- all their arguments are Conjurable, Listable and -- Showable. -- -- For atomic types that are Listable, instances are defined as: -- --

--   instance Conjurable Atomic where
--     conjureTiers  =  reifyTiers
--

-- -- For atomic types that are both Listable and Eq, -- instances are defined as: -- --

--   instance Conjurable Atomic where
--     conjureTiers     =  reifyTiers
--     conjureEquality  =  reifyEquality
--

-- -- For types with subtypes, instances are defined as: -- --

--   instance Conjurable Composite where
--     conjureTiers     =  reifyTiers
--     conjureEquality  =  reifyEquality
--     conjureSubTypes x  =  conjureType y
--                        .  conjureType z
--                        .  conjureType w
--       where
--       (Composite ... y ... z ... w ...)  =  x
--

-- -- Above x, y, z and w are just -- proxies. The Proxy type was avoided for backwards -- compatibility. -- -- Please see the source code of Conjure.Conjurable for more -- examples. -- -- (cf. reifyTiers, reifyEquality, conjureType) class (Typeable a, Name a) => Conjurable a -- | Returns Just the == function encoded as an Expr -- when available or Nothing otherwise. -- -- Use reifyEquality when defining this. conjureEquality :: Conjurable a => a -> Maybe Expr -- | Returns Just tiers of values encoded as Exprs -- when possible or Nothing otherwise. -- -- Use reifyTiers when defining this. conjureTiers :: Conjurable a => a -> Maybe [[Expr]] conjureSubTypes :: Conjurable a => a -> Reification -- | Returns a top-level case breakdown. conjureCases :: Conjurable a => a -> [Expr] -- | Returns the (recursive) size of the given value. conjureSize :: Conjurable a => a -> Int -- | Returns a function that deeply reencodes an expression when possible. -- (id when not available.) -- -- Use reifyExpress when defining this. conjureExpress :: Conjurable a => a -> Expr -> Expr -- | Reifies the expr function in a Conjurable type instance. -- -- This is to be used in the definition of conjureExpress of -- Conjurable typeclass instances. -- --

--   instance ... => Conjurable <Type> where
--     ...
--     conjureExpress  =  reifyExpress
--     ...
--

reifyExpress :: (Express a, Show a) => a -> Expr -> Expr -- | Reifies equality == in a Conjurable type instance. -- -- This is to be used in the definition of conjureEquality of -- Conjurable typeclass instances: -- --

--   instance ... => Conjurable <Type> where
--     ...
--     conjureEquality  =  reifyEquality
--     ...
--

reifyEquality :: (Eq a, Typeable a) => a -> Maybe Expr -- | Reifies equality to be used in a conjurable type. -- -- This is to be used in the definition of conjureTiers of -- Conjurable typeclass instances: -- --

--   instance ... => Conjurable <Type> where
--     ...
--     conjureTiers  =  reifyTiers
--     ...
--

reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]] -- | To be used in the implementation of conjureSubTypes. -- --

--   instance ... => Conjurable <Type> where
--     ...
--     conjureSubTypes x  =  conjureType (field1 x)
--                        .  conjureType (field2 x)
--                        .  ...
--                        .  conjureType (fieldN x)
--     ...
--

conjureType :: Conjurable a => a -> Reification -- | 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''", ...]
--

class () => Name a -- | 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"
--

name :: Name a => a -> String -- | 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.

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

tiers of implementations
tiers of candidates
a list of tests
the underlying theory

--   take :: Int -> [a] -> [a]
--   sort :: Ord a => [a] -> [a]
--

-- -- by binding them to the following types: -- --

--   take :: Int -> [A] -> [A]
--   sort :: [A] -> [A]
--

--   map :: (a -> b) -> [a] -> [b]
--   foldr :: (a -> b -> b) -> b -> [a] -> b
--

-- -- by binding them to the following types: -- --

--   map :: (A -> B) -> [A] -> [B]
--   foldr :: (A -> B -> B) -> B -> [A] -> B
--

--   uncurry :: (a -> b -> c) -> (a, b) -> c
--   zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
--

-- -- by binding them to the following types: -- --

--   uncurry :: (A -> B -> C) -> (A, B) -> C
--   zipWith :: (A -> B -> C) -> [A] -> [B] -> [C]
--