		Search-engine friendly clone of the ACL2 documentation.

Defresult

Introduce a fixtype for good results and error results.

Introduction

This is an experimental tool for now.

It is common for a function to return an error result in certain cases. Otherwise, the function returns a good (i.e. non-error) result.

In ACL2, an approach is to have the function return multiple results: an error result (which is nil if there is no error), and a good result (which is irrelevant if the error result is non-nil); for instance, this is the idiom of error triples. Another approach is to have the function return either an error result or a good result, which requires error and good results to be disjoint.

The two approaches have relative advantages and disadvantages. An advantage of the first approach is that disjointness of error and good results is not required and that each result has always the same type. However, a disadvantage is that even though the good result is irrelevant when the error result is non-nil, some good result must be nonetheless returned, which might be accidentally used, as nothing could prevent that. Returning something like nil as good result means that, unless nil happens to be a good result, it is not the case that the good result always has the type of good results, leading to conditional return type theorems instead of unconditional ones; the latter are more efficient, and conceptually cleaner, but there is nothing technically wrong with conditional ones either. The second approach avoids this issue, because if there is an error result then there is no good result at all; the downside is that the result may have two different types. Since disjunctions are awkward in rewrite rules, it is beneficial to always introduce a type for the union of good and error results, and use that as the return type of the function. But then one needs rules to handle the inherent disjunction.

When functions naturally return multiple results (via mv), the first approach adds an error result, while the second approach could be applied to one of the results (e.g. the ``main'' one, if there is such a thing). Better yet from a conceptual point of view, the function can be made to return a single result, instead of multiple ones, that is either an error or a tuple of the good results. This is less efficient than multiple results (efficiency is indeed the purpose of multiple results with mv), but it may be more appropriate for a higher-level specification function, where issues of efficiency should be secondary, and where it may be more important that, in case of error, no dummy results are returned, so they cannot be accidentally used. The term `tuple' above is used in a broad sense: it does not have to be a list of values; it could be a value of a defprod type, for example. The claim above that issues of efficiency should be secondary in specification functions fits into a vision in which tools like APT are used to turn possibly inefficient or even non-executable functions into efficient ones. When instead, for expediency or practicality, a compromise is sought in which the same function is used for specification and execution (which sometimes also involves uses of mbe), then other considerations may apply, and the first approach above may be preferable to the second one. Nonetheless, there are applications where the second approach fits well.

When calling functions that may return error results (whether the first or second approach above is used), it is common to check whether the returned result is an error one, and in that case also return an error, otherwise continuing the computation if the returned result is a good one. When using the error triple idiom, ACL2 provides er-let* to handle this pattern, which propagates the error triples unchanged; b* provides the er binder, which expands into something like er-let*.

The defresult macro provides support for the second approach above. Given a fixtype of good results, it introduces a fixtype of good and error results, where the fixtype of error results is reserr (from the first three letters of each of the two words of `result error'), which is provided along with defresult. This macro also generates rules to reason about the disjunction of good and error results. To return an error (when an error condition arises), the constructor reserr of the reserr fixtype can be used: it takes an argument of any type. Along with defresult, a b* binder patbind-ok is provided to support the check-and-propagate-error pattern described above.

When using define, which provides automatic binding of __function__ to the current function symbol, it may be useful to automatically incorporate this information into the error result. To this end, a macro reserrf is provided that automatically adds the function information to the information passed explicitly as input to the macro. A macro reserrf-push is also provided to add function and other information to an error of the form returned by reserrf or reserrf-push, resulting in a stack of error information corresponding to the call stack. The patbind-okf binder automates the check-and-propagation of errors that include function information.

The reserrf and reserrf-push macros, and the patbind-okf binder, may be very useful for debugging, or in general to provide informative error information. They may be less useful for higher-level specifications, in which errors do not carry much information (as producing and consuming that information may detract from the clarity and conciseness of the specification): for higher-level specifications, the simpler function reserr and binder patbind-ok may be more appropriate. Note that the f in the names of the first set of items conveys that they are a version of the simpler ones that take the function name bound to __function__ into account; note also that there is no reserr-push, since it is not needed for the simpler errors and checks and propagation. We also remark that the simpler ones can be used in code not written using define.

