		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-*-q-char

Lex zero or more characters in a header name between double quotes, during preprocessing.

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

This is the same as lex-*-q-char, but it operates on preprocessor states instead of parser states.

Definitions and Theorems

Function: plex-*-q-char

(defun plex-*-q-char (ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (ppstatep ppstate)))
 (let ((__function__ 'plex-*-q-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
      "any character other than ~
                               greater-than 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
      "any character other than ~
                               greater-than or new-line"
      :found (char-to-msg char)))
    (qchar (q-char char))
    ((erp qchars closing-dquote-pos ppstate)
     (plex-*-q-char ppstate)))
   (retok (cons qchar qchars)
          closing-dquote-pos ppstate))))

Theorem: q-char-listp-of-plex-*-q-char.qchars

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

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

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

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

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

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

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

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

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