acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / memoize / top.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (INCLUDE-RAW "timer.lsp") (PROGN (PROGN! (SET-RAW-MODE T) (DEFUN RAW-COMPILE (NAME ERROR-ON-FAIL ON-FAIL STATE) (COND ((NOT (MEMBER :CLTL2 *FEATURES*)) (COMPILE-FILE (EXTEND-PATHNAME (CBD) NAME STATE))) (T (HANDLER-CASE (COMPILE-FILE (EXTEND-PATHNAME (CBD) NAME STATE)) (ERROR (CONDITION) (IF ERROR-ON-FAIL (LET ((CONDITION-STR (FORMAT NIL "~a" CONDITION))) (ER HARD (QUOTE INCLUDE-RAW) "Compilation of ~x0 failed with the following message:~%~@1~%" NAME CONDITION-STR)) (EVAL (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE CONDITION) (CONS (CONS (QUOTE QUOTE) (CONS CONDITION (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE DECLARE) (CONS (CONS (QUOTE IGNORABLE) (CONS (QUOTE CONDITION) (QUOTE NIL))) (QUOTE NIL))) (CONS ON-FAIL (QUOTE NIL))))))))) NIL))) (DEFUN RAW-LOAD-UNCOMPILED (NAME ERROR-ON-FAIL ON-FAIL STATE) (COND ((NOT (MEMBER :CLTL2 *FEATURES*)) (LOAD (EXTEND-PATHNAME (CBD) NAME STATE))) (T (HANDLER-CASE (LOAD (EXTEND-PATHNAME (CBD) NAME STATE)) (ERROR (CONDITION) (IF ERROR-ON-FAIL (LET ((CONDITION-STR (FORMAT NIL "~a" CONDITION))) (ER HARD (QUOTE INCLUDE-RAW) "Load of ~x0 failed with the following message:~%~@1~%" NAME CONDITION-STR)) (EVAL (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE CONDITION) (CONS (CONS (QUOTE QUOTE) (CONS CONDITION (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE DECLARE) (CONS (CONS (QUOTE IGNORABLE) (CONS (QUOTE CONDITION) (QUOTE NIL))) (QUOTE NIL))) (CONS ON-FAIL (QUOTE NIL))))))))) NIL))) (DEFUN RAW-LOAD (NAME ERROR-ON-FAIL ON-FAIL STATE) (LET* ((FNAME (EXTEND-PATHNAME (CBD) NAME STATE)) (COMPILED-FNAME (COMPILE-FILE-PATHNAME FNAME))) (COND ((NOT (MEMBER :CLTL2 *FEATURES*)) (COND ((PROBE-FILE COMPILED-FNAME) (LOAD-COMPILED COMPILED-FNAME)) (T (FORMAT T "Compiled file ~a does not exist; loading uncompiled ~a~%" (NAMESTRING COMPILED-FNAME) FNAME) (RAW-LOAD-UNCOMPILED NAME ERROR-ON-FAIL ON-FAIL STATE)))) (T (HANDLER-CASE (LOAD-COMPILED COMPILED-FNAME) (ERROR (CONDITION) (PROGN (FORMAT T "Compiled file ~a did not load; loading uncompiled ~a.~%Message: ~a~%" (NAMESTRING COMPILED-FNAME) FNAME CONDITION) (RAW-LOAD-UNCOMPILED NAME ERROR-ON-FAIL ON-FAIL STATE)))))) NIL))) (RECORD-EXPANSION (MAKE-EVENT (MV-LET (ERP VAL STATE) (PROGN! (SET-RAW-MODE T) (LET ((*READTABLE* (IF NIL *HOST-READTABLE* *ACL2-READTABLE*))) (IF (OR (NOT (F-GET-GLOBAL (QUOTE CERTIFY-BOOK-INFO) STATE)) NIL) (MV NIL NIL STATE) (RAW-COMPILE "timer.lsp" T (QUOTE NIL) STATE)))) (DECLARE (IGNORE ERP VAL)) (VALUE (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (VALUE-TRIPLE :INVISIBLE)) (PROGN! (SET-RAW-MODE T) (LET ((*READTABLE* (IF NIL *HOST-READTABLE* *ACL2-READTABLE*))) (WHEN (NULL *HCOMP-FN-MACRO-RESTORE-HT*) (RAW-LOAD "timer.lsp" T (QUOTE NIL) STATE))) (VALUE-TRIPLE "timer.lsp")))) (4 RECORD-EXPANSION (INCLUDE-RAW "numargs.lsp") (PROGN (PROGN! (SET-RAW-MODE T) (DEFUN RAW-COMPILE (NAME ERROR-ON-FAIL ON-FAIL STATE) (COND ((NOT (MEMBER :CLTL2 *FEATURES*)) (COMPILE-FILE (EXTEND-PATHNAME (CBD) NAME STATE))) (T (HANDLER-CASE (COMPILE-FILE (EXTEND-PATHNAME (CBD) NAME STATE)) (ERROR (CONDITION) (IF ERROR-ON-FAIL (LET ((CONDITION-STR (FORMAT NIL "~a" CONDITION))) (ER HARD (QUOTE INCLUDE-RAW) "Compilation of ~x0 failed with the following message:~%~@1~%" NAME CONDITION-STR)) (EVAL (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE CONDITION) (CONS (CONS (QUOTE QUOTE) (CONS CONDITION (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE DECLARE) (CONS (CONS (QUOTE IGNORABLE) (CONS (QUOTE CONDITION) (QUOTE NIL))) (QUOTE NIL))) (CONS ON-FAIL (QUOTE NIL))))))))) NIL))) (DEFUN RAW-LOAD-UNCOMPILED (NAME ERROR-ON-FAIL ON-FAIL STATE) (COND ((NOT (MEMBER :CLTL2 *FEATURES*)) (LOAD (EXTEND-PATHNAME (CBD) NAME STATE))) (T (HANDLER-CASE (LOAD (EXTEND-PATHNAME (CBD) NAME STATE)) (ERROR (CONDITION) (IF ERROR-ON-FAIL (LET ((CONDITION-STR (FORMAT NIL "~a" CONDITION))) (ER HARD (QUOTE INCLUDE-RAW) "Load of ~x0 failed with the following message:~%~@1~%" NAME CONDITION-STR)) (EVAL (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE CONDITION) (CONS (CONS (QUOTE QUOTE) (CONS CONDITION (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE DECLARE) (CONS (CONS (QUOTE IGNORABLE) (CONS (QUOTE CONDITION) (QUOTE NIL))) (QUOTE NIL))) (CONS ON-FAIL (QUOTE NIL))))))))) NIL))) (DEFUN RAW-LOAD (NAME ERROR-ON-FAIL ON-FAIL STATE) (LET* ((FNAME (EXTEND-PATHNAME (CBD) NAME STATE)) (COMPILED-FNAME (COMPILE-FILE-PATHNAME FNAME))) (COND ((NOT (MEMBER :CLTL2 *FEATURES*)) (COND ((PROBE-FILE COMPILED-FNAME) (LOAD-COMPILED COMPILED-FNAME)) (T (FORMAT T "Compiled file ~a does not exist; loading uncompiled ~a~%" (NAMESTRING COMPILED-FNAME) FNAME) (RAW-LOAD-UNCOMPILED NAME ERROR-ON-FAIL ON-FAIL STATE)))) (T (HANDLER-CASE (LOAD-COMPILED COMPILED-FNAME) (ERROR (CONDITION) (PROGN (FORMAT T "Compiled file ~a did not load; loading uncompiled ~a.~%Message: ~a~%" (NAMESTRING COMPILED-FNAME) FNAME CONDITION) (RAW-LOAD-UNCOMPILED NAME ERROR-ON-FAIL ON-FAIL STATE)))))) NIL))) (RECORD-EXPANSION (MAKE-EVENT (MV-LET (ERP VAL STATE) (PROGN! (SET-RAW-MODE T) (LET ((*READTABLE* (IF NIL *HOST-READTABLE* *ACL2-READTABLE*))) (IF (OR (NOT (F-GET-GLOBAL (QUOTE CERTIFY-BOOK-INFO) STATE)) NIL) (MV NIL NIL STATE) (RAW-COMPILE "numargs.lsp" T (QUOTE NIL) STATE)))) (DECLARE (IGNORE ERP VAL)) (VALUE (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (VALUE-TRIPLE :INVISIBLE)) (PROGN! (SET-RAW-MODE T) (LET ((*READTABLE* (IF NIL *HOST-READTABLE* *ACL2-READTABLE*))) (WHEN (NULL *HCOMP-FN-MACRO-RESTORE-HT*) (RAW-LOAD "numargs.lsp" T (QUOTE NIL) STATE))) (VALUE-TRIPLE "numargs.lsp")))) (5 RECORD-EXPANSION (INCLUDE-RAW "pons.lsp") (PROGN (PROGN! (SET-RAW-MODE T) (DEFUN RAW-COMPILE (NAME ERROR-ON-FAIL ON-FAIL STATE) (COND ((NOT (MEMBER :CLTL2 *FEATURES*)) (COMPILE-FILE (EXTEND-PATHNAME (CBD) NAME STATE))) (T (HANDLER-CASE (COMPILE-FILE (EXTEND-PATHNAME (CBD) NAME STATE)) (ERROR (CONDITION) (IF ERROR-ON-FAIL (LET ((CONDITION-STR (FORMAT NIL "~a" CONDITION))) (ER HARD (QUOTE INCLUDE-RAW) "Compilation of ~x0 failed with the following message:~%~@1~%" NAME CONDITION-STR)) (EVAL (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE CONDITION) (CONS (CONS (QUOTE QUOTE) (CONS CONDITION (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE DECLARE) (CONS (CONS (QUOTE IGNORABLE) (CONS (QUOTE CONDITION) (QUOTE NIL))) (QUOTE NIL))) (CONS ON-FAIL (QUOTE NIL))))))))) NIL))) (DEFUN RAW-LOAD-UNCOMPILED (NAME ERROR-ON-FAIL ON-FAIL STATE) (COND ((NOT (MEMBER :CLTL2 *FEATURES*)) (LOAD (EXTEND-PATHNAME (CBD) NAME STATE))) (T (HANDLER-CASE (LOAD (EXTEND-PATHNAME (CBD) NAME STATE)) (ERROR (CONDITION) (IF ERROR-ON-FAIL (LET ((CONDITION-STR (FORMAT NIL "~a" CONDITION))) (ER HARD (QUOTE INCLUDE-RAW) "Load of ~x0 failed with the following message:~%~@1~%" NAME CONDITION-STR)) (EVAL (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE CONDITION) (CONS (CONS (QUOTE QUOTE) (CONS CONDITION (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE DECLARE) (CONS (CONS (QUOTE IGNORABLE) (CONS (QUOTE CONDITION) (QUOTE NIL))) (QUOTE NIL))) (CONS ON-FAIL (QUOTE NIL))))))))) NIL))) (DEFUN RAW-LOAD (NAME ERROR-ON-FAIL ON-FAIL STATE) (LET* ((FNAME (EXTEND-PATHNAME (CBD) NAME STATE)) (COMPILED-FNAME (COMPILE-FILE-PATHNAME FNAME))) (COND ((NOT (MEMBER :CLTL2 *FEATURES*)) (COND ((PROBE-FILE COMPILED-FNAME) (LOAD-COMPILED COMPILED-FNAME)) (T (FORMAT T "Compiled file ~a does not exist; loading uncompiled ~a~%" (NAMESTRING COMPILED-FNAME) FNAME) (RAW-LOAD-UNCOMPILED NAME ERROR-ON-FAIL ON-FAIL STATE)))) (T (HANDLER-CASE (LOAD-COMPILED COMPILED-FNAME) (ERROR (CONDITION) (PROGN (FORMAT T "Compiled file ~a did not load; loading uncompiled ~a.~%Message: ~a~%" (NAMESTRING COMPILED-FNAME) FNAME CONDITION) (RAW-LOAD-UNCOMPILED NAME ERROR-ON-FAIL ON-FAIL STATE)))))) NIL))) (RECORD-EXPANSION (MAKE-EVENT (MV-LET (ERP VAL STATE) (PROGN! (SET-RAW-MODE T) (LET ((*READTABLE* (IF NIL *HOST-READTABLE* *ACL2-READTABLE*))) (IF (OR (NOT (F-GET-GLOBAL (QUOTE CERTIFY-BOOK-INFO) STATE)) NIL) (MV NIL NIL STATE) (RAW-COMPILE "pons.lsp" T (QUOTE NIL) STATE)))) (DECLARE (IGNORE ERP VAL)) (VALUE (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (VALUE-TRIPLE :INVISIBLE)) (PROGN! (SET-RAW-MODE T) (LET ((*READTABLE* (IF NIL *HOST-READTABLE* *ACL2-READTABLE*))) (WHEN (NULL *HCOMP-FN-MACRO-RESTORE-HT*) (RAW-LOAD "pons.lsp" T (QUOTE NIL) STATE))) (VALUE-TRIPLE "pons.lsp")))))
(("/usr/share/acl2-6.3/books/memoize/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1050774381))
(("/usr/share/acl2-6.3/books/memoize/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:MEMOIZE "/usr/share/acl2-6.3/books/memoize/top.lisp"))) . 1920644264) ("/usr/share/acl2-6.3/books/tools/include-raw.lisp" "tools/include-raw" "include-raw" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 438153625) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/memoize/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1050774381))
699487110