Utilisation de intro_pattern dans NewDestruct/NewInduction

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

15 files changed, 124 insertions, 95 deletions

diff --git a/CHANGES b/CHANGES
index 8451feabc..9b7d2f7a2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -82,6 +82,7 @@ Tactics
 - Quantified names now avoid global names of the current module (like
   Intro names did) [source of rare incompatibilities: 2 changes in the set of
   user contribs]
+- NewDestruct/NewInduction accepts intro patterns as introduction names
 
 Bugs
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 14caa9f98..54f22c646 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -512,6 +512,11 @@ let rec xlate_intro_pattern =
   | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
 
+let xlate_newind_names = 
+  function
+    | IntroIdentifier id -> xlate_ident id
+    | _ -> xlate_error "TODO: intro_patterns for NewDestruct/NewInduction"
+
 let compute_INV_TYPE_from_string = function
    "InversionClear" -> CT_inv_clear
  | "SimpleInversion" -> CT_inv_simple
@@ -1005,12 +1010,12 @@ and xlate_tac =
 	CT_new_destruct
 	  (xlate_int_or_constr a, xlate_using b, 
 	   CT_id_list_list
-	     (List.map (fun l -> CT_id_list(List.map xlate_ident l)) c))
+	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
     | TacNewInduction(a,b,c) ->
 	CT_new_induction
 	  (xlate_int_or_constr a, xlate_using b, 
 	   CT_id_list_list
-	     (List.map (fun l -> CT_id_list(List.map xlate_ident l)) c))
+	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
     | TacInstantiate (a, b) -> 
 	CT_instantiate(CT_int a, xlate_formula b)
     | TacLetTac (id, c, cl) ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 225aa4728..3b7081012 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -236,7 +236,7 @@ GEXTEND Gram
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
   with_names:
