Major Section: NOTE-4-0
Here we describe how to convert an ``old-style'' call of wormhole --
that is, a call suitable for ACL2 versions preceding 4.0 -- in which the
pseudo-flag was t. In order to convert such a call
(wormhole t 'name input form ...)to a new-style call, the following steps must be carried out. Note that the wormhole name must always be quoted now.
First, eliminate the first argument, t, and add a new second argument
that is the quoted lambda expression
'(lambda (whs) (set-wormhole-entry-code whs :ENTER))Setting the entry code to
:ENTER is not necessary if you maintain the
invariant (after initialization) that it is always :ENTER. In that case,
the simpler quoted lambda will suffice:
'(lambda (whs) whs)
Second, change the form argument so that instead of talking about the
state-global variable wormhole-output it talks about the state-global
variable wormhole-status. Look for
(@ wormhole-output), (assign wormhole-output ...),
(f-get-global 'wormhole-output ...) and
(f-put-global 'wormhole-output ...) in form and replace them with
expressions involving wormhole-status.
However, remember that the old data stored in wormhole-output is now
in the wormhole-data component of the wormhole-status. Thus, for
example, an old use of (@ wormhole-output) will typically be replaced
by (wormhole-data (@ wormhole-status)) and an old use of
(assign wormhole-output ...) will typically be replaced by
(assign wormhole-status (set-wormhole-data (@ wormhole-status) ...))
In summary, an old-style call like
(wormhole t 'name
input
'(...1 (@ wormhole-output) ...2
...3 (assign wormhole-output ...4) ...5)
...6)
can become
(wormhole 'name
'(lambda (whs) (set-wormhole-entry-code whs :ENTER))
input
'(...1 (wormhole-data (@ wormhole-status)) ...2
...3 (assign wormhole-status
(set-wormhole-data (@ wormhole-status)
...4) ...5)
...6)
In any case, and especially if your wormhole call had a pseudo-flag
other than t, we recommend that you see wormhole.
