Parse a natural number from the beginning of a character list.
(parse-nat-from-charlist x val len) → (mv val len rest)
This function is somewhat complicated. See also (dec-digit-chars-value x), which is a simpler way to interpret strings where all of the characters are digits.
Function:
(defun parse-nat-from-charlist (x val len) (declare (xargs :guard (and (character-listp x) (natp val) (natp len)))) (declare (type unsigned-byte val len)) (declare (xargs :split-types t)) (let ((acl2::__function__ 'parse-nat-from-charlist)) (declare (ignorable acl2::__function__)) (mbe :logic (cond ((atom x) (mv (nfix val) (nfix len) nil)) ((dec-digit-char-p (car x)) (let ((dec-digit-char-value (dec-digit-char-value (car x)))) (parse-nat-from-charlist (cdr x) (+ dec-digit-char-value (* 10 (nfix val))) (+ 1 (nfix len))))) (t (mv (nfix val) (nfix len) x))) :exec (b* (((when (atom x)) (mv val len nil)) ((the (unsigned-byte 8) code) (char-code (the character (car x)))) ((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 x)) ((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-charlist (cdr x) (the unsigned-byte (+ (the (unsigned-byte 8) dec-digit-char-value) (the unsigned-byte (* 10 val)))) (the unsigned-byte (+ 1 (the integer len))))))))
Theorem:
(defthm val-of-parse-nat-from-charlist (equal (mv-nth 0 (parse-nat-from-charlist x val len)) (+ (dec-digit-chars-value (take-leading-dec-digit-chars x)) (* (nfix val) (expt 10 (len (take-leading-dec-digit-chars x)))))))
Theorem:
(defthm len-of-parse-nat-from-charlist (equal (mv-nth 1 (parse-nat-from-charlist x val len)) (+ (nfix len) (len (take-leading-dec-digit-chars x)))))
Theorem:
(defthm rest-of-parse-nat-from-charlist (equal (mv-nth 2 (parse-nat-from-charlist x val len)) (skip-leading-digits x)))