Name holes in detyping

[Tragicus]

src/rocq_elpi_utils.ml/detype now turns identical evars into identical holes.
Fixes #919

[Tragicus]

@gares I am not too sure what to do about the 3rd point in your guidelines since there no evar_map. Instead, I used GNamedHole with the evar's id.

[gares]

thanks!

It seems that the detyping code is also used for the API corresponding to Notation foo := bar and there Rocq does not like ?[name] inside bar. This kind of forces you to implement the @no-holes! option, at least internally.

Also, I had a memory that the first occurrence in some traversal has to be flagged (I guess the bool argument).
But we had some surprises playing with it. Eg in f ?[x] ?x one can suppose we go left-to-right, but what about the branches of a match? We had let-ins and we got confused as well.
I'm not very familiar with the API of named holes, maybe there is a reliable way to declare these names upfront and not depend on the way the pretyper traverses the input. After all you code collects them already. Summoning @SkySkimmer who may know how this works.

[gares]

Note that detype takes a sigma. The set of evar names may be non-empty (it is in sigma) and you should start from that, or better avoid collisions. Maybe it is a set of names and not a set of evar number you have to carry.

[SkySkimmer]

I'm not very familiar with the API of named holes, maybe there is a reliable way to declare these names upfront

If you know the context & type of the evar it may be possible to declare it upfront. If you want to let them be inferred I don't think it's possible.
Why are you detyping anyway?

[gares]

Because the pretyper wants a glob, and the abbreviation API also wants a glob.

A full discussion is off topic here, I just point out that the elaborator (pretyper) should work on econstr but because of the mess in deep match elaboration it is not easy to split that part into a glob -> econstr step. I think it is possible though, and would make Typing completely redundant (would amount to pretyping with coercions off).

[SkySkimmer]

If you have a constr why do you want to call the pretyper on it?
For abbreviations you could make a genarg to include constr in glob_constr.

[gares]

If you have a constr why do you want to call the pretyper on it?

For example to insert coercions.

[SkySkimmer]

So it's an invalid constr?