Adding support for recursive blocs and associativity in ARGUMENT EXTEND

[herbelin]

Kind: feature

We add support for recursive blocs and associativity of ARGUMENT EXTEND. Example:

ARGUMENT EXTEND rewstrategy0
     RIGHT ASSOCIATIVITY
     PRINTED BY { pr_strategy }
  | [ "(" rewstrategy(h) ")" ] -> { h }
  | [ "subterms" rewstrategy0(h) ] -> { StratUnary (Subterms, h) }

WITH rewstrategy
    RIGHT ASSOCIATIVITY
    PRINTED BY { pr_strategy }
  | [ rewstrategy0(h) ";" rewstrategy(h') ] -> { StratBinary (Compose, h, h') }
  | [ rewstrategy0(h) ] -> { h }
 END

The commit on WITH needs polishing, but I prefer first to get feedback on the principle. When polish, it would be direct to extend it to VERNAC ARGUMENT EXTEND.

In practice, all ARGUMENT EXTEND are naturally with a right associativity. So fixing right associativity to be the default may be considered. In particular, I updated the grammars by necessity. Maybe some rules not covered by an effective example still need an explicit RIGHT associativity. (This is one reason defaulting to RIGHT associativity might be safer for compatibility.)

It is possible that recursive blocks helps the ssr plugin to avoid some GRAMMAR EXTEND but I prefer to let a specialist see (even if such change could also be added directly to the PR).

The change in doc_grammar.ml should be checked.

This PR is preparing the removal of an "optimization" of camlp5 which allows to support a right associativity even if not asked for.

• Updated test-suite
• Clean the WITH commit and extend it to VERNAC ARGUMENT EXTEND
• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in the changelog

[jfehrle]

I don't understand how associativity is used for nonterminals without levels, so not sure about that part.

Supporting recursive definitions in ARGUMENT EXTEND could be useful. On the other hand, it's odd that we have 2 different ways to specify productions that have different formats and feature sets. The original Camlp5 method already supports recursive productions without any additional feature such as WITH. Wouldn't it be possible to move the definition of rewstrategy into a GRAMMAR EXTEND and then have the ARGUMENT EXTEND provide only the extra semantic information?

Excluding GRAMMAR EXTEND, the EXTENDs seem fairly verbose. Each only describes a single nonterminal. Aside from the semantic info they provide, they don't have all the features of the Campl5 style productions (e.g. inline subproductions). I think we'd be better off if we moved the semantic information elsewhere--either as annotations in the Camlp5 format or in some new file, perhaps with a build-time check that all the necessary semantic info is present.

Also, BTW, IIUC attribute_list in EXTEND is always interpreted as a LIST of attribute and can't refer to the nonterminal attribute_list. And the same for induction_clause_list.

We might consider backporting some of the EXTEND production syntax to the Camlp5 format to make it less cluttered, such as not requiring IDENT everywhere, not requiring semicolons to separate tokens and putting the bind variable in parentheses. And introduce a KEYWORD metasymbol to introduce keywords.

[jfehrle]

The doc_grammar.ml change looks OK. I'd encourage you to do a make doc_gram and examine fullGrammar just to see it in action (look at the diffs)--and to perhaps familiarize yourself more with doc_grammar.

[herbelin]

@jfehrle: there are several questions in your comment.

Wouldn't it be possible to move the definition of rewstrategy into a GRAMMAR EXTEND and then have the ARGUMENT EXTEND provide only the extra semantic information?

Do you mean it as a general move of ARGUMENT EXTEND to GRAMMAR EXTEND or just for rewstrategy? If the latter, it seems to me (and @ppedrot was saying the them, afaicj) that we should stick to one way to do such extensions (which would include at the same time parsing, and interpretation).

On the other hand, it's odd that we have 2 different ways to specify productions that have different formats and feature sets

That's right. Then, it is a matter of convention of which syntax we may prefer.

