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 as described below. It is forbidden to invoke
wormhole-eval on the names listed in
*protected-system-wormhole-names*, which includes brr (the break-rewrite wormhole name), accumulated-persistence, and
fc-wormhole (the name of the wormhole managing forward-chaining-reports), among others.
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 persistent-whs (see wormhole-status) of
the named wormhole and remembers the value as the new persistent-whs. If the
lambda has no formal parameter, the lambda is applied to no
arguments and the value is the new persistent-whs. 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 the persistent-whs, but the results
remain hidden. To interact with the wormhole's state you must use 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.
Subtopics
- Wormhole-programming-tips
- some tips for how to use wormholes
