		Search-engine friendly clone of the ACL2 documentation.

Note-4-0

Note-4-0-wormhole-changes

How to convert calls of wormhole for Version 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.