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

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

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