Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




match :: [Clause] -> [Arg DeBruijnPattern] -> Match (Nat, [MPat]) Source #


  1. the function clauses cs
  2. the patterns ps

we want to compute a variable index of the split clause to split on next.

First, we find the set cs' of all the clauses that are instances (via substitutions rhos) of the split clause.

In these substitutions, we look for a column that has only constructor patterns. We try to split on this column first.

Match the given patterns against a list of clauses

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.


VarMP Nat

De Bruijn index (usually, rightmost variable in patterns is 0).

ConMP ConHead (Maybe ConPOrigin) [Arg MPat] 
LitMP Literal 
DotMP MPat

For keeping track of the original dot positions.


For dot patterns that cannot be turned into patterns.

ProjMP QName

Projection copattern.


data Match a Source #

If matching is inconclusive (Block) we want to know which variables are blocking the match.


Yes a

Matches unconditionally.


Definitely does not match.

Block BlockingVars

Could match if non-empty list of blocking variables is instantiated properly.


Could match if split on possible projections is performed.


Functor Match Source # 


fmap :: (a -> b) -> Match a -> Match b #

(<$) :: a -> Match b -> Match a #

Monoid a => Monoid (Match a) Source #

Combine results of checking whether function clause patterns covers split clause patterns.

No is dominant: if one function clause pattern is disjoint to the corresponding split clause pattern, then the whole clauses are disjoint.

Yes is neutral: for a match, all patterns have to match.

Block accumulates variables of the split clause that have to be instantiated to make the split clause an instance of the function clause.

BlockP yields to Block, since blocking vars can also block the result type.


mempty :: Match a #

mappend :: Match a -> Match a -> Match a #

mconcat :: [Match a] -> Match a #

data BlockingVar Source #

Variable blocking a match.




  • blockingVarNo :: Nat

    De Bruijn index of variable blocking the match.

  • blockingVarCons :: Maybe [ConHead]

    Nothing means there is an overlapping match for this variable. This happens if one clause has a constructor pattern at this position, and another a variable. It is also used for "just variable".

    Just cons means that it is an non-overlapping match and cons are the encountered constructors.

zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars Source #

Left dominant merge of blocking vars.

choice :: Match a -> Match a -> Match a Source #

choice m m' combines the match results m of a function clause with the (already combined) match results $m'$ of the later clauses. It is for skipping clauses that definitely do not match (No). It is left-strict, to be used with foldr. If one clause unconditionally matches (Yes) we do not look further.

matchLits :: Clause -> [Arg DeBruijnPattern] -> Bool Source #

Check if a clause could match given generously chosen literals

matchClause :: MatchLit -> [Arg MPat] -> Nat -> Clause -> Match (Nat, [MPat]) Source #

matchClause mlit qs i c checks whether clause c number i covers a split clause with patterns qs.

matchPats :: MatchLit -> [Arg (Pattern' a)] -> [Arg MPat] -> Match [MPat] Source #

matchPats mlit ps qs checks whether a function clause with patterns ps covers a split clause with patterns qs.

Issue 842: if in case of functions with varying arity, the split clause has proper patterns left, we refuse to match, because it would be troublesome to construct the split tree later. We would have to move bindings from the rhs to the lhs. For example, this is rejected: F : Bool -> Set1 F true = Set F = x -> Set

matchPat :: MatchLit -> Pattern' a -> MPat -> Match [MPat] Source #

matchPat mlit p q checks whether a function clause pattern p covers a split clause pattern q. There are three results: Yes () means it covers, because p is a variable pattern or q is a wildcard. No means it does not cover. Block [x] means p is a proper instance of q and could become a cover if q was split on variable x.