a name created by a logical event


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.