Sees through lexeme and token trees to return token subtype trees.
(filter-and-reduce-lexeme-tree-to-subtoken-trees trees) → subtoken-trees
Discards without error trees other than "token" under "lexeme". However, if the structure under lexeme or token is incorrect, returns reserrp.
Function:
(defun filter-and-reduce-lexeme-tree-to-subtoken-trees (trees) (declare (xargs :guard (abnf::tree-listp trees))) (let ((__function__ 'filter-and-reduce-lexeme-tree-to-subtoken-trees)) (declare (ignorable __function__)) (if (mbt (abnf::tree-listp trees)) (b* (((when (endp trees)) nil) (first-tree (car trees)) (rest-trees (cdr trees)) (first-tree-under-lexeme (check-and-deref-tree-lexeme? first-tree)) ((when (reserrp first-tree-under-lexeme)) (reserrf "bad structure under lexeme")) (processed-rest-trees (filter-and-reduce-lexeme-tree-to-subtoken-trees rest-trees)) ((when (reserrp processed-rest-trees)) (reserrf "bad structure under lexeme")) ((unless (abnf::tree-listp processed-rest-trees)) (reserrf "type error that should not happen")) ((unless (is-tree-rulename? first-tree-under-lexeme "token")) processed-rest-trees) (first-tree-under-token (check-and-deref-tree-token? first-tree-under-lexeme)) ((when (reserrp first-tree-under-token)) (reserrf "bad structure under token")) ((unless (abnf::treep first-tree-under-token)) (reserrf "type error that should not happen 2"))) (cons first-tree-under-token processed-rest-trees)) 'nil)))
Theorem:
(defthm tree-list-resultp-of-filter-and-reduce-lexeme-tree-to-subtoken-trees (b* ((subtoken-trees (filter-and-reduce-lexeme-tree-to-subtoken-trees trees))) (abnf::tree-list-resultp subtoken-trees)) :rule-classes :rewrite)