Remove reference name type. by maximedenes · Pull Request #7797 · rocq-prover/rocq

maximedenes · 2018-06-13T10:39:34Z

reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.

We remove the reference type and replace its uses by qualid.

This is still work in progress. We need to:

clean up a few changes we made before introducing qualid_is_ident
port plugins tracked in CI
add documentation in dev/doc/changes.md

SkySkimmer · 2018-06-13T11:32:19Z

library/libnames.mli


-type qualid
+type qualid_r
+type qualid = qualid_r CAst.t


Why do we now expose this?

We don't expose more, qualid_r is the old qualid and the new qualid was used in ad-hoc ways in many places.

herbelin

At some time, the parser was building Qualid only with non-empty path (and probably it is still the case, at least in g_prim.ml4), so in practice, even if not enforced by the OCaml syntax, I would suspect that the invariant was satisfied and that no collision even happened.

On the other side, if I remember correctly, the only real interest in differentiating between Ident in Qualid was for Constrintern (intern_applied_reference, find_pattern_variable, ...). The test qualid_is_ident is as good with this respect.

If I understand correctly, you are keeping the difference between the concept reference (in the sense of ast-level version of GlobRef.t/variable) and the technical incarnation of this concept (an uninterpreted list of identifiers). Seems good.

So, altogether, I find that this PR makes sense (with the usual reserve of the opinion of plugin developers, but that's routine!).

gares

Correct wrt ssr & ide.

If possible I'd made qualid a module and have Qualid.is_ident and Qualid.basename for example. But I was born with C, so I'm also fine with qualid_ ;-)

reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.

maximedenes · 2018-06-18T09:05:39Z

@silene you're the owner of Libnames. Do you approve this PR?

maximedenes · 2018-06-18T09:06:28Z

In fact, @gares is the secondary owner and already approved it. So the only remaining step is to provide overlays for all plugins.

gares · 2018-06-18T11:47:41Z

I've only checked ssr and ide as my review says. Which other files do you want me to check?

maximedenes · 2018-06-18T11:48:49Z

I think the idea is that the owner of Libnames should approve the principle of the change. All the rest is just propagation.

maximedenes · 2018-06-18T11:52:17Z

@ppedrot In Ltac2, I read:

(** Beware, at the raw level, [Qualid [id]] has not the same meaning as
    [Ident id]. The first is an unqualified global reference, the second is
    the dynamic reference to id. *)

which seems completely contradictory with the whole point of this PR. Can you explain a bit more?

ppedrot · 2018-06-18T11:56:45Z

@maximedenes That's just Ltac2 wrongly exploiting the difference between both representations. I need to fix that separately.

maximedenes · 2018-06-18T11:57:46Z

That's just Ltac2 wrongly exploiting the difference between both representations. I need to fix that separately.

Ok, so I will submit a first blind patch that makes it compile, and will let you fix the semantics.

ejgallego · 2018-06-18T12:07:14Z

Can't you provide a compatibility layer for plugins?

maximedenes · 2018-06-18T12:08:48Z

Can't you provide a compatibility layer for plugins?

For now, I prefer to see errors on plugins that I plan to port myself, because there is already an ocean of deprecation warnings produced by plugins we track on CI.

But once that is done, I would be happy to implement a layer. Do you have a suggestion on how to do that?

ejgallego · 2018-06-18T12:37:51Z

You can maybe make reference = qualid and then deprecate it. That won't be 100% but at least should give some warning? Dunno if that's worth it.

ejgallego · 2018-06-18T12:40:44Z

I am also not sure I am a fan of the new naming, as qualid now also stands for unqualified ids. This is confusing IMHO.

maximedenes · 2018-06-18T13:05:24Z

I am also not sure I am a fan of the new naming, as qualid now also stands for unqualified ids. This is confusing IMHO.

I think it is pretty standard that qualified identifiers allow empty prefixes, isn't it?

ejgallego · 2018-06-18T14:38:38Z

I think it is pretty standard that qualified identifiers allow empty prefixes, isn't it?

