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.

2 files changed, 26 insertions, 12 deletions

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;