/usr/share/acl2-6.3/books/tools/clone-stobj.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 | (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") (:SYSTEM . "tools/rulesets.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((20 RECORD-EXPANSION (DEFXDOC DEFSTOBJ-CLONE :PARENTS (STOBJS) :SHORT "Create a new stobj that is congruent to an existing (concrete or
abstract) stobj" :LONG "
<h2>Usage:</h2>
@({
(defstobj-clone new-stobj orig-stobj
:strsubst ((\"OLDSTR\" . \"NEWSTR\")
(\"ETC\" . \"ANDSOON\"))
:prefix \"NEW\"
:suffix \"++\"
:pkg mypkg::some-symbol
;; Only supported for abstract stobjs
:exports (new-get new-set new-acc new-upd))
})
<p>This defines a new stobj called @('NEW-STOBJ') that is congruent to the
existing stobj @('ORIG-STOBJ'). The keyword arguments all have to do with the
way the fields and accessor/updater functions of stobjs are renamed (they must
be given new names in the new stobj).</p>
<p>For an abstract stobj, the accessors/updaters are known as \"exports\". One
option for specifying their names in the new stobj is to provide the
@(':exports') argument, which should be a list of symbols corresponding to the
exported functions from the original abstract stobj. When this is provided,
the other keyword arguments are unused.</p>
<p>If @(':exports') is not used (which it can't be in cloning a concrete
stobj), then one or more of @(':strsubst'), @(':prefix'), and @(':suffix') must
be given. Prefix and suffix should be strings, and strsubst should be an alist
with string keys and values. The @(':pkg') symbol is optional and determines
into what package new symbols are interned; by default, it is the package of
the new stobj name.</p>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . DEFSTOBJ-CLONE) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS STOBJS) (:SHORT . "Create a new stobj that is congruent to an existing (concrete or
abstract) stobj") (:LONG . "
<h2>Usage:</h2>
@({
(defstobj-clone new-stobj orig-stobj
:strsubst ((\"OLDSTR\" . \"NEWSTR\")
(\"ETC\" . \"ANDSOON\"))
:prefix \"NEW\"
:suffix \"++\"
:pkg mypkg::some-symbol
;; Only supported for abstract stobjs
:exports (new-get new-set new-acc new-upd))
})
<p>This defines a new stobj called @('NEW-STOBJ') that is congruent to the
existing stobj @('ORIG-STOBJ'). The keyword arguments all have to do with the
way the fields and accessor/updater functions of stobjs are renamed (they must
be given new names in the new stobj).</p>
<p>For an abstract stobj, the accessors/updaters are known as \"exports\". One
option for specifying their names in the new stobj is to provide the
@(':exports') argument, which should be a list of symbols corresponding to the
exported functions from the original abstract stobj. When this is provided,
the other keyword arguments are unused.</p>
<p>If @(':exports') is not used (which it can't be in cloning a concrete
stobj), then one or more of @(':strsubst'), @(':prefix'), and @(':suffix') must
be given. Prefix and suffix should be strings, and strsubst should be an alist
with string keys and values. The @(':pkg') symbol is optional and determines
into what package new symbols are interned; by default, it is the package of
the new stobj name.</p>") (:FROM . "[books]/tools/clone-stobj.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC DEFSTOBJ-CLONE)))))))
NIL
(("/usr/share/acl2-6.3/books/tools/clone-stobj.lisp" "clone-stobj" "clone-stobj" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2018333540) ("/usr/share/acl2-6.3/books/tools/templates.lisp" "templates" "templates" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1985269982) ("/usr/share/acl2-6.3/books/tools/defmacfun.lisp" "defmacfun" "defmacfun" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 579393516) ("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/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/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))
1464439419
|