[m-dev.] location of assertions

Peter Wang novalazy at gmail.com
Mon Jul 9 11:55:22 AEST 2012

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:


It's reasonable to write an assertion in one module which makes use of
symbols from 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.
> 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.

In the long term, I think the fix is the same as for the problem
where intermodule optimisation introduces ambiguity.

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

More information about the developers mailing list