Ajout Print Implicit avec depliage du type

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

7 files changed, 38 insertions, 23 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6b4b82e399..5e0bc4d9f9 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1474,7 +1474,8 @@ let xlate_vernac =
         | PrintScopes -> xlate_error "TODO: Print Scopes"
         | PrintScope _ -> xlate_error "TODO: Print Scope"
 	| PrintVisibility _ -> xlate_error "TODO: Print Visibility"
-        | PrintAbout _ -> xlate_error "TODO: Print About")
+        | PrintAbout _ -> xlate_error "TODO: Print About"
+	| _ -> xlate_error "TODO: Print")
   | VernacBeginSection id ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment id -> CT_section_end (xlate_ident id)
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 27675758f9..da16be9b5f 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -194,7 +194,8 @@ GEXTEND Gram
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
-      | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s ] ]
+      | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
+      | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]
   ;
   locatable:
     [ [ qid = global -> LocateTerm qid
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index ff6411a402..8c1ff3211e 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -76,7 +76,10 @@ let print_argument_scopes = function
 let print_name_infos ref =
   let impl = implicits_of_global ref in
   let scopes = Symbols.find_arguments_scope ref in
-  (if impl<>[] or not (List.for_all ((=) None) scopes) then fnl() else mt())
+  (if (List.filter is_status_implicit impl<>[])
+      or not (List.for_all ((=) None) scopes) 
+  then fnl()
+  else mt())
   ++ print_impl_args impl ++ print_argument_scopes scopes
 
 let print_id_args_data test pr id l =
@@ -295,8 +298,10 @@ let print_constant with_values sep sp =
     | _ -> 
 	print_basename sp ++ str sep ++ cut () ++
 	(if with_values then print_typed_body (val_0,typ) else prtype typ) ++
-	fnl ()) ++ 
-  print_name_infos (ConstRef sp)
+	fnl ())
+
+let print_constant_with_infos sp =
+  print_constant true " = " sp ++ print_name_infos (ConstRef sp)
 
 let print_inductive sp = (print_mutual sp)
 
@@ -410,7 +415,7 @@ let print_eval red_fun env {uj_val=trm;uj_type=typ} =
 
 let print_name ref = 
   match locate_any_name ref with
-  | Term (ConstRef sp) -> print_constant true " = " sp
+  | Term (ConstRef sp) -> print_constant_with_infos sp
   | Term (IndRef (sp,_)) -> print_inductive sp
   | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
   | Term (VarRef sp) -> print_section_variable sp
@@ -450,7 +455,7 @@ let print_opaque_name qid =
     | ConstRef cst ->
 	let cb = Global.lookup_constant cst in
         if cb.const_body <> None then
-	  print_constant true " = " cst
+	  print_constant_with_infos cst
         else 
 	  error "not a defined constant"
     | IndRef (sp,_) ->
@@ -462,30 +467,34 @@ let print_opaque_name qid =
         let (_,c,ty) = lookup_named id env in 
 	print_named_decl (id,c,ty)
 
+let print_ref reduce ref =
+  let typ = Global.type_of_global ref in
+  let typ = 
+    if reduce then
+      let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
+      in it_mkProd_or_LetIn ccl ctx 
+    else typ in
+  hov 0 (pr_global ref ++ str " :" ++ spc () ++ prtype typ) ++ fnl ()
+
 let print_about ref = 
   let sigma = Evd.empty in
-  let env = Global.env () in
   let k = locate_any_name ref in
   begin match k with
-  | Term (ConstRef sp as ref) -> 
-      print_constant false " : " sp
-  | Term (IndRef ind as ref) ->
-      let ty = Inductive.type_of_inductive env ind in
-      print_typed_value (mkInd ind, ty) ++ 
-      print_name_infos ref
-  | Term (ConstructRef cstr as ref) ->
-      let ty = Inductive.type_of_constructor env cstr in
-      print_typed_value (mkConstruct cstr, ty) ++ 
-      print_name_infos ref
-  | Term (VarRef sp as ref) ->
-      print_named_decl (get_variable sp) ++ 
-      print_name_infos ref
-  | Syntactic kn ->
-      print_syntactic_def " = " kn
+  | Term ref -> print_ref false ref ++ print_name_infos ref
+  | Syntactic kn -> print_syntactic_def " = " kn
   | Dir _ | ModuleType _ | Undefined _ -> mt () end
   ++
   hov 0 (str "Expands to: " ++ pr_located_qualid k)
 
+let print_impargs ref =
+  let ref = Nametab.global ref in
+  let impl = implicits_of_global ref in
+  let has_impl = List.filter is_status_implicit impl <> [] in
+  (* Need to reduce since implicits are computed with products flattened *)
+  print_ref true ref ++ fnl() ++
+  (if has_impl then print_impl_args impl 
+   else (str "No implicit arguments" ++ fnl ()))
+
 let print_local_context () =
   let env = Lib.contents_after None in
   let rec print_var_rec = function 
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 7696884939..d58d7808d8 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -44,6 +44,7 @@ val print_name : reference -> std_ppcmds
 val print_opaque_name : reference -> std_ppcmds
 val print_local_context : unit -> std_ppcmds
 val print_about : reference -> std_ppcmds
+val print_impargs : reference -> std_ppcmds
 
 (*i
 val print_extracted_name : identifier -> std_ppcmds
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 94bdb1a083..67da01408d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -879,6 +879,7 @@ let vernac_print = function
   | PrintVisibility s ->
       pp (Symbols.pr_visibility (Constrextern.without_symbols pr_rawterm) s)
   | PrintAbout qid -> msgnl (print_about qid)
+  | PrintImplicit qid -> msg (print_impargs qid)
 
 let global_module r =
   let (loc,qid) = qualid_of_reference r in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e720245b78..76d16862ae 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -55,6 +55,7 @@ type printable =
   | PrintScope of string
   | PrintVisibility of string option
   | PrintAbout of reference
+  | PrintImplicit of reference
 
 type search_about_item =
   | SearchRef of reference
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 9e6aa0fe05..ae51a552b5 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1020,6 +1020,7 @@ let rec pr_vernac = function
 	| PrintScope s -> str"Print Scope" ++ spc() ++ str s 
 	| PrintVisibility s -> str"Print Visibility" ++ pr_opt str s 
 	| PrintAbout qid -> str"About" ++ spc()  ++ pr_reference qid
+	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_reference qid
       in pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern
   | VernacLocate loc ->