LD-POST-EVAL-PRINT

Major Section:  MISCELLANEOUS

Ld-post-eval-print is an ld special (see ld). The accessor is (ld-post-eval-print state) and the updater is (set-ld-post-eval-print val state). Ld-post-eval-print must be either t, nil, or :command-conventions. The initial value of ld-post-eval-print is :command-conventions.

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-post-eval-print is one of them. If this global variable is t, ld prints the result. In the case of a form that produces a multiple value, ld prints the list containing all the values (which, logically speaking, is what the form returned). If ld-post-eval-print is nil, ld does not print the values. This is most useful when ld is used to load a previously processed file.

Finally, if ld-post-eval-print is :command-conventions then ld prints the result but treats ``error triples'' specially. An ``error triple'' is a result, (mv erp val state), that consists of three values, the third of which is state. Many ACL2 functions use such triples to signal errors. The convention is that if erp (the first value) is nil, then the function is returning val (the second value) as its conventional single result and possibly side-effecting state (as with some output). If erp is t, then an error has been caused, val is irrelevant and the error message has been printed in the returned state. Example ACL2 functions that follow this convention include defun and in-package. If such ``error producing'' functions are evaluated while ld-post-eval-print is set to t, then you would see them producing lists of length 3. This is disconcerting to users accustomed to Common Lisp (where these functions produce single results but sometimes cause errors or side-effect state).

When ld-post-eval-print is :command-conventions and a form produces an error triple (mv erp val state) as its value, ld prints nothing if erp is non-nil and otherwise ld prints just val. Because it is a misrepresentation to suggest that just one result was returned, ld prints the value of the global variable 'triple-print-prefix before printing val. 'triple-print-prefix is initially " ", which means that when non-erroneous error triples are being abbreviated to val, val appears one space off the left margin instead of on the margin.

In addition, when ld-post-eval-print is :command-conventions and the value component of an error triple is the keyword :invisible then ld prints nothing. This is the way certain commands (e.g., :pc) appear to return no value.

By printing nothing when an error has been signalled, ld makes it appear that the error (whose message has already appeared in state) has ``thrown'' the computation back to load without returning a value. By printing just val otherwise, we suppress the fact that state has possibly been changed.