(* 
ソース言語：代入文, 複文
マシン命令セット：Load, Store, Lit, Add
 *)


(*************************)
(* stack machine         *)
(*************************)

val _ = Hol_datatype
    `machine =
    machine_init |
    set_locvar of num => num => machine |
    push of num => machine`;;
val get_locvar = Define
    `(get_locvar n machine_init = 0) /\
    (get_locvar n1 (set_locvar n2 x m) = 
     if n1 = n2 then x else get_locvar n1 m) /\
    (get_locvar n (push x m) = get_locvar n m)`;;
val top = Define
    `(top (set_locvar n x m) = top m) /\
    (top (push x m) = x)`;;
val pop = Define
    `(pop (set_locvar n x m) = pop m) /\
    (pop (push x m) = m)`;;


val exec_load = Define
    `exec_load n s =
    let x = get_locvar n s in
	push x s`;;
val exec_store = Define
    `exec_store n s =
    let x = top s in
    let s1 = pop s in 
	set_locvar n x s1`;;
val exec_lit = Define
    `exec_lit x s = push x s`;;
val exec_add = Define
    `exec_add s =
    let x1 = top s in
    let s1 = pop s in
    let x2 = top s1 in
    let s2 = pop s1 in 
	push (x1+x2) s2`;;
val _ = Hol_datatype 
    `instr = 
    Load of num
  | Store of num
  | Lit of num
  | Add`;;
val exec_instr = Define    
    `(exec_instr (Load n) s = exec_load n s) /\
    (exec_instr (Store n) s = exec_store n s) /\
     (exec_instr (Lit x) s = exec_lit x s) /\
      (exec_instr Add s = exec_add s)`;;
val exec = Define 
    `(exec [] s = s) /\
    (exec (x::l) s = exec l (exec_instr x s))`;;



(*************************)
(* source language       *)
(*************************)

val _= Hol_datatype 
    `exp =
    Const of num
  | Var of num
  | Sum of exp => exp`;;
val _ = Hol_datatype
    `stm =
    Assign of exp => exp
  | Seq of stm => stm`;;
val is_Var = Define
    `(is_Var (Var x) = T) /\ (is_Var (Const x) = F)
    /\ (is_Var (Sum y z) = F)`;;
val dest_Var = Define
    `dest_Var (Var x) = x`;;


val _ = Hol_datatype
    `env =
    env_init |
    set_var of num => num => env`;;
val get_var = Define
    `(get_var n env_init = 0) /\
    (get_var n1 (set_var n2 x env) = 
     if n1 = n2 then x else get_var n1 env)`;;
val eval_exp = Define
    `(eval_exp (Const x) env = x) /\
    (eval_exp (Var x) env = get_var x env) /\
     (eval_exp (Sum y z) env = eval_exp y env + eval_exp z env)`;;
val eval = Define
    `(eval (Assign e1 e2) env = 
      if is_Var e1 then 
	  let x = dest_Var e1 in
	  let y = eval_exp e2 env in
	      set_var x y env
      else
	  env) /\
     (eval (Seq s1 s2) env = eval s2 (eval s1 env))`;;




(*************************)
(* compiler              *)
(*************************)

val compile_exp = Define
    `(compile_exp (Const x) = [Lit x]) /\
    (compile_exp (Var x) = [Load x]) /\
     (compile_exp (Sum e1 e2) =
      APPEND (compile_exp e1) (APPEND (compile_exp e2) [Add]))`;;
val compile = Define
    `(compile (Assign e1 e2) = 
      if is_Var(e1) then 
	  APPEND (compile_exp e2) [Store (dest_Var e1)]
      else
	  []) /\
     (compile (Seq s1 s2) =
      APPEND (compile s1) (compile s2))`;;



(*************************)
(* proof                 *)
(*************************)


val exec_APPEND = prove
    (``!l1 l2 s. exec (APPEND l1 l2) s = exec l2 (exec l1 s)``,
     Induct_on `l1` THEN
     RW_TAC list_ss [exec]);;
