Agda.TypeChecking.CompiledClause.Match

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

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.

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.