		Search-engine friendly clone of the ACL2 documentation.

Abnf-tree-utilities

Check-tree-nonleaf

Check if an ABNF tree has a given rule name or no rule name as root, returning the list of lists of subtrees if successful.

Signature
(check-tree-nonleaf tree rulename?) → sub
Arguments: tree — Guard (abnf::treep tree).; rulename? — Guard (maybe-stringp rulename?).
Returns: sub — Type (abnf::tree-list-list-resultp sub).

Definitions and Theorems

Function: check-tree-nonleaf

(defun check-tree-nonleaf (tree rulename?)
 (declare (xargs :guard (and (abnf::treep tree)
                             (maybe-stringp rulename?))))
 (let ((__function__ 'check-tree-nonleaf))
   (declare (ignorable __function__))
   (if (and (abnf::tree-case tree :nonleaf)
            (equal (abnf::tree-nonleaf->rulename? tree)
                   (if (maybe-string-fix rulename?)
                       (abnf::rulename (maybe-string-fix rulename?))
                     nil)))
       (abnf::tree-nonleaf->branches tree)
     (reserrf (if (abnf::tree-case tree :nonleaf)
                  (list :required (maybe-string-fix rulename?)
                        :found (abnf::tree-nonleaf->rulename? tree))
                (list :required
                      :nonleaf (maybe-string-fix rulename?)
                      :found (abnf::tree-fix tree)))))))

Theorem: tree-list-list-resultp-of-check-tree-nonleaf

(defthm tree-list-list-resultp-of-check-tree-nonleaf
  (b* ((sub (check-tree-nonleaf tree rulename?)))
    (abnf::tree-list-list-resultp sub))
  :rule-classes :rewrite)

Theorem: tree-count-of-check-tree-nonleaf

(defthm tree-count-of-check-tree-nonleaf
  (b* ((?sub (check-tree-nonleaf tree rulename?)))
    (implies (not (reserrp sub))
             (< (abnf::tree-list-list-count sub)
                (abnf::tree-count tree))))
  :rule-classes :linear)

Theorem: check-tree-nonleaf-of-tree-fix-tree

(defthm check-tree-nonleaf-of-tree-fix-tree
  (equal (check-tree-nonleaf (abnf::tree-fix tree)
                             rulename?)
         (check-tree-nonleaf tree rulename?)))

Theorem: check-tree-nonleaf-tree-equiv-congruence-on-tree

(defthm check-tree-nonleaf-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (check-tree-nonleaf tree rulename?)
                  (check-tree-nonleaf tree-equiv rulename?)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-of-maybe-string-fix-rulename?

(defthm check-tree-nonleaf-of-maybe-string-fix-rulename?
  (equal (check-tree-nonleaf tree (maybe-string-fix rulename?))
         (check-tree-nonleaf tree rulename?)))

Theorem: check-tree-nonleaf-maybe-string-equiv-congruence-on-rulename?

(defthm
      check-tree-nonleaf-maybe-string-equiv-congruence-on-rulename?
  (implies (acl2::maybe-string-equiv rulename? rulename?-equiv)
           (equal (check-tree-nonleaf tree rulename?)
                  (check-tree-nonleaf tree rulename?-equiv)))
  :rule-classes :congruence)