Library for representation of firstorder terms.
This library is the basis of other libraries for the manipulation of firstorder terms, e.g., unification of terms. Therefore, this library also defines other structures, like term equations.
Author: JanHendrik 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
:: Eq a => 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
:: Eq a => 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 firstorder 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 