Parse a prose value notation.
(parse-prose-val input) → (mv error? tree? rest-input)
Function:
(defun parse-prose-val (input) (declare (xargs :guard (nat-listp input))) (seq input (tree-open-angle := (parse-ichar #\< input)) (trees-text := (parse-*-in-either-range 32 61 63 126 input)) (tree-close-angle := (parse-ichar #\> input)) (return (make-tree-nonleaf :rulename? *prose-val* :branches (list (list tree-open-angle) trees-text (list tree-close-angle))))))
Theorem:
(defthm maybe-msgp-of-parse-prose-val.error? (b* (((mv ?error? ?tree? ?rest-input) (parse-prose-val input))) (maybe-msgp error?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-prose-val.tree? (b* (((mv ?error? ?tree? ?rest-input) (parse-prose-val input))) (and (tree-optionp tree?) (implies (not error?) (treep tree?)) (implies error? (not tree?)))) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-parse-prose-val.rest-input (b* (((mv ?error? ?tree? ?rest-input) (parse-prose-val input))) (nat-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm len-of-parse-prose-val-linear (b* (((mv ?error? ?tree? ?rest-input) (parse-prose-val input))) (and (<= (len rest-input) (len input)) (implies (not error?) (< (len rest-input) (len input))))) :rule-classes :linear)
Theorem:
(defthm parse-prose-val-of-nat-list-fix-input (equal (parse-prose-val (nat-list-fix input)) (parse-prose-val input)))
Theorem:
(defthm parse-prose-val-nat-list-equiv-congruence-on-input (implies (acl2::nat-list-equiv input input-equiv) (equal (parse-prose-val input) (parse-prose-val input-equiv))) :rule-classes :congruence)