Pretty-printing preliminaire des modules, commandes

Print Module qid.
Print Module Type qid.
et affichage pendant
Print All.

Tout ca est preliminare, seuls les noms des composants sont affiches et
non pas les corps...


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

13 files changed, 219 insertions, 40 deletions

diff --git a/.depend b/.depend
index 7c790d5fa..bec4285cb 100644
--- a/.depend
+++ b/.depend
@@ -109,6 +109,7 @@ parsing/printer.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
     pretyping/termops.cmi 
+parsing/printmod.cmi: kernel/names.cmi lib/pp.cmi 
 parsing/search.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi \
@@ -840,18 +841,18 @@ parsing/prettyp.cmo: pretyping/classops.cmi kernel/declarations.cmi \
     pretyping/inductiveops.cmi pretyping/instantiate.cmi library/lib.cmi \
     library/libnames.cmi library/libobject.cmi library/nameops.cmi \
     kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
-    kernel/reduction.cmi kernel/safe_typing.cmi kernel/sign.cmi \
-    pretyping/syntax_def.cmi kernel/term.cmi pretyping/termops.cmi \
-    lib/util.cmi parsing/prettyp.cmi 
+    parsing/printmod.cmi kernel/reduction.cmi kernel/safe_typing.cmi \
+    kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi parsing/prettyp.cmi 
 parsing/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \
     library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \
     library/global.cmx library/impargs.cmx kernel/inductive.cmx \
     pretyping/inductiveops.cmx pretyping/instantiate.cmx library/lib.cmx \
     library/libnames.cmx library/libobject.cmx library/nameops.cmx \
     kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
-    kernel/reduction.cmx kernel/safe_typing.cmx kernel/sign.cmx \
-    pretyping/syntax_def.cmx kernel/term.cmx pretyping/termops.cmx \
-    lib/util.cmx parsing/prettyp.cmi 
+    parsing/printmod.cmx kernel/reduction.cmx kernel/safe_typing.cmx \
+    kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \
+    pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi 
 parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     kernel/environ.cmi parsing/extend.cmi library/global.cmi \
     library/libnames.cmi library/nameops.cmi kernel/names.cmi \
@@ -864,6 +865,12 @@ parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
     parsing/ppconstr.cmx kernel/sign.cmx kernel/term.cmx parsing/termast.cmx \
     pretyping/termops.cmx lib/util.cmx parsing/printer.cmi 
+parsing/printmod.cmo: kernel/declarations.cmi kernel/environ.cmi \
+    library/global.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
+    parsing/printmod.cmi 
+parsing/printmod.cmx: kernel/declarations.cmx kernel/environ.cmx \
+    library/global.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
+    parsing/printmod.cmi 
 parsing/q_coqast.cmo: parsing/coqast.cmi parsing/genarg.cmi \
     library/libnames.cmi kernel/names.cmi parsing/pcoq.cmi parsing/q_util.cmi \
     pretyping/rawterm.cmi proofs/tacexpr.cmo 
diff --git a/Makefile b/Makefile
index 81d305af2..f07f2527b 100644
--- a/Makefile
+++ b/Makefile
@@ -109,7 +109,8 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo \
         parsing/termast.cmo parsing/astterm.cmo parsing/astmod.cmo \
 	parsing/extend.cmo parsing/esyntax.cmo \
         parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \
-	parsing/coqlib.cmo parsing/prettyp.cmo parsing/search.cmo
+	parsing/coqlib.cmo parsing/printmod.cmo parsing/prettyp.cmo \
+	parsing/search.cmo
 
 HIGHPARSING= parsing/g_prim.cmo parsing/g_basevernac.cmo \
 	parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 62fc841e6..fb342b221 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -43,8 +43,8 @@ let pptype = (fun x -> pp(prtype x))
 let prid id = pp (pr_id id)
 let prlab l = pp (pr_lab l)
 
-let prmsid msid = pp (str (string_of_msid msid))
-let prmbid mbid = pp (str (string_of_mbid mbid))
+let prmsid msid = pp (str (debug_string_of_msid msid))
+let prmbid mbid = pp (str (debug_string_of_mbid mbid))
 
 let prdir dir = pp (pr_dirpath dir)
 
