This is documentation for ACL2 Version 3.0
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.

REWRITE    make some :rewrite rules (possibly conditional ones)

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Example :corollary
formulas from which :rewrite rules might be built are:

     Example:
     (equal (+ x y) (+ y x))            replace (+ a b) by (+ b a) provided
                                        certain heuristics approve the
                                        permutation.

     (implies (true-listp x)            replace (append a nil) by a, if
              (equal (append x nil) x)) (true-listp a) rewrites to t

     (implies                           replace (member a (append b c)) by
         (and (eqlablep e)              (member a (append c b)) in contexts
              (true-listp x)            in which propositional equivalence
              (true-listp y))           is sufficient, provided (eqlablep a)
         (iff (member e (append x y))   (true-listp b) and (true-listp c)
              (member e (append y x)))) rewrite to t and the permutative
                                        heuristics approve

     General Form:
     (and ...
          (implies (and ...hi...)
                   (implies (and ...hk...)
                            (and ...
                                 (equiv lhs rhs)
                                 ...)))
          ...)

Note: One :rewrite rule class object might create many rewrite rules
from the :corollary formula.  To create the rules, we first translate
the formula (expanding all macros; also see TRANS).  Next, we
eliminate all lambdas; one may think of this step as simply substituting
away every let, let*, and mv-let in the formula.  We then flatten the
and and implies structure of the formula, transforming it into a
conjunction of formulas, each of the form

     (implies (and h1 ... hn) concl)

where no hypothesis is a conjunction and concl is neither a conjunction
nor an implication.  If necessary, the hypothesis of such a conjunct may
be vacuous.  We then further coerce each concl into the form (equiv lhs
rhs), where equiv is a known equivalence relation, by replacing any
concl not of that form by (iff concl t).  A concl of the form (not term)
is considered to be of the form (iff term nil).  By these steps we
reduce the given :corollary to a sequence of conjuncts, each of which is
of the form

     (implies (and h1 ... hn)
              (equiv lhs rhs))

where equiv is a known equivalence relation.  See EQUIVALENCEfor
a general discussion of the introduction of new equivalence relations.

We create a :rewrite rule for each such conjunct, if possible, and
otherwise cause an error.  It is possible to create a rewrite rule from
such a conjunct provided lhs is not a variable, a quoted constant, a
let-expression, a lambda application, or an if-expression.

A :rewrite rule is used when any instance of the lhs occurs in a context
in which the equivalence relation is operative.  First, we find a
substitution that makes lhs equal to the target term.  Then we attempt
to relieve the instantiated hypotheses of the rule.  Hypotheses that are
fully instantiated are relieved by recursive rewriting.  Hypotheses that
contain "free variables" (variables not assigned by the unifying
substitution) are relieved by attempting to guess a suitable instance so
as to make the hypothesis equal to some known assumption in the context
of the target.  If the hypotheses are relieved, and certain restrictions
that prevent some forms of infinite regress are met (see
LOOP-STOPPER), the target is replaced by the instantiated rhs, which
is then recursively rewritten.

At the moment, the best description of how ACL2 :rewrite rules are used
may be found in the discussion of "Replacement Rules" on page 279 of A
Computational Logic Handbook (second edition).

