-- 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.3.4 -- | An internal module of Conjure. This exports List, -- Maybe, Function and a few other simple utitilites. module Conjure.Utils count :: (a -> Bool) -> [a] -> Int nubOn :: Eq b => (a -> b) -> [a] -> [a] iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a mzip :: Monoid a => [a] -> [a] -> [a] groupOn :: Eq b => (a -> b) -> [a] -> [[a]] takeUntil :: (a -> Bool) -> [a] -> [a] takeNextWhile :: (a -> a -> Bool) -> [a] -> [a] takeNextUntil :: (a -> a -> Bool) -> [a] -> [a] deconstructions :: (a -> Bool) -> (a -> a) -> a -> [a] -- | The deconstruction is considered valid if it converges for more than -- half of the given values. isDeconstruction :: [a] -> (a -> Bool) -> (a -> a) -> Bool -- | WARNING: uses unsafePerformIO and should only be used -- for debugging! -- --

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

idIO :: (a -> IO ()) -> a -> a mapHead :: (a -> a) -> [a] -> [a] sets :: [a] -> [[a]] -- | This internal module reexports Express along with a few other -- utilities. module Conjure.Expr (-...-) :: Expr -> Expr -> Expr -> Expr enumFromThenTo' :: Expr -> Expr -> Expr -> Expr (-...) :: Expr -> Expr -> Expr enumFromThen' :: Expr -> Expr -> Expr (-..-) :: Expr -> Expr -> Expr enumFromTo' :: Expr -> Expr -> Expr (-..) :: Expr -> Expr enumFrom' :: Expr -> Expr map' :: Expr -> Expr -> Expr mapE :: Expr (-.-) :: Expr -> Expr -> Expr compose :: Expr -- | product of Int elements lifted over the Expr -- type. -- --

--   > product' xxs
--   product xs :: Int
--

-- --

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

product' :: Expr -> Expr -- | sum of Int elements lifted over the Expr type. -- --

--   > sum' xxs
--   sum xs :: Int
--

-- --

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

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

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

-- --

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

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

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

-- --

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

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

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

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

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

pps :: Expr -- | A typed hole of [Bool] type encoded as an Expr. -- --

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

bs_ :: 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 -++- appendInt :: Expr -- | The list constructor lifted over the Expr type. Works for the -- element types Int, Char and Bool. -- --

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

-- --

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

-- --

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

(-:-) :: Expr -> Expr -> Expr infixr 5 -:- -- | 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 zs of type [Int] encoded as an -- Expr. -- --

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

zzs :: 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 'z' encoded as an Expr -- --

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

-- --

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

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

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

-- --

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

-- -- (cf. zee) zed :: 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 -- | signum over the Int type encoded as an Expr. -- --

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

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

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

-- --

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

signum' :: 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 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 h of 'Int -> Int' type encoded as an -- Expr. -- --

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

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

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

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

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

ggE :: 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 4 bound to the Int type encoded as an -- Expr. -- --

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

four :: 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 -- | A variable n of Int type. -- --

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

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

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

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

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

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

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

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

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

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

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

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

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

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 clashes -- are avoided and these variables are not touched: -- --

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

-- --

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

-- --

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

canonicalVariations :: Expr -> [Expr] -- | 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 encompasses the -- second expression in terms of variables. -- -- This is equivalent to flipping the arguments of isInstanceOf. -- --

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

encompasses :: Expr -> Expr -> Bool -- | Given two Exprs, checks if the first expression is an instance -- of the second in terms of variables. (cf. encompasses, -- hasInstanceOf) -- --

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

-- --

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

isInstanceOf :: Expr -> Expr -> Bool -- | 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 (Show a, 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). Returns whether an expression is complete. A complete -- expression is one without holes. -- --

--   > isComplete $ hole (undefined :: Bool)
--   False
--

-- --

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

-- --

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

-- -- isComplete is the negation of hasHole. -- --

--   isComplete  =  not . hasHole
--

-- -- isComplete is to hasHole what isGround is to -- hasVar. isComplete :: Expr -> Bool -- | O(n). Returns whether an expression contains a hole -- --

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

-- --

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

-- --

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

