notes on how wormholes are implemented

What happens when you call wormhole? Recall that a typical call of the function looks like this:

(wormhole 'name
          '(lambda (whs) ...)
          :ld-verbose ...

A brief recap of the advertised semantics for wormhole establishes our terminology: When the above wormhole is evaluated, the lambda-expression is applied to the wormhole's status and the result is stored as the new status. Then, if the entry-code of the new status is :ENTER, ld is invoked on a copy of the ``current state'' with the specified ld- ``special variables;'' output is directed to the comment window. In that copy of the state, the state-global variable wormhole-input is set to the value of input and the state-global variable wormhole-status is set to the (new) status computed by the lambda-expression. Thus, inside the wormhole, (@ wormhole-input) returns the list of inputs, (@ wormhole-status) returns the current status, and (assign wormhole-status ...) sets the wormhole's status. The first form executed by the ld is the value of form and unless that form returns (value :q), causing the ld to quit, the ld proceeds to take subsequent input from the comment window. Upon exiting from ld, the wormhole state ``evaporates.'' The wormhole's status upon exit is remembered and restored the next time the wormhole is entered.

Here is what really happens.

Each wormhole's status is recorded in an alist stored in a Common Lisp global variable named *wormhole-status-alist*. This variable is not part of the ACL2 state. If you exit the ACL2 loop with :q you can inspect the value of *wormhole-status-alist*. When the lambda-expression is evaluated it is applied to the value associated with name in the alist and the result is stored back into that alist. This step is performed by wormhole-eval. To make things more efficient, wormhole-eval is just a macro that expands into a let that binds the lambda formal to the current status and whose body is the lambda body. Guard clauses are generated from the body, with one exception: the lambda formal is replaced by a new variable so that no prior assumptions are available about the value of the the wormhole status.

If the newly computed status has an entry code of :ENTER ld will be invoked. But we don't really copy state, of course. Instead we will invoke ld on the live state, which is always available in the von Neumann world in which ACL2 is implemented. To give the illusion of copying state, we will undo changes to the state upon exiting. To support this, we do two things just before invoking ld: we bind a Common Lisp special variable is to t to record that ACL2 is in a wormhole, and we initialize an accumulator that will be used to record state changes made while in the wormhole.

Then ld is invoked, with first argument, standard-oi, being set to (cons form *standard-oi*). According to the standard semantics of ld, this reads and evaluates form and then the forms in the specified channel. The standard channels are directed to and from the terminal, which is the physical realization of the comment window.

All state modifying functions of ACL2 are sensitive to the special variable that indicates that evaluation is in a wormhole. Some ACL2 state-modifying functions (e.g., those that modify the file system like write-byte$) are made to cause an error if invoked inside a wormhole on a file other than the terminal. Others, like f-put-global (the function behind such features as assign and maintenance of the ACL2 logical world by such events as defun and defthm) are made to record the old value of the state component being changed; these records are kept in the accumulator initialized above.

Upon exit from ld for any reason, the final value of (@ wormhole-status) is stored in *wormhole-status-alist* and then the accumulator is used to ``undo'' all the state changes.

Wormhole always returns nil.