Merge branch 'v8.5'

2 files changed, 116 insertions, 67 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 8f8b29d10..bcbf99e87 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -208,15 +208,6 @@ let map_evar_info f evi =
     evar_concl = f evi.evar_concl;
     evar_candidates = Option.map (List.map f) evi.evar_candidates }
 
-let evar_ident_info evi =
-  match evi.evar_source with
-  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
-  | _,Evar_kinds.VarInstance id -> id
-  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
-  | _ ->
-      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
-      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
-
 (* This exception is raised by *.existential_value *)
 exception NotInstantiatedEvar
 
@@ -363,11 +354,86 @@ type evar_constraint = conv_pb * Environ.env * constr * constr
 
 module EvMap = Evar.Map
 
+module EvNames :
+sig
+
+open Misctypes
+
+type t
+
+val empty : t
+val add_name_newly_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val remove_name_defined : Evar.t -> t -> t
+val rename : Evar.t -> Id.t -> t -> t
+val reassign_name_defined : Evar.t -> Evar.t -> t -> t
+val ident : Evar.t -> t -> Id.t option
+val key : Id.t -> t -> Evar.t
+
+end =
+struct
+
+type t = Id.t EvMap.t * existential_key Idmap.t
+
+let empty = (EvMap.empty, Idmap.empty)
+
+let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) =
+  let id = match naming with
+  | Misctypes.IntroAnonymous -> None
+  | Misctypes.IntroIdentifier id ->
+    if Idmap.mem id idtoev then
+    user_err_loc
+      (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
+    Some id
+  | Misctypes.IntroFresh id ->
+    let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
+    Some id
+  in
+  match id with
+  | None -> names
+  | Some id -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+
+let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
+  if EvMap.mem evk evtoid then
+    evar_names
+  else
+    add_name_newly_undefined naming evk evi evar_names
+
+let remove_name_defined evk (evtoid, idtoev as names) =
+  let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
+  match id with
+  | None -> names
+  | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev)
+
+let rename evk id (evtoid, idtoev) =
+  let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in
+  match id' with
+  | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+  | Some id' ->
+    if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
+    (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
+
+let reassign_name_defined evk evk' (evtoid, idtoev as names) =
+  let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
+  match id with
+  | None -> names (** evk' must not be defined *)
+  | Some id ->
+    (EvMap.add evk' id (EvMap.remove evk evtoid),
+    Idmap.add id evk' (Idmap.remove id idtoev))
+
+let ident evk (evtoid, _) =
+  try Some (EvMap.find evk evtoid) with Not_found -> None
+
+let key id (_, idtoev) =
+  Idmap.find id idtoev
+
+end
+
 type evar_map = {
   (** Existential variables *)
   defn_evars : evar_info EvMap.t;
   undf_evars : evar_info EvMap.t;
-  evar_names : Id.t EvMap.t * existential_key Idmap.t;
+  evar_names : EvNames.t;
   (** Universes *)
   universes  : evar_universe_context;
   (** Conversion problems *)
@@ -392,55 +458,15 @@ type evar_map = {
 
 (*** Lifting primitive from Evar.Map. ***)
 
-let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
-  let id = match naming with
-  | Misctypes.IntroAnonymous ->
-      let id = evar_ident_info evi in
-      Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev)
-  | Misctypes.IntroIdentifier id ->
-      let id' =
-        Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
-      if not (Names.Id.equal id id') then
-        user_err_loc
-          (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
-      id'
-  | Misctypes.IntroFresh id ->
-      Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
-  (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
-
-let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
-  if EvMap.mem evk evtoid then
-    evar_names
-  else
-    add_name_newly_undefined naming evk evi evar_names
-
-let remove_name_defined evk (evtoid,idtoev) =
-  let id = EvMap.find evk evtoid in
-  (EvMap.remove evk evtoid, Idmap.remove id idtoev)
-
-let remove_name_possibly_already_defined evk evar_names =
-  try remove_name_defined evk evar_names
-  with Not_found -> evar_names
-
 let rename evk id evd =
-  let (evtoid,idtoev) = evd.evar_names in
-  let id' = EvMap.find evk evtoid in
-  if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
-  { evd with evar_names =
-      (EvMap.add evk id evtoid (* overwrite old name *),
-       Idmap.add id evk (Idmap.remove id' idtoev)) }
-
-let reassign_name_defined evk evk' (evtoid,idtoev) =
-  let id = EvMap.find evk evtoid in
-  (EvMap.add evk' id (EvMap.remove evk evtoid),
-   Idmap.add id evk' (Idmap.remove id idtoev))
+  { evd with evar_names = EvNames.rename evk id evd.evar_names }
 
 let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with
 | Evar_empty ->
-  let evar_names = add_name_undefined naming e i d.evar_names in
+  let evar_names = EvNames.add_name_undefined naming e i d.evar_names in
   { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
 | Evar_defined _ ->
-  let evar_names = remove_name_possibly_already_defined e d.evar_names in
+  let evar_names = EvNames.remove_name_defined e d.evar_names in
   { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
 let add d e i = add_with_name d e i
@@ -583,7 +609,7 @@ let empty = {
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
   effects    = Safe_typing.empty_private_constants;
-  evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
+  evar_names = EvNames.empty; (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
   extras = Store.empty;
@@ -619,14 +645,8 @@ let add_conv_pb ?(tail=false) pb d =
 
 let evar_source evk d = (find d evk).evar_source
 
-let evar_ident evk evd =
-  try EvMap.find evk (fst evd.evar_names)
-  with Not_found ->
-    (* Unnamed (non-dependent) evar *)
-    add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk))
-
-let evar_key id evd =
-  Idmap.find id (snd evd.evar_names)
+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 =
@@ -648,7 +668,7 @@ let define evk body evd =
   | [] ->  evd.last_mods
   | _ -> Evar.Set.add evk evd.last_mods
   in
-  let evar_names = remove_name_defined evk evd.evar_names in
+  let evar_names = EvNames.remove_name_defined evk evd.evar_names in
   { evd with defn_evars; undf_evars; last_mods; evar_names }
 
 let restrict evk filter ?candidates evd =
@@ -658,7 +678,7 @@ let restrict evk filter ?candidates evd =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
       evar_extra = Store.empty } in
-  let evar_names = reassign_name_defined evk evk' evd.evar_names in
+  let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
   let body = mkEvar(evk',id_inst) in
@@ -1196,7 +1216,34 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (**********************************************************)
 (* Pretty-printing *)
 
-let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma)
+let pr_evar_suggested_name evk sigma =
+  let base_id evk' evi =
+  match evar_ident evk' sigma with
+  | Some id -> id
+  | None -> match evi.evar_source with
+  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
+  | _,Evar_kinds.VarInstance id -> id
+  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
+  | _ ->
+      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
+      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+  in
+  let names = EvMap.mapi base_id sigma.undf_evars in
+  let id = EvMap.find evk names in
+  let fold evk' id' (seen, n) =
+    if seen then (seen, n)
+    else if Evar.equal evk evk' then (true, n)
+    else if Id.equal id id' then (seen, succ n)
+    else (seen, n)
+  in
+  let (_, n) = EvMap.fold fold names (false, 0) in
+  if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n))
+
+let pr_existential_key sigma evk = match evar_ident evk sigma with
+| None ->
+  str "?" ++ pr_id (pr_evar_suggested_name evk sigma)
+| Some id ->
+  str "?" ++ pr_id id
 
 let pr_instance_status (sc,typ) =
   begin match sc with
@@ -1385,7 +1432,7 @@ let pr_evar_list sigma l =
     h 0 (str (string_of_existential ev) ++
       str "==" ++ pr_evar_info evi ++
       (if evi.evar_body == Evar_empty
-       then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}"
+       then str " {" ++  pr_existential_key sigma ev ++ str "}"
        else mt ()))
   in
   h 0 (prlist_with_sep fnl pr l)
diff --git a/engine/evd.mli b/engine/evd.mli
index c8753b9c0..a9ca9a740 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -246,7 +246,7 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 (** Convenience function. Wrapper around {!find} to recover the source of an
     evar in a given evar map. *)
 
-val evar_ident : existential_key -> evar_map -> Id.t
+val evar_ident : existential_key -> evar_map -> Id.t option
 
 val rename : existential_key -> Id.t -> evar_map -> evar_map
 
@@ -597,6 +597,8 @@ type unsolvability_explanation = SeveralInstancesFound of int
 
 val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
 
+val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
+
 (** {5 Debug pretty-printers} *)
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds