1(in-package "ACL2") 2 3; In what follows, logic-only means that we only want events with logical 4; content, such as defaxiom, defthm, and logic-mode defun (and defund) forms, 5; but not including program-mode definitions, table events, etc. 6 7; We drop local forms, regardless of logic-only. 8 9; Either way, we drop all hints. That could be changed. 10 11(program) 12(set-state-ok t) 13 14(defun read-portcullis-cmds1 (chan cert-file ctx state acc) 15 (mv-let (eofp form state) 16 (read-object chan state) 17 (cond (eofp (er soft ctx 18 "Reached end of file ~x0 before reaching ~ 19 :END-PORTCULLIS-CMDS." 20 cert-file)) 21 ((eq form :END-PORTCULLIS-CMDS) 22 (if (eq acc :start) 23 (er soft ctx 24 "In file ~x0, reached :END-PORTCULLIS-CMDS before ~ 25 reaching :BEGIN-PORTCULLIS-CMDS." 26 cert-file) 27 (value (reverse acc)))) 28 ((eq form :BEGIN-PORTCULLIS-CMDS) 29 (if (eq acc :start) 30 (read-portcullis-cmds1 chan cert-file ctx state nil) 31 (er soft ctx 32 "In file ~x0, reached :BEGIN-PORTCULLIS-CMDS twice." 33 cert-file))) 34 ((eq acc :start) 35 (read-portcullis-cmds1 chan cert-file ctx state acc)) 36 (t (read-portcullis-cmds1 chan cert-file ctx state 37 (cons form acc)))))) 38 39(defun read-portcullis-cmds (book-name cert-optional-p ctx state) 40 (let ((cert-file (concatenate 'string 41 (extend-pathname (cbd) book-name state) 42 ".cert"))) 43 (mv-let (chan state) 44 (open-input-channel cert-file :object state) 45 (cond ((null chan) 46 (if cert-optional-p 47 (value nil) 48 (er soft ctx 49 "Unable to open certificate file ~x0." 50 cert-file))) 51 (t (mv-let 52 (erp forms state) 53 (read-portcullis-cmds1 chan cert-file ctx state :start) 54 (pprogn (close-input-channel chan state) 55 (cond (erp (mv erp forms state)) 56 (t (value forms)))))))))) 57 58(defun expand-to-event (form ctx state) 59 (let ((orig-form form) 60 (wrld (w state)) 61 (names 62 63; Warning: If you add a name here, handle it in essential-events (and hence 64; perhaps essential-basic-event). 65 66 (list* 'defun-sk ; given custom handling here 67 'in-package 68 'defpkg 69 70; The following for translating axioms.lisp; you won't find them in a book. 71 72 'value 'set-ld-skip-proofsp 73 (primitive-event-macros))) 74 (portcullisp nil) ; ok to be generous 75 (in-local-flg nil) ; ok to be generous 76 (in-encapsulatep nil) ; ok to be generous 77 (make-event-chk nil) ; we will handle make-event issues ourselves 78 ) 79 (chk-embedded-event-form form orig-form wrld ctx state names portcullisp 80 in-local-flg in-encapsulatep make-event-chk))) 81 82(defmacro internal-error (ctx string &rest args) 83 `(er soft ,ctx 84 "Internal error: ~@0" 85 (msg ,string ,@args))) 86 87(defun essential-basic-event (form ctx state) 88 (declare (xargs :guard (true-listp form))) 89 (let* ((name (cadr form)) 90 (wrld (w state)) 91 (event-type (car form))) 92 (case event-type 93 ((defun defun-sk) 94 (cond 95 ((eq (defun-mode name wrld) :logic) 96 (let ((tbody (getprop name 'unnormalized-body nil 'current-acl2-world 97 wrld))) 98 (cond ((null tbody) 99 (internal-error 100 ctx 101 "Missing 'unnormalized-body property for ~x0." 102 name)) 103 ((eq event-type 'defun) 104 (value (list 'defun name (caddr form) tbody))) 105 (t 106 (case-match form 107 (('defun-sk !name formals 108 (quant vars &) . &) 109 (let ((vars 110 (if (symbolp vars) (list vars) vars))) 111 (cond 112 ((null (cdr vars)) 113 (case-match tbody 114 (('prog2$ ('throw-nonexec-error . &) 115 (('lambda & matrix) . &)) 116 (value (list 'defun-sk name formals 117 (list quant vars matrix)))) 118 (& (internal-error ctx 119 "Unexpected form of ~ 120 'unnormalized-body property for ~ 121 ~x0:~|~% ~x1" 122 name tbody)))) 123 (t ; at least two vars 124 (case-match tbody 125 (('prog2$ ('throw-nonexec-error . &) 126 (('lambda ('mv . &) 127 (('lambda & matrix) . &)) 128 . &)) 129 (value (list 'defun-sk name formals 130 (list quant vars matrix)))) 131 (& (internal-error ctx 132 "Unexpected form of ~ 133 'unnormalized-body property for ~ 134 ~x0:~|~% ~x1" 135 name tbody))))))) 136 (& (internal-error ctx 137 "Expected defun-sk of a certain form, ~ 138 but got:~|~% ~x1." 139 name 140 form))))))) 141 (t 142; Don't cause an error -- maybe we needed this function in order to define 143; macros or constants. 144 (value nil)))) 145 ((defaxiom defthm) 146 (let ((tbody (getprop name 'theorem nil 'current-acl2-world wrld))) 147 (value (and tbody 148 (list event-type 149 (cadr form) 150 tbody))))) 151 (defpkg 152 (let ((pkg-entry (assoc-equal name 153 (known-package-alist 154 state)))) 155 (cond (pkg-entry (value (list event-type 156 (cadr form) 157 (kwote (package-entry-imports 158 pkg-entry))))) 159 (t (internal-error 160 ctx 161 "Missing package entry for ~x0 in the ~ 162 known-package-alist." 163 name))))) 164 (in-package (value form)) 165 (include-book 166 167; !! Should we deal with :ttags too? 168 169 (let* ((kwd-args (cddr form)) 170 (dir (cadr (assoc-keyword :dir kwd-args)))) 171 (cond 172 ((eq dir :system) 173 (value `(include-book ,(cadr form) :dir :system))) 174 (dir 175 176; Warning: Keep the following in sync with ACL2 source function 177; include-book-fn. 178 179 (er-let* 180 ((dir-value 181 (include-book-dir-with-chk soft ctx dir))) 182 (mv-let 183 (full-book-name directory-name familiar-name) 184 (parse-book-name dir-value (cadr form) ".lisp" state) 185 (declare (ignore directory-name familiar-name)) 186 (value `(include-book ,full-book-name))))) 187 (t (value `(include-book ,(cadr form))))))) 188 (otherwise (er soft ctx 189 "Unexpected form type in ~x0: ~x1" 190 'essential-basic-event form))))) 191 192(defun cons-to-all (a x) 193 (declare (xargs :guard (true-listp x))) 194 (cond ((endp x) nil) 195 (t (cons (cons a (car x)) 196 (cons-to-all a (cdr x)))))) 197 198(defun fix-signature (sig) 199 200; Convert a signature to a list (fn . arity). 201 202 (declare (xargs :guard t)) 203 (case-match sig 204 (((name . formals) . &) 205 (list name (length formals))) 206 ((name formals . &) 207 (list name (length formals))) 208 (& (er hard 'fix-signature 209 "Unexpexpected signature, ~x0" 210 sig)))) 211 212(defun fix-signatures (sigs) 213 (declare (xargs :guard (true-listp sigs))) 214 (cond ((endp sigs) nil) 215 (t (cons (fix-signature (car sigs)) 216 (fix-signatures (cdr sigs)))))) 217 218(defun essential-events (forms acc ctx state) 219 220; Warning: state global 'ld-skip-proofsp should be 'local before calling this 221; function. 222 223 (cond 224 ((atom forms) 225 (value (reverse acc))) 226 (t 227 (er-let* 228 ((form (expand-to-event (car forms) ctx state))) 229 (cond 230 ((null form) 231 (essential-events (cdr forms) acc ctx state)) 232 (t 233 (case (car form) 234 (progn 235 (essential-events (append (cdr form) (cdr forms)) acc ctx state)) 236 (with-output 237 (essential-events (cons (car (last form)) (cdr forms)) acc ctx state)) 238 (skip-proofs ; !! special annotation needed? 239 (essential-events (cons (cadr form) (cdr forms)) acc ctx state)) 240 (make-event 241 (let ((exp (cadr (assoc-keyword :check-expansion (cddr form))))) 242 (cond ((consp exp) 243 (essential-events (cons exp (cdr forms)) acc ctx state)) 244 (t 245 (er soft ctx 246 "Encountered make-event form without expansion stored ~ 247 in :check-expansion field, which we cannot currently ~ 248 handle:~|~%~x0" 249 form))))) 250 (encapsulate 251 (let ((signatures (cadr form))) 252 (cond (signatures 253 (er-let* 254 ((events (essential-events (cddr form) nil ctx state))) 255 (essential-events (cdr forms) 256 (cons (list* 'encap 257 (fix-signatures (cadr form)) 258 events) 259 acc) 260 ctx state))) 261 (t (essential-events (append (cddr form) (cdr forms)) acc ctx 262 state))))) 263 ((mutual-recursion defuns) 264 (let ((defs (if (eq (car form) 'mutual-recursion) 265 (cdr form) 266 (cons-to-all 'defun (cdr form))))) 267 (er-let* 268 ((events (essential-events defs nil ctx state))) 269 (essential-events (cdr forms) 270 (if events 271 (cons (cons 'mutual-recursion events) acc) 272 acc) 273 ctx state)))) 274 ((defun defthm defaxiom in-package defpkg include-book defun-sk) 275 (er-let* ((new-form (essential-basic-event form ctx state))) 276 (essential-events (cdr forms) 277 (if new-form (cons new-form acc) acc) 278 ctx 279 state))) 280 (table 281 282; Even :program mode event can be skipped. We'll check modes in 283; essential-basic-event. 284 285 (essential-events (cdr forms) acc ctx state)) 286 ( 287 288; We want to cause an error for every remaining event that has logical content. 289; (But we are handling the defun-mode already, so we can skip (logic) and 290; (program).) The following is the value of the following expression after 291; (push :non-standard-analysis *features*). With this approach, if ACL2 later 292; contains new logical events that we use then we will see an error. If we 293; used the other possible parity, taking the short list below as teh list on 294; which to cause an error, then we would miss that additional logical event 295; rather than causing an error. 296#|| 297 (set-difference-eq (primitive-event-macros) 298 '(#+:non-standard-analysis 299 defun-std 300 #+:non-standard-analysis 301 defthm-std 302 defstobj 303 defchoose 304 progn! 305 defttag)) 306||# 307 308 (value set-ld-skip-proofsp ; see expand-to-event 309 DEFUN MUTUAL-RECURSION DEFUNS DEFTHM DEFAXIOM 310 DEFCONST DEFLABEL DEFDOC DEFTHEORY 311 VERIFY-GUARDS DEFMACRO IN-THEORY 312 IN-ARITHMETIC-THEORY PUSH-UNTOUCHABLE 313 REMOVE-UNTOUCHABLE RESET-PREHISTORY 314 SET-BODY TABLE PROGN ENCAPSULATE 315 INCLUDE-BOOK ADD-CUSTOM-KEYWORD-HINT 316 ADD-INCLUDE-BOOK-DIR 317 DELETE-INCLUDE-BOOK-DIR 318 COMP VERIFY-TERMINATION VERIFY-TERMINATION-BOOT-STRAP 319 ADD-MATCH-FREE-OVERRIDE 320 THEORY-INVARIANT LOGIC PROGRAM 321 ADD-DEFAULT-HINTS! REMOVE-DEFAULT-HINTS! 322 SET-MATCH-FREE-DEFAULT 323 SET-ENFORCE-REDUNDANCY 324 SET-VERIFY-GUARDS-EAGERNESS 325 SET-NON-LINEARP 326 SET-COMPILE-FNS SET-MEASURE-FUNCTION 327 SET-WELL-FOUNDED-RELATION 328 SET-INVISIBLE-FNS-TABLE 329 SET-BACKCHAIN-LIMIT 330 SET-BOGUS-DEFUN-HINTS-OK 331 SET-BOGUS-MUTUAL-RECURSION-OK 332 SET-DEFAULT-BACKCHAIN-LIMIT 333 SET-IRRELEVANT-FORMALS-OK 334 SET-IGNORE-OK SET-INHIBIT-WARNINGS 335 SET-STATE-OK SET-LET*-ABSTRACTIONP 336 SET-NU-REWRITER-MODE 337 SET-CASE-SPLIT-LIMITATIONS 338 SET-DEFAULT-HINTS! 339 SET-REWRITE-STACK-LIMIT VALUE-TRIPLE 340 defattach) 341 (essential-events (cdr forms) acc ctx state)) 342 (otherwise 343 (er soft ctx 344 "~x0 is not yet implemented, hence the following form is ~ 345 illegal:~|~% ~x1" 346 (car form) 347 (car forms)))))))))) 348 349(defun print-objects-pretty-rec (lst ch state) 350 (cond ((null lst) state) 351 (t (mv-let (col state) 352 (fmt1 "~X01~|" 353 (list (cons #\0 (car lst)) (cons #\1 nil)) 354 0 ch state nil) 355 (declare (ignore col)) 356 (pprogn (if (cdr lst) 357 (newline ch state) 358 state) 359 (print-objects-pretty-rec (cdr lst) ch state)))))) 360 361(defun print-objects-pretty (lst ch state) 362 (mv-let (erp val state) 363 (state-global-let* ((write-for-read t)) 364 (pprogn (print-objects-pretty-rec lst ch state) 365 (value :invisible))) 366 (declare (ignore erp val)) 367 state)) 368 369(defun set-ld-skip-proofsp-state (val state) 370 (mv-let (erp x state) 371 (set-ld-skip-proofsp val state) 372 (declare (ignore erp x)) 373 state)) 374 375(defun print-book-essence (book-name infile outfile cert-optional-p ctx state) 376 (state-global-let* 377 ((ld-skip-proofsp 'include-book set-ld-skip-proofsp-state)) 378 (er-let* 379 ((portcullis-cmds 380 (if (eq cert-optional-p :skip) 381 (value nil) 382 (read-portcullis-cmds book-name cert-optional-p ctx state))) 383 (forms (read-object-file infile ctx state)) 384 (events1 (essential-events portcullis-cmds nil ctx 385 state)) 386 (events2 (essential-events forms nil ctx state))) 387 (mv-let (chan state) 388 (open-output-channel outfile :object state) 389 (cond ((null chan) 390 (er soft ctx 391 "Unable to open file ~x0 for output." 392 outfile)) 393 (t (pprogn 394 (print-objects-pretty events1 chan state) 395 (cond (events1 396 (pprogn 397 (newline chan state) 398 (princ$ "; NOTE: Only the forms above are evaluated (as opposed the ones below," 399 chan state) 400 (newline chan state) 401 (princ$ "; which merely are read) when translating to ML." 402 chan state))) 403 (t state)) 404 (assert$ 405 (and (consp (car events2)) 406 (eq (caar events2) 'in-package)) 407 (cond 408 ((equal (cadar events2) "ACL2") state) 409 (t 410 (pprogn 411 (assert$ 412 events1 ; else we could not have a new package here 413 (princ$ " On a related note:" 414 chan state)) 415 (newline chan state) 416 (princ$ "; the following IN-PACKAGE form is for use by a2ml, but all forms in" 417 chan state) 418 (newline chan state) 419 (princ$ "; this file assume that the current package is actually \"ACL2\"." 420 chan state))))) 421 (cond (events1 422 (pprogn (newline chan state) 423 (newline chan state))) 424 (t state)) 425 (print-objects-pretty events2 chan state) 426 (close-output-channel chan state) 427 (value :invisible)))))))) 428 429(defmacro book-essence (infile &optional outfile cert-optional-p infile-keywords) 430 (declare (ignore infile-keywords)) ; add later for parameters, like ttags 431 (let* ((outfile (or outfile (concatenate 'string infile ".essence"))) 432 (len (length infile)) 433 (book-name 434 (cond ((eq cert-optional-p :skip) nil) 435 ((and (< 5 len) 436 (equal (subseq infile (- len 5) len) 437 ".lisp")) 438 (subseq infile 0 (- len 5))) 439 (t (er hard 'book-essence 440 "Input file ~x0 did not end in ~s1 ." 441 infile ".lisp"))))) 442 `(ld '((reset-prehistory) 443 (include-book ,book-name) 444 (print-book-essence ,book-name ,infile ,outfile ,cert-optional-p 445 'book-essence state) 446 (ubt! 1) 447 (ubt-prehistory))))) 448 449; Modification for creating essence file for ACL2 source file axioms.lisp: 450 451(defmacro axioms-essence (&optional (outfile '"defaxioms.lisp.trans")) 452 `(progn 453 (defttag :pprint-axioms) 454 (progn! 455 :state-global-bindings 456 ((temp-touchable-vars t set-temp-touchable-vars) 457 (temp-touchable-fns t set-temp-touchable-fns)) 458 (set-raw-mode-on state) 459 (let ((*features* (cons :acl2-loop-only *features*)) 460 (ctx 'axioms-essence)) 461 (er-let* 462 ((acl2-src-dir 463 (getenv$ "ACL2_SRC" state))) 464 (cond ((null acl2-src-dir) 465 (er soft ctx 466 "Environment variable ACL2_SRC needs to be set.")) 467 (t (print-book-essence nil 468 (concatenate 'string acl2-src-dir 469 "/axioms.lisp") 470 ,outfile :skip 471 ctx state)))))))) 472