aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.mli16
-rw-r--r--library/decl_kinds.ml1
-rw-r--r--library/declaremods.ml2
-rw-r--r--library/decls.mli2
-rw-r--r--library/global.ml7
-rw-r--r--library/globnames.ml20
-rw-r--r--library/globnames.mli4
-rw-r--r--library/goptions.ml6
-rw-r--r--library/keys.ml13
-rw-r--r--library/lib.ml35
-rw-r--r--library/lib.mli5
-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.ml1
-rw-r--r--library/nametab.mli2
-rw-r--r--library/states.ml8
-rw-r--r--library/states.mli4
-rw-r--r--library/summary.ml18
-rw-r--r--library/summary.mli15
21 files changed, 171 insertions, 84 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/decl_kinds.ml b/library/decl_kinds.ml
index c1a673edf0..171d51800e 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -57,7 +57,6 @@ type assumption_object_kind = Definitional | Logical | Conjectural
*)
type assumption_kind = locality * polymorphic * assumption_object_kind
-
type definition_kind = locality * polymorphic * definition_object_kind
(** Kinds used in proofs *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index d20775a0d7..8699583cdf 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -845,7 +845,7 @@ end
(** {6 Module operations handling summary freeze/unfreeze} *)
let protect_summaries f =
- let fs = Summary.freeze_summaries ~marshallable:`No in
+ let fs = Summary.freeze_summaries ~marshallable:false in
try f fs
with reraise ->
(* Something wrong: undo the whole process *)
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/global.ml b/library/global.ml
index 67b00cf411..84d2a37170 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -36,10 +36,9 @@ let is_joined_environment () =
let global_env_summary_tag =
Summary.declare_summary_tag global_env_summary_name
- { Summary.freeze_function = (function
- | `Yes -> join_safe_environment (); !global_env
- | `No -> !global_env
- | `Shallow -> !global_env);
+ { Summary.freeze_function = (fun ~marshallable -> if marshallable then
+ (join_safe_environment (); !global_env)
+ else !global_env);
unfreeze_function = (fun fr -> global_env := fr);
init_function = (fun () -> global_env := Safe_typing.empty_environment) }
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..1b907fd966 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -235,7 +235,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
let default = read() in
let change =
let _ = Summary.declare_summary (nickname key)
- { Summary.freeze_function = (fun _ -> read ());
+ { Summary.freeze_function = (fun ~marshallable -> read ());
Summary.unfreeze_function = write;
Summary.init_function = (fun () -> write default) } in
let cache_options (_,(l,m,v)) =
@@ -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..d4381a6923 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)
@@ -571,7 +571,7 @@ let open_section id =
let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
if Nametab.exists_section obj_dir then
user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
- let fs = Summary.freeze_summaries ~marshallable:`No in
+ let fs = Summary.freeze_summaries ~marshallable:false in
add_entry (make_foname id) (OpenedSection (prefix, fs));
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
@@ -608,24 +608,21 @@ let close_section () =
type frozen = lib_state
-let freeze ~marshallable =
- match marshallable with
- | `Shallow ->
- (* TASSI: we should do something more sensible here *)
- let lib_stk =
- CList.map_filter (function
+let freeze ~marshallable = !lib_state
+
+let unfreeze st = lib_state := st
+
+let drop_objects st =
+ let lib_stk =
+ CList.map_filter (function
| _, Leaf _ -> None
| n, (CompilingLibrary _ as x) -> Some (n,x)
| n, OpenedModule (it,e,op,_) ->
- Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
+ Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
| n, OpenedSection (op, _) ->
- Some(n,OpenedSection(op,Summary.empty_frozen)))
- !lib_state.lib_stk in
- { !lib_state with lib_stk }
- | _ ->
- !lib_state
-
-let unfreeze st = lib_state := st
+ Some(n,OpenedSection(op,Summary.empty_frozen)))
+ st.lib_stk in
+ { st with lib_stk }
let init () =
unfreeze initial_lib_state;
diff --git a/library/lib.mli b/library/lib.mli
index d1b4977dd5..30569197bc 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -148,9 +148,12 @@ val close_section : unit -> unit
type frozen
-val freeze : marshallable:Summary.marshallable -> frozen
+val freeze : marshallable:bool -> frozen
val unfreeze : frozen -> unit
+(** Keep only the libobject structure, not the objects themselves *)
+val drop_objects : frozen -> frozen
+
val init : unit -> unit
(** {6 Section management for discharge } *)
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 f0f643d9b5..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
diff --git a/library/nametab.mli b/library/nametab.mli
index b7926cf515..fccb8fd918 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -171,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 } *)
diff --git a/library/states.ml b/library/states.ml
index ae45b18b9c..92bdc410a3 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -13,8 +13,10 @@ open System
type state = Lib.frozen * Summary.frozen
+let lib_of_state = fst
let summary_of_state = snd
-let replace_summary (lib,_) s = lib, s
+let replace_summary (lib,_) st = lib, st
+let replace_lib (_,st) lib = lib, st
let freeze ~marshallable =
(Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
@@ -24,7 +26,7 @@ let unfreeze (fl,fs) =
Summary.unfreeze_summaries fs
let extern_state s =
- System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes)
+ System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true)
let intern_state s =
unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
@@ -33,7 +35,7 @@ let intern_state s =
(* Rollback. *)
let with_state_protection f x =
- let st = freeze ~marshallable:`No in
+ let st = freeze ~marshallable:false in
try
let a = f x in unfreeze st; a
with reraise ->
diff --git a/library/states.mli b/library/states.mli
index 1e0361ea4f..52feb95222 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -19,11 +19,13 @@ val intern_state : string -> unit
val extern_state : string -> unit
type state
-val freeze : marshallable:Summary.marshallable -> state
+val freeze : marshallable:bool -> state
val unfreeze : state -> unit
val summary_of_state : state -> Summary.frozen
+val lib_of_state : state -> Lib.frozen
val replace_summary : state -> Summary.frozen -> state
+val replace_lib : state -> Lib.frozen -> state
(** {6 Rollback } *)
diff --git a/library/summary.ml b/library/summary.ml
index 9b22945919..8fbca44353 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -14,10 +14,8 @@ open Util
module Dyn = Dyn.Make ()
-type marshallable = [ `Yes | `No | `Shallow ]
-
type 'a summary_declaration = {
- freeze_function : marshallable -> 'a;
+ freeze_function : marshallable:bool -> 'a;
unfreeze_function : 'a -> unit;
init_function : unit -> unit }
@@ -31,7 +29,7 @@ let ml_modules = "ML-MODULES"
let internal_declare_summary fadd sumname sdecl =
let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in
- let dyn_freeze b = infun (sdecl.freeze_function b)
+ let dyn_freeze ~marshallable = infun (sdecl.freeze_function ~marshallable)
and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
and dyn_init = sdecl.init_function in
let ddecl = {
@@ -70,9 +68,9 @@ type frozen = {
let empty_frozen = { summaries = String.Map.empty; ml_module = None }
let freeze_summaries ~marshallable : frozen =
- let smap decl = decl.freeze_function marshallable in
+ let smap decl = decl.freeze_function ~marshallable in
{ summaries = String.Map.map smap !sum_map;
- ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod;
+ ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod;
}
let warn_summary_out_of_scope =
@@ -92,7 +90,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 ->
@@ -130,10 +128,10 @@ let remove_from_summary st tag =
(** All-in-one reference declaration + registration *)
-let ref_tag ?(freeze=fun _ r -> r) ~name x =
+let ref_tag ?(freeze=fun ~marshallable r -> r) ~name x =
let r = ref x in
let tag = declare_summary_tag name
- { freeze_function = (fun b -> freeze b !r);
+ { freeze_function = (fun ~marshallable -> freeze ~marshallable !r);
unfreeze_function = ((:=) r);
init_function = (fun () -> r := x) } in
r, tag
@@ -157,7 +155,7 @@ let (!) r =
let ref ?(freeze=fun x -> x) ~name init =
let r = Pervasives.ref (CEphemeron.create init, name) in
declare_summary name
- { freeze_function = (fun _ -> freeze !r);
+ { freeze_function = (fun ~marshallable -> freeze !r);
unfreeze_function = ((:=) r);
init_function = (fun () -> r := init) };
r
diff --git a/library/summary.mli b/library/summary.mli
index 7d91a79188..0d77d725ac 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -11,17 +11,12 @@
(** This module registers the declaration of global tables, which will be kept
in synchronization during the various backtracks of the system. *)
-type marshallable =
- [ `Yes (* Full data will be marshalled to disk *)
- | `No (* Full data will be store in memory, e.g. for Undo *)
- | `Shallow ] (* Only part of the data will be marshalled to a slave process *)
-
(** 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.
+ freeze_function : marshallable:bool -> 'a;
+ (** freeze_function [true] is for marshalling to disk.
* e.g. lazy must be forced *)
- freeze_function : marshallable -> 'a;
unfreeze_function : 'a -> unit;
init_function : unit -> unit }
@@ -50,8 +45,8 @@ val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag
The [init_function] restores the reference to its initial value.
The [freeze_function] can be overridden *)
-val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
-val ref_tag : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag
+val ref : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag
(* As [ref] but the value is local to a process, i.e. not sent to, say, proof
* workers. It is useful to implement a local cache for example. *)
@@ -81,7 +76,7 @@ val nop : unit -> unit
type frozen
val empty_frozen : frozen
-val freeze_summaries : marshallable:marshallable -> frozen
+val freeze_summaries : marshallable:bool -> frozen
val unfreeze_summaries : ?partial:bool -> frozen -> unit
val init_summaries : unit -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 11:44:52 +0000