diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 142 | ||||
| -rw-r--r-- | library/declaremods.mli | 33 | ||||
| -rw-r--r-- | library/library.ml | 6 | ||||
| -rwxr-xr-x | library/nametab.ml | 5 | ||||
| -rwxr-xr-x | library/nametab.mli | 5 |
5 files changed, 151 insertions, 40 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 2be5e8a73c..5dba4c208e 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -77,7 +77,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) : mod_bound_id list * module_type_entry option) + ref (([],None,None) : mod_bound_id list * module_type_entry option + * module_type_body option) let _ = Summary.declare_summary "MODULE-INFO" { Summary.freeze_function = (fun () -> @@ -91,7 +92,7 @@ let _ = Summary.declare_summary "MODULE-INFO" Summary.init_function = (fun () -> modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; - openmod_info := ([],None)); + openmod_info := ([],None,None)); Summary.survive_section = false } (* auxiliary functions to transform section_path and kernel_name given @@ -119,6 +120,18 @@ let msid_of_prefix (_,(mp,sec)) = anomaly ("Non-empty section in module name!" ^ string_of_mp mp ^ "." ^ string_of_dirpath sec) + +(* 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 _ = Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) + in + () (* The constraints are checked and forgot immediately! *) + + (* This function registers the visibility of the module and iterates through its components. It is called by plenty module functions *) @@ -164,10 +177,20 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = let _ = match entry with | None -> anomaly "You must not recache interactive modules!" - | Some me -> + | 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) + 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" + anomaly "Kernel and Library names do not match"; + + match sub_mtb_o with + None -> () + | Some sub_mtb -> check_subtypes mp sub_mtb + in conv_names_do_module false "cache" load_objects 1 oname substobjs substituted @@ -431,12 +454,31 @@ let start_module interp_modtype id args res_o = List.fold_left (intern_args interp_modtype) (env,[]) args in let arg_entries = List.concat (List.rev arg_entries_revlist) in - let res_entry_o = option_app (interp_modtype env) res_o in + + let res_entry_o, sub_body_o = match res_o with + None -> None, None + | Some (res, true) -> + Some (interp_modtype env res), None + | Some (res, false) -> + (* If the module type is non-restricting, we must translate it + here to catch errors as early as possible. If it is + estricting, the kernel takes care of it. *) + let sub_mte = + List.fold_right + (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + arg_entries + (interp_modtype env res) + in + let sub_mtb = + Mod_typing.translate_modtype (Global.env()) sub_mte + in + None, Some sub_mtb + in let mp = Global.start_module id arg_entries res_entry_o in let mbids = List.map fst arg_entries in - openmod_info:=(mbids,res_entry_o); + openmod_info:=(mbids,res_entry_o,sub_body_o); let prefix = Lib.start_module id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); Lib.add_frozen_state () @@ -446,11 +488,17 @@ let end_module id = let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in let mp = Global.end_module id in + let mbids, res_o, sub_o = !openmod_info 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 let msid = msid_of_prefix oldprefix in - let mbids, res_o = !openmod_info in Summary.unfreeze_other_summaries fs; @@ -528,7 +576,7 @@ let register_library dir cenv objs digest = let start_library dir = let mp = Global.start_library dir in - openmod_info:=[],None; + openmod_info:=[],None,None; Lib.start_compilation dir mp; Lib.add_frozen_state () @@ -542,6 +590,33 @@ let export_library dir = +let do_open_export (_,(_,mp)) = +(* for non-substitutive exports: + let mp = Nametab.locate_module (qualid_of_dirpath dir) in *) + let prefix,objects = MPmap.find mp !modtab_objects in + open_objects 1 prefix objects + +let classify_export (_,(export,_ as obj)) = + if export then Substitute obj else Dispose + +let subst_export (_,subst,(export,mp as obj)) = + let mp' = subst_mp subst mp in + if mp'==mp then obj else + (export,mp') + +let (in_export,out_export) = + declare_object {(default_object "EXPORT MODULE") with + cache_function = do_open_export; + open_function = (fun i o -> if i=1 then do_open_export o); + subst_function = subst_export; + classify_function = classify_export } + +let export_module mp = +(* for non-substitutive exports: + let dir = Nametab.dir_of_mp mp in *) + Lib.add_anonymous_leaf (in_export (true,mp)) + + let import_module mp = let prefix,objects = MPmap.find mp !modtab_objects in open_objects 1 prefix objects @@ -638,21 +713,32 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = List.fold_left (intern_args interp_modtype) (env,[]) args in let arg_entries = List.concat (List.rev arg_entries_revlist) in - let mty_entry_o = option_app (interp_modtype env) mty_o in - let mexpr_entry_o = option_app (interp_modexpr env) mexpr_o 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)) + arg_entries + (interp_modtype env mty)), + None + | (Some (mty, false)) -> + None, + Some (List.fold_right + (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + arg_entries + (interp_modtype env mty)) + in + let mexpr_entry_o = match mexpr_o with + None -> None + | Some mexpr -> + Some (List.fold_right + (fun (mbid,mte) me -> MEfunctor(mbid,mte,me)) + arg_entries + (interp_modexpr env mexpr)) + in let entry = - {mod_entry_type = - option_app - (List.fold_right - (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) - arg_entries) - mty_entry_o; - mod_entry_expr = - option_app - (List.fold_right - (fun (mbid,mte) me -> MEfunctor(mbid,mte,me)) - arg_entries) - mexpr_entry_o } + {mod_entry_type = mty_entry_o; + mod_entry_expr = mexpr_entry_o } in let substobjs = match entry with @@ -660,14 +746,14 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr | _ -> anomaly "declare_module: No type, no body ..." in - Summary.unfreeze_summaries fs; + 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 + 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, substobjs, substituted))) + ignore (add_leaf + id + (in_module (Some (entry, mty_sub_o), substobjs, substituted))) (*s Iterators. *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 9edd051cad..114ea3cf9f 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -15,21 +15,36 @@ open Environ open Libnames open Libobject open Lib -(*i*) + (*i*) -(*s This modules provides official fucntions to declare modules and - module types *) +(*s This modules provides official functions to declare modules and + module types *) (*s Modules *) +(* [declare_module interp_modtype interp_modexpr id fargs typ expr] + declares module [id], with type constructed by [interp_modtype] + from functor arguments [fargs] and [typ] and with module body + constructed by [interp_modtype] from functor arguments [fargs] and + by [interp_modexpr] from [expr]. At least one of [typ], [expr] must + be non-empty. + + The [bool] in [typ] tells if the module must be abstracted [true] + with respect to the module type or merely matched without any + restriction [false]. +*) + val declare_module : (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) -> identifier -> - (identifier list * 'modtype) list -> 'modtype option -> 'modexpr option -> unit - -val start_module : (env -> 'modtype -> module_type_entry) -> - identifier -> (identifier list * 'modtype) list -> 'modtype option -> unit + (identifier list * 'modtype) list -> ('modtype * bool) option -> + 'modexpr option -> unit + +val start_module : (env -> 'modtype -> module_type_entry) -> + identifier -> + (identifier list * 'modtype) list -> ('modtype * bool) option -> + unit val end_module : identifier -> unit @@ -74,6 +89,10 @@ val export_library : val import_module : module_path -> unit +(* [export_module mp] is similar, but is run when the module + containing it is imported *) + +val export_module : module_path -> unit (*s [fold_all_segments] and [iter_all_segments] iterate over all segments, the modules' segments first and then the current diff --git a/library/library.ml b/library/library.ml index e7087438b1..1f75b4ca06 100644 --- a/library/library.ml +++ b/library/library.ml @@ -389,7 +389,7 @@ let rec_intern_by_filename_only id f = let locate_qualified_library qid = (* Look if loaded in current environment *) try - let dir = Nametab.locate_loaded_library qid in + let dir = Nametab.full_name_module qid in (LibLoaded, dir, library_full_filename dir) with Not_found -> (* Look if in loadpath *) @@ -511,8 +511,8 @@ let export_library (loc,qid) = match Nametab.locate_module qid with MPfile dir -> add_anonymous_leaf (in_require ([dir],Some true)) - | _ -> - raise Not_found + | mp -> + export_module mp with Not_found -> user_err_loc diff --git a/library/nametab.ml b/library/nametab.ml index f6418de3e4..cbb3b23e96 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -355,7 +355,7 @@ let locate_module qid = | DirModule (_,(mp,_)) -> mp | _ -> raise Not_found -let locate_loaded_library qid = +let full_name_module qid = match locate_dir qid with | DirModule (dir,_) -> dir | _ -> raise Not_found @@ -428,6 +428,9 @@ let id_of_global ctx_opt ref = let sp_of_syntactic_definition kn = Globrevtab.find (SyntacticDef kn) !the_globrevtab +let dir_of_mp mp = + MPmap.find mp !the_modrevtab + (* Shortest qualid functions **********************************************) diff --git a/library/nametab.mli b/library/nametab.mli index 1f29a9313a..bd1a8b1bdb 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -127,7 +127,7 @@ val full_name_modtype : qualid -> section_path val full_name_cci : qualid -> section_path (* As above but checks that the path found is indeed a module *) -val locate_loaded_library : qualid -> dir_path +val full_name_module : qualid -> dir_path (*s Reverse lookup -- finding user names corresponding to the given @@ -145,6 +145,9 @@ val shortest_qualid_of_syndef : val id_of_global : Sign.named_context option -> global_reference -> identifier +val dir_of_mp : + module_path -> dir_path + (* Printing of global references using names as short as possible *) val pr_global_env : Sign.named_context option -> global_reference -> std_ppcmds |