Data.Rewriting.Substitution.Ops

Documentation

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

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

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

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

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')

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