Cleanup evar_extra: remove evar_info's store and add maps to evar_map

7 files changed, 116 insertions, 61 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index f9d9ce3569..69830960a9 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -410,7 +410,7 @@ let new_pure_evar_full evd evi =
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?(principal=false) sign evd typ =
   let default_naming = IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
@@ -427,8 +427,7 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
     evar_body = Evar_empty;
     evar_filter = filter;
     evar_source = src;
-    evar_candidates = candidates;
-    evar_extra = store; }
+    evar_candidates = candidates }
   in
   let (evd, newevk) = Evd.new_evar evd ?name evi in
   let evd =
@@ -437,24 +436,24 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
   in
   (evd, newevk)
 
-let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance =
+let new_evar_instance ?src ?filter ?candidates ?naming ?principal sign evd typ instance =
   let open EConstr in
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
-let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ =
+let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
   let instance =
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance
+  new_evar_instance sign evd typ ?src ?filter ?candidates ?naming ?principal instance
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ =
+let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ =
   let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
   let map c = csubst_subst subst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
@@ -462,7 +461,7 @@ let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env e
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
+  new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?principal instance
 
 let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
@@ -714,7 +713,7 @@ let rec advance sigma evk =
   match evi.evar_body with
   | Evar_empty -> Some evk
   | Evar_defined v ->
-      match is_restricted_evar evi with
+      match is_restricted_evar sigma evk with
       | Some evk -> advance sigma evk
       | None -> None
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 11e07175e3..49443164cc 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -27,7 +27,7 @@ val mk_new_meta : unit -> constr
 
 val new_evar_from_context :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
+  ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
   named_context_val -> evar_map  -> types -> evar_map * EConstr.t
@@ -40,14 +40,14 @@ type naming_mode =
 
 val new_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
+  ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?principal:bool -> ?hypnaming:naming_mode ->
   env -> evar_map -> types -> evar_map * EConstr.t
 
 val new_pure_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
+  ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
   named_context_val -> evar_map -> types -> evar_map * Evar.t
@@ -77,7 +77,7 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
    as a telescope) is [sign] *)
 val new_evar_instance :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
-  ?store:Store.t -> ?naming:intro_pattern_naming_expr ->
+  ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
  named_context_val -> evar_map -> types ->
   constr list -> evar_map * constr
diff --git a/engine/evd.ml b/engine/evd.ml
index eafdc4cb46..3a01706063 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -144,8 +144,7 @@ type evar_info = {
   evar_body : evar_body;
   evar_filter : Filter.t;
   evar_source : Evar_kinds.t Loc.located;
-  evar_candidates : constr list option; (* if not None, list of allowed instances *)
-  evar_extra : Store.t }
+  evar_candidates : constr list option; (* if not None, list of allowed instances *)}
 
 let make_evar hyps ccl = {
   evar_concl = ccl;
@@ -153,9 +152,7 @@ let make_evar hyps ccl = {
   evar_body = Evar_empty;
   evar_filter = Filter.identity;
   evar_source = Loc.tag @@ Evar_kinds.InternalHole;
-  evar_candidates = None;
-  evar_extra = Store.empty
-}
+  evar_candidates = None; }
 
 let instance_mismatch () =
   anomaly (Pp.str "Signature and its instance do not match.")
@@ -413,6 +410,11 @@ end
 
 type goal_kind = ToShelve | ToGiveUp
 
