LD-PRE-EVAL-FILTER

Parent topic:  MISCELLANEOUS
Home

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

Parent topic:  MISCELLANEOUS
Home

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

Parent topic:  MISCELLANEOUS
Home

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>

LD-QUERY-CONTROL-ALIST

Parent topic:  MISCELLANEOUS
Home

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

Parent topic:  MISCELLANEOUS
Home

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

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

:erase -- erase all properties stored under the name, or

:overwrite -- preserve existing properties and let the redefining overwrite them.

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.

LD-SKIP-PROOFSP

Parent topic:  MISCELLANEOUS
Home

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>

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.

LD-VERBOSE

Parent topic:  MISCELLANEOUS
Home

Ld-verbose is an ld special (see 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 <file>

LEMMA-INSTANCE

Parent topic:  MISCELLANEOUS
Home

Lemma instances are the objects one provides via :use and :by hints (see 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))))

:use reverse-reverse

: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 (see 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 (see 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.

LOCAL-INCOMPATIBILITY

Parent topic:  MISCELLANEOUS
Home

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.