move print_namespace to Pretty

src/core/pretty.ml

@@ -328,7 +328,7 @@ let print_inst fmt (id1,id2) =
   else if Hid.mem phash id2 then
     let n = id_unique pprinter id1 in
     fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2)
-  else 
+  else
     fprintf fmt "ident %s = %s" id1.id_long id2.id_long
 
 let print_decl fmt d = match d.d_node with
@@ -359,3 +359,25 @@ let print_named_task fmt name task =
   fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@\n@."
     name print_task task
 
+module NsTree = struct
+  type t =
+    | Namespace of string * namespace
+    | Leaf      of string
+
+  let contents ns =
+    let add_ns s ns acc = Namespace (s, ns) :: acc in
+    let add_s k s _ acc = Leaf (k ^ s) :: acc in
+    let acc = Mnm.fold add_ns           ns.ns_ns []  in
+    let acc = Mnm.fold (add_s "type ")  ns.ns_ts acc in
+    let acc = Mnm.fold (add_s "logic ") ns.ns_ls acc in
+    let acc = Mnm.fold (add_s "prop ")  ns.ns_pr acc in acc
+
+  let decomp = function
+    | Namespace (s,ns) -> s, contents ns
+    | Leaf s           -> s, []
+end
+
+let print_namespace fmt name ns =
+  let module P = Prtree.Make(NsTree) in
+  P.print fmt (NsTree.Namespace (name, ns))
+

src/core/pretty.mli

@@ -58,4 +58,5 @@ val print_task : formatter -> task -> unit
 val print_theory : formatter -> theory -> unit
 
 val print_named_task : formatter -> string -> task -> unit
+val print_namespace : formatter -> string -> namespace -> unit
 

src/main.ml

@@ -181,26 +181,7 @@ let file_sanitizer = None (* We should remove which character? *)
 (*  Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus*)
 
 let print_theory_namespace fmt th =
-  let module T = struct
-    type t = 
-      | Namespace of string * namespace
-      | Leaf of string
-    let contents ns =
-      let acc = 
-	Mnm.fold (fun s ns acc -> (Namespace (s, ns)) :: acc) ns.ns_ns [] 
-      in
-      let add prefix = Mnm.fold (fun s _ acc -> (Leaf (prefix^s)) :: acc) in
-      let acc = add "type " ns.ns_ts acc in
-      let acc = add "logic " ns.ns_ls acc in
-      let acc = add "prop "  ns.ns_pr acc in
-      acc
-    let decomp = function
-      | Namespace (s, ns) -> s, contents ns
-      | Leaf s -> s, [] 
-  end
-  in
-  let module P = Prtree.Make(T) in
-  P.print fmt (T.Namespace (th.th_name.Ident.id_short, th.th_export))
+  Pretty.print_namespace fmt th.th_name.Ident.id_short th.th_export
 
 let do_file env drv src_filename_printer dest_filename_printer file =
   let file,cin = if file = "-" 

src/util/prtree.mli

@@ -40,6 +40,6 @@ end
     single function [print: formatter -> T.t -> unit] to print a tree on a
     given formatter. *)
 
-module Make : functor (T : Tree) -> sig
+module Make (T : Tree) : sig
   val print : Format.formatter -> T.t -> unit
 end