Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|

Safe Haskell | None |

Subsumption of terms and substitutions.

- compareTermSubs :: LNTerm -> LNTerm -> WithMaude (Maybe Ordering)
- eqTermSubs :: LNTerm -> LNTerm -> WithMaude Bool
- factorSubstVia :: [LVar] -> LNSubst -> LNSubst -> WithMaude [LNSubst]
- canonizeSubst :: LNSubstVFresh -> LNSubstVFresh
- varOccurences :: HasFrees a => a -> [(LVar, Set Occurence)]

# Documentation

compareTermSubs :: LNTerm -> LNTerm -> WithMaude (Maybe Ordering)Source

Compare terms `t1`

and `t2`

with respect to the subsumption order modulo AC.

eqTermSubs :: LNTerm -> LNTerm -> WithMaude BoolSource

Returns True if `s1`

and `s2`

are equal with respect to the subsumption order modulo AC.

# Canonical representations for substitutions

canonizeSubst :: LNSubstVFresh -> LNSubstVFreshSource

Returns a substitution that is equivalent modulo renaming to the given substitution.

# for testing only

varOccurences :: HasFrees a => a -> [(LVar, Set Occurence)]Source

Returns the variables occuring in `t`

together with the contexts they appear in.
Note that certain contexts (and variables only occuring in such contexts) are
ignored by this function.
The function is used to guess renamings of variables, i.e., if t is a renaming of s,
then variables that occur in equal contexts in t and s are probably renamings of
each other.