Safe Haskell | None |
---|---|
Language | Haskell98 |
- match :: [Clause] -> [Arg Pattern] -> Permutation -> Match Nat
- data MPat
- buildMPatterns :: Permutation -> [Arg Pattern] -> [Arg MPat]
- data Match a
- = Yes a
- | No
- | Block BlockingVars
- | BlockP
- data BlockingVar = BlockingVar {
- blockingVarNo :: Nat
- blockingVarCons :: Maybe [ConHead]
- type BlockingVars = [BlockingVar]
- mapBlockingVarCons :: (Maybe [ConHead] -> Maybe [ConHead]) -> BlockingVar -> BlockingVar
- clearBlockingVarCons :: BlockingVar -> 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 Nat Source
Given
- the function clauses
cs
- the patterns
ps
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. |
BlockP | Could match if split on possible projections is performed. |
Functor Match Source | |
Monoid a => Monoid (Match a) Source | Combine results of checking whether function clause patterns covers split clause patterns.
|
data BlockingVar Source
Variable blocking a match.
BlockingVar | |
|
type BlockingVars = [BlockingVar] Source
mapBlockingVarCons :: (Maybe [ConHead] -> Maybe [ConHead]) -> BlockingVar -> BlockingVar Source
zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars Source
Left dominant merge of blocking vars.
choice :: Match a -> Match a -> Match a Source
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 -> Bool Source
Check if a clause could match given generously chosen literals
matchClause :: MatchLit -> [Arg MPat] -> Nat -> Clause -> Match Nat Source
matchClause mlit qs i c
checks whether clause c
number i
covers a split clause with patterns qs
.
matchPats :: MatchLit -> [Arg Pattern] -> [Arg MPat] -> Match () Source
matchPats mlit ps qs
checks whether a function clause with patterns
ps
covers a split clause with patterns qs
.
Issue 842: if in case of functions with varying arity,
the split clause has proper patterns left, we refuse to match,
because it would be troublesome to construct the split tree later.
We would have to move bindings from the rhs to the lhs.
For example, this is rejected:
F : Bool -> Set1
F true = Set
F = x -> Set
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
.