Current-package
The package used for reading and printing
Current-package is an ld special (see ld). The
accessor is (current-package state) and the updater is
(set-current-package val state), or more conventionally, (in-package
val). The value of current-package is actually the string that names
the package. (Common Lisp's ``package'' objects do not exist in ACL2.) The
current package must be known to ACL2, i.e., it must be one of the initial
packages or a package defined with defpkg by the user.
When printing symbols, the package prefix is displayed if it is not the
current-package and may be optionally displayed otherwise. Thus, if
current-package is "ACL2" then the symbol 'ACL2::SYMB may be
printed as SYMB or ACL2::SYMB, while 'MY-PKG::SYMB must be
printed as MY-PKG::SYMB. But if current-package is "MY-PKG"
then the former symbol must be printed as ACL2::SYMB while the latter may
be printed as SYMB.
In Common Lisp, current-package also affects how objects are read from
character streams. Roughly speaking, read and print are inverses if the
current-package is fixed, so reading from a stream produced by printing
an object must produce an equal object.
In ACL2, the situation is more complicated because we never read objects
from character streams, we only read them from object ``streams'' (channels).
Logically speaking, the objects in such a channel are fixed regardless of the
setting of current-package. However, our host file systems do not
support the idea of Lisp object files and instead only support character
files. So when you open an object input channel to a given (character file)
we must somehow convert it to a list of ACL2 objects. This is done by a
deus ex machina (``a person or thing that appears or is introduced
suddenly and unexpectedly and provides a contrived solution to an apparently
insoluble difficulty,'' Webster's Ninth New Collegiate Dictionary). Roughly
speaking, the deus ex machina determines what sequence of calls to
read-object will occur in the future and what the current-package
will be during each of those calls, and then produces a channel containing the
sequence of objects produced by an analogous sequence of Common Lisp reads
with *current-package* bound appropriately for each.
A simple rule suffices to make sane file io possible: before you
read an object from an object channel to a file created by printing to a
character channel, make sure the current-package at read-time is the same
as it was at print-time.
