PAKCS
Exported names: Imported modules:

Module Rewriting.Term

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: February 2020

Summary of exported operations:

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.

Exported datatypes:

VarIdx

A variable represented as an integer greater than or equal to zero.

Type synonym: VarIdx = Int

Term

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

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)

TermEqs

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]

Exported operations:

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.

Further infos:
  • solution complete, i.e., able to compute all solutions

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.

Further infos:
  • solution complete, i.e., able to compute all solutions

tRoot :: Term a -> Either Int a   

Returns the root symbol (variable or constructor) of a term.

Further infos:
  • solution complete, i.e., able to compute all solutions

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. The resulting list may contain duplicates.

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. The resulting list may contain duplicates.

isConsTerm :: Term a -> Bool   

Checks whether a term is a constructor term.

Further infos:
  • solution complete, i.e., able to compute all solutions

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. Returns True if both terms have the same constructor and the same arity.