• 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
          • Parsing
            • Parser
              • Parse-exprs/decls/stmts
              • Parser-states
              • Parse-external-declaration
              • Parse-cast-expression
              • Parse-expression-or-type-name
              • Parse-postfix-expression
              • Lexer
                • Check-full-ppnumber
                • Lex-lexeme
                • Lex-oct-iconst-/-dec-fconst
                • Lex-?-integer-suffix
                • Lex-hex-iconst/fconst
                • Lex-identifier/keyword
                • Lex-dec-iconst/fconst
                • Lex-block-comment
                • Lex-escape-sequence
                • Read-token
                • Lex-*-hexadecimal-digit
                • Lex-?-floating-suffix
                • Lex-*-c-char
                • Lex-*-s-char
                • Lex-prepr-directive
                • Lex-line-comment
                • Lex-*-digit
                • Lex-*-q-char
                • Lex-*-h-char
                • Lex-iconst/fconst
                • Lex-?-exponent-part
                • Lex-character-constant
                • Lexeme
                • Lex-string-literal
                • Lex-dec-fconst
                • Reread-to-token
                • Lex-non-octal-digit
                • Lex-hexadecimal-digit
                • Lex-header-name
                • Lex-binary-exponent-part
                • Lex-exponent-part
                • Lex-?-sign
                • Only-whitespace-backward-through-line
                • Lexeme-option
                • Lex-hex-quad
                • Unread-to-token
                • Read-stringlit
                • Unread-tokens
                • Read-identifier
                • Read-punctuator
                • Read-keyword
                • Unread-token
                • Irr-lexeme
              • Parse-primary-expression
              • Token-unary-expression-start-p
              • Parse-declaration-specifier
              • Parse-declaration-specifiers
              • Parse-unary-expression-or-parenthesized-type-name
              • Parse-asm-name-specifier
              • Parse-specifier/qualifier
              • Parse-expression-rest
              • Token-type-specifier-keyword-p
              • Parse-fileset
              • Parse-*-external-declaration
              • Parse-declarator-or-abstract-declarator
              • Parse-asm-goto-labels
              • Parse-asm-clobbers
              • Parse-translation-unit
              • Parse-*-label-declaration
              • Token-postfix-expression-rest-start-p
              • Parse-?-asm-name-specifier
              • Parse-*-comma-identifier
              • Parse-postfix-expression-rest
              • Parse-expression
              • Make-expr-unary-with-preinc/predec-ops
              • Parse-*-stringlit
              • Parse-statement
              • Token-struct-declaration-start-p
              • Parse-*-attribute-specifier
              • Parse-initializer-list
              • Parse-file
              • Parse-pointer
              • Parse-label-declaration
              • Parse-array/function-declarator
              • Token-type-qualifier-p
              • Parse-*-asm-qualifier
              • Parse-parameter-declaration
              • Parse-attribute-name
              • Parse-argument-expressions
              • Make-expr-cast/add-or-cast/sub-ambig
              • Parse-struct-or-union-specifier
              • Parse-declaration-or-statement
              • Parse-assignment-expression
              • Parse-asm-clobber
              • Token-specifier/qualifier-start-p
              • Token-primary-expression-start-p
              • Token-function-specifier-p
              • Token-expression-start-p
              • Parse-*-increment/decrement
              • Parse-direct-abstract-declarator
              • Parse-compound-statement
              • Token-to-type-specifier-keyword
              • Parse-unary-expression
              • Parse-argument-expressions-rest
              • Parse-generic-associations-rest
              • Parse-conditional-expression
              • Parse-fileset-loop
              • Parse-direct-abstract-declarator-rest
              • Token-designation?-initializer-start-p
              • Token-declaration-specifier-start-p
              • Parse-designator-list
              • Token-abstract-declarator-start-p
              • Parse-?-asm-output-operands
              • Parse-?-asm-input-operands
              • Parse-struct-declaration
              • Parse-specifier-qualifier-list
              • Parse-parameter-declaration-list
              • Parse-constant-expression
              • Token-type-specifier-start-p
              • Token-type-qualifier-or-attribute-specifier-start-p
              • Parse-static-assert-declaration
              • Parse-direct-declarator
              • Parse-declaration
              • Parse-attribute-parameters
              • Token-unary-operator-p
              • Token-to-unary-operator
              • Token-to-type-qualifier
              • Token-storage-class-specifier-p
              • Token-initializer-start-p
              • Token-direct-abstract-declarator-start-p
              • Token-declarator-start-p
              • Parse-initializer
              • Parse-direct-declarator-rest
              • Token-to-storage-class-specifier
              • Token-to-assignment-operator
              • Token-to-asm-qualifier
              • Token-struct-declarator-start-p
              • Token-direct-declarator-start-p
              • Token-assignment-operator-p
              • Parse-type-qualifier-and-attribute-specifier-list
              • Parse-enumerator-list
              • Parse-designation?-initializer
              • Parse-compound-literal
              • Parse-block-item
              • Token-type-name-start-p
              • Token-to-function-specifier
              • Token-preinc/predec-operator-p
              • Token-multiplicative-operator-p
              • Token-designator-start-p
              • Token-designation-start-p
              • Parse-generic-association
              • Parse-declaration-list
              • Parse-attribute-specifier
              • Parse-asm-output-operands
              • Token-to-relational-operator
              • Token-to-preinc/predec-operator
              • Token-to-multiplicative-operator
              • Token-relational-operator-p
              • Token-equality-operator-p
              • Token-asm-qualifier-p
              • Token-additive-operator-p
              • Parse-asm-statement
              • Parse-asm-input-operands
              • Token-to-equality-operator
              • Token-to-additive-operator
              • Token-shift-operator-p
              • Parser-messages
              • Parse-type-name
              • Parse-struct-declarator-list
              • Parse-struct-declaration-list
              • Parse-relational-expression-rest
              • Parse-multiplicative-expression-rest
              • Parse-logical-or-expression-rest
              • Parse-logical-and-expression-rest
              • Parse-inclusive-or-expression-rest
              • Parse-exclusive-or-expression-rest
              • Parse-equality-expression-rest
              • Parse-array/function-abstract-declarator
              • Parse-additive-expression-rest
              • Token-to-shift-operator
              • Parse-struct-declarator
              • Parse-shift-expression-rest
              • Parse-member-designor
              • Parse-init-declarator-list
              • Parse-init-declarator
              • Parse-designator
              • Parse-and-expression-rest
              • Parse-alignment-specifier
              • Reader
              • Parse-shift-expression
              • Parse-relational-expression
              • Parse-multiplicative-expression
              • Parse-logical-or-expression
              • Parse-logical-and-expression
              • Parse-inclusive-or-expression
              • Parse-exclusive-or-expression
              • Parse-equality-expression
              • Parse-enum-specifier
              • Parse-block-item-list
              • Parse-attribute-list
              • Parse-and-expression
              • Parse-additive-expression
              • Parse-abstract-declarator
              • Parse-member-designor-rest
              • Parse-declarator
              • Parse-attribute
              • Parse-type-qualifier-or-attribute-specifier
              • Parse-enumerator
              • Parse-asm-output-operand
              • Parse-asm-input-operand
        • 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

