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.