		Search-engine friendly clone of the ACL2 documentation.

Std/util

Error-value-tuples

Utilities for error-value tuples.

These are experimental utilities for now.

Motivation

Sometimes execution runs into exceptional conditions that warrant returning error indications, which are propagated through the callers up the stack, and may or may not be caught, and recovered from, at some point; if they are not caught, execution terminates, with some kind of error message.

Some languages like Java provide exception mechanisms for this. ACL2 does not have a full exception mechanism, but it has some built-in facilities, as well as the ability to build facilities, to approximate that.

Error-Value Tuples

An error-value tuple is a list consisting of an error component erp followed by zero or more value components val1, ..., valN, where N ≥ 0. An ACL2 function can return an error-value tuple to indicate possible errors: if no error occurs, erp is nil and val1, ..., valN are the normal results of the function; if an error occurs, erp contains non-nil information about the error and val1, ..., valN contain irrelevant values.

There is no strict requirements on the type of erp, but it should be, or include, an optional message that describes the error in human-readable terms; for instance, an error could be a cons pair whose car is a machine-oriented error code or structure, and whose cdr is a human-readable message. When writing code in a statically strongly typed style, particularly using define with argument and result types (the latter in :returns), it may be better to leave erp untyped for future extensibility, while val1, ..., valN should have types that make sense when no error occurs. If a type for erp is used, e.g. maybe-msgp, it should be the same for all the functions that call each other, so that the same type of errors can be propagated (see below).

We provide utilities, described below, to facilitate the use of error-value tuples. More utilities may be added in the future, particularly for richer forms of erp, which for now is assumed to be an optional message.

This is not a new idea, but just a variation of existing ideas. A comparison with these related approaches is given below, after describing the utilities for error-value tuples.

Utilities for Error-Value Tuples

Returning Errors

When there is an error, an ACL2 function can return (mv erp irr-val1 ... irr-valN) if N > 0, or just erp if N is 0, where erp is a non-nil error indication, such as a message of the form (msg ...), and where irr-val1, ..., irr-valN are terms that evaluate to irrelevant values of appropriate types. In a statically strongly typed style, the values should have the same types that they have when no error occurs, so that the :returns theorems apply uniformly to the error and non-error cases, without the need of conditions on the erp results.

To return errors more clearly and concisely, we provide a b* binder patbind-reterr that defines the irrelevant values once, and that makes it possible for the rest of the code in the function to mention just erp when returning an error. The binder is used, generally at the beginning of a function, as

((reterr) irr-val1 ... irr-valN)

where the symbol reterr is in the ACL2 package, but can be of course imported in the application package of interest, and where irr-val1, ..., irr-valN are irrelevant values of appropriate types, to be returned along with a non-nil erp. If N is 0, the binding is just ((reterr)), but must still be provided.

The binding expands to a local macro (in the macrolet sense), also named reterr in the ACL2 package, that takes one argument erp and extends it to an error-value tuple with the irrelevant values. This way, code in the function can return an error as

(reterr erp)

where erp is the desired error, e.g. (msg ...). This not only makes the call more clear and compact, by hiding the irrelevant values, but also avoids repeating the irrelevant values as many times as there are points in the code that return errors. It makes it easier to change the code if the numbers or types of the values change.

The practice of causing hard errors when an unrecoverable internal condition arises (e.g. reaching a state that should never be reached) can be integrated with error-value tuples by doing something like

(reterr (hard-error ...))

or perhaps using the more convenient raise when using define. Technically hard-error returns nil, which would mean no error in an error-value tuple, but such (non-)error is never returned, because hard-error stops execution. The advantage of using hard-error (or similar) inside reterr is that logically the ACL2 function still returns results of the appropriate number and type, without the need to follow hard-error by an explicit dummy term to return irrelevant results.

The terms denoting the irrelevant values do not need to be ground, because this binder expands into a macrolet, which can introduce variables in the expansion. This is useful to return stobj results, including state, as value components of error-value tuples.

