• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
        • Decimal
          • Parse-nat-from-string
          • Parse-nat-from-charlist
          • Nat-to-dec-chars
          • Dec-digit-chars-value
          • Dec-digit-char-p
          • Dec-digit-char-listp
          • Take-leading-dec-digit-chars
          • Dec-digit-char-value
          • Dec-digit-char-list*p
          • Nat-to-dec-string-width
          • Nat-to-dec-string
          • Dec-digit-string-p
          • Strval
          • Skip-leading-digits
          • Nat-to-dec-string-size
          • Int-to-dec-string-width
          • Int-to-dec-string
          • Nonzero-dec-digit-char-p
          • Nat-to-dec-string-list
          • Int-to-dec-string-list
          • Revappend-nat-to-dec-chars
        • Hex
        • Octal
        • Binary
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Decimal

Parse-nat-from-string

Parse a natural number from a string, at some offset.

Signature

(parse-nat-from-string x val len n xl) → (mv val len)

Arguments

x — The string to parse.
    Guard (stringp x).

val — Accumulator for the value we have parsed so far; typically 0 to start with.
    Guard (natp val).

len — Accumulator for the number of digits we have parsed so far; typically 0 to start with.
    Guard (natp len).

n — Offset into x where we should begin parsing. Must be a valid index into the string, i.e., 0 <= n < (length x).
    Guard (natp n).

xl — Pre-computed length of x.
    Guard (eql xl (length x)).

Returns

val — The value of the digits we parsed.
    Type (natp val).

len — The number of digits we parsed.
    Type (natp len).

This function is flexible but very complicated. See strval for a very simple alternative that may do what you want.

The final val and len are guaranteed to be natural numbers; failure is indicated by a return len of zero.

Because of leading zeroes, the len may be much larger than you would expect based on val alone. The len argument is generally useful if you want to continue parsing through the string, i.e., the n you started with plus the len you got out will be the next position in the string after the number.

See also parse-nat-from-charlist for a simpler function that reads a number from the start of a character list. This function also serves as part of our logical definition.

Definitions and Theorems

Function: parse-nat-from-string

(defun parse-nat-from-string (x val len n xl)
  (declare (xargs :guard (and (stringp x)
                              (natp val)
                              (natp len)
                              (natp n)
                              (eql xl (length x)))))
  (declare (type string x)
           (type unsigned-byte val len n xl))
  (declare (xargs :split-types t :guard (<= n xl)))
  (let ((acl2::__function__ 'parse-nat-from-string))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* (((mv val len ?rest)
               (parse-nat-from-charlist (nthcdr n (explode x))
                                        val len)))
           (mv val len))
         :exec
         (b* (((when (eql n xl)) (mv val len))
              ((the (unsigned-byte 8) code)
               (char-code (the character
                               (char (the string x)
                                     (the unsigned-byte n)))))
              ((unless (and (<= (the (unsigned-byte 8) code)
                                (the (unsigned-byte 8) 57))
                            (<= (the (unsigned-byte 8) 48)
                                (the (unsigned-byte 8) code))))
               (mv val len))
              ((the (unsigned-byte 8)
                    dec-digit-char-value)
               (the (unsigned-byte 8)
                    (- (the (unsigned-byte 8) code)
                       (the (unsigned-byte 8) 48)))))
           (parse-nat-from-string
                (the string x)
                (the unsigned-byte
                     (+ (the (unsigned-byte 8)
                             dec-digit-char-value)
                        (the unsigned-byte
                             (* 10 (the unsigned-byte val)))))
                (the unsigned-byte
                     (+ 1 (the unsigned-byte len)))
                (the unsigned-byte
                     (+ 1 (the unsigned-byte n)))
                (the unsigned-byte xl))))))

Theorem: natp-of-parse-nat-from-string.val

(defthm natp-of-parse-nat-from-string.val
  (b* (((mv ?val acl2::?len)
        (parse-nat-from-string x val len n xl)))
    (natp val))
  :rule-classes :type-prescription)

Theorem: natp-of-parse-nat-from-string.len

(defthm natp-of-parse-nat-from-string.len
  (b* (((mv ?val acl2::?len)
        (parse-nat-from-string x val len n xl)))
    (natp len))
  :rule-classes :type-prescription)