| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Data.Rewriting.Rules.Rewrite
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
- data Reduct f v v' = Reduct {}
- type Strategy f v v' = Term f v -> [Reduct f v v']
- fullRewrite :: (Ord v', Eq v, Eq f) => [Rule f v'] -> Strategy f v v'
- outerRewrite :: (Ord v', Eq v, Eq f) => [Rule f v'] -> Strategy f v v'
- innerRewrite :: (Ord v', Eq v, Eq f) => [Rule f v'] -> Strategy f v v'
- rootRewrite :: (Ord v', Eq v, Eq f) => [Rule f v'] -> Strategy f v v'
- nested :: Strategy f v v' -> Strategy f v v'
- listContexts :: [a] -> [(Int, a -> [a], a)]
Documentation
A reduct. It contains the resulting term, the position that the term was rewritten at, and the applied rule.
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.