Data.Rewriting.FirstOrder

First-order rewriting

Documentation

matchM :: (Functor f, Foldable f, EqF f) => LHS f a -> Term f -> WriterT (Subst f) Maybe ()

First-order matching. Results in a list of candidate mappings.

This function assumes that there are no applications of meta-variables in LHS.

solveTerm :: EqF f => [Term f] -> Maybe (Term f)

Check if all terms are equal, and if so, return one of them

solveSubst :: EqF f => [(Name, Term f)] -> Maybe (Subst f)

Turn a list of candidate mappings into a substitution. Succeeds iff. all mappings for the same variable are equal.

match :: (Functor f, Foldable f, EqF f) => LHS f a -> Term f -> Maybe (Subst f)

First-order matching. Succeeds if the pattern matches and all occurrences of a given meta-variable are matched against equal terms.

This function assumes that there are no applications of meta-variables in LHS.

substitute :: Traversable f => Subst f -> RHS f a -> Maybe (Term f)

Naive substitution. Succeeds iff. each meta-variable in RHS has a mapping in the substitution.

This function assumes that there are no applications of meta-variables in RHS.

rewrite :: (Traversable f, EqF f) => Rule (LHS f) (RHS f) -> Term f -> Maybe (Term f)

Apply a rule. Succeeds iff. both matching and substitution succeeds.

This function assumes that there are no applications of meta-variables in LHS or RHS.

applyFirst :: (Traversable f, EqF f) => [Rule (LHS f) (RHS f)] -> Term f -> Term f

Apply the first succeeding rule from a list of rules. If no rule succeeds the term is returned unchanged.

This function assumes that there are no applications of meta-variables in LHS or RHS.

bottomUp :: (Traversable f, EqF f) => [Rule (LHS f) (RHS f)] -> Term f -> Term f

Apply a list of rules bottom-up across a term

This function assumes that there are no applications of meta-variables in LHS or RHS.

topDown :: (Traversable f, EqF f) => [Rule (LHS f) (RHS f)] -> Term f -> Term f

Apply a list of rules top-down across a term

This function assumes that there are no applications of meta-variables in LHS or RHS.