Merge PR coq#20060: Stop storing the module path in modules.

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

checker/mod_checking.ml

@@ -195,7 +195,7 @@ let lookup_module mp env =
   with Not_found ->
     failwith ("Unknown module: "^ModPath.to_string mp)
 
-let mk_mtb mp sign delta = Mod_declarations.make_module_type mp sign delta
+let mk_mtb sign delta = Mod_declarations.make_module_type sign delta
 
 let rec collect_constants_without_body sign mp accu =
   let collect_field s lab = function
@@ -212,16 +212,16 @@ let rec collect_constants_without_body sign mp accu =
 let rec check_mexpr env opac mse mp_mse res = match mse with
   | MEident mp ->
     let mb = lookup_module mp env in
-    let mb = Modops.strengthen_and_subst_module_body mb mp_mse false in
+    let mb = Modops.strengthen_and_subst_module_body mp mb mp_mse false in
     mod_type mb, mod_delta mb
   | MEapply (f,mp) ->
     let sign, delta = check_mexpr env opac f mp_mse res in
     let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
     let mtb = Modops.module_type_of_module (lookup_module mp env) in
     let state = (Environ.universes env, Conversion.checked_universes) in
-    let _ : UGraph.t = Subtyping.check_subtypes state env mtb farg_b in
+    let _ : UGraph.t = Subtyping.check_subtypes state env mp mtb (MPbound farg_id) farg_b in
     let subst = Mod_subst.map_mbid farg_id mp Mod_subst.empty_delta_resolver in
-    Modops.subst_signature subst fbody_b, Mod_subst.subst_codom_delta_resolver subst delta
+    Modops.subst_signature subst mp_mse fbody_b, Mod_subst.subst_codom_delta_resolver subst delta
   | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation")
 
 let rec check_mexpression env opac sign mbtyp mp_mse res = match sign with
@@ -235,7 +235,6 @@ 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) mp (mod_delta mb) opacify
   in
@@ -252,17 +251,16 @@ let rec check_module env opac mp mb opacify =
   let () = match optsign with
   | None -> ()
   | Some (sign,delta) ->
-    let mtb1 = mk_mtb mp sign delta
-    and mtb2 = mk_mtb mp (mod_type mb) (mod_delta mb) in
+    let mtb1 = mk_mtb sign delta
+    and mtb2 = mk_mtb (mod_type mb) (mod_delta mb) in
     let env = Modops.add_module_type mp mtb1 env in
     let state = (Environ.universes env, Conversion.checked_universes) in
-    let _ : UGraph.t = Subtyping.check_subtypes state env mtb1 mtb2 in
+    let _ : UGraph.t = Subtyping.check_subtypes state env mp mtb1 mp mtb2 in
     ()
   in
   opac
 
 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) mp (mod_delta mty) Cset.empty in
@@ -277,11 +275,13 @@ and check_structure_field env opac mp lab res opacify = function
       let kn = Mod_subst.mind_of_delta_kn res kn in
       CheckInductive.check_inductive env kn mib, opac
   | SFBmodule msb ->
-      let opac = check_module env opac (MPdot(mp,lab)) msb opacify in
-      Modops.add_module msb env, opac
+      let mp = MPdot(mp, lab) in
+      let opac = check_module env opac mp msb opacify in
+      Modops.add_module mp msb env, opac
   | SFBmodtype mty ->
-      let () = check_module_type env (MPdot (mp, lab)) mty in
-      add_modtype mty env, opac
+      let mp = MPdot (mp, lab) in
+      let () = check_module_type env mp mty in
+      add_modtype mp mty env, opac
   | SFBrules rrb ->
       check_rewrite_rules_body env lab rrb;
       Environ.add_rewrite_rules rrb.rewrules_rules env, opac

checker/safe_checking.ml

@@ -12,21 +12,19 @@ open Environ
 
 let import senv opac clib vmtab digest =
   let senv = Safe_typing.check_flags_for_library clib senv in
+  let dp = Safe_typing.dirpath_of_library clib in
   let mb = Safe_typing.module_of_library clib in
   let env = Safe_typing.env_of_safe_env senv in
   let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in
   let env = Modops.add_retroknowledge (Mod_declarations.mod_retroknowledge mb) env in
   let env = Environ.link_vm_library vmtab env in
