1(in-package "ACL2")
2
3; Evaluation of (print-kpa lisp-filename ml-filename) prints to the indicated
4; filenames corresponding representations (Lisp and ML) of the current package
5; structure.  In each case (Lisp and ML) there are two forms (which in the case
6; of ML are ML definitions).  The form first provides a list of triples
7
8; <symbol-name, known-pkg-name, actual-pkg-name>
9
10; the idea being that when symbol-name is interned into known-pkg-name, the
11; resulting symbol's package name is actual-pkg-name.  That is, the symbol with
12; name symbol-name and package-name actual-pkg-name is imported into package
13; known-pkg-name.  The second form is a list of known package names.  Note that
14; packages with empty import lists will not be mentioned in any second or third
15; component of a triple.
16
17(set-state-ok t)
18
19(program)
20
21(defun triplesp (x)
22  (if (consp x)
23      (and (true-listp (car x))
24           (equal (length (car x)) 3)
25           (triplesp (cdr x)))
26    (null x)))
27
28(defun kpa-to-triples-aux (pkg-name imports acc)
29  (declare (xargs :guard (and (symbol-listp imports)
30                              (triplesp acc))))
31  (cond ((endp imports) acc)
32        (t (cons (list (symbol-name (car imports))
33                       pkg-name
34                       (symbol-package-name (car imports)))
35                 (kpa-to-triples-aux pkg-name (cdr imports) acc)))))
36
37(defun kpa-to-triples (kpa acc)
38  (declare (xargs :guard (and (alistp kpa) ; should be stronger
39                              (triplesp acc))))
40  (cond ((endp kpa) acc)
41        (t (kpa-to-triples (cdr kpa)
42                           (kpa-to-triples-aux
43                            (package-entry-name (car kpa))
44                            (package-entry-imports (car kpa))
45                            acc)))))
46
47(defun print-string-triples-rec (triples chan state)
48  (declare (xargs :stobjs state
49                  :guard (and (triplesp triples)
50                              (symbolp chan)
51                              (open-output-channel-p chan :character state))))
52  (cond ((endp triples) state)
53        (t (pprogn (fms "    (~x0 , ~x1 , ~x2)~s3"
54                        (list (cons #\0 (nth 0 (car triples)))
55                              (cons #\1 (nth 1 (car triples)))
56                              (cons #\2 (nth 2 (car triples)))
57                              (cons #\3 (if (cdr triples) "," "")))
58                        chan state nil)
59                   (print-string-triples-rec (cdr triples) chan state)))))
60
61(defun print-objs-rec (objs chan state)
62  (declare (xargs :stobjs state
63                  :guard (and (true-listp objs)
64                              (symbolp chan)
65                              (open-output-channel-p chan :character state))))
66  (cond ((endp objs) state)
67        (t (pprogn (fms "    ~x0~s1"
68                        (list (cons #\0 (car objs))
69                              (cons #\1 (if (cdr objs) "," "")))
70                        chan state nil)
71                   (print-objs-rec (cdr objs) chan state)))))
72
73(defun print-ml-string-triples-and-known-pkgs (triples pkg-names filename ctx
74                                                       state)
75  (declare (xargs :stobjs state))
76  (mv-let (chan state)
77    (open-output-channel filename :character state)
78    (cond ((null chan)
79           (er soft ctx
80               "Unable to open file ~x0 for output.~|"
81               filename))
82          (t (pprogn (princ$ "val ACL2_PACKAGE_ALIST =" chan state)
83                     (newline chan state)
84                     (princ$ "   [" chan state)
85                     (print-string-triples-rec triples chan state)
86                     (princ$ "];" chan state)
87                     (newline chan state)
88                     (newline chan state)
89                     (princ$ "val ACL2_KNOWN_PACKAGES =" chan state)
90                     (newline chan state)
91                     (princ$ "   [" chan state)
92                     (print-objs-rec pkg-names chan state)
93                     (princ$ "];" chan state)
94                     (newline chan state)
95                     (close-output-channel chan state)
96                     (value :invisible))))))
97
98(defun imports-alist-from-kpa (kpa)
99  (cond ((endp kpa) nil)
100        (t (let* ((entry (car kpa))
101                  (name (package-entry-name entry))
102                  (imports (package-entry-imports entry)))
103             (acons name imports (imports-alist-from-kpa (cdr kpa)))))))
104
105(defun print-imports-alist (filename ctx state)
106  (mv-let
107   (channel state)
108   (open-output-channel filename :object state)
109   (cond ((null channel)
110          (er soft ctx
111              "Unable to open file ~s0 for :character output."
112              filename))
113         (t (pprogn (print-object$ (imports-alist-from-kpa
114                                    (known-package-alist state))
115                                   channel state)
116                    (newline channel state)
117                    (close-output-channel channel state)
118                    (value :invisible))))))
119
120(defmacro print-kpa (lisp-filename ml-filename)
121  `(let* ((lisp-filename ,lisp-filename)
122          (ml-filename ,ml-filename)
123          (kpa (known-package-alist state))
124          (triples (kpa-to-triples kpa nil))
125          (pkg-names (strip-cars kpa)))
126     (er-progn (print-imports-alist lisp-filename 'print-kpa state)
127               (print-ml-string-triples-and-known-pkgs
128                triples pkg-names ml-filename 'print-kpa state)
129               (pprogn (fms "Wrote files ~x0 and ~x1.~|"
130                            (list (cons #\0 lisp-filename)
131                                  (cons #\1 ml-filename))
132                            (standard-co state) state nil)
133                       (value :invisible)))))
134
135; A test (remove the NOT to see that this is a well-formed test):
136
137#|
138(loop for x in (kpa-to-triples (known-package-alist state) nil)
139      when (not (equal (symbol-package-name (intern (car x) (cadr x))) (caddr x)))
140      do (print x))
141|#
142
143; Now we check that the current known-package-alist agrees with the
144; known-package-alist from a given lisp file, such as was written above.
145
146(defun chk-known-package-alist (pkg-file state)
147  (let ((ctx 'chk-known-package-alist))
148    (er-let* ((lst (read-file pkg-file state)))
149      (cond ((not (and (true-listp lst)
150                       (eql (len lst) 1)
151                       (alistp (car lst))))
152             (er soft ctx
153                 "Unexpected form for package file, ~x0."
154                 pkg-file))
155            (t (let* ((full-imports-alist (car lst))
156                      (full-pkg-list (strip-cars full-imports-alist))
157                      (current-imports-alist
158                       (imports-alist-from-kpa (known-package-alist state)))
159                      (bad-keys
160                       (set-difference-equal (strip-cars current-imports-alist)
161                                             full-pkg-list)))
162                 (cond (bad-keys
163                        (er soft ctx
164                            "Known package~#0~[ ~&0 is~/s ~&0 are~] is ~
165                             missing in package file ~x1."
166                            bad-keys pkg-file))
167                       ((subsetp-equal current-imports-alist full-imports-alist)
168                        (pprogn
169                         (fms "Chk-known-package-alist: PASSED~|"
170                              nil (standard-co state) state nil)
171                         (value :invisible)))
172                       (t (let* ((diff
173                                  (set-difference-equal current-imports-alist
174                                                        full-imports-alist))
175                                 (current-imports (cdar diff))
176                                 (key (caar diff))
177                                 (full-imports
178                                  (cdr (assoc-equal key full-imports-alist))))
179                            (er soft ctx
180                                "The current value of ~x0 is not contained in ~
181                                 the known-package-alist stored in file ~x1.  ~
182                                 For example, compare the symbols imported ~
183                                 into package ~x2, as follows.~|~%For the ~
184                                 current known-package-alist:~| ~
185                                 ~X35.~|~%Stored in the above file:~| ~X45.~|"
186                                '(known-package-alist state)
187                                pkg-file
188                                key
189                                current-imports
190                                full-imports
191                                nil))))))))))
192
193(defun note-chk-known-package-alist-success (filename state)
194  (mv-let
195   (channel state)
196   (open-output-channel filename :character state)
197   (cond ((null channel)
198          (er soft 'note-chk-known-package-alist-success
199              "Unable to open file ~s0 for :character output."
200              filename))
201         (t (pprogn (princ$ "Success!" channel state)
202                    (newline channel state)
203                    (close-output-channel channel state)
204                    (value :invisible))))))
205
206