1open HolKernel boolLib bossLib Parse; val _ = new_theory "milawa_init"; 2 3open lisp_extractLib lisp_extractTheory; 4 5open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory; 6open optionTheory arithmeticTheory relationTheory; 7 8open lisp_sexpTheory lisp_semanticsTheory lisp_parseTheory; 9 10open milawa_coreTheory; 11val _ = max_print_depth := 20; 12 13infix \\ 14val op \\ = op THEN; 15val RW = REWRITE_RULE; 16val RW1 = ONCE_REWRITE_RULE; 17 18 19 20(* Reading in the top-level definitions from the Milawa core *) 21 22val (R_aux_exec_rules,R_aux_exec_ind,R_aux_exec_cases) = Hol_reln ` 23 (!fns io. 24 R_aux_exec ([],fns,io) (io,T)) 25 /\ 26 (!xs fns io exp s fns2 io2 ok2 io3 ok3. 27 R_ev (sexp2term exp,FEMPTY,fns,io,T) (s,fns2,io2,ok2) /\ 28 R_aux_exec (xs,fns2,io2 ++ sexp2string s ++ "\n") (io3,ok3) ==> 29 R_aux_exec (exp::xs,fns,io) (io3,ok2 /\ ok3))`; 30 31val R_aux_exec_IMP_R_exec = prove( 32 ``!p q. R_aux_exec p q ==> 33 !str. (FST p = read_sexps str) ==> R_exec (str,SND p) q``, 34 HO_MATCH_MP_TAC R_aux_exec_ind \\ REPEAT STRIP_TAC 35 \\ FULL_SIMP_TAC (srw_ss()) [] \\ POP_ASSUM MP_TAC 36 \\ ONCE_REWRITE_TAC [read_sexps_def] 37 \\ Cases_on `is_eof str` 38 \\ Cases_on `sexp_parse_stream r` 39 \\ Cases_on `q` \\ FULL_SIMP_TAC (srw_ss()) [LET_DEF] 40 THEN1 METIS_TAC [R_exec_cases] 41 \\ REPEAT STRIP_TAC \\ RES_TAC 42 \\ ONCE_REWRITE_TAC [R_exec_cases] \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []); 43 44val PULL_EXISTS_CONJ = METIS_PROVE [] 45 ``(p /\ (?x. q x) = ?x. p /\ q x) /\ ((?x. q x) /\ p = ?x. q x /\ p)`` 46 47val R_aux_exec6 = prove( 48 ``R_ev (sexp2term x1,FEMPTY,fns1,io1,T) (ans1,fns2,io2',ok2) /\ 49 (io2 = io2' ++ sexp2string ans1 ++ "\n") /\ 50 R_ev (sexp2term x2,FEMPTY,fns2,io2,T) (ans2,fns3,io3',ok3) /\ 51 (io3 = io3' ++ sexp2string ans2 ++ "\n") /\ 52 R_ev (sexp2term x3,FEMPTY,fns3,io3,T) (ans3,fns4,io4',ok4) /\ 53 (io4 = io4' ++ sexp2string ans3 ++ "\n") /\ 54 R_ev (sexp2term x4,FEMPTY,fns4,io4,T) (ans4,fns5,io5',ok5) /\ 55 (io5 = io5' ++ sexp2string ans4 ++ "\n") /\ 56 R_ev (sexp2term x5,FEMPTY,fns5,io5,T) (ans5,fns6,io6',ok6) /\ 57 (io6 = io6' ++ sexp2string ans5 ++ "\n") /\ 58 R_ev (sexp2term x6,FEMPTY,fns6,io6,T) (ans6,fns7,io7',ok7) /\ 59 (io7 = io7' ++ sexp2string ans6 ++ "\n") ==> 60 R_aux_exec ([x1;x2;x3;x4;x5;x6],fns1,io1) (io7,ok2 /\ ok3 /\ ok4 /\ ok5 /\ ok6 /\ ok7)``, 61 SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 62 \\ NTAC 8 (ONCE_REWRITE_TAC [R_aux_exec_cases] \\ SIMP_TAC (srw_ss()) []) 63 \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [PULL_EXISTS_CONJ] 64 \\ Q.LIST_EXISTS_TAC [`ans1`,`fns2`,`io2'`,`ok2`] 65 \\ Q.LIST_EXISTS_TAC [`ans2`,`fns3`,`io3'`,`ok3`] 66 \\ Q.LIST_EXISTS_TAC [`ans3`,`fns4`,`io4'`,`ok4`] 67 \\ Q.LIST_EXISTS_TAC [`ans4`,`fns5`,`io5'`,`ok5`] 68 \\ Q.LIST_EXISTS_TAC [`ans5`,`fns6`,`io6'`,`ok6`] 69 \\ Q.LIST_EXISTS_TAC [`ok7`,`ans6`,`fns7`,`io7'`] 70 \\ ASM_SIMP_TAC std_ss []) |> GEN_ALL; 71 72val list2sexp_11 = prove( 73 ``!xs ys. (list2sexp xs = list2sexp ys) = (xs = ys)``, 74 Induct \\ Cases_on `ys` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []); 75 76val MAP_Sym_11 = prove( 77 ``!xs ys. (MAP Sym xs = MAP Sym ys) = (xs = ys)``, 78 Induct \\ Cases_on `ys` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []); 79 80val sexp2list_list2sexp = prove( 81 ``!xs. sexp2list (list2sexp xs) = xs``, 82 Induct \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss []); 83 84val MAP_getSym_MAP_Sym = prove( 85 ``!xs. MAP getSym (MAP Sym xs) = xs``, 86 Induct \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss []); 87 88val R_ev_App_Define = prove( 89 ``!params. 90 R_ev (App Define [Const (Sym name); Const (list2sexp (MAP Sym params)); Const body],FEMPTY,fns,io,T) 91 (ans,fns1,io1,ok1) = 92 (ans = Sym "NIL") /\ (fns1 = add_def fns (name,params,sexp2term body)) /\ 93 (io1 = io) /\ (ok1 = ~(name IN FDOM fns))``, 94 NTAC 5 (ONCE_REWRITE_TAC [R_ev_cases] 95 \\ SIMP_TAC (srw_ss()) [list2sexp_11,MAP_Sym_11,getSym_def,sexp2list_list2sexp,MAP_getSym_MAP_Sym])); 96 97val R_ev_App_Define_CLAUSES = 98 LIST_CONJ [Q.SPEC `[]` R_ev_App_Define, 99 Q.SPEC `[x1]` R_ev_App_Define, 100 Q.SPEC `[x1;x2]` R_ev_App_Define, 101 Q.SPEC `[x1;x2;x3]` R_ev_App_Define, 102 Q.SPEC `[x1;x2;x3;x4]` R_ev_App_Define, 103 Q.SPEC `[x1;x2;x3;x4;x5]` R_ev_App_Define] |> RW [list2sexp_def,MAP] 104 105fun list_dest f tm = let val (x,y) = f tm in list_dest f x @ list_dest f y end 106 handle HOL_ERR _ => [tm]; 107 108fun REWRITE_EQS th = let 109 val tm = fst (dest_imp (concl th)) 110 fun dest_var_eq tm = let val (x,y) = dest_eq tm 111 val _ = not (x = y) orelse fail() 112 val _ = is_var x orelse fail() in (x,y) end 113 val (v,exp) = dest_eq (first (can dest_var_eq) (list_dest dest_conj tm)) 114 in REWRITE_EQS (INST [v|->exp] th) end handle HOL_ERR _ => th 115 116val (MILAWA_CORE_SEXP_thm,MILAWA_INIT_def) = let 117 val tm = concl MILAWA_CORE_SEXP_def 118 val tm = find_term (can (match_term ``Dot (Dot (Sym "NOT") x) y``)) tm 119 val MILAWA_INIT_def = zDefine `MILAWA_INIT = ^tm` 120 in (RW [GSYM MILAWA_INIT_def] MILAWA_CORE_SEXP_def,MILAWA_INIT_def) end 121 122val IN_FDOM_add_def = prove( 123 ``z IN FDOM (add_def k (x,y)) = (z = x) \/ z IN FDOM k``, 124 SIMP_TAC std_ss [add_def_def,FUNION_DEF,IN_UNION,FDOM_FUPDATE, 125 FDOM_FEMPTY,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []); 126 127val (init_fns_def,init_th) = let 128 val _ = print "." 129 val rw = ASSUME ``read_sexps rest = [Dot (Sym "MILAWA-MAIN") (Dot (Dot (Sym "QUOTE") (Dot x (Sym "NIL"))) (Sym "NIL"))]`` 130 val th = RW [rw] (SPEC_ALL MILAWA_CORE_SEXP_thm) 131 val xs = th |> concl |> rand |> listSyntax.dest_list |> fst 132 val _ = print "." 133 val th = foldr (uncurry SPEC) R_aux_exec6 xs |> RW [GSYM MILAWA_CORE_SEXP_thm] 134 val _ = print "." 135 val tms = find_terms (can (match_term ``sexp2term x``)) (concl th) 136 val _ = print "." 137 val th = RW1 (map (fn t => (print "."; EVAL t)) tms) th 138 val _ = print "." 139 val th = RW [R_ev_App_Define_CLAUSES,GSYM CONJ_ASSOC,AND_IMP_INTRO] (SPEC_ALL th) 140 val _ = print "." 141 val tms = find_terms (can (match_term ``sexp2term x``)) (concl th) 142 val _ = print "." 143 val th = RW1 (map (fn t => (print "."; EVAL t)) tms) th 144 val _ = print "." 145 val th = RW [FDOM_FUPDATE,IN_INSERT,EVAL ``sexp2string (Sym "NIL")``,APPEND,GSYM APPEND_ASSOC] (REWRITE_EQS th) 146 val _ = print "." 147 val th = Q.INST [`fns1`|->`FEMPTY`] th 148 val th = SIMP_RULE (srw_ss()) [] (UNDISCH th) 149 val _ = print "." 150 val th = MATCH_MP R_aux_exec_IMP_R_exec th 151 val _ = print "." 152 val th = Q.SPEC `MILAWA_CORE_TEXT ++ rest` (RW [] th) 153 val th = RW [RW [rw] (SPEC_ALL MILAWA_CORE_SEXP_thm)] th 154 val _ = print "." 155 val th = DISCH_ALL th 156 val _ = print "." 157 val x = find_term (can (match_term ``add_def fns1 qqq``)) (concl th) 158 val _ = print ".\n" 159 val init_fns_def = Define `init_fns = ^x` 160 val th = RW1 [GSYM init_fns_def] th 161 val th = SIMP_RULE (srw_ss()) [IN_FDOM_add_def] th 162 in (init_fns_def,th) end 163 164val milawa_init_expanded = let 165 val th = init_th 166 |> RW1 [MILAWA_INIT_def] 167 |> RW [MILAWA_CORE_TEXT_THM,MILAWA_CORE_SEXP_def,CONS_11,CAR_def] 168 |> GSYM 169 val tm = th |> concl |> dest_imp |> fst 170 val lemma = 171 (ONCE_REWRITE_CONV [R_ev_cases] THENC 172 SIMP_CONV (srw_ss()) [] THENC 173 SIMP_CONV std_ss [Once R_ev_cases] THENC 174 SIMP_CONV (srw_ss()) [] THENC 175 SIMP_CONV std_ss [Once R_ev_cases] THENC 176 SIMP_CONV (srw_ss()) [] THENC 177 SIMP_CONV std_ss [Once R_ev_cases] THENC 178 SIMP_CONV (srw_ss()) []) tm 179 in RW [lemma] th end 180 181val _ = save_thm("milawa_init_expanded",milawa_init_expanded); 182 183 184(* extract functions for Milawa's top-level definitions *) 185 186val xs = concl init_fns_def 187 |> find_terms (can (match_term ``add_def x (y:'a # 'b)``)) 188 |> map rand |> (fn tms => listSyntax.mk_list(tms,type_of (hd tms))) 189 190val init_assum_def = Define `init_assum k = fns_assum k ^xs` 191val init_assum_thm = store_thm("init_assum_thm", 192 ``init_assum init_fns``, 193 EVAL_TAC \\ SRW_TAC [] [FUNION_DEF]); 194 195val _ = install_assum_eq init_assum_def 196 197 198val name = "LOOKUP-SAFE" 199val term_tac = SOME 200 (WF_REL_TAC `measure (LSIZE o SND)` 201 \\ FULL_SIMP_TAC std_ss [lisp_extractTheory.isTrue_CLAUSES] 202 \\ FULL_SIMP_TAC std_ss [isDot_thm] \\ REPEAT STRIP_TAC 203 \\ FULL_SIMP_TAC std_ss [LSIZE_def,CDR_def] \\ DECIDE_TAC) 204val lookup_safe_def = pure_extract name term_tac 205 206val name = "DEFINE-SAFE" 207val term_tac = NONE 208val define_safe_def = impure_extract name term_tac 209 210val name = "DEFINE-SAFE-LIST" 211val term_tac = SOME 212 (WF_REL_TAC `measure (LSIZE o FST o SND)` 213 \\ FULL_SIMP_TAC std_ss [lisp_extractTheory.isTrue_CLAUSES] 214 \\ FULL_SIMP_TAC std_ss [isDot_thm] \\ REPEAT STRIP_TAC 215 \\ FULL_SIMP_TAC std_ss [LSIZE_def,CDR_def] \\ DECIDE_TAC) 216val define_safe_list_def = impure_extract name term_tac 217 218val name = "MILAWA-INIT" 219val term_tac = NONE 220val milawa_init_def = impure_extract name term_tac 221 222 223val define_safe_list_side_thm = store_thm("define_safe_list_side_thm", 224 ``!ftbl defs k io ok. define_safe_list_side ftbl defs k io ok = T``, 225 Induct_on `defs` \\ SIMP_TAC std_ss [] 226 \\ ONCE_REWRITE_TAC [fetch "-" "define_safe_list_side_def"] 227 \\ ASM_SIMP_TAC std_ss [LET_DEF,fetch "-" "define_safe_side_def", 228 isTrue_CLAUSES,isDot_def,CDR_def] 229 \\ CONV_TAC (DEPTH_CONV PairRules.PBETA_CONV) \\ SIMP_TAC std_ss []); 230 231val milawa_init_side_thm = store_thm("milawa_init_side_thm", 232 ``!k io ok. milawa_init_side k io ok = T``, 233 SIMP_TAC std_ss [fetch "-" "milawa_init_side_def", 234 define_safe_list_side_thm]); 235 236 237 238val define_safe_thm = prove( 239 ``define_safe ftbl name formals body k io ok = 240 if isTrue (lookup_safe name ftbl) then 241 if lookup_safe name ftbl = 242 LISP_CONS name (LISP_CONS formals (LISP_CONS body (Sym "NIL"))) 243 then (ftbl,k,io,ok) 244 else (Sym "NIL",k,STRCAT 245 (STRCAT io 246 (sexp2string 247 (list2sexp 248 [Sym "ERROR"; 249 LISP_CONS (Sym "REDEFINITION-ERROR") 250 (LISP_CONS (lookup_safe name ftbl) 251 (LISP_CONS 252 (LISP_CONS name 253 (LISP_CONS formals 254 (LISP_CONS body (Sym "NIL")))) 255 (Sym "NIL")))]))) "\n",F) 256 else 257 (LISP_CONS 258 (LISP_CONS name 259 (LISP_CONS formals (LISP_CONS body (Sym "NIL")))) ftbl, 260 add_def k 261 (getSym name,MAP getSym (sexp2list formals),sexp2term body), 262 io,ok /\ getSym name NOTIN FDOM k)``, 263 SIMP_TAC std_ss [Once define_safe_def,LET_DEF,isTrue_CLAUSES] 264 \\ SRW_TAC [] [] \\ METIS_TAC []); 265 266 267val FDOM_init_fns = prove( 268 ``FDOM init_fns = {"MILAWA-MAIN";"MILAWA-INIT";"DEFINE-SAFE";"DEFINE-SAFE-LIST";"LOOKUP-SAFE"}``, 269 SRW_TAC [] [init_fns_def,EXTENSION,FUNION_DEF,add_def_def] \\ METIS_TAC []); 270 271val lookup_safe_lemma1 = RW [isTrue_CLAUSES] lookup_safe_def 272val lookup_safe_lemma2 = lookup_safe_lemma1 |> Q.INST [`x`|->`Sym t`] |> RW [isDot_def] 273val lookup_safe_lemma3 = lookup_safe_lemma1 274 |> Q.INST [`x`|->`Dot (Dot (Sym s) y) z`,`a`|->`Sym t`] 275 |> RW [isDot_def,CAR_def,CDR_def,SExp_11] 276 277val lookup_safe_conv = 278 REPEATC 279 (REWR_CONV lookup_safe_lemma2 280 ORELSEC 281 (REWR_CONV lookup_safe_lemma3 THENC 282 (RATOR_CONV o RATOR_CONV o RAND_CONV) EVAL THENC 283 COND_CONV)) 284 285val define_safe_conv_lemma = SPEC_ALL define_safe_thm |> RW [LISP_CONS_def] 286 287fun define_safe_conv tm = let 288 val str = tm |> rator |> rator |> rator |> rator |> rator |> rand 289 |> rand |> stringSyntax.fromHOLstring 290 val _ = print "define_safe_conv: " 291 val _ = print str 292 val _ = print "\n" 293 val result = 294 (REWR_CONV define_safe_conv_lemma THENC 295 (RATOR_CONV o RATOR_CONV o RAND_CONV o RAND_CONV) lookup_safe_conv THENC 296 (RATOR_CONV o RATOR_CONV o RAND_CONV) EVAL THENC 297 COND_CONV THENC 298 (RAND_CONV o RATOR_CONV o RAND_CONV o RAND_CONV) EVAL) tm 299 in result end 300 301val define_safe_list_conv_lemma = prove( 302 ``define_safe_list ftbl (Dot (Dot name (Dot params (Dot body z))) y) k io T = 303 (\(ftbl',k',io',ok'). define_safe_list ftbl' y k' io' ok') 304 (define_safe ftbl name params body k io T)``, 305 SIMP_TAC std_ss [Once define_safe_list_def] 306 \\ FULL_SIMP_TAC std_ss [isDot_def,CAR_def,LET_DEF,FIRST_def,SECOND_def, 307 THIRD_def,CDR_def,isTrue_CLAUSES] 308 \\ Cases_on `define_safe ftbl name params body k io ok` 309 \\ FULL_SIMP_TAC std_ss [] 310 \\ CONV_TAC (DEPTH_CONV (PairRules.PBETA_CONV)) 311 \\ FULL_SIMP_TAC std_ss []); 312 313val define_safe_list_conv_lemma_nil = 314 define_safe_list_def 315 |> Q.INST [`defs`|->`Sym t`,`ok`|->`ok`] 316 |> SIMP_RULE std_ss [isDot_def,isTrue_CLAUSES] 317 318fun define_safe_list_conv tm = 319 (REWR_CONV define_safe_list_conv_lemma THENC 320 RAND_CONV define_safe_conv THENC 321 PairRules.PBETA_CONV THENC 322 RAND_CONV (REWRITE_CONV [getSym_def,IN_FDOM_add_def,FDOM_init_fns] 323 THENC SIMP_CONV (srw_ss()) [])) tm 324 325 326local 327 val milawa_init_lemma = let 328 val tm = milawa_init_def |> RW [MILAWA_INIT_def] |> SPEC_ALL 329 |> Q.INST [`k`|->`init_fns`,`ok`|->`T`] |> RW [init_fns_def] |> concl |> rand 330 in (REPEATC define_safe_list_conv THENC 331 TRY_CONV (REWR_CONV define_safe_list_conv_lemma_nil)) tm end 332 val dest_tuple = list_dest pairSyntax.dest_pair 333 val tms = milawa_init_lemma |> concl |> rand |> dest_tuple 334in 335 val init_ftbl_def = Define `init_ftbl = ^(el 1 tms)`; 336 val core_funs_def = Define `core_funs = ^(el 2 tms)`; 337 val milawa_init_evaluated = 338 RW1 [GSYM init_ftbl_def,GSYM core_funs_def,GSYM MILAWA_INIT_def] milawa_init_lemma 339 |> RW [GSYM init_fns_def,GSYM milawa_init_def] 340end 341 342val _ = save_thm("milawa_init_evaluated",milawa_init_evaluated); 343 344 345(* construct fns_assum for all core functions *) 346 347val fns_assum_add_def = prove( 348 ``~(n IN FDOM k) /\ fns_assum k xs ==> 349 fns_assum (add_def k (n,ps,body)) ((n,ps,body)::xs)``, 350 FULL_SIMP_TAC (srw_ss()) [fns_assum_def,EVERY_DEF,add_def_def,FUNION_DEF, 351 EVERY_MEM,IN_UNION,FDOM_FUPDATE,pairTheory.FORALL_PROD] \\ REPEAT STRIP_TAC 352 \\ RES_TAC \\ FULL_SIMP_TAC std_ss []); 353 354val (list_of_defs_tm,core_fun_names) = let 355 val tm = core_funs_def |> RW [init_fns_def] |> concl |> rand 356 fun foo tm = 357 if can (match_term ``add_def x (y:'a # 'b)``) tm then 358 rand tm :: foo (rand (rator tm)) else [] 359 val xs = foo tm 360 val core_fun_names = rev (map (stringSyntax.fromHOLstring o rand o rator) xs) 361 |> tl |> tl |> tl |> tl |> tl 362 val list_of_defs_tm = listSyntax.mk_list(xs,type_of (hd xs)) 363 in (list_of_defs_tm,core_fun_names) end 364 365val core_assum_def = Define `core_assum k = fns_assum k ^list_of_defs_tm`; 366val core_assum_thm = store_thm("core_assum_thm", 367 ``core_assum core_funs``, 368 REWRITE_TAC [init_fns_def,core_funs_def,core_assum_def] 369 \\ REPEAT 370 (MATCH_MP_TAC fns_assum_add_def 371 \\ STRIP_TAC THEN1 372 (REWRITE_TAC [IN_FDOM_add_def] 373 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 374 \\ REWRITE_TAC [] \\ SIMP_TAC (srw_ss()) [])) 375 \\ SIMP_TAC std_ss [fns_assum_def,EVERY_DEF]); 376 377 378val _ = export_theory(); 379 380