More invariants in the code of Refine.

The hypinfo state is now refreshed at a proper time, which should reduce the
overall number of calls to [decompose_applied_relation]. The state passing
nature of the program is also more explicit, removing a use of Evd.merge.
This patch should preserve semantics and efficiency.

1 files changed, 25 insertions, 39 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ed06f5162b..6c62f8d8c3 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -482,11 +482,10 @@ let rec decompose_app_rel env evd t =
 	in (f'', args)
   | _ -> error "The term provided is not an applied relation."
 
-let decompose_applied_relation ?(diff=true) env origsigma sigma orig (c,l) =
-  let c' = c in
-  let ctype = Retyping.get_type_of env sigma c' in
+let decompose_applied_relation env sigma orig (c,l) =
+  let ctype = Retyping.get_type_of env sigma c in
   let find_rel ty =
-    let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c',ty) l in
+    let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c,ty) l in
     let (equiv, args) = decompose_app_rel env eqclause.evd (Clenv.clenv_type eqclause) in
     let c1 = args.(0) and c2 = args.(1) in 
     let ty1, ty2 =
@@ -496,13 +495,9 @@ let decompose_applied_relation ?(diff=true) env origsigma sigma orig (c,l) =
       else
 	let sort = sort_of_rel env eqclause.evd equiv in
 	let value = Clenv.clenv_value eqclause in
-	let eqclause =
-	  if diff then { eqclause with evd = Evd.diff eqclause.evd origsigma } 
-	  else eqclause 
-	in
-	  Some { cl=eqclause; prf=value;
+	  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; })
   in
     match find_rel ctype with
     | Some c -> c
@@ -513,8 +508,8 @@ let decompose_applied_relation ?(diff=true) env origsigma sigma orig (c,l) =
 	| None -> error "The term does not end with an applied homogeneous relation."
 
 let decompose_applied_relation_expr env sigma (is, (c,l)) =
-  let sigma', cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in
-    decompose_applied_relation env sigma sigma' (Some (is, (c,l))) cbl
+  let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in
+    decompose_applied_relation env sigma (Some (is, (c,l))) cbl
 
 let rewrite_db = "rewrite"
 
@@ -596,16 +591,17 @@ let general_rewrite_unif_flags () =
 
 
 let refresh_hypinfo env sigma hypinfo =
-  let {c=c} = hypinfo in
-    match c with
+    match hypinfo.c with
     | Some c ->
       (* Refresh the clausenv to not get the same meta twice in the goal. *)
       decompose_applied_relation_expr env sigma c
-    | _ -> hypinfo
-      
+    | _ ->
+      let cl = { hypinfo.cl with evd = sigma } in
+      sigma, { hypinfo with cl }
+
 let solve_remaining_by by env prf =
   match by with
-  | None -> env, prf
+  | None -> env.evd, prf
   | Some tac ->
     let indep = clenv_independent env in
     let tac = eval_tactic tac in
@@ -616,7 +612,7 @@ let solve_remaining_by by env prf =
 	let evd = Evd.set_universe_context evd ctx' in
 	  meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
       indep env.evd
