Several easy but efficient optimizations for subst and clear tactics.

They were spotted by profiling tactics manipulating huge terms, provided by
Jason Gross.

3 files changed, 32 insertions, 15 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 4506fddb5f..df1424e1c6 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -472,27 +472,30 @@ let cleared = Store.field ()
 
 exception Depends of Id.t
 
-let rec check_and_clear_in_constr env evdref err ids c =
+let rec check_and_clear_in_constr env evdref err ids global c =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
-     evars) *)
-  let check id' =
-    if Id.Set.mem id' ids then
-      raise (ClearDependencyError (id',err))
-  in
+     evars). [global] should be true iff there is some variable of [ids] which
+     is a section variable *)
     match kind_of_term c with
       | Var id' ->
-	  check id'; c
+      if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c
 
       | ( Const _ | Ind _ | Construct _ ) ->
-          let vars = Environ.vars_of_global env c in
-            Id.Set.iter check vars; c
+        let () = if global then
+          let check id' =
+            if Id.Set.mem id' ids then
+              raise (ClearDependencyError (id',err))
+          in
+          Id.Set.iter check (Environ.vars_of_global env c)
+        in
+        c
 
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
 	    let nc = whd_evar !evdref c in
-	      (check_and_clear_in_constr env evdref err ids nc)
+	      (check_and_clear_in_constr env evdref err ids global nc)
 	  else
 	    (* We check for dependencies to elements of ids in the
 	       evar_info corresponding to e and in the instance of
@@ -527,7 +530,8 @@ let rec check_and_clear_in_constr env evdref err ids c =
 	    let _nconcl =
 	      try
                 let nids = Id.Map.domain rids in
-                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi)
+                let global = Id.Set.exists is_section_variable nids in
+                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global (evar_concl evi)
 	      with ClearDependencyError (rid,err) ->
 		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
 
@@ -548,19 +552,20 @@ let rec check_and_clear_in_constr env evdref err ids c =
 	    (* spiwack: /hacking session *)
               whd_evar !evdref c
 
-      | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c
+      | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
 
 let clear_hyps_in_evi_main env evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occurring in evi *)
+  let global = Id.Set.exists is_section_variable ids in
   let terms =
-    List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
+    List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in
   let nhyps =
     let open Context.Named.Declaration in
     let check_context decl =
       let err = OccurHypInSimpleClause (Some (get_id decl)) in
-      map_constr (check_and_clear_in_constr env evdref err ids) decl
+      map_constr (check_and_clear_in_constr env evdref err ids global) decl
     in
     let check_value vk = match force_lazy_val vk with
     | None -> vk
diff --git a/engine/termops.ml b/engine/termops.ml
index f698f81513..ac8461a3ab 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -564,7 +564,14 @@ let occur_var_in_decl env hyp decl =
         occur_var env hyp typ ||
         occur_var env hyp body
 
-(* returns the list of free debruijn indices in a term *)
+let local_occur_var id c =
+  let rec occur c = match kind_of_term c with
+  | Var id' -> if Id.equal id id' then raise Occur
+  | _ -> Constr.iter occur c
+  in
+  try occur c; false with Occur -> true
+
+  (* returns the list of free debruijn indices in a term *)
 
 let free_rels m =
   let rec frec depth acc c = match kind_of_term c with
diff --git a/engine/termops.mli b/engine/termops.mli
index 76a31037bc..5d85088f8d 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -96,6 +96,7 @@ val strip_head_cast : constr -> constr
 val drop_extra_implicit_args : constr -> constr
 
 (** occur checks *)
+
 exception Occur
 val occur_meta : types -> bool
 val occur_existential : types -> bool
@@ -105,6 +106,10 @@ val occur_var : env -> Id.t -> types -> bool
 val occur_var_in_decl :
   env ->
   Id.t -> Context.Named.Declaration.t -> bool
+
+(** As {!occur_var} but assume the identifier not to be a section variable *)
+val local_occur_var : Id.t -> types -> bool
+
 val free_rels : constr -> Int.Set.t
 
 (** [dependent m t] tests whether [m] is a subterm of [t] *)