(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* None | InlineAt i -> Some i | DefaultInline -> default_inline () (* modules and components *) (* This type is for substitutive lib_objects. The first part is a list of bound identifiers which is nonempty only if the objects are owned by a fuctor The second one is the "self" ident of the signature (or structure), which should be substituted in lib_objects with the real name of the module. The third one is the segment itself. *) type substitutive_objects = MBId.t list * module_path * lib_objects (* For each module, we store the following things: In modtab_substobjs: substitutive_objects when we will do Module M:=N, the objects of N will be reloaded with M after substitution In modtab_objects: "substituted objects" @ "keep objects" 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, the two latter lists are empty. * 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. *) let modtab_substobjs = Summary.ref (MPmap.empty : substitutive_objects MPmap.t) ~name:"MODULE-INFO-1" let modtab_objects = Summary.ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t) ~name:"MODULE-INFO-2" type current_module_info = { cur_mp : module_path; (** current started interactive module (if any) *) cur_args : MBId.t list; (** its arguments *) cur_typ : (module_struct_entry * int option) option; (** type via ":" *) cur_typs : module_type_body list (** types via "<:" *) } let default_module_info = { cur_mp = MPfile DirPath.initial; cur_args = []; cur_typ = None; cur_typs = [] } let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO-3" (* The library_cache here is needed to avoid recalculations of substituted modules object during "reloading" of libraries *) let library_cache = Summary.ref Dirmap.empty ~name:"MODULE-INFO-4" (* auxiliary functions to transform full_path and kernel_name given by Lib into module_path and DirPath.t needed for modules *) let mp_of_kn kn = let mp,sec,l = repr_kn kn in if DirPath.is_empty sec then MPdot (mp,l) else anomaly (str "Non-empty section in module name!" ++ spc () ++ pr_kn kn) let dir_of_sp sp = let dir,id = repr_path sp in add_dirpath_suffix dir id (* 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 None 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 functor type entry *) let funct_entry args m = List.fold_right (fun (arg_id,(arg_t,_)) mte -> MSEfunctor (arg_id,arg_t,mte)) args m (* Prepare the module type list for check of subtypes *) let build_subtypes interp_modtype mp args mtys = List.map (fun (m,ann) -> let inl = inl2intopt ann in let mte = interp_modtype (Global.env()) m in let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in let funct_mtb = List.fold_right (fun (arg_id,(arg_t,arg_inl)) mte -> let arg_t = Mod_typing.translate_module_type (Global.env()) (MPbound arg_id) arg_inl arg_t in SEBfunctor(arg_id,arg_t,mte)) args mtb.typ_expr in { mtb with typ_expr = funct_mtb }) mtys (* These functions register the visibility of the module and iterates through its components. They are called by plenty module functions *) let compute_visibility exists what i dir dirinfo = if exists then if try let globref = Nametab.locate_dir (qualid_of_dirpath dir) in eq_global_dir_reference globref dirinfo with Not_found -> false then Nametab.Exactly i else errorlabstrm (what^"_module") (pr_dirpath dir ++ str " should already exist!") else if Nametab.exists_dir dir then errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists") else Nametab.Until i let do_module exists what iter_objects i dir mp substobjs keep = let prefix = (dir,(mp,DirPath.empty)) in let dirinfo = DirModule prefix in let vis = compute_visibility exists what i dir dirinfo in Nametab.push_dir vis dir dirinfo; modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; match substobjs with | ([],mp1,objs) -> modtab_objects := MPmap.add mp (prefix,objs@keep) !modtab_objects; iter_objects (i+1) prefix (objs@keep) | (mbids,_,_) -> () let conv_names_do_module exists what iter_objects i ((sp,kn),substobjs) = let dir = dir_of_sp sp and mp = mp_of_kn kn in do_module exists what iter_objects i dir mp substobjs [] (* Nota: Interactive modules and module types cannot be recached! This used to be checked here via a flag along the substobjs. The check is still there for module types (see cache_modtype). *) let cache_module ((sp,kn),substobjs) = let dir = dir_of_sp sp and mp = mp_of_kn kn in do_module false "cache" load_objects 1 dir mp substobjs [] (* When this function is called the module itself is already in the environment. This function loads its objects only *) let load_module i oname_substobjs = conv_names_do_module false "load" load_objects i oname_substobjs let open_module i oname_substobjs = conv_names_do_module true "open" open_objects i oname_substobjs let subst_module (subst,(mbids,mp,objs)) = (mbids, subst_mp subst mp, subst_objects subst objs) let classify_module substobjs = Substitute substobjs let (in_module : substitutive_objects -> obj), (out_module : obj -> substitutive_objects) = declare_object_full {(default_object "MODULE") with cache_function = cache_module; load_function = load_module; open_function = open_module; subst_function = subst_module; classify_function = classify_module } let cache_keep _ = anomaly (Pp.str "This module should not be cached!") let load_keep i ((sp,kn),seg) = let mp = mp_of_kn kn in let prefix = dir_of_sp sp, (mp,DirPath.empty) in begin try let prefix',objects = MPmap.find mp !modtab_objects in if not (eq_op prefix' prefix) then anomaly (Pp.str "Two different modules with the same path!"); modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects; with Not_found -> anomaly (Pp.str "Keep objects before substitutive") end; load_objects i prefix seg let open_keep i ((sp,kn),seg) = let dirpath,mp = dir_of_sp sp, mp_of_kn kn in open_objects i (dirpath,(mp,DirPath.empty)) seg let in_modkeep : lib_objects -> obj = declare_object {(default_object "MODULE KEEP OBJECTS") with cache_function = cache_keep; load_function = load_keep; open_function = open_keep } (* we remember objects for a module type. In case of a declaration: Module M:SIG:=... The module M gets its objects from SIG *) let modtypetab = Summary.ref (MPmap.empty : substitutive_objects MPmap.t) ~name:"MODTYPE-INFO-1" (* currently started interactive module type. We remember its arguments if it is a functor type *) let openmodtype_info = Summary.ref ([],[] : MBId.t list * module_type_body list) ~name:"MODTYPE-INFO-2" let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = let mp = mp_of_kn kn in (* We enrich the global environment *) let _ = match entry with | None -> anomaly (Pp.str "You must not recache interactive module types!") | Some (mte,inl) -> if not (ModPath.equal mp (Global.add_modtype (basename sp) mte inl)) then anomaly (Pp.str "Kernel and Library names do not match") in (* Using declare_modtype should lead here, where we check that any given subtyping is indeed accurate *) check_subtypes_mt mp sub_mty_l; if Nametab.exists_modtype sp then errorlabstrm "cache_modtype" (pr_path sp ++ str " already exists") ; Nametab.push_modtype (Nametab.Until 1) sp mp; modtypetab := MPmap.add mp modtypeobjs !modtypetab let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) = assert (Option.is_empty entry); if Nametab.exists_modtype sp then errorlabstrm "cache_modtype" (pr_path sp ++ str " already exists") ; Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn); modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab let open_modtype i ((sp,kn),(entry,_,_)) = assert (Option.is_empty entry); if try let mp = Nametab.locate_modtype (qualid_of_path sp) in not (ModPath.equal mp (mp_of_kn kn)) with Not_found -> true then errorlabstrm ("open_modtype") (pr_path sp ++ str " should already exist!"); Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) let subst_modtype (subst,(entry,(mbids,mp,objs),_)) = assert (Option.is_empty entry); (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[]) let classify_modtype (_,substobjs,_) = Substitute (None,substobjs,[]) type modtype_obj = (module_struct_entry * Entries.inline) option (* will be None in vo *) * substitutive_objects * module_type_body list let in_modtype : modtype_obj -> obj = declare_object {(default_object "MODULE TYPE") with cache_function = cache_modtype; open_function = open_modtype; load_function = load_modtype; subst_function = subst_modtype; classify_function = classify_modtype } let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 = let () = match mbids with | [] -> () | _ -> anomaly (Pp.str "Unexpected functor objects") in let rec replace_idl = function | _,[] -> [] | id::idl,(id',obj)::tail when Id.equal id id' -> if not (String.equal (object_tag obj) "MODULE") then anomaly (Pp.str "MODULE expected!"); let substobjs = match idl with | [] -> let mp' = MPdot(mp, Label.of_id id) in mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs | _ -> replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp in (id, in_module substobjs)::tail | idl,lobj::tail -> lobj::replace_idl (idl,tail) in (mbids, mp, replace_idl (idl,lib_stack)) let discr_resolver mb = match mb.mod_type with | SEBstruct _ -> Some mb.mod_delta | _ -> None (* when mp is a functor *) (* Small function to avoid module typing during substobjs retrivial *) let rec get_objs_modtype_application env = function | MSEident mp -> MPmap.find mp !modtypetab,Environ.lookup_modtype mp env,[] | MSEapply (fexpr, MSEident mp) -> let objs,mtb,mp_l= get_objs_modtype_application env fexpr in objs,mtb,mp::mp_l | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr | _ -> error "Application of a non-functor." let rec compute_subst env mbids sign mp_l inl = match mbids,mp_l with | _,[] -> mbids,empty_subst | [],r -> error "Application of a functor with too few arguments." | mbid::mbids,mp::mp_l -> let farg_id, farg_b, fbody_b = Modops.destr_functor env 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 = match discr_resolver mb with | None -> empty_delta_resolver | Some mp_delta -> Modops.inline_delta_resolver env inl mp farg_id farg_b mp_delta in mbid_left,join (map_mbid mbid mp resolver) subst let rec get_modtype_substobjs env inline = function | MSEident ln -> MPmap.find ln !modtypetab | MSEfunctor (mbid,_,mte) -> let (mbids, mp, objs) = get_modtype_substobjs env inline mte in (mbid::mbids, mp, objs) | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env inline mty | MSEwith (mty, With_Module (idl,mp1)) -> let substobjs = get_modtype_substobjs env inline mty in let modobjs = MPmap.find mp1 !modtab_substobjs in replace_module_object idl substobjs modobjs mp1 | MSEapply (fexpr, MSEident mp) as me -> let (mbids, mp1, objs),mtb_mp1,mp_l = get_objs_modtype_application env me in let mbids_left,subst = compute_subst env mbids mtb_mp1.typ_expr (List.rev mp_l) inline in (mbids_left, mp1,subst_objects subst objs) | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr (* push names of a bound module (and its component) to Nametab *) (* add objects associated to it *) let process_module_binding mbid mty = let dir = DirPath.make [MBId.to_id mbid] in let mp = MPbound mbid in let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) (default_inline ()) mty in let subst = map_mp mp_from mp empty_delta_resolver in let substobjs = (mbids,mp,subst_objects subst objs) in do_module false "start" load_objects 1 dir mp substobjs [] (* Same with module_type_body *) let rec seb2mse = function | SEBident mp -> MSEident mp | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s') | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp)) | SEBwith (s,With_definition_body(l,cb)) -> (match cb.const_body with | Def c -> MSEwith(seb2mse s,With_Definition(l,Lazyconstr.force c)) | _ -> assert false) | _ -> failwith "seb2mse: received a non-atomic seb" let process_module_seb_binding mbid seb = process_module_binding mbid (seb2mse seb) let intern_args interp_modtype (idl,(arg,ann)) = let inl = inl2intopt ann in let lib_dir = Lib.library_dp() in let env = Global.env() in let mty = interp_modtype env arg in let (mbi,mp_from,objs) = get_modtype_substobjs env inl mty in List.map (fun (_,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 subst = map_mp mp_from mp resolver in let substobjs = (mbi,mp,subst_objects subst objs) in do_module false "interp" load_objects 1 dir mp substobjs []; (mbid,(mty,inl))) idl let start_module_ interp_modtype export id args res fs = let mp = Global.start_module id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let res_entry_o, subtyps = match res with | Enforce (res,ann) -> let inl = inl2intopt ann in let mte = interp_modtype (Global.env()) res in let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in Some (mte,inl), [] | Check resl -> None, build_subtypes interp_modtype mp arg_entries resl in let mbids = List.map fst arg_entries in openmod_info:= { cur_mp = mp; cur_args = mbids; cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); Lib.add_frozen_state (); 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 let mp_from, substobjs, keep, special = match m_info.cur_typ with | None -> (* the module is not sealed *) None, (m_info.cur_args, m_info.cur_mp, substitute), keep, special | Some (MSEfunctor _, _) -> anomaly (Pp.str "Funsig cannot be here...") | Some (mty, inline) -> let (mbids1,mp1,objs) = try get_modtype_substobjs (Global.env()) inline mty with Not_found -> anomaly (Pp.str "Module objects not found...") in Some mp1,(m_info.cur_args@mbids1,mp1,objs), [], [] in (* must be called after get_modtype_substobjs, because of possible dependencies on functor arguments *) let id = basename (fst oldoname) in let mp,resolver = Global.end_module fs id m_info.cur_typ in check_subtypes mp m_info.cur_typs; (* we substitute objects if the module is sealed by a signature (ie. mp_from != None *) let substobjs = match mp_from,substobjs with | None,_ -> substobjs | Some mp_from,(mbids,_,objs) -> (mbids,mp,subst_objects (map_mp mp_from mp resolver) objs) in let node = in_module substobjs in let objects = match keep, m_info.cur_args with | [], _ | _, _ :: _ -> special@[node] (* no keep objects or we are defining a functor *) | _ -> special@[node;in_modkeep keep] (* otherwise *) in let newoname = Lib.add_leaves id objects in if not (eq_full_path (fst newoname) (fst oldoname)) then anomaly (Pp.str "Names generated on start_ and end_module do not match"); if not (ModPath.equal (mp_of_kn (snd newoname)) mp) then anomaly (Pp.str "Kernel and Library names do not match"); Lib.add_frozen_state () (* to prevent recaching *); mp let module_objects mp = let prefix,objects = MPmap.find mp !modtab_objects in segment_of_objects prefix objects (************************************************************************) (* libraries *) type library_name = DirPath.t (* The first two will form substitutive_objects, the last one is keep *) type library_objects = module_path * lib_objects * lib_objects let register_library dir cenv objs digest = let mp = MPfile dir in let substobjs, keep, values = try ignore(Global.lookup_module mp); (* if it's in the environment, the cached objects should be correct *) Dirmap.find dir !library_cache with Not_found -> let mp', values = Global.import cenv digest in if not (ModPath.equal mp mp') then anomaly (Pp.str "Unexpected disk module name"); let mp,substitute,keep = objs in let substobjs = [], mp, substitute in let modobjs = substobjs, keep, values in library_cache := Dirmap.add dir modobjs !library_cache; modobjs in do_module false "register_library" load_objects 1 dir mp substobjs keep let get_library_symbols_tbl dir = let _,_,values = Dirmap.find dir !library_cache in values let start_library dir = let mp = Global.start_library dir in openmod_info := { default_module_info with cur_mp = mp }; Lib.start_compilation dir mp; Lib.add_frozen_state () let end_library dir = let prefix, lib_stack = Lib.end_compilation dir in let mp,cenv,ast = Global.export dir in let substitute, keep, _ = Lib.classify_segment lib_stack in cenv,(mp,substitute,keep),ast (* implementation of Export M and Import M *) let really_import_module mp = let prefix,objects = MPmap.find mp !modtab_objects in open_objects 1 prefix objects let cache_import (_,(_,mp)) = (* for non-substitutive exports: let mp = Nametab.locate_module (qualid_of_dirpath dir) in *) really_import_module mp let classify_import (export,_ as obj) = if export then Substitute obj else Dispose let subst_import (subst,(export,mp as obj)) = let mp' = subst_mp subst mp in if mp'==mp then obj else (export,mp') let in_import = declare_object {(default_object "IMPORT MODULE") with cache_function = cache_import; open_function = (fun i o -> if Int.equal i 1 then cache_import o); subst_function = subst_import; classify_function = classify_import } let import_module export mp = Lib.add_anonymous_leaf (in_import (export,mp)) (************************************************************************) (* module types *) let start_modtype_ interp_modtype id args mtys fs = let mp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let sub_mty_l = build_subtypes interp_modtype mp arg_entries mtys in let mbids = List.map fst arg_entries in openmodtype_info := mbids, sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); Lib.add_frozen_state (); 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 mbids, sub_mty_l = !openmodtype_info in let mp = Global.end_modtype fs id in let modtypeobjs = mbids, mp, substitute in check_subtypes_mt mp sub_mty_l; let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs,[])]) in if not (eq_full_path (fst oname) (fst oldoname)) then anomaly (str "Section paths generated on start_ and end_modtype do not match"); if not (ModPath.equal (mp_of_kn (snd oname)) mp) then anomaly (str "Kernel and Library names do not match"); Lib.add_frozen_state ()(* to prevent recaching *); mp let declare_modtype_ interp_modtype id args mtys (mty,ann) fs = let inl = inl2intopt ann in let mmp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in (* NB: check of subtyping will be done in cache_modtype *) let sub_mty_l = build_subtypes interp_modtype mmp arg_entries mtys in let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) inl entry in (* Undo the simulated interactive building of the module type *) (* and declare the module type as a whole *) let subst = map_mp mp_from mmp empty_delta_resolver in let substobjs = (mbids,mmp, subst_objects subst objs) in Summary.unfreeze_summaries fs; ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l))); mmp (* Small function to avoid module typing during substobjs retrivial *) let rec get_objs_module_application env = function | MSEident mp -> MPmap.find mp !modtab_substobjs,Environ.lookup_module mp env,[] | MSEapply (fexpr, MSEident mp) -> let objs,mtb,mp_l= get_objs_module_application env fexpr in objs,mtb,mp::mp_l | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr | _ -> error "Application of a non-functor." let rec get_module_substobjs env inl = function | MSEident mp -> MPmap.find mp !modtab_substobjs | MSEfunctor (mbid,mty,mexpr) -> let (mbids, mp, objs) = get_module_substobjs env inl mexpr in (mbid::mbids, mp, objs) | MSEapply (fexpr, MSEident mp) as me -> let (mbids, mp1, objs),mb_mp1,mp_l = get_objs_module_application env me in let mbids_left,subst = compute_subst env mbids mb_mp1.mod_type (List.rev mp_l) inl in (mbids_left, mp1,subst_objects subst objs) | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr | MSEwith (mty, With_Definition _) -> get_module_substobjs env inl mty | MSEwith (mty, With_Module (idl,mp)) -> assert false let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = let mmp = Global.start_module id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let funct f m = funct_entry arg_entries (f (Global.env ()) m) in let env = Global.env() in let mty_entry_o, subs, inl_res = match res with | Enforce (mty,ann) -> Some (funct interp_modtype mty), [], inl2intopt ann | Check mtys -> None, build_subtypes interp_modtype mmp arg_entries mtys, default_inline () in (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in *) let mexpr_entry_o, inl_expr = match mexpr_o with | None -> None, default_inline () | Some (mexpr,ann) -> Some (funct interp_modexpr mexpr), inl2intopt ann in let entry = {mod_entry_type = mty_entry_o; mod_entry_expr = mexpr_entry_o } in let substobjs = match entry with | {mod_entry_type = Some mte} -> get_modtype_substobjs env inl_res mte | {mod_entry_expr = Some mexpr} -> get_module_substobjs env inl_expr mexpr | _ -> anomaly ~label:"declare_module" (Pp.str "No type, no body ...") in let (mbids,mp_from,objs) = substobjs in (* Undo the simulated interactive building of the module *) (* and declare the module as a whole *) Summary.unfreeze_summaries fs; let mp = mp_of_kn (Lib.make_kn id) in let inl = match inl_expr with | None -> None | _ -> inl_res in (* PLTODO *) let mp_env,resolver = Global.add_module id entry inl in if not (ModPath.equal mp_env mp) then anomaly (Pp.str "Kernel and Library names do not match"); check_subtypes mp subs; let subst = map_mp mp_from mp_env resolver in let substobjs = (mbids,mp_env, subst_objects subst objs) in ignore (add_leaf id (in_module substobjs)); mmp (* Include *) let do_include_objs i do_load do_open ((sp,kn),objs) = let dir = Libnames.dirpath sp in let mp = KerName.modpath kn in let prefix = (dir,(mp,DirPath.empty)) in if do_load then load_objects i prefix objs; if do_open then open_objects i prefix objs let cache_include oname_objs = do_include_objs 1 true true oname_objs let load_include i oname_objs = do_include_objs i true false oname_objs let open_include i oname_objs = do_include_objs i false true oname_objs let subst_include (subst,objs) = subst_objects subst objs let classify_include objs = Substitute objs type include_obj = Lib.lib_objects let (in_include : include_obj -> obj), (out_include : obj -> include_obj) = declare_object_full {(default_object "INCLUDE") with cache_function = cache_include; load_function = load_include; open_function = open_include; subst_function = subst_include; classify_function = classify_include } 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 env 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 exception NothingToDo let get_includeself_substobjs env mp1 mbids objs me is_mod inline = try let mb_mp = match me with | MSEident mp -> if is_mod then Environ.lookup_module mp env else Modops.module_body_of_type mp (Environ.lookup_modtype mp env) | MSEapply(fexpr, MSEident p) as mexpr -> let _,mb_mp,mp_l = if is_mod then get_objs_module_application env mexpr else let o,mtb_mp,mp_l = get_objs_modtype_application env mexpr in o,Modops.module_body_of_type mtb_mp.typ_mp mtb_mp,mp_l in List.fold_left (fun mb _ -> match mb.mod_type with | SEBfunctor(_,_,str) -> {mb with mod_type = str} | _ -> error "Application of a functor with too much arguments.") mb_mp mp_l | _ -> raise NothingToDo in let reso = fst (Safe_typing.delta_of_senv (Global.safe_env ())) in let subst = include_subst env mp1 reso mbids mb_mp.mod_type inline in subst_objects subst objs with NothingToDo -> objs let declare_one_include_inner annot (me,is_mod) = let env = Global.env() in let cur_mp = fst (current_prefix ()) in let inl = inl2intopt annot in let (mbids,mp,objs)= if is_mod then get_module_substobjs env inl me else get_modtype_substobjs env inl me in let objs = if List.is_empty mbids then objs else get_includeself_substobjs env cur_mp mbids objs me is_mod inl in let id = current_mod_id() in let resolver = Global.add_include me is_mod inl in let subst = map_mp mp cur_mp resolver in let substobjs = subst_objects subst objs in ignore (add_leaf id (in_include substobjs)) let declare_one_include interp_struct (me_ast,annot) = declare_one_include_inner annot (interp_struct (Global.env()) me_ast) let declare_include_ interp_struct me_asts = List.iter (declare_one_include interp_struct) me_asts (** Versions of earlier functions taking care of the freeze/unfreeze of summaries *) 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 = Errors.push reraise in let () = Summary.unfreeze_summaries fs in raise reraise let declare_include interp_struct me_asts = protect_summaries (fun _ -> declare_include_ interp_struct me_asts) let declare_modtype interp_mt interp_mix id args mtys mty_l = let declare_mt fs = match mty_l with | [] -> assert false | [mty] -> declare_modtype_ interp_mt id args mtys mty fs | mty_l -> ignore (start_modtype_ interp_mt id args mtys fs); declare_include_ interp_mix mty_l; end_modtype () in protect_summaries declare_mt let start_modtype interp_modtype id args mtys = protect_summaries (start_modtype_ interp_modtype id args mtys) let declare_module interp_mt interp_me interp_mix id args mtys me_l = let declare_me fs = match me_l with | [] -> declare_module_ interp_mt interp_me id args mtys None fs | [me] -> declare_module_ interp_mt interp_me id args mtys (Some me) fs | me_l -> ignore (start_module_ interp_mt None id args mtys fs); declare_include_ interp_mix me_l; end_module () in protect_summaries declare_me let start_module interp_modtype export id args res = protect_summaries (start_module_ interp_modtype export id args res) (*s Iterators. *) let iter_all_segments f = let _ = MPmap.iter (fun _ (prefix,objects) -> let rec apply_obj (id,obj) = match object_tag obj with | "INCLUDE" -> List.iter apply_obj (out_include obj) | _ -> f (make_oname prefix id) obj in List.iter apply_obj objects) !modtab_objects in let apply_node = function | sp, Leaf o -> f sp o | _ -> () in List.iter apply_node (Lib.contents ()) let debug_print_modtab _ = let pr_seg = function | [] -> str "[]" | l -> str ("[." ^ string_of_int (List.length l) ^ ".]") in let pr_modinfo mp (prefix,objects) s = s ++ str (string_of_mp mp) ++ (spc ()) ++ (pr_seg (segment_of_objects prefix objects)) in let modules = MPmap.fold pr_modinfo !modtab_objects (mt ()) in hov 0 modules