Ajout Simpl et Change sur des sous-termes

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

7 files changed, 82 insertions, 84 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 75bcb0d6b..52661952e 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -86,7 +86,7 @@ let h_simplest_right  = h_right NoBindings
 
 (* Conversion *)
 let h_reduce r cl  = abstract_tactic (TacReduce (r,cl)) (reduce r cl)
-let h_change c cl  = abstract_tactic (TacChange (c,cl)) (change c cl)
+let h_change oc c cl  = abstract_tactic (TacChange (oc,c,cl)) (change oc c cl)
 
 (* Equivalence relations *)
 let h_reflexivity    = abstract_tactic TacReflexivity intros_reflexivity
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 797315d64..9bef1f269 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -90,7 +90,8 @@ val h_simplest_right  : tactic
 
 (* Conversion *)
 val h_reduce          : Tacred.red_expr -> hyp_location list -> tactic
-val h_change          : constr -> hyp_location list -> tactic
+val h_change          : 
+  constr occurrences option -> constr -> hyp_location list -> tactic
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
diff --git a/tactics/refine.ml b/tactics/refine.ml
index d1f380e49..1a360f9ba 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -284,7 +284,7 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	let c = pf_concl gl in
 	let newc = mkNamedLetIn id c1 t1 c in
 	tclTHEN 
-	  (change_in_concl newc) 
+	  (change_in_concl None newc) 
 	  (match sgp with 
 	     | [None] -> introduction id
 	     | [Some th] -> tclTHEN (introduction id) (tcc_aux th)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index fa62c8dd4..fd57bce87 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -636,7 +636,7 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
 	then
 	  let m = morphism_table_find fleche_constr in
 	  let args = Array.of_list (create_args al a m.profil c1 c2) in  
-	    tclTHEN (change_in_concl new_concl)
+	    tclTHEN (change_in_concl None new_concl)
 	      (tclTHENS (apply (mkApp (m.lem, args)))
 		 ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[unfold_constr (ConstRef fleche_cp)]))
 (*		 ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[tclIDTAC])) *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 214064027..a09bfbd12 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -387,15 +387,16 @@ let glob_unfold ist (l,qid) = (l,glob_evaluable_or_metanum ist qid)
 let glob_flag ist red =
   { red with rConst = List.map (glob_evaluable_or_metanum ist) red.rConst }
 
-let glob_pattern ist (l,c) = (l,glob_constr ist c)
+let glob_constr_occurrence ist (l,c) = (l,glob_constr ist c)
 
 let glob_redexp ist = function
   | Unfold l -> Unfold (List.map (glob_unfold ist) l)
   | Fold l -> Fold (List.map (glob_constr ist) l)
   | Cbv f -> Cbv (glob_flag ist f)
   | Lazy f -> Lazy (glob_flag ist f)
-  | Pattern l -> Pattern (List.map (glob_pattern ist) l)
-  | (Red _ | Simpl | Hnf as r) -> r
+  | Pattern l -> Pattern (List.map (glob_constr_occurrence ist) l)
+  | Simpl o -> Simpl (option_app (glob_constr_occurrence ist) o)
+  | (Red _ | Hnf as r) -> r
   | ExtraRedExpr (s,c) -> ExtraRedExpr (s, glob_constr ist c)
 
 (* Interprets an hypothesis name *)
@@ -544,8 +545,9 @@ let rec glob_atomic lf ist = function
   (* Conversion *)
   | TacReduce (r,cl) ->
       TacReduce (glob_redexp ist r, List.map (glob_hyp_location ist) cl)
