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
namemust be a quoted wormhole name and
lambdamust be a quoted
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
lambdahas one formal,
whs, and uses
infofreely. Note that the
lambdais quoted. The third argument of
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-evalexpression occurs. The value of
vartermis irrelevant and if you provide
nilACL2 will automatically provide a suitable term, namely a
prog2$form like the one shown in the example above.
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
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.
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:
See wormhole for a series of example uses of
For a behind-the-scenes description of how wormholes work, See wormhole-implementation.