1open HolKernel Parse boolLib bossLib; val _ = new_theory "lisp_bigops"; 2open lisp_codegenTheory lisp_initTheory lisp_symbolsTheory lisp_sexpTheory 3open lisp_invTheory lisp_parseTheory lisp_opsTheory; 4 5open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 6open combinTheory finite_mapTheory addressTheory helperLib; 7open set_sepTheory bitTheory fcpTheory stringTheory; 8 9open compilerLib decompilerLib codegenLib; 10 11val _ = let 12 val thms = DB.match [] ``SPEC X64_MODEL`` 13 val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms) 14 val _ = map (fn th => add_compiled [th] handle e => ()) thms 15 in () end; 16 17(* --- *) 18 19infix \\ 20val op \\ = op THEN; 21val RW = REWRITE_RULE; 22val RW1 = ONCE_REWRITE_RULE; 23 24(* 25val _ = set_echo 3; 26*) 27 28(* sex2string *) 29 30val (_,lisp_sexp2string_aux_extra_def,lisp_sexp2string_aux_extra_pre_def) = compile "x64" `` 31 lisp_sexp2string_aux_extra (x0,x2,xs:SExp list,io) = 32 if x2 = Sym "NIL" then (x0,x2,xs,io) else 33 let x0 = Sym "T" in 34 let xs = x0::xs in 35 let io = IO_WRITE io "(" in 36 (x0,x2,xs,io)`` 37 38val (_,lisp_sexp2string_aux_inner_def,lisp_sexp2string_aux_inner_pre_def) = compile "x64" `` 39 lisp_sexp2string_aux_inner (x0,x1,x2,x3:SExp,x4:SExp,x5:SExp,xs:SExp list,io) = 40 if isVal x0 then 41 let (x0,x1,x2,x3,io) = (Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL", IO_WRITE io (num2str (getVal x0))) in 42 (x0,x1,x2,x3,x4,x5,xs,io) 43 else if isSym x0 then 44 let (x0,x1,x2,x3,io) = (Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL", IO_WRITE io (sym2str (getSym x0))) in 45 (x0,x1,x2,x3,x4,x5,xs,io) 46 else 47 let x1 = x0 in 48 let x0 = LISP_TEST (isQuote x0) in 49 if ~(x0 = Sym "NIL") then 50 let io = IO_WRITE io "'" in 51 let x0 = CDR x1 in 52 let x0 = CAR x0 in 53 let x2 = Sym "T" in 54 lisp_sexp2string_aux_inner (x0,x1,x2,x3,x4,x5,xs,io) 55 else 56 let (x0,x2,xs,io) = lisp_sexp2string_aux_extra (x0,x2,xs,io) in 57 let x0 = CDR x1 in 58 let xs = x0::xs in 59 let x0 = Val 0 in 60 let xs = x0::xs in 61 let x0 = CAR x1 in 62 let x2 = Sym "T" in 63 lisp_sexp2string_aux_inner (x0,x1,x2,x3,x4,x5,xs,io)`` 64 65val (_,lisp_sexp2string_aux_space_def,lisp_sexp2string_aux_space_pre_def) = compile "x64" `` 66 lisp_sexp2string_aux_space (x0,io) = 67 if ~(isDot x0) then let io = IO_WRITE io " . " in (x0,io) else 68 let x0 = LISP_TEST (isQuote x0) in 69 if ~(x0 = Sym "NIL") then 70 let io = IO_WRITE io " . " in (x0,io) 71 else 72 let io = IO_WRITE io " " in (x0,io)`` 73 74val (_,lisp_sexp2string_aux_loop_def,lisp_sexp2string_aux_loop_pre_def) = compile "x64" `` 75 lisp_sexp2string_aux_loop (x0,x1,x2,x3,x4,x5,xs,io) = 76 if x3 = Sym "NIL" then 77 let (x0,x1,x2,x3,x4,x5,xs,io) = lisp_sexp2string_aux_inner (x0,x1,x2,x3,x4,x5,xs,io) in 78 let x3 = Sym "T" in 79 lisp_sexp2string_aux_loop (x0,x1,x2,x3,x4,x5,xs,io) 80 else 81 let x0 = HD xs in 82 let xs = TL xs in 83 if x0 = Sym "NIL" then (x0,x1,x2,x3,x4,x5,xs,io) else 84 if x0 = Sym "T" then 85 let io = IO_WRITE io ")" in 86 lisp_sexp2string_aux_loop (x0,x1,x2,x3,x4,x5,xs,io) 87 else 88 let x0 = HD xs in 89 let xs = TL xs in 90 if x0 = Sym "NIL" then 91 lisp_sexp2string_aux_loop (x0,x1,x2,x3,x4,x5,xs,io) 92 else 93 let x1 = x0 in 94 let (x0,io) = lisp_sexp2string_aux_space (x0,io) in 95 let x3 = Sym "NIL" in 96 let x2 = Sym "NIL" in 97 let x0 = x1 in 98 lisp_sexp2string_aux_loop (x0,x1,x2,x3,x4,x5,xs,io)`` 99 100val (lisp_sexp2string_spec,lisp_sexp2string_def,lisp_sexp2string_pre_def) = compile "x64" `` 101 lisp_sexp2string (x0,x1,x2,x3,x4,x5,xs,io) = 102 let xs = x0::xs in 103 let xs = x1::xs in 104 let xs = x2::xs in 105 let xs = x3::xs in 106 let x2 = Sym "T" in 107 let x3 = Sym "NIL" in 108 let xs = x3::xs in 109 let (x0,x1,x2,x3,x4,x5,xs,io) = lisp_sexp2string_aux_loop (x0,x1,x2,x3,x4,x5,xs,io) in 110 let x3 = HD xs in 111 let xs = TL xs in 112 let x2 = HD xs in 113 let xs = TL xs in 114 let x1 = HD xs in 115 let xs = TL xs in 116 let x0 = HD xs in 117 let xs = TL xs in 118 (x0,x1,x2,x3,x4,x5,xs,io)`` 119 120val T_NOT_NIL = CONJ (EVAL ``Sym "NIL" = Sym "T"``) (EVAL ``Sym "T" = Sym "NIL"``) 121 122val LISP_TEST_EQ_NIL = prove( 123 ``!b. (LISP_TEST b = Sym "NIL") = ~b``, 124 Cases \\ EVAL_TAC); 125 126val lisp_sexp2string_aux_loop_thm = prove( 127 ``!x0 x1 xs io b. 128 ?y0 y1 y2. 129 (lisp_sexp2string_aux_loop (x0,x1,LISP_TEST b,Sym "NIL",x4,x5,xs,io) = 130 lisp_sexp2string_aux_loop (y0,y1,y2,Sym "T",x4,x5,xs,IO_WRITE io (sexp2string_aux (x0,b)))) /\ 131 (lisp_sexp2string_aux_loop_pre (x0,x1,LISP_TEST b,Sym "NIL",x4,x5,xs,io) = 132 lisp_sexp2string_aux_loop_pre (y0,y1,y2,Sym "T",x4,x5,xs,IO_WRITE io (sexp2string_aux (x0,b))))``, 133 HO_MATCH_MP_TAC SExp_print_induct \\ REPEAT STRIP_TAC 134 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def] 135 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def] 136 \\ ONCE_REWRITE_TAC [lisp_sexp2string_aux_inner_def] 137 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_inner_pre_def] 138 \\ SIMP_TAC std_ss [LET_DEF] 139 \\ REVERSE (Cases_on `x0`) \\ ASM_SIMP_TAC std_ss [isSym_def,isVal_def,LET_DEF] 140 THEN1 (SIMP_TAC std_ss [isVal_def,isSym_def,LET_DEF,getSym_def, 141 sexp2string_aux_def] \\ METIS_TAC []) 142 THEN1 (SIMP_TAC std_ss [isVal_def,isSym_def,LET_DEF,getSym_def,getVal_def, 143 sexp2string_aux_def] \\ METIS_TAC []) 144 \\ FULL_SIMP_TAC std_ss [isDot_def,CAR_def,CDR_def] 145 \\ Cases_on `isQuote (Dot S' S0)` THEN1 146 (FULL_SIMP_TAC std_ss [LISP_TEST_def,EVAL ``Sym "T" = Sym "NIL"``] 147 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 148 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def] 149 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def] 150 \\ SIMP_TAC std_ss [LET_DEF] 151 \\ STRIP_TAC 152 \\ POP_ASSUM (MP_TAC o Q.SPECL [`Dot S' S0`,`xs`,`IO_WRITE io "'"`,`T`]) 153 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 154 \\ Q.LIST_EXISTS_TAC [`y0`,`y1`,`y2`] 155 \\ ONCE_REWRITE_TAC [sexp2string_aux_def] 156 \\ ASM_SIMP_TAC std_ss [LIST_STRCAT_def,IO_WRITE_APPEND,APPEND,APPEND_NIL] 157 \\ FULL_SIMP_TAC std_ss [isQuote_def,CDR_def,IO_WRITE_APPEND,APPEND]) 158 \\ ASM_SIMP_TAC std_ss [LISP_TEST_def] 159 \\ REVERSE (Cases_on `b`) THEN1 160 (FULL_SIMP_TAC std_ss [lisp_sexp2string_aux_extra_def] 161 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 162 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 163 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def] 164 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def] 165 \\ SIMP_TAC std_ss [LET_DEF] 166 \\ STRIP_TAC 167 \\ POP_ASSUM (MP_TAC o Q.SPECL [`Dot S' S0`,`Val 0::S0::xs`,`io`,`T`]) 168 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [LISP_TEST_def] 169 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def,LET_DEF,T_NOT_NIL] 170 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def,LET_DEF,T_NOT_NIL] 171 \\ SIMP_TAC std_ss [HD,TL,SExp_distinct] 172 \\ Cases_on `S0 = Sym "NIL"` \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL] 173 THEN1 (FULL_SIMP_TAC std_ss [sexp2string_aux_def,LET_DEF, 174 LIST_STRCAT_def,APPEND,APPEND_NIL] \\ METIS_TAC []) 175 \\ SIMP_TAC std_ss [lisp_sexp2string_aux_space_def,LET_DEF,IO_WRITE_APPEND] 176 \\ REVERSE (Cases_on `isDot S0`) \\ ASM_SIMP_TAC std_ss [] THEN1 177 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`xs`,`IO_WRITE io (STRCAT (sexp2string_aux (S',T)) " . ")`,`F`]) 178 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [IO_WRITE_APPEND,NOT_CONS_NIL, 179 sexp2string_aux_def,LET_DEF,LIST_STRCAT_def,APPEND,APPEND_NIL] 180 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] \\ METIS_TAC []) 181 \\ ASM_SIMP_TAC std_ss [LISP_TEST_EQ_NIL] 182 \\ Cases_on `isQuote S0` \\ FULL_SIMP_TAC std_ss [LISP_TEST_def] 183 THEN1 184 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`xs`,`IO_WRITE io (STRCAT (sexp2string_aux (S',T)) " . ")`,`F`]) 185 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [IO_WRITE_APPEND,NOT_CONS_NIL, 186 sexp2string_aux_def,LET_DEF,LIST_STRCAT_def,APPEND,APPEND_NIL] 187 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] \\ METIS_TAC []) 188 THEN1 189 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`xs`,`IO_WRITE io (STRCAT (sexp2string_aux (S',T)) " ")`,`F`]) 190 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [IO_WRITE_APPEND,NOT_CONS_NIL, 191 sexp2string_aux_def,LET_DEF,LIST_STRCAT_def,APPEND,APPEND_NIL] 192 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] \\ METIS_TAC [])) 193 THEN1 194 (FULL_SIMP_TAC std_ss [lisp_sexp2string_aux_extra_def,T_NOT_NIL] 195 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 196 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 197 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def] 198 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def] 199 \\ SIMP_TAC std_ss [LET_DEF] 200 \\ STRIP_TAC 201 \\ POP_ASSUM (MP_TAC o Q.SPECL [`Dot S' S0`,`Val 0::S0::Sym"T"::xs`,`IO_WRITE io "("`,`T`]) 202 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [LISP_TEST_def] 203 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def,LET_DEF,T_NOT_NIL] 204 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def,LET_DEF,T_NOT_NIL] 205 \\ SIMP_TAC std_ss [HD,TL,SExp_distinct] 206 \\ Cases_on `S0 = Sym "NIL"` \\ ASM_SIMP_TAC std_ss [] 207 THEN1 (SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def] 208 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def] 209 \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def,LET_DEF,TL,NOT_CONS_NIL, 210 LIST_STRCAT_def,APPEND,APPEND_NIL,T_NOT_NIL,HD,IO_WRITE_APPEND] 211 \\ METIS_TAC []) 212 \\ SIMP_TAC std_ss [lisp_sexp2string_aux_space_def,LET_DEF,IO_WRITE_APPEND] 213 \\ REVERSE (Cases_on `isDot S0`) \\ ASM_SIMP_TAC std_ss [] THEN1 214 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`Sym "T"::xs`,`IO_WRITE io (STRCAT "(" (STRCAT (sexp2string_aux (S',T)) " . "))`,`F`]) 215 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 216 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def] 217 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def] 218 \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def,LET_DEF,TL,NOT_CONS_NIL, 219 LIST_STRCAT_def,APPEND,APPEND_NIL,T_NOT_NIL,HD,IO_WRITE_APPEND] 220 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 221 \\ METIS_TAC []) 222 \\ ASM_SIMP_TAC std_ss [LISP_TEST_EQ_NIL] 223 \\ Cases_on `isQuote S0` \\ FULL_SIMP_TAC std_ss [LISP_TEST_def] 224 THEN1 225 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`Sym "T"::xs`,`IO_WRITE io (STRCAT "(" (STRCAT (sexp2string_aux (S',T)) " . "))`,`F`]) 226 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 227 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def] 228 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def] 229 \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def,LET_DEF,TL,NOT_CONS_NIL, 230 LIST_STRCAT_def,APPEND,APPEND_NIL,T_NOT_NIL,HD,IO_WRITE_APPEND] 231 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 232 \\ METIS_TAC []) 233 THEN1 234 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`Sym "T"::xs`,`IO_WRITE io (STRCAT "(" (STRCAT (sexp2string_aux (S',T)) " "))`,`F`]) 235 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 236 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_def] 237 \\ SIMP_TAC std_ss [Once lisp_sexp2string_aux_loop_pre_def] 238 \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def,LET_DEF,TL,NOT_CONS_NIL, 239 LIST_STRCAT_def,APPEND,APPEND_NIL,T_NOT_NIL,HD,IO_WRITE_APPEND] 240 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 241 \\ METIS_TAC []))); 242 243val lisp_sexp2string_thm = prove( 244 ``!x0 x1 x2 x3 x4 x5 xs io. 245 lisp_sexp2string_pre (x0,x1,x2,x3,x4,x5,xs,io) /\ 246 (lisp_sexp2string (x0,x1,x2,x3,x4,x5,xs,io) = 247 (x0,x1,x2,x3,x4,x5,xs,IO_WRITE io (sexp2string x0)))``, 248 SIMP_TAC std_ss [lisp_sexp2string_def,lisp_sexp2string_pre_def,LET_DEF] 249 \\ NTAC 8 STRIP_TAC 250 \\ STRIP_ASSUME_TAC (Q.SPECL [`x0`,`x1`,`Sym "NIL"::x3::x2::x1::x0::xs`,`io`,`T`] lisp_sexp2string_aux_loop_thm) 251 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [LISP_TEST_def] 252 \\ ONCE_REWRITE_TAC [lisp_sexp2string_aux_loop_def] 253 \\ ASM_SIMP_TAC std_ss [HD,T_NOT_NIL,LET_DEF,TL,HD,sexp2string_def] 254 \\ ONCE_REWRITE_TAC [lisp_sexp2string_aux_loop_pre_def] 255 \\ ASM_SIMP_TAC std_ss [HD,T_NOT_NIL,LET_DEF,TL,HD,sexp2string_def] 256 \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL]); 257 258 259 260(* string2sexp 261 262mem in x5 263exp in x4 264L_READ -- Sym "NIL" 265L_COLLECT -- Sym "T" 266L_RETURN -- Val 0 267 268*) 269 270val parse_task_def = Define ` 271 (parse_task L_READ = Sym "NIL") /\ 272 (parse_task (L_COLLECT x) = Sym "T") /\ 273 (parse_task (L_RETURN x) = Val 0)`; 274 275val parse_task2_def = Define ` 276 (parse_task2 L_READ y = y) /\ 277 (parse_task2 (L_COLLECT x) y = x) /\ 278 (parse_task2 (L_RETURN x) y = x)`; 279 280val parse_stack_def = Define ` 281 (parse_stack [] = [Sym "NIL"]) /\ 282 (parse_stack (L_CONS a::xs) = [Sym "CONS";a] ++ parse_stack xs) /\ 283 (parse_stack (L_STORE n::xs) = [Val n] ++ parse_stack xs) /\ 284 (parse_stack (L_STOP::xs) = [Sym "CAR"] ++ parse_stack xs) /\ 285 (parse_stack (L_DOT::xs) = [Sym "CDR"] ++ parse_stack xs) /\ 286 (parse_stack (L_QUOTE::xs) = [Sym "QUOTE"] ++ parse_stack xs)`; 287 288val remove_parse_stack_thm = prove( 289 ``!xs ys. (remove_parse_stack (parse_stack xs ++ ys) = ys)``, 290 Induct \\ SIMP_TAC std_ss [remove_parse_stack_def,parse_stack_def,APPEND] 291 \\ Cases \\ ASM_SIMP_TAC (srw_ss()) [remove_parse_stack_def,parse_stack_def,APPEND]) 292 293val (thm,lisp_token_def,lisp_token_pre_def) = compile "x64" `` 294 lisp_token (io) = 295 let (x0,x1,x2,x3,io) = (next_token1 (getINPUT io),next_token2 (getINPUT io),Sym "NIL", Sym "NIL",IO_INPUT_APPLY (SND o next_token) io) in 296 (x0,x1,x2,x3,io)`` 297 298val (thm,lisp_syntaxerr_def,lisp_syntaxerr_pre_def) = compile "x64" `` 299 lisp_syntaxerr (x0:SExp,xs) = 300 let xs = remove_parse_stack xs in 301 let x0 = Sym "NIL" in 302 (x0,xs)`` 303 304val (thm,lisp_parse_lookup_def,lisp_parse_lookup_pre_def) = compile "x64" `` 305 lisp_parse_lookup (x0,x2,x4) = 306 if ~(isDot x4) then let x4 = Sym "NIL" in (x0,x2,x4) else 307 let x2 = CAR x4 in 308 let x4 = CDR x4 in 309 if x0 = x2 then 310 let x4 = CAR x4 in (x0,x2,x4) 311 else 312 let x4 = CDR x4 in lisp_parse_lookup (x0,x2,x4)`` 313 314val (_,lisp_parse_def,lisp_parse_pre_def) = compile "x64" `` 315 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt:num) = 316 if x3 = Sym "NIL" then (* READ *) 317 let (x0,x1,x2,x3,io) = lisp_token io in 318 if x1 = Val 0 then 319 let x3 = x1 in 320 let x4 = x0 in 321 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 322 else if x1 = Val 1 then 323 if x0 = Val 0 then (* L_STOP *) 324 let x3 = Sym "NIL" in 325 let x0 = Sym "CAR" in 326 let xs = x0::xs in 327 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 328 else if x0 = Val 1 then (* L_DOT *) 329 let x3 = Sym "NIL" in 330 let x0 = Sym "CDR" in 331 let xs = x0::xs in 332 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 333 else if x0 = Val 3 then (* L_QUOTE *) 334 let x3 = Sym "NIL" in 335 let x0 = Sym "QUOTE" in 336 let xs = x0::xs in 337 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 338 else 339 let x3 = Sym "T" in 340 let x4 = Sym "NIL" in 341 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 342 else if x1 = Val 3 then 343 let x3 = Val 0 in 344 let x1 = Val amnt in 345 if getVal x0 < getVal x1 then 346 let x1 = x0 in 347 let x4 = EL (LENGTH xs + getVal x1 - xbp) xs in 348 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 349 else 350 let x4 = x5 in 351 let (x0,x2,x4) = lisp_parse_lookup (x0,x2,x4) in 352 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 353 else if x1 = Val 2 then 354 let x3 = Sym "NIL" in 355 let xs = x0::xs in 356 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 357 else 358 let (x0,xs) = lisp_syntaxerr (x0,xs) in 359 (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 360 else if x3 = Sym "T" then (* COLLECT *) 361 let x0 = HD xs in 362 if x0 = Sym "NIL" then 363 let (x0,xs) = lisp_syntaxerr (x0,xs) in 364 (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 365 else 366 let x0 = HD xs in 367 let xs = TL xs in 368 if x0 = Sym "CAR" then (* L_STOP *) 369 let x3 = Val 0 in 370 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 371 else if x0 = Sym "CONS" then (* L_CONS *) 372 let x1 = HD xs in 373 let xs = TL xs in 374 let x1 = Dot x1 x4 in 375 let x4 = x1 in 376 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 377 else if x0 = Sym "CDR" then (* L_DOT *) 378 let x4 = SAFE_CAR x4 in 379 let x3 = Sym "T" in 380 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 381 else 382 let xs = x0::xs in 383 let (x0,xs) = lisp_syntaxerr (x0,xs) in 384 (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 385 else (* RETURN *) 386 let x0 = HD xs in 387 if x0 = Sym "NIL" then 388 let xs = TL xs in 389 let x0 = x4 in 390 (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 391 else 392 let x0 = HD xs in 393 if x0 = Sym "QUOTE" then 394 let xs = TL xs in 395 let x1 = x4 in 396 let x2 = Sym "NIL" in 397 let x1 = Dot x1 x2 in 398 let x0 = Dot x0 x1 in 399 let x4 = x0 in 400 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 401 else if isVal x0 then 402 let xs = TL xs in 403 let x1 = Val amnt in 404 if getVal x0 < getVal x1 then 405 let x1 = x0 in 406 let x0 = x4 in 407 let xs = UPDATE_NTH (LENGTH xs + getVal x1 - xbp) x0 xs in 408 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 409 else 410 let x2 = x4 in 411 let x2 = Dot x2 x5 in 412 let x0 = Dot x0 x2 in 413 let x5 = x0 in 414 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) 415 else 416 let xs = x4::xs in 417 let x0 = Sym "CONS" in 418 let xs = x0::xs in 419 let x3 = Sym "NIL" in 420 lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt)`` 421 422val (_,lisp_pushes_def,lisp_pushes_pre_def) = compile "x64" `` 423 lisp_pushes (x0:SExp,x1,xs) = 424 if x1 = Val 0 then (x0,x1,xs) else 425 let x1 = LISP_SUB x1 (Val 1) in 426 let xs = x0::xs in 427 lisp_pushes (x0,x1,xs)`` 428 429val (lisp_string2sexp_spec,lisp_string2sexp_def,lisp_string2sexp_pre_def) = compile "x64" `` 430 lisp_string2sexp (x0,x1,x2,x3,x4,x5,xs,io,xbp:num,amnt) = 431 let xs = x1::xs in 432 let xs = x2::xs in 433 let xs = x3::xs in 434 let xs = x4::xs in 435 let xs = x5::xs in 436 let x3 = Sym "NIL" in 437 let x5 = x3 in 438 let x0 = x3 in 439 let x1 = Val amnt in 440 let (x0,x1,xs) = lisp_pushes (x0,x1,xs) in 441 let xbp = LENGTH xs in 442 let xs = x3::xs in 443 let (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) = lisp_parse (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) in 444 let x1 = Val amnt in 445 let xs = DROP (getVal x1) xs in 446 let x5 = HD xs in 447 let xs = TL xs in 448 let x4 = HD xs in 449 let xs = TL xs in 450 let x3 = HD xs in 451 let xs = TL xs in 452 let x2 = HD xs in 453 let xs = TL xs in 454 let x1 = HD xs in 455 let xs = TL xs in 456 let xbp = LENGTH xs in 457 (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt)`` 458 459val lisp_mem_def = tDefine "lisp_mem" ` 460 lisp_mem x = if ~(isDot x) then (\x. Sym "NIL") else 461 (getVal (CAR x) =+ CAR (CDR x)) (lisp_mem (CDR (CDR x)))` 462 (WF_REL_TAC `measure LSIZE` 463 \\ SIMP_TAC std_ss [isDot_thm] \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 464 \\ SIMP_TAC std_ss [CDR_def,LSIZE_def] \\ Cases_on `b` 465 \\ SIMP_TAC std_ss [CDR_def,LSIZE_def] \\ DECIDE_TAC) 466 467val READ_L_STORE_NONE_IMP = prove( 468 ``!h x. (READ_L_STORE h = SOME x) ==> (h = L_STORE x)``, 469 Cases \\ SIMP_TAC (srw_ss()) [READ_L_STORE_def]); 470 471val READ_L_CONS_NONE_IMP = prove( 472 ``!h x. (READ_L_CONS h = SOME x) ==> (h = L_CONS x)``, 473 Cases \\ SIMP_TAC (srw_ss()) [READ_L_CONS_def]); 474 475val getINPUT_REPLACE_INPUT_IO = prove( 476 ``!io x. getINPUT (REPLACE_INPUT_IO x io) = x``, 477 Cases \\ EVAL_TAC \\ SIMP_TAC std_ss []); 478 479val APPLY_REPLACE_INPUT_IO = prove( 480 ``!io cs f. IO_INPUT_APPLY f (REPLACE_INPUT_IO cs io) = 481 REPLACE_INPUT_IO (f cs) io``, 482 Cases \\ SIMP_TAC std_ss [REPLACE_INPUT_IO_def,IO_INPUT_APPLY_def,getINPUT_def]); 483 484val next_token_cases = prove( 485 ``!cs. (next_token cs = ((z1,z2),cs3)) ==> 486 ((z2 = Val 1) ==> (z1 = Val 0) \/ (z1 = Val 1) \/ (z1 = Val 2) \/ (z1 = Val 3)) /\ 487 ((z2 = Val 2) ==> isVal z1) /\ 488 ((z2 = Val 3) ==> isVal z1)``, 489 HO_MATCH_MP_TAC next_token_ind \\ SIMP_TAC std_ss [next_token_def,LET_DEF] \\ STRIP_TAC 490 THEN1 (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) []) 491 \\ NTAC 2 STRIP_TAC 492 \\ `?xs1 xs2. read_while number_char cs "" = (xs1,xs2)` by METIS_TAC [PAIR] 493 \\ `?ys1 ys2. str2sym (STRING c cs) = (ys1,ys2)` by METIS_TAC [PAIR] 494 \\ ASM_SIMP_TAC std_ss [] \\ Cases_on `c = #";"` 495 \\ FULL_SIMP_TAC (srw_ss()) [EVAL ``space_char #";"``, EVAL ``number_char #";"``] 496 \\ Cases_on `space_char c` \\ FULL_SIMP_TAC std_ss [] 497 \\ SIMP_TAC std_ss [Once EQ_SYM_EQ] \\ SRW_TAC [] [isVal_def]); 498 499val mem_list2sexp_def = Define ` 500 (mem_list2sexp [] = Sym "NIL") /\ 501 (mem_list2sexp ((n,x)::xs) = Dot (Val n) (Dot x (mem_list2sexp xs)))`; 502 503val ok_mem_sexp_def = Define ` 504 ok_mem_sexp s = ?xs. s = mem_list2sexp xs`; 505 506val EXISTS_IMP_RWT = METIS_PROVE [] ``((?x. P x) ==> Q) = !x. P x ==> Q`` 507 508val lisp_parse_lookup_thm = prove( 509 ``!y mem x a. 510 (lisp_mem y = mem) /\ ok_mem_sexp y ==> 511 ?x2. lisp_parse_lookup_pre (Val a,x,y) /\ 512 (lisp_parse_lookup (Val a,x,y) = (Val a,x2,mem a))``, 513 SIMP_TAC std_ss [ok_mem_sexp_def,EXISTS_IMP_RWT] \\ Induct_on `xs` 514 \\ SIMP_TAC std_ss [mem_list2sexp_def] THEN1 515 (ONCE_REWRITE_TAC [lisp_mem_def,lisp_parse_lookup_def,lisp_parse_lookup_pre_def] 516 \\ SIMP_TAC std_ss [isDot_def,LET_DEF]) 517 \\ Cases_on `h` \\ SIMP_TAC std_ss [mem_list2sexp_def] 518 \\ ONCE_REWRITE_TAC [lisp_mem_def,lisp_parse_lookup_def,lisp_parse_lookup_pre_def] 519 \\ SIMP_TAC (srw_ss()) [isDot_def,LET_DEF,CAR_def,CDR_def,getVal_def] 520 \\ REPEAT STRIP_TAC \\ Cases_on `a = q` 521 \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM,markerTheory.Abbrev_def]); 522 523val lisp_parse_mem_inv_def = Define ` 524 lisp_parse_mem_inv x5 mem xbp amnt xs ys = 525 (mem = \a. if a < amnt then EL a xs else lisp_mem x5 a) /\ 526 ok_mem_sexp x5 /\ (xbp = LENGTH (xs ++ ys)) /\ 527 (amnt = LENGTH xs)`; 528 529val UPDATE_NTH_APPEND = prove( 530 ``!xs ys n x. 531 UPDATE_NTH n x (xs ++ ys) = 532 if LENGTH xs <= n then xs ++ UPDATE_NTH (n - LENGTH xs) x ys 533 else UPDATE_NTH n x xs ++ ys``, 534 Induct \\ SIMP_TAC std_ss [LENGTH,APPEND] 535 \\ Cases_on `n` \\ ASM_SIMP_TAC std_ss [UPDATE_NTH_def,CONS_11,APPEND] 536 \\ METIS_TAC []); 537 538val LIST_UPDATE_NTH_def = Define ` 539 (LIST_UPDATE_NTH [] xs = xs) /\ 540 (LIST_UPDATE_NTH ((n,x)::ys) xs = LIST_UPDATE_NTH ys (UPDATE_NTH n x xs))`; 541 542val lisp_parse_thm = prove( 543 ``!cs s task mem. 544 (\(cs,s,task,mem). 545 !exp cs2 x0 x1 x2 x3 x4 x5 xs ys io xbp. 546 lisp_parse_mem_inv x5 mem xbp amnt xs ys /\ 547 ((exp,cs2) = sexp_lex_parse (cs,s,task,mem)) ==> 548 ?y0 y1 y2 y3 y4 y5 xs2. 549 lisp_parse_pre (x0,x1,x2,parse_task task,parse_task2 task x4,x5, 550 parse_stack s ++ xs ++ ys,REPLACE_INPUT_IO cs io,xbp,amnt:num) /\ 551 (lisp_parse (x0,x1,x2,parse_task task,parse_task2 task x4,x5, 552 parse_stack s ++ xs ++ ys,REPLACE_INPUT_IO cs io,xbp,amnt) = 553 (exp,y1,y2,y3,y4,y5,LIST_UPDATE_NTH xs2 xs ++ ys,REPLACE_INPUT_IO cs2 io,xbp,amnt))) (cs,s,task,mem)``, 554 555 HO_MATCH_MP_TAC sexp_lex_parse_ind \\ SIMP_TAC std_ss [] 556 \\ REVERSE (REPEAT STRIP_TAC) \\ POP_ASSUM MP_TAC THEN1 557 (SIMP_TAC std_ss [Once sexp_lex_parse_def,LET_DEF] 558 \\ Cases_on `s` \\ SIMP_TAC std_ss [parse_stack_def,APPEND,NOT_CONS_NIL] THEN1 559 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [parse_task_def,parse_task2_def] 560 \\ ONCE_REWRITE_TAC [lisp_parse_def] 561 \\ ONCE_REWRITE_TAC [lisp_parse_pre_def] 562 \\ SIMP_TAC std_ss [LET_DEF,HD,SExp_distinct,TL,NOT_CONS_NIL] 563 \\ Q.EXISTS_TAC `[]` \\ SIMP_TAC std_ss [LIST_UPDATE_NTH_def] \\ METIS_TAC []) 564 \\ FULL_SIMP_TAC std_ss [HD,TL] 565 \\ Cases_on `h = L_QUOTE` \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] THEN1 566 (FULL_SIMP_TAC std_ss [parse_task_def,parse_task2_def] 567 \\ ONCE_REWRITE_TAC [lisp_parse_def,lisp_parse_pre_def] 568 \\ SIMP_TAC std_ss [LET_DEF,HD,SExp_distinct,TL,parse_stack_def,APPEND] 569 \\ SIMP_TAC (srw_ss()) [] \\ STRIP_TAC 570 \\ Q.PAT_X_ASSUM `!exp.bbb` MATCH_MP_TAC 571 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 572 \\ Cases_on `READ_L_STORE h` THEN1 573 (FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 574 \\ ONCE_REWRITE_TAC [lisp_parse_def,lisp_parse_pre_def] 575 \\ FULL_SIMP_TAC std_ss [parse_task_def,parse_task2_def] 576 \\ FULL_SIMP_TAC std_ss [LET_DEF,HD,SExp_distinct,TL,parse_stack_def,APPEND] 577 \\ `~(HD (parse_stack (h::t) ++ xs ++ ys) = Sym "NIL") /\ 578 ~(HD (parse_stack (h::t) ++ xs ++ ys) = Sym "QUOTE") /\ 579 ~isVal (HD (parse_stack (h::t) ++ xs ++ ys)) /\ 580 ~(parse_stack (h::t) ++ xs ++ ys = [])` by 581 (Cases_on `h` \\ FULL_SIMP_TAC (srw_ss()) 582 [parse_stack_def,APPEND,isVal_def,READ_L_STORE_def]) 583 \\ ASM_SIMP_TAC std_ss []) 584 \\ FULL_SIMP_TAC (srw_ss()) [] 585 \\ IMP_RES_TAC READ_L_STORE_NONE_IMP 586 \\ FULL_SIMP_TAC (srw_ss()) [parse_stack_def] 587 \\ FULL_SIMP_TAC std_ss [parse_task_def,parse_task2_def] 588 \\ ONCE_REWRITE_TAC [lisp_parse_def,lisp_parse_pre_def] 589 \\ FULL_SIMP_TAC std_ss [LET_DEF,HD,SExp_distinct,TL,parse_stack_def,APPEND,isVal_def] 590 \\ FULL_SIMP_TAC std_ss [getVal_def] 591 \\ Cases_on `x < amnt` \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL] THEN1 592 (`(amnt = LENGTH xs) /\ 593 (xbp = LENGTH (xs ++ ys))` by FULL_SIMP_TAC std_ss [lisp_parse_mem_inv_def] 594 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND] 595 \\ `LENGTH (parse_stack t) + LENGTH xs + LENGTH ys + x - 596 (LENGTH xs + LENGTH ys) = LENGTH (parse_stack t) + x` by DECIDE_TAC 597 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 598 \\ `~(LENGTH xs <= x) /\ x < LENGTH xs + LENGTH ys` by DECIDE_TAC 599 \\ ASM_SIMP_TAC std_ss [UPDATE_NTH_APPEND] 600 \\ ASM_SIMP_TAC std_ss [APPEND_ASSOC] 601 \\ `lisp_parse_mem_inv x5 ((x =+ exp) mem) (LENGTH xs + LENGTH ys) amnt (UPDATE_NTH x exp xs) ys` by 602 (FULL_SIMP_TAC std_ss [lisp_parse_mem_inv_def,LENGTH_APPEND, 603 LENGTH_UPDATE_NTH,FUN_EQ_THM,APPLY_UPDATE_THM,EL_UPDATE_NTH] 604 \\ METIS_TAC []) 605 \\ `LENGTH xs = LENGTH (UPDATE_NTH x exp xs)` by SIMP_TAC std_ss [LENGTH_UPDATE_NTH] 606 \\ POP_ASSUM (fn th => SIMP_TAC std_ss [th]) 607 \\ REPEAT STRIP_TAC 608 \\ Q.PAT_X_ASSUM `!expp.bbb` (MP_TAC o Q.SPECL [`exp'`,`cs2`,`exp`,`Val x`, 609 `x2`,`x5`,`UPDATE_NTH x exp xs`,`ys`,`io`,`LENGTH (xs:SExp list) + LENGTH (ys:SExp list)`]) 610 \\ ASM_SIMP_TAC std_ss [] \\ SIMP_TAC std_ss [LENGTH_UPDATE_NTH] 611 \\ METIS_TAC [LIST_UPDATE_NTH_def]) 612 \\ REPEAT STRIP_TAC 613 \\ `lisp_parse_mem_inv (Dot (Val x) (Dot exp x5)) ((x =+ exp) mem) xbp amnt xs ys` by 614 (FULL_SIMP_TAC std_ss [lisp_parse_mem_inv_def] 615 \\ FULL_SIMP_TAC std_ss [ok_mem_sexp_def] 616 \\ REVERSE (REPEAT STRIP_TAC) 617 THEN1 (Q.EXISTS_TAC `(x,exp)::xs'` \\ FULL_SIMP_TAC std_ss [mem_list2sexp_def]) 618 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] 619 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [Once lisp_mem_def] 620 \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def,getVal_def,APPLY_UPDATE_THM,isDot_def] 621 \\ METIS_TAC []) 622 \\ RES_TAC \\ POP_ASSUM (K ALL_TAC) \\ POP_ASSUM MP_TAC 623 \\ ASM_SIMP_TAC std_ss []) 624 THEN1 625 (SIMP_TAC std_ss [Once sexp_lex_parse_def,LET_DEF] 626 \\ Cases_on `s` \\ SIMP_TAC std_ss [parse_stack_def,APPEND,NOT_CONS_NIL] THEN1 627 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [parse_task_def,parse_task2_def] 628 \\ ONCE_REWRITE_TAC [lisp_parse_def] 629 \\ ONCE_REWRITE_TAC [lisp_parse_pre_def] 630 \\ SIMP_TAC (srw_ss()) [LET_DEF,HD,SExp_distinct,TL,NOT_CONS_NIL] 631 \\ `remove_parse_stack (parse_stack [] ++ xs ++ ys) = xs ++ ys` by 632 FULL_SIMP_TAC std_ss [remove_parse_stack_thm,GSYM APPEND_ASSOC] 633 \\ FULL_SIMP_TAC std_ss [parse_stack_def,APPEND,LET_DEF,lisp_syntaxerr_def] 634 \\ Q.EXISTS_TAC `[]` \\ SIMP_TAC std_ss [LIST_UPDATE_NTH_def] \\ METIS_TAC []) 635 \\ FULL_SIMP_TAC std_ss [HD,TL] 636 \\ Cases_on `h = L_STOP` \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] THEN1 637 (FULL_SIMP_TAC std_ss [parse_task_def,parse_task2_def] 638 \\ ONCE_REWRITE_TAC [lisp_parse_def,lisp_parse_pre_def] 639 \\ SIMP_TAC std_ss [LET_DEF,HD,SExp_distinct,TL,parse_stack_def,APPEND] 640 \\ SIMP_TAC (srw_ss()) [] \\ STRIP_TAC 641 \\ Q.PAT_X_ASSUM `!exp.bbb` MATCH_MP_TAC \\ ASM_SIMP_TAC std_ss []) 642 \\ REVERSE (Cases_on `READ_L_CONS h`) THEN1 643 (IMP_RES_TAC READ_L_CONS_NONE_IMP 644 \\ FULL_SIMP_TAC (srw_ss()) [parse_stack_def] 645 \\ FULL_SIMP_TAC std_ss [parse_task_def,parse_task2_def] 646 \\ ONCE_REWRITE_TAC [lisp_parse_def,lisp_parse_pre_def] 647 \\ FULL_SIMP_TAC (srw_ss()) [LET_DEF,HD,SExp_distinct,TL, 648 parse_stack_def,APPEND,isVal_def]) 649 \\ Cases_on `h = L_DOT` \\ ASM_SIMP_TAC std_ss [] THEN1 650 (FULL_SIMP_TAC (srw_ss()) [parse_stack_def] 651 \\ FULL_SIMP_TAC std_ss [parse_task_def,parse_task2_def] 652 \\ ONCE_REWRITE_TAC [lisp_parse_def,lisp_parse_pre_def] 653 \\ FULL_SIMP_TAC (srw_ss()) [LET_DEF,HD,SExp_distinct,TL, 654 parse_stack_def,APPEND,isVal_def,SAFE_CAR_def]) 655 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [parse_task2_def] 656 \\ ONCE_REWRITE_TAC [lisp_parse_def] 657 \\ ONCE_REWRITE_TAC [lisp_parse_pre_def] 658 \\ `~(HD (parse_stack (h::t) ++ xs ++ ys) = Sym "NIL") /\ 659 ~(HD (parse_stack (h::t) ++ xs ++ ys) = Sym "CONS") /\ 660 ~(HD (parse_stack (h::t) ++ xs ++ ys) = Sym "CAR") /\ 661 ~(HD (parse_stack (h::t) ++ xs ++ ys) = Sym "CDR") /\ 662 ~(parse_stack (h::t) = [])` by 663 (Cases_on `h` \\ FULL_SIMP_TAC (srw_ss()) [HD, 664 parse_stack_def,APPEND,isVal_def,READ_L_CONS_def]) 665 \\ ASM_SIMP_TAC (srw_ss()) [LET_DEF,HD,SExp_distinct,TL, 666 NOT_CONS_NIL,parse_task_def,lisp_syntaxerr_def] 667 \\ `HD (parse_stack (h::t) ++ xs ++ ys)::TL (parse_stack (h::t) ++ xs ++ ys) = 668 parse_stack (h::t) ++ xs ++ ys` by 669 (Cases_on `parse_stack (h::t)` \\ FULL_SIMP_TAC std_ss [HD,TL,APPEND]) 670 \\ ASM_SIMP_TAC std_ss [remove_parse_stack_thm,GSYM APPEND_ASSOC] 671 \\ Q.EXISTS_TAC `[]` \\ ASM_SIMP_TAC std_ss [LIST_UPDATE_NTH_def]) 672 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [parse_task_def] 673 \\ ONCE_REWRITE_TAC [lisp_parse_def] 674 \\ ONCE_REWRITE_TAC [lisp_parse_pre_def] 675 \\ ASM_SIMP_TAC (srw_ss()) [LET_DEF,HD,SExp_distinct,TL, 676 NOT_CONS_NIL,parse_task_def,lisp_syntaxerr_def,lisp_token_def] 677 \\ ASM_SIMP_TAC std_ss [getINPUT_REPLACE_INPUT_IO,next_token1_def,next_token2_def] 678 \\ `?cs3 z1 z2. next_token cs = ((z1,z2),cs3)` by METIS_TAC [PAIR] 679 \\ FULL_SIMP_TAC std_ss [] 680 \\ `~(parse_stack s = [])` by 681 (Cases_on `s` \\ SIMP_TAC std_ss [parse_stack_def,NOT_CONS_NIL] 682 \\ Cases_on `h` \\ SIMP_TAC std_ss [parse_stack_def,NOT_CONS_NIL,APPEND]) 683 \\ Cases_on `z2 = Val 0` \\ FULL_SIMP_TAC (srw_ss()) [parse_task2_def] 684 THEN1 685 (Q.PAT_X_ASSUM `(exp,cs2) = xxx` MP_TAC \\ ONCE_REWRITE_TAC [sexp_lex_parse_def] 686 \\ FULL_SIMP_TAC (srw_ss()) [APPLY_REPLACE_INPUT_IO,LET_DEF] \\ METIS_TAC []) 687 \\ Cases_on `z2 = Val 1` \\ FULL_SIMP_TAC (srw_ss()) [parse_task2_def] THEN1 688 (Cases_on `z1 = Val 0` \\ FULL_SIMP_TAC (srw_ss()) [parse_task2_def, 689 parse_stack_def,APPLY_REPLACE_INPUT_IO] THEN1 690 (Q.PAT_X_ASSUM `(exp,cs2) = xxx` MP_TAC \\ ONCE_REWRITE_TAC [sexp_lex_parse_def] 691 \\ FULL_SIMP_TAC (srw_ss()) [APPLY_REPLACE_INPUT_IO,LET_DEF] \\ METIS_TAC []) 692 \\ Cases_on `z1 = Val 1` \\ FULL_SIMP_TAC (srw_ss()) [parse_task2_def, 693 parse_stack_def,APPLY_REPLACE_INPUT_IO] THEN1 694 (Q.PAT_X_ASSUM `(exp,cs2) = xxx` MP_TAC \\ ONCE_REWRITE_TAC [sexp_lex_parse_def] 695 \\ FULL_SIMP_TAC (srw_ss()) [APPLY_REPLACE_INPUT_IO,LET_DEF] \\ METIS_TAC []) 696 \\ Cases_on `z1 = Val 3` \\ FULL_SIMP_TAC (srw_ss()) [parse_task2_def, 697 parse_stack_def,APPLY_REPLACE_INPUT_IO] THEN1 698 (Q.PAT_X_ASSUM `(exp,cs2) = xxx` MP_TAC \\ ONCE_REWRITE_TAC [sexp_lex_parse_def] 699 \\ FULL_SIMP_TAC (srw_ss()) [APPLY_REPLACE_INPUT_IO,LET_DEF] \\ METIS_TAC []) 700 \\ `z1 = Val 2` by METIS_TAC [next_token_cases] 701 \\ FULL_SIMP_TAC (srw_ss()) [parse_task2_def, 702 parse_stack_def,APPLY_REPLACE_INPUT_IO] 703 \\ Q.PAT_X_ASSUM `(exp,cs2) = xxx` MP_TAC \\ ONCE_REWRITE_TAC [sexp_lex_parse_def] 704 \\ FULL_SIMP_TAC (srw_ss()) [APPLY_REPLACE_INPUT_IO,LET_DEF] \\ METIS_TAC []) 705 \\ Cases_on `z2 = Val 2` \\ FULL_SIMP_TAC (srw_ss()) [parse_task2_def] THEN1 706 (Q.PAT_X_ASSUM `(exp,cs2) = xxx` MP_TAC \\ ONCE_REWRITE_TAC [sexp_lex_parse_def] 707 \\ FULL_SIMP_TAC (srw_ss()) [APPLY_REPLACE_INPUT_IO,LET_DEF] 708 \\ `isVal z1` by METIS_TAC [next_token_cases] 709 \\ FULL_SIMP_TAC (srw_ss()) [isVal_thm,getVal_def] 710 \\ FULL_SIMP_TAC (srw_ss()) [parse_task2_def, 711 parse_stack_def,APPLY_REPLACE_INPUT_IO,getVal_def] \\ METIS_TAC []) 712 \\ Cases_on `z2 = Val 3` \\ FULL_SIMP_TAC (srw_ss()) [parse_task2_def] THEN1 713 (Q.PAT_X_ASSUM `(exp,cs2) = xxx` MP_TAC \\ ONCE_REWRITE_TAC [sexp_lex_parse_def] 714 \\ FULL_SIMP_TAC (srw_ss()) [APPLY_REPLACE_INPUT_IO,LET_DEF] 715 \\ `isVal z1` by METIS_TAC [next_token_cases] 716 \\ FULL_SIMP_TAC (srw_ss()) [isVal_thm,getVal_def] 717 \\ FULL_SIMP_TAC (srw_ss()) [isVal_thm,getVal_def] 718 \\ Cases_on `a < amnt` \\ ASM_SIMP_TAC std_ss [] THEN1 719 (`(amnt = LENGTH xs) /\ 720 (xbp = LENGTH (xs ++ ys))` by FULL_SIMP_TAC std_ss [lisp_parse_mem_inv_def] 721 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND] 722 \\ `LENGTH (parse_stack s) + LENGTH xs + LENGTH ys + a - 723 (LENGTH xs + LENGTH ys) = LENGTH (parse_stack s) + a` by DECIDE_TAC 724 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 725 \\ `LENGTH (parse_stack s) <= LENGTH (parse_stack s) + a` by DECIDE_TAC 726 \\ ASM_SIMP_TAC std_ss [rich_listTheory.EL_APPEND2,rich_listTheory.EL_APPEND1] 727 \\ `EL a xs = mem a` by FULL_SIMP_TAC std_ss [lisp_parse_mem_inv_def] 728 \\ `a < LENGTH xs + LENGTH ys` by DECIDE_TAC 729 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC]) 730 \\ `ok_mem_sexp x5` by FULL_SIMP_TAC std_ss [lisp_parse_mem_inv_def] 731 \\ IMP_RES_TAC (SIMP_RULE std_ss [] lisp_parse_lookup_thm) 732 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`Sym "NIL"`,`a`]) 733 \\ ASM_SIMP_TAC std_ss [] 734 \\ `lisp_mem x5 a = mem a` by 735 (FULL_SIMP_TAC std_ss [lisp_parse_mem_inv_def] \\ METIS_TAC []) 736 \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 737 \\ Q.PAT_X_ASSUM `(exp,cs2) = xxx` MP_TAC \\ ONCE_REWRITE_TAC [sexp_lex_parse_def] 738 \\ FULL_SIMP_TAC (srw_ss()) [APPLY_REPLACE_INPUT_IO,LET_DEF] 739 \\ FULL_SIMP_TAC std_ss [remove_parse_stack_thm,GSYM APPEND_ASSOC] 740 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `[]` 741 \\ ASM_SIMP_TAC std_ss [LIST_UPDATE_NTH_def] \\ METIS_TAC []) 742 |> SIMP_RULE std_ss []; 743 744val lisp_pushes_thm = prove( 745 ``!n x xs. lisp_pushes_pre (x,Val n,xs) /\ 746 (lisp_pushes (x,Val n,xs) = (x,Val 0,GENLIST (\a.x) n ++ xs))``, 747 Induct \\ ONCE_REWRITE_TAC [lisp_pushes_def,lisp_pushes_pre_def] 748 \\ ASM_SIMP_TAC (srw_ss()) [GENLIST,APPEND,LET_DEF,LISP_SUB_def,getVal_def,isVal_def]); 749 750val read_sexp_def = Define ` 751 read_sexp io = FST (sexp_parse_stream (getINPUT io))`; 752 753val next_sexp_def = Define ` 754 next_sexp io = IO_INPUT_APPLY (SND o sexp_parse_stream) io`; 755 756val LENGTH_LIST_UPDATE_NTH = prove( 757 ``!xs ys. LENGTH (LIST_UPDATE_NTH xs ys) = LENGTH ys``, 758 Induct \\ SIMP_TAC std_ss [LIST_UPDATE_NTH_def] 759 \\ Cases \\ ASM_SIMP_TAC std_ss [LIST_UPDATE_NTH_def,LENGTH_UPDATE_NTH]); 760 761val lisp_string2sexp_thm = prove( 762 ``!x0 x1 x2 x3 x4 x5 xs io. 763 lisp_string2sexp_pre (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) /\ 764 (lisp_string2sexp (x0,x1,x2,x3,x4,x5,xs,io,xbp,amnt) = 765 (read_sexp io,x1,x2,x3,x4,x5,xs,next_sexp io,LENGTH xs,amnt))``, 766 SIMP_TAC std_ss [lisp_string2sexp_def,lisp_string2sexp_pre_def,LET_DEF] 767 \\ NTAC 7 STRIP_TAC \\ ASM_SIMP_TAC std_ss [lisp_pushes_thm] 768 \\ `?exp cs2. ((exp,cs2) = sexp_lex_parse (getINPUT io,[],L_READ,lisp_mem (Sym "NIL")))` by METIS_TAC [PAIR] 769 \\ MP_TAC (Q.SPECL [`getINPUT io`,`[]`,`L_READ`,`\x.Sym "NIL"`,`exp`,`cs2`,`Sym "NIL"`,`Val 0`,`x2`,`x4`,`Sym "NIL"`,`GENLIST (\a. Sym "NIL") amnt`,`x5::x4::x3::x2::x1::xs`,`io`,`LENGTH 770 (GENLIST (\a. Sym "NIL") amnt ++ 771 x5::x4::x3::x2::x1::xs)`] lisp_parse_thm) 772 \\ ASM_SIMP_TAC std_ss [parse_stack_def,APPEND] 773 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 774 (SIMP_TAC std_ss [lisp_parse_mem_inv_def,LENGTH_GENLIST] 775 \\ ONCE_REWRITE_TAC [lisp_mem_def] \\ SIMP_TAC std_ss [isDot_def] 776 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ REPEAT STRIP_TAC 777 \\ FULL_SIMP_TAC std_ss [EL_GENLIST] 778 \\ SIMP_TAC std_ss [ok_mem_sexp_def] \\ Q.EXISTS_TAC `[]` \\ EVAL_TAC) 779 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [parse_task_def,parse_task2_def] 780 \\ FULL_SIMP_TAC std_ss [IO_INPUT_LEMMA,NOT_CONS_NIL,CONS_11,TL,HD,getVal_def] 781 \\ Q.ABBREV_TAC `zs = (DROP amnt (LIST_UPDATE_NTH xs2 782 (GENLIST (\a. Sym "NIL") amnt) ++ x5::x4::x3::x2::x1::xs))` 783 \\ `zs = x5::x4::x3::x2::x1::xs` by 784 (`amnt = LENGTH (LIST_UPDATE_NTH xs2 (GENLIST (\a. Sym "NIL") amnt))` by 785 ASM_SIMP_TAC std_ss [LENGTH_LIST_UPDATE_NTH,LENGTH_GENLIST] 786 \\ Q.UNABBREV_TAC `zs` \\ POP_ASSUM (fn th => SIMP_TAC std_ss [Once th]) 787 \\ SIMP_TAC std_ss [rich_listTheory.BUTFIRSTN_LENGTH_APPEND]) 788 \\ ASM_SIMP_TAC std_ss [TL,HD,NOT_CONS_NIL,isVal_def] 789 \\ ASM_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH_LIST_UPDATE_NTH,LENGTH_GENLIST] 790 \\ Q.PAT_X_ASSUM `(exp,cs2) = xxx` (MP_TAC o GSYM) 791 \\ ASM_SIMP_TAC std_ss [read_sexp_def,next_sexp_def,sexp_parse_stream_def] 792 \\ Cases_on `io` \\ FULL_SIMP_TAC std_ss [IO_INPUT_APPLY_def,getINPUT_def, 793 REPLACE_INPUT_IO_def,sexp_parse_stream_def] 794 \\ ONCE_REWRITE_TAC [lisp_mem_def] \\ STRIP_TAC 795 \\ FULL_SIMP_TAC std_ss [isDot_def]); 796 797 798fun abbrev_code (th,jump,def_name) = let 799 val INSERT_UNION_INSERT = prove( 800 ``x INSERT (y UNION (z INSERT t)) = x INSERT z INSERT (y UNION t)``, 801 SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_UNION] \\ METIS_TAC []); 802 fun mk_tuple [] = fail() 803 | mk_tuple [x] = x 804 | mk_tuple (x::xs) = pairSyntax.mk_pair(x,mk_tuple xs) 805 val th = th 806 |> SIMP_RULE std_ss [lisp_string2sexp_thm,LET_DEF,SEP_CLAUSES] 807 |> SIMP_RULE std_ss [INSERT_UNION_INSERT,INSERT_UNION_EQ,UNION_EMPTY, 808 GSYM UNION_ASSOC,UNION_IDEMPOT] 809 val th = Q.INST [`qs`|->`q::qs`] th 810 val th = SPEC_COMPOSE_RULE [th,X64_LISP_RET] 811 val (_,_,c,_) = dest_spec (concl th) 812 val input = mk_tuple (free_vars c) 813 val ty = type_of (pairSyntax.mk_pabs(input,c)) 814 val name = mk_var(def_name,ty) 815 val def = Define [ANTIQUOTE (mk_eq(mk_comb(name,input),c))] 816 val th = RW [GSYM def] th 817 val th = SPEC_COMPOSE_RULE [jump,th] 818 in th end; 819 820 821val X64_LISP_PARSE_SEXP = save_thm("X64_LISP_PARSE_SEXP",let 822 val th = lisp_string2sexp_spec 823 val jump = X64_LISP_CALL_EL3 824 val def_name = "abbrev_code_for_parse" 825 val th = abbrev_code (th,jump,def_name) 826 val _ = add_compiled [th] 827 in th end); 828 829val X64_LISP_PRINT_SEXP = save_thm("X64_LISP_PRINT_SEXP",let 830 val th = SIMP_RULE std_ss [lisp_sexp2string_thm,LET_DEF,SEP_CLAUSES] lisp_sexp2string_spec 831 val jump = X64_LISP_CALL_EL7 832 val def_name = "abbrev_code_for_print" 833 val th = abbrev_code (th,jump,def_name) 834 val _ = add_compiled [th] 835 in th end); 836 837 838val _ = export_theory(); 839 840