Translate from Agda's desugared pattern matching (CompiledClauses) to our AuxAST.
This is all done by magic. It uses substTerm to translate the actual
terms when the cases have been gone through.
The case expressions that we get use de Bruijn indices that change after
each case in the following way.
Say we have this pattern:
f (X x y) (Y z) = term
Initially, the variables have these indexes:
f 0@(X x y) 1@(Y z) = term
The first case will be on 0, and the variables bound inside the X
pattern will replace the outer index, so we get something like this:
f 0 2@(Y z) = case 0 of X 0 1 -> term
Notice how (Y z) now has index 2.
Then the second pattern is desugared in the same way:
f 0 2 = case 0 of X 0 1 -> case 2 of Y 2 -> term
This replacement is what is done using the replaceAt function.
CompiledClauses also have default branches for when all branches fail (even
inner branches), the catchAllBranch. Epic does not support this, so
we have to add the catchAllBranch to each inner case (here we are calling
it omniDefault). To avoid code duplication it is first bound by a let
expression.
|