Today abbreviations cannot be only printing. I'm wondering if this limitation can be lifted, since it would provide a quick alternative to https://github.com/coq/coq/pull/17484

CC @Hugo Herbelin

In particular reverse coercions lets on type, say, `nat`

in place of `nat_eqType`

. If we could print `nat`

in place of `nat_eqType`

we would both obtain a nicer output and keep "round tripping", e.g. copy pasting the goal would just typecheck.

Also CC @Pierre Roux

so you would do `Notation nat := nat_eqType (only printing).`

?

but then depending on imports it might print `mathcomp.whatever.nat`

which sounds confusing (and not round trip since only printing)

On the technical side abbreviations are in the nametab and the nametab doesn't understand "only printing" so you would need to add that somehow. I don't know if it would be easy or a deeper redesign.

If they are only printing, then you don't add them to the nametab, no?

Abuot import, yes, but that is fine since if you don't import a file you also don't get the canonical instances which make the elaboration of nat to nat_eqType possible

printing an abbrev involves doing `shortest_qualid_of`

in the nametab doesn't it?

Was there a reason to not just reverse the canonical projections? That is, when printing a value that is registered in the table of canonical projections, just print the target. It seems straightforward but perhaps I am missing something.

some abbreviation printing behavior

```
Module M.
Notation x := nat.
End M.
Check nat. (* nat *)
Import M.
Check nat. (* x *)
Definition x := bool.
Check nat. (* M.x *)
```

@Gaëtan Gilbert I think I see, the nametab does not have a print-only thing. Could be added, but it is not there.

@Guillaume Melquiond I think you are right, it is more ad-hoc, but also simpler.

@Guillaume Melquiond there is a caveat.

Take a record with 2 projections hence 2 values, eg `Canonical foo_canonical := {| p1 := x; p2 := y |}`

.

Sometimes p2 is not flagged as a canonical projection, so there is a 1:1 correspondence between `foo_canonical`

and `x`

.

But we have to be careful not to print `x`

if the user wrote `y`

;-)

I guess it is worth trying

Oh! I guess you meant the opposite, that is, both `p1`

and `p2`

were registered as canonical projections, so we don't know whether `x`

or `y`

should be displayed.

are they both canonical projections AND coercions?

@Gaëtan Gilbert yes.

Indeed, so this printing behavior should only be enabled if the record has exactly 1 canonical projection

Shouldn't it then be "exactly 1 coercion that happens to be a canonical projection"?

This is a lot less restrictive.

Indeed, whereas it is common to have multiple fields being canonical projections, it seems much less common for more than one to be a coercion?

Last updated: Oct 13 2024 at 01:02 UTC