[m-dev.] location of assertions

[Julien Fischer]

On Thu, 5 Jul 2012, Peter Wang wrote:

> On Wed, 4 Jul 2012 21:19:46 +1000 (EST), Julien Fischer <juliensf at csse.unimelb.edu.au> wrote:
>>
>> On Wed, 4 Jul 2012, Peter Wang wrote:
>>
>>> On Tue, 3 Jul 2012 21:36:52 +1000 (EST), Julien Fischer <juliensf at csse.unimelb.edu.au> wrote:
>>>>
>>>> Agreed.  (Essentially what I am proposing above is that we should change
>>>> it.)
>>>
>>> I've made progress with this proposal but if I'm not mistaken, .int
>>> files are generated without type checking, which would be required to
>>> module-qualify the symbols in assertions.
>>
>> I don't think type-checking is required, IIRC all module-qualification
>> occurs before type-checking.  What does happen however, is that the
>> interface files are generated before all module-qualification takes
>> places; in particular module-qualification of clauses (which is how
>> assertions treated by most of the frontend) doesn't take place until
>> after the interface files have been generated.
>
> Type checking is required to resolve ambiguities in clauses, though.
>
> 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.

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

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