/usr/share/acl2-4.3/books/make-event/local-elided-include.lisp is in acl2-books-source 4.3-3.
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 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 | ; This book checks that expansions are stored as expected. The constant below
; is what we expect to find for the :expansion-alist field of
; local-elided.cert. The last form in this file shows how we can do useful
; file IO on behalf of a make-event.
(in-package "ACL2")
; Here is the expected :expansion-alist from local-elided.cert.
(defconst *local-elided-expansion-alist*
'((1 RECORD-EXPANSION
(LOCAL (MAKE-EVENT '(DEFUN FOO (X) X)))
(LOCAL (VALUE-TRIPLE :ELIDED)))
(2 RECORD-EXPANSION
(MAKE-EVENT '(LOCAL (DEFUN FOO (X) X)))
(LOCAL (VALUE-TRIPLE :ELIDED)))
(3 RECORD-EXPANSION
(MAKE-EVENT '(LOCAL (DEFUN FOO-2 (X) X)))
(LOCAL (VALUE-TRIPLE :ELIDED)))
(5
RECORD-EXPANSION
(PROGN
(MAKE-EVENT '(LOCAL (DEFUN G (X) X)))
(LOCAL (DEFUN G2 (X) X))
(MAKE-EVENT (VALUE '(ENCAPSULATE ((BAR2 (X) T))
(LOCAL (DEFUN BAR2 (X) (FOO X)))
(DEFTHM BAR2-PRESERVES-CONSP
(IMPLIES (CONSP X)
(CONSP (BAR2 X))))))))
(PROGN
(RECORD-EXPANSION (MAKE-EVENT '(LOCAL (DEFUN G (X) X)))
(LOCAL (VALUE-TRIPLE :ELIDED)))
(LOCAL (VALUE-TRIPLE :ELIDED))
(RECORD-EXPANSION
(MAKE-EVENT
(VALUE '(ENCAPSULATE ((BAR2 (X) T))
(LOCAL (DEFUN BAR2 (X) (FOO X)))
(DEFTHM BAR2-PRESERVES-CONSP
(IMPLIES (CONSP X) (CONSP (BAR2 X)))))))
(ENCAPSULATE ((BAR2 (X) T))
(LOCAL (DEFUN BAR2 (X) (FOO X)))
(DEFTHM BAR2-PRESERVES-CONSP
(IMPLIES (CONSP X)
(CONSP (BAR2 X))))))))
(6
RECORD-EXPANSION
(MAKE-EVENT
(VALUE '(ENCAPSULATE ((BAR2 (X) T))
(LOCAL (DEFUN BAR2 (X) (FOO X)))
(DEFTHM BAR2-PRESERVES-CONSP
(IMPLIES (CONSP X) (CONSP (BAR2 X)))))))
(ENCAPSULATE ((BAR2 (X) T))
(LOCAL (DEFUN BAR2 (X) (FOO X)))
(DEFTHM BAR2-PRESERVES-CONSP
(IMPLIES (CONSP X) (CONSP (BAR2 X))))))
(7
RECORD-EXPANSION
(MAKE-EVENT
(VALUE '(ENCAPSULATE ((BAR3 (X) T))
(MAKE-EVENT '(LOCAL (DEFUN BAR3 (X) (FOO X))))
(DEFTHM BAR3-PRESERVES-CONSP
(IMPLIES (CONSP X) (CONSP (BAR3 X)))))))
(ENCAPSULATE
((BAR3 (X) T))
(RECORD-EXPANSION (MAKE-EVENT '(LOCAL (DEFUN BAR3 (X) (FOO X))))
(LOCAL (VALUE-TRIPLE :ELIDED)))
(DEFTHM BAR3-PRESERVES-CONSP
(IMPLIES (CONSP X) (CONSP (BAR3 X))))))
(8 RECORD-EXPANSION
(ENCAPSULATE ((BAR3 (X) T))
(MAKE-EVENT '(LOCAL (DEFUN BAR3 (X) (FOO X))))
(DEFTHM BAR3-PRESERVES-CONSP
(IMPLIES (CONSP X) (CONSP (BAR3 X)))))
(ENCAPSULATE
((BAR3 (X) T))
(RECORD-EXPANSION (MAKE-EVENT '(LOCAL (DEFUN BAR3 (X) (FOO X))))
(LOCAL (VALUE-TRIPLE :ELIDED)))
(DEFTHM BAR3-PRESERVES-CONSP
(IMPLIES (CONSP X) (CONSP (BAR3 X))))))
(10 RECORD-EXPANSION
(MUST-FAIL (ENCAPSULATE ((BAR3 (X) T))
(LOCAL (DEFUN BAR3 (X) (FOO X)))
(DEFTHM BAR3-PRESERVES-CONSP
(IMPLIES (CONSP X) (CONSP (BAR3 X))))))
(VALUE-TRIPLE 'T))
(11 RECORD-EXPANSION
(MAKE-EVENT '(DEFUN FOO-3 (X) X))
(DEFUN FOO-3 (X) X))
(13
RECORD-EXPANSION
(ENCAPSULATE NIL (MY-LOCAL (DEFUN G3 (X) X))
(MAKE-EVENT '(MY-LOCAL (DEFUN G3 (X) X)))
(MAKE-EVENT '(MY-LOCAL (DEFUN G4 (X) X)))
(MY-LOCAL (DEFUN G4 (X) X))
(PROGN (MY-LOCAL (DEFUN G5 (X) X))
(MY-LOCAL (MAKE-EVENT (VALUE '(DEFUN G6 (X) X))))))
(ENCAPSULATE
NIL (MY-LOCAL (DEFUN G3 (X) X))
(RECORD-EXPANSION (MAKE-EVENT '(MY-LOCAL (DEFUN G3 (X) X)))
(LOCAL (VALUE-TRIPLE :ELIDED)))
(RECORD-EXPANSION (MAKE-EVENT '(MY-LOCAL (DEFUN G4 (X) X)))
(LOCAL (VALUE-TRIPLE :ELIDED)))
(MY-LOCAL (DEFUN G4 (X) X))
(RECORD-EXPANSION
(PROGN (MY-LOCAL (DEFUN G5 (X) X))
(MY-LOCAL (MAKE-EVENT (VALUE '(DEFUN G6 (X) X)))))
(PROGN
(MY-LOCAL (DEFUN G5 (X) X))
(RECORD-EXPANSION (MY-LOCAL (MAKE-EVENT (VALUE '(DEFUN G6 (X) X))))
(LOCAL (VALUE-TRIPLE :ELIDED)))))))))
; Include the book whose certificate we want to check.
(include-book "local-elided")
; Define must-succeed (used below).
(include-book "eval")
; Define read-list (used below).
(include-book "misc/file-io" :dir :system)
; Check that the above constant is equal to the :expansion-alist field of the
; certificate of the "local-elided" book.
(must-succeed
(er-let* ((forms (read-list "local-elided.cert" 'top state)))
(let ((erp (not (equal (cadr (member-eq :expansion-alist forms))
*local-elided-expansion-alist*))))
(mv erp nil state))))
|