diff options
Diffstat (limited to 'library/declaremods.ml')
-rw-r--r-- | library/declaremods.ml | 123 |
1 files changed, 59 insertions, 64 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 3b2196a5..aac2b599 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml 7720 2005-12-24 00:25:55Z herbelin $ i*) +(*i $Id: declaremods.ml 8752 2006-04-27 19:37:33Z herbelin $ i*) open Pp open Util @@ -122,6 +122,18 @@ let msid_of_prefix (_,(mp,sec)) = anomaly ("Non-empty section in module name!" ^ string_of_mp mp ^ "." ^ string_of_dirpath sec) +(* Check that a module type is not functorial *) + +let rec check_sig env = function + | MTBident kn -> check_sig env (Environ.lookup_modtype kn env) + | MTBsig _ -> () + | MTBfunsig _ -> Modops.error_result_must_be_signature () + +let rec check_sig_entry env = function + | MTEident kn -> check_sig env (Environ.lookup_modtype kn env) + | MTEsig _ -> () + | MTEfunsig _ -> Modops.error_result_must_be_signature () + | MTEwith (mte,_) -> check_sig_entry env mte (* This function checks if the type calculated for the module [mp] is a subtype of [sub_mtb]. Uses only the global environment. *) @@ -434,58 +446,47 @@ let rec get_some_body mty env = match mty with replace_module (get_some_body mty env) id (Environ.lookup_module mp env) -let intern_args interp_modtype (env,oldargs) (idl,arg) = +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 env arg in + let mty = interp_modtype (Global.env()) arg in let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in - let mps = List.map (fun mbid -> MPbound mbid) mbids in let substobjs = get_modtype_substobjs mty in - let substituted's = - List.map2 - (fun dir mp -> dir, mp, subst_substobjs dir mp substobjs) - dirs mps - in - List.iter - (fun (dir, mp, substituted) -> - do_module false "interp" load_objects 1 dir mp substobjs substituted) - substituted's; - let body = Modops.module_body_of_type (get_some_body mty env) in - let env = - List.fold_left (fun env mp -> Modops.add_module mp body env) env mps - in - env, List.map (fun mbid -> mbid,mty) mbids :: oldargs - + List.map2 + (fun dir mbid -> + Global.add_module_parameter mbid mty; + let mp = MPbound mbid in + let substituted = subst_substobjs dir mp substobjs in + 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 - let env = Global.env () in - let env,arg_entries_revlist = - List.fold_left (intern_args interp_modtype) (env,[]) args - in - let arg_entries = List.concat (List.rev arg_entries_revlist) 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, 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 + | 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 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)) + arg_entries mtb + 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,sub_body_o); let prefix = Lib.start_module export id mp fs in @@ -496,8 +497,8 @@ let start_module interp_modtype export id args res_o = 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 + let mp = Global.end_module id res_o in begin match sub_o with None -> () @@ -584,7 +585,7 @@ let register_library dir cenv objs digest = let msid,substitute,keep = objs in let substobjs = empty_subst, [], msid, substitute in let substituted = subst_substobjs dir mp substobjs in - let objects = option_app (fun seg -> seg@keep) substituted in + let objects = option_map (fun seg -> seg@keep) substituted in let modobjs = substobjs, objects in Hashtbl.add library_cache dir modobjs; modobjs @@ -644,13 +645,9 @@ let import_module export mp = let start_modtype interp_modtype id args = let fs = Summary.freeze_summaries () in - let env = Global.env () in - let env,arg_entries_revlist = - List.fold_left (intern_args interp_modtype) (env,[]) args - in - let arg_entries = List.concat (List.rev arg_entries_revlist) in - let mp = Global.start_modtype id arg_entries in + let mp = Global.start_modtype id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let mbids = List.map fst arg_entries in openmodtype_info := mbids; @@ -685,12 +682,11 @@ let end_modtype id = let declare_modtype interp_modtype id args mty = let fs = Summary.freeze_summaries () in - let env = Global.env () in - let env,arg_entries_revlist = - List.fold_left (intern_args interp_modtype) (env,[]) args - in - let arg_entries = List.concat (List.rev arg_entries_revlist) in - let base_mty = interp_modtype env mty in + + let _ = Global.start_modtype id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in + + let base_mty = interp_modtype (Global.env()) mty in let entry = List.fold_right (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) @@ -730,27 +726,25 @@ let rec get_module_substobjs env = function let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = - let fs = Summary.freeze_summaries () in - let env = Global.env () in - let env,arg_entries_revlist = - List.fold_left (intern_args interp_modtype) (env,[]) args - in - let arg_entries = List.concat (List.rev arg_entries_revlist) in + + let _ = Global.start_module id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in + let mty_entry_o, mty_sub_o = match mty_o with None -> None, None | (Some (mty, true)) -> Some (List.fold_right (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) arg_entries - (interp_modtype env mty)), + (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)) arg_entries - (interp_modtype env mty)) + (interp_modtype (Global.env()) mty)) in let mexpr_entry_o = match mexpr_o with None -> None @@ -758,12 +752,13 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = Some (List.fold_right (fun (mbid,mte) me -> MEfunctor(mbid,mte,me)) arg_entries - (interp_modexpr env mexpr)) + (interp_modexpr (Global.env()) mexpr)) in let entry = {mod_entry_type = mty_entry_o; mod_entry_expr = mexpr_entry_o } in + let env = Global.env() in let substobjs = match entry with | {mod_entry_type = Some mte} -> get_modtype_substobjs mte |