Library for representation of substitutions on first-order terms.
Author: Jan-Hendrik Matthes
Version: August 2016
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 .
|
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)
Transforms a substitution into a string representation. |
The empty substitution. |
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. |
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. |
Returns the term mapped to the given variable in a substitution or
|
Applies a substitution to the given term. |
Applies a substitution to both sides of the given term equation. |
Applies a substitution to every term equation in the given list. |
Returns a new substitution with only those mappings from the given substitution whose variable is in the given list of variables. |