Agda.TypeChecking.Coverage.Match

Given

1. the function clauses cs
2. 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).

Documentation

data 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

Fields

• 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.

Instances

Functor Match

Defined in Agda.TypeChecking.Coverage.Match

Methods

fmap :: (a -> b) -> Match a -> Match b

(<$) :: a -> Match b -> Match a

match

Arguments

:: 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.

matchClause

Arguments

:: 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.

matchClause qs i c checks whether clause c covers a split clause with patterns qs.

type SplitPattern = Pattern' SplitPatVar

data 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

Fields

• splitPatVarName :: PatVarName
• splitPatVarIndex :: Int
• splitExcludedLits :: [Literal]

Instances

PrettyTCM SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

prettyTCM :: MonadPretty m => SplitPatVar -> m Doc

Subst SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

Associated Types

type SubstArg SplitPattern

Methods

applySubst :: Substitution' (SubstArg SplitPattern) -> SplitPattern -> SplitPattern

DeBruijn SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

deBruijnVar :: Int -> SplitPatVar

debruijnNamedVar :: String -> Int -> SplitPatVar

deBruijnView :: SplitPatVar -> Maybe Int

Pretty SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: SplitPatVar -> Doc

prettyPrec :: Int -> SplitPatVar -> Doc

prettyList :: [SplitPatVar] -> Doc

Show SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

showsPrec :: Int -> SplitPatVar -> ShowS

show :: SplitPatVar -> String

showList :: [SplitPatVar] -> ShowS

type SubstArg SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

type SubstArg SplitPattern = SplitPattern

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

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

toSplitPSubst :: PatternSubstitution -> SplitPSubstitution

applySplitPSubst :: TermSubst a => SplitPSubstitution -> a -> a

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

A pattern that matches anything (modulo eta).

data BlockingVar

Variable blocking a match.

Constructors

BlockingVar

Fields

• 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.

Instances

Pretty BlockingVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: BlockingVar -> Doc

prettyPrec :: Int -> BlockingVar -> Doc

prettyList :: [BlockingVar] -> Doc

Show BlockingVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

showsPrec :: Int -> BlockingVar -> ShowS

show :: BlockingVar -> String

showList :: [BlockingVar] -> ShowS

type BlockingVars = [BlockingVar]

data BlockedOnResult

Missing elimination blocking a match.

Constructors

BlockedOnProj

Blocked on unsplit projection.

Fields

• blockedOnResultOverlap :: Bool

  True if there are also matching clauses without an unsplit copattern.

BlockedOnApply

Blocked on unintroduced argument.

Fields

• blockedOnResultIApply :: ApplyOrIApply

  Is the unintroduced argument an IApply pattern?

NotBlockedOnResult

setBlockingVarOverlap :: BlockingVar -> BlockingVar

data ApplyOrIApply

Constructors

IsApply

IsIApply