/usr/share/acl2-6.3/books/make-event/eval-check-tests.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 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((2 RECORD-EXPANSION (MUST-SUCCEED (DEFTHM EVAL-BAR (EQUAL X (CAR (CONS X Y))) :RULE-CLASSES NIL)) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (DEFTHM EVAL-BAR (EQUAL X (CAR (CONS X Y))) :RULE-CLASSES NIL) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (DEFTHM EVAL-BAR (EQUAL X (CAR (CONS X Y))) :RULE-CLASSES NIL) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (DEFTHM EVAL-BAR (EQUAL X (CAR (CONS X Y))) :RULE-CLASSES NIL) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (DEFTHM EVAL-BAR (EQUAL X (CAR (CONS X Y))) :RULE-CLASSES NIL) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))) T)) :ON-BEHALF-OF (MUST-SUCCEED (DEFTHM EVAL-BAR (EQUAL X (CAR (CONS X Y))) :RULE-CLASSES NIL)))) (4 RECORD-EXPANSION (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))))) (5 RECORD-EXPANSION (MUST-SUCCEED (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))) T)) :ON-BEHALF-OF (MUST-SUCCEED (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))))))) (6 RECORD-EXPANSION (MUST-SUCCEED (WITH-OUTPUT :OFF :ALL (PPROGN (F-PUT-GLOBAL (QUOTE SAVED-WORLD-LENGTH) (LENGTH (W STATE)) STATE) (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))))))))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF :ALL (PPROGN (F-PUT-GLOBAL (QUOTE SAVED-WORLD-LENGTH) (LENGTH (W STATE)) STATE) (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF :ALL (PPROGN (F-PUT-GLOBAL (QUOTE SAVED-WORLD-LENGTH) (LENGTH (W STATE)) STATE) (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF :ALL (PPROGN (F-PUT-GLOBAL (QUOTE SAVED-WORLD-LENGTH) (LENGTH (W STATE)) STATE) (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF :ALL (PPROGN (F-PUT-GLOBAL (QUOTE SAVED-WORLD-LENGTH) (LENGTH (W STATE)) STATE) (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))) T)) :ON-BEHALF-OF (MUST-SUCCEED (WITH-OUTPUT :OFF :ALL (PPROGN (F-PUT-GLOBAL (QUOTE SAVED-WORLD-LENGTH) (LENGTH (W STATE)) STATE) (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))))))))))) (7 RECORD-EXPANSION (MUST-SUCCEED (DEFTHM TEMP (EQUAL (CAR (CONS X Y)) X))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (DEFTHM TEMP (EQUAL (CAR (CONS X Y)) X)) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (DEFTHM TEMP (EQUAL (CAR (CONS X Y)) X)) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (DEFTHM TEMP (EQUAL (CAR (CONS X Y)) X)) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (DEFTHM TEMP (EQUAL (CAR (CONS X Y)) X)) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))) T)) :ON-BEHALF-OF (MUST-SUCCEED (DEFTHM TEMP (EQUAL (CAR (CONS X Y)) X))))) (8 RECORD-EXPANSION (MUST-FAIL (MV (EQUAL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))) NIL STATE)) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (MV (EQUAL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))) NIL STATE) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (MV (EQUAL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))) NIL STATE) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (MV (EQUAL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))) NIL STATE) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (MV (EQUAL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))) NIL STATE) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (MV (EQUAL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))) NIL STATE)))) (9 RECORD-EXPANSION (MUST-SUCCEED (WITH-OUTPUT :OFF ERROR (COND ((NOT (EQL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE)))) (WITH-OUTPUT :ON ERROR (ER SOFT (QUOTE TEST-FAILURE) "World length changed from ~x0 to ~x1." (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))))) (T (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF ERROR (THM (EQUAL X (CONS X X))))))))))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF ERROR (COND ((NOT (EQL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE)))) (WITH-OUTPUT :ON ERROR (ER SOFT (QUOTE TEST-FAILURE) "World length changed from ~x0 to ~x1." (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))))) (T (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF ERROR (THM (EQUAL X (CONS X X)))))))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF ERROR (COND ((NOT (EQL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE)))) (WITH-OUTPUT :ON ERROR (ER SOFT (QUOTE TEST-FAILURE) "World length changed from ~x0 to ~x1." (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))))) (T (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF ERROR (THM (EQUAL X (CONS X X)))))))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF ERROR (COND ((NOT (EQL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE)))) (WITH-OUTPUT :ON ERROR (ER SOFT (QUOTE TEST-FAILURE) "World length changed from ~x0 to ~x1." (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))))) (T (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF ERROR (THM (EQUAL X (CONS X X)))))))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (WITH-OUTPUT :OFF ERROR (COND ((NOT (EQL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE)))) (WITH-OUTPUT :ON ERROR (ER SOFT (QUOTE TEST-FAILURE) "World length changed from ~x0 to ~x1." (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))))) (T (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF ERROR (THM (EQUAL X (CONS X X)))))))))) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))) T)) :ON-BEHALF-OF (MUST-SUCCEED (WITH-OUTPUT :OFF ERROR (COND ((NOT (EQL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE)))) (WITH-OUTPUT :ON ERROR (ER SOFT (QUOTE TEST-FAILURE) "World length changed from ~x0 to ~x1." (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))))) (T (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF ERROR (THM (EQUAL X (CONS X X))))))))))))) (10 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL))))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL))))))) (11 RECORD-EXPANSION (MUST-SUCCEED (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)) STATE))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)) STATE)) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)) STATE)) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)) STATE)) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)) STATE)) (DECLARE (IGNORE VAL)) (VALUE (EQ ERP NIL))) T)) :ON-BEHALF-OF (MUST-SUCCEED (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)) STATE))))) (12 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (MV T NIL STATE))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV T NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV T NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV T NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV T NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (MAKE-EVENT (MV T NIL STATE))))) (13 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (MV "Sample Expansion Error" NIL STATE))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV "Sample Expansion Error" NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV "Sample Expansion Error" NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV "Sample Expansion Error" NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV "Sample Expansion Error" NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (MAKE-EVENT (MV "Sample Expansion Error" NIL STATE))))) (14 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (MV (MSG "Sample Expansion Error: ~x0, ~@1" 17 (MSG "howdy ~x0" 23)) NIL STATE))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV (MSG "Sample Expansion Error: ~x0, ~@1" 17 (MSG "howdy ~x0" 23)) NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV (MSG "Sample Expansion Error: ~x0, ~@1" 17 (MSG "howdy ~x0" 23)) NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV (MSG "Sample Expansion Error: ~x0, ~@1" 17 (MSG "howdy ~x0" 23)) NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (MAKE-EVENT (MV (MSG "Sample Expansion Error: ~x0, ~@1" 17 (MSG "howdy ~x0" 23)) NIL STATE)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (MAKE-EVENT (MV (MSG "Sample Expansion Error: ~x0, ~@1" 17 (MSG "howdy ~x0" 23)) NIL STATE))))))
NIL
(("/usr/share/acl2-6.3/books/make-event/eval-check-tests.lisp" "eval-check-tests" "eval-check-tests" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1351300563) ("/usr/share/acl2-6.3/books/make-event/eval-check.lisp" "eval-check" "eval-check" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 309385933))
304597685
|