acl2

(push :acl2 *features*)

(push :cltl2 *features*)

(in-package "COMMON-LISP-USER")

(defvar *acl2-compiler-enabled*)

(defvar *acl2-optimize-form*
  `(optimize (compilation-speed 0)
    (inhibit-warnings 3)
    (speed 3)
    (space ,(LET ((COMMON-LISP-USER::OUR-SPACE
        (IF (BOUNDP 'COMMON-LISP-USER::*ACL2-SPACE*)
            (SYMBOL-VALUE 'COMMON-LISP-USER::*ACL2-SPACE*)
            NIL)))
   (IF COMMON-LISP-USER::OUR-SPACE
       (PROGN
        (FORMAT T "Note: Setting SPACE to ~s." COMMON-LISP-USER::OUR-SPACE)
        COMMON-LISP-USER::OUR-SPACE)
       1)))
    (safety ,(LET ((COMMON-LISP-USER::OUR-SAFETY
        (IF (BOUNDP 'COMMON-LISP-USER::*ACL2-SAFETY*)
            (SYMBOL-VALUE 'COMMON-LISP-USER::*ACL2-SAFETY*)
            NIL)))
   (IF COMMON-LISP-USER::OUR-SAFETY
       (PROGN
        (FORMAT T "Note: Setting SAFETY to ~s." COMMON-LISP-USER::OUR-SAFETY)
        COMMON-LISP-USER::OUR-SAFETY)
       0)))))

(proclaim *acl2-optimize-form*)

(defun acl2-set-character-encoding
  nil
  (setq *default-external-format* :iso-8859-1)
  (setq *default-c-string-external-format* :iso-8859-1))

(acl2-set-character-encoding)

(setq *read-default-float-format* 'double-float)

(let ((*print-base* 16) (*print-case* :downcase))
  (let ((tmp (with-output-to-string (s)
         (princ 10 s))))
    (cond ((equal tmp "A"))
      ((equal tmp "a") (format t
          "~%Note: Numbers in base 16 will be printed using a ~
                    special-purpose~%      ACL2 function, ~s."
          'print-number-base-16-upcase-digits)
        (push :acl2-print-number-base-16-upcase-digits *features*))
      (t (error "Surprising result for (princ 10 s) in base 16: ~s"
          tmp)))))

(setq *compile-verbose* nil)

(setq *compile-print* nil)

(unless (= (char-code (char (string-downcase (coerce (list #\�) 'string))
        0))
    (char-code (char-downcase #\�)))
  (defvar *old-string-downcase*
    (symbol-function 'string-downcase))
  (defun string-downcase-sbcl
    (x &key
      (start 0)
      (end nil))
    (declare (special *old-string-downcase*))
    (let* ((x (string x)) (p (position #\�
            x
            :start start
            :end end)))
      (if p
        (if end
          (concatenate 'string
            (subseq x 0 p)
            (coerce (loop for
                i
                from
                p
                to
                (1- end)
                collect
                (char-downcase (char x i)))
              'string)
            (subseq x
              end
              (length x)))
          (concatenate 'string
            (subseq x 0 p)
            (coerce (loop for
                i
                from
                p
                to
                (1- (length x))
                collect
                (char-downcase (char x i)))
              'string)))
        (funcall *old-string-downcase*
          x
          :start start
          :end end))))
  (without-package-locks (defun string-downcase
      (x &key
        (start 0)
        (end nil))
      (string-downcase-sbcl x
        :start start
        :end end))))

(let ((lisp-pkg (find-package "LISP")))
  (if lisp-pkg
    (let ((cl-pkg (find-package "COMMON-LISP")))
      (cond ((and cl-pkg
           (eq cl-pkg lisp-pkg)))
        (t (when cl-pkg
            (error "This Lisp is unsuitable for ACL2, because the ~
                    COMMON-LISP~% package is defined but is not the LISP ~
                    package."))
          (let ((old-name (package-name lisp-pkg)) (old-nicknames (package-nicknames lisp-pkg)))
            (rename-package "LISP"
              old-name
              (cons "COMMON-LISP" old-nicknames))))))))

(eval-when (:compile-toplevel)
  (error "The file acl2.lisp should never be compiled."))

(dolist (p (list-all-packages))
  (cond ((equal 4
       (string< "ACL2" (package-name p))) (format t
        "~%~%Warning:  There is already a package with the ~
                 name ~a. ~%The ACL2 implementation depends upon ~
                 having complete knowledge of ~%and control over any ~
                 package whose name begins with the ~%four letters ``ACL2'', ~
                 so ACL2 may not work in this Lisp."
        (package-name p))
      (cond ((package-use-list p) (format t
            "~%~%Warning:  The package with name ~a ~
                   USES the packages in the list ~a.  ACL2 will not work ~
                   in state of affairs."
            (package-name p)
            (package-use-list p)))))))

(or (find-package "ACL2") (make-package "ACL2" :use nil))

(let ((inv "ACL2_INVISIBLE"))
  (or (find-package inv)
    (make-package inv :use nil)))

(defconstant *the-live-state*
  '|The Live State Itself|)

(defvar *compiling-certified-file* nil)

(defparameter *safe-mode-verified-p* nil)

(declaim (ftype (function (t) (values t)) large-consp))

(defun elided-defconst-index
  (term)
  (and (consp term)
    (consp (cdr term))
    (null (cddr term))
    (eq (car term) 'cadr)
    (let ((x (cadr term)))
      (and (consp x)
        (consp (cdr x))
        (null (cddr x))
        (eq (car x)
          (symbol-value '*elided-defconst*))
        (cadr x)))))

(defvar *hcomp-elided-defconst-alist* nil)

(defun elided-defconst
  (name index)
  (let ((pair (pop *hcomp-elided-defconst-alist*)))
    (if (and (consp pair)
        (eql (car pair) index)
        (eq (cadr pair) name))
      (cddr pair)
      (error "An unexpected error was encountered when trying to obtain a ~%~
              value for the constant, ~s.  If you have not deliberately ~%~
              messed with write-dates of files, please report this error to ~%~
              the ACL2 implementors."
        name))))

(defmacro defconst
  (name term
    &rest
    rst)
  (declare (ignore rst))
  (let ((disc (gensym)))
    `(defparameter ,COMMON-LISP-USER::NAME
      (let ((*safe-mode-verified-p* t))
        (cond ((boundp ',COMMON-LISP-USER::NAME) (cond (*compiling-certified-file* (symbol-value ',COMMON-LISP-USER::NAME))
              (t (let ((,COMMON-LISP-USER::DISC (get ',COMMON-LISP-USER::NAME
                       'redundant-raw-lisp-discriminator)))
                  (cond ((and (consp ,COMMON-LISP-USER::DISC)
                       (eq (car ,COMMON-LISP-USER::DISC) 'defconst)) (assert (consp (cdr ,COMMON-LISP-USER::DISC)))
                      (cond ((and (eq (cdr (cdr ,COMMON-LISP-USER::DISC))
                             (symbol-value ',COMMON-LISP-USER::NAME))
                           (or ,@(AND (NOT (ELIDED-DEFCONST-INDEX COMMON-LISP-USER::TERM))
       `((LET ((COMMON-LISP-USER::DISC ,COMMON-LISP-USER::DISC)
               (COMMON-LISP-USER::QTERM ',COMMON-LISP-USER::TERM))
           (AND (FBOUNDP 'LARGE-CONSP)
                (NOT (LARGE-CONSP COMMON-LISP-USER::QTERM))
                (EQUAL (CAR (CDR COMMON-LISP-USER::DISC))
                       COMMON-LISP-USER::QTERM)))))
                             (equal (cdr (cdr ,COMMON-LISP-USER::DISC))
                               ,COMMON-LISP-USER::TERM))) (symbol-value ',COMMON-LISP-USER::NAME))
                        (t (qfuncall defconst-redeclare-error ',COMMON-LISP-USER::NAME))))
                    ((raw-mode-p *the-live-state*) ,COMMON-LISP-USER::TERM)
                    (t (qfuncall defconst-redeclare-error ',COMMON-LISP-USER::NAME)))))))
          (t ,(LET ((COMMON-LISP-USER::INDEX (ELIDED-DEFCONST-INDEX COMMON-LISP-USER::TERM)))
   (IF (NULL COMMON-LISP-USER::INDEX)
       `(LET* ((COMMON-LISP-USER::VAL ,COMMON-LISP-USER::TERM)
               (COMMON-LISP-USER::D
                (LIST* 'DEFCONST ',COMMON-LISP-USER::TERM
                       COMMON-LISP-USER::VAL)))
          (SETF (GET ',COMMON-LISP-USER::NAME
                     'REDUNDANT-RAW-LISP-DISCRIMINATOR)
                  COMMON-LISP-USER::D)
          (CDR (CDR COMMON-LISP-USER::D)))
       `(LET* ((COMMON-LISP-USER::QVAL
                (ELIDED-DEFCONST ',COMMON-LISP-USER::NAME
                                 ,COMMON-LISP-USER::INDEX))
               (COMMON-LISP-USER::VAL
                (PROGN
                 (ASSERT
                  (AND (CONSP COMMON-LISP-USER::QVAL)
                       (EQ (CAR COMMON-LISP-USER::QVAL) 'QUOTE)))
                 (CADR COMMON-LISP-USER::QVAL)))
               (COMMON-LISP-USER::D
                (LIST* 'DEFCONST COMMON-LISP-USER::QVAL COMMON-LISP-USER::VAL)))
          (SETF (GET ',COMMON-LISP-USER::NAME
                     'REDUNDANT-RAW-LISP-DISCRIMINATOR)
                  COMMON-LISP-USER::D)
          (CDR (CDR COMMON-LISP-USER::D)))))))))))

(defvar *copy-of-common-lisp-symbols-from-main-lisp-package*)

(defvar *copy-of-common-lisp-specials-and-constants*)

(defvar *copy-of-acl2-version*)

(defconstant *acl2-files*
  '("serialize-raw" "axioms"
    "hons"
    "hons-raw"
    "basis-a"
    "memoize"
    "serialize"
    "basis-b"
    "parallel"
    "memoize-raw"
    "float-a"
    "translate"
    "type-set-a"
    "linear-a"
    "type-set-b"
    "linear-b"
    "non-linear"
    "tau"
    "rewrite"
    "simplify"
    "bdd"
    "other-processes"
    "induct"
    "proof-builder-pkg"
    "doc"
    "history-management"
    "prove"
    "defuns"
    "proof-builder-a"
    "defthm"
    "other-events"
    "float-b"
    "ld"
    "proof-builder-b"
    "apply-raw"
    "interface-raw"
    "float-raw"
    "defpkgs"
    "boot-strap-pass-2-a"
    "apply-prim"
    "apply-constraints"
    "apply"
    "boot-strap-pass-2-b")
  "*acl2-files* is the list of all the files necessary to build
ACL2 from scratch.")

(with-open-file (fl "axioms.lisp" :direction :input)
  (let ((*package* (find-package "COMMON-LISP")))
    (read fl)
    (setq *copy-of-common-lisp-symbols-from-main-lisp-package*
      (eval (caddr (read fl))))
    (import *copy-of-common-lisp-symbols-from-main-lisp-package*
      "ACL2")
    (setq *copy-of-acl2-version*
      (concatenate 'string "ACL2 Version 8.6"))
    (setq *copy-of-common-lisp-specials-and-constants*
      (eval (caddr (read fl))))))

(in-package "ACL2")

(defun proclaim-optimize
  nil
  (proclaim *acl2-optimize-form*))

(defparameter *compiled-file-extension*
  (pathname-type (compile-file-pathname "foo.lisp")))

(defmacro initialize-state-globals
  nil
  (let ((acl2-compiler-enabled-var '*acl2-compiler-enabled*))
    `(let ((state *the-live-state*))
      (dolist (pair *initial-global-table*)
        (f-put-global (car pair) (cdr pair) state))
      (f-put-global 'acl2-sources-dir (our-pwd) state)
      (f-put-global 'iprint-ar
        (compress1 'iprint-ar (f-get-global 'iprint-ar state))
        state)
      (f-put-global 'ld-history
        (list (make ld-history-entry))
        state)
      (f-put-global 'compiler-enabled
        (cond ((boundp ',ACL2-COMPILER-ENABLED-VAR) (or (member ,ACL2-COMPILER-ENABLED-VAR '(t nil :books))
              (error "Illegal value for ~
                                        user::*acl2-compiler-enabled*, ~s"
                ,ACL2-COMPILER-ENABLED-VAR))
            ,ACL2-COMPILER-ENABLED-VAR)
          (t :books))
        state)
      (f-put-global 'host-lisp
        ,(LET ()
   :SBCL)
        state)
      (f-put-global 'compiled-file-extension
        ,*COMPILED-FILE-EXTENSION*
        state)
      (f-put-global 'tmp-dir "/tmp" state)
      nil)))

(defconstant *suppress-compile-build-time* t)

(defparameter *global-package-prefix* "ACL2_GLOBAL_")

(defparameter *1*-package-prefix* "ACL2_*1*_")

(defun make-global-package
  (x)
  (let* ((n (concatenate 'string *global-package-prefix* x)) (p (find-package n)))
    (cond (p (do-symbols (sym p) (makunbound sym)))
      (t (make-package n :use nil)))))

(defun make-*1*-package
  (x)
  (let* ((n (concatenate 'string *1*-package-prefix* x)))
    (make-package n :use nil)))

(or (find-package "ACL2-INPUT-CHANNEL")
  (make-package "ACL2-INPUT-CHANNEL" :use nil))

(or (find-package "ACL2-OUTPUT-CHANNEL")
  (make-package "ACL2-OUTPUT-CHANNEL" :use nil))

(defconstant *main-lisp-package*
  (find-package "COMMON-LISP"))

(defconstant *main-lisp-package-name-raw* "COMMON-LISP")

(make-global-package *main-lisp-package-name-raw*)

(make-global-package "KEYWORD")

(make-global-package "ACL2")

(make-global-package "ACL2-INPUT-CHANNEL")

(make-global-package "ACL2-OUTPUT-CHANNEL")

(make-*1*-package *main-lisp-package-name-raw*)

(make-*1*-package "ACL2")

(make-*1*-package "ACL2-INPUT-CHANNEL")

(make-*1*-package "ACL2-OUTPUT-CHANNEL")

(defparameter *initial-lisp-symbol-mark*
  'initial-lisp-symbol-mark)

(let ((cl-pkg-name *main-lisp-package-name-raw*))
  (dolist (sym *copy-of-common-lisp-symbols-from-main-lisp-package*)
    (setf (get sym *initial-lisp-symbol-mark*) cl-pkg-name)))

(defconstant *acl2-package* (find-package "ACL2"))

(dolist (x *features*)
  (cond ((or (equal "ACL2-LOOP-ONLY" (symbol-name x))
       (equal "ACL2-METERING" (symbol-name x))) (format t
        "~%~%Warning:  This Common Lisp may be ~
                          unsuitable for ACL2 because a symbol with~
                          ~%the name "ACL2-LOOP-ONLY" or "ACL2-METERING" is ~
                          a member of *FEATURES*."))))

(defparameter *acl2-panic-exit-status* nil)

(defvar *acl2-exit-lisp-hook* nil)

(defun exit-lisp
  (&optional (status '0 status-p))
  (when (fboundp *acl2-exit-lisp-hook*)
    (funcall *acl2-exit-lisp-hook* status)
    (setq *acl2-exit-lisp-hook* nil))
  (cond ((null status) (error "Passed null status to exit-lisp!"))
    (*acl2-panic-exit-status* (return-from exit-lisp nil)))
  (setq *acl2-panic-exit-status* status)
  (let ((sym (or (find-symbol "EXIT" 'sb-ext)
         (find-symbol "QUIT" 'sb-ext))))
    (cond ((or (null sym) (not (fboundp sym))) (error "No function named "EXIT" or "QUIT" is defined in the ~%~
                   "SB-EXT" package.  Perhaps you are using a very old or ~%~
                   very new version of SBCL.  If you are surprised by this ~%~
                   message, feel free to contact the ACL2 implementors."))
      ((equal (symbol-name sym) "EXIT") (if status-p
          (funcall sym :code status)
          (funcall sym)))
      (t (if status-p
          (funcall sym :unix-status status)
          (funcall sym)))))
  (progn status-p status))

(defmacro exit-with-build-error
  (str &rest args)
  (let ((prefix "~%***** ERROR ******~%ACL2 build error: ") (suffix "~%******************~%"))
    (declare (ignorable prefix suffix))
    `(progn (format t (concatenate 'string ,PREFIX ,STR ,SUFFIX) ,@ARGS)
      (exit-lisp 1))))

(defmacro with-redefinition-suppressed
  (&rest forms)
  `(let nil
    ,@FORMS))

(defmacro with-warnings-suppressed
  (&rest forms)
  `(handler-bind ((warning (lambda (c)
         (declare (ignore c))
         (invoke-restart 'muffle-warning))))
    ,@FORMS))

(defmacro with-more-warnings-suppressed
  (&rest forms)
  (if (cdr forms)
    `(progn ,@FORMS)
    (car forms)))

(defmacro with-suppression
  (&rest forms)
  `(with-unlocked-packages ("COMMON-LISP")
    (with-warnings-suppressed ,@FORMS)))

(defconstant *acl2-status-file*
  (make-pathname :name "acl2-status" :type "txt"))

(defun check-suitability-for-acl2
  nil
  (with-warnings-suppressed (or (not (probe-file *acl2-status-file*))
      (delete-file *acl2-status-file*))
    (load "acl2-check.lisp")
    t))

(defun note-compile-ok
  nil
  (progn (or (not (probe-file *acl2-status-file*))
      (delete-file *acl2-status-file*))
    (with-open-file (str *acl2-status-file* :direction :output)
      (format str
        "~s"
        (if *suppress-compile-build-time*
          :compile-skipped :compiled)))))

(defvar *lisp-extension* "lisp")

(declaim (muffle-conditions compiler-note))

(defmacro our-with-compilation-unit
  (form)
  `(with-compilation-unit nil ,FORM))

(defconstant *acl2-read-character-terminators*
  '(#\	 #\
 #\ #\  #\" #\' #\( #\) #\; #\` #\,))

(our-with-compilation-unit (progn (load "acl2-fns.lisp")
    (let ((acl2-fns-compiled (make-pathname :name "acl2-fns"
           :type *compiled-file-extension*)))
      (when (probe-file acl2-fns-compiled)
        (delete-file acl2-fns-compiled))
      (when (not *suppress-compile-build-time*)
        (compile-file "acl2-fns.lisp")
        (load acl2-fns-compiled)))))

(or (member :ieee-floating-point *features*)
  (let ((x (getenv$-raw "ACL2_FP_OK")))
    (and x (not (equal x ""))))
  (error "This Lisp may be unsuitable for ACL2 because feature~%~
            :ieee-floating-point is missing.  This is easily fixed~%~
            by setting environment variable ACL2_FP_OK to t, but at~%~
            some risk of unsoundness; see :DOC fp."))

(or (equal (rational (float 0 0.0)) 0)
  (error "This Lisp is unsuitable for ACL2, because it failed~%~
            the sanity check that ~s."
    '(equal (rational (float 0 0.0)) 0)))

(or (equal (float-radix 1.0) 2)
  (error "This Lisp is unsuitable for ACL2, because it failed~%~
            the sanity check that ~s."
    '(equal (float-radix 1.0) 2)))

(defun break-on-overflow-and-nan
  nil
  (set-floating-point-modes :traps '(:overflow :invalid :divide-by-zero)
    :rounding-mode :nearest)
  nil)

(break-on-overflow-and-nan)

(unless (and (let ((*my-most-positive-double-float* most-positive-double-float))
      (declare (special *my-most-positive-double-float*))
      (typep (handler-case (* *my-most-positive-double-float*
            *my-most-positive-double-float*)
          (error nil 0.0))
        'double-float))
    (member :overflow (cadr (member :traps (get-floating-point-modes)))))
  (error "This Lisp is unsuitable for ACL2, because it failed ~%a check that ~
          floating-point overflow causes an error."))

(defparameter *acl2-readtable*
  (copy-readtable nil)
  "*acl2-readtable* is the readtable we use (a) to restrict the use of
#. to cause evaluation during READing (b) and to define our own version
of backquote.")

(defparameter *host-readtable*
  (copy-readtable)
  "*host-readtable* is the original readtable provided by the host Lisp,
which is saved just in case it's needed later.")

(defun set-new-dispatch-macro-character
  (char subchar fn)
  (let ((old (get-dispatch-macro-character char subchar)))
    (cond ((or (null old) (eql fn old)) (set-dispatch-macro-character char subchar fn))
      (t (error "ACL2 cannot be built in this host Lisp, because ~%~
                     ~s is already defined, to be: ~s"
          `(get-dispatch-macro-character ,CHAR ,SUBCHAR)
          old)))))

(defun define-sharp-dot
  nil
  (set-dispatch-macro-character #\# #\. (function sharp-dot-read)))

(defun define-sharp-bang
  nil
  (set-new-dispatch-macro-character #\# #\! (function sharp-bang-read)))

(defun define-sharp-u
  nil
  (set-new-dispatch-macro-character #\# #\u (function sharp-u-read)))

(defun define-sharp-f
  nil
  (set-new-dispatch-macro-character #\# #\f (function sharp-f-read)))

(defun define-sharp-d
  nil
  (set-new-dispatch-macro-character #\# #\d (function sharp-d-read)))

(defvar *old-character-reader*
  (get-dispatch-macro-character #\# #\\))

(defun modify-acl2-readtable
  (do-all-changes)
  (let ((*readtable* *acl2-readtable*))
    (set-new-dispatch-macro-character #\#
      #\{
      'fancy-string-reader-macro)
    (set-new-dispatch-macro-character #\#
      #\Z
      'ser-hons-reader-macro)
    (set-new-dispatch-macro-character #\#
      #\Y
      'ser-cons-reader-macro)
    (set-macro-character #\`
      (function (lambda (stream char)
          (declare (ignore char))
          (let ((*backquote-counter* (1+ *backquote-counter*)))
            `(read stream t nil t)))))
    (set-macro-character #\,
      (function (lambda (stream char)
          (declare (ignore char))
          (let ((*backquote-counter* (1- *backquote-counter*)))
            (acl2-comma-reader stream)))))
    (when do-all-changes
      (define-sharp-dot)
      (define-sharp-bang)
      (define-sharp-u)
      (define-sharp-f)
      (define-sharp-d))
    (when do-all-changes
      (set-dispatch-macro-character #\#
        #\\
        (function acl2-character-reader)))))

(eval-when (:load-toplevel :execute :compile-toplevel)
  (modify-acl2-readtable t))

(defvar *reckless-acl2-readtable*
  (let ((*readtable* (copy-readtable *acl2-readtable*)))
    (set-dispatch-macro-character #\#
      #\#
      (function reckless-sharp-sharp-read))
    (set-dispatch-macro-character #\#
      #\=
      (function reckless-sharp-equal-read))
    (set-dispatch-macro-character #\#
      #\\
      *old-character-reader*)
    *readtable*))

(defun non-trivial-acl2-proclaims-file-p
  nil
  (with-open-file (str "acl2-proclaims.lisp"
      :direction :input :if-does-not-exist nil)
    (and str
      (let* ((new-cons (cons nil nil)) (val (read str nil new-cons)))
        (and (not (eq new-cons val))
          (not (eq new-cons (read str nil new-cons))))))))

(defun compile-acl2
  (&optional use-acl2-proclaims)
  (when (and use-acl2-proclaims (not *do-proclaims*))
    (return-from compile-acl2 nil))
  (proclaim-optimize)
  (with-warnings-suppressed (cond (use-acl2-proclaims (cond ((non-trivial-acl2-proclaims-file-p) (load "acl2-proclaims.lisp"))
          (t (error "Note: For the call ~s, generated file ~
                         "acl2-proclaims.lisp" is missing or has no forms ~
                         in it."
              `(compile-acl2 ,USE-ACL2-PROCLAIMS))))))
    (unless (and (probe-file *acl2-status-file*)
        (with-open-file (str *acl2-status-file* :direction :input)
          (member (read str nil) '(:compiled :compile-skipped))))
      (check-suitability-for-acl2))
    (when (not *suppress-compile-build-time*)
      (let ((*readtable* *acl2-readtable*))
        (our-with-compilation-unit (dolist (name *acl2-files*)
            (or (equal name "defpkgs")
              (let ((source (make-pathname :name name :type *lisp-extension*)))
                (load source)
                (or (equal name "proof-builder-pkg")
                  (progn (compile-file source)
                    (load-compiled (make-pathname :name name :type *compiled-file-extension*))))))))))
    (note-compile-ok)))

(defun load-acl2
  (&key fast load-acl2-proclaims)
  (declare (ignorable fast))
  (proclaim-optimize)
  (our-with-compilation-unit (with-warnings-suppressed (when load-acl2-proclaims
        (cond ((non-trivial-acl2-proclaims-file-p) (load "acl2-proclaims.lisp"))
          (t (error "Expected non-trivial file acl2-proclaims.lisp!"))))
      (when (or (not (probe-file *acl2-status-file*))
          (with-open-file (str *acl2-status-file* :direction :input)
            (not (member (read str nil)
                '(:compiled :compile-skipped :initialized)))))
        (error "Please run ~s, which will write the token ~s to the file ~
              acl2-status.txt."
          '(compile-acl2)
          (if *suppress-compile-build-time*
            :compiled :compile-skipped)))
      (let ((*readtable* *acl2-readtable*) (extension (if *suppress-compile-build-time*
              *lisp-extension*
              *compiled-file-extension*)))
        (dolist (name *acl2-files*)
          (or (equal name "defpkgs")
            (if (equal name "proof-builder-pkg")
              (load "proof-builder-pkg.lisp")
              (load-compiled (make-pathname :name name :type extension)))))
        (load "defpkgs.lisp")
        (in-package "ACL2")
        (set 'state *the-live-state*)
        "ACL2"))))

(declaim (declaration xargs))

(declaim (declaration irrelevant))

(defconstant *slashable-array*
  (let ((ar (make-array 256 :initial-element nil)))
    (loop for
      i
      in
      '(0 1
        2
        3
        4
        5
        6
        7
        8
        9
        10
        11
        12
        13
        14
        15
        16
        17
        18
        19
        20
        21
        22
        23
        24
        25
        26
        27
        28
        29
        30
        31
        32
        34
        35
        39
        40
        41
        44
        58
        59
        92
        96
        97
        98
        99
        100
        101
        102
        103
        104
        105
        106
        107
        108
        109
        110
        111
        112
        113
        114
        115
        116
        117
        118
        119
        120
        121
        122
        124
        127
        128
        129
        130
        131
        132
        133
        134
        135
        136
        137
        138
        139
        140
        141
        142
        143
        144
        145
        146
        147
        148
        149
        150
        151
        152
        153
        154
        155
        156
        157
        158
        159
        160
        168
        170
        175
        178
        179
        180
        181
        184
        185
        186
        188
        189
        190
        223
        224
        225
        226
        227
        228
        229
        230
        231
        232
        233
        234
        235
        236
        237
        238
        239
        240
        241
        242
        243
        244
        245
        246
        248
        249
        250
        251
        252
        253
        254
        255)
      do
      (setf (aref ar i) t))
    ar))

(defconstant *suspiciously-first-numeric-array*
  (let ((ar (make-array 256 :initial-element nil)))
    (dolist (x '(#\0 #\1
          #\2
          #\3
          #\4
          #\5
          #\6
          #\7
          #\8
          #\9
          #\+
          #\-
          #\.
          #\^
          #\_))
      (setf (aref ar (char-code x)) t))
    ar))

(defconstant *suspiciously-first-hex-array*
  (let ((ar (make-array 256 :initial-element nil)))
    (dolist (x '(#\0 #\1
          #\2
          #\3
          #\4
          #\5
          #\6
          #\7
          #\8
          #\9
          #\A
          #\B
          #\C
          #\D
          #\E
          #\F
          #\a
          #\b
          #\c
          #\d
          #\e
          #\f
          #\+
          #\-
          #\.
          #\^
          #\_))
      (setf (aref ar (char-code x)) t))
    ar))

(defconstant *base-10-array*
  (let ((ar (make-array 256 :initial-element nil)))
    (dolist (x '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9))
      (setf (aref ar (char-code x)) t))
    ar))

(defconstant *hex-array*
  (let ((ar (make-array 256 :initial-element nil)))
    (dolist (x '(#\0 #\1
          #\2
          #\3
          #\4
          #\5
          #\6
          #\7
          #\8
          #\9
          #\A
          #\B
          #\C
          #\D
          #\E
          #\F
          #\a
          #\b
          #\c
          #\d
          #\e
          #\f))
      (setf (aref ar (char-code x)) t))
    ar))

(defconstant *letter-array*
  (let ((ar (make-array 256 :initial-element nil)))
    (dolist (ch '(#\A #\B
          #\C
          #\D
          #\E
          #\F
          #\G
          #\H
          #\I
          #\J
          #\K
          #\L
          #\M
          #\N
          #\O
          #\P
          #\Q
          #\R
          #\S
          #\T
          #\U
          #\V
          #\W
          #\X
          #\Y
          #\Z
          #\a
          #\b
          #\c
          #\d
          #\e
          #\f
          #\g
          #\h
          #\i
          #\j
          #\k
          #\l
          #\m
          #\n
          #\o
          #\p
          #\q
          #\r
          #\s
          #\t
          #\u
          #\v
          #\w
          #\x
          #\y
          #\z))
      (setf (aref ar (char-code ch)) t))
    ar))

(defmacro suspiciously-first-numeric-array
  (print-base)
  `(if (eql ,PRINT-BASE 16)
    *suspiciously-first-hex-array*
    *suspiciously-first-numeric-array*))

(defmacro numeric-array
  (print-base)
  `(if (eql ,PRINT-BASE 16)
    *hex-array*
    *base-10-array*))

(defconstant *char-code-backslash* (char-code #\\))

(defconstant *char-code-slash* (char-code #\/))

(defconstant *char-code-double-gritch* (char-code #\"))

(defconstant *big-n-special-object* '(nil))

(defconstant *number-of-return-values* 32)

(defconstant *boole-array*
  (let ((ar (make-array 16 :element-type 'fixnum)) (i 0))
    (declare (type (simple-array fixnum (*)) ar))
    (dolist (x `((boole-1 . ,BOOLE-1) (boole-2 . ,BOOLE-2)
          (boole-and . ,BOOLE-AND)
          (boole-andc1 . ,BOOLE-ANDC1)
          (boole-andc2 . ,BOOLE-ANDC2)
          (boole-c1 . ,BOOLE-C1)
          (boole-c2 . ,BOOLE-C2)
          (boole-clr . ,BOOLE-CLR)
          (boole-eqv . ,BOOLE-EQV)
          (boole-ior . ,BOOLE-IOR)
          (boole-nand . ,BOOLE-NAND)
          (boole-nor . ,BOOLE-NOR)
          (boole-orc1 . ,BOOLE-ORC1)
          (boole-orc2 . ,BOOLE-ORC2)
          (boole-set . ,BOOLE-SET)
          (boole-xor . ,BOOLE-XOR)))
      (or (typep (cdr x) 'fixnum)
        (error "We expected the value of ~s to be a fixnum, but it is ~s!"
          (car x)
          (cdr x)))
      (setf (aref ar i) (cdr x))
      (incf i))
    ar))

(progn (defconstant *mf-old-caller* (make-symbol "OLD-CALLER"))
  (defconstant *mf-start-pons* (make-symbol "START-PONS"))
  (defconstant *mf-start-bytes* (make-symbol "START-BYTES"))
  (defconstant *mf-ans* (make-symbol "ANS"))
  (defconstant *mf-ans-p* (make-symbol "ANS-P"))
  (defconstant *mf-ma* (make-symbol "MA"))
  (defconstant *mf-args* (make-symbol "ARGS"))
  (defconstant *mf-2mmf* (make-symbol "MF-2MMF"))
  (defconstant *mf-2mmf-fnn* (make-symbol "MF-2MMF-FNN"))
  (defconstant *mf-count-loc* (make-symbol "MF-COUNT-LOC"))
  (defconstant *attached-fn-temp*
    (make-symbol "ATTACHED-FN-TEMP")))