Add possible analysis V and G coupling layer

[sim642]

This is a quick sketch of the kind of coupling of V and G modules I described during today's GobCon regarding @michael-schwarz's question.

To use this untested prototype, replace

module V = Foo
module G = Bar

in an analysis with

include Vg.Make2 (Foo) (Bar)

Then instead of man.global and man.sideg, use (currently not so well named/scoped) global man and sideg man.
Additionally, there's all_globals man.

The generality of this interface is that Vg.Make2 could be in-place replaced with Vg.Make3 to switch from the extra-unknown-based trick to a map domain instead (the kind of thing used for privatizations for similar stuff). This is probably just less efficient, but such change should require no other code changes at global, sideg and all_globals.

On the other hand, switching Vg.Make2 to Vg.Make would just remove all_global and just be a thin wrapper against the initial approach. But all the uses of global man and sideg man should remain valid.

TODO

• Improve file module name Vg
• Improve functor names Make, Make2, Make3.
• Try abstracting Either/Lift2 construction from existing analyses.

[michael-schwarz]

Thanks for the PoC! I'll probably be only able to look into it after VDS, but I guess it doesn't become stale too quickly.

[michael-schwarz]

I added this to my TODO list, hopefully I will be able to review during / just after my trip to Munich.

[michael-schwarz]

Nice! I think we want to have something like this!

• My initial concern was that someone could side-step this interface by using man directly, but this would then not type anymore, which is good.
• I think the naming should be improved, Make, Make2, and Make3 are not intuitive.
• This should come with a warning sign that everything that uses all_globals will potentially be very expensive, as it gets re-evaluated every time a new global appears. So one really only use this interface if there's no other way to know which unknowns to query.

---

@sim642: What do you think is the best way forward here? Should we merge this (after addressing the things above), and I try to use it in #2072 and see if it does what I want it to do there?

---

@hseidl, @arkocal, and I also started talking about something similar in the context of implementing history tokens at globals where this would be needed to tame infinite sets of things that are compat# (or, more generally, cases where it's hard to conjure up possible other unknowns, e.g., for thread ids).

[sim642]

• My initial concern was that someone could side-step this interface by using man directly, but this would then not type anymore, which is good.

Indeed, the underlying types are left completely abstract by the signature, so it's even impossible to side-step this interface when one knows which variant is being used under the hood.

• I think the naming should be improved, Make, Make2, and Make3 are not intuitive.

I think the bigger question might be what to call the file module itself, currently it's just Vg... (which could also be confused with https://opam.ocaml.org/packages/vg/).
I currently don't have any amazing ideas: GVars, VarDom, GVarDom, …?

Also, in the current form it's quite specific to being used as V and G via include. If we want to reuse similar abstract constructions for other things (paths, history tokens, …), then some more generic names (K and V?) would be better. But then again, this becomes a bit less convenient if one has to still write some module V = M.K and module G = M.V.
But we probably don't need to aim for such generality right now.

@sim642: What do you think is the best way forward here? Should we merge this (after addressing the things above), and I try to use it in #2072 and see if it does what I want it to do there?

It might be better to try to at least locally merge this into #2072 and see if this does the job. If not, then it'd be better to rethink immediately than merging something useless.

I'm interested in trying out if the common V = Either and G = Lift2 pattern can also fit into this, e.g. by defining a combinator on the Vg.S pair directly. If that works, then this would already be convenient in various places that currently duplicate analogous helpers.