New tactics : econstructor, eleft, eright, esplit

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

11 files changed, 113 insertions, 17 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 8eb8d2a0d6..0ed7b97f47 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -32,6 +32,7 @@ type argument_type =
   | TacticArgType
   | CastedOpenConstrArgType
   | ConstrWithBindingsArgType
+  | WithBindingsArgType
   | RedExprArgType
   | List0ArgType of argument_type
   | List1ArgType of argument_type
@@ -120,6 +121,10 @@ let rawwit_constr_with_bindings = ConstrWithBindingsArgType
 let globwit_constr_with_bindings = ConstrWithBindingsArgType
 let wit_constr_with_bindings = ConstrWithBindingsArgType
 
+let rawwit_with_bindings = WithBindingsArgType
+let globwit_with_bindings = WithBindingsArgType
+let wit_with_bindings = WithBindingsArgType
+
 let rawwit_red_expr = RedExprArgType
 let globwit_red_expr = RedExprArgType
 let wit_red_expr = RedExprArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 6c4da92c76..2418646d9b 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -121,6 +121,10 @@ val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) ab
 val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type
 
+val rawwit_with_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type
+val globwit_with_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_with_bindings : (constr bindings,constr,'ta) abstract_argument_type
+
 val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,constr_expr,'ta) abstract_argument_type
 val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type
@@ -204,6 +208,7 @@ type argument_type =
   | TacticArgType
   | CastedOpenConstrArgType
   | ConstrWithBindingsArgType
+  | WithBindingsArgType
   | RedExprArgType
   | List0ArgType of argument_type
   | List1ArgType of argument_type
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 0f4bc93a83..c37e41a012 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -33,6 +33,7 @@ let rec make_rawwit loc = function
   | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
   | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
+  | WithBindingsArgType -> <:expr< Genarg.rawwit_with_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >>
   | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >>
@@ -56,6 +57,7 @@ let rec make_globwit loc = function
   | RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
   | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
+  | WithBindingsArgType -> <:expr< Genarg.globwit_with_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >>
   | List1ArgType t -> <:expr< Genarg.wit_list1 $make_globwit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >>
@@ -79,6 +81,7 @@ let rec make_wit loc = function
   | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
   | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
+  | WithBindingsArgType -> <:expr< Genarg.wit_with_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
   | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9c450101b0..01b59dcf65 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -62,8 +62,8 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 
 if !Options.v7 then
 GEXTEND Gram
-  GLOBAL: simple_tactic constrarg constr_with_bindings quantified_hypothesis
-    red_expr int_or_var castedopenconstr;
+  GLOBAL: simple_tactic constrarg with_bindings constr_with_bindings 
+  quantified_hypothesis red_expr int_or_var castedopenconstr;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
@@ -161,9 +161,9 @@ GEXTEND Gram
 	  ImplicitBindings (c1 :: bl) ] ]
   ;
   constr_with_bindings:
-    [ [ c = constr; l = with_binding_list -> (c, l) ] ]
+    [ [ c = constr; l = with_bindings -> (c, l) ] ]
   ;
-  with_binding_list:
+  with_bindings:
     [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
   ;
   unfold_occ:
@@ -343,12 +343,12 @@ GEXTEND Gram
 	  id2 = id_or_ltac_ref -> TacRename (id1,id2)
 
       (* Constructors *)
-      | IDENT "Left"; bl = with_binding_list -> TacLeft bl
-      | IDENT "Right"; bl = with_binding_list -> TacRight bl
-      | IDENT "Split"; bl = with_binding_list -> TacSplit (false,bl)
+      | IDENT "Left"; bl = with_bindings -> TacLeft bl
+      | IDENT "Right"; bl = with_bindings -> TacRight bl
+      | IDENT "Split"; bl = with_bindings -> TacSplit (false,bl)
       | IDENT "Exists"; bl = binding_list -> TacSplit (true,bl)
       | IDENT "Exists" -> TacSplit (true,NoBindings)
-      | IDENT "Constructor"; n = num_or_meta; l = with_binding_list ->
+      | IDENT "Constructor"; n = num_or_meta; l = with_bindings ->
 	  TacConstructor (n,l)
       | IDENT "Constructor"; t = OPT tactic -> TacAnyConstructor t
 
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 96805e87b0..8151a8c14f 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -128,7 +128,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
-    red_expr int_or_var castedopenconstr;
+ with_bindings red_expr int_or_var castedopenconstr;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
@@ -211,9 +211,9 @@ GEXTEND Gram
       | bl = LIST1 constr -> ImplicitBindings bl ] ]
   ;
   constr_with_bindings:
