Share the fixNode function

[Jogo27]

The function check whether the premises have change and computes a new resolution only if they do. It is used in most of the compression algorithm implemented so far : RPI/LU, RedRec, RU and more. The difficulty is to find a good place for it.

[ceilican]

Yes. Which candidate places have you already considered?

[Jogo27]

The solution I like the most is to add a trait in algorithm/compressor/package.scala. The drawback is that this function may be usefull for some non-compressing algorithm. But for now it's only useful there.

A second solution is to add the function to Proof (or a subclass of it, or a trait). I find this solution unnatural, but it''s perhaps just a matter of taste.

Another solution is to add it to ProofNode, SequentProofNode, lk or R. But I prefer to keep this classes lightweight. And I think this functionality should be implemented as a function, not as a method.

The last solution is to add an util.something object. I don't like this solution. I think the fewer util objects we have, the better.

[ceilican]

I also prefer the trait solution.

Joseph: it seems that Andreas has just implemented this.