From 2d1910dc6ec51827b5ef4f05b12f0641f46a66f7 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 15 Apr 2013 19:36:51 +0000 Subject: Minor simplifications in Declaremods and Safe_typing - get_module_substobjs (resp. modtype) without useless mp_from arg - no need for the whole Safe_typing.pack_module - ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16407 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.ml | 132 +++++++++++++++++++++++-------------------------- 1 file changed, 61 insertions(+), 71 deletions(-) (limited to 'library/declaremods.ml') diff --git a/library/declaremods.ml b/library/declaremods.ml index 303641596..992ca42fc 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -456,18 +456,18 @@ let rec compute_subst env mbids sign mp_l inl = in mbid_left,join (map_mbid mbid mp resolver) subst -let rec get_modtype_substobjs env mp_from inline = function - MSEident ln -> - MPmap.find ln !modtypetab +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 mp_from inline mte in - (mbid::mbids, mp, objs) + let (mbids, mp, objs) = get_modtype_substobjs env inline mte in + (mbid::mbids, mp, objs) | MSEwith (mty, With_Definition _) -> - get_modtype_substobjs env mp_from inline mty - | MSEwith (mty, With_Module (idl,mp1)) -> - let substobjs = get_modtype_substobjs env mp_from inline mty in + 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 + 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 @@ -478,20 +478,17 @@ let rec get_modtype_substobjs env mp_from inline = function | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr -(* push names of bound modules (and their components) to Nametab *) -(* add objects associated to them *) -let process_module_bindings argids args = - let process_arg id (mbid,(mty,ann)) = - let dir = DirPath.make [id] in - let mp = MPbound mbid in - let (mbids,mp_from,objs) = - get_modtype_substobjs (Global.env()) mp (inline_annot ann) 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 [] +(* 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 - List.iter2 process_arg argids args + 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 *) @@ -506,29 +503,25 @@ let rec seb2mse = function | _ -> failwith "seb2mse: received a non-atomic seb" let process_module_seb_binding mbid seb = - process_module_bindings [MBId.to_id mbid] - [mbid, - (seb2mse seb, - { ann_inline = DefaultInline; ann_scope_subst = [] })] + process_module_binding mbid (seb2mse seb) let intern_args interp_modtype (idl,(arg,ann)) = let inl = inline_annot ann in let lib_dir = Lib.library_dp() in - let mbids = List.map (fun (_,id) -> MBId.make lib_dir id) idl in - let mty = interp_modtype (Global.env()) arg in - let dirs = List.map (fun (_,id) -> DirPath.make [id]) idl in - let (mbi,mp_from,objs) = - get_modtype_substobjs (Global.env()) (MPbound (List.hd mbids)) inl mty - in - List.map2 - (fun dir mbid -> - let resolver = Global.add_module_parameter mbid mty inl in - let mp = MPbound mbid 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))) - dirs mbids + 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 @@ -562,17 +555,17 @@ let end_module () = None,( mbids, mp, substitute), keep, special | Some (MSEident ln as mty, inline) -> let (mbids1,mp1,objs) = - get_modtype_substobjs (Global.env()) mp inline mty in + get_modtype_substobjs (Global.env()) inline mty in Some mp1,(mbids@mbids1,mp1,objs), [], [] | Some (MSEwith _ as mty, inline) -> let (mbids1,mp1,objs) = - get_modtype_substobjs (Global.env()) mp inline mty in + get_modtype_substobjs (Global.env()) inline mty in Some mp1,(mbids@mbids1,mp1,objs), [], [] | Some (MSEfunctor _, _) -> anomaly (Pp.str "Funsig cannot be here...") | Some (MSEapply _ as mty, inline) -> let (mbids1,mp1,objs) = - get_modtype_substobjs (Global.env()) mp inline mty in + get_modtype_substobjs (Global.env()) inline mty in Some mp1,(mbids@mbids1,mp1,objs), [], [] with Not_found -> anomaly (Pp.str "Module objects not found...") @@ -742,7 +735,7 @@ let declare_modtype_ interp_modtype id args mtys (mty,ann) fs = 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()) mmp inl entry 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 *) @@ -767,11 +760,11 @@ let rec get_objs_module_application env = function | _ -> error "Application of a non-functor." -let rec get_module_substobjs env mp_from inl = function +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 mp_from inl mexpr in - (mbid::mbids, mp, objs) + 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 @@ -780,7 +773,7 @@ let rec get_module_substobjs env mp_from inl = function 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 mp_from inl mty + | MSEwith (mty, With_Definition _) -> get_module_substobjs env inl mty | MSEwith (mty, With_Module (idl,mp)) -> assert false @@ -812,8 +805,8 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = let substobjs = match entry with - | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte - | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr + | {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 @@ -876,21 +869,20 @@ let (in_include : include_obj -> obj), subst_function = subst_include; classify_function = classify_include } -let rec include_subst env mb mbids sign inline = +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 mb mbids fbody_b inline in + let subst = include_subst env mp reso mbids fbody_b inline in let mp_delta = - Modops.inline_delta_resolver env inline mb.mod_mp - farg_id farg_b mb.mod_delta + Modops.inline_delta_resolver env inline mp farg_id farg_b reso in - join (map_mbid mbid mb.mod_mp mp_delta) subst + join (map_mbid mbid mp mp_delta) subst exception NothingToDo -let get_includeself_substobjs env objs me is_mod inline = +let get_includeself_substobjs env mp1 mbids objs me is_mod inline = try let mb_mp = match me with | MSEident mp -> @@ -914,10 +906,9 @@ let get_includeself_substobjs env objs me is_mod inline = mb_mp mp_l | _ -> raise NothingToDo in - let (mbids,mp_self,objects) = objs in - let mb = Global.pack_module() in - let subst = include_subst env mb mbids mb_mp.mod_type inline in - ([],mp_self,subst_objects subst objects) + 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 @@ -925,22 +916,21 @@ let get_includeself_substobjs env objs me is_mod inline = let declare_one_include_inner annot (me,is_mod) = let env = Global.env() in - let mp1,_ = current_prefix () in + let cur_mp = fst (current_prefix ()) in let inl = inline_annot annot in let (mbids,mp,objs)= if is_mod then - get_module_substobjs env mp1 inl me - else - get_modtype_substobjs env mp1 inl me in - let (mbids,mp,objs) = - if not (List.is_empty mbids) then - get_includeself_substobjs env (mbids,mp,objs) me is_mod inl + get_module_substobjs env inl me else - (mbids,mp,objs) in + 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 resolver = Global.add_include me is_mod inl in register_scope_subst annot.ann_scope_subst; - let subst = map_mp mp mp1 resolver in + let subst = map_mp mp cur_mp resolver in let substobjs = subst_objects subst objs in reset_scope_subst (); ignore (add_leaf id (in_include substobjs)) -- cgit v1.2.3