feat: Rewrite the Intervals module entirely

[bclement-ocp]

The existing Intervals module suffers from multiple drawbacks. It is undocumented, uses a questionable implementation where explanations associated with each internal bounds have unclear semantics (did I mention it is not documented), and it has been the source of many soundness bug in the past due to the way it uses exceptions to indicate emptiness. This makes it hard to extend the module; for instance #1058 was delayed because we were not quite sure whether the implementation of functions related to bit-vectors were correct.

This patch is a reimplementation of the Intervals module from scratch. The new implementation keeps the representation used by the intersect futnction in the existing implementation (and in a way can be thought of as resolving the TODO in the existing implementation suggesting to generalize that type). It is thoroughly documented, and is split between a "core" module that provides safe functions to deal with explanations, and specialized implementations for common functions (addition, multiplication, etc.) using the "core" interface such that reasoning about the implementation of addition etc. does not require thinking about explanations at all. This makes it easier to extend the module with new specialized functions.

The implementation is done through a (small) family of functors, allowing separate implementations for real and integer intervals that prevent accidentally mixing them up.

For the time being, the old interface is re-implemented on top of the new interface (except where implementation details leaked too much) so as to keep the changes mostly confined to the Intervals module. Migrating to the new interface (and especially abandoning the use of exceptions) will be done in a second step.

The patch is relatively big, but can't realistically be split into smaller parts without ending up in intermediate states full of dead code. I suggest reviewers first take a look at the documentation of the OrderedType, Interval and Union signatures in the Intervals_intf module (note that this includes some LaTeX, and might be easier to read using odoc -- I tried to make sure the odoc-generated documentation was usable). This should provide a good understanding of the "core" functionality of the new implementation. The rest of the review can be split into parts that should be mostly independent:

• Implementation of the OrderedType interface for Z.t and Q.t in ZEuclideanType and QAlgebraicType;

• Implementation of the concrete functions for addition, multiplication, etc. in the Intervals module;

• Re-implementation of the old API in the Intervals.Legacy module (and minor related changes in other modules, notably IntervalCalculus);

• Implementation of the "core" functionality in the Intervals_core module.

[bclement-ocp]

Benchmarks are +9-3 on benchtop-tests and +24-6 on ae-format (from a cursory look at the actual problems, this seems to come from the more precise tracking of explanations performed by the new implementation).

Overall things seems to be a tiny bit slower (1% or so), which I would say is fine given improvements in readability & maintainability. I know a few places where the implementation is less than optimal and could be improved upon if necessary:

• add is a translation, not an arbitrary monotone function; this was used by the previous implementation to perform less comparisons than the new implementation and we could also have a specialized implementation for add at the cost of extra complexity;
• Same for partial_map_inc and partial_map_dec, as mentioned in the documentation;
• In map_mon_to_set we are currently calling the user-provided function f on the initial/final segment when it is forbidden; this means we are often doing additions of [-oo; x] with [-oo; y1] then [y2; y3], etc. which will all ultimately be subsumed by [-oo; x + yn]. We can do better and avoid doing this, at the cost of additional complexity again.

[bclement-ocp]

@Gbury given that you have made a bunch of fixes to the intervals module in the past & some conversations we had wrt API for this module, I'd appreciate your input on the interface file intervals_intf.ml if you find the time to take a look.

[Halbaroth]

I'm doing a second pass on this PR. Sorry for the partial review.

[bclement-ocp]

Many replies inline, I tried to add a bunch of documentation. I also moved all the loop ... (Ex.union ex ex') lines to always be the first of the pattern-matching; hopefully that helps showing that this is not the important case.

Should be ready for round 2.

[Halbaroth]

Thanks for the clarification :)