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.

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.

Wormholes are not re-entrant: it is illegal to invoke wormhole-eval or wormhole while within either. If you do, the inner call just prints an error message and returns nil.

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.