ADD-MACRO-ALIAS

associate a function name with a macro name
Major Section:  EVENTS

Example:
(add-macro-alias append binary-append)
This example associates the function symbol binary-append with the macro name append. As a result, the name append may be used as a runic designator (see theories) by the various theory functions. See macro-aliases-table for more details.

General Form:
(add-macro-alias macro-name function-name)
This is a convenient way to add an entry to macro-aliases-table. See macro-aliases-table and also see remove-macro-alias.













































































DEFABBREV

a convenient form of macro definition for simple expansions
Major Section:  EVENTS

Examples:
(defabbrev snoc (x y) (append y (list x)))
(defabbrev sq (x) (* x x))

General Form: (defabbrev name (v1 ... vn) body)

where name is a new function symbol, the vi are distinct variable symbols, and body is a term.

Roughly speaking, the defabbrev event is akin to defining f so that (f v1 ... vn) = body. But rather than do this by adding a new axiom, defabbrev defines f to be a macro so that (f a1 ... an) expands to body, with the ``formals,'' vi, replaced by the ``actuals,'' ai.

For example, if snoc is defined as shown in the first example above, then (snoc (+ i j) temp) is just an abbreviation for

(append temp (list (+ i j))).
In order to generate efficiently executable Lisp code, the macro that defabbrev introduces uses a let to bind the ``formals'' to the ``actuals.'' Consider the second example above. Logically speaking, (sq (ack i j)) is an abbreviation for (* (ack i j) (ack i j)). But in fact the macro for sq introduced by defabbrev actually arranges for (sq (ack i j)) to expand to:
(let ((x (ack i j)))
  (* x x))
which executes more efficiently than (* (ack i j) (ack i j)).

In the theorem prover, the let above expands to

((lambda (x) (* x x)) (ack i j))
and thence to (* (ack i j) (ack i j)).













































































DEFAXIOM

add an axiom
Major Section:  EVENTS

WARNING: We strongly recommend that you not add axioms. If at all possible you should use defun or mutual-recursion to define new concepts recursively or use encapsulate to constrain them constructively. Adding new axioms frequently renders the logic inconsistent.

Example:
(defaxiom sbar (equal t nil)
          :rule-classes nil
          :doc ":Doc-Section ...")

General Form: (defaxiom name term :rule-classes rule-classes :doc doc-string)

where name is a new symbolic name (see name), term is a term intended to be a new axiom, and rule-classes and doc-string are as described in the corresponding documentation topics . The two keyword arguments are optional. If :rule-classes is not supplied, the list (:rewrite) is used; if you wish the axiom to generate no rules, specify :rule-classes nil.













































































DEFCHOOSE

define a Skolem (witnessing) function
Major Section:  EVENTS

Examples:
(defchoose choose-x-for-p-and-q (x) (y z)
  (and (p x y z)
       (q x y z)))

(defchoose choose-x-for-p-and-q x (y z) ; equivalent to the above (and (p x y z) (q x y z)))

(defchoose choose-x-and-y-for-p-and-q (x y) (z) (and (p x y z) (q x y z)))

General Form: (defchoose fn (bound-var1 ... bound-varn) (free-var1 ... free-vark) doc-string ; optional body),

