; This patch file should only be needed by OpenMCL and CMUCL users who use ; defstobj with :inline t. Thanks to John Matthews for bringing this problem ; to our attention. The definitions below should replace corresponding ones in ; the source code, via editing the sources, though an alternate approach is to ; compile and load this file. ; Patch file for ACL2 Version 2.8 to deal more appropriately with the :inline t ; case of defstobj. Note that some comments and documentation will also be ; updated for ACL2 Version 2.9 that do not appear here. (in-package "ACL2") (defun defstobj-fn (name args state event-form) (with-ctx-summarized (if (output-in-infixp state) event-form (msg "( DEFSTOBJ ~x0 ...)" name)) (let ((event-form (or event-form (list* 'defstobj name args)))) (er-let* ((wrld1 (chk-acceptable-defstobj name args ctx (w state) state))) (cond ((eq wrld1 'redundant) (stop-redundant-event state)) (t (let* ((template (defstobj-template name args)) (field-names (strip-accessor-names (caddr template))) (defconsts (defstobj-defconsts field-names 0)) (field-const-names (strip-cadrs defconsts)) (ax-def-lst (defstobj-axiomatic-defs name template)) (raw-def-lst (defstobj-raw-defs name template)) (recog-name (car template)) (creator-name (cadr template)) (names (strip-cars ax-def-lst)) (the-live-var (the-live-var name)) (doc (defstobj-doc args))) (er-progn (cond ((set-equalp-equal names (strip-cars raw-def-lst)) (value nil)) (t (value (er hard ctx "Defstobj-axiomatic-defs and ~ defstobj-raw-defs are out of sync! They ~ should each define the same set of names. ~ Here are the functions with axiomatic defs ~ that have no raw defs: ~x0. And here are ~ the with raw defs but no axiomatic ones: ~ ~x1." (set-difference-equal names (strip-cars raw-def-lst)) (set-difference-equal (strip-cars raw-def-lst) names))))) (revert-world-on-error (pprogn (set-w 'extension wrld1 state) (er-progn (process-embedded-events 'defstobj (table-alist 'acl2-defaults-table wrld1) t ;;; skip-proofsp (current-package state) (list 'defstobj name names) (append ; We only need to lay down these set-*-ok calls in the case that we do not ; allow array resizing, for the resizing and length field functions. But for ; simplicity, we always lay them down. Note that since we are really modifying ; the acl2-defaults-table here, their effect is local to the defstobj. '((set-ignore-ok t) (set-irrelevant-formals-ok t)) (pairlis-x1 'defun ax-def-lst) defconsts ; It is important to disable the executable counterpart of the creator ; function, so as not to expose the live stobj during proofs. We ensure in ; function chk-theory-expr-value1 that the :executable-counterpart rune below ; will never be enabled. `((in-theory (disable (:executable-counterpart ,creator-name))))) ctx state) ; The processing above will define the functions in the logic, using ; defun, and that, in turn, will define their *1* counterparts in ; Lisp. But because of code in defuns-fn, the processing above will ; not define the raw Lisp versions of the functions themselves ; (normally that would be derived from the axiomatic defs just ; processed). Instead, we will store a CLTL-COMMAND below that ; handles the raw Lisp defs only. ; What follows is hard to follow and rather arcane. Why do we include ; name in the ee-entry computed above, (defstobj name names)? That ; entry will be added to the embedded-event-lst by ; process-embedded-events and be inspected by the individual defuns ; done. Those defuns will recognize their fn name, fn, among names, ; to detect that they are being done as part of a defstobj. The defun ; will pick up the stobj name, name, from the ee-entry and build it ; into the ignorep entry of the defun CLTL-COMMAND, to be processed by ; add-trip. In add-trip, the stobj name, name, will find its way into ; the oneify-cltl-code that generates the *1* body for fn. That body ; contains a throw upon detection of a guard error. The object thrown ; contains the stobjs-in of the offensive expression, so we will know ; how to print it. But the stobjs-in of fn is incorrectly set in the ; world right now -- more accurately, will be incorrectly set in the ; world in which the defun is done and the throw form is constructed ; -- because we have not yet declared name to be a stobj. Indeed, we ; cannot declare it to be a stobj yet since we are defining functions ; that treat it as an ordinary list. This is the stobj version of the ; super-defun-wart problem. (er-let* ((doc-pair (translate-doc name doc ctx state))) (let* ((wrld2 (w state)) (wrld3 (update-doc-data-base name doc doc-pair ; Here I declare that name is Common Lisp compliant. Below I ; similarly declare the-live-var. All elements of the namex list of ; an event must have the same symbol-class. (putprop name 'symbol-class :common-lisp-compliant (put-stobjs-in-and-outs name template ; Rockwell Addition: It is convenient for the recognizer to be in a ; fixed position in this list, so I can find out its name. (putprop name 'stobj (cons the-live-var (cons recog-name (append (delete1-eq recog-name names) field-const-names))) (putprop name 'redundancy-bundle (defstobj-redundancy-bundle name args t) (putprop-x-lst1 names 'stobj-function name (putprop-x-lst1 field-const-names 'stobj-constant name (putprop the-live-var 'stobj-live-var name (putprop the-live-var 'symbol-class :common-lisp-compliant (putprop name 'accessor-names (accessor-array name field-names) wrld2)))))))))))) ; The property 'stobj marks a single-threaded object name. Its value ; is a non-nil list containing all the names associated with this ; object. The car of the list is always the live variable name for ; the object. The cadr of the list (for all stobjs but our STATE) is ; the stobj recognizer for the stobj. The remaining elements are all ; the functions used in the definition of the recognizer, the ; accessors and the updaters. We don't list any of the STATE ; functions, just the live name, so the property is non-nil. ; Every supporting function is marked with the property ; 'stobj-function, whose value is the object name. The live var name ; is marked with 'stobj-live-var, whose value is the object name. ; CHEAT: I ought, at this point, ; (pprogn ; (update-user-stobj-alist ; (cons (cons name (create-stobj name template)) ; (user-stobj-alist state)) ; state) ; That is, I should add to the user-stobj-alist in state an entry for ; this new stobj, binding its name to its initial value. But I don't ; want to create the logical counterpart of its initial value -- the ; function create-stobj cannot be used this way (only uses ; resulting from with-local-stobj will pass translate), and we do ; not want to hack our way through the admission of this function ; which is apparently consing a stobj into an alist. Instead, I rely ; on the live object representing the stobj. This live object is ; created when the CLTL-COMMAND below is processed by add-trip. ; Add-trip evals the init form in raw lisp to create the live object ; and assign it to global variables. It also creates array-based ; accessors and updaters. It then stores this live object in the ; user-stobj-alist of the state just as suggested above, provided this ; is not a redefinition. (For a redefinition of the stobj, it does a ; put-assoc-eq rather than a cons.) ; The down-side to this cheat is that this only works while ; defstobj-fn is a :program mode function called on the live state, ; where the raw code operates. If I admitted this function to the ; logic and then called it on the live state, I would get an effect on ; the live state not explained by the code. Furthermore, if I called ; it on a fake state, I would get a new fake state in which the new ; stobj was not on the user-stobj-alist. ; It will be a while before these discrepancies bother me enough to ; fix. As long as this is a :program mode function, we won't be able ; to prove that its effect on state is contrary to its semantics as ; expressed here. (install-event name event-form 'defstobj ; Note: The namex generated below has consists of the single-threaded ; object name, the live variable name, and then the names of all the ; functions introduced. Big-d-little-d-event knows it can cdr past ; the first two elements of the namex of a defstobj to find the list ; of functions involved. (list* name the-live-var names) nil `(defstobj ,name ,the-live-var ,(defstobj-raw-init template) ,raw-def-lst ,template ,ax-def-lst) wrld3 state)))))))))))))) (defun add-trip (world-name world-key trip) ; Add-trip is the function that moves a triple, (symb key . val) from ; a property list world into the von Neumann space of Common Lisp. ; World-name is the name of the world being installed. World-key is ; the property being used to hold the installed properties of that ; world (i.e., the cdr of its 'acl2-world-pair). ; First we set the properties for the global-symbol and *1*-symbol, so that ; these will ultimately be behind the world-key property (as guaranteed at the ; end of the code for this function). (global-symbol (car trip)) (*1*-symbol (car trip)) ; Our next step is to push val onto the key stack in (get symb world-key). (setf (get (car trip) world-key) (destructive-push-assoc (cadr trip) (cddr trip) (get (car trip) world-key) world-key)) ; Now, in the case that we are messing with 'current-acl2-world and ; symb is 'CLTL-COMMAND and key is 'GLOBAL-VALUE, we smash the ; symbol-function or symbol-value cell of the appropriate name, first ; saving the old value (form) on the undo-stack. (cond ((and (eq world-name 'current-acl2-world) (eq (car trip) 'cltl-command) (eq (cadr trip) 'global-value) (consp (cddr trip))) (let ((boot-strap-flg (global-val 'boot-strap-flg (w *the-live-state*))) #+(and allegro (not acl2-loop-only)) ; The following bindings, guarded by the readtime conditional above, should ; turn off redefinition warnings in Allegro and CLISP (2.33 and beyond, at ; least). We trust that add-trip knows what it is doing. Without this code, ; for example, :oops can cause many screens of such warnings. (excl:*redefinition-warnings* nil) #+(and clisp (not acl2-loop-only)) (custom::*suppress-check-redefinition* t)) (case (car (cddr trip)) (defuns ; (cddr trip) is of the form (defuns defun-mode ignorep def1 ... defn). ; Defun-mode non-nil is stored by DEFUNS and defun-mode nil by :non-executable ; DEFUNS and by ENCAPSULATE when it is defining the constrained fns. ; Oneify-cltl-code relies on the fact that functions with defun-mode nil do a ; THROW. ; Observe that we sometimes use oneify-cltl-code to modify the actual Common ; Lisp code. Why don't we modify the defi before storing the cltl-command ; tuple? Because we want to make it easy on ourselves to recover from the ; world the actual defi used to define :program mode functions. See ; verify-termination. ; Recall that ignorep is non-nil if we are to AVOID storing the ; symbol-functions for names. If ignorep is non-nil, then it is either ; reclassifyingp -- meaning we are reclassifying a symbol from :program ; to :logic mode. We don't want to overwrite its ; symbol-function since that might be ACL2 source code. ; We still write a *1* definition in this case. ; (defstobj . stobj) ; -- meaning the names being introduced are actually being ; defun'd under (defstobj stobj ...). We don't want ; to store the code generated by defun for these ; names because defstobj will generate a ; CLTL-COMMAND containing the made-to-order raw ; defs. We also do not store the *1* definition in this ; case, because in openMCL (at least) this would cause a ; problem since the *1* code calls the raw Lisp function, ; which has not yet been defined and in the :inline case is ; actually a macro. (See also the comment in ; defstobj-functionsp.) ; Why do we need the stobj name in the case of ignorep = '(defstobj ; . stobj)? The reason is that when we generate the *1* code for the ; function, fn, we must generate a throw to handle a guard violation ; and the argument to that throw is an object which includes, among ; other things, the stobjs-in of fn so we will know how to print them. ; You might think we would get the stobjs-in of fn from the world. ; But we can't because this defun is being done under, and as part of, ; a defstobj and the defstobj will later declare stobj to be a stobj ; name. So the stobjs-in of fn in the world right now is wrong. The ; stobjs-in we need is built into the object thrown and so won't be ; overwritten when defstobj gets around to declaring stobj a stobj. ; So oneify-cltl-code, called below, takes the stobj name as its input ; and computes the appropriate stobjs-in from the formals. This is a ; problem analogous to the one addressed by the super-defun-wart ; table. (let ((ignorep (caddr (cddr trip))) (mut-rec-flg (< 1 (length (cdddr (cddr trip))))) (defun-mode (cadr (cddr trip))) (names-to-compile ; We avoid potential "undefined" warnings during compilation by defining all ; the functions first, and compiling them only after they have all been ; defined. nil)) (dolist (def (cdddr (cddr trip))) (cond ((and boot-strap-flg (not (global-val 'boot-strap-pass-2 (w *the-live-state*)))) ; During the first pass of initialization, we insist that every function ; defined already be defined in raw lisp. During pass two we can't expect this ; because there may be LOCAL defuns that got skipped during compilation and the ; first pass. (or (fboundp (car def)) ; Note that names of macros are fboundp, so we can get away with symbols that ; are defined to be macros in raw Lisp but functions in the logic (e.g., ; must-be-equal). (interface-er "~x0 is not fboundp!" (car def))) ; But during the first pass of initialization, we do NOT assume that every (or ; any) function's corresponding *1* function has been defined. So we take care ; of that now. (cond ((not (and *compiled-*1*-fns* (fboundp (*1*-symbol (car def))))) (let ((*1*def (cons 'defun (oneify-cltl-code defun-mode mut-rec-flg def ; The if below returns the stobj name being introduced, if any. (if (consp ignorep) (cdr ignorep) nil) (w *the-live-state*))))) (eval (make-defun-declare-form *1*def)) (eval *1*def))))) ((and (not ignorep) (equal *main-lisp-package-name* (symbol-package-name (car def)))) (interface-er "It is illegal to redefine a ~ function in the main Lisp ~ package, such as ~x0!" (car def))) ((and *compiled-*1*-fns* (fboundp (*1*-symbol (car def)))) ; *Compiled-*1*-fns* is only set during initialization, so we know we are in ; the boot-strap. We already covered the pass one case, so we must be in pass ; two. Therefore the function (car def) must be defined, because its *1* ; function is defined. So we do nothing. We do not even need to consider the ; undo-stack, since we never undo into the initialization. ) ((and (consp ignorep) (eq (car ignorep) 'defstobj)) ; We wait for the cltl-command from the defstobj (which is laid down last by ; defstobj-fn, using install-event) before defining/compiling the *1* ; functions, in order to avoid potential "undefined" warnings and, more ; importantly, to avoid defining *1* functions in terms of undefined macros ; (for the :inline case), which confuses openMCL as described in a comment in ; defstobj-functionsp. We still save the existing values (if any) of the ; current def and the current *1* def; see the next comment about ignorep. (maybe-push-undo-stack 'defun (car def) ignorep)) (t (maybe-push-undo-stack 'defun (car def) ignorep) ; Note: If ignorep is '(defstobj . stobj), we save both the current def and the ; current *1* def. If ignorep is 'reclassifying, we save only the *1* def. ; The former behavior means that in defstobj, when the defun runs for each ; name, we will save both symbol-function cells, even though we store into ; neither. The code for installing a defstobj CLTL-COMMAND doesn't bother to ; do undo-stack work, because it knows both cells were saved by the defun. (let ((def (cons 'defun def)) (*1*def (cons 'defun (oneify-cltl-code defun-mode mut-rec-flg def ; The if below returns the stobj name being introduced, if any. (if (consp ignorep) (cdr ignorep) nil) (w *the-live-state*))))) (cond ((and (not (eq (f-get-global 'ld-skip-proofsp *the-live-state*) 'include-book)) (default-compile-fns (w *the-live-state*))) (or ignorep (progn (eval (make-defun-declare-form def)) (eval def) (setq names-to-compile (cons (cadr def) names-to-compile)))) (eval (make-defun-declare-form *1*def)) (eval *1*def) (setq names-to-compile (cons (cadr *1*def) names-to-compile))) (t (or ignorep (eval def)) (eval *1*def)))))) ; Remove the documentation string potentially stored in raw Lisp, if a copy is ; already around in our documentation database, just to save space. (cond ((doc-stringp (documentation (car def) 'function)) (setf (documentation (car def) 'function) nil)))) (dolist (name names-to-compile) (eval `(compile ',name))))) (*1*defuns ; (cddr trip) is of the form (*1*defuns name-1 ... name-n). We know we are in ; the boot-strapping process but after the label end-of-pass-2, building a ; small image. (dolist (name (cdr (cddr trip))) (let ((*1*def (cons 'defun (oneify-cltl-code-program name (w *the-live-state*))))) (eval (make-defun-declare-form *1*def)) (eval *1*def)) (cond ((doc-stringp (documentation name 'function)) (setf (documentation name 'function) nil))))) (defstobj ; (cddr trip) is of the form ; (DEFSTOBJ name the-live-name init raw-defs template axiomatic-defs). ; Init is a form to eval to obtain the initial setting for the live variable. ; Each def in raw-defs and in axiomatic-defs is of the form (name args dcl ; body), where dcl may be omitted. We defun each raw-def and the oneification ; of each axiomatic-def. (let ((name (nth 1 (cddr trip))) (the-live-name (nth 2 (cddr trip))) (init (nth 3 (cddr trip))) (raw-defs (nth 4 (cddr trip))) (template (nth 5 (cddr trip))) (ax-defs (nth 6 (cddr trip))) (names-to-compile ; We avoid "undefined function" warnings by Allegro during compilation by ; defining all the functions first, and compiling them only after they have all ; been defined. nil)) (maybe-push-undo-stack 'defconst the-live-name) (maybe-push-undo-stack 'defconst '*user-stobj-alist*) ; See the comment below, just above where we formerly set the symbol-value of ; name. If we re-install that code, then the next line of code also needs to ; be re-installed. ; (maybe-push-undo-stack 'defconst name) (eval `(defparameter ,the-live-name ,init)) ; As with defconst we want to make it look like we eval'd this defstobj ; in raw lisp, so we set up the redundancy stuff: (setf (get the-live-name 'redundant-raw-lisp-discriminator) (list* 'defstobj (car template) (cadr template) (caddr template))) ; At one point we executed the following form. But now we see that this is not ; necessary, since trans-eval binds stobj names anyhow using *user-stobj-alist* ; and even acl2-raw-eval uses *user-stobj-alist* to bind stobj names. If this ; code is re-installed, then also re-install the code (maybe-push-undo-stack ; 'defconst name) above. ; (setf (symbol-value name) (symbol-value the-live-name)) ; The following assignment to *user-stobj-alist* is structured to keep ; new ones at the front, so we can more often exploit the optimization ; in put-assoc-eq-alist. (setq *user-stobj-alist* (cond ((assoc-eq name *user-stobj-alist*) ; This is a redefinition! We'll just replace the old entry. (put-assoc-eq name (symbol-value the-live-name) *user-stobj-alist*)) (t (cons (cons name (symbol-value the-live-name)) *user-stobj-alist*)))) ; We eval and compile the raw lisp definitions first, some of which may be ; macros (because :inline t was supplied), before dealing with the *1* ; functions. (dolist (def raw-defs) (cond ((and boot-strap-flg (not (global-val 'boot-strap-pass-2 (w *the-live-state*)))) ; During the first pass of initialization, we insist that every function ; defined already be defined in raw lisp. During pass two we can't expect this ; because there may be LOCAL defuns that got skipped during compilation and the ; first pass. (or (fboundp (car def)) (interface-er "~x0 is not fboundp!" (car def)))) ((equal *main-lisp-package-name* (symbol-package-name (car def))) (interface-er "It is illegal to redefine a function in ~ the main Lisp package, such as ~x0!" (car def))) ((and *compiled-*1*-fns* (fboundp (*1*-symbol (car def)))) ; *Compiled-*1*-fns* is only set during initialization, so we know we are in ; the boot-strap. We already covered the pass one case, so we must be in pass ; two. Therefore the function (car def) must be defined, because its *1* ; function is defined. So we do nothing. We do not even need to consider the ; undo-stack, since we never undo into the initialization. ) ; We don't do maybe-push-undo-stack for defuns (whether inlined or not) under ; the defstobj CLTL-COMMAND, because we did it for their defuns. ((member-equal *stobj-inline-declare* def) ; We now handle the case where we are going to inline the function calls by ; defining the function as a defabbrev. Note that this is allowed for ; access/update/array-length functions for stobjs, but only for these, where ; speed is often a requirement for efficiency. (let ((def (cons 'defabbrev (remove-stobj-inline-declare def)))) (progn (eval def) ; CMUCL 18e cannot seem to compile macros at the top level. #-cmu (cond ((and (not (eq (f-get-global 'ld-skip-proofsp *the-live-state*) 'include-book)) (default-compile-fns (w *the-live-state*))) (setq names-to-compile (cons (cadr def) names-to-compile))))))) (t (let ((def (cons 'defun def))) (cond ((and (not (eq (f-get-global 'ld-skip-proofsp *the-live-state*) 'include-book)) (default-compile-fns (w *the-live-state*))) (eval (make-defun-declare-form def)) (eval def) (setq names-to-compile (cons (cadr def) names-to-compile))) (t (eval def))))))) (dolist (def ax-defs) (let ((*1*def (cons 'defun (oneify-cltl-code :logic nil def name (w *the-live-state*))))) (cond ((and (not (eq (f-get-global 'ld-skip-proofsp *the-live-state*) 'include-book)) (default-compile-fns (w *the-live-state*))) (eval (make-defun-declare-form *1*def)) (eval *1*def) (setq names-to-compile (cons (cadr *1*def) names-to-compile))) (t (eval *1*def))))) (dolist (name ; We reverse names-to-compile because we want to be sure to compile the *1* ; defs after the raw Lisp defs (which may be macros, because of :inline). (reverse names-to-compile)) (compile name)))) (defpkg (maybe-push-undo-stack 'defpkg (cadr (cddr trip))) (eval (cons 'defpkg (cdr (cddr trip))))) (defconst ; Historical remark on defconstant. ; In the beginning we supported defconstant. We changed to ; defparameter and then changed to defconst. As things stand now, ; ACL2 supports defconst, which has the same effect at the raw lisp ; level (i.e., the cltl-command) as defparameter, and in addition ; causes proclaim-file to exectute an appropriate proclamation for the ; parameter, knowing as we do that it is really constant. Here are ; some historical remarks that explain why we have gone down this ; path. ; "Currently we turn defconstants into defparameters at the raw Lisp ; level (that is, the cltl-command for defconstant is a defparameter). ; However, we have begun to contemplate alternatives, as we now ; explain. ; We have run into the following problem with defconstant: the ; compiler won't let us compile certified books containing defconstant ; forms because it thinks that constants are special variables ; (because that is what the defparameter cltl-command does). What can ; we do about this problem? One idea was to temporarily redefine ; defconstant to be defparameter (during the compilation done by ; certify-book), but macrolet has only lexical scope, and anyhow Boyer ; says that it's illegal to redefine a Common Lisp function (as we did ; using setf, macro-function, and unwind-protect). ; Another possibilty is to change defconstant-fn so that it really ; does create defconstants. But the reason we use defparameter now is ; that when we undo we need to unbind (because we're always checking ; to see if something is already bound), and we can't unbind a ; constant. ; Why not just eliminate defconstant in favor of defparameter ; everywhere? This is very appealing, especially because defconstant ; is inherently not amenable to undoing. But, Boyer thinks that when ; you defconstant something to a value that is a fixnum, then the ; compiler knows it's a fixnum. This could be very important for ; speed in type-set reasoning. Without the consideration of ; arithmetic, Schelter thinks that we're only paying the price of two ; memory references for defparameter vs. one for defconstant; but a ; factor of 80 or so seems like too high a price to pay. ; So, how about allowing both defconstant and defparameter, but not ; allowing any undoing back past a defconstant? After all, we already ; have a notion of not undoing into the system initialization, so ; we're just talking about a very reasonable extension of that ; protocol. One problem with this approach is that certify-book ; currently does an include-book after a ubt, and this ubt would ; probably fail. But perhaps we can force this to work. The user ; could then develop his work using defparameter, but certify the ; final "toothbrush" book using defconstant. Perhaps defconst would ; be a convenient macro that could be redefined so as to be one or the ; other of defparameter or defconstant. With this approach it would ; probably be useful to require answering a query in order to execute ; a defconstant. ; Another option would be to have acl2::defconstant be distinct from ; lisp::defconstant, but as Boyer points out, this violates our desire ; to have such Lisp primitives available to the user that he can count ; on. Or, we could define a new package that's just like the acl2 ; package but doesn't import defconstant. But note that ; (symbol-package 'defconstant) would create different answers in the ; ACL2 package than in this package -- ouch!" ; Note: (cddr trip) here is (defconst var form val). (cond (boot-strap-flg (or (boundp (cadr (cddr trip))) (interface-er "~x0 is not boundp!" (cadr (cddr trip))))) ((equal *main-lisp-package-name* (symbol-package-name (cadr (cddr trip)))) (interface-er "It is illegal to redefine a defconst in ~ the main Lisp package, such as ~x0!" (cadr (cddr trip)))) (t (maybe-push-undo-stack 'defconst (cadr (cddr trip))) ; We do not want to eval (defconst var form) here because that will recompute ; val. But we make raw Lisp look like it did that. (setf (get (cadr (cddr trip)) 'redundant-raw-lisp-discriminator) (list* 'defconst (caddr (cddr trip)) ; form (cadddr (cddr trip)))) ; val (eval `(defparameter ,(cadr (cddr trip)) ',(cadddr (cddr trip)))))) (cond ((doc-stringp (documentation (cadr (cddr trip)) 'variable)) (setf (documentation (cadr (cddr trip)) 'variable) nil)))) (defmacro (cond (boot-strap-flg (or (fboundp (cadr (cddr trip))) (interface-er "~x0 is not fboundp!" (cadr (cddr trip))))) ((equal *main-lisp-package-name* (symbol-package-name (cadr (cddr trip)))) (interface-er "It is illegal to redefine a macro in the ~ main Lisp package, such as ~x0!" (cadr (cddr trip)))) (t (maybe-push-undo-stack 'defmacro (cadr (cddr trip))) (eval (cddr trip)))) (cond ((doc-stringp (documentation (cadr (cddr trip)) 'function)) (setf (documentation (cadr (cddr trip)) 'function) nil)))))))) ; Finally, we make sure always to leave the *current-acl2-world-key* as the ; first property on the symbol-plist of the symbol. (let ((temp (get (car trip) *current-acl2-world-key*)) (plist (symbol-plist (car trip)))) (cond ((and temp (not (eq (car plist) *current-acl2-world-key*))) (setf (symbol-plist (car trip)) (cons *current-acl2-world-key* (cons temp (remove-current-acl2-world-key plist)))))))) (defun compile-uncompiled-*1*-defuns (file &optional (fns :some) gcl-flg &aux (state *the-live-state*) (wrld (w *the-live-state*))) ; Same as compile-uncompiled-defuns, but for *1* functions. ; File should be given in Unix-style syntax. Hence for example, "TMP" is ; relative to the current directory, even though on a Macintosh this might ; appear to be an absolute pathname for a file. (setq *package* (find-package (current-package *the-live-state*))) (cond ((null fns) (warning$ 'compile-uncompiled-defuns nil "No functions to compile.") (return-from compile-uncompiled-*1*-defuns file))) (let ((*read-base* 10) (*print-base* 10) (*print-circle* nil) (*print-radix* nil) *print-pretty* *print-level* *print-length* (*readtable* *acl2-readtable*) (*print-case* :upcase) seen #+allegro (excl:*redefinition-warnings* nil) #+clisp (custom::*suppress-check-redefinition* t) (fns (cond ((eq fns :uncompiled) :some) ((eq fns t) :all) (t fns))) (fn-file (format nil "~a.lisp" file)) (os-file (pathname-unix-to-os file state)) (not-boot-strap-p (null (global-val 'boot-strap-flg wrld)))) (mv-let (chan state) (open-output-channel fn-file :character state) (pprogn (mv-let (col state) (fmt1 "; This file is automatically generated, to be compiled.~|; Feel ~ free to delete it after compilation.~|" nil 0 chan state nil) (declare (ignore col)) state) (fms! "~x0" (list (cons #\0 (list 'in-package (current-package *the-live-state*)))) chan state nil) (progn (dolist (trip wrld) (cond ((and (eq (car trip) 'command-landmark) (eq (cadr trip) 'global-value) (eq (car (last trip)) 'exit-boot-strap-mode)) ; If we are compiling while building the system, then we will never see ; 'exit-boot-strap-mode, which allows us to explore the entire world. But when ; a user compiles, the exploration should only consider user-defined events. ; That includes verify-termination applied to system functions, which is why we ; do not want to rule out functions with a '*predefined* property. This ; approach differs from what happens in compile-uncompiled-defuns for this ; verify-termination case, since verify-termination changes the symbol-function ; only for the *1*-symbol, not for the original symbol; thus compilation is ; only appropriate for the *1*-symbol, since the original function remains ; compiled. (return)) ((and (eq (car trip) 'cltl-command) (eq (cadr trip) 'global-value) (consp (cddr trip)) (eq (caddr trip) 'defuns)) (dolist (x (cdddr (cddr trip))) (let ((*1*fn (*1*-symbol (car x)))) (cond ((and (fboundp *1*fn) (not (member-eq (car x) seen)) (cond ((eq fns :some) (if not-boot-strap-p (not (compiled-function-p! *1*fn)) (not (eq (cadr (cddr trip)) :program)))) (t (or (eq fns :all) (member-eq (car x) fns))))) (let ((*1*def (cons 'defun (oneify-cltl-code (cadr (cddr trip)) ; defun-mode (consp (cdr (getprop (car x) 'recursivep nil 'current-acl2-world (w state)))) x (getprop (car x) 'stobj-function nil 'current-acl2-world wrld) wrld)))) (fms! "~x0" (list (cons #\0 *1*def)) chan state nil) (eval (make-defun-declare-form *1*def)) (push (car x) seen))))))))) (newline chan state) (close-output-channel chan state)))) (cond (gcl-flg #+gcl (compile-file (namestring (truename (pathname-unix-to-os fn-file state))) :c-file t :h-file t) #-gcl (er hard 'compile-uncompiled-defuns "The gcl-flg argument to compile-uncompiled-*1*-defuns is only legal ~ when running under GCL.")) (t (compile-file (namestring (truename (pathname-unix-to-os fn-file state)))))) (load-compiled os-file) os-file)) (defun cltl-def-from-name (fn stobj-function wrld) ; If fn does not have a 'stobj-function property in wrld, then this function ; returns the raw Lisp definition of fn, which is also the definition that is ; oneified to create the corresponding *1* function. ; But suppose that fn does have a 'stobj-function property in wrld. If ; stobj-function is non-nil, it should be that property, and we return the raw ; Lisp definition of fn. If stobj-function is, then we return the definition ; of fn that is to be oneified. (let* ((event-number (getprop (or stobj-function fn) 'absolute-event-number nil 'current-acl2-world wrld)) (cltl-command-value (and event-number (getprop 'cltl-command 'global-value nil 'any-old-world (lookup-world-index 'event event-number wrld)))) (def (and cltl-command-value (assoc-eq fn (if stobj-function (nth 4 cltl-command-value) (cdddr cltl-command-value)))))) (and def (or (null stobj-function) (not (member-equal *stobj-inline-declare* def))) (cons 'defun def)))) (defun compile-function (ctx fn state) (declare (xargs :guard (and (symbolp fn) (state-p state)))) (let ((wrld (w state))) (cond ((eq (getprop fn 'formals t 'current-acl2-world wrld) t) (er soft ctx "~x0 is not a defined function in the current ACL2 world." fn)) (t #-acl2-loop-only (let* ((stobj-function (getprop fn 'stobj-function nil 'current-acl2-world wrld)) (form (cltl-def-from-name fn stobj-function wrld)) (*1*fn (*1*-symbol fn))) (cond ((not (compiled-function-p! fn)) (cond (form (eval (make-defun-declare-form form)))) (compile fn))) (cond ((and (fboundp *1*fn) (not (compiled-function-p! *1*fn))) (eval (make-defun-declare-form (cons 'defun (oneify-cltl-code (if (eq (symbol-class fn wrld) :program) :program ; What happens here if the function is non-executable? We believe that ; functions defined by encapsulate will always have mode :logic, since LOCAL ; forms are skipped in :program mode. In fact, we believe that this function ; would be :common-lisp-compliant, and hence its oneified code will simply be a ; call of the raw lisp function, which will do a throw. But the bottom line is ; that the function body contains a throw-raw-ev-fncall, so regardless of how ; we oneify the code, we will get a function that ultimately does a throw. :logic) (consp (cdr (getprop fn 'recursivep nil 'current-acl2-world wrld))) (if stobj-function (cltl-def-from-name fn nil wrld) (cdr form)) stobj-function wrld)))) (compile *1*fn)))) (value fn))))) ; The only change in the following variable is the addition of an advertisement ; that ACL2 has been patched in openMCL, for when ACL2 first starts up (so the ; presumption is that a saved image has been built after replacing functions ; with the patched versions). (defparameter *saved-string* (concatenate 'string "~% ~a built ~a.~ ~% Copyright (C) 2004 University of Texas at Austin~ ~% ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you~ ~% are welcome to redistribute it under certain conditions. For details,~ ~% see the GNU General Public License.~%~ ~% Incorporates a patch for defstobj events with :inline t from June 2004.~%~ ~a" #+lispworks "~% Type (LP) to enter the ACL2 command loop;~ ~% then see the documentation topic note-2-~a for recent changes.~%" #-lispworks "~% See the documentation topic note-2-~a for recent changes.~%" "~% NOTE!! Proof trees are disabled in ACL2. To enable them in emacs,~ ~% look under the ACL2 source directory in interface/emacs/README.doc; ~ ~% and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 ~ ~% command loop. Look in the ACL2 documentation under PROOF-TREE.~%"))