Parse a
(parse-function-parameters token input) → (mv tree next-token rest-input)
Function:
(defun parse-function-parameters (token input) (declare (xargs :guard (and (abnf::tree-optionp token) (abnf::tree-listp input)))) (let ((__function__ 'parse-function-parameters)) (declare (ignorable __function__)) (b* (((pok< tree) (parse-function-parameter token input)) ((pok trees) (parse-*-comma-function-parameter token input))) (if (token-stringp "," token) (b* (((pok ctree) (parse-symbol "," token input))) (mv (abnf::make-tree-nonleaf :rulename? (abnf::rulename "function-parameters") :branches (list (list tree) trees (list (abnf::make-tree-nonleaf :rulename? nil :branches (list (list ctree)))))) token input)) (mv (abnf::make-tree-nonleaf :rulename? (abnf::rulename "function-parameters") :branches (list (list tree) trees (list (abnf::make-tree-nonleaf :rulename? nil :branches nil)))) token input)))))
Theorem:
(defthm tree-resultp-of-parse-function-parameters.tree (b* (((mv ?tree ?next-token ?rest-input) (parse-function-parameters token input))) (abnf::tree-resultp tree)) :rule-classes :rewrite)
Theorem:
(defthm tree-optionp-of-parse-function-parameters.next-token (b* (((mv ?tree ?next-token ?rest-input) (parse-function-parameters token input))) (abnf::tree-optionp next-token)) :rule-classes :rewrite)
Theorem:
(defthm tree-listp-of-parse-function-parameters.rest-input (b* (((mv ?tree ?next-token ?rest-input) (parse-function-parameters token input))) (abnf::tree-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-function-parameters-<= (b* (((mv ?tree ?next-token ?rest-input) (parse-function-parameters token input))) (<= (parsize next-token rest-input) (parsize token input))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-function-parameters-< (b* (((mv ?tree ?next-token ?rest-input) (parse-function-parameters token input))) (implies (not (reserrp tree)) (< (parsize next-token rest-input) (parsize token input)))) :rule-classes :linear)
Theorem:
(defthm parse-function-parameters-of-tree-option-fix-token (equal (parse-function-parameters (abnf::tree-option-fix token) input) (parse-function-parameters token input)))
Theorem:
(defthm parse-function-parameters-tree-option-equiv-congruence-on-token (implies (abnf::tree-option-equiv token token-equiv) (equal (parse-function-parameters token input) (parse-function-parameters token-equiv input))) :rule-classes :congruence)
Theorem:
(defthm parse-function-parameters-of-tree-list-fix-input (equal (parse-function-parameters token (abnf::tree-list-fix input)) (parse-function-parameters token input)))
Theorem:
(defthm parse-function-parameters-tree-list-equiv-congruence-on-input (implies (abnf::tree-list-equiv input input-equiv) (equal (parse-function-parameters token input) (parse-function-parameters token input-equiv))) :rule-classes :congruence)