term-rewriting-0.4.0.1: Term Rewriting Library

Data.Rewriting.Rule.Ops

Synopsis

# Operations on Rules

funs :: Rule f v -> [f] Source #

Lifting of funs to Rule: returns the list of function symbols in left- and right-hand sides.

>>> funs $Rule {lhs = Fun 'f' [Var 3, Fun 'g' [Fun 'f' []]], rhs = Fun 'h' [Fun 'f' []]} "fgfhf"  funsDL :: Rule f v -> [f] -> [f] Source # Difference List version of funs. We have funsDL r vs = funs r ++ vs. vars :: Rule f v -> [v] Source # Lifting of vars to Rule: returns the list of variables in left- and right-hand sides. >>> vars$ Rule {lhs = Fun 'g' [Var 3, Fun 'f' [Var 1, Var 2, Var 3]], rhs = Fun 'g' [Var 4, Var 3]}
[3,1,2,3,4,3]


varsDL :: Rule f v -> [v] -> [v] Source #

Difference List version of vars. We have varsDL r vs = vars r ++ vs.

left :: (Term f v -> a) -> Rule f v -> a Source #

Apply a function to the lhs of a rule.

right :: (Term f v -> a) -> Rule f v -> a Source #

Apply a function to the rhs of a rule.

rename :: (v -> v') -> Rule f v -> Rule f v' Source #

Lifting of rename to Rule: renames left- and right-hand sides.

>>> rename (+ 1) \$ Rule {lhs = (Fun 'f' [Var 1, Fun 'g' [Var 2]]), rhs = Fun 'g' [Var 1]}
Rule {lhs = Fun 'f' [Var 2, Fun 'g' [Var 3]], rhs = Fun 'g' [Var 2]}


# Predicates on Rules

both :: (Term f v -> Bool) -> Rule f v -> Bool Source #

Test whether the given predicate is true for both sides of a rule.

isLinear :: Ord v => Rule f v -> Bool Source #

Check whether both sides of the given rule are linear.

isLeftLinear :: Ord v => Rule f v -> Bool Source #

Check whether the left hand side of the given rule is linear.

isRightLinear :: Ord v => Rule f v -> Bool Source #

Check whether the right hand side of the given rule is linear.

isGround :: Rule f v -> Bool Source #

Check whether both sides of the given rule is are ground terms.

isLeftGround :: Rule f v -> Bool Source #

Check whether the left hand side of the given rule is a ground term.

isRightGround :: Rule f v -> Bool Source #

Check whether the right hand side of the given rule is a ground term.

isErasing :: Ord v => Rule f v -> Bool Source #

Check whether the given rule is erasing, i.e., if some variable occurs in the left hand side but not in the right hand side.

isCreating :: Ord v => Rule f v -> Bool Source #

Check whether the given rule is creating, i.e., if some variable occurs in its right hand side that does not occur in its left hand side.

This is the dual of isErasing. The term creating is non-standard. Creating rules are usually forbidden. See also isValid.

isDuplicating :: Ord v => Rule f v -> Bool Source #

Check whether the given rule is duplicating, i.e., if some variable occurs more often in its right hand side than in its left hand side.

isCollapsing :: Rule f v -> Bool Source #

Check whether the given rule is collapsing, i.e., if its right hand side is a variable.

isExpanding :: Rule f v -> Bool Source #

Check whether the given rule is expanding, i.e., if its left hand sides is a variable.

This is the dual of isCollapsing. The term expanding is non-standard. Expanding rules are usually forbidden. See also isValid.

isValid :: Ord v => Rule f v -> Bool Source #

Check whether the given rule is non-creating and non-expanding. See also isCreating and isExpanding

isInstanceOf :: (Eq f, Ord v, Ord v') => Rule f v -> Rule f v' -> Bool Source #

Check whether the first rule is an instance of the second rule.

isVariantOf :: (Eq f, Ord v, Ord v') => Rule f v -> Rule f v' -> Bool Source #

Check whether two rules are variants of each other.