Major Section: ACL2-BUILT-INS
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 macro whose calls expand to calls of
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.Also see cw!, which is useful if you want to be able to read the printed forms back in.
Finally, we discuss another way to create formatted output that also avoids
the need to pass in the ACL2 state. The idea is to use wormholes;
see wormhole. Below is a function you can write, along with some calls,
providing an illustration of this approach.
(defun my-fmt-to-comment-window (str alist)
(wormhole 'my-fmt-to-comment-window
'(lambda (whs) whs)
(list str alist)
'(pprogn
(fms (car (@ wormhole-input))
(cadr (@ wormhole-input))
*standard-co*
state
nil)
(value :q))
:ld-verbose nil
:ld-error-action :return ; harmless return on error
:ld-prompt nil))
; A non-erroneous call:
(my-fmt-to-comment-window "Here is ~x0 for your inspection~%"
(list (cons #\0 'foo)))
; An error inside the fmt string (unbound fmt var); note that even
; with the error, the wormhole is exited.
(my-fmt-to-comment-window "Here is ~x1 for your inspection~%"
(list (cons #\0 'foo)))
; A guard violation in the binding; note that even with the error,
; the wormhole is exited.
(my-fmt-to-comment-window "Here is ~x0 for your inspection~%"
(list (cons #\0 (car 'foo))))
