From 485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:23:15 +0200 Subject: Use type Universes.universe_binders. --- engine/evd.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 17fa15045..853a34bc4 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -552,7 +552,7 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> - (Id.t * Univ.Level.t) list * Univ.UContext.t + Universes.universe_binders * Univ.UContext.t val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t -- cgit v1.2.3 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(-) (limited to 'engine/evd.mli') 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 From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 21:01:57 +0200 Subject: Separate checking univ_decls and obtaining universe binder names. --- API/API.mli | 3 +- engine/evd.ml | 2 ++ engine/evd.mli | 7 ++-- engine/uState.ml | 8 +++-- engine/uState.mli | 6 ++-- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/recdef.ml | 2 +- plugins/ltac/rewrite.ml | 2 +- plugins/setoid_ring/newring.ml | 2 +- printing/printer.ml | 7 ++++ printing/printer.mli | 1 + proofs/proof_global.ml | 10 +++--- tactics/leminv.ml | 4 +-- vernac/class.ml | 2 +- vernac/classes.ml | 8 ++--- vernac/command.ml | 48 +++++++++++++++------------ vernac/indschemes.ml | 2 +- vernac/lemmas.ml | 12 +++---- vernac/obligations.ml | 15 ++++----- vernac/record.ml | 5 +-- vernac/vernacentries.ml | 6 ++-- 21 files changed, 87 insertions(+), 67 deletions(-) (limited to 'engine/evd.mli') diff --git a/API/API.mli b/API/API.mli index 63c675221..889050d90 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2882,7 +2882,8 @@ sig val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t + val universe_binders : evar_map -> Universes.universe_binders val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map diff --git a/engine/evd.ml b/engine/evd.ml index ca1196b94..67ae73ceb 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -936,6 +936,8 @@ let universe_of_name evd s = UState.universe_of_name evd.universes s let add_universe_name evd s l = { evd with universes = UState.add_universe_name evd.universes s l } +let universe_binders evd = UState.universe_binders evd.universes + let universes evd = UState.ugraph evd.universes let update_sigma_env evd env = diff --git a/engine/evd.mli b/engine/evd.mli index 36c399e98..b6157202d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -509,7 +509,8 @@ val restrict_universe_context : evar_map -> Univ.LSet.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 -> +val universe_binders : evar_map -> Universes.universe_binders +val add_constraints_context : UState.t -> Univ.constraints -> UState.t @@ -552,12 +553,12 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t val check_univ_decl : evar_map -> UState.universe_decl -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 498d73fd3..282acb3d6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -114,6 +114,8 @@ let of_binders b = in { ctx with uctx_names = b, rmap } +let universe_binders ctx = fst ctx.uctx_names + let instantiate_variable l b v = try v := Univ.LMap.update l (Some b) !v with Not_found -> assert false @@ -291,7 +293,7 @@ let universe_context ~names ~extensible uctx = let inst = Univ.Instance.of_array inst in let ctx = Univ.UContext.make (inst, Univ.ContextSet.constraints uctx.uctx_local) in - fst uctx.uctx_names, ctx + ctx let check_implication uctx cstrs ctx = let gr = initial_graph uctx in @@ -303,14 +305,14 @@ let check_implication uctx cstrs ctx = let check_univ_decl uctx decl = let open Misctypes in - let pl, ctx = universe_context + let ctx = universe_context ~names:decl.univdecl_instance ~extensible:decl.univdecl_extensible_instance uctx in if not decl.univdecl_extensible_constraints then check_implication uctx decl.univdecl_constraints ctx; - pl, ctx + ctx let restrict ctx vars = let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in diff --git a/engine/uState.mli b/engine/uState.mli index 7f2357a68..38af08f91 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -32,6 +32,8 @@ val of_context_set : Univ.ContextSet.t -> t val of_binders : Universes.universe_binders -> t +val universe_binders : t -> Universes.universe_binders + (** {5 Projections} *) val context_set : t -> Univ.ContextSet.t @@ -135,12 +137,12 @@ val normalize : t -> t Also return the association list of universe names and universes (including those not in [names]). *) val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl -val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.UContext.t +val check_univ_decl : t -> universe_decl -> Univ.UContext.t (** {5 TODO: Document me} *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 996e2b6af..d5bff57af 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -348,7 +348,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in + let univs = Evd.universe_context ~names:[] ~extensible:true evd' in let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3089ec470..63896bb56 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1556,7 +1556,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in + let ctx = Evd.universe_context ~names:[] ~extensible:true evm in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in (* Refresh the global universes, now including those of _F *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 14b0742a7..2eb660219 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1884,7 +1884,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in + let ctx = Evd.universe_context ~names:[] ~extensible:true sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 1c3bdb958..a37b35b3d 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in let nf c = nf (constr_of c) in - Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd) + Array.map nf !tactic_res, Evd.universe_context ~names:[] ~extensible:true evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; diff --git a/printing/printer.ml b/printing/printer.ml index d7bb0460d..4d5cfcba3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -256,6 +256,13 @@ let safe_pr_constr t = let (sigma, env) = Pfedit.get_current_context () in safe_pr_constr_env env sigma t +let pr_universe_ctx_set sigma c = + if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c + else + mt() + let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 diff --git a/printing/printer.mli b/printing/printer.mli index e014baa2c..a3d0eaac2 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -121,6 +121,7 @@ val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fdc9a236b..9faff3211 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -331,8 +331,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in - let binders = if poly then Some binders else None in + let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in + let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) else (* Since the proof is computed now, we can simply have 1 set of @@ -370,7 +370,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) @@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) let bodyunivs = constrain_variables univctx (Future.force univs) in - let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in (pt,Univ.ContextSet.of_context univs),eff) in let entry_fn p (_, t) = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 62f3866de..4d1b271d6 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -235,9 +235,9 @@ let inversion_scheme env sigma t sort dep_option inv_op = p, Evd.universe_context ~names:[] ~extensible:true sigma let add_inversion_lemma name env sigma t sort dep inv_op = - let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in + let invProof, univs = inversion_scheme env sigma t sort dep inv_op in let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) - ~univs:(snd ctx) invProof in + ~univs invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/vernac/class.ml b/vernac/class.ml index 44f20a088..e59482b71 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,7 +212,7 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in + let univs = Evd.universe_context ~names:[] ~extensible:true sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~poly ~univs diff --git a/vernac/classes.ml b/vernac/classes.ml index ed37bab6d..6f5f96ee2 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -119,14 +119,14 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter (Univops.universes_of_constr term) in Evd.restrict_universe_context evm levels in - let pl, uctx = Evd.check_univ_decl evm decl in + let uctx = Evd.check_univ_decl evm decl in let entry = Declare.definition_entry ~types:termtype ~poly ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; - Universes.register_universe_binders (ConstRef kn) pl; + Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm); instance_hook k info global imps ?hook (ConstRef kn); id @@ -203,12 +203,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) nf t in Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); - let pl, ctx = Evd.check_univ_decl !evars decl in + let ctx = Evd.check_univ_decl !evars decl in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in - Universes.register_universe_binders (ConstRef cst) pl; + Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); instance_hook k pri global imps ?hook (ConstRef cst); id end else ( diff --git a/vernac/command.ml b/vernac/command.ml index 5d83de070..5a063f173 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -107,8 +107,9 @@ let interp_definition pl bl p red_option c ctypopt = let body = nf (it_mkLambda_or_LetIn c ctx) in let vars = Univops.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl evd decl in - imps1@(Impargs.lift_implicits nb_args imps2), pl, + let uctx = Evd.check_univ_decl evd decl in + let binders = Evd.universe_binders evd in + imps1@(Impargs.lift_implicits nb_args imps2), binders, definition_entry ~univs:uctx ~poly:p body | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in @@ -133,8 +134,9 @@ let interp_definition pl bl p red_option c ctypopt = let vars = Univ.LSet.union (Univops.universes_of_constr body) (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl ctx decl in - imps1@(Impargs.lift_implicits nb_args impsty), pl, + let uctx = Evd.check_univ_decl ctx decl in + let binders = Evd.universe_binders evd in + imps1@(Impargs.lift_implicits nb_args impsty), binders, definition_entry ~types:typ ~poly:p ~univs:uctx body in @@ -277,9 +279,10 @@ let do_assumptions_bound_univs coe kind nl id pl c = let ty = nf ty in let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl evd decl in + let binders = Evd.universe_binders evd in let uctx = Univ.ContextSet.of_context uctx in - let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in + let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in st let do_assumptions kind nl l = match l with @@ -576,7 +579,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in - let pl, uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl evd decl in List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -617,7 +620,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = in (if poly && cum then Inductiveops.infer_inductive_subtyping env_ar evd mind_ent - else mind_ent), pl, impls + else mind_ent), Evd.universe_binders evd, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -1025,17 +1028,18 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = - let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in - let ty = it_mkProd_or_LetIn top_arity binders_rel in - let ty = EConstr.Unsafe.to_constr ty in - let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in - (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in - (** FIXME: include locality *) - let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in - let gr = ConstRef c in - if Impargs.is_implicit_args () || not (List.is_empty impls) then - Impargs.declare_manual_implicits false gr [impls] + let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in + let ty = it_mkProd_or_LetIn top_arity binders_rel in + let ty = EConstr.Unsafe.to_constr ty in + let univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in + (*FIXME poly? *) + let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in + (** FIXME: include locality *) + let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in + let gr = ConstRef c in + let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) in + if Impargs.is_implicit_args () || not (List.is_empty impls) then + Impargs.declare_manual_implicits false gr [impls] in let typ = it_mkProd_or_LetIn top_arity binders in hook, name, typ @@ -1168,7 +1172,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let pl, ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl evd pl in + let pl = Evd.universe_binders evd in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); @@ -1200,7 +1205,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let pl, ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl evd pl in + let pl = Evd.universe_binders evd in ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c0ddc7e2c..58f39e303 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,7 +109,7 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in + let univs = Evd.universe_context ~names:[] ~extensible:true ctx in let univs = if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index a025bfff8..cd30c7a68 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -49,7 +49,7 @@ let retrieve_first_recthm uctx = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in + let uctx = UState.universe_context ~names:[] ~extensible:true uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) @@ -223,7 +223,7 @@ let compute_proof_name locality = function let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in next_global_ident_away default_thm_id avoid -let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -420,9 +420,9 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in + let ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in let body = Option.map norm body in - List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in + List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; @@ -513,9 +513,9 @@ let save_proof ?proof = function | _ -> None in let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in - let binders, ctx = Evd.check_univ_decl evd decl in + let ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in - let binders = if poly then Some binders else None in + let binders = if poly then Some (UState.universe_binders universes) else None in Admitted(id,k,(sec_vars, poly, (typ, ctx), None), (universes, binders)) in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 590332d08..216801811 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,20 +475,17 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in + let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in let () = progmap_remove prg in - let cst = - DeclareDef.declare_definition prg.prg_name - 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; - cst + let ubinders = UState.universe_binders prg.prg_ctx in + DeclareDef.declare_definition prg.prg_name + prg.prg_kind ce ubinders prg.prg_implicits + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) let rec lam_index n t acc = match Constr.kind t with @@ -893,7 +890,7 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in + let uctx = UState.universe_context ~names:[] ~extensible:true ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in diff --git a/vernac/record.ml b/vernac/record.ml index 6ffbd1584..9fef8f682 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -168,9 +168,10 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let typ = EConstr.to_constr evars typ in let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in let univs = Evd.check_univ_decl evars decl in + let ubinders = Evd.universe_binders evars in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); - univs, typ, template, imps, newps, impls, newfs + ubinders, univs, typ, template, imps, newps, impls, newfs let degenerate_decl decl = let id = match RelDecl.get_name decl with @@ -605,7 +606,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then user_err Pp.(str "Priorities only allowed for type class substructures"); (* Now, younger decl in params and fields is on top *) - let (pl, ctx), arity, template, implpars, params, implfs, fields = + let pl, ctx, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 62c7edb19..e2f28a371 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1555,8 +1555,8 @@ let vernac_check_may_eval ?loc redexp glopt rc = let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in - let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in + let uctx = Evd.universe_context_set sigma' in + let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then @@ -1572,7 +1572,7 @@ let vernac_check_may_eval ?loc redexp glopt rc = let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in Feedback.msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx sigma uctx) + Printer.pr_universe_ctx_set sigma uctx) | Some r -> let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = -- cgit v1.2.3 From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 22:21:46 +0200 Subject: Stop exposing UState.universe_context and its Evd wrapper. We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former). --- API/API.mli | 4 ++-- engine/evd.ml | 3 +-- engine/evd.mli | 9 +++++++-- engine/uState.mli | 23 +++++++++-------------- interp/modintern.ml | 2 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/recdef.ml | 2 +- plugins/ltac/rewrite.ml | 2 +- plugins/setoid_ring/newring.ml | 2 +- proofs/proof_global.ml | 2 +- tactics/ind_tables.ml | 2 +- tactics/leminv.ml | 2 +- test-suite/success/polymorphism.v | 2 ++ vernac/class.ml | 2 +- vernac/command.ml | 4 +--- vernac/indschemes.ml | 2 +- vernac/lemmas.ml | 15 ++++++++------- vernac/obligations.ml | 13 +++++++------ 18 files changed, 47 insertions(+), 46 deletions(-) (limited to 'engine/evd.mli') diff --git a/API/API.mli b/API/API.mli index 889050d90..5c7860671 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2881,12 +2881,12 @@ sig val universe_context_set : evar_map -> Univ.ContextSet.t val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list - val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> - Univ.UContext.t val universe_binders : evar_map -> Universes.universe_binders val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map + val to_universe_context : evar_map -> Univ.UContext.t + val meta_list : evar_map -> (Constr.metavariable * clbinding) list val meta_defined : evar_map -> Constr.metavariable -> bool diff --git a/engine/evd.ml b/engine/evd.ml index 67ae73ceb..eb0f2e3e7 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -756,8 +756,7 @@ let evar_universe_context d = d.universes let universe_context_set d = UState.context_set d.universes -let universe_context ~names ~extensible evd = - UState.universe_context ~names ~extensible evd.universes +let to_universe_context evd = UState.context evd.universes let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl diff --git a/engine/evd.mli b/engine/evd.mli index b6157202d..49b6a7583 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -492,6 +492,8 @@ type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t val evar_universe_context_constraints : UState.t -> Univ.constraints val evar_context_universe_context : UState.t -> Univ.UContext.t +[@@ocaml.deprecated "alias of UState.context"] + val evar_universe_context_of : Univ.ContextSet.t -> UState.t val empty_evar_universe_context : UState.t val union_evar_universe_context : UState.t -> UState.t -> @@ -552,11 +554,14 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t -val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> - Univ.UContext.t val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t +(** [to_universe_context evm] extracts the local universes and + constraints of [evm] and orders the universes the same as + [Univ.ContextSet.to_context]. *) +val to_universe_context : evar_map -> Univ.UContext.t + val check_univ_decl : evar_map -> UState.universe_decl -> Univ.UContext.t diff --git a/engine/uState.mli b/engine/uState.mli index 38af08f91..5279c6388 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -125,23 +125,18 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t -(** [universe_context names extensible ctx] - - Return a universe context containing the local universes of [ctx] - and their constraints. The universes corresponding to [names] come - first in the order defined by that list. - - If [extensible] is false, check that the universes of [names] are - the only local universes. - - Also return the association list of universe names and universes - (including those not in [names]). *) -val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> - Univ.UContext.t - type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl +(** [check_univ_decl ctx decl] + + If non extensible in [decl], check that the local universes (resp. + universe constraints) in [ctx] are implied by [decl]. + + Return a universe context containing the local universes of [ctx] + and their constraints. The universes corresponding to + [decl.univdecl_instance] come first in the order defined by that + list. *) val check_univ_decl : t -> universe_decl -> Univ.UContext.t (** {5 TODO: Document me} *) diff --git a/interp/modintern.ml b/interp/modintern.ml index 08657936e..3eb91d8cd 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -62,7 +62,7 @@ let transl_with_decl env = function WithMod (fqid,lookup_module qid) | CWith_Definition ((_,fqid),c) -> let c, ectx = interp_constr env (Evd.from_env env) c in - let ctx = Evd.evar_context_universe_context ectx in + let ctx = UState.context ectx in WithDef (fqid,(c,ctx)) let loc_of_module l = l.CAst.loc diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d5bff57af..076fba861 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -348,7 +348,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = Evd.universe_context ~names:[] ~extensible:true evd' in + let univs = Evd.to_universe_context evd' in let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 63896bb56..320f7c7f3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1556,7 +1556,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let ctx = Evd.universe_context ~names:[] ~extensible:true evm in + let ctx = Evd.to_universe_context evm in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in (* Refresh the global universes, now including those of _F *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2eb660219..f6523d28c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1884,7 +1884,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let ctx = Evd.universe_context ~names:[] ~extensible:true sigma in + let ctx = Evd.to_universe_context sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index a37b35b3d..6d0b6fd09 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in let nf c = nf (constr_of c) in - Array.map nf !tactic_res, Evd.universe_context ~names:[] ~extensible:true evd + Array.map nf !tactic_res, Evd.to_universe_context evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9faff3211..ea0408169 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -353,7 +353,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let used_univs_typ = Univops.universes_of_constr typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then - let initunivs = Evd.evar_context_universe_context initial_euctx in + let initunivs = UState.context initial_euctx in let ctx = constrain_variables initunivs universes in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e7fa555c2..92c326b1e 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -123,7 +123,7 @@ let define internal id c p univs = let ctx = Evd.normalize_evar_universe_context univs in let c = Vars.subst_univs_fn_constr (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in - let univs = Evd.evar_context_universe_context ctx in + let univs = UState.context ctx in let univs = if p then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 4d1b271d6..1ee873e0f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -232,7 +232,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let invProof = it_mkNamedLambda_or_LetIn c !ownSign in let invProof = EConstr.Unsafe.to_constr invProof in let p = Evarutil.nf_evars_universes sigma invProof in - p, Evd.universe_context ~names:[] ~extensible:true sigma + p, Evd.to_universe_context sigma let add_inversion_lemma name env sigma t sort dep inv_op = let invProof, univs = inversion_scheme env sigma t sort dep inv_op in diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 7eaafc354..00cab744e 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -190,6 +190,8 @@ Module binders. Fail Defined. Abort. + Fail Lemma bar@{u v | } : let x := (fun x => x) : Type@{u} -> Type@{v} in nat. + Lemma bar@{i j| i < j} : Type@{j}. Proof. exact Type@{i}. diff --git a/vernac/class.ml b/vernac/class.ml index e59482b71..68fd22cb6 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,7 +212,7 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = Evd.universe_context ~names:[] ~extensible:true sigma in + let univs = Evd.to_universe_context sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~poly ~univs diff --git a/vernac/command.ml b/vernac/command.ml index 5a063f173..80599c534 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1022,8 +1022,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders_rel = nf_evar_context !evdref binders_rel in let binders = nf_evar_context !evdref binders in let top_arity = Evarutil.nf_evar !evdref top_arity in - let pl, plext = Option.cata - (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in @@ -1031,7 +1029,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in + let univs = Evd.check_univ_decl !evdref decl in (*FIXME poly? *) let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 58f39e303..c728c2671 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,7 +109,7 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let univs = Evd.universe_context ~names:[] ~extensible:true ctx in + let univs = Evd.to_universe_context ctx in let univs = if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index cd30c7a68..71d80c4db 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -49,7 +49,8 @@ let retrieve_first_recthm uctx = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let uctx = UState.universe_context ~names:[] ~extensible:true uctx in + (* we get the right order somehow but surely it could be enforced in a better way *) + let uctx = UState.context uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) @@ -420,8 +421,8 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in - let body = Option.map norm body in + let ctx = UState.check_univ_decl ctx decl in + let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> @@ -453,9 +454,9 @@ let start_proof_com ?inference_hook kind thms hook = let evd, nf = Evarutil.nf_evars_and_universes !evdref in let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in let () = - if not decl.Misctypes.univdecl_extensible_instance then - ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false) - else () + let open Misctypes in + if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then + ignore (Evd.check_univ_decl evd decl) in let evd = if pi2 kind then evd @@ -490,7 +491,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = Evd.evar_context_universe_context (fst universes) in + let ctx = UState.context (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) | None -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 216801811..43af8968f 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -479,7 +479,7 @@ let declare_definition prg = let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) + ~univs:(UState.context prg.prg_ctx) (nf body) in let () = progmap_remove prg in let ubinders = UState.universe_binders prg.prg_ctx in @@ -549,7 +549,7 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let ctx = Evd.evar_context_universe_context first.prg_ctx in + let ctx = UState.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) Universes.empty_binders ctx) fixnames fixdecls fixtypes fiximps in @@ -855,7 +855,7 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = Evd.evar_context_universe_context ctx in + let uctx = UState.context ctx in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in @@ -890,7 +890,8 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let uctx = UState.universe_context ~names:[] ~extensible:true ctx' in + (* We get the right order somehow, but surely it could be enforced in a clearer way. *) + let uctx = UState.context ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in @@ -969,7 +970,7 @@ and solve_obligation_by_tac prg obls i tac = solve_by_tac obl.obl_name (evar_of_obligation obl) tac (pi2 prg.prg_kind) (Evd.evar_universe_context evd) in - let uctx = Evd.evar_context_universe_context ctx in + let uctx = UState.context ctx in let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; @@ -1120,7 +1121,7 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = Evd.evar_context_universe_context prg.prg_ctx in + let ctx = UState.context prg.prg_ctx in let kn = Declare.declare_constant x.obl_name ~local:true (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural) in -- cgit v1.2.3 From 34d85e1e899f8a045659ccc53bfd6a1f5104130b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 17:22:24 +0200 Subject: Use Entries.constant_universes_entry more. This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. --- API/API.mli | 11 ++- engine/evd.ml | 5 +- engine/evd.mli | 8 +- engine/uState.ml | 107 ++++++++++++++++++-------- engine/uState.mli | 17 +++- interp/declare.ml | 13 +--- interp/declare.mli | 6 +- plugins/funind/functional_principles_types.ml | 7 +- plugins/funind/recdef.ml | 8 +- plugins/ltac/extratactics.ml4 | 6 +- plugins/ltac/rewrite.ml | 9 +-- plugins/setoid_ring/newring.ml | 10 +-- proofs/proof_global.ml | 31 +++----- tactics/leminv.ml | 11 ++- vernac/class.ml | 4 +- vernac/classes.ml | 34 ++++---- vernac/command.ml | 44 ++++++----- vernac/declareDef.ml | 4 +- vernac/declareDef.mli | 7 +- vernac/lemmas.ml | 36 ++++----- vernac/obligations.ml | 17 ++-- vernac/record.ml | 54 +++++++------ 22 files changed, 251 insertions(+), 198 deletions(-) (limited to 'engine/evd.mli') diff --git a/API/API.mli b/API/API.mli index ad5d5490b..4405bf8da 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2764,6 +2764,9 @@ sig val context_set : t -> Univ.ContextSet.t val of_context_set : Univ.ContextSet.t -> t + val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry + val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes + type rigid = | UnivRigid | UnivFlexible of bool @@ -2887,6 +2890,8 @@ sig val from_ctx : UState.t -> evar_map val to_universe_context : evar_map -> Univ.UContext.t + val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry + val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes val meta_list : evar_map -> (Constr.metavariable * clbinding) list @@ -4669,11 +4674,11 @@ sig val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind -> - ?local:bool -> ?poly:Decl_kinds.polymorphic -> Names.Id.t -> ?types:Constr.t -> - Constr.t Univ.in_universe_context_set -> Names.Constant.t + ?local:bool -> Names.Id.t -> ?types:Constr.t -> + Constr.t Entries.in_constant_universes_entry -> Names.Constant.t val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:Constr.types -> - ?poly:Decl_kinds.polymorphic -> ?univs:Univ.UContext.t -> + ?univs:Entries.constant_universes_entry -> ?eff:Safe_typing.private_constants -> Constr.t -> Safe_typing.private_constants Entries.definition_entry val definition_message : Names.Id.t -> unit val declare_variable : Names.Id.t -> variable_declaration -> Libnames.object_name diff --git a/engine/evd.ml b/engine/evd.ml index eb0f2e3e7..9ea2cc00f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -758,7 +758,10 @@ let universe_context_set d = UState.context_set d.universes let to_universe_context evd = UState.context evd.universes -let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl +let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes +let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes + +let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl let restrict_universe_context evd vars = { evd with universes = UState.restrict evd.universes vars } diff --git a/engine/evd.mli b/engine/evd.mli index 49b6a7583..f06fb8d3b 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -562,8 +562,12 @@ val universes : evar_map -> UGraph.t [Univ.ContextSet.to_context]. *) val to_universe_context : evar_map -> Univ.UContext.t -val check_univ_decl : evar_map -> UState.universe_decl -> - Univ.UContext.t +val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry + +(** NB: [ind_univ_entry] cannot create cumulative entries. *) +val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes + +val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index ff91493ee..dadc004c5 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -87,6 +87,17 @@ let constraints ctx = snd ctx.uctx_local let context ctx = Univ.ContextSet.to_context ctx.uctx_local +let const_univ_entry ~poly uctx = + let open Entries in + if poly then Polymorphic_const_entry (context uctx) + else Monomorphic_const_entry (context_set uctx) + +(* does not support cumulativity since you need more info *) +let ind_univ_entry ~poly uctx = + let open Entries in + if poly then Polymorphic_ind_entry (context uctx) + else Monomorphic_ind_entry (context_set uctx) + let of_context_set ctx = { empty with uctx_local = ctx } let subst ctx = ctx.uctx_univ_variables @@ -260,58 +271,92 @@ let pr_uctx_level uctx = type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl +let error_unbound_universes left uctx = + let open Univ in + let n = LSet.cardinal left in + let loc = + try + let info = + LMap.find (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 () ++ + LSet.pr (pr_uctx_level uctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ + str" unbound.")) + let universe_context ~names ~extensible uctx = - let levels = Univ.ContextSet.levels uctx.uctx_local in + let open Univ in + let levels = ContextSet.levels uctx.uctx_local in let newinst, left = List.fold_right (fun (loc,id) (newinst, acc) -> let l = 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.") - in (l :: newinst, Univ.LSet.remove l acc)) + with Not_found -> assert false + in (l :: newinst, LSet.remove l acc)) names ([], levels) in - if not extensible && not (Univ.LSet.is_empty left) then - let n = Univ.LSet.cardinal left in - let loc = - try - let info = - 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 uctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ - str" unbound.")) + if not extensible && not (LSet.is_empty left) + then error_unbound_universes left uctx else - let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in + let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in let inst = Array.append (Array.of_list newinst) left in - let inst = Univ.Instance.of_array inst in - let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints uctx.uctx_local) in + let inst = Instance.of_array inst in + let ctx = UContext.make (inst, ContextSet.constraints uctx.uctx_local) in ctx -let check_implication uctx cstrs ctx = +let check_universe_context_set ~names ~extensible uctx = + if extensible then () + else + let open Univ in + let left = List.fold_left (fun left (loc,id) -> + let l = + try UNameMap.find id (fst uctx.uctx_names) + with Not_found -> assert false + in LSet.remove l left) + (ContextSet.levels uctx.uctx_local) names + in + if not (LSet.is_empty left) + then error_unbound_universes left uctx + +let check_implication uctx cstrs cstrs' = let gr = initial_graph uctx in let grext = UGraph.merge_constraints cstrs gr in - let cstrs' = Univ.UContext.constraints ctx in if UGraph.check_constraints cstrs' grext then () else CErrors.user_err ~hdr:"check_univ_decl" (str "Universe constraints are not implied by the ones declared.") -let check_univ_decl uctx decl = +let check_mono_univ_decl uctx decl = + let open Misctypes in + let () = + let names = decl.univdecl_instance in + let extensible = decl.univdecl_extensible_instance in + check_universe_context_set ~names ~extensible uctx + in + if not decl.univdecl_extensible_constraints then + check_implication uctx + decl.univdecl_constraints + (Univ.ContextSet.constraints uctx.uctx_local); + uctx.uctx_local + +let check_univ_decl ~poly uctx decl = let open Misctypes in - let ctx = universe_context - ~names:decl.univdecl_instance - ~extensible:decl.univdecl_extensible_instance - uctx + let ctx = + let names = decl.univdecl_instance in + let extensible = decl.univdecl_extensible_instance in + if poly + then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx) + else + let () = check_universe_context_set ~names ~extensible uctx in + Entries.Monomorphic_const_entry uctx.uctx_local in if not decl.univdecl_extensible_constraints then - check_implication uctx decl.univdecl_constraints ctx; + check_implication uctx + decl.univdecl_constraints + (Univ.ContextSet.constraints uctx.uctx_local); ctx let restrict ctx vars = diff --git a/engine/uState.mli b/engine/uState.mli index 5279c6388..4265f2b20 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -59,6 +59,13 @@ val constraints : t -> Univ.constraints val context : t -> Univ.UContext.t (** Shorthand for {!context_set} with {!Context_set.to_context}. *) +val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry +(** Pick from {!context} or {!context_set} based on [poly]. *) + +val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes +(** Pick from {!context} or {!context_set} based on [poly]. + Cannot create cumulative entries. *) + (** {5 Constraints handling} *) val add_constraints : t -> Univ.constraints -> t @@ -133,11 +140,15 @@ type universe_decl = If non extensible in [decl], check that the local universes (resp. universe constraints) in [ctx] are implied by [decl]. - Return a universe context containing the local universes of [ctx] - and their constraints. The universes corresponding to + Return a [Entries.constant_universes_entry] containing the local + universes of [ctx] and their constraints. + + When polymorphic, the universes corresponding to [decl.univdecl_instance] come first in the order defined by that list. *) -val check_univ_decl : t -> universe_decl -> Univ.UContext.t +val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry + +val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t (** {5 TODO: Document me} *) diff --git a/interp/declare.ml b/interp/declare.ml index 15999f1d1..1b4645aff 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -203,14 +203,9 @@ let declare_constant_common id cst = update_tables c; c +let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = - let univs = - if poly then Polymorphic_const_entry univs - else - (* FIXME be smarter about this *) - Monomorphic_const_entry (Univ.ContextSet.of_context univs) - in + ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; @@ -263,9 +258,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - ?(poly=false) id ?types (body,ctx) = + id ?types (body,univs) = let cb = - definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body + definition_entry ?types ~univs ~opaque body in declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) diff --git a/interp/declare.mli b/interp/declare.mli index 9b3194dec..d50d37368 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -42,7 +42,7 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> - ?poly:polymorphic -> ?univs:Univ.UContext.t -> + ?univs:Entries.constant_universes_entry -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry (** [declare_constant id cd] declares a global declaration @@ -56,8 +56,8 @@ val declare_constant : val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> - constr Univ.in_universe_context_set -> Constant.t + ?local:bool -> Id.t -> ?types:constr -> + constr Entries.in_constant_universes_entry -> Constant.t (** Since transparent constants' side effects are globally declared, we * need that *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 076fba861..7a9bbd92c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -348,8 +348,11 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = Evd.to_universe_context evd' in - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in + let univs = + let poly = Flags.is_universe_polymorphism () in + Evd.const_univ_entry ~poly evd' + in + let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant name diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 320f7c7f3..b0a76137b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -66,8 +66,8 @@ let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) -let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = - let ce = definition_entry ~univs:ctx value (*FIXME *) in +let declare_fun f_id kind ?univs value = + let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) @@ -1556,8 +1556,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let ctx = Evd.to_universe_context evm in - declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in + declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) let evm = Evd.from_env (Global.env ()) in diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index d6cfa3cf9..750517e91 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -313,10 +313,10 @@ let project_hint pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in - let ctx = Evd.universe_context_set sigma in - let c = EConstr.to_constr sigma c in let poly = Flags.use_polymorphic_flag () in - let c = Declare.declare_definition ~poly ~internal:Declare.InternalTacticRequest id (c,ctx) in + let ctx = Evd.const_univ_entry ~poly sigma in + let c = EConstr.to_constr sigma c in + let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a2f5a4577..c0060c5a7 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1884,11 +1884,11 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let ctx = Evd.to_universe_context sigma in + let univs = Evd.const_univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = - Declare.definition_entry ~types:typ ~poly ~univs:ctx term + Declare.definition_entry ~types:typ ~univs term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) @@ -1972,10 +1972,7 @@ let add_morphism_infer glob m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then - let uctx = if poly - then Entries.Polymorphic_const_entry (UState.context uctx) - else Entries.Monomorphic_const_entry (UState.context_set uctx) - in + let uctx = UState.const_univ_entry ~poly uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry (None,(instance,uctx),None), diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 6d0b6fd09..f22f00839 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -150,13 +150,13 @@ let ic_unsafe c = (*FIXME remove *) let sigma = Evd.from_env env in EConstr.of_constr (fst (Constrintern.interp_constr env sigma c)) -let decl_constant na ctx c = +let decl_constant na univs c = let open Constr in let vars = Univops.universes_of_constr c in - let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in + let univs = Univops.restrict_universe_context univs vars in + let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true - ~univs:(Univ.ContextSet.to_context ctx) c), + (DefinitionEntry (definition_entry ~opaque:true ~univs c), IsProof Lemma)) (* Calling a global tactic *) @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in let nf c = nf (constr_of c) in - Array.map nf !tactic_res, Evd.to_universe_context evd + Array.map nf !tactic_res, Evd.universe_context_set evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 905173efc..bfd64e21b 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -316,10 +316,6 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf -let constrain_variables init uctx = - let levels = Univ.Instance.levels (Univ.UContext.instance init) in - UState.constrain_variables levels uctx - type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t let close_proof ~keep_body_ucst_separate ?feedback_id ~now @@ -329,9 +325,12 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in + let constrain_variables ctx = + UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx + in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let univctx = UState.check_univ_decl universes universe_decl in + let univctx = UState.check_univ_decl ~poly universes universe_decl in let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to @@ -353,15 +352,15 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let used_univs_typ = Univops.universes_of_constr typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then - let initunivs = UState.context initial_euctx in - let ctx = constrain_variables initunivs universes in + let initunivs = UState.const_univ_entry ~poly initial_euctx in + let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in - let univs = UState.check_univ_decl ctx_body universe_decl in - (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) + let univs = UState.check_mono_univ_decl ctx_body universe_decl in + (initunivs, typ), ((body, univs), eff) else (* Since the proof is computed now, we can simply have 1 set of constraints in which we merge the ones for the body and the ones @@ -370,7 +369,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let univs = UState.check_univ_decl ctx universe_decl in + let univs = UState.check_univ_decl ~poly ctx universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) @@ -382,20 +381,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the initial universes, ensure that the final universes respect the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) - let bodyunivs = constrain_variables univctx (Future.force univs) in - let univs = UState.check_univ_decl bodyunivs universe_decl in - (pt,Univ.ContextSet.of_context univs),eff) + let bodyunivs = constrain_variables (Future.force univs) in + let univs = UState.check_mono_univ_decl bodyunivs universe_decl in + (pt,univs),eff) in let entry_fn p (_, t) = let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in - let univs = - if poly then Entries.Polymorphic_const_entry univs - else - (* FIXME be smarter about the unnecessary context linearisation in make_body *) - Entries.Monomorphic_const_entry (Univ.ContextSet.of_context univs) - in {Entries. const_entry_body = body; const_entry_secctx = section_vars; diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 1ee873e0f..1ae3577ed 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -232,12 +232,15 @@ let inversion_scheme env sigma t sort dep_option inv_op = let invProof = it_mkNamedLambda_or_LetIn c !ownSign in let invProof = EConstr.Unsafe.to_constr invProof in let p = Evarutil.nf_evars_universes sigma invProof in - p, Evd.to_universe_context sigma + p, sigma let add_inversion_lemma name env sigma t sort dep inv_op = - let invProof, univs = inversion_scheme env sigma t sort dep inv_op in - let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) - ~univs invProof in + let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in + let univs = + let poly = Flags.use_polymorphic_flag () in + Evd.const_univ_entry ~poly sigma + in + let entry = definition_entry ~univs invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/vernac/class.ml b/vernac/class.ml index 68fd22cb6..943da8fa8 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,10 +212,10 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = Evd.to_universe_context sigma in + let univs = Evd.const_univ_entry ~poly sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs + (definition_entry ~types:typ_f ~univs ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in diff --git a/vernac/classes.ml b/vernac/classes.ml index c99eba2cc..1833b7a1d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -119,9 +119,9 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter (Univops.universes_of_constr term) in Evd.restrict_universe_context evm levels in - let uctx = Evd.check_univ_decl evm decl in + let uctx = Evd.check_univ_decl ~poly evm decl in let entry = - Declare.definition_entry ~types:termtype ~poly ~univs:uctx term + Declare.definition_entry ~types:termtype ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in @@ -203,16 +203,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) nf t in Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); - let ctx = Evd.check_univ_decl !evars decl in - let ctx = if poly - then Polymorphic_const_entry ctx - else - (* FIXME be smarter about this *) - Monomorphic_const_entry (Univ.ContextSet.of_context ctx) - in + let univs = Evd.check_univ_decl ~poly !evars decl in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry - (None,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); instance_hook k pri global imps ?hook (ConstRef cst); id @@ -391,19 +385,16 @@ let context poly l = let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) - let univs = !uctx in + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context univs) - else Monomorphic_const_entry univs - in (ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> - (* FIXME be smarter about this *) - let univs = Univ.ContextSet.to_context univs in - let entry = Declare.definition_entry ~poly ~univs ~types:t b in + let entry = Declare.definition_entry ~univs ~types:t b in (DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in @@ -426,9 +417,12 @@ let context poly l = 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 univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let decl = (Discharge, poly, Definition) in - let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + let entry = Declare.definition_entry ~univs ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () diff --git a/vernac/command.ml b/vernac/command.ml index 06d0c8470..1a8b16a89 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -88,7 +88,7 @@ let warn_implicits_in_term = strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here.") -let interp_definition pl bl p red_option c ctypopt = +let interp_definition pl bl poly red_option c ctypopt = let env = Global.env() in let evd, decl = Univdecls.interp_univ_decl_opt env pl in let evdref = ref evd in @@ -105,15 +105,15 @@ let interp_definition pl bl p red_option c ctypopt = let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = Univops.universes_of_constr body in - let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl evd decl in + let vars = Univops.universes_of_constr body in + let evd = Evd.restrict_universe_context !evdref vars in + let uctx = Evd.check_univ_decl ~poly evd decl in let binders = Evd.universe_binders evd in imps1@(Impargs.lift_implicits nb_args imps2), binders, - definition_entry ~univs:uctx ~poly:p body + definition_entry ~univs:uctx body | Some ctyp -> - let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in - let subst = evd_comb0 Evd.nf_univ_variables evdref in + let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in + let subst = evd_comb0 Evd.nf_univ_variables evdref in let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in @@ -134,10 +134,10 @@ let interp_definition pl bl p red_option c ctypopt = let vars = Univ.LSet.union (Univops.universes_of_constr body) (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ctx decl in + let uctx = Evd.check_univ_decl ~poly ctx decl in let binders = Evd.universe_binders evd in imps1@(Impargs.lift_implicits nb_args impsty), binders, - definition_entry ~types:typ ~poly:p + definition_entry ~types:typ ~univs:uctx body in red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps @@ -282,9 +282,14 @@ let do_assumptions_bound_univs coe kind nl id pl c = let ty = nf ty in let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd decl in let binders = Evd.universe_binders evd in - let uctx = Univ.ContextSet.of_context uctx in + let uctx = match uctx with + | Polymorphic_const_entry uctx -> + (* ?? *) + Univ.ContextSet.of_context uctx + | Monomorphic_const_entry uctx -> uctx + in let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in st @@ -582,7 +587,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in - let uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl ~poly evd decl in List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -604,12 +609,13 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in let univs = - if poly then + match uctx with + | Polymorphic_const_entry uctx -> if cum then Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) else Polymorphic_ind_entry uctx - else - Monomorphic_ind_entry (Univ.ContextSet.of_context uctx) + | Monomorphic_const_entry uctx -> + Monomorphic_ind_entry uctx in (* Build the mutual inductive entry *) let mind_ent = @@ -1032,9 +1038,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let univs = Evd.check_univ_decl !evdref decl in + let univs = Evd.check_univ_decl ~poly !evdref decl in (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in + let ce = definition_entry ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in @@ -1173,7 +1179,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) @@ -1206,7 +1212,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index c18744052..980db4109 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -57,7 +57,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = declare_global_definition ident ce local k pl imps in Lemmas.call_hook fix_exn hook local r -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = + let ce = definition_entry ~opaque ~types:t ~univs ~eff def in declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 01a87818a..55f7c7861 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -15,5 +15,8 @@ val declare_definition : Id.t -> definition_kind -> Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference -val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t -> - Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference +val declare_fix : ?opaque:bool -> definition_kind -> + Universes.universe_binders -> Entries.constant_universes_entry -> + Id.t -> Safe_typing.private_constants Entries.proof_output -> + Constr.types -> Impargs.manual_implicits -> + Globnames.global_reference diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index f59b5fcae..a787ec6fa 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -224,7 +224,7 @@ let compute_proof_name locality = function let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in next_global_ident_away default_thm_id avoid -let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -232,7 +232,13 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Discharge -> let impl = false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in + let univs = match univs with + | Polymorphic_const_entry univs -> + (* What is going on here? *) + Univ.ContextSet.of_context univs + | Monomorphic_const_entry univs -> univs + in + let c = SectionLocalAssum ((t_i, univs),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> @@ -242,11 +248,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Global -> false | Discharge -> assert false in - let ctx = if p - then Polymorphic_const_entry ctx - else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) - in - let decl = (ParameterEntry (None,(t_i,ctx),None), k) in + let decl = (ParameterEntry (None,(t_i,univs),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> @@ -264,8 +266,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im let body_i = body_i body in match locality with | Discharge -> - let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p - ~univs:ctx body_i in + let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Discharge,VarRef id,imps) @@ -276,7 +277,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Discharge -> assert false in let const = - Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i + Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality,ConstRef kn,imps) @@ -425,7 +426,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = UState.check_univ_decl ctx decl in + let ctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in @@ -460,7 +461,7 @@ let start_proof_com ?inference_hook kind thms hook = let () = let open Misctypes in if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then - ignore (Evd.check_univ_decl evd decl) + ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl) in let evd = if pi2 kind then evd @@ -495,10 +496,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = if pi2 k (* polymorphic *) - then Polymorphic_const_entry (UState.context (fst universes)) - else Monomorphic_const_entry (UState.context_set (fst universes)) - in + let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> @@ -521,12 +519,8 @@ let save_proof ?proof = function | _ -> None in let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in - let ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in - let ctx = if poly - then Polymorphic_const_entry ctx - else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) - in + let ctx = Evd.check_univ_decl ~poly evd decl in let binders = if poly then Some (UState.universe_binders universes) else None in Admitted(id,k,(sec_vars, (typ, ctx), None), (universes, binders)) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a9110c76c..97cdd7977 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,12 +475,8 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in - let ce = - definition_entry ~fix_exn - ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(UState.context prg.prg_ctx) (nf body) - in + let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) prg.prg_ctx prg.prg_univdecl in + let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~univs (nf body) in let () = progmap_remove prg in let ubinders = UState.universe_binders prg.prg_ctx in DeclareDef.declare_definition prg.prg_name @@ -549,9 +545,9 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let ctx = UState.context first.prg_ctx in + let univs = UState.const_univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; @@ -856,10 +852,7 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = if pi2 prg.prg_kind - then Polymorphic_const_entry (UState.context ctx) - else Monomorphic_const_entry (UState.context_set ctx) - in + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in diff --git a/vernac/record.ml b/vernac/record.ml index faf277d86..1d255b08e 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -95,7 +95,7 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields finite def id pl t ps nots fs = +let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env0 = Global.env () in let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in let evars = ref evd in @@ -167,7 +167,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let newps = List.map (EConstr.to_rel_decl evars) newps in let typ = EConstr.to_constr evars typ in let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in - let univs = Evd.check_univ_decl evars decl in + let univs = Evd.check_univ_decl ~poly evars decl in let ubinders = Evd.universe_binders evars in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); @@ -449,7 +449,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params arity +let declare_class finite def cum ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -464,21 +464,21 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params let class_body = it_mkLambda_or_LetIn field params in let class_type = it_mkProd_or_LetIn arity params in let class_entry = - Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in + Declare.definition_entry ~types:class_type ~univs class_body in let cst = Declare.declare_constant (snd id) (DefinitionEntry class_entry, IsDefinition Definition) in - let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in + let cstu = (cst, match univs with + | Polymorphic_const_entry univs -> Univ.UContext.instance univs + | Monomorphic_const_entry _ -> Univ.Instance.empty) + in let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in let proj_type = it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in let proj_body = it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in - let proj_entry = - Declare.definition_entry ~types:proj_type ~poly - ~univs:(if poly then ctx else Univ.UContext.empty) proj_body - in + let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in let proj_cst = Declare.declare_constant proj_name (DefinitionEntry proj_entry, IsDefinition Definition) in @@ -495,13 +495,14 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params cref, [Name proj_name, sub, Some proj_cst] | _ -> let univs = - if poly then + match univs with + | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) else - Polymorphic_ind_entry ctx - else - Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) + Polymorphic_ind_entry univs + | Monomorphic_const_entry univs -> + Monomorphic_ind_entry univs in let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields @@ -524,13 +525,15 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params params, params in let univs, ctx_context, fields = - if poly then - let usubst, auctx = Univ.abstract_universes ctx in + match univs with + | Polymorphic_const_entry univs -> + let usubst, auctx = Univ.abstract_universes univs in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in auctx, ctx_context, fields - else Univ.AUContext.empty, ctx_context, fields + | Monomorphic_const_entry _ -> + Univ.AUContext.empty, ctx_context, fields in let k = { cl_univs = univs; @@ -606,14 +609,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then user_err Pp.(str "Priorities only allowed for type class substructures"); (* Now, younger decl in params and fields is on top *) - let pl, ctx, arity, template, implpars, params, implfs, fields = + let pl, univs, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in + typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in let sign = structure_signature (fields@params) in match kind with | Class def -> let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - let gr = declare_class finite def cum poly pl ctx (loc,idstruc) idbuild + let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> @@ -622,13 +625,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf (succ (List.length params)) impls) implfs in let univs = - if poly then + match univs with + | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) else - Polymorphic_ind_entry ctx - else - Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) + Polymorphic_ind_entry univs + | Monomorphic_const_entry univs -> + Monomorphic_ind_entry univs in let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs -- cgit v1.2.3 From d071eac98b7812ac5c03004b438022900885d874 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 21 Sep 2017 11:14:11 +0200 Subject: Forbid repeated names in universe binders. --- engine/evd.ml | 3 --- engine/evd.mli | 1 - engine/uState.ml | 7 +++---- engine/uState.mli | 3 --- engine/universes.ml | 2 +- test-suite/output/UnivBinders.out | 2 ++ test-suite/output/UnivBinders.v | 3 +++ 7 files changed, 9 insertions(+), 12 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.ml b/engine/evd.ml index 9ea2cc00f..0f17e0dc6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -935,9 +935,6 @@ let nf_constraints evd = let universe_of_name evd s = UState.universe_of_name evd.universes s -let add_universe_name evd s l = - { evd with universes = UState.add_universe_name evd.universes s l } - let universe_binders evd = UState.universe_binders evd.universes let universes evd = UState.ugraph evd.universes diff --git a/engine/evd.mli b/engine/evd.mli index f06fb8d3b..c59a67039 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -509,7 +509,6 @@ val make_evar_universe_context : env -> (Id.t located) list option -> UState.t 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 -> Id.t -> Univ.Level.t -val add_universe_name : evar_map -> Id.t -> Univ.Level.t -> evar_map val universe_binders : evar_map -> Universes.universe_binders val add_constraints_context : UState.t -> diff --git a/engine/uState.ml b/engine/uState.ml index dadc004c5..4e30640e4 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -109,6 +109,9 @@ let initial_graph ctx = ctx.uctx_initial_universes let algebraics ctx = ctx.uctx_univ_algebraic let add_uctx_names ?loc s l (names, names_rev) = + if UNameMap.mem s names + then user_err ?loc ~hdr:"add_uctx_names" + Pp.(str "Universe " ++ Names.Id.print s ++ str" already bound."); (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) let add_uctx_loc l loc (names, names_rev) = @@ -573,10 +576,6 @@ let normalize uctx = let universe_of_name uctx s = UNameMap.find s (fst uctx.uctx_names) -let add_universe_name uctx s l = - let names' = add_uctx_names s l uctx.uctx_names in - { uctx with uctx_names = names' } - let update_sigma_env uctx env = let univs = Environ.universes env in let eunivs = diff --git a/engine/uState.mli b/engine/uState.mli index 4265f2b20..16fba41e0 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -80,9 +80,6 @@ val add_universe_constraints : t -> Universes.universe_constraints -> t (** {5 Names} *) -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 -> Id.t -> Univ.Level.t (** Retrieve the universe associated to the name. *) diff --git a/engine/universes.ml b/engine/universes.ml index f2942be6d..5ac1bc685 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -55,7 +55,7 @@ let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj let register_universe_binders ref ubinders = (* Add the polymorphic (section) universes *) let open Names in - let ubinders = Idmap.fold (fun id (poly,lvl) ubinders -> + let ubinders = Id.Map.fold (fun id (poly,lvl) ubinders -> if poly then Id.Map.add id lvl ubinders else ubinders) (fst (Global.global_universe_names ())) ubinders diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 04bd169bd..a2857294b 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -53,6 +53,8 @@ Monomorphic mono = Type@{u} (* {u} |= *) mono is not universe polymorphic +The command has indeed failed with message: +Universe u already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1, M+1, N+1)} diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index f0a990986..013f215b5 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -34,6 +34,9 @@ Print foo. Monomorphic Definition mono@{u} := Type@{u}. Print mono. +(* fun x x => foo is nonsense with local binders *) +Fail Definition fo@{u u} := Type@{u}. + (* Using local binders for printing. *) Print foo@{E M N}. (* Underscores discard the name if there's one. *) -- cgit v1.2.3