machine-code/lisp/lisp_parseScript.sml

219     let r7 = r5:word32 in
221     let r8 = r5 - r7 in
222       (r4,r5,r7,r8,df,f)``
276   arm_streq (r4:word32,r5:word32,r6:word32,r7:word32,df:word32 set,dg:word32 set,f:word32->word8,g:word32->word8) =
277     if r7 = 0x0w then
278       (let r5 = r7 + r5 in (r4,r5,r6,r7,df,dg,f,g))
283            (let r7 = r7 - 0x1w in
285               arm_streq (r4,r5,r6,r7,df,dg,f,g))
287            (let r5 = r7 + r5 in (r4,r5,r6,r7,df,dg,f,g)))``
405      let r7 = r8 + 0x3w in
406      let r7 = r7 >>> 2 in
407      let r7 = r7 << 2 in
408      let r7 = r7 + r3 in
409      let r7 = r7 + 0x8w in
410      let m = (r3 + 0x4w =+ r7) m in
412      let m = (r7 =+ r6) m in
415        (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m))``
493          (let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) =
496             (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m))
499            (let r7 = r8 in
501             let (r4,r5,r6,r7,df,dg,f,g) =
502                   arm_streq (r4,r5,r6,r7,df,dg,f,g)
504               if r7 = 0x0w then
505                 (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m)
663     (let r7 = r5 in
665      let r8 = r5 - r7 in
667      let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) =
671        (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m))``;
701   arm_number_symbol (r9,r3,r4,r5,r7,r8,df,dg,dh:word32 set,dm,f,g,h:word32->word32,m) =
704         (let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) =
712            (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))
718            (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))
720       (let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) =
728          (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))``;
745   arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
747       (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m)
754               let (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
756                       (r9,r3,r4,r5,r7,r8,df,dg,dh,dm,f,g,h,m)
759                 arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))
766                   (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m)))
770            arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))``;
892   ``!s r1 r3 k r6 r7 r8 p x xs df dg dh dm f g h m.
899         arm_lexer_pre (r1,r3,w2w (f k),k,r6,r7,r8,df,dg,dh,dm,f,g,h,m) /\
900         (arm_lexer (r1,r3,w2w (f k),k,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
929     \\ RES_TAC \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`r8`,`r7`,`r6`])
958         [`r1+8w`,`r3`,`k+1w`,`y2`,`r7`,`r8`,`p * one (r1,y2) * one (r1 + 0x4w,y')`,`x`,`xs`,`df`,`dg`,`dh`,`dm`,`f`,`g`,`(r1 =+ y2) h'`,`m`])
1026          [`r1+8w`,`r3`,`x'`,`y`,`r7`,`r8`,`p * one (r1,n) * one (r1 + 0x4w,r3)`,`x`,`xs`,`df`,`dg`,`dh`,`dm`,`f`,`g`,`(r1 =+ n) ((r1 + 4w =+ r3) h')`,`m`])
1450   arm_parse1 (r4:word32,r7:word32,r8:word32,dh:word32 set,h:word32->word32) =
1451     let h = (r4 =+ r7) h in
1453     let r7 = 0x3w in
1455       (r4:word32,r7:word32,r8:word32,dh,h)``
1458   arm_parse2 (r4:word32,r6:word32,r7:word32,r8,dh:word32 set,h:word32->word32) =
1461        let h = (r4 =+ r7) h in
1462        let r7 = r8 in
1466        let h = (r7 =+ r6) h in
1467        let h = (r7 + 0x4w =+ r6) h in
1468        let r7 = r4 in
1469          (r4,r6,r7,r8,dh,h))
1474          (r4,r6,r7,r8,dh,h))``
1477   arm_parse3 (r4:word32,r7:word32,dh:word32 set,h:word32->word32) =
1478     (if r7 && 3w = 0x0w then
1479        (let r6 = r7 in
1480         let r7 = h r7 in
1486           (r4,r6,r7,dh,h))
1491           (r4,r6,r7,dh,h)))``
1494   arm_parse4 (r4:word32,r5:word32,r7:word32,dh:word32 set,h:word32->word32) =
1495     if r7 && 3w = 0x0w then
1496       (let r6 = h r7 in
1504        let h = (r7 =+ r4) h in
1505          (r4,r5,r6,r7,dh,h))
1513          (r4,r5,r6,r7,dh,h))``;
1516   arm_parse_next (r4,r5,r6,r7,r8,dh,h) =
1519         (let (r4,r7,r8,dh,h) = arm_parse1 (r4,r7,r8,dh,h)
1520          in (r4,r5,r6,r7,r8,dh,h))
1523           (let (r4,r6,r7,r8,dh,h) = arm_parse2 (r4,r6,r7,r8,dh,h)
1524            in (r4,r5,r6,r7,r8,dh,h))
1527             (let (r4,r6,r7,dh,h) = arm_parse3 (r4,r7,dh,h)
1528              in (r4,r5,r6,r7,r8,dh,h))
1530             (let (r4,r5,r6,r7,dh,h) = arm_parse4 (r4,r5,r7,dh,h)
1531              in (r4,r5,r6,r7,r8,dh,h))
1533       (let h = (r4 + 0x4w =+ r7) h in
1534        let r7 = r4 in
1535          (r4,r5,r6,r7,r8,dh,h))``
1538   arm_parse_loop1 (r4,r5,r6,r7,r8,dh:word32 set,h:word32->word32) =
1540       if r7 && 3w = 0w then
1542         let r8 = r7 in
1543         let r7 = h r7 in
1545           (r4,r5,r6,r7,r8,dh,h)
1547         (r4,r5,r6,r7,r8,dh,h)
1549       let (r4,r5,r6,r7,r8,dh,h) = arm_parse_next (r4,r5,r6,r7,r8,dh,h) in
1552         arm_parse_loop1 (r4,r5,r6,r7,r8,dh,h)``;
1685   ``!xs r4 r5 r7 r8 df f d1 d2 d3 exp stack p.
1688       (ALIGNED r7 ==> ALIGNED8 (b - r7)) /\
1689       (arm_tokens4 r4 xs b d y * arm_tokens3 (r5 + 8w) xs q * lisp_exp exp r7 (b,d) *
1694         arm_parse_loop1_pre (r4,r5,f r4,r7,r8,df,f) /\
1695         (arm_parse_loop1(r4,r5,f r4,r7,r8,df,f) = (y,q - 8w,r6i,r7i,r8i,df,fi)) /\
1709     \\ `ALIGNED r7 = isDot exp` by
1732     \\ `(f r7 = y''') /\ r7 IN df` by SEP_READ_TAC
1738     \\ Q.EXISTS_TAC `(r7,Dot (Sym "nil") b')::(r8,sexp_list stack)::y'`
1768     \\ `ALIGNED r7 = isDot exp` by
1780            lisp_exp exp r7 (b,d) * lisp_exp (sexp_list stack) r8 (b,d) *
1782       (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5 + 8w`,`r7`,`r8`])
1802      (Q.ABBREV_TAC `f2 = (r7 =+ r4) ((r4 =+ 0x1Bw) ((r4 + 0x4w =+ r5 + 0x8w)
1803               ((r5 + 0xCw =+ 0x3w) ((r5 + 0x8w =+ f r7) f))))`
1807                      r7 (b,d) * lisp_exp (sexp_list stack) r8 (b,d) *
1808            SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5 + 8w`,`r7`,`r8`])
1851       \\ `f r7 = y6` by SEP_READ_TAC
1866     \\ Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ r8) ((r4 =+ r7) f)`
1883     \\ Q.EXISTS_TAC `r7`
1907         ((r8 =+ 0x3w) ((r4 + 0x4w =+ f r8) ((r4 =+ r7) f)))`
1911       \\ `(r4 + 0x4w =+ f r8) ((r4 =+ r7) f) (r8 + 0x4w) = y''''` by
1940       \\ Q.EXISTS_TAC `r7`
1953            lisp_exp exp r7 (b,d) * lisp_exp (sexp_list []) r8 (b,d) *
1954            SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`r7`,`r8`])
1984     \\ `ALIGNED r7 = isDot exp` by
1997            lisp_exp exp r7 (b,d) * lisp_exp (sexp_list stack) r8 (b,d) *
1998            SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`r7`,`r8`])
2019       \\ Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ 0x3w) ((r4 =+ 0x3w) ((r7 =+ 3w) f))`
2024       \\ `f r7 = y'''` by SEP_READ_TAC
2045       \\ Q.EXISTS_TAC `(r4,Dot (Sym "nil") (Sym "nil"))::(r7,Dot (Sym "nil") b')::y'''''`
2055       \\ Q.PAT_X_ASSUM `ALIGNED8 (b - r7)` ASSUME_TAC
2071     \\ Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ r7) f`
2086     \\ Q.EXISTS_TAC `r7`
2101     \\ Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ r7) f`
2118     \\ Q.EXISTS_TAC `r7`
2139   arm_parse8 (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
2141     let (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
2142           arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) in
2146     let r7 = 3w:word32 in
2148     let (r4,r5,r6,r7,r8,dh,h) = arm_parse_loop1 (r4,r5,r6,r7,r8,dh,h) in
2149       (r9,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m)``;
2221   ``!r9 r8 r7 r6 r5 r3 y x s p m h g f dm dh dg df d b.
2230         arm_parse8_pre (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) /\
2231         (arm_parse8 (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
2243   \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`r8`,`r7`,`r6`])
2440     let r7 = r8 + r8 in
2443     let r3 = r9 + r7 in
2450     let (r9,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
2451       arm_parse8 (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) in
2460     let r3 = r7 in
2465     let r7 = 3w:word32 in
2467       (r3,r4,r5,r6,r7,r8,r9,df,dg,dh,dm,f,g,h,m)``;
3115       (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g)``]