Major Section: MISCELLANEOUS
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 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.