hasHole :: Expr -> Bool -- | 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] -- | Application cross-product between lists of Exprs (>$$<) :: [Expr] -> [Expr] -> [Expr] -- | Makes the function in an application a variable funToVar :: Expr -> Expr -- | Expands recursive calls on an expression until the given size limit is -- reached. -- --

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

-- --

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

-- --

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

-- --

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

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

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

-- --

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

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

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

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

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

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

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

-- --

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

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

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

-- -- This currently works by checking if the function is an if, -- && or ||. mayNotEvaluateArgument :: Expr -> Bool 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 -- primitives if you want recursive functions to be considered and -- produced. ifFor :: Typeable a => a -> Expr primitiveHoles :: [Expr] -> [Expr] primitiveApplications :: [Expr] -> [[Expr]] valuesBFS :: Expr -> [Expr] holesBFS :: Expr -> [Expr] fillBFS :: Expr -> Expr -> Expr showEq :: Expr -> String lhs :: Expr -> Expr rhs :: Expr -> Expr ($$**) :: Expr -> Expr -> Maybe Expr ($$|<) :: Expr -> Expr -> Maybe Expr possibleHoles :: [Expr] -> [Expr] isDeconstructionE :: [Expr] -> Expr -> Expr -> Bool revaluate :: Typeable a => (Expr, Expr) -> Int -> Expr -> Maybe a reval :: Typeable a => (Expr, Expr) -> Int -> a -> Expr -> a enumerateApps :: (Expr -> Bool) -> [Expr] -> [[Expr]] enumerateAppsFor :: Expr -> (Expr -> Bool) -> [[Expr]] -> [[Expr]] -- | This module is part of Conjure. -- -- This module defines the Cases typeclass that allows listing -- cases of a type encoded as Exprs -- -- You are probably better off importing Conjure. module Conjure.Cases class Express a => Cases a cases :: Cases a => a -> [Expr] type Fxpr = (Expr, Cxpr) sumFxpr :: Fxpr factFxpr :: Fxpr nullFxpr :: Fxpr isZeroFxpr :: Fxpr instance Conjure.Cases.Cases () instance Conjure.Cases.Cases GHC.Types.Bool instance Conjure.Cases.Cases GHC.Types.Int instance Conjure.Cases.Cases GHC.Integer.Type.Integer instance Conjure.Cases.Cases GHC.Types.Char instance Data.Express.Express.Express a => Conjure.Cases.Cases [a] instance (Data.Express.Express.Express a, Data.Express.Express.Express b) => Conjure.Cases.Cases (a, b) instance (Data.Express.Express.Express a, Data.Express.Express.Express b, Data.Express.Express.Express c) => Conjure.Cases.Cases (a, b, c) instance Data.Express.Express.Express a => Conjure.Cases.Cases (GHC.Maybe.Maybe a) instance (Data.Express.Express.Express a, Data.Express.Express.Express b) => Conjure.Cases.Cases (Data.Either.Either a b) -- | This module is part of Conjure. -- -- This defines the Conjurable typeclass and utilities involving -- it. -- -- You are probably better off importing Conjure. module Conjure.Conjurable -- | Single reification of some functions over a type as Exprs. -- -- A hole, an if function, an equality function and tiers. type Reification1 = (Expr, Expr, Maybe Expr, Maybe [[Expr]]) -- | A reification over a collection of types. -- -- Represented as a transformation of a list to a list. type Reification = [Reification1] -> [Reification1] -- | Class of Conjurable types. Functions are Conjurable if -- all their arguments are Conjurable, Listable and -- Showable. -- -- For atomic types that are Listable, instances are defined as: -- --

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

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

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

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

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

-- -- Above x, y, z and w are just -- proxies. The Proxy type was avoided for backwards -- compatibility. -- -- Please see the source code of Conjure.Conjurable for more -- examples. -- -- (cf. reifyTiers, reifyEquality, conjureType) class Typeable a => Conjurable a conjureArgumentHoles :: Conjurable a => a -> [Expr] -- | Returns Just the == function encoded as an Expr -- when available or Nothing otherwise. conjureEquality :: Conjurable a => a -> Maybe Expr -- | Returns Just tiers of values encoded as Exprs -- when possible or Nothing otherwise. conjureTiers :: Conjurable a => a -> Maybe [[Expr]] conjureSubTypes :: Conjurable a => a -> Reification conjureIf :: Conjurable a => a -> Expr conjureType :: Conjurable a => a -> Reification -- | Reifies equality to be used in a conjurable type. -- -- This is to be used in the definition of conjureTiers of -- Conjurable typeclass instances: -- --

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

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

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

