Delay the computation of frozen evars in legacy unification.

This source of slowness has been observed in VST, but it is probably
pervasive. Most of the unification problems are not mentioning evars,
it is thus useless to compute the set of frozen evars upfront.

We also seize the opportunity to reverse the flag, because it is always
used negatively.

7 files changed, 55 insertions, 41 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 726752a2bf..1493092f2f 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -546,7 +546,7 @@ let rewrite_core_unif_flags = {
   Unification.check_applied_meta_types = true;
   Unification.use_pattern_unification = true;
   Unification.use_meta_bound_pattern_unification = true;
-  Unification.frozen_evars = Evar.Set.empty;
+  Unification.allowed_evars = Unification.AllowAll;
   Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a9eb43e573..4d34139ec0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -254,6 +254,10 @@ let unify_r2l x = x
 let sort_eqns = unify_r2l
 *)
 
+type allowed_evars =
+| AllowAll
+| AllowFun of (Evar.t -> bool)
+
 type core_unify_flags = {
   modulo_conv_on_closed_terms : TransparentState.t option;
     (* What this flag controls was activated with all constants transparent, *)
@@ -287,8 +291,8 @@ type core_unify_flags = {
     (* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *)
     (* when ?B is a Meta. *)
 
-  frozen_evars : Evar.Set.t;
-    (* Evars of this set are considered axioms and never instantiated *)
+  allowed_evars : allowed_evars;
+    (* Evars that are allowed to be instantiated *)
     (* Useful e.g. for autorewrite *)
 
   restrict_conv_on_strict_subterms : bool;
@@ -339,7 +343,7 @@ let default_core_unify_flags () =
   check_applied_meta_types = true;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
-  frozen_evars = Evar.Set.empty;
+  allowed_evars = AllowAll;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = true;
   modulo_eta = true;
@@ -417,6 +421,10 @@ let default_no_delta_unify_flags ts =
   resolve_evars = false
 }
 
+let allow_new_evars sigma =
+  let undefined = Evd.undefined_map sigma in
+  AllowFun (fun evk -> not (Evar.Map.mem evk undefined))
+
 (* Default flags for looking for subterms in elimination tactics *)
 (* Not used in practice at the current date, to the exception of *)
 (* allow_K) because only closed terms are involved in *)
@@ -424,9 +432,7 @@ let default_no_delta_unify_flags ts =
 (* call w_unify for induction/destruct/case/elim  (13/6/2011) *)
 let elim_core_flags sigma = { (default_core_unify_flags ()) with
   modulo_betaiota = false;
-  frozen_evars =
-    fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
-      sigma Evar.Set.empty;
+  allowed_evars = allow_new_evars sigma;
 }
 
 let elim_flags_evars sigma =
@@ -600,8 +606,12 @@ let do_reduce ts (env, nb) sigma c =
   Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state
                   ts env sigma (c, Stack.empty))
 
+let is_evar_allowed flags evk = match flags.allowed_evars with
+| AllowAll -> true
+| AllowFun f -> f evk
+
 let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
-  | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars)
+  | Evar (evk,_) -> is_evar_allowed flags evk
   | _ -> false
 
 