-  | TacChange (c,cl) ->
-      TacChange (glob_constr ist c, List.map (glob_hyp_location ist) cl)
+  | TacChange (occl,c,cl) ->
+      TacChange (option_app (glob_constr_occurrence ist) occl,
+        glob_constr ist c, List.map (glob_hyp_location ist) cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> TacReflexivity
@@ -1008,7 +1010,8 @@ let redexp_interp ist = function
   | Cbv f -> Cbv (flag_interp ist f)
   | Lazy f -> Lazy (flag_interp ist f)
   | Pattern l -> Pattern (List.map (pattern_interp ist) l)
-  | (Red _ | Simpl | Hnf as r) -> r
+  | Simpl o -> Simpl (option_app (pattern_interp ist) o)
+  | (Red _ |  Hnf as r) -> r
   | ExtraRedExpr (s,c) -> ExtraRedExpr (s,constr_interp ist c)
 
 let interp_may_eval f ist = function
@@ -1661,8 +1664,9 @@ and interp_atomic ist = function
   (* Conversion *)
   | TacReduce (r,cl) ->
       h_reduce (redexp_interp ist r) (List.map (interp_hyp_location ist) cl)
-  | TacChange (c,cl) ->
-      h_change (constr_interp ist c) (List.map (interp_hyp_location ist) cl)
+  | TacChange (occl,c,cl) ->
+      h_change (option_app (pattern_interp ist) occl)
+        (constr_interp ist c) (List.map (interp_hyp_location ist) cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7a2014ae1..6f79e9fcb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -142,7 +142,7 @@ type tactic_reduction = env -> evar_map -> constr -> constr
    certain hypothesis *)
 
 let reduct_in_concl redfun gl = 
-  convert_concl (pf_reduce redfun gl (pf_concl gl)) gl
+  convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) gl
 
 let reduct_in_hyp redfun idref gl =
   let inhyp,id = match idref with
@@ -151,12 +151,12 @@ let reduct_in_hyp redfun idref gl =
   let (_,c, ty) = pf_get_hyp gl id in
   let redfun' = under_casts (pf_reduce redfun gl) in
   match c with
