[m-dev.] location of assertions

[Julien Fischer]

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

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

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