[m-dev.] Re: more problems with t234.

[Zoltan Somogyi]

> Zoltan Somogyi, you wrote:
> > 
> > Chris wrote:
> > > I think that a solution to the problem would be to have seperate
> > > predicates for set, set2 and set3.
> 
> What is the problem that Chris is referring to?

For the version of the set and insert predicates with the bug fixed but
without separate predicates, termination analysis cannot determine the
relative sizes of the input and output arguments, thus degrading the
effectiveness of termination analysis for the callers.

> Ah, if versions 2 and 3 are equally efficient, then the criteria for
> deciding which one to include should be simplicity, IMHO.
> Why should we care how well termination analysis does on it?

(1) because we are writing a paper on termination analysis, (2) because
improving termination analysis may help us find further bugs in the system.
It was Chris's investigation of the fact that his analyzer couldn't prove
the termination of tree234__set that caused us to look more intensely at
the predicate, and led to the finding of the bug. BTW, as far as I know
this is the first time that such an analysis had such a practical result,
something we will emphasize in the paper.

In any case, the difference in complexity is not very big, and the maximum
size of a predicate is significantly smaller in version 3 than in version 2,
which can help compilation speed.

To further improve compilation speed, I will comment out the modes involving
tree skeletons in tree234.m. We know they work, but there is no reason to
keep proving that fact on every recompilation by everyone at the cost of
several minutes of compile time. We can enable them again when compile-tim
structure reuse starts working.

> > The diff for tree234.m is unreadable. Here is the affected portion of the
> > new version of the file.
> 
> In general, if the results of `diff -u' are unreadable, try using `diff -c'.
> Context diffs (rather than unified diffs) are almost always readable.

What I posted is smaller than the context diff, since the change was
essentially a rewrite of those predicates.

Zoltan.