Agda.TypeChecking.Patterns.Match

Documentation

data Match a

If matching is inconclusive (DontKnow) we want to know whether it is due to a particular meta variable.

Constructors

Yes Simplification [a]

No

DontKnow (Maybe MetaId)

Instances

Functor Match

Monoid (Match a)

foldMatch :: forall a b. (a -> b -> ReduceM (Match Term, b)) -> [a] -> [b] -> ReduceM (Match Term, [b])

Instead of zipWithM, we need to use this lazy version of combining pattern matching computations.

matchCopatterns :: [NamedArg Pattern] -> [Elim] -> ReduceM (Match Term, [Elim])

matchCopatterns ps es matches spine es against copattern spine ps.

Returns Yes and a substitution for the pattern variables (in form of [Term]) if matching was successful.

Returns No if there was a constructor or projection mismatch.

Returns DontKnow if an argument could not be evaluated to constructor form because of a blocking meta variable.

In any case, also returns spine es in reduced form (with all the weak head reductions performed that were necessary to come to a decision).

matchCopattern :: Pattern -> Elim -> ReduceM (Match Term, Elim)

Match a single copattern.

matchPatterns :: [NamedArg Pattern] -> [Arg Term] -> ReduceM (Match Term, [Arg Term])

matchPattern :: Pattern -> Arg Term -> ReduceM (Match Term, Arg Term)

Match a single pattern.

yesSimplification :: (Match a, t) -> (Match a, t)