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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
|
; Utility for finding theorems defined non-redundantly in a book or encapsulate
; Copyright (C) 2014, Regents of the University of Texas
; Written by Matt Kaufmann (original date October, 2007; augmented January, 2011)
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; Modified by Jared Davis, October 2014, to add support for raw documentation
; strings in defsections.
; This file first introduces two utilities, which require that the indicated
; book already be included when running them.
; (theorems-introduced-in "book-name" state)
; returns a list of names of all the theorems (i.e. defthm event names) and
; axioms (i.e., defaxiom event names) introduced in the book or its
; certifification world (portcullis), not including those introduced in
; sub-books.
; (book-thms "book-name" translated-p)
; is similar to the above, but returns an alist associating names with their
; formulas (in translated form if translated-p is t, but untranslated if
; translated-p is nil).
; Then, this file introduces utilities for collecting and displaying formulas
; introduced by a sequence of events. The main macro at the user level is
; encapsulate-then-new-info, but users may want something different, and the
; underlying utility new-formula-info suggests how to build other such macros.
; Thanks to Jared Davis for requesting and trying out this book.
; See book-thms-example.lisp for an example of the usage of these utilities.
(in-package "ACL2")
(program)
(defun newly-defined-top-level-thms-rec (trips collect-p full-book-name acc
translated-p)
; See newly-defined-top-level-fns-rec in the sources. Translated-p is true if
; we want translated theorems, else is false.
(cond ((endp trips)
acc)
((and (eq (caar trips) 'include-book-path)
(eq (cadar trips) 'global-value))
(newly-defined-top-level-thms-rec (cdr trips)
(equal (car (cddar trips))
full-book-name)
full-book-name
acc
translated-p))
((not collect-p)
(newly-defined-top-level-thms-rec (cdr trips) nil full-book-name acc
translated-p))
((eq (cadar trips) (if translated-p 'theorem 'untranslated-theorem))
(newly-defined-top-level-thms-rec
(cdr trips)
collect-p
full-book-name
(acons (caar trips) (cddar trips) acc)
translated-p))
(t
(newly-defined-top-level-thms-rec (cdr trips) collect-p full-book-name
acc translated-p))))
(defun reversed-world-since-event (wrld ev acc)
(cond ((or (endp wrld)
(let ((trip (car wrld)))
(and (eq (car trip) 'event-landmark)
(eq (cadr trip) 'global-value)
(equal (access-event-tuple-form (cddr trip)) ev))))
acc)
(t (reversed-world-since-event (cdr wrld)
ev
(cons (car wrld) acc)))))
(defun reversed-world-since-boot-strap (wrld)
(reversed-world-since-event wrld '(exit-boot-strap-mode) nil))
(defun book-thms-fn (book-name translated-p state)
; This function assumes that book-name has already been included. Translated-p
; is true if we want translated theorems, else is false.
(declare (xargs :stobjs state))
(mv-let
(full-book-name directory-name familiar-name)
(parse-book-name (cbd) book-name ".lisp" 'book-thms state)
(declare (ignore directory-name familiar-name))
(newly-defined-top-level-thms-rec
(reversed-world-since-boot-strap (w state))
nil
full-book-name
nil
translated-p)))
(defmacro book-thms (book-name translated-p)
; This macro assumes that book-name has already been included. Translated-p is
; true if we want translated theorems, else is false.
`(book-thms-fn ,book-name ,translated-p state))
(defun theorems-introduced-in (book-name state)
; This function assumes that book-name has already been included. Translated-p
; is true if we want translated theorems, else is false.
(declare (xargs :stobjs state))
(strip-cars (book-thms-fn book-name t state)))
;;; Section: New axioms and theorems after executing events, e.g., an
;;; encapsulate
; Below we collect up the new formulas introduced by a sequence of events. We
; do not include information on events that don't introduce formulas, such as
; table events or deflabel events. That wouldn't be difficult to do, but the
; current view is formula-based rather than event-based, so presentation might
; be an issue.
(table acl2-xdoc)
(defmacro acl2-xdoc-fragment (msg)
`(progn
;; Originally I didn't have this extra setting of :fragment to NIL, but
;; that can lead to doc fragments being redundant with one another. This
;; was really confusing when dong the bitops/merge documentation where the
;; fragments were copied and pasted from one function to the next.
;; Anyway, setting the fragment to NIL makes sure that the next message
;; won't be redundant.
(table acl2-xdoc :fragment nil)
(table acl2-xdoc :fragment ,msg)))
; We collect into acc entries of the following forms, using untranslated
; (user-level) syntax for formulas.
; - (name :theorem thm)
; for (defthm name thm ...)
; - (name :def (equal (name . formals) body))
; for (defun name formals ... body)
; - ((name1 ... namek) :constraint formula)
; for names (name1 ... namek) introduced with the indicated constraint
; formula
; - (name :defchoose formula)
; for name introduced by defchoose with the indicated constraint
; - "blah"
; for calls of (acl2-xdoc-fragment "blah")
; Remarks:
; (1) Definitions in a mutual-recursion are listed separately.
; (2) We don't check for which may leave properties *acl2-property-unbound*, so
; we are not handling redefinition,
; (3) Defun-sk is implemented with encapsulate and a local defchoose, so one
; will see a :constrain tuple rather than :defchoose tuple in this case.
; (4) Unlike the function newly-defined-top-level-fns-rec, we give no special
; treatment for include-book. Events from a subsidiary book that are
; represented in trips will be considered. However, typically trips may come
; from (pass 2 of) an encapsulate event, in which case there are no
; include-book events represented (since any such are local to the
; encapsulate).
(defun new-formula-info1 (trip wrld acc)
(let ((name (car trip))
(prop (cddr trip)))
(case (cadr trip)
(theorem
(cons (list name :theorem prop) acc))
(unnormalized-body
(cond ((eq (getprop name 'constraint-lst t 'current-acl2-world wrld) t)
(cons (list name
:def
`(equal (,name ,@(formals name wrld))
,(untranslate prop nil wrld)))
acc))
(t ; function is really constrained
acc)))
(constraint-lst
(cond ((and prop (symbolp prop))
acc)
(t
(cons (list (getprop name 'siblings nil 'current-acl2-world wrld)
:constraint
(untranslate (cons 'and prop) t wrld))
acc))))
(defchoose-axiom
(cons (list name :defchoose (untranslate prop t wrld))
acc))
(global-value
(if (and (eq name 'event-landmark)
(eq (access-event-tuple-type prop) 'table))
(let ((form (access-event-tuple-form prop)))
(if (and (eq (first form) 'table)
(eq (second form) 'acl2-xdoc)
(eq (third form) :fragment)
(stringp (fourth form)))
(cons (fourth form) acc)
acc))
acc))
(t acc))))
(defun new-formula-info (trips wrld acc)
(if (endp trips)
acc
(let ((acc (new-formula-info1 (car trips) wrld acc)))
(new-formula-info (cdr trips) wrld acc))))
(defmacro with-intro-table (&rest events)
; Events is a list of events. We wrap events in a progn that concludes with an
; additional event, a table mapping :info to the information collected by
; new-formula-info (see the comments there) for the indicated events.
(let ((marker ; lay down a non-redundant marker
'(table intro-table :mark world)))
`(progn
,marker
,@events
(make-event
(let* ((wrld (w state))
(trips (reversed-world-since-event wrld ',marker nil))
(info (reverse (new-formula-info trips wrld nil))))
`(table intro-table :info ',info))))))
(defmacro encapsulate-then-new-info (name &rest events)
; Events is a list of events. We wrap events into an (encapsulate () ...) and
; follow that with a zero-ary definition of name, which returns information of
; the sort discussed above (see comments in new-formula-info).
(declare (xargs :guard (and name (symbolp name))))
`(progn (with-intro-table
(encapsulate
()
,@events))
(make-event
(let ((wrld (w state)))
(list 'defun ',name nil
(list 'quote
(cdr (assoc-eq :info (table-alist 'intro-table
wrld)))))))))
#||
;; for testing:
(encapsulate-then-new-info foo
(defun f (x) x)
(acl2-xdoc-fragment "Hello")
(defun f2 (x) x)
(acl2-xdoc-fragment "World")
(defun f3 (x) x))
||#
|
