Merge PR coq#20058: Ensure at runtime that the modpath is synced with…

… module bodies and types

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

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,15 +280,15 @@ 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;
       Environ.add_rewrite_rules rrb.rewrules_rules env, opac
 
 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

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 []; }
 

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) ->

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 =

kernel/nativelibrary.ml

@@ -45,15 +45,17 @@ 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)
         in
         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)

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,66 +284,73 @@ 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 ->
             let mtb1 = match get_mod mp1 map1 l with
               | 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 =
       match struc1,struc2 with
       | 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
     in
     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

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 *)

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] *)