aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declaremods.ml411
-rw-r--r--library/declaremods.mli15
-rw-r--r--library/global.ml2
-rw-r--r--library/global.mli11
-rw-r--r--library/lib.ml22
-rw-r--r--library/lib.mli3
-rw-r--r--library/nametab.ml16
-rwxr-xr-xlibrary/nametab.mli6
8 files changed, 382 insertions, 104 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 29e8012fe..8cfd7e1ae 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -78,8 +78,8 @@ let modtab_objects =
(* currently started interactive module (if any) - its arguments (if it
is a functor) and declared output type *)
let openmod_info =
- ref (([],None,None) : mod_bound_id list * module_type_entry option
- * module_type_body option)
+ ref (([],None,None) : mod_bound_id list * module_struct_entry option
+ * struct_expr_body option)
let _ = Summary.declare_summary "MODULE-INFO"
{ Summary.freeze_function = (fun () ->
@@ -122,23 +122,19 @@ let msid_of_prefix (_,(mp,sec)) =
anomaly ("Non-empty section in module name!" ^
string_of_mp mp ^ "." ^ string_of_dirpath sec)
-(* Check that a module type is not functorial *)
-
-let rec check_sig env = function
- | MTBident kn -> check_sig env (Environ.lookup_modtype kn env)
- | MTBsig _ -> ()
- | MTBfunsig _ -> Modops.error_result_must_be_signature ()
-
-let rec check_sig_entry env = function
- | MTEident kn -> check_sig env (Environ.lookup_modtype kn env)
- | MTEfunsig _ -> Modops.error_result_must_be_signature ()
- | MTEwith (mte,_) -> check_sig_entry env mte
+let rec scrape_alias mp =
+ match (Environ.lookup_module mp
+ (Global.env())) with
+ | {mod_expr = Some (SEBident mp1);
+ mod_type = None} -> scrape_alias mp1
+ | _ -> mp
+
(* This function checks if the type calculated for the module [mp] is
a subtype of [sub_mtb]. Uses only the global environment. *)
let check_subtypes mp sub_mtb =
let env = Global.env () in
- let mtb = (Environ.lookup_module mp env).mod_type in
+ let mtb = Modops.eval_struct env (SEBident mp) in
let _ = Environ.add_constraints
(Subtyping.check_subtypes env mtb sub_mtb)
in
@@ -176,6 +172,35 @@ let do_module exists what iter_objects i dir mp substobjs objects =
| None -> ()
+
+let do_module_alias exists what iter_objects i dir mp alias substobjs objects =
+ let prefix = (dir,(alias,empty_dirpath)) in
+ let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
+ let vis =
+ if exists then
+ if
+ try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo
+ with Not_found -> false
+ then
+ Nametab.Exactly i
+ else
+ errorlabstrm (what^"_module")
+ (pr_dirpath dir ++ str " should already exist!")
+ else
+ if Nametab.exists_dir dir then
+ errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
+ else
+ Nametab.Until i
+ in
+ Nametab.push_dir vis dir dirinfo;
+ modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
+ match objects with
+ Some seg ->
+ modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects;
+ iter_objects (i+1) prefix seg
+ | None -> ()
+
+
let conv_names_do_module exists what iter_objects i
(sp,kn) substobjs substituted =
let dir,mp = dir_of_sp sp, mp_of_kn kn in
@@ -193,7 +218,8 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) =
| Some (me,sub_mte_o) ->
let sub_mtb_o = match sub_mte_o with
None -> None
- | Some mte -> Some (Mod_typing.translate_modtype (Global.env()) mte)
+ | Some mte -> Some (Mod_typing.translate_struct_entry
+ (Global.env()) mte)
in
let mp = Global.add_module (basename sp) me in
@@ -203,12 +229,40 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) =
match sub_mtb_o with
None -> ()
| Some sub_mtb ->
-check_subtypes mp sub_mtb
+ check_subtypes mp sub_mtb
in
conv_names_do_module false "cache" load_objects 1 oname substobjs substituted
+let cache_module_alias ((sp,kn),(entry,substobjs,substituted)) =
+ let dir,mp,alias = match entry with
+ | None ->
+ anomaly "You must not recache interactive modules!"
+ | Some (me,sub_mte_o) ->
+ let sub_mtb_o = match sub_mte_o with
+ None -> None
+ | Some mte -> Some (Mod_typing.translate_struct_entry
+ (Global.env()) mte)
+ in
+
+ let mp' = Global.add_module (basename sp) me in
+ if mp' <> mp_of_kn kn then
+ anomaly "Kernel and Library names do not match";
+
+ let _ = match sub_mtb_o with
+ None -> ()
+ | Some sub_mtb ->
+ check_subtypes mp' sub_mtb in
+ match me with
+ | {mod_entry_type = None;
+ mod_entry_expr = Some (MSEident mp)} ->
+ dir_of_sp sp,mp_of_kn kn,scrape_alias mp
+ | _ -> anomaly "cache module alias"
+ in
+ do_module_alias false "cache" load_objects 1 dir mp alias substobjs substituted
+
+
(* TODO: This check is not essential *)
let check_empty s = function
| None -> ()
@@ -224,12 +278,40 @@ let load_module i (oname,(entry,substobjs,substituted)) =
check_empty "load_module" entry;
conv_names_do_module false "load" load_objects i oname substobjs substituted
+let load_module_alias i ((sp,kn),(entry,substobjs,substituted)) =
+ let dir,mp,alias=
+ match entry with
+ | Some (me,_)->
+ begin
+ match me with
+ |{mod_entry_type = None;
+ mod_entry_expr = Some (MSEident mp)} ->
+ dir_of_sp sp,mp_of_kn kn,scrape_alias mp
+ | _ -> anomaly "tata"
+ end
+ | None -> anomaly "toujours"
+ in
+ do_module_alias false "load" load_objects i dir mp alias substobjs substituted
let open_module i (oname,(entry,substobjs,substituted)) =
(* TODO: This check is not essential *)
check_empty "open_module" entry;
conv_names_do_module true "open" open_objects i oname substobjs substituted
+let open_module_alias i ((sp,kn),(entry,substobjs,substituted)) =
+ let dir,mp,alias=
+ match entry with
+ | Some (me,_)->
+ begin
+ match me with
+ |{mod_entry_type = None;
+ mod_entry_expr = Some (MSEident mp)} ->
+ dir_of_sp sp,mp_of_kn kn,scrape_alias mp
+ | _ -> anomaly "tata"
+ end
+ | None -> anomaly "toujours"
+ in
+ do_module_alias true "open" open_objects i dir mp alias substobjs substituted
let subst_substobjs dir mp (subst,mbids,msid,objs) =
match mbids with
@@ -252,10 +334,36 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
in
(None,substobjs,substituted)
+let subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
+ let dir,mp = dir_of_sp sp, mp_of_kn kn in
+ let (sub,mbids,msid,objs) = substobjs in
+ let subst' = join sub subst in
+ (* substitutive_objects get the new substitution *)
+ let substobjs = (subst',mbids,msid,objs) in
+ (* if we are not a functor - calculate substitued.
+ We add "msid |-> mp" to the substitution *)
+ let substituted = subst_substobjs dir mp substobjs in
+ match entry with
+ | Some (me,sub)->
+ begin
+ match me with
+ |{mod_entry_type = None;
+ mod_entry_expr = Some (MSEident mp)} ->
+ (Some ({mod_entry_type = None;
+ mod_entry_expr =
+ Some (MSEident (subst_mp subst' mp))},sub),
+ substobjs,substituted)
+
+ | _ -> anomaly "tata"
+ end
+ | None -> anomaly "toujours"
let classify_module (_,(_,substobjs,_)) =
Substitute (None,substobjs,None)
+let classify_module_alias (_,(entry,substobjs,_)) =
+ Substitute (entry,substobjs,None)
+
let (in_module,out_module) =
declare_object {(default_object "MODULE") with
cache_function = cache_module;
@@ -265,6 +373,14 @@ let (in_module,out_module) =
classify_function = classify_module;
export_function = (fun _ -> anomaly "No modules in sections!") }
+let (in_module_alias,out_module_alias) =
+ declare_object {(default_object "MODULE ALIAS") with
+ cache_function = cache_module_alias;
+ load_function = load_module_alias;
+ open_function = open_module_alias;
+ subst_function = subst_module_alias;
+ classify_function = classify_module_alias;
+ export_function = (fun _ -> anomaly "No modules in sections!") }
let cache_keep _ = anomaly "This module should not be cached!"
@@ -298,7 +414,7 @@ let (in_modkeep,out_modkeep) =
The module M gets its objects from SIG
*)
let modtypetab =
- ref (KNmap.empty : substitutive_objects KNmap.t)
+ ref (MPmap.empty : substitutive_objects MPmap.t)
(* currently started interactive module type. We remember its arguments
if it is a functor type *)
@@ -312,22 +428,20 @@ let _ = Summary.declare_summary "MODTYPE-INFO"
modtypetab := fst ft;
openmodtype_info := snd ft);
Summary.init_function = (fun () ->
- modtypetab := KNmap.empty;
+ modtypetab := MPmap.empty;
openmodtype_info := []);
Summary.survive_module = false;
Summary.survive_section = true }
-
-
let cache_modtype ((sp,kn),(entry,modtypeobjs)) =
let _ =
match entry with
| None ->
anomaly "You must not recache interactive module types!"
| Some mte ->
- let kn' = Global.add_modtype (basename sp) mte in
- if kn' <> kn then
+ let mp = Global.add_modtype (basename sp) mte in
+ if mp <>mp_of_kn kn then
anomaly "Kernel and Library names do not match"
in
@@ -335,9 +449,9 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs)) =
errorlabstrm "cache_modtype"
(pr_sp sp ++ str " already exists") ;
- Nametab.push_modtype (Nametab.Until 1) sp kn;
+ Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn);
- modtypetab := KNmap.add kn modtypeobjs !modtypetab
+ modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab
let load_modtype i ((sp,kn),(entry,modtypeobjs)) =
@@ -347,23 +461,22 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) =
errorlabstrm "cache_modtype"
(pr_sp sp ++ str " already exists") ;
- Nametab.push_modtype (Nametab.Until i) sp kn;
+ Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn);
- modtypetab := KNmap.add kn modtypeobjs !modtypetab
+ modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab
let open_modtype i ((sp,kn),(entry,_)) =
check_empty "open_modtype" entry;
if
- try Nametab.locate_modtype (qualid_of_sp sp) <> kn
+ try Nametab.locate_modtype (qualid_of_sp sp) <> (mp_of_kn kn)
with Not_found -> true
then
errorlabstrm ("open_modtype")
(pr_sp sp ++ str " should already exist!");
- Nametab.push_modtype (Nametab.Exactly i) sp kn
-
+ Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) =
check_empty "subst_modtype" entry;
@@ -385,7 +498,7 @@ let (in_modtype,out_modtype) =
-let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs =
+let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp =
if mbids<>[] then
error "Unexpected functor objects"
else
@@ -394,10 +507,13 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs =
| id::idl,(id',obj)::tail when id = id' ->
if object_tag obj = "MODULE" then
(match idl with
- [] -> (id, in_module (None,modobjs,None))::tail
+ [] -> (id, in_module_alias (Some
+ ({mod_entry_type = None;
+ mod_entry_expr = Some (MSEident mp)},None)
+ ,modobjs,None))::tail
| _ ->
let (_,substobjs,_) = out_module obj in
- let substobjs' = replace_module_object idl substobjs modobjs in
+ let substobjs' = replace_module_object idl substobjs modobjs mp in
(id, in_module (None,substobjs',None))::tail
)
else error "MODULE expected!"
@@ -408,17 +524,34 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs =
let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) =
(subst, mbids1@mbids2, msid, lib_stack)
-
-let rec get_modtype_substobjs = function
- MTEident ln -> KNmap.find ln !modtypetab
- | MTEfunsig (mbid,_,mte) ->
- let (subst, mbids, msid, objs) = get_modtype_substobjs mte in
+let rec get_modtype_substobjs env = function
+ MSEident ln -> MPmap.find ln !modtypetab
+ | MSEfunctor (mbid,_,mte) ->
+ let (subst, mbids, msid, objs) = get_modtype_substobjs env mte in
(subst, mbid::mbids, msid, objs)
- | MTEwith (mty, With_Definition _) -> get_modtype_substobjs mty
- | MTEwith (mty, With_Module (idl,mp)) ->
- let substobjs = get_modtype_substobjs mty in
+ | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty
+ | MSEwith (mty, With_Module (idl,mp)) ->
+ let substobjs = get_modtype_substobjs env mty in
let modobjs = MPmap.find mp !modtab_substobjs in
- replace_module_object idl substobjs modobjs
+ replace_module_object idl substobjs modobjs mp
+ | MSEapply (mexpr, MSEident mp) ->
+ let ftb = Mod_typing.translate_struct_entry env mexpr in
+ let farg_id, farg_b, fbody_b = Modops.destr_functor env
+ (Modops.eval_struct env ftb) in
+ let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
+ (match mbids with
+ | mbid::mbids ->
+ let resolve =
+ Modops.resolver_of_environment farg_id farg_b mp env in
+ (* application outside the kernel, only for substitutive
+ objects (that are all non-logical objects) *)
+ (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs)
+ | [] -> match mexpr with
+ | MSEident _ -> error "Application of a non-functor"
+ | _ -> error "Application of a functor with too few arguments")
+ | MSEapply (_,mexpr) ->
+ Modops.error_application_to_not_path mexpr
+
(* push names of bound modules (and their components) to Nametab *)
(* add objects associated to them *)
@@ -426,13 +559,14 @@ let process_module_bindings argids args =
let process_arg id (mbid,mty) =
let dir = make_dirpath [id] in
let mp = MPbound mbid in
- let substobjs = get_modtype_substobjs mty in
+ let substobjs = get_modtype_substobjs (Global.env()) mty in
let substituted = subst_substobjs dir mp substobjs in
do_module false "start" load_objects 1 dir mp substobjs substituted
in
List.iter2 process_arg argids args
-
+(* Dead code *)
+(*
let replace_module mtb id mb = todo "replace module after with"; mtb
let rec get_some_body mty env = match mty with
@@ -441,14 +575,15 @@ let rec get_some_body mty env = match mty with
| MTEwith (mty,With_Definition _) -> get_some_body mty env
| MTEwith (mty,With_Module (id,mp)) ->
replace_module (get_some_body mty env) id (Environ.lookup_module mp env)
-
+*)
+(* Dead code *)
let intern_args interp_modtype (idl,arg) =
let lib_dir = Lib.library_dp() in
let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
let mty = interp_modtype (Global.env()) arg in
let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
- let substobjs = get_modtype_substobjs mty in
+ let substobjs = get_modtype_substobjs (Global.env()) mty in
List.map2
(fun dir mbid ->
Global.add_module_parameter mbid mty;
@@ -457,7 +592,6 @@ let intern_args interp_modtype (idl,arg) =
do_module false "interp" load_objects 1 dir mp substobjs substituted;
(mbid,mty))
dirs mbids
-
let start_module interp_modtype export id args res_o =
let fs = Summary.freeze_summaries () in
@@ -469,23 +603,22 @@ let start_module interp_modtype export id args res_o =
| Some (res, restricted) ->
(* we translate the module here to catch errors as early as possible *)
let mte = interp_modtype (Global.env()) res in
- check_sig_entry (Global.env()) mte;
if restricted then
Some mte, None
else
- let mtb = Mod_typing.translate_modtype (Global.env()) mte in
+ let mtb = Mod_typing.translate_struct_entry (Global.env()) mte in
let sub_mtb =
List.fold_right
(fun (arg_id,arg_t) mte ->
- let arg_t = Mod_typing.translate_modtype (Global.env()) arg_t
- in MTBfunsig(arg_id,arg_t,mte))
+ let arg_t = Mod_typing.translate_struct_entry (Global.env()) arg_t
+ in SEBfunctor(arg_id,arg_t,mte))
arg_entries mtb
in
None, Some sub_mtb
in
let mbids = List.map fst arg_entries in
- openmod_info:=(mbids,res_entry_o,sub_body_o);
+ openmod_info:=(mbids,res_entry_o,sub_body_o);
let prefix = Lib.start_module export id mp fs in
Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
Lib.add_frozen_state ()
@@ -511,12 +644,14 @@ let end_module id =
match res_o with
| None ->
(empty_subst, mbids, msid, substitute), keep, special
- | Some (MTEident ln) ->
- abstract_substobjs mbids (KNmap.find ln (!modtypetab)), [], []
- | Some (MTEwith _ as mty) ->
- abstract_substobjs mbids (get_modtype_substobjs mty), [], []
- | Some (MTEfunsig _) ->
+ | Some (MSEident ln) ->
+ abstract_substobjs mbids (MPmap.find ln (!modtypetab)), [], []
+ | Some (MSEwith _ as mty) ->
+ abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
+ | Some (MSEfunctor _) ->
anomaly "Funsig cannot be here..."
+ | Some (MSEapply _ as mty) ->
+ abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
with
Not_found -> anomaly "Module objects not found..."
in
@@ -636,7 +771,6 @@ let import_module export mp =
(************************************************************************)
(* module types *)
-
let start_modtype interp_modtype id args =
let fs = Summary.freeze_summaries () in
@@ -667,7 +801,7 @@ let end_modtype id =
if fst oname <> fst oldoname then
anomaly
"Section paths generated on start_ and end_modtype do not match";
- if snd oname <> ln then
+ if (mp_of_kn (snd oname)) <> ln then
anomaly
"Kernel and Library names do not match";
@@ -684,11 +818,11 @@ let declare_modtype interp_modtype id args mty =
let base_mty = interp_modtype (Global.env()) mty in
let entry =
List.fold_right
- (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+ (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
arg_entries
base_mty
in
- let substobjs = get_modtype_substobjs entry in
+ let substobjs = get_modtype_substobjs (Global.env()) entry in
(* Undo the simulated interactive building of the module type *)
(* and declare the module type as a whole *)
Summary.unfreeze_summaries fs;
@@ -700,14 +834,14 @@ let declare_modtype interp_modtype id args mty =
let rec get_module_substobjs env = function
- | MEident mp -> MPmap.find mp !modtab_substobjs
- | MEfunctor (mbid,mty,mexpr) ->
+ | MSEident mp -> MPmap.find mp !modtab_substobjs
+ | MSEfunctor (mbid,mty,mexpr) ->
let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
(subst, mbid::mbids, msid, objs)
- | MEapply (mexpr, MEident mp) ->
- let feb,ftb = Mod_typing.translate_mexpr env mexpr in
- let ftb = Modops.scrape_modtype env ftb in
- let farg_id, farg_b, fbody_b = Modops.destr_functor ftb in
+ | MSEapply (mexpr, MSEident mp) ->
+ let ftb = Mod_typing.translate_struct_entry env mexpr in
+ let farg_id, farg_b, fbody_b = Modops.destr_functor env
+ (Modops.eval_struct env ftb) in
let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
(match mbids with
| mbid::mbids ->
@@ -717,11 +851,15 @@ let rec get_module_substobjs env = function
objects (that are all non-logical objects) *)
(add_mbid mbid mp (Some resolve) subst, mbids, msid, objs)
| [] -> match mexpr with
- | MEident _ -> error "Application of a non-functor"
+ | MSEident _ -> error "Application of a non-functor"
| _ -> error "Application of a functor with too few arguments")
- | MEapply (_,mexpr) ->
+ | MSEapply (_,mexpr) ->
Modops.error_application_to_not_path mexpr
-
+ | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty
+ | MSEwith (mty, With_Module (idl,mp)) ->
+ let substobjs = get_module_substobjs env mty in
+ let modobjs = MPmap.find mp !modtab_substobjs in
+ replace_module_object idl substobjs modobjs mp
let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
@@ -735,14 +873,14 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
None -> None, None
| (Some (mty, true)) ->
Some (List.fold_right
- (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+ (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
arg_entries
(interp_modtype (Global.env()) mty)),
None
| (Some (mty, false)) ->
None,
Some (List.fold_right
- (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+ (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
arg_entries
(interp_modtype (Global.env()) mty))
in
@@ -750,7 +888,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
None -> None
| Some mexpr ->
Some (List.fold_right
- (fun (mbid,mte) me -> MEfunctor(mbid,mte,me))
+ (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me))
arg_entries
(interp_modexpr (Global.env()) mexpr))
in
@@ -761,29 +899,136 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
let env = Global.env() in
let substobjs =
match entry with
- | {mod_entry_type = Some mte} -> get_modtype_substobjs mte
+ | {mod_entry_type = Some mte} -> get_modtype_substobjs env mte
| {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr
| _ -> anomaly "declare_module: No type, no body ..."
in
-
(* Undo the simulated interactive building of the module *)
(* and declare the module as a whole *)
Summary.unfreeze_summaries fs;
-
- let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
- let substituted = subst_substobjs dir mp substobjs in
-
- ignore (add_leaf
- id
- (in_module (Some (entry, mty_sub_o), substobjs, substituted)))
-
+ match entry with
+ |{mod_entry_type = None;
+ mod_entry_expr = Some (MSEident mp) } ->
+ let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+ let substituted = subst_substobjs dir mp substobjs in
+ ignore (add_leaf
+ id
+ (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted)))
+ | _ ->
+ let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+ let substituted = subst_substobjs dir mp substobjs in
+ ignore (add_leaf
+ id
+ (in_module (Some (entry, mty_sub_o), substobjs, substituted)))
+
with e ->
(* Something wrong: undo the whole process *)
Summary.unfreeze_summaries fs; raise e
+(* Include *)
+
+let rec subst_inc_expr subst me =
+ match me with
+ | MSEident mp -> MSEident (subst_mp subst mp)
+ | MSEwith (me,With_Module(idl,mp)) ->
+ MSEwith (subst_inc_expr subst me,
+ With_Module(idl,subst_mp subst mp))
+ | MSEwith (me,With_Definition(idl,const))->
+ let const1 = Mod_subst.from_val const in
+ let force = Mod_subst.force subst_mps in
+ MSEwith (subst_inc_expr subst me,
+ With_Definition(idl,force (subst_substituted
+ subst const1)))
+ | MSEapply (me1,me2) ->
+ MSEapply (subst_inc_expr subst me1,
+ subst_inc_expr subst me2)
+ | _ -> anomaly "You cannot Include a high-order structure"
+
+let lift_oname (sp,kn) =
+ let mp,_,_ = Names.repr_kn kn in
+ let dir,_ = Libnames.repr_path sp in
+ (dir,mp)
+
+let cache_include (oname,((me,is_mod),substobjs,substituted)) =
+ let dir,mp1 = lift_oname oname in
+ let prefix = (dir,(mp1,empty_dirpath)) in
+ Global.add_include me;
+ match substituted with
+ Some seg ->
+ load_objects 1 prefix seg;
+ open_objects 1 prefix seg;
+ | None -> ()
+
+let load_include i (oname,((me,is_mod),substobjs,substituted)) =
+ let dir,mp1 = lift_oname oname in
+ let prefix = (dir,(mp1,empty_dirpath)) in
+ match substituted with
+ Some seg ->
+ if is_mod then
+ load_objects i prefix seg
+ else
+ if i = 1 then
+ load_objects i prefix seg
+ | None -> ()
-(*s Iterators. *)
+let open_include i (oname,((me,is_mod),substobjs,substituted)) =
+ let dir,mp1 = lift_oname oname in
+ let prefix = (dir,(mp1,empty_dirpath)) in
+ match substituted with
+ Some seg ->
+ if is_mod then
+ open_objects i prefix seg
+ else
+ if i = 1 then
+ open_objects i prefix seg
+ | None -> ()
+let subst_include (oname,subst,((me,is_mod),substobj,_)) =
+ let dir,mp1 = lift_oname oname in
+ let (sub,mbids,msid,objs) = substobj in
+ let subst' = join sub subst in
+ let substobjs = (subst',mbids,msid,objs) in
+ let substituted = subst_substobjs dir mp1 substobjs in
+ ((subst_inc_expr subst' me,is_mod),substobjs,substituted)
+
+let classify_include (_,((me,is_mod),substobjs,_)) =
+ Substitute ((me,is_mod),substobjs,None)
+
+let (in_include,out_include) =
+ declare_object {(default_object "INCLUDE") with
+ cache_function = cache_include;
+ load_function = load_include;
+ open_function = open_include;
+ subst_function = subst_include;
+ classify_function = classify_include;
+ export_function = (fun _ -> anomaly "No modules in section!") }
+
+let declare_include interp_struct me_ast is_mod =
+
+ let fs = Summary.freeze_summaries () in
+
+ try
+ let env = Global.env() in
+ let me = interp_struct env me_ast in
+ let substobjs =
+ if is_mod then
+ get_module_substobjs env me
+ else
+ get_modtype_substobjs env me in
+ let mp1,_ = current_prefix () in
+ let dir = dir_of_sp (Lib.path_of_include()) in
+ let substituted = subst_substobjs dir mp1 substobjs in
+ let id = current_mod_id() in
+
+ ignore (add_leaf id
+ (in_include ((me,is_mod), substobjs, substituted)))
+ with e ->
+ (* Something wrong: undo the whole process *)
+ Summary.unfreeze_summaries fs; raise e
+
+
+(*s Iterators. *)
+
let iter_all_segments f =
let _ =
MPmap.iter
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 2a491b4a6..717fddf79 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -37,12 +37,12 @@ open Lib
*)
val declare_module :
- (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) ->
+ (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) ->
identifier ->
(identifier located list * 'modtype) list -> ('modtype * bool) option ->
'modexpr option -> unit
-val start_module : (env -> 'modtype -> module_type_entry) ->
+val start_module : (env -> 'modtype -> module_struct_entry) ->
bool option -> identifier -> (identifier located list * 'modtype) list ->
('modtype * bool) option -> unit
@@ -52,10 +52,10 @@ val end_module : identifier -> unit
(*s Module types *)
-val declare_modtype : (env -> 'modtype -> module_type_entry) ->
+val declare_modtype : (env -> 'modtype -> module_struct_entry) ->
identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit
-val start_modtype : (env -> 'modtype -> module_type_entry) ->
+val start_modtype : (env -> 'modtype -> module_struct_entry) ->
identifier -> (identifier located list * 'modtype) list -> unit
val end_modtype : identifier -> unit
@@ -95,6 +95,10 @@ val really_import_module : module_path -> unit
val import_module : bool -> module_path -> unit
+(* Include *)
+
+val declare_include : (env -> 'struct_expr -> module_struct_entry) ->
+ 'struct_expr -> bool -> unit
(*s [iter_all_segments] iterate over all segments, the modules'
segments first and then the current segment. Modules are presented
@@ -110,4 +114,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
(* For translator *)
val process_module_bindings : module_ident list ->
- (mod_bound_id * module_type_entry) list -> unit
+ (mod_bound_id * module_struct_entry) list -> unit
+
diff --git a/library/global.ml b/library/global.ml
index 0ee5533f3..4de4029b2 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -73,6 +73,8 @@ let add_constraints c = global_env := add_constraints c !global_env
let set_engagement c = global_env := set_engagement c !global_env
+let add_include me = global_env := add_include me !global_env
+
let start_module id =
let l = label_of_id id in
let mp,newenv = start_module l !global_env in
diff --git a/library/global.mli b/library/global.mli
index 8633dba76..71617f5a1 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -50,7 +50,7 @@ val add_mind :
dir_path -> identifier -> mutual_inductive_entry -> kernel_name
val add_module : identifier -> module_entry -> module_path
-val add_modtype : identifier -> module_type_entry -> kernel_name
+val add_modtype : identifier -> module_struct_entry -> module_path
val add_constraints : constraints -> unit
@@ -64,13 +64,14 @@ val set_engagement : engagement -> unit
of the started module / module type *)
val start_module : identifier -> module_path
-val end_module : identifier -> module_type_entry option -> module_path
+val end_module : identifier -> module_struct_entry option -> module_path
-val add_module_parameter : mod_bound_id -> module_type_entry -> unit
+val add_module_parameter : mod_bound_id -> module_struct_entry -> unit
val start_modtype : identifier -> module_path
-val end_modtype : identifier -> kernel_name
+val end_modtype : identifier -> module_path
+val add_include : module_struct_entry -> unit
(* Queries *)
val lookup_named : variable -> named_declaration
@@ -78,7 +79,7 @@ val lookup_constant : constant -> constant_body
val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
val lookup_mind : mutual_inductive -> mutual_inductive_body
val lookup_module : module_path -> module_body
-val lookup_modtype : kernel_name -> module_type_body
+val lookup_modtype : module_path -> module_type_body
(* Compiled modules *)
val start_library : dir_path -> module_path
diff --git a/library/lib.ml b/library/lib.ml
index 8fff32e1a..de2047dbd 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -98,11 +98,15 @@ let library_dp () =
module path and relative section path *)
let path_prefix = ref initial_prefix
-
let cwd () = fst !path_prefix
let make_path id = Libnames.make_path (cwd ()) id
+let path_of_include () =
+ let dir = Names.repr_dirpath (cwd ()) in
+ let new_dir = List.tl dir in
+ let id = List.hd dir in
+ Libnames.make_path (Names.make_dirpath new_dir) id
let current_prefix () = snd !path_prefix
@@ -236,12 +240,25 @@ let add_frozen_state () =
(* Modules. *)
+
let is_something_opened = function
(_,OpenedSection _) -> true
| (_,OpenedModule _) -> true
| (_,OpenedModtype _) -> true
| _ -> false
+
+let current_mod_id () =
+ try match find_entry_p is_something_opened with
+ | oname,OpenedModule (_,_,nametab) ->
+ basename (fst oname)
+ | oname,OpenedModtype (_,nametab) ->
+ basename (fst oname)
+ | _ -> error "you are not in a module"
+ with Not_found ->
+ error "no opened modules"
+
+
let start_module export id mp nametab =
let dir = extend_dirpath (fst !path_prefix) id in
let prefix = dir,(mp,empty_dirpath) in
@@ -586,7 +603,8 @@ let reset_name (loc,id) =
let is_mod_node = function
| OpenedModule _ | OpenedModtype _ | OpenedSection _
| ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true
- | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
+ | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
+ || t = "MODULE ALIAS"
| _ -> false
(* Reset on a module or section name in order to bypass constants with
diff --git a/library/lib.mli b/library/lib.mli
index f13ff82ae..570685585 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -88,6 +88,7 @@ val contents_after : object_name option -> library_segment
(* User-side names *)
val cwd : unit -> dir_path
val make_path : identifier -> section_path
+val path_of_include : unit -> section_path
(* Kernel-side names *)
val current_prefix : unit -> module_path * dir_path
@@ -101,7 +102,7 @@ val sections_depth : unit -> int
(* Are we inside an opened module type *)
val is_modtype : unit -> bool
val is_module : unit -> bool
-
+val current_mod_id : unit -> module_ident
(* Returns the most recent OpenedThing node *)
val what_is_opened : unit -> object_name * node
diff --git a/library/nametab.ml b/library/nametab.ml
index 9aab07cac..536c9605a 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -263,9 +263,11 @@ type ccitab = extended_global_reference SpTab.t
let the_ccitab = ref (SpTab.empty : ccitab)
type kntab = kernel_name SpTab.t
-let the_modtypetab = ref (SpTab.empty : kntab)
let the_tactictab = ref (SpTab.empty : kntab)
+type mptab = module_path SpTab.t
+let the_modtypetab = ref (SpTab.empty : mptab)
+
type objtab = unit SpTab.t
let the_objtab = ref (SpTab.empty : objtab)
@@ -299,8 +301,10 @@ let the_globrevtab = ref (Globrevtab.empty : globrevtab)
type mprevtab = dir_path MPmap.t
let the_modrevtab = ref (MPmap.empty : mprevtab)
+type mptrevtab = section_path MPmap.t
+let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
+
type knrevtab = section_path KNmap.t
-let the_modtyperevtab = ref (KNmap.empty : knrevtab)
let the_tacticrevtab = ref (KNmap.empty : knrevtab)
@@ -328,7 +332,7 @@ let push = push_cci
let push_modtype vis sp kn =
the_modtypetab := SpTab.push vis sp kn !the_modtypetab;
- the_modtyperevtab := KNmap.add kn sp !the_modtyperevtab
+ the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab
(* This is for tactic definition names *)
@@ -483,7 +487,7 @@ let shortest_qualid_of_module mp =
DirTab.shortest_qualid Idset.empty dir !the_dirtab
let shortest_qualid_of_modtype kn =
- let sp = KNmap.find kn !the_modtyperevtab in
+ let sp = MPmap.find kn !the_modtyperevtab in
SpTab.shortest_qualid Idset.empty sp !the_modtypetab
let shortest_qualid_of_tactic kn =
@@ -504,6 +508,7 @@ let inductive_of_reference r =
user_err_loc (loc_of_reference r,"global_inductive",
pr_reference r ++ spc () ++ str "is not an inductive type")
+
(********************************************************************)
(********************************************************************)
@@ -520,10 +525,11 @@ let init () =
the_tactictab := SpTab.empty;
the_globrevtab := Globrevtab.empty;
the_modrevtab := MPmap.empty;
- the_modtyperevtab := KNmap.empty;
+ the_modtyperevtab := MPmap.empty;
the_tacticrevtab := KNmap.empty
+
let freeze () =
!the_ccitab,
!the_dirtab,
diff --git a/library/nametab.mli b/library/nametab.mli
index 66de6a708..eab86db1d 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -73,7 +73,7 @@ type visibility = Until of int | Exactly of int
val push : visibility -> section_path -> global_reference -> unit
val push_syntactic_definition :
visibility -> section_path -> kernel_name -> unit
-val push_modtype : visibility -> section_path -> kernel_name -> unit
+val push_modtype : visibility -> section_path -> module_path -> unit
val push_dir : visibility -> dir_path -> global_dir_reference -> unit
val push_object : visibility -> section_path -> unit
val push_tactic : visibility -> section_path -> kernel_name -> unit
@@ -106,7 +106,7 @@ val locate_obj : qualid -> section_path
val locate_constant : qualid -> constant
val locate_mind : qualid -> mutual_inductive
val locate_section : qualid -> dir_path
-val locate_modtype : qualid -> kernel_name
+val locate_modtype : qualid -> module_path
val locate_syntactic_definition : qualid -> kernel_name
type ltac_constant = kernel_name
@@ -161,7 +161,7 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds
Coq.A.B.x that denotes the same object. *)
val shortest_qualid_of_module : module_path -> qualid
-val shortest_qualid_of_modtype : kernel_name -> qualid
+val shortest_qualid_of_modtype : module_path -> qualid
(*
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 00:16:08 +0000