• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
          • Disambiguator
          • Abstract-syntax
          • Parser
            • Parse-exprs/decls/stmts
            • Check-full-ppnumber
            • Read-char
            • Parstate
            • Lex-identifier/keyword
            • Lex-oct-iconst-/-dec-fconst
            • Lex-lexeme
            • Parse-external-declaration
            • Parse-cast-expression
            • Lex-isuffix-if-present
            • Parse-expression-or-type-name
            • Parse-postfix-expression
            • Lex-hex-iconst/fconst
            • Lex-dec-iconst/fconst
            • Lex-block-comment
            • Lex-escape-sequence
            • Read-token
            • Token
            • Lex-*-hexadecimal-digit
            • Lex-*-c-char
            • Lex-*-s-char
            • Parse-specifier/qualifier
            • Lex-*-digit
            • Lex-line-comment
            • Char-to-msg
            • Parse-primary-expression
            • Parse-declaration-specifier
            • Lex-iconst/fconst
            • Parse-external-declaration-list
            • Parse-declaration-specifiers
            • Lex-dec-expo-if-present
            • Init-parstate
            • Reread-to-token
            • Parse-asm-name-specifier
            • Lex-character-constant
            • Parse-expression-rest
            • Parstate$
            • Lex-dec-fconst
            • Token-unary-expression-start-p
            • Parse-declarator-or-abstract-declarator
            • Parse-asm-goto-labels
            • Parse-asm-clobbers
            • Lex-stringlit
            • Lex-non-octal-digit
            • Position
            • Lexeme
            • Lex-fsuffix-if-present
            • Parse-translation-unit
            • Lex-hexadecimal-digit
            • Token-type-specifier-keyword-p
            • Token-postfix-expression-rest-start-p
            • To-parstate$
            • Parse-?-asm-name-specifier
            • Parse-postfix-expression-rest
            • Parse-expression
            • Lex-sign-if-present
            • Lex-dec-expo
            • Lex-bin-expo
            • Unread-to-token
            • Parse-*-stringlit
            • Parse-statement
            • Parse-fileset
            • Make-expr-unary-with-preinc/predec-ops
            • Token-option
            • Lexeme-option
            • Token-struct-declaration-start-p
            • Parse-*-attribute-specifier
            • Parse-initializer-list
            • Parse-file
            • Parse-pointer
            • Parse-array/function-declarator
            • Unread-chars
            • Span
            • Read-stringlit
            • Lex-hex-quad
            • Unread-tokens
            • Token-type-qualifier-p
            • Read-identifier
            • Parse-*-asm-qualifier
            • Unread-char
            • Parse-attribute-name
            • Parse-argument-expressions
            • Make-expr-cast/add-or-cast/sub-ambig
            • Read-punctuator
            • Parse-struct-or-union-specifier
            • Parse-assignment-expression
            • Parse-asm-clobber
            • Token-specifier/qualifier-start-p
            • Token-primary-expression-start-p
            • Token-function-specifier-p
            • Reterr-msg
            • Read-keyword
            • Parse-*-increment/decrement
            • Parse-direct-abstract-declarator
            • Parse-declaration-or-statement
            • Char+position
            • Unread-token
            • Token+span
            • Token-expression-start-p
            • Update-parstate->tokens-unread
            • Update-parstate->chars-unread
            • Token-to-msg
            • Update-parstate->tokens-read
            • Update-parstate->tokens-length
            • Update-parstate->position
            • Update-parstate->chars-read
            • Parse-parameter-declaration
            • Parse-argument-expressions-rest
            • Update-parstate->chars-length
            • Token-to-type-specifier-keyword
            • Update-parstate->bytes
            • Parse-unary-expression
            • Parse-generic-associations-rest
            • Parse-conditional-expression
            • Update-parstate->size
            • Update-parstate->gcc
            • Parsize
            • Parse-direct-abstract-declarator-rest
            • Token-declaration-specifier-start-p
            • Parse-designator-list
            • Token-designation?-initializer-start-p
            • 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-fileset-loop
            • 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-punctuatorp
            • Token-direct-abstract-declarator-start-p
            • Token-declarator-start-p
            • Parse-direct-declarator-rest
            • Token-to-storage-class-specifier
            • Token-to-assignment-operator
            • Token-to-asm-qualifier
            • Token-struct-declarator-start-p
            • Token-keywordp
            • Token-initializer-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
            • Parstate->tokens-unread
            • Parstate->chars-unread
            • Parstate->bytes
            • Parse-initializer
            • 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
            • Span-join
            • Parstate->tokens-read
            • Parstate->tokens-length
            • Parstate->size
            • Parstate->chars-read
            • Parstate->chars-length
            • Parse-asm-statement
            • Parse-asm-input-operands
            • Update-parstate->token
            • Update-parstate->char
            • Token-to-equality-operator
            • Token-to-additive-operator
            • Token-shift-operator-p
            • To-parstate$-tokens-unread
            • To-parstate$-chars-unread
            • Position-inc-line
            • Position-inc-column
            • Parstate->gcc
            • 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
            • To-parstate$-tokens-read
            • Parse-struct-declarator
            • Parse-shift-expression-rest
            • Parse-member-designor
            • Parse-init-declarator-list
            • Parse-init-declarator
            • Parse-and-expression-rest
            • Parse-alignment-specifier
            • To-parstate$-chars-read
            • Position-to-msg
            • Parstate->token
            • Parstate->char
            • 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
            • Char+position-list
            • Token+span-list
            • Span-to-msg
            • Parstate-fix
            • Parse-member-designor-rest
            • Position-init
            • Parstate->position
            • Parse-designator
            • Parse-declarator
            • Parse-attribute
            • Irr-token
            • Irr-span
            • Irr-position
            • Irr-lexeme
            • Token-list
            • Parse-type-qualifier-or-attribute-specifier
            • Parse-enumerator
            • Parse-asm-output-operand
            • Parse-asm-input-operand
          • Validator
          • Printer
          • Formalized-subset
          • Mapping-to-language-definition
          • Defpred
          • Validation-information
          • Input-files
          • Abstract-syntax-operations
          • Output-files
          • Implementation-environments
          • Concrete-syntax
          • Unambiguity
          • Preprocessing
          • Abstraction-mapping
        • Atc
        • Language
        • Representation
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Parser