If the question is why recursive entries rather than levels, it is because I found it easier (no need to invent a notation for levels). But I'd be ok to provide instead levels, we just need a notation for that.

Somehow with WITH, there is also a wink to the with of mutual inductive or recursive blocs in Gallina.

[herbelin]

[ARGUMENT EXTEND] don't have all the features of the Campl5 style productions (e.g. inline subproductions). I think we'd be better off if we moved the semantic information elsewhere--either as annotations in the Camlp5 format or in some new file, perhaps with a build-time check that all the necessary semantic info is present.

Why not, but that may be a lot of things to do.

As a bit of history, here is how tactic extensions were done before the ARGUMENT EXTEND mechanism (in Coq V6.3):

In a v file:

(* Parsing rule *)
Grammar tactic simple_tactic :=
  CompareRule 
       [ "Compare" comarg($com1) comarg($com2)] -> 
       [(Compare $com1 $com2)].

(* Printing rule *)
Syntax tactic level 0:
  ComparePP 
       [(Compare $com1 $com2)]    -> 
       ["Compare" [1 2] $com1 [1 2] $com2].

In an ml file:

(* Wrapper extracting and interpreting actual arguments from generic syntax *)
let dyn_compare args g =
      match args with 
       [(COMMAND com1);(COMMAND com2)]  -> 
          let c1 = pf_constr_of_com g com1
          and c2 = pf_constr_of_com g com2
          in  compare c1 c2 g
     | _  ->  error "Invalid arguments for dynamic tactic"

(* Bind syntax to tactic wrapper *)
add_tactic "Compare" dyn_compare

In current Coq, with ARGUMENT EXTEND, it just becomes (in the ml file):

TACTIC EXTEND compare
| [ "compare" constr(c1) constr(c2) ] -> { compare c1 c2 }
END

And if you want to override the default value for what was called pf_constr_of_com at this time, this is done in ARGUMENT EXTEND with INTERPRETED BY and GLOBALIZED BY.

[herbelin]

Also, BTW, IIUC attribute_list in EXTEND is always interpreted as a LIST of attribute and can't refer to the nonterminal attribute_list. And the same for induction_clause_list.

The attribute_list trick is not the clearest thing we can imagine. I did it like that to be closer to the the foo_list names used in the grammar entries at this time, but it is neither very orthodox nor very compatible with primitive entry name already having a similar suffix (even if the suffix is supposed to commute with the action).

We might consider backporting some of the EXTEND production syntax to the Camlp5 format to make it less cluttered, such as not requiring IDENT everywhere, not requiring semicolons to separate tokens and putting the bind variable in parentheses. And introduce a KEYWORD metasymbol to introduce keywords.

You mean in this case backporting the Camlp5 to the ARGUMENT/TACTIC EXTEND syntax? Why not also. Having a unified syntax would indeed be nice.

By the way, with camlp5 in gramlib, I wonder whether it would be worth to change Print Grammar so that it prints entries in a style closer to Notation (using e.g. at level rather than LEVEL, or constr rather than constr:operconstr). We may need first to understand better a couple of ambiguities in camlp5 before, such as the confusion between NEXT and a SELF which, with associativity, behaves like a NEXT, and so on.

[jfehrle]

Perhaps we can chat about this on a phone call as well. We could add this additional feature to ARGUMENT EXTEND. I have no objection. OTOH we have 2 ways to represent productions (GRAMMAR EXTEND and ARGUMENT EXTEND) that look a bit different and have different capabilities. The WITH is adding something that's already supported in GRAMMAR EXTEND. If we can get to a single mechanism that serves all our requirements that will be simpler for us use, think about and maintain, and this PR might not be needed. I'm not planning to make such a change anytime soon but I thought it was worth mentioning.

[herbelin]

@jfehrle: we could talk on next Thursday evening 8pm Paris time?

[jfehrle]

