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