diff options
Diffstat (limited to 'library')
34 files changed, 325 insertions, 2985 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 784360dc8a..11d053624c 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -13,7 +13,6 @@ open Util open Pp open Names open Libnames -open Globnames let make_dir l = DirPath.make (List.rev_map Id.of_string l) @@ -46,7 +45,7 @@ let has_ref s = CString.Map.mem s !table let check_ind_ref s ind = match CString.Map.find s !table with - | IndRef r -> eq_ind r ind + | GlobRef.IndRef r -> eq_ind r ind | _ -> false | exception Not_found -> false @@ -105,8 +104,10 @@ let gen_reference_in_modules locstr dirs s = let check_required_library d = let dir = make_dir d in - if Library.library_is_loaded dir then () - else + try + let _ : Declarations.module_body = Global.lookup_module (ModPath.MPfile dir) in + () + with Not_found -> let in_current_dir = match Lib.current_mp () with | MPfile dp -> DirPath.equal dir dp | _ -> false @@ -157,32 +158,32 @@ let type_of_id = Constant.make2 datatypes_module @@ Label.make "IDProp" let nat_kn = MutInd.make2 datatypes_module @@ Label.make "nat" let nat_path = Libnames.make_path (make_dir datatypes_module_name) (Id.of_string "nat") -let glob_nat = IndRef (nat_kn,0) +let glob_nat = GlobRef.IndRef (nat_kn,0) let path_of_O = ((nat_kn,0),1) let path_of_S = ((nat_kn,0),2) -let glob_O = ConstructRef path_of_O -let glob_S = ConstructRef path_of_S +let glob_O = GlobRef.ConstructRef path_of_O +let glob_S = GlobRef.ConstructRef path_of_S (** Booleans *) let bool_kn = MutInd.make2 datatypes_module @@ Label.make "bool" -let glob_bool = IndRef (bool_kn,0) +let glob_bool = GlobRef.IndRef (bool_kn,0) let path_of_true = ((bool_kn,0),1) let path_of_false = ((bool_kn,0),2) -let glob_true = ConstructRef path_of_true -let glob_false = ConstructRef path_of_false +let glob_true = GlobRef.ConstructRef path_of_true +let glob_false = GlobRef.ConstructRef path_of_false (** Equality *) let eq_kn = MutInd.make2 logic_module @@ Label.make "eq" -let glob_eq = IndRef (eq_kn,0) +let glob_eq = GlobRef.IndRef (eq_kn,0) let identity_kn = MutInd.make2 datatypes_module @@ Label.make "identity" -let glob_identity = IndRef (identity_kn,0) +let glob_identity = GlobRef.IndRef (identity_kn,0) let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq" -let glob_jmeq = IndRef (jmeq_kn,0) +let glob_jmeq = GlobRef.IndRef (jmeq_kn,0) (* Sigma data *) type coq_sigma_data = { diff --git a/library/coqlib.mli b/library/coqlib.mli index f6779dbbde..ab8b18c4fb 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml deleted file mode 100644 index 8d5c2fb687..0000000000 --- a/library/decl_kinds.ml +++ /dev/null @@ -1,76 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Informal mathematical status of declarations *) - -type discharge = DoDischarge | NoDischarge - -type locality = Discharge | Local | Global - -type binding_kind = Explicit | Implicit - -type polymorphic = bool - -type private_flag = bool - -type cumulative_inductive_flag = bool - -type theorem_kind = - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary - -type definition_object_kind = - | Definition - | Coercion - | SubClass - | CanonicalStructure - | Example - | Fixpoint - | CoFixpoint - | Scheme - | StructureComponent - | IdentityCoercion - | Instance - | Method - | Let - -type assumption_object_kind = Definitional | Logical | Conjectural - -(* [assumption_kind] - - | Local | Global - ------------------------------------ - Definitional | Variable | Parameter - Logical | Hypothesis | Axiom - -*) -type assumption_kind = locality * polymorphic * assumption_object_kind -type definition_kind = locality * polymorphic * definition_object_kind - -(** Kinds used in proofs *) - -type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - -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 deleted file mode 100644 index 5fd11e187a..0000000000 --- a/library/declaremods.ml +++ /dev/null @@ -1,1015 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open CErrors -open Util -open Names -open Declarations -open Entries -open Libnames -open Libobject -open Mod_subst - -(** {6 Inlining levels} *) - -(** Rigid / flexible module signature *) - -type 'a module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - -(** Which module inline annotations should we honor, - either None or the ones whose level is less or equal - to the given integer *) - -type inline = - | NoInline - | DefaultInline - | InlineAt of int - -type module_kind = Module | ModType | ModAny - -let default_inline () = Some (Flags.get_inline_level ()) - -let inl2intopt = function - | NoInline -> None - | InlineAt i -> Some i - | DefaultInline -> default_inline () - -(** {6 Substitutive objects} - - - The list of bound identifiers is nonempty only if the objects - are owned by a functor - - - Then comes either the object segment itself (for interactive - modules), or a compact way to store derived objects (path to - a earlier module + subtitution). -*) - -type algebraic_objects = - | Objs of Lib.lib_objects - | Ref of ModPath.t * substitution - -type substitutive_objects = MBId.t list * algebraic_objects - -(** ModSubstObjs : a cache of module substitutive objects - - This table is common to modules and module types. - - For a Module M:=N, the objects of N will be reloaded - with M after substitution. - - For a Module M:SIG:=..., the module M gets its objects from SIG - - Invariants: - - A alias (i.e. a module path inside a Ref constructor) should - never lead to another alias, but rather to a concrete Objs - constructor. - - We will plug later a handler dealing with missing entries in the - cache. Such missing entries may come from inner parts of module - types, which aren't registered by the standard libobject machinery. -*) - -module ModSubstObjs : - sig - val set : ModPath.t -> substitutive_objects -> unit - val get : ModPath.t -> substitutive_objects - val set_missing_handler : (ModPath.t -> substitutive_objects) -> unit - end = - struct - let table = - Summary.ref (MPmap.empty : substitutive_objects MPmap.t) - ~name:"MODULE-SUBSTOBJS" - let missing_handler = ref (fun mp -> assert false) - let set_missing_handler f = (missing_handler := f) - let set mp objs = (table := MPmap.add mp objs !table) - let get mp = - try MPmap.find mp !table with Not_found -> !missing_handler mp - end - -(** Some utilities about substitutive objects : - substitution, expansion *) - -let sobjs_no_functor (mbids,_) = List.is_empty mbids - -let subst_aobjs sub = function - | Objs o -> Objs (Lib.subst_objects sub o) - | Ref (mp, sub0) -> Ref (mp, join sub0 sub) - -let subst_sobjs sub (mbids,aobjs) = (mbids, subst_aobjs sub aobjs) - -let expand_aobjs = function - | Objs o -> o - | Ref (mp, sub) -> - match ModSubstObjs.get mp with - | (_,Objs o) -> Lib.subst_objects sub o - | _ -> assert false (* Invariant : any alias points to concrete objs *) - -let expand_sobjs (_,aobjs) = expand_aobjs aobjs - - -(** {6 ModObjs : a cache of module objects} - - For each module, we also store a cache of - "prefix", "substituted objects", "keep objects". - This is used for instance to implement the "Import" command. - - substituted objects : - roughly the objects above after the substitution - we need to - keep them to call open_object when the module is opened (imported) - - keep objects : - The list of non-substitutive objects - as above, for each of - them we will call open_object when the module is opened - - (Some) Invariants: - * If the module is a functor, it won't appear in this cache. - - * Module objects in substitutive_objects part have empty substituted - objects. - - * Modules which where created with Module M:=mexpr or with - Module M:SIG. ... End M. have the keep list empty. -*) - -type module_objects = Nametab.object_prefix * Lib.lib_objects * Lib.lib_objects - -module ModObjs : - sig - val set : ModPath.t -> module_objects -> unit - val get : ModPath.t -> module_objects (* may raise Not_found *) - val all : unit -> module_objects MPmap.t - end = - struct - let table = - Summary.ref (MPmap.empty : module_objects MPmap.t) - ~name:"MODULE-OBJS" - let set mp objs = (table := MPmap.add mp objs !table) - let get mp = MPmap.find mp !table - let all () = !table - end - - -(** {6 Name management} - - Auxiliary functions to transform full_path and kernel_name given - by Lib into ModPath.t and DirPath.t needed for modules -*) - -let mp_of_kn kn = - let mp,l = KerName.repr kn in - MPdot (mp,l) - -let dir_of_sp sp = - let dir,id = repr_path sp in - add_dirpath_suffix dir id - - -(** {6 Declaration of module substitutive objects} *) - -(** These functions register the visibility of the module and iterates - through its components. They are called by plenty of module functions *) - -let consistency_checks exists dir dirinfo = - if exists then - let globref = - try Nametab.locate_dir (qualid_of_dirpath dir) - with Not_found -> - user_err ~hdr:"consistency_checks" - (DirPath.print dir ++ str " should already exist!") - in - assert (Nametab.GlobDirRef.equal globref dirinfo) - else - if Nametab.exists_dir dir then - user_err ~hdr:"consistency_checks" - (DirPath.print dir ++ str " already exists") - -let compute_visibility exists i = - if exists then Nametab.Exactly i else Nametab.Until 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 = 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; - (* If we're not a functor, let's iter on the internal components *) - if sobjs_no_functor sobjs then begin - let objs = expand_sobjs sobjs in - ModObjs.set obj_mp (prefix,objs,kobjs); - iter_objects (i+1) prefix objs; - iter_objects (i+1) prefix kobjs - end - -let do_module' exists iter_objects i ((sp,kn),sobjs) = - do_module exists iter_objects i (dir_of_sp sp) (mp_of_kn kn) sobjs [] - -(** Nota: Interactive modules and module types cannot be recached! - This used to be checked here via a flag along the substobjs. *) - -let cache_module = do_module' false Lib.load_objects 1 -let load_module = do_module' false Lib.load_objects -let open_module = do_module' true Lib.open_objects -let subst_module (subst,sobjs) = subst_sobjs subst sobjs -let classify_module sobjs = Substitute sobjs - -let (in_module : substitutive_objects -> obj), - (out_module : obj -> substitutive_objects) = - declare_object_full {(default_object "MODULE") with - cache_function = cache_module; - load_function = load_module; - open_function = open_module; - subst_function = subst_module; - classify_function = classify_module } - - -(** {6 Declaration of module keep objects} *) - -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 = 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 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 = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in - Lib.open_objects i prefix kobjs - -let in_modkeep : Lib.lib_objects -> obj = - declare_object {(default_object "MODULE KEEP") with - cache_function = cache_keep; - load_function = load_keep; - open_function = open_keep } - - -(** {6 Declaration of module type substitutive objects} *) - -(** Nota: Interactive modules and module types cannot be recached! - This used to be checked more properly here. *) - -let do_modtype i sp mp sobjs = - if Nametab.exists_modtype sp then - anomaly (pr_path sp ++ str " already exists."); - Nametab.push_modtype (Nametab.Until i) sp mp; - ModSubstObjs.set mp sobjs - -let cache_modtype ((sp,kn),sobjs) = do_modtype 1 sp (mp_of_kn kn) sobjs -let load_modtype i ((sp,kn),sobjs) = do_modtype i sp (mp_of_kn kn) sobjs -let subst_modtype (subst,sobjs) = subst_sobjs subst sobjs -let classify_modtype sobjs = Substitute sobjs - -let open_modtype i ((sp,kn),_) = - let mp = mp_of_kn kn in - let mp' = - try Nametab.locate_modtype (qualid_of_path sp) - with Not_found -> - anomaly (pr_path sp ++ str " should already exist!"); - in - assert (ModPath.equal mp mp'); - Nametab.push_modtype (Nametab.Exactly i) sp mp - -let (in_modtype : substitutive_objects -> obj), - (out_modtype : obj -> substitutive_objects) = - declare_object_full {(default_object "MODULE TYPE") with - cache_function = cache_modtype; - open_function = open_modtype; - load_function = load_modtype; - subst_function = subst_modtype; - classify_function = classify_modtype } - - -(** {6 Declaration of substitutive objects for Include} *) - -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 = 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 - -let cache_include = do_include true true 1 -let load_include = do_include true false -let open_include = do_include false true -let subst_include (subst,aobjs) = subst_aobjs subst aobjs -let classify_include aobjs = Substitute aobjs - -let (in_include : algebraic_objects -> obj), - (out_include : obj -> algebraic_objects) = - declare_object_full {(default_object "INCLUDE") with - cache_function = cache_include; - load_function = load_include; - open_function = open_include; - subst_function = subst_include; - classify_function = classify_include } - - -(** {6 Handler for missing entries in ModSubstObjs} *) - -(** Since the inner of Module Types are not added by default to - the ModSubstObjs table, we compensate this by explicit traversal - of Module Types inner objects when needed. Quite a hack... *) - -let mp_id mp id = MPdot (mp, Label.of_id id) - -let rec register_mod_objs mp (id,obj) = match object_tag obj with - | "MODULE" -> ModSubstObjs.set (mp_id mp id) (out_module obj) - | "MODULE TYPE" -> ModSubstObjs.set (mp_id mp id) (out_modtype obj) - | "INCLUDE" -> - List.iter (register_mod_objs mp) (expand_aobjs (out_include obj)) - | _ -> () - -let handle_missing_substobjs mp = match mp with - | MPdot (mp',l) -> - let objs = expand_sobjs (ModSubstObjs.get mp') in - List.iter (register_mod_objs mp') objs; - ModSubstObjs.get mp - | _ -> - assert false (* Only inner parts of module types should be missing *) - -let () = ModSubstObjs.set_missing_handler handle_missing_substobjs - - - -(** {6 From module expression to substitutive objects} *) - -(** Turn a chain of [MSEapply] into the head ModPath.t and the - list of ModPath.t parameters (deepest param coming first). - The left part of a [MSEapply] must be either [MSEident] or - another [MSEapply]. *) - -let get_applications mexpr = - let rec get params = function - | MEident mp -> mp, params - | MEapply (fexpr, mp) -> get (mp::params) fexpr - | MEwith _ -> user_err Pp.(str "Non-atomic functor application.") - in get [] mexpr - -(** Create the substitution corresponding to some functor applications *) - -let rec compute_subst env mbids sign mp_l inl = - match mbids,mp_l with - | _,[] -> mbids,empty_subst - | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") - | mbid::mbids,mp::mp_l -> - let farg_id, farg_b, fbody_b = Modops.destr_functor sign in - let mb = Environ.lookup_module mp env in - let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in - let resolver = - if Modops.is_functor mb.mod_type then empty_delta_resolver - else - Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta - in - mbid_left,join (map_mbid mbid mp resolver) subst - -(** Create the objects of a "with Module" structure. *) - -let rec replace_module_object idl mp0 objs0 mp1 objs1 = - match idl, objs0 with - | _,[] -> [] - | id::idl,(id',obj)::tail when Id.equal id id' -> - assert (String.equal (object_tag obj) "MODULE"); - let mp_id = MPdot(mp0, Label.of_id id) in - let objs = match idl with - | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 - | _ -> - let objs_id = expand_sobjs (out_module obj) in - replace_module_object idl mp_id objs_id mp1 objs1 - in - (id, in_module ([], Objs objs))::tail - | idl,lobj::tail -> lobj::replace_module_object idl mp0 tail mp1 objs1 - -let type_of_mod mp env = function - |true -> (Environ.lookup_module mp env).mod_type - |false -> (Environ.lookup_modtype mp env).mod_type - -let rec get_module_path = function - |MEident mp -> mp - |MEwith (me,_) -> get_module_path me - |MEapply (me,_) -> get_module_path me - -(** Substitutive objects of a module expression (or module type) *) - -let rec get_module_sobjs is_mod env inl = function - |MEident mp -> - begin match ModSubstObjs.get mp with - |(mbids,Objs _) when not (ModPath.is_bound mp) -> - (mbids,Ref (mp, empty_subst)) (* we create an alias *) - |sobjs -> sobjs - end - |MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty - |MEwith (mty, WithMod (idl,mp1)) -> - assert (not is_mod); - let sobjs0 = get_module_sobjs is_mod env inl mty in - assert (sobjs_no_functor sobjs0); - (* For now, we expanse everything, to be safe *) - let mp0 = get_module_path mty in - let objs0 = expand_sobjs sobjs0 in - let objs1 = expand_sobjs (ModSubstObjs.get mp1) in - ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1)) - |MEapply _ as me -> - let mp1, mp_l = get_applications me in - let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in - let typ = type_of_mod mp1 env is_mod in - let mbids_left,subst = compute_subst env mbids typ mp_l inl in - (mbids_left, subst_aobjs subst aobjs) - -let get_functor_sobjs is_mod env inl (params,mexpr) = - let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in - (List.map fst params @ mbids, aobjs) - - -(** {6 Handling of module parameters} *) - -(** For printing modules, [process_module_binding] adds names of - bound module (and its components) to Nametab. It also loads - objects associated to it. *) - -let process_module_binding mbid me = - let dir = DirPath.make [MBId.to_id mbid] in - let mp = MPbound mbid in - let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in - let subst = map_mp (get_module_path me) mp empty_delta_resolver in - let sobjs = subst_sobjs subst sobjs in - do_module false Lib.load_objects 1 dir mp sobjs [] - -(** Process a declaration of functor parameter(s) (Id1 .. Idn : Typ) - i.e. possibly multiple names with the same module type. - Global environment is updated on the fly. - Objects in these parameters are also loaded. - Output is accumulated on top of [acc] (in reverse order). *) - -let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = - let inl = inl2intopt ann in - let lib_dir = Lib.library_dp() in - let env = Global.env() in - let (mty, _, cst') = interp_modast env ModType typ in - let () = Global.push_context_set true cst' in - let env = Global.env () in - let sobjs = get_module_sobjs false env inl mty in - let mp0 = get_module_path mty in - let fold acc {CAst.v=id} = - let dir = DirPath.make [id] in - let mbid = MBId.make lib_dir id in - let mp = MPbound mbid in - let resolver = Global.add_module_parameter mbid mty inl in - let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in - do_module false Lib.load_objects 1 dir mp sobjs []; - (mbid,mty,inl)::acc - in - let acc = List.fold_left fold acc idl in - (acc, Univ.ContextSet.union cst cst') - -(** Process a list of declarations of functor parameters - (Id11 .. Id1n : Typ1)..(Idk1 .. Idkm : Typk) - Global environment is updated on the fly. - The calls to [interp_modast] should be interleaved with these - env updates, otherwise some "with Definition" could be rejected. - Returns a list of mbids and entries (in reversed order). - - This used to be a [List.concat (List.map ...)], but this should - be more efficient and independent of [List.map] eval order. -*) - -let intern_args interp_modast params = - List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params - - -(** {6 Auxiliary functions concerning subtyping checks} *) - -let check_sub mtb sub_mtb_l = - (* The constraints are checked and forgot immediately : *) - ignore (List.fold_right - (fun sub_mtb env -> - Environ.add_constraints - (Subtyping.check_subtypes env mtb sub_mtb) env) - sub_mtb_l (Global.env())) - -(** This function checks if the type calculated for the module [mp] is - a subtype of all signatures in [sub_mtb_l]. Uses only the global - environment. *) - -let check_subtypes mp sub_mtb_l = - let mb = - try Global.lookup_module mp with Not_found -> assert false - in - let mtb = Modops.module_type_of_module mb in - check_sub mtb sub_mtb_l - -(** Same for module type [mp] *) - -let check_subtypes_mt mp sub_mtb_l = - let mtb = - try Global.lookup_modtype mp with Not_found -> assert false - in - check_sub mtb sub_mtb_l - -(** Create a params entry. - In [args], the youngest module param now comes first. *) - -let mk_params_entry args = - List.rev_map (fun (mbid,arg_t,_) -> (mbid,arg_t)) args - -(** Create a functor type struct. - In [args], the youngest module param now comes first. *) - -let mk_funct_type env args seb0 = - List.fold_left - (fun seb (arg_id,arg_t,arg_inl) -> - let mp = MPbound arg_id in - let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in - MoreFunctor(arg_id,arg_t,seb)) - seb0 args - -(** Prepare the module type list for check of subtypes *) - -let build_subtypes interp_modast env mp args mtys = - let (cst, ans) = List.fold_left_map - (fun cst (m,ann) -> - let inl = inl2intopt ann in - let mte, _, cst' = interp_modast env ModType m in - let env = Environ.push_context_set ~strict:true cst' env in - let cst = Univ.ContextSet.union cst cst' in - let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in - cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type }) - Univ.ContextSet.empty mtys - in - (ans, cst) - - -(** {6 Current module information} - - This information is stored by each [start_module] for use - in a later [end_module]. *) - -type current_module_info = { - cur_typ : (module_struct_entry * int option) option; (** type via ":" *) - cur_typs : module_type_body list (** types via "<:" *) -} - -let default_module_info = { cur_typ = None; cur_typs = [] } - -let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO" - - -(** {6 Current module type information} - - This information is stored by each [start_modtype] for use - in a later [end_modtype]. *) - -let openmodtype_info = - Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" - - -(** {6 Modules : start, end, declare} *) - -module RawModOps = struct - -let start_module interp_modast export id args res fs = - let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in - let () = Global.push_context_set true cst in - let env = Global.env () in - let res_entry_o, subtyps, cst = match res with - | Enforce (res,ann) -> - let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType res in - let env = Environ.push_context_set ~strict:true cst env in - (* We check immediately that mte is well-formed *) - let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in - let cst = Univ.ContextSet.union cst cst' in - Some (mte, inl), [], cst - | Check resl -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in - None, typs, cst - in - 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 (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix)); - mp - -let end_module () = - let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in - let substitute, keep, special = Lib.classify_segment lib_stack in - let m_info = !openmod_info in - - (* For sealed modules, we use the substitutive objects of their signatures *) - let sobjs0, keep, special = match m_info.cur_typ with - | None -> ([], Objs substitute), keep, special - | Some (mty, inline) -> - get_module_sobjs false (Global.env()) inline mty, [], [] - in - let id = basename (fst oldoname) in - let mp,mbids,resolver = Global.end_module fs id m_info.cur_typ in - let sobjs = let (ms,objs) = sobjs0 in (mbids@ms,objs) in - - check_subtypes mp m_info.cur_typs; - - (* We substitute objects if the module is sealed by a signature *) - let sobjs = - match m_info.cur_typ with - | None -> sobjs - | Some (mty, _) -> - subst_sobjs (map_mp (get_module_path mty) mp resolver) sobjs - in - let node = in_module sobjs in - (* We add the keep objects, if any, and if this isn't a functor *) - let objects = match keep, mbids with - | [], _ | _, _ :: _ -> special@[node] - | _ -> special@[node;in_modkeep keep] - in - let newoname = Lib.add_leaves id objects in - - (* Name consistency check : start_ vs. end_module, kernel vs. library *) - assert (eq_full_path (fst newoname) (fst oldoname)); - assert (ModPath.equal (mp_of_kn (snd newoname)) mp); - - mp - -let declare_module interp_modast id args res mexpr_o fs = - (* We simulate the beginning of an interactive module, - then we adds the module parameters to the global env. *) - let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in - let params = mk_params_entry arg_entries_r in - let env = Global.env () in - let env = Environ.push_context_set ~strict:true cst env in - let mty_entry_o, subs, inl_res, cst' = match res with - | Enforce (mty,ann) -> - let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType mty in - let env = Environ.push_context_set ~strict:true cst env in - (* We check immediately that mte is well-formed *) - let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in - let cst = Univ.ContextSet.union cst cst' in - Some mte, [], inl, cst - | Check mtys -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in - None, typs, default_inline (), cst - in - let env = Environ.push_context_set ~strict:true cst' env in - let cst = Univ.ContextSet.union cst cst' in - let mexpr_entry_o, inl_expr, cst' = match mexpr_o with - | None -> None, default_inline (), Univ.ContextSet.empty - | Some (mexpr,ann) -> - let (mte, _, cst) = interp_modast env Module mexpr in - Some mte, inl2intopt ann, cst - in - let env = Environ.push_context_set ~strict:true cst' env in - let cst = Univ.ContextSet.union cst cst' in - let entry = match mexpr_entry_o, mty_entry_o with - | None, None -> assert false (* No body, no type ... *) - | None, Some typ -> MType (params, typ) - | Some body, otyp -> MExpr (params, body, otyp) - in - let sobjs, mp0 = match entry with - | MType (_,mte) | MExpr (_,_,Some mte) -> - get_functor_sobjs false env inl_res (params,mte), get_module_path mte - | MExpr (_,me,None) -> - get_functor_sobjs true env inl_expr (params,me), get_module_path me - in - (* Undo the simulated interactive building of the module - and declare the module as a whole *) - Summary.unfreeze_summaries fs; - let inl = match inl_expr with - | None -> None - | _ -> inl_res - in - let () = Global.push_context_set true cst in - let mp_env,resolver = Global.add_module id entry inl in - - (* Name consistency check : kernel vs. library *) - assert (ModPath.equal mp (mp_of_kn (Lib.make_kn id))); - assert (ModPath.equal mp mp_env); - - check_subtypes mp subs; - - let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in - ignore (Lib.add_leaf id (in_module sobjs)); - mp - -end - -(** {6 Module types : start, end, declare} *) - -module RawModTypeOps = struct - -let start_modtype interp_modast id args mtys fs = - let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in - let () = Global.push_context_set true cst in - let env = Global.env () in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in - 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 (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix)); - mp - -let end_modtype () = - let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in - let id = basename (fst oldoname) in - let substitute, _, special = Lib.classify_segment lib_stack in - let sub_mty_l = !openmodtype_info in - let mp, mbids = Global.end_modtype fs id in - let modtypeobjs = (mbids, Objs substitute) in - check_subtypes_mt mp sub_mty_l; - let oname = Lib.add_leaves id (special@[in_modtype modtypeobjs]) - in - (* Check name consistence : start_ vs. end_modtype, kernel vs. library *) - assert (eq_full_path (fst oname) (fst oldoname)); - assert (ModPath.equal (mp_of_kn (snd oname)) mp); - - mp - -let declare_modtype interp_modast id args mtys (mty,ann) fs = - let inl = inl2intopt ann in - (* We simulate the beginning of an interactive module, - then we adds the module parameters to the global env. *) - let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in - let () = Global.push_context_set true cst in - let params = mk_params_entry arg_entries_r in - let env = Global.env () in - let mte, _, cst = interp_modast env ModType mty in - let () = Global.push_context_set true cst in - let env = Global.env () in - (* We check immediately that mte is well-formed *) - let _, _, _, cst = Mod_typing.translate_mse env None inl mte in - let () = Global.push_context_set true cst in - let env = Global.env () in - let entry = params, mte in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in - let () = Global.push_context_set true cst in - let env = Global.env () in - let sobjs = get_functor_sobjs false env inl entry in - let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in - let sobjs = subst_sobjs subst sobjs in - - (* Undo the simulated interactive building of the module type - and declare the module type as a whole *) - Summary.unfreeze_summaries fs; - - (* We enrich the global environment *) - let mp_env = Global.add_modtype id entry inl in - - (* Name consistency check : kernel vs. library *) - assert (ModPath.equal mp_env mp); - - (* Subtyping checks *) - check_subtypes_mt mp sub_mty_l; - - ignore (Lib.add_leaf id (in_modtype sobjs)); - mp - -end - -(** {6 Include} *) - -module RawIncludeOps = struct - -let rec include_subst env mp reso mbids sign inline = match mbids with - | [] -> empty_subst - | mbid::mbids -> - let farg_id, farg_b, fbody_b = Modops.destr_functor sign in - let subst = include_subst env mp reso mbids fbody_b inline in - let mp_delta = - Modops.inline_delta_resolver env inline mp farg_id farg_b reso - in - join (map_mbid mbid mp mp_delta) subst - -let rec decompose_functor mpl typ = - match mpl, typ with - | [], _ -> typ - | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str - | _ -> user_err Pp.(str "Application of a functor with too much arguments.") - -exception NoIncludeSelf - -let type_of_incl env is_mod = function - |MEident mp -> type_of_mod mp env is_mod - |MEapply _ as me -> - let mp0, mp_l = get_applications me in - decompose_functor mp_l (type_of_mod mp0 env is_mod) - |MEwith _ -> raise NoIncludeSelf - -let declare_one_include interp_modast (me_ast,annot) = - let env = Global.env() in - let me, kind, cst = interp_modast env ModAny me_ast in - let () = Global.push_context_set true cst in - let env = Global.env () in - let is_mod = (kind == Module) in - let cur_mp = Lib.current_mp () in - let inl = inl2intopt annot in - let mbids,aobjs = get_module_sobjs is_mod env inl me in - let subst_self = - try - if List.is_empty mbids then raise NoIncludeSelf; - let typ = type_of_incl env is_mod me in - let reso,_ = Safe_typing.delta_of_senv (Global.safe_env ()) in - include_subst env cur_mp reso mbids typ inl - with NoIncludeSelf -> empty_subst - in - let base_mp = get_module_path me in - let resolver = Global.add_include me is_mod inl in - let subst = join subst_self (map_mp base_mp cur_mp resolver) in - let aobjs = subst_aobjs subst aobjs in - ignore (Lib.add_leaf (Lib.current_mod_id ()) (in_include aobjs)) - -let declare_include interp me_asts = - List.iter (declare_one_include interp) me_asts - -end - - -(** {6 Module operations handling summary freeze/unfreeze} *) - -let protect_summaries f = - let fs = Summary.freeze_summaries ~marshallable:false in - try f fs - with reraise -> - (* Something wrong: undo the whole process *) - let reraise = CErrors.push reraise in - let () = Summary.unfreeze_summaries fs in - iraise reraise - -let start_module interp export id args res = - protect_summaries (RawModOps.start_module interp export id args res) - -let end_module = RawModOps.end_module - -let declare_module interp id args mtys me_l = - let declare_me fs = match me_l with - | [] -> RawModOps.declare_module interp id args mtys None fs - | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs - | me_l -> - ignore (RawModOps.start_module interp None id args mtys fs); - RawIncludeOps.declare_include interp me_l; - RawModOps.end_module () - in - protect_summaries declare_me - -let start_modtype interp id args mtys = - protect_summaries (RawModTypeOps.start_modtype interp id args mtys) - -let end_modtype = RawModTypeOps.end_modtype - -let declare_modtype interp id args mtys mty_l = - let declare_mt fs = match mty_l with - | [] -> assert false - | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs - | mty_l -> - ignore (RawModTypeOps.start_modtype interp id args mtys fs); - RawIncludeOps.declare_include interp mty_l; - RawModTypeOps.end_modtype () - in - protect_summaries declare_mt - -let declare_include interp me_asts = - protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts) - - -(** {6 Libraries} *) - -type library_name = DirPath.t - -(** A library object is made of some substitutive objects - and some "keep" objects. *) - -type library_objects = Lib.lib_objects * Lib.lib_objects - -(** For the native compiler, we cache the library values *) - -let register_library dir cenv (objs:library_objects) digest univ = - let mp = MPfile dir in - let () = - try - (* Is this library already loaded ? *) - ignore(Global.lookup_module mp); - with Not_found -> - (* If not, let's do it now ... *) - let mp' = Global.import cenv univ digest in - if not (ModPath.equal mp mp') then - anomaly (Pp.str "Unexpected disk module name."); - in - let sobjs,keepobjs = objs in - do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs - -let get_library_native_symbols dir = - Safe_typing.get_library_native_symbols (Global.safe_env ()) dir - -let start_library dir = - let mp = Global.start_library dir in - openmod_info := default_module_info; - Lib.start_compilation dir mp - -let end_library_hook = ref ignore -let append_end_library_hook f = - let old_f = !end_library_hook in - end_library_hook := fun () -> old_f(); f () - -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 ~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 - cenv,(substitute,keep),ast - - - -(** {6 Implementation of Import and Export commands} *) - -let really_import_module mp = - (* May raise Not_found for unknown module and for functors *) - let prefix,sobjs,keepobjs = ModObjs.get mp in - Lib.open_objects 1 prefix sobjs; - Lib.open_objects 1 prefix keepobjs - -let cache_import (_,(_,mp)) = really_import_module mp - -let open_import i obj = - if Int.equal i 1 then cache_import obj - -let classify_import (export,_ as obj) = - if export then Substitute obj else Dispose - -let subst_import (subst,(export,mp as obj)) = - let mp' = subst_mp subst mp in - if mp'==mp then obj else (export,mp') - -let in_import : bool * ModPath.t -> obj = - declare_object {(default_object "IMPORT MODULE") with - cache_function = cache_import; - open_function = open_import; - subst_function = subst_import; - classify_function = classify_import } - -let import_module export mp = - Lib.add_anonymous_leaf (in_import (export,mp)) - - -(** {6 Iterators} *) - -let iter_all_segments f = - let rec apply_obj prefix (id,obj) = match object_tag obj with - | "INCLUDE" -> - let objs = expand_aobjs (out_include obj) in - List.iter (apply_obj prefix) objs - | _ -> f (Lib.make_oname prefix id) obj - in - let apply_mod_obj _ (prefix,substobjs,keepobjs) = - List.iter (apply_obj prefix) substobjs; - List.iter (apply_obj prefix) keepobjs - in - let apply_node = function - | sp, Lib.Leaf o -> f sp o - | _ -> () - in - MPmap.iter apply_mod_obj (ModObjs.all ()); - List.iter apply_node (Lib.contents ()) - - -(** {6 Some types used to shorten declaremods.mli} *) - -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** {6 Debug} *) - -let debug_print_modtab _ = - let pr_seg = function - | [] -> str "[]" - | l -> str "[." ++ int (List.length l) ++ str ".]" - in - let pr_modinfo mp (prefix,substobjs,keepobjs) s = - s ++ str (ModPath.to_string mp) ++ (spc ()) - ++ (pr_seg (Lib.segment_of_objects prefix (substobjs@keepobjs))) - in - let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in - hov 0 modules diff --git a/library/declaremods.mli b/library/declaremods.mli deleted file mode 100644 index 2b28ba908e..0000000000 --- a/library/declaremods.mli +++ /dev/null @@ -1,144 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names - -(** {6 Modules } *) - -(** Rigid / flexible module signature *) - -type 'a module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - -(** Which module inline annotations should we honor, - either None or the ones whose level is less or equal - to the given integer *) - -type inline = - | NoInline - | DefaultInline - | InlineAt of int - -(** Kinds of modules *) - -type module_kind = Module | ModType | ModAny - -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** [declare_module interp_modast id fargs typ exprs] - declares module [id], with structure constructed by [interp_modast] - from functor arguments [fargs], with final type [typ]. - [exprs] is usually of length 1 (Module definition with a concrete - body), but it could also be empty ("Declare Module", with non-empty [typ]), - or multiple (body of the shape M <+ N <+ ...). *) - -val declare_module : - 'modast module_interpretor -> - Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> - ('modast * inline) list -> ModPath.t - -val start_module : - 'modast module_interpretor -> - bool option -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> ModPath.t - -val end_module : unit -> ModPath.t - - - -(** {6 Module types } *) - -(** [declare_modtype interp_modast id fargs typs exprs] - Similar to [declare_module], except that the types could be multiple *) - -val declare_modtype : - 'modast module_interpretor -> - Id.t -> - 'modast module_params -> - ('modast * inline) list -> - ('modast * inline) list -> - ModPath.t - -val start_modtype : - 'modast module_interpretor -> - Id.t -> - 'modast module_params -> - ('modast * inline) list -> ModPath.t - -val end_modtype : unit -> ModPath.t - -(** {6 Libraries i.e. modules on disk } *) - -type library_name = DirPath.t - -type library_objects - -val register_library : - library_name -> - Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> - Univ.ContextSet.t -> unit - -val get_library_native_symbols : library_name -> Nativecode.symbols - -val start_library : library_name -> unit - -val end_library : - ?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 *) -val append_end_library_hook : (unit -> unit) -> unit - -(** [really_import_module mp] opens the module [mp] (in a Caml sense). - It modifies Nametab and performs the [open_object] function for - every object of the module. Raises [Not_found] when [mp] is unknown - or when [mp] corresponds to a functor. *) - -val really_import_module : ModPath.t -> unit - -(** [import_module export mp] is a synchronous version of - [really_import_module]. If [export] is [true], the module is also - opened every time the module containing it is. *) - -val import_module : bool -> ModPath.t -> unit - -(** Include *) - -val declare_include : - 'modast module_interpretor -> ('modast * inline) list -> unit - -(** {6 ... } *) -(** [iter_all_segments] iterate over all segments, the modules' - segments first and then the current segment. Modules are presented - in an arbitrary order. The given function is applied to all leaves - (together with their section path). *) - -val iter_all_segments : - (Libobject.object_name -> Libobject.obj -> unit) -> unit - - -val debug_print_modtab : unit -> Pp.t - -(** For printing modules, [process_module_binding] adds names of - bound module (and its components) to Nametab. It also loads - objects associated to it. It may raise a [Failure] when the - bound module hasn't an atomic type. *) - -val process_module_binding : - MBId.t -> Declarations.module_alg_expr -> unit diff --git a/library/decls.ml b/library/decls.ml deleted file mode 100644 index b766b6e2cb..0000000000 --- a/library/decls.ml +++ /dev/null @@ -1,46 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** This module registers tables for some non-logical informations - associated declarations *) - -open Names -open Decl_kinds -open Libnames - -(** Datas associated to section variables and local definitions *) - -type variable_data = - DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind - -let vartab = - Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" - -let add_variable_data id o = vartab := Id.Map.add id o !vartab - -let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p -let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq -let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k -let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx -let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p - -let variable_secpath id = - let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in - make_qualid dir id - -let variable_exists id = Id.Map.mem id !vartab - -(** Datas associated to global parameters and constants *) - -let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT" - -let add_constant_kind kn k = csttab := Cmap.add kn k !csttab - -let constant_kind kn = Cmap.find kn !csttab diff --git a/library/decls.mli b/library/decls.mli deleted file mode 100644 index c0db537427..0000000000 --- a/library/decls.mli +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Libnames -open Decl_kinds - -(** This module manages non-kernel informations about declarations. It - is either non-logical informations or logical informations that - have no place to be (yet) in the kernel *) - -(** Registration and access to the table of variable *) - -type variable_data = - DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind - -val add_variable_data : variable -> variable_data -> unit -val variable_path : variable -> DirPath.t -val variable_secpath : variable -> qualid -val variable_kind : variable -> logical_kind -val variable_opacity : variable -> bool -val variable_context : variable -> Univ.ContextSet.t -val variable_polymorphic : variable -> polymorphic -val variable_exists : variable -> bool - -(** Registration and access to the table of constants *) - -val add_constant_kind : Constant.t -> logical_kind -> unit -val constant_kind : Constant.t -> logical_kind diff --git a/library/global.ml b/library/global.ml index d9f8a6ffa3..c4685370d1 100644 --- a/library/global.ml +++ b/library/global.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -71,6 +71,11 @@ let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ())) let globalize f = let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res +let globalize0_with_summary fs f = + let env = f (safe_env ()) in + Summary.unfreeze_summaries fs; + GlobalSafeEnv.set_safe_env env + let globalize_with_summary fs f = let res,env = f (safe_env ()) in Summary.unfreeze_summaries fs; @@ -83,23 +88,30 @@ let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let push_section_context c = globalize0 (Safe_typing.push_section_context c) 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 set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c) +let set_check_positive c = globalize0 (Safe_typing.set_check_positive c) +let set_check_universes c = globalize0 (Safe_typing.set_check_universes 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_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) +let open_section () = globalize0 Safe_typing.open_section +let close_section fs = globalize0_with_summary fs Safe_typing.close_section + let start_module id = globalize (Safe_typing.start_module (i2l id)) let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) @@ -115,6 +127,7 @@ let add_module_parameter mbid mte inl = (** Queries on the global environment *) let universes () = universes (env()) +let universes_lbound () = universes_lbound (env()) let named_context () = named_context (env()) let named_context_val () = named_context_val (env()) @@ -131,9 +144,25 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let body_of_constant_body ce = body_of_constant_body (env ()) ce - -let body_of_constant cst = body_of_constant_body (lookup_constant cst) +let body_of_constant_body access env cb = + let open Declarations in + let otab = Environ.opaque_tables env in + match cb.const_body with + | Undef _ | Primitive _ -> + None + | Def c -> + let u = match cb.const_universes with + | Monomorphic _ -> Opaqueproof.PrivateMonomorphic () + | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) + in + Some (Mod_subst.force_constr c, u, Declareops.constant_polymorphic_context cb) + | OpaqueDef o -> + let c, u = Opaqueproof.force_proof access otab o in + Some (c, u, Declareops.constant_polymorphic_context cb) + +let body_of_constant_body access ce = body_of_constant_body access (env ()) ce + +let body_of_constant access cst = body_of_constant_body access (lookup_constant cst) (** Operations on kernel names *) @@ -157,16 +186,14 @@ let import c u d = globalize (Safe_typing.import c u d) let env_of_context hyps = reset_with_named_context hyps (env()) -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 = is_template_polymorphic (env ()) r +let is_template_checked r = is_template_checked (env ()) r + +let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r + let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = diff --git a/library/global.mli b/library/global.mli index ca88d2dafd..c45bf65d84 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -22,6 +22,7 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool val universes : unit -> UGraph.t +val universes_lbound : unit -> Univ.Level.t val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Constr.named_context @@ -31,6 +32,9 @@ val named_context : unit -> Constr.named_context val set_engagement : Declarations.engagement -> unit val set_indices_matter : bool -> unit val set_typing_flags : Declarations.typing_flags -> unit +val set_check_guarded : bool -> unit +val set_check_positive : bool -> unit +val set_check_universes : bool -> unit val typing_flags : unit -> Declarations.typing_flags val make_sprop_cumulative : unit -> unit val set_allow_sprop : bool -> unit @@ -38,15 +42,16 @@ val sprop_allowed : unit -> bool (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit +val push_named_assum : (Id.t * Constr.types) -> unit val push_named_def : (Id.t * Entries.section_def_entry) -> unit +val push_section_context : (Name.t array * Univ.UContext.t) -> unit val export_private_constants : in_section:bool -> - Safe_typing.private_constants Entries.definition_entry -> - unit Entries.definition_entry * Safe_typing.exported_private_constant list + Safe_typing.private_constants Entries.proof_output -> + Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : - in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t + side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -66,6 +71,15 @@ val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver +(** Sections *) + +val open_section : unit -> unit +(** [poly] is true when the section should be universe polymorphic *) + +val close_section : Summary.frozen -> unit +(** Close the section and reset the global state to the one at the time when + the section what opened. *) + (** Interactive modules and module types *) val start_module : Id.t -> ModPath.t @@ -84,7 +98,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) val lookup_named : variable -> Constr.named_declaration -val lookup_constant : Constant.t -> Declarations.constant_body +val lookup_constant : Constant.t -> Opaqueproof.opaque Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body val lookup_pinductive : Constr.pinductive -> @@ -99,13 +113,16 @@ val mind_of_delta_kn : KerName.t -> MutInd.t val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> + (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option (** Returns the body of the constant if it has any, and the polymorphic context it lives in. For monomorphic constant, the latter is empty, and for polymorphic constants, the term contains De Bruijn universe variables that need to be instantiated. *) -val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant_body : Opaqueproof.indirect_accessor -> + Opaqueproof.opaque Declarations.constant_body -> + (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** {6 Compiled libraries } *) @@ -129,20 +146,10 @@ val is_joined_environment : unit -> bool val is_polymorphic : GlobRef.t -> bool val is_template_polymorphic : GlobRef.t -> bool +val is_template_checked : GlobRef.t -> bool +val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list val is_type_in_type : GlobRef.t -> bool -val constr_of_global_in_context : Environ.env -> - GlobRef.t -> Constr.types * Univ.AUContext.t - [@@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 - [@@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_inline : Constant.t -> unit diff --git a/library/globnames.ml b/library/globnames.ml index db2e8bfaed..acb05f9ac0 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,12 +12,14 @@ open Names open Constr open Mod_subst -(*s Global reference is a kernel side type for all references together *) type global_reference = GlobRef.t = - | VarRef of variable (** A reference to the section-context. *) - | ConstRef of Constant.t (** A reference to the environment. *) - | IndRef of inductive (** A reference to an inductive type. *) - | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + | VarRef of variable [@ocaml.deprecated "Use Names.GlobRef.VarRef"] + | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"] + | IndRef of inductive [@ocaml.deprecated "Use Names.GlobRef.IndRef"] + | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"] +[@@ocaml.deprecated "Use Names.GlobRef.t"] + +open GlobRef let isVarRef = function VarRef _ -> true | _ -> false let isConstRef = function ConstRef _ -> true | _ -> false @@ -85,21 +87,12 @@ let printable_constr_of_global = function | ConstructRef sp -> mkConstruct sp | IndRef sp -> mkInd sp -module RefOrdered = Names.GlobRef.Ordered -module RefOrdered_env = Names.GlobRef.Ordered_env - -module Refmap = Names.GlobRef.Map -module Refset = Names.GlobRef.Set - -module Refmap_env = Names.GlobRef.Map_env -module Refset_env = Names.GlobRef.Set_env - (* Extended global references *) type syndef_name = KerName.t type extended_global_reference = - | TrueGlobal of global_reference + | TrueGlobal of GlobRef.t | SynDef of syndef_name (* We order [extended_global_reference] via their user part @@ -131,9 +124,6 @@ module ExtRefOrdered = struct end -type global_reference_or_constr = - | IsGlobal of global_reference +type global_reference_or_constr = + | IsGlobal of GlobRef.t | IsConstr of constr - -(* Deprecated *) -let eq_gr = GlobRef.equal diff --git a/library/globnames.mli b/library/globnames.mli index d49ed453f5..fc0de96e36 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,12 +12,11 @@ open Names open Constr open Mod_subst -(** {6 Global reference is a kernel side type for all references together } *) type global_reference = GlobRef.t = - | VarRef of variable (** A reference to the section-context. *) - | ConstRef of Constant.t (** A reference to the environment. *) - | IndRef of inductive (** A reference to an inductive type. *) - | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + | VarRef of variable [@ocaml.deprecated "Use Names.GlobRef.VarRef"] + | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"] + | IndRef of inductive [@ocaml.deprecated "Use Names.GlobRef.IndRef"] + | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"] [@@ocaml.deprecated "Use Names.GlobRef.t"] val isVarRef : GlobRef.t -> bool @@ -25,8 +24,6 @@ val isConstRef : GlobRef.t -> bool val isIndRef : GlobRef.t -> bool val isConstructRef : GlobRef.t -> bool -val eq_gr : GlobRef.t -> GlobRef.t -> bool -[@@ocaml.deprecated "Use Names.GlobRef.equal"] val canonical_gr : GlobRef.t -> GlobRef.t val destVarRef : GlobRef.t -> variable @@ -48,22 +45,6 @@ val printable_constr_of_global : GlobRef.t -> constr raise [Not_found] if not a global reference *) val global_of_constr : constr -> GlobRef.t -module RefOrdered = Names.GlobRef.Ordered -[@@ocaml.deprecated "Use Names.GlobRef.Ordered"] - -module RefOrdered_env = Names.GlobRef.Ordered_env -[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"] - -module Refset = Names.GlobRef.Set -[@@ocaml.deprecated "Use Names.GlobRef.Set"] -module Refmap = Names.GlobRef.Map -[@@ocaml.deprecated "Use Names.GlobRef.Map"] - -module Refset_env = GlobRef.Set_env -[@@ocaml.deprecated "Use Names.GlobRef.Set_env"] -module Refmap_env = GlobRef.Map_env -[@@ocaml.deprecated "Use Names.GlobRef.Map_env"] - (** {6 Extended global references } *) type syndef_name = KerName.t diff --git a/library/goptions.ml b/library/goptions.ml index 1b907fd966..0973944fb5 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -42,22 +42,21 @@ let error_undeclared_key key = (****************************************************************************) (* 1- Tables *) -class type ['a] table_of_A = -object - method add : 'a -> unit - method remove : 'a -> unit - method mem : 'a -> unit - method print : unit -end +type 'a table_of_A = { + add : Environ.env -> 'a -> unit; + remove : Environ.env -> 'a -> unit; + mem : Environ.env -> 'a -> unit; + print : unit -> unit; +} module MakeTable = functor (A : sig type t - type key - val compare : t -> t -> int - val table : (string * key table_of_A) list ref - val encode : key -> t + type key + module Set : CSig.SetS with type elt = t + val table : (string * key table_of_A) list ref + val encode : Environ.env -> key -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -75,7 +74,7 @@ module MakeTable = if String.List.mem_assoc nick !A.table then 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) + module MySet = A.Set let t = Summary.ref MySet.empty ~name:nick @@ -109,20 +108,20 @@ module MakeTable = (fun a b -> spc () ++ printer a ++ b) table (mt ()) ++ str "." ++ fnl ()))) - class table_of_A () = - object - method add x = add_option (A.encode x) - method remove x = remove_option (A.encode x) - method mem x = - let y = A.encode x in + let table_of_A = { + add = (fun env x -> add_option (A.encode env x)); + remove = (fun env x -> remove_option (A.encode env x)); + mem = (fun env x -> + let y = A.encode env x in let answer = MySet.mem y !t in - Feedback.msg_info (A.member_message y answer) - method print = print_table A.title A.printer !t - end + Feedback.msg_info (A.member_message y answer)); + print = (fun () -> print_table A.title A.printer !t); + } + + let _ = A.table := (nick, table_of_A)::!A.table - let _ = A.table := (nick,new table_of_A ())::!A.table - let active c = MySet.mem c !t - let elements () = MySet.elements !t + let v () = !t + let active x = A.Set.mem x !t end let string_table = ref [] @@ -140,9 +139,9 @@ module StringConvert = functor (A : StringConvertArg) -> struct type t = string type key = string - let compare = String.compare + module Set = CString.Set let table = string_table - let encode x = x + let encode _env x = x let subst _ x = x let printer = str let key = A.key @@ -160,8 +159,8 @@ let get_ref_table k = String.List.assoc (nickname k) !ref_table module type RefConvertArg = sig type t - val compare : t -> t -> int - val encode : qualid -> t + module Set : CSig.SetS with type elt = t + val encode : Environ.env -> qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -173,7 +172,7 @@ module RefConvert = functor (A : RefConvertArg) -> struct type t = A.t type key = qualid - let compare = A.compare + module Set = A.Set let table = ref_table let encode = A.encode let subst = A.subst @@ -399,9 +398,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in diff --git a/library/goptions.mli b/library/goptions.mli index b91553bf3c..29af196654 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -70,13 +70,13 @@ module MakeStringTable : val member_message : string -> bool -> Pp.t end) -> sig + val v : unit -> CString.Set.t val active : string -> bool - val elements : unit -> string list end (** The functor [MakeRefTable] declares a new table of objects of type [A.t] practically denoted by [reference]; the encoding function - [encode : reference -> A.t] is typically a globalization function, + [encode : env -> reference -> A.t] is typically a globalization function, possibly with some restriction checks; the function [member_message] say what to print when invoking the "Test Toto Titi foo." command; at the end [title] is the table name printed @@ -87,19 +87,19 @@ end module MakeRefTable : functor (A : sig - type t - val compare : t -> t -> int - val encode : qualid -> t - val subst : substitution -> t -> t - val printer : t -> Pp.t - val key : option_name - val title : string - val member_message : t -> bool -> Pp.t - end) -> - sig - val active : A.t -> bool - val elements : unit -> A.t list - end + type t + module Set : CSig.SetS with type elt = t + val encode : Environ.env -> qualid -> t + val subst : substitution -> t -> t + val printer : t -> Pp.t + val key : option_name + val title : string + val member_message : t -> bool -> Pp.t + end) -> +sig + val v : unit -> A.Set.t + val active : A.t -> bool +end (** {6 Options. } *) @@ -139,19 +139,17 @@ val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> module OptionMap : CSig.MapS with type key = option_name -val get_string_table : - option_name -> - < add : string -> unit; - remove : string -> unit; - mem : string -> unit; - print : unit > +type 'a table_of_A = { + add : Environ.env -> 'a -> unit; + remove : Environ.env -> 'a -> unit; + mem : Environ.env -> 'a -> unit; + print : unit -> unit; +} +val get_string_table : + option_name -> string table_of_A val get_ref_table : - option_name -> - < add : qualid -> unit; - remove : qualid -> unit; - mem : qualid -> unit; - print : unit > + option_name -> qualid table_of_A (** The first argument is a locality flag. *) val set_int_option_value_gen : ?locality:option_locality -> option_name -> int option -> unit @@ -172,6 +170,14 @@ type option_value = | StringValue of string | StringOptValue of string option +val set_option_value : ?locality:option_locality -> + ('a -> option_value -> option_value) -> option_name -> 'a -> unit +(** [set_option_value ?locality f name v] sets [name] to the result of + applying [f] to [v] and [name]'s current value. Use for behaviour + depending on the type of the option, eg erroring when ['a] doesn't + match it. Changing the type will result in errors later so don't do + that. *) + (** Summary of an option status *) type option_state = { opt_depr : bool; diff --git a/library/keys.ml b/library/keys.ml deleted file mode 100644 index 45b6fae2f0..0000000000 --- a/library/keys.ml +++ /dev/null @@ -1,163 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Keys for unification and indexing *) - -open Names -open Constr -open Libobject -open Globnames - -type key = - | KGlob of GlobRef.t - | KLam - | KLet - | KProd - | KSort - | KCase - | KFix - | KCoFix - | KRel - | KInt - -module KeyOrdered = struct - type t = key - - let hash gr = - match gr with - | KGlob gr -> 9 + GlobRef.Ordered.hash gr - | KLam -> 0 - | KLet -> 1 - | KProd -> 2 - | KSort -> 3 - | KCase -> 4 - | KFix -> 5 - | KCoFix -> 6 - | KRel -> 7 - | KInt -> 8 - - let compare gr1 gr2 = - match gr1, gr2 with - | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2 - | _, KGlob _ -> -1 - | KGlob _, _ -> 1 - | k, k' -> Int.compare (hash k) (hash k') - - let equal k1 k2 = - match k1, k2 with - | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2 - | _, KGlob _ -> false - | KGlob _, _ -> false - | k, k' -> k == k' -end - -module Keymap = HMap.Make(KeyOrdered) -module Keyset = Keymap.Set - -(* Mapping structure for references to be considered equivalent *) - -let keys = Summary.ref Keymap.empty ~name:"Keys_decl" - -let add_kv k v m = - try Keymap.modify k (fun k' vs -> Keyset.add v vs) m - with Not_found -> Keymap.add k (Keyset.singleton v) m - -let add_keys k v = - keys := add_kv k v (add_kv v k !keys) - -let equiv_keys k k' = - k == k' || KeyOrdered.equal k k' || - try Keyset.mem k' (Keymap.find k !keys) - with Not_found -> false - -(** Registration of keys as an object *) - -let load_keys _ (_,(ref,ref')) = - add_keys ref ref' - -let cache_keys o = - load_keys 1 o - -let subst_key subst k = - match k with - | KGlob gr -> KGlob (subst_global_reference subst gr) - | _ -> k - -let subst_keys (subst,(k,k')) = - (subst_key subst k, subst_key subst k') - -let discharge_key = function - | KGlob (VarRef _ as g) when Lib.is_in_section g -> None - | x -> Some x - -let discharge_keys (_,(k,k')) = - match discharge_key k, discharge_key k' with - | Some x, Some y -> Some (x, y) - | _ -> None - -type key_obj = key * key - -let inKeys : key_obj -> obj = - 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')) - -let constr_key kind c = - let open Globnames in - try - let rec aux k = - match kind k with - | Const (c, _) -> KGlob (ConstRef c) - | Ind (i, u) -> KGlob (IndRef i) - | Construct (c,u) -> KGlob (ConstructRef c) - | Var id -> KGlob (VarRef id) - | App (f, _) -> aux f - | Proj (p, _) -> KGlob (ConstRef (Projection.constant p)) - | Cast (p, _, _) -> aux p - | Lambda _ -> KLam - | Prod _ -> KProd - | Case _ -> KCase - | Fix _ -> KFix - | CoFix _ -> KCoFix - | Rel _ -> KRel - | Meta _ -> raise Not_found - | Evar _ -> raise Not_found - | Sort _ -> KSort - | LetIn _ -> KLet - | Int _ -> KInt - in Some (aux c) - with Not_found -> None - -open Pp - -let pr_key pr_global = function - | KGlob gr -> pr_global gr - | KLam -> str"Lambda" - | KLet -> str"Let" - | KProd -> str"Product" - | KSort -> str"Sort" - | KCase -> str"Case" - | 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) - -let pr_mapping pr_global k v = - pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v - -let pr_keys pr_global = - Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt()) diff --git a/library/keys.mli b/library/keys.mli deleted file mode 100644 index 198383650a..0000000000 --- a/library/keys.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type key - -val declare_equiv_keys : key -> key -> unit -(** Declare two keys as being equivalent. *) - -val equiv_keys : key -> key -> bool -(** Check equivalence of keys. *) - -val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option -(** Compute the head key of a term. *) - -val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t -(** Pretty-print the mapping *) diff --git a/library/kindops.ml b/library/kindops.ml deleted file mode 100644 index 247319fa2f..0000000000 --- a/library/kindops.ml +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Decl_kinds - -(** Operations about types defined in [Decl_kinds] *) - -let logical_kind_of_goal_kind = function - | DefinitionBody d -> IsDefinition d - | Proof s -> IsProof s - -let string_of_theorem_kind = function - | Theorem -> "Theorem" - | Lemma -> "Lemma" - | Fact -> "Fact" - | Remark -> "Remark" - | Property -> "Property" - | Proposition -> "Proposition" - | Corollary -> "Corollary" - -let string_of_definition_object_kind = function - | Definition -> "Definition" - | Example -> "Example" - | Coercion -> "Coercion" - | SubClass -> "SubClass" - | CanonicalStructure -> "Canonical Structure" - | Instance -> "Instance" - | Let -> "Let" - | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> - CErrors.anomaly (Pp.str "Internal definition kind.") diff --git a/library/kindops.mli b/library/kindops.mli deleted file mode 100644 index df39019da4..0000000000 --- a/library/kindops.mli +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Decl_kinds - -(** Operations about types defined in [Decl_kinds] *) - -val logical_kind_of_goal_kind : goal_object_kind -> logical_kind -val string_of_theorem_kind : theorem_kind -> string -val string_of_definition_object_kind : definition_object_kind -> string diff --git a/library/lib.ml b/library/lib.ml index d4381a6923..991e23eb3a 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -13,7 +13,6 @@ open CErrors open Util open Names open Libnames -open Globnames open Libobject open Context.Named.Declaration @@ -28,7 +27,7 @@ let make_oname Nametab.{ obj_dir; obj_mp } id = (* let make_oname (dirpath,(mp,dir)) id = *) type node = - | Leaf of obj + | Leaf of Libobject.t | CompilingLibrary of Nametab.object_prefix | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen | OpenedSection of Nametab.object_prefix * Summary.frozen @@ -37,7 +36,8 @@ type library_entry = object_name * node type library_segment = library_entry list -type lib_objects = (Names.Id.t * obj) list +type lib_atomic_objects = (Id.t * Libobject.obj) list +type lib_objects = (Names.Id.t * Libobject.t) list let module_kind is_type = if is_type then "module type" else "module" @@ -45,10 +45,10 @@ let module_kind is_type = let iter_objects f i prefix = List.iter (fun (id,obj) -> f i (make_oname prefix id, obj)) -let load_objects i pr = iter_objects load_object i pr -let open_objects i pr = iter_objects open_object i pr +let load_atomic_objects i pr = iter_objects load_object i pr +let open_atomic_objects i pr = iter_objects open_object i pr -let subst_objects subst seg = +let subst_atomic_objects subst seg = let subst_one = fun (id,obj as node) -> let obj' = subst_object (subst,obj) in if obj' == obj then node else @@ -67,15 +67,25 @@ let classify_segment seg = let rec clean ((substl,keepl,anticipl) as acc) = function | (_,CompilingLibrary _) :: _ | [] -> acc | ((sp,kn),Leaf o) :: stk -> - let id = Names.Label.to_id (Names.KerName.label kn) in - (match classify_object o with - | Dispose -> clean acc stk - | Keep o' -> - clean (substl, (id,o')::keepl, anticipl) stk - | Substitute o' -> - clean ((id,o')::substl, keepl, anticipl) stk - | Anticipate o' -> - clean (substl, keepl, o'::anticipl) stk) + let id = Names.Label.to_id (Names.KerName.label kn) in + begin match o with + | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ -> + clean ((id,o)::substl, keepl, anticipl) stk + | KeepObject _ -> + clean (substl, (id,o)::keepl, anticipl) stk + | ExportObject _ -> + clean ((id,o)::substl, keepl, anticipl) stk + | AtomicObject obj -> + begin match classify_object obj with + | Dispose -> clean acc stk + | Keep o' -> + clean (substl, (id,AtomicObject o')::keepl, anticipl) stk + | Substitute o' -> + clean ((id,AtomicObject o')::substl, keepl, anticipl) stk + | Anticipate o' -> + clean (substl, keepl, AtomicObject o'::anticipl) stk + end + end | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections") | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" @@ -211,9 +221,6 @@ let split_lib_at_opening sp = let add_entry sp node = lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk } -let pull_to_head oname = - lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk } - let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) @@ -226,19 +233,19 @@ let add_leaf id obj = user_err Pp.(str "No session module started (use -top dir)"); let oname = make_foname id in cache_object (oname,obj); - add_entry oname (Leaf obj); + add_entry oname (Leaf (AtomicObject obj)); oname let add_discharged_leaf id obj = let oname = make_foname id in let newobj = rebuild_object obj in cache_object (oname,newobj); - add_entry oname (Leaf newobj) + add_entry oname (Leaf (AtomicObject newobj)) let add_leaves id objs = let oname = make_foname id in let add_obj obj = - add_entry oname (Leaf obj); + add_entry oname (Leaf (AtomicObject obj)); load_object 1 (oname,obj) in List.iter add_obj objs; @@ -249,9 +256,9 @@ let add_anonymous_leaf ?(cache_first = true) obj = let oname = make_foname id in if cache_first then begin cache_object (oname,obj); - add_entry oname (Leaf obj) + add_entry oname (Leaf (AtomicObject obj)) end else begin - add_entry oname (Leaf obj); + add_entry oname (Leaf (AtomicObject obj)); cache_object (oname,obj) end @@ -278,7 +285,7 @@ let start_mod is_type export id mp fs = 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 + else Nametab.exists_dir dir in if exists then user_err ~hdr:"open_module" (Id.print id ++ str " already exists"); @@ -403,141 +410,36 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Constr.named_declaration * Decl_kinds.binding_kind - -type variable_context = variable_info list -type abstr_info = { - abstr_ctx : variable_context; +type abstr_info = Section.abstr_info = private { + abstr_ctx : Constr.named_context; abstr_subst : Univ.Instance.t; abstr_uctx : Univ.AUContext.t; } -type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t - -type secentry = - | Variable of (Names.Id.t * Decl_kinds.binding_kind * - Decl_kinds.polymorphic * Univ.ContextSet.t) - | Context of Univ.ContextSet.t - -let sectab = - Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list) - ~name:"section-context" - -let add_section () = - sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty), - (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab - -let check_same_poly p vars = - let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in - if List.exists pred vars then - user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") - -let add_section_variable id impl poly ctx = - match !sectab with - | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | (vars,repl,abs)::sl -> - List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; - sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl - -let add_section_context ctx = - match !sectab with - | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | (vars,repl,abs)::sl -> - check_same_poly true vars; - sectab := (Context ctx :: vars,repl,abs)::sl - -exception PolyFound of bool (* make this a let exception once possible *) -let is_polymorphic_univ u = - try - let open Univ in - List.iter (fun (vars,_,_) -> - List.iter (function - | Variable (_,_,poly,(univs,_)) -> - if LSet.mem u univs then raise (PolyFound poly) - | Context (univs,_) -> - if LSet.mem u univs then raise (PolyFound true) - ) vars - ) !sectab; - false - with PolyFound b -> b - -let extract_hyps (secs,ohyps) = - let rec aux = function - | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> - let l, r = aux (idl,hyps) in - (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r - | (Variable (_,_,poly,ctx)::idl,hyps) -> - let l, r = aux (idl,hyps) in - l, if poly then Univ.ContextSet.union r ctx else r - | (Context ctx :: idl, hyps) -> - let l, r = aux (idl, hyps) in - l, Univ.ContextSet.union r ctx - | [], _ -> [],Univ.ContextSet.empty - in aux (secs,ohyps) let instance_from_variable_context = - List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list - -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 - | [] -> () - | (vars,exps,abs)::sl -> - let () = check_same_poly poly vars in - let sechyps,ctx = extract_hyps (vars,hyps) in - let ctx = Univ.ContextSet.to_context ctx in - let inst = Univ.UContext.instance 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; - abstr_subst = subst; - abstr_uctx = ctx; - } in - sectab := (vars,f (inst,args) exps, g info abs) :: sl - -let add_section_kn poly kn = - let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f poly - -let add_section_constant poly kn = - let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f poly - -let replacement_context () = pi2 (List.hd !sectab) + List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list + +let extract_worklist info = + let args = instance_from_variable_context info.abstr_ctx in + info.abstr_subst, args + +let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () + +let is_polymorphic_univ u = + Section.is_polymorphic_univ u (sections ()) + +let replacement_context () = + Section.replacement_context (Global.env ()) (sections ()) let section_segment_of_constant con = - Names.Cmap.find con (fst (pi3 (List.hd !sectab))) + Section.segment_of_constant (Global.env ()) con (sections ()) let section_segment_of_mutual_inductive kn = - Names.Mindmap.find kn (snd (pi3 (List.hd !sectab))) + Section.segment_of_inductive (Global.env ()) kn (sections ()) -let empty_segment = { - abstr_ctx = []; - abstr_subst = Univ.Instance.empty; - abstr_uctx = Univ.AUContext.empty; -} +let empty_segment = Section.empty_segment -let section_segment_of_reference = function +let section_segment_of_reference = let open GlobRef in function | ConstRef c -> section_segment_of_constant c | IndRef (kn,_) | ConstructRef ((kn,_),_) -> section_segment_of_mutual_inductive kn @@ -546,38 +448,34 @@ let section_segment_of_reference = function let variable_section_segment_of_reference gr = (section_segment_of_reference gr).abstr_ctx -let section_instance = function +let is_in_section ref = + Section.is_in_section (Global.env ()) ref (sections ()) + +let section_instance = let open GlobRef in function | VarRef id -> - let eq = function - | Variable (id',_,_,_) -> Names.Id.equal id id' - | Context _ -> false - in - if List.exists eq (pi1 (List.hd !sectab)) - then Univ.Instance.empty, [||] - else raise Not_found + if is_in_section (VarRef id) then (Univ.Instance.empty, [||]) + else raise Not_found | ConstRef con -> - Names.Cmap.find con (fst (pi2 (List.hd !sectab))) + let data = section_segment_of_constant con in + extract_worklist data | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - Names.Mindmap.find kn (snd (pi2 (List.hd !sectab))) - -let is_in_section ref = - try ignore (section_instance ref); true with Not_found -> false + let data = section_segment_of_mutual_inductive kn in + extract_worklist data (*************) (* Sections. *) let open_section id = + let () = Global.open_section () in let opp = !lib_state.path_prefix 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 + if Nametab.exists_dir obj_dir then user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); 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)); - lib_state := { !lib_state with path_prefix = prefix }; - add_section () - + lib_state := { !lib_state with path_prefix = prefix } (* Restore lib_stk and summaries as before the section opening, and add a ClosedSection object. *) @@ -585,7 +483,12 @@ let open_section id = let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> - Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) + begin match lobj with + | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _ + | ExportObject _ -> None + | AtomicObject obj -> + Option.map (fun o -> (basename sp,o)) (discharge_object (oname,obj)) + end | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -601,7 +504,7 @@ let close_section () = lib_state := { !lib_state with lib_stk = before }; pop_path_prefix (); let newdecls = List.map discharge_item secdecls in - Summary.unfreeze_summaries fs; + let () = Global.close_section fs in List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls (* State and initialization. *) @@ -630,7 +533,7 @@ let init () = (* Misc *) -let mp_of_global = function +let mp_of_global = let open GlobRef in function | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp | ConstRef cst -> Names.Constant.modpath cst | IndRef ind -> Names.ind_modpath ind @@ -649,12 +552,12 @@ let rec split_modpath = function (dp, Names.Label.to_id l :: ids) let library_part = function - |VarRef id -> library_dp () - |ref -> dp_of_mp (mp_of_global ref) + | GlobRef.VarRef id -> library_dp () + | ref -> dp_of_mp (mp_of_global ref) let discharge_proj_repr = Projection.Repr.map_npars (fun mind npars -> - if not (is_in_section (IndRef (mind,0))) then mind, npars + if not (is_in_section (GlobRef.IndRef (mind,0))) then mind, npars else let modlist = replacement_context () in let _, newpars = Mindmap.find mind (snd modlist) in mind, npars + Array.length newpars) diff --git a/library/lib.mli b/library/lib.mli index 30569197bc..d3315b0f2e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -20,22 +20,24 @@ 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 +val make_foname : Names.Id.t -> Libnames.full_path * Names.KerName.t type node = - | Leaf of Libobject.obj + | Leaf of Libobject.t | 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 = (Libobject.object_name * node) list -type lib_objects = (Id.t * Libobject.obj) list +type lib_atomic_objects = (Id.t * Libobject.obj) list +type lib_objects = (Id.t * Libobject.t) list (** {6 Object iteration functions. } *) -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 open_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit +val load_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit +val subst_atomic_objects : Mod_subst.substitution -> lib_atomic_objects -> lib_atomic_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, @@ -44,12 +46,17 @@ val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects [Substitute], [Keep], [Anticipate] respectively. The order of each returned list is the same as in the input list. *) val classify_segment : - library_segment -> lib_objects * lib_objects * Libobject.obj list + library_segment -> lib_objects * lib_objects * Libobject.t list (** [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : Nametab.object_prefix -> lib_objects -> library_segment +(** {6 ... } *) +(** Low-level adding operations *) + +val add_entry : Libobject.object_name -> node -> unit +val add_anonymous_entry : node -> unit (** {6 ... } *) (** Adding operations (which call the [cache] method, and getting the @@ -57,7 +64,6 @@ val segment_of_objects : val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> 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 *) @@ -157,10 +163,8 @@ val drop_objects : frozen -> frozen val init : unit -> unit (** {6 Section management for discharge } *) -type variable_info = Constr.named_declaration * Decl_kinds.binding_kind -type variable_context = variable_info list -type abstr_info = private { - abstr_ctx : variable_context; +type abstr_info = Section.abstr_info = private { + abstr_ctx : Constr.named_context; (** Section variables of this prefix *) abstr_subst : Univ.Instance.t; (** Actual names of the abstracted variables *) @@ -168,24 +172,15 @@ type abstr_info = private { (** Universe quantification, same length as the substitution *) } -val instance_from_variable_context : variable_context -> Id.t array -val named_of_variable_context : variable_context -> Constr.named_context - val section_segment_of_constant : Constant.t -> abstr_info val section_segment_of_mutual_inductive: MutInd.t -> abstr_info val section_segment_of_reference : GlobRef.t -> abstr_info -val variable_section_segment_of_reference : GlobRef.t -> variable_context +val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit -val add_section_context : Univ.ContextSet.t -> unit -val add_section_constant : Decl_kinds.polymorphic -> - Constant.t -> Constr.named_context -> unit -val add_section_kn : Decl_kinds.polymorphic -> - MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list val is_polymorphic_univ : Univ.Level.t -> bool diff --git a/library/libnames.ml b/library/libnames.ml index 87c4de42e8..485f8837e8 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -128,11 +128,6 @@ let path_of_string s = let pr_path sp = str (string_of_path sp) -let restrict_path n sp = - let dir, s = repr_path sp in - let dir' = List.firstn n (DirPath.repr dir) in - make_path (DirPath.make dir') s - (*s qualified names *) type qualid_r = full_path type qualid = qualid_r CAst.t @@ -162,6 +157,9 @@ let qualid_basename qid = let qualid_path qid = qid.CAst.v.dirpath +let idset_mem_qualid qid s = + qualid_is_ident qid && Id.Set.mem (qualid_basename qid) s + (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/libnames.mli b/library/libnames.mli index bbb4d2a058..ffd7032fff 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -57,8 +57,6 @@ val pr_path : full_path -> Pp.t module Spmap : CSig.MapS with type key = full_path -val restrict_path : int -> full_path -> full_path - (** {6 ... } *) (** A [qualid] is a partially qualified ident; it includes fully qualified names (= absolute names) and all intermediate partial @@ -88,6 +86,9 @@ val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t val qualid_basename : qualid -> Id.t +val idset_mem_qualid : qualid -> Id.Set.t -> bool +(** false when the qualid is not an ident *) + (** {6 ... } *) (** some preset paths *) diff --git a/library/libobject.ml b/library/libobject.ml index 3d17b4a605..932f065f73 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -9,6 +9,7 @@ (************************************************************************) open Pp +open Names module Dyn = Dyn.Make () @@ -34,7 +35,7 @@ let default_object s = { open_function = (fun _ _ -> ()); subst_function = (fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")); - classify_function = (fun obj -> Keep obj); + classify_function = (fun atomic_obj -> Keep atomic_obj); discharge_function = (fun _ -> None); rebuild_function = (fun x -> x)} @@ -52,8 +53,35 @@ let default_object s = { let ident_subst_function (_,a) = a + type obj = Dyn.t (* persistent dynamic objects *) +(** {6 Substitutive objects} + + - The list of bound identifiers is nonempty only if the objects + are owned by a functor + + - Then comes either the object segment itself (for interactive + modules), or a compact way to store derived objects (path to + a earlier module + substitution). +*) + +type algebraic_objects = + | Objs of objects + | Ref of Names.ModPath.t * Mod_subst.substitution + +and t = + | ModuleObject of substitutive_objects + | ModuleTypeObject of substitutive_objects + | IncludeObject of algebraic_objects + | KeepObject of objects + | ExportObject of { mpl : ModPath.t list } + | AtomicObject of obj + +and objects = (Names.Id.t * t) list + +and substitutive_objects = MBId.t list * algebraic_objects + type dynamic_object_declaration = { dyn_cache_function : object_name * obj -> unit; dyn_load_function : int -> object_name * obj -> unit; @@ -77,9 +105,9 @@ let declare_object_full odecl = and substituter (sub,lobj) = infun (odecl.subst_function (sub,outfun lobj)) and classifier lobj = match odecl.classify_function (outfun lobj) with | Dispose -> Dispose - | Substitute obj -> Substitute (infun obj) - | Keep obj -> Keep (infun obj) - | Anticipate (obj) -> Anticipate (infun obj) + | Substitute atomic_obj -> Substitute (infun atomic_obj) + | Keep atomic_obj -> Keep (infun atomic_obj) + | Anticipate (atomic_obj) -> Anticipate (infun atomic_obj) and discharge (oname,lobj) = Option.map infun (odecl.discharge_function (oname,outfun lobj)) and rebuild lobj = infun (odecl.rebuild_function (outfun lobj)) diff --git a/library/libobject.mli b/library/libobject.mli index 00515bd273..146ccc293f 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -103,6 +103,22 @@ val ident_subst_function : substitution * 'a -> 'a type obj +type algebraic_objects = + | Objs of objects + | Ref of Names.ModPath.t * Mod_subst.substitution + +and t = + | ModuleObject of substitutive_objects + | ModuleTypeObject of substitutive_objects + | IncludeObject of algebraic_objects + | KeepObject of objects + | ExportObject of { mpl : Names.ModPath.t list } + | AtomicObject of obj + +and objects = (Names.Id.t * t) list + +and substitutive_objects = Names.MBId.t list * algebraic_objects + val declare_object_full : 'a object_declaration -> ('a -> obj) * (obj -> 'a) diff --git a/library/library.ml b/library/library.ml deleted file mode 100644 index 37dadadb76..0000000000 --- a/library/library.ml +++ /dev/null @@ -1,750 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open CErrors -open Util - -open Names -open Libnames -open Lib -open Libobject - -(************************************************************************) -(*s Low-level interning/externing of libraries to files *) - -let raw_extern_library f = - System.raw_extern_state Coq_config.vo_magic_number f - -let raw_intern_library f = - System.with_magic_number_check - (System.raw_intern_state Coq_config.vo_magic_number) f - -(************************************************************************) -(** Serialized objects loaded on-the-fly *) - -exception Faulty of string - -module Delayed : -sig - -type 'a delayed -val in_delayed : string -> in_channel -> 'a delayed * Digest.t -val fetch_delayed : 'a delayed -> 'a - -end = -struct - -type 'a delayed = { - del_file : string; - del_off : int; - del_digest : Digest.t; -} - -let in_delayed f ch = - let pos = pos_in ch in - let _, digest = System.skip_in_segment f ch in - ({ del_file = f; del_digest = digest; del_off = pos; }, digest) - -(** Fetching a table of opaque terms at position [pos] in file [f], - expecting to find first a copy of [digest]. *) - -let fetch_delayed del = - let { del_digest = digest; del_file = f; del_off = pos; } = del in - try - let ch = raw_intern_library f in - let () = seek_in ch pos in - let obj, _, digest' = System.marshal_in_segment f ch in - let () = close_in ch in - if not (String.equal digest digest') then raise (Faulty f); - obj - with e when CErrors.noncritical e -> raise (Faulty f) - -end - -open Delayed - - -(************************************************************************) -(*s Modules on disk contain the following informations (after the magic - number, and before the digest). *) - -type compilation_unit_name = DirPath.t - -type library_disk = { - md_compiled : Safe_typing.compiled_library; - md_objects : Declaremods.library_objects; -} - -type summary_disk = { - md_name : compilation_unit_name; - md_imports : compilation_unit_name array; - md_deps : (compilation_unit_name * Safe_typing.vodigest) array; -} - -(*s Modules loaded in memory contain the following informations. They are - kept in the global table [libraries_table]. *) - -type library_t = { - library_name : compilation_unit_name; - library_data : library_disk delayed; - library_deps : (compilation_unit_name * Safe_typing.vodigest) array; - library_imports : compilation_unit_name array; - library_digests : Safe_typing.vodigest; - library_extra_univs : Univ.ContextSet.t; -} - -type library_summary = { - libsum_name : compilation_unit_name; - libsum_digests : Safe_typing.vodigest; - libsum_imports : compilation_unit_name array; -} - -module LibraryOrdered = DirPath -module LibraryMap = Map.Make(LibraryOrdered) -module LibraryFilenameMap = Map.Make(LibraryOrdered) - -(* This is a map from names to loaded libraries *) -let libraries_table : library_summary LibraryMap.t ref = - Summary.ref LibraryMap.empty ~name:"LIBRARY" - -(* This is the map of loaded libraries filename *) -(* (not synchronized so as not to be caught in the states on disk) *) -let libraries_filename_table = ref LibraryFilenameMap.empty - -(* These are the _ordered_ sets of loaded, imported and exported libraries *) -let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" -let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" -let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" - -(* various requests to the tables *) - -let find_library dir = - LibraryMap.find dir !libraries_table - -let try_find_library dir = - try find_library dir - with Not_found -> - user_err ~hdr:"Library.find_library" - (str "Unknown library " ++ DirPath.print dir) - -let register_library_filename dir f = - (* Not synchronized: overwrite the previous binding if one existed *) - (* from a previous play of the session *) - libraries_filename_table := - LibraryFilenameMap.add dir f !libraries_filename_table - -let library_full_filename dir = - try LibraryFilenameMap.find dir !libraries_filename_table - with Not_found -> "<unavailable filename>" - -let overwrite_library_filenames f = - let f = - if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in - LibraryMap.iter (fun dir _ -> register_library_filename dir f) - !libraries_table - -let library_is_loaded dir = - try let _ = find_library dir in true - with Not_found -> false - -let library_is_opened dir = - List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list - -let loaded_libraries () = !libraries_loaded_list - -let opened_libraries () = !libraries_imports_list - - (* If a library is loaded several time, then the first occurrence must - be performed first, thus the libraries_loaded_list ... *) - -let register_loaded_library m = - let libname = m.libsum_name in - let link () = - let dirname = Filename.dirname (library_full_filename libname) in - let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in - let f = prefix ^ "cmo" in - let f = Dynlink.adapt_filename f in - if Coq_config.native_compiler then - Nativelib.link_library ~prefix ~dirname ~basename:f - in - let rec aux = function - | [] -> link (); [libname] - | m'::_ as l when DirPath.equal m' libname -> l - | m'::l' -> m' :: aux l' in - libraries_loaded_list := aux !libraries_loaded_list; - libraries_table := LibraryMap.add libname m !libraries_table - - (* ... while if a library is imported/exported several time, then - only the last occurrence is really needed - though the imported - list may differ from the exported list (consider the sequence - Export A; Export B; Import A which results in A;B for exports but - in B;A for imports) *) - -let rec remember_last_of_each l m = - match l with - | [] -> [m] - | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m - | m'::l' -> m' :: remember_last_of_each l' m - -let register_open_library export m = - libraries_imports_list := remember_last_of_each !libraries_imports_list m; - if export then - libraries_exports_list := remember_last_of_each !libraries_exports_list m - -(************************************************************************) -(*s Opening libraries *) - -(* [open_library export explicit m] opens library [m] if not already - opened _or_ if explicitly asked to be (re)opened *) - -let open_library export explicit_libs m = - if - (* Only libraries indirectly to open are not reopen *) - (* Libraries explicitly mentionned by the user are always reopen *) - List.exists (fun m' -> DirPath.equal m m') explicit_libs - || not (library_is_opened m) - then begin - register_open_library export m; - Declaremods.really_import_module (MPfile m) - end - else - if export then - libraries_exports_list := remember_last_of_each !libraries_exports_list m - -(* open_libraries recursively open a list of libraries but opens only once - a library that is re-exported many times *) - -let open_libraries export modl = - let to_open_list = - List.fold_left - (fun l m -> - let subimport = - Array.fold_left - (fun l m -> remember_last_of_each l m) - l m.libsum_imports - in remember_last_of_each subimport m.libsum_name) - [] modl in - let explicit = List.map (fun m -> m.libsum_name) modl in - List.iter (open_library export explicit) to_open_list - - -(**********************************************************************) -(* import and export of libraries - synchronous operations *) -(* at the end similar to import and export of modules except that it *) -(* is optimized: when importing several libraries at the same time *) -(* which themselves indirectly imports the very same modules, these *) -(* ones are imported only ones *) - -let open_import_library i (_,(modl,export)) = - if Int.equal i 1 then - (* even if the library is already imported, we re-import it *) - (* if not (library_is_opened dir) then *) - open_libraries export (List.map try_find_library modl) - -let cache_import_library obj = - open_import_library 1 obj - -let subst_import_library (_,o) = o - -let classify_import_library (_,export as obj) = - if export then Substitute obj else Dispose - -let in_import_library : DirPath.t list * bool -> obj = - declare_object {(default_object "IMPORT LIBRARY") with - cache_function = cache_import_library; - open_function = open_import_library; - subst_function = subst_import_library; - classify_function = classify_import_library } - - -(************************************************************************) -(*s Locate absolute or partially qualified library names in the path *) - -exception LibUnmappedDir -exception LibNotFound -type library_location = LibLoaded | LibInPath - -let warn_several_object_files = - CWarnings.create ~name:"several-object-files" ~category:"require" - (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++ - strbrk " instead of " ++ str vo ++ - strbrk " because it is more recent") - -let locate_absolute_library dir = - (* Search in loadpath *) - let pref, base = split_dirpath dir in - let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let loadpath = List.map fst loadpath in - let find ext = - try - let name = Id.to_string base ^ ext in - let _, file = System.where_in_path ~warn:false loadpath name in - Some file - with Not_found -> None in - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some file, None | None, Some file -> file - | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - vi - | Some vo, Some _ -> vo - -let locate_qualified_library ?root ?(warn = true) qid = - (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = Loadpath.expand_path ?root dir in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let find ext = - try - let name = Id.to_string base ^ ext in - let lpath, file = - System.where_in_path ~warn (List.map fst loadpath) name in - Some (lpath, file) - with Not_found -> None in - let lpath, file = - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some res, None | None, Some res -> res - | Some (_, vo), Some (_, vi as resvi) - when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - resvi - | Some resvo, Some _ -> resvo - in - let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in - (* Look if loaded *) - if library_is_loaded dir then (LibLoaded, dir,library_full_filename dir) - (* Otherwise, look for it in the file system *) - else (LibInPath, dir, file) - -let error_unmapped_dir qid = - let prefix, _ = repr_qualid qid in - user_err ~hdr:"load_absolute_library_from" - (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ()) - -let error_lib_not_found qid = - user_err ~hdr:"load_absolute_library_from" - (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") - -let try_locate_absolute_library dir = - try - locate_absolute_library dir - with - | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) - | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) - -(************************************************************************) -(** {6 Tables of opaque proof terms} *) - -(** We now store opaque proof terms apart from the rest of the environment. - See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way, - we can quickly load a first half of a .vo file without these opaque - terms, and access them only when a specific command (e.g. Print or - Print Assumptions) needs it. *) - -(** Delayed / available tables of opaque terms *) - -type 'a table_status = - | ToFetch of 'a Future.computation array delayed - | Fetched of 'a Future.computation array - -let opaque_tables = - ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t) -let univ_tables = - ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t) - -let add_opaque_table dp st = - opaque_tables := LibraryMap.add dp st !opaque_tables -let add_univ_table dp st = - univ_tables := LibraryMap.add dp st !univ_tables - -let access_table what tables dp i = - let t = match LibraryMap.find dp !tables with - | Fetched t -> t - | ToFetch f -> - let dir_path = Names.DirPath.to_string dp in - Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); - let t = - try fetch_delayed f - with Faulty f -> - user_err ~hdr:"Library.access_table" - (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++ - str ") is inaccessible or corrupted,\ncannot load some " ++ - str what ++ str " in it.\n") - in - tables := LibraryMap.add dp (Fetched t) !tables; - t - in - assert (i < Array.length t); t.(i) - -let access_opaque_table dp i = - let what = "opaque proofs" in - access_table what opaque_tables dp i - -let access_univ_table dp i = - try - let what = "universe contexts of opaque proofs" in - Some (access_table what univ_tables dp i) - with Not_found -> None - -let () = - Opaqueproof.set_indirect_opaque_accessor access_opaque_table; - Opaqueproof.set_indirect_univ_accessor access_univ_table - -(************************************************************************) -(* Internalise libraries *) - -type seg_sum = summary_disk -type seg_lib = library_disk -type seg_univ = (* true = vivo, false = vi *) - Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool -type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr Future.computation array - -let mk_library sd md digests univs = - { - library_name = sd.md_name; - library_data = md; - library_deps = sd.md_deps; - library_imports = sd.md_imports; - library_digests = digests; - library_extra_univs = univs; - } - -let mk_summary m = { - libsum_name = m.library_name; - libsum_imports = m.library_imports; - libsum_digests = m.library_digests; -} - -let intern_from_file f = - let ch = raw_intern_library f in - let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in - let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in - let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in - let _ = System.skip_in_segment f ch in - let _ = System.skip_in_segment f ch in - let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in - close_in ch; - register_library_filename lsd.md_name f; - add_opaque_table lsd.md_name (ToFetch del_opaque); - let open Safe_typing in - match univs with - | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty - | Some (utab,uall,true) -> - add_univ_table lsd.md_name (Fetched utab); - mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall - | Some (utab,_,false) -> - add_univ_table lsd.md_name (Fetched utab); - mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty - -module DPMap = Map.Make(DirPath) - -let rec intern_library (needed, contents) (dir, f) from = - (* Look if in the current logical environment *) - try (find_library dir).libsum_digests, (needed, contents) - with Not_found -> - (* Look if already listed and consequently its dependencies too *) - try (DPMap.find dir contents).library_digests, (needed, contents) - with Not_found -> - Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); - (* [dir] is an absolute name which matches [f] which must be in loadpath *) - let f = match f with Some f -> f | None -> try_locate_absolute_library dir in - let m = intern_from_file f in - if not (DirPath.equal dir m.library_name) then - user_err ~hdr:"load_physical_library" - (str "The file " ++ str f ++ str " contains library" ++ spc () ++ - DirPath.print m.library_name ++ spc () ++ str "and not library" ++ - spc() ++ DirPath.print dir); - Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); - m.library_digests, intern_library_deps (needed, contents) dir m f - -and intern_library_deps libs dir m from = - let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in - (dir :: needed, DPMap.add dir m contents ) - -and intern_mandatory_library caller from libs (dir,d) = - let digest, libs = intern_library libs (dir, None) (Some from) in - if not (Safe_typing.digest_match ~actual:digest ~required:d) then - user_err (str "Compiled library " ++ DirPath.print caller ++ - str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ - over library " ++ DirPath.print dir); - libs - -let rec_intern_library libs (dir, f) = - let _, libs = intern_library libs (dir, Some f) None in - libs - -let native_name_from_filename f = - let ch = raw_intern_library f in - let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in - Nativecode.mod_uid_of_dirpath lmd.md_name - -(**********************************************************************) -(*s [require_library] loads and possibly opens a library. This is a - synchronized operation. It is performed as follows: - - preparation phase: (functions require_library* ) the library and its - dependencies are read from to disk (using intern_* ) - [they are read from disk to ensure that at section/module - discharging time, the physical library referred to outside the - section/module is the one that was used at type-checking time in - the section/module] - - execution phase: (through add_leaf and cache_require) - the library is loaded in the environment and Nametab, the objects are - registered etc, using functions from Declaremods (via load_library, - which recursively loads its dependencies) -*) - -let register_library m = - let l = fetch_delayed m.library_data in - Declaremods.register_library - m.library_name - l.md_compiled - l.md_objects - m.library_digests - m.library_extra_univs; - register_loaded_library (mk_summary m) - -(* Follow the semantics of Anticipate object: - - called at module or module type closing when a Require occurs in - the module or module type - - not called from a library (i.e. a module identified with a file) *) -let load_require _ (_,(needed,modl,_)) = - List.iter register_library needed - -let open_require i (_,(_,modl,export)) = - Option.iter (fun exp -> open_libraries exp (List.map find_library modl)) - export - - (* [needed] is the ordered list of libraries not already loaded *) -let cache_require o = - load_require 1 o; - open_require 1 o - -let discharge_require (_,o) = Some o - -(* open_function is never called from here because an Anticipate object *) - -type require_obj = library_t list * DirPath.t list * bool option - -let in_require : require_obj -> obj = - declare_object {(default_object "REQUIRE") with - cache_function = cache_require; - load_function = load_require; - open_function = (fun _ _ -> assert false); - discharge_function = discharge_require; - classify_function = (fun o -> Anticipate o) } - -(* Require libraries, import them if [export <> None], mark them for export - if [export = Some true] *) - -let warn_require_in_module = - CWarnings.create ~name:"require-in-module" ~category:"deprecated" - (fun () -> strbrk "Require inside a module is" ++ - strbrk " deprecated and strongly discouraged. " ++ - strbrk "You can Require a module at toplevel " ++ - strbrk "and optionally Import it inside another one.") - -let require_library_from_dirpath modrefl export = - let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in - let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in - let modrefl = List.map fst modrefl in - if Lib.is_module_or_modtype () then - begin - warn_require_in_module (); - add_anonymous_leaf (in_require (needed,modrefl,None)); - Option.iter (fun exp -> - add_anonymous_leaf (in_import_library (modrefl,exp))) - export - end - else - add_anonymous_leaf (in_require (needed,modrefl,export)); - () - -(* the function called by Vernacentries.vernac_import *) - -let safe_locate_module qid = - try Nametab.locate_module qid - with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"import_library" - (pr_qualid qid ++ str " is not a module") - -let import_module export modl = - (* Optimization: libraries in a raw in the list are imported - "globally". If there is non-library in the list; it breaks the - optimization For instance: "Import Arith MyModule Zarith" will - not be optimized (possibly resulting in redefinitions, but - "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule" - will have the submodules imported by both Arith and ZArith - imported only once *) - let flush = function - | [] -> () - | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in - let rec aux acc = function - | qid :: l -> - let m,acc = - try Nametab.locate_module qid, acc - with Not_found-> flush acc; safe_locate_module qid, [] in - (match m with - | MPfile dir -> aux (dir::acc) l - | mp -> - flush acc; - try Declaremods.import_module export mp; aux [] l - with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"import_library" - (pr_qualid qid ++ str " is not a module")) - | [] -> flush acc - in aux [] modl - -(************************************************************************) -(*s Initializing the compilation of a library. *) - -let load_library_todo f = - let longf = Loadpath.locate_file (f^".v") in - let f = longf^"io" in - let ch = raw_intern_library f in - let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in - let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in - let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in - let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in - let tasks, _, _ = System.marshal_in_segment f ch in - let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in - close_in ch; - if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); - if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); - if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); - if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 - -(************************************************************************) -(*s [save_library dir] ends library [dir] and save it to the disk. *) - -let current_deps () = - let map name = - let m = try_find_library name in - (name, m.libsum_digests) - in - List.map map !libraries_loaded_list - -let current_reexports () = !libraries_exports_list - -let error_recursively_dependent_library dir = - user_err - (strbrk "Unable to use logical name " ++ DirPath.print dir ++ - strbrk " to save current library because" ++ - strbrk " it already depends on a library of this name.") - -(* We now use two different digests in a .vo file. The first one - only covers half of the file, without the opaque table. It is - used for identifying this version of this library : this digest - is the one leading to "inconsistent assumptions" messages. - The other digest comes at the very end, and covers everything - before it. This one is used for integrity check of the whole - file when loading the opaque table. *) - -(* Security weakness: file might have been changed on disk between - writing the content and computing the checksum... *) - -let save_library_to ?todo ~output_native_objects dir f otab = - let except = match todo with - | None -> - (* XXX *) - (* assert(!Flags.compilation_mode = Flags.BuildVo); *) - assert(Filename.check_suffix f ".vo"); - Future.UUIDSet.empty - | Some (l,_) -> - 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 ~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 - | None -> None, None, None - | Some (tasks, rcbackup) -> - let tasks = - List.map Stateid.(fun (r,b) -> - try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b - with Not_found -> assert b; { r with uuid = -1 }, b) - tasks in - Some (tasks,rcbackup), - Some (univ_table,Univ.ContextSet.empty,false), - Some disch_table in - let except = - Future.UUIDSet.fold (fun uuid acc -> - try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc - with Not_found -> acc) - except Int.Set.empty in - let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in - Array.iteri (fun i x -> - if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library" - Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) - opaque_table; - let sd = { - md_name = dir; - md_deps = Array.of_list (current_deps ()); - md_imports = Array.of_list (current_reexports ()); - } in - let md = { - md_compiled = cenv; - md_objects = seg; - } in - if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then - error_recursively_dependent_library dir; - (* Open the vo file and write the magic number *) - let f' = f in - let ch = raw_extern_library f' in - try - (* Writing vo payload *) - System.marshal_out_segment f' ch (sd : seg_sum); - System.marshal_out_segment f' ch (md : seg_lib); - System.marshal_out_segment f' ch (utab : seg_univ option); - System.marshal_out_segment f' ch (dtab : seg_discharge option); - System.marshal_out_segment f' ch (tasks : 'tasks option); - System.marshal_out_segment f' ch (opaque_table : seg_proofs); - close_out ch; - (* Writing native code files *) - 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.") - with reraise -> - let reraise = CErrors.push reraise in - let () = Feedback.msg_warning (str "Removed file " ++ str f') in - let () = close_out ch in - let () = Sys.remove f' in - iraise reraise - -let save_library_raw f sum lib univs proofs = - let f' = f^"o" in - let ch = raw_extern_library f' in - System.marshal_out_segment f' ch (sum : seg_sum); - System.marshal_out_segment f' ch (lib : seg_lib); - System.marshal_out_segment f' ch (Some univs : seg_univ option); - System.marshal_out_segment f' ch (None : seg_discharge option); - System.marshal_out_segment f' ch (None : 'tasks option); - System.marshal_out_segment f' ch (proofs : seg_proofs); - close_out ch - -module StringOrd = struct type t = string let compare = String.compare end -module StringSet = Set.Make(StringOrd) - -let get_used_load_paths () = - StringSet.elements - (List.fold_left (fun acc m -> StringSet.add - (Filename.dirname (library_full_filename m)) acc) - StringSet.empty !libraries_loaded_list) - -let _ = Nativelib.get_load_paths := get_used_load_paths diff --git a/library/library.mli b/library/library.mli deleted file mode 100644 index a976be0184..0000000000 --- a/library/library.mli +++ /dev/null @@ -1,84 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Libnames - -(** This module provides functions to load, open and save - libraries. Libraries correspond to the subclass of modules that - coincide with a file on disk (the ".vo" files). Libraries on the - disk comes with checksums (obtained with the [Digest] module), which - are checked at loading time to prevent inconsistencies between files - written at various dates. -*) - -(** {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 - -(** {6 Start the compilation of a library } *) - -(** Segments of a library *) -type seg_sum -type seg_lib -type seg_univ = (* cst, all_cst, finished? *) - Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool -type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr Future.computation array - -(** Open a module (or a library); if the boolean is true then it's also - an export otherwise just a simple import *) -val import_module : bool -> qualid list -> unit - -(** 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 : - string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs -val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit - -(** {6 Interrogate the status of libraries } *) - - (** - Tell if a library is loaded or opened *) -val library_is_loaded : DirPath.t -> bool -val library_is_opened : DirPath.t -> bool - - (** - Tell which libraries are loaded or imported *) -val loaded_libraries : unit -> DirPath.t list -val opened_libraries : unit -> DirPath.t list - - (** - Return the full filename of a loaded library. *) -val library_full_filename : DirPath.t -> string - - (** - Overwrite the filename of all libraries (used when restoring a state) *) -val overwrite_library_filenames : string -> unit - -(** {6 Locate a library in the load paths } *) -exception LibUnmappedDir -exception LibNotFound -type library_location = LibLoaded | LibInPath - -val locate_qualified_library : - ?root:DirPath.t -> ?warn:bool -> qualid -> - library_location * DirPath.t * CUnix.physical_path -(** Locates a library by implicit name. - - @raise LibUnmappedDir if the library is not in the path - @raise LibNotFound if there is no corresponding file in the path - -*) - -(** {6 Native compiler. } *) -val native_name_from_filename : string -> string diff --git a/library/library.mllib b/library/library.mllib index 8f694f4a31..a6188f7661 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -4,14 +4,8 @@ Libobject Summary Nametab Global -Decl_kinds Lib -Declaremods -Loadpath -Library States Kindops Goptions -Decls -Keys Coqlib diff --git a/library/loadpath.ml b/library/loadpath.ml deleted file mode 100644 index fc13c864d0..0000000000 --- a/library/loadpath.ml +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Util -open CErrors -open Names -open Libnames - -(** Load paths. Mapping from physical to logical paths. *) - -type t = { - path_physical : CUnix.physical_path; - path_logical : DirPath.t; - path_implicit : bool; -} - -let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" - -let logical p = p.path_logical - -let physical p = p.path_physical - -let get_load_paths () = !load_paths - -let anomaly_too_many_paths path = - anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") - -let find_load_path phys_dir = - let phys_dir = CUnix.canonical_path_name phys_dir in - let filter p = String.equal p.path_physical phys_dir in - let paths = List.filter filter !load_paths in - match paths with - | [] -> raise Not_found - | [p] -> p - | _ -> anomaly_too_many_paths phys_dir - -let is_in_load_paths phys_dir = - let dir = CUnix.canonical_path_name phys_dir in - let lp = get_load_paths () in - let check_p p = String.equal dir p.path_physical in - List.exists check_p lp - -let remove_load_path dir = - let filter p = not (String.equal p.path_physical dir) in - load_paths := List.filter filter !load_paths - -let warn_overriding_logical_loadpath = - CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" - (fun (phys_path, old_path, coq_path) -> - str phys_path ++ strbrk " was previously bound to " ++ - DirPath.print old_path ++ strbrk "; it is remapped to " ++ - DirPath.print coq_path) - -let add_load_path phys_path coq_path ~implicit = - let phys_path = CUnix.canonical_path_name phys_path in - let filter p = String.equal p.path_physical phys_path in - let binding = { - path_logical = coq_path; - path_physical = phys_path; - path_implicit = implicit; - } in - match List.filter filter !load_paths with - | [] -> - load_paths := binding :: !load_paths - | [{ path_logical = old_path; path_implicit = old_implicit }] -> - let replace = - if DirPath.equal coq_path old_path then - implicit <> old_implicit - else - let () = - (* Do not warn when overriding the default "-I ." path *) - if not (DirPath.equal old_path Libnames.default_root_prefix) then - warn_overriding_logical_loadpath (phys_path, old_path, coq_path) - in - true in - if replace then - begin - remove_load_path phys_path; - load_paths := binding :: !load_paths; - end - | _ -> anomaly_too_many_paths phys_path - -let filter_path f = - let rec aux = function - | [] -> [] - | p :: l -> - if f p.path_logical then (p.path_physical, p.path_logical) :: aux l - else aux l - in - aux !load_paths - -let expand_path ?root dir = - let rec aux = function - | [] -> [] - | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> - let success = - match root with - | None -> - if implicit then is_dirpath_suffix_of dir lg - else DirPath.equal dir lg - | Some root -> - is_dirpath_prefix_of root lg && - is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in - if success then (ph, lg) :: aux l else aux l in - aux !load_paths - -let locate_file fname = - let paths = List.map physical !load_paths in - let _,longfname = - System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in - longfname diff --git a/library/loadpath.mli b/library/loadpath.mli deleted file mode 100644 index 4044ca1127..0000000000 --- a/library/loadpath.mli +++ /dev/null @@ -1,57 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names - -(** * Load paths. - - A load path is a physical path in the file system; to each load path is - associated a Coq [DirPath.t] (the "logical" path of the physical path). - -*) - -type t -(** Type of loadpath bindings. *) - -val physical : t -> CUnix.physical_path -(** Get the physical path (filesystem location) of a loadpath. *) - -val logical : t -> DirPath.t -(** Get the logical path (Coq module hierarchy) of a loadpath. *) - -val get_load_paths : unit -> t list -(** Get the current loadpath association. *) - -val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit -(** [add_load_path phys log type] adds the binding [phys := log] to the current - loadpaths. *) - -val remove_load_path : CUnix.physical_path -> unit -(** Remove the current logical path binding associated to a given physical path, - if any. *) - -val find_load_path : CUnix.physical_path -> t -(** Get the binding associated to a physical path. Raises [Not_found] if there - is none. *) - -val is_in_load_paths : CUnix.physical_path -> bool -(** Whether a physical path is currently bound. *) - -val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list -(** Given a relative logical path, associate the list of absolute physical and - logical paths which are possible matches of it. *) - -val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list -(** As {!expand_path} but uses a filter function instead, and ignores the - implicit status of loadpaths. *) - -val locate_file : string -> string -(** Locate a file among the registered paths. Do not use this function, as - it does not respect the visibility of paths. *) diff --git a/library/nametab.ml b/library/nametab.ml index 95890b2edf..aed7d08ac1 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -43,12 +43,6 @@ module GlobDirRef = struct 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 let error_global_not_found qid = @@ -398,6 +392,7 @@ let push_xref visibility sp xref = | _ -> begin if ExtRefTab.exists sp !the_ccitab then + let open GlobRef in match ExtRefTab.find sp !the_ccitab with | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) | TrueGlobal( ConstructRef _) as xref -> @@ -489,6 +484,7 @@ let completion_canditates qualid = (* Derived functions *) let locate_constant qid = + let open GlobRef in match locate_extended qid with | TrueGlobal (ConstRef kn) -> kn | _ -> raise Not_found @@ -516,10 +512,6 @@ let exists_cci sp = ExtRefTab.exists sp !the_ccitab let exists_dir dir = DirTab.exists dir !the_dirtab -let exists_section = exists_dir - -let exists_module = exists_dir - let exists_modtype sp = MPTab.exists sp !the_modtypetab let exists_universe kn = UnivTab.exists kn !the_univtab @@ -527,6 +519,7 @@ let exists_universe kn = UnivTab.exists kn !the_univtab (* Reverse locate functions ***********************************************) let path_of_global ref = + let open GlobRef in match ref with | VarRef id -> make_path DirPath.empty id | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab @@ -552,6 +545,7 @@ let path_of_universe mp = (* Shortest qualid functions **********************************************) let shortest_qualid_of_global ?loc ctx ref = + let open GlobRef in match ref with | VarRef id -> make_qualid ?loc DirPath.empty id | _ -> @@ -580,15 +574,9 @@ let pr_global_env env ref = if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e let global_inductive qid = + let open GlobRef in match global qid with | IndRef ind -> ind | ref -> user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" (pr_qualid qid ++ spc () ++ str "is not an inductive type") - -(********************************************************************) - -(* Deprecated synonyms *) - -let extended_locate = locate_extended -let absolute_reference = global_of_path diff --git a/library/nametab.mli b/library/nametab.mli index fccb8fd918..6ee22fc283 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -38,7 +38,7 @@ open Globnames } {- [exists : full_user_name -> bool] - Is the [full_user_name] already atributed as an absolute user name + Is the [full_user_name] already attributed as an absolute user name of some object? } {- [locate : qualid -> object_reference] @@ -89,13 +89,6 @@ module GlobDirRef : sig 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 (** Raises a globalization error *) @@ -170,10 +163,6 @@ val extended_global_of_path : full_path -> extended_global_reference 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 } *) @@ -220,11 +209,6 @@ 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 -> Univ.Level.UGlobal.t -> qualid -(** Deprecated synonyms *) - -val extended_locate : qualid -> extended_global_reference (*= locate_extended *) -val absolute_reference : full_path -> GlobRef.t (** = global_of_path *) - (** {5 Generic name handling} *) (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *) diff --git a/library/states.ml b/library/states.ml index 92bdc410a3..0be153d96a 100644 --- a/library/states.ml +++ b/library/states.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -9,7 +9,6 @@ (************************************************************************) open Util -open System type state = Lib.frozen * Summary.frozen @@ -25,13 +24,6 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let extern_state s = - 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); - Library.overwrite_library_filenames s - (* Rollback. *) let with_state_protection f x = diff --git a/library/states.mli b/library/states.mli index 52feb95222..4870f48fc3 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,9 +15,6 @@ freezing the states of both [Lib] and [Summary]. We provide functions to write and restore state to and from a given file. *) -val intern_state : string -> unit -val extern_state : string -> unit - type state val freeze : marshallable:bool -> state val unfreeze : state -> unit diff --git a/library/summary.ml b/library/summary.ml index 8fbca44353..d3ae42694a 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -153,7 +153,7 @@ let (!) r = CEphemeron.get (fst !r) let ref ?(freeze=fun x -> x) ~name init = - let r = Pervasives.ref (CEphemeron.create init, name) in + let r = pervasives_ref (CEphemeron.create init, name) in declare_summary name { freeze_function = (fun ~marshallable -> freeze !r); unfreeze_function = ((:=) r); diff --git a/library/summary.mli b/library/summary.mli index 0d77d725ac..3a122edf3d 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -28,7 +28,7 @@ type 'a summary_declaration = { Beware: for tables registered dynamically after the initialization of Coq, their init functions may not be run immediately. It is hence - the responsability of plugins to initialize themselves properly. + the responsibility of plugins to initialize themselves properly. *) val declare_summary : string -> 'a summary_declaration -> unit |