theory CompilingLets imports Main begin types binop = "nat \ nat \ nat" types var = "nat" datatype expr = Num nat | Var var | BinOp binop expr expr | LetE var expr expr types env = "(var \ nat) list" primrec lookup :: "env \ var \ nat" where "lookup [] x = 0" | "lookup (b#bs) x = (if x = fst b then snd b else lookup bs x)" definition extend :: "env \ var \ nat \ env" where "extend E x v \ (x,v)#E" declare extend_def[simp] primrec eval :: "expr \ env \ 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 \ env \ stack \ env \ stack" where "exec [] E_vs = E_vs" | "exec (i#is) E_vs = (case i of Const v \ exec is (fst E_vs, v#(snd E_vs)) | Load x \ exec is (fst E_vs, (lookup (fst E_vs) x)#(snd E_vs)) | Push x \ exec is (extend (fst E_vs) x (hd (snd E_vs)), tl (snd E_vs)) | Pop \ exec is (tl (fst E_vs), snd E_vs) | Apply f \ 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