		Search-engine friendly clone of the ACL2 documentation.

Lex-strings

Vl-read-hex-string-escape

Try to read a \xdd string escape.

Signature
(vl-read-hex-string-escape echars) → (mv char/nil prefix remainder)
Arguments: echars — Characters we're lexing, starting with the leading backslash.
Guard (and (vl-echarlist-p echars) (consp echars) (consp (cdr echars)) (eql (vl-echar->char (first echars)) #\\)) .
Returns: char/nil — The character indicated by this hex sequence on success, or nil if this is not a valid escape sequence.
Type (equal (characterp char/nil) (if char/nil t nil)).; prefix — Type (iff prefix char/nil).

Definitions and Theorems

Function: vl-read-hex-string-escape

(defun vl-read-hex-string-escape (echars)
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (consp echars)
                             (consp (cdr echars))
                             (eql (vl-echar->char (first echars))
                                  #\\))))
 (let ((__function__ 'vl-read-hex-string-escape))
  (declare (ignorable __function__))
  (b*
   ((echar1 (first echars))
    (echar2 (second echars))
    ((unless (eql (vl-echar->char echar2) #\x))
     (mv nil nil echars))
    ((unless (consp (cddr echars)))
     (mv
      (cw
       "Lexer error (~s0): EOF during string escape sequence: ~s1<EOF>~%"
       (vl-location-string (vl-echar->loc (car echars)))
       (vl-echarlist->string (list echar1 echar2)))
      nil echars))
    (echar3 (third echars))
    ((when (or (vl-z-digit-echar-p echar3)
               (vl-x-digit-echar-p echar3)))
     (mv
      (cw
       "Lexer error (~s0): invalid string escape sequence: ~s1 ~
                  (x/z/? aren't allowed after \\x)~%"
       (vl-location-string (vl-echar->loc (car echars)))
       (vl-echarlist->string (list echar1 echar2 echar3)))
      nil echars))
    (val3 (vl-echar-digit-value echar3 16))
    ((unless val3)
     (mv
      (cw
       "Lexer error (~s0): invalid string escape sequence: ~s1 ~
                  (hex digit required after \\x)~%"
       (vl-location-string (vl-echar->loc (car echars)))
       (vl-echarlist->string (list echar1 echar2 echar3)))
      nil echars))
    ((unless (consp (cdddr echars)))
     (mv
      (cw
       "Lexer error (~s0): EOF during string escape sequence: ~s1<EOF>~%"
       (vl-location-string (vl-echar->loc (car echars)))
       (vl-echarlist->string (list echar1 echar2 echar3)))
      nil echars))
    (echar4 (fourth echars))
    ((when (or (vl-z-digit-echar-p echar4)
               (vl-x-digit-echar-p echar4)))
     (mv
      (cw
       "Lexer error (~s0): invalid string escape sequence: ~s1 ~
                  (x/z/? aren't allowed after \\x)~%"
       (vl-location-string (vl-echar->loc (car echars)))
       (vl-echarlist->string (list echar1 echar2 echar3 echar4)))
      nil echars))
    (val4 (vl-echar-digit-value echar4 16))
    ((unless val4)
     (mv (code-char val3)
         (list echar1 echar2 echar3)
         (cdddr echars))))
   (mv (code-char (the (unsigned-byte 8)
                       (+ (the (unsigned-byte 8)
                               (* 16 (the (unsigned-byte 8) val3)))
                          (the (unsigned-byte 8)
                               (the (unsigned-byte 8) val4)))))
       (list echar1 echar2 echar3 echar4)
       (cddddr echars)))))

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

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

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

(defthm return-type-of-vl-read-hex-string-escape.prefix
  (b* (((mv ?char/nil ?prefix ?remainder)
        (vl-read-hex-string-escape echars)))
    (iff prefix char/nil))
  :rule-classes :rewrite)

Subtopics

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