Not in Coq I think.

ppedrot · 2018-06-18T15:01:06Z

@maximedenes Ltac2 made not to observe this difference.

maximedenes · 2018-06-18T15:25:54Z

Ok, I ported all plugins. A side remark: having more uniform build systems for all those plugins wouldn't hurt.

I hope the naming issue is not blocking, as far as I'm concerned, this PR is ready modulo CI.

gares · 2018-06-19T09:27:09Z

Not in Coq I think.

Can you give an example where the syntax imposes qualification. I don't think it is the case.

Zimmi48 · 2018-06-19T11:02:34Z

I don't think it is the case.

Indeed, in the refman the notion of qualid is a superset for the notion of ident: https://coq.inria.fr/refman/language/gallina-specification-language.html#grammar-token-qualid

ejgallego · 2018-06-19T13:11:52Z

I don't think it is the case.

Oh indeed you are right, shortest_qualid_of_foo will return an empty prefix. Sorry for the noise.

gares · 2018-06-19T14:49:18Z

@maximedenes can you ping the upstreams you made an overlay, I've to leave the lab now

maximedenes · 2018-06-19T14:50:05Z

can you ping the upstreams you made an overlay, I've to leave the lab now

Sure, thanks for merging! Maybe I don't need to ping you, though ;)

herbelin · 2018-10-10T09:42:42Z

Hi, I noted a regression introduced by this PR. At the time of printing, the information of whether we have a variable or a global reference seems to be lost. This is visible for instance by the loss of color when printing a constant or inductive or constructor.

Example:

Check nat.
(* formerly: nat is displayed in light green in coqtop and navy in coqide *)
(* now: no color *)

I don't know what would be the easier to fix it. At parsing time, we are not able to make the difference, but starting with the translation constr_expr -> glob_constr we should be able to tell the difference. So, there is here an asymmetry between parsing and printing which is delicate to deal with.

maximedenes · 2018-10-10T09:45:53Z

Hi, I'd like to understand better. How was the distinction between variables and global references done previously?

herbelin · 2018-10-10T09:47:52Z

I think it was Ident id vs Qualid id in Ppconstr.pr_reference.

herbelin · 2018-10-10T19:41:20Z

@maximedenes: Maybe a cool way to fix the problem while at the same time making constr_expr more expressive is to enrich the cAst.t record. I don't know what e.g. @ejgallego has in mind, but maybe trying:

type 'a CAst.t = {
  v   : 'a;
  loc : Loc.t option;
  alt : 'a option
}

and in the case of reference, there could be a alt node carrying the full qualified path. (Then, we would have a choice to make for section variables, whether to qualify them or not.)

An alternative fix would be to add a field CVar to constr_expr which would make constr_expr a bit closer to glob_constr.

What do you think?

ejgallego · 2018-10-10T20:08:40Z

and in the case of reference, there could be a alt node carrying the full qualified path. (Then, we would have a choice to make for section variables, whether to qualify them or not.)

And what would that field mean in all other constructors of the AST?

herbelin · 2018-10-10T20:12:42Z

And what would that field mean in all other constructors of the AST?

