This is acl2-doc-emacs.info, produced by makeinfo version 4.5 from
acl2-doc-emacs.texinfo.
This is documentation for ACL2 Version 3.1
Copyright (C) 2006 University of Texas at Austin
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
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.
INFO-DIR-SECTION Math
START-INFO-DIR-ENTRY
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
END-INFO-DIR-ENTRY
File: acl2-doc-emacs.info, Node: THEORY-INVARIANT, Next: USER-DEFINED-FUNCTIONS-TABLE, Prev: TERM-TABLE, Up: EVENTS
THEORY-INVARIANT user-specified invariants on theories
Examples:
(theory-invariant (not (and (active-runep '(:rewrite left-to-right))
(active-runep '(:rewrite right-to-left))))
:key my-invariant
:error nil)
; Equivalent to the above:
(theory-invariant (incompatible '(:rewrite left-to-right)
'(:rewrite right-to-left))
:key my-invariant
:error nil)
General Form:
(theory-invariant term &key key error)
where:
o term is a term that uses no variables other than ens and state;
o key is an arbitrary "name" for this invariant (if omitted, an
integer is generated and used); and
o :error specifies the action to be taken when an invariant is
violated -- either nil if a warning is to be printed, else t (the
default) if an error is to be caused.
Theory-invariant is an event that adds to or modifies the table of
user-supplied theory invariants that are checked each time a theory
expression is evaluated.
The theory invariant mechanism is provided via a table (see *note
TABLE::) named theory-invariant-table. In fact, the theory-invariant
"event" is just a macro that expands into a use of the table event.
More general access to the theory-invariant table is provided by table
itself. For example, the table can be inspected or cleared with table;
you can clear an individual theory invariant by setting the invariant
to t, or eliminate all theory invariants with the command (table
theory-invariant-table nil nil :clear).
Theory-invariant-table maps arbitrary keys to records containing terms
that mention, at most, the variables ens and state. Every time an
alleged theory expression is evaluated, e.g., in the in-theory event or
:in-theory hint, each of the terms in theory-invariant-table is
evaluated with ens bound to a so-called "enabled structure" obtained
from the theory expression and state bound to the current ACL2 state
(see *note STATE::). Users generally need not know about the enabled
structure, other than that it can be accessed using the macros
active-runep and incompatible; see *note ACTIVE-RUNEP:: and see *note
INCOMPATIBLE::. If the result is nil, a message is printed and an
error occurs (except, only a warning occurs if :error nil is
specified). Thus, the table can be thought of as a list of conjuncts.
Each term in the table has a "name," which is just the key under which
the term is stored. When a theory violates the restrictions specified
by some term, both the name and the term are printed. By calling
theory-invariant with a new term but the same name, you can overwrite
that conjunct of the theory invariant; but see the Local Redefinition
Caveat at the end of this note. You may want to avoid using explicit
names, since otherwise the subsequent inclusion of another book that
defines a theory invariant with the same name will override your theory
invariant.
Theory invariants are particularly useful in the context of large rule
sets intended for re-use. Such sets often contain conflicting rules,
e.g., rules that are to be enabled when certain function symbols are
disabled, rules that rewrite in opposite directions and thus loop if
simultaneously enabled, groups of rules which should be enabled in
concert, etc. The developer of such rule sets understands these
restrictions and probably documents them. The theory invariant
mechanism allows the developer to codify his restrictions so that the
user is alerted when they are violated.
Since theory invariants are arbitrary terms, macros may be used to
express commonly used restrictions. For example, executing the event
(theory-invariant (incompatible (:rewrite left-to-right)
(:rewrite right-to-left)))
would subsequently cause an error any time the current theory contained
both of the two runes shown. Of course, incompatible is just defined as
a macro. Its definition may be inspected with :pe incompatible.
In order for a theory-invariant event to be accepted, the proposed
theory invariant must be satisfied by the current theory (see *note
CURRENT-THEORY::). The value returned upon successful execution of the
event is the key (whether user-supplied or generated).
Local Redefinition Caveat. Care needs to be taken when redefining a
theory invariant in a local context. Consider the following example.
(theory-invariant
(active-runep '(:definition binary-append))
:key app-inv)
(encapsulate
()
(local (theory-invariant t :key app-inv))
(in-theory (disable binary-append))
(defthm ...))
The second pass of the encapsulate will fail, because the in-theory
event violates the original theory-invariant and the local
theory-invariant is skipped in the second pass of the encapsulate. Of
course, local theory-invariants in books can cause the analogous
problem in the second (include-book) pass of a certify-book. In both
cases, though, the theory invariants are only checked at the conclusion
of the (include-book or encapsulate) event. Indeed, theory invariants
are checked at the end of every event related to theories, including
defun, defthm, in-theory, encapsulate, and include-book, except for
events executed on behalf of an include-book or the second pass of an
encapsulate.
File: acl2-doc-emacs.info, Node: USER-DEFINED-FUNCTIONS-TABLE, Next: VERIFY-GUARDS, Prev: THEORY-INVARIANT, Up: EVENTS
USER-DEFINED-FUNCTIONS-TABLE an advanced table used to replace certain system functions
Examples:
(table user-defined-functions-table 'untranslate-preprocess 'my-preprocess)
(table user-defined-functions-table 'untranslate 'my-untranslate)
This feature should perhaps only be used by advanced users who have a
thorough understanding of the system functions being replaced. There
are currently two ways a user can affect the way ACL2 prints terms.
The first example associates the user-defined function symbol
my-preprocess with untranslate-preprocess. As a result, when ACL2
prints a term, say during a proof, using its so-called "untranslate"
process the first thing it does is to call my-preprocess on two
arguments: that term and the current ACL2 logical world. If the call
produces a non-nil result, then that result is passed to the untranslate
process.
The second example associates the user-defined function symbol
my-untranslate with the built-in function symbol untranslate. As a
result, the code for my-untranslate will be run whenever the untranslate
process is run. The formals of the two functions must agree and must
not contain any stobj names. Note that these overrides fail to occur
upon guard violations and some other evaluation errors.
The untranslate-preprocess approach may suffice for most cases in which
a user wants to modify the way output is produced by the theorem
prover. We present an example immediately below, but see
books/misc/untranslate-patterns.lisp for a more elaborate example. If
the untranslate-preprocess approach does not seem sufficient for your
purposes, you are invited to look at file
books/misc/rtl-untranslate.lisp for an example of user-defined
untranslate (i.e., following the second example displayed above).
Suppose you have a large constant that you would prefer not to see in
proofs. For example, you may have submitted the following definition
(but imagine a much larger constant, say, a list of length 1,000,000).
(defconst *a* '(a b c d))
If you submit the following (silly) theorem
(thm (equal (cons x *a*) (car (cons yyy zzz))))
then you will see the following output:
(EQUAL (CONS X '(A B C D)) YYY).
If *a* had represented a much larger structure, we would wish we could
see the following instead.
(EQUAL (CONS X *A*) YYY)
That can be accomplished as follows. First we make the following
definition.
(defun my-preprocess (term wrld)
(declare (ignore wrld))
(if (equal term (list 'quote *a*))
'*a*
term))
Now we submit the following table event.
(table user-defined-functions-table
'untranslate-preprocess
'my-preprocess)
This will install my-preprocess as a preprocessor before the normal
untranslation routine is applied to printing a term. When the
untranslation routine encounters the constant (QUOTE (A B C D)), it
will replace it with *a*, and the usual untranlation routine will print
this as *A*.
File: acl2-doc-emacs.info, Node: VERIFY-GUARDS, Next: VERIFY-TERMINATION, Prev: USER-DEFINED-FUNCTIONS-TABLE, Up: EVENTS
VERIFY-GUARDS verify the guards of a function
Examples:
(verify-guards flatten)
(verify-guards flatten
:hints (("Goal" :use (:instance assoc-of-app)))
:otf-flg t
:doc "string")
General Form:
(verify-guards name
:hints hints
:otf-flg otf-flg
:doc doc-string)
See *Note GUARD:: for a general discussion of guards. In the General
Form above, name is the name of a :logic function (see *note
DEFUN-MODE::) or of a theorem or axiom. In the most common case name
is the name of a function that has not yet had its guards verified, each
subroutine of which has had its guards verified. hints and otf-flg are
as described in the corresponding :doc entries; and doc-string, if
supplied, is a string *not* beginning with ":Doc-Section". The three
keyword arguments above are all optional. Verify-guards will attempt
to prove that the guard on the named function implies the guards of all
of the subroutines called in the body of the function, and that the
guards are satisfied for all function calls in the guard itself (under
an implicit guard of t). If successful, name is considered to have had
its guards verified.
If name is one of several functions in a mutually recursive clique,
verify-guards will attempt to verify the guards of all of the functions.
If name is a theorem or axiom name, verify-guards verifies the guards
of the associated formula. When a theorem has had its guards verified
then you know that the theorem will evaluate to non-nil in all Common
Lisps, without causing a runtime error (other than possibly a resource
error). In particular, you know that the theorem's validity does not
depend upon ACL2's arbitrary completion of the domains of partial
Common Lisp functions.
For example, if app is defined as
(defun app (x y)
(declare (xargs :guard (true-listp x)))
(if (endp x)
y
(cons (car x) (app (cdr x) y))))
then we can verify the guards of app and we can prove the theorem:
(defthm assoc-of-app
(equal (app (app a b) c) (app a (app b c))))
However, if you go into almost any Common Lisp in which app is defined
as shown and evaluate
(equal (app (app 1 2) 3) (app 1 (app 2 3)))
we get an error or, perhaps, something worse like nil! How can this
happen since the formula is an instance of a theorem? It is supposed
to be true!
It happens because the theorem exploits the fact that ACL2 has completed
the domains of the partially defined Common Lisp functions like car and
cdr, defining them to be nil on all non-conses. The formula above
violates the guards on app. It is therefore "unreasonable" to expect
it to be valid in Common Lisp.
But the following formula is valid in Common Lisp:
(if (and (true-listp a)
(true-listp b))
(equal (app (app a b) c) (app a (app b c)))
t)
That is, no matter what the values of a, b and c the formula above
evaluates to t in all Common Lisps (unless the Lisp engine runs out of
memory or stack computing it). Furthermore the above formula is a
theorem:
(defthm guarded-assoc-of-app
(if (and (true-listp a)
(true-listp b))
(equal (app (app a b) c) (app a (app b c)))
t))
This formula, guarded-assoc-of-app, is very easy to prove from
assoc-of-app. So why prove it? The interesting thing about
guarded-assoc-of-app is that we can verify the guards of the formula.
That is, (verify-guards guarded-assoc-of-app) succeeds. Note that it
has to prove that if a and b are true lists then so is (app a b) to
establish that the guard on the outermost app on the left is satisfied.
By verifying the guards of the theorem we know it will evaluate to
true in all Common Lisps. Put another way, we know that the validity
of the formula does not depend on ACL2's completion of the partial
functions or that the formula is "well-typed."
One last complication: The careful reader might have thought we could
state guarded-assoc-of-app as
(implies (and (true-listp a)
(true-listp b))
(equal (app (app a b) c)
(app a (app b c))))
rather than using the if form of the theorem. We cannot! The reason
is technical: implies is defined as a function in ACL2. When it is
called, both arguments are evaluated and then the obvious truth table
is checked. That is, implies is not "lazy." Hence, when we write the
guarded theorem in the implies form we have to prove the guards on the
conclusion without knowing that the hypothesis is true. It would have
been better had we defined implies as a macro that expanded to the if
form, making it lazy. But we did not and after we introduced guards we
did not want to make such a basic change.
Recall however that verify-guards is almost always used to verify the
guards on a function definition rather than a theorem. We now return
to that discussion.
Because name is not uniquely associated with the verify-guards event
(it necessarily names a previously defined function) the documentation
string, doc-string, is not stored in the documentation data base.
Thus, we actually prohibit doc-string from having the form of an ACL2
documentation string; see *note DOC-STRING::.
If the guard on a function is not t, then guard verification requires
not only consideration of the body under the assumption that the guard
is true, but also consideration of the guard itself. Thus, for
example, guard verification fails in the following example, even though
there are no proof obligations arising from the body, because the guard
itself can cause a guard violation when evaluated for an arbitrary
value of x:
(defun foo (x)
(declare (xargs :guard (car x)))
x)
Verify-guards must often be used when the value of a recursive call of
a defined function is given as an argument to a subroutine that is
guarded. An example of such a situation is given below. Suppose app
(read "append") has a guard requiring its first argument to be a
true-listp. Consider
(defun rev (x)
(declare (xargs :guard (true-listp x)))
(cond ((endp x) nil)
(t (app (rev (cdr x)) (list (car x))))))
Observe that the value of a recursive call of rev is being passed into
a guarded subroutine, app. In order to verify the guards of this
definition we must show that (rev (cdr x)) produces a true-listp, since
that is what the guard of app requires. How do we know that (rev (cdr
x)) is a true-listp? The most elegant argument is a two-step one,
appealing to the following two lemmas: (1) When x is a true-listp, (cdr
x) is a true-listp. (2) When z is a true-listp, (rev z) is a
true-listp. But the second lemma is a generalized property of rev, the
function we are defining. This property could not be stated before rev
is defined and so is not known to the theorem prover when rev is
defined.
Therefore, we might break the admission of rev into three steps: define
rev without addressing its guard verification, prove some general
properties about rev, and then verify the guards. This can be done as
follows:
(defun rev (x)
(declare (xargs :guard (true-listp x)
:verify-guards nil)) ; Note this additional xarg.
(cond ((endp x) nil)
(t (app (rev (cdr x)) (list (car x))))))
(defthm true-listp-rev
(implies (true-listp x2)
(true-listp (rev x2))))
(verify-guards rev)
The ACL2 system can actually admit the original definition of rev,
verifying the guards as part of the defun event. The reason is that,
in this particular case, the system's heuristics just happen to hit
upon the lemma true-listp-rev. But in many more complicated functions
it is necessary for the user to formulate the inductively provable
properties before guard verification is attempted.
*Note on computation of guard conjectures and evaluation*. When ACL2
computes the guard conjecture for the body of a function, it evaluates
any ground subexpressions (those with no free variables), for calls of
functions whose :executable-counterpart runes are enabled. Note that
here, "enabled" refers to the current global theory, not to any :hints
given to the guard verification process; after all, the guard
conjecture is computed even before its initial goal is produced. Also
note that this evaluation is done in an environment as though
:set-guard-checking :all had been executed, so that we can trust that
this evaluation takes place without guard violations; see *note
SET-GUARD-CHECKING::.
File: acl2-doc-emacs.info, Node: VERIFY-TERMINATION, Next: WITH-OUTPUT, Prev: VERIFY-GUARDS, Up: EVENTS
VERIFY-TERMINATION convert a function from :program mode to :logic mode
Example:
(verify-termination fact)
General Forms:
(verify-termination fn dcl ... dcl)
(verify-termination (fn1 dcl ... dcl)
(fn2 dcl ... dcl)
...)
where fn and the fni are function symbols having :program mode (see
*note DEFUN-MODE::) and all of the dcls are either declare forms or
documentation strings. The first form above is an abbreviation for
(verify-termination (fn dcl ... dcl))
so we limit our discussion to the second form. Each of the fni must be
in the same clique of mutually recursively defined functions, but not
every function in the clique need be among the fni.
Verify-termination attempts to establish the admissibility of the fni.
Verify-termination retrieves their definitions, creates modified
definitions using the dcls supplied above, and resubmits these
definitions. You could avoid using verify-termination by typing the new
definitions yourself. So in that sense, verify-termination adds no new
functionality. But if you have prototyped your system in :program mode
and tested it, you can use verify-termination to resubmit your
definitions and change their defun-modes to :logic, addings hints
without having to retype or recopy the code.
The defun command executed by verify-termination is obtained by
retrieving the defun (or mutual-recursion) command that introduced the
clique in question and then possibly modifying each definition as
follows. Consider a function, fn, in the clique. If fn is not among
the fni above, its definition is left unmodified other than to add
(declare (xargs :mode :logic)). Otherwise, fn is some fni and we
modify its definition by inserting into it the corresponding dcls listed
with fni in the arguments to verify-termination, as well as (declare
(xargs :mode :logic)). In addition, we throw out from the old
declarations in fn the :mode specification and anything that is
specified in the new dcls.
For example, suppose that fact was introduced with:
(defun fact (n)
(declare (type integer n)
(xargs :mode :program))
(if (zp n) 1 (* n (fact (1- n))))).
Suppose later we do (verify-termination fact). Then the following
definition is submitted.
(defun fact (n)
(declare (type integer n))
(if (zp n) 1 (* n (fact (1- n))))).
Observe that this is the same definition as the original one, except
the old specification of the :mode has been deleted so that the
defun-mode now defaults to :logic. Although the termination proof
succeeds, ACL2 also tries to verify the guard, because we have
(implicitly) provided a guard, namely (integerp n), for this function.
(See *Note GUARD:: for a general discussion of guards, and see *note
TYPE-SPEC:: for a discussion of how type declarations are used in
guards.) Unfortunately, the guard verification fails, because the
subterm (zp n) requires that n be nonnegative, as can be seen by
invoking :args zp. (For a discussion of termination issues relating to
recursion on the naturals, see *note ZERO-TEST-IDIOMS::.) So we might
be tempted to submit the following:
(verify-termination
fact
(declare (xargs :guard (and (integerp n) (<= 0 n))))).
However, this is considered a changing of the guard (from (integerp n)),
which is illegal. If we instead change the guard in the earlier defun
after undoing that earlier definition with :ubt fact, then
(verify-termination fact) will succeed.
File: acl2-doc-emacs.info, Node: WITH-OUTPUT, Prev: VERIFY-TERMINATION, Up: EVENTS
WITH-OUTPUT suppressing or turning on specified output for an event
Example:
(with-output
:off summary ; turn off the event summary when evaluating the following:
(in-theory (disable name)))
General Form:
(with-output :key1 val1 ... :keyk valk form)
where each :keyi is either :off or :on and either vali is either :all
or else a symbol or non-empty list of symbols representing output types
that can be inhibited (see *note SET-INHIBIT-OUTPUT-LST::). The result
of evaluating the General Form above is to evaluate form, but in an
environment where the current set of inhibited output types is
modified: if :on :all is specified, then all output is turned on except
as specified by :off; else if :off :all is specified, then all output
is inhibited except as specified by :on; and otherwise, the
currently-inhibited output types are reduced as specified by :on and
then extended as specified by :off.
Warning: With-output has no effect in raw Lisp, and hence is disallowed
in function bodies. However, you can probably get the effect you want
as illustrated below, where