-    [ [ "as"; "["; ids = LIST1 (LIST0 base_ident) SEP "|"; "]" -> ids
+    [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids
       | -> [] ] ]
   ;
   simple_tactic:
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 40a292ca1..c45dc332f 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -234,7 +234,7 @@ GEXTEND Gram
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
   with_names:
-    [ [ "as"; "["; ids = LIST1 (LIST0 base_ident) SEP "|"; "]" -> ids
+    [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids
       | -> [] ] ]
   ;
   simple_tactic:
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 9c23d0ba5..0382a2fdb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -130,24 +130,20 @@ let pr_bindings prc prlc = function
 let pr_with_bindings prc prlc (c,bl) = 
   prc c ++ hv 0 (pr_bindings prc prlc bl)
 
-let pr_with_names = function
-  | [] -> mt ()
-  | ids -> spc () ++ str "as [" ++
-      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
-              (prlist_with_sep spc pr_id) ids ++ str "]")
-
 let rec pr_intro_pattern = function
   | IntroOrAndPattern pll ->
       str "[" ++
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
       ++ str "]"
-(*
-  | IntroAndPattern pl ->
-      str "(" ++ hov 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
-*)
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
 
+let pr_with_names = function
+  | [] -> mt ()
+  | ids -> spc () ++ str "as [" ++
+      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
+              (prlist_with_sep spc pr_intro_pattern) ids ++ str "]")
+
 let pr_hyp_location pr_id = function
   | InHyp id -> spc () ++ pr_id id
   | InHypType id -> spc () ++ str "(Type of " ++ pr_id id ++ str ")"
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index cf59d9a97..f5ebd8fcf 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -376,13 +376,13 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacOldInduction $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacNewInduction (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
       <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>>
   | Tacexpr.TacOldDestruct h ->
       <:expr< Tacexpr.TacOldDestruct $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacNewDestruct (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
       <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
 
   (* Context management *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index f0bace786..3098aceb3 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -111,10 +111,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* Derived basic tactics *)
   | TacOldInduction of quantified_hypothesis
   | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
-      * identifier list list
+      * intro_pattern_expr list list
   | TacOldDestruct of quantified_hypothesis
   | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
-      * identifier list list
+      * intro_pattern_expr list list
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 1dcdec03d..714f56e78 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -183,29 +183,4 @@ let double_ind h1 h2 gls =
 let h_double_induction h1 h2 =
   Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2)
 
-(*****************************)
-(* Decomposing introductions *)
-(*****************************)
-
-let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
-let case_last  = tclLAST_HYP h_simplest_case
-
-let rec intro_pattern = function
-  | IntroWildcard ->
-      tclTHEN intro clear_last
-  | IntroIdentifier id ->
-      intro_mustbe_force id
-  | IntroOrAndPattern l ->
-      tclTHEN introf
-        (tclTHENS
-	  (tclTHEN case_last clear_last)
-	  (List.map intros_pattern l))
-
-and intros_pattern l = tclMAP intro_pattern l
-
-let intro_patterns = function 
-  | [] -> tclREPEAT intro
-  | l  -> tclMAP intro_pattern l
-
-let h_intro_patterns l = Refiner.abstract_tactic (TacIntroPattern l) (intro_patterns l)
 
diff --git a/tactics/elim.mli b/tactics/elim.mli
index c42b27edc..b0fb3981f 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -34,11 +34,3 @@ val h_decompose_and   : constr -> tactic
 
 val double_ind : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis -> tactic
 val h_double_induction : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis->tactic
-
-val intro_pattern     : Tacexpr.intro_pattern_expr      -> tactic
-val intros_pattern    : Tacexpr.intro_pattern_expr list -> tactic
-(*
-val dyn_intro_pattern : tactic_arg list    -> tactic
-val v_intro_pattern   : tactic_arg list    -> tactic
-*)
-val h_intro_patterns  : Tacexpr.intro_pattern_expr list -> tactic
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 8e953084d..9024123f3 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -95,3 +95,5 @@ let h_simplest_apply c  = h_apply (c,NoBindings)
 let h_simplest_elim c   = h_elim (c,NoBindings) None
 let h_simplest_case   c = h_case (c,NoBindings)
 
+let h_intro_patterns l = abstract_tactic (TacIntroPattern l) (intro_patterns l)
+
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 2205ed8ac..c01eca7f2 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -57,10 +57,10 @@ val h_old_induction   : quantified_hypothesis -> tactic
 val h_old_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
   constr induction_arg -> constr with_bindings option ->
-    identifier list list -> tactic
+    intro_pattern_expr list list -> tactic
 val h_new_destruct    :
   constr induction_arg -> constr with_bindings option -> 
-    identifier list list -> tactic
+    intro_pattern_expr list list -> tactic
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
 
@@ -101,3 +101,5 @@ val h_transitivity    : constr -> tactic
 val h_simplest_apply  : constr -> tactic 
 val h_simplest_elim   : constr -> tactic
 val h_simplest_case   : constr -> tactic
+
+val h_intro_patterns  : intro_pattern_expr list -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 17b947ebd..f92eefff0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -583,12 +583,12 @@ let rec intern_atomic lf ist x =
   | TacNewInduction (c,cbo,ids) ->
       TacNewInduction (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               List.map (List.map (intern_ident lf ist)) ids)
+               List.map (List.map (intern_intro_pattern lf ist)) ids)
   | TacOldDestruct h -> TacOldDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               List.map (List.map (intern_ident lf ist)) ids)
+               List.map (List.map (intern_intro_pattern lf ist)) ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
       let h2 = intern_quantified_hypothesis ist h2 in
@@ -1547,7 +1547,7 @@ and interp_tactic ist tac gl =
 and interp_atomic ist gl = function
   (* Basic tactics *)
   | TacIntroPattern l ->
