Term.Rewriting.Definitions

Term Equalities, Matching Problems, and Subterm Rules.

Equalities

data Equal a

An equality.

Constructors

Equal

Fields

eqLHS :: a

eqRHS :: a

Instances

Functor Equal

Applicative Equal

Foldable Equal

Traversable Equal

Eq a => Eq (Equal a)

Show a => Show (Equal a)

Monoid a => Monoid (Equal a)

HasFrees a => HasFrees (Equal a)

Apply t => Apply (Equal t)

evalEqual :: Eq a => Equal a -> Bool

True iff the two sides of the equality are equal with respect to their Eq instance.

Matching Problems

data Match a

Matching problems. Use the Monoid instance to compose matching problems.

Constructors

NoMatch

No matcher exists.

DelayedMatches [(a, a)]

A bunch of delayed (term,pattern) pairs.

Instances

Functor Match

Foldable Match

Traversable Match

Eq a => Eq (Match a)

Show a => Show (Match a)

Monoid (Match a)

HasFrees a => HasFrees (Match a)

flattenMatch :: Match a -> Maybe [(a, a)]

Flatten a matching problem to a list of (term,pattern) pairs. If no matcher exists, then Nothing is returned.

matchWith

Arguments

:: a

Term

-> a

Pattern

-> Match a

Matching problem.

Match a term with a pattern.

matchOnlyIf :: Bool -> Match a

Ensure that matching only succeeds if the condition holds.

Rewriting Rules

data RRule a

A rewrite rule.

Constructors

RRule a a

Instances

Functor RRule

Applicative RRule

Foldable RRule

Traversable RRule

Eq a => Eq (RRule a)

Ord a => Ord (RRule a)

Show a => Show (RRule a)

Monoid a => Monoid (RRule a)

HasFrees a => HasFrees (RRule a)