Utilities for error-value tuples.
These are experimental utilities for now.
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.
An error-value tuple is a list consisting of
an error component
There is no strict requirements on the type of
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
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.
When there is an error,
an ACL2 function can return
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
((reterr) irr-val1 ... irr-valN)
where the symbol
The binding expands to a local macro (in the macrolet sense),
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
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.
When there is no error,
an ACL2 function can return
We provide a macro
(retok val1 ... valN)
Note that while
To propagate an error from a called ACL2 function,
a caller ACL2 function can use a binder for the call,
((mv erp val1 ... valN) (f ...)) ((when erp) (reterr erp))
(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 ...))
This binder assumes that
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
((erp val1 ... valN) (f ...) :iferr erp1)
((mv erp val1 ... valN) (f ...)) ((when erp) (reterr erp1))
(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
To catch (i.e not propagate) an error from a called ACL2 function,
a caller ACL2 function can use an
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.
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
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
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. (tsee 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.
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.
if the first component of a context-message pair is non-
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.
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
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.