acl2-fns

(defun global-symbol
  (x)
  (or (get x *global-symbol-key*)
    (setf (get x *global-symbol-key*)
      (intern (symbol-name x)
        (find-package-fast (concatenate 'string
            *global-package-prefix*
            (symbol-package-name x)))))))

(defun macroexpand-till
  (form sym)
  (loop (cond ((and (consp form) (eq (car form) sym)) (return form))
      (t (multiple-value-bind (new-form flg)
          (macroexpand-1 form)
          (cond ((null flg) (return form)) (t (setq form new-form))))))))

(defun get-type-from-dcls
  (var dcls)
  (cond ((endp dcls) t)
    ((and (consp (car dcls))
       (eq 'type (caar dcls))
       (member var (cddr (car dcls)))) (cadr (car dcls)))
    (t (get-type-from-dcls var (cdr dcls)))))

(defun arg-declarations
  (formals dcls)
  (cond ((endp formals) nil)
    (t (cons (get-type-from-dcls (car formals) dcls)
        (arg-declarations (cdr formals) dcls)))))

(defun collect-types
  (l)
  (cond ((null (cdr l)) nil)
    ((stringp (car l)) (collect-types (cdr l)))
    ((consp (car l)) (let ((exp (car l)))
        (cond ((and (consp exp) (eq (car exp) 'declare)) (append (cdr exp) (collect-types (cdr l))))
          (t nil))))
    (t nil)))

(defun convert-type-to-integer-pair
  (typ)
  (case (car typ)
    (integer (cdr typ))
    (signed-byte (let ((n (expt 2 (1- (cadr typ)))))
        (list (- n) (1- n))))
    (unsigned-byte (list 0 (1- (expt 2 (cadr typ)))))
    (t (error "Unexpected type for convert-to-integer-type ~s" typ))))

(defun min-integer-*
  (x y)
  (cond ((and (integerp x) (integerp y)) (min x y)) (t '*)))

(defun max-integer-*
  (x y)
  (cond ((and (integerp x) (integerp y)) (max x y)) (t '*)))

(defun max-output-type-for-declare-form
  (type1 type2)
  (cond ((equal type1 type2) type1)
    ((or (eq type1 '*) (eq type2 '*)) '*)
    ((not (equal (and (consp type1) (eq (car type1) 'values))
         (and (consp type2) (eq (car type2) 'values)))) '*)
    ((and (or (eq type1 'integer)
         (and (consp type1)
           (eq (car type1) 'integer)
           (or (null (cddr type1)) (member '* (cdr type1) :test 'eq))))
       (or (eq type2 'integer)
         (and (consp type2)
           (eq (car type2) 'integer)
           (or (null (cddr type2)) (member '* (cdr type2) :test 'eq))))) 'integer)
    ((or (atom type1) (atom type2)) t)
    ((cdr (last type1)) (error "Non-atom, non-true-listp type for max-output-type-for-declare-form: ~s"
        type1))
    ((cdr (last type2)) (error "Non-atom, non-true-listp type for max-output-type-for-declare-form: ~s"
        type2))
    (t (let ((sym1 (car type1)) (sym2 (car type2)))
        (cond ((eq sym1 sym2) (case sym1
              ((signed-byte unsigned-byte) (if (< (cadr type1) (cadr type2))
                  type2
                  type1))
              (integer (list 'integer
                  (min-integer-* (cadr type1) (cadr type2))
                  (max-integer-* (caddr type1) (caddr type2))))
              (values (cons 'values
                  (max-output-type-for-declare-form-lst (cdr type1)
                    (cdr type2))))
              (otherwise (error "Unexpected type for max-output-type-for-declare-form: ~s"
                  type1))))
          ((or (eq sym1 'values) (eq sym2 'values)) '*)
          (t (let* ((pair1 (convert-type-to-integer-pair type1)) (pair2 (convert-type-to-integer-pair type2))
                (lower1 (car pair1))
                (upper1 (cadr pair1))
                (lower2 (car pair2))
                (upper2 (cadr pair2))
                (lower-min (min-integer-* lower1 lower2))
                (upper-max (max-integer-* upper1 upper2)))
              (cond ((and (eql lower1 lower-min) (eql upper1 upper-max)) type1)
                ((and (eql lower2 lower-min) (eql upper2 upper-max)) type2)
                (t (list 'integer lower-min upper-max))))))))))

(defun max-output-type-for-declare-form-lst
  (type-list1 type-list2)
  (cond ((or (null type-list1) (null type-list2)) (cond ((and (null type-list1) (null type-list2)) nil)
        ((and *acl2-output-type-abort*
           (or (atom type-list1) (atom type-list2))) (cons '*
            (max-output-type-for-declare-form-lst (cdr type-list1)
              (cdr type-list2))))
        (t (error "Implementation error:~%~
                   max-output-type-for-declare-form-lst called on lists of~%~
                   different length:~%~
                   ~s~%  ~s~%~
                   Please contact the ACL2 implementors."
            type-list1
            type-list2))))
    (t (cons (max-output-type-for-declare-form (car type-list1)
          (car type-list2))
        (max-output-type-for-declare-form-lst (cdr type-list1)
          (cdr type-list2))))))

(defun output-type-for-declare-form-rec
  (form flet-alist)
  (cond ((integerp form) `(integer ,FORM ,FORM))
    ((characterp form) 'character)
    ((atom form) t)
    ((and (eq (car form) 'quote) (consp (cdr form))) (cond ((integerp (cadr form)) `(integerp ,(CADR FORM) ,(CADR FORM)))
        ((rationalp (cadr form)) `rational)
        ((numberp (cadr form)) 'number)
        ((characterp (cadr form)) 'character)
        ((null (cadr form)) 'null)
        ((symbolp (cadr form)) 'symbol)
        ((stringp (cadr form)) 'string)
        ((consp (cadr form)) 'cons)
        (t t)))
    ((and (eq (car form) 'setq) (equal (length form) 3)) (let ((x (output-type-for-declare-form-rec (car (last form))
             flet-alist)))
        (cond (*acl2-output-type-abort* '*)
          ((and (consp x) (eq (car x) 'values)) (cadr x))
          ((eq x '*) t)
          (t x))))
    ((and (eq (car form) 'setf) (equal (length form) 3)) (output-type-for-declare-form-rec (car (last form))
        flet-alist))
    ((eq (car form) 'return-last) (cond ((equal (cadr form) ''mbe1-raw) (output-type-for-declare-form-rec (caddr form) flet-alist))
        ((and (equal (cadr form) ''progn)
           (consp (caddr form))
           (eq (car (caddr form)) 'throw-nonexec-error)) (setq *acl2-output-type-abort* '*))
        (t (output-type-for-declare-form-rec (car (last form))
            flet-alist))))
    ((eq (car form) 'macrolet) (setq *acl2-output-type-abort* '*))
    ((eq (car form) 'return-from) (output-type-for-declare-form-rec (car (last form))
        flet-alist))
    ((eq (car form) 'when) (let ((tmp (output-type-for-declare-form-rec (car (last form))
             flet-alist)))
        (cond (*acl2-output-type-abort* '*)
          ((or (atom tmp) (not (eq (car tmp) 'values))) t)
          (t '*))))
    ((assoc (car form) flet-alist :test 'eq) (cdr (assoc (car form) flet-alist :test 'eq)))
    ((member (car form) '(values mv swap-stobjs) :test 'eq) (cond ((null (cdr form)) (setq *acl2-output-type-abort* '*))
        ((null (cddr form)) (let* ((*acl2-output-type-abort* nil) (tmp (output-type-for-declare-form-rec (cadr form) flet-alist)))
            (cond ((and (symbolp tmp)
                 (not (eq tmp '*))
                 (not *acl2-output-type-abort*)) tmp)
              (t t))))
        (t (cons 'values
            (loop for
              x
              in
              (cdr form)
              collect
              (let* ((*acl2-output-type-abort* nil) (tmp (output-type-for-declare-form-rec x flet-alist)))
                (cond ((and (symbolp tmp)
                     (not (eq tmp '*))
                     (not *acl2-output-type-abort*)) tmp)
                  (t t))))))))
    ((member (car form) '(flet labels) :test 'eq) (let ((temp flet-alist))
        (dolist (binding (cadr form))
          (let ((fn (car binding)) (body (car (last binding)))
              *acl2-output-type-abort*)
            (let ((typ (output-type-for-declare-form-rec body flet-alist)))
              (push (cons fn
                  (if *acl2-output-type-abort*
                    '*
                    typ))
                temp))))
        (output-type-for-declare-form-rec (car (last form)) temp)))
    ((eq (car form) 'the) (let ((typ (cadr form)))
        (cond ((member typ '(integer fixnum character) :test 'eq) typ)
          ((and (consp typ)
             (member (car typ)
               '(integer signed-byte unsigned-byte values)
               :test 'eq)) typ)
          (t t))))
    ((eq (car form) 'if) (cond ((eq (cadr form) t) (output-type-for-declare-form-rec (caddr form) flet-alist))
        ((eq (cadr form) nil) (output-type-for-declare-form-rec (cadddr form) flet-alist))
        (t (let ((type1 (output-type-for-declare-form-rec (caddr form) flet-alist)))
            (if (eq type1 '*)
              '*
              (max-output-type-for-declare-form type1
                (output-type-for-declare-form-rec (cadddr form) flet-alist)))))))
    ((member (car form) '(let let*) :test 'eq) (cond ((cddr form) (output-type-for-declare-form-rec (car (last form))
            flet-alist))
        (t t)))
    ((eq (car form) 'multiple-value-bind) (cond ((cdddr form) (output-type-for-declare-form-rec (car (last form))
            flet-alist))
        (t t)))
    ((eq (car form) 'unwind-protect) (output-type-for-declare-form-rec (cadr form) flet-alist))
    ((eq (car form) 'ec-call) (output-type-for-declare-form-rec (cadr form) flet-alist))
    ((member (car form) '(time progn) :test 'eq) (output-type-for-declare-form-rec (car (last form))
        flet-alist))
    ((member (car form)
       '(tagbody throw-raw-ev-fncall throw-nonexec-error eval error)
       :test 'eq) (setq *acl2-output-type-abort* '*))
    ((member (car form)
       '(* +
         -
         /
         1+
         1-
         =
         /=
         <
         <=
         >
         >=
         append
         assoc
         concatenate
         format
         import
         list
         list*
         make-hash-table
         member
         mv-list
         nreverse
         position
         rassoc
         remove
         subsetp
         cadr
         cdar
         caar
         cddr
         caadr
         cdadr
         cadar
         cddar
         caaar
         cdaar
         caddr
         cdddr
         caaadr
         cadadr
         caadar
         caddar
         cdaadr
         cddadr
         cdadar
         cdddar
         caaaar
         cadaar
         caaddr
         cadddr
         cdaaar
         cddaar
         cdaddr
         cddddr)
       :test 'eq) t)
    (t (multiple-value-bind (new-form flg)
        (macroexpand-1 form)
        (cond ((null flg) (cond ((atom form) t)
              ((eq (car form) 'multiple-value-prog1) (and (consp (cdr form))
                  (output-type-for-declare-form-rec (cadr form) flet-alist)))
              ((and (consp (car form)) (eq (caar form) 'lambda)) (output-type-for-declare-form-rec (caddr (car form))
                  flet-alist))
              ((not (symbolp (car form))) '*)
              (t (let ((x (and (boundp 'current-acl2-world)
                       (fboundp 'get-stobjs-out-for-declare-form)
                       (qfuncall get-stobjs-out-for-declare-form (car form)))))
                  (cond ((consp (cdr x)) (cons 'values (make-list (length x) :initial-element t)))
                    (x t)
                    (t (setq *acl2-output-type-abort* '*)))))))
          (t (output-type-for-declare-form-rec new-form flet-alist)))))))

(defun output-type-for-declare-form-rec-list
  (forms flet-alist)
  (cond ((atom forms) nil)
    (t (cons (let ((tp (output-type-for-declare-form-rec (car forms) flet-alist)))
          (if (member tp '(nil *) :test 'eq)
            t
            tp))
        (output-type-for-declare-form-rec-list (cdr forms)
          flet-alist)))))

(defun output-type-for-declare-form
  (fn form)
  (let* ((*acl2-output-type-abort* nil) (result (output-type-for-declare-form-rec form nil))
      (stobjs-out (and (not (member fn (symbol-value '*stobjs-out-invalid*) :test (function eq)))
          (boundp 'current-acl2-world)
          (fboundp 'get-stobjs-out-for-declare-form)
          (qfuncall get-stobjs-out-for-declare-form fn))))
    (when (and stobjs-out
        (not (eq (and (consp result) (eq (car result) 'values))
            (consp (cdr stobjs-out))))
        (not *acl2-output-type-abort*))
      (error "Implementation error in ~s:~%~
              stobjs-out and result don't mesh.~%~
              Stobjs-out = ~s~%~
              Result = ~s~%~
              Please contact the ACL2 implementors."
        (list 'output-type-for-declare-form fn '|defun...|)
        stobjs-out
        result))
    (cond ((and (consp result) (eq (car result) 'values)) result)
      ((or *acl2-output-type-abort* (eq result '*)) '*)
      (t (list 'values result)))))

(defun make-defun-declare-form
  (fn form &optional (output-type nil output-type-p))
  (when *do-proclaims*
    (let* ((output-type (if output-type-p
           output-type
           (output-type-for-declare-form fn (car (last form))))))
      (let ((formals (caddr form)))
        (cond ((null (intersection formals lambda-list-keywords :test 'eq)) `(declaim (ftype (function ,(ARG-DECLARATIONS FORMALS (COLLECT-TYPES (CDDDR FORM)))
                  ,OUTPUT-TYPE)
                ,(CADR FORM))))
          (t nil))))))

(defun make-defconst-declare-form
  (form)
  (when *do-proclaims*
    (let* ((output (macroexpand-till (caddr form) 'the)) (output-type (cond ((and (consp output) (eq 'the (car output))) (cadr output))
            (t nil))))
      (cond (output-type `(declaim (type ,OUTPUT-TYPE ,(CADR FORM))))
        (t (let ((val (symbol-value (cadr form))))
            (if (integerp val)
              `(declaim (type (integer ,VAL ,VAL) ,(CADR FORM)))
              nil)))))))

(defun make-defstobj-declare-form
  (form)
  (when *do-proclaims*
    (let* ((name (cadr form)) (args (cddr form))
        (template (qfuncall defstobj-template name args nil))
        (raw-defs (qfuncall defstobj-raw-defs name template nil nil)))
      (cons 'progn
        (mapcar (function (lambda (def)
              (if (member (symbol-value '*stobj-inline-declare*)
                  def
                  :test (function equal))
                nil
                (make-defun-declare-form (car def) (cons 'defun def)))))
          raw-defs)))))

(defun proclaim-form
  (form &optional stream)
  (when *do-proclaims*
    (cond ((consp form) (case (car form)
          ((in-package) (eval-or-print form stream)
            (when stream (eval form))
            nil)
          ((defmacro defvar defparameter) nil)
          ((defconst) (eval-or-print (make-defconst-declare-form form) stream)
            nil)
          ((defstobj) (eval-or-print (make-defstobj-declare-form form) stream))
          ((eval-when) (dolist (x (cddr form)) (proclaim-form x stream))
            nil)
          ((progn mutual-recursion) (dolist (x (cdr form)) (proclaim-form x stream))
            nil)
          ((defun defund) (eval-or-print (make-defun-declare-form (cadr form) form)
              stream)
            nil)
          (defun-one-output (eval-or-print (make-defun-declare-form (cadr form) form '(values t))
              stream)
            nil)
          (otherwise nil)))
      (t nil))))

(defun proclaim-file
  (name &optional stream)
  (when *do-proclaims*
    (format t "Note: Proclaiming file ~s.~%" name)
    (with-open-file (file name :direction :input)
      (let ((eof (cons nil nil)) (*package* *package*))
        (loop (let ((form (read file nil eof)))
            (cond ((eq eof form) (return nil))
              (t (proclaim-form form stream)))))
        nil))))

(defun constant-backquote-term-p
  (x)
  (cond ((and (vectorp x) (not (stringp x))) nil)
    ((atom x) t)
    ((eq (car x) *comma*) nil)
    ((eq (car x) *comma-atsign*) nil)
    ((eq (car x) 'lambda) nil)
    (t (constant-backquote-lst-p x))))

(defun constant-backquote-lst-p
  (l)
  (cond ((atom l) t)
    ((eq (car l) *comma*) nil)
    ((eq (car l) *comma-atsign*) nil)
    ((and (consp (car l)) (eq (caar l) *comma*)) nil)
    ((and (consp (car l)) (eq (caar l) *comma-atsign*)) nil)
    (t (and (constant-backquote-term-p (car l))
        (constant-backquote-lst-p (cdr l))))))

(defun acl2-reader-error
  (string &rest args)
  (clear-input)
  (let ((*hard-error-returns-nilp* nil))
    (declare (special *hard-error-returns-nilp*))
    (qfuncall hard-error
      'acl2-reader
      string
      (qfuncall pairlis$ (symbol-value '*base-10-chars*) args))))

(defun backquote
  (x)
  "The two functions BACKQUOTE and BACKQUOTE-LST implement backquote
as described on pp. 349-350 of CLTL1 except that (a) use of vector
notation causes an error and (b) the use of ,. is not permitted."
  (cond ((and (vectorp x) (not (stringp x))) (acl2-reader-error "ACL2 does not handle vectors in backquote."))
    ((constant-backquote-term-p x) (list 'quote x))
    ((eq (car x) *comma*) (cadr x))
    ((eq (car x) *comma-atsign*) (acl2-reader-error "`,@ is an error"))
    (t (backquote-lst x))))

(defun backquote-lst
  (l)
  (cond ((eq (car l) *comma*) (cadr l))
    ((eq (car l) *comma-atsign*) (acl2-reader-error ". ,@ is illegal."))
    (t (let ((r (if (constant-backquote-lst-p (cdr l))
             (list 'quote (cdr l))
             (backquote-lst (cdr l)))))
        (cond ((and (consp (car l)) (eq (caar l) *comma-atsign*)) (cond ((null (cdr l)) (cadr (car l)))
              (t (list 'append (cadr (car l)) r))))
          (t (list 'cons `(car l) r)))))))

(defun acl2-comma-reader
  (stream)
  (when *read-object-comma-count*
    (incf *read-object-comma-count*))
  (when (< *backquote-counter* 0)
    (let* ((pathname (and (typep stream 'file-stream) (pathname stream))) (posn (and pathname (file-position stream))))
      (cond (posn (acl2-reader-error "Illegal comma encountered by READ: file ~x0, position ~x1."
            (namestring pathname)
            posn))
        (*read-object-comma-count* (acl2-reader-error "Illegal comma: ~n0 comma processed while reading top-level form."
            (list *read-object-comma-count*)))
        (t (acl2-reader-error "Illegal comma encountered by READ.")))))
  (case (peek-char nil stream t nil t)
    (#\@ (read-char stream t nil t)
      (list *comma-atsign* (read stream t nil t)))
    (#\. (acl2-reader-error ",. not allowed in ACL2 backquote forms."))
    (otherwise (list *comma* (read stream t nil t)))))

(defun symbol-package-name
  (x)
  (cond ((get x *initial-lisp-symbol-mark*))
    ((let ((p (symbol-package x)))
       (cond ((eq p *main-lisp-package*) (setf (get x *initial-lisp-symbol-mark*)
             *main-lisp-package-name-raw*))
         (t (and p (package-name p))))))
    (t (error "The symbol ~a, which has no package, was encountered~%~
             by ACL2.  This is an inconsistent state of affairs, one that~%~
             may have arisen by undoing a defpkg but holding onto a symbol~%~
             in the package being flushed, contrary to warnings printed.~%~%"
        x))))

(defun maybe-make-package
  (name)
  (when (not (find-package name))
    (make-package name :use nil)))

(defun maybe-make-three-packages
  (name)
  (maybe-make-package name)
  (maybe-make-package (concatenate 'string *global-package-prefix* name))
  (maybe-make-package (concatenate 'string *1*-package-prefix* name)))

(defun package-has-no-imports
  (name)
  (let ((pkg (find-package name)))
    (do-symbols (sym pkg)
      (when (not (eq (symbol-package sym) pkg))
        (return-from package-has-no-imports nil))))
  t)

(defun maybe-introduce-empty-pkg-2
  (name)
  (when (and (not (member name *defpkg-virgins* :test 'equal))
      (not (assoc name *ever-known-package-alist* :test 'equal))
      (package-has-no-imports name))
    (push name *defpkg-virgins*)))

(defun rev1@
  (x acc)
  (cond ((atom x) (cons x acc))
    (t (rev1@ (cdr x) (cons (car x) acc)))))

(defun acl2-read-character-string
  (s acc)
  (let* ((ch (read-char s nil nil)))
    (cond ((or (null ch) (member ch *acl2-read-character-terminators*)) (when ch (unread-char ch s))
        (cond ((characterp acc) acc)
          (t (let ((x (coerce (rev1@ acc nil) 'string)))
              (cond ((string-equal x "SPACE") #\ )
                ((string-equal x "TAB") #\	)
                ((string-equal x "NEWLINE") #\
)
                ((string-equal x "PAGE") #\)
                ((string-equal x "RUBOUT") #\)
                ((string-equal x "RETURN") #\
)
                (t (funcall (if (fboundp 'interface-er)
                      'interface-er
                      'error)
                    "When the ACL2 reader tries to read #\x, then x must ~
                       either be a single character or one of Space, Tab, ~
                       Newline, Page, Rubout, or Return (where case is ~
                       ignored).  What follows x must be a character in the ~
                       list:~|~X01.~|However, ~s2 is neither a single ~
                       character nor one of Space, Tab, Newline, Page, ~
                       Rubout, or Return (where case is ignored)."
                    *acl2-read-character-terminators*
                    nil
                    x)))))))
      (t (acl2-read-character-string s (cons ch acc))))))

(defun acl2-character-reader
  (s c n)
  (declare (ignore n c))
  (let ((ch (read-char s)))
    (acl2-read-character-string s ch)))

(defun sharp-dot-read
  (stream char n)
  (when (not (and (boundp 'current-acl2-world)
        (symbol-value 'current-acl2-world)))
    (return-from sharp-dot-read
      (funcall *old-sharp-dot-read* stream char n)))
  (let ((whitespace-chars '(#\ #\	 #\
 #\
 #\ #\
 #\ )))
    (when (member (peek-char nil stream nil nil t) whitespace-chars)
      (acl2-reader-error "#. must be followed immediately by a non-whitespace character.  See ~
        :DOC sharp-dot-reader.")))
  (let* ((*inside-sharp-dot-read* (or (not *inside-sharp-dot-read*)
         (acl2-reader-error "Recursive attempt to read a sharp-dot (#.) expression while ~
                inside a sharp-dot expression.  This is not allowed in ACL2."))) (sym (read stream t nil t))
      (val (and (symbolp sym)
          (qfuncall fgetprop
            sym
            'const
            nil
            (qfuncall w *the-live-state*)))))
    (cond (val (cond ((and (consp val)
             (eq (car val) 'quote)
             (consp (cdr val))
             (null (cddr val))) (cadr val))
          (t (acl2-reader-error "(Implementation error) Found non-quotep 'const property for ~
                 ~x0."
              sym))))
      (sym (acl2-reader-error "ACL2 supports #. syntax only for #.*a*, where *a* has been defined ~
        by ~x0.  Thus the form #.~x1 is illegal.  See :DOC sharp-dot-reader~@2."
          'defconst
          sym
          (cond ((eval '(f-get-global 'certify-book-info *the-live-state*)) ", in particular Remark (2)")
            (t ""))))
      (t (acl2-reader-error "ACL2 supports #. syntax only for #.*a*, where *a* has been defined by ~
        ~x0."
          'defconst)))))

(defun sharp-bang-read
  (stream char n)
  (declare (ignore char n))
  (let* ((package-name (read stream t nil t)) (package-string (cond ((symbolp package-name) (symbol-name package-name))
          ((stringp package-name) package-name)
          (t (acl2-reader-error "A package name appears to have been ~
                                    missing, where the form ~x0 was read ~
                                    immediately after a #! directive.~|See ~
                                    :DOC sharp-bang-reader."
              package-name))))
      (*package* (cond (*read-suppress* *package*)
          ((assoc package-string
             (qfuncall known-package-alist *the-live-state*)
             :test 'equal) (qfuncall find-package-fast package-string))
          (t (acl2-reader-error "There is no package named ~x0 that is known to ACL2 ~
                        in this context."
              package-string)))))
    (read stream t nil t)))

(defun sharp-u-read
  (stream char n)
  (declare (ignore char n))
  (let* ((*inside-sharp-u-read* (or (not *inside-sharp-u-read*)
         (acl2-reader-error "Recursive attempt to read a sharp-u (#u) expression while ~
                inside a sharp-u expression.  This is not allowed."))) (x (read stream t nil t)))
    (cond ((numberp x) x)
      ((not (symbolp x)) (acl2-reader-error "Failure to read #u expression: #u was not followed by a symbol."))
      (t (let* ((name (symbol-name x)) (c (and (not (equal name "")) (char name 0))))
          (cond ((member c '(#\B #\O #\X)) (values (read-from-string (concatenate 'string "#" (remove #\_ name)))))
            (t (let ((n (read-from-string (remove #\_ name))))
                (cond ((numberp n) n)
                  (*read-suppress* nil)
                  (t (acl2-reader-error "Failure to read #u expression: result ~s is ~
                                not a numeral."
                      n)))))))))))

(defun read-digits
  (stream base-16-p)
  (declare (special *hex-array* *base-10-array*))
  (let ((base-array (if base-16-p
         *hex-array*
         *base-10-array*)) (sign (read-char stream nil :eof t))
      tmp
      lst)
    (cond ((eq sign :eof) (return-from read-digits (values 0 nil :eof)))
      ((not (member sign '(#\+ #\-))) (unread-char sign stream)))
    (loop (setq tmp (read-char stream nil :eof t))
      (cond ((eq tmp :eof) (return))
        ((eql tmp #\_))
        ((aref base-array (char-code tmp)) (push tmp lst))
        (t (return))))
    (let ((len (length lst)))
      (values len
        (eql sign #\-)
        (cond ((null lst) 0)
          (t (let ((*read-base* (if base-16-p
                   16
                   10)))
              (read-from-string (coerce (nreverse lst) 'string)))))
        tmp))))

(defun sharp-f-read
  (stream char n)
  (declare (ignore char n))
  (flet ((read-exp (stream)
       (multiple-value-bind (len negp exp next-char)
         (read-digits stream nil)
         (when (eql len 0)
           (cond (*read-suppress* (return-from sharp-f-read nil))
             (t (acl2-reader-error "Empty exponent in #f expression."))))
         (unread-char next-char stream)
         (if negp
           (- exp)
           exp))))
    (let* ((tmp (read-char stream nil :eof t)) (base-16-p (cond ((member tmp '(#\x #\X)) t)
            ((eq tmp :eof) (cond (*read-suppress* (return-from sharp-f-read nil))
                (t (acl2-reader-error "End of file encountered after #f."))))
            (t (unread-char tmp stream) nil)))
        (exp-chars (if base-16-p
            '(#\p #\P)
            '(#\e #\E))))
      (multiple-value-bind (len negp before-dot next-char)
        (read-digits stream base-16-p)
        (declare (ignore len))
        (cond ((eq next-char :eof) (if negp
              (- before-dot)
              before-dot))
          ((member next-char exp-chars) (let* ((exp (read-exp stream)))
              (* (if negp
                  (- before-dot)
                  before-dot)
                (expt (if base-16-p
                    2
                    10)
                  exp))))
          ((eql next-char #\.) (multiple-value-bind (len negp-after-dot after-dot next-char)
              (read-digits stream base-16-p)
              (when negp-after-dot
                (cond (*read-suppress* (return-from sharp-f-read nil))
                  (t (acl2-reader-error "Illegal sign after point in #f expression."))))
              (let ((significand (+ before-dot
                     (/ after-dot
                       (expt (if base-16-p
                           16
                           10)
                         len)))))
                (cond ((member next-char exp-chars) (let* ((exp (read-exp stream)))
                      (* (if negp
                          (- significand)
                          significand)
                        (expt (if base-16-p
                            2
                            10)
                          exp))))
                  (t (unread-char next-char stream)
                    (if negp
                      (- significand)
                      significand))))))
          (t (unread-char next-char stream)
            (if negp
              (- before-dot)
              before-dot)))))))

(defun sharp-d-read
  (stream char n)
  (declare (ignore char n))
  (let ((num (read stream t nil t)))
    (when (not (typep num 'double-float))
      (acl2-reader-error "The value, ~s0, was read from a token following #d that did not have ~
        the syntax of a double-float.  See :DOC df."
        (format nil "~s" num)))
    (when (or (= num #.SB-EXT:DOUBLE-FLOAT-POSITIVE-INFINITY)
        (= num #.SB-EXT:DOUBLE-FLOAT-NEGATIVE-INFINITY)
        (float-nan-p num))
      (error "The exceptional floating-point value ~s cannot be converted ~
                  to a rational number."
        num))
    (rational num)))

(defun fancy-string-reader-escape-check
  (acc)
  (if (atom acc)
    nil
    (if (eql (car acc) #\\)
      (fancy-string-reader-escape-check (cdr acc))
      (and (eql (first acc) #\")
        (eql (second acc) #\")
        (eql (third acc) #\")))))

(defun fancy-string-reader-macro-aux
  (stream acc)
  (let ((char (read-char stream)))
    (if (and (eql char #\}) (fancy-string-reader-escape-check acc))
      (if (eql (car acc) #\\)
        (fancy-string-reader-macro-aux stream (cons #\} (cdr acc)))
        (cdddr acc))
      (fancy-string-reader-macro-aux stream (cons char acc)))))

(defun fancy-string-reader-macro
  (stream subchar arg)
  (declare (ignorable subchar arg))
  (let ((quote1 (read-char stream)))
    (unless (eql quote1 #\")
      (acl2-reader-error "Undefined reader macro: #{~s0"
        (string quote1))))
  (let ((quote2 (read-char stream)))
    (unless (eql quote2 #\")
      (acl2-reader-error "Undefined reader macro: #{"~s0"
        (string quote2))))
  (let ((quote3 (read-char stream)))
    (unless (eql quote3 #\")
      (acl2-reader-error "Undefined reader macro: #{""~s0"
        (string quote3))))
  (let ((rchars (fancy-string-reader-macro-aux stream nil)))
    (nreverse (coerce rchars 'string))))

(defun update-sharp-reader-max-index
  (index)
  (when (< *sharp-reader-max-index* index)
    (when (>= index *sharp-reader-array-size*)
      (when (>= index *sharp-reader-max-array-size*)
        (acl2-reader-error "Lisp reader encountered #=~x0 (maximum index is ~x1)."
          index
          (1- *sharp-reader-max-array-size*)))
      (let* ((new-sharp-reader-array-size (max (1+ index)
             (min (* *sharp-reader-array-size-multiplier*
                 *sharp-reader-array-size*)
               *sharp-reader-max-array-size*))) (new-sharp-reader-array (make-array new-sharp-reader-array-size))
          (bound (the (unsigned-byte 29) (1+ *sharp-reader-max-index*))))
        (do ((i 0 (the (unsigned-byte 29) (1+ i))))
          ((eql i bound))
          (declare (type (unsigned-byte 29) i))
          (setf (svref new-sharp-reader-array i)
            (svref *sharp-reader-array* i)))
        (setq *sharp-reader-array*
          new-sharp-reader-array
          *sharp-reader-array-size*
          new-sharp-reader-array-size)))
    (setq *sharp-reader-max-index* index)))

(defun reckless-sharp-sharp-read
  (stream char arg)
  (declare (ignore stream char))
  (cond (*read-suppress* nil)
    (t (svref *sharp-reader-array* arg))))

(defun reckless-sharp-equal-read
  (stream char arg)
  (declare (ignore char))
  (cond (*read-suppress* (values))
    (t (let ((val (read stream t nil t)))
        (update-sharp-reader-max-index arg)
        (setf (svref *sharp-reader-array* arg) val)))))

(defun getenv$-raw
  (string)
  (let* ((val (let ((fn 'posix-getenv))
         (and (fboundp fn) (funcall fn string)))) (msg (and val
          (fboundp 'bad-lisp-stringp)
          (qfuncall bad-lisp-stringp val))))
    (cond (msg (qfuncall interface-er
          "The value of environment variable ~x0 is ~x1, which is not a ~
             legal ACL2 string.~%~@2"
          string
          val
          msg))
      (t val))))

(defun get-os nil (return-from get-os :unix))

(defun our-truename
  (filename &optional namestringp)
  (when (pathnamep filename)
    (setq filename (namestring filename)))
  (when (search "//" filename)
    (error "The filename~%~s~%is illegal because it has consecutive directory ~
            separators, //."
      filename))
  (let* ((truename (cond (t (ignore-errors (truename filename))))) (namestring (and truename (namestring truename))))
    (cond ((null namestringp) truename)
      ((null truename) (cond ((eq namestringp :safe) nil)
          (t (qfuncall interface-er
              "Unable to obtain the truename of file ~x0.~@1"
              filename
              (if (qfuncall msgp namestringp)
                (list "  ~@0" (cons #\0 namestringp))
                "")))))
      (t namestring))))

(defun unix-full-pathname
  (name &optional extension)
  (let* ((*check-namestring* t) (os (get-os))
      (state *the-live-state*)
      (name (qfuncall pathname-os-to-unix
          (if extension
            (concatenate 'string name "." extension)
            name)
          os
          state)))
    (qfuncall cancel-dot-dots
      (cond ((qfuncall absolute-pathname-string-p name nil os) name)
        (t (concatenate 'string (qfuncall our-pwd) name))))))

(defun our-user-homedir-pathname
  nil
  (our-ignore-errors (user-homedir-pathname)))

(defun ser-cons-reader-macro
  (stream subchar arg)
  (declare (ignorable subchar arg))
  (ser-decode-from-stream nil :never stream))

(defun ser-hons-reader-macro
  (stream subchar arg)
  (declare (ignorable subchar arg))
  (ser-decode-from-stream nil :smart stream))

(defun load-compiled
  (filename &optional verbose)
  (when (and verbose *load-compiled-verbose*)
    (eval `(format t "~&Note: loading file ~s.~&" ',FILENAME)))
  (load filename))

(defun make-lock
  (&optional lock-name)
  (make-mutex :name lock-name))

(defun our-pwd
  nil
  (qfuncall pathname-os-to-unix
    (our-truename "" "Note: Calling OUR-TRUENAME from OUR-PWD.")
    (get-os)
    *the-live-state*))