		Search-engine friendly clone of the ACL2 documentation.

Formatted-printing

Vl-basic-fmt

Basic fmt-like printing function for ps.

Signature
(vl-basic-fmt x alist &key (ps 'ps)) → ps
Arguments: x — Guard (stringp x).; alist — Guard (alistp alist).

(vl-basic-fmt x alist &key (ps 'ps)) takes as inputs x, a format string as described in formatted-printing, and an alist that should map characters to objects, which provides the arguments to the format string, as in ordinary fmt-style ACL2 printing.

Definitions and Theorems

Function: vl-basic-fmt-fn

(defun vl-basic-fmt-fn (x alist ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (and (stringp x) (alistp alist))))
  (let ((__function__ 'vl-basic-fmt))
    (declare (ignorable __function__))
    (let ((x (string-fix x)))
      (vl-basic-fmt-aux x 0 (length x)
                        alist))))

Theorem: vl-basic-fmt-fn-of-str-fix-x

(defthm vl-basic-fmt-fn-of-str-fix-x
  (equal (vl-basic-fmt-fn (str-fix x) alist ps)
         (vl-basic-fmt-fn x alist ps)))

Theorem: vl-basic-fmt-fn-streqv-congruence-on-x

(defthm vl-basic-fmt-fn-streqv-congruence-on-x
  (implies (streqv x x-equiv)
           (equal (vl-basic-fmt-fn x alist ps)
                  (vl-basic-fmt-fn x-equiv alist ps)))
  :rule-classes :congruence)

Subtopics

Vl-basic-fmt-parse-tilde
Vl-skip-ws: Skip past whitespace in a string.
Vl-basic-fmt-aux: Core loop for printing format strings.
Vl-fmt-tilde-x
Vl-fmt-print-space
Vl-fmt-tilde-&
Vl-fmt-tilde-s
Vl-fmt-print-normal