		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-header-name

Lex a header name during preprocessing.

Signature
(plex-header-name ppstate) → (mv erp lexeme span new-ppstate)
Arguments: ppstate — Guard (ppstatep ppstate).
Returns: lexeme — Type (plexemep lexeme).; span — Type (spanp span).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

This is the same as lex-header-name, but it operates on preprocessor states instead of parser states, and it returns a lexeme instead of a header name.

Definitions and Theorems

Function: plex-header-name

(defun plex-header-name (ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (ppstatep ppstate)))
 (let ((__function__ 'plex-header-name))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-plexeme)
        (irr-span)
        ppstate)
       ((erp char first-pos ppstate)
        (pread-char ppstate)))
   (cond
    ((not char)
     (reterr-msg
      :where (position-to-msg first-pos)
      :expected
      "a greater-than ~
                             or a double quote"
      :found (char-to-msg char)))
    ((utf8-= char (char-code #\<))
     (b* (((erp hchars closing-angle-pos ppstate)
           (plex-*-h-char ppstate))
          (span (make-span :start first-pos
                           :end closing-angle-pos))
          ((unless hchars)
           (reterr-msg :where (position-to-msg closing-angle-pos)
                       :expected "one or more characters"
                       :found "none")))
       (retok (plexeme-header (header-name-angles hchars))
              span ppstate)))
    ((utf8-= char (char-code #\"))
     (b* (((erp qchars closing-dquote-pos ppstate)
           (plex-*-q-char ppstate))
          (span (make-span :start first-pos
                           :end closing-dquote-pos))
          ((unless qchars)
           (reterr-msg :where (position-to-msg closing-dquote-pos)
                       :expected "one or more characters"
                       :found "none")))
       (retok (plexeme-header (header-name-quotes qchars))
              span ppstate)))
    (t
     (reterr-msg
      :where (position-to-msg first-pos)
      :expected
      "a greater-than ~
                             or a double quote"
      :found (char-to-msg char)))))))

Theorem: plexemep-of-plex-header-name.lexeme

(defthm plexemep-of-plex-header-name.lexeme
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-header-name ppstate)))
    (plexemep lexeme))
  :rule-classes :rewrite)

Theorem: spanp-of-plex-header-name.span

(defthm spanp-of-plex-header-name.span
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-header-name ppstate)))
    (spanp span))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-header-name.new-ppstate

(defthm ppstatep-of-plex-header-name.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
                 (plex-header-name ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-header-name-uncond

(defthm ppstate->size-of-plex-header-name-uncond
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-header-name ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-plex-header-name-cond

(defthm ppstate->size-of-plex-header-name-cond
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-header-name ppstate)))
    (implies (not erp)
             (<= (ppstate->size new-ppstate)
                 (1- (ppstate->size ppstate)))))
  :rule-classes :linear)