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 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 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.
