[m-dev.] Q: assigning pred_ids to functions

[Fergus Henderson]

On 29-Jul-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> On 29-Jul-1999, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> > On 29-Jul-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> > > Currently the assertion
> > > 
> > > :- assertion all [A,B,C] ( C = A + B <=> C = B + A ).
> > > 
> > > cannot be used since it parses as unifications not function calls.
> > > 
> > > The compiler notes say that this is done in modecheck_unify.m, but it
> > > appears to me that it is done in polymorphism.
> > > 
> > > So my question is where is it done?
> > 
> > polymorphism.m.  This was changed in my recent existential types changes.
> > I'll fix the documentation.
>
> Thanks for that.

By the way, you might want to move that code from polymorphism.m
into post_typecheck.m (and insert calls to it from purity.m).

> Now for my next question.
> 
> Say I have the above assertion in the interface section for int.
> The assertion then gets written to 'int.int'.
> 
> Now when I use my file foo.m, I would like to import that assertion.
> 
> However since the assertion is an arbitary logic formula we will run
> into problems.  Could you remind me what they are again.

Suppose the interface section of `int.m' imports module `bar'
in its interface and module `baz' in its implementation.

The first problem is that when compiling `int.m', the assertion will
get typechecked with all import of `baz' being visible, so the compiler
won't complain if it contains calls to `baz__whatever', even though it
ought to report an error for such calls (since stuff in the interface
should not depend on modules which are only imported in the implementation.)

The second problem is that when compiling `foo.m', the compiler will
only include the types, modes, and insts from module `baz', since it
assumes that stuff in the interface of `bar' can only depend on the types,
modes, and insts from the modules that bar's interface imports.
So if the assertion contains calls to `bar__whatever' the compiler
will report spurious errors.

Solving those problems is definitely non-trivial, so if you're looking
for a short-term solution, I suggest that for now you should just change
things so `:- assertion' declarations are not allowed in the interface.
Or for a slightly more complicated alternative, you could require that any
`:- assertion' declarations in the interface of a module only contain data
constructors, functions, and predicates from that module, not from any
imported module (you'd need to add extra code to check this).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------