Stream: Coq users

Topic: Controlling printing notations


view this post on Zulip Meven Lennon-Bertrand (Nov 28 2022 at 16:37):

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.

view this post on Zulip 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.

view this post on Zulip 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 :-|

view this post on Zulip Paolo Giarrusso (Nov 28 2022 at 19:37):

ah it's https://github.com/coq/coq/issues/14587

view this post on Zulip 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. :-|

view this post on Zulip Paolo Giarrusso (Nov 28 2022 at 19:42):

Coq will choose the last one defined rather than use scoping information to determine which one to use:

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...

view this post on Zulip Paolo Giarrusso (Nov 28 2022 at 21:15):

uh, I can't find better docs than https://github.com/LPCIC/coq-elpi/blob/v1.15.6/apps/NES/tests/test_NES.v, but that shows the key part:

(* 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.

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Nov 28 2022 at 21:34):

Import A. won't work indeed... but NES.Open A. will

view this post on Zulip 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

view this post on Zulip Meven Lennon-Bertrand (Nov 29 2022 at 09:50):

Paolo Giarrusso said:

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. :-|

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

view this post on Zulip 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)?

view this post on Zulip 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...

view this post on Zulip Meven Lennon-Bertrand (Nov 29 2022 at 12:57):

Ok, let's try and summon @Hugo Herbelin!

view this post on Zulip 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.

An alternative would be to issue commands such as:

etc., depending on the level of specificity you want to get.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Dec 03 2022 at 03:17):

oooh, those commands actually exist! Even in 8.17! https://coq.github.io/doc/v8.17/refman/coq-cmdindex.html


Last updated: Jan 31 2023 at 13:02 UTC