File: LOGICAL-NAME.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (85 lines) | stat: -rw-r--r-- 4,672 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
<html>
<head><title>LOGICAL-NAME.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>LOGICAL-NAME</h2>a name created by a logical event
<pre>Major Section:  <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>


<pre>
Examples:
assoc
caddr
+
"ACL2-USER"
"arith"
"project/task-1/arith.lisp"
:here
</pre>

<p>
A logical name is either a name introduced by some event, such as
<code><a href="DEFUN.html">defun</a></code>, <code><a href="DEFTHM.html">defthm</a></code>, or <code><a href="INCLUDE-BOOK.html">include-book</a></code>, or else is the keyword <code>:here</code>, which
refers to the most recent such event.  See <a href="EVENTS.html">events</a>.  Every
logical name is either a symbol or a string.  For the syntactic
rules on names, see <a href="NAME.html">name</a>.  The symbols name functions, macros,
constants, axioms, theorems, labels, and <a href="THEORIES.html">theories</a>.  The strings name
packages or <a href="BOOKS.html">books</a>.  We permit the keyword symbol <code>:here</code> to be used as
a logical name denoting the most recently completed event.<p>

The logical name introduced by an <a href="INCLUDE-BOOK.html">include-book</a> is the full book name
string for the book (see <a href="FULL-BOOK-NAME.html">full-book-name</a>).  Thus, under the
appropriate setting for the current book directory (see <a href="CBD.html">cbd</a>)
the event <code>(include-book "arith")</code> may introduce the logical name

<pre>
"/usr/home/smith/project/task-1/arith.lisp" .
</pre>

Under a different <code><a href="CBD.html">cbd</a></code> setting, it may introduce a different
logical name, perhaps

<pre>
"/local/src/acl2/library/arith.lisp" .
</pre>

It is possible that identical <code><a href="INCLUDE-BOOK.html">include-book</a></code> events forms in a
session introduce two different logical names because of the current
book directory.<p>

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
<code>".lisp"</code> we extend it appropriately.  Then, we search for any book
name that has the given logical name as a terminal substring.
Suppose <code>(include-book "arith")</code> is the only <a href="INCLUDE-BOOK.html">include-book</a> so far and
that <code>"/usr/home/smith/project/task-1/arith.lisp"</code> is the source
file it processed.  Then <code>"arith"</code>, <code>"arith.lisp"</code> and
<code>"task-1/arith.lisp"</code> are all logical names identifying that
<code><a href="INCLUDE-BOOK.html">include-book</a></code> event (unless they are package names).  Now suppose a
second <code>(include-book "arith")</code> is executed and processes
<code>"/local/src/acl2/library/arith.lisp"</code>.  Then <code>"arith"</code> is no longer
a logical name, because it is ambiguous.  However, <code>"task-1/arith"</code>
is a logical name for the first <code><a href="INCLUDE-BOOK.html">include-book</a></code> and <code>"library/arith"</code>
is a logical name for the second.  Indeed, the first can be named by
<code>"1/arith"</code> and the second by <code>"y/arith"</code>.<p>

Logical names are used primarily in the theory manipulation
functions, e.g., <code><a href="UNIVERSAL-THEORY.html">universal-theory</a></code> and <code><a href="CURRENT-THEORY.html">current-theory</a></code> with which you
may obtain some standard <a href="THEORIES.html">theories</a> 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 <a href="EVENTS.html">events</a> it contains.  One might
ask, ``Why not discuss the past with the much more flexible language
of <a href="COMMAND.html">command</a> descriptors?'' (See <a href="COMMAND-DESCRIPTOR.html">command-descriptor</a>.)  The reason
is that inside of such <a href="EVENTS.html">events</a> as <code><a href="ENCAPSULATE.html">encapsulate</a></code> or macro <a href="COMMAND.html">command</a>s that
expand to <code><a href="PROGN.html">progn</a></code>s of <a href="EVENTS.html">events</a>, <a href="COMMAND.html">command</a> descriptors provide too coarse a
grain.<p>

When logical names are used as referents in theory expressions used
in <a href="BOOKS.html">books</a>, 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 <a href="REDUNDANT-EVENTS.html">redundant-events</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>