[m-dev.] purity of `:- pragma foreign_proc'

[Mark Brown]

On 31-Oct-2001, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 31-Oct-2001, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> > > Before the `:- pragma foreign_proc' syntax becomes widely
> > > used, we should decide what the default purity for foreign
> > > procedures should be. If we are going to make people change
> > > their `:- pragma c_code' declarations to `:- pragma foreign_proc',
> > > we should make any purity annotation changes happen at the same time.
> > > 
> > > At the moment, predicates defined using `:- pragma foreign_proc'
> > > are `pure' by default, but predicates defined using mode-specific
> > > clauses are `impure' by default, even though `:- pragma foreign_proc'
> > > can implement a strict superset of the `impure' behaviour that can be
> > > implemented using mode-specific clauses.
> > 
> > Good point.  Probably impure should be the default.  One simple extension
> > would be to support the syntax
> > 
> > 	:- pragma pure foreign_proc ...
> > 
> > so purity could be concisely specified.  Going further, Mercury could
> > require one of pure, impure, or semipure to always be stated in the
> > foreign_proc declaration, between pragma and foreign_proc.  That approach
> > would get my vote.
> 
> That sounds like a fine approach.
> I think it is slightly preferable to the other two.
> But I'd be happy with any of the three alternatives suggested so far.

Even at the expense of a little conciseness, I'd like the word "promise"
to appear somewhere if the proc is declared to be anything other than
impure.  So far we have purposefully used this word any time there is a
proof obligation on the user, and I think it is a good idea to stick
with this convention.  When a user sees a promise, it will hopefully
remind them of the old adage about lying to the compiler.

So my vote would be for the following syntax:

    :- pragma promise_pure foreign_proc ...
    :- pragma promise_semipure foreign_proc ...
    :- pragma foreign_proc ...

The third case would of course default to impure.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------