Walkabout
Explore an ACL2 cons tree
By typing (walkabout x state) for an ACL2 term x whose
value is a cons tree, you can walk around that tree. For example,
ACL2 developers often use this utility to explore the ACL2 logical world.
When you issue a walkabout command, a summary of commands will be
printed before you enter an interactive loop.
Commands:
1, 2, ..., up, nx, bk, pp, (pp n), (pp lev len), =, (= symb),
(cmds c1 c2 ... cn), and q.
In the interactive walkabout loop, a positive integer n takes you to
the nth position, while up takes you up a level. The commands nx
and bk take you to the next and previous position, respectively, at the
same level. The command pp prints the current object in full, while
(pp level length) hides sub-objects below the indicated level and past
the indicated length, if non-nil; see evisc-tuple. The command
(pp n) abbreviates (pp n n), so in particular (pp nil) is
equivalent to pp. The commands = and cmds are described
below.
Note that the commands above work in any package: up, nx,
bk, pp, =, cmds, and q are converted to the
"ACL2" package if the current package is not "ACL2". Also, as a
convenience, the single character 0 is accepted as equivalent to
up.
The following example illustrates the commands described above.
ACL2 !>(walkabout (append '(a (b1 b2 b3)) '(c d e f)) state)
Commands:
1, 2, ..., up, nx, bk, pp, (pp n), (pp lev len), =, (= symb),
(cmds c1 c2 ... cn), and q.
(A (B1 B2 B3) C ...)
:2
(B1 B2 B3)
:3
B3
:up
(B1 B2 B3)
:nx
C
:nx
D
:up
(A (B1 B2 B3) C ...)
:pp
(A (B1 B2 B3) C D E F)
:(pp 4)
(A (B1 B2 B3) C D ...)
:(pp 1 4)
(A # C D ...)
:(pp nil 2)
(A (B1 B2 ...) ...)
:q
ACL2 !>
The command (cmds c1 c2 ... cn) just executes each of the ci,
sequentially.
The command q simply causes an exit from the
walkabout loop.
The command = also exits, but returns the current object as the value in
an ACL2 error-triple.
The command (= symb) saves an association of symb with the
current object, which can be retrieved outside the walkabout loop using
the macro walkabout=, as illustrated below.
...
:pp
(B1 B2 B3)
:(= my-list)
(walkabout= MY-LIST) is
(B1 B2 B3)
:q
ACL2 !>(walkabout= MY-LIST)
(B1 B2 B3)
ACL2 !>
Finally, we remark that for trees that are not true-lists, walkabout
treats the dot as an object that can be ``walked about''. The following
example illustrates this point.
ACL2 !>(walkabout '(c d e . f) state)
Commands:
1, 2, ..., up, nx, bk, pp, (pp n), (pp lev len), =, (= symb),
(cmds c1 c2 ... cn), and q.
(C D E . F)
:3
E
:nx
.
:nx
F
:up
(C D E . F)
:4
.
:up
(C D E . F)
:5
F
:
