From 7eeec8f82d96a71929289b0b9401a1b96e1d3dda Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Feb 2016 10:26:28 +0100 Subject: More compact representation for evar resolvability flag. This patch was proposed by JH in bug report #4547. --- pretyping/typeclasses.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'pretyping') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 3be98a1ae2..bb475cc554 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -495,15 +495,18 @@ let is_instance = function let resolvable = Store.field () let set_resolvable s b = - Store.set s resolvable b + if b then Store.remove s resolvable + else Store.set s resolvable () let is_resolvable evi = assert (match evi.evar_body with Evar_empty -> true | _ -> false); - Option.default true (Store.get evi.evar_extra resolvable) + Option.is_empty (Store.get evi.evar_extra resolvable) let mark_resolvability_undef b evi = - let t = Store.set evi.evar_extra resolvable b in - { evi with evar_extra = t } + if is_resolvable evi = b then evi + else + let t = set_resolvable evi.evar_extra b in + { evi with evar_extra = t } let mark_resolvability b evi = assert (match evi.evar_body with Evar_empty -> true | _ -> false); -- cgit v1.2.3 From 0ee0b7d2f2365da6e63bc2e94d66f9c5fe1ebe6a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Feb 2016 11:28:34 +0100 Subject: Opacifying the type of evar naming structure in Evd. --- pretyping/evd.ml | 124 +++++++++++++++++++++++++++++++++---------------------- 1 file changed, 74 insertions(+), 50 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5441145189..8be09a7821 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -575,34 +575,28 @@ type evar_constraint = conv_pb * Environ.env * constr * constr module EvMap = Evar.Map -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; - (** Universes *) - universes : evar_universe_context; - (** Conversion problems *) - conv_pbs : evar_constraint list; - last_mods : Evar.Set.t; - (** Metas *) - metas : clbinding Metamap.t; - (** Interactive proofs *) - effects : Safe_typing.private_constants; - future_goals : Evar.t list; (** list of newly created evars, to be - eventually turned into goals if not solved.*) - principal_future_goal : Evar.t option; (** if [Some e], [e] must be - contained - [future_goals]. The evar - [e] will inherit - properties (now: the - name) of the evar which - will be instantiated with - a term containing [e]. *) - extras : Store.t; -} +module EvNames : +sig -(*** Lifting primitive from Evar.Map. ***) +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 +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) = let id = match naming with @@ -630,29 +624,65 @@ 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 rename evk id (evtoid, idtoev) = 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)) } + (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)) +let ident evk (evtoid, _) = + try EvMap.find evk evtoid + with Not_found -> + (* Unnamed (non-dependent) evar *) + add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk)) + +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 : EvNames.t; + (** Universes *) + universes : evar_universe_context; + (** Conversion problems *) + conv_pbs : evar_constraint list; + last_mods : Evar.Set.t; + (** Metas *) + metas : clbinding Metamap.t; + (** Interactive proofs *) + effects : Safe_typing.private_constants; + future_goals : Evar.t list; (** list of newly created evars, to be + eventually turned into goals if not solved.*) + principal_future_goal : Evar.t option; (** if [Some e], [e] must be + contained + [future_goals]. The evar + [e] will inherit + properties (now: the + name) of the evar which + will be instantiated with + a term containing [e]. *) + extras : Store.t; +} + +(*** Lifting primitive from Evar.Map. ***) + +let rename evk id evd = + { evd with evar_names = EvNames.rename evk id evd.evar_names } + let add d e i = match i.evar_body with | Evar_empty -> - let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in + let evar_names = EvNames.add_name_undefined Misctypes.IntroAnonymous 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 = try EvNames.remove_name_defined e d.evar_names with Not_found -> d.evar_names in { d with defn_evars = EvMap.add e i d.defn_evars; evar_names } let remove d e = @@ -783,7 +813,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; @@ -819,14 +849,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 = @@ -848,7 +872,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 evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) @@ -868,7 +892,7 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evar_candidates = candidates; evar_extra = store; } in - let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in + let evar_names = EvNames.add_name_newly_undefined naming evk evar_info evd.evar_names in { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names } let restrict evk evk' filter ?candidates evd = @@ -877,7 +901,7 @@ let restrict evk 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 -- cgit v1.2.3 From 62c141be71dd3c542824c19429eac0fdd686c9cb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Feb 2016 18:39:15 +0100 Subject: Optimizing the computation of frozen evars. --- pretyping/unification.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f97f6fbc57..6cb1bc7028 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1450,9 +1450,7 @@ let default_matching_core_flags sigma = check_applied_meta_types = true; use_pattern_unification = false; use_meta_bound_pattern_unification = false; - frozen_evars = - fold_undefined (fun evk _ evars -> Evar.Set.add evk evars) - sigma Evar.Set.empty; + frozen_evars = Evar.Map.domain (Evd.undefined_map sigma); restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = false; -- cgit v1.2.3 From f46a5686853353f8de733ae7fbd21a3a61977bc7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Feb 2016 15:32:58 +0100 Subject: Do not give a name to anonymous evars anymore. See bug #4547. The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced. --- pretyping/detyping.ml | 5 ++- pretyping/evarutil.ml | 9 +---- pretyping/evd.ml | 103 ++++++++++++++++++++++++++++++-------------------- pretyping/evd.mli | 4 +- 4 files changed, 71 insertions(+), 50 deletions(-) (limited to 'pretyping') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c3877c56e4..0c487ced81 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -518,7 +518,10 @@ let rec detype flags avoid env sigma t = with Not_found -> isVarId id c in let id,l = try - let id = Evd.evar_ident evk sigma in + let id = match Evd.evar_ident evk sigma with + | None -> Evd.pr_evar_suggested_name evk sigma + | Some id -> id + in let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index e23e5a53a7..759e0e4d6d 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -365,14 +365,7 @@ let new_pure_evar_full evd evi = (evd, evk) let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?naming ?(principal=false) typ = - let default_naming = - if principal then - (* waiting for a more principled approach - (unnamed evars, private names?) *) - Misctypes.IntroFresh (Names.Id.of_string "tmp_goal") - else - Misctypes.IntroAnonymous - in + let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let newevk = new_untyped_evar() in let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 8be09a7821..0bc688aacf 100644 --- a/pretyping/evd.ml +++ b/pretyping/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 @@ -588,7 +579,7 @@ val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> 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 +val ident : Evar.t -> t -> Id.t option val key : Id.t -> t -> Evar.t end = @@ -598,21 +589,21 @@ 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) = +let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) = 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.IntroAnonymous -> None | 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' + 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 -> - Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in - (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + 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 @@ -620,25 +611,30 @@ let add_name_undefined naming evk evi (evtoid,idtoev as 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_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' = EvMap.find evk evtoid in - if Idmap.mem id idtoev then anomaly (str "Evar name already in use"); - (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)) + 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 EvMap.find evk evtoid - with Not_found -> - (* Unnamed (non-dependent) evar *) - add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk)) + try Some (EvMap.find evk evtoid) with Not_found -> None let key id (_, idtoev) = Idmap.find id idtoev @@ -682,7 +678,7 @@ let add d e i = match i.evar_body with let evar_names = EvNames.add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } | Evar_defined _ -> - let evar_names = try EvNames.remove_name_defined e d.evar_names with Not_found -> 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 remove d e = @@ -1706,7 +1702,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 @@ -1895,7 +1918,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/pretyping/evd.mli b/pretyping/evd.mli index 9cfca02ed8..d2479c1229 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -249,7 +249,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 @@ -603,6 +603,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 -- cgit v1.2.3