Removed three obsolete fields of state and old-check-sum-obj, and sup…

…porting functions. Clarified overlaps in rule forms in :DOC rewrite-quoted-constant.

Quoting :DOC note-8-6:

  Three obsolete fields of the ACL2 [state] have been removed: t-stack,
  32-bit-integer-stack, and list-all-package-names, as have some
  related built-in, undocumented definitions and theorems, including
  old-check-sum-obj and supporting functions.

Modified books as necessary to accommodate the three deleted fields of
state.

Passed "make proofs" and "make devel-check" in addition to the usual
regression-everything.

basis-a.lisp

@@ -8531,12 +8531,7 @@
 ; after making changes to it.
 
                                 nil)
-                               (*file-clock* *file-clock*)
-                               (*t-stack* *t-stack*)
-                               (*t-stack-length* *t-stack-length*)
-                               (*32-bit-integer-stack* *32-bit-integer-stack*)
-                               (*32-bit-integer-stack-length*
-                                *32-bit-integer-stack-length*)))))
+                               (*file-clock* *file-clock*)))))
                ,(let ((p (if w
                              (oneify producer flet-fns w program-p)
                            producer)))

basis-b.lisp

@@ -1412,183 +1412,23 @@
 
   (check-sum1 0 *1-check-length-exclusive-maximum* channel state))
 
-; We now develop code for computing checksums of objects.  There are two
-; separate algorithms, culminating respectively in functions old-check-sum-obj
-; and fchecksum-obj.  The first development was used up through ACL2
-; Version_3.4, which uses an algorithm similar to that of our file-based
-; function, check-sum.  However, ACL2 (with hons) was being used on large cons
-; trees with significant subtree sharing.  These "galactic" trees could have
-; relatively few distinct cons cells but a huge naive node count.  It was thus
-; desirable to memoize the computation of checksums, which was impossible using
-; the existing algorithm because it modified state.
+; We now develop code for computing checksums of objects.  For many versions
+; through Version_8.5 there were two separate algorithms, culminating
+; respectively in functions named old-check-sum-obj, which has since been
+; removed from the sources, and fchecksum-obj.  The first development was used
+; up through ACL2 Version_3.4, which used an algorithm similar to that of our
+; file-based function, check-sum.  However, ACL2 (with hons) was being used on
+; large cons trees with significant subtree sharing.  These "galactic" trees
+; could have relatively few distinct cons cells but a huge naive node count.
+; It was thus desirable to memoize the computation of checksums, which was
+; impossible using the existing algorithm because it modified state.
 
 ; The second development was contributed by Jared Davis (and is now maintained
 ; by the ACL2 developers, who are responsible for any errors).  It is amenable
 ; to memoization and, indeed, fchecksum-obj is memoized.  We say more after
 ; developing the code for the first algorithm, culminating in function
 ; check-sum-obj1.
 
