[m-rev.] for review: parse promises

[Julien Fischer]

On Tue, 7 Dec 2021, Zoltan Somogyi wrote:

> Add missing code for parsing 'promise_ex's.
> 
> compiler/parse_item.m:
>     Add previusly missing code for parsing promise_ex declarations

s/previusly/previously/

>     (promise_exclusive, promise_exhaustive, and promise_exclusive_exhaustive)
>     of the form ":- all [vars] promise_ex... goal."
>
>     Comment out the code for parsing another form of such declarations,
>     ":- promise_ex... goal.", which also had missing code and thus
>     never worked.
>
>     Check whether the first argument of a "some" or "all" quantifier
>     is a list of variables in just one place.
>
> compiler/status.m:
>     Fix a bug in code that already had an XXX. Without this fix,
>     the new test case would get a spurious error from check_promise.m.
> 
> compiler/check_promise.m:
>     Fix several instances of another bug uncovered by the fix in status.m.
>     The problem was that the code that checked promises in the interface
>     section to see whether they contained any inappropriate references
>     to predicates or data constructors defined in the implementation section
>     considered, due to the bug now fixed in status.m, predicates and data
>     constructors imported from other modules to be defined in the
>     implementation section of this module. In fact, it did not even consider
>     the question of whether the predicate or data constructor was defined
>     in the current module at all.
>
>     Fixing this requires making a choice: may promises in the interface
>     refer to predicates and data constructors defined in other modules,
>     or not? The language manual does not answer this question, or any
>     other, about promises, since (a) all its documentation of promise
>     declarations is commented out, and (b) even the commented-out prose
>     is silent on references to other modules in promises.
>
>     The fix chosen by this diff is to let a promise refer to other modules
>     only if it is in the implementation section. The reason for this is that
>     I would find it strange to have module A rely on a promise made by
>     module B about the properties of e.g. a predicate in module C.
>     While having the code of module B itself rely on a promise that
>     module B itself makes about module C is not ideal, at least if the
>     promise is wrong, the effect of the wrong promise will be local.

If module C has been provided to you by a third-party and you do not
have its source code, you may have to make promises regarding its predicates
in module B.  That's not an objection to the above change, I'm just
noting that there is a possible use-case where promises in interfaces
that refer to entities from another module make sense.

The diff looks fine.

Julien.