diff --git a/kernel/names.ml b/kernel/names.ml
index 0209d1c33..b67fd32ad 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -71,7 +71,7 @@ let string_of_dirpath = function
 
 let u_number = ref 0 
 type uniq_ident = int * string * dir_path
-let make_uid dir s = incr u_number;(!u_number,s,dir)
+let make_uid dir s = incr u_number;(!u_number,String.copy s,dir)
 let string_of_uid (i,s,p) = 
   "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
 
@@ -83,11 +83,12 @@ module Umap = Map.Make(struct
 
 type mod_self_id = uniq_ident
 let make_msid = make_uid
-let string_of_msid = string_of_uid
+let debug_string_of_msid = string_of_uid
 
 type mod_bound_id = uniq_ident
 let make_mbid = make_uid
-let string_of_mbid = string_of_uid
+let debug_string_of_mbid = string_of_uid
+let id_of_mbid (_,s,_) = s
 
 type label = string
 let mk_label l = l
diff --git a/kernel/names.mli b/kernel/names.mli
index b1bcc0b83..d9b9ddc9c 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -48,13 +48,14 @@ type mod_self_id
 (* The first argument is a file name - to prevent conflict between 
    different files *)
 val make_msid : dir_path -> string -> mod_self_id
-val string_of_msid : mod_self_id -> string
+val debug_string_of_msid : mod_self_id -> string
 
 (*s Unique names for bound modules *)
 type mod_bound_id
 
 val make_mbid : dir_path -> string -> mod_bound_id
-val string_of_mbid : mod_bound_id -> string
+val id_of_mbid : mod_bound_id -> identifier
+val debug_string_of_mbid : mod_bound_id -> string
 
 (*s Names of structure elements *)
 type label
diff --git a/library/nametab.ml b/library/nametab.ml
index 1f8111a2c..5e1464f10 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -46,10 +46,17 @@ module Globtab = Map.Make(struct type t=extended_global_reference
 				 let compare = compare end)
 
 type globtab = section_path Globtab.t
-
 let the_globtab = ref (Globtab.empty : globtab)
 
 
+type mprewtab = dir_path MPmap.t
+let the_modrewtab = ref (MPmap.empty : mprewtab)
+
+
+type knrewtab = section_path KNmap.t
+let the_modtyperewtab = ref (KNmap.empty : knrewtab)
+
+
 let sp_of_global ctx_opt ref = 
   match (ctx_opt,ref) with
     | Some ctx, VarRef id -> 
@@ -194,7 +201,9 @@ let push_syntactic_definition visibility sp kn =
 
 let push = push_cci
 
-let push_modtype vis sp kn = push_idtree the_modtypetab vis sp (kn,sp)
+let push_modtype vis sp kn = 
+  push_idtree the_modtypetab vis sp (kn,sp);
+  the_modtyperewtab := KNmap.add kn sp !the_modtyperewtab
 
 
 (* This is for dischargeable non-cci objects (removed at the end of the
@@ -208,8 +217,11 @@ let push_object visibility sp =
 let push_tactic = push_object
 
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
-let push_dir = push_modidtree the_dirtab
-
+let push_dir vis dir dir_ref = 
+  push_modidtree the_dirtab vis dir dir_ref;
+  match dir_ref with
+      DirModule (_,(mp,_)) -> the_modrewtab := MPmap.add mp dir !the_modrewtab
+    | _ -> ()
 
 (* As before we start with generic functions *)
 
@@ -346,17 +358,30 @@ let exists_modtype sp =
 
 (* For a sp Coq.A.B.x, try to find the shortest among x, B.x, A.B.x
    and Coq.A.B.x is a qualid that denotes the same object. *)
-let shortest_qualid_of_global env ref =  
-  let sp = sp_of_global env ref in
-  let (pth,id) = repr_path sp in
+let shortest_qualid locate ref dir_path id =  
   let rec find_visible dir qdir =
     let qid = make_qualid qdir id in
     if (try locate qid = ref with Not_found -> false) then qid
     else match dir with
-      | [] -> qualid_of_sp sp
+      | [] -> make_qualid dir_path id
       | a::l -> find_visible l (add_dirpath_prefix a qdir)
   in
-  find_visible (repr_dirpath pth) (make_dirpath [])
+  find_visible (repr_dirpath dir_path) empty_dirpath
+
+let shortest_qualid_of_global env ref = 
+  let sp = sp_of_global env ref in
+  let (pth,id) = repr_path sp in
+    shortest_qualid locate ref pth id
+
+let shortest_qualid_of_module mp = 
+  let dir = MPmap.find mp !the_modrewtab in
+  let dir,id = split_dirpath dir in
+    shortest_qualid locate_module mp dir id
+
+let shortest_qualid_of_modtype kn =
+  let sp = KNmap.find kn !the_modtyperewtab in
+  let dir,id = repr_path sp in
+    shortest_qualid locate_modtype kn dir id
 
 let pr_global_env env ref =
   (* Il est important de laisser le let-in, car les streams s'évaluent
@@ -377,28 +402,35 @@ let global_inductive (loc,qid as locqid) =
 (********************************************************************)
 (* Registration of tables as a global table and rollback            *)
 
-type frozen = ccitab * dirtab * objtab * knsptab * globtab
+type frozen = ccitab * dirtab * objtab * knsptab 
+    * globtab * mprewtab * knrewtab
 
 let init () = 
   the_ccitab := Idmap.empty; 
   the_dirtab := ModIdmap.empty;
   the_objtab := Idmap.empty;
   the_modtypetab := Idmap.empty;
-  the_globtab := Globtab.empty
+  the_globtab := Globtab.empty;
+  the_modrewtab := MPmap.empty;
+  the_modtyperewtab := KNmap.empty
 
 let freeze () =
   !the_ccitab, 
   !the_dirtab,
   !the_objtab,
   !the_modtypetab,
-  !the_globtab
+  !the_globtab,
+  !the_modrewtab,
+  !the_modtyperewtab
 
-let unfreeze (mc,md,mo,mt,gt) =
+let unfreeze (mc,md,mo,mt,gt,mrt,mtrt) =
   the_ccitab := mc;
   the_dirtab := md;
   the_objtab := mo;
   the_modtypetab := mt;
-  the_globtab := gt
+  the_globtab := gt;
+  the_modrewtab := mrt;
+  the_modtyperewtab := mtrt
 
 let _ = 
   Summary.declare_summary "names"
diff --git a/library/nametab.mli b/library/nametab.mli
index 626a529e6..7456f3a4c 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -56,6 +56,9 @@ val id_of_global : Sign.named_context option -> global_reference -> identifier
 (* Printing of global references using names as short as possible *)
 val pr_global_env : Sign.named_context option -> global_reference -> std_ppcmds
 
+val shortest_qualid_of_module : module_path -> qualid
+val shortest_qualid_of_modtype : kernel_name -> qualid
+
 exception GlobalizationError of qualid
 exception GlobalizationConstantError of qualid
 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index b535f1e24..ede831944 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -79,6 +79,10 @@ GEXTEND Gram
       | IDENT "Print"; p = printable -> VernacPrint p
       | IDENT "Print"; qid = qualid -> VernacPrint (PrintName qid)
       | IDENT "Print" -> VernacPrint PrintLocalContext 
+      | IDENT "Print"; IDENT "Module"; "Type"; qid = qualid -> 
+	  VernacPrint (PrintModuleType qid)
+      | IDENT "Print"; IDENT "Module"; qid = qualid -> 
+	  VernacPrint (PrintModule qid)
       | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n)
 
       (* Searching the environment *)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 159b082f0..0808001bb 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -25,6 +25,7 @@ open Declare
 open Impargs
 open Libobject
 open Printer
+open Printmod
 open Libnames
 open Nametab
 
@@ -262,7 +263,7 @@ let print_mutual sp =
 let print_section_variable sp =
   let (d,_) = get_variable sp in
   let l = implicits_of_var sp in
-  (print_named_decl d ++ print_impl_args l ++ fnl ())
+  (print_named_decl d ++ print_impl_args l)
 
 let print_body = function
   | Some c  -> prterm c
@@ -288,34 +289,34 @@ let print_constant with_values sep sp =
 			 print_typed_body (val_0,typ) 
 		       else 
 			 (prtype typ ++ fnl ()))) ++ 
-	     print_impl_args impls ++ fnl ())
+	     print_impl_args impls)
 
