PRINTING-TO-STRINGS

Major Section:  IO

Each of ACL2's formatted printing functions, FM*, has an analoguous macro FM*-TO-STRING indicated below. These functions do not include a channel or state as an argument, and FM*-TO-STRING returns the string that FM* would print to the state, in place of state; see fmt. The legal keyword arguments are described below.

General Forms:                                 result
(fms-to-string string alist &key ...)          ; string
(fmt-to-string string alist &key ...)          ; (mv col string)
(fmt1-to-string string alist column &key ...)  ; (mv col string)
(fms!-to-string string alist &key ...)         ; string
(fmt!-to-string string alist &key ...)         ; (mv col string)
(fmt1!-to-string string alist column &key ...) ; (mv col string)

The legal keyword arguments are as follows. They are all optional with a default of nil.

Evisc-tuple is evaluated, and corresponds exactly to the evisc-tuple argument of the corresponding FM* function; see fmt.

Fmt-control-alist should typically evaluate to an alist that maps print-control variables to values; see print-control. Any alist mapping variables to values is legal, however. By default the print controls are set according to the value of constant *fmt-control-defaults*; fmt-control-alist overrides these defaults. For example, *fmt-control-defaults* sets the right margin just as it is set in the initial ACL2 state, by binding fmt-soft-right-margin and fmt-hard-right-margin to their respective defaults of *fmt-soft-right-margin-default* and *fmt-hard-right-margin-default*. The following example shows how you can override those defaults, in this case arranging to print flat by setting the right margin to a large number.

(fmt-to-string "~x0"
               (list (cons #\0 (make-list 30)))
               :fmt-control-alist
               `((fmt-soft-right-margin . 10000)
                 (fmt-hard-right-margin . 10000)))

Iprint is typically nil, but t is also a legal value. See set-iprint for the effect of value t, which however is local to this call of a FM*-TO-STRING function; the behavior if iprinting afterwards is not affected by this call. In particular, you will not be able to look at the values of iprint tokens printed by this call, so the value t is probably of limited utility at best.

Also see io for a discussion of the utility get-output-stream-string$, which allows for accumulating the results of more than one printing call into a single string but requires the use of state.