Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Coverage.Match

Synopsis

- match :: [Clause] -> [Arg Pattern] -> Permutation -> Match Nat
- data MPat
  - = VarMP Nat
  - | ConMP QName [Arg MPat]
  - | LitMP Literal
  - | WildMP
- buildMPatterns :: Permutation -> [Arg Pattern] -> [Arg MPat]
- data Match a
  - = Yes a
  - | No
  - | Block BlockingVars
- type BlockingVar = (Nat, Maybe [QName])
- type BlockingVars = [BlockingVar]
- overlapping :: BlockingVars -> BlockingVars
- zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars
- choice :: Match a -> Match a -> Match a
- type MatchLit = Literal -> MPat -> Match ()
- noMatchLit :: MatchLit
- yesMatchLit :: MatchLit
- matchLits :: Clause -> [Arg Pattern] -> Permutation -> Bool
- matchClause :: MatchLit -> [Arg MPat] -> Nat -> Clause -> Match Nat
- matchPats :: MatchLit -> [Arg Pattern] -> [Arg MPat] -> Match ()
- matchPat :: MatchLit -> Pattern -> MPat -> Match ()

# Documentation

match :: [Clause] -> [Arg Pattern] -> Permutation -> Match Nat

Given

1. the function clauses `cs` 2. the patterns `ps` and permutation `perm` of a split clause

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 MPat

We use a special representation of the patterns we're trying to match against a clause. In particular we want to keep track of which variables are blocking a match.

Constructors

VarMP Nat |
ConMP QName [Arg MPat] |
LitMP Literal |
WildMP |

buildMPatterns :: Permutation -> [Arg Pattern] -> [Arg MPat]

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 BlockingVars | Could match if non-empty list of blocking variables is instantiated properly.

Instances

Functor Match |

Monoid a => Monoid (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 to make the split clause an instance of the function clause.

type BlockingVar = (Nat, Maybe [QName])

`Nothing` means there is an overlapping match for this variable. `Just cons` means that it is an non-overlapping match and `cons` are the encountered constructors.

type BlockingVars = [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 -> MPat -> Match ()

noMatchLit :: MatchLit

yesMatchLit :: MatchLit

matchLits :: Clause -> [Arg Pattern] -> Permutation -> Bool

Check if a clause could match given generously chosen literals

matchClause :: MatchLit -> [Arg MPat] -> Nat -> Clause -> Match Nat

`matchClause mlist qs i c` checks whther clause `c` number `i` covers a split clause with patterns `qs`.

matchPats :: MatchLit -> [Arg Pattern] -> [Arg MPat] -> Match ()

`matchPats mlist ps qs` checks whether a function clause with patterns `ps` covers a split clause with patterns `qs`

matchPat :: MatchLit -> Pattern -> MPat -> Match ()

`matchPat mlit p q` checks whether a function clause pattern `p` covers a split clause pattern `q`. There are three results: `Yes ()` means it covers, because `p` is a variable pattern or `q` is a wildcard. `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`.