Printmod: handle more examples thanks to better nametab use

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16329 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 29 insertions, 17 deletions

diff --git a/printing/printmod.ml b/printing/printmod.ml
index e9fc35e2f..88880c293 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -78,10 +78,8 @@ let mk_fake_top =
 
 let nametab_register_dir mp =
   let id = mk_fake_top () in
-  let fp = Libnames.make_path DirPath.empty id in
   let dir = DirPath.make [id] in
-  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty)));
-  fp
+  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty)))
 
 (** Nota: the [global_reference] we register in the nametab below
     might differ from internal ones, since we cannot recreate here
@@ -89,9 +87,10 @@ let nametab_register_dir mp =
     the user names. This works nonetheless since we search now
     [Nametab.the_globrevtab] modulo user name. *)
 
-let nametab_register_body mp fp (l,body) =
+let nametab_register_body mp dir (l,body) =
   let push id ref =
-    Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref
+    Nametab.push (Nametab.Until (1+List.length (DirPath.repr dir)))
+      (make_path dir id) ref
   in
   match body with
     | SFBmodule _ -> () (* TODO *)
@@ -107,6 +106,27 @@ let nametab_register_body mp fp (l,body) =
 	    mip.mind_consnames)
 	mib.mind_packets
 
+let nametab_register_module_body mp struc =
+  (* If [mp] is a globally visible module, we simply import it *)
+  try Declaremods.really_import_module mp
+  with Not_found ->
+    (* Otherwise we try to emulate an import by playing with nametab *)
+    nametab_register_dir mp;
+    List.iter (nametab_register_body mp DirPath.empty) struc
+
+let nametab_register_module_param mbid seb =
+  (* For algebraic seb, we use a Declaremods function that converts into mse *)
+  try Declaremods.process_module_seb_binding mbid seb
+  with e when Errors.noncritical e ->
+    (* Otherwise, for expanded structure, we try to play with the nametab *)
+    match seb with
+      | SEBstruct struc ->
+        let mp = MPbound mbid in
+        let dir = DirPath.make [MBId.to_id mbid] in
+        nametab_register_dir mp;
+        List.iter (nametab_register_body mp dir) struc
+      | _ -> ()
+
 let print_body is_impl env mp (l,body) =
   let name = str (Label.to_string l) in
   hov 2 (match body with
@@ -139,14 +159,6 @@ let print_body is_impl env mp (l,body) =
 	++ name)
 
 let print_struct is_impl env mp struc =
-  begin
-    (* If [mp] is a globally visible module, we simply import it *)
-    try Declaremods.really_import_module mp
-    with Not_found ->
-    (* Otherwise we try to emulate an import by playing with nametab *)
-      let fp = nametab_register_dir mp in
-      List.iter (nametab_register_body mp fp) struc
-  end;
   prlist_with_sep spc (print_body is_impl env mp) struc
 
 let rec flatten_app mexpr l = match mexpr with
@@ -164,8 +176,7 @@ let rec print_modtype env mp locals mty =
       let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
       let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals
       in
-      (try Declaremods.process_module_seb_binding mbid seb1
-       with e when Errors.noncritical e -> ());
+      nametab_register_module_param mbid seb1;
       hov 2 (str "Funsig" ++ spc () ++ str "(" ++
 	       pr_id (MBId.to_id mbid) ++ str ":" ++
 	       print_modtype env mp1 locals seb1 ++
@@ -173,6 +184,7 @@ let rec print_modtype env mp locals mty =
   | SEBstruct (sign) ->
       let env' = Option.map
 	(Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in
+      nametab_register_module_body mp sign;
       hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++
 	    brk (1,-2) ++ str "End")
   | SEBapply _ ->
@@ -199,14 +211,14 @@ let rec print_modexpr env mp locals mexpr = match mexpr with
 	(Modops.add_module (Modops.module_body_of_type mp' mty)) env in
       let typ = Option.default mty.typ_expr mty.typ_expr_alg in
       let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in
-      (try Declaremods.process_module_seb_binding mbid typ
-       with e when Errors.noncritical e -> ());
+      nametab_register_module_param mbid typ;
       hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(MBId.to_id mbid) ++
 	     str ":" ++ print_modtype env mp' locals typ ++
       str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
   | SEBstruct struc ->
       let env' = Option.map
 	(Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in
+      nametab_register_module_body mp struc;
       hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++
 	    brk (1,-2) ++ str "End")
   | SEBapply _ ->