1(in-package "ACL2")
2
3; Note: To run this on ACL2 source file axioms.lisp, see pprint-axioms.lisp.
4
5(program)
6(set-state-ok t)
7
8(include-book "misc/file-io" :dir :system)
9
10; In what follows, logic-only means that we only want events with logical
11; content, such as defaxiom, defthm, and logic-mode defun (and defund) forms,
12; but not including program-mode definitions, table events, etc.
13
14; We drop local forms, regardless of logic-only.
15
16; Either way, we drop all hints.  That could be changed.
17
18(defun expand-form (form untrans-flg state)
19  (declare (xargs :guard (true-listp form)))
20  (let* ((wrld (w state))
21         (event-type (car form))
22         (body (case event-type
23                 ((defun defund) (car (last form)))
24                 ((defaxiom defthm defthmd) (third form)))))
25    (er-let* ((tbody (translate body t t t 'top-level wrld state)))
26             (let ((new-body
27                    (if untrans-flg
28                        (untranslate tbody nil wrld)
29                      tbody)))
30               (value
31                (case event-type
32                  ((defun defund) (list 'defun
33                                        (cadr form)
34                                        (caddr form)
35                                        new-body))
36                  ((defaxiom defthm defthmd) (list event-type
37                                                   (cadr form)
38                                                   new-body))
39                  (otherwise (er hard 'expand-form
40                                 "Unexpected form type: ~x0"
41                                 form))))))))
42
43(defun my-unparse-signature (x)
44
45; Unlike built-in function unparse-signature, here we don't care about outputs,
46; but we do care about all formals names.
47
48  (let* ((fn (car x))
49         (formals (cadr x)))
50    `(,fn ,formals)))
51
52(defun my-unparse-signature-lst (lst)
53  (if (endp lst)
54      nil
55    (cons (my-unparse-signature (car lst))
56          (my-unparse-signature-lst (cdr lst)))))
57
58(defun set-ld-redefinition-action-state (val state)
59  (mv-let (erp val state)
60          (set-ld-redefinition-action val state)
61          (declare (ignore erp val))
62          state))
63
64(defun expand-forms (forms acc untrans-flg logic-only ctx wrld state)
65
66; Result is in reverse order.
67
68  (declare (xargs :guard (true-listp forms)))
69  (if (endp forms)
70      (value acc)
71    (er-let* ((new-acc
72               (let ((form (car forms)))
73                 (cond ((atom form) (value acc))
74                       (t (case (car form)
75                            (local (value acc))
76                            ((progn mutual-recursion)
77                             (er-let* ((defs (expand-forms (cdr form) nil
78                                                           untrans-flg
79                                                           logic-only
80                                                           ctx wrld state)))
81                                      (value
82                                       (if (null defs) ; expect logic-only
83                                           acc
84                                         (cons (cons (car form)
85                                                     (reverse defs))
86                                               acc)))))
87                            (encapsulate
88                             (cond
89                              ((null (cadr form))
90                               (expand-forms (cddr form) acc untrans-flg
91                                             logic-only ctx wrld state))
92                              (t
93                               (er-let*
94                                ((pair
95                                  (state-global-let*
96                                   ((ld-redefinition-action
97                                     '(:doit! . :overwrite)
98                                     set-ld-redefinition-action-state))
99                                   (chk-signatures (cadr form) ctx wrld
100                                                   state)))
101                                 (forms (expand-forms (cddr form) nil untrans-flg
102                                                      logic-only ctx wrld
103                                                      state)))
104                                (value (cons (list* 'encap
105                                                    (my-unparse-signature-lst
106                                                     (car pair))
107                                                    (reverse forms))
108                                             acc))))))
109                            ((defaxiom defthm defthmd defun defund)
110                             (if (and logic-only
111                                      (member-eq (car form) '(defun defund))
112                                      (eq (symbol-class (cadr form) (w state))
113                                          :program))
114                                 (value acc)
115                               (er-let*
116                                ((x (expand-form form untrans-flg state)))
117                                (value (cons x acc)))))
118                            (t (if logic-only
119                                   (value acc)
120                                 (value (cons form acc))))))))))
121             (expand-forms (cdr forms) new-acc untrans-flg logic-only ctx wrld
122                           state))))
123
124(defun write-forms (infile outfile untrans-flg state)
125  (let ((ctx 'write-forms))
126    (er-let* ((forms (read-list infile ctx state))
127              (rev-forms (expand-forms forms nil untrans-flg
128                                       t ; logic-only
129                                       ctx (w state) state)))
130             (write-list (reverse rev-forms)
131                         outfile ctx state))))
132