Returning Non-Errors

When there is no error, an ACL2 function can return (mv nil val1 ... valN) if N > 0, or just nil if N is 0, where val1, ..., valN are appropriate relevant values.

We provide a macro retok, in the ACL2 package (from where it can be imported in an application package), to make this slightly more clear and compact. The use of this macro hides the nil erp, and just takes the values, as

(retok val1 ... valN)

If N is 0, it is writte as (retok), which in a way may be more clear than nil in saying that things are okay, i.e. no error occurred. It is also symmetric with reterr. However, admittedly this does not provide huge advantages over just (mv nil val1 .. valN) or nil.

Note that while reterr is local to a function, and must be introduced via the homonymous binder, retok is a global macro, which takes a variable number of arguments.

Propagating Errors

To propagate an error from a called ACL2 function, a caller ACL2 function can use a binder for the call, check the erp result, and return an error with the same erp and with its own irrelevant values, as

((mv erp val1 ... valN) (f ...))
((when erp) (reterr erp))

or, if N is 0, as

(erp (f ...))
((when erp) (reterr erp))

We provide a b* binder patbind-erp that expands to the code shown just above. This is used as

((erp val1 ... valN) (f ...))

where erp is in the ACL2 package (but can imported into the package of interest). If N is 0, the binding is ((erp) (f ...)). The val1, ..., valN may be b* patterns that can be used as components of the patbind-mv binder.

This binder assumes that reterr is a local macro introduced by a preceding reterr binder (described above).

This binder has an option to change the error to be returned. Only the error component can be changed; the irrelevant values are always the same, from reterr. The option is used as

((erp val1 ... valN) (f ...) :iferr erp1)

where erp1 is a term that evaluates to the error to be returned. This term may reference the variable erp as containing the error returned by the called function, so that it can build a new error component that depends on the old one. When :iferr is present, the binding expands to

((mv erp val1 ... valN) (f ...))
((when erp) (reterr erp1))

or, if N is 0, to

(erp (f ...))
((when erp) (reterr erp1))

We expect that this option may be used less often than not.

Because on the restriction on stobj results with reterr, this binder cannot be currently used when the values of error-value triples include stobjs. In this case, errors must be checked and propagated explicitly.

Catching Errors

To catch (i.e not propagate) an error from a called ACL2 function, a caller ACL2 function can use an mv binder for the call, check the erp result, and continue its computation if an error occurs, presumably to recover from the error somehow. If the called function does not return an error, presumably the caller function will continue computation in some other way.

At this point we do not provide any general utilities for the case in which the error is caught. The reason is that the actions to take when catching the error are application-specific. Furthermore, we expect that this kind of errors will be propagated more often than caught. Error-value tuples are intended for when execution runs into exceptional conditions, similarly to the situations in which languages with exceptions would throw exceptions.

Related Ideas

Hard Errors

A hard error is a bit like an exception. When a hard error occurs, it print a message to ACL2's error output, and it stops execution. A hard error is automatically propagated through the callers up the stack. However, a hard error cannot be caught: it always stops execution.

Since logically a hard error returns nil, when a function returns a hard error, unless it has one result whose type includes nil, one must add code to return an appropriate number and type of results, in order to maintain a statically strongly typed style. This is equivalent in effort to writing the reterr binder, and the hard error call, which contains just a message, is equivalent in effort to writing a reterr call with the message. Hard error propagation is fully automatic, but writing the erp binder is equivalent in effort to writing an mv or a single-variable binder for a call of a function that may return a hard error (such a function needs not return an error result). Thus, all in all, using error-value tuples, with the utilities provided here, takes about the same amount of code as using hard errors, with the advantage that errors can be potentially caught, which is useful for using tools programmatically besides interactively. The only extra effort required for error-value tuples is that, if the error is not caught, there must be some code, near the top level, to actually print the message on the screen, perhaps using a hard or soft error.

