-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | conjure Haskell functions out of partial definitions -- -- Conjure is a tool that produces Haskell functions out of partial -- definitions. -- -- 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. @package code-conjure @version 0.0.2 -- | Some type binding operators that are useful when defining -- Conjurable instances. module Conjure.TypeBinding arg1 :: (a -> b) -> a arg2 :: (a -> b -> c) -> b arg3 :: (a -> b -> c -> d) -> c arg4 :: (a -> b -> c -> d -> e) -> d arg5 :: (a -> b -> c -> d -> e -> f) -> e arg6 :: (a -> b -> c -> d -> e -> f -> g) -> f (==:) :: (a -> b -> c -> d) -> a -> b argTy1of1 :: con a -> a argTy1of2 :: con a b -> a argTy2of2 :: con a b -> b argTy1of3 :: con a b c -> a argTy2of3 :: con a b c -> b argTy3of3 :: con a b c -> c argTy1of4 :: con a b c d -> a argTy2of4 :: con a b c d -> b argTy3of4 :: con a b c d -> c argTy4of4 :: con a b c d -> d argTy1of5 :: con a b c d e -> a argTy2of5 :: con a b c d e -> b argTy3of5 :: con a b c d e -> c argTy4of5 :: con a b c d e -> d argTy5of5 :: con a b c d e -> e argTy1of6 :: con a b c d e f -> a argTy2of6 :: con a b c d e f -> b argTy3of6 :: con a b c d e f -> c argTy4of6 :: con a b c d e f -> d argTy5of6 :: con a b c d e f -> e argTy6of6 :: con a b c d e f -> f -- | An internal module of Conjure. This exports List, -- Maybe, Function and a few other simple utitilites. module Conjure.Utils count :: (a -> Bool) -> [a] -> Int fromLeft :: Either a b -> a fromRight :: Either a b -> b elemBy :: (a -> a -> Bool) -> a -> [a] -> Bool listEq :: (a -> a -> Bool) -> [a] -> [a] -> Bool listOrd :: (a -> a -> Bool) -> [a] -> [a] -> Bool maybeEq :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool maybeOrd :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool eitherEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool eitherOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool pairEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool pairOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool tripleEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (a, b, c) -> (a, b, c) -> Bool tripleOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (a, b, c) -> (a, b, c) -> Bool quadrupleEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (a, b, c, d) -> (a, b, c, d) -> Bool quadrupleOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (a, b, c, d) -> (a, b, c, d) -> Bool -- | This internal module reexports Express along with a few other -- utilities. module Conjure.Expr sixtuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr quintuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr quadruple :: Expr -> Expr -> Expr -> Expr -> Expr triple :: Expr -> Expr -> Expr -> Expr comma :: Expr pair :: Expr -> Expr -> Expr (-|-) :: Expr -> Expr -> Expr just :: Expr -> Expr justBool :: Expr justInt :: Expr nothingBool :: Expr nothingInt :: Expr nothing :: Expr compare' :: Expr -> Expr -> Expr -- | A virtual function if :: Bool -> a -> a -> a lifted -- over the Expr type. This is 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 (-<-) :: Expr -> Expr -> Expr infix 4 -<- (-<=-) :: Expr -> Expr -> Expr infix 4 -<=- (-/=-) :: Expr -> Expr -> Expr infix 4 -/=- (-$-) :: Expr -> Expr -> Expr infixl 6 -$- elem' :: Expr -> Expr -> Expr insert' :: Expr -> Expr -> Expr sort' :: 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 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 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 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 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 -++- -- | 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 -:- -- | 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 list constructor : encoded as an Expr. consChar :: Expr -- | The list constructor : encoded as an Expr. consBool :: Expr -- | The list constructor : encoded as an Expr. consInt :: 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 empty list '[]' encoded as an Expr. nilChar :: Expr -- | The empty list '[]' encoded as an Expr. nilBool :: Expr -- | The empty list '[]' encoded as an Expr. nilInt :: Expr -- | An empty String encoded as an Expr. -- --

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

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

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

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

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

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

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

xxs :: Expr -- | A typed hole of [Int] type encoded as an Expr. -- --

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

is_ :: Expr ordE :: Expr ord' :: Expr -> Expr lineBreak :: Expr space :: Expr -- | The character 'd' encoded as an Expr -- --

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

-- --

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

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

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

-- --

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

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

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

-- --

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

