Parse an
(parse-program-id token input) → (mv tree next-token rest-input)
Function:
(defun parse-program-id (token input) (declare (xargs :guard (and (abnf::tree-optionp token) (abnf::tree-listp input)))) (let ((__function__ 'parse-program-id)) (declare (ignorable __function__)) (b* (((pok tree1) (parse-identifier token input)) ((pok tree2) (parse-symbol "." token input)) ((pok tree3) (parse-identifier token input))) (mv (abnf::make-tree-nonleaf :rulename? (abnf::rulename "program-id") :branches (list (list tree1) (list tree2) (list tree3))) token input))))
Theorem:
(defthm tree-resultp-of-parse-program-id.tree (b* (((mv ?tree ?next-token ?rest-input) (parse-program-id token input))) (abnf::tree-resultp tree)) :rule-classes :rewrite)
Theorem:
(defthm tree-optionp-of-parse-program-id.next-token (b* (((mv ?tree ?next-token ?rest-input) (parse-program-id token input))) (abnf::tree-optionp next-token)) :rule-classes :rewrite)
Theorem:
(defthm tree-listp-of-parse-program-id.rest-input (b* (((mv ?tree ?next-token ?rest-input) (parse-program-id token input))) (abnf::tree-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-program-id-<= (b* (((mv ?tree ?next-token ?rest-input) (parse-program-id token input))) (<= (parsize next-token rest-input) (parsize token input))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-program-id-< (b* (((mv ?tree ?next-token ?rest-input) (parse-program-id token input))) (implies (not (reserrp tree)) (< (parsize next-token rest-input) (parsize token input)))) :rule-classes :linear)
Theorem:
(defthm parse-program-id-of-tree-option-fix-token (equal (parse-program-id (abnf::tree-option-fix token) input) (parse-program-id token input)))
Theorem:
(defthm parse-program-id-tree-option-equiv-congruence-on-token (implies (abnf::tree-option-equiv token token-equiv) (equal (parse-program-id token input) (parse-program-id token-equiv input))) :rule-classes :congruence)
Theorem:
(defthm parse-program-id-of-tree-list-fix-input (equal (parse-program-id token (abnf::tree-list-fix input)) (parse-program-id token input)))
Theorem:
(defthm parse-program-id-tree-list-equiv-congruence-on-input (implies (abnf::tree-list-equiv input input-equiv) (equal (parse-program-id token input) (parse-program-id token input-equiv))) :rule-classes :congruence)