Retrait du i pour tclTHEN_i et correction bugs Decompose

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

12 files changed, 98 insertions, 63 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 9e1698c25c..915431d597 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -337,12 +337,11 @@ let thens_tac tac2l taci (sigr,gs,p) =
     with Failure _ -> errorlabstrm "Refiner.combine_tactics"
         [<'sTR "Wrong number of tactics.">] in
   let tac2gl =
-    List.combine gl tac2l @ list_map_i (fun i g -> (g, taci i)) 0 gi in
+    List.combine gl tac2l @ list_map_i (fun i g -> (g, taci i)) 1 gi in
   let gll,pl =
     List.split(List.map (fun (g,tac2) -> apply_sig_tac sigr tac2 g) tac2gl) in
   (sigr, List.flatten gll,
    compose p (mapshape (List.map List.length gll) pl))
-;;
 
 let then_tac tac = thens_tac [] (fun _ -> tac);;
 
@@ -350,55 +349,51 @@ let then_tac tac = thens_tac [] (fun _ -> tac);;
 let non_existent_goal n =
   errorlabstrm ("No such goal: "^(string_of_int n))
     [< 'sTR"Trying to apply a tactic to a non existent goal" >]
-;;
 
 (* Apply tac on the i-th goal (if i>0). If i<0, then start counting from
    the last goal (i=-1). *)
 let theni_tac i tac ((_,gl,_) as subgoals) =
   let nsg = List.length gl in
-  let k = if i < 0 then nsg + i else (i-1) in
+  let k = if i < 0 then nsg + i + 1 else i in
   if nsg < 1 then errorlabstrm "theni_tac" [< 'sTR"No more subgoals.">]
-  else if k >= 0 & k < nsg then
+  else if k >= 1 & k <= nsg then
     thens_tac [] (fun i -> if i = k then tac else tclIDTAC) subgoals
-  else non_existent_goal (k+1) 
-;;
+  else non_existent_goal k 
 
-
-(* tclTHENSi tac1 [t1 ; ... ; tn] taci gls applies the tactic tac1 to gls and
-   applies t1,..., tn to the n first resulting subgoals, and (taci i) to the
-   (i+n+1)-th goal. Raises an error if the number of resulting subgoals
-   is less than n *)
+(* [tclTHENSi tac1 [t1 ; ... ; tn] taci gls] applies the tactic [tac1]
+   to [gls] and applies [t1], ..., [tn] to the [n] first resulting
+   subgoals, and [(taci i)] to the (i+n)-th goal. Raises an error if
+   the number of resulting subgoals is less than [n] *)
 let tclTHENSi tac1 tac2l taci gls =
   finish_tac (thens_tac tac2l taci (then_tac tac1 (start_tac gls)))
 ;;
 
-(* tclTHEN tac1 tac2 gls applies the tactic tac1 to gls and applies tac2 to
-   every resulting subgoals *)
+(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+   [tac2] to every resulting subgoals *)
 let tclTHEN tac1 tac2 = tclTHENSi tac1 [] (fun _ -> tac2);;
 
-(* tclTHEN_i tac1 tac2 n gls applies the tactic tac1 to gls and applies
-   tac2 (i+n-1) to the i_th resulting subgoal *)
-let tclTHEN_i tac1 tac2 n = tclTHENSi tac1 [] (fun i -> tac2 (i+n));;
+(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+   [(tac2 i)] to the i_th resulting subgoal (starting from 1) *)
+let tclTHEN_i tac1 tac2 = tclTHENSi tac1 [] tac2;;
 
-(* tclTHENS tac1 [t1 ; ... ; tn] gls applies the tactic tac1 to gls and applies
-   t1,..., tn to the n resulting subgoals. Raises an error if the number of
-   resulting subgoals is not n *)
+(* [tclTHENS tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
+   [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
+   an error if the number of resulting subgoals is not [n] *)
 let tclTHENS tac1 tac2l =
   tclTHENSi tac1 tac2l (fun _ -> tclFAIL_s "Wrong number of tactics.");;
 
-(* Same as tclTHENS but completes with Idtac if the number resulting subgoals
-  is strictly less than n *)
+(* Same as [tclTHENS] but completes with [Idtac] if the number resulting 
+  subgoals is strictly less than [n] *)
 let tclTHENSI tac1 tac2l = tclTHENSi tac1 tac2l (fun _ -> tclIDTAC);;
 
-
-(* tclTHENL tac1 tac2 gls applies the tactic tac1 to gls and tac2
+(* [tclTHENL tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
    to the last resulting subgoal *)
 let tclTHENL (tac1 : tactic) (tac2 : tactic) (gls : goal sigma) =
   finish_tac (theni_tac (-1) tac2 (then_tac tac1 (start_tac gls)))
 ;;
 
-(* tclTHENLIST [t1;..;tn] applies t1;..tn. More convenient than tclTHEN
-   when n is large. *)
+(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More
+   convenient than [tclTHEN] when [n] is large. *)
 let rec tclTHENLIST = function
     [] -> tclIDTAC
   | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 4b821596e4..98c6ab96fe 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -45,14 +45,35 @@ val extract_open_proof :
 
 (*s Tacticals. *)
 
+(* [tclIDTAC] is the identity tactic *)
 val tclIDTAC         : tactic
-val tclORELSE        : tactic -> tactic -> tactic
+
+(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+   [tac2] to every resulting subgoals *)
 val tclTHEN          : tactic -> tactic -> tactic
+
+(* [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More
+   convenient than [tclTHEN] when [n] is large *)
 val tclTHENLIST      : tactic list -> tactic
-val tclTHEN_i        : tactic -> (int -> tactic) -> int -> tactic
+
+(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+   [(tac2 i)] to the i_th resulting subgoal (starting from 1) *)
+val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
+
+(* [tclTHENL tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the last resulting subgoal *)
 val tclTHENL         : tactic -> tactic -> tactic
+
+(* [tclTHENS tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
+   [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
+   an error if the number of resulting subgoals is not [n] *)
 val tclTHENS         : tactic -> tactic list -> tactic
+
+(* Same as [tclTHENS] but completes with [Idtac] if the number resulting 
+  subgoals is strictly less than [n] *)
 val tclTHENSI        : tactic -> tactic list -> tactic
+
+val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
 val tclSOLVE         : tactic list -> tactic
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index afb9016ea5..b27b0b789e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -117,7 +117,7 @@ val tclIDTAC         : tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
 val tclTHENLIST      : tactic list -> tactic
-val tclTHEN_i        : tactic -> (int -> tactic) -> int -> tactic
+val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
 val tclTHENL         : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
 val tclTHENSI        : tactic -> tactic list -> tactic
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ff07f6c09a..4e414b35ea 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -42,7 +42,7 @@ Require Elim.
 Require Le.
    Goal (y:nat){x:nat | (le O x)/\(le x y)}->(le O y).
    Intros y H.
-   Decompose [sig and] H;EAuto.
+   Decompose [sig and] H;EAuto.  [HUM HUM !! Y a peu de chance qu'ça marche !]
    Qed.
 
 Another example :
@@ -67,33 +67,46 @@ let rec general_decompose_clause recognizer =
 	 cls)
     (fun _ -> tclIDTAC)
 
+(* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste
+   pas si aucune élimination n'est possible *)
+
 let rec general_decompose recognizer c gl = 
   let typc = pf_type_of gl c in  
   (tclTHENS (cut typc) 
      [(tclTHEN intro 
          (onLastHyp (general_decompose_clause recognizer)));
       (exact c)]) gl
-  
-let head_in l c = List.mem (List.hd (head_constr c)) l
-		    
+
+let head_in gls indl t =
+  try
+    let ity = fst (find_mrectype (pf_env gls) (project gls) t) in
+    List.mem ity indl
+  with Induc -> false
+       
+let inductive_of_ident gls id =
+  try 
+    fst (find_mrectype (pf_env gls) (project gls) (pf_global gls id))
+  with Induc ->
+    errorlabstrm "Decompose" 
+      [< print_id id; 'sTR " is not an inductive type" >]
+
 let decompose_these c l gls =
-  let l = List.map (pf_global gls) l in 
-  general_decompose (fun (_,t) -> head_in l t) c gls
+  let indl = List.map (inductive_of_ident gls) l in 
+  general_decompose (fun (_,t) -> head_in gls indl t) c gls
 
 let decompose_nonrec c gls =
   general_decompose 
-    (fun (_,t) -> 
-       (is_non_recursive_type  (List.hd (head_constr t))))
+    (fun (_,t) -> is_non_recursive_type t)
     c gls
 
 let decompose_and c gls = 
   general_decompose 
-    (fun (_,t) -> (is_conjunction (List.hd (head_constr t))))
+    (fun (_,t) -> is_conjunction t)
     c gls
 
 let decompose_or c gls = 
   general_decompose 
-    (fun (_,t) -> (is_disjunction (List.hd (head_constr t))))
+    (fun (_,t) -> is_disjunction t)
     c gls
 
 let dyn_decompose args gl = 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5ecf3a39a2..b4cc547d13 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -142,7 +142,7 @@ let h_replace c1 c2 = v_replace [(Constr c1);(Constr c2)]
 
 let conditional_rewrite lft2rgt tac (c,bl) = 
   tclTHEN_i (general_rewrite_bindings lft2rgt (c,bl))
-    (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac) 1
+    (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)
 
 let dyn_conditional_rewrite lft2rgt = function
   | [(Tacexp tac); (Command com);(Bindings binds)] -> 
@@ -1470,7 +1470,7 @@ let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false)
 			 
 let conditional_rewrite_in lft2rgt id tac (c,bl) = 
   tclTHEN_i (general_rewrite_in lft2rgt id (c,bl))
-    (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac) 1
+    (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)
     
 let dyn_conditional_rewrite_in lft2rgt = function
   | [(Tacexp tac); Identifier id; (Command com);(Bindings binds)] -> 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 294a13c6d7..c8f6876988 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -48,8 +48,6 @@ let dyn_tclIDTAC = function [] -> tclIDTAC |  _ -> anomaly "tclIDTAC"
 
 let dyn_tclFAIL  = function [] -> tclFAIL |  _ -> anomaly "tclFAIL"
 
-let tclTHEN_i1 tac1 tac2 = tclTHEN_i tac1 tac2 1
-
 (* apply a tactic to the nth element of the signature  *)
 
 let tclNTH_HYP m (tac : constr->tactic) gl =
@@ -344,14 +342,14 @@ let general_elim_then_using
                largs = List.map (clenv_instance_term ce) largs;
                pred = clenv_instance_term ce hd }
     in 
-    tac ba gl 
+    tac ba gl
   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 1 gl
+  elim_res_pf_THEN_i kONT elimclause' after_tac gl
 
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index de91973d62..7a0e3f9c51 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -18,7 +18,7 @@ open Wcclausenv
 val tclIDTAC         : tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
-val tclTHEN_i        : tactic -> (int -> tactic) -> int -> tactic
+val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
 val tclTHENL         : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
 val tclREPEAT        : tactic -> tactic
@@ -44,7 +44,6 @@ val dyn_tclFAIL      : tactic_arg list -> tactic
 
 type clause = identifier option
 
-val tclTHEN_i1     : tactic -> (int -> tactic) -> tactic
 val nth_clause  : int -> goal sigma -> clause
 val clause_type : clause -> goal sigma -> constr
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 860c981264..c35109e2c3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -38,7 +38,16 @@ let get_pairs_from_bindings =
     | _                  -> error "not a binding list!"
   in 
   List.map pair_from_binding
-    
+
+let force_reference c =
+  match fst (decomp_app c) with
+  | DOPN (Const sp,ctxt) -> c
+  | DOPN (Evar ev,ctxt) -> c
+  | DOPN (MutConstruct (spi,j),ctxt) -> c
+  | DOPN (MutInd (sp,i),ctxt) -> c
+  | VAR id -> c
+  | _ -> error "Not an atomic type"
+
 let rec string_head_bound = function 
   | DOPN(Const _,_) as x -> 
       string_of_id (basename (path_of_const x))
@@ -50,10 +59,11 @@ let rec string_head_bound = function
        string_of_id (mib.mind_packets.(tyi).mind_consnames.(i-1))
   |  VAR id -> string_of_id id
   |  _ -> raise Bound
-	 
+
 let string_head c = 
   try string_head_bound c with Bound -> error "Bound head variable"
 
+
 let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
   match t with
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 751a777390..92e76fbd3d 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -25,6 +25,9 @@ val make_clenv_binding_apply :
 val type_clenv_binding : walking_constraints ->
   constr * constr -> constr substitution  -> constr
 
+(* [force_reference c] fails if [c] is not a reference *)
+val force_reference   : constr -> constr
+
 val string_head       : constr -> string
 val head_constr       : constr -> constr list
 val head_constr_bound : constr -> constr list -> constr list
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 2708bf01ae..52b4e288c0 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -1864,18 +1864,14 @@ let tautoOR ti gls =
         (t_exacto := tt;
          subbuts l thyp gls)
 
-let exact_Idtac = function 
-  | 0 -> exacto (!t_exacto)
-  | _ -> tclIDTAC
-
 let tautoOR_0 gl = 
   tclORELSE
-    (tclTHEN_i (tautoOR false) exact_Idtac 0)
+    (tclTHENSI (tautoOR false) [exacto (!t_exacto)])
     tAUTOFAIL gl
 
 let intuitionOR = 
   tclTRY (tclTHEN 
-	    (tclTHEN_i (tautoOR true) exact_Idtac 0)  
+	    (tclTHENSI (tautoOR true) [exacto (!t_exacto)])
 	    default_full_auto)
 
 (*--- Mixed code Chet-Cesar ---*)
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index b7fdd67a70..7cdd5c1fe5 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -124,13 +124,13 @@ let res_pf_THEN kONT clenv tac gls =
   let clenv' = (clenv_unique_resolver false clenv gls) in 
   (tclTHEN (clenv_refine kONT clenv') (tac clenv')) gls
 
-let res_pf_THEN_i kONT clenv tac i gls =
+let res_pf_THEN_i kONT clenv tac gls =
   let clenv' = (clenv_unique_resolver false clenv gls) in 
-  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') i gls
+  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
 
-let elim_res_pf_THEN_i kONT clenv tac i gls =  
+let elim_res_pf_THEN_i kONT clenv tac gls =  
   let clenv' = (clenv_unique_resolver true clenv gls) in
-  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') i gls
+  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
 
 let rec build_args acc ce p_0 p_1 =
   match p_0,p_1 with 
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 01d05a690d..af96177b36 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -42,13 +42,13 @@ val add_prods_sign :
 val res_pf_THEN : 
   (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic) -> tactic
 
+(* This behaves as [res_pf_THEN] but the tactic applied then takes
+   also the subgoal number (starting from 1) as argument *)
 val res_pf_THEN_i : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> 
-    int -> tactic
+  (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
 
 val elim_res_pf_THEN_i : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> 
-    int -> tactic
+  (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
 
 val mk_clenv_using : wc -> constr -> wc clausenv