The fact that the same error result type, namely reserr, is used in all the result types introduced by defresult is crucial to supporting the kind of error propagation explained above: the same type of error result may be returned by any function that returns a type defined via defresult, even if the good result types are different. It is also crucial that the result type is defined as a flat, and not tagged, union of good and error results: otherwise, error results would have to be unwrapped and wrapped depending on the result types of the callee and caller, using different unwrapping and wrapping function for each type.

The fixtype of good and error results introduced by defresult is similar to an instance of Rust's polymorphic type Result, from which the `result' part of defresult is taken. However, while the Rust type is parameterized over both the good and error result types, in defresult errors always have the same type. Nonetheless, reserr is defined to allow any ACL2 value to be contained in an error result, so the lack of parameterization over the type of errors does not limit expressivity.

General Form

(defresult type
           :ok ...
           :pred ...
           :fix ...
           :equiv ...
           :parents ...
           :short ...
           :long ...
           :prepwork ...
  )

Inputs

:type

A symbol that specifies the name of the new fixtype.

:ok

A symbol that specifies the fixtype of the good results. Let ok be the recognizer of this fixtype.

:pred

A symbol that specifies the name of the fixtype's recognizer. If this is nil (the default), the name of the recognizer is type followed by -p.

:fix

A symbol that specifies the name of the fixtype's fixer. If this is nil (the default), the name of the fixer is type followed by -fix.

:equiv

A symbol that specifies the name of the fixtype's equivalence. If this is nil (the default), the name of the equivalence is type followed by -equiv.

:parents
:short
:long

These, if present, are added to the XDOC topic generated for the fixtype.

:prepwork

A list of preparatory event forms. See the `Generated Events' section.

Applicability Conditions

In order for defresult to apply, in addition to the requirements on the inputs stated in the `Inputs' section, the following applicability conditions must be proved. The proofs are attempted when defresult is called, using the hints optionally supplied as the :hints input described in the `Inputs' section.

The fixtype specified by :ok must be disjoint from reserr. Currently this is not quite explicated as an applicability condition as in other event macros, but the macro will fail if the disjointness cannot be proved. The :prepwork option may be used to add events to help the proofs (e.g. lemmas and rule enablements); these events should be normally made local.

Generated Events

type

The fixtype of good and error results.

pred

The recognizer for the fixtype type.

fix

The fixer for the fixtype type.

equiv

The equivalence for the fixtype type.

pred-when-ok

A theorem asserting that a value in the fixtype specified by :ok is also in the fixtype type:
(implies (ok x)
         (pred x))

pred-when-reserrp

A theorem asserting that a value in the fixtype reserrp is also in the fixtype type:
(implies (reserrp x)
         (pred x))

not-reserrp-when-ok

A theorem asserting that a value in the fixtype specified by :ok is not an error in reserrp:
(implies (ok x)
         (not (reserrp x)))
This theorem is disabled by default, because it backchains from reserrp to ok, where the former may be used without any reference to the latter.

ok-when-pred-and-not-error

A theorem asserting that a value in the fixtype type that is not in the fixtype reserr is in the fixtype specified by :ok:
(implies (and (pred x)
              (not (reserrp x)))
         (ok x))
This theorem is disabled by default, because it backchains from ok to pred, where the former may be used without any reference to the latter.

The above events are preceded by the events specified in :prepwork, if any.

Currently the fixtype type and the first two theorems above are generated via defflatsum, but this may change in the future. Users should not rely on the generation of defflatsum, but just on the generation of the items described above.

Subtopics

Reserr: Fixtype of error results.
Reserr-option: Fixtype of optional error results.
Patbind-ok: b* binder for checking and propagating error results of the fixtype reserr.
Reserrf-push: Push the current function onto the stack of an error result, optionally with additional information.
Defresult-macro-definition: Definition of defresult.
Reserrf: Return an error result with a singleton stack.
Patbind-okf: b* binder for checking and propagating error results of the fixtype reserr.