I-AM-HERE

a convenient marker for use with rebuild 
Major Section:  MISCELLANEOUS


Example Input File for Rebuild:
(defun fn1 (x y) ...)
(defthm lemma1 ...)
(defthm lemma2 ...)
(i-am-here)
The following lemma won't go through.  I started
typing the hint but realized I need to prove a
lemma first.  See the failed proof attempt in foo.bar.
I'm going to quit for the night now and resume tomorrow
from home.


(defthm lemma3 ...
  :hints (("Goal" :use (:instance ???
...

By putting an (i-am-here) form at the ``frontier'' of an evolving file of commands, you can use rebuild to load the file up to the (i-am-here). I-am-here simply returns an ld error triple and any form that ``causes an error'' will do the same job. Note that the text of the file after the (i-am-here) need not be machine readable.












































































IMMEDIATE-FORCE-MODEP

when executable counterpart is enabled, forced hypotheses are attacked immediately 
Major Section:  MISCELLANEOUS

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
See 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.












































































IN-PACKAGE

select current package 
Major Section:  MISCELLANEOUS


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)).
See 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.












































































INVISIBLE-FNS-ALIST

functions that are invisible to the loop-stopper algorithm 
Major Section:  MISCELLANEOUS


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. See set-invisible-fns-alist.

The notion of ``invisible functions'' has to do with the control mechanism on permutative :rewrite rules. See loop-stopper for a detailed discussion of the control mechanism. See set-invisible-fns-alist for a discussion of how to set the invisible functions alist.












































































KEYWORD-COMMANDS

how keyword commands are processed 
Major Section:  MISCELLANEOUS


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.












































































LD-ERROR-ACTION

determines ld's response to an error 
Major Section:  MISCELLANEOUS

Ld-error-action is an ld special (see 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.












































































LD-ERROR-TRIPLES

determines whether a form caused an error during ld 
Major Section:  MISCELLANEOUS

Ld-error-triples is an ld special (see 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.












































































LD-EVISC-TUPLE

determines whether ld suppresses details when printing 
Major Section:  MISCELLANEOUS

Ld-evisc-tuple is an ld special (see 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 <hidden>.












































































LD-KEYWORD-ALIASES

allows the abbreviation of some keyword commands 
Major Section:  MISCELLANEOUS


Example:
(set-ld-keyword-aliases '((:q 0 q-fn)
                          (:e 0 exit-acl2-macro))
                        state)
Ld-keyword-aliases is an ld special (see 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; see 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.












































































LD-POST-EVAL-PRINT

determines whether and how ld prints the result of evaluation 
Major Section:  MISCELLANEOUS

Ld-post-eval-print is an ld special (see 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.












































































LD-PRE-EVAL-FILTER

determines which forms ld evaluates 
Major Section:  MISCELLANEOUS

Ld-pre-eval-filter is an ld special (see 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.












































































LD-PRE-EVAL-PRINT

determines whether ld prints the forms to be eval'd 
Major Section:  MISCELLANEOUS

Ld-pre-eval-print is an ld special (see 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.












































































LD-PROMPT

determines the prompt printed by ld 
Major Section:  MISCELLANEOUS

Ld-prompt is an ld special (see 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; see 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.












































































LD-QUERY-CONTROL-ALIST

how to default answers to queries 
Major Section:  MISCELLANEOUS

Ld-query-control-alist is an ld special (see 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''.












































































LD-REDEFINITION-ACTION

to allow redefinition without undoing 
Major Section:  MISCELLANEOUS

Ld-redefinition-action is an ld special (see 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. See 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, see 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.