Controlling printing notations · Coq users

Using scopes, one can control which notations are available for parsing. But it looks like this does not affect printing: if I have two different notations that are defined in different scopes and both apply, Coq will choose the last one defined rather than use scoping information to determine which one to use:

Variable (tag foo : Type).

Declare Scope tagged_scope.
Delimit Scope tagged_scope with tagged.
Declare Scope untagged_scope.
Delimit Scope untagged_scope with untagged.

Class Cl (ta : tag) := cl : foo -> Type.
Notation "[ |-[ ta ] f ]" := (cl (ta := ta) f) : tagged_scope.
Notation "[ |- f ]" := (cl f) : untagged_scope.

Section Sec.
  Context `{Cl}.
  Open Scope tagged_scope.

  (* printed as untagged *)
  Goal forall f, [ |-[ta] f].
  Abort.

End Sec.

Section Sec.
  Context `{Cl}.
  Open Scope untagged_scope.

  (* if I reorder the notations, here this will print as tagged *)
  Goal forall f, [|- f].
  Abort.
End Sec.

Is there a way to locally control over which notation gets used for printing? Ideally, I would like to avoid having to resort to importing modules, because they would force me to define all notations together, while I want to define them in a progressive manner.

Meven Lennon-Bertrand (Nov 28 2022 at 16:40):

I guess a solution would be to defined the "untagged" notation as being parse-only, and always have the tagged variant printed. This adds visual clutter that I would preferably avoid when possible, though.

Paolo Giarrusso (Nov 28 2022 at 19:28):

re "importing modules", you can encode splittable modules (and NES namespaces automates that in elpi), but the real issue is that printing notations are _sometimes_ used even when the module is _not_ imported but only required :-|

Paolo Giarrusso (Nov 28 2022 at 19:37):

Paolo Giarrusso (Nov 28 2022 at 19:40):

and closing scopes isn't meant to affect printing notations — we don't want to lose pretty-printing for 42%N just because I never Open Scope N_scope. :-|

Paolo Giarrusso (Nov 28 2022 at 19:42):

so moving the notations into modules A and B should let you use Import A. and Import B., and NES should enable splitting A and B. Let me find a link...

Paolo Giarrusso (Nov 28 2022 at 21:15):

(* name space creation *)
NES.Begin Foo.
Definition x := 3.
NES.End Foo.
Print Foo.x.

(* adding one name inside an existing name space *)
NES.Begin Foo.
Definition x2 := 4.
NES.End Foo.
Print Foo.x.
Print Foo.x2.

Enrico Tassi (Nov 28 2022 at 21:30):

NES is a POC, I don't thing "Importing a name space" works, since "A" is morally "Rundom1.A" and "Random2.A", and importing both Random1 and Random2 gives you the impression that you get the ordered union of As, but Import A will import just the last one, if I'm not mistaken. CC @Cyril Cohen

Cyril Cohen (Nov 28 2022 at 21:34):

Paolo Giarrusso (Nov 28 2022 at 21:41):

And for better or worse, NES "resolves" coq#14587: a namespace generates auxiliary modules and imports them, so notations are enabled for printing right away

Meven Lennon-Bertrand (Nov 29 2022 at 09:50):

I agree with that, but shouldn't scopes still inform the printer that it should prefer some notations over other?

Meven Lennon-Bertrand (Nov 29 2022 at 09:55):

But so for my usage, do you confirm that I either have to go with modules, or have only one set of printing notations (and the "untagged" version as parse-only if I really want that)?

Paolo Giarrusso (Nov 29 2022 at 12:45):

Not certain you have to, but I don't know another way, maybe you should tag Hugo Herbelin. We use the "module-based shadowing" quite a bit...

Meven Lennon-Bertrand (Nov 29 2022 at 12:57):

Hugo Herbelin (Dec 01 2022 at 22:19):

Trying to use the stack of scope to print notations was tried once and reverted due to incompatibilities (see https://github.com/coq/coq/pull/8187 for a long story). The criterion to prefer more defined notations first seemed to have been a compromise (https://github.com/coq/coq/pull/12986). So, for instance, if your ta could be associated to a specific constructor, then the more defined notation [ |-[ ta ] f ] using this constructor would be used by default whenever possible.

Meven Lennon-Bertrand (Dec 02 2022 at 10:31):

Thanks for the backstory! I think these Disable Notation will let me do what I am after :) I'll just have to wait for 8.18 to be out

Stream: Coq users

Topic: Controlling printing notations

Meven Lennon-Bertrand (Nov 28 2022 at 16:37):