reifyEquality :: (Eq a, Typeable a) => a -> Maybe Expr conjureApplication :: Conjurable f => String -> f -> Expr conjureVarApplication :: Conjurable f => String -> f -> Expr conjureHoles :: Conjurable f => f -> [Expr] conjureIfs :: Conjurable f => f -> [Expr] conjureTiersFor :: Conjurable f => f -> Expr -> [[Expr]] conjureAreEqual :: Conjurable f => f -> Int -> Expr -> Expr -> Bool conjureMkEquation :: Conjurable f => f -> Expr -> Expr -> Expr -- | Generic type A. -- -- Can be used to test polymorphic functions with a type variable such as -- take or sort: -- --

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

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

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

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

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

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

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

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

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

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

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

-- -- This type is homomorphic to A, B, Nat6, D, -- E and F. data C -- | Generic type D. -- -- Can be used to test polymorphic functions with four type variables. -- -- This type is homomorphic to A, B, C, Nat6, -- E and F. data D -- | Generic type E. -- -- Can be used to test polymorphic functions with five type variables. -- -- This type is homomorphic to A, B, C, D, -- Nat6 and F. data E -- | Generic type F. -- -- Can be used to test polymorphic functions with five type variables. -- -- This type is homomorphic to A, B, C, D, -- E and Nat6. data F conjureIsDeconstructor :: Conjurable f => f -> Int -> Expr -> Expr -> Expr -> Bool instance Conjure.Conjurable.Conjurable () instance Conjure.Conjurable.Conjurable GHC.Types.Bool instance Conjure.Conjurable.Conjurable GHC.Types.Int instance Conjure.Conjurable.Conjurable GHC.Integer.Type.Integer instance Conjure.Conjurable.Conjurable GHC.Types.Char instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a) => Conjure.Conjurable.Conjurable [a] instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b) => Conjure.Conjurable.Conjurable (a, b) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c) => Conjure.Conjurable.Conjurable (a, b, c) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a) => Conjure.Conjurable.Conjurable (GHC.Maybe.Maybe a) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b) => Conjure.Conjurable.Conjurable (Data.Either.Either a b) instance (Conjure.Conjurable.Conjurable a, Conjure.Conjurable.Conjurable b) => Conjure.Conjurable.Conjurable (a -> b) instance Conjure.Conjurable.Conjurable GHC.Types.Ordering instance Conjure.Conjurable.Conjurable GHC.Types.Float instance Conjure.Conjurable.Conjurable GHC.Types.Double instance Conjure.Conjurable.Conjurable GHC.Int.Int8 instance Conjure.Conjurable.Conjurable GHC.Int.Int16 instance Conjure.Conjurable.Conjurable GHC.Int.Int32 instance Conjure.Conjurable.Conjurable GHC.Int.Int64 instance Conjure.Conjurable.Conjurable GHC.Types.Word instance Conjure.Conjurable.Conjurable GHC.Word.Word8 instance Conjure.Conjurable.Conjurable GHC.Word.Word16 instance Conjure.Conjurable.Conjurable GHC.Word.Word32 instance Conjure.Conjurable.Conjurable GHC.Word.Word64 instance (GHC.Real.Integral a, Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, GHC.Classes.Eq a) => Conjure.Conjurable.Conjurable (GHC.Real.Ratio a) instance (GHC.Float.RealFloat a, Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, GHC.Classes.Eq a) => Conjure.Conjurable.Conjurable (Data.Complex.Complex a) instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.A instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.B instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.C instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.D instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.E instance Conjure.Conjurable.Conjurable Test.LeanCheck.Utils.Types.F instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d) => Conjure.Conjurable.Conjurable (a, b, c, d) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e) => Conjure.Conjurable.Conjurable (a, b, c, d, e) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Conjure.Conjurable.Conjurable f, Test.LeanCheck.Core.Listable f, GHC.Show.Show f) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f) instance (Conjure.Conjurable.Conjurable a, Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Conjure.Conjurable.Conjurable b, Test.LeanCheck.Core.Listable b, GHC.Show.Show b, Conjure.Conjurable.Conjurable c, Test.LeanCheck.Core.Listable c, GHC.Show.Show c, Conjure.Conjurable.Conjurable d, Test.LeanCheck.Core.Listable d, GHC.Show.Show d, Conjure.Conjurable.Conjurable e, Test.LeanCheck.Core.Listable e, GHC.Show.Show e, Conjure.Conjurable.Conjurable f, Test.LeanCheck.Core.Listable f, GHC.Show.Show f, Conjure.Conjurable.Conjurable g, Test.LeanCheck.Core.Listable g, GHC.Show.Show g) => Conjure.Conjurable.Conjurable (a, b, c, d, e, f, g) -- | An internal module of Conjure, a library for Conjuring -- function implementations from tests or partial definitions. (a.k.a.: -- functional inductive programming) module Conjure.Engine -- | Conjures an implementation of a partially defined function. -- -- Takes a String with the name of a function, a partially-defined -- function from a conjurable type, and a list of building blocks encoded -- as Exprs. -- -- For example, given: -- --

