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