		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-*-c-char

Lex zero or more characters and escape sequences in a character constant, during preprocessing.

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

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

Definitions and Theorems

Function: plex-*-c-char

(defun plex-*-c-char (ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (ppstatep ppstate)))
 (let ((__function__ 'plex-*-c-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 ~
                               single quote or backslash or new-line"
      :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 ~
                               single quote or backslash or new-line"
      :found (char-to-msg char)))
    ((erp cchar & ppstate)
     (if (utf8-= char (char-code #\\))
         (b* (((erp escape pos ppstate)
               (plex-escape-sequence ppstate))
              (cchar (c-char-escape escape)))
           (retok cchar pos ppstate))
       (b* ((cchar (c-char-char char)))
         (retok cchar pos ppstate))))
    ((erp cchars closing-squote-pos ppstate)
     (plex-*-c-char ppstate)))
   (retok (cons cchar cchars)
          closing-squote-pos ppstate))))

Theorem: c-char-listp-of-plex-*-c-char.cchars

(defthm c-char-listp-of-plex-*-c-char.cchars
  (b* (((mv acl2::?erp ?cchars
            ?closing-squote-pos ?new-ppstate)
        (plex-*-c-char ppstate)))
    (c-char-listp cchars))
  :rule-classes :rewrite)

Theorem: positionp-of-plex-*-c-char.closing-squote-pos

(defthm positionp-of-plex-*-c-char.closing-squote-pos
  (b* (((mv acl2::?erp ?cchars
            ?closing-squote-pos ?new-ppstate)
        (plex-*-c-char ppstate)))
    (positionp closing-squote-pos))
  :rule-classes :rewrite)

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

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

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

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

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

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