other
(in-package "ACL2-HACKER")
other
(include-book "doc-section")
other
(program)
other
(set-state-ok t)
other
(make-event (if (earlier-acl2-versionp "ACL2 Version 3.2" (@ acl2-version)) (value '(defmacro progn!-with-bindings (bindings &rest rst) `(progn! :state-global-bindings ,BINDINGS . ,RST))) (value '(defmacro progn!-with-bindings (bindings &rest rst) `(progn! (state-global-let* ,BINDINGS (progn! . ,RST)))))))
@optmacro
(defmacro @opt (var &optional deflt) `(if (boundp-global ',ACL2-HACKER::VAR state) (f-get-global ',ACL2-HACKER::VAR state) ,ACL2-HACKER::DEFLT))
er-whenmacro
(defmacro er-when (test form &rest more-forms) `(if ,ACL2-HACKER::TEST (er-progn ,ACL2-HACKER::FORM . ,ACL2-HACKER::MORE-FORMS) (value :invisible)))
union-eq-with-topfunction
(defun union-eq-with-top (a b) (if (or (eq a t) (eq b t)) t (union-eq a b)))
add-temp-touchable-aliasesfunction
(defun add-temp-touchable-aliases (spec sofar fn-p) (declare (xargs :guard (booleanp fn-p))) (if (null spec) sofar (let ((sym (if (consp spec) (car spec) spec)) (rest (if (consp spec) (cdr spec) nil))) (add-temp-touchable-aliases rest (union-eq-with-top (cond ((eq sym :all) t) ((eq sym :initial) (if fn-p *initial-untouchable-fns* *initial-untouchable-vars*)) (t (list sym))) sofar) fn-p))))
compute-progn-touchable-keyword1function
(defun compute-progn-touchable-keyword1 (bangp addp vars fns form-lst) (cond ((and (not vars) (consp form-lst) (eq :vars (car form-lst)) (consp (cdr form-lst))) (compute-progn-touchable-keyword1 bangp addp (cadr form-lst) fns (cddr form-lst))) ((and (not fns) (consp form-lst) (eq :fns (car form-lst)) (consp (cdr form-lst))) (compute-progn-touchable-keyword1 bangp addp vars (cadr form-lst) (cddr form-lst))) (t `(progn!-with-bindings ((temp-touchable-vars (add-temp-touchable-aliases ',ACL2-HACKER::VARS ,(IF ACL2-HACKER::ADDP '(ACL2-HACKER::@ ACL2-HACKER::TEMP-TOUCHABLE-VARS) 'NIL) nil) set-temp-touchable-vars) (temp-touchable-fns (add-temp-touchable-aliases ',ACL2-HACKER::FNS ,(IF ACL2-HACKER::ADDP '(ACL2-HACKER::@ ACL2-HACKER::TEMP-TOUCHABLE-FNS) 'NIL) 't) set-temp-touchable-fns)) ,(IF ACL2-HACKER::BANGP `(ACL2-HACKER::PROGN! . ,ACL2-HACKER::FORM-LST) `(PROGN . ,ACL2-HACKER::FORM-LST))))))
compute-progn-touchable-keywordfunction
(defun compute-progn-touchable-keyword (bangp addp form-lst) (compute-progn-touchable-keyword1 bangp addp nil nil form-lst))
progn+touchablemacro
(defmacro progn+touchable (&rest args) (declare (xargs :guard (and (consp args) (keywordp (car args))))) (if (not (member-eq (car args) '(:vars :fns))) (compute-progn-touchable-keyword1 nil t (car args) (car args) (cdr args)) (compute-progn-touchable-keyword nil t args)))
progn=touchablemacro
(defmacro progn=touchable (&rest args) (declare (xargs :guard (and (consp args) (keywordp (car args))))) (if (not (member-eq (car args) '(:vars :fns))) (compute-progn-touchable-keyword1 nil nil (car args) (car args) (cdr args)) (compute-progn-touchable-keyword nil nil args)))
progn!+touchablemacro
(defmacro progn!+touchable (&rest args) (declare (xargs :guard (and (consp args) (keywordp (car args))))) (if (not (member-eq (car args) '(:vars :fns))) (compute-progn-touchable-keyword1 t t (car args) (car args) (cdr args)) (compute-progn-touchable-keyword t t args)))
progn!=touchablemacro
(defmacro progn!=touchable (&rest args) (declare (xargs :guard (and (consp args) (keywordp (car args))))) (if (not (member-eq (car args) '(:vars :fns))) (compute-progn-touchable-keyword1 t nil (car args) (car args) (cdr args)) (compute-progn-touchable-keyword t nil args)))
with-touchablemacro
(defmacro with-touchable (&rest args) `(progn+touchable . ,ACL2-HACKER::ARGS))
put-ld-redefinition-actionfunction
(defun put-ld-redefinition-action (v state) (mv-let (erp v state) (set-ld-redefinition-action v state) (declare (ignore v)) (prog2$ (and erp (hard-error 'put-ld-redefinition-action "~x0 returned an error." '((#\0 . set-ld-redefinition-action)))) state)))
expand-redef-action-aliasesfunction
(defun expand-redef-action-aliases (spec) (cond ((equal spec t) '(:doit! . :overwrite)) (t spec)))
progn+redef-actionmacro
(defmacro progn+redef-action (spec &rest form-lst) (declare (xargs :guard form-lst)) `(progn!-with-bindings ((ld-redefinition-action ,(IF (EQ ACL2-HACKER::SPEC :UNSPECIFIED) '(ACL2-HACKER::@ ACL2-HACKER::LD-REDEFINITION-ACTION) `(ACL2-HACKER::EXPAND-REDEF-ACTION-ALIASES ',ACL2-HACKER::SPEC)) put-ld-redefinition-action)) (progn . ,ACL2-HACKER::FORM-LST)))
progn+redefmacro
(defmacro progn+redef (&rest args) (declare (xargs :guard (consp args))) (if (and (equal (car args) :action) (consp (cdr args))) `(progn+redef-action ,(CADR ACL2-HACKER::ARGS) . ,(CDDR ACL2-HACKER::ARGS)) `(progn+redef-action t . ,ACL2-HACKER::ARGS)))
with-redef-allowedmacro
(defmacro with-redef-allowed (&rest args) `(progn+redef . ,ACL2-HACKER::ARGS))
temporary-redefmacro
(defmacro temporary-redef (&rest forms) (declare (ignore forms)) (hard-error 'temporary-redef "Old implementation of ~x0 was flawed. Adapt solution to use ~x1 (See :DOC ~x1)." '((#\0 . temporary-redef) (#\1 . progn+redef))))
in-raw-modemacro
(defmacro in-raw-mode (&rest form-lst) `(progn! (with-output :off observation (set-raw-mode-on state)) (progn ,@ACL2-HACKER::FORM-LST nil)))
with-raw-modemacro
(defmacro with-raw-mode (&rest args) `(in-raw-mode . ,ACL2-HACKER::ARGS))
other
(make-event (if (member-eq 'program-fns-with-raw-code (global-val 'untouchable-vars (w state))) (value '(defconst *program-only-state-global* 'program-fns-with-raw-code)) (value '(defconst *program-only-state-global* 'built-in-program-mode-fns))))
ensure-program-only-flagmacro
(defmacro ensure-program-only-flag (&rest fn-lst) (declare (xargs :guard (and fn-lst (symbol-listp fn-lst)))) `(progn!=touchable :vars ,ACL2-HACKER::*PROGRAM-ONLY-STATE-GLOBAL* (assign ,ACL2-HACKER::*PROGRAM-ONLY-STATE-GLOBAL* (union-eq (@ ,ACL2-HACKER::*PROGRAM-ONLY-STATE-GLOBAL*) ',ACL2-HACKER::FN-LST))))
program-mode-pfunction
(defun program-mode-p (fn wrld) (eq ':program (getprop fn 'symbol-class nil 'current-acl2-world wrld)))
program-mode-p-lstfunction
(defun program-mode-p-lst (fn-lst wrld) (or (endp fn-lst) (and (program-mode-p (car fn-lst) wrld) (program-mode-p-lst (cdr fn-lst) wrld))))
assert-program-modemacro
(defmacro assert-program-mode (&rest fn-lst) (declare (xargs :guard (and fn-lst (symbol-listp fn-lst)))) `(assert-event (program-mode-p-lst ',ACL2-HACKER::FN-LST (w state)) :msg (msg "Assertion failed. At least one not :program mode:~%~x0" ',ACL2-HACKER::FN-LST) :on-skip-proofs t))
ensure-program-onlymacro
(defmacro ensure-program-only (&rest fn-lst) (declare (xargs :guard (and fn-lst (symbol-listp fn-lst)))) `(progn (assert-program-mode . ,ACL2-HACKER::FN-LST) (ensure-program-only-flag . ,ACL2-HACKER::FN-LST)))
other
(defconst *bootstrap-special-raw-definitions* '(complex-rationalp must-be-equal zp zip prog2$ time$ hard-error intern-in-package-of-symbol pkg-witness with-output value-triple-fn value-triple pprogn acl2-unwind-protect defund plist-worldp getprop-default fgetprop sgetprop getprops has-propsp extend-world retract-world array-1p array-2pz header aref1 compress1 aset1 aref2 compress2 aset2 flush-compress state-p1 global-table-cars1 boundp-global1 fboundp-global makunbound-global get-global f-get-global put-global f-put-global zpf open-input-channel-p1 open-output-channel-p1 princ$ write-byte$ print-object$-fn open-input-channel close-input-channel open-output-channel close-output-channel read-char$ peek-char$ read-byte$ read-object prin1-with-slashes may-need-slashes user-stobj-alist update-user-stobj-alist read-idate read-run-time read-acl2-oracle getenv$ setenv$ prin1$ the-mv set-enforce-redundancy set-verify-guards-eagerness set-compile-fns set-measure-function set-well-founded-relation logic program set-bogus-mutual-recursion-ok set-irrelevant-formals-ok set-ignore-ok set-inhibit-warnings set-inhibit-output-lst set-state-ok set-let*-abstractionp set-backchain-limit set-default-backchain-limit set-rewrite-stack-limit set-case-split-limitations set-match-free-default add-match-free-override add-include-book-dir delete-include-book-dir set-non-linearp defttag set-default-hints! add-default-hints! remove-default-hints! with-prover-time-limit catch-time-limit4 time-limit4-reached-p wormhole1 wormhole-p abort! er mfc-clause mfc-rdepth mfc-type-alist mfc-ancestors bad-atom<= alphorder latch-stobjs1 big-n decrement-big-n zp-big-n w-of-any-state ev-fncall-rec ev-rec ev-rec-acl2-unwind-protect ev-fncall ev ev-lst ev-fncall-w untranslate untranslate-lst ev-w ev-w-lst user-stobj-alist-safe start-proof-tree initialize-summary-accumulators print-summary set-w longest-common-tail-length-rec chk-virgin in-package defpkg defchoose defun defuns verify-termination verify-guards defmacro defconst defstobj defthm defaxiom deflabel defdoc deftheory in-theory in-arithmetic-theory push-untouchable reset-prehistory set-body table progn encapsulate include-book local chk-package-reincarnation-import-restrictions theory-invariant acl2-raw-eval protected-eval-with-proofs include-book-fn write-expansion-file certify-book-fn defstobj-field-fns-raw-defs open-trace-file-fn close-trace-file-fn with-error-trace-fn trace$-fn-general trace$-fn-simple untrace$-fn break-on-error-fn ld-print-results print-newline-for-time$ good-bye-fn ld-loop ld-fn-body ld-fn compile-function comp-fn comp break$ set-debugger-enable-fn mfc-ts mfc-rw mfc-rw+ mfc-relieve-hyp mfc-ap save-exec))
update-has-special-raw-definitionmacro
(defmacro update-has-special-raw-definition (fn-lst) `(pprogn (if (boundp-global 'has-special-raw-definition state) state (f-put-global 'has-special-raw-definition *bootstrap-special-raw-definitions* state)) (assign has-special-raw-definition (union-eq (@ has-special-raw-definition) ,ACL2-HACKER::FN-LST))))
other
(push-untouchable has-special-raw-definition nil)
ensure-special-raw-definition-flagmacro
(defmacro ensure-special-raw-definition-flag (&rest fn-lst) (declare (xargs :guard (and fn-lst (symbol-listp fn-lst)))) `(progn!=touchable :vars has-special-raw-definition (update-has-special-raw-definition ',ACL2-HACKER::FN-LST)))
assert-no-special-raw-definitionmacro
(defmacro assert-no-special-raw-definition (&rest fn-lst) (declare (xargs :guard (and fn-lst (symbol-listp fn-lst)))) `(assert-event (not (intersectp-eq (@opt has-special-raw-definition) ',ACL2-HACKER::FN-LST)) :msg (msg "Assertion failed. Flagged as having special raw definition:~%~x0" (intersection-eq (@opt has-special-raw-definition) ',ACL2-HACKER::FN-LST)) :on-skip-proofs t))
modify-raw-defun-permanentmacro
(defmacro modify-raw-defun-permanent (name name-for-old ll &rest decls-and-body) (declare (xargs :guard (and (symbolp name) (symbolp name-for-old) (symbol-listp ll) (consp decls-and-body)))) `(progn (in-raw-mode (unless (fboundp ',ACL2-HACKER::NAME-FOR-OLD) (setf (symbol-function ',ACL2-HACKER::NAME-FOR-OLD) (symbol-function ',ACL2-HACKER::NAME))) (defun ,ACL2-HACKER::NAME ,ACL2-HACKER::LL ,@(AND ACL2-HACKER::LL `((DECLARE (IGNORABLE . ,ACL2-HACKER::LL)))) . ,ACL2-HACKER::DECLS-AND-BODY)) (ensure-special-raw-definition-flag ,ACL2-HACKER::NAME)))
build-deflabelsfunction
(defun build-deflabels (names) (if (endp names) nil (cons (list 'deflabel (car names)) (build-deflabels (cdr names)))))
deflabelsmacro
(defmacro deflabels (&rest names) `(progn (with-output :off summary (progn . ,(ACL2-HACKER::BUILD-DEFLABELS ACL2-HACKER::NAMES))) (value-triple ',ACL2-HACKER::NAMES)))
progn+all-ttags-allowedmacro
(defmacro progn+all-ttags-allowed (&rest form-lst) `(progn!-with-bindings ((temp-touchable-vars (if (eq (@ temp-touchable-vars) t) t (cons 'ttags-allowed (@ temp-touchable-vars))) set-temp-touchable-vars)) (progn!-with-bindings ((ttags-allowed :all)) (progn!-with-bindings ((temp-touchable-vars (if (eq (@ temp-touchable-vars) t) t (cdr (@ temp-touchable-vars))) set-temp-touchable-vars)) (progn . ,ACL2-HACKER::FORM-LST)))))
put-ld-skip-proofspfunction
(defun put-ld-skip-proofsp (v state) (mv-let (erp v state) (set-ld-skip-proofsp v state) (declare (ignore v)) (prog2$ (and erp (hard-error 'set-ld-skip-proofsp "~x0 returned an error." '((#\0 . set-ld-skip-proofsp)))) state)))
ttag-skip-proofsmacro
(defmacro ttag-skip-proofs (x) `(progn!-with-bindings ((ld-skip-proofsp 'include-book put-ld-skip-proofsp)) (progn ,ACL2-HACKER::X)))
progn+ttag-skip-proofsmacro
(defmacro progn+ttag-skip-proofs (&rest args) `(progn!-with-bindings ((ld-skip-proofsp 'include-book put-ld-skip-proofsp)) (progn . ,ACL2-HACKER::ARGS)))