		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-escape-sequence

Lex an escape sequence during preprocessing.

Signature
(plex-escape-sequence ppstate) → (mv erp escape last-pos new-ppstate)
Arguments: ppstate — Guard (ppstatep ppstate).
Returns: escape — Type (escapep escape).; last-pos — Type (positionp last-pos).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

This is the same as lex-escape-sequence, but it operates on preprocessor states instead of parser states.

Definitions and Theorems

Function: plex-escape-sequence

(defun plex-escape-sequence (ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (ppstatep ppstate)))
 (let ((__function__ 'plex-escape-sequence))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-escape)
        (irr-position)
        ppstate)
       ((erp char pos ppstate)
        (pread-char ppstate)))
   (cond
    ((not char)
     (reterr-msg
      :where (position-to-msg pos)
      :expected
      "a single quote ~
                             or a double quote ~
                             or a question mark ~
                             or a backslash ~
                             or a letter in {a, b, f, n, r, t, v, u, U, x} ~
                             or an octal digit"
      :found (char-to-msg char)))
    ((utf8-= char (char-code #\'))
     (retok (escape-simple (simple-escape-squote))
            pos ppstate))
    ((utf8-= char (char-code #\"))
     (retok (escape-simple (simple-escape-dquote))
            pos ppstate))
    ((utf8-= char (char-code #\?))
     (retok (escape-simple (simple-escape-qmark))
            pos ppstate))
    ((utf8-= char (char-code #\\))
     (retok (escape-simple (simple-escape-bslash))
            pos ppstate))
    ((utf8-= char (char-code #\a))
     (retok (escape-simple (simple-escape-a))
            pos ppstate))
    ((utf8-= char (char-code #\b))
     (retok (escape-simple (simple-escape-b))
            pos ppstate))
    ((utf8-= char (char-code #\f))
     (retok (escape-simple (simple-escape-f))
            pos ppstate))
    ((utf8-= char (char-code #\n))
     (retok (escape-simple (simple-escape-n))
            pos ppstate))
    ((utf8-= char (char-code #\r))
     (retok (escape-simple (simple-escape-r))
            pos ppstate))
    ((utf8-= char (char-code #\t))
     (retok (escape-simple (simple-escape-t))
            pos ppstate))
    ((utf8-= char (char-code #\v))
     (retok (escape-simple (simple-escape-v))
            pos ppstate))
    ((and (utf8-= char (char-code #\%))
          (ppstate->gcc ppstate))
     (retok (escape-simple (simple-escape-percent))
            pos ppstate))
    ((and (utf8-<= (char-code #\0) char)
          (utf8-<= char (char-code #\7)))
     (b* (((erp char2 pos2 ppstate)
           (pread-char ppstate)))
      (cond
       ((and char2 (utf8-<= (char-code #\0) char2)
             (utf8-<= char2 (char-code #\7)))
        (b* (((erp char3 pos3 ppstate)
              (pread-char ppstate)))
         (cond
          ((and char3 (utf8-<= (char-code #\0) char3)
                (utf8-<= char3 (char-code #\7)))
           (retok (escape-oct (oct-escape-three (code-char char)
                                                (code-char char2)
                                                (code-char char3)))
                  pos3 ppstate))
          (t
            (b* ((ppstate (if char3 (punread-char ppstate)
                            ppstate)))
              (retok (escape-oct (oct-escape-two (code-char char)
                                                 (code-char char2)))
                     pos2 ppstate))))))
       (t (b* ((ppstate (if char2 (punread-char ppstate)
                          ppstate)))
            (retok (escape-oct (oct-escape-one (code-char char)))
                   pos ppstate))))))
    ((utf8-= char (char-code #\x))
     (b* (((erp hexdigs last-pos next-pos ppstate)
           (plex-*-hexadecimal-digit pos ppstate)))
       (if hexdigs (retok (escape-hex hexdigs)
                          last-pos ppstate)
         (reterr-msg :where (position-to-msg next-pos)
                     :expected "one or more hexadecimal digits"
                     :found "none"))))
    ((utf8-= char (char-code #\u))
     (b* (((erp quad pos ppstate)
           (plex-hex-quad ppstate)))
       (retok (escape-univ (univ-char-name-locase-u quad))
              pos ppstate)))
    ((utf8-= char (char-code #\U))
     (b* (((erp quad1 & ppstate)
           (plex-hex-quad ppstate))
          ((erp quad2 pos ppstate)
           (plex-hex-quad ppstate)))
      (retok
           (escape-univ (make-univ-char-name-upcase-u :quad1 quad1
                                                      :quad2 quad2))
           pos ppstate)))
    (t
     (reterr-msg
      :where (position-to-msg pos)
      :expected
      "a single quote ~
                             or a double quote ~
                             or a question mark ~
                             or a backslash ~
                             or a letter in {a, b, f, n, r, t, v, u, U, x} ~
                             or an octal digit"
      :found (char-to-msg char)))))))

Theorem: escapep-of-plex-escape-sequence.escape

(defthm escapep-of-plex-escape-sequence.escape
  (b* (((mv acl2::?erp
            ?escape ?last-pos ?new-ppstate)
        (plex-escape-sequence ppstate)))
    (escapep escape))
  :rule-classes :rewrite)

Theorem: positionp-of-plex-escape-sequence.last-pos

(defthm positionp-of-plex-escape-sequence.last-pos
  (b* (((mv acl2::?erp
            ?escape ?last-pos ?new-ppstate)
        (plex-escape-sequence ppstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-escape-sequence.new-ppstate

(defthm ppstatep-of-plex-escape-sequence.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp
                     ?escape ?last-pos ?new-ppstate)
                 (plex-escape-sequence ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-escape-sequence-uncond

(defthm ppstate->size-of-plex-escape-sequence-uncond
  (b* (((mv acl2::?erp
            ?escape ?last-pos ?new-ppstate)
        (plex-escape-sequence ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-plex-escape-sequence-cond

(defthm ppstate->size-of-plex-escape-sequence-cond
  (b* (((mv acl2::?erp
            ?escape ?last-pos ?new-ppstate)
        (plex-escape-sequence ppstate)))
    (implies (not erp)
             (<= (ppstate->size new-ppstate)
                 (1- (ppstate->size ppstate)))))
  :rule-classes :linear)