| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.CompiledClause.Match
Synopsis
- matchCompiled :: CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)
- matchCompiledE :: CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
- type Frame = (CompiledClauses, MaybeReducedElims, Elims -> Elims)
- type Stack = [Frame]
- match' :: Stack -> ReduceM (Reduced (Blocked Elims) Term)
Documentation
matchCompiled :: CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term) Source #
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.
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.