[m-dev.] location of assertions

[Peter Wang]

On Mon, 2 Jul 2012 18:18:41 +1000 (EST), Julien Fischer <juliensf at csse.unimelb.edu.au> wrote:
> 
> On Mon, 2 Jul 2012, Zoltan Somogyi wrote:
> 
> > On 02-Jul-2012, Peter Wang <novalazy at gmail.com> wrote:
> >> Assertions required for accumulator introduction are supposed to be
> >> written out to .opt files, right?
> >
> > I don't think that was ever specified; assertions were always too experimental
> > for that. But yes, if all the things (predicates, types) mentioned in an
> > assertion are exported, I think the assertion should be exported as well.
> 
> You would want them in the .int file if they are originally exported
> from a module.   Local assertions should of course appear in the .opt
> file as per local procedures that end up being opt-exported.   (They
> should of course appear in the appropriate private interface file
> whenever submodules are involved.)
> 

In terms of what was intended up till now:

1. intermod.m contains code to write assertions out to .opt files.
   It is never used because predicates representing assertions have
   `status_local' which causes them to be filtered out.

2. modules.m says:
    % Strip out the imported interfaces, assertions are also
    % stripped since they should only be written to .opt files,

That is not to say we shouldn't change it.

> Incidentally, there's an open issue with asssertions and type
> qualifiers, see bug #193
> <http://bugs.mercury.csse.unimelb.edu.au/view.php?id=193>.
> 
> (The fix for #193 is to normalize the form of the assertion clause and
> eliminate the introduced variables just before it is entered into the
> assertion table.)

Is there are reason to write assertions in expanded form?

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