Defpkg
Define a new symbol package
Example:
(defpkg "MY-PKG"
(union-eq *acl2-exports*
*common-lisp-symbols-from-main-lisp-package*))
General Form:
(defpkg "name" term doc-string)
where "name" is a non-empty string, none of whose characters is
lower case, that names the package to be created; term is a variable-free
expression that evaluates to a list of symbols, where no two distinct symbols
in the list may have the same symbol-name, to be imported into the
newly created package; and doc-string, if non-nil, is an optional
string that can provide documentation but is essentially ignored by ACL2. The
name of the new package must be ``new'': the host lisp must not contain any
package of that name. There are two exceptions to this newness rule,
discussed at the end of this documentation.
(There is actually an additional argument, book-path, that is used for
error reporting but has no logical content. Users should generally ignore
this argument, as well as the rest of this sentence: a book-path will be
specified for defpkg events added by ACL2 to the portcullis of
a book's certificate; see hidden-death-package.)
There are two restrictions on term aside from those mentioned above.
Both restrictions relate to ancestral uses of apply$ in term,
i.e., uses of apply$ by term or any function that might be called
during the evaluation of term. First, only badged primitive functions
may be applied. See badge for a way to obtain the complete list of
badged primitives. Second, loop$ and lambda$ may not be used
anywhere in the ancestry of term. See ignored-attachment and
prohibition-of-loop$-and-lambda$ for more discussion.
Defpkg forms can be entered at the top-level of the ACL2 command loop. They should not occur in books (see certify-book).
After a successful defpkg it is possible to ``intern'' a string into
the package using intern-in-package-of-symbol. The result is a symbol
that is in the indicated package, provided the imports allow it. For example,
suppose 'my-pkg::abc is a symbol whose symbol-package-name is
"MY-PKG". Suppose further that the imports specified in the
defpkg for "MY-PKG" do not include a symbol whose symbol-name is "XYZ". Then
(intern-in-package-of-symbol "XYZ" 'my-pkg::abc)
returns a symbol whose symbol-name is "XYZ" and whose symbol-package-name is "MY-PKG". On the other hand, if the imports to
the defpkg does include a symbol with the name "XYZ", say in the
package "LISP", then
(intern-in-package-of-symbol "XYZ" 'my-pkg::abc)
returns that symbol (which is uniquely determined by the restriction on the
imports list above). See intern-in-package-of-symbol.
Upon admission of a defpkg event, the function pkg-imports is
extended to compute a list of all symbols imported into the given package,
without duplicates. If "MY-PKG" is the name of the new package and
symb is the symbol returned by (intern (concatenate 'string "MY-PKG"
"-PACKAGE") "ACL2"), then symb denotes the rewrite rule
added for the package. For example, here is a display of that rule for the
event (defpkg "MY-PKG" '(a b)).
ACL2 !>:pl (pkg-imports "MY-PKG")
(:REWRITE MY-PKG-PACKAGE)
New term: '(A B)
Hypotheses: <none>
Equiv: EQUAL
Substitution: NIL
....
Defpkg is the only means by which an ACL2 user can create a new
package or specify what it imports. That is, ACL2 does not support the Common
Lisp functions make-package or import. Currently, ACL2 does not
support exporting at all.
The Common Lisp function intern is weakly supported by ACL2; see
intern. A more general form of that function is also provided: see
intern$.
We now explain the two exceptions to the newness rule for package names.
The careful experimenter will note that if a package is created with a
defpkg that is subsequently undone, the host lisp system will contain the
created package even after the undo. Because ACL2 hangs onto worlds
after they have been undone, e.g., to implement :oops but, more
importantly, to implement error recovery, we cannot actually destroy a package
upon undoing it. Thus, the first exception to the newness rule is that
name is allowed to be the name of an existing package if that package was
created by an undone defpkg and the newly proposed set of imports is
identical to the old one. See package-reincarnation-import-restrictions. This exception does not violate
the spirit of the newness rule, since one is disinclined to believe in the
existence of undone packages. The second exception is that name is
allowed to be the name of an existing package if the package was created by a
defpkg with identical set of imports. That is, it is permissible to
execute ``redundant'' defpkg commands. The redundancy test is
based on the values of the two import forms (comparing them after sorting and
removing duplicates), not on the forms themselves.
Note that defpkg performs evaluation in so-called safe-mode,
which can slow down evaluation significantly but checks guards on
primitives.
Finally, we explain why we require the package name not to contain
lower-case characters. We have seen at least one implementation that handled
lower-case package names incorrectly. Since we see no need for lower-case
characters in package names, which can lead to confusion anyhow (note for
example that foo::bar is a symbol whose symbol-package-name is
"FOO", not "foo"), we simply disallow them.
NOTE: Also see managing-ACL2-packages for contributed documentation
on managing ACL2 packages.
Subtopics
- Prohibition-of-loop$-and-lambda$
- Certain events do not allow loop$s or lambda$s
- Ignored-attachment
- Why attachments are sometimes not used
- Hidden-death-package
- Handling defpkg events that are local
- Hidden-defpkg
- Handling defpkg events that are local
