• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
    • Vwsim
    • Fgl
    • 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)