SET-MEASURE-FUNCTION

Major Section:  EVENTS

Examples:
(set-measure-function nqthm::count)

General Form:
(set-measure-function name)

This event sets the default measure function to name. Subsequently, if a recursively defined function is submitted to defun with no explicitly given :measure argument, defun ``guesses'' the measure (name var), where name is the then current default measure function and var is the first formal found to be tested along every branch and changed in every recursive call.

SET-STATE-OK

Major Section:  EVENTS

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

Because the variable symbol STATE denotes the ``current ACL2 state,'' ACL2 treats the symbol very restrictively when it occurs as a formal parameter of a defined function. The novice user, who is unlikely to be aware of the special status of that symbol, is likely to be confused when error messages about STATE are printed in response to the innocent choice of that symbol as a formal variable. Therefore the top-level ACL2 loop can operate in a mode in which STATE is simply disallowed as a formal parameter.

For a discussion of STATE, See state. Roughly speaking, at the top-level, the ``current ACL2 state'' is denoted by the variable symbol STATE. Only the current state may be passed into a function expecting a state as an argument. Furthermore, the name of the formal parameter into which the current state is passed must be STATE and nothing but the current state may be passed into a formal of that name. Therefore, only certain access and change functions can use that formal -- namely with a STATE formal -- and if any such function produces a new state it becomes the ``current state'' and must be passed along in the STATE position thereafter. Thus, ACL2 requires that the state be single-threaded. This, in turn, allows us to represent only one state at a time and to produce new states from it destructively in a von Neumaneque fashion. The syntactic restrictions on the variable STATE are enforced by the translate mechanism (see trans and see term) when terms are read.

To prevent the novice user from seeing messages prohibiting certain uses of the variable symbol STATE ACL2 has a mode in which it simply disallows the use of that symbol as a formal parameter. Use of the symbol causes a simple error message. The system is initially in that mode.

To get out of that mode, execute:

:set-state-ok t

To enter the mode in which use of state is prohibited as a formal parameter, do:

:set-state-ok nil

The mode is stored in the defaults table, See acl2-defaults-table. Thus, the mode may be set locally in books.

SET-VERIFY-GUARDS-EAGERNESS

Major Section:  EVENTS

Example Forms:                        try guard verification?
(set-verify-guards-eagerness 0) ; no, unless :verify-guards t
(set-verify-guards-eagerness 1) ; yes if a :guard is supplied
(set-verify-guards-eagerness 2) ; yes, unless :verify-guards nil

General Form:
(set-verify-guards-eagerness n)

(table acl2-defaults-table :verify-guards-eagerness term).

Set-verify-guards-eagerness may be thought of as an event that merely sets a flag to 0, 1, or 2. The flag is used by certain defun events to determine whether guard verification is tried. The flag is irrelevant to those defun events in :program mode and to those defun events in which an explicit :verify-guards setting is provided among the xargs. In the former case, guard verification is not done because it can only be done when logical functions are being defined. In the latter case, the explicit :verify-guards setting determines whether guard verification is tried. So consider a :logic mode defun in which no :verify-guards setting is provided. Is guard verification tried? The answer depends on the eagerness setting as follows. If the eagerness is 0, guard verification is not tried. If the eagerness is 1, it is tried iff a :guard is explicitly provided in the defun. If the eagerness is 2, guard verification is tried.

The default behavior of the system is as though the :verify-guards-eagerness is 1.

SET-WELL-FOUNDED-RELATION

Major Section:  EVENTS

Examples:
(set-well-founded-relation lex2)

General Form:
(set-well-founded-relation rel)

This event sets the default well-founded relation to be that imposed on mp-measures by the relation rel. Subsequently, if a recursively defined function is submitted to defun with no explicitly given :well-founded-relation argument, defun uses the default relation, rel, and the associated domain predicate mp used in its well-foundedness theorem. That is, the termination conditions generated will require proving that the measure used by the defun is an mp-measure and that in every recursive call the measure of the arguments decreases according to rel.

TABLE

Major Section:  EVENTS

