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.)

New view

The previous term_view type was used both for working with locally nameless terms (via inspect_ln/pack_ln) and fully-named terms (with inspect/pack, in Tac). This causes some "slack" in the type, since e.g. a Tv_BVar node should never appear when using the Tac view; and as mentioned before the bv type has two potential meanings: bvar index or unique identifier for a named variable. Another annoyance is that bv, binder, comp, etc, are all abstract and also require using a view (mostly as a consequence of them referring to the internal F* equivalent).

The new FStar.Tactics.NamedView module, included for all clients who open FStar.Tactics, aims to solve some of this by:

• Re-defining (i.e. shadowing) bv, binder, comp, etc, by (almost) their views, so the user can directly work with the underlying records and never do pack/inspect of these. For binder, the new type is a record with all fields of the pure binder_view (sort, ppname, attrs, qual) plus a unique identifier (a nat), as this is a fully-named binder.
• Defining a separate named_term_view type, which uses the types above instead of the abstract ones, so things like these work automatically:

let domcod (t:term) : Tac (term & term) =
  match t with (* NB: coercion inserted *)
  | Tv_Arrow (b, C_Total t) -> b.sort, t
  | _ -> raise NotATotArrow

• Defining inspect : term -> Tac term_view / pack : term_view -> Tot term fully in userland, essentially as:

let open_view : term_view -> Tac named_term_view = ...
let inspect (t:term) : named_term_view = open_view (Reflection.inspect t)

let close_view : named_term_view -> Tot term_view
let pack (tv:term_view) : Tot term = Reflection.pack (close_view tv)

• Types defined in this module can also easily use record payloads on inductives as it is all userspace. (For more primitive types, we'd need to write complicated embeddings/unembeddings due to the indirection via another type.)

So, when using tactics, the user should not open FStar.Reflection (or open it before FStar.Tactics so the latter takes precedence), and work with the named view directly. There is the possibility of confusion since the types are named the same... just that they are in different modules. Any opinions about it...?

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. See https://github.com/FStarLang/FStar/pull/2969

• 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.

• Interactivity of some form. At the very least, decouple the tactic in an assert by from the top-level definition, so it can be tackled after checking the skeleton, and tweaked without rechecking it.

• Efficiency. Perhaps use NBE.