bee :: Expr ae :: Expr ccs :: Expr dd :: Expr cc :: Expr -- | A hole of Char type encoded as an Expr. -- --

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

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

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

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

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

-- --

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

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

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

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

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

-- --

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

negate' :: Expr -> Expr const' :: Expr -> Expr -> Expr -- | The function id encoded as an Expr. (cf. id') idString :: Expr -- | The function id encoded as an Expr. (cf. id') idBools :: Expr -- | The function id encoded as an Expr. (cf. id') idInts :: Expr -- | The function id encoded as an Expr. (cf. id') idChar :: Expr -- | The function id encoded as an Expr. (cf. id') idBool :: Expr -- | The function id encoded as an Expr. (cf. id') idInt :: 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 -- | 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 operator * for the Int type. (See also -*-.) -- --

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

-- --

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

-- --

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

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

--   > three -*- three
--   9 :: Int
--

-- --

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

-- --

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

(-*-) :: Expr -> Expr -> Expr infixl 7 -*- -- | 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 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 -+- -- | A variable g of 'Int -> Int' type encoded as an -- Expr. -- --

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

ggE :: 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: (-?-): cannot apply `(?) :: * -> * -> *` to `x :: Int' and `q :: Bool'.  Unhandled types?
--

(-?-) :: Expr -> Expr -> Expr -- | A variable function g of 'Int -> Int' type lifted over the -- Expr type. -- --

--   > gg yy
--   g y :: Int
--

-- --

--   > gg minusTwo
--   gg (-2) :: Int
--

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

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

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

--   > ff xx
--   f x :: Int
--

-- --

--   > ff one
--   f 1 :: Int
--

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

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

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

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

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

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

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

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

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

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

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

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

zero :: Expr ii' :: Expr kk :: Expr jj :: Expr ii :: Expr -- | A variable x' of Int type. -- --

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

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

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

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

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

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

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

xx :: Expr -- | A typed hole of Int type. -- --

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

i_ :: Expr -- | 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 -||- -- | 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 not lifted over the Expr type. -- --

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

-- --

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

-- --

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

not' :: Expr -> Expr implies :: Expr (-==>-) :: Expr -> Expr -> Expr infixr 0 -==>- -- | The function or encoded as an Expr. -- --

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

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

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

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

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

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

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

true :: Expr -- | False encoded as an Expr. -- --

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

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

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

pp' :: Expr -- | Expr representing a variable r :: Bool. -- --

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

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

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

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

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

pp :: Expr -- | Expr representing a hole of Bool type. -- --

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

b_ :: 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 -- | 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 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] -- | 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 -- | 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 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 new -- variables are introduced so name clashes are avoided: -- --

--   > canonicalVariations $ i_ -+- ii -+- jj -+- i_
--   [ x + y + z + x' :: Int
--   , x + y + z + x :: Int ]
--

-- --

--   > canonicalVariations $ ii -+- jj
--   [x + y :: Int]
--

-- --

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

canonicalVariations :: Expr -> [Expr] -- | Returns whether an Expr is canonical: if applying -- canonicalize is an identity using names as provided by -- preludeNameInstances. isCanonical :: 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)] -- | 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 -- | Like isCanonical but allows specifying the list of variable -- names. isCanonicalWith :: (Expr -> [String]) -> Expr -> Bool -- | Like canonicalization but allows customization of the list of -- variable names. (cf. lookupNames, -- variableNamesFromTemplate) canonicalizationWith :: (Expr -> [String]) -> Expr -> [(Expr, Expr)] -- | Like canonicalize but allows customization of the list of -- variable names. (cf. lookupNames, -- variableNamesFromTemplate) -- --

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

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

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

-- --

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

canonicalizeWith :: (Expr -> [String]) -> Expr -> Expr preludeNameInstances :: [Expr] findValidApp :: [Expr] -> Expr -> Maybe Expr validApps :: [Expr] -> Expr -> [Expr] listVarsWith :: [Expr] -> Expr -> [Expr] lookupNames :: [Expr] -> Expr -> [String] lookupName :: [Expr] -> Expr -> String mkComparisonLE :: [Expr] -> Expr -> Expr -> Expr mkComparisonLT :: [Expr] -> Expr -> Expr -> Expr mkEquation :: [Expr] -> Expr -> Expr -> Expr mkComparison :: String -> [Expr] -> Expr -> Expr -> Expr -- | 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). 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 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). 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). 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 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 lookupComparison :: String -> TypeRep -> [Expr] -> Maybe Expr -- | O(1). Builds a reified Name instance from the given -- String and type. (cf. reifyName, mkName) mkNameWith :: Typeable a => String -> a -> [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 Ord instance from the given -- <= function. (cf. reifyOrd, mkOrd) mkOrdLessEqual :: 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 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). 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). Reifies Eq and Ord instances into a list of -- Expr. reifyEqOrd :: (Typeable a, Ord a) => a -> [Expr] -- | O(1). Reifies an Ord instance into a list of -- Exprs. The list will contain compare, <= and -- < for the given type. (cf. mkOrd, -- mkOrdLessEqual, mkComparisonLE, mkComparisonLT) -- --

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

