This is documentation for ACL2 Version 3.4
Copyright (C) 2008  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.

DEFMACRO    define a macro

     Example Defmacros:
     (defmacro xor (x y)
       (list 'if x (list 'not y) y))

     (defmacro git (sym key)
       (list 'getprop sym key nil
             '(quote current-acl2-world)
             '(w state)))

     (defmacro one-of (x &rest rst)
       (declare (xargs :guard (symbol-listp rst)))
       (cond ((null rst) nil)
             (t (list 'or
                      (list 'eq x (list 'quote (car rst)))
                      (list* 'one-of x (cdr rst))))))

     Example Expansions:
     term                    macroexpansion

     (xor a b)              (if a (not b) b)
     (xor a (foo b))        (if a (not (foo b)) (foo b))

     (git 'car 'lemmas)     (getprop 'car 'lemmas nil
                                     'current-acl2-world
                                     (w state))

     (one-of x a b c)       (or (eq x 'a)
                                (or (eq x 'b)
                                    (or (eq x 'c) nil)))

     (one-of x 1 2 3)       ill-formed (guard violation)

     General Form:
     (defmacro name macro-args doc-string dcl ... dcl body)

where name is a new symbolic name (see NAME), macro-args
specifies the formals of the macro (see MACRO-ARGS for a
description), and body is a term.  Doc-string is an optional
documentation string; see DOC-STRING.  Each dcl is an optional
declaration (see DECLARE) except that the only xargs keyword
permitted by defmacro is :guard.

Macroexpansion occurs when a form is read in, i.e., before the
evaluation or proof of that form is undertaken.  To experiment with
macroexpansion, see TRANS.  When a form whose car is name
arises as the form is read in, the arguments are bound as described in
CLTL pp. 60 and 145, the guard is checked, and then the body is
evaluated.  The result is used in place of the original form.

In ACL2, macros do not have access to state.  That is, state is not
allowed among the formal parameters.  This is in part a reflection of
CLTL, pp. 143, "More generally, an implementation of Common Lisp has
great latitude in deciding exactly when to expand macro calls with a
program. ...  Macros should be written in such a way as to depend as
little as possible on the execution environment to produce a correct
expansion." In ACL2, the product of macroexpansion is independent of
the current environment and is determined entirely by the macro body
and the functions and constants it references.  It is possible,
however, to define macros that produce expansions that refer to state
or other single-threaded objects (see STOBJ) or variables not
among the macro's arguments.  See the git example above.

DEFPKG    define a new symbol package

     Example:
     (defpkg "MY-PKG"
             (union-eq *acl2-exports*
                       *common-lisp-symbols-from-main-lisp-package*))

     * Menu:

     * HIDDEN-DEATH-PACKAGE:: handling defpkg events that are local

     * HIDDEN-DEFPKG:: handling defpkg events that are local

     General Form:
     (defpkg "name" term doc-string)

where "name" is a non-empty string consisting of standard characters
(see STANDARD-CHAR-P), none of which is lower case, that names
the package to be created; term is a variable-free expression that
evaluates to a list of symbols, where no two distinct symbols in the
list may have the same symbol-name, to be imported into the newly
created package; and doc-string is an optional documentation string;
see DOC-STRING.  The name of the new package must be "new": the
host lisp must not contain any package of that name.  There are two
exceptions to this newness rule, discussed at the end of this
documentation.

(There is actually an additional argument, book-path, that is used for
error reporting but has no logical content.  Users should generally
ignore this argument, as well as the rest of this sentence: a book-path
will be specified for defpkg events added by ACL2 to the portcullis of
a book's certificate; see HIDDEN-DEATH-PACKAGE.)

Defpkg forms can be entered at the top-level of the ACL2 command loop.
They should not occur in books (see CERTIFY-BOOK).

After a successful defpkg it is possible to "intern" a string into the
package using intern-in-package-of-symbol.  The result is a symbol that
is in the indicated package, provided the imports allow it.  For
example, suppose 'my-pkg::abc is a symbol whose symbol-package-name is
"MY-PKG".  Suppose further that the imports specified in the defpkg for
"MY-PKG" do not include a symbol whose symbol-name is "XYZ".  Then

     (intern-in-package-of-symbol "XYZ" 'my-pkg::abc)

returns a symbol whose symbol-name is "XYZ" and whose
symbol-package-name is "MY-PKG".  On the other hand, if the imports to
the defpkg does include a symbol with the name "XYZ", say in the
package "LISP", then

     (intern-in-package-of-symbol "XYZ" 'my-pkg::abc)

returns that symbol (which is uniquely determined by the restriction on
the imports list above).  See INTERN-IN-PACKAGE-OF-SYMBOL.

Defpkg is the only means by which an ACL2 user can create a new package
or specify what it imports.  That is, ACL2 does not support the Common
Lisp functions make-package or import.  Currently, ACL2 does not
support exporting at all.

The Common Lisp function intern is weakly supported by ACL2.  See
INTERN.

We now explain the two exceptions to the newness rule for package
names.  The careful experimenter will note that if a package is created
with a defpkg that is subsequently undone, the host lisp system will
contain the created package even after the undo.  Because ACL2 hangs
onto worlds after they have been undone, e.g., to implement :oops but,
more importantly, to implement error recovery, we cannot actually
destroy a package upon undoing it.  Thus, the first exception to the
newness rule is that name is allowed to be the name of an existing
package if that package was created by an undone defpkg and the newly
proposed set of imports is identical to the old one.  See
PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS.  This exception does not
violate the spirit of the newness rule, since one is disinclined to
believe in the existence of undone packages.  The second exception is
that name is allowed to be the name of an existing package if the
package was created by a defpkg with identical set of imports.  That
is, it is permissible to execute "redundant" defpkg commands.  The
redundancy test is based on the values of the two import forms
(comparing them after sorting and removing duplicates), not on the
forms themselves.

Finally, we explain why we require the package name to contain standard
characters, none of which is lower case.  We have seen at least one
implementation that handled lower-case package names incorrectly.
Since we see no need for lower-case characters in package names, which
can lead to confusion anyhow (note for example that foo::bar is a
symbol whose symbol-package-name is "FOO", not "foo"), we simply
disallow them.  Since the notion of "lower case" is only well-specified
in Common Lisp for standard characters, we restrict to these.

HIDDEN-DEATH-PACKAGE    handling defpkg events that are local

This documentation topic explains a little bit about certain errors
users may see when attempting to evaluate a defpkg event.  In brief, if
you see an error that refers you to this topic, you are probably trying
to admit a defpkg event, and you should change the name of the package
to be introduced by that event.

Recall that defpkg events introduce axioms, for example as follows.

     ACL2 !>(defpkg "PKG0" '(a b))

     Summary
     Form:  ( DEFPKG "PKG0" ...)
     Rules: NIL
     Warnings:  None
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      "PKG0"
     ACL2 !>:pr! "PKG0"

     Rune:       (:REWRITE PKG0-PACKAGE)
     Status:     Enabled
     Lhs:        (SYMBOL-PACKAGE-NAME (INTERN-IN-PACKAGE-OF-SYMBOL X Y))
     Rhs:        "PKG0"
     Hyps:       (AND (STRINGP X)
                      (NOT (MEMBER-SYMBOL-NAME X '(A B)))
                      (SYMBOLP Y)
                      (EQUAL (SYMBOL-PACKAGE-NAME Y) "PKG0"))
     Equiv:      EQUAL
     Backchain-limit-lst:    NIL
     Subclass:   BACKCHAIN
     Loop-stopper: NIL
     ACL2 !>

Now, a defpkg event may be executed underneath an encapsulate or
include-book form that is marked local.  In that case, traces of the
added axiom will disappear after the surrounding encapsulate or
include-book form is admitted.  This can cause inconsistencies.  (You
can take our word for it, or you can look at the example shown in the
"Essay on Hidden Packages" in source file axioms.lisp.)

In order to prevent unsoundness, then, ACL2 maintains the following
invariant.  Let us say that a defpkg event is "hidden" if it is in
support of the current logical world but is not present in that world as
an event, because it is local as indicated above.  We maintain the
invariant that all defpkg events, even if "hidden", are tracked
under-the-hood in the current logical world.  Sometimes this property
causes defpkg events to be written to the portcullis of a book's
certificate (see BOOKS).  At any rate, if you then try to
define the package in a manner inconsistent with the earlier such
definition, that is, with a different imports list, you will see an
error because of the above-mentioned tracking.

(By the way, this topic's name comes from Holly Bell, who heard "hidden
death package" instead of "hidden defpkg".  The description seemed to
fit.  Thanks, Holly!)

HIDDEN-DEFPKG    handling defpkg events that are local

See HIDDEN-DEATH-PACKAGE

DEFPUN    define a tail-recursive function symbol

Defpun is a macro developed by Pete Manolios and J Moore that allows
tail-recursive definitions.  It is defined in distributed book
books/misc/defpun.lisp, so to use it, execute the following event.

     (include-book "misc/defpun" :dir :system)

Details of defpun are provided by Manolios and Moore in the "Partial
Functions in ACL2" published with the ACL2 2000 workshop; see
http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/.  Also see
http://www.cs.utexas.edu/users/moore/publications/defpun/index.html.

A variant, defp, has been developed by Matt Kaufmann to allow more
general forms of tail recursion.  If defpun doesn't work for you, try
defp by first executing the following event.

     (include-book "misc/defp" :dir :system)

Sandip Ray has contributed a variant of defpun, defpun-exec, that
supports executability.  See distributed book
books/defexec/defpun-exec/defpun-exec.lisp:

     (include-book "defexec/defpun-exec/defpun-exec" :dir :system)

He has also contributed book
books/misc/misc2/defpun-exec-domain-example.lisp, for functions that are
uniquely defined in a particular domain.

DEFREFINEMENT    prove that equiv1 refines equiv2

     Example:
     (defrefinement equiv1 equiv2)

     is an abbreviation for
     (defthm equiv1-refines-equiv2
       (implies (equiv1 x y) (equiv2 x y))
       :rule-classes (:refinement))

See REFINEMENT.

     General Form:
     (defrefinement equiv1 equiv2
       :rule-classes rule-classes
       :instructions instructions
       :hints hints
       :otf-flg otf-flg
       :event-name event-name
       :doc doc)

where equiv1 and equiv2 are known equivalence relations, event-name, if
supplied, is a symbol and all other arguments are as specified in the
documentation for defthm.  The defrefinement macro expands into a call
of defthm.  The name supplied is equiv1-refines-equiv2, unless
event-name is supplied, in which case it is used as the name.  The term
supplied states that equiv1 refines equiv2.  The rule-class :refinement
is added to the rule-classes specified, if it is not already there.
All other arguments to the generated defthm form are as specified by
the other keyword arguments above.

DEFSTOBJ    define a new single-threaded object

     Example:
     (defstobj st
               (reg :type (array (unsigned-byte 31) (8))
                    :initially 0)
               (p-c :type (unsigned-byte 31)
                    :initially 555)
               halt                  ; = (halt :type t :initially nil)
               (mem :type (array (unsigned-byte 31) (64))
                    :initially 0 :resizable t))

     General Form:
     (defstobj name
               (field1 :type type1 :initially val1 :resizable b1)
               ...
               (fieldk :type typek :initially valk :resizable bk)
               :renaming alist
               :doc doc-string
               :inline inline-flag)

where name is a new symbol, each fieldi is a symbol, each typei is
either a type-spec or (ARRAY type-spec (max)), each vali is an object
satisfying typei, and each bi is t or nil.  Each pair :initially vali
and :resizable bi may be omitted; more on this below.  The alist
argument is optional and allows the user to override the default
function names introduced by this event.  The doc-string is also
optional.  The inline-flag Boolean argument is also optional and
declares to ACL2 that the generated access and update functions for the
stobj should be implemented as macros under the hood (which has the
effect of inlining the function calls).  We describe further
restrictions on the fieldi, typei, vali, and on alist below.  We
recommend that you read about single-threaded objects (stobjs) in ACL2
before proceeding; see STOBJ.

The effect of this event is to introduce a new single-threaded object
(i.e., a "stobj"), named name, and the associated recognizers, creator,
accessors, updaters, constants, and, for fields of ARRAY type, length
and resize functions.

_The Single-Threaded Object Introduced_

The defstobj event effectively introduces a new global variable, named
name, which has as its initial logical value a list of k elements,
where k is the number of "field descriptors" provided.  The elements
are listed in the same order in which the field descriptors appear.  If
the :type of a field is (ARRAY type-spec (max)) then the corresponding
element of the stobj is initially a list of length max containing the
value, val, specified by :initially val.  Otherwise, the :type of the
field is a type-spec and the corresponding element of the stobj is the
specified initial value val.  (The actual representation of the stobj
in the underlying Lisp may be quite different; see
STOBJ-EXAMPLE-2.  For the moment we focus entirely on the logical
aspects of the object.)

In addition, the defstobj event introduces functions for recognizing and
creating the stobj and for recognizing, accessing, and updating its
fields.  For fields of ARRAY type, length and resize functions are also
introduced.  Constants are introduced that correspond to the accessor
functions.

_Restrictions on the Field Descriptions in Defstobj_

Each field descriptor is of the form:

     (fieldi :TYPE typei :INITIALLY vali)

Note that the type and initial value are given in "keyword argument"
format and may be given in either order.  The typei and vali "arguments"
are not evaluated.  If omitted, the type defaults to t (unrestricted)
and the initial value defaults to nil.

Each typei must be either a type-spec or else a list of the form (ARRAY
type-spec (max)).  The latter forms are said to be "array types."
Examples of legal typei are:

     (INTEGERP 0 31)
     (SIGNED-BYTE 31)
     (ARRAY (SIGNED-BYTE 31) (16))

The typei describes the objects which are expected to occupy the given
field.  Those objects in fieldi should satisfy typei.  We are more
precise below about what we mean by "expected."  We first present the
restrictions on typei and vali.

Non-Array Types

When typei is a type-spec it restricts the contents, x, of fieldi
according to the "meaning" formula given in the table for type-spec.
For example, the first typei above restricts the field to be an integer
between 0 and 31, inclusive.  The second restricts the field to be an
integer between -2^30 and (2^30)-1, inclusive.

The initial value, vali, of a field description may be any ACL2 object
but must satisfy typei.  Note that vali is not a form to be evaluated
but an object.  A form that evaluates to vali could be written 'vali,
but defstobj does not expect you to write the quote mark.  For example,
the field description

     (days-off :initially (saturday sunday))

describes a field named days-off whose initial value is the list
consisting of the two symbols SATURDAY and SUNDAY.  In particular, the
initial value is NOT obtained by applying the function saturday to the
variable sunday!  Had we written

     (days-off :initially '(saturday sunday))

it would be equivalent to writing

     (days-off :initially (quote (saturday sunday)))

which would initialize the field to a list of length two, whose first
element is the symbol quote and whose second element is a list
containing the symbols saturday and sunday.

Array Types

When typei is of the form (ARRAY type-spec (max)), the field is
supposed to be a list of items, initially of length max, each of which
satisfies the indicated type-spec.  Max must be a non-negative integer
less than (2^28)-1.  We discuss this limitation below. Thus,

     (ARRAY (SIGNED-BYTE 31) (16))

restricts the field to be a list of integers, initially of length 16,
where each integer in the list is a (SIGNED-BYTE 31).  We sometimes
call such a list an "array" (because it is represented as an array in
the underlying Common Lisp).  The elements of an array field are
indexed by position, starting at 0.  Thus, the maximum legal index of
an array field is max-1.

Note that the ARRAY type requires that the max be enclosed in
parentheses.  This makes ACL2's notation consistent with the Common Lisp
convention of describing the (multi-)dimensionality of arrays.  But ACL2
currently supports only single dimensional arrays in stobjs.

For array fields, the initial value vali must be an object satisfying
the type-spec of the ARRAY description.  The initial value of the field
is a list of max repetitions of vali.

Array fields can be "resized," that is, their lengths can be changed, if
:resizable t is supplied as shown in the example and General Form above.
The new length must satisfy the same restriction as does max, as
described above.  Each array field in a defstobj event gives rise to a
length function, which gives the length of the field, and a resize
function, which modifies the length of the field if :resizable t was
supplied with the field when the defstobj was introduced and otherwise
causes an error.  If :resizable t was supplied and the resize function
specifies a new length k, then: if k is less than the existing array
length, the array is shortened simply by dropping elements with index
at least k; otherwise, the array is extended to length k by mapping the
new indices to the initial value (supplied by :initially, else default
nil).

Array resizing is relatively slow, so we recommend using it somewhat
sparingly.

_The Default Function Names_

To recap, in

     (defstobj name
               (field1 :type type1 :initially val1)
               ...
               (fieldk :type typek :initially valk)
               :renaming alist
               :doc doc-string
               :inline inline-flag)

name must be a new symbol, each fieldi must be a symbol, each typei
must be a type-spec or (ARRAY type-spec (max)), and each vali must be
an object satisfying typei.

Roughly speaking, for each fieldi, a defstobj introduces a recognizer
function, an accessor function, and an updater function.  The accessor
function, for example, takes the stobj and returns the indicated
component; the updater takes a new component value and the stobj and
return a new stobj with the component replaced by the new value.  But
that summary is inaccurate for array fields.

The accessor function for an array field does not take the stobj and
return the indicated component array, which is a list of length max.
Instead, it takes an additional index argument and returns the
indicated element of the array component.  Similarly, the updater
function for an array field takes an index, a new value, and the stobj,
and returns a new stobj with the indicated element replaced by the new
value.

These functions -- the recognizer, accessor, and updater, and also
length and resize functions in the case of array fields -- have
"default names."  The default names depend on the field name, fieldi,
and on whether the field is an array field or not.  For clarity,
suppose fieldi is named c. The default names are shown below in calls,
which also indicate the arities of the functions.  In the expressions,
we use x as the object to be recognized by field recognizers, i as an
array index, v as the "new value" to be installed by an updater, and
name as the single-threaded object.

                      non-array field        array field
     recognizer         (cP x)                (cP x)
     accessor           (c name)              (cI i name)
     updater            (UPDATE-c v name)     (UPDATE-cI i v name)
     length                                   (c-LENGTH name)
     resize                                   (RESIZE-c k name)

Finally, a recognizer and a creator for the entire single-threaded
object are introduced.  The creator returns the initial stobj, but may
only be used in limited contexts; see WITH-LOCAL-STOBJ.  If the
single-threaded object is named name, then the default names and
arities are as shown below.

     top recognizer     (nameP x)
     creator            (CREATE-name)

For example, the event

     (DEFSTOBJ $S
       (X :TYPE INTEGER :INITIALLY 0)
       (A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9))

introduces a stobj named $S.  The stobj has two fields, X and A.  The A
field is an array.  The X field contains an integer and is initially 0.
The A field contains a list of integers, each between 0 and 9,
inclusively.  Initially, each of the three elements of the A field is 9.

This event introduces the following sequence of definitions:

     (DEFUN XP (X) ...)               ; recognizer for X field
     (DEFUN AP (X) ...)               ; recognizer of A field
     (DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
     (DEFUN CREATE-$S () ...)         ; creator for stobj $S
     (DEFUN X ($S) ...)               ; accessor for X field
     (DEFUN UPDATE-X (V $S) ...)      ; updater for X field
     (DEFUN A-LENGTH ($S) ...)        ; length of A field
     (DEFUN RESIZE-A (K $S) ...)      ; resizer for A field
     (DEFUN AI (I $S) ...)            ; accessor for A field at index I
     (DEFUN UPDATE-AI (I V $S) ...)   ; updater for A field at index I

_Avoiding the Default Function Names_

If you do not like the default names listed above you may use the
optional :renaming alist to substitute names of your own choosing.
Each element of alist should be of the form (fn1 fn2), where fn1 is a
default name and fn2 is your choice for that name.

For example

     (DEFSTOBJ $S
       (X :TYPE INTEGER :INITIALLY 0)
       (A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9)
       :renaming ((X XACCESSOR) (CREATE-$S MAKE$S)))

introduces the following definitions

     (DEFUN XP (X) ...)               ; recognizer for X field
     (DEFUN AP (X) ...)               ; recognizer of A field
     (DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
     (DEFUN MAKE$S () ...)            ; creator for stobj $S
     (DEFUN XACCESSOR ($S) ...)       ; accessor for X field
     (DEFUN UPDATE-X (V $S) ...)      ; updater for X field
     (DEFUN A-LENGTH ($S) ...)        ; length of A field
     (DEFUN RESIZE-A (K $S) ...)      ; resizer for A field
     (DEFUN AI (I $S) ...)            ; accessor for A field at index I
     (DEFUN UPDATE-AI (I V $S) ...)   ; updater for A field at index I

Note that even though the renaming alist substitutes "XACCESSOR" for
"X" the updater for the X field is still called "UPDATE-X."  That is
because the renaming is applied to the default function names, not to
the field descriptors in the event.

Use of the :renaming alist may be necessary to avoid name clashes
between the default names and and pre-existing function symbols.

_Constants_

Defstobj events also introduce constant definitions (see
DEFCONST).  One constant is introduced for each accessor function by
prefixing and suffixing a `*' character on the function name.  The
value of that constant is the position of the field being accessed.
For example, if the accessor functions are a, b, and c, in that order,
then the following constant definitions are introduced.

     (defconst *a* 0)
     (defconst *b* 1)
     (defconst *c* 2)

These constants are used for certain calls of nth and update-nth that
are displayed to the user in proof output.  For example, for stobj st
with accessor functions a, b, and c, in that order, the term (nth '2
st) would be printed during a proof as (nth *c* st).  Also see
TERM, in particular the discussion there of untranslated terms, and
see NTH-ALIASES-TABLE.

_Inspecting the Effects of a Defstobj_

Because the stobj functions are introduced as "sub-events" of the
defstobj the history commands :pe and :pc will not print the
definitions of these functions but will print the superior defstobj
event.  To see the definitions of these functions use the history
command :pcb!.

To see an s-expression containing the definitions what constitute the
raw Lisp implementation of the event, evaluate the form

     (nth 4 (global-val 'cltl-command (w state)))

_immediately after_ the defstobj event has been processed.

A defstobj is considered redundant only if the name, field descriptors,
renaming alist, and inline flag are identical to a previously executed
defstobj.  Note that a redundant defstobj does not reset the stobj
fields to their initial values.

_Inlining and Performance_

The :inline keyword argument controls whether or not accessor, updater,
and length functions are inlined (as macros under the hood, in raw
Lisp).  If :inline t is provided then these are inlined; otherwise they
are not.  The advantage of inlining is potentially better performance;
there have been contrived examples, doing essentially nothing except
accessing and updating array fields, where inlining reduced the time by
a factor of 10 or more; and inlining has sped up realistic examples by
a factor of at least 2.  Inlining may get within a factor of 2 of C
execution times for such contrived examples, and within a few percent
of C execution times on realistic examples.

A drawback to inlining is that redefinition may not work as expected,
much as redefinition may not work as expected for macros: defined
functions that call a macro, or inlined stobj function, will not see a
subsequent redefinition of the macro or inlined function.  Another
drawback to inlining is that because inlined functions are implemented
as macros in raw Lisp, tracing (see TRACE$) will not show their
calls.  These drawbacks are avoided by default, but the user who is not
concerned about them is advised to specify :inline t.

DEFSTUB    stub-out a function symbol

     Examples:
     ACL2 !>(defstub subr1 (* * state) => (mv * state))
     ACL2 !>(defstub add-hash (* * hash-table) => hash-table)

     General Forms:
     (defstub name args-sig => output-sig)
     (defstub name args-sig => output-sig :doc doc-string)

Name is a new function symbol and (name . args-sig) => output-sig) is a
signature.  If the optional doc-string is supplied it should be a
documentation string.  See also the "Old Style" heading below.

Defstub macro expands into an encapsulate event (see
ENCAPSULATE).  Thus, no axioms are available about name but it may be
used wherever a function of the given signature is permitted.

Old Style:

     Old Style General Form:
     (defstub name formals output)
     (defstub name formals output :doc doc-string)

where name is a new function symbol, formals is its list of formal
parameters, and output is either a symbol (indicating that the function
returns one result) or a term of the form (mv s1 ... sn), where each si
is a symbol (indicating that the function returns n results).  Whether
and where the symbol state occurs in formals and output indicates how
the function handles state.  It should be the case that (name formals
output) is in fact a signature (see SIGNATURE).

Note that with the old style notation it is impossible to stub-out a
function that uses any single-threaded object other than state.  The
old style is preserved for compatibility with earlier versions of ACL2.

DEFTHEORY    define a theory (to enable or disable a set of rules)

     Example:
     (deftheory interp-theory
                (set-difference-theories
                  (universal-theory :here)
                  (universal-theory 'interp-section)))

     General Form:
     (deftheory name term :doc doc-string)

where name is a new symbolic name (see NAME), term is a term
that when evaluated will produce a theory (see THEORIES), and
doc-string is an optional documentation string (see
DOC-STRING).  Except for the variable world, term must contain no
free variables.  Term is evaluated with world bound to the current
world (see WORLD) and the resulting theory is then converted to
a _runic theory_ (see THEORIES) and associated with name.
Henceforth, this runic theory is returned as the value of the theory
expression (theory name).

The value returned is the length of the resulting theory.  For example,
in the following, the theory associated with 'FOO has 54 runes:

     ACL2 !>(deftheory foo (union-theories '(binary-append)
                                           (theory 'minimal-theory)))

     Summary
     Form:  ( DEFTHEORY FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      54
     ACL2 !>

DEFTHM    prove and name a theorem

     Examples:
     (defthm assoc-of-app
             (equal (app (app a b) c)
                    (app a (app b c))))

The following nonsensical example illustrates all the optional
arguments but is illegal because not all combinations are permitted.
See HINTS for a complete list of hints.

     (defthm main
             (implies (hyps x y z) (concl x y z))
            :rule-classes (:REWRITE :GENERALIZE)
            :instructions (induct prove promote (dive 1) x
                                  (dive 2) = top (drop 2) prove)
            :hints (("Goal"
                     :do-not '(generalize fertilize)
                     :in-theory (set-difference-theories
                                  (current-theory :here)
                                  '(assoc))
                     :induct (and (nth n a) (nth n b))
                     :use ((:instance assoc-of-append
                                      (x a) (y b) (z c))
                           (:functional-instance
                             (:instance p-f (x a) (y b))
                             (p consp)
                             (f assoc)))))
            :otf-flg t
            :doc "#0[one-liner/example/details]")

     General Form:
     (defthm name term
             :rule-classes rule-classes
             :instructions instructions
             :hints        hints
             :otf-flg      otf-flg
             :doc          doc-string)

where name is a new symbolic name (see NAME), term is a term
alleged to be a theorem, and rule-classes, instructions, hints, otf-flg
and doc-string are as described in their respective documentation.  The
five keyword arguments above are all optional, however you may not
supply both :instructions and :hints, since one drives the proof
checker and the other drives the theorem prover.  If :rule-classes is
not specified, the list (:rewrite) is used; if you wish the theorem to
generate no rules, specify :rule-classes nil.

When ACL2 processes a defthm event, it first tries to prove the term
using the indicated hints (see HINTS) or instructions (see
PROOF-CHECKER).  If it is successful, it stores the rules
described by the rule-classes (see RULE-CLASSES), proving the
necessary corollaries.

DEFTHMD    prove and name a theorem and then disable it

Use defthmd instead of defthm when you want to disable a theorem
immediately after proving it.  This macro has been provided for users
who prefer working in a mode where theorems are only enabled when
explicitly directed by :in-theory.  Specifically, the form

     (defthmd NAME TERM ...)

expands to:

     (progn
       (defthmd NAME TERM ...)
       (with-output
        :off summary
        (in-theory (disable NAME)))
       (value NAME)).

Note that defthmd commands are never redundant (see
REDUNDANT-EVENTS).  Even if the defthm event is redundant, then the
in-theory event will still be executed.

The summary for the in-theory event is suppressed.  See DEFTHM
for documentation of defthm.

DEFTTAG    introduce a trust tag (ttag)

*Introduction*.  This event is intended for advanced users who, in
essence, want to build extensions of ACL2.  The typical intended use is
to create books that extend the functionality of ACL2 in ways not
allowed without a so-called "active trust tag".  A trust tag thus
represents a contract: The writer of such a book is guaranteeing that
the book extends ACL2 in a "correct" way as defined by the writer of
the book -- often simply in a sound way --.  The writer of the book
will often have a small section of the book in the scope of an active
trust tag that can be inspected by potential users of that book:

     <initial part of book, which does not use trust tags>
     (defttag :some-ttag) ; install :some-ttag as an active trust tag
     <various code that requires an active trust tag>
     (defttag nil)        ; remove active trust tag
     <initial part of book, which does not use trust tags>

Why may trust tags be needed?  The evaluation of certain functions can
introduce bugs and even unsoundness, but can be useful in restricted
ways that avoid such issues.  For example, sys-call can be used in an
unsafe way, for example to overwrite files, or worse; see
SYS-CALL for a frightening example from Bob Boyer.  The following
example shows that the function sys-call is restricted by default, but
can be called after installing an active trust tag.

     ACL2 !>(sys-call "pwd" nil)

     ACL2 Error in TOP-LEVEL:  The SYS-CALL function cannot be called unless
     a trust tag is in effect.  See :DOC defttag.

     ACL2 !>(defttag t) ; Install T as an active trust tag.

     TTAG NOTE: Adding ttag T from the top level loop.
      T
     ACL2 !>(sys-call "pwd" nil) ; print the current directory and return NIL
     /u/kaufmann
     NIL
     ACL2 !>(defttag nil) ; Remove the active trust tag (using value NIL).
      NIL
     ACL2 !>(sys-call "pwd" nil) ; Now we get the error again:

     ACL2 Error in TOP-LEVEL:  The SYS-CALL function cannot be called unless
     a trust tag is in effect.  See :DOC defttag.

     ACL2 !>

Of course, using sys-call with the Linux command pwd is not likely to
cause any soundness problems!  So suppose we want to create a function
that prints the working directory.  We might put the following events
into a book that is to be certified.

     (in-package "ACL2")
     (defttag :pwd-ttag)
     (defun print-working-dir ()
       (declare (xargs :mode :program))
       (sys-call "pwd" nil))
     (defttag nil) ; optional (books end with this implicitly)

We can certify this book with a specification that :pwd-ttag is a legal
trust tag:

     (certify-book "pwd" 0 t :ttags (:pwd-ttag))

One can now use this book by executing include-book with keyword
parameter :ttags (:pwd-ttag) and then calling function
print-working-dir:

     (include-book "pwd" :ttags (:pwd-ttag))
     (print-working-dir) ; working directory is printed to terminal

*Detailed documentation.*

     General Forms:
     (defttag tag-name)
     (defttag tag-name :doc doc-string)

where tag-name is a symbol.  The :doc doc-string argument is optional;
if supplied, then it must be a valid documentation string (see
DOC-STRING), and the defttag call will generate a corresponding
defdoc event.  For the rest of this discussion we ignore the :doc
argument.

This event introduces or removes a so-called active trust tag (or
"ttag", pronounced "tee tag").  An active ttag is a non-nil symbol
(tag) that is associated with potentially unsafe evaluation.  For
example, calls of sys-call are illegal unless there is an active trust
tag.  An active trust tag can be installed using a defttag event.  If
one introduces an active ttag and then writes definitions that calls
sys-call, presumably in a defensibly "safe" way, then responsibility
for those calls is attributed to that ttag.  This attribution (or
blame!) is at the level of books; a book's certificate contains a list
of ttags that are active in that book, or in a book that is included
(possibly locally), or in a book included in a book that is included
(either inclusion being potentially local), and so on.  We explain all
this in more detail below.

(Defttag tag-name) is essentially equivalent to

     (table acl2-defaults-table :ttag tag-name)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  We say more about the scope of
defttag forms below.

Note: This is an event!  It does not print the usual event summary but
nevertheless executes the above table event and hence changes the ACL2
logical world, and is so recorded.  Although no event summary is
printed, it is important to note that the "TTAG NOTE", discussed below,
is always printed for a non-nil tag-name.

*Active ttags.*  Suppose tag-name is a non-nil symbol.  Then (defttag
tag-name) sets tag-name to be the "active ttag."  There must be an
active ttag in order for there to be any mention of certain function
and macro symbols, including sys-call; evaluate the form (strip-cars
*ttag-fns-and-macros*) to see the full list of such symbols.  On the
other hand, (defttag nil) removes the active ttag, if any; there is
then no active ttag.  The scope of a defttag form in a book being
certified or included is limited to subsequent forms in the same book
before the next defttag (if any) in that book.  Similarly, if a defttag
form is evaluated in the top-level loop, then its effect is limited to
subsequent forms in the top-level loop before the next defttag in the
top-level loop (if any).  Moreoever, certify-book is illegal when a
ttag is active; of course, in such a circumstance one can execute
(defttag nil) in order to allow book certification.

*Ttag notes and the "certifier."*  When a defttag is executed with an
argument other than nil, output is printed, starting on a fresh line
with:  TTAG NOTE.  For example:

     ACL2 !>(defttag foo)

     TTAG NOTE: Adding ttag FOO from the top level loop.
      FOO
     ACL2 !>

If the defttag occurs in an included book, the message looks like this.

     TTAG NOTE (for included book): Adding ttag FOO from file /u/smith/acl2/my-book.lisp.

The "TTAG NOTE" message is always printed on a single line.  The
intention is that one can search the standard output for all such notes
in order to find all defttag events.  In a sense, defttag events can
allow you to define your own system on top of ACL2 (for example, see
PROGN!).  So in order for someone else (who we might call the
"certifier") to be confident that your collection of books is
meaningful, that certifier should certify all the user-supplied books
from scratch and check either that no :ttags were supplied to
certify-book, or else look for every TTAG NOTE in the standard output
in order to locate all defttag events with non-nil tag-name.  In this
way, the certifier can in principle decide whether to be satisfied that
those defttag events did not allow inappropriate forms in the
user-supplied books.

*Allowed ttags when certifying and including books.*  A defttag form
may not be evaluated unless its argument is a so-called "allowed" ttag.
All ttags are allowed in the interactive top-level loop.  However,
during certify-book and include-book, the set of allowed ttags is
restricted according to the :ttags keyword argument.  If this argument
is omitted then no ttag is allowed, so a defttag call will fail during
book certification or inclusion in this case.  This restriction applies
even to defttag forms already evaluated in the so-called certification
world at the time certify-book is called.  But note that (defttag nil)
is always legal.

A :ttags argument of certify-book and include-book can have value :all,
indicating that every ttag is allowed, i.e., no restriction is being
placed on the arguments, just as in the interactive top-level loop.
Otherwise, the value is a true list of ttag specifications, each having
one of the following forms, where sym is a non-nil symbol.

     (1) sym

     (2) (sym)

     (3) (sym x1 x2 ... xk), where k > 0 and each xi is a string, except
     that one xi may be nil.

In Case (1), (defttag sym) is allowed to occur in at most one book or
else in the top-level loop (i.e., the certification world for a book
under certification or a book being included).  Case (2) allows
(defttag sym) to occur in an unlimited number of books.  For case (3)
the xi specify where (defttag sym) may occur, as follows.  The case
that xi is nil refers to the top-level loop, while all other xi are
filenames, where the ".lisp" extension is optional and relative
pathnames are considered to be relative to the connected book directory
(see CBD).

An error message, as shown below, illustrates how ACL2 enforcess the
notion of allowed ttags.  Suppose that you call certify-book with
argument :ttags (foo), where you have already executed (defttag foo) in
the certification world (i.e., before calling certify-book).  Then ACL2
immediately associates the ttag foo with nil, where again, nil refers
to the top-level loop.  If ACL2 then encounters (defttag foo) inside
that book, you will get the following error (using the full book name
for the book, as shown):

     ACL2 Error in ( TABLE ACL2-DEFAULTS-TABLE ...):  The ttag FOO associated
     with file /u/smith/work/my-book.lisp is not among the set of ttags permitted
     in the current context, specified as follows:
       ((FOO NIL)).
     See :DOC defttag.

In general the structure displayed by the error message, which is ((FOO
NIL)) in this case, represents the currently allowed ttags with
elements as discussed in (1) through (3) above.  In this case, that
list's unique element is (FOO NIL), meaning that ttag FOO is only
allowed at the top level (as represented by NIL).

*Associating ttags with books and with the top-level loop.*  When a book
is certified, each form (defttag tag) that is encountered for non-nil
tag in that book or an included book is recorded in the generated
certificate, which associates tag with the full-book-name of the book
containing that deftag.  If such a defttag form is encountered outside
a book, hence in the portcullis of the book being certified or one of
its included books, then tag is associated with nil in the generated
certificate.  Note that the notion of "included book" here applies to
the recursive notion of a book either included directly in the book
being certified or else included in such a book, where we account even
for locally included books.

For examples of ways to take advantage of ttags, see
books/hacking/hacker.lisp and see TTAGS-SEEN, see
PROGN!, see REMOVE-UNTOUCHABLE, see SET-RAW-MODE, and
see SYS-CALL.