templates

(in-package "ACL2")

(defxdoc template-subst
  :parents (macro-libraries)
  :short "Template-subst is a function for manipulating templates that may be
used to generate events."
  :long "<p>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 @(see 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:</p>

@({
    (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)))))))
})

<p>Now, to instantiate this template, we might do:</p>

@({
    (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)
})

<h3>Substitution</h3>
<p>Filling out the template involves recursively traversing the tree checking
for various kinds of substitutions to make, as follows.</p>

<ul>

<li>
At each atom in the tree:
<ul>
<li> We check whether the leaf is bound in atom-alist; if so, we return its
    corresponding value.</li>
<li> If the leaf is a symbol beginning with @('%'), we remove that character
  and re-intern it in its same package.</li>
<li> 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.</li>
</ul></li>


<li>At each cons node of the tree:
<ul>
<li> 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.</li>

<li> 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.</li>

<li> 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.</li>
<li> Otherwise, we return the cons of the recursive substitutions into the
    car and cdr.</li>
</ul></li>


</ul>

<p>Therefore, in our example we make the following replacements:</p>
<ul>
<li> the symbol _treefn_ is replaced with add-to-leaves and _leaffn_ is
    replaced with +</li>
<li> by string substitution, the symbol _treefn_-preserves-acl2-count
    is replaced with add-to-leaves-preserves-acl2-count</li>
<li> each occurrence of _other-args_ is replaced by splicing in the list (n),
    effectively replacing _other-args_ with n.</li>
</ul>
<p>(Of course, the proof fails since our leaf transformation isn't actually
 acl2-count preserving.)</p>

<h3>Feature Processing</h3>
<p>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:</p>

<ul>
<li>A symbol</li>
<li>@('(NOT <subexpression>)')</li>
<li>@('(AND [<subexpression>]*)')</li>
<li>@('(OR [<subexpression>]*])')</li>
</ul>

<p>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.</p>

<p>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.</p>

")

(program)

(make-event (if (equal (mv-list 2
        (tmpl-str-sublis '(("foo" . "bar") ("fuz" "biz" . pkg) ("bar" . "boz"))
          "afuzbarcfoobbarfooafuz"))
      (list "abizbozcbarbbozbarabiz" 'pkg))
    '(value-triple :ok)
    (er hard? 'tmpl-str-sublis "Test failed~%")))

(def-primitive-aggregate tmplsubst
  (atoms strs string-strs pkg-sym splices features subsubsts))

(defmacfun template-subst
  (tree &key
    features
    subsubsts
    splice-alist
    atom-alist
    str-alist
    string-str-alist
    (pkg-sym ''foo))
  (template-subst-top tree
    (make-tmplsubst :features features
      :splices splice-alist
      :atoms atom-alist
      :strs str-alist
      :string-strs string-str-alist
      :subsubsts subsubsts
      :pkg-sym pkg-sym)))

(logic)