term-rewriting-0.3: Term Rewriting Library

Safe HaskellSafe
LanguageHaskell98

Data.Rewriting.Substitution.Ops

Synopsis

Documentation

apply :: Ord v => Subst f v -> Term f v -> Term f v Source #

Apply a substitution, assuming that it's the identity on variables not mentionend in the substitution.

applyRule :: Ord v => Subst f v -> Rule f v -> Rule f v Source #

Liftting of apply to rules: applies the given substitution to left- and right-hand side.

applyCtxt :: Ord v => Subst f v -> Ctxt f v -> Ctxt f v Source #

Liftting of apply to contexts.

gApply :: Ord v => GSubst v f v' -> Term f v -> Maybe (Term f v') Source #

Apply a substitution, assuming that it's total. If the term contains a variable not defined by the substitution, return Nothing.

compose :: Ord v => Subst f v -> Subst f v -> Subst f v Source #

Compose substitutions. We have

(s1 `compose` s2) `apply` t = s1 `apply` (s2 `apply` t).

merge :: (Ord v, Eq f, Eq v') => GSubst v f v' -> GSubst v f v' -> Maybe (GSubst v f v') Source #

Merge two substitutions. The operation fails if some variable is different terms by the substitutions.