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