New tactics : econstructor, eleft, eright, esplit

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

2 files changed, 74 insertions, 2 deletions

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