From 0bd300a1e2fa10ac6f0b830c6aa16416dad0d92e Mon Sep 17 00:00:00 2001 From: soubiran Date: Mon, 21 Apr 2008 08:54:48 +0000 Subject: corection bug #1837 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10822 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.ml | 164 ++++++++++++++++++++++++++++--------------------- 1 file changed, 93 insertions(+), 71 deletions(-) (limited to 'library/declaremods.ml') diff --git a/library/declaremods.ml b/library/declaremods.ml index 14851eced..3907ab21b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -897,78 +897,7 @@ let rec get_module_substobjs env = function let modobjs = MPmap.find mp !modtab_substobjs in replace_module_object idl substobjs modobjs mp -let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = - - let fs = Summary.freeze_summaries () in - - try - let _ = Global.start_module id in - let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in - let mty_entry_o, mty_sub_o = match mty_o with - None -> None, None - | (Some (mty, true)) -> - Some (List.fold_right - (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) - arg_entries - (interp_modtype (Global.env()) mty)), - None - | (Some (mty, false)) -> - None, - Some (List.fold_right - (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) - arg_entries - (interp_modtype (Global.env()) mty)) - in - let mexpr_entry_o = match mexpr_o with - None -> None - | Some mexpr -> - Some (List.fold_right - (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me)) - arg_entries - (interp_modexpr (Global.env()) mexpr)) - in - let entry = - {mod_entry_type = mty_entry_o; - mod_entry_expr = mexpr_entry_o } - in - let env = Global.env() in - let substobjs = - match entry with - | {mod_entry_type = Some mte} -> get_modtype_substobjs env mte - | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr - | _ -> anomaly "declare_module: No type, no body ..." - in - (* Undo the simulated interactive building of the module *) - (* and declare the module as a whole *) - Summary.unfreeze_summaries fs; - match entry with - |{mod_entry_type = None; - mod_entry_expr = Some (MSEident mp) } -> - let dir,mp' = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in - let (sub,mbids,msid,objs) = substobjs in - let prefix = dir,(mp',empty_dirpath) in - let mp1 = Environ.scrape_alias mp env in - let substituted = - match mbids with - | [] -> - Some (subst_objects prefix - (join sub (join (map_msid msid mp') (map_mp mp' mp1))) objs) - | _ -> None in - ignore (add_leaf - id - (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted))) - | _ -> - let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in - let substituted = subst_substobjs dir mp substobjs in - ignore (add_leaf - id - (in_module (Some (entry, mty_sub_o), substobjs, substituted))) - - with e -> - (* Something wrong: undo the whole process *) - Summary.unfreeze_summaries fs; raise e - (* Include *) let rec subst_inc_expr subst me = @@ -1043,6 +972,99 @@ let (in_include,out_include) = classify_function = classify_include; export_function = (fun _ -> anomaly "No modules in section!") } +let rec update_include (sub,mbids,msid,objs) = + let rec replace_include = function + | [] -> [] + | (id,obj)::tail -> + if object_tag obj = "INCLUDE" then + let ((me,is_mod),substobjs,substituted) = out_include obj in + if not (is_mod) then + let substobjs' = update_include substobjs in + (id, in_include ((me,true),substobjs',substituted)):: + (replace_include tail) + else + (id,obj)::(replace_include tail) + else + (id,obj)::(replace_include tail) + in + (sub,mbids,msid,replace_include objs) + + + +let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = + + let fs = Summary.freeze_summaries () in + + try + let _ = Global.start_module id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in + + let mty_entry_o, mty_sub_o = match mty_o with + None -> None, None + | (Some (mty, true)) -> + Some (List.fold_right + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) + arg_entries + (interp_modtype (Global.env()) mty)), + None + | (Some (mty, false)) -> + None, + Some (List.fold_right + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) + arg_entries + (interp_modtype (Global.env()) mty)) + in + let mexpr_entry_o = match mexpr_o with + None -> None + | Some mexpr -> + Some (List.fold_right + (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me)) + arg_entries + (interp_modexpr (Global.env()) mexpr)) + in + let entry = + {mod_entry_type = mty_entry_o; + mod_entry_expr = mexpr_entry_o } + in + let env = Global.env() in + let substobjs = + match entry with + | {mod_entry_type = Some mte} -> get_modtype_substobjs env mte + | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr + | _ -> anomaly "declare_module: No type, no body ..." + in + let substobjs = update_include substobjs in + (* Undo the simulated interactive building of the module *) + (* and declare the module as a whole *) + Summary.unfreeze_summaries fs; + match entry with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp) } -> + let dir,mp' = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let (sub,mbids,msid,objs) = substobjs in + let prefix = dir,(mp',empty_dirpath) in + let mp1 = Environ.scrape_alias mp env in + let substituted = + match mbids with + | [] -> + Some (subst_objects prefix + (join sub (join (map_msid msid mp') (map_mp mp' mp1))) objs) + | _ -> None in + ignore (add_leaf + id + (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted))) + | _ -> + let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let substituted = subst_substobjs dir mp substobjs in + ignore (add_leaf + id + (in_module (Some (entry, mty_sub_o), substobjs, substituted))) + + with e -> + (* Something wrong: undo the whole process *) + Summary.unfreeze_summaries fs; raise e + + let declare_include interp_struct me_ast is_mod = let fs = Summary.freeze_summaries () in -- cgit v1.2.3