Wormhole-eval
State-saving without state — a short-cut to a parallel universe
Example Form:
(wormhole-eval 'demo
'(lambda (whs)
(set-wormhole-data whs
(cons (cons name info)
(wormhole-data whs))))
(prog2$ info name))
General Form:
(wormhole-eval name lambda varterm)
where name must be a quoted wormhole name and lambda must be a
quoted lambda-expression. The lambda-expression must have at most
one formal parameter but the body of the lambda-expression may contain
other variables. Note that in the example form given above, the lambda
has one formal, whs, and uses name and info freely. Note that
the lambda is quoted. The third argument of wormhole-eval,
varterm, is an arbitrary term that should mention all of the free
variables in the lambda-expression. That term establishes your ``right''
to refer to those free variables in the environment in which the
wormhole-eval expression occurs. The value of varterm is irrelevant
and if you provide nil ACL2 will automatically provide a suitable term,
namely a prog2$ form like the one shown in the example above.
Aside: Exception for ACL2(p) (see parallelism) to the irrelevance of
varterm. By default, calls of wormhole-eval employ a lock,
*wormhole-lock*. To avoid such a lock, include the symbol
:NO-WORMHOLE-LOCK in varterm; for example, you might replace a last
argument of nil in wormhole-eval by :NO-WORMHOLE-LOCK. End of
Aside.
See wormhole for a full explanation of wormholes. Most relevant
here is that every wormhole has a name and a status. The status is generally
a cons pair whose car is the keyword :ENTER or the keyword
:SKIP and whose cdr is an arbitrary object used to store information
from one wormhole call to the next.
Here is a succinct summary of wormhole-eval. If the
lambda-expression has a local variable, wormhole-eval applies the
lambda-expression to the wormhole status of the named wormhole and
remembers the value as the new wormhole status. If the lambda has no
formal parameter, the lambda is applied to no arguments and the value is
the new status. Wormhole-eval returns nil. Thus, the formal
parameter of the lambda-expression, if provided, denotes the wormhole's
hidden status information; the value of the lambda is the new status and
is hidden away.
The guard of a wormhole-eval call is the guard of the body of the
lambda-expression, with a fresh variable symbol used in place of the
formal so that no assumptions are possible about the hidden wormhole status.
If the guard of a wormhole-eval is verified, the call is macroexpanded
inline to the evaluation of the body in a suitable environment. Thus, it can
be a very fast way to access and change hidden state information, but the
results must remain hidden. To do arbitrary computations on the hidden state
(i.e., to access the ACL2 state or logical world or to interact
with the user) see wormhole.
Functions that are probably useful in the body of the lambda or the
guard of a function using wormhole-eval include the following: wormhole-statusp, wormhole-entry-code, wormhole-data, set-wormhole-entry-code, set-wormhole-data, and make-wormhole-status.
Wormhole-eval is intended to be fast, but it is further optimized when
the given lambda is of the following form. In this case
wormhole-eval returns immediately when the wormhole-data is
nil, which is reasonable since the old and new status are equal in this
case.
(lambda (whs)
(let ((info (wormhole-data whs)))
(cond ((null info) whs)
...)))
See wormhole for a series of example uses of wormhole-eval and
wormhole.
For a behind-the-scenes description of how wormholes work, See wormhole-implementation.
