Check if the ABNF tree is a nonleaf for rule "lexeme", extracting its component tree (token, comment, or whitespace) if successful. If not successful, returns a reserrp.
(check-and-deref-tree-lexeme? tree) → subtree
Function:
(defun check-and-deref-tree-lexeme? (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'check-and-deref-tree-lexeme?)) (declare (ignorable __function__)) (b* (((unless (abnf::tree-case tree :nonleaf)) (reserrf "should be lexeme tree, but is not a nonleaf")) (rulename? (abnf::tree-nonleaf->rulename? tree)) ((unless (equal rulename? (abnf::rulename "lexeme"))) (reserrf "tree should have rulename lexeme, but does not")) (branches (abnf::tree-nonleaf->branches tree)) ((unless (equal (len branches) 1)) (reserrf "lexeme tree branches should have exactly one list")) (repetition (car branches)) ((unless (equal (len repetition) 1)) (reserrf "lexeme repetition should have exactly one subtree")) ((unless (abnf::treep (car repetition))) (reserrf "lexeme repetition item should be an ABNF tree"))) (car repetition))))
Theorem:
(defthm tree-resultp-of-check-and-deref-tree-lexeme? (b* ((subtree (check-and-deref-tree-lexeme? tree))) (abnf::tree-resultp subtree)) :rule-classes :rewrite)