Wormhole
ld without state — a short-cut to a parallel universe
Example Form:
; The following form enters a recursive read-eval-print loop on a
; copy of the current state, allowing you to interact with that loop.
; Note that the form does not mention the ACL2 state variable!
; Evaluate the form below. Inside the resulting loop, define some function,
; e.g., with (defun foo (x) x). Then exit with :q and observe,
; e.g., with :pe foo, that the external state did not change.
(wormhole 'foo
'(lambda (whs) (set-wormhole-entry-code whs :ENTER))
nil
'(list 'hello 'there))
General Form:
(wormhole name entry-lambda input form
:current-package ... ; known package name
:ld-skip-proofsp ... ; nil, t or 'include-book
:ld-redefinition-action ; nil or '(:a . :b)
:ld-prompt ... ; nil, t, or some prompt printer fn
:ld-missing-input-ok ... ; nil, t, :warn, or warning message
:ld-pre-eval-filter ... ; :all, :query, or some new name
:ld-pre-eval-print ... ; nil, t, or :never
:ld-post-eval-print ... ; nil, t, or :command-conventions
:ld-evisc-tuple ... ; nil or '(alist level length hiding-cars)
:ld-error-triples ... ; nil or t
:ld-error-action ... ; :return!, :return, :continue, :error,
; or (:exit N)
:ld-query-control-alist ; alist supplying default responses
:ld-verbose ...) ; nil or t
The keyword arguments above are exactly those of ld (see ld)
except that three of ld's keyword arguments are missing: the three
that specify the channels standard-oi, standard-co and proofs-co, which default in wormhole to ACL2's comment window.
There are two ways to create and enter a wormhole: wormhole as
described here and the simpler wormhole-eval. We recommend you read
this full account of wormholes before using wormhole-eval.
Ignoring the use of entry-lambda, wormhole manufactures a named
``wormhole state'' and calls the general-purpose ACL2 read-eval-print
loop ld on it. However, when ld exits, the wormhole evaporates
and the function wormhole returns nil. The manufactured state is
like the ``current'' ACL2 state except for two things. First, some
information from the last wormhole state of this name is transferred into the
new state; this allows a wormhole to maintain some state from one call to the
next. Second, some information from the wormhole call itself is transferred
into the new state; this allows the wormhole to be sensitive to context.
These two changes to the current state are reflected in the settings (@
wormhole-status) and (@ wormhole-input) discussed in detail below.
Note that wormhole may be called from environments in which state is not bound. It is still applicative because it always returns
nil.
There are some restrictions about what can be done inside a wormhole. As
you may imagine, we really do not ``copy the current state'' but rather just
keep track of how we modified it and undo those modifications upon exit. In
particular, when exiting a wormhole, values of state globals (see programming-with-state) are restored to their values at the time the wormhole
was entered. Note that information about traced functions is stored in state
globals (see trace$); accordingly, all tracing and untracing done
inside a wormhole is undone upon exit from the wormhole.
An error is signaled if you try to modify state in an unsupported way.
For this same reason, wormholes do not allow updating of any user-defined
single-threaded objects. See stobj.
One example wormhole is the implementation of the ACL2 accumulated-persistence facility for tracking the frequency with which rules
are tried. To implement this feature directly the theorem prover would have
to take the tracking data as an argument and pass it around so that updates
could be accumulated. This would greatly clutter the code. Instead, the
tracking data is maintained in a wormhole. The theorem prover enters the
wormhole to update the data as rules are tried. When you request a display of
the data, show-accumulated-persistence enters the wormhole and prints
the data. But the data is never available outside that wormhole. The ACL2
system uses a second wormhole to implement the brr facility, allowing
the user to interact with the rewriter as rules are applied.
We now specify the arguments and behavior of wormhole.
The name argument must be a quoted constant and is typically a symbol.
It will be the ``name'' of the wormhole. A wormhole of that name will be
created the first time either wormhole or wormhole-eval is
called.
Every wormhole name has a ``status.'' The status of a wormhole is stored
outside of ACL2; it is inaccessible to the ACL2 user except when in the named
wormhole. But the status of a wormhole may be set by the user from within the
wormhole.
Upon the first call of wormhole or wormhole-eval on a name, the
status of that name is nil. But in general you should arrange for the
status to be a cons. The status is set by the quoted lambda every time
wormhole is called; but it may also be set in the form argument (the
first form evaluated in the interactive loop) by assigning to the state global
variable wormhole-status, as with
(assign wormhole-status ...)
or even by the user interacting with the loop if you do not exit the loop
with the first form. The car of the cons should be either :ENTER or
:SKIP and is called the wormhole's ``entry code.'' The entry code of
nil or an unexpectedly shaped status is :ENTER. The cdr of the
cons is arbitrary data maintained by you.
When wormhole is invoked, the status of the specified name is
incorporated into the manufactured wormhole state. In particular, inside the
wormhole, the status is the value of the state global variable
wormhole-status. That is, inside the wormhole, the status may be
accessed by (@ wormhole-status) and set by (assign wormhole-status
...), f-get-global and f-put-global. When ld exits —
typically because the form :q was read by ld — the
then-current value of wormhole-status is hidden away so that it can be
restored when this wormhole is entered again. The rest of the wormhole state
is lost.
This allows a sequence of entries and exits to a wormhole to maintain some
history in the status and this information can be manipulated by ACL2
functions executing inside the wormhole.
The second argument to wormhole must be a quoted lambda expression.
We explain it later.
The third argument, input, may be any term. The value of the term is
passed into the manufactured wormhole state, allowing you to pass in
information about the calling context. Inside the wormhole, the input is
available via (@ wormhole-input). It could be reassigned via (assign
wormhole-input ...), but there is no reason to do that.
The fourth argument, form, may be any term; when ld is called
on the manufactured wormhole state, the first form evaluated by ld will
be the value of form. Note that form will be translated by ld.
Errors, including guard violations, in the translation or execution of that
first form will leave you in the interactive loop of the wormhole state.
When used properly, the first form allows you to greet your user before
reading the first interactive command or simply to do whatever computation you
want to do inside the wormhole and exit silently. We give examples below.
Manufacturing a wormhole state is relatively expensive; in addition, the
forms executed by ld must be read, translated, and interpreted as with
any user type-in. The entry-lambda offers a way to avoid this or, at
least, to decide whether to incur that expense.
Before the wormhole state is manufactured and entered, the
entry-lambda is applied to the current wormhole status with wormhole-eval. That lambda application must produce a new wormhole
status, which is stored as the wormhole's status. The entry code for the new
status determines whether wormhole actually manufactures a wormhole state
and calls ld.
If the entry code for that new status is :ENTER the wormhole state is
manufactured and entered; otherwise, the new status is simply saved as the
most recent status but the wormhole state is not manufactured or entered.
Note therefore that the entry-lambda may be used to perform two
functions: (a) to determine if it is really necessary to manufacture a state
and (b) to update the data in the wormhole status as a function of the old
status without invoking ld.
The entry-lambda must be a quoted lambda expression of at most one
argument. Thus, the argument must be either
'(lambda (whs) <body>)
or
'(lambda () <body>)
Note the quote. If a formal, e.g., whs, is provided, it must be used
as a variable in the lambda body. The lambda-expression may contain
free variables, that is, the body may mention variables other than the
lambda formal. These free variables are understood in the caller's
environment. These conventions allow us to compile the entry-lambda
application very efficiently when the guard has been verified.
The guard on a call of wormhole is the conjunction of the guards on
the arguments conjoined with the guard on the body of the entry-lambda.
See wormhole-eval for a discussion of the guard on the
lambda-expression.
The functions wormhole-statusp, wormhole-entry-code, wormhole-data, set-wormhole-entry-code, set-wormhole-data,
and make-wormhole-status may be useful in manipulating entry codes and
data in the entry-lambda.
Note that you access and manipulate the wormhole's status in two different
ways depending on whether you're ``outside'' of the wormhole applying the
quoted lambda or ``inside'' the read-eval-print loop of the wormhole.
OUTSIDE (wormhole-eval): access via the value of the lambda
formal and set by returning the new status as the value of the lambda
body.
INSIDE (ld phase of wormhole): access via (@
wormhole-status), and set via (assign wormhole-status ...).
Pragmatic Advice on Designing a Wormhole: Suppose you are using wormholes
to implement some extra-logical utility. You must contemplate how you will
use your wormhole's status to store hidden information. You might be tempted
to exploit the entry code as part of the status. For example, you may think
of :ENTER as indicating that your utility is ``turned on'' and :SKIP
as indicating that your utility is ``turned off.'' We advise against such a
design. We recommend you base your decisions on the wormhole data. We
recommend that you set but not read the wormhole entry code to signal whether
you wish to enter a full-fledged wormhole. To use the entry code as a flag
overloads it and invites confusion when your facility is ``turned off'' but
you have to enter the wormhole for some reason.
For a behind-the-scenes description of how wormholes work, See wormhole-implementation.
Here are some sample situations handled by wormhole-eval and
wormhole. Let the wormhole in question be named DEMO. Initially
its status is NIL. The functions below all maintain the convention that
the status is either nil or of the form (:key . lst), where
:key is either :SKIP or :ENTER and lst is a true-list of
arbitrary objects. But since there is no way to prevent the user from
entering the DEMO wormhole interactively and doing something to the
status, this convention cannot be enforced. Thus, the functions below do what
we say they do, e.g., remember all the values of x ever seen, only if
they're the only functions messing with the DEMO status. On the other
hand, the guards of all the functions below can be verified. We have
explicitly declared that the guards on the functions below are to be verified,
to confirm that they can be. Guard verification is optional but wormholes
(and wormhole-eval in particular) are more efficient when guards have
been verified. All of the functions defined below return nil.
The examples below build on each other. If you really want to understand
wormholes we recommend that you evaluate each of the forms below, in the order
they are discussed.
Q. How do I create a wormhole that prints its status to the comment
window?
(defun demo-status ()
(declare (xargs :verify-guards t))
(wormhole-eval 'demo
'(lambda (whs)
(prog2$ (cw "DEMO status:~%~x0~%" whs)
whs))
nil))
Note above that after printing the status to the comment window we return
the new (unchanged) status whs. Had we just written the call of cw,
which returns nil, the function would print the status and then set it to
nil!
Q. How do I use a wormhole to collect every symbol, x, passed
to the function?
(defun demo-collect (x)
(declare (xargs :verify-guards t))
(wormhole-eval 'demo
'(lambda (whs)
(make-wormhole-status whs
(wormhole-entry-code whs)
(if (symbolp x)
(cons x (wormhole-data whs))
(wormhole-data whs))))
nil))
We could have also defined this function this way:
(defun demo-collect (x)
(declare (xargs :verify-guards t))
(if (symbolp x)
(wormhole-eval 'demo
'(lambda (whs)
(set-wormhole-data whs
(cons x (wormhole-data whs))))
nil)
nil))
Both versions always return nil and both versions collect into the
wormhole data field just the symbols x upon which demo-collect is
called.
Q. How do I use demo-collect? Below is a function that maps
over a list and computes its length. But it has been annotated with a call to
demo-collect on every element.
(defun my-len (lst)
(if (endp lst)
0
(+ 1
(prog2$ (demo-collect (car lst))
(my-len (cdr lst))))))
Thus, for example:
ACL2 !>(my-len '(4 temp car "Hi" rfix))
5
ACL2 !>(demo-status)
DEMO status:
(:ENTER RFIX CAR TEMP)
NIL
ACL2 !>
Q. How do I set the entry code to :ENTER or :SKIP
according to whether name is a member-equal of the list of things
seen so far? Note that we cannot check this condition outside the wormhole,
because it depends on the list of things collected so far. We make the
decision inside the lambda-expression. Note that we explicitly check
that the guard of member-equal is satisfied by the current wormhole
status, since we cannot rely on the invariant that no other function
interferes with the status of the DEMO wormhole. In the case that the
status is ``unexpected'' we act like the status is nil and set it to
(:SKIP . NIL).
(defun demo-set-entry-code (name)
(declare (xargs :verify-guards t))
(wormhole-eval 'demo
'(lambda (whs)
(if (true-listp (wormhole-data whs))
(set-wormhole-entry-code
whs
(if (member-equal name (wormhole-data whs))
:ENTER
:SKIP))
'(:SKIP . NIL)))
nil))
Thus
ACL2 !>(demo-set-entry-code 'monday)
NIL
ACL2 !>(demo-status)
DEMO status:
(:SKIP RFIX CAR TEMP)
NIL
ACL2 !>(demo-set-entry-code 'rfix)
NIL
ACL2 !>(demo-status)
DEMO status:
(:ENTER RFIX CAR TEMP)
NIL
ACL2 !>
Q. Suppose I want to collect every symbol and then, if the symbol
has an ABSOLUTE-EVENT-NUMBER property in the ACL2 logical world, print
the defining event with :pe and then enter an interactive loop; but if
the symbol does not have an ABSOLUTE-EVENT-NUMBER, don't print anything
and don't enter an interactive loop.
Here it is not important to know what ABSOLUTE-EVENT-NUMBER is; this
example just shows that we can use a wormhole to access the ACL2 logical
world, even in a function that does not take the state as an argument.
In the code below, we use wormhole instead of wormhole-eval,
because we might have to access the logical world and enter an interactive
loop. But for efficiency we do as much as we can inside the entry
lambda, where we can check whether x is symbol and collect it into
the data field of the wormhole status. Note that if we collect x, we
also set the entry code to :ENTER. If we don't collect x, we set
the entry code to :SKIP.
(defun collect-symbols-and-print-events (x)
(declare (xargs :guard t))
(wormhole 'demo
'(lambda (whs)
(if (symbolp x)
(make-wormhole-status whs
:ENTER
(cons x (wormhole-data whs)))
(set-wormhole-entry-code whs :SKIP)))
; The wormhole will not get past here is unless the entry code is
; :ENTER. If we get past here, we manufacture a state, put
; x into (@ wormhole-input) and call ld in such a way that the
; first form executed is the quoted if-expression below.
x
'(if (getpropc (@ wormhole-input) 'absolute-event-number)
(er-progn
(mv-let (col state)
(fmt "~%Entering a wormhole on the event name ~x0~%"
(list (cons #\0 (@ wormhole-input)))
*standard-co* state nil)
(declare (ignore col))
(value nil))
(pe (@ wormhole-input))
(set-ld-prompt 'wormhole-prompt state)
(value :invisible))
(value :q))
:ld-verbose nil
:ld-prompt nil))
The ``first form'' (the if) asks whether the wormhole-input
(i.e., x) has an ABSOLUTE-EVENT-NUMBER property. If so, it enters
an er-progn to perform a sequence of commands, each of which returns
an ACL2 error triple (see programming-with-state). The first form uses
fmt to print a greeting. Since fmt returns (mv col state)
and we must return an error triple, we embed the fmt term in an
(mv-let (col state) ... (value nil)). The macro value takes an
object and returns a ``normal return'' error triple. The second form in the
er-progn uses the ACL2 history macro pe (see pe) to print the
defining event for a name. The third form sets the prompt of this
read-eval-print loop to the standard function for printing the wormhole
prompt. We silenced the printing of the prompt when we called ld, thanks
to the :ld-prompt nil keyword option. More on this below. The fourth
form returns the error triple value :invisible as the value of the first
form. This prevents ld from printing the value of the first form. Since
we have not exited ld, that function just continues by reading the next
form from the comment window. The user perceives this as entering a
read-eval-print loop. We continue in the loop until the user types
:q.
On the other branch of the if, if the symbol has no
ABSOLUTE-EVENT-NUMBER property, we execute the form (value :q),
which is the programming equivalent of typing :q. That causes the
ld to exit.
The ld special variables set in the call to wormhole and further
manipulated inside the first form to ld may require explanation. By
setting :ld-verbose to nil, we prevent ld from printing
the familiar ACL2 banner when ld is called. If :ld-verbose nil is
deleted, then you would see something like
ACL2 Version 4.0. Level 2.
...
Type (good-bye) to quit completely out of ACL2.
before the first form is read and evaluated.
By setting :ld-prompt to nil we prevent ld from
printing the prompt before reading and evaluating the first form.
As this example shows, to use full-blown wormholes you must understand the
protocol for using wormhole status to control whether a wormhole state is
manufactured for ld and you must also understand programming with state and the effects of the various ld ``special variables.''
From the discussion above we see that wormholes can be used to create
formatted output without passing in the ACL2 state. For examples see
cw, in particular the discussion at the end of that documentation
topic.
Subtopics
- Wormhole-eval
- State-saving without state — a short-cut to a parallel universe
- Wormhole-implementation
- Notes on how wormholes are implemented
- Make-wormhole-status
- Creates a wormhole status object from given status, entry code, and data
- Get-wormhole-status
- Make a wormhole's status visible outside the wormhole
- Set-wormhole-entry-code
- Sets the wormhole entry code in a wormhole status object
- Set-wormhole-data
- Sets the wormhole data object in a wormhole status object
- Wormhole-data
- Determines the wormhole data object from a wormhole status object
- Wormhole-statusp
- Predicate recognizing well-formed wormhole status object
- Wormhole-p
- Predicate to determine if you are inside a wormhole
- Wormhole-entry-code
- Determines the wormhole entry code from a wormhole status object
