add printing of qualified idents

needed for `--modular` extraction

src/mlw/rust_printer.ml

@@ -124,8 +124,13 @@ type info = {
   syntax : Printer.syntax_map;
   literal : Printer.syntax_map;
   converter : Printer.syntax_map;
+  current_th : Theory.theory;
+  current_mo : Pmodule.pmodule;
   th_known_map : Decl.known_map;
   mo_known_map : Pdecl.known_map;
+  fname : string option;
+  flat : bool;
+  current_ph : string list; (* current path *)
 }
 
 module MLToRust = struct
@@ -643,12 +648,14 @@ module Print = struct
   (* TODO sanitize to snake_case, CamelCase.. *)
   (* iprinter: local names
    * aprinter: generic types
-   * lprinter: lifetime variables *)
-  let iprinter, aprinter, lprinter =
+   * lprinter: lifetime variables
+   * tprinter: toplevel definitions *)
+  let iprinter, aprinter, lprinter, tprinter =
     let isanitize = sanitizer char_to_alpha char_to_alnumus in
     let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
     create_ident_printer rust_keywords ~sanitizer:isanitize,
     create_ident_printer rust_keywords ~sanitizer:isanitize,
+    create_ident_printer rust_keywords ~sanitizer:lsanitize,
     create_ident_printer rust_keywords ~sanitizer:lsanitize
 
   let forget_id id = forget_id iprinter id
@@ -664,10 +671,51 @@ module Print = struct
     | Pat (_, p) -> forget_pat p
     | Pbox p -> forget_pat p
 
+  let print_global_ident ~sanitizer fmt id =
+    let s = id_unique ~sanitizer tprinter id in
+    Ident.forget_id tprinter id;
+    fprintf fmt "%s" s
+
+  let colon2 fmt () = fprintf fmt "::@,"
+
+  let print_path ~sanitizer fmt (q, id) =
+    assert (List.length q >= 1);
+    match Lists.chop_last q with
+    | [], _ -> print_global_ident ~sanitizer fmt id
+    | q, _  ->
+        fprintf fmt "%a::%a"
+          (print_list colon2 string) q (print_global_ident ~sanitizer) id
+
+  let rec remove_prefix acc current_path = match acc, current_path with
+    | [], _ | _, [] -> acc
+    | p1 :: _, p2 :: _ when p1 <> p2 -> acc
+    | _ :: r1, _ :: r2 -> remove_prefix r1 r2
+
+  let is_local_id info id =
+    Sid.mem id info.current_th.th_local ||
+    Sid.mem id info.current_mo.Pmodule.mod_local
+
+  exception Local
+
   let print_qident ~sanitizer (info:info) fmt id =
-    (* TODO: support modules *)
+    try
+      if info.flat then raise Not_found;
+      if is_local_id info id then raise Local;
+      let p, t, q =
+        try Pmodule.restore_path id with Not_found -> Theory.restore_path id in
+      let fname = if p = [] then info.fname else None in
+      let m = Compile.module_name ?fname p t in
+      fprintf fmt "super::%s::%a" m (print_path ~sanitizer) (q, id)
+    with
+    | Not_found ->
         let s = id_unique ~sanitizer iprinter id in
         fprintf fmt "%s" s
+    | Local ->
+        let _, _, q =
+          try Pmodule.restore_path id with Not_found ->
+            Theory.restore_path id in
+        let q = remove_prefix q (List.rev info.current_ph) in
+        print_path ~sanitizer fmt (q, id)
 
   let print_lident = print_qident ~sanitizer:String.uncapitalize_ascii
   let print_uident = print_qident ~sanitizer:String.capitalize_ascii
@@ -874,32 +922,22 @@ module Print = struct
     (MLToRust.translate_decl info d)
 end
 
-(*
-  (* used to deal with recursive functions *)
-  let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)
-
-  | Eapp (rs, []) when rs_equal rs rs_true -> fprintf fmt "true"
-  | Eapp (rs, []) when rs_equal rs rs_false -> fprintf fmt "false"
-  | Eapp (rs, pvl) ->
-      begin match query_syntax info.converter rs.rs_name, pvl with
-      | Some s, [{e_node = Econst _}] ->
-          syntax_arguments s print_constant fmt pvl
-      | _ ->
-          fprintf fmt (protect_on false "%a")
-            (print_apply info (Hrs.find_def ht_rs rs rs)) pvl end
-*)
-
 let print_decl =
   (* avoid printing the same decl multiple times *)
   let memo = Hashtbl.create 16 in
   fun pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d ->
-    ignore old; ignore fname; ignore flat;
+    ignore old;
     let info = {
       syntax = pargs.Pdriver.syntax;
       literal = pargs.Pdriver.literal;
       converter = pargs.Pdriver.converter;
+      current_th = th;
+      current_mo = m;
       th_known_map = th.Theory.th_known;
       mo_known_map = m.mod_known;
+      fname = Opt.map Compile.clean_name fname;
+      flat = flat;
+      current_ph = [];
     } in
     if not (Hashtbl.mem memo d) then begin Hashtbl.add memo d ();
       Print.print_decl info fmt d;