1;;; Given a file, check that each of its forms is essentially redundant. Here, 2;;; "essentially redundant" means that they represent the same logical formula. 3;;; Thus, we might include an ACL2 book and then check that the resulting 4;;; round-trip file (created by ACL2 -> HOL/SEXP -> ACL2) contains only 5;;; essentially redundant forms. 6 7;;; Example use: 8; (include-book "~/projects/HOL/examples/acl2/lisp/check-file") 9; (include-book "~/projects/HOL/examples/acl2/tests/inputs/pkg-test") 10; (check-file "~/Downloads/pkg_test.lisp") 11 12(in-package "ACL2") 13 14(program) 15(set-state-ok t) 16 17(mutual-recursion 18 19(defun fold-conses (term) 20 (cond ((or (variablep term) 21 (fquotep term)) 22 term) 23 (t (let ((args (fold-conses-lst (fargs term)))) 24 (cond ((and (eq (ffn-symb term) 'cons) 25 (quotep (car args)) 26 (quotep (cadr args))) 27 (kwote (cons (unquote (car args)) 28 (unquote (cadr args))))) 29 ((flambdap (ffn-symb term)) 30 (cons-term (make-lambda 31 (lambda-formals (ffn-symb term)) 32 (fold-conses-lst 33 (lambda-body (ffn-symb term)))) 34 args)) 35 (t (cons-term (ffn-symb term) 36 args))))))) 37 38(defun fold-conses-lst (x) 39 (cond ((endp x) nil) 40 (t (cons (fold-conses (car x)) 41 (fold-conses-lst (cdr x)))))) 42) 43 44(defun check-form (form ctx wrld state) 45 (case-match form 46 (('defun fn args . rest) 47 (cond 48 ((not (equal args (formals fn wrld))) 49 (er soft ctx 50 "Formals mismatch for ~X01" 51 fn nil)) 52 (t 53 (er-let* 54 ((x (translate (car (last rest)) 55 t ; stobjs-out 56 t ; logic-modep 57 nil ; known-stobjs 58 ctx wrld state))) 59 (cond ((equal 60 (fold-conses x) 61 (fold-conses 62 (getprop fn 'unnormalized-body 63 '(:error "translate-form didn't find a value.") 64 'current-acl2-world wrld))) 65 (value nil)) 66 (t 67 (er soft ctx 68 "Body mismatch for ~x0.~%Loaded:~|~Y12~|File:~|~Y32~|" 69 fn 70 (fold-conses 71 (getprop fn 'unnormalized-body 72 '(:error "translate-form didn't find a value.") 73 'current-acl2-world wrld)) 74 nil 75 (fold-conses x)))))))) 76 (('defthm name body . &) 77 (er-let* 78 ((x (translate body 79 t ; stobjs-out 80 t ; logic-modep 81 nil ; known-stobjs 82 ctx wrld state))) 83 (cond ((equal (fold-conses x) 84 (fold-conses 85 (getprop name 'theorem 86 '(:error "translate-form didn't find a value.") 87 'current-acl2-world wrld))) 88 (value nil)) 89 (t 90 (er soft ctx 91 "Body mismatch for ~x0.~%Loaded:~|~Y12~|File:~|~Y32~|" 92 name 93 (fold-conses 94 (getprop name 'theorem 95 '(:error "translate-form didn't find a value.") 96 'current-acl2-world wrld)) 97 nil 98 (fold-conses x)))))) 99 (('in-package . &) 100 (value nil)) 101 (& 102 (er soft ctx 103 "Unrecognized form (expected (defun ...): ~x0" 104 form)))) 105 106(defun check-form-lst (lst ignore-errors ctx wrld state) 107 (cond ((endp lst) 108 (value nil)) 109 (t (mv-let (erp val state) 110 (check-form (car lst) ctx wrld state) 111 (declare (ignore val)) 112 (cond ((and erp (not ignore-errors)) 113 (silent-error state)) 114 (t (check-form-lst (cdr lst) ignore-errors ctx wrld 115 state))))))) 116 117(defun check-file1 (infile ignore-errors state) 118 (let ((ctx 'check-file) 119 (wrld (w state))) 120 (er-let* 121 ((forms (read-file infile state))) 122 (check-form-lst forms ignore-errors ctx wrld state)))) 123 124(defmacro check-file (infile &optional (show-all 't)) 125 `(check-file1 ,infile ,show-all state)) 126