Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Rewrite the Intervals module entirely #1108

Merged
merged 6 commits into from
Jun 12, 2024

Commits on Jun 11, 2024

  1. feat: Rewrite the Intervals module entirely

    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 OCamlPro#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 committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    fba4054 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    5e36e65 View commit details
    Browse the repository at this point in the history
  3. More Stdcompat

    bclement-ocp committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    a1971c7 View commit details
    Browse the repository at this point in the history
  4. Even more Stdcompat

    bclement-ocp committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    fc4db30 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    4ab06de View commit details
    Browse the repository at this point in the history

Commits on Jun 12, 2024

  1. Missed doc annotation

    bclement-ocp committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    dfd4be7 View commit details
    Browse the repository at this point in the history