Refine test for unresolved evars: not reachable from initial evars

The test is refined to handle aliases: i.e. undefined evars coming from
restrictions and evar-evar unifications with an initial evar are not
considered fresh unresolved evars. To check this, we generalize the
restricted_evars set to an aliased_evars set in the evar map,
registering evars being solved by another evar due to restriction
or evar-evar unifications. This implements the proposal of PR #370
for testing the resolution status of evars independently of the evar-evar
orientation order.

This allows [apply] to refine an evar with a new one if it results from a
[clear] request or an evar-evar solution only, otherwise the new evar is
considered fresh and an error is raised.

Also fixes bugs #4095 and #4413.

Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>

7 files changed, 128 insertions, 99 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index d719731464..771571fd3f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -516,12 +516,7 @@ let restrict_evar evd evk filter ?src candidates =
   let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in
   match candidates with
   | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None))
-  | _ ->
-     let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
-     (* Mark new evar as future goal, removing previous one,
-        circumventing Proofview.advance but making Proof.run_tactic catch these. *)
-     let evd = Evd.remove_future_goal evd evk in
-     (Evd.declare_future_goal evk' evd, evk')
+  | _ -> Evd.restrict evk filter ?candidates ?src evd
 
 let rec check_and_clear_in_constr env evdref err ids global c =
   (* returns a new constr where all the evars have been 'cleaned'
@@ -703,10 +698,22 @@ let rec advance sigma evk =
   match evi.evar_body with
   | Evar_empty -> Some evk
   | Evar_defined v ->
-      match is_restricted_evar sigma evk with
+      match is_aliased_evar sigma evk with
       | Some evk -> advance sigma evk
       | None -> None
 
+let reachable_from_evars sigma evars =
+  let aliased = Evd.get_aliased_evars sigma in
+  let rec search evk visited =
+    if Evar.Set.mem evk visited then visited
+    else
+      let visited = Evar.Set.add evk visited in
+      match Evar.Map.find evk aliased with
+      | evk' -> search evk' visited
+      | exception Not_found -> visited
+  in
+  Evar.Set.fold (fun evk visited -> search evk visited) evars Evar.Set.empty
+
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 9d2c29547e..6e1f67021f 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -112,6 +112,10 @@ val gather_dependent_evars : evar_map -> Evar.t list -> (Evar.Set.t option) Evar
     solved. *)
 val advance : evar_map -> Evar.t -> Evar.t option
 
+(** [reachable_from_evars sigma seeds] computes the descendents of
+    evars in [seeds] by restriction or evar-evar unifications in [sigma]. *)
+val reachable_from_evars : evar_map -> Evar.Set.t -> Evar.Set.t
+
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and
@@ -234,8 +238,8 @@ exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t opti
 
 (** Restrict an undefined evar according to a (sub)filter and candidates.
     The evar will be defined if there is only one candidate left,
-@raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates
-  into an empty list. *)
+    @raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates
+    into an empty list. *)
 
 val restrict_evar : evar_map -> Evar.t -> Filter.t ->
   ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t
diff --git a/engine/evd.ml b/engine/evd.ml
index 65df2643f2..4ae1d034d7 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -453,7 +453,7 @@ end
 
 type evar_flags =
   { obligation_evars : Evar.Set.t;
-    restricted_evars : Evar.t Evar.Map.t;
+    aliased_evars : Evar.t Evar.Map.t;
     typeclass_evars : Evar.Set.t }
 
 type side_effect_role =
@@ -631,7 +631,7 @@ let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body
     associated to an evar, so we prevent registering its typeclass status. *)
 let add d e i = add_with_name ~typeclass_candidate:false d e i
 
-(*** Evar flags: typeclasses, restricted or obligation flag *)
+(*** Evar flags: typeclasses, aliased or obligation flag *)
 
 let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
 
@@ -659,29 +659,28 @@ let is_obligation_evar evd evk =
 let inherit_evar_flags evar_flags evk evk' =
   let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
   let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