val pop_exec_compile_exp = prove
    (``!e s. pop (exec (compile_exp e) s) = s``,
     Induct_on `e` THENL
     [R_TAC [compile_exp] THEN
      R_TAC [exec,exec_instr,exec_lit] THEN
      R_TAC [pop],
      R_TAC [compile_exp] THEN
      R_TAC [exec,exec_instr,exec_load] THEN
      LETR_TAC THEN
      R_TAC [pop],
      R_TAC [compile_exp] THEN
      R_TAC [exec_APPEND] THEN
      R_TAC [exec,exec_instr,exec_add] THEN
      LETR_TAC THEN
      R_TAC [pop] THEN
      RW_TAC list_ss []]);;
val get_locvar_exec_compile_exp = prove
      (``!n e s. 
       get_locvar n (exec (compile_exp e) s) = get_locvar n s``,
       Induct_on `e` THENL
       [R_TAC [exec,compile_exp] THEN 
	R_TAC [exec_instr,exec_lit] THEN
	R_TAC [get_locvar],
	R_TAC [exec,compile_exp] THEN
	R_TAC [exec_instr,exec_load] THEN
	LETR_TAC THEN
	R_TAC [get_locvar],
	R_TAC [exec,compile_exp] THEN
	R_TAC [exec_APPEND] THEN
	R_TAC [exec,exec_instr,exec_add] THEN
	LETR_TAC THEN
	R_TAC [get_locvar] THEN
	R_TAC [pop_exec_compile_exp]]);;
val compiler_exp_correctness = prove
    (``!e s env. 
     (!n. get_locvar n s = get_var n env) ==>
	  (top (exec (compile_exp e) s) = eval_exp e env)``,
     Induct_on `e` THENL
     [R_TAC [compile_exp,eval_exp] THEN
      R_TAC [exec,exec_instr,exec_lit] THEN
      R_TAC [top],
      R_TAC [compile_exp,eval_exp] THEN
      R_TAC [exec,exec_instr,exec_load] THEN
      LETR_TAC THEN
      RW_TAC bool_ss [top],
      R_TAC [compile_exp,eval_exp] THEN
      R_TAC [exec_APPEND] THEN
      R_TAC [exec,exec_instr,exec_add] THEN
      LETR_TAC THEN
      RW_TAC bool_ss [top] THEN
      RW_TAC bool_ss [pop_exec_compile_exp] THEN
      ASSUM_LIST (fn thl => ASSUME_TAC
		  (SPEC ``exec (compile_exp e) s`` (el 2 thl))) THEN
      ASSUM_LIST (fn thl => ASSUME_TAC
		  (REWRITE_RULE [get_locvar_exec_compile_exp] (el 1 thl))) THEN
      RES_TAC THEN
      RW_TAC arith_ss []]);;
val compiler_correctness = prove
    (``!n s prog env. 
     (!n. get_locvar n s = get_var n env) ==>
	  (get_locvar n (exec (compile prog) s) = 
	   get_var n (eval prog env))``,
     Induct_on `prog` THENL
     [R_TAC [compile,eval] THEN
      Induct_on `e` THENL
      [SIMP_TAC bool_ss [is_Var] THEN
       R_TAC [exec] THEN
       RW_TAC bool_ss [],
       LETR_TAC THEN
       SIMP_TAC bool_ss [is_Var] THEN
       R_TAC [exec_APPEND] THEN
       R_TAC [exec,exec_instr,exec_store] THEN
       LETR_TAC THEN
       R_TAC [dest_Var] THEN
       REPEAT STRIP_TAC THEN
       R_TAC [get_locvar] THEN
       RW_TAC bool_ss [] THENL
       [R_TAC [get_var] THEN
	RW_TAC bool_ss [compiler_exp_correctness],
	RW_TAC bool_ss [get_var] THEN
	RW_TAC bool_ss [pop_exec_compile_exp]],
       SIMP_TAC bool_ss [is_Var] THEN
       RW_TAC bool_ss [exec]],
      R_TAC [compile,eval] THEN
      R_TAC [exec_APPEND] THEN
      RW_TAC bool_ss []]);;