-      Elim.h_intro_patterns (List.map (interp_intro_pattern ist) l)
+      h_intro_patterns (List.map (interp_intro_pattern ist) l)
   | TacIntrosUntil hyp ->
       h_intros_until (interp_quantified_hypothesis ist gl hyp)
   | TacIntroMove (ido,ido') ->
@@ -1597,12 +1597,12 @@ and interp_atomic ist gl = function
   | TacNewInduction (c,cbo,ids) ->
       h_new_induction (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (List.map (List.map (eval_ident ist)) ids)
+        (List.map (List.map (interp_intro_pattern ist)) ids)
   | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist gl h)
   | TacNewDestruct (c,cbo,ids) -> 
       h_new_destruct (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (List.map (List.map (eval_ident ist)) ids)
+        (List.map (List.map (interp_intro_pattern ist)) ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist gl h1 in
       let h2 = interp_quantified_hypothesis ist gl h2 in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 02c0e6591..126e61ec2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -305,6 +305,8 @@ let intro_force force_flag = intro_gen (IntroAvoid []) None force_flag
 let intro = intro_force false
 let introf = intro_force true
 
+let introf_move_name destopt = intro_gen (IntroAvoid []) destopt true
+
 (* For backwards compatibility *)
 let central_intro = intro_gen
 
@@ -968,6 +970,46 @@ let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl =
   let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in 
   elimination_in_clause_scheme kONT id elimclause indclause gl
 
+(* Case analysis tactics *)
+
+let general_case_analysis (c,lbindc) gl =
+  let env = pf_env gl in
+  let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+  let sigma    = project gl in 
+  let sort     = elimination_sort_of_goal gl in
+  let case = if occur_term c (pf_concl gl) then Indrec.make_case_dep
+  else Indrec.make_case_gen in
+  let elim     = case env sigma mind sort in 
+  general_elim (c,lbindc) (elim,NoBindings) gl
+    
+let simplest_case c = general_case_analysis (c,NoBindings)
+
+(*****************************)
+(* Decomposing introductions *)
+(*****************************)
+
+let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
+let case_last  = tclLAST_HYP simplest_case
+
+let rec intro_pattern destopt = function
+  | IntroWildcard ->
+      tclTHEN intro clear_last
+  | IntroIdentifier id ->
+      intro_gen (IntroMustBe id) destopt true
+  | IntroOrAndPattern l ->
+      tclTHEN introf
+        (tclTHENS
+	  (tclTHEN case_last clear_last)
+	  (List.map (intros_pattern destopt) l))
+
+and intros_pattern destopt l = tclMAP (intro_pattern destopt) l
+
+let intro_patterns = function 
+  | [] -> tclREPEAT intro
+  | l  -> intros_pattern None l
+
+let h_intro_patterns l = abstract_tactic (TacIntroPattern l) (intro_patterns l)
+
 (*
  * A "natural" induction tactic
  * 
@@ -1000,11 +1042,27 @@ let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl =
 
  *)
 
+let rec str_intro_pattern = function
+  | IntroOrAndPattern pll ->
+      "["^(String.concat "|" 
+	(List.map 
+	  (fun pl -> String.concat " " (List.map str_intro_pattern pl)) pll))
+      ^"]"
+  | IntroWildcard -> "_"
+  | IntroIdentifier id -> string_of_id id
+
 let check_unused_names names =
   if names <> [] & Options.is_verbose () then
-    let s,are = if List.tl names = [] then " "," is" else "s "," are" in
-    let names = String.concat " " (List.map string_of_id names) in
-    warning ("Name"^s^names^are^" unused")
+    let s = if List.tl names = [] then " " else "s " in
+    let names = String.concat " " (List.map str_intro_pattern names) in
+    warning ("Unused introduction pattern"^s^": "^names)
+
+let rec first_name_buggy = function
+  | IntroOrAndPattern [] -> None
+  | IntroOrAndPattern ([]::l) -> first_name_buggy (IntroOrAndPattern l)
+  | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p
+  | IntroWildcard -> None
+  | IntroIdentifier id -> Some id
 
 (* We recompute recargs because we are not sure the elimination lemma
 comes from a canonically generated one *)
@@ -1062,21 +1120,28 @@ let induct_discharge old_style mind statuslists cname destopt avoid ra names gl
   in
   let rec peel_tac ra names gl = match ra with
     | true :: ra' ->
-        let recvar,hyprec,names = match names with
+        let recpat,hyprec,names = match names with
           | [] ->
-              (fresh_id avoid recvarname gl, fresh_id avoid hyprecname gl, [])
-          | [id] -> (id, next_ident_away (add_prefix "IH" id) avoid, [])
-          | id1::id2::names -> (id1,id2,names) in
-	if !tophyp=None then tophyp := Some hyprec;
+              (IntroIdentifier (fresh_id avoid recvarname gl), 
+	       IntroIdentifier (fresh_id avoid hyprecname gl), [])
+          | [IntroIdentifier id as pat] ->
+	      (pat,
+	       IntroIdentifier (next_ident_away (add_prefix "IH" id) avoid),
+	       [])
+	  | [pat] ->
+	      (pat, IntroIdentifier (fresh_id avoid hyprecname gl), [])
+          | pat1::pat2::names -> (pat1,pat2,names) in
+	(* This is buggy for intro-or-patterns with different first hypnames *)
+	if !tophyp=None then tophyp := first_name_buggy hyprec;
         tclTHENLIST
-	  [ intro_gen (IntroMustBe recvar) destopt false;
-	    intro_gen (IntroMustBe hyprec) None false;
+	  [ intros_pattern destopt [recpat];
+	    intros_pattern None [hyprec];
 	    peel_tac ra' names ] gl
     | false :: ra' ->
-        let introstyle,names = match names with
-          | [] -> IntroAvoid avoid, []
-          | id::names -> IntroMustBe id,names in
-	tclTHEN (intro_gen introstyle destopt false) (peel_tac ra' names) gl
+        let introtac,names = match names with
+          | [] -> intro_gen (IntroAvoid avoid) destopt false, []
+          | pat::names -> intros_pattern destopt [pat],names in
+	tclTHEN introtac (peel_tac ra' names) gl
     | [] ->
         check_unused_names names;
         tclIDTAC gl
@@ -1400,20 +1465,6 @@ let old_induct = function
   | NamedHyp id -> old_induct_id id
   | AnonHyp n -> old_induct_nodep n
 
-(* Case analysis tactics *)
-
-let general_case_analysis (c,lbindc) gl =
-  let env = pf_env gl in
-  let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let sigma    = project gl in 
-  let sort     = elimination_sort_of_goal gl in
-  let case = if occur_term c (pf_concl gl) then Indrec.make_case_dep
-  else Indrec.make_case_gen in
-  let elim     = case env sigma mind sort in 
-  general_elim (c,lbindc) (elim,NoBindings) gl
-    
-let simplest_case c = general_case_analysis (c,NoBindings)
-
 (* Destruction tactics *)
 
 let old_destruct_id s    =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0cdf1c086..5ff744e3f 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -91,6 +91,12 @@ val intros_clearing      : bool list -> tactic
 val try_intros_until :
   (identifier -> tactic) -> quantified_hypothesis -> tactic
 
+(*s Introduction tactics with eliminations. *)
+
+val intro_pattern     : identifier option -> intro_pattern_expr      -> tactic
+val intro_patterns    : intro_pattern_expr list -> tactic
+val intros_pattern    : identifier option -> intro_pattern_expr list -> tactic
+
 (*s Exact tactics. *)
 
 val assumption       : tactic
@@ -171,7 +177,7 @@ val general_elim_in : identifier -> constr * constr bindings ->
                       constr * constr bindings -> tactic
 
 val new_induct : constr induction_arg -> constr with_bindings option ->
-  identifier list list -> tactic
+  intro_pattern_expr list list -> tactic
 
 (*s Case analysis tactics. *)
 
@@ -180,7 +186,7 @@ val simplest_case         : constr -> tactic
 
 val old_destruct          : quantified_hypothesis -> tactic
 val new_destruct : constr induction_arg -> constr with_bindings option ->
-  identifier list list -> tactic
+  intro_pattern_expr list list -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)
 
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 6f56a72b2..2bbb2d082 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -65,21 +65,20 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc
 
 let pr_with_bindings prlc prc (c,bl) = prc c ++ pr_bindings prlc prc bl
 
-let pr_with_names = function
-  | [] -> mt ()
-  | ids -> spc () ++ str "as [" ++
-      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
-              (prlist_with_sep spc pr_id) ids ++ str "]")
-
 let rec pr_intro_pattern = function
   | IntroOrAndPattern pll ->
       str "[" ++
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
       ++ str "]"
-
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
 
+let pr_with_names = function
+  | [] -> mt ()
+  | ids -> spc () ++ str "as [" ++
+      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
+              (prlist_with_sep spc pr_intro_pattern) ids ++ str "]")
+
 let pr_hyp_location pr_id = function
   | InHyp id -> spc () ++ pr_id id
   | InHypType id -> spc () ++ str "(type of " ++ pr_id id ++ str ")"