1open HolKernel boolLib bossLib Parse; val _ = new_theory "milawa_core"; 2 3open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory; 4open optionTheory arithmeticTheory relationTheory; 5 6open lisp_sexpTheory lisp_parseTheory; 7 8infix \\ 9val op \\ = op THEN; 10val RW = REWRITE_RULE; 11val RW1 = ONCE_REWRITE_RULE; 12 13 14val _ = max_print_depth := 10; 15 16(* read all lines from file *) 17 18fun text_from_file filename = let 19 val t = TextIO.openIn(filename) 20 fun all_lines () = 21 case TextIO.inputLine(t) of NONE => [] 22 | SOME x => x::all_lines () 23 val text = all_lines () 24 val _ = TextIO.closeIn(t) 25 val output = foldr (fn (x,y) => x ^ y) "" text 26 val _ = print ("\n" ^ filename ^ " contains " ^ int_to_string (length text) ^ 27 " lines and " ^ int_to_string (size output) ^ " characters.\n\n") 28 in output end; 29 30val milawa_core_tm = stringSyntax.fromMLstring (text_from_file "core.lisp"); 31 32local 33 val app_cons = APPEND |> SPEC_ALL |> CONJUNCT2 34 val app_nil = APPEND |> SPEC_ALL |> CONJUNCT1 35 fun append_conv tm = 36 ((REWR_CONV app_cons THENC RAND_CONV append_conv) 37 ORELSEC (REWR_CONV app_nil)) tm 38 handle HOL_ERR _ => ALL_CONV tm 39in 40 val milawa_core_append_thm = append_conv ``^milawa_core_tm ++ rest`` 41 val milawa_core_tm = milawa_core_append_thm |> concl |> rand 42end 43 44 45(* move the following to lisp_parseTheory *) 46 47val LENGTH_sexp_lex_parse = sexp_lex_parse_ind 48 |> Q.ISPEC `\(cs,s,r,mem). LENGTH (SND (sexp_lex_parse (cs,s,r,mem))) <= LENGTH cs` 49 |> SIMP_RULE std_ss []; 50 51val LENGTH_SND_read_while = prove( 52 ``!t x. LENGTH (SND (read_while P t x)) <= LENGTH t``, 53 Induct \\ SIMP_TAC std_ss [read_while_def] \\ SRW_TAC [] [] 54 \\ Q.PAT_ASSUM `!x.bb` (MP_TAC o Q.SPEC `STRCAT x (STRING h "")`) 55 \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 56 57val read_while_IMP_LENGTH_LESS_EQ = prove( 58 ``(read_while P t x = (x1,x2)) ==> (LENGTH x2 <= LENGTH t)``, 59 REPEAT STRIP_TAC 60 \\ MP_TAC (SPEC_ALL LENGTH_SND_read_while) \\ FULL_SIMP_TAC std_ss []); 61 62val PULL_FORALL_IMP = METIS_PROVE [] ``(Q ==> !x. P x) = !x. Q ==> P x`` 63val IMP_IMP = METIS_PROVE [] ``b1 /\ (b2 ==> b3) ==> ((b1 ==> b2) ==> b3)`` 64 65val str2sym_aux_LESS_EQ = prove( 66 ``!xs b y ys. (str2sym_aux xs b = (y,ys)) ==> LENGTH ys <= LENGTH xs``, 67 Induct \\ Cases_on `b` \\ SIMP_TAC std_ss [str2sym_aux_def,LET_DEF] 68 \\ REPEAT STRIP_TAC 69 \\ `?z zs. str2sym_aux xs F = (z,zs)` by METIS_TAC [pairTheory.PAIR] 70 \\ `?z zs. str2sym_aux xs T = (z,zs)` by METIS_TAC [pairTheory.PAIR] 71 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ RES_TAC 72 \\ TRY (Q.PAT_X_ASSUM `zs = ys` (ASSUME_TAC)) \\ FULL_SIMP_TAC std_ss [] 73 \\ TRY (Q.PAT_X_ASSUM `(if b1 then x1 else y1) = z1` MP_TAC) 74 \\ SRW_TAC [] [] \\ DECIDE_TAC); 75 76val str2sym_LENGTH = prove( 77 ``!xs y ys. (str2sym (x::xs) = (y,ys)) ==> LENGTH ys <= LENGTH xs``, 78 SIMP_TAC std_ss [str2sym_def,LET_DEF] \\ REPEAT STRIP_TAC 79 \\ `?y1 y2. read_while identifier_char xs "" = (y1,y2)` by METIS_TAC [pairTheory.PAIR] 80 \\ `?z1 z2. str2sym_aux xs F = (z1,z2)` by METIS_TAC [pairTheory.PAIR] 81 \\ FULL_SIMP_TAC std_ss [] 82 \\ IMP_RES_TAC read_while_IMP_LENGTH_LESS_EQ 83 \\ IMP_RES_TAC str2sym_aux_LESS_EQ 84 \\ Cases_on `x = #"|"` \\ FULL_SIMP_TAC std_ss [] 85 \\ REPEAT (POP_ASSUM MP_TAC) 86 \\ FULL_SIMP_TAC std_ss []); 87 88val next_token_LESS_EQ = prove( 89 ``!cs cs2. (next_token cs = (t,cs2)) ==> LENGTH cs2 <= LENGTH cs``, 90 STRIP_TAC \\ completeInduct_on `LENGTH cs` \\ NTAC 2 STRIP_TAC 91 \\ FULL_SIMP_TAC std_ss [PULL_FORALL_IMP] 92 \\ Cases_on `cs` \\ SIMP_TAC std_ss [next_token_def,LET_DEF] 93 \\ SRW_TAC [] [] THEN1 94 (`STRLEN t' < STRLEN (STRING h t')` by (EVAL_TAC \\ DECIDE_TAC) 95 \\ RES_TAC \\ DECIDE_TAC) 96 THEN1 97 (POP_ASSUM MP_TAC 98 \\ `?z zs. read_while number_char t' "" = (z,zs)` by METIS_TAC [pairTheory.PAIR] 99 \\ FULL_SIMP_TAC std_ss [] \\ SRW_TAC [] [LENGTH] 100 \\ FULL_SIMP_TAC std_ss [LENGTH,TL] 101 \\ Cases_on `zs` \\ FULL_SIMP_TAC std_ss [LENGTH,TL] 102 \\ IMP_RES_TAC read_while_IMP_LENGTH_LESS_EQ 103 \\ FULL_SIMP_TAC std_ss [LENGTH,TL] \\ DECIDE_TAC) 104 THEN1 105 (POP_ASSUM MP_TAC 106 \\ `?z zs. read_while number_char t' "" = (z,zs)` by METIS_TAC [pairTheory.PAIR] 107 \\ FULL_SIMP_TAC std_ss [] \\ SRW_TAC [] [LENGTH] 108 \\ IMP_RES_TAC read_while_IMP_LENGTH_LESS_EQ \\ DECIDE_TAC) 109 THEN1 110 (`?z zs. read_while (\x. x <> #"\n") t' "" = (z,zs)` by METIS_TAC [pairTheory.PAIR] 111 \\ FULL_SIMP_TAC std_ss [] 112 \\ `STRLEN zs < STRLEN (STRING #";" t')` by 113 (IMP_RES_TAC read_while_IMP_LENGTH_LESS_EQ 114 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC) 115 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC) 116 THEN1 117 (`?z1 z2. str2sym (STRING h t') = (z1,z2)` by METIS_TAC [pairTheory.PAIR] 118 \\ IMP_RES_TAC str2sym_LENGTH \\ FULL_SIMP_TAC std_ss [] 119 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)); 120 121val LENGTH_SND_sexp_lex_parse = prove( 122 ``!cs s r mem. LENGTH (SND (sexp_lex_parse (cs,s,r,mem))) <= LENGTH cs``, 123 MATCH_MP_TAC LENGTH_sexp_lex_parse \\ REPEAT STRIP_TAC THEN1 124 (ONCE_REWRITE_TAC [sexp_lex_parse_def] \\ SRW_TAC [] [] \\ SRW_TAC [] [] 125 \\ Q.PAT_X_ASSUM `next_token xx = yy` (MP_TAC) 126 \\ TRY (Cases_on `t`) \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 127 \\ FULL_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] 128 \\ IMP_RES_TAC next_token_LESS_EQ \\ IMP_RES_TAC LESS_EQ_TRANS) 129 \\ Cases_on `s` \\ ONCE_REWRITE_TAC [sexp_lex_parse_def] 130 \\ FULL_SIMP_TAC (srw_ss()) [LET_DEF] \\ SRW_TAC [] [] 131 \\ FULL_SIMP_TAC std_ss []); 132 133val sexp_lex_parse_LESS_EQ = prove( 134 ``!cs s r mem. 135 (sexp_lex_parse (cs,s,r,mem) = (x1,x2)) ==> 136 LENGTH x2 <= LENGTH cs``, 137 REPEAT STRIP_TAC \\ MP_TAC (SPEC_ALL LENGTH_SND_sexp_lex_parse) 138 \\ FULL_SIMP_TAC std_ss []); 139 140val is_eof_F_IMP = prove( 141 ``!str str1. 142 ((F,str1) = is_eof str) ==> 143 ?x xs. (str1 = x::xs) /\ ~(space_char x) /\ ~(x = #";") /\ 144 LENGTH xs < LENGTH str``, 145 STRIP_TAC \\ completeInduct_on `LENGTH str` \\ STRIP_TAC 146 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [PULL_FORALL_IMP] 147 \\ POP_ASSUM MP_TAC \\ Cases_on `str` THEN1 EVAL_TAC 148 \\ SIMP_TAC std_ss [is_eof_def] \\ SRW_TAC [] [] THEN1 149 (Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`t`,`str1`]) 150 \\ FULL_SIMP_TAC std_ss [] \\ MATCH_MP_TAC IMP_IMP 151 \\ STRIP_TAC THEN1 (EVAL_TAC \\ DECIDE_TAC) 152 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`x`,`xs`] 153 \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 154 \\ FULL_SIMP_TAC std_ss [LET_DEF] 155 \\ Q.ABBREV_TAC `str2 = SND (read_while (\x. x <> #"\n") t "")` 156 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`str2`,`str1`]) 157 \\ `LENGTH str2 <= LENGTH t` by 158 (Q.UNABBREV_TAC `str2` \\ FULL_SIMP_TAC std_ss [LENGTH_SND_read_while]) 159 \\ FULL_SIMP_TAC std_ss [] \\ MATCH_MP_TAC IMP_IMP 160 \\ STRIP_TAC THEN1 (EVAL_TAC \\ DECIDE_TAC) 161 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [] \\ DECIDE_TAC); 162 163val next_token_PROGRESS = prove( 164 ``~space_char x /\ x <> #";" ==> 165 LENGTH (SND (next_token (STRING x xs))) <= LENGTH xs``, 166 SIMP_TAC std_ss [next_token_def] \\ REPEAT STRIP_TAC 167 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [] 168 \\ TRY (Cases_on `cs`) \\ FULL_SIMP_TAC (srw_ss()) [LENGTH] 169 \\ SRW_TAC [] [] \\ IMP_RES_TAC read_while_IMP_LENGTH_LESS_EQ 170 \\ IMP_RES_TAC str2sym_LENGTH 171 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC); 172 173val sexp_parse_stream_PROGRESS = store_thm("sexp_parse_stream_PROGRESS", 174 ``((F,str1) = is_eof str) /\ ((s,str2) = sexp_parse_stream str1) ==> 175 LENGTH str2 < LENGTH str``, 176 REPEAT STRIP_TAC \\ IMP_RES_TAC is_eof_F_IMP 177 \\ FULL_SIMP_TAC std_ss [sexp_parse_stream_def] 178 \\ Q.PAT_X_ASSUM `(s,str2) = bb` (MP_TAC o GSYM) 179 \\ SIMP_TAC std_ss [Once sexp_lex_parse_def] 180 \\ `?y1 y2. next_token (STRING x xs) = (y1,y2)` by METIS_TAC [pairTheory.PAIR] 181 \\ FULL_SIMP_TAC std_ss [LET_DEF] 182 \\ IMP_RES_TAC next_token_PROGRESS 183 \\ POP_ASSUM (MP_TAC o Q.SPEC `xs`) 184 \\ FULL_SIMP_TAC std_ss [] \\ SRW_TAC [] [] 185 \\ IMP_RES_TAC sexp_lex_parse_LESS_EQ \\ DECIDE_TAC); 186 187val read_sexps_def = tDefine "read_sexps" ` 188 read_sexps str = 189 let (yes,str) = is_eof str in 190 if yes then [] else 191 let (s,str) = sexp_parse_stream str in 192 s::read_sexps str` 193 (WF_REL_TAC `measure LENGTH` \\ METIS_TAC [sexp_parse_stream_PROGRESS]) 194 |> SPEC_ALL; 195 196val evals = map EVAL 197 [``next_token (STRING #")" cs)``, 198 ``next_token (STRING #"'" cs)``, 199 ``next_token (STRING #"." cs)``, 200 ``next_token (STRING #"(" cs)``, 201 ``next_token (STRING #" " cs)``, 202 ``next_token (STRING #"0" cs)``, 203 ``next_token (STRING #"1" cs)``, 204 ``next_token (STRING #"2" cs)``, 205 ``next_token (STRING #"3" cs)``, 206 ``next_token (STRING #"4" cs)``, 207 ``next_token (STRING #"5" cs)``, 208 ``next_token (STRING #"6" cs)``, 209 ``next_token (STRING #"7" cs)``, 210 ``next_token (STRING #"8" cs)``, 211 ``next_token (STRING #"9" cs)``, 212 ``next_token (STRING #";" cs)``, 213 ``next_token (STRING #"|" cs)``, 214 ``str2sym (STRING #"|" cs)``] |> LIST_CONJ 215 216val sexp_lex_parse_SIMP1 = prove( 217 ``(sexp_lex_parse (#")"::cs,s,L_READ,mem) = sexp_lex_parse (cs,s,L_COLLECT (Sym "NIL"),mem)) /\ 218 (sexp_lex_parse (#"'"::cs,s,L_READ,mem) = sexp_lex_parse (cs,L_QUOTE::s,L_READ,mem)) /\ 219 (sexp_lex_parse (#"."::cs,s,L_READ,mem) = sexp_lex_parse (cs,L_DOT::s,L_READ,mem))``, 220 REPEAT STRIP_TAC \\ SIMP_TAC (srw_ss()) [Once sexp_lex_parse_def,LET_DEF,evals]); 221 222val sexp_lex_parse_SIMP2 = prove( 223 ``(sexp_lex_parse (#" "::cs,s,L_READ,mem) = sexp_lex_parse (cs,s,L_READ,mem)) /\ 224 (sexp_lex_parse (#"\n"::cs,s,L_READ,mem) = sexp_lex_parse (cs,s,L_READ,mem)) /\ 225 (sexp_lex_parse (#"\t"::cs,s,L_READ,mem) = sexp_lex_parse (cs,s,L_READ,mem)) /\ 226 (sexp_lex_parse (#"("::cs,s,L_READ,mem) = sexp_lex_parse (cs,L_STOP::s,L_READ,mem))``, 227 EVAL_TAC); 228 229val DROP_WHILE_NOT_NL_def = Define ` 230 (DROP_WHILE_NOT_NL [] = []) /\ 231 (DROP_WHILE_NOT_NL (x::xs) = if x = #"\n" then #"\n"::xs else DROP_WHILE_NOT_NL xs)` 232 233val DROP_WHILE_NOT_NL_INTRO = prove( 234 ``!t s. SND (read_while (\x. x <> #"\n") t s) = 235 DROP_WHILE_NOT_NL t``, 236 Induct \\ ASM_SIMP_TAC std_ss [read_while_def,DROP_WHILE_NOT_NL_def] 237 \\ REPEAT STRIP_TAC \\ Cases_on `h = #"\n"` \\ ASM_SIMP_TAC std_ss []); 238 239val sexp_lex_parse_COMMENT = prove( 240 ``(sexp_lex_parse (#";"::cs,s,L_READ,mem) = 241 sexp_lex_parse (DROP_WHILE_NOT_NL cs,s,L_READ,mem))``, 242 REPEAT STRIP_TAC \\ SIMP_TAC (srw_ss()) [Once sexp_lex_parse_def,LET_DEF,evals, 243 GSYM (Q.SPECL [`t`,`""`] DROP_WHILE_NOT_NL_INTRO),GSYM ORD_11] 244 \\ EVAL_TAC); 245 246val sexp_lex_parse_SIMP_NUM = prove( 247 ``(sexp_lex_parse (#"0"::cs,s,L_READ,mem) = 248 let (str,cs) = read_while number_char cs "" in 249 sexp_lex_parse (cs,s,L_RETURN (Val (str2num str)),mem)) /\ 250 (sexp_lex_parse (#"1"::cs,s,L_READ,mem) = 251 let (str,cs) = read_while number_char cs "" in 252 sexp_lex_parse (cs,s,L_RETURN (Val (10 ** STRLEN str + str2num str)),mem)) /\ 253 (sexp_lex_parse (#"2"::cs,s,L_READ,mem) = 254 let (str,cs) = read_while number_char cs "" in 255 sexp_lex_parse (cs,s,L_RETURN (Val (2 * 10 ** STRLEN str + str2num str)),mem)) /\ 256 (sexp_lex_parse (#"3"::cs,s,L_READ,mem) = 257 let (str,cs) = read_while number_char cs "" in 258 sexp_lex_parse (cs,s,L_RETURN (Val (3 * 10 ** STRLEN str + str2num str)),mem)) /\ 259 (sexp_lex_parse (#"4"::cs,s,L_READ,mem) = 260 let (str,cs) = read_while number_char cs "" in 261 sexp_lex_parse (cs,s,L_RETURN (Val (4 * 10 ** STRLEN str + str2num str)),mem)) /\ 262 (sexp_lex_parse (#"5"::cs,s,L_READ,mem) = 263 let (str,cs) = read_while number_char cs "" in 264 sexp_lex_parse (cs,s,L_RETURN (Val (5 * 10 ** STRLEN str + str2num str)),mem)) /\ 265 (sexp_lex_parse (#"6"::cs,s,L_READ,mem) = 266 let (str,cs) = read_while number_char cs "" in 267 sexp_lex_parse (cs,s,L_RETURN (Val (6 * 10 ** STRLEN str + str2num str)),mem)) /\ 268 (sexp_lex_parse (#"7"::cs,s,L_READ,mem) = 269 let (str,cs) = read_while number_char cs "" in 270 sexp_lex_parse (cs,s,L_RETURN (Val (7 * 10 ** STRLEN str + str2num str)),mem)) /\ 271 (sexp_lex_parse (#"8"::cs,s,L_READ,mem) = 272 let (str,cs) = read_while number_char cs "" in 273 sexp_lex_parse (cs,s,L_RETURN (Val (8 * 10 ** STRLEN str + str2num str)),mem)) /\ 274 (sexp_lex_parse (#"9"::cs,s,L_READ,mem) = 275 let (str,cs) = read_while number_char cs "" in 276 sexp_lex_parse (cs,s,L_RETURN (Val (9 * 10 ** STRLEN str + str2num str)),mem))``, 277 REPEAT STRIP_TAC 278 \\ SIMP_TAC (srw_ss()) [Once sexp_lex_parse_def,LET_DEF,evals] 279 \\ Cases_on `read_while number_char cs ""` 280 \\ FULL_SIMP_TAC (srw_ss()) []); 281 282val sexp_lex_parse_BAR = prove( 283 ``(sexp_lex_parse (#"|"::cs,s,L_READ,mem) = 284 let (str,cs) = str2sym (STRING #"|" cs) in 285 sexp_lex_parse (cs,s,L_RETURN (Sym str),mem))``, 286 REPEAT STRIP_TAC 287 \\ SIMP_TAC (srw_ss()) [Once sexp_lex_parse_def,LET_DEF,evals] 288 \\ Cases_on `str2sym_aux cs F` 289 \\ FULL_SIMP_TAC (srw_ss()) []); 290 291fun auto_prove (goal,tac) = let 292 val (rest,validation) = tac ([], goal) 293 in if length rest = 0 then validation [] 294 else failwith("auto_prove failed") end 295 296val sexp_lex_parse_chars = let 297 fun is_true tm = (tm = T) 298 fun is_identifier_char c = 299 ``identifier_char ^c`` |> EVAL |> concl |> rand |> is_true 300 fun all_ichars_below 0 xs = xs 301 | all_ichars_below n xs = let 302 val c = stringSyntax.fromMLchar (chr n) 303 in all_ichars_below (n-1) (if is_identifier_char c then c::xs else xs) end 304 val cs = all_ichars_below 255 [] 305 fun thm_for_char c = let 306 val sym_evals = CONJ (EVAL ``next_token (STRING ^c cs)``) 307 (EVAL ``str2sym (STRING ^c cs)``) 308 in auto_prove( 309 ``(sexp_lex_parse (^c::cs,s,L_READ,mem) = 310 let (str,cs) = str2sym (STRING ^c cs) in 311 sexp_lex_parse (cs,s,L_RETURN (Sym str),mem))``, 312 REPEAT STRIP_TAC 313 \\ SIMP_TAC (srw_ss()) [Once sexp_lex_parse_def,LET_DEF,sym_evals] 314 \\ Cases_on `read_while identifier_char cs ""` 315 \\ FULL_SIMP_TAC (srw_ss()) []) end handle HOL_ERR _ => TRUTH 316 in filter (not o is_true o concl) (map thm_for_char cs) end; 317 318val sexp_lex_parse_SIMP_RETURN = prove( 319 ``(sexp_lex_parse (cs,L_STOP::s,L_RETURN x,mem) = 320 sexp_lex_parse (cs,L_CONS x::L_STOP::s,L_READ,mem)) /\ 321 (sexp_lex_parse (cs,L_CONS y::s,L_RETURN x,mem) = 322 sexp_lex_parse (cs,L_CONS x::L_CONS y::s,L_READ,mem)) /\ 323 (sexp_lex_parse (cs,L_DOT::s,L_RETURN x,mem) = 324 sexp_lex_parse (cs,L_CONS x::L_DOT::s,L_READ,mem)) /\ 325 (sexp_lex_parse (cs,L_QUOTE::s,L_RETURN x,mem) = 326 sexp_lex_parse (cs,s,L_RETURN (Dot (Sym "QUOTE") (Dot x (Sym "NIL"))),mem)) /\ 327 (sexp_lex_parse (cs,L_STORE n::s,L_RETURN x,mem) = 328 sexp_lex_parse (cs,s,L_RETURN x,(n =+ x) mem)) /\ 329 (sexp_lex_parse (cs,[],L_RETURN x,mem) = (x,cs))``, 330 REPEAT STRIP_TAC \\ SIMP_TAC (srw_ss()) [Once sexp_lex_parse_def] 331 \\ SIMP_TAC (srw_ss()) [LET_DEF,READ_L_STORE_def] \\ EVAL_TAC); 332 333val sexp_lex_parse_SIMP_COLLECT = prove( 334 ``(sexp_lex_parse (cs,L_STOP::s,L_COLLECT x,mem) = 335 sexp_lex_parse (cs,s,L_RETURN x,mem)) /\ 336 (sexp_lex_parse (cs,L_CONS y::s,L_COLLECT x,mem) = 337 sexp_lex_parse (cs,s,L_COLLECT (Dot y x),mem)) /\ 338 (sexp_lex_parse (cs,L_DOT::s,L_COLLECT x,mem) = 339 sexp_lex_parse (cs,s,L_COLLECT (CAR x),mem)) /\ 340 (sexp_lex_parse (cs,[],L_COLLECT x,mem) = (Sym "NIL",cs))``, 341 REPEAT STRIP_TAC \\ SIMP_TAC (srw_ss()) [Once sexp_lex_parse_def,LET_DEF, 342 READ_L_CONS_def] \\ EVAL_TAC); 343 344val sexp_lex_parse_SIMP = LIST_CONJ 345 (sexp_lex_parse_BAR :: 346 sexp_lex_parse_COMMENT :: 347 sexp_lex_parse_chars @ 348 CONJUNCTS sexp_lex_parse_SIMP_NUM @ 349 CONJUNCTS sexp_lex_parse_SIMP1 @ 350 CONJUNCTS sexp_lex_parse_SIMP2 @ 351 CONJUNCTS sexp_lex_parse_SIMP_RETURN @ 352 CONJUNCTS sexp_lex_parse_SIMP_COLLECT); 353 354local 355 fun eval_term_ss tm_name tm = simpLib.conv_ss 356 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) }; 357 val pattern = ``sexp_lex_parse (str,s,task,mem)`` 358 val str_tm = ``str:string`` 359 val rws = CONJ (EVAL ``str2sym ""``) (EVAL ``str2num ""``) 360 val my_ss = std_ss ++ eval_term_ss "str2sym" ``str2sym (STRING c cs)`` 361 ++ eval_term_ss "str2num" ``str2num (STRING c cs)`` 362 ++ eval_term_ss "read_while_comment" ``DROP_WHILE_NOT_NL (x::xs)`` 363 ++ eval_term_ss "read_while_number" ``read_while number_char (STRING c cs) ""`` 364 fun dest_string tm = let 365 val (x,y) = listSyntax.dest_cons tm 366 in x :: dest_string y end handle HOL_ERR _ => [tm] 367 fun take_until p [] = [] 368 | take_until p (x::xs) = if p x then [] else x :: take_until p xs 369in 370 fun sexp_lex_parse_conv tm = let 371 val _ = print "sexp_lex_parse_conv: " 372 val s = fst (match_term pattern tm) 373 val input_tm = subst s str_tm 374 val input = dest_string input_tm 375 val input_length = length input - 1 376 val fst_line = input 377 |> take_until (fn c => (c = ``#"\n"``) orelse (type_of c = ``:string``)) 378 |> map stringSyntax.fromHOLchar |> implode 379 val _ = print (fst_line ^ " ... \n") 380 val sp_chr_tm = ``#" "`` 381 fun split_after n k [] acc = [implode (rev acc)] 382 | split_after n k [x] acc = [implode (rev acc)] 383 | split_after n k (x::xs) acc = 384 if n < k orelse not (x = sp_chr_tm) 385 then split_after (n+1) k xs ((stringSyntax.fromHOLchar x)::acc) 386 else implode (rev ((stringSyntax.fromHOLchar x)::acc)) 387 :: split_after 0 k xs [] 388 val segments = split_after 0 80 input [] 389 val th = REFL (subst [input_tm|->str_tm] tm) 390 fun find_fringe_terms p tm = 391 if p tm then [tm] else 392 if is_abs tm then find_fringe_terms p (snd (dest_abs tm)) else 393 if is_comb tm then find_fringe_terms p (rator tm) @ find_fringe_terms p (rand tm) else 394 [] 395 val c = SIMP_CONV my_ss [sexp_lex_parse_SIMP,LET_DEF,APPEND,LENGTH,rws] 396 fun c2 tm = let 397 val xs = find_fringe_terms (fn tm => type_of tm = ``:SExp``) tm 398 val ys = map (fn x => (x,genvar(type_of x))) xs 399 val tm2 = subst (map (fn (x,y) => x |-> y) ys) tm 400 val tm3 = c tm2 401 in INST (map (fn (x,y) => y |-> x) ys) tm3 end 402 fun mk_string [] = str_tm 403 | mk_string (x::xs) = listSyntax.mk_cons(stringSyntax.fromMLchar x, mk_string xs) 404 fun process_segments [] th = th 405 | process_segments (s::ss) th = let 406 val _ = print (int_to_string (length ss) ^ " ") 407 val th = CONV_RULE (RAND_CONV c2) (INST [str_tm|->mk_string (explode s)] th) 408 in if pairSyntax.is_pair (rand (concl th)) then let 409 val l = input_length - foldl (fn (x,y) => size x + y) 0 ss 410 fun ntimes 0 f x = x | ntimes n f x = ntimes (n-1) f (f x) 411 in INST [str_tm|->ntimes l rand input_tm] th end 412 else process_segments ss th end 413 val th = INST [str_tm|->last input] (process_segments segments th) 414 val _ = print "\n" 415 in th end; 416end 417 418val is_eof_aux_def = Define ` 419 (is_eof_aux "" = is_eof "") /\ 420 (is_eof_aux (x::xs) = if x = #"\n" then is_eof xs else is_eof_aux xs)` 421 422val is_eof_comment = prove( 423 ``!xs. is_eof (#";"::xs) = is_eof_aux xs``, 424 SIMP_TAC std_ss [is_eof_def,LET_DEF,EVAL ``space_char #";"``] 425 \\ Q.SPEC_TAC (`""`,`ys`) \\ Induct_on `xs` 426 \\ FULL_SIMP_TAC std_ss [read_while_def,is_eof_aux_def] 427 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [is_eof_def,EVAL ``space_char #"\n"``]); 428 429val is_eof_lemmas = let 430 fun all_below f 0 = [] 431 | all_below f n = f (n-1) :: all_below f (n-1) 432 val is_eof_aux_nil = EVAL ``is_eof_aux ""`` 433 fun is_eof_aux n = 434 EVAL (``is_eof_aux (CHR n::cs)`` |> subst [``n:num``|->numSyntax.term_of_int n]) 435 val is_eof_aux_lemmas = (is_eof_aux_nil :: all_below is_eof_aux 256) 436 val is_eof_nil = EVAL ``is_eof ""`` 437 fun is_eof n = 438 if n = ord #";" then SPEC_ALL is_eof_comment else 439 EVAL (``is_eof (CHR n::cs)`` |> subst [``n:num``|->numSyntax.term_of_int n]) 440 val is_eof_lemmas = is_eof_nil :: all_below is_eof 256 441 in is_eof_aux_lemmas @ is_eof_lemmas end; 442 443fun TRY_EACHC [] = NO_CONV 444 | TRY_EACHC (c::cs) = c ORELSEC TRY_EACHC cs 445 446val is_eof_conv = REPEATC (TRY_EACHC (map REWR_CONV is_eof_lemmas)) 447 448local 449 val pattern = ``read_sexps str`` 450 val str_tm = ``str:string`` 451 val lemma = SIMP_RULE std_ss [LET_DEF,sexp_parse_stream_def] read_sexps_def 452in 453 fun read_sexps_conv tm = let 454 val s = fst (match_term pattern tm) 455 val th = INST s lemma |> CONV_RULE ((RAND_CONV o RAND_CONV) is_eof_conv) 456 val pair = (th |> concl |> rand |> rand |> pairSyntax.is_pair) handle HOL_ERR _ => false 457 in if not pair then CONV_RULE (RAND_CONV (REWR_CONV (GSYM lemma))) th else let 458 val th = CONV_RULE (RAND_CONV PairRules.PBETA_CONV THENC RAND_CONV COND_CONV) th 459 val t = th |> concl |> rand 460 in if not (can (find_term (fn tm => tm = ``read_sexps``)) t) then th else let 461 val th = CONV_RULE (RAND_CONV (RAND_CONV sexp_lex_parse_conv 462 THENC PairRules.PBETA_CONV)) th 463 in CONV_RULE ((RAND_CONV o RAND_CONV) read_sexps_conv) th end end end 464end 465 466val read_sexps_milawa_core_thm = 467 time (REWRITE_RULE [CAR_def] o read_sexps_conv) ``read_sexps ^milawa_core_tm``; 468 469val input_tm = milawa_core_append_thm |> concl |> rator |> rand 470val output_tm = read_sexps_milawa_core_thm |> concl |> rand 471 472val MILAWA_CORE_TEXT_def = Define `MILAWA_CORE_TEXT = ^(input_tm |> rator |> rand)`; 473val MILAWA_CORE_SEXP_def = Define `MILAWA_CORE_SEXP rest = ^output_tm`; 474 475val lemma = milawa_core_append_thm 476 |> CONV_RULE ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 477 (REWR_CONV (GSYM MILAWA_CORE_TEXT_def))) 478 479val MILAWA_CORE_TEXT_THM = save_thm("MILAWA_CORE_TEXT_THM", 480 read_sexps_milawa_core_thm 481 |> CONV_RULE (RAND_CONV (REWR_CONV (GSYM MILAWA_CORE_SEXP_def))) 482 |> CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV) (REWR_CONV (GSYM lemma)))); 483 484val _ = max_print_depth := 0; 485val _ = export_theory(); 486