From 01feb4206d26b41bfaab9bd45a7b2fc4db569baf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 23 Sep 2014 18:57:08 +0200
Subject: Fix bug in setoid_rewrite introduced by PMP's commits, which was
 creating two versions of the rewriting lemma, keeping useless evars around.
 This can now happen only when the rewrite lemma is used under binders... Fix
 to do next.

---
 tactics/rewrite.ml | 45 ++++++++++++++++++++++++++++++++++-----------
 1 file changed, 34 insertions(+), 11 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 525cfd7346..3feda7b14f 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -462,6 +462,7 @@ type hypinfo = {
   c1 : constr;
   c2 : constr;
   c  : (Tacinterp.interp_sign * Tacexpr.glob_constr_and_expr with_bindings) option;
+  to_refresh : bool;
 }
 
 let get_symmetric_proof b = 
@@ -497,7 +498,7 @@ let decompose_applied_relation env sigma orig (c,l) =
 	let value = Clenv.clenv_value eqclause in
 	  Some (eqclause.evd, { cl=eqclause; prf=value;
 		 car=ty1; rel = equiv; sort = Sorts.is_prop sort;
-		 c1=c1; c2=c2; c=orig; })
+		 c1=c1; c2=c2; c=orig; to_refresh = false})
   in
     match find_rel ctype with
     | Some c -> c
@@ -592,8 +593,16 @@ let general_rewrite_unif_flags () =
 
 let refresh_hypinfo env sigma hypinfo =
     match hypinfo.c with
-    | Some c ->
-      (* Refresh the clausenv to not get the same meta twice in the goal. *)
+    | Some c when hypinfo.to_refresh ->
+      (* Refresh the clausenv to not get the same meta twice in the goal
+	 and be able to capture binders under them *)
+      decompose_applied_relation_expr env sigma c
+    | Some c when hypinfo.cl.env != env ->
+      	(* If the lemma actually generates existential variables, we cannot 
+	   use it here as it will polute the evar map with existential variables
+	   that might not ever get instantiated (e.g. if we rewrite under a binder
+	   and need to refresh [c] again) *)
+       (* TODO: remove bindings in sigma corresponding to c *)
       decompose_applied_relation_expr env sigma c
     | _ ->
       let cl = { hypinfo.cl with evd = sigma } in
@@ -687,7 +696,7 @@ let unify_eqn l2r flags env (sigma, cstrs) hypinfo by t =
     let rew_prf = RewPrf (rel, prf) in
     let rew = { rew_evars; rew_prf; rew_car; rew_from = c1; rew_to = c2; } in
     let rew = if l2r then rew else symmetry env hypinfo.sort rew in
-    Some (hypinfo, rew)
+    Some ({ hypinfo with to_refresh = true}, rew)
   with 
   | e when Class_tactics.catchable e -> None
   | Reduction.NotConvertible -> None
@@ -828,17 +837,16 @@ let apply_rule unify loccs : ('a * int) pure_strategy =
       let unif = unify hypinfo env evars t in
 	match unif with
 	| None -> ((hypinfo, occ), Fail)
-        | Some (hypinfo, rew) ->
+        | Some (hypinfo', rew) ->
 	  let occ = succ occ in
-	  let res = 
-	    if not (is_occ occ) then Fail
-	    else if eq_constr t rew.rew_to then Identity
+	    if not (is_occ occ) then ((hypinfo, occ), Fail)
+	    else if eq_constr t rew.rew_to then ((hypinfo, occ), Identity)
 	    else
 	      let res = { rew with rew_car = ty } in
               let rel, prf = get_rew_prf res in
-              Success (apply_constraint env avoid rew.rew_car rel prf cstr res)
-	  in ((hypinfo, occ), res)
-	    
+	      let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in
+		((hypinfo', occ), res)
+		  
 let apply_lemma l2r flags oc by loccs : strategy =
   fun () env avoid t ty cstr (sigma, cstrs) ->
     let sigma, c = oc sigma in
@@ -1360,9 +1368,24 @@ let get_hypinfo_ids {c = opt} =
   | Some (is, gc) ->
     let avoid = Option.default [] (TacStore.get is.extra f_avoid_ids) in
       Id.Map.fold (fun id _ accu -> id :: accu) is.lfun avoid
+
+(** A dummy initial clauseenv to avoid generating initial evars before
+    even finding a first application of the rewriting lemma, in setoid_rewrite
+    mode *)
+
+let init_hypinfo env sigma c = 
+  { cl = { env = env; evd = sigma; templval = mk_freelisted mkProp; 
+	   templtyp = mk_freelisted mkProp };
+    prf = mkProp; car = mkProp; rel = mkProp; sort = true; c1 = mkProp; c2 = mkProp; 
+    c = c; to_refresh = true }
       
 let rewrite_with l2r flags c occs : strategy =
   fun () env avoid t ty cstr (sigma, cstrs) ->
+    (** FIXME: This is wrong... the evars in c should not register to the global sigma
+	as the hypothesis might need to be refreshed, e.g. to rewrite under binders
+	and the initial version will not be used while its evars will appear in 
+	the final sigma. Leaving for now to not impact performance, but should be
+	fixed using matching with patterns to avoid costly retypings instead. *)
     let sigma, hypinfo = decompose_applied_relation_expr env sigma c in
     let avoid = get_hypinfo_ids hypinfo @ avoid in
     let unify hypinfo env evars t = unify_eqn l2r flags env evars hypinfo None t in
-- 
cgit v1.2.3