/usr/share/acl2-6.3/books/ccg/ccg.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "REWRITE-CODE" (APPEND (QUOTE (VALUE ER-LET* ER-DECODE-LOGICAL-NAME GETPROP CURRENT-ACL2-WORLD STOBJS-IN CLTL-COMMAND GLOBAL-VALUE SOFT)) (QUOTE (ER-REWRITE-FORM GET-DEFUN COMPUTE-COPY-DEFUN+REWRITE ASSERT-INCLUDE-DEFUN-MATCHES-CERTIFY-DEFUN COPY-DEFUN+REWRITE COPY-DEFUN)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)) NIL ((:SYSTEM . "hacking/all.lisp")) T)
(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*)) NIL ((:SYSTEM . "hacking/hacker.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((7 RECORD-EXPANSION (ADD-ACL2-DEFAULTS-TABLE-KEY :TERMINATION-METHOD (MEMBER-EQ VAL (QUOTE (:MEASURE :CCG)))) (PROGN (RECORD-EXPANSION (REWRITE-TABLE-GUARD ACL2-DEFAULTS-TABLE (:CARPAT %BODY% :VARS %BODY% :REPL (IF (EQ KEY (QUOTE :TERMINATION-METHOD)) (MEMBER-EQ VAL (QUOTE (:MEASURE :CCG))) %BODY%))) (TABLE ACL2-DEFAULTS-TABLE NIL NIL :GUARD (IF (EQ KEY (QUOTE :TERMINATION-METHOD)) (MEMBER-EQ VAL (QUOTE (:MEASURE :CCG))) (IF (EQ KEY (QUOTE :DEFUN-MODE)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (:LOGIC :PROGRAM))) (IF (EQ KEY (QUOTE :VERIFY-GUARDS-EAGERNESS)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQL-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (0 1 2))) (IF (EQ KEY (QUOTE :ENFORCE-REDUNDANCY)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :IGNORE-DOC-STRING-ERROR)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :COMPILE-FNS)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL))) (IF (EQ KEY (QUOTE :MEASURE-FUNCTION)) (IF (SYMBOLP VAL) (IF (FUNCTION-SYMBOLP VAL WORLD) (= (LENGTH (FGETPROP VAL (QUOTE FORMALS) (QUOTE T) WORLD)) (QUOTE 1)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :WELL-FOUNDED-RELATION)) (IF (SYMBOLP VAL) ((LAMBDA (X ALIST) (RETURN-LAST (QUOTE MBE1-RAW) (ASSOC-EQ-EXEC X ALIST) (ASSOC-EQUAL X ALIST))) VAL (GLOBAL-VAL (QUOTE WELL-FOUNDED-RELATION-ALIST) WORLD)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :BOGUS-DEFUN-HINTS-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :BOGUS-MUTUAL-RECURSION-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :IRRELEVANT-FORMALS-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :IGNORE-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :BDD-CONSTRUCTORS)) (SYMBOL-LISTP VAL) (IF (EQ KEY (QUOTE :TTAG)) (IF (NULL VAL) (NULL VAL) (IF (KEYWORDP VAL) (NOT (EQUAL (SYMBOL-NAME VAL) (QUOTE "NIL"))) (QUOTE NIL))) (IF (EQ KEY (QUOTE :STATE-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL))) (IF (EQ KEY (QUOTE :LET*-ABSTRACTIONP)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL))) (IF (EQ KEY (QUOTE :NU-REWRITER-MODE)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (NIL T :LITERALS))) (IF (EQ KEY (QUOTE :BACKCHAIN-LIMIT)) (IF (TRUE-LISTP VAL) (IF (EQUAL (LENGTH VAL) (QUOTE 2)) (IF (IF (NULL (CAR VAL)) (NULL (CAR VAL)) (NATP (CAR VAL))) (IF (NULL (CAR (CDR VAL))) (NULL (CAR (CDR VAL))) (NATP (CAR (CDR VAL)))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :STEP-LIMIT)) (IF (NATP VAL) (NOT (< (QUOTE 536870911) VAL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :DEFAULT-BACKCHAIN-LIMIT)) (IF (TRUE-LISTP VAL) (IF (EQUAL (LENGTH VAL) (QUOTE 2)) (IF (IF (NULL (CAR VAL)) (NULL (CAR VAL)) (NATP (CAR VAL))) (IF (NULL (CAR (CDR VAL))) (NULL (CAR (CDR VAL))) (NATP (CAR (CDR VAL)))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :REWRITE-STACK-LIMIT)) (UNSIGNED-BYTE-P (QUOTE 29) VAL) (IF (EQ KEY (QUOTE :CASE-SPLIT-LIMITATIONS)) (IF (TRUE-LISTP VAL) (IF (EQUAL (LENGTH VAL) (QUOTE 2)) (IF (IF (NULL (CAR VAL)) (NULL (CAR VAL)) (NATP (CAR VAL))) (IF (NULL (CAR (CDR VAL))) (NULL (CAR (CDR VAL))) (NATP (CAR (CDR VAL)))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :MATCH-FREE-DEFAULT)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (:ONCE :ALL NIL))) (IF (EQ KEY (QUOTE :MATCH-FREE-OVERRIDE)) (IF (EQ VAL (QUOTE :CLEAR)) (EQ VAL (QUOTE :CLEAR)) (NULL (NON-FREE-VAR-RUNES VAL (FREE-VAR-RUNES (QUOTE :ONCE) WORLD) (FREE-VAR-RUNES (QUOTE :ALL) WORLD) (QUOTE NIL)))) (IF (EQ KEY (QUOTE :MATCH-FREE-OVERRIDE-NUME)) (INTEGERP VAL) (IF (EQ KEY (QUOTE :NON-LINEARP)) (BOOLEANP VAL) (IF (EQ KEY (QUOTE :TAU-AUTO-MODEP)) (BOOLEANP VAL) (IF (EQ KEY (QUOTE :INCLUDE-BOOK-DIR-ALIST)) (IF (INCLUDE-BOOK-DIR-ALISTP VAL (OS WORLD)) (NULL ((LAMBDA (X ALIST) (RETURN-LAST (QUOTE MBE1-RAW) (ASSOC-EQ-EXEC X ALIST) (ASSOC-EQUAL X ALIST))) (QUOTE :SYSTEM) VAL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :RULER-EXTENDERS)) (IF (EQ VAL (QUOTE :ALL)) (EQ VAL (QUOTE :ALL)) ((LAMBDA (CTX ERR-STR MSG) (IF MSG (ILLEGAL CTX ERR-STR (CONS (CONS (QUOTE #\0) MSG) (QUOTE NIL))) (QUOTE T))) (QUOTE ACL2-DEFAULTS-TABLE) (QUOTE "The proposed ruler-extenders is illegal because ~@0.") (RULER-EXTENDERS-MSG VAL WORLD))) (QUOTE NIL)))))))))))))))))))))))))))))))) (DEFMACRO SET-TERMINATION-METHOD (V) (CONS (QUOTE WITH-OUTPUT) (CONS (QUOTE :OFF) (CONS (QUOTE SUMMARY) (CONS (CONS (QUOTE PROGN) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ACL2-DEFAULTS-TABLE) (CONS (QUOTE :TERMINATION-METHOD) (CONS (CONS (QUOTE QUOTE) (CONS V (QUOTE NIL))) (QUOTE NIL))))) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ACL2-DEFAULTS-TABLE) (CONS (QUOTE :TERMINATION-METHOD) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL)))))))) (20 RECORD-EXPANSION (REWRITE-TABLE-GUARD ACL2-DEFAULTS-TABLE (:CARPAT %BODY% :VARS %BODY% :REPL (IF (EQ KEY :CCG-HIERARCHY) (NON-EMPTY-HLEVEL-LISTP VAL) %BODY%))) (TABLE ACL2-DEFAULTS-TABLE NIL NIL :GUARD (IF (EQ KEY :CCG-HIERARCHY) (NON-EMPTY-HLEVEL-LISTP VAL) (IF (EQ KEY (QUOTE :TERMINATION-METHOD)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (:MEASURE :CCG))) (IF (EQ KEY (QUOTE :DEFUN-MODE)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (:LOGIC :PROGRAM))) (IF (EQ KEY (QUOTE :VERIFY-GUARDS-EAGERNESS)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQL-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (0 1 2))) (IF (EQ KEY (QUOTE :ENFORCE-REDUNDANCY)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :IGNORE-DOC-STRING-ERROR)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :COMPILE-FNS)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL))) (IF (EQ KEY (QUOTE :MEASURE-FUNCTION)) (IF (SYMBOLP VAL) (IF (FUNCTION-SYMBOLP VAL WORLD) (= (LENGTH (FGETPROP VAL (QUOTE FORMALS) (QUOTE T) WORLD)) (QUOTE 1)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :WELL-FOUNDED-RELATION)) (IF (SYMBOLP VAL) ((LAMBDA (X ALIST) (RETURN-LAST (QUOTE MBE1-RAW) (ASSOC-EQ-EXEC X ALIST) (ASSOC-EQUAL X ALIST))) VAL (GLOBAL-VAL (QUOTE WELL-FOUNDED-RELATION-ALIST) WORLD)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :BOGUS-DEFUN-HINTS-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :BOGUS-MUTUAL-RECURSION-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :IRRELEVANT-FORMALS-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :IGNORE-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :BDD-CONSTRUCTORS)) (SYMBOL-LISTP VAL) (IF (EQ KEY (QUOTE :TTAG)) (IF (NULL VAL) (NULL VAL) (IF (KEYWORDP VAL) (NOT (EQUAL (SYMBOL-NAME VAL) (QUOTE "NIL"))) (QUOTE NIL))) (IF (EQ KEY (QUOTE :STATE-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL))) (IF (EQ KEY (QUOTE :LET*-ABSTRACTIONP)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL))) (IF (EQ KEY (QUOTE :NU-REWRITER-MODE)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (NIL T :LITERALS))) (IF (EQ KEY (QUOTE :BACKCHAIN-LIMIT)) (IF (TRUE-LISTP VAL) (IF (EQUAL (LENGTH VAL) (QUOTE 2)) (IF (IF (NULL (CAR VAL)) (NULL (CAR VAL)) (NATP (CAR VAL))) (IF (NULL (CAR (CDR VAL))) (NULL (CAR (CDR VAL))) (NATP (CAR (CDR VAL)))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :STEP-LIMIT)) (IF (NATP VAL) (NOT (< (QUOTE 536870911) VAL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :DEFAULT-BACKCHAIN-LIMIT)) (IF (TRUE-LISTP VAL) (IF (EQUAL (LENGTH VAL) (QUOTE 2)) (IF (IF (NULL (CAR VAL)) (NULL (CAR VAL)) (NATP (CAR VAL))) (IF (NULL (CAR (CDR VAL))) (NULL (CAR (CDR VAL))) (NATP (CAR (CDR VAL)))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :REWRITE-STACK-LIMIT)) (UNSIGNED-BYTE-P (QUOTE 29) VAL) (IF (EQ KEY (QUOTE :CASE-SPLIT-LIMITATIONS)) (IF (TRUE-LISTP VAL) (IF (EQUAL (LENGTH VAL) (QUOTE 2)) (IF (IF (NULL (CAR VAL)) (NULL (CAR VAL)) (NATP (CAR VAL))) (IF (NULL (CAR (CDR VAL))) (NULL (CAR (CDR VAL))) (NATP (CAR (CDR VAL)))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :MATCH-FREE-DEFAULT)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (:ONCE :ALL NIL))) (IF (EQ KEY (QUOTE :MATCH-FREE-OVERRIDE)) (IF (EQ VAL (QUOTE :CLEAR)) (EQ VAL (QUOTE :CLEAR)) (NULL (NON-FREE-VAR-RUNES VAL (FREE-VAR-RUNES (QUOTE :ONCE) WORLD) (FREE-VAR-RUNES (QUOTE :ALL) WORLD) (QUOTE NIL)))) (IF (EQ KEY (QUOTE :MATCH-FREE-OVERRIDE-NUME)) (INTEGERP VAL) (IF (EQ KEY (QUOTE :NON-LINEARP)) (BOOLEANP VAL) (IF (EQ KEY (QUOTE :TAU-AUTO-MODEP)) (BOOLEANP VAL) (IF (EQ KEY (QUOTE :INCLUDE-BOOK-DIR-ALIST)) (IF (INCLUDE-BOOK-DIR-ALISTP VAL (OS WORLD)) (NULL ((LAMBDA (X ALIST) (RETURN-LAST (QUOTE MBE1-RAW) (ASSOC-EQ-EXEC X ALIST) (ASSOC-EQUAL X ALIST))) (QUOTE :SYSTEM) VAL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :RULER-EXTENDERS)) (IF (EQ VAL (QUOTE :ALL)) (EQ VAL (QUOTE :ALL)) ((LAMBDA (CTX ERR-STR MSG) (IF MSG (ILLEGAL CTX ERR-STR (CONS (CONS (QUOTE #\0) MSG) (QUOTE NIL))) (QUOTE T))) (QUOTE ACL2-DEFAULTS-TABLE) (QUOTE "The proposed ruler-extenders is illegal because ~@0.") (RULER-EXTENDERS-MSG VAL WORLD))) (QUOTE NIL))))))))))))))))))))))))))))))))) (31 RECORD-EXPANSION (ADD-ACL2-DEFAULTS-TABLE-KEY :CCG-TIME-LIMIT (OR (NULL VAL) (AND (RATIONALP VAL) (< 0 VAL)))) (PROGN (RECORD-EXPANSION (REWRITE-TABLE-GUARD ACL2-DEFAULTS-TABLE (:CARPAT %BODY% :VARS %BODY% :REPL (IF (EQ KEY (QUOTE :CCG-TIME-LIMIT)) (OR (NULL VAL) (AND (RATIONALP VAL) (< 0 VAL))) %BODY%))) (TABLE ACL2-DEFAULTS-TABLE NIL NIL :GUARD (IF (EQ KEY (QUOTE :CCG-TIME-LIMIT)) (OR (NULL VAL) (AND (RATIONALP VAL) (< 0 VAL))) (IF (EQ KEY (QUOTE :CCG-HIERARCHY)) (NON-EMPTY-HLEVEL-LISTP VAL) (IF (EQ KEY (QUOTE :TERMINATION-METHOD)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (:MEASURE :CCG))) (IF (EQ KEY (QUOTE :DEFUN-MODE)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (:LOGIC :PROGRAM))) (IF (EQ KEY (QUOTE :VERIFY-GUARDS-EAGERNESS)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQL-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (0 1 2))) (IF (EQ KEY (QUOTE :ENFORCE-REDUNDANCY)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :IGNORE-DOC-STRING-ERROR)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :COMPILE-FNS)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL))) (IF (EQ KEY (QUOTE :MEASURE-FUNCTION)) (IF (SYMBOLP VAL) (IF (FUNCTION-SYMBOLP VAL WORLD) (= (LENGTH (FGETPROP VAL (QUOTE FORMALS) (QUOTE T) WORLD)) (QUOTE 1)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :WELL-FOUNDED-RELATION)) (IF (SYMBOLP VAL) ((LAMBDA (X ALIST) (RETURN-LAST (QUOTE MBE1-RAW) (ASSOC-EQ-EXEC X ALIST) (ASSOC-EQUAL X ALIST))) VAL (GLOBAL-VAL (QUOTE WELL-FOUNDED-RELATION-ALIST) WORLD)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :BOGUS-DEFUN-HINTS-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :BOGUS-MUTUAL-RECURSION-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :IRRELEVANT-FORMALS-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :IGNORE-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL :WARN))) (IF (EQ KEY (QUOTE :BDD-CONSTRUCTORS)) (SYMBOL-LISTP VAL) (IF (EQ KEY (QUOTE :TTAG)) (IF (NULL VAL) (NULL VAL) (IF (KEYWORDP VAL) (NOT (EQUAL (SYMBOL-NAME VAL) (QUOTE "NIL"))) (QUOTE NIL))) (IF (EQ KEY (QUOTE :STATE-OK)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL))) (IF (EQ KEY (QUOTE :LET*-ABSTRACTIONP)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (T NIL))) (IF (EQ KEY (QUOTE :NU-REWRITER-MODE)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (NIL T :LITERALS))) (IF (EQ KEY (QUOTE :BACKCHAIN-LIMIT)) (IF (TRUE-LISTP VAL) (IF (EQUAL (LENGTH VAL) (QUOTE 2)) (IF (IF (NULL (CAR VAL)) (NULL (CAR VAL)) (NATP (CAR VAL))) (IF (NULL (CAR (CDR VAL))) (NULL (CAR (CDR VAL))) (NATP (CAR (CDR VAL)))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :STEP-LIMIT)) (IF (NATP VAL) (NOT (< (QUOTE 536870911) VAL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :DEFAULT-BACKCHAIN-LIMIT)) (IF (TRUE-LISTP VAL) (IF (EQUAL (LENGTH VAL) (QUOTE 2)) (IF (IF (NULL (CAR VAL)) (NULL (CAR VAL)) (NATP (CAR VAL))) (IF (NULL (CAR (CDR VAL))) (NULL (CAR (CDR VAL))) (NATP (CAR (CDR VAL)))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :REWRITE-STACK-LIMIT)) (UNSIGNED-BYTE-P (QUOTE 29) VAL) (IF (EQ KEY (QUOTE :CASE-SPLIT-LIMITATIONS)) (IF (TRUE-LISTP VAL) (IF (EQUAL (LENGTH VAL) (QUOTE 2)) (IF (IF (NULL (CAR VAL)) (NULL (CAR VAL)) (NATP (CAR VAL))) (IF (NULL (CAR (CDR VAL))) (NULL (CAR (CDR VAL))) (NATP (CAR (CDR VAL)))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :MATCH-FREE-DEFAULT)) ((LAMBDA (X L) (RETURN-LAST (QUOTE MBE1-RAW) (MEMBER-EQ-EXEC X L) (MEMBER-EQUAL X L))) VAL (QUOTE (:ONCE :ALL NIL))) (IF (EQ KEY (QUOTE :MATCH-FREE-OVERRIDE)) (IF (EQ VAL (QUOTE :CLEAR)) (EQ VAL (QUOTE :CLEAR)) (NULL (NON-FREE-VAR-RUNES VAL (FREE-VAR-RUNES (QUOTE :ONCE) WORLD) (FREE-VAR-RUNES (QUOTE :ALL) WORLD) (QUOTE NIL)))) (IF (EQ KEY (QUOTE :MATCH-FREE-OVERRIDE-NUME)) (INTEGERP VAL) (IF (EQ KEY (QUOTE :NON-LINEARP)) (BOOLEANP VAL) (IF (EQ KEY (QUOTE :TAU-AUTO-MODEP)) (BOOLEANP VAL) (IF (EQ KEY (QUOTE :INCLUDE-BOOK-DIR-ALIST)) (IF (INCLUDE-BOOK-DIR-ALISTP VAL (OS WORLD)) (NULL ((LAMBDA (X ALIST) (RETURN-LAST (QUOTE MBE1-RAW) (ASSOC-EQ-EXEC X ALIST) (ASSOC-EQUAL X ALIST))) (QUOTE :SYSTEM) VAL)) (QUOTE NIL)) (IF (EQ KEY (QUOTE :RULER-EXTENDERS)) (IF (EQ VAL (QUOTE :ALL)) (EQ VAL (QUOTE :ALL)) ((LAMBDA (CTX ERR-STR MSG) (IF MSG (ILLEGAL CTX ERR-STR (CONS (CONS (QUOTE #\0) MSG) (QUOTE NIL))) (QUOTE T))) (QUOTE ACL2-DEFAULTS-TABLE) (QUOTE "The proposed ruler-extenders is illegal because ~@0.") (RULER-EXTENDERS-MSG VAL WORLD))) (QUOTE NIL)))))))))))))))))))))))))))))))))) (DEFMACRO SET-CCG-TIME-LIMIT (V) (CONS (QUOTE WITH-OUTPUT) (CONS (QUOTE :OFF) (CONS (QUOTE SUMMARY) (CONS (CONS (QUOTE PROGN) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ACL2-DEFAULTS-TABLE) (CONS (QUOTE :CCG-TIME-LIMIT) (CONS (CONS (QUOTE QUOTE) (CONS V (QUOTE NIL))) (QUOTE NIL))))) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ACL2-DEFAULTS-TABLE) (CONS (QUOTE :CCG-TIME-LIMIT) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL)))))))) (350 RECORD-EXPANSION (REDEFUN DEFUNS-FN (DEF-LST STATE EVENT-FORM) (CCG-DEFUNS-FN DEF-LST STATE EVENT-FORM)) (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) (CCG-DEFUNS-FN DEF-LST STATE EVENT-FORM))) (QUOTE REDEFUN) (W STATE) STATE) (ENSURE-PROGRAM-ONLY-FLAG DEFUNS-FN) (DEFUN DEFUNS-FN (DEF-LST STATE EVENT-FORM) (CCG-DEFUNS-FN DEF-LST STATE EVENT-FORM))) :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) (CCG-DEFUNS-FN DEF-LST STATE EVENT-FORM)))) (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) (CCG-DEFUNS-FN DEF-LST STATE EVENT-FORM))) (QUOTE REDEFUN) (W STATE) STATE) (ENSURE-PROGRAM-ONLY-FLAG DEFUNS-FN) (DEFUN DEFUNS-FN (DEF-LST STATE EVENT-FORM) (CCG-DEFUNS-FN DEF-LST STATE EVENT-FORM))) :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) (CCG-DEFUNS-FN DEF-LST STATE EVENT-FORM))))))) (351 RECORD-EXPANSION (PROGN+TOUCHABLE :ALL (REDEFUN+REWRITE DEFSTOBJ-FN (:CARPAT (PROCESS-EMBEDDED-EVENTS %1% %2% %3% %4% %5% (APPEND . %APP-CDR%) . %PEE-CDR%) :REPL (PROCESS-EMBEDDED-EVENTS %1% %2% %3% %4% %5% (APPEND (QUOTE ((SET-TERMINATION-METHOD :MEASURE))) . %APP-CDR%) . %PEE-CDR%) :VARS (%1% %2% %3% %4% %5% %APP-CDR% %PEE-CDR%) :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 DEFSTOBJ-FN (:CARPAT (PROCESS-EMBEDDED-EVENTS %1% %2% %3% %4% %5% (APPEND . %APP-CDR%) . %PEE-CDR%) :REPL (PROCESS-EMBEDDED-EVENTS %1% %2% %3% %4% %5% (APPEND (QUOTE ((SET-TERMINATION-METHOD :MEASURE))) . %APP-CDR%) . %PEE-CDR%) :VARS (%1% %2% %3% %4% %5% %APP-CDR% %PEE-CDR%) :MULT 1))) (PROGN (RECORD-EXPANSION (REDEFUN+REWRITE DEFSTOBJ-FN (:CARPAT (PROCESS-EMBEDDED-EVENTS %1% %2% %3% %4% %5% (APPEND . %APP-CDR%) . %PEE-CDR%) :REPL (PROCESS-EMBEDDED-EVENTS %1% %2% %3% %4% %5% (APPEND (QUOTE ((SET-TERMINATION-METHOD :MEASURE))) . %APP-CDR%) . %PEE-CDR%) :VARS (%1% %2% %3% %4% %5% %APP-CDR% %PEE-CDR%) :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 DEFSTOBJ-FN) (DEFCODE :LOOP (ER-PROGN (ASSERT-NO-SPECIAL-RAW-DEFINITION DEFSTOBJ-FN) (CHK-ACCEPTABLE-REDEFUN (QUOTE (DEFSTOBJ-FN (NAME ARGS STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM (MSG "( DEFSTOBJ ~x0 ...)" NAME)) (LET ((EVENT-FORM (OR EVENT-FORM (LIST* (QUOTE DEFSTOBJ) NAME ARGS))) (WRLD0 (W STATE))) (ER-LET* ((WRLD1 (CHK-ACCEPTABLE-DEFSTOBJ NAME ARGS CTX WRLD0 STATE))) (COND ((EQ WRLD1 (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD0 (LET* ((TEMPLATE (DEFSTOBJ-TEMPLATE NAME ARGS WRLD1)) (FIELD-NAMES (STRIP-ACCESSOR-NAMES (CADDR TEMPLATE))) (DEFCONSTS (DEFSTOBJ-DEFCONSTS FIELD-NAMES 0)) (FIELD-CONST-NAMES (STRIP-CADRS DEFCONSTS)) (AX-DEF-LST (DEFSTOBJ-AXIOMATIC-DEFS NAME TEMPLATE WRLD1)) (RAW-DEF-LST (DEFSTOBJ-RAW-DEFS NAME TEMPLATE NIL WRLD1)) (RECOG-NAME (CAR TEMPLATE)) (CREATOR-NAME (CADR TEMPLATE)) (NAMES (STRIP-CARS AX-DEF-LST)) (THE-LIVE-VAR (THE-LIVE-VAR NAME)) (DOC (FOURTH TEMPLATE)) (CONGRUENT-TO (SIXTH TEMPLATE))) (ER-PROGN (COND ((SET-EQUALP-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (VALUE NIL)) (T (VALUE (ER HARD CTX "Defstobj-axiomatic-defs and defstobj-raw-defs are ~
                            out of sync!  They should each define the same set ~
                            of names.  Here are the functions with axiomatic ~
                            defs that have no raw defs:  ~x0.  And here are ~
                            the with raw defs but no axiomatic ones:  ~x1." (SET-DIFFERENCE-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (SET-DIFFERENCE-EQUAL (STRIP-CARS RAW-DEF-LST) NAMES))))) (REVERT-WORLD-ON-ERROR (PPROGN (SET-W (QUOTE EXTENSION) WRLD1 STATE) (ER-PROGN (PROCESS-EMBEDDED-EVENTS (QUOTE DEFSTOBJ) (TABLE-ALIST (QUOTE ACL2-DEFAULTS-TABLE) WRLD1) (OR (LD-SKIP-PROOFSP STATE) T) (CURRENT-PACKAGE STATE) (LIST (QUOTE DEFSTOBJ) NAME NAMES) (APPEND (QUOTE ((SET-TERMINATION-METHOD :MEASURE))) (PAIRLIS-X1 (QUOTE DEFUN) AX-DEF-LST) DEFCONSTS (CONS (CONS (QUOTE ENCAPSULATE) (CONS (QUOTE NIL) (CONS (CONS (QUOTE SET-INHIBIT-WARNINGS) (CONS (QUOTE "theory") (QUOTE NIL))) (CONS (CONS (QUOTE IN-THEORY) (CONS (CONS (QUOTE DISABLE) (CONS (CONS (QUOTE :EXECUTABLE-COUNTERPART) (CONS CREATOR-NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))))) (QUOTE NIL))) 0 T CTX STATE) (ER-LET* ((DOC-PAIR (TRANSLATE-DOC NAME DOC CTX STATE))) (LET* ((WRLD2 (W STATE)) (WRLD3 (UPDATE-DOC-DATABASE NAME DOC DOC-PAIR (PUTPROP NAME (QUOTE CONGRUENT-STOBJ-REP) (AND CONGRUENT-TO (CONGRUENT-STOBJ-REP CONGRUENT-TO WRLD2)) (PUTPROP NAME (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUT-STOBJS-IN-AND-OUTS NAME TEMPLATE (PUTPROP NAME (QUOTE STOBJ) (CONS THE-LIVE-VAR (LIST* RECOG-NAME CREATOR-NAME (APPEND (REMOVE1-EQ CREATOR-NAME (REMOVE1-EQ RECOG-NAME NAMES)) FIELD-CONST-NAMES))) (PUTPROP-X-LST1 NAMES (QUOTE STOBJ-FUNCTION) NAME (PUTPROP-X-LST1 FIELD-CONST-NAMES (QUOTE STOBJ-CONSTANT) NAME (PUTPROP THE-LIVE-VAR (QUOTE STOBJ-LIVE-VAR) NAME (PUTPROP THE-LIVE-VAR (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUTPROP NAME (QUOTE ACCESSOR-NAMES) (ACCESSOR-ARRAY NAME FIELD-NAMES) WRLD2)))))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE DEFSTOBJ) (LIST* NAME THE-LIVE-VAR NAMES) NIL (CONS (QUOTE DEFSTOBJ) (CONS NAME (CONS THE-LIVE-VAR (CONS (DEFSTOBJ-RAW-INIT TEMPLATE) (CONS RAW-DEF-LST (CONS TEMPLATE (CONS AX-DEF-LST (QUOTE NIL)))))))) T CTX WRLD3 STATE)))))))))))))))) (QUOTE REDEFUN) (W STATE) STATE) (ENSURE-PROGRAM-ONLY-FLAG DEFSTOBJ-FN) (DEFUN DEFSTOBJ-FN (NAME ARGS STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM (MSG "( DEFSTOBJ ~x0 ...)" NAME)) (LET ((EVENT-FORM (OR EVENT-FORM (LIST* (QUOTE DEFSTOBJ) NAME ARGS))) (WRLD0 (W STATE))) (ER-LET* ((WRLD1 (CHK-ACCEPTABLE-DEFSTOBJ NAME ARGS CTX WRLD0 STATE))) (COND ((EQ WRLD1 (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD0 (LET* ((TEMPLATE (DEFSTOBJ-TEMPLATE NAME ARGS WRLD1)) (FIELD-NAMES (STRIP-ACCESSOR-NAMES (CADDR TEMPLATE))) (DEFCONSTS (DEFSTOBJ-DEFCONSTS FIELD-NAMES 0)) (FIELD-CONST-NAMES (STRIP-CADRS DEFCONSTS)) (AX-DEF-LST (DEFSTOBJ-AXIOMATIC-DEFS NAME TEMPLATE WRLD1)) (RAW-DEF-LST (DEFSTOBJ-RAW-DEFS NAME TEMPLATE NIL WRLD1)) (RECOG-NAME (CAR TEMPLATE)) (CREATOR-NAME (CADR TEMPLATE)) (NAMES (STRIP-CARS AX-DEF-LST)) (THE-LIVE-VAR (THE-LIVE-VAR NAME)) (DOC (FOURTH TEMPLATE)) (CONGRUENT-TO (SIXTH TEMPLATE))) (ER-PROGN (COND ((SET-EQUALP-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (VALUE NIL)) (T (VALUE (ER HARD CTX "Defstobj-axiomatic-defs and defstobj-raw-defs are ~
                            out of sync!  They should each define the same set ~
                            of names.  Here are the functions with axiomatic ~
                            defs that have no raw defs:  ~x0.  And here are ~
                            the with raw defs but no axiomatic ones:  ~x1." (SET-DIFFERENCE-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (SET-DIFFERENCE-EQUAL (STRIP-CARS RAW-DEF-LST) NAMES))))) (REVERT-WORLD-ON-ERROR (PPROGN (SET-W (QUOTE EXTENSION) WRLD1 STATE) (ER-PROGN (PROCESS-EMBEDDED-EVENTS (QUOTE DEFSTOBJ) (TABLE-ALIST (QUOTE ACL2-DEFAULTS-TABLE) WRLD1) (OR (LD-SKIP-PROOFSP STATE) T) (CURRENT-PACKAGE STATE) (LIST (QUOTE DEFSTOBJ) NAME NAMES) (APPEND (QUOTE ((SET-TERMINATION-METHOD :MEASURE))) (PAIRLIS-X1 (QUOTE DEFUN) AX-DEF-LST) DEFCONSTS (CONS (CONS (QUOTE ENCAPSULATE) (CONS (QUOTE NIL) (CONS (CONS (QUOTE SET-INHIBIT-WARNINGS) (CONS (QUOTE "theory") (QUOTE NIL))) (CONS (CONS (QUOTE IN-THEORY) (CONS (CONS (QUOTE DISABLE) (CONS (CONS (QUOTE :EXECUTABLE-COUNTERPART) (CONS CREATOR-NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))))) (QUOTE NIL))) 0 T CTX STATE) (ER-LET* ((DOC-PAIR (TRANSLATE-DOC NAME DOC CTX STATE))) (LET* ((WRLD2 (W STATE)) (WRLD3 (UPDATE-DOC-DATABASE NAME DOC DOC-PAIR (PUTPROP NAME (QUOTE CONGRUENT-STOBJ-REP) (AND CONGRUENT-TO (CONGRUENT-STOBJ-REP CONGRUENT-TO WRLD2)) (PUTPROP NAME (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUT-STOBJS-IN-AND-OUTS NAME TEMPLATE (PUTPROP NAME (QUOTE STOBJ) (CONS THE-LIVE-VAR (LIST* RECOG-NAME CREATOR-NAME (APPEND (REMOVE1-EQ CREATOR-NAME (REMOVE1-EQ RECOG-NAME NAMES)) FIELD-CONST-NAMES))) (PUTPROP-X-LST1 NAMES (QUOTE STOBJ-FUNCTION) NAME (PUTPROP-X-LST1 FIELD-CONST-NAMES (QUOTE STOBJ-CONSTANT) NAME (PUTPROP THE-LIVE-VAR (QUOTE STOBJ-LIVE-VAR) NAME (PUTPROP THE-LIVE-VAR (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUTPROP NAME (QUOTE ACCESSOR-NAMES) (ACCESSOR-ARRAY NAME FIELD-NAMES) WRLD2)))))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE DEFSTOBJ) (LIST* NAME THE-LIVE-VAR NAMES) NIL (CONS (QUOTE DEFSTOBJ) (CONS NAME (CONS THE-LIVE-VAR (CONS (DEFSTOBJ-RAW-INIT TEMPLATE) (CONS RAW-DEF-LST (CONS TEMPLATE (CONS AX-DEF-LST (QUOTE NIL)))))))) T CTX WRLD3 STATE)))))))))))))))) :EXTEND (IN-RAW-MODE (DEFUN-*1* DEFSTOBJ-FN (NAME ARGS STATE EVENT-FORM) (IF (F-GET-GLOBAL (QUOTE SAFE-MODE) *THE-LIVE-STATE*) (THROW-RAW-EV-FNCALL (LIST (QUOTE PROGRAM-ONLY-ER) (QUOTE DEFSTOBJ-FN) (LIST NAME ARGS STATE EVENT-FORM) (QUOTE T) (QUOTE (NIL)) T)) (DEFSTOBJ-FN NAME ARGS STATE EVENT-FORM)))) :COMPILE (DEFUN DEFSTOBJ-FN (NAME ARGS STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM (MSG "( DEFSTOBJ ~x0 ...)" NAME)) (LET ((EVENT-FORM (OR EVENT-FORM (LIST* (QUOTE DEFSTOBJ) NAME ARGS))) (WRLD0 (W STATE))) (ER-LET* ((WRLD1 (CHK-ACCEPTABLE-DEFSTOBJ NAME ARGS CTX WRLD0 STATE))) (COND ((EQ WRLD1 (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD0 (LET* ((TEMPLATE (DEFSTOBJ-TEMPLATE NAME ARGS WRLD1)) (FIELD-NAMES (STRIP-ACCESSOR-NAMES (CADDR TEMPLATE))) (DEFCONSTS (DEFSTOBJ-DEFCONSTS FIELD-NAMES 0)) (FIELD-CONST-NAMES (STRIP-CADRS DEFCONSTS)) (AX-DEF-LST (DEFSTOBJ-AXIOMATIC-DEFS NAME TEMPLATE WRLD1)) (RAW-DEF-LST (DEFSTOBJ-RAW-DEFS NAME TEMPLATE NIL WRLD1)) (RECOG-NAME (CAR TEMPLATE)) (CREATOR-NAME (CADR TEMPLATE)) (NAMES (STRIP-CARS AX-DEF-LST)) (THE-LIVE-VAR (THE-LIVE-VAR NAME)) (DOC (FOURTH TEMPLATE)) (CONGRUENT-TO (SIXTH TEMPLATE))) (ER-PROGN (COND ((SET-EQUALP-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (VALUE NIL)) (T (VALUE (ER HARD CTX "Defstobj-axiomatic-defs and defstobj-raw-defs are ~
                            out of sync!  They should each define the same set ~
                            of names.  Here are the functions with axiomatic ~
                            defs that have no raw defs:  ~x0.  And here are ~
                            the with raw defs but no axiomatic ones:  ~x1." (SET-DIFFERENCE-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (SET-DIFFERENCE-EQUAL (STRIP-CARS RAW-DEF-LST) NAMES))))) (REVERT-WORLD-ON-ERROR (PPROGN (SET-W (QUOTE EXTENSION) WRLD1 STATE) (ER-PROGN (PROCESS-EMBEDDED-EVENTS (QUOTE DEFSTOBJ) (TABLE-ALIST (QUOTE ACL2-DEFAULTS-TABLE) WRLD1) (OR (LD-SKIP-PROOFSP STATE) T) (CURRENT-PACKAGE STATE) (LIST (QUOTE DEFSTOBJ) NAME NAMES) (APPEND (QUOTE ((SET-TERMINATION-METHOD :MEASURE))) (PAIRLIS-X1 (QUOTE DEFUN) AX-DEF-LST) DEFCONSTS (CONS (CONS (QUOTE ENCAPSULATE) (CONS (QUOTE NIL) (CONS (CONS (QUOTE SET-INHIBIT-WARNINGS) (CONS (QUOTE "theory") (QUOTE NIL))) (CONS (CONS (QUOTE IN-THEORY) (CONS (CONS (QUOTE DISABLE) (CONS (CONS (QUOTE :EXECUTABLE-COUNTERPART) (CONS CREATOR-NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))))) (QUOTE NIL))) 0 T CTX STATE) (ER-LET* ((DOC-PAIR (TRANSLATE-DOC NAME DOC CTX STATE))) (LET* ((WRLD2 (W STATE)) (WRLD3 (UPDATE-DOC-DATABASE NAME DOC DOC-PAIR (PUTPROP NAME (QUOTE CONGRUENT-STOBJ-REP) (AND CONGRUENT-TO (CONGRUENT-STOBJ-REP CONGRUENT-TO WRLD2)) (PUTPROP NAME (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUT-STOBJS-IN-AND-OUTS NAME TEMPLATE (PUTPROP NAME (QUOTE STOBJ) (CONS THE-LIVE-VAR (LIST* RECOG-NAME CREATOR-NAME (APPEND (REMOVE1-EQ CREATOR-NAME (REMOVE1-EQ RECOG-NAME NAMES)) FIELD-CONST-NAMES))) (PUTPROP-X-LST1 NAMES (QUOTE STOBJ-FUNCTION) NAME (PUTPROP-X-LST1 FIELD-CONST-NAMES (QUOTE STOBJ-CONSTANT) NAME (PUTPROP THE-LIVE-VAR (QUOTE STOBJ-LIVE-VAR) NAME (PUTPROP THE-LIVE-VAR (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUTPROP NAME (QUOTE ACCESSOR-NAMES) (ACCESSOR-ARRAY NAME FIELD-NAMES) WRLD2)))))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE DEFSTOBJ) (LIST* NAME THE-LIVE-VAR NAMES) NIL (CONS (QUOTE DEFSTOBJ) (CONS NAME (CONS THE-LIVE-VAR (CONS (DEFSTOBJ-RAW-INIT TEMPLATE) (CONS RAW-DEF-LST (CONS TEMPLATE (CONS AX-DEF-LST (QUOTE NIL)))))))) T CTX WRLD3 STATE))))))))))))))))) (PROGN (RECORD-EXPANSION (ASSERT-INCLUDE-DEFUN-MATCHES-CERTIFY-DEFUN DEFSTOBJ-FN) (VALUE-TRIPLE (LET ((REWRITE-CODE::CERTIFY-TIME-DEFUN (QUOTE (DEFUN DEFSTOBJ-FN (NAME ARGS STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM (MSG "( DEFSTOBJ ~x0 ...)" NAME)) (LET ((EVENT-FORM (OR EVENT-FORM (LIST* (QUOTE DEFSTOBJ) NAME ARGS))) (WRLD0 (W STATE))) (ER-LET* ((WRLD1 (CHK-ACCEPTABLE-DEFSTOBJ NAME ARGS CTX WRLD0 STATE))) (COND ((EQ WRLD1 (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD0 (LET* ((TEMPLATE (DEFSTOBJ-TEMPLATE NAME ARGS WRLD1)) (FIELD-NAMES (STRIP-ACCESSOR-NAMES (CADDR TEMPLATE))) (DEFCONSTS (DEFSTOBJ-DEFCONSTS FIELD-NAMES 0)) (FIELD-CONST-NAMES (STRIP-CADRS DEFCONSTS)) (AX-DEF-LST (DEFSTOBJ-AXIOMATIC-DEFS NAME TEMPLATE WRLD1)) (RAW-DEF-LST (DEFSTOBJ-RAW-DEFS NAME TEMPLATE NIL WRLD1)) (RECOG-NAME (CAR TEMPLATE)) (CREATOR-NAME (CADR TEMPLATE)) (NAMES (STRIP-CARS AX-DEF-LST)) (THE-LIVE-VAR (THE-LIVE-VAR NAME)) (DOC (FOURTH TEMPLATE)) (CONGRUENT-TO (SIXTH TEMPLATE))) (ER-PROGN (COND ((SET-EQUALP-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (VALUE NIL)) (T (VALUE (ER HARD CTX "Defstobj-axiomatic-defs and defstobj-raw-defs are ~
                            out of sync!  They should each define the same set ~
                            of names.  Here are the functions with axiomatic ~
                            defs that have no raw defs:  ~x0.  And here are ~
                            the with raw defs but no axiomatic ones:  ~x1." (SET-DIFFERENCE-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (SET-DIFFERENCE-EQUAL (STRIP-CARS RAW-DEF-LST) NAMES))))) (REVERT-WORLD-ON-ERROR (PPROGN (SET-W (QUOTE EXTENSION) WRLD1 STATE) (ER-PROGN (PROCESS-EMBEDDED-EVENTS (QUOTE DEFSTOBJ) (TABLE-ALIST (QUOTE ACL2-DEFAULTS-TABLE) WRLD1) (OR (LD-SKIP-PROOFSP STATE) T) (CURRENT-PACKAGE STATE) (LIST (QUOTE DEFSTOBJ) NAME NAMES) (APPEND (PAIRLIS-X1 (QUOTE DEFUN) AX-DEF-LST) DEFCONSTS (CONS (CONS (QUOTE ENCAPSULATE) (CONS (QUOTE NIL) (CONS (CONS (QUOTE SET-INHIBIT-WARNINGS) (CONS (QUOTE "theory") (QUOTE NIL))) (CONS (CONS (QUOTE IN-THEORY) (CONS (CONS (QUOTE DISABLE) (CONS (CONS (QUOTE :EXECUTABLE-COUNTERPART) (CONS CREATOR-NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))))) (QUOTE NIL))) 0 T CTX STATE) (ER-LET* ((DOC-PAIR (TRANSLATE-DOC NAME DOC CTX STATE))) (LET* ((WRLD2 (W STATE)) (WRLD3 (UPDATE-DOC-DATABASE NAME DOC DOC-PAIR (PUTPROP NAME (QUOTE CONGRUENT-STOBJ-REP) (AND CONGRUENT-TO (CONGRUENT-STOBJ-REP CONGRUENT-TO WRLD2)) (PUTPROP NAME (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUT-STOBJS-IN-AND-OUTS NAME TEMPLATE (PUTPROP NAME (QUOTE STOBJ) (CONS THE-LIVE-VAR (LIST* RECOG-NAME CREATOR-NAME (APPEND (REMOVE1-EQ CREATOR-NAME (REMOVE1-EQ RECOG-NAME NAMES)) FIELD-CONST-NAMES))) (PUTPROP-X-LST1 NAMES (QUOTE STOBJ-FUNCTION) NAME (PUTPROP-X-LST1 FIELD-CONST-NAMES (QUOTE STOBJ-CONSTANT) NAME (PUTPROP THE-LIVE-VAR (QUOTE STOBJ-LIVE-VAR) NAME (PUTPROP THE-LIVE-VAR (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUTPROP NAME (QUOTE ACCESSOR-NAMES) (ACCESSOR-ARRAY NAME FIELD-NAMES) WRLD2)))))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE DEFSTOBJ) (LIST* NAME THE-LIVE-VAR NAMES) NIL (CONS (QUOTE DEFSTOBJ) (CONS NAME (CONS THE-LIVE-VAR (CONS (DEFSTOBJ-RAW-INIT TEMPLATE) (CONS RAW-DEF-LST (CONS TEMPLATE (CONS AX-DEF-LST (QUOTE NIL)))))))) T CTX WRLD3 STATE))))))))))))))))) (REWRITE-CODE::INCLUDE-TIME-DEFUN (GET-DEFUN (QUOTE DEFSTOBJ-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 DEFSTOBJ-FN) (CHK-ACCEPTABLE-REDEFUN (QUOTE (DEFSTOBJ-FN (NAME ARGS STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM (MSG "( DEFSTOBJ ~x0 ...)" NAME)) (LET ((EVENT-FORM (OR EVENT-FORM (LIST* (QUOTE DEFSTOBJ) NAME ARGS))) (WRLD0 (W STATE))) (ER-LET* ((WRLD1 (CHK-ACCEPTABLE-DEFSTOBJ NAME ARGS CTX WRLD0 STATE))) (COND ((EQ WRLD1 (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD0 (LET* ((TEMPLATE (DEFSTOBJ-TEMPLATE NAME ARGS WRLD1)) (FIELD-NAMES (STRIP-ACCESSOR-NAMES (CADDR TEMPLATE))) (DEFCONSTS (DEFSTOBJ-DEFCONSTS FIELD-NAMES 0)) (FIELD-CONST-NAMES (STRIP-CADRS DEFCONSTS)) (AX-DEF-LST (DEFSTOBJ-AXIOMATIC-DEFS NAME TEMPLATE WRLD1)) (RAW-DEF-LST (DEFSTOBJ-RAW-DEFS NAME TEMPLATE NIL WRLD1)) (RECOG-NAME (CAR TEMPLATE)) (CREATOR-NAME (CADR TEMPLATE)) (NAMES (STRIP-CARS AX-DEF-LST)) (THE-LIVE-VAR (THE-LIVE-VAR NAME)) (DOC (FOURTH TEMPLATE)) (CONGRUENT-TO (SIXTH TEMPLATE))) (ER-PROGN (COND ((SET-EQUALP-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (VALUE NIL)) (T (VALUE (ER HARD CTX "Defstobj-axiomatic-defs and defstobj-raw-defs are ~
                            out of sync!  They should each define the same set ~
                            of names.  Here are the functions with axiomatic ~
                            defs that have no raw defs:  ~x0.  And here are ~
                            the with raw defs but no axiomatic ones:  ~x1." (SET-DIFFERENCE-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (SET-DIFFERENCE-EQUAL (STRIP-CARS RAW-DEF-LST) NAMES))))) (REVERT-WORLD-ON-ERROR (PPROGN (SET-W (QUOTE EXTENSION) WRLD1 STATE) (ER-PROGN (PROCESS-EMBEDDED-EVENTS (QUOTE DEFSTOBJ) (TABLE-ALIST (QUOTE ACL2-DEFAULTS-TABLE) WRLD1) (OR (LD-SKIP-PROOFSP STATE) T) (CURRENT-PACKAGE STATE) (LIST (QUOTE DEFSTOBJ) NAME NAMES) (APPEND (QUOTE ((SET-TERMINATION-METHOD :MEASURE))) (PAIRLIS-X1 (QUOTE DEFUN) AX-DEF-LST) DEFCONSTS (CONS (CONS (QUOTE ENCAPSULATE) (CONS (QUOTE NIL) (CONS (CONS (QUOTE SET-INHIBIT-WARNINGS) (CONS (QUOTE "theory") (QUOTE NIL))) (CONS (CONS (QUOTE IN-THEORY) (CONS (CONS (QUOTE DISABLE) (CONS (CONS (QUOTE :EXECUTABLE-COUNTERPART) (CONS CREATOR-NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))))) (QUOTE NIL))) 0 T CTX STATE) (ER-LET* ((DOC-PAIR (TRANSLATE-DOC NAME DOC CTX STATE))) (LET* ((WRLD2 (W STATE)) (WRLD3 (UPDATE-DOC-DATABASE NAME DOC DOC-PAIR (PUTPROP NAME (QUOTE CONGRUENT-STOBJ-REP) (AND CONGRUENT-TO (CONGRUENT-STOBJ-REP CONGRUENT-TO WRLD2)) (PUTPROP NAME (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUT-STOBJS-IN-AND-OUTS NAME TEMPLATE (PUTPROP NAME (QUOTE STOBJ) (CONS THE-LIVE-VAR (LIST* RECOG-NAME CREATOR-NAME (APPEND (REMOVE1-EQ CREATOR-NAME (REMOVE1-EQ RECOG-NAME NAMES)) FIELD-CONST-NAMES))) (PUTPROP-X-LST1 NAMES (QUOTE STOBJ-FUNCTION) NAME (PUTPROP-X-LST1 FIELD-CONST-NAMES (QUOTE STOBJ-CONSTANT) NAME (PUTPROP THE-LIVE-VAR (QUOTE STOBJ-LIVE-VAR) NAME (PUTPROP THE-LIVE-VAR (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUTPROP NAME (QUOTE ACCESSOR-NAMES) (ACCESSOR-ARRAY NAME FIELD-NAMES) WRLD2)))))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE DEFSTOBJ) (LIST* NAME THE-LIVE-VAR NAMES) NIL (CONS (QUOTE DEFSTOBJ) (CONS NAME (CONS THE-LIVE-VAR (CONS (DEFSTOBJ-RAW-INIT TEMPLATE) (CONS RAW-DEF-LST (CONS TEMPLATE (CONS AX-DEF-LST (QUOTE NIL)))))))) T CTX WRLD3 STATE)))))))))))))))) (QUOTE REDEFUN) (W STATE) STATE) (ENSURE-PROGRAM-ONLY-FLAG DEFSTOBJ-FN) (DEFUN DEFSTOBJ-FN (NAME ARGS STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM (MSG "( DEFSTOBJ ~x0 ...)" NAME)) (LET ((EVENT-FORM (OR EVENT-FORM (LIST* (QUOTE DEFSTOBJ) NAME ARGS))) (WRLD0 (W STATE))) (ER-LET* ((WRLD1 (CHK-ACCEPTABLE-DEFSTOBJ NAME ARGS CTX WRLD0 STATE))) (COND ((EQ WRLD1 (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD0 (LET* ((TEMPLATE (DEFSTOBJ-TEMPLATE NAME ARGS WRLD1)) (FIELD-NAMES (STRIP-ACCESSOR-NAMES (CADDR TEMPLATE))) (DEFCONSTS (DEFSTOBJ-DEFCONSTS FIELD-NAMES 0)) (FIELD-CONST-NAMES (STRIP-CADRS DEFCONSTS)) (AX-DEF-LST (DEFSTOBJ-AXIOMATIC-DEFS NAME TEMPLATE WRLD1)) (RAW-DEF-LST (DEFSTOBJ-RAW-DEFS NAME TEMPLATE NIL WRLD1)) (RECOG-NAME (CAR TEMPLATE)) (CREATOR-NAME (CADR TEMPLATE)) (NAMES (STRIP-CARS AX-DEF-LST)) (THE-LIVE-VAR (THE-LIVE-VAR NAME)) (DOC (FOURTH TEMPLATE)) (CONGRUENT-TO (SIXTH TEMPLATE))) (ER-PROGN (COND ((SET-EQUALP-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (VALUE NIL)) (T (VALUE (ER HARD CTX "Defstobj-axiomatic-defs and defstobj-raw-defs are ~
                            out of sync!  They should each define the same set ~
                            of names.  Here are the functions with axiomatic ~
                            defs that have no raw defs:  ~x0.  And here are ~
                            the with raw defs but no axiomatic ones:  ~x1." (SET-DIFFERENCE-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (SET-DIFFERENCE-EQUAL (STRIP-CARS RAW-DEF-LST) NAMES))))) (REVERT-WORLD-ON-ERROR (PPROGN (SET-W (QUOTE EXTENSION) WRLD1 STATE) (ER-PROGN (PROCESS-EMBEDDED-EVENTS (QUOTE DEFSTOBJ) (TABLE-ALIST (QUOTE ACL2-DEFAULTS-TABLE) WRLD1) (OR (LD-SKIP-PROOFSP STATE) T) (CURRENT-PACKAGE STATE) (LIST (QUOTE DEFSTOBJ) NAME NAMES) (APPEND (QUOTE ((SET-TERMINATION-METHOD :MEASURE))) (PAIRLIS-X1 (QUOTE DEFUN) AX-DEF-LST) DEFCONSTS (CONS (CONS (QUOTE ENCAPSULATE) (CONS (QUOTE NIL) (CONS (CONS (QUOTE SET-INHIBIT-WARNINGS) (CONS (QUOTE "theory") (QUOTE NIL))) (CONS (CONS (QUOTE IN-THEORY) (CONS (CONS (QUOTE DISABLE) (CONS (CONS (QUOTE :EXECUTABLE-COUNTERPART) (CONS CREATOR-NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))))) (QUOTE NIL))) 0 T CTX STATE) (ER-LET* ((DOC-PAIR (TRANSLATE-DOC NAME DOC CTX STATE))) (LET* ((WRLD2 (W STATE)) (WRLD3 (UPDATE-DOC-DATABASE NAME DOC DOC-PAIR (PUTPROP NAME (QUOTE CONGRUENT-STOBJ-REP) (AND CONGRUENT-TO (CONGRUENT-STOBJ-REP CONGRUENT-TO WRLD2)) (PUTPROP NAME (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUT-STOBJS-IN-AND-OUTS NAME TEMPLATE (PUTPROP NAME (QUOTE STOBJ) (CONS THE-LIVE-VAR (LIST* RECOG-NAME CREATOR-NAME (APPEND (REMOVE1-EQ CREATOR-NAME (REMOVE1-EQ RECOG-NAME NAMES)) FIELD-CONST-NAMES))) (PUTPROP-X-LST1 NAMES (QUOTE STOBJ-FUNCTION) NAME (PUTPROP-X-LST1 FIELD-CONST-NAMES (QUOTE STOBJ-CONSTANT) NAME (PUTPROP THE-LIVE-VAR (QUOTE STOBJ-LIVE-VAR) NAME (PUTPROP THE-LIVE-VAR (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUTPROP NAME (QUOTE ACCESSOR-NAMES) (ACCESSOR-ARRAY NAME FIELD-NAMES) WRLD2)))))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE DEFSTOBJ) (LIST* NAME THE-LIVE-VAR NAMES) NIL (CONS (QUOTE DEFSTOBJ) (CONS NAME (CONS THE-LIVE-VAR (CONS (DEFSTOBJ-RAW-INIT TEMPLATE) (CONS RAW-DEF-LST (CONS TEMPLATE (CONS AX-DEF-LST (QUOTE NIL)))))))) T CTX WRLD3 STATE)))))))))))))))) :EXTEND (IN-RAW-MODE (DEFUN-*1* DEFSTOBJ-FN (NAME ARGS STATE EVENT-FORM) (IF (F-GET-GLOBAL (QUOTE SAFE-MODE) *THE-LIVE-STATE*) (THROW-RAW-EV-FNCALL (LIST (QUOTE PROGRAM-ONLY-ER) (QUOTE DEFSTOBJ-FN) (LIST NAME ARGS STATE EVENT-FORM) (QUOTE T) (QUOTE (NIL)) T)) (DEFSTOBJ-FN NAME ARGS STATE EVENT-FORM)))) :COMPILE (DEFUN DEFSTOBJ-FN (NAME ARGS STATE EVENT-FORM) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (STATE))) (WITH-CTX-SUMMARIZED (IF (OUTPUT-IN-INFIXP STATE) EVENT-FORM (MSG "( DEFSTOBJ ~x0 ...)" NAME)) (LET ((EVENT-FORM (OR EVENT-FORM (LIST* (QUOTE DEFSTOBJ) NAME ARGS))) (WRLD0 (W STATE))) (ER-LET* ((WRLD1 (CHK-ACCEPTABLE-DEFSTOBJ NAME ARGS CTX WRLD0 STATE))) (COND ((EQ WRLD1 (QUOTE REDUNDANT)) (STOP-REDUNDANT-EVENT CTX STATE)) (T (ENFORCE-REDUNDANCY EVENT-FORM CTX WRLD0 (LET* ((TEMPLATE (DEFSTOBJ-TEMPLATE NAME ARGS WRLD1)) (FIELD-NAMES (STRIP-ACCESSOR-NAMES (CADDR TEMPLATE))) (DEFCONSTS (DEFSTOBJ-DEFCONSTS FIELD-NAMES 0)) (FIELD-CONST-NAMES (STRIP-CADRS DEFCONSTS)) (AX-DEF-LST (DEFSTOBJ-AXIOMATIC-DEFS NAME TEMPLATE WRLD1)) (RAW-DEF-LST (DEFSTOBJ-RAW-DEFS NAME TEMPLATE NIL WRLD1)) (RECOG-NAME (CAR TEMPLATE)) (CREATOR-NAME (CADR TEMPLATE)) (NAMES (STRIP-CARS AX-DEF-LST)) (THE-LIVE-VAR (THE-LIVE-VAR NAME)) (DOC (FOURTH TEMPLATE)) (CONGRUENT-TO (SIXTH TEMPLATE))) (ER-PROGN (COND ((SET-EQUALP-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (VALUE NIL)) (T (VALUE (ER HARD CTX "Defstobj-axiomatic-defs and defstobj-raw-defs are ~
                            out of sync!  They should each define the same set ~
                            of names.  Here are the functions with axiomatic ~
                            defs that have no raw defs:  ~x0.  And here are ~
                            the with raw defs but no axiomatic ones:  ~x1." (SET-DIFFERENCE-EQUAL NAMES (STRIP-CARS RAW-DEF-LST)) (SET-DIFFERENCE-EQUAL (STRIP-CARS RAW-DEF-LST) NAMES))))) (REVERT-WORLD-ON-ERROR (PPROGN (SET-W (QUOTE EXTENSION) WRLD1 STATE) (ER-PROGN (PROCESS-EMBEDDED-EVENTS (QUOTE DEFSTOBJ) (TABLE-ALIST (QUOTE ACL2-DEFAULTS-TABLE) WRLD1) (OR (LD-SKIP-PROOFSP STATE) T) (CURRENT-PACKAGE STATE) (LIST (QUOTE DEFSTOBJ) NAME NAMES) (APPEND (QUOTE ((SET-TERMINATION-METHOD :MEASURE))) (PAIRLIS-X1 (QUOTE DEFUN) AX-DEF-LST) DEFCONSTS (CONS (CONS (QUOTE ENCAPSULATE) (CONS (QUOTE NIL) (CONS (CONS (QUOTE SET-INHIBIT-WARNINGS) (CONS (QUOTE "theory") (QUOTE NIL))) (CONS (CONS (QUOTE IN-THEORY) (CONS (CONS (QUOTE DISABLE) (CONS (CONS (QUOTE :EXECUTABLE-COUNTERPART) (CONS CREATOR-NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))))) (QUOTE NIL))) 0 T CTX STATE) (ER-LET* ((DOC-PAIR (TRANSLATE-DOC NAME DOC CTX STATE))) (LET* ((WRLD2 (W STATE)) (WRLD3 (UPDATE-DOC-DATABASE NAME DOC DOC-PAIR (PUTPROP NAME (QUOTE CONGRUENT-STOBJ-REP) (AND CONGRUENT-TO (CONGRUENT-STOBJ-REP CONGRUENT-TO WRLD2)) (PUTPROP NAME (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUT-STOBJS-IN-AND-OUTS NAME TEMPLATE (PUTPROP NAME (QUOTE STOBJ) (CONS THE-LIVE-VAR (LIST* RECOG-NAME CREATOR-NAME (APPEND (REMOVE1-EQ CREATOR-NAME (REMOVE1-EQ RECOG-NAME NAMES)) FIELD-CONST-NAMES))) (PUTPROP-X-LST1 NAMES (QUOTE STOBJ-FUNCTION) NAME (PUTPROP-X-LST1 FIELD-CONST-NAMES (QUOTE STOBJ-CONSTANT) NAME (PUTPROP THE-LIVE-VAR (QUOTE STOBJ-LIVE-VAR) NAME (PUTPROP THE-LIVE-VAR (QUOTE SYMBOL-CLASS) :COMMON-LISP-COMPLIANT (PUTPROP NAME (QUOTE ACCESSOR-NAMES) (ACCESSOR-ARRAY NAME FIELD-NAMES) WRLD2)))))))))))) (INSTALL-EVENT NAME EVENT-FORM (QUOTE DEFSTOBJ) (LIST* NAME THE-LIVE-VAR NAMES) NIL (CONS (QUOTE DEFSTOBJ) (CONS NAME (CONS THE-LIVE-VAR (CONS (DEFSTOBJ-RAW-INIT TEMPLATE) (CONS RAW-DEF-LST (CONS TEMPLATE (CONS AX-DEF-LST (QUOTE NIL)))))))) T CTX WRLD3 STATE)))))))))))))))))))))))))
NIL
(("/usr/share/acl2-6.3/books/ccg/ccg.lisp" "ccg" "ccg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:CCG "/usr/share/acl2-6.3/books/ccg/ccg.lisp"))) . 313094761) ("/usr/share/acl2-6.3/books/hacking/all.lisp" "hacking/all" "all" ((: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"))) . 247444498) ("/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/subsumption.lisp" "subsumption" "subsumption" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 560393729) ("/usr/share/acl2-6.3/books/hacking/bridge.lisp" "bridge" "bridge" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 690072471) ("/usr/share/acl2-6.3/books/hacking/redefun.lisp" "redefun" "redefun" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 198064993) ("/usr/share/acl2-6.3/books/hacking/raw.lisp" "raw" "raw" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1732285021) ("/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/hacker.lisp" "hacker" "hacker" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197252797) ("/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/rewrite-code.lisp" "rewrite-code" "rewrite-code" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 720904925) ("/usr/share/acl2-6.3/books/hacking/defstruct-parsing.lisp" "defstruct-parsing" "defstruct-parsing" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1553047268) ("/usr/share/acl2-6.3/books/hacking/hacker.lisp" "hacking/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/misc/expander.lisp" "misc/expander" "expander" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2012198438))
1719333008
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / ccg / ccg.cert