Soft Errors

A soft error print a message to ACL2's error output, but does not stop execution. It causes the current function to return an error triple, which the function's caller can treat just like any other result. The caller can catch it and continue execution, or it can propagate it up to the caller. The propagation is not automatic, but it is facilitated by macros like the built-in er-let* or the b* binder er, which is similar to the erp binder for error-value tuples.

Soft errors are used when programming with state. They need state to be available (i.e. to be passed to the function that throws the soft error). They also require the function that throws the soft error to return state, in the form of an error triple. Taking, and even more returning state, is sometimes inconvenient, namely when there is otherwise no reason to take or return it.

If a function that could naturally return multiple results needs to throw soft errors, the multiple results must be aggregated into the value component of the error triple, because mv cannot be nested. This aggregation is slightly inconvenient, especially when writing code in a statically strongly typed style, in which every argument and result has a clear type. A possible aggregation is a tuple (i.e. list), which means that the multiple results in the value must be accessed as elements of the list, which is not as direct (see std::tuple for a macro to facilitate the declaration of multiple value reuslts in define return specifiers). Another possible aggregation is a user-defined product type (e.g. std::defaggregate or fty::defprod), but that requires such a type to be explicitly defined. Neither approach is as convenient as just returning multiple results, but that is not possible if the function already returns an error triple due to soft errors.

For the above reason, it seems that, unless error triples are needed for some other reason, error-value tuples may be more flexible.

Context-Message Pairs

A context-message pair is a bit like an error triple without state. Another difference with soft errors is that, instead of printing an error message, it returns a message, which a (direct or indirect) caller can print.

A context-message pair can be caught or propagated. The propagation is not automatic, but it is facilitated by macros like the built-in er-let*-cmp. Since there is no automatic printing, if the error is not caught, the message should be explicitly printed, which makes context-message pairs slightly less convenient than hard and soft errors in this respect. However, an advantage is that state does not need not be taken and returned.

Note that, if the first component of a context-message pair is non-nil, the error message is the second component of the context-message pair. This nicely solves the issue of which value to return when there is an error; in a soft error, some value must be picked for the second component, even though it is often irrelevant. However, the fact that the second component of a context-message pair may be either a message or an application-specific value goes a bit against a statically strongly typed style of coding, in which ideally every result of a function has a clear type. If the value may be a message, its type is the union of the ``real'' type and the type of messages, which is a little more complicated than just using the ``real''type, and makes it necessary to create a type for the union.

Context-message pairs are thus quite similar to error-value tuples, and are sometimes used as context-message tuples (i.e. with more than one value). The difference is that, in error-message pairs, we put the message in the error, so that values have more uniform types. The error-value tuple utilities are also tailored to this.

Result Types

A different approach to errors is that of result types, in which a function returns either a good result or an error result. See the discussion in the documentation of result types for a comparison with the approach of returning a possibly nil error and some values, as done with error-value tuples, soft errors, and context-message pairs. In short, the advantage of result types is that they avoid the issue of irrelevant values when the error is non-nil, and prevent any accidental use of such irrelevant values. The disadvantage is that functions that return multiple results must return one aggregate result (whose type can be defined via std::defaggregate or fty::defprod, for example), and also that the code may be less efficient due to the construction and deconstruction of aggregations of multiple results.

Result types may be more appropriate for development in which ACL2 is used as a logical language, e.g. in a formalization, where clarity has paramount importance, and efficiency, or the need to define additional aggregate types, is a secondary concern. Error-value tuples, like soft errors and context-message pairs, may be more appropriate for programs, where ACL2 is used as a programming language, e.g. in a tool implementation, where expediency and efficiency may be more important than extreme conceptual clarity.

Subtopics

Retok: Macro to return an error-value tuple with no error.
Patbind-reterr: Binder to introduce a local function that returns an error-value tuple with certain irrelevant values.
Patbind-erp: Binder to propagate errors from error-value tuples.