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