diff options
Diffstat (limited to 'library')
34 files changed, 139 insertions, 409 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 784360dc8a..7cd2e50274 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 *) 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 index 8d5c2fb687..0e2ef95739 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.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,7 +12,9 @@ type discharge = DoDischarge | NoDischarge -type locality = Discharge | Local | Global +type import_status = ImportDefaultBehavior | ImportNeedQualified + +type locality = Discharge | Global of import_status type binding_kind = Explicit | Implicit @@ -46,7 +48,7 @@ type definition_object_kind = | Method | Let -type assumption_object_kind = Definitional | Logical | Conjectural +type assumption_object_kind = Definitional | Logical | Conjectural | Context (* [assumption_kind] diff --git a/library/declaremods.ml b/library/declaremods.ml index 5fd11e187a..fc3e667c20 100644 --- a/library/declaremods.ml +++ b/library/declaremods.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 *) @@ -51,7 +51,7 @@ let inl2intopt = function - Then comes either the object segment itself (for interactive modules), or a compact way to store derived objects (path to - a earlier module + subtitution). + a earlier module + substitution). *) type algebraic_objects = diff --git a/library/declaremods.mli b/library/declaremods.mli index 2b28ba908e..93aadd25de 100644 --- a/library/declaremods.mli +++ b/library/declaremods.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/decls.ml b/library/decls.ml index b766b6e2cb..ef60a44ac7 100644 --- a/library/decls.ml +++ b/library/decls.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 *) diff --git a/library/decls.mli b/library/decls.mli index c0db537427..0d09499b51 100644 --- a/library/decls.mli +++ b/library/decls.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/global.ml b/library/global.ml index 58e2380440..ca774dbd74 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 *) @@ -94,7 +94,7 @@ 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 ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~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_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~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) @@ -132,9 +132,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 *) diff --git a/library/global.mli b/library/global.mli index 984d8c666c..51307b3604 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 *) @@ -42,11 +42,11 @@ val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set val push_named_def : (Id.t * Entries.section_def_entry) -> 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 : - ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants + side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -100,13 +100,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 : Opaqueproof.opaque 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 } *) diff --git a/library/globnames.ml b/library/globnames.ml index 99dcc43ad1..71447c4b81 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 *) diff --git a/library/globnames.mli b/library/globnames.mli index 14e422b743..547755b088 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 *) diff --git a/library/goptions.ml b/library/goptions.ml index f4b8ce9465..c7024ca81d 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 *) @@ -53,9 +53,9 @@ module MakeTable = functor (A : sig type t - type key - val compare : t -> t -> int - val table : (string * key table_of_A) list ref + 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 @@ -74,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 @@ -119,8 +119,9 @@ module MakeTable = } let _ = A.table := (nick, 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 [] @@ -138,7 +139,7 @@ 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 _env x = x let subst _ x = x @@ -158,7 +159,7 @@ let get_ref_table k = String.List.assoc (nickname k) !ref_table module type RefConvertArg = sig type t - val compare : t -> t -> int + module Set : CSig.SetS with type elt = t val encode : Environ.env -> qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t @@ -171,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 diff --git a/library/goptions.mli b/library/goptions.mli index 381ba4d34a..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,8 +70,8 @@ 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 @@ -87,19 +87,19 @@ end module MakeRefTable : functor (A : sig - type t - val compare : t -> t -> int - 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 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. } *) diff --git a/library/keys.ml b/library/keys.ml index 45b6fae2f0..30ecc9dfdb 100644 --- a/library/keys.ml +++ b/library/keys.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 *) diff --git a/library/keys.mli b/library/keys.mli index 198383650a..a7adf7791b 100644 --- a/library/keys.mli +++ b/library/keys.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/kindops.ml b/library/kindops.ml index 247319fa2f..0bf55c62a9 100644 --- a/library/kindops.ml +++ b/library/kindops.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 *) diff --git a/library/kindops.mli b/library/kindops.mli index df39019da4..3c9f2bb7c3 100644 --- a/library/kindops.mli +++ b/library/kindops.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/lib.ml b/library/lib.ml index 4be288ed20..ae657dbd70 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 *) @@ -474,9 +474,6 @@ let extract_hyps (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. *) diff --git a/library/lib.mli b/library/lib.mli index 5da76961a6..f6bd61e2da 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 *) @@ -168,7 +168,6 @@ type abstr_info = private { } 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 diff --git a/library/libnames.ml b/library/libnames.ml index 41b38e0378..18af216e46 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 *) diff --git a/library/libnames.mli b/library/libnames.mli index 7d77d95991..4455e29818 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 *) diff --git a/library/libobject.ml b/library/libobject.ml index 3d17b4a605..72791661bc 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 *) diff --git a/library/libobject.mli b/library/libobject.mli index 00515bd273..a7151d3bf2 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 *) diff --git a/library/library.ml b/library/library.ml index 500e77f89b..0d4148d7e4 100644 --- a/library/library.ml +++ b/library/library.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 *) @@ -208,7 +208,7 @@ let register_open_library export m = 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 *) + (* 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 @@ -264,90 +264,11 @@ let in_import_library : DirPath.t list * bool -> obj = 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, + 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. *) @@ -355,18 +276,14 @@ let try_locate_absolute_library dir = (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of 'a Future.computation array delayed - | Fetched of 'a Future.computation array + | ToFetch of 'a array delayed + | Fetched of 'a 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) + 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 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 @@ -391,15 +308,10 @@ 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 +let indirect_accessor = { + Opaqueproof.access_proof = access_opaque_table; + Opaqueproof.access_discharge = Cooking.cook_constr; +} (************************************************************************) (* Internalise libraries *) @@ -407,9 +319,8 @@ let () = 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 + Univ.ContextSet.t * bool +type seg_proofs = Opaqueproof.opaque_proofterm array let mk_library sd md digests univs = { @@ -433,7 +344,6 @@ let intern_from_file f = 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; @@ -441,16 +351,14 @@ let intern_from_file f = 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); + | Some (uall,true) -> mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall - | Some (utab,_,false) -> - add_univ_table lsd.md_name (Fetched utab); + | Some (_,false) -> 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 = +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 -> @@ -459,7 +367,7 @@ let rec intern_library (needed, contents) (dir, f) from = 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 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" @@ -467,22 +375,24 @@ let rec intern_library (needed, contents) (dir, f) from = 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 + m.library_digests, intern_library_deps ~lib_resolver (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 +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 caller from libs (dir,d) = - let digest, libs = intern_library libs (dir, None) (Some from) in +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 libs (dir, f) = - let _, libs = intern_library libs (dir, Some f) None in +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 = @@ -557,8 +467,8 @@ let warn_require_in_module = 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 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 @@ -616,15 +526,13 @@ let load_library_todo f = 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 + 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 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"); - s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + 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. *) @@ -667,10 +575,10 @@ let save_library_to ?todo ~output_native_objects dir f otab = 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 = + let opaque_table, f2t_map = Opaqueproof.dump ~except otab in + let tasks, utab = match todo with - | None -> None, None, None + | None -> None, None | Some (tasks, rcbackup) -> let tasks = List.map Stateid.(fun (r,b) -> @@ -678,18 +586,8 @@ let save_library_to ?todo ~output_native_objects dir f otab = 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; + Some (Univ.ContextSet.empty,false) + in let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); @@ -709,7 +607,6 @@ let save_library_to ?todo ~output_native_objects dir f otab = 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; @@ -729,7 +626,6 @@ let save_library_raw f sum lib univs proofs = 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 diff --git a/library/library.mli b/library/library.mli index 390299bf56..bb6c42e393 100644 --- a/library/library.mli +++ b/library/library.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,17 +22,20 @@ open Libnames (** {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 +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 = (* 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 +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 *) @@ -45,8 +48,10 @@ val save_library_to : output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit -val load_library_todo : - string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs +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 } *) @@ -65,20 +70,8 @@ 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 + +(** {6 Opaque accessors} *) +val indirect_accessor : Opaqueproof.indirect_accessor diff --git a/library/library.mllib b/library/library.mllib index 8f694f4a31..ef53471377 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -7,7 +7,6 @@ Global Decl_kinds Lib Declaremods -Loadpath Library States Kindops 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 bd0ea5f04f..71ee7a6d5a 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 *) diff --git a/library/nametab.mli b/library/nametab.mli index a4f177aad0..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] diff --git a/library/states.ml b/library/states.ml index 92bdc410a3..a73f16957d 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 *) diff --git a/library/states.mli b/library/states.mli index 52feb95222..c4f3eae49d 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 *) diff --git a/library/summary.ml b/library/summary.ml index 8fbca44353..b3ec4c2db2 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 *) 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 |