TERM

Parent topic:  MISCELLANEOUS
Home

Examples of Terms:
(cond ((caar x) (cons t x)) (t 0))   ; an untranslated term


(if (car (car x)) (cons 't x) '0)    ; a translated term


(car (cons x y) 'nil v)              ; a pseudo-term

In traditional first-order predicate calculus a ``term'' is a syntactic entity denoting some object in the universe of individuals. Often, for example, the syntactic characterization of a term is that it is either a variable symbol or the application of a function symbol to the appropriate number of argument terms. Traditionally, ``atomic formulas'' are built from terms with predicate symbols such as ``equal'' and ``member;'' ``formulas'' are then built from atomic formulas with propositional ``operators'' like ``not,'' ``and,'' and ``implies.'' Theorems are formulas. Theorems are ``valid'' in the sense that the value of a theorem is true, in any model of the axioms and under all possible assignments of individuals to variables.

However, in ACL2, terms are used in place of both atomic formulas and formulas. ACL2 does not have predicate symbols or propositional operators as distinguished syntactic entities. The ACL2 universe of individuals includes a ``true'' object (denoted by t) and a ``false'' object (denoted by nil), predicates and propositional operators are functions that return these objects. Theorems in ACL2 are terms and the ``validity'' of a term means that, under no assignment to the variables does the term evaluate to nil.

We use the word ``term'' in ACL2 in three distinct senses. We will speak of ``translated'' terms, ``untranslated'' terms, and ``pseudo-'' terms.

Translated Terms: The Strict Sense and Internal Form

In its most strict sense, a ``term'' is either a legal variable symbol, a quoted constant, or the application of an n-ary function symbol or closed lambda expression to a true list of n terms.

The legal variable symbols are symbols other than t or nil which are not in the keyword package, do not start with ampersand, do not start and end with asterisks, and if in the main Lisp package, do not violate an appropriate restriction (see name).

Quoted constants are expressions of the form (quote x), where x is any ACL2 object. Such expressions may also be written 'x.

Closed lambda expressions are expressions of the form (lambda (v1 ... vn) body) where the vi are distinct legal variable symbols, body is a term, and the only free variables in body are among the vi.

The function termp, which takes two arguments, an alleged term x and a logical world w (see world), recognizes terms of a given extension of the logic. Termp is defined in :program mode. Its definition may be inspected with :pe termp for a complete specification of what we mean by ``term'' in the most strict sense. Most ACL2 term-processing functions deal with terms in this strict sense and use termp as a guard. That is, the ``internal form'' of a term satisfies termp, the strict sense of the word ``term.''

Untranslated Terms: What the User Types

While terms in the strict sense are easy to explore (because their structure is so regular and simple) they can be cumbersome to type. Thus, ACL2 supports a more sugary syntax that includes uses of macros and constant symbols. Very roughly speaking, macros are functions that produce terms as their results. Constants are symbols that are associated with quoted objects. Terms in this sugary syntax are ``translated'' to terms in the strict sense; the sugary syntax is more often called ``untranslated.'' Roughly speaking, translation just implements macroexpansion, the replacement of constant symbols by their quoted values, and the checking of all the rules governing the strict sense of ``term.''

More precisely, macro symbols are as described in the documentation for defmacro. A macro, mac, can be thought of as a function, mac-fn, from ACL2 objects to an ACL2 object to be treated as an untranslated term. For example, caar is defined as a macro symbol; the associated macro function maps the object x into the object (car (car x)). A macro form is a ``call'' of a macro symbol, i.e., a list whose car is the macro symbol and whose cdr is an arbitrary true list of objects, used as a term. Macroexpansion is the process of replacing in an untranslated term every occurrence of a macro form by the result of applying the macro function to the appropriate arguments. The ``appropriate'' arguments are determined by the exact form of the definition of the macro; macros support positional, keyword, optional and other kinds of arguments. See defmacro.

In addition to macroexpansion and constant symbol dereferencing, translation implements the mapping of let and let* forms into applications of lambda expressions and closes lambda expressions containing free variables. Thus, the translation of

(let ((x (1+ i))) (cons x k))

((lambda (x) (cons x k)) (1+ i))

((lambda (x k) (cons x k)) (1+ i) k) .

When we say, of an event-level function such as defun or defthm, that some argument ``must be a term'' we mean an untranslated term. The event functions translate their term-like arguments.

To better understand the mapping between untranslated terms and translated terms it is convenient to use the keyword command :trans to see examples of translations. See trans and also see trans1.

Pseudo-Terms: A Common Guard for Metafunctions

Because termp is defined in :program mode, it cannot be used effectively in conjectures to be proved. Furthermore, from the perspective of merely guarding a term processing function, termp often checks more than is required. Finally, because termp requires the logical world as one of its arguments it is impossible to use termp as a guard in places where the logical world is not itself one of the arguments.

For these reasons we support the idea of ``pseudo-terms.'' A pseudo-term is either a symbol (but not necessarily one having the syntax of a legal variable symbol), a true list beginning with quote (but not necessarily well-formed), or the ``application of'' a symbol or pseudo lambda expression to a true list of pseudo-terms. A pseudo lambda expression is an expression of the form (lambda (v1 ... vn) body) where the vi are all symbols and body is a pseudo-term.

Pseudo-terms are recognized by the unary function pseudo-termp. If (termp x w) is true, then (pseudo-termp x) is true. However, if x fails to be a (strict) term it may nevertheless still be a pseudo-term. For example, (car a b) is not a term, because car is applied to the wrong number of arguments, but it is a pseudo-term.

The structures recognized by pseudo-termp can be recursively explored with the same simplicity that terms can be. In particular, if x is not a variablep or an fquotep, then (ffn-symb x) is the function (symbol or lambda expression) and (fargs x) is the list of argument pseudo-terms. A metafunction may use pseudo-termp as the guard.

TERM-ORDER

Parent topic:  MISCELLANEOUS
Home

ACL2 must occasionally choose which of two terms is syntactically smaller. The need for such a choice arises, for example, when using equality hypotheses in conjectures (the smaller term is substituted for the larger elsewhere in the formula), in stopping loops in permutative rewrite rules (see loop-stopper), and in choosing the order in which to try to cancel the addends in linear arithmetic inequalities. When this notion of syntactic size is needed, ACL2 uses ``term order.'' Popularly speaking, term order is just a lexicographic ordering on terms. But the situation is actually more complicated.

We define term order only with respect to terms in translated form. See trans.

Term1 comes before term2 in the term order iff

(a) the number of variable occurrences in term1 is less than that in term2, or

(b) the numbers of variable occurrences in the two terms are equal but the number of function applications in term1 is less than that in term2, or

(c) the numbers of variable occurrences in the two terms are equal, the numbers of functions applications in the two terms are equal, and term1 comes before term2 in a certain lexicographic ordering based their structure as Lisp objects.

By ``number of variable occurrences'' we do not mean ``number of distinct variables'' but ``number of times a variable symbol is mentioned.'' (cons x x) has two variable occurrences, not one. Thus, perhaps counterintuitively, a large term that contains only one variable occurrence, e.g., (standard-char-p (car (reverse x))) comes before (cons x x) in the term order.

Since constants contain no variable occurrences and non-constant expressions must contain at least one variable occurrence, constants come before non-constants in the term order, no matter how large the constants. For example, the list constant

'(monday tuesday wednesday thursday friday)

(+ x 3 (car (reverse klst)) (dx i j)) ,

(binary-+ x
          (binary-+ '3
                    (binary-+ (dx i j)
                              (car (reverse klst))))),

(binary-+ '3
          (binary-+ x
                    (binary-+ (car (reverse klst))
                              (dx i j))))

(+ 3 x (car (reverse klst)) (dx i j)).

The constant function z constructs 0. Positive integers are constructed from (z) by the successor function, s. Thus 2 is (s (s (z))) and contains three function applications. 100 contains one hundred and one applications. Negative integers are constructed from their positive counterparts by -. Thus, -2 is (- (s (s (z)))) and has four applications. Ratios are constructed by the dyadic function /. Thus, -1/2 is

(/ (- (s (z))) (s (s (z))))

(p (cs (#\a) (cs (#\b) (o))))

Two terms with the same numbers of variable occurrences and function applications are ordered by lexicographic means, based on their structures. In the lexicographic ordering, two atoms are ordered ``alphabetically'' as described below, an atom and a cons are ordered so that the atom comes first, and two conses are ordered so that the one with the recursively smaller car comes first, with the cdrs being compared only if the cars are equal. Thus, if two terms (member ...) and (reverse ...) contain the same numbers of variable occurrences and function applications, then the member term is first in the term order because member comes before reverse in the term order (which is here reduced to alphabetic ordering).

It remains only to define what we mean by the alphabetic ordering on Lisp atoms. Within a single type, numbers are compared arithmetically, characters are compared via their (char) codes, and strings and symbols are compared with the conventional alphabetic ordering on sequences of characters. Across types, numbers come before characters, characters before strings, and strings before symbols.

TYPE-SET

Parent topic:  MISCELLANEOUS
Home

To help you experiment with type-sets we briefly note the following utility functions.

(type-set-quote x) will return the type-set of the object x. For example, (type-set-quote "test") is 2048 and (type-set-quote '(a b c)) is 512.

(type-set 'term nil nil nil nil (ens state) (w state) nil) will return the type-set of term. For example,

(type-set '(integerp x) nil nil nil nil (ens state) (w state) nil)

(type-set-implied-by-term 'x nil 'term (ens state)(w state) nil) will return the type-set deduced for the variable symbol x assuming the translated term, term, true. The second result may be ignored in these experiments. For example,

(type-set-implied-by-term 'v nil '(integerp v)
                          (ens state) (w state) nil)

(convert-type-set-to-term 'x ts (ens state) (w state) nil) will return a term whose truth is equivalent to the assertion that the term x has type-set ts. The second result may be ignored in these experiments. For example

(convert-type-set-to-term 'v 523 (ens state) (w state) nil)

The ``actual primitive types'' of ACL2 are listed in *actual-primitive-types*. These primitive types include such types as *ts-zero*, *ts-positive-integer*, *ts-nil* and *ts-proper-consp*. Each actual primitive type denotes a set -- sometimes finite and sometimes not -- of ACL2 objects and these sets are pairwise disjoint. For example, *ts-zero* denotes the set containing 0 while *ts-positive-integer* denotes the set containing all of the positive integers.

The actual primitive types were chosen by us to make theorem proving convenient. Thus, for example, the actual primitive type *ts-nil* contains just nil so that we can encode the hypothesis ``x is nil'' by saying ``x has type *ts-nil*'' and the hypothesis ``x is non-nil'' by saying ``x has type complement of *ts-nil*.'' We similarly devote a primitive type to t, *ts-t*, and to a third type, *ts-non-t-non-nil-symbol*, to contain all the other ACL2 symbols.

Let *ts-other* denote the set of all Common Lisp objects other than those in the actual primitive types. Thus, *ts-other* includes such things as floating point numbers and CLTL array objects. The actual primitive types together with *ts-other* constitute what we call *universe*. Note that *universe* is a finite set containing one more object than there are actual primitive types; that is, here we are using *universe* to mean the finite set of primitive types, not the infinite set of all objects in all of those primitive types. *Universe* is a partitioning of the set of all Common Lisp objects: every object belongs to exactly one of the sets in *universe*.

Abstractly, a ``type-set'' is a subset of *universe*. To say that a term, x, ``has type-set ts'' means that under all possible assignments to the variables in x, the value of x is a member of some member of ts. Thus, (cons x y) has type-set {*ts-proper-cons* *ts-improper-cons*}. A term can have more than one type-set. For example, (cons x y) also has the type-set {*ts-proper-cons* *ts-improper-cons* *ts-nil*}. Extraneous types can be added to a type-set without invalidating the claim that a term ``has'' that type-set. Generally we are interested in the smallest type-set a term has, but because the entire theorem-proving problem for ACL2 can be encoded as a type-set question, namely, ``Does p have type-set complement of *ts-nil*?,'' finding the smallest type-set for a term is an undecidable problem. When we speak informally of ``the'' type-set we generally mean ``the type-set found by our heuristics'' or ``the type-set assumed in the current context.''

Note that if a type-set, ts, does not contain *ts-other* as an element then it is just a subset of the actual primitive types. If it does contain *ts-other* it can be obtained by subtracting from *universe* the complement of ts. Thus, every type-set can be written as a (possibly complemented) subset of the actual primitive types.

By assigning a unique bit position to each actual primitive type we can encode every subset, s, of the actual primitive types by the nonnegative integer whose ith bit is on precisely if s contains the ith actual primitive type. The type-sets written as the complement of s are encoded as the twos-complement of the encoding of s. Those type-sets are thus negative integers. The bit positions assigned to the actual primitive types are enumerated from 0 in the same order as the types are listed in *actual-primitive-types*. At the concrete level, a type-set is an integer between *min-type-set* and *max-type-set*, inclusive.

For example, *ts-nil* has bit position 6. The type-set containing just *ts-nil* is thus represented by 64. If a term has type-set 64 then the term is always equal to nil. The type-set containing everything but *ts-nil* is the twos-complement of 64, which is -65. If a term has type-set -65, it is never equal to nil. By ``always'' and ``never'' we mean under all, or under no, assignments to the variables, respectively.

Here is a more complicated example. Let s be the type-set containing all of the symbols and the natural numbers. The relevant actual primitive types, their bit positions and their encodings are:

actual primitive type       bit    value


*ts-zero*                    0       1
*ts-positive-integer*        1       2
*ts-nil*                     6      64
*ts-t*                       7     128
*ts-non-t-non-nil-symbol*    8     256

WHY-BRR

Parent topic:  MISCELLANEOUS
Home

Why isn't brr mode automatically disabled when there are no monitored runes? The reason is that the list of monitored runes is kept in a wormhole state.

See wormhole for more information on wormholes in general. But the fundamental property of the wormhole function is that it is a logical no-op, a constant function that does not take state as an argument. When entering a wormhole, arbitrary information can be passed in (including the external state). That information is used to construct a near copy of the external state and that ``wormhole state'' is the one with respect to which interactions occur during breaks. But no information is carried by ACL2 out of a wormhole -- if that were allowed wormholes would not be logical no-ops. The only information carried out of a wormhole is in the user's head.

Break-rewrite interacts with the user in a wormhole state because the signature of the ACL2 rewrite function does not permit it to modify state. Hence, only wormhole interaction is possible. (This has the additional desirable property that the correctness of the rewriter does not depend on what the user does during interactive breaks within it; indeed, it is logically impossible for the user to affect the course of rewrite.)

Now consider the list of monitored runes. Is that kept in the external state as a normal state global or is it kept in the wormhole state? If it is in the external state then it can be inspected within the wormhole but not changed. This is unacceptable; it is common to change the monitored rules as the proof attempt progresses, installing monitors when certain rules are about to be used in certain contexts. Thus, the list of monitored runes must be kept as a wormhole variable. Hence, its value cannot be determined outside the wormhole, where the proof attempt is ongoing.

This raises another question: If the list of monitored runes is unknown to the rewriter operating on the external state, how does the rewriter know when to break? The answer is simple: it breaks every time, for every rune, if brr mode is enabled. The wormhole is entered (silently), computations are done within the wormhole state to determine if the user wants to see the break, and if so, interactions begin. For unmonitored runes and runes with false break conditions, the silent wormhole entry is followed by a silent wormhole exit and the user perceives no break.

Thus, the penalty for running with brr mode enabled when there are no monitored runes is high: a wormhole is entered on every application of every rune and the user is simply unware of it. The user who has finally unmonitored all runes is therefore strongly advised to carry this information out of the wormhole and to do :brr nil in the external state when the next opportunity arises.

WORLD

Parent topic:  MISCELLANEOUS
Home

A ``world'' is a list of triples, each of the form (sym prop . val), implementing the ACL2 notion of property lists. ACL2 permits the simultaneous existence of many property list worlds. ``The world'' is often used as a shorthand for ``the ACL2 logical world'' which is the particular property list world used within the ACL2 system to maintain the data base of rules.

Common Lisp provides the notion of ``property lists'' by which one can attach ``properties'' and their corresponding ``values'' to symbols. For example, one can arrange for the 'color property of the symbol 'box-14 to be 'purple and the 'color property of the symbol 'triangle-7 to be 'yellow. Access to property lists is given via the Common Lisp function get. Thus, (get 'box-14 'color) might return 'purple. Property lists can be changed via the special form setf. Thus, (setf (get 'box-14 'color) 'blue) changes the Common Lisp property list configuration so that (get 'box-14 'color) returns 'blue. It should be obvious that ACL2 cannot provide this facility, because Common Lisp's get ``function'' is not a function of its argument, but instead a function of some implicit state object representing the property list settings for all symbols.

ACL2 provides the functions getprop and putprop which allow one to mimic the Common Lisp property list facility. However, ACL2's getprop takes as one of its arguments a list that is a direct encoding of what was above called the ``state object representing the property list settings for all symbols.'' Because ACL2 already has a notion of ``state'' that is quite distinct from that used here, we call this property list object a ``world.'' A world is just a true list of triples. Each triple is of the form (sym prop . val). This world can be thought of as a slightly elaborated form of association list and getprop is a slightly elaborated form of assoc that takes two keys. When getprop is called on a symbol, s, property p, and world, w, it scans w for the first triple whose sym is s and prop is p and returns the corresponding val. Getprop has two additional arguments, one of which that controls what it returns if no such sym and prop exist in w, and other other of which allows an extremely efficient implementation. To set some property's value for some symbol, ACL2 provides putprop. (putprop sym prop val w) merely returns a new world, w', in which (sym prop . val) has been consed onto the front of w, thus ``overwriting'' the prop value of sym in w to val and leaving all other properties in w unchanged.

One aspect of ACL2's property list arrangment is that it is possible to have many different property list worlds. For example, 'box-14 can have 'color 'purple in one world and can have 'color 'yes in another, and these two worlds can exist simultaneously because getprop is explicitly provided the world from which the property value is to be extracted.

The efficiency alluded to above stems from the fact that Common Lisp provides property lists. Using Common Lisp's provisions behind the scenes, ACL2 can ``install'' the properties of a given world into the Common Lisp property list state so as to make retrieval via getprop very fast in the special case that the world provided to getprop has been installed. To permit multiple installed worlds, each of which is permitted to be changed via putprop, ACL2 requires that worlds be named and these names are used to distinquish installed versions of the various worlds. At the moment we do not further document getprop and putprop.

However, the ACL2 system uses a property list world, named 'current-acl2-world, in which to store the succession of user commands and their effects on the logic. This world is often referred to in our documentation as ``the world'' though it should be stressed that the user is permitted to have worlds and ACL2's is in no way distinguished except that the user is not permitted to modify it except via event commands. The ACL2 world is part of the ACL2 state and may be obtained via (w state).

Warning: The ACL2 world is very large. Its length as of this writing (Version 1.5) is over 31,000 and it grows with each release. Furthermore, some of the values stored in it are pointers to old versions of itself. Printing (w state) is something you should avoid because you likely will not have the patience to await its completion. For these practical reasons, the only thing you should do with (w state) is provide it to getprop, as in the form

  (getprop sym prop default 'current-acl2-world (w state))

Some ACL2 command forms, such as theory expressions (see theories) and the values to be stored in tables (see table), are permitted to use the variable symbol world freely with the understanding that when these forms are evaluated that variable is bound to (w state). Theoretically, this gives those forms complete knowledge of the current logical configuration of ACL2. However, at the moment, few world scanning functions have been documented for the ACL2 user. Instead, supposedly convenient macro forms have been created and documented. For example, (current-theory :here), which is the theory expression which returns the currently enabled theory, actually macroexpands to (current-theory-fn :here world). When evaluated with world bound to (w state), current-theory-fn scans the current ACL2 world and computes the set of runes currently enabled in it.

WORMHOLE

Parent topic:  MISCELLANEOUS
Home

Example Form:
(wormhole t 'interactive-break nil '(value 'hi!))
                             ; Enters a recursive read-eval-print loop
                             ; on a copy of the ``current state'' and
                             ; returns nil!

General Form:
(wormhole pseudo-flg name input form
  :current-package    ...  ; known package name
  :ld-skip-proofsp    ...  ; t, nil or 'include-book
  :ld-redefinition-action  ; nil or '(:a . :b)
  :ld-prompt          ...  ; nil, t, or some prompt printer fn
  :ld-keyword-aliases ...  ; an alist pairing keywords to parse info
  :ld-pre-eval-filter ...  ; :all, :query, or some new name
  :ld-pre-eval-print  ...  ; nil, t, or :never
  :ld-post-eval-print ...  ; nil, t, or :command-conventions
  :ld-evisc-tuple     ...  ; nil or '(alist nil nil level length)
  :ld-error-triples   ...  ; nil or t
  :ld-error-action    ...  ; :continue, :return, or :error
  :ld-query-control-alist  ; alist supplying default responses
  :ld-verbose         ...) ; nil or t

Wormhole does this by manufacturing a ``wormhole state,'' a copy of the ``current state'' (whatever that is) modified so as to contain some of the wormhole arguments. Ld is called on that wormhole state with the three ld channels directed to ACL2's ``comment window.'' At the moment, the comment window is overlaid on the terminal and you cannot tell when output is going to *standard-co* and when it is going to the comment window. But we imagine that eventually a different window will pop up on your screen. In any case, the interaction provided by this call of ld does not modify the state ``from which'' wormhole was called, it modifies the copied state. When ld exits (e.g., in response to :q being typed in the comment window) the wormhole state evaporates and wormhole returns nil. Logically and actually (from the perspective of the ongoing computation) nothing has happened except that a ``no-op'' function was called and returned nil.

The name wormhole is meant to suggest the idea that the function provides easy access to state in situations where it is apparently impossible to get state. Thus, for example, if you define the factorial function, say, except that you sprinkled into its body appropriate calls of wormhole, then the execution of (factorial 6) would cause interactive breaks in the comment window. During those breaks you would apparently be able to inspect the ``current state'' even though factorial does not take state as an argument. The whole notion of there being a ``current state'' during the evaluation of (factorial 6) is logically ill-defined. And yet, we know from practical experience with the sequential computing machines upon which ACL2 is implemented that there is a ``current state'' (to which the factorial function is entirely insensitive) and that is the state to which wormhole ``tunnels.'' A call of wormhole from within factorial can pass factorial-specific information that is embedded in the wormhole state and made available for inspection by the user in an interactive setting. But no information ever flows out of a wormhole state: wormhole always returns nil.

There are four arguments to wormhole that need further explanation: pseudo-flg, name, input, and form. Roughly speaking, the value of pseudo-flg should be t or nil and indicates whether we are actually to enter a wormhole or just return nil immediately. The actual handling of pseudo-flg is more sophisticated and is explained in detail at the end of this documentation.

Name and input are used as follows. Recall that wormhole copies the ``current state'' and then modifies it slightly to obtain the state upon which ld is called. We now describe the modifications. First, the state global variable 'wormhole-name is set to name, which may be any non-nil ACL2 object but is usually a symbol. Then, 'wormhole-input is set to input, which may be any ACL2 object. Finally, and inexplicably, 'wormhole-output is set to the value of 'wormhole-output the last time a wormhole named name was exited (or nil if this is the first time a wormhole named name was entered). this last aspect of wormholes, namely the preservation of 'wormhole-output, allows all the wormholes of a given name to communicate with each other.

We can now explain how form is used. The modified state described above is the state on which ld is called. However, standard-oi -- the input channel from which ld reads commands -- is set so that the first command that ld reads and evaluates is form. If form returns an error triple with value :q, i.e., form returns via (value :q), then no further commands are read, ld exits, and the wormhole exits and returns nil. But if form returns any other value (or is not an error triple), then subsequent commands are read from the comment window.

As usual, the ld-specials affect whether a herald is printed upon entry, whether form is printed before evaluation, whether a prompt is printed, how errors are handled, etc. The ld-specials can be specified with the corresponding arguments to wormhole. It is standard practice to call wormhole so that the entry to ld and the evaluation of form are totally silent. Then, tests in form can inspect the state and decide whether user interaction is desired. If so, form can appropriately set ld-prompt, ld-error-action, etc., print a herald, and then return (value :invisible). Recall (see ld) that (value :invisible) causes ld not to print a value for the just executed form. The result of this arrangement is that whether interaction occurs can be based on tests that are performed on the wormhole state after (@ wormhole-input) and the last (@ wormhole-output) are available for inspection. This is important because outside the wormhole you can access wormhole-input (you are passing it into the wormhole) but you may not be able to access the current state (because you might be in factorial) and you definitely cannot access the wormhole-output of the last wormhole because it is not part of the ACL2 state. Thus, if the condition under which you wish to interact depends upon the state or that part of it preserved from the last wormhole interaction, that condition can only be tested from within the wormhole, via form.

It is via this mechanism that break-rewrite (see break-rewrite) is implemented. To be more precise, the list of monitored runes is maintained as part of the preserved wormhole-output of the break-rewrite wormhole. Because it is not part of the normal state, it may be changed by the user during proofs. That is what allows you to install new monitors while debugging proofs. But that means that the list of monitored runes cannot be inspected from outside the wormhole. Therefore, to decide whether a break is to occur when a given rule is applied, the rewriter must enter the break-rewrite wormhole, supplying a form that causes interaction if the given rule's break condition is satisfied. The user perceives this as though the wormhole was conditionally entered -- a perception that is happily at odds with the informed user's knowledge that the list of monitored runes is not part of the state. In fact, the wormhole was unconditionally entered and the condition was checked from within the wormhole, that being the only state in which the condition is known.

Another illustrative example is available in the implemention of the monitor command. How can we add a new rune to the list of monitored runes while in the normal ACL2 state (i.e., while not in a wormhole)? The answer is: by getting into a wormhole. In particular, when you type (monitor rune expr) at the top-level of ACL2, monitor enters the break-rewrite wormhole with a cleverly designed first form. That form adds rune and expr to the list of monitored runes -- said list only being available in break-rewrite wormhole states. Then the first form returns (value :q), which causes us to exit the wormhole. By using ld-specials that completely suppress all output during the process, it does not appear to the user that a wormhole was entered. The moral here is rather subtle: the first form supplied to wormhole may be the entire computation you want to perform in the wormhole; it need not just be a predicate that decides if interaction is to occur. Using wormholes of different names you can maintain a variety of ``hidden'' data structures that are always accessible (whether passed in or not). This appears to violate completely the applicative semantics of ACL2, but it does not: because these data structures are only accessible via wormholes, it is impossible for them to affect any ACL2 computation (except in the comment window).

As one might imagine, there is some overhead associated with entering a wormhole because of the need to copy the current state. This brings us back to pseudo-flg. Ostensibly, wormhole is a function and hence all of its argument expressions are evaluated outside the function (and hence, outside the wormhole it creates) and then their values are passed into the function where an appropriate wormhole is created. In fact, wormhole is a macro that permits the pseudo-flg expression to peer dimly into the wormhole that will be created before it is created. In particular, pseudo-flg allows the user to access the wormhole-output that will be used to create the wormhole state.

This is done by allowing the user to mention the (apparently unbound) variable wormhole-output in the first argument to wormhole. Logically, wormhole is a macro that wraps

(let ((wormhole-output nil)) ...)

(if pseudo-flg (wormhole name input form ...) nil).

We conclude with an example of the use of pseudo-flg. This example is a simplification of our implementation of break-rewrite. To enter break-rewrite at the beginning of the attempted application of a rule, rule, we use

(wormhole
 (and (f-get-global 'brr-mode state)
      (member-equal (access rewrite-rule rule :rune)
                    (cdr (assoc-eq 'monitored-runes wormhole-output))))
 'break-rewrite
 ...)

However, it is useful to think of wormhole as a simple function that evaluates all of its arguments but to also imagine that somehow wormhole-output is magically bound around the first argument so that wormhole-output is the output of the last break-rewrite wormhole. If we so imagine, then the pseudo-flg expression above evaluates either to nil or non-nil and we will enter the wormhole named break-rewrite in the latter case.

Now what does the pseudo-flg expression above actually test? We know the format of our own wormhole-output because we are responsible for maintaining it. In particular, we know that the list of monitored runes can be obtained via

(cdr (assoc-eq 'monitored-runes wormhole-output)).