Stream: Coq devs & plugin devs

Topic: Syntax of projections


view this post on Zulip Hugo Herbelin (Jul 04 2021 at 15:08):

Hi, I'm currently re-experimenting introducing Proj nodes in constr_expr, as well as in glob_term (as in Maxime's #6651).

My main motivation at the current time is to replace the isproj encoding of projections in nodes App and AppExpl. Strictly speaking, we could keep this encoding, but:

In particular, I'm not making any difference at the current time between primitive and non-primitive projections since x.(p) is available for all kinds of Record, primitive or not, leaving the question of implementing different treatments for future work.

Also, since the current syntax accepts providing parameters to the projections, as in x.(p c) or x.(@p c), I need to let the Proj node in constr_expr and glob_termto potentially accept explicit parameters (even it these parameters are dropped in the primitive case when arriving at the constr level).

Note that the experience does not address the question of notations yet (as in #6764) for which PMP experimented 189528e2.

I wonder whether the invariant that any projection in constr_expr or glob_term is non-ambiguously represented with a Proj node when sufficiently applied and an App node otherwise could be maintained.

view this post on Zulip Matthieu Sozeau (Jul 05 2021 at 07:10):

Why would you need to "drop" params in the primitive case? They should just not appear, i.e. there'll be nothing to drop, no?

view this post on Zulip Matthieu Sozeau (Jul 05 2021 at 07:12):

I think getting rid of isproj is good. I also think we should take some time to sync with @Gaëtan Gilbert maybe to see how we should proceed for the "hard" part of changing/extending globrefs

view this post on Zulip Hugo Herbelin (Jul 05 2021 at 08:06):

Matthieu Sozeau said:

Why would you need to "drop" params in the primitive case? They should just not appear, i.e. there'll be nothing to drop, no?

I use the same constr_expr/glob_term nodes for "primitive" and non primitive projections, which means being able to support explicit parameters. So, even if these are replace by hole in the nodes, we need to "drop" these holes. But anyway, this is a question of terminology.

view this post on Zulip Hugo Herbelin (Jul 05 2021 at 08:08):

Matthieu Sozeau said:

I think getting rid of isproj is good. I also think we should take some time to sync with Gaëtan Gilbert maybe to see how we should proceed for the "hard" part of changing/extending globrefs

Synchronizing with who is working on it is the purpose of this message. I did nothing with about GlobRef.

view this post on Zulip Hugo Herbelin (Jul 05 2021 at 08:14):

Actually, after having started this experience (which is now a draft PR #14598), contrarily to what I said above, it seems possible to support at the same time a f p notation (an applied constant, not optimized as a constr in memory) notation and an p.(f) notation (an applied projection, optimized as a constr in memory), each with their own implicit arguments, without posing problems (the former unfolding to the latter for reduction). Sorry to be late if that was already obvious to you.

view this post on Zulip Matthieu Sozeau (Jul 05 2021 at 13:37):

What you describe sounds like the compatibility layer, having both f p and p.(f)

view this post on Zulip Matthieu Sozeau (Jul 05 2021 at 13:38):

Having these only convertible and not syntactically equal makes the whole thing difficult

view this post on Zulip Ali Caglayan (Jul 05 2021 at 13:39):

What is the reason for the p.(f) syntax? I seem to remember p.f had an issue with parsing, but I can't find the discussion on it.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 13:41):

That's the same syntax as module qualification.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 13:42):

Contrarily to OCaml, which has different syntactic classes for modules vs term variables, we don't have that in Coq so we must separate qualification syntax from projection syntax.

view this post on Zulip Ali Caglayan (Jul 05 2021 at 13:44):

Is there a good reason for not having different syntactic classes?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 13:48):

History.

view this post on Zulip Hugo Herbelin (Jul 05 2021 at 21:29):

Matthieu Sozeau said:

What you describe sounds like the compatibility layer, having both f p and p.(f)

Having these only convertible and not syntactically equal makes the whole thing difficult

I don't know. If both have a distinct and consistent representation both in the kernel and in the concrete syntax, one as a primitive field name, the other as the name of a constant, that's maybe not so worrying (but I may miss details).

view this post on Zulip Ali Caglayan (Jul 07 2021 at 13:56):

I found a related issue: https://github.com/coq/coq/issues/4167


Last updated: Oct 16 2021 at 09:07 UTC