Agda.TypeChecking.Coverage.Match

Documentation

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 variable is blocking the match. If a dot pattern is blocking a match we're screwed.

Constructors

Yes a

No

Block (Maybe Nat)

Instances

Functor Match

Monoid a => Monoid (Match a)

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

type MatchLit = Literal -> MPat -> Match ()

noMatchLit :: MatchLit

yesMatchLit :: MatchLit

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

Match the given patterns against a list of clauses

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

Check if a clause could match given generously chosen literals

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

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

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