About the Prompt
About the Prompt
The string ``ACL2 !>'' is the ACL2 prompt.
The prompt tells the user that an ACL2 command 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.
An ACL2 command is generally a Lisp expression to be evaluated. There are
some unusual commands (such as :q for
quitting 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
ld (after Lisp's ``load'').
When a command is read, all the symbols in it are converted to uppercase.
Thus, typing (defun app ...) is the same as typing (DEFUN APP ...)
or (defun App ...). There are ways to force lowercase case characters
into symbols but we won't discuss them here. A consequence of Common Lisp's
default uppercasing is that you'll see a general lack of concern over the case
used when symbols are displayed in this documentation.
In addition, symbols ``belong'' to ``packages'' which give the user a way
to control namespaces. The prompt tells us which package is the default one,
namely "ACL2". That means when we call car, for example, we are
invoking the standard definition of that symbol. If the packager were
"JONES" then car would refer to the definition of that symbol in
that package (which may or may not be different depending on what symbols were
imported into that package.
A command like (defun app (x y) ...) causes ACL2 to evaluate the
defun function on app, (x y) and
.... When that command is evaluated it prints some information to the
terminal explaining the processing of the proposed definition. It returns the
symbol APP as its value, which is printed by the command interpreter.
(Actually, defun is not a function but a macro which expands to a form that involves state
, a necessary precondition to printing output to the
terminal and to ``changing'' the set of axioms. But we do not discuss this
further here.)
The defun command is an example of a special kind of command called an
``event.'' Events are those commands that change the ``logical
world'' by adding such things as axioms or theorems to ACL2's database. See
world . But not every command is an event command.
A command like (app '(1 2 3) '(4 5 6 7)) is an example of a
non-event. It is processed the same general way: the function app is
applied to the indicated arguments and the result is printed. The function
app does not print anything and does not change the ``world.''
A third kind of command is one that display information about the current
logical world or that ``roll back'' to previous versions of the world. Such
commands are called ``history''
commands.
What does the ACL2 prompt tell us about the read-eval-print loop? The
prompt ``ACL2 !>'' tells us that the command will be read with current-package set to "ACL2", that guard checking (see
set-guard-checking ) is on (``!''), and that we are at the
top-level (there is only one ``>''). For more about the prompt, see
default-print-prompt .
You should now return to the Walking Tour.