@@ -749,7 +759,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
 	| Evar (evk,_ as ev), Evar (evk',_)
-            when not (Evar.Set.mem evk flags.frozen_evars)
+            when is_evar_allowed flags evk
               && Evar.equal evk evk' ->
             begin match constr_cmp cv_pb env sigma flags cM cN with
             | Some sigma ->
@@ -758,14 +768,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	      sigma,metasubst,((curenv,ev,cN)::evarsubst)
             end
 	| Evar (evk,_ as ev), _
-            when not (Evar.Set.mem evk flags.frozen_evars) 
+            when is_evar_allowed flags evk
 	      && not (occur_evar sigma evk cN) ->
 	    let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
 	      if Int.Set.subset cnvars cmvars then
 		sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	      else error_cannot_unify_local curenv sigma (m,n,cN)
 	| _, Evar (evk,_ as ev)
-            when not (Evar.Set.mem evk flags.frozen_evars)
+            when is_evar_allowed flags evk
 	      && not (occur_evar sigma evk cM) ->
 	    let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
 	      if Int.Set.subset cmvars cnvars then
@@ -1554,7 +1564,7 @@ let default_matching_core_flags sigma =
   check_applied_meta_types = true;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = false;
-  frozen_evars = Evar.Map.domain (Evd.undefined_map sigma);
+  allowed_evars = allow_new_evars sigma;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
   modulo_eta = false;
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 0ee71246d8..d7ddbcb721 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -13,6 +13,10 @@ open EConstr
 open Environ
 open Evd
 
+type allowed_evars =
+| AllowAll
+| AllowFun of (Evar.t -> bool)
+
 type core_unify_flags = {
   modulo_conv_on_closed_terms : TransparentState.t option;
   use_metas_eagerly_in_conv_on_closed_terms : bool;
@@ -22,7 +26,7 @@ type core_unify_flags = {
   check_applied_meta_types : bool;
   use_pattern_unification : bool;
   use_meta_bound_pattern_unification : bool;
-  frozen_evars : Evar.Set.t;
+  allowed_evars : allowed_evars;
   restrict_conv_on_strict_subterms : bool;
   modulo_betaiota : bool;
   modulo_eta : bool;
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 1904d9b112..8e7d1df29a 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -108,7 +108,7 @@ let fail_quick_core_unif_flags = {
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true; (* ? *)
-  frozen_evars = Evar.Set.empty;
+  allowed_evars = AllowAll;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
   modulo_eta = true;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 499e7a63d7..67f49f0074 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -49,7 +49,7 @@ let auto_core_unif_flags_of st1 st2 = {
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
-  frozen_evars = Evar.Set.empty;
+  allowed_evars = AllowAll;
   restrict_conv_on_strict_subterms = false; (* Compat *)
   modulo_betaiota = false;
   modulo_eta = true;
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 05f40d0570..cf5c64c3ae 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -151,7 +151,7 @@ let pr_ev evs ev =
 open Auto
 open Unification
 
-let auto_core_unif_flags st freeze = {
+let auto_core_unif_flags st allowed_evars = {
   modulo_conv_on_closed_terms = Some st;
   use_metas_eagerly_in_conv_on_closed_terms = true;
   use_evars_eagerly_in_conv_on_closed_terms = false;
@@ -160,14 +160,14 @@ let auto_core_unif_flags st freeze = {
   check_applied_meta_types = false;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
-  frozen_evars = freeze;
+  allowed_evars;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = true;
   modulo_eta = false;
 }
 
-let auto_unif_flags freeze st =
-  let fl = auto_core_unif_flags st freeze in
+let auto_unif_flags ?(allowed_evars = AllowAll) st =
+  let fl = auto_core_unif_flags st allowed_evars in
   { core_unify_flags = fl;
     merge_unify_flags = fl;
     subterm_unify_flags = fl;
@@ -357,23 +357,25 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
   let open Proofview.Notations in
   let prods, concl = EConstr.decompose_prod_assum sigma concl in
   let nprods = List.length prods in
-  let freeze =
+  let allowed_evars =
     try
       match hdc with
       | Some (hd,_) when only_classes ->
          let cl = Typeclasses.class_info env sigma hd in
          if cl.cl_strict then
-           Evarutil.undefined_evars_of_term sigma concl
-         else Evar.Set.empty
-      | _ -> Evar.Set.empty
-    with e when CErrors.noncritical e -> Evar.Set.empty
+          let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in
+          let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in
+          AllowFun allowed
+         else AllowAll
+      | _ -> AllowAll
+    with e when CErrors.noncritical e -> AllowAll
   in
   let hint_of_db = hintmap_of sigma hdc secvars concl in
   let hintl =
     List.map_append
       (fun db ->
         let tacs = hint_of_db db in
-        let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
+        let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in
           List.map (fun x -> (flags, x)) tacs)
       (local_db::db_list)
   in
@@ -1198,7 +1200,7 @@ let autoapply c i =
   let hintdb = try Hints.searchtable_map i with Not_found ->
     CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ "."))
   in
-  let flags = auto_unif_flags Evar.Set.empty
+  let flags = auto_unif_flags
     (Hints.Hint_db.transparent_state hintdb) in
   let cty = Tacmach.New.pf_unsafe_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b9d718dd61..220b9bc475 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -38,7 +38,6 @@ open Coqlib
 open Declarations
 open Indrec
 open Clenv
-open Evd
 open Ind_tables
 open Eqschemes
 open Locus
@@ -107,7 +106,7 @@ let rewrite_core_unif_flags = {
   check_applied_meta_types = true;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
-  frozen_evars = Evar.Set.empty;
+  allowed_evars = AllowAll;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
   modulo_eta = true;
@@ -126,16 +125,17 @@ let freeze_initial_evars sigma flags clause =
   (* We take evars of the type: this may include old evars! For excluding *)
   (* all old evars, including the ones occurring in the rewriting lemma, *)
   (* we would have to take the clenv_value *)
-  let newevars = Evarutil.undefined_evars_of_term sigma (clenv_type clause) in
-  let evars =
-    fold_undefined (fun evk _ evars ->
-      if Evar.Set.mem evk newevars then evars
-      else Evar.Set.add evk evars)
-      sigma Evar.Set.empty in
+  let newevars = lazy (Evarutil.undefined_evars_of_term sigma (clenv_type clause)) in
+  let initial = Evd.undefined_map sigma in
+  let allowed evk =
+    if Evar.Map.mem evk initial then false
+    else Evar.Set.mem evk (Lazy.force newevars)
+  in
+  let allowed_evars = AllowFun allowed in
   {flags with
-    core_unify_flags = {flags.core_unify_flags with frozen_evars = evars};
-    merge_unify_flags = {flags.merge_unify_flags with frozen_evars = evars};
-    subterm_unify_flags = {flags.subterm_unify_flags with frozen_evars = evars}}
+    core_unify_flags = {flags.core_unify_flags with allowed_evars};
+    merge_unify_flags = {flags.merge_unify_flags with allowed_evars};
+    subterm_unify_flags = {flags.subterm_unify_flags with allowed_evars}}
 
 let make_flags frzevars sigma flags clause =
   if frzevars then freeze_initial_evars sigma flags clause else flags
@@ -188,8 +188,7 @@ let rewrite_conv_closed_core_unif_flags = {
 
   use_meta_bound_pattern_unification = true;
 
-  frozen_evars = Evar.Set.empty;
-    (* This is set dynamically *)
+  allowed_evars = AllowAll;
 
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
@@ -223,8 +222,7 @@ let rewrite_keyed_core_unif_flags = {
 
   use_meta_bound_pattern_unification = true;
 
-  frozen_evars = Evar.Set.empty;
-    (* This is set dynamically *)
+  allowed_evars = AllowAll;
 
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = true;