# 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.

- Mutual exclusivity:

      	:- all [X, Y] promise_exclusive
      		some [Z] (
      			p(X, Y, Z)
      		;
      			q(X, Y, Z)
      		).

- Exhaustiveness:

      	:- all [X] promise_exhaustive
      		(
      			p(X, _)
      		;
      			q(X, _)
      		).

- Both together:

      	:- all [X] promise_exclusive_exhaustive
      		some [Y] (
      			p(X, Y)
      		;
      			q(X, Y, Z)
      		).

All three declarations are restricted in the following ways:

- Any variable that occurs in more than one disjunct must be explicitly quantified.
- Any variable occurring in only one disjunct is existentially quantified. This is similarly applicable when an underscore is used in place of a variable.

## 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.
   - The operators are defined (library/ops.m).
   - The structure for promise ex declarations in the parse tree is defined (prog_data.m).
   - They are parsed and entered into the parse tree (parse_item.m).
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.
   - Error checking (make_hlds.m).
   - Entering of declarations into the HLDS as dummy predicates (make_hlds.m).
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).
   - Post typechecking processing initiated for promise ex declarations (purity.m).
   - promise_exclusive and promise_exhaustive declarations are indexed by the predicate calls made in them in the exclusive table (post_typecheck.m).
   - Definition of exclusive table as part of HLDS, and operations on the table (hlds_module.m).
   - (*) Where a promise_exhaustive declaration is paired with a promise_exclusive declaration, they are merged into a promise_exclusive_exhaustive declaration; otherwise the promise_exhaustive declaration is entered in the exhaustive table of the HLDS (post_typecheck.m).
   - (*) Definition of exhaustive table as part of HLDS, and operations on the table (hlds_module.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).