[m-rev.] diff: avoid runtime aborts from the decl debug oracle

[Mark Brown]

On 11-Oct-2002, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> On 11-Oct-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > Another solution to this problem may have been to implement a 'set_cc'
> > module, which would be to 'set' as 'tree234_cc' is to 'tree234'.
> > Unfortunately, we would need to implement 'set_cc__intersect' but it
> > appears not to be possible to implement a satisfactory committed choice
> > version of intersection.
> 
> What is wrong with the obvious solution of using the code of
> set_ordlist__intersect after replacing the call to compare with a call
> to compare_representation?

I'll illustrate the way the oracle would hypothetically use set intersection
with the following example (it is hypothetical because we aren't yet able to
save the oracle state between invocations):

	1) The user is asked a missing answer question for p, for which the
	solutions are A, B and C.  The user asserts that this set is complete
	(but it may contain wrong answers).

	2) The user goes on to diagnose a bug, then saves the oracle
	state, fixes the bug, and fires up another debugging session to
	diagnose some other symptom.

	3) The user is again asked about that call to p, but this time the
	solutions are A, B and D.  The user asserts that this set is also
	complete.

	4) At this point, the oracle deduces that {A, B} must be a complete
	set of solutions for that call to p, since it is the intersection
	of the two previous complete sets.

Now, imagine that the meta-variables C and D represent two functions
which are equal but represented differently.  With set_cc__intersect the
deduction at 4) would still be made, but it would be wrong.  If at some
later stage the oracle was asked about the call to p with solutions {A, B},
it would wrongly say that it knows the answer to be "yes", when in fact
it shouldn't know the answer.  The user will not even be aware that the
question has been asked.

The way we currently use tree234_cc, on the other hand, is different.
If we try to look up some higher order term in one of these and the search
fails due to some difference in representation, then the worst that will
happen is the oracle will say "don't know" when it should know the answer,
which means is that the user may be asked some questions that ideally could
have been avoided.  Compared to above, this is a relatively innocuous
problem.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------