Defsection
Fancy (encapsulate nil ...) with a name and xdoc support.
General Form
(defsection name
[:parents parents]
[:short short]
[:long long]
[:autodoc autodoc]
[:extension topic]
[:set-as-default-parent t/nil]
... events and commentary ...)
Example
(defsection foo
:parents (parent1 parent2 ...)
:short "@(call foo) is like @(see bar), but better when..."
:long "<p>The main differences between @('foo') and @('bar') are ...</p>"
(defund foo (x) ...)
(local (in-theory (enable foo)))
(defthm foo-thm1 ...)
(defthm foo-thm2 ...)
"<p>NOTE: the next theorem is really useful, but we keep it disabled
because it gets too expensive when...</p>"
(defthmd foo-thm3 ...))
Note: this example might be better written as a ACL2::define,
which is much like a defsection but has additional features.
Overview
Like an encapsulate, a defsection introduces a new scope for
local events. This is often useful when you are trying to prove a
theorem that requires some lemmas: by proving the lemmas locally, you can
prevent them from affecting the rest of your book.
It is often useful to organize books into sections. There are a few minor
reasons you might prefer using defsection for this, instead of plain
encapsulates. For instance,
- It is easier to identify in the :pbt history, and
- It indents more nicely than encapsulate in a vanilla emacs.
But the main reasons to use defsection are its documentation features.
The definitions and theorems within a section can be automatically
included in the documentation page for that section, along with any running
commentary. This helps to avoid copying-and-pasting code into the manual, and
keeps it up-to-date as the code changes.
Ordinary Sections
The :parents, :short, and :long keywords are optional. If
any of these keywords are provided, they will be used to introduce a defxdoc command; otherwise no documentation will be generated.
By default, the :long string you give will be automatically extended
with a "Definitions and Theorems" part that lists all of the (non-local,
non-redundant) definitions and theorems introduced in the section.
For instance, in the above example, the :long field would be extended
with:
<h3>Definition and Theorems</h3>
@(def foo)
@(thm foo-thm1)
@(thm foo-thm2)
<p>NOTE: the next theorem is really useful, but we keep it disabled
because it gets too expensive when...</p>
@(thm foo-thm3)
If you do not want this automatic documentation, you can turn it off with
:autodoc nil.
If you want the section name to be the default parent for the encapsulated
events, then you can pass :set-as-default-parent t. Then (local
(xdoc::set-default-parents name)) will be inserted at the beginning of the
events, where "name" is the name of the section.
Extended Sections
The :extension keyword allows you to say that this section is a
continuation of a previously introduced concept.
When :extension topic is provided, then topic must be the name of
a previously documented xdoc section, and you are not allowed to use
:parents or :short since the topic already exists. Note that whereas
topics can have multiple parents, you can only extend a single topic at a
time.
The main purpose of an :extension section is to add additional
documentation, either via the :long string or via the automatic events and
commentary. The documentation obtained this way is just appended onto the
existing :long for the topic.
For example, say we have already defined the above foo section in some
"basic" book. We might then want to add some additional "advanced"
theorems about it in some other book. We could do this via:
(defsection advanced-theorems-about-foo
:extension foo
"<p>Additional theorems are also available in the @('advanced') book. (We
don't include these in the basic book since they take a long time to
prove.)</p>"
(defthm foo-thm4 ...)
(defthm foo-thm5 ...))
This will result in the commentary and definitions of foo-thm4 and
foo-thm5 being added onto the end of the documentation for foo.
Subtopics
- Throw-away-keyword-parts
- Throw away any keyword arguments and their values from a macro
argument list.
- Extract-keyword-from-args
- Get the value for a keyword argument like :foo value.
