Info file: acl2-doc-lemacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-lemacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.9 Copyright (C) 1997 Computational Logic, Inc. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.  File: acl2-doc-lemacs.info, Node: WORLD, Next: WORMHOLE, Prev: WHY-BRR, Up: MISCELLANEOUS WORLD ACL2 property lists and the ACL2 logical data base A "world" is a list of triples, each of the form (sym prop . val), implementing the ACL2 notion of property lists. ACL2 permits the simultaneous existence of many property list worlds. "The world" is often used as a shorthand for "the ACL2 logical world" which is the particular property list world used within the ACL2 system to maintain the data base of rules. Common Lisp provides the notion of "property lists" by which one can attach "properties" and their corresponding "values" to symbols. For example, one can arrange for the 'color property of the symbol 'box-14 to be 'purple and the 'color property of the symbol 'triangle-7 to be 'yellow. Access to property lists is given via the Common Lisp function get. Thus, (get 'box-14 'color) might return 'purple. Property lists can be changed via the special form setf. Thus, (setf (get 'box-14 'color) 'blue) changes the Common Lisp property list configuration so that (get 'box-14 'color) returns 'blue. It should be obvious that ACL2 cannot provide this facility, because Common Lisp's get "function" is not a function of its argument, but instead a function of some implicit state object representing the property list settings for all symbols. ACL2 provides the functions getprop and putprop which allow one to mimic the Common Lisp property list facility. However, ACL2's getprop takes as one of its arguments a list that is a direct encoding of what was above called the "state object representing the property list settings for all symbols." Because ACL2 already has a notion of "state" that is quite distinct from that used here, we call this property list object a "world." A world is just a true list of triples. Each triple is of the form (sym prop . val). This world can be thought of as a slightly elaborated form of association list and getprop is a slightly elaborated form of assoc that takes two keys. When getprop is called on a symbol, s, property p, and world, w, it scans w for the first triple whose sym is s and prop is p and returns the corresponding val. Getprop has two additional arguments, one of which that controls what it returns if no such sym and prop exist in w, and other other of which allows an extremely efficient implementation. To set some property's value for some symbol, ACL2 provides putprop. (putprop sym prop val w) merely returns a new world, w', in which (sym prop . val) has been consed onto the front of w, thus "overwriting" the prop value of sym in w to val and leaving all other properties in w unchanged. One aspect of ACL2's property list arrangment is that it is possible to have many different property list worlds. For example, 'box-14 can have 'color 'purple in one world and can have 'color 'yes in another, and these two worlds can exist simultaneously because getprop is explicitly provided the world from which the property value is to be extracted. The efficiency alluded to above stems from the fact that Common Lisp provides property lists. Using Common Lisp's provisions behind the scenes, ACL2 can "install" the properties of a given world into the Common Lisp property list state so as to make retrieval via getprop very fast in the special case that the world provided to getprop has been installed. To permit multiple installed worlds, each of which is permitted to be changed via putprop, ACL2 requires that worlds be named and these names are used to distinquish installed versions of the various worlds. At the moment we do not further document getprop and putprop. However, the ACL2 system uses a property list world, named 'current-acl2-world, in which to store the succession of user commands and their effects on the logic. This world is often referred to in our documentation as "the world" though it should be stressed that the user is permitted to have worlds and ACL2's is in no way distinguished except that the user is not permitted to modify it except via event commands. The ACL2 world is part of the ACL2 state and may be obtained via (w state). *Warning*: The ACL2 world is very large. Its length as of this writing (Version 1.5) is over 31,000 and it grows with each release. Furthermore, some of the values stored in it are pointers to old versions of itself. Printing (w state) is something you should avoid because you likely will not have the patience to await its completion. For these practical reasons, the only thing you should do with (w state) is provide it to getprop, as in the form (getprop sym prop default 'current-acl2-world (w state)) to inspect properties within it, or to pass it to ACL2 primitives, such as theory functions, where it is expected. Some ACL2 command forms, such as theory expressions (*Note THEORIES::) and the values to be stored in tables (*Note TABLE::), are permitted to use the variable symbol world freely with the understanding that when these forms are evaluated that variable is bound to (w state). Theoretically, this gives those forms complete knowledge of the current logical configuration of ACL2. However, at the moment, few world scanning functions have been documented for the ACL2 user. Instead, supposedly convenient macro forms have been created and documented. For example, (current-theory :here), which is the theory expression which returns the currently enabled theory, actually macroexpands to (current-theory-fn :here world). When evaluated with world bound to (w state), current-theory-fn scans the current ACL2 world and computes the set of runes currently enabled in it.  File: acl2-doc-lemacs.info, Node: WORMHOLE, Next: XARGS, Prev: WORLD, Up: MISCELLANEOUS WORMHOLE ld without state -- a short-cut to a parallel universe Example Form: (wormhole t 'interactive-break nil '(value 'hi!)) ; Enters a recursive read-eval-print loop ; on a copy of the "current state" and ; returns nil! General Form: (wormhole pseudo-flg name input form :current-package ... ; known package name :ld-skip-proofsp ... ; t, nil or 'include-book :ld-redefinition-action ; nil or '(:a . :b) :ld-prompt ... ; nil, t, or some prompt printer fn :ld-keyword-aliases ... ; an alist pairing keywords to parse info :ld-pre-eval-filter ... ; :all, :query, or some new name :ld-pre-eval-print ... ; nil, t, or :never :ld-post-eval-print ... ; nil, t, or :command-conventions :ld-evisc-tuple ... ; nil or '(alist nil nil level length) :ld-error-triples ... ; nil or t :ld-error-action ... ; :continue, :return, or :error :ld-query-control-alist ; alist supplying default responses :ld-verbose ...) ; nil or t The keyword arguments above are exactly those of ld (*Note LD::) except that three of ld's keyword arguments are missing: the three that specify the channels standard-oi, standard-co and proofs-co. Essentially wormhole is just a call of ld on the current state with the given keyword arguments. Wormhole always returns nil. The *amazing* thing about wormhole is that it calls ld and interacts with the user even though state is not available as an argument! Wormhole does this by manufacturing a "wormhole state," a copy of the "current state" (whatever that is) modified so as to contain some of the wormhole arguments. Ld is called on that wormhole state with the three ld channels directed to ACL2's "comment window." At the moment, the comment window is overlaid on the terminal and you cannot tell when output is going to *standard-co* and when it is going to the comment window. But we imagine that eventually a different window will pop up on your screen. In any case, the interaction provided by this call of ld does not modify the state "from which" wormhole was called, it modifies the copied state. When ld exits (e.g., in response to :q being typed in the comment window) the wormhole state evaporates and wormhole returns nil. Logically and actually (from the perspective of the ongoing computation) nothing has happened except that a "no-op" function was called and returned nil. The name wormhole is meant to suggest the idea that the function provides easy access to state in situations where it is apparently impossible to get state. Thus, for example, if you define the factorial function, say, except that you sprinkled into its body appropriate calls of wormhole, then the execution of (factorial 6) would cause interactive breaks in the comment window. During those breaks you would apparently be able to inspect the "current state" even though factorial does not take state as an argument. The whole notion of there being a "current state" during the evaluation of (factorial 6) is logically ill-defined. And yet, we know from practical experience with the sequential computing machines upon which ACL2 is implemented that there is a "current state" (to which the factorial function is entirely insensitive) and that is the state to which wormhole "tunnels." A call of wormhole from within factorial can pass factorial-specific information that is embedded in the wormhole state and made available for inspection by the user in an interactive setting. But no information ever flows out of a wormhole state: wormhole always returns nil. There are four arguments to wormhole that need further explanation: pseudo-flg, name, input, and form. Roughly speaking, the value of pseudo-flg should be t or nil and indicates whether we are actually to enter a wormhole or just return nil immediately. The actual handling of pseudo-flg is more sophisticated and is explained in detail at the end of this documentation. Name and input are used as follows. Recall that wormhole copies the "current state" and then modifies it slightly to obtain the state upon which ld is called. We now describe the modifications. First, the state global variable 'wormhole-name is set to name, which may be any non-nil ACL2 object but is usually a symbol. Then, 'wormhole-input is set to input, which may be any ACL2 object. Finally, and inexplicably, 'wormhole-output is set to the value of 'wormhole-output the last time a wormhole named name was exited (or nil if this is the first time a wormhole named name was entered). this last aspect of wormholes, namely the preservation of 'wormhole-output, allows all the wormholes of a given name to communicate with each other. We can now explain how form is used. The modified state described above is the state on which ld is called. However, standard-oi --- the input channel from which ld reads commands -- is set so that the first command that ld reads and evaluates is form. If form returns an error triple with value :q, i.e., form returns via (value :q), then no further commands are read, ld exits, and the wormhole exits and returns nil. But if form returns any other value (or is not an error triple), then subsequent commands are read from the comment window. As usual, the ld-specials affect whether a herald is printed upon entry, whether form is printed before evaluation, whether a prompt is printed, how errors are handled, etc. The ld-specials can be specified with the corresponding arguments to wormhole. It is standard practice to call wormhole so that the entry to ld and the evaluation of form are totally silent. Then, tests in form can inspect the state and decide whether user interaction is desired. If so, form can appropriately set ld-prompt, ld-error-action, etc., print a herald, and then return (value :invisible). Recall (*Note LD::) that (value :invisible) causes ld not to print a value for the just executed form. The result of this arrangement is that whether interaction occurs can be based on tests that are performed on the wormhole state after (@ wormhole-input) and the last (@ wormhole-output) are available for inspection. This is important because outside the wormhole you can access wormhole-input (you are passing it into the wormhole) but you may not be able to access the current state (because you might be in factorial) and you definitely cannot access the wormhole-output of the last wormhole because it is not part of the ACL2 state. Thus, if the condition under which you wish to interact depends upon the state or that part of it preserved from the last wormhole interaction, that condition can only be tested from within the wormhole, via form. It is via this mechanism that break-rewrite (*Note BREAK-REWRITE::) is implemented. To be more precise, the list of monitored runes is maintained as part of the preserved wormhole-output of the break-rewrite wormhole. Because it is not part of the normal state, it may be changed by the user during proofs. That is what allows you to install new monitors while debugging proofs. But that means that the list of monitored runes cannot be inspected from outside the wormhole. Therefore, to decide whether a break is to occur when a given rule is applied, the rewriter must enter the break-rewrite wormhole, supplying a form that causes interaction if the given rule's break condition is satisfied. The user perceives this as though the wormhole was conditionally entered -- a perception that is happily at odds with the informed user's knowledge that the list of monitored runes is not part of the state. In fact, the wormhole was unconditionally entered and the condition was checked from within the wormhole, that being the only state in which the condition is known. Another illustrative example is available in the implemention of the monitor command. How can we add a new rune to the list of monitored runes while in the normal ACL2 state (i.e., while not in a wormhole)? The answer is: by getting into a wormhole. In particular, when you type (monitor rune expr) at the top-level of ACL2, monitor enters the break-rewrite wormhole with a cleverly designed first form. That form adds rune and expr to the list of monitored runes -- said list only being available in break-rewrite wormhole states. Then the first form returns (value :q), which causes us to exit the wormhole. By using ld-specials that completely suppress all output during the process, it does not appear to the user that a wormhole was entered. The moral here is rather subtle: the first form supplied to wormhole may be the entire computation you want to perform in the wormhole; it need not just be a predicate that decides if interaction is to occur. Using wormholes of different names you can maintain a variety of "hidden" data structures that are always accessible (whether passed in or not). This appears to violate completely the applicative semantics of ACL2, but it does not: because these data structures are only accessible via wormholes, it is impossible for them to affect any ACL2 computation (except in the comment window). As one might imagine, there is some overhead associated with entering a wormhole because of the need to copy the current state. This brings us back to pseudo-flg. Ostensibly, wormhole is a function and hence all of its argument expressions are evaluated outside the function (and hence, outside the wormhole it creates) and then their values are passed into the function where an appropriate wormhole is created. In fact, wormhole is a macro that permits the pseudo-flg expression to peer dimly into the wormhole that will be created before it is created. In particular, pseudo-flg allows the user to access the wormhole-output that will be used to create the wormhole state. This is done by allowing the user to mention the (apparently unbound) variable wormhole-output in the first argument to wormhole. Logically, wormhole is a macro that wraps (let ((wormhole-output nil)) ...) around the expression supplied as its first argument. So logically, wormhole-output is always nil when the expression is evaluated. However, actually, wormhole-output is bound to the value of (@ wormhole-output) on the last exit from a wormhole of the given name (or nil if this is the first entrance). Thus, the pseudo-flg expression, while having to handle the possibility that wormhole-output is nil, will sometimes see non-nil values. The next question is, of course, "But how can you get away with saying that logically wormhole-output is always nil but actually it is not? That doesn't appear to be sound." But it is sound because whether pseudo-flg evaluates to nil or non-nil doesn't matter, since in either case wormhole returns nil. To make that point slightly more formal, imagine that wormhole did not take pseudo-flg as an argument. Then it could be implemented by writing (if pseudo-flg (wormhole name input form ...) nil). Now since wormhole always returns nil, this expression is equivalent to (if pseudo-flg nil nil) and we see that the value of pseudo-flg is irrelevant. So we could in fact allow the user to access arbitrary information to decide which branch of this if to take. We allow access to wormhole-output because it is often all that is needed. We don't allow access to state (unless state is available at the level of the wormhole call) for technical reasons having to do with the difficulty of overcoming translate's prohibition of the sudden appearance of the variable state. We conclude with an example of the use of pseudo-flg. This example is a simplification of our implementation of break-rewrite. To enter break-rewrite at the beginning of the attempted application of a rule, rule, we use (wormhole (and (f-get-global 'brr-mode state) (member-equal (access rewrite-rule rule :rune) (cdr (assoc-eq 'monitored-runes wormhole-output)))) 'break-rewrite ...) The function in which this call of wormhole occurs has state as a formal. The pseudo-flg expression can therefore refer to state to determine whether 'brr-mode is set. But the pseudo-flg expression above mentions the variable wormhole-output; this variable is not bound in the context of the call of wormhole; if wormhole were a simple function symbol, this expression would be illegal because it mentions a free variable. However, it is useful to think of wormhole as a simple function that evaluates all of its arguments but to also imagine that somehow wormhole-output is magically bound around the first argument so that wormhole-output is the output of the last break-rewrite wormhole. If we so imagine, then the pseudo-flg expression above evaluates either to nil or non-nil and we will enter the wormhole named break-rewrite in the latter case. Now what does the pseudo-flg expression above actually test? We know the format of our own wormhole-output because we are responsible for maintaining it. In particular, we know that the list of monitored runes can be obtained via (cdr (assoc-eq 'monitored-runes wormhole-output)). Using that knowledge we can design a pseudo-flg expression which tests whether (a) we are in brr-mode and (b) the rune of the current rule is a member of the monitored runes. Question (a) is answered by looking into the current state. Question (b) is answered by looking into that part of the about-to-be-created wormhole state that will differ from the current state. To reiterate the reason we can make wormhole-output available here even though it is not in the current state: logically speaking the value of wormhole-output is irrelevant because it is only used to choose between two identical alternatives. This example also makes it clear that pseudo-flg provides no additional functionality. The test made in the pseudo-flg expression could be moved into the first form evaluated by the wormhole -- changing the free variable wormhole-output to (@ wormhole-output) and arranging for the first form to return (value :q) when the pseudo-flg expression returns nil. The only reason we provide the pseudo-flg feature is because it allows the test to be carried out without the overhead of entering the wormhole. Wormholes can be used not only in :program mode definitions but also in :logic mode definitions. Thus, it is possible (though somewhat cumbersome without investing in macro support) to annotate logical functions with output facilities that do not require STATE. These facilities do not complicate proof obligations. Suppose then that one doctored a simple function, e.g., APP, so as to do some printing and then proved that APP is associative. The proof may generate extraneous output due to the doctoring. Furthermore, contrary to the theorem proved, execution of the function appears to affect *standard-co*. To see what the function "really" does when evaluated, enter raw lisp and set the global variable *inhibit-wormhole-activityp* to t.  File: acl2-doc-lemacs.info, Node: XARGS, Prev: WORMHOLE, Up: MISCELLANEOUS XARGS giving hints to defun Common Lisp's defun function does not easily allow one to pass extra arguments such as "hints". ACL2 therefore supports a peculiar new declaration (*Note DECLARE::) designed explicitly for passing additional arguments to defun via a keyword-like syntax. The following declaration is nonsensical but does illustrate all of the xargs keywords: (declare (xargs :guard (symbolp x) :measure (- i j) :well-founded-relation my-wfr :hints (("Goal" :in-theory (theory batch1))) :guard-hints (("Goal" :in-theory (theory batch1))) :mode :logic :verify-guards t :otf-flg t)) General Form: (xargs :key1 val1 ... :keyn valn) where the keywords and their respective values are as shown below. Note that once "inside" the xargs form, the "extra arguments" to defun are passed exactly as though they were keyword arguments. :GUARD Value is a term involving only the formals of the function being defined. The actual guard used for the definition is the conjunction of all the guards and types (*Note DECLARE::) declared. :GUARD-HINTS Value: hints (*Note HINTS::), to be used during the guard verification proofs as opposed to the termination proofs of the defun. :MEASURE Value is a term involving only the formals of the function being defined. This term is indicates what is getting smaller in the recursion. The well-founded relation with which successive measures are compared is e0-ord-<. :WELL-FOUNDED-RELATION Value is a function symbol that is known to be a well-founded relation in the sense that a rule of class :well-founded-relation has been proved about it. *Note WELL-FOUNDED-RELATION::. :HINTS Value: hints (*Note HINTS::), to be used during the termination proofs as opposed to the guard verification proofs of the defun. :MODE Value is :program or :logic, indicating the defun mode of the function introduced. *Note DEFUN-MODE::. If unspecified, the defun mode defaults to the default defun mode of the current world. To convert a function from :program mode to :logic mode, *Note VERIFY-TERMINATION::. :VERIFY-GUARDS Value is t or nil, indicating whether or not guards are to be verified upon completion of the termination proof. This flag should only be t if the :mode is unspecified but the default defun mode is :logic, or else the :mode is :logic. :OTF-FLG Value is a flag indicating "onward through the fog" (*Note OTF-FLG::).  File: acl2-doc-lemacs.info, Node: OTHER, Next: PROGRAMMING, Prev: MISCELLANEOUS, Up: Top OTHER other commonly used top-level functions * Menu: * atsign:: (@) get the value of a global variable in state * ACL2-DEFAULTS-TABLE:: a table specifying certain defaults, e.g., the default defun-mode * ASSIGN:: assign to a global variable in state * CERTIFY-BOOK!:: a variant of certify-book * COMP:: compile some ACL2 functions * GOOD-BYE:: quit entirely out of Lisp * LD:: the ACL2 read-eval-print loop, file loader, and command processor * PROPS:: print the ACL2 properties on a symbol * Q:: quit ACL2 (type :q) -- reenter with (lp) * REBUILD:: a convenient way to reconstruct your old state * RESET-LD-SPECIALS:: restores initial settings of the ld specials * SET-GUARD-CHECKING:: control checking guards during execution of top-level forms * SET-INHIBIT-OUTPUT-LST:: control output * SKIP-PROOFS:: skip proofs for an event -- a quick way to introduce unsoundness * THM:: prove a theorem * TRANS:: print the macroexpansion of a form * TRANS1:: print the one-step macroexpansion of a form Related topics other than immediate subtopics: * CERTIFY-BOOK:: how to produce a certificate for a book This section contains an assortment of functions that fit into none of the other categories and yet are suffiently useful as to merit "advertisement" in the :help command.  File: acl2-doc-lemacs.info, Node: atsign, Next: ACL2-DEFAULTS-TABLE, Prev: OTHER, Up: OTHER @ get the value of a global variable in state Examples: (+ (@ y) 1) (assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B)) General Form: (@ symbol) where symbol is any symbol to which you have assigned a global value. This macro expands into (f-get-global 'symbol state), which retrieves the stored value of the symbol. The macro assign makes it convenient to set the value of a symbol. The :ubt operation has no effect on the global-table of state. Thus, you may use these globals to hang onto useful data structures even though you may undo back past where you computed and saved them.  File: acl2-doc-lemacs.info, Node: ACL2-DEFAULTS-TABLE, Next: ASSIGN, Prev: atsign, Up: OTHER ACL2-DEFAULTS-TABLE a table specifying certain defaults, e.g., the default defun-mode Example Forms: (table acl2-defaults-table :defun-mode) ; current default defun-mode (table acl2-defaults-table :defun-mode :program) ; set default defun-mode to :program *Note TABLE:: for a discussion of tables in general. The legal keys for this table are shown below. They may be accessed and changed via the general mechanisms provided by tables. However, there are often more convenient ways to access and/or change the defaults. (See also the note below.) :defun-mode the default defun-mode, which must be :program or :logic. *Note DEFUN-MODE:: for a general discussion of defun-modes. The :defun-mode key may be conveniently set by keyword commands naming the new defun-mode, :program and :logic. *Note PROGRAM:: and *Note LOGIC::. :verify-guards-eagerness an integer between 0 and 2 indicating how eager the system is to verify the guards of a defun event. *Note SET-VERIFY-GUARDS-EAGERNESS::. :compile-fns When this key's value is t, functions are compiled when they are defun'd; otherwise, the value is nil. To set the flag, *Note SET-COMPILE-FNS::. :measure-function the default measure function used by defun when no :measure is supplied in xargs. The default measure function must be a function symbol of one argument. Let mfn be the default measure function and suppose no :measure is supplied with some recursive function definition. Then defun finds the first formal, var, that is tested along every branch and changed in each recursive call. The system then "guesses" that (mfn var) is the :measure for that defun. :well-founded-relation the default well-founded relation used by defun when no :well-founded-relation is supplied in xargs. The default well-founded relation must be a function symbol, rel, of two arguments about which a :well-founded-relation rule has been proved. *Note WELL-FOUNDED-RELATION::. :invisible-fns-alist an alist used in the control of permutative rewriting. Each entry in this alist must be of the form (fn ufn1 ufn2 ... ufnk), where fn and each ufni is a function symbol and the ufni are all unary functions. Such an entry makes each of the ufni "invisible" when ordering the arguments of fn via commutative rules. *Note SET-INVISIBLE-FNS-ALIST::. :irrelevant-formals-ok When this key's value is t, the check for irrelevant formals is bypassed; otherwise, the value is the keyword nil (the default). *Note IRRELEVANT-FORMALS:: and *Note SET-IRRELEVANT-FORMALS-OK::. :ignore-ok When this key's value is t, the check for ignored variables is bypassed; otherwise, the value is the keyword nil (the default). *Note SET-IGNORE-OK::. :inhibit-warnings ACL2 prints warnings that may, from time to time, seem excessive to experienced users. Each warning is "labeled" with a string identifying the type of warning. Consider for example ACL2 Warning [Use] in ( THM ...): It is unusual to :USE .... Here, the label is "Use". The value of the key :inhibit-warnings is a list of such labels, where case is ignored. Any warning whose label is a member of this list (where again, case is ignored) is suppressed. *Note SET-INHIBIT-WARNINGS:: and also *Note SET-INHIBIT-OUTPUT-LST::. :bdd-constructors This key's value is a list of function symbols used to define the notion of "BDD normal form." *Note BDD-ALGORITHM:: and *Note HINTS::. :state-ok This key's value is either t or nil and indicates whether the user is aware of the syntactic restrictions on the variable symbol STATE. *Note SET-STATE-OK::. Note: Unlike all other tables, acl2-defaults-table can affect the soundness of the system. The table mechanism therefore enforces on it a restriction not imposed on other tables: when table is used to update the acl2-defaults-table, the key and value must be variable-free forms. Thus, while (table acl2-defaults-table :defun-mode :program), (table acl2-defaults-table :defun-mode ':program), and (table acl2-defaults-table :defun-mode (compute-mode *my-data*)) are all examples of legal events (assuming compute-mode is a function of one non-state argument that produces a defun-mode as its single value), (table acl2-defaults-table :defun-mode (compute-mode (w state))) is not legal because the value form is state-sensitive. Consider for example the following three events which one might make into the text of a book. (in-package "ACL2") (table acl2-defaults-table :defun-mode (if (ld-skip-proofsp state) :logic :program)) (defun crash-and-burn (x) (car x)) The second event is illegal because its value form is state-sensitive. If it were not illegal, then it would set the :defun-mode to :program when the book was being certified but would set the defun-mode to :logic when the book was being loaded by include-book. That is because during certification, ld-skip-proofsp is nil (proof obligations are generated and proved), but during book inclusion ld-skip-proofsp is non-nil (those obligations are assumed to have been satisfied.) Thus, the above book, when loaded, would create a function in :logic mode that does not actually meet the conditions for such status. For similar reasons, table events affecting acl2-defaults-table are illegal within the scope of local forms. That is, the text (in-package "ACL2") (local (table acl2-defaults-table :defun-mode :program)) (defun crash-and-burn (x) (car x)) is illegal because acl2-defaults-table is changed locally. If this text were acceptable as a book, then when the book was certified, crash-and-burn would be processed in :program mode, but when the certified book was included later, crash-and-burn would have :logic mode because the local event would be skipped. The text (in-package "ACL2") (program) ;which is (table acl2-defaults-table :defun-mode :program) (defun crash-and-burn (x) (car x)) is acceptable and defines crash-and-burn in :program mode, both during certification and subsequent inclusion. We conclude with an important observation about the relation between acl2-defaults-table and include-book, certify-book, and encapsulate. Including or certifying a book never has an effect on the acl2-defaults-table, nor does executing an encapsulate event; we always restore the value of this table as a final act. (Also *Note INCLUDE-BOOK::, *Note ENCAPSULATE::, and *Note CERTIFY-BOOK::.) That is, no matter how a book fiddles with the acl2-defaults-table, its value immediately after including that book is the same as immediately before including that book. If you want to set the acl2-defaults-table in a way that persists, you need to do so using commands that are not inside books. It may be useful to set your favorite defaults in your acl2-customization file; *Note ACL2-CUSTOMIZATION::.  File: acl2-doc-lemacs.info, Node: ASSIGN, Next: CERTIFY-BOOK!, Prev: ACL2-DEFAULTS-TABLE, Up: OTHER ASSIGN assign to a global variable in state Examples: (assign x (expt 2 10)) (assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B)) General Form: (assign symbol term) where symbol is any symbol (with certain enforced exclusions to avoid overwriting ACL2 system "globals") and term is any ACL2 term that could be evaluated at the top-level. Assign evaluates the term, stores the result as the value of the given symbol in the global-table of state, and returns the result. (Note: the actual implementation of the storage of this value is much more efficient than this discussion of the logic might suggest.) Assign is a macro that effectively expands to the more complicated but understandable: (pprogn (f-put-global 'symbol term state) (mv nil (f-get-global 'symbol term state) state)). The macro @ gives convenient access to the value of such globals. The :ubt operation has no effect on the global-table of state. Thus, you may use these globals to hang onto useful data structures even though you may undo back past where you computed and saved them.  File: acl2-doc-lemacs.info, Node: CERTIFY-BOOK!, Next: COMP, Prev: ASSIGN, Up: OTHER CERTIFY-BOOK! a variant of certify-book Examples: (certify-book! "my-arith" 3) ;Certify in a world with 3 ; commands, starting in a world ; with at least 3 commands. (certify-book! "my-arith") ;Certify in the initial world. (certify-book! "my-arith" 0 nil) ;As above, but do not compile. General Form: (certify-book! book-name k compile-flg) where book-name is a book name (*Note BOOK-NAME::), k is a nonnegative integer used to indicate the "certification world," and compile-flg indicates whether you wish to compile the (functions in the) book. This command is identical to certify-book, except that the second argument k may not be t in certify-book! and if k exceeds the current command number, then an appropriate ubt! will be executed first. *Note CERTIFY-BOOK:: and *Note UBT!::.  File: acl2-doc-lemacs.info, Node: COMP, Next: GOOD-BYE, Prev: CERTIFY-BOOK!, Up: OTHER COMP compile some ACL2 functions Examples: :comp t ; compile all uncompiled ACL2 functions :comp foo ; compile the defined function foo :comp (foo bar) ; compile the defined functions foo and bar General Form: :comp specifier where specifier is one of the following: t compile all defined ACL2 functions that are currently uncompiled (name-1 ... name-k) a non-empty list of names of functions defined by DEFUN in ACL2 name same as (name) Note: Unless a single function is specified (either as a symbol or as a one-element list containing its name), ACL2 will write out files "TMP.lisp" and "TMP1.lisp" (the latter is for the executable counterparts; *Note EXECUTABLE-COUNTERPART::) that are subsequently compiled. Also *Note SET-COMPILE-FNS:: for a way to get each function to be compiled as you go along.  File: acl2-doc-lemacs.info, Node: GOOD-BYE, Next: LD, Prev: COMP, Up: OTHER GOOD-BYE quit entirely out of Lisp Example: ACL2 !>:good-bye *Note: Your entire session will disappear forever when you type* :good-bye. The command :good-bye quits not only out of the ACL2 command loop, but in fact quits entirely out of the underlying Lisp. Thus, there is no going back! You will *not* be able to re-enter the command loop after typing :good-bye! All your work will be lost!!! This command may not work in some underlying Common Lisp implementations. But we don't expect there to be any harm in trying. It *does* work in AKCL and GCL, at least as of this writing. If you merely want to exit the ACL2 command loop, use :q instead (*Note Q::).  File: acl2-doc-lemacs.info, Node: LD, Next: PROPS, Prev: GOOD-BYE, Up: OTHER LD the ACL2 read-eval-print loop, file loader, and command processor Example: (LD standard-oi ; open obj in channel, stringp file name ; to open and close, or list of forms ; Optional keyword arguments: :standard-co ... ; open char out or file to open and close :proofs-co ... ; open char out or file to open and close :current-package ... ; known package name :ld-skip-proofsp ... ; nil, 'include-book, t, or ; *Note LD-SKIP-PROOFSP:: :ld-redefinition-action ; nil or '(:a . :b) :ld-prompt ... ; nil, t, or some prompt printer fn :ld-keyword-aliases ... ; an alist pairing keywords to parse info :ld-pre-eval-filter ... ; :all, :query, or some new name :ld-pre-eval-print ... ; nil, t, or :never :ld-post-eval-print ... ; nil, t, or :command-conventions :ld-evisc-tuple ... ; nil or '(alist nil nil level length) :ld-error-triples ... ; nil or t :ld-error-action ... ; :return (default), :continue or :error :ld-query-control-alist ; alist supplying default responses :ld-verbose ...) ; nil or t Ld is the top-level ACL2 read-eval-print loop. (When you call lp, a little initialization is done in raw Common Lisp and then ld is called.) ld is also a general-purpose ACL2 file loader and a command interpreter. Ld is actually a macro that expands to a function call involving state. Ld returns an "error/value/state" triple as explained below. The arguments to ld all happen to be global variables in state. For example, 'current-package and 'ld-verbose are global variables, which may be accessed via (@ current-package) and (@ ld-verbose). When ld is called, it "binds" these variables. By "binds" we actually mean the variables are globally set but restored to their old values on exit. Because ld provides the illusion of state global variables being bound, they are called "ld specials" (after the Lisp convention of calling a variable "special" if it is referenced freely after having been bound). Note that all arguments but the first are passed via keyword. Any variable not explicitly given a value in a call retains its pre-call value, with the exception of :ld-error-action, which defaults to :return if not explicitly specified. Just as an example to drive the point home: If current-package is "ACL2" and you typed (ld *standard-oi* :current-package "MY-PKG") you would find yourself in (an inner) read-eval-print loop in which the current-package was "MY-PKG". You could operate there as long as you wished, changing the current package at will. But when you typed :q you would return to the outer read-eval-print loop where the current package would still be "ACL2". Roughly speaking, ld repeatedly reads a form from standard-oi, evaluates it, and prints its result to standard-co. It does this until the form evaluates to an error triple whose value component is :q or until the input channel or list is emptied. However, ld has many bells and whistles controlled by the ld specials. Each such special is documented individually. For example, see the documentation for standard-oi, current-package, ld-pre-eval-print, etc. A more precise description of ld is as follows. In the description below we use the ld specials as variables, e.g., we say "a form is read from standard-oi." By this usage we refer to the current value of the named state global variable, e.g., we mean "a form is read from the current value of 'standard-oi." This technicality has an important implication: If while interacting with ld you change the value of one of the ld specials, e.g., 'standard-oi, you will change the behavior of ld, e.g., subsequent input will be taken from the new value. Three ld specials are treated as channels: standard-oi is treated as an object input channel and is the source of forms evaluated by ld; standard-co and proofs-co are treated as character output channels and various flavors of output are printed to them. However, the supplied values of these specials need not actually be channels; several special cases are recognized. If the supplied value of one of these is in fact an open channel of the appropriate type, that channel is used and is not closed by ld. If the supplied value of one of these specials is a string, the string is treated as a file name and a channel of the appropriate type is opened to/from that file. (Note that ld does *not* support structured pathnames, as described in the documentation for pathname.) Any channel opened by ld during the binding of the ld specials is automatically closed by ld upon termination. If standard-co and proofs-co are equal strings, only one channel to that file is opened and is used for both. Several other alternatives are allowed for standard-oi. If standard-oi is a true list then it is taken as the list of forms to be processed. If standard-oi is a list ending in an open channel, then ld processes the forms in the list and then reads and processes the forms from the channel. Analogously, if standard-oi is a list ending a string, an object channel from the named file is opened and ld processes the forms in the list followed by the forms in the file. That channel is closed upon termination of ld. The remaining ld specials are handled more simply and generally have to be bound to one of a finite number of tokens described in the :doc entries for each ld special. Should any ld special be supplied an inappropriate value, an error message is printed. Next, if ld-verbose is t, ld prints the message "ACL2 loading name" where name names the file or channel from which forms are being read. At the conclusion of ld, it will print "Finished loading name" if ld-verbose is t. Finally, ld repeatedly executes the ACL2 read-eval-print step, which may be described as follows. A prompt is printed to standard-co if ld-prompt is non-nil. The format of the prompt is determined by ld-prompt. If it is t, the default ACL2 prompt is used. If it is any other non-nil value then it is treated as an ACL2 function that will print the desired prompt. *Note LD-PROMPT::. In the exceptional case where ld's input is coming from the terminal (*standard-oi*) but its output is going to a different sink (i.e., standard-co is not *standard-co*), we also print the prompt to the terminal. Ld then reads a form from standard-oi. If the object read is a keyword, ld constructs a "keyword command form" by possibly reading several more objects. *Note KEYWORD-COMMANDS::. This construction process is sensitive to the value of ld-keyword-aliases. *Note LD-KEYWORD-ALIASES::. Otherwise, the object read is treated as the command form. Ld next decides whether to evaluate or skip this form, depending on ld-pre-eval-filter. Initially, the filter must be either :all, :query, or a new name. If it is :all, it means all forms are evaluated. If it is :query, it means each form that is read is displayed and the user is queried. Otherwise, the filter is a name and each form that is read is evaluated as long as the name remains new, but if the name is ever introduced then no more forms are read and ld terminates. *Note LD-PRE-EVAL-FILTER::. If the form is to be evaluated, first prints the form to standard-co, if ld-pre-eval-print is t. With this feature, ld can process an input file or form list and construct a script of the session that appears as though each form was typed in. *Note LD-PRE-EVAL-PRINT::. Ld then evaluates the form, with state bound to the current state. The result is some list of multiple values. If a state is among the values, then ld uses that state as the subsequent current state. Depending on ld-error-triples, ld may interpret the result as an "error." *Note LD-ERROR-TRIPLES::. We first discuss ld's behavior if no error signal is detected (either because none was sent or because ld is ignoring them as per ld-error-triples). In the case of a non-erroneous result, ld does two things: First, if the logical world in the now current state is different than the world before execution of the form, ld adds to the world a "command landmark" containing the form evaluated. *Note COMMAND-DESCRIPTOR::. Second, ld prints the result to standard-co, according to ld-post-eval-print. If ld-post-eval-print is nil, no result is printed. If it is t, all of the results are printed as a list of multiple values. Otherwise, it is :command-conventions and only the non-erroneous "value" component of the result is printed. *Note LD-POST-EVAL-PRINT::. Whenever ld prints anything (whether the input form, a query, or some results) it "eviscerates" it if ld-evisc-tuple is non-nil. Essentially, evisceration is a generalization of Common Lisp's use of *print-level* and *print-length* to hide large substructures. *Note LD-EVISC-TUPLE::. We now return to the case of a form whose evaluation signals an error. In this case, ld first restores the ACL2 logical world to what it was just before the erroneous form was evaluated. Thus, a form that partially changes the world (i.e., begins to store properties) and then signals an error, has no effect on the world. You may see this happen on commands that execute several events (e.g., an encapsulate or a progn of several defuns): even though the output makes it appear that the initial events were executed, if an error is signalled by a later event the entire block of events is discarded. After rolling back, ld takes an action determined by ld-error-action. If the action is :continue, ld merely iterates the read-eval-print step. Note that nothing suggestive of the value of the "erroneous" form is printed. If the action is :return, ld terminates normally. If the action is :error, ld terminates signalling an error to its caller. If its caller is in fact another instance of ld and that instance is watching out for error signals, the entire world created by the erroneous inner ld will be discarded by the outer ld. Ld returns an error triple, (mv erp val state). Erp is t or nil indicating whether an error is being signalled. If no error is signalled, val is the "reason" ld terminated and is one of :exit (meaning :q was read), :eof (meaning the input source was exhausted), :error (meaning an error occurred but has been supressed) or :filter (meaning the ld-pre-eval-filter terminated ld).  File: acl2-doc-lemacs.info, Node: PROPS, Next: Q, Prev: LD, Up: OTHER PROPS print the ACL2 properties on a symbol Example: :props assoc-eq Props takes one argument, a symbol, and prints all of the properties that are on that symbol in the ACL2 world.  File: acl2-doc-lemacs.info, Node: Q, Next: REBUILD, Prev: PROPS, Up: OTHER Q quit ACL2 (type :q) -- reenter with (lp) Example: ACL2 !>:Q The keyword command :q typed at the top-level of the ACL2 loop will terminate the loop and return control to the Common Lisp top-level (or, more precisely, to whatever program invoked lp). To reenter the ACL2 loop, execute (acl2::lp) in Common Lisp. You will be in the same state as you were when you exited with :q, unless during your stay in Common Lisp you messed the data structures representating the ACL2 state. Unlike all other keyword commands, typing :q is not equivalent to invoking the function q. There is no function q.  File: acl2-doc-lemacs.info, Node: REBUILD, Next: RESET-LD-SPECIALS, Prev: Q, Up: OTHER REBUILD a convenient way to reconstruct your old state Examples: ACL2 !>(rebuild "project.lisp") ACL2 !>(rebuild "project.lisp" t) ACL2 !>(rebuild "project.lisp" :all) ACL2 !>(rebuild "project.lisp" :query) ACL2 !>(rebuild "project.lisp" 'lemma-22) Rebuild allows you to assume all the commands in a given file or list, supplied in the first argument. Because rebuild processes an arbitrary sequence of commands with ld-skip-proofsp t, it is unsound! However, if each of these commands is in fact admissible, then processing them with rebuild will construct the same logical state that you would be in if you typed each command and waited through the proofs again. Thus, rebuild is a way to reconstruct a state previously obtained by proving your way through the commands. The second, optional argument to rebuild is a "filter" (*Note LD-PRE-EVAL-FILTER::) that lets you specify which commands to process. You may specify t, :all, :query, or a new logical name. t and :all both mean that you expect the entire file or list to be processed. :query means that you will be asked about each command in turn. A new name means that all commands will be processed as long as the name is new, i.e., rebuild will stop processing commands immediately after executing a command that introduces name. Rebuild will also stop if any command causes an error. You may therefore wish to plant an erroneous form in the file, e.g., (mv t nil state), (*Note LD-ERROR-TRIPLES::), to cause rebuild to stop there. The form (i-am-here) is such a pre-defined form. If you do not specify a filter, rebuild will query you for one. Inspection of the definition of rebuild, e.g., via :pc rebuild-fn, will reveal that it is just a glorified call to the function ld. *Note LD:: if you find yourself wishing that rebuild had additional functionality.