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!, 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
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).