		Search-engine friendly clone of the ACL2 documentation.

Formatted-printing

Vl-basic-cw-obj

Like vl-basic-cw, but reads its format string from an object.

Signature
(vl-basic-cw-obj msg args &key (ps 'ps)) → ps
Arguments: msg — Guard (stringp msg).

Ordinariy, vl-basic-cw requires you to provide its arguments explicitly in the macro call. That is, you might write something like this:

(vl-basic-cw "foo is ~x0 and bar is ~x1.~%" foo bar)

With vl-basic-cw-obj, the arguments are instead expected to be a list, and this list is deconstructed to produce the alist to be given to vl-basic-fmt. For instance, to print the same text as above, we might write:

(vl-basic-cw-obj "foo is ~x0 and bar is ~x1~%" (list foo bar))

This is particularly useful for, e.g., warnings or other cases where you want to cons up a structure that can be printed, but not necessarily print it right away.

Definitions and Theorems

Function: vl-basic-cw-obj-fn

(defun vl-basic-cw-obj-fn (msg args ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (stringp msg)))
 (let ((__function__ 'vl-basic-cw-obj))
  (declare (ignorable __function__))
  (cond
    ((<= (len args) 10)
     (vl-basic-fmt
          msg
          (pairlis$ '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)
                    (list-fix args))))
    (t (progn$ (raise "vl-basic-cw-obj is limited to 10 arguments.")
               ps)))))

Theorem: vl-basic-cw-obj-fn-of-str-fix-msg

(defthm vl-basic-cw-obj-fn-of-str-fix-msg
  (equal (vl-basic-cw-obj-fn (str-fix msg)
                             args ps)
         (vl-basic-cw-obj-fn msg args ps)))

Theorem: vl-basic-cw-obj-fn-streqv-congruence-on-msg

(defthm vl-basic-cw-obj-fn-streqv-congruence-on-msg
  (implies (streqv msg msg-equiv)
           (equal (vl-basic-cw-obj-fn msg args ps)
                  (vl-basic-cw-obj-fn msg-equiv args ps)))
  :rule-classes :congruence)