Templatesubst
Templatesubst is a function for manipulating templates that may be
used to generate events.
As an example, suppose that we want to develop a general way to map
a function over all of the atoms of a tree. Also, when the function to be run
on the leaves is ACL2count preserving, we'd like to prove that the tree
function is as well. So we might define the following constant as a template
for generating these sorts of functions/proofs:
(defconst *maptreetemplate*
'((progn (defun _treefn_ (x _otherargs_)
(if (atom x)
(_leaffn_ x _otherargs_)
(cons (_treefn_ (car x) _otherargs_)
(_treefn_ (cdr x) _otherargs_))))
(:@ :preservesacl2count
(defthm _treefn_preservesacl2count
(equal (acl2count (_treefn_ x _otherargs_))
(acl2count x)))))))
Now, to instantiate this template, we might do:
(templatesubst *maptreetemplate*
:features '(:preservesacl2count)
:splicealist '((_otherargs_ . (n)))
:atomalist '((_treefn_ . addtoleaves)
(_leaffn_ . +))
:stralist '(("_TREEFN_" . "ADDTOLEAVES"))
:subsubsts nil
:pkgsym 'acl2::asdf)
Substitution
Filling out the template involves recursively traversing the tree checking
for various kinds of substitutions to make, as follows.

At each atom in the tree:
 We check whether the leaf is bound in atomalist; if so, we return its
corresponding value.
 If the leaf is a symbol beginning with %, we remove that character
and reintern it in its same package.
 If the leaf is a symbol, we apply stralist as a substitution to its
symbolname. If any substitutions are made, we intern the resulting
string in the package of pkgsym.
 At each cons node of the tree:
 We check whether the car of the tree is a feature conditional, of the form
(:@ <featureexpr> forms ...)
If so, we evaluate the feature expression (see the section on features below)
and if it is satisfied, recursive substitute on the append of the forms onto
the cdr of the tree; otherwise, just recursively substitute the cdr of the
tree and ignore the car.
 We check whether the car of the tree is a repetition operator, of the form
(:@proj <subtemplatesname> subform)
or
(:@append <subtemplatesname> . subforms)
If so, we first look up the subtemplatesname in the subsubsts field of
our substitution. The value should be a list of other substitution objects.
These substitutions are each applied to subforms. For the :@proj case,
the subform is expanded with to each subtemplate and the results are consed
into a list; for the :@append case, all subforms are expanded with each
subtemplate and the results are appended together. In either case, the
resulting list is appended to the cdr and recursively substituted.
 We check whether the car of the tree is bound in splicealist, and if so
we append its corresponding value to the recursive substitution of the
cdr of the tree.
 Otherwise, we return the cons of the recursive substitutions into the
car and cdr.
Therefore, in our example we make the following replacements:
 the symbol _treefn_ is replaced with addtoleaves and _leaffn_ is
replaced with +
 by string substitution, the symbol _treefn_preservesacl2count
is replaced with addtoleavespreservesacl2count
 each occurrence of _otherargs_ is replaced by splicing in the list (n),
effectively replacing _otherargs_ with n.
(Of course, the proof fails since our leaf transformation isn't actually
acl2count preserving.)
Feature Processing
When :@ occurs as the first element of a list, the second element of
that list is treated as a feature expression, much like in the #+ reader
macro. A feature expression is:
 A symbol
 (NOT <subexpression>)
 (AND [<subexpression>]*)
 (OR [<subexpression>]*])
When templates are expanded using templatesubst, each symbol present
in the features list becomes true, any not present become false, and the
resulting Boolean expression is evaluated. If the feature expression evaluates
to true, the rest of the list (not including the feature expression) is spliced
into the template and recursively preprocessed.
In our *maptreetemplate* example, then, since the feature
:preservesacl2count is present in our :features argument to
templatesubst, we paste in the DEFTHM form. If it was not present, that
defthm would disappear.