Generic support for parsing optional arguments in Ltac2 tactic notations

[mattam82]

This PR adds a new scope attributes (which could also be called options, but reuses the genric s-expr structure of attributes) for Ltac2 notations and an API to consume attribute declarations (hiding the ADT but letting users access most of the functionality). Right now they are parsed using @[ attribute_list ] so one can write tactic notations like:

  typeclasses eauto @[best_effort, strategy="dfs", depth="1"] with typeclass_instances.

After talking with PMP, this seems like a more lightweight solution than generally extending Ltac2's type system with optional arguments. It also stays at the parsing level, so we don't need to do much at the ML level really. The solution using (delimited) attributes also avoids any potential headache with factorization of rules or crazy GADTs to have a generic mechanism in ML to parse options in any order while writing type-safe code.

Kind: feature / infrastructure.

There is a bit of Ltac2 code used to generically parse flags/options but this is all user customizable: we have more or less access to the raw sexprs of attributes, as in the vernac level.

• Added / updated test-suite

• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).
• Overlay pull requests (if this breaks 3rd party developments in CI, see
  https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md for details)

[gares]

Personally, I would prefer #[...] t and have ltac2 expose this optional argument as it prefers.

The syntax for #[...] <tactic> would be there automatically, for all tactics, as it is there for all vernaculars (here <tactic> is the non terminal we extend when we write TACTIC EXTEND and co). Then each tactic can ignore, error, or use the attributes, be it written in ltac2 or ML or you name it, as vernaculars do.

In this way there is no consistency problem, and we decorrelate the optional presence of the attributes with the way the languages in which the tactics are written do represent optional arguments.

If we don't like #[] or we want a postfix version, that is another story. And even this PR, I think it should be split in 2 parts, attributes to tactics and ltac2 API to access them. If we want a syntax for optional arguments in ltac2 notations, it is yet another story.

[ppedrot]

@gares you really can't do that, for quite a lot of reasons.

1. It would immediately create a parsing conflict with proper command attributes when in head position.
2. Attributes currently only apply to commands, what you propose doesn't make sense for subterms.
3. How would you even type that? You can't expect all your functions to take a leading option without breaking all kind of HO.

I think I have not repeated that enough during the talk, but the current PR is about Ltac2 notations. Passing arguments to an Ltac2 function should be performed as ML arguments. There seem to be a lasting confusion between static semantics with runtime semantics, the kind of which led to the Ltac1 nonsense...

[gares]

The parsing conflict is easy to fix, we already parse Time Check .. and Time apply .... It is indeed the only parsing conflict an LL grammar solves easily by factoring the common prefix.

