Lean4
/-- The program that evaluates code `c` with continuation `k`. This expects an initial state where
`trList v` is on `main`, `trContStack k` is on `stack`, and `aux` and `rev` are empty.
See the section documentation for details. -/
@[simp]
def trNormal : Code → Cont' → Λ'
| Code.zero', k => (Λ'.push main fun _ => some Γ'.cons) <| Λ'.ret k
| Code.succ, k => head main <| Λ'.succ <| Λ'.ret k
| Code.tail, k => Λ'.clear natEnd main <| Λ'.ret k
| Code.cons f fs, k =>
(Λ'.push stack fun _ => some Γ'.consₗ) <|
Λ'.move (fun _ => false) main rev <| Λ'.copy <| trNormal f (Cont'.cons₁ fs k)
| Code.comp f g, k => trNormal g (Cont'.comp f k)
| Code.case f g, k => Λ'.pred (trNormal f k) (trNormal g k)
| Code.fix f, k => trNormal f (Cont'.fix f k)
