other
(in-package "ACL2")
raw-acl2-exports1function
(defun raw-acl2-exports1 (x pkg-witness wrld allp acc) (declare (xargs :guard (and (alistp x) (symbolp pkg-witness) (plist-worldp wrld) (symbol-listp acc)))) (cond ((endp x) acc) (t (raw-acl2-exports1 (cdr x) pkg-witness wrld allp (let ((sym (caar x))) (cond ((and (symbolp sym) (eq (intern-in-package-of-symbol (symbol-name sym) pkg-witness) sym) (or allp (getprop sym 'const nil 'current-acl2-world wrld) (not (eq (getprop sym 'formals t 'current-acl2-world wrld) t)) (getprop sym 'macro-body nil 'current-acl2-world wrld))) (cons sym acc)) (t acc)))))))
raw-acl2-exportsfunction
(defun raw-acl2-exports (allp wrld) (declare (xargs :guard (plist-worldp wrld))) (let ((doc-alist *acl2-system-documentation*)) (cond ((alistp doc-alist) (raw-acl2-exports1 doc-alist (pkg-witness "ACL2") wrld allp nil)) (t (er hard? 'raw-acl2-exports "Expected ~x0 to be an alistp!")))))
symbol-listp-revappendtheorem
(defthm symbol-listp-revappend (implies (and (symbol-listp x) (symbol-listp y)) (symbol-listp (revappend x y))))
symbol-listp-raw-acl2-exports1theorem
(defthm symbol-listp-raw-acl2-exports1 (implies (symbol-listp acc) (symbol-listp (raw-acl2-exports1 x pkg-witness wrld allp acc))))
symbol-listp-raw-acl2-exportstheorem
(defthm symbol-listp-raw-acl2-exports (symbol-listp (raw-acl2-exports allp wrld)) :rule-classes ((:forward-chaining :trigger-terms ((raw-acl2-exports allp wrld)))))
*acl2-exports-exclusions*constant
(defconst *acl2-exports-exclusions* '(*untroublesome-characters* add-dive-into-macro bdd book-hash check-sum comp-gcl count defun-mode dive-into-macros-table error1 find-rules-of-rune loop-stopper mbe1 non-linear-arithmetic normalize pos-listp proof-builder redefined-names remove-dive-into-macro rewrite safe-mode tag-tree type-set useless-runes waterfall assume-true-false-aggressive-p heavy-linear-p remove-trivial-equivalences-enabled-p rewrite-if-avoid-swap arglistp alist-keys-subsetp alist-to-doublets all-calls all-fnnames all-fnnames-lst all-fnnames1 body conjoin conjoin2 cons-count-bounded cons-term cons-term* defined-constant disjoin disjoin2 dumb-negate-lit enabled-numep enabled-runep evens fargn fargs fcons-term fcons-term* fdefun-mode ffn-symb ffn-symb-p ffnnamep ffnnamep-lst first-keyword flambda-applicationp flambdap flatten-ands-in-lit fn-rune-nume fn-symb formals fsubcor-var fquotep genvar get-brr-local get-event get-skipped-proofs-p implicate io? keyword-listp known-package-alist lambda-applicationp lambda-body lambda-formals legal-constantp legal-variablep logicp make-lambda make-lambda-application make-lambda-term merge-sort-lexorder nvariablep odds packn packn-pos pairlis-x1 pairlis-x2 prettyify-clause programp recursivep rewrite-lambda-object rw-cache-state stobjp stobjs-in stobjs-out subcor-var sublis-var subst-expr subst-var symbol-class trans-eval translate translate-hints translate-cmp translate1 translate1-cmp translate11 variablep))
*special-ops*constant
(defconst *special-ops* '(quote lambda lambda$ let mv mv-let pargs check-vars-not-free translate-and-test with-local-stobj stobj-let flet declare if mv-list return-last))
missing-from-acl2-exportsfunction
(defun missing-from-acl2-exports (wrld) (declare (xargs :guard (plist-worldp wrld) :mode :program)) (let ((expected (append *acl2-exports-exclusions* *acl2-exports*))) (union-eq (set-difference-eq *special-ops* expected) (set-difference-eq (raw-acl2-exports nil wrld) expected))))
other
(assert-event (null (missing-from-acl2-exports (w state))) :msg (msg "Each symbol in the following list should either be added to the ~ constant ~x0 defined in the ACL2 source code, or else should be ~ added to the constant ~x1 defined in this book, ~ ~s2:~| ~X34" '*acl2-exports* '*acl2-exports-exclusions* "check-acl2-exports.lisp" (sort-symbol-listp (missing-from-acl2-exports (w state))) nil))
in-theory
(in-theory (disable raw-acl2-exports))
undocumented-acl2-exportsfunction
(defun undocumented-acl2-exports (wrld) (declare (xargs :guard (plist-worldp wrld))) (set-difference-eq *acl2-exports* (raw-acl2-exports t wrld)))
suspicious-acl2-exportsfunction
(defun suspicious-acl2-exports (wrld) (declare (xargs :guard (plist-worldp wrld))) (set-difference-eq (raw-acl2-exports t wrld) (raw-acl2-exports nil wrld)))