Adding support for an "only parsing" modifier in "where"-based notation

[herbelin]

Kind: enhancement

To be merged synchronously with overlay for Equations (mattam82/Coq-Equations#261).

Since Reserved Notation does not support the only parsing modifier, there was no way to tell that a notation declared using a where clause is only parsing. For consistency of the picture, this PR adds this support.

While updating the refman, I fixed what seems typos but I hope I did not introduce problems in the meantime. For instance, I renamed decl_notation into decl_notations and one_decl_notation into decl_notation and I hope this is consistent with the naming policies for the reference manual (cc @jfehrle).

• Added / updated test-suite
• Corresponding documentation was added / updated
• Entry added in the changelog

[ppedrot]

Probably the right time to turn this into a record.

[herbelin]

Yes, this is what I thought too... Maybe tonight or tomorrow (or even later if not urgent)?

[herbelin]

I experimenting using a record. It is much more verbose, but certainly also more self-explanatory. Any suggestions in passing on how formatting records?

[ppedrot]

You mean, the type declaration? I subscribe to the

type foo = {
  foo_bla : Tbla;
  foo_bar : Tbar;
  ...
}

syntax, but I am not sure that's what your asking.

[herbelin]

but I am not sure that's what your asking.

Yes, that was part of my question. In practice, I used:

type decl_notation =
  { decl_ntn_string : lstring
  ; decl_ntn_interp : constr_expr
  ; decl_ntn_only_parsing : bool
  ; decl_ntn_scope : scope_name option
  }

because that's the style which was already used nearby in vernacexpr.ml (even if other part of vernacexpr.ml use the style that you're mentioning.

On the other side, in metasyntax.ml, I used the style:

    let open Vernacexpr in
    let
      { decl_ntn_string = {CAst.loc;v=ntn};
        decl_ntn_interp = c;
        decl_ntn_only_parsing = onlyparsing;
        decl_ntn_scope = scopt } = decl_ntn in

[jfehrle]

For instance, I renamed decl_notation into decl_notations and one_decl_notation into decl_notation and I hope this is consistent with the naming policies for the reference manual (cc @jfehrle).

I made the same change myself (not yet merged).

Changes made in .mlg files are easy to notice and to then make rst adjustments. In the .rsts, the productionlists will be going away entirely in favor of insertprodn/prodns in which the insertprodn automatically updates the prodn from the edited grammar. Updating the syntax in the rst directly will usually not be the preferred process. I'll explain the ins and outs of this somewhat later when it's more fully integrated into the build process.

   .. insertprodn fix_definition decl_notation

   .. prodn::
      fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @term } {? := @term } {? @decl_notations }
      decl_notations ::= where @decl_notation {* and @decl_notation }
      decl_notation ::= @string := @term1_extended {? : @ident }

which looks like this in the HTML:

[herbelin]

which looks like this in the HTML:

Nice.

Updating the syntax in the rst directly will usually not be the preferred process. I'll explain the ins and outs of this somewhat later when it's more fully integrated into the build process.

OK, so, if I understand correctly, for this PR, I do nothing special more at the moment.

[ppedrot]

The ML code is fine with me.

[herbelin]

Same fiat-crypto error as in #10832.

[Zimmi48]

This error is everywhere indeed.

[ppedrot]

@herbelin can you rebase to get a clean CI just in case?

[maximedenes]

LGTM

[ppedrot]

@herbelin The Equations overlay looks like it also needs to be rebased.

[herbelin]

@herbelin The Equations overlay looks like it also needs to be rebased.

Done.