Stream: Coq users

Topic: Printing notations with patterns


view this post on Zulip Li-yao (Apr 05 2024 at 11:28):

I have two definitions that appear identical with Set Printing All (even the variable names!). Yet they show up differently with notations enabled. Is there some internal state that the pretty-printer uses to decide what notation to use, that can't be seen with Set Printing All?

For more details, I have a notation for a monadic bind

Notation "'let+' x := u 'in' v" := (bind u (fun x => v))
  (at level 200, x pattern) : otick_scope.

which lets me bind patterns let+ (x,y) := foo in bar x y, which under the hood is desugared to bind u (fun pat => match pat with (x, y) => bar x y end).

For one definition it prints let+ (d0, d1) := unConsA d in OTick.ret (d0, d1). For the other definition it prints let+ pat := unConsA d in (let (d0, d1) := pat in OTick.ret (d0, d1)). AFAICT both desugar to the same term, so they should be printed the same.

view this post on Zulip Gaëtan Gilbert (Apr 05 2024 at 11:38):

can reproduce with

Axiom M : Type -> Type.

Axiom bind : forall {A B}, M A -> (A -> M B) -> M B.

Axiom ret : forall {A}, A -> M A.

Notation "'let+' x := u 'in' v" :=
  (bind u (fun x => v))
    (at level 200, x pattern).

Check fun d : M (nat * nat) => let+ (d0, d1) := d in ret (d0, d1).
(* fun d : M (nat * nat) => let+ (d0, d1) := d in ret (d0, d1) *)
(* fun d : M (prod nat nat) =>
@bind (prod nat nat) (prod nat nat) d
  (fun pat : prod nat nat =>
   match pat return (M (prod nat nat)) with
   | pair d0 d1 => @ret (prod nat nat) (@pair nat nat d0 d1)
   end)
*)

Check fun d : M (nat * nat) => let+ pat := d in (let (d0, d1) := pat in ret (d0, d1)).
(* fun d : M (nat * nat) => let+ pat := d in (let (d0, d1) := pat in ret (d0, d1)) *)
(* fun d : M (prod nat nat) =>
@bind (prod nat nat) (prod nat nat) d
  (fun pat : prod nat nat =>
   match pat return (M (prod nat nat)) with
   | pair d0 d1 => @ret (prod nat nat) (@pair nat nat d0 d1)
   end)
*)

first comment is default printing, second is Set Printing All

view this post on Zulip Gaëtan Gilbert (Apr 05 2024 at 11:39):

it's probably the case style as

Check fun d : M (nat * nat) => let+ pat := d in (let '(d0, d1) := pat in ret (d0, d1)).

(note the ' in the let)
prints fun d : M (nat * nat) => let+ (d0, d1) := d in ret (d0, d1)

view this post on Zulip Li-yao (Apr 05 2024 at 11:47):

Does coq remember that I used let '?

view this post on Zulip Gaëtan Gilbert (Apr 05 2024 at 11:47):

and https://github.com/coq/coq/blob/ac1414522d0cfbdbbbd99915f0ba4eea8d3898da/theories/Init/Datatypes.v#L226 makes a match on prod print as let (_,_) := by default (ie when you write a regular match)

view this post on Zulip Gaëtan Gilbert (Apr 05 2024 at 11:47):

Li-yao said:

Does coq remember that I used let '?

yes

view this post on Zulip Li-yao (Apr 05 2024 at 11:52):

Can I write my term without using notations so it gets printed like the first?

view this post on Zulip Gaëtan Gilbert (Apr 05 2024 at 11:53):

Unset Printing Notations. Print (the first one). ->

bind d (fun '(pair d0 d1) => ret (pair d0 d1))

view this post on Zulip Gaëtan Gilbert (Apr 05 2024 at 11:58):

LetPatternStyle is the only one that factorizes with lambda https://github.com/coq/coq/blob/ac1414522d0cfbdbbbd99915f0ba4eea8d3898da/interp/constrextern.ml#L1168-L1176
and I don't think there's an option to use LetPatternStyle by default so it has to be explicitly used

view this post on Zulip Li-yao (Apr 05 2024 at 12:08):

Because that was too easy, another challenge is to get that printing when my term is generated in elpi:

(* include your snippet above here *)

From elpi Require Import elpi.
Elpi Program foo lp:{{ }}.
Elpi Query lp:{{
  M = {{ fun d : M (prod nat nat) => bind d (fun '(pair d0 d1) => ret (pair d0 d1)) }},
  coq.elaborate-skeleton M _ M' _,
  coq.env.add-const {coq.env.fresh-global-id "f"} M' _ _ _.
}}.

Print f.
(* fun d : M (nat * nat) => let+ pat := d in (let (d0, d1) := pat in ret (d0, d1)) *)
(* but I want this notation: *)
Check fun d : M (prod nat nat) => bind d (fun '(pair d0 d1) => ret (pair d0 d1)).
(* fun d : M (nat * nat) => let+ (d0, d1) := d in ret (d0, d1) *)

Last updated: Jun 18 2024 at 22:01 UTC