aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml12
-rw-r--r--library/coqlib.mli16
-rw-r--r--library/decl_kinds.ml2
-rw-r--r--library/declaremods.ml28
-rw-r--r--library/declaremods.mli4
-rw-r--r--library/decls.mli2
-rw-r--r--library/global.ml148
-rw-r--r--library/global.mli28
-rw-r--r--library/globnames.ml20
-rw-r--r--library/globnames.mli4
-rw-r--r--library/goptions.ml32
-rw-r--r--library/goptions.mli13
-rw-r--r--library/keys.ml19
-rw-r--r--library/lib.ml108
-rw-r--r--library/lib.mli43
-rw-r--r--library/libnames.ml31
-rw-r--r--library/libnames.mli44
-rw-r--r--library/libobject.ml48
-rw-r--r--library/libobject.mli51
-rw-r--r--library/library.ml28
-rw-r--r--library/library.mli13
-rw-r--r--library/nametab.ml85
-rw-r--r--library/nametab.mli65
-rw-r--r--library/states.ml8
-rw-r--r--library/states.mli4
-rw-r--r--library/summary.ml18
-rw-r--r--library/summary.mli15
27 files changed, 456 insertions, 433 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 677515981a..784360dc8a 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -14,7 +14,6 @@ open Pp
open Names
open Libnames
open Globnames
-open Nametab
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
@@ -79,7 +78,7 @@ let register_ref s c =
(* Generic functions to find Coq objects *)
let has_suffix_in_dirs dirs ref =
- let dir = dirpath (path_of_global ref) in
+ let dir = dirpath (Nametab.path_of_global ref) in
List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
let gen_reference_in_modules locstr dirs s =
@@ -228,8 +227,7 @@ type coq_eq_data = {
(* Leibniz equality on Type *)
-let build_eqdata_gen lib str =
- let _ = check_required_library lib in {
+let build_eqdata_gen str = {
eq = lib_ref ("core." ^ str ^ ".type");
ind = lib_ref ("core." ^ str ^ ".ind");
refl = lib_ref ("core." ^ str ^ ".refl");
@@ -238,9 +236,9 @@ let build_eqdata_gen lib str =
congr = lib_ref ("core." ^ str ^ ".congr");
}
-let build_coq_eq_data () = build_eqdata_gen logic_module_name "eq"
-let build_coq_jmeq_data () = build_eqdata_gen jmeq_module_name "JMeq"
-let build_coq_identity_data () = build_eqdata_gen datatypes_module_name "identity"
+let build_coq_eq_data () = build_eqdata_gen "eq"
+let build_coq_jmeq_data () = build_eqdata_gen "JMeq"
+let build_coq_identity_data () = build_eqdata_gen "identity"
(* Inversion data... *)
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..8d5c2fb687 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 *)
@@ -71,6 +70,7 @@ type goal_kind = locality * polymorphic * goal_object_kind
(** Kinds used in library *)
type logical_kind =
+ | IsPrimitive
| IsAssumption of assumption_object_kind
| IsDefinition of definition_object_kind
| IsProof of theorem_kind
diff --git a/library/declaremods.ml b/library/declaremods.ml
index e01a99f731..5fd11e187a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -139,7 +139,7 @@ let expand_sobjs (_,aobjs) = expand_aobjs aobjs
Module M:SIG. ... End M. have the keep list empty.
*)
-type module_objects = object_prefix * Lib.lib_objects * Lib.lib_objects
+type module_objects = Nametab.object_prefix * Lib.lib_objects * Lib.lib_objects
module ModObjs :
sig
@@ -185,7 +185,7 @@ let consistency_checks exists dir dirinfo =
user_err ~hdr:"consistency_checks"
(DirPath.print dir ++ str " should already exist!")
in
- assert (eq_global_dir_reference globref dirinfo)
+ assert (Nametab.GlobDirRef.equal globref dirinfo)
else
if Nametab.exists_dir dir then
user_err ~hdr:"consistency_checks"
@@ -197,8 +197,8 @@ let compute_visibility exists i =
(** Iterate some function [iter_objects] on all components of a module *)
let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
- let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in
- let dirinfo = DirModule prefix in
+ let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+ let dirinfo = Nametab.GlobDirRef.DirModule prefix in
consistency_checks exists obj_dir dirinfo;
Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo;
ModSubstObjs.set obj_mp sobjs;
@@ -239,19 +239,19 @@ let cache_keep _ = anomaly (Pp.str "This module should not be cached!")
let load_keep i ((sp,kn),kobjs) =
(* Invariant : seg isn't empty *)
let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
- let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
let prefix',sobjs,kobjs0 =
try ModObjs.get obj_mp
with Not_found -> assert false (* a substobjs should already be loaded *)
in
- assert (eq_op prefix' prefix);
+ assert Nametab.(eq_op prefix' prefix);
assert (List.is_empty kobjs0);
ModObjs.set obj_mp (prefix,sobjs,kobjs);
Lib.load_objects i prefix kobjs
let open_keep i ((sp,kn),kobjs) =
let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
- let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
Lib.open_objects i prefix kobjs
let in_modkeep : Lib.lib_objects -> obj =
@@ -302,7 +302,7 @@ let (in_modtype : substitutive_objects -> obj),
let do_include do_load do_open i ((sp,kn),aobjs) =
let obj_dir = Libnames.dirpath sp in
let obj_mp = KerName.modpath kn in
- let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
let o = expand_aobjs aobjs in
if do_load then Lib.load_objects i prefix o;
if do_open then Lib.open_objects i prefix o
@@ -605,7 +605,7 @@ let start_module interp_modast export id args res fs =
let () = Global.push_context_set true cst in
openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
let prefix = Lib.start_module export id mp fs in
- Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModule prefix);
+ Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix));
mp
let end_module () =
@@ -723,7 +723,7 @@ let start_modtype interp_modast id args mtys fs =
let () = Global.push_context_set true cst in
openmodtype_info := sub_mty_l;
let prefix = Lib.start_modtype id mp fs in
- Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModtype prefix);
+ Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix));
mp
let end_modtype () =
@@ -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 *)
@@ -928,10 +928,10 @@ let append_end_library_hook f =
let old_f = !end_library_hook in
end_library_hook := fun () -> old_f(); f ()
-let end_library ?except dir =
+let end_library ?except ~output_native_objects dir =
!end_library_hook();
let oname = Lib.end_compilation_checks dir in
- let mp,cenv,ast = Global.export ?except dir in
+ let mp,cenv,ast = Global.export ?except ~output_native_objects dir in
let prefix, lib_stack = Lib.end_compilation oname in
assert (ModPath.equal mp (MPfile dir));
let substitute, keep, _ = Lib.classify_segment lib_stack in
@@ -977,7 +977,7 @@ let iter_all_segments f =
| "INCLUDE" ->
let objs = expand_aobjs (out_include obj) in
List.iter (apply_obj prefix) objs
- | _ -> f (make_oname prefix id) obj
+ | _ -> f (Lib.make_oname prefix id) obj
in
let apply_mod_obj _ (prefix,substobjs,keepobjs) =
List.iter (apply_obj prefix) substobjs;
diff --git a/library/declaremods.mli b/library/declaremods.mli
index b42a59bfbd..2b28ba908e 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -99,7 +99,7 @@ val get_library_native_symbols : library_name -> Nativecode.symbols
val start_library : library_name -> unit
val end_library :
- ?except:Future.UUIDSet.t -> library_name ->
+ ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name ->
Safe_typing.compiled_library * library_objects * Safe_typing.native_library
(** append a function to be executed at end_library *)
@@ -130,7 +130,7 @@ val declare_include :
(together with their section path). *)
val iter_all_segments :
- (Libnames.object_name -> Libobject.obj -> unit) -> unit
+ (Libobject.object_name -> Libobject.obj -> unit) -> unit
val debug_print_modtab : unit -> Pp.t
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 0e236e6d34..d9f8a6ffa3 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) }
@@ -88,8 +87,12 @@ let add_constraints c = globalize0 (Safe_typing.add_constraints c)
let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
+let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
let typing_flags () = Environ.typing_flags (env ())
+let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
+let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
+let sprop_allowed () = Environ.sprop_allowed (env())
let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d)
let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
@@ -128,42 +131,23 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
let opaque_tables () = Environ.opaque_tables (env ())
-let instantiate cb c =
- let open Declarations in
- match cb.const_universes with
- | Monomorphic_const _ -> c, Univ.AUContext.empty
- | Polymorphic_const ctx -> c, ctx
-
-let body_of_constant_body cb =
- let open Declarations in
- let otab = opaque_tables () in
- match cb.const_body with
- | Undef _ -> None
- | Def c -> Some (instantiate cb (Mod_subst.force_constr c))
- | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o))
+let body_of_constant_body ce = body_of_constant_body (env ()) ce
let body_of_constant cst = body_of_constant_body (lookup_constant cst)
(** Operations on kernel names *)
let constant_of_delta_kn kn =
- let resolver,resolver_param = Safe_typing.delta_of_senv (safe_env ())
- in
- (* TODO : are resolver and resolver_param orthogonal ?
- the effect of resolver is lost if resolver_param isn't
- trivial at that spot. *)
- Mod_subst.constant_of_deltas_kn resolver_param resolver kn
+ Safe_typing.constant_of_delta_kn_senv (safe_env ()) kn
let mind_of_delta_kn kn =
- let resolver,resolver_param = Safe_typing.delta_of_senv (safe_env ())
- in
- (* TODO idem *)
- Mod_subst.mind_of_deltas_kn resolver_param resolver kn
+ Safe_typing.mind_of_delta_kn_senv (safe_env ()) kn
(** Operations on libraries *)
let start_library dir = globalize (Safe_typing.start_library dir)
-let export ?except s = Safe_typing.export ?except (safe_env ()) s
+let export ?except ~output_native_objects s =
+ Safe_typing.export ?except ~output_native_objects (safe_env ()) s
let import c u d = globalize (Safe_typing.import c u d)
@@ -173,91 +157,17 @@ let import c u d = globalize (Safe_typing.import c u d)
let env_of_context hyps =
reset_with_named_context hyps (env())
-open Globnames
-
-(** Build a fresh instance for a given context, its associated substitution and
- the instantiated constraints. *)
-
-let constr_of_global_in_context env r =
- let open Constr in
- match r with
- | VarRef id -> mkVar id, Univ.AUContext.empty
- | ConstRef c ->
- let cb = Environ.lookup_constant c env in
- let univs = Declareops.constant_polymorphic_context cb in
- mkConstU (c, Univ.make_abstract_instance univs), univs
- | IndRef ind ->
- let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- let univs = Declareops.inductive_polymorphic_context mib in
- mkIndU (ind, Univ.make_abstract_instance univs), univs
- | ConstructRef cstr ->
- let (mib,oib as specif) =
- Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
- in
- let univs = Declareops.inductive_polymorphic_context mib in
- mkConstructU (cstr, Univ.make_abstract_instance univs), univs
-
-let type_of_global_in_context env r =
- match r with
- | VarRef id -> Environ.named_type id env, Univ.AUContext.empty
- | ConstRef c ->
- let cb = Environ.lookup_constant c env in
- let univs = Declareops.constant_polymorphic_context cb in
- cb.Declarations.const_type, univs
- | IndRef ind ->
- let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- let univs = Declareops.inductive_polymorphic_context mib in
- let inst = Univ.make_abstract_instance univs in
- let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
- Inductive.type_of_inductive env (specif, inst), univs
- | ConstructRef cstr ->
- let (mib,oib as specif) =
- Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
- in
- let univs = Declareops.inductive_polymorphic_context mib in
- let inst = Univ.make_abstract_instance univs in
- Inductive.type_of_constructor (cstr,inst) specif, univs
-
-let universes_of_global env r =
- match r with
- | VarRef id -> Univ.AUContext.empty
- | ConstRef c ->
- let cb = Environ.lookup_constant c env in
- Declareops.constant_polymorphic_context cb
- | IndRef ind ->
- let (mib, oib) = Inductive.lookup_mind_specif env ind in
- Declareops.inductive_polymorphic_context mib
- | ConstructRef cstr ->
- let (mib,oib) =
- Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Declareops.inductive_polymorphic_context mib
+let constr_of_global_in_context = Typeops.constr_of_global_in_context
+let type_of_global_in_context = Typeops.type_of_global_in_context
let universes_of_global gr =
universes_of_global (env ()) gr
-let is_polymorphic r =
- let env = env() in
- match r with
- | VarRef id -> false
- | ConstRef c -> Environ.polymorphic_constant c env
- | IndRef ind -> Environ.polymorphic_ind ind env
- | ConstructRef cstr -> Environ.polymorphic_ind (inductive_of_constructor cstr) env
-
-let is_template_polymorphic r =
- let env = env() in
- match r with
- | VarRef id -> false
- | ConstRef c -> false
- | IndRef ind -> Environ.template_polymorphic_ind ind env
- | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
-
-let is_type_in_type r =
- let env = env() in
- match r with
- | VarRef id -> false
- | ConstRef c -> Environ.type_in_type_constant c env
- | IndRef ind -> Environ.type_in_type_ind ind env
- | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env
+let is_polymorphic r = Environ.is_polymorphic (env()) r
+
+let is_template_polymorphic r = is_template_polymorphic (env ()) r
+
+let is_type_in_type r = is_type_in_type (env ()) r
let current_modpath () =
Safe_typing.current_modpath (safe_env ())
@@ -269,18 +179,14 @@ let with_global f =
let (a, ctx) = f (env ()) (current_dirpath ()) in
push_context_set false ctx; a
-(* spiwack: register/unregister functions for retroknowledge *)
-let register field value =
- globalize0 (Safe_typing.register field value)
-
let register_inline c = globalize0 (Safe_typing.register_inline c)
+let register_inductive c r = globalize0 (Safe_typing.register_inductive c r)
let set_strategy k l =
- GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l)
-
-let set_reduction_sharing b =
- let env = safe_env () in
- let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in
- let flags = { flags with Declarations.share_reduction = b } in
- let env = Safe_typing.set_typing_flags flags env in
- GlobalSafeEnv.set_safe_env env
+ globalize0 (Safe_typing.set_strategy k l)
+
+let set_share_reduction b =
+ globalize0 (Safe_typing.set_share_reduction b)
+
+let set_VM b = globalize0 (Safe_typing.set_VM b)
+let set_native_compiler b = globalize0 (Safe_typing.set_native_compiler b)
diff --git a/library/global.mli b/library/global.mli
index fd6c9a60d4..ca88d2dafd 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -29,8 +29,12 @@ val named_context : unit -> Constr.named_context
(** Changing the (im)predicativity of the system *)
val set_engagement : Declarations.engagement -> unit
+val set_indices_matter : bool -> unit
val set_typing_flags : Declarations.typing_flags -> unit
val typing_flags : unit -> Declarations.typing_flags
+val make_sprop_cumulative : unit -> unit
+val set_allow_sprop : bool -> unit
+val sprop_allowed : unit -> bool
(** Variables, Local definitions, constants, inductive types *)
@@ -107,7 +111,7 @@ val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.
(** {6 Compiled libraries } *)
val start_library : DirPath.t -> ModPath.t
-val export : ?except:Future.UUIDSet.t -> DirPath.t ->
+val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t ->
ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library
val import :
Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest ->
@@ -129,33 +133,31 @@ val is_type_in_type : GlobRef.t -> bool
val constr_of_global_in_context : Environ.env ->
GlobRef.t -> Constr.types * Univ.AUContext.t
-(** Returns the type of the constant in its local universe
- context. The type should not be used without pushing it's universe
- context in the environmnent of usage. For non-universe-polymorphic
- constants, it does not matter. *)
+ [@@ocaml.deprecated "alias of [Typeops.constr_of_global_in_context]"]
val type_of_global_in_context : Environ.env ->
GlobRef.t -> Constr.types * Univ.AUContext.t
-(** Returns the type of the constant in its local universe
- context. The type should not be used without pushing it's universe
- context in the environmnent of usage. For non-universe-polymorphic
- constants, it does not matter. *)
+ [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"]
(** Returns the universe context of the global reference (whatever its polymorphic status is). *)
val universes_of_global : GlobRef.t -> Univ.AUContext.t
+[@@ocaml.deprecated "Use [Environ.universes_of_global]"]
(** {6 Retroknowledge } *)
-val register :
- Retroknowledge.field -> GlobRef.t -> unit
-
val register_inline : Constant.t -> unit
+val register_inductive : inductive -> CPrimitives.prim_ind -> unit
(** {6 Oracle } *)
val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
-val set_reduction_sharing : bool -> unit
+(** {6 Conversion settings } *)
+
+val set_share_reduction : bool -> unit
+
+val set_VM : bool -> unit
+val set_native_compiler : bool -> unit
(* Modifies the global state, registering new universes *)
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 dcbc46ab72..1b907fd966 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -73,7 +73,7 @@ module MakeTable =
let _ =
if String.List.mem_assoc nick !A.table then
- user_err Pp.(str "Sorry, this table name is already used.")
+ user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.")
module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
@@ -216,11 +216,11 @@ let get_option key = OptionMap.find key !value_tab
let check_key key = try
let _ = get_option key in
- user_err Pp.(str "Sorry, this option name is already used.")
+ user_err Pp.(str "Sorry, this option name ("++ str (nickname key) ++ str ") is already used.")
with Not_found ->
if String.List.mem_assoc (nickname key) !string_table
|| String.List.mem_assoc (nickname key) !ref_table
- then user_err Pp.(str "Sorry, this option name is already used.")
+ then user_err Pp.(str "Sorry, this option name (" ++ str (nickname key) ++ str ") is already used.")
open Libobject
@@ -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
@@ -276,10 +276,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
let cread () = cast (read ()) in
let cwrite l v = warn (); change l OptSet (uncast v) in
let cappend l v = warn (); change l OptAppend (uncast v) in
- value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab;
- write
-
-type 'a write_function = 'a -> unit
+ value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab
let declare_int_option =
declare_option
@@ -302,6 +299,18 @@ let declare_stringopt_option =
(function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
(fun _ _ -> anomaly (Pp.str "async_option."))
+let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) =
+ let r_opt = ref value in
+ let optwrite v = r_opt := v in
+ let optread () = !r_opt in
+ let _ = declare_bool_option {
+ optdepr = depr;
+ optname = name;
+ optkey = key;
+ optread; optwrite
+ } in
+ optread
+
(* 3- User accessible commands *)
(* Setting values of options *)
@@ -425,6 +434,3 @@ let print_tables () =
(fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ())
!ref_table (mt ()) ++
fnl ()
-
-
-
diff --git a/library/goptions.mli b/library/goptions.mli
index 3d7df18fed..b91553bf3c 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -122,17 +122,18 @@ type 'a option_sig = {
(** The [preprocess] function is triggered before setting the option. It can be
used to emit a warning on certain values, and clean-up the final value. *)
-type 'a write_function = 'a -> unit
-
val declare_int_option : ?preprocess:(int option -> int option) ->
- int option option_sig -> int option write_function
+ int option option_sig -> unit
val declare_bool_option : ?preprocess:(bool -> bool) ->
- bool option_sig -> bool write_function
+ bool option_sig -> unit
val declare_string_option: ?preprocess:(string -> string) ->
- string option_sig -> string write_function
+ string option_sig -> unit
val declare_stringopt_option: ?preprocess:(string option -> string option) ->
- string option option_sig -> string option write_function
+ string option option_sig -> unit
+(** Helper to declare a reference controlled by an option. Read-only
+ as to avoid races. *)
+val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool)
(** {6 Special functions supposed to be used only in vernacentries.ml } *)
diff --git a/library/keys.ml b/library/keys.ml
index 53447a679a..45b6fae2f0 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -25,13 +25,14 @@ type key =
| KFix
| KCoFix
| KRel
+ | KInt
module KeyOrdered = struct
type t = key
let hash gr =
match gr with
- | KGlob gr -> 8 + GlobRef.Ordered.hash gr
+ | KGlob gr -> 9 + GlobRef.Ordered.hash gr
| KLam -> 0
| KLet -> 1
| KProd -> 2
@@ -40,6 +41,7 @@ module KeyOrdered = struct
| KFix -> 5
| KCoFix -> 6
| KRel -> 7
+ | KInt -> 8
let compare gr1 gr2 =
match gr1, gr2 with
@@ -100,18 +102,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'))
@@ -138,6 +135,7 @@ let constr_key kind c =
| Evar _ -> raise Not_found
| Sort _ -> KSort
| LetIn _ -> KLet
+ | Int _ -> KInt
in Some (aux c)
with Not_found -> None
@@ -153,6 +151,7 @@ let pr_key pr_global = function
| KFix -> str"Fix"
| KCoFix -> str"CoFix"
| KRel -> str"Rel"
+ | KInt -> str"Int"
let pr_keyset pr_global v =
prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
diff --git a/library/lib.ml b/library/lib.ml
index 27c5056a7f..d4381a6923 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -22,11 +22,16 @@ module NamedDecl = Context.Named.Declaration
type is_type = bool (* Module Type or just Module *)
type export = bool option (* None for a Module Type *)
+(* let make_oname (dirpath,(mp,dir)) id = *)
+let make_oname Nametab.{ obj_dir; obj_mp } id =
+ Names.(make_path obj_dir id, KerName.make obj_mp (Label.of_id id))
+
+(* let make_oname (dirpath,(mp,dir)) id = *)
type node =
| Leaf of obj
- | CompilingLibrary of object_prefix
- | OpenedModule of is_type * export * object_prefix * Summary.frozen
- | OpenedSection of object_prefix * Summary.frozen
+ | CompilingLibrary of Nametab.object_prefix
+ | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen
+ | OpenedSection of Nametab.object_prefix * Summary.frozen
type library_entry = object_name * node
@@ -89,7 +94,7 @@ let segment_of_objects prefix =
sections, but on the contrary there are many constructions of section
paths based on the library path. *)
-let initial_prefix = {
+let initial_prefix = Nametab.{
obj_dir = default_library;
obj_mp = ModPath.initial;
obj_sec = DirPath.empty;
@@ -98,7 +103,7 @@ let initial_prefix = {
type lib_state = {
comp_name : DirPath.t option;
lib_stk : library_segment;
- path_prefix : object_prefix;
+ path_prefix : Nametab.object_prefix;
}
let initial_lib_state = {
@@ -115,9 +120,9 @@ let library_dp () =
(* [path_prefix] is a pair of absolute dirpath and a pair of current
module path and relative section path *)
-let cwd () = !lib_state.path_prefix.obj_dir
-let current_mp () = !lib_state.path_prefix.obj_mp
-let current_sections () = !lib_state.path_prefix.obj_sec
+let cwd () = !lib_state.path_prefix.Nametab.obj_dir
+let current_mp () = !lib_state.path_prefix.Nametab.obj_mp
+let current_sections () = !lib_state.path_prefix.Nametab.obj_sec
let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
@@ -138,7 +143,7 @@ let make_kn id =
let mp = current_mp () in
Names.KerName.make mp (Names.Label.of_id id)
-let make_oname id = Libnames.make_oname !lib_state.path_prefix id
+let make_foname id = make_oname !lib_state.path_prefix id
let recalc_path_prefix () =
let rec recalc = function
@@ -153,9 +158,9 @@ let recalc_path_prefix () =
let pop_path_prefix () =
let op = !lib_state.path_prefix in
lib_state := { !lib_state
- with path_prefix = { op with obj_dir = pop_dirpath op.obj_dir;
- obj_sec = pop_dirpath op.obj_sec;
- } }
+ with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir;
+ obj_sec = pop_dirpath op.obj_sec;
+ } }
let find_entry_p p =
let rec find = function
@@ -214,24 +219,24 @@ let anonymous_id =
fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
let add_anonymous_entry node =
- add_entry (make_oname (anonymous_id ())) node
+ add_entry (make_foname (anonymous_id ())) node
let add_leaf id obj =
if ModPath.equal (current_mp ()) ModPath.initial then
user_err Pp.(str "No session module started (use -top dir)");
- let oname = make_oname id in
+ let oname = make_foname id in
cache_object (oname,obj);
add_entry oname (Leaf obj);
oname
let add_discharged_leaf id obj =
- let oname = make_oname id in
+ let oname = make_foname id in
let newobj = rebuild_object obj in
cache_object (oname,newobj);
add_entry oname (Leaf newobj)
let add_leaves id objs =
- let oname = make_oname id in
+ let oname = make_foname id in
let add_obj obj =
add_entry oname (Leaf obj);
load_object 1 (oname,obj)
@@ -241,7 +246,7 @@ let add_leaves id objs =
let add_anonymous_leaf ?(cache_first = true) obj =
let id = anonymous_id () in
- let oname = make_oname id in
+ let oname = make_foname id in
if cache_first then begin
cache_object (oname,obj);
add_entry oname (Leaf obj)
@@ -269,15 +274,15 @@ let current_mod_id () =
let start_mod is_type export id mp fs =
- let dir = add_dirpath_suffix (!lib_state.path_prefix.obj_dir) id in
- let prefix = { obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
+ let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in
+ let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
let exists =
if is_type then Nametab.exists_cci (make_path id)
else Nametab.exists_module dir
in
if exists then
user_err ~hdr:"open_module" (Id.print id ++ str " already exists");
- add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
+ add_entry (make_foname id) (OpenedModule (is_type,export,prefix,fs));
lib_state := { !lib_state with path_prefix = prefix} ;
prefix
@@ -318,9 +323,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
let start_compilation s mp =
if !lib_state.comp_name != None then
user_err Pp.(str "compilation unit is already started");
- if not (Names.DirPath.is_empty (!lib_state.path_prefix.obj_sec)) then
+ if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then
user_err Pp.(str "some sections are already opened");
- let prefix = Libnames.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in
+ let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in
add_anonymous_entry (CompilingLibrary prefix);
lib_state := { !lib_state with comp_name = Some s;
path_prefix = prefix }
@@ -474,7 +479,24 @@ let instance_from_variable_context =
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. *)
+ let map lvl = match Univ.Level.name lvl with
+ | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+ assert false
+ | Some na ->
+ try
+ 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. *)
+ Name (Id.of_string_soft (Univ.Level.to_string lvl))
+ in
+ Array.map map (Univ.Instance.to_array inst)
+
let add_section_replacement f g poly hyps =
match !sectab with
| [] -> ()
@@ -483,7 +505,8 @@ let add_section_replacement f g poly hyps =
let sechyps,ctx = extract_hyps (vars,hyps) in
let ctx = Univ.ContextSet.to_context ctx in
let inst = Univ.UContext.instance ctx in
- let subst, ctx = Univ.abstract_universes ctx in
+ let nas = name_instance inst in
+ let subst, ctx = Univ.abstract_universes nas ctx in
let args = instance_from_variable_context (List.rev sechyps) in
let info = {
abstr_ctx = sechyps;
@@ -544,14 +567,14 @@ let is_in_section ref =
(* Sections. *)
let open_section id =
let opp = !lib_state.path_prefix in
- let obj_dir = add_dirpath_suffix opp.obj_dir id in
- let prefix = { obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
+ let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
+ 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
- add_entry (make_oname id) (OpenedSection (prefix, fs));
+ 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 (Nametab.Until 1) obj_dir (DirOpenSection prefix);
+ Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
lib_state := { !lib_state with path_prefix = prefix };
add_section ()
@@ -585,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;
@@ -611,7 +631,7 @@ let init () =
(* Misc *)
let mp_of_global = function
- | VarRef id -> !lib_state.path_prefix.obj_mp
+ | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp
| ConstRef cst -> Names.Constant.modpath cst
| IndRef ind -> Names.ind_modpath ind
| ConstructRef constr -> Names.constr_modpath constr
diff --git a/library/lib.mli b/library/lib.mli
index 686e6a0e2d..30569197bc 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -19,22 +19,24 @@ open Names
type is_type = bool (* Module Type or just Module *)
type export = bool option (* None for a Module Type *)
+val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name
+
type node =
| Leaf of Libobject.obj
- | CompilingLibrary of Libnames.object_prefix
- | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen
- | OpenedSection of Libnames.object_prefix * Summary.frozen
+ | CompilingLibrary of Nametab.object_prefix
+ | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen
+ | OpenedSection of Nametab.object_prefix * Summary.frozen
-type library_segment = (Libnames.object_name * node) list
+type library_segment = (Libobject.object_name * node) list
type lib_objects = (Id.t * Libobject.obj) list
(** {6 Object iteration functions. } *)
-val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
-val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val open_objects : int -> Nametab.object_prefix -> lib_objects -> unit
+val load_objects : int -> Nametab.object_prefix -> lib_objects -> unit
val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects
-(*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
+(*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
(** [classify_segment seg] verifies that there are no OpenedThings,
clears ClosedSections and FrozenStates and divides Leafs according
@@ -46,20 +48,20 @@ val classify_segment :
(** [segment_of_objects prefix objs] forms a list of Leafs *)
val segment_of_objects :
- Libnames.object_prefix -> lib_objects -> library_segment
+ Nametab.object_prefix -> lib_objects -> library_segment
(** {6 ... } *)
(** Adding operations (which call the [cache] method, and getting the
current list of operations (most recent ones coming first). *)
-val add_leaf : Id.t -> Libobject.obj -> Libnames.object_name
+val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name
val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
-val pull_to_head : Libnames.object_name -> unit
+val pull_to_head : Libobject.object_name -> unit
(** this operation adds all objects with the same name and calls [load_object]
for each of them *)
-val add_leaves : Id.t -> Libobject.obj list -> Libnames.object_name
+val add_leaves : Id.t -> Libobject.obj list -> Libobject.object_name
(** {6 ... } *)
@@ -70,7 +72,7 @@ val contents : unit -> library_segment
(** The function [contents_after] returns the current library segment,
starting from a given section path. *)
-val contents_after : Libnames.object_name -> library_segment
+val contents_after : Libobject.object_name -> library_segment
(** {6 Functions relative to current path } *)
@@ -105,28 +107,28 @@ val find_opening_node : Id.t -> node
val start_module :
export -> module_ident -> ModPath.t ->
- Summary.frozen -> Libnames.object_prefix
+ Summary.frozen -> Nametab.object_prefix
val start_modtype :
module_ident -> ModPath.t ->
- Summary.frozen -> Libnames.object_prefix
+ Summary.frozen -> Nametab.object_prefix
val end_module :
unit ->
- Libnames.object_name * Libnames.object_prefix *
+ Libobject.object_name * Nametab.object_prefix *
Summary.frozen * library_segment
val end_modtype :
unit ->
- Libnames.object_name * Libnames.object_prefix *
+ Libobject.object_name * Nametab.object_prefix *
Summary.frozen * library_segment
(** {6 Compilation units } *)
val start_compilation : DirPath.t -> ModPath.t -> unit
-val end_compilation_checks : DirPath.t -> Libnames.object_name
+val end_compilation_checks : DirPath.t -> Libobject.object_name
val end_compilation :
- Libnames.object_name-> Libnames.object_prefix * library_segment
+ Libobject.object_name-> Nametab.object_prefix * library_segment
(** The function [library_dp] returns the [DirPath.t] of the current
compiling library (or [default_library]) *)
@@ -146,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.ml b/library/libnames.ml
index bd2ca550b9..87c4de42e8 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -162,37 +162,6 @@ let qualid_basename qid =
let qualid_path qid =
qid.CAst.v.dirpath
-type object_name = full_path * KerName.t
-
-type object_prefix = {
- obj_dir : DirPath.t;
- obj_mp : ModPath.t;
- obj_sec : DirPath.t;
-}
-
-(* let make_oname (dirpath,(mp,dir)) id = *)
-let make_oname { obj_dir; obj_mp } id =
- make_path obj_dir id, KerName.make obj_mp (Label.of_id id)
-
-(* to this type are mapped DirPath.t's in the nametab *)
-type global_dir_reference =
- | DirOpenModule of object_prefix
- | DirOpenModtype of object_prefix
- | DirOpenSection of object_prefix
- | DirModule of object_prefix
-
-let eq_op op1 op2 =
- DirPath.equal op1.obj_dir op2.obj_dir &&
- DirPath.equal op1.obj_sec op2.obj_sec &&
- ModPath.equal op1.obj_mp op2.obj_mp
-
-let eq_global_dir_reference r1 r2 = match r1, r2 with
-| DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
-| DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
-| DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
-| DirModule op1, DirModule op2 -> eq_op op1 op2
-| _ -> false
-
(* Default paths *)
let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/libnames.mli b/library/libnames.mli
index 447eecbb5c..bbb4d2a058 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -88,54 +88,14 @@ val qualid_is_ident : qualid -> bool
val qualid_path : qualid -> DirPath.t
val qualid_basename : qualid -> Id.t
-(** Both names are passed to objects: a "semantic" [kernel_name], which
- can be substituted and a "syntactic" [full_path] which can be printed
-*)
-
-type object_name = full_path * KerName.t
-
-(** Object prefix morally contains the "prefix" naming of an object to
- be stored by [library], where [obj_dir] is the "absolute" path,
- [obj_mp] is the current "module" prefix and [obj_sec] is the
- "section" prefix.
-
- Thus, for an object living inside [Module A. Section B.] the
- prefix would be:
-
- [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ]
-
- Note that both [obj_dir] and [obj_sec] are "paths" that is to say,
- as opposed to [obj_mp] which is a single module name.
-
- *)
-type object_prefix = {
- obj_dir : DirPath.t;
- obj_mp : ModPath.t;
- obj_sec : DirPath.t;
-}
-
-val eq_op : object_prefix -> object_prefix -> bool
-
-val make_oname : object_prefix -> Id.t -> object_name
-
-(** to this type are mapped [DirPath.t]'s in the nametab *)
-type global_dir_reference =
- | DirOpenModule of object_prefix
- | DirOpenModtype of object_prefix
- | DirOpenSection of object_prefix
- | DirModule of object_prefix
-
-val eq_global_dir_reference :
- global_dir_reference -> global_dir_reference -> bool
-
(** {6 ... } *)
(** some preset paths *)
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 79a3fed1b9..3d17b4a605 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Libnames
open Pp
module Dyn = Dyn.Make ()
@@ -16,6 +15,8 @@ module Dyn = Dyn.Make ()
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
+type object_name = Libnames.full_path * Names.KerName.t
+
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
@@ -65,7 +66,7 @@ type dynamic_object_declaration = {
let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
let cache_tab =
- (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
+ (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t)
let declare_object_full odecl =
let na = odecl.object_name in
@@ -128,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 aefa81b225..00515bd273 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -66,6 +66,12 @@ open Mod_subst
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
+(** Both names are passed to objects: a "semantic" [kernel_name], which
+ can be substituted and a "syntactic" [full_path] which can be printed
+*)
+
+type object_name = full_path * Names.KerName.t
+
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
@@ -113,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.ml b/library/library.ml
index 0ff82d7cc4..37dadadb76 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -611,28 +611,6 @@ let import_module export modl =
(************************************************************************)
(*s Initializing the compilation of a library. *)
-let check_coq_overwriting p id =
- let l = DirPath.repr p in
- let is_empty = match l with [] -> true | _ -> false in
- if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
- user_err
- (str "Cannot build module " ++ DirPath.print p ++ str "." ++ Id.print id ++ str "." ++ spc () ++
- str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
-
-let start_library fo =
- let ldir0 =
- try
- let lp = Loadpath.find_load_path (Filename.dirname fo) in
- Loadpath.logical lp
- with Not_found -> Libnames.default_root_prefix
- in
- let file = Filename.chop_extension (Filename.basename fo) in
- let id = Id.of_string file in
- check_coq_overwriting ldir0 id;
- let ldir = add_dirpath_suffix ldir0 id in
- Declaremods.start_library ldir;
- ldir
-
let load_library_todo f =
let longf = Loadpath.locate_file (f^".v") in
let f = longf^"io" in
@@ -679,7 +657,7 @@ let error_recursively_dependent_library dir =
(* Security weakness: file might have been changed on disk between
writing the content and computing the checksum... *)
-let save_library_to ?todo dir f otab =
+let save_library_to ?todo ~output_native_objects dir f otab =
let except = match todo with
| None ->
(* XXX *)
@@ -690,7 +668,7 @@ let save_library_to ?todo dir f otab =
assert(Filename.check_suffix f ".vio");
List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
Future.UUIDSet.empty l in
- let cenv, seg, ast = Declaremods.end_library ~except dir in
+ let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
let tasks, utab, dtab =
match todo with
@@ -738,7 +716,7 @@ let save_library_to ?todo dir f otab =
System.marshal_out_segment f' ch (opaque_table : seg_proofs);
close_out ch;
(* Writing native code files *)
- if !Flags.output_native_objects then
+ if output_native_objects then
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
if not (Nativelib.compile_library dir ast fn) then
user_err Pp.(str "Could not compile the library to native code.")
diff --git a/library/library.mli b/library/library.mli
index d5815afc40..a976be0184 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
@@ -38,14 +38,11 @@ type seg_proofs = Constr.constr Future.computation array
an export otherwise just a simple import *)
val import_module : bool -> qualid list -> unit
-(** Start the compilation of a file as a library. The first argument must be
- output file, and the
- returned path is the associated absolute logical path of the library. *)
-val start_library : CUnix.physical_path -> DirPath.t
-
-(** End the compilation of a library and save it to a ".vo" file *)
+(** End the compilation of a library and save it to a ".vo" file.
+ [output_native_objects]: when producing vo objects, also compile the native-code version. *)
val save_library_to :
?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
+ output_native_objects:bool ->
DirPath.t -> string -> Opaqueproof.opaquetab -> unit
val load_library_todo :
diff --git a/library/nametab.ml b/library/nametab.ml
index 06ace373c3..95890b2edf 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -15,6 +15,39 @@ open Names
open Libnames
open Globnames
+type object_prefix = {
+ obj_dir : DirPath.t;
+ obj_mp : ModPath.t;
+ obj_sec : DirPath.t;
+}
+
+let eq_op op1 op2 =
+ DirPath.equal op1.obj_dir op2.obj_dir &&
+ DirPath.equal op1.obj_sec op2.obj_sec &&
+ ModPath.equal op1.obj_mp op2.obj_mp
+
+(* to this type are mapped DirPath.t's in the nametab *)
+module GlobDirRef = struct
+ type t =
+ | DirOpenModule of object_prefix
+ | DirOpenModtype of object_prefix
+ | DirOpenSection of object_prefix
+ | DirModule of object_prefix
+
+ let equal r1 r2 = match r1, r2 with
+ | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
+ | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
+ | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
+ | DirModule op1, DirModule op2 -> eq_op op1 op2
+ | _ -> false
+
+end
+
+type global_dir_reference = GlobDirRef.t
+[@@ocaml.deprecated "Use [GlobDirRef.t]"]
+
+let eq_global_dir_reference = GlobDirRef.equal
+[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
exception GlobalizationError of qualid
@@ -74,6 +107,9 @@ 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
module Make (U : UserName) (E : EqualityType) : NAMETREE
@@ -259,9 +295,19 @@ let find_prefixes qid tab =
search_prefixes (Id.Map.find id tab) (DirPath.repr dir)
with Not_found -> []
-end
-
+let match_prefixes =
+ let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in
+ fun qid tab ->
+ try
+ let (dir,id) = repr_qualid qid in
+ let id_prefix = cprefix Id.(to_string id) in
+ let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in
+ let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in
+ (* Coq's flatten is "magical", so this is not so bad perf-wise *)
+ CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches [])
+ with Not_found -> []
+end
(* Global name tables *************************************************)
@@ -295,25 +341,17 @@ struct
| id :: l -> (id, l)
end
-module GlobDir =
-struct
- type t = global_dir_reference
- let equal = eq_global_dir_reference
-end
-
-module DirTab = Make(DirPath')(GlobDir)
+module DirTab = Make(DirPath')(GlobDirRef)
(* If we have a (closed) module M having a submodule N, than N does not
have the entry in [the_dirtab]. *)
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
@@ -336,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)
@@ -390,7 +425,7 @@ let push_modtype vis sp kn =
let push_dir vis dir dir_ref =
the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
match dir_ref with
- | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab
+ | GlobDirRef.DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab
| _ -> ()
(* This is for global universe names *)
@@ -424,17 +459,17 @@ let locate_dir qid = DirTab.locate qid !the_dirtab
let locate_module qid =
match locate_dir qid with
- | DirModule { obj_mp ; _} -> obj_mp
+ | GlobDirRef.DirModule { obj_mp ; _} -> obj_mp
| _ -> raise Not_found
let full_name_module qid =
match locate_dir qid with
- | DirModule { obj_dir ; _} -> obj_dir
+ | GlobDirRef.DirModule { obj_dir ; _} -> obj_dir
| _ -> raise Not_found
let locate_section qid =
match locate_dir qid with
- | DirOpenSection { obj_dir; _ } -> obj_dir
+ | GlobDirRef.DirOpenSection { obj_dir; _ } -> obj_dir
| _ -> raise Not_found
let locate_all qid =
@@ -447,6 +482,10 @@ let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab
let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab
+(* Completion *)
+let completion_canditates qualid =
+ ExtRefTab.match_prefixes qualid !the_ccitab
+
(* Derived functions *)
let locate_constant qid =
diff --git a/library/nametab.mli b/library/nametab.mli
index 1c3322bfb1..fccb8fd918 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -57,6 +57,44 @@ open Globnames
*)
+(** Object prefix morally contains the "prefix" naming of an object to
+ be stored by [library], where [obj_dir] is the "absolute" path,
+ [obj_mp] is the current "module" prefix and [obj_sec] is the
+ "section" prefix.
+
+ Thus, for an object living inside [Module A. Section B.] the
+ prefix would be:
+
+ [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ]
+
+ Note that both [obj_dir] and [obj_sec] are "paths" that is to say,
+ as opposed to [obj_mp] which is a single module name.
+
+ *)
+type object_prefix = {
+ obj_dir : DirPath.t;
+ obj_mp : ModPath.t;
+ obj_sec : DirPath.t;
+}
+
+val eq_op : object_prefix -> object_prefix -> bool
+
+(** to this type are mapped [DirPath.t]'s in the nametab *)
+module GlobDirRef : sig
+ type t =
+ | DirOpenModule of object_prefix
+ | DirOpenModtype of object_prefix
+ | DirOpenSection of object_prefix
+ | DirModule of object_prefix
+ val equal : t -> t -> bool
+end
+
+type global_dir_reference = GlobDirRef.t
+[@@ocaml.deprecated "Use [GlobDirRef.t]"]
+
+val eq_global_dir_reference :
+ GlobDirRef.t -> GlobDirRef.t -> bool
+[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
exception GlobalizationError of qualid
@@ -79,14 +117,12 @@ val map_visibility : (int -> int) -> visibility -> visibility
val push : visibility -> full_path -> GlobRef.t -> unit
val push_modtype : visibility -> full_path -> ModPath.t -> unit
-val push_dir : visibility -> DirPath.t -> global_dir_reference -> 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 } *)
@@ -98,10 +134,10 @@ val locate_extended : qualid -> extended_global_reference
val locate_constant : qualid -> Constant.t
val locate_syndef : qualid -> syndef_name
val locate_modtype : qualid -> ModPath.t
-val locate_dir : qualid -> global_dir_reference
+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
@@ -115,9 +151,15 @@ val global_inductive : qualid -> inductive
val locate_all : qualid -> GlobRef.t list
val locate_extended_all : qualid -> extended_global_reference list
-val locate_extended_all_dir : qualid -> global_dir_reference list
+val locate_extended_all_dir : qualid -> GlobDirRef.t list
val locate_extended_all_modtype : qualid -> ModPath.t list
+(** Experimental completion support, API is _unstable_ *)
+val completion_canditates : qualid -> extended_global_reference list
+(** [completion_canditates qualid] will return the list of global
+ references that have [qualid] as a prefix. UI usually will want to
+ compose this with [shortest_qualid_of_global] *)
+
(** Mapping a full path to a global reference *)
val global_of_path : full_path -> GlobRef.t
@@ -129,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 } *)
@@ -152,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 *)
@@ -174,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 *)
@@ -211,6 +255,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
+ val match_prefixes : qualid -> t -> elt list
end
module Make (U : UserName) (E : EqualityType) :
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-05-04 09:10:27 +0000