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
|
<html>
<head><title>About_the_Prompt.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>About the Prompt</h2>
The string ``<code>ACL2 !></code>'' is the ACL2 prompt.
<p>
The prompt tells the user that an ACL2 <a href="COMMAND.html">command</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>is expected. In
addition, the prompt tells us a little about the current state of
the ACL2 command interpreter. We explain the prompt briefly below.
But first we talk about the command interpreter.<p>
An ACL2 command is generally a Lisp expression to be evaluated.
There are some unusual commands (such as :<a href="Q.html">q</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> for <b>quitting</B>
ACL2) which cause other behavior. But most commands are read,
evaluated, and then have their results printed. Thus, we call the
command interpreter a ``read-eval-print loop.'' The ACL2 command
interpreter is named <code><a href="LD.html">LD</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> (after Lisp's ``load'').<p>
A command like <b>(defun app (x y) ...)</B> causes ACL2 to evaluate the
<a href="DEFUN.html">defun</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> function on <b>app</B>, <b>(x y)</B> and <b>...</B>. When
that command is evaluated it prints some information to the terminal
explaining the processing of the proposed definition. It returns
the symbol <code>APP</code> as its value, which is printed by the command
interpreter. (Actually, <code>defun</code> is not a function but a <a href="DEFMACRO.html">macro</a>
which expands to a form that involves <code><a href="STATE.html">state</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>, a necessary
precondition to printing output to the terminal and to ``changing''
the set of axioms. But we do not discuss this further here.)<p>
The <code>defun</code> command is an example of a special kind of command
called an ``event.'' <a href="EVENTS.html">Events</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> are those commands that
change the ``logical world'' by adding such things as axioms or
theorems to ACL2's data base. See <a href="WORLD.html">world</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>. But not
every command is an event command.<p>
A command like <b>(app '(1 2 3) '(4 5 6 7))</B> is an example of a
non-event. It is processed the same general way: the function
<b>app</B> is applied to the indicated arguments and the result is
printed. The function <b>app</B> does not print anything and does not
change the ``world.''<p>
A third kind of command are those that display information about the
current logical world or that ``backup'' to previous versions of the
world. Such commands are called ``<a href="HISTORY.html">history</a>'' <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> commands.<p>
What does the ACL2 prompt tell us about the read-eval-print loop?
The prompt ``<code>ACL2 !></code>'' tells us that the command will be read
with <code><a href="CURRENT-PACKAGE.html">current-package</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> set to <code>"ACL2"</code>, that guard checking
(see <a href="SET-GUARD-CHECKING.html">set-guard-checking</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>) is on (``<code>!</code>''), and that we are at
the top-level (there is only one ``<code>></code>'').
For more about the prompt, see <a href="DEFAULT-PRINT-PROMPT.html">default-print-prompt</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>.<p>
You should now return to <a href="Revisiting_the_Admission_of_App.html">the Walking Tour</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>
|
