1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_alt_semantics"; 2 3open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory; 4open optionTheory arithmeticTheory relationTheory; 5 6open lisp_sexpTheory lisp_parseTheory lisp_semanticsTheory; 7 8infix \\ 9val op \\ = op THEN; 10val RW = REWRITE_RULE; 11val RW1 = ONCE_REWRITE_RULE; 12 13 14(* We define an alternative formulation of the semantics that is 15 better suited for compiler verification. At the bottom of this 16 script we prove that the two fomrmulations are equivalent. *) 17 18val isFun_def = Define `(isFun (Fun x) = T) /\ (isFun _ = F)`; 19 20val (RR_ev_rules,RR_ev_ind,RR_ev_cases) = Hol_reln ` 21 (!s a fns. 22 RR_ev (Const s, a,fns,io,ok) (s,fns,io,ok)) 23 /\ 24 (!x (a: string |-> SExp) fns. 25 x IN FDOM a ==> 26 RR_ev (Var x,a,fns,io,ok) (a ' x,fns,io,ok)) 27 /\ 28 (!a fns io s fns1 io1. 29 RR_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==> 30 RR_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1)) 31 /\ 32 (!a fns io s1 fns1 io1 t ts. 33 RR_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 ==> 34 RR_ev (Or (t::ts),a,fns,io,ok) (s1,fns1,io1,ok1)) 35 /\ 36 (!a fns io s1 fns1 io1 s2 fns2 io2 t ts. 37 RR_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~(isTrue s1) /\ 38 RR_ev (Or ts,a,fns1,io1,ok1) (s2,fns2,io2,ok2) ==> 39 RR_ev (Or (t::ts),a,fns,io,ok) (s2,fns2,io2,ok2)) 40 /\ 41 (!e1 e2 e3 s1 s a. 42 RR_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~isTrue s1 /\ 43 RR_ev (e3,a,fns1,io1,ok1) (s,fns2,io2,ok2) 44 ==> 45 RR_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2)) 46 /\ 47 (!e1 e2 e3 s1 s a. 48 RR_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 /\ 49 RR_ev (e2,a,fns1,io1,ok1) (s,fns2,io2,ok2) 50 ==> 51 RR_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2)) 52 /\ 53 (!e xs ys fns a. 54 RR_evl (ys,a,fns,io,ok) (sl,fns1,io1,ok1) /\ (LENGTH xs = LENGTH ys) /\ 55 RR_ev (e,FUNION (VarBind xs sl) a,fns1,io1,ok1) (x,fns2,io2,ok2) 56 ==> 57 RR_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2)) 58 /\ 59 (!el args a fc fns x. 60 RR_evl (el,a,fns,io,ok) (args,fns1,io1,ok1) /\ RR_ap (fc,args,a,fns1,io1,ok1) (x,fns2,io2,ok2) /\ 61 ~(isFun fc) 62 ==> 63 RR_ev (App fc el,a,fns,io,ok) (x,fns2,io2,ok2)) 64 /\ 65 (!fc args a fns f. 66 (EVAL_DATA_OP fc = (f,LENGTH args)) 67 ==> 68 RR_ap (PrimitiveFun fc,args,a,fns,io,ok) (f args,fns,io,ok)) 69 /\ 70 (!el args a fc fns params exp x. 71 fc IN FDOM fns1 /\ 72 (fns1 ' fc = (params,exp)) /\ (LENGTH params = LENGTH args) /\ 73 RR_evl (el,a,fns,io,ok) (args,fns1,io1,ok1) /\ 74 RR_ev (exp,VarBind params args,fns1,io1,ok1) (x,fns2,io2,ok2) 75 ==> 76 RR_ev (App (Fun fc) el,a,fns,io,ok) (x,fns2,io2,ok2)) 77 /\ 78 (!args a fns. 79 RR_ap (Print,args,a,fns,io,ok) (Sym "NIL",fns, 80 io ++ sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n",ok)) 81 /\ 82 (!args a fns. 83 RR_ap (Error,args,a,fns,io,ok) (anything,fns, 84 io ++ sexp2string (list2sexp (Sym "ERROR"::args)) ++ "\n",F)) 85 /\ 86 (!a fns fc formals body. 87 RR_ap (Define,[fc; formals; body],a,fns,io,ok) 88 (Sym "NIL",add_def fns (getSym fc,MAP getSym (sexp2list formals),sexp2term body), 89 io,ok /\ ~(getSym fc IN FDOM fns))) 90 /\ 91 (!args params a fname fns x. 92 fname IN FDOM fns /\ 93 (fns ' fname = (params,exp)) /\ (LENGTH params = LENGTH args) /\ 94 RR_ev (exp,VarBind params args,fns,io,ok) (x,fns2,io2,ok2) 95 ==> 96 RR_ap (Funcall,Sym fname::args,a,fns,io,ok) (x,fns2,io2,ok2)) 97 /\ (* give short-cut semantics for failure states *) 98 (!f args a fns io res. 99 RR_ap (Fun f,args,a,fns,io,F) (res,fns,io,F)) 100 /\ (* give short-cut semantics for failure states *) 101 (!args a fns io res. 102 RR_ap (Funcall,args,a,fns,io,F) (res,fns,io,F)) 103 /\ (* give short-cut semantics for failure states *) 104 (!exp a fns io res. 105 RR_ev (exp,a,fns,io,F) (res,fns,io,F)) 106 /\ 107 (!a. 108 RR_evl ([],a,fns,io,ok) ([],fns,io,ok)) 109 /\ 110 (!e el s sl a. 111 RR_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) /\ RR_evl (el,a,fns1,io1,ok1) (sl,fns2,io2,ok2) 112 ==> 113 RR_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2:bool)) 114 /\ 115 116 (* semantics of macros below *) 117 118 (!e a fns io s fns1 io1. 119 RR_ev (App (PrimitiveFun opCAR) [e],a,fns,io,ok) (s,fns1,io1,ok1) ==> 120 RR_ev (First e,a,fns,io,ok) (s,fns1,io1,ok1)) 121 /\ 122 (!e a fns io s fns1 io1. 123 RR_ev (First (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==> 124 RR_ev (Second e,a,fns,io,ok) (s,fns1,io1,ok1)) 125 /\ 126 (!e a fns io s fns1 io1. 127 RR_ev (Second (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==> 128 RR_ev (Third e,a,fns,io,ok) (s,fns1,io1,ok1)) 129 /\ 130 (!e a fns io s fns1 io1. 131 RR_ev (Third (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==> 132 RR_ev (Fourth e,a,fns,io,ok) (s,fns1,io1,ok1)) 133 /\ 134 (!e a fns io s fns1 io1. 135 RR_ev (Fourth (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==> 136 RR_ev (Fifth e,a,fns,io,ok) (s,fns1,io1,ok1)) 137 /\ 138 (!zs x a fns io s fns1 io1. 139 RR_ev (LamApp (MAP FST zs) x (MAP SND zs),a,fns,io,ok) (s,fns1,io1,ok1) ==> 140 RR_ev (Let zs x,a,fns,io,ok) (s,fns1,io1,ok1)) 141 /\ 142 (!x a fns io s fns1 io1. 143 RR_ev (x,a,fns,io,ok) (s,fns1,io1,ok1) ==> 144 RR_ev (LetStar [] x,a,fns,io,ok) (s,fns1,io1,ok1)) 145 /\ 146 (!z zs x a fns io s fns1 io1. 147 RR_ev (Let [z] (LetStar zs x),a,fns,io,ok) (s,fns1,io1,ok1) ==> 148 RR_ev (LetStar (z::zs) x,a,fns,io,ok) (s,fns1,io1,ok1)) 149 /\ 150 (!a fns io s fns1 io1. 151 RR_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==> 152 RR_ev (Cond [],a,fns,io,ok) (s,fns1,io1,ok1)) 153 /\ 154 (!x1 x2 qs a fns io s fns1 io1. 155 RR_ev (If x1 x2 (Cond qs),a,fns,io,ok) (s,fns1,io1,ok1) ==> 156 RR_ev (Cond ((x1,x2)::qs),a,fns,io,ok) (s,fns1,io1,ok1)) 157 /\ 158 (!a fns io s fns1 io1. 159 RR_ev (Const (Sym "T"),a,fns,io,ok) (s,fns1,io1,ok1) ==> 160 RR_ev (And [],a,fns,io,ok) (s,fns1,io1,ok1)) 161 /\ 162 (!a fns io s fns1 io1. 163 RR_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==> 164 RR_ev (List [],a,fns,io,ok) (s,fns1,io1,ok1)) 165 /\ 166 (!a fns io s fns1 io1. 167 RR_ev (t,a,fns,io,ok) (s,fns1,io1,ok1) ==> 168 RR_ev (And [t],a,fns,io,ok) (s,fns1,io1,ok1)) 169 /\ 170 (!a fns io s fns1 io1. 171 RR_ev (If t1 (And (t2::ts)) (Const (Sym "NIL")),a,fns,io,ok) (s,fns1,io1,ok1) ==> 172 RR_ev (And (t1::t2::ts),a,fns,io,ok) (s,fns1,io1,ok1)) 173 /\ 174 (!a fns io s fns1 io1. 175 RR_ev (App (PrimitiveFun opCONS) [t;List ts],a,fns,io,ok) (s,fns1,io1,ok1) ==> 176 RR_ev (List (t::ts),a,fns,io,ok) (s,fns1,io1,ok1)) 177 /\ 178 (!fname ps body a fns io s fns1 io1. 179 RR_ev (App Define [Const (Sym fname); Const (list2sexp (MAP Sym ps)); Const body],a,fns,io,ok) (s,fns1,io1,ok1) ==> 180 RR_ev (Defun fname ps body,a,fns,io,ok) (s,fns1,io1,ok1))`; 181 182val RR_evl_LENGTH = save_thm("RR_evl_LENGTH", 183 RR_ev_ind 184 |> Q.SPECL [`\x y. T`,`\x y. (LENGTH (FST x) = LENGTH (FST y))`,`\x y. T`] 185 |> SIMP_RULE std_ss [LENGTH]); 186 187 188(* R_ev implies RR_ev *) 189 190val lemma = R_ev_ind 191 |> Q.SPECL [`\x y. if isFun (FST x) then 192 ?fc args a fns1 io1 ok1 fc' params exp. 193 ((fc,args,a,fns1,io1,ok1) = x) /\ 194 (fc = Fun fc') /\ fc' IN FDOM fns1 /\ 195 (fns1 ' fc' = (params,exp)) /\ 196 (LENGTH params = LENGTH args) /\ 197 RR_ev (exp,VarBind params args,fns1,io1,ok1) y 198 else RR_ap x y`, 199 `\x y. RR_evl x y`, 200 `\x y. RR_ev x y`] 201 202val goal = lemma |> concl |> rand; 203 204(* 205 set_goal([],goal) 206*) 207 208val R_ev_IMP_RR_ev = prove(goal, 209 MATCH_MP_TAC lemma 210 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [] 211 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 212 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 213 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 214 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 215 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 216 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 217 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 218 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 219 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 220 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 221 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 222 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 223 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 224 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 225 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 226 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 227 THEN1 (ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] \\ METIS_TAC []) 228 \\ ONCE_REWRITE_TAC [RR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] 229 \\ METIS_TAC []) |> SIMP_RULE std_ss [] |> CONJUNCTS |> last; 230 231val _ = save_thm("R_ev_IMP_RR_ev",R_ev_IMP_RR_ev); 232 233val _ = export_theory(); 234