acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / misc / nested-stobj-tests.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((13 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN CHECK-UPDATE-MOM (INDEX VAL1 VAL2 LAST-OP MOM) (DECLARE (XARGS :STOBJS MOM :MODE :PROGRAM :GUARD (OR (NULL INDEX) (AND (NATP INDEX) (< INDEX (KID2-AR-FIELD-LENGTH MOM)))))) (AND (EQUAL (LAST-OP MOM) LAST-OP) (STOBJ-LET ((KID1 (KID1-FIELD MOM)) (KID2 (KID2-AR-FIELDI INDEX MOM))) (VAL) (AND (EQUAL VAL1 (FLD1 KID1)) (EQUAL VAL2 (FLD2 KID2))) VAL)))) :RUN (LET* ((MOM (UPDATE-MOM 3 MOM)) (MOM (UPDATE-MOM (QUOTE (SWAP . 1)) MOM)) (MOM (UPDATE-MOM 7 MOM)) (MOM (UPDATE-MOM (QUOTE (SWAP . 0)) MOM)) (MOM (UPDATE-MOM 5 MOM)) (MOM (UPDATE-MOM (QUOTE (SWAP . 0)) MOM))) MOM) :CHECK (AND (CHECK-UPDATE-MOM 0 7 5 (QUOTE SWAP) MOM) (CHECK-UPDATE-MOM 1 7 3 (QUOTE SWAP) MOM))) (VALUE-TRIPLE :SUCCESS)) (16 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN CHECK-UPDATE-MOM-2 (I J VAL-I VAL-J MOM) (DECLARE (XARGS :STOBJS MOM :MODE :PROGRAM :GUARD (AND (NATP J) (< J (KID2-AR-FIELD-LENGTH MOM)) (NATP J) (< J (KID2-AR-FIELD-LENGTH MOM)) (NOT (EQUAL I J))))) (STOBJ-LET ((KID2 (KID2-AR-FIELDI I MOM)) (KID2A (KID2-AR-FIELDI J MOM))) (VAL) (AND (EQUAL (FLD2 KID2) VAL-I) (EQUAL (FLD2A KID2A) VAL-J)) VAL))) :RUN (LET* ((MOM (UPDATE-MOM 10 MOM)) (MOM (UPDATE-MOM (QUOTE (SWAP . 1)) MOM)) (MOM (UPDATE-MOM 20 MOM)) (MOM (UPDATE-MOM (QUOTE (SWAP . 0)) MOM)) (MOM (UPDATE-MOM 30 MOM)) (MOM (UPDATE-MOM (QUOTE (SWAP . 0)) MOM))) MOM) :CHECK (CHECK-UPDATE-MOM-2 0 1 30 10 MOM)) (VALUE-TRIPLE :SUCCESS)) (19 RECORD-EXPANSION (MUST-FAIL (DEFUN F (TOP1) (DECLARE (XARGS :STOBJS TOP1)) (TOP1-FLD TOP1))) (VALUE-TRIPLE (QUOTE T))) (20 RECORD-EXPANSION (MUST-FAIL (DEFUN F (SUB1 TOP1) (DECLARE (XARGS :STOBJS (SUB1 TOP1))) (UPDATE-TOP1-FLD SUB1 TOP1))) (VALUE-TRIPLE (QUOTE T))) (22 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (X TOP1) (DECLARE (XARGS :STOBJS TOP1)) (STOBJ-LET ((SUB1 (TOP1-FLD TOP1))) (VAL) (SUB1-FLD1 SUB1) (EQUAL VAL X)))) :RUN (TOP1-FLD.UPDATE-FLD1 17 TOP1) :CHECK (F1 17 TOP1)) (VALUE-TRIPLE :SUCCESS)) (23 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (X TOP1) (DECLARE (XARGS :STOBJS TOP1)) (STOBJ-LET ((SUB1 (TOP1-FLD TOP1))) (VAL) (SUB1-FLD1 SUB1) (EQUAL VAL X))) (DEFSTOBJ TOP1-INLINE (TOP1-FLD-INLINE :TYPE SUB1) :INLINE T :CONGRUENT-TO TOP1)) :RUN (TOP1-FLD.UPDATE-FLD1 18 TOP1-INLINE) :CHECK (F1 18 TOP1-INLINE)) (VALUE-TRIPLE :SUCCESS)) (28 RECORD-EXPANSION (MUST-FAIL (DEFUN TOP2.TEST1-BAD (TOP2) (DECLARE (XARGS :STOBJS TOP2)) (STOBJ-LET ((SUB1 (TOP2-FLD1 TOP2))) (SUB1 SUB1A) (LET* ((SUB1 (UPDATE-SUB1-FLD1 3 SUB1)) (SUB1A (UPDATE-SUB1-FLD1 4 SUB1A))) (MV SUB1 SUB1A)) TOP2))) (VALUE-TRIPLE (QUOTE T))) (30 RECORD-EXPANSION (MUST-FAIL (DEFUN NEWER-TOP1-FLD.UPDATE-FLD1 (X TOP1) (DECLARE (XARGS :STOBJS TOP1)) (STOBJ-LET ((SUB2 (TOP1-FLD TOP1))) (SUB2) (UPDATE-SUB1-FLD1 X SUB2) TOP1))) (VALUE-TRIPLE (QUOTE T))) (34 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (TOP3) (DECLARE (XARGS :STOBJS TOP3)) (STOBJ-LET ((SUB1 (TOP3-FLDI *I1* TOP3)) (SUB1A (TOP3-FLDI *I2* TOP3))) (SUB1 SUB1A) (LET* ((SUB1 (UPDATE-SUB1-FLD1 (QUOTE X) SUB1)) (SUB1A (UPDATE-SUB1-FLD1 (QUOTE Y) SUB1A))) (MV SUB1 SUB1A)) TOP3)) (DEFUN F2 (TOP3) (DECLARE (XARGS :STOBJS TOP3)) (STOBJ-LET ((SUB1 (TOP3-FLDI *I1* TOP3)) (SUB1A (TOP3-FLDI *I2* TOP3))) (VAL1 VAL2) (MV (SUB1-FLD1 SUB1) (SUB1-FLD1 SUB1A)) (AND (EQ VAL1 (QUOTE X)) (EQ VAL2 (QUOTE Y)))))) :RUN (F1 TOP3) :CHECK (F2 TOP3)) (VALUE-TRIPLE :SUCCESS)) (35 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (TOP3) (DECLARE (XARGS :STOBJS TOP3)) (STOBJ-LET ((SUB1 (TOP3-FLDI 3 TOP3)) (SUB1A (TOP3-FLDI 4 TOP3))) (SUB1 SUB1A) (LET* ((SUB1 (UPDATE-SUB1-FLD1 (QUOTE A) SUB1)) (SUB1A (UPDATE-SUB1-FLD1 (QUOTE B) SUB1A))) (MV SUB1 SUB1A)) TOP3)) (DEFUN F2 (TOP3) (DECLARE (XARGS :STOBJS TOP3)) (STOBJ-LET ((SUB1 (TOP3-FLDI 3 TOP3)) (SUB1A (TOP3-FLDI 4 TOP3))) (VAL3 VAL4) (MV (SUB1-FLD1 SUB1) (SUB1-FLD1 SUB1A)) (AND (EQ VAL3 (QUOTE A)) (EQ VAL4 (QUOTE B)))))) :RUN (F1 TOP3) :CHECK (F2 TOP3)) (VALUE-TRIPLE :SUCCESS)) (36 RECORD-EXPANSION (MUST-FAIL (DEFUN FOO (TOP3) (DECLARE (XARGS :STOBJS TOP3)) (STOBJ-LET ((SUB1 (TOP3-FLDI 5 TOP3))) (SUB1) (UPDATE-SUB1-FLD1 (QUOTE X) SUB1) (TOP3P TOP3)))) (VALUE-TRIPLE (QUOTE T))) (37 RECORD-EXPANSION (MUST-FAIL (DEFUN FOO (TOP3) (DECLARE (XARGS :STOBJS TOP3)) (STOBJ-LET ((SUB1 (TOP3-FLDI 5 TOP3)) (SUB1A (TOP3-FLDI 6 TOP3))) (SUB1 SUB1A) (LET* ((SUB1 (UPDATE-SUB1-FLD1 (QUOTE X) SUB1)) (SUB1A (UPDATE-SUB1-FLD1 (QUOTE X) SUB1A))) (MV SUB1 SUB1A)) (TOP3P TOP3)))) (VALUE-TRIPLE (QUOTE T))) (38 RECORD-EXPANSION (MUST-FAIL (DEFUN FOO (TOP3) (DECLARE (XARGS :STOBJS TOP3)) (STOBJ-LET ((SUB1 (TOP3-FLDI 5 TOP3)) (SUB1A (TOP3-FLDI 5 TOP3))) (SUB1 SUB1A) (LET* ((SUB1A (UPDATE-SUB1-FLD1 (QUOTE X) SUB1A)) (SUB1 (UPDATE-SUB1-FLD1 (QUOTE Y) SUB1))) (MV SUB1 SUB1A)) TOP3))) (VALUE-TRIPLE (QUOTE T))) (45 RECORD-EXPANSION (MUST-FAIL (DEFUN TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 (I1 V1 I2 V2 TOP3) (DECLARE (TYPE (INTEGER 0 9) I1 I2) (XARGS :STOBJS TOP3)) (STOBJ-LET ((SUB1 (TOP3-FLDI I1 TOP3)) (SUB1A (TOP3-FLDI I2 TOP3))) (SUB1 SUB1A) (LET* ((SUB1A (UPDATE-SUB1-FLD1 V2 SUB1A)) (SUB1 (UPDATE-SUB1-FLD1 V1 SUB1))) (MV SUB1 SUB1A)) TOP3))) (VALUE-TRIPLE (QUOTE T))) (46 RECORD-EXPANSION (MUST-FAIL (DEFUN TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 (I1 V1 I2 V2 TOP3) (DECLARE (TYPE (INTEGER 0 9) I1) (XARGS :STOBJS TOP3 :GUARD (NOT (EQL I1 I2)))) (STOBJ-LET ((SUB1 (TOP3-FLDI I1 TOP3)) (SUB1A (TOP3-FLDI I2 TOP3))) (SUB1 SUB1A) (LET* ((SUB1A (UPDATE-SUB1-FLD1 V2 SUB1A)) (SUB1 (UPDATE-SUB1-FLD1 V1 SUB1))) (MV SUB1 SUB1A)) TOP3))) (VALUE-TRIPLE (QUOTE T))) (47 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (TOP3) (DECLARE (XARGS :STOBJS TOP3)) (STOBJ-LET ((SUB1 (TOP3-FLDI 3 TOP3)) (SUB1A (TOP3-FLDI 4 TOP3))) (V1 V2) (LET* ((V2 (SUB1-FLD1 SUB1A)) (V1 (SUB1-FLD1 SUB1))) (MV V1 V2)) (AND (EQUAL V1 (QUOTE THREE)) (EQUAL V2 (QUOTE FOUR)))))) :RUN (TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 3 (QUOTE THREE) 4 (QUOTE FOUR) TOP3) :CHECK (F1 TOP3)) (VALUE-TRIPLE :SUCCESS)) (49 RECORD-EXPANSION (MUST-FAIL (DEFSTOBJ TOP1B (TOP1B-FLD :TYPE SUB1A) :CONGRUENT-TO TOP1)) (VALUE-TRIPLE (QUOTE T))) (50 RECORD-EXPANSION (MUST-FAIL (TRANS-EVAL (QUOTE (LET ((TOP1A TOP1)) TOP1A)) (QUOTE TOP) STATE T)) (VALUE-TRIPLE (QUOTE T))) (51 RECORD-EXPANSION (MUST-FAIL (TRANS-EVAL (QUOTE (MV-LET (TOP1A X) (MV TOP1 3) (MV TOP1A X))) (QUOTE TOP) STATE T)) (VALUE-TRIPLE (QUOTE T))) (52 RECORD-EXPANSION (MUST-FAIL (DEFSTOBJ TOP1-BAD (TOP1-BAD-FLD :TYPE STATE))) (VALUE-TRIPLE (QUOTE T))) (53 RECORD-EXPANSION (MUST-FAIL (DEFSTOBJ BAD-STOBJ STATE)) (VALUE-TRIPLE (QUOTE T))) (67 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (TOP1) (DECLARE (XARGS :STOBJS TOP1 :VERIFY-GUARDS NIL)) (STOBJ-ER-TEST (QUOTE (4 5)) TOP1))) :RUN (F1 TOP1) :CHECK T) (VALUE-TRIPLE :SUCCESS)) (68 RECORD-EXPANSION (MUST-FAIL (LOCAL-TEST :DEFS ((DEFUN F1 (TOP1) (DECLARE (XARGS :STOBJS TOP1 :VERIFY-GUARDS NIL)) (STOBJ-ER-TEST (QUOTE 3) TOP1))) :RUN (WITH-GUARD-CHECKING T (F1 TOP1)) :CHECK T)) (VALUE-TRIPLE (QUOTE T))) (69 RECORD-EXPANSION (MUST-FAIL (DEFUN BAD-TOP1-FLD.UPDATE-FLD1 (TOP1 STATE) (DECLARE (XARGS :MODE :PROGRAM :STOBJS (TOP1 STATE))) (STOBJ-LET ((SUB1 (TOP1-FLD TOP1))) (ERP VAL STATE) (UPDATE-SUB1-FLD1 17 SUB1) (MV ERP VAL STATE)))) (VALUE-TRIPLE (QUOTE T))) (71 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (X) (WITH-LOCAL-STOBJ TOP1 (MV-LET (VAL TOP1) (LET* ((TOP1 (STOBJ-LET ((SUB1 (TOP1-FLD TOP1))) (SUB1) (UPDATE-SUB1-FLD1 X SUB1) TOP1)) (VAL (STOBJ-LET ((SUB1 (TOP1-FLD TOP1))) (VAL) (SUB1-FLD1 SUB1) VAL))) (MV VAL TOP1)) VAL)))) :RUN (TOP1-FLD.UPDATE-FLD1 17 TOP1) :CHECK (AND (EQL (F1 3) 3) (EQL (TOP1-FLD.FLD1 TOP1) 17))) (VALUE-TRIPLE :SUCCESS)) (72 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (X Y TOP1) (DECLARE (XARGS :STOBJS TOP1)) (STOBJ-LET ((SUB1 (TOP1-FLD TOP1))) (SUB1) (WITH-LOCAL-STOBJ TOP1 (MV-LET (SUB1 TOP1) (LET ((TOP1 (TOP1-FLD.UPDATE-FLD1 Y TOP1))) (LET ((SUB1 (UPDATE-SUB1-FLD1 X SUB1))) (MV SUB1 TOP1))) SUB1)) TOP1))) :RUN (F1 10 20 TOP1) :CHECK (EQL (TOP1-FLD.FLD1 TOP1) 10)) (VALUE-TRIPLE :SUCCESS)) (73 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (X Y TOP1) (DECLARE (XARGS :STOBJS TOP1)) (STOBJ-LET ((SUB1 (TOP1-FLD TOP1))) (SUB1) (WITH-LOCAL-STOBJ TOP1 (MV-LET (SUB1 TOP1) (LET ((SUB1 (UPDATE-SUB1-FLD1 X SUB1))) (LET ((TOP1 (TOP1-FLD.UPDATE-FLD1 Y TOP1))) (MV SUB1 TOP1))) SUB1)) TOP1))) :RUN (F1 30 40 TOP1) :CHECK (EQL (TOP1-FLD.FLD1 TOP1) 30)) (VALUE-TRIPLE :SUCCESS)) (76 RECORD-EXPANSION (MUST-FAIL (SKIP-PROOFS (DEFUN BAD-TOP4.TEST1 (TOP4) (DECLARE (XARGS :STOBJS TOP4)) (STOBJ-LET ((SUB2 (TOP4-FLD1 TOP4)) (SUB1 (TOP4-FLD2 TOP4))) (SUB1 SUB2) (LET* ((SUB1 (UPDATE-SUB1-FLD1 3 SUB1)) (SUB2 (UPDATE-SUB2-FLD1 4 SUB2))) (MV SUB1 SUB2)) TOP4)))) (VALUE-TRIPLE (QUOTE T))) (78 RECORD-EXPANSION (MUST-FAIL (DEFUN TOP3A.FLDI.UPDATE-SUB1-FLD1/I1/I2 (I1 V1 I2 V2 TOP3A) (DECLARE (TYPE (INTEGER 0 9) I1 I2) (XARGS :STOBJS TOP3A :GUARD (NOT (EQL I1 I2)))) (STOBJ-LET ((SUB1 (TOP3A-FLDI I1 TOP3A)) (SUB1A (TOP3A-FLDI I2 TOP3A))) (SUB1 SUB1A) (LET* ((SUB1A (UPDATE-SUB1-FLD1 V2 SUB1A)) (SUB1 (UPDATE-SUB1-FLD1 V1 SUB1))) (MV SUB1 SUB1A)) TOP3A))) (VALUE-TRIPLE (QUOTE T))) (84 RECORD-EXPANSION (LOCAL-TEST :DEFS NIL :RUN (LET ((TOP3A (RESIZE-TOP3A-FLD 20 TOP3A))) (TOP3A.FLDI.UPDATE-SUB1-FLD1/I1/I2 3 (QUOTE THREE) 15 (QUOTE FIFTEEN) TOP3A)) :CHECK (AND (EQUAL (TOP3A.SUB1-FLD1/I 15 TOP3A) (QUOTE FIFTEEN)) (EQUAL (TOP3A.SUB1-FLD1/I 16 TOP3A) NIL))) (VALUE-TRIPLE :SUCCESS)) (88 RECORD-EXPANSION (LOCAL-TEST :DEFS NIL :RUN (SUPER1-UPDATE (QUOTE ABC) SUPER1) :CHECK (EQ (SUPER1-ACCESS SUPER1) (QUOTE ABC))) (VALUE-TRIPLE :SUCCESS)) (90 RECORD-EXPANSION (LOCAL-TEST :DEFS ((DEFUN F1 (X TOP1C) (DECLARE (XARGS :STOBJS TOP1C)) (STOBJ-LET ((SUB1 (GET-TOP1C-SUB1 TOP1C) SET-TOP1C-SUB1)) (VAL) (SUB1-FLD1 SUB1) (EQUAL VAL X)))) :RUN (TOP1-FLD.UPDATE-FLD1 17 TOP1C) :CHECK (F1 17 TOP1C)) (VALUE-TRIPLE :SUCCESS)))
NIL
(("/usr/share/acl2-6.3/books/misc/nested-stobj-tests.lisp" "nested-stobj-tests" "nested-stobj-tests" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 61670677) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718))
469983412