Major Section: PROGRAMMING
Example:
(cw "The goal is ~p0 and the alist is ~x1.~%"
(untranslate term t nil)
unify-subst)
Logically, this expression is equivalent to nil. However, it has
the effect of first printing to the so-called ``comment window'' the
fmt string as indicated. Thus, cw is like fmt (see fmt) except
in three important ways. First, it is a :logic mode function.
Second, it neither takes nor returns the ACL2 state; logically cw
simply returns nil, although it prints to a comment window that just
happens to share the terminal screen with the standard character
output *standard-co*. Third, its fmt args are positional
references, so that for example
(cw "Answers: ~p0 and ~p1" ans1 ans2)prints in the same manner as:
(fmt "Answers: ~p0 and ~p1"
(list (cons #\0 ans1) (cons #\1 ans2))
*standard-co* state nil)
Typically, calls of cw are embedded in prog2$ forms, e.g.,
(prog2$ (cw ...)
(mv a b c))
which has the side-effect of printing to the comment window and
logically returning (mv a b c).
General Form: (cw fmt-string arg1 arg2 ... argn)where n is between 0 and 9 (inclusive). The macro uses
fmt-to-comment-window, passing it the column 0 and
evisc-tuple nil, after assembling the appropriate alist binding the
fmt vars #\0 through #\9; see fmt. If you want
(a) more than 10 vars, (b) vars other than the digit chars, (c) a different column, or (d) a different evisc-tuple,then call
fmt-to-comment-window instead.
