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)

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.6.0