pretty-printing: rework the pretty-printing of module restrictions

The output can now be reparsed

Author: strub

src/ecPrinting.ml

@@ -388,6 +388,26 @@ let rec pp_list sep pp fmt xs =
     | [x]     -> Format.fprintf fmt "%a" pp x
     | x :: xs -> Format.fprintf fmt "%a%(%)%a" pp x sep pp_list xs
 
+(* -------------------------------------------------------------------- *)
+type pphlist =
+  PpHList : (Format.formatter -> 'a -> unit) * 'a list -> pphlist
+
+(* -------------------------------------------------------------------- *)
+type pphlist1 =
+  PpHList1 : (Format.formatter -> 'a -> unit) * 'a -> pphlist1
+
+(* -------------------------------------------------------------------- *)
+let pp_hlist (sep : _ format6) (fmt : Format.formatter) (xs : pphlist list) =
+  let xs =
+    xs
+    |> List.map (fun (PpHList (f, xs)) -> List.map (fun x -> PpHList1 (f, x)) xs)
+    |> List.flatten
+  in
+
+  let pp fmt (PpHList1 (f, x)) = f fmt x in
+
+  Format.fprintf fmt "%a" (pp_list sep pp) xs
+
 (* -------------------------------------------------------------------- *)
 let pp_option pp fmt x =
   match x with None -> () | Some x -> pp fmt x
@@ -519,8 +539,6 @@ let get_f_projarg ppe e i ty =
   | _ -> raise NoProjArg
 
 (* -------------------------------------------------------------------- *)
-let all_mem_sym = "+all mem"
-
 let pp_restr_s fmt = function
   | true -> Format.fprintf fmt "+"
   | false -> Format.fprintf fmt "-"
@@ -1895,42 +1913,31 @@ and pp_orclinfos ppe fmt ois =
 (* -------------------------------------------------------------------- *)
 and pp_mem_restr ppe fmt mr =
   let pp_rx sign fmt rx =
-    let pp_x fmt x =
-      Format.fprintf fmt "%a%a" pp_restr_s sign (pp_pv ppe) (pv_glob x) in
-    pp_list ",@ " pp_x fmt (EcPath.Sx.elements rx) in
+    Format.fprintf fmt "%a%a" pp_restr_s sign (pp_pv ppe) (pv_glob rx) in
+
   let pp_r sign fmt r =
-    let pp_m fmt m =
-      Format.fprintf fmt "%a%a" pp_restr_s sign (pp_topmod ppe) m in
-    pp_list ",@ " pp_m fmt (EcPath.Sm.elements r) in
-  let pp_top fmt b =
-    if b then Format.fprintf fmt "%s" all_mem_sym else () in
-
-  let xpos_emp =
-    EcPath.Sx.is_empty (odfl EcPath.Sx.empty (mr_xpaths mr).ur_pos) in
-  let mpos_emp =
-    EcPath.Sm.is_empty (odfl EcPath.Sm.empty (mr_mpaths mr).ur_pos) in
-  let all_mem = mr.ur_pos = None in
-
-  let printed = ref (all_mem) in
-  let pp_sep fmt b =
-    let b' = (not b) && !printed in
-    printed := !printed || not b;
-    if b' then Format.fprintf fmt ",@ " else () in
-
-  if all_mem &&
+    Format.fprintf fmt "%a%a" pp_restr_s sign (pp_topmod ppe) r in
+
+  let all_mem = Option.is_none mr.ur_pos in
+
+  if not (all_mem &&
      EcPath.Sm.is_empty (mr_mpaths mr).ur_neg &&
-     EcPath.Sx.is_empty (mr_xpaths mr).ur_neg
-  then ()
-  else Format.fprintf fmt "@[<h>{%a%a%a%a%a%a%a%a%a}@]@ "
-      pp_top (all_mem)
-      pp_sep xpos_emp
-      (pp_rx true) (odfl EcPath.Sx.empty (mr_xpaths mr).ur_pos)
-      pp_sep mpos_emp
-      (pp_r true) (odfl EcPath.Sm.empty (mr_mpaths mr).ur_pos)
-      pp_sep (EcPath.Sx.is_empty (mr_xpaths mr).ur_neg)
-      (pp_rx false) (mr_xpaths mr).ur_neg
-      pp_sep (EcPath.Sm.is_empty (mr_mpaths mr).ur_neg)
-      (pp_r false) (mr_mpaths mr).ur_neg
+     EcPath.Sx.is_empty (mr_xpaths mr).ur_neg)
+  then begin
+    let urx_pos = (mr_xpaths mr).ur_pos |> omap P.Sx.elements |> odfl [] in
+    let urm_pos = (mr_mpaths mr).ur_pos |> omap P.Sm.elements |> odfl [] in
+    let urx_neg = (mr_xpaths mr).ur_neg |> P.Sx.elements in
+    let urm_neg = (mr_mpaths mr).ur_neg |> P.Sm.elements in
+
+    let toprint = [
+      PpHList (pp_rx true , urx_pos);
+      PpHList (pp_r  true , urm_pos);
+      PpHList (pp_rx false, urx_neg);
+      PpHList (pp_r  false, urm_neg);
+    ] in
+
+    Format.fprintf fmt "@[<h>{%a}@]" (pp_hlist ",@ ") toprint
+  end
 
 (* -------------------------------------------------------------------- *)
 (* Use in an hv box. *)