Major Section: OTHER
Example:
(LD standard-oi ; open obj in channel, stringp file name
; to open and close, or list of forms
; Optional keyword arguments:
:standard-co ... ; open char out or file to open and close
:proofs-co ... ; open char out or file to open and close
:current-package ... ; known package name
:ld-skip-proofsp ... ; nil, 'include-book, or t
; (see ld-skip-proofsp)
:ld-redefinition-action ; nil or '(:a . :b)
:ld-prompt ... ; nil, t, or some prompt printer fn
:ld-keyword-aliases ... ; an alist pairing keywords to parse info
:ld-pre-eval-filter ... ; :all, :query, or some new name
:ld-pre-eval-print ... ; nil, t, or :never
:ld-post-eval-print ... ; nil, t, or :command-conventions
:ld-evisc-tuple ... ; nil or '(alist nil nil level length)
:ld-error-triples ... ; nil or t
:ld-error-action ... ; :return (default), :continue or :error
:ld-query-control-alist ; alist supplying default responses
:ld-verbose ...) ; nil or t
Ld is the top-level ACL2 read-eval-print loop. (When you call lp, a
little initialization is done in raw Common Lisp and then ld is
called.) ld is also a general-purpose ACL2 file loader and a
command interpreter. Ld is actually a macro that expands to a
function call involving state. Ld returns an ``error/value/state''
triple as explained below.
The arguments to ld all happen to be global variables in state. For
example, 'current-package and 'ld-verbose are global variables,
which may be accessed via (@ current-package) and (@ ld-verbose).
When ld is called, it ``binds'' these variables. By ``binds'' we
actually mean the variables are globally set but restored to their
old values on exit. Because ld provides the illusion of state
global variables being bound, they are called ``ld specials'' (after
the Lisp convention of calling a variable ``special'' if it is
referenced freely after having been bound).
Note that all arguments but the first are passed via keyword. Any
variable not explicitly given a value in a call retains its pre-call
value, with the exception of :ld-error-action, which defaults to
:return if not explicitly specified.
Just as an example to drive the point home: If current-package is
"ACL2" and you typed
(ld *standard-oi* :current-package "MY-PKG")you would find yourself in (an inner) read-eval-print loop in which the current-package was
"MY-PKG". You could operate
there as long as you wished, changing the current package at will.
But when you typed :q you would return to the outer
read-eval-print loop where the current package would still be
"ACL2".
Roughly speaking, ld repeatedly reads a form from standard-oi,
evaluates it, and prints its result to standard-co. It does this
until the form evaluates to an error triple whose value component is
:q or until the input channel or list is emptied. However, ld has
many bells and whistles controlled by the ld specials. Each such
special is documented individually. For example, see the
documentation for standard-oi, current-package,
ld-pre-eval-print, etc.
A more precise description of ld is as follows. In the description
below we use the ld specials as variables, e.g., we say ``a form is
read from standard-oi.'' By this usage we refer to the current
value of the named state global variable, e.g., we mean ``a form is
read from the current value of 'standard-oi.'' This technicality has
an important implication: If while interacting with ld you change
the value of one of the ld specials, e.g., 'standard-oi, you will
change the behavior of ld, e.g., subsequent input will be taken from
the new value.
Three ld specials are treated as channels: standard-oi is treated as
an object input channel and is the source of forms evaluated by ld;
standard-co and proofs-co are treated as character output channels
and various flavors of output are printed to them. However, the
supplied values of these specials need not actually be channels;
several special cases are recognized. If the supplied value of one
of these is in fact an open channel of the appropriate type, that
channel is used and is not closed by ld. If the supplied value of
one of these specials is a string, the string is treated as a file
name in (essentially) Unix syntax (see pathname) and a channel
of the appropriate type is opened to/from that file. Any channel
opened by ld during the binding of the ld specials is automatically
closed by ld upon termination. If standard-co and proofs-co are
equal strings, only one channel to that file is opened and is used
for both.
Several other alternatives are allowed for standard-oi. If
standard-oi is a true list then it is taken as the list of forms to
be processed. If standard-oi is a list ending in an open channel,
then ld processes the forms in the list and then reads and processes
the forms from the channel. Analogously, if standard-oi is a list
ending a string, an object channel from the named file is opened and
ld processes the forms in the list followed by the forms in the
file. That channel is closed upon termination of ld.
The remaining ld specials are handled more simply and generally have
to be bound to one of a finite number of tokens described in the
:doc entries for each ld special. Should any ld special be supplied
an inappropriate value, an error message is printed.
Next, if ld-verbose is t, ld prints the message ``ACL2 loading
name'' where name names the file or channel from which forms are
being read. At the conclusion of ld, it will print ``Finished
loading name'' if ld-verbose is t.
Finally, ld repeatedly executes the ACL2 read-eval-print step, which
may be described as follows. A prompt is printed to standard-co if
ld-prompt is non-nil. The format of the prompt is determined by
ld-prompt. If it is t, the default ACL2 prompt is used. If it is
any other non-nil value then it is treated as an ACL2 function that
will print the desired prompt. See ld-prompt. In the
exceptional case where ld's input is coming from the terminal
(*standard-oi*) but its output is going to a different sink (i.e.,
standard-co is not *standard-co*), we also print the prompt to the
terminal.
Ld then reads a form from standard-oi. If the object read is a
keyword, ld constructs a ``keyword command form'' by possibly
reading several more objects. See keyword-commands. This
construction process is sensitive to the value of
ld-keyword-aliases. See ld-keyword-aliases. Otherwise, the
object read is treated as the command form.
Ld next decides whether to evaluate or skip this form, depending on
ld-pre-eval-filter. Initially, the filter must be either :all,
:query, or a new name. If it is :all, it means all forms are
evaluated. If it is :query, it means each form that is read is
displayed and the user is queried. Otherwise, the filter is a name
and each form that is read is evaluated as long as the name remains
new, but if the name is ever introduced then no more forms are read
and ld terminates. See ld-pre-eval-filter.
If the form is to be evaluated, first prints the form to
standard-co, if ld-pre-eval-print is t. With this feature, ld can
process an input file or form list and construct a script of the
session that appears as though each form was typed in.
See ld-pre-eval-print.
Ld then evaluates the form, with state bound to the current state.
The result is some list of multiple values. If a state is among the
values, then ld uses that state as the subsequent current state.
Depending on ld-error-triples, ld may interpret the result as an
``error.'' See ld-error-triples. We first discuss ld's
behavior if no error signal is detected (either because none was
sent or because ld is ignoring them as per ld-error-triples).
In the case of a non-erroneous result, ld does two things: First, if
the logical world in the now current state is different than the
world before execution of the form, ld adds to the world a ``command
landmark'' containing the form evaluated.
See command-descriptor. Second, ld prints the result to
standard-co, according to ld-post-eval-print. If ld-post-eval-print
is nil, no result is printed. If it is t, all of the results are
printed as a list of multiple values. Otherwise, it is
:command-conventions and only the non-erroneous ``value'' component
of the result is printed. See ld-post-eval-print.
Whenever ld prints anything (whether the input form, a query, or
some results) it ``eviscerates'' it if ld-evisc-tuple is non-nil.
Essentially, evisceration is a generalization of Common Lisp's use
of *print-level* and *print-length* to hide large substructures.
See ld-evisc-tuple.
We now return to the case of a form whose evaluation signals an
error. In this case, ld first restores the ACL2 logical world to
what it was just before the erroneous form was evaluated. Thus, a
form that partially changes the world (i.e., begins to store
properties) and then signals an error, has no effect on the world.
You may see this happen on commands that execute several events
(e.g., an encapsulate or a progn of several defuns): even though the
output makes it appear that the initial events were executed, if an
error is signalled by a later event the entire block of events is
discarded.
After rolling back, ld takes an action determined by
ld-error-action. If the action is :continue, ld merely iterates the
read-eval-print step. Note that nothing suggestive of the value of
the ``erroneous'' form is printed. If the action is :return, ld
terminates normally. If the action is :error, ld terminates
signalling an error to its caller. If its caller is in fact another
instance of ld and that instance is watching out for error signals,
the entire world created by the erroneous inner ld will be discarded
by the outer ld.
Ld returns an error triple, (mv erp val state). Erp is t or nil
indicating whether an error is being signalled. If no error is
signalled, val is the ``reason'' ld terminated and is one of :exit
(meaning :q was read), :eof (meaning the input source was
exhausted), :error (meaning an error occurred but has been
supressed) or :filter (meaning the ld-pre-eval-filter terminated
ld).
