WORMHOLE

Major Section:  MISCELLANEOUS

Example Form:
; The following form enters a recursive read-eval-print loop on a
; copy of the current state, allowing you to interact with that loop.
; Note that the form does not mention the ACL2 state variable!
; Evaluate the form below. Inside the resulting loop, define some function,
; e.g., with (defun foo (x) x).  Then exit with :q and observe,
; e.g., with :pe foo, that the external state did not change.

(wormhole 'foo
          '(lambda (whs) (set-wormhole-entry-code whs :ENTER))
          nil
          '(list 'hello 'there))

General Form:
(wormhole name entry-lambda input form
  :current-package    ...  ; known package name
  :ld-skip-proofsp    ...  ; nil, t 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-missing-input-ok ... ; nil, t, :warn, or warning message
  :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 level length hiding-cars)
  :ld-error-triples   ...  ; nil or t
  :ld-error-action    ...  ; :return!, :return, :continue, or :error
  :ld-query-control-alist  ; alist supplying default responses
  :ld-verbose         ...) ; nil or t

There are two ways to create and enter a wormhole: wormhole as described here and the simpler wormhole-eval. We recommend you read this full account of wormholes before using wormhole-eval.

Ignoring the use of entry-lambda, wormhole manufactures a named ``wormhole state'' and calls the general-purpose ACL2 read-eval-print loop ld on it. However, when ld exits, the wormhole evaporates and the function wormhole returns nil. The manufactured state is like the ``current'' ACL2 state except for two things. First, some information from the last wormhole state of this name is transferred into the new state; this allows a wormhole to maintain some state from one call to the next. Second, some information from the wormhole call itself is transferred into the new state; this allows the wormhole to be sensitive to context. These two changes to the current state are reflected in the settings (@ wormhole-status) and (@ wormhole-input) discussed in detail below.

Note that wormhole may be called from environments in which state is not bound. It is still applicative because it always returns nil.

There are some restrictions about what can be done inside a wormhole. As you may imagine, we really do not ``copy the current state'' but rather just keep track of how we modified it and undo those modifications upon exit. An error is signalled if you try to modify state in an unsupported way. For this same reason, wormholes do not allow updating of any user-defined single-threaded objects. See stobj.

One example wormhole is the implementation of the ACL2 accumulated-persistence facility for tracking the frequency with which rules are tried. To implement this feature directly the theorem prover would have to take the tracking data as an argument and pass it around so that updates could be accumulated. This would greatly clutter the code. Instead, the tracking data is maintained in a wormhole. The theorem prover enters the wormhole to update the data as rules are tried. When you request a display of the data, show-accumulated-persistence enters the wormhole and prints the data. But the data is never available outside that wormhole. The ACL2 system uses a second wormhole to implement the brr facility, allowing the user to interact with the rewriter as rules are applied.

We now specify the arguments and behavior of wormhole.

The name argument must be a quoted constant and is typically a symbol. It will be the ``name'' of the wormhole. A wormhole of that name will be created the first time either wormhole or wormhole-eval is called.

Every wormhole name has a ``status.'' The status of a wormhole is stored outside of ACL2; it is inaccessible to the ACL2 user except when in the named wormhole. But the status of a wormhole may be set by the user from within the wormhole.

Upon the first call of wormhole or wormhole-eval on a name, the status of that name is nil. But in general you should arrange for the status to be a cons. The status is set by the quoted lambda every time wormhole is called; but it may also be set in the form argument (the first form evaluated in the interactive loop) by assigning to the state global variable wormhole-status, as with

(assign wormhole-status ...)

When wormhole is invoked, the status of the specified name is incorporated into the manufactured wormhole state. In particular, inside the wormhole, the status is the value of the state global variable wormhole-status. That is, inside the wormhole, the status may be accessed by (@ wormhole-status) and set by (assign wormhole-status ...), f-get-global and f-put-global. When ld exits -- typically because the form :q was read by ld -- the then-current value of wormhole-status is hidden away so that it can be restored when this wormhole is entered again. The rest of the wormhole state is lost.

This allows a sequence of entries and exits to a wormhole to maintain some history in the status and this information can be manipulated by ACL2 functions executing inside the wormhole.

The second argument to wormhole must be a quoted lambda expression. We explain it later.

The third argument, input, may be any term. The value of the term is passed into the manufactured wormhole state, allowing you to pass in information about the calling context. Inside the wormhole, the input is available via (@ wormhole-input). It could be reassigned via (assign wormhole-input ...), but there is no reason to do that.

The fourth argument, form, may be any term; when ld is called on the manufactured wormhole state, the first form evaluated by ld will be the value of form. Note that form will be translated by ld. Errors, including guard violations, in the translation or execution of that first form will leave you in the interactive loop of the wormhole state.

When used properly, the first form allows you to greet your user before reading the first interactive command or simply to do whatever computation you want to do inside the wormhole and exit silently. We give examples below.

Manufacturing a wormhole state is relatively expensive; in addition, the forms executed by ld must be read, translated, and interpreted as with any user type-in. The entry-lambda offers a way to avoid this or, at least, to decide whether to incur that expense.

