Major Section: OTHER
(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
walkaboutloop, a positive integer n takes you to the nth position, while 0 takes you up a level. The commands
bktake you to the next and previous position, respectively, at the same level. The command
ppprints 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 n), so in particular
(pp nil)is equivalent to
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
(= 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
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,
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 :