-- --

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

-- --

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

reifyOrd :: (Typeable a, Ord a) => a -> [Expr] -- | O(1). Reifies an Eq instance into a list of -- Exprs. The list will contain == and /= for the -- given type. (cf. mkEq, mkEquation) -- --

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

-- --

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

-- --

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

reifyEq :: (Typeable a, Eq a) => a -> [Expr] -- | 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 -- | Checks if any of the subexpressions of the first argument Expr -- is an instance of the second argument Expr. hasInstanceOf :: Expr -> Expr -> Bool -- | Given two Exprs, checks if the first expression is an instance -- of the second in terms of variables. (cf. 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 -- | 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 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)] -- | Derives a Express instance for a given type Name -- cascading derivation of type arguments as well. deriveExpressCascading :: Name -> DecsQ -- | Same as deriveExpress but does not warn when instance already -- exists (deriveExpress is preferable). deriveExpressIfNeeded :: Name -> DecsQ -- | Derives an Express instance for the given type Name. -- -- This function needs the TemplateHaskell extension. -- -- If -:, ->:, ->>:, ->>>:, -- ... are not in scope, this will derive them as well. deriveExpress :: Name -> DecsQ -- | Express typeclass instances provide an expr function -- that allows values to be deeply encoded as applications of -- Exprs. -- --

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

-- -- The function expr can be contrasted with the function -- val: -- --

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

-- -- Depending on the situation, one or the other may be desirable. -- -- Instances can be automatically derived using the TH function -- deriveExpress. -- -- The following example shows a datatype and its instance: -- --

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

-- --

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

-- -- To declare expr it may be useful to use auxiliary type binding -- operators: -:, ->:, ->>:, -- ->>>:, ->>>>:, -- ->>>>>:, ... -- -- For types with atomic values, just declare expr = val class Typeable a => Express a expr :: Express a => a -> Expr -- | O(n). Unfolds an Expr representing a list into a list of -- Exprs. This reverses the effect of fold. -- --

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

unfold :: 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 unfoldTrio :: Expr -> (Expr, Expr, Expr) foldTrio :: (Expr, 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 pair of Expr values into a single -- Expr. (cf. unfoldPair) -- -- This always generates an ill-typed expression. -- --

--   > 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(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 -- | 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 -- | 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] -- | 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] -- | O(n^2). Lists all holes in an expression without repetitions. -- (cf. holes) -- --

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

-- --

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

-- --

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

-- -- Runtime averages to O(n log n) on evenly distributed -- expressions such as (f x + g y) + (h z + f w); and to -- O(n^2) on deep expressions such as f (g (h (f (g (h -- x))))). nubHoles :: Expr -> [Expr] -- | O(n). Lists all holes in an expression, in order and with -- repetitions. (cf. nubHoles) -- --

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

-- --

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

-- --

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

