aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-13 17:36:16 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-13 17:51:34 +0100
commit97e1fccd878190a1fc51a1da45f4c06369c0e3db (patch)
tree27e38c1ae4c8ebef7dc7f8f893ccc8f93aee8227 /engine
parente9675e068f9e0e92bab05c030fb4722b146123b8 (diff)
parentf46a5686853353f8de733ae7fbd21a3a61977bc7 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml179
-rw-r--r--engine/evd.mli4
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