diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 12 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/global.ml | 90 | ||||
| -rw-r--r-- | library/global.mli | 14 | ||||
| -rw-r--r-- | library/lib.ml | 2 | ||||
| -rw-r--r-- | library/lib.mli | 18 | ||||
| -rw-r--r-- | library/libnames.ml | 6 | ||||
| -rw-r--r-- | library/libnames.mli | 8 | ||||
| -rw-r--r-- | library/libobject.ml | 6 | ||||
| -rw-r--r-- | library/libobject.mli | 7 |
10 files changed, 44 insertions, 121 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/declaremods.mli b/library/declaremods.mli index b42a59bfbd..7aa4bc30ce 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -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/global.ml b/library/global.ml index 1ad72afea1..bfea6d3dea 100644 --- a/library/global.ml +++ b/library/global.ml @@ -128,19 +128,7 @@ 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) @@ -165,71 +153,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 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 = Environ.is_polymorphic (env()) r -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_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 ()) @@ -248,11 +182,7 @@ let register field value = let register_inline c = globalize0 (Safe_typing.register_inline c) 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) diff --git a/library/global.mli b/library/global.mli index 29255a70ff..762a3f006d 100644 --- a/library/global.mli +++ b/library/global.mli @@ -129,17 +129,11 @@ 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]"] (** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : GlobRef.t -> Univ.AUContext.t @@ -156,7 +150,9 @@ val register_inline : Constant.t -> unit 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 (* Modifies the global state, registering new universes *) diff --git a/library/lib.ml b/library/lib.ml index 27c5056a7f..1acc8fd8fd 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -138,7 +138,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_oname id = Libobject.make_oname !lib_state.path_prefix id let recalc_path_prefix () = let rec recalc = function diff --git a/library/lib.mli b/library/lib.mli index 686e6a0e2d..c6c6a307d4 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -25,7 +25,7 @@ type node = | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen | OpenedSection of Libnames.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 @@ -53,13 +53,13 @@ val segment_of_objects : (** 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 +70,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 } *) @@ -113,20 +113,20 @@ val start_modtype : val end_module : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Libnames.object_prefix * Summary.frozen * library_segment val end_modtype : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Libnames.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-> Libnames.object_prefix * library_segment (** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) diff --git a/library/libnames.ml b/library/libnames.ml index bd2ca550b9..f6fc5ed4b7 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,18 +162,12 @@ 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 diff --git a/library/libnames.mli b/library/libnames.mli index 447eecbb5c..9d75ec6e40 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -88,12 +88,6 @@ 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 @@ -116,8 +110,6 @@ type object_prefix = { 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 diff --git a/library/libobject.ml b/library/libobject.ml index 79a3fed1b9..ea19fbb90b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -16,6 +16,12 @@ 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 + +(* let make_oname (dirpath,(mp,dir)) id = *) +let make_oname { obj_dir; obj_mp } id = + Names.(make_path obj_dir id, KerName.make obj_mp (Label.of_id id)) + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; diff --git a/library/libobject.mli b/library/libobject.mli index aefa81b225..c53537e654 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -66,6 +66,13 @@ 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 +val make_oname : object_prefix -> Names.Id.t -> object_name + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; |