Several easy but efficient optimizations for subst and clear tactics.

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

8 files changed, 64 insertions, 54 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] *)
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 78dce0d64c..853410db8b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -109,7 +109,7 @@ let clenv_environments evd bound t =
       | (n, Cast (t,_,_)) -> clrec (e,metas) n t
       | (n, Prod (na,t1,t2)) ->
 	  let mv = new_meta () in
-	  let dep = dependent (mkRel 1) t2 in
+	  let dep = not (noccurn 1 t2) in
 	  let na' = if dep then na else Anonymous in
 	  let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1d3239ef68..35be1fcb6e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1663,10 +1663,14 @@ exception FoundHyp of (Id.t * constr * bool)
 let is_eq_x gl x d =
   let id = get_id d in
   try
+    let is_var id c = match kind_of_term c with
+    | Var id' -> Id.equal id id'
+    | _ -> false
+    in
     let c = pf_nf_evar gl (get_type d) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
-    if (Term.eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
-    if (Term.eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
+    if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true));
+    if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false))
   with Constr_matching.PatternMatchingFailure ->
     ()
 
@@ -1713,14 +1717,12 @@ let subst_one_var dep_proof_ok x =
     let xval = pf_get_hyp x gl |> get_value in
     (* If x has a body, simply replace x with body and clear x *)
     if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) else
-      (* x is a variable: *)
-      let varx = mkVar x in
       (* Find a non-recursive definition for x *)
       let res =
         try
           (** [is_eq_x] ensures nf_evar on its side *)
           let hyps = Proofview.Goal.hyps gl in
-          let test hyp _ = is_eq_x gl varx hyp in
+          let test hyp _ = is_eq_x gl x hyp in
           Context.Named.fold_outside test ~init:() hyps;
           errorlabstrm "Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
@@ -1730,7 +1732,7 @@ let subst_one_var dep_proof_ok x =
   end }
 
 let subst_gen dep_proof_ok ids =
-  tclTHEN Proofview.V82.nf_evar_goals (tclMAP (subst_one_var dep_proof_ok) ids)
+  tclMAP (subst_one_var dep_proof_ok) ids
 
 (* For every x, look for an hypothesis hyp of the form "x=rhs" or "rhs=x",
    rewrite it everywhere, and erase hyp and x; proceed by generalizing
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index fded54fcb1..4c2c84d23b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -406,38 +406,27 @@ let rec first_match matcher = function
 
 (*** Equality *)
 
-(* Patterns "(eq ?1 ?2 ?3)" and "(identity ?1 ?2 ?3)" *)
-(** %eq ?X1 ?X2 ?X3 *)
-let coq_eq_pattern_gen eq =
-  lazy (mkPattern (mkGAppRef eq (List.map mkGPatVar ["X1"; "X2"; "X3";])))
-let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
-let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
-(** %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 *)
-let coq_jmeq_pattern =
-  lazy (mkPattern
-    (mkGAppRef coq_jmeq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"; "X4"])))
-
-let match_eq eqn eq_pat =
-  let pat =
-    try Lazy.force eq_pat
+let match_eq eqn (ref, hetero) =
+  let ref =
+    try Lazy.force ref
     with e when Errors.noncritical e -> raise PatternMatchingFailure
   in
-  match Id.Map.bindings (matches pat eqn) with
-    | [(m1,t);(m2,x);(m3,y)] ->
-	assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
-        PolymorphicLeibnizEq (t,x,y)
-    | [(m1,t);(m2,x);(m3,t');(m4,x')] ->
-        assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4);
-	HeterogenousEq (t,x,t',x')
-    | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 or 4 terms")
+  match kind_of_term eqn with
+  | App (c, [|t; x; y|]) ->
+    if not hetero && is_global ref c then PolymorphicLeibnizEq (t, x, y)
+    else raise PatternMatchingFailure
+  | App (c, [|t; x; t'; x'|]) ->
+    if hetero && is_global ref c then HeterogenousEq (t, x, t', x')
+    else raise PatternMatchingFailure
+  | _ -> raise PatternMatchingFailure
 
 let no_check () = true
 let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module
 
 let equalities =
-  [coq_eq_pattern, no_check, build_coq_eq_data;
-   coq_jmeq_pattern, check_jmeq_loaded, build_coq_jmeq_data;
-   coq_identity_pattern, no_check, build_coq_identity_data]
+  [(coq_eq_ref, false), no_check, build_coq_eq_data;
+   (coq_jmeq_ref, true), check_jmeq_loaded, build_coq_jmeq_data;
+   (coq_identity_ref, false), no_check, build_coq_identity_data]
 
 let find_eq_data eqn = (* fails with PatternMatchingFailure *)
   let d,k = first_match (match_eq eqn) equalities in
@@ -468,8 +457,11 @@ let find_this_eq_data_decompose gl eqn =
       error "Don't know what to do with JMeq on arguments not of same type." in
   (lbeq,u,eq_args)
 
-let match_eq_nf gls eqn eq_pat =
-  match Id.Map.bindings (pf_matches gls (Lazy.force eq_pat) eqn) with
+let match_eq_nf gls eqn (ref, hetero) =
+  let n = if hetero then 4 else 3 in
+  let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in
+  let pat = mkPattern (mkGAppRef ref args) in
+  match Id.Map.bindings (pf_matches gls pat eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
 	(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3d51623eaa..46145d1116 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -590,8 +590,8 @@ module New = struct
   let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end }
 
   let afterHyp id tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let hyps = Proofview.Goal.hyps gl in
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     let rem, _ = List.split_when (Id.equal id % get_id) hyps in
     tac rem
     end }
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c336bb434a..e264505314 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2928,12 +2928,11 @@ let unfold_body x =
   let xval = match Context.Named.lookup x hyps with
   | LocalAssum _ -> errorlabstrm "unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
-  | LocalDef (_,xval,_) -> pf_nf_evar gl xval
+  | LocalDef (_,xval,_) -> xval
   in
   Tacticals.New.afterHyp x begin fun aft ->
   let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in
-  let xvar = mkVar x in
-  let rfun _ _ c = replace_term xvar xval c in
+  let rfun _ _ c = replace_vars [x, xval] c in
   let reducth h = reduct_in_hyp rfun h in
   let reductc = reduct_in_concl (rfun, DEFAULTcast) in
   Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]