• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
        • Ps
        • Verilog-printing
        • Basic-printing
        • Printing-locally
        • Formatted-printing
          • Vl-basic-fmt
            • Vl-basic-fmt-parse-tilde
            • Vl-skip-ws
            • Vl-basic-fmt-aux
            • Vl-fmt-tilde-x
            • Vl-fmt-print-space
            • Vl-fmt-tilde-&
            • Vl-fmt-tilde-s
            • Vl-fmt-print-normal
          • Vl-basic-cw-obj
          • Vl-basic-cw
        • Accessing-printed-output
        • Json-printing
        • Vl-printedlist
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Vl-basic-fmt

Vl-basic-fmt-aux

Core loop for printing format strings.

Signature

(vl-basic-fmt-aux x n xl alist &key (ps 'ps)) → ps

Arguments

x — Guard (stringp x).

n — Guard (natp n).

xl — Guard (eql xl (length x)).

alist — Guard (alistp alist).

Definitions and Theorems

Function: vl-basic-fmt-aux-fn

(defun
 vl-basic-fmt-aux-fn (x n xl alist ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (and (stringp x)
                             (natp n)
                             (alistp alist)
                             (eql xl (length x)))))
 (declare (xargs :guard (<= n xl)))
 (let
  ((__function__ 'vl-basic-fmt-aux))
  (declare (ignorable __function__))
  (b*
   (((when (mbe :logic (zp (- (nfix xl) (nfix n)))
                :exec (eql xl n)))
     ps)
    ((mv type val n)
     (vl-basic-fmt-parse-tilde x n xl))
    (ps
     (case
      type (:skip ps)
      (:normal (vl-fmt-print-normal val))
      (:hard-space (vl-print #\Space))
      (:cbreak (if (zp (vl-ps->col))
                   ps (vl-println "")))
      (otherwise
       (b*
        ((lookup (assoc val alist))
         ((unless lookup)
          (prog2$
               (raise "alist does not bind ~x0; fmt-string is ~x1."
                      val x)
               ps)))
        (case
         type (#\s (vl-fmt-tilde-s (cdr lookup)))
         (#\& (vl-fmt-tilde-& (cdr lookup)))
         (#\x (vl-fmt-tilde-x (cdr lookup)))
         (otherwise
              (prog2$ (raise "Unsupported directive: ~~~x0.~%" type)
                      ps))))))))
   (vl-basic-fmt-aux x n xl alist))))

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

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

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

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

Theorem: vl-basic-fmt-aux-fn-of-nfix-n

(defthm vl-basic-fmt-aux-fn-of-nfix-n
        (equal (vl-basic-fmt-aux-fn x (nfix n)
                                    xl alist ps)
               (vl-basic-fmt-aux-fn x n xl alist ps)))

Theorem: vl-basic-fmt-aux-fn-nat-equiv-congruence-on-n

(defthm
     vl-basic-fmt-aux-fn-nat-equiv-congruence-on-n
     (implies (acl2::nat-equiv n n-equiv)
              (equal (vl-basic-fmt-aux-fn x n xl alist ps)
                     (vl-basic-fmt-aux-fn x n-equiv xl alist ps)))
     :rule-classes :congruence)