Before the wormhole state is manufactured and entered, the entry-lambda is applied to the current wormhole status with wormhole-eval. That lambda application must produce a new wormhole status, which is stored as the wormhole's status. The entry code for the new status determines whether wormhole actually manufactures a wormhole state and calls ld.

If the entry code for that new status is :ENTER the wormhole state is manufactured and entered; otherwise, the new status is simply saved as the most recent status but the wormhole state is not manufactured or entered. Note therefore that the entry-lambda may be used to perform two functions: (a) to determine if it is really necessary to manufacture a state and (b) to update the data in the wormhole status as a function of the old status without invoking ld.

The entry-lambda must be a quoted lambda expression of at most one argument. Thus, the argument must be either

'(lambda (whs) <body>)

'(lambda () <body>)

The guard on a call of wormhole is the conjunction of the guards on the arguments conjoined with the guard on the body of the entry-lambda. See wormhole-eval for a discussion of the guard on the lambda-expression.

The functions wormhole-statusp, wormhole-entry-code, wormhole-data, set-wormhole-entry-code, set-wormhole-data, and make-wormhole-status may be useful in manipulating entry codes and data in the entry-lambda.

Note that you access and manipulate the wormhole's status in two different ways depending on whether you're ``outside'' of the wormhole applying the quoted lambda or ``inside'' the read-eval-print loop of the wormhole.

OUTSIDE (wormhole-eval): access via the value of the lambda formal and set by returning the new status as the value of the lambda body.

INSIDE (ld phase of wormhole): access via (@ wormhole-status), and set via (assign wormhole-status ...).

Pragmatic Advice on Designing a Wormhole: Suppose you are using wormholes to implement some extra-logical utility. You must contemplate how you will use your wormhole's status to store hidden information. You might be tempted to exploit the entry code as part of the status. For example, you may think of :ENTER as indicating that your utility is ``turned on'' and :SKIP as indicating that your utility is ``turned off.'' We advise against such a design. We recommend you base your decisions on the wormhole data. We recommend that you set but not read the wormhole entry code to signal whether you wish to enter a full-fledged wormhole. To use the entry code as a flag overloads it and invites confusion when your facility is ``turned off'' but you have to enter the wormhole for some reason.

For a behind-the-scenes description of how wormholes work, See wormhole-implementation.

Here are some sample situations handled by wormhole-eval and wormhole. Let the wormhole in question be named DEMO. Initially its status is NIL. The functions below all maintain the convention that the status is either nil or of the form (:key . lst), where :key is either :SKIP or :ENTER and lst is a true-list of arbitrary objects. But since there is no way to prevent the user from entering the DEMO wormhole interactively and doing something to the status, this convention cannot be enforced. Thus, the functions below do what we say they do, e.g., remember all the values of x ever seen, only if they're the only functions messing with the DEMO status. On the other hand, the guards of all the functions below can be verified. We have explicitly declared that the guards on the functions below are to be verified, to confirm that they can be. Guard verification is optional but wormholes (and wormhole-eval in particular) are more efficient when guards have been verified. All of the functions defined below return nil.

The examples below build on each other. If you really want to understand wormholes we recommend that you evaluate each of the forms below, in the order they are discussed.

Q. How do I create a wormhole that prints its status to the comment window?

(defun demo-status ()
  (declare (xargs :verify-guards t))
  (wormhole-eval 'demo
                 '(lambda (whs)
                    (prog2$ (cw "DEMO status:~%~x0~%" whs)
                            whs))
                 nil))

Note above that after printing the status to the comment window we return the new (unchanged) status whs. Had we just written the call of cw, which returns nil, the function would print the status and then set it to nil!

Q. How do I use a wormhole to collect every symbol, x, passed to the function?

(defun demo-collect (x)
  (declare (xargs :verify-guards t))
  (wormhole-eval 'demo
                 '(lambda (whs)
                    (make-wormhole-status whs
                                          (wormhole-entry-code whs)
                                          (if (symbolp x)
                                              (cons x (wormhole-data whs))
                                              (wormhole-data whs))))
                 nil))

(defun demo-collect (x)
  (declare (xargs :verify-guards t))
  (if (symbolp x)
      (wormhole-eval 'demo
                     '(lambda (whs)
                        (set-wormhole-data whs
                                           (cons x (wormhole-data whs))))
                     nil)
      nil))

Q. How do I use demo-collect? Below is a function that maps over a list and computes its length. But it has been annotated with a call to demo-collect on every element.

 (defun my-len (lst)
   (if (endp lst)
       0
       (+ 1
          (prog2$ (demo-collect (car lst))
                  (my-len (cdr lst))))))

