basis-a

(defun equal-x-constant
  (x const)
  (declare (xargs :guard (and (consp const)
        (eq (car const) 'quote)
        (consp (cdr const)))))
  (let ((guts (cadr const)))
    (cond ((symbolp guts) (list 'eq x const))
      ((or (acl2-numberp guts) (characterp guts)) (list 'eql x guts))
      ((stringp guts) (list 'equal x guts))
      (t (list 'equal x const)))))

(defun match-tests-and-bindings
  (x pat tests bindings dups)
  (declare (xargs :guard (and (symbol-doublet-listp bindings) (true-listp dups))))
  (cond ((symbolp pat) (cond ((or (eq pat t) (eq pat nil) (keywordp pat)) (mv (cons (list 'eq x pat) tests) bindings dups))
        ((let ((len (length (symbol-name pat))))
           (and (> len 0)
             (eql #\* (char (symbol-name pat) 0))
             (eql #\* (char (symbol-name pat) (1- len))))) (mv (cons (list 'equal x pat) tests) bindings dups))
        ((and (> (length (symbol-name pat)) 0)
           (eql #\! (char (symbol-name pat) 0))) (mv (cons (list 'equal
                x
                (intern-in-package-of-symbol (subseq (symbol-name pat) 1 (length (symbol-name pat)))
                  pat))
              tests)
            bindings
            dups))
        ((eq pat '&) (mv tests bindings dups))
        (t (let ((binding (assoc-eq pat bindings)))
            (cond ((null binding) (mv tests (cons (list pat x) bindings) dups))
              (t (mv (cons (list 'equal x (cadr binding)) tests)
                  bindings
                  (add-to-set-eq pat dups))))))))
    ((atom pat) (mv (cons (equal-x-constant x (list 'quote pat)) tests)
        bindings
        dups))
    ((and (eq (car pat) 'quote)
       (consp (cdr pat))
       (null (cddr pat))) (mv (cons (equal-x-constant x pat) tests) bindings dups))
    ((and (eq (car pat) 'quote~)
       (consp (cdr pat))
       (symbolp (cadr pat))
       (null (cddr pat))) (mv (cons (list 'symbol-name-equal x (symbol-name (cadr pat)))
          tests)
        bindings
        dups))
    (t (mv-let (tests1 bindings1 dups1)
        (match-tests-and-bindings (list 'car x)
          (car pat)
          (cons (list 'consp x) tests)
          bindings
          dups)
        (match-tests-and-bindings (list 'cdr x)
          (cdr pat)
          tests1
          bindings1
          dups1)))))

(defun match-clause
  (x pat forms)
  (declare (xargs :guard t))
  (mv-let (tests bindings dups)
    (match-tests-and-bindings x pat nil nil nil)
    (list (if (null tests)
        t
        (cons 'and (reverse tests)))
      `(let ,(REVERSE BINDINGS)
        ,@(AND DUPS `((DECLARE (IGNORABLE ,@DUPS))))
        ,@FORMS))))

(defun match-clause-list
  (x clauses)
  (declare (xargs :guard (alistp clauses)))
  (cond ((consp clauses) (if (eq (caar clauses) '&)
        (list (match-clause x (caar clauses) (cdar clauses)))
        (cons (match-clause x (caar clauses) (cdar clauses))
          (match-clause-list x (cdr clauses)))))
    (t '((t nil)))))

(defun wormhole-statusp
  (whs)
  (declare (xargs :mode :logic :guard t))
  (or (equal whs nil)
    (and (consp whs)
      (or (eq (car whs) :enter) (eq (car whs) :skip)))))

(defun wormhole-entry-code
  (whs)
  (declare (xargs :mode :logic :guard t))
  (if (and (consp whs) (eq (car whs) :skip))
    :skip :enter))

(defun wormhole-data
  (whs)
  (declare (xargs :mode :logic :guard t))
  (if (consp whs)
    (cdr whs)
    nil))

(defun set-wormhole-entry-code
  (whs code)
  (declare (xargs :mode :logic :guard (or (eq code :enter) (eq code :skip))))
  (if (consp whs)
    (if (eq (car whs) code)
      whs
      (cons code (cdr whs)))
    (if (eq code :enter)
      whs
      (cons :skip whs))))

(defun set-wormhole-data
  (whs data)
  (declare (xargs :mode :logic :guard t))
  (if (consp whs)
    (if (equal (cdr whs) data)
      whs
      (cons (car whs) data))
    (cons :enter data)))

(defun make-wormhole-status
  (old-status new-code new-data)
  (declare (xargs :mode :logic :guard (or (eq new-code :enter) (eq new-code :skip))))
  (if (consp old-status)
    (if (and (eq new-code (car old-status))
        (equal new-data (cdr old-status)))
      old-status
      (cons new-code new-data))
    (cons new-code new-data)))

(defun tree-occur-eq
  (x y)
  (declare (xargs :guard (symbolp x)))
  (cond ((consp y) (or (tree-occur-eq x (car y)) (tree-occur-eq x (cdr y))))
    (t (eq x y))))

(defun wormhole-eval
  (qname qlambda free-vars)
  (declare (xargs :mode :logic :guard t)
    (ignore qname qlambda free-vars))
  nil)

(defun wormhole-eval-early-null-exit-p
  (qlambda)
  (case-match qlambda
    (('quote ('lambda (whs)
         ('let ((info ('wormhole-data whs)))
           ('cond (('null info) whs) . &)))) (declare (ignore info whs))
      t)
    (& nil)))

(defun sync-ephemeral-whs-with-persistent-whs
  (name state)
  (declare (xargs :stobjs state))
  (if (and name (equal (f-get-global 'wormhole-name state) name))
    (mv-let (erp val state)
      (read-acl2-oracle state)
      (declare (ignore erp))
      (f-put-global 'wormhole-status val state))
    state))

(defun set-persistent-whs-and-ephemeral-whs
  (name new-status state)
  (declare (xargs :stobjs state))
  (prog2$ (wormhole-eval name '(lambda nil new-status) new-status)
    (sync-ephemeral-whs-with-persistent-whs name state)))

(defun lambda-keywordp
  (x)
  (and (symbolp x) (eql 1 (string<= "&" (symbol-name x)))))

(defun legal-variable-or-constant-namep
  (name)
  (and (symbolp name)
    (cond ((or (eq name t) (eq name nil)) 'constant)
      (t (let ((p (symbol-package-name name)))
          (and (not (equal p "KEYWORD"))
            (let ((s (symbol-name name)))
              (cond ((and (not (= (length s) 0))
                   (eql (char s 0) #\*)
                   (eql (char s (1- (length s))) #\*)) (if (equal p *main-lisp-package-name*)
                    nil
                    'constant))
                ((and (not (= (length s) 0)) (eql (char s 0) #\&)) nil)
                ((equal p *main-lisp-package-name*) (and (not (member-eq name *common-lisp-specials-and-constants*))
                    (member-eq name
                      *common-lisp-symbols-from-main-lisp-package*)
                    'variable))
                (t 'variable)))))))))

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

(defun arglistp1
  (lst)
  (cond ((atom lst) (null lst))
    (t (and (legal-variablep (car lst)) (arglistp1 (cdr lst))))))

(defun arglistp
  (lst)
  (and (arglistp1 lst) (no-duplicatesp-eq lst)))

(defun find-first-bad-arg
  (args)
  (declare (xargs :guard (and (true-listp args) (not (arglistp args)))))
  (cond ((not (symbolp (car args))) (mv (car args) "is not a symbol"))
    ((legal-constantp1 (car args)) (mv (car args) "has the syntax of a constant"))
    ((lambda-keywordp (car args)) (mv (car args) "is a lambda keyword"))
    ((keywordp (car args)) (mv (car args) "is in the KEYWORD package"))
    ((member-eq (car args) *common-lisp-specials-and-constants*) (mv (car args)
        "belongs to the list *common-lisp-specials-and-constants* ~
                    of symbols from the main Lisp package"))
    ((member-eq (car args) (cdr args)) (mv (car args) "occurs more than once in the list"))
    ((and (equal (symbol-package-name (car args))
         *main-lisp-package-name*)
       (not (member-eq (car args)
           *common-lisp-symbols-from-main-lisp-package*))) (mv (car args)
        "belongs to the main Lisp package but not to the list ~
                    *common-lisp-symbols-from-main-lisp-package*"))
    (t (find-first-bad-arg (cdr args)))))

(defun process-defabbrev-declares
  (decls)
  (cond ((endp decls) nil)
    ((not (and (consp (car decls))
         (eq (caar decls) 'declare)
         (true-list-listp (cdar decls))
         (subsetp-eq (strip-cars (cdar decls))
           '(ignore ignorable type)))) (er hard
        'process-defabbrev-declares
        "In a DEFABBREV form, each expression after the argument list ~
              but before the body must be of the form (DECLARE decl1 .. ~
              declk), where each dcli is of the form (IGNORE ..), (IGNORABLE ~
              ..), or (TYPE ..).  The form ~x0 is thus illegal."
        (car decls)))
    (t (cons (kwote (car decls))
        (process-defabbrev-declares (cdr decls))))))

(defun defabbrev1
  (lst)
  (declare (xargs :guard (true-listp lst)))
  (cond ((null lst) nil)
    (t (cons (list 'list (list 'quote (car lst)) (car lst))
        (defabbrev1 (cdr lst))))))

(defun get-sharp-atsign
  (i)
  (declare (xargs :guard (posp i)))
  (cond ((<= i *iprint-hard-bound-default*) (aref1 'sharp-atsign-ar *sharp-atsign-ar* i))
    (t (make-sharp-atsign i))))

(defun iprint-alistp1
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) (null x))
    ((atom (cdr x)) (and (consp (car x)) (posp (caar x)) (null (cdr x))))
    (t (and (consp (car x))
        (posp (caar x))
        (consp (car (cdr x)))
        (integerp (caar (cdr x)))
        (< (caar (cdr x)) (caar x))
        (iprint-alistp1 (cdr x))))))

(defun iprint-alistp
  (x)
  (declare (xargs :guard t))
  (or (eq x t) (natp x) (iprint-alistp1 x)))

(defun update-iprint-alist-fal
  (iprint-alist iprint-fal-new iprint-fal-old val)
  (declare (xargs :guard (and (iprint-alistp iprint-alist)
        (not (symbolp iprint-alist)))))
  (let ((pair (and iprint-fal-old
         (or (hons-get val iprint-fal-new)
           (hons-get val iprint-fal-old)))))
    (cond (pair (mv (cdr pair) iprint-alist iprint-fal-new))
      ((consp iprint-alist) (let ((index (1+ (caar iprint-alist))))
          (mv index
            (acons index val iprint-alist)
            (and iprint-fal-old (hons-acons val index iprint-fal-new)))))
      (t (let ((index (1+ iprint-alist)))
          (mv index
            (acons index val nil)
            (and iprint-fal-old (hons-acons val index iprint-fal-new))))))))

(defun eviscerate
  (x print-level
    print-length
    alist
    evisc-table
    hiding-cars
    iprint-alist
    iprint-fal-new
    iprint-fal-old
    eager-p)
  (declare (xargs :guard (and (or (null print-level) (integerp print-level))
        (or (null print-length) (integerp print-length))
        (alistp alist)
        (symbol-listp hiding-cars)
        (iprint-alistp iprint-alist)
        (iprint-falp iprint-fal-new)
        (iprint-falp iprint-fal-old))))
  (cond ((and (null print-level) (null print-length)) (cond ((eviscerate1p x alist evisc-table hiding-cars) (eviscerate1 x
            0
            -1
            -1
            alist
            evisc-table
            hiding-cars
            nil
            nil
            nil
            nil))
        (t (mv x iprint-alist iprint-fal-new))))
    (t (eviscerate1 (if eager-p
          (hons-copy x)
          x)
        0
        (or print-level -1)
        (or print-length -1)
        alist
        evisc-table
        hiding-cars
        iprint-alist
        iprint-fal-new
        iprint-fal-old
        eager-p))))

(defun eviscerate-simple
  (x print-level print-length alist evisc-table hiding-cars)
  (declare (xargs :guard (and (or (null print-level) (integerp print-level))
        (or (null print-length) (integerp print-length))
        (alistp alist)
        (symbol-listp hiding-cars))))
  (mv-let (result null-iprint-alist null-iprint-fal)
    (eviscerate x
      print-level
      print-length
      alist
      evisc-table
      hiding-cars
      nil
      nil
      nil
      nil)
    (declare (ignorable null-iprint-alist null-iprint-fal))
    (assert* (and (booleanp null-iprint-alist) (null null-iprint-fal))
      result)))

(defun bounded-integer-listp
  (i j lst)
  (declare (xargs :guard (and (integerp i) (or (integerp j) (eq j 'infinity)))))
  (cond ((consp lst) (and (integerp (car lst))
        (<= i (car lst))
        (or (eq j 'infinity) (<= (car lst) j))
        (bounded-integer-listp i j (cdr lst))))
    (t (null lst))))

(defun aset1-lst
  (name alist ar)
  (declare (xargs :guard (eqlable-alistp alist)))
  (declare (xargs :guard (and (alistp alist)
        (array1p name ar)
        (bounded-integer-listp 0
          (- (car (dimensions name ar)) 1)
          (strip-cars alist)))))
  (cond ((endp alist) ar)
    (t (aset1-lst name
        (cdr alist)
        (aset1 name ar (caar alist) (cdar alist))))))

(defun iprint-hard-bound
  (state)
  (f-get-global 'iprint-hard-bound state))

(defun iprint-soft-bound
  (state)
  (f-get-global 'iprint-soft-bound state))

(defun iprint-last-index
  (state)
  (declare (xargs :guard (array1p 'iprint-ar (f-get-global 'iprint-ar state))))
  (iprint-last-index* (f-get-global 'iprint-ar state)))

(defun iprint-ar-illegal-index
  (index state)
  (declare (xargs :guard (and (natp index)
        (array1p 'iprint-ar (f-get-global 'iprint-ar state))
        (natp (iprint-last-index state))
        (or (null (default 'iprint-ar (f-get-global 'iprint-ar state)))
          (integerp (default 'iprint-ar (f-get-global 'iprint-ar state)))))))
  (or (zp index)
    (let* ((iprint-ar (f-get-global 'iprint-ar state)) (bound (default 'iprint-ar iprint-ar)))
      (if (null bound)
        (> index (iprint-last-index* iprint-ar))
        (> index bound)))))

(defun iprint-enabledp
  (state)
  (declare (xargs :guard (array1p 'iprint-ar (f-get-global 'iprint-ar state))))
  (natp (aref1 'iprint-ar (f-get-global 'iprint-ar state) 0)))

(defun iprint-blockedp
  (state)
  (declare (xargs :guard (array1p 'iprint-ar (f-get-global 'iprint-ar state))))
  (let ((x (aref1 'iprint-ar (f-get-global 'iprint-ar state) 0)))
    (and (consp x) (cdr x))))

(defun iprint-ar-aref1
  (index state)
  (declare (xargs :guard (and (posp index)
        (array1p 'iprint-ar (f-get-global 'iprint-ar state))
        (< index
          (car (dimensions 'iprint-ar (f-get-global 'iprint-ar state)))))))
  (let ((iprint-ar (f-get-global 'iprint-ar state)))
    (aref1 'iprint-ar iprint-ar index)))

(defun iprint-alistp1-weak
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) (null x))
    (t (and (consp (car x))
        (posp (caar x))
        (iprint-alistp1-weak (cdr x))))))

(defun collect-posp-indices-to-header
  (ar acc)
  (declare (xargs :guard (and (array1p 'iprint-ar ar) (iprint-alistp1-weak acc))))
  (cond ((endp ar) (er hard
        'collect-posp-indices-to-header
        "Implementation error: Failed to find :HEADER as expected!"))
    ((eq (caar ar) :header) acc)
    (t (collect-posp-indices-to-header (cdr ar)
        (if (eql (caar ar) 0)
          acc
          (cons (car ar) acc))))))

(defun iprint-fal-name
  (iprint-fal)
  (declare (xargs :guard (iprint-falp iprint-fal)))
  (if (consp iprint-fal)
    (cdr (last iprint-fal))
    iprint-fal))

(defun iprint-eager-p
  (iprint-fal)
  (declare (xargs :guard (iprint-falp iprint-fal)))
  (eq (iprint-fal-name iprint-fal) :eager))

(defun init-iprint-fal
  (sym state)
  (declare (xargs :guard (and (symbolp sym)
        (iprint-falp (f-get-global 'iprint-fal state)))))
  (let* ((old-iprint-fal (f-get-global 'iprint-fal state)) (old-iprint-name (iprint-fal-name old-iprint-fal))
      (new-iprint-fal (cond ((null sym) nil)
          ((eq sym t) :iprint-fal)
          ((eq sym :same) old-iprint-name)
          (t sym))))
    (prog2$ (and (consp old-iprint-fal)
        (fast-alist-free old-iprint-fal))
      (pprogn (f-put-global 'iprint-fal new-iprint-fal state)
        (mv (cond ((eq old-iprint-name new-iprint-fal) nil)
            (new-iprint-fal (msg "Iprinting is enabled with~@0 sharing, with a ~
                                fast-alist whose name is ~x1."
                (if (iprint-eager-p new-iprint-fal)
                  " eager"
                  "")
                new-iprint-fal))
            (t (msg "Iprinting is enabled without sharing.")))
          state)))))

(defun rollover-iprint-ar
  (iprint-alist last-index state)
  (declare (xargs :guard (and (iprint-alistp1 iprint-alist)
        (consp iprint-alist)
        (iprint-falp (f-get-global 'iprint-fal state))
        (array1p 'iprint-ar (f-get-global 'iprint-ar state))
        (posp last-index)
        (equal last-index (caar iprint-alist))
        (iprint-array-p (f-get-global 'iprint-ar state) last-index)
        (natp (f-get-global 'iprint-hard-bound state))
        (<= (* 4 (1+ (f-get-global 'iprint-hard-bound state)))
          (array-maximum-length-bound)))))
  (let* ((old-iprint-ar (f-get-global 'iprint-ar state)) (new-dim (1+ (max (iprint-hard-bound state) last-index)))
      (new-max-len (* 4 new-dim)))
    (cond ((< (array-maximum-length-bound) new-max-len) (prog2$ (er hard?
            'rollover-iprint-ar
            "Attempted to expand iprint-ar to a maximum-length of ~x0, ~
            exceeding (array-maximum-length-bound), which is ~x1."
            new-max-len
            (array-maximum-length-bound))
          state))
      (t (let* ((new-header `(:header :dimensions (,NEW-DIM)
               :maximum-length ,NEW-MAX-LEN
               :default ,LAST-INDEX
               :name iprint-ar
               :order :none)) (new-iprint-ar (compress1 'iprint-ar
                (cons new-header
                  (acons 0
                    0
                    (collect-posp-indices-to-header old-iprint-ar iprint-alist))))))
          (mv-let (msg state)
            (init-iprint-fal :same state)
            (declare (ignore msg))
            (f-put-global 'iprint-ar new-iprint-ar state)))))))

(defun update-iprint-fal-rec
  (iprint-fal-new iprint-fal-old)
  (declare (xargs :guard (iprint-falp iprint-fal-new)))
  (cond ((atom iprint-fal-new) iprint-fal-old)
    (t (update-iprint-fal-rec (cdr iprint-fal-new)
        (hons-acons (caar iprint-fal-new)
          (cdar iprint-fal-new)
          iprint-fal-old)))))

(defun update-iprint-fal
  (iprint-fal-new state)
  (declare (xargs :guard (iprint-falp iprint-fal-new)))
  (cond ((atom iprint-fal-new) state)
    (t (f-put-global 'iprint-fal
        (update-iprint-fal-rec iprint-fal-new
          (f-get-global 'iprint-fal state))
        state))))

(defun update-iprint-ar-fal
  (iprint-alist iprint-fal-new iprint-fal-old state)
  (declare (xargs :guard (and (iprint-alistp1 iprint-alist)
        (consp iprint-alist)
        (equal iprint-fal-old (f-get-global 'iprint-fal state))
        (iprint-falp iprint-fal-old)
        (array1p 'iprint-ar (f-get-global 'iprint-ar state))
        (iprint-array-p (f-get-global 'iprint-ar state)
          (caar iprint-alist))
        (natp (f-get-global 'iprint-hard-bound state))
        (< (f-get-global 'iprint-hard-bound state)
          (car (dimensions 'iprint-ar (f-get-global 'iprint-ar state))))
        (<= (* 4 (1+ (f-get-global 'iprint-hard-bound state)))
          (array-maximum-length-bound))
        (iprint-falp iprint-fal-new))))
  (let ((last-index (caar iprint-alist)))
    (cond ((> last-index (iprint-hard-bound state)) (rollover-iprint-ar iprint-alist last-index state))
      (t (assert$ (or (null iprint-fal-old)
            (equal (f-get-global 'iprint-fal state) iprint-fal-old))
          (pprogn (update-iprint-fal iprint-fal-new state)
            (f-put-global 'iprint-ar
              (aset1-lst 'iprint-ar
                (acons 0 last-index iprint-alist)
                (f-get-global 'iprint-ar state))
              state)))))))

(defun brr-evisc-tuple-oracle-update@par nil nil)

(defun iprint-oracle-updates@par nil nil)

(defun iprint-oracle-updates?
  (state)
  (declare (xargs :guard (array1p 'iprint-ar (f-get-global 'iprint-ar state))))
  (cond ((iprint-blockedp state) state)
    (t (iprint-oracle-updates state))))

(defun eviscerate-top-state-p
  (state)
  (declare (xargs :stobjs state))
  (and (natp (f-get-global 'iprint-hard-bound state))
    (iprint-falp (f-get-global 'iprint-fal state))
    (array1p 'iprint-ar (f-get-global 'iprint-ar state))
    (consp (f-get-global 'iprint-ar state))
    (natp (iprint-last-index state))
    (iprint-array-p (f-get-global 'iprint-ar state)
      (1+ (iprint-last-index state)))
    (<= (* 4 (1+ (f-get-global 'iprint-hard-bound state)))
      (array-maximum-length-bound))
    (< (f-get-global 'iprint-hard-bound state)
      (car (dimensions 'iprint-ar (f-get-global 'iprint-ar state))))
    (= (maximum-length 'iprint-ar (f-get-global 'iprint-ar state))
      (* 4
        (car (dimensions 'iprint-ar (f-get-global 'iprint-ar state)))))))

(defun eviscerate-top
  (x print-level
    print-length
    alist
    evisc-table
    hiding-cars
    state)
  (declare (xargs :guard (and (or (null print-level) (integerp print-level))
        (or (null print-length) (integerp print-length))
        (alistp alist)
        (symbol-listp hiding-cars)
        (eviscerate-top-state-p 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 x
          print-level
          print-length
          alist
          evisc-table
          hiding-cars
          (and (iprint-enabledp state) (iprint-last-index state))
          nil
          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 xxxjoin-fixnum
  (fn args root)
  (declare (xargs :guard (true-listp args)))
  (if (cdr args)
    (list 'the-fixnum
      (list fn
        (list 'the-fixnum (car args))
        (xxxjoin-fixnum fn (cdr args) root)))
    (if args
      (list 'the-fixnum (car args))
      root)))

(defun symbol-to-fixnat-alistp
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) (eq x nil))
    (t (and (consp (car x))
        (symbolp (car (car x)))
        (fixnat-guard (cdr (car x)))
        (symbol-to-fixnat-alistp (cdr x))))))

(defun special-term-num
  (sym state)
  (declare (xargs :guard (and (symbolp sym)
        (symbol-to-fixnat-alistp (table-alist 'ppr-special-syms (w state))))))
  (let ((pair (assoc-eq sym (table-alist 'ppr-special-syms (w state)))))
    (and pair (cdr pair))))

(defun set-ppr-flat-right-margin
  (val state)
  (if (posp val)
    (f-put-global 'ppr-flat-right-margin val state)
    (prog2$ (illegal 'set-ppr-flat-right-margin
        "Set-ppr-flat-right-margin takes a positive integer ~
                      argument, unlike ~x0."
        (list (cons #\0 val)))
      state)))

(defun keyword-param-valuep
  (tuple eviscp)
  (declare (type cons tuple)
    (xargs :guard (ppr-tuple-p tuple)))
  (or (and (eq (car tuple) 'flat)
      (not (or (atom (cddr tuple)) (evisceratedp eviscp (cddr tuple))))
      (null (cdr (cddr tuple))))
    (eq (car tuple) 'quote)
    (eq (car tuple) 'wide)
    (integerp (car tuple))))

(defun cons-ppr1-guardp
  (x column width ppr-flat-right-margin)
  (declare (xargs :guard t))
  (and (ppr-tuple-p x)
    (ppr-tuple-lst-p column)
    (unsigned-byte-p 57 width)
    (unsigned-byte-p 57 ppr-flat-right-margin)
    (cond ((eq (car x) 'flat) (and (consp (cddr x)) (null (cdddr x))))
      (t t))
    (cond ((eq (car x) 'dot) (and (consp column)
          (consp (car column))
          (implies (eq (car (car column)) 'flat)
            (consp (cddr (car column))))))
      (t t))))

(defun cons-ppr1
  (x column
    width
    ppr-flat-right-margin
    pair-keywords-p
    eviscp)
  (declare (type cons x)
    (type (unsigned-byte 57) width ppr-flat-right-margin)
    (xargs :guard (cons-ppr1-guardp x column width ppr-flat-right-margin)
      :split-types t))
  (cond ((and (eq (car x) 'flat)
       (or (atom (car (cddr x)))
         (evisceratedp eviscp (car (cddr x))))
       (consp column)) (let ((x1 (car (cddr x))) (row1 (car column)))
        (cond ((keywordp x1) (cond ((and (keyword-param-valuep row1 eviscp)
                 (or pair-keywords-p
                   (null (cdr column))
                   (eq (car (cadr column)) 'keypair)
                   (eq (car (cadr column)) 'matched-keyword))) (let ((n (+g! (cadr x) 1 (cadr row1))))
                  (declare (type (unsigned-byte 57) n))
                  (cond ((<= n width) (cons (cons 'keypair (cons n (cons x row1))) (cdr column)))
                    (t (cons (cons 'matched-keyword (cdr x)) column)))))
              ((eq (car row1) 'flat) (let ((n (+g! (cadr x) 1 (cadr row1))))
                  (declare (type (unsigned-byte 57) n))
                  (cond ((and (<= n ppr-flat-right-margin) (<= n width)) (cons (cons 'flat (cons n (cons x1 (cddr row1))))
                        (cdr column)))
                    (t (cons x column)))))
              (t (cons x column))))
          ((eq (car row1) 'flat) (let ((n (+g! (cadr x) 1 (cadr row1))))
              (declare (type (unsigned-byte 57) n))
              (cond ((and (<= n ppr-flat-right-margin) (<= n width)) (cons (cons 'flat (cons n (cons x1 (cddr row1))))
                    (cdr column)))
                (t (cons x column)))))
          (t (cons x column)))))
    ((and (eq (car x) 'dot) (consp column)) (let ((row1 (car column)))
        (cond ((eq (car row1) 'flat) (let ((n (+g! (cadr x) 1 (cadr row1))))
              (declare (type (unsigned-byte 57) n))
              (cond ((and (<= n ppr-flat-right-margin) (<= n width)) (cons (cons 'flat (cons n (car (cddr row1)))) (cdr column)))
                (t (cons x column)))))
          (t (cons x column)))))
    (t (cons x column))))

(defun flsz-integer
  (x print-base acc)
  (declare (type integer x)
    (type (unsigned-byte 5) print-base)
    (type (unsigned-byte 60) acc)
    (xargs :guard (print-base-p print-base)
      :ruler-extenders :lambdas :measure (cond ((not (and (integerp x)
             (natp acc)
             (< acc (fixnum-bound))
             (print-base-p print-base))) 0)
        ((< x 0) (+ 1 (- x)))
        ((< x print-base) 0)
        (t x))))
  (the-fixnat (cond ((not (mbt (and (integerp x) (natp acc) (print-base-p print-base)))) 0)
      ((mbe :logic (>= acc (fixnum-bound))
         :exec (= acc (fixnum-bound))) (fixnum-bound))
      ((< x 0) (flsz-integer (- x) print-base (1+f acc)))
      ((< x print-base) (1+f acc))
      (t (flsz-integer (truncate x print-base)
          print-base
          (1+f acc))))))

(defun flsz-atom
  (x print-base print-radix acc state)
  (declare (type (unsigned-byte 5) print-base)
    (type (unsigned-byte 60) acc)
    (xargs :guard (print-base-p print-base)
      :ruler-extenders :lambdas :measure (cond ((not (fixnat-guard acc)) 0) (t (acl2-count x)))))
  (the-fixnat (cond ((not (mbt (fixnat-guard acc))) 0)
      ((integerp x) (flsz-integer x
          print-base
          (cond ((null print-radix) acc)
            ((int= print-base 10) (+f! 1 acc))
            (t (+f! 2 acc)))))
      ((symbolp x) (the-fixnat (let* ((s (symbol-name x)) (len (min (fixnum-bound) (length s)))
              (s-sz (cond ((needs-slashes s state) (+f! 2 len)) (t len)))
              (acc (+f! acc s-sz)))
            (declare (type string s)
              (type (unsigned-byte 60) len s-sz acc))
            (the-fixnat (cond ((keywordp x) (+f! 1 acc))
                ((symbol-in-current-package-p x state) acc)
                (t (let* ((p (symbol-package-name x)) (p-len (min (fixnum-bound) (length p))))
                    (declare (type string p)
                      (type (unsigned-byte 60) p-len))
                    (cond ((needs-slashes p state) (+f! 4 acc p-len))
                      (t (+f! 2 acc p-len))))))))))
      ((rationalp x) (flsz-integer (numerator x)
          print-base
          (flsz-integer (denominator x)
            print-base
            (cond ((null print-radix) (+f! 1 acc))
              ((= print-base 10) (+f! 5 acc))
              (t (+f! 3 acc))))))
      ((complex-rationalp x) (flsz-atom (realpart x)
          print-base
          print-radix
          (mbe :logic (min (fixnum-bound)
              (max 0
                (flsz-atom (imagpart x) print-base print-radix acc state)))
            :exec (flsz-atom (imagpart x) print-base print-radix acc state))
          state))
      ((stringp x) (+f! 2 acc (min (fixnum-bound) (length x))))
      ((characterp x) (cond ((eql x #\
) (+f! 9 acc))
          ((eql x #\) (+f! 8 acc))
          ((eql x #\
) (+f! 8 acc))
          ((eql x #\ ) (+f! 7 acc))
          ((eql x #\) (+f! 6 acc))
          ((eql x #\	) (+f! 5 acc))
          (t (+f! 3 acc))))
      (t 0))))

(defun flsz1
  (x print-base print-radix j maximum state eviscp)
  (declare (type (unsigned-byte 5) print-base)
    (type (unsigned-byte 57) j maximum)
    (xargs :guard (print-base-p print-base)
      :measure (acl2-count x)
      :ruler-extenders :lambdas :verify-guards nil))
  (the-small t
    (cond ((> j maximum) j)
      ((atom x) (round-to-small t
          (flsz-atom x print-base print-radix j state)))
      ((evisceratedp eviscp x) (if (stringp (cdr x))
          (let ((p (search *newline-string* (cdr x) :from-end t)))
            (cond (p (+g! 1 maximum))
              (t (+g! j (min (length (cdr x)) *small-hi*)))))
          (+g! 1 maximum)))
      ((atom (cdr x)) (cond ((null (cdr x)) (flsz1 (car x)
              print-base
              print-radix
              (+g! 2 j)
              maximum
              state
              eviscp))
          (t (flsz1 (cdr x)
              print-base
              print-radix
              (flsz1 (car x)
                print-base
                print-radix
                (+g! 5 j)
                maximum
                state
                eviscp)
              maximum
              state
              eviscp))))
      ((and (eq (car x) 'quote) (consp (cdr x)) (null (cddr x))) (flsz1 (cadr x)
          print-base
          print-radix
          (+g! 1 j)
          maximum
          state
          eviscp))
      (t (flsz1 (cdr x)
          print-base
          print-radix
          (flsz1 (car x)
            print-base
            print-radix
            (+g! 1 j)
            maximum
            state
            eviscp)
          maximum
          state
          eviscp)))))

(defun fmt-state-p
  (state)
  (declare (xargs :stobjs state))
  (and (state-p state)
    (small-nat-guard (f-get-global 'fmt-hard-right-margin state))
    (small-nat-guard (f-get-global 'fmt-soft-right-margin state))
    (alistp (table-alist 'evisc-table (w state)))
    (eviscerate-top-state-p state)
    (equal (array-order (header 'iprint-ar (f-get-global 'iprint-ar state)))
      nil)
    (small-nat-guard (ppr-flat-right-margin))
    (symbol-to-fixnat-alistp (table-alist 'ppr-special-syms (w state)))
    (not (assoc-eq 'quote (table-alist 'ppr-special-syms (w state))))))

(defun flsz
  (x j maximum state eviscp)
  (declare (type (unsigned-byte 60) j maximum)
    (xargs :guard (fmt-state-p state)))
  (flsz1 x
    (the-fixnat (print-base))
    (print-radix)
    (round-to-small t j)
    (round-to-small t maximum)
    state
    eviscp))

(defun max-width
  (lst maximum)
  (declare (type (signed-byte 58) maximum)
    (xargs :guard (ppr-tuple-lst-p lst)))
  (cond ((endp lst) maximum)
    ((> (cadr (car lst)) maximum) (max-width (cdr lst) (cadr (car lst))))
    (t (max-width (cdr lst) maximum))))

(defun newline
  (channel state)
  (declare (xargs :guard (and (symbolp channel)
        (open-output-channel-p channel :character state))))
  (princ$ #\
 channel state))

(defun fmt-hard-right-margin
  (state)
  (declare (xargs :guard (small-nat-guard (f-get-global 'fmt-hard-right-margin state))))
  (the (unsigned-byte 57)
    (f-get-global 'fmt-hard-right-margin state)))

(defun fmt-soft-right-margin
  (state)
  (declare (xargs :guard (small-nat-guard (f-get-global 'fmt-soft-right-margin state))))
  (the (unsigned-byte 57)
    (f-get-global 'fmt-soft-right-margin state)))

(defun set-fmt-hard-right-margin
  (n state)
  (declare (xargs :guard t :stobjs state))
  (cond ((and (small-nat-guard n) (not (= n 0))) (f-put-global 'fmt-hard-right-margin n state))
    (t (prog2$ (er hard?
          'set-fmt-hard-right-margin
          "The fmt-hard-right-margin must be a positive integer no ~
                   greater than ~x0, but ~x1 is not."
          *small-hi*
          n)
        state))))

(defun set-fmt-soft-right-margin
  (n state)
  (declare (xargs :guard t :stobjs state))
  (cond ((and (small-nat-guard n) (not (= n 0))) (f-put-global 'fmt-soft-right-margin n state))
    (t (prog2$ (er hard?
          'set-fmt-soft-right-margin
          "The fmt-soft-right-margin must be a positive integer no ~
                   greater than ~x0, but ~x1 is not."
          *small-hi*
          n)
        state))))

(defun write-for-read
  (state)
  (declare (xargs :guard t))
  (f-get-global 'write-for-read state))

(defun spaces1
  (n col hard-right-margin channel state)
  (declare (type (unsigned-byte 60) n col)
    (type (unsigned-byte 57) hard-right-margin)
    (type symbol channel)
    (xargs :measure (nfix (+ (* 2 n) col))
      :guard (open-output-channel-p channel :character state)))
  (cond ((mbt (and (natp n) (natp col) (natp hard-right-margin))) (cond ((= n 0) state)
        ((> col hard-right-margin) (pprogn (if (write-for-read state)
              state
              (princ$ #\\ channel state))
            (newline channel state)
            (spaces1 n 0 hard-right-margin channel state)))
        (t (pprogn (princ$ #\  channel state)
            (spaces1 (the (unsigned-byte 60) (1- n))
              (the (unsigned-byte 60) (1+ col))
              hard-right-margin
              channel
              state)))))
    (t state)))

(defun make-spaces-array-rec
  (n acc)
  (if (zp n)
    (cons (cons 0 "") acc)
    (make-spaces-array-rec (1- n)
      (cons (cons n (coerce (make-list n :initial-element #\ ) 'string))
        acc))))

(defun make-spaces-array
  (n)
  (compress1 'acl2-built-in-spaces-array
    (cons `(:header :dimensions (,(1+ N))
        :maximum-length ,(+ 2 N)
        :default nil
        :name acl2-built-in-spaces-array)
      (make-spaces-array-rec n nil))))

(defun spaces
  (n col channel state)
  (declare (type (unsigned-byte 60) n col)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (open-output-channel-p channel :character state))))
  (let ((hard-right-margin (fmt-hard-right-margin state)) (result-col (+f! n col)))
    (declare (type (unsigned-byte 57) hard-right-margin)
      (type (unsigned-byte 60) result-col))
    (if (and (<= result-col hard-right-margin) (<= n 200))
      (princ$ (aref1 'acl2-built-in-spaces-array
          *acl2-built-in-spaces-array*
          n)
        channel
        state)
      (spaces1 n col hard-right-margin channel state))))

(defun flpr
  (x channel state eviscp)
  (declare (type symbol channel)
    (xargs :guard (open-output-channel-p channel :character state)))
  (flpr1 x channel state eviscp))

(defun ppr2-flat
  (x channel state eviscp)
  (declare (xargs :guard (and (symbolp channel)
        (open-output-channel-p channel :character state))))
  (cond ((null x) state)
    ((or (atom x) (evisceratedp eviscp x)) (pprogn (princ$ #\. channel state)
        (princ$ #\  channel state)
        (flpr1 x channel state eviscp)))
    (t (pprogn (flpr1 (car x) channel state eviscp)
        (cond ((cdr x) (pprogn (princ$ #\  channel state)
              (ppr2-flat (cdr x) channel state eviscp)))
          (t state))))))

(defun ppr
  (x col channel state eviscp)
  (declare (type (unsigned-byte 57) col)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (open-output-channel-p channel :character state))))
  (let ((fmt-hard-right-margin (fmt-hard-right-margin state)))
    (declare (type (unsigned-byte 57) fmt-hard-right-margin))
    (cond ((< col fmt-hard-right-margin) (ppr2 (ppr1 x
            (print-base)
            (print-radix)
            (-g! fmt-hard-right-margin col)
            0
            state
            eviscp)
          col
          channel
          state
          eviscp))
      (t (let ((er (er hard?
               'ppr
               "The `col' argument to ppr must be less than value ~
                    of the state global variable ~
                    fmt-hard-right-margin, but ~x0 is not less than ~
                    ~x1."
               col
               fmt-hard-right-margin)))
          (declare (ignore er))
          state)))))

(defun illegal-fmt-string
  (key)
  (declare (xargs :guard (member-eq key *illegal-fmt-keys*)))
  (case key
    (bad-evisc-tuple "In the fmt string displayed below, the tilde directive at location ~x0 ~
      associates character ~x1 with ~x2, which does not satisfy ~x3.~|~%~x4")
    (bad-tilde-&v-arg "The tilde directive at location ~x0 in the fmt string below uses the ~
      variable ~x1.  That ~s2 directive requires a true list, but it was ~
      supplied the value ~x3.~|~%~x4")
    (bad-tilde-*-arg "The tilde directive, ~~*, at location ~x0 in the fmt string below uses ~
      the variable ~x1.  That directive requires a list of the form ("str0" ~
      "str1" "str2" "str3" lst . alist) such that lst is a true-list ~
      and alist satisfies ~x2, but it was supplied the value ~x3.~|~%~x4")
    (bad-tilde-@-arg "The tilde-@ directive at position ~x0 of the string below is illegal ~
      because its variable evaluated to ~x1, which does not satisfy ~
      ~x2.~|~%~x3")
    (bad-tilde-c-arg "The tilde-c directive at position ~x0 of the string below is illegal ~
      because its variable evaluated to ~x1, which is not of the form (n . ~
      width), where n and width are integers and width is nonnegative.~|~%~x2")
    (bad-tilde-n-arg "The tilde directive at location ~x0 in the fmt string below uses the ~
      variable ~x1.  That ~s2 directive requires either an integer or a CONS ~
      whose CAR is an integer, but it was supplied the value ~x3.~|~%~x4")
    (bad-tilde-s-arg "The tilde-~s0 directive at position ~x1 of the string below is illegal ~
      because its variable evaluated to ~x2, which is not a symbol, a string, ~
      or a number.~|~%~x3")
    (bad-tilde-t-arg-natp "It is illegal to tab past the value of (@ fmt-hard-right-margin), ~x0, ~
      and hence the directive ~~t~s1 to tab to column ~x2 is illegal.  See ~
      :DOC set-fmt-hard-right-margin.")
    (bad-tilde-t-arg-not-natp "The tilde directive at location ~x0 in the fmt string below uses the ~
      variable ~x1.  That ~~t directive requires a natural number, but it was ~
      supplied the value ~x2.~|~%~x3")
    (bad-tilde-_-arg "The tilde-_ directive at position ~x0 of the string below is illegal ~
      because its variable evaluated to ~x1, which fails to be a natural ~
      number not exceeding ~x2.~|~%~x3")
    (find-alternative-skip "While looking for the terminating bracket of a tilde alternative ~
      directive in the string below we ran off the end of the string.~|~%~x0")
    (find-alternative-start "The tilde-# directive at ~x0 in the fmt string below must be followed ~
      immediately by ~~[.~|~%~x1")
    (find-alternative-start1-a "The tilde-# directive ~s0 at position ~x1 of the string below ~
      does not have enough alternative clauses.  When the terminal bracket ~
      was reached we still needed ~#2~[~/1 more alternative~/~x3 more ~
      alternatives~].~|~%~x4")
    (find-alternative-start1-b "While searching for the appropriate alternative clause of a tilde-# ~
      directive in the string below, we ran off the end of the string.~|~%~x0")
    (find-alternative-stop "While looking for the end of a tilde-# directive's alternative clause ~
      in the string below, we ran off the end of the string.~|~%~x0")
    (tilde-arg-points-past-string "The tilde directive at location ~x0 in the fmt string below requires ~
      that we look at the character ~x1 further down in the string.  But the ~
      string terminates at location ~x2.~|~%~x3")
    (unbound-tilde-arg "Unbound Fmt Variable.  The tilde directive at location ~x0 in the fmt ~
      string below uses the variable ~x1.  But this variable is not bound in ~
      the association list, ~x2, supplied with the fmt string.~|~%~x3")
    (unrecognized-tilde-arg "The tilde directive at position ~x0 of the string below is ~
      unrecognized.~|~%~x1")
    (otherwise (er hard
        'illegal-fmt-string
        "Implementation error in illegal-fmt-string: unknown key, ~x0."
        key))))

(defun scan-past-whitespace
  (s i maximum)
  (declare (type (unsigned-byte 60) i maximum)
    (type string s)
    (xargs :guard (<= maximum (length s))
      :measure (nfix (- maximum i))
      :ruler-extenders :all))
  (the-fixnat (cond ((not (mbt (and (integerp i) (integerp maximum)))) maximum)
      ((< i maximum) (cond ((member (charf s i) '(#\  #\	 #\
)) (scan-past-whitespace s (+f i 1) maximum))
          (t i)))
      (t maximum))))

(defun zero-one-or-more
  (x)
  (declare (xargs :guard (or (integerp x) (true-listp x))))
  (let ((n (cond ((integerp x) x) (t (length x)))))
    (case n (0 0) (1 1) (otherwise 2))))

(defun find-alternative-skip
  (s i maximum quiet)
  (declare (type (unsigned-byte 60) i maximum)
    (type string s)
    (xargs :guard (and (<= maximum (length s)) (<= i maximum))
      :measure (nfix (- maximum i))
      :ruler-extenders :lambdas))
  (the-fixnat (cond ((and (mbt (and (integerp i) (integerp maximum)))
         (< i (1-f maximum))) (let ((char-s-i (charf s i)))
          (declare (type character char-s-i))
          (case char-s-i
            (#\~ (let ((i+2 (+f 2 i)) (char-s-1+i (charf s (1+f i))))
                (declare (type character char-s-1+i)
                  (type (unsigned-byte 60) i+2))
                (case char-s-1+i
                  (#\] i+2)
                  (#\[ (let ((new-i (find-alternative-skip s i+2 maximum quiet)))
                      (declare (type (unsigned-byte 60) new-i))
                      (cond ((and (not (= new-i 0))
                           (mbt (and (integerp new-i) (< i new-i)))) (find-alternative-skip s new-i maximum quiet))
                        (t 0))))
                  (otherwise (find-alternative-skip s i+2 maximum quiet)))))
            (otherwise (find-alternative-skip s (+f 1 i) maximum quiet)))))
      (t (er-hard?-val? 0
          quiet
          'find-alternative-skip
          "~@0"
          (illegal-fmt-msg find-alternative-skip s))))))

(defun find-alternative-start1
  (x s i maximum quiet)
  (declare (type (unsigned-byte 60) x i maximum)
    (type string s)
    (xargs :guard (and (<= maximum (length s)) (<= i maximum))
      :measure (nfix (- maximum i))
      :ruler-extenders :lambdas))
  (the-fixnat (cond ((= x 0) i)
      ((and (mbt (and (natp x) (integerp i) (integerp maximum)))
         (< i (1-f maximum))) (let ((char-s-i (charf s i)))
          (declare (type character char-s-i))
          (case char-s-i
            (#\~ (let ((char-s-1+-i (charf s (1+f i))))
                (declare (type character char-s-1+-i))
                (case char-s-1+-i
                  (#\/ (find-alternative-start1 (1-f x) s (+f 2 i) maximum quiet))
                  (#\] (er-hard?-val? 0
                      quiet
                      'find-alternative-start1
                      "~@0"
                      (illegal-fmt-msg find-alternative-start1-a
                        "terminating"
                        i
                        (zero-one-or-more x)
                        x
                        s)))
                  (#\[ (let ((k (find-alternative-skip s (+f 2 i) maximum quiet)))
                      (declare (type (unsigned-byte 60) k))
                      (cond ((= k 0) 0)
                        (t (find-alternative-start1 x s k maximum quiet)))))
                  (otherwise (find-alternative-start1 x s (+f 2 i) maximum quiet)))))
            (otherwise (find-alternative-start1 x s (+f 1 i) maximum quiet)))))
      (t (er-hard?-val? 0
          quiet
          'find-alternative-start1
          "~@0"
          (illegal-fmt-msg find-alternative-start1-b s))))))

(defun fmt-char
  (s i j maximum err-flg)
  (declare (type (unsigned-byte 60) i maximum)
    (type (integer 1 4) j)
    (type string s)
    (xargs :guard (and (<= maximum (length s)) (< i maximum))))
  (the character
    (let ((index (+f! i j)))
      (declare (type (unsigned-byte 60) index))
      (cond ((< index maximum) (charf s index))
        (t (prog2$ (cond (err-flg (mv-let (i j)
                  (if (or (= 0 i)
                      (eql (charf s i) #\~)
                      (not (eql (charf s (1-f i)) #\~)))
                    (mv i j)
                    (mv (1-f i) (1+f j)))
                  (er hard?
                    'fmt-char
                    "~@0"
                    (illegal-fmt-msg tilde-arg-points-past-string i j maximum s))))
              (t nil))
            *null-char*))))))

(defun find-alternative-start
  (x s i maximum quiet)
  (declare (type (unsigned-byte 60) i maximum)
    (type string s)
    (xargs :guard (<= maximum (length s))))
  (the-fixnat (cond ((not (< i (-f maximum 4))) (er-hard?-val? 0
          quiet
          'find-alternative-start
          "~@0"
          (illegal-fmt-msg tilde-arg-points-past-string i 4 maximum s)))
      (t (let ((x (cond ((natp x) (the-fixnat! x 'find-alternative-start))
               ((and (consp x) (atom (cdr x))) 0)
               (t 1))))
          (declare (type (unsigned-byte 60) x))
          (cond ((not (and (eql (the character (fmt-char s i 3 maximum t)) #\~)
                 (eql (the character (fmt-char s i 4 maximum t)) #\[))) (er-hard?-val? 0
                quiet
                'find-alternative-start
                "~@0"
                (illegal-fmt-msg find-alternative-start i s)))
            (t (find-alternative-start1 x s (+f i 5) maximum quiet))))))))

(defun find-alternative-stop
  (s i maximum quiet)
  (declare (type (unsigned-byte 60) i maximum)
    (type string s)
    (xargs :guard (and (<= maximum (length s)) (<= i maximum))
      :measure (nfix (- (1+ maximum) i))
      :ruler-extenders :lambdas))
  (the-fixnat (cond ((and (mbt (and (integerp i) (integerp maximum)))
         (< i (1-f maximum))) (let ((char-s-i (charf s i)))
          (declare (type character char-s-i))
          (case char-s-i
            (#\~ (let ((char-s-1+i (charf s (1+f i))))
                (declare (type character char-s-1+i))
                (case char-s-1+i
                  (#\/ i)
                  (#\[ (let ((k (find-alternative-skip s (+f 2 i) maximum quiet)))
                      (declare (type (unsigned-byte 60) k))
                      (cond ((= k 0) k)
                        (t (find-alternative-stop s k maximum quiet)))))
                  (#\] i)
                  (otherwise (find-alternative-stop s (+f 2 i) maximum quiet)))))
            (otherwise (find-alternative-stop s (+f 1 i) maximum quiet)))))
      (t (er-hard?-val? 0
          quiet
          'find-alternative-stop
          "~@0"
          (illegal-fmt-msg find-alternative-stop s))))))

(defun punctp
  (c)
  (if (member c '(#\. #\, #\: #\; #\? #\! #\) #\]))
    c
    nil))

(defun fmt-tilde-s1
  (s i maximum col channel state)
  (declare (type (unsigned-byte 60) i maximum col)
    (type string s)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (<= (the-fixnat maximum) (length s))
        (open-output-channel-p channel :character state))
      :ruler-extenders :lambdas :measure (cond ((not (and (fmt-state-p state)
             (fixnat-guard i)
             (fixnat-guard maximum)
             (fixnat-guard col)
             (stringp s)
             (<= maximum (length s))
             (open-output-channel-p channel :character state)
             (< i maximum))) 0)
        ((and (> col (fmt-hard-right-margin state))
           (not (write-for-read state))) (+ 2 (nfix (* 2 (- maximum i)))))
        (t (+ 1 (nfix (* 2 (- maximum i))))))))
  (the2s (unsigned-byte 60)
    (cond ((not (mbt (and (fmt-state-p state)
             (fixnat-guard i)
             (fixnat-guard maximum)
             (fixnat-guard col)
             (stringp s)
             (<= maximum (length s))
             (open-output-channel-p channel :character state)))) (mv (nfix col) state))
      ((not (< i maximum)) (mv col state))
      ((and (> col (fmt-hard-right-margin state))
         (not (write-for-read state))) (pprogn (princ$ #\\ channel state)
          (newline channel state)
          (fmt-tilde-s1 s i maximum 0 channel state)))
      (t (let ((c (charf s i)) (fmt-soft-right-margin (fmt-soft-right-margin state)))
          (declare (type character c)
            (type (unsigned-byte 57) fmt-soft-right-margin))
          (cond ((and (> col fmt-soft-right-margin) (eql c #\ )) (pprogn (newline channel state)
                (fmt-tilde-s1 s
                  (the-fixnat (scan-past-whitespace s (+f i 1) maximum))
                  maximum
                  0
                  channel
                  state)))
            ((and (> col fmt-soft-right-margin)
               (or (eql c #\-) (eql c #\_))
               (not (= (1+f i) maximum))) (pprogn (princ$ c channel state)
                (if (eql c #\-)
                  state
                  (princ$ #\- channel state))
                (newline channel state)
                (fmt-tilde-s1 s
                  (the-fixnat (scan-past-whitespace s (+f i 1) maximum))
                  maximum
                  0
                  channel
                  state)))
            (t (pprogn (princ$ c channel state)
                (fmt-tilde-s1 s
                  (1+f i)
                  maximum
                  (cond ((eql c #\
) 0)
                    ((= col (fixnum-bound)) (fixnum-bound))
                    (t (1+f col)))
                  channel
                  state)))))))))

(defun fmt-tilde-cap-s1
  (s i maximum col channel state)
  (declare (type (unsigned-byte 60) i col maximum)
    (type string s)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (<= (the-fixnat maximum) (length s))
        (open-output-channel-p channel :character state))
      :ruler-extenders :lambdas :measure (cond ((not (and (fmt-state-p state)
             (fixnat-guard i)
             (fixnat-guard maximum)
             (fixnat-guard col)
             (stringp s)
             (<= maximum (length s))
             (open-output-channel-p channel :character state)
             (< i maximum))) 0)
        (t (nfix (- maximum i))))))
  (the2s (unsigned-byte 60)
    (cond ((not (mbt (and (fmt-state-p state)
             (fixnat-guard i)
             (fixnat-guard maximum)
             (fixnat-guard col)
             (stringp s)
             (<= maximum (length s))
             (open-output-channel-p channel :character state)))) (mv 0 state))
      ((not (< i maximum)) (mv col state))
      (t (let ((c (charf s i)))
          (declare (type character c))
          (pprogn (princ$ c channel state)
            (fmt-tilde-cap-s1 s
              (1+f i)
              maximum
              (cond ((eql c #\
) 0)
                ((= col (fixnum-bound)) col)
                (t (1+f col)))
              channel
              state)))))))

(defun fmt-var
  (s alist i maximum)
  (declare (type (unsigned-byte 60) i maximum)
    (type string s)
    (xargs :guard (and (<= maximum (length s))
        (< i maximum)
        (character-alistp alist))))
  (let* ((c (the character (fmt-char s i 2 maximum t))) (x (assoc c alist)))
    (declare (type character c))
    (cond (x (cdr x))
      (t (let ((tilde-position (if (eql (charf s i) #\~)
               i
               (1-f i))))
          (er hard?
            'fmt-var
            "~@0"
            (illegal-fmt-msg unbound-tilde-arg tilde-position c alist s)))))))

(defun splat-atom
  (x print-base print-radix indent col channel state)
  (declare (type (unsigned-byte 5) print-base)
    (type (unsigned-byte 60) indent col)
    (type symbol channel)
    (xargs :guard (and (atom x)
        (print-base-p print-base)
        (fmt-state-p state)
        (open-output-channel-p channel :character state))))
  (the2s (unsigned-byte 60)
    (let* ((sz (flsz-atom x print-base print-radix 0 state)) (too-bigp (> (+f! col sz) (fmt-hard-right-margin state))))
      (pprogn (if too-bigp
          (pprogn (newline channel state)
            (spaces indent 0 channel state))
          state)
        (prin1$ x channel state)
        (mv (if too-bigp
            (+f! indent sz)
            (+f! col sz))
          state)))))

(defun splat-atom!
  (x print-base print-radix col channel state)
  (declare (type (unsigned-byte 5) print-base)
    (type (unsigned-byte 60) col)
    (type symbol channel)
    (xargs :guard (and (atom x)
        (print-base-p print-base)
        (open-output-channel-p channel :character state))))
  (the2s (unsigned-byte 60)
    (pprogn (prin1$ x channel state)
      (mv (flsz-atom x print-base print-radix col state) state))))

(defun splat-string
  (x indent col channel state)
  (declare (type string x)
    (type (unsigned-byte 60) indent col)
    (type symbol channel)
    (xargs :guard (and (open-output-channel-p channel :character state)
        (fmt-state-p state))))
  (the2s (unsigned-byte 60)
    (let* ((sz (min (fixnum-bound) (length x))) (too-bigp (> (+f! col sz) (fmt-hard-right-margin state))))
      (declare (type (unsigned-byte 60) sz))
      (pprogn (if too-bigp
          (pprogn (newline channel state)
            (spaces indent 0 channel state))
          state)
        (princ$ x channel state)
        (mv (if too-bigp
            (+f! indent sz)
            (+f! col sz))
          state)))))

(defun number-of-digits
  (n print-base print-radix)
  (declare (type (unsigned-byte 5) print-base)
    (type integer n)
    (xargs :guard (print-base-p print-base)
      :measure (cond ((not (and (integerp n) (print-base-p print-base))) 0)
        ((< n 0) (1+ (- n)))
        (t n))
      :ruler-extenders :lambdas))
  (the-fixnat (cond ((not (mbt (and (integerp n) (print-base-p print-base)))) 0)
      ((< n 0) (+f! 1 (number-of-digits (abs n) print-base print-radix)))
      ((< n print-base) (cond ((null print-radix) 1) ((= print-base 10) 2) (t 3)))
      (t (+f! 1
          (number-of-digits (floor n print-base)
            print-base
            print-radix))))))

(defun left-pad-with-blanks
  (n width col channel state)
  (declare (type integer n)
    (type (integer 0 *) width)
    (type (unsigned-byte 60) col)
    (type symbol channel)
    (xargs :guard (and (open-output-channel-p channel :character state)
        (fmt-state-p state))))
  (the2s (unsigned-byte 60)
    (cond ((> width (fixnum-bound)) (prog2$ (er hard?
            'left-pad-with-blanks
            "It is illegal to supply a padding width of greater than ~x0."
            (fixnum-bound))
          (mv (fixnum-bound) state)))
      (t (let ((d (number-of-digits n (print-base) (print-radix))))
          (declare (type (unsigned-byte 60) d))
          (cond ((>= d width) (pprogn (prin1$ n channel state) (mv (+f! col d) state)))
            (t (pprogn (spaces (-f (the-fixnat width) d) col channel state)
                (prin1$ n channel state)
                (mv (+f! col width) state)))))))))

(defun evisc-tuple
  (print-level print-length alist hiding-cars)
  (list alist print-level print-length hiding-cars))

(defun world-evisceration-alist
  (state alist)
  (declare (xargs :stobjs state))
  (let ((wrld (w state)))
    (cond ((null wrld) alist)
      (t (cons (cons wrld *evisceration-world-mark*) alist)))))

(defun abbrev-evisc-tuple
  (state)
  (declare (xargs :guard t))
  (let ((evisc-tuple (f-get-global 'abbrev-evisc-tuple state)))
    (cond ((eq evisc-tuple :default) (cons (world-evisceration-alist state nil) '(5 7 nil)))
      (t evisc-tuple))))

(defun term-evisc-tuple
  (flg state)
  (let ((evisc-tuple (f-get-global 'term-evisc-tuple state)))
    (cond ((not (eq evisc-tuple :default)) evisc-tuple)
      ((f-get-global 'eviscerate-hide-terms state) (cond (flg '(nil 3 4 (hide))) (t '(nil nil nil (hide)))))
      (flg '(nil 3 4 nil))
      (t nil))))

(defun gag-mode-evisc-tuple
  (state)
  (cond ((gag-mode) (let ((val (f-get-global 'gag-mode-evisc-tuple state)))
        (if (eq val :default)
          nil
          val)))
    (t (term-evisc-tuple nil state))))

(defun ld-evisc-tuple
  (state)
  (let ((evisc-tuple (f-get-global 'ld-evisc-tuple state)))
    (assert$ (not (eq evisc-tuple :default)) evisc-tuple)))

(defun brr-evisc-tuple
  (state)
  (let ((val (f-get-global 'brr-evisc-tuple state)))
    (cond ((eq val :default) (term-evisc-tuple t state))
      (t val))))

(defun fmt-ppr
  (x width rpc col channel state eviscp)
  (declare (type (unsigned-byte 60) width rpc col)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (open-output-channel-p channel :character state))))
  (ppr2 (ppr1 x
      (print-base)
      (print-radix)
      (round-to-small t width)
      (round-to-small t rpc)
      state
      eviscp)
    (round-to-small t col)
    channel
    state
    eviscp))

(defun scan-past-empty-fmt-directives1
  (s alist i maximum clk)
  (declare (type (unsigned-byte 60) i maximum clk)
    (type string s)
    (xargs :ruler-extenders :lambdas :verify-guards nil
      :guard (and (<= maximum (length s)) (character-alistp alist))))
  (the-fixnat (cond ((or (not (mbt (and (natp i)
               (natp maximum)
               (<= maximum (length s))
               (<= maximum (fixnum-bound)))))
         (>= i maximum)
         (zp clk)) (min (fixnum-bound) (nfix i)))
      (t (let ((c (charf s i)))
          (declare (type character c))
          (cond ((eql c #\~) (let ((fmc (the character (fmt-char s i 1 maximum t))))
                (declare (type character fmc))
                (case fmc
                  ((#\s #\S) (cond ((equal (fmt-var s alist i maximum) "") (scan-past-empty-fmt-directives1 s
                          alist
                          (+f! i 3)
                          maximum
                          (1-f clk)))
                      (t i)))
                  (#\@ (let ((val (fmt-var s alist i maximum)))
                      (cond ((not (msgp val)) (er-hard?-val? i
                            nil
                            'scan-past-empty-fmt-directives1
                            "~@0"
                            (illegal-fmt-msg bad-tilde-@-arg i val 'msgp s)))
                        ((equal val "") (scan-past-empty-fmt-directives1 s
                            alist
                            (+f! i 3)
                            maximum
                            (1-f clk)))
                        ((stringp val) i)
                        ((equal (car val) "") (scan-past-empty-fmt-directives1 s
                            alist
                            (+f! i 3)
                            maximum
                            (1-f clk)))
                        (t (let ((len (length (car val))) (alist1 (append (cdr val) alist)))
                            (if (and (<= len (fixnum-bound))
                                (equal (scan-past-empty-fmt-directives1 (car val)
                                    alist1
                                    0
                                    len
                                    (1-f clk))
                                  len))
                              (scan-past-empty-fmt-directives1 s
                                alist
                                (+f! i 3)
                                maximum
                                (1-f clk))
                              i))))))
                  (#\# (let* ((n (find-alternative-start (fmt-var s alist i maximum)
                           s
                           i
                           maximum
                           nil)) (m (if (= n 0)
                            0
                            (find-alternative-stop s n maximum nil)))
                        (o (if (= m 0)
                            0
                            (find-alternative-skip s m maximum nil))))
                      (declare (type (unsigned-byte 60) n)
                        (type (unsigned-byte 60) m o))
                      (cond ((= o 0) 0)
                        ((or (= n m)
                           (= (scan-past-empty-fmt-directives1 s alist n m (1-f clk))
                             m)) (scan-past-empty-fmt-directives1 s
                            alist
                            o
                            maximum
                            (1-f clk)))
                        (t i))))
                  (otherwise i))))
            (t i)))))))

(defun scan-past-empty-fmt-directives
  (s alist i maximum)
  (declare (type (unsigned-byte 60) i maximum)
    (type string s)
    (xargs :guard (and (<= maximum (length s)) (character-alistp alist))))
  (scan-past-empty-fmt-directives1 s
    alist
    i
    maximum
    (fixnum-bound)))

(defun out-of-time-the2s
  (fn state)
  (declare (xargs :stobjs state))
  (the2s (unsigned-byte 60)
    (prog2$ (er hard? fn "Clock ran out in ~x0!" fn)
      (mv 0 state))))

(defun char?
  (s i)
  (declare (xargs :guard (and (stringp s) (natp i))))
  (the character
    (if (and (mbt (natp i)) (< i (length s)))
      (char s i)
      (prog2$ (er hard?
          'char?
          "Unexpected out of bounds index ~x0 for string ~s1!"
          i
          s)
        *null-char*))))

(defun tilde-*-&v-strings
  (flg lst punct)
  (case flg
    (& (case punct
        (#\. (list "" ""~s*"." ""~s*" and " ""~s*", " lst))
        (#\, (list "" ""~s*"," ""~s*" and " ""~s*", " lst))
        (#\: (list "" ""~s*":" ""~s*" and " ""~s*", " lst))
        (#\; (list "" ""~s*";" ""~s*" and " ""~s*", " lst))
        (#\! (list "" ""~s*"!" ""~s*" and " ""~s*", " lst))
        (#\) (list "" ""~s*")" ""~s*" and " ""~s*", " lst))
        (#\? (list "" ""~s*"?" ""~s*" and " ""~s*", " lst))
        (otherwise (list "" ""~s*"" ""~s*" and " ""~s*", " lst))))
    (otherwise (case punct
        (#\. (list "" ""~s*"." ""~s*" or " ""~s*", " lst))
        (#\, (list "" ""~s*"," ""~s*" or " ""~s*", " lst))
        (#\: (list "" ""~s*":" ""~s*" or " ""~s*", " lst))
        (#\; (list "" ""~s*";" ""~s*" or " ""~s*", " lst))
        (#\! (list "" ""~s*"!" ""~s*" or " ""~s*", " lst))
        (#\) (list "" ""~s*")" ""~s*" or " ""~s*", " lst))
        (#\? (list "" ""~s*"?" ""~s*" or " ""~s*", " lst))
        (otherwise (list "" ""~s*"" ""~s*" or " ""~s*", " lst))))))

(defun fmt1
  (str alist col channel state evisc-tuple)
  (declare (type (unsigned-byte 60) col)
    (type string str)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep evisc-tuple))))
  (the2s (unsigned-byte 60)
    (cond ((not (character-alistp alist)) (mv (prog2$ (er hard!
              'fmt0
              "The second argument of any of the FMT family of ~
                      functions must satisfy ~x0, but ~x1 does not."
              'character-alistp
              alist)
            col)
          state))
      (t (mv-let (col state)
          (fmt0 str
            alist
            0
            (min (length str) (fixnum-bound))
            col
            nil
            channel
            state
            evisc-tuple
            (fixnum-bound))
          (declare (type (unsigned-byte 60) col))
          (prog2$ (and (eq channel *standard-co*)
              (maybe-finish-output$ *standard-co* state))
            (mv col state)))))))

(defun fmt
  (str alist channel state evisc-tuple)
  (declare (type string str)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep evisc-tuple))))
  (the2s (unsigned-byte 60)
    (pprogn (newline channel state)
      (fmt1 str alist 0 channel state evisc-tuple))))

(defun fms
  (str alist channel state evisc-tuple)
  (declare (type string str)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep evisc-tuple))))
  (pprogn (newline channel state)
    (mv-let (col state)
      (fmt1 str alist 0 channel state evisc-tuple)
      (declare (ignore col))
      state)))

(defun fmt1!
  (str alist col channel state evisc-tuple)
  (declare (type (unsigned-byte 60) col)
    (type string str)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep evisc-tuple))))
  (the2s (unsigned-byte 60)
    (mv-let (erp col state)
      (state-global-let* ((write-for-read t))
        (mv-let (col state)
          (fmt1 str alist col channel state evisc-tuple)
          (mv nil col state)))
      (declare (ignore erp))
      (mv col state))))

(defun fmt!
  (str alist channel state evisc-tuple)
  (declare (type string str)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep evisc-tuple))))
  (the2s (unsigned-byte 60)
    (mv-let (erp col state)
      (state-global-let* ((write-for-read t))
        (mv-let (col state)
          (fmt str alist channel state evisc-tuple)
          (mv nil col state)))
      (declare (ignore erp))
      (mv col state))))

(defun fms!
  (str alist channel state evisc-tuple)
  (declare (type string str)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep evisc-tuple))))
  (mv-let (erp val state)
    (state-global-let* ((write-for-read t))
      (pprogn (fms str alist channel state evisc-tuple)
        (mv nil nil state)))
    (declare (ignore erp val))
    state))

(defun fmx-cw-msg-1
  (s alist i maximum clk)
  (declare (type (unsigned-byte 60) i maximum clk)
    (type string s)
    (xargs :guard (and (character-alistp alist)
        (< (length s) (fixnum-bound))
        (<= maximum (length s)))
      :guard-hints (("Goal" :in-theory (disable nth)))
      :measure (nfix clk)))
  (fmx-cw-msg-1-body))

(defun fmx-cw-msg
  (str alist)
  (declare (xargs :guard t))
  (cond ((not (stringp str)) (msg "Not a string:~|~x0" str))
    ((not (character-alistp alist)) (msg "Not a character-alistp:~|~x0" alist))
    (t (let ((len (length str)))
        (cond ((not (< len (fixnum-bound))) (msg "String is too long:~|~x0" str))
          (t (fmx-cw-msg-1 str alist 0 (length str) (fixnum-bound))))))))

(defun fmx-cw-fn-guard
  (str alist)
  (declare (xargs :guard t))
  (null (fmx-cw-msg str alist)))

(defun fmx-cw-fn
  (str alist)
  (declare (xargs :guard (fmx-cw-fn-guard str alist)))
  (fmt-to-comment-window str alist 0 nil nil))

(defun fmx!-cw-fn
  (str alist)
  (declare (xargs :guard (fmx-cw-fn-guard str alist)))
  (fmt-to-comment-window! str alist 0 nil nil))

(defun fmt-doc-example1
  (lst i)
  (cond ((null lst) nil)
    (t (cons (cons "~c0 (~n1)~tc~y2~|"
          (list (cons #\0 (cons i 5))
            (cons #\1 (list i))
            (cons #\2 (car lst))))
        (fmt-doc-example1 (cdr lst) (1+ i))))))

(defun fmt-doc-example
  (x state)
  (fmt "Here is a true list:  ~x0.  It has ~#1~[no elements~/a single ~
        element~/~n2 elements~], ~@3~%~%We could print each element in square ~
        brackets:~%(~*4).  And if we wished to itemize them into column 15 we ~
        could do it like this~%0123456789012345~%~*5End of example."
    (list (cons #\0 x)
      (cons #\1 (cond ((null x) 0) ((null (cdr x)) 1) (t 2)))
      (cons #\2 (length x))
      (cons #\3
        (cond ((< (length x) 3) "and so we can't print the third one!")
          (t (cons "the third of which is ~x0."
              (list (cons #\0 (caddr x)))))))
      (cons #\4
        (list "[empty]"
          "[the end: ~y*]"
          "[almost there: ~y*], "
          "[~y*], "
          x))
      (cons #\5
        (list* ""
          "~@*"
          "~@*"
          "~@*"
          (fmt-doc-example1 x 0)
          (list (cons #\c 15)))))
    *standard-co*
    state
    nil))

(defun fmt-abbrev1
  (str alist col channel state suffix-msg)
  (declare (type string str)
    (type (unsigned-byte 60) col)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep (abbrev-evisc-tuple state)))))
  (the2s (unsigned-byte 60)
    (pprogn (f-put-global 'evisc-hitp-without-iprint nil state)
      (mv-let (col state)
        (fmt1 str
          alist
          col
          channel
          state
          (abbrev-evisc-tuple state))
        (fmt1 "~@0~@1"
          (list (cons #\0
              (cond ((f-get-global 'evisc-hitp-without-iprint state) (assert$? (not (iprint-enabledp state))
                    *see-doc-set-iprint*))
                (t "")))
            (cons #\1 suffix-msg))
          col
          channel
          state
          nil)))))

(defun fmt-abbrev
  (str alist col channel state suffix-msg)
  (declare (type string str)
    (type (unsigned-byte 60) col)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep (abbrev-evisc-tuple state)))))
  (mv-let (col state)
    (fmt-abbrev1 str alist col channel state suffix-msg)
    (declare (ignore col))
    state))

(defun fmt-ctx
  (ctx col channel state)
  (declare (type (unsigned-byte 60) col)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep (abbrev-evisc-tuple state)))))
  (the2s (unsigned-byte 60)
    (cond ((null ctx) (mv col state))
      ((symbolp ctx) (fmt1 "~x0" (list (cons #\0 ctx)) col channel state nil))
      ((and (consp ctx) (symbolp (car ctx))) (fmt1 "(~@0~x1 ~x2 ...)"
          (list (cons #\0
              (if (member-eq (car ctx) *fmt-ctx-spacers*)
                " "
                ""))
            (cons #\1 (car ctx))
            (cons #\2 (cdr ctx)))
          col
          channel
          state
          nil))
      (t (fmt-abbrev1 "~@0"
          (list (cons #\0 ctx))
          col
          channel
          state
          "")))))

(defun fmt-in-ctx
  (ctx col channel state)
  (declare (type (unsigned-byte 60) col)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep (abbrev-evisc-tuple state)))))
  (the2s (unsigned-byte 60)
    (cond ((null ctx) (fmt1 ":  " nil col channel state nil))
      (t (mv-let (col state)
          (fmt1 " in " nil col channel state nil)
          (mv-let (col state)
            (fmt-ctx ctx col channel state)
            (fmt1 ":  " nil col channel state nil)))))))

(defun er-off-p1
  (summary wrld)
  (declare (xargs :guard (and (or (null summary) (stringp summary))
        (plist-worldp wrld)
        (string-alistp (table-alist 'inhibit-er-table wrld)))))
  (and summary
    (assoc-string-equal summary
      (table-alist 'inhibit-er-table wrld))))

(defun er-off-p
  (summary state)
  (declare (xargs :stobjs state
      :guard (and (or (null summary) (stringp summary))
        (string-alistp (table-alist 'inhibit-er-table (w state))))))
  (er-off-p1 summary (w state)))

(defun error-fms-channel
  (hardp ctx summary str alist channel state newlines)
  (declare (type string str)
    (type symbol channel)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (open-output-channel-p channel :character state)
        (standard-evisc-tuplep (abbrev-evisc-tuple state))
        (or (null summary) (stringp summary))
        (string-alistp (table-alist 'inhibit-er-table (w state))))))
  (cond ((er-off-p summary state) state)
    (t (flet ((newlines (n channel state)
           (case n
             (0 state)
             (1 (newline channel state))
             (2 (pprogn (newline channel state) (newline channel state)))
             (t (prog2$ (er hard?
                   'error-fms-channel
                   "Error: The NEWLINES argument of ~
                                            error-fms-channel must be 0, 1, ~
                                            or 2, hence ~x0 is illegal."
                   n)
                 state)))))
        (with-output-lock (pprogn (newlines newlines channel state)
            (mv-let (col state)
              (fmt1 (if hardp
                  "HARD ACL2 ERROR~#0~[~/ [~s1]~]"
                  "ACL2 Error~#0~[~/ [~s1]~]")
                (list (cons #\0
                    (if summary
                      1
                      0))
                  (cons #\1 summary))
                0
                channel
                state
                nil)
              (mv-let (col state)
                (fmt-in-ctx ctx col channel state)
                (fmt-abbrev str alist col channel state "")))
            (newlines newlines channel state)))))))

(defun standard-co
  (state)
  (declare (xargs :guard t))
  (f-get-global 'standard-co state))

(defun error-fms
  (hardp ctx summary str alist state)
  (declare (type string str)
    (xargs :guard (and (fmt-state-p state)
        (character-alistp alist)
        (standard-evisc-tuplep (abbrev-evisc-tuple state))
        (or (null summary) (stringp summary))
        (string-alistp (table-alist 'inhibit-er-table (w state)))
        (symbolp (standard-co state))
        (open-output-channel-p (standard-co state) :character state))))
  (let ((chan (f-get-global 'standard-co state)))
    (error-fms-channel hardp ctx summary str alist chan state 2)))

(defun push-warning-frame (state) state)

(defun absorb-frame
  (lst stk)
  (if (consp stk)
    (cons (union-equal lst (car stk)) (cdr stk))
    stk))

(defun pop-warning-frame
  (accum-p state)
  (declare (ignore accum-p))
  (mv-let (erp val state)
    (read-acl2-oracle state)
    (declare (ignore erp))
    (mv val state)))

(defun push-warning
  (summary state)
  (declare (ignore summary))
  state)

(defun record-maker-function-name
  (name)
  (intern-in-package-of-symbol (coerce (append (coerce "Make " 'list)
        (coerce (symbol-name name) 'list)
        (coerce " record" 'list))
      'string)
    name))

(defun record-changer-function-name
  (name)
  (intern-in-package-of-symbol (coerce (append (coerce "Change " 'list)
        (coerce (symbol-name name) 'list)
        (coerce " record fields" 'list))
      'string)
    name))

(defun make-record-car-cdrs1
  (lst var)
  (cond ((null lst) var)
    (t (list (car lst) (make-record-car-cdrs1 (cdr lst) var)))))

(defun make-record-car-cdrs
  (field-layout car-cdr-lst)
  (cond ((atom field-layout) (cond ((null field-layout) nil)
        (t (list (make-record-car-cdrs1 car-cdr-lst field-layout)))))
    (t (append (make-record-car-cdrs (car field-layout)
          (cons 'car car-cdr-lst))
        (make-record-car-cdrs (cdr field-layout)
          (cons 'cdr car-cdr-lst))))))

(defun make-record-accessors
  (name field-lst car-cdrs cheap)
  (cond ((null field-lst) nil)
    (t (cons (cond (cheap (list 'defabbrev
              (record-accessor-function-name name (car field-lst))
              (list (car field-lst))
              (car car-cdrs)))
          (t (list 'defabbrev
              (record-accessor-function-name name (car field-lst))
              (list (car field-lst))
              (sublis (list (cons 'name name)
                  (cons 'x (car field-lst))
                  (cons 'z (car car-cdrs)))
                '(prog2$ (or (and (consp x) (eq (car x) 'name))
                    (record-error 'name x))
                  z)))))
        (make-record-accessors name
          (cdr field-lst)
          (cdr car-cdrs)
          cheap)))))

(defun symbol-name-tree-occur
  (sym sym-tree)
  (cond ((symbolp sym-tree) (cond ((equal (symbol-name sym) (symbol-name sym-tree)) sym-tree)
        (t nil)))
    ((atom sym-tree) nil)
    (t (or (symbol-name-tree-occur sym (car sym-tree))
        (symbol-name-tree-occur sym (cdr sym-tree))))))

(defun some-symbol-name-tree-occur
  (syms sym-tree)
  (cond ((null syms) nil)
    ((symbol-name-tree-occur (car syms) sym-tree) t)
    (t (some-symbol-name-tree-occur (cdr syms) sym-tree))))

(defun make-record-changer-cons
  (fields field-layout x)
  (cond ((not (some-symbol-name-tree-occur fields field-layout)) x)
    ((atom field-layout) field-layout)
    (t (list 'cons
        (make-record-changer-cons fields
          (car field-layout)
          (list 'car x))
        (make-record-changer-cons fields
          (cdr field-layout)
          (list 'cdr x))))))

(defun make-record-changer-let-bindings
  (field-layout lst)
  (cond ((null lst) nil)
    (t (let ((var (symbol-name-tree-occur (car lst) field-layout)))
        (cond ((null var) (er hard
              'record-error
              "A make or change form has used ~x0 as though ~
                         it were a legal field specifier in a record ~
                         with the layout ~x1."
              (car lst)
              field-layout))
          (t (cons (list var (cadr lst))
              (make-record-changer-let-bindings field-layout (cddr lst)))))))))

(defun make-record-changer-let
  (name field-layout cheap rec lst)
  (cond (cheap (list 'let
        (cons (list 'record-changer-not-to-be-used-elsewhere rec)
          (make-record-changer-let-bindings field-layout lst))
        (make-record-changer-cons (evens lst)
          field-layout
          'record-changer-not-to-be-used-elsewhere)))
    (t (list 'let
        (cons (list 'record-changer-not-to-be-used-elsewhere rec)
          (make-record-changer-let-bindings field-layout lst))
        (sublis (list (cons 'name name)
            (cons 'cons-nest
              (make-record-changer-cons (evens lst)
                field-layout
                '(cdr record-changer-not-to-be-used-elsewhere))))
          '(prog2$ (or (and (consp record-changer-not-to-be-used-elsewhere)
                (eq (car record-changer-not-to-be-used-elsewhere) 'name))
              (record-error 'name record-changer-not-to-be-used-elsewhere))
            (cons 'name cons-nest)))))))

(defun make-record-changer
  (name field-layout cheap)
  (list 'defmacro
    (record-changer-function-name name)
    '(&rest args)
    (list 'make-record-changer-let
      (kwote name)
      (kwote field-layout)
      cheap
      '(car args)
      '(cdr args))))

(defun make-record-maker-cons
  (fields field-layout)
  (cond ((atom field-layout) (cond ((some-symbol-name-tree-occur fields field-layout) field-layout)
        (t nil)))
    (t (list 'cons
        (make-record-maker-cons fields (car field-layout))
        (make-record-maker-cons fields (cdr field-layout))))))

(defun make-record-maker-let
  (name field-layout cheap lst)
  (cond (cheap (list 'let
        (make-record-changer-let-bindings field-layout lst)
        (make-record-maker-cons (evens lst) field-layout)))
    (t (list 'let
        (make-record-changer-let-bindings field-layout lst)
        (list 'cons
          (kwote name)
          (make-record-maker-cons (evens lst) field-layout))))))

(defun make-record-maker
  (name field-layout cheap)
  (list 'defmacro
    (record-maker-function-name name)
    '(&rest args)
    (list 'make-record-maker-let
      (kwote name)
      (kwote field-layout)
      cheap
      'args)))

(defun make-record-field-lst
  (field-layout)
  (cond ((atom field-layout) (cond ((null field-layout) nil) (t (list field-layout))))
    (t (append (make-record-field-lst (car field-layout))
        (make-record-field-lst (cdr field-layout))))))

(defun record-maker-recognizer-name
  (name)
  (declare (xargs :guard (symbolp name)))
  (intern-in-package-of-symbol (concatenate 'string "WEAK-" (symbol-name name) "-P")
    name))

(defun make-record-recognizer-body
  (field-layout)
  (declare (xargs :guard t))
  (cond ((consp field-layout) (cond ((consp (car field-layout)) (cond ((consp (cdr field-layout)) `(and (consp x)
                (let ((x (car x)))
                  ,(MAKE-RECORD-RECOGNIZER-BODY (CAR FIELD-LAYOUT)))
                (let ((x (cdr x)))
                  ,(MAKE-RECORD-RECOGNIZER-BODY (CDR FIELD-LAYOUT)))))
            (t `(and (consp x)
                (let ((x (car x)))
                  ,(MAKE-RECORD-RECOGNIZER-BODY (CAR FIELD-LAYOUT)))))))
        ((consp (cdr field-layout)) `(and (consp x)
            (let ((x (cdr x)))
              ,(MAKE-RECORD-RECOGNIZER-BODY (CDR FIELD-LAYOUT)))))
        (t '(consp x))))
    (t t)))

(defun make-record-recognizer
  (name field-layout cheap recog-name)
  `(defun ,RECOG-NAME
    (x)
    (declare (xargs :mode :logic :guard t)
      ,@(AND CHEAP (SYMBOLP FIELD-LAYOUT) `((IGNORE X))))
    ,(COND (CHEAP (MAKE-RECORD-RECOGNIZER-BODY FIELD-LAYOUT))
       (T
        `(AND (CONSP X) (EQ (CAR X) ',NAME)
              ,@(AND (CONSP FIELD-LAYOUT)
                     `((LET ((X (CDR X)))
                         ,(MAKE-RECORD-RECOGNIZER-BODY FIELD-LAYOUT)))))))))

(defun record-macros
  (name field-layout cheap recog-name)
  (declare (xargs :guard (or recog-name (symbolp name))))
  (let ((recog-name (or recog-name (record-maker-recognizer-name name))))
    (cons 'progn
      (append (make-record-accessors name
          (make-record-field-lst field-layout)
          (make-record-car-cdrs field-layout
            (if cheap
              nil
              '(cdr)))
          cheap)
        (list (make-record-changer name field-layout cheap)
          (make-record-maker name field-layout cheap)
          (make-record-recognizer name field-layout cheap recog-name))))))

(defun io?-nil-output
  (lst default-bindings)
  (cond ((null lst) nil)
    (t (cons (cond ((eq (car lst) 'state) 'state)
          ((cadr (assoc-eq (car lst) default-bindings)))
          (t nil))
        (io?-nil-output (cdr lst) default-bindings)))))

(defun formal-bindings
  (vars)
  (if (endp vars)
    nil
    (cons (list 'list
        (list 'quote (car vars))
        (list 'list ''quote (car vars)))
      (formal-bindings (cdr vars)))))

(defun push-io-record
  (io-marker form state)
  (declare (xargs :guard t))
  (f-put-global 'saved-output-reversed
    (cons (make io-record :io-marker io-marker :form form)
      (f-get-global 'saved-output-reversed state))
    state))

(defun saved-output-token-p
  (token state)
  (declare (xargs :stobjs state
      :guard (and (symbolp token)
        (or (eq (f-get-global 'saved-output-token-lst state) :all)
          (true-listp (f-get-global 'saved-output-token-lst state))))))
  (and (f-get-global 'saved-output-p state)
    (or (eq (f-get-global 'saved-output-token-lst state) :all)
      (member-eq token
        (f-get-global 'saved-output-token-lst state)))))

(defun io?-wormhole-bindings
  (i vars)
  (declare (xargs :guard (and (true-listp vars) (natp i))))
  (cond ((endp vars) nil)
    (t (cons (list (car vars) `(nth ,I (@ wormhole-input)))
        (io?-wormhole-bindings (1+ i) (cdr vars))))))

(defun output-ignored-p
  (token state)
  (member-eq token (f-get-global 'inhibit-output-lst state)))

(defun error1-state-p
  (state)
  (declare (xargs :stobjs state))
  (and (fmt-state-p state)
    (let ((e (f-get-global 'abbrev-evisc-tuple state)))
      (or (eq e :default) (standard-evisc-tuplep e)))
    (string-alistp (table-alist 'inhibit-er-table (w state)))
    (symbolp (standard-co state))
    (open-output-channel-p (standard-co state) :character state)
    (open-output-channel-p *standard-co* :character state)
    (true-listp (f-get-global 'inhibit-output-lst state))
    (stringp (f-get-global 'window-interface-prelude state))
    (stringp (f-get-global 'window-interface-postlude state))
    (or (eq (f-get-global 'saved-output-token-lst state) :all)
      (true-listp (f-get-global 'saved-output-token-lst state)))))

(defun state-p+
  (state)
  (declare (xargs :stobjs state))
  (error1-state-p state))

(defun error1
  (ctx summary str alist state)
  (declare (type string str)
    (xargs :guard (and (error1-state-p state)
        (character-alistp alist)
        (or (null summary) (stringp summary)))))
  (pprogn (io? error
      nil
      state
      (alist str ctx summary)
      (error-fms nil ctx summary str alist state))
    (mv t nil state)))

(defun error1-safe
  (ctx str alist state)
  (declare (type string str)
    (xargs :guard (and (error1-state-p state) (character-alistp alist))))
  (pprogn (io? error
      nil
      state
      (alist str ctx)
      (error-fms nil ctx nil str alist state))
    (mv nil nil state)))

(defun set-inhibited-summary-types-fn
  (lst state)
  (declare (xargs :stobjs state :mode :program))
  (let ((msg (chk-inhibited-summary-types 'set-inhibited-summary-types
         lst)))
    (cond (msg (er soft 'set-inhibited-summary-types "~@0" msg))
      (t (pprogn (f-put-global 'inhibited-summary-types lst state)
          (value lst))))))

(defun warning-off-p1
  (summary wrld ld-skip-proofsp)
  (declare (xargs :guard (and (or (null summary) (stringp summary))
        (plist-worldp wrld)
        (string-alistp (table-alist 'inhibit-warnings-table wrld)))))
  (or (and summary
      (assoc-string-equal summary
        (table-alist 'inhibit-warnings-table wrld)))
    (and (or (eq ld-skip-proofsp 'include-book)
        (eq ld-skip-proofsp 'include-book-with-locals)
        (eq ld-skip-proofsp 'initialize-acl2))
      (not (and summary
          (member-string-equal summary
            *uninhibited-warning-summaries*))))))

(defun warning-off-p
  (summary state)
  (warning-off-p1 summary (w state) (ld-skip-proofsp state)))

(defun set-warnings-as-errors-alist
  (strings flg alist uninhibited-warning-summaries)
  (cond ((endp strings) alist)
    ((member-string-equal (car strings)
       uninhibited-warning-summaries) (er hard
        'set-warnings-as-errors
        "It is illegal to specify that warnings of type ~x0 are to be ~
              converted to errors, because ~x0 is a member (up to case) of ~x1"
        (car strings)
        '*uninhibited-warning-summaries*))
    (t (set-warnings-as-errors-alist (cdr strings)
        flg
        (let ((pair (assoc-string-equal (car strings) alist)))
          (cond ((and (consp pair) (eq (cdr pair) flg)) alist)
            ((null pair) (acons (car strings) flg alist))
            (t (acons (car strings)
                flg
                (remove1-assoc-string-equal (car strings) alist)))))
        uninhibited-warning-summaries))))

(defun set-warnings-as-errors
  (flg strings state)
  (declare (xargs :guard (member-eq flg '(t nil :always))))
  (cond ((eq strings :all) (f-put-global 'warnings-as-errors
        (make warnings-as-errors :default flg :alist nil)
        state))
    ((string-listp strings) (let* ((old (f-get-global 'warnings-as-errors state)) (default (warnings-as-errors-default old))
          (alist (warnings-as-errors-alist old)))
        (cond ((and (eq flg default)
             (null (assoc-string-equal (car strings) alist))) state)
          (t (f-put-global 'warnings-as-errors
              (if old
                (change warnings-as-errors
                  old
                  :alist (set-warnings-as-errors-alist strings
                    flg
                    alist
                    *uninhibited-warning-summaries*))
                (make warnings-as-errors
                  :default nil
                  :alist (set-warnings-as-errors-alist strings
                    flg
                    alist
                    *uninhibited-warning-summaries*)))
              state)))))
    (t (prog2$ (er hard
          'set-warnings-as-errors
          "Illegal second argument of ~x0, ~x1: must be :ALL or a ~
                   list of strings."
          'set-warnings-as-errors
          strings)
        state))))

(defun warning1-body
  (ctx summary str+ alist state)
  (let ((channel (f-get-global 'proofs-co state)))
    (pprogn (if summary
        (push-warning summary state)
        state)
      (cond ((f-get-global 'raw-warning-format state) (cond ((consp str+) (fms "~y0"
                (list (cons #\0
                    (list :warning summary (cons (list :ctx ctx) (cdr str+)))))
                channel
                state
                nil))
            (t (fms "(:WARNING ~x0~t1~y2)~%"
                (list (cons #\0 summary)
                  (cons #\1 10)
                  (cons #\2
                    (list (cons :ctx ctx)
                      (cons :fmt-string str+)
                      (cons :fmt-alist alist))))
                channel
                state
                nil))))
        (t (let ((str (cond ((consp str+) (assert$ (and (stringp (car str+)) (alistp (cdr str+)))
                     (car str+)))
                 (t str+))))
            (mv-let (col state)
              (fmt "ACL2 Warning~#0~[~/ [~s1]~]"
                (list (cons #\0
                    (if summary
                      1
                      0))
                  (cons #\1 summary))
                channel
                state
                nil)
              (mv-let (col state)
                (fmt-in-ctx ctx col channel state)
                (fmt-abbrev str alist col channel state "~%~%")))))))))

(defun warnings-as-errors-val-guard
  (summary warnings-as-errors)
  (declare (xargs :guard t))
  (and (or (null summary) (stringp summary))
    (or (null warnings-as-errors)
      (and (weak-warnings-as-errors-p warnings-as-errors)
        (string-alistp (warnings-as-errors-alist warnings-as-errors))))))

(defun warnings-as-errors-val
  (summary warnings-as-errors)
  (declare (xargs :guard (warnings-as-errors-val-guard summary warnings-as-errors)))
  (let* ((pair (and summary
         (assoc-string-equal summary
           (warnings-as-errors-alist warnings-as-errors)))) (erp (if pair
          (cdr pair)
          (warnings-as-errors-default warnings-as-errors))))
    (if (booleanp erp)
      erp
      :always)))

(defun warning1
  (ctx summary str alist state)
  (warning1-form nil))

(defun observation1
  (ctx str alist abbrev-p state)
  (observation1-body nil))

(defun observation1-cw
  (ctx str alist abbrev-p)
  (observation1-body t))

(defun packn1
  (lst)
  (declare (xargs :guard (atom-listp lst)))
  (cond ((endp lst) nil)
    (t (append (explode-atom (car lst) 10) (packn1 (cdr lst))))))

(defun packn-pos
  (lst witness)
  (declare (xargs :guard (and (atom-listp lst) (symbolp witness))))
  (intern-in-package-of-symbol (coerce (packn1 lst) 'string)
    witness))

(defun find-first-non-cl-symbol
  (lst)
  (declare (xargs :guard (atom-listp lst)))
  (cond ((endp lst) nil)
    ((and (symbolp (car lst))
       (not (equal (symbol-package-name (car lst)) "COMMON-LISP"))) (car lst))
    (t (find-first-non-cl-symbol (cdr lst)))))

(defun packn
  (lst)
  (declare (xargs :guard (atom-listp lst)))
  (packn-pos lst (or (find-first-non-cl-symbol lst) 'packn)))

(defun pack2 (n1 n2) (packn (list n1 n2)))

(defun defstobj-fnname-key2
  (type)
  (declare (xargs :guard t))
  (if (consp type)
    (case (car type)
      (array :array)
      (hash-table :hash-table)
      (stobj-table :stobj-table)
      (t :scalar))
    :scalar))

(defun doublet-listp
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) (equal x nil))
    (t (and (true-listp (car x))
        (eql (length (car x)) 2)
        (doublet-listp (cdr x))))))

(defun defstobj-fnname
  (root key1 key2 renaming-alist)
  (declare (xargs :guard (and (symbolp root)
        (member-eq key1
          '(:recognizer :length :resize :accessor :updater :creator :boundp :accessor? :remove :count :clear :init))
        (symbolp key2)
        (doublet-listp renaming-alist))))
  (let* ((default-fnname (case key1
         (:recognizer (packn-pos (list root "P") root))
         (:length (and (eq key2 :array)
             (packn-pos (list root "-LENGTH") root)))
         (:resize (and (eq key2 :array)
             (packn-pos (list "RESIZE-" root) root)))
         (:accessor (case key2
             (:array (packn-pos (list root "I") root))
             ((:hash-table :stobj-table) (packn-pos (list root "-GET") root))
             (otherwise root)))
         (:updater (case key2
             (:array (packn-pos (list "UPDATE-" root "I") root))
             ((:hash-table :stobj-table) (packn-pos (list root "-PUT") root))
             (otherwise (packn-pos (list "UPDATE-" root) root))))
         (:creator (packn-pos (list "CREATE-" root) root))
         (:boundp (and (or (eq key2 :hash-table) (eq key2 :stobj-table))
             (packn-pos (list root "-BOUNDP") root)))
         (:accessor? (and (eq key2 :hash-table)
             (packn-pos (list root "-GET?") root)))
         (:remove (and (or (eq key2 :hash-table) (eq key2 :stobj-table))
             (packn-pos (list root "-REM") root)))
         (:count (and (or (eq key2 :hash-table) (eq key2 :stobj-table))
             (packn-pos (list root "-COUNT") root)))
         (:clear (and (or (eq key2 :hash-table) (eq key2 :stobj-table))
             (packn-pos (list root "-CLEAR") root)))
         (:init (and (or (eq key2 :hash-table) (eq key2 :stobj-table))
             (packn-pos (list root "-INIT") root)))
         (otherwise (er hard
             'defstobj-fnname
             "Implementation error (bad case); please contact the ACL2 ~
                   implementors.")))) (temp (and default-fnname
          (assoc-eq default-fnname renaming-alist))))
    (if temp
      (cadr temp)
      default-fnname)))