{-
  Toy programming language with expressions like:

  - add (lit two) (lit two)
  - add (lit two) (add (lit one) (lit one))

  Goal:
  0. Define the type of abstract syntax trees
  1. Implement an interpreter (reference implementation)
  2. Implement a virtual machine
  3. Implement a compiler
  4. Verify the correctness of the compiler
-}

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.Reasoning.Core

-- Step 0. The Agda datatype of expressions of Toy
data Expr : Set where
  lit : ℕ → Expr
  add : Expr → Expr → Expr

-- Step 1. An interpreter for Toy
eval : Expr → ℕ
eval (lit x)   = x
eval (add x y) = eval x + eval y

example-expr : Expr
example-expr = add (lit two) (add (lit one) (lit one))

_ : eval example-expr ≡ four
_ = refl

-- Step 2. Implementing a virtual machine, more precisely a stack machine

-- The Agda datatypes of operations supported by the virtual machine
data Op : Set where
  PUSH : ℕ → Op
  SUM  : Op
  POP  : Op

-- The Agda type of possible stacks for the virtual machine
Stack : Set
Stack = List ℕ

-- The Agda type of machine code for the virtual machine
Code : Set
Code = List Op

-- A simulator for our virtual machine:
-- "run cs st" runs the given code "cs" on the initial stack "st" and outputs
-- the resulting stack.
run : Code → Stack → Stack
run []            st           = st
run (PUSH x ∷ cs) st           = run cs (x ∷ st)
run (SUM    ∷ cs) []           = []
run (SUM    ∷ cs) (x ∷ [])     = []
run (SUM    ∷ cs) (x ∷ y ∷ st) = run cs ((y + x) ∷ st)
run (POP    ∷ cs) []           = run cs []
run (POP    ∷ cs) (x ∷ st)     = run cs st

-- Step 3. Implementing the compiler, from Toy to Code
compile : Expr → Code → Code
compile (lit x)   cs = PUSH x ∷ cs
compile (add x y) cs = compile x (compile y (SUM ∷ cs)) 

compile₀ : Expr → Code
compile₀ x = compile x []

-- Step 4. Verification
theorem : (e : Expr) (cs : Code) (st : Stack) → run (compile e cs) st ≡ run cs (eval e ∷ st)
theorem (lit x)   cs st = refl
theorem (add x y) cs st = begin
  run (compile (add x y) cs) st             ≡⟨⟩
  run (compile x (compile y (SUM ∷ cs))) st ≡⟨ theorem x (compile y (SUM ∷ cs)) st ⟩
  run (compile y (SUM ∷ cs)) (eval x ∷ st)  ≡⟨ theorem y (SUM ∷ cs) (eval x ∷ st) ⟩
  run (SUM ∷ cs) (eval y ∷ eval x ∷ st)     ≡⟨⟩
  run cs ((eval x + eval y) ∷ st)           ≡⟨⟩
  run cs (eval (add x y) ∷ st)              ∎

theorem₀ : (e : Expr) → run (compile₀ e) [] ≡ eval e ∷ []
theorem₀ e = theorem e [] []