[m-dev.] location of assertions

[Julien Fischer]

On Mon, 9 Jul 2012, Peter Wang wrote:

> On Mon, 9 Jul 2012 02:40:23 +1000 (EST), Julien Fischer <juliensf at csse.unimelb.edu.au> wrote:
>>>
>>> However, there is (currently?) a restriction that assertions in the
>>> interface can't refer to any symbols defined in the implementation
>>
>> As you would expect.
>>
>>> or another module.
>>
>> That might be more problematic.
>
> I think the restriction was only intended as a short-term measure:
>
> http://www.mercury.cs.mu.oz.au/mailing-lists/mercury-developers/mercury-developers.9907/0265.html
>
> It's reasonable to write an assertion in one module which makes use of
> symbols from another module:
>
> http://www.mercury.cs.mu.oz.au/mailing-lists/mercury-developers/mercury-developers.9908/0117.html

Yep, that's why I described it as problematic.

>>> This is checked while compiling, but not while
>>> making the interface file.  I wonder if we can use the restriction to
>>> module-qualify assertions unambiguously.
>>
>> By restricting assertions made about a predicate to the module that
>> declares the predicate?  For associativity, commutivity and state update
>> assertions that doesn't seem to be an issue.  In principle, it could
>> be a problem for construction equivalence assertions, but in practice
>> I suspect it wouldn't be.  (Or at the least, that programmers could
>> live with that restriction.)
>
> We could require that assertions in the interface have fully-qualified
> references to any symbols outside of the current module.  Unqualified
> symbols would be qualified to the current module when making the
> interface file.

That bothers me a little, since it means assertions don't behave like
other declarations that can occur in a module interface w.r.t module
qualification.

(OTOH, I can't think of any better solution to this that doens't involve
shifting the generation of interface files until after type checking.)

Julien.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------