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 :
