From 7acb63cad5f92c2618f99ca2a812a465092a523f Mon Sep 17 00:00:00 2001 From: soubiran Date: Fri, 1 Feb 2008 12:18:37 +0000 Subject: Beaoucoup de changements dans la representation interne des modules. kernel: -declaration.ml unification des representations pour les modules et modules types. (type struct_expr_body) -mod_typing.ml le typage des modules est separe de l'evaluation des modules -modops.ml nouvelle fonction qui pour toutes expressions de structure calcule sa forme evaluee.(eval_struct) -safe_typing.ml ajout du support du nouvel operateur Include.(add_include). library: -declaremods.ml nouveaux objets Include et Module-alias et gestion de la resolution de noms pour les alias via la nametab. parsing: -g_vernac.ml4: nouvelles regles pour le support des Includes et pour l'application des signatures fonctorielles. extraction: Adaptation a la nouvelle representation des modules et support de l'operateur with. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.ml | 411 ++++++++++++++++++++++++++++++++++++++---------- library/declaremods.mli | 15 +- library/global.ml | 2 + library/global.mli | 11 +- library/lib.ml | 22 ++- library/lib.mli | 3 +- library/nametab.ml | 16 +- library/nametab.mli | 6 +- 8 files changed, 382 insertions(+), 104 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index 29e8012fe..8cfd7e1ae 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -78,8 +78,8 @@ 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) let _ = Summary.declare_summary "MODULE-INFO" { Summary.freeze_function = (fun () -> @@ -122,23 +122,19 @@ 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) - | MTEfunsig _ -> Modops.error_result_must_be_signature () - | MTEwith (mte,_) -> check_sig_entry env mte +let rec scrape_alias mp = + match (Environ.lookup_module mp + (Global.env())) with + | {mod_expr = Some (SEBident mp1); + mod_type = None} -> scrape_alias mp1 + | _ -> mp + (* 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 = Modops.eval_struct env (SEBident mp) in let _ = Environ.add_constraints (Subtyping.check_subtypes env mtb sub_mtb) in @@ -176,6 +172,35 @@ let do_module exists what iter_objects i dir mp substobjs objects = | None -> () + +let do_module_alias exists what iter_objects i dir mp alias substobjs objects = + let prefix = (dir,(alias,empty_dirpath)) 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 objects with + Some seg -> + modtab_objects := MPmap.add mp (prefix,seg) !modtab_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 @@ -193,7 +218,8 @@ 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 @@ -203,12 +229,40 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = match sub_mtb_o with None -> () | Some sub_mtb -> -check_subtypes mp sub_mtb + check_subtypes mp sub_mtb in conv_names_do_module false "cache" load_objects 1 oname substobjs substituted +let 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' = Global.add_module (basename sp) me 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 -> + 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 + + (* TODO: This check is not essential *) let check_empty s = function | None -> () @@ -224,12 +278,40 @@ let load_module i (oname,(entry,substobjs,substituted)) = check_empty "load_module" entry; conv_names_do_module false "load" load_objects i oname substobjs substituted +let 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 "tata" + end + | None -> anomaly "toujours" + in + do_module_alias false "load" load_objects i dir mp alias substobjs substituted let open_module i (oname,(entry,substobjs,substituted)) = (* TODO: This check is not essential *) check_empty "open_module" entry; conv_names_do_module true "open" open_objects i oname substobjs substituted +let 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 "tata" + end + | None -> anomaly "toujours" + in + do_module_alias true "open" open_objects i dir mp alias substobjs substituted let subst_substobjs dir mp (subst,mbids,msid,objs) = match mbids with @@ -252,10 +334,36 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) = in (None,substobjs,substituted) +let 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 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 + match entry with + | Some (me,sub)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + (Some ({mod_entry_type = None; + mod_entry_expr = + Some (MSEident (subst_mp subst' mp))},sub), + substobjs,substituted) + + | _ -> anomaly "tata" + end + | None -> anomaly "toujours" let classify_module (_,(_,substobjs,_)) = Substitute (None,substobjs,None) +let classify_module_alias (_,(entry,substobjs,_)) = + Substitute (entry,substobjs,None) + let (in_module,out_module) = declare_object {(default_object "MODULE") with cache_function = cache_module; @@ -265,6 +373,14 @@ let (in_module,out_module) = classify_function = classify_module; export_function = (fun _ -> anomaly "No modules in sections!") } +let (in_module_alias,out_module_alias) = + declare_object {(default_object "MODULE ALIAS") with + cache_function = cache_module_alias; + load_function = load_module_alias; + open_function = open_module_alias; + subst_function = subst_module_alias; + classify_function = classify_module_alias; + export_function = (fun _ -> anomaly "No modules in sections!") } let cache_keep _ = anomaly "This module should not be cached!" @@ -298,7 +414,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 +428,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 +449,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 +461,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; @@ -385,7 +498,7 @@ let (in_modtype,out_modtype) = -let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs = +let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp = if mbids<>[] then error "Unexpected functor objects" else @@ -394,10 +507,13 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs = | id::idl,(id',obj)::tail when id = id' -> if object_tag obj = "MODULE" then (match idl with - [] -> (id, in_module (None,modobjs,None))::tail + [] -> (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 in + let substobjs' = replace_module_object idl substobjs modobjs mp in (id, in_module (None,substobjs',None))::tail ) else error "MODULE expected!" @@ -408,17 +524,34 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs = 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 + replace_module_object idl substobjs modobjs mp + | MSEapply (mexpr, MSEident mp) -> + let ftb = 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 (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 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) + | [] -> 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 *) @@ -426,13 +559,14 @@ 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 - +(* Dead code *) +(* let replace_module mtb id mb = todo "replace module after with"; mtb let rec get_some_body mty env = match mty with @@ -441,14 +575,15 @@ let rec get_some_body mty env = match mty with | 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) - +*) +(* Dead code *) 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; @@ -457,7 +592,6 @@ let intern_args interp_modtype (idl,arg) = do_module false "interp" load_objects 1 dir mp substobjs substituted; (mbid,mty)) dirs mbids - let start_module interp_modtype export id args res_o = let fs = Summary.freeze_summaries () in @@ -469,23 +603,22 @@ 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 = Mod_typing.translate_struct_entry (Global.env()) arg_t + 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 () @@ -511,12 +644,14 @@ 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 (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..." + | Some (MSEapply _ as mty) -> + abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] with Not_found -> anomaly "Module objects not found..." in @@ -636,7 +771,6 @@ let import_module export mp = (************************************************************************) (* module types *) - let start_modtype interp_modtype id args = let fs = Summary.freeze_summaries () in @@ -667,7 +801,7 @@ 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"; @@ -684,11 +818,11 @@ let declare_modtype interp_modtype id args mty = 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; @@ -700,14 +834,14 @@ let declare_modtype interp_modtype id args mty = 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) - | 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 = 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 (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (match mbids with | mbid::mbids -> @@ -717,11 +851,15 @@ let rec get_module_substobjs env = function objects (that are all non-logical objects) *) (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs) | [] -> match mexpr with - | MEident _ -> 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 let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = @@ -735,14 +873,14 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = 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 +888,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,29 +899,136 @@ 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 - (* Undo the simulated interactive building of the module *) (* and declare the module as a whole *) Summary.unfreeze_summaries fs; - - 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))) - + 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 substituted = subst_substobjs dir mp substobjs 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 = + 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 -> + if is_mod then + load_objects i prefix seg + else + if i = 1 then + load_objects i prefix seg + | None -> () -(*s Iterators. *) +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 declare_include interp_struct me_ast is_mod = + + 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 diff --git a/library/declaremods.mli b/library/declaremods.mli index 2a491b4a6..717fddf79 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -37,12 +37,12 @@ open Lib *) val declare_module : - (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) -> + (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> 'modexpr option -> unit -val start_module : (env -> 'modtype -> module_type_entry) -> +val start_module : (env -> 'modtype -> module_struct_entry) -> bool option -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> unit @@ -52,10 +52,10 @@ val end_module : identifier -> unit (*s Module types *) -val declare_modtype : (env -> 'modtype -> module_type_entry) -> +val declare_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit -val start_modtype : (env -> 'modtype -> module_type_entry) -> +val start_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> unit val end_modtype : identifier -> unit @@ -95,6 +95,10 @@ val really_import_module : module_path -> unit val import_module : bool -> module_path -> unit +(* Include *) + +val declare_include : (env -> 'struct_expr -> module_struct_entry) -> + 'struct_expr -> bool -> unit (*s [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented @@ -110,4 +114,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (* For translator *) val process_module_bindings : module_ident list -> - (mod_bound_id * module_type_entry) list -> unit + (mod_bound_id * module_struct_entry) list -> unit + diff --git a/library/global.ml b/library/global.ml index 0ee5533f3..4de4029b2 100644 --- a/library/global.ml +++ b/library/global.ml @@ -73,6 +73,8 @@ let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env +let add_include me = global_env := add_include me !global_env + let start_module id = let l = label_of_id id in let mp,newenv = start_module l !global_env in diff --git a/library/global.mli b/library/global.mli index 8633dba76..71617f5a1 100644 --- a/library/global.mli +++ b/library/global.mli @@ -50,7 +50,7 @@ val add_mind : dir_path -> identifier -> mutual_inductive_entry -> kernel_name val add_module : identifier -> module_entry -> module_path -val add_modtype : identifier -> module_type_entry -> kernel_name +val add_modtype : identifier -> module_struct_entry -> module_path val add_constraints : constraints -> unit @@ -64,13 +64,14 @@ val set_engagement : engagement -> unit of the started module / module type *) val start_module : identifier -> module_path -val end_module : identifier -> module_type_entry option -> module_path +val end_module : identifier -> module_struct_entry option -> module_path -val add_module_parameter : mod_bound_id -> module_type_entry -> unit +val add_module_parameter : mod_bound_id -> module_struct_entry -> unit val start_modtype : identifier -> module_path -val end_modtype : identifier -> kernel_name +val end_modtype : identifier -> module_path +val add_include : module_struct_entry -> unit (* Queries *) val lookup_named : variable -> named_declaration @@ -78,7 +79,7 @@ val lookup_constant : constant -> constant_body val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body val lookup_mind : mutual_inductive -> mutual_inductive_body val lookup_module : module_path -> module_body -val lookup_modtype : kernel_name -> module_type_body +val lookup_modtype : module_path -> module_type_body (* Compiled modules *) val start_library : dir_path -> module_path diff --git a/library/lib.ml b/library/lib.ml index 8fff32e1a..de2047dbd 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -98,11 +98,15 @@ let library_dp () = module path and relative section path *) let path_prefix = ref initial_prefix - let cwd () = fst !path_prefix let make_path id = Libnames.make_path (cwd ()) id +let path_of_include () = + let dir = Names.repr_dirpath (cwd ()) in + let new_dir = List.tl dir in + let id = List.hd dir in + Libnames.make_path (Names.make_dirpath new_dir) id let current_prefix () = snd !path_prefix @@ -236,12 +240,25 @@ let add_frozen_state () = (* Modules. *) + let is_something_opened = function (_,OpenedSection _) -> true | (_,OpenedModule _) -> true | (_,OpenedModtype _) -> true | _ -> false + +let current_mod_id () = + try match find_entry_p is_something_opened with + | oname,OpenedModule (_,_,nametab) -> + basename (fst oname) + | oname,OpenedModtype (_,nametab) -> + basename (fst oname) + | _ -> error "you are not in a module" + with Not_found -> + error "no opened modules" + + let start_module export id mp nametab = let dir = extend_dirpath (fst !path_prefix) id in let prefix = dir,(mp,empty_dirpath) in @@ -586,7 +603,8 @@ let reset_name (loc,id) = let is_mod_node = function | OpenedModule _ | OpenedModtype _ | OpenedSection _ | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true - | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" + | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" + || t = "MODULE ALIAS" | _ -> false (* Reset on a module or section name in order to bypass constants with diff --git a/library/lib.mli b/library/lib.mli index f13ff82ae..570685585 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -88,6 +88,7 @@ val contents_after : object_name option -> library_segment (* User-side names *) val cwd : unit -> dir_path val make_path : identifier -> section_path +val path_of_include : unit -> section_path (* Kernel-side names *) val current_prefix : unit -> module_path * dir_path @@ -101,7 +102,7 @@ val sections_depth : unit -> int (* Are we inside an opened module type *) val is_modtype : unit -> bool val is_module : unit -> bool - +val current_mod_id : unit -> module_ident (* Returns the most recent OpenedThing node *) val what_is_opened : unit -> object_name * node diff --git a/library/nametab.ml b/library/nametab.ml index 9aab07cac..536c9605a 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -263,9 +263,11 @@ type ccitab = extended_global_reference SpTab.t let the_ccitab = ref (SpTab.empty : ccitab) type kntab = kernel_name SpTab.t -let the_modtypetab = ref (SpTab.empty : kntab) let the_tactictab = ref (SpTab.empty : kntab) +type mptab = module_path SpTab.t +let the_modtypetab = ref (SpTab.empty : mptab) + type objtab = unit SpTab.t let the_objtab = ref (SpTab.empty : objtab) @@ -299,8 +301,10 @@ let the_globrevtab = ref (Globrevtab.empty : globrevtab) type mprevtab = dir_path MPmap.t let the_modrevtab = ref (MPmap.empty : mprevtab) +type mptrevtab = section_path MPmap.t +let the_modtyperevtab = ref (MPmap.empty : mptrevtab) + type knrevtab = section_path KNmap.t -let the_modtyperevtab = ref (KNmap.empty : knrevtab) let the_tacticrevtab = ref (KNmap.empty : knrevtab) @@ -328,7 +332,7 @@ let push = push_cci let push_modtype vis sp kn = the_modtypetab := SpTab.push vis sp kn !the_modtypetab; - the_modtyperevtab := KNmap.add kn sp !the_modtyperevtab + the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab (* This is for tactic definition names *) @@ -483,7 +487,7 @@ let shortest_qualid_of_module mp = DirTab.shortest_qualid Idset.empty dir !the_dirtab let shortest_qualid_of_modtype kn = - let sp = KNmap.find kn !the_modtyperevtab in + let sp = MPmap.find kn !the_modtyperevtab in SpTab.shortest_qualid Idset.empty sp !the_modtypetab let shortest_qualid_of_tactic kn = @@ -504,6 +508,7 @@ let inductive_of_reference r = user_err_loc (loc_of_reference r,"global_inductive", pr_reference r ++ spc () ++ str "is not an inductive type") + (********************************************************************) (********************************************************************) @@ -520,10 +525,11 @@ let init () = the_tactictab := SpTab.empty; the_globrevtab := Globrevtab.empty; the_modrevtab := MPmap.empty; - the_modtyperevtab := KNmap.empty; + the_modtyperevtab := MPmap.empty; the_tacticrevtab := KNmap.empty + let freeze () = !the_ccitab, !the_dirtab, diff --git a/library/nametab.mli b/library/nametab.mli index 66de6a708..eab86db1d 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -73,7 +73,7 @@ type visibility = Until of int | Exactly of int val push : visibility -> section_path -> global_reference -> unit val push_syntactic_definition : visibility -> section_path -> kernel_name -> unit -val push_modtype : visibility -> section_path -> kernel_name -> unit +val push_modtype : visibility -> section_path -> module_path -> unit val push_dir : visibility -> dir_path -> global_dir_reference -> unit val push_object : visibility -> section_path -> unit val push_tactic : visibility -> section_path -> kernel_name -> unit @@ -106,7 +106,7 @@ val locate_obj : qualid -> section_path val locate_constant : qualid -> constant val locate_mind : qualid -> mutual_inductive val locate_section : qualid -> dir_path -val locate_modtype : qualid -> kernel_name +val locate_modtype : qualid -> module_path val locate_syntactic_definition : qualid -> kernel_name type ltac_constant = kernel_name @@ -161,7 +161,7 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds Coq.A.B.x that denotes the same object. *) val shortest_qualid_of_module : module_path -> qualid -val shortest_qualid_of_modtype : kernel_name -> qualid +val shortest_qualid_of_modtype : module_path -> qualid (* -- cgit v1.2.3