From 3eabc97f756b7fc91c2730d4c869cd918e155967 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 9 Jan 2025 11:31:30 +0100 Subject: [PATCH] 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 | 26 ++++++------- checker/safe_checking.ml | 8 ++-- checker/values.ml | 4 +- kernel/environ.ml | 6 +-- kernel/environ.mli | 4 +- kernel/mod_declarations.ml | 63 +++++++++++++------------------ kernel/mod_declarations.mli | 19 +++++----- kernel/mod_typing.ml | 42 +++++++++++---------- kernel/modops.ml | 44 ++++++++++----------- kernel/modops.mli | 12 +++--- kernel/nativelibrary.ml | 2 - kernel/safe_typing.ml | 44 ++++++++++----------- kernel/safe_typing.mli | 1 + kernel/subtyping.ml | 14 ++----- kernel/subtyping.mli | 3 +- plugins/extraction/extract_env.ml | 2 - vernac/assumptions.ml | 4 +- vernac/declaremods.ml | 14 +++---- 18 files changed, 142 insertions(+), 170 deletions(-) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 29ffc26f9f06..afc267c53c2f 100644 --- a/checker/mod_checking.ml +++ b/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 diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml index 6bc38d235a01..2a8a0486f1da 100644 --- a/checker/safe_checking.ml +++ b/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) () diff --git a/checker/values.ml b/checker/values.ml index bcb073a46223..6b38acfed041 100644 --- a/checker/values.ml +++ b/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]) diff --git a/kernel/environ.ml b/kernel/environ.ml index d77b2a165af7..bfb49382432f 100644 --- a/kernel/environ.ml +++ b/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 } diff --git a/kernel/environ.mli b/kernel/environ.mli index 773e461417d7..54d7b8b9ca2e 100644 --- a/kernel/environ.mli +++ b/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 diff --git a/kernel/mod_declarations.ml b/kernel/mod_declarations.ml index 3e0d7d989bed..cd93fb4e6d2e 100644 --- a/kernel/mod_declarations.ml +++ b/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,8 +69,7 @@ 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; @@ -79,8 +77,7 @@ let make_module_body mp typ delta retro = { 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; @@ -88,10 +85,8 @@ let make_module_type mp typ 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,7 +202,6 @@ 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 @@ -217,7 +209,6 @@ and hcons_generic_module_body : 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' && @@ -225,7 +216,6 @@ and hcons_generic_module_body : 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,9 +303,9 @@ 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 = @@ -323,8 +313,8 @@ and subst_module_body : type a. _ -> _ -> _ -> a generic_module_body -> a generi 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 @@ -332,23 +322,22 @@ and subst_module_body : type a. _ -> _ -> _ -> a generic_module_body -> a generi && 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 diff --git a/kernel/mod_declarations.mli b/kernel/mod_declarations.mli index 4fe483a10030..1a816fd22302 100644 --- a/kernel/mod_declarations.mli +++ b/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} *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index f84f92de7120..ff7035a1ef39 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -153,6 +153,8 @@ let rec check_with_def (cst, ustate) env struc (idl, wth) mp reso = with | Not_found -> error_no_such_label lab mp +(* [mp] is the ambient modpath of [struc], + [new_mp] is the path of the module to replace [idl] with *) let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso = let lab,idl = match idl with | [] -> assert false @@ -172,7 +174,7 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso = let cst = match Mod_declarations.mod_expr old with | Abstract -> let mtb_old = module_type_of_module old in - let cst = Subtyping.check_subtypes (cst, ustate) env' new_mtb mtb_old in + let cst = Subtyping.check_subtypes (cst, ustate) env' new_mp new_mtb (MPdot (mp, lab)) mtb_old in cst | Algebraic (MENoFunctor (MEident(mp'))) -> check_modpath_equiv env' new_mp mp'; @@ -180,14 +182,14 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso = | _ -> error_generative_module_expected lab in let mp' = MPdot (mp,lab) in - let new_mb = strengthen_and_subst_module_body new_mb mp' false in + let new_mb = strengthen_and_subst_module_body new_mp new_mb mp' false in (** TODO: check this is fine when new_mb is a functor *) - let new_mb' = strengthen_module_body ~src:new_mp ~dst:(Some mp') (mod_type new_mb) (mod_delta new_mb) new_mb in + let new_mb' = strengthen_module_body ~src:new_mp (mod_type new_mb) (mod_delta new_mb) new_mb in let new_reso = add_delta_resolver reso (mod_delta new_mb) in (* we propagate the new equality in the rest of the signature with the identity substitution accompanied by the new resolver*) let id_subst = map_mp mp' mp' (mod_delta new_mb) in - let new_after = subst_structure id_subst after in + let new_after = subst_structure id_subst mp after in before@(lab,SFBmodule new_mb')::new_after, new_reso, cst else (* Module definition of a sub-module *) @@ -205,7 +207,7 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso = let new_mb = replace_module_body struc' reso' old in let new_reso = add_delta_resolver reso reso' in let id_subst = map_mp mp' mp' reso' in - let new_after = subst_structure id_subst after in + let new_after = subst_structure id_subst mp after in before@(lab,SFBmodule new_mb)::new_after, new_reso, cst | Algebraic (MENoFunctor (MEident mp0)) -> let mpnew = rebuild_mp mp0 idl in @@ -236,14 +238,14 @@ let check_with_alg ustate vmstate env mp (sign, alg, reso, cst, vm) wd = let struc, reso, cst, vm = check_with ustate vmstate env mp (sign, reso, cst, vm) wd in struc, MEwith (alg, wd), reso, cst, vm -let translate_apply ustate env inl (sign,alg,reso,cst,vm) mp1 mkalg = +let translate_apply ustate env inl mp (sign,alg,reso,cst,vm) mp1 mkalg = let farg_id, farg_b, fbody_b = destr_functor sign in let mtb = module_type_of_module (lookup_module mp1 env) in - let cst = Subtyping.check_subtypes (cst, ustate) env mtb farg_b in + let cst = Subtyping.check_subtypes (cst, ustate) env mp1 mtb (MPbound farg_id) farg_b in let mp_delta = discr_resolver mtb in let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in let subst = map_mbid farg_id mp1 mp_delta in - let body = subst_signature subst fbody_b in + let body = subst_signature subst mp fbody_b in let alg' = mkalg alg mp1 in let reso' = subst_codom_delta_resolver subst reso in body, alg', reso', cst, vm @@ -260,15 +262,15 @@ let mk_alg_app alg arg = MEapply (alg,arg) let rec translate_mse (cst, ustate) (vm, vmstate) env mpo inl = function | MEident mp1 as me -> let mb = match mpo with - | Some mp -> strengthen_and_subst_module_body (lookup_module mp1 env) mp false + | Some mp -> strengthen_and_subst_module_body mp1 (lookup_module mp1 env) mp false | None -> let mt = lookup_modtype mp1 env in - let () = assert (ModPath.equal mp1 (mod_mp mt)) in - module_body_of_type mp1 mt + module_body_of_type mt in mod_type mb, me, mod_delta mb, cst, vm | MEapply (fe,mp1) -> - translate_apply ustate env inl (translate_mse (cst, ustate) (vm, vmstate) env mpo inl fe) mp1 mk_alg_app + let mp = match mpo with Some mp -> mp | None -> mp_from_mexpr fe in + translate_apply ustate env inl mp (translate_mse (cst, ustate) (vm, vmstate) env mpo inl fe) mp1 mk_alg_app | MEwith(me, with_decl) -> assert (Option.is_empty mpo); (* No 'with' syntax for modules *) let mp = mp_from_mexpr me in @@ -293,7 +295,7 @@ let rec translate_mse_funct (cst, ustate) (vm, vmstate) env ~is_mod mp inl mse = and translate_modtype state vmstate env mp inl (params,mte) = let sign,alg,reso,cst,vm = translate_mse_funct state vmstate env ~is_mod:false mp inl mte params in - let mtb = mk_modtype mp sign reso in + let mtb = mk_modtype sign reso in set_algebraic_type mtb alg, cst, vm (** [finalize_module] : @@ -303,13 +305,13 @@ and translate_modtype state vmstate env mp inl (params,mte) = let finalize_module_alg (cst, ustate) (vm, vmstate) env mp (sign,alg,reso) restype = match restype with | None -> let impl = match alg with Some e -> Algebraic e | None -> FullStruct in - let mb = make_module_body mp sign reso [] in + let mb = make_module_body sign reso [] in let mb = set_implementation impl mb in mb, cst, vm | Some (params_mte,inl) -> let res_mtb, cst, vm = translate_modtype (cst, ustate) (vm, vmstate) env mp inl params_mte in - let auto_mtb = mk_modtype mp sign reso in - let cst = Subtyping.check_subtypes (cst, ustate) env auto_mtb res_mtb in + let auto_mtb = mk_modtype sign reso in + let cst = Subtyping.check_subtypes (cst, ustate) env mp auto_mtb mp res_mtb in let impl = match alg with | Some e -> Algebraic e | None -> @@ -319,7 +321,7 @@ let finalize_module_alg (cst, ustate) (vm, vmstate) env mp (sign,alg,reso) resty in Struct sign in - let mb = module_body_of_type mp res_mtb in + let mb = module_body_of_type res_mtb in let mb = set_implementation impl mb in mb, (** constraints from module body typing + subtyping + module type. *) @@ -332,7 +334,7 @@ let finalize_module univs vm env mp (sign, reso) typ = let translate_module (cst, ustate) (vm, vmstate) env mp inl = function | MType (params,ty) -> let mtb, cst, vm = translate_modtype (cst, ustate) (vm, vmstate) env mp inl (params,ty) in - module_body_of_type mp mtb, cst, vm + module_body_of_type mtb, cst, vm | MExpr (params,mse,oty) -> let (sg,alg,reso,cst,vm) = translate_mse_funct (cst, ustate) (vm, vmstate) env ~is_mod:true mp inl mse params in let restype = Option.map (fun ty -> ((params,ty),inl)) oty in @@ -363,12 +365,12 @@ let rec forbid_incl_signed_functor env = function let rec translate_mse_include_module (cst, ustate) (vm, vmstate) env mp inl = function | MEident mp1 -> - let mb = strengthen_and_subst_module_body (lookup_module mp1 env) mp true in + let mb = strengthen_and_subst_module_body mp1 (lookup_module mp1 env) mp true in let sign = clean_bounded_mod_expr (mod_type mb) in sign, (), mod_delta mb, cst, vm | MEapply (fe,arg) -> let ftrans = translate_mse_include_module (cst, ustate) (vm, vmstate) env mp inl fe in - translate_apply ustate env inl ftrans arg (fun _ _ -> ()) + translate_apply ustate env inl mp ftrans arg (fun _ _ -> ()) | MEwith _ -> assert false (* No 'with' syntax for modules *) let translate_mse_include is_mod (cst, ustate) (vm, vmstate) env mp inl me = diff --git a/kernel/modops.ml b/kernel/modops.ml index 97e8cd107fd4..30cd2ed08931 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -180,32 +180,31 @@ let rec add_structure mp sign resolver linkinfo env = else mib in Environ.add_mind_key mind (mib,ref linkinfo) env - | SFBmodule mb -> add_module mb linkinfo env (* adds components as well *) - | SFBmodtype mtb -> Environ.add_modtype mtb env + | SFBmodule mb -> add_module (MPdot (mp, l)) mb linkinfo env (* adds components as well *) + | SFBmodtype mtb -> Environ.add_modtype (MPdot (mp, l)) mtb env | SFBrules r -> Environ.add_rewrite_rules r.rewrules_rules env in List.fold_left add_field env sign -and add_module mb linkinfo env = - let mp = mod_mp mb in - let env = Environ.shallow_add_module mb env in +and add_module mp mb linkinfo env = + let env = Environ.shallow_add_module mp mb env in match mod_type mb with | NoFunctor struc -> add_retroknowledge (mod_retroknowledge mb) (add_structure mp struc (mod_delta mb) linkinfo env) | MoreFunctor _ -> env -let add_linked_module mb linkinfo env = - add_module mb linkinfo env +let add_linked_module mp mb linkinfo env = + add_module mp mb linkinfo env let add_structure mp sign resolver env = add_structure mp sign resolver no_link_info env -let add_module mb env = - add_module mb no_link_info env +let add_module mp mb env = + add_module mp mb no_link_info env let add_module_type mp mtb env = - add_module (module_body_of_type mp mtb) env + add_module mp (module_body_of_type mtb) env (** {6 Strengthening a signature for subtyping } *) @@ -221,13 +220,12 @@ 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 = - 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 let reso = add_mp_delta_resolver mp_from mp_to (add_delta_resolver (mod_delta mb) reso) in - strengthen_module_body ~src:mp_to ~dst:None (NoFunctor struc') reso mb + strengthen_module_body ~src:mp_to (NoFunctor struc') reso mb | MoreFunctor _ -> mb and strengthen_signature mp_from struc mp_to reso = match struc with @@ -251,7 +249,6 @@ 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 mp (mod_delta mtb) then mtb else match mod_type mtb with @@ -264,21 +261,20 @@ let strengthen mtb mp = (** {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 mp_from (mod_delta mb) in - if mb_is_an_alias then subst_module subst do_delta_dom mb + if mb_is_an_alias then subst_module subst do_delta_dom mp_from mb else let reso',struc' = strengthen_and_subst_struct struc subst mp_from mp_to false false (mod_delta mb) in 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 + strengthen_module_body ~src:mp_from (NoFunctor struc') reso' mb | MoreFunctor _ -> let subst = add_mp mp_from mp_to empty_delta_resolver subst in - subst_module subst do_delta_dom mb + subst_module subst do_delta_dom mp_from mb and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso = let strengthen_and_subst_field reso' item = match item with @@ -328,7 +324,7 @@ and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso = let mp_from' = MPdot (mp_from,l) in let mp_to' = MPdot (mp_to,l) in let mb' = if alias then - subst_module subst do_delta_dom mb + subst_module subst do_delta_dom mp_from' mb else strengthen_and_subst_module mb subst mp_from' mp_to' in @@ -347,6 +343,7 @@ and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso = let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in let mty' = subst_modtype subst' (fun resolver _ -> subst_dom_codom_delta_resolver subst' resolver) + mp_from' mty in let item' = if mty' == mty then item else (l, SFBmodtype mty') in @@ -370,9 +367,8 @@ and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso = - in the "Include" case: add a Delta-equivalence "t := t'" where "t'" is the canonical form of "P.t" on each field *) -let strengthen_and_subst_module_body mb mp include_b = match mod_type mb with +let strengthen_and_subst_module_body mp_from mb mp include_b = match mod_type mb with | NoFunctor struc -> - 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)*) @@ -388,15 +384,15 @@ let strengthen_and_subst_module_body mb mp include_b = match mod_type mb with 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:mp_from ~dst:(Some mp) (NoFunctor struc') reso' mb + strengthen_module_body ~src:mp_from (NoFunctor struc') reso' mb | MoreFunctor _ -> - 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 + subst_module subst do_delta_dom_codom mp_from mb +(* [mp_from] is the ambient modpath of [sign] *) let subst_modtype_signature_and_resolver mp_from mp_to sign reso = let subst = map_mp mp_from mp_to empty_delta_resolver in - subst_dom_codom_signature subst sign, subst_dom_codom_delta_resolver subst reso + subst_dom_codom_signature subst mp_from sign, subst_dom_codom_delta_resolver subst reso let rec collect_mbid l sign = match sign with | MoreFunctor (mbid,ty,m) -> diff --git a/kernel/modops.mli b/kernel/modops.mli index 7da30ab203ab..ea128ff383e4 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -29,7 +29,7 @@ val destr_nofunctor : ModPath.t -> ('ty,'a) functorize -> 'a (** Conversions between [module_body] and [module_type_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 check_modpath_equiv : env -> ModPath.t -> ModPath.t -> unit @@ -40,8 +40,8 @@ val annotate_struct_body : structure_body -> module_signature -> module_signatur (** {6 Substitutions } *) -val subst_signature : substitution -> module_signature -> module_signature -val subst_structure : substitution -> structure_body -> structure_body +val subst_signature : substitution -> ModPath.t -> module_signature -> module_signature +val subst_structure : substitution -> ModPath.t -> structure_body -> structure_body (** {6 Adding to an environment } *) @@ -49,11 +49,11 @@ val add_structure : ModPath.t -> structure_body -> delta_resolver -> env -> env (** adds a module and its components, but not the constraints *) -val add_module : module_body -> env -> env +val add_module : ModPath.t -> module_body -> env -> env (** same as add_module, but for a module whose native code has been linked by the native compiler. The linking information is updated. *) -val add_linked_module : module_body -> link_info -> env -> env +val add_linked_module : ModPath.t -> module_body -> link_info -> env -> env (** same, for a module type *) val add_module_type : ModPath.t -> module_type_body -> env -> env @@ -64,7 +64,7 @@ val add_retroknowledge : Retroknowledge.action list -> env -> env val strengthen : module_type_body -> ModPath.t -> module_type_body -val strengthen_and_subst_module_body : module_body -> ModPath.t -> bool -> module_body +val strengthen_and_subst_module_body : ModPath.t -> module_body -> ModPath.t -> bool -> module_body val subst_modtype_signature_and_resolver : ModPath.t -> ModPath.t -> module_signature -> delta_resolver -> module_signature * delta_resolver diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 75fa40815ac3..b3c04abd07d1 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -46,7 +46,6 @@ and translate_field mp env acc (l,x) = compile_rewrite_rules env l acc rrb | SFBmodule md -> 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) @@ -55,7 +54,6 @@ and translate_field mp env acc (l,x) = translate_mod mp env (mod_type md) acc | SFBmodtype mdtyp -> 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/safe_typing.ml b/kernel/safe_typing.ml index 9d49940eb0fc..ddd55395217a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -593,8 +593,8 @@ type generic_name = | C of Constant.t | I of MutInd.t | R - | M (** name already known, cf the mod_mp field *) - | MT (** name already known, cf the mod_mp field *) + | M of ModPath.t + | MT of ModPath.t let add_field ((l,sfb) as field) gn senv = let mlabs,olabs = match sfb with @@ -609,8 +609,8 @@ let add_field ((l,sfb) as field) gn senv = let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env - | SFBmodtype mtb, MT -> Environ.add_modtype mtb senv.env - | SFBmodule mb, M -> Modops.add_module mb senv.env + | SFBmodtype mtb, MT mp -> Environ.add_modtype mp mtb senv.env + | SFBmodule mb, M mp -> Modops.add_module mp mb senv.env | SFBrules r, R -> Environ.add_rewrite_rules r.rewrules_rules senv.env | _ -> assert false in @@ -624,7 +624,7 @@ let add_field ((l,sfb) as field) gn senv = | SFBmind mib, I mind -> let poly = Declareops.inductive_is_polymorphic mib in Some Section.(push_global ~poly env' (SecInductive mind) sections) - | _, (M | MT) -> Some sections + | _, (M _ | MT _) -> Some sections | _ -> assert false in { senv with @@ -1115,15 +1115,15 @@ let add_modtype l params_mte inl senv = let mtb, _, vmtab = Mod_typing.translate_modtype state vmstate senv.env mp inl params_mte in let senv = set_vm_library vmtab senv in let mtb = Mod_declarations.hcons_module_type mtb in - let senv = add_field (l,SFBmodtype mtb) MT senv in + let senv = add_field (l,SFBmodtype mtb) (MT mp) senv in mp, senv (** full_add_module adds module with universes and constraints *) -let full_add_module mb senv = - let dp = ModPath.dp (mod_mp mb) in +let full_add_module mp mb senv = + let dp = ModPath.dp mp in let linkinfo = Nativecode.link_info_of_dirpath dp in - { senv with env = Modops.add_linked_module mb linkinfo senv.env } + { senv with env = Modops.add_linked_module mp mb linkinfo senv.env } let full_add_module_type mp mt senv = { senv with env = Modops.add_module_type mp mt senv.env } @@ -1137,7 +1137,7 @@ let add_module l me inl senv = let mb, _, vmtab = Mod_typing.translate_module state vmstate senv.env mp inl me in let senv = set_vm_library vmtab senv in let mb = Mod_declarations.hcons_module_body mb in - let senv = add_field (l,SFBmodule mb) M senv in + let senv = add_field (l,SFBmodule mb) (M mp) senv in let senv = if Modops.is_functor @@ mod_type mb then senv else update_resolver (Mod_subst.add_delta_resolver @@ mod_delta mb) senv @@ -1220,7 +1220,7 @@ let functorize params init = let propagate_loads senv = List.fold_left - (fun env (_,mb) -> full_add_module mb env) + (fun env (mp, mb) -> full_add_module mp mb env) senv (List.rev senv.loads) @@ -1277,7 +1277,7 @@ let end_module l restype senv = let newenv = if Environ.rewrite_rules_allowed senv.env then Environ.allow_rewrite_rules newenv else newenv in let newenv = Environ.set_vm_library (Environ.vm_library senv.env) newenv in let senv' = propagate_loads { senv with env = newenv } in - let newenv = Modops.add_module mb senv'.env in + let newenv = Modops.add_module mp mb senv'.env in let newresolver = if Modops.is_functor @@ mod_type mb then oldsenv.modresolver else Mod_subst.add_delta_resolver (mod_delta mb) oldsenv.modresolver @@ -1298,8 +1298,8 @@ let end_modtype l senv = let newenv = Environ.set_vm_library (Environ.vm_library senv.env) newenv in let senv' = propagate_loads {senv with env=newenv} in let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in - let mtb = build_mtb mp auto_tb senv.modresolver in - let newenv = Environ.add_modtype mtb senv'.env in + let mtb = build_mtb auto_tb senv.modresolver in + let newenv = Environ.add_modtype mp mtb senv'.env in let newresolver = oldsenv.modresolver in (mp,mbids), propagate_senv (l,SFBmodtype mtb) newenv newresolver senv' oldsenv @@ -1317,18 +1317,18 @@ let add_include me is_module inl senv = let senv = set_vm_library vmtab senv in (* Include Self support *) let struc = NoFunctor (List.rev senv.revstruct) in - let mb = build_mtb mp_sup struc senv.modresolver in + let mb = build_mtb struc senv.modresolver in let rec compute_sign sign resolver = match sign with | MoreFunctor(mbid,mtb,str) -> let state = check_state senv in - let (_ : UGraph.t) = Subtyping.check_subtypes state senv.env mb mtb in + let (_ : UGraph.t) = Subtyping.check_subtypes state senv.env mp_sup mb (MPbound mbid) mtb in let mpsup_delta = Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb senv.modresolver in let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in - compute_sign (Modops.subst_signature subst str) resolver + compute_sign (Modops.subst_signature subst mp_sup str) resolver | NoFunctor str -> resolver, str in let resolver, str = compute_sign sign resolver in @@ -1340,8 +1340,8 @@ let add_include me is_module inl senv = | SFBmind _ -> I (Mod_subst.mind_of_delta_kn resolver (KerName.make mp_sup l)) | SFBrules _ -> R - | SFBmodule _ -> M - | SFBmodtype _ -> MT + | SFBmodule _ -> M (MPdot (mp_sup, l)) + | SFBmodtype _ -> MT (MPdot (mp_sup, l)) in add_field field new_name senv in @@ -1349,6 +1349,8 @@ let add_include me is_module inl senv = (** {6 Libraries, i.e. compiled modules } *) +let dirpath_of_library lib = lib.comp_name + let module_of_library lib = lib.comp_mod let univs_of_library lib = lib.comp_univs @@ -1392,7 +1394,7 @@ let export ~output_native_objects senv dir = let () = assert (Sorts.QVar.Set.is_empty senv.env.Environ.env_qualities) in let mp = senv.modpath in let str = NoFunctor (List.rev senv.revstruct) in - let mb = Mod_declarations.make_module_body mp str senv.modresolver senv.local_retroknowledge in + let mb = Mod_declarations.make_module_body str senv.modresolver senv.local_retroknowledge in let ast, symbols = if output_native_objects then Nativelibrary.dump_library mp senv.env str @@ -1428,7 +1430,7 @@ let import lib vmtab vodigest senv = let env = Environ.link_vm_library vmtab env in let env = let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in - Modops.add_linked_module mb linkinfo env + Modops.add_linked_module mp mb linkinfo env in let sections = Option.map (Section.map_custom (fun custom -> diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1cc7e65a16e5..7d985342bcf5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -229,6 +229,7 @@ val current_dirpath : safe_environment -> DirPath.t type compiled_library +val dirpath_of_library : compiled_library -> DirPath.t val module_of_library : compiled_library -> Mod_declarations.module_body val univs_of_library : compiled_library -> Univ.ContextSet.t val check_flags_for_library : compiled_library -> safe_transformer0 diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index fac647bca330..93d5708d614b 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -265,8 +265,6 @@ let check_constant (cst, ustate) trace env l info1 cb2 subst1 subst2 = check_conv NotConvertibleBodyField cst poly CONV env c1 c2)) 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 mp1 mty1 mp2 mty2 subst1 subst2 false @@ -297,16 +295,12 @@ and check_signatures (cst, ustate) trace env mp1 sig1 mp2 sig2 subst1 subst2 res in 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 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 = @@ -339,17 +333,15 @@ and check_modtypes (cst, ustate) trace env mp1 mtb1 mp2 mtb2 subst1 subst2 equiv let env = if Modops.is_functor body_t1 then env else - let mtb = make_module_type mp1 (subst_signature subst1 body_t1) (mod_delta mtb1) in - add_module (module_body_of_type mp1 mtb) env + let mtb = make_module_type (subst_signature subst1 mp1 body_t1) (mod_delta mtb1) in + add_module mp1 (module_body_of_type 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 mp_sup = mod_mp sup in - let mp_super = mod_mp super in +let check_subtypes state env mp_sup sup mp_super super = let env = add_module_type mp_sup sup env in check_modtypes state [] env mp_sup (strengthen sup mp_sup) mp_super super empty_subst diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index fa622a2d1f0a..f7a7fee3e6a1 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -8,7 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Mod_declarations open Environ -val check_subtypes : ('a, UGraph.univ_inconsistency) Conversion.universe_state -> env -> module_type_body -> module_type_body -> 'a +val check_subtypes : ('a, UGraph.univ_inconsistency) Conversion.universe_state -> env -> ModPath.t -> module_type_body -> ModPath.t -> module_type_body -> 'a diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 8dea38ae5b37..e97455d365de 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -224,13 +224,11 @@ let rec extract_structure_spec env mp reso = function | (l,SFBmodule mb) :: msig -> let specs = extract_structure_spec env mp reso msig 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 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 diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 35540f5f6e60..498c786c9812 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -84,13 +84,12 @@ 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 () = 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 + Modops.subst_structure subs mp fields 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 @@ -111,7 +110,6 @@ and fields_of_expr subs mp0 args = function | MEident mp -> 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] *) diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 6dcdea181174..5031b1108ce9 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -915,10 +915,10 @@ module Interp = struct (** {6 Auxiliary functions concerning subtyping checks} *) -let check_sub mtb sub_mtb_l = +let check_sub mp mtb sub_mtb_l = let fold sub_mtb (cst, env) = let state = ((Environ.universes env, cst), Reductionops.inferred_universes) in - let graph, cst = Subtyping.check_subtypes state env mtb sub_mtb in + let graph, cst = Subtyping.check_subtypes state env mp mtb mp sub_mtb in (cst, Environ.set_universes graph env) in let cst, _ = List.fold_right fold sub_mtb_l (Univ.Constraints.empty, Global.env ()) in @@ -933,7 +933,7 @@ let check_subtypes mp sub_mtb_l = try Global.lookup_module mp with Not_found -> assert false in let mtb = Modops.module_type_of_module mb in - check_sub mtb sub_mtb_l + check_sub mp mtb sub_mtb_l (** Same for module type [mp] *) @@ -941,7 +941,7 @@ let check_subtypes_mt mp sub_mtb_l = let mtb = try Global.lookup_modtype mp with Not_found -> assert false in - check_sub mtb sub_mtb_l + check_sub mp mtb sub_mtb_l let current_modresolver () = fst @@ Safe_typing.delta_of_senv @@ Global.safe_env () @@ -1381,18 +1381,18 @@ let declare_one_include_core (me,base,kind,inl) = let () = Global.add_constraints cst in let () = assert (ModPath.equal cur_mp (Global.current_modpath ())) in (* Include Self support *) - let mb = make_module_type cur_mp (RawModOps.Interp.current_struct ()) (RawModOps.Interp.current_modresolver ()) in + let mb = make_module_type (RawModOps.Interp.current_struct ()) (RawModOps.Interp.current_modresolver ()) in let rec compute_sign sign = match sign with | MoreFunctor(mbid,mtb,str) -> let state = ((Global.universes (), Univ.Constraints.empty), Reductionops.inferred_universes) in - let (_, cst) = Subtyping.check_subtypes state (Global.env ()) mb mtb in + let (_, cst) = Subtyping.check_subtypes state (Global.env ()) cur_mp mb (MPbound mbid) mtb in let () = Global.add_constraints cst in let mpsup_delta = Modops.inline_delta_resolver (Global.env ()) inl cur_mp mbid mtb (mod_delta mb) in let subst = Mod_subst.map_mbid mbid cur_mp mpsup_delta in - compute_sign (Modops.subst_signature subst str) + compute_sign (Modops.subst_signature subst cur_mp str) | NoFunctor str -> () in let () = compute_sign sign in