Port [rewrite] tactics to open terms. Currently no check that evars

introduced by the lemma remain in the subgoals (i.e. it's really
[erewrite]).


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

7 files changed, 65 insertions, 73 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bda1fabbc..e051d1aad 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -66,13 +66,13 @@ let intersects s t =
 
 open Auto
 
-let e_give_exact c gl = 
+let e_give_exact flags c gl = 
   let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
-  if occur_existential t1 or occur_existential t2 then 
-     tclTHEN (Clenvtac.unify t1) (exact_check c) gl
-  else exact_check c gl
-
-let assumption id = e_give_exact (mkVar id)
+    if occur_existential t1 or occur_existential t2 then 
+      tclTHEN (Clenvtac.unify (* ~flags *) t1) (exact_check c) gl
+    else exact_check c gl
+      
+let assumption flags id = e_give_exact flags (mkVar id)
 
 open Unification
 
@@ -130,7 +130,7 @@ and e_my_find_search db_list local_db hdc concl =
 	match t with
 	  | Res_pf (term,cl) -> unify_resolve flags (term,cl)
 	  | ERes_pf (term,cl) -> unify_e_resolve flags (term,cl)
-	  | Give_exact (c) -> e_give_exact c
+	  | Give_exact (c) -> e_give_exact flags c
 	  | Res_pf_THEN_trivial_fail (term,cl) ->
               tclTHEN (unify_e_resolve flags (term,cl)) 
 		(e_trivial_fail_db db_list local_db)
@@ -812,6 +812,8 @@ let unify_eqn env sigma hypinfo t =
 		let mvs = clenv_dependent false env' in
 		  clenv_pose_metas_as_evars env' mvs
 	      in
+	      let evd' = Typeclasses.resolve_typeclasses ~fail:false env'.env env'.evd in
+	      let env' = { env' with evd = evd' } in
 	      let c1 = Clenv.clenv_nf_meta env' c1
 	      and c2 = Clenv.clenv_nf_meta env' c2
 	      and car = Clenv.clenv_nf_meta env' car
@@ -833,7 +835,7 @@ let unify_eqn env sigma hypinfo t =
 		let mvs = clenv_dependent false env' in
 		  clenv_pose_metas_as_evars env' mvs
 	      in
-	      let evd' = Typeclasses.resolve_typeclasses env'.env env'.evd in
+	      let evd' = Typeclasses.resolve_typeclasses ~fail:false env'.env env'.evd in
 	      let env' = { env' with evd = evd' } in
 	      let nf c = Evarutil.nf_evar (Evd.evars_of evd') (Clenv.clenv_nf_meta env' c) in
 	      let c1 = nf c1 and c2 = nf c2
@@ -1066,16 +1068,16 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
 		      mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
 		in
 		  cut_replacing id newt 
