Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Pattern matcher used in the reducer for clauses that have not been compiled to case trees yet.



data Match a Source #

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


Yes Simplification [a] 
DontKnow (Blocked ()) 


Functor Match Source # 


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

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

Null (Match a) Source # 


empty :: Match a Source #

null :: Match a -> Bool Source #

foldMatch :: forall p v. (p -> v -> ReduceM (Match Term, v)) -> [p] -> [v] -> ReduceM (Match Term, [v]) Source #

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

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

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

Match a single copattern.

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

Match a single pattern.

yesSimplification :: (Match a, b) -> (Match a, b) Source #