Splitting tuple types into separate modules for each

[mtzguido]

Discussed with @nikswamy today: always loading the definitions for all tuples (normal ones up to 14, dependent up to 5) is an unnecessary load on the typechecker and SMT solver.

This PR splits all tuples of arity >=3 into separate modules. The dependency analysis is modified to recognize tuple patterns and types and add the relevant dependencies (it is slightly conservative since it always treats * and & as referring to tuples even if they are overloaded, but over-approximating is not terrible here). I measured a very slight improvement in FStar.ModifiesGen (63s -> 60s). Not sure if other files will have more significant gains, but this anyway looks desirable to me.

It does mean that, in an interactive setting, if you try to use a tuple you have not yet used you will have to reload the module.

In a follow up, I think we should call the constructor for each tuple just Mk, since they are already in different modules. Also, I changed the tuple detection logic into just a table that we look up. This actually removes a few incorrect snippets, and is not too bad to maintain IMO.

[mtzguido]

@nikswamy FYI before merging we should fix Pulse and possibly other projects. If they mention, say, Mktuple3 directly now they need to use a qualified name. Pulse will break because of the snapshot too.

[mtzguido]

I have a patch for Steel+Pulse ready. HACL* is failing since I think Vale relies on the concrete location of tuples, I'm taking a look.

Maybe we wait until after the fork..?

Meanwhile I added an FStar.AllTuples module one can import to bring all tuple types in scope, for easy upgrading.

[mtzguido]

Updated on top of the new build and prelude. All tuples and all dtuples except for dtuple2 are now in standalone modules, with uniform naming, and are automatically loaded. Some projects will need a patch due to things moving modules.

I wonder if we could introduce some kind of migration mechanism like a top-level migrate Mktuple2 -> FStar.Tuple2.Mk directive, that indicates that if a name resolved to Mktuple2 in this module, then we automatically rewrite it to FStar.Tuple2.Mk and warn.

[mtzguido]

We discussed about this today and thought that it would be preferable to:

• Split tuples into modules, but retain old names (Mktuple3 instead of just Mk, etc)
• Include all of them in the Prelude
• Remove the autodetection business
  This would at least modularize the Prelude more, and parallelize the checking of all tuple types. The autodetection would help breaking some dependencies (e.g. almost no module depends on tuple14) but this isn't crucial.

However looks like this already needs some patches, including for vale which hard-codes the location of tuples:
https://github.com/project-everest/vale/blob/bbae0eb89143734363b14a77642dbf8dec36e288/tools/ImportFStarTypes/src/main.fs#L901-L904

I'm not sure how to even update Vale, so I'm not gonna push for this PR for now.