Wormhole-implementation
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) ...)
input
form
: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 persistent-whs and the result is
stored as the new persistent-whs. Then, if the entry-code of the new status
is :ENTER (actually, if it is not :SKIP), 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 variables wormhole-name, wormhole-input and
wormhole-status are assigned name, the the value of input and
the persistent-whs, respectively. Thus, inside the wormhole, (@
wormhole-name) returns the name of the current wormhole, (@
wormhole-input) returns the list of inputs, (@ wormhole-status) returns
the ephemeral-whs. 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 ephemeral-whs is written to the persistent-whs
and the wormhole state ``evaporates.'' The next time the wormhole is entered
its ephemeral-whs will be what it was when it last exited.
Here is what really happens.
Each wormhole's persistent-whs 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*. However, be cautious about
printing it because the persistent-whs of some wormholes can be quite large.
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 wormhole
status.
If the newly computed status has an entry code other than :SKIP 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, *wormholep*, 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 we assign the three state globals
wormhole-name, wormhole-input, and wormhole-status. Those
assignments are made undoably since *wormholep* is set.
Then ld is invoked, with first argument, standard-oi, being set
to (cons form *standard-oi*). According to the standard semantics of
ld, the first read from this standard-oi returns form and
subsequent reads, if any, come from *standard-oi*. 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
*wormholep* 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 ephemeral-whs is transferred to
the persistent-whs, i.e., the final value of (@ wormhole-status) is
stored under the current wormhole-name in *wormhole-status-alist*
and then the accumulator is used to ``undo'' all the state changes.
Wormhole always returns nil.
The system wormhole named brr, which implements break-rewrite,
is treated a little differently. When ld exits due to an abort the
ephemeral-whs is not transferred to the persistent-whs. Instead, the
persistent-whs is set to what it was at the time break-rewrite was first
entered from the top-level. See the Essay on Break-Rewrite in the source code
file rewrite.lisp for details about the implementation of break-rewrite,
which is intimately connected to wormholes.