where fn is the symbol you wish to define and is a new symbolic name (see name), (bound-var1 ... bound-varn) is a list of distinct `bound' variables (see below), (free-var1 ... free-vark) is the list of formal parameters of fn and is disjoint from the bound variables, and body is a term. The use of lambda-list keywords (such as &optional) is not allowed. The documentation string, doc-string, is optional; for a description of its form, see doc-string.

In the most common case, where there is only one bound variable, it is permissible to omit the enclosing parentheses on that variable. The effect is the same whether or not those parentheses are omitted. We describe this case first, where there is only one bound variable, and address the other case at the end.

The effect of the form

(defchoose fn bound-var (free-var1 ... free-vark)
  body)
is to introduce a new function symbol, fn, with formal parameters (free-var1 ... free-vark), and the following axiom stating that fn picks a value of bound-var so that the body will be true, if such a value exists:
(implies body
         (let ((bound-var (fn free-var1 ... free-vark)))
           body))
This axiom is ``clearly'' conservative under the conditions expressed above: the function fn merely picks out a ``witnessing'' value of bound-var if there is one. The system in fact treats fn very much as though it were declared in the signature of an encapsulate event, with the axiom above as the only axiom exported.

If there is more than one bound variable, as in

(defchoose fn 
           (bound-var1 ... bound-varn)
           (free-var1 ... free-vark)
           body)
then fn returns n multiple values, and the defining axiom is expressed using mv-let (see mv-let) as follows:
(implies body
         (mv-let (bound-var1 ... bound-varn)
                 (fn free-var1 ... free-vark)
                 body))

Defchoose is only executed in defun-mode :logic; see defun-mode.

Also see defun-sk.

Comment for logicians: As we point out in the documentation for defun-sk, defchoose is ``appropriate,'' by which we mean that it is conservative, even in the presence of epsilon-0 induction. This fact is shown in a paper by ACL2 authors Kaufmann and Moore, entitled ``Structured Theory Development for a Mechanized Logic'' (to appear in the Journal of Automated Reasoning, 2000).













































































DEFCONG

prove that one equivalence relation preserves another in a given argument position of a given function
Major Section:  EVENTS

Example:
(defcong set-equal iff (memb x y) 2)

is an abbreviation for (defthm set-equal-implies-iff-memb-2 (implies (set-equal y y-equiv) (iff (memb x y) (memb x y-equiv))) :rule-classes (:congruence))

See congruence and also see equivalence.

General Form:
(defcong equiv1 equiv2 term k
  :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, term is a call of a function fn on the correct number of distinct variable arguments (fn x1 ... xn), k is a positive integer less than or equal to the arity of fn, and other arguments are as specified in the documentation for defthm. The defcong macro expands into a call of defthm. The name of the defthm event is equiv1-implies-equiv2-fn-k unless an :event-name keyword argument is supplied for the name. The term of the theorem is
(implies (equiv1 xk yk)
         (equiv2 (fn x1... xk ...xn)
                 (fn x1... yk ...xn))).
The rule-class :congruence 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 keyword arguments above.













































































DEFCONST

define a constant
Major Section:  EVENTS

Examples:
(defconst *digits* '(0 1 2 3 4 5 6 7 8 9))
(defconst *n-digits* (the unsigned-byte (length *digits*)))

General Form: (defconst name term doc-string)

where name is a symbol beginning and ending with the character *, term is a variable-free term that is evaluated to determine the value of the constant, and doc-string is an optional documentation string (see doc-string).

When a constant symbol is used as a term, ACL2 replaces it by its value; see term.

It may be of interest to note that defconst is implemented at the lisp level using defparameter, as opposed to defconstant. (Implementation note: this is important for proper support of undoing and redefinition.)













































































DEFDOC

add a documentation topic
Major Section:  EVENTS

Examples:
(defdoc interp-section
   ":Doc-Section ...")

General Form: (defdoc name doc-string)

where name is a symbol or string to be documented and doc-string is a documentation string (see doc-string). This event adds the documentation string for symbol name to the :doc data base. It may also be used to change the documentation for name if name already has documentation. The difference between this event and deflabel is that, unlike deflabel (but like table), it does not mark the current history with the name. But like deflabel, defdoc events are never considered redundant (see redundant-events).

See deflabel for a means of attaching a documentation string to a name that marks the current history with that name. We now elaborate further on how defdoc may be useful in place of deflabel.

It is usually sufficient to use deflabel when you might be tempted to use defdoc. However, unlike deflabel, defdoc does not mark the current history with name. Thus, defdoc is useful for introducing the documentation for a defun or deftheory event, for example, several events before the function or theory is actually defined.

For example, suppose you want to define a theory (using deftheory). You need to prove the lemmas in that theory before executing the deftheory event. However, it is quite natural to define a :doc-section (see doc-string) whose name is the name of the theory to be defined, and put the documentation for that theory's lemmas into that :doc-section. Defdoc is ideal for this purpose, since it can be used to introduce the :doc-section, followed by the lemmas referring to that :doc-section, and finally concluded with a deftheory event of the same name. If deflabel were used instead of defdoc, for example, then the deftheory event would be disallowed because the name is already in use by the deflabel event.

We also imagine that some users will want to use defdoc to insert the documentation for a function under development. This defdoc event would be followed by definitions of all the subroutines of that function, followed in turn by the function definition itself.

Any time defdoc is used to attach documentation to an already-documented name, the name must not be attached to a new :doc-section. We make this requirement as a way of avoiding loops in the documentation tree. When documentation is redefined, a warning will be printed to the terminal.













































































DEFEQUIV

prove that a function is an equivalence relation
Major Section:  EVENTS

Example:
(defequiv set-equal)

is an abbreviation for (defthm set-equal-is-an-equivalence (and (booleanp (set-equal x y)) (set-equal x x) (implies (set-equal x y) (set-equal y x)) (implies (and (set-equal x y) (set-equal y z)) (set-equal x z))) :rule-classes (:equivalence))

See equivalence.

General Form:
(defequiv fn
  :rule-classes rule-classes
  :instructions instructions
  :hints hints
  :otf-flg otf-flg
  :event-name event-name
  :doc doc)
where fn is a function symbol of arity 2, event-name, if supplied, is a symbol, and all other arguments are as specified in the documentation for defthm. The defequiv macro expands into a call of defthm. The name of the defthm is fn-is-an-equivalence, unless event-name is supplied, in which case event-name is the name used. The term generated for the defthm event states that fn is Boolean, reflexive, symmetric, and transitive. The rule-class :equivalence 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.













































































DEFEVALUATOR

introduce an evaluator function
Major Section:  EVENTS

Example:
(defevaluator evl evl-list
  ((length x) (member x y)))
See meta.

General Form:
(defevaluator ev ev-list
   ((g1 x1 ... xn_1)
    ...
    (gk x1 ... xn_k))
where ev and ev-list are new function symbols and g1, ..., gk are old function symbols with the indicated number of formals, i.e., each gi has n_i formals.

This function provides a convenient way to constrain ev and ev-list to be mutually-recursive evaluator functions for the symbols g1, ..., gk. Roughly speaking, an evaluator function for a fixed, finite set of function symbols is a restriction of the universal evaluator to terms composed of variables, constants, lambda expressions, and applications of the given functions. However, evaluator functions are constrained rather than defined, so that the proof that a given metafunction is correct vis-a-vis a particular evaluator function can be lifted (by functional instantiation) to a proof that it is correct for any larger evaluator function. See meta for a discussion of metafunctions.

Defevaluator executes an encapsulate after generating the appropriate defun and defthm events. Perhaps the easiest way to understand what defevaluator does is to execute the keyword command

:trans1 (defevaluator evl evl-list ((length x) (member x y)))
and inspect the output.

Formally, ev is said to be an ``evaluator function for g1, ..., gk, with mutually-recursive counterpart ev-list'' iff ev and ev-list are constrained functions satisfying just the constraints discussed below.

Ev and ev-list must satisfy constraints (1)-(4) and (k):

(1) How to ev a variable symbol:
    (implies (symbolp x)
             (equal (ev x a) (cdr (assoc-eq x a))))

(2) How to ev a constant: (implies (and (consp x) (equal (car x) 'quote)) (equal (ev x a) (cadr x)))

(3) How to ev a lambda application: (implies (and (consp x) (consp (car x))) (equal (ev x a) (ev (caddar x) (pairlis$ (cadar x) (ev-list (cdr x) a)))))

(4) How to ev an argument list: (implies (consp x-lst) (equal (ev-list x-lst a) (cons (ev (car x-lst) a) (ev-list (cdr x-lst) a)))) (implies (not (consp x-lst)) (equal (ev-list x-lst a) nil))

(k) For each i from 1 to k, how to ev an application of gi, where gi is a function symbol of n arguments: (implies (and (consp x) (equal (car x) 'gi)) (equal (ev x a) (gi (ev x1 a) ... (ev xn a)))), where xi is the (cad...dr x) expression equivalent to (nth i x).

Defevaluator defines suitable witnesses for ev and ev-list, proves the theorems about them, and constrains ev and ev-list appropriately. We expect defevaluator to work without assistance from you, though the proofs do take some time and generate a lot of output. The proofs are done in the context of a fixed theory, namely the result of applying union-theories to two lists: the function symbols supplied, and the value of the constant *defevaluator-form-base-theory*.













































































DEFLABEL

build a landmark and/or add a documentation topic
Major Section:  EVENTS

Examples:
(deflabel interp-section
   :doc
   ":Doc-Section ...")

General Form: (deflabel name :doc doc-string)

where name is a new symbolic name (see name) and doc-string is an optional documentation string (see doc-string). This event adds the documentation string for symbol name to the :doc data base. By virtue of the fact that deflabel is an event, it also marks the current history with the name. Thus, even undocumented labels are convenient as landmarks in a proof development. For example, you may wish to undo back through some label or compute a theory expression (see theories) in terms of some labels. Deflabel events are never considered redundant. See redundant-events.

See defdoc for a means of attaching a documentation string to a name without marking the current history with that name.













































































DEFMACRO

define a macro
Major Section:  EVENTS

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
Major Section:  EVENTS

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

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

where "name" is a (case-sensitive) string that names the package to be created, term is a variable-free expression that evaluates to a list of symbols (no two of which 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.

defpkg forms can be entered at the top-level of the ACL2 command loop. They should occur in a file only if the file is not to be compiled and contains nothing besides defpkg and in-package forms.

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 imports list 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 imports. That is, it is permissible to execute ``redundant'' defpkg commands. The redundancy test is based on the values of the two import forms, not on the forms themselves.













































































DEFREFINEMENT

prove that equiv1 refines equiv2
Major Section:  EVENTS

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
Major Section:  EVENTS

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

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

where name is a new symbol, each fieldi is a symbol, each typei is either a type-spec or (ARRAY type-spec (max)), and each vali is an object satisfying typei. 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. 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.

The effect of this event is to introduce a new single-threaded object (i.e., a ``stobj''), named name, and the associated recognizers, accessors, and updaters.

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 a list of length max containing the initial 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 stobj in the underlying Lisp may be quite different, as described in 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, accessing and updating the fields of the stobj.

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 form 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 max items, each of which satisfies the indicated type-spec. Max must be a positive 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 16 integers, each of which 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.

Note also that ACL2's max must be less than (2^28)-1. Each Common Lisp implementation is allowed to set its own upper bound on array size. That upper bound is given by the Common Lisp ``constant'' array-dimension-limit, which varies from Lisp to Lisp. The standard requires that array-dimension-limit be a fixnum larger than 1023. When ACL2 was built we checked that the array-dimension-limit in this Lisp is at least (2^28)-1. But there are Lisps in which the fixnum limit is (2^28)-1. In an effort to ensure that ACL2 is portable between Lisps, we have limited our max. If this limitation prevents you from using ACL2, please notify the implementors and we will modify our treatment of max. (Even as it stands, some ACL2 hosts can handle larger problems than others, simply because of memory restrictions. So there is precedent for being more relaxed here.)

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.

The Default Function Names

To recap, in

(defstobj name 
          (field1 :type type1 :initially val1)
          ...
          (fieldk :type typek :initially valk)                
          :renaming alist
          :doc doc-string)
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 three functions -- the recognizer, accessor, and updater -- for each field 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)

If the field is an array field, an auxiliary function, used in the definition of the field recognizer, is introduced,

                 non-array field        array field
aux recognizer                           (cP1 x)

Finally, a recognizer for the entire single-threaded object is introduced. If the single-threaded object is named name, then

top recognizer     (nameP x)             (nameP x)

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 three integers, each between 0 and 9, inclusively. Initially, each of the elements of the A field is 9.

This event introduces the following sequence of definitions:

(DEFUN XP (X) ...)               ; recognizer for X field
(DEFUN AP1 (X N) ...)            ; aux fn for recogizer of A field
(DEFUN AP (X) ...)               ; recognizer of A field
(DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
(DEFUN X ($S) ...)               ; accessor for X field
(DEFUN UPDATE-X (V $S) ...)      ; updater for X 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 ((AP1 AP-HELPER) (X XACCESSOR)))
introduces the following definitions
(DEFUN XP (X) ...)               ; recognizer for X field
(DEFUN AP-HELPER (X N) ...)      ; aux fn for recogizer of A field
(DEFUN AP (X) ...)               ; recognizer of A field
(DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
(DEFUN XACCESSOR ($S) ...)       ; accessor for X field
(DEFUN UPDATE-X (V $S) ...)      ; updater for X 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.

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

To see an s-expression indicating what the raw Lisp implementation of the event is, evaluate the form

(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 and renaming alist are identical to a previously executed defstobj.