		Search-engine friendly clone of the ACL2 documentation.

Printing-to-strings

Printing to strings instead of files or standard output

Each of ACL2's formatted printing functions, FM*, has an analogous 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)))

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.

Remarks on deviation from the fmt functions.

The evisc-table is ignored by these functions that print to strings. Use the :evisc-tuple keyword instead.
Iprinting is turned off during evaluation of calls of these functions, even if it is enabled globally. The reason is that for each iprint index, i, that is bound during creation of the result string, that binding would disappear after the string is returned; so it would be misleading or an error to read #@i# after that return.
The following remark is subtle; see fmt! for relevant background. By default, there is identical behavior for each pair of functions of the form fm<..>-to-string and fm<..>!-to-string: both functions act like the fm<..>! function, which is to say, they both avoid printing a backslash (\) when the right margin is exceeded, so that the results can be read by ACL2. If you include the pair (:WRITE-FOR-READ NIL) in :fmt-control-alist, then the fm<..>-to-string functions will be free to insert such backslashes; but that pair will have no effect on the fm<..>!-to-string functions.