aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-08-02 17:17:42 +0000
committerGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-08-02 17:17:42 +0000
commit12965209478bd99dfbe57f07d5b525e51b903f22 (patch)
tree36a7f5e4802cd321caf02fed0be8349100be09fb /library
parent8b26fd6ba739d4f49fae99ed764b086022e44b50 (diff)
Modules dans COQ\!\!\!\!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml179
-rw-r--r--library/declare.mli20
-rw-r--r--library/declaremods.ml630
-rw-r--r--library/declaremods.mli85
-rw-r--r--library/global.ml85
-rw-r--r--library/global.mli67
-rw-r--r--library/goptions.ml41
-rw-r--r--library/goptions.mli2
-rw-r--r--library/impargs.ml130
-rw-r--r--library/impargs.mli1
-rw-r--r--library/lib.ml447
-rw-r--r--library/lib.mli107
-rw-r--r--library/libnames.ml212
-rw-r--r--library/libnames.mli118
-rw-r--r--library/libobject.ml98
-rw-r--r--library/libobject.mli93
-rw-r--r--library/library.ml502
-rw-r--r--library/library.mli68
-rw-r--r--library/nameops.ml85
-rw-r--r--library/nameops.mli36
-rwxr-xr-xlibrary/nametab.ml409
-rwxr-xr-xlibrary/nametab.mli111
-rw-r--r--library/summary.ml22
-rw-r--r--library/summary.mli3
24 files changed, 2596 insertions, 955 deletions
diff --git a/library/declare.ml b/library/declare.ml
index fc80cfda9..31af6dbbb 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -11,10 +11,12 @@
open Pp
open Util
open Names
+open Libnames
open Nameops
open Term
open Sign
open Declarations
+open Entries
open Inductive
open Indtypes
open Reduction
@@ -91,7 +93,7 @@ let _ = Summary.declare_summary "VARIABLE"
Summary.init_function = (fun () -> vartab := Idmap.empty);
Summary.survive_section = false }
-let cache_variable (sp,(id,(p,d,strength))) =
+let cache_variable ((sp,_),(id,(p,d,strength))) =
(* Constr raisonne sur les noms courts *)
if Idmap.mem id !vartab then
errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
@@ -100,17 +102,13 @@ let cache_variable (sp,(id,(p,d,strength))) =
| SectionLocalDef (c,t) -> Global.push_named_def (id,c,t) in
let (_,bd,ty) = Global.lookup_named id in
let vd = (bd,ty,cst) in
- Nametab.push 0 (restrict_path 0 sp) (VarRef id);
+ Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
vartab := Idmap.add id (p,vd,strength) !vartab
let (in_variable, out_variable) =
- let od = {
+ declare_object { (default_object "VARIABLE") with
cache_function = cache_variable;
- load_function = (fun _ -> ());
- open_function = (fun _ -> ());
- export_function = (fun x -> Some x) }
- in
- declare_object ("VARIABLE", od)
+ classify_function = (fun _ -> Dispose) }
let declare_variable id obj =
let sp = add_leaf id (in_variable (id,obj)) in
@@ -119,7 +117,7 @@ let declare_variable id obj =
(* Globals: constants and parameters *)
-type constant_declaration = global_declaration * strength
+type constant_declaration = constant_entry * strength
let csttab = ref (Spmap.empty : strength Spmap.t)
@@ -129,90 +127,101 @@ let _ = Summary.declare_summary "CONSTANT"
Summary.init_function = (fun () -> csttab := Spmap.empty);
Summary.survive_section = false }
-let cache_constant (sp,(cdt,stre)) =
+let cache_constant ((sp,kn),(cdt,stre)) =
(if Idmap.mem (basename sp) !vartab then
errorlabstrm "cache_constant"
(pr_id (basename sp) ++ str " already exists"));
(if Nametab.exists_cci sp then
let (_,id) = repr_path sp in
errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
- Global.add_constant sp cdt;
+ let _,dir,_ = repr_kn kn in
+ let kn' = Global.add_constant dir (basename sp) cdt in
+ if kn' <> kn then
+ anomaly "Kernel and Library names do not match";
(match stre with
| DischargeAt (dp,n) when not (is_dirpath_prefix_of dp (Lib.cwd ())) ->
(* Only qualifications including the sections segment from the current
section to the discharge section is available for Remark & Fact *)
- Nametab.push (n-Lib.sections_depth()) sp (ConstRef sp)
+ Nametab.push (Nametab.Until ((*n-Lib.sections_depth()+*)1)) sp (ConstRef kn)
| (NeverDischarge| DischargeAt _) ->
(* All qualifications of Theorem, Lemma & Definition are visible *)
- Nametab.push 0 sp (ConstRef sp)
+ Nametab.push (Nametab.Until 1) sp (ConstRef kn)
| NotDeclare -> assert false);
csttab := Spmap.add sp stre !csttab
(* At load-time, the segment starting from the module name to the discharge *)
(* section (if Remark or Fact) is needed to access a construction *)
-let load_constant (sp,(ce,stre)) =
+let load_constant i ((sp,kn),(ce,stre)) =
(if Nametab.exists_cci sp then
let (_,id) = repr_path sp in
errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
csttab := Spmap.add sp stre !csttab;
- Nametab.push (depth_of_strength stre + 1) sp (ConstRef sp)
+ Nametab.push (Nametab.Until ((*depth_of_strength stre + *)i)) sp (ConstRef kn)
(* Opening means making the name without its module qualification available *)
-let open_constant (sp,(_,stre)) =
+let open_constant i ((sp,kn),(_,stre)) =
let n = depth_of_strength stre in
- Nametab.push n (restrict_path n sp) (ConstRef sp)
+ Nametab.push (Nametab.Exactly (i(*+n*))) sp (ConstRef kn)
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ParameterEntry mkProp
+let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
+
+let dummy_constant (ce,stre) = dummy_constant_entry,stre
-let export_constant (ce,stre) = Some (dummy_constant_entry,stre)
+let export_constant cst = Some (dummy_constant cst)
+
+let classify_constant (_,cst) = Substitute (dummy_constant cst)
let (in_constant, out_constant) =
- let od = {
+ declare_object { (default_object "CONSTANT") with
cache_function = cache_constant;
load_function = load_constant;
open_function = open_constant;
+ classify_function = classify_constant;
+ subst_function = ident_subst_function;
export_function = export_constant }
- in
- declare_object ("CONSTANT", od)
let hcons_constant_declaration = function
- | (ConstantEntry ce, stre) ->
- (ConstantEntry
+ | (DefinitionEntry ce, stre) ->
+ (DefinitionEntry
{ const_entry_body = hcons1_constr ce.const_entry_body;
const_entry_type = option_app hcons1_constr ce.const_entry_type;
const_entry_opaque = ce.const_entry_opaque }, stre)
| cd -> cd
-let declare_constant id cd =
+let declare_constant id (cd,stre) =
(* let cd = hcons_constant_declaration cd in *)
- let sp = add_leaf id (in_constant cd) in
- if is_implicit_args() then declare_constant_implicits sp;
- sp
+ let oname = add_leaf id (in_constant (ConstantEntry cd,stre)) in
+ if is_implicit_args() then declare_constant_implicits (snd oname);
+ oname
-let redeclare_constant sp (cd,stre) =
- add_absolutely_named_leaf sp (in_constant (GlobalRecipe cd,stre));
- if is_implicit_args() then declare_constant_implicits sp
+let redeclare_constant id (cd,stre) =
+ let _,kn = add_leaf id (in_constant (GlobalRecipe cd,stre)) in
+ if is_implicit_args() then declare_constant_implicits kn
(* Inductives. *)
-let inductive_names sp mie =
+let inductive_names sp kn mie =
let (dp,_) = repr_path sp in
let names, _ =
List.fold_left
(fun (names, n) ind ->
- let indsp = (sp,n) in
+ let ind_p = (kn,n) in
let names, _ =
List.fold_left
- (fun (names, p) id ->
- let sp = Names.make_path dp id in
- ((sp, ConstructRef (indsp,p)) :: names, p+1))
+ (fun (names, p) l ->
+ let sp =
+ Libnames.make_path dp l
+ in
+ ((sp, ConstructRef (ind_p,p)) :: names, p+1))
(names, 1) ind.mind_entry_consnames in
- let sp = Names.make_path dp ind.mind_entry_typename in
- ((sp, IndRef indsp) :: names, n+1))
+ let sp = Libnames.make_path dp ind.mind_entry_typename
+ in
+ ((sp, IndRef ind_p) :: names, n+1))
([], 0) mie.mind_entry_inds
in names
+
let check_exists_inductive (sp,_) =
(if Idmap.mem (basename sp) !vartab then
errorlabstrm "cache_inductive"
@@ -221,22 +230,27 @@ let check_exists_inductive (sp,_) =
let (_,id) = repr_path sp in
errorlabstrm "cache_inductive" (pr_id id ++ str " already exists")
-let cache_inductive (sp,mie) =
- let names = inductive_names sp mie in
+let cache_inductive ((sp,kn),mie) =
+ let names = inductive_names sp kn mie in
List.iter check_exists_inductive names;
- Global.add_mind sp mie;
+ let _,dir,_ = repr_kn kn in
+ let kn' = Global.add_mind dir (basename sp) mie in
+ if kn' <> kn then
+ anomaly "Kernel and Library names do not match";
+
List.iter
- (fun (sp, ref) -> Nametab.push 0 sp ref)
+ (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref)
names
-let load_inductive (sp,mie) =
- let names = inductive_names sp mie in
+let load_inductive i ((sp,kn),mie) =
+ let names = inductive_names sp kn mie in
List.iter check_exists_inductive names;
- List.iter (fun (sp, ref) -> Nametab.push 1 sp ref) names
+ List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names
-let open_inductive (sp,mie) =
- let names = inductive_names sp mie in
- List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names
+let open_inductive i ((sp,kn),mie) =
+ let names = inductive_names sp kn mie in
+(* List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names*)
+ List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
let dummy_one_inductive_entry mie = {
mind_entry_params = [];
@@ -254,28 +268,28 @@ let dummy_inductive_entry m = {
let export_inductive x = Some (dummy_inductive_entry x)
let (in_inductive, out_inductive) =
- let od = {
+ declare_object {(default_object "INDUCTIVE") with
cache_function = cache_inductive;
load_function = load_inductive;
open_function = open_inductive;
+ classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a));
+ subst_function = ident_subst_function;
export_function = export_inductive }
- in
- declare_object ("INDUCTIVE", od)
let declare_mind mie =
let id = match mie.mind_entry_inds with
| ind::_ -> ind.mind_entry_typename
| [] -> anomaly "cannot declare an empty list of inductives"
in
- let sp = add_leaf id (in_inductive mie) in
- if is_implicit_args() then declare_mib_implicits sp;
- sp
+ let oname = add_leaf id (in_inductive mie) in
+ if is_implicit_args() then declare_mib_implicits (snd oname);
+ oname
(*s Test and access functions. *)
let is_constant sp =
- try let _ = Global.lookup_constant sp in true with Not_found -> false
+ try let _ = Spmap.find sp !csttab in true with Not_found -> false
let constant_strength sp = Spmap.find sp !csttab
@@ -291,7 +305,7 @@ let variable_strength id =
let (_,_,str) = Idmap.find id !vartab in str
let find_section_variable id =
- let (p,_,_) = Idmap.find id !vartab in Names.make_path p id
+ let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id
(* Global references. *)
@@ -353,12 +367,14 @@ let construct_qualified_reference qid =
let ref = Nametab.locate qid in
constr_of_reference ref
-let construct_reference env id =
- try
- mkVar (let _ = Environ.lookup_named id env in id)
- with Not_found ->
- let ref = Nametab.sp_of_id id in
- constr_of_reference ref
+let construct_reference ctx_opt id =
+ match ctx_opt with
+ | None -> construct_qualified_reference (make_short_qualid id)
+ | Some ctx ->
+ try
+ mkVar (let _ = Sign.lookup_named id ctx in id)
+ with Not_found ->
+ construct_qualified_reference (make_short_qualid id)
let global_qualified_reference qid =
construct_qualified_reference qid
@@ -370,36 +386,42 @@ let global_reference_in_absolute_module dir id =
constr_of_reference (Nametab.locate_in_absolute_module dir id)
let global_reference id =
- construct_reference (Global.env()) id
-
-let dirpath sp = let (p,_) = repr_path sp in p
-
-let dirpath_of_global = function
- | VarRef id -> empty_dirpath
- | ConstRef sp -> dirpath sp
- | IndRef (sp,_) -> dirpath sp
- | ConstructRef ((sp,_),_) -> dirpath sp
+ construct_qualified_reference (make_short_qualid id)
let is_section_variable = function
| VarRef _ -> true
| _ -> false
+(* TODO temporary hack!!! *)
+let rec is_imported_modpath = function
+ | MPfile dp -> dp <> (Lib.module_dp ())
+(* | MPdot (mp,_) -> is_imported_modpath mp *)
+ | _ -> false
+
+let is_imported_ref = function
+ | VarRef _ -> false
+ | ConstRef kn
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_)
+(* | ModTypeRef ln *) ->
+ let (mp,_,_) = repr_kn kn in is_imported_modpath mp
+(* | ModRef mp ->
+ is_imported_modpath mp
+*)
let is_global id =
try
- let osp = Nametab.locate (make_short_qualid id) in
- (* Compatibilité V6.3: Les variables de section ne sont pas globales
- not (is_section_variable osp) && *)
- is_dirpath_prefix_of (dirpath_of_global osp) (Lib.cwd())
+ let ref = Nametab.locate (make_short_qualid id) in
+ not (is_imported_ref ref)
with Not_found ->
false
-let strength_of_global = function
- | ConstRef sp -> constant_strength sp
+let strength_of_global ref = match ref with
+ | ConstRef kn -> constant_strength (full_name ref)
| VarRef id -> variable_strength id
| IndRef _ | ConstructRef _ -> NeverDischarge
let library_part ref =
- let sp = Nametab.sp_of_global (Global.env ()) ref in
+ let sp = Nametab.sp_of_global None ref in
let dir,_ = repr_path sp in
match strength_of_global ref with
| DischargeAt (dp,n) ->
@@ -412,3 +434,4 @@ let library_part ref =
(* Theorem/Lemma outside its outer section of definition *)
dir
| NotDeclare -> assert false
+
diff --git a/library/declare.mli b/library/declare.mli
index 07b9d98b6..273a2b344 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -10,9 +10,11 @@
(*i*)
open Names
+open Libnames
open Term
open Sign
open Declarations
+open Entries
open Indtypes
open Safe_typing
open Library
@@ -34,16 +36,16 @@ type section_variable_entry =
type variable_declaration = dir_path * section_variable_entry * strength
-val declare_variable : variable -> variable_declaration -> section_path
+val declare_variable : variable -> variable_declaration -> object_name
-type constant_declaration = global_declaration * strength
+type constant_declaration = constant_entry * strength
(* [declare_constant id cd] declares a global declaration
(constant/parameter) with name [id] in the current section; it returns
the full path of the declaration *)
-val declare_constant : identifier -> constant_declaration -> constant
+val declare_constant : identifier -> constant_declaration -> object_name
-val redeclare_constant : constant -> Cooking.recipe * strength -> unit
+val redeclare_constant : identifier -> Cooking.recipe * strength -> unit
(*
val declare_parameter : identifier -> constr -> constant
@@ -52,7 +54,7 @@ val declare_parameter : identifier -> constr -> constant
(* [declare_mind me] declares a block of inductive types with
their constructors in the current section; it returns the path of
the whole block *)
-val declare_mind : mutual_inductive_entry -> mutual_inductive
+val declare_mind : mutual_inductive_entry -> object_name
val out_inductive : Libobject.obj -> mutual_inductive_entry
@@ -65,7 +67,7 @@ val strength_min : strength * strength -> strength
(*s Corresponding test and access functions. *)
val is_constant : section_path -> bool
-val constant_strength : constant -> strength
+val constant_strength : section_path -> strength
val out_variable : Libobject.obj -> identifier * variable_declaration
val get_variable : variable -> named_declaration * strength
@@ -86,11 +88,11 @@ val constr_of_reference : global_reference -> constr
raise [Not_found] if not a global *)
val reference_of_constr : constr -> global_reference
-val global_qualified_reference : Nametab.qualid -> constr
+val global_qualified_reference : qualid -> constr
val global_absolute_reference : section_path -> constr
val global_reference_in_absolute_module : dir_path -> identifier -> constr
-val construct_qualified_reference : Nametab.qualid -> constr
+val construct_qualified_reference : qualid -> constr
val construct_absolute_reference : section_path -> constr
(* This should eventually disappear *)
@@ -98,7 +100,7 @@ val construct_absolute_reference : section_path -> constr
the name [id] in the global environment. It looks also for variables in a
given environment instead of looking in the current global environment. *)
val global_reference : identifier -> constr
-val construct_reference : Environ.env -> identifier -> constr
+val construct_reference : Sign.named_context option -> identifier -> constr
val is_global : identifier -> bool
diff --git a/library/declaremods.ml b/library/declaremods.ml
new file mode 100644
index 000000000..76ed46619
--- /dev/null
+++ b/library/declaremods.ml
@@ -0,0 +1,630 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Pp
+open Util
+open Names
+open Declarations
+open Entries
+open Libnames
+open Libobject
+open Lib
+open Nametab
+
+(* modules and components *)
+
+
+(* This type is a functional closure of a substitutive
+ library_segment.
+
+ The first part is a partial substitution (which will be later
+ applied to the library_segment when completed).
+
+ The second one is a list of bound identifiers which is nonempty
+ only if the segment is owned by a fuctor
+
+ The third one is the "magic" ident of the current structure (which
+ should be substituted with the real name of the current module.
+
+ The fourth one is the segment itself which can contain references
+ to identifiers in the domain of the substitution or in other two
+ elements. These references are invalid in the current scope and
+ therefore must be substitued with valid names before use.
+
+*)
+
+type substitutive_objects =
+ substitution * mod_bound_id list * mod_self_id * lib_objects
+
+
+(* For each module, we store the following things:
+
+ substitutive_objects
+ when we will do Module M:=N, the objects of N will be loaded
+ with M as well (after substitution)
+
+ substituted objects -
+ roughly the objects above after the substitution - we need to
+ keep them to call open_object when the module is opened (imported)
+
+ keep objects -
+ The list of non-substitutive objects - as above, for each of
+ them we will call open_object when the module is opened
+
+ (Some) Invariants:
+ * If the module is a functor, the two latter lists are empty.
+
+ * Module objects in substitutive_objects part have empty substituted
+ objects and keep objects.
+
+ * Modules which where created with Module M:=mexpr (and not with
+ End Module) have the keep list empty.
+*)
+
+
+ (* substitutive_objects * substituted objects *)
+(*type module_objects = substitutive_objects * library_objects*)
+
+let modtab_substobjs =
+ ref (MPmap.empty : substitutive_objects MPmap.t)
+let modtab_objects =
+ ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)
+(*let modtab_keep =
+ ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)*)
+
+(* currently begun interactive module (if any) - its arguments (if it
+ is a functor) and declared output type *)
+let openmod_info =
+ ref (([],None) : mod_bound_id list * module_type_entry option)
+
+let _ = Summary.declare_summary "MODULE-INFO"
+ { Summary.freeze_function = (fun () ->
+ !modtab_substobjs,
+ !modtab_objects,
+ !openmod_info);
+ Summary.unfreeze_function = (fun (sobjs,objs,info) ->
+ modtab_substobjs := sobjs;
+ modtab_objects := objs;
+ openmod_info := info);
+ Summary.init_function = (fun () ->
+ modtab_substobjs := MPmap.empty;
+ modtab_objects := MPmap.empty;
+ openmod_info := ([],None));
+ Summary.survive_section = false }
+
+(* auxiliary functions to transform section_path and kernel_name given
+ by Lib into module_path and dir_path needed for modules *)
+
+let mp_of_kn kn =
+ let mp,sec,l = repr_kn kn in
+ if sec=empty_dirpath then
+ MPdot (mp,l)
+ else
+ anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
+
+let dir_of_sp sp =
+ let dir,id = repr_path sp in
+ extend_dirpath 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)
+
+(* This function registers the visibility of the module and iterates
+ through its components. It is called by plenty module functions *)
+
+let do_module exists what iter_objects i dir mp substobjs objects =
+ let prefix = (dir,(mp,empty_dirpath)) in
+ let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
+ let vis =
+ if exists then
+ if
+ try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo
+ with Not_found -> false
+ then
+ Nametab.Exactly i
+ else
+ errorlabstrm (what^"_module")
+ (pr_dirpath dir ++ str " should already exist!")
+ else
+ if Nametab.exists_dir dir then
+ errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
+ else
+ Nametab.Until i
+ in
+ Nametab.push_dir vis dir dirinfo;
+ modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
+ match objects with
+ Some seg ->
+ modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects;
+ iter_objects (i+1) prefix seg
+ | None -> ()
+
+
+let conv_names_do_module exists what iter_objects i (sp,kn) substobjs substituted =
+ let dir,mp = dir_of_sp sp, mp_of_kn kn in
+ do_module exists what iter_objects i dir mp substobjs substituted
+
+(* 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 ->
+ let mp = Global.add_module (basename sp) me in
+ if mp <> mp_of_kn kn then
+ anomaly "Kernel and Library names do not match"
+ 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 -> ()
+ | Some _ ->
+ anomaly ("We should never have full info in " ^ s^"!")
+
+
+(* 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)) =
+ (* TODO: This check is not essential *)
+ check_empty "load_module" entry;
+ conv_names_do_module false "load" load_objects i oname substobjs substituted
+
+
+let open_module i (oname,(entry,substobjs,substituted)) =
+ (* TODO: This check is not essential *)
+ check_empty "open_module" entry;
+ conv_names_do_module true "open" open_objects i oname substobjs substituted
+
+
+let 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 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)
+
+let (in_module,out_module) =
+ declare_object {(default_object "MODULE") with
+ cache_function = cache_module;
+ load_function = load_module;
+ open_function = open_module;
+ subst_function = subst_module;
+ classify_function = classify_module;
+ 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) =
+ let mp = mp_of_kn kn in
+ let prefix = dir_of_sp sp, (mp,empty_dirpath) in
+ begin
+ try
+ let prefix',objects = MPmap.find mp !modtab_objects in
+ if prefix' <> prefix then
+ anomaly "Two different modules with the same path!";
+ modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects;
+ with
+ Not_found -> anomaly "Keep objects before substitutive"
+ end;
+ load_objects i prefix seg
+
+let open_keep i ((sp,kn),seg) =
+ let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
+ open_objects i (dirpath,(mp,empty_dirpath)) seg
+
+let (in_modkeep,out_modkeep) =
+ declare_object {(default_object "MODULE KEEP OBJECTS") with
+ cache_function = cache_keep;
+ load_function = load_keep;
+ open_function = open_keep;
+ export_function = (fun _ -> anomaly "No modules in sections!") }
+
+(* we remember objects for a module type. In case of a declaration:
+ Module M:SIG:=...
+ The module M gets its objects from SIG
+*)
+let modtypetab =
+ ref (KNmap.empty : substitutive_objects KNmap.t)
+
+(* currently started interactive module type. We remember its arguments
+ if it is a functor type *)
+let openmodtype_info =
+ ref ([] : mod_bound_id list)
+
+let _ = Summary.declare_summary "MODTYPE-INFO"
+ { Summary.freeze_function = (fun () ->
+ !modtypetab,!openmodtype_info);
+ Summary.unfreeze_function = (fun ft ->
+ modtypetab := fst ft;
+ openmodtype_info := snd ft);
+ Summary.init_function = (fun () ->
+ modtypetab := KNmap.empty;
+ openmodtype_info := []);
+ 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
+ anomaly "Kernel and Library names do not match"
+ in
+
+ if Nametab.exists_modtype sp then
+ errorlabstrm "cache_modtype"
+ (pr_sp sp ++ str " already exists") ;
+
+ Nametab.push_modtype (Nametab.Until 1) sp kn;
+
+ modtypetab := KNmap.add kn modtypeobjs !modtypetab
+
+
+let load_modtype i ((sp,kn),(entry,modtypeobjs)) =
+ check_empty "load_modtype" entry;
+
+ if Nametab.exists_modtype sp then
+ errorlabstrm "cache_modtype"
+ (pr_sp sp ++ str " already exists") ;
+
+ Nametab.push_modtype (Nametab.Until i) sp kn;
+
+ modtypetab := KNmap.add 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
+ with Not_found -> true
+ then
+ errorlabstrm ("open_modtype")
+ (pr_sp sp ++ str " should already exist!");
+
+ Nametab.push_modtype (Nametab.Exactly i) sp kn
+
+
+let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) =
+ check_empty "subst_modtype" entry;
+ (entry,(join subs subst,mbids,msid,objs))
+
+
+let classify_modtype (_,(_,substobjs)) =
+ Substitute (None,substobjs)
+
+
+let (in_modtype,out_modtype) =
+ declare_object {(default_object "MODULE TYPE") with
+ cache_function = cache_modtype;
+ load_function = load_modtype;
+ subst_function = subst_modtype;
+ classify_function = classify_modtype;
+ export_function = in_some }
+
+
+
+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
+ (subst, mbid::mbids, msid, objs)
+ | MTEsig (msid,_) -> (empty_subst, [], msid, [])
+ (* this is plainly wrong, but it is hard to do otherwise... *)
+
+(* 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 substituted = subst_substobjs dir mp substobjs in
+ do_module false "begin" load_objects 1 dir mp substobjs substituted
+ in
+ List.iter2 process_arg argids args
+
+(*
+(* this function removes keep objects from submodules *)
+let rec kill_keep objs =
+ let kill = function
+ | (oname,Leaf obj) as node ->
+ if object_tag obj = "MODULE" then
+ let (entry,substobjs,substitute) = out_module obj in
+ match substitute,keep with
+ | [],[] -> node
+ | _ -> oname, Leaf (in_module (entry,(substobjs,[],[])))
+ else
+ node
+ | _ -> anomaly "kill_keep expects Leafs only!"
+ in
+ match objs with
+ | [] -> objs
+ | h::tl -> let h'=kill h and tl'=kill_keep tl in
+ if h==h' && tl==tl' then
+ objs
+ else
+ h'::tl'
+*)
+
+let start_module id argids args res_o =
+ let mp = Global.start_module (Lib.module_dp()) id args res_o in
+ let mbids = List.map fst args in
+ let fs = Summary.freeze_summaries () in
+ process_module_bindings argids args;
+ openmod_info:=(mbids,res_o);
+ Lib.start_module id mp fs;
+ Lib.add_frozen_state ()
+
+
+let end_module id =
+
+ let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
+ let mp = Global.end_module id in
+ let substitute, keep, special = Lib.classify_objects lib_stack in
+
+ let dir = fst oldprefix in
+ let msid = msid_of_prefix oldprefix in
+ let mbids, res_o = !openmod_info in
+
+ Summary.unfreeze_other_summaries fs;
+
+ let substobjs = match res_o with
+ | None ->
+ empty_subst, mbids, msid, substitute
+ | Some (MTEident ln) ->
+ abstract_substobjs mbids (KNmap.find ln (!modtypetab))
+ | Some (MTEsig (msid,_)) ->
+ todo "Anonymous signatures not supported";
+ empty_subst, mbids, msid, []
+ | Some (MTEfunsig _) ->
+ anomaly "Funsig cannot be here..."
+ in
+ let substituted = subst_substobjs dir mp substobjs in
+ let node = in_module (None,substobjs,substituted) in
+ let objects =
+ if keep = [] then
+ special@[node]
+ else
+ special@[node;in_modkeep keep]
+ in
+ let newoname = Lib.add_leaves id objects in
+
+ if (fst newoname) <> (fst oldoname) then
+ anomaly "Names generated on start_ and end_module do not match";
+ if mp_of_kn (snd newoname) <> mp then
+ anomaly "Kernel and Library names do not match";
+
+ Lib.add_frozen_state () (* to prevent recaching *)
+
+
+
+let module_objects mp =
+ let prefix,objects = MPmap.find mp !modtab_objects in
+ segment_of_objects prefix objects
+
+
+type library_name = dir_path
+
+(* The first two will form a substitutive_objects, the last one is keep *)
+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 prefix = dir, (mp, empty_dirpath) 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
+ 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 substituted = subst_substobjs dir mp substobjs in
+ let objects = option_app (fun seg -> seg@keep) substituted in
+ let modobjs = substobjs, objects in
+ Hashtbl.add library_cache dir modobjs;
+ modobjs
+ in
+ do_module false "register_compilation" load_objects 1 dir mp substobjs objects
+
+
+let start_library dir =
+ let mp = Global.start_library dir in
+ openmod_info:=[],None;
+ Lib.start_compilation dir mp;
+ Lib.add_frozen_state ()
+
+
+let export_library dir =
+ let cenv = Global.export dir in
+ let prefix, lib_stack = Lib.end_compilation dir in
+ let msid = msid_of_prefix prefix in
+ let substitute, keep, _ = Lib.classify_objects lib_stack in
+ cenv,(msid,substitute,keep)
+
+
+
+let import_module mp =
+ let prefix,objects = MPmap.find mp !modtab_objects in
+ open_objects 1 prefix objects
+
+
+let start_modtype id argids args =
+ let mp = Global.start_modtype (Lib.module_dp()) id args in
+ let fs= Summary.freeze_summaries () in
+ process_module_bindings argids args;
+ openmodtype_info := (List.map fst args);
+ Lib.start_modtype id mp fs;
+ Lib.add_frozen_state ()
+
+
+let end_modtype id =
+
+ let oldoname,prefix,fs,lib_stack = Lib.end_modtype id in
+ let ln = Global.end_modtype id in
+ let substitute, _, special = Lib.classify_objects lib_stack in
+
+ let msid = msid_of_prefix prefix in
+ let mbids = !openmodtype_info in
+
+ Summary.unfreeze_other_summaries fs;
+
+ let modtypeobjs = empty_subst, mbids, msid, 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 snd oname <> ln then
+ anomaly
+ "Kernel and Library names do not match";
+
+ Lib.add_frozen_state ()(* to prevent recaching *)
+
+
+let declare_modtype id mte =
+ let substobjs = get_modtype_substobjs mte in
+ ignore (add_leaf id (in_modtype (Some mte, substobjs)))
+
+
+
+let rec get_module_substobjs = function
+ MEident mp -> MPmap.find mp !modtab_substobjs
+ | MEfunctor (mbid,_,mexpr) ->
+ let (subst, mbids, msid, objs) = get_module_substobjs mexpr in
+ (subst, mbid::mbids, msid, objs)
+ | MEstruct (msid,_) ->
+ (empty_subst, [], msid, [])
+ | MEapply (mexpr, MEident mp) ->
+ let (subst, mbids, msid, objs) = get_module_substobjs mexpr in
+ (match mbids with
+ | mbid::mbids ->
+ (add_mbid mbid mp subst, mbids, msid, objs)
+ | [] -> anomaly "Too few arguments in functor")
+ | MEapply (_,_) ->
+ anomaly "The argument of a module application must be a path!"
+
+
+let declare_module id me =
+ let substobjs =
+ match me with
+ | {mod_entry_type = Some mte} -> get_modtype_substobjs mte
+ | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr
+ | _ -> anomaly "declare_module: No type, no body ..."
+ in
+ 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 me, substobjs, substituted)))
+
+
+(*s Iterators. *)
+
+let fold_all_segments insec f x =
+ let acc' =
+ MPmap.fold
+ (fun _ (prefix,objects) acc ->
+ let apply_obj acc (id,obj) = f acc (make_oname prefix id) obj in
+ List.fold_left apply_obj acc objects)
+ !modtab_objects x
+ in
+ let rec apply_node acc = function
+ | sp, Leaf o -> f acc sp o
+ | _, ClosedSection (_,_,seg) ->
+ if insec then List.fold_left apply_node acc seg else acc
+ | _ -> acc
+ in
+ List.fold_left apply_node acc' (Lib.contents_after None)
+
+let iter_all_segments insec f =
+ let _ =
+ MPmap.iter
+ (fun _ (prefix,objects) ->
+ let apply_obj (id,obj) = f (make_oname prefix id) obj in
+ List.iter apply_obj objects)
+ !modtab_objects
+ in
+ let rec apply_node = function
+ | sp, Leaf o -> f sp o
+ | _, ClosedSection (_,_,seg) -> if insec then List.iter apply_node seg
+ | _ -> ()
+ in
+ List.iter apply_node (Lib.contents_after None)
+
+
+
+let debug_print_modtab _ =
+ let pr_seg = function
+ | [] -> str "[]"
+ | l -> str ("[." ^ string_of_int (List.length l) ^ ".]")
+ in
+ let pr_modinfo mp (prefix,objects) s =
+ s ++ str (string_of_mp mp) ++ (spc ())
+ ++ (pr_seg (segment_of_objects prefix objects))
+ in
+ let modules = MPmap.fold pr_modinfo !modtab_objects (mt ()) in
+ hov 0 modules
+
+
diff --git a/library/declaremods.mli b/library/declaremods.mli
new file mode 100644
index 000000000..17db827e8
--- /dev/null
+++ b/library/declaremods.mli
@@ -0,0 +1,85 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Entries
+open Libnames
+open Libobject
+open Lib
+(*i*)
+
+(*s This modules provides official fucntions to declare modules and
+ module types *)
+
+
+(*s Modules *)
+
+val declare_module : identifier -> module_entry -> unit
+
+val start_module :
+ identifier -> identifier list -> (mod_bound_id * module_type_entry) list
+ -> module_type_entry option -> unit
+val end_module : identifier -> unit
+
+
+
+(*s Module types *)
+
+val declare_modtype : identifier -> module_type_entry -> unit
+
+val start_modtype :
+ identifier -> identifier list -> (mod_bound_id * module_type_entry) list
+ -> unit
+val end_modtype : identifier -> unit
+
+
+(*s Objects of a module. They come in two lists: the substitutive ones
+ and the other *)
+
+val module_objects : module_path -> library_segment
+
+
+(*s Libraries i.e. modules on disk *)
+
+type library_name = dir_path
+
+type library_objects
+
+val register_library :
+ library_name ->
+ Safe_typing.compiled_library -> library_objects -> Digest.t -> unit
+
+val start_library : library_name -> unit
+
+val export_library :
+ library_name -> Safe_typing.compiled_library * library_objects
+
+
+(* [import_module mp] opens the module [mp] (in a Caml sense).
+ It modifies Nametab and performs the "open_object" function
+ for every object of the module. *)
+
+val import_module : module_path -> unit
+
+
+(*s [fold_all_segments] and [iter_all_segments] iterate over all
+ segments, the modules' segments first and then the current
+ segment. Modules are presented in an arbitrary order. The given
+ function is applied to all leaves (together with their section
+ path). The boolean indicates if we must enter closed sections. *)
+
+val fold_all_segments : bool -> ('a -> object_name -> obj -> 'a) -> 'a -> 'a
+val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit
+
+
+val debug_print_modtab : unit -> Pp.std_ppcmds
+
+(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*)
diff --git a/library/global.ml b/library/global.ml
index db0e5f470..cdebc52f5 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -26,7 +26,7 @@ let safe_env () = !global_env
let env () = env_of_safe_env !global_env
let _ =
- declare_summary "Global environment"
+ declare_global_environment
{ freeze_function = (fun () -> !global_env);
unfreeze_function = (fun fr -> global_env := fr);
init_function = (fun () -> global_env := empty_environment);
@@ -46,17 +46,81 @@ let push_named_def d =
global_env := env;
cst
-let add_constant sp ce = global_env := add_constant sp ce !global_env
-let add_mind sp mie = global_env := add_mind sp mie !global_env
+(*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
+ global_env := newenv;
+ kn
+
+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_constraints c = global_env := add_constraints c !global_env
+
+
+let start_module dir id params mtyo =
+ let l = label_of_id id in
+ let mp,newenv = start_module dir l params mtyo !global_env in
+ global_env := newenv;
+ mp
+
+let end_module id =
+ let l = label_of_id id in
+ let mp,newenv = end_module l !global_env in
+ global_env := newenv;
+ mp
+
+
+let start_modtype dir id params =
+ let l = label_of_id id in
+ let mp,newenv = start_modtype dir l params !global_env in
+ global_env := newenv;
+ mp
+
+let end_modtype id =
+ let l = label_of_id id in
+ let kn,newenv = end_modtype l !global_env in
+ global_env := newenv;
+ kn
+
+
+
+
let lookup_named id = lookup_named id (env())
-let lookup_constant sp = lookup_constant sp (env())
+let lookup_constant kn = lookup_constant kn (env())
let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind
-let lookup_mind sp = lookup_mind sp (env())
+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 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 import cenv digest =
+ let mp,newenv = import cenv digest !global_env in
+ global_env := newenv;
+ mp
+
-let export s = export !global_env s
-let import cenv = global_env := import cenv !global_env
(*s Function to get an environment from the constants part of the global
environment and a given context. *)
@@ -64,7 +128,7 @@ let import cenv = global_env := import cenv !global_env
let env_of_context hyps =
reset_with_named_context hyps (env())
-open Nametab
+open Libnames
let type_of_reference env = function
| VarRef id -> let (_,_,t) = Environ.lookup_named id env in t
@@ -73,3 +137,8 @@ let type_of_reference env = function
| ConstructRef cstr -> Inductive.type_of_constructor env cstr
let type_of_global t = type_of_reference (env ()) t
+
+
+(*let get_kn dp l =
+ make_kn (current_modpath !global_env) dp l
+*)
diff --git a/library/global.mli b/library/global.mli
index 48e90d12e..4a215167a 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -13,13 +13,18 @@ open Names
open Univ
open Term
open Declarations
+open Entries
open Indtypes
open Safe_typing
-(*i*)
+ (*i*)
+
+(* This module defines the global environment of Coq. The functions
+ below are exactly the same as the ones in [Safe_typing], operating on
+ that global environment. [add_*] functions perform name verification,
+ i.e. check that the name given as argument match those provided by
+ [Safe_typing]. *)
+
-(* This module defines the global environment of Coq.
- The functions below are exactly the same as the ones in [Typing],
- operating on that global environment. *)
val safe_env : unit -> safe_environment
val env : unit -> Environ.env
@@ -27,26 +32,62 @@ val env : unit -> Environ.env
val universes : unit -> universes
val named_context : unit -> Sign.named_context
-(* Extending env with variables, constants and inductives *)
+(*s Extending env with variables and local definitions *)
val push_named_assum : (identifier * types) -> Univ.constraints
val push_named_def : (identifier * constr * types option) -> Univ.constraints
-val add_constant : constant -> global_declaration -> unit
-val add_mind : mutual_inductive -> mutual_inductive_entry -> unit
+(*s Adding constants, inductives, modules and module types. All these
+ functions verify that given names match those generated by kernel *)
+
+val add_constant :
+ dir_path -> identifier -> global_declaration -> kernel_name
+val add_mind :
+ dir_path -> identifier -> mutual_inductive_entry -> kernel_name
+
+val add_module : identifier -> module_entry -> module_path
+val add_modtype : identifier -> module_type_entry -> kernel_name
+
val add_constraints : constraints -> unit
+(*s Interactive modules and module types *)
+(* Both [start_*] functions take the [dir_path] argument to create a
+ [mod_self_id]. This should be the name of the compilation unit. *)
+
+(* [start_*] functions return the [module_path] valid for components
+ of the started module / module type *)
+
+val start_module :
+ dir_path -> identifier -> (mod_bound_id * module_type_entry) list
+ -> module_type_entry option
+ -> module_path
+
+val end_module :
+ identifier -> module_path
+
+val start_modtype :
+ dir_path -> identifier -> (mod_bound_id * module_type_entry) list
+ -> module_path
+
+val end_modtype :
+ identifier -> kernel_name
+
+
(* Queries *)
val lookup_named : variable -> named_declaration
val lookup_constant : constant -> constant_body
val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
val lookup_mind : mutual_inductive -> mutual_inductive_body
+val lookup_module : module_path -> module_body
+val lookup_modtype : kernel_name -> module_type_body
-(* Modules *)
-val export : dir_path -> Environ.compiled_env
-val import : Environ.compiled_env -> unit
+(* Compiled modules *)
+val start_library : dir_path -> module_path
+val export : dir_path -> compiled_library
+val import : compiled_library -> Digest.t -> module_path
(*s Function to get an environment from the constants part of the global
- environment and a given context. *)
-
-val type_of_global : Nametab.global_reference -> types
+ * environment and a given context. *)
+
+val type_of_global : Libnames.global_reference -> types
val env_of_context : Sign.named_context -> Environ.env
+
diff --git a/library/goptions.ml b/library/goptions.ml
index b4056472b..4d505b5aa 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -14,6 +14,7 @@ open Pp
open Util
open Libobject
open Names
+open Libnames
open Term
open Nametab
@@ -55,6 +56,7 @@ module MakeTable =
type key
val table : (string * key table_of_A) list ref
val encode : key -> t
+ val subst : substitution -> t -> t
val printer : t -> std_ppcmds
val key : option_name
val title : string
@@ -66,10 +68,10 @@ module MakeTable =
| GOadd
| GOrmv
- let kn = nickname A.key
+ let nick = nickname A.key
let _ =
- if List.mem_assoc kn !A.table then
+ if List.mem_assoc nick !A.table then
error "Sorry, this table name is already used"
module MyType = struct type t = A.t let compare = Pervasives.compare end
@@ -82,7 +84,7 @@ module MakeTable =
let freeze () = !t in
let unfreeze c = t := c in
let init () = t := MySet.empty in
- Summary.declare_summary kn
+ Summary.declare_summary nick
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init;
@@ -90,17 +92,25 @@ module MakeTable =
let (add_option,remove_option) =
if A.synchronous then
- let load_options _ = () in
let cache_options (_,(f,p)) = match f with
| GOadd -> t := MySet.add p !t
| GOrmv -> t := MySet.remove p !t in
- let export_options fp = Some fp in
+ let load_options i o = if i=1 then cache_options o in
+ let subst_options (_,subst,(f,p as obj)) =
+ let p' = A.subst subst p in
+ if p' == p then obj else
+ (f,p')
+ in
+ let export_options fp = Some fp in
let (inGo,outGo) =
- Libobject.declare_object (kn,
- { Libobject.load_function = load_options;
- Libobject.open_function = cache_options;
+ Libobject.declare_object {(Libobject.default_object nick) with
+ Libobject.load_function = load_options;
+ Libobject.open_function = load_options;
Libobject.cache_function = cache_options;
- Libobject.export_function = export_options}) in
+ Libobject.subst_function = subst_options;
+ Libobject.classify_function = (fun (_,x) -> Substitute x);
+ Libobject.export_function = export_options}
+ in
((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
(fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
else
@@ -126,7 +136,7 @@ module MakeTable =
method print = print_table A.title A.printer !t
end
- let _ = A.table := (kn,new table_of_A ())::!A.table
+ let _ = A.table := (nick,new table_of_A ())::!A.table
let active c = MySet.mem c !t
let elements () = MySet.elements !t
end
@@ -149,6 +159,7 @@ struct
type key = string
let table = string_table
let encode x = x
+ let subst _ x = x
let printer = str
let key = A.key
let title = A.title
@@ -167,6 +178,7 @@ module type RefConvertArg =
sig
type t
val encode : qualid located -> t
+ val subst : substitution -> t -> t
val printer : t -> std_ppcmds
val key : option_name
val title : string
@@ -180,6 +192,7 @@ struct
type key = qualid located
let table = ref_table
let encode = A.encode
+ let subst = A.subst
let printer = A.printer
let key = A.key
let title = A.title
@@ -228,11 +241,9 @@ let declare_option cast uncast
check_key key;
let write = if sync then
let (decl_obj,_) =
- declare_object ((nickname key),
- {load_function = (fun _ -> ());
- open_function = (fun _ -> ());
+ declare_object {(default_object (nickname key)) with
cache_function = (fun (_,v) -> write v);
- export_function = (fun x -> None)})
+ classify_function = (fun _ -> Dispose)}
in
let _ = declare_summary (nickname key)
{freeze_function = read;
@@ -298,7 +309,7 @@ let msg_option_value (name,v) =
| IntValue (Some n) -> int n
| IntValue None -> str "undefined"
| StringValue s -> str s
- | IdentValue r -> pr_global_env (Global.env()) r
+ | IdentValue r -> pr_global_env None r
let print_option_value key =
let (name,(_,read,_)) = get_option key in
diff --git a/library/goptions.mli b/library/goptions.mli
index d43a4283e..28da69ea6 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -56,6 +56,7 @@
open Pp
open Util
open Names
+open Libnames
open Term
open Nametab
(*i*)
@@ -107,6 +108,7 @@ module MakeRefTable :
(A : sig
type t
val encode : qualid located -> t
+ val subst : substitution -> t -> t
val printer : t -> std_ppcmds
val key : option_name
val title : string
diff --git a/library/impargs.ml b/library/impargs.ml
index af6bfd6b7..14a93123b 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -10,6 +10,7 @@
open Util
open Names
+open Libnames
open Term
open Reduction
open Declarations
@@ -92,31 +93,35 @@ let list_of_implicits = function
(*s Constants. *)
-let constants_table = ref Spmap.empty
+let constants_table = ref KNmap.empty
-let compute_constant_implicits sp =
+let compute_constant_implicits kn =
let env = Global.env () in
- let cb = lookup_constant sp env in
+ let cb = lookup_constant kn env in
auto_implicits env (body_of_type cb.const_type)
-let cache_constant_implicits (_,(sp,imps)) =
- constants_table := Spmap.add sp imps !constants_table
+let cache_constant_implicits (_,(kn,imps)) =
+ constants_table := KNmap.add kn imps !constants_table
+
+let subst_constant_implicits (_,subst,(kn,imps as obj)) =
+ let kn' = subst_kn subst kn in
+ if kn' == kn then obj else
+ kn',imps
let (in_constant_implicits, _) =
- let od = {
+ declare_object {(default_object "CONSTANT-IMPLICITS") with
cache_function = cache_constant_implicits;
- load_function = cache_constant_implicits;
- open_function = (fun _ -> ());
+ load_function = (fun _ -> cache_constant_implicits);
+ subst_function = subst_constant_implicits;
+ classify_function = (fun (_,x) -> Substitute x);
export_function = (fun x -> Some x) }
- in
- declare_object ("CONSTANT-IMPLICITS", od)
-let declare_constant_implicits sp =
- let imps = compute_constant_implicits sp in
- add_anonymous_leaf (in_constant_implicits (sp,imps))
+let declare_constant_implicits kn =
+ let imps = compute_constant_implicits kn in
+ add_anonymous_leaf (in_constant_implicits (kn,imps))
let constant_implicits sp =
- try Spmap.find sp !constants_table with Not_found -> No_impl
+ try KNmap.find sp !constants_table with Not_found -> No_impl
let constant_implicits_list sp =
list_of_implicits (constant_implicits sp)
@@ -151,30 +156,40 @@ let constructors_table = ref Constrmap.empty
let cache_inductive_implicits (_,(indp,imps)) =
inductives_table := Indmap.add indp imps !inductives_table
+let subst_inductive_implicits (_,subst,((kn,i),imps as obj)) =
+ let kn' = subst_kn subst kn in
+ if kn' == kn then obj else
+ (kn',i),imps
+
let (in_inductive_implicits, _) =
- let od = {
+ declare_object {(default_object "INDUCTIVE-IMPLICITS") with
cache_function = cache_inductive_implicits;
- load_function = cache_inductive_implicits;
- open_function = (fun _ -> ());
- export_function = (fun x -> Some x) }
- in
- declare_object ("INDUCTIVE-IMPLICITS", od)
+ load_function = (fun _ -> cache_inductive_implicits);
+ subst_function = subst_inductive_implicits;
+ classify_function = (fun (_,x) -> Substitute x);
+ export_function = (fun x -> Some x) }
let cache_constructor_implicits (_,(consp,imps)) =
constructors_table := Constrmap.add consp imps !constructors_table
+let subst_constructor_implicits (_,subst,(((kn,i),j),imps as obj)) =
+ let kn' = subst_kn subst kn in
+ if kn' == kn then obj else
+ ((kn',i),j),imps
+
+
let (in_constructor_implicits, _) =
- let od = {
+ declare_object {(default_object "CONSTRUCTOR-IMPLICITS") with
cache_function = cache_constructor_implicits;
- load_function = cache_constructor_implicits;
- open_function = (fun _ -> ());
- export_function = (fun x -> Some x) }
- in
- declare_object ("CONSTRUCTOR-IMPLICITS", od)
+ load_function = (fun _ -> cache_constructor_implicits);
+ subst_function = subst_constructor_implicits;
+ classify_function = (fun (_,x) -> Substitute x);
+ export_function = (fun x -> Some x) }
-let compute_mib_implicits sp =
+
+let compute_mib_implicits kn =
let env = Global.env () in
- let mib = lookup_mind sp env in
+ let mib = lookup_mind kn env in
let ar =
Array.to_list
(Array.map (* No need to lift, arities contain no de Bruijn *)
@@ -188,10 +203,10 @@ let compute_mib_implicits sp =
in
Array.map imps_one_inductive mib.mind_packets
-let cache_mib_implicits (_,(sp,mibimps)) =
+let cache_mib_implicits (_,(kn,mibimps)) =
Array.iteri
(fun i (imps,v) ->
- let indp = (sp,i) in
+ let indp = (kn,i) in
inductives_table := Indmap.add indp imps !inductives_table;
Array.iteri
(fun j imps ->
@@ -199,18 +214,22 @@ let cache_mib_implicits (_,(sp,mibimps)) =
Constrmap.add (indp,succ j) imps !constructors_table) v)
mibimps
+let subst_mib_implicits (_,subst,(kn,mibimps as obj)) =
+ let kn' = subst_kn subst kn in
+ if kn' == kn then obj else
+ kn',mibimps
+
let (in_mib_implicits, _) =
- let od = {
+ declare_object {(default_object "MIB-IMPLICITS") with
cache_function = cache_mib_implicits;
- load_function = cache_mib_implicits;
- open_function = (fun _ -> ());
- export_function = (fun x -> Some x) }
- in
- declare_object ("MIB-IMPLICITS", od)
+ load_function = (fun _ -> cache_mib_implicits);
+ subst_function = subst_mib_implicits;
+ classify_function = (fun (_,x) -> Substitute x);
+ export_function = (fun x -> Some x) }
-let declare_mib_implicits sp =
- let imps = compute_mib_implicits sp in
- add_anonymous_leaf (in_mib_implicits (sp,imps))
+let declare_mib_implicits kn =
+ let imps = compute_mib_implicits kn in
+ add_anonymous_leaf (in_mib_implicits (kn,imps))
let inductive_implicits indp =
try Indmap.find indp !inductives_table with Not_found -> No_impl
@@ -237,13 +256,12 @@ let cache_var_implicits (_,(id,imps)) =
var_table := Idmap.add id imps !var_table
let (in_var_implicits, _) =
- let od = {
+ declare_object {(default_object "VARIABLE-IMPLICITS") with
cache_function = cache_var_implicits;
- load_function = cache_var_implicits;
- open_function = (fun _ -> ());
- export_function = (fun x -> Some x) }
- in
- declare_object ("VARIABLE-IMPLICITS", od)
+ load_function = (fun _ -> cache_var_implicits);
+ export_function = (fun x -> Some x) }
+
+
let declare_var_implicits id =
let imps = compute_var_implicits id in
@@ -255,16 +273,16 @@ let implicits_of_var id =
(*s Implicits of a global reference. *)
let declare_implicits = function
- | VarRef sp ->
- declare_var_implicits sp
- | ConstRef sp ->
- declare_constant_implicits sp
- | IndRef ((sp,i) as indp) ->
- let mib_imps = compute_mib_implicits sp in
+ | VarRef id ->
+ declare_var_implicits id
+ | ConstRef kn ->
+ declare_constant_implicits kn
+ | IndRef ((kn,i) as indp) ->
+ let mib_imps = compute_mib_implicits kn in
let imps = fst mib_imps.(i) in
add_anonymous_leaf (in_inductive_implicits (indp, imps))
- | ConstructRef (((sp,i),j) as consp) ->
- let mib_imps = compute_mib_implicits sp in
+ | ConstructRef (((kn,i),j) as consp) ->
+ let mib_imps = compute_mib_implicits kn in
let imps = (snd mib_imps.(i)).(j-1) in
add_anonymous_leaf (in_constructor_implicits (consp, imps))
@@ -296,7 +314,7 @@ let declare_manual_implicits r l =
(*s Tests if declared implicit *)
let is_implicit_constant sp =
- try let _ = Spmap.find sp !constants_table in true with Not_found -> false
+ try let _ = KNmap.find sp !constants_table in true with Not_found -> false
let is_implicit_inductive_definition indp =
try let _ = Indmap.find indp !inductives_table in true
@@ -313,13 +331,13 @@ let implicits_of_global = function
(*s Registration as global tables and rollback. *)
-type frozen_t = implicits Spmap.t
+type frozen_t = implicits KNmap.t
* implicits Indmap.t
* implicits Constrmap.t
* implicits Idmap.t
let init () =
- constants_table := Spmap.empty;
+ constants_table := KNmap.empty;
inductives_table := Indmap.empty;
constructors_table := Constrmap.empty;
var_table := Idmap.empty
diff --git a/library/impargs.mli b/library/impargs.mli
index 022a38230..751d96844 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -10,6 +10,7 @@
(*i*)
open Names
+open Libnames
open Term
open Environ
open Nametab
diff --git a/library/lib.ml b/library/lib.ml
index 8eaba772e..286133305 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -11,23 +11,102 @@
open Pp
open Util
open Names
+open Libnames
open Nameops
open Libobject
open Summary
+
type node =
| Leaf of obj
- | Module of dir_path
- | OpenedSection of dir_path * Summary.frozen
+ | CompilingModule of object_prefix
+ | OpenedModule of object_prefix * Summary.frozen
+ | OpenedModtype of object_prefix * Summary.frozen
+ | OpenedSection of object_prefix * Summary.frozen
(* bool is to tell if the section must be opened automatically *)
| ClosedSection of bool * dir_path * library_segment
| FrozenState of Summary.frozen
-and library_entry = section_path * node
+and library_entry = object_name * node
and library_segment = library_entry list
+type lib_objects = (identifier * obj) list
+
+let rec iter_leaves f i seg =
+ match seg with
+ | [] -> ()
+ | (oname ,Leaf obj)::segtl ->
+ f i (oname,obj);
+ iter_leaves f i segtl
+ | _ -> anomaly "We should have leaves only here"
+
+
+let open_segment = iter_leaves open_object
+
+let load_segment = iter_leaves load_object
+
+let change_kns mp seg =
+ let subst_one = function
+ | ((sp,kn),(Leaf obj as lobj)) ->
+ let kn' = make_kn mp empty_dirpath (label kn) in
+ ((sp,kn'),lobj)
+ | _ -> anomaly "We should have leaves only here"
+ in
+ List.map subst_one seg
+
+let subst_segment (dirpath,(mp,dir)) subst seg =
+ let subst_one = function
+ | ((sp,kn),Leaf obj) ->
+ let sp' = make_path dirpath (basename sp) in
+ let kn' = make_kn mp dir (label kn) in
+ let oname' = sp',kn' in
+ let obj' = subst_object (oname',subst,obj) in
+ (oname', Leaf obj')
+ | _ -> anomaly "We should have leaves only here"
+ in
+ List.map subst_one seg
+
+
+let iter_objects f i prefix =
+ List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
+
+let load_objects = iter_objects load_object
+let open_objects = iter_objects open_object
+
+let subst_objects prefix subst seg =
+ let subst_one = fun (id,obj as node) ->
+ let obj' = subst_object (make_oname prefix id, subst, obj) in
+ if obj' == obj then node else
+ (id, obj')
+ in
+ list_smartmap subst_one seg
+
+let classify_objects seg =
+ let rec clean ((substl,keepl,anticipl) as acc) = function
+ | (_,CompilingModule _) :: _ | [] -> acc
+ | ((sp,kn as oname),Leaf o) as node :: stk ->
+ let id = id_of_label (label kn) in
+ (match classify_object (oname,o) with
+ | Dispose -> clean acc stk
+ | Keep o' ->
+ clean (substl, (id,o')::keepl, anticipl) stk
+ | Substitute o' ->
+ clean ((id,o')::substl, keepl, anticipl) stk
+ | Anticipate o' ->
+ clean (substl, keepl, o'::anticipl) stk)
+ | (oname,ClosedSection _ as item) :: stk -> clean acc stk
+ | (_,OpenedSection _) :: _ -> error "there are still opened sections"
+ | (_,OpenedModule _) :: _ -> error "there are still opened modules"
+ | (_,OpenedModtype _) :: _ -> error "there are still opened module types"
+ | (_,FrozenState _) :: stk -> clean acc stk
+ in
+ clean ([],[],[]) (List.rev seg)
+
+
+let segment_of_objects prefix =
+ List.map (fun (id,obj) -> (make_oname prefix id, Leaf obj))
(* We keep trace of operations in the stack [lib_stk].
[path_prefix] is the current path of sections, where sections are stored in
@@ -36,31 +115,44 @@ and library_segment = library_entry list
sections, but on the contrary there are many constructions of section
paths based on the library path. *)
+let initial_prefix = default_module,(initial_path,empty_dirpath)
+
let lib_stk = ref ([] : library_segment)
-let module_name = ref None
-let path_prefix = ref (default_module : dir_path)
+let comp_name = ref None
+let path_prefix = ref initial_prefix
-let module_sp () =
- match !module_name with Some m -> m | None -> default_module
+let module_dp () =
+ match !comp_name with Some m -> m | None -> default_module
let recalc_path_prefix () =
let rec recalc = function
| (sp, OpenedSection (dir,_)) :: _ -> dir
+ | (sp, OpenedModule (dir,_)) :: _ -> dir
+ | (sp, OpenedModtype (dir,_)) :: _ -> dir
+ | (sp, CompilingModule dir) :: _ -> dir
| _::l -> recalc l
- | [] -> module_sp ()
+ | [] -> initial_prefix
in
path_prefix := recalc !lib_stk
-let pop_path_prefix () = path_prefix := fst (split_dirpath !path_prefix)
+let pop_path_prefix () =
+ let dir,(mp,sec) = !path_prefix in
+ path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec))
+
+let make_path id = Libnames.make_path (fst !path_prefix) id
-let make_path id = Names.make_path !path_prefix id
+let make_kn id =
+ let mp,dir = snd !path_prefix in
+ Names.make_kn mp dir (label_of_id id)
+
+let make_oname id = make_path id, make_kn id
let sections_depth () =
- List.length (repr_dirpath !path_prefix)
- - List.length (repr_dirpath (module_sp ()))
+ List.length (repr_dirpath (snd (snd !path_prefix)))
-let cwd () = !path_prefix
+let cwd () = fst !path_prefix
+let current_prefix () = snd !path_prefix
let find_entry_p p =
let rec find = function
@@ -70,12 +162,17 @@ let find_entry_p p =
find !lib_stk
let split_lib sp =
- let rec findrec after = function
- | ((sp',obj) as hd)::before ->
- if sp = sp' then (after,hd,before) else findrec (hd::after) before
+ let rec collect after equal = function
+ | ((sp',_) as hd)::before ->
+ if sp = sp' then collect after (hd::equal) before else after,equal,hd::before
+ | [] -> after,equal,[]
+ in
+ let rec findeq after = function
+ | ((sp',_) as hd)::before ->
+ if sp = sp' then collect after [hd] before else findeq (hd::after) before
| [] -> error "no such entry"
in
- findrec [] !lib_stk
+ findeq [] !lib_stk
(* Adding operations. *)
@@ -87,119 +184,267 @@ let anonymous_id =
fun () -> incr n; id_of_string ("_" ^ (string_of_int !n))
let add_anonymous_entry node =
- let sp = make_path (anonymous_id()) in
- add_entry sp node;
- sp
+ let id = anonymous_id () in
+ let name = make_oname id in
+ add_entry name node;
+ name
let add_absolutely_named_leaf sp obj =
cache_object (sp,obj);
add_entry sp (Leaf obj)
let add_leaf id obj =
- let sp = make_path id in
- cache_object (sp,obj);
- add_entry sp (Leaf obj);
- sp
+ let oname = make_oname id in
+ cache_object (oname,obj);
+ add_entry oname (Leaf obj);
+ oname
+
+let add_leaves id objs =
+ let oname = make_oname id in
+ let add_obj obj =
+ add_entry oname (Leaf obj);
+ load_object 1 (oname,obj)
+ in
+ List.iter add_obj objs;
+ oname
let add_anonymous_leaf obj =
- let sp = make_path (anonymous_id()) in
- cache_object (sp,obj);
- add_entry sp (Leaf obj)
+ let id = anonymous_id () in
+ let oname = make_oname id in
+ cache_object (oname,obj);
+ add_entry oname (Leaf obj)
let add_frozen_state () =
let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
+(* Modules. *)
+
+let is_something_opened = function
+ (_,OpenedSection _) -> true
+ | (_,OpenedModule _) -> true
+ | (_,OpenedModtype _) -> true
+ | _ -> false
+
+let classify_segment seg =
+ let rec clean ((substl,keepl,anticipl) as acc) = function
+ | (_,CompilingModule _) :: _ | [] -> acc
+ | (oname,Leaf o) as node :: stk ->
+ (match classify_object (oname,o) with
+ | Dispose -> clean acc stk
+ | Keep o' ->
+ clean (substl, (oname,Leaf o')::keepl, anticipl) stk
+ | Substitute o' ->
+ clean ((oname,Leaf o')::substl, keepl, anticipl) stk
+ | Anticipate o' ->
+ clean (substl, keepl, (oname,Leaf o')::anticipl) stk)
+ | (oname,ClosedSection _ as item) :: stk -> clean acc stk
+ | (_,OpenedSection _) :: _ -> error "there are still opened sections"
+ | (_,OpenedModule _) :: _ -> error "there are still opened modules"
+ | (_,OpenedModtype _) :: _ -> error "there are still opened module types"
+ | (_,FrozenState _) :: stk -> clean acc stk
+ in
+ clean ([],[],[]) (List.rev seg)
+
+let export_segment seg =
+ let rec clean acc = function
+ | (_,CompilingModule _) :: _ | [] -> acc
+ | (oname,Leaf o) as node :: stk ->
+ (match export_object o with
+ | None -> clean acc stk
+ | Some o' -> clean ((oname,Leaf o') :: acc) stk)
+ | (oname,ClosedSection _ as item) :: stk -> clean (item :: acc) stk
+ | (_,OpenedSection _) :: _ -> error "there are still opened sections"
+ | (_,OpenedModule _) :: _ -> error "there are still opened modules"
+ | (_,OpenedModtype _) :: _ -> error "there are still opened module types"
+ | (_,FrozenState _) :: stk -> clean acc stk
+ in
+ clean [] seg
+
+
+let start_module id mp nametab =
+ let dir = extend_dirpath (fst !path_prefix) id in
+ let prefix = dir,(mp,empty_dirpath) in
+ let oname = make_path id, make_kn id in
+ if Nametab.exists_module dir then
+ errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
+ add_entry oname (OpenedModule (prefix,nametab));
+ path_prefix := prefix
+(* add_frozen_state () must be called in declaremods *)
+
+let end_module id =
+ let oname,nametab =
+ try match find_entry_p is_something_opened with
+ | oname,OpenedModule (_,nametab) ->
+ let sp = fst oname in
+ let id' = basename sp in
+ if id<>id' then error "this is not the last opened module";
+ oname,nametab
+ | _,OpenedModtype _ ->
+ error "there are some open module types"
+ | _,OpenedSection _ ->
+ error "there are some open sections"
+ | _ -> assert false
+ with Not_found ->
+ error "no opened modules"
+ in
+ let (after,_,before) = split_lib oname in
+ lib_stk := before;
+ let prefix = !path_prefix in
+ recalc_path_prefix ();
+ (* add_frozen_state must be called after processing the module,
+ because we cannot recache interactive modules *)
+ (oname, prefix, nametab,after)
+
+let start_modtype id mp nametab =
+ let dir = extend_dirpath (fst !path_prefix) id in
+ let prefix = dir,(mp,empty_dirpath) in
+ let sp = make_path id in
+ let name = sp, make_kn id in
+ if Nametab.exists_cci sp then
+ errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ;
+ add_entry name (OpenedModtype (prefix,nametab));
+ path_prefix := prefix
+
+let end_modtype id =
+ let sp,nametab =
+ try match find_entry_p is_something_opened with
+ | sp,OpenedModtype (_,nametab) ->
+ let id' = basename (fst sp) in
+ if id<>id' then error "this is not the last opened module";
+ sp,nametab
+ | _,OpenedModule _ ->
+ error "there are some open modules"
+ | _,OpenedSection _ ->
+ error "there are some open sections"
+ | _ -> assert false
+ with Not_found ->
+ error "no opened module types"
+ in
+ let (after,_,before) = split_lib sp in
+ lib_stk := before;
+ let dir = !path_prefix in
+ recalc_path_prefix ();
+ (* add_frozen_state must be called after processing the module type.
+ This is because we cannot recache interactive module types *)
+ (sp,dir,nametab,after)
+
+
+
let contents_after = function
| None -> !lib_stk
| Some sp -> let (after,_,_) = split_lib sp in after
(* Modules. *)
-let check_for_module () =
+let check_for_comp_unit () =
let is_decl = function (_,FrozenState _) -> false | _ -> true in
try
let _ = find_entry_p is_decl in
- error "a module can not be started after some declarations"
+ error "a module cannot be started after some declarations"
with Not_found -> ()
(* TODO: use check_for_module ? *)
-let start_module s =
- if !module_name <> None then
- error "a module is already started";
- if !path_prefix <> default_module then
+let start_compilation s mp =
+ if !comp_name <> None then
+ error "compilation unit is already started";
+ if snd (snd (!path_prefix)) <> empty_dirpath then
error "some sections are already opened";
- module_name := Some s;
- let _ = add_anonymous_entry (Module s) in
- path_prefix := s
-
-let end_module s =
- match !module_name with
- | None -> error "no module declared"
- | Some m ->
- let (_,bm) = split_dirpath m in
- if bm <> s then
- error ("The current open module has basename "^(string_of_id bm));
- m
+ let prefix = s, (mp, empty_dirpath) in
+ let _ = add_anonymous_entry (CompilingModule prefix) in
+ comp_name := Some s;
+ path_prefix := prefix
+
+let end_compilation dir =
+ let _ =
+ try match find_entry_p is_something_opened with
+ | _, OpenedSection _ -> error "There are some open sections"
+ | _, OpenedModule _ -> error "There are some open modules"
+ | _, OpenedModtype _ -> error "There are some open module types"
+ | _ -> assert false
+ with
+ Not_found -> ()
+ in
+ let module_p =
+ function (_,CompilingModule _) -> true | x -> is_something_opened x
+ in
+ let oname =
+ try match find_entry_p module_p with
+ (oname, CompilingModule prefix) -> oname
+ | _ -> assert false
+ with
+ Not_found -> anomaly "No module declared"
+ in
+ let _ = match !comp_name with
+ | None -> anomaly "There should be a module name..."
+ | Some m ->
+ if m <> dir then anomaly
+ ("The current open module has name "^ (string_of_dirpath m) ^
+ " and not " ^ (string_of_dirpath m));
+ in
+ let (after,_,before) = split_lib oname in
+ !path_prefix,after
+
+(* Returns true if we are inside an opened module type *)
+let is_specification () =
+ let opened_p = function
+ | _, OpenedModtype _ -> true
+ | _ -> false
+ in
+ try
+ let _ = find_entry_p opened_p in true
+ with
+ Not_found -> false
+
+(* Returns the most recent OpenedThing node *)
+let what_is_opened () = find_entry_p is_something_opened
(* Sections. *)
let open_section id =
- let dir = extend_dirpath !path_prefix id in
- let sp = make_path id in
+ let olddir,(mp,oldsec) = !path_prefix in
+ let dir = extend_dirpath olddir id in
+ let prefix = dir, (mp, extend_dirpath oldsec id) in
+ let name = make_path id, make_kn id (* this makes little sense however *) in
if Nametab.exists_section dir then
errorlabstrm "open_section" (pr_id id ++ str " already exists");
let sum = freeze_summaries() in
- add_entry sp (OpenedSection (dir, sum));
+ add_entry name (OpenedSection (prefix, sum));
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
- Nametab.push_section dir;
- path_prefix := dir;
- sp
-
-let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
+ Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
+ path_prefix := prefix;
+ prefix
let sections_are_opened () =
- try let _ = find_entry_p is_opened_section in true
+ try
+ match find_entry_p is_something_opened with
+ | (_,OpenedSection _) -> true
+ | (_,OpenedModule _) -> false
+ | _ -> false
with Not_found -> false
-let export_segment seg =
- let rec clean acc = function
- | (_,Module _) :: _ | [] -> acc
- | (sp,Leaf o) as node :: stk ->
- (match export_object o with
- | None -> clean acc stk
- | Some o' -> clean ((sp,Leaf o') :: acc) stk)
- | (sp,ClosedSection _ as item) :: stk -> clean (item :: acc) stk
- | (_,OpenedSection _) :: _ -> error "there are still opened sections"
- | (_,FrozenState _) :: stk -> clean acc stk
- in
- clean [] seg
-
(* Restore lib_stk and summaries as before the section opening, and
add a ClosedSection object. *)
let close_section ~export id =
- let sp,dir,fs =
- try match find_entry_p is_opened_section with
- | sp,OpenedSection (dir,fs) ->
- if id<>snd(split_dirpath dir) then
+ let oname,fs =
+ try match find_entry_p is_something_opened with
+ | oname,OpenedSection (_,fs) ->
+ if id <> basename (fst oname) then
error "this is not the last opened section";
- (sp,dir,fs)
- | _ -> assert false
+ (oname,fs)
+ | _ -> assert false
with Not_found ->
error "no opened section"
in
- let (after,_,before) = split_lib sp in
+ let (after,_,before) = split_lib oname in
lib_stk := before;
+ let prefix = !path_prefix in
pop_path_prefix ();
- let closed_sec = ClosedSection (export, dir, export_segment after) in
- add_entry (make_path id) closed_sec;
- (dir,after,fs)
-
-(* The following function exports the whole library segment, that will be
- saved as a module. Objects are presented in chronological order, and
- frozen states are removed. *)
-
-let export_module s =
- export_segment !lib_stk
+ let closed_sec =
+ ClosedSection (export, (fst prefix), export_segment after)
+ in
+ let name = make_path id, make_kn id in
+ add_entry name closed_sec;
+ (prefix, after, fs)
(* Backtracking. *)
@@ -207,6 +452,7 @@ let recache_decl = function
| (sp, Leaf o) -> cache_object (sp,o)
| _ -> ()
+
let recache_context ctx =
List.iter recache_decl ctx
@@ -226,21 +472,16 @@ let reset_to sp =
let reset_name id =
let (sp,_) =
try
- find_entry_p (fun (sp,_) -> let (_,spi) = repr_path sp in id = spi)
+ find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
with Not_found ->
error (string_of_id id ^ ": no such entry")
in
reset_to sp
let point_obj =
- let (f,_) =
- declare_object
- ("DOT",
- {cache_function = (fun _ -> ());
- load_function = (fun _ -> ());
- open_function = (fun _ -> ());
- export_function = (fun _ -> None) }) in
- f()
+ let (f,_) = declare_object {(default_object "DOT") with
+ classify_function = (fun _ -> Dispose)} in
+ f()
let mark_end_of_command () =
match !lib_stk with
@@ -258,41 +499,41 @@ let back n = reset_to (back_stk n !lib_stk)
(* [dir] is a section dir if [module] < [dir] <= [path_prefix] *)
let is_section_p sp =
- not (is_dirpath_prefix_of sp (module_sp ()))
- & (is_dirpath_prefix_of sp !path_prefix)
+ not (is_dirpath_prefix_of sp (module_dp ()))
+ & (is_dirpath_prefix_of sp (fst !path_prefix))
(* State and initialization. *)
type frozen = dir_path option * library_segment
-let freeze () = (!module_name, !lib_stk)
+let freeze () = (!comp_name, !lib_stk)
let unfreeze (mn,stk) =
- module_name := mn;
+ comp_name := mn;
lib_stk := stk;
recalc_path_prefix ()
let init () =
lib_stk := [];
add_frozen_state ();
- module_name := None;
- path_prefix := make_dirpath [];
+ comp_name := None;
+ path_prefix := initial_prefix;
init_summaries()
(* Initial state. *)
-let initial_state = ref (None : section_path option)
+let initial_state = ref None
let declare_initial_state () =
- let sp = add_anonymous_entry (FrozenState (freeze_summaries())) in
- initial_state := Some sp
+ let name = add_anonymous_entry (FrozenState (freeze_summaries())) in
+ initial_state := Some name
let reset_initial () =
match !initial_state with
| None -> init ()
| Some sp ->
begin match split_lib sp with
- | (_,(_,FrozenState fs as hd),before) ->
+ | (_,[_,FrozenState fs as hd],before) ->
lib_stk := hd::before;
recalc_path_prefix ();
unfreeze_summaries fs
diff --git a/library/lib.mli b/library/lib.mli
index b86c08f72..90f111c4b 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -10,6 +10,7 @@
(*i*)
open Names
+open Libnames
open Libobject
open Summary
(*i*)
@@ -20,53 +21,127 @@ open Summary
type node =
| Leaf of obj
- | Module of dir_path
- | OpenedSection of dir_path * Summary.frozen
+ | CompilingModule of object_prefix
+ | OpenedModule of object_prefix * Summary.frozen
+ | OpenedModtype of object_prefix * Summary.frozen
+ | OpenedSection of object_prefix * Summary.frozen
| ClosedSection of bool * dir_path * library_segment
| FrozenState of Summary.frozen
-and library_entry = section_path * node
+and library_entry = object_name * node
and library_segment = library_entry list
+type lib_objects = (identifier * obj) list
-(*s Adding operations (which calls the [cache] method, and getting the
+(*s These functions iterate (or map) object functions.
+
+ [subst_segment prefix subst seg] makes an assumption that all
+ objects in [seg] have the same prefix. This prefix is universally
+ changed to [prefix].
+
+ [classify_segment seg] divides segment into objects which responded
+ with [Substitute], [Keep], [Anticipate] respectively, to the
+ [classify_object] function. The order of each returned list is the
+ same as in the input list.
+
+ [change_kns mp lib] only changes the prefix of the [kernel_name]
+ part of the [object_name] of every object to [(mp,empty_dirpath)].
+ The [section_path] part of the [object_name] and the object itself
+ are unchanged.
+*)
+
+
+val open_segment : int -> library_segment -> unit
+val load_segment : int -> library_segment -> unit
+val subst_segment :
+ object_prefix -> substitution -> library_segment -> library_segment
+val classify_segment :
+ library_segment -> library_segment * library_segment * library_segment
+val change_kns : module_path -> library_segment -> library_segment
+
+
+
+val open_objects : int -> object_prefix -> lib_objects -> unit
+val load_objects : int -> object_prefix -> lib_objects -> unit
+val subst_objects :
+ object_prefix -> substitution -> lib_objects -> lib_objects
+val classify_objects :
+ library_segment -> lib_objects * lib_objects * obj list
+
+val segment_of_objects :
+ object_prefix -> lib_objects -> library_segment
+
+(*s Adding operations (which call the [cache] method, and getting the
current list of operations (most recent ones coming first). *)
-val add_leaf : identifier -> obj -> section_path
-val add_absolutely_named_leaf : section_path -> obj -> unit
+val add_leaf : identifier -> obj -> object_name
+val add_absolutely_named_leaf : object_name -> obj -> unit
val add_anonymous_leaf : obj -> unit
+
+(* this operation adds all objects with the same name and calls load_object
+ for each of them *)
+val add_leaves : identifier -> obj list -> object_name
+
val add_frozen_state : unit -> unit
val mark_end_of_command : unit -> unit
(*s The function [contents_after] returns the current library segment,
- starting from a given section path. If not given, the entire segment
- is returned. *)
+ starting from a given section path. If not given, the entire segment
+ is returned. *)
-val contents_after : section_path option -> library_segment
+val contents_after : object_name option -> library_segment
+(* Returns true if we are inside an opened module type *)
+val is_specification : unit -> bool
+
+(* Returns the most recent OpenedThing node *)
+val what_is_opened : unit -> library_entry
(*s Opening and closing a section. *)
-val open_section : identifier -> section_path
-val close_section :
- export:bool -> identifier -> dir_path * library_segment * Summary.frozen
+val open_section : identifier -> object_prefix
+
+val close_section : export:bool -> identifier ->
+ object_prefix * library_segment * Summary.frozen
+
val sections_are_opened : unit -> bool
val make_path : identifier -> section_path
+val make_kn : identifier -> kernel_name
+
val cwd : unit -> dir_path
val sections_depth : unit -> int
val is_section_p : dir_path -> bool
-val start_module : dir_path -> unit
-val end_module : module_ident -> dir_path
-val export_module : dir_path -> library_segment
+(*s Compilation units *)
+
+val start_compilation : dir_path -> module_path -> unit
+val end_compilation : dir_path -> object_prefix * library_segment
+
+val module_dp : unit -> dir_path
+(*s Modules and module types *)
+
+val start_module : module_ident -> module_path -> Summary.frozen -> unit
+val end_module : module_ident
+ -> object_name * object_prefix * Summary.frozen * library_segment
+
+val start_modtype : module_ident -> module_path -> Summary.frozen -> unit
+val end_modtype : module_ident
+ -> object_name * object_prefix * Summary.frozen * library_segment
+
+(* Lib.add_frozen_state must be called after all of the above functions *)
+
+val current_prefix : unit -> module_path * dir_path
(*s Backtracking (undo). *)
-val reset_to : section_path -> unit
+val reset_to : object_name -> unit
val reset_name : identifier -> unit
+
+(* [back n] resets to the place corresponding to the $n$-th call of
+ [mark_end_of_command] (counting backwards) *)
val back : int -> unit
(*s We can get and set the state of the operations (used in [States]). *)
diff --git a/library/libnames.ml b/library/libnames.ml
new file mode 100644
index 000000000..d5e9c8dc7
--- /dev/null
+++ b/library/libnames.ml
@@ -0,0 +1,212 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Pp
+open Util
+open Names
+
+type global_reference =
+ | VarRef of variable
+ | ConstRef of constant
+ | IndRef of inductive
+ | ConstructRef of constructor
+
+let subst_global subst ref = match ref with
+ | VarRef _ -> ref
+ | ConstRef kn ->
+ let kn' = subst_kn subst kn in if kn==kn' then ref else
+ ConstRef kn'
+ | IndRef (kn,i) ->
+ let kn' = subst_kn subst kn in if kn==kn' then ref else
+ IndRef(kn',i)
+ | ConstructRef ((kn,i),j) ->
+ let kn' = subst_kn subst kn in if kn==kn' then ref else
+ ConstructRef ((kn',i),j)
+
+
+(**********************************************)
+
+let pr_dirpath sl = (str (string_of_dirpath sl))
+
+(*s Operations on dirpaths *)
+
+(* Pop the last n module idents *)
+let extract_dirpath_prefix n dir =
+ let (_,dir') = list_chop n (repr_dirpath dir) in
+ make_dirpath dir'
+
+let dirpath_prefix p = match repr_dirpath p with
+ | [] -> anomaly "dirpath_prefix: empty dirpath"
+ | _::l -> make_dirpath l
+
+let is_dirpath_prefix_of d1 d2 =
+ list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+
+(* To know how qualified a name should be to be understood in the current env*)
+let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
+
+let split_dirpath d =
+ let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
+
+let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
+
+
+(*
+let path_of_constructor env ((sp,tyi),ind) =
+ let mib = Environ.lookup_mind sp env in
+ let mip = mib.mind_packets.(tyi) in
+ let (pa,_) = repr_path sp in
+ Names.make_path pa (mip.mind_consnames.(ind-1))
+
+let path_of_inductive env (sp,tyi) =
+ if tyi = 0 then sp
+ else
+ let mib = Environ.lookup_mind sp env in
+ let mip = mib.mind_packets.(tyi) in
+ let (pa,_) = repr_path sp in
+ Names.make_path pa (mip.mind_typename)
+*)
+(* parsing *)
+let parse_dir s =
+ let len = String.length s in
+ let rec decoupe_dirs dirs n =
+ if n>=len then dirs else
+ let pos =
+ try
+ String.index_from s n '.'
+ with Not_found -> len
+ in
+ let dir = String.sub s n (pos-n) in
+ decoupe_dirs ((id_of_string dir)::dirs) (pos+1)
+ in
+ decoupe_dirs [] 0
+
+let dirpath_of_string s =
+ match parse_dir s with
+ [] -> invalid_arg "dirpath_of_string"
+ | dir -> make_dirpath dir
+
+
+(*s Section paths are absolute names *)
+
+type section_path = {
+ dirpath : dir_path ;
+ basename : identifier }
+
+let make_path pa id = { dirpath = pa; basename = id }
+let repr_path { dirpath = pa; basename = id } = (pa,id)
+
+(* parsing and printing of section paths *)
+let string_of_path sp =
+ let (sl,id) = repr_path sp in
+ if repr_dirpath sl = [] then string_of_id id
+ else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+
+let sp_ord sp1 sp2 =
+ let (p1,id1) = repr_path sp1
+ and (p2,id2) = repr_path sp2 in
+ let p_bit = compare p1 p2 in
+ if p_bit = 0 then id_ord id1 id2 else p_bit
+
+module SpOrdered =
+ struct
+ type t = section_path
+ let compare = sp_ord
+ end
+
+module Spset = Set.Make(SpOrdered)
+module Sppred = Predicate.Make(SpOrdered)
+module Spmap = Map.Make(SpOrdered)
+
+let dirpath sp = let (p,_) = repr_path sp in p
+let basename sp = let (_,id) = repr_path sp in id
+
+let path_of_string s =
+ try
+ let dir, id = split_dirpath (dirpath_of_string s) in
+ make_path dir id
+ with
+ | Invalid_argument _ -> invalid_arg "path_of_string"
+
+let pr_sp sp = str (string_of_path sp)
+
+let restrict_path n sp =
+ let dir, s = repr_path sp in
+ let (dir',_) = list_chop n (repr_dirpath dir) in
+ make_path (make_dirpath dir') s
+
+type extended_global_reference =
+ | TrueGlobal of global_reference
+ | SyntacticDef of kernel_name
+
+let subst_ext subst glref = match glref with
+ | TrueGlobal ref ->
+ let ref' = subst_global subst ref in
+ if ref' == ref then glref else
+ TrueGlobal ref'
+ | SyntacticDef kn ->
+ let kn' = subst_kn subst kn in
+ if kn' == kn then glref else
+ SyntacticDef kn'
+
+let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
+
+let decode_kn kn =
+ let mp,sec_dir,l = repr_kn kn in
+ match mp,(repr_dirpath sec_dir) with
+ MPfile dir,[] -> (dir,id_of_label l)
+ | _ , [] -> anomaly "MPfile expected!"
+ | _ -> anomaly "Section part should be empty!"
+
+(*s qualified names *)
+type qualid = section_path
+
+let make_qualid = make_path
+let repr_qualid = repr_path
+
+let string_of_qualid = string_of_path
+let pr_qualid = pr_sp
+
+let qualid_of_string = path_of_string
+
+let qualid_of_sp sp = sp
+let make_short_qualid id = make_qualid empty_dirpath id
+let qualid_of_dirpath dir =
+ let (l,a) = split_dirpath dir in
+ make_qualid l a
+
+type object_name = section_path * kernel_name
+
+type object_prefix = dir_path * (module_path * dir_path)
+
+let make_oname (dirpath,(mp,dir)) id =
+ make_path dirpath id, make_kn mp dir (label_of_id id)
+
+(* to this type are mapped dir_path's in the nametab *)
+type global_dir_reference =
+ | DirOpenModule of object_prefix
+ | DirOpenModtype of object_prefix
+ | DirOpenSection of object_prefix
+ | DirModule of object_prefix
+ | DirClosedSection of dir_path
+ (* this won't last long I hope! *)
+
+(* | ModRef mp ->
+ let mp' = subst_modpath subst mp in if mp==mp' then ref else
+ ModRef mp'
+ | ModTypeRef kn ->
+ let kn' = subst_kernel_name subst kn in if kn==kn' then ref else
+ ModTypeRef kn'
+*)
+
+type strength =
+ | NotDeclare
+ | DischargeAt of dir_path * int
+ | NeverDischarge
diff --git a/library/libnames.mli b/library/libnames.mli
new file mode 100644
index 000000000..915cdf3d2
--- /dev/null
+++ b/library/libnames.mli
@@ -0,0 +1,118 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Pp
+open Names
+(*i*)
+
+(*s Global reference is a kernel side type for all references together *)
+type global_reference =
+ | VarRef of variable
+ | ConstRef of constant
+ | IndRef of inductive
+ | ConstructRef of constructor
+
+val subst_global : substitution -> global_reference -> global_reference
+
+(* dirpaths *)
+val pr_dirpath : dir_path -> Pp.std_ppcmds
+
+val dirpath_of_string : string -> dir_path
+
+(* Give the immediate prefix of a [dir_path] *)
+val dirpath_prefix : dir_path -> dir_path
+
+(* Give the immediate prefix and basename of a [dir_path] *)
+val split_dirpath : dir_path -> dir_path * identifier
+
+val extend_dirpath : dir_path -> module_ident -> dir_path
+val add_dirpath_prefix : module_ident -> dir_path -> dir_path
+
+val extract_dirpath_prefix : int -> dir_path -> dir_path
+val is_dirpath_prefix_of : dir_path -> dir_path -> bool
+
+(*s Section paths are {\em absolute} names *)
+type section_path
+
+(* Constructors of [section_path] *)
+val make_path : dir_path -> identifier -> section_path
+
+(* Destructors of [section_path] *)
+val repr_path : section_path -> dir_path * identifier
+val dirpath : section_path -> dir_path
+val basename : section_path -> identifier
+
+(* Parsing and printing of section path as ["coq_root.module.id"] *)
+val path_of_string : string -> section_path
+val string_of_path : section_path -> string
+val pr_sp : section_path -> std_ppcmds
+
+module Sppred : Predicate.S with type elt = section_path
+module Spmap : Map.S with type key = section_path
+
+val restrict_path : int -> section_path -> section_path
+
+type extended_global_reference =
+ | TrueGlobal of global_reference
+ | SyntacticDef of kernel_name
+
+val subst_ext :
+ substitution -> extended_global_reference -> extended_global_reference
+
+(*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
+
+
+(*s A [qualid] is a partially qualified ident; it includes fully
+ qualified names (= absolute names) and all intermediate partial
+ qualifications of absolute names, including single identifiers *)
+type qualid
+
+val make_qualid : dir_path -> identifier -> qualid
+val repr_qualid : qualid -> dir_path * identifier
+
+val string_of_qualid : qualid -> string
+val pr_qualid : qualid -> std_ppcmds
+
+val qualid_of_string : string -> qualid
+
+(* Turns an absolute name into a qualified name denoting the same name *)
+val qualid_of_sp : section_path -> qualid
+
+val qualid_of_dirpath : dir_path -> qualid
+
+val make_short_qualid : identifier -> qualid
+
+(* Both names are passed to objects: a "semantic" kernel_name, which
+ can be substituted and a "syntactic" section_path which can be printed
+*)
+
+type object_name = section_path * kernel_name
+
+type object_prefix = dir_path * (module_path * dir_path)
+
+val make_oname : object_prefix -> identifier -> object_name
+
+(* to this type are mapped dir_path's in the nametab *)
+type global_dir_reference =
+ | DirOpenModule of object_prefix
+ | DirOpenModtype of object_prefix
+ | DirOpenSection of object_prefix
+ | DirModule of object_prefix
+ | DirClosedSection of dir_path
+ (* this won't last long I hope! *)
+
+type strength =
+ | NotDeclare
+ | DischargeAt of dir_path * int
+ | NeverDischarge
diff --git a/library/libobject.ml b/library/libobject.ml
index bbd8615be..2049e8e04 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -10,6 +10,7 @@
open Util
open Names
+open Libnames
(* The relax flag is used to make it possible to load files while ignoring
failures to incorporate some objects. This can be useful when one
@@ -23,18 +24,53 @@ let relax_flag = ref false;;
let relax b = relax_flag := b;;
+type 'a substitutivity =
+ Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
+
+
type 'a object_declaration = {
- cache_function : section_path * 'a -> unit;
- load_function : section_path * 'a -> unit;
- open_function : section_path * 'a -> unit;
+ object_name : string;
+ cache_function : object_name * 'a -> unit;
+ load_function : int -> object_name * 'a -> unit;
+ open_function : int -> object_name * 'a -> unit;
+ classify_function : object_name * 'a -> 'a substitutivity;
+ subst_function : object_name * substitution * 'a -> 'a;
export_function : 'a -> 'a option }
+let yell s = anomaly s
+
+let default_object s = {
+ object_name = s;
+ cache_function = (fun _ -> ());
+ load_function = (fun _ _ -> ());
+ open_function = (fun _ _ -> ());
+ subst_function = (fun _ ->
+ yell ("The object "^s^" does not know how to substitute!"));
+ classify_function = (fun (_,obj) -> Keep obj);
+ export_function = (fun _ -> None)}
+
+
+(* The suggested object declaration is the following:
+
+ declare_object { (default_object "MY OBJECT") with
+ cache_function = fun (sp,a) -> Mytbl.add sp a}
+
+ and the listed functions are only those which definitions accually
+ differ from the default.
+
+ This helps introducing new functions in objects.
+*)
+
+let ident_subst_function (_,_,a) = a
+
type obj = Dyn.t (* persistent dynamic objects *)
type dynamic_object_declaration = {
- dyn_cache_function : section_path * obj -> unit;
- dyn_load_function : section_path * obj -> unit;
- dyn_open_function : section_path * obj -> unit;
+ 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_classify_function : object_name * obj -> obj substitutivity;
dyn_export_function : obj -> obj option }
let object_tag lobj = Dyn.tag lobj
@@ -42,23 +78,43 @@ let object_tag lobj = Dyn.tag lobj
let cache_tab =
(Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
-let declare_object (na,odecl) =
+let declare_object odecl =
+ let na = odecl.object_name in
let (infun,outfun) = Dyn.create na in
- let cacher (spopt,lobj) =
- if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj)
+ let cacher (oname,lobj) =
+ if Dyn.tag lobj = na then odecl.cache_function (oname,outfun lobj)
else anomaly "somehow we got the wrong dynamic object in the cachefun"
- and loader (spopt,lobj) =
- if Dyn.tag lobj = na then odecl.load_function (spopt,outfun lobj)
+ and loader i (oname,lobj) =
+ if Dyn.tag lobj = na then odecl.load_function i (oname,outfun lobj)
else anomaly "somehow we got the wrong dynamic object in the loadfun"
- and opener (spopt,lobj) =
- if Dyn.tag lobj = na then odecl.open_function (spopt,outfun lobj)
+ 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))
+ else anomaly "somehow we got the wrong dynamic object in the substfun"
+ and classifier (spopt,lobj) =
+ if Dyn.tag lobj = na then
+ match odecl.classify_function (spopt,outfun lobj) with
+ | Dispose -> Dispose
+ | Substitute obj -> Substitute (infun obj)
+ | Keep obj -> Keep (infun obj)
+ | Anticipate (obj) -> Anticipate (infun obj)
+ else
+ anomaly "somehow we got the wrong dynamic object in the classifyfun"
and exporter lobj =
- option_app infun (odecl.export_function (outfun lobj))
+ if Dyn.tag lobj = na then
+ option_app infun (odecl.export_function (outfun lobj))
+ else
+ anomaly "somehow we got the wrong dynamic object in the exportfun"
+
in
Hashtbl.add cache_tab na { dyn_cache_function = cacher;
dyn_load_function = loader;
dyn_open_function = opener;
+ dyn_subst_function = substituter;
+ dyn_classify_function = classifier;
dyn_export_function = exporter };
(infun,outfun)
@@ -85,11 +141,17 @@ let apply_dyn_fun deflt f lobj =
let cache_object ((_,lobj) as node) =
apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
-let load_object ((_,lobj) as node) =
- apply_dyn_fun () (fun d -> d.dyn_load_function node) lobj
+let load_object i ((_,lobj) as node) =
+ apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj
+
+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) =
+ apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
-let open_object ((_,lobj) as node) =
- apply_dyn_fun () (fun d -> d.dyn_open_function node) lobj
+let classify_object ((_,lobj) as node) =
+ apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
let export_object lobj =
apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 017650e76..1c1209019 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -10,37 +10,96 @@
(*i*)
open Names
+open Libnames
(*i*)
-(* [Libobject] declares persistent objects, given with three methods:
- a caching function specifying how to add the object in the current
- scope of theory modules;
- a loading function, specifying what to do when the object is loaded
- from the disk;
- an opening function, specifying what to do when the module containing
- the object is opened;
- a specification function, to extract its specification when writing
- the specification of a module to the disk (.vi) *)
+(* [Libobject] declares persistent objects, given with methods:
+
+ * a caching function specifying how to add the object in the current
+ scope;
+ If the object wishes to register its visibility in the Nametab,
+ it should do so for all possible sufixes.
+
+ * a loading function, specifying what to do when the module
+ containing the object is loaded;
+ If the object wishes to register its visibility in the Nametab,
+ it should do so for all sufixes no shorter then the "int" argument
+
+ * an opening function, specifying what to do when the module
+ containing the object is opened (imported);
+ If the object wishes to register its visibility in the Nametab,
+ it should do so for the sufix of the length the "int" argument
+
+ * a classification function, specyfying what to do with the object,
+ when the current module (containing the object) is ended;
+ The possibilities are:
+ Dispose - the object dies at the end of the module
+ Substitue - meaning the object is substitutive and
+ the module name must be updated
+ Keep - the object is not substitutive, but survives module
+ closing
+ Anticipate - this is for objects which have to be explicitely
+ managed by the end_module function (like Require
+ and Read markers)
+
+ The classification function is also an occasion for a cleanup
+ (if this function returns Keep or Substitute of some object, the
+ cache method is never called for it)
+
+ * a substitution function, performing the substitution;
+ this function should be declared for substitutive objects
+ only (see obove)
+
+ * an export function, to enable optional writing of its contents
+ to disk (.vo). This function is also the oportunity to remove
+ redundant information in order to keep .vo size small
+
+ The export function is a little obsolete and will be removed
+ in the near future...
+
+*)
+
+type 'a substitutivity =
+ Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
type 'a object_declaration = {
- cache_function : section_path * 'a -> unit;
- load_function : section_path * 'a -> unit;
- open_function : section_path * 'a -> unit;
+ object_name : string;
+ cache_function : object_name * 'a -> unit;
+ load_function : int -> object_name * 'a -> unit;
+ open_function : int -> object_name * 'a -> unit;
+ classify_function : object_name * 'a -> 'a substitutivity;
+ subst_function : object_name * substitution * 'a -> 'a;
export_function : 'a -> 'a option }
-(*s Given an object name and a declaration, the function [declare_object]
+(* The default object is a "Keep" object with empty methods.
+ Object creators are advised to use the construction
+ [{(default_object "MY_OBJECT") with
+ cache_function = ...
+ }]
+ and specify only these functions which are not empty/meaningless
+
+*)
+
+val default_object : string -> 'a object_declaration
+
+(* the identity substitution function *)
+val ident_subst_function : object_name * substitution * 'a -> 'a
+
+(*s Given an object declaration, the function [declare_object]
will hand back two functions, the "injection" and "projection"
functions for dynamically typed library-objects. *)
type obj
val declare_object :
- (string * 'a object_declaration) -> ('a -> obj) * (obj -> 'a)
+ 'a object_declaration -> ('a -> obj) * (obj -> 'a)
val object_tag : obj -> string
-val cache_object : section_path * obj -> unit
-val load_object : section_path * obj -> unit
-val open_object : section_path * obj -> unit
+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 classify_object : object_name * obj -> obj substitutivity
val export_object : obj -> obj option
val relax : bool -> unit
diff --git a/library/library.ml b/library/library.ml
index 93ab76371..8dd3c5432 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -12,13 +12,16 @@ open Pp
open Util
open Names
+open Libnames
open Nameops
-open Environ
+open Safe_typing
open Libobject
open Lib
open Nametab
+open Declaremods
-(*s Load path. *)
+(*************************************************************************)
+(*s Load path. Mapping from physical to logical paths etc.*)
type logical_path = dir_path
@@ -54,6 +57,7 @@ let canonical_path_name p =
(* We give up to find a canonical name and just simplify it... *)
strip_path p
+
let find_logical_path phys_dir =
let phys_dir = canonical_path_name phys_dir in
match list_filter2 (fun p d -> p = phys_dir) !load_path with
@@ -75,7 +79,7 @@ let add_load_path_entry (phys_path,coq_path) =
&& coq_path = Nameops.default_root_prefix)
then
begin
- (* Assume the user is concerned by module naming *)
+ (* Assume the user is concerned by library naming *)
if dir <> Nameops.default_root_prefix then
(Options.if_verbose warning (phys_path^" was previously bound to "
^(string_of_dirpath dir)
@@ -95,31 +99,32 @@ let load_path_of_logical_path dir =
let get_full_load_path () = List.combine (fst !load_path) (snd !load_path)
+(***********************************************************************)
(*s Modules on disk contain the following informations (after the magic
number, and before the digest). *)
type compilation_unit_name = dir_path
-type module_disk = {
+type library_disk = {
md_name : compilation_unit_name;
- md_compiled_env : compiled_env;
- md_declarations : library_segment;
+ md_compiled : compiled_library;
+ md_objects : library_objects;
md_deps : (compilation_unit_name * Digest.t) list;
md_imports : compilation_unit_name list }
(*s Modules loaded in memory contain the following informations. They are
- kept in the global table [modules_table]. *)
-
-type module_t = {
- module_name : compilation_unit_name;
- module_filename : System.physical_path;
- module_compiled_env : compiled_env;
- module_declarations : library_segment;
- module_deps : (compilation_unit_name * Digest.t) list;
- module_imports : compilation_unit_name list;
- module_digest : Digest.t }
-
-module CompUnitOrdered =
+ kept in the global table [libraries_table]. *)
+
+type library_t = {
+ library_name : compilation_unit_name;
+ library_filename : System.physical_path;
+ library_compiled : compiled_library;
+ library_objects : library_objects;
+ library_deps : (compilation_unit_name * Digest.t) list;
+ library_imports : compilation_unit_name list;
+ library_digest : Digest.t }
+
+module CompilingModuleOrdered =
struct
type t = dir_path
let compare d1 d2 =
@@ -127,33 +132,33 @@ module CompUnitOrdered =
(List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
end
-module CompUnitmap = Map.Make(CompUnitOrdered)
+module CompilingModulemap = Map.Make(CompilingModuleOrdered)
-(* This is a map from names to modules *)
-let modules_table = ref CompUnitmap.empty
+(* This is a map from names to libraries *)
+let libraries_table = ref CompilingModulemap.empty
-(* These are the _ordered_ lists of loaded, imported and exported modules *)
-let modules_loaded_list = ref []
-let modules_imports_list = ref []
-let modules_exports_list = ref []
+(* These are the _ordered_ lists of loaded, imported and exported libraries *)
+let libraries_loaded_list = ref []
+let libraries_imports_list = ref []
+let libraries_exports_list = ref []
let freeze () =
- !modules_table,
- !modules_loaded_list,
- !modules_imports_list,
- !modules_exports_list
+ !libraries_table,
+ !libraries_loaded_list,
+ !libraries_imports_list,
+ !libraries_exports_list
let unfreeze (mt,mo,mi,me) =
- modules_table := mt;
- modules_loaded_list := mo;
- modules_imports_list := mi;
- modules_exports_list := me
+ libraries_table := mt;
+ libraries_loaded_list := mo;
+ libraries_imports_list := mi;
+ libraries_exports_list := me
let init () =
- modules_table := CompUnitmap.empty;
- modules_loaded_list := [];
- modules_imports_list := [];
- modules_exports_list := []
+ libraries_table := CompilingModulemap.empty;
+ libraries_loaded_list := [];
+ libraries_imports_list := [];
+ libraries_exports_list := []
let _ =
Summary.declare_summary "MODULES"
@@ -162,40 +167,42 @@ let _ =
Summary.init_function = init;
Summary.survive_section = false }
-let find_module s =
+let find_library s =
try
- CompUnitmap.find s !modules_table
+ CompilingModulemap.find s !libraries_table
with Not_found ->
- error ("Unknown module " ^ (string_of_dirpath s))
+ error ("Unknown library " ^ (string_of_dirpath s))
-let module_is_loaded dir =
- try let _ = CompUnitmap.find dir !modules_table in true
+let library_full_filename m = (find_library m).library_filename
+
+let library_is_loaded dir =
+ try let _ = CompilingModulemap.find dir !libraries_table in true
with Not_found -> false
-let module_is_opened dir =
- List.exists (fun m -> m.module_name = dir) !modules_imports_list
+let library_is_opened dir =
+ List.exists (fun m -> m.library_name = dir) !libraries_imports_list
-let module_is_exported dir =
- List.exists (fun m -> m.module_name = dir) !modules_exports_list
+let library_is_exported dir =
+ List.exists (fun m -> m.library_name = dir) !libraries_exports_list
-let loaded_modules () =
- List.map (fun m -> m.module_name) !modules_loaded_list
+let loaded_libraries () =
+ List.map (fun m -> m.library_name) !libraries_loaded_list
-let opened_modules () =
- List.map (fun m -> m.module_name) !modules_imports_list
+let opened_libraries () =
+ List.map (fun m -> m.library_name) !libraries_imports_list
- (* If a module is loaded several time, then the first occurrence must
- be performed first, thus the modules_loaded_list ... *)
+ (* If a library is loaded several time, then the first occurrence must
+ be performed first, thus the libraries_loaded_list ... *)
-let register_loaded_module m =
+let register_loaded_library m =
let rec aux = function
| [] -> [m]
- | m'::_ as l when m'.module_name = m.module_name -> l
+ | m'::_ as l when m'.library_name = m.library_name -> l
| m'::l' -> m' :: aux l' in
- modules_loaded_list := aux !modules_loaded_list;
- modules_table := CompUnitmap.add m.module_name m !modules_table
+ libraries_loaded_list := aux !libraries_loaded_list;
+ libraries_table := CompilingModulemap.add m.library_name m !libraries_table
- (* ... while if a module is imported/exported several time, then
+ (* ... while if a library is imported/exported several time, then
only the last occurrence is really needed - though the imported
list may differ from the exported list (consider the sequence
Export A; Export B; Import A which results in A;B for exports but
@@ -204,87 +211,89 @@ let register_loaded_module m =
let rec remember_last_of_each l m =
match l with
| [] -> [m]
- | m'::l' when m'.module_name = m.module_name -> remember_last_of_each l' m
+ | m'::l' when m'.library_name = m.library_name -> remember_last_of_each l' m
| m'::l' -> m' :: remember_last_of_each l' m
-let register_open_module export m =
- modules_imports_list := remember_last_of_each !modules_imports_list m;
+let register_open_library export m =
+ libraries_imports_list := remember_last_of_each !libraries_imports_list m;
if export then
- modules_exports_list := remember_last_of_each !modules_exports_list m
-
-let compunit_cache = ref CompUnitmap.empty
-
-let module_segment = function
- | None -> contents_after None
- | Some m -> (find_module m).module_declarations
-
-let module_full_filename m = (find_module m).module_filename
-
-let vo_magic_number = 0703 (* V7.3 *)
+ libraries_exports_list := remember_last_of_each !libraries_exports_list m
-let (raw_extern_module, raw_intern_module) =
- System.raw_extern_intern vo_magic_number ".vo"
+(************************************************************************)
+(*s Operations on library objects and opening *)
-let segment_rec_iter f =
+(*let segment_rec_iter f =
let rec apply = function
| sp,Leaf obj -> f (sp,obj)
| _,OpenedSection _ -> assert false
| _,ClosedSection (_,_,seg) -> iter seg
- | _,(FrozenState _ | Module _) -> ()
+ | _,(FrozenState _ | CompilingModule _
+ | OpenedModule _ | OpenedModtype _) -> ()
and iter seg =
List.iter apply seg
in
iter
-let segment_iter f =
+let segment_iter i v f =
let rec apply = function
- | sp,Leaf obj -> f (sp,obj)
+ | sp,Leaf obj -> f (i,sp,obj)
| _,OpenedSection _ -> assert false
| sp,ClosedSection (export,dir,seg) ->
- push_section dir;
+ push_dir v dir (DirClosedSection dir);
if export then iter seg
- | _,(FrozenState _ | Module _) -> ()
+ | _,(FrozenState _ | CompilingModule _
+ | OpenedModule _ | OpenedModtype _) -> ()
and iter seg =
List.iter apply seg
in
iter
+*)
-(*s [open_module s] opens a module. The module [s] and all modules needed by
+(*s [open_library s] opens a library. The library [s] and all libraries needed by
[s] are assumed to be already loaded. When opening [s] we recursively open
- all the modules needed by [s] and tagged [exported]. *)
+ all the libraries needed by [s] and tagged [exported]. *)
-let open_objects decls =
- segment_iter open_object decls
+(*let open_objects i decls =
+ segment_iter i (Exactly i) open_object decls*)
-let open_module export m =
- if not (module_is_opened m.module_name) then
- (register_open_module export m;
- open_objects m.module_declarations)
+let open_library export m =
+ if not (library_is_opened m.library_name) then begin
+ register_open_library export m;
+ Declaremods.import_module (MPfile m.library_name)
+ end
else
if export then
- modules_exports_list := remember_last_of_each !modules_exports_list m
+ libraries_exports_list := remember_last_of_each !libraries_exports_list m
-let open_modules export modl =
+let open_libraries export modl =
let to_open_list =
List.fold_left
(fun l m ->
let subimport =
List.fold_left
- (fun l m -> remember_last_of_each l (find_module m))
- [] m.module_imports
+ (fun l m -> remember_last_of_each l (find_library m))
+ [] m.library_imports
in remember_last_of_each subimport m)
[] modl in
- List.iter (open_module export) to_open_list
+ List.iter (open_library export) to_open_list
-(*s [load_module s] loads the module [s] from the disk, and [find_module s]
- returns the module of name [s], loading it if necessary.
- The boolean [doexp] specifies if we open the modules which are declared
+
+(************************************************************************)
+(*s Loading from disk to cache (preparation phase) *)
+
+let compunit_cache = ref CompilingModulemap.empty
+
+let vo_magic_number = 0703 (* V7.3 *)
+
+let (raw_extern_library, raw_intern_library) =
+ System.raw_extern_intern vo_magic_number ".vo"
+
+(*s [load_library s] loads the library [s] from the disk, and [find_library s]
+ returns the library of name [s], loading it if necessary.
+ The boolean [doexp] specifies if we open the libraries which are declared
exported in the dependencies (it is [true] at the highest level;
then same value as for caller is reused in recursive loadings). *)
-let load_objects decls =
- segment_iter load_object decls
-
exception LibUnmappedDir
exception LibNotFound
type library_location = LibLoaded | LibInPath
@@ -292,8 +301,8 @@ type library_location = LibLoaded | LibInPath
let locate_absolute_library dir =
(* Look if loaded in current environment *)
try
- let m = CompUnitmap.find dir !modules_table in
- (dir, m.module_filename)
+ let m = CompilingModulemap.find dir !libraries_table in
+ (dir, m.library_filename)
with Not_found ->
(* Look if in loadpath *)
try
@@ -313,112 +322,94 @@ let with_magic_number_check f a =
spc () ++ str"It is corrupted" ++ spc () ++
str"or was compiled with another version of Coq.")
-let rec load_module dir =
- try
- (* Look if loaded in current env (and consequently its dependencies) *)
- CompUnitmap.find dir !modules_table
- with Not_found ->
- (* [dir] is an absolute name which matches [f] which must be in loadpath *)
- let m =
- try CompUnitmap.find dir !compunit_cache
- with Not_found ->
- anomaly ((string_of_dirpath dir)^" should be in cache")
- in
- List.iter (fun (dir,_) -> ignore (load_module dir)) m.module_deps;
- Global.import m.module_compiled_env;
- load_objects m.module_declarations;
- register_loaded_module m;
- Nametab.push_loaded_library m.module_name;
- m
-
-let mk_module md f digest = {
- module_name = md.md_name;
- module_filename = f;
- module_compiled_env = md.md_compiled_env;
- module_declarations = md.md_declarations;
- module_deps = md.md_deps;
- module_imports = md.md_imports;
- module_digest = digest }
+let mk_library md f digest = {
+ library_name = md.md_name;
+ library_filename = f;
+ library_compiled = md.md_compiled;
+ library_objects = md.md_objects;
+ library_deps = md.md_deps;
+ library_imports = md.md_imports;
+ library_digest = digest }
let intern_from_file f =
- let ch = with_magic_number_check raw_intern_module f in
+ let ch = with_magic_number_check raw_intern_library f in
let md = System.marshal_in ch in
let digest = System.marshal_in ch in
close_in ch;
- mk_module md f digest
+ mk_library md f digest
-let rec intern_module (dir, f) =
+let rec intern_library (dir, f) =
try
(* Look if in the current logical environment *)
- CompUnitmap.find dir !modules_table
+ CompilingModulemap.find dir !libraries_table
with Not_found ->
try
(* Look if already loaded in cache and consequently its dependencies *)
- CompUnitmap.find dir !compunit_cache
+ CompilingModulemap.find dir !compunit_cache
with Not_found ->
(* [dir] is an absolute name which matches [f] which must be in loadpath *)
let m = intern_from_file f in
- if dir <> m.module_name then
- errorlabstrm "load_physical_module"
- (str ("The file " ^ f ^ " contains module") ++ spc () ++
- pr_dirpath m.module_name ++ spc () ++ str "and not module" ++
+ if dir <> m.library_name then
+ errorlabstrm "load_physical_library"
+ (str ("The file " ^ f ^ " contains library") ++ spc () ++
+ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
spc() ++ pr_dirpath dir);
- compunit_cache := CompUnitmap.add dir m !compunit_cache;
- List.iter (intern_mandatory_module dir) m.module_deps;
+ compunit_cache := CompilingModulemap.add dir m !compunit_cache;
+ List.iter (intern_mandatory_library dir) m.library_deps;
m
-and intern_mandatory_module caller (dir,d) =
- let m = intern_absolute_module_from dir in
- if d <> m.module_digest then
- error ("compiled module "^(string_of_dirpath caller)^
- " makes inconsistent assumptions over module "
+and intern_mandatory_library caller (dir,d) =
+ let m = intern_absolute_library_from dir in
+ if d <> m.library_digest then
+ error ("compiled library "^(string_of_dirpath caller)^
+ " makes inconsistent assumptions over library "
^(string_of_dirpath dir))
-and intern_absolute_module_from dir =
+and intern_absolute_library_from dir =
try
- intern_module (locate_absolute_library dir)
+ intern_library (locate_absolute_library dir)
with
| LibUnmappedDir ->
let prefix, dir = fst (split_dirpath dir), string_of_dirpath dir in
- errorlabstrm "load_absolute_module_from"
+ errorlabstrm "load_absolute_library_from"
(str ("Cannot load "^dir^":") ++ spc () ++
str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
| LibNotFound ->
- errorlabstrm "load_absolute_module_from"
- (str"Cannot find module " ++ pr_dirpath dir ++ str" in loadpath")
+ errorlabstrm "load_absolute_library_from"
+ (str"Cannot find library " ++ pr_dirpath dir ++ str" in loadpath")
| e -> raise e
-let rec_intern_module mref = let _ = intern_module mref in ()
+let rec_intern_library mref = let _ = intern_library mref in ()
-let check_module_short_name f dir = function
+let check_library_short_name f dir = function
| Some id when id <> snd (split_dirpath dir) ->
- errorlabstrm "check_module_short_name"
- (str ("The file " ^ f ^ " contains module") ++ spc () ++
- pr_dirpath dir ++ spc () ++ str "and not module" ++ spc () ++
+ errorlabstrm "check_library_short_name"
+ (str ("The file " ^ f ^ " contains library") ++ spc () ++
+ pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
pr_id id)
| _ -> ()
let rec_intern_by_filename_only id f =
let m = intern_from_file f in
(* Only the base name is expected to match *)
- check_module_short_name f m.module_name id;
- (* We check no other file containing same module is loaded *)
+ check_library_short_name f m.library_name id;
+ (* We check no other file containing same library is loaded *)
try
- let m' = CompUnitmap.find m.module_name !modules_table in
+ let m' = CompilingModulemap.find m.library_name !libraries_table in
Options.if_verbose warning
- ((string_of_dirpath m.module_name)^" is already loaded from file "^
- m'.module_filename);
- m.module_name
+ ((string_of_dirpath m.library_name)^" is already loaded from file "^
+ m'.library_filename);
+ m.library_name
with Not_found ->
- compunit_cache := CompUnitmap.add m.module_name m !compunit_cache;
- List.iter (intern_mandatory_module m.module_name) m.module_deps;
- m.module_name
+ compunit_cache := CompilingModulemap.add m.library_name m !compunit_cache;
+ List.iter (intern_mandatory_library m.library_name) m.library_deps;
+ m.library_name
let locate_qualified_library qid =
(* Look if loaded in current environment *)
try
let dir = Nametab.locate_loaded_library qid in
- (LibLoaded, dir, module_full_filename dir)
+ (LibLoaded, dir, library_full_filename dir)
with Not_found ->
(* Look if in loadpath *)
try
@@ -438,7 +429,7 @@ let locate_qualified_library qid =
let rec_intern_qualified_library (loc,qid) =
try
let (_,dir,f) = locate_qualified_library qid in
- rec_intern_module (dir,f);
+ rec_intern_library (dir,f);
dir
with
| LibUnmappedDir ->
@@ -449,42 +440,79 @@ let rec_intern_qualified_library (loc,qid) =
fnl ())
| LibNotFound ->
user_err_loc (loc, "rec_intern_qualified_library",
- str"Cannot find module " ++ pr_qualid qid ++ str" in loadpath")
+ str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
-let rec_intern_module_from_file idopt f =
- (* A name is specified, we have to check it contains module id *)
+let rec_intern_library_from_file idopt f =
+ (* A name is specified, we have to check it contains library id *)
let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
rec_intern_by_filename_only idopt f
-(*s [require_module] loads and opens a module. This is a synchronized
- operation. *)
+(**********************************************************************)
+(*s [require_library] loads and opens a library. This is a synchronized
+ operation. It is performed as follows:
+
+ preparation phase: (functions require_library* ) the library and its
+ dependencies are read from to disk to the compunit_cache
+ (using intern_* )
-type module_reference = dir_path list * bool option
+ execution phase: (through add_leaf and cache_require)
+ the library is loaded in the environment and Nametab, the objects are
+ registered etc, using functions from Declaremods (via load_library,
+ which recursively loads its dependencies)
-let string_of_module (_,dir,_) = string_of_id (List.hd (repr_dirpath dir))
+
+ The [read_library] operation is very similar, but has does not "open"
+ the library
+*)
+
+type library_reference = dir_path list * bool option
+
+let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir))
+
+let rec load_library dir =
+ try
+ (* Look if loaded in current env (and consequently its dependencies) *)
+ CompilingModulemap.find dir !libraries_table
+ with Not_found ->
+ (* [dir] is an absolute name matching [f] which must be in loadpath *)
+ let m =
+ try CompilingModulemap.find dir !compunit_cache
+ with Not_found ->
+ anomaly ((string_of_dirpath dir)^" should be in cache")
+ in
+ List.iter (fun (dir,_) -> ignore (load_library dir)) m.library_deps;
+ Declaremods.register_library
+ m.library_name
+ m.library_compiled
+ m.library_objects
+ m.library_digest;
+ register_loaded_library m;
+ m
let cache_require (_,(modl,export)) =
- let ml = list_map_left load_module modl in
+ let ml = list_map_left load_library modl in
match export with
| None -> ()
- | Some export -> open_modules export ml
+ | Some export -> open_libraries export ml
+
+let load_require _ (_,(modl,_)) =
+ ignore(list_map_left load_library modl)
(* keeps the require marker for closed section replay but removes
OS dependent fields from .vo files for cross-platform compatibility *)
let export_require (l,e) = Some (l,e)
let (in_require, out_require) =
- declare_object
- ("REQUIRE",
- { cache_function = cache_require;
- load_function = (fun _ -> ());
- open_function = (fun _ -> ());
- export_function = export_require })
+ declare_object {(default_object "REQUIRE") with
+ cache_function = cache_require;
+ load_function = load_require;
+ export_function = export_require;
+ classify_function = (fun (_,o) -> Anticipate o) }
-let require_module spec qidl export =
+let require_library spec qidl export =
(*
if sections_are_opened () && Options.verbose () then
- warning ("Objets of "^(string_of_module modref)^
+ warning ("Objets of "^(string_of_library modref)^
" not surviving sections (e.g. Grammar \nand Hints)\n"^
"will be removed at the end of the section");
*)
@@ -492,53 +520,67 @@ let require_module spec qidl export =
add_anonymous_leaf (in_require (modrefl,Some export));
add_frozen_state ()
-let require_module_from_file spec idopt file export =
- let modref = rec_intern_module_from_file idopt file in
+let require_library_from_file spec idopt file export =
+ let modref = rec_intern_library_from_file idopt file in
add_anonymous_leaf (in_require ([modref],Some export));
add_frozen_state ()
-let import_module export (loc,qid) =
- let modref =
- try
- Nametab.locate_loaded_library qid
- with Not_found ->
- user_err_loc
- (loc,"import_module",
- str ((Nametab.string_of_qualid qid)^" not loaded")) in
- add_anonymous_leaf (in_require ([modref],Some export))
-
-let read_module qid =
+let export_library (loc,qid) =
+ try
+ match Nametab.locate_module qid with
+ MPfile dir ->
+ add_anonymous_leaf (in_require ([dir],Some true))
+ | _ ->
+ raise Not_found
+ with
+ Not_found ->
+ user_err_loc
+ (loc,"export_library",
+ str ((string_of_qualid qid)^" is not a loaded library"))
+
+let read_library qid =
let modref = rec_intern_qualified_library qid in
add_anonymous_leaf (in_require ([modref],None));
add_frozen_state ()
-let read_module_from_file f =
+let read_library_from_file f =
let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
let modref = rec_intern_by_filename_only None f in
add_anonymous_leaf (in_require ([modref],None));
add_frozen_state ()
-let reload_module (modrefl, export) =
+let reload_library (modrefl, export) =
add_anonymous_leaf (in_require (modrefl,export));
add_frozen_state ()
-(*s [save_module s] saves the module [m] to the disk. *)
+
+(***********************************************************************)
+(*s [save_library s] saves the library [m] to the disk. *)
+
+let start_library f =
+ let _,longf =
+ System.find_file_in_path (get_load_path ()) (f^".v") in
+ let ldir0 = find_logical_path (Filename.dirname longf) in
+ let id = id_of_string (Filename.basename f) in
+ let ldir = extend_dirpath ldir0 id in
+ Declaremods.start_library ldir;
+ ldir,longf
let current_deps () =
- List.map (fun m -> (m.module_name, m.module_digest)) !modules_loaded_list
+ List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list
let current_reexports () =
- List.map (fun m -> m.module_name) !modules_exports_list
+ List.map (fun m -> m.library_name) !libraries_exports_list
-let save_module_to s f =
- let seg = export_module s in
+let save_library_to s f =
+ let cenv, seg = Declaremods.export_library s in
let md = {
md_name = s;
- md_compiled_env = Global.export s;
- md_declarations = seg;
+ md_compiled = cenv;
+ md_objects = seg;
md_deps = current_deps ();
md_imports = current_reexports () } in
- let (f',ch) = raw_extern_module f in
+ let (f',ch) = raw_extern_library f in
try
System.marshal_out ch md;
flush ch;
@@ -547,62 +589,38 @@ let save_module_to s f =
close_out ch
with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e)
-(*s Iterators. *)
-
-let fold_all_segments insec f x =
- let rec apply acc = function
- | sp, Leaf o -> f acc sp o
- | _, ClosedSection (_,_,seg) ->
- if insec then List.fold_left apply acc seg else acc
- | _ -> acc
- in
- let acc' =
- CompUnitmap.fold
- (fun _ m acc -> List.fold_left apply acc m.module_declarations)
- !modules_table x
- in
- List.fold_left apply acc' (Lib.contents_after None)
-
-let iter_all_segments insec f =
- let rec apply = function
- | sp, Leaf o -> f sp o
- | _, ClosedSection (_,_,seg) -> if insec then List.iter apply seg
- | _ -> ()
- in
- CompUnitmap.iter
- (fun _ m -> List.iter apply m.module_declarations) !modules_table;
- List.iter apply (Lib.contents_after None)
-
-(*s Pretty-printing of modules state. *)
-
-let fmt_modules_state () =
- let opened = opened_modules ()
- and loaded = loaded_modules () in
+(*s Pretty-printing of libraries state. *)
+
+let fmt_libraries_state () =
+ let opened = opened_libraries ()
+ and loaded = loaded_libraries () in
(str "Imported (open) Modules: " ++
prlist_with_sep pr_spc pr_dirpath opened ++ fnl () ++
str "Loaded Modules: " ++
prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ())
+
(*s For tactics/commands requiring vernacular libraries *)
-let check_required_module d =
+let check_required_library d =
let d' = List.map id_of_string d in
let dir = make_dirpath (List.rev d') in
- if not (module_is_loaded dir) then
+ if not (library_is_loaded dir) then
(* Loading silently ...
let m, prefix = list_sep_last d' in
- read_module
+ read_library
(dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
*)
(* or failing ...*)
- error ("Module "^(list_last d)^" has to be required first")
+ error ("Library "^(list_last d)^" has to be required first")
+
-(*s Display the memory use of a module. *)
+(*s Display the memory use of a library. *)
open Printf
let mem s =
- let m = find_module s in
+ let m = find_library s in
h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
- (size_kb m) (size_kb m.module_compiled_env)
- (size_kb m.module_declarations)))
+ (size_kb m) (size_kb m.library_compiled)
+ (size_kb m.library_objects)))
diff --git a/library/library.mli b/library/library.mli
index dc34ec72e..43d73d241 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -11,61 +11,59 @@
(*i*)
open Util
open Names
+open Libnames
open Libobject
(*i*)
(*s This module is the heart of the library. It provides low level functions to
- load, open and save modules. Modules are saved onto the disk with checksums
+ load, open and save libraries. Modules are saved onto the disk with checksums
(obtained with the [Digest] module), which are checked at loading time to
prevent inconsistencies between files written at various dates. It also
provides a high level function [require] which corresponds to the
vernacular command [Require]. *)
-val read_module : Nametab.qualid located -> unit
-val read_module_from_file : System.physical_path -> unit
-val import_module : bool -> Nametab.qualid located -> unit
+val read_library : qualid located -> unit
-val module_is_loaded : dir_path -> bool
-val module_is_opened : dir_path -> bool
+val read_library_from_file : System.physical_path -> unit
-val loaded_modules : unit -> dir_path list
-val opened_modules : unit -> dir_path list
+val export_library : qualid located -> unit
-val fmt_modules_state : unit -> Pp.std_ppcmds
+val library_is_loaded : dir_path -> bool
+val library_is_opened : dir_path -> bool
-(*s Require. The command [require_module spec m file export] loads and opens
- a module [m]. [file] specifies the filename, if not [None]. [spec]
+val loaded_libraries : unit -> dir_path list
+val opened_libraries : unit -> dir_path list
+
+val fmt_libraries_state : unit -> Pp.std_ppcmds
+
+(*s Require. The command [require_library spec m file export] loads and opens
+ a library [m]. [file] specifies the filename, if not [None]. [spec]
specifies to look for a specification ([true]) or for an implementation
- ([false]), if not [None]. And [export] specifies if the module must be
+ ([false]), if not [None]. And [export] specifies if the library must be
exported. *)
-val require_module :
- bool option -> Nametab.qualid located list -> bool -> unit
+val require_library :
+ bool option -> qualid located list -> bool -> unit
-val require_module_from_file :
+val require_library_from_file :
bool option -> identifier option -> string -> bool -> unit
-(*s [save_module_to s f] saves the current environment as a module [s]
+(*s [save_library_to s f] saves the current environment as a library [s]
in the file [f]. *)
-val save_module_to : dir_path -> string -> unit
+val start_library : string -> dir_path * string
+val save_library_to : dir_path -> string -> unit
-(*s [module_segment m] returns the segment of the loaded module
- [m]; if not given, the segment of the current module is returned
+(*s [library_segment m] returns the segment of the loaded library
+ [m]; if not given, the segment of the current library is returned
(which is then the same as [Lib.contents_after None]).
- [module_full_filename] returns the full filename of a loaded module. *)
+*)
+(*val library_segment : dir_path option -> Lib.library_segment*)
-val module_segment : dir_path option -> Lib.library_segment
-val module_full_filename : dir_path -> string
+(* [library_full_filename] returns the full filename of a loaded library. *)
-(*s [fold_all_segments] and [iter_all_segments] iterate over all
- segments, the modules' segments first and then the current
- segment. Modules are presented in an arbitrary order. The given
- function is applied to all leaves (together with their section
- path). The boolean indicates if we must enter closed sections. *)
+val library_full_filename : dir_path -> string
-val fold_all_segments : bool -> ('a -> section_path -> obj -> 'a) -> 'a -> 'a
-val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit
(*s Global load path *)
type logical_path = dir_path
@@ -82,16 +80,16 @@ exception LibNotFound
type library_location = LibLoaded | LibInPath
val locate_qualified_library :
- Nametab.qualid -> library_location * dir_path * System.physical_path
+ qualid -> library_location * dir_path * System.physical_path
-val check_required_module : string list -> unit
-(*s Displays the memory use of a module. *)
+val check_required_library : string list -> unit
+(*s Displays the memory use of a library. *)
val mem : dir_path -> Pp.std_ppcmds
(* For discharge *)
-type module_reference
+type library_reference
-val out_require : Libobject.obj -> module_reference
-val reload_module : module_reference -> unit
+val out_require : Libobject.obj -> library_reference
+val reload_library : library_reference -> unit
diff --git a/library/nameops.ml b/library/nameops.ml
index ecbe07e77..0fd9ec0d1 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -143,12 +143,7 @@ let next_name_away name l =
| Name str -> next_ident_away str l
| Anonymous -> id_of_string "_"
-(**********************************************)
-
-let pr_dirpath sl = (str (string_of_dirpath sl))
-
-(* Operations on dirpaths *)
-let empty_dirpath = make_dirpath []
+let pr_lab l = str (string_of_label l)
let default_module_name = id_of_string "Top"
let default_module = make_dirpath [default_module_name]
@@ -157,81 +152,3 @@ let default_module = make_dirpath [default_module_name]
let coq_root = id_of_string "Coq"
let default_root_prefix = make_dirpath []
-let restrict_path n sp =
- let dir, s = repr_path sp in
- let (dir',_) = list_chop n (repr_dirpath dir) in
- Names.make_path (make_dirpath dir') s
-
-(* Pop the last n module idents *)
-let extract_dirpath_prefix n dir =
- let (_,dir') = list_chop n (repr_dirpath dir) in
- make_dirpath dir'
-
-let dirpath_prefix p = match repr_dirpath p with
- | [] -> anomaly "dirpath_prefix: empty dirpath"
- | _::l -> make_dirpath l
-
-let is_dirpath_prefix_of d1 d2 =
- list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
-
-(* To know how qualified a name should be to be understood in the current env*)
-let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
-
-let split_dirpath d =
- let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
-
-let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
-
-
-(* Section paths *)
-
-let dirpath sp = let (p,_) = repr_path sp in p
-let basename sp = let (_,id) = repr_path sp in id
-
-let path_of_constructor env ((sp,tyi),ind) =
- let mib = Environ.lookup_mind sp env in
- let mip = mib.mind_packets.(tyi) in
- let (pa,_) = repr_path sp in
- Names.make_path pa (mip.mind_consnames.(ind-1))
-
-let path_of_inductive env (sp,tyi) =
- if tyi = 0 then sp
- else
- let mib = Environ.lookup_mind sp env in
- let mip = mib.mind_packets.(tyi) in
- let (pa,_) = repr_path sp in
- Names.make_path pa (mip.mind_typename)
-
-(* parsing *)
-let parse_sp s =
- let len = String.length s in
- let rec decoupe_dirs n =
- try
- let pos = String.index_from s n '.' in
- let dir = String.sub s n (pos-n) in
- let dirs,n' = decoupe_dirs (succ pos) in
- (id_of_string dir)::dirs,n'
- with
- | Not_found -> [],n
- in
- if len = 0 then invalid_arg "parse_section_path";
- let dirs,n = decoupe_dirs 0 in
- let id = String.sub s n (len-n) in
- make_dirpath (List.rev dirs), (id_of_string id)
-
-let dirpath_of_string s =
- try
- let sl,s = parse_sp s in
- extend_dirpath sl s
- with
- | Invalid_argument _ -> invalid_arg "dirpath_of_string"
-
-let path_of_string s =
- try
- let sl,s = parse_sp s in
- make_path sl s
- with
- | Invalid_argument _ -> invalid_arg "path_of_string"
-
-(* Section paths *)
-let pr_sp sp = (str (string_of_path sp))
diff --git a/library/nameops.mli b/library/nameops.mli
index 35346b0a6..591e9030d 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -34,9 +34,11 @@ val next_name_away_with_default :
val out_name : name -> identifier
-(* Section and module mechanism: dealinng with dir paths *)
-val pr_dirpath : dir_path -> Pp.std_ppcmds
-val empty_dirpath : dir_path
+
+val pr_lab : label -> Pp.std_ppcmds
+
+(* some preset paths *)
+
val default_module : dir_path
(* This is the root of the standard library of Coq *)
@@ -45,31 +47,3 @@ val coq_root : module_ident
(* This is the default root prefix for developments which doesn't
mention a root *)
val default_root_prefix : dir_path
-
-
-val dirpath_of_string : string -> dir_path
-val path_of_string : string -> section_path
-
-val path_of_constructor : env -> constructor -> section_path
-val path_of_inductive : env -> inductive -> section_path
-
-
-val dirpath : section_path -> dir_path
-val basename : section_path -> identifier
-
-(* Give the immediate prefix of a [dir_path] *)
-val dirpath_prefix : dir_path -> dir_path
-
-(* Give the immediate prefix and basename of a [dir_path] *)
-val split_dirpath : dir_path -> dir_path * identifier
-
-val extend_dirpath : dir_path -> module_ident -> dir_path
-val add_dirpath_prefix : module_ident -> dir_path -> dir_path
-
-val extract_dirpath_prefix : int -> dir_path -> dir_path
-val is_dirpath_prefix_of : dir_path -> dir_path -> bool
-
-val restrict_path : int -> section_path -> section_path
-
-(* Section path *)
-val pr_sp : section_path -> Pp.std_ppcmds
diff --git a/library/nametab.ml b/library/nametab.ml
index b28506f91..c80675aec 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -11,23 +11,10 @@
open Util
open Pp
open Names
+open Libnames
open Nameops
open Declarations
-(*s qualified names *)
-type qualid = section_path
-
-let make_qualid = make_path
-let repr_qualid = repr_path
-
-let string_of_qualid = string_of_path
-let pr_qualid = pr_sp
-
-let qualid_of_sp sp = sp
-let make_short_qualid id = make_qualid empty_dirpath id
-let qualid_of_dirpath dir =
- let (l,a) = split_dirpath dir in
- make_qualid l a
exception GlobalizationError of qualid
exception GlobalizationConstantError of qualid
@@ -40,118 +27,150 @@ let error_global_constant_not_found_loc loc q =
let error_global_not_found q = raise (GlobalizationError q)
-(* Constructions and syntactic definitions live in the same space *)
-type global_reference =
- | VarRef of variable
- | ConstRef of constant
- | IndRef of inductive
- | ConstructRef of constructor
-
-type extended_global_reference =
- | TrueGlobal of global_reference
- | SyntacticDef of section_path
-
-let sp_of_global env = function
- | VarRef id -> make_path empty_dirpath id
- | ConstRef sp -> sp
- | IndRef (sp,tyi) ->
- (* Does not work with extracted inductive types when the first
- inductive is logic : if tyi=0 then basename sp else *)
- let mib = Environ.lookup_mind sp env in
- assert (tyi < mib.mind_ntypes && tyi >= 0);
- let mip = mib.mind_packets.(tyi) in
- let (p,_) = repr_path sp in
- make_path p mip.mind_typename
- | ConstructRef ((sp,tyi),i) ->
- let mib = Environ.lookup_mind sp env in
- assert (tyi < mib.mind_ntypes && i >= 0);
- let mip = mib.mind_packets.(tyi) in
- assert (i <= Array.length mip.mind_consnames && i > 0);
- let (p,_) = repr_path sp in
- make_path p mip.mind_consnames.(i-1)
-
+type 'a path_status = Nothing | Relative of 'a | Absolute of 'a
(* Dictionaries of short names *)
-type 'a nametree = ('a option * 'a nametree ModIdmap.t)
+type 'a nametree = ('a path_status * 'a nametree ModIdmap.t)
type ccitab = extended_global_reference nametree Idmap.t
+type kntab = kernel_name nametree Idmap.t
type objtab = section_path nametree Idmap.t
-type dirtab = dir_path nametree ModIdmap.t
+type dirtab = global_dir_reference nametree ModIdmap.t
let the_ccitab = ref (Idmap.empty : ccitab)
-let the_libtab = ref (ModIdmap.empty : dirtab)
-let the_sectab = ref (ModIdmap.empty : dirtab)
+let the_dirtab = ref (ModIdmap.empty : dirtab)
let the_objtab = ref (Idmap.empty : objtab)
+let the_modtypetab = ref (Idmap.empty : kntab)
+
+(* This table translates extended_global_references back to section paths *)
+module Globtab = Map.Make(struct type t=extended_global_reference
+ let compare = compare end)
+
+type globtab = section_path Globtab.t
+
+let the_globtab = ref (Globtab.empty : globtab)
+
+
+let sp_of_global ctx_opt ref =
+ match (ctx_opt,ref) with
+ | Some ctx, VarRef id ->
+ let _ = Sign.lookup_named id ctx in
+ make_path empty_dirpath id
+ | _ -> Globtab.find (TrueGlobal ref) !the_globtab
+
+
+let full_name = sp_of_global None
+
+let id_of_global ctx_opt ref =
+ let (_,id) = repr_path (sp_of_global ctx_opt ref) in
+ id
+
+let sp_of_syntactic_definition kn =
+ Globtab.find (SyntacticDef kn) !the_globtab
+
+(******************************************************************)
+(* the_dirpath is the table matching dir_paths to toplevel
+ modules/files or sections
+
+ If we have a closed module M having a submodule N, than N does not
+ have the entry here.
+
+*)
+
+type visibility = Until of int | Exactly of int
-let dirpath_of_reference ref =
- let sp = match ref with
- | ConstRef sp -> sp
- | VarRef id -> make_path empty_dirpath id
- | ConstructRef ((sp,_),_) -> sp
- | IndRef (sp,_) -> sp in
- let (p,_) = repr_path sp in
- p
-
-let dirpath_of_extended_ref = function
- | TrueGlobal ref -> dirpath_of_reference ref
- | SyntacticDef sp ->
- let (p,_) = repr_path sp in p
-
-(* How [visibility] works: a value of [0] means all suffixes of [dir] are
- allowed to access the object, a value of [1] means all suffixes, except the
- base name, are available, [2] means all suffixes except the base name and
- the name qualified by the module name *)
-
-(* Concretely, library roots and directory are
- always open but modules/files are open only during their interactive
- construction or on demand if a precompiled one: for a name
- "Root.Rep.Lib.name", then "Lib.name", "Rep.Lib.name" and
- "Root.Rep.Lib.name", but not "name" are pushed; which means, visibility is
- always 1 *)
-
-(* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *)
-(* We proceed in the reverse way, looking first to [id] *)
-let push_tree extract_dirpath tab visibility dir o =
- let extract = option_app (fun c -> repr_dirpath (extract_dirpath c)) in
+(* is the short name visible? tests for 1 *)
+let is_short_visible v sp = match v with
+ Until 1 | Exactly 1 -> true
+ | _ -> false
+
+(* In general, directories and sections are always open and modules
+ (and files) are open on request only *)
+
+(* We add a binding of ["modid1.....modidn.id"] to [o] in the table *)
+(* Using the fact that the reprezentation of a [dir_path] is already
+ reversed, we proceed in the reverse way, looking first for [id] *)
+
+(* [push_many] is used to register [Until vis] visibility and
+ [push_one] to [Exactly vis] and [push_tree] chooses the right one*)
+
+let push_many vis tab dir o =
let rec push level (current,dirmap) = function
| modid :: path as dir ->
let mc =
try ModIdmap.find modid dirmap
- with Not_found -> (None, ModIdmap.empty)
+ with Not_found -> (Nothing, ModIdmap.empty)
in
let this =
- if level >= visibility then
- if extract current = Some dir then
+ if level >= vis then
+ match current with
+ | Absolute _ ->
+ (* This is an absolute name, we must keep it otherwise it may
+ become unaccessible forever *)
+ warning "Trying to zaslonic an absolute name!"; current
+ | Nothing
+ | Relative _ -> Relative o
+ else current
+ in
+ (this, ModIdmap.add modid (push (level+1) mc path) dirmap)
+ | [] ->
+ match current with
+ | Absolute _ ->
(* This is an absolute name, we must keep it otherwise it may
- become unaccessible forever *)
- current
- else
- Some o
- else current in
- (this, ModIdmap.add modid (push (level+1) mc path) dirmap)
- | [] -> (Some o,dirmap) in
- push 0 tab (repr_dirpath dir)
-
-let push_idtree extract_dirpath tab n dir id o =
+ become unaccessible forever *)
+ (* But ours is also absolute! This is an error! *)
+ error "Trying to zaslonic an absolute name!"
+ | Nothing
+ | Relative _ -> Absolute o, dirmap
+ in
+ push 0 tab (repr_dirpath dir)
+
+let push_one vis tab dir o =
+ let rec push level (current,dirmap) = function
+ | modid :: path as dir ->
+ let mc =
+ try ModIdmap.find modid dirmap
+ with Not_found -> (Nothing, ModIdmap.empty)
+ in
+ if level = vis then
+ let this =
+ match current with
+ | Absolute _ ->
+ (* This is an absolute name, we must keep it otherwise it may
+ become unaccessible forever *)
+ error "Trying to zaslonic an absolute name!"
+ | Nothing
+ | Relative _ -> Relative o
+ in
+ (this, dirmap)
+ else
+ (current, ModIdmap.add modid (push (level+1) mc path) dirmap)
+ | [] -> anomaly "We should never come to this point"
+ in
+ push 0 tab (repr_dirpath dir)
+
+
+let push_tree = function
+ | Until i -> push_many (i-1)
+ | Exactly i -> push_one (i-1)
+
+
+
+let push_idtree tab visibility sp o =
+ let dir,id = repr_path sp in
let modtab =
try Idmap.find id !tab
- with Not_found -> (None, ModIdmap.empty) in
- tab := Idmap.add id (push_tree extract_dirpath modtab n dir o) !tab
+ with Not_found -> (Nothing, ModIdmap.empty) in
+ tab :=
+ Idmap.add id (push_tree visibility modtab dir o) !tab
-let push_long_names_ccipath = push_idtree dirpath_of_extended_ref the_ccitab
-let push_short_name_ccipath = push_idtree dirpath_of_extended_ref the_ccitab
-let push_long_names_objpath =
- push_idtree (fun sp -> let (p,_) = repr_path sp in p) the_objtab
-let push_short_name_objpath =
- push_idtree (fun sp -> let (p,_) = repr_path sp in p) the_objtab
-let push_modidtree tab dir id o =
+let push_modidtree tab visibility dirpath o =
+ let dir,id = split_dirpath dirpath in
let modtab =
try ModIdmap.find id !tab
- with Not_found -> (None, ModIdmap.empty) in
- tab := ModIdmap.add id (push_tree (fun x -> x) modtab 0 dir o) !tab
+ with Not_found -> (Nothing, ModIdmap.empty) in
+ tab := ModIdmap.add id (push_tree visibility modtab dir o) !tab
-let push_long_names_secpath = push_modidtree the_sectab
-let push_long_names_libpath = push_modidtree the_libtab
(* These are entry points for new declarations at toplevel *)
@@ -159,95 +178,122 @@ let push_long_names_libpath = push_modidtree the_libtab
possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom,
Parameter but also Remark and Fact) *)
-let push_cci ~visibility:n sp ref =
- let dir, s = repr_path sp in
- (* We push partially qualified name (with at least one prefix) *)
- push_long_names_ccipath n dir s (TrueGlobal ref)
+let push_xref visibility sp xref =
+ push_idtree the_ccitab visibility sp xref;
+ match visibility with
+ | Until _ ->
+ the_globtab := Globtab.add xref sp !the_globtab
+ | _ -> ()
-let push = push_cci
+let push_cci visibility sp ref =
+ push_xref visibility sp (TrueGlobal ref)
(* This is for Syntactic Definitions *)
+let push_syntactic_definition visibility sp kn =
+ push_xref visibility sp (SyntacticDef kn)
-let push_syntactic_definition sp =
- let dir, s = repr_path sp in
- push_long_names_ccipath 0 dir s (SyntacticDef sp)
+let push = push_cci
+
+let push_modtype = push_idtree the_modtypetab
-let push_short_name_syntactic_definition sp =
- let _, s = repr_qualid (qualid_of_sp sp) in
- push_short_name_ccipath Pervasives.max_int empty_dirpath s (SyntacticDef sp)
(* This is for dischargeable non-cci objects (removed at the end of the
section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
-let push_short_name_object sp =
- let _, s = repr_qualid (qualid_of_sp sp) in
- push_short_name_objpath 0 empty_dirpath s sp
+let push_object visibility sp =
+ push_idtree the_objtab visibility sp sp
(* This is for tactic definition names *)
-let push_tactic_path sp =
- let dir, s = repr_qualid (qualid_of_sp sp) in
- push_long_names_objpath 0 dir s sp
+let push_tactic = push_object
(* This is to remember absolute Section/Module names and to avoid redundancy *)
-let push_section fulldir =
- let dir, s = split_dirpath fulldir in
- (* We push all partially qualified name *)
- push_long_names_secpath dir s fulldir;
- push_long_names_secpath empty_dirpath s fulldir
-
-(* These are entry points to locate names *)
-let locate_in_tree tab dir =
- let dir = repr_dirpath dir in
+let push_dir = push_modidtree the_dirtab
+
+
+(* As before we start with generic functions *)
+
+let find_in_tree tab dir =
let rec search (current,modidtab) = function
| modid :: path -> search (ModIdmap.find modid modidtab) path
- | [] -> match current with Some o -> o | _ -> raise Not_found
+ | [] -> current
in
search tab dir
-let locate_cci (qid:qualid) =
+let find_in_idtree tab qid =
+ let (dir,id) = repr_qualid qid in
+ find_in_tree (Idmap.find id !tab) (repr_dirpath dir)
+
+let find_in_modidtree tab qid =
let (dir,id) = repr_qualid qid in
- locate_in_tree (Idmap.find id !the_ccitab) dir
+ find_in_tree (ModIdmap.find id !tab) (repr_dirpath dir)
+
+let get = function
+ Absolute o | Relative o -> o
+ | Nothing -> raise Not_found
+
+let absolute = function
+ Absolute _ -> true
+ | Relative _
+ | Nothing -> false
+
+
+(* These are entry points to locate different things *)
+let find_cci = find_in_idtree the_ccitab
+
+let find_dir = find_in_modidtree the_dirtab
+
+let find_modtype = find_in_idtree the_modtypetab
(* This should be used when syntactic definitions are allowed *)
-let extended_locate = locate_cci
+let extended_locate qid = get (find_cci qid)
(* This should be used when no syntactic definitions is expected *)
-let locate qid = match locate_cci qid with
+let locate qid = match extended_locate qid with
| TrueGlobal ref -> ref
| SyntacticDef _ -> raise Not_found
-let locate_obj qid =
- let (dir,id) = repr_qualid qid in
- locate_in_tree (Idmap.find id !the_objtab) dir
+let locate_syntactic_definition qid = match extended_locate qid with
+ | TrueGlobal _ -> raise Not_found
+ | SyntacticDef kn -> kn
-let locate_tactic qid =
- let (dir,id) = repr_qualid qid in
- locate_in_tree (Idmap.find id !the_objtab) dir
+let locate_modtype qid = get (find_modtype qid)
-(* Actually, this table has only two levels, since only basename and *)
-(* fullname are registered *)
-let push_loaded_library fulldir =
- let dir, s = split_dirpath fulldir in
- push_long_names_libpath dir s fulldir;
- push_long_names_libpath empty_dirpath s fulldir
+let locate_obj qid = get (find_in_idtree the_objtab qid)
-let locate_loaded_library qid =
- let (dir,id) = repr_qualid qid in
- locate_in_tree (ModIdmap.find id !the_libtab) dir
+let locate_tactic qid = get (find_in_idtree the_objtab qid)
+
+let locate_dir qid = get (find_dir qid)
+
+let locate_module qid =
+ match locate_dir qid with
+ | DirModule (_,(mp,_)) -> mp
+ | _ -> raise Not_found
+
+let locate_loaded_library qid =
+ match locate_dir qid with
+ | DirModule (dir,_) -> dir
+ | _ -> raise Not_found
let locate_section qid =
- let (dir,id) = repr_qualid qid in
- locate_in_tree (ModIdmap.find id !the_sectab) dir
+ match locate_dir qid with
+ | DirOpenSection (dir, _)
+ | DirClosedSection dir -> dir
+ | _ -> raise Not_found
(* Derived functions *)
let locate_constant qid =
- (* TODO: restrict to defined constants *)
- match locate_cci qid with
- | TrueGlobal (ConstRef sp) -> sp
+ match extended_locate qid with
+ | TrueGlobal (ConstRef kn) -> kn
+ | _ -> raise Not_found
+
+let locate_mind qid =
+ match extended_locate qid with
+ | TrueGlobal (IndRef (kn,0)) -> kn
| _ -> raise Not_found
+(*
let sp_of_id id = match locate_cci (make_short_qualid id) with
| TrueGlobal ref -> ref
| SyntacticDef _ ->
@@ -258,14 +304,11 @@ let constant_sp_of_id id =
match locate_cci (make_short_qualid id) with
| TrueGlobal (ConstRef sp) -> sp
| _ -> raise Not_found
+*)
let absolute_reference sp =
- let a = locate_cci sp in
- let (p,_) = repr_path sp in
- if not (dirpath_of_extended_ref a = p) then
- anomaly ("Not an absolute path: "^(string_of_path sp));
- match a with
- | TrueGlobal ref -> ref
+ match find_cci (qualid_of_sp sp) with
+ | Absolute (TrueGlobal ref) -> ref
| _ -> raise Not_found
let locate_in_absolute_module dir id =
@@ -282,13 +325,23 @@ let global (loc,qid) =
error_global_not_found_loc loc qid
let exists_cci sp =
- try let _ = locate_cci sp in true
+ try
+ absolute (find_cci (qualid_of_sp sp))
with Not_found -> false
-
-let exists_section dir =
- try let _ = locate_section (qualid_of_dirpath dir) in true
+
+let exists_dir dir =
+ try
+ absolute (find_dir (qualid_of_dirpath dir))
with Not_found -> false
+let exists_section = exists_dir
+
+let exists_module = exists_dir
+
+let exists_modtype sp =
+ try
+ absolute (find_modtype (qualid_of_sp sp))
+ with Not_found -> false
(* For a sp Coq.A.B.x, try to find the shortest among x, B.x, A.B.x
and Coq.A.B.x is a qualid that denotes the same object. *)
@@ -323,25 +376,25 @@ let global_inductive (loc,qid as locqid) =
(********************************************************************)
(* Registration of tables as a global table and rollback *)
-type frozen = ccitab * dirtab * dirtab * objtab * identifier list
+type frozen = ccitab * dirtab * objtab * globtab
let init () =
the_ccitab := Idmap.empty;
- the_libtab := ModIdmap.empty;
- the_sectab := ModIdmap.empty;
- the_objtab := Idmap.empty
+ the_dirtab := ModIdmap.empty;
+ the_objtab := Idmap.empty;
+ the_globtab := Globtab.empty
let freeze () =
!the_ccitab,
- !the_libtab,
- !the_sectab,
- !the_objtab
+ !the_dirtab,
+ !the_objtab,
+ !the_globtab
-let unfreeze (mc,ml,ms,mo) =
+let unfreeze (mc,md,mo,gt) =
the_ccitab := mc;
- the_libtab := ml;
- the_sectab := ms;
- the_objtab := mo
+ the_dirtab := md;
+ the_objtab := mo;
+ the_globtab := gt
let _ =
Summary.declare_summary "names"
@@ -350,7 +403,3 @@ let _ =
Summary.init_function = init;
Summary.survive_section = false }
-type strength =
- | NotDeclare
- | DischargeAt of dir_path * int
- | NeverDischarge
diff --git a/library/nametab.mli b/library/nametab.mli
index d71e3e379..b64fe0d9d 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -12,44 +12,49 @@
open Util
open Pp
open Names
+open Libnames
(*i*)
-(*s This module contains the table for globalization, which associates global
- names (section paths) to qualified names. *)
+(*s This module contains the tables for globalization, which
+ associates internal object references to qualified names (qualid). *)
-type global_reference =
- | VarRef of variable
- | ConstRef of constant
- | IndRef of inductive
- | ConstructRef of constructor
+(* Most functions in this module fall into one of the following categories:
+ \begin{itemize}
+ \item [push : visibility -> full_user_name -> object_reference -> unit]
+
+ Registers the [object_reference] to be referred to by the
+ [full_user_name] (and its suffixes according to [visibility])
-(* Finds the real name of a global (e.g. fetch the constructor names
- from the inductive name and constructor number) *)
-val sp_of_global : Environ.env -> global_reference -> section_path
-
-type extended_global_reference =
- | TrueGlobal of global_reference
- | SyntacticDef of section_path
+ \item [exists : full_user_name -> bool]
+
+ Is the [full_user_name] already atributed as an absolute user name
+ of some object?
-(*s A [qualid] is a partially qualified ident; it includes fully
- qualified names (= absolute names) and all intermediate partial
- qualifications of absolute names, including single identifiers *)
-type qualid
+ \item [locate : qualid -> object_reference]
-val make_qualid : dir_path -> identifier -> qualid
-val repr_qualid : qualid -> dir_path * identifier
-val make_short_qualid : identifier -> qualid
+ Finds the object referred to by [qualid] or raises Not_found
+
+ \item [name_of] : object_reference -> user_name
-val string_of_qualid : qualid -> string
-val pr_qualid : qualid -> std_ppcmds
+ The [user_name] can be for example the shortest non ambiguous [qualid] or
+ the [full_user_name] or [identifier]. Such a function can also have a
+ local context argument.
+*)
+
+
-val qualid_of_sp : section_path -> qualid
+(* Finds the real name of a global (e.g. fetch the constructor names
+ from the inductive name and constructor number) *)
+val sp_of_global : Sign.named_context option -> global_reference -> section_path
+val sp_of_syntactic_definition : kernel_name -> section_path
(* Turns an absolute name into a qualified name denoting the same name *)
-val shortest_qualid_of_global : Environ.env -> global_reference -> qualid
+val full_name : global_reference -> section_path
+val shortest_qualid_of_global : Sign.named_context option -> global_reference -> qualid
+val id_of_global : Sign.named_context option -> global_reference -> identifier
(* Printing of global references using names as short as possible *)
-val pr_global_env : Environ.env -> global_reference -> std_ppcmds
+val pr_global_env : Sign.named_context option -> global_reference -> std_ppcmds
exception GlobalizationError of qualid
exception GlobalizationConstantError of qualid
@@ -59,29 +64,29 @@ val error_global_not_found_loc : loc -> qualid -> 'a
val error_global_not_found : qualid -> 'a
val error_global_constant_not_found_loc : loc -> qualid -> 'a
-(*s Register visibility of absolute paths by qualified names *)
-val push : visibility:int -> section_path -> global_reference -> unit
-val push_syntactic_definition : section_path -> unit
+(*s Register visibility of things *)
-(*s Register visibility of absolute paths by short names *)
-val push_short_name_syntactic_definition : section_path -> unit
-val push_short_name_object : section_path -> unit
+(* The visibility can be registered either for all suffixes not
+ shorter then a given int - when the object is loaded inside a module,
+ or for a precise suffix, when the module containing (the module
+ containing ...) the object is open (imported) *)
-(*s Register visibility of absolute paths by short names *)
-val push_tactic_path : section_path -> unit
-val locate_tactic : qualid -> section_path
+type visibility = Until of int | Exactly of int
-(*s Register visibility by all qualifications *)
-val push_section : dir_path -> unit
+(* is the short name visible? tests for 1 *)
+val is_short_visible : visibility -> section_path -> bool
-(* This should eventually disappear *)
-val sp_of_id : identifier -> global_reference
+val push : visibility -> section_path -> global_reference -> unit
+val push_syntactic_definition :
+ visibility -> section_path -> kernel_name -> unit
+val push_modtype : visibility -> section_path -> kernel_name -> unit
+val push_dir : visibility -> dir_path -> global_dir_reference -> unit
+val push_object : visibility -> section_path -> unit
+val push_tactic : visibility -> section_path -> unit
(*s The following functions perform globalization of qualified names *)
(* This returns the section path of a constant or fails with [Not_found] *)
-val constant_sp_of_id : identifier -> section_path
-
val locate : qualid -> global_reference
(* This function is used to transform a qualified identifier into a
@@ -97,11 +102,23 @@ val extended_locate : qualid -> extended_global_reference
val locate_obj : qualid -> section_path
val locate_constant : qualid -> constant
+val locate_mind : qualid -> mutual_inductive
val locate_section : qualid -> dir_path
+val locate_modtype : qualid -> kernel_name
+val locate_syntactic_definition : qualid -> kernel_name
+
+val locate_tactic : qualid -> section_path
+val locate_dir : qualid -> global_dir_reference
+val locate_module : qualid -> module_path
(* [exists sp] tells if [sp] is already bound to a cci term *)
val exists_cci : section_path -> bool
-val exists_section : dir_path -> bool
+val exists_modtype : section_path -> bool
+
+(* Those three functions are the same *)
+val exists_dir : dir_path -> bool
+val exists_section : dir_path -> bool (* deprecated *)
+val exists_module : dir_path -> bool (* deprecated *)
(*s Roots of the space of absolute names *)
@@ -114,10 +131,10 @@ val absolute_reference : section_path -> global_reference
one of its section/subsection *)
val locate_in_absolute_module : dir_path -> identifier -> global_reference
-val push_loaded_library : dir_path -> unit
val locate_loaded_library : qualid -> dir_path
-type strength =
- | NotDeclare
- | DischargeAt of dir_path * int
- | NeverDischarge
+type frozen
+
+val freeze : unit -> frozen
+val unfreeze : frozen -> unit
+
diff --git a/library/summary.ml b/library/summary.ml
index 210a1a81b..59560af22 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -10,7 +10,6 @@
open Pp
open Util
-open Names
type 'a summary_declaration = {
freeze_function : unit -> 'a;
@@ -21,8 +20,8 @@ type 'a summary_declaration = {
let summaries =
(Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
-let declare_summary sumname sdecl =
- let (infun,outfun) = Dyn.create (sumname^"-SUMMARY") in
+let internal_declare_summary sumname sdecl =
+ let (infun,outfun) = Dyn.create sumname in
let dyn_freeze () = infun (sdecl.freeze_function())
and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
and dyn_init = sdecl.init_function in
@@ -37,6 +36,14 @@ let declare_summary sumname sdecl =
(str "Cannot declare a summary twice: " ++ str sumname);
Hashtbl.add summaries sumname ddecl
+let declare_summary sumname decl =
+ internal_declare_summary (sumname^"-SUMMARY") decl
+
+let envsummary = "Global environment SUMMARY"
+
+let declare_global_environment sdecl =
+ internal_declare_summary envsummary sdecl
+
type frozen = Dyn.t Stringmap.t
let freeze_summaries () =
@@ -62,5 +69,14 @@ let unfreeze_lost_summaries fs =
with Not_found -> decl.init_function())
summaries
+let unfreeze_other_summaries fs =
+ Hashtbl.iter
+ (fun id decl ->
+ try
+ if id <> envsummary then
+ decl.unfreeze_function (Stringmap.find id fs)
+ with Not_found -> decl.init_function())
+ summaries
+
let init_summaries () =
Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
diff --git a/library/summary.mli b/library/summary.mli
index d381543b9..781b31144 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -10,6 +10,7 @@
(*i*)
open Names
+open Libnames
(*i*)
(* This module registers the declaration of global tables, which will be kept
@@ -22,12 +23,14 @@ type 'a summary_declaration = {
survive_section : bool }
val declare_summary : string -> 'a summary_declaration -> unit
+val declare_global_environment : 'a summary_declaration -> unit
type frozen
val freeze_summaries : unit -> frozen
val unfreeze_summaries : frozen -> unit
val unfreeze_lost_summaries : frozen -> unit
+val unfreeze_other_summaries : frozen -> unit
val init_summaries : unit -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 22:51:39 +0000