Parse zero or more natural numbers, each of which in one of two given ranges, into a list of trees that matches the repetition of zero or more alternations of the corresponding range numeric value notations.
(parse-*-in-either-range min1 max1 min2 max2 input) → (mv error? trees rest-input)
Function:
(defun parse-*-in-either-range (min1 max1 min2 max2 input) (declare (xargs :guard (and (natp min1) (natp max1) (natp min2) (natp max2) (nat-listp input)))) (declare (xargs :guard (and (<= min1 max1) (< max1 min2) (<= min2 max2)))) (seq-backtrack input ((tree := (parse-in-either-range min1 max1 min2 max2 input)) (trees := (parse-*-in-either-range min1 max1 min2 max2 input)) (return (cons tree trees))) ((return-raw (mv nil nil (nat-list-fix input))))))
Theorem:
(defthm not-of-parse-*-in-either-range.error? (b* (((mv ?error? ?trees ?rest-input) (parse-*-in-either-range min1 max1 min2 max2 input))) (not error?)) :rule-classes :rewrite)
Theorem:
(defthm tree-listp-of-parse-*-in-either-range.trees (b* (((mv ?error? ?trees ?rest-input) (parse-*-in-either-range min1 max1 min2 max2 input))) (tree-listp trees)) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-parse-*-in-either-range.rest-input (b* (((mv ?error? ?trees ?rest-input) (parse-*-in-either-range min1 max1 min2 max2 input))) (nat-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm parse-*-in-either-range-of-nat-list-fix-input (equal (parse-*-in-either-range min1 max1 min2 max2 (nat-list-fix input)) (parse-*-in-either-range min1 max1 min2 max2 input)))
Theorem:
(defthm parse-*-in-either-range-nat-list-equiv-congruence-on-input (implies (acl2::nat-list-equiv input input-equiv) (equal (parse-*-in-either-range min1 max1 min2 max2 input) (parse-*-in-either-range min1 max1 min2 max2 input-equiv))) :rule-classes :congruence)
Theorem:
(defthm len-of-parse-*-in-either-range-linear (b* (((mv ?error? ?trees ?rest-input) (parse-*-in-either-range min1 max1 min2 max2 input))) (<= (len rest-input) (len input))) :rule-classes :linear)