-    [ [ c = constr; l = with_binding_list -> (c, l) ] ]
+    [ [ c = constr; l = with_bindings -> (c, l) ] ]
   ;
-  with_binding_list:
+  with_bindings:
     [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
   ;
   red_flag:
@@ -387,12 +387,12 @@ GEXTEND Gram
 	  TacRename (id1,id2)
 
       (* Constructors *)
-      | IDENT "left"; bl = with_binding_list -> TacLeft bl
-      | IDENT "right"; bl = with_binding_list -> TacRight bl
-      | IDENT "split"; bl = with_binding_list -> TacSplit (false,bl)
+      | IDENT "left"; bl = with_bindings -> TacLeft bl
+      | IDENT "right"; bl = with_bindings -> TacRight bl
+      | IDENT "split"; bl = with_bindings -> TacSplit (false,bl)
       | "exists"; bl = binding_list -> TacSplit (true,bl)
       | "exists" -> TacSplit (true,NoBindings)
-      | IDENT "constructor"; n = num_or_meta; l = with_binding_list ->
+      | IDENT "constructor"; n = num_or_meta; l = with_bindings ->
 	  TacConstructor (n,l)
       | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor t
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 759030fbe5..32ab9894ed 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -369,6 +369,8 @@ module Tactic =
       make_gen_entry utactic rawwit_casted_open_constr "castedopenconstr"
     let constr_with_bindings =
       make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
+    let with_bindings =
+      make_gen_entry utactic rawwit_with_bindings "with_bindings"
     let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg"
     let quantified_hypothesis =
       make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
@@ -410,6 +412,7 @@ let reset_all_grammars () =
   f Tactic.simple_tactic;
   f Tactic.castedopenconstr;
   f Tactic.constr_with_bindings;
+  f Tactic.with_bindings;
   f Tactic.constrarg;
   f Tactic.quantified_hypothesis;
   f Tactic.int_or_var;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a91a3592dd..cbf416acc8 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -154,6 +154,7 @@ module Tactic :
     open Rawterm
     val castedopenconstr : constr_expr Gram.Entry.e
     val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
+    val with_bindings : constr_expr bindings Gram.Entry.e
     val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
     val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
     val int_or_var : int or_var Gram.Entry.e
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 12e57e85f9..d7b2cbe449 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -268,6 +268,8 @@ let rec pr_raw_generic prc prlc prtac prref x =
       pr_arg prc (out_gen rawwit_casted_open_constr x)
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
+  | WithBindingsArgType -> 
+      pr_arg (pr_bindings prc prlc) (out_gen rawwit_with_bindings x)
   | List0ArgType _ -> 
       hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt()))
   | List1ArgType _ ->
@@ -311,6 +313,8 @@ let rec pr_glob_generic prc prlc prtac x =
       pr_arg prc (out_gen globwit_casted_open_constr x)
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
+  | WithBindingsArgType -> 
+      pr_arg (pr_bindings prc prlc) (out_gen globwit_with_bindings x)
   | List0ArgType _ -> 
       hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt()))
   | List1ArgType _ ->
@@ -353,6 +357,8 @@ let rec pr_generic prc prlc prtac x =
       pr_arg prc (snd (out_gen wit_casted_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x)
+  | WithBindingsArgType -> 
+      pr_arg (pr_bindings prc prlc) (out_gen wit_with_bindings x)
   | List0ArgType _ -> 
       hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt()))
   | List1ArgType _ ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index decb60923d..06b1b8bf99 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -252,6 +252,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
   | Genarg.CastedOpenConstrArgType -> <:expr< Genarg.CastedOpenConstrArgType >>
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
+  | Genarg.WithBindingsArgType -> <:expr< Genarg.WithBindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
   | Genarg.TacticArgType -> <:expr< Genarg.TacticArgType >>
   | Genarg.SortArgType -> <:expr< Genarg.SortArgType >>
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index abacad432f..60a6972b81 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -20,6 +20,7 @@ open Sign
 open Reduction
 open Proof_type
 open Proof_trees
+open Declarations
 open Tacticals
 open Tacmach
 open Evar_refiner
@@ -70,6 +71,68 @@ END
 
 let vernac_e_resolve_constr c = h_eapply (c,NoBindings)
 
