An algebra of types for the argument of notations

[herbelin]

The main objective of the PR is to replace the notation arguments of possible atomic type constr, pattern, and binders by an algebra of types based on the same atoms but composable by means of lists and tuples. It is a step towards granting #7959 as well as a way to make #18531 easier (by easily supporting a new type of notation variables).

The main commit is "A richer type system for notation variables". Two structures are provided:

• Constrexpr.notation_arg_type: the type of instances of notation variables as known at parsing time (the atoms are: term, pattern, and binders, that is list of binders, as in forall binders, term or as in match term with pattern => term end)
• Notation_term.notation_var_type: the type of notation variable assigned at interpretation time
  • There are three atoms again, constr, pattern and binders, but with refinements:
    • pattern carries possible constraints of the forms:
      • only ident/name
      • strict, i.e. non ident/name pattern (those patterns written `(x,y) in binders and (x,y) in match patterns)
      • patterns without restriction
    • constr carries information on whether it becomes a pattern in notations for patterns (as in (t,u) vs match term with (x,y) => term end/fun `(x,y) => term, where there is a change of type), or remain constr (as in (t,u) : typ vs fun ((x,y) : typ) => termwheretyp` is a constr even when parsed in a pattern expression)
  • Each of atom also comes with the information of how it was orginally parsed (which may differ from how it is interpreted)

Then, a number of correspondences are implemented to adjust an instance as parsed to its expected type as interpreted:

• at definition time of the notation interpretation: by means of Metasyntax.make_interp_atom_type_rec and Metasyntax.make_interp_atom_type to inform of how parsing and interpretation types differ
• at interpretation time: by means of functions get_term, get_pattern, ... in constrintern.ml
• at printing time:
  • by means of functions extern_cases_pattern_notation_substitution and extern_notation_substitution in constrextern.ml to build parsing-level instances from interpretation-level instances
  • by means of functions is_term_meta, is_pattern_meta, ... in notation_ops.ml to take into account the possible constraints on the type (as well as to manage variables which denote both a term and a pattern, knowing that such notation variables used both as term and either pattern or binders are registered as patterns)

Another data type introduced in the PR is:

• Notation_term.notation_raw_type which reflects the (possibly nested, so as to grant Recursive notation with "pairs" as recursive pattern #7959) recursive and atomic structure of the expressiong being parsed

Note: I would not say that the invariants of the code could not be improved further and comments are welcome.

Synchronous overlays:

• Adapt to Coq PR #19404: an algebra of types for the instances of notation variables ejgallego/rocq-lsp#810
• Adapt to Coq PR #19404: an algebra of types for the instances of notation variables uds-psl/autosubst-ocaml#19
• Adapt to Coq PR #19404: an algebra of types for the instances of notation variables LPCIC/coq-elpi#673
• Adapt to Coq PR #19404: an algebra of types for the instances of notation variables QuickChick/QuickChick#386
• Adapt to Coq PR #19404: an algebra of types for the instances of notation variables coq-tactician/coq-tactician#87

[proux01]

Arg, this looks huge, I'll try to take a closer look during summer but this may take me some time.

[herbelin]

Note that if ever useful I can try to isolate the main commit from the auxiliary commits.

[proux01]

Maybe not needed, let me have a look first

[SkySkimmer]

rebased
EDIT I guess overlays need rebase too

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