diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
commit | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch) | |
tree | 12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /library | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'library')
-rw-r--r-- | library/assumptions.ml | 151 | ||||
-rw-r--r-- | library/assumptions.mli | 15 | ||||
-rw-r--r-- | library/declare.ml | 33 | ||||
-rw-r--r-- | library/declare.mli | 2 | ||||
-rw-r--r-- | library/global.mli | 18 | ||||
-rw-r--r-- | library/globnames.ml | 1 | ||||
-rw-r--r-- | library/goptions.ml | 10 | ||||
-rw-r--r-- | library/libnames.ml | 5 | ||||
-rw-r--r-- | library/libnames.mli | 2 | ||||
-rw-r--r-- | library/library.ml | 326 | ||||
-rw-r--r-- | library/library.mli | 15 | ||||
-rw-r--r-- | library/loadpath.ml | 83 | ||||
-rw-r--r-- | library/loadpath.mli | 16 | ||||
-rw-r--r-- | library/states.ml | 1 | ||||
-rw-r--r-- | library/states.mli | 1 | ||||
-rw-r--r-- | library/summary.ml | 1 | ||||
-rw-r--r-- | library/universes.ml | 9 | ||||
-rw-r--r-- | library/universes.mli | 3 |
18 files changed, 372 insertions, 320 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml index 04ee14fb..62645b23 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -21,6 +21,7 @@ open Names open Term open Declarations open Mod_subst +open Globnames type context_object = | Variable of Id.t (* A section variable or a Let definition *) @@ -158,93 +159,67 @@ let lookup_constant cst = else lookup_constant_in_impl cst (Some cb) with Not_found -> lookup_constant_in_impl cst None -let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = - modcache := MPmap.empty; - let (idts,knst) = st in - (* Infix definition for chaining function that accumulate - on a and a ContextObjectSet, ContextObjectMap. *) - let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in - (* This function eases memoization, by checking if an object is already - stored before trying and applying a function. - If the object is there, the function is not fired (we are in a - particular case where memoized object don't need a treatment at all). - If the object isn't there, it is stored and the function is fired*) - let try_and_go o f s m = - if ContextObjectSet.mem o s then - (s,m) - else - f (ContextObjectSet.add o s) m - in - let identity2 s m = (s,m) +(** Graph traversal of an object, collecting on the way the dependencies of + traversed objects *) +let rec traverse accu t = match kind_of_term t with +| Var id -> + let body () = match Global.lookup_named id with (_, body, _) -> body in + traverse_object accu body (VarRef id) +| Const (kn, _) -> + let body () = Global.body_of_constant_body (lookup_constant kn) in + traverse_object accu body (ConstRef kn) +| Ind (ind, _) -> + traverse_object accu (fun () -> None) (IndRef ind) +| Construct (cst, _) -> + traverse_object accu (fun () -> None) (ConstructRef cst) +| Meta _ | Evar _ -> assert false +| _ -> Constr.fold traverse accu t + +and traverse_object (curr, data) body obj = + let data = + if Refmap.mem obj data then data + else match body () with + | None -> Refmap.add obj Refset.empty data + | Some body -> + let (contents, data) = traverse (Refset.empty, data) body in + Refmap.add obj contents data in - (* Goes recursively into the term to see if it depends on assumptions. - The 3 important cases are : - - Const _ where we need to first unfold the constant and return - the needed assumptions of its body in the environment, - - Rel _ which means the term is a variable which has been bound - earlier by a Lambda or a Prod (returns [] ), - - Var _ which means that the term refers to a section variable or - a "Let" definition, in the former it is an assumption of [t], - in the latter is must be unfolded like a Const. - The other cases are straightforward recursion. - Calls to the environment are memoized, thus avoiding exploration of - the DAG of the environment as if it was a tree (can cause - exponential behavior and prevent the algorithm from terminating - in reasonable time). [s] is a set of [context_object], representing - the object already visited.*) - let rec do_constr t s acc = - let rec iter t = - match kind_of_term t with - | Var id -> do_memoize_id id - | Meta _ | Evar _ -> assert false - | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> - (iter e1)**(iter e2) - | LetIn (_,e1,e2,e3) -> (iter e1)**(iter e2)**(iter e3) - | App (e1, e_array) -> (iter e1)**(iter_array e_array) - | Case (_,e1,e2,e_array) -> (iter e1)**(iter e2)**(iter_array e_array) - | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> - (iter_array e1_array) ** (iter_array e2_array) - | Const (kn,_) -> do_memoize_kn kn - | _ -> identity2 (* closed atomic types + rel *) - and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2 - in iter t s acc - - and add_id id s acc = - (* a Var can be either a variable, or a "Let" definition.*) - match Global.lookup_named id with - | (_,None,t) -> - (s,ContextObjectMap.add (Variable id) t acc) - | (_,Some bdy,_) -> do_constr bdy s acc - - and do_memoize_id id = - try_and_go (Variable id) (add_id id) - - and add_kn kn s acc = + (Refset.add obj curr, data) + +let traverse t = + let () = modcache := MPmap.empty in + traverse (Refset.empty, Refmap.empty) t + +(** Hopefully bullet-proof function to recover the type of a constant. It just + ignores all the universe stuff. There are many issues that can arise when + considering terms out of any valid environment, so use with caution. *) +let type_of_constant cb = match cb.Declarations.const_type with +| Declarations.RegularArity ty -> ty +| Declarations.TemplateArity (ctx, arity) -> + Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level) + +let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = + let (idts, knst) = st in + (** Only keep the transitive dependencies *) + let (_, graph) = traverse t in + let fold obj _ accu = match obj with + | VarRef id -> + let (_, body, t) = Global.lookup_named id in + if Option.is_empty body then ContextObjectMap.add (Variable id) t accu + else accu + | ConstRef kn -> let cb = lookup_constant kn in - let do_type cst = - let ctype = Global.type_of_global_unsafe (Globnames.ConstRef kn) in - (s,ContextObjectMap.add cst ctype acc) - in - let (s,acc) = - if Declareops.constant_has_body cb then - if Declareops.is_opaque cb || not (Cpred.mem kn knst) then - (** it is opaque *) - if add_opaque then do_type (Opaque kn) - else (s, acc) - else - if add_transparent then do_type (Transparent kn) - else (s, acc) - else (s, acc) - in - match Global.body_of_constant_body cb with - | None -> do_type (Axiom kn) - | Some body -> do_constr body s acc - - and do_memoize_kn kn = - try_and_go (Axiom kn) (add_kn kn) - - in - fun t -> - snd (do_constr t - (ContextObjectSet.empty) - (ContextObjectMap.empty)) + if not (Declareops.constant_has_body cb) then + let t = type_of_constant cb in + ContextObjectMap.add (Axiom kn) t accu + else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then + let t = type_of_constant cb in + ContextObjectMap.add (Opaque kn) t accu + else if add_transparent then + let t = type_of_constant cb in + ContextObjectMap.add (Transparent kn) t accu + else + accu + | IndRef _ | ConstructRef _ -> accu + in + Refmap.fold fold graph ContextObjectMap.empty diff --git a/library/assumptions.mli b/library/assumptions.mli index 0a2c62f5..bb36a972 100644 --- a/library/assumptions.mli +++ b/library/assumptions.mli @@ -9,6 +9,7 @@ open Util open Names open Term +open Globnames (** A few declarations for the "Print Assumption" command @author spiwack *) @@ -23,8 +24,18 @@ module ContextObjectSet : Set.S with type elt = context_object module ContextObjectMap : Map.ExtS with type key = context_object and module Set := ContextObjectSet -(** collects all the assumptions (optionally including opaque definitions) - on which a term relies (together with their type) *) +(** Collects all the objects on which a term directly relies, bypassing kernel + opacity, together with the recursive dependence DAG of objects. + + WARNING: some terms may not make sense in the environment, because they are + sealed inside opaque modules. Do not try to do anything fancy with those + terms apart from printing them, otherwise demons may fly out of your nose. +*) +val traverse : constr -> (Refset.t * Refset.t Refmap.t) + +(** Collects all the assumptions (optionally including opaque definitions) + on which a term relies (together with their type). The above warning of + {!traverse} also applies. *) val assumptions : ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> constr -> Term.types ContextObjectMap.t diff --git a/library/declare.ml b/library/declare.ml index 7f42a747..c3181e4c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -253,24 +253,25 @@ let declare_sideff env fix_exn se = if Constant.equal c c' then Some (x,kn) else None) inds_consts) knl)) -let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = - let cd = (* We deal with side effects of non-opaque constants *) +let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = + let cd = (* We deal with side effects *) match cd with - | Entries.DefinitionEntry ({ - const_entry_opaque = false; const_entry_body = bo } as de) - | Entries.DefinitionEntry ({ - const_entry_polymorphic = true; const_entry_body = bo } as de) - -> - let _, seff = Future.force bo in - if Declareops.side_effects_is_empty seff then cd - else begin - let seff = Declareops.uniquize_side_effects seff in - Declareops.iter_side_effects - (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff; - Entries.DefinitionEntry { de with - const_entry_body = Future.chain ~pure:true bo (fun (pt, _) -> - pt, Declareops.no_seff) } + | Entries.DefinitionEntry de -> + if export_seff || + not de.const_entry_opaque || + de.const_entry_polymorphic then + let bo = de.const_entry_body in + let _, seff = Future.force bo in + if Declareops.side_effects_is_empty seff then cd + else begin + let seff = Declareops.uniquize_side_effects seff in + Declareops.iter_side_effects + (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff; + Entries.DefinitionEntry { de with + const_entry_body = Future.chain ~pure:true bo (fun (pt, _) -> + pt, Declareops.no_seff) } end + else cd | _ -> cd in let cst = { diff --git a/library/declare.mli b/library/declare.mli index 03b66271..d8a00db0 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -53,7 +53,7 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> constr -> definition_entry val declare_constant : - ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant + ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> diff --git a/library/global.mli b/library/global.mli index af23d9b7..62d7ea32 100644 --- a/library/global.mli +++ b/library/global.mli @@ -118,9 +118,23 @@ val is_template_polymorphic : Globnames.global_reference -> bool val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types Univ.in_universe_context -val type_of_global_unsafe : Globnames.global_reference -> Constr.types +(** Returns the type of the constant in its global or local universe + context. The type should not be used without pushing it's universe + context in the environmnent of usage. For non-universe-polymorphic + constants, it does not matter. *) -(** Returns the universe context of the global reference (whatever it's polymorphic status is). *) +val type_of_global_unsafe : Globnames.global_reference -> Constr.types +(** Returns the type of the constant, forgetting its universe context if + it is polymorphic, use with care: for polymorphic constants, the + type cannot be used to produce a term used by the kernel. For safe + handling of polymorphic global references, one should look at a + particular instantiation of the reference, in some particular + universe context (part of an [env] or [evar_map]), see + e.g. [type_of_constant_in]. If you want to create a fresh instance + of the reference and get its type look at [Evd.fresh_global] or + [Evarutil.new_global] and [Retyping.get_type_of]. *) + +(** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : Globnames.global_reference -> Univ.universe_context (** {6 Retroknowledge } *) diff --git a/library/globnames.ml b/library/globnames.ml index 5eb091af..3befaa9a 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Errors open Names open Term diff --git a/library/goptions.ml b/library/goptions.ml index 4aea3368..ef25fa59 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -268,10 +268,14 @@ let declare_option cast uncast begin fun v -> add_anonymous_leaf (gdecl_obj v) end else write,write,write in + let warn () = + if depr then + msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") + in let cread () = cast (read ()) in - let cwrite v = write (uncast v) in - let clwrite v = lwrite (uncast v) in - let cgwrite v = gwrite (uncast v) in + let cwrite v = warn (); write (uncast v) in + let clwrite v = warn (); lwrite (uncast v) in + let cgwrite v = warn (); gwrite (uncast v) in value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab; write diff --git a/library/libnames.ml b/library/libnames.ml index f2a9d041..cdaec6a3 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -32,6 +32,11 @@ let is_dirpath_prefix_of d1 d2 = List.prefix_of Id.equal (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) +let is_dirpath_suffix_of dir1 dir2 = + let dir1 = DirPath.repr dir1 in + let dir2 = DirPath.repr dir2 in + List.prefix_of Id.equal dir1 dir2 + let chop_dirpath n d = let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in DirPath.make (List.rev d1), DirPath.make (List.rev d2) diff --git a/library/libnames.mli b/library/libnames.mli index 3b5feb94..b95c0887 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -37,6 +37,8 @@ val append_dirpath : DirPath.t -> DirPath.t -> DirPath.t val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool +val is_dirpath_suffix_of : DirPath.t -> DirPath.t -> bool + module Dirset : Set.S with type elt = DirPath.t module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset diff --git a/library/library.ml b/library/library.ml index b078e2c4..b4261309 100644 --- a/library/library.ml +++ b/library/library.ml @@ -17,6 +17,59 @@ open Libobject open Lib (************************************************************************) +(*s Low-level interning/externing of libraries to files *) + +(*s Loading from disk to cache (preparation phase) *) + +let (raw_extern_library, raw_intern_library) = + System.raw_extern_intern Coq_config.vo_magic_number + +(************************************************************************) +(** Serialized objects loaded on-the-fly *) + +exception Faulty of string + +module Delayed : +sig + +type 'a delayed +val in_delayed : string -> in_channel -> 'a delayed +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; } + +(** 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 = System.with_magic_number_check 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 Errors.noncritical e -> raise (Faulty f) + +end + +open Delayed + + +(************************************************************************) (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) @@ -42,12 +95,19 @@ type library_t = { library_extra_univs : Univ.universe_context_set; } +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 = Summary.ref LibraryMap.empty ~name:"LIBRARY" +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) *) @@ -89,32 +149,31 @@ let library_is_loaded dir = with Not_found -> false let library_is_opened dir = - List.exists (fun m -> DirPath.equal m.library_name dir) !libraries_imports_list + List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list -let loaded_libraries () = - List.map (fun m -> m.library_name) !libraries_loaded_list +let loaded_libraries () = !libraries_loaded_list -let opened_libraries () = - List.map (fun m -> m.library_name) !libraries_imports_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 m = - let dirname = Filename.dirname (library_full_filename m.library_name) in - let prefix = Nativecode.mod_uid_of_dirpath m.library_name ^ "." in + 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 not !Flags.no_native_compiler then Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function - | [] -> link m; [m] - | m'::_ as l when DirPath.equal m'.library_name m.library_name -> l + | [] -> link m; [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 m.library_name m !libraries_table + 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 @@ -125,7 +184,7 @@ let register_loaded_library m = let rec remember_last_of_each l m = match l with | [] -> [m] - | m'::l' when DirPath.equal m'.library_name m.library_name -> remember_last_of_each l' 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 = @@ -139,17 +198,15 @@ let register_open_library export m = (* [open_library export explicit m] opens library [m] if not already opened _or_ if explicitly asked to be (re)opened *) -let eq_lib_name m1 m2 = DirPath.equal m1.library_name m2.library_name - let open_library export explicit_libs m = if (* Only libraries indirectly to open are not reopen *) (* Libraries explicitly mentionned by the user are always reopen *) - List.exists (eq_lib_name m) explicit_libs - || not (library_is_opened m.library_name) + 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.library_name) + Declaremods.really_import_module (MPfile m) end else if export then @@ -164,47 +221,44 @@ let open_libraries export modl = (fun l m -> let subimport = Array.fold_left - (fun l m -> remember_last_of_each l (try_find_library m)) - l m.library_imports - in remember_last_of_each subimport m) + (fun l m -> remember_last_of_each l m) + l m.libsum_imports + in remember_last_of_each subimport m.libsum_name) [] modl in - List.iter (open_library export modl) to_open_list + let explicit = List.map (fun m -> m.libsum_name) modl in + List.iter (open_library export explicit) to_open_list (**********************************************************************) -(* import and export - synchronous operations*) +(* 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 i (_,(dir,export)) = +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 [try_find_library dir] + open_libraries export (List.map try_find_library modl) -let cache_import obj = - open_import 1 obj +let cache_import_library obj = + open_import_library 1 obj -let subst_import (_,o) = o +let subst_import_library (_,o) = o -let classify_import (_,export as obj) = +let classify_import_library (_,export as obj) = if export then Substitute obj else Dispose -let in_import : DirPath.t * bool -> obj = +let in_import_library : DirPath.t list * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with - cache_function = cache_import; - open_function = open_import; - subst_function = subst_import; - classify_function = classify_import } + cache_function = cache_import_library; + open_function = open_import_library; + subst_function = subst_import_library; + classify_function = classify_import_library } (************************************************************************) -(*s Low-level interning/externing of libraries to files *) - -(*s Loading from disk to cache (preparation phase) *) - -let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern Coq_config.vo_magic_number - -(************************************************************************) (*s Locate absolute or partially qualified library names in the path *) exception LibUnmappedDir @@ -214,8 +268,9 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = Loadpath.expand_root_path pref 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 @@ -232,10 +287,20 @@ let locate_absolute_library dir = | [vo;vi] -> dir, vo | _ -> assert false -let locate_qualified_library warn qid = +let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) let dir, base = repr_qualid qid in - let loadpath = Loadpath.expand_path dir in + let loadpath = match root with + | None -> Loadpath.expand_path dir + | Some root -> + let filter path = + if is_dirpath_prefix_of root path then + let path = drop_dirpath_prefix root path in + is_dirpath_suffix_of dir path + else false + in + Loadpath.filter_path filter + in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let find ext = try @@ -279,14 +344,6 @@ let try_locate_absolute_library dir = | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) -let try_locate_qualified_library (loc,qid) = - try - let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in - dir,f - with - | LibUnmappedDir -> error_unmapped_dir qid - | LibNotFound -> error_lib_not_found qid - (************************************************************************) (** {6 Tables of opaque proof terms} *) @@ -296,34 +353,10 @@ let try_locate_qualified_library (loc,qid) = terms, and access them only when a specific command (e.g. Print or Print Assumptions) needs it. *) -exception Faulty - -(** Fetching a table of opaque terms at position [pos] in file [f], - expecting to find first a copy of [digest]. *) - -let fetch_table what dp (f,pos,digest) = - let dir_path = Names.DirPath.to_string dp in - try - msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); - let ch = System.with_magic_number_check raw_intern_library f in - let () = seek_in ch pos in - if not (String.equal (System.digest_in f ch) digest) then raise Faulty; - let table, pos', digest' = System.marshal_in_segment f ch in - let () = close_in ch in - let ch' = open_in f in - if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty; - let () = close_in ch' in - table - with e when Errors.noncritical e -> - error - ("The file "^f^" (bound to " ^ dir_path ^ - ") is inaccessible or corrupted,\n" ^ - "cannot load some "^what^" in it.\n") - (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of string * int * Digest.t + | ToFetch of 'a Future.computation array delayed | Fetched of 'a Future.computation array let opaque_tables = @@ -336,25 +369,33 @@ let add_opaque_table dp st = let add_univ_table dp st = univ_tables := LibraryMap.add dp st !univ_tables -let access_table fetch_table add_table tables dp i = - let t = match LibraryMap.find dp tables with +let access_table what tables dp i = + let t = match LibraryMap.find dp !tables with | Fetched t -> t - | ToFetch (f,pos,digest) -> - let t = fetch_table dp (f,pos,digest) in - add_table dp (Fetched t); + | ToFetch f -> + let dir_path = Names.DirPath.to_string dp in + msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + let t = + try fetch_delayed f + with Faulty f -> + error + ("The file "^f^" (bound to " ^ dir_path ^ + ") is inaccessible or corrupted,\n" ^ + "cannot load some "^what^" 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 = - access_table - (fetch_table "opaque proofs") - add_opaque_table !opaque_tables dp i + let what = "opaque proofs" in + access_table what opaque_tables dp i + let access_univ_table dp i = try - Some (access_table - (fetch_table "universe contexts of opaque proofs") - add_univ_table !univ_tables dp i) + let what = "universe contexts of opaque proofs" in + Some (access_table what univ_tables dp i) with Not_found -> None let () = @@ -381,15 +422,22 @@ let mk_library md digests univs = 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 = System.with_magic_number_check raw_intern_library f in let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment 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 pos, digest = 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 lmd.md_name f; - add_opaque_table lmd.md_name (ToFetch (f,pos,digest)); + add_opaque_table lmd.md_name (ToFetch del_opaque); let open Safe_typing in match univs with | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty @@ -402,16 +450,13 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) -let deps_to_string deps = - Array.fold_left (fun s (n, _) -> s^"\n - "^(DirPath.to_string n)) "" deps - let rec intern_library (needed, contents) (dir, f) from = Pp.feedback(Feedback.FileDependency (from, f)); (* Look if in the current logical environment *) - try find_library dir, (needed, contents) + 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, (needed, contents) + try (DPMap.find dir contents).library_digests, (needed, contents) with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in @@ -421,15 +466,15 @@ let rec intern_library (needed, contents) (dir, f) from = pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); - m, intern_library_deps (needed, contents) dir m (Some f) + m.library_digests, intern_library_deps (needed, contents) dir m (Some f) and intern_library_deps libs dir m from = let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in (dir :: needed, DPMap.add dir m contents ) and intern_mandatory_library caller from libs (dir,d) = - let m, libs = intern_library libs (try_locate_absolute_library dir) from in - if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then + let digest, libs = intern_library libs (try_locate_absolute_library dir) from in + if not (Safe_typing.digest_match ~actual:digest ~required:d) then errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^ ".vo makes inconsistent assumptions over library " ^ DirPath.to_string dir)); @@ -500,7 +545,7 @@ let register_library m = m.library_objects m.library_digests m.library_extra_univs; - register_loaded_library m + register_loaded_library (mk_summary m) (* Follow the semantics of Anticipate object: - called at module or module type closing when a Require occurs in @@ -543,23 +588,19 @@ let require_library_from_dirpath modrefl export = begin add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> - List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) + add_anonymous_leaf (in_import_library (modrefl,exp))) export end else add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library qidl export = - let modrefl = List.map try_locate_qualified_library qidl in - require_library_from_dirpath modrefl export - let require_library_from_file idopt file export = let modref,needed = rec_intern_library_from_file idopt file in let needed = List.rev_map snd needed in if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); - Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) + Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp))) export end else @@ -568,21 +609,38 @@ let require_library_from_file idopt file export = (* the function called by Vernacentries.vernac_import *) -let import_module export (loc,qid) = - try - match Nametab.locate_module qid with - | MPfile dir -> - if Lib.is_module_or_modtype () || not export then - add_anonymous_leaf (in_import (dir, export)) - else - add_anonymous_leaf (in_import (dir, export)) - | mp -> - Declaremods.import_module export mp - with - Not_found -> - user_err_loc - (loc,"import_library", - str ((string_of_qualid qid)^" is not a module")) +let safe_locate_module (loc,qid) = + try Nametab.locate_module qid + with Not_found -> + user_err_loc + (loc,"import_library", str (string_of_qualid qid ^ " 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 + | (loc,dir as m) :: l -> + let m,acc = + try Nametab.locate_module dir, acc + with Not_found-> flush acc; safe_locate_module m, [] 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 (loc,"import_library", + str ((string_of_qualid dir)^" is not a module"))) + | [] -> flush acc + in aux [] modl (************************************************************************) (*s Initializing the compilation of a library. *) @@ -654,10 +712,13 @@ let load_library_todo f = (*s [save_library dir] ends library [dir] and save it to the disk. *) let current_deps () = - List.map (fun m -> m.library_name, m.library_digests) !libraries_loaded_list + let map name = + let m = try_find_library name in + (name, m.libsum_digests) + in + List.map map !libraries_loaded_list -let current_reexports () = - List.map (fun m -> m.library_name) !libraries_exports_list +let current_reexports () = !libraries_exports_list let error_recursively_dependent_library dir = errorlabstrm "" @@ -683,7 +744,7 @@ let save_library_to ?todo dir f otab = f ^ "o", Future.UUIDSet.empty | Some (l,_) -> f ^ "io", - List.fold_left (fun e r -> Future.UUIDSet.add r.Stateid.uuid e) + 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 ~except dir in let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in @@ -692,14 +753,17 @@ let save_library_to ?todo dir f otab = | None -> None, None, None | Some (tasks, rcbackup) -> let tasks = - List.map Stateid.(fun r -> - { r with uuid = Future.UUIDMap.find r.uuid f2t_map }) tasks in + List.map Stateid.(fun (r,b) -> + try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b + with Not_found -> assert b; { r with uuid = -1 }, b) + tasks in Some (tasks,rcbackup), Some (univ_table,Univ.ContextSet.empty,false), Some disch_table in let except = Future.UUIDSet.fold (fun uuid acc -> - Int.Set.add (Future.UUIDMap.find uuid f2t_map) 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 -> @@ -750,11 +814,7 @@ let save_library_raw f lib univs proofs = open Printf -let mem s = - let m = try_find_library s in - h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" - (CObj.size_kb m) (CObj.size_kb m.library_compiled) - (CObj.size_kb m.library_objects))) +let mem s = Pp.mt () module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) @@ -762,7 +822,7 @@ 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.library_name)) acc) + (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 index 13d83a5c..35067068 100644 --- a/library/library.mli +++ b/library/library.mli @@ -21,7 +21,6 @@ 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 : qualid located list -> bool option -> unit val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit val require_library_from_file : Id.t option -> CUnix.physical_path -> bool option -> unit @@ -37,14 +36,14 @@ type seg_proofs = Term.constr Future.computation array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) -val import_module : bool -> qualid located -> unit +val import_module : bool -> qualid located list -> unit (** {6 Start the compilation of a library } *) val start_library : string -> DirPath.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) val save_library_to : - ?todo:((Future.UUID.t,'document) Stateid.request list * 'counters) -> + ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : @@ -73,8 +72,14 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - bool -> qualid -> library_location * DirPath.t * CUnix.physical_path -val try_locate_qualified_library : qualid located -> DirPath.t * string + ?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 Statistics: display the memory use of a library. } *) val mem : DirPath.t -> Pp.std_ppcmds diff --git a/library/loadpath.ml b/library/loadpath.ml index 5876eedd..26af809e 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -12,14 +12,12 @@ open Errors open Names open Libnames -type path_type = ImplicitPath | ImplicitRootPath | RootPath - (** Load paths. Mapping from physical to logical paths. *) type t = { path_physical : CUnix.physical_path; path_logical : DirPath.t; - path_type : path_type; + path_implicit : bool; } let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" @@ -54,32 +52,35 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths -let add_load_path phys_path path_type 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_type = path_type; + path_implicit = implicit; } in match List.filter filter !load_paths with | [] -> load_paths := binding :: !load_paths - | [p] -> - let dir = p.path_logical in - if not (DirPath.equal coq_path dir) - (* If this is not the default -I . to coqtop *) - && not - (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) - && DirPath.equal coq_path (Nameops.default_root_prefix)) - then + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DirPath.equal coq_path old_path then + implicit <> old_implicit + else if DirPath.equal coq_path (Nameops.default_root_prefix) + && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then + false (* This is the default "-I ." path, don't override the old path *) + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DirPath.equal old_path Nameops.default_root_prefix) then + msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath old_path ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path) in + true in + if replace then begin - (* Assume the user is concerned by library naming *) - if not (DirPath.equal dir Nameops.default_root_prefix) then - msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath dir ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path); remove_load_path phys_path; load_paths := binding :: !load_paths; end @@ -89,47 +90,25 @@ let extend_path_with_dirpath p dir = List.fold_left Filename.concat p (List.rev_map Id.to_string (DirPath.repr dir)) -let expand_root_path dir = +let filter_path f = let rec aux = function | [] -> [] | p :: l -> - if p.path_type <> ImplicitPath && is_dirpath_prefix_of p.path_logical dir then - let suffix = drop_dirpath_prefix p.path_logical dir in - extend_path_with_dirpath p.path_physical suffix :: aux l + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l else aux l in aux !load_paths -(* Root p is bound to A.B.C.D and we require file C.D.E.F *) -(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *) - -(* Root p is bound to A.B.C.C and we require file C.C.E.F *) -(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *) - -let intersections d1 d2 = - let rec aux d1 = - if DirPath.is_empty d1 then [d2] else - let rest = aux (snd (chop_dirpath 1 d1)) in - if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest - else rest in - aux d1 - -let expand p dir = - let ph = extend_path_with_dirpath p.path_physical dir in - let log = append_dirpath p.path_logical dir in - (ph, log) - let expand_path dir = let rec aux = function | [] -> [] - | p :: l -> - match p.path_type with - | ImplicitPath -> expand p dir :: aux l - | ImplicitRootPath -> - let inters = intersections p.path_logical dir in - List.map (expand p) inters @ aux l - | RootPath -> - if is_dirpath_prefix_of p.path_logical dir then - expand p (drop_dirpath_prefix p.path_logical dir) :: aux l - else aux l in + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + match implicit with + | true -> + (** The path is implicit, so that we only want match the logical suffix *) + if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l + | false -> + (** Otherwise we must match exactly *) + if DirPath.equal dir lg then (ph, lg) :: aux l else aux l + in aux !load_paths diff --git a/library/loadpath.mli b/library/loadpath.mli index 62dc5d59..3251b8c6 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -15,11 +15,6 @@ open Names *) -type path_type = - | ImplicitPath (** Can be implicitly appended to a logical path. *) - | ImplicitRootPath (** Can be implicitly appended to the suffix of a logical path. *) - | RootPath (** Can only be a prefix of a logical path. *) - type t (** Type of loadpath bindings. *) @@ -35,8 +30,8 @@ val get_load_paths : unit -> t list val get_paths : unit -> CUnix.physical_path list (** Same as [get_load_paths] but only get the physical part. *) -val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit -(** [add_load_path phys type log] adds the binding [phys := log] to the current +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 @@ -52,7 +47,8 @@ val is_in_load_paths : CUnix.physical_path -> bool val expand_path : 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 expansions of it. *) + logical paths which are possible matches of it. *) -val expand_root_path : DirPath.t -> CUnix.physical_path list -(** As [expand_path] but restricts to root loadpaths. *) +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. *) diff --git a/library/states.ml b/library/states.ml index a1c2a095..96a487b1 100644 --- a/library/states.ml +++ b/library/states.ml @@ -12,6 +12,7 @@ open System type state = Lib.frozen * Summary.frozen let summary_of_state = snd +let replace_summary (lib,_) s = lib, s let freeze ~marshallable = (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable) diff --git a/library/states.mli b/library/states.mli index 66de1490..4d5d63e0 100644 --- a/library/states.mli +++ b/library/states.mli @@ -21,6 +21,7 @@ val freeze : marshallable:Summary.marshallable -> state val unfreeze : state -> unit val summary_of_state : state -> Summary.frozen +val replace_summary : state -> Summary.frozen -> state (** {6 Rollback } *) diff --git a/library/summary.ml b/library/summary.ml index 7e7628a1..8e2abbf1 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -66,6 +66,7 @@ let freeze_summaries ~marshallable : frozen = let fold id (_, decl) accu = (* to debug missing Lazy.force if marshallable <> `No then begin + let id, _ = Int.Map.find id !summaries in prerr_endline ("begin marshalling " ^ id); ignore(Marshal.to_string (decl.freeze_function marshallable) []); prerr_endline ("end marshalling " ^ id); diff --git a/library/universes.ml b/library/universes.ml index 79070763..9fddc706 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -165,7 +165,7 @@ let leq_constr_univs_infer univs m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts + Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in @@ -213,7 +213,7 @@ let leq_constr_universes m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n + Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in res, !cstrs @@ -772,7 +772,7 @@ let minimize_univ_variables ctx us algs left right cstrs = else try let lev = Option.get (Universe.level inst) in Constraint.add (lev, d, r) cstrs - with Option.IsNone -> assert false) + with Option.IsNone -> failwith "") cstrs dangling in (ctx', us, algs, insts, cstrs'), b @@ -784,7 +784,8 @@ let minimize_univ_variables ctx us algs left right cstrs = | None -> (* Nothing to do *) acc' (acc, (true, false, Universe.make u)) | Some lbound -> - acc' (instantiate_lbound lbound) + try acc' (instantiate_lbound lbound) + with Failure _ -> acc' (acc, (true, false, Universe.make u)) and aux (ctx', us, algs, seen, cstrs as acc) u = try acc, LMap.find u seen with Not_found -> instance acc u diff --git a/library/universes.mli b/library/universes.mli index f2f68d32..252648d7 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -7,12 +7,9 @@ (************************************************************************) open Util -open Pp open Names open Term -open Context open Environ -open Locus open Univ (** Universes *) |