acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / parallel / syntax-tests.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((4 RECORD-EXPANSION (ASSERT! (EQUAL (PLET-TEST10) 10)) (VALUE-TRIPLE :SUCCESS)) (5 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (QUOTE (LET ((Q 10)) (PLET ((X 4) (Y (+ 9 Q))) (+ X Y)))))) (VALUE-TRIPLE (QUOTE T))) (6 RECORD-EXPANSION (MUST-SUCCEED (SET-PARALLEL-EXECUTION NIL)) (VALUE-TRIPLE (QUOTE T))) (7 RECORD-EXPANSION (ASSERT! (AND (PAND) (PAND (EQUAL 4 4)) (PAND (EQUAL 4 4) (EQUAL 6 6) (EQUAL 9 9) (EQUAL 1 1) (EQUAL 5 5)) (NOT (PAND (EQUAL 4 5))) (NOT (PAND (EQUAL 4 4) (EQUAL 4 5))) (NOT (PAND (EQUAL 1 1) (EQUAL 2 3) (EQUAL 1 1))) (PAND (QUOTE (CONSP 3))) (NOT (PAND (CONSP 3))))) (VALUE-TRIPLE :SUCCESS)) (8 RECORD-EXPANSION (ASSERT! (AND (POR (QUOTE (CONSP 3))) (NOT (POR (CONSP 3))))) (VALUE-TRIPLE :SUCCESS)) (10 RECORD-EXPANSION (MUST-SUCCEED (ASSERT! (EQUAL (PFIB 10) 55))) (VALUE-TRIPLE (QUOTE T))) (11 RECORD-EXPANSION (ASSERT! (EQUAL (LET ((Q 10)) (PLET ((X 4) (Y (+ 9 Q))) (+ X Y))) 23)) (VALUE-TRIPLE :SUCCESS)) (12 RECORD-EXPANSION (ASSERT! (EQUAL (LET ((Q 10)) (PLET ((X 4) (Y 9)) (+ X Y Q))) 23)) (VALUE-TRIPLE :SUCCESS)) (13 RECORD-EXPANSION (ASSERT! (EQUAL (LET ((Q 10)) (PLET ((X 4) (Y (+ 9 Q))) (+ X Y Q))) 33)) (VALUE-TRIPLE :SUCCESS)) (14 RECORD-EXPANSION (ASSERT! (EQUAL (PLET NIL 4) 4)) (VALUE-TRIPLE :SUCCESS)) (15 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (QUOTE (VALUE-TRIPLE (PARGS 4))))) (VALUE-TRIPLE (QUOTE T))) (17 RECORD-EXPANSION (ASSERT! (EQUAL (PLET ((X *TMP*)) X) 4)) (VALUE-TRIPLE :SUCCESS)) (19 RECORD-EXPANSION (MUST-FAIL (DEFUN TEST-GRANULARITY2 (X) (DECLARE (XARGS :GUARD (NATP X))) (PARGS (DECLARE (WRONG-NAME (> X 5))) (BINARY-+ X X)))) (VALUE-TRIPLE (QUOTE T))) (24 RECORD-EXPANSION (MUST-FAIL (DEFUN ERROR-PAND (X) (DECLARE (XARGS :GUARD T)) (PAND (CONSP X) (EQUAL (CAR X) 4)))) (VALUE-TRIPLE (QUOTE T))) (25 RECORD-EXPANSION (MUST-FAIL (DEFUN ERROR-POR (X) (DECLARE (XARGS :GUARD T)) (POR (ATOM X) (EQUAL (CAR X) 4)))) (VALUE-TRIPLE (QUOTE T))) (26 RECORD-EXPANSION (MUST-FAIL (DEFUN PARGS-LET NIL (PARGS (LET ((X 4) (Y 5)) (+ X Y))))) (VALUE-TRIPLE (QUOTE T))) (27 RECORD-EXPANSION (MUST-FAIL (DEFUN PARGS-PLET NIL (PARGS (PLET ((X 4) (Y 5)) (+ X Y))))) (VALUE-TRIPLE (QUOTE T))) (29 RECORD-EXPANSION (LOCAL (ENCAPSULATE NIL (DEFUN TEST-STOBJ (X FOO) (DECLARE (XARGS :STOBJS FOO)) (PLET ((FOO (UPDATE-FIELD1 17 FOO))) (UPDATE-FIELD2 X FOO))) (ASSERT!-STOBJ (LET* ((FOO (TEST-STOBJ 14 FOO))) (MV (EQUAL (FIELD1 FOO) 17) FOO)) FOO) (ASSERT!-STOBJ (LET* ((FOO (TEST-STOBJ 14 FOO))) (MV (EQUAL (FIELD1 FOO) 17) FOO)) FOO) (ASSERT!-STOBJ (LET* ((FOO (TEST-STOBJ 14 FOO))) (MV (EQUAL (FIELD1 FOO) 17) FOO)) FOO) (MUST-FAIL (ASSERT!-STOBJ (LET* ((FOO (TEST-STOBJ 14 FOO))) (MV (EQUAL (FIELD1 FOO) 14) FOO)) FOO)))) (LOCAL (VALUE-TRIPLE :ELIDED))) (30 RECORD-EXPANSION (MUST-FAIL (DEFUN TEST-STOBJ-PWRITE (FOO) (DECLARE (XARGS :STOBJS FOO :GUARD (AND (ACL2-NUMBERP (FIELD1 FOO)) (ACL2-NUMBERP (FIELD2 FOO))))) (PLET ((FOO (UPDATE-FIELD1 FOO 14)) (FOO (UPDATE-FIELD2 FOO 15))) (FIELD1 FOO)))) (VALUE-TRIPLE (QUOTE T))) (35 RECORD-EXPANSION (MUST-SUCCEED (DEFUN PLET-DECLARE-TEST0 (X) (DECLARE (XARGS :GUARD (INTEGERP X))) (PLET (DECLARE (GRANULARITY (> X 4))) ((Y X) (Z 8)) (DECLARE (IGNORE Z)) Y))) (VALUE-TRIPLE (QUOTE T))) (36 RECORD-EXPANSION (MUST-FAIL (DEFUN PLET-DECLARE-TEST1 (X) (DECLARE (XARGS :GUARD T)) (PLET (DECLARE (GRANULARITY (> X 4))) ((Y X) (Z 8)) (DECLARE (IGNORE Z)) Y))) (VALUE-TRIPLE (QUOTE T))) (37 RECORD-EXPANSION (MUST-SUCCEED (DEFUN PLET-DECLARE-TEST2 (X) (DECLARE (XARGS :GUARD (INTEGERP X))) (PLET (DECLARE (GRANULARITY (> X 4))) ((Y X) (Z 8) (BOOGA (QUOTE THE_CLOUDS))) (DECLARE (IGNORE Z)) (DECLARE (IGNORE BOOGA)) Y))) (VALUE-TRIPLE (QUOTE T))) (38 RECORD-EXPANSION (MUST-FAIL (DEFUN PLET-DECLARE-TEST3 (X) (DECLARE (XARGS :GUARD (INTEGERP X))) (PLET (DECLARE (GRANULARITY (> X 4))) ((Y X) (Z 8)) (DECLARE (IGNORE Z)) (DECLARE (FIXNUM Y)) Y))) (VALUE-TRIPLE (QUOTE T))) (39 RECORD-EXPANSION (MUST-FAIL (DEFUN PLET-DECLARE-TEST4 (X) (DECLARE (XARGS :GUARD (INTEGERP X))) (PLET (DECLARE (GRANULARITY (> X 4))) ((Y X) (Z 8)) (DECLARE (FIXNUM Y)) Y))) (VALUE-TRIPLE (QUOTE T))) (40 RECORD-EXPANSION (MUST-FAIL (DEFUN LET-DECLARE-TEST0 (X) (DECLARE (XARGS :GUARD T)) (LET ((Y X) (Z 8)) (DECLARE (IGNORE Z)) Y Y))) (VALUE-TRIPLE (QUOTE T))))
NIL
(("/usr/share/acl2-6.3/books/parallel/syntax-tests.lisp" "syntax-tests" "syntax-tests" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 931179814) ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718))
1016622025