		Search-engine friendly clone of the ACL2 documentation.

Lex-strings

Vl-read-string-aux

Main loop for reading string literals.

Signature
(vl-read-string-aux echars eacc vacc st) → (mv error eacc vacc remainder)
Arguments: echars — Characters we're reading.
Guard (vl-echarlist-p echars).; eacc — Accumulator for actual characters read (e.g., #\n), as extended characters.; vacc — Accumulator for interpreted characters read (e.g., a newline), as ordinary characters.; st — Guard (vl-lexstate-p st).
Returns: error — nil on success, stringp error message on failure.
Type (equal (stringp error) (if error t nil)).; eacc — Type (vl-echarlist-p eacc), given (and (force (vl-echarlist-p echars)) (force (vl-echarlist-p eacc))).; vacc — Type (character-listp vacc), given (and (force (vl-echarlist-p echars)) (force (character-listp vacc))).; remainder — Type (vl-echarlist-p remainder), given (force (vl-echarlist-p echars)).

Definitions and Theorems

Function: vl-read-string-aux

(defun vl-read-string-aux (echars eacc vacc st)
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (vl-lexstate-p st))))
 (let ((__function__ 'vl-read-string-aux))
   (declare (ignorable __function__))
   (b* (((unless (consp echars))
         (mv "the file ends before the string is closed."
             eacc vacc echars))
        (echar1 (first echars))
        ((the character char1)
         (vl-echar->char echar1))
        ((when (eql char1 #\"))
         (mv nil (cons echar1 eacc)
             vacc (rest echars)))
        ((when (eql char1 #\Newline))
         (mv "the line ends before the string is closed."
             eacc vacc echars))
        ((when (eql char1 #\\))
         (b* (((mv char prefix remainder)
               (vl-read-string-escape-sequence echars st))
              ((unless prefix)
               (mv "the string contains an invalid escape sequence."
                   eacc vacc echars))
              (eacc (revappend prefix eacc))
              (vacc (if char (cons char vacc) vacc)))
           (vl-read-string-aux remainder eacc vacc st))))
     (vl-read-string-aux (cdr echars)
                         (cons echar1 eacc)
                         (cons char1 vacc)
                         st))))

Theorem: return-type-of-vl-read-string-aux.error

(defthm return-type-of-vl-read-string-aux.error
  (b* (((mv common-lisp::?error
            ?eacc ?vacc ?remainder)
        (vl-read-string-aux echars eacc vacc st)))
    (equal (stringp error)
           (if error t nil)))
  :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-read-string-aux.eacc

(defthm vl-echarlist-p-of-vl-read-string-aux.eacc
  (implies (and (force (vl-echarlist-p echars))
                (force (vl-echarlist-p eacc)))
           (b* (((mv common-lisp::?error
                     ?eacc ?vacc ?remainder)
                 (vl-read-string-aux echars eacc vacc st)))
             (vl-echarlist-p eacc)))
  :rule-classes :rewrite)

Theorem: character-listp-of-vl-read-string-aux.vacc

(defthm character-listp-of-vl-read-string-aux.vacc
  (implies (and (force (vl-echarlist-p echars))
                (force (character-listp vacc)))
           (b* (((mv common-lisp::?error
                     ?eacc ?vacc ?remainder)
                 (vl-read-string-aux echars eacc vacc st)))
             (character-listp vacc)))
  :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-read-string-aux.remainder

(defthm vl-echarlist-p-of-vl-read-string-aux.remainder
  (implies (force (vl-echarlist-p echars))
           (b* (((mv common-lisp::?error
                     ?eacc ?vacc ?remainder)
                 (vl-read-string-aux echars eacc vacc st)))
             (vl-echarlist-p remainder)))
  :rule-classes :rewrite)

Theorem: vl-read-string-aux-of-nil

(defthm vl-read-string-aux-of-nil
  (implies (atom echars)
           (mv-nth 0
                   (vl-read-string-aux echars eacc vacc st))))

Theorem: true-listp-of-vl-read-string-aux.eacc

(defthm true-listp-of-vl-read-string-aux.eacc
 (equal
      (true-listp (mv-nth 1
                          (vl-read-string-aux echars eacc vacc st)))
      (true-listp eacc)))

Theorem: true-listp-of-vl-read-string-aux.remainder

(defthm true-listp-of-vl-read-string-aux.remainder
 (equal
      (true-listp (mv-nth 3
                          (vl-read-string-aux echars eacc vacc st)))
      (true-listp echars)))

Theorem: revappend-of-vl-read-string-aux

(defthm revappend-of-vl-read-string-aux
 (equal
     (append (rev (mv-nth 1
                          (vl-read-string-aux echars eacc vacc st)))
             (mv-nth 3
                     (vl-read-string-aux echars eacc vacc st)))
     (append (rev eacc) echars)))

Theorem: acl2-count-of-vl-read-string-aux-weak

(defthm acl2-count-of-vl-read-string-aux-weak
  (<= (acl2-count (mv-nth 3
                          (vl-read-string-aux echars eacc vacc st)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-read-string-aux-strong

(defthm acl2-count-of-vl-read-string-aux-strong
 (implies
   (not (mv-nth 0
                (vl-read-string-aux echars eacc vacc st)))
   (< (acl2-count (mv-nth 3
                          (vl-read-string-aux echars eacc vacc st)))
      (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))