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))))))
|
