basis-b

(defun enforce-redundancy-er-args
  (event-form-var wrld-var)
  (list "Enforce-redundancy is active; see :DOC set-enforce-redundancy and ~
         see :DOC redundant-events.  However, the following event ~@0:~|~%~x1"
    `(if (and (symbolp (cadr ,EVENT-FORM-VAR))
        (decode-logical-name (cadr ,EVENT-FORM-VAR) ,WRLD-VAR))
      "conflicts with an existing event of the same name"
      "is not redundant")
    event-form-var))

(defun global-set
  (var val wrld)
  (declare (xargs :guard (and (symbolp var) (plist-worldp wrld))))
  (putprop var 'global-value val wrld))

(defun tilde-@-illegal-variable-or-constant-name-phrase
  (name)
  (cond ((not (symbolp name)) "be symbols")
    ((keywordp name) "not be in the KEYWORD package")
    ((and (legal-constantp1 name)
       (equal (symbol-package-name name) *main-lisp-package-name*)) (cons "not be in the main Lisp package, ~x0"
        (list (cons #\0 *main-lisp-package-name*))))
    ((and (> (length (symbol-name name)) 0)
       (eql (char (symbol-name name) 0) #\&)) "not start with ampersands")
    ((and (not (legal-constantp1 name))
       (member-eq name *common-lisp-specials-and-constants*)) "not be among certain symbols from the main Lisp package, namely, the ~
          value of the list *common-lisp-specials-and-constants*")
    ((and (not (legal-constantp1 name))
       (equal (symbol-package-name name) *main-lisp-package-name*)
       (not (member-eq name
           *common-lisp-symbols-from-main-lisp-package*))) "either not be in the main Lisp package, or else must be among the ~
          imports into ACL2 from that package, namely, the list ~
          *common-lisp-symbols-from-main-lisp-package*")
    (t "be approved by LEGAL-VARIABLE-OR-CONSTANT-NAMEP and this ~
            one wasn't, even though it passes all the checks known to ~
            the diagnostic function ~
            TILDE-@-ILLEGAL-VARIABLE-OR-CONSTANT-NAME-PHRASE")))

(defun legal-constantp
  (name)
  (eq (legal-variable-or-constant-namep name) 'constant))

(defun gsym
  (pkg-witness char-lst cnt)
  (declare (xargs :guard (and (symbolp pkg-witness)
        (character-listp char-lst)
        (integerp cnt)
        (<= 0 cnt))))
  (intern-in-package-of-symbol (coerce (append char-lst (explode-nonnegative-integer cnt 10 nil))
      'string)
    pkg-witness))

(defun genvar1-guardp
  (pkg-witness char-lst avoid-lst cnt)
  (declare (xargs :guard t))
  (and (symbolp pkg-witness)
    (let ((p (symbol-package-name pkg-witness)))
      (and (not (equal p "KEYWORD"))
        (not (equal p *main-lisp-package-name*))))
    (character-listp char-lst)
    (consp char-lst)
    (not (eql (car char-lst) #\*))
    (not (eql (car char-lst) #\&))
    (true-listp avoid-lst)
    (natp cnt)))

(defun genvar1
  (pkg-witness char-lst avoid-lst cnt)
  (declare (xargs :guard (genvar1-guardp pkg-witness char-lst avoid-lst cnt)))
  (if (mbt (genvar1-guardp pkg-witness char-lst avoid-lst cnt))
    (let ((sym (mbe :logic (gsym pkg-witness char-lst cnt)
           :exec (intern-in-package-of-symbol (coerce (append char-lst (explode-nonnegative-integer cnt 10 nil))
               'string)
             pkg-witness))))
      (cond ((or (member sym avoid-lst) (not (legal-variablep sym))) (genvar1 pkg-witness char-lst avoid-lst (1+ cnt)))
        (t sym)))
    nil))

(defun genvar-guardp
  (pkg-witness prefix n avoid-lst)
  (declare (xargs :guard t))
  (and (symbolp pkg-witness)
    (stringp prefix)
    (or (null n) (natp n))
    (true-listp avoid-lst)))

(defun genvar
  (pkg-witness prefix n avoid-lst)
  (declare (xargs :guard (genvar-guardp pkg-witness prefix n avoid-lst)))
  (let* ((pkg-witness (cond ((let ((p (symbol-package-name pkg-witness)))
            (or (equal p "KEYWORD") (equal p *main-lisp-package-name*))) 'genvar)
         (t pkg-witness))) (sym (if (null n)
          (intern-in-package-of-symbol prefix pkg-witness)
          nil))
      (cnt (if n
          n
          0)))
    (cond ((and (null n)
         (legal-variablep sym)
         (not (member sym avoid-lst))) sym)
      (t (let ((char-lst (coerce prefix 'list)))
          (cond ((null char-lst) (genvar1 pkg-witness '(#\V) avoid-lst cnt))
            ((and (consp char-lst)
               (or (eql (car char-lst) #\*) (eql (car char-lst) #\&))) (genvar1 pkg-witness (cons #\V char-lst) avoid-lst cnt))
            (t (genvar1 pkg-witness char-lst avoid-lst cnt))))))))

(defun gen-formals-from-pretty-flags1
  (pretty-flags i avoid)
  (cond ((endp pretty-flags) nil)
    ((and (symbolp (car pretty-flags))
       (or (equal (symbol-name (car pretty-flags)) "*")
         (eq (car pretty-flags) :df))) (let ((xi (pack2 'x i)))
        (cond ((member-eq xi avoid) (let ((new-var (genvar 'genvar "GENSYM" 1 avoid)))
              (cons new-var
                (gen-formals-from-pretty-flags1 (cdr pretty-flags)
                  (+ i 1)
                  (cons new-var avoid)))))
          (t (cons xi
              (gen-formals-from-pretty-flags1 (cdr pretty-flags)
                (+ i 1)
                avoid))))))
    (t (cons (car pretty-flags)
        (gen-formals-from-pretty-flags1 (cdr pretty-flags)
          (+ i 1)
          avoid)))))

(defun gen-formals-from-pretty-flags
  (pretty-flags)
  (gen-formals-from-pretty-flags1 pretty-flags 1 pretty-flags))

(defun collect-non-x
  (x lst)
  (declare (xargs :guard (true-listp lst)))
  (cond ((endp lst) nil)
    ((equal (car lst) x) (collect-non-x x (cdr lst)))
    (t (cons (car lst) (collect-non-x x (cdr lst))))))

(defun collect-non-nil-df
  (lst)
  (declare (xargs :guard (true-listp lst)))
  (cond ((endp lst) nil)
    ((or (eq (car lst) nil) (eq (car lst) :df)) (collect-non-nil-df (cdr lst)))
    (t (cons (car lst) (collect-non-nil-df (cdr lst))))))

(defun collect-non-*
  (lst)
  (declare (xargs :guard (symbol-listp lst)))
  (cond ((endp lst) nil)
    ((equal (symbol-name (car lst)) "*") (collect-non-* (cdr lst)))
    (t (cons (car lst) (collect-non-* (cdr lst))))))

(defun defstub-body-new
  (outputs)
  (cond ((atom outputs) (cond ((and (symbolp outputs) (equal (symbol-name outputs) "*")) nil)
        ((eq outputs :df) '(df0))
        (t outputs)))
    ((and (symbolp (car outputs))
       (equal (symbol-name (car outputs)) "*")) (cons nil (defstub-body-new (cdr outputs))))
    ((eq (car outputs) :df) (cons '(df0) (defstub-body-new (cdr outputs))))
    (t (cons (car outputs) (defstub-body-new (cdr outputs))))))

(defun collect-non-*-df
  (lst)
  (declare (xargs :guard (symbol-listp lst)))
  (cond ((endp lst) nil)
    ((or (equal (symbol-name (car lst)) "*") (eq (car lst) :df)) (collect-non-*-df (cdr lst)))
    (t (cons (car lst) (collect-non-*-df (cdr lst))))))

(defun collect-by-position
  (sub-domain full-domain full-range)
  (declare (xargs :guard (and (symbol-listp full-domain)
        (true-listp sub-domain)
        (true-listp full-range)
        (eql (length full-domain) (length full-range)))))
  (if (endp full-domain)
    nil
    (if (member-eq (car full-domain) sub-domain)
      (cons (car full-range)
        (collect-by-position sub-domain
          (cdr full-domain)
          (cdr full-range)))
      (collect-by-position sub-domain
        (cdr full-domain)
        (cdr full-range)))))

(defun defstub-ignores
  (formals body)
  (declare (xargs :guard t))
  (if (and (symbol-listp formals)
      (or (symbolp body)
        (and (consp body) (true-listp (cdr body)))))
    (set-difference-eq formals
      (if (symbolp body)
        (list body)
        (cdr body)))
    nil))

(defun defstub-body-old-aux
  (outputs-without-mv stobjs)
  (declare (xargs :guard (symbol-listp stobjs)))
  (cond ((atom outputs-without-mv) nil)
    ((member-eq (car outputs-without-mv) stobjs) (cons (car outputs-without-mv)
        (defstub-body-old-aux (cdr outputs-without-mv) stobjs)))
    (t (cons nil
        (defstub-body-old-aux (cdr outputs-without-mv) stobjs)))))

(defun defstub-body-old
  (outputs stobjs)
  (declare (xargs :guard (symbol-listp stobjs)))
  (cond ((atom outputs) (cond ((member-eq outputs stobjs) outputs) (t nil)))
    (t (cons (car outputs)
        (defstub-body-old-aux (cdr outputs) stobjs)))))

(defun defstub-fn1
  (signatures name formals ign-dcl stobjs dfs body outputs)
  `(with-output :off (:other-than error summary)
    :ctx '(defstub . ,NAME)
    :summary-off value
    (encapsulate ,SIGNATURES
      (with-output :off summary (logic))
      (with-output :summary-off (:other-than redundant)
        (local (defun ,NAME
            ,FORMALS
            (declare ,IGN-DCL
              ,@(AND STOBJS `((XARGS :STOBJS ,STOBJS)))
              ,@(AND DFS `((TYPE DOUBLE-FLOAT ,@DFS))))
            ,BODY)))
      ,@(AND (CONSP OUTPUTS)
       `((WITH-OUTPUT :OFF SUMMARY
                      (DEFTHM ,(PACKN-POS (LIST "TRUE-LISTP-" NAME) NAME)
                              (TRUE-LISTP (,NAME ,@FORMALS)) :RULE-CLASSES
                              :TYPE-PRESCRIPTION)))))))

(defun defstub-fn
  (name args)
  (let ((len-args (length args)))
    (cond ((not (and name (symbolp name))) `(er soft
          '(defstub . ,NAME)
          "The first argument of defstub must be a non-nil symbol.  The form ~
            ~x0 is thus illegal."
          '(defstub ,NAME ,@ARGS)))
      ((< len-args 2) `(er soft
          '(defstub . ,NAME)
          "Defstub must be of the form (defstub name inputs => outputs ...) ~
            or (defstub name inputs outputs ...).  See :DOC defstub."))
      ((or (= len-args 2)
         (and (keywordp (caddr args)) (not (eq (caddr args) :df)))) (let* ((inputs (car args)) (outputs (cadr args))
            (options (cddr args))
            (stobjs (and (keyword-value-listp options)
                (cadr (assoc-keyword :stobjs options))))
            (stobjs (cond ((symbol-listp stobjs) stobjs)
                ((symbolp stobjs) (list stobjs))
                (t nil)))
            (stobjs (cond ((and (true-listp inputs) (member-eq 'state inputs)) (add-to-set-eq 'state stobjs))
                (t stobjs)))
            (dfs (and (keyword-value-listp options)
                (cadr (assoc-keyword :dfs options))))
            (body (defstub-body-old outputs stobjs)))
          (defstub-fn1 `((,NAME ,@ARGS))
            name
            inputs
            `(ignorable ,@INPUTS)
            stobjs
            dfs
            body
            outputs)))
      (t (let* ((inputs (car args)) (arrow (cadr args))
            (outputs (caddr args))
            (options (cdddr args))
            (formals (and (symbol-listp inputs)
                (gen-formals-from-pretty-flags inputs)))
            (body (defstub-body-new outputs))
            (ignores (defstub-ignores formals body))
            (stobjs (and (symbol-listp inputs) (collect-non-*-df inputs)))
            (dfs (collect-by-position '(:df) inputs formals)))
          (defstub-fn1 `(((,NAME ,@INPUTS) ,ARROW ,OUTPUTS ,@OPTIONS))
            name
            formals
            `(ignore ,@IGNORES)
            stobjs
            dfs
            body
            outputs))))))

(defun cons-term1-cases
  (alist)
  (cond ((endp alist) nil)
    ((member-eq (caar alist)
       '(if bad-atom<=
         pkg-imports
         pkg-witness)) (cons-term1-cases (cdr alist)))
    (t (cons (let* ((trip (car alist)) (fn (car trip))
            (formals (cadr trip))
            (guard (caddr trip)))
          (list fn
            (cond ((equal guard *t*) `(kwote (,FN ,@FORMALS)))
              ((or (equal formals '(x)) (equal formals '(x y))) `(and ,GUARD (kwote (,FN ,@FORMALS))))
              (t (case-match formals
                  ((f1) `(let ((,F1 x))
                      (and ,GUARD (kwote (,FN ,@FORMALS)))))
                  ((f1 f2) `(let ((,F1 x) (,F2 y))
                      (and ,GUARD (kwote (,FN ,@FORMALS)))))
                  (& (er hard!
                      'cons-term1-cases
                      "Unexpected formals, ~x0"
                      formals)))))))
        (cons-term1-cases (cdr alist))))))

(defun quote-listp
  (l)
  (declare (xargs :guard (true-listp l)))
  (cond ((null l) t)
    (t (and (quotep (car l)) (quote-listp (cdr l))))))

(defun cons-term1
  (fn args)
  (declare (xargs :guard (and (pseudo-term-listp args) (quote-listp args))))
  (cons-term1-body))

(defun cons-term
  (fn args)
  (declare (xargs :guard (pseudo-term-listp args)))
  (cond ((quote-listp args) (cons-term1 fn args))
    (t (cons fn args))))

(defun cdr-nest
  (n v)
  (cond ((equal n 0) v) (t (fargn1 v n))))

(defun df-string
  (x)
  (declare (xargs :guard t :mode :logic))
  (constrained-df-string x))

(defun stobj-print-name
  (name)
  (declare (xargs :guard (symbolp name)))
  (let* ((s (symbol-name name)))
    (coerce (cons #\<
        (append (string-downcase1 (coerce s 'list)) '(#\>)))
      'string)))

(defun eviscerate-stobjs1
  (estobjs-out lst
    print-level
    print-length
    alist
    evisc-table
    hiding-cars
    iprint-alist
    iprint-fal-new
    iprint-fal-old
    eager-p)
  (cond ((null estobjs-out) (mv nil iprint-alist iprint-fal-new))
    ((car estobjs-out) (mv-let (rest iprint-alist iprint-fal-new)
        (eviscerate-stobjs1 (cdr estobjs-out)
          (cdr lst)
          print-level
          print-length
          alist
          evisc-table
          hiding-cars
          iprint-alist
          iprint-fal-new
          iprint-fal-old
          eager-p)
        (mv (cons (car estobjs-out) rest)
          iprint-alist
          iprint-fal-new)))
    (t (mv-let (first iprint-alist iprint-fal-new)
        (eviscerate (car lst)
          print-level
          print-length
          alist
          evisc-table
          hiding-cars
          iprint-alist
          iprint-fal-new
          iprint-fal-old
          eager-p)
        (mv-let (rest iprint-alist iprint-fal-new)
          (eviscerate-stobjs1 (cdr estobjs-out)
            (cdr lst)
            print-level
            print-length
            alist
            evisc-table
            hiding-cars
            iprint-alist
            iprint-fal-new
            iprint-fal-old
            eager-p)
          (mv (cons first rest) iprint-alist iprint-fal-new))))))

(defun eviscerate-stobjs
  (estobjs-out lst
    print-level
    print-length
    alist
    evisc-table
    hiding-cars
    iprint-alist
    iprint-fal-old
    eager-p)
  (cond ((null estobjs-out) (eviscerate lst
        print-level
        print-length
        alist
        evisc-table
        hiding-cars
        iprint-alist
        nil
        iprint-fal-old
        eager-p))
    ((null (cdr estobjs-out)) (cond ((car estobjs-out) (mv (car estobjs-out) iprint-alist nil))
        (t (eviscerate lst
            print-level
            print-length
            alist
            evisc-table
            hiding-cars
            iprint-alist
            nil
            iprint-fal-old
            eager-p))))
    (t (eviscerate-stobjs1 estobjs-out
        lst
        print-level
        print-length
        alist
        evisc-table
        hiding-cars
        iprint-alist
        nil
        iprint-fal-old
        eager-p))))

(defun eviscerate-stobjs-top
  (estobjs-out lst
    print-level
    print-length
    alist
    evisc-table
    hiding-cars
    state)
  (pprogn (iprint-oracle-updates? state)
    (brr-evisc-tuple-oracle-update state)
    (let ((iprint-fal-old (f-get-global 'iprint-fal state)))
      (mv-let (result iprint-alist iprint-fal-new)
        (eviscerate-stobjs estobjs-out
          lst
          print-level
          print-length
          alist
          evisc-table
          hiding-cars
          (and (iprint-enabledp state) (iprint-last-index state))
          iprint-fal-old
          (iprint-eager-p iprint-fal-old))
        (fast-alist-free-on-exit iprint-fal-new
          (let ((state (cond ((eq iprint-alist t) (f-put-global 'evisc-hitp-without-iprint t state))
                 ((atom iprint-alist) state)
                 (t (update-iprint-ar-fal iprint-alist
                     iprint-fal-new
                     iprint-fal-old
                     state)))))
            (mv result state)))))))

(defun make-let
  (bindings ignores type-dcls body)
  `(let ,BINDINGS
    ,@(AND (OR IGNORES TYPE-DCLS)
       `((DECLARE ,@(AND IGNORES `((IGNORE ,@IGNORES)))
                  ,@TYPE-DCLS)))
    ,BODY))

(defun def-basic-type-sets1
  (lst i)
  (declare (xargs :guard (and (integerp i) (true-listp lst))))
  (cond ((null lst) nil)
    (t (cons (list 'defconst (car lst) (list 'the-type-set (expt 2 i)))
        (def-basic-type-sets1 (cdr lst) (+ i 1))))))

(defun list-of-the-type-set
  (x)
  (cond ((consp x) (cons (list 'the-type-set (car x))
        (list-of-the-type-set (cdr x))))
    (t nil)))

(defun ts-union0-fn
  (x)
  (list 'the-type-set
    (cond ((null x) '*ts-empty*)
      ((null (cdr x)) (car x))
      (t (xxxjoin 'logior (list-of-the-type-set x))))))

(defun ts-builder-case-listp
  (x)
  (cond ((atom x) (eq x nil))
    ((and (consp (car x))
       (true-listp (car x))
       (not (null (cdr (car x))))) (cond ((or (eq t (car (car x))) (eq 'otherwise (car (car x)))) (cond ((null (cdr x)) 'otherwise) (t nil)))
        (t (let ((ans (ts-builder-case-listp (cdr x))))
            (cond ((eq ans 'otherwise) (cond ((symbolp (car (car x))) 'otherwise) (t nil)))
              (t ans))))))
    (t nil)))

(defun ts-builder-macro1
  (x case-lst seen)
  (declare (xargs :guard (and (symbolp x) (ts-builder-case-listp case-lst))))
  (cond ((null case-lst) nil)
    ((or (eq (caar case-lst) t) (eq (caar case-lst) 'otherwise)) (sublis (list (cons 'x x)
          (cons 'seen seen)
          (cons 'ts2 (cadr (car case-lst))))
        '((cond ((ts-intersectp x (ts-complement0 (ts-union0 . seen))) ts2)
           (t *ts-empty*)))))
    (t (cons (sublis (list (cons 'x x)
            (cons 'ts1 (caar case-lst))
            (cons 'ts2 (cadr (car case-lst))))
          '(cond ((ts-intersectp x ts1) ts2) (t *ts-empty*)))
        (ts-builder-macro1 x
          (cdr case-lst)
          (cons (caar case-lst) seen))))))

(defun ts-builder-macro
  (x case-lst)
  (declare (xargs :guard (and (symbolp x) (ts-builder-case-listp case-lst))))
  (cons 'ts-union (ts-builder-macro1 x case-lst nil)))

(defun print-current-idate
  (channel state)
  (mv-let (d state)
    (read-idate state)
    (print-idate d channel state)))

(defun skip-when-logic
  (str state)
  (pprogn (observation 'top-level
      "~s0 events are skipped when the default-defun-mode is ~x1."
      str
      (default-defun-mode-from-state state))
    (mv nil nil state)))

(defun chk-inhibit-output-lst
  (lst ctx state)
  (let ((msg (chk-inhibit-output-lst-msg lst)))
    (cond (msg (er soft ctx "~@0" msg))
      (t (let ((lst (if (member-eq 'warning! lst)
               (add-to-set-eq 'warning lst)
               lst)))
          (pprogn (cond ((and (member-eq 'prove lst)
                 (not (member-eq 'proof-tree lst))
                 (member-eq 'proof-tree
                   (f-get-global 'inhibit-output-lst state))) (warning$ ctx
                  nil
                  "The printing of proof-trees is being ~
                                         enabled while the printing of proofs ~
                                         is being disabled.  You may want to ~
                                         execute :STOP-PROOF-TREE in order to ~
                                         inhibit proof-trees as well."))
              (t state))
            (value lst)))))))

(defun set-inhibit-output-lst-fn
  (lst state)
  (er-let* ((lst (chk-inhibit-output-lst lst 'set-inhibit-output-lst state)))
    (pprogn (f-put-global 'inhibit-output-lst lst state)
      (value lst))))

(defun chk-ld-skip-proofsp
  (val ctx state)
  (declare (xargs :mode :program))
  (cond ((member-eq val
       '(t nil
         include-book
         initialize-acl2
         include-book-with-locals)) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-skip-proofsp val))))

(defun set-ld-skip-proofsp
  (val state)
  (declare (xargs :mode :program))
  (er-progn (chk-ld-skip-proofsp val 'set-ld-skip-proofsp state)
    (pprogn (f-put-global 'ld-skip-proofsp val state)
      (value val))))

(defun set-write-acl2x
  (val state)
  (declare (xargs :guard (state-p state)))
  (er-progn (cond ((member-eq val '(t nil)) (value nil))
      ((and (consp val) (null (cdr val))) (chk-ld-skip-proofsp (car val) 'set-write-acl2x state))
      (t (er soft
          'set-write-acl2x
          "Illegal value for set-write-acl2x, ~x0.  See :DOC ~
                 set-write-acl2x."
          val)))
    (pprogn (f-put-global 'write-acl2x val state) (value val))))

(defun ascii-code!
  (x)
  (let ((y (char-code x)))
    (cond ((or (= y 0) (= y 128)) 1)
      ((< 127 y) (- y 128))
      (t y))))

(defun check-sum1
  (sum len channel state)
  (declare (type (signed-byte 32) sum len))
  (let ((len (cond ((= len 0) *1-check-length-exclusive-maximum*)
         (t (the (signed-byte 32) (1- len))))))
    (declare (type (signed-byte 32) len))
    (mv-let (x state)
      (read-char$ channel state)
      (cond ((not (characterp x)) (mv sum state))
        (t (let ((inc (ascii-code! x)))
            (declare (type (unsigned-byte 7) inc))
            (cond ((and (= inc 0) (not (eql x #\	))) (mv x state))
              (t (let ((inc (the (unsigned-byte 7) (cond ((= inc 0) 9) (t inc)))))
                  (declare (type (unsigned-byte 7) inc))
                  (let ((sum (+ sum (the (signed-byte 32) (* inc len)))))
                    (declare (type (signed-byte 32) sum))
                    (check-sum1 (cond ((>= sum *check-sum-exclusive-maximum*) (the (signed-byte 32)
                            (+ sum *-check-sum-exclusive-maximum*)))
                        (t sum))
                      len
                      channel
                      state)))))))))))

(defun check-sum
  (channel state)
  (check-sum1 0
    *1-check-length-exclusive-maximum*
    channel
    state))

(defun plus-mod-m31
  (u v)
  (declare (type (signed-byte 32) u v))
  (the (signed-byte 32)
    (let ((u (min u v)) (v (max u v)))
      (declare (type (signed-byte 32) u v))
      (cond ((< u 1073741824) (cond ((< v 1073741824) (the (signed-byte 32) (+ u v)))
            (t (let ((part (+ (the (signed-byte 32) (logand v 1073741823)) u)))
                (declare (type (signed-byte 32) part))
                (cond ((< part 1073741823) (the (signed-byte 32) (logior part 1073741824)))
                  ((eql part 1073741823) 0)
                  (t (the (signed-byte 32)
                      (1+ (the (signed-byte 32) (logxor part 1073741824))))))))))
        (t (the (signed-byte 32)
            (- 2147483647
              (the (signed-byte 32)
                (+ (the (signed-byte 32) (- 2147483647 u))
                  (the (signed-byte 32) (- 2147483647 v)))))))))))

(defun double-mod-m31
  (x)
  (declare (type (signed-byte 32) x))
  (the (signed-byte 32)
    (cond ((< x 1073741824) (the (signed-byte 32) (ash x 1)))
      (t (the (signed-byte 32)
          (- 2147483647
            (the (signed-byte 32)
              (ash (the (signed-byte 32) (- 2147483647 x)) 1))))))))

(defun times-expt-2-16-mod-m31
  (x)
  (declare (type (signed-byte 32) x))
  (the (signed-byte 32)
    (let ((hi (ash x -16)) (lo (logand x 65535)))
      (declare (type (signed-byte 32) hi lo))
      (cond ((eql 0 (the (signed-byte 32) (logand lo 32768))) (the (signed-byte 32)
            (plus-mod-m31 (double-mod-m31 hi)
              (the (signed-byte 32) (ash lo 16)))))
        (t (the (signed-byte 32)
            (plus-mod-m31 (double-mod-m31 hi)
              (the (signed-byte 32)
                (logior 1
                  (the (signed-byte 32)
                    (ash (the (signed-byte 32) (logand lo 32767)) 16)))))))))))

(defun times-mod-m31
  (u v)
  (declare (type (signed-byte 32) u v))
  (the (signed-byte 32)
    (rem (the (signed-byte 64) (* u v)) 2147483647)))

(defun fchecksum-natural-aux
  (n ans)
  (declare (type (integer 0 *) n))
  (declare (type (signed-byte 32) ans))
  (the (signed-byte 32)
    (if (eql n 0)
      ans
      (fchecksum-natural-aux (the (integer 0 *) (ash n -31))
        (the (signed-byte 32)
          (logxor ans
            (the (signed-byte 32)
              (times-mod-m31 (logand n 2147483647) 392894102))))))))

(defun fchecksum-natural
  (n)
  (declare (type (integer 0 *) n))
  (the (signed-byte 32) (fchecksum-natural-aux n 28371987)))

(defun fchecksum-string1
  (str i len ans)
  (declare (type string str))
  (declare (type (signed-byte 32) i len ans))
  (the (signed-byte 32)
    (if (>= i len)
      ans
      (let* ((c0 (logand 127
             (the (signed-byte 32)
               (char-code (the character (char str i)))))) (i (+ i 1))
          (c1 (if (>= i len)
              0
              (char-code (the character (char str i)))))
          (i (+ i 1))
          (c2 (if (>= i len)
              0
              (char-code (the character (char str i)))))
          (i (+ i 1))
          (c3 (if (>= i len)
              0
              (char-code (the character (char str i)))))
          (bits (logior (the (signed-byte 32) (ash c0 24))
              (the (signed-byte 32)
                (logior (the (signed-byte 32) (ash c1 16))
                  (the (signed-byte 32)
                    (logior (the (signed-byte 32) (ash c2 8))
                      (the (signed-byte 32) c3))))))))
        (declare (type (signed-byte 32) c0 i c1 c2 c3 bits))
        (fchecksum-string1 str
          i
          len
          (the (signed-byte 32)
            (logxor ans
              (the (signed-byte 32) (times-mod-m31 bits 506249751)))))))))

(defun fchecksum-string2
  (str i len ans)
  (declare (type string str))
  (declare (type (signed-byte 32) ans))
  (declare (type (integer 0 *) i len))
  (the (signed-byte 32)
    (if (>= i len)
      ans
      (let* ((c0 (logand 127
             (the (signed-byte 32)
               (char-code (the character (char str i)))))) (i (+ i 1))
          (c1 (if (>= i len)
              0
              (char-code (the character (char str i)))))
          (i (+ i 1))
          (c2 (if (>= i len)
              0
              (char-code (the character (char str i)))))
          (i (+ i 1))
          (c3 (if (>= i len)
              0
              (char-code (the character (char str i)))))
          (bits (logior (the (signed-byte 32) (ash c0 24))
              (the (signed-byte 32)
                (logior (the (signed-byte 32) (ash c1 16))
                  (the (signed-byte 32)
                    (logior (the (signed-byte 32) (ash c2 8))
                      (the (signed-byte 32) c3))))))))
        (declare (type (signed-byte 32) c0 c1 c2 c3 bits)
          (type (integer 0 *) i))
        (fchecksum-string2 str
          i
          len
          (the (signed-byte 32)
            (logxor ans
              (the (signed-byte 32) (times-mod-m31 bits 506249751)))))))))

(defun fchecksum-string
  (str)
  (declare (type string str))
  (the (signed-byte 32)
    (let ((length (length str)))
      (declare (type (integer 0 *) length))
      (cond ((< length 2147483647) (fchecksum-string1 str
            0
            length
            (times-mod-m31 (the (signed-byte 32) (+ 1 length))
              718273893)))
        (t (fchecksum-string2 str
            0
            length
            (rem (the integer (* (+ 1 length) 718273893)) 2147483647)))))))

(defun fchecksum-atom
  (x)
  (the (signed-byte 32)
    (cond ((natp x) (fchecksum-natural x))
      ((integerp x) (let ((abs-code (fchecksum-natural (- x))))
          (declare (type (signed-byte 32) abs-code))
          (times-mod-m31 abs-code 283748912)))
      ((symbolp x) (let* ((pkg-code (fchecksum-string (symbol-package-name x))) (sym-code (fchecksum-string (symbol-name x)))
            (pkg-code-scramble (times-mod-m31 pkg-code 938187814)))
          (declare (type (signed-byte 32) pkg-code sym-code pkg-code-scramble))
          (logxor pkg-code-scramble sym-code)))
      ((stringp x) (fchecksum-string x))
      ((characterp x) (times-mod-m31 (char-code x) 619823821))
      ((rationalp x) (let* ((num-code (fchecksum-atom (numerator x))) (den-code (fchecksum-natural (denominator x)))
            (num-scramble (times-mod-m31 num-code 111298397))
            (den-scramble (times-mod-m31 den-code 391892127)))
          (declare (type (signed-byte 32)
              num-code
              den-code
              num-scramble
              den-scramble))
          (logxor num-scramble den-scramble)))
      ((complex-rationalp x) (let* ((imag-code (fchecksum-atom (imagpart x))) (real-code (fchecksum-atom (realpart x)))
            (imag-scramble (times-mod-m31 imag-code 18783723))
            (real-scramble (times-mod-m31 real-code 981827319)))
          (declare (type (signed-byte 32)
              imag-code
              real-code
              imag-scramble
              real-scramble))
          (logxor imag-scramble real-scramble)))
      (t (prog2$ (er hard 'fchecksum-atom "Bad atom, ~x0" x) 0)))))

(defun check-sum-obj
  (obj)
  (declare (xargs :guard t))
  (fchecksum-obj obj))

(defun read-file-iterate
  (channel acc state)
  (mv-let (eof obj state)
    (read-object channel state)
    (cond (eof (mv (reverse acc) state))
      (t (read-file-iterate channel (cons obj acc) state)))))

(defun read-file+
  (name msg ctx state)
  (declare (xargs :stobjs state :mode :program))
  (mv-let (channel state)
    (open-input-channel name :object state)
    (cond (channel (mv-let (ans state)
          (read-file-iterate channel nil state)
          (pprogn (close-input-channel channel state)
            (mv nil ans state))))
      (msg (er soft ctx "~@0" msg))
      (t (er soft ctx "No file found ~x0." name)))))

(defun read-file
  (name state)
  (declare (xargs :stobjs state :mode :program))
  (read-file+ name nil 'read-file state))

(defun formals
  (fn w)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp w))))
  (let ((temp (getpropc fn 'formals t w)))
    (cond ((eq temp t) (er hard?
          'formals
          "Every function symbol is supposed to have a 'FORMALS property ~
                but ~x0 does not!"
          fn))
      (t temp))))

(defun plist-worldp-with-formals
  (alist)
  (declare (xargs :guard t))
  (cond ((atom alist) (eq alist nil))
    (t (and (consp (car alist))
        (symbolp (car (car alist)))
        (consp (cdr (car alist)))
        (symbolp (cadr (car alist)))
        (or (not (eq (cadr (car alist)) 'formals))
          (eq (cddr (car alist)) *acl2-property-unbound*)
          (true-listp (cddr (car alist))))
        (plist-worldp-with-formals (cdr alist))))))

(defun arity
  (fn w)
  (declare (xargs :guard (and (or (and (consp fn) (consp (cdr fn)) (true-listp (cadr fn)))
          (symbolp fn))
        (plist-worldp-with-formals w))))
  (cond ((flambdap fn) (length (lambda-formals fn)))
    (t (let ((temp (getpropc fn 'formals t w)))
        (cond ((eq temp t) nil) (t (length temp)))))))

(defun symbol-class
  (sym wrld)
  (declare (xargs :guard (and (symbolp sym) (plist-worldp wrld))))
  (if (eq sym 'cons)
    :common-lisp-compliant (or (getpropc sym 'symbol-class nil wrld)
      (if (getpropc sym 'theorem nil wrld)
        :ideal :program))))

(defun defun-mode
  (name wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (cond ((and (symbolp name) (function-symbolp name wrld)) (fdefun-mode name wrld))
    (t nil)))

(defun arities-okp
  (user-table w)
  (declare (xargs :guard (and (symbol-alistp user-table)
        (plist-worldp-with-formals w))))
  (cond ((endp user-table) t)
    (t (and (equal (arity (car (car user-table)) w)
          (cdr (car user-table)))
        (logicp (car (car user-table)) w)
        (arities-okp (cdr user-table) w)))))

(defun latest-body
  (fncall hyp concl)
  (if hyp
    (fcons-term* 'if hyp concl (fcons-term* 'hide fncall))
    concl))

(defun def-body
  (fn wrld)
  (declare (xargs :guard (and (symbolp fn)
        (plist-worldp wrld)
        (true-listp (getpropc fn 'def-bodies nil wrld)))))
  (car (getpropc fn 'def-bodies nil wrld)))

(defun body
  (fn normalp w)
  (cond ((flambdap fn) (lambda-body fn))
    (normalp (let ((def-body (def-body fn w)))
        (cond ((not (eq (access def-body def-body :equiv) 'equal)) (getpropc fn 'unnormalized-body nil w))
          (t (latest-body (fcons-term fn (access def-body def-body :formals))
              (access def-body def-body :hyp)
              (access def-body def-body :concl))))))
    (t (getpropc fn 'unnormalized-body nil w))))

(defun get-stobj-recognizer
  (stobj wrld)
  (cond ((eq stobj 'state) 'state-p)
    (t (let ((prop (getpropc stobj 'stobj nil wrld)))
        (and prop (access stobj-property prop :recognizer))))))

(defun stobj-recognizer-terms
  (known-stobjs wrld)
  (cond ((endp known-stobjs) nil)
    (t (cons (fcons-term* (get-stobj-recognizer (car known-stobjs) wrld)
          (car known-stobjs))
        (stobj-recognizer-terms (cdr known-stobjs) wrld)))))

(defun mcons-term-smart
  (fn args)
  (if (and (eq fn 'if) (equal (car args) *t*))
    (cadr args)
    (cons-term fn args)))

(defun optimize-stobj-recognizers
  (known-stobjs term wrld)
  (cond ((null known-stobjs) term)
    (t (optimize-stobj-recognizers1 known-stobjs
        (stobj-recognizer-terms known-stobjs wrld)
        term))))

(defun guard
  (fn stobj-optp w)
  (cond ((flambdap fn) *t*)
    ((or (not stobj-optp) (all-nils (stobjs-in fn w))) (getpropc fn 'guard *t* w))
    (t (let* ((guard (or (getpropc fn 'guard *t* w)
             (illegal 'guard
               "Found a nil guard for ~x0."
               (list (cons #\0 fn))))) (stobjs-in (stobjs-in fn w))
          (known-dfs (collect-by-position '(:df) stobjs-in (formals fn w))))
        (optimize-stobj-recognizers (collect-non-nil-df stobjs-in)
          (if known-dfs
            (optimize-dfp known-dfs guard)
            guard)
          w)))))

(defun guard-lst
  (fns stobj-optp w)
  (cond ((null fns) nil)
    (t (cons (guard (car fns) stobj-optp w)
        (guard-lst (cdr fns) stobj-optp w)))))

(defun global-set-lst
  (alist wrld)
  (cond ((null alist) wrld)
    (t (global-set-lst (cdr alist)
        (global-set (caar alist) (cadar alist) wrld)))))

(defun cons-term1-mv2
  (fn args form)
  (declare (xargs :guard (and (pseudo-term-listp args) (quote-listp args))))
  (cons-term1-body-mv2))

(defun sublis-var
  (alist form)
  (declare (xargs :guard (and (symbol-alistp alist)
        (pseudo-term-listp (strip-cdrs alist))
        (pseudo-termp form))))
  (mv-let (changedp val)
    (sublis-var1 alist form)
    (declare (ignore changedp))
    val))

(defun sublis-var-lst
  (alist l)
  (declare (xargs :guard (and (symbol-alistp alist)
        (pseudo-term-listp (strip-cdrs alist))
        (pseudo-term-listp l))))
  (mv-let (changedp val)
    (sublis-var1-lst alist l)
    (declare (ignore changedp))
    val))

(defun subcor-var1
  (vars terms var)
  (declare (xargs :guard (and (symbol-listp vars)
        (pseudo-term-listp terms)
        (equal (length vars) (length terms))
        (variablep var))))
  (cond ((endp vars) var)
    ((eq var (car vars)) (car terms))
    (t (subcor-var1 (cdr vars) (cdr terms) var))))

(defun make-reversed-ad-list
  (term ans)
  (cond ((variablep term) (mv ans term))
    ((fquotep term) (mv ans term))
    ((eq (ffn-symb term) 'car) (make-reversed-ad-list (fargn term 1) (cons '#\A ans)))
    ((eq (ffn-symb term) 'cdr) (make-reversed-ad-list (fargn term 1) (cons '#\D ans)))
    (t (mv ans term))))

(defun car-cdr-abbrev-name
  (adr-lst)
  (intern (coerce (cons #\C adr-lst) 'string) "ACL2"))

(defun pretty-parse-ad-list
  (ad-list dr-list n base)
  (cond ((eql n 5) (pretty-parse-ad-list ad-list
        '(#\R)
        1
        (list (car-cdr-abbrev-name dr-list) base)))
    ((endp ad-list) (cond ((eql n 1) base)
        (t (list (car-cdr-abbrev-name dr-list) base))))
    ((eql (car ad-list) #\A) (pretty-parse-ad-list (cdr ad-list)
        '(#\R)
        1
        (list (car-cdr-abbrev-name (cons #\A dr-list)) base)))
    (t (pretty-parse-ad-list (cdr ad-list)
        (cons #\D dr-list)
        (+ 1 n)
        base))))

(defun untranslate-car-cdr-nest
  (term)
  (mv-let (ad-list base)
    (make-reversed-ad-list term nil)
    (cond ((null ad-list) base)
      (t (pretty-parse-ad-list ad-list '(#\R) 1 base)))))

(defun collect-non-trivial-bindings
  (vars vals)
  (cond ((null vars) nil)
    ((eq (car vars) (car vals)) (collect-non-trivial-bindings (cdr vars) (cdr vals)))
    (t (cons (list (car vars) (car vals))
        (collect-non-trivial-bindings (cdr vars) (cdr vals))))))

(defun untranslate-and
  (p q iff-flg)
  (declare (ignore iff-flg))
  (cond ((and (consp q) (eq (car q) 'and)) (cons 'and (cons p (cdr q))))
    (t (list 'and p q))))

(defun untranslate-or
  (p q)
  (cond ((and (consp q) (eq (car q) 'or)) (cons 'or (cons p (cdr q))))
    (t (list 'or p q))))

(defun case-length
  (key term)
  (case-match term
    (('if ('equal key1 ('quote val)) & y) (cond ((and (if (null key)
             (variablep key1)
             (eq key key1))
           (eqlablep val)) (1+ (case-length key1 y)))
        (t 1)))
    (('if ('eql key1 ('quote val)) & y) (cond ((and (if (null key)
             (variablep key1)
             (eq key key1))
           (eqlablep val)) (1+ (case-length key1 y)))
        (t 1)))
    (('if ('member key1 ('quote val)) & y) (cond ((and (if (null key)
             (variablep key1)
             (eq key key1))
           (eqlable-listp val)) (1+ (case-length key1 y)))
        (t 1)))
    (& 1)))

(defun cond-length
  (term)
  (case-match term (('if & & z) (1+ (cond-length z))) (& 1)))

(defun right-associated-args
  (fn term)
  (let ((arg2 (fargn term 2)))
    (cond ((and (nvariablep arg2)
         (not (fquotep arg2))
         (eq fn (ffn-symb arg2))) (cons (fargn term 1) (right-associated-args fn arg2)))
      (t (fargs term)))))

(defun dumb-negate-lit
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (cond ((variablep term) (fcons-term* 'not term))
    ((fquotep term) (cond ((equal term *nil*) *t*) (t *nil*)))
    ((eq (ffn-symb term) 'not) (fargn term 1))
    ((and (eq (ffn-symb term) 'equal)
       (or (equal (fargn term 2) *nil*)
         (equal (fargn term 1) *nil*))) (if (equal (fargn term 2) *nil*)
        (fargn term 1)
        (fargn term 2)))
    (t (fcons-term* 'not term))))

(defun dumb-negate-lit-lst
  (lst)
  (cond ((endp lst) nil)
    (t (cons (dumb-negate-lit (car lst))
        (dumb-negate-lit-lst (cdr lst))))))

(defun accessor-root
  (n term wrld)
  (let ((st (term-stobjs-out term
         (table-alist 'nth-aliases-table wrld)
         wrld)))
    (and st
      (symbolp st)
      (let ((accessor-names (getpropc st 'accessor-names nil wrld)))
        (and accessor-names
          (< n (car (dimensions st accessor-names)))
          (aref1 st accessor-names n))))))

(defun ld-redefinition-action
  (state)
  (f-get-global 'ld-redefinition-action state))

(defun chk-ld-redefinition-action
  (val ctx state)
  (cond ((or (null val)
       (and (consp val)
         (member-eq (car val) '(:query :warn :doit :warn! :doit!))
         (member-eq (cdr val) '(:erase :overwrite)))) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-redefinition-action val))))

(defun set-ld-redefinition-action
  (val state)
  (er-progn (chk-ld-redefinition-action val
      'set-ld-redefinition-action
      state)
    (pprogn (f-put-global 'ld-redefinition-action val state)
      (value val))))

(defun chk-current-package
  (val ctx state)
  (cond ((find-non-hidden-package-entry val
       (known-package-alist state)) (value nil))
    (t (er soft ctx *ld-special-error* 'current-package val))))

(defun set-current-package
  (val state)
  (er-progn (chk-current-package val 'set-current-package state)
    (pprogn (f-put-global 'current-package val state)
      (value val))))

(defun defun-for-state-name
  (name)
  (add-suffix name "-STATE"))

(defun standard-oi
  (state)
  (f-get-global 'standard-oi state))

(defun read-standard-oi
  (state)
  (let ((standard-oi (standard-oi state)))
    (cond ((consp standard-oi) (let ((state (f-put-global 'standard-oi (cdr standard-oi) state)))
          (mv nil (car standard-oi) state)))
      ((null standard-oi) (mv t nil state))
      (t (read-object standard-oi state)))))

(defun chk-standard-oi
  (val ctx state)
  (cond ((and (symbolp val) (open-input-channel-p val :object state)) (value nil))
    ((true-listp val) (value nil))
    ((and (consp val)
       (symbolp (cdr (last val)))
       (open-input-channel-p (cdr (last val)) :object state)) (value nil))
    (t (er soft ctx *ld-special-error* 'standard-oi val))))

(defun set-standard-oi
  (val state)
  (er-progn (chk-standard-oi val 'set-standard-oi state)
    (pprogn (f-put-global 'standard-oi val state) (value val))))

(defun chk-standard-co
  (val ctx state)
  (cond ((and (symbolp val)
       (open-output-channel-p val :character state)) (value nil))
    (t (er soft ctx *ld-special-error* 'standard-co val))))

(defun set-standard-co
  (val state)
  (er-progn (chk-standard-co val 'set-standard-co state)
    (pprogn (f-put-global 'standard-co val state) (value val))))

(defun proofs-co (state) (f-get-global 'proofs-co state))

(defun chk-proofs-co
  (val ctx state)
  (cond ((and (symbolp val)
       (open-output-channel-p val :character state)) (value nil))
    (t (er soft ctx *ld-special-error* 'proofs-co val))))

(defun set-proofs-co
  (val state)
  (er-progn (chk-proofs-co val 'set-proofs-co state)
    (pprogn (f-put-global 'proofs-co val state) (value val))))

(defun chk-trace-co
  (val ctx state)
  (cond ((and (symbolp val)
       (open-output-channel-p val :character state)) (value nil))
    (t (er soft ctx *state-global-error* 'trace-co val))))

(defun set-trace-co
  (val state)
  (er-progn (chk-trace-co val 'set-trace-co state)
    (pprogn (f-put-global 'trace-co val state) (value val))))

(defun illegal-state-ld-prompt
  (channel state)
  (fmt1 "[Illegal-State] ~*0"
    (list (cons #\0
        (list ""
          ">"
          ">"
          ">"
          (make-list-ac (f-get-global 'ld-level state) nil nil))))
    0
    channel
    state
    nil))

(defun ld-pre-eval-filter
  (state)
  (f-get-global 'ld-pre-eval-filter state))

(defun illegal-state-p
  (state)
  (eq (ld-pre-eval-filter state) :illegal-state))

(defun ld-prompt
  (state)
  (cond ((illegal-state-p state) 'illegal-state-ld-prompt)
    (t (f-get-global 'ld-prompt state))))

(defun chk-ld-prompt
  (val ctx state)
  (cond ((or (null val) (eq val t)) (value nil))
    (t (let ((wrld (w state)))
        (cond ((and (symbolp val)
             (equal (arity val wrld) 2)
             (equal (stobjs-in val wrld) '(nil state))
             (equal (stobjs-out val wrld) '(nil state))) (cond ((or (eq val 'brr-prompt)
                 (eq val 'wormhole-prompt)
                 (ttag wrld)) (value nil))
              (t (er soft
                  ctx
                  "It is illegal to set the ld-prompt to ~x0 ~
                                  unless there is an active trust ttag.  See ~
                                  :DOC ~x1."
                  val
                  'ld-prompt))))
          (t (er soft ctx *ld-special-error* 'ld-prompt val)))))))

(defun set-ld-prompt
  (val state)
  (er-progn (chk-ld-prompt val 'set-ld-prompt state)
    (pprogn (f-put-global 'ld-prompt val state) (value val))))

(defun ld-keyword-aliases
  (state)
  (table-alist 'ld-keyword-aliases (w state)))

(defun ld-keyword-aliasesp
  (key val wrld)
  (and (keywordp key)
    (true-listp val)
    (int= (length val) 2)
    (let ((n (car val)) (fn (cadr val)))
      (and (natp n)
        (cond ((and (symbolp fn) (function-symbolp fn wrld)) (equal (arity fn wrld) n))
          ((and (symbolp fn) (getpropc fn 'macro-body nil wrld)) t)
          (t (and (true-listp fn)
              (>= (length fn) 3)
              (<= (length fn) 4)
              (eq (car fn) 'lambda)
              (arglistp (cadr fn))
              (int= (length (cadr fn)) n))))))))

(defun ld-missing-input-ok
  (state)
  (f-get-global 'ld-missing-input-ok state))

(defun chk-ld-missing-input-ok
  (val ctx state)
  (cond ((or (member-eq val '(t nil :warn)) (msgp val)) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-missing-input-ok val))))

(defun set-ld-missing-input-ok
  (val state)
  (er-progn (chk-ld-missing-input-ok val 'set-ld-missing-input-ok state)
    (pprogn (f-put-global 'ld-missing-input-ok val state)
      (value val))))

(defun ld-always-skip-top-level-locals
  (state)
  (f-get-global 'ld-always-skip-top-level-locals state))

(defun chk-ld-always-skip-top-level-locals
  (val ctx state)
  (cond ((member-eq val '(t nil)) (value nil))
    (t (er soft
        ctx
        *ld-special-error*
        'ld-always-skip-top-level-locals
        val))))

(defun set-ld-always-skip-top-level-locals
  (val state)
  (er-progn (chk-ld-always-skip-top-level-locals val
      'set-ld-always-skip-top-level-locals
      state)
    (pprogn (f-put-global 'ld-always-skip-top-level-locals val state)
      (value val))))

(defun new-namep
  (name wrld)
  (declare (xargs :guard (and (symbolp name) (plist-worldp wrld))))
  (let ((redefined (getpropc name 'redefined nil wrld)))
    (cond ((and (consp redefined) (eq (car redefined) :erase)) (not (has-propsp name
            '(redefined global-value table-alist table-guard)
            'current-acl2-world
            wrld
            nil)))
      ((and (consp redefined)
         (or (eq (car redefined) :overwrite)
           (eq (car redefined) :reclassifying-overwrite))) (not (has-propsp name
            '(redefined lemmas
              global-value
              label
              linear-lemmas
              forward-chaining-rules
              eliminate-destructors-rules
              coarsenings
              congruences
              pequivs
              induction-rules
              theorem
              untranslated-theorem
              classes
              const
              theory
              table-guard
              table-alist
              macro-body
              macro-args
              predefined
              tau-pair
              pos-implicants
              neg-implicants
              unevalable-but-known
              signature-rules-form-1
              signature-rules-form-2
              big-switch
              tau-bounders-form-1
              tau-bounders-form-2)
            'current-acl2-world
            wrld
            nil)))
      (t (not (has-propsp name
            '(global-value table-alist table-guard)
            'current-acl2-world
            wrld
            nil))))))

(defun attach-stobj-guard-msg
  (gen impl wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (cond ((not (and (symbolp gen) (symbolp impl))) (msg "The arguments to ~x0 must evaluate to symbols but ~&1 ~
               ~#1~[is not a symbol~/are not symbols~]."
        'attach-stobj
        (append (if (symbolp gen)
            nil
            (list gen))
          (if (symbolp impl)
            nil
            (list impl)))))
    ((not (new-namep gen wrld)) (msg "The name ~x0 is in use, so it cannot serve here as an ~
               attachable stobj.  See :DOC attach-stobj."
        gen))
    ((or (null impl) (getpropc impl 'absstobj-info nil wrld)) nil)
    (t (msg "Since ~x0 is not currently the name of an abstract stobj, it ~
               is not available to be attached to a stobj.  See :DOC ~
               attach-stobj."
        impl))))

(defun attach-stobj-guard
  (gen impl wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (null (attach-stobj-guard-msg gen impl wrld)))

(defun chk-ld-pre-eval-filter
  (val ctx state)
  (cond ((or (member-eq val '(:all :query :illegal-state))
       (and (symbolp val)
         (not (keywordp val))
         (not (equal (symbol-package-name val) *main-lisp-package-name*))
         (new-namep val (w state)))) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-pre-eval-filter val))))

(defun set-ld-pre-eval-filter
  (val state)
  (er-progn (chk-ld-pre-eval-filter val 'set-ld-pre-eval-filter state)
    (pprogn (f-put-global 'ld-pre-eval-filter val state)
      (value val))))

(defun ld-pre-eval-print
  (state)
  (f-get-global 'ld-pre-eval-print state))

(defun chk-ld-pre-eval-print
  (val ctx state)
  (cond ((member-eq val '(nil t :never)) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-pre-eval-print val))))

(defun set-ld-pre-eval-print
  (val state)
  (er-progn (chk-ld-pre-eval-print val 'set-ld-pre-eval-print state)
    (pprogn (f-put-global 'ld-pre-eval-print val state)
      (value val))))

(defun ld-post-eval-print
  (state)
  (f-get-global 'ld-post-eval-print state))

(defun chk-ld-post-eval-print
  (val ctx state)
  (cond ((member-eq val '(nil t :command-conventions)) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-post-eval-print val))))

(defun set-ld-post-eval-print
  (val state)
  (er-progn (chk-ld-post-eval-print val 'set-ld-post-eval-print state)
    (pprogn (f-put-global 'ld-post-eval-print val state)
      (value val))))

(defun ld-error-triples
  (state)
  (f-get-global 'ld-error-triples state))

(defun chk-ld-error-triples
  (val ctx state)
  (cond ((member-eq val '(nil t)) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-error-triples val))))

(defun set-ld-error-triples
  (val state)
  (er-progn (chk-ld-error-triples val 'set-ld-error-triples state)
    (pprogn (f-put-global 'ld-error-triples val state)
      (value val))))

(defun ld-error-action
  (state)
  (f-get-global 'ld-error-action state))

(defun chk-ld-error-action
  (val ctx state)
  (cond ((member-eq val '(:continue :return :return! :error)) (value nil))
    ((and (consp val)
       (eq (car val) :exit)
       (consp (cdr val))
       (natp (cadr val))
       (null (cddr val))) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-error-action val))))

(defun set-ld-error-action
  (val state)
  (er-progn (chk-ld-error-action val 'set-ld-error-action state)
    (pprogn (f-put-global 'ld-error-action val state)
      (value val))))

(defun ld-query-control-alist
  (state)
  (f-get-global 'ld-query-control-alist state))

(defun ld-query-control-alistp
  (val)
  (cond ((atom val) (or (eq val nil) (eq val t)))
    ((and (consp (car val))
       (symbolp (caar val))
       (or (eq (cdar val) nil)
         (eq (cdar val) t)
         (keywordp (cdar val))
         (and (consp (cdar val))
           (keywordp (cadar val))
           (null (cddar val))))) (ld-query-control-alistp (cdr val)))
    (t nil)))

(defun cdr-assoc-query-id
  (id alist)
  (cond ((atom alist) alist)
    ((eq id (caar alist)) (cdar alist))
    (t (cdr-assoc-query-id id (cdr alist)))))

(defun chk-ld-query-control-alist
  (val ctx state)
  (cond ((ld-query-control-alistp val) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-query-control-alist val))))

(defun set-ld-query-control-alist
  (val state)
  (er-progn (chk-ld-query-control-alist val
      'set-ld-query-control-alist
      state)
    (pprogn (f-put-global 'ld-query-control-alist val state)
      (value val))))

(defun ld-verbose (state) (f-get-global 'ld-verbose state))

(defun chk-ld-verbose
  (val ctx state)
  (cond ((or (stringp val) (and (consp val) (stringp (car val)))) (value nil))
    ((member-eq val '(nil t)) (value nil))
    (t (er soft ctx *ld-special-error* 'ld-verbose val))))

(defun set-ld-verbose
  (val state)
  (er-progn (chk-ld-verbose val 'set-ld-verbose state)
    (pprogn (f-put-global 'ld-verbose val state) (value val))))

(defun chk-ld-user-stobjs-modified-warning
  (val ctx state)
  (cond ((member-eq val '(nil t :same)) (value nil))
    (t (er soft
        ctx
        *ld-special-error*
        'ld-user-stobjs-modified-warning
        val))))

(defun set-ld-user-stobjs-modified-warning
  (val state)
  (er-progn (chk-ld-user-stobjs-modified-warning val
      'set-ld-user-stobjs-modified-warning
      state)
    (pprogn (f-put-global 'ld-user-stobjs-modified-warning val state)
      (value val))))

(defun nqthm-to-acl2-fn
  (name state)
  (declare (xargs :guard (symbolp name)))
  (io? temporary
    nil
    (mv erp val state)
    (name)
    (let ((prims (cdr (assoc-eq name *nqthm-to-acl2-primitives*))) (comms (cdr (assoc-eq name *nqthm-to-acl2-commands*))))
      (pprogn (cond (prims (let ((syms (fix-true-list prims)) (info (if (consp prims)
                    (cdr (last prims))
                    prims)))
              (pprogn (if syms
                  (fms "Related ACL2 primitives (use :PE or see documentation ~
                         to learn more):  ~&0.~%"
                    (list (cons #\0 syms))
                    *standard-co*
                    state
                    nil)
                  state)
                (if info
                  (pprogn (fms info (list (cons #\0 syms)) *standard-co* state nil)
                    (newline *standard-co* state))
                  state))))
          (t state))
        (cond (comms (let ((syms (fix-true-list comms)) (info (if (consp comms)
                    (cdr (last comms))
                    comms)))
              (pprogn (if syms
                  (fms "Related ACL2 commands (use :PE or see documentation ~
                         to learn more):  ~&0.~%"
                    (list (cons #\0 syms))
                    *standard-co*
                    state
                    nil)
                  state)
                (if info
                  (pprogn (fms info (list (cons #\0 syms)) *standard-co* state nil)
                    (newline *standard-co* state))
                  state))))
          (t state))
        (if (or prims comms)
          (value :invisible)
          (pprogn (fms "Sorry, but there seems to be no ACL2 notion corresponding ~
                   to the alleged Nqthm notion ~x0.~%"
              (list (cons #\0 name))
              *standard-co*
              state
              nil)
            (value :invisible)))))))

(defun allocate-fixnum-range
  (fixnum-lo fixnum-hi)
  (declare (xargs :guard (and (integerp fixnum-lo)
        (integerp fixnum-hi)
        (>= fixnum-hi fixnum-lo)))
    (type (signed-byte 61) fixnum-lo fixnum-hi))
  (let ((tmp (- fixnum-hi fixnum-lo)))
    (declare (ignore tmp))
    nil))

(defun allegro-allocate-slowly-fn
  (free-bytes-new-other free-bytes-new-pages
    free-percent-new
    expansion-free-percent-old
    expansion-free-percent-new)
  (declare (ignore free-bytes-new-other
      free-bytes-new-pages
      free-percent-new
      expansion-free-percent-old
      expansion-free-percent-new))
  nil)

(defun pstk-bindings-and-args
  (args vars)
  (cond ((endp args) (mv nil nil nil))
    ((endp vars) (mv (er hard
          'pstk-bindings-and-args
          "The ACL2 sources need *pstk-vars* to be extended.")
        nil
        nil))
    (t (mv-let (bindings rest-args fake-args)
        (pstk-bindings-and-args (cdr args) (cdr vars))
        (cond ((eq (car args) 'state) (mv bindings
              (cons (car args) rest-args)
              (cons ''<state> rest-args)))
          ((symbolp (car args)) (mv bindings
              (cons (car args) rest-args)
              (cons (car args) fake-args)))
          (t (mv (cons (list (car vars) (car args)) bindings)
              (cons (car vars) rest-args)
              (cons (car vars) fake-args))))))))

(defun pstack-fn
  (allp state)
  (declare (ignore allp))
  (value :invisible))

(defun verbose-pstack
  (flg-or-list)
  (declare (xargs :guard (or (eq flg-or-list t)
        (eq flg-or-list nil)
        (symbol-listp flg-or-list))))
  flg-or-list)

(defun set-saved-output-token-lst
  (save-flg state)
  (declare (xargs :stobjs state))
  (cond ((member-eq save-flg '(t :all)) (f-put-global 'saved-output-token-lst :all state))
    ((null save-flg) (f-put-global 'saved-output-token-lst nil state))
    ((true-listp save-flg) (f-put-global 'saved-output-token-lst save-flg state))
    (t (prog2$ (er hard
          'set-saved-output
          "Illegal first argument to set-saved-output-token-lst ~
                        (must be ~x0 or a true-listp): ~x1."
          t
          save-flg)
        state))))

(defun set-gag-mode-fn
  (action state)
  (let ((action (if (and (consp action)
           (consp (cdr action))
           (eq (car action) 'quote))
         (cadr action)
         action)))
    (pprogn (case action
        ((t) (pprogn (set-saved-output-token-lst t state)
            (set-print-clause-ids nil)))
        (:goals (pprogn (set-saved-output-token-lst t state)
            (set-print-clause-ids t)))
        ((nil) (pprogn (set-saved-output-token-lst nil state)
            (set-print-clause-ids nil)))
        (otherwise (prog2$ (er hard
              'set-gag-mode
              "Unknown set-gag-mode argument, ~x0"
              action)
            state)))
      (f-put-global 'gag-mode action state))))

(defun pop-inhibit-output-lst-stack
  (state)
  (let ((stk (f-get-global 'inhibit-output-lst-stack state)))
    (cond ((atom stk) state)
      ((atom (car stk)) (f-put-global 'inhibit-output-lst-stack (cdr stk) state))
      (t (pprogn (set-inhibit-output-lst-state (caar stk) state)
          (set-gag-mode (cdar stk))
          (f-put-global 'inhibit-output-lst-stack (cdr stk) state))))))

(defun push-inhibit-output-lst-stack
  (state)
  (f-put-global 'inhibit-output-lst-stack
    (cons (cons (f-get-global 'inhibit-output-lst state)
        (f-get-global 'gag-mode state))
      (f-get-global 'inhibit-output-lst-stack state))
    state))

(defun set-gc-threshold$-fn
  (new-threshold verbose-p)
  (declare (ignorable verbose-p))
  (let ((ctx 'set-gc-threshold$))
    (cond ((not (posp new-threshold)) (er hard
          ctx
          "The argument to set-gc-threshold$ must be a positive integer, so ~
           the value ~x0 is illegal."
          new-threshold))
      (t t))))