- debugging og "Show Intros": no line breaking + fresh ids

- added the command "Show Match t" which prints a typical
  "match...with" for type t.


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

4 files changed, 58 insertions, 9 deletions

diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index 914a92bf48..f482aa152e 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -75,6 +75,7 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
       | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
       | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
+      | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id)
       | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer ->
 	  VernacShow (ExplainProof l)
       | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d288c3153f..926d3e73b6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -114,7 +114,7 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
 
 let fresh_id_of_name avoid gl = function
     Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl
-  | Name id   -> id
+  | Name id   -> Tactics.fresh_id avoid id gl
 
 let rec do_renum avoid gl = function
     [] -> mt ()
@@ -128,15 +128,60 @@ let show_intro all =
   let gl = nth_goal_of_pftreestate 1 pf in
   let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in
   let nl = List.rev_map fst l in
-  if all then
-    msgnl (do_renum [] gl nl)
-  else
-    try 
-      let n = List.hd nl in
-      msgnl (pr_id (fresh_id_of_name [] gl n))
-    with Failure "hd" -> message "" 
+  if all then msgnl (hov 0 (do_renum [] gl nl))
+  else try 
+    let n = List.hd nl in
+    msgnl (pr_id (fresh_id_of_name [] gl n))
+  with Failure "hd" -> message "" 
+
+
+let id_of_name = function 
+  | Names.Anonymous -> id_of_string "x" 
+  | Names.Name x -> x
+
+
+(* Building of match expression *)
+(* From ide/coq.ml *)
+let make_cases s = 
+  let qualified_name = Libnames.qualid_of_string s in
+  let glob_ref = Nametab.locate qualified_name in
+  match glob_ref with
+    | Libnames.IndRef i -> 
+	let {Declarations.mind_nparams = np}
+	    , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } 
+	      = Global.lookup_inductive i in
+	Util.array_fold_right2 
+	  (fun n t l ->  
+	     let (al,_) = Term.decompose_prod t in
+	     let al,_ = Util.list_chop (List.length al - np) al in
+	     let rec rename avoid = function 
+	       | [] -> []
+	       | (n,_)::l -> 
+		   let n' = Termops.next_global_ident_away true (id_of_name n) avoid in
+		   string_of_id n' :: rename (n'::avoid) l in
+	     let al' = rename [] (List.rev al) in
+	     (string_of_id n :: al') :: l)
+	  carr tarr []
+    | _ -> raise Not_found
+
+
+let show_match id = 
+  try
+    let s = string_of_id (snd id) in
+    let patterns = make_cases s in
+    let cases = 
+      List.fold_left 
+	(fun acc x -> 
+	  match x with
+	    | [] -> assert false
+	    | [x] -> "| "^ x  ^ " => \n" ^ acc
+	    | x::l -> 
+		"| (" ^ List.fold_left (fun acc s ->  acc ^ " " ^ s) x l ^ ")" 
+		^ " => \n" ^ acc)
+	"end" patterns in
+    msg (str ("match # with\n" ^ cases))
+  with Not_found -> error "Unknown inductive type"
 
-(********************)
 (* "Print" commands *)
 
 let print_path_entry (s,l) =
@@ -1045,6 +1090,7 @@ let vernac_show = function
   | ShowProofNames ->
       msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names()))
   | ShowIntros all -> show_intro all
+  | ShowMatch id -> show_match id
   | ExplainProof occ -> explain_proof occ
   | ExplainTree occ -> explain_tree occ
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ba556c01cc..e62288d16d 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -99,6 +99,7 @@ type showable =
   | ShowTree
   | ShowProofNames
   | ShowIntros of bool
+  | ShowMatch of lident
   | ExplainProof of int list
   | ExplainTree of int list
 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index af1f66c739..e5d7d75bd9 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -492,6 +492,7 @@ let rec pr_vernac = function
 	| ShowTree -> str"Show Tree"
 	| ShowProofNames -> str"Show Conjectures"
 	| ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro")
+	| ShowMatch id -> str"Show Match " ++ pr_lident id
 	| ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l
 	| ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l 
       in pr_showable s