PKG-IMPORTS

Major Section:  ACL2-BUILT-INS

Completion Axiom (completion-of-pkg-imports):

(equal (pkg-imports x)
       (if (stringp x)
           (pkg-imports x)
         nil))

Guard for (pkg-imports x):

(stringp x)

(Pkg-imports pkg) returns a duplicate-free list of all symbols imported into pkg, which should be the name of a package known to ACL2. For example, suppose "MY-PKG" was created by

(defpkg "MY-PKG" '(ACL2::ABC LISP::CAR)).

If pkg is not a string, then (pkg-imports pkg) is nil. If pkg is a string but not the name of a package known to ACL2, then the value of the form (pkg-imports pkg) is unspecified, and it evaluation will fail to yield a value. By ``the symbols imported into pkg'' we mean the symbols imported into pkg by the defpkg event that introduced pkg. There are no imports for built-in packages except for the "ACL2" package, which imports the symbols in the list value of the constant *common-lisp-symbols-from-main-lisp-package*. In particular, this is the case for the "COMMON-LISP" package. Users familiar with Common Lisp may find this surprising, since in actual Common Lisp implementations it is often the case that many symbols in that package are imported from other packages. However, ACL2 treats all symbols in the constant *common-lisp-symbols-from-main-lisp-package* as having a symbol-package-name of "COMMON-LISP", as though they were not imported. ACL2 admits a symbol imported into in the "COMMON-LISP" package only if it belongs to that list: any attempt to read any other symbol imported into the "COMMON-LISP" package, or to produce such a symbol with intern$ or intern-in-package-of-symbol, will cause an error.

The following axioms formalize properties of pkg-imports discussed above (use :pe to view them).

symbol-package-name-intern-in-package-of-symbol
intern-in-package-of-symbol-is-identity
symbol-listp-pkg-imports
no-duplicatesp-pkg-imports
completion-of-pkg-imports