Agda.TypeChecking.CompiledClause.Match

Documentation

matchCompiled :: CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)

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

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)

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]

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

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.