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: IMMEDIATE-FORCE-MODEP, Next: IN-PACKAGE, Prev: I-AM-HERE, Up: MISCELLANEOUS IMMEDIATE-FORCE-MODEP when executable counterpart is enabled, forced hypotheses are attacked immediately This function symbol is defined simply to provide a rune which can be enabled and disabled. Enabling (:executable-counterpart immediate-force-modep) causes ACL2 to attack forced hypotheses immediately instead of delaying them to the next forcing round. Example Hints :in-theory (disable (:executable-counterpart immediate-force-modep)) ; delay forced hyps to forcing round :in-theory (enable (:executable-counterpart immediate-force-modep)) ; split on forced hyps immediately *Note FORCE:: for background information. When a forced hypothesis cannot be established a record is made of that fact and the proof continues. When the proof succeeds a "forcing round" is undertaken in which the system attempts to prove each of the forced hypotheses explicitly. However, if the rune (:executable-counterpart immediate-force-modep) is enabled at the time the hypothesis is forced, then ACL2 does not delay the attempt to prove that hypothesis but undertakes the attempt more or less immediately.  File: acl2-doc-lemacs.info, Node: IN-PACKAGE, Next: INVISIBLE-FNS-ALIST, Prev: IMMEDIATE-FORCE-MODEP, Up: MISCELLANEOUS IN-PACKAGE select current package Example: (in-package "MY-PKG") General Form: (in-package str) where str is a string that names an existing ACL2 package, i.e., one of the initial packages such as "KEYWORD" or "ACL2" or a package introduced with defpkg. For a complete list of the known packages created with defpkg, evaluate (strip-cars (known-package-alist state)). *Note DEFPKG::. In-package forms can only be typed at the top-level of the ACL2 loop and as the first form in a file being loaded or compiled.  File: acl2-doc-lemacs.info, Node: INVISIBLE-FNS-ALIST, Next: KEYWORD-COMMANDS, Prev: IN-PACKAGE, Up: MISCELLANEOUS INVISIBLE-FNS-ALIST functions that are invisible to the loop-stopper algorithm Examples: ACL2 !>(invisible-fns-alist (w state)) ((binary-+ unary--) (binary-* unary-/) (unary-- unary--) (unary-/ unary-/)) Among other things, the setting above has the effect of making unary-- "invisible" for the purposes of applying permutative :rewrite rules to binary-+ trees. *Note SET-INVISIBLE-FNS-ALIST::. The notion of "invisible functions" has to do with the control mechanism on permutative :rewrite rules. *Note LOOP-STOPPER:: for a detailed discussion of the control mechanism. *Note SET-INVISIBLE-FNS-ALIST:: for a discussion of how to set the invisible functions alist.  File: acl2-doc-lemacs.info, Node: KEYWORD-COMMANDS, Next: LD-ERROR-ACTION, Prev: INVISIBLE-FNS-ALIST, Up: MISCELLANEOUS KEYWORD-COMMANDS how keyword commands are processed Examples: user type-in form evaluated :pc 5 (ACL2::PC '5) :pcs app rev (ACL2::PCS 'app 'rev) :length (1 2 3) (ACL2::LENGTH '(1 2 3)) When a keyword, :key, is read as a command, ACL2 determines whether the symbol with the same name in the "ACL2" package, acl2::key, is a function or simple macro of n arguments. If so, ACL2 reads n more objects, obj1, ..., objn, and then acts as though it had read the following form (for a given key): (ACL2::key 'obj1 ... 'objn) Thus, by using the keyword command hack you avoid typing the parentheses, the "ACL2" package name, and the quotation marks. Note the generality of this hack. Almost any function or macro in the "ACL2" package can be so invoked, not just "commands." Indeed, there is no such thing as a distinguished class of commands. The one caveat is that the keyword hack can be used to invoke a macro only if that macro has a simple argument list -- one containing no lambda keywords (such as &rest), since they complicate or render impossible the task of deciding how many objects to read. Users may take advantage of the keyword command hack by defining functions and macros in the "ACL2" package.  File: acl2-doc-lemacs.info, Node: LD-ERROR-ACTION, Next: LD-ERROR-TRIPLES, Prev: KEYWORD-COMMANDS, Up: MISCELLANEOUS LD-ERROR-ACTION determines ld's response to an error Ld-error-action is an ld special (*Note LD::). The accessor is (ld-error-action state) and the updater is (set-ld-error-action val state). Ld-error-action must be :continue, :return, or :error. The initial value of ld-error-action is :continue, which means that the top-level ACL2 command loop will not exit when an error is caused by user-typein. But the default value for ld-error-action on calls of ld is :return. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-error-action is one of them. If, while ld-error-triples is t, a form evaluates to three results, the first of which is non-nil and the third of which is state, an error is said to have occurred. If an error occurs, ld's action depends on ld-error-action. If it is :continue, ld just continues processing the forms in standard-oi. If it is :return, ld stops and returns as though it had emptied the channel. If it is :error, ld stops and returns, signalling an error to its caller.  File: acl2-doc-lemacs.info, Node: LD-ERROR-TRIPLES, Next: LD-EVISC-TUPLE, Prev: LD-ERROR-ACTION, Up: MISCELLANEOUS LD-ERROR-TRIPLES determines whether a form caused an error during ld Ld-error-triples is an ld special (*Note LD::). The accessor is (ld-error-triples state) and the updater is (set-ld-error-triples val state). Ld-error-triples must be either t or nil. The initial value of ld-error-triples is t. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-error-triples is one of them. If this variable has the value t then when a form evaluates to 3 values, the first of which is non-nil and the third of which is state, an error is deemed to have occurred. When an error occurs in evaluating a form, ld rolls back the ACL2 world to the configuration it had at the conclusion of the last error-free form. Then ld takes the action determined by ld-error-action.  File: acl2-doc-lemacs.info, Node: LD-EVISC-TUPLE, Next: LD-KEYWORD-ALIASES, Prev: LD-ERROR-TRIPLES, Up: MISCELLANEOUS LD-EVISC-TUPLE determines whether ld suppresses details when printing Ld-evisc-tuple is an ld special (*Note LD::). The accessor is (ld-evisc-tuple state) and the updater is (set-ld-evisc-tuple val state). Ld-evisc-tuple must be either nil or a list of the form (alist nil nil print-level print-length hiding-cars) where alist is an alist that pairs objects to strings, print-level and print-length are either nil or non-negative integers, and hiding-cars is a list of symbols. The initial value of ld-evisc-tuple is nil. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-evisc-tuple is one of them. Ld may print the forms it is evaluating and/or the results of evaluation. If the value of ld-evisc-tuple is a list as shown above, then ld "eviscerates" the objects it prints before printing them. To "eviscerate" an object we replace certain substructures within it by strings which are printed in their stead. Print-level and print-length, above, are used as described in CLTL (pp 372) to replace those substructures deeper than print-level by "#" and those longer than print-length by "...". Alist is used to replace any substructure occuring as a key in alist by the corresponding string. Finally, any consp x that starts with one of the symbols in hiding-cars is printed as .  File: acl2-doc-lemacs.info, Node: LD-KEYWORD-ALIASES, Next: LD-POST-EVAL-PRINT, Prev: LD-EVISC-TUPLE, Up: MISCELLANEOUS LD-KEYWORD-ALIASES allows the abbreviation of some keyword commands Example: (set-ld-keyword-aliases '((:q 0 q-fn) (:e 0 exit-acl2-macro)) state) Ld-keyword-aliases is an ld special (*Note LD::). The accessor is (ld-keyword-aliases state) and the updater is (set-ld-keyword-aliases val state). Ld-keyword-aliases must be an alist, each element of which is of the form (:keyword n fn), where :keyword is a keyword, n is a nonnegative integer, and fn is a function symbol of arity n, a macro symbol, or a lambda expression of arity n. When keyword is typed as an ld command, n more forms are read, x1, ..., xn, and the form (fn 'x1 ... 'xn) is then evaluated. The initial value of ld-keyword-aliases is nil. In the example above, :q has been redefined to have the effect of executing (q-fn), so for example if you define (defmacro q-fn () '(er soft 'q "You un-bound :q and now we have a soft error.")) then :q will cause an error, and if you define (defmacro exit-acl2-macro () '(exit-ld state)) then :e will cause the effect (it so happens) that :q normally has. If you prefer :e to :q for exiting the ACL2 loop, you might even want to put such definitions of q-fn and exit-acl2-macro together with the set-ld-keyword-aliases form above in your "acl2-customization.lisp" file; *Note ACL2-CUSTOMIZATION::. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-keyword-aliases is one of them. Ld-keyword-aliases affects how keyword commands are parsed. Generally speaking, ld's command interpreter reads ":fn x1 ... xn" as "(fn 'x1 ... 'xn)" when :fn is a keyword and fn is the name of an n-ary function. But this parse is overridden, as described above, for the keywords bound in ld-keyword-aliases.  File: acl2-doc-lemacs.info, Node: LD-POST-EVAL-PRINT, Next: LD-PRE-EVAL-FILTER, Prev: LD-KEYWORD-ALIASES, Up: MISCELLANEOUS LD-POST-EVAL-PRINT determines whether and how ld prints the result of evaluation Ld-post-eval-print is an ld special (*Note LD::). The accessor is (ld-post-eval-print state) and the updater is (set-ld-post-eval-print val state). Ld-post-eval-print must be either t, nil, or :command-conventions. The initial value of ld-post-eval-print is :command-conventions. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-post-eval-print is one of them. If this global variable is t, ld prints the result. In the case of a form that produces multiple values, ld prints the list containing them all (which, logically speaking, is what the form returned). If ld-post-eval-print is nil, ld does not print the values. This is most useful when ld is used to load a previously processed file. Finally, if ld-post-eval-print is :command-conventions then ld prints the result but treats "error triples" specially. An "error triple" is a result, (mv erp val state), that consists of three values, the third of which is state. Many ACL2 functions use such triples to signal errors. The convention is that if erp (the first value) is nil, then the function is returning val (the second value) as its conventional single result and possibly side-effecting state (as with some output). If erp is t, then an error has been caused, val is irrelevant and the error message has been printed in the returned state. Example ACL2 functions that follow this convention include defun and in-package. If such "error producing" functions are evaluated while ld-post-eval-print is set to t, then you would see them producing lists of length 3. This is disconcerting to users accustomed to Common Lisp (where these functions produce single results but sometimes cause errors or side-effect state). When ld-post-eval-print is :command-conventions and a form produces an error triple (mv erp val state) as its value, ld prints nothing if erp is non-nil and otherwise ld prints just val. Because it is a misrepresentation to suggest that just one result was returned, ld prints the value of the global variable 'triple-print-prefix before printing val. 'triple-print-prefix is initially " ", which means that when non-erroneous error triples are being abbreviated to val, val appears one space off the left margin instead of on the margin. In addition, when ld-post-eval-print is :command-conventions and the value component of an error triple is the keyword :invisible then ld prints nothing. This is the way certain commands (e.g., :pc) appear to return no value. By printing nothing when an error has been signalled, ld makes it appear that the error (whose message has already appeared in state) has "thrown" the computation back to load without returning a value. By printing just val otherwise, we suppress the fact that state has possibly been changed.  File: acl2-doc-lemacs.info, Node: LD-PRE-EVAL-FILTER, Next: LD-PRE-EVAL-PRINT, Prev: LD-POST-EVAL-PRINT, Up: MISCELLANEOUS LD-PRE-EVAL-FILTER determines which forms ld evaluates Ld-pre-eval-filter is an ld special (*Note LD::). The accessor is (ld-pre-eval-filter state) and the updater is (set-ld-pre-eval-filter val state). Ld-pre-eval-filter must be either :all, :query, or a new name that could be defined (e.g., by defun or defconst). The initial value of ld-pre-eval-filter is :all. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-pre-eval-filter is one of them. If the filter is :all, then every form read is evaluated. If the filter is :query, then after a form is read it is printed to standard-co and the user is asked if the form is to be evaluated or skipped. If the filter is a new name, then all forms are evaluated until that name is introduced, at which time ld terminates normally. The :all filter is, of course, the normal one. :Query is useful if you want to replay selected the commands in some file. The new name filter is used if you wish to replay all the commands in a file up through the introduction of the given one.  File: acl2-doc-lemacs.info, Node: LD-PRE-EVAL-PRINT, Next: LD-PROMPT, Prev: LD-PRE-EVAL-FILTER, Up: MISCELLANEOUS LD-PRE-EVAL-PRINT determines whether ld prints the forms to be eval'd Ld-pre-eval-print is an ld special (*Note LD::). The accessor is (ld-pre-eval-print state) and the updater is (set-ld-pre-eval-print val state). Ld-pre-eval-print must be either t, nil, or :never. The initial value of ld-pre-eval-print is nil. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-pre-eval-print is one of them. If this global variable is t, then before evaluating the form just read from standard-oi, ld prints the form to standard-co. If the variable is nil, no such printing occurs. The t option is useful if you are reading from a file of commands and wish to assemble a complete script of the session in standard-co. The value :never of ld-pre-eval-print is rarely used. During the evaluation of encapsulate and of certify-book forms, subsidiary events are normally printed, even if ld-pre-eval-print is nil. Thus for example, when the user submits an encapsulate form, all subsidiary events are generally printed even in the default situation where ld-pre-eval-print is nil. But occasionally one may want to suppress such printing. In that case, ld-pre-eval-print should be set to :never.  File: acl2-doc-lemacs.info, Node: LD-PROMPT, Next: LD-QUERY-CONTROL-ALIST, Prev: LD-PRE-EVAL-PRINT, Up: MISCELLANEOUS LD-PROMPT determines the prompt printed by ld Ld-prompt is an ld special (*Note LD::). The accessor is (ld-prompt state) and the updater is (set-ld-prompt val state). Ld-prompt must be either nil, t, or a function symbol that, when given an open output character channel and state, prints the desired prompt to the channel and returns two values: the number of characters printed and the state. The initial value of ld-prompt is t. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-prompt is one of them. Ld-prompt determines whether ld prints a prompt before reading the next form from standard-oi. If ld-prompt is nil, ld prints no prompt. If ld-prompt is t, the default prompt printer is used, which displays information that includes the current package, default defun-mode, guard checking status (on or off), and ld-skip-proofsp; *Note DEFAULT-PRINT-PROMPT::. If ld-prompt is neither nil nor t, then it should be a function name, fn, such that (fn channel state) will print the desired prompt to channel in state and return (mv col state), where col is the number of characters output (on the last line output). You may define your own prompt printing function. If you supply an inappropriate prompt function, i.e., one that causes an error or does not return the correct number and type of results, the following odd prompt will be printed instead: Bad Prompt See :DOC ld-prompt> which will lead you to this message. You should either call ld appropriately next time or assign an appropriate value to ld-prompt.  File: acl2-doc-lemacs.info, Node: LD-QUERY-CONTROL-ALIST, Next: LD-REDEFINITION-ACTION, Prev: LD-PROMPT, Up: MISCELLANEOUS LD-QUERY-CONTROL-ALIST how to default answers to queries Ld-query-control-alist is an ld special (*Note LD::). The accessor is (ld-query-control-alist state) and the updater is (set-ld-query-control-alist val state). Roughly speaking, ld-query-control-alist is either nil (meaning all queries should be interactive), t (meaning all should default to the first accepted response), or an alist that pairs query ids to keyword responses. The alist may end in either t or nil, indicating the default value for all ids not listed explicitly. Formally, the ld-query-control-alist must satisfy ld-query-control-alistp. The initial ld-query-control-alist is nil, which means all queries are handled interactively. When an ACL2 query is raised, a unique identifying symbol is printed in parentheses after the word "Query". This symbol, called the "query id," can be used in conjunction with ld-query-control-alist to prevent the query from being handled interactively. By "handled interactively" we mean that the query is printed to *standard-co* and a response is read from *standard-oi*. The alist can be used to obtain a "default value" for each query id. If this value is nil, then the query is handled interactively. In all other cases, the system handles the query without interaction (although text may be printed to standard-co to make it appear that an interaction has occurred; see below). If the default value is t, the system acts as though the user responded to the query by typing the first response listed among the acceptable responses. If the default value is neither nil nor t, then it must be a keyword and one of the acceptable responses. In that case, the system acts as though the user responded with the given keyword. Next, we discuss how the ld-query-control-alist assigns a default value to each query id. It assigns each id the first value paired with the id in the alist, or, if no such pair appears in the alist, it assigns the final cdr of the alist as the value. Thus, nil assigns all ids nil. T assigns all ids t. '((:filter . nil) (:sysdef . :n) . t) assigns nil to the :filter query, :n to the :sysdef query, and t to all others. It remains only to discuss how the system prints text when the default value is not nil, i.e., when the query is handled without interaction. In fact, it is allowed to pair a query id with a singleton list containing a keyword, rather than a keyword, and this indicates that no printing is to be done. Thus for the example above, :sysdef queries would be handled noninteractively, with printing done to simulate the interaction. But if we change the example so that :sysdef is paired with (:n), i.e., if ld-query-control-alist is '((:filter . nil) (:sysdef :n) . t), then no such printing would take place for sysdef queries. Instead, the default value of :n would be assigned "quietly".  File: acl2-doc-lemacs.info, Node: LD-REDEFINITION-ACTION, Next: LD-SKIP-PROOFSP, Prev: LD-QUERY-CONTROL-ALIST, Up: MISCELLANEOUS LD-REDEFINITION-ACTION to allow redefinition without undoing Ld-redefinition-action is an ld special (*Note LD::). The accessor is (ld-redefinition-action state) and the updater is (set-ld-redefinition-action val state). *If* ld-redefinition-action *is* non-nil *then ACL2 is liable to be made unsafe or unsound by* *ill-considered definitions*. The keyword command :redef will set ld-redefinition-action to a convenient setting allowing unsound redefinition. See below. When ld-redefinition-action is nil, redefinition is prohibited. In that case, an error message is printed upon any attempt to introduce a name that is already in use. There is one exception to this rule. It is permitted to redefine a function symbol in :program mode to be a function symbol in :logic mode provided the formals and body remain the same. This is the standard way a function "comes into" logical existence. Throughout the rest of this discussion we exclude from our meaning of "redefinition" the case in which a function in :program mode is identically redefined in :logic mode. At one time, ACL2 freely permitted the signature-preserving redefinition of :program mode functions but it no longer does. *Note REDEFINING-PROGRAMS::. When ld-redefinition-action is non-nil, you are allowed to redefine a name that is already in use. *The system may be rendered unsound* by such an act. It is important to understand how dangerous redefinition is. Suppose fn is a function symbol that is called from within some other function, say g. Suppose fn is redefined so that its arity changes. Then the definition of g is rendered syntactically ill-formed by the redefinition. This can be devastating since the entire ACL2 system assumes that terms in its data base are well-formed. For example, if ACL2 executes g by running the corresponding function in raw Common Lisp the redefinition of fn may cause raw lisp to break in irreparable ways. As Lisp programmers we live with this all the time by following the simple rule: after changing the syntax of a function don't run any function that calls it via its old syntax. This rule also works in the context of the evaluation of ACL2 functions, but it is harder to follow in the context of ACL2 deductions, since it is hard to know whether the data base contains a path leading the theorem prover from facts about one function to facts about another. Finally, of course, even if the data base is still syntactically well-formed there is no assurance that all the rules stored in it are valid. For example, theorems proved about g survive the redefinition of fn but may have crucially depended on the properties of the old fn. In summary, we repeat the warning: *all bets are off if you set* ld-redefinition-action TO *non*-nil. If at any point in a session you wish to see the list of all names that have been redefined, *Note REDEFINED-NAMES::. That said, we'll give you enough rope to hang yourself. When ld-redefinition-action is non-nil, it must be a pair, (a . b). The value of a determines how the system interacts with you when a redefinition is submitted. The value of b allows you to specify how the property list of the redefined name is to be "renewed" before the redefinition. There are several dimensions to the space of possibilities controlled by part a: Do you want to be queried each time you redefine a name, so you can confirm your intention? (We sometimes make typing mistakes or simply forget we have used that name already.) Do you want to see a warning stating that the name has been redefined? Do you want ACL2 system functions given special protection from possible redefinition? Below are the choices for part a: :query -- every attempt to redefine a name will produce a query. The query will allow you to abort the redefinition or proceed. It will will also allow you to specify the part b for this redefinition. :Query is the recommended setting for users who wish to dabble in redefinition. :warn -- any user-defined function may be redefined but a post-redefinition warning is printed. The attempt to redefine a system name produces a query. If you are prototyping and testing a big system in ACL2 this is probably the desired setting for part a. :doit -- any user-defined function may be redefined silently (without query or warning) but when an attempt is made to redefine a system function, a query is made. This setting is recommended when you start making massive changes to your prototyped system (and tire of even the warning messages issued by :warn). In support of our own ACL2 systems programming there are two other settings. We suggest ordinary users not use them. :warn! -- every attempt to redefine a name produces a warning but no query. Since ACL2 system functions can be redefined this way, this setting should be used by the only-slightly-less-than supremely confident ACL2 system hacker. :doit! -- this setting allows any name to be redefined silently (without query or warnings). ACL2 system functions are fair game. This setting is reserved for the supremely confident ACL2 system hacker. (Actually, this setting is used when we are loading massively modified versions of the ACL2 source files.) Part b of ld-redefinition-action tells the system how to "renew" the property list of the name being redefined. There are two choices: :erase -- erase all properties stored under the name, or :overwrite -- preserve existing properties and let the redefining overwrite them. It should be stressed that neither of these b settings is guaranteed to result in an entirely satisfactory state of affairs after the redefinition. Roughly speaking, :erase returns the property list of the name to the state it was in when the name was first introduced. Lemmas, type information, etc., stored under that name are lost. Is that what you wanted? Sometimes it is, as when the old definition is "completely wrong." But other times the old definition was "almost right" in the sense that some of the work done with it is still (intended to be) valid. In that case, :overwrite might be the correct b setting. For example if fn was a function and is being re-defun'd with the same signature, then the properties stored by the new defun should overwrite those stored by the old defun but the properties stored by defthms will be preserved. The b setting is only used as the default action when no query is made. If you choose a setting for part a that produces a query then you will have the opportunity, for each redefinition, to specify whether the property list is to be erased or overwritten. The keyword command :redef sets ld-redefinition-action to the pair (:query . :overwrite). Since the resulting query will give you the chance to specify :erase instead of :overwrite, this setting is quite convenient. But when you are engaged in heavy-duty prototyping, you may wish to use a setting such as :warn or even :doit. For that you will have to invoke a form such as: (set-ld-redefinition-action '(:doit . :overwrite) state) . Encapsulate causes somewhat odd interaction with the user if redefinition occurs within the encapsulation because the encapsulated event list is processed several times. For example, if the redefinition action causes a query and a non-local definition is actually a redefinition, then the query will be posed twice, once during each pass. C'est la vie. Finally, it should be stressed again that redefinition is dangerous because not all of the rules about a name are stored on the property list of the name. Thus, redefinition can render ill-formed terms stored elsewhere in the data base or can preserve now-invalid rules.  File: acl2-doc-lemacs.info, Node: LD-SKIP-PROOFSP, Next: LD-VERBOSE, Prev: LD-REDEFINITION-ACTION, Up: MISCELLANEOUS LD-SKIP-PROOFSP how carefully ACL2 processes your commands Examples: ACL2 !>(set-ld-skip-proofsp t state) T ACL2 !s>(set-ld-skip-proofsp nil state) NIL ACL2 !>(set-ld-skip-proofsp 'include-book state) INCLUDE-BOOK ACL2 !s> A global variable in the ACL2 state, called 'ld-skip-proofsp, determines the thoroughness with which ACL2 processes your commands. This variable may take on one of three values: t, nil or 'include-book. When ld-skip-proofsp is non-nil, the system assumes that which ought to be proved and is thus unsound. The form (set-ld-skip-proofsp flg state) is the general-purpose way of setting ld-skip-proofsp. This global variable is an "ld special," which is to say, you may call ld in such a way as to "bind" this variable for the dynamic extent of the ld. When ld-skip-proofsp is non-nil, the default prompt displays the character s. Thus, the prompt ACL2 !s> means that the default defun-mode is :logic (otherwise the character p, for :program, would also be printed; *Note DEFAULT-PRINT-PROMPT::) but "proofs are being skipped." Observe that there are two legal non-nil values, t and 'include-book. When ld-skip-proofsp is t, ACL2 skips all proof obligations but otherwise performs all other required analysis of input events. When ld-skip-proofsp is 'include-book, ACL2 skips not only proof obligations but all analysis except that required to compute the effect of successfully executed events. To explain the distinction, let us consider one particular event, say a defun. Very roughly speaking, a defun event normally involves a check of the syntactic well-formedness of the submitted definition, the generation and proof of the termination conditions, and the computation and storage of various rules such as a :definition rule and some :type-prescription rules. By "normally" above we mean when ld-skip-proofsp is nil. How does a defun behave when ld-skip-proofsp is non-nil? If ld-skip-proofsp is t, then defun performs the syntactic well-formedness checks and computes and stores the various rules, but it does not actually carry out the termination proofs. If ld-skip-proofsp is 'include-book, defun does not do the syntactic well-formedness check nor does it carry out the termination proof. Instead, it merely computes and stores the rules under the assumption that the checks and proofs would all succeed. Observe that a setting of 'include-book is "stronger" than a setting of t in the sense that 'include-book causes defun to assume even more about the admissibility of the event than t does. As one might infer from the choice of name, the include-book event sets ld-skip-proofsp to 'include-book when processing the events in a book being loaded. Thus, include-book does the miminal work necessary to carry out the effects of every event in the book. The syntactic checks and proof obligations were, presumably, successfully carried out when the book was certified. A non-nil value for ld-skip-proofsp also affects the system's output messages. Event summaries (the paragraphs that begin "Summary" and display the event forms, rules used, etc.) are not printed when ld-skip-proofsp is non-nil. Warnings and observations are printed when ld-skip-proofsp is t but are not printed when it is 'include-book. Intuitively, ld-skip-proofsp t means skip just the proofs and otherwise do all the work normally required for an event; while ld-skip-proofsp 'include-book is "stronger" and means do as little as possible to process events. In accordance with this intuition, local events are processed when ld-skip-proofsp is t but are skipped when ld-skip-proofsp is 'include-book. The ACL2 system itself uses only two settings, nil and 'include-book, the latter being used only when executing the events inside of a book being included. The ld-skip-proofsp setting of t is provided as a convenience to the user. For example, suppose one has a file of events. By loading it with ld with ld-skip-proofsp set to t, the events can all be checked for syntactic correctness and assumed without proof. This is a convenient way to recover a state lost by a system crash or to experiment with a modification of an events file. The foregoing discussion is actually based on a lie. ld-skip-proofsp is allowed two other values, 'initialize-acl2 and 'include-book-with-locals. The first causes behavior similar to t but skips local events and avoids some error checks that would otherwise prevent ACL2 from properly booting. The second is identical to 'include-book but also executes local events. These additional values are not intended for use by the user, but no barriers to their use have been erected. We close by reminding the user that ACL2 is potentially unsound if ld-skip-proofsp is ever set by the user. We provide access to it simply to allow experimentation and rapid reconstruction of lost or modified logical worlds.  File: acl2-doc-lemacs.info, Node: LD-VERBOSE, Next: LEMMA-INSTANCE, Prev: LD-SKIP-PROOFSP, Up: MISCELLANEOUS LD-VERBOSE determines whether ld prints "ACL2 Loading ..." Ld-verbose is an ld special (*Note LD::). The accessor is (ld-verbose state) and the updater is (set-ld-verbose val state). Ld-verbose must be t, nil or a string or consp suitable for fmt printing via the ~@ command. The initial value of ld-verbose is a fmt message that prints the ACL2 version number, ld level and connected book directory. Before processing the forms in standard-oi, ld may print a header. The printing of this header is controlled by ld-verbose. If ld-verbose is nil, no header is printed. If it is t, ld prints the message ACL2 loading where is the input channel supplied to ld. A similar message is printed when ld completes. If ld-verbose is neither t nor nil then it is presumably a header and is printed with the ~@ fmt directive before ld begins to read and process forms. In this case the ~@ fmt directive is interpreted in an environment in which #\v is the ACL2 version string, #\l is the level of the current recursion in ld and/or wormhole, and #\c is the connected book directory (cbd).  File: acl2-doc-lemacs.info, Node: LEMMA-INSTANCE, Next: LOCAL-INCOMPATIBILITY, Prev: LD-VERBOSE, Up: MISCELLANEOUS LEMMA-INSTANCE an object denoting an instance of a theorem Lemma instances are the objects one provides via :use and :by hints (*Note HINTS::) to bring to the theorem prover's attention some previously proved or easily provable fact. A typical use of the :use hint is given below. The value specified is a list of five lemma instances. :use (reverse-reverse (:type-prescription app) (:instance assoc-of-app (x a) (y b) (z c)) (:functional-instance p-f (p consp) (f flatten)) (:instance (:theorem (equal x x)) (x (flatten a)))) Observe that an event name can be a lemma instance. The :use hint allows a single lemma instance to be provided in lieu of a list, as in: :use reverse-reverse or :use (:instance assoc-of-app (x a) (y b) (z c)) A lemma instance denotes a formula which is either known to be a theorem or which must be proved to be a theorem before it can be used. To use a lemma instance in a particular subgoal, the theorem prover adds the formula as a hypothesis to the subgoal before the normal theorem proving heuristics are applied. A lemma instance, or lmi, is of one of the following five forms: (1) name, where name names a previously proved theorem, axiom, or definition and denotes the formula (theorem) of that name. (2) rune, where rune is a rune (*Note RUNE::) denoting the :corollary justifying the rule named by the rune. (3) (:theorem term), where term is any term alleged to be a theorem. Such a lemma instance denotes the formula term. But before using such a lemma instance the system will undertake to prove term. (4) (:instance lmi (v1 t1) ... (vn tn)), where lmi is recursively a lemma instance, the vi's are distinct variables and the ti's are terms. Such a lemma instance denotes the formula obtained by instantiating the formula denoted by lmi, replacing each vi by ti. (5) (:functional-instance lmi (f1 g1) ... (fn gn)), where lmi is recursively a lemma instance and each fi is an "instantiable" function symbol of arity ni and gi is a function symbol or a pseudo-lambda expression of arity ni. An instantiable function symbol is any defined or constrained function symbol except the primitives not, member, implies, and e0-ord-<, and a few others, as listed by the constant *non-instantiable-primitives*. These are built-in in such a way that we cannot recover the constraints on them. A pseudo-lambda expression is an expression of the form (lambda (v1 ... vn) body) where the vi are distinct variable symbols and body is any term. No a priori relation is imposed between the vi and the variables of body, i.e., body may ignore some vi's and may contain "free" variables. However, we do not permit v to occur freely in body if the functional substitution is to be applied to any formula (lmi or the constraints to be satisfied) that contains v as a variable. This is our draconian restriction to avoid capture. If you happen to violate this restriction by choosing a v that does occur, say in one of the relevant constraints, an informative error message will be printed. That message will list for you the illegal choices for v in the context in which the functional substitution is offered. A :functional-substitution lemma instance denotes the formula obtained by functionally instantiating the formula denoted by lmi, replacing fi by gi. However, before such a lemma instance can be used, the system will undertake to prove that the gi's satisfy the constraints (*Note CONSTRAINT::) on the fi's. Any such constraint that was generated and proved by ACL2 on behalf of a previously-proved event will be considered proved.  File: acl2-doc-lemacs.info, Node: LOCAL-INCOMPATIBILITY, Next: LOGICAL-NAME, Prev: LEMMA-INSTANCE, Up: MISCELLANEOUS LOCAL-INCOMPATIBILITY when non-local events won't replay in isolation Sometimes a "local incompatibility" is reported while attempting to embed some events, as in an encapsulate or include-book. This is generally due to the use of a locally defined name in a non-local event or the failure to make a witnessing definition local. Local incompatibilities may be detected while trying to execute the strictly non-local events of an embedding. For example, encapsulate operates by first executing all the events (local and non-local) with ld-skip-proofsp nil, to confirm that they are all admissible. Then it attempts merely to assume the non-local ones to create the desired theory, by executing the events with ld-skip-proofsp set to 'include-book. Similarly, include-book assumes the non-local ones, with the understanding that a previously successful certify-book has performed the admissiblity check. How can a sequence of events admitted with ld-skip-proofsp nil fail when ld-skip-proofsp is 'include-book? The key observation is that in the latter case only the non-local events are processed. The local ones are skipped and so the non-local ones must not depend upon them. Two typical mistakes are suggested by the detection of a local incompatibility: (1) a locally defined function or macro was used in a non-local event (and, in the case of encapsulate, was not included among the signatures) and (2) the witnessing definition of a function that was included among the signatures of an encapsulate was not made local. An example of mistake (1) would be to include among your encapsulated events both (local (defun fn ...)) and (defthm lemma (implies (fn ...) ...)). Observe that fn is defined locally but a formula involving fn is defined non-locally. In this case, either the defthm should be made local or the defun should be made non-local. An example of mistake (2) would be to include (fn (x) t) among your signatures and then to write (defun fn (x) ...) in your events, instead of (local (defun fn ...)). One subtle aspect of encapsulate is that if you constrain any member of a mutually recursive clique you must define the entire clique locally and then you must constrain those members of it you want axiomatized non-locally. Errors due to local incompatibility should never occur in the assumption of a fully certified book. Certification insures against it. Therefore, if include-book reports an incompatibility, we assert that earlier in the processing of the include-book a warning was printed advising you that some book was uncertified. If this is not the case -- if include-book reports an incompatibility and there has been no prior warning about lack of certification -- please report it to us. When a local incompatibility is detected, we roll-back to the world in which we started the encapsulate or include-book. That is, we discard the intermediate world created by trying to process the events skipping proofs. This is clean, but we realize it is very frustrating because the entire sequence of events must be processed from scratch. Assuming that the embedded events were, once upon a time, processed as top-level commands (after all, at some point you managed to create this sequence of commands so that the local and non-local ones together could survive a pass in which proofs were done), it stands to reason that we could define a predicate that would determine then, before you attempted to embed them, if local incompatibilities exist. We hope to do that, eventually.  File: acl2-doc-lemacs.info, Node: LOGICAL-NAME, Next: LOOP-STOPPER, Prev: LOCAL-INCOMPATIBILITY, Up: MISCELLANEOUS LOGICAL-NAME a name created by a logical event Examples: assoc caddr + "ACL2-USER" "arith" "project/task-1/arith.lisp" :here A logical name is either a name introduced by some event, such as defun, defthm, or include-book, or else is the keyword :here, which refers to the most recent such event. *Note EVENTS::. Every logical name is either a symbol or a string. For the syntactic rules on names, *Note NAME::. The symbols name functions, macros, constants, axioms, theorems, labels, and theories. The strings name packages or books. We permit the keyword symbol :here to be used as a logical name denoting the most recently completed event. The logical name introduced by an include-book is the full book name string for the book (*Note FULL-BOOK-NAME::). Thus, under the appropriate setting for the current book directory (*Note CBD::) the event (include-book "arith") may introduce the logical name "/usr/home/smith/project/task-1/arith.lisp" . Under a different cbd setting, it may introduce a different logical name, perhaps "/local/src/acl2/library/arith.lisp" . It is possible that identical include-book events forms in a session introduce two different logical names because of the current book directory. A logical name that is a string is either a package name or a book name. If it is not a package name, we support various conventions to interpret it as a book name. If it does not end with the string ".lisp" we extend it appropriately. Then, we search for any book name that has the given logical name as a terminal substring. Suppose (include-book "arith") is the only include-book so far and that "/usr/home/smith/project/task-1/arith.lisp" is the source file it processed. Then "arith", "arith.lisp" and "task-1/arith.lisp" are all logical names identifying that include-book event (unless they are package names). Now suppose a second (include-book "arith") is executed and processes "/local/src/acl2/library/arith.lisp". Then "arith" is no longer a logical name, because it is ambiguous. However, "task-1/arith" is a logical name for the first include-book and "library/arith" is a logical name for the second. Indeed, the first can be named by "1/arith" and the second by "y/arith". Logical names are used primarily in the theory manipulation functions, e.g., universal-theory and current-theory with which you may obtain some standard theories as of some point in the historical past. The reference points are the introductions of logical names, i.e., the past is determined by the events it contains. One might ask, "Why not discuss the past with the much more flexible language of command descriptors?" (*Note COMMAND-DESCRIPTOR::.) The reason is that inside of such events as encapsulate or macro commands that expand to progns of events, command descriptors provide too coarse a grain. When logical names are used as referents in theory expressions used in books, one must consider the possibility that the defining event within the book in question becomes redundant by the definition of the name prior to the assumption of the book. *Note REDUNDANT-EVENTS::.  File: acl2-doc-lemacs.info, Node: LOOP-STOPPER, Next: LP, Prev: LOGICAL-NAME, Up: MISCELLANEOUS LOOP-STOPPER limit application of permutative rewrite rules *Note RULE-CLASSES:: for a discussion of the syntax of the :loop-stopper field of :rewrite rule-classes. Here we describe how that field is used, and also how that field is created when the user does not explicitly supply it. For example, the built-in :rewrite rule commutativity-of-+, (implies (and (acl2-numberp x) (acl2-numberp y)) (equal (+ x y) (+ y x))), creates a rewrite rule with a loop-stopper of ((x y binary-+)). This means, very roughly, that the term corresponding to y must be "smaller" than the term corresponding to x in order for this rule to apply. However, the presence of binary-+ in the list means that certain functions that are "invisible" with respect to binary-+ (by default, unary-- is the only such function) are more or less ignored when making this "smaller" test. We are much more precise below. Our explanation of loop-stopping is in four parts. First we discuss ACL2's notion of "term order." Next, we bring in the notion of "invisibility", and use it together with term order to define orderings on terms that are used in the loop-stopping algorithm. Third, we describe that algorithm. These topics all assume that we have in hand the :loop-stopper field of a given rewrite rule; the fourth and final topic describes how that field is calculated when it is not supplied by the user. ACL2 must sometimes decide which of two terms is syntactically simpler. It uses a total ordering on terms, called the "term order." Under this ordering constants such as '(a b c) are simpler than terms containing variables such as x and (+ 1 x). Terms containing variables are ordered according to how many occurrences of variables there are. Thus x and (+ 1 x) are both simpler than (cons x x) and (+ x y). If variable counts do not decide the order, then the number of function applications are tried. Thus (cons x x) is simpler than (+ x (+ 1 y)) because the latter has one more function application. Finally, if the number of function applications do not decide the order, a lexicographic ordering on Lisp objects is used. *Note TERM-ORDER:: for details. When the loop-stopping algorithm is controlling the use of permutative :rewrite rules it allows term1 to be moved leftward over term2 only if term1 is smaller, in a suitable sense. Note: The sense used in loop-stopping is *not* the above explained term order but a more complicated ordering described below. The use of a total ordering stops rules like commutativity from looping indefinitely because it allows (+ b a) to be permuted to (+ a b) but not vice versa, assuming a is smaller than b in the ordering. Given a set of permutative rules that allows arbitrary permutations of the tips of a tree of function calls, this will normalize the tree so that the smallest argument is leftmost and the arguments ascend in the order toward the right. Thus, for example, if the same argument appears twice in the tree, as x does in the binary-+ tree denoted by the term (+ a x b x), then when the allowed permutations are done, all occurrences of the duplicated argument in the tree will be adjacent, e.g., the tree above will be normalized to (+ a b x x). Suppose the loop-stopping algorithm used term order, as noted above, and consider the binary-+ tree denoted by (+ x y (- x)). The arguments here are in ascending term order already. Thus, no permutative rules are applied. But because we are inside a +-expression it is very convenient if x and (- x) could be given virtually the same position in the ordering so that y is not allowed to separate them. This would allow such rules as (+ i (- i) j) = j to be applied. In support of this, the ordering used in the control of permutative rules allows certain unary functions, e.g., the unary minus function above, to be "invisible" with respect to certain "surrounding" functions, e.g., + function above. Briefly, a unary function symbol fn1 is invisible with respect to a function symbol fn2 if fn2 belongs to the value of fn1 in invisible-fns-alist; also *Note SET-INVISIBLE-FNS-ALIST::, which explains its format and how it can be set by the user. Roughly speaking, "invisible" function symbols are ignored for the purposes of the term-order test. Consider the example above, (+ x y (- x)). The translated version of this term is (binary-+ x (binary-+ y (unary-- x))). The initial invisible-fns-alist makes unary-- invisible with repect to binary-+. The commutativity rule for binary-+ will attempt to swap y and (unary-- x) and the loop-stopping algorithm is called to approve or disapprove. If term order is used, the swap will be disapproved. But term order is not used. While the loop-stopping algorithm is permuting arguments inside a binary-+ expression, unary-- is invisible. Thus, insted of comparing y with (unary-- x), the loop-stopping algorithm compares y with x, approving the swap because x comes before y. Here is a more precise specification of the total order used for loop-stopping with respect to a list, fns, of functions that are to be considered invisible. Let x and y be distinct terms; we specify when "x is smaller than y with respect to fns." If x is the application of a unary function symbol that belongs to fns, replace x by its argument. Repeat this process until the result is not the application of such a function; let us call the result x-guts. Similarly obtain y-guts from y. Now if x-guts is the same term as y-guts, then x is smaller than y in this order iff x is smaller than y in the standard term order. On the other hand, if x-guts is different than y-guts, then x is smaller than y in this order iff x-guts is smaller than y-guts in the standard term order. Now we may describe the loop-stopping algorithm. Consider a rewrite rule with conclusion (equiv lhs rhs) that applies to a term x in a given context; *Note REWRITE::. Suppose that this rewrite rule has a loop-stopper field (technically, the :heuristic-info field) of ((x1 y1 . fns-1) ... (xn yn . fns-n)). (Note that this field can be observed by using the command :pr with the name of the rule; *Note PR::.) We describe when rewriting is permitted. The simplest case is when the loop-stopper list is nil (i.e., n is 0); in that case, rewriting is permitted. Otherwise, for each i from 1 to n let xi' be the actual term corresponding to the variable xi when lhs is matched against the term to be rewritten, and similarly correspond yi' with y. If xi' and yi' are the same term for all i, then rewriting is not permitted. Otherwise, let k be the least i such that xi' and yi' are distinct. Let fns be the list of all functions that are invisible with respect to every function in fns-k, if fns-k is non-empty; otherwise, let fns be nil. Then rewriting is permitted if and only if yi' is smaller than xi' with respect to fns, in the sense defined in the preceding paragraph. It remains only to describe how the loop-stopper field is calculated for a rewrite rule when this field is not supplied by the user. (On the other hand, to see how the user may specify the :loop-stopper, *Note RULE-CLASSES::.) Suppose the conclusion of the rule is of the form (equiv lhs rhs). First of all, if rhs is not an instance of the left hand side by a substitution whose range is a list of distinct variables, then the loop-stopper field is nil. Otherwise, consider all pairs (u . v) from this substitution with the property that the first occurrence of v appears in front of the first occurrence of u in the print representation of rhs. For each such u and v, form a list fns of all functions fn in lhs with the property that u or v (or both) appears as a top-level argument of a subterm of lhs with function symbol fn. Then the loop-stopper for this rewrite rule is a list of all lists (u v . fns).