TYPE-PRESCRIPTION    make a rule that specifies the type of a term

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Some example :corollary
formulas from which :type-prescription rules might be built are:

     Examples:
     (implies                           (nth n lst) is of type characterp
      (and (character-listp lst)        provided the two hypotheses can
           (< n (length lst)))          be established by type reasoning
      (characterp (nth n lst))).

     (implies                           (demodulize a lst 'value ans) is
      (and (atom a)                     either a nonnegative integer or
           (true-listp lst)             of the same type as ans, provided
           (member-equal a lst))        the hyps can be established by type
      (or (and                          reasoning
            (integerp
             (demodulize a lst 'value ans))
            (>= (demodulize a lst 'value ans) 0))
          (equal (demodulize a lst 'value ans) ans))).

To specify the term whose type (see TYPE-SET) is described by
the rule, provide that term as the value of the :typed-term field of the
rule class object.

     General Form:
     (implies hyps
              (or type-restriction1-on-pat
                  ...
                  type-restrictionk-on-pat
                  (equal pat var1)
                  ...
                  (equal pat varj)))

where pat is the application of some function symbol to some arguments,
each type-restrictioni-on-pat is a term involving pat and containing no
variables outside of the occurrences of pat, and each vari is one of the
variables of pat.  Generally speaking, the type-restriction terms ought
to be terms that inform us as to the type of pat.  Ideally, they should
be "primitive recognizing expressions" about pat; see
COMPOUND-RECOGNIZER.

If the :typed-term is not provided in the rule class object, it is
computed heuristically by looking for a term in the conclusion whose
type is being restricted.  An error is caused if no such term is found.

Roughly speaking, the effect of adding such a rule is to inform the ACL2
typing mechanism that pat has the type described by the conclusion, when
the hypotheses are true.  In particular, the type of pat is within the
union of the types described by the several disjuncts.  The "type
described by" (equal pat vari) is the type of vari.

More operationally, when asked to determine the type of a term that is
an instance of pat, ACL2 will first attempt to establish the hypotheses.
*This is done by type reasoning alone, not rewriting!* Of course, if
some hypothesis is to be forced, it is so treated; see FORCE and
see CASE-SPLIT.  So-called free variables in hypotheses are
treated specially; see FREE-VARIABLES.  Provided the hypotheses
are established by type reasoning, ACL2 then unions the types described
by the type-restrictioni-on-pat terms together with the types of those
subexpressions of pat identified by the vari.  The final type computed
for a term is the intersection of the types implied by each applicable
rule.  Type prescription rules may be disabled.

Because only type reasoning is used to establish the hypotheses of
:type-prescription rules, some care must be taken with the hypotheses.
Suppose, for example, that the non-recursive function my-statep is
defined as

       (defun my-statep (x)
         (and (true-listp x)
              (equal (length x) 2)))

and suppose (my-statep s) occurs as a hypothesis of a :type-prescription
rule that is being considered for use in the proof attempt for a
conjecture with the hypothesis (my-statep s).  Since the hypothesis in
the conjecture is rewritten, it will become the conjunction of
(true-listp s) and (equal (length s) 2).  Those two terms will be
assumed to have type t in the context in which the :type-prescription
rule is tried.  But type reasoning will be unable to deduce that
(my-statep s) has type t in this context.  Thus, either my-statep should
be disabled (see DISABLE) during the proof attempt or else the
occurrence of (my-statep s) in the :type-prescription rule should be
replaced by the conjunction into which it rewrites.

While this example makes it clear how non-recursive predicates can cause
problems, non-recursive functions in general can cause problems.  For
example, if (mitigate x) is defined to be (if (rationalp x) (1- x) x)
then the hypothesis (pred (mitigate s)) in the conjecture will rewrite,
opening mitigate and splitting the conjecture into two subgoals, one in
which (rationalp s) and (pred (1- x)) are assumed and the other in which
(not (rationalp s)) and (pred x) are assumed.  But (pred (mitigate s))
will not be typed as t in either of these contexts.  The moral is:
beware of non-recursive functions occuring in the hypotheses of
:type-prescription rules.

Because of the freedom one has in forming the conclusion of a
type-prescription, we have to use heuristics to recover the pattern,
pat, whose type is being specified.  In some cases our heuristics may
not identify the intended term and the :type-prescription rule will be
rejected as illegal because the conclusion is not of the correct form.
When this happens you may wish to specify the pat directly.  This may be
done by using a suitable rule class token.  In particular, when the
token :type-prescription is used it means ACL2 is to compute pat with
its heuristics; otherwise the token should be of the form
(:type-prescription :typed-term pat), where pat is the term whose type
is being specified.

The defun event may generate a :type-prescription rule.  Suppose fn is
the name of the function concerned.  Then (:type-prescription fn) is the
rune given to the type-prescription, if any, generated for fn by defun.
(The trivial rule, saying fn has unknown type, is not stored, but defun
still allocates the rune and the corollary of this rune is known to be
t.)

TYPE-SET-INVERTER    exhibit a new decoding for an ACL2 type-set

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.

     Example Rule Class:
     (:type-set-inverter
       :corollary (equal (and (counting-number x) (not (equal x 0)))
                         (and (integerp x) (< x 0)))
       :type-set 2)

     General Forms of Rule Class:
     :type-set-inverter, or
     (:type-set-inverter :type-set n)

     General Form of Theorem or Corollary:
     (EQUAL new-expr old-expr)

where n is a type-set (see TYPE-SET) and old-expr is the term
containing x as a free variable that ACL2 currently uses to recognize
type-set n.  For a given n, the exact form of old-expr is generated by

     (convert-type-set-to-term 'x n (ens state) (w state) nil)].

If the :type-set field of the rule-class is omitted, we attempt to
compute it from the right-hand side, old-expr, of the corollary.  That
computation is done by type-set-implied-by-term (see TYPE-SET).
However, it is possible that the type-set we compute from lhs does not
have the required property that when inverted with
convert-type-set-to-term the result is lhs.  If you omit :type-set and
an error is caused because lhs has the incorrect form, you should
manually specify both :type-set and the lhs generated by
convert-type-set-to-term.

The rule generated will henceforth make new-expr be the term used by
ACL2 to recognize type-set n.  If this rule is created by a defthm event
named name then the rune of the rule is (:type-set-inverter name) and by
disabling that rune you can prevent its being used to decode type-sets.

Type-sets are inverted when forced assumptions are turned into formulas
to be proved.  In their internal form, assumptions are essentially pairs
consisting of a context and a goal term, which was forced.  Abstractly a
context is just a list of hypotheses which may be assumed while proving
the goal term.  But actually contexts are alists which pair terms with
type-sets, encoding the current hypotheses.  For example, if the
original conjecture contained the hypothesis (integerp x) then the
context used while working on that conjecture will include the
assignment to x of the type-set *ts-integer*.

WELL-FOUNDED-RELATION    show that a relation is well-founded on a set

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :well-founded-relation rule might be built is as
follows.  (Of course, the functions pairp, lex2p, and ordinate would
have to be defined first.)

     Example:
     (and (implies (pairp x) (o-p (ordinate x)))
          (implies (and (pairp x)
                        (pairp y)
                        (lex2p x y))
                   (o< (ordinate x) (ordinate y))))

The above example establishes that lex2p is a well-founded relation on
pairps.  We explain and give details below.

Exactly two general forms are recognized:

     General Forms
     (AND (IMPLIES (mp x) (O-P (fn x)))              ; Property 1
          (IMPLIES (AND (mp x)                       ; Property 2
                        (mp y)
                        (rel x y))
                   (O< (fn x) (fn y)))),

or

     (AND (O-P (fn x))                               ; Property 1
          (IMPLIES (rel x y)                         ; Property 2
                   (O< (fn x) (fn y))))

where mp, fn, and rel are function symbols, x and y are distinct
variable symbols, and no other :well-founded-relation theorem about fn
has been proved.  When the second general form is used, we act as though
the first form were used with mp being the function that ignores its
argument and returns t.  The discussion below therefore considers only
the first general form.

Note: We are very rigid when checking that the submitted formula is of
one of these forms.  For example, in the first form, we insist that all
the conjuncts appear in the order shown above.  Thus, interchanging the
two properties in the top-level conjunct or rearranging the hyptheses in
the second conjunct both produce unrecognized forms.  The requirement
that each fn be proved well-founded at most once ensures that for each
well-founded relation, fn, there is a unique mp that recognizes the
domain on which rel is well-founded.  We impose this requirement simply
so that rel can be used as a short-hand when specifying the well-founded
relations to be used in definitions; otherwise the specification would
have to indicate which mp was to be used.

Mp is a predicate that recognizes the objects that are supposedly
ordered in a well-founded way by rel.  We call such an object an
"mp-measure" or simply a "measure" when mp is understood.  Property 1
tells us that every measure can be mapped into an ACL2 ordinal.  (See
O-P.)  This mapping is performed by fn.  Property 2 tells us
that if the measure x is smaller than the measure y according to rel
then the image of x under fn is a smaller than that of y, according to
the well-founded relation o<.  (See O<.)  Thus, the general form
of a :well-founded-relation formula establishes that there exists a
rel-order preserving embedding (namely via fn) of the mp-measures into
the ordinals.  We can thus conclude that rel is well-founded on
mp-measures.

Such well-founded relations are used in the admissibility test for
recursive functions, in particular, to show that the recursion
terminates.  To illustrate how such information may be used, consider a
generic function definition

     (defun g (x) (if (test x) (g (step x)) (base x))).

If rel has been shown to be well-founded on mp-measures, then g's
termination can be ensured by finding a measure, (m x), with the
property that m produces a measure:

     (mp (m x)),                                     ; Defun-goal-1

and that the argument to g gets smaller (when measured by m and compared
by rel) in the recursion,

     (implies (test x) (rel (m (step x)) (m x))).    ; Defun-goal-2

If rel is selected as the :well-founded-relation to be used in the
definition of g, the definitional principal will generate and attempt to
prove defun-goal-1 and defun-goal-2 to justify g.  We show later why
these two goals are sufficient to establish the termination of g.
Observe that neither the ordinals nor the embedding, fn, of the
mp-measures into the ordinals is involved in the goals generated by the
definitional principal.

Suppose now that a :well-founded-relation theorem has been proved for mp
and rel.  How can rel be "selected as the :well-founded-relation" by
defun?  There are two ways.  First, an xargs keyword to the defun event
allows the specification of a :well-founded-relation.  Thus, the
definition of g above might be written

     (defun g (x)
      (declare (xargs :well-founded-relation (mp . rel)))
      (if (test x) (g (step x)) (base x)))

Alternatively, rel may be specified as the
:default-well-founded-relation in acl2-defaults-table by executing the
event

     (set-default-well-founded-relation rel).

When a defun event does not explicitly specify the relation in its xargs
the default relation is used.  When ACL2 is initialized, the default
relation is o<.

Finally, though it is probably obvious, we now show that defun-goal-1
and defun-goal-2 are sufficient to ensure the termination of g provided
property-1 and property-2 of mp and rel have been proved.  To this end,
assume we have proved defun-goal-1 and defun-goal-2 as well as
property-1 and property-2 and we show how to admit g under the primitive
ACL2 definitional principal (i.e., using only the ordinals).  In
particular, consider the definition event

     (defun g (x)
      (declare (xargs :well-founded-relation o<
                      :measure (fn (m x))))
      (if (test x) (g (step x)) (base x)))

Proof that g is admissible: To admit the definition of g above we must
prove

     (o-p (fn (m x)))                        ; *1

and

     (implies (test x)                               ; *2
              (o< (fn (m (step x))) (fn (m x)))).

But *1 can be proved by instantiating property-1 to get

     (implies (mp (m x)) (o-p (fn (m x)))),

and then relieving the hypothesis with defun-goal-1, (mp (m x)).

Similarly, *2 can be proved by instantiating property-2 to get

     (implies (and (mp (m (step x)))
                   (mp (m x))
                   (rel (m (step x)) (m x)))
              (o< (fn (m (step x))) (fn (m x))))

and relieving the first two hypotheses by appealing to two instances of
defun-goal-1, thus obtaining

     (implies (rel (m (step x)) (m x))
              (o< (fn (m (step x))) (fn (m x)))).

By chaining this together with defun-goal-2,

     (implies (test x)
              (rel (m (step x)) (m x)))

we obtain *2.  Q.E.D.

STOBJ    single-threaded objects or "von Neumann bottlenecks"

In ACL2, a "single-threaded object" is a data structure whose use is so
syntactically restricted that only one instance of the object need ever
exist and its fields can be updated by destructive assignments.

The documentation in this section is laid out in the form of a tour that
visits the documented topics in a reasonable order.  We recommend that
you follow the tour the first time you read about stobjs.  The list of
all stobj topics is shown below.  The tour starts immediately
afterwards.

As noted, a "single-threaded object" is a data structure whose use is so
syntactically restricted that only one instance of the object need ever
exist.  Updates to the object must be sequentialized.  This allows us to
update its fields with destructive assignments without wrecking the
axiomatic semantics of update-by-copy.  For this reason, single-threaded
objects are sometimes called "von Neumann bottlenecks."

From the logical perspective, a single-threaded object is an ordinary
ACL2 object, e.g., composed of integers and conses.  Logically speaking,
ordinary ACL2 functions are defined to allow the user to "access" and
"update" its fields.  Logically speaking, when fields in the object,
obj, are "updated" with new values, a new object, obj', is constructed.

But suppose that by syntactic means we could ensure that there were no
more references to the "old" object, obj.  Then we could create obj' by
destructively modifying the memory locations involved in the
representation of obj.  The syntactic means is pretty simple but
draconian: the only reference to obj is in the variable named OBJ.

The consequences of this simple rule are far-reaching and require some
getting used to.  For example, if OBJ has been declared as a
single-threaded object name, then:

obj.

expression" that can be passed into that slot is the variable OBJ, not
merely a term that "evaluates to an obj"; thus, such functions can only
operate on the current object.  So for example, instead of (FOO
(UPDATE-FIELD1 3 ST)) write (LET ((ST (UPDATE-FIELD1 3 ST))) (FOO ST)).

those functions can only be applied to the current object.

the variable OBJ.  Thus, for example, obj may not be consed into a list
(which would create another pointer to it) or accessed or copied via
"unapproved" means.

updater is called, the only variable which can hold its result is OBJ.

(either as the sole value returned, or in (mv ... OBJ ...); see
MV).

object becomes the new current value of OBJ.

What makes ACL2 different from other functional languages supporting
such operations (e.g., Haskell's "monads" and Clean's "uniqueness type
system") is that ACL2 also gives single-threaded objects an explicit
axiomatic semantics so that theorems can be proved about them.  In
particular, the syntactic restrictions noted above are enforced only
when single-threaded objects are used in function definitions (which
might be executed outside of the ACL2 read-eval-print loop in Common
Lisp).  The accessor and update functions for single-threaded objects
may be used without restriction in formulas to be proved.  Since
function evaluation is sometimes necessary during proofs, ACL2 must be
able to evaluate these functions on logical constants representing the
object, even when the constant is not "the current object."  Thus, ACL2
supports both the efficient von Neumann semantics and the clean
applicative semantics, and uses the first in contexts where execution
speed is paramount and the second during proofs.

To start the stobj tour, see STOBJ-EXAMPLE-1.

DECLARE-STOBJS    declaring a formal parameter name to be a single-threaded object

When a defun uses one of its formals as a single-threaded object
(stobj), the defun *must* include a declaration that the formal is to be
so used.  An exception is the formal "state," which if not declared as
explained below, may still be used provided an appropriate global
"declaration" is issued: see SET-STATE-OK.

If the formal in question is counters then an appropriate declaration is

     (declare (xargs :stobjs counters))

or, more generally,

     (declare (xargs :stobjs (... counters ...)))

where all the single-threaded formals are listed.

For such a declaration to be legal it must be the case that all the
names have previously been defined as single-threaded objects with
defstobj.

When an argument is declared to be single-threaded the guard of the
function is augmented by conjoining to it the condition that the
argument satisfy the recognizer for the single-threaded object.
Furthermore, the syntactic checks done to enforce the legal use of
single-threaded objects are also sufficient to allow these guard
conjuncts to be automatically proved.

The obvious question arises: Why does ACL2 insist that you declare stobj
names before using them in defuns if you can only declare names that
have already been defined with defstobj?  What would go wrong if a
formal were treated as a single-threaded object if and only if it had
already been so defined?

Suppose that one user, say Jones, creates a book in which counters is
defined as a single-threaded object.  Suppose another user, Smith,
creates a book in which counters is used as an ordinary formal
parameter.  Finally, suppose a third user, Brown, wishes to use both
books.  If Brown includes Jones' book first and then Smith's, then
Smith's function treats counters as single-threaded.  But if Brown
includes Smith's book first, the argument is treated as ordinary.

ACL2 insists on the declaration to ensure that the definition is
processed the same way no matter what the context.

RESIZE-LIST    list resizer in support of stobjs

(Resize-list lst n default-value) takes a list, lst, and a desired
length, n, for the result list, as well as a default-value to use for
the extra elements if n is greater than the length of lst.

Resize-list has a guard of t.  This function is called in the body of
function, resize-<a> where <a> is an array field of a stobj.  See
STOBJ and see DEFSTOBJ.

STOBJ-EXAMPLE-1    an example of the use of single-threaded objects

Suppose we want to sweep a tree and (1) count the number of interior
nodes, (2) count the number of tips and (3) keep a record of every tip
we encounter that is an integer.  We could use a single-threaded object
as our "accumulator".  Such an object would have three fields, one
holding the number of nodes seen so far, one holding the number of tips,
and one holding all the integer tips seen.

The following event declares counters to be a single-threaded object.

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

It has three fields, NodeCnt, TipCnt, and IntTipsSeen.  (As always in
ACL2, capitalization is irrelevant in simple symbol names, so the first
name could be written nodecnt or NODECNT, etc.) Those are the name of
the accessor functions for the object.  The corresponding update
functions are named update-NodeCnt, update-TipCnt and
update-IntTipsSeen.

If you do not like the default function names chosen above, there is a
feature in the defstobj event that allows you to specify other names.

If you want to see the ACL2 definitions of all the functions defined by
this event, look at stobj-example-1-defuns.

If, after this event, we evaluate the top-level "global variable"
counters in the ACL2 read-eval-print loop we get:

     ACL2 !>counters
     <counters>

Note that the value printed is "<counters>".  Actually, the value of
counters in the logic is (0 0 NIL).  But ACL2 always prints
single-threaded objects in this non-informative way because they are
usually so big that to do otherwise would be unpleasant.

Had you tried to evaluate the "global variable" counters before
declaring it a single-threaded object, ACL2 would have complained that
it does not support global variables.  So a lesson here is that once you
have declared a new single-threaded object your top-level forms can
reference it.  In versions of ACL2 prior to Version 2.4 the only
variable enjoying this status was STATE.  single-threaded objects are a
straightforward generalization of the long-implemented von Neumann state
feature of ACL2.

We can access the fields of counters as with:

     ACL2 !>(NodeCnt counters)
     0
     ACL2 !>(IntTipsSeen counters)
     NIL

and we can set the fields of counters as with:

     ACL2 !>(update-NodeCnt 3 counters)
     <counters>
     ACL2 !>(NodeCnt counters)
     3

Observe that when we evaluate an expression that returns a counter
object, that object becomes the "current value" of counters.

Here is a function that "converts" the counters object to its "ordinary"
representation:

     (defun show-counters (counters)
       (declare (xargs :stobjs (counters)))
       (list (NodeCnt counters)
             (TipCnt counters)
             (IntTipsSeen counters)))

Observe that we *must* declare, at the top of the defun, that we mean to
use the formal parameter counters as a single-threaded object!  If we
did not make this declaration, the body of show-counters would be
processed as though counters were an ordinary object.  An error would be
caused because the accessors used above cannot be applied to anything
but the single-threaded object counters.  If you want to know why we
insist on this declaration, see DECLARE-STOBJS.

When show-counters is admitted, the following message is printed:

     Since SHOW-COUNTERS is non-recursive, its admission is trivial.  We
     observe that the type of SHOW-COUNTERS is described by the theorem
     (AND (CONSP (SHOW-COUNTERS COUNTERS))
          (TRUE-LISTP (SHOW-COUNTERS COUNTERS))).
     We used primitive type reasoning.

     (SHOW-COUNTERS COUNTERS) => *.

     The guard conjecture for SHOW-COUNTERS is trivial to prove.
     SHOW-COUNTERS is compliant with Common Lisp.

The line above containing the "=>" is called the "signature" of
show-counters; it conveys the information that the first argument is the
single-threaded object counters and the only result is an ordinary
object.  Here is an example of another signature:

     (PROCESSOR * * COUNTERS) => (MV * COUNTERS)

which indicates that the function PROCESSOR (which we haven't shown you)
takes three arguments, the third of which is the COUNTERS stobj, and
returns two results, the second of which is the modified COUNTERS.

Returning to the admission of show-counters above, the last sentence
printed indicates that the guard conjectures for the function were
proved.  When some argument of a function is declared to be a
single-threaded object via the xargs :stobj, we automatically add
(conjoin) to the guard the condition that the argument satisfy the
recognizer for that single-threaded object.  In the case of
show-counters the guard is (countersp counters).

Here is an example of show-counters being called:

     ACL2 !>(show-counters counters)
     (3 0 NIL)

This is what we would see had we set the NodeCnt field of the initial
value of counters to 3, as we did earlier in this example.

We next wish to define a function to reset the counters object.  We
could define it this way:

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (let ((counters (update-NodeCnt 0 counters)))
         (let ((counters (update-TipCnt 0 counters)))
           (update-IntTipsSeen nil counters))))

which "successively" sets the NodeCnt field to 0, then the TipCnt field
to 0, and then the IntTipsSeen field to nil and returns the resulting
object.

However, the nest of let expressions is tedious and we use this
definition instead.  This definition exploits a macro, here named "seq"
(for "sequentially") which evaluates each of the forms given, binding
their results successively to the stobj name given.

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (seq counters
            (update-NodeCnt 0 counters)
            (update-TipCnt 0 counters)
            (update-IntTipsSeen nil counters)))

This definition is syntactically identical to the one above, after macro
expansion.  Our definition of seq is shown below and is not part of
native ACL2.

     (defmacro seq (stobj &rest rst)
       (cond ((endp rst) stobj)
             ((endp (cdr rst)) (car rst))
             (t `(let ((,stobj ,(car rst)))
                  (seq ,stobj ,@(cdr rst))))))

The signature printed for reset-counters is

     (RESET-COUNTERS COUNTERS) => COUNTERS.

Here is an example.

     ACL2 !>(show-counters counters)
     (3 0 NIL)
     ACL2 !>(reset-counters counters)
     <counters>
     ACL2 !>(show-counters counters)
     (0 0 NIL)

Here finally is a function that uses counters as a single-threaded
accumulator to collect the desired information about the tree x.

     (defun sweep-tree (x counters)
       (declare (xargs :stobjs (counters)))
       (cond ((atom x)
              (seq counters
                   (update-TipCnt (+ 1 (TipCnt counters)) counters)
                   (if (integerp x)
                       (update-IntTipsSeen (cons x (IntTipsSeen counters))
                                       counters)
                     counters)))
             (t (seq counters
                     (update-NodeCnt (+ 1 (NodeCnt counters)) counters)
                     (sweep-tree (car x) counters)
                     (sweep-tree (cdr x) counters)))))

We can paraphrase this definition as follows.  If x is an atom, then
increment the TipCnt field of counters and *then*, if x is an integer,
add x to the IntTipsSeen field, and return counters.  On the other hand,
if x is not an atom, then increment the NodeCnt field of counters, and
*then* sweep the car of x and *then* sweep the cdr of x and return the
result.

Here is an example of its execution.  We have displayed the input tree
in full dot notation so that the number of interior nodes is just the
number of dots.

     ACL2 !>(sweep-tree '((((a . 1) . (2 . b)) . 3)
                          . (4 . (5 . d)))
                        counters)
     <counters>
     ACL2 !>(show-counters counters)
     (7 8 (5 4 3 2 1))
     ACL2 !>(reset-counters counters)
     <counters>
     ACL2 !>(show-counters counters)
     (0 0 NIL)

The counters object has two integer fields and a field whose type is
unrestricted.  single-threaded objects support other types of fields,
such as arrays.  We deal with that in the stobj-example-2.  But we
recommend that you first consider the implementation issues for the
counters example (in stobj-example-1-implementation) and then consider
the proof issues (in stobj-example-1-proofs).

To continue the stobj tour, see STOBJ-EXAMPLE-2.

STOBJ-EXAMPLE-1-DEFUNS    the defuns created by the counters stobj

Consider the event shown in stobj-example-1:

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

Here is a complete list of the defuns added by the event.

The careful reader will note that the counters argument below is *not*
declared with the :stobjs xarg even though we insist that the argument
be a stobj in calls of these functions.  This "mystery" is explained
below.

     (defun NodeCntp (x)                 ;;; Recognizer for 1st field
       (declare (xargs :guard t :verify-guards t))
       (integerp x))

     (defun TipCntp (x)                  ;;; Recognizer for 2nd field
       (declare (xargs :guard t :verify-guards t))
       (integerp x))

     (defun IntTipsSeenp (x)             ;;; Recognizer for 3rd field
       (declare (xargs :guard t :verify-guards t) (ignore x))
       t)

     (defun countersp (counters)         ;;; Recognizer for object
       (declare (xargs :guard t :verify-guards t))
       (and (true-listp counters)
            (= (length counters) 3)
            (NodeCntp (nth 0 counters))
            (TipCntp (nth 1 counters))
            (IntTipsSeenp (nth 2 counters))
            t))

     (defun create-counters ()           ;;; Creator for object
       (declare (xargs :guard t :verify-guards t))
       (list '0 '0 'nil))

     (defun NodeCnt (counters)           ;;; Accessor for 1st field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 0 counters))

     (defun update-NodeCnt (v counters)  ;;; Updater for 1st field
       (declare (xargs :guard
                       (and (integerp v)
                            (countersp counters))
                       :verify-guards t))
       (update-nth 0 v counters))

     (defun TipCnt (counters)            ;;; Accessor for 2nd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 1 counters))

     (defun update-TipCnt (v counters)   ;;; Updater for 2nd field
       (declare (xargs :guard
                       (and (integerp v)
                            (countersp counters))
                       :verify-guards t))
       (update-nth 1 v counters))

     (defun IntTipsSeen (counters)       ;;; Accessor for 3rd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 2 counters))

     (defun update-IntTipsSeen (v counters) ;;; Updater for 3rd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (update-nth 2 v counters))

Observe that there is a recognizer for each of the three fields and then
a recognizer for the counters object itself.  Then, for each field,
there is an accessor and an updater.

Observe also that the functions are guarded so that they expect a
countersp for their counters argument and an appropriate value for the
new field values.

You can see all of the defuns added by a defstobj event by executing the
event and then using the :pcb! command on the stobj name.  E.g.,

     ACL2 !>:pcb! counters

will print the defuns above.

We now clear up the "mystery" mentioned above.  Note, for example in
TipCnt, that the formal counters is used.  From the discussion in
stobj-example-1 it has been made clear that TipCnt can only be called on
the counters object.  And yet, in that same discussion it was said that
an argument is so treated only if it it declared among the :stobjs in
the definition of the function.  So why doesn't TipCnt include something
like (declare (xargs :stobjs (counters)))?

The explanation of this mystery is as follows.  At the time TipCnt was
defined, during the introduction of the counters stobj, the name
"counters" was not yet a single-threaded object.  The introduction of a
new single-threaded object occurs in three steps: (1) The new primitive
recognizers, accessors, and updaters are introduced as "ordinary
functions," producing their logical axiomatizations.  (2) The executable
counterparts are defined in raw Lisp to support destructive updating.
(3) The new name is declared a single-threaded object to ensure that all
future use of these primitives respects the single-threadedness of the
object.  The functions defined as part of the introduction of a new
single-threaded object are the only functions in the system that have
undeclared stobj formals other than state.

You may return to stobj-example-1 here.

STOBJ-EXAMPLE-1-IMPLEMENTATION    the implementation of the counters stobj

the event

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

discussed in stobj-example-1, creates a Common Lisp object to represent
the current value of counters.  That object is created by evaluating
either of the following "raw" (non-ACL2) Common Lisp forms:

     (create-counters)

     (vector (make-array 1 :element-type 'integer
                           :initial-element '0)
             (make-array 1 :element-type 'integer
                           :initial-element '0)
             'nil)

and the value is stored in the Common Lisp global variable named
*the-live-counters*.

Thus, the counters object is an array of length three.  The first two
elements are arrays of size 1 and are used to hold the NodeCnt and
TipCnt fields.  The third element is the IntTipsSeen field.  The first
two fields are represented by arrays so that we can implement the
integer type specification efficiently.  Generally, integers are "boxed"
in some Common Lisp implementations, for example, GCL.  Creating a new
integer requires creating a new box to put it in.  But in some lisps,
including GCL, the integers inside arrays of integers are not boxed.

The function NodeCnt is defined in raw Lisp as:

     (defun NodeCnt (counters)
       (the integer
            (aref (the (simple-array integer (1))
                       (svref counters 0))
                  0)))

Observe that the form (svref counters 0) is evaluated to get an array of
size 1, which is followed by a call of aref to access the 0th element of
that array.

The function update-NodeCnt is defined in raw Lisp as:

     (defun update-NodeCnt (v counters)
       (declare (type integer v))
       (progn
        (setf (aref (the (simple-array integer (1))
                         (svref counters 0))
                    0)
              (the integer v))
        counters))

Note that when this function is called, it does not create a new vector
of length three, but "smashes" the existing one.

One way to see all the raw Lisp functions defined by a given defstobj is
to evaluate the defstobj event and then evaluate, in the ACL2 loop, the
expression (nth 4 (global-val 'cltl-command (w state))).  Those
functions that contain (DECLARE (STOBJ-INLINE-FN T)) will generate
defabbrev forms because the :inline keyword of defstobj was supplied the
value t.  The rest will generate defuns.

We now recommend that you look at stobj-example-1-proofs.

STOBJ-EXAMPLE-1-PROOFS    some proofs involving the counters stobj

Consider again the event

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

discussed in stobj-example-1, followed by the definition

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (seq counters
            (update-NodeCnt 0 counters)
            (update-TipCnt 0 counters)
            (update-IntTipsSeen nil counters)))

which, because of the seq macro in stobj-example-1, is just syntactic
sugar for

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (let ((counters (update-NodeCnt 0 counters)))
         (let ((counters (update-TipCnt 0 counters)))
           (update-IntTipsSeen nil counters)))).

Here is a simple theorem about reset-counters.

     (defthm reset-counters-is-constant
       (implies (countersp x)
                (equal (reset-counters x)
                       '(0 0 nil))))

Before we talk about how to prove this theorem, note that the theorem is
unusual in two respects.

First, it calls reset-counters on an argument other than the variable
counters!  That is allowed in theorems; logically speaking, the stobj
functions are indistinguishable from ordinary functions.  Their use is
syntactically restricted only in defuns, which might be compiled and run
in raw Lisp.  Those restrictions allow us to implement stobj
modification destructively.  But logically speaking, reset-counters and
other stobj "modifying" functions just create new objects,
constructively.

Second, the theorem above explicitly provides the hypothesis that
reset-counters is being applied to an object satisfying countersp.  Such
a hypothesis is not always required: reset-counters is total and will do
something no matter what x is.  But in this particular case, the result
is not '(0 0 nil) unless x is, at least, a true-list of length three.

To make a long story short, to prove theorems about stobj functions you
behave in exactly the way you would to prove the same theorems about the
same functions defined without the stobj features.

How can we prove the above theorem?  Unfolding the definition of
reset-counters shows that (reset-counters x) is equal to

     (update-IntTipsSeen nil
       (update-TipCnt 0
         (update-NodeCnt 0 x)))

which in turn is

     (update-nth 2 nil
      (update-nth 1 0
       (update-nth 0 0 x))).

Opening up the definition of update-nth reduces this to

     (list* 0 0 nil (cdddr x)).

This is clearly equal to '(0 0 nil), provided we know that (cdddr x) is
nil.

Unfortunately, that last fact requires a lemma.  The most specific lemma
we could provide is

     (defthm special-lemma-for-counters
       (implies (countersp x)
                (equal (cdddr x) nil)))

but if you try to prove that lemma you will find that it requires some
reasoning about len and true-listp.  Furthermore, the special lemma
above is of interest only for counters.

The following lemma about len is the one we prefer.

     (defthm equal-len-n
       (implies (syntaxp (quotep n))
                (equal (equal (len x) n)
                       (if (integerp n)
                           (if (< n 0)
                               nil
                             (if (equal n 0)
                                 (atom x)
                               (and (consp x)
                                    (equal (len (cdr x)) (- n 1)))))
                         nil))))

This lemma will simplify any equality in which a len expression is
equated to any explicitly given constant *n*, e.g., 3, reducing the
equation to a conjunction of consp terms about the first *n* cdrs.

If the above lemma is available then ACL2 immediately proves

     (defthm reset-counters-is-constant
       (implies (countersp x)
                (equal (reset-counters x)
                       '(0 0 nil))))

The point is presumably well made: proving theorems about
single-threaded object accessors and updaters is no different than
proving theorems about other recursively defined functions on lists.

As we have seen, operations on stobjs turn into definitions involving
nth and update-nth in the logic.  Here are two lemmas that are useful
for simplifying terms involving nth and update-nth, which are therefore
useful in reasoning about single-threaded objects.

     (defthm update-nth-update-nth-same
       (implies (equal (nfix i1) (nfix i2))
                (equal (update-nth i1 v1 (update-nth i2 v2 l))
                       (update-nth i1 v1 l))))

     (defthm update-nth-update-nth-diff
       (implies (not (equal (nfix i1) (nfix i2)))
                (equal (update-nth i1 v1 (update-nth i2 v2 l))
                       (update-nth i2 v2 (update-nth i1 v1 l))))
       :rule-classes ((:rewrite :loop-stopper ((i1 i2)))))

These lemmas are due to Matt Wilding.  See NU-REWRITER for a
discussion of the efficient simplification of terms of the form (nth n
(update-nth key val lst)), which can be critical in settings involving
sequential bindings that commonly arise in operations involving stobjs.

We now recommend that you see STOBJ-EXAMPLE-2.

STOBJ-EXAMPLE-2    an example of the use of arrays in single-threaded objects

The following event

     (defstobj ms
       (pcn  :type integer                  :initially 0)
       (mem  :type (array integer (100000)) :initially -1)
       (code :type t                        :initially nil))

introduces a single-threaded object named ms (which stands for "machine
state").  The object has three fields, a pcn or program counter, a mem
or memory, and a code field.

The mem field is occupied by an object initially of type (array integer
(100000)).  Logically speaking, this is a list of length 100000, each
element of which is an integer.  But in the underlying implementation of
the ms object, this field is occupied by a raw Lisp array, initially of
size 100000.

You might expect the above defstobj to define the accessor function mem
and the updater update-mem.  *That does not happen!*.

The above event defines the accessor function memi and the updater
update-memi.  These functions do not access/update the mem field of the
ms object; they access/update the individual elements of the array in
that field.

In particular, the logical definitions of the two functions are:

     (defun memi (i ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms)))))
       (nth i (nth 1 ms)))

     (defun update-memi (i v ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms))
                            (integerp v))))
       (update-nth-array 1 i v ms))

For example, to access the 511th (0-based) memory location of the
current ms you could evaluate:

     ACL2 !>(memi 511 ms)
     -1

The answer is -1 initially, because that is the above-specified initial
value of the elements of the mem array.

To set that element you could do

     ACL2 !>(update-memi 511 777 ms)
     <ms>
     ACL2 !>(memi 511 ms)
     777

The raw Lisp implementing these two functions is shown below.

     (defun memi (i ms)
       (declare (type (integer 0 268435455) i))
       (the integer
            (aref (the (simple-array integer (*))
                       (svref ms 1))
                  (the (integer 0 268435455) i))))

     (defun update-memi (i v ms)
       (declare (type (integer 0 268435455) i)
                (type integer v))
       (progn
        (setf (aref (the (simple-array integer (*))
                         (svref ms 1))
                    (the (integer 0 268435455) i))
              (the integer v))
        ms))

If you want to see the raw Lisp supporting a defstobj, execute the
defstobj and then evaluate the ACL2 form (nth 4 (global-val
'cltl-command (w state))).

To continue the stobj tour, see STOBJ-EXAMPLE-3.