• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
        • Syntax-for-tools
          • Formalized-subset
          • Mapping-to-language-definition
          • Input-files
          • Compilation-database
          • Printer
          • Output-files
          • Abstract-syntax-operations
          • Implementation-environments
          • Abstract-syntax
          • Concrete-syntax
          • Disambiguation
          • Validation
          • Gcc-builtins
          • Preprocessing
            • Preprocessor
              • Pproc
              • Preprocessor-states
              • Preprocessor-printer
              • Pproc-directive
              • Pread-token
              • Pproc-files
              • Pread-token/newline
              • Pproc-group-part
              • Preprocessor-lexer
                • Plex-lexeme
                • Plex-block-comment
                • Plex-pp-number
                • Plex-line-comment
                • Plex-identifier
                • Plex-escape-sequence
                • Plex-spaces
                • Plex-*-hexadecimal-digit
                • Plex-*-s-char
                • Plex-*-c-char
                • Plex-header-name
                • Plex-*-q-char
                • Plex-*-h-char
                • Plex-character-constant
                • Plex-hexadecimal-digit
                • Plex-string-literal
                • Plex-hex-quad
              • Pproc-file
              • Pproc-include-directive
              • Pproc-text-line
              • Pproc-*-group-part
              • Punread-token
              • *pproc-files-max*
              • String-plexeme-list-alist-to-filepath-filedata-map
              • String-plexeme-list-alist
              • Read-input-file-to-preproc
              • Preprocessor-reader
              • Preprocessor-messages
            • External-preprocessing
          • Parsing
        • Atc
        • Transformation-tools
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Preprocessor-lexer

Plex-pp-number

Lex a preprocessing number during preprocessing.

Signature

(plex-pp-number dot digit first-pos ppstate) 
  → 
(mv erp lexeme span new-ppstate)

Arguments

dot — Guard (booleanp dot).

digit — Guard (dec-digit-char-p digit).

first-pos — Guard (positionp first-pos).

Returns

lexeme — Type (plexemep lexeme).

span — Type (spanp span).

new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

This is called after the initial digit, or dot followed by digit, has been read; see the grammar rule for pp-number. The dot input says whether the preprocessing number starts with a dot, and the digit input is the first digit (preceded by . or not).

The initial digit, or dot followed by digit, already forms a preprocessing number. We keep reading characters so long as we can ``extend'' the preprocessing number, according to the grammar rule. Eventually we return the full preprocessing number and the full span.

Definitions and Theorems

Function: plex-pp-number-loop

