Major Section: MISCELLANEOUS
Examples: assoc caddr + "ACL2-USER" "arith" "project/task-1/arith.lisp" :here
A logical name is either a name introduced by some event, such as
defun, defthm, or include-book, or else is the keyword :here, which
refers to the most recent such event. See events. Every
logical name is either a symbol or a string. For the syntactic
rules on names, see name. The symbols name functions, macros,
constants, axioms, theorems, labels, and theories. The strings name
packages or books. We permit the keyword symbol :here to be used as
a logical name denoting the most recently completed event.
The logical name introduced by an include-book is the full book name
string for the book (see full-book-name). Thus, under the
appropriate setting for the current book directory (see cbd)
the event (include-book "arith") may introduce the logical name
"/usr/home/smith/project/task-1/arith.lisp" .Under a different
cbd setting, it may introduce a different
logical name, perhaps
"/local/src/acl2/library/arith.lisp" .It is possible that identical
include-book events forms in a
session introduce two different logical names because of the current
book directory.
A logical name that is a string is either a package name or a book
name. If it is not a package name, we support various conventions
to interpret it as a book name. If it does not end with the string
".lisp" we extend it appropriately. Then, we search for any book
name that has the given logical name as a terminal substring.
Suppose (include-book "arith") is the only include-book so far and
that "/usr/home/smith/project/task-1/arith.lisp" is the source
file it processed. Then "arith", "arith.lisp" and
"task-1/arith.lisp" are all logical names identifying that
include-book event (unless they are package names). Now suppose a
second (include-book "arith") is executed and processes
"/local/src/acl2/library/arith.lisp". Then "arith" is no longer
a logical name, because it is ambiguous. However, "task-1/arith"
is a logical name for the first include-book and "library/arith"
is a logical name for the second. Indeed, the first can be named by
"1/arith" and the second by "y/arith".
Logical names are used primarily in the theory manipulation
functions, e.g., universal-theory and current-theory with which you
may obtain some standard theories as of some point in the historical
past. The reference points are the introductions of logical names,
i.e., the past is determined by the events it contains. One might
ask, ``Why not discuss the past with the much more flexible language
of command descriptors?'' (See command-descriptor.) The reason
is that inside of such events as encapsulate or macro commands that
expand to progns of events, command descriptors provide too coarse a
grain.
When logical names are used as referents in theory expressions used
in books, one must consider the possibility that the defining event
within the book in question becomes redundant by the definition of
the name prior to the assumption of the book.
See redundant-events.