ACL2 !>(my-len '(4 temp car "Hi" rfix))
5
ACL2 !>(demo-status)
DEMO status:
(:ENTER RFIX CAR TEMP)
NIL
ACL2 !>

Q. How do I set the entry code to :ENTER or :SKIP according to whether name is a member-equal of the list of things seen so far? Note that we cannot check this condition outside the wormhole, because it depends on the list of things collected so far. We make the decision inside the lambda-expression. Note that we explicitly check that the guard of member-equal is satisfied by the current wormhole status, since we cannot rely on the invariant that no other function interferes with the status of the DEMO wormhole. In the case that the status is ``unexpected'' we act like the status is nil and set it to (:SKIP . NIL).

(defun demo-set-entry-code (name)
  (declare (xargs :verify-guards t))
  (wormhole-eval 'demo
                 '(lambda (whs)
                    (if (true-listp (wormhole-data whs))
                        (set-wormhole-entry-code
                         whs
                         (if (member-equal name (wormhole-data whs))
                             :ENTER
                             :SKIP))
                        '(:SKIP . NIL)))
                 nil))

ACL2 !>(demo-set-entry-code 'monday)
NIL
ACL2 !>(demo-status)
DEMO status:
(:SKIP RFIX CAR TEMP)
NIL
ACL2 !>(demo-set-entry-code 'rfix)
NIL
ACL2 !>(demo-status)
DEMO status:
(:ENTER RFIX CAR TEMP)
NIL
ACL2 !>

Q. Suppose I want to collect every symbol and then, if the symbol has an ABSOLUTE-EVENT-NUMBER property in the ACL2 logical world, print the defining event with :pe and then enter an interactive loop; but if the symbol does not have an ABSOLUTE-EVENT-NUMBER, don't print anything and don't enter an interactive loop.

Here it is not important to know what ABSOLUTE-EVENT-NUMBER is; this example just shows that we can use a wormhole to access the ACL2 logical world, even in a function that does not take the state as an argument.

In the code below, we use wormhole instead of wormhole-eval, because we might have to access the logical world and enter an interactive loop. But for efficiency we do as much as we can inside the entry lambda, where we can check whether x is symbol and collect it into the data field of the wormhole status. Note that if we collect x, we also set the entry code to :ENTER. If we don't collect x, we set the entry code to :SKIP.

(defun collect-symbols-and-print-events (x)
  (declare (xargs :guard t))
  (wormhole 'demo
            '(lambda (whs)
               (if (symbolp x)
                   (make-wormhole-status whs
                                         :ENTER
                                         (cons x (wormhole-data whs)))
                   (set-wormhole-entry-code whs :SKIP)))

; The wormhole will not get past here is unless the entry code is
; :ENTER.  If we get past here, we manufacture a state, put
; x into (@ wormhole-input) and call ld in such a way that the
; first form executed is the quoted if-expression below.

            x
            '(if (getprop (@ wormhole-input)
                          'absolute-event-number
                          nil
                          'CURRENT-ACL2-WORLD (w state))
                 (er-progn
                  (mv-let (col state)
                          (fmt "~%Entering a wormhole on the event name ~x0~%"
                               (list (cons #\0 (@ wormhole-input)))
                               *standard-co* state nil)
                          (declare (ignore col))
                          (value nil))
                  (pe (@ wormhole-input))
                  (set-ld-prompt 'wormhole-prompt state)
                  (value :invisible))
                 (value :q))
            :ld-verbose nil
            :ld-prompt nil))

The ``first form'' (the if) asks whether the wormhole-input (i.e., x) has an ABSOLUTE-EVENT-NUMBER property. If so, it enters an er-progn to perform a sequence of commands, each of which returns an ACL2 error triple (see programming-with-state). The first form uses fmt to print a greeting. Since fmt returns (mv col state) and we must return an error triple, we embed the fmt term in an (mv-let (col state) ... (value nil)). The macro value takes an object and returns a ``normal return'' error triple. The second form in the er-progn uses the ACL2 history macro pe (see pe) to print the defining event for a name. The third form sets the prompt of this read-eval-print loop to the standard function for printing the wormhole prompt. We silenced the printing of the prompt when we called ld, thanks to the :ld-prompt nil keyword option. More on this below. The fourth form returns the error triple value :invisible as the value of the first form. This prevents ld from printing the value of the first form. Since we have not exited ld, that function just continues by reading the next form from the comment window. The user perceives this as entering a read-eval-print loop. We continue in the loop until the user types :q.

On the other branch of the if, if the symbol has no ABSOLUTE-EVENT-NUMBER property, we execute the form (value :q), which is the programming equivalent of typing :q. That causes the ld to exit.

The ld special variables set in the call to wormhole and further manipulated inside the first form to ld may require explanation. By setting :ld-verbose to nil, we prevent ld from printing the familiar ACL2 banner when ld is called. If :ld-verbose nil is deleted, then you would see something like

ACL2 Version  4.0.  Level 2.
...
Type (good-bye) to quit completely out of ACL2.

By setting :ld-prompt to nil we prevent ld from printing the prompt before reading and evaluating the first form.

As this example shows, to use full-blown wormholes you must understand the protocol for using wormhole status to control whether a wormhole state is manufactured for ld and you must also understand programming with state and the effects of the various ld ``special variables.''

From the discussion above we see that wormholes can be used to create formatted output without passing in the ACL2 state. For examples see cw, in particular the discussion at the end of that documentation topic.