		Search-engine friendly clone of the ACL2 documentation.

Lex-strings

Vl-read-string

Signature
(vl-read-string echars st) → (mv str? prefix remainder)
Arguments: echars — Characters we're reading, which we assume begin with a double-quote.
Guard (and (vl-echarlist-p echars) (consp echars) (equal (vl-echar->char (car echars)) #\")) .; st — Guard (vl-lexstate-p st).
Returns: str? — NIL on failure. A stringp with the interpreted characters from the string literal otherwise. That is, we'll have already expanded things like \n into proper newline characters.
Type (equal (stringp str?) (if str? t nil)).; prefix — The matched characters, starting at the opening double quote and extending through the closing double quote, inclusively, on success.
Type (iff prefix str?).

Definitions and Theorems

Function: vl-read-string

(defun vl-read-string (echars st)
  (declare
       (xargs :guard (and (and (vl-echarlist-p echars)
                               (consp echars)
                               (equal (vl-echar->char (car echars))
                                      #\"))
                          (vl-lexstate-p st))))
  (let ((__function__ 'vl-read-string))
    (declare (ignorable __function__))
    (b* (((mv err eacc vacc remainder)
          (vl-read-string-aux (cdr echars)
                              nil nil st))
         ((when err)
          (mv (cw "Lexer error (~s0) while reading string: ~s1.~%"
                  (vl-location-string (vl-echar->loc (car echars)))
                  err)
              nil echars)))
      (mv (str::rchars-to-string vacc)
          (cons (car echars) (reverse eacc))
          remainder))))

Theorem: return-type-of-vl-read-string.str?

(defthm return-type-of-vl-read-string.str?
  (b* (((mv ?str? ?prefix ?remainder)
        (vl-read-string echars st)))
    (equal (stringp str?) (if str? t nil)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-read-string.prefix

(defthm return-type-of-vl-read-string.prefix
  (b* (((mv ?str? ?prefix ?remainder)
        (vl-read-string echars st)))
    (iff prefix str?))
  :rule-classes :rewrite)

Subtopics

Vl-read-string-prefix/remainder-thms: Prefix and remainder theorems for vl-read-string, automatically generated by def-prefix/remainder-thms.