module McCarthyPainter where

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

-- a simplified version of the fundamental paper of McCarthy and Painter
-- on correctness of a compiler for arithmetic expressions (1967)

data Expr : Set where
  const : Nat → Expr
  add : Expr → Expr → Expr

val : Expr → Nat
val (const n) = n
val (add e₀ e₁) = val e₀ + val e₁

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

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

Stack = List Nat
Machine = Code × Stack

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 >

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

-- Theorem 0.1 in Thierry's notes

compiler-correct-inv : (e : Expr) → (cd : Code) → (S : Stack) → < compile e cd , S > ⇒* < cd , val e :: S >
compiler-correct-inv (const n) cd S = i < compile (const n) cd , S > < cd , val (const n) :: S > loadstep
compiler-correct-inv (add e₀ e₁) cd S = t _
                                          < ADD cd , val e₀ :: (val e₁ :: S) >
                                          _
                                          (t _ < compile e₀ (ADD cd) , val e₁ :: S > _ (compiler-correct-inv e₁ (compile e₀ (ADD cd)) S)
                                                   (compiler-correct-inv e₀ (ADD cd) (val e₁ :: S)))
                                          (i < ADD cd , val e₀ :: (val e₁ :: S) > < cd , (val e₀ + val e₁) :: S > addstep)

compiler-correct : (e : Expr) → < compile e HALT , [] > ⇒* < HALT , val e :: [] >
compiler-correct e = compiler-correct-inv e HALT []

{-

   < compile (add e₀ e₁) cd , S >
=  < compile e₁ (compile e₀ (ADD cd)) , S > -- ind.hyp
=>* < compile e₀ (ADD cd) , val e₁ :: S > -- ind.hyp
=>* < ADD cd , val e₀ :: val e₁ :: S > -- addstep
=>* < cd , (val e₀) + (val e₁) :: S >
= < cd , (val (add e₀ e₁) :: S >

-}