From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- kernel/safe_typing.ml | 100 ++++++++++++++++++++++++-------------------------- 1 file changed, 47 insertions(+), 53 deletions(-) (limited to 'kernel/safe_typing.ml') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 34071182..95092814 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: safe_typing.ml 7602 2005-11-23 15:10:16Z barras $ *) +(* $Id: safe_typing.ml 8898 2006-06-05 23:15:51Z letouzey $ *) open Util open Names @@ -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,36 +223,18 @@ let add_module l me senv = (* Interactive modules *) -let start_module l params result 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 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 [] } in mp, { old = senv; - env = env; + env = senv.env; modinfo = modinfo; labset = Labset.empty; revsign = []; @@ -261,21 +242,21 @@ let start_module l params result senv = imports = senv.imports; loads = [] } - - -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_map (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; - 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 @@ -288,10 +269,10 @@ let end_module l senv = mtb, Some mtb, cst in let mexpr = - List.fold_right - (fun (arg_id,arg_b) mtb -> MEBfunctor (arg_id,arg_b,mtb)) - params + List.fold_left + (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb)) (MEBstruct (modinfo.msid, List.rev senv.revstruct)) + params in let mb = { mod_expr = Some mexpr; @@ -326,31 +307,44 @@ let end_module l 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 = []; @@ -370,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 @@ -520,9 +514,9 @@ let import (dp,mb,depends,engmt) digest senv = let rec lighten_module mb = { mb with - mod_expr = option_app lighten_modexpr mb.mod_expr; + mod_expr = option_map lighten_modexpr mb.mod_expr; mod_type = lighten_modtype mb.mod_type; - mod_user_type = option_app lighten_modtype mb.mod_user_type } + mod_user_type = option_map lighten_modtype mb.mod_user_type } and lighten_modtype = function | MTBident kn as x -> x -- cgit v1.2.3