Parse zero or more given natural numbers into a tree that matches a direct numeric value notation that consists of that list of numbers.
(parse-exact-list nats input) → (mv error? tree? rest-input)
Function:
(defun parse-exact-list-aux (nats input) (declare (xargs :guard (and (nat-listp nats) (nat-listp input)))) (let ((__function__ 'parse-exact-list-aux)) (declare (ignorable __function__)) (b* (((when (endp nats)) (mv nil (nat-list-fix input))) (nat (lnfix (car nats))) ((mv error? input-nat input) (parse-any input)) ((when error?) (mv error? input)) ((unless (= input-nat nat)) (mv (msg "Failed to parse ~x0: found ~x1 instead." nat input-nat) (cons input-nat input))) ((mv error? input) (parse-exact-list-aux (cdr nats) input)) ((when error?) (mv error? input))) (mv nil input))))
Theorem:
(defthm maybe-msgp-of-parse-exact-list-aux.error? (b* (((mv ?error? ?rest-input) (parse-exact-list-aux nats input))) (maybe-msgp error?)) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-parse-exact-list-aux.rest-input (b* (((mv ?error? ?rest-input) (parse-exact-list-aux nats input))) (nat-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm len-of-parse-exact-list-aux-linear-<= (b* (((mv ?error? ?rest-input) (parse-exact-list-aux nats input))) (<= (len rest-input) (len input))) :rule-classes :linear)
Theorem:
(defthm len-of-parse-exact-list-aux-linear-< (b* (((mv ?error? ?rest-input) (parse-exact-list-aux nats input))) (implies (and (not error?) (consp nats)) (< (len rest-input) (len input)))) :rule-classes :linear)
Theorem:
(defthm parse-exact-list-aux-of-nat-list-fix-nats (equal (parse-exact-list-aux (nat-list-fix nats) input) (parse-exact-list-aux nats input)))
Theorem:
(defthm parse-exact-list-aux-nat-list-equiv-congruence-on-nats (implies (acl2::nat-list-equiv nats nats-equiv) (equal (parse-exact-list-aux nats input) (parse-exact-list-aux nats-equiv input))) :rule-classes :congruence)
Theorem:
(defthm parse-exact-list-aux-of-nat-list-fix-input (equal (parse-exact-list-aux nats (nat-list-fix input)) (parse-exact-list-aux nats input)))
Theorem:
(defthm parse-exact-list-aux-nat-list-equiv-congruence-on-input (implies (acl2::nat-list-equiv input input-equiv) (equal (parse-exact-list-aux nats input) (parse-exact-list-aux nats input-equiv))) :rule-classes :congruence)
Function:
(defun parse-exact-list (nats input) (declare (xargs :guard (and (nat-listp nats) (nat-listp input)))) (let ((__function__ 'parse-exact-list)) (declare (ignorable __function__)) (b* (((mv error? input) (parse-exact-list-aux nats input)) ((when error?) (mv error? nil input))) (mv nil (tree-leafterm nats) input))))
Theorem:
(defthm maybe-msgp-of-parse-exact-list.error? (b* (((mv ?error? ?tree? ?rest-input) (parse-exact-list nats input))) (maybe-msgp error?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exact-list.tree? (b* (((mv ?error? ?tree? ?rest-input) (parse-exact-list nats input))) (and (tree-optionp tree?) (implies (not error?) (treep tree?)) (implies error? (not tree?)))) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-parse-exact-list.rest-input (b* (((mv ?error? ?tree? ?rest-input) (parse-exact-list nats input))) (nat-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm len-of-parse-exact-list-linear-<= (b* (((mv ?error? ?tree? ?rest-input) (parse-exact-list nats input))) (<= (len rest-input) (len input))) :rule-classes :linear)
Theorem:
(defthm len-of-parse-exact-list-linear-< (b* (((mv ?error? ?tree? ?rest-input) (parse-exact-list nats input))) (implies (and (not error?) (consp nats)) (< (len rest-input) (len input)))) :rule-classes :linear)
Theorem:
(defthm parse-exact-list-of-nat-list-fix-nats (equal (parse-exact-list (nat-list-fix nats) input) (parse-exact-list nats input)))
Theorem:
(defthm parse-exact-list-nat-list-equiv-congruence-on-nats (implies (acl2::nat-list-equiv nats nats-equiv) (equal (parse-exact-list nats input) (parse-exact-list nats-equiv input))) :rule-classes :congruence)
Theorem:
(defthm parse-exact-list-of-nat-list-fix-input (equal (parse-exact-list nats (nat-list-fix input)) (parse-exact-list nats input)))
Theorem:
(defthm parse-exact-list-nat-list-equiv-congruence-on-input (implies (acl2::nat-list-equiv input input-equiv) (equal (parse-exact-list nats input) (parse-exact-list nats input-equiv))) :rule-classes :congruence)