Promise Ex Declarations

This document is a description of promise ex declarations, which are currently unfinished and as such are undocumented in the reference manual.

Syntax

There are currently three promise ex declarations: promise_exclusive, promise_exhaustive, and promise_exclusive_exhaustive. They are used to denote determinism properties of a disjunction, and denote either exclusivity, exhaustiveness, or both. The examples of each, given below, also show the different ways that existential quantification can be handled. All three declarations are restricted in the following ways:

Development

This tracks the use of promise ex declarations through the compiler, and may be useful as a quick summary of the current state of development. Items marked with an asterisk (*) are not yet implemented. Places where data structures etc. have been defined are in italics. (The module names listed have suffered bit rot.)
  1. The declarations enter the parse tree.
  2. They may be pretty printed (mercury_to_mercury.m, parse_tree_out.m).
  3. They are error checked, and entered into the HLDS as dummy predicates.
  4. They go through typechecking as predicates. After the typecheck, post-typecheck and purity passes of the front-end, they are removed from processing as predicates and entered into the appropriate table in the HLDS (by check_promises.m).
  5. (*) Exclusivity information is used during switch detection, and where it leads to a full switch being made, applicable exhaustiveness information is also used (switch_detection.m).
  6. (*) Exhaustiveness information is used during determinism analysis (det_analysis.m) or as an add-on to switch detection (switch_detection.m).