Réorganisation des tclTHEN (cf dev/changements.txt)

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

2 files changed, 54 insertions, 69 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 238dd4b950..b6fea7dc20 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -19,6 +19,7 @@ open Inductive
 open Reduction
 open Environ
 open Declare
+open Refiner
 open Tacmach
 open Clenv
 open Pattern
@@ -29,24 +30,39 @@ open Wcclausenv
 (*         Basic Tacticals                *)
 (******************************************)
 
-let tclIDTAC         = Tacmach.tclIDTAC
-let tclORELSE        = Tacmach.tclORELSE
-let tclTHEN          = Tacmach.tclTHEN
-let tclTHEN_i        = Tacmach.tclTHEN_i
-let tclTHENL         = Tacmach.tclTHENL
-let tclTHENS         = Tacmach.tclTHENS
-let tclTHENSi        = Tacmach.tclTHENSi
-let tclREPEAT        = Tacmach.tclREPEAT
-let tclFIRST         = Tacmach.tclFIRST
-let tclSOLVE         = Tacmach.tclSOLVE
-let tclTRY           = Tacmach.tclTRY
-let tclINFO          = Tacmach.tclINFO
-let tclCOMPLETE      = Tacmach.tclCOMPLETE
-let tclAT_LEAST_ONCE = Tacmach.tclAT_LEAST_ONCE
-let tclFAIL          = Tacmach.tclFAIL
-let tclDO            = Tacmach.tclDO
-let tclPROGRESS      = Tacmach.tclPROGRESS
-let tclWEAK_PROGRESS = Tacmach.tclWEAK_PROGRESS
+(*************************************************)
+(* Tacticals re-exported from the Refiner module.*)
+(*************************************************)
+
+let tclIDTAC         = tclIDTAC
+let tclORELSE        = tclORELSE
+let tclTHEN          = tclTHEN
+let tclTHENLIST      = tclTHENLIST
+let tclTHEN_i        = tclTHEN_i
+let tclTHENFIRST     = tclTHENFIRST
+let tclTHENLAST      = tclTHENLAST
+let tclTHENS         = tclTHENS
+let tclTHENSV        = Refiner.tclTHENSV
+let tclTHENSFIRSTn   = Refiner.tclTHENSFIRSTn
+let tclTHENSLASTn    = Refiner.tclTHENSLASTn
+let tclTHENFIRSTn    = Refiner.tclTHENFIRSTn
+let tclTHENLASTn     = Refiner.tclTHENLASTn
+let tclREPEAT        = Refiner.tclREPEAT
+let tclREPEAT_MAIN   = tclREPEAT_MAIN
+let tclFIRST         = Refiner.tclFIRST
+let tclSOLVE         = Refiner.tclSOLVE
+let tclTRY           = Refiner.tclTRY
+let tclINFO          = Refiner.tclINFO
+let tclCOMPLETE      = Refiner.tclCOMPLETE
+let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
+let tclFAIL          = Refiner.tclFAIL
+let tclDO            = Refiner.tclDO
+let tclPROGRESS      = Refiner.tclPROGRESS
+let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
+let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
+let tclTHENTRY       = tclTHENTRY
+
+let unTAC            = unTAC
 
 (* [rclTHENSEQ [t1;..;tn] is equivalent to t1;..;tn *)
 let tclTHENSEQ = List.fold_left tclTHEN tclIDTAC
@@ -56,10 +72,6 @@ let tclTHENSEQ = List.fold_left tclTHEN tclIDTAC
 let tclMAP tacfun l = 
   List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
 
-(*let dyn_tclIDTAC = function [] -> tclIDTAC |  _ -> anomaly "tclIDTAC"*)
-
-(*let dyn_tclFAIL  = function [] -> tclFAIL |  _ -> anomaly "tclFAIL"*)
-
 (* apply a tactic to the nth element of the signature  *)
 
 let tclNTH_HYP m (tac : constr->tactic) gl =
@@ -187,30 +199,6 @@ let tryAllHyps     tac gls = tryClauses tac (allHyps gls) gls
 let onNLastHyps n  tac     = onHyps (nLastHyps n) (tclMAP tac)
 let onLastHyp      tac gls = tac (lastHyp gls) gls
 
-(* Serait-ce possible de compiler d'abord la tactique puis de faire la
-   substitution sans passer par bdize dont l'objectif est de préparer un
-   terme pour l'affichage ? (HH) *)
-
-(* Si on enlève le dernier argument (gl) conclPattern est calculé une
-fois pour toutes : en particulier si Pattern.somatch produit une UserError 
-Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
-si après Intros la conclusion matche le pattern.
-*)
-
-(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
-
-let conclPattern concl pat tacast gl =
-  let constr_bindings =
-    try Pattern.matches pat concl
-    with PatternMatchingFailure -> error "conclPattern" in
-  let ast_bindings = 
-    List.map 
-      (fun (i,c) ->
-	 (i, Termast.ast_of_constr false (pf_env gl) c))
-      constr_bindings in 
-  let tacast' = Coqast.subst_meta ast_bindings tacast in
-  Tacinterp.interp tacast' gl
-
 let clauseTacThen tac continuation =
   (fun cls -> (tclTHEN (tac cls) continuation))
 
@@ -252,7 +240,7 @@ type branch_args = {
 
 type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
-  assums    : named_context; (* the list of assumptions introduced *)
+  assums    : named_context;   (* the list of assumptions introduced *)
   cargs     : identifier list; (* the constructor arguments *)
   constargs : identifier list; (* the CONSTANT constructor arguments *)
   recargs   : identifier list; (* the RECURSIVE constructor arguments *)
@@ -337,24 +325,25 @@ let general_elim_then_using
   let branchsigns = elim_sign_fun ity in
   let after_tac ce i gl =
     let (hd,largs) = decompose_app (clenv_template_type ce).rebus in
-    let ba = { branchsign = branchsigns.(i-1);
+    let ba = { branchsign = branchsigns.(i);
                nassums = 
 		 List.fold_left 
                    (fun acc b -> if b then acc+2 else acc+1)
-                   0 branchsigns.(i-1);
-               branchnum = i;
+                   0 branchsigns.(i);
+               branchnum = i+1;
                ity = ity;
                largs = List.map (clenv_instance_term ce) largs;
                pred = clenv_instance_term ce hd }
     in 
     tac ba gl
   in
+  let branchtacs ce = Array.init (Array.length branchsigns) (after_tac ce) in
   let elimclause' =
     match predicate with
        | None   -> elimclause'
        | Some p -> clenv_assign pmv p elimclause'
   in 
-  elim_res_pf_THEN_i kONT elimclause' after_tac gl
+  elim_res_pf_THEN_i kONT elimclause' branchtacs gl
 
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 90cb04f3ea..0557be8829 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -25,12 +25,19 @@ open Wcclausenv
 val tclIDTAC         : tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
+val tclTHENSEQ       : tactic list -> tactic
+val tclTHENLIST      : tactic list -> tactic
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
-val tclTHENL         : tactic -> tactic -> tactic
+val tclTHENFIRST     : tactic -> tactic -> tactic
+val tclTHENLAST      : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
-val tclTHENSi        : tactic -> tactic list -> (int -> tactic) -> tactic
-val tclTHENSEQ       : tactic list -> tactic
+val tclTHENSV        : tactic -> tactic array -> tactic
+val tclTHENSLASTn    : tactic -> tactic -> tactic array -> tactic
+val tclTHENLASTn     : tactic -> tactic array -> tactic
+val tclTHENSFIRSTn   : tactic -> tactic array -> tactic -> tactic
+val tclTHENFIRSTn    : tactic -> tactic array -> tactic
 val tclREPEAT        : tactic -> tactic
+val tclREPEAT_MAIN   : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
 val tclSOLVE         : tactic list -> tactic
 val tclTRY           : tactic -> tactic
@@ -41,16 +48,16 @@ val tclFAIL          : int -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
+val tclNOTSAMEGOAL   : tactic -> tactic
+val tclTHENTRY       : tactic -> tactic -> tactic
+
 val tclNTH_HYP       : int -> (constr -> tactic) -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 val tclLAST_HYP      : (constr -> tactic) -> tactic
 val tclTRY_sign      : (constr -> tactic) -> named_context -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
 
-(*i
-val dyn_tclIDTAC     : tactic_arg list -> tactic
-val dyn_tclFAIL      : tactic_arg list -> tactic
-i*)
+val unTAC            : tactic -> goal sigma -> proof_tree sigma
 
 (*s Clause tacticals. *)
 
@@ -59,10 +66,6 @@ type clause = identifier option
 val nth_clause  : int -> goal sigma -> clause
 val clause_type : clause -> goal sigma -> constr
 
-(*i
-val matches      : goal sigma -> constr -> marked_term -> bool
-val dest_match   : goal sigma -> constr -> marked_term -> constr list
-i*)
 val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
 val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
@@ -95,13 +98,6 @@ val tryAllHyps     : (identifier -> tactic) -> tactic
 val onNLastHyps    : int -> (named_declaration -> tactic) -> tactic
 val onLastHyp      : (identifier -> tactic) -> tactic
 
-(* [ConclPattern concl pat tacast]:
-   if the term concl matches the pattern pat, (in sense of 
-   [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
-   right values to build a tactic *)
-
-val conclPattern : constr -> constr_pattern -> Coqast.t -> tactic
-
 (*s Elimination tacticals. *)
 
 type branch_args = {