{-# OPTIONS --allow-unsolved-metas #-}
open import Padova2024.EquationalReasoning
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
_+_ : ℕ → ℕ → ℕ
zero + b = b
succ a + b = succ (a + b)
data List (X : Set) : Set where
[] : List X
_∷_ : X → List X → List X
_++_ : {X : Set} → List X → List X → List X
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
data Expr : Set where
lit : ℕ → Expr
add : Expr → Expr → Expr
example : Expr
example = add (lit zero) (add (lit (succ zero)) (lit zero))
eval : Expr → ℕ
eval (lit x) = x
eval (add a b) = eval a + eval b
_ : eval example ≡ succ zero
_ = refl
data Op : Set where
PUSH : ℕ → Op
SUM : Op
Stack : Set
Stack = List ℕ
Code : Set
Code = List Op
run : Code → Stack → Stack
run [] s = s
run (PUSH x ∷ c) s = run c (x ∷ s)
run (SUM ∷ c) (a ∷ (b ∷ s)) = run c ((a + b) ∷ s)
run _ _ = []
compile : Expr → Code → Code
compile (lit x) c = PUSH x ∷ c
compile (add a b) c = compile b (compile a (SUM ∷ c))
theorem : (e : Expr) (c : Code) (s : Stack) → run (compile e c) s ≡ run c (eval e ∷ s)
theorem (lit x) c s = refl
theorem (add a b) c s = begin
run (compile (add a b) c) s ≡⟨⟩
run (compile b (compile a (SUM ∷ c))) s ≡⟨ theorem b (compile a (SUM ∷ c)) s ⟩
run (compile a (SUM ∷ c)) (eval b ∷ s) ≡⟨ theorem a (SUM ∷ c) (eval b ∷ s) ⟩
run c ((eval a + eval b) ∷ s) ≡⟨⟩
run c (eval (add a b) ∷ s) ∎
compile₀ : Expr → Code
compile₀ e = compile e []
theorem₀ : (e : Expr) → run (compile₀ e) [] ≡ (eval e ∷ [])
theorem₀ e = theorem e [] []