The attribute would apply to the head notation as well, eg (#[foo] tac1 + #[foo] tac2). Of course #[foo](tac1 + tac2) would also parse, and tclPLUS would error it does not support attributes, or it could even be the ast -> Proofview.tactic step to fail (to avoid having a ~atts argument just to say no). #[foo] x for an x bound could be an error detected in that phase too.

[mattam82]

This might be a recipe for disaster, but what you propose Enrico could give a way to have versioned tactics as in:

((#[compat="8.5"] apply foo); destruct k)

I think we thought about something like this when discussing how to allow tactics to evolve while maintaining compatibility before. I find it slightly funny to pass options before the tactic itself but we might get used to it...

[gares]

I think I don't see attributes as arguments (of a vernac) anymore, but rather as options for it. In a sense, I prefer #[nodelta] apply t, #[TC="off"] refine to the current way of doing, the idea being that apply t convoys the intent, and #[bla] is just technical stuff.

[ppedrot]

@gares I am really afraid this doesn't make sense at all in the Ltac2 evaluation model. Look at what attributes are used for in OCaml for a reasonable semantics.

[gares]

What I propose is fully static, so something escapes to me. What makes them dynamic? (we ruled out HO stuff)

[mattam82]

Yes, maybe there is a misunderstanding here. This syntax shall never allow to do:

Ltac2 foo := 
  let myopt := ... in
  #[foo=myopt] bla.

[ppedrot]

@gares OK, I might have misunderstood you. So you want to make any Ltac2 notation take an optional attribute and expand it away statically? If so, how are you even going to make any complex parsing rule work? You'll get those nasty attributes in the way of your syntax factorization almost immediately.

[ppedrot]

Also, @mattam82 's proposal subsumes yours in this case. It just enforces the fact that all notations must accept this and that the position is restricted to be the leading one, both features which I believe are defeating the purpose of notations.

[ppedrot]

It is indeed the only parsing conflict an LL grammar solves easily by factoring the common prefix.

Except that IIUC entries are significant in camlp5 so factorization won't happen across different entries, which is the case for vernac vs. Ltac2. We have to hack the grammar to make this work for the various Print commands and friends, it's a nightmare.

[gares]

We have to hack the grammar to make this work for the various Print commands and friends, it's a nightmare.

I understand you don't like fighting with the parser. I don't either, but if this is the only thing keeping us away from a uniform syntax, I offer my time to make the parsing engine do what we want (I believe it's time well spent).

[gares]

So you want to make any Ltac2 notation

Any tactic notation, not just the ones created via ltac2. It is really like the thing we do with the vernacular commands. E.g. in elpi I have a Tactic Extend for elpi tacticname arguments and I'd like that one too to accept attributes, (exactly as I could do with the Vernac Extend for Elpi commandname arguments).

[ppedrot]

But Ltac2 notations do not serve the same purpose as TACTIC EXTEND. The former can be used to define mere pieces of syntax, for which attributes do not make sense. Why would you ever write an attribute for the boolean and notation &&?

this is the only thing keeping us away from a uniform syntax

No, it's not a matter of uniformity nor parser fighting. It's that in general it doesn't make sense (sorry to insist) to ask for an attribute without completely breaking the point of the notation. Once again, pick the boolean and notation and consider the fact that if ever you were to add an attribute somewhere it would completely break the associativity / precedence of that rule. Why don't you trust the user to let him put attributes where it makes sense instead of imposing a parsing rule that is useless in 99% of the cases?

[mattam82]

I think there is a basic misunderstanding stemming from the semantics attached to attributes. While I understand that we would like to use attributes for general treatment of options for vernac commands (Elpi/Equations/Definition/Function...) I also side with @ppedrot that for tactic notations, we don't need to restrict ourselves to having a prefix #[opt1=value1] tactic notation which could also be problematic to parse. I also find myfancysmt @[debug, atp="Z3"] to carry the intent more explicitly than #[debug, atp="Z3"] myfancysmt. I don't know of any other system that passes options before the object that takes them, and to me it would lead to think that #[debug] (tac1 ; tac2) should work in that case, somehow passing the debug flag to whatever tac1 and tac2 are, i.e., a general option passing mechanism for all tactics (probably that would be carried around by the proof/tactic engine as additional state). As you pointed out @gares these are two different things: one is a way to pass general options to tactics while what I intended to provide here is a way to pass optional arguments to a specific tactic.

[gares]

The syntax of attributes is dumb and open so that we can pass to all commands options without hacking the parser. I think it serves this purpose very well. Here it seems one has to define a specific notation for each tactic he wants to get options to. So the point about being generic seems moot.

Moreover, in the running example, there is already an optional argument, the "with db" one. I frankly don't see why the others can't be a key value pairs that follow it, eg with depth=1, strategy=dfs.... It seem much more consistent with the other tactics no? (and even stay open ended, if you really want to, like attributes).

I'm sorry, but It still looks like a hack to me.

[Zimmi48]

One point in favor of reusing the generic attribute syntax: most attributes (though not all) amount to locally setting some option (and some even have a corresponding option that can be set globally). The obvious semantics of #[ X ] (tac1; tac2) would be to set X for both tac1 and tac2. This would mean that both tac1 and tac2 should support the attribute X. For some attributes, it could make sense to have many tactics support them (or even all tactics, with some of them just ignoring them), for instance for attributes that would be used to parametrize the behavior of the unification engine (they could even be used to choose locally between the legacy and the future unification engine, instead of having to set a global option).

That being said, the current proposal still satisfies my initial request which was to avoid syntactic explosion when tactics take many arguments. It satisfies the two important characteristics that the attributes / optional arguments are well parenthesized (so no risk to confuse them with term arguments or any other syntactic part of the tactic) and that the attributes / arguments can be passed in any order.

[gares]

attributes / arguments can be passed in any order.

I think this is totally possible even with with foo=bar, baz=1, what you need is access to a non terminal for this sytnax so that you don't have to write its grammar by yourself (and which can produce an Attribute.t data type, if this is what one wants).

About confusing them with the other arguments, it goes both ways IMO. with is a keyword already, even syntax highlighting will tell you. If you want confusion, what about tac l1 @[x] ? (my ocaml-burned retinas will think we are passing the list l1 with [x] appended to it, not that it's an error because the optional x goes first).

[ppedrot]

You still need delimiters to work around the fact that people may randomly register keywords.

[gares]

I don't think the problem with keywords has anything to do with delimiters

Coq < Notation "'foo'" := 3.
Identifier 'foo' now a keyword
Setting notation at level 0.

Coq < #[foo="broken"] Check nat.
Toplevel input, characters 2-5:
> #[foo="broken"] Check nat.
>   ^^^
Error:
Syntax error: [attribute_list] expected after '#[' (in [quoted_attributes]).

[ppedrot]

But the fix, yes. If you have a delimiter you can basically use an unlimited amount of lookahead to disregard to ident / token difference and roll up your own well-delimited parser for this grammar.

[Zimmi48]

If you want confusion, what about tac l1 @[x] ? (my ocaml-burned retinas will think we are passing the list l1 with [x] appended to it, not that it's an error because the optional x goes first).

Just always put the attributes first.

[mattam82]

If you want confusion, what about tac l1 @[x] ? (my ocaml-burned retinas will think we are passing the list l1 with [x] appended to it, not that it's an error because the optional x goes first).

Just always put the attributes first.

f foo @[x] is not valid ML syntax for passing to f foo@[x], they need delimiters too: f (foo@[x])!

[gares]

OK, this discussion is going nowhere. I don't like this new syntax and I don't see what it unblocks. At the call Cyril did not like it either because it inconsistent with a very similar syntax we already have. If you think this design is good enough, go ahead, I won't question further.

[mattam82]

Well, I get your point about consistency, and I didn't think of the traditional keyword with connector which is already used for different options by at least (e)autos to pass a db and apply foo with, so I would be more favorable to the convention of passing optional arguments to tactics using with after their main arguments, keeping with the current standard. It would then look like typeclasses eauto with depth="5", strategy="dfs", dbs=("foo", "bar"). @ppedrot would that cause any parsing problem? I'd keep the generic Attribute.t API, maybe just renaming all this to Options.t to advertise it to Ltac2 users as a generic option handling library.

[ppedrot]

would that cause any parsing problem?

Yes. See my last post.

[gares]

FTR, since we are likely to have a tactic in Elpi which will go "in production" soon, I did push the integration of Elpi-written tactics a bit further, as for command, so that one does not have to write "elpi tactic" to run it, but just "tactic". In passing, I tries to add support for attributes (as I did for commands).

As you can see, even without modifing Coq the results is quite OK, and the only problem/conflict would vanish (I'll prepare a PR for Coq shortly). Here the doc I wrote:

Attributes

Attributes are supported in both commands and tactics. Examples:

• #[ att ] Elpi cmd
• #[ att ] cmd for a command cmd exported via Elpi Export cmd
• #[ att ] elpi tac
• Tactic Notation ... attributes(A) ... := ltac_attributes:(A) elpi tac.
  Due to a parsing conflict in Coq grammar, at the time of writing this code:

  Tactic Notation "#[" attributes(A) "]" "tac" :=
    ltac_attributes:(A) elpi tac.

  has the following limitation:
  • #[ att ] tac. does not parse
  • (#[ att ] tac). works
  • idtac; #[ att ] tac. works

So, maybe Ltac2 tactic notations are a very different beast, for for ltac1 tactics attributes seem to work fine.

[mattam82]

@ppedrot what do you answer to @gares' proposal? It is delimited, and similar to commands. We just need to put an optional #[ ] delimited attribute list before every tactic call, basically implementing the proposed notation in the grammar.
We could even have TACTIC EXTEND allow to bind them, no? I personally don't like to put them in front, but well, too late, let's not make the syntax even more heterogeneous.

[mattam82]

More urgently, we need this for 13942 that fixes a number of annoying bugs.

[ppedrot]

@mattam82 this. does. not. make. sense.

[ppedrot]

I think we should synchronize for a visio on the topic, btw. There seems to be some fundamental misunderstandings goin on.

[mattam82]

It makes sense to me. Sadly we have a parsing conflict with commands because the parser does not change when in proof mode, otherwise I don't see the issue with having Ltac2 Notations of the shape attrs(attributes) "foo" "bar" := ... compared to "foo" attrs(attributes) "bar". With attrs being parsed using delimiters #[ attrs ] of course.

[mattam82]

@gares do you have time to discuss this this week?

[ppedrot]

I don't see the issue with having Ltac2 Notations of the shape attrs(attributes) "foo" "bar" := ...

This opt-in proposal has nothing to do with uniformly adding an attribute in front of every single notation, thereby utterly destroying the interest of the notation. We're back to square one because this was the original proposal of the PR. I'm a bit tired to repeat myself here, so I'll wait for the synchronization point before commenting further.

[mattam82]

Ok, I guess I see your point. You would prefer it if attributes stayed opt-in then? People could parse them anywhere in their notations but I guess it does not do much harm. This PR implements that, not a uniform addition over every notation. The only remaining issue is the conflict with the uniform #[attrs] Command parsing, which I think should be disallowed in proof scripts, or made available in some kind of "escaped" way.

[jfehrle]

I just saw this PR today. Some thoughts in brief:

• It's a serious mistake to make the syntax for a tactic (or tactics in general) differ at all between Ltac2 and outside of Ltac2. It tends to creates a barrier to later transitioning to Ltac2, it is confusing for users and it makes quite a mess for documentation. We should find a solution that can be used everywhere.
• Representing syntax in code as in optsyntax.v makes it quite tedious to determine what syntax is accepted. As in prohibitively tedious. That's one reason why we write grammars in mlgs and yacc files.
• I'm not a fan of the #[ ... ] or @[ ... ] syntax or making the attributes a prefix to the tactic (or command). We should try to do better, if possible.
• Our current parser is weak in two ways: First, the parser does very little lookahead without hand-coded ML routines. Second, we don't have any tooling that identifies ambiguous constructs. I believe both of these can be fixed with moderate effort. That ought to make it possible to represent attributes with a more natural, in-line syntax in most cases without the distracting punctuation , e.g. typeclasses eauto best_effort, strategy="dfs", depth="1" with typeclass_instance or a variation. It might also resolve the unparsable limitations of @gares' elpi construct.

@gares do you have time to discuss this this week?

I might join you if my participation is welcome and if the meeting can be scheduled at a reasonable time for me, say 5 PM or later Paris time. Any day of the week is fine. (I would need to know when a meeting will take place, say, 12 or more hours in advance.)

[gares]

We do have a coq call tomorrow, maybe 4:30 pm Paris time would be okish?

[ppedrot]

I won't be around tomorrow unfortunately :/

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.