		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-hexadecimal-digit

Lex a hexadecimal digit during preprocessing.

Signature
(plex-hexadecimal-digit ppstate) → (mv erp hexdig pos new-ppstate)
Arguments: ppstate — Guard (ppstatep ppstate).
Returns: hexdig — Type (hex-digit-char-p hexdig).; pos — Type (positionp 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 (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (ppstatep ppstate)))
  (let ((__function__ 'plex-hexadecimal-digit))
    (declare (ignorable __function__))
    (b* (((reterr) #\0 (irr-position) ppstate)
         ((erp char pos ppstate)
          (pread-char ppstate))
         ((when (not char))
          (reterr-msg :where (position-to-msg pos)
                      :expected "a hexadecimal digit"
                      :found (char-to-msg char)))
         ((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)))))
          (reterr-msg :where (position-to-msg pos)
                      :expected "a hexadecimal digit"
                      :found (char-to-msg char))))
      (retok (code-char char) pos ppstate))))

Theorem: hex-digit-char-p-of-plex-hexadecimal-digit.hexdig

(defthm hex-digit-char-p-of-plex-hexadecimal-digit.hexdig
  (b* (((mv acl2::?erp
            ?hexdig acl2::?pos ?new-ppstate)
        (plex-hexadecimal-digit ppstate)))
    (hex-digit-char-p hexdig))
  :rule-classes :rewrite)

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

(defthm positionp-of-plex-hexadecimal-digit.pos
  (b* (((mv acl2::?erp
            ?hexdig acl2::?pos ?new-ppstate)
        (plex-hexadecimal-digit ppstate)))
    (positionp 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
                     ?hexdig acl2::?pos ?new-ppstate)
                 (plex-hexadecimal-digit ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

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

(defthm ppstate->size-of-plex-hexadecimal-digit-uncond
  (b* (((mv acl2::?erp
            ?hexdig acl2::?pos ?new-ppstate)
        (plex-hexadecimal-digit ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-plex-hexadecimal-digit-cond

(defthm ppstate->size-of-plex-hexadecimal-digit-cond
  (b* (((mv acl2::?erp
            ?hexdig acl2::?pos ?new-ppstate)
        (plex-hexadecimal-digit ppstate)))
    (implies (not erp)
             (<= (ppstate->size new-ppstate)
                 (1- (ppstate->size ppstate)))))
  :rule-classes :linear)