		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lex-*-q-char

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

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

That is, lex a *q-char, in ABNF notation, i.e. a repetition of zero or more instances of q-char.

This is called when we expect a header name, after reading the opening double quote of a header name. If successful, this reads up to and including the closing double quote, and returns the position of the latter, along with the sequence of characters.

We read the next character; it is an error if there is none. It is also an error if the character is a new-line. If the character is a closing double quote, we end the recursion and return. In all other cases, we take the character as is, we read zero or more additional characters and escape sequences, and we combine them with the character.

Definitions and Theorems

Function: lex-*-q-char

(defun lex-*-q-char (parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (parstatep parstate)))
 (let ((__function__ 'lex-*-q-char))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil (irr-position) parstate)
    ((erp char pos parstate)
     (read-char parstate))
    ((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 parstate))
    ((when (utf8-= char 10))
     (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 parstate)
     (lex-*-q-char parstate)))
   (retok (cons qchar qchars)
          closing-dquote-pos parstate))))

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

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

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

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

Theorem: parstatep-of-lex-*-q-char.new-parstate

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

Theorem: parsize-of-lex-*-q-char-uncond

(defthm parsize-of-lex-*-q-char-uncond
  (b* (((mv acl2::?erp ?qchars
            ?closing-dquote-pos ?new-parstate)
        (lex-*-q-char parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-lex-*-q-char-cond

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