--   square :: Int -> Int
--   square 0  =  0
--   square 1  =  1
--   square 2  =  4
--   
--   primitives :: [Expr]
--   primitives =
--     [ val (0::Int)
--     , val (1::Int)
--     , value "+" ((+) :: Int -> Int -> Int)
--     , value "*" ((*) :: Int -> Int -> Int)
--   ]
--

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

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

-- -- The primitives list is defined with val and value. conjure :: Conjurable f => String -> f -> [Expr] -> IO () -- | Like conjure but allows setting the maximum size of considered -- expressions instead of the default value of 12. -- --

--   conjureWithMaxSize 10 "function" function [...]
--

conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO () -- | Arguments to be passed to conjureWith or conjpureWith. -- See args for the defaults. data Args Args :: Int -> Int -> Int -> Int -> Int -> Int -> [[Expr]] -> Args -- | maximum number of tests to each candidate [maxTests] :: Args -> Int -- | maximum size of candidate bodies [maxSize] :: Args -> Int -- | maximum number of allowed recursive calls [maxRecursiveCalls] :: Args -> Int -- | maximum size of equation operands [maxEquationSize] :: Args -> Int -- | maximum size of a recursive expression expansion [maxRecursionSize] :: Args -> Int -- | maximum number of tests to search for defined values [maxSearchTests] :: Args -> Int -- | force tests [forceTests] :: Args -> [[Expr]] -- | Default arguments to conjure. -- --

60 tests
functions of up to 12 symbols
maximum of 1 recursive call
pruning with equations up to size 5
recursion up to 60 symbols
search for defined applications for up to 100000 combinations

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

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

conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO () -- | Like conjure but in the pure world. -- -- Returns a triple with: -- --

tiers of implementations
tiers of candidate bodies (right type)
tiers of candidate expressions (any type)
a list of tests

conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr]) -- | Like conjpure but allows setting options through Args -- and args. conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr]) candidateExprs :: Conjurable f => String -> f -> Int -> Int -> (Expr -> Expr -> Bool) -> [Expr] -> [[Expr]] (-...-) :: Expr -> Expr -> Expr -> Expr enumFromThenTo' :: Expr -> Expr -> Expr -> Expr (-...) :: Expr -> Expr -> Expr enumFromThen' :: Expr -> Expr -> Expr (-..-) :: Expr -> Expr -> Expr enumFromTo' :: Expr -> Expr -> Expr (-..) :: Expr -> Expr enumFrom' :: Expr -> Expr map' :: Expr -> Expr -> Expr mapE :: Expr (-.-) :: Expr -> Expr -> Expr compose :: Expr -- | product of Int elements lifted over the Expr -- type. -- --

--   > product' xxs
--   product xs :: Int
--

-- --

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

product' :: Expr -> Expr -- | sum of Int elements lifted over the Expr type. -- --

--   > sum' xxs
--   sum xs :: Int
--

-- --

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

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

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

-- --

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

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

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

-- --

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

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

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

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

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

pps :: Expr -- | A typed hole of [Bool] type encoded as an Expr. -- --

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

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

-- --

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

