		Search-engine friendly clone of the ACL2 documentation.

Grammar

Abnf-tree-with-root-p

Recognize CSTs whose root is the given rule name, for the ABNF grammar of PFCS.

Signature
(abnf-tree-with-root-p tree rulename) → yes/no
Arguments: rulename — Guard (stringp rulename).
Returns: yes/no — Type (booleanp yes/no).

This implements the definition of sets of CSTs that match given rule names.

This is a useful abbreviation for a more verbose conjunction of ABNF predicates with more verbose arguments.

The tree is terminated, i.e. it has natural numbers at its leaves, not rule names. These natural numbers are ascii codes because the grammar satisfies abnf::rulelist-in-termset-p for the set (integers-from-to 0 127) as proved in *grammar*.

Definitions and Theorems

Function: abnf-tree-with-root-p

(defun abnf-tree-with-root-p (tree rulename)
  (declare (xargs :guard (stringp rulename)))
  (and (abnf::treep tree)
       (abnf::tree-terminatedp tree)
       (abnf::tree-match-element-p
            tree
            (abnf::element-rulename (abnf::rulename rulename))
            *grammar*)))

Theorem: booleanp-of-abnf-tree-with-root-p

(defthm booleanp-of-abnf-tree-with-root-p
  (b* ((yes/no (abnf-tree-with-root-p tree rulename)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: abnf-treep-when-abnf-tree-with-root-p

(defthm abnf-treep-when-abnf-tree-with-root-p
  (implies (abnf-tree-with-root-p tree rulename)
           (abnf::treep tree)))

Theorem: not-abnf-tree-with-root-p-of-nil

(defthm not-abnf-tree-with-root-p-of-nil
  (not (abnf-tree-with-root-p nil rulename)))

Theorem: abnf-tree-with-root-p-of-str-fix-rulename

(defthm abnf-tree-with-root-p-of-str-fix-rulename
  (equal (abnf-tree-with-root-p tree (str-fix rulename))
         (abnf-tree-with-root-p tree rulename)))

Theorem: abnf-tree-with-root-p-streqv-congruence-on-rulename

(defthm abnf-tree-with-root-p-streqv-congruence-on-rulename
  (implies (acl2::streqv rulename rulename-equiv)
           (equal (abnf-tree-with-root-p tree rulename)
                  (abnf-tree-with-root-p tree rulename-equiv)))
  :rule-classes :congruence)