Abstract type for allowed evars

11 files changed, 66 insertions, 39 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a8a3a21f4a..a1dbf9a439 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.allowed_evars = Evarsolve.AllowAll;
+  Unification.allowed_evars = Evarsolve.AllowedEvars.all;
   Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3dc00d195e..61453ff214 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -40,7 +40,7 @@ let default_transparent_state env = TransparentState.full
 let default_flags_of ?(subterm_ts=TransparentState.empty) ts =
   { modulo_betaiota = true;
     open_ts = ts; closed_ts = ts; subterm_ts;
-    allowed_evars = AllowAll; with_cs = true;
+    allowed_evars = AllowedEvars.all; with_cs = true;
     allow_K_at_toplevel = true }
 
 let default_flags env =
@@ -1209,7 +1209,7 @@ let default_occurrence_test ~allowed_evars ts _ origsigma _ env sigma _ c pat =
   | Success sigma -> true, sigma
   | UnifFailure _ -> false, sigma
 
-let default_occurrences_selection ?(allowed_evars=AllowAll) ts n =
+let default_occurrences_selection ?(allowed_evars=AllowedEvars.all) ts n =
   (default_occurrence_test ~allowed_evars ts,
    List.init n (fun _ -> default_occurrence_selection))
 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9343be6484..a5a8d1f916 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -105,11 +105,11 @@ val default_occurrence_selection : occurrence_selection
 type occurrences_selection =
   occurrence_match_test * occurrence_selection list
 
-val default_occurrence_test : allowed_evars:Evarsolve.allowed_evars -> TransparentState.t -> occurrence_match_test
+val default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test
 
 (** [default_occurrence_selection n]
     Gives the default test and occurrences for [n] arguments *)
-val default_occurrences_selection : ?allowed_evars:Evarsolve.allowed_evars (* By default, all *) ->
+val default_occurrences_selection : ?allowed_evars:Evarsolve.AllowedEvars.t (* By default, all *) ->
   TransparentState.t -> int -> occurrences_selection
 
 val second_order_matching : unify_flags -> env -> evar_map ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9cf1e6fd6f..09e49f3253 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -25,23 +25,46 @@ open Reductionops
 open Evarutil
 open Pretype_errors
 
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
+module AllowedEvars = struct
+
+  type t =
+  | AllowAll
+  | AllowFun of (Evar.t -> bool)
+
+  let mem allowed evk =
+    match allowed with
+    | AllowAll -> true
+    | AllowFun f -> f evk
+
+  let remove evk allowed =
+    let allowed = match allowed with
+      | AllowAll -> fun evk' -> not (Evar.equal evk evk')
+      | AllowFun f -> fun evk' -> not (Evar.equal evk evk') && f evk'
+    in
+    AllowFun allowed
+
+  let all = AllowAll
+
+  let except evars =
+    AllowFun (fun evk -> not (Evar.Set.mem evk evars))
+
+  let from_pred f =
+    AllowFun f
+
+end
 
 type unify_flags = {
   modulo_betaiota: bool;
   open_ts : TransparentState.t;
   closed_ts : TransparentState.t;
   subterm_ts : TransparentState.t;
-  allowed_evars : allowed_evars;
+  allowed_evars : AllowedEvars.t;
   allow_K_at_toplevel : bool;
   with_cs : bool
 }
 
-let is_evar_allowed flags evk = match flags.allowed_evars with
-| AllowAll -> true
-| AllowFun f -> f evk
+let is_evar_allowed flags evk =
+  AllowedEvars.mem flags.allowed_evars evk
 
 type unification_kind =
   | TypeUnification
@@ -1464,11 +1487,8 @@ let occur_evar_upto_types sigma n c =
 let instantiate_evar unify flags env evd evk body =
   (* Check instance freezing the evar to be defined, as
      checking could involve the same evar definition problem again otherwise *)
