diff options
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 734 |
1 files changed, 565 insertions, 169 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index aac2b599..123417a6 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,8 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml 8752 2006-04-27 19:37:33Z herbelin $ i*) - +(*i $Id: declaremods.ml 11142 2008-06-18 15:37:31Z soubiran $ i*) open Pp open Util open Names @@ -78,22 +77,29 @@ let modtab_objects = (* currently started interactive module (if any) - its arguments (if it is a functor) and declared output type *) let openmod_info = - ref (([],None,None) : mod_bound_id list * module_type_entry option - * module_type_body option) + ref (([],None,None) : mod_bound_id list * module_struct_entry option + * struct_expr_body option) + +(* The library_cache here is needed to avoid recalculations of + substituted modules object during "reloading" of libraries *) +let library_cache = ref Dirmap.empty let _ = Summary.declare_summary "MODULE-INFO" { Summary.freeze_function = (fun () -> !modtab_substobjs, !modtab_objects, - !openmod_info); - Summary.unfreeze_function = (fun (sobjs,objs,info) -> + !openmod_info, + !library_cache); + Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) -> modtab_substobjs := sobjs; modtab_objects := objs; - openmod_info := info); + openmod_info := info; + library_cache := libcache); Summary.init_function = (fun () -> modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; - openmod_info := ([],None,None)); + openmod_info := ([],None,None); + library_cache := Dirmap.empty); Summary.survive_module = false; Summary.survive_section = false } @@ -107,6 +113,11 @@ let mp_of_kn kn = else anomaly ("Non-empty section in module name!" ^ string_of_kn kn) +let is_bound mp = + match mp with + | MPbound _ -> true + | _ -> false + let dir_of_sp sp = let dir,id = repr_path sp in extend_dirpath dir id @@ -122,29 +133,32 @@ let msid_of_prefix (_,(mp,sec)) = anomaly ("Non-empty section in module name!" ^ string_of_mp mp ^ "." ^ string_of_dirpath sec) -(* Check that a module type is not functorial *) - -let rec check_sig env = function - | MTBident kn -> check_sig env (Environ.lookup_modtype kn env) - | MTBsig _ -> () - | MTBfunsig _ -> Modops.error_result_must_be_signature () - -let rec check_sig_entry env = function - | MTEident kn -> check_sig env (Environ.lookup_modtype kn env) - | MTEsig _ -> () - | MTEfunsig _ -> Modops.error_result_must_be_signature () - | MTEwith (mte,_) -> check_sig_entry env mte +let scrape_alias mp = + Environ.scrape_alias mp (Global.env()) + (* This function checks if the type calculated for the module [mp] is a subtype of [sub_mtb]. Uses only the global environment. *) let check_subtypes mp sub_mtb = let env = Global.env () in - let mtb = (Environ.lookup_module mp env).mod_type in + let mtb = Environ.lookup_modtype mp env in + let sub_mtb = + {typ_expr = sub_mtb; + typ_strength = None; + typ_alias = empty_subst} in let _ = Environ.add_constraints (Subtyping.check_subtypes env mtb sub_mtb) in () (* The constraints are checked and forgot immediately! *) +let subst_substobjs dir mp (subst,mbids,msid,objs) = + match mbids with + | [] -> + let prefix = dir,(mp,empty_dirpath) in + let subst' = join_alias (map_msid msid mp) subst in + let subst = join subst' subst in + Some (subst_objects prefix (join (map_msid msid mp) subst) objs) + | _ -> None (* This function registers the visibility of the module and iterates through its components. It is called by plenty module functions *) @@ -176,7 +190,6 @@ let do_module exists what iter_objects i dir mp substobjs objects = iter_objects (i+1) prefix seg | None -> () - let conv_names_do_module exists what iter_objects i (sp,kn) substobjs substituted = let dir,mp = dir_of_sp sp, mp_of_kn kn in @@ -194,21 +207,25 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = | Some (me,sub_mte_o) -> let sub_mtb_o = match sub_mte_o with None -> None - | Some mte -> Some (Mod_typing.translate_modtype (Global.env()) mte) + | Some mte -> Some (Mod_typing.translate_struct_entry + (Global.env()) mte) in - + let mp = Global.add_module (basename sp) me in - if mp <> mp_of_kn kn then - anomaly "Kernel and Library names do not match"; + if mp <> mp_of_kn kn then + anomaly "Kernel and Library names do not match"; - match sub_mtb_o with - None -> () - | Some sub_mtb -> check_subtypes mp sub_mtb + match sub_mtb_o with + None -> () + | Some (sub_mtb,sub) -> + check_subtypes mp sub_mtb in conv_names_do_module false "cache" load_objects 1 oname substobjs substituted + + (* TODO: This check is not essential *) let check_empty s = function | None -> () @@ -231,18 +248,16 @@ let open_module i (oname,(entry,substobjs,substituted)) = conv_names_do_module true "open" open_objects i oname substobjs substituted -let subst_substobjs dir mp (subst,mbids,msid,objs) = - match mbids with - | [] -> - let prefix = dir,(mp,empty_dirpath) in - Some (subst_objects prefix (add_msid msid mp subst) objs) - | _ -> None - let subst_module ((sp,kn),subst,(entry,substobjs,_)) = check_empty "subst_module" entry; let dir,mp = dir_of_sp sp, mp_of_kn kn in let (sub,mbids,msid,objs) = substobjs in + let sub = subst_key subst sub in + let sub' = update_subst_alias subst sub in + let sub' = update_subst_alias sub' (map_msid msid mp) in + (* let sub = join_alias sub sub' in*) + let sub = join sub' sub in let subst' = join sub subst in (* substitutive_objects get the new substitution *) let substobjs = (subst',mbids,msid,objs) in @@ -256,6 +271,8 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) = let classify_module (_,(_,substobjs,_)) = Substitute (None,substobjs,None) + + let (in_module,out_module) = declare_object {(default_object "MODULE") with cache_function = cache_module; @@ -266,6 +283,182 @@ let (in_module,out_module) = export_function = (fun _ -> anomaly "No modules in sections!") } +let rec replace_alias modalias_obj obj = + let rec put_alias (id_alias,obj_alias) l = + match l with + [] -> [] + | (id,o)::r + when ( object_tag o = "MODULE") -> + if id = id_alias then +(* let (entry,subst_o,substed_o) = out_module_alias obj_alias in + let (entry',subst_o',substed_o') = out_module o in + begin + match substed_o,substed_o' with + Some a,Some b -> + (id,in_module_alias + (entry,subst_o',Some (dump_alias_object a b)))::r*) + (id_alias,obj_alias)::r + (* | _,_ -> (id,o)::r + end*) + else (id,o)::(put_alias (id_alias,obj_alias) r) + | e::r -> e::(put_alias (id_alias,obj_alias) r) in + let rec choose_obj_alias list_alias list_obj = + match list_alias with + | [] -> list_obj + | o::r ->choose_obj_alias r (put_alias o list_obj) in + choose_obj_alias modalias_obj obj + +and dump_alias_object alias_obj obj = + let rec alias_in_obj seg = + match seg with + | [] -> [] + | (id,o)::r when (object_tag o = "MODULE ALIAS") -> + (id,o)::(alias_in_obj r) + | e::r -> (alias_in_obj r) in + let modalias_obj = alias_in_obj alias_obj in + replace_alias modalias_obj obj + +and do_module_alias exists what iter_objects i dir mp alias substobjs objects = + let prefix = (dir,(alias,empty_dirpath)) in + let alias_objects = + try Some (MPmap.find alias !modtab_objects) with + Not_found -> None in + let dirinfo = DirModule (dir,(mp,empty_dirpath)) in + let vis = + if exists then + if + try Nametab.locate_dir (qualid_of_dirpath dir) = 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 + in + Nametab.push_dir vis dir dirinfo; + modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; + match alias_objects,objects with + Some (_,seg), Some seg' -> + let new_seg = dump_alias_object seg seg' in + modtab_objects := MPmap.add mp (prefix,new_seg) !modtab_objects; + iter_objects (i+1) prefix new_seg + | _,_-> () + +and cache_module_alias ((sp,kn),(entry,substobjs,substituted)) = + let dir,mp,alias = match entry with + | None -> + anomaly "You must not recache interactive modules!" + | Some (me,sub_mte_o) -> + let sub_mtb_o = match sub_mte_o with + None -> None + | Some mte -> Some (Mod_typing.translate_struct_entry + (Global.env()) mte) + in + + let mp' = match me with + | {mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + Global.add_alias (basename sp) mp + | _ -> anomaly "cache module alias" + in + if mp' <> mp_of_kn kn then + anomaly "Kernel and Library names do not match"; + + let _ = match sub_mtb_o with + None -> () + | Some (sub_mtb,sub) -> + check_subtypes mp' sub_mtb in + match me with + | {mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + dir_of_sp sp,mp_of_kn kn,scrape_alias mp + | _ -> anomaly "cache module alias" + in + do_module_alias false "cache" load_objects 1 dir mp alias substobjs substituted + +and load_module_alias i ((sp,kn),(entry,substobjs,substituted)) = + let dir,mp,alias= + match entry with + | Some (me,_)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + dir_of_sp sp,mp_of_kn kn,scrape_alias mp + | _ -> anomaly "Modops: Not an alias" + end + | None -> anomaly "Modops: Empty info" + in + do_module_alias false "load" load_objects i dir mp alias substobjs substituted + +and open_module_alias i ((sp,kn),(entry,substobjs,substituted)) = + let dir,mp,alias= + match entry with + | Some (me,_)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + dir_of_sp sp,mp_of_kn kn,scrape_alias mp + | _ -> anomaly "Modops: Not an alias" + end + | None -> anomaly "Modops: Empty info" + in + do_module_alias true "open" open_objects i dir mp alias substobjs substituted + +and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = + let dir,mp = dir_of_sp sp, mp_of_kn kn in + let (sub,mbids,msid,objs) = substobjs in + let sub' = update_subst_alias subst (map_msid msid mp) in + let subst' = join sub' subst in + let subst' = join sub subst' in + (* substitutive_objects get the new substitution *) + let substobjs = (subst',mbids,msid,objs) in + (* if we are not a functor - calculate substitued. + We add "msid |-> mp" to the substitution *) + match entry with + | Some (me,sub)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp')} -> + let mp' = subst_mp subst' mp' in + let mp' = scrape_alias mp' in + (Some ({mod_entry_type = None; + mod_entry_expr = + Some (MSEident mp')},sub), + substobjs, match mbids with + | [] -> + Some (subst_objects (dir,(mp',empty_dirpath)) + (join subst' (join (map_msid msid mp') + (map_mp mp mp'))) objs) + | _ -> None) + + | _ -> anomaly "Modops: Not an alias" + end + | None -> anomaly "Modops: Empty info" + +and classify_module_alias (_,(entry,substobjs,_)) = + Substitute (entry,substobjs,None) + +let (in_module_alias,out_module_alias) = + declare_object {(default_object "MODULE ALIAS") with + cache_function = cache_module_alias; + open_function = open_module_alias; + classify_function = classify_module_alias; + subst_function = subst_module_alias; + load_function = load_module_alias; + export_function = (fun _ -> anomaly "No modules in sections!") } + + + + + let cache_keep _ = anomaly "This module should not be cached!" let load_keep i ((sp,kn),seg) = @@ -298,7 +491,7 @@ let (in_modkeep,out_modkeep) = The module M gets its objects from SIG *) let modtypetab = - ref (KNmap.empty : substitutive_objects KNmap.t) + ref (MPmap.empty : substitutive_objects MPmap.t) (* currently started interactive module type. We remember its arguments if it is a functor type *) @@ -312,22 +505,20 @@ let _ = Summary.declare_summary "MODTYPE-INFO" modtypetab := fst ft; openmodtype_info := snd ft); Summary.init_function = (fun () -> - modtypetab := KNmap.empty; + modtypetab := MPmap.empty; openmodtype_info := []); Summary.survive_module = false; Summary.survive_section = true } - - let cache_modtype ((sp,kn),(entry,modtypeobjs)) = let _ = match entry with | None -> anomaly "You must not recache interactive module types!" | Some mte -> - let kn' = Global.add_modtype (basename sp) mte in - if kn' <> kn then + let mp = Global.add_modtype (basename sp) mte in + if mp <>mp_of_kn kn then anomaly "Kernel and Library names do not match" in @@ -335,9 +526,9 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs)) = errorlabstrm "cache_modtype" (pr_sp sp ++ str " already exists") ; - Nametab.push_modtype (Nametab.Until 1) sp kn; + Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn); - modtypetab := KNmap.add kn modtypeobjs !modtypetab + modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab let load_modtype i ((sp,kn),(entry,modtypeobjs)) = @@ -347,23 +538,22 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) = errorlabstrm "cache_modtype" (pr_sp sp ++ str " already exists") ; - Nametab.push_modtype (Nametab.Until i) sp kn; + Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn); - modtypetab := KNmap.add kn modtypeobjs !modtypetab + modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab let open_modtype i ((sp,kn),(entry,_)) = check_empty "open_modtype" entry; if - try Nametab.locate_modtype (qualid_of_sp sp) <> kn + try Nametab.locate_modtype (qualid_of_sp sp) <> (mp_of_kn kn) with Not_found -> true then errorlabstrm ("open_modtype") (pr_sp sp ++ str " should already exist!"); - Nametab.push_modtype (Nametab.Exactly i) sp kn - + Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) = check_empty "subst_modtype" entry; @@ -381,77 +571,106 @@ let (in_modtype,out_modtype) = load_function = load_modtype; subst_function = subst_modtype; classify_function = classify_modtype; - export_function = in_some } + export_function = Option.make } -let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs = - if mbids<>[] then +let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp = + let rec mp_rec = function + | [] -> MPself msid + | i::r -> MPdot(mp_rec r,label_of_id i) + in + if mbids<>[] then error "Unexpected functor objects" - else - let rec replace_idl = function - | _,[] -> [] - | id::idl,(id',obj)::tail when id = id' -> - if object_tag obj = "MODULE" then - (match idl with - [] -> (id, in_module (None,modobjs,None))::tail - | _ -> - let (_,substobjs,_) = out_module obj in - let substobjs' = replace_module_object idl substobjs modobjs in - (id, in_module (None,substobjs',None))::tail - ) - else error "MODULE expected!" - | idl,lobj::tail -> lobj::replace_idl (idl,tail) - in - (subst, mbids, msid, replace_idl (idl,lib_stack)) - + else + let rec replace_idl = function + | _,[] -> [] + | id::idl,(id',obj)::tail when id = id' -> + if object_tag obj = "MODULE" then + (match idl with + [] -> (id, in_module_alias (Some + ({mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)},None) + ,modobjs,None))::tail + | _ -> + let (_,substobjs,_) = out_module obj in + let substobjs' = replace_module_object idl substobjs modobjs mp in + (id, in_module (None,substobjs',None))::tail + ) + else error "MODULE expected!" + | idl,lobj::tail -> lobj::replace_idl (idl,tail) + in + (join (map_mp (mp_rec (List.rev idl)) mp) subst, mbids, msid, replace_idl (idl,lib_stack)) + let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) = (subst, mbids1@mbids2, msid, lib_stack) - -let rec get_modtype_substobjs = function - MTEident ln -> KNmap.find ln !modtypetab - | MTEfunsig (mbid,_,mte) -> - let (subst, mbids, msid, objs) = get_modtype_substobjs mte in +let rec get_modtype_substobjs env = function + MSEident ln -> MPmap.find ln !modtypetab + | MSEfunctor (mbid,_,mte) -> + let (subst, mbids, msid, objs) = get_modtype_substobjs env mte in (subst, mbid::mbids, msid, objs) - | MTEwith (mty, With_Definition _) -> get_modtype_substobjs mty - | MTEwith (mty, With_Module (idl,mp)) -> - let substobjs = get_modtype_substobjs mty in + | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty + | MSEwith (mty, With_Module (idl,mp)) -> + let substobjs = get_modtype_substobjs env mty in let modobjs = MPmap.find mp !modtab_substobjs in - replace_module_object idl substobjs modobjs - | MTEsig (msid,_) -> - todo "Anonymous module types"; (empty_subst, [], msid, []) + replace_module_object idl substobjs modobjs mp + | MSEapply (mexpr, MSEident mp) -> + let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in + let farg_id, farg_b, fbody_b = Modops.destr_functor env + (Modops.eval_struct env ftb) in + let mp = Environ.scrape_alias mp env in + let sub_alias = (Environ.lookup_modtype mp env).typ_alias in + let sub_alias = match Modops.eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> join_alias + (subst_key (map_msid msid mp) sub_alias) + (map_msid msid mp) + | _ -> sub_alias in + let sub3= + if sub1 = empty_subst then + update_subst sub_alias (map_mbid farg_id mp None) + else + let sub1' = join_alias sub1 (map_mbid farg_id mp None) in + let sub_alias' = update_subst sub_alias sub1' in + join sub1' sub_alias' + in + let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in + let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in + (match mbids with + | mbid::mbids -> + let resolve = + Modops.resolver_of_environment farg_id farg_b mp sub_alias env in + (* application outside the kernel, only for substitutive + objects (that are all non-logical objects) *) + ((join + (join subst (map_mbid mbid mp (Some resolve))) + sub3) + , mbids, msid, objs) + | [] -> match mexpr with + | MSEident _ -> error "Application of a non-functor" + | _ -> error "Application of a functor with too few arguments") + | 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) = let dir = make_dirpath [id] in let mp = MPbound mbid in - let substobjs = get_modtype_substobjs mty in + let substobjs = get_modtype_substobjs (Global.env()) mty in let substituted = subst_substobjs dir mp substobjs in do_module false "start" load_objects 1 dir mp substobjs substituted in List.iter2 process_arg argids args - -let replace_module mtb id mb = todo "replace module after with"; mtb - -let rec get_some_body mty env = match mty with - MTEident kn -> Environ.lookup_modtype kn env - | MTEfunsig _ - | MTEsig _ -> anomaly "anonymous module types not supported" - | MTEwith (mty,With_Definition _) -> get_some_body mty env - | MTEwith (mty,With_Module (id,mp)) -> - replace_module (get_some_body mty env) id (Environ.lookup_module mp env) - - let intern_args interp_modtype (idl,arg) = let lib_dir = Lib.library_dp() in let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in let mty = interp_modtype (Global.env()) arg in let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in - let substobjs = get_modtype_substobjs mty in + let substobjs = get_modtype_substobjs (Global.env()) mty in List.map2 (fun dir mbid -> Global.add_module_parameter mbid mty; @@ -472,39 +691,35 @@ let start_module interp_modtype export id args res_o = | Some (res, restricted) -> (* we translate the module here to catch errors as early as possible *) let mte = interp_modtype (Global.env()) res in - check_sig_entry (Global.env()) mte; if restricted then Some mte, None else - let mtb = Mod_typing.translate_modtype (Global.env()) mte in + let mtb,_ = Mod_typing.translate_struct_entry (Global.env()) mte in let sub_mtb = List.fold_right (fun (arg_id,arg_t) mte -> - let arg_t = Mod_typing.translate_modtype (Global.env()) arg_t - in MTBfunsig(arg_id,arg_t,mte)) + let arg_t,sub = Mod_typing.translate_struct_entry (Global.env()) arg_t + in + let arg_t = {typ_expr = arg_t; + typ_strength = None; + typ_alias = sub} in + SEBfunctor(arg_id,arg_t,mte)) arg_entries mtb in None, Some sub_mtb in let mbids = List.map fst arg_entries in - openmod_info:=(mbids,res_entry_o,sub_body_o); + openmod_info:=(mbids,res_entry_o,sub_body_o); let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - Lib.add_frozen_state () + Lib.add_frozen_state (); mp let end_module id = let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in let mbids, res_o, sub_o = !openmod_info in - let mp = Global.end_module id res_o in - - begin match sub_o with - None -> () - | Some sub_mtb -> check_subtypes mp sub_mtb - end; - let substitute, keep, special = Lib.classify_segment lib_stack in let dir = fst oldprefix in @@ -514,21 +729,27 @@ let end_module id = match res_o with | None -> (empty_subst, mbids, msid, substitute), keep, special - | Some (MTEident ln) -> - abstract_substobjs mbids (KNmap.find ln (!modtypetab)), [], [] - | Some (MTEsig (msid,_)) -> - todo "Anonymous signatures not supported"; - (empty_subst, mbids, msid, []), keep, special - | Some (MTEwith _ as mty) -> - abstract_substobjs mbids (get_modtype_substobjs mty), [], [] - | Some (MTEfunsig _) -> + | Some (MSEident ln) -> + abstract_substobjs mbids (MPmap.find ln (!modtypetab)), [], [] + | Some (MSEwith _ as mty) -> + abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] + | Some (MSEfunctor _) -> anomaly "Funsig cannot be here..." - with + | Some (MSEapply _ as mty) -> + abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] + with Not_found -> anomaly "Module objects not found..." in - - (* must be called after get_modtype_substobjs, because of possible + (* must be called after get_modtype_substobjs, because of possible dependencies on functor arguments *) + + let mp = Global.end_module id res_o in + + begin match sub_o with + None -> () + | Some sub_mtb -> check_subtypes mp sub_mtb + end; + Summary.module_unfreeze_summaries fs; let substituted = subst_substobjs dir mp substobjs in @@ -546,7 +767,8 @@ let end_module id = if mp_of_kn (snd newoname) <> mp then anomaly "Kernel and Library names do not match"; - Lib.add_frozen_state () (* to prevent recaching *) + Lib.add_frozen_state () (* to prevent recaching *); + mp @@ -566,18 +788,13 @@ type library_objects = mod_self_id * lib_objects * lib_objects -(* The library_cache here is needed to avoid recalculations of - substituted modules object during "reloading" of libraries *) -let library_cache = Hashtbl.create 17 - - let register_library dir cenv objs digest = let mp = MPfile dir in let substobjs, objects = try ignore(Global.lookup_module mp); (* if it's in the environment, the cached objects should be correct *) - Hashtbl.find library_cache dir + Dirmap.find dir !library_cache with Not_found -> if mp <> Global.import cenv digest then @@ -585,9 +802,9 @@ let register_library dir cenv objs digest = let msid,substitute,keep = objs in let substobjs = empty_subst, [], msid, substitute in let substituted = subst_substobjs dir mp substobjs in - let objects = option_map (fun seg -> seg@keep) substituted in + let objects = Option.map (fun seg -> seg@keep) substituted in let modobjs = substobjs, objects in - Hashtbl.add library_cache dir modobjs; + library_cache := Dirmap.add dir modobjs !library_cache; modobjs in do_module false "register_library" load_objects 1 dir mp substobjs objects @@ -625,16 +842,17 @@ 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 + let subst' = remove_alias subst in + let mp' = subst_mp subst' mp in if mp'==mp then obj else (export,mp') - + let (in_import,out_import) = declare_object {(default_object "IMPORT MODULE") with - cache_function = cache_import; - open_function = (fun i o -> if i=1 then cache_import o); - subst_function = subst_import; - classify_function = classify_import } + cache_function = cache_import; + open_function = (fun i o -> if i=1 then cache_import o); + subst_function = subst_import; + classify_function = classify_import } let import_module export mp = @@ -642,7 +860,6 @@ let import_module export mp = (************************************************************************) (* module types *) - let start_modtype interp_modtype id args = let fs = Summary.freeze_summaries () in @@ -653,7 +870,7 @@ let start_modtype interp_modtype id args = openmodtype_info := mbids; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - Lib.add_frozen_state () + Lib.add_frozen_state (); mp let end_modtype id = @@ -673,76 +890,202 @@ let end_modtype id = if fst oname <> fst oldoname then anomaly "Section paths generated on start_ and end_modtype do not match"; - if snd oname <> ln then + if (mp_of_kn (snd oname)) <> ln then anomaly "Kernel and Library names do not match"; - Lib.add_frozen_state ()(* to prevent recaching *) + Lib.add_frozen_state ()(* to prevent recaching *); + ln let declare_modtype interp_modtype id args mty = let fs = Summary.freeze_summaries () in - let _ = Global.start_modtype id in + try + let mmp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let base_mty = interp_modtype (Global.env()) mty in let entry = List.fold_right - (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) arg_entries base_mty in - let substobjs = get_modtype_substobjs entry in + let substobjs = get_modtype_substobjs (Global.env()) entry in + (* Undo the simulated interactive building of the module type *) + (* and declare the module type as a whole *) Summary.unfreeze_summaries fs; - ignore (add_leaf id (in_modtype (Some entry, substobjs))) + ignore (add_leaf id (in_modtype (Some entry, substobjs))); + mmp + with e -> + (* Something wrong: undo the whole process *) + Summary.unfreeze_summaries fs; raise e let rec get_module_substobjs env = function - | MEident mp -> MPmap.find mp !modtab_substobjs - | MEfunctor (mbid,mty,mexpr) -> + | MSEident mp -> MPmap.find mp !modtab_substobjs + | MSEfunctor (mbid,mty,mexpr) -> let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (subst, mbid::mbids, msid, objs) - | MEstruct (msid,_) -> - (empty_subst, [], msid, []) - | MEapply (mexpr, MEident mp) -> - let feb,ftb = Mod_typing.translate_mexpr env mexpr in - let ftb = Modops.scrape_modtype env ftb in - let farg_id, farg_b, fbody_b = Modops.destr_functor ftb in + | MSEapply (mexpr, MSEident mp) -> + let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in + let farg_id, farg_b, fbody_b = Modops.destr_functor env + (Modops.eval_struct env ftb) in + let mp = Environ.scrape_alias mp env in + let sub_alias = (Environ.lookup_modtype mp env).typ_alias in + let sub_alias = match Modops.eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> join_alias + (subst_key (map_msid msid mp) sub_alias) + (map_msid msid mp) + | _ -> sub_alias in + + let sub3= + if sub1 = empty_subst then + update_subst sub_alias (map_mbid farg_id mp None) + else + let sub1' = join_alias sub1 (map_mbid farg_id mp None) in + let sub_alias' = update_subst sub_alias sub1' in + join sub1' sub_alias' + in + let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (match mbids with | mbid::mbids -> - let resolve = - Modops.resolver_of_environment farg_id farg_b mp env in - (* application outside the kernel, only for substitutive - objects (that are all non-logical objects) *) - (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs) + let resolve = + Modops.resolver_of_environment farg_id farg_b mp sub_alias env in + (* application outside the kernel, only for substitutive + objects (that are all non-logical objects) *) + ((join + (join subst (map_mbid mbid mp (Some resolve))) + sub3) + , mbids, msid, objs) | [] -> match mexpr with - | MEident _ | MEstruct _ -> error "Application of a non-functor" + | MSEident _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") - | MEapply (_,mexpr) -> + | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr + | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty + | MSEwith (mty, With_Module (idl,mp)) -> + let substobjs = get_module_substobjs env mty in + let modobjs = MPmap.find mp !modtab_substobjs in + replace_module_object idl substobjs modobjs mp + + +(* Include *) + +let rec subst_inc_expr subst me = + match me with + | MSEident mp -> MSEident (subst_mp subst mp) + | MSEwith (me,With_Module(idl,mp)) -> + MSEwith (subst_inc_expr subst me, + With_Module(idl,subst_mp subst mp)) + | MSEwith (me,With_Definition(idl,const))-> + let const1 = Mod_subst.from_val const in + let force = Mod_subst.force subst_mps in + MSEwith (subst_inc_expr subst me, + With_Definition(idl,force (subst_substituted + subst const1))) + | MSEapply (me1,me2) -> + MSEapply (subst_inc_expr subst me1, + subst_inc_expr subst me2) + | _ -> anomaly "You cannot Include a high-order structure" + +let lift_oname (sp,kn) = + let mp,_,_ = Names.repr_kn kn in + let dir,_ = Libnames.repr_path sp in + (dir,mp) + +let cache_include (oname,((me,is_mod),substobjs,substituted)) = + let dir,mp1 = lift_oname oname in + let prefix = (dir,(mp1,empty_dirpath)) in + Global.add_include me; + match substituted with + Some seg -> + load_objects 1 prefix seg; + open_objects 1 prefix seg; + | None -> () + +let load_include i (oname,((me,is_mod),substobjs,substituted)) = + let dir,mp1 = lift_oname oname in + let prefix = (dir,(mp1,empty_dirpath)) in + match substituted with + Some seg -> + load_objects i prefix seg + | None -> () +let open_include i (oname,((me,is_mod),substobjs,substituted)) = + let dir,mp1 = lift_oname oname in + let prefix = (dir,(mp1,empty_dirpath)) in + match substituted with + Some seg -> + if is_mod then + open_objects i prefix seg + else + if i = 1 then + open_objects i prefix seg + | None -> () +let subst_include (oname,subst,((me,is_mod),substobj,_)) = + let dir,mp1 = lift_oname oname in + let (sub,mbids,msid,objs) = substobj in + let subst' = join sub subst in + let substobjs = (subst',mbids,msid,objs) in + let substituted = subst_substobjs dir mp1 substobjs in + ((subst_inc_expr subst' me,is_mod),substobjs,substituted) + +let classify_include (_,((me,is_mod),substobjs,_)) = + Substitute ((me,is_mod),substobjs,None) + +let (in_include,out_include) = + declare_object {(default_object "INCLUDE") with + cache_function = cache_include; + load_function = load_include; + open_function = open_include; + subst_function = subst_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 - let _ = Global.start_module id in + try + let mmp = 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 -> MTEfunsig(arg_id,arg_t,mte)) + (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 -> MTEfunsig(arg_id,arg_t,mte)) + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) arg_entries (interp_modtype (Global.env()) mty)) in @@ -750,7 +1093,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = None -> None | Some mexpr -> Some (List.fold_right - (fun (mbid,mte) me -> MEfunctor(mbid,mte,me)) + (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me)) arg_entries (interp_modexpr (Global.env()) mexpr)) in @@ -761,22 +1104,75 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = let env = Global.env() in let substobjs = match entry with - | {mod_entry_type = Some mte} -> get_modtype_substobjs mte + | {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 mp1 = Environ.scrape_alias mp env in + let prefix = dir,(mp1,empty_dirpath) in + let substituted = + match mbids with + | [] -> + Some (subst_objects prefix + (join sub (join (map_msid msid mp1) (map_mp mp' mp1))) objs) + | _ -> None in + ignore (add_leaf + id + (in_module_alias (Some ({mod_entry_type = None; + mod_entry_expr = Some (MSEident mp1) }, mty_sub_o), + substobjs, substituted))); + mmp + | _ -> + 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 sub' = subst_key (map_msid msid mp) sub in + let substobjs = (join sub sub',mbids,msid,objs) in + let substituted = subst_substobjs dir mp substobjs in + ignore (add_leaf + id + (in_module (Some (entry, mty_sub_o), substobjs, substituted))); + mmp + + with e -> + (* Something wrong: undo the whole process *) + Summary.unfreeze_summaries fs; raise e + + +let declare_include interp_struct me_ast is_mod = - 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))) - + let fs = Summary.freeze_summaries () in + try + let env = Global.env() in + let me = interp_struct env me_ast in + let substobjs = + if is_mod then + get_module_substobjs env me + else + get_modtype_substobjs env me in + let mp1,_ = current_prefix () in + let dir = dir_of_sp (Lib.path_of_include()) in + let substituted = subst_substobjs dir mp1 substobjs in + let id = current_mod_id() in + + ignore (add_leaf id + (in_include ((me,is_mod), substobjs, substituted))) + with e -> + (* Something wrong: undo the whole process *) + Summary.unfreeze_summaries fs; raise e + + (*s Iterators. *) - + let iter_all_segments f = let _ = MPmap.iter |