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

[Julien Fischer]

On Thu, 15 Dec 2005, Mark Brown wrote:

> 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".
>
Yes, assuming that actually works with the current parser.

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

The impression I received further back in this thread was that we didn't
want to allow the promise_* annotations on the predicate declarations
for exported predicates.  I am opposed to the idea of allowing them
on local pred declarations but not on exported ones.  In that case
I would just prefer that we have separate promise_(semi)pure
declarations and not allow promise_(semi)pure declarations on predicate
declarations at all (lambda expressions would be okay though).

> (*) 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.
>

That's fine, it's the annotations on predicate declarations not goals
that are the issue here.

Cheers,
Julien.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------