Safe Haskell  None 

 match :: [Clause] > [Arg Pattern] > Permutation > Match Nat
 data MPat
 buildMPatterns :: Permutation > [Arg Pattern] > [Arg MPat]
 data Match a
 = Yes a
  No
  Block BlockingVars
 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 ()
Documentation
match :: [Clause] > [Arg Pattern] > Permutation > Match NatSource
Given
 the function clauses
cs
2. the patternsps
and permutationperm
of 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.
buildMPatterns :: Permutation > [Arg Pattern] > [Arg MPat]Source
If matching is inconclusive (Block
) we want to know which
variables are blocking the match.
Yes a  Matches unconditionally. 
No  Definitely does not match. 
Block BlockingVars  Could match if nonempty list of blocking variables is instantiated properly. 
Functor Match  
Monoid a => Monoid (Match a)  Combine results of checking whether function clause patterns covers split clause patterns.

type BlockingVar = (Nat, Maybe [QName])Source
Nothing
means there is an overlapping match for this variable.
Just cons
means that it is an nonoverlapping match and
cons
are the encountered constructors.
type BlockingVars = [BlockingVar]Source
zipBlockingVars :: BlockingVars > BlockingVars > BlockingVarsSource
Left dominant merge of blocking vars.
choice :: Match a > Match a > Match aSource
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 (No
).
It is leftstrict, to be used with foldr
.
If one clause unconditionally matches (Yes
) we do not look further.
matchLits :: Clause > [Arg Pattern] > Permutation > BoolSource
Check if a clause could match given generously chosen literals
matchClause :: MatchLit > [Arg MPat] > Nat > Clause > Match NatSource
matchClause mlist qs i c
checks whther clause c
number i
covers a split clause with patterns qs
.
matchPats :: MatchLit > [Arg Pattern] > [Arg MPat] > Match ()Source
matchPats mlist ps qs
checks whether a function clause with patterns
ps
covers a split clause with patterns qs
matchPat :: MatchLit > Pattern > MPat > Match ()Source
matchPat mlit p q
checks whether a function clause pattern p
covers a split clause pattern q
. There are three results:
Yes ()
means it covers, because p
is a variable
pattern or 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 x
.