• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • 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
        • Ordering
        • Numbers
          • Decimal
            • Parse-nat-from-string
            • Parse-nat-from-charlist
            • Nat-to-dec-chars
            • Dec-digit-chars-value
            • Dec-digit-char-p
            • Take-leading-dec-digit-chars
            • Dec-digit-char-value
            • Dec-digit-char-listp
            • 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
              • Nat-to-dec-string-list
              • Int-to-dec-string-list
              • Nonzero-dec-digit-char-p
              • Revappend-nat-to-dec-chars
            • Hex
            • Octal
            • Binary
          • Pad-trim
          • Coercion
          • Std/strings-extensions
          • Std/strings/digit-to-char
          • Substitution
          • Symbols
        • Std/io
        • Std/osets
        • Std/system
        • Std/basic
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Decimal

    Strval

    Interpret a string as a decimal number.

    Signature
    (strval x) → value?
    Arguments
    x — Guard (stringp x).
    Returns
    value? — Type (or (natp value?) (not value?)).

    For example, (strval "35") is 35. If the string has any non-decimal digit characters or is empty, we return nil.

    Definitions and Theorems

    Function: strval

    (defun strval (x)
           (declare (xargs :guard (stringp x)))
           (declare (type string x))
           (declare (xargs :split-types t))
           (let ((acl2::__function__ 'strval))
                (declare (ignorable acl2::__function__))
                (mbe :logic (let ((chars (explode x)))
                                 (and (consp chars)
                                      (dec-digit-char-listp chars)
                                      (dec-digit-chars-value chars)))
                     :exec (b* (((the unsigned-byte xl) (length x))
                                ((mv (the unsigned-byte val)
                                     (the unsigned-byte len))
                                 (parse-nat-from-string x 0 0 0 xl)))
                               (and (not (eql 0 len))
                                    (eql len xl)
                                    val)))))

    Theorem: return-type-of-strval

    (defthm return-type-of-strval
            (b* ((value? (strval x)))
                (or (natp value?) (not value?)))
            :rule-classes :type-prescription)

    Theorem: istreqv-implies-equal-strval-1

    (defthm istreqv-implies-equal-strval-1
            (implies (istreqv x x-equiv)
                     (equal (strval x) (strval x-equiv)))
            :rule-classes (:congruence))