		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-*-hexadecimal-digit

Lex zero or more hexadecimal digits, as many as available, during preprocessing.

Signature
(plex-*-hexadecimal-digit pos-so-far ppstate) → (mv erp hexdigs last-pos next-pos new-ppstate)
Arguments: pos-so-far — Guard (positionp pos-so-far).; ppstate — Guard (ppstatep ppstate).
Returns: hexdigs — Type (hex-digit-char-listp hexdigs).; last-pos — Type (positionp last-pos).; next-pos — Type (positionp next-pos).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

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

Definitions and Theorems

Function: plex-*-hexadecimal-digit

(defun plex-*-hexadecimal-digit (pos-so-far ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (positionp pos-so-far)
                              (ppstatep ppstate))))
  (b* (((reterr)
        nil (irr-position)
        (irr-position)
        ppstate)
       ((erp char pos ppstate)
        (pread-char ppstate))
       ((when (not char))
        (retok nil (position-fix pos-so-far)
               pos ppstate))
       ((unless (or (and (utf8-<= (char-code #\0) char)
                         (utf8-<= char (char-code #\9)))
                    (and (utf8-<= (char-code #\A) char)
                         (utf8-<= char (char-code #\F)))
                    (and (utf8-<= (char-code #\a) char)
                         (utf8-<= char (char-code #\f)))))
        (b* ((ppstate (punread-char ppstate)))
          (retok nil (position-fix pos-so-far)
                 pos ppstate)))
       (hexdig (code-char char))
       ((erp hexdigs last-pos next-pos ppstate)
        (plex-*-hexadecimal-digit pos ppstate)))
    (retok (cons hexdig hexdigs)
           last-pos next-pos ppstate)))

Theorem: hex-digit-char-listp-of-plex-*-hexadecimal-digit.hexdigs

(defthm hex-digit-char-listp-of-plex-*-hexadecimal-digit.hexdigs
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-ppstate)
        (plex-*-hexadecimal-digit pos-so-far ppstate)))
    (hex-digit-char-listp hexdigs))
  :rule-classes :rewrite)

Theorem: positionp-of-plex-*-hexadecimal-digit.last-pos

(defthm positionp-of-plex-*-hexadecimal-digit.last-pos
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-ppstate)
        (plex-*-hexadecimal-digit pos-so-far ppstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: positionp-of-plex-*-hexadecimal-digit.next-pos

(defthm positionp-of-plex-*-hexadecimal-digit.next-pos
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-ppstate)
        (plex-*-hexadecimal-digit pos-so-far ppstate)))
    (positionp next-pos))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-*-hexadecimal-digit.new-ppstate

(defthm ppstatep-of-plex-*-hexadecimal-digit.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp ?hexdigs
                     ?last-pos ?next-pos ?new-ppstate)
                 (plex-*-hexadecimal-digit pos-so-far ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: true-listp-of-plex-*-hexadecimal-digit.hexdigs

(defthm true-listp-of-plex-*-hexadecimal-digit.hexdigs
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-ppstate)
        (plex-*-hexadecimal-digit pos-so-far ppstate)))
    (true-listp hexdigs))
  :rule-classes :type-prescription)

Theorem: ppstate->size-of-plex-*-hexadecimal-digit-uncond

(defthm ppstate->size-of-plex-*-hexadecimal-digit-uncond
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-ppstate)
        (plex-*-hexadecimal-digit pos-so-far ppstate)))
    (<= (ppstate->size new-ppstate)
        (- (ppstate->size ppstate)
           (len hexdigs))))
  :rule-classes :linear)