Merge PR coq#18443: Granting wish coq#18097: Print and About see thro…

…ugh abbreviations playing the role of aliases

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

dev/ci/user-overlays/18443-herbelin-master+wish18097-print-about-see-through-aliases.sh

@@ -0,0 +1 @@
+overlay coq_lsp https://github.com/herbelin/coq-lsp  main+adapt-18443-print_abbreviation-sigma 18443 master+wish18097-print-about-see-through-aliases

interp/notation.ml

@@ -2429,11 +2429,11 @@ let browse_notation strict ntn map =
       map [] in
   List.sort (fun x y -> String.compare (snd (pi1 x)) (snd (pi1 y))) l
 
-let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c)})) =
+let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c as interp); not_location = (_, df)})) =
   match c with
-  | NRef (ref,_) when test ref -> Some (on_parsing,on_printing,ntn,sc,ref)
+  | NRef (ref,_) when test ref -> Some (on_parsing,on_printing,ntn,df,sc,interp,ref)
   | NApp (NRef (ref,_), l) when head || List.for_all isNVar_or_NHole l && test ref ->
-      Some (on_parsing,on_printing,ntn,sc,ref)
+      Some (on_parsing,on_printing,ntn,df,sc,interp,ref)
   | _ -> None
 
 type notation_as_reference_error =
@@ -2450,29 +2450,33 @@ let error_notation_not_reference ?loc ntn ntns =
   let env = Global.env () in let sigma = Evd.from_env env in
   Loc.raise ?loc (NotationAsReferenceError (NotationNotReference (env, sigma, ntn, ntns)))
 
-let interp_notation_as_global_reference ?loc ~head test ntn sc =
+let interp_notation_as_global_reference_expanded ?loc ~head test ntn sc =
   let scopes = match sc with
   | Some sc ->
       let scope = find_scope (find_delimiters_scope sc) in
       String.Map.add sc scope String.Map.empty
   | None -> !scope_map in
   let ntns = browse_notation true ntn scopes in
   let refs = List.map (global_reference_of_notation ~head test) ntns in
+  let make_scope sc = if String.equal sc default_scope then LastLonelyNotation else NotationInScope sc in
   match Option.List.flatten refs with
-  | [Some true,_ (* why not if the only one? *),_,_,ref] -> ref
+  | [Some true,_ (* why not if the only one? *),ntn,df,sc,interp,ref] -> (ntn,df,make_scope sc,interp,ref)
   | [] -> error_notation_not_reference ?loc ntn ntns
   | refs ->
-      let f (on_parsing,_,ntn,sc,ref) =
+      let f (on_parsing,_,ntn,df,sc,_,ref) =
         let def = find_default ntn !scope_stack in
         match def with
         | None -> false
         | Some sc' -> on_parsing = Some true && String.equal sc sc'
       in
       match List.filter f refs with
-      | [_,_,_,_,ref] -> ref
+      | [_,_,ntn,df,sc,interp,ref] -> (ntn,df,make_scope sc,interp,ref)
       | [] -> error_notation_not_reference ?loc ntn ntns
       | _ -> error_ambiguous_notation ?loc ntn
 
+let interp_notation_as_global_reference ?loc ~head test ntn sc =
+  let _,_,_,_,ref = interp_notation_as_global_reference_expanded ?loc ~head test ntn sc in ref
+
 let locate_notation prglob ntn scope =
   let ntns = factorize_entries (browse_notation false ntn !scope_map) in
   let scopes = Option.fold_right push_scope scope !scope_stack in
@@ -2667,7 +2671,7 @@ let toggle_abbreviations ~on found ntn_pattern =
     Abbreviation.toggle_abbreviations ~on ~use:ntn_pattern.use_pattern test
   with Exit -> ()
 
-let toggle_notations ~on ~all prglob ntn_pattern =
+let toggle_notations ~on ~all ?(verbose=true) prglob ntn_pattern =
   let found = ref [] in
   (* Deal with (parsing) notations *)
   begin
@@ -2689,7 +2693,7 @@ let toggle_notations ~on ~all prglob ntn_pattern =
   | _::_::_ when not all ->
     user_err (strbrk "More than one interpretation bound to this notation, confirm with the \"all\" modifier.")
   | _ ->
