Merge PR #9062: Delay the computation of frozen evars in legacy unification.

Reviewed-by: mattam82

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;