From 63896b2443e71e47c016fc9d0709cc22cf24f288 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 12:37:55 +0200 Subject: [lib] Remove obsolete state-management function add_frozen_state AFAICS this function predates modern state-handling; nowadays summaries are stored by the STM and nobody were using this information. --- library/declaremods.ml | 7 +------ library/lib.ml | 13 ++----------- library/lib.mli | 5 ----- library/library.ml | 2 +- 4 files changed, 4 insertions(+), 23 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index c98d4a7f31..187b749b87 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -589,7 +589,6 @@ let start_module interp_modast export id args res fs = openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - Lib.add_frozen_state (); if_xml (Hook.get f_xml_start_module) mp; mp @@ -629,7 +628,6 @@ let end_module () = assert (eq_full_path (fst newoname) (fst oldoname)); assert (ModPath.equal (mp_of_kn (snd newoname)) mp); - Lib.add_frozen_state () (* to prevent recaching *); if_xml (Hook.get f_xml_end_module) mp; mp @@ -701,7 +699,6 @@ let start_modtype interp_modast id args mtys fs = openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - Lib.add_frozen_state (); if_xml (Hook.get f_xml_start_module_type) mp; mp @@ -719,7 +716,6 @@ let end_modtype () = assert (eq_full_path (fst oname) (fst oldoname)); assert (ModPath.equal (mp_of_kn (snd oname)) mp); - Lib.add_frozen_state ()(* to prevent recaching *); if_xml (Hook.get f_xml_end_module_type) mp; mp @@ -894,8 +890,7 @@ let get_library_native_symbols dir = let start_library dir = let mp = Global.start_library dir in openmod_info := default_module_info; - Lib.start_compilation dir mp; - Lib.add_frozen_state () + Lib.start_compilation dir mp let end_library_hook = ref ignore let append_end_library_hook f = diff --git a/library/lib.ml b/library/lib.ml index 9d71a854f0..f22f53eadf 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -27,7 +27,6 @@ type node = | ClosedModule of library_segment | OpenedSection of object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_entry = object_name * node @@ -80,7 +79,6 @@ let classify_segment seg = | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" (str "there are still opened " ++ str (module_kind ty) ++ str "s") - | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -254,10 +252,6 @@ let add_anonymous_leaf ?(cache_first = true) obj = cache_object (oname,obj) end -let add_frozen_state () = - add_anonymous_entry - (FrozenState (Summary.freeze_summaries ~marshallable:`No)) - (* Modules. *) let is_opening_node = function @@ -544,7 +538,6 @@ let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | FrozenState _ -> None | ClosedSection _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -585,8 +578,7 @@ let freeze ~marshallable = | n, ClosedModule _ -> Some (n,ClosedModule []) | n, OpenedSection (op, _) -> Some(n,OpenedSection(op,Summary.empty_frozen)) - | n, ClosedSection _ -> Some (n,ClosedSection []) - | _, FrozenState _ -> None) + | n, ClosedSection _ -> Some (n,ClosedSection [])) !lib_state.lib_stk in { !lib_state with lib_stk } | _ -> @@ -596,8 +588,7 @@ let unfreeze st = lib_state := st let init () = unfreeze initial_lib_state; - Summary.init_summaries (); - add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *) + Summary.init_summaries () (* Misc *) diff --git a/library/lib.mli b/library/lib.mli index 9f9d8c7e5f..f47d6e1a58 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -23,7 +23,6 @@ type node = | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_segment = (Libnames.object_name * node) list @@ -61,8 +60,6 @@ val pull_to_head : Libnames.object_name -> unit for each of them *) val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name -val add_frozen_state : unit -> unit - (** {6 ... } *) (** The function [contents] gives access to the current entire segment *) @@ -123,8 +120,6 @@ val end_modtype : Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment -(** [Lib.add_frozen_state] must be called after each of the above functions *) - (** {6 Compilation units } *) val start_compilation : Names.DirPath.t -> Names.module_path -> unit diff --git a/library/library.ml b/library/library.ml index 5a5f99cc51..db05ad2b7b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -575,7 +575,7 @@ let require_library_from_dirpath modrefl export = else add_anonymous_leaf (in_require (needed,modrefl,export)); if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl; - add_frozen_state () + () (* the function called by Vernacentries.vernac_import *) -- cgit v1.2.3 From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 28 Mar 2017 19:24:02 +0200 Subject: Extend definition of inductives to include subtyping info --- library/declare.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 7d0edbc8b3..06eeeeab56 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -352,7 +352,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; - mind_entry_universes = Univ.UContext.empty; + mind_entry_universes = (Univ.UContext.empty, Univ.UContext.empty); mind_entry_private = None; }) -- cgit v1.2.3 From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- library/declare.ml | 2 +- library/global.ml | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 06eeeeab56..f3150174c9 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -352,7 +352,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; - mind_entry_universes = (Univ.UContext.empty, Univ.UContext.empty); + mind_entry_universes = Univ.UInfoInd.empty; mind_entry_private = None; }) diff --git a/library/global.ml b/library/global.ml index 1ba86699d3..a459983849 100644 --- a/library/global.ml +++ b/library/global.ml @@ -178,13 +178,13 @@ let type_of_global_unsafe r = let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let inst = if mib.Declarations.mind_polymorphic then - Univ.UContext.instance mib.Declarations.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) else Univ.Instance.empty in Inductive.type_of_inductive env (specif, inst) | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let inst = Univ.UContext.instance mib.Declarations.mind_universes in + let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in Inductive.type_of_constructor (cstr,inst) specif let type_of_global_in_context env r = @@ -200,13 +200,13 @@ let type_of_global_in_context env r = | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = - if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.UContext.empty in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = - if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.UContext.empty in let inst = Univ.UContext.instance univs in @@ -222,10 +222,10 @@ let universes_of_global env r = (Environ.opaque_tables env) cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in - Univ.instantiate_univ_context mib.mind_universes + Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) | ConstructRef cstr -> let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Univ.instantiate_univ_context mib.mind_universes + Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) let universes_of_global gr = universes_of_global (env ()) gr -- cgit v1.2.3 From c07215582ab75faeea864827b153eed80a28527a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 6 Apr 2017 19:03:24 +0200 Subject: Change the place of inference after sect discharge --- library/declare.ml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index f3150174c9..fcaadaa6e0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -356,6 +356,21 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_private = None; }) +(* reinfer subtyping constraints for inductive after section is dischared. *) +let infer_inductive_subtyping (pth, mind_ent) = + if mind_ent.mind_entry_polymorphic then + begin + let env = Global.env () in + let env' = + Environ.push_context (Univ.UInfoInd.univ_context mind_ent.mind_entry_universes) env + in + let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in + let evd = Evd.from_env env'' in + (pth, Inductiveops.infer_inductive_subtyping env'' evd mind_ent) + end + else (pth, mind_ent) + + type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry let inInductive : inductive_obj -> obj = @@ -365,7 +380,8 @@ let inInductive : inductive_obj -> obj = open_function = open_inductive; classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; - discharge_function = discharge_inductive } + discharge_function = discharge_inductive; + rebuild_function = infer_inductive_subtyping } let declare_projections mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in -- cgit v1.2.3 From 7b5fcef8a0fb3b97a3980f10596137234061990f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 26 Apr 2017 15:24:35 +0200 Subject: Fix bugs --- library/declare.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index fcaadaa6e0..bf5313545c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -364,9 +364,9 @@ let infer_inductive_subtyping (pth, mind_ent) = let env' = Environ.push_context (Univ.UInfoInd.univ_context mind_ent.mind_entry_universes) env in - let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in - let evd = Evd.from_env env'' in - (pth, Inductiveops.infer_inductive_subtyping env'' evd mind_ent) + (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) + let evd = Evd.from_env env' in + (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent) end else (pth, mind_ent) -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- library/declare.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index bf5313545c..e2b726f457 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -352,13 +352,14 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; + mind_entry_cumulative = false; mind_entry_universes = Univ.UInfoInd.empty; mind_entry_private = None; }) (* reinfer subtyping constraints for inductive after section is dischared. *) let infer_inductive_subtyping (pth, mind_ent) = - if mind_ent.mind_entry_polymorphic then + if mind_ent.mind_entry_polymorphic && mind_ent.mind_entry_cumulative then begin let env = Global.env () in let env' = @@ -370,7 +371,6 @@ let infer_inductive_subtyping (pth, mind_ent) = end else (pth, mind_ent) - type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry let inInductive : inductive_obj -> obj = -- cgit v1.2.3 From 47ce63d23b8efe35babe0f4429c550400afd6b4f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 4 May 2017 17:53:12 +0200 Subject: Move univops from kernel to library --- library/library.mllib | 1 + library/univops.ml | 70 +++++++++++++++++++++++++++++++++++++++++++++++++++ library/univops.mli | 17 +++++++++++++ 3 files changed, 88 insertions(+) create mode 100644 library/univops.ml create mode 100644 library/univops.mli (limited to 'library') diff --git a/library/library.mllib b/library/library.mllib index 6f433b77d1..d94fc22919 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,3 +1,4 @@ +Univops Nameops Libnames Globnames diff --git a/library/univops.ml b/library/univops.ml new file mode 100644 index 0000000000..e9383c6d9f --- /dev/null +++ b/library/univops.ml @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> fold_constr aux s c + in aux LSet.empty c + +let universes_of_inductive mind = + if mind.mind_polymorphic then + begin + let u = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in + let univ_of_one_ind oind = + let arity_univs = + Context.Rel.fold_outside + (fun decl unvs -> + Univ.LSet.union + (Context.Rel.Declaration.fold_constr + (fun cnstr unvs -> + let cnstr = Vars.subst_instance_constr u cnstr in + Univ.LSet.union + (universes_of_constr cnstr) unvs) + decl Univ.LSet.empty) unvs) + oind.mind_arity_ctxt ~init:Univ.LSet.empty + in + Array.fold_left (fun unvs cns -> + let cns = Vars.subst_instance_constr u cns in + Univ.LSet.union (universes_of_constr cns) unvs) arity_univs + oind.mind_nf_lc + in + let univs = Array.fold_left (fun unvs pk -> Univ.LSet.union (univ_of_one_ind pk) unvs) Univ.LSet.empty mind.mind_packets in + let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mind.mind_universes)) in + let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in + univs + end + else LSet.empty + +let restrict_universe_context (univs,csts) s = + (* Universes that are not necessary to typecheck the term. + E.g. univs introduced by tactics and not used in the proof term. *) + let diff = LSet.diff univs s in + let rec aux diff candid univs ness = + let (diff', candid', univs', ness') = + Constraint.fold + (fun (l, d, r as c) (diff, candid, univs, csts) -> + if not (LSet.mem l diff) then + (LSet.remove r diff, candid, univs, Constraint.add c csts) + else if not (LSet.mem r diff) then + (LSet.remove l diff, candid, univs, Constraint.add c csts) + else (diff, Constraint.add c candid, univs, csts)) + candid (diff, Constraint.empty, univs, ness) + in + if ness' == ness then (LSet.diff univs diff', ness) + else aux diff' candid' univs' ness' + in aux diff csts univs Constraint.empty diff --git a/library/univops.mli b/library/univops.mli new file mode 100644 index 0000000000..5b499c75bc --- /dev/null +++ b/library/univops.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* universe_set +val universes_of_inductive : mutual_inductive_body -> universe_set +val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set -- cgit v1.2.3 From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- library/declare.ml | 19 ++++++++++--------- library/global.ml | 38 +++++++++++++++----------------------- library/lib.ml | 6 +++--- library/lib.mli | 2 +- library/univops.ml | 23 ++++++++++++++++------- 5 files changed, 45 insertions(+), 43 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index e2b726f457..db3dbcbd92 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) = assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in - add_section_constant cst.const_polymorphic kn' cst.const_hyps; + add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (constant_of_kn kn) obj.cst_kind @@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let kn' = Global.add_mind dir id mie in assert (eq_mind kn' (mind_of_kn kn)); let mind = Global.lookup_mind kn' in - add_section_kn mind.mind_polymorphic kn' mind.mind_hyps; + add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names @@ -351,25 +351,26 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_record = None; mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_polymorphic = false; - mind_entry_cumulative = false; - mind_entry_universes = Univ.UInfoInd.empty; + mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty; mind_entry_private = None; }) (* reinfer subtyping constraints for inductive after section is dischared. *) -let infer_inductive_subtyping (pth, mind_ent) = - if mind_ent.mind_entry_polymorphic && mind_ent.mind_entry_cumulative then +let infer_inductive_subtyping (pth, mind_ent) = + match mind_ent.mind_entry_universes with + | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> + (pth, mind_ent) + | Cumulative_ind_entry cumi -> begin let env = Global.env () in let env' = - Environ.push_context (Univ.UInfoInd.univ_context mind_ent.mind_entry_universes) env + Environ.push_context + (Univ.CumulativityInfo.univ_context cumi) env in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) let evd = Evd.from_env env' in (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent) end - else (pth, mind_ent) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry diff --git a/library/global.ml b/library/global.ml index a459983849..6d80012f47 100644 --- a/library/global.ml +++ b/library/global.ml @@ -176,19 +176,14 @@ let type_of_global_unsafe r = Vars.subst_instance_constr (Univ.UContext.instance univs) ty | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let inst = - if mib.Declarations.mind_polymorphic then - Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) - else Univ.Instance.empty - in + let inst = Declareops.inductive_polymorphic_instance mib in Inductive.type_of_inductive env (specif, inst) | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in - Inductive.type_of_constructor (cstr,inst) specif + let inst = Declareops.inductive_polymorphic_instance mib in + Inductive.type_of_constructor (cstr,inst) specif let type_of_global_in_context env r = - let open Declarations in match r with | VarRef id -> Environ.named_type id env, Univ.UContext.empty | ConstRef c -> @@ -199,21 +194,17 @@ let type_of_global_in_context env r = Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let univs = - if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) - else Univ.UContext.empty - in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs + let univs = Declareops.inductive_polymorphic_context mib in + Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let univs = - if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) - else Univ.UContext.empty - in - let inst = Univ.UContext.instance univs in - Inductive.type_of_constructor (cstr,inst) specif, univs + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.UContext.instance univs in + Inductive.type_of_constructor (cstr,inst) specif, univs let universes_of_global env r = - let open Declarations in match r with | VarRef id -> Univ.UContext.empty | ConstRef c -> @@ -222,10 +213,11 @@ let universes_of_global env r = (Environ.opaque_tables env) cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in - Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) + Declareops.inductive_polymorphic_context mib | ConstructRef cstr -> - let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) + let (mib,oib) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + Declareops.inductive_polymorphic_context mib let universes_of_global gr = universes_of_global (env ()) gr diff --git a/library/lib.ml b/library/lib.ml index f22f53eadf..8127316d73 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -402,7 +402,7 @@ let find_opening_node id = type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t +type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t @@ -465,9 +465,9 @@ let add_section_replacement f g poly hyps = let () = check_same_poly poly vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in - let subst, ctx = Univ.abstract_universes true ctx in + let subst, ctx = Univ.abstract_universes ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.UContext.instance ctx,args) exps, + sectab := (vars,f (Univ.AUContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl let add_section_kn poly kn = diff --git a/library/lib.mli b/library/lib.mli index f47d6e1a58..284d339801 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -157,7 +157,7 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t +type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.Named.t diff --git a/library/univops.ml b/library/univops.ml index e9383c6d9f..60c12f0d81 100644 --- a/library/univops.ml +++ b/library/univops.ml @@ -22,9 +22,8 @@ let universes_of_constr c = in aux LSet.empty c let universes_of_inductive mind = - if mind.mind_polymorphic then - begin - let u = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in + let process auctx = + let u = Univ.AUContext.instance auctx in let univ_of_one_ind oind = let arity_univs = Context.Rel.fold_outside @@ -43,12 +42,22 @@ let universes_of_inductive mind = Univ.LSet.union (universes_of_constr cns) unvs) arity_univs oind.mind_nf_lc in - let univs = Array.fold_left (fun unvs pk -> Univ.LSet.union (univ_of_one_ind pk) unvs) Univ.LSet.empty mind.mind_packets in - let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mind.mind_universes)) in + let univs = + Array.fold_left + (fun unvs pk -> + Univ.LSet.union + (univ_of_one_ind pk) unvs + ) + Univ.LSet.empty mind.mind_packets + in + let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in univs - end - else LSet.empty + in + match mind.mind_universes with + | Monomorphic_ind _ -> LSet.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) let restrict_universe_context (univs,csts) s = (* Universes that are not necessary to typecheck the term. -- cgit v1.2.3