		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lex-*-h-char

Lex zero or more characters in a header name between angle brackets.

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

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

This is called when we expect a header name, after reading the opening angle bracker of a header name. If successful, this reads up to and including the closing angle bracket, 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 angle bracket, 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-*-h-char

(defun lex-*-h-char (parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (parstatep parstate)))
 (let ((__function__ 'lex-*-h-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)))
    (hchar (h-char char))
    ((erp hchars closing-angle-pos parstate)
     (lex-*-h-char parstate)))
   (retok (cons hchar hchars)
          closing-angle-pos parstate))))

Theorem: h-char-listp-of-lex-*-h-char.hchars

(defthm h-char-listp-of-lex-*-h-char.hchars
  (b* (((mv acl2::?erp ?hchars
            ?closing-angle-pos ?new-parstate)
        (lex-*-h-char parstate)))
    (h-char-listp hchars))
  :rule-classes :rewrite)

Theorem: positionp-of-lex-*-h-char.closing-angle-pos

(defthm positionp-of-lex-*-h-char.closing-angle-pos
  (b* (((mv acl2::?erp ?hchars
            ?closing-angle-pos ?new-parstate)
        (lex-*-h-char parstate)))
    (positionp closing-angle-pos))
  :rule-classes :rewrite)

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

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

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

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

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

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