diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declare.ml | 23 | ||||
| -rw-r--r-- | vernac/declaremods.ml | 97 |
2 files changed, 57 insertions, 63 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 366dd2d026..357f58feea 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -135,11 +135,6 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified (** Declaration of constants and parameters *) -type constant_obj = { - cst_kind : Decls.logical_kind; - cst_locl : import_status; -} - type 'a proof_entry = { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) @@ -265,8 +260,11 @@ type 'a constant_entry = | ParameterEntry of Entries.parameter_entry | PrimitiveEntry of Entries.primitive_entry -(* At load-time, the segment starting from the module name to the discharge *) -(* section (if Remark or Fact) is needed to access a construction *) +type constant_obj = { + cst_kind : Decls.logical_kind; + cst_locl : import_status; +} + let load_constant i ((sp,kn), obj) = if Nametab.exists_cci sp then raise (AlreadyDeclared (None, Libnames.basename sp)); @@ -292,8 +290,7 @@ let check_exists id = raise (AlreadyDeclared (None, id)) let cache_constant ((sp,kn), obj) = - (* Invariant: the constant must exist in the logical environment, except when - redefining it when exiting a section. See [discharge_constant]. *) + (* Invariant: the constant must exist in the logical environment *) let kn' = if Global.exists_objlabel (Label.of_id (Libnames.basename sp)) then Constant.make1 kn @@ -306,13 +303,7 @@ let cache_constant ((sp,kn), obj) = let discharge_constant ((sp, kn), obj) = Some obj -(* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant cst = { - cst_kind = cst.cst_kind; - cst_locl = cst.cst_locl; -} - -let classify_constant cst = Libobject.Substitute (dummy_constant cst) +let classify_constant cst = Libobject.Substitute cst let (objConstant : constant_obj Libobject.Dyn.tag) = let open Libobject in 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 |