holes :: Expr -> [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(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). 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 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 -- | 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(n*n*m). Substitute subexpressions in an expression from the -- given list of substitutions. (cf. mapSubexprs). -- -- Please consider using //- if you are replacing just terminal -- values as it is faster. -- -- Given that: -- --

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

-- -- Then: -- --

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

-- --

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

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

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

-- -- Given that the argument list has length m, this function is -- O(n*n*m). Remember that since n is the size of an -- expression, comparing two expressions is O(n) in the worst -- case, and we may need to compare with n subexpressions in the -- worst case. (//) :: Expr -> [(Expr, Expr)] -> Expr -- | O(n*m). Substitute occurrences of values in an expression from -- the given list of substitutions. (cf. mapValues) -- -- Given that: -- --

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

-- -- Then: -- --

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

-- --

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

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

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

-- -- Please use the slower // if you want the above replacement to -- work. -- -- Replacement happens only once: -- --

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

-- -- Given that the argument list has length m, this function is -- O(n*m). (//-) :: 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). 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). 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 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 -- | 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 -- | 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 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(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 -- | 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). Lists all variables in an expression in order and with -- repetitions. (cf. nubVars) -- --

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

-- --

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

-- --

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

-- --

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

vars :: Expr -> [Expr] -- | O(n^2). List terminal constants in an expression without -- repetitions. (cf. consts) -- --

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

-- --

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

-- --

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

-- -- Runtime averages to O(n log n) on evenly distributed -- expressions such as (f x + g y) + (h z + f w); and to -- O(n^2) on deep expressions such as f (g (h (f (g (h -- x))))). nubConsts :: Expr -> [Expr] -- | O(n). List terminal constants in an expression in order and -- with repetitions. (cf. nubConsts) -- --

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

-- --

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

-- --

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

-- --

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

consts :: Expr -> [Expr] -- | O(n^2). Lists all terminal values in an expression without -- repetitions. (cf. values) -- --

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

-- -- ] -- --

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

-- --

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

-- --

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

-- -- Runtime averages to O(n log n) on evenly distributed -- expressions such as (f x + g y) + (h z + f w); and to -- O(n^2) on deep expressions such as f (g (h (f (g (h -- x))))). nubValues :: 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^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) 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(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(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 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 constant. -- (cf. isGround). -- --

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

-- --

--   > isConst $ val False
--   True
--

-- --

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

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

-- -- You need to provide this as part of your building blocks on the -- background if you want recursive functions to be considered and -- produced. ifFor :: Typeable a => a -> Expr -- | 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 class Typeable a => Conjurable a canonicalApplication :: Conjurable f => String -> f -> Expr canonicalVarApplication :: Conjurable f => String -> f -> Expr unifiedArgumentTiers :: Conjurable f => f -> [[Expr]] tiersFor :: Conjurable f => f -> Expr -> [[Expr]] mkExprTiers :: (Listable a, Show a, Typeable a) => a -> [[Expr]] instance Conjure.Conjurable.Conjurable () instance Conjure.Conjurable.Conjurable GHC.Types.Int instance Conjure.Conjurable.Conjurable GHC.Integer.Type.Integer instance Conjure.Conjurable.Conjurable GHC.Types.Bool instance Data.Typeable.Internal.Typeable a => Conjure.Conjurable.Conjurable [a] instance (Data.Typeable.Internal.Typeable a, Data.Typeable.Internal.Typeable b) => Conjure.Conjurable.Conjurable (a, b) instance Data.Typeable.Internal.Typeable a => Conjure.Conjurable.Conjurable (GHC.Maybe.Maybe a) instance (Data.Typeable.Internal.Typeable a, Data.Typeable.Internal.Typeable b) => Conjure.Conjurable.Conjurable (Data.Either.Either a b) instance Conjure.Conjurable.Conjurable GHC.Types.Float instance Conjure.Conjurable.Conjurable GHC.Types.Double instance Conjure.Conjurable.Conjurable GHC.Types.Ordering instance (Data.Typeable.Internal.Typeable a, Data.Typeable.Internal.Typeable b, Data.Typeable.Internal.Typeable c) => Conjure.Conjurable.Conjurable (a, b, c) instance (Data.Typeable.Internal.Typeable a, Data.Typeable.Internal.Typeable b, Data.Typeable.Internal.Typeable c, Data.Typeable.Internal.Typeable d) => Conjure.Conjurable.Conjurable (a, b, c, d) instance (Data.Typeable.Internal.Typeable a, Data.Typeable.Internal.Typeable b, Data.Typeable.Internal.Typeable c, Data.Typeable.Internal.Typeable d, Data.Typeable.Internal.Typeable e) => Conjure.Conjurable.Conjurable (a, b, c, d, e) instance (Data.Typeable.Internal.Typeable a, Data.Typeable.Internal.Typeable b, Data.Typeable.Internal.Typeable c, Data.Typeable.Internal.Typeable d, Data.Typeable.Internal.Typeable e, Data.Typeable.Internal.Typeable f) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f) instance (Test.LeanCheck.Core.Listable a, Data.Express.Name.Name a, GHC.Show.Show a, Data.Typeable.Internal.Typeable a, Conjure.Conjurable.Conjurable b) => Conjure.Conjurable.Conjurable (a -> b) -- | 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 sixtuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr quintuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr quadruple :: Expr -> Expr -> Expr -> Expr -> Expr triple :: Expr -> Expr -> Expr -> Expr comma :: Expr pair :: Expr -> Expr -> Expr (-|-) :: Expr -> Expr -> Expr just :: Expr -> Expr justBool :: Expr justInt :: Expr nothingBool :: Expr nothingInt :: Expr nothing :: Expr compare' :: Expr -> Expr -> Expr -- | A virtual function if :: Bool -> a -> a -> a lifted -- over the Expr type. This is 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'
--

--   > 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 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 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 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 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 -++- -- | 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 -:- -- | unit constructs a list with a single element. This works for -- elements of type Int, Char and Bool. -- --

--   > unit one
--   [1]
--

-- --

--   > unit false
--   [False]
--

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

-- --

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

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

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

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

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

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

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

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

xxs :: Expr -- | A typed hole of [Int] type encoded as an Expr. -- --

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

is_ :: Expr ordE :: Expr ord' :: Expr -> Expr lineBreak :: Expr space :: Expr -- | The character 'd' encoded as an Expr -- --

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

-- --

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

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

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

-- --

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

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

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

-- --

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

bee :: Expr ae :: Expr ccs :: Expr dd :: Expr cc :: Expr -- | A hole of Char type encoded as an Expr. -- --

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

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

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

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

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

-- --

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

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

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

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

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

-- --

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

--   > idE :$ xx
--   id x :: Int
--

-- --

--   > idE :$ zero
--   id 0 :: Int
--

-- --

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

idE :: 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 operator * for the Int type. (See also -*-.) -- --

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

-- --

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

-- --

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

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

--   > three -*- three
--   9 :: Int
--

-- --

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

-- --

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

(-*-) :: Expr -> Expr -> Expr infixl 7 -*- -- | 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 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 -+- -- | A variable g of 'Int -> Int' type encoded as an -- Expr. -- --

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

ggE :: 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: (-?-): cannot apply `(?) :: * -> * -> *` to `x :: Int' and `q :: Bool'.  Unhandled types?
--

(-?-) :: Expr -> Expr -> Expr -- | A variable function g of 'Int -> Int' type lifted over the -- Expr type. -- --

--   > gg yy
--   g y :: Int
--

-- --

--   > gg minusTwo
--   gg (-2) :: Int
--

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

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

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

--   > ff xx
--   f x :: Int
--

-- --

--   > ff one
--   f 1 :: Int
--

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

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

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

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

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

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

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

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

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

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

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

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

zero :: Expr ii' :: Expr kk :: Expr jj :: Expr ii :: Expr -- | A variable x' of Int type. -- --

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

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

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

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

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

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

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

xx :: Expr -- | A typed hole of Int type. -- --

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

i_ :: Expr -- | 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 -||- -- | 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 not lifted over the Expr type. -- --

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

-- --

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

-- --

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

not' :: Expr -> Expr implies :: Expr (-==>-) :: Expr -> Expr -> Expr infixr 0 -==>- -- | The function or encoded as an Expr. -- --

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

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

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

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

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

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

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

true :: Expr -- | False encoded as an Expr. -- --

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

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

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

pp' :: Expr -- | Expr representing a variable r :: Bool. -- --

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

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

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

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

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

pp :: Expr -- | Expr representing a hole of Bool type. -- --

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

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

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

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

--   > 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 new -- variables are introduced so name clashes are avoided: -- --

--   > canonicalVariations $ i_ -+- ii -+- jj -+- i_
--   [ x + y + z + x' :: Int
--   , x + y + z + x :: Int ]
--

-- --

--   > canonicalVariations $ ii -+- jj
--   [x + y :: Int]
--

-- --

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

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

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

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

-- --

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

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

-- --

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

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

-- --

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

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

-- --

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

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

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

-- --

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

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

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

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

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

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

unfold :: 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 unfoldTrio :: Expr -> (Expr, Expr, Expr) foldTrio :: (Expr, 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 pair of Expr values into a single -- Expr. (cf. unfoldPair) -- -- This always generates an ill-typed expression. -- --

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

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

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

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

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

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

--   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)
--   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(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 -- | 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). Lists all variables in an expression in order and with -- repetitions. (cf. nubVars) -- --

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

-- --

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

-- --

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

-- --

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

vars :: Expr -> [Expr] -- | O(n^2). List terminal constants in an expression without -- repetitions. (cf. consts) -- --

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

-- --

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

-- --

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

-- -- Runtime averages to O(n log n) on evenly distributed -- expressions such as (f x + g y) + (h z + f w); and to -- O(n^2) on deep expressions such as f (g (h (f (g (h -- x))))). nubConsts :: Expr -> [Expr] -- | O(n). List terminal constants in an expression in order and -- with repetitions. (cf. nubConsts) -- --

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

-- --

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

-- --

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

-- --

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

consts :: Expr -> [Expr] -- | O(n^2). Lists all terminal values in an expression without -- repetitions. (cf. values) -- --

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

-- -- ] -- --

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

-- --

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

-- --

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

-- -- Runtime averages to O(n log n) on evenly distributed -- expressions such as (f x + g y) + (h z + f w); and to -- O(n^2) on deep expressions such as f (g (h (f (g (h -- x))))). nubValues :: 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
--   ]
--

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

