Add utility function to deal with mutual dependency across different modules

[W95Psp]

(this issue was extracted from #203 (comment))

Rust modules are really about namespacing. Rust allows items to be mutually recursive across modules.

This is rarely allowed in other statically typed languages, and even less in proof assistants. Thus, we need a strategy for removing such recursive bundles that span across multiple modules.

Example

Situation A

mod a {
    pub fn f (x: u8) -> u8 {
        if x < 0 { x } else { super::b::f(x - 1) }
    }
}
mod b {
    pub fn f (x: u8) -> u8 {
        if x < 0 { x } else { super::a::f(x - 1) }
    }
}

In this case, we should probably transform to:

mod bundle_a_b {
    pub fn a_f (x: u8) -> u8 {
        if x < 0 { x } else { b_f(x - 1) }
    }
    pub fn b_f (x: u8) -> u8 {
        if x < 0 { x } else { a_f(x - 1) }
    }
}
mod a { pub fn f (x: u8) -> u8 { super::bundle_a_b::a_f(x) } }
mod b { pub fn f (x: u8) -> u8 { super::bundle_a_b::b_f(x) } }

Situation B

We can also write something like:

fn f() {}
mod b {
    use super::*;
    pub fn g() {super::f ()}
}
fn h() { b::g() }

Here we have:

• a dependency from b to a (a::b::g uses a::f);
• a dependency from a to b (f::h uses a::b::g)

In this case, we can either:

• make a bundle for f, g and h just like above;
• make a bundle only for f and g and use that in the rest of the top-level module.

Solution

We want our module-level dependency graph to be a tree.
For this, we should identify every group of items that span across multiple modules and isolate them in newly named modules.

This is partially implemented by engine/lib/dependencies.ml, but we need to revisit it and test it heavily.
This issue is blocking for extracting Core to anything (F*/Coq/whatever) useful.