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