-let print_inductive sp = (print_mutual sp ++ fnl ())
+let print_inductive sp = (print_mutual sp)
 
 let print_syntactic_def sep kn =
   let l = label kn in
   let c = Syntax_def.search_syntactic_definition kn in 
   (str" Syntactic Definition " ++ pr_lab l ++ str sep ++ pr_rawterm c ++ fnl ())
-
-let print_module with_values kn = 
+(*let print_module with_values kn = 
   str "Module " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl ()
 
 let print_modtype kn =
   str "Module Type " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl ()
-
+*)
 let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
   let tag = object_tag lobj in
   match (oname,tag) with
     | (_,"VARIABLE") ->
-	print_section_variable (basename sp)
+	print_section_variable (basename sp) ++ fnl ()
     | (_,("CONSTANT"|"PARAMETER")) ->
-	print_constant with_values sep kn
+	print_constant with_values sep kn ++ fnl ()
     | (_,"INDUCTIVE") ->
-	print_inductive kn
+	print_inductive kn ++ fnl ()
     | (_,"MODULE") ->
-	print_module with_values kn
+	let (mp,_,l) = repr_kn kn in 
+	  print_module with_values (MPdot (mp,l)) ++ fnl ()
     | (_,"MODULE TYPE") ->
-	print_modtype kn
+	print_modtype kn ++ fnl ()
     | (_,"AUTOHINT") -> 
 (*	(str" Hint Marker" ++ fnl ())*)
 	(mt ())
