Fmt
Formatted printing
ACL2 provides the functions fmt, fmt1, and fms
as substitutes for Common Lisp's format function. Also see fmt!,
see fmt1!, and see fms! for versions of these functions that
write forms to files in a manner that allows them to be read, by avoiding
using backslash (\) to break long lines. There are also analogues of
these functions that return a string without taking state as an
argument; see printing-to-strings. A convenient macro, fmx, is
described below; also see cw and see fmx-cw.
All three print a given string under an alist pairing character objects
with values, interpreting certain ``tilde-directives'' in the string.
Channel must be a character output channel (e.g., *standard-co*).
General Forms: result
(fms string alist channel state evisc-tuple) ; state
(fmt string alist channel state evisc-tuple) ; (mv col state)
(fmt1 string alist column channel state evisc-tuple) ; (mv col state)
Fms and fmt print an initial newline to put channel in
column 0; Fmt1 requires the current column as input. Columns are
numbered from 0. The current column is the column into which the next
character will be printed. (Thus, the current column number is also the
number of characters printed since the last newline.) The col
returned by fmt and fmt1 is the current column at the conclusion
of the formatting. Evisc-tuple must be either nil (meaning no
abbreviations are used when objects are printed) or an ``evisceration tuple'';
see evisc-tuple.
We list the tilde-directives below. The notation is explained after the
chart.
~xx pretty print vx (maybe after printing a newline)
~yx pretty print vx starting in current column; end with newline
~Xxy like ~xx but use vy as the evisceration tuple
~Yxy like ~yx but use vy as the evisceration tuple
~@x if vx is a string, "str", recursively format "str"
if vx is ("str" . a), recursively format "str" under a+
~#x~[...~/...~/ ... ~/...~] cases on vx
^ ^ ... ^ if 0<=vx<=k, choose vxth alternative
0 1 ... k if vx is a list of length 1, case 0; else 1
~*x iterator: vx must be of the form
("str0" "str1" "str2" "str3" lst . a);
if lst is initially empty, format "str0" under a+; otherwise,
bind #\* successively to the elements of lst and then
recursively format "stri" under a+, where i=1 if there is one
element left to process, i=2 if there are two left, and i=3
otherwise.
~&x print elements of vx with ~x, separated by commas and a
final ``and''
~vx print elements of vx with ~x, separated by commas and a
final ``or''
~nx if vx is a small positive integer, print it as a word, e.g.,
seven;
if vx is a singleton containing a small positive integer, print
the corresponding ordinal as a word, e.g., seventh
~Nx like ~nx but the word is capitalized, e.g., Seven or Seventh
~tx tab out to column vx; newline first if at or past column vx
~cx vx is (n . w), print integer n right justified in field of
width w
~fx print object vx flat over as many lines as necessary
~Fx same as ~f, except that subsequent lines are indented to
start one character to the right of the first character printed
~sx if vx is a symbol, print vx, breaking on hyphens (unless the
symbol would normally be printed with surrounding vertical bar
characters (|), in which case print as with ~fx); if vx is a
string, print the characters in it, breaking on hyphens; else
vx is a number, to be printed using the current print-base and
print-radix
~Sx same as ~s, except that margins are ignored (hence no breaking on
hyphens and no breaking when the column exceeds the value of
the hard right-margin)
~ tilde space: print a space
~_x print vx spaces
~
tilde newline: skip following whitespace
~% output a newline
~| output a newline unless already on left margin
~~ print a tilde
~- if close to right margin, output a hyphen and newline; else
skip this char
If x is a character, then vx is the value of #\x under the
current alist. Consider for example the discussion above for ~y,
``~yx pretty print vx'', applied to the following expression: (fmt
"HELLO ~y7" (list (cons #\7 'world)) *standard-co* state nil). Then in
this example: #\x is 7; and vx is the value of character #\7
under the given alist, which is the symbol, WORLD. Thus, ACL2 will print
HELLO WORLD. When we say ``format str under a+'' we mean:
process the given string under an alist obtained by appending a to the
current alist. The following example illustrates how this works.
ACL2 !>(fms "~@0"
(list (cons #\0 (cons "~x0 ~@1" (list (cons #\0 'abc))))
(cons #\1 "-- and now: ~x0 again~%"))
*standard-co* state nil)
ABC -- and now: ABC again
<state>
ACL2 !>
Note: ~p, ~q, ~P, and ~Q are also currently supported,
but are deprecated and generally avoided in this manual. These are
respectively the same as ~x, ~y, ~X, and ~Y, except that
their arguments may be expected to be terms, preferably
untranslated (user-level) terms, since at one time there was the possibility
that they could be printed using infix notation in certain environments.
Infix printing is no longer supported, however.
ACL2's formatting functions print to the indicated channel, keeping track
of which column they are in. Fmt1 can be used if the caller knows
which column the channel is in (i.e., how many characters have been
printed since the last newline). Otherwise, fmt or fms must be
used, both of which output a newline so as to establish the column position at
0. Unlike Common Lisp's format routine, fmt and its relatives
break the output into lines so that, by default, an attempt is made to avoid
printing past column 77 (the value of constant
*fmt-hard-right-margin-default*), except when using ~S. See set-fmt-hard-right-margin for a discussion of how linebreaks are inserted and
how to change the relevant default settings. A right margin of 40 is used for
pretty printing with ~y, ~Y, ~q, and ~Q and can be changed
to a positive integer N with (set-ppr-flat-right-margin N
state).
The formatting functions scan the string from left to right, printing each
successive character unless it is a tilde (~). Upon encountering tildes
the formatters take action determined by the character or characters
immediately following the tilde. The typical tilde-directive is a group of
three successive characters from the string being printed. For
example, ~x0 is a 3 character tilde-directive. The first character
in a tilde-directive is always the tilde character itself. The next character
is called the ``command'' character. The character after that is usually
taken as the name of a ``format variable'' that is bound in the alist under
which the string is being printed. Format variables are, by necessity, characters. The objects actually printed by a tilde-directive are the
objects obtained by looking up the command's format variables in the alist.
Typical format variable names are 0, 1, 2, ..., 9, a,
b, c, etc., and if a tilde-directive uses the format variable
0, as in ~x0, then the character #\0 must be bound in the
alist. Some tilde commands take no arguments and others take more than one,
so some directives are of length two and others are longer.
It should be noted that this use of characters in the string to
denote arguments is another break from Common Lisp's format routine. In
Common Lisp, the directives refer implicitly to the ``next item to be
printed.'' But in ACL2 the directives name each item explicitly with our
format variables.
The following text contains examples that can be evaluated. To make this
process easier, we use a macro, fmx. It takes up to eleven arguments,
the first of which is a format string, str, and the others of which are
taken as the values of format variables; for similar utilities that do not
take or return state, see cw and fmx-cw. The variables
used are #\0 through #\9. The macro constructs an appropriate
alist, a, and then evaluates (fmt` str a 0 *standard-co* state
nil).
Thus,
(fmx "~%Here is v0, ~x0, and here is v1, ~x1."
(cons 'value 0)
(cons 'value 1))
is just an abbreviation for
(fmt1 "~%Here is v0, ~x0, and here is v1, ~x1."
(list (cons #\0 (cons 'value 0))
(cons #\1 (cons 'value 1)))
0
*standard-co*
state
nil)
which returns (mv 53 state) after printing, on a separate line,
Here is v0, (VALUE . 0), and here is v1, (VALUE . 1).
We now devote special attention to three of the tilde-directives whose use
is non-obvious.
The Case Statement
~#x is essentially a ``case statement'' in the language of fmt.
The proper form of the statement is
~#x~[case-0~/case-1~/ ... ~/case-k~],
where each of the case-i is a format string. In the most common use,
the variable x has an integer value, vx, between 0 and k,
inclusive. The effect of formatting the directive is to format
case-vx.
For example
(fmx "Go ~#0~[North~/East~/South~/West~].~%" 1)
will print ``Go East.'' followed by a newline and will return
(mv 0 state), while if you change the 1 above to 3 (the
maximum legal value), it will print ``Go West.''
In order to make it easier to print such phrases as ``there are seven
cases'' requiring agreement between subject and verb based on the number of
elements of a list, the case statement allows its variable to take a list as
its value and selects case-0 if the list has length 1 and
case-1 otherwise.
(let ((cases '(a b c)))
(fmx "There ~#0~[is ~n1 case~/are ~n1 cases~]."
cases
(length cases)))
will print ``There are three cases.'' but if you change the
'(a b c) above simply to '(a) it will print ``There is one
case.'' and if you change it to nil it will print ``There are zero
cases.''
Indirection
Roughly speaking, ~@ will act as though the value of its argument is a
format string and splice it into the current string at the current position.
It is often used when the phrase to be printed must be computed. For
example,
(let ((ev 'DEFUN))
(fmx "~x0 is an event~@1."
'foo
(if (member-eq ev '(defun defstub encapsulate))
" that may introduce a function symbol"
"")))
will print ``foo is an event that may introduce a function symbol,''
but if the value of ev is changed from 'defun to
'defthm, it prints ``foo is an event.'' The ~@
directive ``splices'' in the computed phrase (which might be empty). Of
course, this particular example could be done with the case statement
~#1~[~/ that may introduce a function symbol~]
where the value of #\1 is appropriately computed to be 0 or
1.
If the argument to ~@ is a pair, it is taken to be a format string
consed onto an alist, i.e., ("str" . a), and the alist, a,
is used to extend the current one before "str" is recursively
processed. This feature of fmt can be used to pass around ``phrases''
that contain computed contextual information in a. The most typical use
is as ``error messages.'' For example, suppose you are writing a function
which does not have access to state and so cannot print an error
message. It may nevertheless be necessary for it to signal an error to its
caller, say by returning two results, the first of which is interpreted as an
error message if non-nil. Our convention is to use a ~@ pair to
represent such messages. For example, the error value might be produced by
the code:
(cons
"Error: The instruction ~x0 is illegal when the stack is ~x1.~%"
(list (cons #\0 (current-instruction st))
(cons #\1 (i-stack st))))
If the current-instruction and i-stack (whatever they are) are
'(popi 3) and '(a b) when the cons above is evaluated, then
it produces
'("Error: The instruction ~x0 is illegal when the stack is ~x1.~%"
(#\0 POPI 3)
(#\1 A B))
and if this pair is made the value of the fmt variable 0, then
~@0 will print
Error: The instruction (POPI 3) is illegal when the stack is (A B).
For example, evaluate
(let
((pair
'("~%Error: The instruction ~x0 is illegal when the stack is ~x1.~%"
(#\0 POPI 3)
(#\1 A B))))
(fmx "~@0" pair)).
Thus, even though the function that produced the ``error'' could not print
it, it could specify exactly what error message and data are to be
printed.
This example raises another issue. Sometimes it is desirable to break
lines in your format strings so as to make your source code more attractive.
That is the purpose of the tilde-newline directive. The following code
produces exactly the same output as described above.
(let ((pair '("Error: The instruction ~x0 ~
is illegal when the stack is ~
~x1.~%"
(#\0 POPI 3)
(#\1 A B))))
(fmx "~%~@0" pair)).
Finally, observe that when ~@0 extends the current alist, alist,
with the one, a, in its argument, the bindings from a are added to
the front of alist, overriding the current values of any shared
variables. This ensures that the variable values seen by the recursively
processed string, "str", are those from a, but if "str"
uses variables not bound in a, their values are as specified in the
original alist. Intuitively, variables bound in a are local to the
processing of ("str" . a) but "str" may use ``global
variables.'' The example above illustrates this because when the ~@0 is
processed, #\0 is bound to the error message pair. But when the
~x0 in the error string is processed, #\0 is bound to the illegal
instruction.
Iteration
The ~* directive is used to process each element of a list. For
example,
(let ((lst '(a b c d e f g h))) ; a true-list whose elements we exhibit
(fmx "~*0"
`("Whoa!" ; what to print if there's nothing to print
"~x*!" ; how to print the last element
"~x* and " ; how to print the 2nd to last element
"~x*, " ; how to print all other elements
,lst))) ; the list of elements to print
will print ``A, B, C, D, E, F, G and H!''. Try this example with
other true list values of lst, such as '(a b), '(a), and
nil. The tilde-directives ~&0 and ~v0, which take a true list
argument and display its elements separated by commas and a final ``and'' or
``or,'' are implemented in terms of the more general ~*.
The ~* directive allows the 5-tuple to specify in its final cdr an alist with which to extend the current one before processing the
individual elements.
We often use ~* to print a series of phrases, separated by suitable
punctuation, whitespace and noise words. In such use, the ~* handles the
separation of the phrases and each phrase is generally printed by ~@.
Here is a complex example. In the let*, below, we bind phrases to
a list of ~@ pairs and then we create a ~* 5-tuple to print out the
conjunction of the phrases with a parenthetical ``finally!'' if the series is
longer than 3.
(let* ((phrases
(list (list "simplifying with the replacement rules ~&0"
(cons #\0 '(rewrite-rule1
rewrite-rule2
rewrite-rule3)))
(list "destructor elimination using ~x0"
(cons #\0 'elim-rule))
(list "generalizing the terms ~&0"
(cons #\0 '((rev x) (app u v))))
(list "inducting on ~x0"
(cons #\0 'I))))
(5-tuple
(list
"magic" ; no phrases
"~@*" ; last phrase
"~@*, and~#f~[~/ (finally!)~] " ; second to last phrase
"~@*, " ; other phrases
phrases ; the phrases themselves
(cons #\f
(if (>(length phrases) 3) 1 0))))) ;print ``finally''?
(fmx "We did it by ~*0." 5-tuple))
This let* prints
We did it by simplifying with the replacement rules REWRITE-RULE1,
REWRITE-RULE2 and REWRITE-RULE3, destructor elimination using ELIM-
RULE, generalizing the terms (REV X) and (APP U V), and (finally!)
inducting on I.
You might wish to try evaluating the let* after removing elements
of phrases.
Most of the output produced by ACL2 is produced via fmt statements.
Thus, inspection of the source code will yield many examples. A complicated
example is the code that explains the simplifier's work. See :pc
simplify-clause-msg1. An ad hoc example is provided by the function
fmt-doc-example, which takes two arguments: an arbitrary true list and
state. To see how fmt-doc-example works, :pe
fmt-doc-example.
(fmt-doc-example '(a b c d e f g h i j k l m n o p) state)
will produce the output
Here is a true list: (A B C D E F G H I J K L M N O P). It has 16
elements, the third of which is C.
We could print each element in square brackets:
([A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N],
[almost there: O], [the end: P]). And if we wished to itemize them
into column 15 we could do it like this
0123456789012345
0 (zeroth) A
1 (first) B
2 (second) C
3 (third) D
4 (fourth) E
5 (fifth) F
6 (sixth) G
7 (seventh)
H
8 (eighth) I
9 (ninth) J
10 (tenth) K
11 (eleventh)
L
12 (twelfth)
M
13 (thirteenth)
N
14 (14th) O
15 (15th) P
End of example.
and return (mv 15 state).
Finally, we should remind the reader that fmt and its subfunctions,
most importantly fmt0, are written entirely in ACL2. We make this
comment for two reasons. First, it illustrates the fact that quite low level
code can be efficiently written in the language. Second, it means that as a
last resort for documentation purposes you can read the source code without
changing languages.
