feat(print): prefix each printed object with its `locate' report

src/ecCommands.ml

@@ -393,11 +393,14 @@ let process_pr fmt scope p =
   let env = EcScope.env scope in
 
   match p with
-  | Pr_ty   qs -> EcPrinting.ObjectInfo.pr_ty   fmt env   (unloc qs)
-  | Pr_op   qs -> EcPrinting.ObjectInfo.pr_op   fmt env   (unloc qs)
-  | Pr_pr   qs -> EcPrinting.ObjectInfo.pr_op   fmt env   (unloc qs)
+  (* [~locate] prefixes each printed object with the name `locate' reports
+     for it, so that a lookup that had homonyms to choose from says which
+     one each declaration is. *)
+  | Pr_ty   qs -> EcPrinting.ObjectInfo.pr_ty   ~locate:true fmt env (unloc qs)
+  | Pr_op   qs -> EcPrinting.ObjectInfo.pr_op   ~locate:true fmt env (unloc qs)
+  | Pr_pr   qs -> EcPrinting.ObjectInfo.pr_op   ~locate:true fmt env (unloc qs)
   | Pr_th   qs -> EcPrinting.ObjectInfo.pr_th   fmt env   (unloc qs)
-  | Pr_ax   qs -> EcPrinting.ObjectInfo.pr_ax   fmt env   (unloc qs)
+  | Pr_ax   qs -> EcPrinting.ObjectInfo.pr_ax   ~locate:true fmt env (unloc qs)
   | Pr_mod  qs -> EcPrinting.ObjectInfo.pr_mod  fmt env   (unloc qs)
   | Pr_proc qs -> EcPrinting.ObjectInfo.pr_fun  fmt env   (unloc qs)
   | Pr_mty  qs -> EcPrinting.ObjectInfo.pr_mty  fmt env   (unloc qs)

src/ecCorePrinting.ml

@@ -43,6 +43,9 @@ module type PrinterAPI = sig
   val pp_list : ?on_empty:unit pp -> ('a, 'b, 'c, 'd, 'd, 'a) format6 -> 'a pp -> 'a list pp
 
   (* ------------------------------------------------------------------ *)
+  (* an operator name, with the parentheses that make it valid syntax *)
+  val pp_opqsymbol : qsymbol pp
+
   val pp_pv      : PPEnv.t -> prog_var pp
   val pp_local   : ?fv:Sid.t -> PPEnv.t -> ident pp
   val pp_opname  : PPEnv.t -> path pp
@@ -67,6 +70,16 @@ module type PrinterAPI = sig
 
   val pp_shorten_path : PPEnv.t -> (path -> qsymbol -> bool) -> path pp
 
