/usr/share/acl2-6.3/books/tools/templates.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "XDOC" (SET-DIFFERENCE-EQ (UNION-EQ (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (B* QUIT EXIT VALUE DEFXDOC DEFXDOC-RAW MACRO-ARGS XDOC-EXTEND DEFSECTION DEFSECTION-PROGN CUTIL LNFIX SET-DEFAULT-PARENTS GETPROP FORMALS JUSTIFICATION DEF-BODIES CURRENT-ACL2-WORLD DEF-BODY ACCESS THEOREM UNTRANSLATED-THEOREM GUARD XDOC XDOC! UNQUOTE UNDOCUMENTED ASSERT! TOP EXPLODE IMPLODE))) (QUOTE NIL)) NIL ((:SYSTEM . "xdoc/portcullis.lisp") (:SYSTEM . "xdoc/top.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((4 RECORD-EXPANSION (DEFXDOC TEMPLATE-SUBST :PARENTS (MACRO-LIBRARIES) :SHORT "Process a template to generate some events" :LONG "
<p>Template-subst is a function for manipulating templates that
may be used to generate events. For example, we might want to generate a
function that runs some function on all the atoms of a tree. Also, if 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)
:subtree-alist nil
:splice-alist '((_other-args_ . (n)))
:atom-alist '((_treefn_ . add-to-leaves)
(_leaffn_ . +))
:str-alist '((\"_TREEFN_\" . \"ADD-TO-LEAVES\"))
:pkg-sym 'acl2::asdf)
})
</p>
<p>The process has two main steps.</p>
<h3>Preprocessing</h3>
<p>The first step involves the :features argument and
parts of the template beginning with :@. It does something like the #+
reader macro in Lisp. 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.</p>
<p>A feature expression is:
<ul>
<li>a symbol</li>
<li>(NOT <subexpression>)</li>
<li>(AND [<subexpression>])</li>
<li>(OR [<subexpression>])</li>
</ul></p>
<p>Each symbol present in the features list becomes true, any not present
become false, and the resulting Boolean expression is evaluated. If it
evaluates to T, the rest of the list (not including the feature expression)
is spliced into the template and recursively preprocessed.
Therefore in our example, 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 effectively disappear.
</p>
<h3>Substitution</h3>
<p> The second step involves substitution of various kinds into the tree.</p>
<ul>
<li>At each cons node of the tree:
<ul>
<li> We check whether the tree is bound in subtree-alist, and if so we
return its corresponding value.</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>
<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, 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>
</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>
") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . TEMPLATE-SUBST) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS MACRO-LIBRARIES) (:SHORT . "Process a template to generate some events") (:LONG . "
<p>Template-subst is a function for manipulating templates that
may be used to generate events. For example, we might want to generate a
function that runs some function on all the atoms of a tree. Also, if 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)
:subtree-alist nil
:splice-alist '((_other-args_ . (n)))
:atom-alist '((_treefn_ . add-to-leaves)
(_leaffn_ . +))
:str-alist '((\"_TREEFN_\" . \"ADD-TO-LEAVES\"))
:pkg-sym 'acl2::asdf)
})
</p>
<p>The process has two main steps.</p>
<h3>Preprocessing</h3>
<p>The first step involves the :features argument and
parts of the template beginning with :@. It does something like the #+
reader macro in Lisp. 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.</p>
<p>A feature expression is:
<ul>
<li>a symbol</li>
<li>(NOT <subexpression>)</li>
<li>(AND [<subexpression>])</li>
<li>(OR [<subexpression>])</li>
</ul></p>
<p>Each symbol present in the features list becomes true, any not present
become false, and the resulting Boolean expression is evaluated. If it
evaluates to T, the rest of the list (not including the feature expression)
is spliced into the template and recursively preprocessed.
Therefore in our example, 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 effectively disappear.
</p>
<h3>Substitution</h3>
<p> The second step involves substitution of various kinds into the tree.</p>
<ul>
<li>At each cons node of the tree:
<ul>
<li> We check whether the tree is bound in subtree-alist, and if so we
return its corresponding value.</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>
<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, 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>
</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>
") (:FROM . "[books]/tools/templates.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC TEMPLATE-SUBST)))))) (8 RECORD-EXPANSION (MAKE-EVENT (IF (EQUAL (MV-LIST 2 (TMPL-STR-SUBLIS (QUOTE (("foo" . "bar") ("fuz" "biz" . PKG) ("bar" . "boz"))) "afuzbarcfoobbarfooafuz")) (LIST "abizbozcbarbbozbarabiz" (QUOTE PKG))) (QUOTE (VALUE-TRIPLE :OK)) (ER HARD? (QUOTE TMPL-STR-SUBLIS) "Test failed~%"))) (VALUE-TRIPLE :OK)) (16 RECORD-EXPANSION (LOCAL (PROGN (DEFCONST *MAPTREE-TEMPLATE* (QUOTE (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))))))) (MAKE-EVENT (IF (EQUAL (TEMPLATE-SUBST *MAPTREE-TEMPLATE* :FEATURES (QUOTE (:PRESERVES-ACL2-COUNT)) :SUBTREE-ALIST NIL :SPLICE-ALIST (QUOTE ((_OTHER-ARGS_ N))) :ATOM-ALIST (QUOTE ((_TREEFN_ . ADD-TO-LEAVES) (_LEAFFN_ . +))) :STR-ALIST (QUOTE (("_TREEFN_" . "ADD-TO-LEAVES"))) :PKG-SYM (QUOTE ASDF)) (QUOTE (PROGN (DEFUN ADD-TO-LEAVES (X N) (IF (ATOM X) (+ X N) (CONS (ADD-TO-LEAVES (CAR X) N) (ADD-TO-LEAVES (CDR X) N)))) (DEFTHM ADD-TO-LEAVES-PRESERVES-ACL2-COUNT (EQUAL (ACL2-COUNT (ADD-TO-LEAVES X N)) (ACL2-COUNT X)))))) (QUOTE (VALUE-TRIPLE :OK)) (ER HARD? (QUOTE TEMPLATE-SUBST) "Test failed~%"))))) (LOCAL (VALUE-TRIPLE :ELIDED))))
NIL
(("/usr/share/acl2-6.3/books/tools/templates.lisp" "templates" "templates" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1985269982) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/tools/defmacfun.lisp" "defmacfun" "defmacfun" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 579393516) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439))
1107062777
|