acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / tools / bstar.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((51 RECORD-EXPANSION (WITH-OUTPUT :OFF WARNING (LOCAL (PROGN (DEFUN RETURN-TWO-VALUES (A B) (MV A B)) (DEFUN TRANSL-EQUAL-TESTS-FN (TESTS) (IF (ATOM TESTS) (CONS (QUOTE MV) (CONS (QUOTE NIL) (CONS (QUOTE STATE) (QUOTE NIL)))) (CONS (QUOTE MV-LET) (CONS (CONS (QUOTE ERR) (CONS (QUOTE VAL) (CONS (QUOTE STATE) (QUOTE NIL)))) (CONS (CONS (QUOTE TRANSL-EQUAL) (CONS (CONS (QUOTE QUOTE) (CONS (CAAR TESTS) (QUOTE NIL))) (CONS (CONS (QUOTE QUOTE) (CONS (CADAR TESTS) (QUOTE NIL))) (QUOTE NIL)))) (CONS (CONS (QUOTE IF) (CONS (CONS (QUOTE OR) (CONS (QUOTE ERR) (CONS (CONS (QUOTE NOT) (CONS (QUOTE VAL) (QUOTE NIL))) (QUOTE NIL)))) (CONS (CONS (QUOTE MV) (CONS (CONS (QUOTE QUOTE) (CONS (CAR TESTS) (QUOTE NIL))) (CONS (QUOTE STATE) (QUOTE NIL)))) (CONS (TRANSL-EQUAL-TESTS-FN (CDR TESTS)) (QUOTE NIL))))) (QUOTE NIL))))))) (DEFMACRO TRANSL-EQUAL-TESTS (&REST TESTS) (TRANSL-EQUAL-TESTS-FN TESTS)) (DEFSTOBJ ST1 (ARR1 :TYPE (ARRAY T (0)) :RESIZABLE T)) (DEFSTOBJ ST2 (ARR2 :TYPE (ARRAY T (0)) :RESIZABLE T)) (DEFUN PATBIND-TESTS-FN (TESTS STATE) (DECLARE (XARGS :MODE :PROGRAM)) (IF (ATOM TESTS) (VALUE (QUOTE (VALUE-TRIPLE :INVISIBLE))) (MV-LET (ERP VAL STATE) (THM-FN (CONS (QUOTE EQUAL) (CONS (CAAR TESTS) (CONS (CADAR TESTS) (QUOTE NIL)))) STATE (QUOTE (("goal" :IN-THEORY NIL))) NIL NIL) (IF ERP (MV (MSG "~% ****** ERROR ******~%~
Testing of the patbind macro failed on expression ~x0~%~%" (CAR TESTS)) VAL STATE) (PATBIND-TESTS-FN (CDR TESTS) STATE))))) (DEFMACRO PATBIND-RUN-TESTS (&REST TESTS) (CONS (QUOTE MAKE-EVENT) (CONS (CONS (QUOTE PATBIND-TESTS-FN) (CONS (CONS (QUOTE QUOTE) (CONS TESTS (QUOTE NIL))) (CONS (QUOTE STATE) (QUOTE NIL)))) (QUOTE NIL)))) (PATBIND-RUN-TESTS ((PATBIND (CONS (CONS A B) C) (X) (LIST A B C)) (LET* ((|(CAR X)| (CAR X)) (C (CDR X))) (LET* ((A (CAR |(CAR X)|)) (B (CDR |(CAR X)|))) (LIST A B C)))) ((PATBIND X ((CONS (QUOTE A) (QUOTE B))) X) (LET ((X (CONS (QUOTE A) (QUOTE B)))) X)) ((PATBIND (MV A B) ((MV (QUOTE A) (QUOTE B))) (LIST A B)) (MV-LET (A B) (MV (QUOTE A) (QUOTE B)) (LIST A B))) ((PATBIND & ((CW "Hello")) NIL) NIL) ((PATBIND - ((CW "Hello")) NIL) (PROG2$ (CW "Hello") NIL)) ((PATBIND (CONS A &) ((QUOTE (A B))) A) (LET ((A (CAR (QUOTE (A B))))) A)) ((PATBIND (CONS (CONS A B) C) (X) (LIST A B C)) (LET ((|(CONS A B)| (CAR X)) (C (CDR X))) (LET ((A (CAR |(CONS A B)|)) (B (CDR |(CONS A B)|))) (LIST A B C)))) ((PATBIND (CONS (CONS A B) C) ((CONS X Y)) (LIST A B C)) (LET ((|(CONS (CONS A B) C)| (CONS X Y))) (LET ((|(CONS A B)| (CAR |(CONS (CONS A B) C)|)) (C (CDR |(CONS (CONS A B) C)|))) (LET ((A (CAR |(CONS A B)|)) (B (CDR |(CONS A B)|))) (LIST A B C))))) ((PATBIND (CONS (CONS & B) C) ((CONS X Y)) (LIST B C)) (LET ((|(CONS (CONS & B) C)| (CONS X Y))) (LET ((|(CONS & B)| (CAR |(CONS (CONS & B) C)|)) (C (CDR |(CONS (CONS & B) C)|))) (LET ((B (CDR |(CONS & B)|))) (LIST B C))))) ((PATBIND (CONS (CONS A &) C) ((CONS X Y)) (LIST A C)) (LET ((|(CONS (CONS A &) C)| (CONS X Y))) (LET ((|(CONS A &)| (CAR |(CONS (CONS A &) C)|)) (C (CDR |(CONS (CONS A &) C)|))) (LET ((A (CAR |(CONS A &)|))) (LIST A C))))) ((PATBIND (MV (CONS A (CONS B C)) D) ((RETURN-TWO-VALUES X Y)) (LIST A B C D)) (MV-LET (|(CONS A (CONS B C))| D) (RETURN-TWO-VALUES X Y) (LET ((A (CAR |(CONS A (CONS B C))|)) (|(CONS B C)| (CDR |(CONS A (CONS B C))|))) (LET ((B (CAR |(CONS B C)|)) (C (CDR |(CONS B C)|))) (LIST A B C D))))) ((PATBIND (MV (CONS A (CONS B C)) &) ((RETURN-TWO-VALUES X Y)) (LIST A B C D)) (MV-LET (|(CONS A (CONS B C))| IGNORE-0) (RETURN-TWO-VALUES X Y) (DECLARE (IGNORE IGNORE-0)) (LET ((A (CAR |(CONS A (CONS B C))|)) (|(CONS B C)| (CDR |(CONS A (CONS B C))|))) (LET ((B (CAR |(CONS B C)|)) (C (CDR |(CONS B C)|))) (LIST A B C D))))) ((PATBIND (MV (CONS A (CONS & C)) &) ((RETURN-TWO-VALUES X Y)) (LIST A C D)) (MV-LET (|(CONS A (CONS & C))| IGNORE-0) (RETURN-TWO-VALUES X Y) (DECLARE (IGNORE IGNORE-0)) (LET ((A (CAR |(CONS A (CONS & C))|)) (|(CONS & C)| (CDR |(CONS A (CONS & C))|))) (LET ((C (CDR |(CONS & C)|))) (LIST A C D))))) ((PATBIND (CONS A (CONS B (QUOTE NIL))) ((CONS X Y)) (LIST A B)) (LET ((|(CONS A (CONS B (QUOTE NIL)))| (CONS X Y))) (LET ((A (CAR |(CONS A (CONS B (QUOTE NIL)))|)) (|(CONS B (QUOTE NIL))| (CDR |(CONS A (CONS B (QUOTE NIL)))|))) (LET ((B (CAR |(CONS B (QUOTE NIL))|))) (LIST A B)))))) (DEFTHM LEN-RESIZE-LIST (EQUAL (LEN (RESIZE-LIST A B C)) (NFIX B))) (DEFUN LOCALSTOBJTEST (A B C) (DECLARE (XARGS :GUARD T)) (B* ((D (CONS B C)) ((LOCAL-STOBJS ST1 ST2) (MV G ST2 H ST1)) (A (NFIX A)) (ST1 (RESIZE-ARR1 (+ 1 A) ST1)) (ST2 (RESIZE-ARR2 (+ 1 (NFIX B)) ST2)) (ST1 (UPDATE-ARR1I A D ST1)) (ST2 (UPDATE-ARR2I (NFIX B) A ST2))) (MV (ARR2I (NFIX B) ST2) ST2 (ARR1I A ST1) ST1))) (MAKE-EVENT (MV-LET (RES1 RES2) (LOCALSTOBJTEST NIL 10 (QUOTE C)) (IF (AND (EQUAL RES1 0) (EQUAL RES2 (QUOTE (10 . C)))) (QUOTE (VALUE-TRIPLE :PASSED)) (ER HARD (QUOTE TEST-LOCAL-STOBJ) "test failed"))))))) (WITH-OUTPUT :OFF WARNING (LOCAL (VALUE-TRIPLE :ELIDED)))))
NIL
(("/usr/share/acl2-6.3/books/tools/bstar.lisp" "bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439))
1521988724