Adapting to Coq PR #14598: adding explicit constr_expr/glob_constr node for projections

[herbelin]

This PR adds code for the new node GProj. So that the examples involving the syntax t.(f) continue to work, I did not try to do better than simulating what was done when t.(f) was encoded with a GApp node, leading to reuse in_elpi_appl rather than, say, adding a new in_elpi_proj method.

Also adapting to lighter syntax of CAppExpl and CApp.

This has to be merged synchrounously with coq/coq#14598.

[gares]

Just to be sure: is this node just about the projection syntax? (because I now have a way to represent primitive projections)

[herbelin]

As of coq/coq#14598, GProj strictly corresponds to the t.(f args) syntax. However, it is not clear to me what will then be the consensus about the role to give to the GProj, whether it matches CProj (i.e. the t.(f args) syntax) or the Proj kernel syntax (i.e. the "primitive" projections), or if t.(f args) and kernel-primitive get eventually identified.

[herbelin]

For instance, in coq/coq#14598, pretyping map GProj to Proj when the projection is registered as primitive and to App if not.

[herbelin]

So, I don't know what it implies for elpi. I guess it depends if the elpi way to represent primitive projections is about kernel Proj or about t.(f args).

[gares]

For instance, in coq/coq#14598, pretyping map GProj to Proj when the projection is registered as primitive and to App if not.

ok, then I'll try to push a commit on top of yours

[herbelin]

ok

[gares]

Sorry, I need #256 to go in first, then I'll rebase this one and add a few lines to it

[gares]

rebased, but I don't have the time to write down the code contracting a primitive projection today. I'll do it next week

[gares]

done. I made:

• x.(p) -> primitive (is p is a prim proj)
• p x -> regular projection even if p is the compat constant
• x.(@p params) -> regular

I'm not 100% sure about the last one, but tossing away something the user wrote seems wrong.

[herbelin]

I'm not 100% sure about the last one, but tossing away something the user wrote seems wrong.

I'm not sure either. For instance, as of now, it is not forbidden to explicitly give the parameters of primitive projections.

Set Primitive Projections.
Record T A := {a:A}.
Check fun x => x.(a nat).
(* fun x : T nat => a _ x *)

[gares]

That, in the code I wrote, would result into its compat constant(in elpi). The idea is: if you pass the params, the you are not talking about the primitive one. I don't know yet if this is a good rule.

[ppedrot]

Please merge.