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