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_term
to 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.
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 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
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.
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
.
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.
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
Matthieu Sozeau said:
What you describe sounds like the compatibility layer, having both
f p
andp.(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).
I found a related issue: https://github.com/coq/coq/issues/4167
Last updated: Oct 13 2024 at 01:02 UTC