/usr/share/acl2-7.2dfsg/books/make-event/macros-include.lisp is in acl2-books-source 7.2dfsg-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 | ; This book checks that expansions are stored as expected. The constant
; *macros-expansion-alist* below is what we expect to find for the
; :expansion-alist field of macros.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 macros.cert.
(defconst *macros-expansion-alist*
'((2 RECORD-EXPANSION
(MY-MAC (MAKE-EVENT '(DEFUN FOO (X) X)))
(DEFUN FOO (X) X))
(3 RECORD-EXPANSION
(MY-MAC (MAKE-EVENT '(DEFUN FOO (X) X)
:CHECK-EXPANSION T))
(MAKE-EVENT '(DEFUN FOO (X) X)
:CHECK-EXPANSION (DEFUN FOO (X) X)))
(4
RECORD-EXPANSION
(ENCAPSULATE ((LOCAL-FN (X) T))
(LOCAL (DEFUN LOCAL-FN (X) X))
(MY-MAC (MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION T)))
(ENCAPSULATE
((LOCAL-FN (X) T))
(LOCAL (DEFUN LOCAL-FN (X) X))
(RECORD-EXPANSION (MY-MAC (MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION T))
(MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION (DEFUN FOO2 (X) X)))))
(5 RECORD-EXPANSION
(ENCAPSULATE NIL
(MY-MAC (MAKE-EVENT '(DEFUN FOO3 (X) X))))
(ENCAPSULATE NIL
(RECORD-EXPANSION (MY-MAC (MAKE-EVENT '(DEFUN FOO3 (X) X)))
(DEFUN FOO3 (X) X))))
(7
RECORD-EXPANSION
(ENCAPSULATE ((LOCAL-FN (X) T))
(LOCAL (DEFUN LOCAL-FN (X) X))
(MY-MAC (MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION T)))
(ENCAPSULATE
((LOCAL-FN (X) T))
(LOCAL (DEFUN LOCAL-FN (X) X))
(RECORD-EXPANSION (MY-MAC (MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION T))
(MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION (DEFUN FOO2 (X) X)))))
(8
RECORD-EXPANSION
(ENCAPSULATE ((LOCAL-FN (X) T))
(LOCAL (DEFUN LOCAL-FN (X) X))
(MY-MAC (MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION T)))
(ENCAPSULATE
((LOCAL-FN (X) T))
(LOCAL (DEFUN LOCAL-FN (X) X))
(RECORD-EXPANSION (MY-MAC (MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION T))
(MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION (DEFUN FOO2 (X) X)))))
(10 RECORD-EXPANSION
(MUST-FAIL (ENCAPSULATE ((LOCAL-FN (X) T))
(LOCAL (DEFUN LOCAL-FN (X) X))
(MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION T)))
(WITH-OUTPUT :OFF
:ALL (VALUE-TRIPLE 'T)))
(11
RECORD-EXPANSION
(MUST-FAIL
(ENCAPSULATE ((LOCAL-FN (X) T))
(LOCAL (DEFUN LOCAL-FN (X) X))
(MY-MAC (MAKE-EVENT '(DEFUN FOO2 (X) X)
:CHECK-EXPANSION (DEFUN FOO2 (X) X)))))
(WITH-OUTPUT :OFF
:ALL (VALUE-TRIPLE 'T)))))
; Include the book whose certificate we want to check.
(include-book "macros")
; Define must-succeed (used below).
(include-book "misc/eval" :dir :system)
; Define read-list (used below).
(include-book "misc/file-io" :dir :system)
; Check that *macros-expansion-alist*, defined above, is equal to the
; :expansion-alist field of the certificate of the "macros" book. Skip the
; check if we might be doing provisional certification (not the default
; anyhow), since locals are elided more aggressively in that case.
(must-succeed
(cond
((member-eq (cert-op state)
'(:create-pcert :convert-pcert))
(value t))
(t (er-let* ((forms (read-list "macros.cert" 'top state)))
(let ((erp (not (equal (cadr (member-eq :expansion-alist forms))
*macros-expansion-alist*))))
(mv erp nil state))))))
|