WALKABOUT

explore an ACL2 cons tree
Major Section:  OTHER

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.

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 :