[m-dev.] location of assertions

[Peter Wang]

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 or
another module.  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.

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