Ld-error-action
Determines ld's response to an error
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!, :error, or (:exit N)
for some natural number N. The initial value of ld-error-action is
:continue, which means that the top-level ACL2 command loop (see
lp) 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!, with one exception: in the case that the value of ld
special ld-error-action is (:exit N), the default remains that
value.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co. Note that the ACL2 top-level loop (see lp) results from
an invocation of ld.
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).
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, signaling 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. If it is (:exit N), then ACL2 quits with exit
status N. Later in this topic we discuss another case in which an error
is said to have occurred: when the value component of an error triple is of
the form (:STOP-LD . x).
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). If ld-error-action is of
the form (:EXIT N), then ACL2 quits with exit status N.
Otherwise (i.e., when ld-error-action is :RETURN, :RETURN!, or
:ERROR), 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 encounters 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).