--   > 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(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(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 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 constant. -- (cf. isGround). -- --

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

-- --

--   > isConst $ val False
--   True
--

-- --

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

isConst :: 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(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). 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]
--

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

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

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

-- --

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

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

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

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

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

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

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

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

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

--   > 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] -- | 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 -- | 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] -- | Arguments to be passed to conjureWith or conjpureWith. -- See args for the defaults. data Args Args :: Int -> Int -> Int -> Int -> Args -- | defaults to 60 [maxTests] :: Args -> Int -- | defaults to 9, keep greater than maxEquationSize [maxSize] :: Args -> Int -- | defaults to 5, keep smaller than maxSize [maxEquationSize] :: Args -> Int -- | defaults to 60 [maxRecursionSize] :: Args -> Int -- | Default arguments to conjure. -- --

60 tests
functions of up to 9 symbols
pruning with equations up to size 5
recursion up to 60 symbols.

args :: Args -- | 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
--   
--   background :: [Expr]
--   background =
--     [ val (0::Int)
--     , val (1::Int)
--     , value "+" ((+) :: Int -> Int -> Int)
--     , value "*" ((*) :: Int -> Int -> Int)
--     , value "==" ((==) :: Int -> Int -> Bool)
--   ]
--

-- -- The conjure function does the following: -- --