@@ -323,7 +324,7 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
 (*	(str" Grammar Marker" ++ fnl ())*)
 	(mt ())
     | (_,"SYNTAXCONSTANT") -> 
-	print_syntactic_def sep kn
+	print_syntactic_def sep kn ++ fnl ()
     | (_,"PPSYNTAX") -> 
 (*	(str" Syntax Marker" ++ fnl ())*)
 	(mt ())
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
new file mode 100644
index 000000000..075fdb03d
--- /dev/null
+++ b/parsing/printmod.ml
@@ -0,0 +1,96 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+open Pp
+open Util
+open Names
+open Declarations
+open Nameops
+open Libnames
+
+let print_modpath env mp = 
+  try (* must be with let because streams are lazy! *)
+    let qid = Nametab.shortest_qualid_of_module mp in pr_qualid qid
+  with
+    | Not_found as e -> 
+	match mp with 
+	  | MPbound mbid -> Nameops.pr_id (id_of_mbid mbid)
+	  | _ -> raise e
+
+let print_kn env kn = 
+  let qid = Nametab.shortest_qualid_of_modtype kn in 
+    pr_qualid qid
+
+let rec flatten_app mexpr l = match mexpr with
+  | MEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l)
+  | mexpr -> mexpr::l
+
+let rec print_module name env with_body mb =
+  let body = match mb.mod_equiv, with_body, mb.mod_expr with 
+    | None, false, _ 
+    | None, true, None -> mt()
+    | None, true, Some mexpr -> str " := " ++ print_modexpr env mexpr
+    | Some mp, _, _ -> str " == " ++ print_modpath env mp
+  in
+  str "Module " ++ name ++ str" : " ++ print_modtype env mb.mod_type ++ body
+
+and print_modtype env mty = match mty with
+  | MTBident kn -> print_kn env kn
+  | MTBfunsig (mbid,mtb1,mtb2) ->
+(*      let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
+      in *)
+      hov 2 (str "Funsig" ++ spc () ++ str "(" ++ 
+        pr_id (id_of_mbid mbid) ++ str " : " ++ print_modtype env mtb1 ++ 
+      str ")" ++ spc() ++ print_modtype env mtb2)
+  | MTBsig (msid,sign) -> 
+      hv 2 (str "Sig" ++ spc () ++ print_sig env msid sign ++ brk (1,-2) ++ str "End")
+
+and print_sig env msid sign = 
+  let print_spec (l,spec) = (match spec with
+    | SPBconst _ -> str "Definition "
+    | SPBmind _ -> str "Inductive "
+    | SPBmodule _ -> str "Module "
+    | SPBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
+  in
+    prlist_with_sep spc print_spec sign
+
+and print_struct env msid struc = 
+  let print_body (l,body) = (match body with
+    | SEBconst _ -> str "Definition "
+    | SEBmind _ -> str "Inductive "
+    | SEBmodule _ -> str "Module "
+    | SEBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
+  in
+    prlist_with_sep spc print_body struc
+
+and print_modexpr env mexpr = match mexpr with 
+  | MEBident mp -> print_modpath env mp
+  | MEBfunctor (mbid,mty,mexpr) ->
+(*      let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
+      in *)
+      hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ 
+	     str ":" ++ print_modtype env mty ++ 
+      str "]" ++ spc () ++ print_modexpr env mexpr)
+  | MEBstruct (msid, struc) -> 
+      hv 2 (str "Struct" ++ spc () ++ print_struct env msid struc ++ brk (1,-2) ++ str "End")
+  | MEBapply (mexpr,marg,_) -> 
+      let lapp = flatten_app mexpr [marg] in
+	hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr env) lapp ++ str")")
+
+
+
+let print_module with_body mp = 
+  let env = Global.env() in
+  let name = print_modpath env mp in
+    print_module name env with_body (Environ.lookup_module mp env) ++ fnl ()
+
+let print_modtype kn = 
+  let env = Global.env() in
+  let name = print_kn env kn in
+    str "Module Type " ++ name ++ str " = " ++
+    print_modtype env (Environ.lookup_modtype kn env) ++ fnl ()
diff --git a/parsing/printmod.mli b/parsing/printmod.mli
new file mode 100644
index 000000000..ed23fb501
--- /dev/null
+++ b/parsing/printmod.mli
@@ -0,0 +1,14 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+open Pp
+open Names
+
+val print_module : bool -> module_path -> std_ppcmds
+
+val print_modtype : kernel_name -> std_ppcmds
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8b41ba038..904db670f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -173,6 +173,21 @@ let print_modules () =
   str"Loaded and not imported modules: " ++
   pr_vertical_list pr_dirpath only_loaded
 
