Safe Haskell | None |
---|---|

Language | Haskell2010 |

Checking confluence of rewrite rules.

Given a rewrite rule `f ps ↦ v`

, we construct critical pairs
involving this as the main rule by searching for:

- *Different* rules
`f ps' ↦ v'`

where`ps`

and`ps'`

can be unified@. - Subpatterns
`g qs`

of`ps`

and rewrite rules`g qs' ↦ w`

where`qs`

and`qs'`

can be unified.

Each of these leads to a *critical pair* `v₁ u -- v₂`

, which
should satisfy `v₁ = v₂`

.

## Synopsis

- checkConfluenceOfRules :: [RewriteRule] -> TCM ()
- checkConfluenceOfClause :: QName -> Int -> Clause -> TCM ()

# Documentation

checkConfluenceOfRules :: [RewriteRule] -> TCM () Source #

Check confluence of the given clause wrt rewrite rules of the constructors it matches against

Check confluence of the given rewrite rules wrt all other rewrite rules (also amongst themselves).