-  let allowed = match flags.allowed_evars with
-    | AllowAll -> fun evk' -> not (Evar.equal evk evk')
-    | AllowFun f -> fun evk' -> not (Evar.equal evk evk') && f evk'
-  in
-  let flags = { flags with allowed_evars = AllowFun allowed } in
+  let allowed_evars = AllowedEvars.remove evk flags.allowed_evars in
+  let flags = { flags with allowed_evars } in
   let evd' = check_evar_instance unify flags env evd evk body in
   Evd.define evk body evd'
 
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 89e162937d..c248e50820 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -16,9 +16,17 @@ type alias
 
 val of_alias : alias -> EConstr.t
 
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
+module AllowedEvars : sig
+
+  type t
+
+  val all : t
+  val mem : t -> Evar.t -> bool
+  val remove : Evar.t -> t -> t
+  val except : Evar.Set.t -> t
+  val from_pred : (Evar.t -> bool) -> t
+
+end
 
 type unify_flags = {
   modulo_betaiota : bool;
@@ -30,7 +38,7 @@ type unify_flags = {
   subterm_ts : TransparentState.t;
   (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order
      unifications. *)
-  allowed_evars : allowed_evars;
+  allowed_evars : AllowedEvars.t;
   (* Disallowed evars are treated like rigid variables during unification: they can not be instantiated. *)
   allow_K_at_toplevel : bool;
   (* During higher-order unifications, allow to produce K-redexes: i.e. to produce
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d63d367a84..746a237b24 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -285,7 +285,7 @@ type core_unify_flags = {
     (* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *)
     (* when ?B is a Meta. *)
 
-  allowed_evars : allowed_evars;
+  allowed_evars : AllowedEvars.t;
     (* Evars that are allowed to be instantiated *)
     (* Useful e.g. for autorewrite *)
 
@@ -337,7 +337,7 @@ let default_core_unify_flags () =
   check_applied_meta_types = true;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
-  allowed_evars = AllowAll;
+  allowed_evars = AllowedEvars.all;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = true;
   modulo_eta = true;
@@ -417,7 +417,7 @@ let default_no_delta_unify_flags ts =
 
 let allow_new_evars sigma =
   let undefined = Evd.undefined_map sigma in
-  AllowFun (fun evk -> not (Evar.Map.mem evk undefined))
+  AllowedEvars.except @@ Evar.Map.domain undefined
 
 (* Default flags for looking for subterms in elimination tactics *)
 (* Not used in practice at the current date, to the exception of *)
@@ -600,9 +600,8 @@ 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 is_evar_allowed flags evk =
+  AllowedEvars.mem flags.allowed_evars evk
 
 let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
   | Evar (evk,_) -> is_evar_allowed flags evk
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index e3750f7d97..5462e09359 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -22,7 +22,7 @@ type core_unify_flags = {
   check_applied_meta_types : bool;
   use_pattern_unification : bool;
   use_meta_bound_pattern_unification : bool;
-  allowed_evars : Evarsolve.allowed_evars;
+  allowed_evars : Evarsolve.AllowedEvars.t;
   restrict_conv_on_strict_subterms : bool;
   modulo_betaiota : bool;
   modulo_eta : bool;
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 65a7a6c711..8e3cab70ea 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -673,7 +673,7 @@ let fail_quick_core_unif_flags = {
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true; (* ? *)
-  allowed_evars = Evarsolve.AllowAll;
+  allowed_evars = Evarsolve.AllowedEvars.all;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
   modulo_eta = true;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4cec72597a..369508c2a3 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -47,7 +47,7 @@ let auto_core_unif_flags_of st1 st2 = {
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
-  allowed_evars = Evarsolve.AllowAll;
+  allowed_evars = Evarsolve.AllowedEvars.all;
   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 39589b2d11..96cbbf0ba8 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -134,7 +134,7 @@ let auto_core_unif_flags st allowed_evars = {
   modulo_eta = false;
 }
 
-let auto_unif_flags ?(allowed_evars = Evarsolve.AllowAll) st =
+let auto_unif_flags ?(allowed_evars = Evarsolve.AllowedEvars.all) st =
   let fl = auto_core_unif_flags st allowed_evars in
   { core_unify_flags = fl;
     merge_unify_flags = fl;
@@ -307,10 +307,10 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
          if cl.cl_strict then
           let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in
           let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in
-          Evarsolve.AllowFun allowed
-         else Evarsolve.AllowAll
-      | _ -> Evarsolve.AllowAll
-    with e when CErrors.noncritical e -> Evarsolve.AllowAll
+          Evarsolve.AllowedEvars.from_pred allowed
+         else Evarsolve.AllowedEvars.all
+      | _ -> Evarsolve.AllowedEvars.all
+    with e when CErrors.noncritical e -> Evarsolve.AllowedEvars.all
   in
   let tac_of_hint =
     fun (flags, h) ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index cecb2df8e0..2388085059 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -105,7 +105,7 @@ let rewrite_core_unif_flags = {
   check_applied_meta_types = true;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
-  allowed_evars = Evarsolve.AllowAll;
+  allowed_evars = Evarsolve.AllowedEvars.all;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
   modulo_eta = true;
@@ -130,7 +130,7 @@ let freeze_initial_evars sigma flags clause =
     if Evar.Map.mem evk initial then false
     else Evar.Set.mem evk (Lazy.force newevars)
   in
-  let allowed_evars = Evarsolve.AllowFun allowed in
+  let allowed_evars = Evarsolve.AllowedEvars.from_pred allowed in
   {flags with
     core_unify_flags = {flags.core_unify_flags with allowed_evars};
     merge_unify_flags = {flags.merge_unify_flags with allowed_evars};
@@ -187,7 +187,7 @@ let rewrite_conv_closed_core_unif_flags = {
 
   use_meta_bound_pattern_unification = true;
 
-  allowed_evars = Evarsolve.AllowAll;
+  allowed_evars = Evarsolve.AllowedEvars.all;
 
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
@@ -221,7 +221,7 @@ let rewrite_keyed_core_unif_flags = {
 
   use_meta_bound_pattern_unification = true;
 
-  allowed_evars = Evarsolve.AllowAll;
+  allowed_evars = Evarsolve.AllowedEvars.all;
 
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = true;