--   > conjure "square" square background
--   square :: Int -> Int
--   -- looking through 815 candidates, 100% match, 3/3 assignments
--   square x  =  x * x
--

-- -- The background is defined with val, value and -- ifFor. conjure :: Conjurable f => String -> f -> [Expr] -> IO () -- | Like conjure but allows setting options through Args and -- args. conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO () -- | Like conjure but in the pure world. -- -- Returns a triple whose: -- --

first element is the number of candidates considered
second element is the number of defined points in the given -- function
third element is a list of implementations encoded as Exprs -- paired with the number of matching points.

conjpure :: Conjurable f => String -> f -> [Expr] -> (Int, Int, [(Int, Expr)]) -- | Like conjpure but allows setting options through Args -- and args. conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> (Int, Int, [(Int, Expr)]) candidateExprs :: Conjurable f => String -> f -> Int -> (Expr -> Expr -> Bool) -> [[Expr]] -> [[Expr]] -- | 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]
--

-- -- You need to provide this as part of your building blocks on the -- background if you want recursive functions to be considered and -- produced. ifFor :: Typeable a => a -> Expr -- | 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: -- --

--   background :: [Expr]
--   background =
--     [ val (0::Int)
--     , val (1::Int)
--     , value "+" ((+) :: Int -> Int -> Int)
--     , value "*" ((*) :: Int -> Int -> Int)
--     , value "==" ((==) :: Int -> Int -> Bool)
--   ]
--

-- -- Including equality == over the given type is a good rule of -- thumb to improve performance. -- -- Step 3: call conjure and see your generated function: -- --

--   > conjure "square" square background
--   square :: Int -> Int
--   -- looking through 815 candidates, 100% match, 3/3 assignments
--   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
--   
--   background :: [Expr]
--   background =
--     [ val (0::Int)
--     , val (1::Int)
--     , value "+" ((+) :: Int -> Int -> Int)
--     , value "*" ((*) :: Int -> Int -> Int)
--     , value "==" ((==) :: Int -> Int -> Bool)
--   ]
--

-- -- The conjure function does the following: -- --

--   > conjure "square" square background
--   square :: Int -> Int
--   -- looking through 815 candidates, 100% match, 3/3 assignments
--   square x  =  x * x
--

