Data.Rewriting.Rules

Operations on lists of rules.

See also Data.Rewriting.CriticalPair

Important operations

fullRewrite :: (Ord v', Eq v, Eq f) => [Rule f v'] -> Strategy f v v'

Full rewriting: Apply rules anywhere in the term.

Reducts are returned in pre-order: the first is a leftmost, outermost redex.

Reexported modules

type Strategy f v v' = Term f v -> [Reduct f v v']

A rewrite strategy.

data Reduct f v v'

A reduct. It contains the resulting term, the position that the term was rewritten at, and the applied rule.

Constructors

Reduct

Fields

• result :: Term f v
• pos :: Pos
• rule :: Rule f v'
• subst :: GSubst v' f v

fullRewrite :: (Ord v', Eq v, Eq f) => [Rule f v'] -> Strategy f v v'

Full rewriting: Apply rules anywhere in the term.

Reducts are returned in pre-order: the first is a leftmost, outermost redex.

outerRewrite :: (Ord v', Eq v, Eq f) => [Rule f v'] -> Strategy f v v'

Outer rewriting: Apply rules at outermost redexes.

Reducts are returned in left to right order.

innerRewrite :: (Ord v', Eq v, Eq f) => [Rule f v'] -> Strategy f v v'

Inner rewriting: Apply rules at innermost redexes.

Reducts are returned in left to right order.

rootRewrite :: (Ord v', Eq v, Eq f) => [Rule f v'] -> Strategy f v v'

Root rewriting: Apply rules only at the root of the term.

This is mainly useful as a building block for various rewriting strategies.

module Data.Rewriting.Rules.Ops