# Treep

Recognize XDOC trees.

These are the trees produced by the XDOC constructors.

These trees have strings at the leaves.
A non-leaf node consists of one of the following:

- A single keyword.
This represents either
(i) a preprocessor directive
or (ii) a concatenation of subtrees
without a surrounding XML tag or preprocessor directive.
Examples of (i) are :@def and :@{}.
The keyword :&& is used for (ii).
The latter is useful to treat sequences of trees as single trees.
- A
`cons` pair
whose `car` is a keyword and
whose `cdr` is an alist from keywords to subtrees.
This represents an XML tag,
identified by the keyword at the `car`,
with the attributes represented by the alist at the `cdr`.
Examples are (:p) and (:img (:src ...)).
The alist may often be nil.
The values of the attributes are recursively represented as subtrees,
but there may often be a single string subtree per attribute.

In some sense,
the semantics of XDOC trees is defined by their conversion to flat strings.
See `tree-to-string`.

### Definitions and Theorems

**Function: **treep

(defun treep (x)
(or (stringp x)
(and (true-listp x)
(consp x)
(or (keywordp (car x))
(tree-tagp (car x)))
(tree-listp (cdr x)))))

**Function: **tree-listp

(defun tree-listp (x)
(cond ((atom x) (eq x nil))
(t (and (treep (car x))
(tree-listp (cdr x))))))

**Function: **tree-tagp

(defun tree-tagp (x)
(and (consp x)
(keywordp (car x))
(keyword-tree-alistp (cdr x))))

**Function: **keyword-tree-alistp

(defun keyword-tree-alistp (x)
(cond ((atom x) (eq x nil))
(t (and (consp (car x))
(keywordp (car (car x)))
(treep (cdr (car x)))
(keyword-tree-alistp (cdr x))))))

**Theorem: **treep-when-stringp

(defthm treep-when-stringp
(implies (stringp x) (treep x)))

**Theorem: **tree-listp-when-string-listp

(defthm tree-listp-when-string-listp
(implies (string-listp x)
(tree-listp x)))

**Theorem: **true-listp-when-tree-listp

(defthm true-listp-when-tree-listp
(implies (tree-listp x) (true-listp x))
:rule-classes :forward-chaining)

**Theorem: **treep-of-cons

(defthm treep-of-cons
(equal (treep (cons x y))
(and (or (keywordp x) (tree-tagp x))
(tree-listp y))))

**Theorem: **tree-listp-of-cons

(defthm tree-listp-of-cons
(equal (tree-listp (cons x y))
(and (treep x) (tree-listp y))))

**Theorem: **tagp-of-cons

(defthm tagp-of-cons
(equal (tree-tagp (cons x y))
(and (keywordp x)
(keyword-tree-alistp y))))

**Theorem: **keyword-tree-alistp-of-cons

(defthm keyword-tree-alistp-of-cons
(equal (keyword-tree-alistp (cons x y))
(and (consp x)
(keywordp (car x))
(treep (cdr x))
(keyword-tree-alistp y))))