Data.Rewriting.CriticalPair.Type

Documentation

data CP f v v'

A critical pair. Critical pairs (should) have the following properties:

 top   == Context.ofTerm top pos (Term.map Left id (Rule.lhs leftRule))
 left  == Context.ofTerm top pos (Term.map Left id (Rule.rhs leftRule))
 top   == Substitution.apply subst (Term.map Right id (Rule.lhs rightRule))
 right == Substitution.apply subst (Term.map Right id (Rule.rhs rightRule))

Furthermore, pos is a non-variable position of (lhs rightRule) and subst is a most general substitution with these properties.

Constructors

CP

Fields

left :: Term f (Either v v')

left reduct

top :: Term f (Either v v')

source

right :: Term f (Either v v')

right reduct

leftRule :: Rule f v

rule applied on left side

leftPos :: Pos

position of left rule application

rightRule :: Rule f v'

rule applied on right side

subst :: Subst f (Either v v')

common substitution of the rewrite steps