Major Section: MISCELLANEOUS

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;
see 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.

`ld`

prints ``ACL2 Loading ...''
Major Section: MISCELLANEOUS

`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>where

`<file>`

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

.
Major Section: MISCELLANEOUS

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

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

Major Section: MISCELLANEOUS

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.

Major Section: MISCELLANEOUS

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. See events. Every
logical name is either a symbol or a string. For the syntactic
rules on names, see 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 (see full-book-name). Thus, under the
appropriate setting for the current book directory (see 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?'' (See command-descriptor.) The reason
is that inside of such events as `encapsulate`

or macro commands that
expand to `progn`

s 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.
See redundant-events.

Major Section: MISCELLANEOUS

See 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. See 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 see 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; see 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;
see 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`

,
see 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)`

.

Major Section: MISCELLANEOUS

To enter the ACL2 command loop from Common Lisp, call the Common
Lisp program `lp`

(which stands for ``loop,'' as in ``read-eval-print
loop'' or ``command loop.'') The ACL2 command loop is actually
coded in ACL2 as the function `ld`

(which stands for ``load''). The
command loop is just what you get by loading from the standard
object input channel, `*standard-oi*`

. Calling `ld`

directly from
Common Lisp is possible but fragile because hard lisp errors or
aborts throw you out of `ld`

and back to the top-level of Common Lisp.
`Lp`

calls `ld`

in such a way as to prevent this and is thus the
standard way to get into the ACL2 command loop. Also
see acl2-customization for information on the loading of an
initialization file.

All of the visible functionality of `lp`

is in fact provided by `ld`

,
which is written in ACL2 itself. Therefore, you should see ld
for detailed documentation of the ACL2 command loop. We sketch it
below, for novice users.

Every expression typed to the ACL2 top-level must be an ACL2 expression.

Any ACL2 expression containing no variables may be evaluated.
Because of the applicative nature of ACL2, we make a special
exception for the variable `state`

. If this variable occurs in the
form, it is taken to mean the ``current'' ACL2 state object. If the
form returns a new state object as one of its values, then that is
considered the new ``current'' state for the evaluation of the
subsequent form. See state.

If the form read is a single keyword, e.g., `:`

`pe`

or `:`

`ubt`

, then
special procedures are followed. See keyword-commands.

The command loop keeps track of the commands you have typed and allows you to review them, display them, and roll the logical state back to that created by any command. See history.

ACL2 makes the convention that if a top-level form returns three
values, the last of which is an ACL2 state, then the first is
treated as a flag that means ``an error occurred,'' the second is
the value to be printed if no error occurred, and the third is (of
course) the new state. When ``an error occurs'' no value is
printed. Thus, if you execute a top-level form that happens to
return three such values, only the second will be printed (and that
will only happen if the first is `nil`

!). See ld for details.

Major Section: MISCELLANEOUS

Examples: (x y z) (x y z &optional max (base '10 basep)) (x y &rest rst) (x y &key max base) (&whole sexpr x y)

The ``lambda-list'' of a macro definition may include simple formal
parameter names as well as appropriate uses of the following
`lambda`

-list keywords from CLTL (pp. 60 and 145):

&optional, &rest, &key, &whole, &body, and &allow-other-keys.ACL2 does not support

`&aux`

and `&environment`

. In addition, we make
the following restrictions:
You are encouraged to experiment with the macro facility. One way to do so is to define a macro that does nothing but return the quotation of its arguments, e.g.,(1) initialization forms in

`&optional`

and`&key`

specifiers must be quoted values;(2)

`&allow-other-keys`

may only be used once, as the last specifier; and(3) destructuring is not allowed.

(defmacro demo (x y &optional opt &key key1 key2) (list 'quote (list x y opt key1 key2)))You may then execute the macro on some sample forms, e.g.,

term value (demo 1 2) (1 2 NIL NIL NIL) (demo 1 2 3) (1 2 3 NIL NIL) (demo 1 2 :key1 3) error: non-even key/value arglist (because :key1 is used as opt) (demo 1 2 3 :key2 5) (1 2 3 NIL 5)Also see trans.

Major Section: MISCELLANEOUS

Examples Counter-ExamplesPRIMEP 91 (not a symbolp) F-AC-23 :CHK-LIST (in KEYWORD package) 1AX *PACKAGE* (in the Lisp Package) |Prime Number| 1E3 (not a symbolp)

Many different ACL2 entities have names, e.g., functions, macros,
variables, constants, packages, theorems, theories, etc.
Package names are strings. All other names are symbols and may not
be in the `"KEYWORD"`

package. Moreover, names of functions,
macros, constrained functions, and constants, other than those that
are predefined, must not be in the ``main Lisp package'' (which is
(`"LISP"`

or `"COMMON-LISP"`

, according to whether we are
following CLTL1 or CLTL2). An analogous restriction on variables
is given below.

`T`

, `nil`

, and all names above except those that begin with ampersand
(&) are names of variables or constants. `T`

, `nil`

, and those names
beginning and ending with star (*) are constants. All other such
names are variables.

Note that names that start with ampersand, such as `&rest`

, may be
lambda list keywords and are reserved for such use whether or not
they are in the CLTL constant `lambda-list-keywords`

. (See pg 82
of CLTL2.) That is, these may not be used as variables. Unlike
constants, variables may be in the main Lisp package as long as they
are in the original list of imports from that package to ACL2, the
list `*common-lisp-symbols-from-main-lisp-package*`

, and do not
belong to a list of symbols that are potentially ``global.'' This
latter list is the value of `*common-lisp-specials-and-constants*`

.

Our restrictions pertaining to the main Lisp package take into
account that some symbols, e.g., `lambda-list-keywords`

and
`boole-c2`

, are ``special.'' Permitting them to be bound could
have harmful effects. In addition, the Common Lisp language does
not allow certain manipulations with many symbols of that package.
So, we stay away from them, except for allowing certain variables as
indicated above.

Major Section: MISCELLANEOUS

See bdd for information on this topic.

Major Section: MISCELLANEOUS

The value of this flag is normally `nil`

. If you want to prevent the
theorem prover from abandoning its initial work upon pushing the
second subgoal, set `:otf-flg`

to `t`

.

Suppose you submit a conjecture to the theorem prover and the system
splits it up into many subgoals. Any subgoal not proved by other
methods is eventually set aside for an attempted induction proof.
But upon setting aside the second such subgoal, the system chickens
out and decides that rather than prove n>1 subgoals inductively, it
will abandon its initial work and attempt induction on the
originally submitted conjecture. The `:otf-flg`

(Onward Thru the Fog)
allows you to override this chickening out. When `:otf-flg`

is `t`

, the
system will push all the initial subgoals and proceed to try to
prove each, independently, by induction.

Even when you don't expect induction to be used or to succeed,
setting the `:otf-flg`

is a good way to force the system to generate
and display all the initial subgoals.

The `:otf-flg`

may be supplied to `defun`

via the `xargs`

declare option. When you supply an `:otf-flg`

hint to `defun`

, the
flag is effective for the termination proofs and the guard proofs, if
any.

`defpkg`

s
Major Section: MISCELLANEOUS

Suppose `(defpkg "pkg" imports)`

is the most recently executed
successful definition of `"pkg"`

in this ACL2 session and that it
has since been undone, as by `:`

`ubt`

. Any future attempt in this
session to define `"pkg"`

as a package must specify an identical
imports list.

The restriction stems from the need to implement the reinstallation
of saved logical worlds as in error recovery and the `:`

`oops`

command.
Suppose that the new `defpkg`

attempts to import some symbol, `a::sym`

,
not imported by the previous definition of `"pkg"`

. Because it was
not imported in the original package, the symbol `pkg::sym`

, different
from `a::sym`

, may well have been created and may well be used in some
saved worlds. Those saved worlds are Common Lisp objects being held
for you ``behind the scenes.'' In order to import `a::sym`

into
`"pkg"`

now we would have to unintern `pkg::sym`

, rendering those
saved worlds ill-formed. It is because of saved worlds that we do
not actually clear out a package when it is undone.

At one point we thought it was sound to allow the new `defpkg`

to
import a subset of the old. But that is incorrect. Suppose the old
definition of `"pkg"`

imported `a::sym`

but the new one does not.
Suppose we allowed that and implemented it simply by setting the
imports of `"pkg"`

to the new subset. Then consider the conjecture
`(eq a::sym pkg::sym)`

. This ought not be a theorem because we did
not import `a::sym`

into `"pkg"`

. But in fact in AKCL it is a theorem
because `pkg::sym`

is read as `a::sym`

because of the old imports.