From 7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 16 Apr 2020 23:06:35 +0200 Subject: Remove mod_constraints field of module body --- checker/mod_checking.ml | 1 - checker/safe_checking.ml | 2 +- checker/values.ml | 6 +- .../user-overlays/12107-SkySkimmer-no-mod-univs.sh | 6 ++ kernel/declarations.ml | 2 - kernel/declareops.ml | 3 - kernel/environ.ml | 3 + kernel/environ.mli | 2 + kernel/mod_typing.ml | 71 ++++++++-------- kernel/mod_typing.mli | 8 +- kernel/modops.ml | 3 +- kernel/safe_typing.ml | 66 +++++++-------- kernel/safe_typing.mli | 1 + kernel/subtyping.ml | 2 - plugins/extraction/extract_env.ml | 3 +- vernac/declaremods.ml | 97 +++++++++++----------- 16 files changed, 140 insertions(+), 136 deletions(-) create mode 100644 dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 44b7089fd0..e3cca50f06 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -84,7 +84,6 @@ let mk_mtb mp sign delta = mod_expr = (); mod_type = sign; mod_type_alg = None; - mod_constraints = Univ.ContextSet.empty; mod_delta = delta; mod_retroknowledge = ModTypeRK; } diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml index 524ffbc022..b5beab532e 100644 --- a/checker/safe_checking.ml +++ b/checker/safe_checking.ml @@ -14,7 +14,7 @@ open Environ let import senv clib univs digest = let mb = Safe_typing.module_of_library clib in let env = Safe_typing.env_of_safe_env senv in - let env = push_context_set ~strict:true mb.mod_constraints env in + let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in let env = push_context_set ~strict:true univs env in let env = Modops.add_retroknowledge mb.mod_retroknowledge env in Mod_checking.check_module env mb.mod_mp mb; diff --git a/checker/values.ml b/checker/values.ml index b9efce6948..2bd6a37d0b 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -356,17 +356,17 @@ and v_impl = and v_noimpl = v_unit and v_module = Tuple ("module_body", - [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_retroknowledge|]) + [|v_mp;v_impl;v_sign;Opt v_mexpr;v_resolver;v_retroknowledge|]) and v_modtype = Tuple ("module_type_body", - [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|]) + [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_resolver;v_unit|]) (** kernel/safe_typing *) let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |]) let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|]) let v_compiled_lib = - v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|] + v_tuple "compiled" [|v_dp;v_module;v_context_set;v_deps;v_engagement;Any|] (** Library objects *) diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh new file mode 100644 index 0000000000..b5faabcfe1 --- /dev/null +++ b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then + + elpi_CI_REF=no-mod-univs + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + +fi diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 244cd2865d..d5f219b55f 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -293,8 +293,6 @@ and 'a generic_module_body = mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) mod_type_alg : module_expression option; (** algebraic type *) - mod_constraints : Univ.ContextSet.t; (** - set of all universes constraints in the module *) mod_delta : Mod_subst.delta_resolver; (** quotiented set of equivalent constants and inductive names *) mod_retroknowledge : 'a module_retroknowledge } diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 20dc21900c..0cd5dea53d 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -390,7 +390,6 @@ and hcons_generic_module_body : let expr' = hcons_impl mb.mod_expr in let type' = hcons_module_signature mb.mod_type in let type_alg' = mb.mod_type_alg in - let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in let delta' = mb.mod_delta in let retroknowledge' = mb.mod_retroknowledge in @@ -399,7 +398,6 @@ and hcons_generic_module_body : mb.mod_expr == expr' && mb.mod_type == type' && mb.mod_type_alg == type_alg' && - mb.mod_constraints == constraints' && mb.mod_delta == delta' && mb.mod_retroknowledge == retroknowledge' then mb @@ -408,7 +406,6 @@ and hcons_generic_module_body : mod_expr = expr'; mod_type = type'; mod_type_alg = type_alg'; - mod_constraints = constraints'; mod_delta = delta'; mod_retroknowledge = retroknowledge'; } diff --git a/kernel/environ.ml b/kernel/environ.ml index de8692ff21..93f1b051ab 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -279,6 +279,9 @@ let indices_matter env = env.env_typing_flags.indices_matter let universes env = env.env_stratification.env_universes let universes_lbound env = env.env_stratification.env_universes_lbound +let set_universes g env = + {env with env_stratification = {env.env_stratification with env_universes=g}} + let set_universes_lbound env lbound = let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in { env with env_stratification } diff --git a/kernel/environ.mli b/kernel/environ.mli index 25ecdfd852..9e35e2f608 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -102,6 +102,8 @@ val rel_context : env -> Constr.rel_context val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val +val set_universes : UGraph.t -> env -> env + val opaque_tables : env -> Opaqueproof.opaquetab val set_opaque_tables : env -> Opaqueproof.opaquetab -> env diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 76e2a584bd..44b010204b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -23,7 +23,7 @@ open Modops open Mod_subst type 'alg translation = - module_signature * 'alg * delta_resolver * Univ.ContextSet.t + module_signature * 'alg * delta_resolver * Univ.Constraint.t let rec mp_from_mexpr = function | MEident mp -> mp @@ -54,8 +54,6 @@ let rec rebuild_mp mp l = | []-> mp | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r -let (+++) = Univ.ContextSet.union - let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let lab,idl = match idl with | [] -> assert false @@ -173,10 +171,10 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = | Abstract -> let mtb_old = module_type_of_module old in let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in - Univ.ContextSet.add_constraints chk_cst old.mod_constraints + chk_cst | Algebraic (NoFunctor (MEident(mp'))) -> check_modpath_equiv env' mp1 mp'; - old.mod_constraints + Univ.Constraint.empty | _ -> error_generative_module_expected lab in let mp' = MPdot (mp,lab) in @@ -185,7 +183,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = { new_mb with mod_mp = mp'; mod_expr = Algebraic (NoFunctor (MEident mp1)); - mod_constraints = cst } + } in let new_equiv = add_delta_resolver equiv new_mb.mod_delta in (* we propagate the new equality in the rest of the signature @@ -219,7 +217,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = | Algebraic (NoFunctor (MEident mp0)) -> let mpnew = rebuild_mp mp0 idl in check_modpath_equiv env' mpnew mp; - before@(lab,spec)::after, equiv, Univ.ContextSet.empty + before@(lab,spec)::after, equiv, Univ.Constraint.empty | _ -> error_generative_module_expected lab end with @@ -231,11 +229,11 @@ let check_with env mp (sign,alg,reso,cst) = function let struc = destr_nofunctor sign in let struc', c', cst' = check_with_def env struc (idl, (c, ctx)) mp reso in let wd' = WithDef (idl, (c', ctx)) in - NoFunctor struc', MEwith (alg,wd'), reso, Univ.ContextSet.add_constraints cst' cst + NoFunctor struc', MEwith (alg,wd'), reso, Univ.Constraint.union cst' cst |WithMod(idl,mp1) as wd -> let struc = destr_nofunctor sign in let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in - NoFunctor struc', MEwith (alg,wd), reso', cst+++cst' + NoFunctor struc', MEwith (alg,wd), reso', Univ.Constraint.union cst' cst let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg = let farg_id, farg_b, fbody_b = destr_functor sign in @@ -247,7 +245,7 @@ let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg = let body = subst_signature subst fbody_b in let alg' = mkalg alg mp1 in let reso' = subst_codom_delta_resolver subst reso in - body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1 + body,alg',reso', Univ.Constraint.union cst2 cst1 (** Translation of a module struct entry : - We translate to a module when a [module_path] is given, @@ -266,7 +264,7 @@ let rec translate_mse env mpo inl = function let mt = lookup_modtype mp1 env in module_body_of_type mt.mod_mp mt in - mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty + mb.mod_type, me, mb.mod_delta, Univ.Constraint.empty |MEapply (fe,mp1) -> translate_apply env inl (translate_mse env mpo inl fe) mp1 mk_alg_app |MEwith(me, with_decl) -> @@ -274,17 +272,16 @@ let rec translate_mse env mpo inl = function let mp = mp_from_mexpr me in check_with env mp (translate_mse env None inl me) with_decl -let mk_mod mp e ty cst reso = +let mk_mod mp e ty reso = { mod_mp = mp; mod_expr = e; mod_type = ty; mod_type_alg = None; - mod_constraints = cst; mod_delta = reso; mod_retroknowledge = ModBodyRK []; } -let mk_modtype mp ty cst reso = - let mb = mk_mod mp Abstract ty cst reso in +let mk_modtype mp ty reso = + let mb = mk_mod mp Abstract ty reso in { mb with mod_expr = (); mod_retroknowledge = ModTypeRK } let rec translate_mse_funct env mpo inl mse = function @@ -293,45 +290,45 @@ let rec translate_mse_funct env mpo inl mse = function sign, NoFunctor alg, reso, cst |(mbid, ty) :: params -> let mp_id = MPbound mbid in - let mtb = translate_modtype env mp_id inl ([],ty) in + let mtb, cst = translate_modtype env mp_id inl ([],ty) in let env' = add_module_type mp_id mtb env in - let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in + let sign,alg,reso,cst' = translate_mse_funct env' mpo inl mse params in let alg' = MoreFunctor (mbid,mtb,alg) in - MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints + MoreFunctor (mbid, mtb, sign), alg',reso, Univ.Constraint.union cst cst' and translate_modtype env mp inl (params,mte) = let sign,alg,reso,cst = translate_mse_funct env None inl mte params in - let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in + let mtb = mk_modtype (mp_from_mexpr mte) sign reso in let mtb' = subst_modtype_and_resolver mtb mp in - { mtb' with mod_type_alg = Some alg } + { mtb' with mod_type_alg = Some alg }, cst (** [finalize_module] : from an already-translated (or interactive) implementation and an (optional) signature entry, produces a final [module_body] *) -let finalize_module env mp (sign,alg,reso,cst) restype = match restype with - |None -> +let finalize_module env mp (sign,alg,reso,cst1) restype = match restype with + | None -> let impl = match alg with Some e -> Algebraic e | None -> FullStruct in - mk_mod mp impl sign cst reso - |Some (params_mte,inl) -> - let res_mtb = translate_modtype env mp inl params_mte in - let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in - let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in + mk_mod mp impl sign reso, cst1 + | Some (params_mte,inl) -> + let res_mtb, cst2 = translate_modtype env mp inl params_mte in + let auto_mtb = mk_modtype mp sign reso in + let cst3 = Subtyping.check_subtypes env auto_mtb res_mtb in let impl = match alg with Some e -> Algebraic e | None -> Struct sign in { res_mtb with mod_mp = mp; mod_expr = impl; mod_retroknowledge = ModBodyRK []; - (** cst from module body typing, - cst' from subtyping, - constraints from module type. *) - mod_constraints = - Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) } + }, + (** cst from module body typing, + cst' from subtyping, + constraints from module type. *) + Univ.Constraint.(union cst1 (union cst2 cst3)) let translate_module env mp inl = function |MType (params,ty) -> - let mtb = translate_modtype env mp inl (params,ty) in - module_body_of_type mp mtb + let mtb, cst = translate_modtype env mp inl (params,ty) in + module_body_of_type mp mtb, cst |MExpr (params,mse,oty) -> let (sg,alg,reso,cst) = translate_mse_funct env (Some mp) inl mse params in let restype = Option.map (fun ty -> ((params,ty),inl)) oty in @@ -364,7 +361,7 @@ let rec translate_mse_inclmod env mp inl = function |MEident mp1 -> let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in let sign = clean_bounded_mod_expr mb.mod_type in - sign,(),mb.mod_delta,Univ.ContextSet.empty + sign,(),mb.mod_delta,Univ.Constraint.empty |MEapply (fe,arg) -> let ftrans = translate_mse_inclmod env mp inl fe in translate_apply env inl ftrans arg (fun _ _ -> ()) @@ -375,6 +372,6 @@ let translate_mse_incl is_mod env mp inl me = let () = forbid_incl_signed_functor env me in translate_mse_inclmod env mp inl me else - let mtb = translate_modtype env mp inl ([],me) in + let mtb, cst = translate_modtype env mp inl ([],me) in let sign = clean_bounded_mod_expr mtb.mod_type in - sign,(),mtb.mod_delta,mtb.mod_constraints + sign, (), mtb.mod_delta, cst diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index fd5421aefe..94a4b17df3 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -23,13 +23,13 @@ open Names *) val translate_module : - env -> ModPath.t -> inline -> module_entry -> module_body + env -> ModPath.t -> inline -> module_entry -> module_body * Univ.Constraint.t (** [translate_modtype] produces a [module_type_body] whose [mod_type_alg] cannot be [None] (and of course [mod_expr] is [Abstract]). *) val translate_modtype : - env -> ModPath.t -> inline -> module_type_entry -> module_type_body + env -> ModPath.t -> inline -> module_type_entry -> module_type_body * Univ.Constraint.t (** Low-level function for translating a module struct entry : - We translate to a module when a [ModPath.t] is given, @@ -39,7 +39,7 @@ val translate_modtype : the extraction. *) type 'alg translation = - module_signature * 'alg * delta_resolver * Univ.ContextSet.t + module_signature * 'alg * delta_resolver * Univ.Constraint.t val translate_mse : env -> ModPath.t option -> inline -> module_struct_entry -> @@ -51,7 +51,7 @@ val translate_mse : val finalize_module : env -> ModPath.t -> (module_expression option) translation -> (module_type_entry * inline) option -> - module_body + module_body * Univ.Constraint.t (** [translate_mse_incl] translate the mse of a module or module type given to an Include *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 301af328e4..77ef38dfd5 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -225,8 +225,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> && retro==retro' && delta'==mb.mod_delta then mb else - { mb with - mod_mp = mp'; + { mod_mp = mp'; mod_expr = me'; mod_type = ty'; mod_type_alg = aty'; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 58b516dfdd..3b70aba884 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -116,6 +116,7 @@ type module_parameters = (MBId.t * module_type_body) list type compiled_library = { comp_name : DirPath.t; comp_mod : module_body; + comp_univs : Univ.ContextSet.t; comp_deps : library_info array; comp_enga : engagement; comp_natsymbs : Nativevalues.symbols @@ -566,8 +567,7 @@ let constraints_of_sfb sfb = match sfb with | SFBconst cb -> globalize_constant_universes cb | SFBmind mib -> globalize_mind_universes mib - | SFBmodtype mtb -> [mtb.mod_constraints] - | SFBmodule mb -> [mb.mod_constraints] + | SFBmodtype _ | SFBmodule _ -> [] let add_retroknowledge pttc senv = { senv with @@ -986,35 +986,35 @@ let add_mind l mie senv = let add_modtype l params_mte inl senv = let mp = MPdot(senv.modpath, l) in - let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte in + let mtb, cst = Mod_typing.translate_modtype senv.env mp inl params_mte in + let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in let mtb = Declareops.hcons_module_type mtb in - let senv' = add_field (l,SFBmodtype mtb) MT senv in - mp, senv' + let senv = add_field (l,SFBmodtype mtb) MT senv in + mp, senv (** full_add_module adds module with universes and constraints *) let full_add_module mb senv = - let senv = add_constraints (Now mb.mod_constraints) senv in let dp = ModPath.dp mb.mod_mp in let linkinfo = Nativecode.link_info_of_dirpath dp in { senv with env = Modops.add_linked_module mb linkinfo senv.env } let full_add_module_type mp mt senv = - let senv = add_constraints (Now mt.mod_constraints) senv in { senv with env = Modops.add_module_type mp mt senv.env } (** Insertion of modules *) let add_module l me inl senv = let mp = MPdot(senv.modpath, l) in - let mb = Mod_typing.translate_module senv.env mp inl me in + let mb, cst = Mod_typing.translate_module senv.env mp inl me in + let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in let mb = Declareops.hcons_module_body mb in - let senv' = add_field (l,SFBmodule mb) M senv in - let senv'' = - if Modops.is_functor mb.mod_type then senv' - else update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv' + let senv = add_field (l,SFBmodule mb) M senv in + let senv = + if Modops.is_functor mb.mod_type then senv + else update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv in - (mp,mb.mod_delta),senv'' + (mp,mb.mod_delta),senv (** {6 Starting / ending interactive modules and module types } *) @@ -1046,7 +1046,8 @@ let start_modtype l senv = let add_module_parameter mbid mte inl senv = let () = check_empty_struct senv in let mp = MPbound mbid in - let mtb = Mod_typing.translate_modtype senv.env mp inl ([],mte) in + let mtb, cst = Mod_typing.translate_modtype senv.env mp inl ([],mte) in + let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in let senv = full_add_module_type mp mtb senv in let new_variant = match senv.modvariant with | STRUCT (params,oldenv) -> STRUCT ((mbid,mtb) :: params, oldenv) @@ -1084,12 +1085,12 @@ let functorize_module params mb = let build_module_body params restype senv = let struc = NoFunctor (List.rev senv.revstruct) in let restype' = Option.map (fun (ty,inl) -> (([],ty),inl)) restype in - let mb = + let mb, cst = Mod_typing.finalize_module senv.env senv.modpath - (struc,None,senv.modresolver,senv.univ) restype' + (struc,None,senv.modresolver,Univ.Constraint.empty) restype' in let mb' = functorize_module params mb in - { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge } + { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge }, cst (** Returning back to the old pre-interactive-module environment, with one extra component and some updated fields @@ -1129,15 +1130,13 @@ let end_module l restype senv = let () = check_current_label l mp in let () = check_empty_context senv in let mbids = List.rev_map fst params in - let mb = build_module_body params restype senv in + let mb, cst = build_module_body params restype senv in + let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in let newenv = set_engagement_opt newenv senv.engagement in - let senv'= - propagate_loads { senv with - env = newenv; - univ = Univ.ContextSet.union senv.univ mb.mod_constraints} in - let newenv = Environ.push_context_set ~strict:true mb.mod_constraints senv'.env in + let newenv = Environ.set_universes (Environ.universes senv.env) newenv in + let senv' = propagate_loads { senv with env = newenv } in let newenv = Modops.add_module mb newenv in let newresolver = if Modops.is_functor mb.mod_type then oldsenv.modresolver @@ -1146,12 +1145,11 @@ let end_module l restype senv = (mp,mbids,mb.mod_delta), propagate_senv (l,SFBmodule mb) newenv newresolver senv' oldsenv -let build_mtb mp sign cst delta = +let build_mtb mp sign delta = { mod_mp = mp; mod_expr = (); mod_type = sign; mod_type_alg = None; - mod_constraints = cst; mod_delta = delta; mod_retroknowledge = ModTypeRK } @@ -1163,11 +1161,11 @@ let end_modtype l senv = let mbids = List.rev_map fst params in let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in - let newenv = Environ.push_context_set ~strict:true senv.univ newenv in let newenv = set_engagement_opt newenv senv.engagement in + let newenv = Environ.set_universes (Environ.universes senv.env) newenv in let senv' = propagate_loads {senv with env=newenv} in let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in - let mtb = build_mtb mp auto_tb senv'.univ senv.modresolver in + let mtb = build_mtb mp auto_tb senv.modresolver in let newenv = Environ.add_modtype mtb senv'.env in let newresolver = oldsenv.modresolver in (mp,mbids), @@ -1181,7 +1179,7 @@ let add_include me is_module inl senv = let sign,(),resolver,cst = translate_mse_incl is_module senv.env mp_sup inl me in - let senv = add_constraints (Now cst) senv in + let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in (* Include Self support *) let rec compute_sign sign mb resolver senv = match sign with @@ -1201,7 +1199,7 @@ let add_include me is_module inl senv = in let resolver,str,senv = let struc = NoFunctor (List.rev senv.revstruct) in - let mtb = build_mtb mp_sup struc Univ.ContextSet.empty senv.modresolver in + let mtb = build_mtb mp_sup struc senv.modresolver in compute_sign sign mtb resolver senv in let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv @@ -1223,6 +1221,8 @@ let add_include me is_module inl senv = let module_of_library lib = lib.comp_mod +let univs_of_library lib = lib.comp_univs + type native_library = Nativecode.global list (** FIXME: MS: remove?*) @@ -1251,7 +1251,6 @@ let export ?except ~output_native_objects senv dir = mod_expr = FullStruct; mod_type = str; mod_type_alg = None; - mod_constraints = senv.univ; mod_delta = senv.modresolver; mod_retroknowledge = ModBodyRK senv.local_retroknowledge } @@ -1264,6 +1263,7 @@ let export ?except ~output_native_objects senv dir = let lib = { comp_name = dir; comp_mod = mb; + comp_univs = senv.univ; comp_deps = Array.of_list (DPmap.bindings senv.required); comp_enga = Environ.engagement senv.env; comp_natsymbs = symbols } @@ -1271,7 +1271,7 @@ let export ?except ~output_native_objects senv dir = mp, lib, ast (* cst are the constraints that were computed by the vi2vo step and hence are - * not part of the mb.mod_constraints field (but morally should be) *) + * not part of the [lib.comp_univs] field (but morally should be) *) let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; @@ -1281,8 +1281,8 @@ let import lib cst vodigest senv = let mp = MPfile lib.comp_name in let mb = lib.comp_mod in let env = Environ.push_context_set ~strict:true - (Univ.ContextSet.union mb.mod_constraints cst) - senv.env + (Univ.ContextSet.union lib.comp_univs cst) + senv.env in let env = let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b42746a882..58a583e169 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -195,6 +195,7 @@ type compiled_library type native_library = Nativecode.global list val module_of_library : compiled_library -> Declarations.module_body +val univs_of_library : compiled_library -> Univ.ContextSet.t val start_library : DirPath.t -> ModPath.t safe_transformer diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 3f81a62956..28baa82666 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -336,7 +336,6 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = mod_expr = Abstract; mod_type = subst_signature subst1 body_t1; mod_type_alg = None; - mod_constraints = mtb1.mod_constraints; mod_retroknowledge = ModBodyRK []; mod_delta = mtb1.mod_delta} env in @@ -347,7 +346,6 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = let check_subtypes env sup super = let env = add_module_type sup.mod_mp sup env in - let env = Environ.push_context_set ~strict:true super.mod_constraints env in check_modtypes Univ.Constraint.empty env (strengthen sup sup.mod_mp) super empty_subst (map_mp super.mod_mp sup.mod_mp sup.mod_delta) false diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 02383799a9..f7d78551d8 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -163,7 +163,8 @@ let expand_mexpr env mpo me = let expand_modtype env mp me = let inl = Some (Flags.get_inline_level()) in - Mod_typing.translate_modtype env mp inl ([],me) + let mtb, _cst = Mod_typing.translate_modtype env mp inl ([],me) in + mtb let no_delta = Mod_subst.empty_delta_resolver diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 438509e28a..50fa6052f6 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -651,26 +651,28 @@ let mk_params_entry args = let mk_funct_type env args seb0 = List.fold_left - (fun seb (arg_id,arg_t,arg_inl) -> + (fun (seb,cst) (arg_id,arg_t,arg_inl) -> let mp = MPbound arg_id in - let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in - MoreFunctor(arg_id,arg_t,seb)) + let arg_t, cst' = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in + MoreFunctor(arg_id,arg_t,seb), Univ.Constraint.union cst cst') seb0 args (** Prepare the module type list for check of subtypes *) let build_subtypes env mp args mtys = - let (cst, ans) = List.fold_left_map - (fun cst (m,ann) -> + let (ctx, ans) = List.fold_left_map + (fun ctx (m,ann) -> let inl = inl2intopt ann in - let mte, _, cst' = Modintern.interp_module_ast env Modintern.ModType m in - let env = Environ.push_context_set ~strict:true cst' env in - let cst = Univ.ContextSet.union cst cst' in - let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in - cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type }) + let mte, _, ctx' = Modintern.interp_module_ast env Modintern.ModType m in + let env = Environ.push_context_set ~strict:true ctx' env in + let ctx = Univ.ContextSet.union ctx ctx' in + let mtb, cst = Mod_typing.translate_modtype env mp inl ([],mte) in + let mod_type, cst = mk_funct_type env args (mtb.mod_type,cst) in + let ctx = Univ.ContextSet.add_constraints cst ctx in + ctx, { mtb with mod_type }) Univ.ContextSet.empty mtys in - (ans, cst) + (ans, ctx) (** {6 Current module information} @@ -703,23 +705,23 @@ module RawModOps = struct let start_module export id args res fs = let mp = Global.start_module id in - let arg_entries_r, cst = intern_args args in - let () = Global.push_context_set ~strict:true cst in + let arg_entries_r, ctx = intern_args args in + let () = Global.push_context_set ~strict:true ctx in let env = Global.env () in - let res_entry_o, subtyps, cst = match res with + let res_entry_o, subtyps, ctx = match res with | Enforce (res,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType res in - let env = Environ.push_context_set ~strict:true cst env in + let (mte, _, ctx) = Modintern.interp_module_ast env Modintern.ModType res in + let env = Environ.push_context_set ~strict:true ctx env in (* We check immediately that mte is well-formed *) - let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in - let cst = Univ.ContextSet.union cst cst' in - Some (mte, inl), [], cst + let _, _, _, cst = Mod_typing.translate_mse env None inl mte in + let ctx = Univ.ContextSet.add_constraints cst ctx in + Some (mte, inl), [], ctx | Check resl -> - let typs, cst = build_subtypes env mp arg_entries_r resl in - None, typs, cst + let typs, ctx = build_subtypes env mp arg_entries_r resl in + None, typs, ctx in - let () = Global.push_context_set ~strict:true cst in + let () = Global.push_context_set ~strict:true ctx in openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix)); @@ -763,37 +765,38 @@ let end_module () = mp +(* TODO cleanup push universes directly to global env *) let declare_module id args res mexpr_o fs = (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_module id in - let arg_entries_r, cst = intern_args args in + let arg_entries_r, ctx = intern_args args in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let env = Environ.push_context_set ~strict:true cst env in - let mty_entry_o, subs, inl_res, cst' = match res with + let env = Environ.push_context_set ~strict:true ctx env in + let mty_entry_o, subs, inl_res, ctx' = match res with | Enforce (mty,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType mty in - let env = Environ.push_context_set ~strict:true cst env in + let (mte, _, ctx) = Modintern.interp_module_ast env Modintern.ModType mty in + let env = Environ.push_context_set ~strict:true ctx env in (* We check immediately that mte is well-formed *) - let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in - let cst = Univ.ContextSet.union cst cst' in - Some mte, [], inl, cst + let _, _, _, cst = Mod_typing.translate_mse env None inl mte in + let ctx = Univ.ContextSet.add_constraints cst ctx in + Some mte, [], inl, ctx | Check mtys -> - let typs, cst = build_subtypes env mp arg_entries_r mtys in - None, typs, default_inline (), cst + let typs, ctx = build_subtypes env mp arg_entries_r mtys in + None, typs, default_inline (), ctx in - let env = Environ.push_context_set ~strict:true cst' env in - let cst = Univ.ContextSet.union cst cst' in - let mexpr_entry_o, inl_expr, cst' = match mexpr_o with + let env = Environ.push_context_set ~strict:true ctx' env in + let ctx = Univ.ContextSet.union ctx ctx' in + let mexpr_entry_o, inl_expr, ctx' = match mexpr_o with | None -> None, default_inline (), Univ.ContextSet.empty | Some (mexpr,ann) -> - let (mte, _, cst) = Modintern.interp_module_ast env Modintern.Module mexpr in - Some mte, inl2intopt ann, cst + let (mte, _, ctx) = Modintern.interp_module_ast env Modintern.Module mexpr in + Some mte, inl2intopt ann, ctx in - let env = Environ.push_context_set ~strict:true cst' env in - let cst = Univ.ContextSet.union cst cst' in + let env = Environ.push_context_set ~strict:true ctx' env in + let ctx = Univ.ContextSet.union ctx ctx' in let entry = match mexpr_entry_o, mty_entry_o with | None, None -> assert false (* No body, no type ... *) | None, Some typ -> MType (params, typ) @@ -812,7 +815,7 @@ let declare_module id args res mexpr_o fs = | None -> None | _ -> inl_res in - let () = Global.push_context_set ~strict:true cst in + let () = Global.push_context_set ~strict:true ctx in let mp_env,resolver = Global.add_module id entry inl in (* Name consistency check : kernel vs. library *) @@ -864,20 +867,20 @@ let declare_modtype id args mtys (mty,ann) fs = (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args args in - let () = Global.push_context_set ~strict:true cst in + let arg_entries_r, ctx = intern_args args in + let () = Global.push_context_set ~strict:true ctx in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in - let () = Global.push_context_set ~strict:true cst in + let mte, _, ctx = Modintern.interp_module_ast env Modintern.ModType mty in + let () = Global.push_context_set ~strict:true ctx in let env = Global.env () in (* We check immediately that mte is well-formed *) let _, _, _, cst = Mod_typing.translate_mse env None inl mte in - let () = Global.push_context_set ~strict:true cst in + let () = Global.push_context_set ~strict:true (Univ.LSet.empty,cst) in let env = Global.env () in let entry = params, mte in - let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in - let () = Global.push_context_set ~strict:true cst in + let sub_mty_l, ctx = build_subtypes env mp arg_entries_r mtys in + let () = Global.push_context_set ~strict:true ctx in let env = Global.env () in let sobjs = get_functor_sobjs false env inl entry in let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in -- cgit v1.2.3