/usr/share/acl2-6.3/books/hacking/dynamic-make-event-test.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "ACL2-HACKER" (APPEND (QUOTE (VALUE SET-W! ASSERT-EVENT MSG LD-EVISC-TUPLE CONNECTED-BOOK-DIRECTORY GUARD-CHECKING-ON INHIBIT-OUTPUT-LST PRINT-CLAUSE-IDS ACL2-RAW-MODE-P RAW-MODE-RESTORE-LST SAVED-OUTPUT-TOKEN-LST TAINTED-OKP IN-PACKAGE-FN DEFPKG-FN PE! TRANS! PSO PSO! VALUE-TRIPLE DEFAULT-EVISC-TUPLE TTAG HARD SOFT PROGN! UNTOUCHABLE-FNS UNTOUCHABLE-VARS LD-REDEFINITION-ACTION SET-LD-SKIP-PROOFSP SET-LD-REDEFINITION-ACTION SET-LD-PROMPT SET-LD-KEYWORD-ALIASES SET-LD-PRE-EVAL-FILTER SET-LD-ERROR-TRIPLES SET-LD-ERROR-ACTION SET-LD-QUERY-CONTROL-ALIST SET-CBD-FN SET-RAW-MODE SET-RAW-MODE-FN SET-TAINTED-OKP PUSH-UNTOUCHABLE-FN REMOVE-UNTOUCHABLE-FN SET-RAW-MODE-ON SET-RAW-MODE-OFF TEMP-TOUCHABLE-VARS TEMP-TOUCHABLE-FNS SET-TEMP-TOUCHABLE-VARS SET-TEMP-TOUCHABLE-FNS BUILT-IN-PROGRAM-MODE-FNS PROGRAM-FNS-WITH-RAW-CODE GLOBAL-VALUE CURRENT-ACL2-WORLD LD-LEVEL *WORMHOLEP* RAW-MODE-P MAX-ABSOLUTE-EVENT-NUMBER GETPROP ER-LET* *VALID-OUTPUT-NAMES* STATE-GLOBAL-LET* EXTENSION ABSOLUTE-TO-RELATIVE-COMMAND-NUMBER ACCESS-COMMAND-TUPLE-NUMBER GLOBAL-SET-LST COMMAND-NUMBER-BASELINE EVENT-NUMBER-BASELINE NEXT-ABSOLUTE-COMMAND-NUMBER ADD-COMMAND-LANDMARK NEXT-ABSOLUTE-EVENT-NUMBER ADD-EVENT-LANDMARK SCAN-TO-COMMAND CERTIFY-BOOK-FN F-GET-GLOBAL F-PUT-GLOBAL F-BOUNDP-GLOBAL CHECKPOINT-PROCESSORS GLOBAL-VAL ACL2-VERSION EARLIER-ACL2-VERSIONP)) (QUOTE (PROGN!-WITH-BINDINGS HACKER PROGN+TOUCHABLE PROGN=TOUCHABLE PROGN!+TOUCHABLE PROGN!=TOUCHABLE WITH-TOUCHABLE PROGN+REDEF WITH-REDEF-ALLOWED IN-RAW-MODE WITH-RAW-MODE ASSERT-PROGRAM-MODE ENSURE-PROGRAM-ONLY-FLAG ENSURE-PROGRAM-ONLY HAS-SPECIAL-RAW-DEFINITION ENSURE-SPECIAL-RAW-DEFINITION-FLAG ASSERT-NO-SPECIAL-RAW-DEFINITION RECONSTRUCT-DECLARE-LST MODIFY-RAW-DEFUN-PERMANENT PROGN+ALL-TTAGS-ALLOWED DEFLABELS TTAG-SKIP-PROOFS PROGN+TTAG-SKIP-PROOFS)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)))
(INCLUDE-BOOK "rewrite-code")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((8 RECORD-EXPANSION (PROGN+TOUCHABLE :ALL (REDEFUN+REWRITE DEFUNS-FN (:CARPAT %BODY% :REPL (IF (EQ (CAAR DEF-LST) (QUOTE THE-MAGIC-NAME)) (DYNAMIC-MAKE-EVENT-FN (QUOTE (DEFUN SOME-OTHER-NAME (X) (1+ X))) EVENT-FORM STATE) %BODY%) :VARS (%BODY%)))) (PROGN! :STATE-GLOBAL-BINDINGS ((TEMP-TOUCHABLE-VARS (ACL2-HACKER::ADD-TEMP-TOUCHABLE-ALIASES (QUOTE :ALL) (@ TEMP-TOUCHABLE-VARS) NIL) SET-TEMP-TOUCHABLE-VARS) (TEMP-TOUCHABLE-FNS (ACL2-HACKER::ADD-TEMP-TOUCHABLE-ALIASES (QUOTE :ALL) (@ TEMP-TOUCHABLE-FNS) (QUOTE T)) SET-TEMP-TOUCHABLE-FNS)) (RECORD-EXPANSION (PROGN (REDEFUN+REWRITE DEFUNS-FN (:CARPAT %BODY% :REPL (IF (EQ (CAAR DEF-LST) (QUOTE THE-MAGIC-NAME)) (DYNAMIC-MAKE-EVENT-FN (QUOTE (DEFUN SOME-OTHER-NAME (X) (1+ X))) EVENT-FORM STATE) %BODY%) :VARS (%BODY%)))) (PROGN (RECORD-EXPANSION (REDEFUN+REWRITE DEFUNS-FN (:CARPAT %BODY% :REPL (IF (EQ (CAAR DEF-LST) (QUOTE THE-MAGIC-NAME)) (DYNAMIC-MAKE-EVENT-FN (QUOTE (DEFUN SOME-OTHER-NAME (X) (1+ X))) EVENT-FORM STATE) %BODY%) :VARS (%BODY%))) (PROGN! :STATE-GLOBAL-BINDINGS ((LD-REDEFINITION-ACTION (ACL2-HACKER::EXPAND-REDEF-ACTION-ALIASES (QUOTE T)) ACL2-HACKER::PUT-LD-REDEFINITION-ACTION)) (RECORD-EXPANSION (PROGN (ASSERT-INCLUDE-DEFUN-MATCHES-CERTIFY-DEFUN DEFUNS-FN) (DEFCODE :LOOP (ER-PROGN (ASSERT-NO-SPECIAL-RAW-DEFINITION DEFUNS-FN) (CHK-ACCEPTABLE-REDEFUN (QUOTE (DEFUNS-FN (DEF-LST STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (IF (EQ (CAAR DEF-LST) (QUOTE THE-MAGIC-NAME)) (DYNAMIC-MAKE-EVENT-FN (QUOTE (DEFUN SOME-OTHER-NAME (X) (1+ X))) EVENT-FORM STATE) (WITH-CTX-SUMMARIZED (DEFUN-CTX DEF-LST STATE EVENT-FORM) (LET ((WRLD (W STATE)) (DEF-LST0 DEF-LST) (EVENT-FORM (OR EVENT-FORM (LIST (QUOTE DEFUNS) DEF-LST)))) (REVERT-WORLD-ON-ERROR (ER-LET* ((TUPLE (CHK-ACCEPTABLE-DEFUNS DEF-LST CTX WRLD STATE))) (COND ((EQ TUPLE (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD (LET ((NAMES (NTH 1 TUPLE)) (ARGLISTS (NTH 2 TUPLE)) (DOCS (NTH 3 TUPLE)) (PAIRS (NTH 4 TUPLE)) (GUARDS (NTH 5 TUPLE)) (MEASURES (NTH 6 TUPLE)) (RULER-EXTENDERS-LST (NTH 7 TUPLE)) (MP (NTH 8 TUPLE)) (REL (NTH 9 TUPLE)) (HINTS (NTH 10 TUPLE)) (GUARD-HINTS (NTH 11 TUPLE)) (STD-HINTS (NTH 12 TUPLE)) (OTF-FLG (NTH 13 TUPLE)) (BODIES (NTH 14 TUPLE)) (SYMBOL-CLASS (NTH 15 TUPLE)) (NORMALIZEPS (NTH 16 TUPLE)) (RECLASSIFYINGP (NTH 17 TUPLE)) (WRLD (NTH 18 TUPLE)) (NON-EXECUTABLEP (NTH 19 TUPLE)) (GUARD-DEBUG (NTH 20 TUPLE)) (SPLIT-TYPES-TERMS (NTH 21 TUPLE))) (ER-LET* ((PAIR (DEFUNS-FN0 NAMES ARGLISTS DOCS PAIRS GUARDS MEASURES RULER-EXTENDERS-LST MP REL HINTS GUARD-HINTS STD-HINTS OTF-FLG GUARD-DEBUG BODIES SYMBOL-CLASS NORMALIZEPS SPLIT-TYPES-TERMS NON-EXECUTABLEP CTX WRLD STATE))) (ER-PROGN (CHK-ASSUMPTION-FREE-TTREE (CDR PAIR) CTX STATE) (INSTALL-EVENT-DEFUNS NAMES EVENT-FORM DEF-LST0 SYMBOL-CLASS RECLASSIFYINGP NON-EXECUTABLEP PAIR CTX WRLD STATE)))))))))))))) (QUOTE REDEFUN) (W STATE) STATE) (ENSURE-PROGRAM-ONLY-FLAG DEFUNS-FN) (DEFUN DEFUNS-FN (DEF-LST STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (IF (EQ (CAAR DEF-LST) (QUOTE THE-MAGIC-NAME)) (DYNAMIC-MAKE-EVENT-FN (QUOTE (DEFUN SOME-OTHER-NAME (X) (1+ X))) EVENT-FORM STATE) (WITH-CTX-SUMMARIZED (DEFUN-CTX DEF-LST STATE EVENT-FORM) (LET ((WRLD (W STATE)) (DEF-LST0 DEF-LST) (EVENT-FORM (OR EVENT-FORM (LIST (QUOTE DEFUNS) DEF-LST)))) (REVERT-WORLD-ON-ERROR (ER-LET* ((TUPLE (CHK-ACCEPTABLE-DEFUNS DEF-LST CTX WRLD STATE))) (COND ((EQ TUPLE (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD (LET ((NAMES (NTH 1 TUPLE)) (ARGLISTS (NTH 2 TUPLE)) (DOCS (NTH 3 TUPLE)) (PAIRS (NTH 4 TUPLE)) (GUARDS (NTH 5 TUPLE)) (MEASURES (NTH 6 TUPLE)) (RULER-EXTENDERS-LST (NTH 7 TUPLE)) (MP (NTH 8 TUPLE)) (REL (NTH 9 TUPLE)) (HINTS (NTH 10 TUPLE)) (GUARD-HINTS (NTH 11 TUPLE)) (STD-HINTS (NTH 12 TUPLE)) (OTF-FLG (NTH 13 TUPLE)) (BODIES (NTH 14 TUPLE)) (SYMBOL-CLASS (NTH 15 TUPLE)) (NORMALIZEPS (NTH 16 TUPLE)) (RECLASSIFYINGP (NTH 17 TUPLE)) (WRLD (NTH 18 TUPLE)) (NON-EXECUTABLEP (NTH 19 TUPLE)) (GUARD-DEBUG (NTH 20 TUPLE)) (SPLIT-TYPES-TERMS (NTH 21 TUPLE))) (ER-LET* ((PAIR (DEFUNS-FN0 NAMES ARGLISTS DOCS PAIRS GUARDS MEASURES RULER-EXTENDERS-LST MP REL HINTS GUARD-HINTS STD-HINTS OTF-FLG GUARD-DEBUG BODIES SYMBOL-CLASS NORMALIZEPS SPLIT-TYPES-TERMS NON-EXECUTABLEP CTX WRLD STATE))) (ER-PROGN (CHK-ASSUMPTION-FREE-TTREE (CDR PAIR) CTX STATE) (INSTALL-EVENT-DEFUNS NAMES EVENT-FORM DEF-LST0 SYMBOL-CLASS RECLASSIFYINGP NON-EXECUTABLEP PAIR CTX WRLD STATE)))))))))))))) :EXTEND (IN-RAW-MODE (DEFUN-*1* DEFUNS-FN (DEF-LST STATE EVENT-FORM) (IF (F-GET-GLOBAL (QUOTE SAFE-MODE) *THE-LIVE-STATE*) (THROW-RAW-EV-FNCALL (LIST (QUOTE PROGRAM-ONLY-ER) (QUOTE DEFUNS-FN) (LIST DEF-LST STATE EVENT-FORM) (QUOTE T) (QUOTE (NIL)) T)) (DEFUNS-FN DEF-LST STATE EVENT-FORM)))) :COMPILE (DEFUN DEFUNS-FN (DEF-LST STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (IF (EQ (CAAR DEF-LST) (QUOTE THE-MAGIC-NAME)) (DYNAMIC-MAKE-EVENT-FN (QUOTE (DEFUN SOME-OTHER-NAME (X) (1+ X))) EVENT-FORM STATE) (WITH-CTX-SUMMARIZED (DEFUN-CTX DEF-LST STATE EVENT-FORM) (LET ((WRLD (W STATE)) (DEF-LST0 DEF-LST) (EVENT-FORM (OR EVENT-FORM (LIST (QUOTE DEFUNS) DEF-LST)))) (REVERT-WORLD-ON-ERROR (ER-LET* ((TUPLE (CHK-ACCEPTABLE-DEFUNS DEF-LST CTX WRLD STATE))) (COND ((EQ TUPLE (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD (LET ((NAMES (NTH 1 TUPLE)) (ARGLISTS (NTH 2 TUPLE)) (DOCS (NTH 3 TUPLE)) (PAIRS (NTH 4 TUPLE)) (GUARDS (NTH 5 TUPLE)) (MEASURES (NTH 6 TUPLE)) (RULER-EXTENDERS-LST (NTH 7 TUPLE)) (MP (NTH 8 TUPLE)) (REL (NTH 9 TUPLE)) (HINTS (NTH 10 TUPLE)) (GUARD-HINTS (NTH 11 TUPLE)) (STD-HINTS (NTH 12 TUPLE)) (OTF-FLG (NTH 13 TUPLE)) (BODIES (NTH 14 TUPLE)) (SYMBOL-CLASS (NTH 15 TUPLE)) (NORMALIZEPS (NTH 16 TUPLE)) (RECLASSIFYINGP (NTH 17 TUPLE)) (WRLD (NTH 18 TUPLE)) (NON-EXECUTABLEP (NTH 19 TUPLE)) (GUARD-DEBUG (NTH 20 TUPLE)) (SPLIT-TYPES-TERMS (NTH 21 TUPLE))) (ER-LET* ((PAIR (DEFUNS-FN0 NAMES ARGLISTS DOCS PAIRS GUARDS MEASURES RULER-EXTENDERS-LST MP REL HINTS GUARD-HINTS STD-HINTS OTF-FLG GUARD-DEBUG BODIES SYMBOL-CLASS NORMALIZEPS SPLIT-TYPES-TERMS NON-EXECUTABLEP CTX WRLD STATE))) (ER-PROGN (CHK-ASSUMPTION-FREE-TTREE (CDR PAIR) CTX STATE) (INSTALL-EVENT-DEFUNS NAMES EVENT-FORM DEF-LST0 SYMBOL-CLASS RECLASSIFYINGP NON-EXECUTABLEP PAIR CTX WRLD STATE))))))))))))))) (PROGN (RECORD-EXPANSION (ASSERT-INCLUDE-DEFUN-MATCHES-CERTIFY-DEFUN DEFUNS-FN) (VALUE-TRIPLE (LET ((REWRITE-CODE::CERTIFY-TIME-DEFUN (QUOTE (DEFUN DEFUNS-FN (DEF-LST STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (WITH-CTX-SUMMARIZED (DEFUN-CTX DEF-LST STATE EVENT-FORM) (LET ((WRLD (W STATE)) (DEF-LST0 DEF-LST) (EVENT-FORM (OR EVENT-FORM (LIST (QUOTE DEFUNS) DEF-LST)))) (REVERT-WORLD-ON-ERROR (ER-LET* ((TUPLE (CHK-ACCEPTABLE-DEFUNS DEF-LST CTX WRLD STATE))) (COND ((EQ TUPLE (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD (LET ((NAMES (NTH 1 TUPLE)) (ARGLISTS (NTH 2 TUPLE)) (DOCS (NTH 3 TUPLE)) (PAIRS (NTH 4 TUPLE)) (GUARDS (NTH 5 TUPLE)) (MEASURES (NTH 6 TUPLE)) (RULER-EXTENDERS-LST (NTH 7 TUPLE)) (MP (NTH 8 TUPLE)) (REL (NTH 9 TUPLE)) (HINTS (NTH 10 TUPLE)) (GUARD-HINTS (NTH 11 TUPLE)) (STD-HINTS (NTH 12 TUPLE)) (OTF-FLG (NTH 13 TUPLE)) (BODIES (NTH 14 TUPLE)) (SYMBOL-CLASS (NTH 15 TUPLE)) (NORMALIZEPS (NTH 16 TUPLE)) (RECLASSIFYINGP (NTH 17 TUPLE)) (WRLD (NTH 18 TUPLE)) (NON-EXECUTABLEP (NTH 19 TUPLE)) (GUARD-DEBUG (NTH 20 TUPLE)) (SPLIT-TYPES-TERMS (NTH 21 TUPLE))) (ER-LET* ((PAIR (DEFUNS-FN0 NAMES ARGLISTS DOCS PAIRS GUARDS MEASURES RULER-EXTENDERS-LST MP REL HINTS GUARD-HINTS STD-HINTS OTF-FLG GUARD-DEBUG BODIES SYMBOL-CLASS NORMALIZEPS SPLIT-TYPES-TERMS NON-EXECUTABLEP CTX WRLD STATE))) (ER-PROGN (CHK-ASSUMPTION-FREE-TTREE (CDR PAIR) CTX STATE) (INSTALL-EVENT-DEFUNS NAMES EVENT-FORM DEF-LST0 SYMBOL-CLASS RECLASSIFYINGP NON-EXECUTABLEP PAIR CTX WRLD STATE)))))))))))))) (REWRITE-CODE::INCLUDE-TIME-DEFUN (GET-DEFUN (QUOTE DEFUNS-FN) STATE))) (OR (EQUAL REWRITE-CODE::CERTIFY-TIME-DEFUN REWRITE-CODE::INCLUDE-TIME-DEFUN) (CW "Certify time def: ~x0~%Include time def: ~x1~%" REWRITE-CODE::CERTIFY-TIME-DEFUN REWRITE-CODE::INCLUDE-TIME-DEFUN))) :ON-SKIP-PROOFS T :CHECK T)) (DEFCODE :LOOP (ER-PROGN (ASSERT-NO-SPECIAL-RAW-DEFINITION DEFUNS-FN) (CHK-ACCEPTABLE-REDEFUN (QUOTE (DEFUNS-FN (DEF-LST STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (IF (EQ (CAAR DEF-LST) (QUOTE THE-MAGIC-NAME)) (DYNAMIC-MAKE-EVENT-FN (QUOTE (DEFUN SOME-OTHER-NAME (X) (1+ X))) EVENT-FORM STATE) (WITH-CTX-SUMMARIZED (DEFUN-CTX DEF-LST STATE EVENT-FORM) (LET ((WRLD (W STATE)) (DEF-LST0 DEF-LST) (EVENT-FORM (OR EVENT-FORM (LIST (QUOTE DEFUNS) DEF-LST)))) (REVERT-WORLD-ON-ERROR (ER-LET* ((TUPLE (CHK-ACCEPTABLE-DEFUNS DEF-LST CTX WRLD STATE))) (COND ((EQ TUPLE (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD (LET ((NAMES (NTH 1 TUPLE)) (ARGLISTS (NTH 2 TUPLE)) (DOCS (NTH 3 TUPLE)) (PAIRS (NTH 4 TUPLE)) (GUARDS (NTH 5 TUPLE)) (MEASURES (NTH 6 TUPLE)) (RULER-EXTENDERS-LST (NTH 7 TUPLE)) (MP (NTH 8 TUPLE)) (REL (NTH 9 TUPLE)) (HINTS (NTH 10 TUPLE)) (GUARD-HINTS (NTH 11 TUPLE)) (STD-HINTS (NTH 12 TUPLE)) (OTF-FLG (NTH 13 TUPLE)) (BODIES (NTH 14 TUPLE)) (SYMBOL-CLASS (NTH 15 TUPLE)) (NORMALIZEPS (NTH 16 TUPLE)) (RECLASSIFYINGP (NTH 17 TUPLE)) (WRLD (NTH 18 TUPLE)) (NON-EXECUTABLEP (NTH 19 TUPLE)) (GUARD-DEBUG (NTH 20 TUPLE)) (SPLIT-TYPES-TERMS (NTH 21 TUPLE))) (ER-LET* ((PAIR (DEFUNS-FN0 NAMES ARGLISTS DOCS PAIRS GUARDS MEASURES RULER-EXTENDERS-LST MP REL HINTS GUARD-HINTS STD-HINTS OTF-FLG GUARD-DEBUG BODIES SYMBOL-CLASS NORMALIZEPS SPLIT-TYPES-TERMS NON-EXECUTABLEP CTX WRLD STATE))) (ER-PROGN (CHK-ASSUMPTION-FREE-TTREE (CDR PAIR) CTX STATE) (INSTALL-EVENT-DEFUNS NAMES EVENT-FORM DEF-LST0 SYMBOL-CLASS RECLASSIFYINGP NON-EXECUTABLEP PAIR CTX WRLD STATE)))))))))))))) (QUOTE REDEFUN) (W STATE) STATE) (ENSURE-PROGRAM-ONLY-FLAG DEFUNS-FN) (DEFUN DEFUNS-FN (DEF-LST STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (IF (EQ (CAAR DEF-LST) (QUOTE THE-MAGIC-NAME)) (DYNAMIC-MAKE-EVENT-FN (QUOTE (DEFUN SOME-OTHER-NAME (X) (1+ X))) EVENT-FORM STATE) (WITH-CTX-SUMMARIZED (DEFUN-CTX DEF-LST STATE EVENT-FORM) (LET ((WRLD (W STATE)) (DEF-LST0 DEF-LST) (EVENT-FORM (OR EVENT-FORM (LIST (QUOTE DEFUNS) DEF-LST)))) (REVERT-WORLD-ON-ERROR (ER-LET* ((TUPLE (CHK-ACCEPTABLE-DEFUNS DEF-LST CTX WRLD STATE))) (COND ((EQ TUPLE (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD (LET ((NAMES (NTH 1 TUPLE)) (ARGLISTS (NTH 2 TUPLE)) (DOCS (NTH 3 TUPLE)) (PAIRS (NTH 4 TUPLE)) (GUARDS (NTH 5 TUPLE)) (MEASURES (NTH 6 TUPLE)) (RULER-EXTENDERS-LST (NTH 7 TUPLE)) (MP (NTH 8 TUPLE)) (REL (NTH 9 TUPLE)) (HINTS (NTH 10 TUPLE)) (GUARD-HINTS (NTH 11 TUPLE)) (STD-HINTS (NTH 12 TUPLE)) (OTF-FLG (NTH 13 TUPLE)) (BODIES (NTH 14 TUPLE)) (SYMBOL-CLASS (NTH 15 TUPLE)) (NORMALIZEPS (NTH 16 TUPLE)) (RECLASSIFYINGP (NTH 17 TUPLE)) (WRLD (NTH 18 TUPLE)) (NON-EXECUTABLEP (NTH 19 TUPLE)) (GUARD-DEBUG (NTH 20 TUPLE)) (SPLIT-TYPES-TERMS (NTH 21 TUPLE))) (ER-LET* ((PAIR (DEFUNS-FN0 NAMES ARGLISTS DOCS PAIRS GUARDS MEASURES RULER-EXTENDERS-LST MP REL HINTS GUARD-HINTS STD-HINTS OTF-FLG GUARD-DEBUG BODIES SYMBOL-CLASS NORMALIZEPS SPLIT-TYPES-TERMS NON-EXECUTABLEP CTX WRLD STATE))) (ER-PROGN (CHK-ASSUMPTION-FREE-TTREE (CDR PAIR) CTX STATE) (INSTALL-EVENT-DEFUNS NAMES EVENT-FORM DEF-LST0 SYMBOL-CLASS RECLASSIFYINGP NON-EXECUTABLEP PAIR CTX WRLD STATE)))))))))))))) :EXTEND (IN-RAW-MODE (DEFUN-*1* DEFUNS-FN (DEF-LST STATE EVENT-FORM) (IF (F-GET-GLOBAL (QUOTE SAFE-MODE) *THE-LIVE-STATE*) (THROW-RAW-EV-FNCALL (LIST (QUOTE PROGRAM-ONLY-ER) (QUOTE DEFUNS-FN) (LIST DEF-LST STATE EVENT-FORM) (QUOTE T) (QUOTE (NIL)) T)) (DEFUNS-FN DEF-LST STATE EVENT-FORM)))) :COMPILE (DEFUN DEFUNS-FN (DEF-LST STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (IF (EQ (CAAR DEF-LST) (QUOTE THE-MAGIC-NAME)) (DYNAMIC-MAKE-EVENT-FN (QUOTE (DEFUN SOME-OTHER-NAME (X) (1+ X))) EVENT-FORM STATE) (WITH-CTX-SUMMARIZED (DEFUN-CTX DEF-LST STATE EVENT-FORM) (LET ((WRLD (W STATE)) (DEF-LST0 DEF-LST) (EVENT-FORM (OR EVENT-FORM (LIST (QUOTE DEFUNS) DEF-LST)))) (REVERT-WORLD-ON-ERROR (ER-LET* ((TUPLE (CHK-ACCEPTABLE-DEFUNS DEF-LST CTX WRLD STATE))) (COND ((EQ TUPLE (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD (LET ((NAMES (NTH 1 TUPLE)) (ARGLISTS (NTH 2 TUPLE)) (DOCS (NTH 3 TUPLE)) (PAIRS (NTH 4 TUPLE)) (GUARDS (NTH 5 TUPLE)) (MEASURES (NTH 6 TUPLE)) (RULER-EXTENDERS-LST (NTH 7 TUPLE)) (MP (NTH 8 TUPLE)) (REL (NTH 9 TUPLE)) (HINTS (NTH 10 TUPLE)) (GUARD-HINTS (NTH 11 TUPLE)) (STD-HINTS (NTH 12 TUPLE)) (OTF-FLG (NTH 13 TUPLE)) (BODIES (NTH 14 TUPLE)) (SYMBOL-CLASS (NTH 15 TUPLE)) (NORMALIZEPS (NTH 16 TUPLE)) (RECLASSIFYINGP (NTH 17 TUPLE)) (WRLD (NTH 18 TUPLE)) (NON-EXECUTABLEP (NTH 19 TUPLE)) (GUARD-DEBUG (NTH 20 TUPLE)) (SPLIT-TYPES-TERMS (NTH 21 TUPLE))) (ER-LET* ((PAIR (DEFUNS-FN0 NAMES ARGLISTS DOCS PAIRS GUARDS MEASURES RULER-EXTENDERS-LST MP REL HINTS GUARD-HINTS STD-HINTS OTF-FLG GUARD-DEBUG BODIES SYMBOL-CLASS NORMALIZEPS SPLIT-TYPES-TERMS NON-EXECUTABLEP CTX WRLD STATE))) (ER-PROGN (CHK-ASSUMPTION-FREE-TTREE (CDR PAIR) CTX STATE) (INSTALL-EVENT-DEFUNS NAMES EVENT-FORM DEF-LST0 SYMBOL-CLASS RECLASSIFYINGP NON-EXECUTABLEP PAIR CTX WRLD STATE)))))))))))))))))))))) (10 RECORD-EXPANSION (DEFUN THE-MAGIC-NAME (X) (1- X)) (DEFUN SOME-OTHER-NAME (X) (1+ X))))
(("/usr/share/acl2-6.3/books/hacking/rewrite-code.lisp" "rewrite-code" "rewrite-code" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 720904925))
(("/usr/share/acl2-6.3/books/hacking/dynamic-make-event-test.lisp" "dynamic-make-event-test" "dynamic-make-event-test" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:DEFCODE "/usr/share/acl2-6.3/books/hacking/defcode.lisp" "/usr/share/acl2-6.3/books/hacking/progn-bang-enh.lisp") (:DYNAMIC-MAKE-EVENT-TEST "/usr/share/acl2-6.3/books/hacking/dynamic-make-event-test.lisp"))) . 1656731663) ("/usr/share/acl2-6.3/books/hacking/dynamic-make-event.lisp" "dynamic-make-event" "dynamic-make-event" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 290321638) ("/usr/share/acl2-6.3/books/hacking/redefun.lisp" "redefun" "redefun" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 198064993) ("/usr/share/acl2-6.3/books/hacking/defcode.lisp" "defcode" "defcode" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:DEFCODE "/usr/share/acl2-6.3/books/hacking/progn-bang-enh.lisp" "/usr/share/acl2-6.3/books/hacking/defcode.lisp"))) . 1845433737) ("/usr/share/acl2-6.3/books/hacking/progn-bang-enh.lisp" "progn-bang-enh" "progn-bang-enh" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:DEFCODE "/usr/share/acl2-6.3/books/hacking/progn-bang-enh.lisp"))) . 737908112) ("/usr/share/acl2-6.3/books/hacking/hacker.lisp" "hacker" "hacker" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197252797) ("/usr/share/acl2-6.3/books/hacking/doc-section.lisp" "doc-section" "doc-section" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1293647265) ("/usr/share/acl2-6.3/books/hacking/rewrite-code.lisp" "rewrite-code" "rewrite-code" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 720904925))
656704100
|