• 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
        • Hex
        • Octal
        • Binary
          • Parse-bits-from-string
          • Parse-bits-from-charlist
          • Nat-to-bin-chars
          • Bin-digit-chars-value
          • Take-leading-bin-digit-chars
          • Bin-digit-char-listp
          • Skip-leading-bit-digits
          • Bin-digit-char-list*p
          • Bin-digit-string-p
          • Bin-digit-char-value
          • Strval2
          • Nat-to-bin-string
          • Bin-digit-char-p
          • Nat-to-bin-string-list
          • Nat-to-bin-string-size
          • Revappend-nat-to-bin-chars
          • Binify-width
          • Binify
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Binary

Parse-bits-from-string

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

Signature

(parse-bits-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 bits 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 bits we parsed.
    Type (natp val).

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

This function is flexible but very complicated. See strval2 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-bits-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-bits-from-string

(defun parse-bits-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-bits-from-string))
  (declare (ignorable acl2::__function__))
  (mbe :logic
       (b* (((mv val len ?rest)
             (parse-bits-from-charlist (nthcdr n (explode x))
                                       val len)))
         (mv val len))
       :exec
       (b* (((when (eql n xl)) (mv val len))
            ((the character char)
             (char (the string x)
                   (the unsigned-byte n)))
            ((when (equal char #\0))
             (parse-bits-from-string (the string x)
                                     (the unsigned-byte (ash val 1))
                                     (the unsigned-byte (+ 1 len))
                                     (the unsigned-byte (+ 1 n))
                                     (the unsigned-byte xl)))
            ((when (equal char #\1))
             (parse-bits-from-string
                  (the string x)
                  (the unsigned-byte
                       (+ 1 (the unsigned-byte (ash val 1))))
                  (the unsigned-byte (+ 1 len))
                  (the unsigned-byte (+ 1 n))
                  (the unsigned-byte xl))))
         (mv val len)))))

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

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

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

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