-  let opac = Mod_checking.check_module env opac (Mod_declarations.mod_mp mb) mb in
+  let opac = Mod_checking.check_module env opac (Names.ModPath.MPfile dp) mb in
   let (_,senv) = Safe_typing.import clib vmtab digest senv in senv, opac
 
 let import senv opac clib vmtab digest : _ * _ =
   NewProfile.profile "import"
     ~args:(fun () ->
-        let dp = match Mod_declarations.mod_mp (Safe_typing.module_of_library clib) with
-          | MPfile dp -> dp
-          | _ -> assert false
-        in
+        let dp = Safe_typing.dirpath_of_library clib in
         [("name", `String (Names.DirPath.to_string dp))])
     (fun () ->import senv opac clib vmtab digest)
     ()

checker/values.ml

@@ -572,10 +572,10 @@ let [_v_sfb;_v_struc;_v_sign;_v_mexpr;_v_impl;v_module;_v_modtype] : _ Vector.t
            [|v_struc|]|])  (* Struct *)
   and v_module =
     v_tuple_c ("module_body",
-           [|v_mp;v_sum_c ("when_mod_body", 0, [|[|v_impl|]|]);v_sign;v_opt v_mexpr;v_resolver;v_retroknowledge|])
+           [|v_sum_c ("when_mod_body", 0, [|[|v_impl|]|]);v_sign;v_opt v_mexpr;v_resolver;v_retroknowledge|])
   and v_modtype =
     v_tuple_c ("module_type_body",
-           [|v_mp;v_noimpl;v_sign;v_opt v_mexpr;v_resolver;v_unit|])
+           [|v_noimpl;v_sign;v_opt v_mexpr;v_resolver;v_unit|])
   in
   [v_sfb;v_struc;v_sign;v_mexpr;v_impl;v_module;v_modtype])
 

kernel/environ.ml

@@ -854,14 +854,12 @@ let keep_hyps env needed =
 
 (* Modules *)
 
-let add_modtype mtb env =
-  let mp = mod_mp mtb in
+let add_modtype mp mtb env =
   let new_modtypes = MPmap.add mp mtb env.env_globals.Globals.modtypes in
   let new_globals = { env.env_globals with Globals.modtypes = new_modtypes } in
   { env with env_globals = new_globals }
 
-let shallow_add_module mb env =
-  let mp = mod_mp mb in
+let shallow_add_module mp mb env =
   let new_mods = MPmap.add mp mb env.env_globals.Globals.modules in
   let new_globals = { env.env_globals with Globals.modules = new_mods } in
   { env with env_globals = new_globals }

kernel/environ.mli

@@ -346,10 +346,10 @@ module QGlobRef : QNameS with type t = GlobRef.t
 
 (** {5 Modules } *)
 
-val add_modtype : module_type_body -> env -> env
+val add_modtype : ModPath.t -> module_type_body -> env -> env
 
 (** [shallow_add_module] does not add module components *)
-val shallow_add_module : module_body -> env -> env
+val shallow_add_module : ModPath.t -> module_body -> env -> env
 
 val lookup_module : ModPath.t -> env -> module_body
 val lookup_modtype : ModPath.t -> env -> module_type_body

kernel/mod_declarations.ml

@@ -31,8 +31,7 @@ and module_implementation =
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
 and 'a generic_module_body =
-  { mod_mp : ModPath.t; (** absolute path of the module *)
-    mod_expr : ('a, module_implementation) when_mod_body; (** implementation *)
+  { mod_expr : ('a, module_implementation) when_mod_body; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     mod_type_alg : module_expression option; (** algebraic type *)
     mod_delta : Mod_subst.delta_resolver; (**
@@ -70,28 +69,24 @@ type 'a module_retroknowledge = ('a, Retroknowledge.action list) when_mod_body
 
 (** Builders *)
 
-let make_module_body mp typ delta retro = {
-  mod_mp = mp;
+let make_module_body typ delta retro = {
   mod_expr = ModBodyVal FullStruct;
   mod_type = typ;
   mod_type_alg = None;
   mod_delta = delta;
   mod_retroknowledge = ModBodyVal retro;
 }
 
-let make_module_type mp typ delta = {
-  mod_mp = mp;
+let make_module_type typ delta = {
   mod_expr = ModTypeNul;
   mod_type = typ;
   mod_type_alg = None;
   mod_delta = delta;
   mod_retroknowledge = ModTypeNul;
 }
 
-let strengthen_module_body ~src ~dst typ delta mb =
-  let mp = match dst with None -> mb.mod_mp | Some mp -> mp in
+let strengthen_module_body ~src typ delta mb =
   { mb with
-    mod_mp = mp;
     mod_expr = ModBodyVal (Algebraic (MENoFunctor (MEident src)));
     mod_type = typ;
     mod_delta = delta; }
@@ -114,9 +109,8 @@ let module_type_of_module mb =
   { mb with mod_expr = ModTypeNul; mod_type_alg = None;
     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;
+let module_body_of_type mtb =
+  { mtb with mod_expr = ModBodyVal Abstract;
       mod_retroknowledge = ModBodyVal []; }
 
 (** Setters *)
@@ -132,7 +126,6 @@ let set_retroknowledge mb rk =
 
 (** Accessors *)
 
-let mod_mp { mod_mp = mp; _ } = mp
 let mod_expr { mod_expr = ModBodyVal v; _ } = v
 let mod_type m = m.mod_type
 let mod_type_alg m = m.mod_type_alg
@@ -209,23 +202,20 @@ and hcons_module_implementation mip = match mip with
 and hcons_generic_module_body :
   'a. 'a generic_module_body -> 'a generic_module_body =
   fun mb ->
-  let mp' = mb.mod_mp in
   let expr' = hcons_when_mod_body hcons_module_implementation mb.mod_expr in
   let type' = hcons_module_signature mb.mod_type in
   let type_alg' = mb.mod_type_alg in
   let delta' = mb.mod_delta in
   let retroknowledge' = mb.mod_retroknowledge in
 
   if
-    mb.mod_mp == mp' &&
     mb.mod_expr == expr' &&
     mb.mod_type == type' &&
     mb.mod_type_alg == type_alg' &&
     mb.mod_delta == delta' &&
     mb.mod_retroknowledge == retroknowledge'
   then mb
   else {
-    mod_mp = mp';
     mod_expr = expr';
     mod_type = type';
     mod_type_alg = type_alg';
@@ -243,7 +233,7 @@ let hcons_module_type =
 
 let rec functor_smart_map fty f0 funct = match funct with
   | MoreFunctor (mbid,ty,e) ->
-    let ty' = fty ty in
+    let ty' = fty mbid ty in
     let e' = functor_smart_map fty f0 e in
     if ty==ty' && e==e' then funct else MoreFunctor (mbid,ty',e')
   | NoFunctor a ->
@@ -285,7 +275,7 @@ let subst_with_body subst = function
     let c' = subst_mps subst c in
     if c==c' then orig else WithDef(id,(c',ctx))
 
-let rec subst_structure subst do_delta sign =
+let rec subst_structure subst do_delta mp sign =
   let subst_field ((l,body) as orig) = match body with
     | SFBconst cb ->
       let cb' = subst_const_body subst cb in
@@ -297,10 +287,10 @@ let rec subst_structure subst do_delta sign =
       let rrb' = subst_rewrite_rules subst rrb in
       if rrb==rrb' then orig else (l,SFBrules rrb')
     | SFBmodule mb ->
-      let mb' = subst_module subst do_delta mb in
+      let mb' = subst_module subst do_delta (MPdot (mp, l)) mb in
       if mb==mb' then orig else (l,SFBmodule mb')
     | SFBmodtype mtb ->
-      let mtb' = subst_modtype subst do_delta mtb in
+      let mtb' = subst_modtype subst do_delta (MPdot (mp, l)) mtb in
       if mtb==mtb' then orig else (l,SFBmodtype mtb')
   in
   List.Smart.map subst_field sign
@@ -313,42 +303,41 @@ and subst_retro : type a. Mod_subst.substitution -> a module_retroknowledge -> a
       let l' = List.Smart.map (subst_retro_action subst) l in
       if l == l' then r else ModBodyVal l
 
-and subst_module_body : type a. _ -> _ -> _ -> a generic_module_body -> a generic_module_body =
-  fun is_mod subst do_delta mb ->
-    let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty;
+and subst_module_body : type a. _ -> _ -> _ -> _ -> a generic_module_body -> a generic_module_body =
+  fun is_mod subst do_delta mp mb ->
+    let { mod_expr=me; mod_type=ty; mod_type_alg=aty;
           mod_retroknowledge=retro; _ } = mb in
   let mp' = subst_mp subst mp in
   let subst =
     if ModPath.equal mp mp' then subst
     else if is_mod && not (is_functor ty) then subst
     else add_mp mp mp' empty_delta_resolver subst
   in
-  let ty' = subst_signature subst do_delta ty in
-  let me' = subst_impl subst me in
+  let ty' = subst_signature subst do_delta mp ty in
+  let me' = subst_impl subst mp me in
   let aty' = Option.Smart.map (subst_expression subst id_delta) aty in
   let retro' = subst_retro subst retro in
   let delta' = do_delta mb.mod_delta subst in
   if mp==mp' && me==me' && ty==ty' && aty==aty'
      && retro==retro' && delta'==mb.mod_delta
   then mb
   else
-    { mod_mp = mp';
-      mod_expr = me';
+    { mod_expr = me';
       mod_type = ty';
       mod_type_alg = aty';
       mod_retroknowledge = retro';
       mod_delta = delta';
     }
 
-and subst_module subst do_delta mb =
-  subst_module_body true subst do_delta mb
+and subst_module subst do_delta mp mb =
+  subst_module_body true subst do_delta mp mb
 
-and subst_impl : type a. _ -> (a, _) when_mod_body -> (a, _) when_mod_body =
-  fun subst me ->
+and subst_impl : type a. _ -> _ -> (a, _) when_mod_body -> (a, _) when_mod_body =
+  fun subst mp me ->
   implem_smart_map
-    (subst_structure subst id_delta) (subst_expression subst id_delta) me
+    (fun sign -> subst_structure subst id_delta mp sign) (subst_expression subst id_delta) me
 
-and subst_modtype subst do_delta mtb = subst_module_body false subst do_delta mtb
+and subst_modtype subst do_delta mp mtb = subst_module_body false subst do_delta mp mtb
 
 and subst_expr subst do_delta seb = match seb with
   | MEident mp ->
@@ -371,10 +360,10 @@ and subst_expression subst do_delta me = match me with
   let mf' = subst_expression subst do_delta mf in
   if mf == mf' then me else MEMoreFunctor mf'
 
-and subst_signature subst do_delta =
+and subst_signature subst do_delta mp =
   functor_smart_map
-    (subst_modtype subst do_delta)
-    (subst_structure subst do_delta)
+    (fun mbid mtb -> subst_modtype subst do_delta (MPbound mbid) mtb)
+    (fun sign -> subst_structure subst do_delta mp sign)
 
 (** Cleaning a module expression from bounded parts
 
@@ -409,7 +398,7 @@ and clean_field l field = match field with
 and clean_structure l = List.Smart.map (clean_field l)
 
 and clean_signature l =
-  functor_smart_map (clean_module_body l) (clean_structure l)
+  functor_smart_map (fun _ mb -> clean_module_body l mb) (clean_structure l)
 
 and clean_expression _ me = me
 

kernel/mod_declarations.mli

@@ -60,7 +60,6 @@ type 'a module_retroknowledge = ('a, Retroknowledge.action list) when_mod_body
 
 (** {6 Accessors} *)
 
-val mod_mp : 'a generic_module_body -> ModPath.t
 val mod_expr : module_body -> module_implementation
 val mod_type : 'a generic_module_body -> module_signature
 val mod_type_alg : 'a generic_module_body -> module_expression option
@@ -69,10 +68,10 @@ val mod_retroknowledge : module_body -> Retroknowledge.action list
 
 (** {6 Builders} *)
 
-val make_module_body : ModPath.t -> module_signature -> Mod_subst.delta_resolver -> Retroknowledge.action list -> module_body
-val make_module_type : ModPath.t -> module_signature -> Mod_subst.delta_resolver -> module_type_body
+val make_module_body : module_signature -> Mod_subst.delta_resolver -> Retroknowledge.action list -> module_body
+val make_module_type : module_signature -> Mod_subst.delta_resolver -> module_type_body
 
-val strengthen_module_body : src:ModPath.t -> dst:ModPath.t option ->
+val strengthen_module_body : src:ModPath.t ->
   module_signature -> delta_resolver -> module_body -> module_body
 
 val strengthen_module_type :
@@ -81,7 +80,7 @@ val strengthen_module_type :
 val replace_module_body : structure_body -> delta_resolver -> module_body -> module_body
 
 val module_type_of_module : module_body -> module_type_body
-val module_body_of_type : ModPath.t -> module_type_body -> module_body
+val module_body_of_type : module_type_body -> module_body
 
 val functorize_module : (Names.MBId.t * module_type_body) list -> module_body -> module_body
 
@@ -101,22 +100,22 @@ val implem_smart_map :
   ('a, module_implementation) when_mod_body ->
   ('a, module_implementation) when_mod_body
 
-val functor_smart_map : ('a -> 'a) -> ('b -> 'b) ->
+val functor_smart_map : (MBId.t -> 'a -> 'a) -> ('b -> 'b) ->
   ('a, 'b) functorize -> ('a, 'b) functorize
 
 (** {6 Substitution} *)
 
 val subst_signature : substitution ->
-  (delta_resolver -> substitution -> delta_resolver) -> module_signature -> module_signature
+  (delta_resolver -> substitution -> delta_resolver) -> ModPath.t -> module_signature -> module_signature
 
 val subst_structure : substitution ->
-  (delta_resolver -> substitution -> delta_resolver) -> structure_body -> structure_body
+  (delta_resolver -> substitution -> delta_resolver) -> ModPath.t -> structure_body -> structure_body
 
 val subst_module : substitution ->
-  (delta_resolver -> substitution -> delta_resolver) -> module_body -> module_body
+  (delta_resolver -> substitution -> delta_resolver) -> ModPath.t -> module_body -> module_body
 
 val subst_modtype : substitution ->
-  (delta_resolver -> substitution -> delta_resolver) -> module_type_body -> module_type_body
+  (delta_resolver -> substitution -> delta_resolver) -> ModPath.t -> module_type_body -> module_type_body
 
 (** {6 Hashconsing} *)