-		    (fun x -> Tactics.refine (mkApp (term, [| mkVar id |])))
+		    (fun x -> Tacmach.refine_no_check (mkApp (term, [| mkVar id |])))
 	    | None -> 
 		(match abs with
 		| None -> 
 		    let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
 		      tclTHENLAST
 			(Tacmach.internal_cut_no_check false name newt)
-			(tclTHEN (Tactics.revert [name]) (Tactics.refine p))
+			(tclTHEN (Tactics.revert [name]) (Tacmach.refine_no_check p))
 		| Some (t, ty) -> 
-		    Tactics.refine
+		    Tacmach.refine_no_check
 		      (mkApp (mkLambda (Name (id_of_string "newt"), newt,
 				       mkLambda (Name (id_of_string "lemma"), ty,
 						mkApp (p, [| mkRel 2 |]))),
@@ -1584,27 +1586,27 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
     {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
 
 let get_hyp gl c clause l2r = 
-  let hi = decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r in
+  let hi = decompose_setoid_eqhyp (pf_env gl) (fst c) (snd c) l2r in
   let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
     unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
 	
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
 
-let general_s_rewrite l2r occs c ~new_goals gl =
-  let meta = Evarutil.new_meta() in
-  let hypinfo = ref (get_hyp gl c None l2r) in
-    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs None gl
-
-let general_s_rewrite_in id l2r occs c ~new_goals gl =
+let general_s_rewrite cl l2r occs c ~new_goals gl =
   let meta = Evarutil.new_meta() in
-  let hypinfo = ref (get_hyp gl c (Some id) l2r) in
-    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs (Some (([],id), [])) gl
+  let hypinfo = ref (get_hyp gl c cl l2r) in
+  let cl' = Option.map (fun id -> (([],id), [])) cl in
+    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs cl' gl
+(*     if fst c = Evd.empty || fst c == project gl then tac gl *)
+(*     else *)
+(*       let evars = Evd.merge (fst c) (project gl) in *)
+(* 	tclTHEN (Refiner.tclEVARS evars) tac gl *)
 
 let general_s_rewrite_clause x =
   init_setoid ();
   match x with
-    | None -> general_s_rewrite
-    | Some id -> general_s_rewrite_in id
+    | None -> general_s_rewrite None
+    | Some id -> general_s_rewrite (Some id)
 	
 let _ = Equality.register_general_setoid_rewrite_clause general_s_rewrite_clause
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9994bd784..cbcf5993c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -43,6 +43,7 @@ open Indrec
 open Printer
 open Clenv
 open Clenvtac
+open Evd
 
 (* Rewriting tactics *)
 
@@ -55,16 +56,17 @@ open Clenvtac
 *)
 
 (* Ad hoc asymmetric general_elim_clause *)
-let general_elim_clause with_evars cls c elim = 
+let general_elim_clause with_evars cls sigma c l elim = 
   try 
     (match cls with
       | None ->
 	  (* was tclWEAK_PROGRESS which only fails for tactics generating one 
              subgoal and did not fail for useless conditional rewritings generating
              an extra condition *)
-	  tclNOTSAMEGOAL (general_elim with_evars c elim ~allow_K:false)
+	  tclNOTSAMEGOAL (tclTHEN (Refiner.tclEVARS sigma)
+			     (general_elim with_evars (c,l) elim ~allow_K:false))
       | Some id ->
-	  general_elim_in with_evars id c elim)
+	  tclTHEN (Refiner.tclEVARS sigma) (general_elim_in with_evars id (c,l) elim))
   with Pretype_errors.PretypeError (env,
 				   (Pretype_errors.NoOccurrenceFound (c', _))) ->
     raise (Pretype_errors.PretypeError
@@ -81,11 +83,7 @@ let elimination_sort_of_clause = function
   If occurrences are set, use setoid_rewrite.
 *)
 
-let general_s_rewrite_clause = function
-  | None -> general_s_rewrite
-  | Some id -> general_s_rewrite_in id
-
-let general_setoid_rewrite_clause = ref general_s_rewrite_clause
+let general_setoid_rewrite_clause = ref (fun _ -> assert false)
 let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause
 
 let is_applied_setoid_relation = ref (fun _ -> false)
@@ -96,7 +94,7 @@ let is_applied_relation t =
   | App (c, args) when Array.length args >= 2 -> true
   | _ -> false
 
-let leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl =
+let leibniz_rewrite_ebindings_clause cls lft2rgt sigma c l with_evars gl hdcncl =
   let hdcncls = string_of_inductive hdcncl in 
   let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
   let dir = if cls=None then lft2rgt else not lft2rgt in
@@ -105,21 +103,22 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl =
     try pf_global gl (id_of_string rwr_thm)
     with Not_found ->
       error ("Cannot find rewrite principle "^rwr_thm^".")
-  in general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
+  in general_elim_clause with_evars cls sigma c l (elim,NoBindings) gl
 
 let leibniz_eq = Lazy.lazy_from_fun build_coq_eq
 
-let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
+let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_bindings) with_evars gl =
   if occs <> all_occurrences then (
     !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
   else
-    let ctype = pf_apply get_type_of gl c in 
     let env = pf_env gl in
-    let sigma = project gl in 
+    let sigma, c' = c in
+    let sigma = Evd.merge sigma (project gl) in
+    let ctype = get_type_of env sigma c' in 
     let rels, t = decompose_prod (whd_betaiotazeta ctype) in
       match match_with_equation t with
       | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *)
-	  leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl
+	  leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl
       | None ->
 	  let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in
 	  let _,t' = splay_prod env' sigma t in (* Search for underlying eq *)
@@ -128,7 +127,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
 		if l = NoBindings && !is_applied_setoid_relation t then
 		  !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
 		else
-		  (try leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl
+		  (try leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl
 		    with e -> 
 		      try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
 		      with _ -> raise e)
@@ -140,7 +139,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
 let general_rewrite_ebindings = 
   general_rewrite_ebindings_clause None
 let general_rewrite_bindings l2r occs (c,bl) = 
-  general_rewrite_ebindings_clause None l2r occs (c,inj_ebindings bl)
+  general_rewrite_ebindings_clause None l2r occs (inj_open c,inj_ebindings bl)
 
 let general_rewrite l2r occs c =
   general_rewrite_bindings l2r occs (c,NoBindings) false
@@ -148,9 +147,9 @@ let general_rewrite l2r occs c =
 let general_rewrite_ebindings_in l2r occs id =
   general_rewrite_ebindings_clause (Some id) l2r occs
 let general_rewrite_bindings_in l2r occs id (c,bl) =
-  general_rewrite_ebindings_clause (Some id) l2r occs (c,inj_ebindings bl)
+  general_rewrite_ebindings_clause (Some id) l2r occs (inj_open c,inj_ebindings bl)
 let general_rewrite_in l2r occs id c = 
-  general_rewrite_ebindings_clause (Some id) l2r occs (c,NoBindings)
+  general_rewrite_ebindings_clause (Some id) l2r occs (inj_open c,NoBindings)
 
 let general_multi_rewrite l2r with_evars c cl = 
   let occs_of = on_snd (List.fold_left 
@@ -186,7 +185,7 @@ let general_multi_rewrite l2r with_evars c cl =
 	let do_hyps gl = 
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
 	  let ids = 
-	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
+	    let ids_in_c = Environ.global_vars_set (Global.env()) (snd (fst c)) in
 	      Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl)
 	  in do_hyps_atleastonce ids gl
 	in 
@@ -265,7 +264,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id -> 
 	tclTHEN 
-	  (tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause))
+	  (tclTRY (general_multi_rewrite false false (inj_open (mkVar id),NoBindings) clause))
 	  (clear [id]));
        tclFIRST
 	 [assumption;
@@ -1275,7 +1274,7 @@ let rewrite_multi_assumption_cond cond_eq_term cl gl =
 	begin 
 	  try 
 	    let dir = cond_eq_term t gl in 
-	    general_multi_rewrite dir false (mkVar id,NoBindings) cl gl
+	    general_multi_rewrite dir false (inj_open (mkVar id),NoBindings) cl gl
 	  with | Failure _ | UserError _ -> arec rest
 	end
   in 
@@ -1335,14 +1334,4 @@ let replace_term_in_right t hyp = replace_multi_term (Some false) t (Tacticals.o
 
 let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp)
 
-
-
-
-
-
-
-
-
-let _ = Setoid_replace.register_replace (fun tac_opt c2 c1 gl ->  replace_in_clause_maybe_by c2 c1 onConcl tac_opt gl)
-let _ = Setoid_replace.register_general_rewrite general_rewrite
 let _ = Tactics.register_general_multi_rewrite general_multi_rewrite
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 7aeb7af37..df59867bb 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -45,7 +45,7 @@ val rewriteRL   : constr  -> tactic
 
 val register_general_setoid_rewrite_clause :
   (identifier option -> bool ->
-    occurrences -> constr -> new_goals:constr list -> tactic) -> unit
+    occurrences -> open_constr -> new_goals:constr list -> tactic) -> unit
 val register_is_applied_setoid_relation : (constr -> bool) -> unit
 
 val general_rewrite_bindings_in :
@@ -54,14 +54,14 @@ val general_rewrite_in          :
   bool -> occurrences -> identifier -> constr -> evars_flag -> tactic
 
 val general_multi_rewrite : 
-  bool -> evars_flag -> constr with_ebindings -> clause -> tactic
+  bool -> evars_flag -> open_constr with_bindings -> clause -> tactic
 val general_multi_multi_rewrite : 
-  evars_flag -> (bool * multi * constr with_ebindings) list -> clause -> 
+  evars_flag -> (bool * multi * open_constr with_bindings) list -> clause -> 
   tactic option -> tactic
 
-val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic
+val conditional_rewrite : bool -> tactic -> open_constr with_bindings -> tactic
 val conditional_rewrite_in :
-  bool -> identifier -> tactic -> constr with_ebindings -> tactic
+  bool -> identifier -> tactic -> open_constr with_bindings -> tactic
 
 val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
 val replace    : constr -> constr -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 9d73cf75f..845483436 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -18,6 +18,7 @@ open Mod_subst
 open Names
 open Tacexpr
 open Rawterm
+open Tactics
 
 (* Equality *)
 open Equality
@@ -133,10 +134,10 @@ let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings)
 
 TACTIC EXTEND conditional_rewrite
 | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ]
-    -> [ conditional_rewrite b (snd tac) c ]
+    -> [ conditional_rewrite b (snd tac) (inj_open (fst c), snd c) ]
 | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c)
     "in" hyp(h) ]
