Safe Haskell | None |
---|---|
Language | Haskell2010 |
- match :: [Clause] -> [NamedArg DeBruijnPattern] -> Match (Nat, ([DeBruijnPattern], [Literal]))
- buildPattern :: Term -> Maybe DeBruijnPattern
- isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool
- type MatchResult = Match ([DeBruijnPattern], [Literal])
- data Match a
- = Yes a
- | No
- | Block Any BlockingVars
- 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 -> DeBruijnPattern -> MatchResult
- noMatchLit :: MatchLit
- yesMatchLit :: MatchLit
- matchLits :: Clause -> [NamedArg DeBruijnPattern] -> Maybe [Literal]
- matchClause :: MatchLit -> [NamedArg DeBruijnPattern] -> Nat -> Clause -> MatchResult
- matchPats :: MatchLit -> [NamedArg (Pattern' a)] -> [NamedArg DeBruijnPattern] -> MatchResult
- matchPat :: MatchLit -> Pattern' a -> DeBruijnPattern -> MatchResult
Documentation
match :: [Clause] -> [NamedArg DeBruijnPattern] -> Match (Nat, ([DeBruijnPattern], [Literal])) Source #
Given
- the function clauses
cs
- the patterns
ps
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
buildPattern :: Term -> Maybe DeBruijnPattern Source #
Convert the root of a term into a pattern constructor, if possible.
isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool Source #
A pattern that matches anything (modulo eta).
type MatchResult = Match ([DeBruijnPattern], [Literal]) Source #
If matching succeeds, we return the instantiation of the clause pattern vector to obtain the split clause pattern vector, plus the literals of the clause patterns matched against split clause variables.
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 Any BlockingVars | Could match if non-empty list of blocking variables
is instantiated properly.
Also |
Functor Match Source # | |
Semigroup a => Semigroup (Match a) Source # | Combine results of checking whether function clause patterns covers split clause patterns.
|
(Semigroup a, Monoid a) => Monoid (Match a) Source # | |
data BlockingVar Source #
Variable blocking a match.
BlockingVar | |
|
type BlockingVars = [BlockingVar] Source #
mapBlockingVarCons :: (Maybe [ConHead] -> Maybe [ConHead]) -> BlockingVar -> BlockingVar Source #
Lens for blockingVarCons
.
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.
type MatchLit = Literal -> DeBruijnPattern -> MatchResult Source #
Could the literal cover (an instantiation of) the split clause pattern? Basically, the split clause pattern needs to be a variable.
Note: literal patterns do not occur in the split clause since we cannot split into all possible literals (that would be infeasible).
noMatchLit :: MatchLit Source #
Use this function if literal patterns should not cover a split clause pattern.
yesMatchLit :: MatchLit Source #
Use this function if a literal pattern should cover a split clause variable pattern.
matchLits :: Clause -> [NamedArg DeBruijnPattern] -> Maybe [Literal] Source #
Check if a clause could match given generously chosen literals
:: MatchLit | Consider literals? |
-> [NamedArg DeBruijnPattern] | Split clause patterns |
-> Nat | Clause number |
-> Clause | Clause |
-> MatchResult | Result.
If |
matchClause mlit qs i c
checks whether clause c
number i
covers a split clause with patterns qs
.
:: MatchLit | Matcher for literals. |
-> [NamedArg (Pattern' a)] | Clause pattern vector |
-> [NamedArg DeBruijnPattern] | Split clause pattern vector |
-> MatchResult | Result.
If |
matchPats mlit ps qs
checks whether a function clause with patterns
ps
covers a split clause with patterns qs
.
Issue 1986: This is accepted:
F : Bool -> Set1
F true = Set
F = x -> Set
For the second clause, the split clause is F false
,
so there are more patterns in the split clause than
in the considered clause. These additional patterns
are simply dropped by zipWith
. This will result
in mconcat []
which is Yes []
.
:: MatchLit | Matcher for literals. |
-> Pattern' a | Clause pattern |
-> DeBruijnPattern | Split clause pattern |
-> MatchResult | Result.
If |
matchPat mlit p q
checks whether a function clause pattern p
covers a split clause pattern q
. There are three results:
Yes rs
means it covers, because p
is a variable pattern. rs
collects
the instantiations of the variables in p
s.t. p[rs] = q
.
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
.