other
(in-package "ACL2")
sharp-atsign-read-ermacro
(defmacro sharp-atsign-read-er (str &rest format-args) `(progn (loop (when (null (read-char-no-hang stream nil nil t)) (return))) (error (concatenate 'string ,STR ". See :DOC set-iprint.") ,@FORMAT-ARGS)))
sharp-atsign-readfunction
(defun sharp-atsign-read (stream char n &aux (state *the-live-state*)) (declare (ignore char n)) (let (ch bad-ch (zero-code (char-code #\0)) (index 0) (iprint-last-index (iprint-last-index state))) (loop (when (eql (setq ch (read-char stream t nil t)) #\#) (return)) (let ((digit (- (char-code ch) zero-code))) (cond ((or (< digit 0) (> digit 9)) (when (not bad-ch) (setq bad-ch ch)) (return)) (t (setq index (+ digit (* 10 index))))))) (cond (bad-ch (sharp-atsign-read-er "Non-digit character ~s following #@~s" bad-ch index)) ((f-get-global 'certify-book-info state) (sharp-atsign-read-er "Illegal use of #@ reader macro during certify-book, #@~s#" index)) ((iprint-ar-illegal-index index state) (sharp-atsign-read-er "Out-of-bounds index in #@~s#" index)) (t (let ((old-read-state *iprint-read-state*)) (cond ((eq old-read-state nil) (iprint-ar-aref1 index state)) (t (let ((new-read-state-order (if (<= index iprint-last-index) '<= '>))) (cond ((eq old-read-state t) (setq *iprint-read-state* (cons index new-read-state-order)) (iprint-ar-aref1 index state)) ((eq (cdr old-read-state) new-read-state-order) (iprint-ar-aref1 index state)) (t (multiple-value-bind (index-before index-after) (cond ((eq (cdr old-read-state) '<=) (values index (car old-read-state))) (t (values (car old-read-state) index))) (sharp-atsign-read-er "Attempt to read a form containing both an index~%~ created before the most recent rollover (#@~s#) and~%~ an index created after that rollover (#@~s#)" index-before index-after))))))))))))
define-sharp-atsignfunction
(defun define-sharp-atsign nil (set-new-dispatch-macro-character #\# #\@ (function sharp-atsign-read)))
other
(eval-when (:load-toplevel :execute) (when (compiled-function-p! 'sharp-atsign-read) (let ((*readtable* *acl2-readtable*)) (define-sharp-atsign))))
gvmacro
(defmacro gv (fn args val) (sublis `((funny-fn . ,FN) (funny-args . ,ARGS)) `(let ((gc-on (not (gc-off *the-live-state*)))) (if (or gc-on (f-get-global 'safe-mode *the-live-state*)) (throw-raw-ev-fncall (list 'ev-fncall-guard-er 'funny-fn ,(CONS 'LIST 'FUNNY-ARGS) (guard-raw 'funny-fn (w *the-live-state*)) (stobjs-in 'funny-fn (w *the-live-state*)) (not gc-on))) ,VAL))))
other
(defun-*1* mv-list (input-arity x) (declare (ignore input-arity)) x)
other
(defun-*1* return-last (fn x y) (cond ((and (equal fn 'mbe1-raw) (f-get-global 'safe-mode *the-live-state*)) (if (equal x y) y (gv return-last (fn x y) y))) (t y)))
other
(defun-*1* wormhole-eval (qname qlambda free-vars) (declare (ignore qname qlambda free-vars)) nil)
other
(defun-*1* acl2-numberp (x) (numberp x))
other
(defun-*1* binary-* (x y) (the number (if (numberp x) (if (numberp y) (* x y) (gv binary-* (x y) 0)) (gv binary-* (x y) 0))))
other
(defun-*1* binary-+ (x y) (the number (if (numberp x) (if (numberp y) (+ (the number x) (the number y)) (gv binary-+ (x y) x)) (gv binary-+ (x y) (if (numberp y) y 0)))))
other
(defun-*1* unary-/ (x) (the number (if (and (numberp x) (not (= x 0))) (/ x) (gv unary-/ (x) 0))))
other
(defun-*1* < (x y) (if (and (rationalp x) (rationalp y)) (< (the rational x) (the rational y)) (gv < (x y) (let ((x1 (if (numberp x) x 0)) (y1 (if (numberp y) y 0))) (or (< (realpart x1) (realpart y1)) (and (= (realpart x1) (realpart y1)) (< (imagpart x1) (imagpart y1))))))))
other
(defun-*1* apply
(x y)
(error "We have called apply on ~s and ~s, but we thought we were rid of apply."
x
y))
other
(defun-*1* bad-atom<= (x y) (cond ((and (bad-atom x) (bad-atom y)) (error "We have called (the executable-counterpart of) bad-atom<= on ~ ~s and ~s, but bad-atom<= has no Common Lisp definition." x y)) (t (gv bad-atom<= (x y) nil))))
other
(defun-*1* char-code
(x)
(if (characterp x)
(char-code x)
(gv char-code (x) 0)))
other
(defun-*1* characterp (x) (characterp x))
other
(defun-*1* code-char (x) (if (and (integerp x) (>= x 0) (< x 256)) (code-char x) (gv code-char (x) *null-char*)))
other
(defun-*1* complex (x y) (complex (the rational (if (rationalp x) x (gv complex (x y) 0))) (the rational (if (rationalp y) y (gv complex (x y) 0)))))
other
(defun-*1* complex-rationalp (x) (complexp x))
other
(defun-*1* coerce (x y) (cond ((equal y 'list) (if (stringp x) (coerce x 'list) (gv coerce (x y) nil))) ((character-listp x) (if (equal y 'string) (coerce x 'string) (gv coerce (x y) (coerce x 'string)))) (t (gv coerce (x y) (coerce (make-character-list x) 'string)))))
other
(defun-*1* cons (x y) (cons x y))
other
(defun-*1* consp (x) (consp x))
other
(defun-*1* denominator
(x)
(if (rationalp x)
(denominator x)
(gv denominator (x) 1)))
other
(defun-*1* equal (x y) (equal x y))
other
(defun-*1* if (x y z) (error "We just can't stand having a non-lazy IF around. But we attempted ~%~ to call the executable-counterpart of IF on argument list ~s." (list x y z)))
other
(defun-*1* imagpart
(x)
(if (numberp x)
(imagpart x)
(gv imagpart (x) 0)))
other
(defun-*1* integerp (x) (integerp x))
other
(defun-*1* intern-in-package-of-symbol (x y) (if (and (stringp x) (symbolp y)) (intern-in-package-of-symbol x y) (gv intern-in-package-of-symbol (x y) nil)))
other
(defun-*1* pkg-imports
(pkg)
(if (stringp pkg)
(pkg-imports pkg)
(gv pkg-imports (pkg) nil)))
other
(defun-*1* pkg-witness
(pkg)
(if (stringp pkg)
(pkg-witness pkg)
(gv pkg-witness (pkg) (intern *pkg-witness-name* "ACL2"))))
other
(defun-*1* numerator
(x)
(if (rationalp x)
(numerator x)
(gv numerator (x) 0)))
other
(defun-*1* rationalp (x) (rationalp x))
other
(defun-*1* realpart
(x)
(if (numberp x)
(realpart x)
(gv realpart (x) 0)))
other
(defun-*1* stringp (x) (stringp x))
other
(defun-*1* symbol-name
(x)
(if (symbolp x)
(symbol-name x)
(gv symbol-name (x) "")))
other
(defun-*1* symbol-package-name
(x)
(if (symbolp x)
(progn (chk-bad-lisp-object x) (symbol-package-name x))
(gv symbol-package-name (x) "")))
other
(defun-*1* symbolp (x) (symbolp x))
other
(defun-*1* apply$-lambda (fn args) (declare (ftype (function (t t) (values t)) ev$)) (if (apply$-lambda-guard fn args) (apply$-lambda fn args) (gv apply$-lambda (fn args) (apply$-lambda-logical fn args))))
other
(defun-one-output macroexpand1! (x) (mv-let (erp val state) (macroexpand1 x 'oneify *the-live-state*) (declare (ignore erp state)) val))
oneified-stobj-let-actualsfunction
(defun oneified-stobj-let-actuals (actuals creators fns w program-p) (cond ((endp actuals) nil) (t (cons (cond ((car creators) (let ((actual (car actuals))) (case-match actual ((tbl-get ('quote st) parent (create-st)) `(or ,(ONEIFY `(,TBL-GET ',ST ,PARENT NIL) FNS W PROGRAM-P) (,CREATE-ST))) (& (er hard 'oneified-stobj-let-actuals "Implementation error: unexpected stobj-let ~ actual, ~x0. Please contact the ACL2 ~ implementors." actual))))) (t (oneify (car actuals) fns w program-p))) (oneified-stobj-let-actuals (cdr actuals) (cdr creators) fns w program-p)))))
stobj-let-fn-oneifyfunction
(defun stobj-let-fn-oneify (x fns w program-p) (mv-let (msg bound-vars actuals creators stobj producer-vars producer updaters bindings consumer) (parse-stobj-let x) (declare (ignore bindings)) (cond (msg (mv (er hard 'stobj-let "~@0" msg) nil nil nil nil)) (t (let* ((oneified-producer (oneify producer fns w program-p)) (oneified-consumer (oneify consumer fns w program-p)) (oneified-updaters (oneify-lst updaters fns w program-p)) (updated-oneified-consumer `(let* ,(PAIRLIS-X1 STOBJ (PAIRLIS$ ONEIFIED-UPDATERS NIL)) ,ONEIFIED-CONSUMER)) (oneified-actuals (oneified-stobj-let-actuals actuals creators fns w program-p)) (form `(let (,@(PAIRLIS$ BOUND-VARS (PAIRLIS$ ONEIFIED-ACTUALS NIL))) (declare (ignorable ,@BOUND-VARS)) ,(COND ((CDR PRODUCER-VARS) `(MV-LET ,PRODUCER-VARS ,ONEIFIED-PRODUCER ,UPDATED-ONEIFIED-CONSUMER)) (T `(LET ((,(CAR PRODUCER-VARS) ,ONEIFIED-PRODUCER)) ,UPDATED-ONEIFIED-CONSUMER)))))) (mv form bound-vars actuals creators producer-vars stobj w))))))
oneify-flet-bindingsmutual-recursion
(mutual-recursion (defun-one-output oneify-flet-bindings (alist fns w program-p) (cond ((endp alist) nil) (t (cons (let* ((def (car alist)) (dcls (append-lst (strip-cdrs (remove-strings (butlast (cddr def) 1))))) (ignore-vars (ignore-vars dcls)) (guardian (conjoin-untranslated-terms (loop for dcl in dcls when (eq (car dcl) 'type) append (loop with pred = (cadr dcl) for var in (cddr dcl) collect (oneify `(the ,PRED ,VAR) fns w program-p))))) (oneified-body0 (oneify (car (last def)) fns w program-p)) (oneified-body (if (eq guardian t) oneified-body0 `(progn ,GUARDIAN ,ONEIFIED-BODY0)))) (list* (*1*-symbol (car def)) (cadr def) (if ignore-vars (list `(declare (ignore ,@IGNORE-VARS)) oneified-body) (list oneified-body)))) (oneify-flet-bindings (cdr alist) fns w program-p))))) (defun remove-type-dcls (dcls) (let* ((alist nil) (new-dcls (loop for dcl in dcls as dcl2 = (assert$ (and (consp dcl) (eq (car dcl) 'declare)) (cond ((assoc-eq 'type (cdr dcl)) (let ((dcl2-body (loop for d in (cdr dcl) when (cond ((eq (car d) 'type) (let ((tp (cadr d))) (case-match tp (('or 't . &) nil) (& (loop for v in (cddr d) collect (push `(,TP . ,V) alist))))) nil) (t t)) collect d))) (and dcl2-body (cons 'declare dcl2-body)))) (t dcl))) when dcl2 collect dcl2))) (values new-dcls alist))) (defun alist-to-the-for-*1*-lst (type-to-var-alist) (cond ((endp type-to-var-alist) nil) (t (cons `(the-for-*1* ,(CAAR TYPE-TO-VAR-ALIST) ,(CDAR TYPE-TO-VAR-ALIST)) (alist-to-the-for-*1*-lst (cdr type-to-var-alist)))))) (defconst *touchable-state-vars* (default-state-vars nil :temp-touchable-vars t :temp-touchable-fns t)) (defun remove-double-floats (stobjs-out-with-dfs *1*body check) (cond ((null (cdr stobjs-out-with-dfs)) (cond (check `(let ((x ,*1*BODY)) (if (typep x 'double-float) (rational x) x))) (t `(rational ,*1*BODY)))) (t (let ((xs (loop for s in stobjs-out-with-dfs as i from 0 collect (progn s (packn (list 'x i)))))) `(multiple-value-bind ,XS ,*1*BODY (values ,@(COND (CHECK (LOOP FOR S IN STOBJS-OUT-WITH-DFS AS X IN XS COLLECT (IF (EQ S :DF) `(IF (TYPEP ,X 'DOUBLE-FLOAT) (RATIONAL ,X) ,X) X))) (T (LOOP FOR S IN STOBJS-OUT-WITH-DFS AS X IN XS COLLECT (IF (EQ S :DF) `(RATIONAL ,X) X)))))))))) (defun-one-output oneify (x fns w program-p) (cond ((atom x) (cond ((keywordp x) (kwote x)) ((symbolp x) x) ((atom x) (kwote x)) (t x))) ((eq (car x) 'quote) (cond ((and (consp (cadr x)) (eq (car (cadr x)) 'lambda)) (mv-let (erp val) (hons-copy-lambda-object? x) (cond (erp (interface-er "~@0" val)) (t val)))) (t x))) ((eq (car x) 'lambda$) (mv-let (flg tx bindings) (translate11-lambda-object x t nil t nil x 'oneify w *touchable-state-vars* nil) (declare (ignore bindings)) (if flg (interface-er "Implementation error: Translate11-lambda-object in ~ oneify encountered an untranslatable LAMBDA$, ~x0, ~ even though it was supposedly translated ~ successfully earlier. Please contact the ACL2 ~ implementors." x) tx))) ((eq (car x) 'loop$) (mv-let (flg tx bindings) (translate11-loop$ x t nil t nil nil x 'oneify w *touchable-state-vars*) (declare (ignore bindings)) (if flg `(interface-er "Implementation error: translate11-loop$ in oneify ~ encountered an untranslatable LOOP$, ~x0. We ~ thought that this could only happen under a call of ~ non-exec, in which case we should never be ~ executing this code! Please contact the ACL2 ~ implementors." ',X) (let ((tmp (oneify tx fns w program-p)) (stobjs-out (loop$-stobjs-out x tx))) (cond ((cdr stobjs-out) `(values-list ,TMP)) (t tmp)))))) ((not (symbolp (car x))) (oneify (list* 'let (listlis (cadr (car x)) (cdr x)) (cddr (car x))) fns w program-p)) ((let ((pair (assoc-eq (car x) fns))) (and (cdr pair) (let* ((args (cadr pair)) (body (caddr pair)) (alist (mv-let (erp alist) (bind-macro-args args x w *touchable-state-vars*) (cond (erp (error "Implementation error: Unexpected error in ~ oneify:~%x = ~s~%fns = ~s" x fns)) (t alist)))) (expansion (eval `(let ,(LOOP FOR PAIR IN ALIST COLLECT (LIST (CAR PAIR) (KWOTE (CDR PAIR)))) ,BODY)))) (oneify expansion fns w program-p))))) ((eq (car x) 'return-last) (let* ((qfn (and (consp (cdr x)) (cadr x))) (return-last-fn (return-last-fn qfn)) (fn (or return-last-fn 'progn)) (arg2 (and (not (eq fn 'ec-call1-raw)) (return-last-arg2 return-last-fn (oneify (caddr x) fns w program-p))))) (cond ((eq fn 'ec-call1-raw) (cond ((not (eq program-p 'invariant-risk)) (oneify (car (last x)) fns w program-p)) (t (let ((form (car (last x)))) `(let* ((args (list ,@(ONEIFY-LST (CDR FORM) FNS W PROGRAM-P))) (**1*-as-raw* nil)) (apply ',(IF (FUNCTION-SYMBOLP (CAR FORM) W) (*1*-SYMBOL (CAR FORM)) (ASSERT$ (GETPROPC (CAR FORM) 'MACRO-BODY NIL W) (*1*-SYMBOL (ADD-SUFFIX (CAR FORM) *INLINE-SUFFIX*)))) args)))))) ((eq fn 'mbe1-raw) (let* ((oneified-logic-body (oneify (cadddr x) fns w program-p)) (oneified-exec-body arg2) (logic-fn (and (not program-p) (acl2-gentemp "ONEIFY"))) (exec-fn (acl2-gentemp "ONEIFY")) (logic-body (if program-p oneified-logic-body (list logic-fn)))) `(flet (,@(AND (NOT PROGRAM-P) `((,LOGIC-FN NIL ,ONEIFIED-LOGIC-BODY))) (,EXEC-FN nil ,ONEIFIED-EXEC-BODY)) (cond ((f-get-global 'safe-mode *the-live-state*) (,(*1*-SYMBOL 'RETURN-LAST) ,QFN (,EXEC-FN) ,LOGIC-BODY)) (t ,(IF PROGRAM-P `(,EXEC-FN) `(IF **1*-AS-RAW* (,EXEC-FN) ,LOGIC-BODY))))))) (t (list fn arg2 (oneify (cadddr x) fns w program-p)))))) ((or (member-eq (car x) *oneify-primitives*) (member-eq (car x) *macros-for-nonexpansion-in-raw-lisp*)) (let ((args (oneify-lst (cdr x) fns w program-p))) (cons (car x) args))) ((eq (car x) 'mv-let) (multiple-value-bind (dcls alist) (remove-type-dcls (butlast (cdddr x) 1)) (let* ((value-form (oneify (caddr x) fns w program-p)) (new-body (cond (alist `(progn$ ,@(ALIST-TO-THE-FOR-*1*-LST ALIST) ,(CAR (LAST X)))) (t (car (last x))))) (body-form (oneify new-body fns w program-p))) `(mv-let ,(CADR X) ,VALUE-FORM ,@DCLS ,BODY-FORM)))) ((eq (car x) 'flet) (list 'flet (oneify-flet-bindings (cadr x) fns w program-p) (oneify (car (last x)) (append (pairlis$ (strip-cars (cadr x)) nil) fns) w program-p))) ((eq (car x) 'macrolet) (oneify (car (last x)) (append (loop for tuple in (cadr x) collect (list* (car tuple) (cadr tuple) (last tuple))) fns) w program-p)) ((eq (car x) 'translate-and-test) (oneify (caddr x) fns w program-p)) ((eq (car x) 'with-local-stobj) (mv-let (erp st mv-let-form creator) (parse-with-local-stobj (cdr x)) (declare (ignore erp)) (mv-let-for-with-local-stobj mv-let-form st creator fns w program-p))) ((eq (car x) 'with-global-stobj) (let ((len (length x))) (case len (3 `(with-global-stobj ,(CADR X) ,(ONEIFY (CADDR X) FNS W PROGRAM-P))) (4 `(with-global-stobj ,(CADR X) ,(CADDR X) ,(ONEIFY (CADDDR X) FNS W PROGRAM-P))) (otherwise (error "Unexpected case for with-global-stobj,~|~x0" x))))) ((eq (car x) 'stobj-let) (mv-let (temp bound-vars actuals creators producer-vars stobj) (stobj-let-fn-oneify x fns w program-p) (let ((dups-check (no-duplicate-indices-checks-for-stobj-let-actuals bound-vars actuals creators producer-vars stobj w))) (cond (dups-check `(prog2$ (flet ((chk-no-stobj-index-aliasing (x1 x2) (,(*1*-SYMBOL 'CHK-NO-STOBJ-INDEX-ALIASING) x1 x2))) ,DUPS-CHECK) temp)) (t temp))))) ((member-eq (car x) '(let)) (let* ((args (cdr x)) (bindings (car args)) (post-bindings (cdr args))) (multiple-value-bind (dcls alist) (remove-type-dcls (butlast post-bindings 1)) (let* ((value-forms (oneify-lst (strip-cadrs bindings) fns w program-p)) (new-body (cond (alist `(progn$ ,@(ALIST-TO-THE-FOR-*1*-LST ALIST) ,(CAR (LAST POST-BINDINGS)))) (t (car (last post-bindings))))) (body-form (oneify new-body fns w program-p))) `(,(CAR X) ,(LISTLIS (STRIP-CARS BINDINGS) VALUE-FORMS) ,@DCLS ,BODY-FORM))))) ((eq (car x) 'throw-or-attach) (interface-er "Implementation error: Unexpected call of throw-or-attach in oneify:~%~x0" x)) ((and (getpropc (car x) 'macro-body nil w) (not (assoc-eq (car x) fns))) (oneify (macroexpand1! x) fns w program-p)) ((eq (car x) 'wormhole-eval) (let* ((qname (cadr x)) (qlambda (caddr x)) (formals (cadr (cadr qlambda))) (body (caddr (cadr qlambda)))) (cond ((not (or (variablep qname) (fquotep qname))) (interface-er "We thought that the name argument of every call of wormhole-eval in ~ the ACL2 source code was either a variable symbol or a quoted ~ constant. But oneify has encountered a call of wormhole-eval with ~ the term ~x0 in the wormhole name position. Out of sheer laziness, ~ oneify is not prepared to deal with such a call of wormhole-eval! ~ Please inform the ACL2 developers of this error and we'll fix it!" qname)) (t (list 'wormhole-eval qname (list 'quote (list 'lambda formals (oneify body fns w program-p))) *nil*))))) (t (let ((arg-forms (oneify-lst (cdr x) fns w program-p))) (cond ((and (eq program-p 'invariant-risk) (not (getpropc (car x) 'invariant-risk nil w))) (let ((stobjs-in (getpropc (car x) 'stobjs-in nil w))) (when (member-eq :df stobjs-in) (setq arg-forms (loop for arg in arg-forms as s in stobjs-in collect (if (eq s :df) `(to-df ,ARG) arg))))) (let ((stobjs-out (getpropc (car x) 'stobjs-out nil w))) (if (member-eq :df stobjs-out) (remove-double-floats stobjs-out (cons (car x) arg-forms) nil) (cons (car x) arg-forms)))) (t (cons (*1*-symbol (car x)) arg-forms))))))) (defun-one-output oneify-lst (lst fns w program-p) (cond ((atom lst) nil) (t (let ((x (oneify (car lst) fns w program-p)) (y (oneify-lst (cdr lst) fns w program-p))) (cons x y))))))
other
(defun-one-output select-stobj (name stobjs terms) (cond ((endp stobjs) nil) ((eq name (car stobjs)) (car terms)) (t (select-stobj name (cdr stobjs) (cdr terms)))))
other
(defun-one-output super-defstobj-wart-stobjs-in (formals stobj-flag) (cond ((endp formals) nil) ((eq (car formals) stobj-flag) (cons stobj-flag (super-defstobj-wart-stobjs-in (cdr formals) stobj-flag))) (t (cons nil (super-defstobj-wart-stobjs-in (cdr formals) stobj-flag)))))
other
(defun-one-output oneify-fail-form (er-type fn formals guard super-stobjs-in wrld extra) `(throw-raw-ev-fncall (list ',ER-TYPE ',FN (list ,@FORMALS) ',GUARD ',(OR SUPER-STOBJS-IN (STOBJS-IN FN WRLD) (IF FORMALS (ER HARD 'ONEIFY-CLTL-CODE "I didn't think this could happen, but for fn = ~x0 ~ stobjs-in is nil and formals isn't." FN) NIL)) ,EXTRA)))
other
(defun-one-output get-declared-stobjs (edcls) (if (endp edcls) nil (union-eq (and (eq (caar edcls) 'xargs) (let ((stobjs (cadr (assoc-keyword :stobjs (cdar edcls))))) (cond ((symbol-listp stobjs) stobjs) ((and stobjs (symbolp stobjs)) (list stobjs)) (t nil)))) (get-declared-stobjs (cdr edcls)))))
maybe-warn-for-guard-bodyfunction
(defun maybe-warn-for-guard-body (fn state) (assert$ (f-get-global 'raw-guard-warningp state) (pprogn (f-put-global 'raw-guard-warningp nil state) (warning$ 'top-level "Guards" "Guard-checking will be inhibited for some ~ recursive calls, including ~x0; see :DOC ~ guard-checking-inhibited." fn))))
other
(defun-one-output create-live-user-stobjp-test (stobjs) (if (endp stobjs) t (let* ((stj (car stobjs)) (rst (create-live-user-stobjp-test (cdr stobjs))) (tst `(live-stobjp ,STJ))) (cond ((eq stj 'state) rst) ((eq rst t) tst) (t `(and ,TST ,RST))))))
labels-form-for-*1*function
(defun labels-form-for-*1* (fn *1*fn formals *1*body ignore-vars ignorable-vars super-stobjs-in super-stobjs-chk guard wrld) (let ((*1*fn-binding `(,*1*FN ,FORMALS ,@(AND IGNORE-VARS `((DECLARE (IGNORE ,@IGNORE-VARS)))) ,@(AND IGNORABLE-VARS `((DECLARE (IGNORABLE ,@IGNORABLE-VARS)))) ,@(AND SUPER-STOBJS-IN `((WHEN ,SUPER-STOBJS-CHK ,(ONEIFY-FAIL-FORM 'EV-FNCALL-GUARD-ER FN FORMALS GUARD SUPER-STOBJS-IN WRLD :LIVE-STOBJ)))) ,*1*BODY))) `(labels (,*1*FN-BINDING) (,*1*FN ,@FORMALS))))
df-callfunction
(defun df-call (fn formals) (let ((stobjs-in (stobjs-in fn (w *the-live-state*)))) (cons fn (loop for f in formals as s in stobjs-in collect (if (eq s :df) `(to-df ,F) f)))))
oneify-cltl-code-1function
(defun oneify-cltl-code-1 (defun-mode def stobj-flag wrld trace-rec-for-none) (when stobj-flag (cond ((null (cadr def)) (return-from oneify-cltl-code-1 `(,(*1*-SYMBOL (CAR DEF)) nil (throw-raw-ev-fncall (list 'ev-fncall-creator-er ',(CAR DEF)))))))) (when (null defun-mode) (return-from oneify-cltl-code-1 (case-match def ((fn formals ('declare ('xargs ':non-executable ':program)) ('throw-or-attach fn formals)) `(,(*1*-SYMBOL FN) ,FORMALS (throw-or-attach ,FN ,FORMALS t))) ((fn formals ('declare ('xargs ':guard guard)) ('throw-or-attach fn formals)) `(,(*1*-SYMBOL FN) ,FORMALS ,(COND ((OR (EQ GUARD T) (EQUAL GUARD *T*)) (CAR (LAST DEF))) (T `(THROW-OR-ATTACH ,FN ,FORMALS T))))) ((fn formals ('throw-or-attach fn formals)) (prog2$ formals `(,(*1*-SYMBOL FN) ,@(CDR DEF)))) ((fn formals ('throw-without-attach 'nil fn formals)) (prog2$ formals `(,(*1*-SYMBOL FN) ,@(CDR DEF)))) (& (interface-er "Implementation error: Oneify-cltl-code encountered ~ non-executable definition, ~x0, that was not what we ~ would expect to be generated by intro-udf-lst2." def))))) (mv-let (dcls guard) (dcls-guard-raw-from-def def wrld) (let* ((guard-is-t (and (or (eq guard t) (equal guard *t*)) (not (and stobj-flag (getpropc stobj-flag 'absstobj-info nil wrld))))) (fn (car def)) (*1*fn (*1*-symbol fn)) (cl-compliant-p-optimization (and (eq defun-mode :logic) (eq (symbol-class fn wrld) :common-lisp-compliant))) (formals (cadr def)) (optimize-dcls (loop with tmp = nil for tail on (cddr def) do (if (null (cdr tail)) (return (reverse tmp)) (and (consp (car tail)) (loop for pair in (cdr (car tail)) when (eq (car pair) 'optimize) do (push pair tmp)))))) (boot-strap-p (f-get-global 'boot-strap-flg *the-live-state*))) (cond ((or (and guard-is-t cl-compliant-p-optimization) (and boot-strap-p (member-eq fn *avoid-oneify-fns*))) `(,*1*FN ,FORMALS ,(CONS FN FORMALS))) (t (let* ((program-p (eq defun-mode :program)) (invariant-risk (and program-p (getpropc fn 'invariant-risk nil wrld))) (super-stobjs-in (if stobj-flag (let ((temp (super-defstobj-wart-stobjs-in formals stobj-flag))) (cond ((find-first-non-nil temp) temp) (t nil))) (cdr (assoc-eq fn *super-defun-wart-stobjs-in-alist*)))) (ignore-vars (and (not super-stobjs-in) (ignore-vars dcls))) (ignorable-vars (ignorable-vars dcls)) (stobjs-out (getpropc fn 'stobjs-out nil wrld)) (declared-stobjs (if stobj-flag (list stobj-flag) (get-declared-stobjs dcls))) (live-stobjp-test (create-live-user-stobjp-test declared-stobjs)) (body (car (last def))) (*1*body (oneify body nil wrld program-p)) (guard-checking-on-form (cond (super-stobjs-in '(let ((temp (f-get-global 'guard-checking-on *the-live-state*))) (cond ((gc-off1 temp) t) (t temp)))) (t '(f-get-global 'guard-checking-on *the-live-state*)))) (skip-early-exit-code-when-none (and (eq defun-mode :logic) (or (not boot-strap-p) (eq fn 'the-check)))) (guard-checking-is-really-on-form (cond (super-stobjs-in t) (skip-early-exit-code-when-none guard-checking-on-form) (t `(not (gc-off1 ,GUARD-CHECKING-ON-FORM))))) (fail_guard (oneify-fail-form 'ev-fncall-guard-er fn formals guard super-stobjs-in wrld (and super-stobjs-in '(cond ((gc-off1 (f-get-global 'guard-checking-on *the-live-state*)) :live-stobj) (t :live-stobj-gc-on))))) (fail_safe (oneify-fail-form 'ev-fncall-guard-er fn formals guard super-stobjs-in wrld t)) (safe-form '(f-get-global 'safe-mode *the-live-state*)) (super-stobjs-chk (if stobj-flag (let ((first-non-nil (find-first-non-nil super-stobjs-in))) `(live-stobjp ,FIRST-NON-NIL)) `(live-state-p ,(SELECT-STOBJ 'STATE SUPER-STOBJS-IN FORMALS)))) (guarded-primitive-p (and (not guard-is-t) boot-strap-p (not (member-equal (symbol-package-name fn) '("ACL2" "ACL2-PC"))))) (logic-recursive-p (and (eq defun-mode :logic) (ffnnamep-mod-mbe fn (body fn nil wrld)))) (labels-can-miss-guard (and logic-recursive-p (not cl-compliant-p-optimization) (not guard-is-t))) (trace-rec-for-none (and trace-rec-for-none logic-recursive-p (eq defun-mode :logic))) (program-only (and program-p (member-eq fn (f-get-global 'program-fns-with-raw-code *the-live-state*)))) (fail_program-only `(progn (save-ev-fncall-guard-er ',FN ',GUARD (stobjs-in ',FN (w *the-live-state*)) (list ,@FORMALS) (w *the-live-state*)) (er hard! 'program-only "~@0" (program-only-er-msg ',FN (list ,@FORMALS) ,SAFE-FORM)))) (early-exit-code-main (let* ((df-inputs-p (member-eq :df (stobjs-in fn (w *the-live-state*)))) (*1*guard (cond ((and cl-compliant-p-optimization (not live-stobjp-test) (not df-inputs-p)) (assert$ (not guard-is-t) :unused)) (t (oneify guard nil wrld program-p)))) (guard0 (cond (df-inputs-p *1*guard) (t guard))) (cl-compliant-code-guard-not-t (and (not program-only) (not guard-is-t) (eq defun-mode :logic) `(cond ,(COND ((EQ LIVE-STOBJP-TEST T) `(,GUARD0 (RETURN-FROM ,*1*FN ,(DF-CALL FN FORMALS)))) (T `((IF ,LIVE-STOBJP-TEST ,(IF STOBJ-FLAG (COND ((AND STOBJS-OUT (ALL-NILS-OR-DFS STOBJS-OUT)) GUARD0) (T `(LET ((*AOKP* NIL)) ,GUARD0))) GUARD0) ,*1*GUARD) ,(ASSERT$ (NOT GUARDED-PRIMITIVE-P) `(COND (,LIVE-STOBJP-TEST (RETURN-FROM ,*1*FN ,(DF-CALL FN FORMALS)))))))) ,@(COND (SUPER-STOBJS-IN `((T ,FAIL_GUARD))) (GUARDED-PRIMITIVE-P `((,SAFE-FORM ,FAIL_SAFE) (,GUARD-CHECKING-IS-REALLY-ON-FORM ,FAIL_GUARD))) (T `((,GUARD-CHECKING-IS-REALLY-ON-FORM ,FAIL_GUARD)))))))) (cond (cl-compliant-p-optimization (assert$ (not guard-is-t) (list cl-compliant-code-guard-not-t))) (program-only (list `(when (or ,SAFE-FORM ,@(AND (NOT GUARD-IS-T) `((NOT ,*1*GUARD)))) ,FAIL_PROGRAM-ONLY))) (t (let ((cond-clauses `(,@(AND (EQ DEFUN-MODE :LOGIC) (NOT GUARD-IS-T) `(((EQ (SYMBOL-CLASS ',FN (W *THE-LIVE-STATE*)) :COMMON-LISP-COMPLIANT) ,CL-COMPLIANT-CODE-GUARD-NOT-T))) ,@(AND (NOT GUARD-IS-T) (COND (SUPER-STOBJS-IN `(((NOT ,*1*GUARD) ,FAIL_GUARD))) (GUARDED-PRIMITIVE-P `(((AND (OR ,SAFE-FORM ,GUARD-CHECKING-IS-REALLY-ON-FORM) (NOT ,*1*GUARD)) (IF ,SAFE-FORM ,FAIL_SAFE ,FAIL_GUARD)))) (T `(((AND ,GUARD-CHECKING-IS-REALLY-ON-FORM (NOT ,*1*GUARD)) ,FAIL_GUARD))))) ,@(AND PROGRAM-P (COND (BOOT-STRAP-P `((,SAFE-FORM (RETURN-FROM ,*1*FN ,*1*BODY)) ,@(AND INVARIANT-RISK `((T (RETURN-FROM ,*1*FN ,*1*BODY)))))) (T `(((OR (MEMBER-EQ ,GUARD-CHECKING-ON-FORM '(:NONE :ALL)) ,SAFE-FORM) (RETURN-FROM ,*1*FN ,*1*BODY))))))))) (and cond-clauses (list (cons 'cond cond-clauses)))))))) (early-exit-code (and early-exit-code-main (cond ((and invariant-risk (not super-stobjs-in)) `((when (not **1*-as-raw*) ,@EARLY-EXIT-CODE-MAIN))) (t early-exit-code-main)))) (main-body-before-final-call (append (and (set-difference-eq stobjs-out '(nil :df state)) `((when *wormholep* (wormhole-er ',FN (list ,@FORMALS))))) (and (eq defun-mode :logic) guard-is-t (assert$ (not cl-compliant-p-optimization) `((when (eq (symbol-class ',FN (w *the-live-state*)) :common-lisp-compliant) (return-from ,*1*FN ,(DF-CALL FN FORMALS)))))) (cond ((and skip-early-exit-code-when-none early-exit-code) (cond (super-stobjs-in early-exit-code) (t `((when (not (eq ,GUARD-CHECKING-ON-FORM :none)) ,@EARLY-EXIT-CODE))))) (t early-exit-code)) (cond (trace-rec-for-none `((return-from ,*1*FN ,*1*BODY))) (labels-can-miss-guard `((when (eq ,GUARD-CHECKING-ON-FORM :all) (return-from ,*1*FN ,*1*BODY))))) (and (and labels-can-miss-guard (not trace-rec-for-none)) `((when (and (f-get-global 'raw-guard-warningp *the-live-state*) (eq ,GUARD-CHECKING-ON-FORM t)) (maybe-warn-for-guard-body ',FN *the-live-state*)))))) (*1*-body-forms (cond ((eq defun-mode :program) (append main-body-before-final-call (cond (invariant-risk (let ((check-invariant-risk-sym (gentemp)) (cont-p (gentemp))) `((let ((,CHECK-INVARIANT-RISK-SYM (get-check-invariant-risk *the-live-state*)) (,CONT-P nil)) (cond ((and ,CHECK-INVARIANT-RISK-SYM (not (f-get-global 'boot-strap-flg *the-live-state*))) (cond ((eq ,CHECK-INVARIANT-RISK-SYM :error) (state-free-global-let* ((debugger-enable t)) (cerror "~% Continue with invariant-risk ~ mode of T~% (that is, with state ~ global 'check-invariant-risk bound to ~ T)~% to complete the current call ~ of ~s.~% See :DOC invariant-risk." "Invariant-risk has been detected for a ~ call of function ~s~%(as possibly ~ leading to an ill-guarded call of ~ ~s);~%see :DOC invariant-risk." ',FN ',INVARIANT-RISK)) (setq ,CONT-P t)) ((eq ,CHECK-INVARIANT-RISK-SYM :warning) (with-live-state (warning$ ',FN "Invariant-risk" "Invariant-risk has been ~ detected for a call of ~ function ~x0 (as possibly ~ leading to an ill-guarded call ~ of ~x1); see :DOC ~ invariant-risk." ',FN ',INVARIANT-RISK)) (setq ,CONT-P t)) (t t)) (let ((**1*-as-raw* t)) ,(LET ((LABELS-FORM (LABELS-FORM-FOR-*1* FN *1*FN FORMALS (ONEIFY BODY NIL WRLD 'INVARIANT-RISK) IGNORE-VARS IGNORABLE-VARS SUPER-STOBJS-IN SUPER-STOBJS-CHK GUARD WRLD))) `(IF ,CONT-P (STATE-FREE-GLOBAL-LET* ((CHECK-INVARIANT-RISK T)) ,LABELS-FORM) ,LABELS-FORM)))) (t ,(DF-CALL FN FORMALS))))))) (t `(,(DF-CALL FN FORMALS)))))) (trace-rec-for-none main-body-before-final-call) (t (append main-body-before-final-call (list (labels-form-for-*1* fn *1*fn formals *1*body ignore-vars ignorable-vars super-stobjs-in super-stobjs-chk guard wrld))))))) `(,*1*FN ,FORMALS ,@(AND OPTIMIZE-DCLS `((DECLARE ,@OPTIMIZE-DCLS))) ,@*1*-BODY-FORMS)))))))
oneify-cltl-codefunction
(defun oneify-cltl-code (defun-mode def stobj-flag wrld &optional trace-rec-for-none) (let* ((stobjs-out-invalid (member-eq (car def) *stobjs-out-invalid*)) (fn (car def)) (stobjs-out (and (not stobjs-out-invalid) (stobjs-out fn wrld))) (stobjs-in (stobjs-in fn wrld)) (stobjs-in-df (member-eq :df stobjs-in)) (stobjs-out-df (member-eq :df stobjs-out))) (when (or stobjs-out-invalid (and (not stobjs-in-df) (not stobjs-out-df))) (return-from oneify-cltl-code (oneify-cltl-code-1 defun-mode def stobj-flag wrld trace-rec-for-none))) (let* ((new-def (oneify-cltl-code-1 defun-mode def stobj-flag wrld trace-rec-for-none)) (*1*fn (car new-def)) (formals (cadr new-def)) (formals-checks (loop for f in formals as s in stobjs-in when (eq s :df) collect `(assert (not (typep ,F 'double-float))))) *1*body *1*dcls/strings) (loop for tail on (cddr new-def) while (or (stringp (car tail)) (and (consp (car tail)) (eq (caar tail) 'declare))) collect (car tail) into dcls finally (setq *1*dcls/strings dcls *1*body `(block ,*1*FN ,@TAIL))) `(,*1*FN ,FORMALS ,@*1*DCLS/STRINGS ,@FORMALS-CHECKS ,(IF STOBJS-OUT-DF (REMOVE-DOUBLE-FLOATS STOBJS-OUT *1*BODY T) *1*BODY)))))
other
(defvar *saved-raw-prompt* nil)
other
(defvar *saved-raw-prompt-p* nil)
other
(progn (defun-one-output install-new-raw-prompt nil nil) (defun-one-output install-old-raw-prompt nil nil))
other
(defvar *dmr-interval* 1000)
other
(defvar *dmr-interval-acl2-par-hack* 300000)
other
(defvar *dmr-interval-used*)
other
(defvar *dmr-indent-max* 20)
other
(defvar *dmr-file-name*)
dmr-file-namefunction
(defun dmr-file-name nil (let ((user (or (getenv$-raw "USER") (progn (format t "Warning: Unable to determine USER ~ environment variable for ~ dmr-file-name.~%Will treat USER as ~ SOME-USER. In emacs, evaluate:~%(setq ~ *dmr-file-name* ~ "/tmp/acl2-dmr-SOME-USER")~%") "SOME-USER")))) (concatenate 'string "/tmp/acl2-dmr-" user)))
other
(defg *dmr-stream* nil)
other
(defg *dmr-counter* 0)
dmr-stop-fn-rawfunction
(defun dmr-stop-fn-raw nil (when *dmr-stream* (let ((str *dmr-stream*)) (setq *dmr-stream* nil) (close str))))
initialize-dmr-interval-usedfunction
(defun initialize-dmr-interval-used nil (setq *dmr-interval-used* *dmr-interval*))
dmr-start-fn-rawfunction
(defun dmr-start-fn-raw (state) (initialize-dmr-interval-used) (or (boundp '*dmr-file-name*) (setq *dmr-file-name* (dmr-file-name))) (setq *dmr-stream* (open *dmr-file-name* :if-exists :supersede :direction :output)) state)
other
(defv *dmr-array* (make-array 10000))
reverse-into-dmr-arrayfunction
(defun reverse-into-dmr-array (lst) (let ((len-1 (1- (length lst)))) (when (< (length *dmr-array*) len-1) (setq *dmr-array* (make-array (* 2 len-1)))) (loop for i from len-1 downto 0 as tail on lst do (setf (aref *dmr-array* i) (car tail))) len-1))
other
(defparameter *dmr-reusable-string* (make-array '(0) :element-type 'character :fill-pointer 0 :adjustable t))
other
(defvar *dmr-indent*)
dmr-increment-indentmacro
(defmacro dmr-increment-indent nil '(setq *dmr-indent* (+ 2 *dmr-indent*)))
tilde-@-bkptr-stringfunction
(defun tilde-@-bkptr-string (calling-sys-fn called-sys-fn bkptr) (case called-sys-fn (rewrite (cond ((integerp bkptr) (cond ((member-eq calling-sys-fn '(rewrite-with-lemma rewrite-quoted-constant-with-lemma add-linear-lemma)) (dmr-increment-indent) (format nil " the atom of hypothesis ~s" bkptr)) ((eq calling-sys-fn 'simplify-clause) (format nil " the atom of literal ~s" bkptr)) (t (format nil " argument ~s" bkptr)))) ((consp bkptr) (dmr-increment-indent) (format nil " the ~arhs of hypothesis ~s" (if (eq (car bkptr) 'rhs2) "rewritten " "") (cdr bkptr))) ((symbolp bkptr) (case bkptr (guard " the guard") (body " the body") (lambda-body " the lambda body") (lambda-object-body " the body of the lambda object") (rewritten-body " the rewritten body") (expansion " the expansion") (equal-consp-hack-car " the equality of the cars") (equal-consp-hack-cdr " the equality of the cdrs") (rhs " the rhs of the conclusion") (meta " the result of the metafunction") (nth-update " the result of the nth/update rewriter") (multiply-alists2 " the product of two polys") (forced-assumption " a forced assumption") (proof-builder " proof-builder top level") (otherwise (er hard 'tilde-@-bkptr-string "When ~x0 calls ~x1 we get an unrecognized ~ bkptr, ~x2." calling-sys-fn called-sys-fn bkptr)))) (t (er hard 'tilde-@-bkptr-string "When ~x0 calls ~x1 we get an unrecognized bkptr, ~x2." calling-sys-fn called-sys-fn bkptr)))) ((rewrite-with-lemma setup-simplify-clause-pot-lst simplify-clause add-terms-and-lemmas add-linear-lemma non-linear-arithmetic synp) "") (t (er hard 'tilde-@-bkptr-string "When ~x0 calls ~x1 we get an unrecognized bkptr, ~x2." calling-sys-fn called-sys-fn bkptr))))
other
(defvar *dmr-interp-state* 0)
dmr-interp-fresh-rewrite-pfunction
(defun dmr-interp-fresh-rewrite-p (calling-sys-fn frame) (not (and (eq calling-sys-fn 'rewrite) (integerp (access gframe frame :bkptr)))))
dmr-prefixfunction
(defun dmr-prefix nil (if (> *dmr-indent* *dmr-indent-max*) (concatenate 'string (aref1 'acl2-built-in-spaces-array *acl2-built-in-spaces-array* *dmr-indent-max*) (format nil "{~s} " *dmr-indent*)) (aref1 'acl2-built-in-spaces-array *acl2-built-in-spaces-array* *dmr-indent*)))
dmr-interpfunction
(defun dmr-interp (i calling-sys-fn frame) (let ((sys-fn (access gframe frame :sys-fn))) (case sys-fn (rewrite (cond ((dmr-interp-fresh-rewrite-p calling-sys-fn frame) (setq *dmr-interp-state* 0) (let ((bkptr-string (tilde-@-bkptr-string calling-sys-fn 'rewrite (access gframe frame :bkptr)))) (format nil "~a~s. Rewriting (to ~a)~a" (dmr-prefix) i (let ((obj (cddr (access gframe frame :args)))) (cond ((eq obj nil) "falsify") ((eq obj t) "establish") (t "simplify"))) bkptr-string))) ((eq *dmr-interp-state* 0) (setq *dmr-interp-state* 1) (format nil "; argument(s) ~s" (access gframe frame :bkptr))) (t (format nil "|~s" (access gframe frame :bkptr))))) ((rewrite-with-lemma add-linear-lemma rewrite-quoted-constant-with-lemma) (format nil "~a~s. Applying ~s~%" (dmr-prefix) i (get-rule-field (cdr (access gframe frame :args)) :rune))) (add-terms-and-lemmas (let ((len (length (car (access gframe frame :args)))) (obj (cdr (access gframe frame :args)))) (cond ((eq obj '?) (format nil "~a~s. Applying linear arithmetic to a clause with ~s term~a~%" (dmr-prefix) i len (if (eql len 1) "" "s"))) (t (format nil "~a~s. Applying linear arithmetic to ~a ~s term~a~%" (dmr-prefix) i (cond ((eq obj nil) "falsify") (t "establish")) len (if (eql len 1) "" "s")))))) (non-linear-arithmetic (let ((len (length (access gframe frame :args)))) (format nil "~a~s. Applying non-linear arithmetic to ~s var~a~%" (dmr-prefix) i len (if (eql len 1) "" "s")))) (synp (let ((synp-fn (access gframe frame :args))) (dmr-increment-indent) (format nil "~a~s. Entering ~s for hypothesis ~s~%" (dmr-prefix) i synp-fn (access gframe frame :bkptr)))) (setup-simplify-clause-pot-lst (format nil "~a~s. Setting up the linear pot list~%" (dmr-prefix) i)) (otherwise (er hard 'dmr-interp "Unrecognized sys-fn, ~x0" (access gframe frame :sys-fn))))))
other
(defvar *dmr-delete-string*
"delete-from-here-to-end-of-buffer")
dmr-stringfunction
(defun dmr-string nil (when (null *pstk-stack*) (setq *dmr-counter* *dmr-interval-used*) (setq *deep-gstack* nil) (return-from dmr-string *dmr-delete-string*)) (setf (fill-pointer *dmr-reusable-string*) 0) (let* ((pstk-tokens (loop with result = nil for x in *pstk-stack* do (push (cond ((eq (car x) 'waterfall) (car (nthcdr 8 x))) ((eq (car x) 'ev-fncall) (list (car x) (cadr x))) (t (car x))) result) finally (return result))) (pstk-tokens-tail pstk-tokens) (len-1 (reverse-into-dmr-array *deep-gstack*)) (calling-sys-fn 'start) (*print-pretty* nil) (counter 0) (*dmr-indent* 3) (no-newline-last-time nil)) (with-output-to-string (s *dmr-reusable-string*) (loop for token in pstk-tokens do (progn (setq pstk-tokens-tail (cdr pstk-tokens-tail)) (cond ((member-eq token '(rewrite-atm setup-simplify-clause-pot-lst)) (return)) (t (princ (format nil " ~s. ~s~%" counter token) s) (incf counter))))) (loop for i from 0 to len-1 do (let* ((frame (aref *dmr-array* i)) (sys-fn (access gframe frame :sys-fn))) (when (not (eq sys-fn 'simplify-clause)) (setq no-newline-last-time (eq calling-sys-fn 'rewrite)) (when (and no-newline-last-time (or (not (eq sys-fn 'rewrite)) (dmr-interp-fresh-rewrite-p calling-sys-fn frame))) (terpri s)) (princ (dmr-interp counter calling-sys-fn frame) s) (incf counter)) (setq calling-sys-fn (access gframe frame :sys-fn)))) (when (eq calling-sys-fn 'rewrite) (terpri s)) (dmr-increment-indent) (loop for token in pstk-tokens-tail when (not (eq token 'ev-fncall-meta)) do (progn (princ (if (eq token 'add-polynomial-inequalities) (format nil "~a~s. ~s: ~s calls~%" (dmr-prefix) counter token *add-polys-counter*) (format nil "~a~s. ~s~%" (dmr-prefix) counter token)) s) (incf counter))) (princ *dmr-delete-string* s))) *dmr-reusable-string*)
dmr-flush1function
(defun dmr-flush1 (&optional reset-counter) (file-position *dmr-stream* :start) (princ (dmr-string) *dmr-stream*) (without-interrupts (force-output *dmr-stream*)) (when reset-counter (setq *dmr-counter* 0)) t)
other
(declaim (inline dmr-flush))
dmr-flushfunction
(defun dmr-flush (&optional reset-counter) (when *dmr-stream* (cond (t (dmr-flush1 reset-counter)))))
other
(declaim (inline dmr-display))
dmr-displayfunction
(defun dmr-display nil (when *dmr-stream* (cond ((> *dmr-counter* *dmr-interval-used*) (setq *dmr-counter* 0) (cond (t (dmr-flush1)))) (t (setq *dmr-counter* (1+ *dmr-counter*))))))
cw-gstack-shortfunction
(defun cw-gstack-short nil (let* ((str (dmr-string)) (pos (search *dmr-delete-string* str))) (princ (if pos (subseq str 0 pos) str) *terminal-io*)))
other
(eval-when (:load-toplevel :execute) (f-put-global 'current-acl2-world nil *the-live-state*) (setf (get 'current-acl2-world 'acl2-world-pair) (cons nil *current-acl2-world-key*)))
other
(defun-one-output fmakunbound!
(name)
(fmakunbound name)
(when (macro-function name)
(error "This Common Lisp implementation seems unable to unbind ~~%
macro-functions. Please let the ACL2 implementors know about ~%~
this problem.")))
other
(defun-one-output maybe-push-undo-stack (fn name &optional extra) (cond ((and (symbolp name) (fboundp name) (not (eq fn 'attachment))) (maybe-untrace! name t))) (case fn ((defun defmacro) (cond ((fboundp name) (let ((oneified-name (*1*-symbol name)) (macro-p (macro-function name))) (push `(progn ,@(AND (NOT MACRO-P) `((MAYBE-UNTRACE! ',NAME) (MAYBE-UNMEMOIZE ',NAME))) ,@(IF (EQ EXTRA 'RECLASSIFYING) (ASSERT$ (NOT MACRO-P) `((SETF (SYMBOL-FUNCTION ',ONEIFIED-NAME) ',(SYMBOL-FUNCTION ONEIFIED-NAME)))) `(,@(IF (NOT (IFF (EQ FN 'DEFMACRO) MACRO-P)) `((FMAKUNBOUND! ',NAME))) ,(COND (MACRO-P `(SETF (MACRO-FUNCTION ',NAME) ',(MACRO-FUNCTION NAME))) (T `(SETF (SYMBOL-FUNCTION ',NAME) ',(SYMBOL-FUNCTION NAME)))) ,(COND ((FBOUNDP ONEIFIED-NAME) `(SETF (SYMBOL-FUNCTION ',ONEIFIED-NAME) ',(SYMBOL-FUNCTION ONEIFIED-NAME))) (T `(FMAKUNBOUND! ',ONEIFIED-NAME)))))) (get name '*undo-stack*)))) (t (push `(progn (maybe-untrace! ',NAME) (maybe-unmemoize ',NAME) (fmakunbound! ',NAME) (fmakunbound! ',(*1*-SYMBOL NAME))) (get name '*undo-stack*))))) (defconst (cond ((boundp name) (push `(progn (setf (symbol-value ',NAME) ',(SYMBOL-VALUE NAME)) (setf (get ',NAME 'redundant-raw-lisp-discriminator) ',(GET NAME 'REDUNDANT-RAW-LISP-DISCRIMINATOR))) (get name '*undo-stack*))) (t (push `(progn (makunbound ',NAME) (remprop ',NAME 'redundant-raw-lisp-discriminator)) (get name '*undo-stack*))))) ((defstobj defabsstobj) (push `(remhash ',NAME (the hash-table *current-stobj-gensym-ht*)) (get name '*undo-stack*))) (defpkg (let ((temp (find-non-hidden-package-entry name (known-package-alist *the-live-state*)))) (cond (temp (push `(defpkg ,NAME ',(PACKAGE-ENTRY-IMPORTS TEMP)) (get (packn (cons name '("-PACKAGE"))) '*undo-stack*)))))) (attachment (cond ((eq name *special-cltl-cmd-attachment-mark-name*) (push `(unless (eq ',NAME (car *defattach-fns*)) (push ',NAME *defattach-fns*)) (get name '*undo-stack*))) (t (push `(progn (push ',NAME *defattach-fns*) ,(SET-ATTACHMENT-SYMBOL-FORM NAME (SYMBOL-VALUE (ATTACHMENT-SYMBOL NAME)))) (get name '*undo-stack*))))) (memoize (push `(when (memoizedp-raw ',NAME) (unmemoize-fn ',NAME)) (get name '*undo-stack*))) (unmemoize (let* ((entry (gethash name *memoize-info-ht*)) (condition (access memoize-info-ht-entry entry :condition)) (inline (access memoize-info-ht-entry entry :inline)) (commutative (access memoize-info-ht-entry entry :commutative)) (forget (access memoize-info-ht-entry entry :forget)) (memo-table-init-size (access memoize-info-ht-entry entry :memo-table-init-size)) (aokp (and (access memoize-info-ht-entry entry :ext-anc-attachments) t)) (cl-defun (access memoize-info-ht-entry entry :cl-defun)) (invoke (access memoize-info-ht-entry entry :invoke))) (push `(memoize-fn ',NAME :condition ',CONDITION :inline ',INLINE ,@(AND COMMUTATIVE `(:COMMUTATIVE T)) ,@(AND FORGET `(:FORGET T)) ,@(AND MEMO-TABLE-INIT-SIZE `(:MEMO-TABLE-INIT-SIZE ',MEMO-TABLE-INIT-SIZE)) ,@(AND AOKP `(:AOKP ',AOKP)) ,@(AND CL-DEFUN `(:CL-DEFUN ',CL-DEFUN)) ,@(AND INVOKE `(:INVOKE ',INVOKE))) (get name '*undo-stack*)))) (otherwise (er hard 'maybe-push-undo-stack "Unrecognized CLTL-COMMAND spawn ~x0" fn))))
other
(defun-one-output maybe-pop-undo-stack (name) (let* ((name (if (symbolp name) name (packn (cons name '("-PACKAGE"))))) (stk (get name '*undo-stack*))) (cond ((null stk) nil) (t (eval (car stk)) (setf (get name '*undo-stack*) (cdr stk))))))
other
(defparameter *current-acl2-world-key-ordering*
'(coarsenings global-value
recognizer-alist
runic-mapping-pairs
def-bodies
symbol-class
stobjs-out
type-prescriptions
table-alist
lemmas
congruences
pequivs
macro-body
formals))
other
(defun-one-output key-lesseqp (key1 key2 ordering) (cond ((null ordering) t) ((eq key1 (car ordering)) t) ((eq key2 (car ordering)) nil) (t (key-lesseqp key1 key2 (cdr ordering)))))
other
(defun-one-output merge-into-alist (key val alist) (cond ((null alist) (list (cons key val))) ((key-lesseqp key (caar alist) *current-acl2-world-key-ordering*) (cons (cons key val) alist)) (t (cons (car alist) (merge-into-alist key val (cdr alist))))))
other
(defun-one-output destructive-push-assoc (key value alist world-key) (let ((temp (assoc key alist :test (function eq)))) (cond (temp (setf (cdr temp) (cons value (cdr temp))) alist) ((eq world-key *current-acl2-world-key*) (merge-into-alist key (list value) alist)) (t (cons (cons key (list value)) alist)))))
other
(defun-one-output destructive-pop-assoc (key alist) (let ((temp (assoc key alist :test (function eq)))) (cond (temp (setf (cdr temp) (cdr (cdr temp))) alist) (t alist))))
other
(defun-one-output remove-current-acl2-world-key (plist) (cond ((null plist) plist) ((eq (car plist) *current-acl2-world-key*) (cddr plist)) (t (cons (car plist) (cons (cadr plist) (remove-current-acl2-world-key (cddr plist)))))))
hcomp-initfunction
(defun hcomp-init (&aux (state *the-live-state*)) (when (or (raw-mode-p state) (null *hcomp-fn-ht*)) (assert (and (null *hcomp-const-ht*) (null *hcomp-macro-ht*))) (return-from hcomp-init nil)) (dolist (pair *hcomp-fn-alist*) (when (cdr pair) (setf (gethash (car pair) *hcomp-fn-ht*) (cdr pair)))) (dolist (pair *hcomp-const-alist*) (when (cdr pair) (setf (gethash (car pair) *hcomp-const-ht*) (cdr pair))) (when *hcomp-const-restore-ht* (multiple-value-bind (old present-p) (gethash (car pair) *hcomp-const-restore-ht*) (declare (ignore old)) (when (not present-p) (setf (gethash (car pair) *hcomp-const-restore-ht*) (cond ((boundp (car pair)) (symbol-value (car pair))) (t *hcomp-fake-value*))))))) (dolist (pair *hcomp-macro-alist*) (when (cdr pair) (setf (gethash (car pair) *hcomp-macro-ht*) (cdr pair)))) (when *hcomp-fn-macro-restore-ht* (dolist (pair (append *hcomp-macro-alist* *hcomp-fn-alist*)) (multiple-value-bind (old present-p) (gethash (car pair) *hcomp-fn-macro-restore-ht*) (declare (ignore old)) (when (not present-p) (setf (gethash (car pair) *hcomp-fn-macro-restore-ht*) (let ((mac (macro-function (car pair)))) (cond (mac (cons 'macro mac)) ((fboundp (car pair)) (cons 'function (symbol-function (car pair)))) (t *hcomp-fake-value*)))))))) (when *load-compiled-stack* (assert (boundp '*hcomp-full-book-string*)) (chk-certificate-file *hcomp-full-book-string* *hcomp-directory-name* *hcomp-full-book-name* 'include-book-raw *hcomp-ctx* state nil nil)) nil)
reclassifying-value-pother
(defabbrev reclassifying-value-p (x) (and (consp x) (eq (car x) *hcomp-fake-value*)))
make-reclassifying-valuemacro
(defmacro make-reclassifying-value (x) `(cons *hcomp-fake-value* ,X))
unmake-reclassifying-valuemacro
(defmacro unmake-reclassifying-value (x) `(cdr ,X))
hcomp-transfer-to-hash-tablesfunction
(defun hcomp-transfer-to-hash-tables nil (dolist (pair *hcomp-fn-alist*) (let ((qualified (gethash (car pair) *hcomp-fn-ht*))) (cond ((and qualified (fboundp (car pair))) (setf (gethash (car pair) *hcomp-fn-ht*) (cond ((eq qualified t) (symbol-function (car pair))) (t (assert$ (eq qualified 'semi) (make-reclassifying-value (symbol-function (car pair)))))))) (t (remhash (car pair) *hcomp-fn-ht*))))) (dolist (pair *hcomp-const-alist*) (let ((qualified (gethash (car pair) *hcomp-const-ht*))) (cond ((and qualified (boundp (car pair))) (setf (gethash (car pair) *hcomp-const-ht*) (assert$ (eq qualified t) (symbol-value (car pair))))) (t (remhash (car pair) *hcomp-const-ht*))))) (dolist (pair *hcomp-macro-alist*) (let ((qualified (gethash (car pair) *hcomp-macro-ht*))) (cond ((and qualified (macro-function (car pair))) (setf (gethash (car pair) *hcomp-macro-ht*) (assert$ (eq qualified t) (macro-function (car pair))))) (t (remhash (car pair) *hcomp-macro-ht*))))))
other
(defvar *saved-hcomp-restore-hts* nil)
hcomp-restore-defsfunction
(defun hcomp-restore-defs nil (when (null *saved-hcomp-restore-hts*) (er hard 'hcomp-restore-defs "Apparently an interrupt has occurred at exactly the right time to ~ thwart ACL2's attempt to clean up by removing certain definitions in ~ raw Lisp. You are strongly advised to restart ACL2. You could ~ instead try to continue, but you might well encounter errors ~ regarding having definitions in raw Common Lisp.")) (let ((fn-macro-restore-ht (car *saved-hcomp-restore-hts*)) (const-restore-ht (cdr *saved-hcomp-restore-hts*))) (when fn-macro-restore-ht (maphash (lambda (k val) (cond ((eq val *hcomp-fake-value*) (fmakunbound! k)) ((eq (car val) 'macro) (setf (macro-function k) (cdr val))) (t (when (macro-function k) (fmakunbound! k)) (setf (symbol-function k) (cdr val))))) fn-macro-restore-ht)) (when const-restore-ht (maphash (lambda (k val) (cond ((eq val *hcomp-fake-value*) (remprop k 'redundant-raw-lisp-discriminator) (makunbound k)) (t (setf (symbol-value k) val)))) const-restore-ht)) nil))
missing-compiled-bookfunction
(defun missing-compiled-book (ctx file reason-msg load-compiled-file state) (let ((see-doc " See :DOC include-book.") (wrld (w state))) (cond ((null load-compiled-file) (er hard ctx "Implementation error: the LOAD-COMPILED-FILE argument is ~x0 ~ in call ~x1." nil `(missing-compiled-book ',CTX ',FILE ',REASON-MSG ',LOAD-COMPILED-FILE state))) ((or (eq load-compiled-file t) (rassoc-eq t *load-compiled-stack*)) (let ((stack-msg (cond ((eq load-compiled-file t) (tilde-@-book-stack-msg t *load-compiled-stack* ctx wrld)) (t (tilde-@-book-stack-msg (car (rassoc-eq t *load-compiled-stack*)) *load-compiled-stack* ctx wrld))))) (cond (reason-msg (er hard ctx "Unable to load compiled file~| ~s0~|because ~ ~@1.~@2~@3" file reason-msg see-doc stack-msg)) (t (er hard ctx "Unable to complete load of compiled file for book~|~ ~ ~ ~s0,~|as already noted by a warning.~@1~@2" file see-doc stack-msg))))) (reason-msg (warning$ ctx "Compiled file" "Unable to load compiled file for book~| ~s0~|because ~ ~@1.~@2~@3" file reason-msg see-doc (tilde-@-book-stack-msg nil *load-compiled-stack* ctx wrld))) (t (warning$ ctx "Compiled file" "Unable to complete load of compiled file for book~| ~ ~s0,~|as already noted by a previous warning.~@1" file (tilde-@-book-stack-msg nil *load-compiled-stack* ctx wrld))))) 'incomplete)
our-handler-bindmacro
(defmacro our-handler-bind (bindings &rest forms) `(handler-bind ,BINDINGS ,@FORMS))
load-compiled-bookfunction
(defun load-compiled-book (file full-book-name directory-name load-compiled-file ctx state) (assert load-compiled-file) (mv-let (acl2-cfile state) (certificate-file file state) (let* ((cfile (and acl2-cfile (pathname-unix-to-os acl2-cfile state))) (os-file (pathname-unix-to-os file state)) (cfile-date (and cfile (file-write-date cfile))) (ofile (convert-book-string-to-compiled os-file state)) (ofile-exists (probe-file ofile)) (ofile-date (and ofile-exists (file-write-date ofile))) (ofile-p (and ofile-date cfile-date (>= ofile-date cfile-date))) (efile (and (not (eq load-compiled-file t)) (expansion-filename os-file))) (efile-exists (and efile (probe-file efile))) (file-is-older-str "the file-write-date of ~x0 is less than that of ~x1")) (cond ((not cfile) (missing-compiled-book ctx file (if (probe-file (convert-book-string-to-cert file t)) "that book is not certified (but note that ~ its .cert file exists and is not readable)" "that book is not certified") load-compiled-file state)) ((and (not ofile-exists) (not efile-exists)) (missing-compiled-book ctx file "the compiled file does not exist" load-compiled-file state)) ((not cfile-date) (missing-compiled-book ctx file (msg "~x0 is ~x1 (which is odd since file ~x2 exists)" `(file-write-date$ ,ACL2-CFILE state) nil acl2-cfile) load-compiled-file state)) ((not (or ofile-p (let ((efile-date (and efile-exists (file-write-date efile)))) (and efile-date (>= efile-date cfile-date))))) (cond (ofile-exists (missing-compiled-book ctx file (msg file-is-older-str ofile cfile) load-compiled-file state)) (t (missing-compiled-book ctx file (msg "the compiled file does not exist and ~@0" (msg file-is-older-str (expansion-filename file) acl2-cfile)) load-compiled-file state)))) ((and (not ofile-p) (rassoc-eq t *load-compiled-stack*)) (missing-compiled-book ctx file (if ofile-exists "that compiled file does not exist" "that compiled file is out-of-date") load-compiled-file state)) (t (let ((to-be-compiled-p (and (not ofile-p) (null *load-compiled-stack*) (eq load-compiled-file :comp))) (status 'incomplete)) (when (and (not ofile-p) (not to-be-compiled-p)) (let ((acl2-ofile (convert-book-string-to-compiled file state))) (warning$ ctx "Compiled file" "Loading expansion file ~x0 in place of compiled file ~ ~x1, because ~@2." (expansion-filename file) acl2-ofile (cond (ofile-exists (msg file-is-older-str acl2-ofile acl2-cfile)) (t (msg "the compiled file is missing")))))) (catch 'missing-compiled-book (state-global-let* ((raw-include-book-dir-alist nil)) (with-cbd directory-name (let ((*load-compiled-stack* (acons full-book-name load-compiled-file *load-compiled-stack*))) (multiple-value-bind (er val) (catch 'my-book-error (our-handler-bind ((error (function (lambda (c) (setq *hcomp-fn-ht* nil *hcomp-const-ht* nil *hcomp-macro-ht* nil) (throw 'my-book-error (values t (format nil "~a" c))))))) (values nil (cond (ofile-p (load-compiled ofile t)) (t (with-reckless-readtable (load efile))))))) (value (setq status (cond (er (setq status val)) (to-be-compiled-p 'to-be-compiled) (t 'complete))))))))) (cond ((stringp status) (warning$ ctx "Compiled file" "The following raw Lisp error occurred when loading ~ file~|~s0:~|~s1" (cond (ofile-p ofile) (t efile)) status) (missing-compiled-book ctx file (msg "an error occurred in raw Lisp (see above)") load-compiled-file state)) (t (hcomp-transfer-to-hash-tables) (assert$ (member-eq status '(to-be-compiled complete incomplete)) status)))))))))
include-book-rawfunction
(defun include-book-raw (book-string book-name directory-name load-compiled-file dir ctx state) (when (not (member-eq load-compiled-file *load-compiled-file-values*)) (er hard ctx "The only legal values for the :LOAD-COMPILED-FILE keyword argument ~ of ~x0 are ~&1. The value ~x2 is thus illegal." 'include-book *load-compiled-file-values* load-compiled-file)) (when *compiling-certified-file* (return-from include-book-raw nil)) (let* ((raw-mode-p (raw-mode-p state)) (load-compiled-file (cond ((null (f-get-global 'compiler-enabled state)) nil) ((eq load-compiled-file :default) :warn) (t (or load-compiled-file (and *load-compiled-stack* :warn)))))) (when (and (not raw-mode-p) (null load-compiled-file)) (return-from include-book-raw nil)) (mv-let (full-book-string full-book-name directory-name ignore-familiar-name) (cond (directory-name (mv book-string book-name directory-name nil)) (t (parse-book-name (cond (dir (or (include-book-dir dir state) (er hard ctx "Unable to resolve the :DIR argument to ~ include-book, ~x0, which should have been ~ defined by ~v1 or by the ~ project-dir-alist. Perhaps the book ~x2 ~ needs to be recertified, or perhaps the ~ project-dir-alist needs to be set up to ~ associate a directory with ~x0 and ~ possibly other keywords (see :DOC ~ project-dir-alist)." dir '(add-include-book-dir add-include-book-dir!) book-string))) (t (f-get-global 'connected-book-directory state))) book-string ".lisp" ctx state))) (declare (ignore ignore-familiar-name)) (cond ((assoc-equal full-book-name (global-val 'include-book-alist (w state))) nil) ((or raw-mode-p (null *hcomp-book-ht*)) (with-cbd-raw state-free-global-let*-safe directory-name (let* ((os-file (pathname-unix-to-os full-book-string state)) (ofile (convert-book-string-to-compiled os-file state)) (os-file-exists (probe-file os-file)) (ofile-exists (probe-file ofile)) (book-date (and os-file-exists (file-write-date os-file))) (ofile-date (and ofile-exists (file-write-date ofile)))) (cond ((not os-file-exists) (er hard ctx "The file named ~x0 does not exist." full-book-string)) ((null load-compiled-file) (assert$ raw-mode-p (load os-file))) ((and book-date ofile-date (<= book-date ofile-date)) (load-compiled ofile t)) (t (let ((reason (cond (ofile-exists "the compiled file is not at least as ~ recent as the book") (t "the compiled file does not exist")))) (cond ((eq load-compiled-file t) (er hard ctx "The compiled file for ~x0 was not loaded ~ because ~@1." reason)) (t (let* ((efile (expansion-filename os-file)) (efile-date (and (probe-file efile) (file-write-date efile))) (efile-p (and book-date efile-date (<= book-date efile-date))) (lfile (cond (efile-p efile) (raw-mode-p os-file) (t (er hard ctx "Implementation error: ~ We seem to have ~ called ~ include-book-raw on ~ book ~x0 with non-nil ~ load-compiled-file ~ argument under the ~ include-book-fn call ~ in certify-book-fn." book-string))))) (warning$ ctx "Compiled file" "Attempting to load ~@0 instead of ~ the corresponding compiled file, ~ because ~@1." (msg (cond (efile-p "expansion file ~x0") (t "source file ~x0")) lfile) reason) (cond (efile-p (with-reckless-readtable (load efile))) (raw-mode-p (load os-file)))))))))))) ((let* ((entry (assert$ *hcomp-book-ht* (gethash full-book-name *hcomp-book-ht*))) (status (and entry (access hcomp-book-ht-entry entry :status)))) (cond (raw-mode-p status) ((and (eq status 'incomplete) *load-compiled-stack*) (error "Implementation error; see include-book-raw.") (throw 'missing-compiled-book (missing-compiled-book ctx full-book-string nil load-compiled-file state))) (t status)))) (t (with-hcomp-bindings (let ((status (let ((*user-stobj-alist* *user-stobj-alist*) (*hcomp-full-book-string* full-book-string) (*hcomp-full-book-name* full-book-name) (*hcomp-directory-name* directory-name) (*hcomp-ctx* ctx)) (load-compiled-book full-book-string full-book-name directory-name load-compiled-file ctx state)))) (setf (gethash full-book-name *hcomp-book-ht*) (make hcomp-book-ht-entry :status status :fn-ht *hcomp-fn-ht* :const-ht *hcomp-const-ht* :macro-ht *hcomp-macro-ht* :cert-obj *hcomp-cert-obj* :cert-filename *hcomp-cert-filename*)) (cond ((member-eq status '(to-be-compiled complete)) status) (status (assert$ (eq status 'incomplete) (cond (*load-compiled-stack* (throw 'missing-compiled-book 'incomplete)) (t 'incomplete))))))))))))
include-book-raw-topfunction
(defun include-book-raw-top (full-book-string full-book-name directory-name load-compiled-file dir ctx state) (handler-bind ((warning (lambda (c) (declare (ignore c)) (invoke-restart 'muffle-warning)))) (let ((*hcomp-fn-macro-restore-ht* (make-hash-table :test 'eq)) (*hcomp-const-restore-ht* (make-hash-table :test 'eq))) (setq *saved-hcomp-restore-hts* nil) (acl2-unwind-protect "include-book-raw" (unwind-protect (state-global-let* ((ld-skip-proofsp 'include-book) (raw-include-book-dir!-alist (assert$ (not (raw-include-book-dir-p state)) (table-alist 'include-book-dir!-table (w state)))) (raw-include-book-dir-alist nil)) (progn (include-book-raw full-book-string full-book-name directory-name load-compiled-file dir ctx state) (value nil))) (setq *saved-hcomp-restore-hts* (list* *hcomp-fn-macro-restore-ht* *hcomp-const-restore-ht*))) (progn (hcomp-restore-defs) (setq *saved-hcomp-restore-hts* nil) state) (progn (hcomp-restore-defs) (setq *saved-hcomp-restore-hts* nil) state)))))
hcomp-ht-from-typemacro
(defmacro hcomp-ht-from-type (type ctx) `(case ,TYPE (defun *hcomp-fn-ht*) (defparameter *hcomp-const-ht*) ((defmacro defabbrev) *hcomp-macro-ht*) (otherwise (er hard ,CTX "Implementation error: Unknown case, ~x0." ,TYPE))))
hcomp-build-pfunction
(defun hcomp-build-p nil (let ((s *hcomp-status*)) (cond ((eq s 'certify-book) 'certify-book) ((eq s 'encapsulate-pass-1) 'encapsulate-pass-1) (t nil))))
install-for-add-trip-hcomp-buildfunction
(defun install-for-add-trip-hcomp-build (def reclassifyingp evalp) (let* ((type (car def)) (name (cadr def)) (ht (hcomp-ht-from-type type 'install-for-add-trip-hcomp-build))) (when evalp (with-debug (eval def) "[~s] Eval def for ~s.~%" 'idfathb-1 name)) (assert ht) (multiple-value-bind (old present-p) (gethash name ht) (cond ((eq old *hcomp-fake-value*)) ((and (consp (car (last def))) (eq (car (car (last def))) 'quote)) (with-debug (setf (gethash name ht) *hcomp-fake-value*) "[~s] Set hash table to *hcomp-fake-value* for ~s.~%" 'idfathb-3 name)) (present-p (cond ((and reclassifyingp (not (reclassifying-value-p old))) (with-debug (assert$ (eq type 'defun) (setf (gethash name ht) (make-reclassifying-value (symbol-function name)))) "[~s] Set hash table to reclassifying value for ~ ~s.~%" 'idfathb-4 name)) (t (with-debug (setf (gethash name ht) *hcomp-fake-value*) "[~s] Set hash table to ~ *hcomp-fake-value* for ~s.~%" 'idfathb-5 name)))) (t (with-debug (setf (gethash name ht) (case type (defun (symbol-function name)) (defparameter (symbol-value name)) (otherwise (macro-function name)))) "[~s] Set hash table for ~s.~%" 'idfathb-6 name))))))
install-for-add-trip-include-bookfunction
(defun install-for-add-trip-include-book (type name name0 def reclassifyingp wrld) (let ((ht (hcomp-ht-from-type type 'install-for-add-trip-include-book)) (return-val nil)) (when (null ht) (return-from install-for-add-trip-include-book (and def (with-debug (eval def) "[~s] Eval def for ~s.~%" 'ifatib-1 name)))) (multiple-value-bind (val present-p) (gethash name ht) (when present-p (setq return-val (cond ((eq val *hcomp-fake-value*) nil) ((not (or (eq type 'defun) (and (eq type 'defmacro) wrld))) t) (t (let ((ext-gens (and wrld (global-val 'ext-gens wrld))) ext-gen-barriers) (cond ((null ext-gens) t) ((and ext-gens (member-eq name0 ext-gens)) (cond ((and (eq type 'defun) (compiled-function-p val)) 'to-compile) (t nil))) ((and (setq ext-gen-barriers (and ext-gens (global-val 'ext-gen-barriers wrld))) (member-eq name0 ext-gen-barriers)) (assert (eq type 'defun)) (if (compiled-function-p val) 'to-compile nil)) (t t))))))) (cond ((eq return-val t) (assert$ (not (eq val *hcomp-fake-value*)) (cond ((reclassifying-value-p val) (assert$ (eq type 'defun) (let ((fixed-val (unmake-reclassifying-value val))) (setf (gethash name ht) fixed-val) (cond (reclassifyingp (with-debug (setf (symbol-function name) fixed-val) "[~s] Set (symbol-function ~s) with fixed-val.~%" 'ifatib-2 name)) (t (cond (def (with-debug (eval def) "[~s] Eval def for ~s.~%" 'ifatib-3 name)) (t (setq return-val nil)))))))) (t (case type (defun (with-debug (setf (symbol-function name) val) "[~s] Set (symbol-function ~s), mode ~s.~%" 'ifatib-4 name (fdefun-mode name0 wrld))) (defparameter (with-debug (setf (symbol-value name) val) "[~s] Set (symbol-value ~s).~%" 'ifatib-5 name)) (otherwise (assert$ (member-eq type '(defabbrev defmacro)) (with-debug (setf (macro-function name) val) "[~s] Set (macro-function ~s).~%" 'ifatib-6 name)))) t)))) (t (when def (with-debug (eval def) "[~s] Eval def for ~s.~%" 'ifatib-7 def)))) return-val)))
install-for-add-tripfunction
(defun install-for-add-trip (def reclassifyingp evalp) (cond ((eq *hcomp-status* 'include-book) (install-for-add-trip-include-book (car def) (cadr def) (cadr def) def reclassifyingp nil)) ((hcomp-build-p) (install-for-add-trip-hcomp-build def reclassifyingp evalp)) (t (with-debug (eval def) "[~s] Eval def for ~s.~%" 'ifat-1 (cadr def)))))
install-defs-for-add-tripfunction
(defun install-defs-for-add-trip (defs reclassifying-p wrld declaim-p evalp &aux (hcomp-build-p (hcomp-build-p))) (loop for tail on defs do (let* ((def (car tail)) (oneify-p (eq (car def) 'oneify-cltl-code)) (def0 (if oneify-p (caddr def) (cdr def))) (name (car def0)) (sname (symbol-name name))) (cond ((equal (caddr def0) '(declare (xargs :non-executable :program))) (let ((form (list 'notinline (if oneify-p (*1*-symbol name) name)))) (with-debug (proclaim form) "[~s] (proclaim ~s)~%" 'idfat-1 form) (when hcomp-build-p (push (list 'declaim form) *declaim-list*)))) (oneify-p nil) ((inline-namep sname) (let ((form (list 'inline name))) (with-debug (proclaim form) "[~s] (proclaim ~s)~%" 'idfat-2 form) (when hcomp-build-p (push (list 'declaim form) *declaim-list*)))) ((notinline-namep sname) (let ((form (list 'notinline name))) (with-debug (proclaim form) "[~s] (proclaim ~s)~%" 'idfat-3 form) (when hcomp-build-p (push (list 'declaim form) *declaim-list*))))))) (loop with ext-gen-barriers = (and evalp (global-val 'ext-gen-barriers wrld)) for tail on defs do (let* ((def (car tail)) (oneify-p (eq (car def) 'oneify-cltl-code)) (def0 (if oneify-p (caddr def) (cdr def))) (name (car def0)) (flg nil)) (cond ((and (eq *hcomp-status* 'include-book) (cond (oneify-p (setq flg (install-for-add-trip-include-book 'defun (*1*-symbol name) name nil reclassifying-p wrld))) ((and (not (member-eq (car def) '(defmacro defabbrev))) (inline-namep (symbol-name name))) nil) (t (setq flg (install-for-add-trip-include-book (car def) (cadr def) (cadr def) nil reclassifying-p wrld)))) (eq flg t)) (setf (car tail) nil)) (t (let (form) (cond (oneify-p (let ((*1*-def (cons 'defun (oneify-cltl-code (cadr def) def0 (cdddr def) wrld)))) (setf (car tail) *1*-def))) ((and declaim-p (not (member-eq (car def) '(defmacro defabbrev)))) (setq form (make-defun-declare-form (cadr def) def)))) (when (and form hcomp-build-p) (push form *declaim-list*)) (when (and ext-gen-barriers (or oneify-p (eq (car def) 'defun)) (member-eq name ext-gen-barriers)) (let ((tmp `(notinline ,(IF ONEIFY-P (*1*-SYMBOL NAME) NAME)))) (with-debug (proclaim tmp) "[~s] (proclaim ~s)~%" 'idfat-4 tmp))) (when form (with-debug (eval form) "[~s] (eval ~s)~%" 'idfat-5 form)) (let ((skip-reason (and (eq hcomp-build-p 'encapsulate-pass-1) (let ((state *the-live-state*)) (and (f-get-global 'in-local-flg state) (cond ((and oneify-p (eq (cadr def) :logic)) 'logic) ((in-nested-encapsulatep state) 'nested-encapsulate) (t nil))))))) (when skip-reason (cond ((eq skip-reason 'logic) (assert *hcomp-fn-ht*) (with-debug (eval (car tail)) "[~s] Storing *hcomp-fake-value* for ~ ~s.~%" 'idfat-6 (*1*-symbol name)) (setf (gethash (*1*-symbol name) *hcomp-fn-ht*) *hcomp-fake-value*)) (evalp (with-debug (eval (car tail)) "[~s] Eval def for ~s.~%" 'idfat-7 (cadr (car tail))))) (setf (car tail) nil)))))))) (cond ((eq *hcomp-status* 'include-book) (assert evalp) (loop for def in defs when def do (with-debug (eval def) "[~s] Eval def for ~s.~%" 'idfat-8 (cadr def)))) (hcomp-build-p (loop for def in defs when def do (install-for-add-trip-hcomp-build def reclassifying-p evalp))) (t (assert evalp) (loop for def in defs do (with-debug (eval def) "[~s] Eval def for ~s.~%" 'idfat-9 (cadr def))))))
ifat-defparameterfunction
(defun ifat-defparameter (name val form) (if (and (consp form) (eq (car form) 'quote)) `(defparameter ,NAME ',VAL) `(defparameter ,NAME (our-quote-macro ,VAL))))
hcomp-build-from-state-rawfunction
(defun hcomp-build-from-state-raw (cltl-cmds state) (let ((*hcomp-status* 'certify-book)) (dolist (cltl-cmd cltl-cmds) (let* ((wrld (w state))) (case (car cltl-cmd) (defuns (let ((ignorep (caddr cltl-cmd)) (defun-mode (cadr cltl-cmd)) (new-defs nil) (new-*1*-defs nil)) (dolist (def (cdddr cltl-cmd)) (cond ((and (consp ignorep) (eq (car ignorep) 'defstobj)) nil) (t (or ignorep (setq new-defs (cons (cons 'defun def) new-defs))) (setq new-*1*-defs (cons (list* 'oneify-cltl-code defun-mode def (if (consp ignorep) (cdr ignorep) nil)) new-*1*-defs))))) (install-defs-for-add-trip (nconc new-defs new-*1*-defs) (eq ignorep 'reclassifying) wrld t nil))) ((defstobj defabsstobj) (let ((name (nth 1 cltl-cmd)) (raw-defs (nth 4 cltl-cmd)) (ax-defs (nth 6 cltl-cmd)) (new-defs nil)) (dolist (def raw-defs) (push (cond ((eq (car cltl-cmd) 'defabsstobj) (cons 'defmacro def)) ((member-equal *stobj-inline-declare* def) (cons 'defabbrev (remove-stobj-inline-declare def))) (t (cons 'defun def))) new-defs)) (dolist (def ax-defs) (push (list* 'oneify-cltl-code :logic def name) new-defs)) (setq new-defs (nreverse new-defs)) (install-defs-for-add-trip new-defs nil wrld t nil))) (defconst (install-for-add-trip (ifat-defparameter (cadr cltl-cmd) (cadddr cltl-cmd) (caddr cltl-cmd)) nil nil)) (defmacro (install-for-add-trip cltl-cmd nil nil)) (attachment (dolist (x (cdr cltl-cmd)) (let ((name (if (symbolp x) x (car x)))) (unless (eq name *special-cltl-cmd-attachment-mark-name*) (install-for-add-trip (cond ((symbolp x) (set-attachment-symbol-form x nil)) (t (set-attachment-symbol-form name (cdr x)))) nil nil))))))))) (value nil))
eq-symbol-function-possibly-unmemoizedmacro
(defmacro eq-symbol-function-possibly-unmemoized (fn sym) (assert (and (symbolp fn) (symbolp sym))) `(or (eq ,FN (symbol-function ,SYM)) (let ((entry (gethash ,SYM *memoize-info-ht*))) (and entry (eq ,FN (access memoize-info-ht-entry entry :old-fn))))))
hcomp-alists-from-htsfunction
(defun hcomp-alists-from-hts nil (let ((fn-alist nil) (const-alist nil) (macro-alist nil)) (maphash (lambda (k val) (push (cons k (cond ((eq val *hcomp-fake-value*) nil) ((not (fboundp k)) nil) ((reclassifying-value-p val) (let ((fn (unmake-reclassifying-value val))) (and (eq-symbol-function-possibly-unmemoized fn k) 'semi))) (t (eq-symbol-function-possibly-unmemoized val k)))) fn-alist)) *hcomp-fn-ht*) (maphash (lambda (k val) (push (cons k (cond ((eq val *hcomp-fake-value*) nil) ((not (boundp k)) nil) ((eq val (symbol-value k)) t) (t nil))) const-alist)) *hcomp-const-ht*) (maphash (lambda (k val) (push (cons k (cond ((eq val *hcomp-fake-value*) nil) ((and val (eq val (macro-function k))) t) (t nil))) macro-alist)) *hcomp-macro-ht*) (mv fn-alist const-alist macro-alist)))
*boot-strap-pass-2-acl2-loop-only-fns*constant
(defconst *boot-strap-pass-2-acl2-loop-only-fns* '(apply$-prim apply$-lambda))
other
(defvar *proclaim-dfs-ht* (make-hash-table :test (function eq)))
proclaim-dfsfunction
(defun proclaim-dfs (fn &aux (wrld (w *the-live-state*))) (cond ((string>= (lisp-implementation-version) "2.5.6") nil) ((member-eq fn *stobjs-out-invalid*) nil) (t (let ((stobjs-in (getpropc fn 'stobjs-in nil wrld)) (stobjs-out (getpropc fn 'stobjs-out '(nil) wrld))) (assert stobjs-out) (cond ((or (member-eq :df stobjs-in) (member-eq :df stobjs-out)) (let ((dcl `(ftype (function ,(NCONC (LOOP FOR X IN STOBJS-IN COLLECT (IF (EQ X :DF) 'DOUBLE-FLOAT T)) '(&OPTIONAL)) (values ,@(LOOP FOR X IN STOBJS-OUT COLLECT (IF (EQ X :DF) 'DOUBLE-FLOAT T)) &optional)) ,FN))) (setf (gethash fn *proclaim-dfs-ht*) dcl) (proclaim dcl))) ((gethash fn *proclaim-dfs-ht*) (remhash fn *proclaim-dfs-ht*)) (t nil))))))
other
(defun-one-output add-trip
(world-name world-key trip status)
(global-symbol (car trip))
(*1*-symbol? (car trip))
(without-interrupts (let ((alist (get (car trip) world-key)))
(setf (get (car trip) world-key)
(destructive-push-assoc (cadr trip)
(cddr trip)
alist
world-key))
(setf (car status) (cadr trip))
(setf (cdr status) alist)))
(when (and (eq world-name 'current-acl2-world)
(eq (car trip) 'cltl-command)
(eq (cadr trip) 'global-value)
(consp (cddr trip)))
(let* ((wrld (w *the-live-state*)) (boot-strap-flg (f-get-global 'boot-strap-flg *the-live-state*))
(cltl-cmd (cddr trip)))
(case (car cltl-cmd)
(defuns (let ((ignorep (caddr cltl-cmd)) (defun-mode (cadr cltl-cmd))
(new-defs nil)
(new-*1*-defs nil))
(without-interrupts (dolist (def (cdddr cltl-cmd))
(cond ((and boot-strap-flg
(not (global-val 'boot-strap-pass-2 wrld))) (or (fboundp (car def))
(interface-er "~x0 is not fboundp!" (car def)))
(or (member-eq (car def)
`(mv-list return-last
wormhole-eval
,@*DF-PRIMITIVES*
,@*DEFUN-OVERRIDES*))
(setq new-*1*-defs
(cons (list* 'oneify-cltl-code
defun-mode
def
(if (consp ignorep)
(cdr ignorep)
nil))
new-*1*-defs))))
((and (not ignorep)
(equal *main-lisp-package-name*
(symbol-package-name (car def)))) (interface-er "It is illegal to redefine a function in ~
the main Lisp package, such as ~x0!"
(car def)))
((and (consp ignorep) (eq (car ignorep) 'defstobj)) (maybe-push-undo-stack 'defun (car def) ignorep))
((and boot-strap-flg
(or (member-eq (car def) *boot-strap-pass-2-acl2-loop-only-fns*)
(member-eq (car def) *df-primitives*)
(member-eq (car def) *defun-overrides*))))
(t (maybe-push-undo-stack 'defun (car def) ignorep)
(unless ignorep
(proclaim-dfs (car def))
(setq new-defs (cons (cons 'defun def) new-defs)))
(setq new-*1*-defs
(cons (list* 'oneify-cltl-code
defun-mode
def
(if (consp ignorep)
(cdr ignorep)
nil))
new-*1*-defs)))))
(setf (cdr status) 'maybe-push-undo-stack-completed))
(setq new-defs (nconc new-defs new-*1*-defs))
(install-defs-for-add-trip new-defs
(eq ignorep 'reclassifying)
wrld
(not boot-strap-flg)
t)
(cond ((not (eq (f-get-global 'compiler-enabled *the-live-state*) t)))
((or (and boot-strap-flg)) (dolist (def new-defs)
(when def
(let ((name (cond ((eq (car def) 'defun) (cadr def))
((eq (car def) 'oneify-cltl-code) (car (caddr def)))
(t (error "Implementation error: ~
unexpected form in ~
add-trip, ~x0"
def)))))
(eval `(compile ',NAME)))))))))
((defstobj defabsstobj) (let* ((absp (eq (car cltl-cmd) 'defabsstobj)) (name (nth 1 cltl-cmd))
(the-live-name (nth 2 cltl-cmd))
(init (nth 3 cltl-cmd))
(raw-defs (nth 4 cltl-cmd))
(discriminator (nth 5 cltl-cmd))
(ax-defs (nth 6 cltl-cmd))
(non-executable (access defstobj-redundant-raw-lisp-discriminator-value
(cdr discriminator)
:non-executable))
(new-defs nil))
(without-interrupts (maybe-push-undo-stack (car cltl-cmd) name)
(maybe-push-undo-stack 'defconst '*user-stobj-alist*)
(setf (cdr status) 'maybe-push-undo-stack-completed))
(let ((var (st-lst name)))
(or (boundp var) (eval `(defg ,VAR nil))))
(setf (get the-live-name 'redundant-raw-lisp-discriminator)
discriminator)
(cond ((assoc-eq name *user-stobj-alist*) (assert (not (member-eq name *non-executable-user-stobj-lst*)))
(cond (non-executable (setq *user-stobj-alist*
(remove1-assoc-eq name *user-stobj-alist*))
(push name *non-executable-user-stobj-lst*))
(t (setq *user-stobj-alist*
(put-assoc-eq name (eval init) *user-stobj-alist*)))))
(non-executable (pushnew name *non-executable-user-stobj-lst* :test 'eq))
(t (when (member-eq name *non-executable-user-stobj-lst*)
(setq *non-executable-user-stobj-lst*
(remove1 name *non-executable-user-stobj-lst*)))
(push (cons name (eval init)) *user-stobj-alist*)))
(dolist (def raw-defs)
(cond ((and boot-strap-flg
(not (global-val 'boot-strap-pass-2 wrld))) (or (fboundp (car def))
(interface-er "~x0 is not fboundp!" (car def))))
((equal *main-lisp-package-name*
(symbol-package-name (car def))) (interface-er "It is illegal to redefine a function in the main Lisp ~
package, such as ~x0!"
(car def)))
(t (let ((def (cond (absp (cons 'defmacro def))
((member-equal *stobj-inline-declare* def) (cons 'defabbrev (remove-stobj-inline-declare def)))
(t (proclaim-dfs (car def)) (cons 'defun def)))))
(setq new-defs (cons def new-defs))))))
(dolist (def ax-defs)
(setq new-defs
(cons (list* 'oneify-cltl-code :logic def name) new-defs)))
(setq new-defs (nreverse new-defs))
(install-defs-for-add-trip new-defs
nil
wrld
(not boot-strap-flg)
t)
(when (and (eq (f-get-global 'compiler-enabled *the-live-state*) t)
(default-compile-fns wrld))
(dolist (def new-defs)
(when def
(let ((name (cond ((or (eq (car def) 'defun)
(eq (car def) 'defabbrev)
(eq (car def) 'defmacro)) (cadr def))
((eq (car def) 'oneify-cltl-code) (car (caddr def)))
(t (error "Implementation error: ~
unexpected form in add-trip, ~x0"
def)))))
(eval `(compile ',NAME))))))))
(defpkg (without-interrupts (maybe-push-undo-stack 'defpkg (cadr cltl-cmd))
(setf (cdr status) 'maybe-push-undo-stack-completed))
(eval (cons 'defpkg (cdr cltl-cmd))))
(defconst (cond (boot-strap-flg (or (boundp (cadr cltl-cmd))
(interface-er "~x0 is not boundp!" (cadr cltl-cmd)))
(or (get (cadr cltl-cmd) 'redundant-raw-lisp-discriminator)
(setf (get (cadr cltl-cmd) 'redundant-raw-lisp-discriminator)
(list* 'defconst (caddr cltl-cmd) (cadddr cltl-cmd)))))
((equal *main-lisp-package-name*
(symbol-package-name (cadr cltl-cmd))) (interface-er "It is illegal to redefine a defconst in the ~
main Lisp package, such as ~x0!"
(cadr cltl-cmd)))
(t (without-interrupts (let* ((name (cadr cltl-cmd)) (form (caddr cltl-cmd))
(val (cadddr cltl-cmd)))
(maybe-push-undo-stack 'defconst name)
(setf (get name 'redundant-raw-lisp-discriminator)
(list* 'defconst form val))
(install-for-add-trip (ifat-defparameter name val form)
nil
t))
(setf (cdr status) 'maybe-push-undo-stack-completed)))))
(defmacro (cond ((and boot-strap-flg
(not (global-val 'boot-strap-pass-2 wrld))) (or (fboundp (cadr cltl-cmd))
(interface-er "~x0 is not fboundp!" (cadr cltl-cmd))))
((equal *main-lisp-package-name*
(symbol-package-name (cadr cltl-cmd))) (interface-er "It is illegal to redefine a macro in the ~
main Lisp package, such as ~x0!"
(cadr cltl-cmd)))
(t (without-interrupts (maybe-push-undo-stack 'defmacro (cadr cltl-cmd))
(setf (cdr status) 'maybe-push-undo-stack-completed))
(install-for-add-trip cltl-cmd nil t))))
(attachment (dolist (x (cdr cltl-cmd))
(let ((name (if (symbolp x)
x
(car x))))
(without-interrupts (maybe-push-undo-stack 'attachment name)
(setf (cdr status) 'maybe-push-undo-stack-completed))
(unless (eq name *special-cltl-cmd-attachment-mark-name*)
(push name *defattach-fns*)
(install-for-add-trip (cond ((symbolp x) (set-attachment-symbol-form x nil))
(t (set-attachment-symbol-form name (cdr x))))
nil
t)))))
(memoize (without-interrupts (maybe-push-undo-stack 'memoize (cadr cltl-cmd))
(setf (cdr status) 'maybe-push-undo-stack-completed))
(let* ((tuple cltl-cmd) (cl-defun (nth 4 tuple)))
(assert$ cl-defun
(with-overhead (nth 13 tuple)
(memoize-fn (nth 1 tuple)
:condition (nth 2 tuple)
:inline (nth 3 tuple)
:cl-defun cl-defun
:formals (nth 5 tuple)
:stobjs-in (nth 6 tuple)
:stobjs-out (nth 7 tuple)
:commutative (nth 9 tuple)
:forget (nth 10 tuple)
:memo-table-init-size (nth 11 tuple)
:aokp (nth 12 tuple)
:invoke (nth 14 tuple))))))
(unmemoize (without-interrupts (maybe-push-undo-stack 'unmemoize (cadr cltl-cmd))
(unmemoize-fn (cadr cltl-cmd))
(setf (cdr status) 'maybe-push-undo-stack-completed))))))
(let ((temp (get (car trip) *current-acl2-world-key*)) (plist (symbol-plist (car trip))))
(cond ((and temp (not (eq (car plist) *current-acl2-world-key*))) (setf (symbol-plist (car trip))
(cons *current-acl2-world-key*
(cons temp (remove-current-acl2-world-key plist))))))))
other
(defun-one-output undo-trip
(world-name world-key trip)
(setf (get (car trip) world-key)
(destructive-pop-assoc (cadr trip)
(get (car trip) world-key)))
(cond ((and (eq world-name 'current-acl2-world)
(eq (car trip) 'cltl-command)
(eq (cadr trip) 'global-value)
(consp (cddr trip))) (case (car (cddr trip))
(defuns (dolist (tuple (cdddr (cddr trip)))
(maybe-pop-undo-stack (car tuple))))
((defstobj defabsstobj) (let ((name (nth 1 (cddr trip))))
(maybe-pop-undo-stack name)
(maybe-pop-undo-stack '*user-stobj-alist*)))
(defpkg nil)
((defconst defmacro memoize unmemoize) (maybe-pop-undo-stack (cadr (cddr trip))))
(attachment (let ((lst (cdr (cddr trip))))
(dolist (x lst)
(let ((name (if (symbolp x)
x
(car x))))
(maybe-pop-undo-stack name)))))
(otherwise nil)))))
other
(defvar *bad-wrld*)
check-acl2-world-invariantfunction
(defun check-acl2-world-invariant (wrld old-wrld) (cond ((not (eq old-wrld (w *the-live-state*))) (setq *bad-wrld* wrld) (interface-er "Extend-world1 or retract-world1 has been asked to install ~ a world at a moment when the current global value of ~ 'current-acl2-world was not the installed world! The ~ world we were asked to install may be found in the variable ~ *bad-wrld*."))))
other
(defparameter *known-worlds* nil)
other
(defvar *saved-user-stobj-alist* nil)
other
(defvar *saved-non-executable-user-stobj-lst* nil)
update-wrld-structuresfunction
(defun update-wrld-structures (wrld state) (install-global-enabled-structure wrld state) (recompress-global-enabled-structure 'global-arithmetic-enabled-structure wrld) (when (not (eq *saved-user-stobj-alist* *user-stobj-alist*)) (recompress-stobj-accessor-arrays (strip-cars *user-stobj-alist*) wrld) (setq *saved-user-stobj-alist* *user-stobj-alist*)) (when (not (eq *saved-non-executable-user-stobj-lst* *non-executable-user-stobj-lst*)) (recompress-stobj-accessor-arrays *non-executable-user-stobj-lst* wrld) (setq *saved-non-executable-user-stobj-lst* *non-executable-user-stobj-lst*)) (update-memo-entries-for-attachments *defattach-fns* wrld state) nil)
other
(defun-one-output extend-world1
(name wrld)
(let ((status (cons nil nil)) (state *the-live-state*)
(pair (get name 'acl2-world-pair))
old-wrld
world-key
new-trips)
(unwind-protect-disable-interrupts-during-cleanup (progn (cond ((null pair) (setq pair
(cons nil
(if (eq name 'current-acl2-world)
*current-acl2-world-key*
(gensym))))
(pushnew name *known-worlds*)
(cond ((eq name 'current-acl2-world) (f-put-global 'current-acl2-world nil state)))
(setf (get name 'acl2-world-pair) pair)))
(setq old-wrld (car pair))
(setq world-key (cdr pair))
(cond ((eq name 'current-acl2-world) (check-acl2-world-invariant wrld old-wrld)))
(do ((tl wrld (cdr tl)))
((equal tl old-wrld))
(cond ((null tl) (setq *bad-wrld* wrld)
(er hard
'extend-world1
"Extend-world1 was called upon to ``extend'' ~x0. But the ~
world supplied to extend-world1, which is now the value of ~
the Lisp global *bad-wrld*, is not an extension of the ~
current ~x0. The alist corresponding to the current ~x0 ~
may be obtained via ~x1. No properties were modified -- ~
that is, the symbol-plists still reflect the ~
pre-extend-world1 ~x0. You may report this problem to the ~
ACL2 implementors."
name
`(car (get ',NAME 'acl2-world-pair))))
(t (push (car tl) new-trips))))
(with-more-warnings-suppressed (loop (when (null new-trips) (return))
(let ((trip (car new-trips)))
(setf (cdr status) nil)
(add-trip name world-key trip status)
(setq new-trips (cdr new-trips))))
(setf (car pair) wrld)))
(cond ((eq (car pair) wrld) (when (eq name 'current-acl2-world)
(f-put-global 'current-acl2-world wrld state)
(update-wrld-structures wrld state)))
(t (when (eq name 'current-acl2-world)
(format t
"~%~
; *Note*: Interrupt or error detected while extending the~%~
; ACL2 logical world; now reverting the world with~%~
; interrupts disabled. This should complete~%~
; quickly.~&~%")
(finish-output))
(let* ((alist (cdr status)) (remaining (if (eq alist 'maybe-push-undo-stack-completed)
(assert$ (consp new-trips) (1- (length new-trips)))
(length new-trips)))
(w (nthcdr remaining wrld)))
(when (consp alist)
(assert$ (consp new-trips)
(destructive-pop-assoc (car status) alist)))
(setf (car pair) w)
(when (eq name 'current-acl2-world)
(f-put-global 'current-acl2-world w state)
(update-wrld-structures w state))
(retract-world1 name old-wrld))))))
wrld)
other
(defun-one-output retract-world1
(name wrld)
(let ((state *the-live-state*) (pair (get name 'acl2-world-pair))
(processed 0)
old-wrld
world-key)
(unwind-protect-disable-interrupts-during-cleanup (progn (cond ((null pair) (setq pair
(cons nil
(if (eq name 'current-acl2-world)
*current-acl2-world-key*
(gensym))))
(pushnew name *known-worlds*)
(cond ((eq name 'current-acl2-world) (f-put-global 'current-acl2-world nil state)))
(setf (get name 'acl2-world-pair) pair)))
(setq old-wrld (car pair))
(setq world-key (cdr pair))
(cond ((eq name 'current-acl2-world) (check-acl2-world-invariant wrld old-wrld)))
(do ((tl old-wrld (cdr tl)))
((equal tl wrld))
(cond ((null tl) (setq *bad-wrld* wrld)
(er hard
'retract-world1
"Retract-world1 was called upon to ``retract'' ~x0. But the ~
world supplied to retract-world1, which is now the value of ~
the Lisp global variable *bad-wrld*, is not a retraction of ~
the currently installed ~x0. The alist corresponding to ~
the current ~x0 may be obtained via ~x1. Unfortunately, ~
this problem was not discovered until all of the properties ~
in ~x0 were removed.~@2"
name
`(car (get ',NAME 'acl2-world-pair))
(cond ((eq name 'current-acl2-world) " Your session is not recoverable. You may report ~
this issue to the ACL2 implementors, as a workaround ~
might be possible.")
(t ""))))
(t (without-interrupts (undo-trip name world-key (car tl))
(incf processed)))))
(setf (car pair) wrld))
(cond ((eq (car pair) wrld) (when (eq name 'current-acl2-world)
(f-put-global 'current-acl2-world wrld state)
(when (not (find-non-hidden-package-entry (current-package state)
(known-package-alist state)))
(f-put-global 'current-package "ACL2" state))
(update-wrld-structures wrld state)))
((and (eq name 'current-acl2-world)
(boundp '*bad-wrld*)
*bad-wrld*))
(t (let ((w (nthcdr processed old-wrld)))
(setf (car pair) w)
(when (eq name 'current-acl2-world)
(f-put-global 'current-acl2-world w state)
(format t
"~%~
; *Note*: Interrupt or error detected while retracting~%~
; the ACL2 logical world; now extending the~%~
; world (~s triples) with interrupts disabled.~%~
; This may take awhile.~&~%"
processed)
(finish-output))
(extend-world1 name old-wrld))))))
wrld)
other
(defun-one-output virginp (name new-type) (and (symbolp name) (if (member-eq new-type '(function macro constrained-function t)) (not (or (fboundp name) (macro-function name) (special-form-or-op-p name))) t) (if (member-eq new-type '(const stobj stobj-live-var t)) (not (boundp name)) t)))
other
(defun-one-output chk-virgin-msg2 (name new-type wrld state) (cond ((virginp name new-type) nil) ((f-get-global 'boot-strap-flg state) (setf (get name '*predefined*) t) nil) ((getpropc name 'redefined nil wrld) nil) (t (let ((reason (cond ((not (symbolp name)) "it is not a symbol") ((member-eq new-type '(function macro constrained-function t)) (cond ((special-form-or-op-p name) "it is a special form") ((macro-function name) "it has a macro definition") ((fboundp name) "it has a function definition") (t "there is an inconsistency in the definition of ~ virginp and chk-virgin2"))) ((member-eq new-type '(const stobj stobj-live-var t)) (cond ((boundp name) "it has a top level binding") (t "there is an inconsistency in the definition of ~ virginp and chk-virgin2"))) (t "there is an inconsistency in the definition of ~ virginp and chk-virgin2"))) (suggestion (let ((str " If earlier you accidentally made this ~ definition or assignment outside the ACL2 ~ loop, then you might consider exiting the ~ ACL2 loop and executing appropriate ~ Common Lisp to erase those mistakes. ~ This is a potentially perilous act unless ~ you are sure these names were introduced ~ by you and are not involved in any ~ logical code. ~#3~[~/To erase a function ~ or macro definition use (fmakunbound! ~ '~x0). ~]~#4~[~/To erase a variable ~ setting use (makunbound '~x0). ~]")) (cond ((not (symbolp name)) "") ((member-eq new-type '(function macro constrained-function t)) (cond ((special-form-or-op-p name) "") (t str))) (t str))))) (msg "It is illegal to define ~x0 because ~@1 in raw Common Lisp.~@2" name reason suggestion (if (member-eq new-type '(function macro constrained-function t)) 1 0) (if (member-eq new-type '(const stobj stobj-live-var t)) 1 0))))))
other
(defun-one-output chk-package-reincarnation-import-restrictions2 (name proposed-imports) (let ((pkg (find-package name)) (temp (find-package-entry name *ever-known-package-alist*))) (cond (pkg (cond (temp (check-proposed-imports name temp proposed-imports) nil) ((member-equal name *defpkg-virgins*) nil) (t (interface-er "It is illegal to defpkg ~x0 because a package of that name already ~ exists in this lisp." name)))) (t nil))))
other
(defun-one-output enter-boot-strap-mode (system-books-dir operating-system) (acl2-unwind *ld-level* nil) (push nil *acl2-unwind-protect-stack*) (set-w 'retraction nil *the-live-state*) (do-symbols (sym (find-package "ACL2_GLOBAL_ACL2")) (makunbound sym)) (do-symbols (sym (find-package (concatenate 'string *global-package-prefix* *main-lisp-package-name*))) (makunbound sym)) (do-symbols (sym (find-package "ACL2_GLOBAL_KEYWORD")) (makunbound sym)) (initialize-state-globals) (f-put-global 'global-enabled-structure (initial-global-enabled-structure "ENABLED-ARRAY-") *the-live-state*) (f-put-ld-specials *initial-ld-special-bindings* nil *the-live-state*) (let ((project-dir-alist (acons :system (cond (system-books-dir (let* ((dir (unix-full-pathname (cond ((symbolp system-books-dir) (symbol-name system-books-dir)) ((stringp system-books-dir) system-books-dir) (t (er hard 'initialize-acl2 "Unable to complete initialization, ~ because the supplied system books ~ directory, ~x0, is not a string." system-books-dir))))) (msg (bad-lisp-stringp dir))) (when msg (interface-er "The value of the system-books-dir argument of ~ ENTER-BOOT-STRAP-MODE, which is ~x0, is not a legal ~ ACL2 string.~%~@1" dir msg)) (canonical-dirname! (maybe-add-separator dir) 'enter-boot-strap-mode *the-live-state*))) (t (concatenate 'string (canonical-dirname! (our-pwd) 'enter-boot-strap-mode *the-live-state*) "books/"))) nil))) (set-w 'extension (primordial-world operating-system project-dir-alist) *the-live-state*)) (f-put-global 'inhibit-output-lst '(proof-tree) *the-live-state*) (acl2-unwind *ld-level* nil))
other
(defun-one-output move-current-acl2-world-key-to-front (wrld) (cond ((null wrld) nil) ((eq (car (symbol-plist (caar wrld))) *current-acl2-world-key*) (move-current-acl2-world-key-to-front (cdr wrld))) (t (let ((temp (get (caar wrld) *current-acl2-world-key*))) (cond (temp (setf (symbol-plist (caar wrld)) (cons *current-acl2-world-key* (cons temp (remove-current-acl2-world-key (symbol-plist (caar wrld))))))))) (move-current-acl2-world-key-to-front (cdr wrld)))))
other
(progn (defun-overrides mfc-ts-fn (term mfc state forcep) (mv-let (ans ttree) (mfc-ts-raw term mfc state forcep) (declare (ignore ttree)) ans)) (defun-overrides mfc-ts-ttree (term mfc state forcep) (mfc-ts-raw term mfc state forcep)) (defun-overrides mfc-rw-fn (term obj equiv-info mfc state forcep) (mv-let (ans ttree) (mfc-rw-raw term nil obj equiv-info mfc 'mfc-rw state forcep) (declare (ignore ttree)) ans)) (defun-overrides mfc-rw-ttree (term obj equiv-info mfc state forcep) (mfc-rw-raw term nil obj equiv-info mfc 'mfc-rw state forcep)) (defun-overrides mfc-rw+-fn (term alist obj equiv-info mfc state forcep) (mfc-rw-raw term alist obj equiv-info mfc 'mfc-rw+ state forcep)) (defun-overrides mfc-rw+-ttree (term alist obj equiv-info mfc state forcep) (mv-let (ans ttree) (mfc-rw-raw term alist obj equiv-info mfc 'mfc-rw+ state forcep) (declare (ignore ttree)) ans)) (defun-overrides mfc-relieve-hyp-fn (hyp alist rune target bkptr mfc state forcep) (mfc-relieve-hyp-raw hyp alist rune target bkptr mfc state forcep)) (defun-overrides mfc-relieve-hyp-ttree (hyp alist rune target bkptr mfc state forcep) (mv-let (ans ttree) (mfc-relieve-hyp-raw hyp alist rune target bkptr mfc state forcep) (declare (ignore ttree)) ans)) (defun-overrides mfc-ap-fn (term mfc state forcep) (mfc-ap-raw term mfc state forcep)))
other
(defun-one-output exit-boot-strap-mode nil (push nil *acl2-unwind-protect-stack*) (set-w 'extension (end-prehistoric-world (w *the-live-state*)) *the-live-state*) (f-put-global 'boot-strap-flg nil *the-live-state*) (acl2-unwind *ld-level* nil) (f-put-global 'inhibit-output-lst nil *the-live-state*) (f-put-global 'slow-array-action :warning *the-live-state*) (stop-proof-tree-fn *the-live-state*) (f-put-global 'ld-skip-proofsp nil *the-live-state*) (move-current-acl2-world-key-to-front (w *the-live-state*)) (progn (initialize-never-memoize-ht) (acl2h-init-memoizations)) (setq *hard-error-is-error* nil) nil)
other
(defun-one-output ld-alist-raw (standard-oi ld-skip-proofsp ld-error-action) `((standard-oi . ,STANDARD-OI) (standard-co . ,*STANDARD-CO*) (proofs-co . ,*STANDARD-CO*) (current-package . "ACL2") (useless-runes) (ld-skip-proofsp . ,LD-SKIP-PROOFSP) (ld-redefinition-action) (ld-prompt . ,(IF LD-SKIP-PROOFSP NIL T)) (ld-missing-input-ok) (ld-always-skip-top-level-locals) (ld-pre-eval-filter . :all) (ld-pre-eval-print . ,(IF LD-SKIP-PROOFSP NIL T)) (ld-post-eval-print . :command-conventions) (ld-evisc-tuple . ,(ABBREV-EVISC-TUPLE *THE-LIVE-STATE*)) (ld-error-triples . t) (ld-error-action . ,LD-ERROR-ACTION) (ld-query-control-alist . t) (ld-verbose . t) (ld-user-stobjs-modified-warning)))
enter-boot-strap-pass-2function
(defun enter-boot-strap-pass-2 nil (push nil *acl2-unwind-protect-stack*) (set-w 'extension (global-set 'boot-strap-pass-2 t (w *the-live-state*)) *the-live-state*) (acl2-unwind *ld-level* nil) (memoize-init) (ld-fn (ld-alist-raw '((logic)) t :error) *the-live-state* nil))
*acl2-pass-2-files*constant
(defconst *acl2-pass-2-files* '("axioms" "memoize" "hons" "serialize" "boot-strap-pass-2-a" "float-a" "float-b" "apply-prim" "apply-constraints" "apply" "boot-strap-pass-2-b"))
other
(assert (subsetp-equal *acl2-pass-2-files* *acl2-files*))
our-update-htfunction
(defun our-update-ht (key val ht when-pass-2-p) (let ((old (gethash key ht)) (val (if when-pass-2-p (list :when-pass-2-p val) val))) (setf (gethash key ht) (cond ((and (consp old) (eq (car old) :multiple)) (list* (car old) val (cdr old))) (old (list :multiple val old)) (t val)))))
note-fns-in-formfunction
(defun note-fns-in-form (form ht when-pass-2-p) (and (consp form) (case (car form) ((defun defund defn defproxy defun-nx defun-one-output defun-df-unary defun-df-binary defstub defmacro defmacro-untouchable defabbrev defun@par defmacro-last defun-overrides defun-with-guard-check defun-sk defdeprecate defun-inline defund-inline defun-notinline defund-notinline) (our-update-ht (cadr form) form ht when-pass-2-p)) (save-def (note-fns-in-form (cadr form) ht when-pass-2-p)) (defun-for-state (our-update-ht (defun-for-state-name (cadr form)) form ht when-pass-2-p)) ((define-pc-atomic-macro define-pc-bind* define-pc-help define-pc-macro define-pc-meta define-pc-primitive) (let ((name (make-official-pc-command (if (eq (car form) 'define-pc-meta-or-macro-fn) (nth 2 form) (nth 1 form))))) (our-update-ht name form ht when-pass-2-p))) ((mutual-recursion mutual-recursion@par progn) (loop for x in (cdr form) do (note-fns-in-form x ht when-pass-2-p))) ((when-pass-2) (loop for x in (cdr form) do (note-fns-in-form x ht t))) ((encapsulate when) (loop for x in (cddr form) do (note-fns-in-form x ht when-pass-2-p))) (partial-encapsulate (loop for x in (cdddr form) do (note-fns-in-form x ht when-pass-2-p))) ((skip-proofs local) (note-fns-in-form (cadr form) ht when-pass-2-p)) (defrec (our-update-ht (record-changer-function-name (cadr form)) form ht when-pass-2-p)) (state-global-let* (note-fns-in-form (caddr form) ht when-pass-2-p)) (df-constrained-functions-intro (strip-cars *df-function-sigs-exec*)) (df-non-constrained-functions-intro (loop for ev in (df-non-constrained-functions-events) when (eq (car ev) 'defun) collect (cadr ev))) ((add-custom-keyword-hint add-macro-alias add-macro-fn assert declaim def-basic-type-sets defbadge defwarrant defattach defaxiom defconst defconstant defequiv defg define-@par-macros define-atomically-modifiable-counter define-trusted-clause-processor deflabel deflock defparameter defpkg defstruct deftheory defthm defthmd deftype defun-*1* defun-df-*1*-unary defun-df-*1*-binary defun-df-*1*-from-function-sigs defv defvar error eval eval-when f-put-global in-package in-theory initialize-state-globals let logic make-waterfall-parallelism-constants make-waterfall-printing-constants memoize pprogn program push reset-future-parallelism-variables set-duplicate-keys-action set-guard-msg set-invisible-fns-table set-tau-auto-mode set-waterfall-parallelism setq system-events system-verify-guards table value verify-guards verify-termination-boot-strap make-event make-apply$-prim-body-fn-raw set-brr-data-attachments set-compile-fns set-ignore-ok set-irrelevant-formals-ok set-raw-mode set-table-guard set-table-guard-doc) nil) (t (error "Unexpected type of form, ~s. See note-fns-in-form." (car form))))))
note-fns-in-filefunction
(defun note-fns-in-file (filename ht) (with-open-file (str filename :direction :input) (let ((avrc (cons nil nil)) x) (loop while (not (eq (setq x (read str nil avrc)) avrc)) do (note-fns-in-form x ht nil)))))
note-fns-in-filesfunction
(defun note-fns-in-files (filenames ht loop-only-p) (let ((*features* (if loop-only-p (cons :acl2-loop-only *features*) (remove :acl2-loop-only *features*)))) (loop for filename in filenames do (note-fns-in-file filename ht))))
raw-source-name-pfunction
(defun raw-source-name-p (filename-without-extension) (let ((len (length filename-without-extension))) (and (<= 4 len) (equal (subseq filename-without-extension (- len 4) len) "-raw"))))
other
(defvar *check-built-in-constants-debug* nil)
fns-different-wrt-acl2-loop-onlyfunction
(defun fns-different-wrt-acl2-loop-only (acl2-files) (flet ((when-pass-2-p (val) (and (consp val) (if (eq (car val) :multiple) (assoc-eq :when-pass-2-p (cdr val)) (eq (car val) :when-pass-2-p))))) (let ((logic-filenames (loop for x in acl2-files when (not (raw-source-name-p x)) collect (concatenate 'string x ".lisp"))) (raw-filenames (loop for x in acl2-files collect (concatenate 'string x ".lisp"))) (ht-raw (make-hash-table :test 'eq)) (ht-logic (make-hash-table :test 'eq)) (when-pass-2-result nil) (macro-result nil) (program-mode-result nil) (logic-mode-result nil) (wrld (w *the-live-state*))) (note-fns-in-files raw-filenames ht-raw nil) (note-fns-in-files logic-filenames ht-logic t) (maphash (lambda (key logic-val) (progn (assert (symbolp key)) (let ((raw-val (gethash key ht-raw))) (or (equalp logic-val raw-val) (let ((x (if *check-built-in-constants-debug* (list key :logic logic-val :raw raw-val) key)) (when-pass-2-p (or (when-pass-2-p logic-val) (when-pass-2-p raw-val)))) (cond ((and when-pass-2-p (not (and (eq (car logic-val) :when-pass-2-p) (consp raw-val) (if (eq (car raw-val) :multiple) (loop for form in (cdr raw-val) always (not (and (consp (car form)) (eq (car form) :when-pass-2-p)))) (not (eq (car raw-val) :when-pass-2-p)))))) (push x when-pass-2-result)) ((getpropc key 'macro-body nil wrld) (push x macro-result)) ((eq (symbol-class key wrld) :program) (push x program-mode-result)) (t (push x logic-mode-result)))))))) ht-logic) (maphash (lambda (key raw-val) (progn (assert (symbolp key)) (when (not (gethash key ht-logic)) (let ((x (if *check-built-in-constants-debug* (list key :raw raw-val) key))) (cond ((when-pass-2-p raw-val) (push x when-pass-2-result)) ((assoc key *primitive-formals-and-guards* :test 'eq)) ((getpropc key 'macro-body nil wrld) (push x macro-result)) (t (let ((c (getpropc key 'symbol-class nil wrld))) (when c (if (eq c :program) (push x program-mode-result) (push x logic-mode-result)))))))))) ht-raw) (mv when-pass-2-result macro-result program-mode-result logic-mode-result))))
collect-monadic-booleansfunction
(defun collect-monadic-booleans (fns ens wrld) (cond ((endp fns) nil) ((and (equal (arity (car fns) wrld) 1) (ts= (mv-let (ts ttree) (type-set (fcons-term* (car fns) '(v)) nil nil nil ens wrld nil nil nil) (declare (ignore ttree)) ts) *ts-boolean*)) (cons (car fns) (collect-monadic-booleans (cdr fns) ens wrld))) (t (collect-monadic-booleans (cdr fns) ens wrld))))
check-invariant-riskfunction
(defun check-invariant-risk nil (let ((bad (remove-duplicates-eq (loop for trip in (w *the-live-state*) when (and (eq (cadr trip) 'invariant-risk) (not (or (cdr (assoc-eq (car trip) *boot-strap-invariant-risk-alist*)) (member-eq (car trip) 'nil)))) collect (car trip))))) (or (null bad) (error "Each function symbol in the following non-empty list ~%~ has unexpected invariant-risk:~%~s.~%~ You can eliminate this error by doing the following for ~%~ each such symbol: either map it to nil in ~%~ *BOOT-STRAP-INVARIANT-RISK-ALIST*, or else add it to the ~%~ list of ``acceptable exceptions'' in the definition of ~%~ check-invariant-risk." bad))) (let ((bad (loop for tuple in *super-defun-wart-table* when (and (not (member-eq (car tuple) (global-val 'untouchable-fns (w *the-live-state*)))) (member-eq 'state (caddr tuple)) (cadr tuple) (not (equal (cadr tuple) '(state))) (not (member-eq (car tuple) '(read-char$ read-byte$ read-object princ$ write-byte$ print-object$-fn makunbound-global put-global open-input-channel open-output-channel get-output-stream-string$-fn close-input-channel close-output-channel write-user-stobj-alist)))) collect (car tuple)))) (or (loop for x in bad always (cdr (assoc-eq x *boot-strap-invariant-risk-alist*))) (error "It is probably necessary to modify ~s to map each symbol in ~%~ the following list to t:~%~s" '*boot-strap-invariant-risk-alist* (loop for x in bad when (not (cdr (assoc-eq x *boot-strap-invariant-risk-alist*))) collect x)))))
computed-type-expr-to-type-spec-alistfunction
(defun computed-type-expr-to-type-spec-alist (state) (pair-type-expressions-with-type-specs *type-spec-templates* '((-3 . int-lo) (5 . int-hi) (2 . nat) (-1/7 . rat-lo) (1/11 . rat-hi)) '(('-3 . int-lo) ('5 . int-hi) ('2 . nat) ('-1/7 . rat-lo) ('1/11 . rat-hi)) nil (w state)))
state-global-let*-untouchable-alistfunction
(defun state-global-let*-untouchable-alist nil (let (fn (wrld (w *the-live-state*)) (n-s '(nil state))) (loop for x in (sort (copy-list *initial-untouchable-vars*) (function symbol<)) when (or (and (equal (stobjs-in (setq fn (packn (list 'set- x '-state))) wrld) n-s) (equal (stobjs-out fn wrld) '(state)) (not (member-eq fn *initial-untouchable-fns*))) (and (equal (stobjs-in (setq fn (packn (list 'set- x))) wrld) n-s) (equal (stobjs-out fn wrld) '(state)) (not (member-eq fn *initial-untouchable-fns*)))) collect (cons x fn))))
check-built-in-constantsfunction
(defun check-built-in-constants (&aux (state *the-live-state*)) (check-invariant-risk) (let ((str "The defconst of ~x0 is ~x1 but should be ~x2. To fix ~ the error, change the offending defconst to the value ~ indicated and rebuild the system. To understand why the code ~ is written this way, see the comment in ~ check-built-in-constants.")) (cond ((not (equal *force-xrune* (fn-rune-nume 'force nil t (w state)))) (interface-er str '*force-xrune* *force-xrune* (fn-rune-nume 'force nil t (w state))))) (cond ((not (equal *force-xnume* (fn-rune-nume 'force t t (w state)))) (interface-er str '*force-xnume* *force-xnume* (fn-rune-nume 'force t t (w state))))) (cond ((not (equal *immediate-force-modep-xnume* (fn-rune-nume 'immediate-force-modep t t (w state)))) (interface-er str '*immediate-force-modep-xnume* *immediate-force-modep-xnume* (fn-rune-nume 'immediate-force-modep t t (w state))))) (cond ((not (equal *tau-system-xnume* (fn-rune-nume 'tau-system t t (w state)))) (interface-er str '*tau-system-xnume* *tau-system-xnume* (fn-rune-nume 'tau-system t t (w state))))) (cond ((not (equal *rewrite-lambda-modep-xnume* (fn-rune-nume 'rewrite-lambda-modep t t (w state)))) (interface-er str '*rewrite-lambda-modep-xnume* *rewrite-lambda-modep-xnume* (fn-rune-nume 'rewrite-lambda-modep t t (w state))))) (cond ((not (equal *rewrite-lambda-modep-def-nume* (fn-rune-nume 'rewrite-lambda-modep t nil (w state)))) (interface-er str '*rewrite-lambda-modep-def-nume* *rewrite-lambda-modep-def-nume* (fn-rune-nume 'rewrite-lambda-modep t nil (w state))))) (cond ((not (equal *tau-acl2-numberp-pair* (getpropc 'acl2-numberp 'tau-pair))) (interface-er str '*tau-acl2-numberp-pair* *tau-acl2-numberp-pair* (getpropc 'acl2-numberp 'tau-pair)))) (cond ((not (equal *tau-integerp-pair* (getpropc 'integerp 'tau-pair))) (interface-er str '*tau-integerp-pair* *tau-integerp-pair* (getpropc 'integerp 'tau-pair)))) (cond ((not (equal *tau-rationalp-pair* (getpropc 'rationalp 'tau-pair))) (interface-er str '*tau-rationalp-pair* *tau-rationalp-pair* (getpropc 'rationalp 'tau-pair)))) (cond ((not (equal *tau-natp-pair* (getpropc 'natp 'tau-pair))) (interface-er str '*tau-natp-pair* *tau-natp-pair* (getpropc 'natp 'tau-pair)))) (cond ((not (equal *tau-bitp-pair* (getpropc 'bitp 'tau-pair))) (interface-er str '*tau-bitp-pair* *tau-bitp-pair* (getpropc 'bitp 'tau-pair)))) (cond ((not (equal *tau-posp-pair* (getpropc 'posp 'tau-pair))) (interface-er str '*tau-posp-pair* *tau-posp-pair* (getpropc 'posp 'tau-pair)))) (cond ((not (equal *tau-minusp-pair* (getpropc 'minusp 'tau-pair))) (interface-er str '*tau-minusp-pair* *tau-minusp-pair* (getpropc 'minusp 'tau-pair)))) (cond ((not (equal *tau-booleanp-pair* (getpropc 'booleanp 'tau-pair))) (interface-er str '*tau-booleanp-pair* *tau-booleanp-pair* (getpropc 'booleanp 'tau-pair)))) (cond ((not (equal *state-global-let*-untouchable-alist* (state-global-let*-untouchable-alist))) (interface-er str '*state-global-let*-untouchable-alist* *state-global-let*-untouchable-alist* (state-global-let*-untouchable-alist)))) (cond ((not (and (equal *min-type-set* -16384) (equal *max-type-set* 16383))) (interface-er "The minimal and maximal type-sets are incorrectly built into the ~ definition of type-alist-entryp. These type-sets get generated by ~ the call of def-basic-type-sets in type-set-a.lisp are must be ~ mentioned, as above, in axioms.lisp. Evidently, a new type-set bit ~ was added. Update type-alist-entryp."))) (cond ((not (equal *primitive-monadic-booleans* (collect-monadic-booleans (strip-cars *primitive-formals-and-guards*) (ens state) (w state)))) (interface-er str '*primitive-monadic-booleans* *primitive-monadic-booleans* (collect-monadic-booleans (strip-cars *primitive-formals-and-guards*) (ens state) (w state))))) (cond ((not (equal *type-expr-to-type-spec-alist* (computed-type-expr-to-type-spec-alist state))) (interface-er str '*type-expr-to-type-spec-alist* *type-expr-to-type-spec-alist* (computed-type-expr-to-type-spec-alist state)))) (cond ((not (getpropc 'booleanp 'tau-pair)) (interface-er "Our code for tau-term assumes that BOOLEANP is a tau predicate. But ~ it has no tau-pair property!"))) (let ((good-lst (chk-initial-built-in-clauses *initial-built-in-clauses* (w state) nil nil))) (cond (good-lst (interface-er "The defconst of *initial-built-in-clauses* is bad because at least ~ one of the records supplies an :all-fnnames that is different from ~ that computed by all-fnnames-subsumer. The correct setting is ~ shown below. To preserve the comments in the source file it might ~ be best to compare -- with EQUAL -- the elements below with the ~ corresponding elements in the current source file and just replace ~ the ones that have changed. Here is a correct setting in 1:1 ~ correspondence with the current setting: ~X01." `(defconst *initial-built-in-clauses* (list ,@GOOD-LST)) nil)))) (cond ((not (equal *bbody-alist* (merge-sort-lexorder (loop for f in *definition-minimal-theory* when (not (eq f 'mv-nth)) collect (cons f (body f t (w *the-live-state*))))))) (interface-er "There is a discrepancy between the value of *bbody-alist* and ~ its expected value.~%Actual value of ~ *bbody-alist*:~%~X01~%Expected value of *bbody-alist*:~X21" *bbody-alist* nil (merge-sort-lexorder (loop for f in *definition-minimal-theory* when (not (eq f 'mv-nth)) collect (cons f (body f t (w *the-live-state*)))))))) (mv-let (when-pass-2-result macros-found program-found logic-found) (fns-different-wrt-acl2-loop-only *acl2-files*) (flet ((my-diff (x y) (if *check-built-in-constants-debug* (loop for tuple in x when (not (member (car tuple) y :test 'eq)) collect tuple) (set-difference-eq x y)))) (let ((bad-macros (my-diff macros-found *initial-macros-with-raw-code*)) (bad-program (my-diff program-found *initial-program-fns-with-raw-code*)) (bad-logic (my-diff logic-found *initial-logic-fns-with-raw-code*))) (when (or when-pass-2-result bad-macros bad-program bad-logic) (format t "~%ERROR: Failed check for coverage of functions with~%~ acl2-loop-only code differences! Please send this~%~ error message to the ACL2 implementors. Problems are~%~ as shown below; use *check-built-in-constants-debug* = t~%~ for a verbose report.~%~ Note: (lisp-implementation-type) =~%~ ~6t~s~%~ Note: (lisp-implementation-version) =~%~ ~6t~s~%~%" (lisp-implementation-type) (lisp-implementation-version)) (when when-pass-2-result (format t "The following have #-acl2-loop-only code within ~ (when-pass-2 ...):~%~s~%~%" when-pass-2-result)) (when bad-macros (format t "The following macros differ in their #+acl2-loop-only~%~ and #-acl2-loop-only code:~%~s~%~ They probably should be added to ~s.~%~%" bad-macros '*initial-macros-with-raw-code*)) (when bad-program (format t "The following program-mode functions differ in their~%~ #+acl2-loop-only and #-acl2-loop-only code:~%~s~%~ They probably should be added to ~s.~%~%" bad-program '*initial-program-fns-with-raw-code*)) (when bad-logic (format t "The following logic-mode functions differ in their~%~ #+acl2-loop-only and #-acl2-loop-only code:~%~s~%~ They probably should be added to ~s.~%~%" bad-logic '*initial-logic-fns-with-raw-code*)) (exit-with-build-error "Check failed!"))))) (let* ((wrld (w state)) (fns (loop for fn in (append (strip-cars *ttag-fns*) *initial-untouchable-fns*) when (and (getpropc fn 'unnormalized-body nil wrld) (all-nils-or-dfs (stobjs-in fn wrld))) collect fn)) (bad (set-difference-eq fns (symbol-value '*blacklisted-apply$-fns*)))) (when bad (interface-er "The value of *blacklisted-apply$-fns* fails to include ~&0. This ~ is an error because all defined functions from *ttag-fns* and ~ *initial-untouchable-fns* with all-nils stobjs-in and stobjs-out ~ must be in *blacklisted-apply$-fns*." bad)))))
other
(defun-one-output check-none-ideal (trips acc &aux (state *the-live-state*)) (cond ((null trips) (cond ((null acc) nil) (t (exit-with-build-error "The following are :ideal mode functions that are not ~%~ non-executable. We rely in oneify-cltl-code on the absence ~%~ of such functions in the boot-strap world (see the comment ~%~ on check-none-ideal there); moreover, we want system ~%~ functions to execute efficiently, which might not be the ~%~ case for an :ideal mode function. Functions in the ~%~ following list should have their guards verified: ~s." (remove-duplicates-eq acc))))) (t (let* ((trip (car trips)) (fn (and (eq (car trip) 'event-landmark) (eq (cadr trip) 'global-value) (case (access-event-tuple-type (cddr trip)) (defun (access-event-tuple-namex (cddr trip))) (defuns (car (access-event-tuple-namex (cddr trip)))) (otherwise nil))))) (cond ((and fn (symbolp fn) (eq (symbol-class fn (w state)) :ideal) (not (eq (getpropc fn 'non-executablep) t))) (check-none-ideal (cdr trips) (cons fn acc))) (t (check-none-ideal (cdr trips) acc)))))))
check-state-globals-initializedfunction
(defun check-state-globals-initialized nil (let (bad) (do-symbols (sym (find-package "ACL2_GLOBAL_ACL2")) (when (boundp sym) (let ((acl2-sym (intern (symbol-name sym) "ACL2"))) (when (not (assoc acl2-sym *initial-global-table* :test 'eq)) (push (cons acl2-sym (symbol-value sym)) bad))))) (when bad (exit-with-build-error "The following symbols, perhaps with the values shown, need to~%~ be added to *initial-global-table*:~%~s~%" bad))))
check-slashablefunction
(defun check-slashable nil (let ((bad (loop for char in '(#\ #\ #\ #\ #\" #\# #\' #\( #\) #\, #\: #\; #\\ #\` #\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 #\|) when (not (svref *slashable-array* (char-code char))) collect (char-code char)))) (when bad (interface-er "The character code~#0~[~/s~] ~&0 must be associated with T in ~ *slashable-array*." bad))) (let ((bad (loop for i from 0 to 255 when (not (iff (member (code-char i) *slashable-chars*) (svref *slashable-array* i))) collect i))) (when bad (interface-er "Each character code in the list ~x0 is marked as slashable in exactly ~ one of *slashable-array* and *slashable-chars*; but those two ~ structures are supposed to represent the same set of slashable ~ characters." bad))) (let ((bad (loop for i from 0 to 255 when (let ((str (coerce (list (code-char i) #\A #\B (code-char i) #\U #\V (code-char i)) 'string))) (and (not (eq (ignore-errors (read-from-string str)) (intern str "ACL2"))) (not (svref *slashable-array* i)))) collect i))) (when bad (interface-er "Each character code in the list ~x0 needs to be marked as slashable ~ in both *slashable-array* and *slashable-chars*." bad))))
check-some-builtins-for-executabilityfunction
(defun check-some-builtins-for-executability nil (let ((wrld (w *the-live-state*)) ans) (do-symbols (fn (find-package "ACL2")) (when (and (eq (car (get-event fn wrld)) 'verify-termination-boot-strap) (getpropc fn 'non-executablep nil wrld)) (push fn ans))) (or (null ans) (interface-er "The initial ACL2 world has the following non-empty list of ~ functions for which get-defun-event will produce the wrong ~ result:~%~x0.~%See ACL2 function check-executable-builtins for an ~ explanation, or contact the ACL2 implementors." ans))))
other
(defun-one-output check-acl2-initialization nil (check-built-in-constants) (check-out-instantiablep (w *the-live-state*)) (check-none-ideal (w *the-live-state*) nil) (check-state-globals-initialized) (or (plist-worldp-with-formals (w *the-live-state*)) (exit-with-build-error "The initial ACL2 world does not satisfy plist-worldp-with-formals!")) (check-slashable) (check-some-builtins-for-executability) nil)
set-initial-cbdfunction
(defun set-initial-cbd nil (let ((state *the-live-state*)) (setq *initial-cbd* (our-pwd)) (cond ((and (stringp *initial-cbd*) (not (equal *initial-cbd* "")) (not (eql (char *initial-cbd* (1- (length *initial-cbd*))) #\/))) (setq *initial-cbd* (concatenate 'string *initial-cbd* "/")))) (cond ((not (absolute-pathname-string-p *initial-cbd* t (get-os))) (error "Our guess for the initial setting of cbd, ~x0, which was ~%~ generated by (our-pwd), is not a legal directory! Before ~%~ entering ACL2, please setq *initial-cbd* to a nonempty ~%~ string that represents an absolute ACL2 (i.e., Unix-style) ~%~ pathname. Sorry for the inconvenience." *initial-cbd*))) (set-cbd-fn1 *initial-cbd* state)))
initialize-acl2function
(defun initialize-acl2 (&optional (pass-2-ld-skip-proofsp 'include-book) &aux (acl2-pass-2-files *acl2-pass-2-files*) system-books-dir (*do-proclaims* nil)) (let ((dir (getenv$-raw "ACL2_SYSTEM_BOOKS"))) (when (and dir (not (equal dir ""))) (setq system-books-dir dir))) (with-warnings-suppressed (set-initial-cbd) (makunbound '*copy-of-common-lisp-symbols-from-main-lisp-package*) (let* ((*features* (cons :acl2-loop-only *features*)) (state *the-live-state*) pass-2-alist) (enter-boot-strap-mode system-books-dir (get-os)) (dolist (fl *acl2-files*) (when (not (or (equal fl "boot-strap-pass-2-a") (equal fl "boot-strap-pass-2-b") (raw-source-name-p fl))) (mv-let (er val st) (ld-fn (ld-alist-raw (or (cdr (assoc fl pass-2-alist :test (function equal))) (coerce (append (coerce fl 'list) (cons #\. (coerce *lisp-extension* 'list))) 'string)) (if (eq pass-2-ld-skip-proofsp nil) nil 'initialize-acl2) :error) *the-live-state* nil) (declare (ignore val st)) (cond (er (return-from initialize-acl2 nil)))))) (setq pass-2-alist (let ((ans nil)) (dolist (fl acl2-pass-2-files) (mv-let (erp val state) (read-file (coerce (append (coerce fl 'list) (cons #\. (coerce *lisp-extension* 'list))) 'string) *the-live-state*) (declare (ignore state)) (cond (erp (interface-er "Unable to read file ~x0!" fl)) (t (push (cons fl val) ans))))) ans)) (enter-boot-strap-pass-2) (dolist (fl acl2-pass-2-files) (mv-let (er val st) (ld-fn (ld-alist-raw (or (cdr (assoc fl pass-2-alist :test (function equal))) (interface-er "Did not find ~x0 in pass-2-alist." fl)) pass-2-ld-skip-proofsp :error) state nil) (declare (ignore val st)) (cond (er (return-from initialize-acl2 nil))))) (ld '((comp-fn :exec nil "1" state))) (exit-boot-strap-mode) (initialize-pc-acl2 *the-live-state*) (f-put-ld-specials *initial-ld-special-bindings* nil *the-live-state*) (or (check-acl2-initialization)) (cond ((or (not (probe-file *acl2-status-file*)) (delete-file *acl2-status-file*)) (with-open-file (str *acl2-status-file* :direction :output) (format str "~s" :initialized)))) (setq *saved-build-date-lst* (list (eval '(saved-build-date-string)))) t)))
our-abortfunction
(defun our-abort (condition y &aux (state *the-live-state*) (btp (member-eq (f-get-global 'debugger-enable *the-live-state*) '(:bt :break-bt :bt-break)))) (declare (ignore y)) (print-proof-tree-finish state) (when btp (print-call-history)) (cond ((or (debugger-enabledp state) (eql *ld-level* 0) (f-get-global 'boot-strap-flg state)) nil) (t (let ((*debugger-hook* nil) (*package* (find-package (current-package state))) (continue-p (if (f-get-global 'wormhole-name state) nil (and (f-get-global 'abort-soft state) (find-restart 'continue) *acl2-time-limit-boundp* (not (eql *acl2-time-limit* 0)))))) (terpri t) (format t "***********************************************") (cond (continue-p (format t "~&Note: ~A~ ~& Will attempt to exit the proof in progress;~ ~& otherwise, the next interrupt will abort the proof.~ ~& For an immediate abort see :DOC abort-soft." condition)) (t (format t "~&************ ABORTING from raw Lisp ***********") (format t "~&********** (see :DOC raw-lisp-error) **********") (cond (t (format t "~&Error: ~A" condition))))) (when btp (format t "~%NOTE: See above for backtrace.~%")) (format t "~&***********************************************~&") (when *acl2-error-msg* (format t *acl2-error-msg*)) (when (not (untouchable-fn-p 'set-debugger-enable-fn (w state) (f-get-global 'temp-touchable-fns state))) (format t "~%To enable breaks into the debugger (also see :DOC ~ acl2-customization):~&~s~&" '(set-debugger-enable t))) (force-output t) (when (eq (standard-oi state) *standard-oi*) (clear-input (get-input-stream-from-channel *standard-oi*))) (cond (continue-p (setq *acl2-time-limit* 0) (invoke-restart 'continue)) (t (our-ignore-errors (throw 'local-top-level (if (f-get-global 'wormhole-name state) :abort :our-abort)))))))))
initial-customization-filenamefunction
(defun initial-customization-filename nil (let* ((cfb00 (getenv$-raw "ACL2_CUSTOMIZATION")) (cfb0 (if (equal cfb00 "NONE") :none (and cfb00 (not (equal cfb00 "")) (extend-pathname (f-get-global 'connected-book-directory *the-live-state*) cfb00 *the-live-state*))))) (cond ((eq cfb0 :none) :none) ((and cfb0 (probe-file cfb0)) cfb0) (cfb0 (let ((*print-circle* nil)) (format t "~%ERROR: Environment variable ACL2_CUSTOMIZATION has value~%~ ~3T~a~%but file~%~3T~a~%does not appear to exist.~%~ Now quitting ACL2. To fix this problem, you may wish~%~ to fix the value of that environment variable by setting it~%~ to a valid file name, by unsetting it, or by setting it to~%~ the empty string.~%~%" cfb00 cfb0)) (exit-lisp 1)) (t (let* ((cb1 (our-merge-pathnames (f-get-global 'connected-book-directory *the-live-state*) "acl2-customization")) (cfb1 (string-append cb1 ".lsp")) (cfb1a (string-append cb1 ".lisp"))) (cond ((probe-file (pathname-unix-to-os cfb1 *the-live-state*)) cfb1) ((probe-file (pathname-unix-to-os cfb1a *the-live-state*)) cfb1a) (t (let* ((home (our-user-homedir-pathname)) (cb2 (and home (our-merge-pathnames (pathname-os-to-unix (our-truename home "Note: Calling OUR-TRUENAME from ~ INITIAL-CUSTOMIZATION-FILENAME") (os (w *the-live-state*)) *the-live-state*) "acl2-customization"))) (cfb2 (and cb2 (string-append cb2 ".lsp"))) (cfb2a (and cb2 (string-append cb2 ".lisp")))) (cond (cb2 (cond ((probe-file (pathname-unix-to-os cfb2 *the-live-state*)) cfb2) ((probe-file (pathname-unix-to-os cfb2a *the-live-state*)) cfb2a) (t nil))))))))))))
other
(defconstant *our-standard-io* (make-two-way-stream *standard-input* *standard-output*))
ld-acl2-customizationfunction
(defun ld-acl2-customization (state) (let ((customization-full-file-name (initial-customization-filename))) (cond ((or (eq customization-full-file-name :none) (f-get-global 'boot-strap-flg state)) nil) (customization-full-file-name (let ((quietp (let ((s (getenv$-raw "ACL2_CUSTOMIZATION_QUIET"))) (and s (not (equal s "")) (not (string-equal s "NIL")) (if (string-equal s "ALL") :all t))))) (when (not quietp) (fms "Customizing with ~x0.~%" (list (cons #\0 customization-full-file-name)) *standard-co* state nil)) (let ((ld-alist (put-assoc-eq 'standard-oi customization-full-file-name (put-assoc-eq 'ld-error-action :error (f-get-ld-specials *the-live-state*))))) (mv-let (erp val state) (with-suppression (with-cbd-raw state-free-global-let* :same (cond (quietp (state-free-global-let* ((inhibit-output-lst *valid-output-names*) (gag-mode nil) (print-clause-ids nil)) (let ((quiet-alist ld-alist)) (loop for pair in '((ld-verbose) (ld-pre-eval-print . :never) (ld-post-eval-print) (ld-prompt)) do (setq quiet-alist (put-assoc-eq (car pair) (cdr pair) quiet-alist))) (cond ((eq quietp :all) (ld-fn quiet-alist *the-live-state* nil)) (t (state-free-global-let* ((ld-verbose nil) (ld-pre-eval-print :never) (ld-post-eval-print nil) (ld-prompt nil)) (ld-fn quiet-alist *the-live-state* nil))))))) (t (ld-fn ld-alist *the-live-state* nil))))) (cond (erp (format t "**Error encountered during LD of ACL2 ~ customization file,~%~s.~%Quitting....~%" customization-full-file-name) (quit 1)) (t (value val))))))))))
project-dir-filenamefunction
(defun project-dir-filename (dir0 filename filename-dir key ctx state) (let* ((dir (extend-pathname+ filename-dir dir0 t state))) (cond ((and dir (or (equal dir "") (not (eql (char dir (1- (length dir))) *directory-separator*)))) (cond (filename (er soft ctx "The project pathname ~x0, supplied in file ~x1 for the key ~ ~x2, represents a file but not a directory." dir0 filename key)) (t (er soft ctx "The pathname ~x0, supplied by environment variable ~ ACL2_SYSTEM_BOOKS, represents a file but not a directory." dir0)))) (dir (value dir)) (filename (er soft ctx "The project pathname ~x0, supplied in file ~x1 for the key ~ ~x2, represents a directory that does not exist." dir0 filename key)) (t (er soft ctx "The pathname ~x0, supplied by environment variable ~ ACL2_SYSTEM_BOOKS, represents a directory that does not exist." dir0)))))
project-dir-alist-from-file-recfunction
(defun project-dir-alist-from-file-rec (lst filename filename-dir ctx state) (declare (xargs :guard (and (keyword-value-listp lst) (string-listp (odds lst))))) (cond ((endp lst) (value nil)) (t (let* ((key (car lst)) (dir0 (cadr lst)) (dir1 (if (equal dir0 "") "./" dir0))) (er-let* ((dir (project-dir-filename dir1 filename filename-dir key ctx state)) (rest (project-dir-alist-from-file-rec (cddr lst) filename filename-dir ctx state))) (value (acons (car lst) dir rest)))))))
project-dir-alist-from-file-0function
(defun project-dir-alist-from-file-0 (filename ctx state) (declare (xargs :stobjs state :mode :program)) (let ((filename-u (pathname-os-to-unix filename (os (w state)) state))) (er-let* ((lst (read-file+ filename-u (msg "Unable to open file ~x0 to read the ~ project-dir-alist." filename) ctx state))) (cond ((not (keyword-value-string-listp lst)) (er soft ctx "The value read for the project-dir-alist must be an ~ alternating list of keywords and strings, starting with a ~ keyword. But the value read from file ~x0 is ~x1, which ~ does not have that property." filename lst)) ((not (project-dir-file-p filename-u state)) (er soft ctx "The value read for the project-dir-alist is, as expected, ~ an alternating list of keywords and strings, starting with ~ a keyword. But each line must either be blank, be a ~ comment (i.e., its first non-whitespace character is `;'), ~ or contain a keyword followed by a filename without `"' in ~ its name. File ~x0 does not have that property." filename)) (t (let ((abs (canonical-unix-pathname filename-u nil state))) (cond ((null abs) (er soft ctx "Surprising error: Unable to get the absolute pathname ~ for file ~x0~@1." filename-u (if (equal filename filename-u) "" (msg " (which was obtained from filename ~x0)" filename)))) (t (project-dir-alist-from-file-rec lst abs (directory-of-absolute-pathname abs) ctx state)))))))))
project-dir-alist-from-filefunction
(defun project-dir-alist-from-file (filename ctx state) (let* ((old-inh (f-get-global 'inhibit-output-lst state)) (flg (member-eq 'error old-inh))) (er-progn (if flg (set-inhibit-output-lst (cons 'error old-inh)) (value nil)) (er-let* ((val (project-dir-alist-from-file-0 filename ctx state))) (er-progn (if flg (set-inhibit-output-lst old-inh) (value nil)) (cond ((duplicate-keysp-eq val) (er soft ctx "The keyword ~x0 occurs more than once in the ~ ACL2_PROJECTS file, ~x1." (car (duplicate-keysp-eq val)) filename)) ((loop for tail on val thereis (rassoc-equal (cdar tail) (cdr tail))) (er soft ctx "The directory ~x0 is specified more than once in the ~ ACL2_PROJECTS file, ~x1." (loop for tail on val when (rassoc-equal (cdar tail) (cdr tail)) do (return (cdar tail))) filename)) (t (value val))))))))
replace-project-dir-alistfunction
(defun replace-project-dir-alist (project-dir-alist) (let ((sorted-project-dir-alist (merge-sort-length>=-cdr project-dir-alist))) (let ((doublet (assoc-eq 'global-value (get 'project-dir-alist *current-acl2-world-key*)))) (assert (and (consp doublet) (consp (cdr doublet)) (not (eq (cadr doublet) *acl2-property-unbound*)))) (setf (cadr doublet) sorted-project-dir-alist)) (loop for trip in (lookup-world-index 'event 0 (w *the-live-state*)) when (and (eq (car trip) 'project-dir-alist) (eq (cadr trip) 'global-value)) do (progn (setf (cddr trip) sorted-project-dir-alist) (return t)) finally (error "Implementation error: Failure in ~ replace-project-dir-alist!"))))
establish-project-dir-alistfunction
(defun establish-project-dir-alist (system-dir0 ctx state) (declare (xargs :stobjs state :mode :program)) (mv-let (erp val state) (er-let* ((system-books-dir (value (and system-dir0 (extend-pathname+ (cbd) (pathname-os-to-unix system-dir0 (os (w state)) state) t state)))) (proj-file (getenv$ "ACL2_PROJECTS" state)) (proj-alist (if proj-file (project-dir-alist-from-file proj-file ctx state) (value nil))) (new-sys-pair (value (assoc-eq :system proj-alist))) (old-project-dir-alist (value (project-dir-alist (w state))))) (cond ((null proj-file) (when system-books-dir (replace-project-dir-alist (put-assoc-eq :system system-books-dir old-project-dir-alist))) (value nil)) ((and new-sys-pair system-books-dir (not (equal (cdr new-sys-pair) system-books-dir))) (er-let* ((dir0 (getenv$ "ACL2_SYSTEM_BOOKS" state))) (er soft ctx "The project-dir-alist read from file ~x0 associates :SYSTEM ~ with ~x1. This conflicts with the value ~x2 associated with ~ :SYSTEM~@3." proj-file (cdr new-sys-pair) system-books-dir (if dir0 (msg " using environment variable ACL2_SYSTEM_BOOKS") (msg ", which is the pathname of the books/ directory of your ~ ACL2 distribution"))))) ((rassoc-equal (or system-books-dir (cdr (assoc-eq :system old-project-dir-alist))) (remove-assoc-eq :system proj-alist)) (let ((pair (rassoc-equal (or system-books-dir (cdr (assoc-eq :system old-project-dir-alist))) (remove-assoc-equal :system proj-alist)))) (er soft ctx "The project-dir-alist read from file ~x0 associates keyword ~ ~x1 with ~x2, which is also the system books directory." proj-file (car pair) (cdr pair)))) ((and (let ((wrld (w state))) (or (conflicting-symbol-alists proj-alist (cdr (assoc-eq :include-book-dir-alist (table-alist 'acl2-defaults-table wrld)))) (conflicting-symbol-alists proj-alist (table-alist 'include-book-dir!-table wrld))))) (let* ((wrld (w state)) (c1 (conflicting-symbol-alists proj-alist (cdr (assoc-eq :include-book-dir-alist (table-alist 'acl2-defaults-table wrld))))) (c2 (conflicting-symbol-alists proj-alist (table-alist 'include-book-dir!-table wrld)))) (mv-let (k new old fn) (if c1 (mv (car c1) (cadr c1) (cddr c1) 'add-include-book-dir) (mv (car c2) (cadr c2) (cddr c2) 'add-include-book-dir!)) (er soft ctx "The project-dir-alist read from file ~x0 assigns the value ~ ~x1 to the key ~x2. But before the present ACL2 executable ~ was created with save-exec, that key was associated with a ~ different value by ~x3, namely, ~x4." proj-file new k fn old)))) (t (replace-project-dir-alist (if new-sys-pair proj-alist (acons :system (or system-books-dir (cdr (assoc-eq :system old-project-dir-alist))) proj-alist))) (value nil)))) (cond (erp (pprogn (fms "**ABORTING start of ACL2!**~|Address the error ~ noted above in order to run ACL2.~|See :DOC ~ project-dir-alist." nil *standard-co* state nil) (prog2$ (exit 1) (mv erp val state)))) (t (value val)))))
lpfunction
(defun lp (&rest args) (when args (error "LP takes no arguments.")) (when (not *acl2-default-restart-complete*) (acl2-default-restart t)) (setq *read-default-float-format* 'double-float) (with-more-warnings-suppressed (unwind-protect (let ((state *the-live-state*) (*debug-io* *our-standard-io*)) (pushnew :acl2-loop-only *features*) (cond ((> *ld-level* 0) (when (raw-mode-p *the-live-state*) (fms "You have attempted to enter the ACL2 read-eval-print loop ~ from within raw mode. However, you appear already to be ~ in that loop. If your intention is to leave raw mode, ~ then execute: :set-raw-mode nil.~|" nil (standard-co *the-live-state*) *the-live-state* nil)) (return-from lp nil)) ((not *lp-ever-entered-p*) (f-put-global 'saved-output-reversed nil state) (push-current-acl2-world 'saved-output-reversed *the-live-state*) (set-initial-cbd) (eval `(in-package ,*STARTUP-PACKAGE-NAME*)) (setq *debugger-hook* 'our-abort) (break-on-overflow-and-nan) (define-our-sbcl-putenv) (let* ((save-expansion (let ((s (getenv$-raw "ACL2_SAVE_EXPANSION"))) (and s (not (equal s "")) (not (equal (string-upcase s) "NIL"))))) (fast-cert-mode-val (and (null (f-get-global 'fast-cert-status state)) (let ((x (getenv$-raw "ACL2_FAST_CERT"))) (and x (cond ((equal x "") nil) ((string-equal x "accept") :accept) (t t)))))) (book-hash-alistp-env (let ((s (getenv$-raw "ACL2_BOOK_HASH_ALISTP"))) (or (null s) (not (equal (string-upcase s) "NIL"))))) (os-user-home-dir-path (our-user-homedir-pathname)) (os-user-home-dir0 (and os-user-home-dir-path (our-truename os-user-home-dir-path "Note: Calling OUR-TRUENAME from ~ LP."))) (os-user-home-dir (and os-user-home-dir0 (if (eql (char os-user-home-dir0 (1- (length os-user-home-dir0))) *directory-separator*) (subseq os-user-home-dir0 0 (1- (length os-user-home-dir0))) os-user-home-dir0))) (user-home-dir (and os-user-home-dir (pathname-os-to-unix os-user-home-dir (os (w *the-live-state*)) *the-live-state*))) (system-dir0 (getenv$-raw "ACL2_SYSTEM_BOOKS"))) (when save-expansion (f-put-global 'save-expansion-file t *the-live-state*)) (when fast-cert-mode-val (set-fast-cert fast-cert-mode-val state)) (when book-hash-alistp-env (f-put-global 'book-hash-alistp t *the-live-state*)) (when user-home-dir (f-put-global 'user-home-dir user-home-dir *the-live-state*)) (establish-project-dir-alist system-dir0 'lp *the-live-state*)) (set-gag-mode-fn :goals *the-live-state*) (f-put-global 'serialize-character-system #\Z state) (f-put-global 'pc-info (make pc-info :print-macroexpansion-flg nil :print-prompt-and-instr-flg t :prompt "->: " :prompt-depth-prefix "#") state) (setup-standard-io) (ld-acl2-customization state) (let ((val (getenv$-raw "ACL2_CHECK_INVARIANT_RISK"))) (when (and val (not (equal val ""))) (let* ((val1 (string-upcase val)) (val2 (cond ((equal val1 "NIL") nil) ((equal val1 "T") t) ((member-equal val1 '(":ERROR" "ERROR")) :error) ((member-equal val1 '(":WARNING" "WARNING")) :warning) (t (error "Error detected in ~ initialize-state-globals:~%Illegal ~ value, ~s, for environment variable ~ ACL2_CHECK_INVARIANT_RISK.~%See :DOC ~ invariant-risk." val1))))) (ld-fn (put-assoc-eq 'standard-oi `((set-check-invariant-risk ,VAL2)) (put-assoc-eq 'ld-pre-eval-print t (f-get-ld-specials *the-live-state*))) *the-live-state* t)))) (f-put-global 'ld-error-action :continue *the-live-state*))) (with-suppression (cond ((and *return-from-lp* (not *lp-ever-entered-p*)) (f-put-global 'standard-oi `(,*RETURN-FROM-LP* (value :q)) *the-live-state*) (setq *return-from-lp* nil) (setq *lp-ever-entered-p* t) (state-free-global-let* ((ld-verbose nil) (ld-prompt nil) (ld-post-eval-print nil)) (ld-fn (f-get-ld-specials *the-live-state*) *the-live-state* nil))) (t (setq *lp-ever-entered-p* t) (f-put-global 'standard-oi *standard-oi* *the-live-state*) (cond (*lp-init-forms* (let ((standard-oi (append *lp-init-forms* *standard-oi*))) (setq *lp-init-forms* nil) (ld-fn (put-assoc-eq 'standard-oi standard-oi (f-get-ld-specials *the-live-state*)) *the-live-state* nil))) (t (ld-fn (f-get-ld-specials *the-live-state*) *the-live-state* nil))) (fms "Exiting the ACL2 read-eval-print loop. To re-enter, ~ execute (LP)." nil *standard-co* *the-live-state* nil)))) (values)) (setq *features* (remove :acl2-loop-only *features* :test 'eq)))))
lp!function
(defun lp! (&rest args) (declare (ignore args)) (error "LP! is no longer supported or necessary. Evaluate (LP) to enter the ACL2 read-eval-print loop such that feature :acl2-loop-only is true."))
acl2-compile-filefunction
(defun acl2-compile-file (full-book-string os-expansion-filename) (let ((*defeat-slow-alist-action* t) (*readtable* *acl2-readtable*) (ofile (convert-book-string-to-compiled (pathname-unix-to-os full-book-string *the-live-state*) *the-live-state*)) (stream (get (proofs-co *the-live-state*) *open-output-channel-key*))) (let ((*readtable* *reckless-acl2-readtable*)) (cond (t (compile-file os-expansion-filename :output-file ofile)))) (terpri stream) (terpri stream)))
other
(defun-one-output delete-auxiliary-book-files (full-book-string) (let* ((file (pathname-unix-to-os full-book-string *the-live-state*)) (ofile (convert-book-string-to-compiled file *the-live-state*)) (efile (expansion-filename file)) (err-string "A file created for book ~x0, namely ~x1, exists and ~ cannot be deleted with Common Lisp's delete-file. We ~ do not know for sure whether this file was produced by ~ ACL2 and we do not even know that it corresponds to the ~ book ~x0. If ~x1 exists at the time of an ~ (include-book ~x0), it might be erroneously loaded, ~ possibly causing inconsistency.")) (when (probe-file ofile) (cond ((delete-file ofile) nil) (t (er hard 'delete-auxiliary-book-files err-string full-book-string ofile)))) (when (probe-file efile) (cond ((delete-file efile) nil) (t (er hard 'delete-auxiliary-book-files err-string full-book-string efile))))))
delete-expansion-filefunction
(defun delete-expansion-file (os-expansion-filename full-book-string state) (delete-file os-expansion-filename) (io? event nil state (full-book-string) (fms! "Note: Deleting expansion file for the book, ~s0.~|" (list (cons #\0 full-book-string)) (proofs-co state) state nil)))
compile-uncompiled-defunsfunction
(defun compile-uncompiled-defuns (file &optional (fns :some) gcl-flg &aux (state *the-live-state*)) (when (and (not (symbol-listp fns)) (not (eq fns :some))) (er hard 'compile-uncompiled-defuns "The argument to compile-uncompiled-defuns must be either a true list ~ of symbols or the keyword :some. The argument ~x0 is thus illegal." fns)) (cond ((null fns) (warning$ 'compile-uncompiled-defuns nil "No functions to compile.") (return-from compile-uncompiled-defuns file))) (let ((os-file (pathname-unix-to-os file state))) (state-global-let* ((print-circle (f-get-global 'print-circle-files state)) (writes-okp t) (serialize-character (f-get-global 'serialize-character-system state))) (with-print-controls :defaults ((*print-circle* (f-get-global 'print-circle state))) (let ((seen (make-hash-table :test 'eq)) (fns (cond ((eq fns :uncompiled) :some) ((eq fns t) :all) (t fns))) (fn-file (format nil "~a.lisp" file))) (with-output-object-channel-sharing chan fn-file (let ((str0 (get-output-stream-from-channel chan)) (str1 "; (ACL2 Note) Attempting separate compilation ~a: ~s.~&")) (format str0 "; This file is automatically generated, to be ~ compiled.~%; Feel free to delete it after compilation.~%") (print-object$ (list 'in-package (current-package state)) chan state) (dolist (trip (w state)) (cond ((and (eq fns :some) (eq (car trip) 'command-landmark) (eq (cadr trip) 'global-value) (equal (access-command-tuple-form (cddr trip)) '(exit-boot-strap-mode))) (return)) ((and (eq (car trip) 'cltl-command) (eq (cadr trip) 'global-value) (consp (cddr trip)) (eq (caddr trip) 'memoize) (not (gethash (cadddr trip) seen)) (memoizedp-raw (cadddr trip)) (or (eq fns :some) (member-eq (cadddr trip) fns))) (setf (gethash (cadddr trip) seen) t) (when (not (compiled-function-p! (cadddr trip))) (format t str1 "for memoized function" (cadddr trip)) (our-ignore-errors (compile (cadddr trip))))) ((and (eq (car trip) 'cltl-command) (eq (cadr trip) 'global-value) (consp (cddr trip)) (eq (caddr trip) 'defuns) (not (and (consp (caddr (cddr trip))) (eq (car (caddr (cddr trip))) 'defstobj)))) (dolist (x (cdddr (cddr trip))) (cond ((and (not (gethash (car x) seen)) (or (eq fns :some) (member-eq (car x) fns))) (setf (gethash (car x) seen) t) (when (not (compiled-function-p! (car x))) (cond ((or (member-eq (car x) (f-get-global 'program-fns-with-raw-code state)) (member-eq (car x) (f-get-global 'logic-fns-with-raw-code state))) (format t str1 "due to raw code" (car x)) (our-ignore-errors (compile (car x)))) (t (print-object$ (cons 'defun x) chan state)))))))) ((and (eq (car trip) 'cltl-command) (eq (cadr trip) 'global-value) (consp (cddr trip)) (eq (caddr trip) 'defstobj)) (dolist (x (car (cddddr (cddr trip)))) (cond ((and (not (gethash (car x) seen)) (not (member-equal *stobj-inline-declare* x)) (or (eq fns :some) (member-eq (car x) fns))) (setf (gethash (car x) seen) t) (when (not (compiled-function-p! (car x))) (print-object$ (cons 'defun x) chan state)))))) ((eq (cadr trip) 'redefined) (setf (gethash (car trip) seen) t)))) (newline chan state) (close-output-channel chan state))) (when (not (eq fns :some)) (let (missing) (dolist (fn fns) (when (not (gethash fn seen)) (push fn missing))) (when missing (format t "~%Warning: The following functions have not been ~ compiled.~% ~s~%Perhaps you have not defined them ~ inside the ACL2 command loop.~%" missing)))) (cond (gcl-flg (er hard 'compile-uncompiled-defuns "The gcl-flg argument to compile-uncompiled-defuns is only ~ legal when running under GCL.")) (t (let ((lisp-file (our-truename (pathname-unix-to-os fn-file state) "Note: Calling OUR-TRUENAME from ~ COMPILE-UNCOMPILED-DEFUNS."))) (compile-file lisp-file) (when (not (keep-tmp-files state)) (delete-file lisp-file))))) (load-compiled os-file t) (if (not (keep-tmp-files state)) (delete-file (concatenate 'string os-file "." *compiled-file-extension*)))) (value nil))) os-file))
compile-uncompiled-*1*-defunsfunction
(defun compile-uncompiled-*1*-defuns (file &optional (fns :some) gcl-flg chan0 &aux (state *the-live-state*) (wrld (w *the-live-state*))) (when (and (not (symbol-listp fns)) (not (eq fns :some))) (er hard 'compile-uncompiled-*1*-defuns "The argument to compile-uncompiled-*1*-defuns must be either a true ~ list of symbols or the keyword :some. The argument ~x0 is thus ~ illegal." fns)) (cond ((and (null fns) (null chan0)) (warning$ 'compile-uncompiled-defuns nil "No functions to compile.") (return-from compile-uncompiled-*1*-defuns file))) (let ((os-file (pathname-unix-to-os file state))) (state-global-let* ((print-circle (f-get-global 'print-circle-files state)) (writes-okp t) (serialize-character (f-get-global 'serialize-character-system state))) (with-print-controls :defaults ((*print-circle* (f-get-global 'print-circle state))) (let ((seen (let ((tbl (make-hash-table :test 'eq))) (when (not (eq fns :some)) (dolist (fn fns) (setf (gethash fn tbl) :init))) tbl)) (fns (cond ((eq fns :uncompiled) :some) ((eq fns t) :all) (t fns))) (fn-file (format nil "~a.lisp" file)) (not-boot-strap-p (null (f-get-global 'boot-strap-flg state)))) (with-output-object-channel-sharing chan fn-file (cond ((null chan) (return-from compile-uncompiled-*1*-defuns (er hard 'compile-uncompiled-*1*-defuns "Unable to open file ~x0 for object output." fn-file))) (t (let ((defs nil) (str0 (get-output-stream-from-channel chan))) (cond ((null chan0) (format str0 "; This file is automatically generated, to be ~ compiled.~%; Feel free to delete it after ~ compilation.~%") (print-object$ (list 'in-package (current-package state)) chan state)) (t state)) (dolist (trip wrld) (cond ((and (eq fns :some) (eq (car trip) 'command-landmark) (eq (cadr trip) 'global-value) (equal (access-command-tuple-form (cddr trip)) '(exit-boot-strap-mode))) (return)) ((and (eq (car trip) 'cltl-command) (eq (cadr trip) 'global-value) (consp (cddr trip)) (eq (caddr trip) 'defuns)) (dolist (x (cdddr (cddr trip))) (when (not (member-eq (car x) `(mv-list return-last wormhole-eval ,@*DF-PRIMITIVES* ,@*DEFUN-OVERRIDES*))) (let ((*1*fn (*1*-symbol (car x)))) (cond ((and (fboundp *1*fn) (cond ((eq fns :some) (and (not (gethash (car x) seen)) (if not-boot-strap-p (not (compiled-function-p! *1*fn)) (not (eq (cadr (cddr trip)) :program))) (setf (gethash (car x) seen) t))) ((eq (gethash (car x) seen) :init) (setf (gethash (car x) seen) t) (or chan0 (not (compiled-function-p! *1*fn)))))) (let ((*1*def (cons 'defun (oneify-cltl-code (cadr (cddr trip)) x (getpropc (car x) 'stobj-function nil wrld) wrld)))) (cond (chan0 (push *1*def defs)) (t (print-object$ *1*def chan state)))))))))) ((eq (cadr trip) 'redefined) (setf (gethash (car trip) seen) t)))) (when chan0 (print-object$ (cons 'progn (nreverse defs)) chan state)) (newline chan state) (cond (chan0 (return-from compile-uncompiled-*1*-defuns os-file)) (t (close-output-channel chan state)))))) chan0) (when (not (eq fns :some)) (let (missing) (dolist (fn fns) (when (not (eq (gethash fn seen) t)) (push fn missing))) (when missing (format t "~%Warning: The following executable-counterpart ~ functions have not been compiled.~% ~s~%Perhaps you ~ have not defined them inside the ACL2 command loop.~%" missing)))) (cond (gcl-flg (er hard 'compile-uncompiled-defuns "The gcl-flg argument to compile-uncompiled-*1*-defuns is only ~ legal when running under GCL.")) (t (let ((lisp-file (our-truename (pathname-unix-to-os fn-file state) "Note: Calling OUR-TRUENAME from ~ COMPILE-UNCOMPILED-*1*-DEFUNS."))) (compile-file lisp-file) (when (not (keep-tmp-files state)) (delete-file lisp-file))))) (load-compiled os-file t) (if (not (keep-tmp-files state)) (delete-file (concatenate 'string os-file "." *compiled-file-extension*))) (value nil)))) os-file))
compile-certified-filefunction
(defun compile-certified-file (os-expansion-filename full-book-string state) (let* ((os-full-book-string (pathname-unix-to-os full-book-string state)) (os-full-book-string-compiled (convert-book-string-to-compiled os-full-book-string state))) (when (probe-file os-full-book-string-compiled) (delete-file os-full-book-string-compiled)) (acl2-compile-file full-book-string os-expansion-filename) os-full-book-string-compiled))
compile-for-include-bookfunction
(defun compile-for-include-book (full-book-string full-book-name certified-p ctx state) (cond ((not certified-p) (pprogn (warning$ ctx "Compiled file" "An include-book form for book ~x0 has specified option ~ :load-compiled-file :comp. But this book is ~ uncertified, so compilation is being skipped." full-book-string) (value nil))) (t (let* ((efile (pathname-unix-to-os (expansion-filename full-book-string) state)) (entry (and *hcomp-book-ht* (gethash full-book-name *hcomp-book-ht*))) (status (and entry (access hcomp-book-ht-entry entry :status)))) (cond ((eq status 'complete) (value nil)) (t (mv-let (cfile state) (certificate-file full-book-string state) (let* ((cfile (and cfile (pathname-unix-to-os cfile state))) (cfile-write-date (and cfile (file-write-date cfile))) (efile-write-date (and (probe-file efile) (file-write-date efile))) (reason (cond ((not (probe-file cfile)) "the certificate file does not exist") ((not (probe-file efile)) "the expansion file does not exist") ((not (eq status 'to-be-compiled)) "the expansion file or compiled file ~ appears not to have been loaded to ~ completion") ((and cfile-write-date efile-write-date (<= cfile-write-date efile-write-date)) nil) (t "the write-date of the expansion file is ~ not greater than the write date of the ~ certificate file")))) (cond (reason (er soft ctx "An include-book event with option ~ :load-compiled-file :comp has failed for ~ book~|~s0,~|because ~@1. See :DOC ~ include-book and see :DOC ~ book-compiled-file." full-book-string reason)) (t (observation ctx "Compiling file ~x0, as specified by ~ include-book option :load-compiled-file ~ :comp." full-book-string) (acl2-compile-file full-book-string efile) (value nil)))))))))))
other
(defun-one-output enabled-structurep (x) (case-match x (((index-of-last-enabling . theory-array) (array-name . array-length) array-name-root . array-name-suffix) (and (integerp index-of-last-enabling) (symbolp array-name) (array1p array-name theory-array) (integerp array-length) (character-listp array-name-root) (integerp array-name-suffix))) (& nil)))
other
(defun-one-output rcnstp (x) (case-match x (((current-enabled-structure) (& & . &) (& . &) (& . &) . &) (enabled-structurep current-enabled-structure)) (& nil)))
other
(defvar *trace-alist* (list (cons 'state '|*the-live-state*|)))
other
(defun-one-output assoc-eq-trace-alist (val alist) (cond ((endp alist) nil) ((and (boundp (caar alist)) (eq val (symbol-value (caar alist)))) (car alist)) (t (assoc-eq-trace-alist val (cdr alist)))))
other
(defun-one-output stobj-print-symbol (x user-stobj-alist-tail &optional rawp) (and (live-stobjp x) (loop for pair in user-stobj-alist-tail when (eq x (cdr pair)) do (return (intern-in-package-of-symbol (stobj-print-name (car pair)) (car pair))) finally (return (and (not rawp) (intern "<some-stobj>" (find-package-fast (current-package *the-live-state*))))))))
other
(defun-one-output replace-live-stobjs-in-list
(lst &optional rawp)
(loop for
x
in
lst
collect
(if (live-state-p x)
'|<state>|
(or (stobj-print-symbol x *user-stobj-alist* rawp) x))))
trace-hide-world-and-statefunction
(defun trace-hide-world-and-state (l &optional no-stobj-hiding) (let* ((l (if no-stobj-hiding l (let ((stobj-pair (rassoc l *user-stobj-alist*))) (cond (stobj-pair (intern-in-package-of-symbol (stobj-print-name (car stobj-pair)) (car stobj-pair))) (t (or (and (arrayp l) (stobj-print-symbol l *user-stobj-alist*)) l)))))) (pair (assoc-eq-trace-alist l *trace-alist*))) (cond (pair (cdr pair)) ((atom l) l) ((eq l (w *the-live-state*)) '|current-acl2-world|) ((rcnstp l) '|some-rcnst|) ((enabled-structurep l) '|some-enabled-structure|) ((and (consp l) (or (eq (car l) 'event-index) (eq (car l) 'command-index)) (consp (cdr l)) (eq (car (cdr l)) 'global-value)) (list* (car l) 'global-value '|some-index|)) (t (cons (trace-hide-world-and-state (car l) no-stobj-hiding) (trace-hide-world-and-state (cdr l) no-stobj-hiding))))))
other
(defun-one-output get-stobjs-out-for-declare-form (fn) (cond ((eq fn 'cons) '(nil)) ((member-eq fn *stobjs-out-invalid*) (interface-er "Implementation error in ~ get-stobjs-out-for-declare-form: Attempted to find ~ stobjs-out for ~x0." fn)) (t (let ((w (w *the-live-state*))) (or (getpropc fn 'stobjs-out nil w) (and (getpropc fn 'symbol-class nil w) '(nil)))))))
fix-trace-untracefunction
(defun fix-trace-untrace (new-trace-specs old-trace-specs) (cond ((endp new-trace-specs) nil) ((assoc-eq (caar new-trace-specs) old-trace-specs) (fix-trace-untrace (cdr new-trace-specs) old-trace-specs)) (t (cons (caar new-trace-specs) (fix-trace-untrace (cdr new-trace-specs) old-trace-specs)))))
fix-tracefunction
(defun fix-trace (old-trace-specs) (let* ((new-trace-specs (f-get-global 'trace-specs *the-live-state*)) (to-untrace (fix-trace-untrace new-trace-specs old-trace-specs)) (to-retrace (set-difference-equal old-trace-specs new-trace-specs))) (when to-untrace (eval `(untrace$ ,@TO-UNTRACE))) (when to-retrace (eval `(trace$ ,@TO-RETRACE)))))
mf-looking-atfunction
(defun mf-looking-at (str1 str2 &key (start1 0) (start2 0)) (unless (typep str1 'simple-base-string) (error "looking at: ~a is not a string." str1)) (unless (typep str2 'simple-base-string) (error "looking at: ~a is not a string." str2)) (unless (typep start1 'fixnum) (error "looking at: ~a is not a fixnum." start1)) (unless (typep start2 'fixnum) (error "looking at: ~a is not a fixnum." start2)) (locally (declare (simple-base-string str1 str2) (fixnum start1 start2)) (let ((l1 (length str1)) (l2 (length str2))) (declare (fixnum l1 l2)) (loop (when (>= start1 l1) (return t)) (when (or (>= start2 l2) (not (eql (char str1 start1) (char str2 start2)))) (return nil)) (incf start1) (incf start2)))))
our-unamefunction
(defun our-uname nil (multiple-value-bind (exit-code val) (system-call+ "uname" nil) (and (eql exit-code 0) (stringp val) (<= 6 (length val)) (cond ((string-equal (subseq val 0 6) "Darwin") :darwin) ((string-equal (subseq val 0 5) "Linux") :linux) ((string-equal (subseq val 0 7) "FreeBSD") :freebsd)))))
meminfofunction
(defun meminfo (&optional arg) (assert (or (null arg) (stringp arg))) (or (our-with-standard-io-syntax (case (our-uname) (:linux (let ((arg (or arg "MemTotal:"))) (and (our-ignore-errors (probe-file "/proc/meminfo")) (with-open-file (stream "/proc/meminfo") (let (line) (loop while (setq line (read-line stream nil nil)) do (when (mf-looking-at arg line) (return (values (read-from-string line nil nil :start (length arg))))))))))) (:darwin (let* ((arg (or arg "hw.memsize")) (len (length arg))) (multiple-value-bind (exit-code val) (system-call+ "sysctl" (list arg)) (and (eql exit-code 0) (mf-looking-at arg val) (mf-looking-at arg ": " :start1 len) (let ((ans (read-from-string val nil nil :start (+ 2 len)))) (and (integerp ans) (equal (mod ans 1024) 0) (/ ans 1024))))))) (:freebsd (let* ((arg (or arg "hw.usermem")) (len (length arg))) (multiple-value-bind (exit-code val) (system-call+ "sysctl" (list arg)) (and (eql exit-code 0) (mf-looking-at arg val) (mf-looking-at arg ": " :start1 len) (let ((ans (read-from-string val nil nil :start (+ 2 len)))) (and (integerp ans) (equal (mod ans 1024) 0) (/ ans 1024))))))) (t nil))) 0))
other
(defg *max-mem-usage* (expt 2 32))
other
(defg *gc-min-threshold* (min (expt 2 30) most-positive-fixnum))