-- -- The background is defined with val, value and -- ifFor. conjure :: Conjurable f => String -> f -> [Expr] -> IO () -- | 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
--

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

-- -- You need to provide this as part of your building blocks on the -- background if you want recursive functions to be considered and -- produced. ifFor :: Typeable a => a -> Expr -- | Values of type Expr represent objects or applications between -- objects. Each object is encapsulated together with its type and string -- representation. Values encoded in Exprs are always monomorphic. -- -- An Expr can be constructed using: -- --

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

-- --

--   > val False
--   False :: Bool
--

-- --

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

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

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

-- --

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

-- --

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

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

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

first element is the number of candidates considered
second element is the number of defined points in the given -- function
third element is a list of implementations encoded as Exprs -- paired with the number of matching points.

conjpure :: Conjurable f => String -> f -> [Expr] -> (Int, Int, [(Int, Expr)]) -- | Arguments to be passed to conjureWith or conjpureWith. -- See args for the defaults. data Args Args :: Int -> Int -> Int -> Int -> Args -- | defaults to 60 [maxTests] :: Args -> Int -- | defaults to 9, keep greater than maxEquationSize [maxSize] :: Args -> Int -- | defaults to 5, keep smaller than maxSize [maxEquationSize] :: Args -> Int -- | defaults to 60 [maxRecursionSize] :: Args -> Int -- | Default arguments to conjure. -- --

60 tests
functions of up to 9 symbols
pruning with equations up to size 5
recursion up to 60 symbols.

args :: Args -- | Like conjure but allows setting options through Args and -- args. conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO () -- | Like conjpure but allows setting options through Args -- and args. conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> (Int, Int, [(Int, Expr)]) -- | This module is part of Arguable. -- -- This defines the Arguable typeclass and utilities involving it. -- -- You are probably better off importing Conjure. module Conjure.Arguable -- | Extrapolate can generalize counter-examples of any types that are -- Arguable. -- -- Arguable types must first be instances of -- --

Listable, so Extrapolate knows how to enumerate -- values;
Express, so Extrapolate can represent then manipulate -- values;
Name, so Extrapolate knows how to name variables.

-- -- There are no required functions, so we can define instances with: -- --

--   instance Arguable OurType
--

-- -- However, it is desirable to define both background and -- subInstances. -- -- The following example shows a datatype and its instance: -- --

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

-- --

--   instance Arguable a => Arguable (Stack a) where
--     subInstances s  =  instances (argTy1of1 s)
--

-- -- To declare instances it may be useful to use type binding -- operators such as: argTy1of1, argTy1of2 and -- argTy2of2. -- -- Instances can be automatically derived using deriveArguable -- which will also automatically derivate Listable, Express -- and Name when needed. class (Listable a, Express a, Name a, Show a) => Arguable a -- | List of symbols allowed to appear in side-conditions. Defaults to -- []. See value. background :: Arguable a => a -> [Expr] -- | Computes a list of reified subtype instances. Defaults to id. -- See instances. subInstances :: Arguable a => a -> Instances -> Instances -- | Used in the definition of subInstances in Arguable -- typeclass instances. instances :: Arguable a => a -> Instances -> Instances mkEq1 :: (Arguable a, Arguable b) => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr] mkEq2 :: (Arguable a, Arguable b, Arguable c) => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr] mkEq3 :: (Arguable a, Arguable b, Arguable c, Arguable d) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool) -> [Expr] mkEq4 :: (Arguable a, Arguable b, Arguable c, Arguable d, Arguable e) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (e -> e -> Bool) -> a -> a -> Bool) -> [Expr] mkOrd1 :: (Arguable a, Arguable b) => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr] mkOrd2 :: (Arguable a, Arguable b, Arguable c) => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr] mkOrd3 :: (Arguable a, Arguable b, Arguable c, Arguable d) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool) -> [Expr] mkOrd4 :: (Arguable a, Arguable b, Arguable c, Arguable d, Arguable e) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (e -> e -> Bool) -> a -> a -> Bool) -> [Expr] (*==*) :: Arguable a => a -> a -> Bool (*/=*) :: Arguable a => a -> a -> Bool (*<=*) :: Arguable a => a -> a -> Bool (*<*) :: Arguable a => a -> a -> Bool -- | A type is Listable when there exists a function that is able to -- list (ideally all of) its values. -- -- Ideally, instances should be defined by a tiers function that -- returns a (potentially infinite) list of finite sub-lists (tiers): the -- first sub-list contains elements of size 0, the second sub-list -- contains elements of size 1 and so on. Size here is defined by the -- implementor of the type-class instance. -- -- For algebraic data types, the general form for tiers is -- --

