diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 6 | ||||
| -rw-r--r-- | library/decl_kinds.ml | 11 | ||||
| -rw-r--r-- | library/global.ml | 8 | ||||
| -rw-r--r-- | library/global.mli | 6 | ||||
| -rw-r--r-- | library/keys.ml | 162 | ||||
| -rw-r--r-- | library/keys.mli | 23 | ||||
| -rw-r--r-- | library/lib.ml | 10 | ||||
| -rw-r--r-- | library/lib.mli | 3 | ||||
| -rw-r--r-- | library/library.ml | 642 | ||||
| -rw-r--r-- | library/library.mli | 77 | ||||
| -rw-r--r-- | library/library.mllib | 3 | ||||
| -rw-r--r-- | library/states.ml | 8 | ||||
| -rw-r--r-- | library/states.mli | 3 |
13 files changed, 21 insertions, 941 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index b1e4ef2b00..11d053624c 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -104,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 diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml deleted file mode 100644 index 17746645ee..0000000000 --- a/library/decl_kinds.ml +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* 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 *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type binding_kind = Explicit | Implicit diff --git a/library/global.ml b/library/global.ml index ca774dbd74..6bb4614aa4 100644 --- a/library/global.ml +++ b/library/global.ml @@ -89,6 +89,9 @@ 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) @@ -116,6 +119,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()) @@ -178,6 +182,10 @@ 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 d034bc4208..d0bd556d70 100644 --- a/library/global.mli +++ b/library/global.mli @@ -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 @@ -133,6 +137,8 @@ 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 (** {6 Retroknowledge } *) diff --git a/library/keys.ml b/library/keys.ml deleted file mode 100644 index 9964992433..0000000000 --- a/library/keys.ml +++ /dev/null @@ -1,162 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* 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 *) -(* * 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 (GlobRef.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 = - try - let rec aux k = - match kind k with - | Const (c, _) -> KGlob (GlobRef.ConstRef c) - | Ind (i, u) -> KGlob (GlobRef.IndRef i) - | Construct (c,u) -> KGlob (GlobRef.ConstructRef c) - | Var id -> KGlob (GlobRef.VarRef id) - | App (f, _) -> aux f - | Proj (p, _) -> KGlob (GlobRef.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 a7adf7791b..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-2019 *) -(* <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/lib.ml b/library/lib.ml index 6b01eb07e9..3f51826315 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -441,9 +441,6 @@ let empty_section_data ~poly = { let sectab = Summary.ref ([] : section_data list) ~name:"section-context" -let sec_implicits = - Summary.ref Id.Map.empty ~name:"section-implicits" - let check_same_poly p sec = if p != sec.sec_poly then user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") @@ -452,14 +449,13 @@ let add_section ~poly () = List.iter (fun tab -> check_same_poly poly tab) !sectab; sectab := empty_section_data ~poly :: !sectab -let add_section_variable ~name ~kind ~poly = +let add_section_variable ~name ~poly = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | s :: sl -> List.iter (fun tab -> check_same_poly poly tab) !sectab; let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in - sectab := s :: sl; - sec_implicits := Id.Map.add name kind !sec_implicits + sectab := s :: sl let add_section_context ctx = match !sectab with @@ -576,8 +572,6 @@ let section_segment_of_reference = let open GlobRef in function let variable_section_segment_of_reference gr = (section_segment_of_reference gr).abstr_ctx -let variable_section_kind id = Id.Map.get id !sec_implicits - let section_instance = let open GlobRef in function | VarRef id -> let eq = function diff --git a/library/lib.mli b/library/lib.mli index 7dc8b52282..9ffa69ef93 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -177,12 +177,11 @@ 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 -> Constr.named_context -val variable_section_kind : Id.t -> Decl_kinds.binding_kind val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> unit +val add_section_variable : name:Id.t -> poly:bool -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit diff --git a/library/library.ml b/library/library.ml deleted file mode 100644 index 0faef7bf84..0000000000 --- a/library/library.ml +++ /dev/null @@ -1,642 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* 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 *) -(* * 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 (Global.env()) ~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 mentioned 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 } - -(************************************************************************) -(** {6 Tables of opaque proof terms} *) - -(** We now store opaque proof terms apart from the rest of the environment. - See the [Indirect] constructor 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 array delayed - | Fetched of 'a array - -let opaque_tables = - ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t) - -let add_opaque_table dp st = - opaque_tables := LibraryMap.add dp st !opaque_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 indirect_accessor = { - Opaqueproof.access_proof = access_opaque_table; - Opaqueproof.access_discharge = Cooking.cook_constr; -} - -(************************************************************************) -(* Internalise libraries *) - -type seg_sum = summary_disk -type seg_lib = library_disk -type seg_univ = (* true = vivo, false = vi *) - Univ.ContextSet.t * bool -type seg_proofs = Opaqueproof.opaque_proofterm 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 ((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 (uall,true) -> - mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall - | Some (_,false) -> - mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty - -module DPMap = Map.Make(DirPath) - -let rec intern_library ~lib_resolver (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 -> lib_resolver 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 ~lib_resolver (needed, contents) dir m f - -and intern_library_deps ~lib_resolver libs dir m from = - let needed, contents = - Array.fold_left (intern_mandatory_library ~lib_resolver dir from) - libs m.library_deps in - (dir :: needed, DPMap.add dir m contents ) - -and intern_mandatory_library ~lib_resolver caller from libs (dir,d) = - let digest, libs = intern_library ~lib_resolver 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 ~lib_resolver libs (dir, f) = - let _, libs = intern_library ~lib_resolver 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 ~lib_resolver modrefl export = - let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], 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:"safe_locate_module" - (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_module" - (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 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 tasks, _, _ = System.marshal_in_segment f ch in - let (s4 : 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 snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - s0, s1, Option.get s2, Option.get tasks, s4 - -(************************************************************************) -(*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, f2t_map = Opaqueproof.dump ~except otab in - let tasks, utab = - match todo with - | 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.ContextSet.empty,false) - in - 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 (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 - Nativelib.compile_library dir ast fn - 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 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 : '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 bb6c42e393..0000000000 --- a/library/library.mli +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* 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 *) -(* * 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 - : lib_resolver:(DirPath.t -> CUnix.physical_path) - -> (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 = (* all_cst, finished? *) - Univ.ContextSet.t * bool -type seg_proofs = Opaqueproof.opaque_proofterm 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 - : CUnix.physical_path - -> seg_sum * seg_lib * seg_univ * '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 Native compiler. } *) -val native_name_from_filename : string -> string - -(** {6 Opaque accessors} *) -val indirect_accessor : Opaqueproof.indirect_accessor diff --git a/library/library.mllib b/library/library.mllib index 35af5fa43b..c34d8911e8 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,4 +1,3 @@ -Decl_kinds Libnames Globnames Libobject @@ -7,9 +6,7 @@ Nametab Global Lib Declaremods -Library States Kindops Goptions -Keys Coqlib diff --git a/library/states.ml b/library/states.ml index a73f16957d..0be153d96a 100644 --- a/library/states.ml +++ b/library/states.ml @@ -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 c4f3eae49d..4870f48fc3 100644 --- a/library/states.mli +++ b/library/states.mli @@ -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 |