Parse a natural number in one of two given ranges into a tree that matches a group consisting of an alternation of the corresponding range numeric value notations.
(parse-in-either-range min1 max1 min2 max2 input) → (mv error? tree? 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-range min1 max1 input)) (return (make-tree-nonleaf :rulename? nil :branches (list (list tree))))) ((tree := (parse-in-range min2 max2 input)) (return (make-tree-nonleaf :rulename? nil :branches (list (list tree)))))))
Theorem:
(defthm maybe-msgp-of-parse-in-either-range.error? (b* (((mv ?error? ?tree? ?rest-input) (parse-in-either-range min1 max1 min2 max2 input))) (maybe-msgp error?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-in-either-range.tree? (b* (((mv ?error? ?tree? ?rest-input) (parse-in-either-range min1 max1 min2 max2 input))) (and (tree-optionp tree?) (implies (not error?) (treep tree?)) (implies error? (not tree?)))) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-parse-in-either-range.rest-input (b* (((mv ?error? ?tree? ?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? ?tree? ?rest-input) (parse-in-either-range min1 max1 min2 max2 input))) (and (<= (len rest-input) (len input)) (implies (not error?) (< (len rest-input) (len input))))) :rule-classes :linear)