--   tiers  =  cons<N> ConstructorA
--          \/ cons<N> ConstructorB
--          \/ ...
--          \/ cons<N> ConstructorZ
--

-- -- where N is the number of arguments of each constructor -- A...Z. -- -- Here is a datatype with 4 constructors and its listable instance: -- --

--   data MyType  =  MyConsA
--                |  MyConsB Int
--                |  MyConsC Int Char
--                |  MyConsD String
--   
--   instance Listable MyType where
--     tiers =  cons0 MyConsA
--           \/ cons1 MyConsB
--           \/ cons2 MyConsC
--           \/ cons1 MyConsD
--

-- -- The instance for Hutton's Razor is given by: -- --

--   data Expr  =  Val Int
--              |  Add Expr Expr
--   
--   instance Listable Expr where
--     tiers  =  cons1 Val
--            \/ cons2 Add
--

-- -- Instances can be alternatively defined by list. In this case, -- each sub-list in tiers is a singleton list (each succeeding -- element of list has +1 size). -- -- The function deriveListable from Test.LeanCheck.Derive -- can automatically derive instances of this typeclass. -- -- A Listable instance for functions is also available but is not -- exported by default. Import Test.LeanCheck.Function if you need -- to test higher-order properties. class Listable a tiers :: Listable a => [[a]] list :: Listable a => [a] instance Conjure.Arguable.Arguable () instance Conjure.Arguable.Arguable GHC.Types.Bool instance Conjure.Arguable.Arguable GHC.Types.Int instance Conjure.Arguable.Arguable GHC.Integer.Type.Integer instance Conjure.Arguable.Arguable GHC.Types.Char instance Conjure.Arguable.Arguable a => Conjure.Arguable.Arguable (GHC.Maybe.Maybe a) instance (Conjure.Arguable.Arguable a, Conjure.Arguable.Arguable b) => Conjure.Arguable.Arguable (Data.Either.Either a b) instance (Conjure.Arguable.Arguable a, Conjure.Arguable.Arguable b) => Conjure.Arguable.Arguable (a, b) instance (Conjure.Arguable.Arguable a, Conjure.Arguable.Arguable b, Conjure.Arguable.Arguable c) => Conjure.Arguable.Arguable (a, b, c) instance (Conjure.Arguable.Arguable a, Conjure.Arguable.Arguable b, Conjure.Arguable.Arguable c, Conjure.Arguable.Arguable d) => Conjure.Arguable.Arguable (a, b, c, d) instance Conjure.Arguable.Arguable a => Conjure.Arguable.Arguable [a] instance Conjure.Arguable.Arguable GHC.Types.Ordering instance (GHC.Real.Integral a, Conjure.Arguable.Arguable a) => Conjure.Arguable.Arguable (GHC.Real.Ratio a) instance (Conjure.Arguable.Arguable a, Conjure.Arguable.Arguable b, Conjure.Arguable.Arguable c, Conjure.Arguable.Arguable d, Conjure.Arguable.Arguable e) => Conjure.Arguable.Arguable (a, b, c, d, e) instance (Conjure.Arguable.Arguable a, Conjure.Arguable.Arguable b, Conjure.Arguable.Arguable c, Conjure.Arguable.Arguable d, Conjure.Arguable.Arguable e, Conjure.Arguable.Arguable f) => Conjure.Arguable.Arguable (a, b, c, d, e, f) instance (Conjure.Arguable.Arguable a, Conjure.Arguable.Arguable b, Conjure.Arguable.Arguable c, Conjure.Arguable.Arguable d, Conjure.Arguable.Arguable e, Conjure.Arguable.Arguable f, Conjure.Arguable.Arguable g) => Conjure.Arguable.Arguable (a, b, c, d, e, f, g) instance (Conjure.Arguable.Arguable a, Conjure.Arguable.Arguable b, Conjure.Arguable.Arguable c, Conjure.Arguable.Arguable d, Conjure.Arguable.Arguable e, Conjure.Arguable.Arguable f, Conjure.Arguable.Arguable g, Conjure.Arguable.Arguable h) => Conjure.Arguable.Arguable (a, b, c, d, e, f, g, h)