		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-identifier

Lex an identifier during preprocessing.

Signature
(plex-identifier first-char first-pos ppstate) → (mv erp lexeme span new-ppstate)
Arguments: first-char — Guard (unsigned-byte-p 8 first-char).; first-pos — Guard (positionp first-pos).; ppstate — Guard (ppstatep ppstate).
Returns: lexeme — Type (plexemep lexeme).; span — Type (spanp span).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

This is quite similar to lex-identifier/keyword, except that there are no keywords to consider during preprocessing, just identifiers.

Like lex-identifier/keyword, this is called after the first character of the identifier has been already read; that character is passed to this function. The position of that character is also passed as input.

Definitions and Theorems

Function: plex-identifier-loop

(defun plex-identifier-loop (pos-so-far ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (positionp pos-so-far)
                              (ppstatep ppstate))))
  (b* (((reterr) nil (irr-position) ppstate)
       ((erp char pos ppstate)
        (pread-char ppstate))
       ((when (not char))
        (retok nil (position-fix pos-so-far)
               ppstate))
       ((unless (or (and (utf8-<= (char-code #\A) char)
                         (utf8-<= char (char-code #\Z)))
                    (and (utf8-<= (char-code #\a) char)
                         (utf8-<= char (char-code #\z)))
                    (and (utf8-<= (char-code #\0) char)
                         (utf8-<= char (char-code #\9)))
                    (utf8-= char (char-code #\_))))
        (b* ((ppstate (punread-char ppstate)))
          (retok nil (position-fix pos-so-far)
                 ppstate)))
       ((erp chars last-pos ppstate)
        (plex-identifier-loop pos ppstate)))
    (retok (cons char chars)
           last-pos ppstate)))

Theorem: return-type-of-plex-identifier-loop.chars

(defthm return-type-of-plex-identifier-loop.chars
  (b* (((mv acl2::?erp
            ?chars ?last-pos ?new-ppstate)
        (plex-identifier-loop pos-so-far ppstate)))
    (unsigned-byte-listp 8 chars))
  :rule-classes :rewrite)

Theorem: positionp-of-plex-identifier-loop.last-pos

(defthm positionp-of-plex-identifier-loop.last-pos
  (b* (((mv acl2::?erp
            ?chars ?last-pos ?new-ppstate)
        (plex-identifier-loop pos-so-far ppstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-identifier-loop.new-ppstate

(defthm ppstatep-of-plex-identifier-loop.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp
                     ?chars ?last-pos ?new-ppstate)
                 (plex-identifier-loop pos-so-far ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-identifier-loop-uncond

(defthm ppstate->size-of-plex-identifier-loop-uncond
  (b* (((mv acl2::?erp
            ?chars ?last-pos ?new-ppstate)
        (plex-identifier-loop pos-so-far ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Function: plex-identifier

(defun plex-identifier (first-char first-pos ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (unsigned-byte-p 8 first-char)
                              (positionp first-pos)
                              (ppstatep ppstate))))
  (declare
       (xargs :guard (or (and (utf8-<= (char-code #\A) first-char)
                              (utf8-<= first-char (char-code #\Z)))
                         (and (utf8-<= (char-code #\a) first-char)
                              (utf8-<= first-char (char-code #\z)))
                         (utf8-= first-char (char-code #\_)))))
  (b* (((reterr)
        (irr-plexeme)
        (irr-span)
        ppstate)
       ((erp rest-chars last-pos ppstate)
        (plex-identifier-loop first-pos ppstate))
       (span (make-span :start first-pos
                        :end last-pos))
       (chars (cons first-char rest-chars))
       (string (nats=>string chars)))
    (retok (plexeme-ident (ident string))
           span ppstate)))

Theorem: plexemep-of-plex-identifier.lexeme

(defthm plexemep-of-plex-identifier.lexeme
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-identifier first-char first-pos ppstate)))
    (plexemep lexeme))
  :rule-classes :rewrite)

Theorem: spanp-of-plex-identifier.span

(defthm spanp-of-plex-identifier.span
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-identifier first-char first-pos ppstate)))
    (spanp span))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-identifier.new-ppstate

(defthm ppstatep-of-plex-identifier.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
                 (plex-identifier first-char first-pos ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-identifier-uncond

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