+
+let print_module (loc,qid) =
+  try
+    let mp = Nametab.locate_module qid in
+      msgnl (Printmod.print_module true mp)
+  with
+      Not_found -> msgnl (str"Unknown Module " ++ pr_qualid qid)
+
+let print_modtype (loc,qid) = 
+  try
+    let kn = Nametab.locate_modtype qid in
+      msgnl (Printmod.print_modtype kn)
+  with
+      Not_found -> msgnl (str"Unknown Module Type " ++ pr_qualid qid)
+
 let dump_universes s =
   let output = open_out s in
   try
@@ -792,6 +807,8 @@ let vernac_print = function
   | PrintGrammar (uni,ent) -> Metasyntax.print_grammar uni ent
   | PrintLoadPath -> (* For compatibility ? *) print_loadpath ()
   | PrintModules -> msg (print_modules ())
+  | PrintModule qid -> print_module qid
+  | PrintModuleType qid -> print_modtype qid
   | PrintMLLoadPath -> Mltop.print_ml_path ()
   | PrintMLModules -> Mltop.print_ml_modules ()
   | PrintName qid -> 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 869760411..d8d67a357 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -39,6 +39,8 @@ type printable =
   | PrintGrammar of string * string
   | PrintLoadPath
   | PrintModules
+  | PrintModule of qualid located
+  | PrintModuleType of qualid located
   | PrintMLLoadPath
   | PrintMLModules
   | PrintName of qualid located