| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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

Instances

Functor Match
Monoid a => Monoid (Match a)

choice :: Match a -> Match a -> Match a | Source

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

noMatchLit :: MatchLit | Source

yesMatchLit :: MatchLit | Source

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

Match the given patterns against a list of clauses

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

Check if a clause could match given generously chosen literals

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

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

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

Produced by Haddock version 2.4.2