Examples:
(table tests 1 '(...))               ; set contents of tests[1] to '(...)
(table tests 25)                     ; get contents of tests[25]
(table tests)                        ; return table tests as an alist
(table tests nil nil :clear)         ; clear table tests
(table tests nil (foo 7) :clear)     ; set table tests to (foo 7)
(table tests nil nil :guard)         ; fetch the table guard
(table tests nil nil :guard term)    ; set the table guard

General Form:
(table table-name key-term value-term op term)

The ACL2 system provides ``tables'' by which the user can associate one object with another. Tables are in essence just conventional association lists -- lists of pairs -- but the ACL2 environment provides a means of storing these lists in the ``ACL2 world'' of the current state. The ACL2 user could accomplish the same ends by using ACL2 ``global variables;'' however, limitations on global variable names are imposed to insure ACL2's soundness. By convention, no table is important to ACL2's soundness, even though some features of the system use tables, and the user is invited to make free use of tables. Because tables are stored in the ACL2 world they are restored by include-book and undone by :ubt. many users of Nqthm requested a facility by which user data could be saved in Nqthm ``lib files'' and tables are ACL2's answer to that request.

Abstractly, each table is an association list mapping ``keys'' to ``values.'' In addition, each table has a ``:guard,'' which is a term that must be true of any key and value used. By setting the :guard on a table you may enforce an invariant on the objects in the table, e.g., that all keys are positive integers and all values are symbols. Each table has a ``name,'' which must be a symbol. Given a table name, there are six operations one might perform on the table.

:put -- associate a value with a key (possibly changing the value currently associated with that key).

:get -- retrieve the value associated with a key (or nil if no value has been associated with that key).

:alist -- return an alist showing all keys and non-nil values in the table.

:clear -- clear the table (so that every value is nil), or if val is supplied then set table to that value (which must be an alist).

:guard -- fetch or set the :guard of the table.

When the operations above suggest that the table or its :guard are modified, what is actually meant is that the current state is redefined so that in it, the affected table name has the appropriate properties. in such cases, the table form is an event.

Table forms are commonly typed by the user while interacting with the system. :Put and :get forms are especially common. Therefore, we have adopted a positional syntax that is intended to be convenient for most applications. Essentially, some operations admit a ``short form'' of invocation.

(table name key-term value-term :put)   ; long form
(table name key-term value-term)        ; short form

(table name key-term nil :get)          ; long form
(table name key-term)                   ; short form

(table name nil nil :alist)             ; long form
(table name)                            ; short form

(table name nil val :clear)

(table name nil nil :guard)

(table name nil nil :guard term)

Note that it is not allowed to change the :guard on a table once it has been explicitly set. Before the :guard is explicitly set, it is effectively just t. After it is set it can be changed only by undoing the event that set it. The purpose of this restriction is to prevent the user from changing the :guards on tables provided by other people or the system.

The intuition behind the :guard mechanism on tables is to enforce invariants on the keys and values in a table, so that the values, say, can be used without run-time checking. But if the :guard of a table is sensitive to the ACL2 world, it may be possible to cause some value in the table to cease satisfying the :guard without doing any operations on the table. Consider for example the :guard ``no value in this table is the name of an event.'' As described, that is enforced each time a value is stored. Thus, 'bang can be :put in the table provided there is no event named bang. But once it is in the table, there is nothing to prevent the user from defining bang as a function, causing the table to contain a value that could not be :put there anymore. Observe that not all state-sensitive :guards suffer this problem. The :guard ``every value is an event name'' remains invariant, courtesy of the fact that undoing back through an event name in the table would necessarily undo the :put of the name into the table.

Table was designed primarily for convenient top-level use. Tables are not especially efficient. Each table is represented by an alist stored on the property list of the table name. :Get is just a getprop and assoc-equal. :Put does a getprop to the get the table alist, a put-assoc-equal to record the new association, and a putprop to store the new table alist -- plus the overhead associated with :guards and undoable events. Note that there are never duplicate keys in the resulting alist; in particular, when the operation :clear is used to install new alist, duplicate keys are removed from that alist.

A table name may be any symbol whatsoever. Symbols already in use as function or theorem names, for example, may be used as table names. Symbols in use only as table names may be defined with defun, etc. Because there are no restrictions on the user's choice of table names, table names are not included among the logical names. Thus, :pe name will never display a table event (for a logical name other than :here). Either :pe name will display a ``normal'' event such as (defun name ...) or (defthm name ...) or else :pe name will cause an error indicating that name is not a logical name. This happens even if name is in use as a table name. Similarly, we do not permit table names to have documentation strings, since the same name might already have a documentation string. If you want to associate a documentation string with a table name that is being used no other way, define the name as a label and use the :doc feature of deflabel (see deflabel); also see defdoc.

TERM-TABLE

Major Section:  EVENTS

Example:
(table term-table t '((binary-+ x y) '3 'nil (car x)))

See table for a general discussion of tables and the table event used to manipulate tables.

The ``term-table'' is used at the time a meta rule is checked for syntactic correctness. Each proposed metafunction is run on each term in this table, and the result in each case is checked to make sure that it is a termp in the current world. In each case where this test fails, a warning is printed.

Whenever a metafunction is run in support of the application of a meta rule, the result must be a term in the current world. When the result is not a term, a hard error arises. The term-table is simply a means for providing feedback to the user at the time a meta rule is submitted, warning of the definite possibility that such a hard error will occur at some point in the future.

The key used in term-table is arbitrary. The top-most value is always the one that is used; it is the entire list of terms to be considered. Each must be a termp in the current ACL2 world.

THEORY-INVARIANT

Major Section:  EVENTS

Example:
(theory-invariant (not (and (member-equal '(:rewrite left-to-right)
                                           theory)
                            (member-equal '(:rewrite right-to-left)
                                          theory))))

General Forms:
(theory-invariant term)     ; conjoin a new invariant term
or
(theory-invariant term key) ; change an existing invariant term

The theory invariant mechanism is provided via a table (see table) named theory-invariant-table. In fact, the theory-invariant ``event'' is just a macro that expands into a use of the table event. More general access to the theory-invariant table is provided by table itself. For example, the table can be inspected or cleared (setting the invariant to t) with table.

Theory-invariant-table maps arbitrary keys to terms mentioning, at most, the variables theory and world. Every time an alleged theory expression is evaluated, e.g., in the in-theory event or :in-theory hint, each of the terms in theory-invariant-table is evaluated with theory bound to the runic theory (see theories) obtained from the theory expression and world bound to the current ACL2 world (see world). If the result is nil, a warning message is printed. Thus, the table can be thought of as a list of conjuncts. Each term in the table has a ``name,'' which is just the key under which the term is stored. When a theory violates the restrictions specified by some term, both the name and the term are printed. By calling theory-invariant with a new term but the same name, you can overwrite that conjunct of the theory invariant.

Theory invariants are particularly useful in the context of large rule sets intended for re-use. Such sets often contain conflicting rules, e.g., rules that are to be enabled when certain function symbols are disabled, rules that rewrite in opposite directions and thus loop if simultaneously enabled, groups of rules which should be enabled in concert, etc. The developer of such rule sets understands these restrictions and probably documents them. The theory invariant mechanism allows the developer to codify his restrictions so that when they are violated the user is warned.

Since theory invariants are arbitrary terms, macros may be used to express commonly used restrictions. Because theory invariants are a new idea in ACL2, we have only defined one such macro for illustrative purposes. Executing the event

(theory-invariant (incompatible (:rewrite left-to-right)
                                (:rewrite right-to-left)))

Note: If the table event is used directly to :put a term into the theory invariant table, be aware that the term must be in translated form. This is enforced by the value invariant for theory-invariant-table. But the upshot of this is that you will be unable to use macros in theory invariants stored directly with the :put table event.

VERIFY-GUARDS

Major Section:  EVENTS

Examples:
(verify-guards flatten)
(verify-guards flatten
               :hints (("Goal" :use (:instance assoc-of-app)))
               :otf-flg t
               :doc "string")

General Form:
(verify-guards name
        :hints        hints
        :otf-flg      otf-flg
        :doc          doc-string)

If name is one of several functions in a mutually recursive clique, verify-guards will attempt to verify the guards of all of the functions.

If name is a theorem or axiom name, verify-guards verifies the guards of the associated formula. When a theorem has had its guards verified then you know that the theorem will evaluate to non-nil in all Common Lisps, without causing a runtime error (other than possibly a resource error). In particular, you know that the theorem's validity does not depend upon ACL2's arbitrary completion of the domains of partial Common Lisp functions.

For example, if app is defined as

(defun app (x y)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      y
      (cons (car x) (app (cdr x) y))))

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

(equal (app (app 1 2) 3) (app 1 (app 2 3)))

It happens because the theorem exploits the fact that ACL2 has completed the domains of the partially defined Common Lisp functions like car and cdr, defining them to be nil on all non-conses. The formula above violates the guards on app. It is therefore ``unreasonable'' to expect it to be valid in Common Lisp.

But the following formula is valid in Common Lisp:

(if (and (true-listp a)
         (true-listp b))
    (equal (app (app a b) c) (app a (app b c)))
    t)

(defthm guarded-assoc-of-app
  (if (and (true-listp a)
           (true-listp b))
      (equal (app (app a b) c) (app a (app b c)))
      t))

One last complication: The careful reader might have thought we could state guarded-assoc-of-app as

(implies (and (true-listp a)
              (true-listp b))
         (equal (app (app a b) c)
                (app a (app b c))))

Recall however that verify-guards is almost always used to verify the guards on a function definition rather than a theorem. We now return to that discussion.

Because name is not uniquely associated with the verify-guards event (it necessarily names a previously defined function) the documentation string, doc-string, is not stored in the documentation data base. Thus, we actually prohibit doc-string from having the form of an ACL2 documentation string; see doc-string.

Verify-guards must often be used when the value of a recursive call of a defined function is given as an argument to a subroutine that is guarded. An example of such a situation is given below. Suppose app (read ``append'') has a guard requiring its first argument to be a true-listp. Consider

(defun rev (x)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) nil)
        (t (app (rev (cdr x)) (list (car x))))))