• Lexer

Lex-*-digit

Lex zero or more (decimal) digits, as many as available.

Signature

(lex-*-digit pos-so-far parstate) 
  → 
(mv erp decdigs last-pos next-pos new-parstate)

Arguments

pos-so-far — Guard (positionp pos-so-far).

parstate — Guard (parstatep parstate).

Returns

decdigs — Type (dec-digit-char-listp decdigs).

last-pos — Type (positionp last-pos).

next-pos — Type (positionp next-pos).

new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

That is, we read *digit, in ABNF notation, i.e. a repetition of zero of more instances of digit.

The pos-so-far input is the position that has been read so far, just before attempting to read the digits. The last-pos output is the position of the last digit read, or pos-so-far if there are no digits. The next-pos output is the position just after the last digit read, or just after pos-so-far if there are no digits.

We read the next character. If it does not exist, we return. If it exists but is not a digit, we put the character back and return. Otherwise, we recursively read zero or more, and we put the one just read in front. We always return the position of the last digit, or the input pos-so-far if there is no digit: this input is the position read so far, just before the zero or more digits to be read.

Definitions and Theorems

Function: lex-*-digit

(defun lex-*-digit (pos-so-far parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (and (positionp pos-so-far)
                              (parstatep parstate))))
  (let ((__function__ 'lex-*-digit))
    (declare (ignorable __function__))
    (b* (((reterr)
          nil (irr-position)
          (irr-position)
          parstate)
         ((erp char pos parstate)
          (read-char parstate))
         ((when (not char))
          (retok nil (position-fix pos-so-far)
                 pos parstate))
         ((unless (and (utf8-<= (char-code #\0) char)
                       (utf8-<= char (char-code #\9))))
          (b* ((parstate (unread-char parstate)))
            (retok nil (position-fix pos-so-far)
                   pos parstate)))
         (decdig (code-char char))
         ((erp decdigs last-pos next-pos parstate)
          (lex-*-digit pos parstate)))
      (retok (cons decdig decdigs)
             last-pos next-pos parstate))))

Theorem: dec-digit-char-listp-of-lex-*-digit.decdigs

(defthm dec-digit-char-listp-of-lex-*-digit.decdigs
  (b* (((mv acl2::?erp ?decdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-digit pos-so-far parstate)))
    (dec-digit-char-listp decdigs))
  :rule-classes :rewrite)

Theorem: positionp-of-lex-*-digit.last-pos

(defthm positionp-of-lex-*-digit.last-pos
  (b* (((mv acl2::?erp ?decdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-digit pos-so-far parstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: positionp-of-lex-*-digit.next-pos

(defthm positionp-of-lex-*-digit.next-pos
  (b* (((mv acl2::?erp ?decdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-digit pos-so-far parstate)))
    (positionp next-pos))
  :rule-classes :rewrite)

Theorem: parstatep-of-lex-*-digit.new-parstate

(defthm parstatep-of-lex-*-digit.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp ?decdigs
                     ?last-pos ?next-pos ?new-parstate)
                 (lex-*-digit pos-so-far parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: true-listp-of-lex-*-digit.decdigs

(defthm true-listp-of-lex-*-digit.decdigs
  (b* (((mv acl2::?erp ?decdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-digit pos-so-far parstate)))
    (true-listp decdigs))
  :rule-classes :type-prescription)

Theorem: parsize-of-lex-*-digit-uncond

(defthm parsize-of-lex-*-digit-uncond
  (b* (((mv acl2::?erp ?decdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-digit pos-so-far parstate)))
    (<= (parsize new-parstate)
        (- (parsize parstate) (len decdigs))))
  :rule-classes :linear)