Copyright | (c) 2021 Rudy Matela |
---|---|
License | 3-Clause BSD (see the file LICENSE) |
Maintainer | Rudy Matela <rudy@matela.com.br> |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
An internal module of Conjure, a library for Conjuring function implementations from tests or partial definitions. (a.k.a.: functional inductive programming)
Synopsis
- conjure :: Conjurable f => String -> f -> [Prim] -> IO ()
- conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()
- data Args = Args {}
- args :: Args
- conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()
- conjureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> IO ()
- conjureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> IO ()
- conjure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> IO ()
- conjure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
- conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
- conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
- conjpureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
- conjpureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
- conjpure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
- conjpure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
- candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy)
- candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
- candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
- candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
- conjureTheory :: Conjurable f => String -> f -> [Prim] -> IO ()
- conjureTheoryWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()
- equalModuloTesting :: Conjurable f => Int -> Int -> String -> f -> Defn -> Defn -> Bool
- module Data.Express
- class Name a where
- data Expr
- class (Show a, Typeable a) => Express a where
- (//) :: Expr -> [(Expr, Expr)] -> Expr
- fill :: Expr -> [Expr] -> Expr
- fold :: [Expr] -> Expr
- evaluate :: Typeable a => Expr -> Maybe a
- unfold :: Expr -> [Expr]
- cons :: Expr
- div' :: Expr -> Expr -> Expr
- mod' :: Expr -> Expr -> Expr
- (>$$<) :: [Expr] -> [Expr] -> [Expr]
- size :: Expr -> Int
- value :: Typeable a => String -> a -> Expr
- times :: Expr
- typ :: Expr -> TypeRep
- arity :: Expr -> Int
- compose :: Expr
- unit :: Expr -> Expr
- zero :: Expr
- match :: Expr -> Expr -> Maybe [(Expr, Expr)]
- canonicalize :: Expr -> Expr
- mapValues :: (Expr -> Expr) -> Expr -> Expr
- canonicalVariations :: Expr -> [Expr]
- deriveExpress :: Name -> DecsQ
- variableNamesFromTemplate :: String -> [String]
- names :: Name a => a -> [String]
- isInstanceOf :: Expr -> Expr -> Bool
- deriveName :: Name -> DecsQ
- deriveNameIfNeeded :: Name -> DecsQ
- deriveNameCascading :: Name -> DecsQ
- val :: (Typeable a, Show a) => a -> Expr
- ($$) :: Expr -> Expr -> Maybe Expr
- var :: Typeable a => String -> a -> Expr
- etyp :: Expr -> Either (TypeRep, TypeRep) TypeRep
- mtyp :: Expr -> Maybe TypeRep
- isIllTyped :: Expr -> Bool
- isWellTyped :: Expr -> Bool
- isFun :: Expr -> Bool
- eval :: Typeable a => a -> Expr -> a
- evl :: Typeable a => Expr -> a
- toDynamic :: Expr -> Maybe Dynamic
- showOpExpr :: String -> Expr -> String
- showPrecExpr :: Int -> Expr -> String
- showExpr :: Expr -> String
- compareComplexity :: Expr -> Expr -> Ordering
- compareLexicographically :: Expr -> Expr -> Ordering
- compareQuickly :: Expr -> Expr -> Ordering
- unfoldApp :: Expr -> [Expr]
- hasVar :: Expr -> Bool
- isGround :: Expr -> Bool
- isConst :: Expr -> Bool
- isVar :: Expr -> Bool
- isValue :: Expr -> Bool
- isApp :: Expr -> Bool
- subexprs :: Expr -> [Expr]
- nubSubexprs :: Expr -> [Expr]
- values :: Expr -> [Expr]
- nubValues :: Expr -> [Expr]
- consts :: Expr -> [Expr]
- nubConsts :: Expr -> [Expr]
- vars :: Expr -> [Expr]
- nubVars :: Expr -> [Expr]
- depth :: Expr -> Int
- height :: Expr -> Int
- matchWith :: [(Expr, Expr)] -> Expr -> Expr -> Maybe [(Expr, Expr)]
- encompasses :: Expr -> Expr -> Bool
- hasInstanceOf :: Expr -> Expr -> Bool
- isSubexprOf :: Expr -> Expr -> Bool
- mapVars :: (Expr -> Expr) -> Expr -> Expr
- mapConsts :: (Expr -> Expr) -> Expr -> Expr
- mapSubexprs :: (Expr -> Maybe Expr) -> Expr -> Expr
- (//-) :: Expr -> [(Expr, Expr)] -> Expr
- renameVarsBy :: (String -> String) -> Expr -> Expr
- varAsTypeOf :: String -> Expr -> Expr
- holeAsTypeOf :: Expr -> Expr
- hole :: Typeable a => a -> Expr
- isHole :: Expr -> Bool
- holes :: Expr -> [Expr]
- nubHoles :: Expr -> [Expr]
- hasHole :: Expr -> Bool
- isComplete :: Expr -> Bool
- listVars :: Typeable a => String -> a -> [Expr]
- listVarsAsTypeOf :: String -> Expr -> [Expr]
- foldApp :: [Expr] -> Expr
- foldPair :: (Expr, Expr) -> Expr
- unfoldPair :: Expr -> (Expr, Expr)
- foldTrio :: (Expr, Expr, Expr) -> Expr
- unfoldTrio :: Expr -> (Expr, Expr, Expr)
- deriveExpressIfNeeded :: Name -> DecsQ
- deriveExpressCascading :: Name -> DecsQ
- (>$$) :: [Expr] -> Expr -> [Expr]
- ($$<) :: Expr -> [Expr] -> [Expr]
- reifyEq :: (Typeable a, Eq a) => a -> [Expr]
- reifyOrd :: (Typeable a, Ord a) => a -> [Expr]
- reifyEqOrd :: (Typeable a, Ord a) => a -> [Expr]
- reifyName :: (Typeable a, Name a) => a -> [Expr]
- mkEq :: Typeable a => (a -> a -> Bool) -> [Expr]
- mkOrd :: Typeable a => (a -> a -> Ordering) -> [Expr]
- mkOrdLessEqual :: Typeable a => (a -> a -> Bool) -> [Expr]
- mkName :: Typeable a => (a -> String) -> [Expr]
- mkNameWith :: Typeable a => String -> a -> [Expr]
- lookupComparison :: String -> TypeRep -> [Expr] -> Maybe Expr
- isEqT :: [Expr] -> TypeRep -> Bool
- isOrdT :: [Expr] -> TypeRep -> Bool
- isEqOrdT :: [Expr] -> TypeRep -> Bool
- isEq :: [Expr] -> Expr -> Bool
- isOrd :: [Expr] -> Expr -> Bool
- isEqOrd :: [Expr] -> Expr -> Bool
- mkComparison :: String -> [Expr] -> Expr -> Expr -> Expr
- mkEquation :: [Expr] -> Expr -> Expr -> Expr
- mkComparisonLT :: [Expr] -> Expr -> Expr -> Expr
- mkComparisonLE :: [Expr] -> Expr -> Expr -> Expr
- lookupName :: [Expr] -> Expr -> String
- lookupNames :: [Expr] -> Expr -> [String]
- listVarsWith :: [Expr] -> Expr -> [Expr]
- validApps :: [Expr] -> Expr -> [Expr]
- findValidApp :: [Expr] -> Expr -> Maybe Expr
- preludeNameInstances :: [Expr]
- canonicalizeWith :: (Expr -> [String]) -> Expr -> Expr
- canonicalizationWith :: (Expr -> [String]) -> Expr -> [(Expr, Expr)]
- isCanonicalWith :: (Expr -> [String]) -> Expr -> Bool
- canonicalization :: Expr -> [(Expr, Expr)]
- isCanonical :: Expr -> Bool
- mostGeneralCanonicalVariation :: Expr -> Expr
- mostSpecificCanonicalVariation :: Expr -> Expr
- fastCanonicalVariations :: Expr -> [Expr]
- fastMostGeneralVariation :: Expr -> Expr
- fastMostSpecificVariation :: Expr -> Expr
- b_ :: Expr
- pp :: Expr
- qq :: Expr
- rr :: Expr
- pp' :: Expr
- false :: Expr
- true :: Expr
- notE :: Expr
- andE :: Expr
- orE :: Expr
- (-==>-) :: Expr -> Expr -> Expr
- implies :: Expr
- not' :: Expr -> Expr
- (-&&-) :: Expr -> Expr -> Expr
- (-||-) :: Expr -> Expr -> Expr
- i_ :: Expr
- xx :: Expr
- yy :: Expr
- zz :: Expr
- xx' :: Expr
- ii :: Expr
- jj :: Expr
- kk :: Expr
- ii' :: Expr
- ll :: Expr
- mm :: Expr
- nn :: Expr
- one :: Expr
- two :: Expr
- three :: Expr
- four :: Expr
- five :: Expr
- six :: Expr
- seven :: Expr
- eight :: Expr
- nine :: Expr
- ten :: Expr
- eleven :: Expr
- twelve :: Expr
- minusOne :: Expr
- minusTwo :: Expr
- ff :: Expr -> Expr
- ffE :: Expr
- gg :: Expr -> Expr
- ggE :: Expr
- hh :: Expr -> Expr
- hhE :: Expr
- (-?-) :: Expr -> Expr -> Expr
- question :: Expr
- oo :: Expr -> Expr -> Expr
- ooE :: Expr
- (-+-) :: Expr -> Expr -> Expr
- plus :: Expr
- (-*-) :: Expr -> Expr -> Expr
- minus :: Expr
- divE :: Expr
- modE :: Expr
- quot' :: Expr -> Expr -> Expr
- quotE :: Expr
- rem' :: Expr -> Expr -> Expr
- remE :: Expr
- id' :: Expr -> Expr
- idE :: Expr
- idInt :: Expr
- idBool :: Expr
- idChar :: Expr
- idInts :: Expr
- idBools :: Expr
- idString :: Expr
- const' :: Expr -> Expr -> Expr
- negate' :: Expr -> Expr
- negateE :: Expr
- abs' :: Expr -> Expr
- absE :: Expr
- signum' :: Expr -> Expr
- signumE :: Expr
- odd' :: Expr -> Expr
- even' :: Expr -> Expr
- c_ :: Expr
- cs_ :: Expr
- cc :: Expr
- dd :: Expr
- ccs :: Expr
- ae :: Expr
- bee :: Expr
- cee :: Expr
- dee :: Expr
- zed :: Expr
- zee :: Expr
- space :: Expr
- lineBreak :: Expr
- ord' :: Expr -> Expr
- ordE :: Expr
- is_ :: Expr
- xxs :: Expr
- yys :: Expr
- zzs :: Expr
- nil :: Expr
- emptyString :: Expr
- nilInt :: Expr
- nilBool :: Expr
- nilChar :: Expr
- consInt :: Expr
- consBool :: Expr
- consChar :: Expr
- (-:-) :: Expr -> Expr -> Expr
- appendInt :: Expr
- (-++-) :: Expr -> Expr -> Expr
- head' :: Expr -> Expr
- tail' :: Expr -> Expr
- null' :: Expr -> Expr
- length' :: Expr -> Expr
- init' :: Expr -> Expr
- sort' :: Expr -> Expr
- insert' :: Expr -> Expr -> Expr
- elem' :: Expr -> Expr -> Expr
- (-$-) :: Expr -> Expr -> Expr
- (-/=-) :: Expr -> Expr -> Expr
- (-<=-) :: Expr -> Expr -> Expr
- (-<-) :: Expr -> Expr -> Expr
- if' :: Expr -> Expr -> Expr -> Expr
- caseBool :: Expr -> Expr -> Expr -> Expr
- caseOrdering :: Expr -> Expr -> Expr -> Expr -> Expr
- compare' :: Expr -> Expr -> Expr
- nothing :: Expr
- nothingInt :: Expr
- nothingBool :: Expr
- justInt :: Expr
- justBool :: Expr
- just :: Expr -> Expr
- (-|-) :: Expr -> Expr -> Expr
- pair :: Expr -> Expr -> Expr
- comma :: Expr
- triple :: Expr -> Expr -> Expr -> Expr
- quadruple :: Expr -> Expr -> Expr -> Expr -> Expr
- quintuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr
- sixtuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr
- bs_ :: Expr
- pps :: Expr
- qqs :: Expr
- and' :: Expr -> Expr
- or' :: Expr -> Expr
- sum' :: Expr -> Expr
- product' :: Expr -> Expr
- (-%-) :: Expr -> Expr -> Expr
- (-.-) :: Expr -> Expr -> Expr
- mapE :: Expr
- map' :: Expr -> Expr -> Expr
- enumFrom' :: Expr -> Expr
- (-..) :: Expr -> () -> Expr
- enumFromTo' :: Expr -> Expr -> Expr
- (-..-) :: Expr -> Expr -> Expr
- enumFromThen' :: Expr -> Expr -> Expr
- (--..) :: (Expr, Expr) -> () -> Expr
- enumFromThenTo' :: Expr -> Expr -> Expr -> Expr
- (--..-) :: (Expr, Expr) -> Expr -> Expr
- boolTy :: TypeRep
- grounds :: (Expr -> [[Expr]]) -> Expr -> [Expr]
- groundBinds :: (Expr -> [[Expr]]) -> Expr -> [Binds]
- theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
- data Thy
- printThy :: Thy -> IO ()
- doubleCheck :: (Expr -> Expr -> Bool) -> Thy -> Thy
Documentation
conjure :: Conjurable f => String -> f -> [Prim] -> IO () Source #
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 Expr
s.
For example, given:
square :: Int -> Int square 0 = 0 square 1 = 1 square 2 = 4 primitives :: [Prim] primitives = [ pr (0::Int) , pr (1::Int) , prim "+" ((+) :: Int -> Int -> Int) , prim "*" ((*) :: Int -> Int -> Int) ]
The conjure function does the following:
> conjure "square" square primitives square :: Int -> Int -- pruning with 14/25 rules -- testing 3 combinations of argument values -- looking through 3 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 5 candidates of size 3 square x = x * x
conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO () Source #
Like conjure
but allows setting the maximum size of considered expressions
instead of the default value of 12.
conjureWithMaxSize 10 "function" function [...]
Arguments to be passed to conjureWith
or conjpureWith
.
See args
for the defaults.
Args | |
|
Default arguments to conjure.
- 60 tests
- functions of up to 12 symbols
- maximum of one recursive call allowed in candidate bodies
- maximum evaluation of up to 60 recursions
- pruning with equations up to size 5
- search for defined applications for up to 100000 combinations
- require recursive calls to deconstruct arguments
- don't show the theory used in pruning
- do not make candidates unique module testing
conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO () Source #
conjureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> IO () Source #
Conjures an implementation from a function specification.
This function works like conjure
but instead of receiving a partial definition
it receives a boolean filter / property about the function.
For example, given:
squareSpec :: (Int -> Int) -> Bool squareSpec square = square 0 == 0 && square 1 == 1 && square 2 == 4
Then:
> conjureFromSpec "square" squareSpec primitives square :: Int -> Int -- pruning with 14/25 rules -- looking through 3 candidates of size 1 -- looking through 4 candidates of size 2 -- looking through 9 candidates of size 3 square x = x * x
This allows users to specify QuickCheck-style properties, here is an example using LeanCheck:
import Test.LeanCheck (holds, exists) squarePropertySpec :: (Int -> Int) -> Bool squarePropertySpec square = and [ holds n $ \x -> square x >= x , holds n $ \x -> square x >= 0 , exists n $ \x -> square x > x ] where n = 60
conjureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> IO () Source #
Like conjureFromSpec
but allows setting options through Args
/args
.
conjureFromSpecWith args{maxSize = 11} "function" spec [...]
conjure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> IO () Source #
Synthesizes an implementation from both a partial definition and a function specification.
This works like the functions conjure
and conjureFromSpec
combined.
conjure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> IO () Source #
conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) Source #
Like conjure
but in the pure world.
Returns a quadruple with:
- tiers of implementations
- tiers of candidates
- a list of tests
- the underlying theory
conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) Source #
conjpureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) Source #
Like conjureFromSpec
but in the pure world. (cf. conjpure
)
conjpureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) Source #
Like conjureFromSpecWith
but in the pure world. (cf. conjpure
)
conjpure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) Source #
conjpure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) Source #
Like conjpure0
but allows setting options through Args
and args
.
This is where the actual implementation resides. The functions
conjpure
, conjpureWith
, conjpureFromSpec
, conjpureFromSpecWith
,
conjure
, conjureWith
, conjureFromSpec
, conjureFromSpecWith
and
conjure0
all refer to this.
candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy) Source #
Return apparently unique candidate bodies.
candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy) Source #
Return apparently unique candidate definitions.
candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy) Source #
Return apparently unique candidate definitions where there is a single body.
candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy) Source #
Return apparently unique candidate definitions using pattern matching.
conjureTheory :: Conjurable f => String -> f -> [Prim] -> IO () Source #
Just prints the underlying theory found by Test.Speculate without actually synthesizing a function.
conjureTheoryWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO () Source #
Like conjureTheory
but allows setting options through Args
/args
.
equalModuloTesting :: Conjurable f => Int -> Int -> String -> f -> Defn -> Defn -> Bool Source #
module Data.Express
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''", ...]
Nothing
O(1).
Returns a name for a variable of the given argument's type.
> name (undefined :: Int) "x"
> name (undefined :: [Bool]) "ps"
> name (undefined :: [Maybe Integer]) "mxs"
The default definition is:
name _ = "x"
Instances
Name Int16 | |
Defined in Data.Express.Name | |
Name Int32 | |
Defined in Data.Express.Name | |
Name Int64 | |
Defined in Data.Express.Name | |
Name Int8 | |
Defined in Data.Express.Name | |
Name GeneralCategory | |
Defined in Data.Express.Name name :: GeneralCategory -> String # | |
Name Word16 | |
Defined in Data.Express.Name | |
Name Word32 | |
Defined in Data.Express.Name | |
Name Word64 | |
Defined in Data.Express.Name | |
Name Word8 | |
Defined in Data.Express.Name | |
Name Ordering | name (undefined :: Ordering) = "o" names (undefined :: Ordering) = ["o", "p", "q", "o'", ...] |
Defined in Data.Express.Name | |
Name A Source # | |
Defined in Conjure.Conjurable | |
Name B Source # | |
Defined in Conjure.Conjurable | |
Name C Source # | |
Defined in Conjure.Conjurable | |
Name D Source # | |
Defined in Conjure.Conjurable | |
Name E Source # | |
Defined in Conjure.Conjurable | |
Name F Source # | |
Defined in Conjure.Conjurable | |
Name Integer | name (undefined :: Integer) = "x" names (undefined :: Integer) = ["x", "y", "z", "x'", ...] |
Defined in Data.Express.Name | |
Name () | name (undefined :: ()) = "u" names (undefined :: ()) = ["u", "v", "w", "u'", "v'", ...] |
Defined in Data.Express.Name | |
Name Bool | name (undefined :: Bool) = "p" names (undefined :: Bool) = ["p", "q", "r", "p'", "q'", ...] |
Defined in Data.Express.Name | |
Name Char | name (undefined :: Char) = "c" names (undefined :: Char) = ["c", "d", "e", "c'", "d'", ...] |
Defined in Data.Express.Name | |
Name Double | name (undefined :: Double) = "x" names (undefined :: Double) = ["x", "y", "z", "x'", ...] |
Defined in Data.Express.Name | |
Name Float | name (undefined :: Float) = "x" names (undefined :: Float) = ["x", "y", "z", "x'", ...] |
Defined in Data.Express.Name | |
Name Int | name (undefined :: Int) = "x" names (undefined :: Int) = ["x", "y", "z", "x'", "y'", ...] |
Defined in Data.Express.Name | |
Name Word | |
Defined in Data.Express.Name | |
Name (Complex a) | name (undefined :: Complex) = "x" names (undefined :: Complex) = ["x", "y", "z", "x'", ...] |
Defined in Data.Express.Name | |
Name (Ratio a) | name (undefined :: Rational) = "q" names (undefined :: Rational) = ["q", "r", "s", "q'", ...] |
Defined in Data.Express.Name | |
Name a => Name (Maybe a) | names (undefined :: Maybe Int) = ["mx", "mx1", "mx2", ...] nemes (undefined :: Maybe Bool) = ["mp", "mp1", "mp2", ...] |
Defined in Data.Express.Name | |
Name a => Name [a] | names (undefined :: [Int]) = ["xs", "ys", "zs", "xs'", ...] names (undefined :: [Bool]) = ["ps", "qs", "rs", "ps'", ...] |
Defined in Data.Express.Name | |
(Name a, Name b) => Name (Either a b) | names (undefined :: Either Int Int) = ["exy", "exy1", ...] names (undefined :: Either Int Bool) = ["exp", "exp1", ...] |
Defined in Data.Express.Name | |
(Name a, Name b) => Name (a, b) | names (undefined :: (Int,Int)) = ["xy", "zw", "xy'", ...] names (undefined :: (Bool,Bool)) = ["pq", "rs", "pq'", ...] |
Defined in Data.Express.Name | |
Name (a -> b) | names (undefined :: ()->()) = ["f", "g", "h", "f'", ...] names (undefined :: Int->Int) = ["f", "g", "h", ...] |
Defined in Data.Express.Name | |
(Name a, Name b, Name c) => Name (a, b, c) | names (undefined :: (Int,Int,Int)) = ["xyz","uvw", ...] names (undefined :: (Int,Bool,Char)) = ["xpc", "xpc1", ...] |
Defined in Data.Express.Name | |
(Name a, Name b, Name c, Name d) => Name (a, b, c, d) | names (undefined :: ((),(),(),())) = ["uuuu", "uuuu1", ...] names (undefined :: (Int,Int,Int,Int)) = ["xxxx", ...] |
Defined in Data.Express.Name | |
(Name a, Name b, Name c, Name d, Name e) => Name (a, b, c, d, e) | |
Defined in Data.Express.Name | |
(Name a, Name b, Name c, Name d, Name e, Name f) => Name (a, b, c, d, e, f) | |
Defined in Data.Express.Name | |
(Name a, Name b, Name c, Name d, Name e, Name f, Name g) => Name (a, b, c, d, e, f, g) | |
Defined in Data.Express.Name | |
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h) => Name (a, b, c, d, e, f, g, h) | |
Defined in Data.Express.Name | |
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i) => Name (a, b, c, d, e, f, g, h, i) | |
Defined in Data.Express.Name | |
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i, Name j) => Name (a, b, c, d, e, f, g, h, i, j) | |
Defined in Data.Express.Name | |
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i, Name j, Name k) => Name (a, b, c, d, e, f, g, h, i, j, k) | |
Defined in Data.Express.Name | |
(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i, Name j, Name k, Name l) => Name (a, b, c, d, e, f, g, h, i, j, k, l) | |
Defined in Data.Express.Name |
Values of type Expr
represent objects or applications between objects.
Each object is encapsulated together with its type and string representation.
Values encoded in Expr
s are always monomorphic.
An Expr
can be constructed using:
val
, for values that areShow
instances;value
, for values that are notShow
instances, like functions;:$
, for applications betweenExpr
s.
> 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'
Show
ing 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 Expr
s usually follow the convention
where a value
whose String
representation starts with '_'
represents a var
iable.
Instances
Show Expr | Shows > show (value "not" not :$ val False) "not False :: Bool" |
Eq Expr | O(n). Does not evaluate values when comparing, but rather uses their representation as strings and their types. This instance works for ill-typed expressions. |
Ord Expr | O(n). Does not evaluate values when comparing, but rather uses their representation as strings and their types. This instance works for ill-typed expressions. Expressions come first
when they have smaller complexity ( |
class (Show a, Typeable a) => Express a where #
Express
typeclass instances provide an expr
function
that allows values to be deeply encoded as applications of Expr
s.
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 atomicValue
Expr
s -- shallow encoding.expr
ideally encodes expressions as applications (:$
) betweenValue
Expr
s -- 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
Instances
(//) :: Expr -> [(Expr, Expr)] -> Expr #
O(n*n*m).
Substitute subexpressions in an expression
from the given list of substitutions.
(cf. mapSubexprs
).
Please consider using //-
if you are replacing just terminal values
as it is faster.
Given that:
> let xx = var "x" (undefined :: Int) > let yy = var "y" (undefined :: Int) > let zz = var "z" (undefined :: Int) > let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy
Then:
> ((xx -+- yy) -+- (yy -+- zz)) // [(xx -+- yy, yy), (yy -+- zz, yy)] y + y :: Int
> ((xx -+- yy) -+- zz) // [(xx -+- yy, zz), (zz, xx -+- yy)] z + (x + y) :: Int
Replacement happens only once with outer expressions having more precedence than inner expressions.
> (xx -+- yy) // [(yy,xx), (xx -+- yy,zz), (zz,xx)] z :: Int
Given that the argument list has length m, this function is O(n*n*m). Remember that since n is the size of an expression, comparing two expressions is O(n) in the worst case, and we may need to compare with n subexpressions in the worst case.
fill :: Expr -> [Expr] -> Expr #
Fill holes in an expression with the given list.
> let i_ = hole (undefined :: Int) > let e1 -+- e2 = value "+" ((+) :: Int -> Int -> Int) :$ e1 :$ e2 > let xx = var "x" (undefined :: Int) > let yy = var "y" (undefined :: Int)
> fill (i_ -+- i_) [xx, yy] x + y :: Int
> fill (i_ -+- i_) [xx, xx] x + x :: Int
> let one = val (1::Int)
> fill (i_ -+- i_) [one, one -+- one] 1 + (1 + 1) :: Int
This function silently remaining expressions:
> fill i_ [xx, yy] x :: Int
This function silently keeps remaining holes:
> fill (i_ -+- i_ -+- i_) [xx, yy] (x + y) + _ :: Int
This function silently skips remaining holes if one is not of the right type:
> fill (i_ -+- i_ -+- i_) [xx, val 'c', yy] (x + _) + _ :: Int
O(n).
Folds a list of Expr
s 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 Expr
s, such as
canonicalize
,
mapValues
or
canonicalVariations
.
> let ii = var "i" (undefined::Int) > let kk = var "k" (undefined::Int) > let qq = var "q" (undefined::Bool) > let notE = value "not" not > unfold . canonicalize . fold $ [ii,kk,notE :$ qq, notE :$ val False] [x :: Int,y :: Int,not p :: Bool,not False :: Bool]
evaluate :: Typeable a => Expr -> Maybe a #
O(n).
Just
the value of an expression when possible (correct type),
Nothing
otherwise.
This does not catch errors from undefined
Dynamic
value
s.
> 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
(>$$<) :: [Expr] -> [Expr] -> [Expr] #
Lists valid applications between lists of Expr
s
> [notE, plus] >$$< [false, true, zero] [not False :: Bool,not True :: Bool,(0 +) :: Int -> Int]
O(n). Returns the size of the given expression, i.e. the number of terminal values in it.
zero = val (0 :: Int) one = val (1 :: Int) two = val (2 :: Int) xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy abs' xx = value "abs" (abs :: Int->Int) :$ xx
> size zero 1
> size (one -+- two) 3
> size (abs' one) 2
value :: Typeable a => String -> a -> Expr #
O(1).
It takes a string representation of a value and a value, returning an
Expr
with that terminal value.
For instances of Show
, it is preferable to use val
.
> value "0" (0 :: Integer) 0 :: Integer
> value "'a'" 'a' 'a' :: Char
> value "True" True True :: Bool
> value "id" (id :: Int -> Int) id :: Int -> Int
> value "(+)" ((+) :: Int -> Int -> Int) (+) :: Int -> Int -> Int
> value "sort" (sort :: [Bool] -> [Bool]) sort :: [Bool] -> [Bool]
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'
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
Function composition encoded as an Expr
:
> compose (.) :: (Int -> Int) -> (Int -> Int) -> Int -> Int
match :: Expr -> Expr -> Maybe [(Expr, Expr)] #
Given two expressions, returns a Just
list of matches
of subexpressions of the first expressions
to variables in the second expression.
Returns Nothing
when there is no match.
> let zero = val (0::Int) > let one = val (1::Int) > let xx = var "x" (undefined :: Int) > let yy = var "y" (undefined :: Int) > let e1 -+- e2 = value "+" ((+)::Int->Int->Int) :$ e1 :$ e2
> (zero -+- one) `match` (xx -+- yy) Just [(y :: Int,1 :: Int),(x :: Int,0 :: Int)]
> (zero -+- (one -+- two)) `match` (xx -+- yy) Just [(y :: Int,1 + 2 :: Int),(x :: Int,0 :: Int)]
> (zero -+- (one -+- two)) `match` (xx -+- (yy -+- yy)) Nothing
In short:
(zero -+- one) `match` (xx -+- yy) = Just [(xx,zero), (yy,one)] (zero -+- (one -+- two)) `match` (xx -+- yy) = Just [(xx,zero), (yy,one-+-two)] (zero -+- (one -+- two)) `match` (xx -+- (yy -+- yy)) = Nothing
canonicalize :: Expr -> Expr #
Canonicalizes an Expr
so that variable names appear in order.
Variable names are taken from the preludeNameInstances
.
> canonicalize (xx -+- yy) x + y :: Int
> canonicalize (yy -+- xx) x + y :: Int
> canonicalize (xx -+- xx) x + x :: Int
> canonicalize (yy -+- yy) x + x :: Int
Constants are untouched:
> canonicalize (jj -+- (zero -+- abs' ii)) x + (y + abs y) :: Int
This also works for variable functions:
> canonicalize (gg yy -+- ff xx -+- gg xx) (f x + g y) + f y :: Int
mapValues :: (Expr -> Expr) -> Expr -> Expr #
O(n*m).
Applies a function to all terminal values in an expression.
(cf. //-
)
Given that:
> let zero = val (0 :: Int) > let one = val (1 :: Int) > let two = val (2 :: Int) > let three = val (3 :: Int) > let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy > let intToZero e = if typ e == typ zero then zero else e
Then:
> one -+- (two -+- three) 1 + (2 + 3) :: Int
> mapValues intToZero $ one -+- (two -+- three) 0 + (0 + 0) :: Integer
Given that the argument function is O(m), this function is O(n*m).
canonicalVariations :: Expr -> [Expr] #
Returns all canonical variations of an Expr
by filling holes with variables.
Where possible, variations are listed
from most general to least general.
> canonicalVariations $ i_ [x :: Int]
> canonicalVariations $ i_ -+- i_ [ x + y :: Int , x + x :: Int ]
> canonicalVariations $ i_ -+- i_ -+- i_ [ (x + y) + z :: Int , (x + y) + x :: Int , (x + y) + y :: Int , (x + x) + y :: Int , (x + x) + x :: Int ]
> canonicalVariations $ i_ -+- ord' c_ [x + ord c :: Int]
> canonicalVariations $ i_ -+- i_ -+- ord' c_ [ (x + y) + ord c :: Int , (x + x) + ord c :: Int ]
> canonicalVariations $ i_ -+- i_ -+- length' (c_ -:- unit c_) [ (x + y) + length (c:d:"") :: Int , (x + y) + length (c:c:"") :: Int , (x + x) + length (c:d:"") :: Int , (x + x) + length (c:c:"") :: Int ]
In an expression without holes this functions just returns a singleton list with the expression itself:
> canonicalVariations $ val (0 :: Int) [0 :: Int]
> canonicalVariations $ ord' bee [ord 'b' :: Int]
When applying this to expressions already containing variables clashes are avoided and these variables are not touched:
> canonicalVariations $ i_ -+- ii -+- jj -+- i_ [ x + i + j + y :: Int , x + i + j + y :: Int ]
> canonicalVariations $ ii -+- jj [i + j :: Int]
> canonicalVariations $ xx -+- i_ -+- i_ -+- length' (c_ -:- unit c_) -+- yy [ (((x + z) + x') + length (c:d:"")) + y :: Int , (((x + z) + x') + length (c:c:"")) + y :: Int , (((x + z) + z) + length (c:d:"")) + y :: Int , (((x + z) + z) + length (c:c:"")) + y :: Int ]
deriveExpress :: Name -> DecsQ #
variableNamesFromTemplate :: String -> [String] #
Returns an infinite list of variable names based on the given template.
> variableNamesFromTemplate "x" ["x", "y", "z", "x'", "y'", ...]
> variableNamesFromTemplate "p" ["p", "q", "r", "p'", "q'", ...]
> variableNamesFromTemplate "xy" ["xy", "zw", "xy'", "zw'", "xy''", ...]
names :: Name a => a -> [String] #
Returns na infinite list of variable names from the given type:
the result of variableNamesFromTemplate
after name
.
> names (undefined :: Int) ["x", "y", "z", "x'", "y'", "z'", "x''", "y''", "z''", ...]
> names (undefined :: Bool) ["p", "q", "r", "p'", "q'", "r'", "p''", "q''", "r''", ...]
> names (undefined :: [Int]) ["xs", "ys", "zs", "xs'", "ys'", "zs'", "xs''", "ys''", ...]
isInstanceOf :: Expr -> Expr -> Bool #
Given two Expr
s,
checks if the first expression
is an instance of the second
in terms of variables.
(cf. encompasses
, hasInstanceOf
)
> let zero = val (0::Int) > let one = val (1::Int) > let xx = var "x" (undefined :: Int) > let yy = var "y" (undefined :: Int) > let e1 -+- e2 = value "+" ((+)::Int->Int->Int) :$ e1 :$ e2
one `isInstanceOf` one = True xx `isInstanceOf` xx = True yy `isInstanceOf` xx = True zero `isInstanceOf` xx = True xx `isInstanceOf` zero = False one `isInstanceOf` zero = False (xx -+- (yy -+- xx)) `isInstanceOf` (xx -+- yy) = True (yy -+- (yy -+- xx)) `isInstanceOf` (xx -+- yy) = True (zero -+- (yy -+- xx)) `isInstanceOf` (zero -+- yy) = True (one -+- (yy -+- xx)) `isInstanceOf` (zero -+- yy) = False
deriveName :: Name -> DecsQ #
deriveNameIfNeeded :: Name -> DecsQ #
Same as deriveName
but does not warn when instance already exists
(deriveName
is preferable).
deriveNameCascading :: Name -> DecsQ #
($$) :: Expr -> Expr -> Maybe Expr #
O(n).
Creates an Expr
representing a function application.
Just
an Expr
application if the types match, Nothing
otherwise.
(cf. :$
)
> value "id" (id :: () -> ()) $$ val () Just (id () :: ())
> value "abs" (abs :: Int -> Int) $$ val (1337 :: Int) Just (abs 1337 :: Int)
> value "abs" (abs :: Int -> Int) $$ val 'a' Nothing
> value "abs" (abs :: Int -> Int) $$ val () Nothing
var :: Typeable a => String -> a -> Expr #
O(1).
Creates an Expr
representing a variable with the given name and argument
type.
> var "x" (undefined :: Int) x :: Int
> var "u" (undefined :: ()) u :: ()
> var "xs" (undefined :: [Int]) xs :: [Int]
This function follows the underscore convention:
a variable is just a value
whose string representation
starts with underscore ('_'
).
etyp :: Expr -> Either (TypeRep, TypeRep) TypeRep #
O(n). Computes the type of an expression returning either the type of the given expression when possible or when there is a type error, the pair of types which produced the error.
> let one = val (1 :: Int) > let bee = val 'b' > let absE = value "abs" (abs :: Int -> Int)
> etyp one Right Int
> etyp bee Right Char
> etyp absE Right (Int -> Int)
> etyp (absE :$ one) Right Int
> etyp (absE :$ bee) Left (Int -> Int, Char)
> etyp ((absE :$ bee) :$ one) Left (Int -> Int, Char)
isIllTyped :: Expr -> Bool #
O(n).
Returns whether the given Expr
is ill typed.
(cf. isWellTyped
)
> let one = val (1 :: Int) > let bee = val 'b' > let absE = value "abs" (abs :: Int -> Int)
> isIllTyped (absE :$ val (1 :: Int)) False
> isIllTyped (absE :$ val 'b') True
isWellTyped :: Expr -> Bool #
O(n).
Returns whether the given Expr
is well typed.
(cf. isIllTyped
)
> isWellTyped (absE :$ val (1 :: Int)) True
> isWellTyped (absE :$ val 'b') False
eval :: Typeable a => a -> Expr -> a #
O(n). Evaluates an expression when possible (correct type). Returns a default value otherwise.
> let two = val (2 :: Int) > let three = val (3 :: Int) > let e1 -+- e2 = value "+" ((+) :: Int->Int->Int) :$ e1 :$ e2
> eval 0 $ two -+- three :: Int 5
> eval 'z' $ two -+- three :: Char 'z'
> eval 0 $ two -+- val '3' :: Int 0
toDynamic :: Expr -> Maybe Dynamic #
O(n).
Evaluates an expression to a terminal Dynamic
value when possible.
Returns Nothing
otherwise.
> toDynamic $ val (123 :: Int) :: Maybe Dynamic Just <<Int>>
> toDynamic $ value "abs" (abs :: Int -> Int) :$ val (-1 :: Int) Just <<Int>>
> toDynamic $ value "abs" (abs :: Int -> Int) :$ val 'a' Nothing
showOpExpr :: String -> Expr -> String #
O(n).
Like showPrecExpr
but
the precedence is taken from the given operator name.
> showOpExpr "*" (two -*- three) "(2 * 3)"
> showOpExpr "+" (two -*- three) "2 * 3"
To imply that the surrounding environment is a function application,
use " "
as the given operator.
> showOpExpr " " (two -*- three) "(2 * 3)"
showPrecExpr :: Int -> Expr -> String #
O(n).
Like showExpr
but allows specifying the surrounding precedence.
> showPrecExpr 6 (one -+- two) "1 + 2"
> showPrecExpr 7 (one -+- two) "(1 + 2)"
O(n).
Returns a string representation of an expression.
Differently from show
(:: Expr -> String
)
this function does not include the type in the output.
> putStrLn $ showExpr (one -+- two) 1 + 2
> putStrLn $ showExpr $ (pp -||- true) -&&- (qq -||- false) (p || True) && (q || False)
compareComplexity :: Expr -> Expr -> Ordering #
O(n).
Compares the complexity of two Expr
s.
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.
compareLexicographically :: Expr -> Expr -> Ordering #
O(n).
Lexicographical structural comparison of Expr
s
where variables < constants < applications
then types are compared before string representations.
> compareLexicographically one (one -+- one) LT > compareLexicographically one zero GT > compareLexicographically (xx -+- zero) (zero -+- xx) LT > compareLexicographically (zero -+- xx) (zero -+- xx) EQ
(cf. compareTy
)
This comparison is a total order.
compareQuickly :: Expr -> Expr -> Ordering #
O(n).
A fast total order between Expr
s
that can be used when sorting Expr
values.
This is lazier than its counterparts
compareComplexity
and compareLexicographically
and tries to evaluate the given Expr
s as least as possible.
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]
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
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
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)
O(n) for the spine, O(n^2) for full evaluation.
Lists subexpressions of a given expression in order and with repetitions.
This includes the expression itself and partial function applications.
(cf. nubSubexprs
)
> subexprs (xx -+- yy) [ x + y :: Int , (x +) :: Int -> Int , (+) :: Int -> Int -> Int , x :: Int , y :: Int ]
> subexprs (pp -&&- (pp -&&- true)) [ p && (p && True) :: Bool , (p &&) :: Bool -> Bool , (&&) :: Bool -> Bool -> Bool , p :: Bool , p && True :: Bool , (p &&) :: Bool -> Bool , (&&) :: Bool -> Bool -> Bool , p :: Bool , True :: Bool ]
nubSubexprs :: Expr -> [Expr] #
O(n^3) for full evaluation.
Lists all subexpressions of a given expression without repetitions.
This includes the expression itself and partial function applications.
(cf. subexprs
)
> nubSubexprs (xx -+- yy) [ x :: Int , y :: Int , (+) :: Int -> Int -> Int , (x +) :: Int -> Int , x + y :: Int ]
> nubSubexprs (pp -&&- (pp -&&- true)) [ p :: Bool , True :: Bool , (&&) :: Bool -> Bool -> Bool , (p &&) :: Bool -> Bool , p && True :: Bool , p && (p && True) :: Bool ]
Runtime averages to
O(n^2 log n) on evenly distributed expressions
such as (f x + g y) + (h z + f w)
;
and to O(n^3) on deep expressions
such as f (g (h (f (g (h x)))))
.
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 ]
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)))))
.
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 ]
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)))))
.
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]
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)))))
.
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.
O(n).
Returns the maximum height of a given expression
given by the maximum number of nested function applications.
Curried function application is counted each time,
i.e. the application of a two argument function
increases the depth of its first argument by two
and of its second argument by one.
(cf. depth
)
With:
zero = val (0 :: Int) one = val (1 :: Int) two = val (2 :: Int) const' xx yy = value "const" (const :: Int->Int->Int) :$ xx :$ yy abs' xx = value "abs" (abs :: Int->Int) :$ xx
Then:
> height zero 1
> height (abs' one) 2
> height ((const' one) two) 3
> height ((const' (abs' one)) two) 4
> height ((const' one) (abs' two)) 3
Flipping arguments of applications in subterms may change the result of the function.
matchWith :: [(Expr, Expr)] -> Expr -> Expr -> Maybe [(Expr, Expr)] #
Like match
but allowing predefined bindings.
matchWith [(xx,zero)] (zero -+- one) (xx -+- yy) = Just [(xx,zero), (yy,one)] matchWith [(xx,one)] (zero -+- one) (xx -+- yy) = Nothing
encompasses :: Expr -> Expr -> Bool #
Given two Expr
s,
checks if the first expression
encompasses the second expression
in terms of variables.
This is equivalent to flipping the arguments of isInstanceOf
.
zero `encompasses` xx = False xx `encompasses` zero = True
hasInstanceOf :: Expr -> Expr -> Bool #
isSubexprOf :: Expr -> Expr -> Bool #
O(n^2).
Checks if an Expr
is a subexpression of another.
> (xx -+- yy) `isSubexprOf` (zz -+- (xx -+- yy)) True
> (xx -+- yy) `isSubexprOf` abs' (yy -+- xx) False
> xx `isSubexprOf` yy False
mapVars :: (Expr -> Expr) -> Expr -> Expr #
O(n*m). Applies a function to all variables in an expression.
Given that:
> let primeify e = if isVar e | then case e of (Value n d) -> Value (n ++ "'") d | else e > let xx = var "x" (undefined :: Int) > let yy = var "y" (undefined :: Int) > let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy
Then:
> xx -+- yy x + y :: Int
> primeify xx x' :: Int
> mapVars primeify $ xx -+- yy x' + y' :: Int
> mapVars (primeify . primeify) $ xx -+- yy x'' + y'' :: Int
Given that the argument function is O(m), this function is O(n*m).
mapConsts :: (Expr -> Expr) -> Expr -> Expr #
O(n*m). Applies a function to all terminal constants in an expression.
Given that:
> let one = val (1 :: Int) > let two = val (2 :: Int) > let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy > let intToZero e = if typ e == typ zero then zero else e
Then:
> one -+- (two -+- xx) 1 + (2 + x) :: Int
> mapConsts intToZero (one -+- (two -+- xx)) 0 + (0 + x) :: Integer
Given that the argument function is O(m), this function is O(n*m).
mapSubexprs :: (Expr -> Maybe Expr) -> Expr -> Expr #
O(n*m).
Substitute subexpressions of an expression using the given function.
Outer expressions have more precedence than inner expressions.
(cf. //
)
With:
> let xx = var "x" (undefined :: Int) > let yy = var "y" (undefined :: Int) > let zz = var "z" (undefined :: Int) > let plus = value "+" ((+) :: Int->Int->Int) > let times = value "*" ((*) :: Int->Int->Int) > let xx -+- yy = plus :$ xx :$ yy > let xx -*- yy = times :$ xx :$ yy
> let pluswap (o :$ xx :$ yy) | o == plus = Just $ o :$ yy :$ xx | pluswap _ = Nothing
Then:
> mapSubexprs pluswap $ (xx -*- yy) -+- (yy -*- zz) y * z + x * y :: Int
> mapSubexprs pluswap $ (xx -+- yy) -*- (yy -+- zz) (y + x) * (z + y) :: Int
Substitutions do not stack, in other words a replaced expression or its subexpressions are not further replaced:
> mapSubexprs pluswap $ (xx -+- yy) -+- (yy -+- zz) (y + z) + (x + y) :: Int
Given that the argument function is O(m), this function is O(n*m).
(//-) :: Expr -> [(Expr, Expr)] -> Expr #
O(n*m).
Substitute occurrences of values in an expression
from the given list of substitutions.
(cf. mapValues
)
Given that:
> let xx = var "x" (undefined :: Int) > let yy = var "y" (undefined :: Int) > let zz = var "z" (undefined :: Int) > let xx -+- yy = value "+" ((+) :: Int->Int->Int) :$ xx :$ yy
Then:
> ((xx -+- yy) -+- (yy -+- zz)) //- [(xx, yy), (zz, yy)] (y + y) + (y + y) :: Int
> ((xx -+- yy) -+- (yy -+- zz)) //- [(yy, yy -+- zz)] (x + (y + z)) + ((y + z) + z) :: Int
This function does not work for substituting non-terminal subexpressions:
> (xx -+- yy) //- [(xx -+- yy, zz)] x + y :: Int
Please use the slower //
if you want the above replacement to work.
Replacement happens only once:
> xx //- [(xx,yy), (yy,zz)] y :: Int
Given that the argument list has length m, this function is O(n*m).
renameVarsBy :: (String -> String) -> Expr -> Expr #
Rename variables in an Expr
.
> renameVarsBy (++ "'") (xx -+- yy) x' + y' :: Int
> renameVarsBy (++ "'") (yy -+- (zz -+- xx)) (y' + (z' + x')) :: Int
> renameVarsBy (++ "1") (abs' xx) abs x1 :: Int
> renameVarsBy (++ "2") $ abs' (xx -+- yy) abs (x2 + y2) :: Int
NOTE: this will affect holes!
varAsTypeOf :: String -> Expr -> Expr #
holeAsTypeOf :: Expr -> Expr #
hole :: Typeable a => a -> Expr #
O(1).
Creates an Expr
representing a typed hole of the given argument type.
> hole (undefined :: Int) _ :: Int
> hole (undefined :: Maybe String) _ :: Maybe [Char]
A hole is represented as a variable with no name or
a value named "_"
:
hole x = var "" x hole x = value "_" x
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]
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)))))
.
O(n). Returns whether an expression contains a hole
> hasHole $ hole (undefined :: Bool) True
> hasHole $ value "not" not :$ val True False
> hasHole $ value "not" not :$ hole (undefined :: Bool) True
isComplete :: Expr -> Bool #
O(n). Returns whether an expression is complete. A complete expression is one without holes.
> isComplete $ hole (undefined :: Bool) False
> isComplete $ value "not" not :$ val True True
> isComplete $ value "not" not :$ hole (undefined :: Bool) False
isComplete
is the negation of hasHole
.
isComplete = not . hasHole
isComplete
is to hasHole
what
isGround
is to hasVar
.
listVars :: Typeable a => String -> a -> [Expr] #
Generate an infinite list of variables
based on a template and a given type.
(cf. listVarsAsTypeOf
)
> putL 10 $ listVars "x" (undefined :: Int) [ x :: Int , y :: Int , z :: Int , x' :: Int , y' :: Int , z' :: Int , x'' :: Int , ... ]
> putL 10 $ listVars "p" (undefined :: Bool) [ p :: Bool , q :: Bool , r :: Bool , p' :: Bool , q' :: Bool , r' :: Bool , p'' :: Bool , ... ]
listVarsAsTypeOf :: String -> Expr -> [Expr] #
Generate an infinite list of variables
based on a template
and the type of a given Expr
.
(cf. listVars
)
> let one = val (1::Int) > putL 10 $ "x" `listVarsAsTypeOf` one [ x :: Int , y :: Int , z :: Int , x' :: Int , ... ]
> let false = val False > putL 10 $ "p" `listVarsAsTypeOf` false [ p :: Bool , q :: Bool , r :: Bool , p' :: Bool , ... ]
O(n).
Folds a list of Expr
with function application (:$
).
This reverses the effect of unfoldApp
.
foldApp [e0] = e0 foldApp [e0,e1] = e0 :$ e1 foldApp [e0,e1,e2] = e0 :$ e1 :$ e2 foldApp [e0,e1,e2,e3] = e0 :$ e1 :$ e2 :$ e3
Remember :$
is left-associative, so:
foldApp [e0] = e0 foldApp [e0,e1] = (e0 :$ e1) foldApp [e0,e1,e2] = ((e0 :$ e1) :$ e2) foldApp [e0,e1,e2,e3] = (((e0 :$ e1) :$ e2) :$ e3)
This function may produce an ill-typed expression.
foldPair :: (Expr, Expr) -> Expr #
O(1).
Folds a pair of Expr
values into a single Expr
.
(cf. unfoldPair
)
This always generates an ill-typed expression, as it uses a fake pair constructor.
> foldPair (val False, val (1::Int)) (False,1) :: ill-typed # ExprPair $ Bool #
> foldPair (val (0::Int), val True) (0,True) :: ill-typed # ExprPair $ Int #
This is useful when applying transformations on pairs of Expr
s, such as
canonicalize
,
mapValues
or
canonicalVariations
.
> let ii = var "i" (undefined::Int) > let kk = var "k" (undefined::Int) > unfoldPair $ canonicalize $ foldPair (ii,kk) (x :: Int,y :: Int)
unfoldPair :: Expr -> (Expr, Expr) #
foldTrio :: (Expr, Expr, Expr) -> Expr #
O(1).
Folds a trio/triple of Expr
values into a single Expr
.
(cf. unfoldTrio
)
This always generates an ill-typed expression as it uses a fake trio/triple constructor.
> foldTrio (val False, val (1::Int), val 'a') (False,1,'a') :: ill-typed # ExprTrio $ Bool #
> foldTrio (val (0::Int), val True, val 'b') (0,True,'b') :: ill-typed # ExprTrio $ Int #
This is useful when applying transformations on pairs of Expr
s, such as
canonicalize
,
mapValues
or
canonicalVariations
.
> let ii = var "i" (undefined::Int) > let kk = var "k" (undefined::Int) > let zz = var "z" (undefined::Int) > unfoldPair $ canonicalize $ foldPair (ii,kk,zz) (x :: Int,y :: Int,z :: Int)
unfoldTrio :: Expr -> (Expr, Expr, Expr) #
O(1).
Unfolds an Expr
representing a trio/triple.
This reverses the effect of foldTrio
.
> value ",," ((,,) :: Bool->Bool->Bool->(Bool,Bool,Bool)) :$ val True :$ val False :$ val True (True,False,True) :: (Bool,Bool,Bool) > unfoldTrio $ value ",," ((,,) :: Bool->Bool->Bool->(Bool,Bool,Bool)) :$ val True :$ val False :$ val True (True :: Bool,False :: Bool,True :: Bool)
(cf. unfoldPair
)
deriveExpressIfNeeded :: Name -> DecsQ #
Same as deriveExpress
but does not warn when instance already exists
(deriveExpress
is preferable).
deriveExpressCascading :: Name -> DecsQ #
reifyEq :: (Typeable a, Eq a) => a -> [Expr] #
O(1).
Reifies an Eq
instance into a list of Expr
s.
The list will contain ==
and /=
for the given type.
(cf. mkEq
, mkEquation
)
> reifyEq (undefined :: Int) [ (==) :: Int -> Int -> Bool , (/=) :: Int -> Int -> Bool ]
> reifyEq (undefined :: Bool) [ (==) :: Bool -> Bool -> Bool , (/=) :: Bool -> Bool -> Bool ]
> reifyEq (undefined :: String) [ (==) :: [Char] -> [Char] -> Bool , (/=) :: [Char] -> [Char] -> Bool ]
reifyOrd :: (Typeable a, Ord a) => a -> [Expr] #
O(1).
Reifies an Ord
instance into a list of Expr
s.
The list will contain compare
, <=
and <
for the given type.
(cf. mkOrd
, mkOrdLessEqual
, mkComparisonLE
, mkComparisonLT
)
> reifyOrd (undefined :: Int) [ (<=) :: Int -> Int -> Bool , (<) :: Int -> Int -> Bool ]
> reifyOrd (undefined :: Bool) [ (<=) :: Bool -> Bool -> Bool , (<) :: Bool -> Bool -> Bool ]
> reifyOrd (undefined :: [Bool]) [ (<=) :: [Bool] -> [Bool] -> Bool , (<) :: [Bool] -> [Bool] -> Bool ]
reifyEqOrd :: (Typeable a, Ord a) => a -> [Expr] #
reifyName :: (Typeable a, Name a) => a -> [Expr] #
O(1).
Reifies a Name
instance into a list of Expr
s.
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]]
mkOrd :: Typeable a => (a -> a -> Ordering) -> [Expr] #
O(1).
Builds a reified Ord
instance from the given compare
function.
(cf. reifyOrd
, mkOrdLessEqual
)
mkOrdLessEqual :: Typeable a => (a -> a -> Bool) -> [Expr] #
mkName :: Typeable a => (a -> String) -> [Expr] #
O(1).
Builds a reified Name
instance from the given name
function.
(cf. reifyName
, mkNameWith
)
mkNameWith :: Typeable a => String -> a -> [Expr] #
lookupComparison :: String -> TypeRep -> [Expr] -> Maybe Expr #
O(n).
Lookups for a comparison function (:: a -> a -> Bool
)
with the given name and argument type.
isEqT :: [Expr] -> TypeRep -> Bool #
O(n).
Returns whether an Eq
instance exists in the given instances list
for the given TypeRep
.
> isEqT (reifyEqOrd (undefined :: Int)) (typeOf (undefined :: Int)) True
> isEqT (reifyEqOrd (undefined :: Int)) (typeOf (undefined :: [[[Int]]])) False
Given that the instances list has length n, this function is O(n).
isOrdT :: [Expr] -> TypeRep -> Bool #
O(n).
Returns whether an Ord
instance exists in the given instances list
for the given TypeRep
.
> isOrdT (reifyEqOrd (undefined :: Int)) (typeOf (undefined :: Int)) True
> isOrdT (reifyEqOrd (undefined :: Int)) (typeOf (undefined :: [[[Int]]])) False
Given that the instances list has length n, this function is O(n).
isEq :: [Expr] -> Expr -> Bool #
O(n+m).
Returns whether an Eq
instance exists in the given instances list
for the given Expr
.
> isEq (reifyEqOrd (undefined :: Int)) (val (0::Int)) True
> isEq (reifyEqOrd (undefined :: Int)) (val ([[[0::Int]]])) False
Given that the instances list has length m
and that the given Expr
has size n,
this function is O(n+m).
isOrd :: [Expr] -> Expr -> Bool #
O(n+m).
Returns whether an Ord
instance exists in the given instances list
for the given Expr
.
> isOrd (reifyEqOrd (undefined :: Int)) (val (0::Int)) True
> isOrd (reifyEqOrd (undefined :: Int)) (val ([[[0::Int]]])) False
Given that the instances list has length m
and that the given Expr
has size n,
this function is O(n+m).
mkComparison :: String -> [Expr] -> Expr -> Expr -> Expr #
O(n+m).
Like mkEquation
, mkComparisonLE
and mkComparisonLT
but allows providing the binary operator name.
When not possible, this function returns False
encoded as an Expr
.
lookupName :: [Expr] -> Expr -> String #
lookupNames :: [Expr] -> Expr -> [String] #
O(n+m).
A mix between lookupName
and names
:
this returns an infinite list of names
based on an instances list and an Expr
.
listVarsWith :: [Expr] -> Expr -> [Expr] #
O(n+m).
Like lookupNames
but returns a list of variables encoded as Expr
s.
validApps :: [Expr] -> Expr -> [Expr] #
Given a list of functional expressions and another expression, returns a list of valid applications.
preludeNameInstances :: [Expr] #
canonicalizeWith :: (Expr -> [String]) -> Expr -> Expr #
Like canonicalize
but allows customization
of the list of variable names.
(cf. lookupNames
, variableNamesFromTemplate
)
> canonicalizeWith (const ["i","j","k","l",...]) (xx -+- yy) i + j :: Int
The argument Expr
of the argument function allows
to provide a different list of names for different types:
> let namesFor e > | typ e == typeOf (undefined::Char) = variableNamesFromTemplate "c1" > | typ e == typeOf (undefined::Int) = variableNamesFromTemplate "i" > | otherwise = variableNamesFromTemplate "x"
> canonicalizeWith namesFor ((xx -+- ord' dd) -+- (ord' cc -+- yy)) (i + ord c1) + (ord c2 + j) :: Int
canonicalizationWith :: (Expr -> [String]) -> Expr -> [(Expr, Expr)] #
Like canonicalization
but allows customization
of the list of variable names.
(cf. lookupNames
, variableNamesFromTemplate
)
isCanonicalWith :: (Expr -> [String]) -> Expr -> Bool #
Like isCanonical
but allows specifying
the list of variable names.
canonicalization :: Expr -> [(Expr, Expr)] #
Return a canonicalization of an Expr
that makes variable names appear in order
using names
as provided by preludeNameInstances
.
By using //-
it can canonicalize
Expr
s.
> canonicalization (gg yy -+- ff xx -+- gg xx) [ (x :: Int, y :: Int) , (f :: Int -> Int, g :: Int -> Int) , (y :: Int, x :: Int) , (g :: Int -> Int, f :: Int -> Int) ]
> canonicalization (yy -+- xx -+- yy) [ (x :: Int, y :: Int) , (y :: Int, x :: Int) ]
isCanonical :: Expr -> Bool #
Returns whether an Expr
is canonical:
if applying canonicalize
is an identity
using names
as provided by preludeNameInstances
.
mostGeneralCanonicalVariation :: Expr -> Expr #
Returns the most general canonical variation of an Expr
by filling holes with variables.
> mostGeneralCanonicalVariation $ i_ x :: Int
> mostGeneralCanonicalVariation $ i_ -+- i_ x + y :: Int
> mostGeneralCanonicalVariation $ i_ -+- i_ -+- i_ (x + y) + z :: Int
> mostGeneralCanonicalVariation $ i_ -+- ord' c_ x + ord c :: Int
> mostGeneralCanonicalVariation $ i_ -+- i_ -+- ord' c_ (x + y) + ord c :: Int
> mostGeneralCanonicalVariation $ i_ -+- i_ -+- length' (c_ -:- unit c_) (x + y) + length (c:d:"") :: Int
In an expression without holes this functions just returns the given expression itself:
> mostGeneralCanonicalVariation $ val (0 :: Int) 0 :: Int
> mostGeneralCanonicalVariation $ ord' bee ord 'b' :: Int
This function is the same as taking the head
of canonicalVariations
but a bit faster.
mostSpecificCanonicalVariation :: Expr -> Expr #
Returns the most specific canonical variation of an Expr
by filling holes with variables.
> mostSpecificCanonicalVariation $ i_ x :: Int
> mostSpecificCanonicalVariation $ i_ -+- i_ x + x :: Int
> mostSpecificCanonicalVariation $ i_ -+- i_ -+- i_ (x + x) + x :: Int
> mostSpecificCanonicalVariation $ i_ -+- ord' c_ x + ord c :: Int
> mostSpecificCanonicalVariation $ i_ -+- i_ -+- ord' c_ (x + x) + ord c :: Int
> mostSpecificCanonicalVariation $ i_ -+- i_ -+- length' (c_ -:- unit c_) (x + x) + length (c:c:"") :: Int
In an expression without holes this functions just returns the given expression itself:
> mostSpecificCanonicalVariation $ val (0 :: Int) 0 :: Int
> mostSpecificCanonicalVariation $ ord' bee ord 'b' :: Int
This function is the same as taking the last
of canonicalVariations
but a bit faster.
fastCanonicalVariations :: Expr -> [Expr] #
A faster version of canonicalVariations
that
disregards name clashes across different types.
Results are confusing to the user
but fine for Express which differentiates
between variables with the same name but different types.
Without applying canonicalize
, the following Expr
may seem to have only one variable:
> fastCanonicalVariations $ i_ -+- ord' c_ [x + ord x :: Int]
Where in fact it has two, as the second x
has a different type.
Applying canonicalize
disambiguates:
> map canonicalize . fastCanonicalVariations $ i_ -+- ord' c_ [x + ord c :: Int]
This function is useful when resulting Expr
s are
not intended to be presented to the user
but instead to be used by another function.
It is simply faster to skip the step where clashes are resolved.
fastMostGeneralVariation :: Expr -> Expr #
A faster version of mostGeneralCanonicalVariation
that disregards name clashes across different types.
Consider using mostGeneralCanonicalVariation
instead.
The same caveats of fastCanonicalVariations
do apply here.
fastMostSpecificVariation :: Expr -> Expr #
A faster version of mostSpecificCanonicalVariation
that disregards name clashes across different types.
Consider using mostSpecificCanonicalVariation
instead.
The same caveats of fastCanonicalVariations
do apply here.
(-==>-) :: Expr -> Expr -> Expr infixr 0 #
The function ==>
lifted over Expr
s.
> false -==>- true False ==> True :: Bool
> evl $ false -==>- true :: Bool True
A variable function f
of 'Int -> Int' type lifted over the Expr
type.
> ff xx f x :: Int
> ff one f 1 :: Int
A variable function g
of 'Int -> Int' type lifted over the Expr
type.
> gg yy g y :: Int
> gg minusTwo gg (-2) :: Int
A variable function h
of 'Int -> Int' type lifted over the Expr
type.
> hh zz h z :: Int
(-?-) :: Expr -> Expr -> Expr #
A variable binary operator ?
lifted over the Expr
type.
Works for Int
, Bool
, Char
, [Int]
and String
.
> xx -?- yy x ? y :: Int
> pp -?- qq p ? q :: Bool
> xx -?- qq *** Exception: (-?-): unhandled type: 1 :: Int, False :: Bool accepted types are: (?) :: Int -> Int -> Int (?) :: Bool -> Bool -> Bool (?) :: Char -> Char -> Char (?) :: [Int] -> [Int] -> [Int] (?) :: [Char] -> [Char] -> [Char] (?) :: Int -> [Int] -> [Int] (?) :: Char -> [Char] -> [Char]
A variable binary operator o
lifted over the Expr
type.
Works for Int
, Bool
, Char
, [Int]
and String
.
> xx `oo` yy x `o` y :: Int
> pp `oo` qq p `o` q :: Bool
> xx `oo` qq *** Exception: oo: unhandled type: 1 :: Int, False :: Bool accepted types are: o :: Int -> Int -> Int o :: Bool -> Bool -> Bool o :: Char -> Char -> Char o :: [Int] -> [Int] -> [Int] o :: [Char] -> [Char] -> [Char]
emptyString :: Expr #
(-/=-) :: Expr -> Expr -> Expr infix 4 #
Constructs an inequation between two Expr
s.
> xx -/=- zero x /= 0 :: Bool
> cc -/=- ae c /= 'a' :: Bool
(-<=-) :: Expr -> Expr -> Expr infix 4 #
Constructs a less-than-or-equal inequation between two Expr
s.
> xx -<=- zero x <= 0 :: Bool
> cc -<=- ae c <= 'a' :: Bool
(-<-) :: Expr -> Expr -> Expr infix 4 #
Constructs a less-than inequation between two Expr
s.
> xx -<- zero x < 0 :: Bool
> cc -<- bee c < 'b' :: Bool
if' :: Expr -> Expr -> Expr -> Expr #
A function if :: Bool -> a -> a -> a
lifted over the Expr
type
that encodes if-then-else functionality.
This is properly displayed as an if-then-else.
> if' pp zero xx (if p then 0 else x) :: Int
> zz -*- if' pp xx yy z * (if p then x else y) :: Int
> if' pp false true -||- if' qq true false (if p then False else True) || (if q then True else False) :: Bool
> evl $ if' true (val 't') (val 'f') :: Char 't'
caseBool :: Expr -> Expr -> Expr -> Expr #
A function case :: Bool -> a -> a -> a
lifted over the Expr
type
that encodes case-of-False-True functionality.
This is properly displayed as a case-of-False-True expression.
> caseBool pp zero xx (case p of False -> 0; True -> x) :: Int
> zz -*- caseBool pp xx yy z * (case p of False -> x; True -> y) :: Int
> caseBool pp false true -||- caseBool qq true false (caseBool p of False -> False; True -> True) || (caseBool q of False -> True; True -> False) :: Bool
> evl $ caseBool true (val 'f') (val 't') :: Char 't'
By convention, the False
case comes before True
as False < True
and data Bool = False | True
.
When evaluating, this is equivalent to if with arguments reversed.
Instead of using this, you are perhaps better of using if encoded as an
expression. This is just here to be consistent with caseOrdering
.
caseOrdering :: Expr -> Expr -> Expr -> Expr -> Expr #
A function case :: Ordering -> a -> a -> a -> a
lifted over the Expr
type
that encodes case-of-LT-EQ-GT functionality.
This is properly displayed as a case-of-LT-EQ-GT expression.
(cf. caseBool
)
> caseOrdering (xx `compare'` yy) zero one two (case compare x y of LT -> 0; EQ -> 1; GT -> 2) :: Int
> evl $ caseOrdering (val EQ) (val 'l') (val 'e') (val 'g') :: Char 'e'
By convention cases are given in LT
, EQ
and GT
order
as LT < EQ < GT
and data Ordering = LT | EQ | GT
.
Nothing
bound to the Maybe
Int
type encoded as an Expr
.
This is an alias to nothingInt
.
enumFromTo' :: Expr -> Expr -> Expr #
enumFromTo
lifted over Expr
s
> enumFromTo' zero four enumFromTo 0 4 :: [Int]
(-..-) :: Expr -> Expr -> Expr #
enumFromTo
lifted over Expr
s but named as ".."
for pretty-printing.
> zero -..- four [0..4] :: [Int]
enumFromThen' :: Expr -> Expr -> Expr #
enumFromThen
lifted over Expr
s
> enumFromThen' zero ten enumFromThen 0 10 :: [Int]
(--..) :: (Expr, Expr) -> () -> Expr #
enumFromThen
lifted over Expr
s but named as ",.."
for pretty printing.
> (zero,ten) --.. () [0,10..] :: [Int]
enumFromThenTo' :: Expr -> Expr -> Expr -> Expr #
enumFromThenTo
lifted over Expr
s.
> enumFromThenTo' zero two ten enumFromThenTo 0 2 10 :: [Int]
(--..-) :: (Expr, Expr) -> Expr -> Expr #
enumFromThenTo
lifted over Expr
s but named as ",.."
for pretty-printing.
> (zero,two) --..- ten [0,2..10] :: [Int]
groundBinds :: (Expr -> [[Expr]]) -> Expr -> [Binds] #
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)] ]
theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy #
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 }
doubleCheck :: (Expr -> Expr -> Bool) -> Thy -> Thy #
Double-checks a resulting theory moving untrue rules and equations to the invalid list.
As a side-effect of using testing to conjecturing equations, we may get smaller equations that are obviously incorrect when we consider a bigger (harder-to-test) equation that is incorrect.
For example, given an incorrect large equation, it may follow that False=True.
This function can be used to double-check the generated theory. If any equation or rule is discarded, that means the number of tests should probably be increased.