-- --

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

-- --

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

--   > 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 -++- appendInt :: Expr -- | The list constructor lifted over the Expr type. Works for the -- element types Int, Char and Bool. -- --

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

-- --

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

-- --

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

(-:-) :: Expr -> Expr -> Expr infixr 5 -:- -- | 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 zs of type [Int] encoded as an -- Expr. -- --

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

zzs :: 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 'z' encoded as an Expr -- --

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

-- --

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

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

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

-- --

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

-- -- (cf. zee) zed :: 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 -- | signum over the Int type encoded as an Expr. -- --

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

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

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

-- --

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

signum' :: 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 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 h of 'Int -> Int' type encoded as an -- Expr. -- --

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

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

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

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

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

ggE :: 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 4 bound to the Int type encoded as an -- Expr. -- --

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

four :: 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 -- | A variable n of Int type. -- --

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

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

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

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

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

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

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

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

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

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

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

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

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

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 clashes -- are avoided and these variables are not touched: -- --

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

-- --

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

-- --

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

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

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

encompasses :: Expr -> Expr -> Bool -- | Given two Exprs, checks if the first expression is an instance -- of the second in terms of variables. (cf. encompasses, -- hasInstanceOf) -- --

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

-- --

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

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). Returns whether an expression is complete. A complete -- expression is one without holes. -- --

--   > isComplete $ hole (undefined :: Bool)
--   False
--

-- --

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

-- --

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

-- -- isComplete is the negation of hasHole. -- --

--   isComplete  =  not . hasHole
--

-- -- isComplete is to hasHole what isGround is to -- hasVar. isComplete :: Expr -> Bool -- | O(n). Returns whether an expression contains a hole -- --

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

-- --

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

-- --

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

hasHole :: Expr -> Bool -- | 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] boolTy :: TypeRep -- | Computes a theory from atomic expressions. Example: -- --

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

theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy -- | List all possible variable bindings to an expression -- --

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

groundBinds :: (Expr -> [[Expr]]) -> Expr -> [Binds] printThy :: Thy -> IO () data Thy -- | An internal module of Conjure, a library for Conjuring -- function implementations from tests or partial definitions. (a.k.a.: -- functional inductive programming) module Conjure.Spec -- | A partial specification of a function with one argument: -- --

--   sumSpec :: Spec1 [Int] Int
--   sumSpec  =
--     [ []      -= 0
--     , [1,2]   -= 3
--     , [3,4,5] -= 12
--     ]
--

-- -- To be passed as one of the arguments to conjure1. type Spec1 a b = [(a, b)] -- | A partial specification of a function with two arguments: -- --

--   appSpec :: Spec2 [Int] [Int] [Int]
--   appSpec  =
--     [ (,) []      [0,1]   -= [0,1]
--     , (,) [2,3]   []      -= [2,3]
--     , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
--     ]
--

-- -- To be passed as one of the arguments to conjure2. type Spec2 a b c = [((a, b), c)] -- | A partial specification of a function with three arguments. -- -- To be passed as one of the arguments to conjure3 type Spec3 a b c d = [((a, b, c), d)] -- | To be used when constructing specifications: Spec1, -- Spec2 and Spec3. (-=) :: a -> b -> (a, b) -- | Conjures a one argument function from a specification. -- -- Given: -- --

--   sumSpec :: Spec1 [Int] Int
--   sumSpec  =
--     [ []      -= 0
--     , [1,2]   -= 3
--     , [3,4,5] -= 12
--     ]
--

-- --

--   sumPrimitives :: [Expr]
--   sumPrimitives  =
--     [ value "null" (null :: [Int] -> Bool)
--     , val (0::Int)
--     , value "+"    ((+) :: Int -> Int -> Int)
--     , value "head" (head :: [Int] -> Int)
--     , value "tail" (tail :: [Int] -> [Int])
--     ]
--

-- -- Then: -- --

--   > conjure1 "sum" sumSpec sumPrimitives
--   sum :: [Int] -> Int
--   -- testing 3 combinations of argument values
--   -- ...
--   -- looking through 189/465 candidates of size 10
--   xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
--

-- -- (cf. Spec1, conjure1With) conjure1 :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b) => String -> Spec1 a b -> [Expr] -> IO () -- | Conjures a two argument function from a specification. -- -- Given: -- --

