- match :: [Clause] -> [Arg Pattern] -> Permutation -> Match Nat
- data MPat
- buildMPatterns :: Permutation -> [Arg Pattern] -> [Arg MPat]
- data Match a
- type BlockingVar = (Nat, Maybe [QName])
- type BlockingVars = [BlockingVar]
- overlapping :: BlockingVars -> BlockingVars
- zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars
- choice :: Match a -> Match a -> Match a
- type MatchLit = Literal -> MPat -> Match ()
- noMatchLit :: MatchLit
- yesMatchLit :: MatchLit
- matchLits :: Clause -> [Arg Pattern] -> Permutation -> Bool
- matchClause :: MatchLit -> [Arg MPat] -> Nat -> Clause -> Match Nat
- matchPats :: MatchLit -> [Arg Pattern] -> [Arg MPat] -> Match ()
- matchPat :: MatchLit -> Pattern -> MPat -> Match ()
- the function clauses
cs2. the patterns
permof a split clause
we want to compute a variable index of the split clause to split on next.
First, we find the set
cs' of all the clauses that are
instances (via substitutions
rhos) of the split clause.
In these substitutions, we look for a column that has only constructor patterns. We try to split on this column first.
Match the given patterns against a list of clauses
We use a special representation of the patterns we're trying to match against a clause. In particular we want to keep track of which variables are blocking a match.
If matching is inconclusive (
Block) we want to know which
variables are blocking the match.
Definitely does not match.
Could match if non-empty list of blocking variables is instantiated properly.
|Monoid a => Monoid (Match a)|
Combine results of checking whether function clause patterns covers split clause patterns.
Nothing means there is an overlapping match for this variable.
Just cons means that it is an non-overlapping match and
cons are the encountered constructors.
Left dominant merge of blocking vars.
choice m m' combines the match results
m of a function clause
with the (already combined) match results $m'$ of the later clauses.
It is for skipping clauses that definitely do not match (
It is left-strict, to be used with
If one clause unconditionally matches (
Yes) we do not look further.
Check if a clause could match given generously chosen literals
matchClause mlist qs i c checks whther clause
covers a split clause with patterns
matchPats mlist ps qs checks whether a function clause with patterns
ps covers a split clause with patterns
matchPat mlit p q checks whether a function clause pattern
covers a split clause pattern
q. There are three results:
Yes () means it covers, because
p is a variable
q is a wildcard.
No means it does not cover.
Block [x] means
p is a proper instance of
q and could become
a cover if
q was split on variable