-  if not (evk_obligation || evk_typeclass) then evar_flags
-  else
-    let typeclass_evars =
-      if evk_typeclass then
-        let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
-        Evar.Set.add evk' typeclass_evars
-      else evar_flags.typeclass_evars
-    in
-    let obligation_evars =
-      if evk_obligation then
-        let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
-        Evar.Set.add evk' obligation_evars
-      else evar_flags.obligation_evars
-    in
-    { evar_flags with obligation_evars; typeclass_evars }
+  let aliased_evars = Evar.Map.add evk evk' evar_flags.aliased_evars in
+  let typeclass_evars =
+    if evk_typeclass then
+      let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
+      Evar.Set.add evk' typeclass_evars
+    else evar_flags.typeclass_evars
+  in
+  let obligation_evars =
+    if evk_obligation then
+      let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
+      Evar.Set.add evk' obligation_evars
+    else evar_flags.obligation_evars
+  in
+  { obligation_evars; aliased_evars; typeclass_evars }
 
 (** Removal: in all other cases of definition *)
 
 let remove_evar_flags evk evar_flags =
   { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
     obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
-    (* Restriction information is kept. *)
-    restricted_evars = evar_flags.restricted_evars }
+    (* Aliasing information is kept. *)
+    aliased_evars = evar_flags.aliased_evars }
 
 (** New evars *)
 
@@ -809,7 +808,7 @@ let create_evar_defs sigma = { sigma with
 
 let empty_evar_flags =
   { obligation_evars = Evar.Set.empty;
-    restricted_evars = Evar.Map.empty;
+    aliased_evars = Evar.Map.empty;
     typeclass_evars = Evar.Set.empty }
 
 let empty_side_effects = {
@@ -872,71 +871,12 @@ 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 define_aux def undef evk body =
-  let oldinfo =
-    try EvMap.find evk undef
-    with Not_found ->
-      if EvMap.mem evk def then
-        anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.")
-      else
-        anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
-  in
-  let () = assert (oldinfo.evar_body == Evar_empty) 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 *)
-let define_gen evk body evd evar_flags =
-  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
-  let last_mods = match evd.conv_pbs with
-  | [] ->  evd.last_mods
-  | _ -> 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; evar_flags }
+let get_aliased_evars evd = evd.evar_flags.aliased_evars
 
-(** By default, the obligation and evar tag of the evar is removed *)
-let define evk body evd =
-  let evar_flags = remove_evar_flags evk evd.evar_flags in
-  define_gen evk body evd evar_flags
-
-(** In case of an evar-evar solution, the flags are inherited *)
-let define_with_evar evk body evd =
-  let evk' = fst (destEvar body) in
-  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
-  define_gen evk body evd evar_flags
-
-let is_restricted_evar evd evk =
-  try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
+let is_aliased_evar evd evk =
+  try Some (Evar.Map.find evk evd.evar_flags.aliased_evars)
   with Not_found -> None
 
