Data.Rewriting.Rules.Rewrite

Simple rewriting.

Note: The rules are assumed to be non-creating, i.e., variables on the rhs should also occur on the lhs. Rules violating this constraint will have no effect.

Documentation

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

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

A rewrite strategy.

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.

utilities not reexported from Data.Rewriting.Rules

nested :: Strategy f v v' -> Strategy f v v'

Nested rewriting: Apply a rewriting strategy to all arguments of a function symbol, left to right. For variables, the result will be empty.

This is another building block for rewriting strategies.

listContexts :: [a] -> [(Int, a -> [a], a)]

Return a list of contexts of a list. Each returned element is an element index (starting from 0), a function that replaces the list element by a new one, and the original element.