Print Module (Type) M now tries to print more details

 "Print Module M" prints now by default both a signature
 (fields with their types) and a body (fields with their types
 and transparent bodies).

 "Print Module Type M" could be used both when M is a module
 or a module Type, it will only display th signature of M.

 The earlier minimalist behavior (printing only the field names)
 could be reactivated by option "Set Short Module Printing".

 For the moment, the content of internal sub-modules and sub-modtypes
 are not displayed.

 Note: this commit is an experiment, many sitations are still
 unsupported. When such situations are encountered, Print Module
 will fall back on the earlier minimalist behavior. This might
 occur in particular in presence of "with" annotations, or in the
 conjonction of a non-global module (i.e. functor or module type)
 and internal sub-modules.

 Side effects of this commit:

 - a better compare function for global_reference, with no
   allocations at each comparison

 - Nametab.the_globrevtab is now searched according to user part only
   of a kernel_name

 - The printing of an inductive block is now in Printer, and rely less
   on the Nametab. Instead, we use identifiers in mind_typename and
   mind_consnames. Note that Print M.indu will not display anymore
   the pseudo-code "Inductive M.indu ..." but rather "Inductive indu..."

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

5 files changed, 71 insertions, 19 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 68d928aef..2b29868bd 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -525,6 +525,24 @@ let process_module_bindings argids args =
     in
       List.iter2 process_arg argids args
 
+(* Same with module_type_body *)
+
+let rec seb2mse = function
+  | SEBident mp -> MSEident mp
+  | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s')
+  | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp))
+  | SEBwith (s,With_definition_body(l,cb)) ->
+      (match cb.const_body with
+	| Def c -> MSEwith(seb2mse s,With_Definition(l,Declarations.force c))
+	| _ -> assert false)
+  | _ -> failwith "seb2mse: received a non-atomic seb"
+
+let process_module_seb_binding mbid seb =
+  process_module_bindings [id_of_mbid mbid]
+    [mbid,
+     (seb2mse seb,
+      { ann_inline = DefaultInline; ann_scope_subst = [] })]
+
 let intern_args interp_modtype (idl,(arg,ann)) =
   let inl = inline_annot ann in
   let lib_dir = Lib.library_dp() in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 21a7aeabe..9d44ba973 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -152,3 +152,7 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
 (** For translator *)
 val process_module_bindings : module_ident list ->
   (mod_bound_id * (module_struct_entry annotated)) list -> unit
+
+(** For Printer *)
+val process_module_seb_binding :
+  mod_bound_id -> Declarations.struct_expr_body -> unit
diff --git a/library/libnames.ml b/library/libnames.ml
index 733c45af2..c82b3476e 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -76,25 +76,37 @@ let constr_of_global = function
 let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
 
-(* outside of the kernel, names are ordered on their canonical part *)
+let global_ord_gen fc fmi x y =
+  let ind_ord (indx,ix) (indy,iy) =
+    let c = Pervasives.compare ix iy in
+    if c = 0 then kn_ord (fmi indx) (fmi indy) else c
+  in
+  match x, y with
+    | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy)
+    | IndRef indx, IndRef indy -> ind_ord indx indy
+    | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
+      let c = Pervasives.compare jx jy in
+      if c = 0 then ind_ord indx indy else c
+    | _, _ -> Pervasives.compare x y
+
+let global_ord_can = global_ord_gen canonical_con canonical_mind
+let global_ord_user = global_ord_gen user_con user_mind
+
+(* By default, [global_reference] are ordered on their canonical part *)
+
 module RefOrdered = struct
   type t = global_reference
-  let compare x y = 
-    let make_name = function
-      | ConstRef con -> 
-	  ConstRef(constant_of_kn(canonical_con con))
-      | IndRef (kn,i) ->
-	  IndRef(mind_of_kn(canonical_mind kn),i)
-      | ConstructRef ((kn,i),j )->
-	  ConstructRef((mind_of_kn(canonical_mind kn),i),j)
-      | VarRef id ->  VarRef id
-    in
-	Pervasives.compare (make_name x) (make_name y)
+  let compare = global_ord_can
 end
-  
+
+module RefOrdered_env = struct
+  type t = global_reference
+  let compare = global_ord_user
+end
+
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
-  
+
 (* Extended global references *)
 
 type syndef_name = kernel_name
@@ -103,6 +115,18 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SynDef of syndef_name
 
+(* We order [extended_global_reference] via their user part
+   (cf. pretty printer) *)
+
+module ExtRefOrdered = struct
+  type t = extended_global_reference
+  let compare x y =
+    match x, y with
+      | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry
+      | SynDef knx, SynDef kny -> kn_ord knx kny
+      | _, _ -> Pervasives.compare x y
+end
+
 (**********************************************)
 
 let pr_dirpath sl = (str (string_of_dirpath sl))
diff --git a/library/libnames.mli b/library/libnames.mli
index 1f49b6a4f..18b6ac49a 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -51,7 +51,11 @@ module RefOrdered : sig
   type t = global_reference
   val compare : global_reference -> global_reference -> int
 end
-  
+
+module RefOrdered_env : sig
+  type t = global_reference
+  val compare : global_reference -> global_reference -> int
+end
 
 module Refset : Set.S with type elt = global_reference
 module Refmap : Map.S with type key = global_reference
@@ -64,6 +68,11 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SynDef of syndef_name
 
+module ExtRefOrdered : sig
+  type t = extended_global_reference
+  val compare : t -> t -> int
+end
+
 (** {6 Dirpaths } *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
diff --git a/library/nametab.ml b/library/nametab.ml
index e43ae650c..c6f04b016 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -287,10 +287,7 @@ let the_dirtab = ref (DirTab.empty : dirtab)
 (* Reversed name tables ***************************************************)
 
 (* This table translates extended_global_references back to section paths *)
-module Globrevtab = Map.Make(struct
-			       type t=extended_global_reference
-			       let compare = compare
-			     end)
+module Globrevtab = Map.Make(ExtRefOrdered)
 
 type globrevtab = full_path Globrevtab.t
 let the_globrevtab = ref (Globrevtab.empty : globrevtab)