Abstract type for allowed evars

6 files changed, 54 insertions, 27 deletions

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;