[m-dev.] more correctness problems

[Kathryn Francis]

On Thu, 30 Mar 2006, Ralph Becket wrote:

> schachte at csse.unimelb.edu.au, Thursday, 30 March 2006:
> > Hi all,

> >
> > Note that this problem is different from the problem of negations
> > involving any insts.  There the concern is that a negated goal should
> > not further constrain a non-ground variable.  I don't imagine there
> > are many goals involving any inst variables that don't constrain those
> > variables, so I don't expect there would be many cases where a negated
> > context mentioning an any inst variable is sound.  They really should
> > be impure.
>
> There are many sound cases where you end up with a solver variable in
> the condition of an if-then-else.  For example, list.length(Xs) (Xs is a
> list of solver vars) or any_map.search(AnyMap, Key, X) (AnyMap contains
> solver vars, but Keys are ground).  Currently the compiler *does* require
> such situations to be treated as impure.  It has been suggested (and I
> think it's a good idea) that such things should instead only be allowed
> in a scope that states explicitly the nature of the problem (e.g.,
> something like promise_solver_type_in_negation_is_sound, but hopefully
> less wordy).
>

I don't know if this is possible, but it would be nice to have a mode
which meant that the argument was input only, even though it was of inst
any. Currently we have oa which means that this any inst argument is only
an output (it starts free), but ia means the argument is both input and
output. There's no way to say that an argument has inst any before and
after the call, but after the call it still has the same partial
instantiation, ie it has only been used as an input and hasn't been
constrained further.

If there was such a mode (and again I don't know if it's possible for the
compiler to check such a thing), then predicates using this mode would be
safe inside a negated context, while those using the in-and-out ia mode
would not.

Kathryn

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