[m-dev.] location of assertions

Julien Fischer juliensf at csse.unimelb.edu.au
Tue Jul 3 21:36:52 AEST 2012

Hi Peter,

On Tue, 3 Jul 2012, Peter Wang wrote:

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

Agreed.  (Essentially what I am proposing above is that we should change

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

Write them where in expanded form?  The problem in bug #193, is that
type (and module?) qualifiers cause the form of the assertion clause to
change in such a way that the code in the accumulator introduction pass
doesn't (currently) recognise them as valid assertions of the types it

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