ld's response to an error
Major Section: MISCELLANEOUS
Ld-error-action is an ld special (see ld). The accessor is
(ld-error-action state) and the updater is
(set-ld-error-action val state). Ld-error-action must be
:continue, :return, :return!, or :error. The initial value
of ld-error-action is :continue, which means that the top-level ACL2
command loop will not exit when an error is caused by user-typein.
But the default value for ld-error-action on calls of ld is
:return!.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-error-action is one of them. Suppose that ld-error-triples is
t and a form evaluates to an error triple (mv erp val state);
see error-triples. If the ``error component'', erp, is non-nil,
then an error is said to have occurred. If an error occurs, ld's
action depends on ld-error-action. If it is :continue, ld just
continues processing the forms in standard-oi. If it is :return or
:return!, ld stops and returns as though it had emptied the
channel. If it is :error, ld stops and returns, signalling an
error to its caller by returning an error triple with non-nil error
component, and reverting the logical world to its value just before that
call of ld.
To see this effect of :ERROR for ld-error-action, consider the
following example.
(ld '((defun f (x) x) (defun bad (x)) (defun g (x) x)))When the
defun of bad fails (because its body is missing),
evaluation of the ld call stops; thus, the defun of g is not
evaluated. The definition of f will be removed from the logical
world before the call of ld returns.However, by default each user call of ld is made with a
ld-error-action of :RETURN! (not :ERROR). In the common case
that all nested calls of ld inside the ACL2 loop are made this way, an
error will not roll back the logical world. However, it will still halt
evaluation of forms for the current call of ld and any parent calls of
ld (other than the call made on behalf of lp that entered the ACL2
loop in the first place), as though there were no more forms to evaluate.
We have already discussed the behavior of ld when an error occurs. But
there is another case when ld can stop processing more forms: when
ld-error-action is not :CONTINUE, ld-error-triples is t,
and evaluation of a form returns an error triple (mv nil val state),
where nil is the error component and whose ``value component'', val
is a cons pair whose car is the symbol :STOP-LD. Let val
be the pair (:STOP-LD . x). Then the call of ld returns the error
triple (mv nil (:STOP-LD n . x) state), where n is the value of
state global variable 'ld-level at the time of termination. The
following example illustrates how this works.
(ld '((defun f1 (x) x)
(ld '((defun f2 (x) x)
(mv nil '(:STOP-LD my-error more-info) state)
(defun g2 (x) x)))
(defun g1 (x) x)))
The outer call of ld returns the value
(:STOP-LD 2 3 MY-ERROR MORE-INFO)and leaves us in a world the includes definitions for
f1 and f2, but
no definition for g1 or g2 since neither of their two defun forms
was evaluated. The value of state global 'ld-level is incremented
from 1 to 2 when the outer ld is entered and then again to 3 when the
inner ld is entered. When the inner ld escounters the error triple
(mv nil (:STOP-LD my-error more-info) state), it sees :STOP-LD in the
car of the value component and pushes the current value of 'ld-level,
3, onto the cdr of that value, to return the value triple
(mv nil (:STOP-LD my-error 3 more-info) state). The outer of ld then
sees this value and returns
(mv nil (:STOP-LD my-error 2 3 more-info) state), since its current value
of 'ld-level is 2 after the inner ld exits.That concludes our discussion of how these special :STOP-LD values are
handled; but how are they created? While they can be created directly by
evaluation results as suggested in the example above, that is not the
standard way. Rather, ld returns an error triple
(mv nil (:STOP-LD n) state), where n is the value of variable
ld-level at the time of termination, when the following conditions hold:
an error occurs, ld-error-action is RETURN! (which is the default),
and ld-error-triples is t (the default). The following example,
which is a bit similar to the preceding one, illustrates both creation and
handling of the special :STOP-LD values.
(ld '((defun f1 (x) x)
(ld '((defun f2 (x) x)
(ld '((defun f3 (x) x)
(defun bad (x)) ; ERROR -- missing the body
(defun g3 (x) x)))
(defun g2 (x) x)))
(defun g1 (x) x)))
The result is that f1, f2, and f3 are defined, but none of
g1, g2, or g3 is defined. Let's see why. The innermost call
of ld has a default :ld-error-action of :RETURN! (as do the
other calls). So when the definition of bad fails, then the innermost
ld returns (mv nil (:STOP-LD 4) state). The middle ld sees this
value, and since its :ld-error-action is not :CONTINUE (because it
has the default value of :RETURN!), it returns before considering the
definition of g2, with value (mv nil (:STOP-LD 3 4) state). The
topmost call of ld similarly sees the :STOP-LD; stops evaluation
of forms, without defining g1; and returns
(mv nil (:STOP-LD 2 3 4) state).
