From a74338cc598b5fb45e2cc148d243433500bb5294 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 13 Mar 2013 18:01:12 +0000 Subject: Declaremods: a few syntactic improvements git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16299 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.ml | 45 ++++++++++++++++++++++----------------------- 1 file changed, 22 insertions(+), 23 deletions(-) (limited to 'library/declaremods.ml') diff --git a/library/declaremods.ml b/library/declaremods.ml index 366fb77a0..356defcac 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -509,12 +509,13 @@ let process_module_bindings argids args = 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 substobjs = (mbids,mp,subst_objects - (map_mp mp_from mp empty_delta_resolver) objs)in - do_module false "start" load_objects 1 dir mp substobjs [] + get_modtype_substobjs (Global.env()) mp (inline_annot ann) 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 [] + in + List.iter2 process_arg argids args (* Same with module_type_body *) @@ -540,16 +541,17 @@ let intern_args interp_modtype (idl,(arg,ann)) = 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 + 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 substobjs = (mbi,mp,subst_objects - (map_mp mp_from mp resolver) objs) in - do_module false "interp" load_objects 1 dir mp substobjs []; - (mbid,(mty,inl))) + 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 start_module_ interp_modtype export id args res fs = @@ -769,9 +771,8 @@ let declare_modtype_ interp_modtype id args mtys (mty,ann) fs = (* and declare the module type as a whole *) register_scope_subst ann.ann_scope_subst; - let substobjs = (mbids,mmp, - subst_objects (map_mp mp_from mmp empty_delta_resolver) objs) - in + let subst = map_mp mp_from mmp empty_delta_resolver in + let substobjs = (mbids,mmp, subst_objects subst objs) in reset_scope_subst (); Summary.unfreeze_summaries fs; ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l))); @@ -850,17 +851,15 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = in (* PLTODO *) let mp_env,resolver = Global.add_module id entry inl in - if not (mp_eq mp_env mp) then anomaly (Pp.str "Kernel and Library names do not match"); + if not (mp_eq mp_env mp) + then anomaly (Pp.str "Kernel and Library names do not match"); - check_subtypes mp subs; register_scope_subst scl; - let substobjs = (mbids,mp_env, - subst_objects(map_mp mp_from mp_env resolver) objs) in + let subst = map_mp mp_from mp_env resolver in + let substobjs = (mbids,mp_env, subst_objects subst objs) in reset_scope_subst (); - ignore (add_leaf - id - (in_module substobjs)); + ignore (add_leaf id (in_module substobjs)); mmp (* Include *) @@ -986,8 +985,8 @@ let declare_one_include_inner annot (me,is_mod) = let id = current_mod_id() in let resolver = Global.add_include me is_mod inl in register_scope_subst annot.ann_scope_subst; - let substobjs = (mbids,mp1, - subst_objects (map_mp mp mp1 resolver) objs) in + let subst = map_mp mp mp1 resolver in + let substobjs = (mbids,mp1, subst_objects subst objs) in reset_scope_subst (); ignore (add_leaf id (in_include (me, substobjs))) -- cgit v1.2.3