Template-subst
Template-subst 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 ACL2-count 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 *maptree-template*
'((progn (defun _treefn_ (x _other-args_)
(if (atom x)
(_leaffn_ x _other-args_)
(cons (_treefn_ (car x) _other-args_)
(_treefn_ (cdr x) _other-args_))))
(:@ :preserves-acl2-count
(defthm _treefn_-preserves-acl2-count
(equal (acl2-count (_treefn_ x _other-args_))
(acl2-count x)))))))
Now, to instantiate this template, we might do:
(template-subst *maptree-template*
:features '(:preserves-acl2-count)
:splice-alist '((_other-args_ . (n)))
:atom-alist '((_treefn_ . add-to-leaves)
(_leaffn_ . +))
:str-alist '(("_TREEFN_" . "ADD-TO-LEAVES"))
:subsubsts nil
:pkg-sym '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 atom-alist; if so, we return its
corresponding value.
- If the leaf is a symbol beginning with %, we remove that character
and re-intern it in its same package.
- If the leaf is a symbol, we apply str-alist as a substitution to its
symbol-name. If any substitutions are made, we intern the resulting
string in the package of pkg-sym.
- At each cons node of the tree:
- We check whether the car of the tree is a feature conditional, of the form
(:@ <feature-expr> 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 <subtemplates-name> subform)
or
(:@append <subtemplates-name> . subforms)
If so, we first look up the subtemplates-name 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 splice-alist, 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 add-to-leaves and _leaffn_ is
replaced with +
- by string substitution, the symbol _treefn_-preserves-acl2-count
is replaced with add-to-leaves-preserves-acl2-count
- each occurrence of _other-args_ is replaced by splicing in the list (n),
effectively replacing _other-args_ with n.
(Of course, the proof fails since our leaf transformation isn't actually
acl2-count 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 template-subst, 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 *maptree-template* example, then, since the feature
:preserves-acl2-count is present in our :features argument to
template-subst, we paste in the DEFTHM form. If it was not present, that
defthm would disappear.
