[m-dev.] location of assertions

[Julien Fischer]

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

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

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