Lean4
/-- The main program. See the section documentation for details. -/
def tr : Λ' → Stmt'
| Λ'.move p k₁ k₂ q =>
pop' k₁ <| branch (fun s => s.elim true p) (goto fun _ => q) (push' k₂ <| goto fun _ => Λ'.move p k₁ k₂ q)
| Λ'.push k f q => branch (fun s => (f s).isSome) ((push k fun s => (f s).iget) <| goto fun _ => q) (goto fun _ => q)
| Λ'.read q => goto q
| Λ'.clear p k q => pop' k <| branch (fun s => s.elim true p) (goto fun _ => q) (goto fun _ => Λ'.clear p k q)
| Λ'.copy q =>
pop' rev <| branch Option.isSome (push' main <| push' stack <| goto fun _ => Λ'.copy q) (goto fun _ => q)
| Λ'.succ q =>
pop' main <|
branch (fun s => s = some Γ'.bit1) ((push rev fun _ => Γ'.bit0) <| goto fun _ => Λ'.succ q) <|
branch (fun s => s = some Γ'.cons)
((push main fun _ => Γ'.cons) <| (push main fun _ => Γ'.bit1) <| goto fun _ => unrev q)
((push main fun _ => Γ'.bit1) <| goto fun _ => unrev q)
| Λ'.pred q₁ q₂ =>
pop' main <|
branch (fun s => s = some Γ'.bit0) ((push rev fun _ => Γ'.bit1) <| goto fun _ => Λ'.pred q₁ q₂) <|
branch (fun s => natEnd s.iget) (goto fun _ => q₁)
(peek' main <|
branch (fun s => natEnd s.iget) (goto fun _ => unrev q₂)
((push rev fun _ => Γ'.bit0) <| goto fun _ => unrev q₂))
| Λ'.ret (Cont'.cons₁ fs k) =>
goto fun _ =>
move₂ (fun _ => false) main aux <|
move₂ (fun s => s = Γ'.consₗ) stack main <| move₂ (fun _ => false) aux stack <| trNormal fs (Cont'.cons₂ k)
| Λ'.ret (Cont'.cons₂ k) => goto fun _ => head stack <| Λ'.ret k
| Λ'.ret (Cont'.comp f k) => goto fun _ => trNormal f k
| Λ'.ret (Cont'.fix f k) =>
pop' main <| goto fun s => cond (natEnd s.iget) (Λ'.ret k) <| Λ'.clear natEnd main <| trNormal f (Cont'.fix f k)
| Λ'.ret Cont'.halt => (load fun _ => none) <| halt
