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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.CompiledClause.Match

Synopsis

Documentation

matchCompiledE :: CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term) Source

matchCompiledE c es takes a function given by case tree c and and a spine es and tries to apply the function to es.

type Frame = (CompiledClauses, MaybeReducedElims, Elims -> Elims) Source

A stack entry is a triple consisting of 1. the part of the case tree to continue matching, 2. the current argument vector, and 3. a patch function taking the current argument vector back to the original argument vector.

type Stack = [Frame] Source

match' :: Stack -> ReduceM (Reduced (Blocked Elims) Term) Source

match' tries to solve the matching problems on the Stack. In each iteration, the top problem is removed and handled.

If the top problem was a Done, we succeed.

If the top problem was a Case n and the nth argument of the problem is not a constructor or literal, we are stuck, thus, fail.

If we have a branch for the constructor/literal, we put it on the stack to continue. If we do not have a branch, we fall through to the next problem, which should be the corresponding catch-all branch.

An empty stack is an exception that can come only from an incomplete function definition.