aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml25
-rw-r--r--library/declaremods.ml835
-rw-r--r--library/global.ml47
-rw-r--r--library/global.mli19
-rw-r--r--library/goptions.ml2
-rw-r--r--library/heads.ml16
-rw-r--r--library/impargs.ml4
-rw-r--r--library/impargs.mli2
-rw-r--r--library/lib.ml28
-rw-r--r--library/lib.mli10
-rw-r--r--library/libnames.ml58
-rw-r--r--library/libnames.mli15
-rw-r--r--library/libobject.ml14
-rw-r--r--library/libobject.mli6
-rw-r--r--library/library.ml2
-rw-r--r--library/nametab.ml22
16 files changed, 461 insertions, 644 deletions
diff --git a/library/declare.ml b/library/declare.ml
index da723aa4bf..1084aa07d6 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -100,12 +100,14 @@ let load_constant i ((sp,kn),(_,_,kind)) =
if Nametab.exists_cci sp then
errorlabstrm "cache_constant"
(pr_id (basename sp) ++ str " already exists");
- Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn));
- add_constant_kind (constant_of_kn kn) kind
-
+ let con = Global.constant_of_delta (constant_of_kn kn) in
+ Nametab.push (Nametab.Until i) sp (ConstRef con);
+ add_constant_kind con kind
+
(* Opening means making the name without its module qualification available *)
let open_constant i ((sp,kn),_) =
- Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
+ let con = constant_of_kn kn in
+ Nametab.push (Nametab.Exactly i) sp (ConstRef con)
let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
let id = basename sp in
@@ -187,6 +189,7 @@ let declare_inductive_argument_scopes kn mie =
let inductive_names sp kn mie =
let (dp,_) = repr_path sp in
+ let kn = Global.mind_of_delta (mind_of_kn kn) in
let names, _ =
List.fold_left
(fun (names, n) ind ->
@@ -228,17 +231,18 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
let id = basename sp in
let _,dir,_ = repr_kn kn in
let kn' = Global.add_mind dir id mie in
- assert (kn'=kn);
- add_section_kn kn (Global.lookup_mind kn').mind_hyps;
+ assert (kn'= mind_of_kn kn);
+ add_section_kn kn' (Global.lookup_mind kn').mind_hyps;
Dischargedhypsmap.set_discharged_hyps sp dhyps;
List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names;
List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie)
let discharge_inductive ((sp,kn),(dhyps,mie)) =
- let mie = Global.lookup_mind kn in
+ let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+ let mie = Global.lookup_mind mind in
let repl = replacement_context () in
- let sechyps = section_segment_of_mutual_inductive kn in
+ let sechyps = section_segment_of_mutual_inductive mind in
Some (discharged_hyps kn sechyps,
Discharge.process_inductive (named_of_variable_context sechyps) repl mie)
@@ -271,8 +275,9 @@ let declare_mind isrecord mie =
| ind::_ -> ind.mind_entry_typename
| [] -> anomaly "cannot declare an empty list of inductives" in
let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
- declare_mib_implicits kn;
- declare_inductive_argument_scopes kn mie;
+ let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+ declare_mib_implicits mind;
+ declare_inductive_argument_scopes mind mie;
!xml_declare_inductive (isrecord,oname);
oname
diff --git a/library/declaremods.ml b/library/declaremods.ml
index d796a2906f..548a9b0f36 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -22,7 +22,7 @@ open Mod_subst
(* modules and components *)
-(* This type is a functional closure of substitutive lib_objects.
+(* OBSOLETE This type is a functional closure of substitutive lib_objects.
The first part is a partial substitution (which will be later
applied to lib_objects when completed).
@@ -41,7 +41,7 @@ open Mod_subst
*)
type substitutive_objects =
- substitution * mod_bound_id list * mod_self_id * lib_objects
+ mod_bound_id list * module_path * lib_objects
(* For each module, we store the following things:
@@ -77,9 +77,10 @@ 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_struct_entry option
- * struct_expr_body option)
+let openmod_info =
+ ref ((MPfile(initial_dir),[],None,None)
+ : module_path * mod_bound_id list * module_struct_entry option
+ * module_type_body option)
(* The library_cache here is needed to avoid recalculations of
substituted modules object during "reloading" of libraries *)
@@ -99,7 +100,8 @@ let _ = Summary.declare_summary "MODULE-INFO"
Summary.init_function = (fun () ->
modtab_substobjs := MPmap.empty;
modtab_objects := MPmap.empty;
- openmod_info := ([],None,None);
+ openmod_info := ((MPfile(initial_dir),
+ [],None,None));
library_cache := Dirmap.empty) }
(* auxiliary functions to transform full_path and kernel_name given
@@ -116,50 +118,18 @@ let dir_of_sp sp =
let dir,id = repr_path sp in
add_dirpath_suffix dir id
-let msid_of_mp = function
- MPself msid -> msid
- | _ -> anomaly "'Self' module path expected!"
-
-let msid_of_prefix (_,(mp,sec)) =
- if sec=empty_dirpath then
- msid_of_mp mp
- else
- anomaly ("Non-empty section in module name!" ^
- string_of_mp mp ^ "." ^ string_of_dirpath sec)
-
-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_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)
+ let mb = Environ.lookup_module mp env in
+ let mtb = Modops.module_type_of_module env None mb in
+ let _ = Environ.add_constraints
+ (Subtyping.check_subtypes env mtb sub_mtb)
in
() (* The constraints are checked and forgot immediately! *)
-let compute_subst_objects mp (subst,mbids,msid,objs) =
- match mbids with
- | [] ->
- let subst' = join_alias (map_msid msid mp) subst in
- Some (join (map_msid msid mp) (join subst' subst), objs)
- | _ ->
- None
-
-let subst_substobjs dir mp substobjs =
- match compute_subst_objects mp substobjs with
- | Some (subst, objs) ->
- let prefix = dir,(mp,empty_dirpath) in
- Some (subst_objects prefix subst objs)
- | None -> None
-
(* These functions register the visibility of the module and iterates
through its components. They are called by plenty module functions *)
@@ -178,12 +148,12 @@ let compute_visibility exists what i dir dirinfo =
errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
else
Nametab.Until i
-
+(*
let do_load_and_subst_module i dir mp substobjs keep =
let prefix = (dir,(mp,empty_dirpath)) in
let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
let vis = compute_visibility false "load_and_subst" i dir dirinfo in
- let objects = compute_subst_objects mp substobjs in
+ let objects = compute_subst_objects mp substobjs resolver in
Nametab.push_dir vis dir dirinfo;
modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
match objects with
@@ -194,55 +164,33 @@ let do_load_and_subst_module i dir mp substobjs keep =
Some (seg@keep)
| None ->
None
+*)
-let do_module exists what iter_objects i dir mp substobjs objects =
+let do_module exists what iter_objects i dir mp substobjs keep=
let prefix = (dir,(mp,empty_dirpath)) in
let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
let vis = compute_visibility exists what i dir dirinfo 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 -> ()
+ match substobjs with
+ ([],mp1,objs) ->
+ modtab_objects := MPmap.add mp (prefix,objs@keep) !modtab_objects;
+ iter_objects (i+1) prefix (objs@keep)
+ | (mbids,_,_) -> ()
let conv_names_do_module exists what iter_objects i
- (sp,kn) substobjs substituted =
+ (sp,kn) substobjs =
let dir,mp = dir_of_sp sp, mp_of_kn kn in
- do_module exists what iter_objects i dir mp substobjs substituted
+ do_module exists what iter_objects i dir mp substobjs []
(* Interactive modules and module types cannot be recached! cache_mod*
functions can be called only once (and "end_mod*" set the flag to
false then)
*)
-
-let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) =
- let _ = 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";
-
- 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
-
-
-
-
+let cache_module ((sp,kn),(entry,substobjs)) =
+ let dir,mp = dir_of_sp sp, mp_of_kn kn in
+ do_module false "cache" load_objects 1 dir mp substobjs []
+
(* TODO: This check is not essential *)
let check_empty s = function
| None -> ()
@@ -253,42 +201,26 @@ let check_empty s = function
(* When this function is called the module itself is already in the
environment. This function loads its objects only *)
-let load_module i (oname,(entry,substobjs,substituted)) =
+let load_module i (oname,(entry,substobjs)) =
(* TODO: This check is not essential *)
check_empty "load_module" entry;
- conv_names_do_module false "load" load_objects i oname substobjs substituted
+ conv_names_do_module false "load" load_objects i oname substobjs
-let open_module i (oname,(entry,substobjs,substituted)) =
+let open_module i (oname,(entry,substobjs)) =
(* TODO: This check is not essential *)
check_empty "open_module" entry;
- conv_names_do_module true "open" open_objects i oname substobjs substituted
+ conv_names_do_module true "open" open_objects i oname substobjs
-let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
+let subst_module (subst,(entry,(mbids,mp,objs))) =
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
- (* if we are not a functor - calculate substitued.
- We add "msid |-> mp" to the substitution *)
- let substituted = subst_substobjs dir mp substobjs
- in
- (None,substobjs,substituted)
-
-
-let classify_module (_,substobjs,_) =
- Substitute (None,substobjs,None)
+ (None,(mbids,subst_mp subst mp, subst_objects subst objs))
+let classify_module (_,substobjs) =
+ Substitute (None,substobjs)
let (in_module,out_module) =
declare_object {(default_object "MODULE") with
@@ -298,168 +230,6 @@ let (in_module,out_module) =
subst_function = subst_module;
classify_function = classify_module }
-
-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 = compute_visibility exists what i dir dirinfo 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
- | [] -> let subst = update_subst subst' (map_mp mp' mp) in
- Some (subst_objects (dir,(mp',empty_dirpath))
- (join (join subst' 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 }
-
-
-
-
let cache_keep _ = anomaly "This module should not be cached!"
let load_keep i ((sp,kn),seg) =
@@ -553,9 +323,9 @@ let open_modtype i ((sp,kn),(entry,_)) =
Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
-let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) =
+let subst_modtype (subst,(entry,(mbids,mp,objs))) =
check_empty "subst_modtype" entry;
- (entry,(join subs subst,mbids,msid,objs))
+ (entry,(mbids,subst_mp subst mp,subst_objects subst objs))
let classify_modtype (_,substobjs) =
@@ -571,147 +341,143 @@ let (in_modtype,_) =
classify_function = classify_modtype }
-
-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
+let rec replace_module_object idl ( mbids, mp, lib_stack) (mbids2,mp2,objs) mp1=
+ if mbids<>[] then
error "Unexpected functor objects"
- else
- let rec replace_idl = function
- | _,[] -> []
- | id::idl,(id',obj)::tail when id = id' ->
- let tag = object_tag obj in
- if tag = "MODULE" or tag ="MODULE ALIAS" then
- (match idl with
- [] -> (id, in_module_alias (Some
- ({mod_entry_type = None;
- mod_entry_expr = Some (MSEident mp)},None)
- ,modobjs,None))::tail
- | _ ->
- let (a,substobjs,_) = if tag = "MODULE ALIAS" then
- out_module_alias obj else out_module obj in
- let substobjs' = replace_module_object idl substobjs modobjs mp in
- if tag = "MODULE ALIAS" then
- (id, in_module_alias (a,substobjs',None))::tail
- else
- (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 env = function
- MSEident ln -> MPmap.find ln !modtypetab
+ 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,(mbids,(MPdot(mp,label_of_id id)),subst_objects
+ (map_mp mp1 (MPdot(mp,label_of_id id)) empty_delta_resolver) objs)))::tail
+ | _ ->
+ let (_,substobjs) = out_module obj in
+ let substobjs' = replace_module_object idl substobjs
+ (mbids2,mp2,objs) mp in
+ (id, in_module (None,substobjs'))::tail
+ )
+ else error "MODULE expected!"
+ | idl,lobj::tail -> lobj::replace_idl (idl,tail)
+ in
+ (mbids, mp, replace_idl (idl,lib_stack))
+
+let discr_resolver mb =
+ match mb.mod_type with
+ SEBstruct _ ->
+ Some mb.mod_delta
+ | _ -> (*case mp is a functor *)
+ None
+
+(* Small function to avoid module typing during substobjs retrivial *)
+let rec get_objs_modtype_application env = function
+| MSEident mp ->
+ MPmap.find mp !modtypetab,Environ.lookup_modtype mp env,[]
+| MSEapply (fexpr, MSEident mp) ->
+ let objs,mtb,mp_l= get_objs_modtype_application env fexpr in
+ objs,mtb,mp::mp_l
+| MSEapply (_,mexpr) ->
+ Modops.error_application_to_not_path mexpr
+| _ -> error "Application of a non-functor."
+
+let rec get_modtype_substobjs env mp_from= 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)
- | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty
- | MSEwith (mty, With_Module (idl,mp)) ->
- let substobjs = get_modtype_substobjs env mty in
- let mp = Environ.scrape_alias mp env in
- let modobjs = MPmap.find mp !modtab_substobjs in
- 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 (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
- 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
- (* application outside the kernel, only for substitutive
- objects (that are all non-logical objects) *)
- ((join
- (join subst sub3)
- (map_mbid mbid mp (Some resolve)))
- , mbids, msid, objs)
- | [] -> match mexpr with
- | MSEident _ -> error "Application of a non-functor"
- | _ -> error "Application of a functor with too few arguments")
+ let (mbids, mp, objs) = get_modtype_substobjs env mp_from mte in
+ (mbid::mbids, mp, objs)
+ | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mp_from mty
+ | MSEwith (mty, With_Module (idl,mp1)) ->
+ let substobjs = get_modtype_substobjs env mp_from mty in
+ let modobjs = MPmap.find mp1 !modtab_substobjs in
+ replace_module_object idl substobjs modobjs mp1
+ | MSEapply (fexpr, MSEident mp) ->
+ let (mbids, mp1, objs),mtb_mp1,mp_l =
+ get_objs_modtype_application env (MSEapply(fexpr, MSEident mp)) in
+ let rec compute_subst mbids sign mp_l =
+ match mbids,mp_l with
+ [],[] -> [],empty_subst
+ | mbid,[] -> mbid,empty_subst
+ | [],r -> error ("Application of a functor with too few arguments.")
+ | mbid::mbids,mp::mp_l ->
+ let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+ let mb = Environ.lookup_module mp env in
+ let mp_delta = discr_resolver mb in
+ let mbid_left,subst=compute_subst mbids fbody_b mp_l in
+ if mp_delta = None then
+ mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst
+ else
+ let mp_delta = Modops.complete_inline_delta_resolver env mp
+ farg_id farg_b (Option.get mp_delta) in
+ mbid_left,join (map_mbid mbid mp mp_delta) subst
+ in
+ let mbids_left,subst = compute_subst mbids mtb_mp1.typ_expr (List.rev mp_l) in
+ (mbids_left, mp1,subst_objects subst objs)
| 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 (Global.env()) mty in
- ignore (do_load_and_subst_module 1 dir mp substobjs [])
- in
- List.iter2 process_arg argids args
-
+ let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mp mty in
+ let substobjs = (mbids,mp,subst_objects
+ (map_mp mp_from mp empty_delta_resolver) objs)in
+ do_module false "start" load_objects 1 dir mp substobjs []
+ in
+ List.iter2 process_arg argids args
+
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 (Global.env()) mty in
+ let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
+ (MPbound (List.hd mbids)) mty in
List.map2
(fun dir mbid ->
- Global.add_module_parameter mbid mty;
- let mp = MPbound mbid in
- ignore (do_load_and_subst_module 1 dir mp substobjs []);
- (mbid,mty))
+ let resolver = Global.add_module_parameter mbid mty in
+ let mp = MPbound mbid in
+ let substobjs = (mbi,mp,subst_objects
+ (map_mp mp_from mp resolver) objs) in
+ do_module false "interp" load_objects 1 dir mp substobjs [];
+ (mbid,mty))
dirs mbids
let start_module interp_modtype export id args res_o =
let fs = Summary.freeze_summaries () in
-
let mp = Global.start_module id in
let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
let res_entry_o, sub_body_o = match res_o with
None -> None, None
| Some (res, restricted) ->
(* we translate the module here to catch errors as early as possible *)
let mte = interp_modtype (Global.env()) res in
- if restricted then
- Some mte, None
- else
- 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,sub = Mod_typing.translate_struct_entry (Global.env()) arg_t
+ if restricted then
+ let _ = Mod_typing.translate_struct_type_entry (Global.env()) mte in
+ Some mte, None
+ else
+ let mtb = Mod_typing.translate_module_type (Global.env())
+ mp mte in
+ let funct_mtb =
+ List.fold_right
+ (fun (arg_id,arg_t) mte ->
+ let arg_t = Mod_typing.translate_module_type (Global.env())
+ (MPbound arg_id) 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
+ arg_entries mtb.typ_expr
+ in
+ None, Some {mtb with
+ typ_expr = funct_mtb}
in
let mbids = List.map fst arg_entries in
- openmod_info:=(mbids,res_entry_o,sub_body_o);
+ openmod_info:=(mp,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 (); mp
@@ -720,24 +486,25 @@ let start_module interp_modtype export id args res_o =
let end_module () =
let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in
- let mbids, res_o, sub_o = !openmod_info in
+ let mp,mbids, res_o, sub_o = !openmod_info in
let substitute, keep, special = Lib.classify_segment lib_stack in
- let dir = fst oldprefix in
- let msid = msid_of_prefix oldprefix in
-
- let substobjs, keep, special = try
+ let mp_from,substobjs, keep, special = try
match res_o with
| None ->
- (empty_subst, mbids, msid, substitute), keep, special
- | Some (MSEident ln) ->
- abstract_substobjs mbids (MPmap.find ln (!modtypetab)), [], []
+ (* the module is not sealed *)
+ None,( mbids, mp, substitute), keep, special
+ | Some (MSEident ln as mty) ->
+ let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in
+ Some mp1,(mbids@mbids1,mp1,objs), [], []
| Some (MSEwith _ as mty) ->
- abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
+ let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in
+ Some mp1,(mbids@mbids1,mp1,objs), [], []
| Some (MSEfunctor _) ->
anomaly "Funsig cannot be here..."
| Some (MSEapply _ as mty) ->
- abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
+ let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in
+ Some mp1,(mbids@mbids1,mp1,objs), [], []
with
Not_found -> anomaly "Module objects not found..."
in
@@ -745,15 +512,21 @@ let end_module () =
dependencies on functor arguments *)
let id = basename (fst oldoname) in
- let mp = Global.end_module fs id res_o in
+ let mp,resolver = Global.end_module fs id res_o in
begin match sub_o with
None -> ()
| Some sub_mtb -> check_subtypes mp sub_mtb
end;
- let substituted = subst_substobjs dir mp substobjs in
- let node = in_module (None,substobjs,substituted) in
+(* we substitute objects if the module is
+ sealed by a signature (ie. mp_from != None *)
+ let substobjs = match mp_from,substobjs with
+ None,_ -> substobjs
+ | Some mp_from,(mbids,_,objs) ->
+ (mbids,mp,subst_objects (map_mp mp_from mp resolver) objs)
+ in
+ let node = in_module (None,substobjs) in
let objects =
if keep = [] || mbids <> [] then
special@[node] (* no keep objects or we are defining a functor *)
@@ -785,28 +558,30 @@ type library_name = dir_path
(* The first two will form substitutive_objects, the last one is keep *)
type library_objects =
- mod_self_id * lib_objects * lib_objects
+ module_path * lib_objects * lib_objects
let register_library dir cenv objs digest =
let mp = MPfile dir in
- try
+ let substobjs, keep =
+ try
ignore(Global.lookup_module mp);
(* if it's in the environment, the cached objects should be correct *)
- let substobjs, objects = Dirmap.find dir !library_cache in
- do_module false "register_library" load_objects 1 dir mp substobjs objects
+ Dirmap.find dir !library_cache
with Not_found ->
if mp <> Global.import cenv digest then
anomaly "Unexpected disk module name";
- let msid,substitute,keep = objs in
- let substobjs = empty_subst, [], msid, substitute in
- let objects = do_load_and_subst_module 1 dir mp substobjs keep in
- let modobjs = substobjs, objects in
- library_cache := Dirmap.add dir modobjs !library_cache
+ let mp,substitute,keep = objs in
+ let substobjs = [], mp, substitute in
+ let modobjs = substobjs, keep in
+ library_cache := Dirmap.add dir modobjs !library_cache;
+ modobjs
+ in
+ do_module false "register_library" load_objects 1 dir mp substobjs keep
let start_library dir =
let mp = Global.start_library dir in
- openmod_info:=[],None,None;
+ openmod_info:=mp,[],None,None;
Lib.start_compilation dir mp;
Lib.add_frozen_state ()
@@ -816,10 +591,9 @@ let set_end_library_hook f = end_library_hook := f
let end_library dir =
!end_library_hook();
let prefix, lib_stack = Lib.end_compilation dir in
- let cenv = Global.export dir in
- let msid = msid_of_prefix prefix in
+ let mp,cenv = Global.export dir in
let substitute, keep, _ = Lib.classify_segment lib_stack in
- cenv,(msid,substitute,keep)
+ cenv,(mp,substitute,keep)
(* implementation of Export M and Import M *)
@@ -838,8 +612,8 @@ let cache_import (_,(_,mp)) =
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_import (subst,(export,mp as obj)) =
+ let mp' = subst_mp subst mp in
if mp'==mp then obj else
(export,mp')
@@ -870,27 +644,23 @@ let start_modtype interp_modtype id args =
let end_modtype () =
-
let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in
let id = basename (fst oldoname) in
let substitute, _, special = Lib.classify_segment lib_stack in
-
- let msid = msid_of_prefix prefix in
let mbids = !openmodtype_info in
- let modtypeobjs = empty_subst, mbids, msid, substitute in
-
- let ln = Global.end_modtype fs id in
+ let mp = Global.end_modtype fs id in
+ let modtypeobjs = mbids, mp, substitute in
let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in
if fst oname <> fst oldoname then
anomaly
"Section paths generated on start_ and end_modtype do not match";
- if (mp_of_kn (snd oname)) <> ln then
+ if (mp_of_kn (snd oname)) <> mp then
anomaly
"Kernel and Library names do not match";
Lib.add_frozen_state ()(* to prevent recaching *);
- ln
+ mp
let declare_modtype interp_modtype id args mty =
@@ -907,64 +677,79 @@ let declare_modtype interp_modtype id args mty =
arg_entries
base_mty
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;
+ let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp entry in
+ (* Undo the simulated interactive building of the module type *)
+ (* and declare the module type as a whole *)
- ignore (add_leaf id (in_modtype (Some entry, substobjs)));
- mmp
+ let substobjs = (mbids,mmp,
+ subst_objects (map_mp mp_from mmp empty_delta_resolver) objs) in
+ Summary.unfreeze_summaries fs;
+ ignore (add_leaf id (in_modtype (Some entry, substobjs)));
+ mmp
with e ->
(* Something wrong: undo the whole process *)
Summary.unfreeze_summaries fs; raise e
+(* Small function to avoid module typing during substobjs retrivial *)
+let rec get_objs_module_application env = function
+| MSEident mp ->
+ MPmap.find mp !modtab_substobjs,Environ.lookup_module mp env,[]
+| MSEapply (fexpr, MSEident mp) ->
+ let objs,mtb,mp_l= get_objs_module_application env fexpr in
+ objs,mtb,mp::mp_l
+| MSEapply (_,mexpr) ->
+ Modops.error_application_to_not_path mexpr
+| _ -> error "Application of a non-functor."
-let rec get_module_substobjs env = function
+
+let rec get_module_substobjs env mp_from = function
| 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)
- | 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 (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
+ let (mbids, mp, objs) = get_module_substobjs env mp_from mexpr in
+ (mbid::mbids, mp, objs)
+ | MSEapply (fexpr, MSEident mp) ->
+ let (mbids, mp1, objs),mb_mp1,mp_l =
+ get_objs_module_application env (MSEapply(fexpr, MSEident mp)) in
+ let rec compute_subst mbids sign mp_l =
+ match mbids,mp_l with
+ [],[] -> [],empty_subst
+ | mbid,[] -> mbid,empty_subst
+ | [],r -> error ("Application of a functor with too few arguments.")
+ | mbid::mbids,mp::mp_l ->
+ let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+ let mb = Environ.lookup_module mp env in
+ let mp_delta = discr_resolver mb in
+ let mbid_left,subst=compute_subst mbids fbody_b mp_l in
+ if mp_delta = None then
+ mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst
+ else
+ let mp_delta = Modops.complete_inline_delta_resolver env mp
+ farg_id farg_b (Option.get mp_delta) in
+ mbid_left,join (map_mbid mbid mp mp_delta) subst
+ in
+ let mbids_left,subst = compute_subst mbids mb_mp1.mod_type (List.rev mp_l) in
+ (mbids_left, mp1,subst_objects subst objs)
+ (* let sign,alg,equiv,_ = Mod_typing.translate_struct_module_entry env mp_from fexpr in
+ let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+ let mb = Environ.lookup_module mp env in
+ let mp_delta = discr_resolver mb in
+ let (mbids, mp1, objs) = get_module_substobjs env mp_from fexpr in
(match mbids with
| mbid::mbids ->
- let resolve =
- Modops.resolver_of_environment farg_id farg_b mp sub_alias env 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
- (* application outside the kernel, only for substitutive
- objects (that are all non-logical objects) *)
- ((join
- (join subst sub3)
- (map_mbid mbid mp (Some resolve)))
- , mbids, msid, objs)
- | [] -> match mexpr with
+ if mp_delta = None then
+ (mbids, mp1,subst_objects (map_mbid mbid mp empty_delta_resolver) objs)
+ else
+ let mp_delta = Modops.complete_inline_delta_resolver env mp
+ farg_id farg_b (Option.get mp_delta) in
+ (mbids, mp1,subst_objects (map_mbid mbid mp mp_delta) objs)
+ | [] -> match fexpr with
| MSEident _ -> error "Application of a non-functor."
- | _ -> error "Application of a functor with too few arguments.")
+ | _ -> error "Application of a functor with too few arguments.")*)
| 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
+ | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from mty
+ | MSEwith (mty, With_Module (idl,mp)) -> assert false
+
(* Include *)
@@ -991,46 +776,32 @@ let lift_oname (sp,kn) =
let dir,_ = Libnames.repr_path sp in
(dir,mp)
-let cache_include (oname,((me,is_mod),substobjs,substituted)) =
+let cache_include (oname,((me,is_mod),(mbis,mp1,objs))) =
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)) =
+ load_objects 1 prefix objs;
+ open_objects 1 prefix objs
+
+let load_include i (oname,((me,is_mod),(mbis,mp1,objs))) =
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)) =
+ load_objects i prefix objs
+
+
+let open_include i (oname,((me,is_mod),(mbis,mp1,objs))) =
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)
+ if is_mod || i = 1 then
+ open_objects i prefix objs
+ else ()
+
+let subst_include (subst,((me,is_mod),substobj)) =
+ let (mbids,mp,objs) = substobj in
+ let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in
+ ((subst_inc_expr subst me,is_mod),substobjs)
+
+let classify_include ((me,is_mod),substobjs) =
+ Substitute ((me,is_mod),substobjs)
let (in_include,out_include) =
declare_object {(default_object "INCLUDE") with
@@ -1040,20 +811,19 @@ let (in_include,out_include) =
subst_function = subst_include;
classify_function = classify_include }
-let rec update_include (sub,mbids,msid,objs) =
+let rec update_include (mbids,mp,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
+ let ((me,is_mod),substobjs) = out_include obj in
let substobjs' = update_include substobjs in
- (id, in_include ((me,true),substobjs',substituted))::
+ (id, in_include ((me,true),substobjs'))::
(replace_include tail)
else
(id,obj)::(replace_include tail)
in
- (sub,mbids,msid,replace_include objs)
-
+ (mbids,mp,replace_include objs)
let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
@@ -1084,8 +854,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
Some (List.fold_right
(fun (mbid,mte) me -> MSEfunctor(mbid,mte,me))
arg_entries
- (interp_modexpr (Global.env()) mexpr))
- in
+ (interp_modexpr (Global.env()) mexpr)) in
let entry =
{mod_entry_type = mty_entry_o;
mod_entry_expr = mexpr_entry_o }
@@ -1093,45 +862,33 @@ 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 env mte
- | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr
+ | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp mte
+ | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp mexpr
| _ -> anomaly "declare_module: No type, no body ..."
in
- let substobjs = update_include substobjs in
+ let (mbids,mp_from,objs) = 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' = join_alias (subst_key (map_msid msid mp) sub) (map_msid msid mp) in
- let substobjs = ( 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 ->
+ let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+ let mp_env,resolver = Global.add_module id entry in
+ let _ = if mp_env <> mp then
+ anomaly "Kernel and Library names do not match";
+ match mty_sub_o with
+ | None -> ()
+ | Some sub_mte ->
+ let sub_mtb = Mod_typing.translate_module_type
+ env mp sub_mte in
+ check_subtypes mp_env sub_mtb
+ in
+ let substobjs = (mbids,mp_env,
+ subst_objects(map_mp mp_from mp_env resolver) objs) in
+ ignore (add_leaf
+ id
+ (in_module (Some (entry, mty_sub_o), substobjs)));
+ mmp
+
+ with e ->
(* Something wrong: undo the whole process *)
Summary.unfreeze_summaries fs; raise e
@@ -1142,19 +899,19 @@ let declare_include interp_struct me_ast is_mod =
try
let env = Global.env() in
- let me = interp_struct env me_ast in
- let substobjs =
+ let me = interp_struct env me_ast in
+ let mp1,_ = current_prefix () in
+ let (mbids,mp,objs)=
if is_mod then
- get_module_substobjs env me
+ get_module_substobjs env mp1 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
+ get_modtype_substobjs env mp1 me in
let id = current_mod_id() in
-
+ let resolver = Global.add_include me is_mod in
+ let substobjs = (mbids,mp1,
+ subst_objects (map_mp mp mp1 resolver) objs) in
ignore (add_leaf id
- (in_include ((me,is_mod), substobjs, substituted)))
+ (in_include ((me,is_mod), substobjs)))
with e ->
(* Something wrong: undo the whole process *)
Summary.unfreeze_summaries fs; raise e
diff --git a/library/global.ml b/library/global.ml
index e228de23a7..6d7942ec07 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -48,14 +48,6 @@ let push_named_def d =
global_env := env;
cst
-(*let add_thing add kn thing =
- let _,dir,l = repr_kn kn in
- let kn',newenv = add dir l thing !global_env in
- if kn = kn' then
- global_env := newenv
- else
- anomaly "Kernel names do not match."
-*)
let add_thing add dir id thing =
let kn, newenv = add dir (label_of_id id) thing !global_env in
@@ -65,14 +57,23 @@ let add_thing add dir id thing =
let add_constant = add_thing add_constant
let add_mind = add_thing add_mind
let add_modtype = add_thing (fun _ -> add_modtype) ()
-let add_module = add_thing (fun _ -> add_module) ()
-let add_alias = add_thing (fun _ -> add_alias) ()
+
+
+let add_module id me =
+ let l = label_of_id id in
+ let mp,resolve,new_env = add_module l me !global_env in
+ global_env := new_env;
+ mp,resolve
+
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 add_include me is_module =
+ let resolve,newenv = add_include me is_module !global_env in
+ global_env := newenv;
+ resolve
let start_module id =
let l = label_of_id id in
@@ -82,15 +83,16 @@ let start_module id =
let end_module fs id mtyo =
let l = label_of_id id in
- let mp,newenv = end_module l mtyo !global_env in
+ let mp,resolve,newenv = end_module l mtyo !global_env in
Summary.unfreeze_summaries fs;
global_env := newenv;
- mp
+ mp,resolve
let add_module_parameter mbid mte =
- let newenv = add_module_parameter mbid mte !global_env in
- global_env := newenv
+ let resolve,newenv = add_module_parameter mbid mte !global_env in
+ global_env := newenv;
+ resolve
let start_modtype id =
@@ -117,15 +119,22 @@ let lookup_mind kn = lookup_mind kn (env())
let lookup_module mp = lookup_module mp (env())
let lookup_modtype kn = lookup_modtype kn (env())
+let constant_of_delta con =
+ let resolver,resolver_param = (delta_of_senv !global_env) in
+ Mod_subst.constant_of_delta resolver_param
+ (Mod_subst.constant_of_delta resolver con)
-
-
+let mind_of_delta mind =
+ let resolver,resolver_param = (delta_of_senv !global_env) in
+ Mod_subst.mind_of_delta resolver_param
+ (Mod_subst.mind_of_delta resolver mind)
+
let start_library dir =
let mp,newenv = start_library dir !global_env in
global_env := newenv;
mp
-let export s = snd (export !global_env s)
+let export s = export !global_env s
let import cenv digest =
let mp,newenv = import cenv digest !global_env in
@@ -161,3 +170,5 @@ let register field value by_clause =
let entry = kind_of_term value in
let senv = Safe_typing.register !global_env field entry by_clause in
global_env := senv
+
+
diff --git a/library/global.mli b/library/global.mli
index 3c2317122c..30bd041503 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -15,6 +15,7 @@ open Term
open Declarations
open Entries
open Indtypes
+open Mod_subst
open Safe_typing
(*i*)
@@ -47,12 +48,11 @@ val push_named_def : (identifier * constr * types option) -> Univ.constraints
val add_constant :
dir_path -> identifier -> global_declaration -> constant
val add_mind :
- dir_path -> identifier -> mutual_inductive_entry -> kernel_name
+ dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive
-val add_module : identifier -> module_entry -> module_path
+val add_module : identifier -> module_entry -> module_path * delta_resolver
val add_modtype : identifier -> module_struct_entry -> module_path
-val add_include : module_struct_entry -> unit
-val add_alias : identifier -> module_path -> module_path
+val add_include : module_struct_entry -> bool -> delta_resolver
val add_constraints : constraints -> unit
@@ -66,10 +66,11 @@ val set_engagement : engagement -> unit
of the started module / module type *)
val start_module : identifier -> module_path
-val end_module :
- Summary.frozen -> identifier -> module_struct_entry option -> module_path
-val add_module_parameter : mod_bound_id -> module_struct_entry -> unit
+val end_module : Summary.frozen ->identifier -> module_struct_entry option ->
+ module_path * delta_resolver
+
+val add_module_parameter : mod_bound_id -> module_struct_entry -> delta_resolver
val start_modtype : identifier -> module_path
val end_modtype : Summary.frozen -> identifier -> module_path
@@ -83,10 +84,12 @@ 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 : module_path -> module_type_body
+val constant_of_delta : constant -> constant
+val mind_of_delta : mutual_inductive -> mutual_inductive
(* Compiled modules *)
val start_library : dir_path -> module_path
-val export : dir_path -> compiled_library
+val export : dir_path -> module_path * compiled_library
val import : compiled_library -> Digest.t -> module_path
(*s Function to get an environment from the constants part of the global
diff --git a/library/goptions.ml b/library/goptions.ml
index 032016c3db..06d4b618e5 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -91,7 +91,7 @@ module MakeTable =
| GOadd -> t := MySet.add p !t
| GOrmv -> t := MySet.remove p !t in
let load_options i o = if i=1 then cache_options o in
- let subst_options (_,subst,(f,p as obj)) =
+ let subst_options (subst,(f,p as obj)) =
let p' = A.subst subst p in
if p' == p then obj else
(f,p')
diff --git a/library/heads.ml b/library/heads.ml
index 150ba89422..056f78a5f3 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -39,8 +39,20 @@ type head_approximation =
(** Registration as global tables and rollback. *)
+module Evalreford = struct
+ type t = evaluable_global_reference
+ let compare x y =
+ let make_name = function
+ | EvalConstRef con ->
+ EvalConstRef(constant_of_kn(canonical_con con))
+ | k -> k
+ in
+ Pervasives.compare (make_name x) (make_name y)
+end
+
module Evalrefmap =
- Map.Make (struct type t = evaluable_global_reference let compare = compare end)
+ Map.Make (Evalreford)
+
let head_map = ref Evalrefmap.empty
@@ -144,7 +156,7 @@ let subst_head_approximation subst = function
kind_of_head (Global.env()) c
| x -> x
-let subst_head (_,subst,(ref,k)) =
+let subst_head (subst,(ref,k)) =
(subst_evaluable_reference subst ref, subst_head_approximation subst k)
let discharge_head (_,(ref,k)) =
diff --git a/library/impargs.ml b/library/impargs.ml
index d27ced2204..1edac69aa8 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -435,7 +435,7 @@ type implicit_interactive_request =
type implicit_discharge_request =
| ImplLocal
| ImplConstant of constant * implicits_flags
- | ImplMutualInductive of kernel_name * implicits_flags
+ | ImplMutualInductive of mutual_inductive * implicits_flags
| ImplInteractive of global_reference * implicits_flags *
implicit_interactive_request
@@ -455,7 +455,7 @@ let cache_implicits o =
let subst_implicits_decl subst (r,imps as o) =
let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
-let subst_implicits (_,subst,(req,l)) =
+let subst_implicits (subst,(req,l)) =
(ImplLocal,list_smartmap (subst_implicits_decl subst) l)
let impls_of_context ctx =
diff --git a/library/impargs.mli b/library/impargs.mli
index 6d2b01e8f5..e8191e863a 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -108,7 +108,7 @@ type implicit_interactive_request =
type implicit_discharge_request =
| ImplLocal
| ImplConstant of constant * implicits_flags
- | ImplMutualInductive of kernel_name * implicits_flags
+ | ImplMutualInductive of mutual_inductive * implicits_flags
| ImplInteractive of global_reference * implicits_flags *
implicit_interactive_request
diff --git a/library/lib.ml b/library/lib.ml
index 961a4ebb99..b8dcee9d26 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -37,21 +37,21 @@ let iter_objects f i prefix =
let load_objects = iter_objects load_object
let open_objects = iter_objects open_object
-let subst_objects prefix subst seg =
+let subst_objects subst seg =
let subst_one = fun (id,obj as node) ->
- let obj' = subst_object (make_oname prefix id, subst, obj) in
+ let obj' = subst_object (subst,obj) in
if obj' == obj then node else
(id, obj')
in
list_smartmap subst_one seg
-let load_and_subst_objects i prefix subst seg =
+(*let load_and_subst_objects i prefix subst seg =
List.rev (List.fold_left (fun seg (id,obj as node) ->
let obj' = subst_object (make_oname prefix id, subst, obj) in
let node = if obj == obj' then node else (id, obj') in
load_object i (make_oname prefix id, obj');
node :: seg) [] seg)
-
+*)
let classify_segment seg =
let rec clean ((substl,keepl,anticipl) as acc) = function
| (_,CompilingLibrary _) :: _ | [] -> acc
@@ -435,13 +435,13 @@ type binding_kind = Explicit | Implicit
type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types
type variable_context = variable_info list
-type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
+type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t
let sectab =
ref ([] : ((Names.identifier * binding_kind) list * Cooking.work_list * abstr_list) list)
let add_section () =
- sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
+ sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
let add_section_variable id impl =
match !sectab with
@@ -474,7 +474,7 @@ let add_section_replacement f g hyps =
sectab := (vars,f args exps,g sechyps abs)::sl
let add_section_kn kn =
- let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in
+ let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
add_section_replacement f f
let add_section_constant kn =
@@ -489,7 +489,7 @@ let section_segment_of_constant con =
Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
let section_segment_of_mutual_inductive kn =
- Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
+ Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
let rec list_mem_assoc x = function
| [] -> raise Not_found
@@ -502,7 +502,7 @@ let section_instance = function
| ConstRef con ->
Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
- Names.KNmap.find kn (snd (pi2 (List.hd !sectab)))
+ Names.Mindmap.find kn (snd (pi2 (List.hd !sectab)))
let is_in_section ref =
try ignore (section_instance ref); true with Not_found -> false
@@ -772,7 +772,7 @@ let mp_of_global ref =
let rec dp_of_mp modp =
match modp with
| Names.MPfile dp -> dp
- | Names.MPbound _ | Names.MPself _ -> library_dp ()
+ | Names.MPbound _ -> library_dp ()
| Names.MPdot (mp,_) -> dp_of_mp mp
let rec split_mp mp =
@@ -781,7 +781,6 @@ let rec split_mp mp =
| Names.MPdot (prfx, lbl) ->
let mprec, dprec = split_mp prfx in
mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
- | Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in library_dp(), Names.make_dirpath [Names.id_of_string id]
| Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [Names.id_of_string id]
let split_modpath mp =
@@ -789,7 +788,6 @@ let split_modpath mp =
| Names.MPfile dp -> dp, []
| Names.MPbound mbid ->
library_dp (), [Names.id_of_mbid mbid]
- | Names.MPself msid -> library_dp (), [Names.id_of_msid msid]
| Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
(mp', Names.id_of_label l :: lab)
in
@@ -819,8 +817,8 @@ let remove_section_part ref =
(* Discharging names *)
let pop_kn kn =
- let (mp,dir,l) = Names.repr_kn kn in
- Names.make_kn mp (pop_dirpath dir) l
+ let (mp,dir,l) = Names.repr_mind kn in
+ Names.make_mind mp (pop_dirpath dir) l
let pop_con con =
let (mp,dir,l) = Names.repr_con con in
@@ -831,7 +829,7 @@ let con_defined_in_sec kn =
dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
let defined_in_sec kn =
- let _,dir,_ = Names.repr_kn kn in
+ let _,dir,_ = Names.repr_mind kn in
dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
let discharge_global = function
diff --git a/library/lib.mli b/library/lib.mli
index 0e2e304cdf..32d1c0009b 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -32,8 +32,8 @@ type lib_objects = (Names.identifier * Libobject.obj) list
val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
-val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
-val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
+val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects
+(*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
(* [classify_segment seg] verifies that there are no OpenedThings,
clears ClosedSections and FrozenStates and divides Leafs according
@@ -183,13 +183,13 @@ val is_in_section : Libnames.global_reference -> bool
val add_section_variable : Names.identifier -> binding_kind -> unit
val add_section_constant : Names.constant -> Sign.named_context -> unit
-val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
+val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit
val replacement_context : unit ->
- (Names.identifier array Names.Cmap.t * Names.identifier array Names.KNmap.t)
+ (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t)
(*s Discharge: decrease the section level if in the current section *)
-val discharge_kn : Names.kernel_name -> Names.kernel_name
+val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive
val discharge_con : Names.constant -> Names.constant
val discharge_global : Libnames.global_reference -> Libnames.global_reference
val discharge_inductive : Names.inductive -> Names.inductive
diff --git a/library/libnames.ml b/library/libnames.ml
index 2b335ea6c9..fad0336fc2 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -27,13 +27,21 @@ let isConstRef = function ConstRef _ -> true | _ -> false
let isIndRef = function IndRef _ -> true | _ -> false
let isConstructRef = function ConstructRef _ -> true | _ -> false
+let eq_gr gr1 gr2 =
+ match gr1,gr2 with
+ ConstRef con1, ConstRef con2 ->
+ eq_constant con1 con2
+ | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2
+ | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2
+ | _,_ -> gr1=gr2
+
let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
let subst_constructor subst ((kn,i),j as ref) =
- let kn' = subst_kn subst kn in
+ let kn' = subst_ind subst kn in
if kn==kn' then ref, mkConstruct ref
else ((kn',i),j), mkConstruct ((kn',i),j)
@@ -43,7 +51,7 @@ let subst_global subst ref = match ref with
let kn',t = subst_con subst kn in
if kn==kn' then ref, mkConst kn else ConstRef kn', t
| IndRef (kn,i) ->
- let kn' = subst_kn subst kn in
+ let kn' = subst_ind subst kn in
if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
| ConstructRef ((kn,i),j as c) ->
let c',t = subst_constructor subst c in
@@ -65,15 +73,25 @@ let constr_of_global = function
let constr_of_reference = constr_of_global
let reference_of_constr = global_of_constr
-module RefOrdered =
- struct
- type t = global_reference
- let compare = Pervasives.compare
- end
-
+(* outside of the kernel, names are ordered on their canonical part *)
+module RefOrdered = struct
+ type t = global_reference
+ let compare x y =
+ let make_name = function
+ | ConstRef con ->
+ ConstRef(constant_of_kn(canonical_con con))
+ | IndRef (kn,i) ->
+ IndRef(mind_of_kn(canonical_mind kn),i)
+ | ConstructRef ((kn,i),j )->
+ ConstructRef((mind_of_kn(canonical_mind kn),i),j)
+ | VarRef id -> VarRef id
+ in
+ Pervasives.compare (make_name x) (make_name y)
+end
+
module Refset = Set.Make(RefOrdered)
module Refmap = Map.Make(RefOrdered)
-
+
(* Extended global references *)
type syndef_name = kernel_name
@@ -191,26 +209,22 @@ let restrict_path n sp =
let dir' = list_firstn n (repr_dirpath dir) in
make_path (make_dirpath dir') s
-let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
+let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id)
let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
-let decode_kn kn =
- let rec dirpath_of_module = function
+let decode_mind kn =
+ let rec dir_of_mp = function
| MPfile dir -> repr_dirpath dir
- | MPbound mbid ->
+ | MPbound mbid ->
let _,_,dp = repr_mbid mbid in
let id = id_of_mbid mbid in
id::(repr_dirpath dp)
- | MPself msid ->
- let _,_,dp = repr_msid msid in
- let id = id_of_msid msid in
- id::(repr_dirpath dp)
- | MPdot(mp,l) -> (id_of_label l)::(dirpath_of_module mp)
+ | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
in
- let mp,sec_dir,l = repr_kn kn in
+ let mp,sec_dir,l = repr_mind kn in
if (repr_dirpath sec_dir) = [] then
- (make_dirpath (dirpath_of_module mp)),id_of_label l
+ (make_dirpath (dir_of_mp mp)),id_of_label l
else
anomaly "Section part should be empty!"
@@ -289,8 +303,8 @@ let pop_con con =
Names.make_con mp (pop_dirpath dir) l
let pop_kn kn =
- let (mp,dir,l) = repr_kn kn in
- Names.make_kn mp (pop_dirpath dir) l
+ let (mp,dir,l) = repr_mind kn in
+ Names.make_mind mp (pop_dirpath dir) l
let pop_global_reference = function
| ConstRef con -> ConstRef (pop_con con)
diff --git a/library/libnames.mli b/library/libnames.mli
index 43ca252c1c..fd2ca37ae1 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -28,11 +28,14 @@ val isConstRef : global_reference -> bool
val isIndRef : global_reference -> bool
val isConstructRef : global_reference -> bool
+val eq_gr : global_reference -> global_reference -> bool
+
val destVarRef : global_reference -> variable
val destConstRef : global_reference -> constant
val destIndRef : global_reference -> inductive
val destConstructRef : global_reference -> constructor
+
val subst_constructor : substitution -> constructor -> constructor * constr
val subst_global : substitution -> global_reference -> global_reference * constr
@@ -47,6 +50,12 @@ val global_of_constr : constr -> global_reference
val constr_of_reference : global_reference -> constr
val reference_of_constr : constr -> global_reference
+module RefOrdered : sig
+ type t = global_reference
+ val compare : global_reference -> global_reference -> int
+end
+
+
module Refset : Set.S with type elt = global_reference
module Refmap : Map.S with type key = global_reference
@@ -108,8 +117,8 @@ val restrict_path : int -> full_path -> full_path
(*s Temporary function to brutally form kernel names from section paths *)
-val encode_kn : dir_path -> identifier -> kernel_name
-val decode_kn : kernel_name -> dir_path * identifier
+val encode_mind : dir_path -> identifier -> mutual_inductive
+val decode_mind : mutual_inductive -> dir_path * identifier
val encode_con : dir_path -> identifier -> constant
val decode_con : constant -> dir_path * identifier
@@ -170,7 +179,7 @@ val loc_of_reference : reference -> loc
(*s Popping one level of section in global names *)
val pop_con : constant -> constant
-val pop_kn : kernel_name -> kernel_name
+val pop_kn : mutual_inductive-> mutual_inductive
val pop_global_reference : global_reference -> global_reference
(* Deprecated synonyms *)
diff --git a/library/libobject.ml b/library/libobject.ml
index 4bd701e137..ecdcacf1d2 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -34,7 +34,7 @@ type 'a object_declaration = {
load_function : int -> object_name * 'a -> unit;
open_function : int -> object_name * 'a -> unit;
classify_function : 'a -> 'a substitutivity;
- subst_function : object_name * substitution * 'a -> 'a;
+ subst_function : substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
rebuild_function : 'a -> 'a }
@@ -63,7 +63,7 @@ let default_object s = {
This helps introducing new functions in objects.
*)
-let ident_subst_function (_,_,a) = a
+let ident_subst_function (_,a) = a
type obj = Dyn.t (* persistent dynamic objects *)
@@ -71,7 +71,7 @@ type dynamic_object_declaration = {
dyn_cache_function : object_name * obj -> unit;
dyn_load_function : int -> object_name * obj -> unit;
dyn_open_function : int -> object_name * obj -> unit;
- dyn_subst_function : object_name * substitution * obj -> obj;
+ dyn_subst_function : substitution * obj -> obj;
dyn_classify_function : obj -> obj substitutivity;
dyn_discharge_function : object_name * obj -> obj option;
dyn_rebuild_function : obj -> obj }
@@ -93,9 +93,9 @@ let declare_object odecl =
and opener i (oname,lobj) =
if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj)
else anomaly "somehow we got the wrong dynamic object in the openfun"
- and substituter (oname,sub,lobj) =
- if Dyn.tag lobj = na then
- infun (odecl.subst_function (oname,sub,outfun lobj))
+ and substituter (sub,lobj) =
+ if Dyn.tag lobj = na then
+ infun (odecl.subst_function (sub,outfun lobj))
else anomaly "somehow we got the wrong dynamic object in the substfun"
and classifier lobj =
if Dyn.tag lobj = na then
@@ -158,7 +158,7 @@ let load_object i ((_,lobj) as node) =
let open_object i ((_,lobj) as node) =
apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj
-let subst_object ((_,_,lobj) as node) =
+let subst_object ((_,lobj) as node) =
apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
let classify_object lobj =
diff --git a/library/libobject.mli b/library/libobject.mli
index 834a70c648..9c0abafde5 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -70,7 +70,7 @@ type 'a object_declaration = {
load_function : int -> object_name * 'a -> unit;
open_function : int -> object_name * 'a -> unit;
classify_function : 'a -> 'a substitutivity;
- subst_function : object_name * substitution * 'a -> 'a;
+ subst_function : substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
rebuild_function : 'a -> 'a }
@@ -86,7 +86,7 @@ type 'a object_declaration = {
val default_object : string -> 'a object_declaration
(* the identity substitution function *)
-val ident_subst_function : object_name * substitution * 'a -> 'a
+val ident_subst_function : substitution * 'a -> 'a
(*s Given an object declaration, the function [declare_object]
will hand back two functions, the "injection" and "projection"
@@ -102,7 +102,7 @@ val object_tag : obj -> string
val cache_object : object_name * obj -> unit
val load_object : int -> object_name * obj -> unit
val open_object : int -> object_name * obj -> unit
-val subst_object : object_name * substitution * obj -> obj
+val subst_object : substitution * obj -> obj
val classify_object : obj -> obj substitutivity
val discharge_object : object_name * obj -> obj option
val rebuild_object : obj -> obj
diff --git a/library/library.ml b/library/library.ml
index d129a24db5..fbe437fc44 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -302,7 +302,7 @@ let open_import i (_,(dir,export)) =
let cache_import obj =
open_import 1 obj
-let subst_import (_,_,o) = o
+let subst_import (_,o) = o
let classify_import (_,export as obj) =
if export then Substitute obj else Dispose
diff --git a/library/nametab.ml b/library/nametab.ml
index 31915c95a0..c14b6cfc0e 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -314,18 +314,26 @@ let the_tacticrevtab = ref (KNmap.empty : knrevtab)
Parameter but also Remark and Fact) *)
let push_xref visibility sp xref =
- the_ccitab := SpTab.push visibility sp xref !the_ccitab;
match visibility with
| Until _ ->
- if Globrevtab.mem xref !the_globrevtab then
- ()
- else
- the_globrevtab := Globrevtab.add xref sp !the_globrevtab
- | _ -> ()
+ the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+ the_globrevtab := Globrevtab.add xref sp !the_globrevtab
+ | _ ->
+ begin
+ if SpTab.exists sp !the_ccitab then
+ match SpTab.find sp !the_ccitab with
+ | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
+ TrueGlobal( ConstructRef _) as xref ->
+ the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+ | _ ->
+ the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+ else
+ the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+ end
let push_cci visibility sp ref =
push_xref visibility sp (TrueGlobal ref)
-
+
(* This is for Syntactic Definitions *)
let push_syndef visibility sp kn =
push_xref visibility sp (SynDef kn)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-30 13:49:34 +0000