1;;; Translate a file of defuns into readable defp forms.  We want to translate
2;;; first both as a sanity check on the input and to be sure that we have
3;;; proper internal form; and then we untranslate into pretty user-level
4;;; syntax.
5
6;;; For simplicity, our implementation loads the input file first in order to
7;;; get ACL2 to know about the new names.
8
9;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
10;;; INSTRUCTIONS
11;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
12
13;;; BEFORE USE, start ACL2 and certify this book in this directory:
14
15;;; (certify-book "untranslate-file")
16
17;;; FOR EACH USE, start ACL2 and do the following.
18
19;;; 1. Include this book:
20
21;;; (include-book "untranslate-file")
22
23;;; 2. Include the necessary books before running this tool, e.g.:
24
25;;; (include-book "models/jvm/m1/m1-story" :dir :system)
26
27;;; 3. Then run the tool with specified input file to read, output file to write,
28;;;    and the package into which to write the output file.  For example:
29
30;;; (untranslate-file "fact.lisp" "fact-out.lisp" "M1")
31
32;;; 4. Optionally, as a sanity check, restart ACL2 and certify the resulting
33;;;    book, after including the book from step 2.  For example:
34
35;;; (include-book "models/jvm/m1/m1-story" :dir :system)
36;;; (certify-book "fact-out" ?)
37
38;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
39
40
41(in-package "ACL2")
42
43(program)
44(set-state-ok t)
45
46(mutual-recursion
47
48(defun merge-lets-lst (form)
49  (cond ((atom form) form)
50        (t (cons (merge-lets (car form) nil)
51                 (merge-lets-lst (cdr form))))))
52
53(defun merge-lets (form bindings)
54
55; Warning: This is a hack, as it operates on untranslated forms, which might
56; have macro calls!  But in our intended application, we expect only harmless
57; macros (like append, and, etc.).
58
59; Form is an untranslated form.  We feel secure in replacing repeated (let
60; ((var val)) ...) by let*, provided there are no declare forms and a unique
61; variable bound each time.
62
63  (case-match form
64    (('let ((var val)) body)
65     (merge-lets body (cons (list var val) bindings)))
66    (&
67     (let ((new-form (cond ((atom form) form)
68                           (t (cons (car form)
69                                    (merge-lets-lst (cdr form)))))))
70       (cond ((cdr bindings)
71              `(let* ,(reverse bindings)
72                 ,new-form))
73             (bindings
74              `(let (,(car bindings))
75                 ,new-form))
76             (t new-form))))))
77
78)
79
80(defun untranslate-form (form ctx wrld)
81  (case-match form
82    (('defun fn args . &)
83     `(defp ,fn ,args
84        ,(merge-lets (untranslate
85                      (getprop fn 'unnormalized-body
86                               '(:error "translate-form didn't find a value.")
87                               'current-acl2-world wrld)
88                      nil wrld)
89                     nil)))
90    (&
91     (er hard ctx
92         "Unrecognized form (expected (defun ...): ~x0"
93         form))))
94
95(defun untranslate-form-lst (lst ctx wrld acc)
96  (cond ((endp lst)
97         (reverse acc))
98        (t (untranslate-form-lst (cdr lst) ctx wrld
99                                 (cons (untranslate-form (car lst) ctx wrld)
100                                       acc)))))
101
102(defun set-current-package-state (val state)
103  (mv-let (erp val state)
104          (set-current-package val state)
105          (declare (ignore val))
106          (cond (erp (prog2$ (er hard 'set-current-package-state
107                                 "Aborting")
108                             state))
109                (t state))))
110
111(defun pprint-objects (lst ch state)
112  (cond ((null lst) state)
113        (t (pprogn (fms "~x0~|" (list (cons #\0 (car lst))) ch state nil)
114                   (pprint-objects (cdr lst) ch state)))))
115
116(defun untranslate-file1 (infile outfile pkg state)
117  (let ((ctx 'untranslate-file))
118    (state-global-let*
119     ((current-package pkg set-current-package-state))
120     (er-let*
121      ((forms (read-file infile state)))
122      (mv-let (chan state)
123              (open-output-channel outfile :object state)
124              (cond ((null chan)
125                     (er soft ctx
126                         "Unable to write to ~x0"
127                         outfile))
128                    (t
129                     (pprogn
130                      (fms "(in-package ~x0)~|" (list (cons #\0 pkg)) chan
131                           state nil)
132                      (pprint-objects
133                       (list* '(include-book "misc/defp" :dir :system)
134                              (untranslate-form-lst forms ctx (w state) nil))
135                       chan state)
136                      (close-output-channel chan state)
137                      (value (list :written-to outfile))))))))))
138
139(defmacro untranslate-file (infile outfile pkg)
140  `(ld '((program)
141         (ld ,infile)
142         (untranslate-file1 ,infile ,outfile ,pkg state))))
143