+  (* [pp_locate_path ?pp_name ppe lookup] says where an object lives: the
+     name it is known under, plus the shortest form that [lookup] still
+     resolves to it. [pp_name] is how the category at hand spells a name --
+     [pp_opqsymbol] for an operator, the default for a type or a lemma. *)
+  val pp_locate_path :
+       ?pp_name:qsymbol pp
+    -> PPEnv.t
+    -> (qsymbol -> EcEnv.env -> (path * 'a) option)
+    -> path pp
+
   (* ------------------------------------------------------------------ *)
   val pp_codepos1      : PPEnv.t -> EcMatching.Position.codepos1 pp
   val pp_codepos_brsel : EcMatching.Position.codepos_brsel pp
@@ -131,10 +144,12 @@ module type PrinterAPI = sig
   module ObjectInfo : sig
     type db = [`Rewrite of qsymbol | `Solve of symbol]
 
-    val pr_ty  : Format.formatter -> EcEnv.env -> qsymbol -> unit
-    val pr_op  : Format.formatter -> EcEnv.env -> qsymbol -> unit
+    (* [locate:true] prefixes each printed object with the name
+       [pp_locate_path] reports for it. *)
+    val pr_ty  : ?locate:bool -> Format.formatter -> EcEnv.env -> qsymbol -> unit
+    val pr_op  : ?locate:bool -> Format.formatter -> EcEnv.env -> qsymbol -> unit
     val pr_th  : Format.formatter -> EcEnv.env -> qsymbol -> unit
-    val pr_ax  : Format.formatter -> EcEnv.env -> qsymbol -> unit
+    val pr_ax  : ?locate:bool -> Format.formatter -> EcEnv.env -> qsymbol -> unit
     val pr_mod : Format.formatter -> EcEnv.env -> qsymbol -> unit
     val pr_fun : Format.formatter -> EcEnv.env -> qsymbol -> unit
     val pr_mty : Format.formatter -> EcEnv.env -> qsymbol -> unit

src/ecPrinting.ml

@@ -506,22 +506,59 @@ let pp_path fmt p =
 let pp_xpath fmt (xp: P.xpath) =
   Format.fprintf fmt "%s" (P.x_tostring xp)
 
+(* -------------------------------------------------------------------- *)
+(* [pp_name] is how the category at hand spells a name: an operator needs
+   its parentheses back ([pp_opqsymbol]) to be valid syntax again, whereas
+   a type or a lemma is spelled as it stands. *)
+let pp_shortened
+  ?(pp_name : qsymbol pp = EcSymbols.pp_qsymbol)
+   (fmt : Format.formatter)
+  ((plong, pshort) : qsymbol * qsymbol option)
+=
+  match pshort with
+  | None ->
+    Format.fprintf fmt "%a" pp_name plong
+  | Some pshort ->
+    Format.fprintf fmt "%a (shorten name: %a)"
+    pp_name plong
+    pp_name pshort
+
 (* -------------------------------------------------------------------- *)
 let pp_shorten_path
   (ppe  : PPEnv.t)
   (cond : P.path -> qsymbol -> bool)
   (fmt  : Format.formatter)
   (p    : P.path)
 =
-  let plong, pshort = shorten_path ppe cond p in
+  pp_shortened fmt (shorten_path ppe cond p)
 
-  match pshort with
-  | None ->
-    Format.fprintf fmt "%a" EcSymbols.pp_qsymbol plong
-  | Some pshort ->
-    Format.fprintf fmt "%a (shorten name: %a)"
-    EcSymbols.pp_qsymbol plong
-    EcSymbols.pp_qsymbol pshort
+(* -------------------------------------------------------------------- *)
+(* An object is reachable under a name exactly when looking that name up
+   resolves back to it -- which is the condition [shorten_path] wants. *)
+let locate_path
+  (ppe    : PPEnv.t)
+  (lookup : qsymbol -> EcEnv.env -> (P.path * 'a) option)
+  (p      : P.path)
+  : qsymbol * qsymbol option
+=
+  let cond (p : P.path) (qs : qsymbol) =
+    match lookup qs ppe.PPEnv.ppe_env with
+    | Some (p', _) -> P.p_equal p p'
+    | None -> false
+  in shorten_path ppe cond p
+
+(* [pp_locate_path] says where an object lives: the name it is known under,
+   plus the shortest form that still resolves to it. This is the report the
+   `locate' command lists, and the one `print' prefixes each of the objects
+   it displays with. *)
+let pp_locate_path
+  ?(pp_name : qsymbol pp = EcSymbols.pp_qsymbol)
+   (ppe    : PPEnv.t)
+   (lookup : qsymbol -> EcEnv.env -> (P.path * 'a) option)
+   (fmt    : Format.formatter)
+   (p      : P.path)
+=
+  pp_shortened ~pp_name fmt (locate_path ppe lookup p)
 
 (* -------------------------------------------------------------------- *)
 let rec pp_msymbol (fmt : Format.formatter) (mx : msymbol) =
@@ -929,6 +966,10 @@ let pp_opname (fmt : Format.formatter) ((nm, op) : symbol list * symbol) =
 
   in EcSymbols.pp_qsymbol fmt (nm, op)
 
+(* [pp_opname] under a name the path-level [pp_opname] defined below does
+   not shadow. *)
+let pp_opqsymbol : qsymbol pp = pp_opname
+
 (* -------------------------------------------------------------------- *)
 let pp_opname_with_tvi
   (ppe           : PPEnv.t)
@@ -4039,6 +4080,30 @@ module ObjectInfo = struct
     od_printer : PPEnv.t -> Format.formatter -> 'a -> unit;
   }
 
+  (* ------------------------------------------------------------------ *)
+  (* With [locate], an object is prefixed by the name [locate] reports for
+     it: the one it is known under, and the shortest form that still
+     resolves to it. A name with no namespace prefix says nothing the
+     declaration does not, and is left out -- the same convention as the
+     [~long] flag of the declaration printers, which the report
+     supersedes. *)
+  let pp_located
+    ?(locate = false)
+    ?pp_name
+     (lookup : qsymbol -> EcEnv.env -> (P.path * 'a) option)
+     (pp     : PPEnv.t -> (P.path * 'a) pp)
+     (ppe    : PPEnv.t)
+     (fmt    : Format.formatter)
+    ((p, _) as obj : P.path * 'a)
+  =
+    if locate then begin
+      match locate_path ppe lookup p with
+      | (([], _), None) -> ()
+      | located ->
+          Format.fprintf fmt "(* %a *)@ " (pp_shortened ?pp_name) located
+    end;
+    pp ppe fmt obj
+
   (* -------------------------------------------------------------------- *)
   let pr_gen_r ?(prcat = false) dumper = fun fmt env qs ->
     let ppe = PPEnv.ofenv env in
@@ -4058,30 +4123,35 @@ module ObjectInfo = struct
         theprinter fmt env qs
       with NoObject ->
         Format.fprintf fmt
-          "no such object in the category [%s]@." dumper.od_name
+          "no object `%a' in the category [%s]@\n@."
+          EcSymbols.pp_qsymbol qs dumper.od_name
 
   (* ------------------------------------------------------------------ *)
-  let pr_ty_r =
+  let pr_ty_r ?locate () =
     { od_name    = "type declarations";
       od_lookup  = EcEnv.Ty.lookup;
-      od_printer = pp_typedecl; }
+      od_printer = pp_located ?locate EcEnv.Ty.lookup_opt pp_typedecl; }
 
-  let pr_ty = pr_gen pr_ty_r
+  let pr_ty ?locate fmt env qs = pr_gen (pr_ty_r ?locate ()) fmt env qs
 
   (* ------------------------------------------------------------------ *)
-  let pr_op_r =
+  let pr_op_r ?(locate = false) () =
     let get_ops qs env =
       let l = EcEnv.Op.all ~name:qs env in
       if l = [] then raise NoObject;
       l in
+    let pp_one =
+      pp_located ~locate ~pp_name:pp_opqsymbol EcEnv.Op.lookup_opt
+        (pp_opdecl ~long:(not locate)) in
     { od_name    = "operators, predicates or exceptions";
       od_lookup  = get_ops;
       od_printer =
         fun ppe fmt l ->
+          (* an annotated object spans two lines: keep the entries apart *)
           Format.fprintf fmt "@[<v>%a@]"
-            (pp_list "@ " (pp_opdecl ~long:true ppe)) l; }
+            (pp_list (if locate then "@ @ " else "@ ") (pp_one ppe)) l; }
 
-  let pr_op = pr_gen pr_op_r
+  let pr_op ?locate fmt env qs = pr_gen (pr_op_r ?locate ()) fmt env qs
 
   (* ------------------------------------------------------------------ *)
   let pr_th_r =
@@ -4092,19 +4162,23 @@ module ObjectInfo = struct
   let pr_th = pr_gen pr_th_r
 
   (* ------------------------------------------------------------------ *)
-  let pr_ax_r =
+  let pr_ax_r ?(locate = false) () =
     let get_ops qs env =
       let l = EcEnv.Ax.all ~name:qs env in
       if l = [] then raise NoObject;
       l in
+    let pp_one =
+      pp_located ~locate EcEnv.Ax.lookup_opt
+        (pp_axiom ~long:(not locate)) in
     { od_name    = "lemmas or axioms";
       od_lookup  = get_ops;
       od_printer =
         fun ppe fmt l ->
+          (* an annotated object spans two lines: keep the entries apart *)
           Format.fprintf fmt "@[<v>%a@]"
-            (pp_list "@ " (pp_axiom ~long:true ppe)) l; }
+            (pp_list (if locate then "@ @ " else "@ ") (pp_one ppe)) l; }
 
-  let pr_ax = pr_gen pr_ax_r
+  let pr_ax ?locate fmt env qs = pr_gen (pr_ax_r ?locate ()) fmt env qs
 
   (* ------------------------------------------------------------------ *)
   let pr_mod_r =
@@ -4179,10 +4253,10 @@ module ObjectInfo = struct
 
   (* ------------------------------------------------------------------ *)
   let pr_any fmt env qs =
-    let printers = [pr_gen_r ~prcat:true pr_ty_r ;
-                    pr_gen_r ~prcat:true pr_op_r ;
+    let printers = [pr_gen_r ~prcat:true (pr_ty_r ~locate:true ());
+                    pr_gen_r ~prcat:true (pr_op_r ~locate:true ());
                     pr_gen_r ~prcat:true pr_th_r ;
-                    pr_gen_r ~prcat:true pr_ax_r ;
+                    pr_gen_r ~prcat:true (pr_ax_r ~locate:true ());
                     pr_gen_r ~prcat:true pr_mod_r;
                     pr_gen_r ~prcat:true pr_fun_r;
                     pr_gen_r ~prcat:true pr_mty_r;
@@ -4195,7 +4269,8 @@ module ObjectInfo = struct
       (fun f -> try f fmt env qs with NoObject -> decr ok)
       printers;
     if !ok = 0 then
-      Format.fprintf fmt "%s@." "no such object in any category"
+      Format.fprintf fmt "no object `%a' in any category@\n@."
+        EcSymbols.pp_qsymbol qs
 end
 
 (* ------------------------------------------------------------------ *)

src/ecScope.ml

@@ -3327,46 +3327,33 @@ module Search = struct
   let locate (scope : scope) ({ pl_desc = name } : pqsymbol) =
     let ppe = EcPrinting.PPEnv.ofenv (env scope) in
 
-    let shorten lk p =
-      let lk (p : path) (qs : qsymbol) =
-        match lk qs (env scope) with
-        | Some (p', _) -> p_equal p p'
-        | _ -> false in
-      EcPrinting.shorten_path ppe lk p
-    in
-
     let buffer = Buffer.create 0 in
     let fmt    = Format.formatter_of_buffer buffer in
 
-    let for_kind section getall shorten =
+    let for_kind ?pp_name section getall lookup =
       let objs = getall ?check:None ?name:(Some name) (env scope) in
-      let objs = List.map shorten (List.fst objs) in
 
       if not (List.is_empty objs) then begin
         Format.fprintf fmt "In section [%s]@\n@\n" section;
 
-        List.iter (fun (long, short) ->
-            match short with
-            | None ->
-                Format.fprintf fmt " - %a@\n"
-                  EcSymbols.pp_qsymbol long
-            | Some short ->
-                Format.fprintf fmt " - %a (shorten name: %a)@\n"
-                  EcSymbols.pp_qsymbol long
-                  EcSymbols.pp_qsymbol short
-          )  objs
+        List.iter (fun p ->
+            Format.fprintf fmt " - %a@\n"
+              (EcPrinting.pp_locate_path ?pp_name ppe lookup) p
+          ) (List.fst objs)
       end in
 
-    for_kind "operators" EcEnv.Op.all (shorten EcEnv.Op.lookup_opt);
-    for_kind "types"     EcEnv.Ty.all (shorten EcEnv.Ty.lookup_opt);
-    for_kind "lemmas"    EcEnv.Ax.all (shorten EcEnv.Ax.lookup_opt);
+    for_kind "operators" EcEnv.Op.all EcEnv.Op.lookup_opt
+      ~pp_name:EcPrinting.pp_opqsymbol;
+    for_kind "types"     EcEnv.Ty.all EcEnv.Ty.lookup_opt;
+    for_kind "lemmas"    EcEnv.Ax.all EcEnv.Ax.lookup_opt;
 
     Format.pp_print_flush fmt ();
 
     if Buffer.length buffer = 0 then begin
       Format.fprintf fmt
         "no objects found for `%a'"
-        EcSymbols.pp_qsymbol name
+        EcSymbols.pp_qsymbol name;
+      Format.pp_print_flush fmt ()
     end;
 
     notify scope `Info "%s" (Buffer.contents buffer)

tests/clone-type-inline.ec

@@ -31,8 +31,11 @@ clone BV as L with type t =  int.   (* L.t is a plain alias        *)
 clone import Use as UK with theory P <= K.
 clone import Use as UL with theory P <= L.
 
-(* UK.P.t receives K.t's *body* (K.t is clinline): prints `int`. *)
-expect "type t = int." by print type UK.P.t.
+(* UK.P.t receives K.t's *body* (K.t is clinline): prints `int`. The
+   leading comment is the `locate' report `print' prefixes objects with. *)
+expect "(* UK.P.t *)
+type t = int." by print type UK.P.t.
 
 (* UL.P.t keeps the reference to L.t (L.t is a plain alias): prints `L.t`. *)
-expect "type t = L.t." by print type UL.P.t.
+expect "(* UL.P.t *)
+type t = L.t." by print type UL.P.t.