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