Agda.TypeChecking.Coverage.Match

Documentation

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

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

buildPattern :: Term -> Maybe DeBruijnPattern

Convert the root of a term into a pattern constructor, if possible.

isTrivialPattern :: Pattern' a -> Bool

A pattern that matches anything (modulo eta).

type MatchResult = Match ([DeBruijnPattern], [Literal])

If matching succeeds, we return the instantiation of the clause pattern vector to obtain the split clause pattern vector, plus the literals of the clause patterns matched against split clause variables.

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 Any BlockingVars

Could match if non-empty list of blocking variables is instantiated properly. Also Any is True if all clauses have a result split. (Only then can we do result splitting.)

Instances

Functor Match

Methods

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

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

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

Methods

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

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

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

Monoid a => Monoid (Match a)

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 :: Maybe [ConHead]

  Nothing means there is an overlapping match for this variable. This happens if one clause has a constructor pattern at this position, and another a variable. It is also used for "just variable".

  Just cons means that it is an non-overlapping match and cons are the encountered constructors.

Instances

Show BlockingVar

Methods

showsPrec :: Int -> BlockingVar -> ShowS

show :: BlockingVar -> String

showList :: [BlockingVar] -> ShowS

type BlockingVars = [BlockingVar]

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

Lens for blockingVarCons.

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

type MatchLit = Literal -> DeBruijnPattern -> MatchResult

Could the literal cover (an instantiation of) the split clause pattern? Basically, the split clause pattern needs to be a variable.

Note: literal patterns do not occur in the split clause since we cannot split into all possible literals (that would be infeasible).

noMatchLit :: MatchLit

Use this function if literal patterns should not cover a split clause pattern.

yesMatchLit :: MatchLit

Use this function if a literal pattern should cover a split clause variable pattern.

matchLits :: Clause -> [NamedArg DeBruijnPattern] -> Maybe [Literal]

Check if a clause could match given generously chosen literals

matchClause

Arguments

:: MatchLit

Consider literals?

-> [NamedArg DeBruijnPattern]

Split clause patterns qs.

-> Nat

Clause number i.

-> Clause

Clause c to cover split clause.

-> MatchResult

Result. If Yes the instantiation rs such that (namedClausePats c)[rs] == qs.

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

matchPats

Arguments

:: MatchLit

Matcher for literals.

-> [NamedArg (Pattern' a)]

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

-> [NamedArg DeBruijnPattern]

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

:: MatchLit

Matcher for literals.

-> Pattern' a

Clause pattern p (to cover split clause pattern).

-> DeBruijnPattern

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