--   appSpec :: Spec2 [Int] [Int] [Int]
--   appSpec  =
--     [ (,) []      [0,1]   -= [0,1]
--     , (,) [2,3]   []      -= [2,3]
--     , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
--     ]
--

-- --

--   appPrimitives :: [Expr]
--   appPrimitives =
--     [ value "null" (null :: [Int] -> Bool)
--     , value ":"    ((:) :: Int -> [Int] -> [Int])
--     , value "head" (head :: [Int] -> Int)
--     , value "tail" (tail :: [Int] -> [Int])
--     ]
--

-- -- Then: -- --

--   > conjure2 "++" appSpec appPrimitives
--   (++) :: [Int] -> [Int] -> [Int]
--   -- testing 3 combinations of argument values
--   -- ...
--   -- looking through 26166/57090 candidates of size 11
--   xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
--

-- -- (cf. Spec2, conjure2With) conjure2 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c) => String -> Spec2 a b c -> [Expr] -> IO () -- | Conjures a three argument function from a specification. -- -- (cf. Spec3, conjure3With) conjure3 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d, Eq d) => String -> Spec3 a b c d -> [Expr] -> IO () -- | Like conjure1 but allows setting options through -- Args/args. conjure1With :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b) => Args -> String -> Spec1 a b -> [Expr] -> IO () -- | Like conjure2 but allows setting options through -- Args/args. conjure2With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c) => Args -> String -> Spec2 a b c -> [Expr] -> IO () -- | Like conjure3 but allows setting options through -- Args/args. conjure3With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d, Eq d) => Args -> String -> Spec3 a b c d -> [Expr] -> IO () -- | A library for Conjuring function implementations from tests or partial -- definitions. (a.k.a.: functional inductive programming) -- -- This is currently an experimental tool in its early stages, don't -- expect much from its current version. It is just a piece of curiosity -- in its current state. -- -- Step 1: declare your partial function -- --

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

-- -- Step 2: declare a list with the potential building blocks: -- --

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

-- -- Step 3: call conjure and see your generated function: -- --

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

module Conjure -- | Conjures an implementation of a partially defined function. -- -- Takes a String with the name of a function, a partially-defined -- function from a conjurable type, and a list of building blocks encoded -- as Exprs. -- -- For example, given: -- --

--   square :: Int -> Int
--   square 0  =  0
--   square 1  =  1
--   square 2  =  4
--   
--   primitives :: [Expr]
--   primitives =
--     [ val (0::Int)
--     , val (1::Int)
--     , value "+" ((+) :: Int -> Int -> Int)
--     , value "*" ((*) :: Int -> Int -> Int)
--   ]
--

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

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

-- -- The primitives list is defined with val and value. 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]
--

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

--   conjureWithMaxSize 10 "function" function [...]
--

conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO () -- | Like conjure but allows setting options through -- Args/args. -- --

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

conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO () -- | Arguments to be passed to conjureWith or conjpureWith. -- See args for the defaults. data Args Args :: Int -> Int -> Int -> Int -> Int -> Int -> [[Expr]] -> Args -- | maximum number of tests to each candidate [maxTests] :: Args -> Int -- | maximum size of candidate bodies [maxSize] :: Args -> Int -- | maximum number of allowed recursive calls [maxRecursiveCalls] :: Args -> Int -- | maximum size of equation operands [maxEquationSize] :: Args -> Int -- | maximum size of a recursive expression expansion [maxRecursionSize] :: Args -> Int -- | maximum number of tests to search for defined values [maxSearchTests] :: Args -> Int -- | force tests [forceTests] :: Args -> [[Expr]] -- | Default arguments to conjure. -- --

60 tests
functions of up to 12 symbols
maximum of 1 recursive call
pruning with equations up to size 5
recursion up to 60 symbols
search for defined applications for up to 100000 combinations

args :: Args -- | A partial specification of a function with one argument: -- --

--   sumSpec :: Spec1 [Int] Int
--   sumSpec  =
--     [ []      -= 0
--     , [1,2]   -= 3
--     , [3,4,5] -= 12
--     ]
--

-- -- To be passed as one of the arguments to conjure1. type Spec1 a b = [(a, b)] -- | A partial specification of a function with two arguments: -- --

