Agda.TypeChecking.Coverage.Match

Documentation

match :: [Clause] -> [NamedArg SplitPattern] -> Match (Nat, [SplitPattern])

Given

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

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

Show SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

showsPrec :: Int -> SplitPatVar -> ShowS

show :: SplitPatVar -> String

showList :: [SplitPatVar] -> ShowS

Pretty SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: SplitPatVar -> Doc

prettyPrec :: Int -> SplitPatVar -> Doc

prettyList :: [SplitPatVar] -> Doc

DeBruijn SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

Methods

deBruijnVar :: Int -> SplitPattern

debruijnNamedVar :: String -> Int -> SplitPattern

deBruijnView :: SplitPattern -> Maybe Int

PrettyTCM SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

prettyTCM :: SplitPatVar -> TCM Doc

Subst SplitPattern SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

Methods

applySubst :: Substitution' SplitPattern -> SplitPattern -> SplitPattern

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

A pattern that matches anything (modulo eta).

type MatchResult = Match [SplitPattern]

If matching succeeds, we return the instantiation of the clause pattern vector to obtain the split clause pattern vector.

data Match a

If matching is inconclusive (Block) we want to know which variables are blocking the match.

Constructors

Yes a

Matches unconditionally.

No

Definitely does not match.

Block

Fields

• blockedOnResult :: Bool

  True 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

Semigroup a => Semigroup (Match a)

Combine results of checking whether function clause patterns covers split clause patterns.

No is dominant: if one function clause pattern is disjoint to the corresponding split clause pattern, then the whole clauses are disjoint.

Yes is neutral: for a match, all patterns have to match.

Block accumulates variables of the split clause that have to be instantiated (an projection names of copattern matches) to make the split clause an instance of the function clause.

Defined in Agda.TypeChecking.Coverage.Match

Methods

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

sconcat :: NonEmpty (Match a) -> Match a

stimes :: Integral b => b -> Match a -> Match a

(Semigroup a, Monoid a) => Monoid (Match a)

Defined in Agda.TypeChecking.Coverage.Match

Methods

mempty :: Match a

mappend :: Match a -> Match a -> Match a

mconcat :: [Match a] -> Match a

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.

Instances

Show BlockingVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

showsPrec :: Int -> BlockingVar -> ShowS

show :: BlockingVar -> String

showList :: [BlockingVar] -> ShowS

Pretty BlockingVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: BlockingVar -> Doc

prettyPrec :: Int -> BlockingVar -> Doc

prettyList :: [BlockingVar] -> Doc

type BlockingVars = [BlockingVar]

blockedOnConstructor :: Nat -> ConHead -> Match a

blockedOnLiteral :: Nat -> Literal -> Match a

blockedOnProjection :: Match a

mapBlockingVarCons :: ([ConHead] -> [ConHead]) -> BlockingVar -> BlockingVar

Lens for blockingVarCons.

mapBlockingVarLits :: ([Literal] -> [Literal]) -> BlockingVar -> BlockingVar

Lens for blockingVarLits.

setBlockingVarOverlap :: BlockingVar -> BlockingVar

overlapping :: BlockingVars -> BlockingVars

zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars

Left dominant merge of blocking vars.

choice :: Match a -> Match a -> Match a

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.

matchClause

Arguments

:: [NamedArg SplitPattern]

Split clause patterns qs.

-> Clause

Clause c to cover split clause.

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

matchPats

Arguments

:: [NamedArg (Pattern' a)]

Clause pattern vector ps (to cover split clause pattern vector).

-> [NamedArg SplitPattern]

Split clause pattern vector qs (to be covered by clause pattern vector).

-> MatchResult

Result. If Yes the instantiation rs such that ps[rs] == qs.

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 [].

matchPat

Arguments

:: Pattern' a

Clause pattern p (to cover split clause pattern).

-> SplitPattern

Split clause pattern q (to be covered by clause pattern).

-> MatchResult

Result. If Yes, also the instantiation rs of the clause pattern variables to produce the split clause pattern, p[rs] = q.

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.