Msg
Construct a ``message'' suitable for the ~@ directive of fmt
See fmt for background on formatted printing with ACL2.
In short: for a call (msg s arg0 arg1 arg2 ...), s should be a
string suitable as an argument to fmt and (arg0 arg1 arg2 ...)
should be the bindings of #\0, #\1, #\2, and so on. See
msgp for a weak recognizer of objects returned by msg. Now, for a
more careful explanation:
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 your
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).
