From 601ce3738253e4bb197900ee6dad271c4e3666d6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 27 Sep 2018 14:23:25 +0200 Subject: Adding universe names to polymorphic entry instances. --- interp/declare.ml | 14 +++++++------- interp/discharge.ml | 6 ++++-- interp/modintern.ml | 2 +- 3 files changed, 12 insertions(+), 10 deletions(-) (limited to 'interp') diff --git a/interp/declare.ml b/interp/declare.ml index 7a32018c0e..29e777d0c6 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -219,7 +219,7 @@ let cache_variable ((sp,_),o) = let (body, uctx), () = Future.force de.const_entry_body in let poly, univs = match de.const_entry_universes with | Monomorphic_const_entry uctx -> false, uctx - | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx + | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in (** We must declare the universe constraints before type-checking the @@ -339,7 +339,7 @@ let infer_inductive_subtyping mind_ent = match mind_ent.mind_entry_universes with | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> mind_ent - | Cumulative_ind_entry cumi -> + | Cumulative_ind_entry (_, cumi) -> begin let env = Global.env () in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) @@ -366,14 +366,14 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter | Monomorphic_ind_entry _ -> (** Global constraints already defined through the inductive *) Monomorphic_const_entry Univ.ContextSet.empty - | Polymorphic_ind_entry ctx -> - Polymorphic_const_entry ctx - | Cumulative_ind_entry ctx -> - Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx) + | Polymorphic_ind_entry (nas, ctx) -> + Polymorphic_const_entry (nas, ctx) + | Cumulative_ind_entry (nas, ctx) -> + Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx) in let term, types = match univs with | Monomorphic_const_entry _ -> term, types - | Polymorphic_const_entry ctx -> + | Polymorphic_const_entry (_, ctx) -> let u = Univ.UContext.instance ctx in Vars.subst_instance_constr u term, Vars.subst_instance_constr u types in diff --git a/interp/discharge.ml b/interp/discharge.ml index 21b2e85e8f..eeda5a6867 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -79,13 +79,15 @@ let process_inductive info modlist mib = | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx | Polymorphic_ind auctx -> let subst, auctx = Lib.discharge_abstract_universe_context info auctx in + let nas = Univ.AUContext.names auctx in let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_ind_entry auctx + subst, Polymorphic_ind_entry (nas, auctx) | Cumulative_ind cumi -> let auctx = Univ.ACumulativityInfo.univ_context cumi in let subst, auctx = Lib.discharge_abstract_universe_context info auctx in + let nas = Univ.AUContext.names auctx in let auctx = Univ.AUContext.repr auctx in - subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx) + subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx) in let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in let inds = diff --git a/interp/modintern.ml b/interp/modintern.ml index 51e27299e3..93aa271e8b 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -107,7 +107,7 @@ let transl_with_decl env base kind = function let c, ectx = interp_constr env sigma c in let poly = lookup_polymorphism env base kind fqid in begin match UState.check_univ_decl ~poly ectx udecl with - | Entries.Polymorphic_const_entry ctx -> + | Entries.Polymorphic_const_entry (nas, ctx) -> let inst, ctx = Univ.abstract_universes ctx in let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let c = EConstr.to_constr sigma c in -- cgit v1.2.3 From 168af2ba6ae1facf948c7c7bee725ac0f0cd3b41 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 27 Sep 2018 15:34:28 +0200 Subject: Force the user to provide names when generating abstract universe contexts. For now this data is not stored, but the code checks that indeed the number of names provided coincide with the instance length. I had to reimplement the same kind of workaround hack in section handling as the one already performed in UnivNames because the name information is not present in the section data structure. This deserves a FIXME. --- interp/modintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/modintern.ml b/interp/modintern.ml index 93aa271e8b..60056dfd90 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -108,7 +108,7 @@ let transl_with_decl env base kind = function let poly = lookup_polymorphism env base kind fqid in begin match UState.check_univ_decl ~poly ectx udecl with | Entries.Polymorphic_const_entry (nas, ctx) -> - let inst, ctx = Univ.abstract_universes ctx in + let inst, ctx = Univ.abstract_universes nas ctx in let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let c = EConstr.to_constr sigma c in WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty -- cgit v1.2.3 From 6e5dd2ee8bc014d1f99cef3156a5114b11510398 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 27 Sep 2018 17:00:10 +0200 Subject: Remove remnants of polymorphic instance name registration. --- interp/declare.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/declare.ml b/interp/declare.ml index 29e777d0c6..fe8fc7c969 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -520,7 +520,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj = let declare_univ_binders gr pl = if Global.is_polymorphic gr then - UnivNames.register_universe_binders gr pl + () else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c -- cgit v1.2.3