-let declare_restricted_evar evar_flags evk evk' =
-  { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
-
-(* In case of restriction, we declare the restriction and inherit the obligation
-   and typeclass flags. *)
-
-let restrict evk filter ?candidates ?src evd =
-  let evk' = new_untyped_evar () in
-  let evar_info = EvMap.find evk evd.undf_evars in
-  let id_inst = Filter.filter_list filter evar_info.evar_hyps.env_named_var in
-  let evar_info' =
-    { evar_info with evar_filter = filter;
-      evar_candidates = candidates;
-      evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
-      evar_identity = Identity.make id_inst;
-    } in
-  let last_mods = match evd.conv_pbs with
-  | [] ->  evd.last_mods
-  | _ -> Evar.Set.add evk evd.last_mods in
-  let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
-  let body = mkEvar(evk',id_inst) 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_evar_flags evar_flags evk evk' in
-  { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; last_mods; evar_names; evar_flags }, evk'
-
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
   let evar_info' = { evar_info with evar_concl = ccl } in
@@ -1224,6 +1164,73 @@ let pr_shelf evd =
   if List.is_empty evd.shelf then str"(empty stack)"
   else prlist_with_sep (fun () -> str"||") (prlist_with_sep spc Evar.print) evd.shelf
 
+let define_aux def undef evk body =
+  let oldinfo =
+    try EvMap.find evk undef
+    with Not_found ->
+      if EvMap.mem evk def then
+        anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.")
+      else
+        anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
+  in
+  let () = assert (oldinfo.evar_body == Evar_empty) 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 *)
+let define_gen evk body evd evar_flags =
+  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+  let last_mods = match evd.conv_pbs with
+  | [] ->  evd.last_mods
+  | _ -> 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; evar_flags }
+
+(** By default, the obligation and evar tag of the evar is removed *)
+let define evk body evd =
+  let evar_flags = remove_evar_flags evk evd.evar_flags in
+  define_gen evk body evd evar_flags
+
+(** In case of an evar-evar solution, the flags are inherited *)
+let define_with_evar evk body evd =
+  let evk' = fst (destEvar body) in
+  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+  let evd = unshelve evd [evk] in
+  let future_goals = FutureGoals.remove evk evd.future_goals in
+  let evd = { evd with future_goals } in
+  define_gen evk body evd evar_flags
+
+(* In case of restriction, we declare the aliasing and inherit the obligation
+   and typeclass flags. *)
+
+let restrict evk filter ?candidates ?src evd =
+  let evk' = new_untyped_evar () in
+  let evar_info = EvMap.find evk evd.undf_evars in
+  let id_inst = Filter.filter_list filter evar_info.evar_hyps.env_named_var in
+  let evar_info' =
+    { evar_info with evar_filter = filter;
+      evar_candidates = candidates;
+      evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
+      evar_identity = Identity.make id_inst;
+    } in
+  let last_mods = match evd.conv_pbs with
+  | [] ->  evd.last_mods
+  | _ -> Evar.Set.add evk evd.last_mods in
+  let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
+  let body = mkEvar(evk',id_inst) in
+  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+  let evd = { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
+    defn_evars; last_mods; evar_names; evar_flags }
+  in
+  (* Mark new evar as future goal, removing previous one,
+    circumventing Proofview.advance but making Proof.run_tactic catch these. *)
+  let evd = unshelve evd [evk] in
+  let evd = remove_future_goal evd evk in
+  let evd = declare_future_goal evk' evd in
+  (evd, evk')
+
 (**********************************************************)
 (* Accessing metas *)
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 9394f9a9dd..fafaad9a04 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -284,8 +284,11 @@ 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_map -> Evar.t -> Evar.t option
-(** Tell if an evar comes from restriction of another evar, and if yes, which *)
+val get_aliased_evars : evar_map -> Evar.t Evar.Map.t
+(** The map of aliased evars *)
+
+val is_aliased_evar : evar_map -> Evar.t -> Evar.t option
+(** Tell if an evar has been aliased to another evar, and if yes, which *)
 
 val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map
 (** Mark the given set of evars as available for resolution.
@@ -388,7 +391,6 @@ val pop_future_goals : evar_map -> FutureGoals.t * evar_map
 
 val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
 
-
 val remove_future_goal : evar_map -> Evar.t -> evar_map
 
 val pr_future_goals_stack : evar_map -> Pp.t
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index df9fc5dab3..80263694f5 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -202,6 +202,11 @@ module type State = sig
   val modify : (t->t) -> unit Logical.t
 end
 
+module type Reader = sig
+  type t
+  val get : t Logical.t
+end
+
 module type Writer = sig
   type t
   val put : t -> unit Logical.t
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 6cca3f5a5e..00d322858d 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -79,7 +79,7 @@ val with_empty_state : goal -> goal_with_state
 val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
 
 (** Type of proof views: current [evar_map] together with the list of
-    focused goals. *)
+    focused goals, locally shelved goals and globally shelved goals. *)
 type proofview = {
   solution : Evd.evar_map;
   comb : goal_with_state list;
@@ -115,6 +115,10 @@ module type State = sig
   val set : t -> unit Logical.t
   val modify : (t->t) -> unit Logical.t
 end
+module type Reader = sig
+  type t
+  val get : t Logical.t
+end
 
 module type Writer = sig
   type t
diff --git a/engine/termops.ml b/engine/termops.ml
index ac6870a39e..0923ab6f4b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -310,15 +310,15 @@ let pr_evar_map_gen with_univs pr_evars env sigma =
 
 let pr_evar_list env sigma l =
   let open Evd in
-  let pr_restrict ev =
-    match is_restricted_evar sigma ev with
+  let pr_alias ev =
+    match is_aliased_evar sigma ev with
     | None -> mt ()
-    | Some ev' -> str " (restricted to " ++ Evar.print ev' ++ str ")"
+    | Some ev' -> str " (aliased to " ++ Evar.print ev' ++ str ")"
   in
   let pr (ev, evi) =
     h 0 (Evar.print ev ++
       str "==" ++ pr_evar_info env sigma evi ++
-      pr_restrict ev ++
+      pr_alias ev ++
       (if evi.evar_body == Evar_empty
        then str " {" ++ pr_existential_key sigma ev ++ str "}"
        else mt ()))