Stop storing the module path in modules.

This data does not belong semantically here. Instead, it should be derived
from the context, as it is alway in sync with the name through which the
module was added to the environment.

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