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

7 files changed, 98 insertions, 70 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 1dcdec03df..714f56e788 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 c42b27edc1..b0fb3981fa 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 8e953084da..9024123f3f 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 2205ed8acd..c01eca7f27 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 17b947ebd0..f92eefff0c 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 02c0e65918..126e61ec2a 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 0cdf1c086c..5ff744e3fd 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. *)