		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-*-s-char

Lex zero or more characters and escape sequences in a string literal, during preprocessing.

Signature
(plex-*-s-char ppstate) → (mv erp schars closing-dquote-pos new-ppstate)
Arguments: ppstate — Guard (ppstatep ppstate).
Returns: schars — Type (s-char-listp schars).; closing-dquote-pos — Type (positionp closing-dquote-pos).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

This is the same as lex-*-s-char, but it operates on preprocessor states instead of parser states, and we exclude CR besides LF.

Definitions and Theorems

Function: plex-*-s-char

(defun plex-*-s-char (ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (ppstatep ppstate)))
 (let ((__function__ 'plex-*-s-char))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil (irr-position) ppstate)
    ((erp char pos ppstate)
     (pread-char ppstate))
    ((unless char)
     (reterr-msg
      :where (position-to-msg pos)
      :expected
      "an escape sequence or ~
                               any character other than ~
                               double quote or backslash"
      :found (char-to-msg char)))
    ((when (utf8-= char (char-code #\")))
     (retok nil pos ppstate))
    ((when (or (utf8-= char 10) (utf8-= char 13)))
     (reterr-msg
      :where (position-to-msg pos)
      :expected
      "an escape sequence or ~
                               any character other than ~
                               double quote or backslash"
      :found (char-to-msg char)))
    ((erp schar & ppstate)
     (if (utf8-= char (char-code #\\))
         (b* (((erp escape pos ppstate)
               (plex-escape-sequence ppstate))
              (schar (s-char-escape escape)))
           (retok schar pos ppstate))
       (b* ((schar (s-char-char char)))
         (retok schar pos ppstate))))
    ((erp schars closing-dquote-pos ppstate)
     (plex-*-s-char ppstate)))
   (retok (cons schar schars)
          closing-dquote-pos ppstate))))

Theorem: s-char-listp-of-plex-*-s-char.schars

(defthm s-char-listp-of-plex-*-s-char.schars
  (b* (((mv acl2::?erp ?schars
            ?closing-dquote-pos ?new-ppstate)
        (plex-*-s-char ppstate)))
    (s-char-listp schars))
  :rule-classes :rewrite)

Theorem: positionp-of-plex-*-s-char.closing-dquote-pos

(defthm positionp-of-plex-*-s-char.closing-dquote-pos
  (b* (((mv acl2::?erp ?schars
            ?closing-dquote-pos ?new-ppstate)
        (plex-*-s-char ppstate)))
    (positionp closing-dquote-pos))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-*-s-char.new-ppstate

(defthm ppstatep-of-plex-*-s-char.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp ?schars
                     ?closing-dquote-pos ?new-ppstate)
                 (plex-*-s-char ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-*-s-char-uncond

(defthm ppstate->size-of-plex-*-s-char-uncond
  (b* (((mv acl2::?erp ?schars
            ?closing-dquote-pos ?new-ppstate)
        (plex-*-s-char ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-plex-*-s-char-cond

(defthm ppstate->size-of-plex-*-s-char-cond
  (b* (((mv acl2::?erp ?schars
            ?closing-dquote-pos ?new-ppstate)
        (plex-*-s-char ppstate)))
    (implies (not erp)
             (<= (ppstate->size new-ppstate)
                 (1- (- (ppstate->size ppstate)
                        (len schars))))))
  :rule-classes :linear)