@herbelin To talk about possible improvements to parsing? I don't have anything new to say yet about this particular PR. For parsing improvements, it may make more sense to wait a little longer so I have specific ideas that I've vetted somewhat. But I could do 8PM Paris time in any case. On August 20th, right?

[herbelin]

To talk about possible improvements to parsing?

I meant to talk about this PR (providing recursivity vs levels, and if levels, with which syntax). But this can be a larger discussion too. Yes, on August 20th.

[herbelin]

@ppedrot: I'd like to have your opinion about this PR. Indeed, this PR is introducing new syntax, namely support for recursive grammars, which is an alternative way to using levels.

I could also support levels, e.g. with a user syntax of the following form:

ARGUMENT EXTEND rewstrategy
LEVEL 1
    RIGHT ASSOCIATIVITY
    PRINTED BY { pr_strategy1 }
  | [ rewstrategy(0)(h) ";" rewstrategy(0)(h') ] -> { StratBinary (Compose, h, h') }
  | [ rewstrategy(0)(h) ] -> { h }
LEVEL 0
     RIGHT ASSOCIATIVITY
     PRINTED BY { pr_strategy0 }
  | [ "(" rewstrategy(1)(h) ")" ] -> { h }
  | [ "subterms" rewstrategy(0)(h) ] -> { StratUnary (Subterms, h) }
 END

Q1: Do you have an opinion on providing levels vs recursion vs both of them?

Also, we talked with @jfehrle about the diversity of Coq-level user syntaxes for syntax extensions (the Tactic Notation syntax, the TACTIC/ARGUMENT/VERNAC-EXTEND syntax, the Ltac2 Notation syntax, the camlp5 syntax used by Print Grammar, ...).

Q2: Do you see a way to unify this?

For instance, I don't mind renouncing to the _list/_opt trick of Tactic Notation and of Coq's EXTEND as it is a bit confusing. Also, for Print Grammar, we now have access to the printer in gramlib, so we could adapt it to make it closer to the syntax that users see at the Coq level.

[ppedrot]

@herbelin On second thoughts I am not sure I see the interest of adding that much complexity to the ARGUMENT EXTEND macro. At first I thought that at least it'd help to generate a printer automatically, but I realized that it's not even the case because you still have to provide one in the PRINTED BY clauses.

So, essentially, my opinion on this PR depends on the following question: what is gained here compared to an explicit parsing rule performed through GRAMMAR EXTEND? The latter gives you all the expressive power of the campl5 API without having to invent a fresh, partial syntax for recursive entries. I know for a thing that SSR does it in a quite ugly way, but we could simply tweak the Tacentries API to make this easier...

[herbelin]

The question is about not having too many APIs and syntaxes to do the same thing. It is also a way to explicitly say that declaring an argument is not only a parsing rule, but also a printing rule, an interning rule, an interpretation rule, a substitution rule.

Or are you saying that we could keep the ARGUMENT EXTEND header but change the syntax for the body of ARGUMENT EXTEND to camlp5 syntax?

[ppedrot]

The question is about not having too many APIs and syntaxes to do the same thing

In that respect, this PR is making things worse then?

It is also a way to explicitly say that declaring an argument is not only [...]

There is more you can define around generic arguments, e.g. you can extend constr quotations with arbitrary stuff and the like. The set of features registered on a generic argument is open. To me, ARGUMENT EXTEND is just a helper to make the easy case easy. If you want to get non-trivial instances you better register your argument by hand, as done in SSR.

[herbelin]

The question is about not having too many APIs and syntaxes to do the same thing

In that respect, this PR is making things worse then?

Not if we consider that camlp5 is not supposed to be used by plugin developers.

It is also a way to explicitly say that declaring an argument is not only [...]

There is more you can define around generic arguments, e.g. you can extend constr quotations with arbitrary stuff and the like. The set of features registered on a generic argument is open. To me, ARGUMENT EXTEND is just a helper to make the easy case easy. If you want to get non-trivial instances you better register your argument by hand, as done in SSR.

