acl2-check

(in-package "ACL2")

(or (equal (length "ab
cd")
    5)
  (error "We have tested that the string ab\ncd (where \n denotes
a Newline character) has length 5, but it does not.  Perhaps your system
is using two characters to indicate a new line?"))

(dolist (name lambda-list-keywords)
  (cond ((let ((s (symbol-name name)))
       (or (= (length s) 0) (not (eql (char s 0) #\&)))) (error "We assume that all lambda-list-keywords start with the ~
                  character #&.~%However, ~s does not.  ACL2 will not work in ~
                  this Common Lisp."
        name))))

(or (and (integerp char-code-limit)
    (<= 256 char-code-limit)
    (typep 256 'fixnum))
  (error "We assume that 256 is a fixnum not exceeding char-code-limit, for ~
            purposes of~%character manipulation.  ACL2 will not work in this ~
            Common Lisp."))

(or (equal (symbol-name 'a) "A")
  (error "This Common Lisp image appears to be case-sensitive:~%~
            (equal (symbol-name 'a) "A") evaluates to NIL.~%~
            It is therefore not suitable for ACL2."))

(let ((filename "acl2-characters"))
  (with-open-file (str filename :direction :input)
    (loop for
      i
      from
      0
      to
      255
      do
      (let ((temp (read-char str)))
        (when (not (eql (char-code temp) i))
          (error "Bad character in file ~s: character ~s at position ~s."
            filename
            (char-code temp)
            i))))))

(loop for
  pair
  in
  (pairlis '(#\  #\	 #\
 #\ #\ #\
)
    '(32 9 10 12 127 13))
  do
  (let* ((ch (car pair)) (code (cdr pair)) (val (char-code ch)))
    (or (eql val code)
      (error "(char-code ~s) evaluated to ~s (expected ~s)."
        ch
        val
        code))))

(dotimes (i 256)
  (let ((ch (code-char i)))
    (or (equal (standard-char-p ch)
        (or (= i 10) (and (>= i 32) (<= i 126))))
      (let ((v (lisp-implementation-version)))
        (when (and (string<= "2.4.2" v) (string< v "2.4.2.46"))
          (exit-with-build-error "Please avoid SBCL versions 2.4.2 through ~
                     2.4.2.45.~%Instead use a later SBCL version --~%2.4.3 or ~
                     later or, for example, the latest from GitHub --~%or ~
                     else SBCL version 2.4.1 or earlier.~%(Technical reason: ~
                     function standard-char-p does not return t on ~
                     a~%standard character input, but instead returns the ~
                     input character.)")))
      (exit-with-build-error "This Common Lisp is unsuitable for ACL2 because the ~
                 character~%with char-code ~d ~a standard in this Common Lisp ~
                 but should~%~abe."
        i
        (if (standard-char-p ch)
          "is"
          "is not")
        (if (standard-char-p ch)
          "not "
          "")))))

(dotimes (i 256)
  (let ((ch (code-char i)))
    (or (not (standard-char-p ch))
      (eql (char-downcase ch)
        (if (and (>= i 65) (<= i 90))
          (code-char (+ i 32))
          ch))
      (exit-with-build-error "This Common Lisp is unsuitable for ACL2 because ~
                 (char-downcase ~s)~%is ~s but should be ~s."
        ch
        (char-downcase ch)
        (if (and (>= i 65) (<= i 90))
          (code-char (+ i 32))
          ch)))))

(dotimes (i 256)
  (let ((ch (code-char i)))
    (or (not (standard-char-p ch))
      (eql (char-upcase ch)
        (if (and (>= i 97) (<= i 122))
          (code-char (- (char-code ch) 32))
          ch))
      (exit-with-build-error "This Common Lisp is unsuitable for ACL2 because (char-upcase ~
                 ~s)~%is ~s but should be ~s."
        ch
        (char-upcase ch)
        (if (and (>= i 65) (<= i 90))
          (code-char (- (char-code ch) 32))
          ch)))))

(dotimes (i 256)
  (let ((ch (code-char i)) bad)
    (unless (equal (standard-char-p (char-upcase ch))
        (standard-char-p ch))
      (setq bad 0))
    (unless (equal (standard-char-p (char-downcase ch))
        (standard-char-p ch))
      (setq bad 1))
    (unless (or (not (upper-case-p ch))
        (equal (char-upcase (char-downcase ch)) ch))
      (setq bad 2))
    (unless (or (not (lower-case-p ch))
        (equal (char-downcase (char-upcase ch)) ch))
      (setq bad 3))
    (when bad
      (exit-with-build-error "This Common Lisp is unsuitable for ACL2 because the~%~
        following test failed for the character ch = (code-char ~s):~%~s~a"
        i
        (case bad
          (0 '(equal (standard-char-p (char-upcase ch))
              (standard-char-p ch)))
          (1 '(equal (standard-char-p (char-downcase ch))
              (standard-char-p ch)))
          (2 '(or (not (upper-case-p ch))
              (equal (char-upcase (char-downcase ch)) ch)))
          (3 '(or (not (lower-case-p ch))
              (equal (char-downcase (char-upcase ch)) ch)))
          (otherwise "Implementation Error!   Please contact the ACL2 implementors."))
        ""))))

(or (typep array-dimension-limit 'fixnum)
  (exit-with-build-error "We assume that ARRAY-DIMENSION-LIMIT is a fixnum.  CLTL2 requires ~
      this.~%ACL2 will not work in this Common Lisp."))

(or (>= multiple-values-limit *number-of-return-values*)
  (exit-with-build-error "We assume that multiple-values-limit is at least ~s, but in this Common ~
      Lisp its value is ~s.  Please contact the ACL2 implementors about ~
      lowering the value of ACL2 constant *NUMBER-OF-RETURN-VALUES*."
    multiple-values-limit
    *number-of-return-values*))

(let ((badvars nil))
  (dolist (var *copy-of-common-lisp-symbols-from-main-lisp-package*)
    (or (member var
        *copy-of-common-lisp-specials-and-constants*
        :test (function eq))
      (if (and (let ((s (symbol-name var)))
            (or (= (length s) 0) (not (eql (char s 0) #\&))))
          (eval `(let ((,VAR (gensym)))
              (and (boundp ',VAR) (eq ,VAR (symbol-value ',VAR))))))
        (setq badvars (cons var badvars)))))
  (if badvars
    (exit-with-build-error "The following constants or special variables in the main~%Lisp ~
        package needs to be included in the ~
        list~%*common-lisp-specials-and-constants*:~%~s."
      badvars)))

(format t "Check completed.~%")