/usr/share/acl2-6.3/books/hacking/table-guard.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 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 | (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
((7 RECORD-EXPANSION (PROGN+TOUCHABLE :ALL (REDEFUN+REWRITE TABLE-FN1 (:CARPAT (COND ((EQUAL OLD-GUARD TTERM) %REDUNDANT%) (OLD-GUARD %ER1%) ((GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) %WRLD%) %ER2%) (T %REST%)) :REPL (COND ((EQUAL OLD-GUARD TTERM) %REDUNDANT%) ((AND OLD-GUARD (NOT (TTAG %WRLD%))) %ER1%) ((AND (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) %WRLD%) (NOT (TTAG %WRLD%))) %ER2%) (T %REST%)) :VARS (%REDUNDANT% %ER1% %ER2% %WRLD% %REST%) :MULT 1))) (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 TABLE-FN1 (:CARPAT (COND ((EQUAL OLD-GUARD TTERM) %REDUNDANT%) (OLD-GUARD %ER1%) ((GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) %WRLD%) %ER2%) (T %REST%)) :REPL (COND ((EQUAL OLD-GUARD TTERM) %REDUNDANT%) ((AND OLD-GUARD (NOT (TTAG %WRLD%))) %ER1%) ((AND (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) %WRLD%) (NOT (TTAG %WRLD%))) %ER2%) (T %REST%)) :VARS (%REDUNDANT% %ER1% %ER2% %WRLD% %REST%) :MULT 1))) (PROGN (RECORD-EXPANSION (REDEFUN+REWRITE TABLE-FN1 (:CARPAT (COND ((EQUAL OLD-GUARD TTERM) %REDUNDANT%) (OLD-GUARD %ER1%) ((GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) %WRLD%) %ER2%) (T %REST%)) :REPL (COND ((EQUAL OLD-GUARD TTERM) %REDUNDANT%) ((AND OLD-GUARD (NOT (TTAG %WRLD%))) %ER1%) ((AND (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) %WRLD%) (NOT (TTAG %WRLD%))) %ER2%) (T %REST%)) :VARS (%REDUNDANT% %ER1% %ER2% %WRLD% %REST%) :MULT 1)) (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 TABLE-FN1) (DEFCODE :LOOP (ER-PROGN (ASSERT-NO-SPECIAL-RAW-DEFINITION TABLE-FN1) (CHK-ACCEPTABLE-REDEFUN (QUOTE (TABLE-FN1 (NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (CASE OP (:ALIST (ER-PROGN (CHK-TABLE-NIL-ARGS :ALIST (OR KEY VAL TERM) (COND (KEY (QUOTE (2))) (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (TABLE-ALIST NAME WRLD)))) (:GET (ER-PROGN (CHK-TABLE-NIL-ARGS :GET (OR VAL TERM) (COND (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (CDR (ASSOC-EQUAL KEY (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD)))))) (:PUT (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (LET* ((TBL (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (ER-PROGN (CHK-TABLE-NIL-ARGS :PUT TERM (QUOTE (5)) CTX STATE) (COND ((LET ((PAIR (ASSOC-EQUAL KEY TBL))) (AND PAIR (EQUAL VAL (CDR PAIR)))) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ER-LET* ((PAIR (CHK-TABLE-GUARD NAME KEY VAL CTX WRLD STATE)) (WRLD1 (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) (PUT-ASSOC-EQUAL-FAST KEY VAL TBL) WRLD1) STATE)))))))) (:CLEAR (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS :CLEAR (OR KEY TERM) (COND (KEY (QUOTE (2))) (T (QUOTE (5)))) CTX STATE) (COND ((EQUAL VAL (TABLE-ALIST NAME WRLD)) (STOP-REDUNDANT-EVENT CTX STATE)) ((NOT (ALISTP VAL)) (ER SOFT (QUOTE TABLE) ":CLEAR requires an alist, but ~x0 is not." VAL)) (T (LET ((VAL (IF (DUPLICATE-KEYSP VAL) (REVERSE (CLEAN-UP-ALIST VAL NIL)) VAL))) (ER-LET* ((WRLD1 (ER-LET* ((PAIR (CHK-TABLE-GUARDS NAME VAL CTX WRLD STATE))) (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD)))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) VAL WRLD1) STATE)))))))) (:GUARD (COND ((EQ TERM NIL) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (VALUE (GETPROP NAME (QUOTE TABLE-GUARD) *T* (QUOTE CURRENT-ACL2-WORLD) WRLD)))) (T (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (ER-LET* ((TTERM (TRANSLATE TERM (QUOTE (NIL)) NIL NIL CTX WRLD STATE))) (LET ((OLD-GUARD (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (COND ((EQUAL OLD-GUARD TTERM) (STOP-REDUNDANT-EVENT CTX STATE)) ((AND OLD-GUARD (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to change the :guard on a table ~
after it has been given an explicit :guard. ~
The :guard of ~x0 is ~x1 and this can be ~
changed only by undoing the event that set it. ~
See :DOC table." NAME (UNTRANSLATE (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) T WRLD))) ((AND (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to set the :guard of the ~
non-empty table ~x0. See :DOC table." NAME)) (T (LET ((LEGAL-VARS (QUOTE (KEY VAL WORLD))) (VARS (ALL-VARS TTERM))) (COND ((NOT (SUBSETP-EQ VARS LEGAL-VARS)) (ER SOFT CTX "The only variables permitted in the ~
:guard of a table are ~&0, but your ~
guard uses ~&1. See :DOC table." LEGAL-VARS VARS)) (T (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-GUARD) TTERM WRLD) STATE))))))))))))) (OTHERWISE (ER SOFT CTX "Unrecognized table operation, ~x0. See :DOC table." OP))))) (QUOTE REDEFUN) (W STATE) STATE) (ENSURE-PROGRAM-ONLY-FLAG TABLE-FN1) (DEFUN TABLE-FN1 (NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (CASE OP (:ALIST (ER-PROGN (CHK-TABLE-NIL-ARGS :ALIST (OR KEY VAL TERM) (COND (KEY (QUOTE (2))) (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (TABLE-ALIST NAME WRLD)))) (:GET (ER-PROGN (CHK-TABLE-NIL-ARGS :GET (OR VAL TERM) (COND (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (CDR (ASSOC-EQUAL KEY (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD)))))) (:PUT (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (LET* ((TBL (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (ER-PROGN (CHK-TABLE-NIL-ARGS :PUT TERM (QUOTE (5)) CTX STATE) (COND ((LET ((PAIR (ASSOC-EQUAL KEY TBL))) (AND PAIR (EQUAL VAL (CDR PAIR)))) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ER-LET* ((PAIR (CHK-TABLE-GUARD NAME KEY VAL CTX WRLD STATE)) (WRLD1 (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) (PUT-ASSOC-EQUAL-FAST KEY VAL TBL) WRLD1) STATE)))))))) (:CLEAR (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS :CLEAR (OR KEY TERM) (COND (KEY (QUOTE (2))) (T (QUOTE (5)))) CTX STATE) (COND ((EQUAL VAL (TABLE-ALIST NAME WRLD)) (STOP-REDUNDANT-EVENT CTX STATE)) ((NOT (ALISTP VAL)) (ER SOFT (QUOTE TABLE) ":CLEAR requires an alist, but ~x0 is not." VAL)) (T (LET ((VAL (IF (DUPLICATE-KEYSP VAL) (REVERSE (CLEAN-UP-ALIST VAL NIL)) VAL))) (ER-LET* ((WRLD1 (ER-LET* ((PAIR (CHK-TABLE-GUARDS NAME VAL CTX WRLD STATE))) (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD)))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) VAL WRLD1) STATE)))))))) (:GUARD (COND ((EQ TERM NIL) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (VALUE (GETPROP NAME (QUOTE TABLE-GUARD) *T* (QUOTE CURRENT-ACL2-WORLD) WRLD)))) (T (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (ER-LET* ((TTERM (TRANSLATE TERM (QUOTE (NIL)) NIL NIL CTX WRLD STATE))) (LET ((OLD-GUARD (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (COND ((EQUAL OLD-GUARD TTERM) (STOP-REDUNDANT-EVENT CTX STATE)) ((AND OLD-GUARD (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to change the :guard on a table ~
after it has been given an explicit :guard. ~
The :guard of ~x0 is ~x1 and this can be ~
changed only by undoing the event that set it. ~
See :DOC table." NAME (UNTRANSLATE (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) T WRLD))) ((AND (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to set the :guard of the ~
non-empty table ~x0. See :DOC table." NAME)) (T (LET ((LEGAL-VARS (QUOTE (KEY VAL WORLD))) (VARS (ALL-VARS TTERM))) (COND ((NOT (SUBSETP-EQ VARS LEGAL-VARS)) (ER SOFT CTX "The only variables permitted in the ~
:guard of a table are ~&0, but your ~
guard uses ~&1. See :DOC table." LEGAL-VARS VARS)) (T (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-GUARD) TTERM WRLD) STATE))))))))))))) (OTHERWISE (ER SOFT CTX "Unrecognized table operation, ~x0. See :DOC table." OP))))) :EXTEND (IN-RAW-MODE (DEFUN-*1* TABLE-FN1 (NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (IF (F-GET-GLOBAL (QUOTE SAFE-MODE) *THE-LIVE-STATE*) (THROW-RAW-EV-FNCALL (LIST (QUOTE PROGRAM-ONLY-ER) (QUOTE TABLE-FN1) (LIST NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (QUOTE T) (QUOTE (NIL)) T)) (TABLE-FN1 NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM)))) :COMPILE (DEFUN TABLE-FN1 (NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (CASE OP (:ALIST (ER-PROGN (CHK-TABLE-NIL-ARGS :ALIST (OR KEY VAL TERM) (COND (KEY (QUOTE (2))) (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (TABLE-ALIST NAME WRLD)))) (:GET (ER-PROGN (CHK-TABLE-NIL-ARGS :GET (OR VAL TERM) (COND (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (CDR (ASSOC-EQUAL KEY (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD)))))) (:PUT (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (LET* ((TBL (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (ER-PROGN (CHK-TABLE-NIL-ARGS :PUT TERM (QUOTE (5)) CTX STATE) (COND ((LET ((PAIR (ASSOC-EQUAL KEY TBL))) (AND PAIR (EQUAL VAL (CDR PAIR)))) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ER-LET* ((PAIR (CHK-TABLE-GUARD NAME KEY VAL CTX WRLD STATE)) (WRLD1 (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) (PUT-ASSOC-EQUAL-FAST KEY VAL TBL) WRLD1) STATE)))))))) (:CLEAR (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS :CLEAR (OR KEY TERM) (COND (KEY (QUOTE (2))) (T (QUOTE (5)))) CTX STATE) (COND ((EQUAL VAL (TABLE-ALIST NAME WRLD)) (STOP-REDUNDANT-EVENT CTX STATE)) ((NOT (ALISTP VAL)) (ER SOFT (QUOTE TABLE) ":CLEAR requires an alist, but ~x0 is not." VAL)) (T (LET ((VAL (IF (DUPLICATE-KEYSP VAL) (REVERSE (CLEAN-UP-ALIST VAL NIL)) VAL))) (ER-LET* ((WRLD1 (ER-LET* ((PAIR (CHK-TABLE-GUARDS NAME VAL CTX WRLD STATE))) (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD)))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) VAL WRLD1) STATE)))))))) (:GUARD (COND ((EQ TERM NIL) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (VALUE (GETPROP NAME (QUOTE TABLE-GUARD) *T* (QUOTE CURRENT-ACL2-WORLD) WRLD)))) (T (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (ER-LET* ((TTERM (TRANSLATE TERM (QUOTE (NIL)) NIL NIL CTX WRLD STATE))) (LET ((OLD-GUARD (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (COND ((EQUAL OLD-GUARD TTERM) (STOP-REDUNDANT-EVENT CTX STATE)) ((AND OLD-GUARD (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to change the :guard on a table ~
after it has been given an explicit :guard. ~
The :guard of ~x0 is ~x1 and this can be ~
changed only by undoing the event that set it. ~
See :DOC table." NAME (UNTRANSLATE (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) T WRLD))) ((AND (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to set the :guard of the ~
non-empty table ~x0. See :DOC table." NAME)) (T (LET ((LEGAL-VARS (QUOTE (KEY VAL WORLD))) (VARS (ALL-VARS TTERM))) (COND ((NOT (SUBSETP-EQ VARS LEGAL-VARS)) (ER SOFT CTX "The only variables permitted in the ~
:guard of a table are ~&0, but your ~
guard uses ~&1. See :DOC table." LEGAL-VARS VARS)) (T (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-GUARD) TTERM WRLD) STATE))))))))))))) (OTHERWISE (ER SOFT CTX "Unrecognized table operation, ~x0. See :DOC table." OP)))))) (PROGN (RECORD-EXPANSION (ASSERT-INCLUDE-DEFUN-MATCHES-CERTIFY-DEFUN TABLE-FN1) (VALUE-TRIPLE (LET ((REWRITE-CODE::CERTIFY-TIME-DEFUN (QUOTE (DEFUN TABLE-FN1 (NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (CASE OP (:ALIST (ER-PROGN (CHK-TABLE-NIL-ARGS :ALIST (OR KEY VAL TERM) (COND (KEY (QUOTE (2))) (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (TABLE-ALIST NAME WRLD)))) (:GET (ER-PROGN (CHK-TABLE-NIL-ARGS :GET (OR VAL TERM) (COND (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (CDR (ASSOC-EQUAL KEY (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD)))))) (:PUT (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (LET* ((TBL (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (ER-PROGN (CHK-TABLE-NIL-ARGS :PUT TERM (QUOTE (5)) CTX STATE) (COND ((LET ((PAIR (ASSOC-EQUAL KEY TBL))) (AND PAIR (EQUAL VAL (CDR PAIR)))) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ER-LET* ((PAIR (CHK-TABLE-GUARD NAME KEY VAL CTX WRLD STATE)) (WRLD1 (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) (PUT-ASSOC-EQUAL-FAST KEY VAL TBL) WRLD1) STATE)))))))) (:CLEAR (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS :CLEAR (OR KEY TERM) (COND (KEY (QUOTE (2))) (T (QUOTE (5)))) CTX STATE) (COND ((EQUAL VAL (TABLE-ALIST NAME WRLD)) (STOP-REDUNDANT-EVENT CTX STATE)) ((NOT (ALISTP VAL)) (ER SOFT (QUOTE TABLE) ":CLEAR requires an alist, but ~x0 is not." VAL)) (T (LET ((VAL (IF (DUPLICATE-KEYSP VAL) (REVERSE (CLEAN-UP-ALIST VAL NIL)) VAL))) (ER-LET* ((WRLD1 (ER-LET* ((PAIR (CHK-TABLE-GUARDS NAME VAL CTX WRLD STATE))) (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD)))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) VAL WRLD1) STATE)))))))) (:GUARD (COND ((EQ TERM NIL) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (VALUE (GETPROP NAME (QUOTE TABLE-GUARD) *T* (QUOTE CURRENT-ACL2-WORLD) WRLD)))) (T (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (ER-LET* ((TTERM (TRANSLATE TERM (QUOTE (NIL)) NIL NIL CTX WRLD STATE))) (LET ((OLD-GUARD (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (COND ((EQUAL OLD-GUARD TTERM) (STOP-REDUNDANT-EVENT CTX STATE)) (OLD-GUARD (ER SOFT CTX "It is illegal to change the :guard on a table ~
after it has been given an explicit :guard. ~
The :guard of ~x0 is ~x1 and this can be ~
changed only by undoing the event that set it. ~
See :DOC table." NAME (UNTRANSLATE (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) T WRLD))) ((GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) (ER SOFT CTX "It is illegal to set the :guard of the ~
non-empty table ~x0. See :DOC table." NAME)) (T (LET ((LEGAL-VARS (QUOTE (KEY VAL WORLD))) (VARS (ALL-VARS TTERM))) (COND ((NOT (SUBSETP-EQ VARS LEGAL-VARS)) (ER SOFT CTX "The only variables permitted in the ~
:guard of a table are ~&0, but your ~
guard uses ~&1. See :DOC table." LEGAL-VARS VARS)) (T (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-GUARD) TTERM WRLD) STATE))))))))))))) (OTHERWISE (ER SOFT CTX "Unrecognized table operation, ~x0. See :DOC table." OP)))))) (REWRITE-CODE::INCLUDE-TIME-DEFUN (GET-DEFUN (QUOTE TABLE-FN1) 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 TABLE-FN1) (CHK-ACCEPTABLE-REDEFUN (QUOTE (TABLE-FN1 (NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (CASE OP (:ALIST (ER-PROGN (CHK-TABLE-NIL-ARGS :ALIST (OR KEY VAL TERM) (COND (KEY (QUOTE (2))) (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (TABLE-ALIST NAME WRLD)))) (:GET (ER-PROGN (CHK-TABLE-NIL-ARGS :GET (OR VAL TERM) (COND (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (CDR (ASSOC-EQUAL KEY (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD)))))) (:PUT (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (LET* ((TBL (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (ER-PROGN (CHK-TABLE-NIL-ARGS :PUT TERM (QUOTE (5)) CTX STATE) (COND ((LET ((PAIR (ASSOC-EQUAL KEY TBL))) (AND PAIR (EQUAL VAL (CDR PAIR)))) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ER-LET* ((PAIR (CHK-TABLE-GUARD NAME KEY VAL CTX WRLD STATE)) (WRLD1 (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) (PUT-ASSOC-EQUAL-FAST KEY VAL TBL) WRLD1) STATE)))))))) (:CLEAR (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS :CLEAR (OR KEY TERM) (COND (KEY (QUOTE (2))) (T (QUOTE (5)))) CTX STATE) (COND ((EQUAL VAL (TABLE-ALIST NAME WRLD)) (STOP-REDUNDANT-EVENT CTX STATE)) ((NOT (ALISTP VAL)) (ER SOFT (QUOTE TABLE) ":CLEAR requires an alist, but ~x0 is not." VAL)) (T (LET ((VAL (IF (DUPLICATE-KEYSP VAL) (REVERSE (CLEAN-UP-ALIST VAL NIL)) VAL))) (ER-LET* ((WRLD1 (ER-LET* ((PAIR (CHK-TABLE-GUARDS NAME VAL CTX WRLD STATE))) (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD)))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) VAL WRLD1) STATE)))))))) (:GUARD (COND ((EQ TERM NIL) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (VALUE (GETPROP NAME (QUOTE TABLE-GUARD) *T* (QUOTE CURRENT-ACL2-WORLD) WRLD)))) (T (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (ER-LET* ((TTERM (TRANSLATE TERM (QUOTE (NIL)) NIL NIL CTX WRLD STATE))) (LET ((OLD-GUARD (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (COND ((EQUAL OLD-GUARD TTERM) (STOP-REDUNDANT-EVENT CTX STATE)) ((AND OLD-GUARD (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to change the :guard on a table ~
after it has been given an explicit :guard. ~
The :guard of ~x0 is ~x1 and this can be ~
changed only by undoing the event that set it. ~
See :DOC table." NAME (UNTRANSLATE (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) T WRLD))) ((AND (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to set the :guard of the ~
non-empty table ~x0. See :DOC table." NAME)) (T (LET ((LEGAL-VARS (QUOTE (KEY VAL WORLD))) (VARS (ALL-VARS TTERM))) (COND ((NOT (SUBSETP-EQ VARS LEGAL-VARS)) (ER SOFT CTX "The only variables permitted in the ~
:guard of a table are ~&0, but your ~
guard uses ~&1. See :DOC table." LEGAL-VARS VARS)) (T (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-GUARD) TTERM WRLD) STATE))))))))))))) (OTHERWISE (ER SOFT CTX "Unrecognized table operation, ~x0. See :DOC table." OP))))) (QUOTE REDEFUN) (W STATE) STATE) (ENSURE-PROGRAM-ONLY-FLAG TABLE-FN1) (DEFUN TABLE-FN1 (NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (CASE OP (:ALIST (ER-PROGN (CHK-TABLE-NIL-ARGS :ALIST (OR KEY VAL TERM) (COND (KEY (QUOTE (2))) (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (TABLE-ALIST NAME WRLD)))) (:GET (ER-PROGN (CHK-TABLE-NIL-ARGS :GET (OR VAL TERM) (COND (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (CDR (ASSOC-EQUAL KEY (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD)))))) (:PUT (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (LET* ((TBL (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (ER-PROGN (CHK-TABLE-NIL-ARGS :PUT TERM (QUOTE (5)) CTX STATE) (COND ((LET ((PAIR (ASSOC-EQUAL KEY TBL))) (AND PAIR (EQUAL VAL (CDR PAIR)))) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ER-LET* ((PAIR (CHK-TABLE-GUARD NAME KEY VAL CTX WRLD STATE)) (WRLD1 (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) (PUT-ASSOC-EQUAL-FAST KEY VAL TBL) WRLD1) STATE)))))))) (:CLEAR (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS :CLEAR (OR KEY TERM) (COND (KEY (QUOTE (2))) (T (QUOTE (5)))) CTX STATE) (COND ((EQUAL VAL (TABLE-ALIST NAME WRLD)) (STOP-REDUNDANT-EVENT CTX STATE)) ((NOT (ALISTP VAL)) (ER SOFT (QUOTE TABLE) ":CLEAR requires an alist, but ~x0 is not." VAL)) (T (LET ((VAL (IF (DUPLICATE-KEYSP VAL) (REVERSE (CLEAN-UP-ALIST VAL NIL)) VAL))) (ER-LET* ((WRLD1 (ER-LET* ((PAIR (CHK-TABLE-GUARDS NAME VAL CTX WRLD STATE))) (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD)))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) VAL WRLD1) STATE)))))))) (:GUARD (COND ((EQ TERM NIL) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (VALUE (GETPROP NAME (QUOTE TABLE-GUARD) *T* (QUOTE CURRENT-ACL2-WORLD) WRLD)))) (T (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (ER-LET* ((TTERM (TRANSLATE TERM (QUOTE (NIL)) NIL NIL CTX WRLD STATE))) (LET ((OLD-GUARD (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (COND ((EQUAL OLD-GUARD TTERM) (STOP-REDUNDANT-EVENT CTX STATE)) ((AND OLD-GUARD (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to change the :guard on a table ~
after it has been given an explicit :guard. ~
The :guard of ~x0 is ~x1 and this can be ~
changed only by undoing the event that set it. ~
See :DOC table." NAME (UNTRANSLATE (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) T WRLD))) ((AND (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to set the :guard of the ~
non-empty table ~x0. See :DOC table." NAME)) (T (LET ((LEGAL-VARS (QUOTE (KEY VAL WORLD))) (VARS (ALL-VARS TTERM))) (COND ((NOT (SUBSETP-EQ VARS LEGAL-VARS)) (ER SOFT CTX "The only variables permitted in the ~
:guard of a table are ~&0, but your ~
guard uses ~&1. See :DOC table." LEGAL-VARS VARS)) (T (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-GUARD) TTERM WRLD) STATE))))))))))))) (OTHERWISE (ER SOFT CTX "Unrecognized table operation, ~x0. See :DOC table." OP))))) :EXTEND (IN-RAW-MODE (DEFUN-*1* TABLE-FN1 (NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (IF (F-GET-GLOBAL (QUOTE SAFE-MODE) *THE-LIVE-STATE*) (THROW-RAW-EV-FNCALL (LIST (QUOTE PROGRAM-ONLY-ER) (QUOTE TABLE-FN1) (LIST NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (QUOTE T) (QUOTE (NIL)) T)) (TABLE-FN1 NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM)))) :COMPILE (DEFUN TABLE-FN1 (NAME KEY VAL OP TERM CTX WRLD STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (CASE OP (:ALIST (ER-PROGN (CHK-TABLE-NIL-ARGS :ALIST (OR KEY VAL TERM) (COND (KEY (QUOTE (2))) (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (TABLE-ALIST NAME WRLD)))) (:GET (ER-PROGN (CHK-TABLE-NIL-ARGS :GET (OR VAL TERM) (COND (VAL (QUOTE (3))) (T (QUOTE (5)))) CTX STATE) (VALUE (CDR (ASSOC-EQUAL KEY (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD)))))) (:PUT (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (LET* ((TBL (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (ER-PROGN (CHK-TABLE-NIL-ARGS :PUT TERM (QUOTE (5)) CTX STATE) (COND ((LET ((PAIR (ASSOC-EQUAL KEY TBL))) (AND PAIR (EQUAL VAL (CDR PAIR)))) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ER-LET* ((PAIR (CHK-TABLE-GUARD NAME KEY VAL CTX WRLD STATE)) (WRLD1 (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) (PUT-ASSOC-EQUAL-FAST KEY VAL TBL) WRLD1) STATE)))))))) (:CLEAR (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS :CLEAR (OR KEY TERM) (COND (KEY (QUOTE (2))) (T (QUOTE (5)))) CTX STATE) (COND ((EQUAL VAL (TABLE-ALIST NAME WRLD)) (STOP-REDUNDANT-EVENT CTX STATE)) ((NOT (ALISTP VAL)) (ER SOFT (QUOTE TABLE) ":CLEAR requires an alist, but ~x0 is not." VAL)) (T (LET ((VAL (IF (DUPLICATE-KEYSP VAL) (REVERSE (CLEAN-UP-ALIST VAL NIL)) VAL))) (ER-LET* ((WRLD1 (ER-LET* ((PAIR (CHK-TABLE-GUARDS NAME VAL CTX WRLD STATE))) (COND ((NULL PAIR) (VALUE WRLD)) (T (LET ((TTAGS-ALLOWED1 (CAR PAIR)) (TTAGS-SEEN1 (CDR PAIR))) (PPROGN (F-PUT-GLOBAL (QUOTE TTAGS-ALLOWED) TTAGS-ALLOWED1 STATE) (VALUE (GLOBAL-SET? (QUOTE TTAGS-SEEN) TTAGS-SEEN1 WRLD (GLOBAL-VAL (QUOTE TTAGS-SEEN) WRLD)))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-ALIST) VAL WRLD1) STATE)))))))) (:GUARD (COND ((EQ TERM NIL) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (VALUE (GETPROP NAME (QUOTE TABLE-GUARD) *T* (QUOTE CURRENT-ACL2-WORLD) WRLD)))) (T (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM CTX) (ER-PROGN (CHK-TABLE-NIL-ARGS OP (OR KEY VAL) (COND (KEY (QUOTE (2))) (T (QUOTE (3)))) CTX STATE) (ER-LET* ((TTERM (TRANSLATE TERM (QUOTE (NIL)) NIL NIL CTX WRLD STATE))) (LET ((OLD-GUARD (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD))) (COND ((EQUAL OLD-GUARD TTERM) (STOP-REDUNDANT-EVENT CTX STATE)) ((AND OLD-GUARD (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to change the :guard on a table ~
after it has been given an explicit :guard. ~
The :guard of ~x0 is ~x1 and this can be ~
changed only by undoing the event that set it. ~
See :DOC table." NAME (UNTRANSLATE (GETPROP NAME (QUOTE TABLE-GUARD) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) T WRLD))) ((AND (GETPROP NAME (QUOTE TABLE-ALIST) NIL (QUOTE CURRENT-ACL2-WORLD) WRLD) (NOT (TTAG WRLD))) (ER SOFT CTX "It is illegal to set the :guard of the ~
non-empty table ~x0. See :DOC table." NAME)) (T (LET ((LEGAL-VARS (QUOTE (KEY VAL WORLD))) (VARS (ALL-VARS TTERM))) (COND ((NOT (SUBSETP-EQ VARS LEGAL-VARS)) (ER SOFT CTX "The only variables permitted in the ~
:guard of a table are ~&0, but your ~
guard uses ~&1. See :DOC table." LEGAL-VARS VARS)) (T (INSTALL-EVENT NAME EVENT-FORM (QUOTE TABLE) 0 NIL (TABLE-CLTL-CMD NAME KEY VAL OP CTX WRLD) NIL NIL (PUTPROP NAME (QUOTE TABLE-GUARD) TTERM WRLD) STATE))))))))))))) (OTHERWISE (ER SOFT CTX "Unrecognized table operation, ~x0. See :DOC table." OP))))))))))))))
(("/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/table-guard.lisp" "table-guard" "table-guard" ((: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") (:TABLE-GUARD "/usr/share/acl2-6.3/books/hacking/table-guard.lisp"))) . 1640973006) ("/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))
98022789
|