aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.mli16
-rw-r--r--library/decls.mli2
-rw-r--r--library/globnames.ml20
-rw-r--r--library/globnames.mli4
-rw-r--r--library/goptions.ml4
-rw-r--r--library/keys.ml13
-rw-r--r--library/lib.ml8
-rw-r--r--library/libnames.mli4
-rw-r--r--library/libobject.ml43
-rw-r--r--library/libobject.mli45
-rw-r--r--library/library.mli4
-rw-r--r--library/nametab.ml16
-rw-r--r--library/nametab.mli14
-rw-r--r--library/summary.ml2
-rw-r--r--library/summary.mli4
15 files changed, 142 insertions, 57 deletions
diff --git a/library/coqlib.mli b/library/coqlib.mli
index 351a0a7e84..f6779dbbde 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -190,12 +190,18 @@ val build_bool_type : coq_bool_data delayed
val build_prod : coq_sigma_data delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
-val build_coq_eq : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *)
+val build_coq_eq : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
-val build_coq_eq_refl : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *)
+(** = [(build_coq_eq_data()).eq] *)
+
+val build_coq_eq_refl : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
-val build_coq_eq_sym : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *)
+(** = [(build_coq_eq_data()).refl] *)
+
+val build_coq_eq_sym : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
+(** = [(build_coq_eq_data()).sym] *)
+
val build_coq_f_equal2 : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
@@ -222,8 +228,8 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed
val build_coq_sumbool : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
-(** {6 ... } *)
-(** Connectives
+(** {6 ... }
+ Connectives
The False proposition *)
val build_coq_False : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
diff --git a/library/decls.mli b/library/decls.mli
index 401884736e..c0db537427 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -19,7 +19,7 @@ open Decl_kinds
(** Registration and access to the table of variable *)
type variable_data =
- DirPath.t * bool (** opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
+ DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
val add_variable_data : variable -> variable_data -> unit
val variable_path : variable -> DirPath.t
diff --git a/library/globnames.ml b/library/globnames.ml
index 9aca7788d2..db2e8bfaed 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -31,8 +31,8 @@ let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destCon
let subst_constructor subst (ind,j as ref) =
let ind' = subst_ind subst ind in
- if ind==ind' then ref, mkConstruct ref
- else (ind',j), mkConstruct (ind',j)
+ if ind==ind' then ref
+ else (ind',j)
let subst_global_reference subst ref = match ref with
| VarRef var -> ref
@@ -43,20 +43,20 @@ let subst_global_reference subst ref = match ref with
let ind' = subst_ind subst ind in
if ind==ind' then ref else IndRef ind'
| ConstructRef ((kn,i),j as c) ->
- let c',t = subst_constructor subst c in
- if c'==c then ref else ConstructRef c'
+ let c' = subst_constructor subst c in
+ if c'==c then ref else ConstructRef c'
let subst_global subst ref = match ref with
- | VarRef var -> ref, mkVar var
+ | VarRef var -> ref, None
| ConstRef kn ->
- let kn',t = subst_con_kn subst kn in
- if kn==kn' then ref, mkConst kn else ConstRef kn', t
+ let kn',t = subst_con subst kn in
+ if kn==kn' then ref, None else ConstRef kn', t
| IndRef ind ->
let ind' = subst_ind subst ind in
- if ind==ind' then ref, mkInd ind else IndRef ind', mkInd ind'
+ if ind==ind' then ref, None else IndRef ind', None
| ConstructRef ((kn,i),j as c) ->
- let c',t = subst_constructor subst c in
- if c'==c then ref,t else ConstructRef c', t
+ let c' = subst_constructor subst c in
+ if c'==c then ref,None else ConstructRef c', None
let canonical_gr = function
| ConstRef con -> ConstRef(Constant.make1 (Constant.canonical con))
diff --git a/library/globnames.mli b/library/globnames.mli
index a96a42ced2..d49ed453f5 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -36,8 +36,8 @@ val destConstructRef : GlobRef.t -> constructor
val is_global : GlobRef.t -> constr -> bool
-val subst_constructor : substitution -> constructor -> constructor * constr
-val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr
+val subst_constructor : substitution -> constructor -> constructor
+val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
(** This constr is not safe to be typechecked, universe polymorphism is not
diff --git a/library/goptions.ml b/library/goptions.ml
index 98efb512ab..340d74151b 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -246,14 +246,14 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
| OptGlobal -> cache_options o
| OptExport -> ()
| OptLocal | OptDefault ->
- (** Ruled out by classify_function *)
+ (* Ruled out by classify_function *)
assert false
in
let open_options i (_, (l, _, _) as o) = match l with
| OptExport -> if Int.equal i 1 then cache_options o
| OptGlobal -> ()
| OptLocal | OptDefault ->
- (** Ruled out by classify_function *)
+ (* Ruled out by classify_function *)
assert false
in
let subst_options (subst,obj) = obj in
diff --git a/library/keys.ml b/library/keys.ml
index 53447a679a..58883ccc88 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -100,18 +100,13 @@ let discharge_keys (_,(k,k')) =
| Some x, Some y -> Some (x, y)
| _ -> None
-let rebuild_keys (ref,ref') = (ref, ref')
-
type key_obj = key * key
let inKeys : key_obj -> obj =
- declare_object {(default_object "KEYS") with
- cache_function = cache_keys;
- load_function = load_keys;
- subst_function = subst_keys;
- classify_function = (fun x -> Substitute x);
- discharge_function = discharge_keys;
- rebuild_function = rebuild_keys }
+ declare_object @@ superglobal_object "KEYS"
+ ~cache:cache_keys
+ ~subst:(Some subst_keys)
+ ~discharge:discharge_keys
let declare_equiv_keys ref ref' =
Lib.add_anonymous_leaf (inKeys (ref,ref'))
diff --git a/library/lib.ml b/library/lib.ml
index 9c13cdafdb..cce5feeb4a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -481,8 +481,8 @@ let named_of_variable_context =
List.map fst
let name_instance inst =
- (** FIXME: this should probably be done at an upper level, by storing the
- name information in the section data structure. *)
+ (* FIXME: this should probably be done at an upper level, by storing the
+ name information in the section data structure. *)
let map lvl = match Univ.Level.name lvl with
| None -> (* Having Prop/Set/Var as section universes makes no sense *)
assert false
@@ -491,8 +491,8 @@ let name_instance inst =
let qid = Nametab.shortest_qualid_of_universe na in
Name (Libnames.qualid_basename qid)
with Not_found ->
- (** Best-effort naming from the string representation of the level.
- See univNames.ml for a similar hack. *)
+ (* Best-effort naming from the string representation of the level.
+ See univNames.ml for a similar hack. *)
Name (Id.of_string_soft (Univ.Level.to_string lvl))
in
Array.map map (Univ.Instance.to_array inst)
diff --git a/library/libnames.mli b/library/libnames.mli
index 9960603cbb..bbb4d2a058 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -94,8 +94,8 @@ val qualid_basename : qualid -> Id.t
val default_library : DirPath.t
(** This is the root of the standard library of Coq *)
-val coq_root : module_ident (** "Coq" *)
-val coq_string : string (** "Coq" *)
+val coq_root : module_ident (* "Coq" *)
+val coq_string : string (* "Coq" *)
(** This is the default root prefix for developments which doesn't
mention a root *)
diff --git a/library/libobject.ml b/library/libobject.ml
index c153e9a09a..3d17b4a605 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -129,3 +129,46 @@ let rebuild_object lobj =
apply_dyn_fun (fun d -> d.dyn_rebuild_function lobj) lobj
let dump = Dyn.dump
+
+let local_object_nodischarge s ~cache =
+ { (default_object s) with
+ cache_function = cache;
+ classify_function = (fun _ -> Dispose);
+ }
+
+let local_object s ~cache ~discharge =
+ { (local_object_nodischarge s ~cache) with
+ discharge_function = discharge }
+
+let global_object_nodischarge s ~cache ~subst =
+ let import i o = if Int.equal i 1 then cache o in
+ { (default_object s) with
+ cache_function = cache;
+ open_function = import;
+ subst_function = (match subst with
+ | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")
+ | Some subst -> subst;
+ );
+ classify_function =
+ if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o);
+ }
+
+let global_object s ~cache ~subst ~discharge =
+ { (global_object_nodischarge s ~cache ~subst) with
+ discharge_function = discharge }
+
+let superglobal_object_nodischarge s ~cache ~subst =
+ { (default_object s) with
+ load_function = (fun _ x -> cache x);
+ cache_function = cache;
+ subst_function = (match subst with
+ | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")
+ | Some subst -> subst;
+ );
+ classify_function =
+ if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o);
+ }
+
+let superglobal_object s ~cache ~subst ~discharge =
+ { (superglobal_object_nodischarge s ~cache ~subst) with
+ discharge_function = discharge }
diff --git a/library/libobject.mli b/library/libobject.mli
index 32ffc5b79e..00515bd273 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -119,6 +119,51 @@ val classify_object : obj -> obj substitutivity
val discharge_object : object_name * obj -> obj option
val rebuild_object : obj -> obj
+(** Higher-level API for objects with fixed scope.
+
+- Local means that the object cannot be imported from outside.
+- Global means that it can be imported (by importing the module that contains the
+object).
+- Superglobal means that the object survives to closing a module, and is imported
+when the file which contains it is Required (even without Import).
+- With the nodischarge variants, the object does not survive section closing.
+ With the normal variants, it does.
+
+We recommend to avoid declaring superglobal objects and using the nodischarge
+variants.
+*)
+
+val local_object : string ->
+ cache:(object_name * 'a -> unit) ->
+ discharge:(object_name * 'a -> 'a option) ->
+ 'a object_declaration
+
+val local_object_nodischarge : string ->
+ cache:(object_name * 'a -> unit) ->
+ 'a object_declaration
+
+val global_object : string ->
+ cache:(object_name * 'a -> unit) ->
+ subst:(Mod_subst.substitution * 'a -> 'a) option ->
+ discharge:(object_name * 'a -> 'a option) ->
+ 'a object_declaration
+
+val global_object_nodischarge : string ->
+ cache:(object_name * 'a -> unit) ->
+ subst:(Mod_subst.substitution * 'a -> 'a) option ->
+ 'a object_declaration
+
+val superglobal_object : string ->
+ cache:(object_name * 'a -> unit) ->
+ subst:(Mod_subst.substitution * 'a -> 'a) option ->
+ discharge:(object_name * 'a -> 'a option) ->
+ 'a object_declaration
+
+val superglobal_object_nodischarge : string ->
+ cache:(object_name * 'a -> unit) ->
+ subst:(Mod_subst.substitution * 'a -> 'a) option ->
+ 'a object_declaration
+
(** {6 Debug} *)
val dump : unit -> (int * string) list
diff --git a/library/library.mli b/library/library.mli
index d298a371b5..c016352808 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -19,8 +19,8 @@ open Libnames
written at various dates.
*)
-(** {6 ... } *)
-(** Require = load in the environment + open (if the optional boolean
+(** {6 ... }
+ Require = load in the environment + open (if the optional boolean
is not [None]); mark also for export if the boolean is [Some true] *)
val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
diff --git a/library/nametab.ml b/library/nametab.ml
index e29c7b2960..95890b2edf 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -107,6 +107,7 @@ module type NAMETREE = sig
val user_name : qualid -> t -> user_name
val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
val find_prefixes : qualid -> t -> elt list
+
(** Matches a prefix of [qualid], useful for completion *)
val match_prefixes : qualid -> t -> elt list
end
@@ -347,12 +348,10 @@ module DirTab = Make(DirPath')(GlobDirRef)
type dirtab = DirTab.t
let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
-type universe_id = DirPath.t * int
-
module UnivIdEqual =
struct
- type t = universe_id
- let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+ type t = Univ.Level.UGlobal.t
+ let equal = Univ.Level.UGlobal.equal
end
module UnivTab = Make(FullPath)(UnivIdEqual)
type univtab = UnivTab.t
@@ -375,12 +374,9 @@ let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevt
module UnivIdOrdered =
struct
- type t = universe_id
- let hash (d, i) = i + DirPath.hash d
- let compare (d, i) (d', i') =
- let c = Int.compare i i' in
- if Int.equal c 0 then DirPath.compare d d'
- else c
+ type t = Univ.Level.UGlobal.t
+ let hash = Univ.Level.UGlobal.hash
+ let compare = Univ.Level.UGlobal.compare
end
module UnivIdMap = HMap.Make(UnivIdOrdered)
diff --git a/library/nametab.mli b/library/nametab.mli
index 24af07619d..fccb8fd918 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -120,11 +120,9 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit
val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
val push_syndef : visibility -> full_path -> syndef_name -> unit
-type universe_id = DirPath.t * int
+module UnivIdMap : CMap.ExtS with type key = Univ.Level.UGlobal.t
-module UnivIdMap : CMap.ExtS with type key = universe_id
-
-val push_universe : visibility -> full_path -> universe_id -> unit
+val push_universe : visibility -> full_path -> Univ.Level.UGlobal.t -> unit
(** {6 The following functions perform globalization of qualified names } *)
@@ -139,7 +137,7 @@ val locate_modtype : qualid -> ModPath.t
val locate_dir : qualid -> GlobDirRef.t
val locate_module : qualid -> ModPath.t
val locate_section : qualid -> DirPath.t
-val locate_universe : qualid -> universe_id
+val locate_universe : qualid -> Univ.Level.UGlobal.t
(** These functions globalize user-level references into global
references, like [locate] and co, but raise a nice error message
@@ -173,7 +171,9 @@ val exists_cci : full_path -> bool
val exists_modtype : full_path -> bool
val exists_dir : DirPath.t -> bool
val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+
val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+
val exists_universe : full_path -> bool
(** {6 These functions locate qualids into full user names } *)
@@ -196,7 +196,7 @@ val path_of_modtype : ModPath.t -> full_path
(** A universe_id might not be registered with a corresponding user name.
@raise Not_found if the universe was not introduced by the user. *)
-val path_of_universe : universe_id -> full_path
+val path_of_universe : Univ.Level.UGlobal.t -> full_path
(** Returns in particular the dirpath or the basename of the full path
associated to global reference *)
@@ -218,7 +218,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
(** Deprecated synonyms *)
diff --git a/library/summary.ml b/library/summary.ml
index 9b22945919..b68f1fb01b 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -92,7 +92,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
| None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
| Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module
end;
- (** We must be independent on the order of the map! *)
+ (* We must be independent on the order of the map! *)
let ufz name decl =
try decl.unfreeze_function String.Map.(find name summaries)
with Not_found ->
diff --git a/library/summary.mli b/library/summary.mli
index 7d91a79188..64222761ba 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -19,9 +19,9 @@ type marshallable =
(** Types of global Coq states. The ['a] type should be pure and marshallable by
the standard OCaml marshalling function. *)
type 'a summary_declaration = {
- (** freeze_function [true] is for marshalling to disk.
- * e.g. lazy must be forced *)
freeze_function : marshallable -> 'a;
+ (** freeze_function [true] is for marshalling to disk.
+ * e.g. lazy must be forced *)
unfreeze_function : 'a -> unit;
init_function : unit -> unit }
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 02:38:52 +0000