diff options
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 835 |
1 files changed, 296 insertions, 539 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index d796a2906..548a9b0f3 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -22,7 +22,7 @@ open Mod_subst (* modules and components *) -(* This type is a functional closure of substitutive lib_objects. +(* OBSOLETE This type is a functional closure of substitutive lib_objects. The first part is a partial substitution (which will be later applied to lib_objects when completed). @@ -41,7 +41,7 @@ open Mod_subst *) type substitutive_objects = - substitution * mod_bound_id list * mod_self_id * lib_objects + mod_bound_id list * module_path * lib_objects (* For each module, we store the following things: @@ -77,9 +77,10 @@ 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_struct_entry option - * struct_expr_body option) +let openmod_info = + ref ((MPfile(initial_dir),[],None,None) + : module_path * mod_bound_id list * module_struct_entry option + * module_type_body option) (* The library_cache here is needed to avoid recalculations of substituted modules object during "reloading" of libraries *) @@ -99,7 +100,8 @@ let _ = Summary.declare_summary "MODULE-INFO" Summary.init_function = (fun () -> modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; - openmod_info := ([],None,None); + openmod_info := ((MPfile(initial_dir), + [],None,None)); library_cache := Dirmap.empty) } (* auxiliary functions to transform full_path and kernel_name given @@ -116,50 +118,18 @@ let dir_of_sp sp = let dir,id = repr_path sp in add_dirpath_suffix dir id -let msid_of_mp = function - MPself msid -> msid - | _ -> anomaly "'Self' module path expected!" - -let msid_of_prefix (_,(mp,sec)) = - if sec=empty_dirpath then - msid_of_mp mp - else - anomaly ("Non-empty section in module name!" ^ - string_of_mp mp ^ "." ^ string_of_dirpath sec) - -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_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) + let mb = Environ.lookup_module mp env in + let mtb = Modops.module_type_of_module env None mb in + let _ = Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) in () (* The constraints are checked and forgot immediately! *) -let compute_subst_objects mp (subst,mbids,msid,objs) = - match mbids with - | [] -> - let subst' = join_alias (map_msid msid mp) subst in - Some (join (map_msid msid mp) (join subst' subst), objs) - | _ -> - None - -let subst_substobjs dir mp substobjs = - match compute_subst_objects mp substobjs with - | Some (subst, objs) -> - let prefix = dir,(mp,empty_dirpath) in - Some (subst_objects prefix subst objs) - | None -> None - (* These functions register the visibility of the module and iterates through its components. They are called by plenty module functions *) @@ -178,12 +148,12 @@ let compute_visibility exists what i dir dirinfo = errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists") else Nametab.Until i - +(* let do_load_and_subst_module i dir mp substobjs keep = let prefix = (dir,(mp,empty_dirpath)) in let dirinfo = DirModule (dir,(mp,empty_dirpath)) in let vis = compute_visibility false "load_and_subst" i dir dirinfo in - let objects = compute_subst_objects mp substobjs in + let objects = compute_subst_objects mp substobjs resolver in Nametab.push_dir vis dir dirinfo; modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; match objects with @@ -194,55 +164,33 @@ let do_load_and_subst_module i dir mp substobjs keep = Some (seg@keep) | None -> None +*) -let do_module exists what iter_objects i dir mp substobjs objects = +let do_module exists what iter_objects i dir mp substobjs keep= let prefix = (dir,(mp,empty_dirpath)) in let dirinfo = DirModule (dir,(mp,empty_dirpath)) 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 objects with - Some seg -> - modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects; - iter_objects (i+1) prefix seg - | None -> () + 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 substituted = + (sp,kn) substobjs = let dir,mp = dir_of_sp sp, mp_of_kn kn in - do_module exists what iter_objects i dir mp substobjs substituted + do_module exists what iter_objects i dir mp substobjs [] (* Interactive modules and module types cannot be recached! cache_mod* functions can be called only once (and "end_mod*" set the flag to false then) *) - -let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = - let _ = 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 = Global.add_module (basename sp) me in - if mp <> mp_of_kn kn then - anomaly "Kernel and Library names do not match"; - - 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 - - - - +let cache_module ((sp,kn),(entry,substobjs)) = + let dir,mp = dir_of_sp sp, mp_of_kn kn in + do_module false "cache" load_objects 1 dir mp substobjs [] + (* TODO: This check is not essential *) let check_empty s = function | None -> () @@ -253,42 +201,26 @@ let check_empty s = function (* When this function is called the module itself is already in the environment. This function loads its objects only *) -let load_module i (oname,(entry,substobjs,substituted)) = +let load_module i (oname,(entry,substobjs)) = (* TODO: This check is not essential *) check_empty "load_module" entry; - conv_names_do_module false "load" load_objects i oname substobjs substituted + conv_names_do_module false "load" load_objects i oname substobjs -let open_module i (oname,(entry,substobjs,substituted)) = +let open_module i (oname,(entry,substobjs)) = (* TODO: This check is not essential *) check_empty "open_module" entry; - conv_names_do_module true "open" open_objects i oname substobjs substituted + conv_names_do_module true "open" open_objects i oname substobjs -let subst_module ((sp,kn),subst,(entry,substobjs,_)) = +let subst_module (subst,(entry,(mbids,mp,objs))) = 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 - (* if we are not a functor - calculate substitued. - We add "msid |-> mp" to the substitution *) - let substituted = subst_substobjs dir mp substobjs - in - (None,substobjs,substituted) - - -let classify_module (_,substobjs,_) = - Substitute (None,substobjs,None) + (None,(mbids,subst_mp subst mp, subst_objects subst objs)) +let classify_module (_,substobjs) = + Substitute (None,substobjs) let (in_module,out_module) = declare_object {(default_object "MODULE") with @@ -298,168 +230,6 @@ let (in_module,out_module) = subst_function = subst_module; classify_function = classify_module } - -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 = compute_visibility exists what i dir dirinfo 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 - | [] -> let subst = update_subst subst' (map_mp mp' mp) in - Some (subst_objects (dir,(mp',empty_dirpath)) - (join (join subst' 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 } - - - - let cache_keep _ = anomaly "This module should not be cached!" let load_keep i ((sp,kn),seg) = @@ -553,9 +323,9 @@ let open_modtype i ((sp,kn),(entry,_)) = Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) -let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) = +let subst_modtype (subst,(entry,(mbids,mp,objs))) = check_empty "subst_modtype" entry; - (entry,(join subs subst,mbids,msid,objs)) + (entry,(mbids,subst_mp subst mp,subst_objects subst objs)) let classify_modtype (_,substobjs) = @@ -571,147 +341,143 @@ let (in_modtype,_) = classify_function = classify_modtype } - -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 +let rec replace_module_object idl ( mbids, mp, lib_stack) (mbids2,mp2,objs) mp1= + if mbids<>[] then error "Unexpected functor objects" - else - let rec replace_idl = function - | _,[] -> [] - | id::idl,(id',obj)::tail when id = id' -> - let tag = object_tag obj in - if tag = "MODULE" or tag ="MODULE ALIAS" then - (match idl with - [] -> (id, in_module_alias (Some - ({mod_entry_type = None; - mod_entry_expr = Some (MSEident mp)},None) - ,modobjs,None))::tail - | _ -> - let (a,substobjs,_) = if tag = "MODULE ALIAS" then - out_module_alias obj else out_module obj in - let substobjs' = replace_module_object idl substobjs modobjs mp in - if tag = "MODULE ALIAS" then - (id, in_module_alias (a,substobjs',None))::tail - else - (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 env = function - MSEident ln -> MPmap.find ln !modtypetab + 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,(mbids,(MPdot(mp,label_of_id id)),subst_objects + (map_mp mp1 (MPdot(mp,label_of_id id)) empty_delta_resolver) objs)))::tail + | _ -> + let (_,substobjs) = out_module obj in + let substobjs' = replace_module_object idl substobjs + (mbids2,mp2,objs) mp in + (id, in_module (None,substobjs'))::tail + ) + else error "MODULE expected!" + | 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 + | _ -> (*case mp is a functor *) + None + +(* 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 get_modtype_substobjs env mp_from= 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) - | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty - | MSEwith (mty, With_Module (idl,mp)) -> - let substobjs = get_modtype_substobjs env mty in - let mp = Environ.scrape_alias mp env in - let modobjs = MPmap.find mp !modtab_substobjs in - 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 (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 - 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 - (* application outside the kernel, only for substitutive - objects (that are all non-logical objects) *) - ((join - (join subst sub3) - (map_mbid mbid mp (Some resolve))) - , mbids, msid, objs) - | [] -> match mexpr with - | MSEident _ -> error "Application of a non-functor" - | _ -> error "Application of a functor with too few arguments") + let (mbids, mp, objs) = get_modtype_substobjs env mp_from mte in + (mbid::mbids, mp, objs) + | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mp_from mty + | MSEwith (mty, With_Module (idl,mp1)) -> + let substobjs = get_modtype_substobjs env mp_from mty in + let modobjs = MPmap.find mp1 !modtab_substobjs in + replace_module_object idl substobjs modobjs mp1 + | MSEapply (fexpr, MSEident mp) -> + let (mbids, mp1, objs),mtb_mp1,mp_l = + get_objs_modtype_application env (MSEapply(fexpr, MSEident mp)) in + let rec compute_subst mbids sign mp_l = + match mbids,mp_l with + [],[] -> [],empty_subst + | mbid,[] -> mbid,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 mp_delta = discr_resolver mb in + let mbid_left,subst=compute_subst mbids fbody_b mp_l in + if mp_delta = None then + mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst + else + let mp_delta = Modops.complete_inline_delta_resolver env mp + farg_id farg_b (Option.get mp_delta) in + mbid_left,join (map_mbid mbid mp mp_delta) subst + in + let mbids_left,subst = compute_subst mbids mtb_mp1.typ_expr (List.rev mp_l) in + (mbids_left, mp1,subst_objects subst objs) | 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 (Global.env()) mty in - ignore (do_load_and_subst_module 1 dir mp substobjs []) - in - List.iter2 process_arg argids args - + let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mp 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 [] + in + List.iter2 process_arg argids args + 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 (Global.env()) mty in + let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env()) + (MPbound (List.hd mbids)) mty in List.map2 (fun dir mbid -> - Global.add_module_parameter mbid mty; - let mp = MPbound mbid in - ignore (do_load_and_subst_module 1 dir mp substobjs []); - (mbid,mty)) + let resolver = Global.add_module_parameter mbid mty 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)) dirs mbids let start_module interp_modtype export id args res_o = let fs = Summary.freeze_summaries () in - let mp = Global.start_module id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in - let res_entry_o, sub_body_o = match res_o with None -> None, None | Some (res, restricted) -> (* we translate the module here to catch errors as early as possible *) let mte = interp_modtype (Global.env()) res in - if restricted then - Some mte, None - else - 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,sub = Mod_typing.translate_struct_entry (Global.env()) arg_t + if restricted then + let _ = Mod_typing.translate_struct_type_entry (Global.env()) mte in + Some mte, None + else + let mtb = Mod_typing.translate_module_type (Global.env()) + mp mte in + let funct_mtb = + List.fold_right + (fun (arg_id,arg_t) mte -> + let arg_t = Mod_typing.translate_module_type (Global.env()) + (MPbound arg_id) 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 + arg_entries mtb.typ_expr + in + None, Some {mtb with + typ_expr = funct_mtb} in let mbids = List.map fst arg_entries in - openmod_info:=(mbids,res_entry_o,sub_body_o); + openmod_info:=(mp,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 (); mp @@ -720,24 +486,25 @@ let start_module interp_modtype export id args res_o = let end_module () = let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in - let mbids, res_o, sub_o = !openmod_info in + let mp,mbids, res_o, sub_o = !openmod_info in let substitute, keep, special = Lib.classify_segment lib_stack in - let dir = fst oldprefix in - let msid = msid_of_prefix oldprefix in - - let substobjs, keep, special = try + let mp_from,substobjs, keep, special = try match res_o with | None -> - (empty_subst, mbids, msid, substitute), keep, special - | Some (MSEident ln) -> - abstract_substobjs mbids (MPmap.find ln (!modtypetab)), [], [] + (* the module is not sealed *) + None,( mbids, mp, substitute), keep, special + | Some (MSEident ln as mty) -> + let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in + Some mp1,(mbids@mbids1,mp1,objs), [], [] | Some (MSEwith _ as mty) -> - abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] + let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in + Some mp1,(mbids@mbids1,mp1,objs), [], [] | Some (MSEfunctor _) -> anomaly "Funsig cannot be here..." | Some (MSEapply _ as mty) -> - abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] + let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in + Some mp1,(mbids@mbids1,mp1,objs), [], [] with Not_found -> anomaly "Module objects not found..." in @@ -745,15 +512,21 @@ let end_module () = dependencies on functor arguments *) let id = basename (fst oldoname) in - let mp = Global.end_module fs id res_o in + let mp,resolver = Global.end_module fs id res_o in begin match sub_o with None -> () | Some sub_mtb -> check_subtypes mp sub_mtb end; - let substituted = subst_substobjs dir mp substobjs in - let node = in_module (None,substobjs,substituted) in +(* 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 (None,substobjs) in let objects = if keep = [] || mbids <> [] then special@[node] (* no keep objects or we are defining a functor *) @@ -785,28 +558,30 @@ type library_name = dir_path (* The first two will form substitutive_objects, the last one is keep *) type library_objects = - mod_self_id * lib_objects * lib_objects + module_path * lib_objects * lib_objects let register_library dir cenv objs digest = let mp = MPfile dir in - try + let substobjs, keep = + try ignore(Global.lookup_module mp); (* if it's in the environment, the cached objects should be correct *) - let substobjs, objects = Dirmap.find dir !library_cache in - do_module false "register_library" load_objects 1 dir mp substobjs objects + Dirmap.find dir !library_cache with Not_found -> if mp <> Global.import cenv digest then anomaly "Unexpected disk module name"; - let msid,substitute,keep = objs in - let substobjs = empty_subst, [], msid, substitute in - let objects = do_load_and_subst_module 1 dir mp substobjs keep in - let modobjs = substobjs, objects in - library_cache := Dirmap.add dir modobjs !library_cache + let mp,substitute,keep = objs in + let substobjs = [], mp, substitute in + let modobjs = substobjs, keep in + library_cache := Dirmap.add dir modobjs !library_cache; + modobjs + in + do_module false "register_library" load_objects 1 dir mp substobjs keep let start_library dir = let mp = Global.start_library dir in - openmod_info:=[],None,None; + openmod_info:=mp,[],None,None; Lib.start_compilation dir mp; Lib.add_frozen_state () @@ -816,10 +591,9 @@ let set_end_library_hook f = end_library_hook := f let end_library dir = !end_library_hook(); let prefix, lib_stack = Lib.end_compilation dir in - let cenv = Global.export dir in - let msid = msid_of_prefix prefix in + let mp,cenv = Global.export dir in let substitute, keep, _ = Lib.classify_segment lib_stack in - cenv,(msid,substitute,keep) + cenv,(mp,substitute,keep) (* implementation of Export M and Import M *) @@ -838,8 +612,8 @@ let cache_import (_,(_,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 +let subst_import (subst,(export,mp as obj)) = + let mp' = subst_mp subst mp in if mp'==mp then obj else (export,mp') @@ -870,27 +644,23 @@ let start_modtype interp_modtype id args = 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 msid = msid_of_prefix prefix in let mbids = !openmodtype_info in - let modtypeobjs = empty_subst, mbids, msid, substitute in - - let ln = Global.end_modtype fs id in + let mp = Global.end_modtype fs id in + let modtypeobjs = mbids, mp, substitute in let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in if fst oname <> fst oldoname then anomaly "Section paths generated on start_ and end_modtype do not match"; - if (mp_of_kn (snd oname)) <> ln then + if (mp_of_kn (snd oname)) <> mp then anomaly "Kernel and Library names do not match"; Lib.add_frozen_state ()(* to prevent recaching *); - ln + mp let declare_modtype interp_modtype id args mty = @@ -907,64 +677,79 @@ let declare_modtype interp_modtype id args mty = arg_entries base_mty 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; + let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp entry in + (* Undo the simulated interactive building of the module type *) + (* and declare the module type as a whole *) - ignore (add_leaf id (in_modtype (Some entry, substobjs))); - mmp + let substobjs = (mbids,mmp, + subst_objects (map_mp mp_from mmp empty_delta_resolver) objs) in + Summary.unfreeze_summaries fs; + ignore (add_leaf id (in_modtype (Some entry, substobjs))); + mmp with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e +(* 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 = function + +let rec get_module_substobjs env mp_from = function | 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) - | 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 (subst, mbids, msid, objs) = get_module_substobjs env mexpr in + let (mbids, mp, objs) = get_module_substobjs env mp_from mexpr in + (mbid::mbids, mp, objs) + | MSEapply (fexpr, MSEident mp) -> + let (mbids, mp1, objs),mb_mp1,mp_l = + get_objs_module_application env (MSEapply(fexpr, MSEident mp)) in + let rec compute_subst mbids sign mp_l = + match mbids,mp_l with + [],[] -> [],empty_subst + | mbid,[] -> mbid,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 mp_delta = discr_resolver mb in + let mbid_left,subst=compute_subst mbids fbody_b mp_l in + if mp_delta = None then + mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst + else + let mp_delta = Modops.complete_inline_delta_resolver env mp + farg_id farg_b (Option.get mp_delta) in + mbid_left,join (map_mbid mbid mp mp_delta) subst + in + let mbids_left,subst = compute_subst mbids mb_mp1.mod_type (List.rev mp_l) in + (mbids_left, mp1,subst_objects subst objs) + (* let sign,alg,equiv,_ = Mod_typing.translate_struct_module_entry env mp_from fexpr in + let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in + let mb = Environ.lookup_module mp env in + let mp_delta = discr_resolver mb in + let (mbids, mp1, objs) = get_module_substobjs env mp_from fexpr in (match mbids with | mbid::mbids -> - let resolve = - Modops.resolver_of_environment farg_id farg_b mp sub_alias env 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 - (* application outside the kernel, only for substitutive - objects (that are all non-logical objects) *) - ((join - (join subst sub3) - (map_mbid mbid mp (Some resolve))) - , mbids, msid, objs) - | [] -> match mexpr with + if mp_delta = None then + (mbids, mp1,subst_objects (map_mbid mbid mp empty_delta_resolver) objs) + else + let mp_delta = Modops.complete_inline_delta_resolver env mp + farg_id farg_b (Option.get mp_delta) in + (mbids, mp1,subst_objects (map_mbid mbid mp mp_delta) objs) + | [] -> match fexpr with | MSEident _ -> error "Application of a non-functor." - | _ -> error "Application of a functor with too few arguments.") + | _ -> error "Application of a functor with too few arguments.")*) | 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 + | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from mty + | MSEwith (mty, With_Module (idl,mp)) -> assert false + (* Include *) @@ -991,46 +776,32 @@ let lift_oname (sp,kn) = let dir,_ = Libnames.repr_path sp in (dir,mp) -let cache_include (oname,((me,is_mod),substobjs,substituted)) = +let cache_include (oname,((me,is_mod),(mbis,mp1,objs))) = 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)) = + load_objects 1 prefix objs; + open_objects 1 prefix objs + +let load_include i (oname,((me,is_mod),(mbis,mp1,objs))) = 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)) = + load_objects i prefix objs + + +let open_include i (oname,((me,is_mod),(mbis,mp1,objs))) = 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) + if is_mod || i = 1 then + open_objects i prefix objs + else () + +let subst_include (subst,((me,is_mod),substobj)) = + let (mbids,mp,objs) = substobj in + let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in + ((subst_inc_expr subst me,is_mod),substobjs) + +let classify_include ((me,is_mod),substobjs) = + Substitute ((me,is_mod),substobjs) let (in_include,out_include) = declare_object {(default_object "INCLUDE") with @@ -1040,20 +811,19 @@ let (in_include,out_include) = subst_function = subst_include; classify_function = classify_include } -let rec update_include (sub,mbids,msid,objs) = +let rec update_include (mbids,mp,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 + let ((me,is_mod),substobjs) = out_include obj in let substobjs' = update_include substobjs in - (id, in_include ((me,true),substobjs',substituted)):: + (id, in_include ((me,true),substobjs')):: (replace_include tail) else (id,obj)::(replace_include tail) in - (sub,mbids,msid,replace_include objs) - + (mbids,mp,replace_include objs) let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = @@ -1084,8 +854,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = Some (List.fold_right (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me)) arg_entries - (interp_modexpr (Global.env()) mexpr)) - in + (interp_modexpr (Global.env()) mexpr)) in let entry = {mod_entry_type = mty_entry_o; mod_entry_expr = mexpr_entry_o } @@ -1093,45 +862,33 @@ 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 env mte - | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr + | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp mte + | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp mexpr | _ -> anomaly "declare_module: No type, no body ..." in - let substobjs = update_include substobjs in + let (mbids,mp_from,objs) = 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' = join_alias (subst_key (map_msid msid mp) sub) (map_msid msid mp) in - let substobjs = ( 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 -> + let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let mp_env,resolver = Global.add_module id entry in + let _ = if mp_env <> mp then + anomaly "Kernel and Library names do not match"; + match mty_sub_o with + | None -> () + | Some sub_mte -> + let sub_mtb = Mod_typing.translate_module_type + env mp sub_mte in + check_subtypes mp_env sub_mtb + in + let substobjs = (mbids,mp_env, + subst_objects(map_mp mp_from mp_env resolver) objs) in + ignore (add_leaf + id + (in_module (Some (entry, mty_sub_o), substobjs))); + mmp + + with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e @@ -1142,19 +899,19 @@ let declare_include interp_struct me_ast is_mod = try let env = Global.env() in - let me = interp_struct env me_ast in - let substobjs = + let me = interp_struct env me_ast in + let mp1,_ = current_prefix () in + let (mbids,mp,objs)= if is_mod then - get_module_substobjs env me + get_module_substobjs env mp1 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 + get_modtype_substobjs env mp1 me in let id = current_mod_id() in - + let resolver = Global.add_include me is_mod in + let substobjs = (mbids,mp1, + subst_objects (map_mp mp mp1 resolver) objs) in ignore (add_leaf id - (in_include ((me,is_mod), substobjs, substituted))) + (in_include ((me,is_mod), substobjs))) with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e |