Lex-dec-iconst/fconst

Lex a decimal integer or floating constant.

Signature

(lex-dec-iconst/fconst first-digit first-pos parstate) 
  → 
(mv erp const last-pos new-parstate)

Arguments

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

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

parstate — Guard (parstatep parstate).

Returns

const — Type (constp const).

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

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

This is called when we expect a decimal constant, after reading the first digit, when that digit is not 0. The first digit, and its position, are passed to this function.

First we read as many additional decimal digits as possible, of which there may be none. Then we attempt to read the next character, and we do different things based on that.

If there is no character after the digits, we have an integer decimal constant.

If the next character is a dot, then this must be a decimal floating constant. We read as many digits as possible after the dot; there may no other digits. Then we attempt to read a decimal exponent, if any. Then a floating suffix, if any. Finally, if check-full-ppnumber succeeds (see the documentation of that function for details), we return the appropriate constant.

If the next character is e or E, then this must be a decimal floating constant, consisting of an integer and an exponent. We read the exponent after putting back the letter; the exponent must be present for the constant to be valid. We read a floating suffix if present. If check-full-ppnumber succeeds, we return the appropriate constant.

Otherwise, this must be a decimal integer constant, if it is a valid constant at all. We put back the character and read an integer suffix if present. If check-full-ppnumber passes, we return the appropriate integer constant.

Definitions and Theorems

Function: lex-dec-iconst/fconst

