Ensure at runtime that the modpath is synced with module bodies and t…

…ypes.

We also seize the opportunity to remove subsequent calls to mod_mp once
we have asserted that they are equal to some other modpath. This will be
less work when actually removing the modpaths from modules for good.
Assuming no assertion fails, the new code is in particular equivalent to
the old one.

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