Therefore, we might break the admission of rev into three steps: define rev without addressing its guard verification, prove some general properties about rev, and then verify the guards. This can be done as follows:

(defun rev (x)
  (declare (xargs :guard (true-listp x)
                  :verify-guards nil))    ; Note this additional xarg.
  (cond ((endp x) nil)
        (t (app (rev (cdr x)) (list (car x))))))


(defthm true-listp-rev
  (implies (true-listp x2)
           (true-listp (rev x2))))


(verify-guards rev)

VERIFY-TERMINATION

Major Section:  EVENTS

Examples:
(verify-termination fact)
(verify-termination 
 fact
 (declare (xargs :guard (and (integerp x) (>= x 0)))))

General Forms:
(verify-termination fn dcl ... dcl)
(verify-termination (fn1 dcl ... dcl)
                    (fn2 dcl ... dcl)
                    ...)

(verify-termination (fn dcl ... dcl))

Verify-termination attempts to establish the admissibility of the fni. Verify-termination retrieves their definitions, creates modified definitions using the dcls supplied above, and resubmits these definitions. You could avoid using verify-termination by typing the new definitions yourself. So in that sense, verify-termination adds no new functionality. But if you have prototyped your system in :program mode and tested it, you can use verify-termination to resubmit your definitions and change their defun-modes to :logic, addings hints without having to retype or recopy the code. You can also add or modify guards at this time.

The defun command executed by verify-termination is obtained by retrieving the defun (or mutual-recursion) command that introduced the clique in question and then possibly modifying each definition as follows. Consider a function, fn, in the clique. If fn is not among the fni above, its definition is left unmodified. Otherwise, fn is some fni and we modify its definition by inserting into it the corresponding dcls listed with fni in the arguments to verify-termination. In addition, we throw out from the old declarations in fn the :mode specification and anything that is specified in the new dcls.

For example, suppose that fact was introduced with:

(defun fact (n)
  (declare (type integer n)
           (xargs :mode :program))
  (if (zp n) 1 (* n (fact (1- n))))).

(defun fact (n)
  (declare (type integer n))
  (if (zp n) 1 (* n (fact (1- n))))).

(verify-termination
 fact 
 (declare (xargs :guard (and (integerp n) (<= 0 n)))))

(defun fact (n)
  (declare (xargs :guard (and (integerp n) (<= 0 n))))
  (if (zp n) 1 (* n (fact (1- n))))).