-     Feedback.msg_info
+     if verbose then Feedback.msg_info
        (str "The following notations have been " ++
           str (if on then "enabled" else "disabled") ++
           (match ntn_pattern.use_pattern with

interp/notation.mli

@@ -276,7 +276,7 @@ type 'a notation_query_pattern_gen = {
 
 type notation_query_pattern = qualid notation_query_pattern_gen
 
-val toggle_notations : on:bool -> all:bool -> (glob_constr -> Pp.t) -> notation_query_pattern -> unit
+val toggle_notations : on:bool -> all:bool -> ?verbose:bool -> (glob_constr -> Pp.t) -> notation_query_pattern -> unit
 
 (** {6 Miscellaneous} *)
 
@@ -294,6 +294,11 @@ exception NotationAsReferenceError of notation_as_reference_error
 val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool ->
       (GlobRef.t -> bool) -> notation_key -> delimiters option -> GlobRef.t
 
+(** Same together with the full notation *)
+val interp_notation_as_global_reference_expanded : ?loc:Loc.t -> head:bool ->
+      (GlobRef.t -> bool) -> notation_key -> delimiters option ->
+  (notation_entry * notation_key) * notation_key * notation_with_optional_scope * interpretation * GlobRef.t
+
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
   bool (** true=local *) -> GlobRef.t -> scope_name list list -> unit

test-suite/output/PrintInfos.out

@@ -78,6 +78,13 @@ Arguments bar {x}
 Module Coq.Init.Peano
 Notation sym_eq := eq_sym
 Expands to: Notation Coq.Init.Logic.sym_eq
+
+eq_sym : forall [A : Type] [x y : A], x = y -> y = x
+
+eq_sym is not universe polymorphic
+Arguments eq_sym [A]%type_scope [x y] _
+eq_sym is transparent
+Expands to: Constant Coq.Init.Logic.eq_sym
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x.
 
 Arguments eq {A}%type_scope x _

test-suite/output/bug_12777.out

@@ -1 +1,3 @@
 Notation tt' := tt
+
+Inductive unit : Set :=  tt : unit.

test-suite/output/wish_18097.out

@@ -0,0 +1,20 @@
+Notation pow := Nat.pow
+
+Nat.pow =
+fix pow (n m : nat) {struct m} : nat :=
+  match m with
+  | 0 => 1
+  | S m0 => n * pow n m0
+  end
+     : nat -> nat -> nat
+
+Arguments Nat.pow (n m)%nat_scope
+Notation pow := Nat.pow
+Expands to: Notation wish_18097.pow
+
+Nat.pow : nat -> nat -> nat
+
+Nat.pow is not universe polymorphic
+Arguments Nat.pow (n m)%nat_scope
+Nat.pow is transparent
+Expands to: Constant Coq.Init.Nat.pow

test-suite/output/wish_18097.v

@@ -0,0 +1,3 @@
+Notation pow := Nat.pow.
+Print pow.
+About pow.

vernac/prettyp.ml

@@ -527,8 +527,13 @@ let print_abbreviation_body env kn (vars,c) =
          Abbreviation.toggle_abbreviation ~on:false ~use:ParsingAndPrinting kn;
          pr_glob_constr_env env (Evd.from_env env) c) ())
 
