~@ directive of fmt
Major Section: ACL2-BUILT-INS
See fmt for background on formatted printing with ACL2.
We document msg precisely below, but first, we give an informal
introduction and illustrate with an example. Suppose you are writing a
program that is to do some printing. Typically, you will either pass the
ACL2 state around (see programming-with-state) and use formatted printing
functions that take the state as an argument (see fmt)), or else you might
avoid using state by calling the utility, cw, to do you printing.
Alternatively, you might print error messages upon encountering illegal
situations; see er. But there are times where instead of printing
immediately, you may prefer to pass messages around, for example to
accumulate them before printing a final message. In such cases, it may be
desirable to construct ``message'' objects to pass around.
For example, consider the following pair of little programs. The first either performs a computation or prints an error, and the second calls the first on two inputs.
(defun invert1 (x)
(if (consp x)
(cons (cdr x) (car x))
(prog2$ (cw "ERROR: ~x0 expected a cons, but was given ~x1.~|"
'invert1 x)
nil)))
(defun invert2 (x1 x2)
(list (invert1 x1) (invert1 x2)))
For example:
ACL2 !>(invert1 '(3 . 4)) (4 . 3) ACL2 !>(invert1 'a) ERROR: INVERT1 expected a cons, but was given A. NIL ACL2 !>(invert2 '(3 . 4) '(5 . 6)) ((4 . 3) (6 . 5)) ACL2 !>(invert2 'a 'b) ERROR: INVERT1 expected a cons, but was given A. ERROR: INVERT1 expected a cons, but was given B. (NIL NIL) ACL2 !>Notice that when there are errors, there is no attempt to explain that these are due to a call of
invert2. That could be fixed, of course, by
arranging for invert2 to print its own error; but for complicated
programs it can be awkward to coordinate printing from many sources. So
let's try a different approach. This time, the first function returns two
results. The first result is an ``error indicator'' -- either a message
object or nil -- while the second is the computed value (only of
interest when the first result is nil). Then the higher-level function
can print a single error message that includes the error message(s) from the
lower-level function, as shown below.
(defun invert1a (x)
(if (consp x)
(mv nil
(cons (cdr x) (car x)))
(mv (msg "ERROR: ~x0 expected a cons, but was given ~x1.~|"
'invert1a x)
nil)))
(defun invert2a (x1 x2)
(mv-let (erp1 y1)
(invert1a x1)
(mv-let (erp2 y2)
(invert1a x2)
(if erp1
(if erp2
(cw "~x0 failed with two errors:~| ~@1 ~@2"
'invert2a erp1 erp2)
(cw "~x0 failed with one error:~| ~@1"
'invert2a erp1))
(if erp2
(cw "~x0 failed with one error:~| ~@1"
'invert2a erp2)
(list y1 y2))))))
For example:
ACL2 !>(invert2a '(3 . 4) '(5 . 6))
((4 . 3) (6 . 5))
ACL2 !>(invert2a '(3 . 4) 'b)
INVERT2A failed with one error:
ERROR: INVERT1A expected a cons, but was given B.
NIL
ACL2 !>(invert2a 'a 'b)
INVERT2A failed with two errors:
ERROR: INVERT1A expected a cons, but was given A.
ERROR: INVERT1A expected a cons, but was given B.
NIL
ACL2 !>
If you study the example above, you might well understand msg. But we
conclude with precise documentation.
General Form: (msg str arg1 ... argk)where
str is a string and k is at most 9.This macro returns a pair suitable for giving to the fmt directive
~@. Thus, suppose that #\c is bound to the value of
(msg str arg1 ... argk), where c is a character and k is at most
9. Then the fmt directive ~@c will print out the string, str,
in the context of the alist in which the successive fmt variables
#\0, #\1, ..., #\k are bound to the successive elements of
(arg1 ... argk).