--   appSpec :: Spec2 [Int] [Int] [Int]
--   appSpec  =
--     [ (,) []      [0,1]   -= [0,1]
--     , (,) [2,3]   []      -= [2,3]
--     , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
--     ]
--

--   sumSpec :: Spec1 [Int] Int
--   sumSpec  =
--     [ []      -= 0
--     , [1,2]   -= 3
--     , [3,4,5] -= 12
--     ]
--

-- --

--   sumPrimitives :: [Expr]
--   sumPrimitives  =
--     [ value "null" (null :: [Int] -> Bool)
--     , val (0::Int)
--     , value "+"    ((+) :: Int -> Int -> Int)
--     , value "head" (head :: [Int] -> Int)
--     , value "tail" (tail :: [Int] -> [Int])
--     ]
--

-- -- Then: -- --

--   > conjure1 "sum" sumSpec sumPrimitives
--   sum :: [Int] -> Int
--   -- testing 3 combinations of argument values
--   -- ...
--   -- looking through 189/465 candidates of size 10
--   xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
--

--   appSpec :: Spec2 [Int] [Int] [Int]
--   appSpec  =
--     [ (,) []      [0,1]   -= [0,1]
--     , (,) [2,3]   []      -= [2,3]
--     , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
--     ]
--

-- --

--   appPrimitives :: [Expr]
--   appPrimitives =
--     [ value "null" (null :: [Int] -> Bool)
--     , value ":"    ((:) :: Int -> [Int] -> [Int])
--     , value "head" (head :: [Int] -> Int)
--     , value "tail" (tail :: [Int] -> [Int])
--     ]
--

-- -- Then: -- --

--   > conjure2 "++" appSpec appPrimitives
--   (++) :: [Int] -> [Int] -> [Int]
--   -- testing 3 combinations of argument values
--   -- ...
--   -- looking through 26166/57090 candidates of size 11
--   xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
--

-- -- (cf. Spec2, conjure2With) conjure2 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c) => String -> Spec2 a b c -> [Expr] -> IO () -- | Conjures a three argument function from a specification. -- -- (cf. Spec3, conjure3With) conjure3 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d, Eq d) => String -> Spec3 a b c d -> [Expr] -> IO () -- | Like conjure1 but allows setting options through -- Args/args. conjure1With :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b) => Args -> String -> Spec1 a b -> [Expr] -> IO () -- | Like conjure2 but allows setting options through -- Args/args. conjure2With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c) => Args -> String -> Spec2 a b c -> [Expr] -> IO () -- | Like conjure3 but allows setting options through -- Args/args. conjure3With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d, Eq d) => Args -> String -> Spec3 a b c d -> [Expr] -> IO () -- | Class of Conjurable types. Functions are Conjurable if -- all their arguments are Conjurable, Listable and -- Showable. -- -- For atomic types that are Listable, instances are defined as: -- --

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

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

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

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

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

-- -- Above x, y, z and w are just -- proxies. The Proxy type was avoided for backwards -- compatibility. -- -- Please see the source code of Conjure.Conjurable for more -- examples. -- -- (cf. reifyTiers, reifyEquality, conjureType) class Typeable a => Conjurable a -- | Returns Just the == function encoded as an Expr -- when available or Nothing otherwise. conjureEquality :: Conjurable a => a -> Maybe Expr -- | Returns Just tiers of values encoded as Exprs -- when possible or Nothing otherwise. conjureTiers :: Conjurable a => a -> Maybe [[Expr]] conjureSubTypes :: Conjurable a => a -> Reification -- | Reifies equality to be used in a conjurable type. -- -- This is to be used in the definition of conjureEquality of -- Conjurable typeclass instances: -- --

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

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

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

reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]] conjureType :: Conjurable a => a -> Reification -- | Like conjure but in the pure world. -- -- Returns a triple with: -- --

tiers of implementations
tiers of candidate bodies (right type)
tiers of candidate expressions (any type)
a list of tests

conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr]) -- | Like conjpure but allows setting options through Args -- and args. conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr]) -- | Generic type A. -- -- Can be used to test polymorphic functions with a type variable such as -- take or sort: -- --

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

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

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

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

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

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

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

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

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

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