-; We turn now to the first development (which is no longer used in ACL2).
-
-(defun check-sum-inc (n state)
-  (declare (type (unsigned-byte 7) n))
-  (let ((top
-         (32-bit-integer-stack-length state)))
-    (declare (type (signed-byte 32) top))
-    (let ((sum-loc (the (signed-byte 32) (+ top -1)))
-          (len-loc (the (signed-byte 32) (+ top -2))))
-      (declare (type (signed-byte 32) sum-loc len-loc))
-      (let ((sum
-             (aref-32-bit-integer-stack sum-loc state)))
-        (declare (type (signed-byte 32) sum))
-        (let ((len
-               (aref-32-bit-integer-stack len-loc state)))
-          (declare (type (signed-byte 32) len))
-          (let ((len (cond ((= 0 len) *1-check-length-exclusive-maximum*)
-                           (t (the (signed-byte 32) (+ len -1))))))
-            (declare (type (signed-byte 32) len))
-            (let ((state
-                   (aset-32-bit-integer-stack len-loc len state)))
-              (let ((new-sum
-                     (the (signed-byte 32)
-                      (+ sum (the (signed-byte 32) (* n len))))))
-                (declare (type (signed-byte 32) new-sum))
-                (let ((new-sum
-                       (cond ((>= new-sum *check-sum-exclusive-maximum*)
-                              (the (signed-byte 32)
-                               (+ new-sum *-check-sum-exclusive-maximum*)))
-                             (t new-sum))))
-                  (declare (type (signed-byte 32) new-sum))
-                  (aset-32-bit-integer-stack sum-loc new-sum state))))))))))
-
-(defun check-sum-natural (n state)
-  (declare (type unsigned-byte n))
-  (cond ((<= n 127)
-         (check-sum-inc (the (unsigned-byte 7) n) state))
-        (t (pprogn (check-sum-inc (the (unsigned-byte 7) (rem n 127)) state)
-                   (check-sum-natural (truncate n 127) state)))))
-
-(defun check-sum-string1 (str i len state)
-  (declare (type string str))
-  (declare (type (signed-byte 32) i len))
-  (cond ((= i len) state)
-        (t (let ((chr (char str i)))
-             (declare (type character chr))
-             (let ((code (ascii-code! chr)))
-               (declare (type (unsigned-byte 7) code))
-               (cond ((> code 127)
-                      (f-put-global
-                       'check-sum-weirdness (cons str i) state))
-                     (t (pprogn (check-sum-inc code state)
-                                (check-sum-string1
-                                 str
-                                 (the (signed-byte 32) (1+ i))
-                                 len
-                                 state)))))))))
-
-(defun check-sum-string2 (str i len state)
-
-; This function serves the same purpose as check-sum-string1 except
-; that no assumption is made that i or len fit into 32 bits.  It
-; seems unlikely that this function will ever be called, since it
-; seems unlikely that any Lisp will support strings of length 2 billion
-; or more, but who knows.
-
-  (declare (type string str))
-  (cond ((= i len) state)
-        (t (let ((chr (char str i)))
-             (let ((code (ascii-code! chr)))
-               (cond ((> code 127)
-                      (f-put-global
-                       'check-sum-weirdness (cons str i) state))
-                     (t (pprogn (check-sum-inc code state)
-                                (check-sum-string2
-                                 str
-                                 (1+ i)
-                                 len
-                                 state)))))))))
-
-(defun check-sum-string (str state)
-  (let ((len (the integer (length (the string str)))))
-    (cond ((32-bit-integerp len)
-           (check-sum-string1 str 0 (the (signed-byte 32) len) state))
-          (t (check-sum-string2 str 0 len state)))))
-
-(defun check-sum-obj1 (obj state)
-  (cond ((symbolp obj)
-         (pprogn (check-sum-inc 1 state)
-                 (check-sum-string (symbol-name obj) state)))
-        ((stringp obj)
-         (pprogn (check-sum-inc 2 state)
-                 (check-sum-string obj state)))
-        ((rationalp obj)
-         (cond ((integerp obj)
-                (cond ((< obj 0)
-                       (pprogn (check-sum-inc 3 state)
-                               (check-sum-natural (- obj) state)))
-                      (t (pprogn (check-sum-inc 4 state)
-                                 (check-sum-natural obj state)))))
-               (t (let ((n (numerator obj)))
-                    (pprogn (check-sum-inc 5 state)
-                            (check-sum-natural (if (< n 0) (1- (- n)) n) state)
-                            (check-sum-natural (denominator obj) state))))))
-        ((consp obj)
-         (pprogn (check-sum-inc 6 state)
-                 (check-sum-obj1 (car obj) state)
-                 (cond ((atom (cdr obj))
-                        (cond ((cdr obj)
-                               (pprogn (check-sum-inc 7 state)
-                                       (check-sum-obj1 (cdr obj) state)))
-                              (t (check-sum-inc 8 state))))
-                       (t (check-sum-obj1 (cdr obj) state)))))
-        ((characterp obj)
-         (pprogn (check-sum-inc 9 state)
-                 (let ((n (ascii-code! obj)))
-                   (cond ((< n 128)
-                          (check-sum-inc (ascii-code! obj) state))
-                         (t (f-put-global
-                             'check-sum-weirdness obj state))))))
-        ((complex-rationalp obj)
-         (pprogn (check-sum-inc 14 state)
-                 (check-sum-obj1 (realpart obj) state)
-                 (check-sum-obj1 (imagpart obj) state)))
-        (t (f-put-global
-            'check-sum-weirdness obj state))))
-
-(defun old-check-sum-obj (obj state)
-
-; This function became obsolete after Version_3.4 but we include it in case
-; there are situations where it becomes useful again.  It is the culmination of
-; our first development of checksums for objects (as discussed above).
-
-; We return a checksum on obj, using an algorithm similar to that of
-; check-sum.  We return a non-integer as the first value if (and only if) the
-; obj is not composed entirely of conses, symbols, strings, rationals, complex
-; rationals, and characters. If the first value is not an integer, it is one of
-; the offending objects encountered.
-
-; We typically used this function to compute checksums for .cert files.
-
-  (pprogn
-   (extend-32-bit-integer-stack 2 0 state)
-   (let ((top
-          (32-bit-integer-stack-length state)))
-     (let ((sum-loc (+ top -1))
-           (len-loc (+ top -2)))
-       (pprogn
-        (aset-32-bit-integer-stack sum-loc 0 state)
-        (aset-32-bit-integer-stack len-loc *1-check-length-exclusive-maximum*
-                                   state)
-        (f-put-global 'check-sum-weirdness nil state)
-        (check-sum-obj1 obj state)
-        (let ((ans (aref-32-bit-integer-stack sum-loc state)))
-          (pprogn (shrink-32-bit-integer-stack 2 state)
-                  (let ((x (f-get-global 'check-sum-weirdness state)))
-                    (cond (x (pprogn (f-put-global
-                                      'check-sum-weirdness nil state)
-                                     (mv x state)))
-                          (t (mv ans state)))))))))))
-
 ; We now develop code for the second checksum algorithm, contributed by Jared
 ; Davis (now maintained by the ACL2 developers, who are responsible for any
 ; errors).  See also the long comment after check-sum-obj, below.
@@ -2119,19 +1959,6 @@
   (setq *fchecksum-obj-stack-bound* *fchecksum-obj-stack-bound-init*)
   (fchecksum-obj obj))
 
-; ; To use old check-sum-obj code, but then add check-sum-obj to
-; ; *INITIAL-PROGRAM-FNS-WITH-RAW-CODE* if doing this for a build:
-; (defun check-sum-obj (obj)
-;   #-acl2-loop-only
-;   (return-from check-sum-obj
-;                (mv-let (val state)
-;                        (old-check-sum-obj obj *the-live-state*)
-;                        (declare (ignore state))
-;                        val))
-;   #+acl2-loop-only
-;   (declare (ignore obj))
-;   (er hard 'check-sum-obj "ran *1* code for check-sum-obj"))
-
 ; Here are some examples.  Warning: in raw Lisp, set
 ; *fchecksum-obj-stack-bound* to a very large value (say, 10000000) before
 ; running these examples.

books/acl2s/cgen/basis.lisp

@@ -589,8 +589,8 @@ General form: ~
     translate-and-test intersectp check-vars-not-free position
     collect-cdrs-when-car-eq restrict-alist substitute sublis
     ;; added remove1-assoc here, after the change in commit 374edd977999637845227330eb8e99985529b1fc:
-    remove1-assoc function-symbolp the 32-bit-integerp
-    32-bit-integer-listp with-live-state state-global-let*
+    remove1-assoc function-symbolp the
+    with-live-state state-global-let*
     integer-range-p signed-byte-p unsigned-byte-p boole$
     make-var-lst the-mv nth-aliases fix-true-list
     duplicates evens odds resize-list conjoin2

books/build/universal-dependency.certdep

@@ -2,5 +2,4 @@
 ; books.  Suggestion: leave a short note saying why recertification was
 ; required.
 
-Modification for fast-cert mode, and in particular the change to
-support local event-tuples.
+Deleted three fields of state.  It seems safest to recertify everything.

books/clause-processors/SULFA/books/sat/local-clause-simp.lisp

@@ -114,11 +114,10 @@
 ; to a guard violation because (judging from the channel's name) there is an
 ; attempt to write to an input channel.  I'm working around this problem by
 ; introducing the following :program mode wrapper for print-object$-ser.  Note
-; that with one obscure exception (32-bit-integer-stack), fields of the state
-; do not get this special guard-coercion treatment; so the workaround is
-; successful.  Of course, it might be better to provide a "real" fix, to avoid
-; writing to an input channel; but I'm not inclined to put in the effort, since
-; I don't know the details of this work.
+; that fields of the state do not get this special guard-coercion treatment; so
+; the workaround is successful.  Of course, it might be better to provide a
+; "real" fix, to avoid writing to an input channel; but I'm not inclined to put
+; in the effort, since I don't know the details of this work.
 
 ; Matt K. mod, 7/2021: print-object$-ser is now print-object$-fn.
 (defun print-object$-fn-wrapper (x serialize-character channel state)

books/coi/util/tau.lisp

@@ -256,7 +256,7 @@
 ;;      (EQLABLEP (FOO X))
 ;;      (NATP (FOO X))
 ;;      (O-FINP (FOO X))
-;;      (32-BIT-INTEGERP (FOO X))
+;;      (32-BIT-INTEGERP (FOO X)) ; probably not computed after 3/29/2023
 ;;      (FILE-CLOCK-P (FOO X))
 ;;      (<= 0 (FOO X))
 ;;      (<= (FOO X) 3)

books/hacking/hacker.lisp

@@ -732,21 +732,10 @@
     acl2::read-object
     acl2::prin1-with-slashes
     acl2::may-need-slashes
-    acl2::t-stack-length1
-    acl2::extend-t-stack
-    acl2::shrink-t-stack
-    acl2::aref-t-stack
-    acl2::aset-t-stack
-    acl2::32-bit-integer-stack-length1
-    acl2::extend-32-bit-integer-stack
-    acl2::shrink-32-bit-integer-stack
-    acl2::aref-32-bit-integer-stack
-    acl2::aset-32-bit-integer-stack
     acl2::f-big-clock-negative-p
     acl2::f-decrement-big-clock
     acl2::big-clock-negative-p
     acl2::decrement-big-clock
-    acl2::list-all-package-names
     acl2::user-stobj-alist
     acl2::update-user-stobj-alist
     acl2::read-idate

books/kestrel/built-ins/collect.lisp

@@ -446,9 +446,7 @@
     commutativity-2-of-+
     fold-consts-in-+
     distributivity-of-minus-over-+
-    pos-listp-forward-to-integer-listp
-    32-bit-integerp-forward-to-integerp
-    32-bit-integer-listp-forward-to-integer-listp))
+    pos-listp-forward-to-integer-listp))
 
 (defconst *builtin-defaxiom/defthm-characters*
   '(booleanp-characterp

books/kestrel/utilities/channels.lisp

@@ -93,11 +93,6 @@
            (open-channel1 (cdr (assoc-equal channel channels))))
   :hints (("Goal" :in-theory (enable open-channels-p open-channel-listp))))
 
-(local ; also in state.lisp
- (defthm t-stack-of-update-open-input-channels
-   (equal (t-stack (update-open-input-channels x st))
-          (t-stack st))))
-
 (defthm ordered-symbol-alistp-of-add-pair
   (implies (ordered-symbol-alistp x)
            (equal (ordered-symbol-alistp (add-pair key val x))