ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Coverage.Match

Given

the function clauses cs
the patterns ps of the split clause

we want to compute a variable index (in the split clause) to split on next.

The matcher here checks whether the split clause is covered by one of the given clauses cs or whether further splitting is needed (and when yes, where).

7 types
9 values

PackageAgda-2.7.0.1
Exports16
LanguageHaskell2010
LicenceMIT
SourceMatch.hs

datadata Match a

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
- blockedOnResult :: BlockedOnResult
  BlockedOnProj o if the clause has a result split.
- blockedOnVars :: BlockingVars
  BlockingVar i cs ls o means variable i is blocked on constructors cs and literals ls.

Instances1Functor

Functor MatchDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match

valuematch

:: PureTCM m
=> [Clause]
Search for clause that covers the patterns.
-> [NamedArg SplitPattern]
Patterns of the current SplitClause.
-> m (Match (Nat, SplitInstantiation))

Match the given patterns against a list of clauses.

If successful, return the index of the covering clause.

valuematchClause

:: PureTCM m
=> [NamedArg SplitPattern]
Split clause patterns qs.
-> Clause
Clause c to cover split clause.
-> m MatchResult
Result. If Yes the instantiation rs such that (namedClausePats c)[rs] == qs.

typetype SplitPattern = Pattern' SplitPatVar

datadata SplitPatVar

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
- splitPatVarName :: PatVarName
- splitPatVarIndex :: Int
- splitExcludedLits :: [Literal]

Instances6Show, Pretty, DeBruijn, Subst, PrettyTCM, SubstArg

Show SplitPatVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match
Pretty SplitPatVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match
DeBruijn SplitPatVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match
Subst SplitPatternDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match
PrettyTCM SplitPatVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match
type SubstArg SplitPattern = SplitPatternDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match

valuefromSplitPattern :: NamedArg SplitPattern -> NamedArg DeBruijnPattern

valuefromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]

valuetoSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]

valuetoSplitPSubst :: PatternSubstitution -> SplitPSubstitution

valueapplySplitPSubst :: TermSubst a => SplitPSubstitution -> a -> a

valueisTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool

A pattern that matches anything (modulo eta).

datadata BlockingVar

Variable blocking a match.

Constructors

BlockingVar
- blockingVarNo :: Nat
  De Bruijn index of variable blocking the match.
- blockingVarCons :: [ConHead]
  Constructors in this position.
- blockingVarLits :: [Literal]
  Literals in this position.
- blockingVarOverlap :: Bool
  True if at least one clause has a variable pattern in this position.
- blockingVarLazy :: Bool
  True if at least one clause has a lazy pattern in this position.

Instances2Show, Pretty

Show BlockingVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match
Pretty BlockingVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match

typetype BlockingVars = [BlockingVar]

datadata BlockedOnResult

Missing elimination blocking a match.

Constructors

BlockedOnProj
Blocked on unsplit projection.
- blockedOnResultOverlap :: Bool
  True if there are also matching clauses without an unsplit copattern.
BlockedOnApply
Blocked on unintroduced argument.
- blockedOnResultIApply :: ApplyOrIApply
  Is the unintroduced argument an IApply pattern?
NotBlockedOnResult

valuesetBlockingVarOverlap :: BlockingVar -> BlockingVar

datadata ApplyOrIApply

IsApply IsIApply