diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index a1a29c701250..29ffc26f9f06 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -235,17 +235,18 @@ let rec check_mexpression env opac sign mbtyp mp_mse res = match sign with let rec check_module env opac mp mb opacify = Flags.if_verbose Feedback.msg_notice (str " checking module: " ++ str (ModPath.to_string mp)); let env = Modops.add_retroknowledge (mod_retroknowledge mb) env in + let () = assert (ModPath.equal (mod_mp mb) mp) in let opac = - check_signature env opac (mod_type mb) (mod_mp mb) (mod_delta mb) opacify + check_signature env opac (mod_type mb) mp (mod_delta mb) opacify in let optsign, opac = match Mod_declarations.mod_expr mb with | Struct sign_struct -> - let opacify = collect_constants_without_body (mod_type mb) (mod_mp mb) opacify in + let opacify = collect_constants_without_body (mod_type mb) mp opacify in (* TODO: a bit wasteful, we recheck the types of parameters twice *) let sign_struct = Modops.annotate_struct_body sign_struct (mod_type mb) in - let opac = check_signature env opac sign_struct (mod_mp mb) (mod_delta mb) opacify in + let opac = check_signature env opac sign_struct mp (mod_delta mb) opacify in Some (sign_struct, mod_delta mb), opac - | Algebraic me -> Some (check_mexpression env opac me (mod_type mb) (mod_mp mb) (mod_delta mb)), opac + | Algebraic me -> Some (check_mexpression env opac me (mod_type mb) mp (mod_delta mb)), opac | Abstract|FullStruct -> None, opac in let () = match optsign with @@ -260,10 +261,11 @@ let rec check_module env opac mp mb opacify = in opac -and check_module_type env mty = - Flags.if_verbose Feedback.msg_notice (str " checking module type: " ++ str (ModPath.to_string @@ mod_mp mty)); +and check_module_type env mp mty = + let () = assert (ModPath.equal (mod_mp mty) mp) in + Flags.if_verbose Feedback.msg_notice (str " checking module type: " ++ str (ModPath.to_string @@ mp)); let _ : _ Cmap.t = - check_signature env Cmap.empty (mod_type mty) (mod_mp mty) (mod_delta mty) Cset.empty in + check_signature env Cmap.empty (mod_type mty) mp (mod_delta mty) Cset.empty in () and check_structure_field env opac mp lab res opacify = function @@ -278,7 +280,7 @@ and check_structure_field env opac mp lab res opacify = function let opac = check_module env opac (MPdot(mp,lab)) msb opacify in Modops.add_module msb env, opac | SFBmodtype mty -> - check_module_type env mty; + let () = check_module_type env (MPdot (mp, lab)) mty in add_modtype mty env, opac | SFBrules rrb -> check_rewrite_rules_body env lab rrb; @@ -286,7 +288,7 @@ and check_structure_field env opac mp lab res opacify = function and check_signature env opac sign mp_mse res opacify = match sign with | MoreFunctor (arg_id, mtb, body) -> - check_module_type env mtb; + let () = check_module_type env (MPbound arg_id) mtb in let env' = Modops.add_module_type (MPbound arg_id) mtb env in let opac = check_signature env' opac body mp_mse res Cset.empty in opac diff --git a/kernel/mod_declarations.ml b/kernel/mod_declarations.ml index 7469d3f7026c..3e0d7d989bed 100644 --- a/kernel/mod_declarations.ml +++ b/kernel/mod_declarations.ml @@ -115,6 +115,7 @@ let module_type_of_module mb = mod_retroknowledge = ModTypeNul; } let module_body_of_type mp mtb = + let () = assert (ModPath.equal mp mtb.mod_mp) in { mtb with mod_expr = ModBodyVal Abstract; mod_mp = mp; mod_retroknowledge = ModBodyVal []; } diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 1f441382c6c4..f84f92de7120 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -263,7 +263,8 @@ let rec translate_mse (cst, ustate) (vm, vmstate) env mpo inl = function | Some mp -> strengthen_and_subst_module_body (lookup_module mp1 env) mp false | None -> let mt = lookup_modtype mp1 env in - module_body_of_type (mod_mp mt) mt + let () = assert (ModPath.equal mp1 (mod_mp mt)) in + module_body_of_type mp1 mt in mod_type mb, me, mod_delta mb, cst, vm | MEapply (fe,mp1) -> diff --git a/kernel/modops.ml b/kernel/modops.ml index f874994675db..97e8cd107fd4 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -221,7 +221,8 @@ let strengthen_const mp_from l cb resolver = const_body_code = Some (Vmbytegen.compile_alias con) } let rec strengthen_module mp_from mp_to mb = - if mp_in_delta (mod_mp mb) (mod_delta mb) then mb + let () = assert (ModPath.equal mp_from (mod_mp mb)) in + if mp_in_delta mp_from (mod_delta mb) then mb else match mod_type mb with | NoFunctor struc -> let reso,struc' = strengthen_signature mp_from struc mp_to (mod_delta mb) in @@ -250,21 +251,23 @@ and strengthen_signature mp_from struc mp_to reso = match struc with reso',item::rest' let strengthen mtb mp = + let () = assert (ModPath.equal mp (mod_mp mtb)) in (* Has mtb already been strengthened ? *) - if mp_in_delta (mod_mp mtb) (mod_delta mtb) then mtb + if mp_in_delta mp (mod_delta mtb) then mtb else match mod_type mtb with | NoFunctor struc -> - let reso',struc' = strengthen_signature (mod_mp mtb) struc mp (mod_delta mtb) in - let reso' = add_delta_resolver (mod_delta mtb) (add_mp_delta_resolver (mod_mp mtb) mp reso') in + let reso',struc' = strengthen_signature mp struc mp (mod_delta mtb) in + let reso' = add_delta_resolver (mod_delta mtb) (add_mp_delta_resolver mp mp reso') in strengthen_module_type struc' reso' mtb | MoreFunctor _ -> mtb (** {6 Strengthening a module for [Module M := M'] or [Include M] } *) let rec strengthen_and_subst_module mb subst mp_from mp_to = + let () = assert (ModPath.equal mp_from (mod_mp mb)) in match mod_type mb with | NoFunctor struc -> - let mb_is_an_alias = mp_in_delta (mod_mp mb) (mod_delta mb) in + let mb_is_an_alias = mp_in_delta mp_from (mod_delta mb) in if mb_is_an_alias then subst_module subst do_delta_dom mb else let reso',struc' = @@ -274,7 +277,7 @@ let rec strengthen_and_subst_module mb subst mp_from mp_to = let reso' = add_mp_delta_resolver mp_to mp_from reso' in strengthen_module_body ~src:mp_from ~dst:(Some mp_to) (NoFunctor struc') reso' mb | MoreFunctor _ -> - let subst = add_mp (mod_mp mb) mp_to empty_delta_resolver subst in + let subst = add_mp mp_from mp_to empty_delta_resolver subst in subst_module subst do_delta_dom mb and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso = @@ -369,24 +372,26 @@ and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso = let strengthen_and_subst_module_body mb mp include_b = match mod_type mb with | NoFunctor struc -> - let mb_is_an_alias = mp_in_delta (mod_mp mb) (mod_delta mb) in + let mp_from = mod_mp mb in + let mb_is_an_alias = mp_in_delta mp_from (mod_delta mb) in (* if mb.mod_mp is an alias then the strengthening is useless (i.e. it is already done)*) - let mp_alias = mp_of_delta (mod_delta mb) (mod_mp mb) in - let subst_resolver = map_mp (mod_mp mb) mp empty_delta_resolver in + let mp_alias = mp_of_delta (mod_delta mb) mp_from in + let subst_resolver = map_mp mp_from mp empty_delta_resolver in let new_resolver = add_mp_delta_resolver mp mp_alias (subst_dom_delta_resolver subst_resolver (mod_delta mb)) in - let subst = map_mp (mod_mp mb) mp new_resolver in + let subst = map_mp mp_from mp new_resolver in let reso',struc' = strengthen_and_subst_struct struc subst - (mod_mp mb) mp mb_is_an_alias include_b (mod_delta mb) + mp_from mp mb_is_an_alias include_b (mod_delta mb) in let reso' = if include_b then reso' else add_delta_resolver new_resolver reso' in - strengthen_module_body ~src:(mod_mp mb) ~dst:(Some mp) (NoFunctor struc') reso' mb + strengthen_module_body ~src:mp_from ~dst:(Some mp) (NoFunctor struc') reso' mb | MoreFunctor _ -> - let subst = map_mp (mod_mp mb) mp empty_delta_resolver in + let mp_from = mod_mp mb in + let subst = map_mp mp_from mp empty_delta_resolver in subst_module subst do_delta_dom_codom mb let subst_modtype_signature_and_resolver mp_from mp_to sign reso = diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 33a53b8df38c..75fa40815ac3 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -45,7 +45,8 @@ and translate_field mp env acc (l,x) = Pp.str msg)); compile_rewrite_rules env l acc rrb | SFBmodule md -> - let mp = mod_mp md in + let mp = MPdot (mp, l) in + let () = assert (ModPath.equal mp (mod_mp md)) in (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module %s..." (ModPath.to_string mp) @@ -53,7 +54,8 @@ and translate_field mp env acc (l,x) = Pp.str msg)); translate_mod mp env (mod_type md) acc | SFBmodtype mdtyp -> - let mp = mod_mp mdtyp in + let mp = MPdot (mp, l) in + let () = assert (ModPath.equal mp (mod_mp mdtyp)) in (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 5126cf36c1ce..fac647bca330 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -264,10 +264,12 @@ let check_constant (cst, ustate) trace env l info1 cb2 subst1 subst2 = Anyway [check_conv] will handle that afterwards. *) check_conv NotConvertibleBodyField cst poly CONV env c1 c2)) -let rec check_modules state trace env msb1 msb2 subst1 subst2 = +let rec check_modules state trace env mp1 msb1 mp2 msb2 subst1 subst2 = + let () = assert (ModPath.equal mp1 (mod_mp msb1)) in + let () = assert (ModPath.equal mp2 (mod_mp msb2)) in let mty1 = module_type_of_module msb1 in - let mty2 = module_type_of_module msb2 in - check_modtypes state trace env mty1 mty2 subst1 subst2 false + let mty2 = module_type_of_module msb2 in + check_modtypes state trace env mp1 mty1 mp2 mty2 subst1 subst2 false and check_signatures (cst, ustate) trace env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2 = let map1 = make_labmap mp1 sig1 in @@ -282,8 +284,10 @@ and check_signatures (cst, ustate) trace env mp1 sig1 mp2 sig2 subst1 subst2 res | SFBrules _ -> error_signature_mismatch trace l NoRewriteRulesSubtyping | SFBmodule msb2 -> + let mp1' = MPdot (mp1, l) in + let mp2' = MPdot (mp2, l) in begin match get_mod mp1 map1 l with - | Module msb -> check_modules (cst, ustate) (Submodule l :: trace) env msb msb2 subst1 subst2 + | Module msb1 -> check_modules (cst, ustate) (Submodule l :: trace) env mp1' msb1 mp2' msb2 subst1 subst2 | _ -> error_signature_mismatch trace l ModuleFieldExpected end | SFBmodtype mtb2 -> @@ -291,15 +295,18 @@ and check_signatures (cst, ustate) trace env mp1 sig1 mp2 sig2 subst1 subst2 res | Modtype mtb -> mtb | _ -> error_signature_mismatch trace l ModuleTypeFieldExpected in - let env = - add_module_type (mod_mp mtb2) mtb2 - (add_module_type (mod_mp mtb1) mtb1 env) - in - check_modtypes (cst, ustate) (Submodule l :: trace) env mtb1 mtb2 subst1 subst2 true + let mp1' = MPdot (mp1, l) in + let mp2' = MPdot (mp2, l) in + let () = assert (ModPath.equal mp1' (mod_mp mtb1)) in + let () = assert (ModPath.equal mp2' (mod_mp mtb2)) in + let env = add_module_type mp2' mtb2 (add_module_type mp1' mtb1 env) in + check_modtypes (cst, ustate) (Submodule l :: trace) env mp1' mtb1 mp2' mtb2 subst1 subst2 true in List.fold_left check_one_body cst sig2 -and check_modtypes (cst, ustate) trace env mtb1 mtb2 subst1 subst2 equiv = +and check_modtypes (cst, ustate) trace env mp1 mtb1 mp2 mtb2 subst1 subst2 equiv = + let () = assert (ModPath.equal mp1 (mod_mp mtb1)) in + let () = assert (ModPath.equal mp2 (mod_mp mtb2)) in if mtb1==mtb2 || mod_type mtb1 == mod_type mtb2 then cst else let rec check_structure cst ~nargs env struc1 struc2 equiv subst1 subst2 = @@ -307,32 +314,33 @@ and check_modtypes (cst, ustate) trace env mtb1 mtb2 subst1 subst2 equiv = | NoFunctor list1, NoFunctor list2 -> if equiv then - let subst2 = add_mp (mod_mp mtb2) (mod_mp mtb1) (mod_delta mtb1) subst2 in + let subst2 = add_mp mp2 mp1 (mod_delta mtb1) subst2 in let cst = check_signatures (cst, ustate) trace env - (mod_mp mtb1) list1 (mod_mp mtb2) list2 subst1 subst2 + mp1 list1 mp2 list2 subst1 subst2 (mod_delta mtb1) (mod_delta mtb2) in let cst = check_signatures (cst, ustate) trace env - (mod_mp mtb2) list2 (mod_mp mtb1) list1 subst2 subst1 + mp2 list2 mp1 list1 subst2 subst1 (mod_delta mtb2) (mod_delta mtb1) in cst else check_signatures (cst, ustate) trace env - (mod_mp mtb1) list1 (mod_mp mtb2) list2 subst1 subst2 + mp1 list1 mp2 list2 subst1 subst2 (mod_delta mtb1) (mod_delta mtb2) | MoreFunctor (arg_id1,arg_t1,body_t1), MoreFunctor (arg_id2,arg_t2,body_t2) -> - let mp2 = MPbound arg_id2 in - let subst1 = join (map_mbid arg_id1 mp2 (mod_delta arg_t2)) subst1 in - let env = add_module_type mp2 arg_t2 env in - let cst = check_modtypes (cst, ustate) (FunctorArgument (nargs+1) :: trace) env arg_t2 arg_t1 subst2 subst1 equiv in + let mparg1 = MPbound arg_id1 in + let mparg2 = MPbound arg_id2 in + let subst1 = join (map_mbid arg_id1 mparg2 (mod_delta arg_t2)) subst1 in + let env = add_module_type mparg2 arg_t2 env in + let cst = check_modtypes (cst, ustate) (FunctorArgument (nargs+1) :: trace) env mparg2 arg_t2 mparg1 arg_t1 subst2 subst1 equiv in (* contravariant *) let env = if Modops.is_functor body_t1 then env else - let mtb = make_module_type (mod_mp mtb1) (subst_signature subst1 body_t1) (mod_delta mtb1) in - add_module (module_body_of_type (mod_mp mtb1) mtb) env + let mtb = make_module_type mp1 (subst_signature subst1 body_t1) (mod_delta mtb1) in + add_module (module_body_of_type mp1 mtb) env in check_structure cst ~nargs:(nargs + 1) env body_t1 body_t2 equiv subst1 subst2 | _ , _ -> error_incompatible_modtypes mtb1 mtb2 @@ -340,8 +348,9 @@ and check_modtypes (cst, ustate) trace env mtb1 mtb2 subst1 subst2 equiv = check_structure cst ~nargs:0 env (mod_type mtb1) (mod_type mtb2) equiv subst1 subst2 let check_subtypes state env sup super = - let env = add_module_type (mod_mp sup) sup env in + let mp_sup = mod_mp sup in + let mp_super = mod_mp super in + let env = add_module_type mp_sup sup env in check_modtypes state [] env - (strengthen sup (mod_mp sup)) super empty_subst - (map_mp (mod_mp super) (mod_mp sup) (mod_delta sup)) false - + mp_sup (strengthen sup mp_sup) mp_super super empty_subst + (map_mp mp_super mp_sup (mod_delta sup)) false diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 297b794fda58..8dea38ae5b37 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -223,11 +223,15 @@ let rec extract_structure_spec env mp reso = function specs | (l,SFBmodule mb) :: msig -> let specs = extract_structure_spec env mp reso msig in - let spec = extract_mbody_spec env (mod_mp mb) mb in + let mp = MPdot (mp, l) in + let () = assert (ModPath.equal mp (mod_mp mb)) in + let spec = extract_mbody_spec env mp mb in (l,Smodule spec) :: specs | (l,SFBmodtype mtb) :: msig -> let specs = extract_structure_spec env mp reso msig in - let spec = extract_mbody_spec env (mod_mp mtb) mtb in + let mp = MPdot (mp, l) in + let () = assert (ModPath.equal mp (mod_mp mtb)) in + let spec = extract_mbody_spec env mp mtb in (l,Smodtype spec) :: specs (* From [module_expression] to specifications *) diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 401ccf11fe97..35540f5f6e60 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -84,19 +84,20 @@ and memoize_fields_of_mp mp = and fields_of_mp mp = let open Mod_subst in let mb = lookup_module_in_impl mp in - let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in + let () = assert (ModPath.equal mp (mod_mp mb)) in + let fields,inner_mp,subs = fields_of_mb empty_subst mp mb [] in let subs = if ModPath.equal inner_mp mp then subs else add_mp inner_mp mp (mod_delta mb) subs in Modops.subst_structure subs fields -and fields_of_mb subs mb args = match Mod_declarations.mod_expr mb with - | Algebraic expr -> fields_of_expression subs (mod_mp mb) args (mod_type mb) expr +and fields_of_mb subs mp mb args = match Mod_declarations.mod_expr mb with + | Algebraic expr -> fields_of_expression subs mp args (mod_type mb) expr | Struct sign -> let sign = Modops.annotate_struct_body sign (mod_type mb) in - fields_of_signature subs (mod_mp mb) args sign - | Abstract|FullStruct -> fields_of_signature subs (mod_mp mb) args (mod_type mb) + fields_of_signature subs mp args sign + | Abstract|FullStruct -> fields_of_signature subs mp args (mod_type mb) (** The Abstract case above corresponds to [Declare Module] *) @@ -108,8 +109,10 @@ and fields_of_signature x = and fields_of_expr subs mp0 args = function | MEident mp -> - let mb = lookup_module_in_impl (Mod_subst.subst_mp subs mp) in - fields_of_mb subs mb args + let mp = Mod_subst.subst_mp subs mp in + let mb = lookup_module_in_impl mp in + let () = assert (ModPath.equal mp (mod_mp mb)) in + fields_of_mb subs mp mb args | MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1 | MEwith _ -> assert false (* no 'with' in [mod_expr] *)