-    | None -> convert_hyp (id,None,redfun' ty) gl
+    | None -> convert_hyp_no_check (id,None,redfun' ty) gl
     | Some b ->
 	if inhyp then (* Default for defs: reduce in body *)
-	  convert_hyp (id,Some (redfun' b),ty) gl
+	  convert_hyp_no_check (id,Some (redfun' b),ty) gl
 	else
-	  convert_hyp (id,Some b,redfun' ty) gl
+	  convert_hyp_no_check (id,Some b,redfun' ty) gl
 
 let reduct_option redfun = function
   | Some id -> reduct_in_hyp   redfun id 
@@ -166,34 +166,32 @@ let reduct_option redfun = function
    function has to be applied to the conclusion or
    to the hypotheses. *) 
 
-let in_combinator tac1 tac2 = function 
-  | [] -> tac1 
-  | x  -> (tclMAP tac2 x)
-	
 let redin_combinator redfun = function 
   | [] ->  reduct_in_concl redfun 
   | x  -> (tclMAP (reduct_in_hyp redfun) x)
 
 
 (* Now we introduce different instances of the previous tacticals *)
-let change_hyp_and_check t env sigma c =
-  if is_conv env sigma t c then 
+let change_and_check cv_pb t env sigma c =
+  if is_fconv cv_pb env sigma t c then 
     t
   else 
     errorlabstrm "convert-check-hyp" (str "Not convertible")
 
-let change_concl_and_check t env sigma c =
-  if is_conv_leq env sigma t c then 
-    t
-  else 
-    errorlabstrm "convert-check-concl" (str "Not convertible")
+(* Use cumulutavity only if changing the conclusion not a subterm *)
+let change_on_subterm cv_pb t = function
+  | None -> change_and_check cv_pb t
+  | Some occl -> contextually occl (change_and_check CONV t) 
 
-let change_in_concl t = reduct_in_concl (change_concl_and_check t)
-let change_in_hyp t   = reduct_in_hyp (change_hyp_and_check t)
+let change_in_concl occl t = reduct_in_concl (change_on_subterm CUMUL t occl) 
+let change_in_hyp occl t   = reduct_in_hyp (change_on_subterm CONV t occl)
 
-let change_option t = function
-  | Some id -> reduct_in_hyp   (change_hyp_and_check t) id
-  | None    -> reduct_in_concl (change_concl_and_check t) 
+let change occl c = function
+  | [] -> change_in_concl occl c
+  | l  -> 
+      if List.tl l <> [] & occl <> None then
+	error "No occurrences expected when changing several hypotheses";
+      tclMAP (change_in_hyp occl c) l
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl red_product
@@ -213,8 +211,6 @@ let unfold_in_hyp   loccname   = reduct_in_hyp   (unfoldn loccname)
 let unfold_option   loccname   = reduct_option   (unfoldn loccname) 
 let pattern_option l = reduct_option (pattern_occs l)
 
-let change c = in_combinator (change_in_concl c) (change_in_hyp c)
-
 (* A function which reduces accordingly to a reduction expression,
    as the command Eval does. *)
 
@@ -259,15 +255,13 @@ let id_of_name_with_default s = function
   | Anonymous -> id_of_string s
   | Name id   -> id
 
-let default_id gl =
-  match kind_of_term (strip_outer_cast (pf_concl gl)) with
-    | Prod (name,c1,c2) ->
-  	(match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl c1)) with
-	   | Sort (Prop _) -> (id_of_name_with_default "H" name)
-	   | Sort (Type _) -> (id_of_name_with_default "X" name)
-	   | _                   -> anomaly "Wrong sort")
-    | LetIn (name,b,_,_) -> id_of_name_using_hdchar (pf_env gl) b name
-    | _ -> raise (RefinerError IntroNeedsProduct)
+let default_id gl = function
+  | (name,None,t) ->
+      (match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl t)) with
+	| Sort (Prop _) -> (id_of_name_with_default "H" name)
+	| Sort (Type _) -> (id_of_name_with_default "X" name)
+	| _                   -> anomaly "Wrong sort")
+  | (name,Some b,_) -> id_of_name_using_hdchar (pf_env gl) b name
 
 (* Non primitive introduction tactics are treated by central_intro
    There is possibly renaming, with possibly names to avoid and 
@@ -278,31 +272,32 @@ type intro_name_flag =
   | IntroBasedOn of identifier * identifier list
   | IntroMustBe of identifier
 
+let find_name decl gl = function
+  | IntroAvoid idl        -> fresh_id idl (default_id gl decl) gl
+  | IntroBasedOn (id,idl) -> fresh_id idl id gl
+  | IntroMustBe id        -> 
+      let id' = fresh_id [] id gl in
+      if id' <> id then error ((string_of_id id)^" is already used");
+      id'
+
+let build_intro_tac id = function
+  | None      -> introduction id
+  | Some dest -> tclTHEN (introduction id) (move_hyp true id dest)
+
 let rec intro_gen name_flag move_flag force_flag gl =
-  try
-    let id =
-      match name_flag with
-        | IntroAvoid idl        -> fresh_id idl (default_id gl) gl
-        | IntroBasedOn (id,idl) -> fresh_id idl id gl
-        | IntroMustBe id        -> 
-	    let id' = fresh_id [] id gl in
-  	    if id' <> id then error ((string_of_id id)^" is already used");
-	    id'
-    in
-    begin match move_flag with
-      | None      -> introduction id gl
-      | Some dest -> tclTHEN (introduction id) (move_hyp true id dest) gl
-    end
-  with RefinerError IntroNeedsProduct as e ->
-    if force_flag then
-      try
-        ((tclTHEN (reduce (Red true) [])
-	    (intro_gen name_flag move_flag force_flag)) gl)
-      with Redelimination ->
-        errorlabstrm "Intro" 
-	  (str "No product even after head-reduction")
-    else
-      raise e
+  match kind_of_term (pf_concl gl) with
+    | Prod (name,t,_) -> 
+	build_intro_tac (find_name (name,None,t) gl name_flag) move_flag gl
+    | LetIn (name,b,t,_) ->
+	build_intro_tac (find_name (name,Some b,t) gl name_flag) move_flag gl
+    | _ -> 
+	if not force_flag then raise (RefinerError IntroNeedsProduct);
+	try
+	  tclTHEN
+	    (reduce (Red true) [])
+	    (intro_gen name_flag move_flag force_flag) gl
+	with Redelimination ->
+	  errorlabstrm "Intro" (str "No product even after head-reduction")
 
 let intro_mustbe_force id = intro_gen (IntroMustBe id) None true
 let intro_using id = intro_gen (IntroBasedOn (id,[])) None false
@@ -446,7 +441,7 @@ let bring_hyps hyps =
     (fun gl ->
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
       let f = mkCast (mkMeta (new_meta()),newcl) in
-      refine (mkApp (f, instance_from_named_context hyps)) gl)
+      refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
 
 (* Resolution with missing arguments *)
 
@@ -479,7 +474,6 @@ let apply_with_bindings (c,lbind) gl =
     let clause = make_clenv_binding_apply wc (-1) (c,thm_ty0) lbind in 
     apply kONT clause gl
 
-
 let apply c = apply_with_bindings (c,NoBindings)
 
 let apply_list = function 
@@ -739,23 +733,23 @@ let exact_check c gl =
   let concl = (pf_concl gl) in
   let ct = pf_type_of gl c in
   if pf_conv_x_leq gl ct concl then  
-    refine c gl 
+    refine_no_check c gl 
   else 
     error "Not an exact proof"
 
-let exact_no_check = refine
+let exact_no_check = refine_no_check
 
 let exact_proof c gl =
   (* on experimente la synthese d'ise dans exact *)
   let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
-  in refine c gl 
+  in refine_no_check c gl 
 
 let (assumption : tactic) = fun gl ->
   let concl =  pf_concl gl in 
   let rec arec = function
     | [] -> error "No such assumption"
     | (id,c,t)::rest -> 
-	if pf_conv_x_leq gl t concl then refine (mkVar id) gl
+	if pf_conv_x_leq gl t concl then refine_no_check (mkVar id) gl
 	else arec rest
   in
   arec (pf_hyps gl)
@@ -770,7 +764,7 @@ let (assumption : tactic) = fun gl ->
  * goal. *)                                                               
 
 let clear ids gl = (* avant seul dyn_clear n'echouait pas en [] *)
-  if ids=[] then tclIDTAC gl else thin ids gl
+  if ids=[] then tclIDTAC gl else with_check (thin ids) gl
 
 let clear_body = thin_body
 
@@ -822,7 +816,7 @@ let constructor_tac boundopt i lbind gl =
   end;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
   let apply_tac = apply_with_bindings (cons,lbind) in
-  (tclTHENLIST [convert_concl redcl; intros; apply_tac]) gl
+  (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl
 
 let one_constructor i = constructor_tac None i
 
@@ -956,7 +950,7 @@ let elimination_in_clause_scheme kONT id elimclause indclause =
       [ (* Try to insert the new hyp at the same place *)
         tclORELSE (intro_replacing id)
           (tclTHEN (clear [id]) (introduction id));
-        refine new_hyp_prf])
+        refine_no_check new_hyp_prf])
 
 let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl = 
   let (wc,kONT)  = startWalk gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 2e35c1761..29107c32a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -93,8 +93,8 @@ val try_intros_until :
 
 (*s Exact tactics. *)
 
-val assumption         : tactic
-val exact_no_check      : constr -> tactic
+val assumption       : tactic
+val exact_no_check   : constr -> tactic
 val exact_check      : constr -> tactic
 val exact_proof      : Topconstr.constr_expr -> tactic
 
@@ -105,10 +105,9 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
 val reduct_option     : tactic_reduction -> hyp_location option -> tactic
 val reduct_in_concl   : tactic_reduction -> tactic
-val change_in_concl   : constr -> tactic
-
-val change_in_hyp     : constr -> hyp_location -> tactic
-val change_option     : constr -> hyp_location option -> tactic
+val change_in_concl   : constr occurrences option -> constr -> tactic
+val change_in_hyp     : constr occurrences option -> constr -> hyp_location ->
+  tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location        -> tactic
 val red_option        : hyp_location option -> tactic
@@ -128,7 +127,8 @@ val unfold_option     :
   (int list * evaluable_global_reference) list -> hyp_location option
     -> tactic
 val reduce            : red_expr -> hyp_location list -> tactic
-val change            : constr -> hyp_location list -> tactic
+val change            :
+  constr occurrences option -> constr -> hyp_location list -> tactic
 
 val unfold_constr     : global_reference -> tactic
 val pattern_option  : (int list * constr) list -> hyp_location option -> tactic
@@ -136,7 +136,6 @@ val pattern_option  : (int list * constr) list -> hyp_location option -> tactic
 (*s Modification of the local context. *)
 
 val clear         : identifier list -> tactic
-
 val clear_body    : identifier list -> tactic
 
 val new_hyp       : int option ->constr -> constr substitution -> tactic