Match as many characters of some type as possible.
(vl-read-while-ctype echars) → (mv prefix remainder)
This is a generic function. See defchar for a convenient way to instantiate this function, and its corresponding theory, for your own character recognizers.
Function:
(defun vl-read-while-ctype (echars) (declare (xargs :guard (vl-echarlist-p echars))) (let ((__function__ 'vl-read-while-ctype)) (declare (ignorable __function__)) (mbe :logic (b* (((when (atom echars)) (mv nil echars)) ((unless (vl-ctype-p (vl-echar->char (car echars)))) (mv nil echars)) ((mv prefix remainder) (vl-read-while-ctype (cdr echars)))) (mv (cons (car echars) prefix) remainder)) :exec (b* (((mv prefix-rev remainder) (vl-read-while-ctype-impl echars nil))) (mv (reverse prefix-rev) remainder)))))
Theorem:
(defthm prefix-of-vl-read-while-ctype (and (true-listp (mv-nth 0 (vl-read-while-ctype echars))) (implies (force (vl-echarlist-p echars)) (vl-echarlist-p (mv-nth 0 (vl-read-while-ctype echars))))) :rule-classes ((:rewrite) (:type-prescription :corollary (true-listp (mv-nth 0 (vl-read-while-ctype echars))))))
Theorem:
(defthm equiv-of-vl-read-while-ctype-impl (and (equal (len (vl-read-while-ctype-impl echars acc)) 2) (implies (true-listp acc) (and (true-listp (mv-nth 0 (vl-read-while-ctype-impl echars acc))) (equal (mv-nth 0 (vl-read-while-ctype-impl echars acc)) (revappend (mv-nth 0 (vl-read-while-ctype echars)) acc)) (equal (mv-nth 1 (vl-read-while-ctype-impl echars acc)) (mv-nth 1 (vl-read-while-ctype echars)))))))
Theorem:
(defthm remainder-of-vl-read-while-ctype (and (equal (true-listp (mv-nth 1 (vl-read-while-ctype echars))) (true-listp echars)) (implies (force (vl-echarlist-p echars)) (vl-echarlist-p (mv-nth 1 (vl-read-while-ctype echars))))) :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp echars) (true-listp (mv-nth 1 (vl-read-while-ctype echars)))))))
Theorem:
(defthm prefix-of-vl-read-while-ctype-when-vl-ctype-p (implies (vl-ctype-p (vl-echar->char (car echars))) (iff (mv-nth 0 (vl-read-while-ctype echars)) (consp echars))))
Theorem:
(defthm vl-read-while-ctype-sound (vl-ctype-list-p (vl-echarlist->chars (mv-nth 0 (vl-read-while-ctype echars)))))
Theorem:
(defthm vl-read-while-ctype-complete (equal (vl-ctype-p (vl-echar->char (car (mv-nth 1 (vl-read-while-ctype echars))))) (if (consp (mv-nth 1 (vl-read-while-ctype echars))) nil (vl-ctype-p (vl-echar->char nil)))))
Theorem:
(defthm append-of-vl-read-while-ctype (equal (append (mv-nth 0 (vl-read-while-ctype echars)) (mv-nth 1 (vl-read-while-ctype echars))) echars))
Theorem:
(defthm no-change-loser-of-vl-read-while-ctype (implies (not (mv-nth 0 (vl-read-while-ctype echars))) (equal (mv-nth 1 (vl-read-while-ctype echars)) echars)))
Theorem:
(defthm acl2-count-of-vl-read-while-ctype-weak (<= (acl2-count (mv-nth 1 (vl-read-while-ctype echars))) (acl2-count echars)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm acl2-count-of-vl-read-while-ctype-strong (implies (mv-nth 0 (vl-read-while-ctype echars)) (< (acl2-count (mv-nth 1 (vl-read-while-ctype echars))) (acl2-count echars))) :rule-classes ((:rewrite) (:linear)))