PAKCS
Exported names: Imported modules:

Module Rewriting.Substitution

Library for representation of substitutions on first-order terms.

Author: Jan-Hendrik Matthes

Version: February 2020

Summary of exported operations:

showSubst :: (a -> String) -> FM Int (Term a) -> String   
Transforms a substitution into a string representation.
emptySubst :: FM Int (Term a)   
The empty substitution.
extendSubst :: FM Int (Term a) -> Int -> Term a -> FM Int (Term a)   
Extends a substitution with a new mapping from the given variable to the given term.
listToSubst :: [(Int,Term a)] -> FM Int (Term a)   
Returns a substitution that contains all the mappings from the given list.
lookupSubst :: FM Int (Term a) -> Int -> Maybe (Term a)   
Returns the term mapped to the given variable in a substitution or Nothing if no such mapping exists.
applySubst :: FM Int (Term a) -> Term a -> Term a   
Applies a substitution to the given term.
applySubstEq :: FM Int (Term a) -> (Term a,Term a) -> (Term a,Term a)   
Applies a substitution to both sides of the given term equation.
applySubstEqs :: FM Int (Term a) -> [(Term a,Term a)] -> [(Term a,Term a)]   
Applies a substitution to every term equation in the given list.
restrictSubst :: FM Int (Term a) -> [Int] -> FM Int (Term a)   
Returns a new substitution with only those mappings from the given substitution whose variable is in the given list of variables.
composeSubst :: FM Int (Term a) -> FM Int (Term a) -> FM Int (Term a)   
Composes the first substitution phi with the second substitution sigma.

Exported datatypes:

Subst

A substitution represented as a finite map from variables to terms and parameterized over the kind of function symbols, e.g., strings.

Type synonym: Subst a = FM VarIdx (Term a)

Exported operations:

showSubst :: (a -> String) -> FM Int (Term a) -> String   

Transforms a substitution into a string representation.

emptySubst :: FM Int (Term a)   

The empty substitution.

extendSubst :: FM Int (Term a) -> Int -> Term a -> FM Int (Term a)   

Extends a substitution with a new mapping from the given variable to the given term. An already existing mapping with the same variable will be thrown away.

listToSubst :: [(Int,Term a)] -> FM Int (Term a)   

Returns a substitution that contains all the mappings from the given list. For multiple mappings with the same variable, the last corresponding mapping of the given list is taken.

lookupSubst :: FM Int (Term a) -> Int -> Maybe (Term a)   

Returns the term mapped to the given variable in a substitution or Nothing if no such mapping exists.

applySubst :: FM Int (Term a) -> Term a -> Term a   

Applies a substitution to the given term.

applySubstEq :: FM Int (Term a) -> (Term a,Term a) -> (Term a,Term a)   

Applies a substitution to both sides of the given term equation.

applySubstEqs :: FM Int (Term a) -> [(Term a,Term a)] -> [(Term a,Term a)]   

Applies a substitution to every term equation in the given list.

restrictSubst :: FM Int (Term a) -> [Int] -> FM Int (Term a)   

Returns a new substitution with only those mappings from the given substitution whose variable is in the given list of variables.

composeSubst :: FM Int (Term a) -> FM Int (Term a) -> FM Int (Term a)   

Composes the first substitution phi with the second substitution sigma. The resulting substitution sub fulfills the property sub(t) = phi(sigma(t)) for a term t. Mappings in the first substitution shadow those in the second.