+let e_constructor_tac boundopt i lbind gl = 
+    let cl = pf_concl gl in 
+  let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in 
+  let nconstr =
+    Array.length (snd (Global.lookup_inductive mind)).mind_consnames
+  and sigma   = project gl in
+  if i=0 then error "The constructors are numbered starting from 1";
+  if i > nconstr then error "Not enough constructors";
+  begin match boundopt with 
+    | Some expctdnum -> 
+        if expctdnum <> nconstr then 
+	  error "Not the expected number of constructors"
+    | None -> ()
+  end;
+  let cons = mkConstruct (ith_constructor_of_inductive mind i) in
+  let apply_tac = e_resolve_with_bindings_tac (cons,lbind) in
+  (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl
+
+let e_one_constructor i = e_constructor_tac None i
+
+let e_any_constructor tacopt gl =
+  let t = match tacopt with None -> tclIDTAC | Some t -> t in
+  let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in
+  let nconstr =
+    Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
+  if nconstr = 0 then error "The type has no constructors";
+  tclFIRST (List.map (fun i -> tclTHEN (e_one_constructor i NoBindings) t) 
+              (interval 1 nconstr)) gl
+
+let e_left = e_constructor_tac (Some 2) 1
+
+let e_right = e_constructor_tac (Some 2) 2
+
+let e_split = e_constructor_tac (Some 1) 1
+
+(* This automatically define h_econstructor (among other things) *)
+(*V8 TACTIC EXTEND eapply
+  [ "econstructor" integer(n) with_bindings(c) ] -> [ e_constructor_tac None n c ]
+END*)
+TACTIC EXTEND econstructor
+  [ "EConstructor" integer(n) with_bindings(c) ] -> [ e_constructor_tac None n c ]
+  | [ "EConstructor" tactic_opt(t) ] -> [ e_any_constructor (option_app Tacinterp.eval_tactic t) ] 
+END
+
+TACTIC EXTEND eleft
+  [ "ELeft" with_bindings(l) ] -> [e_left l]
+END
+
+TACTIC EXTEND eright
+  [ "ERight" with_bindings(l) ] -> [e_right l]
+END
+
+TACTIC EXTEND esplit
+  [ "ESplit" with_bindings(l) ] -> [e_split l]
+END
+
+(*
+TACTIC EXTEND eexists
+  [ "EExists" with_bindings(l) ] -> [e_split l]
+END
+*)
+
 (************************************************************************)
 (*   PROLOG tactic                                                      *)
 (************************************************************************)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index efe2e3f2c2..f6b05af45c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -821,6 +821,9 @@ and intern_genarg ist x =
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
+  | WithBindingsArgType ->
+      in_gen globwit_with_bindings
+        (intern_bindings ist (out_gen rawwit_with_bindings x))
   | List0ArgType _ -> app_list0 (intern_genarg ist) x
   | List1ArgType _ -> app_list1 (intern_genarg ist) x
   | OptArgType _ -> app_opt (intern_genarg ist) x
@@ -1530,6 +1533,9 @@ and interp_genarg ist goal x =
   | ConstrWithBindingsArgType ->
       in_gen wit_constr_with_bindings
         (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x))
+  | WithBindingsArgType ->
+      in_gen wit_with_bindings
+        (interp_bindings ist goal (out_gen globwit_with_bindings x))
   | List0ArgType _ -> app_list0 (interp_genarg ist goal) x
   | List1ArgType _ -> app_list1 (interp_genarg ist goal) x
   | OptArgType _ -> app_opt (interp_genarg ist goal) x
@@ -1722,8 +1728,8 @@ and interp_atomic ist gl = function
     | QuantHypArgType | RedExprArgType 
     | TacticArgType -> 
 	val_interp ist gl (out_gen globwit_tactic x)
-    | CastedOpenConstrArgType | ConstrWithBindingsArgType | ExtraArgType _
-    | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
+    | CastedOpenConstrArgType | ConstrWithBindingsArgType | WithBindingsArgType 
+    | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
     in
     let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
@@ -2011,6 +2017,9 @@ and subst_genarg subst (x:glob_generic_argument) =
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x))
+  | WithBindingsArgType ->
+      in_gen globwit_with_bindings
+        (subst_bindings subst (out_gen globwit_with_bindings x))
   | List0ArgType _ -> app_list0 (subst_genarg subst) x
   | List1ArgType _ -> app_list1 (subst_genarg subst) x
   | OptArgType _ -> app_opt (subst_genarg subst) x