1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_parse"; 2val _ = ParseExtras.temp_loose_equality() 3 4open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 5open combinTheory finite_mapTheory stringTheory relationTheory; 6 7open lisp_sexpTheory; 8 9(* file structure: 10 1. we first define how to print s-expressions, then 11 2. we define a function which parses printed s-expressions. 12*) 13 14infix \\ 15val op \\ = op THEN; 16val RW = REWRITE_RULE; 17val RW1 = ONCE_REWRITE_RULE; 18 19val TOKEN_OPEN = ``(Val 0, Val 1)`` 20val TOKEN_DOT = ``(Val 1, Val 1)`` 21val TOKEN_CLOSE = ``(Val 2, Val 1)`` 22val TOKEN_QUOTE = ``(Val 3, Val 1)`` 23val TOKEN_SAVE = ``(Val index, Val 2)`` 24val TOKEN_LOAD = ``(Val index, Val 3)`` 25val NO_TOKEN = ``(Sym "NIL", Sym "NIL")`` 26 27val SExp_print_induct = store_thm("SExp_print_induct", 28 ``!P. (!x. (if isQuote x then P (CAR (CDR x)) else 29 if isDot x then P (CAR x) /\ P (CDR x) else T) ==> P x) ==> 30 !x. P x``, 31 REPEAT STRIP_TAC \\ completeInduct_on `LSIZE x` 32 \\ REPEAT STRIP_TAC 33 \\ Cases_on `isQuote x` 34 \\ Q.PAT_X_ASSUM `!x. bbb ==> P x` MATCH_MP_TAC THEN1 35 (ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [isQuote_thm,CAR_def,CDR_def] 36 \\ FULL_SIMP_TAC std_ss [LSIZE_def,ADD1,GSYM ADD_ASSOC]) 37 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 38 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def,CDR_def,LSIZE_def] 39 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def,CDR_def,LSIZE_def] 40 \\ METIS_TAC [DECIDE ``n < SUC (m + n)``,ADD_COMM]); 41 42 43(* Part 1 - section 1: print s-expressions *) 44 45val LIST_STRCAT_def = Define ` 46 (LIST_STRCAT [] = "") /\ 47 (LIST_STRCAT (x::xs) = STRCAT x (LIST_STRCAT xs))`; 48 49val dec2str_def = Define `dec2str n = STRING (CHR (n + 48)) ""`; 50 51val num2str_def = tDefine "num2str" ` 52 num2str n = 53 if n DIV 10 = 0 then dec2str (n MOD 10) else 54 STRCAT (num2str (n DIV 10)) (dec2str (n MOD 10))` 55 (Q.EXISTS_TAC `measure I` 56 \\ SIMP_TAC std_ss [prim_recTheory.WF_measure] 57 \\ SIMP_TAC std_ss [prim_recTheory.measure_thm] 58 \\ STRIP_TAC 59 \\ STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DA (DECIDE ``0 < 10:num``))) 60 \\ ASM_SIMP_TAC std_ss [DIV_MULT] 61 \\ DECIDE_TAC); 62 63val number_char_def = Define ` 64 number_char c = 48 <= ORD c /\ ORD c < 58`; 65 66val space_char_def = Define ` 67 space_char c = ORD c <= 32`; 68 69val identifier_char_def = Define ` 70 identifier_char c = 42 <= ORD c /\ ~(ORD c = 46) /\ ~(ORD c = 59) /\ ~(ORD c = 124)`; 71 72val identifier_string_def = Define ` 73 identifier_string s = 74 ~(s = "") /\ EVERY identifier_char s /\ ~number_char (HD s)`; 75 76val sym2str_aux_def = Define ` 77 (sym2str_aux [] = []) /\ 78 (sym2str_aux (x::xs) = 79 if (ORD x = 0) then (#"\\")::(#"0")::sym2str_aux xs else 80 if MEM x [#"|";#"\\"] 81 then #"\\"::x::sym2str_aux xs else x::sym2str_aux xs)`; 82 83val is_lower_case_def = Define ` 84 is_lower_case c = #"a" <= c /\ c <= #"z"`; 85 86val upper_case_def = Define ` 87 upper_case c = if is_lower_case c then CHR (ORD c - 32) else c`; 88 89val sym2str_def = Define ` 90 sym2str s = 91 if identifier_string s /\ EVERY (\c. ~(is_lower_case c)) s 92 then s else "|" ++ sym2str_aux s ++ "|"`; 93 94val sexp2string_aux_def = tDefine "sexp2string_aux" ` 95 (sexp2string_aux (Val n, b) = num2str n) /\ 96 (sexp2string_aux (Sym s, b) = sym2str s) /\ 97 (sexp2string_aux (Dot x y, b) = 98 if isQuote (Dot x y) then LIST_STRCAT ["'"; sexp2string_aux (CAR y,T)] else 99 let (a,e) = if b then ("(",")") else ("","") in 100 if y = Sym "NIL" then LIST_STRCAT [a; sexp2string_aux (x,T); e] else 101 if isDot y /\ ~(isQuote y) 102 then LIST_STRCAT [a; sexp2string_aux (x,T); " "; sexp2string_aux (y,F); e] 103 else LIST_STRCAT [a; sexp2string_aux (x,T); " . "; sexp2string_aux (y,F); e])` 104 (WF_REL_TAC `measure (LSIZE o FST)` \\ REWRITE_TAC [LSIZE_def,ADD1] 105 \\ REPEAT STRIP_TAC 106 \\ FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,LSIZE_def] 107 \\ DECIDE_TAC); 108 109val sexp2string_def = Define `sexp2string x = sexp2string_aux (x, T)`; 110 111 112(* Part 1 - section 2: printing s-expressions with abbreviations *) 113 114val isAtom_def = Define ` 115 isAtom abbrevs s = ~isDot s \/ isQuote s \/ s IN FDOM abbrevs`; 116 117val sexp2abbrev_aux_def = tDefine "sexp2abbrev_aux" ` 118 sexp2abbrev_aux s b abbrevs ps = 119 let index = abbrevs ' s in 120 let prefix = (if s IN FDOM abbrevs then "#" ++ (num2str index) ++ "=" else "") in 121 if s IN FDOM abbrevs /\ s IN ps then 122 ("#" ++ (num2str index) ++ "#", ps) 123 else 124 if isVal s then (prefix ++ num2str (getVal s), if s IN FDOM abbrevs then s INSERT ps else ps) else 125 if isSym s then (prefix ++ sym2str (getSym s), if s IN FDOM abbrevs then s INSERT ps else ps) else 126 if isQuote s then 127 let (str2,ps2) = sexp2abbrev_aux (CAR (CDR s)) T abbrevs ps in 128 (prefix ++ "'" ++ str2, 129 if s IN FDOM abbrevs then s INSERT ps2 else ps2) 130 else 131 let b = b \/ ~(prefix = "") in 132 let (s1,s2) = (if b then ("(",")") else ("","")) in 133 let (str1,ps1) = sexp2abbrev_aux (CAR s) T abbrevs ps in 134 let (str2,ps2) = sexp2abbrev_aux (CDR s) F abbrevs ps1 in 135 ((prefix ++ s1 ++ str1 ++ 136 (if CDR s = Sym "NIL" then "" else 137 (if isAtom abbrevs (CDR s) then " . " else " ") ++ 138 str2) ++ s2), 139 if CDR s = Sym "NIL" 140 then if s IN FDOM abbrevs then s INSERT ps1 else ps1 141 else if s IN FDOM abbrevs then s INSERT ps2 else ps2)` 142 (WF_REL_TAC `measure (\(s,b,abbrevs,ps). LSIZE s)` \\ SRW_TAC [] [] 143 \\ `isDot s` by (Cases_on `s` \\ FULL_SIMP_TAC std_ss [isVal_def,isDot_def,isSym_def]) 144 \\ FULL_SIMP_TAC std_ss [isQuote_thm,isDot_thm,CDR_def,CAR_def,LSIZE_def] 145 \\ FULL_SIMP_TAC std_ss [SExp_11,LSIZE_def,CAR_def,CDR_def] 146 \\ DECIDE_TAC); 147 148val sexp_abbrev_fmap_def = Define ` 149 (sexp_abbrev_fmap [] n = FEMPTY) /\ 150 (sexp_abbrev_fmap (x::xs) n = sexp_abbrev_fmap xs (n+1) |+ (x:SExp,n))`; 151 152val sexp2abbrev_def = Define ` 153 sexp2abbrev s abbrevs = FST (sexp2abbrev_aux s T (sexp_abbrev_fmap abbrevs 0) {})`; 154 155val sexp2abbrev_aux_EQ_sexp2string_aux = prove( 156 ``!s b. sexp2abbrev_aux s b FEMPTY {} = (sexp2string_aux (s,b),{})``, 157 HO_MATCH_MP_TAC SExp_print_induct \\ REPEAT STRIP_TAC 158 \\ ONCE_REWRITE_TAC [sexp2abbrev_aux_def] 159 \\ SIMP_TAC std_ss [NOT_IN_EMPTY,FDOM_FEMPTY,LET_DEF] 160 \\ Cases_on `isVal s` \\ ASM_SIMP_TAC std_ss [APPEND] 161 THEN1 (FULL_SIMP_TAC std_ss [isVal_thm,getVal_def,sexp2string_aux_def]) 162 \\ Cases_on `isSym s` \\ ASM_SIMP_TAC std_ss [APPEND] 163 THEN1 (FULL_SIMP_TAC std_ss [isSym_thm,getSym_def,sexp2string_aux_def]) 164 \\ Cases_on `isQuote s` \\ ASM_SIMP_TAC std_ss [APPEND] THEN1 165 (FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [isQuote_thm] 166 \\ SIMP_TAC std_ss [sexp2string_aux_def,isQuote_def,CAR_def,CDR_def, 167 isDot_def,LIST_STRCAT_def,APPEND_NIL,APPEND]) 168 \\ `isDot s` by (Cases_on `s` \\ FULL_SIMP_TAC std_ss [isDot_def,isVal_def,isSym_def]) 169 \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [isDot_thm] 170 \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def,CAR_def,CDR_def,LIST_STRCAT_def] 171 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [LET_DEF,isAtom_def,FDOM_FEMPTY,NOT_IN_EMPTY] 172 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss []); 173 174val sexp2abbrev_NIL = prove( 175 ``!s. sexp2abbrev s [] = sexp2string s``, 176 SIMP_TAC std_ss [sexp2abbrev_def,sexp2string_def,sexp_abbrev_fmap_def, 177 sexp2abbrev_aux_EQ_sexp2string_aux]); 178 179(* 180 181val list2sexp_def = Define ` 182 (list2sexp [] = Sym "NIL") /\ 183 (list2sexp (x::xs) = Dot x (list2sexp xs))`; 184 185val A1 = Define `A1 = list2sexp [Sym "a"; Val 4]`; 186val A2 = Define `A2 = list2sexp [Sym "b"; Sym "c"]`; 187 188EVAL ``sexp2abbrev (list2sexp [A1;Dot A1 A2;list2sexp [Sym "QUOTE"; A2]]) [A1;A2]`` 189 190*) 191 192val sexp2abbrevt_aux_def = tDefine "sexp2abbrevt_aux" ` 193 sexp2abbrevt_aux s b abbrevs ps = 194 let index = abbrevs ' s in 195 let prefix = (if s IN FDOM abbrevs then [^TOKEN_SAVE] else []) in 196 if s IN FDOM abbrevs /\ s IN ps then 197 ([(^TOKEN_LOAD)], ps) 198 else 199 if ~(isDot s) then (prefix ++ [(s,Val 0)], if s IN FDOM abbrevs then s INSERT ps else ps) else 200 if isQuote s then 201 let (str2,ps2) = sexp2abbrevt_aux (CAR (CDR s)) T abbrevs ps in 202 (prefix ++ [^TOKEN_QUOTE] ++ str2, 203 if s IN FDOM abbrevs then s INSERT ps2 else ps2) 204 else 205 let b = b \/ ~(prefix = []) in 206 let (s1,s2) = (if b then ([^TOKEN_OPEN],[^TOKEN_CLOSE]) else ([],[])) in 207 let (str1,ps1) = sexp2abbrevt_aux (CAR s) T abbrevs ps in 208 let (str2,ps2) = sexp2abbrevt_aux (CDR s) F abbrevs ps1 in 209 ((prefix ++ s1 ++ str1 ++ 210 (if CDR s = Sym "NIL" then [] else 211 (if isAtom abbrevs (CDR s) then [^TOKEN_DOT] else []) ++ 212 str2) ++ s2), 213 if CDR s = Sym "NIL" 214 then if s IN FDOM abbrevs then s INSERT ps1 else ps1 215 else if s IN FDOM abbrevs then s INSERT ps2 else ps2)` 216 (WF_REL_TAC `measure (\(s,b,abbrevs,ps). LSIZE s)` \\ SRW_TAC [] [] 217 \\ `isDot s` by (Cases_on `s` \\ FULL_SIMP_TAC std_ss [isVal_def,isDot_def,isSym_def]) 218 \\ FULL_SIMP_TAC std_ss [isQuote_thm,isDot_thm,CDR_def,CAR_def,LSIZE_def] 219 \\ FULL_SIMP_TAC std_ss [SExp_11,LSIZE_def,CAR_def,CDR_def] 220 \\ DECIDE_TAC) 221 222 223 224(* Part 2 - section 1: reading tokens from a string, i.e. lexing or scanning *) 225 226val read_while_def = Define ` 227 (read_while P "" s = (s,"")) /\ 228 (read_while P (STRING c cs) s = 229 if P c then read_while P cs (STRCAT s (STRING c "")) 230 else (s,STRING c cs))`; 231 232val read_while_thm = prove( 233 ``!cs s cs' s'. 234 (read_while P cs s = (s',cs')) ==> LENGTH cs' <= LENGTH cs + LENGTH s``, 235 Induct \\ SIMP_TAC std_ss [read_while_def] 236 \\ REPEAT STRIP_TAC 237 \\ Cases_on `P h` \\ FULL_SIMP_TAC std_ss [LENGTH] 238 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND] 239 \\ REPEAT (Q.PAT_X_ASSUM `STRING c cs = cs'` (ASSUME_TAC o GSYM)) 240 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND] \\ DECIDE_TAC); 241 242val str2num_def = Define ` 243 (str2num "" = 0) /\ 244 (str2num (STRING c s) = (ORD c - 48) * 10 ** (LENGTH s) + str2num s)`; 245 246val str2num_dec2str = prove( 247 ``!n. n < 10 ==> (str2num (dec2str n) = n) /\ ~(dec2str n = "") /\ 248 EVERY number_char (dec2str n)``, 249 SRW_TAC [] [dec2str_def,str2num_def,LENGTH,ORD_CHR,number_char_def] 250 \\ `n + 48 < 256` by DECIDE_TAC 251 \\ IMP_RES_TAC ORD_CHR 252 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 253 254val str2num_STRCAT = prove( 255 ``!s c. str2num (STRCAT s (STRING c "")) = str2num s * 10 + str2num (STRING c "")``, 256 Induct \\ ASM_SIMP_TAC std_ss [str2num_def,STRCAT_def,LENGTH_APPEND, 257 LENGTH,EXP_ADD,RIGHT_ADD_DISTRIB,AC MULT_ASSOC MULT_COMM, AC ADD_ASSOC ADD_COMM]); 258 259val dec2str_lemma = prove( 260 ``?c. dec2str r = STRING c ""``, 261 SRW_TAC [] [dec2str_def,str2num_def,LENGTH]); 262 263val str2num_num2str = store_thm("str2num_num2str", 264 ``!n. (str2num (num2str n) = n) /\ ~((num2str n) = "") /\ 265 EVERY number_char (num2str n)``, 266 completeInduct_on `n` \\ Cases_on `n < 10` THEN1 267 (IMP_RES_TAC LESS_DIV_EQ_ZERO \\ ONCE_REWRITE_TAC [num2str_def] 268 \\ ASM_SIMP_TAC std_ss [str2num_dec2str]) 269 \\ STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DA (DECIDE ``0 < 10:num``))) 270 \\ ONCE_REWRITE_TAC [num2str_def] 271 \\ ASM_SIMP_TAC std_ss [DIV_MULT] 272 \\ Cases_on `q = 0` THEN1 (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 273 \\ ASM_SIMP_TAC std_ss [MOD_TIMES,STRCAT_EQ_EMPTY,EVERY_APPEND] 274 \\ ASM_SIMP_TAC std_ss [str2num_dec2str,str2num_STRCAT] 275 \\ `q < n` by DECIDE_TAC \\ RES_TAC 276 \\ STRIP_ASSUME_TAC dec2str_lemma 277 \\ ASM_SIMP_TAC std_ss [str2num_STRCAT] 278 \\ METIS_TAC [str2num_dec2str]); 279 280val str2sym_aux_def = Define ` 281 (str2sym_aux [] b = ("",[])) /\ 282 (str2sym_aux (c::cs) T = 283 let (x1,x2) = str2sym_aux cs F in ((if c = #"0" then CHR 0 else c)::x1,x2)) /\ 284 (str2sym_aux (c::cs) F = 285 if c = #"\\" then str2sym_aux cs T else 286 if c = #"|" then ("",cs) else 287 let (x1,x2) = str2sym_aux cs F in (c::x1,x2))`; 288 289val str2sym_def = Define ` 290 (str2sym "" = ("","")) /\ 291 (str2sym (c::cs) = 292 if c = #"|" then 293 (let (ident,cs) = str2sym_aux cs F 294 in 295 ((ident,cs))) 296 else 297 (let (ident,cs1) = read_while identifier_char cs "" in 298 let ident = MAP upper_case (c :: ident) 299 in 300 ((ident,cs1))))`; 301 302val str2sym_aux_sym2str_aux = prove( 303 ``!s. str2sym_aux (sym2str_aux s ++ "|" ++ ts) F = (s,ts)``, 304 Induct \\ SRW_TAC [] [str2sym_aux_def,sym2str_aux_def,MEM] 305 \\ FULL_SIMP_TAC std_ss [] 306 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [ORD_CHR]); 307 308val next_token_def = tDefine "next_token" ` 309 (next_token "" = (^NO_TOKEN,"")) /\ 310 (next_token (c::cs) = 311 if space_char c then next_token cs else 312 if c = #"(" then (^TOKEN_OPEN,cs) else 313 if c = #"." then (^TOKEN_DOT,cs) else 314 if c = #")" then (^TOKEN_CLOSE,cs) else 315 if c = #"'" then (^TOKEN_QUOTE,cs) else 316 if c = #"#" then 317 (let (index_str,cs) = read_while number_char cs "" in 318 let index = str2num index_str in 319 if cs = "" then (^NO_TOKEN,"") else 320 if HD cs = #"#" then (^TOKEN_LOAD,TL cs) else 321 if HD cs = #"=" then (^TOKEN_SAVE,TL cs) else (^NO_TOKEN,TL cs)) else 322 if number_char c then 323 (let (index_str,cs) = read_while number_char cs "" in 324 let index = str2num (c::index_str) in 325 ((Val index, Val 0),cs)) else 326 if c = #";" then 327 (let cs = SND (read_while (\x. ~(x = #"\n")) cs "") in 328 next_token cs) 329 else let (ident,cs) = str2sym (c::cs) in 330 ((Sym ident, Val 0),cs))` 331 (WF_REL_TAC `measure LENGTH` \\ SIMP_TAC std_ss [LENGTH] \\ REPEAT STRIP_TAC 332 \\ Cases_on `read_while (\x. x <> #"\n") cs ""` \\ IMP_RES_TAC read_while_thm 333 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC); 334 335val is_eof_def = tDefine "is_eof" ` 336 (is_eof "" = (T,"")) /\ 337 (is_eof (c::cs) = 338 if space_char c then is_eof cs else 339 if c = #";" then 340 (let cs = SND (read_while (\x. ~(x = #"\n")) cs "") in 341 is_eof cs) 342 else (F,c::cs))` 343 (WF_REL_TAC `measure LENGTH` \\ SIMP_TAC std_ss [LENGTH] \\ REPEAT STRIP_TAC 344 \\ Cases_on `read_while (\x. x <> #"\n") cs ""` \\ IMP_RES_TAC read_while_thm 345 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC); 346 347val str2sym_aux_LENGTH = prove( 348 ``!s b t x. (str2sym_aux s b = (x,t)) ==> LENGTH t <= LENGTH s``, 349 Induct \\ SRW_TAC [] [str2sym_aux_def] \\ SRW_TAC [] [] 350 \\ Cases_on `b`\\ FULL_SIMP_TAC std_ss [str2sym_aux_def] 351 \\ POP_ASSUM MP_TAC 352 \\ `?a1 a2. str2sym_aux s F = (a1,a2)` by METIS_TAC [PAIR] 353 \\ `?b1 b2. str2sym_aux s T = (b1,b2)` by METIS_TAC [PAIR] 354 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 355 \\ REPEAT (Q.PAT_X_ASSUM `bbb = t` (ASSUME_TAC o GSYM)) 356 THEN1 (RES_TAC \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 357 \\ POP_ASSUM MP_TAC \\ SRW_TAC [] [] 358 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 359 360val str2sym_LENGTH = prove( 361 ``!s t x. ~(s = []) /\ (str2sym s = (x,t)) ==> LENGTH t < LENGTH s``, 362 SIMP_TAC std_ss [str2sym_def,LET_DEF] \\ NTAC 3 STRIP_TAC \\ Cases_on `s` 363 \\ SIMP_TAC std_ss [str2sym_def,LET_DEF] 364 \\ `?a1 a2. str2sym_aux t' F = (a1,a2)` by METIS_TAC [PAIR] 365 \\ `?y1 y2. read_while identifier_char t' "" = (y1,y2)` by METIS_TAC [PAIR] 366 \\ IMP_RES_TAC read_while_thm 367 \\ ASM_SIMP_TAC std_ss [] \\ IMP_RES_TAC str2sym_aux_LENGTH 368 \\ FULL_SIMP_TAC std_ss [LENGTH,HD,LENGTH_NIL,NOT_CONS_NIL,TL] 369 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [TL] \\ DECIDE_TAC); 370 371val next_token_LENGTH = prove( 372 ``!s x t. (next_token s = (x,t)) ==> LENGTH t < LENGTH s \/ (s = "")``, 373 HO_MATCH_MP_TAC (fetch "-" "next_token_ind") \\ REPEAT STRIP_TAC 374 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM MP_TAC 375 \\ ONCE_REWRITE_TAC [next_token_def] 376 \\ ASM_SIMP_TAC std_ss [] 377 \\ Cases_on `space_char c` \\ ASM_SIMP_TAC std_ss [] THEN1 378 (REPEAT STRIP_TAC \\ RES_TAC \\ ASM_SIMP_TAC std_ss [LENGTH] 379 THEN1 (DISJ1_TAC \\ DECIDE_TAC) 380 \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [next_token_def] 381 \\ Q.PAT_X_ASSUM `"" = t` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 382 \\ EVAL_TAC) 383 \\ `?x1 x2. read_while number_char s "" = (x1,x2)` by METIS_TAC [PAIR] 384 \\ `?y1 y2. read_while (\x. x <> #"\n") s "" = (y1,y2)` by METIS_TAC [PAIR] 385 \\ `?z1 z2. str2sym (c::s) = (z1,z2)` by METIS_TAC [PAIR] 386 \\ IMP_RES_TAC str2sym_LENGTH 387 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ IMP_RES_TAC read_while_thm 388 \\ SRW_TAC [] [LENGTH] \\ ASM_SIMP_TAC std_ss [LENGTH] 389 \\ REPEAT (Cases_on `x2`) 390 \\ FULL_SIMP_TAC std_ss [LENGTH,TL,NOT_CONS_NIL,HD,ADD1] 391 \\ REPEAT DECIDE_TAC 392 \\ RES_TAC \\ REPEAT DECIDE_TAC 393 \\ FULL_SIMP_TAC std_ss [EVAL ``next_token ""``] 394 \\ REPEAT (Q.PAT_X_ASSUM `"" = t` (fn th => FULL_SIMP_TAC std_ss [GSYM th])) 395 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ REPEAT DECIDE_TAC); 396 397val sexp_lex_def = tDefine "sexp_lex" ` 398 sexp_lex s = 399 if SND (FST (next_token s)) = Sym "NIL" then ([],"") else 400 let (ts,s2) = sexp_lex (SND (next_token s)) in 401 (FST (next_token s)::ts,s2)` 402 (WF_REL_TAC `measure (LENGTH)` \\ REPEAT STRIP_TAC 403 \\ Cases_on `next_token s` \\ FULL_SIMP_TAC std_ss [] 404 \\ Cases_on `q` \\ FULL_SIMP_TAC std_ss [] 405 \\ IMP_RES_TAC next_token_LENGTH \\ FULL_SIMP_TAC std_ss [] 406 \\ FULL_SIMP_TAC std_ss [next_token_def] \\ METIS_TAC []); 407 408val sexp_lex_thm = prove( 409 ``sexp_lex s = 410 let (t,s) = next_token s in 411 if SND t = Sym "NIL" then ([],[]) else 412 let (ts,s) = sexp_lex s in 413 (t::ts,s)``, 414 SIMP_TAC std_ss [Once sexp_lex_def] 415 \\ SIMP_TAC std_ss [LET_DEF] 416 \\ Cases_on `next_token s` \\ ASM_SIMP_TAC std_ss []); 417 418val sexp2abbrev_aux_SND = prove( 419 ``!exp b abbrevs ps xs1 xs2 ps1 ps2. 420 ((xs1,ps1) = sexp2abbrev_aux exp b abbrevs ps) ==> 421 ((xs2,ps2) = sexp2abbrevt_aux exp b abbrevs ps) ==> 422 (ps1 = ps2)``, 423 HO_MATCH_MP_TAC SExp_print_induct \\ NTAC 9 STRIP_TAC 424 \\ ONCE_REWRITE_TAC [sexp2abbrevt_aux_def,sexp2abbrev_aux_def] 425 \\ Q.ABBREV_TAC `index = abbrevs ' exp` 426 \\ SIMP_TAC std_ss [LET_DEF] 427 \\ Q.ABBREV_TAC `t_prefix = if exp IN FDOM abbrevs then [(Val index,Val 2)] else []` 428 \\ Q.ABBREV_TAC `s_prefix = if exp IN FDOM abbrevs then STRCAT (STRCAT "#" (num2str index)) "=" else ""` 429 \\ `?t_str1 t_ps1. sexp2abbrevt_aux (CAR exp) T abbrevs ps = (t_str1,t_ps1)` by METIS_TAC [PAIR] 430 \\ `?t_str2 t_ps2. sexp2abbrevt_aux (CDR exp) F abbrevs t_ps1 = (t_str2,t_ps2)` by METIS_TAC [PAIR] 431 \\ `?t_str3 t_ps3. sexp2abbrevt_aux (CAR (CDR exp)) T abbrevs ps = (t_str3,t_ps3)` by METIS_TAC [PAIR] 432 \\ `?s_str1 s_ps1. sexp2abbrev_aux (CAR exp) T abbrevs ps = (s_str1,s_ps1)` by METIS_TAC [PAIR] 433 \\ `?s_str2 s_ps2. sexp2abbrev_aux (CDR exp) F abbrevs s_ps1 = (s_str2,s_ps2)` by METIS_TAC [PAIR] 434 \\ `?s_str3 s_ps3. sexp2abbrev_aux (CAR (CDR exp)) T abbrevs ps = (s_str3,s_ps3)` by METIS_TAC [PAIR] 435 \\ ASM_SIMP_TAC std_ss [] 436 \\ Cases_on `Abbrev (exp IN FDOM abbrevs /\ exp IN ps)` 437 THEN1 (POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [markerTheory.Abbrev_def]) 438 \\ IMP_RES_TAC (METIS_PROVE [] ``~Abbrev b ==> ~b``) 439 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 440 \\ Cases_on `isVal exp` 441 THEN1 (FULL_SIMP_TAC std_ss [isVal_thm,isDot_def,isVal_def,SExp_11]) 442 \\ Cases_on `isSym exp` 443 THEN1 (FULL_SIMP_TAC std_ss [isSym_thm,isDot_def,isSym_def,SExp_11]) 444 \\ `isDot exp` by (Cases_on `exp` \\ FULL_SIMP_TAC std_ss [isVal_def,isSym_def,isDot_def]) 445 \\ ASM_SIMP_TAC std_ss [] 446 \\ Cases_on `isQuote exp` THEN1 (FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 447 \\ ASM_SIMP_TAC std_ss [] 448 \\ `(t_prefix = []) = (s_prefix = [])` by 449 (FULL_SIMP_TAC std_ss [APPEND] \\ METIS_TAC [NOT_CONS_NIL]) 450 \\ ASM_SIMP_TAC std_ss [] 451 \\ Cases_on `b \/ s_prefix <> ""` \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []); 452 453val read_while_eval = (GEN_ALL o RW [APPEND_NIL,APPEND] o Q.SPECL [`xs`,`[]`] o prove)( 454 ``!xs zs. EVERY P xs /\ ~P y ==> (read_while P (xs ++ y::ys) zs = (zs ++ xs,y::ys))``, 455 Induct \\ ASM_SIMP_TAC std_ss [EVERY_DEF,APPEND,read_while_def,APPEND_NIL] 456 \\ SIMP_TAC std_ss [APPEND_NIL,GSYM APPEND_ASSOC,APPEND]); 457 458val read_while_entire = (GEN_ALL o RW [APPEND_NIL,APPEND] o Q.SPECL [`xs`,`[]`] o prove)( 459 ``!xs zs. EVERY P xs ==> (read_while P xs zs = (zs ++ xs,""))``, 460 Induct \\ ASM_SIMP_TAC std_ss [EVERY_DEF,APPEND,read_while_def,APPEND_NIL] 461 \\ SIMP_TAC std_ss [APPEND_NIL,GSYM APPEND_ASSOC,APPEND]); 462 463val read_while_lemma = prove( 464 ``(read_while number_char (num2str index ++ #"#"::xs) "" = (num2str index,#"#"::xs)) /\ 465 (read_while number_char (num2str index ++ #"="::xs) "" = (num2str index,#"="::xs))``, 466 REPEAT STRIP_TAC \\ MATCH_MP_TAC read_while_eval 467 \\ ASM_SIMP_TAC std_ss [str2num_num2str] \\ EVAL_TAC); 468 469val next_token_lemma = prove( 470 ``(s <> "" ==> MEM (HD s) " )") ==> 471 (next_token (STRCAT (num2str a) s) = ((Val a,Val 0), s)) /\ 472 (next_token (STRCAT (sym2str t) s) = ((Sym t,Val 0), s))``, 473 REPEAT STRIP_TAC THEN1 474 (Cases_on `num2str a` THEN1 METIS_TAC [str2num_num2str] 475 \\ ASM_SIMP_TAC std_ss [APPEND,next_token_def] 476 \\ `EVERY number_char (STRING h t)` by METIS_TAC [str2num_num2str] 477 \\ FULL_SIMP_TAC std_ss [EVERY_DEF] 478 \\ `~space_char h` by 479 (FULL_SIMP_TAC std_ss [number_char_def,space_char_def] \\ DECIDE_TAC) 480 \\ `~MEM h "(.)'#"` by 481 (FULL_SIMP_TAC std_ss [MEM] \\ REPEAT STRIP_TAC 482 \\ FULL_SIMP_TAC (srw_ss()) [number_char_def]) 483 \\ FULL_SIMP_TAC std_ss [MEM] 484 \\ `read_while number_char (STRCAT t s) "" = (t,s)` by 485 (Cases_on `s` \\ FULL_SIMP_TAC std_ss [APPEND_NIL,read_while_entire] 486 \\ MATCH_MP_TAC read_while_eval \\ FULL_SIMP_TAC std_ss [HD,NOT_CONS_NIL] 487 \\ EVAL_TAC) 488 \\ ASM_SIMP_TAC std_ss [LET_DEF] 489 \\ METIS_TAC [str2num_num2str]) 490 \\ SIMP_TAC std_ss [sym2str_def] 491 \\ Cases_on `identifier_string t /\ EVERY (\c. ~is_lower_case c) t` 492 \\ ASM_SIMP_TAC std_ss [] THEN1 493 (FULL_SIMP_TAC std_ss [identifier_string_def] 494 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [APPEND,EVERY_DEF] 495 \\ FULL_SIMP_TAC std_ss [next_token_def,HD] 496 \\ FULL_SIMP_TAC std_ss [identifier_char_def,MEM,str2sym_def,HD,NOT_CONS_NIL,TL] 497 \\ `read_while identifier_char (STRCAT t' s) "" = (t',s)` by 498 (Cases_on `s` \\ FULL_SIMP_TAC std_ss [APPEND_NIL,read_while_entire] 499 \\ MATCH_MP_TAC read_while_eval \\ FULL_SIMP_TAC std_ss [HD,NOT_CONS_NIL] 500 \\ EVAL_TAC) 501 \\ ASM_SIMP_TAC std_ss [LET_DEF] 502 \\ `~(space_char h)` by (FULL_SIMP_TAC std_ss [space_char_def] \\ DECIDE_TAC) 503 \\ Cases_on `h = #"("` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 504 \\ Cases_on `h = #")"` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 505 \\ Cases_on `h = #"'"` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 506 \\ Cases_on `h = #"#"` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 507 \\ Cases_on `h = #"."` THEN1 (FULL_SIMP_TAC std_ss [EVAL ``ORD #"."``]) 508 \\ Cases_on `h = #"|"` THEN1 (FULL_SIMP_TAC std_ss [EVAL ``ORD #"|"``]) 509 \\ Cases_on `h = #";"` THEN1 (FULL_SIMP_TAC std_ss [EVAL ``ORD #";"``]) 510 \\ ASM_SIMP_TAC std_ss [] 511 \\ AP_TERM_TAC 512 \\ `EVERY (\c. ~is_lower_case c) (h::t')` by ASM_SIMP_TAC std_ss [EVERY_DEF] 513 \\ POP_ASSUM MP_TAC \\ Q.SPEC_TAC (`h::t'`,`xs`) 514 \\ Induct \\ ASM_SIMP_TAC std_ss [MAP,EVERY_DEF,upper_case_def]) 515 \\ SIMP_TAC (srw_ss()) [APPEND,next_token_def,EVAL ``space_char #"|"``, 516 EVAL ``number_char #"|"``,str2sym_def,LET_DEF] 517 \\ SIMP_TAC std_ss [str2sym_aux_sym2str_aux,LET_DEF]); 518 519val sexp_lex_SPACE = prove( 520 ``!xs. sexp_lex (#" "::xs) = sexp_lex xs``, 521 ONCE_REWRITE_TAC [sexp_lex_thm] 522 \\ SIMP_TAC std_ss [next_token_def,EVAL ``space_char #" "``]); 523 524fun FORCE_PBETA_CONV tm = let 525 val (tm1,tm2) = dest_comb tm 526 val vs = fst (pairSyntax.dest_pabs tm1) 527 fun expand_pair_conv tm = ISPEC tm (GSYM pairTheory.PAIR) 528 fun get_conv vs = let 529 val (x,y) = dest_pair vs 530 in expand_pair_conv THENC (RAND_CONV (get_conv y)) end 531 handle e => ALL_CONV 532 in (RAND_CONV (get_conv vs) THENC PairRules.PBETA_CONV) tm end; 533 534val sexp2abbrev_aux_FST = prove( 535 ``!exp s b abbrevs ps xs1 xs2 ps1 ps2. 536 (~(s = []) ==> MEM (HD s) " )") ==> 537 ((xs1,ps1) = sexp2abbrev_aux exp b abbrevs ps) ==> 538 ((xs2,ps2) = sexp2abbrevt_aux exp b abbrevs ps) ==> 539 (FST (sexp_lex (xs1 ++ s)) = xs2 ++ FST (sexp_lex s))``, 540 HO_MATCH_MP_TAC SExp_print_induct \\ NTAC 10 STRIP_TAC 541 \\ ONCE_REWRITE_TAC [sexp2abbrevt_aux_def,sexp2abbrev_aux_def] 542 \\ Q.ABBREV_TAC `index = abbrevs ' exp` 543 \\ SIMP_TAC std_ss [LET_DEF] 544 \\ Q.ABBREV_TAC `t_prefix = if exp IN FDOM abbrevs then [(Val index,Val 2)] else []` 545 \\ Q.ABBREV_TAC `s_prefix = if exp IN FDOM abbrevs then STRCAT (STRCAT "#" (num2str index)) "=" else ""` 546 \\ `?t_str1 t_ps1. sexp2abbrevt_aux (CAR exp) T abbrevs ps = (t_str1,t_ps1)` by METIS_TAC [PAIR] 547 \\ `?t_str2 t_ps2. sexp2abbrevt_aux (CDR exp) F abbrevs t_ps1 = (t_str2,t_ps2)` by METIS_TAC [PAIR] 548 \\ `?t_str3 t_ps3. sexp2abbrevt_aux (CAR (CDR exp)) T abbrevs ps = (t_str3,t_ps3)` by METIS_TAC [PAIR] 549 \\ `?s_str1 s_ps1. sexp2abbrev_aux (CAR exp) T abbrevs ps = (s_str1,s_ps1)` by METIS_TAC [PAIR] 550 \\ `?s_str2 s_ps2. sexp2abbrev_aux (CDR exp) F abbrevs s_ps1 = (s_str2,s_ps2)` by METIS_TAC [PAIR] 551 \\ `?s_str3 s_ps3. sexp2abbrev_aux (CAR (CDR exp)) T abbrevs ps = (s_str3,s_ps3)` by METIS_TAC [PAIR] 552 \\ ASM_SIMP_TAC std_ss [] 553 \\ Cases_on `Abbrev (exp IN FDOM abbrevs /\ exp IN ps)` 554 THEN1 (POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [markerTheory.Abbrev_def] 555 \\ REPEAT STRIP_TAC 556 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 557 \\ SIMP_TAC (srw_ss()) [APPEND,next_token_def,EVAL ``space_char #"#"``] 558 \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND,read_while_lemma] 559 \\ SIMP_TAC std_ss [LET_DEF,NOT_CONS_NIL,TL,HD,SExp_distinct] 560 \\ Cases_on `sexp_lex s` \\ ASM_SIMP_TAC std_ss [str2num_num2str]) 561 \\ IMP_RES_TAC (METIS_PROVE [] ``~Abbrev b ==> ~b``) 562 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 563 \\ `(t_prefix = []) = (s_prefix = [])` by 564 (FULL_SIMP_TAC std_ss [APPEND] \\ METIS_TAC [NOT_CONS_NIL]) 565 \\ ASM_SIMP_TAC std_ss [] 566 \\ `!ss ts. 567 (FST (sexp_lex (STRCAT s_prefix (STRCAT ss s))) = 568 t_prefix ++ (ts ++ FST (sexp_lex s))) = 569 (FST (sexp_lex (STRCAT ss s)) = ts ++ FST (sexp_lex s))` by 570 (Q.UNABBREV_TAC `t_prefix` \\ Q.UNABBREV_TAC `s_prefix` 571 \\ REVERSE (Cases_on `exp IN FDOM abbrevs`) \\ ASM_SIMP_TAC std_ss [] 572 THEN1 (ASM_SIMP_TAC std_ss [APPEND]) 573 \\ SIMP_TAC std_ss [Once sexp_lex_thm] \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC] 574 \\ SIMP_TAC (srw_ss()) [APPEND,next_token_def,EVAL ``space_char #"#"``] 575 \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC] 576 \\ SIMP_TAC std_ss [APPEND,read_while_lemma,LET_DEF,NOT_CONS_NIL,TL,HD] 577 \\ SIMP_TAC std_ss [str2num_num2str,EVAL ``#"=" = #"#"``,SExp_distinct] 578 \\ REPEAT STRIP_TAC 579 \\ Cases_on `sexp_lex (STRCAT ss s)` \\ ASM_SIMP_TAC std_ss [CONS_11]) 580 \\ Cases_on `isVal exp` 581 THEN1 (FULL_SIMP_TAC std_ss [isVal_thm,isDot_def,isVal_def,SExp_11] 582 \\ ASM_SIMP_TAC std_ss [getVal_def,GSYM APPEND_ASSOC] 583 \\ REPEAT STRIP_TAC 584 \\ SIMP_TAC std_ss [Once sexp_lex_thm] \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC] 585 \\ ASM_SIMP_TAC (srw_ss()) [APPEND,next_token_lemma] 586 \\ ASM_SIMP_TAC std_ss [LET_DEF,SExp_distinct] 587 \\ Cases_on `sexp_lex s` \\ ASM_SIMP_TAC std_ss []) 588 \\ Cases_on `isSym exp` 589 THEN1 (FULL_SIMP_TAC std_ss [isSym_thm,isDot_def,isSym_def,SExp_11] 590 \\ ASM_SIMP_TAC std_ss [getSym_def,GSYM APPEND_ASSOC] 591 \\ REPEAT STRIP_TAC 592 \\ SIMP_TAC std_ss [Once sexp_lex_thm] \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC] 593 \\ ASM_SIMP_TAC (srw_ss()) [APPEND,next_token_lemma] 594 \\ ASM_SIMP_TAC std_ss [LET_DEF,SExp_distinct] 595 \\ Cases_on `sexp_lex s` \\ ASM_SIMP_TAC std_ss []) 596 \\ `isDot exp` by (Cases_on `exp` \\ FULL_SIMP_TAC std_ss [isVal_def,isSym_def,isDot_def]) 597 \\ ASM_SIMP_TAC std_ss [] 598 \\ `s_ps1 = t_ps1` by METIS_TAC [sexp2abbrev_aux_SND] 599 \\ Cases_on `isQuote exp` 600 THEN1 (FULL_SIMP_TAC std_ss [] 601 \\ Q.PAT_X_ASSUM `!ss ts. bbb` (ASSUME_TAC o Q.SPECL [`"'" ++ s_str3`,`[(Val 3,Val 1)] ++ t_str3`]) 602 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] \\ REPEAT STRIP_TAC 603 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 604 \\ SIMP_TAC (srw_ss()) [APPEND,next_token_def,EVAL ``space_char #"'"``,LET_DEF,SExp_distinct] 605 \\ CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 606 \\ SIMP_TAC std_ss [FST,CONS_11] \\ METIS_TAC []) 607 \\ ASM_SIMP_TAC std_ss [] 608 \\ Q.ABBREV_TAC `s1 = if b \/ s_prefix <> "" then ("(") else ("")` 609 \\ Q.ABBREV_TAC `s2 = if b \/ s_prefix <> "" then (")") else ("")` 610 \\ Q.ABBREV_TAC `t1 = if b \/ s_prefix <> "" then ([(Val 0,Val 1)]) else ([])` 611 \\ Q.ABBREV_TAC `t2 = if b \/ s_prefix <> "" then ([(Val 2,Val 1)]) else ([])` 612 \\ `(if b \/ s_prefix <> "" then 613 ([(Val 0,Val 1)],[(Val 2,Val 1)]) 614 else 615 ([],[])) = (t1,t2)` by METIS_TAC [] 616 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 617 \\ `(if b \/ s_prefix <> "" then 618 ("(",")") 619 else 620 ([],[])) = (s1,s2)` by METIS_TAC [] 621 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 622 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 623 \\ Q.ABBREV_TAC `t3 = if CDR exp = Sym "NIL" then [] 624 else (if isAtom abbrevs (CDR exp) then [(Val 1,Val 1)] else []) ++ t_str2` 625 \\ Q.ABBREV_TAC `s3 = if CDR exp = Sym "NIL" then "" 626 else STRCAT (if isAtom abbrevs (CDR exp) then " . " else " ") s_str2` 627 \\ Q.PAT_X_ASSUM `!ss ts. bbb` (ASSUME_TAC o Q.SPECL [`s1 ++ s_str1 ++ s3 ++ s2`,`t1 ++ t_str1 ++ t3 ++ t2`]) 628 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC] \\ POP_ASSUM (K ALL_TAC) 629 \\ `FST (sexp_lex (STRCAT (STRCAT (STRCAT (s_str1) s3) s2) s)) = 630 t_str1 ++ t3 ++ t2 ++ FST (sexp_lex s)` suffices_by (STRIP_TAC THEN Cases_on `s1 = []` 631 THEN1 (`t1 = []` by METIS_TAC [NOT_CONS_NIL] \\ ASM_SIMP_TAC std_ss [APPEND]) 632 \\ `s1 = "("` by METIS_TAC [NOT_CONS_NIL] 633 \\ `t1 = [^TOKEN_OPEN]` by METIS_TAC [NOT_CONS_NIL] 634 \\ ASM_SIMP_TAC std_ss [APPEND] 635 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 636 \\ SIMP_TAC std_ss [next_token_def,EVAL ``space_char #"("``,LET_DEF,SExp_distinct] 637 \\ CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 638 \\ ASM_SIMP_TAC std_ss [FST,CONS_11]) 639 \\ `~(s3++s2++s = []) ==> MEM (HD (s3++s2++s)) " )"` by 640 (Q.UNABBREV_TAC `s3` \\ Q.UNABBREV_TAC `s2` 641 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [MEM]) 642 \\ `FST (sexp_lex (STRCAT s_str1 (s3++s2++s))) = 643 t_str1 ++ FST (sexp_lex (s3++s2++s))` by 644 (Q.PAT_X_ASSUM `!s b abbrevs ps xs1 xs2 ps1 ps2. bbb` (K ALL_TAC) 645 \\ Q.PAT_X_ASSUM `!s b abbrevs ps xs1 xs2 ps1 ps2. bbb` (MATCH_MP_TAC o RW [AND_IMP_INTRO]) 646 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 647 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND_11] 648 \\ (sg `FST (sexp_lex (STRCAT (s2) s)) = 649 t2 ++ FST (sexp_lex s)`) THEN1 650 (Cases_on `s2 = []` 651 THEN1 (`t2 = []` by METIS_TAC [NOT_CONS_NIL] \\ ASM_SIMP_TAC std_ss [APPEND]) 652 \\ `s2 = ")"` by METIS_TAC [NOT_CONS_NIL] 653 \\ `t2 = [^TOKEN_CLOSE]` by METIS_TAC [NOT_CONS_NIL] 654 \\ ASM_SIMP_TAC std_ss [APPEND] 655 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 656 \\ SIMP_TAC (srw_ss()) [next_token_def,EVAL ``space_char #")"``,LET_DEF,SExp_distinct] 657 \\ CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 658 \\ SIMP_TAC std_ss [FST]) 659 \\ Q.UNABBREV_TAC `s3` \\ Q.UNABBREV_TAC `t3` 660 \\ Cases_on `CDR exp = Sym "NIL"` \\ ASM_SIMP_TAC std_ss [APPEND] 661 \\ `FST (sexp_lex (STRCAT (STRCAT s_str2 s2) s)) = 662 t_str2 ++ t2 ++ FST (sexp_lex s)` suffices_by (STRIP_TAC THEN REVERSE (Cases_on `isAtom abbrevs (CDR exp)`) 663 \\ ASM_SIMP_TAC std_ss [APPEND,sexp_lex_SPACE] 664 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 665 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 666 \\ SIMP_TAC (srw_ss()) [next_token_def,EVAL ``space_char #"."``,LET_DEF,sexp_lex_SPACE] 667 \\ CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 668 \\ FULL_SIMP_TAC std_ss [FST,APPEND_ASSOC]) 669 \\ `~(s2++s = []) ==> MEM (HD (s2++s)) " )"` by 670 (Q.UNABBREV_TAC `s2` \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [MEM]) 671 \\ `FST (sexp_lex (STRCAT s_str2 (s2++s))) = 672 t_str2 ++ FST (sexp_lex (s2++s))` by 673 (Q.PAT_X_ASSUM `!s b abbrevs ps xs1 xs2 ps1 ps2. bbb` (MATCH_MP_TAC o RW [AND_IMP_INTRO]) 674 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 675 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC]); 676 677val sexp_lex_sexp2abbrev_aux = prove( 678 ``!exp b abbrevs ps. 679 FST (sexp_lex (FST (sexp2abbrev_aux exp b abbrevs ps))) = 680 FST (sexp2abbrevt_aux exp b abbrevs ps)``, 681 REPEAT STRIP_TAC 682 \\ MP_TAC (Q.SPECL [`exp`,`[]`] sexp2abbrev_aux_FST) 683 \\ ASM_SIMP_TAC std_ss [APPEND_NIL,EVAL ``sexp_lex ""``] 684 \\ METIS_TAC [PAIR]); 685 686 687(* Part 2 - section 2: algorithm for parsing a list of tokens *) 688 689val _ = Hol_datatype ` 690 lisp_parse_mode = 691 L_READ 692 | L_RETURN of SExp 693 | L_COLLECT of SExp`; 694 695val _ = Hol_datatype ` 696 lisp_parse_action = 697 L_CONS of SExp 698 | L_STOP 699 | L_DOT 700 | L_QUOTE 701 | L_STORE of num`; 702 703val (R_parse_rules,R_parse_ind,R_parse_cases) = Hol_reln ` 704 (* from mode: L_READ *) 705 (!ts s mem x. 706 R_parse ((x, Val 0)::ts,s,L_READ,mem) 707 (ts,s,L_RETURN x,mem)) 708 /\ 709 (!ts s mem. 710 R_parse ((^TOKEN_OPEN)::ts,s,L_READ,mem) 711 (ts,L_STOP::s,L_READ,mem)) 712 /\ 713 (!ts s mem. 714 R_parse ((^TOKEN_DOT)::ts,s,L_READ,mem) 715 (ts,L_DOT::s,L_READ,mem)) 716 /\ 717 (!ts s mem. 718 R_parse ((^TOKEN_QUOTE)::ts,s,L_READ,mem) 719 (ts,L_QUOTE::s,L_READ,mem)) 720 /\ 721 (!ts s mem. 722 R_parse ((^TOKEN_CLOSE)::ts,s,L_READ,mem) 723 (ts,s,L_COLLECT (Sym "NIL"),mem)) 724 /\ 725 (!ts s mem index. 726 R_parse ((^TOKEN_LOAD)::ts,s,L_READ,mem) 727 (ts,s,L_RETURN (mem index),mem)) 728 /\ 729 (!ts s mem index. 730 R_parse ((^TOKEN_SAVE)::ts,s,L_READ,mem) 731 (ts,L_STORE index::s,L_READ,mem)) 732 /\ 733 (* from mode: L_COLLECT *) 734 (!ts s mem exp. 735 R_parse (ts,L_STOP::s,L_COLLECT exp,mem) 736 (ts,s,L_RETURN exp,mem)) 737 /\ 738 (!ts s mem x exp. 739 R_parse (ts,L_CONS x::s,L_COLLECT exp,mem) 740 (ts,s,L_COLLECT (Dot x exp),mem)) 741 /\ 742 (!ts s mem exp. 743 R_parse (ts,L_DOT::s,L_COLLECT exp,mem) 744 (ts,s,L_COLLECT (CAR exp),mem)) 745 /\ 746 (* from mode: L_RETURN *) 747 (!ts s mem exp. 748 R_parse (ts,L_QUOTE::s,L_RETURN exp,mem) 749 (ts,s,L_RETURN (Dot (Sym "QUOTE") (Dot exp (Sym "NIL"))),mem)) 750 /\ 751 (!ts s mem n exp. 752 R_parse (ts,L_STORE n::s,L_RETURN exp,mem) 753 (ts,s,L_RETURN exp,(n =+ exp) mem)) 754 /\ 755 (!ts s mem exp. 756 ~(s = []) /\ ~(HD s = L_QUOTE) /\ ~(?k. HD s = L_STORE k) ==> 757 R_parse (ts,s,L_RETURN exp,mem) 758 (ts,L_CONS exp::s,L_READ,mem))` 759 760val READ_L_STORE_def = Define ` 761 (READ_L_STORE (L_STORE n) = SOME n) /\ 762 (READ_L_STORE _ = NONE)`; 763 764val READ_L_CONS_def = Define ` 765 (READ_L_CONS (L_CONS exp) = SOME exp) /\ 766 (READ_L_CONS _ = NONE)`; 767 768val NOT_NIL_IMP = prove( 769 ``!x. ~(x = []) ==> ?x1 x2. x = x1::x2``, 770 Cases \\ SRW_TAC [] []) 771 772val sexp_parse_aux_def = tDefine "sexp_parse_aux" ` 773 (sexp_parse_aux (ts,s,L_READ,mem) = 774 if ts = [] then Sym "NIL" else 775 let (t,ts) = (HD ts, TL ts) in 776 if SND t = Val 0 then sexp_parse_aux (ts,s,L_RETURN (FST t),mem) else 777 if (t = ^TOKEN_OPEN) then sexp_parse_aux (ts,L_STOP::s,L_READ,mem) else 778 if (t = ^TOKEN_DOT) then sexp_parse_aux (ts,L_DOT::s,L_READ,mem) else 779 if (t = ^TOKEN_QUOTE) then sexp_parse_aux (ts,L_QUOTE::s,L_READ,mem) else 780 if (t = ^TOKEN_CLOSE) then sexp_parse_aux (ts,s,L_COLLECT (Sym "NIL"),mem) else 781 if ~isVal (FST t) then Sym "NIL" else 782 if SND t = Val 3 then sexp_parse_aux (ts,s,L_RETURN (mem (getVal (FST t))),mem) else 783 if SND t = Val 2 then sexp_parse_aux (ts,L_STORE (getVal (FST t))::s,L_READ,mem) else 784 Sym "NIL") /\ 785 (sexp_parse_aux (ts,s,L_COLLECT exp,mem) = 786 if s = [] then Sym "NIL" else 787 let (x,s) = (HD s, TL s) in 788 if x = L_STOP then sexp_parse_aux (ts,s,L_RETURN exp,mem) else 789 if ~(READ_L_CONS x = NONE) then sexp_parse_aux (ts,s,L_COLLECT (Dot (THE (READ_L_CONS x)) exp),mem) else 790 if x = L_DOT then sexp_parse_aux (ts,s,L_COLLECT (CAR exp),mem) else 791 Sym "NIL") /\ 792 (sexp_parse_aux (ts,s,L_RETURN exp,mem) = 793 if s = [] then exp else 794 let (x,s) = (HD s, TL s) in 795 if x = L_QUOTE then sexp_parse_aux (ts,s,L_RETURN (Dot (Sym "QUOTE") (Dot exp (Sym "NIL"))),mem) else 796 if ~(READ_L_STORE x = NONE) then sexp_parse_aux (ts,s,L_RETURN exp,(THE (READ_L_STORE x) =+ exp) mem) else 797 sexp_parse_aux (ts,L_CONS exp::x::s,L_READ,mem))` 798 (WF_REL_TAC `measure (\(ts,s,mode,mem). 799 3 * LENGTH ts + LENGTH s + if mode = L_READ then 0 else 2)` 800 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC NOT_NIL_IMP 801 \\ FULL_SIMP_TAC (srw_ss()) [] \\ DECIDE_TAC) 802 803val RTC_parse_IMP_sexp_parse_aux = prove( 804 ``!x y. RTC R_parse x y ==> 805 !exp. (FST (SND (SND y)) = L_RETURN exp) /\ (FST (SND y) = []) ==> 806 (sexp_parse_aux x = exp)``, 807 HO_MATCH_MP_TAC RTC_INDUCT \\ REPEAT STRIP_TAC THEN1 808 (`?ts s mode mem. x = (ts,s,mode,mem)` by METIS_TAC [PAIR] 809 \\ FULL_SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [sexp_parse_aux_def] 810 \\ ASM_SIMP_TAC std_ss []) 811 \\ `sexp_parse_aux x = sexp_parse_aux x'` suffices_by (STRIP_TAC THEN METIS_TAC []) 812 \\ Q.PAT_X_ASSUM `R_parse x x'` MP_TAC 813 \\ ONCE_REWRITE_TAC [R_parse_cases] 814 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 815 \\ SIMP_TAC std_ss [Once sexp_parse_aux_def] 816 \\ FULL_SIMP_TAC (srw_ss()) [isVal_def,isSym_def,LET_DEF,getVal_def, 817 DECIDE ``~(SUC (SUC n) < 2)``,READ_L_CONS_def,READ_L_STORE_def] 818 \\ IMP_RES_TAC NOT_NIL_IMP 819 \\ Cases_on `x1` 820 \\ FULL_SIMP_TAC (srw_ss()) [isVal_def,isSym_def,LET_DEF,getVal_def, 821 DECIDE ``~(SUC (SUC n) < 2)``,READ_L_CONS_def,READ_L_STORE_def]); 822 823val RTC_UNROLL = prove( 824 ``!x y z. R x y /\ RTC R y z ==> RTC R x z``, 825 METIS_TAC [RTC_RULES]); 826 827val RTC_UNROLL2 = prove( 828 ``!x y z. RTC R x y /\ R y z ==> RTC R x z``, 829 METIS_TAC [RTC_RULES_RIGHT1]); 830 831val R_parse_abbrev_def = Define ` 832 R_parse_abbrev abbrevs ps (mem:num->SExp) = 833 !s. s IN ps ==> s IN FDOM abbrevs /\ (mem (abbrevs ' s) = s)`; 834 835val FMAP_11_def = Define ` 836 FMAP_11 f = !x y. x IN FDOM f /\ y IN FDOM f ==> ((f ' x = f ' y) = (x = y))`; 837 838val cons_atoms_def = tDefine "cons_atoms" ` 839 cons_atoms abbrevs exp s = 840 if isAtom abbrevs exp then L_CONS exp :: s else 841 if CDR exp = Sym "NIL" then L_CONS (CAR exp) :: s else 842 if isAtom abbrevs (CDR exp) then L_CONS (CDR exp)::L_DOT::L_CONS (CAR exp)::s else 843 cons_atoms abbrevs (CDR exp) (L_CONS (CAR exp) :: s)` 844 (WF_REL_TAC `measure (LSIZE o FST o SND)` 845 \\ REPEAT STRIP_TAC \\ POP_ASSUM (K ALL_TAC) 846 \\ FULL_SIMP_TAC std_ss [isAtom_def,isDot_thm] \\ REPEAT STRIP_TAC 847 \\ FULL_SIMP_TAC std_ss [LSIZE_def,CDR_def] \\ DECIDE_TAC) 848 849val cons_atoms_lemma = prove( 850 ``~isAtom abbrevs (Dot a1 a2) /\ ~(a2 = Sym "NIL") ==> 851 (cons_atoms abbrevs (Dot a1 a2) s = 852 if isAtom abbrevs a2 then 853 L_CONS a2::L_DOT::L_CONS a1::s 854 else 855 cons_atoms abbrevs a2 (L_CONS a1::s))``, 856 REPEAT STRIP_TAC 857 \\ SIMP_TAC std_ss [Once cons_atoms_def] 858 \\ ASM_SIMP_TAC std_ss [CDR_def,CAR_def]); 859 860val MAP_L_CONS_COLLECT = prove( 861 ``!xs y. 862 RTC R_parse (ts,MAP L_CONS xs ++ [L_STOP] ++ s,L_COLLECT y,mem) 863 (ts,s,L_RETURN (FOLDL (\x y. Dot y x) y xs),mem)``, 864 Induct THEN1 865 (SIMP_TAC std_ss [MAP,FOLDL,APPEND] \\ REPEAT STRIP_TAC 866 \\ MATCH_MP_TAC RTC_SINGLE 867 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 868 \\ SIMP_TAC std_ss [MAP,FOLDL,APPEND] \\ REPEAT STRIP_TAC 869 \\ MATCH_MP_TAC RTC_UNROLL 870 \\ Q.EXISTS_TAC `(ts,(MAP L_CONS xs ++ [L_STOP] ++ s),L_COLLECT (Dot h y),mem)` 871 \\ STRIP_TAC 872 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 873 \\ ASM_SIMP_TAC std_ss []); 874 875val cons_atoms_FOLDL = prove( 876 ``!y xs. 877 ~(isAtom abbrevs y) ==> 878 RTC R_parse 879 (ts,cons_atoms abbrevs y (MAP L_CONS xs ++ [L_STOP] ++ s),L_COLLECT (Sym "NIL"),mem) 880 (ts,s,L_RETURN (FOLDL (\x y. Dot y x) y xs),mem)``, 881 completeInduct_on `LSIZE y` \\ REPEAT STRIP_TAC 882 \\ ONCE_REWRITE_TAC [cons_atoms_def] 883 \\ ASM_SIMP_TAC std_ss [] \\ SRW_TAC [] [] 884 THEN1 885 (`isDot y` by METIS_TAC [isAtom_def] 886 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def] \\ FULL_SIMP_TAC std_ss [CDR_def] 887 \\ MATCH_MP_TAC RTC_UNROLL 888 \\ Q.EXISTS_TAC `(ts,MAP L_CONS xs ++ [L_STOP] ++ s, L_COLLECT y,mem)` 889 \\ STRIP_TAC 890 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 891 \\ ASM_SIMP_TAC std_ss [MAP_L_CONS_COLLECT]) 892 THEN1 893 (`isDot y` by METIS_TAC [isAtom_def] 894 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def] \\ FULL_SIMP_TAC std_ss [CDR_def] 895 \\ MATCH_MP_TAC RTC_UNROLL 896 \\ Q.EXISTS_TAC `(ts,L_DOT::L_CONS a::(MAP L_CONS xs ++ [L_STOP] ++ s), L_COLLECT (Dot b (Sym "NIL")),mem)` 897 \\ STRIP_TAC 898 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 899 \\ MATCH_MP_TAC RTC_UNROLL 900 \\ Q.EXISTS_TAC `(ts,L_CONS a::(MAP L_CONS xs ++ [L_STOP] ++ s), L_COLLECT b,mem)` 901 \\ STRIP_TAC 902 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 903 \\ MATCH_MP_TAC RTC_UNROLL 904 \\ Q.EXISTS_TAC `(ts,(MAP L_CONS xs ++ [L_STOP] ++ s), L_COLLECT (Dot a b),mem)` 905 \\ STRIP_TAC 906 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 907 \\ ASM_SIMP_TAC std_ss [MAP_L_CONS_COLLECT]) 908 \\ `isDot y` by METIS_TAC [isAtom_def] 909 \\ FULL_SIMP_TAC std_ss [isDot_thm] 910 \\ FULL_SIMP_TAC std_ss [LSIZE_def,CDR_def,CAR_def] 911 \\ `LSIZE b < SUC (LSIZE a + LSIZE b)` by DECIDE_TAC 912 \\ RES_TAC \\ POP_ASSUM (MP_TAC o Q.SPEC `b`) 913 \\ Q.PAT_X_ASSUM `!m.bb` (K ALL_TAC) 914 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 915 \\ POP_ASSUM (MP_TAC o Q.SPEC `a::xs`) 916 \\ SIMP_TAC std_ss [APPEND,MAP,FOLDL]); 917 918val R_parse_lemma = prove( 919 ``!exp b ts s mem ps. 920 (~b ==> ~(s = []) /\ ~(HD s = L_QUOTE) /\ ~(?k. HD s = L_STORE k)) /\ 921 FMAP_11 abbrevs /\ R_parse_abbrev abbrevs ps mem ==> 922 ?ps5 mem5 str5. 923 (sexp2abbrevt_aux exp b abbrevs ps = (str5,ps5)) /\ 924 RTC R_parse (str5 ++ ts,s,L_READ,mem) 925 (if b then (ts,s,L_RETURN exp,mem5) 926 else (ts,cons_atoms abbrevs exp s,L_READ,mem5)) /\ 927 R_parse_abbrev abbrevs ps5 mem5``, 928 HO_MATCH_MP_TAC SExp_print_induct \\ REPEAT STRIP_TAC 929 \\ ONCE_REWRITE_TAC [sexp2abbrevt_aux_def] 930 \\ ASM_SIMP_TAC std_ss [LET_DEF] 931 \\ Q.ABBREV_TAC `index = abbrevs ' exp` 932 \\ Q.ABBREV_TAC `prefix = if exp IN FDOM abbrevs then [^TOKEN_SAVE] else []` 933 \\ Q.ABBREV_TAC `ps0 = if exp IN FDOM abbrevs then exp INSERT ps else ps` 934 \\ `(if exp IN FDOM abbrevs then 935 ([^TOKEN_SAVE],exp INSERT ps) 936 else 937 ([],ps)) = (prefix,ps0)` by METIS_TAC [] 938 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 939 \\ Cases_on `exp IN ps` \\ ASM_SIMP_TAC std_ss [] THEN1 940 (`exp IN FDOM abbrevs` by METIS_TAC [R_parse_abbrev_def] 941 \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `mem` 942 \\ ASM_SIMP_TAC std_ss [] 943 \\ MATCH_MP_TAC RTC_UNROLL 944 \\ FULL_SIMP_TAC std_ss [R_parse_abbrev_def] 945 \\ Q.UNABBREV_TAC `index` 946 \\ RES_TAC 947 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,mem)` 948 \\ STRIP_TAC 949 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 950 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] 951 \\ MATCH_MP_TAC RTC_SINGLE 952 \\ ONCE_REWRITE_TAC [cons_atoms_def] 953 \\ ASM_SIMP_TAC std_ss [isAtom_def] 954 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 955 \\ `?str1 ps1. sexp2abbrevt_aux (CAR exp) T abbrevs ps = (str1,ps1)` by METIS_TAC [PAIR] 956 \\ `?str2 ps2. sexp2abbrevt_aux (CDR exp) F abbrevs ps1 = (str2,ps2)` by METIS_TAC [PAIR] 957 \\ `?str3 ps3. sexp2abbrevt_aux (CAR (CDR exp)) T abbrevs ps = (str3,ps3)` by METIS_TAC [PAIR] 958 \\ ASM_SIMP_TAC std_ss [] 959 \\ Q.ABBREV_TAC `s1 = if b \/ prefix <> [] then [^TOKEN_OPEN] else []` 960 \\ Q.ABBREV_TAC `s2 = if b \/ prefix <> [] then [^TOKEN_CLOSE] else []` 961 \\ `(if b \/ prefix <> [] then ([^TOKEN_OPEN],[^TOKEN_CLOSE]) 962 else ([],[])) = (s1,s2)` by METIS_TAC [] 963 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 964 \\ `!tts. RTC R_parse (prefix ++ tts,s,L_READ,mem) 965 (tts,(if exp IN FDOM abbrevs 966 then (L_STORE (abbrevs ' exp))::s else s),L_READ,mem)` by 967 (Q.UNABBREV_TAC `prefix` 968 \\ REVERSE (Cases_on `exp IN FDOM abbrevs`) 969 \\ ASM_SIMP_TAC std_ss [APPEND,RTC_REFL] 970 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC RTC_SINGLE 971 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 972 \\ Q.ABBREV_TAC `s9 = if exp IN FDOM abbrevs then L_STORE (abbrevs ' exp)::s else s` 973 \\ Cases_on `~(isDot exp)` \\ ASM_SIMP_TAC std_ss [] THEN1 974 (ONCE_REWRITE_TAC [cons_atoms_def] \\ ASM_SIMP_TAC std_ss [isAtom_def,isDot_def] 975 \\ Q.EXISTS_TAC `if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem else mem` 976 \\ REVERSE STRIP_TAC THEN1 977 (Q.UNABBREV_TAC `ps0` \\ POP_ASSUM (ASSUME_TAC o GSYM) 978 \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `exp IN FDOM abbrevs` 979 \\ ASM_SIMP_TAC std_ss [] 980 \\ FULL_SIMP_TAC std_ss [IN_INSERT,R_parse_abbrev_def,APPLY_UPDATE_THM] 981 \\ CONV_TAC (RAND_CONV (ALPHA_CONV ``exp2:SExp``)) \\ STRIP_TAC 982 \\ Cases_on `exp2 = exp` \\ ASM_SIMP_TAC std_ss [] 983 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [FMAP_11_def]) 984 \\ Q.ABBREV_TAC `mem2 = if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem else mem` 985 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 986 \\ Q.EXISTS_TAC `([(exp,Val 0)] ++ ts,s9,L_READ,mem)` 987 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 988 \\ MATCH_MP_TAC RTC_UNROLL 989 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN exp,mem)` 990 \\ STRIP_TAC 991 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 992 \\ Q.UNABBREV_TAC `s9` 993 \\ Q.UNABBREV_TAC `mem2` 994 \\ REVERSE (Cases_on `exp IN FDOM abbrevs` \\ ASM_SIMP_TAC std_ss []) 995 THEN1 (Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] \\ MATCH_MP_TAC RTC_SINGLE 996 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 997 \\ MATCH_MP_TAC RTC_UNROLL 998 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,(abbrevs ' exp =+ exp) mem)` 999 \\ STRIP_TAC 1000 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1001 THEN1 (Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] \\ MATCH_MP_TAC RTC_SINGLE 1002 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [])) 1003 \\ Cases_on `isQuote exp` \\ ASM_SIMP_TAC std_ss [] THEN1 1004 (ONCE_REWRITE_TAC [cons_atoms_def] \\ ASM_SIMP_TAC std_ss [isAtom_def,isDot_def] 1005 \\ FULL_SIMP_TAC std_ss [isQuote_thm] \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def] 1006 \\ FULL_SIMP_TAC std_ss [] 1007 \\ Q.PAT_X_ASSUM `!b ts. bbb` (MP_TAC o Q.SPECL [`T`,`ts`,`L_QUOTE::s9`,`mem`,`ps`]) 1008 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1009 \\ Q.ABBREV_TAC `mem6 = if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem5 else mem5` 1010 \\ Q.EXISTS_TAC `mem6` 1011 \\ REVERSE STRIP_TAC THEN1 1012 (Q.UNABBREV_TAC `mem6` \\ POP_ASSUM (ASSUME_TAC o GSYM) 1013 \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `exp IN FDOM abbrevs` 1014 \\ ASM_SIMP_TAC std_ss [] 1015 \\ FULL_SIMP_TAC std_ss [IN_INSERT,R_parse_abbrev_def,APPLY_UPDATE_THM] 1016 \\ CONV_TAC (RAND_CONV (ALPHA_CONV ``exp2:SExp``)) \\ STRIP_TAC 1017 \\ Cases_on `exp2 = exp` \\ ASM_SIMP_TAC std_ss [] 1018 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1019 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,IN_INSERT] 1020 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [FMAP_11_def]) 1021 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1022 \\ Q.EXISTS_TAC `([^TOKEN_QUOTE] ++ str3 ++ ts,s9,L_READ,mem)` 1023 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1024 \\ MATCH_MP_TAC RTC_UNROLL 1025 \\ Q.EXISTS_TAC `(str3 ++ ts,L_QUOTE::s9,L_READ,mem)` 1026 \\ STRIP_TAC 1027 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1028 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1029 \\ Q.EXISTS_TAC `(ts,L_QUOTE::s9,L_RETURN y,mem5)` 1030 \\ ASM_SIMP_TAC std_ss [] 1031 \\ MATCH_MP_TAC RTC_UNROLL 1032 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN exp,mem5)` 1033 \\ STRIP_TAC 1034 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1035 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1036 \\ FULL_SIMP_TAC std_ss [] 1037 \\ Q.UNABBREV_TAC `s9` 1038 \\ Q.UNABBREV_TAC `mem6` 1039 \\ REVERSE (Cases_on `exp IN FDOM abbrevs` \\ ASM_SIMP_TAC std_ss []) 1040 THEN1 (Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] \\ MATCH_MP_TAC RTC_SINGLE 1041 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1042 \\ MATCH_MP_TAC RTC_UNROLL 1043 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,(abbrevs ' exp =+ exp) mem5)` 1044 \\ STRIP_TAC 1045 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1046 THEN1 (Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] \\ MATCH_MP_TAC RTC_SINGLE 1047 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [])) 1048 \\ FULL_SIMP_TAC std_ss [] 1049 \\ `?a1 a2. exp = Dot a1 a2` by METIS_TAC [isDot_thm] 1050 \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def] 1051 \\ Cases_on `a2 = Sym "NIL"` \\ FULL_SIMP_TAC std_ss [APPEND_NIL] THEN1 1052 (Q.PAT_X_ASSUM `!b ts. bbb` (K ALL_TAC) 1053 \\ Q.ABBREV_TAC `s8 = if s1 = [] then s9 else L_STOP::s9` 1054 \\ Q.PAT_X_ASSUM `!b ts. bbb` (MP_TAC o Q.SPECL [`T`,`s2++ts`,`s8`,`mem`,`ps`]) 1055 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1056 \\ Q.ABBREV_TAC `mem6 = if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem5 else mem5` 1057 \\ Q.EXISTS_TAC `mem6` 1058 \\ REVERSE STRIP_TAC THEN1 1059 (Q.UNABBREV_TAC `mem6` \\ POP_ASSUM (ASSUME_TAC o GSYM) 1060 \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `exp IN FDOM abbrevs` 1061 \\ ASM_SIMP_TAC std_ss [] 1062 \\ FULL_SIMP_TAC std_ss [IN_INSERT,R_parse_abbrev_def,APPLY_UPDATE_THM] 1063 \\ CONV_TAC (RAND_CONV (ALPHA_CONV ``exp2:SExp``)) \\ STRIP_TAC 1064 \\ Cases_on `exp2 = exp` \\ ASM_SIMP_TAC std_ss [] 1065 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1066 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,IN_INSERT] 1067 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [FMAP_11_def]) 1068 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1069 \\ Q.EXISTS_TAC `(s1 ++ str1 ++ s2 ++ ts,s9,L_READ,mem)` 1070 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1071 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1072 \\ Q.EXISTS_TAC `((str1 ++ (s2 ++ ts)),s8,L_READ,mem)` 1073 \\ STRIP_TAC THEN1 1074 (Q.UNABBREV_TAC `s8` \\ Cases_on `s1 = []` 1075 \\ ASM_SIMP_TAC std_ss [APPEND,RTC_REFL] 1076 \\ Q.UNABBREV_TAC `s1` \\ Cases_on `b \/ prefix <> []` 1077 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 1078 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 1079 \\ MATCH_MP_TAC RTC_SINGLE 1080 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1081 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1082 \\ Q.EXISTS_TAC `(s2 ++ ts,s8,L_RETURN a1,mem5)` 1083 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1084 \\ MATCH_MP_TAC RTC_UNROLL 1085 \\ Q.EXISTS_TAC `(s2 ++ ts,L_CONS a1::s8,L_READ,mem5)` 1086 \\ STRIP_TAC 1087 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [] 1088 \\ FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def] 1089 \\ Cases_on `b` \\ FULL_SIMP_TAC (srw_ss()) [NOT_CONS_NIL,HD] 1090 \\ METIS_TAC [NOT_CONS_NIL,fetch "-" "lisp_parse_action_distinct",HD,CONS_11]) 1091 \\ Cases_on `s2 = []` THEN1 1092 (`~b` by METIS_TAC [NOT_CONS_NIL] 1093 \\ `s1 = []` by METIS_TAC [NOT_CONS_NIL] 1094 \\ FULL_SIMP_TAC std_ss [APPEND] 1095 \\ Q.UNABBREV_TAC `s8` 1096 \\ `(s9 = s) /\ ~(exp IN FDOM abbrevs)` by METIS_TAC [NOT_CONS_NIL] 1097 \\ POP_ASSUM MP_TAC 1098 \\ ONCE_REWRITE_TAC [cons_atoms_def] \\ Q.UNABBREV_TAC `mem6` 1099 \\ ASM_SIMP_TAC std_ss [isAtom_def,CAR_def,CDR_def,RTC_REFL]) 1100 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1101 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN exp,mem5)` 1102 \\ STRIP_TAC THEN1 1103 (`s2 = [^TOKEN_CLOSE]` by METIS_TAC [] \\ ASM_SIMP_TAC std_ss [APPEND] 1104 \\ `s8 = L_STOP::s9` by METIS_TAC [NOT_CONS_NIL] \\ ASM_SIMP_TAC std_ss [] 1105 \\ MATCH_MP_TAC RTC_UNROLL 1106 \\ Q.EXISTS_TAC `(ts,L_CONS a1::L_STOP::s9,L_COLLECT (Sym "NIL"),mem5)` 1107 \\ STRIP_TAC 1108 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1109 \\ MATCH_MP_TAC RTC_UNROLL 1110 \\ Q.EXISTS_TAC `(ts,L_STOP::s9,L_COLLECT (Dot a1 (Sym "NIL")),mem5)` 1111 \\ STRIP_TAC 1112 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1113 \\ MATCH_MP_TAC RTC_UNROLL 1114 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN (Dot a1 (Sym "NIL")),mem5)` 1115 \\ STRIP_TAC 1116 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1117 \\ ASM_SIMP_TAC std_ss [RTC_REFL]) 1118 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1119 \\ FULL_SIMP_TAC std_ss [] 1120 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1121 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,mem6)` 1122 \\ STRIP_TAC THEN1 1123 (Q.UNABBREV_TAC `s9` \\ Q.UNABBREV_TAC `mem6` 1124 \\ Cases_on `exp IN FDOM abbrevs` \\ ASM_SIMP_TAC std_ss [RTC_REFL] 1125 \\ MATCH_MP_TAC RTC_SINGLE 1126 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1127 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] 1128 \\ ONCE_REWRITE_TAC [cons_atoms_def] 1129 \\ `isAtom abbrevs exp` by METIS_TAC [NOT_CONS_NIL,isAtom_def] 1130 \\ ASM_SIMP_TAC std_ss [] 1131 \\ MATCH_MP_TAC RTC_SINGLE 1132 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1133 \\ Q.PAT_X_ASSUM `!b ts. bbb` MP_TAC 1134 \\ Q.ABBREV_TAC `s8 = if s1 = [] then s9 else L_STOP::s9` 1135 \\ Q.ABBREV_TAC `s7 = if isAtom abbrevs a2 then L_DOT::L_CONS a1::s8 else L_CONS a1::s8` 1136 \\ `~(s7 = [])` by METIS_TAC [NOT_CONS_NIL] 1137 \\ `~(s8 = [])` by (FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def] \\ Cases_on `b` 1138 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] \\ METIS_TAC [NOT_CONS_NIL]) 1139 \\ `HD s7 <> L_QUOTE /\ (!k. HD s7 <> L_STORE k)` by 1140 (METIS_TAC [NOT_CONS_NIL,fetch "-" "lisp_parse_action_distinct",HD,CONS_11]) 1141 \\ Q.PAT_X_ASSUM `!b ts. bbb` (MP_TAC o Q.SPECL [`T`,`((if isAtom (abbrevs:SExp|->num) a2 then [^TOKEN_DOT] else []) ++ str2) ++ s2++ts`,`s8`,`mem`,`ps`]) 1142 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1143 \\ POP_ASSUM (MP_TAC o Q.SPECL [`F`,`s2++ts`,`s7`,`mem5`,`ps1`]) 1144 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1145 \\ Q.ABBREV_TAC `mem6 = if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem5' else mem5'` 1146 \\ Q.EXISTS_TAC `mem6` 1147 \\ REVERSE STRIP_TAC THEN1 1148 (Q.UNABBREV_TAC `mem6` \\ POP_ASSUM (ASSUME_TAC o GSYM) 1149 \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `exp IN FDOM abbrevs` 1150 \\ ASM_SIMP_TAC std_ss [] 1151 \\ FULL_SIMP_TAC std_ss [IN_INSERT,R_parse_abbrev_def,APPLY_UPDATE_THM] 1152 \\ CONV_TAC (RAND_CONV (ALPHA_CONV ``exp2:SExp``)) \\ STRIP_TAC 1153 \\ Cases_on `exp2 = exp` \\ ASM_SIMP_TAC std_ss [] 1154 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1155 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,IN_INSERT,R_parse_abbrev_def] 1156 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [FMAP_11_def]) 1157 \\ Q.ABBREV_TAC `dot = if isAtom abbrevs a2 then [^TOKEN_DOT] else []` 1158 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1159 \\ Q.EXISTS_TAC `(s1 ++ str1 ++ (dot ++ str2) ++ s2 ++ ts,s9,L_READ,mem)` 1160 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1161 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1162 \\ Q.EXISTS_TAC `(str1 ++ (dot ++ (str2 ++ (s2 ++ ts))),s8,L_READ,mem)` 1163 \\ STRIP_TAC THEN1 1164 (Q.UNABBREV_TAC `s8` \\ Cases_on `s1 = []` 1165 \\ ASM_SIMP_TAC std_ss [APPEND,RTC_REFL] 1166 \\ Q.UNABBREV_TAC `s1` \\ Cases_on `b \/ prefix <> []` 1167 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 1168 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 1169 \\ MATCH_MP_TAC RTC_SINGLE 1170 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1171 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1172 \\ Q.EXISTS_TAC `(dot ++ str2 ++ s2 ++ ts,s8,L_RETURN a1,mem5)` 1173 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1174 \\ MATCH_MP_TAC RTC_UNROLL 1175 \\ Q.EXISTS_TAC `(dot ++ (str2 ++ (s2 ++ ts)),L_CONS a1::s8,L_READ,mem5)` 1176 \\ STRIP_TAC 1177 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [] 1178 \\ METIS_TAC [NOT_CONS_NIL,fetch "-" "lisp_parse_action_distinct",HD,CONS_11]) 1179 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1180 \\ Q.EXISTS_TAC `(str2 ++ s2 ++ ts,s7,L_READ,mem5)` 1181 \\ STRIP_TAC THEN1 1182 (Q.UNABBREV_TAC `dot` \\ Q.UNABBREV_TAC `s7` 1183 \\ Cases_on `isAtom abbrevs a2` \\ ASM_SIMP_TAC std_ss [] 1184 \\ FULL_SIMP_TAC std_ss [RTC_REFL,APPEND,APPEND_ASSOC] 1185 \\ MATCH_MP_TAC RTC_SINGLE 1186 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1187 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1188 \\ Q.EXISTS_TAC `(s2 ++ ts,cons_atoms abbrevs a2 s7,L_READ,mem5')` 1189 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1190 \\ Cases_on `s2 = []` THEN1 1191 (`~b` by METIS_TAC [NOT_CONS_NIL] 1192 \\ `s1 = []` by METIS_TAC [NOT_CONS_NIL] 1193 \\ FULL_SIMP_TAC std_ss [APPEND] 1194 \\ Q.UNABBREV_TAC `s8` 1195 \\ Q.UNABBREV_TAC `s7` 1196 \\ `(s9 = s) /\ ~(exp IN FDOM abbrevs)` by METIS_TAC [NOT_CONS_NIL] 1197 \\ POP_ASSUM MP_TAC 1198 \\ ASM_SIMP_TAC std_ss [] 1199 \\ Cases_on `isAtom abbrevs a2` \\ ASM_SIMP_TAC std_ss [] 1200 \\ Q.UNABBREV_TAC `mem6` 1201 \\ REPEAT STRIP_TAC 1202 \\ `~(isAtom abbrevs (Dot a1 a2))` by (FULL_SIMP_TAC std_ss [isAtom_def]) 1203 \\ ASM_SIMP_TAC std_ss [cons_atoms_lemma,RTC_REFL] 1204 \\ ONCE_REWRITE_TAC [cons_atoms_def] \\ ASM_SIMP_TAC std_ss [RTC_REFL]) 1205 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1206 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN exp,mem5')` 1207 \\ STRIP_TAC THEN1 1208 (`s2 = [^TOKEN_CLOSE]` by METIS_TAC [] \\ ASM_SIMP_TAC std_ss [APPEND] 1209 \\ `s8 = L_STOP::s9` by METIS_TAC [NOT_CONS_NIL] \\ ASM_SIMP_TAC std_ss [] 1210 \\ MATCH_MP_TAC RTC_UNROLL 1211 \\ Q.EXISTS_TAC `(ts,cons_atoms abbrevs a2 s7,L_COLLECT (Sym "NIL"),mem5')` 1212 \\ STRIP_TAC 1213 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1214 \\ Q.UNABBREV_TAC `s7` \\ ASM_SIMP_TAC std_ss [] 1215 \\ Cases_on `isAtom abbrevs a2` \\ ASM_SIMP_TAC std_ss [] THEN1 1216 (ONCE_REWRITE_TAC [cons_atoms_def] \\ ASM_SIMP_TAC std_ss [] 1217 \\ MATCH_MP_TAC RTC_UNROLL 1218 \\ Q.EXISTS_TAC `(ts,L_DOT::L_CONS a1::L_STOP::s9,L_COLLECT (Dot a2 (Sym "NIL")),mem5')` 1219 \\ STRIP_TAC 1220 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1221 \\ MATCH_MP_TAC RTC_UNROLL 1222 \\ Q.EXISTS_TAC `(ts,L_CONS a1::L_STOP::s9,L_COLLECT a2,mem5')` 1223 \\ STRIP_TAC 1224 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 1225 \\ MATCH_MP_TAC RTC_UNROLL 1226 \\ Q.EXISTS_TAC `(ts,L_STOP::s9,L_COLLECT (Dot a1 a2),mem5')` 1227 \\ STRIP_TAC 1228 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 1229 \\ MATCH_MP_TAC RTC_UNROLL 1230 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN (Dot a1 a2),mem5')` 1231 \\ STRIP_TAC 1232 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 1233 \\ ASM_SIMP_TAC std_ss [RTC_REFL]) 1234 \\ MATCH_MP_TAC (SIMP_RULE std_ss [MAP,APPEND,FOLDL] (Q.SPECL [`a2`,`[a1]`] cons_atoms_FOLDL)) 1235 \\ ASM_SIMP_TAC std_ss []) 1236 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1237 \\ FULL_SIMP_TAC std_ss [] 1238 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1239 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,mem6)` 1240 \\ STRIP_TAC THEN1 1241 (Q.UNABBREV_TAC `s9` \\ Q.UNABBREV_TAC `mem6` 1242 \\ Cases_on `exp IN FDOM abbrevs` \\ ASM_SIMP_TAC std_ss [RTC_REFL] 1243 \\ MATCH_MP_TAC RTC_SINGLE 1244 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1245 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] 1246 \\ `exp IN FDOM abbrevs` by METIS_TAC [NOT_CONS_NIL] 1247 \\ ASM_SIMP_TAC std_ss [Once cons_atoms_def,isAtom_def] 1248 \\ MATCH_MP_TAC RTC_SINGLE 1249 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []); 1250 1251val R_parse_thm = prove( 1252 ``!exp ts s mem abbrevs. 1253 FMAP_11 abbrevs ==> 1254 ?mem2. 1255 RTC R_parse (FST (sexp2abbrevt_aux exp T abbrevs {}) ++ ts,s,L_READ,mem) 1256 (ts,s,L_RETURN exp,mem2)``, 1257 REPEAT STRIP_TAC 1258 \\ `?str ps. sexp2abbrevt_aux exp T abbrevs {} = (str,ps)` by METIS_TAC [PAIR] 1259 \\ MP_TAC (Q.SPECL [`exp`,`T`,`ts`,`s`,`mem`,`{}`] R_parse_lemma) 1260 \\ ASM_SIMP_TAC std_ss [R_parse_abbrev_def,NOT_IN_EMPTY] \\ METIS_TAC []); 1261 1262val sexp_parse_def = Define ` 1263 sexp_parse ts = sexp_parse_aux (ts,[],L_READ,\x.Sym "NIL")`; 1264 1265val sexp_parse_aux_sexp2abbrevt = prove( 1266 ``!exp ts abbrevs. 1267 FMAP_11 abbrevs ==> 1268 (sexp_parse (FST (sexp2abbrevt_aux exp T abbrevs {}) ++ ts) = exp)``, 1269 METIS_TAC [R_parse_thm,RTC_parse_IMP_sexp_parse_aux,FST,SND,sexp_parse_def]); 1270 1271val string2sexp_def = Define ` 1272 string2sexp str = (sexp_parse (FST (sexp_lex str)))`; 1273 1274val FDOM_sexp_abbrev_fmap_IMP = prove( 1275 ``!xs x k. x IN FDOM (sexp_abbrev_fmap xs k) ==> 1276 k <= sexp_abbrev_fmap xs k ' x``, 1277 Induct \\ SIMP_TAC (srw_ss()) [sexp_abbrev_fmap_def, 1278 FDOM_FEMPTY,FAPPLY_FUPDATE_THM] \\ REPEAT STRIP_TAC 1279 \\ ASM_SIMP_TAC std_ss [] \\ RES_TAC 1280 \\ METIS_TAC [LESS_EQ_REFL,DECIDE ``k <= k+1:num``,LESS_EQ_TRANS]); 1281 1282val FMAP_11_sexp_abbrev_fmap = prove( 1283 ``!xs k. FMAP_11 (sexp_abbrev_fmap xs k)``, 1284 Induct \\ SIMP_TAC (srw_ss()) [sexp_abbrev_fmap_def, 1285 FMAP_11_def,FDOM_FEMPTY,FAPPLY_FUPDATE_THM] 1286 \\ REVERSE (REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] \\ SRW_TAC [] []) 1287 THEN1 METIS_TAC [FMAP_11_def] 1288 \\ IMP_RES_TAC FDOM_sexp_abbrev_fmap_IMP \\ DECIDE_TAC); 1289 1290val string2sexp_sexp2abbrev = store_thm("string2sexp_sexp2abbrev", 1291 ``!exp abbrevs. string2sexp (sexp2abbrev exp abbrevs) = exp``, 1292 SIMP_TAC std_ss [string2sexp_def,sexp2abbrev_def,sexp_lex_sexp2abbrev_aux] 1293 \\ METIS_TAC [sexp_parse_aux_sexp2abbrevt,FMAP_11_sexp_abbrev_fmap,APPEND_NIL]); 1294 1295val string2sexp_sexp2string = store_thm("string2sexp_sexp2string", 1296 ``!exp. string2sexp (sexp2string exp) = exp``, 1297 ASM_SIMP_TAC std_ss [GSYM sexp2abbrev_NIL,string2sexp_sexp2abbrev]); 1298 1299 1300(* Part 2 - section 3: merge lexer and parser *) 1301 1302val next_token_IMP = prove( 1303 ``(((p,Val n),ds) = next_token cs) ==> LENGTH ds < LENGTH cs``, 1304 ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ REPEAT STRIP_TAC \\ IMP_RES_TAC next_token_LENGTH 1305 \\ FULL_SIMP_TAC std_ss [next_token_def,SExp_distinct]); 1306 1307val sexp_lex_parse_def = tDefine "sexp_lex_parse" ` 1308 (sexp_lex_parse (cs,s,L_READ,mem) = 1309 let (t,cs) = next_token cs in 1310 if SND t = Sym "NIL" then (Sym "NIL",cs) else (* error or end of input *) 1311 if SND t = Val 0 then sexp_lex_parse (cs,s,L_RETURN (FST t),mem) else 1312 if (t = ^TOKEN_OPEN) then sexp_lex_parse (cs,L_STOP::s,L_READ,mem) else 1313 if (t = ^TOKEN_DOT) then sexp_lex_parse (cs,L_DOT::s,L_READ,mem) else 1314 if (t = ^TOKEN_QUOTE) then sexp_lex_parse (cs,L_QUOTE::s,L_READ,mem) else 1315 if (t = ^TOKEN_CLOSE) then sexp_lex_parse (cs,s,L_COLLECT (Sym "NIL"),mem) else 1316 if ~isVal (FST t) then (Sym "NIL",cs) else 1317 if SND t = Val 3 then sexp_lex_parse (cs,s,L_RETURN (mem (getVal (FST t))),mem) else 1318 if SND t = Val 2 then sexp_lex_parse (cs,L_STORE (getVal (FST t))::s,L_READ,mem) else 1319 (Sym "NIL",cs)) /\ 1320 (sexp_lex_parse (cs,s,L_COLLECT exp,mem) = 1321 if s = [] then (Sym "NIL",cs) else 1322 let (x,s) = (HD s, TL s) in 1323 if x = L_STOP then sexp_lex_parse (cs,s,L_RETURN exp,mem) else 1324 if ~(READ_L_CONS x = NONE) then sexp_lex_parse (cs,s,L_COLLECT (Dot (THE (READ_L_CONS x)) exp),mem) else 1325 if x = L_DOT then sexp_lex_parse (cs,s,L_COLLECT (CAR exp),mem) else 1326 (Sym "NIL",cs)) /\ 1327 (sexp_lex_parse (cs,s,L_RETURN exp,mem) = 1328 if s = [] then (exp,cs) else 1329 let (x,s) = (HD s, TL s) in 1330 if x = L_QUOTE then sexp_lex_parse (cs,s,L_RETURN (Dot (Sym "QUOTE") (Dot exp (Sym "NIL"))),mem) else 1331 if ~(READ_L_STORE x = NONE) then sexp_lex_parse (cs,s,L_RETURN exp,(THE (READ_L_STORE x) =+ exp) mem) else 1332 sexp_lex_parse (cs,L_CONS exp::x::s,L_READ,mem))` 1333 (WF_REL_TAC `measure (\(cs,s,mode,mem). 1334 3 * LENGTH cs + LENGTH s + if mode = L_READ then 0 else 2)` 1335 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC NOT_NIL_IMP 1336 \\ IMP_RES_TAC next_token_IMP \\ FULL_SIMP_TAC (srw_ss()) [] \\ DECIDE_TAC); 1337 1338val sexp_parse_stream_def = Define ` 1339 sexp_parse_stream cs = sexp_lex_parse (cs,[],L_READ,\x.Sym "NIL")`; 1340 1341 1342(* 1343 1344val sexp_lex_parse_thm = prove( 1345 ``!cs ds s x mem. 1346 (~(ds = []) ==> MEM (HD ds) " )") ==> 1347 (sexp_lex_parse (cs++ds,s,x,mem) = 1348 (sexp_parse_aux (FST (sexp_lex (cs++ds)),s,x,mem),ds))``, 1349 1350val sexp_parse_stream_thm = store_thm("sexp_parse_stream_thm", 1351 ``!exp abbrevs s. 1352 (~(s = []) ==> MEM (HD s) " )") ==> 1353 (sexp_parse_stream (sexp2abbrev exp abbrevs ++ s) = (exp,s))``, 1354 SIMP_TAC std_ss [sexp_parse_stream_def] \\ REPEAT STRIP_TAC 1355 \\ IMP_RES_TAC sexp_lex_parse_thm \\ ASM_SIMP_TAC std_ss [] 1356 \\ ASM_SIMP_TAC std_ss [sexp2abbrev_def] 1357 \\ `?xs1 ps1. sexp2abbrev_aux exp T (sexp_abbrev_fmap abbrevs 0) {} = (xs1,ps1)` by METIS_TAC [PAIR] 1358 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (ASSUME_TAC o GSYM) 1359 \\ `?xs2 ps2. (xs2,ps2) = sexp2abbrevt_aux exp T (sexp_abbrev_fmap abbrevs 0) {}` by METIS_TAC [PAIR] 1360 \\ IMP_RES_TAC sexp2abbrev_aux_FST 1361 \\ ASM_SIMP_TAC std_ss [] 1362 \\ `xs2 = FST (sexp2abbrevt_aux exp T (sexp_abbrev_fmap abbrevs 0) {})` by 1363 (Cases_on `sexp2abbrevt_aux exp T (sexp_abbrev_fmap abbrevs 0) {}` 1364 \\ FULL_SIMP_TAC std_ss []) 1365 \\ ASM_SIMP_TAC std_ss [GSYM sexp_parse_def] 1366 \\ MATCH_MP_TAC sexp_parse_aux_sexp2abbrevt 1367 \\ ASM_SIMP_TAC std_ss [FMAP_11_sexp_abbrev_fmap]); 1368 1369*) 1370 1371val _ = export_theory(); 1372