-let print_abbreviation env kn =
-  print_abbreviation_body env kn (glob_constr_of_abbreviation kn)
+let print_abbreviation env sigma kn =
+  let (vars,c) = glob_constr_of_abbreviation kn in
+  let pp = match DAst.get c with
+  | GRef (gref,_udecl) -> (* TODO: don't drop universes? *) [print_global_reference env sigma gref None]
+  | _ -> [] in
+  print_abbreviation_body env kn (vars,c) ++
+  with_line_skip pp
 
 (** Unused outside? *)
 
@@ -819,7 +824,7 @@ let print_any_name env sigma na udecl =
   maybe_error_reject_univ_decl na udecl;
   match na with
   | Term gref -> print_global_reference env sigma gref udecl
-  | Abbreviation kn -> print_abbreviation env kn
+  | Abbreviation kn -> print_abbreviation env sigma kn
   | Module mp -> print_module mp
   | Dir _ -> mt ()
   | ModuleType mp -> print_modtype mp
@@ -831,13 +836,24 @@ let print_any_name env sigma na udecl =
     print_named_decl env sigma true str
   with Not_found -> user_err ?loc:qid.loc (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
+let print_notation_interpretation env sigma (entry,ntn) df sc c =
+  let filter = Notation.{
+    notation_entry_pattern = [entry];
+    interp_rule_key_pattern = Some (Inl ntn);
+    use_pattern = OnlyPrinting;
+    scope_pattern = sc;
+    interpretation_pattern = Some c;
+  } in
+  Vernacstate.System.protect (fun () ->
+      Notation.toggle_notations ~on:false ~all:false ~verbose:false (pr_glob_constr_env env sigma) filter;
+      hov 0 (str "Notation" ++ spc () ++ Notation_ops.pr_notation_info (pr_glob_constr_env env sigma) df (snd c))) ()
+
 let print_name env sigma na udecl =
   match na with
   | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
-    print_any_name env sigma
-      (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
-               ntn sc))
-      udecl
+    let ntn, df, sc, c, ref = Notation.interp_notation_as_global_reference_expanded ?loc ~head:false (fun _ -> true) ntn sc in
+    print_notation_interpretation env sigma ntn df (Some sc) c ++ fnl () ++ fnl () ++
+    print_any_name env sigma (Term ref) udecl
   | {loc; v=Constrexpr.AN ref} ->
     print_any_name env sigma (locate_any_name ref) udecl
 
@@ -896,25 +912,29 @@ let print_about_global_reference ?loc ref udecl =
     print_bidi_hints ref @
     [hov 0 (str "Expands to: " ++ pr_located_qualid (Term ref))])
 
-let print_about_abbreviation env kn =
+let print_about_abbreviation env sigma kn =
   let (vars,c) = glob_constr_of_abbreviation kn in
+  let pp = match DAst.get c with
+  | GRef (gref,_udecl) -> (* TODO: don't drop universes? *) [print_about_global_reference gref None]
+  | _ -> [] in
   print_abbreviation_body env kn (vars,c) ++ fnl () ++
-  hov 0 (str "Expands to: " ++ pr_located_qualid (Abbreviation kn))
+  hov 0 (str "Expands to: " ++ pr_located_qualid (Abbreviation kn)) ++
+  with_line_skip pp
 
 let print_about_any ?loc env sigma k udecl =
   maybe_error_reject_univ_decl k udecl;
   match k with
   | Term ref -> Dumpglob.add_glob ?loc ref; print_about_global_reference ref udecl
-  | Abbreviation kn -> v 0 (print_about_abbreviation env kn)
+  | Abbreviation kn -> v 0 (print_about_abbreviation env sigma kn)
   | Dir _ | Module _ | ModuleType _ | Undefined _ -> hov 0 (pr_located_qualid k)
   | Other (obj, info) -> hov 0 (info.about obj)
 
 let print_about env sigma na udecl =
   match na with
   | {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
-      print_about_any ?loc env sigma
-        (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
-               ntn sc)) udecl
+    let ntn, df, sc, c, ref = Notation.interp_notation_as_global_reference_expanded ?loc ~head:false (fun _ -> true) ntn sc in
+    print_notation_interpretation env sigma ntn df (Some sc) c ++ fnl () ++ fnl () ++
+    print_about_any ?loc env sigma (Term ref) udecl
   | {loc;v=Constrexpr.AN ref} ->
       print_about_any ?loc env sigma (locate_any_name ref) udecl
 

vernac/prettyp.mli

@@ -48,7 +48,7 @@ val print_notation : env -> Evd.evar_map
   -> string
   -> Pp.t
 
-val print_abbreviation : env -> KerName.t -> Pp.t
+val print_abbreviation : env -> Evd.evar_map -> KerName.t -> Pp.t
 
 val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
   UnivNames.full_name_list option -> Pp.t