1(in-package "ACL2")
2
3; In what follows, logic-only means that we only want events with logical
4; content, such as defaxiom, defthm, and logic-mode defun (and defund) forms,
5; but not including program-mode definitions, table events, etc.
6
7; We drop local forms, regardless of logic-only.
8
9; Either way, we drop all hints.  That could be changed.
10
11(program)
12(set-state-ok t)
13
14(defun read-portcullis-cmds1 (chan cert-file ctx state acc)
15  (mv-let (eofp form state)
16          (read-object chan state)
17          (cond (eofp (er soft ctx
18                          "Reached end of file ~x0 before reaching ~
19                           :END-PORTCULLIS-CMDS."
20                          cert-file))
21                ((eq form :END-PORTCULLIS-CMDS)
22                 (if (eq acc :start)
23                     (er soft ctx
24                         "In file ~x0, reached :END-PORTCULLIS-CMDS before ~
25                          reaching :BEGIN-PORTCULLIS-CMDS."
26                          cert-file)
27                   (value (reverse acc))))
28                ((eq form :BEGIN-PORTCULLIS-CMDS)
29                 (if (eq acc :start)
30                     (read-portcullis-cmds1 chan cert-file ctx state nil)
31                   (er soft ctx
32                       "In file ~x0, reached :BEGIN-PORTCULLIS-CMDS twice."
33                       cert-file)))
34                ((eq acc :start)
35                 (read-portcullis-cmds1 chan cert-file ctx state acc))
36                (t (read-portcullis-cmds1 chan cert-file ctx state
37                                          (cons form acc))))))
38
39(defun read-portcullis-cmds (book-name cert-optional-p ctx state)
40  (let ((cert-file (concatenate 'string
41                                (extend-pathname (cbd) book-name state)
42                                ".cert")))
43    (mv-let (chan state)
44            (open-input-channel cert-file :object state)
45            (cond ((null chan)
46                   (if cert-optional-p
47                       (value nil)
48                     (er soft ctx
49                         "Unable to open certificate file ~x0."
50                         cert-file)))
51                  (t (mv-let
52                      (erp forms state)
53                      (read-portcullis-cmds1 chan cert-file ctx state :start)
54                      (pprogn (close-input-channel chan state)
55                              (cond (erp (mv erp forms state))
56                                    (t (value forms))))))))))
57
58(defun expand-to-event (form ctx state)
59  (let ((orig-form form)
60        (wrld (w state))
61        (names
62
63; Warning: If you add a name here, handle it in essential-events (and hence
64; perhaps essential-basic-event).
65
66         (list* 'defun-sk ; given custom handling here
67                'in-package
68                'defpkg
69
70; The following for translating axioms.lisp; you won't find them in a book.
71
72                'value 'set-ld-skip-proofsp
73                (primitive-event-macros)))
74        (portcullisp nil)     ; ok to be generous
75        (in-local-flg nil)    ; ok to be generous
76        (in-encapsulatep nil) ; ok to be generous
77        (make-event-chk nil)  ; we will handle make-event issues ourselves
78        )
79    (chk-embedded-event-form form orig-form wrld ctx state names portcullisp
80                             in-local-flg in-encapsulatep make-event-chk)))
81
82(defmacro internal-error (ctx string &rest args)
83  `(er soft ,ctx
84       "Internal error: ~@0"
85       (msg ,string ,@args)))
86
87(defun essential-basic-event (form ctx state)
88  (declare (xargs :guard (true-listp form)))
89  (let* ((name (cadr form))
90         (wrld (w state))
91         (event-type (car form)))
92    (case event-type
93      ((defun defun-sk)
94       (cond
95        ((eq (defun-mode name wrld) :logic)
96         (let ((tbody (getprop name 'unnormalized-body nil 'current-acl2-world
97                               wrld)))
98           (cond ((null tbody)
99                  (internal-error
100                   ctx
101                   "Missing 'unnormalized-body property for ~x0."
102                   name))
103                 ((eq event-type 'defun)
104                  (value (list 'defun name (caddr form) tbody)))
105                 (t
106                  (case-match form
107                    (('defun-sk !name formals
108                       (quant vars &) . &)
109                     (let ((vars
110                            (if (symbolp vars) (list vars) vars)))
111                       (cond
112                        ((null (cdr vars))
113                         (case-match tbody
114                           (('prog2$ ('throw-nonexec-error . &)
115                                     (('lambda & matrix) . &))
116                            (value (list 'defun-sk name formals
117                                         (list quant vars matrix))))
118                           (& (internal-error ctx
119                                              "Unexpected form of ~
120                                             'unnormalized-body property for ~
121                                             ~x0:~|~%  ~x1"
122                                              name tbody))))
123                        (t ; at least two vars
124                         (case-match tbody
125                           (('prog2$ ('throw-nonexec-error . &)
126                                     (('lambda ('mv . &)
127                                        (('lambda & matrix) . &))
128                                      . &))
129                            (value (list 'defun-sk name formals
130                                         (list quant vars matrix))))
131                           (& (internal-error ctx
132                                              "Unexpected form of ~
133                                             'unnormalized-body property for ~
134                                             ~x0:~|~%  ~x1"
135                                              name tbody)))))))
136                    (& (internal-error ctx
137                                       "Expected defun-sk of a certain form, ~
138                                        but got:~|~%  ~x1."
139                                       name
140                                       form)))))))
141        (t
142; Don't cause an error -- maybe we needed this function in order to define
143; macros or constants.
144         (value nil))))
145      ((defaxiom defthm)
146       (let ((tbody (getprop name 'theorem nil 'current-acl2-world wrld)))
147         (value (and tbody
148                     (list event-type
149                           (cadr form)
150                           tbody)))))
151      (defpkg
152        (let ((pkg-entry (assoc-equal name
153                                      (known-package-alist
154                                       state))))
155          (cond (pkg-entry (value (list event-type
156                                        (cadr form)
157                                        (kwote (package-entry-imports
158                                                pkg-entry)))))
159                (t (internal-error
160                    ctx
161                    "Missing package entry for ~x0 in the ~
162                              known-package-alist."
163                    name)))))
164      (in-package (value form))
165      (include-book
166
167; !! Should we deal with :ttags too?
168
169       (let* ((kwd-args (cddr form))
170              (dir (cadr (assoc-keyword :dir kwd-args))))
171         (cond
172          ((eq dir :system)
173           (value `(include-book ,(cadr form) :dir :system)))
174          (dir
175
176; Warning: Keep the following in sync with ACL2 source function
177; include-book-fn.
178
179           (er-let*
180            ((dir-value
181              (include-book-dir-with-chk soft ctx dir)))
182            (mv-let
183             (full-book-name directory-name familiar-name)
184             (parse-book-name dir-value (cadr form) ".lisp" state)
185             (declare (ignore directory-name familiar-name))
186             (value `(include-book ,full-book-name)))))
187          (t (value `(include-book ,(cadr form)))))))
188      (otherwise (er soft ctx
189                     "Unexpected form type in ~x0: ~x1"
190                     'essential-basic-event form)))))
191
192(defun cons-to-all (a x)
193  (declare (xargs :guard (true-listp x)))
194  (cond ((endp x) nil)
195        (t (cons (cons a (car x))
196                 (cons-to-all a (cdr x))))))
197
198(defun fix-signature (sig)
199
200; Convert a signature to a list (fn . arity).
201
202  (declare (xargs :guard t))
203  (case-match sig
204    (((name . formals) . &)
205     (list name (length formals)))
206    ((name formals . &)
207     (list name (length formals)))
208    (& (er hard 'fix-signature
209           "Unexpexpected signature, ~x0"
210           sig))))
211
212(defun fix-signatures (sigs)
213  (declare (xargs :guard (true-listp sigs)))
214  (cond ((endp sigs) nil)
215        (t (cons (fix-signature (car sigs))
216                 (fix-signatures (cdr sigs))))))
217
218(defun essential-events (forms acc ctx state)
219
220; Warning: state global 'ld-skip-proofsp should be 'local before calling this
221; function.
222
223  (cond
224   ((atom forms)
225    (value (reverse acc)))
226   (t
227    (er-let*
228     ((form (expand-to-event (car forms) ctx state)))
229     (cond
230      ((null form)
231       (essential-events (cdr forms) acc ctx state))
232      (t
233       (case (car form)
234         (progn
235           (essential-events (append (cdr form) (cdr forms)) acc ctx state))
236         (with-output
237          (essential-events (cons (car (last form)) (cdr forms)) acc ctx state))
238         (skip-proofs ; !! special annotation needed?
239          (essential-events (cons (cadr form) (cdr forms)) acc ctx state))
240         (make-event
241          (let ((exp (cadr (assoc-keyword :check-expansion (cddr form)))))
242            (cond ((consp exp)
243                   (essential-events (cons exp (cdr forms)) acc ctx state))
244                  (t
245                   (er soft ctx
246                       "Encountered make-event form without expansion stored ~
247                        in :check-expansion field, which we cannot currently ~
248                        handle:~|~%~x0"
249                       form)))))
250         (encapsulate
251          (let ((signatures (cadr form)))
252            (cond (signatures
253                   (er-let*
254                    ((events (essential-events (cddr form) nil ctx state)))
255                    (essential-events (cdr forms)
256                                      (cons (list* 'encap
257                                                   (fix-signatures (cadr form))
258                                                   events)
259                                            acc)
260                                      ctx state)))
261                  (t (essential-events (append (cddr form) (cdr forms)) acc ctx
262                                       state)))))
263         ((mutual-recursion defuns)
264          (let ((defs (if (eq (car form) 'mutual-recursion)
265                          (cdr form)
266                        (cons-to-all 'defun (cdr form)))))
267            (er-let*
268             ((events (essential-events defs nil ctx state)))
269             (essential-events (cdr forms)
270                               (if events
271                                   (cons (cons 'mutual-recursion events) acc)
272                                 acc)
273                               ctx state))))
274         ((defun defthm defaxiom in-package defpkg include-book defun-sk)
275          (er-let* ((new-form (essential-basic-event form ctx state)))
276                   (essential-events (cdr forms)
277                                     (if new-form (cons new-form acc) acc)
278                                     ctx
279                                     state)))
280         (table
281
282; Even :program mode event can be skipped.  We'll check modes in
283; essential-basic-event.
284
285          (essential-events (cdr forms) acc ctx state))
286         (
287
288; We want to cause an error for every remaining event that has logical content.
289; (But we are handling the defun-mode already, so we can skip (logic) and
290; (program).)  The following is the value of the following expression after
291; (push :non-standard-analysis *features*).  With this approach, if ACL2 later
292; contains new logical events that we use then we will see an error.  If we
293; used the other possible parity, taking the short list below as teh list on
294; which to cause an error, then we would miss that additional logical event
295; rather than causing an error.
296#||
297 (set-difference-eq (primitive-event-macros)
298                    '(#+:non-standard-analysis
299                      defun-std
300                      #+:non-standard-analysis
301                      defthm-std
302                      defstobj
303                      defchoose
304                      progn!
305                      defttag))
306||#
307
308          (value set-ld-skip-proofsp ; see expand-to-event
309           DEFUN MUTUAL-RECURSION DEFUNS DEFTHM DEFAXIOM
310           DEFCONST DEFLABEL DEFDOC DEFTHEORY
311           VERIFY-GUARDS DEFMACRO IN-THEORY
312           IN-ARITHMETIC-THEORY PUSH-UNTOUCHABLE
313           REMOVE-UNTOUCHABLE RESET-PREHISTORY
314           SET-BODY TABLE PROGN ENCAPSULATE
315           INCLUDE-BOOK ADD-CUSTOM-KEYWORD-HINT
316           ADD-INCLUDE-BOOK-DIR
317           DELETE-INCLUDE-BOOK-DIR
318           COMP VERIFY-TERMINATION VERIFY-TERMINATION-BOOT-STRAP
319           ADD-MATCH-FREE-OVERRIDE
320           THEORY-INVARIANT LOGIC PROGRAM
321           ADD-DEFAULT-HINTS! REMOVE-DEFAULT-HINTS!
322           SET-MATCH-FREE-DEFAULT
323           SET-ENFORCE-REDUNDANCY
324           SET-VERIFY-GUARDS-EAGERNESS
325           SET-NON-LINEARP
326           SET-COMPILE-FNS SET-MEASURE-FUNCTION
327           SET-WELL-FOUNDED-RELATION
328           SET-INVISIBLE-FNS-TABLE
329           SET-BACKCHAIN-LIMIT
330           SET-BOGUS-DEFUN-HINTS-OK
331           SET-BOGUS-MUTUAL-RECURSION-OK
332           SET-DEFAULT-BACKCHAIN-LIMIT
333           SET-IRRELEVANT-FORMALS-OK
334           SET-IGNORE-OK SET-INHIBIT-WARNINGS
335           SET-STATE-OK SET-LET*-ABSTRACTIONP
336           SET-NU-REWRITER-MODE
337           SET-CASE-SPLIT-LIMITATIONS
338           SET-DEFAULT-HINTS!
339           SET-REWRITE-STACK-LIMIT VALUE-TRIPLE
340           defattach)
341          (essential-events (cdr forms) acc ctx state))
342         (otherwise
343          (er soft ctx
344              "~x0 is not yet implemented, hence the following form is ~
345               illegal:~|~%  ~x1"
346              (car form)
347              (car forms))))))))))
348
349(defun print-objects-pretty-rec (lst ch state)
350  (cond ((null lst) state)
351        (t (mv-let (col state)
352                   (fmt1 "~X01~|"
353                         (list (cons #\0 (car lst)) (cons #\1 nil))
354                         0 ch state nil)
355                   (declare (ignore col))
356                   (pprogn (if (cdr lst)
357                               (newline ch state)
358                             state)
359                           (print-objects-pretty-rec (cdr lst) ch state))))))
360
361(defun print-objects-pretty (lst ch state)
362  (mv-let (erp val state)
363          (state-global-let* ((write-for-read t))
364                             (pprogn (print-objects-pretty-rec lst ch state)
365                                     (value :invisible)))
366          (declare (ignore erp val))
367          state))
368
369(defun set-ld-skip-proofsp-state (val state)
370  (mv-let (erp x state)
371          (set-ld-skip-proofsp val state)
372          (declare (ignore erp x))
373          state))
374
375(defun print-book-essence (book-name infile outfile cert-optional-p ctx state)
376  (state-global-let*
377   ((ld-skip-proofsp 'include-book set-ld-skip-proofsp-state))
378   (er-let*
379       ((portcullis-cmds
380         (if (eq cert-optional-p :skip)
381             (value nil)
382           (read-portcullis-cmds book-name cert-optional-p ctx state)))
383        (forms (read-object-file infile ctx state))
384        (events1 (essential-events portcullis-cmds nil ctx
385                                   state))
386        (events2 (essential-events forms nil ctx state)))
387     (mv-let (chan state)
388             (open-output-channel outfile :object state)
389             (cond ((null chan)
390                    (er soft ctx
391                        "Unable to open file ~x0 for output."
392                        outfile))
393                   (t (pprogn
394                       (print-objects-pretty events1 chan state)
395                       (cond (events1
396                              (pprogn
397                               (newline chan state)
398                               (princ$ "; NOTE: Only the forms above are evaluated (as opposed the ones below,"
399                                       chan state)
400                               (newline chan state)
401                               (princ$ "; which merely are read) when translating to ML."
402                                       chan state)))
403                             (t state))
404                       (assert$
405                        (and (consp (car events2))
406                             (eq (caar events2) 'in-package))
407                        (cond
408                         ((equal (cadar events2) "ACL2") state)
409                         (t
410                          (pprogn
411                           (assert$
412                            events1 ; else we could not have a new package here
413                            (princ$ "  On a related note:"
414                                    chan state))
415                           (newline chan state)
416                           (princ$ "; the following IN-PACKAGE form is for use by a2ml, but all forms in"
417                                   chan state)
418                           (newline chan state)
419                           (princ$ "; this file assume that the current package is actually \"ACL2\"."
420                                   chan state)))))
421                       (cond (events1
422                              (pprogn (newline chan state)
423                                      (newline chan state)))
424                             (t state))
425                       (print-objects-pretty events2 chan state)
426                       (close-output-channel chan state)
427                       (value :invisible))))))))
428
429(defmacro book-essence (infile &optional outfile cert-optional-p infile-keywords)
430  (declare (ignore infile-keywords)) ; add later for parameters, like ttags
431  (let* ((outfile (or outfile (concatenate 'string infile ".essence")))
432         (len (length infile))
433         (book-name
434          (cond ((eq cert-optional-p :skip) nil)
435                ((and (< 5 len)
436                      (equal (subseq infile (- len 5) len)
437                             ".lisp"))
438                 (subseq infile 0 (- len 5)))
439                (t (er hard 'book-essence
440                       "Input file ~x0 did not end in ~s1 ."
441                       infile ".lisp")))))
442    `(ld '((reset-prehistory)
443           (include-book ,book-name)
444           (print-book-essence ,book-name ,infile ,outfile ,cert-optional-p
445                               'book-essence state)
446           (ubt! 1)
447           (ubt-prehistory)))))
448
449; Modification for creating essence file for ACL2 source file axioms.lisp:
450
451(defmacro axioms-essence (&optional (outfile '"defaxioms.lisp.trans"))
452  `(progn
453     (defttag :pprint-axioms)
454     (progn!
455      :state-global-bindings
456      ((temp-touchable-vars t set-temp-touchable-vars)
457       (temp-touchable-fns t set-temp-touchable-fns))
458      (set-raw-mode-on state)
459      (let ((*features* (cons :acl2-loop-only *features*))
460            (ctx 'axioms-essence))
461        (er-let*
462         ((acl2-src-dir
463           (getenv$ "ACL2_SRC" state)))
464         (cond ((null acl2-src-dir)
465                (er soft ctx
466                    "Environment variable ACL2_SRC needs to be set."))
467               (t (print-book-essence nil
468                                      (concatenate 'string acl2-src-dir
469                                                   "/axioms.lisp")
470                                      ,outfile :skip
471                                      ctx state))))))))
472