diff options
| -rw-r--r-- | kernel/safe_typing.ml | 73 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 8 | ||||
| -rw-r--r-- | library/declaremods.ml | 94 | ||||
| -rw-r--r-- | library/global.ml | 15 | ||||
| -rw-r--r-- | library/global.mli | 15 |
5 files changed, 84 insertions, 121 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ca1bf6f65..2a165f74e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -223,29 +223,18 @@ let add_module l me senv = (* Interactive modules *) -let start_module l params senv = +let start_module l senv = check_label l senv.labset; - let rec trans_params env = function - | [] -> env,[] - | (mbid,mte)::rest -> - let mtb = translate_modtype env mte in - let env = - full_add_module (MPbound mbid) (module_body_of_type mtb) env - in - let env,transrest = trans_params env rest in - env, (mbid,mtb)::transrest - in - let env,params_body = trans_params senv.env params in 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 } + variant = STRUCT [] } in mp, { old = senv; - env = env; + env = senv.env; modinfo = modinfo; labset = Labset.empty; revsign = []; @@ -253,8 +242,6 @@ let start_module l params senv = imports = senv.imports; loads = [] } - - let end_module l restype senv = let oldsenv = senv.old in let modinfo = senv.modinfo in @@ -266,9 +253,10 @@ let end_module l restype senv = in if l <> modinfo.label then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_local_context None; - let functorize_type = - List.fold_right - (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb)) + let functorize_type tb = + List.fold_left + (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb)) + tb params in let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in @@ -319,31 +307,44 @@ let end_module l restype senv = loads = senv.loads@oldsenv.loads } +(* Adding parameters to modules or module types *) + +let add_module_parameter mbid mte senv = + if senv.revsign <> [] or senv.revstruct <> [] or senv.loads <> [] then + anomaly "Cannot add a module parameter to a non empty module"; + let mtb = translate_modtype senv.env mte in + let env = full_add_module (MPbound mbid) (module_body_of_type mtb) senv.env + in + let new_variant = match senv.modinfo.variant with + | STRUCT params -> STRUCT ((mbid,mtb) :: params) + | SIG params -> SIG ((mbid,mtb) :: params) + | _ -> + anomaly "Module parameters can only be added to modules or signatures" + in + { old = senv.old; + env = env; + modinfo = { senv.modinfo with variant = new_variant }; + labset = senv.labset; + revsign = []; + revstruct = []; + imports = senv.imports; + loads = [] } + + (* Interactive module types *) -let start_modtype l params senv = +let start_modtype l senv = check_label l senv.labset; - let rec trans_params env = function - | [] -> env,[] - | (mbid,mte)::rest -> - let mtb = translate_modtype env mte in - let env = - full_add_module (MPbound mbid) (module_body_of_type mtb) env - in - let env,transrest = trans_params env rest in - env, (mbid,mtb)::transrest - in - let env,params_body = trans_params senv.env params in 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 = SIG params_body } + variant = SIG [] } in mp, { old = senv; - env = env; + env = senv.env; modinfo = modinfo; labset = Labset.empty; revsign = []; @@ -363,10 +364,10 @@ let end_modtype l senv = if not (empty_context senv.env) then error_local_context None; let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in let mtb = - List.fold_right - (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb)) - params + List.fold_left + (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb)) res_tb + params in let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in let newenv = oldsenv.env in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 43755b908..1b4d932b5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -72,17 +72,17 @@ val set_engagement : engagement -> safe_environment -> safe_environment (*s Interactive module functions *) val start_module : - label -> (mod_bound_id * module_type_entry) list - -> safe_environment -> module_path * safe_environment + label -> safe_environment -> module_path * safe_environment val end_module : label -> module_type_entry option -> safe_environment -> module_path * safe_environment +val add_module_parameter : + mod_bound_id -> module_type_entry -> safe_environment -> safe_environment val start_modtype : - label -> (mod_bound_id * module_type_entry) list - -> safe_environment -> module_path * safe_environment + label -> safe_environment -> module_path * safe_environment val end_modtype : label -> safe_environment -> kernel_name * safe_environment diff --git a/library/declaremods.ml b/library/declaremods.ml index 0c1cafdd7..39b9fc643 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -446,47 +446,34 @@ 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,oldsubst) (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, substobjs, subst_substobjs dir mp substobjs) - dirs mps - in - 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 + 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,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 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 mte = interp_modtype env res in - check_sig_entry env mte; - if restricted then + 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 @@ -496,9 +483,8 @@ let start_module interp_modtype export id args res_o = 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 + None, Some sub_mtb in let mbids = List.map fst arg_entries in @@ -659,15 +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,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 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; @@ -702,25 +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,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) *) + let _ = Global.start_modtype id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in - List.iter (List.iter load_args_object) (List.rev substituted_revlist); - - let base_mty = interp_modtype env mty 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)) @@ -760,15 +726,10 @@ 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,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 _ = 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 @@ -776,14 +737,14 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = 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 @@ -791,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 diff --git a/library/global.ml b/library/global.ml index 6ad414339..19b416519 100644 --- a/library/global.ml +++ b/library/global.ml @@ -73,12 +73,12 @@ 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 = +let start_module id = let l = label_of_id id in - let mp,newenv = start_module l params !global_env in + let mp,newenv = start_module l !global_env in global_env := newenv; mp - + let end_module id mtyo = let l = label_of_id id in let mp,newenv = end_module l mtyo !global_env in @@ -86,9 +86,14 @@ let end_module id mtyo = mp -let start_modtype id params = +let add_module_parameter mbid mte = + let newenv = add_module_parameter mbid mte !global_env in + global_env := newenv + + +let start_modtype id = let l = label_of_id id in - let mp,newenv = start_modtype l params !global_env in + let mp,newenv = start_modtype l !global_env in global_env := newenv; mp diff --git a/library/global.mli b/library/global.mli index af6ec6ae9..6842a44eb 100644 --- a/library/global.mli +++ b/library/global.mli @@ -63,18 +63,13 @@ val set_engagement : engagement -> unit (* [start_*] functions return the [module_path] valid for components of the started module / module type *) -val start_module : - identifier -> (mod_bound_id * module_type_entry) list -> module_path +val start_module : identifier -> module_path +val end_module : identifier -> module_type_entry option -> module_path -val end_module : - identifier -> module_type_entry option -> module_path +val add_module_parameter : mod_bound_id -> module_type_entry -> unit -val start_modtype : - identifier -> (mod_bound_id * module_type_entry) list - -> module_path - -val end_modtype : - identifier -> kernel_name +val start_modtype : identifier -> module_path +val end_modtype : identifier -> kernel_name (* Queries *) |