(defun lex-dec-iconst/fconst (first-digit first-pos parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (and (dec-digit-char-p first-digit)
                             (positionp first-pos)
                             (parstatep parstate))))
 (declare (xargs :guard (not (equal first-digit #\0))))
 (let ((__function__ 'lex-dec-iconst/fconst))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-const)
        (irr-position)
        parstate)
       ((erp decdigs decdigs-last-pos & parstate)
        (lex-*-digit first-pos parstate))
       ((erp char pos parstate)
        (read-char parstate)))
   (cond
    ((not char)
     (retok
      (const-int
       (make-iconst
        :core
        (make-dec/oct/hex-const-dec
            :value
            (str::dec-digit-chars-value (cons first-digit decdigs)))
        :suffix? nil))
      (cond (decdigs decdigs-last-pos)
            (t (position-fix first-pos)))
      parstate))
    ((= char (char-code #\.))
     (b*
      (((erp decdigs2 decdigs2-last-pos & parstate)
        (lex-*-digit pos parstate))
       ((erp expo? expo-last/next-pos parstate)
        (lex-dec-expo-if-present parstate))
       ((erp fsuffix? suffix-last/next-pos parstate)
        (lex-fsuffix-if-present parstate))
       ((erp parstate)
        (check-full-ppnumber nil parstate))
       (core
        (if decdigs2
         (if expo?
          (make-dec-core-fconst-frac
             :significand
             (make-dec-frac-const :before (cons first-digit decdigs)
                                  :after decdigs2)
             :expo? expo?)
          (make-dec-core-fconst-frac
             :significand
             (make-dec-frac-const :before (cons first-digit decdigs)
                                  :after decdigs2)
             :expo? nil))
         (if expo?
          (make-dec-core-fconst-frac
             :significand
             (make-dec-frac-const :before (cons first-digit decdigs)
                                  :after nil)
             :expo? expo?)
          (make-dec-core-fconst-frac
             :significand
             (make-dec-frac-const :before (cons first-digit decdigs)
                                  :after nil)
             :expo? nil)))))
      (retok (const-float (make-fconst-dec :core core
                                           :suffix? fsuffix?))
             (cond (fsuffix? suffix-last/next-pos)
                   (expo? expo-last/next-pos)
                   (decdigs2 decdigs2-last-pos)
                   (t pos))
             parstate)))
    ((or (= char (char-code #\e))
         (= char (char-code #\E)))
     (b* ((parstate (unread-char parstate))
          ((erp expo expo-last-pos parstate)
           (lex-dec-expo parstate))
          ((erp fsuffix? suffix-last/next-pos parstate)
           (lex-fsuffix-if-present parstate))
          ((erp parstate)
           (check-full-ppnumber nil parstate)))
      (retok
        (const-float
             (make-fconst-dec
                  :core (make-dec-core-fconst-int
                             :significand (cons first-digit decdigs)
                             :expo expo)
                  :suffix? fsuffix?))
        (cond (fsuffix? suffix-last/next-pos)
              (t expo-last-pos))
        parstate)))
    (t
     (b* ((parstate (unread-char parstate))
          ((erp isuffix? suffix-last/next-pos parstate)
           (lex-isuffix-if-present parstate))
          ((erp parstate)
           (check-full-ppnumber nil parstate)))
      (retok
       (const-int
        (make-iconst
         :core
         (make-dec/oct/hex-const-dec
            :value
            (str::dec-digit-chars-value (cons first-digit decdigs)))
         :suffix? isuffix?))
       (cond (isuffix? suffix-last/next-pos)
             (decdigs decdigs-last-pos)
             (t (position-fix first-pos)))
       parstate)))))))

Theorem: constp-of-lex-dec-iconst/fconst.const

(defthm constp-of-lex-dec-iconst/fconst.const
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-dec-iconst/fconst first-digit first-pos parstate)))
    (constp const))
  :rule-classes :rewrite)

Theorem: positionp-of-lex-dec-iconst/fconst.last-pos

(defthm positionp-of-lex-dec-iconst/fconst.last-pos
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-dec-iconst/fconst first-digit first-pos parstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: parstatep-of-lex-dec-iconst/fconst.new-parstate

(defthm parstatep-of-lex-dec-iconst/fconst.new-parstate
 (implies
      (parstatep parstate)
      (b* (((mv acl2::?erp
                ?const ?last-pos ?new-parstate)
            (lex-dec-iconst/fconst first-digit first-pos parstate)))
        (parstatep new-parstate)))
 :rule-classes :rewrite)

Theorem: parsize-of-lex-dec-iconst/fconst-uncond

(defthm parsize-of-lex-dec-iconst/fconst-uncond
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-dec-iconst/fconst first-digit first-pos parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)