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:
0, 1, 2, ..., 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 0 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: nx, bk,
pp, =, cmds, and q are converted to the "ACL2"
package if the current package is not "ACL2".
The following example illustrates the commands described above.
ACL2 !>(walkabout (append '(a (b1 b2 b3)) '(c d e f)) state)
Commands:
0, 1, 2, ..., 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
:0
(B1 B2 B3)
:nx
C
:nx
D
:0
(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:
0, 1, 2, ..., nx, bk, pp, (pp n), (pp lev len), =, (= symb),
(cmds c1 c2 ... cn), and q.
(C D E . F)
:3
E
:nx
.
:nx
F
:0
(C D E . F)
:4
.
:0
(C D E . F)
:5
F
:
