Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Coverage.Match
Synopsis
- data Match a
- match :: (MonadReduce m, HasConstInfo m, HasBuiltins m) => [Clause] -> [NamedArg SplitPattern] -> m (Match (Nat, [SplitAssignment]))
- type SplitPattern = Pattern' SplitPatVar
- data SplitPatVar = SplitPatVar {
- splitPatVarName :: PatVarName
- splitPatVarIndex :: Int
- splitExcludedLits :: [Literal]
- fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
- toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
- toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
- applySplitPSubst :: Subst Term a => SplitPSubstitution -> a -> a
- isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool
- data BlockingVar = BlockingVar {
- blockingVarNo :: Nat
- blockingVarCons :: [ConHead]
- blockingVarLits :: [Literal]
- blockingVarOverlap :: Bool
- type BlockingVars = [BlockingVar]
- data BlockedOnResult
- = BlockedOnProj {
- blockedOnResultOverlap :: Bool
- | BlockedOnApply { }
- | NotBlockedOnResult
- = BlockedOnProj {
- setBlockingVarOverlap :: BlockingVar -> BlockingVar
- data ApplyOrIApply
Documentation
If matching is inconclusive (Block
) we want to know which
variables or projections are blocking the match.
Constructors
Yes a | Matches unconditionally. |
No | Definitely does not match. |
Block | |
Fields
|
match :: (MonadReduce m, HasConstInfo m, HasBuiltins m) => [Clause] -> [NamedArg SplitPattern] -> m (Match (Nat, [SplitAssignment])) Source #
Match the given patterns against a list of clauses
type SplitPattern = Pattern' SplitPatVar Source #
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.
Constructors
SplitPatVar | |
Fields
|
Instances
toSplitPSubst :: PatternSubstitution -> SplitPSubstitution Source #
applySplitPSubst :: Subst Term a => SplitPSubstitution -> a -> a Source #
isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool Source #
A pattern that matches anything (modulo eta).
data BlockingVar Source #
Variable blocking a match.
Constructors
BlockingVar | |
Fields
|
Instances
Show BlockingVar Source # | |
Defined in Agda.TypeChecking.Coverage.Match Methods showsPrec :: Int -> BlockingVar -> ShowS show :: BlockingVar -> String showList :: [BlockingVar] -> ShowS | |
Pretty BlockingVar Source # | |
Defined in Agda.TypeChecking.Coverage.Match Methods pretty :: BlockingVar -> Doc Source # prettyPrec :: Int -> BlockingVar -> Doc Source # prettyList :: [BlockingVar] -> Doc Source # |
type BlockingVars = [BlockingVar] Source #
data BlockedOnResult Source #
Constructors
BlockedOnProj | Blocked on unsplit projection |
Fields
| |
BlockedOnApply | Blocked on unintroduced argument |
Fields
| |
NotBlockedOnResult |
data ApplyOrIApply Source #