Library for representation of first-order terms.
This library is the basis of other libraries for the manipulation of first-order terms, e.g., unification of terms. Therefore, this library also defines other structures, like term equations.
Author: Jan-Hendrik Matthes
Version: August 2016
showVarIdx
:: Int -> String
Transforms a variable into a string representation. |
showTerm
:: (a -> String) -> Term a -> String
Transforms a term into a string representation. |
showTermEq
:: (a -> String) -> (Term a,Term a) -> String
Transforms a term equation into a string representation. |
showTermEqs
:: (a -> String) -> [(Term a,Term a)] -> String
Transforms a list of term equations into a string representation. |
tConst
:: a -> Term a
Returns a term with the given constructor and no argument terms. |
tOp
:: Term a -> a -> Term a -> Term a
Returns an infix operator term with the given constructor and the given left and right argument term. |
tRoot
:: Term a -> Either Int a
Returns the root symbol (variable or constructor) of a term. |
tCons
:: Term a -> [a]
Returns a list without duplicates of all constructors in a term. |
tConsAll
:: Term a -> [a]
Returns a list of all constructors in a term. |
tVars
:: Term a -> [Int]
Returns a list without duplicates of all variables in a term. |
tVarsAll
:: Term a -> [Int]
Returns a list of all variables in a term. |
isConsTerm
:: Term a -> Bool
Checks whether a term is a constructor term. |
isVarTerm
:: Term a -> Bool
Checks whether a term is a variable term. |
isGround
:: Term a -> Bool
Checks whether a term is a ground term (contains no variables). |
isLinear
:: Term a -> Bool
Checks whether a term is linear (contains no variable more than once). |
isNormal
:: Term a -> Bool
Checks whether a term is normal (behind a variable is not a constructor). |
maxVarInTerm
:: Term a -> Maybe Int
Returns the maximum variable in a term or Nothing
if no variable exists.
|
minVarInTerm
:: Term a -> Maybe Int
Returns the minimum variable in a term or Nothing
if no variable exists.
|
normalizeTerm
:: Term a -> Term a
Normalizes a term by renaming all variables with an increasing order, starting from the minimum possible variable. |
renameTermVars
:: Int -> Term a -> Term a
Renames the variables in a term by the given number. |
mapTerm
:: (a -> b) -> Term a -> Term b
Transforms a term by applying a transformation on all constructors. |
eqConsPattern
:: Term a -> Term a -> Bool
Checks whether the constructor pattern of the first term is equal to the constructor pattern of the second term. |
A variable represented as an integer greater than or equal to zero.
Type synonym: VarIdx = Int
Representation of a first-order term, parameterized over the kind of function symbols, e.g., strings.
Constructors:
TermVar
:: VarIdx -> Term a
: The variable term with variable v
.
TermCons
:: a -> [Term a] -> Term a
: The constructor term with constructor c
and
argument terms ts
.
A term equation represented as a pair of terms and parameterized over the kind of function symbols, e.g., strings.
Type synonym: TermEq a = (Term a,Term a)
Multiple term equations represented as a list of term equations and parameterized over the kind of function symbols, e.g., strings.
Type synonym: TermEqs a = [TermEq a]
Transforms a variable into a string representation. |
Transforms a term equation into a string representation. |
Transforms a list of term equations into a string representation. |
Returns a term with the given constructor and no argument terms.
|
Returns an infix operator term with the given constructor and the given left and right argument term.
|
Returns the root symbol (variable or constructor) of a term.
|
Returns a list of all constructors in a term. The resulting list may contain duplicates. |
Returns a list of all variables in a term. The resulting list may contain duplicates. |
Checks whether a term is a constructor term.
|
Checks whether a term is normal (behind a variable is not a constructor). |
Returns the maximum variable in a term or |
Returns the minimum variable in a term or |
Normalizes a term by renaming all variables with an increasing order, starting from the minimum possible variable. |
Renames the variables in a term by the given number. |
Transforms a term by applying a transformation on all constructors. |
Checks whether the constructor pattern of the first term is equal to the
constructor pattern of the second term. Returns |