• 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-parse-tilde

    Signature
    (vl-basic-fmt-parse-tilde x n xl) → (mv type val n-prime)
    Arguments
    x — Format string we're parsing.
        Guard (stringp x).
    n — Current position in the format string.
        Guard (natp n).
    xl — Guard (eql xl (length x)).
    Returns
    val — Type (characterp val).
    n-prime — Type (natp n-prime).

    Valid types:

    • :SKIP means do not print anything, just skip until N-PRIME
    • :NORMAL means print VAL as normal text
    • :CBREAK means print a conditional break

    For any other directive, we assume the directive has the form

    ~[char2][char3]

    For instance, ~x0 would have:

    • char2 = #x and
    • char3 = #0

    For these directives, we return char2 as TYPE and char3 as VAL.

    Definitions and Theorems

    Function: vl-basic-fmt-parse-tilde

    (defun vl-basic-fmt-parse-tilde (x n xl)
     (declare (xargs :guard (and (stringp x)
                                 (natp n)
                                 (eql xl (length x)))))
     (declare (xargs :guard (< n xl)))
     (let ((__function__ 'vl-basic-fmt-parse-tilde))
      (declare (ignorable __function__))
      (b*
       ((n (lnfix n))
        (xl (lnfix xl))
        ((the character char1)
         (mbe :logic (char-fix (char x n))
              :exec (char x n)))
        ((when (not (eql char1 #\~)))
         (mv :normal char1 (+ n 1)))
        ((when (eql (+ n 1) xl))
         (prog2$ (raise "The format string ~x0 ends with a lone tilde."
                        x)
                 (mv :normal char1 (+ n 1))))
        ((the character char2)
         (mbe :logic (char-fix (char x (+ n 1)))
              :exec (char x (+ n 1))))
        ((when (eql char2 #\~))
         (mv :normal #\~ (+ n 2)))
        ((when (eql char2 #\%))
         (mv :normal #\Newline (+ n 2)))
        ((when (eql char2 #\Space))
         (mv :hard-space #\Space (+ n 2)))
        ((when (eql char2 #\|))
         (mv :cbreak #\Newline (+ n 2)))
        ((when (eql char2 #\Newline))
         (mv :skip
             #\Space (vl-skip-ws x (+ n 2) xl)))
        ((when (eql (+ n 2) xl))
         (prog2$
          (raise
           "The format string ~x0 ends with ~x1, but this directive needs argument."
           x (implode (list char1 char2)))
          (mv :normal char1 (+ n 1))))
        ((the character char3)
         (mbe :logic (char-fix (char x (+ n 2)))
              :exec (char x (+ n 2)))))
       (mv char2 char3 (+ n 3)))))

    Theorem: characterp-of-vl-basic-fmt-parse-tilde.val

    (defthm characterp-of-vl-basic-fmt-parse-tilde.val
      (b* (((mv common-lisp::?type ?val ?n-prime)
            (vl-basic-fmt-parse-tilde x n xl)))
        (characterp val))
      :rule-classes :type-prescription)

    Theorem: natp-of-vl-basic-fmt-parse-tilde.n-prime

    (defthm natp-of-vl-basic-fmt-parse-tilde.n-prime
      (b* (((mv common-lisp::?type ?val ?n-prime)
            (vl-basic-fmt-parse-tilde x n xl)))
        (natp n-prime))
      :rule-classes :type-prescription)

    Theorem: upper-bound-of-vl-basic-fmt-parse-tilde-nprime

    (defthm upper-bound-of-vl-basic-fmt-parse-tilde-nprime
      (implies (and (< (nfix n) (nfix xl)))
               (<= (mv-nth 2 (vl-basic-fmt-parse-tilde x n xl))
                   (nfix xl)))
      :rule-classes ((:rewrite) (:linear)))

    Theorem: lower-bound-of-vl-basic-fmt-parse-tilde-nprime

    (defthm lower-bound-of-vl-basic-fmt-parse-tilde-nprime
      (< (nfix n)
         (mv-nth 2 (vl-basic-fmt-parse-tilde x n xl)))
      :rule-classes ((:rewrite) (:linear)))

    Theorem: vl-basic-fmt-parse-tilde-of-str-fix-x

    (defthm vl-basic-fmt-parse-tilde-of-str-fix-x
      (equal (vl-basic-fmt-parse-tilde (str-fix x)
                                       n xl)
             (vl-basic-fmt-parse-tilde x n xl)))

    Theorem: vl-basic-fmt-parse-tilde-streqv-congruence-on-x

    (defthm vl-basic-fmt-parse-tilde-streqv-congruence-on-x
      (implies (streqv x x-equiv)
               (equal (vl-basic-fmt-parse-tilde x n xl)
                      (vl-basic-fmt-parse-tilde x-equiv n xl)))
      :rule-classes :congruence)

    Theorem: vl-basic-fmt-parse-tilde-of-nfix-n

    (defthm vl-basic-fmt-parse-tilde-of-nfix-n
      (equal (vl-basic-fmt-parse-tilde x (nfix n) xl)
             (vl-basic-fmt-parse-tilde x n xl)))

    Theorem: vl-basic-fmt-parse-tilde-nat-equiv-congruence-on-n

    (defthm vl-basic-fmt-parse-tilde-nat-equiv-congruence-on-n
      (implies (acl2::nat-equiv n n-equiv)
               (equal (vl-basic-fmt-parse-tilde x n xl)
                      (vl-basic-fmt-parse-tilde x n-equiv xl)))
      :rule-classes :congruence)