diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_typing.ml | 63 | ||||
| -rw-r--r-- | kernel/mod_typing.mli | 10 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 27 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 10 |
4 files changed, 60 insertions, 50 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 26ad7e383a..cfa256888e 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -224,12 +224,12 @@ and check_with_aux_mod env sign with_decl mp equiv = Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l -and translate_module env mp me = +and translate_module env mp inl me = match me.mod_entry_expr, me.mod_entry_type with | None, None -> anomaly "Mod_typing.translate_module: empty type and expr in module entry" | None, Some mte -> - let mtb = translate_module_type env mp mte in + let mtb = translate_module_type env mp inl mte in { mod_mp = mp; mod_expr = None; mod_type = mtb.typ_expr; @@ -239,13 +239,13 @@ and translate_module env mp me = mod_retroknowledge = []} | Some mexpr, _ -> let sign,alg_implem,resolver,cst1 = - translate_struct_module_entry env mp mexpr in + translate_struct_module_entry env mp inl mexpr in let sign,alg1,resolver,cst2 = match me.mod_entry_type with | None -> sign,None,resolver,Constraint.empty | Some mte -> - let mtb = translate_module_type env mp mte in + let mtb = translate_module_type env mp inl mte in let cst = check_subtypes env {typ_mp = mp; typ_expr = sign; @@ -269,21 +269,23 @@ and translate_module env mp me = fix the bug.*) -and translate_struct_module_entry env mp mse = match mse with +and translate_struct_module_entry env mp inl mse = match mse with | MSEident mp1 -> let mb = lookup_module mp1 env in let mb' = strengthen_and_subst_mb mb mp env false in mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.Constraint.empty | MSEfunctor (arg_id, arg_e, body_expr) -> - let mtb = translate_module_type env (MPbound arg_id) arg_e in + let mtb = translate_module_type env (MPbound arg_id) inl arg_e in let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in - let sign,alg,resolver,cst = translate_struct_module_entry env' - mp body_expr in - SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver, + let sign,alg,resolver,cst = + translate_struct_module_entry env' mp inl body_expr in + SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver, Univ.Constraint.union cst mtb.typ_constraints | MSEapply (fexpr,mexpr) -> - let sign,alg,resolver,cst1 = translate_struct_module_entry env mp fexpr in + let sign,alg,resolver,cst1 = + translate_struct_module_entry env mp inl fexpr + in let farg_id, farg_b, fbody_b = destr_functor env sign in let mtb,mp1 = try @@ -294,32 +296,35 @@ and translate_struct_module_entry env mp mse = match mse with | Not_path -> error_application_to_not_path mexpr (* place for nondep_supertype *) in let cst = check_subtypes env mtb farg_b in - let mp_delta = discr_resolver env mtb in - let mp_delta = complete_inline_delta_resolver env mp1 - farg_id farg_b mp_delta in + let mp_delta = discr_resolver env mtb in + let mp_delta = if not inl then mp_delta else + complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta + in let subst = map_mbid farg_id mp1 mp_delta in (subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst), (subst_codom_delta_resolver subst resolver), Univ.Constraint.union cst1 cst | MSEwith(mte, with_decl) -> - let sign,alg,resolve,cst1 = translate_struct_module_entry env mp mte in + let sign,alg,resolve,cst1 = translate_struct_module_entry env mp inl mte in let sign,alg,resolve,cst2 = check_with env sign with_decl (Some alg) mp resolve in sign,Option.get alg,resolve,Univ.Constraint.union cst1 cst2 -and translate_struct_type_entry env mse = match mse with +and translate_struct_type_entry env inl mse = match mse with | MSEident mp1 -> let mtb = lookup_modtype mp1 env in mtb.typ_expr, Some (SEBident mp1),mtb.typ_delta,mp1,Univ.Constraint.empty | MSEfunctor (arg_id, arg_e, body_expr) -> - let mtb = translate_module_type env (MPbound arg_id) arg_e in + let mtb = translate_module_type env (MPbound arg_id) inl arg_e in let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in - let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env' - body_expr in + let sign,alg,resolve,mp_from,cst = + translate_struct_type_entry env' inl body_expr in SEBfunctor (arg_id, mtb, sign),None,resolve,mp_from, Univ.Constraint.union cst mtb.typ_constraints | MSEapply (fexpr,mexpr) -> - let sign,alg,resolve,mp_from,cst1 = translate_struct_type_entry env fexpr in + let sign,alg,resolve,mp_from,cst1 = + translate_struct_type_entry env inl fexpr + in let farg_id, farg_b, fbody_b = destr_functor env sign in let mtb,mp1 = try @@ -331,19 +336,20 @@ and translate_struct_type_entry env mse = match mse with (* place for nondep_supertype *) in let cst2 = check_subtypes env mtb farg_b in let mp_delta = discr_resolver env mtb in - let mp_delta = complete_inline_delta_resolver env mp1 - farg_id farg_b mp_delta in + let mp_delta = if not inl then mp_delta else + complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta + in let subst = map_mbid farg_id mp1 mp_delta in (subst_struct_expr subst fbody_b),None, (subst_codom_delta_resolver subst resolve),mp_from,Univ.Constraint.union cst1 cst2 | MSEwith(mte, with_decl) -> - let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env mte in + let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in let sign,alg,resolve,cst1 = check_with env sign with_decl alg mp_from resolve in sign,alg,resolve,mp_from,Univ.Constraint.union cst cst1 -and translate_module_type env mp mte = - let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env mte in +and translate_module_type env mp inl mte = + let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in subst_modtype_and_resolver {typ_mp = mp_from; typ_expr = sign; @@ -351,14 +357,14 @@ and translate_module_type env mp mte = typ_constraints = cst; typ_delta = resolve} mp env -let rec translate_struct_include_module_entry env mp mse = match mse with +let rec translate_struct_include_module_entry env mp inl mse = match mse with | MSEident mp1 -> let mb = lookup_module mp1 env in let mb' = strengthen_and_subst_mb mb mp env true in mb'.mod_type, mb'.mod_delta,Univ.Constraint.empty | MSEapply (fexpr,mexpr) -> let sign,resolver,cst1 = - translate_struct_include_module_entry env mp fexpr in + translate_struct_include_module_entry env mp inl fexpr in let farg_id, farg_b, fbody_b = destr_functor env sign in let mtb,mp1 = try @@ -370,8 +376,9 @@ let rec translate_struct_include_module_entry env mp mse = match mse with (* place for nondep_supertype *) in let cst = check_subtypes env mtb farg_b in let mp_delta = discr_resolver env mtb in - let mp_delta = complete_inline_delta_resolver env mp1 - farg_id farg_b mp_delta in + let mp_delta = if not inl then mp_delta else + complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta + in let subst = map_mbid farg_id mp1 mp_delta in (subst_struct_expr subst fbody_b), (subst_codom_delta_resolver subst resolver), diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 746a80e151..63f7696c48 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -17,20 +17,20 @@ open Names (*i*) -val translate_module : env -> module_path -> module_entry +val translate_module : env -> module_path -> bool -> module_entry -> module_body -val translate_module_type : env -> module_path -> module_struct_entry -> +val translate_module_type : env -> module_path -> bool -> module_struct_entry -> module_type_body -val translate_struct_module_entry : env -> module_path -> module_struct_entry -> +val translate_struct_module_entry : env -> module_path -> bool -> module_struct_entry -> struct_expr_body * struct_expr_body * delta_resolver * Univ.constraints -val translate_struct_type_entry : env -> module_struct_entry -> +val translate_struct_type_entry : env -> bool -> module_struct_entry -> struct_expr_body * struct_expr_body option * delta_resolver * module_path * Univ.constraints val translate_struct_include_module_entry : env -> module_path - -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints + -> bool -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints val add_modtype_constraints : env -> module_type_body -> env diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ef2ea800cf..e4c6ec35e1 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -262,10 +262,10 @@ let add_mind dir l mie senv = (* Insertion of module types *) -let add_modtype l mte senv = +let add_modtype l mte inl senv = check_label l senv.labset; let mp = MPdot(senv.modinfo.modpath, l) in - let mtb = translate_module_type senv.env mp mte in + let mtb = translate_module_type senv.env mp inl mte in let senv' = add_constraints mtb.typ_constraints senv in let env'' = Environ.add_modtype mp mtb senv'.env in mp, { old = senv'.old; @@ -288,10 +288,10 @@ let full_add_module mb senv = (* Insertion of modules *) -let add_module l me senv = +let add_module l me inl senv = check_label l senv.labset; let mp = MPdot(senv.modinfo.modpath, l) in - let mb = translate_module senv.env mp me in + let mb = translate_module senv.env mp inl me in let senv' = full_add_module mb senv in let modinfo = match mb.mod_type with SEBstruct _ -> @@ -339,7 +339,9 @@ let end_module l restype senv = let oldsenv = senv.old in let modinfo = senv.modinfo in let mp = senv.modinfo.modpath in - let restype = Option.map (translate_module_type senv.env mp) restype in + let restype = + Option.map + (fun (res,inl) -> translate_module_type senv.env mp inl res) restype in let params,is_functor = match modinfo.variant with | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () @@ -420,17 +422,17 @@ let end_module l restype senv = (* Include for module and module type*) - let add_include me is_module senv = + let add_include me is_module inl senv = let sign,cst,resolver = if is_module then let sign,resolver,cst = translate_struct_include_module_entry senv.env - senv.modinfo.modpath me in + senv.modinfo.modpath inl me in sign,cst,resolver else let mtb = translate_module_type senv.env - senv.modinfo.modpath me in + senv.modinfo.modpath inl me in mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta in let senv = add_constraints cst senv in @@ -441,8 +443,9 @@ let end_module l restype senv = | SEBfunctor(mbid,mtb,str) -> let cst_sub = check_subtypes senv.env mb mtb in let senv = add_constraints cst_sub senv in - let mpsup_delta = complete_inline_delta_resolver senv.env mp_sup - mbid mtb mb.typ_delta in + let mpsup_delta = if not inl then mb.typ_delta else + complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta + in (compute_sign (subst_struct_expr (map_mbid mbid mp_sup mpsup_delta) str) mb senv) | str -> str,senv @@ -534,10 +537,10 @@ let end_module l restype senv = (* Adding parameters to modules or module types *) -let add_module_parameter mbid mte senv = +let add_module_parameter mbid mte inl senv = if senv.revstruct <> [] or senv.loads <> [] then anomaly "Cannot add a module parameter to a non empty module"; - let mtb = translate_module_type senv.env (MPbound mbid) mte in + let mtb = translate_module_type senv.env (MPbound mbid) inl mte in let senv = full_add_module (module_body_of_type (MPbound mbid) mtb) senv in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 169fd158d8..c378d8ccc7 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -55,12 +55,12 @@ val add_mind : (* Adding a module *) val add_module : - label -> module_entry -> safe_environment + label -> module_entry -> bool -> safe_environment -> module_path * delta_resolver * safe_environment (* Adding a module type *) val add_modtype : - label -> module_struct_entry -> safe_environment + label -> module_struct_entry -> bool -> safe_environment -> module_path * safe_environment (* Adding universe constraints *) @@ -76,11 +76,11 @@ val start_module : label -> safe_environment -> module_path * safe_environment val end_module : - label -> module_struct_entry option + label -> (module_struct_entry * bool) option -> safe_environment -> module_path * delta_resolver * safe_environment val add_module_parameter : - mod_bound_id -> module_struct_entry -> safe_environment -> delta_resolver * safe_environment + mod_bound_id -> module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment val start_modtype : label -> safe_environment -> module_path * safe_environment @@ -89,7 +89,7 @@ val end_modtype : label -> safe_environment -> module_path * safe_environment val add_include : - module_struct_entry -> bool -> safe_environment -> + module_struct_entry -> bool -> bool -> safe_environment -> delta_resolver * safe_environment val pack_module : safe_environment -> module_body |