(defun plex-pp-number-loop (current-pnumber current-pos ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (and (pnumberp current-pnumber)
                             (positionp current-pos))))
 (b* (((reterr)
       (irr-pnumber)
       (irr-position)
       ppstate)
      ((erp char pos ppstate)
       (pread-char ppstate)))
  (cond
   ((not char)
    (retok (pnumber-fix current-pnumber)
           (position-fix current-pos)
           ppstate))
   ((and (utf8-<= (char-code #\0) char)
         (utf8-<= char (char-code #\9)))
    (plex-pp-number-loop
         (make-pnumber-number-digit :number current-pnumber
                                    :digit (code-char char))
         pos ppstate))
   ((utf8-= char (char-code #\e))
    (b* (((erp char2 pos2 ppstate)
          (pread-char ppstate)))
     (cond
      ((and char2 (utf8-= char2 (char-code #\+)))
       (plex-pp-number-loop
          (make-pnumber-number-locase-e-sign :number current-pnumber
                                             :sign (sign-plus))
          pos2 ppstate))
      ((and char2 (utf8-= char2 (char-code #\-)))
       (plex-pp-number-loop
          (make-pnumber-number-locase-e-sign :number current-pnumber
                                             :sign (sign-minus))
          pos2 ppstate))
      (t
        (b* ((ppstate (if char2 (punread-char ppstate)
                        ppstate)))
          (plex-pp-number-loop
               (make-pnumber-number-nondigit :number current-pnumber
                                             :nondigit #\e)
               pos ppstate))))))
   ((utf8-= char (char-code #\E))
    (b* (((erp char2 pos2 ppstate)
          (pread-char ppstate)))
     (cond
      ((and char2 (utf8-= char2 (char-code #\+)))
       (plex-pp-number-loop
          (make-pnumber-number-upcase-e-sign :number current-pnumber
                                             :sign (sign-plus))
          pos2 ppstate))
      ((and char2 (utf8-= char2 (char-code #\-)))
       (plex-pp-number-loop
          (make-pnumber-number-upcase-e-sign :number current-pnumber
                                             :sign (sign-minus))
          pos2 ppstate))
      (t
        (b* ((ppstate (if char2 (punread-char ppstate)
                        ppstate)))
          (plex-pp-number-loop
               (make-pnumber-number-nondigit :number current-pnumber
                                             :nondigit #\E)
               pos ppstate))))))
   ((utf8-= char (char-code #\p))
    (b* (((erp char2 pos2 ppstate)
          (pread-char ppstate)))
     (cond
      ((and char2 (utf8-= char2 (char-code #\+)))
       (plex-pp-number-loop
          (make-pnumber-number-locase-p-sign :number current-pnumber
                                             :sign (sign-plus))
          pos2 ppstate))
      ((and char2 (utf8-= char2 (char-code #\-)))
       (plex-pp-number-loop
          (make-pnumber-number-locase-p-sign :number current-pnumber
                                             :sign (sign-minus))
          pos2 ppstate))
      (t
        (b* ((ppstate (if char2 (punread-char ppstate)
                        ppstate)))
          (plex-pp-number-loop
               (make-pnumber-number-nondigit :number current-pnumber
                                             :nondigit #\p)
               pos ppstate))))))
   ((utf8-= char (char-code #\P))
    (b* (((erp char2 pos2 ppstate)
          (pread-char ppstate)))
     (cond
      ((and char2 (utf8-= char2 (char-code #\+)))
       (plex-pp-number-loop
          (make-pnumber-number-upcase-p-sign :number current-pnumber
                                             :sign (sign-plus))
          pos2 ppstate))
      ((and char2 (utf8-= char2 (char-code #\-)))
       (plex-pp-number-loop
          (make-pnumber-number-upcase-p-sign :number current-pnumber
                                             :sign (sign-minus))
          pos2 ppstate))
      (t
        (b* ((ppstate (if char2 (punread-char ppstate)
                        ppstate)))
          (plex-pp-number-loop
               (make-pnumber-number-nondigit :number current-pnumber
                                             :nondigit #\P)
               pos ppstate))))))
   ((or (and (utf8-<= (char-code #\A) char)
             (utf8-<= char (char-code #\Z)))
        (and (utf8-<= (char-code #\a) char)
             (utf8-<= char (char-code #\z)))
        (utf8-= char (char-code #\_)))
    (plex-pp-number-loop
         (make-pnumber-number-nondigit :number current-pnumber
                                       :nondigit (code-char char))
         pos ppstate))
   ((utf8-= char (char-code #\.))
    (plex-pp-number-loop
         (make-pnumber-number-dot :number current-pnumber)
         pos ppstate))
   (t (b* ((ppstate (if char (punread-char ppstate)
                      ppstate)))
        (retok (pnumber-fix current-pnumber)
               (position-fix current-pos)
               ppstate))))))

Theorem: pnumberp-of-plex-pp-number-loop.final-pnumber

(defthm pnumberp-of-plex-pp-number-loop.final-pnumber
  (b* (((mv acl2::?erp
            ?final-pnumber ?last-pos ?new-ppstate)
        (plex-pp-number-loop current-pnumber current-pos ppstate)))
    (pnumberp final-pnumber))
  :rule-classes :rewrite)

Theorem: positionp-of-plex-pp-number-loop.last-pos

(defthm positionp-of-plex-pp-number-loop.last-pos
  (b* (((mv acl2::?erp
            ?final-pnumber ?last-pos ?new-ppstate)
        (plex-pp-number-loop current-pnumber current-pos ppstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-pp-number-loop.new-ppstate

(defthm ppstatep-of-plex-pp-number-loop.new-ppstate
 (implies
   (ppstatep ppstate)
   (b* (((mv acl2::?erp
             ?final-pnumber ?last-pos ?new-ppstate)
         (plex-pp-number-loop current-pnumber current-pos ppstate)))
     (ppstatep new-ppstate)))
 :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-pp-number-loop-uncond

(defthm ppstate->size-of-plex-pp-number-loop-uncond
  (b* (((mv acl2::?erp
            ?final-pnumber ?last-pos ?new-ppstate)
        (plex-pp-number-loop current-pnumber current-pos ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Function: plex-pp-number

(defun plex-pp-number (dot digit first-pos ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (booleanp dot)
                              (dec-digit-char-p digit)
                              (positionp first-pos))))
  (b* (((reterr)
        (irr-plexeme)
        (irr-span)
        ppstate)
       (initial-pnumber (if dot (pnumber-dot-digit digit)
                          (pnumber-digit digit)))
       ((erp final-pnumber last-pos ppstate)
        (plex-pp-number-loop initial-pnumber first-pos ppstate)))
    (retok (plexeme-number final-pnumber)
           (make-span :start first-pos
                      :end last-pos)
           ppstate)))

Theorem: plexemep-of-plex-pp-number.lexeme

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

Theorem: spanp-of-plex-pp-number.span

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

Theorem: ppstatep-of-plex-pp-number.new-ppstate

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

Theorem: ppstate->size-of-plex-pp-number-uncond

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