ld

(defun default-print-prompt
  (channel state)
  (let ((prompt-memo (f-get-global 'prompt-memo state)))
    (cond ((and prompt-memo
         (equal (access ld-prompt-memo prompt-memo :current-package)
           (f-get-global 'current-package state))
         (equal (access ld-prompt-memo prompt-memo :ld-level)
           (f-get-global 'ld-level state))
         (eq (access ld-prompt-memo prompt-memo :ld-skip-proofsp)
           (f-get-global 'ld-skip-proofsp state))
         (eq (access ld-prompt-memo prompt-memo :mode)
           (and (not (raw-mode-p state))
             (default-defun-mode (w state))))
         (eq (access ld-prompt-memo prompt-memo :not-gc-off)
           (f-get-global 'guard-checking-on state))) (fmt1 "~@0~sr ~@1~*2"
          (access ld-prompt-memo prompt-memo :alist)
          0
          channel
          state
          nil))
      (t (let ((alist (list (cons #\0 (f-get-global 'current-package state))
               (cons #\1 (defun-mode-prompt-string state))
               (cons #\2
                 (list ""
                   ">"
                   ">"
                   ">"
                   (make-list-ac (f-get-global 'ld-level state) nil nil)))
               (cons #\r ""))))
          (pprogn (f-put-global 'prompt-memo
              (make ld-prompt-memo
                :current-package (f-get-global 'current-package state)
                :ld-level (f-get-global 'ld-level state)
                :ld-skip-proofsp (f-get-global 'ld-skip-proofsp state)
                :mode (and (not (raw-mode-p state))
                  (default-defun-mode (w state)))
                :not-gc-off (not (gc-off state))
                :alist alist)
              state)
            (fmt1 "~@0~sr ~@1~*2" alist 0 channel state nil)))))))

(defun print-prompt
  (prompt output-channel state)
  (with-output-forced output-channel
    (col state)
    (let ((prompt-fn (cond ((null prompt) nil)
           ((eq prompt t) (f-get-global 'prompt-function state))
           (t prompt))))
      (cond ((null prompt-fn) (mv 0 state))
        ((eq prompt-fn 'default-print-prompt) (default-print-prompt output-channel state))
        (t (mv-let (erp trans-ans state)
            (trans-eval-default-warning (list prompt-fn (list 'quote output-channel) 'state)
              'print-prompt
              state
              t)
            (cond ((or erp
                 (not (and (equal (car trans-ans) '(nil state))
                     (integerp (car (cdr trans-ans)))))) (fmt1 "~%~%Bad Prompt~%See :DOC ld-prompt>"
                  nil
                  0
                  output-channel
                  state
                  nil))
              (t (mv (car (cdr trans-ans)) state)))))))))

(defun initialize-timers
  (state)
  (pprogn (set-timer 'prove-time '(0) state)
    (set-timer 'print-time '(0) state)
    (set-timer 'proof-tree-time '(0) state)
    (set-timer 'other-time '(0) state)))

(defun world-extended-p
  (old-wrld wrld)
  (cond ((endp wrld) (er hard
        'world-extended-p1
        "Implementation error: Unexpected empty world!"))
    ((eq old-wrld wrld) :trivial)
    (t (let ((trip2 (car wrld)))
        (case-match trip2
          (('acl2-system-table 'table-alist ('empty-event-key . &)) (world-extended-p old-wrld (cdr wrld)))
          (('event-landmark 'global-value . &) (world-extended-p old-wrld (cdr wrld)))
          (('event-index 'global-value . &) (world-extended-p old-wrld (cdr wrld)))
          (('top-level-cltl-command-stack 'global-value . &) (world-extended-p old-wrld (cdr wrld)))
          (& t))))))

(defun maybe-add-command-landmark
  (old-wrld old-default-defun-mode form trans-ans state)
  (let* ((wrld (w state)) (ext (and (member-eq 'state (car trans-ans))
          (not (and (eq (caar wrld) 'command-landmark)
              (eq (cadar wrld) 'global-value)))
          (world-extended-p old-wrld wrld))))
    (cond ((eq ext t) (er-progn (get-and-chk-last-make-event-expansion (cond ((consp form) (case (car form) (time$ (cadr form)) (otherwise form)))
              (t form))
            wrld
            'top-level
            state
            (primitive-event-macros))
          (pprogn (cond ((raw-mode-p state) (warning$ 'top-level
                  "Raw"
                  "The ACL2 world is being modified while in raw ~
                               mode.  See :DOC set-raw-mode.  Further ~
                               computation in this ACL2 session may have some ~
                               surprising results."))
              (t state))
            (set-w 'extension
              (add-command-landmark old-default-defun-mode
                form
                (f-get-global 'connected-book-directory state)
                (f-get-global 'last-make-event-expansion state)
                wrld)
              state)
            (value nil))))
      ((eq ext :trivial) (pprogn (set-w! old-wrld state) (value nil)))
      (t (value nil)))))

(defun replace-last-cdr
  (x val)
  (cond ((atom x) val)
    ((atom (cdr x)) (cons (car x) val))
    (t (cons (car x) (replace-last-cdr (cdr x) val)))))

(defun ld-standard-oi-missing
  (val file-name ld-missing-input-ok ctx state)
  (cond ((eq ld-missing-input-ok t) (value nil))
    (t (let ((msg (msg "~@0  It is likely that the file you requested, ~
                            ~x1, does not exist."
             (msg *ld-special-error* 'standard-oi val)
             file-name)))
        (cond (ld-missing-input-ok (pprogn (warning$ ctx "ld-missing-input" "~@0" msg)
              (value nil)))
          (t (er soft ctx "~@0" msg)))))))

(defun chk-acceptable-ld-fn1-pair
  (pair ld-missing-input-ok ctx state co-string co-channel)
  (let* ((var (car pair)) (val (cdr pair))
      (file-name (and (member-eq var '(standard-oi standard-co proofs-co))
          (stringp val)
          (extend-pathname (f-get-global 'connected-book-directory state)
            val
            state))))
    (case var
      (standard-oi (cond ((and (symbolp val) (open-input-channel-p val :object state)) (value pair))
          ((true-listp val) (value pair))
          ((stringp val) (mv-let (ch state)
              (open-input-channel file-name :object state)
              (cond (ch (value (cons 'standard-oi ch)))
                (t (ld-standard-oi-missing val
                    file-name
                    ld-missing-input-ok
                    ctx
                    state)))))
          ((consp val) (let ((last-cons (last val)))
              (cond ((and (symbolp (cdr last-cons))
                   (open-input-channel-p (cdr last-cons) :object state)) (value pair))
                ((stringp (cdr last-cons)) (let ((file-name (extend-pathname (f-get-global 'connected-book-directory state)
                         (cdr last-cons)
                         state)))
                    (mv-let (ch state)
                      (open-input-channel file-name :object state)
                      (cond (ch (value (cons 'standard-oi (replace-last-cdr val ch))))
                        (t (ld-standard-oi-missing val
                            file-name
                            ld-missing-input-ok
                            ctx
                            state))))))
                (t (er soft ctx *ld-special-error* 'standard-oi val)))))
          (t (er soft ctx *ld-special-error* 'standard-oi val))))
      (standard-co (cond ((and (symbolp val)
             (open-output-channel-p val :character state)) (value pair))
          ((equal val co-string) (value (cons 'standard-co co-channel)))
          ((stringp val) (mv-let (ch state)
              (open-output-channel file-name :character state)
              (cond (ch (value (cons 'standard-co ch)))
                (t (er soft ctx *ld-special-error* 'standard-co val)))))
          (t (er soft ctx *ld-special-error* 'standard-co val))))
      (proofs-co (cond ((and (symbolp val)
             (open-output-channel-p val :character state)) (value pair))
          ((stringp val) (cond ((equal file-name co-string) (value (cons 'proofs-co co-channel)))
              (t (mv-let (ch state)
                  (open-output-channel file-name :character state)
                  (cond (ch (value (cons 'proofs-co ch)))
                    (t (er soft ctx *ld-special-error* 'proofs-co val)))))))
          (t (er soft ctx *ld-special-error* 'proofs-co val))))
      (current-package (er-progn (chk-current-package val ctx state) (value pair)))
      (useless-runes (value pair))
      (ld-skip-proofsp (er-progn (chk-ld-skip-proofsp val ctx state) (value pair)))
      (ld-redefinition-action (er-progn (chk-ld-redefinition-action val ctx state)
          (value pair)))
      (ld-prompt (er-progn (chk-ld-prompt val ctx state) (value pair)))
      (ld-missing-input-ok (er-progn (chk-ld-missing-input-ok val ctx state)
          (value pair)))
      (ld-always-skip-top-level-locals (er-progn (chk-ld-always-skip-top-level-locals val ctx state)
          (value pair)))
      (ld-pre-eval-filter (er-progn (chk-ld-pre-eval-filter val ctx state)
          (value pair)))
      (ld-pre-eval-print (er-progn (chk-ld-pre-eval-print val ctx state)
          (value pair)))
      (ld-post-eval-print (er-progn (chk-ld-post-eval-print val ctx state)
          (value pair)))
      (ld-evisc-tuple (er-progn (chk-evisc-tuple val ctx state) (value pair)))
      (ld-error-triples (er-progn (chk-ld-error-triples val ctx state) (value pair)))
      (ld-error-action (er-progn (chk-ld-error-action val ctx state) (value pair)))
      (ld-query-control-alist (er-progn (chk-ld-query-control-alist val ctx state)
          (value pair)))
      (ld-verbose (er-progn (chk-ld-verbose val ctx state) (value pair)))
      (ld-user-stobjs-modified-warning (er-progn (chk-ld-user-stobjs-modified-warning val ctx state)
          (value pair)))
      (otherwise (er soft
          ctx
          "The variable ~x0 is not an authorized LD special and ~
                hence cannot be bound by LD."
          var)))))

(defun close-channels
  (channel-closing-alist state)
  (cond ((null channel-closing-alist) state)
    (t (pprogn (cond ((eq (cdar channel-closing-alist) 'oi) (cond ((open-input-channel-p (caar channel-closing-alist)
                 :object state) (close-input-channel (caar channel-closing-alist) state))
              (t state)))
          ((eq (cdar channel-closing-alist) 'co) (cond ((open-output-channel-p (caar channel-closing-alist)
                 :character state) (close-output-channel (caar channel-closing-alist) state))
              (t state)))
          (t (let ((temp (er hard
                   'close-channels
                   "The channel ~x0 was tagged with an unimplemented ~
                            channel type, ~x1."
                   (caar channel-closing-alist)
                   (cdar channel-closing-alist))))
              (declare (ignore temp))
              state)))
        (close-channels (cdr channel-closing-alist) state)))))

(defun chk-acceptable-ld-fn1
  (alist ld-missing-input-ok
    ctx
    state
    co-string
    co-channel
    new-alist
    channel-closing-alist
    standard-oi0)
  (cond ((null alist) (er-let* ((u-r-pair (value (assoc-eq 'useless-runes new-alist))) (useless-runes (let* ((useless-runes-r/w (cdr u-r-pair)) (useless-runes-r/w-p (consp u-r-pair)))
              (initial-useless-runes standard-oi0
                useless-runes-r/w
                useless-runes-r/w-p
                t
                'ld
                state))))
        (let ((new-alist (put-assoc-eq 'useless-runes useless-runes new-alist)))
          (value (cons new-alist channel-closing-alist)))))
    (t (mv-let (erp pair state)
        (chk-acceptable-ld-fn1-pair (car alist)
          ld-missing-input-ok
          ctx
          state
          co-string
          co-channel)
        (cond (erp (pprogn (close-channels channel-closing-alist state)
              (mv t nil state)))
          ((null pair) (assert$ (eq (caar alist) 'standard-oi)
              (pprogn (close-channels channel-closing-alist state)
                (mv nil nil state))))
          (t (chk-acceptable-ld-fn1 (cdr alist)
              ld-missing-input-ok
              ctx
              state
              (cond ((and (null co-string)
                   (or (eq (car pair) 'standard-co) (eq (car pair) 'proofs-co))
                   (stringp (cdr (car alist)))) (extend-pathname (f-get-global 'connected-book-directory state)
                    (cdr (car alist))
                    state))
                (t co-string))
              (cond ((and (null co-channel)
                   (or (eq (car pair) 'standard-co) (eq (car pair) 'proofs-co))
                   (stringp (cdr (car alist)))) (cdr pair))
                (t co-channel))
              (cons pair new-alist)
              (cond ((eq (car pair) 'standard-oi) (cond ((stringp (cdr (car alist))) (cons (cons (cdr pair) 'oi) channel-closing-alist))
                    ((and (consp (cdr (car alist)))
                       (stringp (cdr (last (cdr (car alist)))))) (cons (cons (cdr (last (cdr pair))) 'oi)
                        channel-closing-alist))
                    (t channel-closing-alist)))
                ((and (or (eq (car pair) 'standard-co) (eq (car pair) 'proofs-co))
                   (stringp (cdr (car alist)))) (cons (cons (cdr pair) 'co) channel-closing-alist))
                (t channel-closing-alist))
              standard-oi0)))))))

(defun chk-acceptable-ld-fn
  (alist standard-oi0 state)
  (let ((ctx 'ld))
    (er-progn (cond ((or (null (f-boundp-global 'current-acl2-world state))
           (null (w state))) (er soft
            ctx
            "The theorem prover's database has not yet been initialized.  To ~
            initialize ACL2 to its full theory, which currently takes about 3 ~
            minutes on a Sparc 2 (Dec. 1992), invoke (initialize-acl2) from ~
            Common Lisp."))
        (t (value nil)))
      (cond ((symbol-alistp alist) (value nil))
        (t (er soft
            ctx
            "The argument to ld-fn must be a symbol-alistp and ~x0 is ~
                   not."
            alist)))
      (cond ((assoc-eq 'standard-oi alist) (value nil))
        (t (er soft
            ctx
            "The alist argument to ld-fn must specify a value ~
                   for 'standard-oi and ~x0 does not."
            alist)))
      (cond ((not (duplicate-keysp-eq alist)) (value nil))
        (t (er soft
            ctx
            "The alist argument to ld-fn must contain no duplications ~
                   among the LD specials to be bound.  Your alist contains ~
                   duplicate values for ~&0."
            (duplicates (strip-cars alist)))))
      (chk-acceptable-ld-fn1 alist
        (cdr (assoc-eq 'ld-missing-input-ok alist))
        ctx
        state
        nil
        nil
        nil
        nil
        standard-oi0))))

(defun f-put-ld-specials
  (alist uurp state)
  (cond ((null alist) (cond (uurp (update-useless-runes nil state)) (t state)))
    ((eq (caar alist) 'useless-runes) (pprogn (cond (uurp (update-useless-runes (cdar alist) state))
          (t (f-put-global 'useless-runes (cdar alist) state)))
        (f-put-ld-specials (cdr alist) nil state)))
    (t (pprogn (case (caar alist)
          (standard-oi (f-put-global 'standard-oi (cdar alist) state))
          (standard-co (f-put-global 'standard-co (cdar alist) state))
          (proofs-co (f-put-global 'proofs-co (cdar alist) state))
          (current-package (f-put-global 'current-package (cdar alist) state))
          (ld-skip-proofsp (f-put-global 'ld-skip-proofsp (cdar alist) state))
          (ld-redefinition-action (f-put-global 'ld-redefinition-action (cdar alist) state))
          (ld-prompt (f-put-global 'ld-prompt (cdar alist) state))
          (ld-missing-input-ok (f-put-global 'ld-missing-input-ok (cdar alist) state))
          (ld-always-skip-top-level-locals (f-put-global 'ld-always-skip-top-level-locals
              (cdar alist)
              state))
          (ld-pre-eval-filter (if (and (f-boundp-global 'ld-pre-eval-filter state)
                (eq (f-get-global 'ld-pre-eval-filter state) :illegal-state))
              state
              (f-put-global 'ld-pre-eval-filter (cdar alist) state)))
          (ld-pre-eval-print (f-put-global 'ld-pre-eval-print (cdar alist) state))
          (ld-post-eval-print (f-put-global 'ld-post-eval-print (cdar alist) state))
          (ld-evisc-tuple (f-put-global 'ld-evisc-tuple (cdar alist) state))
          (ld-error-triples (f-put-global 'ld-error-triples (cdar alist) state))
          (ld-error-action (f-put-global 'ld-error-action (cdar alist) state))
          (ld-query-control-alist (f-put-global 'ld-query-control-alist (cdar alist) state))
          (ld-verbose (f-put-global 'ld-verbose (cdar alist) state))
          (ld-user-stobjs-modified-warning (if (eq (cdar alist) :same)
              state
              (f-put-global 'ld-user-stobjs-modified-warning
                (cdar alist)
                state)))
          (otherwise (let ((x (er hard
                   'f-put-ld-specials
                   "Someone is using ~x0 as an unauthorized LD-special."
                   (caar alist))))
              (declare (ignore x))
              state)))
        (f-put-ld-specials (cdr alist) uurp state)))))

(defun f-get-ld-specials
  (state)
  (list (cons 'standard-oi (f-get-global 'standard-oi state))
    (cons 'standard-co (f-get-global 'standard-co state))
    (cons 'proofs-co (f-get-global 'proofs-co state))
    (cons 'current-package
      (f-get-global 'current-package state))
    (cons 'useless-runes (f-get-global 'useless-runes state))
    (cons 'ld-skip-proofsp
      (f-get-global 'ld-skip-proofsp state))
    (cons 'ld-redefinition-action
      (f-get-global 'ld-redefinition-action state))
    (cons 'ld-prompt (f-get-global 'ld-prompt state))
    (cons 'ld-missing-input-ok
      (f-get-global 'ld-missing-input-ok state))
    (cons 'ld-always-skip-top-level-locals
      (f-get-global 'ld-always-skip-top-level-locals state))
    (cons 'ld-pre-eval-filter
      (f-get-global 'ld-pre-eval-filter state))
    (cons 'ld-pre-eval-print
      (f-get-global 'ld-pre-eval-print state))
    (cons 'ld-post-eval-print
      (f-get-global 'ld-post-eval-print state))
    (cons 'ld-evisc-tuple (f-get-global 'ld-evisc-tuple state))
    (cons 'ld-error-triples
      (f-get-global 'ld-error-triples state))
    (cons 'ld-error-action
      (f-get-global 'ld-error-action state))
    (cons 'ld-query-control-alist
      (f-get-global 'ld-query-control-alist state))
    (cons 'ld-verbose (f-get-global 'ld-verbose state))
    (cons 'ld-user-stobjs-modified-warning
      (f-get-global 'ld-user-stobjs-modified-warning state))))

(defun ld-read-keyword-command1
  (n state)
  (cond ((= n 0) (value nil))
    (t (mv-let (eofp obj state)
        (read-standard-oi state)
        (cond (eofp (er soft
              'ld-read-keyword-command
              "Unfinished keyword command at eof on (standard-oi ~
                          state)."))
          (t (er-let* ((rst (ld-read-keyword-command1 (1- n) state)))
              (value (cons (list 'quote obj) rst)))))))))

(defun exit-ld (state) (value :q))

(defun ld-read-keyword-command
  (key state)
  (let ((temp (assoc-eq key (ld-keyword-aliases state))))
    (cond (temp (mv-let (erp args state)
          (ld-read-keyword-command1 (cadr temp) state)
          (cond (erp (mv t nil nil state))
            (t (mv nil
                (cons key (strip-cadrs args))
                (cons (caddr temp) args)
                state)))))
      ((eq key :q) (mv nil '(:q) '(exit-ld state) state))
      (t (let* ((sym (intern (symbol-name key) "ACL2")) (wrld (w state))
            (len (cond ((function-symbolp sym wrld) (length (formals sym wrld)))
                ((getpropc sym 'macro-body nil wrld) (macro-minimal-arity sym
                    `(:error "See LD-READ-KEYWORD-COMMAND.")
                    wrld))
                (t nil))))
          (cond (len (mv-let (erp args state)
                (ld-read-keyword-command1 len state)
                (cond (erp (mv t nil nil state))
                  (t (mv nil (cons key (strip-cadrs args)) (cons sym args) state)))))
            (t (mv-let (erp val state)
                (er soft 'ld "Unrecognized keyword command ~x0." key)
                (declare (ignore erp val))
                (mv t nil nil state)))))))))

(defun ld-fix-command (form) form)

(defun ld-read-command
  (state)
  (pprogn (brr-evisc-tuple-oracle-update state)
    (prog2$ (and (int= (f-get-global 'ld-level state) 1)
        (semi-initialize-brr-wormhole state))
      (mv-let (eofp val state)
        (read-standard-oi state)
        (pprogn (cond ((int= (f-get-global 'ld-level state) 1) (let ((last-index (iprint-last-index state)))
                (cond ((> last-index (iprint-soft-bound state)) (rollover-iprint-ar nil last-index state))
                  (t state))))
            (t state))
          (cond (eofp (mv t nil nil nil state))
            ((keywordp val) (mv-let (erp keyp form state)
                (ld-read-keyword-command val state)
                (mv nil erp keyp form state)))
            ((stringp val) (let ((upval (string-upcase val)))
                (cond ((find-non-hidden-package-entry upval
                     (global-val 'known-package-alist (w state))) (mv nil nil nil `(in-package ,UPVAL) state))
                  (t (mv nil nil nil val state)))))
            (t (mv nil nil nil (ld-fix-command val) state))))))))

(defun ld-print-command
  (keyp form col state)
  (with-base-10 (mv-let (col state)
      (cond ((not (eq (ld-pre-eval-print state) t)) (mv col state))
        (keyp (fmt1 "~*0~|"
            (list (cons #\0 (list "" "~x*" "~x* " "~x* " keyp)))
            col
            (standard-co state)
            state
            (ld-evisc-tuple state)))
        (t (fmt1 "~q0~|"
            (list (cons #\0 form))
            col
            (standard-co state)
            state
            (ld-evisc-tuple state))))
      (declare (ignore col))
      state)))

(defun ld-filter-command
  (form state)
  (let ((filter (ld-pre-eval-filter state)))
    (cond ((eq filter :all) (value t))
      ((eq filter :query) (acl2-query :filter '("~#0~[~Y12?~/Eval?~]" :y t
            :n nil
            :r :return :q :error :? ("We are in the LD read-eval-print loop, ~
                              processing the forms in standard-oi.  The ~
                              form printed above is one of those forms.  Do ~
                              you want to evaluate it (Y) or not (N)?   You ~
                              may also answer R, meaning ``return ~
                              immediately from LD (without reading or ~
                              evaluating any more forms)'' or Q meaning ~
                              ``return immediately from LD, signaling an ~
                              error.''" :y t
              :n nil
              :r :return :q :error))
          (list (cons #\0
              (if (eq (ld-pre-eval-print state) t)
                1
                0))
            (cons #\1 form)
            (cons #\2 (ld-evisc-tuple state)))
          state))
      ((eq filter :illegal-state) (cond ((equal form '(exit-ld state)) (value t))
          ((equal form '(continue-from-illegal-state)) (er-progn (continue-from-illegal-state) (value t)))
          (t (er soft
              'ld-filter-command
              "You are still in an illegal state!  See :DOC ~
                         illegal-state.  You can submit the ~
                         form~|:CONTINUE-FROM-ILLEGAL-STATE~|to continue -- ~
                         AT YOUR OWN RISK."))))
      (t (value t)))))

(defun evisceration-stobj-mark
  (name val)
  (cond ((eq name 'state) *evisceration-state-mark*)
    ((eq name :df) (and (rationalp val)
        (cons *evisceration-mark*
          (concatenate 'string "#d" (df-string (to-df val))))))
    (t (cons *evisceration-mark* (stobj-print-name name)))))

(defun evisceration-stobj-marks1
  (stobjs-flags lst)
  (cond ((endp stobjs-flags) nil)
    ((car stobjs-flags) (cons (evisceration-stobj-mark (car stobjs-flags) (car lst))
        (evisceration-stobj-marks1 (cdr stobjs-flags) (cdr lst))))
    (t (cons nil
        (evisceration-stobj-marks1 (cdr stobjs-flags) (cdr lst))))))

(defun evisceration-stobj-marks
  (stobjs-flags lst)
  (cond ((equal stobjs-flags *error-triple-sig*) *evisceration-error-triple-marks*)
    ((equal stobjs-flags '(nil)) '(nil))
    ((equal stobjs-flags '(:df)) (and (rationalp lst)
        (list (evisceration-stobj-mark :df lst))))
    ((null (cdr stobjs-flags)) (assert$ (symbolp lst)
        (list (evisceration-stobj-mark (car stobjs-flags) lst))))
    (t (evisceration-stobj-marks1 stobjs-flags lst))))

(defun ld-print-results
  (trans-ans state)
  (let ((flg (ld-post-eval-print state)) (output-channel (standard-co state)))
    (cond ((null flg) state)
      (t (let* ((stobjs-out (car trans-ans)) (valx (cdr trans-ans))
            (evisc-tuple (ld-evisc-tuple state))
            (evisc-alist (world-evisceration-alist state (car evisc-tuple)))
            (print-level (cadr evisc-tuple))
            (print-length (caddr evisc-tuple))
            (hiding-cars (cadddr evisc-tuple)))
          (mv-let (eviscerated-valx state)
            (eviscerate-stobjs-top (evisceration-stobj-marks stobjs-out valx)
              valx
              print-level
              print-length
              evisc-alist
              (table-alist 'evisc-table (w state))
              hiding-cars
              state)
            (cond ((and (eq flg :command-conventions)
                 (ld-error-triples state)
                 (or (equal stobjs-out *error-triple-sig*)
                   (equal stobjs-out *error-triple-df-sig*))) (cond ((eq (cadr valx) :invisible) state)
                  (t (pprogn (if (stringp (f-get-global 'triple-print-prefix state))
                        (princ$ (f-get-global 'triple-print-prefix state)
                          output-channel
                          state)
                        state)
                      (ppr (cadr eviscerated-valx)
                        (if (stringp (f-get-global 'triple-print-prefix state))
                          (length (f-get-global 'triple-print-prefix state))
                          0)
                        output-channel
                        state
                        t)
                      (newline output-channel state)))))
              (t (pprogn (ppr eviscerated-valx 0 output-channel state t)
                  (newline output-channel state))))))))))

(defun ld-print-prompt
  (state)
  (mv-let (col state)
    (print-prompt (ld-prompt state) (standard-co state) state)
    (cond ((and (eq (standard-oi state) *standard-oi*)
         (not (eq (standard-co state) *standard-co*))) (mv-let (irrel-col state)
          (print-prompt (ld-prompt state) *standard-co* state)
          (declare (ignore irrel-col))
          (mv col state)))
      (t (mv col state)))))

(defun ld-return-error
  (state)
  (let ((action (ld-error-action state)))
    (cond ((eq action :return!) (mv :return (list :stop-ld (f-get-global 'ld-level state))
          state))
      ((and (consp action) (eq (car action) :exit)) (mv action (good-bye-fn (cadr action)) state))
      (t (mv action :error state)))))

(defun initialize-accumulated-warnings nil nil)

(defun ld-history
  (state)
  (declare (xargs :stobjs state))
  (f-get-global 'ld-history state))

(defun ld-history-entry-input
  (x)
  (declare (xargs :guard (weak-ld-history-entry-p x)))
  (access ld-history-entry x :input))

(defun ld-history-entry-error-flg
  (x)
  (declare (xargs :guard (weak-ld-history-entry-p x)))
  (access ld-history-entry x :error-flg))

(defun ld-history-entry-stobjs-out/value
  (x)
  (declare (xargs :guard (weak-ld-history-entry-p x)))
  (access ld-history-entry x :stobjs-out/value))

(defun ld-history-entry-stobjs-out
  (x)
  (declare (xargs :guard (weak-ld-history-entry-p x)))
  (and (not (access ld-history-entry x :error-flg))
    (let ((y (access ld-history-entry x :stobjs-out/value)))
      (and (consp y) (car y)))))

(defun ld-history-entry-value
  (x)
  (declare (xargs :guard (weak-ld-history-entry-p x)))
  (and (not (access ld-history-entry x :error-flg))
    (let ((y (access ld-history-entry x :stobjs-out/value)))
      (and (consp y) (cdr y)))))

(defun ld-history-entry-user-data
  (x)
  (declare (xargs :guard (weak-ld-history-entry-p x)))
  (access ld-history-entry x :user-data))

(defun set-ld-history-entry-user-data-default
  (input error-flg stobjs-out/value state)
  (declare (ignore input error-flg stobjs-out/value state)
    (xargs :stobjs state))
  nil)

(defun adjust-ld-history
  (x state)
  (declare (xargs :guard (and (or (and (integerp x) (not (zerop x))) (booleanp x))
        (consp (f-get-global 'ld-history state)))))
  (let* ((ld-history (f-get-global 'ld-history state)) (len (len ld-history))
      (end (cdr ld-history)))
    (cond ((and (integerp x) (not (zerop x))) (cond ((null end) (prog2$ (hard-error 'adjust-ld-history
                "It is illegal to call ~x0 on an integer argument ~
                           here, because the ld-history is in single-entry ~
                           mode.  See :DOC ld-history."
                (list (cons #\0 'adjust-ld-history)))
              (value :error)))
          (t (let ((abs (abs x)))
              (cond ((< abs len) (let* ((new-len (if (< 0 x)
                         x
                         (- len abs))) (new-ld-history (cond ((int= new-len 1) (list (car ld-history) *empty-ld-history-entry*))
                          (t (take new-len (fix-true-list ld-history))))))
                    (pprogn (f-put-global 'ld-history new-ld-history state)
                      (value `(:ld-history-truncated :old-length ,LEN
                          :new-length ,NEW-LEN)))))
                (t (value `(:no-change :length ,LEN))))))))
      ((and (eq x t) end) (value `(:no-change :length ,LEN)))
      ((and (eq x nil) (null end)) (value `(:no-change :length ,LEN)))
      ((eq x t) (pprogn (f-put-global 'ld-history
            (list (car ld-history) *empty-ld-history-entry*)
            state)
          (value '(:saving-ld-history t))))
      ((eq x nil) (pprogn (f-put-global 'ld-history (list (car ld-history)) state)
          (value '(:saving-ld-history nil))))
      (t (prog2$ (illegal 'adjust-ld-history
            "Illegal value for ~x0: ~x1.  Note: Normally ~
                      guard-checking would avoid this error.  See :DOC ~
                      ld-history."
            (list (cons #\0 'adjust-ld-history) (cons #\1 x)))
          (value :error))))))

(defun extend-ld-history
  (input error-flg trans-ans state)
  (declare (xargs :stobjs state
      :guard (consp (f-get-global 'ld-history state))))
  (let* ((ld-history (f-get-global 'ld-history state)) (new-entry (make ld-history-entry
          :input input
          :error-flg error-flg
          :stobjs-out/value trans-ans
          :user-data (set-ld-history-entry-user-data input
            error-flg
            trans-ans
            state))))
    (f-put-global 'ld-history
      (cond ((eq (cdr ld-history) nil) (list new-entry))
        ((and (consp (cdr ld-history))
           (equal (cadr ld-history) *empty-ld-history-entry*)) (list new-entry (car ld-history)))
        (t (cons new-entry ld-history)))
      state)))

(defun ld-read-eval-print
  (state)
  (pprogn (cond ((<= (f-get-global 'ld-level state) 1) (print-deferred-ttag-notes-summary state))
      (t state))
    (f-put-global 'raw-guard-warningp t state)
    (chk-absstobj-invariants state)
    (mv-let (col state)
      (if (and (eql (f-get-global 'in-verify-flg state) 1)
          (eql (f-get-global 'ld-level state) 1)
          (not (illegal-state-p state)))
        (mv 0 state)
        (ld-print-prompt state))
      (mv-let (eofp erp keyp form state)
        (let ((in-verify-flg (f-get-global 'in-verify-flg state)))
          (cond (in-verify-flg (pprogn (f-put-global 'in-verify-flg nil state)
                (cond ((and (eql (f-get-global 'ld-level state) 1)
                     (eql in-verify-flg 1)
                     (not (illegal-state-p state))) (pprogn (print-re-entering-proof-builder nil state)
                      (mv nil nil nil '(verify) state)))
                  (t (ld-read-command state)))))
            (t (ld-read-command state))))
        (cond (eofp (cond ((ld-prompt state) (pprogn (princ$ "Bye." (standard-co state) state)
                  (newline (standard-co state) state)
                  (prog2$ (and (equal (standard-oi state) *standard-oi*) (good-bye))
                    state)
                  (mv :return :eof state)))
              (t (mv :return :eof state))))
          (erp (ld-return-error state))
          (t (pprogn (ld-print-command keyp form col state)
              (mv-let (erp ans state)
                (ld-filter-command form state)
                (cond (erp (ld-return-error state))
                  ((null ans) (mv :continue nil state))
                  ((eq ans :error) (mv :error nil state))
                  ((eq ans :return) (mv :return :filter state))
                  (t (assert$ (eq ans t)
                      (pprogn (cond ((<= (f-get-global 'ld-level state) 1) (prog2$ (initialize-accumulated-warnings)
                              (initialize-timers state)))
                          (t state))
                        (f-put-global 'last-make-event-expansion nil state)
                        (let* ((old-wrld (w state)) (old-default-defun-mode (default-defun-mode old-wrld))
                            (in-local-flg (f-get-global 'in-local-flg state)))
                          (mv-let (error-flg trans-ans state)
                            (revert-world-on-error (mv-let (error-flg trans-ans state)
                                (if (raw-mode-p state)
                                  (acl2-raw-eval form state)
                                  (trans-eval-default-warning form 'top-level state t))
                                (let ((form0 (if (and in-local-flg
                                         (equal (car trans-ans) *error-triple-sig*)
                                         (not (and (consp form) (eq (car form) 'local))))
                                       (list 'local form)
                                       form)))
                                  (pprogn (extend-ld-history form0 error-flg trans-ans state)
                                    (cond (error-flg (mv t nil state))
                                      ((and (ld-error-triples state)
                                         (or (equal (car trans-ans) *error-triple-sig*)
                                           (equal (car trans-ans) *error-triple-df-sig*))
                                         (car (cdr trans-ans))) (mv t nil state))
                                      (t (er-progn (maybe-add-command-landmark old-wrld
                                            old-default-defun-mode
                                            form0
                                            trans-ans
                                            state)
                                          (mv nil trans-ans state))))))))
                            (cond (error-flg (ld-return-error state))
                              ((and (equal (car trans-ans) *error-triple-sig*)
                                 (eq (cadr (cdr trans-ans)) :q)) (mv :return :exit state))
                              (t (pprogn (ld-print-results trans-ans state)
                                  (let ((action (ld-error-action state)))
                                    (cond ((and (ld-error-triples state)
                                         (not (eq action :continue))
                                         (equal (car trans-ans) *error-triple-sig*)
                                         (let ((val (cadr (cdr trans-ans))))
                                           (and (consp val) (eq (car val) :stop-ld)))) (cond ((and (consp action) (eq (car action) :exit)) (mv action (good-bye-fn (cadr action)) state))
                                          (t (mv :return (list* :stop-ld (f-get-global 'ld-level state)
                                                (cdr (cadr (cdr trans-ans))))
                                              state))))
                                      (t (let ((filter (ld-pre-eval-filter state)))
                                          (cond ((and (not (eq filter :all))
                                               (not (eq filter :query))
                                               (not (eq filter :illegal-state))
                                               (not (new-namep filter (w state)))) (er-progn (set-ld-pre-eval-filter :all state)
                                                (mv :return :filter state)))
                                            (t (mv :continue nil state))))))))))))))))))))))))

(defun ld-loop
  (state)
  (mv-let (signal val state)
    (ld-read-eval-print state)
    (cond ((eq signal :continue) (ld-loop state))
      ((eq signal :return) (value val))
      (t (mv t nil state)))))

(defun get-directory-of-file
  (p)
  (let* ((p-rev (reverse p)) (posn (position *directory-separator* p-rev)))
    (if posn
      (subseq p 0 (1- (- (length p) posn)))
      (er hard
        'get-directory-of-file
        "Implementation error!  Unable to get directory for file ~x0."
        p))))

(defun update-cbd
  (standard-oi0 state)
  (let ((old-cbd (f-get-global 'connected-book-directory state)))
    (cond ((and old-cbd
         (stringp standard-oi0)
         (position *directory-separator* standard-oi0)) (let* ((os (os (w state))) (filename-dir (expand-tilde-to-user-home-dir (concatenate 'string
                  (get-directory-of-file standard-oi0)
                  *directory-separator-string*)
                os
                'update-cbd
                state)))
          (set-cbd-state (if (absolute-pathname-string-p filename-dir nil os)
              filename-dir
              (our-merge-pathnames old-cbd filename-dir))
            state)))
      (t state))))

(defun ld-fn-body
  (standard-oi0 new-ld-specials-alist state)
  (pprogn (f-put-ld-specials new-ld-specials-alist nil state)
    (update-cbd standard-oi0 state)
    (cond ((ld-verbose state) (cond ((eq (ld-verbose state) t) (fms (if (eq standard-oi0 *standard-oi*)
                "ACL2 loading *standard-oi*.~%"
                "ACL2 loading ~x0.~%")
              (list (cons #\0
                  (cond ((consp standard-oi0) (kwote standard-oi0))
                    (t standard-oi0))))
              (standard-co state)
              state
              (ld-evisc-tuple state)))
          (t (with-base-10 (fms "~@0"
                (list (cons #\0 (ld-verbose state))
                  (cons #\v (f-get-global 'acl2-version state))
                  (cons #\l (f-get-global 'ld-level state))
                  (cons #\c (f-get-global 'connected-book-directory state))
                  (cons #\b (project-dir-alist (w state))))
                (standard-co state)
                state
                (ld-evisc-tuple state))))))
      (t state))
    (mv-let (erp val state)
      (ld-loop state)
      (pprogn (cond ((eq (ld-verbose state) t) (fms (if (eq standard-oi0 *standard-oi*)
                "Finished loading *standard-oi*.~%"
                "Finished loading ~x0.~%")
              (list (cons #\0
                  (cond ((consp standard-oi0) (kwote standard-oi0))
                    (t standard-oi0))))
              (standard-co state)
              state
              (ld-evisc-tuple state)))
          (t state))
        (mv erp val state)))))

(defun ld-fn1
  (standard-oi0 alist state bind-flg)
  (let* ((old-ld-level (f-get-global 'ld-level state)) (new-ld-level (1+ old-ld-level))
      (old-cbd (f-get-global 'connected-book-directory state)))
    (er-let* ((pair (chk-acceptable-ld-fn alist standard-oi0 state)))
      (cond ((null pair) (value :missing-input))
        (t (let ((old-ld-specials-alist (f-get-ld-specials state)) (new-ld-specials-alist (car pair))
              (channel-closing-alist (cdr pair)))
            (if bind-flg
              (acl2-unwind-protect "ld-fn"
                (pprogn (f-put-global 'ld-level new-ld-level state)
                  (ld-fn-body standard-oi0 new-ld-specials-alist state))
                (pprogn (f-put-global 'ld-level old-ld-level state)
                  (set-cbd-state old-cbd state)
                  (f-put-ld-specials old-ld-specials-alist t state)
                  (close-channels channel-closing-alist state))
                (pprogn (f-put-global 'ld-level old-ld-level state)
                  (set-cbd-state old-cbd state)
                  (f-put-ld-specials old-ld-specials-alist t state)
                  (close-channels channel-closing-alist state)))
              (acl2-unwind-protect "ld-fn"
                (pprogn (f-put-global 'ld-level new-ld-level state)
                  (ld-fn-body standard-oi0 new-ld-specials-alist state))
                (f-put-global 'ld-level old-ld-level state)
                (f-put-global 'ld-level old-ld-level state)))))))))

(defun ld-fn-alist
  (alist bind-flg state)
  (let* ((standard-oi (cdr (assoc 'standard-oi alist))) (dir (cdr (assoc 'dir alist)))
      (ctx 'ld)
      (os (os (w state)))
      (alist (if (null bind-flg)
          (put-assoc-eq 'useless-runes nil alist)
          alist)))
    (cond ((and (stringp standard-oi) dir) (let ((standard-oi-expanded (expand-tilde-to-user-home-dir standard-oi os ctx state)))
          (cond ((absolute-pathname-string-p standard-oi-expanded nil os) (er hard
                ctx
                "It is illegal to supply a :DIR argument to LD here ~
                         because the supplied filename,~|~%  ~s0,~|~%is an ~
                         absolute pathname (see :DOC pathname), and hence ~
                         there is no reasonable way to merge it with a :DIR ~
                         value."
                standard-oi))
            (t (let ((resolve-dir (include-book-dir-with-chk hard 'ld dir)))
                (cond (resolve-dir (put-assoc-eq 'standard-oi
                      (our-merge-pathnames resolve-dir standard-oi-expanded)
                      (remove1-assoc-eq 'dir alist)))
                  (t alist)))))))
      ((and (not (stringp standard-oi)) dir) (er hard
          ctx
          "It is illegal to supply a :DIR argument to LD here because ~
                the first argument of the LD call, ~x0, is not a string.  ~
                Such an argument would be ignored anyhow, so you probably ~
                should consider simply removing that :DIR argument.  See :DOC ~
                ld."
          standard-oi))
      ((assoc-eq 'dir alist) (remove1-assoc-eq 'dir alist))
      (t alist))))

(defun ld-fn0
  (alist state bind-flg)
  (let* ((alist (ld-fn-alist alist bind-flg state)) (standard-oi0 (cdr (assoc-eq 'standard-oi alist))))
    (ld-fn1 standard-oi0 alist state bind-flg)))

(defun ld-fn
  (alist state bind-flg)
  (let ((alist (if (assoc-eq 'ld-error-action alist)
         alist
         (acons 'ld-error-action
           (let ((action (ld-error-action state)))
             (if (and (consp action) (eq (car action) :exit))
               action
               :return!))
           alist))))
    (cond ((not (f-get-global 'ld-okp state)) (er soft
          'ld
          "It is illegal to call LD in this context.  See :DOC ~
           calling-ld-in-bad-contexts."))
      (t (ld-fn0 alist state bind-flg)))))

(defun wormhole-prompt
  (channel state)
  (the2s (unsigned-byte 60)
    (fmt1 "Wormhole ~s0~sr ~@1~*2"
      (list (cons #\0 (f-get-global 'current-package state))
        (cons #\1 (defun-mode-prompt-string state))
        (cons #\r "")
        (cons #\2
          (list ""
            ">"
            ">"
            ">"
            (make-list-ac (- (f-get-global 'ld-level state) 1) nil nil))))
      0
      channel
      state
      nil)))

(defun reset-ld-specials-fn
  (reset-channels-flg state)
  (f-put-ld-specials (cond (reset-channels-flg *initial-ld-special-bindings*)
      (t (cdddr *initial-ld-special-bindings*)))
    nil
    state))

(defun maybe-reset-defaults-table1
  (key pre-defaults-tbl post-defaults-tbl state)
  (let* ((pre-val (cdr (assoc-eq key pre-defaults-tbl))) (post-val (cdr (assoc-eq key post-defaults-tbl)))
      (cmd `(table acl2-defaults-table ,KEY ',PRE-VAL)))
    (if (equal pre-val post-val)
      (value nil)
      (er-let* ((ans (acl2-query :ubt-defaults '("The default ~s0 was ~x1 before undoing, but will be ~x2 after ~
             undoing unless the command ~x3 is executed.  Do you wish to ~
             re-execute this command after the :ubt?" :y t
               :n nil
               :? ("If you answer in the affirmative, then the command ~X34 will ~
                 be executed on your behalf.  This will make the default ~s0 ~
                 equal to ~x1, which is what it was just before your :ubt ~
                 command was executed.  Otherwise, the default ~s0 will be ~
                 what it is in the world after the undoing, namely ~x2.  See ~
                 also :DOC acl2-defaults-table." :y t
                 :n nil))
             (list (cons #\0 (string-downcase (symbol-name key)))
               (cons #\1 pre-val)
               (cons #\2 post-val)
               (cons #\3 cmd)
               (cons #\4 nil))
             state)))
        (if ans
          (ld (list cmd)
            :ld-pre-eval-filter :all :ld-pre-eval-print t
            :ld-post-eval-print :command-conventions :ld-evisc-tuple (abbrev-evisc-tuple state)
            :ld-error-triples t
            :ld-error-action :return)
          (value nil))))))

(defun maybe-reset-defaults-table2
  (keys pre-defaults-tbl post-defaults-tbl state)
  (if keys
    (er-progn (maybe-reset-defaults-table1 (car keys)
        pre-defaults-tbl
        post-defaults-tbl
        state)
      (maybe-reset-defaults-table2 (cdr keys)
        pre-defaults-tbl
        post-defaults-tbl
        state))
    (value nil)))

(defun maybe-reset-defaults-table
  (pre-defaults-tbl post-defaults-tbl state)
  (maybe-reset-defaults-table2 (union-equal (strip-cars pre-defaults-tbl)
      (strip-cars post-defaults-tbl))
    pre-defaults-tbl
    post-defaults-tbl
    state))

(defun delete-something
  (lst)
  (cond ((null (cdr lst)) nil)
    ((null (car lst)) (cdr lst))
    (t (cons (car lst) (delete-something (cdr lst))))))

(defun store-in-kill-ring
  (x0 ring)
  (cond ((or (null x0) (null ring)) ring)
    (t (cons x0 (delete-something ring)))))

(defun rotate-kill-ring1
  (ring xn)
  (cond ((null ring) xn)
    ((car ring) (append ring xn))
    (t (rotate-kill-ring1 (cdr ring) (append xn (list nil))))))

(defun rotate-kill-ring
  (ring xn)
  (cond ((null (car ring)) (mv nil ring))
    (t (mv (car ring) (rotate-kill-ring1 (cdr ring) (list xn))))))

(defun ubt-ubu-fn1
  (kwd wrld pred-wrld state)
  (let ((pre-defaults-table (table-alist 'acl2-defaults-table wrld)))
    (er-let* ((redo-cmds (ubt-ubu-query kwd wrld pred-wrld nil nil wrld state nil)))
      (pprogn (f-put-global 'undone-worlds-kill-ring
          (store-in-kill-ring wrld
            (f-get-global 'undone-worlds-kill-ring state))
          state)
        (set-w 'retraction pred-wrld state)
        (let ((redo-cmds (if (eq (car redo-cmds) (default-defun-mode pred-wrld))
               (cdr redo-cmds)
               redo-cmds)))
          (er-progn (if redo-cmds
              (mv-let (col state)
                (fmt "Undoing complete.  Redoing started...~%"
                  nil
                  (standard-co state)
                  state
                  nil)
                (declare (ignore col))
                (value nil))
              (value nil))
            (if redo-cmds
              (ld redo-cmds
                :ld-redefinition-action '(:doit! . :overwrite)
                :ld-pre-eval-filter :all :ld-pre-eval-print t
                :ld-post-eval-print :command-conventions :ld-evisc-tuple (abbrev-evisc-tuple state)
                :ld-error-triples t
                :ld-error-action :return :ld-query-control-alist (cons '(:redef :y) (ld-query-control-alist state)))
              (value nil))
            (if redo-cmds
              (mv-let (col state)
                (fmt1 "Redoing complete.~%~%"
                  nil
                  0
                  (standard-co state)
                  state
                  nil)
                (declare (ignore col))
                (value nil))
              (value nil))
            (maybe-reset-defaults-table pre-defaults-table
              (table-alist 'acl2-defaults-table (w state))
              state)
            (pcs-fn :x :x nil state)
            (value :invisible)))))))

(defun ubt?-ubu?-fn
  (kwd cd state)
  (let* ((wrld (w state)) (info (global-val 'command-number-baseline-info wrld))
      (permanent-p (access command-number-baseline-info info :permanent-p))
      (current (access command-number-baseline-info info :current)))
    (er-let* ((cmd-wrld (er-decode-cd cd wrld kwd state)) (command-tuple-number (value (access-command-tuple-number (cddar cmd-wrld)))))
      (cond ((if (eq kwd :ubt)
           (<= command-tuple-number current)
           (< command-tuple-number current)) (cond ((let ((original (access command-number-baseline-info info :original)))
               (if (eq kwd :ubt)
                 (<= command-tuple-number original)
                 (< command-tuple-number original))) (er soft kwd "Can't undo into system initialization."))
            (t (er soft
                kwd
                "Can't undo into prehistory.  See :DOC ~
                      reset-prehistory."))))
        ((and (consp permanent-p)
           (if (eq kwd :ubt)
             (<= command-tuple-number (car permanent-p))
             (< command-tuple-number (car permanent-p)))) (er soft
            kwd
            "Can't undo a :disable-ubt event (at command ~x0).~@1  See ~
                  :DOC disable-ubt."
            (absolute-to-relative-command-number (car permanent-p) wrld)
            (if (cdr permanent-p)
              (msg "  ~@0" (cdr permanent-p))
              "")))
        ((and (eq kwd :ubu) (equal wrld cmd-wrld)) (er soft kwd "Can't undo back to where we already are!"))
        (t (let ((pred-wrld (if (eq kwd :ubt)
                 (scan-to-command (cdr cmd-wrld))
                 cmd-wrld)))
            (ubt-ubu-fn1 kwd wrld pred-wrld state)))))))

(defun ubt-ubu-fn
  (kwd cd state)
  (state-global-let* ((ld-query-control-alist (list* `(,KWD :n!)
         '(:ubt-defaults :n)
         (@ ld-query-control-alist))))
    (mv-let (erp val state)
      (ubt?-ubu?-fn kwd cd state)
      (declare (ignore erp val))
      (value :invisible))))

(defun ubt!-ubu!-fn
  (kwd cd state)
  (state-global-let* ((ld-query-control-alist (list* `(,KWD :n!)
         '(:ubt-defaults :n)
         (@ ld-query-control-alist))) (inhibit-output-lst (union-equal '(observation warning error)
          (@ inhibit-output-lst))))
    (mv-let (erp val state)
      (ubt?-ubu?-fn kwd cd state)
      (declare (ignore erp val))
      (value :invisible))))

(defun ubt-prehistory-fn
  (state)
  (let* ((ctx 'ubt-prehistory) (wrld (w state))
      (command-number-baseline-info (global-val 'command-number-baseline-info wrld))
      (command-number-baseline (access command-number-baseline-info
          command-number-baseline-info
          :current))
      (permanent-p (access command-number-baseline-info
          command-number-baseline-info
          :permanent-p)))
    (cond ((eql command-number-baseline
         (access command-number-baseline-info
           command-number-baseline-info
           :original)) (er soft ctx "There is no reset-prehistory event to undo."))
      ((eq permanent-p t) (er soft
          ctx
          "It is illegal to undo a (reset-prehistory t) event.  See :DOC ~
                reset-prehistory."))
      (permanent-p (er soft
          ctx
          "It is illegal to undo a reset-prehistory event with a non-nil ~
                pflg argument.  See :DOC reset-prehistory.~@0"
          (if (and (consp permanent-p) (cdr permanent-p))
            (msg "  ~@0" (cdr permanent-p))
            "")))
      (t (er-let* ((val (ubt-ubu-fn1 :ubt-prehistory wrld
               (scan-to-command (cdr (lookup-world-index 'command command-number-baseline wrld)))
               state)))
          (er-progn (reset-kill-ring t state) (value val)))))))

(defun oops-warning
  (state)
  (observation 'oops-warning
    "Installing the requested world."))

(defun oops-fn
  (state)
  (mv-let (new-wrld new-kill-ring)
    (rotate-kill-ring (f-get-global 'undone-worlds-kill-ring state)
      (w state))
    (cond ((null new-wrld) (cond ((null (f-get-global 'undone-worlds-kill-ring state)) (er soft
              :oops "Oops has been disabled in this ACL2 session.  ~
                             See :DOC reset-kill-ring"))
          (t (er soft
              :oops "ACL2 cannot execute :oops at this time, ~
                             presumably because you have never executed :ubt ~
                             or :u during this ACL2 session (at least not ~
                             since the last invocation of reset-kill-ring)."))))
      (t (er-progn (revert-world-on-error (pprogn (oops-warning state)
              (set-w! new-wrld state)
              (er-progn (pcs-fn :x :x nil state) (value nil))))
          (pprogn (f-put-global 'undone-worlds-kill-ring new-kill-ring state)
            (value :invisible)))))))

(defun rebuild-fn-read-filter
  (file state)
  (state-global-let* ((standard-oi *standard-oi*) (standard-co *standard-co*))
    (er-let* ((ans (acl2-query :rebuild '("How much of ~x0 do you want to process?" :t :all :all :all :query :query :until :until :? ("If you answer T or ALL, then the entire file will be ~
               loaded.  If you answer QUERY, then you will be asked ~
               about each command in the file.  If you answer UNTIL, ~
               then you should also type some name after the UNTIL ~
               and we will then proceed to process all of the events ~
               in file until that name has been introduced.  Rebuild ~
               automatically stops if any command causes an error.  ~
               When it stops, it leaves the logical world in the ~
               state it was in immediately before the erroneous ~
               command.  Thus, another way to use rebuild is to get ~
               into the habit of planting (i-am-here) -- or any other ~
               form that causes an error when executed -- and then ~
               using the filter T or ALL when you rebuild." :t :all :all :all :query :query :until :until))
           (list (cons #\0 file))
           state)))
      (cond ((eq ans :until) (read-object *standard-oi* state))
        (t (value ans))))))

(defun rebuild-fn
  (file filter filterp dir state)
  (er-let* ((filter (if filterp
         (value (if (eq filter t)
             :all filter))
         (rebuild-fn-read-filter file state))))
    (mv-let (erp val state)
      (ld file
        :dir dir
        :standard-co *standard-co*
        :proofs-co *standard-co*
        :ld-skip-proofsp t
        :ld-prompt nil
        :ld-missing-input-ok nil
        :ld-always-skip-top-level-locals nil
        :ld-pre-eval-filter filter
        :ld-pre-eval-print nil
        :ld-post-eval-print :command-conventions :ld-evisc-tuple (abbrev-evisc-tuple state)
        :ld-error-triples t
        :ld-error-action :return! :ld-query-control-alist '((:filter) . t)
        :ld-verbose t)
      (declare (ignore erp val))
      (value t))))

(defun sweep-symbol-binding-for-bad-symbol
  (sym obj deceased-packages state)
  (cond ((symbolp obj) (cond ((member-equal (symbol-package-name obj) deceased-packages) (er soft
            "undo consistency check"
            "~@0In particular, the value of the global ~
                     variable ~x1 contains the symbol ~x2 in package ~
                     ~x3, which we have been asked to remove.   ~
                     Please reset ~x1, as with (assign ~x1 nil)."
            *basic-sweep-error-str*
            sym
            obj
            (symbol-package-name obj)))
        (t (value nil))))
    ((atom obj) (value nil))
    ((equal obj (w state)) (value nil))
    (t (er-progn (sweep-symbol-binding-for-bad-symbol sym
          (car obj)
          deceased-packages
          state)
        (sweep-symbol-binding-for-bad-symbol sym
          (cdr obj)
          deceased-packages
          state)))))

(defun sweep-global-lst
  (l deceased-packages state)
  (cond ((null l) (value nil))
    (t (er-progn (sweep-symbol-binding-for-bad-symbol (car l)
          (get-global (car l) state)
          deceased-packages
          state)
        (sweep-global-lst (cdr l) deceased-packages state)))))

(defun sweep-stack-entry-for-bad-symbol
  (name i obj deceased-packages state)
  (cond ((symbolp obj) (cond ((member-equal (symbol-package-name obj) deceased-packages) (er soft
            "undo consistency check"
            "~@0In particular, the entry in the ~@1 at ~
                     location ~x2 contains the symbol ~x3 in package ~
                     ~x4, which we have been asked to undo.  Please ~
                     change the ~@1 entry at location ~x2 or ~
                     shrink the ~@1."
            *basic-sweep-error-str*
            name
            i
            obj
            (symbol-package-name obj)))
        (t (value nil))))
    ((atom obj) (value nil))
    ((equal obj (w state)) (value nil))
    (t (er-progn (sweep-stack-entry-for-bad-symbol name
          i
          (car obj)
          deceased-packages
          state)
        (sweep-stack-entry-for-bad-symbol name
          i
          (cdr obj)
          deceased-packages
          state)))))

(defun sweep-acl2-oracle
  (i deceased-packages state)
  (mv-let (nullp car-oracle state)
    (read-acl2-oracle state)
    (cond (nullp (value nil))
      (t (er-progn (sweep-stack-entry-for-bad-symbol "acl2-oracle"
            i
            car-oracle
            deceased-packages
            state)
          (sweep-acl2-oracle (+ 1 i) deceased-packages state))))))

(defun sweep-global-state-for-lisp-objects
  (deceased-packages state)
  (er-progn (sweep-global-lst (global-table-cars state)
      deceased-packages
      state)
    (sweep-acl2-oracle 0 deceased-packages state)))

(defun compile-function
  (ctx fn0 state)
  (declare (xargs :guard (and (or (symbolp fn0)
          (and (consp fn0)
            (member-eq (car fn0) '(:raw :exec))
            (consp (cdr fn0))
            (null (cddr fn0))))
        (state-p state))))
  (let ((wrld (w state)) (fn (if (consp fn0)
          (cadr fn0)
          fn0)))
    (cond ((not (eq (f-get-global 'compiler-enabled state) t)) (value (er hard
            ctx
            "Implementation error: Compile-function called when ~x0."
            '(not (eq (f-get-global 'compiler-enabled state) t)))))
      ((eq (getpropc fn 'formals t wrld) t) (er soft
          ctx
          "~x0 is not a defined function in the current ACL2 world."
          fn))
      (t (state-global-let* ((trace-specs (f-get-global 'trace-specs state)) (retrace-p t))
          (prog2$ nil (value fn)))))))

(defun keep-tmp-files
  (state)
  (f-get-global 'keep-tmp-files state))

(defun comp-fn
  (fns gcl-flg tmp-suffix state)
  (declare (xargs :guard (and (state-p state)
        (or (and (true-listp fns) fns) (symbolp fns))
        (stringp tmp-suffix)
        (not (equal tmp-suffix ""))))
    (ignore tmp-suffix))
  (cond ((eql 0 (f-get-global 'ld-level state)) (pprogn (warning$ 'comp
          "Comp"
          "Comp is ignored outside the ACL2 loop.")
        (value nil)))
    (gcl-flg (er soft
        'comp
        "Comp-gcl may only be used in GCL implementations."))
    ((not (eq (f-get-global 'compiler-enabled state) t)) (value nil))
    (t (let ((fns (cond ((or (and (symbolp fns)
                  (not (eq fns t))
                  (not (eq fns :raw))
                  (not (eq fns :exec))
                  (not (eq fns nil)))
                (and (consp fns)
                  (member-eq (car fns) '(:raw :exec))
                  (consp (cdr fns))
                  (null (cddr fns)))) (list fns))
             (t fns))))
        (cond ((and (consp fns) (null (cdr fns)) (not gcl-flg)) (compile-function 'comp (car fns) state))
          ((null fns) (er soft
              'comp
              "We do not allow the notion of compiling the empty list of ~
             functions.  Perhaps you meant to do something else."))
          (t (value t)))))))

(defun scan-past-deeper-event-landmarks
  (depth wrld)
  (cond ((or (null wrld)
       (and (eq (car (car wrld)) 'command-landmark)
         (eq (cadr (car wrld)) 'global-value))) wrld)
    ((and (eq (car (car wrld)) 'event-landmark)
       (eq (cadr (car wrld)) 'global-value)) (cond ((> (access-event-tuple-depth (cddr (car wrld))) depth) (scan-past-deeper-event-landmarks depth (cdr wrld)))
        (t wrld)))
    (t (scan-past-deeper-event-landmarks depth (cdr wrld)))))

(defun puffable-encapsulate-p
  (cddr-car-wrld installed-wrld ntep)
  (and (eq (access-event-tuple-type cddr-car-wrld) 'encapsulate)
    (let* ((encap (access-event-tuple-form cddr-car-wrld)) (signatures (cadr encap))
        (fns (signature-fns signatures)))
      (not (and (consp fns)
          (or (not ntep)
            (mv-let (name x origins)
              (constraint-info (car fns) installed-wrld)
              (declare (ignore name origins))
              (unknown-constraints-p x))))))))

(defun puffable-command-blockp
  (wrld cmd-form ntep installed-wrld)
  (cond ((or (null wrld)
       (and (eq (car (car wrld)) 'command-landmark)
         (eq (cadr (car wrld)) 'global-value))) nil)
    ((and (eq (car (car wrld)) 'event-landmark)
       (eq (cadr (car wrld)) 'global-value)) (cond ((atom cmd-form) nil)
        ((eq (car cmd-form) 'certify-book) 'certify-book)
        ((eq (car cmd-form) 'include-book) (assert$ (eq (car (access-event-tuple-form (cddr (car wrld))))
              'include-book)
            'include-book))
        ((eq (car cmd-form) 'encapsulate) (and (puffable-encapsulate-p (cddr (car wrld))
              installed-wrld
              ntep)
            'encapsulate))
        (t (not (equal cmd-form (access-event-tuple-form (cddr (car wrld))))))))
    (t (puffable-command-blockp (cdr wrld)
        cmd-form
        ntep
        installed-wrld))))

(defun puffable-command-numberp
  (i state)
  (mv-let (flg n)
    (normalize-absolute-command-number (relative-to-absolute-command-number i (w state))
      (w state))
    (and (null flg)
      (let ((wrld (lookup-world-index 'command n (w state))))
        (puffable-command-blockp (cdr wrld)
          (access-command-tuple-form (cddr (car wrld)))
          nil
          (w state))))))

(defun puff-include-book
  (wrld include-book-alist-entry final-cmds ctx state)
  (let* ((full-book-string (access-event-tuple-namex (cddr (car wrld)))) (installed-wrld (w state))
      (full-book-name (filename-to-book-name full-book-string installed-wrld)))
    (cond ((assoc-equal full-book-name
         (table-alist 'puff-included-books installed-wrld)) (value final-cmds))
      (t (er-progn (chk-input-object-file full-book-string ctx state)
          (er-let* ((ev-lst (read-object-file full-book-string ctx state)) (cert-obj (chk-certificate-file full-book-string
                  nil
                  nil
                  'puff
                  ctx
                  state
                  '((:uncertified-okp . t) (:defaxioms-okp t)
                    (:skip-proofs-okp t))
                  nil)))
            (let* ((old-book-hash (cddddr (assoc-equal full-book-name
                     (global-val 'include-book-alist (w state))))) (expansion-alist (and old-book-hash
                    cert-obj
                    (access cert-obj cert-obj :expansion-alist)))
                (cert-data (and old-book-hash
                    cert-obj
                    (access cert-obj cert-obj :cert-data)))
                (cmds (and cert-obj (access cert-obj cert-obj :cmds))))
              (er-let* ((ev-lst-book-hash (if old-book-hash
                     (book-hash old-book-hash
                       full-book-string
                       cmds
                       expansion-alist
                       cert-data
                       ev-lst
                       state)
                     (value nil))))
                (cond ((and old-book-hash
                     (not (equal ev-lst-book-hash old-book-hash))) (er soft
                      ctx
                      "When the certified book ~x0 was included, its book-hash ~
                    was ~x1.  The book-hash for ~x0 is now ~x2.  The book has ~
                    thus presumably been modified since it was last included ~
                    and we cannot now recover the events that created the ~
                    current logical world."
                      full-book-string
                      old-book-hash
                      ev-lst-book-hash))
                  (t (let ((fixed-cmds (append cmds
                           (cons (assert$ (and (consp (car ev-lst)) (eq (caar ev-lst) 'in-package))
                               (car ev-lst))
                             (subst-by-position expansion-alist (cdr ev-lst) 1)))))
                      (value `((ld '((set-cbd ,(DIRECTORY-OF-ABSOLUTE-PATHNAME FULL-BOOK-STRING)) ,@FIXED-CMDS
                             ,@(AND INCLUDE-BOOK-ALIST-ENTRY
       `((TABLE PUFF-INCLUDED-BOOKS ',FULL-BOOK-NAME
                ',INCLUDE-BOOK-ALIST-ENTRY))))
                           :ld-error-action :error) (maybe-install-acl2-defaults-table ',(TABLE-ALIST 'ACL2-DEFAULTS-TABLE WRLD)
                            state)
                          ,@FINAL-CMDS)))))))))))))

(defun puff-command-block1
  (wrld immediate ans ctx state)
  (cond ((or (null wrld)
       (and (eq (car (car wrld)) 'command-landmark)
         (eq (cadr (car wrld)) 'global-value))) (value ans))
    ((and (eq (car (car wrld)) 'event-landmark)
       (eq (cadr (car wrld)) 'global-value)) (let* ((event-tuple (cddr (car wrld))) (event-type (access-event-tuple-type event-tuple))
          (include-book-alist-entry (car (global-val 'include-book-alist wrld))))
        (cond ((and (eq immediate 'certify-book)
             (eq event-type 'include-book)
             (equal (car include-book-alist-entry)
               (filename-to-book-name (access-event-tuple-namex event-tuple)
                 (w state)))) (puff-include-book wrld
              include-book-alist-entry
              ans
              ctx
              state))
          ((eq immediate 'encapsulate) (assert$ (eq event-type 'encapsulate)
              (value (append (cddr (access-event-tuple-form (cddr (car wrld))))
                  (cons `(maybe-install-acl2-defaults-table ',(TABLE-ALIST 'ACL2-DEFAULTS-TABLE WRLD)
                      state)
                    ans)))))
          (t (puff-command-block1 (cond ((member-eq event-type '(encapsulate include-book)) (scan-past-deeper-event-landmarks (access-event-tuple-depth event-tuple)
                    (cdr wrld)))
                (t (cdr wrld)))
              nil
              (cons (access-event-tuple-form event-tuple) ans)
              ctx
              state)))))
    (t (puff-command-block1 (cdr wrld) immediate ans ctx state))))

(defun puff-command-block
  (cmd-type wrld final-cmds ctx state)
  (case cmd-type
    (encapsulate (puff-command-block1 wrld 'encapsulate final-cmds ctx state))
    (include-book (puff-include-book wrld
        (car (global-val 'include-book-alist wrld))
        final-cmds
        ctx
        state))
    (certify-book (puff-command-block1 wrld
        'certify-book
        final-cmds
        ctx
        state))
    (otherwise (puff-command-block1 wrld nil final-cmds ctx state))))

(defun commands-back-to-1
  (wrld1 wrld2 cbd cbd0 ans)
  (cond ((equal wrld1 wrld2) (assert$ (and (eq (car (car wrld1)) 'command-landmark)
          (eq (cadr (car wrld1)) 'global-value))
        (if (equal cbd cbd0)
          ans
          (cons `(set-cbd ,CBD) ans))))
    ((and (eq (car (car wrld1)) 'command-landmark)
       (eq (cadr (car wrld1)) 'global-value)) (let* ((next-cbd (access-command-tuple-cbd (cddr (car wrld1)))) (ans (if (equal cbd next-cbd)
              ans
              (cons `(set-cbd ,CBD) ans))))
        (commands-back-to-1 (cdr wrld1)
          wrld2
          next-cbd
          cbd0
          (cons (access-command-tuple-form (cddr (car wrld1))) ans))))
    (t (commands-back-to-1 (cdr wrld1) wrld2 cbd cbd0 ans))))

(defun commands-back-to
  (wrld1 wrld2 state)
  (let ((cbd (f-get-global 'connected-book-directory state)))
    (commands-back-to-1 wrld1
      wrld2
      cbd
      cbd
      (cond ((equal cbd (access-command-tuple-cbd (cddr (car wrld1)))) nil)
        (t (list `(set-cbd ,CBD)))))))

(defun puffed-command-sequence
  (cd ctx wrld state)
  (er-let* ((cmd-wrld (er-decode-cd cd wrld ctx state)))
    (let ((cmd-type (puffable-command-blockp (cdr cmd-wrld)
           (access-command-tuple-form (cddr (car cmd-wrld)))
           (eq ctx :puff)
           (w state))) (final-cmds (commands-back-to wrld cmd-wrld state)))
      (cond (cmd-type (puff-command-block cmd-type
            (scan-to-event (cdr cmd-wrld))
            final-cmds
            ctx
            state))
        (t (er soft
            ctx
            "The command at ~x0, namely ~X12, cannot be puffed.  See :DOC ~
               puff."
            cd
            (access-command-tuple-form (cddr (car cmd-wrld)))
            '(nil 2 3 nil)))))))

(defun ld-read-eval-print-simple
  (state)
  (mv-let (eofp erp keyp form state)
    (ld-read-command state)
    (declare (ignore keyp))
    (cond (eofp (mv :return :eof state))
      (erp (ld-return-error state))
      (t (pprogn (f-put-global 'last-make-event-expansion nil state)
          (let* ((old-wrld (w state)) (old-default-defun-mode (default-defun-mode old-wrld)))
            (mv-let (error-flg trans-ans state)
              (mv-let (error-flg trans-ans state)
                (if (raw-mode-p state)
                  (acl2-raw-eval form state)
                  (trans-eval-default-warning form 'top-level state t))
                (cond (error-flg (mv t nil state))
                  ((and (ld-error-triples state)
                     (or (equal (car trans-ans) *error-triple-sig*)
                       (equal (car trans-ans) *error-triple-df-sig*))
                     (car (cdr trans-ans))) (mv t nil state))
                  (t (er-progn (maybe-add-command-landmark old-wrld
                        old-default-defun-mode
                        form
                        trans-ans
                        state)
                      (mv nil trans-ans state)))))
              (cond (error-flg (ld-return-error state))
                ((and (equal (car trans-ans) *error-triple-sig*)
                   (eq (cadr (cdr trans-ans)) :q)) (mv :return :exit state))
                ((and (ld-error-triples state)
                   (equal (car trans-ans) *error-triple-sig*)
                   (let ((val (cadr (cdr trans-ans))))
                     (and (consp val) (eq (car val) :stop-ld)))) (mv :return (list* :stop-ld (f-get-global 'ld-level state)
                      (cdr (cadr (cdr trans-ans))))
                    state))
                (t (mv :continue nil state))))))))))

(defun ld-loop-simple
  (state)
  (mv-let (signal val state)
    (ld-read-eval-print-simple state)
    (cond ((eq signal :continue) (ld-loop-simple state))
      ((eq signal :return) (value val))
      (t (mv t nil state)))))

(defun ld-simple
  (forms state)
  (state-global-let* ((standard-oi forms) (ld-skip-proofsp 'include-book-with-locals)
      (ld-verbose nil)
      (ld-prompt nil)
      (ld-missing-input-ok nil)
      (ld-always-skip-top-level-locals nil)
      (ld-pre-eval-filter :all)
      (ld-pre-eval-print :never)
      (ld-post-eval-print nil)
      (ld-error-triples t)
      (ld-error-action :error)
      (ld-query-control-alist (cons '(:redef :y) (ld-query-control-alist state))))
    (ld-loop-simple state)))

(defun puff-fn1
  (cd ctx state)
  (revert-world-on-error (state-global-let* ((current-package (current-package state)) (modifying-include-book-dir-alist t))
      (let* ((wrld (w state)) (info (global-val 'command-number-baseline-info wrld))
          (permanent-p (access command-number-baseline-info info :permanent-p))
          (current (access command-number-baseline-info info :current))
          (barrier (if (consp permanent-p)
              (max (car permanent-p) current)
              current)))
        (er-let* ((cmd-wrld (er-decode-cd cd wrld ctx state)) (command-tuple-number (value (access-command-tuple-number (cddar cmd-wrld)))))
          (cond ((<= command-tuple-number barrier) (cond ((<= command-tuple-number
                   (access command-number-baseline-info info :original)) (er soft
                    ctx
                    "Can't puff a command within the system initialization."))
                ((<= command-tuple-number current) (er soft
                    ctx
                    "Can't puff a command within prehistory.  See :DOC ~
                      reset-prehistory."))
                (t (er soft
                    ctx
                    "Can't puff a command executed at or before the ~
                      reset-prehistory event (at command ~x0) that disabled ~
                      undoing.~@1  See :DOC disable-ubt."
                    (absolute-to-relative-command-number (car permanent-p) wrld)
                    (if (cdr permanent-p)
                      (msg "  ~@0" (cdr permanent-p))
                      "")))))
            (t (er-let* ((cmds (puffed-command-sequence cd ctx wrld state)))
                (let* ((pred-wrld (scan-to-command (cdr cmd-wrld))) (i (absolute-to-relative-command-number (max-absolute-command-number cmd-wrld)
                        (w state)))
                    (k (- (absolute-to-relative-command-number (max-absolute-command-number (w state))
                          (w state))
                        i)))
                  (pprogn (set-w 'retraction pred-wrld state)
                    (er-progn (state-global-let* ((guard-checking-on t))
                        (ld-simple cmds state))
                      (value (cons i
                          (- (absolute-to-relative-command-number (max-absolute-command-number (w state))
                              (w state))
                            k))))))))))))))

(defun puff-report
  (caller new-cd1 new-cd2 cd state)
  (cond ((eql new-cd1 (1+ new-cd2)) (pprogn (io? history
          nil
          state
          (caller cd)
          (fms "Note: ~x0 is complete, but no events were ~
                            executed under the given command descriptor, ~
                            ~x1.~|"
            (list (cons #\0 caller) (cons #\1 cd))
            (standard-co state)
            state
            nil))
        (value :invisible)))
    (t (pcs-fn new-cd1 new-cd2 t state))))

(defun puff-fn
  (cd state)
  (er-let* ((pair (puff-fn1 cd :puff state)))
    (puff-report :puff (car pair) (cdr pair) cd state)))

(defun puff*-fn11
  (ptr k i j state)
  (cond ((> i j) (value (cons ptr j)))
    ((puffable-command-numberp i state) (mv-let (erp val state)
        (puff-fn1 i :puff* state)
        (declare (ignore val))
        (cond (erp (mv erp (cons i (cons ptr j)) state))
          (t (puff*-fn11 ptr
              k
              ptr
              (- (absolute-to-relative-command-number (max-absolute-command-number (w state))
                  (w state))
                k)
              state)))))
    (t (puff*-fn11 ptr k (1+ i) j state))))

(defun puff*-fn1
  (ptr k state)
  (puff*-fn11 ptr
    k
    ptr
    (- (absolute-to-relative-command-number (max-absolute-command-number (w state))
        (w state))
      k)
    state))

(defun puff*-fn
  (cd state)
  (let* ((wrld (w state)) (info (global-val 'command-number-baseline-info wrld))
      (permanent-p (access command-number-baseline-info info :permanent-p))
      (current (access command-number-baseline-info info :current))
      (barrier (if (consp permanent-p)
          (max (car permanent-p) current)
          current)))
    (er-let* ((cmd-wrld (er-decode-cd cd wrld :puff* state)) (command-tuple-number (value (access-command-tuple-number (cddar cmd-wrld)))))
      (cond ((<= command-tuple-number barrier) (cond ((<= command-tuple-number
               (access command-number-baseline-info info :original)) (er soft
                :puff* "Can't puff* a command within the system initialization."))
            ((<= command-tuple-number current) (er soft
                :puff* "Can't puff* a command within prehistory.  See :DOC ~
                    reset-prehistory."))
            (t (er soft
                :puff* "Can't puff* a command executed at or before :disable-ubt ~
                    (at command ~x0).~@1  See :DOC disable-ubt."
                (absolute-to-relative-command-number (car permanent-p) wrld)
                (if (cdr permanent-p)
                  (msg "  ~@0" (cdr permanent-p))
                  "")))))
        (t (let* ((mx (absolute-to-relative-command-number (max-absolute-command-number wrld)
                 wrld)) (ptr (absolute-to-relative-command-number (max-absolute-command-number cmd-wrld)
                  wrld))
              (k (- mx ptr)))
            (er-let* ((pair (puff*-fn1 ptr k state)))
              (puff-report :puff* (car pair) (cdr pair) cd state))))))))

(defun dmr-stop-fn
  (state)
  (declare (xargs :guard (state-p state)))
  (let ((dmrp (f-get-global 'dmrp state)))
    (cond (dmrp (pprogn (f-put-global 'dmrp nil state)
          (if (consp dmrp)
            (set-debugger-enable-fn (car dmrp) state)
            state)))
      (t (observation 'dmr-stop
          "Skipping dmr-stop (dmr is already stopped).")))))

(defun dmr-start-fn
  (state)
  (declare (xargs :guard (state-p state)))
  (cond ((f-get-global 'dmrp state) (observation 'dmr-start
        "Skipping dmr-start (dmr is already started)."))
    (t (let* ((old-debugger-enable (f-get-global 'debugger-enable state)) (new-debugger-enable (case old-debugger-enable ((nil) t) (:bt :break-bt))))
        (pprogn (if new-debugger-enable
            (set-debugger-enable-fn new-debugger-enable state)
            state)
          (f-put-global 'dmrp
            (if new-debugger-enable
              (list old-debugger-enable)
              t)
            state))))))

(defun congruence-rule-listp
  (x wrld)
  (if (atom x)
    (null x)
    (and (let ((rule (car x)))
        (case-match rule
          ((nume equiv . rune) (and (equivalence-relationp equiv wrld)
              (or (runep rune wrld)
                (equal rune *fake-rune-for-anonymous-enabled-rule*))
              (eql (fnume rune wrld) nume)))))
      (congruence-rule-listp (cdr x) wrld))))

(defun term-alistp-failure-msg
  (alist wrld)
  (cond ((atom alist) (and alist (msg "a non-nil final cdr")))
    ((atom (car alist)) (msg "a non-consp element, ~x0" (car alist)))
    ((not (and (termp (caar alist) wrld) (variablep (caar alist)))) (msg "an element, ~p0, whose car is not a variable"
        (caar alist)))
    ((not (termp (cdar alist) wrld)) (msg "an element, ~p0, whose cdr is not a term"
        (cdar alist)))
    (t (term-alistp-failure-msg (cdr alist) wrld))))

(defun find-runed-linear-lemma
  (rune lst)
  (cond ((null lst) nil)
    ((equal rune (access linear-lemma (car lst) :rune)) (car lst))
    (t (find-runed-linear-lemma rune (cdr lst)))))

(defun mfc-force-flg
  (forcep mfc)
  (cond ((eq forcep :same) (ok-to-force (access metafunction-context mfc :rcnst)))
    (t forcep)))

(defun update-rncst-for-forcep
  (forcep rcnst)
  (cond ((or (eq forcep :same) (iff forcep (ok-to-force rcnst))) rcnst)
    (t (change rewrite-constant
        rcnst
        :force-info (if forcep
          t
          'weak)))))

(defun print-saved-output-lst
  (io-record-lst io-markers stop-markers ctx state)
  (cond ((endp io-record-lst) (value :invisible))
    (t (let ((io-marker (access io-record (car io-record-lst) :io-marker)))
        (cond ((member-equal io-marker stop-markers) (value :invisible))
          ((or (eq io-markers :all)
             (member-equal io-marker io-markers)) (er-progn (trans-eval (access io-record (car io-record-lst) :form)
                ctx
                state
                t)
              (print-saved-output-lst (cdr io-record-lst)
                (if stop-markers
                  :all io-markers)
                stop-markers
                ctx
                state)))
          (t (print-saved-output-lst (cdr io-record-lst)
              io-markers
              stop-markers
              ctx
              state)))))))

(defun print-saved-output
  (inhibit-output-lst gag-mode io-markers stop-markers state)
  (let ((saved-output (reverse (f-get-global 'saved-output-reversed state))) (channel (standard-co state))
      (ctx 'print-saved-output))
    (cond ((or (null saved-output)
         (and (null (cdr saved-output))
           (eq (access io-record (car saved-output) :io-marker) :ctx))) (er-progn (if saved-output
            (trans-eval (access io-record (car saved-output) :form)
              ctx
              state
              t)
            (value nil))
          (pprogn (let ((inh (member-eq 'prove (f-get-global 'inhibit-output-lst state))))
              (fms "There is no saved output to print.  See :DOC ~
                                pso.~#0~[~/  Note that PROVE output is ~
                                inhibited, and output is not saved when that ~
                                is the case; see :DOC set-inhibit-output-lst ~
                                for how to turn on PROVE output.~]~|"
                (list (cons #\0
                    (if inh
                      1
                      0)))
                channel
                state
                nil))
            (value :invisible))))
      (t (state-global-let* ((saved-output-reversed nil) (inhibit-output-lst inhibit-output-lst)
            (gag-mode gag-mode)
            (gag-state-saved (f-get-global 'gag-state-saved state)))
          (pprogn (initialize-summary-accumulators state)
            (save-event-state-globals (revert-world (state-global-let* ((saved-output-p nil) (acl2-world-alist (f-get-global 'acl2-world-alist state)))
                  (pprogn (pop-current-acl2-world 'saved-output-reversed state)
                    (print-saved-output-lst saved-output
                      io-markers
                      stop-markers
                      ctx
                      state)))))))))))

(defun convert-io-markers-lst
  (io-markers acc)
  (cond ((endp io-markers) acc)
    (t (convert-io-markers-lst (cdr io-markers)
        (cons (if (stringp (car io-markers))
            (parse-clause-id (car io-markers))
            (car io-markers))
          acc)))))

(defun convert-io-markers
  (io-markers)
  (cond ((member-eq io-markers '(nil :all)) io-markers)
    ((and io-markers (atom io-markers)) (convert-io-markers-lst (list io-markers) nil))
    (t (convert-io-markers-lst io-markers nil))))

(defun set-raw-proof-format-fn
  (val state)
  (declare (xargs :guard (member-eq val '(t nil :clause))))
  (f-put-global 'raw-proof-format val state))

(defun set-ld-evisc-tuple
  (val state)
  (set-evisc-tuple val :sites :ld :iprint :same))

(defun set-abbrev-evisc-tuple
  (val state)
  (set-evisc-tuple val :sites :abbrev :iprint :same))

(defun set-gag-mode-evisc-tuple
  (val state)
  (set-evisc-tuple val :sites :gag-mode :iprint :same))

(defun set-term-evisc-tuple
  (val state)
  (set-evisc-tuple val :sites :term :iprint :same))

(defun set-brr-evisc-tuple
  (val state)
  (set-evisc-tuple val :sites :brr :iprint :same))

(defun without-evisc-fn
  (form state)
  (state-global-let* ((abbrev-evisc-tuple nil set-abbrev-evisc-tuple-state) (gag-mode-evisc-tuple nil set-gag-mode-evisc-tuple-state)
      (term-evisc-tuple nil set-term-evisc-tuple-state))
    (er-progn (ld (list form)
        :ld-verbose nil
        :ld-prompt nil
        :ld-evisc-tuple nil
        :ld-user-stobjs-modified-warning nil
        :ld-error-action :error)
      (value :invisible))))

(defun keyword-value-string-listp
  (l)
  (declare (xargs :guard t))
  (cond ((atom l) (null l))
    (t (and (keywordp (car l))
        (consp (cdr l))
        (stringp (cadr l))
        (keyword-value-string-listp (cddr l))))))

(defun project-dir-string-p
  (s pos bound)
  (declare (type (unsigned-byte 60) bound)
    (xargs :measure (nfix (- bound pos))
      :guard (and (stringp s)
        (natp pos)
        (natp bound)
        (<= pos bound)
        (<= bound (length s)))))
  (let ((pos (scan-past-whitespace s pos bound)))
    (cond ((mbe :logic (or (not (natp pos)) (>= pos bound))
         :exec (= pos bound)) t)
      ((eql (char s pos) #\;) (let ((p0 (search *newline-string* s :start2 (1+ pos) :end2 bound)))
          (or (null p0) (project-dir-string-p s p0 bound))))
      (t (let* ((p0 (search *newline-string* s :start2 pos :end2 bound)) (p (or p0 bound))
            (k (search ":" s :start2 pos :end2 p))
            (q (search """ s :start2 pos :end2 p))
            (q2 (and q (search """ s :start2 (1+ q) :end2 p))))
          (and k
            q2
            (< k q)
            (= p (scan-past-whitespace s (1+ q2) p))
            (not (search ":" s :start2 (1+ q2) :end2 p))
            (not (search """ s :start2 (1+ q2) :end2 p))
            (project-dir-string-p s p bound)))))))

(defun project-dir-file-p
  (filename state)
  (declare (xargs :stobjs state :guard (stringp filename)))
  (let* ((s (read-file-into-string filename)) (len (length s)))
    (and (stringp s)
      (unsigned-byte-p *fixnat-bits* len)
      (project-dir-string-p s 0 len))))

(defun merge-length>=-cdr
  (l1 l2)
  (declare (xargs :guard (and (alistp l1) (alistp l2))
      :measure (+ (length l1) (length l2))))
  (cond ((endp l1) l2)
    ((endp l2) l1)
    ((>= (length (cdar l1)) (length (cdar l2))) (cons (car l1) (merge-length>=-cdr (cdr l1) l2)))
    (t (cons (car l2) (merge-length>=-cdr l1 (cdr l2))))))

(defun merge-sort-length>=-cdr
  (l)
  (declare (xargs :guard (alistp l)
      :measure (length l)
      :verify-guards nil))
  (cond ((endp (cdr l)) l)
    (t (merge-length>=-cdr (merge-sort-length>=-cdr (evens l))
        (merge-sort-length>=-cdr (odds l))))))

(defun conflicting-symbol-alists
  (a1 a2)
  (declare (xargs :guard (and (symbol-alistp a1) (symbol-alistp a2))))
  (cond ((endp a1) nil)
    (t (let ((pair (assoc-eq (caar a1) a2)))
        (cond ((and pair (not (equal (cdr pair) (cdar a1)))) (list* (car pair) (cdar a1) (cdr pair)))
          (t (conflicting-symbol-alists (cdr a1) a2)))))))