[m-rev.] For review: change the way we handle inst any non-locals in negated contexts (again)

[Mark Brown]

On 15-Dec-2005, Julien Fischer <juliensf at cs.mu.OZ.AU> wrote:
> On Thu, 15 Dec 2005, Mark Brown wrote:
> > On 15-Dec-2005, Julien Fischer <juliensf at cs.mu.OZ.AU> wrote:
> > > I would still like to get rid of the pragma - I don't think promise_pure
> > > should be a pragma at all.  Since the proposal adds promise_(semi)pure
> > > annotations maybe we don't need to annotate the predicate declarations
> > > at all.  If you want promise something is (semi)pure then just put a
> > > promise_(semi)pure annotation on the top-level goal.
> >
> > That won't be able to express what we want.  A predicate or function
> > definition (as opposed to a goal) can be inferred impure for a number
> > of reasons:
> >
> > 	- because the body is impure,
> > 	- because it has a foreign_proc,
> > 	- because it has different code for different modes.
> >
> > Placing a promise on the top-level goal (that is, on the body) will deal with
> > the first of these, and there are foreign_proc attributes that can deal with
> > the second.  But the only way to deal with the third is to have a promise
> > in the declaration, or in some other item like a pragma.
> >
> 
> For mode-specific clauses can't we just require that each clause must have
> a purity annotation on its top-level goal (if it is a Mercury clause) or
> promise_pure attribute if it is a foreign clause.

But that won't mean what we want either.  The clauses may be individually
pure but they may not all implement the same relation, so the individual
promises would all be true, but the compiler would be wrong to think that
the predicate definition was pure.  Indeed, the individual clauses may be
_inferred_ pure and therefore putting a promise at the top-level would
result in an error (if you go by what I've written) or a warning (if we
decide that an unnecessary promise should only warrant that).

> Failing that, I think we should just introduce promise_(semi)pure
> declarations in place of the pragmas

That's fine by me.  I take it they would look exactly like the pragmas,
except without the "pragma".

> and not bother putting promise_*
> annotations on the pred decls.

These I still want.  Currently, and in the new proposal, this is where
the "impure" or "semipure" annotations go.  A key feature of the new
system is that, where we used to require an "impure" or "semipure"
annotation on goals, we now also allow a promise instead (*).  I'd like
this to apply to the declarations as well, so that the way you use
annotations in the declaration is the same as how you use them in the
clauses.

Cheers,
Mark.

(*) The rationale for this came up in the office discussion, and is worth
mentioning here.  Allowing a promise instead of the usual annotation saves
you from ever having to assert that something is impure, and then immediately
promise that it isn't.  This sort of situation can happen all the time with
inst 'any' in negations, but it can happen with other forms of impurity too.

For example, to get the value V of a solver variable X which we know is
ground we will be able to write:

	promise_pure ( is_ground(X, V0) -> V = V0 ; error(...) )

instead of

	promise_pure ( impure ( is_ground(X, V0) -> V = V0 ; error(...) ) )

which is what would be required if if-then-elses were to be treated like the
other impure goals.

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------