18. Compiler Correctness

09/12/22

/- Lecture 19, IFR (COMP2009,2022-23) -/
set_option pp.structure_projections false
namespace l19
inductive Expr : Type 
| const : ℕ → Expr
| var : string → Expr
| plus : Expr → Expr → Expr
| times : Expr → Expr → Expr

open Expr

--- x * (y + 2)

def e1 : Expr 
  := times (var "x") (plus (var "y") (const 2))

-- (x * y) + 2

def e2 := plus (times (var "x") (var "y")) (const 2)

theorem no_conf : ∀ n : ℕ, ∀ l r : Expr, 
    const n ≠ plus l r :=
begin 
  assume n l r h,
  contradiction,
end

theorem inj_plus_l : ∀ l r l' r' : Expr , 
    plus l r = plus l' r' → l=l' :=
begin
  assume l r l' r' h,
  injection h,
end

--#reduce e1

def Env : Type
  := string → ℕ

def eval : Expr → Env → ℕ
| (const n) env := n
| (var s) env := env s
| (plus l r) env := (eval l env) + (eval r env)
| (times l r) env := (eval l env) * (eval r env)

def env0 : Env
| "x" := 3
| "y" := 5
| _ := 0

#reduce env0 "y"

#reduce eval e1 env0

#reduce eval e2 env0

inductive Instr : Type
| pushC : ℕ → Instr
| pushV : string → Instr
| add : Instr
| mult : Instr

open Instr

@[reducible]
def Code : Type
  := list Instr

def Stack : Type
  := list ℕ

def run : Code → Stack → Env → ℕ 
| [] [n] env := n
| (pushC n ::c) s env := run c (n :: s) env
| (pushV x ::c) s env := run c (env x :: s) env
| (add :: c) (m :: n :: s) env := run c ((n + m) :: s) env
| (mult :: c) (m :: n :: s) env := run c ((n * m) :: s) env
| _ _ _ := 0

def c1 : Code
:= [pushV "x",pushV "y",pushC 2,add,mult]

#eval run c1 [] env0

open list

def compile0 : Expr → Code 
| (const n) := [pushC n]
| (var x) := [pushV x]
| (plus l r) := 
(compile0 l) ++ (compile0 r) ++ [add]
| (times l r) := 
(compile0 l) ++ (compile0 r) ++ [mult]
 
#reduce run (compile0 e1) [] env0

#reduce run (compile0 e2) [] env0

theorem compile0_ok : ∀ e : Expr, ∀ env : Env,
 run (compile0 e) [] env = eval e env :=
begin
  sorry
end

-- continuation passing compilation
def compile_aux : Expr → Code → Code 
| (const n) c := pushC n :: c
| (var x) c := pushV x :: c
| (plus l r) c := 
compile_aux l (compile_aux r (add :: c))
| (times l r) c := 
compile_aux l (compile_aux r (mult :: c)) 

def compile (e : Expr) : Code :=
  compile_aux e []

#reduce run (compile e1) [] env0

#reduce run (compile e2) [] env0

lemma compile_aux_lem :
  ∀ e : Expr, ∀ c : Code, ∀ s : Stack, 
  ∀ env : Env,
   run (compile_aux e c) s env =
    run c (eval e env :: s) env :=
begin
  assume e,
  induction e,
  case const : n {
    assume c s env,
    dsimp [compile_aux,eval,run],
    reflexivity,},
  case var : name {
    assume c s env,
    dsimp [compile_aux,eval,run],
    reflexivity,},
  case plus : l r ih_l ih_r {
    assume c s env,
    dsimp [compile_aux],
    rewrite ih_l,
    rewrite ih_r,
    dsimp [eval,run],
    reflexivity,
  },
  case times : l r ih_l ih_r {
    assume c s env,
    dsimp [compile_aux],
    rewrite ih_l,
    rewrite ih_r,
    dsimp [eval,run],
    reflexivity,
  },
end

theorem compile_ok : ∀ e : Expr, ∀ env : Env,
 run (compile e) [] env = eval e env :=
-- run (compile e) [] env
-- = run c (eval e env :: s) env
-- = run (compile_aux e []) [] env
-- = run [] (eval e env :: []) env
-- = eval e env
begin
  assume e env,
  apply compile_aux_lem,
end


end l19