theory CompilingLets
imports Main
begin

types binop = "nat \<Rightarrow> nat \<Rightarrow> nat"
types var = "nat"

datatype expr = 
    Num nat
  | Var var
  | BinOp binop expr expr
  | LetE var expr expr

types env = "(var \<times> nat) list"

primrec lookup :: "env \<Rightarrow> var \<Rightarrow> nat" where
  "lookup [] x = 0" |
  "lookup (b#bs) x = (if x = fst b then snd b else lookup bs x)"

definition extend :: "env \<Rightarrow> var \<Rightarrow> nat \<Rightarrow> env" where
  "extend E x v \<equiv> (x,v)#E"
declare extend_def[simp]

primrec eval :: "expr \<Rightarrow> env \<Rightarrow> nat" where
  "eval (Num n) E = n" |
  "eval (Var x) E = lookup E x" |
  "eval (BinOp f e1 e2) E = f (eval e1 E) (eval e2 E)" |
  "eval (LetE x e1 e2) E = eval e2 (extend E x (eval e1 E))"

datatype instr = 
    Const nat
  | Push var
  | Load var
  | Pop 
  | Apply binop

types stack = "nat list" 
  program = "instr list"

primrec exec :: "program \<Rightarrow> env \<times> stack \<Rightarrow> env \<times> stack" where
  "exec [] E_vs = E_vs" |
  "exec (i#is) E_vs = (case i of
     Const v \<Rightarrow> exec is (fst E_vs, v#(snd E_vs))
   | Load x \<Rightarrow> exec is (fst E_vs, (lookup (fst E_vs) x)#(snd E_vs))
   | Push x \<Rightarrow> exec is (extend (fst E_vs) x (hd (snd E_vs)), tl (snd E_vs))
   | Pop \<Rightarrow> exec is (tl (fst E_vs), snd E_vs) 
   | Apply f \<Rightarrow> exec is (fst E_vs, 
                    ((f (hd (snd E_vs)) (hd (tl (snd E_vs))))#(tl (tl (snd E_vs))))))"

(*

  Exercise: define a new compile primrec then prove that 

  (exec (compile e) E_vs) = (fst E_vs, (eval e (fst E_vs))#(snd E_vs))

*)

end