Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Coverage.Match
Synopsis
data MPat
= VarMP Nat
| ConMP QName [Arg MPat]
| LitMP Literal
| WildMP
buildMPatterns :: Permutation -> [Arg Pattern] -> [Arg MPat]
data Match a
= Yes a
| No
| Block (Maybe Nat)
choice :: Match a -> Match a -> Match a
type MatchLit = Literal -> MPat -> Match ()
noMatchLit :: MatchLit
yesMatchLit :: MatchLit
match :: [Clause] -> [Arg Pattern] -> Permutation -> Match Nat
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
data MPat Source
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]Source
data Match a Source
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)
show/hide Instances
choice :: Match a -> Match a -> Match aSource
type MatchLit = Literal -> MPat -> Match ()Source
noMatchLit :: MatchLitSource
yesMatchLit :: MatchLitSource
match :: [Clause] -> [Arg Pattern] -> Permutation -> Match NatSource
Match the given patterns against a list of clauses
matchLits :: Clause -> [Arg Pattern] -> Permutation -> BoolSource
Check if a clause could match given generously chosen literals
matchClause :: MatchLit -> [Arg MPat] -> Nat -> Clause -> Match NatSource
matchPats :: MatchLit -> [Arg Pattern] -> [Arg MPat] -> Match ()Source
matchPat :: MatchLit -> Pattern -> MPat -> Match ()Source
Produced by Haddock version 2.4.2