		Search-engine friendly clone of the ACL2 documentation.

Grammar

Abnf-tree-wrap

Wrap a CST into a nest of CSTs with the given rule names as roots (in the order given) and each with a single subtree, ending with the original tree.

Macro: abnf-tree-wrap

(defmacro abnf-tree-wrap (tree &rest rulenames)
  (cons 'abnf-tree-wrap-fn
        (cons tree
              (cons (cons 'list rulenames) 'nil))))

Definitions and Theorems

Function: abnf-tree-wrap-fn

(defun abnf-tree-wrap-fn (tree rulenames)
  (declare (xargs :guard (and (abnf::treep tree)
                              (string-listp rulenames))))
  (let ((__function__ 'abnf-tree-wrap-fn))
    (declare (ignorable __function__))
    (cond ((endp rulenames) (abnf::tree-fix tree))
          (t (abnf-tree-wrap-fn
                  (abnf::make-tree-nonleaf
                       :rulename? (abnf::rulename (car rulenames))
                       :branches (list (list tree)))
                  (cdr rulenames))))))

Theorem: treep-of-abnf-tree-wrap-fn

(defthm treep-of-abnf-tree-wrap-fn
  (b* ((wrapped-tree (abnf-tree-wrap-fn tree rulenames)))
    (abnf::treep wrapped-tree))
  :rule-classes :rewrite)

Theorem: abnf-tree-wrap-fn-of-tree-fix-tree

(defthm abnf-tree-wrap-fn-of-tree-fix-tree
  (equal (abnf-tree-wrap-fn (abnf::tree-fix tree)
                            rulenames)
         (abnf-tree-wrap-fn tree rulenames)))

Theorem: abnf-tree-wrap-fn-tree-equiv-congruence-on-tree

(defthm abnf-tree-wrap-fn-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (abnf-tree-wrap-fn tree rulenames)
                  (abnf-tree-wrap-fn tree-equiv rulenames)))
  :rule-classes :congruence)

Theorem: abnf-tree-wrap-fn-of-string-list-fix-rulenames

(defthm abnf-tree-wrap-fn-of-string-list-fix-rulenames
  (equal (abnf-tree-wrap-fn tree (str::string-list-fix rulenames))
         (abnf-tree-wrap-fn tree rulenames)))

Theorem: abnf-tree-wrap-fn-string-list-equiv-congruence-on-rulenames

(defthm abnf-tree-wrap-fn-string-list-equiv-congruence-on-rulenames
  (implies (str::string-list-equiv rulenames rulenames-equiv)
           (equal (abnf-tree-wrap-fn tree rulenames)
                  (abnf-tree-wrap-fn tree rulenames-equiv)))
  :rule-classes :congruence)