+type evar_flags =
+  { obligation_evars : Evar.Set.t;
+    restricted_evars : Evar.t Evar.Map.t;
+    unresolvable_evars : Evar.Set.t }
+
 type evar_map = {
   (** Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -425,6 +427,7 @@ type evar_map = {
   last_mods  : Evar.Set.t;
   (** Metas *)
   metas      : clbinding Metamap.t;
+  evar_flags : evar_flags;
   (** Interactive proofs *)
   effects    : Safe_typing.private_constants;
   future_goals : Evar.t list; (** list of newly created evars, to be
@@ -456,6 +459,45 @@ let add_with_name ?name d e i = match i.evar_body with
 
 let add d e i = add_with_name d e i
 
+(*** Evar flags: resolvable, restricted or obligation flag *)
+
+let set_resolvable_evar evd evk b =
+  let flags = evd.evar_flags in
+  let unresolvable_evars = flags.unresolvable_evars in
+  let unresolvable_evars =
+    if b then Evar.Set.remove evk unresolvable_evars
+    else Evar.Set.add evk unresolvable_evars
+  in
+  { evd with evar_flags = { flags with unresolvable_evars } }
+
+let is_resolvable_evar evd evk =
+  let flags = evd.evar_flags in
+  not (Evar.Set.mem evk flags.unresolvable_evars)
+
+let inherit_unresolvable_evar evar_flags evk evk' =
+  let evk_unres = Evar.Set.mem evk evar_flags.unresolvable_evars in
+  let unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars in
+  let unresolvable_evars =
+    if evk_unres then Evar.Set.add evk' unresolvable_evars else unresolvable_evars
+  in { evar_flags with unresolvable_evars }
+
+let unresolvable_evars evd = evd.evar_flags.unresolvable_evars
+
+let set_obligation_evar evd evk =
+  let flags = evd.evar_flags in
+  let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in
+  { evd with evar_flags }
+
+let is_obligation_evar evd evk =
+  let flags = evd.evar_flags in
+  Evar.Set.mem evk flags.obligation_evars
+
+let remove_evar_flags evk evar_flags =
+  { unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars;
+    obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
+    (** Restriction information is kept. *)
+    restricted_evars = evar_flags.restricted_evars }
+
 (** New evars *)
 
 let evar_counter_summary_name = "evar counter"
@@ -478,7 +520,9 @@ let remove d e =
   in
   let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
   let future_goals_status = EvMap.remove e d.future_goals_status in
-  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status }
+  let evar_flags = remove_evar_flags e d.evar_flags in
+  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status;
+           evar_flags }
 
 let find d e =
   try EvMap.find e d.undf_evars
@@ -583,12 +627,18 @@ let cmap f evd =
 let create_evar_defs sigma = { sigma with
   conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
 
+let empty_evar_flags =
+  { obligation_evars = Evar.Set.empty;
+    restricted_evars = Evar.Map.empty;
+    unresolvable_evars = Evar.Set.empty }
+
 let empty = {
   defn_evars = EvMap.empty;
   undf_evars = EvMap.empty;
   universes  = UState.empty;
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
+  evar_flags = empty_evar_flags;
   metas      = Metamap.empty;
   effects    = Safe_typing.empty_private_constants;
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
@@ -634,9 +684,7 @@ let evar_source evk d = (find d evk).evar_source
 let evar_ident evk evd = EvNames.ident evk evd.evar_names
 let evar_key id evd = EvNames.key id evd.evar_names
 
-let restricted = Store.field ()
-
-let define_aux ?dorestrict def undef evk body =
+let define_aux def undef evk body =
   let oldinfo =
     try EvMap.find evk undef
     with Not_found ->
@@ -646,10 +694,7 @@ let define_aux ?dorestrict def undef evk body =
         anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
   in
   let () = assert (oldinfo.evar_body == Evar_empty) in
-  let evar_extra = match dorestrict with
-    | Some evk' -> Store.set oldinfo.evar_extra restricted evk'
-    | None -> oldinfo.evar_extra in
-  let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in
+  let newinfo = { oldinfo with evar_body = Evar_defined body } in
   EvMap.add evk newinfo def, EvMap.remove evk undef
 
 (* define the existential of section path sp as the constr body *)
@@ -660,10 +705,15 @@ let define evk body evd =
   | _ -> Evar.Set.add evk evd.last_mods
   in
   let evar_names = EvNames.remove_name_defined evk evd.evar_names in
-  { evd with defn_evars; undf_evars; last_mods; evar_names }
+  let evar_flags = remove_evar_flags evk evd.evar_flags in
+  { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+
+let is_restricted_evar evd evk =
+  try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
+  with Not_found -> None
 
-let is_restricted_evar evi =
-  Store.get evi.evar_extra restricted
+let declare_restricted_evar evar_flags evk evk' =
+  { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
 
 let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
@@ -679,9 +729,11 @@ let restrict evk filter ?candidates ?src evd =
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
-  let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in
+  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+  let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
+  let evar_flags = inherit_unresolvable_evar evar_flags evk evk' in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; last_mods; evar_names }, evk'
+    defn_evars; last_mods; evar_names; evar_flags }, evk'
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -1019,6 +1071,7 @@ let set_metas evd metas = {
   universes  = evd.universes;
   conv_pbs = evd.conv_pbs;
   last_mods = evd.last_mods;
+  evar_flags = evd.evar_flags;
   metas;
   effects = evd.effects;
   evar_names = evd.evar_names;
diff --git a/engine/evd.mli b/engine/evd.mli
index 1a5614988d..87f74f660d 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -83,10 +83,6 @@ type evar_body =
   | Evar_empty
   | Evar_defined of econstr
 
-
-module Store : Store.S
-(** Datatype used to store additional information in evar maps. *)
-
 type evar_info = {
   evar_concl : econstr;
   (** Type of the evar. *)
@@ -102,8 +98,6 @@ type evar_info = {
   (** Information about the evar. *)
   evar_candidates : econstr list option;
   (** List of possible solutions when known that it is a finite list *)
-  evar_extra : Store.t
-  (** Extra store, used for clever hacks. *)
 }
 
 val make_evar : named_context_val -> etypes -> evar_info
@@ -247,9 +241,24 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
     possibly limiting the instances to a set of candidates (candidates
     are filtered according to the filter) *)
 
-val is_restricted_evar : evar_info -> Evar.t option
+val is_restricted_evar : evar_map -> Evar.t -> Evar.t option
 (** Tell if an evar comes from restriction of another evar, and if yes, which *)
 
+val set_resolvable_evar : evar_map -> Evar.t -> bool -> evar_map
+(** Declare an evar resolvable or unresolvable for typeclass resolution *)
+
+val unresolvable_evars : evar_map -> Evar.Set.t
+(** The set of unresolvable evars *)
+
+val is_resolvable_evar : evar_map -> Evar.t -> bool
+(** Is the evar declared resolvable for typeclass resolution *)
+
+val set_obligation_evar : evar_map -> Evar.t -> evar_map
+(** Declare an evar as an obligation *)
+
+val is_obligation_evar : evar_map -> Evar.t -> bool
+(** Is the evar declared as an obligation *)
+
 val downcast : Evar.t-> etypes -> evar_map -> evar_map
 (** Change the type of an undefined evar to a new type assumed to be a
     subtype of its current type; subtyping must be ensured by caller *)
@@ -357,6 +366,9 @@ val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map
 
 *)
 
+module Store : Store.S
+(** Datatype used to store additional information in evar maps. *)
+
 val get_extra_data : evar_map -> Store.t
 val set_extra_data : Store.t -> evar_map -> evar_map
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 12d31e5f46..aabc629ee4 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -60,20 +60,18 @@ type telescope =
   | TNil of Evd.evar_map
   | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
 
-let typeclass_resolvable = Evd.Store.field ()
-
 let dependent_init =
-  (* Goals are created with a store which marks them as unresolvable
-     for type classes. *)
-  let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in
   (* Goals don't have a source location. *)
   let src = Loc.tag @@ Evar_kinds.GoalEvar in
   (* Main routine *)
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
-    let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in
+    let (sigma, econstr) = Evarutil.new_evar env sigma ~src typ in
     let (gl, _) = EConstr.destEvar sigma econstr in
+    (* Goals are created with a store which marks them as unresolvable
+       for type classes. *)
+    let sigma = Evd.set_resolvable_evar sigma gl false in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let entry = (econstr, typ) :: ret in
     entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
@@ -760,11 +758,8 @@ let mark_in_evm ~goal evd content =
             | loc,_ -> loc,Evar_kinds.GoalEvar }
     else info
   in
-  let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
-  | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
-  | Some () -> info
-  in
-  Evd.add evd content info
+  let evd = Evd.add evd content info in
+  Evd.set_resolvable_evar evd content false
 
 let with_shelf tac =
   let open Proof in
@@ -1045,8 +1040,6 @@ module Unsafe = struct
   let mark_as_unresolvable p gl =
     { p with solution = mark_in_evm ~goal:false p.solution gl }
 
-  let typeclass_resolvable = typeclass_resolvable
-
 end
 
 module UnsafeRepr = Proof.Unsafe
@@ -1065,10 +1058,6 @@ let goal_nf_evar sigma gl =
   let sigma = Evd.add sigma gl evi in
   (gl, sigma)
 
-let goal_extra evars gl =
-  let evi = Evd.find evars gl in
-  evi.Evd.evar_extra
-
 
 let catchable_exception = function
   | Logic_monad.Exception _ -> false
@@ -1093,7 +1082,6 @@ module Goal = struct
   let sigma {sigma} = sigma
   let hyps {env} = EConstr.named_context env
   let concl {concl} = concl
-  let extra {sigma; self} = goal_extra sigma self
 
   let gmake_with info env sigma goal state =
     { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 0bb3229a9b..7bf6390f0e 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -475,8 +475,6 @@ module Unsafe : sig
   val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list ->
     Proofview_monad.goal_with_state list
 
-  val typeclass_resolvable : unit Evd.Store.field
-
 end
 
 (** This module gives access to the innards of the monad. Its use is
@@ -507,7 +505,6 @@ module Goal : sig
   val hyps : t -> named_context
   val env : t -> Environ.env
   val sigma : t -> Evd.evar_map
-  val extra : t -> Evd.Store.t
   val state : t -> Proofview_monad.StateStore.t
 
   (** [nf_enter t] applies the goal-dependent tactic [t] in each goal
diff --git a/engine/termops.ml b/engine/termops.ml
index e1f5fb0d7f..c4b57e4dd2 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -365,12 +365,18 @@ let pr_evar_map_gen with_univs pr_evars sigma =
     else
     str "CONSTRAINTS:" ++ brk (0, 1) ++
       pr_evar_constraints sigma conv_pbs ++ fnl ()
+  and unresolvables =
+    let evars = Evd.unresolvable_evars sigma in
+    if Evar.Set.is_empty evars then mt ()
+    else
+      str "UNRESOLVABLE:" ++ brk (0, 1) ++
+      prlist_with_sep spc (pr_existential_key sigma) (Evar.Set.elements evars) ++ fnl ()
   and metas =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
       str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
   in
-  evs ++ svs ++ cstrs ++ metas
+  evs ++ svs ++ cstrs ++ unresolvables ++ metas
 
 let pr_evar_list sigma l =
   let open Evd in