diff options
| -rw-r--r-- | kernel/modops.ml | 2 | ||||
| -rw-r--r-- | kernel/modops.mli | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 19 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
| -rw-r--r-- | library/declaremods.ml | 113 | ||||
| -rw-r--r-- | library/global.ml | 8 | ||||
| -rw-r--r-- | library/global.mli | 6 |
7 files changed, 89 insertions, 65 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index b20e7259d..166b23007 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -41,7 +41,7 @@ let error_incompatible_labels l l' = error ("Opening and closing labels are not the same: " ^string_of_label l^" <> "^string_of_label l'^" !") -let error_result_must_be_signature mtb = +let error_result_must_be_signature () = error "The result module type must be a signature" let error_signature_expected mtb = diff --git a/kernel/modops.mli b/kernel/modops.mli index f102a5b2c..b8f1f66a3 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -74,7 +74,7 @@ val error_incompatible_labels : label -> label -> 'a val error_no_such_label : label -> 'a -val error_result_must_be_signature : module_type_body -> 'a +val error_result_must_be_signature : unit -> 'a val error_signature_expected : module_type_body -> 'a diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9b638427c..ca1bf6f65 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -30,7 +30,6 @@ type modvariant = | NONE | SIG of (* funsig params *) (mod_bound_id * module_type_body) list | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list - * (* optional result type *) module_type_body option | LIBRARY of dir_path type module_info = @@ -224,7 +223,7 @@ let add_module l me senv = (* Interactive modules *) -let start_module l params result senv = +let start_module l params senv = check_label l senv.labset; let rec trans_params env = function | [] -> env,[] @@ -237,20 +236,13 @@ let start_module l params result senv = env, (mbid,mtb)::transrest in let env,params_body = trans_params senv.env params in - let check_sig mtb = match scrape_modtype env mtb with - | MTBsig _ -> () - | MTBfunsig _ -> error_result_must_be_signature mtb - | _ -> anomaly "start_module: modtype not scraped" - in - let result_body = option_app (translate_modtype env) result in - ignore (option_app check_sig result_body); let msid = make_msid senv.modinfo.seed (string_of_label l) in let mp = MPself msid in let modinfo = { msid = msid; modpath = mp; seed = senv.modinfo.seed; label = l; - variant = STRUCT(params_body,result_body) } + variant = STRUCT params_body } in mp, { old = senv; env = env; @@ -263,13 +255,14 @@ let start_module l params result senv = -let end_module l senv = +let end_module l restype senv = let oldsenv = senv.old in let modinfo = senv.modinfo in - let params, restype = + let restype = option_app (translate_modtype senv.env) restype in + let params = match modinfo.variant with | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () - | STRUCT(params,restype) -> (params,restype) + | STRUCT params -> params in if l <> modinfo.label then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_local_context None; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5412287ee..43755b908 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -73,11 +73,11 @@ val set_engagement : engagement -> safe_environment -> safe_environment (*s Interactive module functions *) val start_module : label -> (mod_bound_id * module_type_entry) list - -> module_type_entry option -> safe_environment -> module_path * safe_environment val end_module : - label -> safe_environment -> module_path * safe_environment + label -> module_type_entry option + -> safe_environment -> module_path * safe_environment val start_modtype : 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)) -> diff --git a/library/global.ml b/library/global.ml index d4ad97a8c..6ad414339 100644 --- a/library/global.ml +++ b/library/global.ml @@ -73,15 +73,15 @@ let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env -let start_module id params mtyo = +let start_module id params = let l = label_of_id id in - let mp,newenv = start_module l params mtyo !global_env in + let mp,newenv = start_module l params !global_env in global_env := newenv; mp -let end_module id = +let end_module id mtyo = let l = label_of_id id in - let mp,newenv = end_module l !global_env in + let mp,newenv = end_module l mtyo !global_env in global_env := newenv; mp diff --git a/library/global.mli b/library/global.mli index 579882498..af6ec6ae9 100644 --- a/library/global.mli +++ b/library/global.mli @@ -64,12 +64,10 @@ val set_engagement : engagement -> unit of the started module / module type *) val start_module : - identifier -> (mod_bound_id * module_type_entry) list - -> module_type_entry option - -> module_path + identifier -> (mod_bound_id * module_type_entry) list -> module_path val end_module : - identifier -> module_path + identifier -> module_type_entry option -> module_path val start_modtype : identifier -> (mod_bound_id * module_type_entry) list |