Better printing of hint DBs

This commit introduces the following printing commands:

  - `print hint`: prints all hints in the current scope
  - `print hint simplify`:  same but only for simplify hints
  - `print hint solve`: same but only for solve hints
  - `print hint rewrite`: same but only for rewrite hints

Co-Authored-By: Gustavo Delerue <gxdelerue@proton.me>
Co-Authored-By: Pierre-Yves Strub <pierre-yves@strub.nu>

Author: Gustavo2622

src/ecCommands.ml

@@ -284,14 +284,20 @@ module HiPrinting = struct
     let hint_rewrite = EcEnv.BaseRw.all env in
 
     let ppe = EcPrinting.PPEnv.ofenv env in
-    let pp_path = EcPrinting.pp_long_short_path (fun q -> EcEnv.Ax.lookup_opt q env) in
+
+    let pp_path =
+      EcPrinting.pp_shorten_path
+        (fun (p : EcPath.path) (q : EcSymbols.qsymbol) ->
+          Option.equal EcPath.p_equal
+            (Some p)
+            (Option.map fst (EcEnv.Ax.lookup_opt q env))) in
 
     let pp_hint_rewrite _ppe fmt = (fun (p,  sp) ->
       let elems = EcPath.Sp.ntr_elements sp in
       if List.is_empty elems then
         Format.fprintf fmt "%s (empty)@." (EcPath.basename p)
       else
-        Format.fprintf fmt "@[<b 2>%s = @\n%a@]@." (EcPath.basename p) 
+        Format.fprintf fmt "@[<b 2>%s = @\n%a@]@\n" (EcPath.basename p) 
           (EcPrinting.pp_list "@\n" (fun fmt p -> 
             Format.fprintf fmt "%a" pp_path p))
           (EcPath.Sp.ntr_elements sp)
@@ -320,7 +326,7 @@ module HiPrinting = struct
         (EcPrinting.pp_list "@\n" (fun fmt rl ->
           begin match rl.rl_cond with
           | [] -> Format.fprintf fmt "Conditions: None@\n"
-          | xs -> Format.fprintf fmt "Conditions: %a@\n" (EcPrinting.pp_list "," (EcPrinting.pp_form ppe)) xs
+          | xs -> Format.fprintf fmt "Conditions: %a@\n" (EcPrinting.pp_list ",@ " (EcPrinting.pp_form ppe)) xs
           end;
           Format.fprintf fmt "Target: %a@\nPattern: %a@\n"
           (EcPrinting.pp_form ppe) rl.rl_tg

src/ecCorePrinting.ml

@@ -61,7 +61,11 @@ module type PrinterAPI = sig
   val pp_tyvar    : PPEnv.t -> ident pp
   val pp_tyunivar : PPEnv.t -> EcUid.uid pp
   val pp_path     : path pp
-  val pp_long_short_path : (qsymbol -> (EcPath.path * 'a) option) -> path pp
+  
+  (* ------------------------------------------------------------------ *)
+  val shorten_path : (path -> qsymbol -> bool) -> path -> qsymbol * qsymbol option
+
+  val pp_shorten_path : (path -> qsymbol -> bool) -> path pp
 
   (* ------------------------------------------------------------------ *)
   val pp_codepos1    : PPEnv.t -> EcMatching.Position.codepos1 pp

src/ecPrinting.ml

@@ -143,7 +143,7 @@ module PPEnv = struct
             (fun env x -> EcEnv.Mod.bind_param x mty env)
             ppe.ppe_env xs; }
 
-  let p_shorten cond p =
+  let p_shorten cond (nm, x) =
     let rec shorten prefix (nm, x) =
       match cond (nm, x) with
       | true  -> (nm, x)
@@ -154,36 +154,35 @@ module PPEnv = struct
       end
     in
 
-    let (nm, x) = P.toqsymbol p in
     shorten (List.rev nm) ([], x)
 
   let ty_symb (ppe : t) p =
       let exists sm =
       try  EcPath.p_equal (EcEnv.Ty.lookup_path ~unique:true sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten exists (P.toqsymbol p)
 
   let tc_symb (ppe : t) p =
       let exists sm =
       try  EcPath.p_equal (EcEnv.TypeClass.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten exists (P.toqsymbol p)
 
   let rw_symb (ppe : t) p =
       let exists sm =
       try  EcPath.p_equal (EcEnv.BaseRw.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten exists (P.toqsymbol p)
 
   let ax_symb (ppe : t) p =
       let exists sm =
       try  EcPath.p_equal (EcEnv.Ax.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten exists (P.toqsymbol p)
 
   let op_symb (ppe : t) p info =
     let specs = [1, EcPath.pqoname (EcPath.prefix EcCoreLib.CI_Bool.p_eq) "<>"] in
@@ -221,21 +220,21 @@ module PPEnv = struct
       (* FIXME: for special operators, do check `info` *)
       if   List.exists (fun (_, sp) -> EcPath.p_equal sp p) specs
       then ([], EcPath.basename p)
-      else p_shorten exists p
+      else p_shorten exists (P.toqsymbol p)
 
   let ax_symb (ppe : t) p =
     let exists sm =
       try  EcPath.p_equal (EcEnv.Ax.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten exists (P.toqsymbol p)
 
   let th_symb (ppe : t) p =
     let exists sm =
       try  EcPath.p_equal (EcEnv.Theory.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten exists (P.toqsymbol p)
 
   let rec mod_symb (ppe : t) mp : EcSymbols.msymbol =
     let (nm, x, p2) =
@@ -361,6 +360,18 @@ module PPEnv = struct
 end
 
 (* -------------------------------------------------------------------- *)
+let shorten_path (cond : P.path -> qsymbol -> bool) (p : P.path) : qsymbol * qsymbol option =
+  let (nm, x) = EcPath.toqsymbol p in
+  let nm =
+    match nm with
+    | top :: nm when top = EcCoreLib.i_top -> nm
+    | _ -> nm in
+  let nm', x' = PPEnv.p_shorten (cond p) (nm, x) in
+  let plong, pshort = (nm, x), (nm', x') in
+
+  (plong, if plong = pshort then None else Some pshort)
+
+(* -------------------------------------xz------------------------------- *)
 let pp_id pp fmt x = Format.fprintf fmt "%a" pp x
 
 (* -------------------------------------------------------------------- *)
@@ -434,33 +445,16 @@ let pp_path fmt p =
   Format.fprintf fmt "%s" (P.tostring p)
 
 (* -------------------------------------------------------------------- *)
-let pp_long_short_path (lk: qsymbol -> (EcPath.path * 'a) option) fmt p =
-  let rec doit prefix (nm, x) =
-    match lk (nm, x) with
-    | Some (p', _) when EcPath.p_equal p p' ->
-        (nm, x)
-    | _ -> begin
-        match prefix with
-        | [] -> (nm, x)
-        | n :: prefix -> doit prefix (n :: nm, x)
-      end
-  in
+let pp_shorten_path (cond : P.path -> qsymbol -> bool) (fmt : Format.formatter) (p : P.path) =
+  let plong, pshort  = shorten_path cond p in
 
-  let (nm, x) = EcPath.toqsymbol p in
-  let nm =
-    match nm with
-    | top :: nm when top = EcCoreLib.i_top ->
-        nm
-    | _ -> nm in
-
-  let nm', x' = doit (List.rev nm) ([], x) in
-  let plong, pshort = (nm, x), (nm', x') in
-  match plong, pshort with
-  | plong, pshort when plong = pshort -> Format.fprintf fmt "%a" EcSymbols.pp_qsymbol plong
-  | plong, pshort -> 
-      Format.fprintf fmt "%a (shorten name: %a)" 
-      EcSymbols.pp_qsymbol plong 
-      EcSymbols.pp_qsymbol pshort
+  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
 
 (* -------------------------------------------------------------------- *)
 let rec pp_msymbol (fmt : Format.formatter) (mx : msymbol) =

src/ecScope.ml

@@ -2364,28 +2364,11 @@ module Search = struct
 
   let locate (scope : scope) ({ pl_desc = name } : pqsymbol) =
     let shorten lk p =
-      let rec doit prefix (nm, x) =
-        match lk (nm, x) (env scope) with
-        | Some (p', _) when EcPath.p_equal p p' ->
-            (nm, x)
-        | _ -> begin
-            match prefix with
-            | [] -> (nm, x)
-            | n :: prefix -> doit prefix (n :: nm, x)
-          end
-      in
-
-      let (nm, x) = EcPath.toqsymbol p in
-      let nm =
-        match nm with
-        | top :: nm when top = EcCoreLib.i_top ->
-            nm
-        | _ -> nm in
-
-      let nm', x' = doit (List.rev nm) ([], x) in
-      let plong, pshort = (nm, x), (nm', x') in
-
-      (plong, if plong = pshort then None else Some pshort)
+      let lk (p : path) (qs : qsymbol) =
+        match lk qs (env scope) with
+        | Some (p', _) -> p_equal p p'
+        | _ -> false in
+      EcPrinting.shorten_path lk p
     in
 
     let buffer = Buffer.create 0 in