diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 17 | ||||
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | library/library.ml | 132 | ||||
| -rw-r--r-- | library/library.mli | 34 | ||||
| -rw-r--r-- | library/library.mllib | 1 | ||||
| -rw-r--r-- | library/loadpath.ml | 119 | ||||
| -rw-r--r-- | library/loadpath.mli | 57 |
7 files changed, 53 insertions, 311 deletions
diff --git a/library/global.ml b/library/global.ml index 58e2380440..d5ffae7716 100644 --- a/library/global.ml +++ b/library/global.ml @@ -132,9 +132,20 @@ 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 -> + Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) + | OpaqueDef o -> + Some (Opaqueproof.force_proof access otab o, 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..aa9fc18477 100644 --- a/library/global.mli +++ b/library/global.mli @@ -100,13 +100,13 @@ 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 * 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 * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** {6 Compiled libraries } *) diff --git a/library/library.ml b/library/library.ml index d8eaf5f659..039124635e 100644 --- a/library/library.ml +++ b/library/library.ml @@ -264,85 +264,6 @@ 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} *) @@ -355,8 +276,8 @@ 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 option array delayed + | Fetched of 'a option array let opaque_tables = ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t) @@ -394,12 +315,13 @@ let access_opaque_table 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) + 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_constraints = access_univ_table; +} (************************************************************************) (* Internalise libraries *) @@ -407,9 +329,9 @@ 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 + Univ.ContextSet.t option array * Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr Future.computation array +type seg_proofs = Constr.constr option array let mk_library sd md digests univs = { @@ -450,7 +372,7 @@ let intern_from_file f = 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 +381,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 +389,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 +481,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 @@ -667,7 +591,7 @@ 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 opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in let tasks, utab, dtab = match todo with | None -> None, None, None @@ -680,16 +604,6 @@ let save_library_to ?todo ~output_native_objects dir f otab = 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 ()); diff --git a/library/library.mli b/library/library.mli index 390299bf56..2c0673c3b1 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,7 +22,11 @@ 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 } *) @@ -30,9 +34,9 @@ val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> u type seg_sum type seg_lib type seg_univ = (* cst, all_cst, finished? *) - Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool + Univ.ContextSet.t option array * Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr Future.computation array +type seg_proofs = Constr.constr option 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 +49,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 * 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 } *) @@ -65,20 +71,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. *) |