From 2ddd0afea124874576b1468c3ce5830352be4322 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 18 Nov 2009 00:03:14 +0000 Subject: Module subtyping : allow many <: and module type declaration with <: Any place where <: was legal can now contain many <: declarations. Moreover we can say that the module type we are declaring is a subtype of an earlier module type. See DecidableType2 for examples. Also try to handle correctly the freeze/unfreeze summaries when simulating start/include/end (syntax ... := ... <+ ...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12532 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.ml | 320 +++++++++++++++++++++++++------------------------ 1 file changed, 165 insertions(+), 155 deletions(-) (limited to 'library/declaremods.ml') diff --git a/library/declaremods.ml b/library/declaremods.ml index 42d3652aa..0ed617a0b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -77,10 +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 ((MPfile(initial_dir),[],None,None) - : module_path * mod_bound_id list * module_struct_entry option - * module_type_body option) +let openmod_info = + ref ((MPfile(initial_dir),[],None,[]) + : module_path * mod_bound_id list * module_struct_entry option + * module_type_body list) (* The library_cache here is needed to avoid recalculations of substituted modules object during "reloading" of libraries *) @@ -101,7 +101,7 @@ let _ = Summary.declare_summary "MODULE-INFO" modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; openmod_info := ((MPfile(initial_dir), - [],None,None)); + [],None,[])); library_cache := Dirmap.empty) } (* auxiliary functions to transform full_path and kernel_name given @@ -118,17 +118,58 @@ let dir_of_sp sp = let dir,id = repr_path sp in add_dirpath_suffix dir id +(* Subtyping checks *) + +let check_sub mtb sub_mtb_l = + (* The constraints are checked and forgot immediately : *) + ignore (List.fold_right + (fun sub_mtb env -> + Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) env) + sub_mtb_l (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 = + a subtype of all signatures in [sub_mtb_l]. Uses only the global + environment. *) + +let check_subtypes mp sub_mtb_l = let env = Global.env () in 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! *) + check_sub mtb sub_mtb_l + +(* Same for module type [mp] *) + +let check_subtypes_mt mp sub_mtb_l = + check_sub (Environ.lookup_modtype mp (Global.env())) sub_mtb_l + +(* Create a functor type entry *) + +let funct_entry args m = + List.fold_right + (fun (arg_id,arg_t) mte -> MSEfunctor (arg_id,arg_t,mte)) + args m + +(* Prepare the module type list for check of subtypes *) + +let build_subtypes interp_modtype mp args mtys = + List.map + (fun m -> + let mte = interp_modtype (Global.env()) m in + 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 + SEBfunctor(arg_id,arg_t,mte)) + args mtb.typ_expr + in + { mtb with typ_expr = funct_mtb }) + mtys + (* These functions register the visibility of the module and iterates through its components. They are called by plenty module functions *) @@ -266,7 +307,7 @@ let modtypetab = (* currently started interactive module type. We remember its arguments if it is a functor type *) let openmodtype_info = - ref ([] : mod_bound_id list) + ref ([],[] : mod_bound_id list * module_type_body list) let _ = Summary.declare_summary "MODTYPE-INFO" { Summary.freeze_function = (fun () -> @@ -276,30 +317,35 @@ let _ = Summary.declare_summary "MODTYPE-INFO" openmodtype_info := snd ft); Summary.init_function = (fun () -> modtypetab := MPmap.empty; - openmodtype_info := []) } + openmodtype_info := [],[]) } + +let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = + let mp = mp_of_kn kn in -let cache_modtype ((sp,kn),(entry,modtypeobjs)) = let _ = match entry with | None -> anomaly "You must not recache interactive module types!" | Some mte -> - let mp = Global.add_modtype (basename sp) mte in - if mp <>mp_of_kn kn then + if mp <> Global.add_modtype (basename sp) mte then anomaly "Kernel and Library names do not match" in + (* Using declare_modtype should lead here, where we check + that any given subtyping is indeed accurate *) + check_subtypes_mt mp sub_mty_l; + if Nametab.exists_modtype sp then errorlabstrm "cache_modtype" (pr_path sp ++ str " already exists") ; - Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn); + Nametab.push_modtype (Nametab.Until 1) sp mp; - modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab + modtypetab := MPmap.add mp modtypeobjs !modtypetab -let load_modtype i ((sp,kn),(entry,modtypeobjs)) = +let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) = check_empty "load_modtype" entry; if Nametab.exists_modtype sp then @@ -311,7 +357,7 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) = modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab -let open_modtype i ((sp,kn),(entry,_)) = +let open_modtype i ((sp,kn),(entry,_,_)) = check_empty "open_modtype" entry; if @@ -323,13 +369,13 @@ let open_modtype i ((sp,kn),(entry,_)) = Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) -let subst_modtype (subst,(entry,(mbids,mp,objs))) = +let subst_modtype (subst,(entry,(mbids,mp,objs),_)) = check_empty "subst_modtype" entry; - (entry,(mbids,subst_mp subst mp,subst_objects subst objs)) + (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[]) -let classify_modtype (_,substobjs) = - Substitute (None,substobjs) +let classify_modtype (_,substobjs,_) = + Substitute (None,substobjs,[]) let (in_modtype,_) = @@ -448,36 +494,19 @@ let intern_args interp_modtype (idl,arg) = (mbid,mty)) dirs mbids -let start_module interp_modtype export id args res_o = - let fs = Summary.freeze_summaries () in +let start_module_ interp_modtype export id args res fs = 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 res_entry_o, sub_body_l = match res with + | Topconstr.Enforce res -> let mte = interp_modtype (Global.env()) res in - 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 - SEBfunctor(arg_id,arg_t,mte)) - arg_entries mtb.typ_expr - in - None, Some {mtb with - typ_expr = funct_mtb} + let _ = Mod_typing.translate_struct_type_entry (Global.env()) mte in + Some mte, [] + | Topconstr.Check resl -> + None, build_subtypes interp_modtype mp arg_entries resl in - let mbids = List.map fst arg_entries in - openmod_info:=(mp,mbids,res_entry_o,sub_body_o); + openmod_info:=(mp,mbids,res_entry_o,sub_body_l); 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 @@ -486,7 +515,7 @@ let start_module interp_modtype export id args res_o = let end_module () = let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in - let mp,mbids, res_o, sub_o = !openmod_info in + let mp,mbids, res_o, sub_l = !openmod_info in let substitute, keep, special = Lib.classify_segment lib_stack in let mp_from,substobjs, keep, special = try @@ -514,10 +543,7 @@ let end_module () = let id = basename (fst oldoname) 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; + check_subtypes mp sub_l; (* we substitute objects if the module is sealed by a signature (ie. mp_from != None *) @@ -581,7 +607,7 @@ let register_library dir cenv objs digest = let start_library dir = let mp = Global.start_library dir in - openmod_info:=mp,[],None,None; + openmod_info:=mp,[],None,[]; Lib.start_compilation dir mp; Lib.add_frozen_state () @@ -630,14 +656,13 @@ let import_module export mp = (************************************************************************) (* module types *) -let start_modtype interp_modtype id args = - let fs = Summary.freeze_summaries () in +let start_modtype_ interp_modtype id args mtys fs = let mp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in - + let sub_mty_l = build_subtypes interp_modtype mp arg_entries mtys in let mbids = List.map fst arg_entries in - openmodtype_info := mbids; + openmodtype_info := mbids, sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); Lib.add_frozen_state (); mp @@ -647,11 +672,12 @@ 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 mbids = !openmodtype_info in + let mbids, sub_mty_l = !openmodtype_info 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 - + let modtypeobjs = mbids, mp, substitute in + check_subtypes_mt mp sub_mty_l; + 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"; @@ -663,32 +689,23 @@ let end_modtype () = mp -let declare_modtype_real interp_modtype id args mty = - let fs = Summary.freeze_summaries () in - - try +let declare_modtype_ interp_modtype id args mtys mty fs = 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 -> MSEfunctor(arg_id,arg_t,mte)) - arg_entries - base_mty - in + let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in + (* NB: check of subtyping will be done in cache_modtype *) + let sub_mty_l = build_subtypes interp_modtype mmp arg_entries mtys in 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 *) + (* Undo the simulated interactive building of the module type *) + (* and declare the module type as a whole *) 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 + 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, sub_mty_l))); + mmp + (* Small function to avoid module typing during substobjs retrivial *) let rec get_objs_module_application env = function @@ -824,36 +841,16 @@ let rec update_include (mbids,mp,objs) = in (mbids,mp,replace_include objs) -let declare_module_real interp_modtype interp_modexpr id args mty_o mexpr_o = - - let fs = Summary.freeze_summaries () in - - try +let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = 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 -> MSEfunctor(arg_id,arg_t,mte)) - arg_entries - (interp_modtype (Global.env()) mty)), - None - | (Some (mty, false)) -> - None, - Some (List.fold_right - (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) - arg_entries - (interp_modtype (Global.env()) mty)) + let funct f m = funct_entry arg_entries (f (Global.env ()) m) in + let mty_entry_o, mty_sub_l = match res with + | Topconstr.Enforce mty -> Some (funct interp_modtype mty), [] + | Topconstr.Check mtys -> None, List.map (funct interp_modtype) mtys in - let mexpr_entry_o = match mexpr_o with - None -> None - | Some mexpr -> - Some (List.fold_right - (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me)) - arg_entries - (interp_modexpr (Global.env()) mexpr)) in + let mexpr_entry_o = Option.map (funct interp_modexpr) mexpr_o in let entry = {mod_entry_type = mty_entry_o; mod_entry_expr = mexpr_entry_o } @@ -866,30 +863,23 @@ let declare_module_real interp_modtype interp_modexpr id args mty_o mexpr_o = | _ -> anomaly "declare_module: No type, no body ..." 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; - 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 + (* 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 mp_env,resolver = Global.add_module id entry in + + if mp_env <> mp then anomaly "Kernel and Library names do not match"; + + let subs = List.map (Mod_typing.translate_module_type env mp) mty_sub_l in + check_subtypes mp subs; + + let substobjs = (mbids,mp_env, + subst_objects(map_mp mp_from mp_env resolver) objs) in + ignore (add_leaf + id + (in_module (Some (entry), substobjs))); + mmp let declare_one_include interp_struct me_ast is_mod is_self = @@ -937,33 +927,53 @@ let declare_one_include interp_struct me_ast is_mod is_self = (in_include ((me,is_mod), substobjs))) -let declare_include interp_struct me_ast me_asts is_mod is_self = +let declare_include_ interp_struct me_ast me_asts is_mod is_self = + declare_one_include interp_struct me_ast is_mod is_self; + List.iter + (fun me -> declare_one_include interp_struct me is_mod true) + me_asts + +(** Versions of earlier functions taking care of the freeze/unfreeze + of summaries *) + +let protect_summaries f = let fs = Summary.freeze_summaries () in - try - declare_one_include interp_struct me_ast is_mod is_self; - List.iter - (fun me -> declare_one_include interp_struct me is_mod true) - me_asts + try f fs with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e +let declare_include interp_struct me_ast me_asts is_mod is_self = + protect_summaries + (fun _ -> declare_include_ interp_struct me_ast me_asts is_mod is_self) + +let declare_modtype interp_mt id args mtys mty_l = + let declare_mt fs = match mty_l with + | [] -> assert false + | [mty] -> declare_modtype_ interp_mt id args mtys mty fs + | mty :: mty_l -> + ignore (start_modtype_ interp_mt id args mtys fs); + declare_include_ interp_mt mty mty_l false false; + end_modtype () + in + protect_summaries declare_mt + +let start_modtype interp_modtype id args mtys = + protect_summaries (start_modtype_ interp_modtype id args mtys) + +let declare_module interp_mt interp_me id args mtys me_l = + let declare_me fs = match me_l with + | [] -> declare_module_ interp_mt interp_me id args mtys None fs + | [me] -> declare_module_ interp_mt interp_me id args mtys (Some me) fs + | me :: me_l -> + ignore (start_module_ interp_mt None id args mtys fs); + declare_include_ interp_me me me_l true false; + end_module () + in + protect_summaries declare_me -let declare_modtype interp_mt id args = function - | [] -> assert false - | [mty] -> declare_modtype_real interp_mt id args mty - | mty :: mty_l -> - ignore (start_modtype interp_mt id args); - declare_include interp_mt mty mty_l false false; - end_modtype () - -let declare_module interp_mt interp_me id args mty_o = function - | [] -> declare_module_real interp_mt interp_me id args mty_o None - | [me] -> declare_module_real interp_mt interp_me id args mty_o (Some me) - | me :: me_l -> - ignore (start_module interp_mt None id args mty_o); - declare_include interp_me me me_l true false; - end_module () +let start_module interp_modtype export id args res = + protect_summaries (start_module_ interp_modtype export id args res) (*s Iterators. *) -- cgit v1.2.3