summaryrefslogtreecommitdiff
path: root/library/declaremods.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/declaremods.ml')
-rw-r--r--library/declaremods.ml734
1 files changed, 565 insertions, 169 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml
index aac2b599..123417a6 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,8 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declaremods.ml 8752 2006-04-27 19:37:33Z herbelin $ i*)
-
+(*i $Id: declaremods.ml 11142 2008-06-18 15:37:31Z soubiran $ i*)
open Pp
open Util
open Names
@@ -78,22 +77,29 @@ 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)
+
+(* The library_cache here is needed to avoid recalculations of
+ substituted modules object during "reloading" of libraries *)
+let library_cache = ref Dirmap.empty
let _ = Summary.declare_summary "MODULE-INFO"
{ Summary.freeze_function = (fun () ->
!modtab_substobjs,
!modtab_objects,
- !openmod_info);
- Summary.unfreeze_function = (fun (sobjs,objs,info) ->
+ !openmod_info,
+ !library_cache);
+ Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) ->
modtab_substobjs := sobjs;
modtab_objects := objs;
- openmod_info := info);
+ openmod_info := info;
+ library_cache := libcache);
Summary.init_function = (fun () ->
modtab_substobjs := MPmap.empty;
modtab_objects := MPmap.empty;
- openmod_info := ([],None,None));
+ openmod_info := ([],None,None);
+ library_cache := Dirmap.empty);
Summary.survive_module = false;
Summary.survive_section = false }
@@ -107,6 +113,11 @@ let mp_of_kn kn =
else
anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
+let is_bound mp =
+ match mp with
+ | MPbound _ -> true
+ | _ -> false
+
let dir_of_sp sp =
let dir,id = repr_path sp in
extend_dirpath dir id
@@ -122,29 +133,32 @@ 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)
- | MTEsig _ -> ()
- | MTEfunsig _ -> Modops.error_result_must_be_signature ()
- | MTEwith (mte,_) -> check_sig_entry env mte
+let scrape_alias mp =
+ Environ.scrape_alias mp (Global.env())
+
(* 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 = Environ.lookup_modtype mp env in
+ let sub_mtb =
+ {typ_expr = sub_mtb;
+ typ_strength = None;
+ typ_alias = empty_subst} in
let _ = Environ.add_constraints
(Subtyping.check_subtypes env mtb sub_mtb)
in
() (* The constraints are checked and forgot immediately! *)
+let subst_substobjs dir mp (subst,mbids,msid,objs) =
+ match mbids with
+ | [] ->
+ let prefix = dir,(mp,empty_dirpath) in
+ let subst' = join_alias (map_msid msid mp) subst in
+ let subst = join subst' subst in
+ Some (subst_objects prefix (join (map_msid msid mp) subst) objs)
+ | _ -> None
(* This function registers the visibility of the module and iterates
through its components. It is called by plenty module functions *)
@@ -176,7 +190,6 @@ let do_module exists what iter_objects i dir mp substobjs 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
@@ -194,21 +207,25 @@ 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
- if mp <> mp_of_kn kn then
- anomaly "Kernel and Library names do not match";
+ if mp <> mp_of_kn kn then
+ anomaly "Kernel and Library names do not match";
- match sub_mtb_o with
- None -> ()
- | Some sub_mtb -> check_subtypes mp sub_mtb
+ match sub_mtb_o with
+ None -> ()
+ | Some (sub_mtb,sub) ->
+ check_subtypes mp sub_mtb
in
conv_names_do_module false "cache" load_objects 1 oname substobjs substituted
+
+
(* TODO: This check is not essential *)
let check_empty s = function
| None -> ()
@@ -231,18 +248,16 @@ let open_module i (oname,(entry,substobjs,substituted)) =
conv_names_do_module true "open" open_objects i oname substobjs substituted
-let subst_substobjs dir mp (subst,mbids,msid,objs) =
- match mbids with
- | [] ->
- let prefix = dir,(mp,empty_dirpath) in
- Some (subst_objects prefix (add_msid msid mp subst) objs)
- | _ -> None
-
let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
check_empty "subst_module" entry;
let dir,mp = dir_of_sp sp, mp_of_kn kn in
let (sub,mbids,msid,objs) = substobjs in
+ let sub = subst_key subst sub in
+ let sub' = update_subst_alias subst sub in
+ let sub' = update_subst_alias sub' (map_msid msid mp) in
+ (* let sub = join_alias sub sub' in*)
+ let sub = join sub' sub in
let subst' = join sub subst in
(* substitutive_objects get the new substitution *)
let substobjs = (subst',mbids,msid,objs) in
@@ -256,6 +271,8 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
let classify_module (_,(_,substobjs,_)) =
Substitute (None,substobjs,None)
+
+
let (in_module,out_module) =
declare_object {(default_object "MODULE") with
cache_function = cache_module;
@@ -266,6 +283,182 @@ let (in_module,out_module) =
export_function = (fun _ -> anomaly "No modules in sections!") }
+let rec replace_alias modalias_obj obj =
+ let rec put_alias (id_alias,obj_alias) l =
+ match l with
+ [] -> []
+ | (id,o)::r
+ when ( object_tag o = "MODULE") ->
+ if id = id_alias then
+(* let (entry,subst_o,substed_o) = out_module_alias obj_alias in
+ let (entry',subst_o',substed_o') = out_module o in
+ begin
+ match substed_o,substed_o' with
+ Some a,Some b ->
+ (id,in_module_alias
+ (entry,subst_o',Some (dump_alias_object a b)))::r*)
+ (id_alias,obj_alias)::r
+ (* | _,_ -> (id,o)::r
+ end*)
+ else (id,o)::(put_alias (id_alias,obj_alias) r)
+ | e::r -> e::(put_alias (id_alias,obj_alias) r) in
+ let rec choose_obj_alias list_alias list_obj =
+ match list_alias with
+ | [] -> list_obj
+ | o::r ->choose_obj_alias r (put_alias o list_obj) in
+ choose_obj_alias modalias_obj obj
+
+and dump_alias_object alias_obj obj =
+ let rec alias_in_obj seg =
+ match seg with
+ | [] -> []
+ | (id,o)::r when (object_tag o = "MODULE ALIAS") ->
+ (id,o)::(alias_in_obj r)
+ | e::r -> (alias_in_obj r) in
+ let modalias_obj = alias_in_obj alias_obj in
+ replace_alias modalias_obj obj
+
+and do_module_alias exists what iter_objects i dir mp alias substobjs objects =
+ let prefix = (dir,(alias,empty_dirpath)) in
+ let alias_objects =
+ try Some (MPmap.find alias !modtab_objects) with
+ Not_found -> None 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 alias_objects,objects with
+ Some (_,seg), Some seg' ->
+ let new_seg = dump_alias_object seg seg' in
+ modtab_objects := MPmap.add mp (prefix,new_seg) !modtab_objects;
+ iter_objects (i+1) prefix new_seg
+ | _,_-> ()
+
+and 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' = match me with
+ | {mod_entry_type = None;
+ mod_entry_expr = Some (MSEident mp)} ->
+ Global.add_alias (basename sp) mp
+ | _ -> anomaly "cache module alias"
+ 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,sub) ->
+ 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
+
+and 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 "Modops: Not an alias"
+ end
+ | None -> anomaly "Modops: Empty info"
+ in
+ do_module_alias false "load" load_objects i dir mp alias substobjs substituted
+
+and 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 "Modops: Not an alias"
+ end
+ | None -> anomaly "Modops: Empty info"
+ in
+ do_module_alias true "open" open_objects i dir mp alias substobjs substituted
+
+and 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 sub' = update_subst_alias subst (map_msid msid mp) in
+ let subst' = join sub' subst 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 *)
+ match entry with
+ | Some (me,sub)->
+ begin
+ match me with
+ |{mod_entry_type = None;
+ mod_entry_expr = Some (MSEident mp')} ->
+ let mp' = subst_mp subst' mp' in
+ let mp' = scrape_alias mp' in
+ (Some ({mod_entry_type = None;
+ mod_entry_expr =
+ Some (MSEident mp')},sub),
+ substobjs, match mbids with
+ | [] ->
+ Some (subst_objects (dir,(mp',empty_dirpath))
+ (join subst' (join (map_msid msid mp')
+ (map_mp mp mp'))) objs)
+ | _ -> None)
+
+ | _ -> anomaly "Modops: Not an alias"
+ end
+ | None -> anomaly "Modops: Empty info"
+
+and classify_module_alias (_,(entry,substobjs,_)) =
+ Substitute (entry,substobjs,None)
+
+let (in_module_alias,out_module_alias) =
+ declare_object {(default_object "MODULE ALIAS") with
+ cache_function = cache_module_alias;
+ open_function = open_module_alias;
+ classify_function = classify_module_alias;
+ subst_function = subst_module_alias;
+ load_function = load_module_alias;
+ export_function = (fun _ -> anomaly "No modules in sections!") }
+
+
+
+
+
let cache_keep _ = anomaly "This module should not be cached!"
let load_keep i ((sp,kn),seg) =
@@ -298,7 +491,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 +505,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 +526,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 +538,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;
@@ -381,77 +571,106 @@ let (in_modtype,out_modtype) =
load_function = load_modtype;
subst_function = subst_modtype;
classify_function = classify_modtype;
- export_function = in_some }
+ export_function = Option.make }
-let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs =
- if mbids<>[] then
+let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp =
+ let rec mp_rec = function
+ | [] -> MPself msid
+ | i::r -> MPdot(mp_rec r,label_of_id i)
+ in
+ if mbids<>[] then
error "Unexpected functor objects"
- else
- let rec replace_idl = function
- | _,[] -> []
- | id::idl,(id',obj)::tail when id = id' ->
- if object_tag obj = "MODULE" then
- (match idl with
- [] -> (id, in_module (None,modobjs,None))::tail
- | _ ->
- let (_,substobjs,_) = out_module obj in
- let substobjs' = replace_module_object idl substobjs modobjs in
- (id, in_module (None,substobjs',None))::tail
- )
- else error "MODULE expected!"
- | idl,lobj::tail -> lobj::replace_idl (idl,tail)
- in
- (subst, mbids, msid, replace_idl (idl,lib_stack))
-
+ else
+ let rec replace_idl = function
+ | _,[] -> []
+ | id::idl,(id',obj)::tail when id = id' ->
+ if object_tag obj = "MODULE" then
+ (match idl with
+ [] -> (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 mp in
+ (id, in_module (None,substobjs',None))::tail
+ )
+ else error "MODULE expected!"
+ | idl,lobj::tail -> lobj::replace_idl (idl,tail)
+ in
+ (join (map_mp (mp_rec (List.rev idl)) mp) subst, mbids, msid, replace_idl (idl,lib_stack))
+
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
- | MTEsig (msid,_) ->
- todo "Anonymous module types"; (empty_subst, [], msid, [])
+ replace_module_object idl substobjs modobjs mp
+ | MSEapply (mexpr, MSEident mp) ->
+ let ftb,sub1 = 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 mp = Environ.scrape_alias mp env in
+ let sub_alias = (Environ.lookup_modtype mp env).typ_alias in
+ let sub_alias = match Modops.eval_struct env (SEBident mp) with
+ | SEBstruct (msid,sign) -> join_alias
+ (subst_key (map_msid msid mp) sub_alias)
+ (map_msid msid mp)
+ | _ -> sub_alias in
+ let sub3=
+ if sub1 = empty_subst then
+ update_subst sub_alias (map_mbid farg_id mp None)
+ else
+ let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+ let sub_alias' = update_subst sub_alias sub1' in
+ join sub1' sub_alias'
+ in
+ let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) 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 sub_alias env in
+ (* application outside the kernel, only for substitutive
+ objects (that are all non-logical objects) *)
+ ((join
+ (join subst (map_mbid mbid mp (Some resolve)))
+ sub3)
+ , 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 *)
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
-
-let replace_module mtb id mb = todo "replace module after with"; mtb
-
-let rec get_some_body mty env = match mty with
- MTEident kn -> Environ.lookup_modtype kn env
- | MTEfunsig _
- | MTEsig _ -> anomaly "anonymous module types not supported"
- | 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)
-
-
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;
@@ -472,39 +691,35 @@ 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,sub = Mod_typing.translate_struct_entry (Global.env()) arg_t
+ in
+ let arg_t = {typ_expr = arg_t;
+ typ_strength = None;
+ typ_alias = sub} 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 ()
+ Lib.add_frozen_state (); mp
let end_module id =
let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
let mbids, res_o, sub_o = !openmod_info in
- let mp = Global.end_module id res_o in
-
- begin match sub_o with
- None -> ()
- | Some sub_mtb -> check_subtypes mp sub_mtb
- end;
-
let substitute, keep, special = Lib.classify_segment lib_stack in
let dir = fst oldprefix in
@@ -514,21 +729,27 @@ 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 (MTEsig (msid,_)) ->
- todo "Anonymous signatures not supported";
- (empty_subst, mbids, msid, []), keep, special
- | 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..."
- with
+ | Some (MSEapply _ as mty) ->
+ abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
+ with
Not_found -> anomaly "Module objects not found..."
in
-
- (* must be called after get_modtype_substobjs, because of possible
+ (* must be called after get_modtype_substobjs, because of possible
dependencies on functor arguments *)
+
+ let mp = Global.end_module id res_o in
+
+ begin match sub_o with
+ None -> ()
+ | Some sub_mtb -> check_subtypes mp sub_mtb
+ end;
+
Summary.module_unfreeze_summaries fs;
let substituted = subst_substobjs dir mp substobjs in
@@ -546,7 +767,8 @@ let end_module id =
if mp_of_kn (snd newoname) <> mp then
anomaly "Kernel and Library names do not match";
- Lib.add_frozen_state () (* to prevent recaching *)
+ Lib.add_frozen_state () (* to prevent recaching *);
+ mp
@@ -566,18 +788,13 @@ type library_objects =
mod_self_id * lib_objects * lib_objects
-(* The library_cache here is needed to avoid recalculations of
- substituted modules object during "reloading" of libraries *)
-let library_cache = Hashtbl.create 17
-
-
let register_library dir cenv objs digest =
let mp = MPfile dir in
let substobjs, objects =
try
ignore(Global.lookup_module mp);
(* if it's in the environment, the cached objects should be correct *)
- Hashtbl.find library_cache dir
+ Dirmap.find dir !library_cache
with
Not_found ->
if mp <> Global.import cenv digest then
@@ -585,9 +802,9 @@ let register_library dir cenv objs digest =
let msid,substitute,keep = objs in
let substobjs = empty_subst, [], msid, substitute in
let substituted = subst_substobjs dir mp substobjs in
- let objects = option_map (fun seg -> seg@keep) substituted in
+ let objects = Option.map (fun seg -> seg@keep) substituted in
let modobjs = substobjs, objects in
- Hashtbl.add library_cache dir modobjs;
+ library_cache := Dirmap.add dir modobjs !library_cache;
modobjs
in
do_module false "register_library" load_objects 1 dir mp substobjs objects
@@ -625,16 +842,17 @@ let classify_import (_,(export,_ as obj)) =
if export then Substitute obj else Dispose
let subst_import (_,subst,(export,mp as obj)) =
- let mp' = subst_mp subst mp in
+ let subst' = remove_alias subst in
+ let mp' = subst_mp subst' mp in
if mp'==mp then obj else
(export,mp')
-
+
let (in_import,out_import) =
declare_object {(default_object "IMPORT MODULE") with
- cache_function = cache_import;
- open_function = (fun i o -> if i=1 then cache_import o);
- subst_function = subst_import;
- classify_function = classify_import }
+ cache_function = cache_import;
+ open_function = (fun i o -> if i=1 then cache_import o);
+ subst_function = subst_import;
+ classify_function = classify_import }
let import_module export mp =
@@ -642,7 +860,6 @@ let import_module export mp =
(************************************************************************)
(* module types *)
-
let start_modtype interp_modtype id args =
let fs = Summary.freeze_summaries () in
@@ -653,7 +870,7 @@ let start_modtype interp_modtype id args =
openmodtype_info := mbids;
let prefix = Lib.start_modtype id mp fs in
Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
- Lib.add_frozen_state ()
+ Lib.add_frozen_state (); mp
let end_modtype id =
@@ -673,76 +890,202 @@ 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";
- Lib.add_frozen_state ()(* to prevent recaching *)
+ Lib.add_frozen_state ()(* to prevent recaching *);
+ ln
let declare_modtype interp_modtype id args mty =
let fs = Summary.freeze_summaries () in
- let _ = Global.start_modtype id in
+ try
+ let mmp = Global.start_modtype id in
let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
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;
- ignore (add_leaf id (in_modtype (Some entry, substobjs)))
+ ignore (add_leaf id (in_modtype (Some entry, substobjs)));
+ mmp
+ with e ->
+ (* Something wrong: undo the whole process *)
+ Summary.unfreeze_summaries fs; raise e
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)
- | MEstruct (msid,_) ->
- (empty_subst, [], msid, [])
- | 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,sub1 = 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 mp = Environ.scrape_alias mp env in
+ let sub_alias = (Environ.lookup_modtype mp env).typ_alias in
+ let sub_alias = match Modops.eval_struct env (SEBident mp) with
+ | SEBstruct (msid,sign) -> join_alias
+ (subst_key (map_msid msid mp) sub_alias)
+ (map_msid msid mp)
+ | _ -> sub_alias in
+
+ let sub3=
+ if sub1 = empty_subst then
+ update_subst sub_alias (map_mbid farg_id mp None)
+ else
+ let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+ let sub_alias' = update_subst sub_alias sub1' in
+ join sub1' sub_alias'
+ in
+ let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
let (subst, mbids, msid, objs) = get_module_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)
+ let resolve =
+ Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
+ (* application outside the kernel, only for substitutive
+ objects (that are all non-logical objects) *)
+ ((join
+ (join subst (map_mbid mbid mp (Some resolve)))
+ sub3)
+ , mbids, msid, objs)
| [] -> match mexpr with
- | MEident _ | MEstruct _ -> 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
+
+
+(* 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 ->
+ load_objects i prefix seg
+ | None -> ()
+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 rec update_include (sub,mbids,msid,objs) =
+ let rec replace_include = function
+ | [] -> []
+ | (id,obj)::tail ->
+ if object_tag obj = "INCLUDE" then
+ let ((me,is_mod),substobjs,substituted) = out_include obj in
+ if not (is_mod) then
+ let substobjs' = update_include substobjs in
+ (id, in_include ((me,true),substobjs',substituted))::
+ (replace_include tail)
+ else
+ (id,obj)::(replace_include tail)
+ else
+ (id,obj)::(replace_include tail)
+ in
+ (sub,mbids,msid,replace_include objs)
+
+
+
let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
+
let fs = Summary.freeze_summaries () in
- let _ = Global.start_module id in
+ try
+ let mmp = Global.start_module id in
let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
let mty_entry_o, mty_sub_o = match mty_o with
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 +1093,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,22 +1104,75 @@ 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
+ let substobjs = update_include substobjs in
+ (* Undo the simulated interactive building of the module *)
+ (* and declare the module as a whole *)
Summary.unfreeze_summaries fs;
+ 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 (sub,mbids,msid,objs) = substobjs in
+ let mp1 = Environ.scrape_alias mp env in
+ let prefix = dir,(mp1,empty_dirpath) in
+ let substituted =
+ match mbids with
+ | [] ->
+ Some (subst_objects prefix
+ (join sub (join (map_msid msid mp1) (map_mp mp' mp1))) objs)
+ | _ -> None in
+ ignore (add_leaf
+ id
+ (in_module_alias (Some ({mod_entry_type = None;
+ mod_entry_expr = Some (MSEident mp1) }, mty_sub_o),
+ substobjs, substituted)));
+ mmp
+ | _ ->
+ let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+ let (sub,mbids,msid,objs) = substobjs in
+ let sub' = subst_key (map_msid msid mp) sub in
+ let substobjs = (join sub sub',mbids,msid,objs) in
+ let substituted = subst_substobjs dir mp substobjs in
+ ignore (add_leaf
+ id
+ (in_module (Some (entry, mty_sub_o), substobjs, substituted)));
+ mmp
+
+ with e ->
+ (* Something wrong: undo the whole process *)
+ Summary.unfreeze_summaries fs; raise e
+
+
+let declare_include interp_struct me_ast is_mod =
- 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)))
-
+ 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