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 non-empty 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 non-overlapping 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 left-strict, 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
.