lisp-runtime/implementation/lisp_codegenScript.sml

159   \\ Q.EXISTS_TAC `f (w2w w0 + EL 6 ds)` \\ FULL_SIMP_TAC std_ss []
230   ``~(EL 7 ds = 0w) /\ ^LISP ==>
234       let (x0,xs1,tw2,w0,f,ds) = (Val (LENGTH xs1), xs1 ++ [x0],
235              tw2i, w0i, fi, UPDATE_NTH 7 (EL 7 ds - 1w) (UPDATE_NTH 8 (EL 8 ds + 1w) ds)) in ^LISP``,
241   \\ Q.EXISTS_TAC `w2w (EL 8 ds) << 2 + 0x1w` \\ FULL_SIMP_TAC std_ss []
333       let (xbp,tw2,ds,f) = (LENGTH xs, tw2i, UPDATE_NTH 1 (sp + 4w * wsp - 1w) ds, fi) in ^LISP``,
348   \\ Cases_on `ds` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1]
402   \\ `EL 1 ds + w2w w1 = sp + 0x4w * wsp + 0x4w * n2w n` by
531   \\ `EL 1 ds + w2w w1 = sp + 0x4w * wsp + 0x4w * n2w n` by
591   \\ `EL 2 ds - EL 4 cs = n2w (code_ptr code)` by
770     ((w2w (f (sp - 0x54w)) << 32 !! w2w (f (sp - 0x58w))) = EL 3 ds) /\
962   ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==>
966          let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``,
983     \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC))
1013   \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM)
1041   ``^LISP /\ 0x100w <+ EL 3 ds ==> isSym x0 ==>
1045          let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``,
1062     \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC))
1093   \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM)
1235     \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC))
1265   \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM)
1299   ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==>
1303          let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``,
1308   ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==>
1312          let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``,
1317   ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==>
1321          let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``,
1452     \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC))
1483   \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM)
1520   ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==>
1524          let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``,
1529   ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 /\ getVal x0 < 536870912 ==>
1533          let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``,
1538   ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 /\ getVal x0 < 536870912 ==>
1542          let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``,
1678   val ds = map (car o fst o dest_eq o concl) (CONJUNCTS def_thm)
1679   val def = el 1 ds
1680   val pre = el 2 ds
1682     ``^LISP /\ 0x100w <+ EL 3 ds ==>
1686          let (code,f,d,tw2,ds) = (WRITE_CODE code [inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length inst)) ds)) in ^LISP``
1716     \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC))
1737   \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM)
1965   ``^LISP /\ 0x100w <+ EL 3 ds ==>
1975   ``^LISP /\ 0x100w <+ EL 3 ds ==>