Major Section: MISCELLANEOUS
Many low-level ACL2 functions take and return ``tag trees'' or ``ttrees'' (pronounced ``tee-trees'') which contain various useful bits of information such as the lemmas used, the linearize assumptions made, etc.
Let a ``tagged pair'' be a list whose car is a symbol, called the ``tag,'' and whose cdr is an arbitrary object, called the ``tagged object.'' A ``tag tree'' is either nil, a tagged pair consed onto a tag tree, or a non-nil tag tree consed onto a tag tree.
Abstractly a tag tree represents a list of sets, each member set
having a name given by one of the tags occurring in the ttree. The
elements of the set named
tag are all of the objects tagged
tag in the tree. To cons a tagged pair
(tag . obj) onto a
tree is to
obj to the set corresponding to
cons two tag trees together is to union-equal the
corresponding sets. The concrete representation of the union so
produced has duplicates in it, but we feel free to ignore or delete
The beauty of this definition is that to combine two non-
trees you need do only one
The following function accumulates onto ans the set associated with a given tag in a ttree:
(defun tagged-objects (tag ttree ans) (cond ((null ttree) ans) ((symbolp (caar ttree)) ; ttree = ((tag . obj) . ttree) (tagged-objects tag (cdr ttree) (cond ((eq (caar ttree) tag) (add-to-set-equal (cdar ttree) ans)) (t ans)))) (t ; ttree = (ttree . ttree) (tagged-objects tag (cdr ttree) (tagged-objects tag (car ttree) ans)))))This function is defined as a :
PROGRAMmode function in ACL2.
The rewriter, for example, takes a term and a ttree (among other
things), and returns a new term, term', and new ttree, ttree'.
Term' is equivalent to term (under the current assumptions) and the
ttree' is an extension of ttree. If we focus just on the set
associated with the tag
LEMMA in the ttrees, then the set for
ttree' is the extension of that for ttree obtained by unioning into
it all the runes used by the rewrite. The set associated with
LEMMA can be obtained by
(tagged-objects 'LEMMA ttree nil).