Towards a Tactics v2

In #2960 we started some work to refactor and bring some order into tactics. This was mostly motivated by tidying up the syntax representation, particularly the "punning" between de Bruijn variables and named variables both sharing the same type (bv).

The new version is more explicit about this, separating them into the bv and namedv types (latter to possibly be renamed to var). It also distinguishes binders (anonymous, essentially a type + qualifier) and bindings (an id-type pair in the environment). The reflected syntax AST and types are in FStar.Reflection.V2.Types and .Data, and have no notion of opening/closing names. That is now all done in userspace in FStar.Tactics.V2.NamedView, and marked as a plugin to be efficient.

The PR also includes already:

• Autogeneration of embeddings for inductive types, so many more functions can be made plugins easily.
• A mechanisms of extensible coercions, which already replaces the previous one. I have yet to benchmark to see if this is more expensive than before. (A @@coercion attribute is used. I considered using a typeclass, but I fear it would be too slow to call it so often.)

Compatibility

All existing metaprograms should still work as before, V1 is still present and has exactly the same semantics. All breaking changes will be done on V2 only (except perhaps for critical fixes). All Tactics and Reflection modules now point to the V1 implementation, via using an include, so open FStar.Tactics.Builtins actually opens FStar.Tactics.V1.Builtins, and likewise for most others. V2 has to be explicitly asked for.

Some modules are completely version agnostic, so there is a single one. E.g. FStar.Tactics.Visit which exposes visit : (term -> Tac term) -> term -> Tac term. Internally, it now uses V2, but the client need not care about this.

Note that the two versions "interoperate". The main discrepancy (for now at least) is the semantics and relevant types of the pack/inspect functions.

We plan to support V1 for a several more months, but eventually all code should switch to the new API.

TODO

Things to add:

• Heavier uses of typeclasses, even within tactics. MApply already uses them, as the dependencies of typeclasses were decreased significantly (and it also now has an interface, so clients pay almost no cost).
• Also we should start using typeclasses in compiler sources, it should be helpful and a good way to dogfood.
• Easier goal handling? The list-of-goals state is very annoying to handle
• Deep pattern matching on terms would be great, but that's more complicated than coercing the scrutinee.
• Consider dropping Tv_BVar from the named view?
• Plugin autoloading, immediately after typechecking, would be amazing.