Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- match :: [Clause] -> [NamedArg SplitPattern] -> Match (Nat, [SplitPattern])
- data SplitPatVar = SplitPatVar {}
- type SplitPattern = Pattern' SplitPatVar
- toSplitVar :: DBPatVar -> SplitPatVar
- fromSplitVar :: SplitPatVar -> DBPatVar
- toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
- fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
- type SplitPSubstitution = Substitution' SplitPattern
- toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
- fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
- applySplitPSubst :: Subst Term a => SplitPSubstitution -> a -> a
- isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool
- type MatchResult = Match [SplitPattern]
- data Match a
- data BlockingVar = BlockingVar {}
- type BlockingVars = [BlockingVar]
- blockedOnConstructor :: Nat -> ConHead -> Match a
- blockedOnLiteral :: Nat -> Literal -> Match a
- blockedOnProjection :: Match a
- mapBlockingVarCons :: ([ConHead] -> [ConHead]) -> BlockingVar -> BlockingVar
- mapBlockingVarLits :: ([Literal] -> [Literal]) -> BlockingVar -> BlockingVar
- setBlockingVarOverlap :: BlockingVar -> BlockingVar
- overlapping :: BlockingVars -> BlockingVars
- zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars
- choice :: Match a -> Match a -> Match a
- matchClause :: [NamedArg SplitPattern] -> Clause -> MatchResult
- matchPats :: [NamedArg (Pattern' a)] -> [NamedArg SplitPattern] -> MatchResult
- matchPat :: Pattern' a -> SplitPattern -> MatchResult
Documentation
match :: [Clause] -> [NamedArg SplitPattern] -> Match (Nat, [SplitPattern]) 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
data SplitPatVar Source #
For each variable in the patterns of a split clause, we remember the de Bruijn-index and the literals excluded by previous matches.
Instances
Show SplitPatVar Source # | |
Defined in Agda.TypeChecking.Coverage.Match showsPrec :: Int -> SplitPatVar -> ShowS # show :: SplitPatVar -> String # showList :: [SplitPatVar] -> ShowS # | |
Pretty SplitPatVar Source # | |
Defined in Agda.TypeChecking.Coverage.Match pretty :: SplitPatVar -> Doc Source # prettyPrec :: Int -> SplitPatVar -> Doc Source # prettyList :: [SplitPatVar] -> Doc Source # | |
DeBruijn SplitPattern Source # | |
Defined in Agda.TypeChecking.Coverage.Match deBruijnVar :: Int -> SplitPattern Source # debruijnNamedVar :: String -> Int -> SplitPattern Source # deBruijnView :: SplitPattern -> Maybe Int Source # | |
PrettyTCM SplitPatVar Source # | |
Defined in Agda.TypeChecking.Coverage.Match | |
Subst SplitPattern SplitPattern Source # | |
Defined in Agda.TypeChecking.Coverage.Match |
type SplitPattern = Pattern' SplitPatVar Source #
toSplitVar :: DBPatVar -> SplitPatVar Source #
fromSplitVar :: SplitPatVar -> DBPatVar Source #
applySplitPSubst :: Subst Term a => SplitPSubstitution -> a -> a Source #
isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool Source #
A pattern that matches anything (modulo eta).
type MatchResult = Match [SplitPattern] Source #
If matching succeeds, we return the instantiation of the clause pattern vector to obtain the split clause pattern vector.
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 | |
|
Instances
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 | |
|
Instances
Show BlockingVar Source # | |
Defined in Agda.TypeChecking.Coverage.Match showsPrec :: Int -> BlockingVar -> ShowS # show :: BlockingVar -> String # showList :: [BlockingVar] -> ShowS # | |
Pretty BlockingVar Source # | |
Defined in Agda.TypeChecking.Coverage.Match pretty :: BlockingVar -> Doc Source # prettyPrec :: Int -> BlockingVar -> Doc Source # prettyList :: [BlockingVar] -> Doc Source # |
type BlockingVars = [BlockingVar] Source #
blockedOnProjection :: Match a Source #
mapBlockingVarCons :: ([ConHead] -> [ConHead]) -> BlockingVar -> BlockingVar Source #
Lens for blockingVarCons
.
mapBlockingVarLits :: ([Literal] -> [Literal]) -> BlockingVar -> BlockingVar Source #
Lens for blockingVarLits
.
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.
:: [NamedArg SplitPattern] | Split clause patterns |
-> Clause | Clause |
-> MatchResult | Result.
If |
matchClause qs i c
checks whether clause c
covers a split clause with patterns qs
.
:: [NamedArg (Pattern' a)] | Clause pattern vector |
-> [NamedArg SplitPattern] | Split clause pattern vector |
-> MatchResult | Result.
If |
matchPats 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 []
.
:: Pattern' a | Clause pattern |
-> SplitPattern | Split clause pattern |
-> MatchResult | Result.
If |
matchPat 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
.
BlockLit [x] means
p is a proper instance of
q and could become
a cover if variable
x@ is instantiated with an appropriate literal.