-    in { env with evd = evd' }, prf
+    in evd', prf
 
 let no_constraints cstrs = 
   fun ev _ -> not (Evar.Set.mem ev cstrs)
@@ -670,22 +666,16 @@ let symmetry env sort rew =
 let unify_eqn l2r flags env (sigma, cstrs) hypinfo by t =
   if isEvar t then None else 
   try
-    let hypinfo =
-      if eq_env hypinfo.cl.env env then hypinfo
-      else refresh_hypinfo env sigma hypinfo
-    in
+    let sigma, hypinfo = refresh_hypinfo env sigma hypinfo in
     let {cl=cl; prf=prf; car=car; rel=rel; c1=c1; c2=c2; c=c;} = 
       hypinfo in
     let left = if l2r then c1 else c2 in
-    let evd' = Evd.merge sigma cl.evd in
-    let cl = { cl with evd = evd' } in
     let env' = clenv_unify ~flags CONV left t cl in
     let env' = Clenvtac.clenv_pose_dependent_evars true env' in
     let evd' = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
       ~fail:true env env'.evd in
     let env' = { env' with evd = evd' } in
-    let env', prf = solve_remaining_by by env' (Clenv.clenv_value env') in
-    let evd = env'.evd in
+    let evd, prf = solve_remaining_by by env' (Clenv.clenv_value env') in
     let nf c = Evarutil.nf_evar evd (Reductionops.nf_meta evd c) in
     let c1 = nf c1 and c2 = nf c2
     and rew_car = nf car and rel = nf rel
@@ -693,7 +683,6 @@ let unify_eqn l2r flags env (sigma, cstrs) hypinfo by t =
     let ty1 = Retyping.get_type_of env evd c1 in
     let ty2 = Retyping.get_type_of env evd c2 in
     let () = if not (convertible env evd ty2 ty1) then raise Reduction.NotConvertible in
-    let hypinfo = refresh_hypinfo env evd hypinfo in
     let rew_evars = evd, cstrs in
     let rew_prf = RewPrf (rel, prf) in
     let rew = { rew_evars; rew_prf; rew_car; rew_from = c1; rew_to = c2; } in
@@ -851,15 +840,13 @@ let apply_rule unify loccs : ('a * int) pure_strategy =
 	  in ((hypinfo, occ), res)
 	    
 let apply_lemma l2r flags (evm,c) by loccs : strategy =
-  fun () env avoid t ty cstr evars ->
-    let hypinfo = 
-      let evars' = Evd.merge (goalevars evars) evm in
-	decompose_applied_relation env (goalevars evars) evars'
-	  None c
-    in
+  fun () env avoid t ty cstr (sigma, cstrs) ->
+    let sigma = Evd.merge sigma evm in
+    let sigma, hypinfo = decompose_applied_relation env sigma None c in
+    let evars = (sigma, cstrs) in
     let unify hypinfo env evars t = unify_eqn l2r flags env evars hypinfo by t in
     let _, res = apply_rule unify loccs (hypinfo,0) env avoid t ty cstr evars in
-      (), res
+    (), res
 
 let e_app_poly env evars f args =
   let evars', c = app_poly_nocheck env !evars f args in
@@ -1375,9 +1362,8 @@ let get_hypinfo_ids {c = opt} =
       Id.Map.fold (fun id _ accu -> id :: accu) is.lfun avoid
       
 let rewrite_with l2r flags c occs : strategy =
-  fun () env avoid t ty cstr evars ->
-    let gevars = goalevars evars in
-    let hypinfo = decompose_applied_relation_expr env gevars c in
+  fun () env avoid t ty cstr (sigma, cstrs) ->
+    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
     let app = apply_rule unify occs in
@@ -1385,7 +1371,7 @@ let rewrite_with l2r flags c occs : strategy =
       Strategies.fix (fun aux -> 
 	Strategies.choice app (subterm true default_flags aux))
     in
-    let _, res = strat (hypinfo, 0) env avoid t ty cstr (gevars, cstrevars evars) in
+    let _, res = strat (hypinfo, 0) env avoid t ty cstr (sigma, cstrs) in
       ((), res)
 
 let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
@@ -1970,7 +1956,7 @@ let unification_rewrite l2r c1 c2 cl car rel but env =
 let get_hyp gl (c,l) clause l2r =
   let evars = project gl in
   let env = pf_env gl in
-  let hi = decompose_applied_relation ~diff:false env evars evars None (c,l) in
+  let _, hi = decompose_applied_relation env evars None (c,l) in
   let but = match clause with
     | Some id -> pf_get_hyp_typ gl id 
     | None -> Evarutil.nf_evar evars (pf_concl gl)