		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-*-h-char

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

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

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

Definitions and Theorems

Function: plex-*-h-char

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

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

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

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

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

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

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

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

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

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

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