		Search-engine friendly clone of the ACL2 documentation.

Cw

Print to the comment window

Cw is a macro that expands to a function whose guard is t. For a guarded variant of cw, see fmx-cw. For variants of cw that provide readable output (suffix "!") and are never inhibited (suffix "+"), see cw!, cw+, and cw!+. For corresponding functions see fmt-to-comment-window, fmt-to-comment-window!, fmt-to-comment-window+, and fmt-to-comment-window!+.

Example:

(cw "The goal is ~x0 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 four 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: ~x0 and ~x1" ans1 ans2)

prints in the same manner as:

(fmt "Answers: ~x0 and ~x1"
     (list (cons #\0 ans1) (cons #\1 ans2))
     *standard-co* state nil)

And finally, output from cw is suppressed if the COMMENT type of output is suppressed; see set-inhibit-output-lst.

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.

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))))

Subtopics

Fmt-to-comment-window: Print to the comment window
Cw!: Print readably to the comment window
Fmt-to-comment-window!: Print readably to the comment window
Fmt-to-comment-window!+: Print readably and uninhibited to the comment window
Fmt-to-comment-window+: Print uninhibited to the comment window
Cw!+: Print readably and uninhibited to the comment window
Cw+: Print uninhibited to the comment window