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) when in the wormhole. This is
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 it is modified while in the wormhole and we 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, named brr, to implement the break-rewrite 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 wormhole, wormhole-eval, or set-persistent-whs-and-ephemeral-whs is called. However, it is forbidden to
invoke these functions on any name 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.
Every wormhole name has a ``status.'' The status of a wormhole is stored
outside of ACL2 at a location known to hold the ``persistent wormhole status''
or ``persistent-whs'' of that wormhole. Before wormhole enters its
read-eval-print loop the persistent-whs is assigned to the state global
variable wormhole-status and so while inside the wormhole the status is
available as (@ wormhole-status). Wormhole-status is untouchable:
you cannot change it directly as with (assign wormhole-status ...). But
the persistent-whs can be changed, e.g., with wormhole,
wormhole-eval, or set-persistent-whs-and-ephemeral-whs. See wormhole-status for a discussion of the ramifications of there being two
places a wormhole's status might be found and of the importance of the notion
of ``wormhole coherence.''
Upon the first call on name of wormhole (or the other wormhole creator
functions mentioned above) 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
by set in the form argument of wormhole using
set-persistent-whs-and-ephemeral-whs or sync-ephemeral-whs-with-persistent-whs.
The car of the status should be either :ENTER or :SKIP and
is called the wormhole's ``entry code.'' The entry code of nil or,
indeed, of any value other than :SKIP is treated as thought it were
:ENTER. The cdr of the status is arbitrary data maintained by the
author of the wormhole.
When the wormhole is exited — typically because the form :q was
read by ld — the then-current ephemeral-whs (i.e., (@
wormhole-status)) is moved to the persistent-whs so that it can be restored
when this wormhole is entered again. (Note: The break-rewrite wormhole,
brr, is handled differently. When it is exited back to the top-level,
the persistent-whs is set to what it was when ACL2 was last at the top-level.)
The rest of the wormhole state is lost upon exit.
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) and may be assigned with assign.
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 exit the wormhole.
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 persistent-whs with wormhole-eval.
That lambda application must produce a new wormhole status, which is
stored as the wormhole's new persistent-whs. 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 :SKIP the wormhole state is
not manufactured; the new persistent-whs is merely saved and wormhole
returns nil. Otherwise, a new state is manufactured and 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.
See wormhole-programming-tips for some advice about using wormholes,
maintaining (or not maintaining) coherence, etc.
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. The wormhole in question will be named demo and it is
created in the answer to the first question below. 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 initialize the status of the demo wormhole?
Actually, it is often unnecessary to explicitly initialize the status of a
new wormhole because it is nil by default, the wormhole-entry-code of nil is :enter and the wormhole-data
of nil is nil, which often is enough. But if the data field of your
wormhole needs more structure for whatever you're planning to do with it to
make sense, you can initialize it by executing a form like this, where the
nil below is the contents of the initial data field.
ACL2 !>(wormhole-eval 'demo
'(lambda (whs) (make-wormhole-status whs :enter nil))
nil)
NIL
ACL2 !>(get-persistent-whs 'demo state)
(:ENTER)
Q. How do I define a function that prints the (persistent) status of
the demo wormhole 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 the prog2$ above. After printing the status to the comment
window we return the unchanged status whs. Had we just written the
cw term, which returns nil, without then returning whs, the
function would print the status and then set it to nil!
Q. How can I define a function, demo-collect, that does not
take or return state but that can collect every symbol passed to
it (but not collect non-symbols)?
(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. Note that the lambda expressions used in both definitions
mention x as a free variable.
Q. How do I use demo-collect? Below we show an interactive
session log with demo-collect and demo-status. Notice that
state is nowhere involved but that the functions always return nil.
The computation, collection, and printing are done inside the wormhole.
ACL2 !>(demo-status)
DEMO status:
(:ENTER)
NIL
ACL2 !>(demo-collect 'a)
NIL
ACL2 !>(demo-status)
DEMO status:
(:ENTER A)
NIL
ACL2 !>(demo-collect 'b)
NIL
ACL2 !>(demo-collect 'c)
NIL
ACL2 !>(demo-status)
DEMO status:
(:ENTER C B A)
NIL
Q. How do I reset the data to nil?
The answer is the same as the answer to the first question, use
wormhole-eval as we did there. But we'll repeat it as a session
log because in the next question we want the data field to start off at nil
again.
ACL2 !>(wormhole-eval 'demo
'(lambda (whs) (make-wormhole-status whs :enter nil))
nil)
NIL
ACL2 !>(demo-status)
DEMO status:
(:ENTER)
NIL
Q. How can I use demo-collect in a function? 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. We illustrate a
call below.
(defun my-len (lst)
(if (endp lst)
0
(+ 1
(prog2$ (demo-collect (car lst))
(my-len (cdr lst))))))
Thus, for example, if we call my-len on a list of length 5 it
returns 5 but accumulates the symbols into the demo wormhole,
without state. From a logical perspective my-len is just len
and that can be proved trivially.
ACL2 !>(my-len '(4 temp car "Hi" fix))
5
ACL2 !>(demo-status)
DEMO status:
(:ENTER FIX CAR TEMP)
NIL
ACL2 !>(thm (equal (my-len x) (len x)))
...
Proof succeeded.
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 data,
since we cannot rely on the invariant that no other function interferes with
the status of the demo wormhole. In the case that the data is not a
true-list we act like the data is nil and set the status 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 FIX CAR TEMP)
NIL
ACL2 !>(demo-set-entry-code 'fix)
NIL
ACL2 !>(demo-status)
DEMO status:
(:ENTER FIX CAR TEMP)
NIL
ACL2 !>
We won't be using demo-set-entry-code again in these questions and
answers, so don't spend time learning more about it!
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 demo-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, wormhole will 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~%~
Exit with :q~%~%"
(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'' — so called because it is the first form executed
by the wormhole's read-eval-print loop — is the quoted
if-expression in the fourth argument of wormhole. It asks whether
the wormhole-input
(i.e., x) has an absolute-event-number property.
The true branch of that if is 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 and being prompted
for input. We continue in the loop until the user types :q.
The false branch of the if is taken when x 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.
every time 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.''
Had we defined demo-collect-symbols-and-print-events before my-len
we could have called it instead of demo-collect. Then
ACL2 !>(my-len '(4 temp car "Hi" fix))
would have still collected all the symbols into the demo wormhole, but
on the symbols car and fix it would have entered an interactive
break. Here is the break that would be triggered when this version of
my-len encounters the fix.
Entering a wormhole on the event name FIX
Exit with :q
V -8055 (DEFUN FIX (X)
(DECLARE (XARGS :GUARD T :MODE :LOGIC))
(IF (ACL2-NUMBERP X) X 0))
Wormhole ACL2 !>(fix 123)
123
Wormhole ACL2 !>(fix t)
0
Wormhole ACL2 !>:q
After printing the (DEFUN FIX ...) above the user in this session
called fix twice to see how it behaves. Then the user issued the :q
command to exit the interactive loop, allowing my-len to continue. When
my-len finishes processing the list, it would return 5.
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-status
- the two senses of a wormhole's status
- Wormhole-programming-tips
- some tips for how to use wormholes
- Wormhole-implementation
- Notes on how wormholes are implemented
- Sync-ephemeral-whs-with-persistent-whs
- establishing wormhole coherence
- Get-persistent-whs
- Make a wormhole's status visible outside the wormhole
- Set-persistent-whs-and-ephemeral-whs
- maintaining wormhole coherence
- Make-wormhole-status
- Creates a wormhole status object from given status, entry code, and data
- 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-entry-code
- Determines the wormhole entry code 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
