		Search-engine friendly clone of the ACL2 documentation.

Lex-strings

Vl-read-string-escape-sequence

Try to read a string escape sequence.

Signature
(vl-read-string-escape-sequence echars st) → (mv char/nil prefix remainder)
Arguments: echars — Characters we're lexing, starting with the leading backslash.
Guard (and (vl-echarlist-p echars) (consp echars) (equal (vl-echar->char (car echars)) #\\)) .; st — Governs which escape sequences are allowed.
Guard (vl-lexstate-p st).
Returns: char/nil — The interpretation of this escape sequence if any. This will be nil for line continuations, and also in case of any error.
Type (equal (characterp char/nil) (if char/nil t nil)).; prefix — The matched characters on success. You have to check the prefix rather than char/nil to determine success, because line continuations don't result in any character.

Definitions and Theorems

Function: vl-read-string-escape-sequence

(defun vl-read-string-escape-sequence (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-escape-sequence))
  (declare (ignorable __function__))
  (b* (((unless (consp (cdr echars)))
        (mv nil nil echars))
       (echar1 (first echars))
       (echar2 (second echars))
       (char2 (vl-echar->char echar2))
       ((when (eql char2 #\n))
        (mv #\Newline (list echar1 echar2)
            (cddr echars)))
       ((when (eql char2 #\t))
        (mv #\Tab (list echar1 echar2)
            (cddr echars)))
       ((when (eql char2 #\\))
        (mv #\\ (list echar1 echar2)
            (cddr echars)))
       ((when (eql char2 #\"))
        (mv #\" (list echar1 echar2)
            (cddr echars)))
       ((when (vl-echar-digit-value echar2 8))
        (vl-read-octal-string-escape echars))
       ((vl-lexstate st) st)
       ((unless st.strextsp)
        (mv nil nil echars))
       ((when (eql char2 #\Newline))
        (mv nil (list echar1 echar2)
            (cddr echars)))
       ((when (eql char2 #\v))
        (mv (vertical-tab-char)
            (list echar1 echar2)
            (cddr echars)))
       ((when (eql char2 #\f))
        (mv #\Page (list echar1 echar2)
            (cddr echars)))
       ((when (eql char2 #\a))
        (mv (code-char 7)
            (list echar1 echar2)
            (cddr echars)))
       ((when (eql char2 #\x))
        (vl-read-hex-string-escape echars))
       ((when (vl-string-self-escape-p char2))
        (mv char2 (list echar1 echar2)
            (cddr echars))))
   (mv
      (cw "Lexer error (~s0): invalid string escape sequence: ~s1~%"
          (vl-location-string (vl-echar->loc (car echars)))
          (vl-echarlist->string (list echar1 echar2)))
      nil echars))))

Theorem: return-type-of-vl-read-string-escape-sequence.char/nil

(defthm return-type-of-vl-read-string-escape-sequence.char/nil
  (b* (((mv ?char/nil ?prefix ?remainder)
        (vl-read-string-escape-sequence echars st)))
    (equal (characterp char/nil)
           (if char/nil t nil)))
  :rule-classes :rewrite)

Subtopics

Vl-string-self-escape-p: I'm not sure the standard really says this is OK, but it seems like these characters escape to themselves when preceded by a backslash on other tools.
Vl-read-string-escape-sequence-prefix/remainder-thms: Prefix and remainder theorems for vl-read-string-escape-sequence, automatically generated by def-prefix/remainder-thms.
Vl-string-self-escape-list-p: (vl-string-self-escape-list-p x) recognizes lists where every element satisfies vl-string-self-escape-p.