diff options
-rw-r--r-- | checker/cic.mli | 4 | ||||
-rw-r--r-- | checker/declarations.ml | 6 | ||||
-rw-r--r-- | checker/values.ml | 9 | ||||
-rw-r--r-- | interp/modintern.ml | 31 | ||||
-rw-r--r-- | interp/modintern.mli | 2 | ||||
-rw-r--r-- | kernel/declarations.ml | 2 | ||||
-rw-r--r-- | kernel/mod_typing.ml | 27 | ||||
-rw-r--r-- | library/declaremods.ml | 116 | ||||
-rw-r--r-- | library/declaremods.mli | 2 | ||||
-rw-r--r-- | test-suite/modules/SeveralWith.v | 12 |
10 files changed, 123 insertions, 88 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 95dd18f5f..1f4322dff 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -358,9 +358,7 @@ type ('ty,'a) functorize = and won't play any role into the kernel after that : they are kept only for short module printing and for extraction. *) -type with_declaration = - | WithMod of Id.t list * ModPath.t - | WithDef of Id.t list * (constr * Univ.universe_context) +type with_declaration type module_alg_expr = | MEident of ModPath.t diff --git a/checker/declarations.ml b/checker/declarations.ml index 15b1f0a0c..2fe930dca 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -573,14 +573,10 @@ let implem_map fs fa = function | Algebraic a -> Algebraic (fa a) | impl -> impl -let subst_with_body sub = function - | WithMod(id,mp) -> WithMod(id,subst_mp sub mp) - | WithDef(id,(c,ctx)) -> WithDef(id,(subst_mps sub c,ctx)) - let rec subst_expr sub = function | MEident mp -> MEident (subst_mp sub mp) | MEapply (me1,mp2)-> MEapply (subst_expr sub me1, subst_mp sub mp2) - | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd) + | MEwith (me,wd)-> MEwith (subst_expr sub me, wd) let rec subst_expression sub me = functor_map (subst_module_type sub) (subst_expr sub) me diff --git a/checker/values.ml b/checker/values.ml index 55e1cdb6f..283adca03 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 483493b20fe91cc1bea4350a2db2f82d checker/cic.mli +MD5 79ed7b5c069b1994bf1a8d2cec22bdce checker/cic.mli *) @@ -295,16 +295,11 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Opt v_bool; v_typing_flags|] -let v_with = - Sum ("with_declaration_body",0, - [|[|List v_id;v_mp|]; - [|List v_id;v_tuple "with_def" [|v_constr;v_context|]|]|]) - let rec v_mae = Sum ("module_alg_expr",0, [|[|v_mp|]; (* SEBident *) [|v_mae;v_mp|]; (* SEBapply *) - [|v_mae;v_with|] (* SEBwith *) + [|v_mae; Any|] (* SEBwith *) |]) let rec v_sfb = diff --git a/interp/modintern.ml b/interp/modintern.ml index 3eb91d8cd..e631b3ea4 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -59,33 +59,42 @@ let lookup_module lqid = fst (lookup_module_or_modtype Module lqid) let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> - WithMod (fqid,lookup_module qid) + WithMod (fqid,lookup_module qid), Univ.ContextSet.empty | CWith_Definition ((_,fqid),c) -> let c, ectx = interp_constr env (Evd.from_env env) c in - let ctx = UState.context ectx in - WithDef (fqid,(c,ctx)) + if Flags.is_universe_polymorphism () then + let ctx = UState.context ectx in + let inst, ctx = Univ.abstract_universes ctx in + let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in + WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty + else + WithDef (fqid,(c, None)), UState.context_set ectx let loc_of_module l = l.CAst.loc (* Invariant : the returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let rec interp_module_ast env kind m = match m.CAst.v with +let rec interp_module_ast env kind m cst = match m.CAst.v with | CMident qid -> let (mp,kind) = lookup_module_or_modtype kind (m.CAst.loc,qid) in - (MEident mp, kind) + (MEident mp, kind, cst) | CMapply (me1,me2) -> - let me1',kind1 = interp_module_ast env kind me1 in - let me2',kind2 = interp_module_ast env ModAny me2 in + let me1',kind1, cst = interp_module_ast env kind me1 cst in + let me2',kind2, cst = interp_module_ast env ModAny me2 cst in let mp2 = match me2' with | MEident mp -> mp | _ -> error_application_to_not_path (loc_of_module me2) me2' in if kind2 == ModType then error_application_to_module_type (loc_of_module me2); - (MEapply (me1',mp2), kind1) + (MEapply (me1',mp2), kind1, cst) | CMwith (me,decl) -> - let me,kind = interp_module_ast env kind me in + let me,kind,cst = interp_module_ast env kind me cst in if kind == Module then error_incorrect_with_in_module m.CAst.loc; - let decl = transl_with_decl env decl in - (MEwith(me,decl), kind) + let decl, cst' = transl_with_decl env decl in + let cst = Univ.ContextSet.union cst cst' in + (MEwith(me,decl), kind, cst) + +let interp_module_ast env kind m = + interp_module_ast env kind m Univ.ContextSet.empty diff --git a/interp/modintern.mli b/interp/modintern.mli index a21b6e231..8d6100667 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -28,4 +28,4 @@ exception ModuleInternalizationError of module_internalization_error isn't ModAny. *) val interp_module_ast : - env -> module_kind -> module_ast -> module_struct_entry * module_kind + env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 5b9e1a141..cb7f0ecef 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -219,7 +219,7 @@ type ('ty,'a) functorize = type with_declaration = | WithMod of Id.t list * ModPath.t - | WithDef of Id.t list * constr Univ.in_universe_context + | WithDef of Id.t list * (constr * Univ.AUContext.t option) type module_alg_expr = | MEident of ModPath.t diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index b7eb481ee..6b89a1da0 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -73,13 +73,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = any implementations of parameters and opaques terms, as long as they have the right type *) let c', univs, ctx' = - match cb.const_universes with - | Monomorphic_const _ -> - (** We do not add the deferred constraints of the body in the - environment, because they do not appear in the type of the - definition. Any inconsistency will be raised at a later stage - when joining the environment. *) - let env' = Environ.push_context ~strict:true ctx env' in + match cb.const_universes, ctx with + | Monomorphic_const _, None -> let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in @@ -91,11 +86,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let c' = Mod_subst.force_constr cs in c, Reduction.infer_conv env' (Environ.universes env') c c' in - let ctx = Univ.ContextSet.of_context ctx in - c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx - | Polymorphic_const uctx -> - let inst, ctx = Univ.abstract_universes ctx in - let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in + c', Monomorphic_const Univ.ContextSet.empty, cst + | Polymorphic_const uctx, Some ctx -> let () = if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab @@ -116,7 +108,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = in if not (Univ.Constraint.is_empty cst) then error_incorrect_with_constraint lab; - c, Polymorphic_const ctx, Univ.ContextSet.empty + c, Polymorphic_const ctx, Univ.Constraint.empty + | _ -> error_incorrect_with_constraint lab in let def = Def (Mod_subst.from_val c') in (* let ctx' = Univ.UContext.make (newus, cst) in *) @@ -225,11 +218,11 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = | Reduction.NotConvertible -> error_incorrect_with_constraint lab let check_with env mp (sign,alg,reso,cst) = function - |WithDef(idl,c) -> + |WithDef(idl, (c, ctx)) -> let struc = destr_nofunctor sign in - let struc',c',cst' = check_with_def env struc (idl,c) mp reso in - let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in - NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst' + 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 |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 diff --git a/library/declaremods.ml b/library/declaremods.ml index 41e00a41c..28a04252a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -442,23 +442,26 @@ let process_module_binding mbid me = Objects in these parameters are also loaded. Output is accumulated on top of [acc] (in reverse order). *) -let intern_arg interp_modast acc (idl,(typ,ann)) = +let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = let inl = inl2intopt ann in let lib_dir = Lib.library_dp() in let env = Global.env() in - let mty,_ = interp_modast env ModType typ in + let (mty, _, cst') = interp_modast env ModType typ in + let () = Global.push_context_set true cst' in + let env = Global.env () in let sobjs = get_module_sobjs false env inl mty in let mp0 = get_module_path mty in - List.fold_left - (fun acc (_,id) -> - let dir = DirPath.make [id] in - let mbid = MBId.make lib_dir id in - let mp = MPbound mbid in - let resolver = Global.add_module_parameter mbid mty inl in - let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in - do_module false Lib.load_objects 1 dir mp sobjs []; - (mbid,mty,inl)::acc) - acc idl + let fold acc (_, id) = + let dir = DirPath.make [id] in + let mbid = MBId.make lib_dir id in + let mp = MPbound mbid in + let resolver = Global.add_module_parameter mbid mty inl in + let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in + do_module false Lib.load_objects 1 dir mp sobjs []; + (mbid,mty,inl)::acc + in + let acc = List.fold_left fold acc idl in + (acc, Univ.ContextSet.union cst cst') (** Process a list of declarations of functor parameters (Id11 .. Id1n : Typ1)..(Idk1 .. Idkm : Typk) @@ -472,7 +475,7 @@ let intern_arg interp_modast acc (idl,(typ,ann)) = *) let intern_args interp_modast params = - List.fold_left (intern_arg interp_modast) [] params + List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params (** {6 Auxiliary functions concerning subtyping checks} *) @@ -524,13 +527,17 @@ let mk_funct_type env args seb0 = (** Prepare the module type list for check of subtypes *) let build_subtypes interp_modast env mp args mtys = - List.map - (fun (m,ann) -> + let (cst, ans) = List.fold_left_map + (fun cst (m,ann) -> let inl = inl2intopt ann in - let mte,_ = interp_modast env ModType m in + let mte, _, cst' = interp_modast env 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 - { mtb with mod_type = mk_funct_type env args mtb.mod_type }) - mtys + cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type }) + Univ.ContextSet.empty mtys + in + (ans, cst) (** {6 Current module information} @@ -563,18 +570,23 @@ module RawModOps = struct let start_module interp_modast export id args res fs = let mp = Global.start_module id in - let arg_entries_r = intern_args interp_modast args in + let arg_entries_r, cst = intern_args interp_modast args in + let () = Global.push_context_set true cst in let env = Global.env () in - let res_entry_o, subtyps = match res with + let res_entry_o, subtyps, cst = match res with | Enforce (res,ann) -> let inl = inl2intopt ann in - let mte,_ = interp_modast env ModType res in + let (mte, _, cst) = interp_modast env ModType res in + let env = Environ.push_context_set ~strict:true cst env in (* We check immediately that mte is well-formed *) - let _ = Mod_typing.translate_mse env None inl mte in - Some (mte,inl), [] + let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in + let cst = Univ.ContextSet.union cst cst' in + Some (mte, inl), [], cst | Check resl -> - None, build_subtypes interp_modast env mp arg_entries_r resl + let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in + None, typs, cst in + let () = Global.push_context_set true cst in 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) (prefix.obj_dir) (DirOpenModule prefix); @@ -622,25 +634,33 @@ let declare_module interp_modast 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 = intern_args interp_modast args in + let arg_entries_r, cst = intern_args interp_modast args in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let mty_entry_o, subs, inl_res = match res with + let env = Environ.push_context_set ~strict:true cst env in + let mty_entry_o, subs, inl_res, cst' = match res with | Enforce (mty,ann) -> let inl = inl2intopt ann in - let mte, _ = interp_modast env ModType mty in + let (mte, _, cst) = interp_modast env ModType mty in + let env = Environ.push_context_set ~strict:true cst env in (* We check immediately that mte is well-formed *) - let _ = Mod_typing.translate_mse env None inl mte in - Some mte, [], inl + let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in + let cst = Univ.ContextSet.union cst cst' in + Some mte, [], inl, cst | Check mtys -> - None, build_subtypes interp_modast env mp arg_entries_r mtys, - default_inline () + let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + None, typs, default_inline (), cst in - let mexpr_entry_o, inl_expr = match mexpr_o with - | None -> None, default_inline () + 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 + | None -> None, default_inline (), Univ.ContextSet.empty | Some (mexpr,ann) -> - Some (fst (interp_modast env Module mexpr)), inl2intopt ann + let (mte, _, cst) = interp_modast env Module mexpr in + Some mte, inl2intopt ann, cst in + let env = Environ.push_context_set ~strict:true cst' env in + let cst = Univ.ContextSet.union cst cst' 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) @@ -659,6 +679,7 @@ let declare_module interp_modast id args res mexpr_o fs = | None -> None | _ -> inl_res in + let () = Global.push_context_set true cst in let mp_env,resolver = Global.add_module id entry inl in (* Name consistency check : kernel vs. library *) @@ -679,9 +700,11 @@ module RawModTypeOps = struct let start_modtype interp_modast id args mtys fs = let mp = Global.start_modtype id in - let arg_entries_r = intern_args interp_modast args in + let arg_entries_r, cst = intern_args interp_modast args in + let () = Global.push_context_set true cst in let env = Global.env () in - let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let () = Global.push_context_set true cst in openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModtype prefix); @@ -708,14 +731,21 @@ let declare_modtype interp_modast 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 = intern_args interp_modast args in + let arg_entries_r, cst = intern_args interp_modast args in + let () = Global.push_context_set true cst in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let mte, _ = interp_modast env ModType mty in + let mte, _, cst = interp_modast env ModType mty in + let () = Global.push_context_set true cst in + let env = Global.env () in (* We check immediately that mte is well-formed *) - let _ = Mod_typing.translate_mse env None inl mte in + let _, _, _, cst = Mod_typing.translate_mse env None inl mte in + let () = Global.push_context_set true cst in + let env = Global.env () in let entry = params, mte in - let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let () = Global.push_context_set true cst 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 let sobjs = subst_sobjs subst sobjs in @@ -769,7 +799,9 @@ let type_of_incl env is_mod = function let declare_one_include interp_modast (me_ast,annot) = let env = Global.env() in - let me,kind = interp_modast env ModAny me_ast in + let me, kind, cst = interp_modast env ModAny me_ast in + let () = Global.push_context_set true cst in + let env = Global.env () in let is_mod = (kind == Module) in let cur_mp = Lib.current_mp () in let inl = inl2intopt annot in @@ -947,7 +979,7 @@ let iter_all_segments f = type 'modast module_interpretor = Environ.env -> Misctypes.module_kind -> 'modast -> - Entries.module_struct_entry * Misctypes.module_kind + Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t type 'modast module_params = (Id.t Loc.located list * ('modast * inline)) list diff --git a/library/declaremods.mli b/library/declaremods.mli index 42e5f4b13..0df55f34d 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -13,7 +13,7 @@ open Vernacexpr type 'modast module_interpretor = Environ.env -> Misctypes.module_kind -> 'modast -> - Entries.module_struct_entry * Misctypes.module_kind + Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t type 'modast module_params = (Id.t Loc.located list * ('modast * inline)) list diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v new file mode 100644 index 000000000..bbf72a764 --- /dev/null +++ b/test-suite/modules/SeveralWith.v @@ -0,0 +1,12 @@ +Module Type S. +Parameter A : Type. +End S. + +Module Type ES. +Parameter A : Type. +Parameter eq : A -> A -> Type. +End ES. + +Module Make + (AX : S) + (X : ES with Definition A := AX.A with Definition eq := @eq AX.A). |