Introducing a local flag to hypothesis conversion function.

If the reduction function is known not to depend on the named context,
then we can perform it in parallel on the various variables.

1 files changed, 49 insertions, 13 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 869e3039ab..ecb8c9dc1f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -718,23 +718,56 @@ let e_change_in_hyp ~check ~reorder redfun (id,where) =
     (convert_hyp ~check ~reorder c)
   end
 
+type hyp_conversion =
+| AnyHypConv (** Arbitrary conversion *)
+| StableHypConv (** Does not introduce new dependencies on variables *)
+| LocalHypConv (** Same as above plus no dependence on the named environment *)
+
 let e_change_in_hyps ~check ~reorder f args =
   Proofview.Goal.enter begin fun gl ->
-    let fold (env, sigma) arg =
-      let (id, redfun) = f arg in
-      let hyp =
-        try lookup_named id env
-        with Not_found ->
-          raise (RefinerError (env, sigma, NoSuchHyp id))
+    let env = Proofview.Goal.env gl in
+    let sigma = Tacmach.New.project gl in
+    let (env, sigma) = match reorder with
+    | LocalHypConv ->
+      (* If the reduction function is known not to depend on the named
+          context, then we can perform it in parallel. *)
+      let fold accu arg =
+        let (id, redfun) = f arg in
+        let old = try Id.Map.find id accu with Not_found -> [] in
+        Id.Map.add id (redfun :: old) accu
+      in
+      let reds = List.fold_left fold Id.Map.empty args in
+      let evdref = ref sigma in
+      let map d =
+        let id = NamedDecl.get_id d in
+        match Id.Map.find id reds with
+        | reds ->
+          let d = EConstr.of_named_decl d in
+          let fold redfun (sigma, d) = redfun env sigma d in
+          let (sigma, d) = List.fold_right fold reds (sigma, d) in
+          let () = evdref := sigma in
+          EConstr.Unsafe.to_named_decl d
+        | exception Not_found -> d
       in
-      let (sigma, d) = redfun env sigma hyp in
-      let sign = Logic.convert_hyp ~check ~reorder env sigma d in
+      let sign = Environ.map_named_val map (Environ.named_context_val env) in
       let env = reset_with_named_context sign env in
-      (env, sigma)
+      (env, !evdref)
+    | StableHypConv | AnyHypConv ->
+      let reorder = reorder == AnyHypConv in
+      let fold (env, sigma) arg =
+        let (id, redfun) = f arg in
+        let hyp =
+          try lookup_named id env
+          with Not_found ->
+            raise (RefinerError (env, sigma, NoSuchHyp id))
+        in
+        let (sigma, d) = redfun env sigma hyp in
+        let sign = Logic.convert_hyp ~check ~reorder env sigma d in
+        let env = reset_with_named_context sign env in
+        (env, sigma)
+      in
+      List.fold_left fold (env, sigma) args
     in
-    let env = Proofview.Goal.env gl in
-    let sigma = Tacmach.New.project gl in
-    let (env, sigma) = List.fold_left fold (env, sigma) args in
     let ty = Proofview.Goal.concl gl in
     Proofview.Unsafe.tclEVARS sigma
     <*>
@@ -854,8 +887,9 @@ let change ~check chg c cls =
       let redfun env sigma d = e_pf_change_decl redfun where env sigma d in
       (id, redfun)
     in
+    let reorder = if check then AnyHypConv else StableHypConv in
     (* Don't check, we do it already in [change_on_subterm] *)
-    e_change_in_hyps ~check:false ~reorder:check f hyps
+    e_change_in_hyps ~check:false ~reorder f hyps
   end
 
 let change_concl t = 
@@ -909,6 +943,8 @@ let reduce redexp cl =
     let redfun env sigma d = e_pf_change_decl redfun where env sigma d in
     (id, redfun)
   in
+  (* FIXME: use local flag *)
+  let reorder = if reorder then AnyHypConv else StableHypConv in
   e_change_in_hyps ~check ~reorder f hyps
   end
   end