From d437078a4ca82f7ca6d19be5ee9452359724f9a0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:46:30 +0200 Subject: Use Maps and ids for universe binders Before sometimes there were lists and strings. --- API/API.mli | 2 +- engine/evd.ml | 2 +- engine/evd.mli | 14 +++++++------- engine/uState.ml | 33 +++++++++++++++++---------------- engine/uState.mli | 6 +++--- engine/universes.ml | 8 +++++--- engine/universes.mli | 4 +++- interp/declare.ml | 8 ++++---- pretyping/pretyping.ml | 25 ++++++++++++------------- pretyping/univdecls.ml | 2 +- vernac/classes.ml | 4 ++-- vernac/command.ml | 2 +- vernac/obligations.ml | 4 ++-- vernac/record.ml | 2 +- 14 files changed, 60 insertions(+), 56 deletions(-) diff --git a/API/API.mli b/API/API.mli index d912dc771..63c675221 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2869,7 +2869,7 @@ sig val clear_metas : evar_map -> evar_map (** Allocates a new evar that represents a {i sort}. *) - val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t + val new_sort_variable : ?loc:Loc.t -> ?name:Names.Id.t -> rigid -> evar_map -> evar_map * Sorts.t val remove : evar_map -> Evar.t -> evar_map val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> Environ.env -> diff --git a/engine/evd.ml b/engine/evd.ml index 60bd6de2a..ca1196b94 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -802,7 +802,7 @@ let make_evar_universe_context e l = | Some us -> List.fold_left (fun uctx (loc,id) -> - fst (UState.new_univ_variable ?loc univ_rigid (Some (Id.to_string id)) uctx)) + fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx)) uctx us (****************************************) diff --git a/engine/evd.mli b/engine/evd.mli index 853a34bc4..36c399e98 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -502,12 +502,12 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t val evar_universe_context_of_binders : Universes.universe_binders -> UState.t - + val make_evar_universe_context : env -> (Id.t located) list option -> UState.t -val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map +val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) -val universe_of_name : evar_map -> string -> Univ.Level.t -val add_universe_name : evar_map -> string -> Univ.Level.t -> evar_map +val universe_of_name : evar_map -> Id.t -> Univ.Level.t +val add_universe_name : evar_map -> Id.t -> Univ.Level.t -> evar_map val add_constraints_context : UState.t -> Univ.constraints -> UState.t @@ -519,9 +519,9 @@ val normalize_evar_universe_context_variables : UState.t -> val normalize_evar_universe_context : UState.t -> UState.t -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Level.t -val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Universe.t -val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t +val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t +val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t +val new_sort_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Sorts.t val add_global_univ : evar_map -> Univ.Level.t -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 123b64314..498d73fd3 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -11,16 +11,16 @@ open CErrors open Util open Names -module UNameMap = String.Map +module UNameMap = Names.Id.Map type uinfo = { - uname : string option; + uname : Id.t option; uloc : Loc.t option; } (* 2nd part used to check consistency on the fly. *) type t = - { uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t; + { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t; uctx_local : Univ.ContextSet.t; (** The local context of variables *) uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) @@ -107,10 +107,12 @@ let add_uctx_loc l loc (names, names_rev) = let of_binders b = let ctx = empty in - let names = - List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc) - ctx.uctx_names b - in { ctx with uctx_names = names } + let rmap = + UNameMap.fold (fun id l rmap -> + Univ.LMap.add l { uname = Some id; uloc = None } rmap) + b Univ.LMap.empty + in + { ctx with uctx_names = b, rmap } let instantiate_variable l b v = try v := Univ.LMap.update l (Some b) !v @@ -249,20 +251,20 @@ let constrain_variables diff ctx = let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try str (Option.get (Univ.LMap.find l map_rev).uname) + try Id.print (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> Universes.pr_with_global_universes l type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl -let universe_context ~names ~extensible ctx = - let levels = Univ.ContextSet.levels ctx.uctx_local in +let universe_context ~names ~extensible uctx = + let levels = Univ.ContextSet.levels uctx.uctx_local in let newinst, left = List.fold_right (fun (loc,id) (newinst, acc) -> let l = - try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) + try UNameMap.find id (fst uctx.uctx_names) with Not_found -> user_err ?loc ~hdr:"universe_context" (str"Universe " ++ Id.print id ++ str" is not bound anymore.") @@ -274,23 +276,22 @@ let universe_context ~names ~extensible ctx = let loc = try let info = - Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in + Univ.LMap.find (Univ.LSet.choose left) (snd uctx.uctx_names) in info.uloc with Not_found -> None in user_err ?loc ~hdr:"universe_context" ((str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level ctx) left ++ + Univ.LSet.pr (pr_uctx_level uctx) left ++ spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")) else let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in let inst = Array.append (Array.of_list newinst) left in let inst = Univ.Instance.of_array inst in - let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints ctx.uctx_local) in - map, ctx + Univ.ContextSet.constraints uctx.uctx_local) in + fst uctx.uctx_names, ctx let check_implication uctx cstrs ctx = let gr = initial_graph uctx in diff --git a/engine/uState.mli b/engine/uState.mli index f54bcc832..7f2357a68 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -71,10 +71,10 @@ val add_universe_constraints : t -> Universes.universe_constraints -> t (** {5 Names} *) -val add_universe_name : t -> string -> Univ.Level.t -> t +val add_universe_name : t -> Id.t -> Univ.Level.t -> t (** Associate a human-readable name to a local variable. *) -val universe_of_name : t -> string -> Univ.Level.t +val universe_of_name : t -> Id.t -> Univ.Level.t (** Retrieve the universe associated to the name. *) (** {5 Unification} *) @@ -93,7 +93,7 @@ val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t val merge_subst : t -> Universes.universe_opt_subst -> t val emit_side_effects : Safe_typing.private_constants -> t -> t -val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t +val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t val add_global_univ : t -> Univ.Level.t -> t (** [make_flexible_variable g algebraic l] diff --git a/engine/universes.ml b/engine/universes.ml index 6c1b64d74..459c53002 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -21,14 +21,16 @@ let pr_with_global_universes l = (** Local universe names of polymorphic references *) -type universe_binders = (Id.t * Univ.Level.t) list +type universe_binders = Univ.Level.t Names.Id.Map.t + +let empty_binders = Id.Map.empty let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" -let universe_binders_of_global ref = +let universe_binders_of_global ref : universe_binders = try let l = Refmap.find ref !universe_binders_table in l - with Not_found -> [] + with Not_found -> Names.Id.Map.empty let register_universe_binders ref l = universe_binders_table := Refmap.add ref l !universe_binders_table diff --git a/engine/universes.mli b/engine/universes.mli index a960099ed..621ca5e84 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -21,7 +21,9 @@ val pr_with_global_universes : Level.t -> Pp.t (** Local universe name <-> level mapping *) -type universe_binders = (Id.t * Univ.Level.t) list +type universe_binders = Univ.Level.t Names.Id.Map.t + +val empty_binders : universe_binders val register_universe_binders : Globnames.global_reference -> universe_binders -> unit val universe_binders_of_global : Globnames.global_reference -> universe_binders diff --git a/interp/declare.ml b/interp/declare.ml index 7ab13b859..dc77981f2 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -462,11 +462,11 @@ type universe_decl = polymorphic * Universes.universe_binders let cache_universes (p, l) = let glob = Global.global_universe_names () in let glob', ctx = - List.fold_left (fun ((idl,lid),ctx) (id, lev) -> + Id.Map.fold (fun id lev ((idl,lid),ctx) -> ((Id.Map.add id (p, lev) idl, Univ.LMap.add lev id lid), Univ.ContextSet.add_universe lev ctx)) - (glob, Univ.ContextSet.empty) l + l (glob, Univ.ContextSet.empty) in cache_universe_context (p, ctx); Global.set_global_universe_names glob' @@ -487,9 +487,9 @@ let do_universe poly l = (str"Cannot declare polymorphic universes outside sections") in let l = - List.map (fun (l, id) -> + List.fold_left (fun acc (l, id) -> let lev = Universes.new_univ_level (Global.current_dirpath ()) in - (id, lev)) l + Id.Map.add id lev acc) Id.Map.empty l in Lib.add_anonymous_leaf (input_universes (poly, l)) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e3470b0f1..ffbc21a5e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -181,9 +181,8 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = match s with | Anonymous -> new_univ_level_variable ?loc anon_rigidity evd - | Name s -> - let s = Id.to_string s in - let names, _ = Global.global_universe_names () in + | Name id -> + let s = Id.to_string id in if CString.string_contains ~where:s ~what:"." then match List.rev (CString.split '.' s) with | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") @@ -197,17 +196,17 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = in evd, level else try - let level = Evd.universe_of_name evd s in - evd, level + let level = Evd.universe_of_name evd id in + evd, level with Not_found -> - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, snd (Id.Map.find id names) - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc ~name:s univ_rigid evd - else user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) + try + let names, _ = Global.global_universe_names () in + evd, snd (Id.Map.find id names) + with Not_found -> + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:id univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ str s)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index 5576e33f4..a5266125a 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -31,7 +31,7 @@ let interp_univ_constraints env evd cstrs = user_err ~hdr:"interp_constraint" (str "Cannot declare constraints on anonymous universes") | GType (Some (loc, Name id)) -> - try loc, Evd.universe_of_name evd (Id.to_string id) + try loc, Evd.universe_of_name evd id with Not_found -> user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ Id.print id) in diff --git a/vernac/classes.ml b/vernac/classes.ml index 20cb43b24..ed37bab6d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -411,14 +411,14 @@ let context poly l = let decl = (Discharge, poly, Definitional) in let nstatus = match b with | None -> - pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl + pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> let ctx = Univ.ContextSet.to_context !uctx in let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in - let _ = DeclareDef.declare_definition id decl entry [] [] hook in + let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/command.ml b/vernac/command.ml index 257c003b5..5d83de070 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -258,7 +258,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let l = List.map (on_pi2 nf_evar) l in pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in - let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in + let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) Universes.empty_binders imps false nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a44de66e9..590332d08 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -484,7 +484,7 @@ let declare_definition prg = let () = progmap_remove prg in let cst = DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce [] prg.prg_implicits + prg.prg_kind ce Universes.empty_binders prg.prg_implicits (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) in Universes.register_universe_binders cst pl; @@ -554,7 +554,7 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; diff --git a/vernac/record.ml b/vernac/record.ml index f09b57048..6ffbd1584 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -426,7 +426,7 @@ let declare_structure finite univs id idbuild paramimpls params arity template else mie in - let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in + let kn = Command.declare_mutual_inductive_with_eliminations mie Universes.empty_binders [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let fields = -- cgit v1.2.3