-    -> [ conditional_rewrite_in b h (snd tac) c ]
+    -> [ conditional_rewrite_in b h (snd tac) (inj_open (fst c), snd c) ]
 END
 
 TACTIC EXTEND dependent_rewrite
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 063f387ac..e89672e51 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2297,7 +2297,7 @@ and interp_atomic ist gl = function
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) -> 
       Equality.general_multi_multi_rewrite ev
-	(List.map (fun (b,m,c) -> (b,m,interp_constr_with_bindings ist gl c)) l)
+	(List.map (fun (b,m,c) -> (b,m,interp_open_constr_with_bindings ist gl c)) l)
 	(interp_clause ist gl cl)
 	(Option.map (interp_tactic ist) by)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 047cb0b74..e0f5a3a42 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -535,6 +535,13 @@ let bring_hyps hyps =
       let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in
       refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
 
+let resolve_classes gl =
+  let env = pf_env gl and evd = project gl in
+    if evd = Evd.empty then tclIDTAC gl
+    else
+      let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
+	(tclTHEN (tclEVARS (Evd.evars_of evd')) tclNORMEVAR) gl
+
 (**************************)
 (*     Cut tactics        *)
 (**************************)
@@ -719,13 +726,6 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 (*            Resolution tactics                    *)
 (****************************************************)
 
-let resolve_classes gl =
-  let env = pf_env gl and evd = project gl in
-    if evd = Evd.empty then tclIDTAC gl
-    else
-      let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
-	(tclTHEN (tclEVARS (Evd.evars_of evd')) tclNORMEVAR) gl
-
 (* Resolution with missing arguments *)
 
 let general_apply with_delta with_destruct with_evars (c,lbind) gl =
@@ -1172,8 +1172,8 @@ let rec intros_patterns b avoid thin destopt = function
       tclTHEN 
         (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
         (onLastHyp (fun id ->
-	  tclTHENLIST [
-	    !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) 
+	  tclTHENLIST [ 
+	    !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings)
 	      allClauses;
 	    clear_if_atomic l2r id;
 	    intros_patterns b avoid thin destopt l ]))
@@ -1200,7 +1200,7 @@ let prepare_intros s (loc,ipat) gl = match ipat with
   | IntroWildcard -> let id = make_id s gl in id, clear_wildcards [dloc,id]
   | IntroRewrite l2r -> 
       let id = make_id s gl in
-      id, !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allClauses
+      id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
   | IntroOrAndPattern ll -> make_id s gl, 
       intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
 
@@ -1231,7 +1231,7 @@ let true_cut = assert_tac true
 
 let as_tac id ipat = match ipat with
   | Some (loc,IntroRewrite l2r) -> 
-      !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allClauses
+      !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
   | Some (loc,IntroOrAndPattern ll) ->
       intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
   | Some (loc,
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 589be18c8..f18860af4 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -366,4 +366,4 @@ val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic
 val dependent_pattern : constr -> tactic
 
 val register_general_multi_rewrite : 
-  (bool -> evars_flag -> constr with_ebindings -> clause -> tactic) -> unit
+  (bool -> evars_flag -> open_constr with_bindings -> clause -> tactic) -> unit