aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/safe_typing.ml11
-rw-r--r--kernel/safe_typing.mli3
-rw-r--r--library/declaremods.ml132
-rw-r--r--library/declaremods.mli6
-rw-r--r--library/global.ml4
-rw-r--r--library/global.mli1
6 files changed, 61 insertions, 96 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a1b820466..851803621 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -616,7 +616,6 @@ let end_modtype l senv =
local_retroknowledge =
senv.local_retroknowledge@oldsenv.local_retroknowledge}
-let current_modpath senv = senv.modinfo.modpath
let delta_of_senv senv = senv.modinfo.resolver,senv.modinfo.resolver_of_param
(* Check that the engagement expected by a library matches the initial one *)
@@ -679,16 +678,6 @@ let start_library dir senv =
loads = [];
local_retroknowledge = [] }
-let pack_module senv =
- {mod_mp=senv.modinfo.modpath;
- mod_expr=None;
- mod_type= SEBstruct (List.rev senv.revstruct);
- mod_type_alg=None;
- mod_constraints=empty_constraint;
- mod_delta=senv.modinfo.resolver;
- mod_retroknowledge=[];
- }
-
let export senv dir =
let modinfo = senv.modinfo in
begin
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index cd24bd8d0..46dac02aa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -91,10 +91,7 @@ val add_include :
module_struct_entry -> bool -> inline -> safe_environment ->
delta_resolver * safe_environment
-val pack_module : safe_environment -> module_body
-val current_modpath : safe_environment -> module_path
val delta_of_senv : safe_environment -> delta_resolver*delta_resolver
-
(** Loading and saving compilation units *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 303641596..992ca42fc 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -456,18 +456,18 @@ let rec compute_subst env mbids sign mp_l inl =
in
mbid_left,join (map_mbid mbid mp resolver) subst
-let rec get_modtype_substobjs env mp_from inline = function
- MSEident ln ->
- MPmap.find ln !modtypetab
+let rec get_modtype_substobjs env inline = function
+ | MSEident ln ->
+ MPmap.find ln !modtypetab
| MSEfunctor (mbid,_,mte) ->
- let (mbids, mp, objs) = get_modtype_substobjs env mp_from inline mte in
- (mbid::mbids, mp, objs)
+ let (mbids, mp, objs) = get_modtype_substobjs env inline mte in
+ (mbid::mbids, mp, objs)
| MSEwith (mty, With_Definition _) ->
- get_modtype_substobjs env mp_from inline mty
- | MSEwith (mty, With_Module (idl,mp1)) ->
- let substobjs = get_modtype_substobjs env mp_from inline mty in
+ get_modtype_substobjs env inline mty
+ | MSEwith (mty, With_Module (idl,mp1)) ->
+ let substobjs = get_modtype_substobjs env inline mty in
let modobjs = MPmap.find mp1 !modtab_substobjs in
- replace_module_object idl substobjs modobjs mp1
+ replace_module_object idl substobjs modobjs mp1
| MSEapply (fexpr, MSEident mp) as me ->
let (mbids, mp1, objs),mtb_mp1,mp_l =
get_objs_modtype_application env me in
@@ -478,20 +478,17 @@ let rec get_modtype_substobjs env mp_from inline = function
| MSEapply (_,mexpr) ->
Modops.error_application_to_not_path mexpr
-(* push names of bound modules (and their components) to Nametab *)
-(* add objects associated to them *)
-let process_module_bindings argids args =
- let process_arg id (mbid,(mty,ann)) =
- let dir = DirPath.make [id] in
- let mp = MPbound mbid in
- let (mbids,mp_from,objs) =
- get_modtype_substobjs (Global.env()) mp (inline_annot ann) mty
- in
- let subst = map_mp mp_from mp empty_delta_resolver in
- let substobjs = (mbids,mp,subst_objects subst objs) in
- do_module false "start" load_objects 1 dir mp substobjs []
+(* push names of a bound module (and its component) to Nametab *)
+(* add objects associated to it *)
+let process_module_binding mbid mty =
+ let dir = DirPath.make [MBId.to_id mbid] in
+ let mp = MPbound mbid in
+ let (mbids,mp_from,objs) =
+ get_modtype_substobjs (Global.env()) (default_inline ()) mty
in
- List.iter2 process_arg argids args
+ let subst = map_mp mp_from mp empty_delta_resolver in
+ let substobjs = (mbids,mp,subst_objects subst objs) in
+ do_module false "start" load_objects 1 dir mp substobjs []
(* Same with module_type_body *)
@@ -506,29 +503,25 @@ let rec seb2mse = function
| _ -> failwith "seb2mse: received a non-atomic seb"
let process_module_seb_binding mbid seb =
- process_module_bindings [MBId.to_id mbid]
- [mbid,
- (seb2mse seb,
- { ann_inline = DefaultInline; ann_scope_subst = [] })]
+ process_module_binding mbid (seb2mse seb)
let intern_args interp_modtype (idl,(arg,ann)) =
let inl = inline_annot ann in
let lib_dir = Lib.library_dp() in
- let mbids = List.map (fun (_,id) -> MBId.make lib_dir id) idl in
- let mty = interp_modtype (Global.env()) arg in
- let dirs = List.map (fun (_,id) -> DirPath.make [id]) idl in
- let (mbi,mp_from,objs) =
- get_modtype_substobjs (Global.env()) (MPbound (List.hd mbids)) inl mty
- in
- List.map2
- (fun dir mbid ->
- let resolver = Global.add_module_parameter mbid mty inl in
- let mp = MPbound mbid in
- let subst = map_mp mp_from mp resolver in
- let substobjs = (mbi,mp,subst_objects subst objs) in
- do_module false "interp" load_objects 1 dir mp substobjs [];
- (mbid,(mty,inl)))
- dirs mbids
+ let env = Global.env() in
+ let mty = interp_modtype env arg in
+ let (mbi,mp_from,objs) = get_modtype_substobjs env inl mty in
+ List.map
+ (fun (_,id) ->
+ let dir = DirPath.make [id] in
+ let mbid = MBId.make lib_dir id in
+ let mp = MPbound mbid in
+ let resolver = Global.add_module_parameter mbid mty inl in
+ let subst = map_mp mp_from mp resolver in
+ let substobjs = (mbi,mp,subst_objects subst objs) in
+ do_module false "interp" load_objects 1 dir mp substobjs [];
+ (mbid,(mty,inl)))
+ idl
let start_module_ interp_modtype export id args res fs =
let mp = Global.start_module id in
@@ -562,17 +555,17 @@ let end_module () =
None,( mbids, mp, substitute), keep, special
| Some (MSEident ln as mty, inline) ->
let (mbids1,mp1,objs) =
- get_modtype_substobjs (Global.env()) mp inline mty in
+ get_modtype_substobjs (Global.env()) inline mty in
Some mp1,(mbids@mbids1,mp1,objs), [], []
| Some (MSEwith _ as mty, inline) ->
let (mbids1,mp1,objs) =
- get_modtype_substobjs (Global.env()) mp inline mty in
+ get_modtype_substobjs (Global.env()) inline mty in
Some mp1,(mbids@mbids1,mp1,objs), [], []
| Some (MSEfunctor _, _) ->
anomaly (Pp.str "Funsig cannot be here...")
| Some (MSEapply _ as mty, inline) ->
let (mbids1,mp1,objs) =
- get_modtype_substobjs (Global.env()) mp inline mty in
+ get_modtype_substobjs (Global.env()) inline mty in
Some mp1,(mbids@mbids1,mp1,objs), [], []
with
Not_found -> anomaly (Pp.str "Module objects not found...")
@@ -742,7 +735,7 @@ let declare_modtype_ interp_modtype id args mtys (mty,ann) fs =
let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in
(* NB: check of subtyping will be done in cache_modtype *)
let sub_mty_l = build_subtypes interp_modtype mmp arg_entries mtys in
- let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp inl entry in
+ let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) inl entry in
(* Undo the simulated interactive building of the module type *)
(* and declare the module type as a whole *)
@@ -767,11 +760,11 @@ let rec get_objs_module_application env = function
| _ -> error "Application of a non-functor."
-let rec get_module_substobjs env mp_from inl = function
+let rec get_module_substobjs env inl = function
| MSEident mp -> MPmap.find mp !modtab_substobjs
| MSEfunctor (mbid,mty,mexpr) ->
- let (mbids, mp, objs) = get_module_substobjs env mp_from inl mexpr in
- (mbid::mbids, mp, objs)
+ let (mbids, mp, objs) = get_module_substobjs env inl mexpr in
+ (mbid::mbids, mp, objs)
| MSEapply (fexpr, MSEident mp) as me ->
let (mbids, mp1, objs),mb_mp1,mp_l =
get_objs_module_application env me
@@ -780,7 +773,7 @@ let rec get_module_substobjs env mp_from inl = function
compute_subst env mbids mb_mp1.mod_type (List.rev mp_l) inl in
(mbids_left, mp1,subst_objects subst objs)
| MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr
- | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from inl mty
+ | MSEwith (mty, With_Definition _) -> get_module_substobjs env inl mty
| MSEwith (mty, With_Module (idl,mp)) -> assert false
@@ -812,8 +805,8 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
let substobjs =
match entry with
- | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte
- | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
+ | {mod_entry_type = Some mte} -> get_modtype_substobjs env inl_res mte
+ | {mod_entry_expr = Some mexpr} -> get_module_substobjs env inl_expr mexpr
| _ -> anomaly ~label:"declare_module" (Pp.str "No type, no body ...")
in
let (mbids,mp_from,objs) = substobjs in
@@ -876,21 +869,20 @@ let (in_include : include_obj -> obj),
subst_function = subst_include;
classify_function = classify_include }
-let rec include_subst env mb mbids sign inline =
+let rec include_subst env mp reso mbids sign inline =
match mbids with
| [] -> empty_subst
| mbid::mbids ->
let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
- let subst = include_subst env mb mbids fbody_b inline in
+ let subst = include_subst env mp reso mbids fbody_b inline in
let mp_delta =
- Modops.inline_delta_resolver env inline mb.mod_mp
- farg_id farg_b mb.mod_delta
+ Modops.inline_delta_resolver env inline mp farg_id farg_b reso
in
- join (map_mbid mbid mb.mod_mp mp_delta) subst
+ join (map_mbid mbid mp mp_delta) subst
exception NothingToDo
-let get_includeself_substobjs env objs me is_mod inline =
+let get_includeself_substobjs env mp1 mbids objs me is_mod inline =
try
let mb_mp = match me with
| MSEident mp ->
@@ -914,10 +906,9 @@ let get_includeself_substobjs env objs me is_mod inline =
mb_mp mp_l
| _ -> raise NothingToDo
in
- let (mbids,mp_self,objects) = objs in
- let mb = Global.pack_module() in
- let subst = include_subst env mb mbids mb_mp.mod_type inline in
- ([],mp_self,subst_objects subst objects)
+ let reso = fst (Safe_typing.delta_of_senv (Global.safe_env ())) in
+ let subst = include_subst env mp1 reso mbids mb_mp.mod_type inline in
+ subst_objects subst objs
with NothingToDo -> objs
@@ -925,22 +916,21 @@ let get_includeself_substobjs env objs me is_mod inline =
let declare_one_include_inner annot (me,is_mod) =
let env = Global.env() in
- let mp1,_ = current_prefix () in
+ let cur_mp = fst (current_prefix ()) in
let inl = inline_annot annot in
let (mbids,mp,objs)=
if is_mod then
- get_module_substobjs env mp1 inl me
- else
- get_modtype_substobjs env mp1 inl me in
- let (mbids,mp,objs) =
- if not (List.is_empty mbids) then
- get_includeself_substobjs env (mbids,mp,objs) me is_mod inl
+ get_module_substobjs env inl me
else
- (mbids,mp,objs) in
+ get_modtype_substobjs env inl me in
+ let objs =
+ if List.is_empty mbids then objs
+ else get_includeself_substobjs env cur_mp mbids objs me is_mod inl
+ in
let id = current_mod_id() in
- let resolver = Global.add_include me is_mod inl in
+ let resolver = Global.add_include me is_mod inl in
register_scope_subst annot.ann_scope_subst;
- let subst = map_mp mp mp1 resolver in
+ let subst = map_mp mp cur_mp resolver in
let substobjs = subst_objects subst objs in
reset_scope_subst ();
ignore (add_leaf id (in_include substobjs))
diff --git a/library/declaremods.mli b/library/declaremods.mli
index e350c9fb1..c5a43dfbf 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -126,12 +126,6 @@ val iter_all_segments : (object_name -> obj -> unit) -> unit
val debug_print_modtab : unit -> Pp.std_ppcmds
-(*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*)
-
-(** For translator *)
-val process_module_bindings : module_ident list ->
- (MBId.t * (module_struct_entry annotated)) list -> unit
-
(** For Printer *)
val process_module_seb_binding :
MBId.t -> Declarations.struct_expr_body -> unit
diff --git a/library/global.ml b/library/global.ml
index 3b911e229..929f7418f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -104,10 +104,6 @@ let end_modtype fs id =
global_env := newenv;
kn
-let pack_module () =
- pack_module !global_env
-
-
let lookup_named id = lookup_named id (env())
let lookup_constant kn = lookup_constant kn (env())
diff --git a/library/global.mli b/library/global.mli
index f8edf3165..b1184da11 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -75,7 +75,6 @@ val add_module_parameter :
val start_modtype : Id.t -> module_path
val end_modtype : Summary.frozen -> Id.t -> module_path
-val pack_module : unit -> module_body
(** Queries *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 03:34:08 +0000