I don't get what is your proposal. Is it to keep things as they are? ARGUMENT EXTEND for easy cases and GRAMMAR EXTEND for more complex cases?

In particular, I have a concrete question which is blocking me to continue working on notations: the rewstrategy argument works by chance and it would not work any more when I force camlp5 to respect priorities (which is needed to have a correct treatment of associativity of notations). So, one way or the other,rewstrategy has to be written in a stratified way so that correct expected priorities are statically enforced. Should I better rewrite rewstrategy using GRAMMAR EXTEND rather than extending ARGUMENT EXTEND?

[ppedrot]

Not if we consider that camlp5 is not supposed to be used by plugin developers.

In the end the Tacentries API generates tokens using the campl5 production type, so at best it's a pious lie.

I don't get what is your proposal. Is it to keep things as they are?

The current situation is not satisfactory, but I think that adding layers of complexity to reimplement the very same thing as the base API except for the use of a half-baked, quirky syntax that is constrained by some unfortunate historical design choices is not the way to go.

In particular, I have a concrete question which is blocking me to continue working on notations

I agree this is a real problem[1], but judging from the parsing rules of that argument, it's definitely leaning on the side of full-blown DSLs. It'd be indeed more robust to write it via a GRAMMAR EXTEND in ssr-style, which would solve your blocker on notations. I don't remember the details, but weren't there a handful of arguments that were having the same kind of associativity issues as well?

[1] Given the guarantees enforced by the campl5 engine and its overall implementation, I technically believe that most of the Coq syntax works by accident. In a streak of cognitive dissonance, I both dream and fear of the day we switch to a parser engine that gives you more invariants.

[herbelin]

In particular, I have a concrete question which is blocking me to continue working on notations

I agree this is a real problem[1], but judging from the parsing rules of that argument, it's definitely leaning on the side of full-blown DSLs. It'd be indeed more robust to write it via a GRAMMAR EXTEND in ssr-style, which would solve your blocker on notations.

Honestly, in term of time, it would be faster to me to have this PR merged (which is not a big deal), but I can also backtrack and study how to move rewstrategy to GRAMMAR EXTEND.

I don't remember the details, but weren't there a handful of arguments that were having the same kind of associativity issues as well?

Not that I know.

[1] Given the guarantees enforced by the campl5 engine and its overall implementation, I technically believe that most of the Coq syntax works by accident. In a streak of cognitive dissonance, I both dream and fear of the day we switch to a parser engine that gives you more invariants.

I recognize here your taste for "pedagogical exaggeration"! As far as I'm concerned, I'd be curious to know if other parser would be helpful for us (though this does not go in the direction of replacing ARGUMENT EXTEND with PARSING EXTEND). I'm otherwise also ok to progressively adapt camlp5 to our needs, as I know it better and better.

[jfehrle]

Given the guarantees enforced by the campl5 engine and its overall implementation, I technically believe that most of the Coq syntax works by accident.

"works" meaning "parses correctly", right?

In a streak of cognitive dissonance, I both dream and fear of the day we switch to a parser engine that gives you more invariants.

We should think about ways to evolve what we have; switching to another parser engine is likely to create havoc both for developers and users. I've been thinking about writing some code to analyze the grammar and (for example) identify productions that are disambiguated only by their order. We may well be able to make the parser somewhat more powerful so it's less tricky to update the grammar without breaking anything.

Not quite sure what you mean by "invariants" here.

[herbelin]

@ppedrot: unless we take the decision to renounce to ARGUMENT EXTEND, I'd be leaning to keep ARGUMENT EXTEND for rewstrategy.

[jfehrle]

Looks like the rebase picked up extra incorrect commits.

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

[herbelin]

Trying #17832 as an approach based on GRAMMAR EXTEND.