From 42ff3109217452853c3b853d21f09a317dd6e37d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 10 Jun 2019 23:11:06 +0200 Subject: [library] Move `Declaremods` to `vernac/` We move `Declaremods` to the vernac layer as it implement vernac-specific logic to manipulate modules which moreover is highly imperative. This forces code [such as printing] to manipulate the _global imperative_ state which is a bit fishy. The key improvement in this PR is that now `Global` is not used anymore in `library`, so we can proceed to move it upwards. This move is a follow-up of #10562 and a step towards moving `Global` upper, likely to `interp` in the short term. --- interp/modintern.ml | 6 +- interp/modintern.mli | 4 +- library/declaremods.ml | 1078 ----------------------------------------------- library/declaremods.mli | 141 ------- library/library.mllib | 1 - printing/prettyp.ml | 63 +-- printing/prettyp.mli | 37 +- printing/printmod.ml | 75 ++-- printing/printmod.mli | 10 +- toplevel/coqc.ml | 5 +- vernac/declaremods.ml | 1077 ++++++++++++++++++++++++++++++++++++++++++++++ vernac/declaremods.mli | 139 ++++++ vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 15 +- 14 files changed, 1341 insertions(+), 1311 deletions(-) delete mode 100644 library/declaremods.ml delete mode 100644 library/declaremods.mli create mode 100644 vernac/declaremods.ml create mode 100644 vernac/declaremods.mli diff --git a/interp/modintern.ml b/interp/modintern.ml index 955288244e..ddf5b2d7b1 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -12,7 +12,6 @@ open Declarations open Libnames open Constrexpr open Constrintern -open Declaremods type module_internalization_error = | NotAModuleNorModtype of string @@ -21,9 +20,11 @@ type module_internalization_error = exception ModuleInternalizationError of module_internalization_error +type module_kind = Module | ModType | ModAny + let error_not_a_module_loc kind loc qid = let s = string_of_qualid qid in - let e = let open Declaremods in match kind with + let e = match kind with | Module -> Modops.ModuleTypingError (Modops.NotAModule s) | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) @@ -46,7 +47,6 @@ let error_application_to_module_type loc = it is equal to the input kind when this one isn't ModAny. *) let lookup_module_or_modtype kind qid = - let open Declaremods in let loc = qid.CAst.loc in try if kind == ModType then raise Not_found; diff --git a/interp/modintern.mli b/interp/modintern.mli index 75ab38c64a..72695a680e 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -28,5 +28,7 @@ exception ModuleInternalizationError of module_internalization_error kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) +type module_kind = Module | ModType | ModAny + val interp_module_ast : - env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t + env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t diff --git a/library/declaremods.ml b/library/declaremods.ml deleted file mode 100644 index b4dc42bdfe..0000000000 --- a/library/declaremods.ml +++ /dev/null @@ -1,1078 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* None - | InlineAt i -> Some i - | DefaultInline -> default_inline () - -(** ModSubstObjs : a cache of module substitutive objects - - This table is common to modules and module types. - - For a Module M:=N, the objects of N will be reloaded - with M after substitution. - - For a Module M:SIG:=..., the module M gets its objects from SIG - - Invariants: - - A alias (i.e. a module path inside a Ref constructor) should - never lead to another alias, but rather to a concrete Objs - constructor. - - We will plug later a handler dealing with missing entries in the - cache. Such missing entries may come from inner parts of module - types, which aren't registered by the standard libobject machinery. -*) - -module ModSubstObjs : - sig - val set : ModPath.t -> substitutive_objects -> unit - val get : ModPath.t -> substitutive_objects - val set_missing_handler : (ModPath.t -> substitutive_objects) -> unit - end = - struct - let table = - Summary.ref (MPmap.empty : substitutive_objects MPmap.t) - ~name:"MODULE-SUBSTOBJS" - let missing_handler = ref (fun mp -> assert false) - let set_missing_handler f = (missing_handler := f) - let set mp objs = (table := MPmap.add mp objs !table) - let get mp = - try MPmap.find mp !table with Not_found -> !missing_handler mp - end - -(** Some utilities about substitutive objects : - substitution, expansion *) - -let sobjs_no_functor (mbids,_) = List.is_empty mbids - -let rec subst_aobjs sub = function - | Objs o as objs -> - let o' = subst_objects sub o in - if o == o' then objs else Objs o' - | Ref (mp, sub0) as r -> - let sub0' = join sub0 sub in - if sub0' == sub0 then r else Ref (mp, sub0') - -and subst_sobjs sub (mbids,aobjs as sobjs) = - let aobjs' = subst_aobjs sub aobjs in - if aobjs' == aobjs then sobjs else (mbids, aobjs') - -and subst_objects subst seg = - let subst_one (id,obj as node) = - match obj with - | AtomicObject obj -> - let obj' = Libobject.subst_object (subst,obj) in - if obj' == obj then node else (id, AtomicObject obj') - | ModuleObject sobjs -> - let sobjs' = subst_sobjs subst sobjs in - if sobjs' == sobjs then node else (id, ModuleObject sobjs') - | ModuleTypeObject sobjs -> - let sobjs' = subst_sobjs subst sobjs in - if sobjs' == sobjs then node else (id, ModuleTypeObject sobjs') - | IncludeObject aobjs -> - let aobjs' = subst_aobjs subst aobjs in - if aobjs' == aobjs then node else (id, IncludeObject aobjs') - | ExportObject { mpl } -> - let mpl' = List.map (subst_mp subst) mpl in - if mpl'==mpl then node else (id, ExportObject { mpl = mpl' }) - | KeepObject _ -> assert false - in - List.Smart.map subst_one seg - -let expand_aobjs = function - | Objs o -> o - | Ref (mp, sub) -> - match ModSubstObjs.get mp with - | (_,Objs o) -> subst_objects sub o - | _ -> assert false (* Invariant : any alias points to concrete objs *) - -let expand_sobjs (_,aobjs) = expand_aobjs aobjs - - -(** {6 ModObjs : a cache of module objects} - - For each module, we also store a cache of - "prefix", "substituted objects", "keep objects". - This is used for instance to implement the "Import" command. - - substituted objects : - roughly the objects above after the substitution - we need to - keep them to call open_object when the module is opened (imported) - - keep objects : - The list of non-substitutive objects - as above, for each of - them we will call open_object when the module is opened - - (Some) Invariants: - * If the module is a functor, it won't appear in this cache. - - * Module objects in substitutive_objects part have empty substituted - objects. - - * Modules which where created with Module M:=mexpr or with - Module M:SIG. ... End M. have the keep list empty. -*) - -type module_objects = - { module_prefix : Nametab.object_prefix; - module_substituted_objects : Lib.lib_objects; - module_keep_objects : Lib.lib_objects; - } - -module ModObjs : - sig - val set : ModPath.t -> module_objects -> unit - val get : ModPath.t -> module_objects (* may raise Not_found *) - val all : unit -> module_objects MPmap.t - end = - struct - let table = - Summary.ref (MPmap.empty : module_objects MPmap.t) - ~name:"MODULE-OBJS" - let set mp objs = (table := MPmap.add mp objs !table) - let get mp = MPmap.find mp !table - let all () = !table - end - - -(** {6 Name management} - - Auxiliary functions to transform full_path and kernel_name given - by Lib into ModPath.t and DirPath.t needed for modules -*) - -let mp_of_kn kn = - let mp,l = KerName.repr kn in - MPdot (mp,l) - -let dir_of_sp sp = - let dir,id = repr_path sp in - add_dirpath_suffix dir id - - -(** {6 Declaration of module substitutive objects} *) - -(** These functions register the visibility of the module and iterates - through its components. They are called by plenty of module functions *) - -let consistency_checks exists dir dirinfo = - if exists then - let globref = - try Nametab.locate_dir (qualid_of_dirpath dir) - with Not_found -> - user_err ~hdr:"consistency_checks" - (DirPath.print dir ++ str " should already exist!") - in - assert (Nametab.GlobDirRef.equal globref dirinfo) - else - if Nametab.exists_dir dir then - user_err ~hdr:"consistency_checks" - (DirPath.print dir ++ str " already exists") - -let compute_visibility exists i = - if exists then Nametab.Exactly i else Nametab.Until i - -(** Iterate some function [iter_objects] on all components of a module *) - -let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs = - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in - let dirinfo = Nametab.GlobDirRef.DirModule prefix in - consistency_checks exists obj_dir dirinfo; - Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo; - ModSubstObjs.set obj_mp sobjs; - (* If we're not a functor, let's iter on the internal components *) - if sobjs_no_functor sobjs then begin - let objs = expand_sobjs sobjs in - let module_objects = - { module_prefix = prefix; - module_substituted_objects = objs; - module_keep_objects = kobjs; - } - in - ModObjs.set obj_mp module_objects; - iter_objects (i+1) prefix objs; - iter_objects (i+1) prefix kobjs - end - -let do_module' exists iter_objects i ((sp,kn),sobjs) = - do_module exists iter_objects i (dir_of_sp sp) (mp_of_kn kn) sobjs [] - -(** Nota: Interactive modules and module types cannot be recached! - This used to be checked here via a flag along the substobjs. *) - -(** {6 Declaration of module type substitutive objects} *) - -(** Nota: Interactive modules and module types cannot be recached! - This used to be checked more properly here. *) - -let load_modtype i sp mp sobjs = - if Nametab.exists_modtype sp then - anomaly (pr_path sp ++ str " already exists."); - Nametab.push_modtype (Nametab.Until i) sp mp; - ModSubstObjs.set mp sobjs - -(** {6 Declaration of substitutive objects for Include} *) - -let rec load_object i (name, obj) = - match obj with - | AtomicObject o -> Libobject.load_object i (name, o) - | ModuleObject sobjs -> do_module' false load_objects i (name, sobjs) - | ModuleTypeObject sobjs -> - let (sp,kn) = name in - load_modtype i sp (mp_of_kn kn) sobjs - | IncludeObject aobjs -> load_include i (name, aobjs) - | ExportObject _ -> () - | KeepObject objs -> load_keep i (name, objs) - -and load_objects i prefix objs = - List.iter (fun (id, obj) -> load_object i (Lib.make_oname prefix id, obj)) objs - -and load_include i ((sp,kn), aobjs) = - let obj_dir = Libnames.dirpath sp in - let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in - let o = expand_aobjs aobjs in - load_objects i prefix o - -and load_keep i ((sp,kn),kobjs) = - (* Invariant : seg isn't empty *) - let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in - let modobjs = - try ModObjs.get obj_mp - with Not_found -> assert false (* a substobjs should already be loaded *) - in - assert Nametab.(eq_op modobjs.module_prefix prefix); - assert (List.is_empty modobjs.module_keep_objects); - ModObjs.set obj_mp { modobjs with module_keep_objects = kobjs }; - load_objects i prefix kobjs - -(** {6 Implementation of Import and Export commands} *) - -let mark_object obj (exports,acc) = - (exports, obj::acc) - -let rec collect_module_objects mp acc = - (* May raise Not_found for unknown module and for functors *) - let modobjs = ModObjs.get mp in - let prefix = modobjs.module_prefix in - let acc = collect_objects 1 prefix modobjs.module_keep_objects acc in - collect_objects 1 prefix modobjs.module_substituted_objects acc - -and collect_object i (name, obj as o) acc = - match obj with - | ExportObject { mpl; _ } -> collect_export i mpl acc - | AtomicObject _ | IncludeObject _ | KeepObject _ - | ModuleObject _ | ModuleTypeObject _ -> mark_object o acc - -and collect_objects i prefix objs acc = - List.fold_right (fun (id, obj) acc -> collect_object i (Lib.make_oname prefix id, obj) acc) objs acc - -and collect_one_export mp (exports,objs as acc) = - if not (MPset.mem mp exports) then - collect_module_objects mp (MPset.add mp exports, objs) - else acc - -and collect_export i mpl acc = - if Int.equal i 1 then - List.fold_right collect_one_export mpl acc - else acc - -let rec open_object i (name, obj) = - match obj with - | AtomicObject o -> Libobject.open_object i (name, o) - | ModuleObject sobjs -> - let dir = dir_of_sp (fst name) in - let mp = mp_of_kn (snd name) in - open_module i dir mp sobjs - | ModuleTypeObject sobjs -> open_modtype i (name, sobjs) - | IncludeObject aobjs -> open_include i (name, aobjs) - | ExportObject { mpl; _ } -> open_export i mpl - | KeepObject objs -> open_keep i (name, objs) - -and open_module i obj_dir obj_mp sobjs = - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in - let dirinfo = Nametab.GlobDirRef.DirModule prefix in - consistency_checks true obj_dir dirinfo; - Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo; - (* If we're not a functor, let's iter on the internal components *) - if sobjs_no_functor sobjs then begin - let modobjs = ModObjs.get obj_mp in - open_objects (i+1) modobjs.module_prefix modobjs.module_substituted_objects - end - -and open_objects i prefix objs = - List.iter (fun (id, obj) -> open_object i (Lib.make_oname prefix id, obj)) objs - -and open_modtype i ((sp,kn),_) = - let mp = mp_of_kn kn in - let mp' = - try Nametab.locate_modtype (qualid_of_path sp) - with Not_found -> - anomaly (pr_path sp ++ str " should already exist!"); - in - assert (ModPath.equal mp mp'); - Nametab.push_modtype (Nametab.Exactly i) sp mp - -and open_include i ((sp,kn), aobjs) = - let obj_dir = Libnames.dirpath sp in - let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in - let o = expand_aobjs aobjs in - open_objects i prefix o - -and open_export i mpl = - let _,objs = collect_export i mpl (MPset.empty, []) in - List.iter (open_object 1) objs - -and open_keep i ((sp,kn),kobjs) = - let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in - open_objects i prefix kobjs - -let rec cache_object (name, obj) = - match obj with - | AtomicObject o -> Libobject.cache_object (name, o) - | ModuleObject sobjs -> do_module' false load_objects 1 (name, sobjs) - | ModuleTypeObject sobjs -> - let (sp,kn) = name in - load_modtype 0 sp (mp_of_kn kn) sobjs - | IncludeObject aobjs -> cache_include (name, aobjs) - | ExportObject { mpl } -> anomaly Pp.(str "Export should not be cached") - | KeepObject objs -> cache_keep (name, objs) - -and cache_include ((sp,kn), aobjs) = - let obj_dir = Libnames.dirpath sp in - let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in - let o = expand_aobjs aobjs in - load_objects 1 prefix o; - open_objects 1 prefix o - -and cache_keep ((sp,kn),kobjs) = - anomaly (Pp.str "This module should not be cached!") - -(* Adding operations with containers *) - -let add_leaf id obj = - if ModPath.equal (Lib.current_mp ()) ModPath.initial then - user_err Pp.(str "No session module started (use -top dir)"); - let oname = Lib.make_foname id in - cache_object (oname,obj); - Lib.add_entry oname (Lib.Leaf obj); - oname - -let add_leaves id objs = - let oname = Lib.make_foname id in - let add_obj obj = - Lib.add_entry oname (Lib.Leaf obj); - load_object 1 (oname,obj) - in - List.iter add_obj objs; - oname - -(** {6 Handler for missing entries in ModSubstObjs} *) - -(** Since the inner of Module Types are not added by default to - the ModSubstObjs table, we compensate this by explicit traversal - of Module Types inner objects when needed. Quite a hack... *) - -let mp_id mp id = MPdot (mp, Label.of_id id) - -let rec register_mod_objs mp (id,obj) = match obj with - | ModuleObject sobjs -> ModSubstObjs.set (mp_id mp id) sobjs - | ModuleTypeObject sobjs -> ModSubstObjs.set (mp_id mp id) sobjs - | IncludeObject aobjs -> - List.iter (register_mod_objs mp) (expand_aobjs aobjs) - | _ -> () - -let handle_missing_substobjs mp = match mp with - | MPdot (mp',l) -> - let objs = expand_sobjs (ModSubstObjs.get mp') in - List.iter (register_mod_objs mp') objs; - ModSubstObjs.get mp - | _ -> - assert false (* Only inner parts of module types should be missing *) - -let () = ModSubstObjs.set_missing_handler handle_missing_substobjs - - - -(** {6 From module expression to substitutive objects} *) - -(** Turn a chain of [MSEapply] into the head ModPath.t and the - list of ModPath.t parameters (deepest param coming first). - The left part of a [MSEapply] must be either [MSEident] or - another [MSEapply]. *) - -let get_applications mexpr = - let rec get params = function - | MEident mp -> mp, params - | MEapply (fexpr, mp) -> get (mp::params) fexpr - | MEwith _ -> user_err Pp.(str "Non-atomic functor application.") - in get [] mexpr - -(** Create the substitution corresponding to some functor applications *) - -let rec compute_subst env mbids sign mp_l inl = - match mbids,mp_l with - | _,[] -> mbids,empty_subst - | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") - | mbid::mbids,mp::mp_l -> - let farg_id, farg_b, fbody_b = Modops.destr_functor sign in - let mb = Environ.lookup_module mp env in - let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in - let resolver = - if Modops.is_functor mb.mod_type then empty_delta_resolver - else - Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta - in - mbid_left,join (map_mbid mbid mp resolver) subst - -(** Create the objects of a "with Module" structure. *) - -let rec replace_module_object idl mp0 objs0 mp1 objs1 = - match idl, objs0 with - | _,[] -> [] - | id::idl,(id',obj)::tail when Id.equal id id' -> - begin match obj with - | ModuleObject sobjs -> - let mp_id = MPdot(mp0, Label.of_id id) in - let objs = match idl with - | [] -> subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 - | _ -> - let objs_id = expand_sobjs sobjs in - replace_module_object idl mp_id objs_id mp1 objs1 - in - (id, ModuleObject ([], Objs objs))::tail - | _ -> assert false - end - | idl,lobj::tail -> lobj::replace_module_object idl mp0 tail mp1 objs1 - -let type_of_mod mp env = function - |true -> (Environ.lookup_module mp env).mod_type - |false -> (Environ.lookup_modtype mp env).mod_type - -let rec get_module_path = function - |MEident mp -> mp - |MEwith (me,_) -> get_module_path me - |MEapply (me,_) -> get_module_path me - -(** Substitutive objects of a module expression (or module type) *) - -let rec get_module_sobjs is_mod env inl = function - |MEident mp -> - begin match ModSubstObjs.get mp with - |(mbids,Objs _) when not (ModPath.is_bound mp) -> - (mbids,Ref (mp, empty_subst)) (* we create an alias *) - |sobjs -> sobjs - end - |MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty - |MEwith (mty, WithMod (idl,mp1)) -> - assert (not is_mod); - let sobjs0 = get_module_sobjs is_mod env inl mty in - assert (sobjs_no_functor sobjs0); - (* For now, we expanse everything, to be safe *) - let mp0 = get_module_path mty in - let objs0 = expand_sobjs sobjs0 in - let objs1 = expand_sobjs (ModSubstObjs.get mp1) in - ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1)) - |MEapply _ as me -> - let mp1, mp_l = get_applications me in - let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in - let typ = type_of_mod mp1 env is_mod in - let mbids_left,subst = compute_subst env mbids typ mp_l inl in - (mbids_left, subst_aobjs subst aobjs) - -let get_functor_sobjs is_mod env inl (params,mexpr) = - let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in - (List.map fst params @ mbids, aobjs) - - -(** {6 Handling of module parameters} *) - -(** For printing modules, [process_module_binding] adds names of - bound module (and its components) to Nametab. It also loads - objects associated to it. *) - -let process_module_binding mbid me = - let dir = DirPath.make [MBId.to_id mbid] in - let mp = MPbound mbid in - let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in - let subst = map_mp (get_module_path me) mp empty_delta_resolver in - let sobjs = subst_sobjs subst sobjs in - do_module false load_objects 1 dir mp sobjs [] - -(** Process a declaration of functor parameter(s) (Id1 .. Idn : Typ) - i.e. possibly multiple names with the same module type. - Global environment is updated on the fly. - Objects in these parameters are also loaded. - Output is accumulated on top of [acc] (in reverse order). *) - -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, _, 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 - let fold acc {CAst.v=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 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) - Global environment is updated on the fly. - The calls to [interp_modast] should be interleaved with these - env updates, otherwise some "with Definition" could be rejected. - Returns a list of mbids and entries (in reversed order). - - This used to be a [List.concat (List.map ...)], but this should - be more efficient and independent of [List.map] eval order. -*) - -let intern_args interp_modast params = - List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params - - -(** {6 Auxiliary functions concerning subtyping checks} *) - -let check_sub mtb sub_mtb_l = - (* The constraints are checked and forgot immediately : *) - ignore (List.fold_right - (fun sub_mtb env -> - Environ.add_constraints - (Subtyping.check_subtypes env mtb sub_mtb) env) - sub_mtb_l (Global.env())) - -(** This function checks if the type calculated for the module [mp] is - a subtype of all signatures in [sub_mtb_l]. Uses only the global - environment. *) - -let check_subtypes mp sub_mtb_l = - let mb = - try Global.lookup_module mp with Not_found -> assert false - in - let mtb = Modops.module_type_of_module mb in - check_sub mtb sub_mtb_l - -(** Same for module type [mp] *) - -let check_subtypes_mt mp sub_mtb_l = - let mtb = - try Global.lookup_modtype mp with Not_found -> assert false - in - check_sub mtb sub_mtb_l - -(** Create a params entry. - In [args], the youngest module param now comes first. *) - -let mk_params_entry args = - List.rev_map (fun (mbid,arg_t,_) -> (mbid,arg_t)) args - -(** Create a functor type struct. - In [args], the youngest module param now comes first. *) - -let mk_funct_type env args seb0 = - List.fold_left - (fun seb (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)) - seb0 args - -(** Prepare the module type list for check of subtypes *) - -let build_subtypes interp_modast env mp args mtys = - let (cst, ans) = List.fold_left_map - (fun cst (m,ann) -> - let inl = inl2intopt ann 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 - cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type }) - Univ.ContextSet.empty mtys - in - (ans, cst) - - -(** {6 Current module information} - - This information is stored by each [start_module] for use - in a later [end_module]. *) - -type current_module_info = { - cur_typ : (module_struct_entry * int option) option; (** type via ":" *) - cur_typs : module_type_body list (** types via "<:" *) -} - -let default_module_info = { cur_typ = None; cur_typs = [] } - -let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO" - - -(** {6 Current module type information} - - This information is stored by each [start_modtype] for use - in a later [end_modtype]. *) - -let openmodtype_info = - Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" - - -(** {6 Modules : start, end, declare} *) - -module RawModOps = struct - -let start_module interp_modast export id args res fs = - let mp = Global.start_module id 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, cst = match res with - | Enforce (res,ann) -> - let inl = inl2intopt ann 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 _, _, _, cst' = Mod_typing.translate_mse env None inl mte in - let cst = Univ.ContextSet.union cst cst' in - Some (mte, inl), [], cst - | Check 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 (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix)); - mp - -let end_module () = - let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in - let substitute, keep, special = Lib.classify_segment lib_stack in - let m_info = !openmod_info in - - (* For sealed modules, we use the substitutive objects of their signatures *) - let sobjs0, keep, special = match m_info.cur_typ with - | None -> ([], Objs substitute), keep, special - | Some (mty, inline) -> - get_module_sobjs false (Global.env()) inline mty, [], [] - in - let id = basename (fst oldoname) in - let mp,mbids,resolver = Global.end_module fs id m_info.cur_typ in - let sobjs = let (ms,objs) = sobjs0 in (mbids@ms,objs) in - - check_subtypes mp m_info.cur_typs; - - (* We substitute objects if the module is sealed by a signature *) - let sobjs = - match m_info.cur_typ with - | None -> sobjs - | Some (mty, _) -> - subst_sobjs (map_mp (get_module_path mty) mp resolver) sobjs - in - let node = ModuleObject sobjs in - (* We add the keep objects, if any, and if this isn't a functor *) - let objects = match keep, mbids with - | [], _ | _, _ :: _ -> special@[node] - | _ -> special@[node;KeepObject keep] - in - let newoname = add_leaves id objects in - - (* Name consistency check : start_ vs. end_module, kernel vs. library *) - assert (eq_full_path (fst newoname) (fst oldoname)); - assert (ModPath.equal (mp_of_kn (snd newoname)) mp); - - mp - -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, cst = intern_args interp_modast 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 - | Enforce (mty,ann) -> - let inl = inl2intopt ann 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 _, _, _, cst' = Mod_typing.translate_mse env None inl mte in - let cst = Univ.ContextSet.union cst cst' in - Some mte, [], inl, cst - | Check mtys -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in - None, typs, default_inline (), cst - 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 - | None -> None, default_inline (), Univ.ContextSet.empty - | Some (mexpr,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) - | Some body, otyp -> MExpr (params, body, otyp) - in - let sobjs, mp0 = match entry with - | MType (_,mte) | MExpr (_,_,Some mte) -> - get_functor_sobjs false env inl_res (params,mte), get_module_path mte - | MExpr (_,me,None) -> - get_functor_sobjs true env inl_expr (params,me), get_module_path me - in - (* Undo the simulated interactive building of the module - and declare the module as a whole *) - Summary.unfreeze_summaries fs; - let inl = match inl_expr with - | 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 *) - assert (ModPath.equal mp (mp_of_kn (Lib.make_kn id))); - assert (ModPath.equal mp mp_env); - - check_subtypes mp subs; - - let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in - ignore (add_leaf id (ModuleObject sobjs)); - mp - -end - -(** {6 Module types : start, end, declare} *) - -module RawModTypeOps = struct - -let start_modtype interp_modast id args mtys fs = - let mp = Global.start_modtype id 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, 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 (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix)); - mp - -let end_modtype () = - let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in - let id = basename (fst oldoname) in - let substitute, _, special = Lib.classify_segment lib_stack in - let sub_mty_l = !openmodtype_info in - let mp, mbids = Global.end_modtype fs id in - let modtypeobjs = (mbids, Objs substitute) in - check_subtypes_mt mp sub_mty_l; - let oname = add_leaves id (special@[ModuleTypeObject modtypeobjs]) - in - (* Check name consistence : start_ vs. end_modtype, kernel vs. library *) - assert (eq_full_path (fst oname) (fst oldoname)); - assert (ModPath.equal (mp_of_kn (snd oname)) mp); - - mp - -let declare_modtype interp_modast id args mtys (mty,ann) fs = - let inl = inl2intopt ann in - (* 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 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, _, 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 _, _, _, 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, 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 - - (* Undo the simulated interactive building of the module type - and declare the module type as a whole *) - Summary.unfreeze_summaries fs; - - (* We enrich the global environment *) - let mp_env = Global.add_modtype id entry inl in - - (* Name consistency check : kernel vs. library *) - assert (ModPath.equal mp_env mp); - - (* Subtyping checks *) - check_subtypes_mt mp sub_mty_l; - - ignore (add_leaf id (ModuleTypeObject sobjs)); - mp - -end - -(** {6 Include} *) - -module RawIncludeOps = struct - -let rec include_subst env mp reso mbids sign inline = match mbids with - | [] -> empty_subst - | mbid::mbids -> - let farg_id, farg_b, fbody_b = Modops.destr_functor sign in - let subst = include_subst env mp reso mbids fbody_b inline in - let mp_delta = - Modops.inline_delta_resolver env inline mp farg_id farg_b reso - in - join (map_mbid mbid mp mp_delta) subst - -let rec decompose_functor mpl typ = - match mpl, typ with - | [], _ -> typ - | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str - | _ -> user_err Pp.(str "Application of a functor with too much arguments.") - -exception NoIncludeSelf - -let type_of_incl env is_mod = function - |MEident mp -> type_of_mod mp env is_mod - |MEapply _ as me -> - let mp0, mp_l = get_applications me in - decompose_functor mp_l (type_of_mod mp0 env is_mod) - |MEwith _ -> raise NoIncludeSelf - -let declare_one_include interp_modast (me_ast,annot) = - let env = Global.env() 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 - let mbids,aobjs = get_module_sobjs is_mod env inl me in - let subst_self = - try - if List.is_empty mbids then raise NoIncludeSelf; - let typ = type_of_incl env is_mod me in - let reso,_ = Safe_typing.delta_of_senv (Global.safe_env ()) in - include_subst env cur_mp reso mbids typ inl - with NoIncludeSelf -> empty_subst - in - let base_mp = get_module_path me in - let resolver = Global.add_include me is_mod inl in - let subst = join subst_self (map_mp base_mp cur_mp resolver) in - let aobjs = subst_aobjs subst aobjs in - ignore (add_leaf (Lib.current_mod_id ()) (IncludeObject aobjs)) - -let declare_include interp me_asts = - List.iter (declare_one_include interp) me_asts - -end - - -(** {6 Module operations handling summary freeze/unfreeze} *) - -let protect_summaries f = - let fs = Summary.freeze_summaries ~marshallable:false in - try f fs - with reraise -> - (* Something wrong: undo the whole process *) - let reraise = CErrors.push reraise in - let () = Summary.unfreeze_summaries fs in - iraise reraise - -let start_module interp export id args res = - protect_summaries (RawModOps.start_module interp export id args res) - -let end_module = RawModOps.end_module - -let declare_module interp id args mtys me_l = - let declare_me fs = match me_l with - | [] -> RawModOps.declare_module interp id args mtys None fs - | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs - | me_l -> - ignore (RawModOps.start_module interp None id args mtys fs); - RawIncludeOps.declare_include interp me_l; - RawModOps.end_module () - in - protect_summaries declare_me - -let start_modtype interp id args mtys = - protect_summaries (RawModTypeOps.start_modtype interp id args mtys) - -let end_modtype = RawModTypeOps.end_modtype - -let declare_modtype interp id args mtys mty_l = - let declare_mt fs = match mty_l with - | [] -> assert false - | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs - | mty_l -> - ignore (RawModTypeOps.start_modtype interp id args mtys fs); - RawIncludeOps.declare_include interp mty_l; - RawModTypeOps.end_modtype () - in - protect_summaries declare_mt - -let declare_include interp me_asts = - protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts) - - -(** {6 Libraries} *) - -type library_name = DirPath.t - -(** A library object is made of some substitutive objects - and some "keep" objects. *) - -type library_objects = Lib.lib_objects * Lib.lib_objects - -(** For the native compiler, we cache the library values *) - -let register_library dir cenv (objs:library_objects) digest univ = - let mp = MPfile dir in - let () = - try - (* Is this library already loaded ? *) - ignore(Global.lookup_module mp); - with Not_found -> - (* If not, let's do it now ... *) - let mp' = Global.import cenv univ digest in - if not (ModPath.equal mp mp') then - anomaly (Pp.str "Unexpected disk module name."); - in - let sobjs,keepobjs = objs in - do_module false load_objects 1 dir mp ([],Objs sobjs) keepobjs - -let start_library dir = - let mp = Global.start_library dir in - openmod_info := default_module_info; - Lib.start_compilation dir mp - -let end_library_hook = ref ignore -let append_end_library_hook f = - let old_f = !end_library_hook in - end_library_hook := fun () -> old_f(); f () - -let end_library ?except ~output_native_objects dir = - !end_library_hook(); - let oname = Lib.end_compilation_checks dir in - let mp,cenv,ast = Global.export ?except ~output_native_objects dir in - let prefix, lib_stack = Lib.end_compilation oname in - assert (ModPath.equal mp (MPfile dir)); - let substitute, keep, _ = Lib.classify_segment lib_stack in - cenv,(substitute,keep),ast - -let import_modules ~export mpl = - let _,objs = List.fold_right collect_module_objects mpl (MPset.empty, []) in - List.iter (open_object 1) objs; - if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl })) - -let import_module ~export mp = - import_modules ~export [mp] - -(** {6 Iterators} *) - -let iter_all_segments f = - let rec apply_obj prefix (id,obj) = match obj with - | IncludeObject aobjs -> - let objs = expand_aobjs aobjs in - List.iter (apply_obj prefix) objs - | _ -> f (Lib.make_oname prefix id) obj - in - let apply_mod_obj _ modobjs = - let prefix = modobjs.module_prefix in - List.iter (apply_obj prefix) modobjs.module_substituted_objects; - List.iter (apply_obj prefix) modobjs.module_keep_objects - in - let apply_node = function - | sp, Lib.Leaf o -> f sp o - | _ -> () - in - MPmap.iter apply_mod_obj (ModObjs.all ()); - List.iter apply_node (Lib.contents ()) - - -(** {6 Some types used to shorten declaremods.mli} *) - -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** {6 Debug} *) - -let debug_print_modtab _ = - let pr_seg = function - | [] -> str "[]" - | l -> str "[." ++ int (List.length l) ++ str ".]" - in - let pr_modinfo mp modobjs s = - let objs = modobjs.module_substituted_objects @ modobjs.module_keep_objects in - s ++ str (ModPath.to_string mp) ++ (spc ()) - ++ (pr_seg (Lib.segment_of_objects modobjs.module_prefix objs)) - in - let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in - hov 0 modules diff --git a/library/declaremods.mli b/library/declaremods.mli deleted file mode 100644 index b7c7cd1dba..0000000000 --- a/library/declaremods.mli +++ /dev/null @@ -1,141 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** [declare_module interp_modast id fargs typ exprs] - declares module [id], with structure constructed by [interp_modast] - from functor arguments [fargs], with final type [typ]. - [exprs] is usually of length 1 (Module definition with a concrete - body), but it could also be empty ("Declare Module", with non-empty [typ]), - or multiple (body of the shape M <+ N <+ ...). *) - -val declare_module : - 'modast module_interpretor -> - Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> - ('modast * inline) list -> ModPath.t - -val start_module : - 'modast module_interpretor -> - bool option -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> ModPath.t - -val end_module : unit -> ModPath.t - - - -(** {6 Module types } *) - -(** [declare_modtype interp_modast id fargs typs exprs] - Similar to [declare_module], except that the types could be multiple *) - -val declare_modtype : - 'modast module_interpretor -> - Id.t -> - 'modast module_params -> - ('modast * inline) list -> - ('modast * inline) list -> - ModPath.t - -val start_modtype : - 'modast module_interpretor -> - Id.t -> - 'modast module_params -> - ('modast * inline) list -> ModPath.t - -val end_modtype : unit -> ModPath.t - -(** {6 Libraries i.e. modules on disk } *) - -type library_name = DirPath.t - -type library_objects - -val register_library : - library_name -> - Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> - Univ.ContextSet.t -> unit - -val start_library : library_name -> unit - -val end_library : - ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name -> - Safe_typing.compiled_library * library_objects * Safe_typing.native_library - -(** append a function to be executed at end_library *) -val append_end_library_hook : (unit -> unit) -> unit - -(** [import_module export mp] imports the module [mp]. - It modifies Nametab and performs the [open_object] function for - every object of the module. Raises [Not_found] when [mp] is unknown - or when [mp] corresponds to a functor. If [export] is [true], the module is also - opened every time the module containing it is. *) - -val import_module : export:bool -> ModPath.t -> unit - -(** Same as [import_module] but for multiple modules, and more optimized than - iterating [import_module]. *) -val import_modules : export:bool -> ModPath.t list -> unit - -(** Include *) - -val declare_include : - 'modast module_interpretor -> ('modast * inline) list -> unit - -(** {6 ... } *) -(** [iter_all_segments] iterate over all segments, the modules' - segments first and then the current segment. Modules are presented - in an arbitrary order. The given function is applied to all leaves - (together with their section path). *) - -val iter_all_segments : - (Libobject.object_name -> Libobject.t -> unit) -> unit - - -val debug_print_modtab : unit -> Pp.t - -(** For printing modules, [process_module_binding] adds names of - bound module (and its components) to Nametab. It also loads - objects associated to it. It may raise a [Failure] when the - bound module hasn't an atomic type. *) - -val process_module_binding : - MBId.t -> Declarations.module_alg_expr -> unit diff --git a/library/library.mllib b/library/library.mllib index c34d8911e8..a6188f7661 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -5,7 +5,6 @@ Summary Nametab Global Lib -Declaremods States Kindops Goptions diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fb0b1eca8d..c995887f31 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -38,11 +38,11 @@ type object_pr = { print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : bool -> ModPath.t -> Pp.t; - print_modtype : ModPath.t -> Pp.t; + print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } @@ -618,7 +618,7 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> @@ -639,17 +639,17 @@ let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as end | ModuleObject _ -> let (mp,l) = KerName.repr kn in - Some (print_module with_values (MPdot (mp,l))) + Some (print_module ~mod_ops with_values (MPdot (mp,l))) | ModuleTypeObject _ -> let (mp,l) = KerName.repr kn in - Some (print_modtype (MPdot (mp,l))) + Some (print_modtype ~mod_ops (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry indirect_accessor env sigma with_values ent = +let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry indirect_accessor env sigma with_values (oname,lobj) + gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> @@ -657,10 +657,10 @@ let gallina_print_library_entry indirect_accessor env sigma with_values ent = | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context indirect_accessor env sigma with_values = +let gallina_print_context ~mod_ops indirect_accessor env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry indirect_accessor env sigma with_values h with + (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -698,8 +698,8 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x let print_module x = !object_pr.print_module x let print_modtype x = !object_pr.print_modtype x let print_named_decl x = !object_pr.print_named_decl x -let print_library_entry x = !object_pr.print_library_entry x -let print_context x = !object_pr.print_context x +let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x +let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x let print_eval x = !object_pr.print_eval x @@ -720,10 +720,12 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context indirect_accessor env sigma = print_context indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ indirect_accessor env sigma = print_context indirect_accessor env sigma false None (Lib.contents ()) +let print_full_context ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) +let print_full_context_typ ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) -let print_full_pure_context ~library_accessor env sigma = +let print_full_pure_context ~mod_ops ~library_accessor env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with @@ -758,11 +760,11 @@ let print_full_pure_context ~library_accessor env sigma = | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _::rest -> prec rest | _ -> mt () in prec (Lib.contents ()) @@ -787,11 +789,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context indirect_accessor env sigma sec = - print_context indirect_accessor env sigma true None (read_sec_context sec) +let print_sec_context ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) -let print_sec_context_typ indirect_accessor env sigma sec = - print_context indirect_accessor env sigma false None (read_sec_context sec) +let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -801,7 +803,7 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name indirect_accessor env sigma na udecl = +let print_any_name ~mod_ops indirect_accessor env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with @@ -810,9 +812,10 @@ let print_any_name indirect_accessor env sigma na udecl = | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp | Syntactic kn -> print_syntactic_def env kn - | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp + | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> + print_module ~mod_ops (printable_body obj_dir) obj_mp | Dir _ -> mt () - | ModuleType mp -> print_modtype mp + | ModuleType mp -> print_modtype ~mod_ops mp | Other (obj, info) -> info.print obj | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) @@ -824,15 +827,15 @@ let print_any_name indirect_accessor env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name indirect_accessor env sigma na udecl = +let print_name ~mod_ops indirect_accessor env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name indirect_accessor env sigma + print_any_name ~mod_ops indirect_accessor env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name indirect_accessor env sigma (locate_any_name ref) udecl + print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl let print_opaque_name indirect_accessor env sigma qid = let open GlobRef in @@ -888,8 +891,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect indirect_accessor env sigma depth = - print_context indirect_accessor env sigma false (Some depth) (Lib.contents ()) +let inspect ~mod_ops indirect_accessor env sigma depth = + print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 4299bcc880..c8b361d95b 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -19,28 +19,35 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t val print_library_entry - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option val print_full_context - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_full_context_typ - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_full_pure_context - : library_accessor:Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> library_accessor:Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_sec_context - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_sec_context_typ - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : @@ -48,7 +55,8 @@ val print_eval : Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t val print_name - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_opaque_name @@ -69,7 +77,10 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> int -> Pp.t +val inspect + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -105,11 +116,11 @@ type object_pr = { print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : bool -> ModPath.t -> Pp.t; - print_modtype : ModPath.t -> Pp.t; + print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/printing/printmod.ml b/printing/printmod.ml index 141469ff9c..03921bca30 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -240,9 +240,14 @@ let nametab_register_body mp dir (l,body) = mip.mind_consnames) mib.mind_packets -let nametab_register_module_body mp struc = +type mod_ops = + { import_module : export:bool -> ModPath.t -> unit + ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + } + +let nametab_register_module_body ~mod_ops mp struc = (* If [mp] is a globally visible module, we simply import it *) - try Declaremods.import_module ~export:false mp + try mod_ops.import_module ~export:false mp with Not_found -> (* Otherwise we try to emulate an import by playing with nametab *) nametab_register_dir mp; @@ -252,7 +257,7 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with | Some (NoFunctor me) -> me | _ -> raise Not_found -let nametab_register_modparam mbid mtb = +let nametab_register_modparam ~mod_ops mbid mtb = let id = MBId.to_id mbid in match mtb.mod_type with | MoreFunctor _ -> id (* functorial param : nothing to register *) @@ -260,7 +265,7 @@ let nametab_register_modparam mbid mtb = (* We first try to use the algebraic type expression if any, via a Declaremods function that converts back to module entries *) try - let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in + let () = mod_ops.process_module_binding mbid (get_typ_expr_alg mtb) in id with e when CErrors.noncritical e -> (* Otherwise, we try to play with the nametab ourselves *) @@ -314,9 +319,9 @@ let print_body is_impl extent env mp (l,body) = let print_struct is_impl extent env mp struc = prlist_with_sep spc (print_body is_impl extent env mp) struc -let print_structure is_type extent env mp locals struc = +let print_structure ~mod_ops is_type extent env mp locals struc = let env' = Modops.add_structure mp struc Mod_subst.empty_delta_resolver env in - nametab_register_module_body mp struc; + nametab_register_module_body ~mod_ops mp struc; let kwd = if is_type then "Sig" else "Struct" in hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++ brk (1,-2) ++ keyword "End") @@ -362,31 +367,31 @@ let print_mod_expr env mp locals = function (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")") | MEwith _ -> assert false (* No 'with' syntax for modules *) -let rec print_functor fty fatom is_type extent env mp locals = function - | NoFunctor me -> fatom is_type extent env mp locals me +let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function + | NoFunctor me -> fatom ~mod_ops is_type extent env mp locals me | MoreFunctor (mbid,mtb1,me2) -> - let id = nametab_register_modparam mbid mtb1 in + let id = nametab_register_modparam ~mod_ops mbid mtb1 in let mp1 = MPbound mbid in - let pr_mtb1 = fty extent env mp1 locals mtb1 in + let pr_mtb1 = fty ~mod_ops extent env mp1 locals mtb1 in let env' = Modops.add_module_type mp1 mtb1 env in let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ - spc() ++ print_functor fty fatom is_type extent env' mp locals' me2) + spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2) -let rec print_expression x = - print_functor +let rec print_expression ~mod_ops x = + print_functor ~mod_ops print_modtype - (function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x + (fun ~mod_ops -> function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x -and print_signature x = - print_functor print_modtype print_structure x +and print_signature ~mod_ops x = + print_functor ~mod_ops print_modtype print_structure x -and print_modtype extent env mp locals mtb = match mtb.mod_type_alg with - | Some me -> print_expression true extent env mp locals me - | None -> print_signature true extent env mp locals mtb.mod_type +and print_modtype ~mod_ops extent env mp locals mtb = match mtb.mod_type_alg with + | Some me -> print_expression ~mod_ops true extent env mp locals me + | None -> print_signature ~mod_ops true extent env mp locals mtb.mod_type let rec printable_body dir = let dir = pop_dirpath dir in @@ -403,52 +408,52 @@ let rec printable_body dir = (** Since we might play with nametab above, we should reset to prior state after the printing *) -let print_expression' is_type extent env mp me = +let print_expression' ~mod_ops is_type extent env mp me = States.with_state_protection - (fun e -> print_expression is_type extent env mp [] e) me + (fun e -> print_expression ~mod_ops is_type extent env mp [] e) me -let print_signature' is_type extent env mp me = +let print_signature' ~mod_ops is_type extent env mp me = States.with_state_protection - (fun e -> print_signature is_type extent env mp [] e) me + (fun e -> print_signature ~mod_ops is_type extent env mp [] e) me -let unsafe_print_module extent env mp with_body mb = +let unsafe_print_module ~mod_ops extent env mp with_body mb = let name = print_modpath [] mp in let pr_equals = spc () ++ str ":= " in let body = match with_body, mb.mod_expr with | false, _ | true, Abstract -> mt() - | _, Algebraic me -> pr_equals ++ print_expression' false extent env mp me - | _, Struct sign -> pr_equals ++ print_signature' false extent env mp sign - | _, FullStruct -> pr_equals ++ print_signature' false extent env mp mb.mod_type + | _, Algebraic me -> pr_equals ++ print_expression' ~mod_ops false extent env mp me + | _, Struct sign -> pr_equals ++ print_signature' ~mod_ops false extent env mp sign + | _, FullStruct -> pr_equals ++ print_signature' ~mod_ops false extent env mp mb.mod_type in let modtype = match mb.mod_expr, mb.mod_type_alg with | FullStruct, _ -> mt () - | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true extent env mp ty - | _, _ -> brk (1,1) ++ str": " ++ print_signature' true extent env mp mb.mod_type + | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' ~mod_ops true extent env mp ty + | _, _ -> brk (1,1) ++ str": " ++ print_signature' ~mod_ops true extent env mp mb.mod_type in hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body) exception ShortPrinting -let print_module with_body mp = +let print_module ~mod_ops with_body mp = let me = Global.lookup_module mp in try if !short then raise ShortPrinting; - unsafe_print_module WithContents + unsafe_print_module ~mod_ops WithContents (Global.env ()) mp with_body me ++ fnl () with e when CErrors.noncritical e -> - unsafe_print_module OnlyNames + unsafe_print_module ~mod_ops OnlyNames (Global.env ()) mp with_body me ++ fnl () -let print_modtype kn = +let print_modtype ~mod_ops kn = let mtb = Global.lookup_modtype kn in let name = print_kn [] kn in hv 1 (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++ try if !short then raise ShortPrinting; - print_signature' true WithContents + print_signature' ~mod_ops true WithContents (Global.env ()) kn mtb.mod_type with e when CErrors.noncritical e -> - print_signature' true OnlyNames + print_signature' ~mod_ops true OnlyNames (Global.env ()) kn mtb.mod_type) diff --git a/printing/printmod.mli b/printing/printmod.mli index 8fd1cb4183..4c9245ee27 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -16,5 +16,11 @@ val printable_body : DirPath.t -> bool val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> UnivNames.univ_name_list option -> Pp.t -val print_module : bool -> ModPath.t -> Pp.t -val print_modtype : ModPath.t -> Pp.t + +type mod_ops = + { import_module : export:bool -> ModPath.t -> unit + ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + } + +val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t +val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 7658ad68a5..642dc94ab2 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -54,7 +54,10 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in let library_accessor = Library.indirect_accessor in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~library_accessor env) sigma) ++ fnl ()) + let mod_ops = { Printmod.import_module = Declaremods.import_module + ; process_module_binding = Declaremods.process_module_binding + } in + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~mod_ops ~library_accessor env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml new file mode 100644 index 0000000000..9f2e30b7a6 --- /dev/null +++ b/vernac/declaremods.ml @@ -0,0 +1,1077 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* None + | InlineAt i -> Some i + | DefaultInline -> default_inline () + +(** ModSubstObjs : a cache of module substitutive objects + + This table is common to modules and module types. + - For a Module M:=N, the objects of N will be reloaded + with M after substitution. + - For a Module M:SIG:=..., the module M gets its objects from SIG + + Invariants: + - A alias (i.e. a module path inside a Ref constructor) should + never lead to another alias, but rather to a concrete Objs + constructor. + + We will plug later a handler dealing with missing entries in the + cache. Such missing entries may come from inner parts of module + types, which aren't registered by the standard libobject machinery. +*) + +module ModSubstObjs : + sig + val set : ModPath.t -> substitutive_objects -> unit + val get : ModPath.t -> substitutive_objects + val set_missing_handler : (ModPath.t -> substitutive_objects) -> unit + end = + struct + let table = + Summary.ref (MPmap.empty : substitutive_objects MPmap.t) + ~name:"MODULE-SUBSTOBJS" + let missing_handler = ref (fun mp -> assert false) + let set_missing_handler f = (missing_handler := f) + let set mp objs = (table := MPmap.add mp objs !table) + let get mp = + try MPmap.find mp !table with Not_found -> !missing_handler mp + end + +(** Some utilities about substitutive objects : + substitution, expansion *) + +let sobjs_no_functor (mbids,_) = List.is_empty mbids + +let rec subst_aobjs sub = function + | Objs o as objs -> + let o' = subst_objects sub o in + if o == o' then objs else Objs o' + | Ref (mp, sub0) as r -> + let sub0' = join sub0 sub in + if sub0' == sub0 then r else Ref (mp, sub0') + +and subst_sobjs sub (mbids,aobjs as sobjs) = + let aobjs' = subst_aobjs sub aobjs in + if aobjs' == aobjs then sobjs else (mbids, aobjs') + +and subst_objects subst seg = + let subst_one (id,obj as node) = + match obj with + | AtomicObject obj -> + let obj' = Libobject.subst_object (subst,obj) in + if obj' == obj then node else (id, AtomicObject obj') + | ModuleObject sobjs -> + let sobjs' = subst_sobjs subst sobjs in + if sobjs' == sobjs then node else (id, ModuleObject sobjs') + | ModuleTypeObject sobjs -> + let sobjs' = subst_sobjs subst sobjs in + if sobjs' == sobjs then node else (id, ModuleTypeObject sobjs') + | IncludeObject aobjs -> + let aobjs' = subst_aobjs subst aobjs in + if aobjs' == aobjs then node else (id, IncludeObject aobjs') + | ExportObject { mpl } -> + let mpl' = List.map (subst_mp subst) mpl in + if mpl'==mpl then node else (id, ExportObject { mpl = mpl' }) + | KeepObject _ -> assert false + in + List.Smart.map subst_one seg + +let expand_aobjs = function + | Objs o -> o + | Ref (mp, sub) -> + match ModSubstObjs.get mp with + | (_,Objs o) -> subst_objects sub o + | _ -> assert false (* Invariant : any alias points to concrete objs *) + +let expand_sobjs (_,aobjs) = expand_aobjs aobjs + + +(** {6 ModObjs : a cache of module objects} + + For each module, we also store a cache of + "prefix", "substituted objects", "keep objects". + This is used for instance to implement the "Import" command. + + substituted objects : + roughly the objects above after the substitution - we need to + keep them to call open_object when the module is opened (imported) + + keep objects : + The list of non-substitutive objects - as above, for each of + them we will call open_object when the module is opened + + (Some) Invariants: + * If the module is a functor, it won't appear in this cache. + + * Module objects in substitutive_objects part have empty substituted + objects. + + * Modules which where created with Module M:=mexpr or with + Module M:SIG. ... End M. have the keep list empty. +*) + +type module_objects = + { module_prefix : Nametab.object_prefix; + module_substituted_objects : Lib.lib_objects; + module_keep_objects : Lib.lib_objects; + } + +module ModObjs : + sig + val set : ModPath.t -> module_objects -> unit + val get : ModPath.t -> module_objects (* may raise Not_found *) + val all : unit -> module_objects MPmap.t + end = + struct + let table = + Summary.ref (MPmap.empty : module_objects MPmap.t) + ~name:"MODULE-OBJS" + let set mp objs = (table := MPmap.add mp objs !table) + let get mp = MPmap.find mp !table + let all () = !table + end + + +(** {6 Name management} + + Auxiliary functions to transform full_path and kernel_name given + by Lib into ModPath.t and DirPath.t needed for modules +*) + +let mp_of_kn kn = + let mp,l = KerName.repr kn in + MPdot (mp,l) + +let dir_of_sp sp = + let dir,id = repr_path sp in + add_dirpath_suffix dir id + + +(** {6 Declaration of module substitutive objects} *) + +(** These functions register the visibility of the module and iterates + through its components. They are called by plenty of module functions *) + +let consistency_checks exists dir dirinfo = + if exists then + let globref = + try Nametab.locate_dir (qualid_of_dirpath dir) + with Not_found -> + user_err ~hdr:"consistency_checks" + (DirPath.print dir ++ str " should already exist!") + in + assert (Nametab.GlobDirRef.equal globref dirinfo) + else + if Nametab.exists_dir dir then + user_err ~hdr:"consistency_checks" + (DirPath.print dir ++ str " already exists") + +let compute_visibility exists i = + if exists then Nametab.Exactly i else Nametab.Until i + +(** Iterate some function [iter_objects] on all components of a module *) + +let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs = + let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let dirinfo = Nametab.GlobDirRef.DirModule prefix in + consistency_checks exists obj_dir dirinfo; + Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo; + ModSubstObjs.set obj_mp sobjs; + (* If we're not a functor, let's iter on the internal components *) + if sobjs_no_functor sobjs then begin + let objs = expand_sobjs sobjs in + let module_objects = + { module_prefix = prefix; + module_substituted_objects = objs; + module_keep_objects = kobjs; + } + in + ModObjs.set obj_mp module_objects; + iter_objects (i+1) prefix objs; + iter_objects (i+1) prefix kobjs + end + +let do_module' exists iter_objects i ((sp,kn),sobjs) = + do_module exists iter_objects i (dir_of_sp sp) (mp_of_kn kn) sobjs [] + +(** Nota: Interactive modules and module types cannot be recached! + This used to be checked here via a flag along the substobjs. *) + +(** {6 Declaration of module type substitutive objects} *) + +(** Nota: Interactive modules and module types cannot be recached! + This used to be checked more properly here. *) + +let load_modtype i sp mp sobjs = + if Nametab.exists_modtype sp then + anomaly (pr_path sp ++ str " already exists."); + Nametab.push_modtype (Nametab.Until i) sp mp; + ModSubstObjs.set mp sobjs + +(** {6 Declaration of substitutive objects for Include} *) + +let rec load_object i (name, obj) = + match obj with + | AtomicObject o -> Libobject.load_object i (name, o) + | ModuleObject sobjs -> do_module' false load_objects i (name, sobjs) + | ModuleTypeObject sobjs -> + let (sp,kn) = name in + load_modtype i sp (mp_of_kn kn) sobjs + | IncludeObject aobjs -> load_include i (name, aobjs) + | ExportObject _ -> () + | KeepObject objs -> load_keep i (name, objs) + +and load_objects i prefix objs = + List.iter (fun (id, obj) -> load_object i (Lib.make_oname prefix id, obj)) objs + +and load_include i ((sp,kn), aobjs) = + let obj_dir = Libnames.dirpath sp in + let obj_mp = KerName.modpath kn in + let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let o = expand_aobjs aobjs in + load_objects i prefix o + +and load_keep i ((sp,kn),kobjs) = + (* Invariant : seg isn't empty *) + let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in + let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let modobjs = + try ModObjs.get obj_mp + with Not_found -> assert false (* a substobjs should already be loaded *) + in + assert Nametab.(eq_op modobjs.module_prefix prefix); + assert (List.is_empty modobjs.module_keep_objects); + ModObjs.set obj_mp { modobjs with module_keep_objects = kobjs }; + load_objects i prefix kobjs + +(** {6 Implementation of Import and Export commands} *) + +let mark_object obj (exports,acc) = + (exports, obj::acc) + +let rec collect_module_objects mp acc = + (* May raise Not_found for unknown module and for functors *) + let modobjs = ModObjs.get mp in + let prefix = modobjs.module_prefix in + let acc = collect_objects 1 prefix modobjs.module_keep_objects acc in + collect_objects 1 prefix modobjs.module_substituted_objects acc + +and collect_object i (name, obj as o) acc = + match obj with + | ExportObject { mpl; _ } -> collect_export i mpl acc + | AtomicObject _ | IncludeObject _ | KeepObject _ + | ModuleObject _ | ModuleTypeObject _ -> mark_object o acc + +and collect_objects i prefix objs acc = + List.fold_right (fun (id, obj) acc -> collect_object i (Lib.make_oname prefix id, obj) acc) objs acc + +and collect_one_export mp (exports,objs as acc) = + if not (MPset.mem mp exports) then + collect_module_objects mp (MPset.add mp exports, objs) + else acc + +and collect_export i mpl acc = + if Int.equal i 1 then + List.fold_right collect_one_export mpl acc + else acc + +let rec open_object i (name, obj) = + match obj with + | AtomicObject o -> Libobject.open_object i (name, o) + | ModuleObject sobjs -> + let dir = dir_of_sp (fst name) in + let mp = mp_of_kn (snd name) in + open_module i dir mp sobjs + | ModuleTypeObject sobjs -> open_modtype i (name, sobjs) + | IncludeObject aobjs -> open_include i (name, aobjs) + | ExportObject { mpl; _ } -> open_export i mpl + | KeepObject objs -> open_keep i (name, objs) + +and open_module i obj_dir obj_mp sobjs = + let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let dirinfo = Nametab.GlobDirRef.DirModule prefix in + consistency_checks true obj_dir dirinfo; + Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo; + (* If we're not a functor, let's iter on the internal components *) + if sobjs_no_functor sobjs then begin + let modobjs = ModObjs.get obj_mp in + open_objects (i+1) modobjs.module_prefix modobjs.module_substituted_objects + end + +and open_objects i prefix objs = + List.iter (fun (id, obj) -> open_object i (Lib.make_oname prefix id, obj)) objs + +and open_modtype i ((sp,kn),_) = + let mp = mp_of_kn kn in + let mp' = + try Nametab.locate_modtype (qualid_of_path sp) + with Not_found -> + anomaly (pr_path sp ++ str " should already exist!"); + in + assert (ModPath.equal mp mp'); + Nametab.push_modtype (Nametab.Exactly i) sp mp + +and open_include i ((sp,kn), aobjs) = + let obj_dir = Libnames.dirpath sp in + let obj_mp = KerName.modpath kn in + let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let o = expand_aobjs aobjs in + open_objects i prefix o + +and open_export i mpl = + let _,objs = collect_export i mpl (MPset.empty, []) in + List.iter (open_object 1) objs + +and open_keep i ((sp,kn),kobjs) = + let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in + let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + open_objects i prefix kobjs + +let rec cache_object (name, obj) = + match obj with + | AtomicObject o -> Libobject.cache_object (name, o) + | ModuleObject sobjs -> do_module' false load_objects 1 (name, sobjs) + | ModuleTypeObject sobjs -> + let (sp,kn) = name in + load_modtype 0 sp (mp_of_kn kn) sobjs + | IncludeObject aobjs -> cache_include (name, aobjs) + | ExportObject { mpl } -> anomaly Pp.(str "Export should not be cached") + | KeepObject objs -> cache_keep (name, objs) + +and cache_include ((sp,kn), aobjs) = + let obj_dir = Libnames.dirpath sp in + let obj_mp = KerName.modpath kn in + let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let o = expand_aobjs aobjs in + load_objects 1 prefix o; + open_objects 1 prefix o + +and cache_keep ((sp,kn),kobjs) = + anomaly (Pp.str "This module should not be cached!") + +(* Adding operations with containers *) + +let add_leaf id obj = + if ModPath.equal (Lib.current_mp ()) ModPath.initial then + user_err Pp.(str "No session module started (use -top dir)"); + let oname = Lib.make_foname id in + cache_object (oname,obj); + Lib.add_entry oname (Lib.Leaf obj); + oname + +let add_leaves id objs = + let oname = Lib.make_foname id in + let add_obj obj = + Lib.add_entry oname (Lib.Leaf obj); + load_object 1 (oname,obj) + in + List.iter add_obj objs; + oname + +(** {6 Handler for missing entries in ModSubstObjs} *) + +(** Since the inner of Module Types are not added by default to + the ModSubstObjs table, we compensate this by explicit traversal + of Module Types inner objects when needed. Quite a hack... *) + +let mp_id mp id = MPdot (mp, Label.of_id id) + +let rec register_mod_objs mp (id,obj) = match obj with + | ModuleObject sobjs -> ModSubstObjs.set (mp_id mp id) sobjs + | ModuleTypeObject sobjs -> ModSubstObjs.set (mp_id mp id) sobjs + | IncludeObject aobjs -> + List.iter (register_mod_objs mp) (expand_aobjs aobjs) + | _ -> () + +let handle_missing_substobjs mp = match mp with + | MPdot (mp',l) -> + let objs = expand_sobjs (ModSubstObjs.get mp') in + List.iter (register_mod_objs mp') objs; + ModSubstObjs.get mp + | _ -> + assert false (* Only inner parts of module types should be missing *) + +let () = ModSubstObjs.set_missing_handler handle_missing_substobjs + + + +(** {6 From module expression to substitutive objects} *) + +(** Turn a chain of [MSEapply] into the head ModPath.t and the + list of ModPath.t parameters (deepest param coming first). + The left part of a [MSEapply] must be either [MSEident] or + another [MSEapply]. *) + +let get_applications mexpr = + let rec get params = function + | MEident mp -> mp, params + | MEapply (fexpr, mp) -> get (mp::params) fexpr + | MEwith _ -> user_err Pp.(str "Non-atomic functor application.") + in get [] mexpr + +(** Create the substitution corresponding to some functor applications *) + +let rec compute_subst env mbids sign mp_l inl = + match mbids,mp_l with + | _,[] -> mbids,empty_subst + | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") + | mbid::mbids,mp::mp_l -> + let farg_id, farg_b, fbody_b = Modops.destr_functor sign in + let mb = Environ.lookup_module mp env in + let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in + let resolver = + if Modops.is_functor mb.mod_type then empty_delta_resolver + else + Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta + in + mbid_left,join (map_mbid mbid mp resolver) subst + +(** Create the objects of a "with Module" structure. *) + +let rec replace_module_object idl mp0 objs0 mp1 objs1 = + match idl, objs0 with + | _,[] -> [] + | id::idl,(id',obj)::tail when Id.equal id id' -> + begin match obj with + | ModuleObject sobjs -> + let mp_id = MPdot(mp0, Label.of_id id) in + let objs = match idl with + | [] -> subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 + | _ -> + let objs_id = expand_sobjs sobjs in + replace_module_object idl mp_id objs_id mp1 objs1 + in + (id, ModuleObject ([], Objs objs))::tail + | _ -> assert false + end + | idl,lobj::tail -> lobj::replace_module_object idl mp0 tail mp1 objs1 + +let type_of_mod mp env = function + |true -> (Environ.lookup_module mp env).mod_type + |false -> (Environ.lookup_modtype mp env).mod_type + +let rec get_module_path = function + |MEident mp -> mp + |MEwith (me,_) -> get_module_path me + |MEapply (me,_) -> get_module_path me + +(** Substitutive objects of a module expression (or module type) *) + +let rec get_module_sobjs is_mod env inl = function + |MEident mp -> + begin match ModSubstObjs.get mp with + |(mbids,Objs _) when not (ModPath.is_bound mp) -> + (mbids,Ref (mp, empty_subst)) (* we create an alias *) + |sobjs -> sobjs + end + |MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty + |MEwith (mty, WithMod (idl,mp1)) -> + assert (not is_mod); + let sobjs0 = get_module_sobjs is_mod env inl mty in + assert (sobjs_no_functor sobjs0); + (* For now, we expanse everything, to be safe *) + let mp0 = get_module_path mty in + let objs0 = expand_sobjs sobjs0 in + let objs1 = expand_sobjs (ModSubstObjs.get mp1) in + ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1)) + |MEapply _ as me -> + let mp1, mp_l = get_applications me in + let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in + let typ = type_of_mod mp1 env is_mod in + let mbids_left,subst = compute_subst env mbids typ mp_l inl in + (mbids_left, subst_aobjs subst aobjs) + +let get_functor_sobjs is_mod env inl (params,mexpr) = + let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in + (List.map fst params @ mbids, aobjs) + + +(** {6 Handling of module parameters} *) + +(** For printing modules, [process_module_binding] adds names of + bound module (and its components) to Nametab. It also loads + objects associated to it. *) + +let process_module_binding mbid me = + let dir = DirPath.make [MBId.to_id mbid] in + let mp = MPbound mbid in + let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in + let subst = map_mp (get_module_path me) mp empty_delta_resolver in + let sobjs = subst_sobjs subst sobjs in + do_module false load_objects 1 dir mp sobjs [] + +(** Process a declaration of functor parameter(s) (Id1 .. Idn : Typ) + i.e. possibly multiple names with the same module type. + Global environment is updated on the fly. + Objects in these parameters are also loaded. + Output is accumulated on top of [acc] (in reverse order). *) + +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, _, 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 + let fold acc {CAst.v=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 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) + Global environment is updated on the fly. + The calls to [interp_modast] should be interleaved with these + env updates, otherwise some "with Definition" could be rejected. + Returns a list of mbids and entries (in reversed order). + + This used to be a [List.concat (List.map ...)], but this should + be more efficient and independent of [List.map] eval order. +*) + +let intern_args interp_modast params = + List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params + + +(** {6 Auxiliary functions concerning subtyping checks} *) + +let check_sub mtb sub_mtb_l = + (* The constraints are checked and forgot immediately : *) + ignore (List.fold_right + (fun sub_mtb env -> + Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) env) + sub_mtb_l (Global.env())) + +(** This function checks if the type calculated for the module [mp] is + a subtype of all signatures in [sub_mtb_l]. Uses only the global + environment. *) + +let check_subtypes mp sub_mtb_l = + let mb = + try Global.lookup_module mp with Not_found -> assert false + in + let mtb = Modops.module_type_of_module mb in + check_sub mtb sub_mtb_l + +(** Same for module type [mp] *) + +let check_subtypes_mt mp sub_mtb_l = + let mtb = + try Global.lookup_modtype mp with Not_found -> assert false + in + check_sub mtb sub_mtb_l + +(** Create a params entry. + In [args], the youngest module param now comes first. *) + +let mk_params_entry args = + List.rev_map (fun (mbid,arg_t,_) -> (mbid,arg_t)) args + +(** Create a functor type struct. + In [args], the youngest module param now comes first. *) + +let mk_funct_type env args seb0 = + List.fold_left + (fun seb (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)) + seb0 args + +(** Prepare the module type list for check of subtypes *) + +let build_subtypes interp_modast env mp args mtys = + let (cst, ans) = List.fold_left_map + (fun cst (m,ann) -> + let inl = inl2intopt ann 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 + cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type }) + Univ.ContextSet.empty mtys + in + (ans, cst) + + +(** {6 Current module information} + + This information is stored by each [start_module] for use + in a later [end_module]. *) + +type current_module_info = { + cur_typ : (module_struct_entry * int option) option; (** type via ":" *) + cur_typs : module_type_body list (** types via "<:" *) +} + +let default_module_info = { cur_typ = None; cur_typs = [] } + +let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO" + + +(** {6 Current module type information} + + This information is stored by each [start_modtype] for use + in a later [end_modtype]. *) + +let openmodtype_info = + Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" + + +(** {6 Modules : start, end, declare} *) + +module RawModOps = struct + +let start_module interp_modast export id args res fs = + let mp = Global.start_module id 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, cst = match res with + | Enforce (res,ann) -> + let inl = inl2intopt ann 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 _, _, _, cst' = Mod_typing.translate_mse env None inl mte in + let cst = Univ.ContextSet.union cst cst' in + Some (mte, inl), [], cst + | Check 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 (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix)); + mp + +let end_module () = + let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in + let substitute, keep, special = Lib.classify_segment lib_stack in + let m_info = !openmod_info in + + (* For sealed modules, we use the substitutive objects of their signatures *) + let sobjs0, keep, special = match m_info.cur_typ with + | None -> ([], Objs substitute), keep, special + | Some (mty, inline) -> + get_module_sobjs false (Global.env()) inline mty, [], [] + in + let id = basename (fst oldoname) in + let mp,mbids,resolver = Global.end_module fs id m_info.cur_typ in + let sobjs = let (ms,objs) = sobjs0 in (mbids@ms,objs) in + + check_subtypes mp m_info.cur_typs; + + (* We substitute objects if the module is sealed by a signature *) + let sobjs = + match m_info.cur_typ with + | None -> sobjs + | Some (mty, _) -> + subst_sobjs (map_mp (get_module_path mty) mp resolver) sobjs + in + let node = ModuleObject sobjs in + (* We add the keep objects, if any, and if this isn't a functor *) + let objects = match keep, mbids with + | [], _ | _, _ :: _ -> special@[node] + | _ -> special@[node;KeepObject keep] + in + let newoname = add_leaves id objects in + + (* Name consistency check : start_ vs. end_module, kernel vs. library *) + assert (eq_full_path (fst newoname) (fst oldoname)); + assert (ModPath.equal (mp_of_kn (snd newoname)) mp); + + mp + +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, cst = intern_args interp_modast 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 + | Enforce (mty,ann) -> + let inl = inl2intopt ann 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 _, _, _, cst' = Mod_typing.translate_mse env None inl mte in + let cst = Univ.ContextSet.union cst cst' in + Some mte, [], inl, cst + | Check mtys -> + let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + None, typs, default_inline (), cst + 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 + | None -> None, default_inline (), Univ.ContextSet.empty + | Some (mexpr,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) + | Some body, otyp -> MExpr (params, body, otyp) + in + let sobjs, mp0 = match entry with + | MType (_,mte) | MExpr (_,_,Some mte) -> + get_functor_sobjs false env inl_res (params,mte), get_module_path mte + | MExpr (_,me,None) -> + get_functor_sobjs true env inl_expr (params,me), get_module_path me + in + (* Undo the simulated interactive building of the module + and declare the module as a whole *) + Summary.unfreeze_summaries fs; + let inl = match inl_expr with + | 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 *) + assert (ModPath.equal mp (mp_of_kn (Lib.make_kn id))); + assert (ModPath.equal mp mp_env); + + check_subtypes mp subs; + + let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in + ignore (add_leaf id (ModuleObject sobjs)); + mp + +end + +(** {6 Module types : start, end, declare} *) + +module RawModTypeOps = struct + +let start_modtype interp_modast id args mtys fs = + let mp = Global.start_modtype id 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, 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 (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix)); + mp + +let end_modtype () = + let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in + let id = basename (fst oldoname) in + let substitute, _, special = Lib.classify_segment lib_stack in + let sub_mty_l = !openmodtype_info in + let mp, mbids = Global.end_modtype fs id in + let modtypeobjs = (mbids, Objs substitute) in + check_subtypes_mt mp sub_mty_l; + let oname = add_leaves id (special@[ModuleTypeObject modtypeobjs]) + in + (* Check name consistence : start_ vs. end_modtype, kernel vs. library *) + assert (eq_full_path (fst oname) (fst oldoname)); + assert (ModPath.equal (mp_of_kn (snd oname)) mp); + + mp + +let declare_modtype interp_modast id args mtys (mty,ann) fs = + let inl = inl2intopt ann in + (* 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 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, _, 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 _, _, _, 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, 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 + + (* Undo the simulated interactive building of the module type + and declare the module type as a whole *) + Summary.unfreeze_summaries fs; + + (* We enrich the global environment *) + let mp_env = Global.add_modtype id entry inl in + + (* Name consistency check : kernel vs. library *) + assert (ModPath.equal mp_env mp); + + (* Subtyping checks *) + check_subtypes_mt mp sub_mty_l; + + ignore (add_leaf id (ModuleTypeObject sobjs)); + mp + +end + +(** {6 Include} *) + +module RawIncludeOps = struct + +let rec include_subst env mp reso mbids sign inline = match mbids with + | [] -> empty_subst + | mbid::mbids -> + let farg_id, farg_b, fbody_b = Modops.destr_functor sign in + let subst = include_subst env mp reso mbids fbody_b inline in + let mp_delta = + Modops.inline_delta_resolver env inline mp farg_id farg_b reso + in + join (map_mbid mbid mp mp_delta) subst + +let rec decompose_functor mpl typ = + match mpl, typ with + | [], _ -> typ + | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str + | _ -> user_err Pp.(str "Application of a functor with too much arguments.") + +exception NoIncludeSelf + +let type_of_incl env is_mod = function + |MEident mp -> type_of_mod mp env is_mod + |MEapply _ as me -> + let mp0, mp_l = get_applications me in + decompose_functor mp_l (type_of_mod mp0 env is_mod) + |MEwith _ -> raise NoIncludeSelf + +let declare_one_include interp_modast (me_ast,annot) = + let env = Global.env() 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 + let mbids,aobjs = get_module_sobjs is_mod env inl me in + let subst_self = + try + if List.is_empty mbids then raise NoIncludeSelf; + let typ = type_of_incl env is_mod me in + let reso,_ = Safe_typing.delta_of_senv (Global.safe_env ()) in + include_subst env cur_mp reso mbids typ inl + with NoIncludeSelf -> empty_subst + in + let base_mp = get_module_path me in + let resolver = Global.add_include me is_mod inl in + let subst = join subst_self (map_mp base_mp cur_mp resolver) in + let aobjs = subst_aobjs subst aobjs in + ignore (add_leaf (Lib.current_mod_id ()) (IncludeObject aobjs)) + +let declare_include interp me_asts = + List.iter (declare_one_include interp) me_asts + +end + + +(** {6 Module operations handling summary freeze/unfreeze} *) + +let protect_summaries f = + let fs = Summary.freeze_summaries ~marshallable:false in + try f fs + with reraise -> + (* Something wrong: undo the whole process *) + let reraise = CErrors.push reraise in + let () = Summary.unfreeze_summaries fs in + iraise reraise + +let start_module interp export id args res = + protect_summaries (RawModOps.start_module interp export id args res) + +let end_module = RawModOps.end_module + +let declare_module interp id args mtys me_l = + let declare_me fs = match me_l with + | [] -> RawModOps.declare_module interp id args mtys None fs + | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs + | me_l -> + ignore (RawModOps.start_module interp None id args mtys fs); + RawIncludeOps.declare_include interp me_l; + RawModOps.end_module () + in + protect_summaries declare_me + +let start_modtype interp id args mtys = + protect_summaries (RawModTypeOps.start_modtype interp id args mtys) + +let end_modtype = RawModTypeOps.end_modtype + +let declare_modtype interp id args mtys mty_l = + let declare_mt fs = match mty_l with + | [] -> assert false + | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs + | mty_l -> + ignore (RawModTypeOps.start_modtype interp id args mtys fs); + RawIncludeOps.declare_include interp mty_l; + RawModTypeOps.end_modtype () + in + protect_summaries declare_mt + +let declare_include interp me_asts = + protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts) + + +(** {6 Libraries} *) + +type library_name = DirPath.t + +(** A library object is made of some substitutive objects + and some "keep" objects. *) + +type library_objects = Lib.lib_objects * Lib.lib_objects + +(** For the native compiler, we cache the library values *) + +let register_library dir cenv (objs:library_objects) digest univ = + let mp = MPfile dir in + let () = + try + (* Is this library already loaded ? *) + ignore(Global.lookup_module mp); + with Not_found -> + (* If not, let's do it now ... *) + let mp' = Global.import cenv univ digest in + if not (ModPath.equal mp mp') then + anomaly (Pp.str "Unexpected disk module name."); + in + let sobjs,keepobjs = objs in + do_module false load_objects 1 dir mp ([],Objs sobjs) keepobjs + +let start_library dir = + let mp = Global.start_library dir in + openmod_info := default_module_info; + Lib.start_compilation dir mp + +let end_library_hook = ref ignore +let append_end_library_hook f = + let old_f = !end_library_hook in + end_library_hook := fun () -> old_f(); f () + +let end_library ?except ~output_native_objects dir = + !end_library_hook(); + let oname = Lib.end_compilation_checks dir in + let mp,cenv,ast = Global.export ?except ~output_native_objects dir in + let prefix, lib_stack = Lib.end_compilation oname in + assert (ModPath.equal mp (MPfile dir)); + let substitute, keep, _ = Lib.classify_segment lib_stack in + cenv,(substitute,keep),ast + +let import_modules ~export mpl = + let _,objs = List.fold_right collect_module_objects mpl (MPset.empty, []) in + List.iter (open_object 1) objs; + if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl })) + +let import_module ~export mp = + import_modules ~export [mp] + +(** {6 Iterators} *) + +let iter_all_segments f = + let rec apply_obj prefix (id,obj) = match obj with + | IncludeObject aobjs -> + let objs = expand_aobjs aobjs in + List.iter (apply_obj prefix) objs + | _ -> f (Lib.make_oname prefix id) obj + in + let apply_mod_obj _ modobjs = + let prefix = modobjs.module_prefix in + List.iter (apply_obj prefix) modobjs.module_substituted_objects; + List.iter (apply_obj prefix) modobjs.module_keep_objects + in + let apply_node = function + | sp, Lib.Leaf o -> f sp o + | _ -> () + in + MPmap.iter apply_mod_obj (ModObjs.all ()); + List.iter apply_node (Lib.contents ()) + + +(** {6 Some types used to shorten declaremods.mli} *) + +type 'modast module_interpretor = + Environ.env -> module_kind -> 'modast -> + Entries.module_struct_entry * module_kind * Univ.ContextSet.t + +type 'modast module_params = + (lident list * ('modast * inline)) list + +(** {6 Debug} *) + +let debug_print_modtab _ = + let pr_seg = function + | [] -> str "[]" + | l -> str "[." ++ int (List.length l) ++ str ".]" + in + let pr_modinfo mp modobjs s = + let objs = modobjs.module_substituted_objects @ modobjs.module_keep_objects in + s ++ str (ModPath.to_string mp) ++ (spc ()) + ++ (pr_seg (Lib.segment_of_objects modobjs.module_prefix objs)) + in + let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in + hov 0 modules diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli new file mode 100644 index 0000000000..5c2c992825 --- /dev/null +++ b/vernac/declaremods.mli @@ -0,0 +1,139 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Modintern.module_kind -> 'modast -> + Entries.module_struct_entry * Modintern.module_kind * Univ.ContextSet.t + +type 'modast module_params = + (lident list * ('modast * inline)) list + +(** [declare_module interp_modast id fargs typ exprs] + declares module [id], with structure constructed by [interp_modast] + from functor arguments [fargs], with final type [typ]. + [exprs] is usually of length 1 (Module definition with a concrete + body), but it could also be empty ("Declare Module", with non-empty [typ]), + or multiple (body of the shape M <+ N <+ ...). *) + +val declare_module : + 'modast module_interpretor -> + Id.t -> + 'modast module_params -> + ('modast * inline) module_signature -> + ('modast * inline) list -> ModPath.t + +val start_module : + 'modast module_interpretor -> + bool option -> Id.t -> + 'modast module_params -> + ('modast * inline) module_signature -> ModPath.t + +val end_module : unit -> ModPath.t + + + +(** {6 Module types } *) + +(** [declare_modtype interp_modast id fargs typs exprs] + Similar to [declare_module], except that the types could be multiple *) + +val declare_modtype : + 'modast module_interpretor -> + Id.t -> + 'modast module_params -> + ('modast * inline) list -> + ('modast * inline) list -> + ModPath.t + +val start_modtype : + 'modast module_interpretor -> + Id.t -> + 'modast module_params -> + ('modast * inline) list -> ModPath.t + +val end_modtype : unit -> ModPath.t + +(** {6 Libraries i.e. modules on disk } *) + +type library_name = DirPath.t + +type library_objects + +val register_library : + library_name -> + Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> + Univ.ContextSet.t -> unit + +val start_library : library_name -> unit + +val end_library : + ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name -> + Safe_typing.compiled_library * library_objects * Safe_typing.native_library + +(** append a function to be executed at end_library *) +val append_end_library_hook : (unit -> unit) -> unit + +(** [import_module export mp] imports the module [mp]. + It modifies Nametab and performs the [open_object] function for + every object of the module. Raises [Not_found] when [mp] is unknown + or when [mp] corresponds to a functor. If [export] is [true], the module is also + opened every time the module containing it is. *) + +val import_module : export:bool -> ModPath.t -> unit + +(** Same as [import_module] but for multiple modules, and more optimized than + iterating [import_module]. *) +val import_modules : export:bool -> ModPath.t list -> unit + +(** Include *) + +val declare_include : + 'modast module_interpretor -> ('modast * inline) list -> unit + +(** {6 ... } *) +(** [iter_all_segments] iterate over all segments, the modules' + segments first and then the current segment. Modules are presented + in an arbitrary order. The given function is applied to all leaves + (together with their section path). *) + +val iter_all_segments : + (Libobject.object_name -> Libobject.t -> unit) -> unit + + +val debug_print_modtab : unit -> Pp.t + +(** For printing modules, [process_module_binding] adds names of + bound module (and its components) to Nametab. It also loads + objects associated to it. It may raise a [Failure] when the + bound module hasn't an atomic type. *) + +val process_module_binding : + MBId.t -> Declarations.module_alg_expr -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index cd13f83e96..4868182bb3 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,6 +1,7 @@ Vernacexpr Attributes Pvernac +Declaremods G_vernac G_proofs Vernacprop diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 43b58d6d4b..85ba464a2d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1966,26 +1966,29 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = + let mod_ops = { Printmod.import_module = Declaremods.import_module + ; process_module_binding = Declaremods.process_module_binding + } in let sigma, env = get_current_or_global_context ~pstate in function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ Library.indirect_accessor env sigma - | PrintSectionContext qid -> print_sec_context_typ Library.indirect_accessor env sigma qid - | PrintInspect n -> inspect Library.indirect_accessor env sigma n + | PrintFullContext-> print_full_context_typ ~mod_ops Library.indirect_accessor env sigma + | PrintSectionContext qid -> print_sec_context_typ ~mod_ops Library.indirect_accessor env sigma qid + | PrintInspect n -> inspect ~mod_ops Library.indirect_accessor env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () - | PrintModule qid -> print_module qid - | PrintModuleType qid -> print_modtype qid + | PrintModule qid -> print_module ~mod_ops qid + | PrintModuleType qid -> print_modtype ~mod_ops qid | PrintNamespace ns -> print_namespace ~pstate ns | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name Library.indirect_accessor env sigma qid udecl + print_name ~mod_ops Library.indirect_accessor env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() -- cgit v1.2.3 From cca4665778dd799e5802594761e13b8d53502824 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 3 Sep 2019 16:42:53 +0200 Subject: [declaremods] Remove abstraction layer over module interpretation. Now that we place imperative module declaration on top of module interpretation we can remove the abstraction layer used in `Declaremods`, so the `interp_modast` parameter goes away. Improvement suggested by Gaëtan Gilbert. --- .../10727-ejgallego-library+to_vernac_step2.sh | 6 ++ vernac/declaremods.ml | 91 ++++++++++------------ vernac/declaremods.mli | 45 ++++------- vernac/himsg.ml | 4 +- vernac/vernacentries.ml | 25 ++---- 5 files changed, 72 insertions(+), 99 deletions(-) create mode 100644 dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh new file mode 100644 index 0000000000..a5f6551474 --- /dev/null +++ b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then + + elpi_CI_REF=library+to_vernac_step2 + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 9f2e30b7a6..58a7dff5fd 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -17,7 +17,6 @@ open Entries open Libnames open Libobject open Mod_subst -open Modintern (** {6 Inlining levels} *) @@ -546,11 +545,11 @@ 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, cst) (idl,(typ,ann)) = +let intern_arg (acc, cst) (idl,(typ,ann)) = let inl = inl2intopt ann in let lib_dir = Lib.library_dp() in let env = Global.env() in - let (mty, _, cst') = interp_modast env ModType typ in + let (mty, _, cst') = Modintern.interp_module_ast env Modintern.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 @@ -578,8 +577,8 @@ let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = be more efficient and independent of [List.map] eval order. *) -let intern_args interp_modast params = - List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params +let intern_args params = + List.fold_left intern_arg ([], Univ.ContextSet.empty) params (** {6 Auxiliary functions concerning subtyping checks} *) @@ -630,11 +629,11 @@ 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 = +let build_subtypes env mp args mtys = let (cst, ans) = List.fold_left_map (fun cst (m,ann) -> let inl = inl2intopt ann in - let mte, _, cst' = interp_modast env ModType m 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 @@ -672,22 +671,22 @@ let openmodtype_info = module RawModOps = struct -let start_module interp_modast export id args res fs = +let start_module export id args res fs = let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let env = Global.env () in let res_entry_o, subtyps, cst = match res with | Enforce (res,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType res in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType res in let env = Environ.push_context_set ~strict:true cst 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 | Check resl -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in + let typs, cst = build_subtypes env mp arg_entries_r resl in None, typs, cst in let () = Global.push_context_set true cst in @@ -734,25 +733,25 @@ let end_module () = mp -let declare_module interp_modast id args res mexpr_o fs = +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 interp_modast args in + let arg_entries_r, cst = 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 | Enforce (mty,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType mty in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType mty in let env = Environ.push_context_set ~strict:true cst 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 | Check mtys -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let typs, cst = build_subtypes env mp arg_entries_r mtys in None, typs, default_inline (), cst in let env = Environ.push_context_set ~strict:true cst' env in @@ -760,7 +759,7 @@ let declare_module interp_modast id args res mexpr_o fs = let mexpr_entry_o, inl_expr, cst' = match mexpr_o with | None -> None, default_inline (), Univ.ContextSet.empty | Some (mexpr,ann) -> - let (mte, _, cst) = interp_modast env Module mexpr in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.Module mexpr in Some mte, inl2intopt ann, cst in let env = Environ.push_context_set ~strict:true cst' env in @@ -802,12 +801,12 @@ end module RawModTypeOps = struct -let start_modtype interp_modast id args mtys fs = +let start_modtype id args mtys fs = let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let env = Global.env () in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes 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 @@ -830,16 +829,16 @@ let end_modtype () = mp -let declare_modtype interp_modast id args mtys (mty,ann) fs = +let declare_modtype id args mtys (mty,ann) fs = let inl = inl2intopt ann in (* 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 interp_modast args in + let arg_entries_r, cst = intern_args 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, _, cst = interp_modast env ModType mty in + let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in let () = Global.push_context_set true cst in let env = Global.env () in (* We check immediately that mte is well-formed *) @@ -847,7 +846,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = let () = Global.push_context_set true cst in let env = Global.env () in let entry = params, mte in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes 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 @@ -901,12 +900,12 @@ let type_of_incl env is_mod = function decompose_functor mp_l (type_of_mod mp0 env is_mod) |MEwith _ -> raise NoIncludeSelf -let declare_one_include interp_modast (me_ast,annot) = +let declare_one_include (me_ast,annot) = let env = Global.env() in - let me, kind, cst = interp_modast env ModAny me_ast in + let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in let () = Global.push_context_set true cst in let env = Global.env () in - let is_mod = (kind == Module) in + let is_mod = (kind == Modintern.Module) in let cur_mp = Lib.current_mp () in let inl = inl2intopt annot in let mbids,aobjs = get_module_sobjs is_mod env inl me in @@ -924,8 +923,7 @@ let declare_one_include interp_modast (me_ast,annot) = let aobjs = subst_aobjs subst aobjs in ignore (add_leaf (Lib.current_mod_id ()) (IncludeObject aobjs)) -let declare_include interp me_asts = - List.iter (declare_one_include interp) me_asts +let declare_include me_asts = List.iter declare_one_include me_asts end @@ -941,40 +939,40 @@ let protect_summaries f = let () = Summary.unfreeze_summaries fs in iraise reraise -let start_module interp export id args res = - protect_summaries (RawModOps.start_module interp export id args res) +let start_module export id args res = + protect_summaries (RawModOps.start_module export id args res) let end_module = RawModOps.end_module -let declare_module interp id args mtys me_l = +let declare_module id args mtys me_l = let declare_me fs = match me_l with - | [] -> RawModOps.declare_module interp id args mtys None fs - | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs + | [] -> RawModOps.declare_module id args mtys None fs + | [me] -> RawModOps.declare_module id args mtys (Some me) fs | me_l -> - ignore (RawModOps.start_module interp None id args mtys fs); - RawIncludeOps.declare_include interp me_l; + ignore (RawModOps.start_module None id args mtys fs); + RawIncludeOps.declare_include me_l; RawModOps.end_module () in protect_summaries declare_me -let start_modtype interp id args mtys = - protect_summaries (RawModTypeOps.start_modtype interp id args mtys) +let start_modtype id args mtys = + protect_summaries (RawModTypeOps.start_modtype id args mtys) let end_modtype = RawModTypeOps.end_modtype -let declare_modtype interp id args mtys mty_l = +let declare_modtype id args mtys mty_l = let declare_mt fs = match mty_l with | [] -> assert false - | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs + | [mty] -> RawModTypeOps.declare_modtype id args mtys mty fs | mty_l -> - ignore (RawModTypeOps.start_modtype interp id args mtys fs); - RawIncludeOps.declare_include interp mty_l; + ignore (RawModTypeOps.start_modtype id args mtys fs); + RawIncludeOps.declare_include mty_l; RawModTypeOps.end_modtype () in protect_summaries declare_mt -let declare_include interp me_asts = - protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts) +let declare_include me_asts = + protect_summaries (fun _ -> RawIncludeOps.declare_include me_asts) (** {6 Libraries} *) @@ -1054,12 +1052,7 @@ let iter_all_segments f = (** {6 Some types used to shorten declaremods.mli} *) -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list +type module_params = (lident list * (Constrexpr.module_ast * inline)) list (** {6 Debug} *) diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index 5c2c992825..ae84704656 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -29,32 +29,24 @@ type inline = (** Kinds of modules *) -type 'modast module_interpretor = - Environ.env -> Modintern.module_kind -> 'modast -> - Entries.module_struct_entry * Modintern.module_kind * Univ.ContextSet.t +type module_params = (lident list * (Constrexpr.module_ast * inline)) list -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** [declare_module interp_modast id fargs typ exprs] - declares module [id], with structure constructed by [interp_modast] - from functor arguments [fargs], with final type [typ]. - [exprs] is usually of length 1 (Module definition with a concrete - body), but it could also be empty ("Declare Module", with non-empty [typ]), - or multiple (body of the shape M <+ N <+ ...). *) +(** [declare_module id fargs typ exprs] declares module [id], from + functor arguments [fargs], with final type [typ]. [exprs] is + usually of length 1 (Module definition with a concrete body), but + it could also be empty ("Declare Module", with non-empty [typ]), or + multiple (body of the shape M <+ N <+ ...). *) val declare_module : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_module : - 'modast module_interpretor -> bool option -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> ModPath.t val end_module : unit -> ModPath.t @@ -66,18 +58,16 @@ val end_module : unit -> ModPath.t Similar to [declare_module], except that the types could be multiple *) val declare_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> - ('modast * inline) list -> + module_params -> + (Constrexpr.module_ast * inline) list -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) list -> ModPath.t val end_modtype : unit -> ModPath.t @@ -115,8 +105,7 @@ val import_modules : export:bool -> ModPath.t list -> unit (** Include *) -val declare_include : - 'modast module_interpretor -> ('modast * inline) list -> unit +val declare_include : (Constrexpr.module_ast * inline) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ea34b601e8..c335d3ad55 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1079,9 +1079,7 @@ let explain_incorrect_with_in_module () = let explain_incorrect_module_application () = str "Illegal application to a module type." -open Modintern - -let explain_module_internalization_error = function +let explain_module_internalization_error = let open Modintern in function | NotAModuleNorModtype s -> explain_not_module_nor_modtype s | IncorrectWithInModule -> explain_incorrect_with_in_module () | IncorrectModuleApplication -> explain_incorrect_module_application () diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 85ba464a2d..ca29a6afb9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -872,10 +872,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = if not (Option.is_empty export) then user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = - Declaremods.declare_module Modintern.interp_module_ast - id binders_ast (Declaremods.Enforce mty_ast) [] - in + let mp = Declaremods.declare_module id binders_ast (Declaremods.Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export @@ -892,10 +889,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in - let mp = - Declaremods.start_module Modintern.interp_module_ast - export id binders_ast mty_ast_o - in + let mp = Declaremods.start_module export id binders_ast mty_ast_o in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Interactive Module " ++ Id.print id ++ str " started"); @@ -911,7 +905,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = - Declaremods.declare_module Modintern.interp_module_ast + Declaremods.declare_module id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef ?loc mp "mod"; @@ -938,10 +932,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in - let mp = - Declaremods.start_modtype Modintern.interp_module_ast - id binders_ast mty_sign - in + let mp = Declaremods.start_modtype id binders_ast mty_sign in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Interactive Module Type " ++ Id.print id ++ str " started"); @@ -957,10 +948,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if not (Option.is_empty export) then user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = - Declaremods.declare_modtype Modintern.interp_module_ast - id binders_ast mty_sign mty_ast_l - in + let mp = Declaremods.declare_modtype id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") @@ -970,8 +958,7 @@ let vernac_end_modtype {loc;v=id} = Dumpglob.dump_modref ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") -let vernac_include l = - Declaremods.declare_include Modintern.interp_module_ast l +let vernac_include l = Declaremods.declare_include l (**********************) (* Gallina extensions *) -- cgit v1.2.3