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), 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.
Note that the commands above work in any package: nx, bk,
pp, =, 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), 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 !>
Finally we describe the commands q, =, and (= symb), where
symb is a symbol. The command q simply causes an exit from the
walkabout loop. The command = also exits, but causes the current
object to be printed in full. 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.
:2
(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), and q.
(C D E . F)
:3
E
:nx
.
:nx
F
:0
(C D E . F)
:4
.
:0
(C D E . F)
:5
F
:
