diff options
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 113 |
1 files changed, 73 insertions, 40 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index b33b12d2b..0c1cafdd7 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -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,57 +446,60 @@ 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 (env,oldargs,oldsubst) (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 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 = + let substituted's = List.map2 - (fun dir mp -> dir, mp, subst_substobjs dir mp substobjs) - dirs mps + (fun dir mp -> dir, mp, substobjs, 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 - + 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, + substituted's :: oldsubst + +let load_args_object (dir,mp,substobjs,substituted) = + do_module false "interp" load_objects 1 dir mp substobjs substituted + 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 + let env,arg_entries_revlist,substituted_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 arg_entries in + + List.iter (List.iter load_args_object) (List.rev substituted_revlist); + 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) + | Some (res, restricted) -> + (* we translate the module here to catch errors as early as possible *) + let mte = interp_modtype env res in + check_sig_entry 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 - let sub_mtb = - Mod_typing.translate_modtype (Global.env()) sub_mte - in - None, Some sub_mtb - in + None, Some sub_mtb - let mp = Global.start_module id arg_entries res_entry_o in + in let mbids = List.map fst arg_entries in openmod_info:=(mbids,res_entry_o,sub_body_o); @@ -496,8 +511,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 -> () @@ -645,13 +660,15 @@ 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 + let env,arg_entries_revlist,substituted_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 + List.iter (List.iter load_args_object) (List.rev substituted_revlist); + let mbids = List.map fst arg_entries in openmodtype_info := mbids; let prefix = Lib.start_modtype id mp fs in @@ -686,10 +703,23 @@ 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 + let env,arg_entries_revlist,substituted_revlist = + List.fold_left (intern_args interp_modtype) (env,[],[]) args in let arg_entries = List.concat (List.rev arg_entries_revlist) in + + (* Too strong: may depend of the logical object which are not registered, + while only names are needed in the constraint and the body; + The example + + Module Type T. Record t : Set := { a : nat }. Parameter b:Set. End T. + Module A. Record t : Set := { a : nat }. Definition b:=t. End A. + Module F (X:T) : T with Definition b:=X.t := A. + + fails (15 Apr 2006) *) + + List.iter (List.iter load_args_object) (List.rev substituted_revlist); + let base_mty = interp_modtype env mty in let entry = List.fold_right @@ -733,10 +763,13 @@ 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 + let env,arg_entries_revlist,substituted_revlist = + List.fold_left (intern_args interp_modtype) (env,[],[]) args in let arg_entries = List.concat (List.rev arg_entries_revlist) in + + List.iter (List.iter load_args_object) (List.rev substituted_revlist); + let mty_entry_o, mty_sub_o = match mty_o with None -> None, None | (Some (mty, true)) -> |