• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
          • Ps
          • Basic-printing
          • Verilog-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
            • Vl-printedlist
            • Json-printing
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • 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)