term-rewriting-0.3: Term Rewriting Library

Safe HaskellNone
LanguageHaskell98

Data.Rewriting.Rules.Rewrite

Contents

Description

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.

Synopsis

Documentation

data Reduct f v v' Source #

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

Constructors

Reduct 

Fields

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

A rewrite strategy.

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

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' Source #

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' Source #

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' Source #

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' Source #

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)] Source #

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.