Outcome
Fixtype of Syntheto outcomes.
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :function-success → outcome-function-success
- :type-success → outcome-type-success
- :specification-success → outcome-specification-success
- :theorem-success → outcome-theorem-success
- :transformation-success → outcome-transformation-success
- :proof-obligation-failure → outcome-proof-obligation-failure
- :theorem-failure → outcome-theorem-failure
- :transformation-failure → outcome-transformation-failure
- :unexpected-failure → outcome-unexpected-failure
Each type of top-level definition, when submitted to ACL2,
will be accepted or rejected. The success or failure
of the submission is modeled by an outcome, which is returned
to the submitter.
A function or clique of mutually-recursive functions, when
submitted successfully to ACL2, is represented by function-success.
Similarly, a type definition or clique of mutually-recursive type
definitions is represented by type-success. Specifications,
theorems, and transformations also have success types.
Since a successful transformation results in new submitted top-level
definitions, those are returned as part of the success outcome.
For submission of a top-level definition to be accepted,
there are certain implicit proof obligations such as termination and
guard verification. If one of these fails, a
proof-obligation-failure outcome is returned, containing
an expression that could not be proved. This failure may result for a
number of different reasons, and may result from a number of different
top-level constructs including failure to prove the applicability
condition of a transformation.
If a theorem is submitted that is not mechanically proved by ACL2,
a theorem-failure outcome is returned.
If a transformation is submitted that is applicable, but fails
due to some other reason, potentially a transformation-failure
outcome is returned.
Any other submission failure results in a unexpected-failure
outcome, which might have been expected but is at least not otherwise
classified.
Subtopics
- Outcome-fix
- Fixing function for outcome structures.
- Outcome-case
- Case macro for the different kinds of outcome structures.
- Outcomep
- Recognizer for outcome structures.
- Outcome-equiv
- Basic equivalence relation for outcome structures.
- Outcome-proof-obligation-failure
- Outcome-transformation-success
- Outcome-kind
- Get the kind (tag) of a outcome structure.
- Outcome-unexpected-failure
- Outcome-type-success
- Outcome-transformation-failure
- Outcome-theorem-success
- Outcome-theorem-failure
- Outcome-specification-success
- Outcome-function-success