It is an optional field, to give a possible alternative rendering (to be then propogated to Pp.t or to whatever outputting format). (I'm not saying that this is the solution, just trying to find one.)

Adapt to Coq's PR rocq-prover#7797 (removal of reference).

maximedenes added the kind: cleanup Code removal, deprecation, refactorings, etc. label Jun 13, 2018

maximedenes requested review from PierreCorbineau, SkySkimmer, amahboubi, forestjulien, gares, herbelin, letouzey, mattam82, ppedrot and silene as code owners June 13, 2018 10:39

maximedenes added needs: progress Work in progress: awaiting action from the author. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Jun 13, 2018

maximedenes force-pushed the rm-reference branch from 3bfff1d to d98c2d7 Compare June 13, 2018 11:04

maximedenes removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 13, 2018

maximedenes force-pushed the rm-reference branch from d98c2d7 to fed3bd7 Compare June 13, 2018 11:24

SkySkimmer reviewed Jun 13, 2018

View reviewed changes

herbelin reviewed Jun 13, 2018

View reviewed changes

gares approved these changes Jun 15, 2018

View reviewed changes

maximedenes force-pushed the rm-reference branch from fed3bd7 to 61c7a4b Compare June 18, 2018 09:03

Overlay for reference removal

133ac4f

maximedenes force-pushed the rm-reference branch from 4ec7f4f to 133ac4f Compare June 18, 2018 15:24

maximedenes removed the needs: progress Work in progress: awaiting action from the author. label Jun 18, 2018

gares self-assigned this Jun 19, 2018

gares added this to the 8.9+beta1 milestone Jun 19, 2018

gares merged commit 133ac4f into rocq-prover:master Jun 19, 2018

gares added a commit that referenced this pull request Jun 19, 2018

Merge PR #7797: Remove reference name type.

6715e68

maximedenes deleted the rm-reference branch October 1, 2018 07:09

ybertot pushed a commit to ybertot/coq that referenced this pull request Feb 20, 2019

Adapt to Coq's PR rocq-prover#7797 (removal of reference).

266be82

ybertot added a commit to ybertot/coq that referenced this pull request Feb 20, 2019

Merge pull request rocq-prover#48 from maximedenes/rm-reference

bcd7a59

Adapt to Coq's PR rocq-prover#7797 (removal of reference).

ejgallego mentioned this pull request Mar 27, 2019

Regression in tagging of identifiers for pretty-printed output #9843

Open

maximedenes added a commit to maximedenes/coq that referenced this pull request Apr 25, 2019

Adapt to Coq's PR rocq-prover#7797 (removal of reference).

4d8f4b1

maximedenes added a commit to maximedenes/coq that referenced this pull request May 6, 2019

Adapt to Coq's PR rocq-prover#7797 (removal of reference).

eba6d1f

Conversation

maximedenes commented Jun 13, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SkySkimmer Jun 13, 2018

Choose a reason for hiding this comment

Uh oh!

maximedenes Jun 13, 2018

Choose a reason for hiding this comment

Uh oh!

herbelin left a comment

Choose a reason for hiding this comment

Uh oh!

gares left a comment

Choose a reason for hiding this comment

Uh oh!

maximedenes commented Jun 18, 2018

Uh oh!

maximedenes commented Jun 18, 2018

Uh oh!

gares commented Jun 18, 2018

Uh oh!

maximedenes commented Jun 18, 2018 • edited by Zimmi48 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

maximedenes commented Jun 18, 2018

Uh oh!

ppedrot commented Jun 18, 2018

Uh oh!

maximedenes commented Jun 18, 2018

Uh oh!

ejgallego commented Jun 18, 2018

Uh oh!

maximedenes commented Jun 18, 2018

Uh oh!

ejgallego commented Jun 18, 2018

Uh oh!

ejgallego commented Jun 18, 2018

Uh oh!

maximedenes commented Jun 18, 2018

Uh oh!

ejgallego commented Jun 18, 2018

Uh oh!

ppedrot commented Jun 18, 2018

Uh oh!

maximedenes commented Jun 18, 2018

Uh oh!

gares commented Jun 19, 2018

Uh oh!

Zimmi48 commented Jun 19, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ejgallego commented Jun 19, 2018

Uh oh!

gares commented Jun 19, 2018

Uh oh!

maximedenes commented Jun 19, 2018

Uh oh!

herbelin commented Oct 10, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

maximedenes commented Oct 10, 2018

Uh oh!

herbelin commented Oct 10, 2018

Uh oh!

herbelin commented Oct 10, 2018

Uh oh!

ejgallego commented Oct 10, 2018

Uh oh!

herbelin commented Oct 10, 2018

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

maximedenes commented Jun 13, 2018 •

edited

Loading

maximedenes commented Jun 18, 2018 •

edited by Zimmi48

Loading

Zimmi48 commented Jun 19, 2018 •

edited

Loading

herbelin commented Oct 10, 2018 •

edited

Loading