		Search-engine friendly clone of the ACL2 documentation.

Lex-strings

Vl-read-octal-string-escape

Try to read a \ddd string escape.

Signature
(vl-read-octal-string-escape echars) → (mv char/nil prefix remainder)
Arguments: echars — Characters we're lexing. We know these start with a leading backslash, but we don't know what follows. For instance, we might be at a valid octal string escape like \123, or we might be at some other kind of escape like \n.
Guard (and (vl-echarlist-p echars) (consp echars) (consp (cdr echars)) (eql (vl-echar->char (first echars)) #\\)) .
Returns: char/nil — If we're at a valid octal sequence, the particular characterp indicated by that sequence.
Type (equal (characterp char/nil) (if char/nil t nil)).; prefix — Type (iff prefix char/nil).

This can fail for two reasons.

We might just be looking at some non-octal escape sequence like \n, which is fine and we'll fail without complaining about it.
We might encounter an invalid octal sequence, e.g., \378 or \40x. In this case, we'll print a message to standard output before failing.

BOZO consider revamping this to return an error msg instead of printing.

Definitions and Theorems

Function: vl-read-octal-string-escape

(defun vl-read-octal-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-octal-string-escape))
  (declare (ignorable __function__))
  (b*
   ((echar1 (first echars))
    (echar2 (second echars))
    (val2 (vl-echar-digit-value echar2 8))
    ((unless val2) (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, and ? digits aren't allowed here)~%"
       (vl-location-string (vl-echar->loc (car echars)))
       (vl-echarlist->string (list echar1 echar2 echar3)))
      nil echars))
    (val3 (vl-echar-digit-value echar3 8))
    ((unless val3)
     (mv (code-char val2)
         (list echar1 echar2)
         (cddr 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, and ? digits aren't allowed here)~%"
       (vl-location-string (vl-echar->loc (car echars)))
       (vl-echarlist->string (list echar1 echar2 echar3 echar4)))
      nil echars))
    (val4 (vl-echar-digit-value echar4 8))
    ((unless val4)
     (mv (code-char (the (unsigned-byte 8)
                         (+ (the (unsigned-byte 8)
                                 (* 8 (the (unsigned-byte 8) val2)))
                            (the (unsigned-byte 8) val3))))
         (list echar1 echar2 echar3)
         (cdddr echars)))
    ((the (unsigned-byte 12) value)
     (+ (the (unsigned-byte 12)
             (* 64 (the (unsigned-byte 8) val2)))
        (the (unsigned-byte 8)
             (+ (the (unsigned-byte 8)
                     (* 8 (the (unsigned-byte 8) val3)))
                (the (unsigned-byte 8) val4)))))
    ((unless (< value 256))
     (mv
      (cw
       "Lexer error (~s0): invalid escape sequence: ~s1. ~
                  (characters beyond \\377 aren't valid)~%"
       (vl-location-string (vl-echar->loc (car echars)))
       (vl-echarlist->string (list echar1 echar2 echar3 echar4)))
      nil echars)))
   (mv (code-char value)
       (list echar1 echar2 echar3 echar4)
       (cddddr echars)))))

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

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

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

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

Subtopics

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