module McCarthyPainter where

open import Nat
open import List
open import Product
open import ReflexiveTransitiveClosure
open import AddExpr

-- The virtual machine consists of
-- a "code", which is a sequence of instructions "LOAD n, ADD",
-- and a "stack" of intermediate expressions.
-- The empty sequence is called "HALT".

data Code : Set where
  LOAD : Nat → Code → Code
  ADD : Code → Code
  HALT : Code

Stack = List Nat
Machine = Code × Stack

-- We define one-step-reduction for this virtual machine

data _⇒_ : Machine → Machine → Set where

  loadstep : {cd : Code} → {n : Nat} → {S : Stack}
           → < LOAD n cd , S > ⇒ < cd , n :: S >
           
  addstep : {cd : Code} → {n₀ n₁ : Nat} → {S : Stack}
          → < ADD cd , n₀ :: (n₁ :: S) > ⇒ < cd , n₀ + n₁ :: S >

-- The compiler turns an additive expression into a sequence of instructions (a code)

compile : AddExpr → Code → Code
compile (const n) cd = LOAD n cd
compile (add e₀ e₁) cd = compile e₁ (compile e₀ (ADD cd))

-- We can define many-step-reduction as the reflexive transitive closure of one-step reduction

_⇒*_ : Machine → Machine → Set
m ⇒* m' = ((_⇒_) *) m m'

-- or more conveniently as a list of one-step-reductions:

_⇒⁺_ : Machine → Machine → Set
m ⇒⁺ m' = ((_⇒_) **) m m'

{-
We can now state the compiler-correctness theorem

compiler-correct : (e : AddExpr) 
    → < compile e HALT , [] > ⇒⁺ < HALT , [[ e ]] :: [] >

which states that if you compile an additive expression and then 
run the virtual machine, it will stop with the value of
the additive expression on the stack.

The theorem will be proved by induction on the additive expression. However, we will need to strengthen the induction hypothesis.
It doesn't suffice to prove that the compiler works when it starts with an empty stack, but when it starts with an arbitrary stack:
-}

compiler-correct-inv : (e : AddExpr) → (cd : Code) → (S : Stack)
                     → < compile e cd , S > ⇒⁺ < cd , [[ e ]] :: S >
compiler-correct-inv (const n) cd S = j loadstep
compiler-correct-inv (add e₀ e₁) cd S =
  (compiler-correct-inv e₁ (compile e₀ (ADD cd)) S
  ++ compiler-correct-inv e₀ (ADD cd) ([[ e₁ ]] :: S))
  ::: addstep

{-
Note that ::: is "snoc" - adding a new element at the end of a list (of reductions).

Note also that the proof of the induction step (for add e₀ e₁) is based on
the following calculation:

    < compile (add e₀ e₁) cd , S >
=   < compile e₁ (compile e₀ (ADD cd)) , S > -- ind.hyp: (compiler-correct-inv e₁ (compile e₀ (ADD cd)) S)
=>* < compile e₀ (ADD cd) , [[ e₁ ]] :: S > -- ind.hyp: (compiler-correct-inv e₀ (ADD cd) ([[ e₁ ]] :: S)
=>* < ADD cd , [[ e₀ ]] :: [[ e₁ ]] :: S > -- addstep
=>* < cd , [[ e₀ ]] + [[ e₁ ]] :: S >
=   < cd , [[ add e₀ e₁ ]] :: S >

The proof of compiler correctness is now just an instance of the strengthened theorem: 
we start with an empty code (HALT) and an empty stack []:
-}

compiler-correct : (e : AddExpr)
                 → < compile e HALT , [] > ⇒⁺ < HALT , [[ e ]] :: [] >
compiler-correct e = compiler-correct-inv e HALT []