From 40479227cba680496bf358e196e57a9a64f9c65b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 20 Sep 2015 00:58:25 +0200 Subject: Nametab: print debug notice only in debug mode. --- library/nametab.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/nametab.ml b/library/nametab.ml index 6af1e686b0..5b6d7cd982 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -524,7 +524,8 @@ let shortest_qualid_of_tactic kn = let pr_global_env env ref = try str (string_of_qualid (shortest_qualid_of_global env ref)) - with Not_found as e -> prerr_endline "pr_global_env not found"; raise e + with Not_found as e -> + if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e let global_inductive r = match global r with -- cgit v1.2.3 From 2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 Sep 2015 18:25:15 +0200 Subject: Hopefully better names to constructors of internal_flag, as discussed with Enrico. --- library/declare.ml | 10 +++++----- library/declare.mli | 6 +++--- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index c3181e4c75..8438380c9c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -28,9 +28,9 @@ open Decl_kinds (** flag for internal message display *) type internal_flag = - | KernelVerbose (* kernel action, a message is displayed *) - | KernelSilent (* kernel action, no message is displayed *) - | UserVerbose (* user action, a message is displayed *) + | UserAutomaticRequest (* kernel action, a message is displayed *) + | InternalTacticRequest (* kernel action, no message is displayed *) + | UserIndividualRequest (* user action, a message is displayed *) (** Declaration of section variables and local definitions *) @@ -253,7 +253,7 @@ 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 ?(export_seff=false) (cd, kind) = +let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = let cd = (* We deal with side effects *) match cd with | Entries.DefinitionEntry de -> @@ -283,7 +283,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff let kn = declare_constant_common id cst in kn -let declare_definition ?(internal=UserVerbose) +let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = let cb = diff --git a/library/declare.mli b/library/declare.mli index d8a00db0cf..76538a6248 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -43,9 +43,9 @@ type constant_declaration = constant_entry * logical_kind *) type internal_flag = - | KernelVerbose - | KernelSilent - | UserVerbose + | UserAutomaticRequest + | InternalTacticRequest + | UserIndividualRequest (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> -- cgit v1.2.3 From b6725a2d0077239e51385a62a526ab9465eea26d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Sep 2015 18:45:40 +0200 Subject: The -compile option now accepts ".v" files and outputs a warning otherwise. --- library/library.ml | 12 ++++++------ library/library.mli | 10 ++++++---- 2 files changed, 12 insertions(+), 10 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index f7ca4e9760..1bcffcd147 100644 --- a/library/library.ml +++ b/library/library.ml @@ -678,22 +678,22 @@ let check_module_name s = | c -> err c let start_library f = - let paths = Loadpath.get_paths () in - let _, longf = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let () = if not (Sys.file_exists f) then + errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f)) + in let ldir0 = try - let lp = Loadpath.find_load_path (Filename.dirname longf) in + let lp = Loadpath.find_load_path (Filename.dirname f) in Loadpath.logical lp with Not_found -> Nameops.default_root_prefix in - let file = Filename.basename f in + let file = Filename.chop_extension (Filename.basename f) in let id = Id.of_string file in check_module_name file; check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in Declaremods.start_library ldir; - ldir,longf + ldir let load_library_todo f = let paths = Loadpath.get_paths () in diff --git a/library/library.mli b/library/library.mli index 967a54e4c8..f2e60718d6 100644 --- a/library/library.mli +++ b/library/library.mli @@ -25,7 +25,7 @@ val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> u val require_library_from_file : Id.t option -> CUnix.physical_path -> bool option -> unit -(** {6 ... } *) +(** {6 Start the compilation of a library } *) (** Segments of a library *) type seg_sum @@ -39,10 +39,12 @@ type seg_proofs = Term.constr Future.computation array an export otherwise just a simple import *) val import_module : bool -> qualid located list -> unit -(** {6 Start the compilation of a library } *) -val start_library : string -> DirPath.t * string +(** Start the compilation of a file as a library. The argument must be an + existing file on the system, and the returned path is the associated + absolute logical path of the library. *) +val start_library : CUnix.physical_path -> DirPath.t -(** {6 End the compilation of a library and save it to a ".vo" file } *) +(** End the compilation of a library and save it to a ".vo" file *) val save_library_to : ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit -- cgit v1.2.3 From 8e25e107a8715728a7227934d7b11035863ee5f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Sep 2015 12:25:35 +0200 Subject: The -require option now accepts a logical path instead of a physical one. --- library/library.ml | 20 +++++--------------- library/library.mli | 3 +-- 2 files changed, 6 insertions(+), 17 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 1bcffcd147..a09f91b15a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,18 +488,8 @@ let rec_intern_library libs mref = let _, libs = intern_library libs mref None in libs -let check_library_short_name f dir = function - | Some id when not (Id.equal id (snd (split_dirpath dir))) -> - errorlabstrm "check_library_short_name" - (str "The file " ++ str f ++ str " contains library" ++ spc () ++ - pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ - pr_id id) - | _ -> () - -let rec_intern_by_filename_only id f = +let rec_intern_by_filename_only f = let m = try intern_from_file f with Sys_error s -> error s in - (* Only the base name is expected to match *) - check_library_short_name f m.library_name id; (* We check no other file containing same library is loaded *) if library_is_loaded m.library_name then begin @@ -518,12 +508,12 @@ let native_name_from_filename f = let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name -let rec_intern_library_from_file idopt f = +let rec_intern_library_from_file f = (* A name is specified, we have to check it contains library id *) let paths = Loadpath.get_paths () in let _, f = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in - rec_intern_by_filename_only idopt f + rec_intern_by_filename_only f (**********************************************************************) (*s [require_library] loads and possibly opens a library. This is a @@ -600,8 +590,8 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library_from_file idopt file export = - let modref,needed = rec_intern_library_from_file idopt file in +let require_library_from_file file export = + let modref,needed = rec_intern_library_from_file 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)); diff --git a/library/library.mli b/library/library.mli index f2e60718d6..3d96f9a751 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,8 +22,7 @@ open Libnames (** 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_file : - Id.t option -> CUnix.physical_path -> bool option -> unit +val require_library_from_file : CUnix.physical_path -> bool option -> unit (** {6 Start the compilation of a library } *) -- cgit v1.2.3 From 2cf609c41f7af83d9eaf43308a368fcb7307e6fa Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 28 Sep 2015 11:04:59 +0200 Subject: Make -load-vernac-object respect the loadpath. This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq. --- library/library.ml | 34 ---------------------------------- library/library.mli | 1 - 2 files changed, 35 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index a09f91b15a..6d7b0f603a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,33 +488,11 @@ let rec_intern_library libs mref = let _, libs = intern_library libs mref None in libs -let rec_intern_by_filename_only f = - let m = try intern_from_file f with Sys_error s -> error s in - (* We check no other file containing same library is loaded *) - if library_is_loaded m.library_name then - begin - msg_warning - (pr_dirpath m.library_name ++ str " is already loaded from file " ++ - str (library_full_filename m.library_name)); - m.library_name, [] - end - else - let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in - let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in - m.library_name, needed - let native_name_from_filename f = let ch = System.with_magic_number_check raw_intern_library f in let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name -let rec_intern_library_from_file f = - (* A name is specified, we have to check it contains library id *) - let paths = Loadpath.get_paths () in - let _, f = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in - rec_intern_by_filename_only f - (**********************************************************************) (*s [require_library] loads and possibly opens a library. This is a synchronized operation. It is performed as follows: @@ -590,18 +568,6 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library_from_file file export = - let modref,needed = rec_intern_library_from_file 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_library ([modref],exp))) - export - end - else - add_anonymous_leaf (in_require (needed,[modref],export)); - add_frozen_state () - (* the function called by Vernacentries.vernac_import *) let safe_locate_module (loc,qid) = diff --git a/library/library.mli b/library/library.mli index 3d96f9a751..d5e610dd67 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,7 +22,6 @@ open Libnames (** 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_file : CUnix.physical_path -> bool option -> unit (** {6 Start the compilation of a library } *) -- cgit v1.2.3 From da4d0b0e3d82621fe8338dd313b788472fc31bb2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 10:26:08 +0200 Subject: Remove some uses of Loadpath.get_paths. The single remaining use is in library/states.ml. This use should be reviewed, as it is most certainly broken. The other uses of Loadpath.get_paths did not disappear by miracle though. They were replaced by a new function Loadpath.locate_file which factors all the uses of the function. This function should not be used as it is as broken as Loadpath.get_paths, by definition. Vernac.load_vernac now takes a complete path rather than looking up for the file. That is the way it was used most of the time, so the lookup was unnecessary. For instance, Vernac.compile was calling Library.start_library which already expected a complete path. Another consequence is that System.find_file_in_path is almost no longer used (except for Loadpath.locate_file, obviously). The two remaining uses are System.intern_state (used by States.intern_state, cf above) and Mltop.dir_ml_load for dynamically loading compiled .ml files. --- library/library.ml | 4 +--- library/loadpath.ml | 6 ++++++ library/loadpath.mli | 4 ++++ 3 files changed, 11 insertions(+), 3 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 6d7b0f603a..f5c7f63358 100644 --- a/library/library.ml +++ b/library/library.ml @@ -652,9 +652,7 @@ let start_library f = ldir let load_library_todo f = - let paths = Loadpath.get_paths () in - let _, longf = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let longf = Loadpath.locate_file (f^".v") in let f = longf^"io" in let ch = System.with_magic_number_check raw_intern_library f in let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in diff --git a/library/loadpath.ml b/library/loadpath.ml index 26af809e78..d35dca2125 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -112,3 +112,9 @@ let expand_path dir = if DirPath.equal dir lg then (ph, lg) :: aux l else aux l in aux !load_paths + +let locate_file fname = + let paths = get_paths () in + let _,longfname = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + longfname diff --git a/library/loadpath.mli b/library/loadpath.mli index 3251b8c60c..c2c689af70 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -52,3 +52,7 @@ val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list 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. *) -- cgit v1.2.3 From 82a618e8a4945752698a7900c8af7a51091f7b1b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:05:45 +0200 Subject: Prevent States.intern_state and System.extern_intern from looking up files in the loadpath. This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner. --- library/library.ml | 6 ++++-- library/states.ml | 6 +----- 2 files changed, 5 insertions(+), 7 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index f5c7f63358..0fb938e9b6 100644 --- a/library/library.ml +++ b/library/library.ml @@ -742,7 +742,8 @@ let save_library_to ?todo dir f otab = if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then error_recursively_dependent_library dir; (* Open the vo file and write the magic number *) - let (f',ch) = raw_extern_library f in + let f' = f in + let ch = raw_extern_library f' in try (* Writing vo payload *) System.marshal_out_segment f' ch (sd : seg_sum); @@ -765,7 +766,8 @@ let save_library_to ?todo dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let (f',ch) = raw_extern_library (f^"o") in + let f' = f^".o" in + let ch = raw_extern_library f' in System.marshal_out_segment f' ch (sum : seg_sum); System.marshal_out_segment f' ch (lib : seg_lib); System.marshal_out_segment f' ch (Some univs : seg_univ option); diff --git a/library/states.ml b/library/states.ml index 96a487b160..4e55f0cdc6 100644 --- a/library/states.ml +++ b/library/states.ml @@ -22,16 +22,12 @@ let unfreeze (fl,fs) = Summary.unfreeze_summaries fs let (extern_state,intern_state) = - let ensure_suffix f = CUnix.make_suffix f ".coq" in let (raw_extern, raw_intern) = extern_intern Coq_config.state_magic_number in (fun s -> - let s = ensure_suffix s in raw_extern s (freeze ~marshallable:`Yes)), (fun s -> - let s = ensure_suffix s in - let paths = Loadpath.get_paths () in - unfreeze (with_magic_number_check (raw_intern paths) s); + unfreeze (with_magic_number_check raw_intern s); Library.overwrite_library_filenames s) (* Rollback. *) -- cgit v1.2.3 From 05ab666a1283de5500dbc0520d18bdb05d95f286 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:45:27 +0200 Subject: Make the interface of System.raw_extern_intern much saner. There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures. --- library/library.ml | 16 +++++++++------- library/states.ml | 14 ++++++-------- 2 files changed, 15 insertions(+), 15 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 0fb938e9b6..6da9ccf68b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -19,10 +19,12 @@ open Lib (************************************************************************) (*s Low-level interning/externing of libraries to files *) -(*s Loading from disk to cache (preparation phase) *) +let raw_extern_library f = + System.raw_extern_state Coq_config.vo_magic_number f -let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern Coq_config.vo_magic_number +let raw_intern_library f = + System.with_magic_number_check + (System.raw_intern_state Coq_config.vo_magic_number) f (************************************************************************) (** Serialized objects loaded on-the-fly *) @@ -56,7 +58,7 @@ let in_delayed f ch = 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 ch = raw_intern_library f in let () = seek_in ch pos in let obj, _, digest' = System.marshal_in_segment f ch in let () = close_in ch in @@ -434,7 +436,7 @@ let mk_summary m = { } let intern_from_file f = - let ch = System.with_magic_number_check raw_intern_library f in + let ch = raw_intern_library f in let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in let (lmd : seg_lib delayed) = in_delayed f ch in let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in @@ -489,7 +491,7 @@ let rec_intern_library libs mref = libs let native_name_from_filename f = - let ch = System.with_magic_number_check raw_intern_library f in + let ch = raw_intern_library f in let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name @@ -654,7 +656,7 @@ let start_library f = let load_library_todo f = let longf = Loadpath.locate_file (f^".v") in let f = longf^"io" in - let ch = System.with_magic_number_check raw_intern_library f in + let ch = raw_intern_library f in let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in diff --git a/library/states.ml b/library/states.ml index 4e55f0cdc6..3cb6da12ec 100644 --- a/library/states.ml +++ b/library/states.ml @@ -21,14 +21,12 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let (extern_state,intern_state) = - let (raw_extern, raw_intern) = - extern_intern Coq_config.state_magic_number in - (fun s -> - raw_extern s (freeze ~marshallable:`Yes)), - (fun s -> - unfreeze (with_magic_number_check raw_intern s); - Library.overwrite_library_filenames s) +let extern_state s = + System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes) + +let intern_state s = + unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); + Library.overwrite_library_filenames s (* Rollback. *) -- cgit v1.2.3 From 99918c8a8cfb4285798a70351673be2679a6e819 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 21:27:26 +0200 Subject: Fix dumb typo. --- library/library.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 6da9ccf68b..024ac9e6fa 100644 --- a/library/library.ml +++ b/library/library.ml @@ -768,7 +768,7 @@ let save_library_to ?todo dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let f' = f^".o" in + let f' = f^"o" in let ch = raw_extern_library f' in System.marshal_out_segment f' ch (sum : seg_sum); System.marshal_out_segment f' ch (lib : seg_lib); -- cgit v1.2.3 From b248c23b84a96ef692e4a3ded6668733820e1a77 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 30 Sep 2015 06:52:01 +0200 Subject: Unexport Loadpath.get_paths. --- library/loadpath.ml | 4 +--- library/loadpath.mli | 3 --- 2 files changed, 1 insertion(+), 6 deletions(-) (limited to 'library') diff --git a/library/loadpath.ml b/library/loadpath.ml index d35dca2125..622d390a2c 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -28,8 +28,6 @@ let physical p = p.path_physical let get_load_paths () = !load_paths -let get_paths () = List.map physical !load_paths - let anomaly_too_many_paths path = anomaly (str "Several logical paths are associated to" ++ spc () ++ str path) @@ -114,7 +112,7 @@ let expand_path dir = aux !load_paths let locate_file fname = - let paths = get_paths () in + let paths = List.map physical !load_paths in let _,longfname = System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in longfname diff --git a/library/loadpath.mli b/library/loadpath.mli index c2c689af70..269e28e0b5 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -27,9 +27,6 @@ val logical : t -> DirPath.t val get_load_paths : unit -> t list (** Get the current loadpath association. *) -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 -> DirPath.t -> implicit:bool -> unit (** [add_load_path phys log type] adds the binding [phys := log] to the current loadpaths. *) -- cgit v1.2.3 From e759333a8b5c11247c4cc134fdde8c1bd85a6e17 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 11 Sep 2015 18:07:39 +0200 Subject: Universes: enforce Set <= i for all Type occurrences. --- library/universes.ml | 41 ++++++++++++++++++++++++++++------------- 1 file changed, 28 insertions(+), 13 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 1c8a5ad77d..c67371e3be 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -182,10 +182,13 @@ let leq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, ULe, u2) !cstrs; - true) + if Univ.check_leq univs u1 u2 then + ((if Univ.is_small_univ u1 then + cstrs := Constraints.add (u1, ULe, u2) !cstrs); + true) + else + (cstrs := Constraints.add (u1, ULe, u2) !cstrs; + true) in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -820,10 +823,18 @@ let minimize_univ_variables ctx us algs left right cstrs = if v == None then fst (aux acc u) else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) us (ctx, us, algs, lbounds, cstrs) - + let normalize_context_set ctx us algs = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in let uf = UF.create () in + (** Keep the Prop/Set <= i constraints separate for minimization *) + let smallles, csts = + Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> + if d == Le && Univ.Level.is_small l then + (Constraint.add cstr smallles, noneqs) + else (smallles, Constraint.add cstr noneqs)) + csts (Constraint.empty, Constraint.empty) + in let csts = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) @@ -831,11 +842,15 @@ let normalize_context_set ctx us algs = Univ.constraints_of_universes g in let noneqs = - Constraint.fold (fun (l,d,r) noneqs -> - if d == Eq then (UF.union l r uf; noneqs) - else Constraint.add (l,d,r) noneqs) - csts Constraint.empty + Constraint.fold (fun (l,d,r as cstr) noneqs -> + if d == Eq then (UF.union l r uf; noneqs) + else (* We ignore the trivial Prop/Set <= i constraints. *) + if d == Le && Univ.Level.is_small l then + noneqs + else Constraint.add cstr noneqs) + csts Constraint.empty in + let noneqs = Constraint.union noneqs smallles in let partition = UF.partition uf in let flex x = LMap.mem x us in let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> @@ -941,12 +956,12 @@ let simplify_universe_context (univs,csts) = let csts' = subst_univs_level_constraints subst csts' in (univs', csts'), subst -let is_small_leq (l,d,r) = - Level.is_small l && d == Univ.Le +let is_trivial_leq (l,d,r) = + Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) (* Prop < i <-> Set+1 <= i <-> Set < i *) let translate_cstr (l,d,r as cstr) = - if Level.equal Level.prop l && d == Univ.Lt then + if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then (Level.set, d, r) else cstr @@ -954,7 +969,7 @@ let refresh_constraints univs (ctx, cstrs) = let cstrs', univs' = Univ.Constraint.fold (fun c (cstrs', univs as acc) -> let c = translate_cstr c in - if Univ.check_constraint univs c && not (is_small_leq c) then acc + if is_trivial_leq c then acc else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs)) cstrs (Univ.Constraint.empty, univs) in ((ctx, cstrs'), univs') -- cgit v1.2.3 From 4838a3a3c25cc9f7583dd62e4585460aca8ee961 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 21 Sep 2015 11:55:32 +0200 Subject: Forcing i > Set for global universes (incomplete) --- library/universes.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index c67371e3be..0544585dce 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -830,8 +830,13 @@ let normalize_context_set ctx us algs = (** Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> - if d == Le && Univ.Level.is_small l then - (Constraint.add cstr smallles, noneqs) + if d == Le then + if Univ.Level.is_small l then + (Constraint.add cstr smallles, noneqs) + else if Level.is_small r then + raise (Univ.UniverseInconsistency + (Le,Universe.make l,Universe.make r,None)) + else (smallles, Constraint.add cstr noneqs) else (smallles, Constraint.add cstr noneqs)) csts (Constraint.empty, Constraint.empty) in -- cgit v1.2.3 From 26628315688e07c43b9881872a737454e93fe4c9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:11:56 +0200 Subject: Univs: minimization, adapt to graph invariants. We are forced to declare universes that are global and appear in the local constraints as we start from an empty universe graph. --- library/universes.ml | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 0544585dce..0133f5deb6 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -843,7 +843,25 @@ let normalize_context_set ctx us algs = let csts = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = Univ.merge_constraints csts Univ.empty_universes in + let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g) + ctx Univ.empty_universes + in + let g = + Univ.Constraint.fold (fun (l, d, r) g -> + let g = + if not (Level.is_small l || LSet.mem l ctx) then + try Univ.add_universe l true g + with Univ.AlreadyDeclared -> g + else g + in + let g = + if not (Level.is_small r || LSet.mem r ctx) then + try Univ.add_universe r true g + with Univ.AlreadyDeclared -> g + else g + in g) csts g + in + let g = Univ.Constraint.fold Univ.enforce_constraint csts g in Univ.constraints_of_universes g in let noneqs = @@ -852,6 +870,8 @@ let normalize_context_set ctx us algs = else (* We ignore the trivial Prop/Set <= i constraints. *) if d == Le && Univ.Level.is_small l then noneqs + else if Level.is_small l && d == Lt && not (LSet.mem r ctx) then + noneqs else Constraint.add cstr noneqs) csts Constraint.empty in -- cgit v1.2.3 From 43858a207437fa08f066bdd3cae7bcd3034808f1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 19:14:05 +0200 Subject: Univs: fix Universe vernacular, fix bug #4287. No universe can be set lower than Prop anymore (or Set). --- library/declare.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 8438380c9c..8908a2c919 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -455,12 +455,14 @@ let input_universes : universe_names -> Libobject.obj = let do_universe l = let glob = Universes.global_universe_names () in - let glob' = - List.fold_left (fun (idl,lid) (l, id) -> + let glob', ctx = + List.fold_left (fun ((idl,lid),ctx) (l, id) -> let lev = Universes.new_univ_level (Global.current_dirpath ()) in - (Idmap.add id lev idl, Univ.LMap.add lev id lid)) - glob l + ((Idmap.add id lev idl, Univ.LMap.add lev id lid), + Univ.ContextSet.add_universe lev ctx)) + (glob, Univ.ContextSet.empty) l in + Global.push_context_set ctx; Lib.add_anonymous_leaf (input_universes glob') -- cgit v1.2.3 From 62e6f7e37512e523eafe65e6a58369361e74d4d5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 30 Sep 2015 18:32:23 +0200 Subject: Univs: fix minimization to allow lowering a universe to Set, not Prop. --- library/universes.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 0133f5deb6..9bc21b0e55 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -834,8 +834,10 @@ let normalize_context_set ctx us algs = if Univ.Level.is_small l then (Constraint.add cstr smallles, noneqs) else if Level.is_small r then - raise (Univ.UniverseInconsistency - (Le,Universe.make l,Universe.make r,None)) + if Level.is_prop r then + raise (Univ.UniverseInconsistency + (Le,Universe.make l,Universe.make r,None)) + else (smallles, Constraint.add (l,Eq,r) noneqs) else (smallles, Constraint.add cstr noneqs) else (smallles, Constraint.add cstr noneqs)) csts (Constraint.empty, Constraint.empty) @@ -850,13 +852,13 @@ let normalize_context_set ctx us algs = Univ.Constraint.fold (fun (l, d, r) g -> let g = if not (Level.is_small l || LSet.mem l ctx) then - try Univ.add_universe l true g + try Univ.add_universe l false g with Univ.AlreadyDeclared -> g else g in let g = if not (Level.is_small r || LSet.mem r ctx) then - try Univ.add_universe r true g + try Univ.add_universe r false g with Univ.AlreadyDeclared -> g else g in g) csts g -- cgit v1.2.3 From 4585baa53e7fa4c25e304b8136944748a7622e10 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 18:42:38 +0200 Subject: Univs: refined handling of assumptions According to their polymorphic/non-polymorphic status, which imply that universe variables introduced with it are assumed to be >= or > Set respectively in the following definitions. --- library/declare.ml | 11 ++++++----- library/global.ml | 6 +++--- library/global.mli | 6 +++--- library/lib.ml | 1 + library/universes.ml | 32 +++++++++++++++----------------- 5 files changed, 28 insertions(+), 28 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 8908a2c919..ec0e1047e7 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -42,7 +42,7 @@ type variable_declaration = DirPath.t * section_variable_entry * logical_kind let cache_variable ((sp,_),o) = match o with - | Inl ctx -> Global.push_context_set ctx + | Inl ctx -> Global.push_context_set false ctx | Inr (id,(p,d,mk)) -> (* Constr raisonne sur les noms courts *) if variable_exists id then @@ -50,7 +50,7 @@ let cache_variable ((sp,_),o) = let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ((id,ty),ctx) in + let () = Global.push_named_assum ((id,ty,poly),ctx) in let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> @@ -116,8 +116,9 @@ let open_constant i ((sp,kn), obj) = match (Global.lookup_constant con).const_body with | (Def _ | Undef _) -> () | OpaqueDef lc -> - match Opaqueproof.get_constraints (Global.opaque_tables ())lc with - | Some f when Future.is_val f -> Global.push_context_set (Future.force f) + match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with + | Some f when Future.is_val f -> + Global.push_context_set false (Future.force f) | _ -> () let exists_name id = @@ -462,7 +463,7 @@ let do_universe l = Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in - Global.push_context_set ctx; + Global.push_context_set false ctx; Lib.add_anonymous_leaf (input_universes glob') diff --git a/library/global.ml b/library/global.ml index 0419799b67..382abb8467 100644 --- a/library/global.ml +++ b/library/global.ml @@ -80,8 +80,8 @@ let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) let push_named_def d = globalize0 (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) -let push_context_set c = globalize0 (Safe_typing.push_context_set c) -let push_context c = globalize0 (Safe_typing.push_context c) +let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) +let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) @@ -249,7 +249,7 @@ let current_dirpath () = let with_global f = let (a, ctx) = f (env ()) (current_dirpath ()) in - push_context_set ctx; a + push_context_set false ctx; a (* spiwack: register/unregister functions for retroknowledge *) let register field value by_clause = diff --git a/library/global.mli b/library/global.mli index 363bb57890..e6b5c1cbab 100644 --- a/library/global.mli +++ b/library/global.mli @@ -30,7 +30,7 @@ val set_engagement : Declarations.engagement -> unit (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit +val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit val push_named_def : (Id.t * Entries.definition_entry) -> unit val add_constant : @@ -41,8 +41,8 @@ val add_mind : (** Extra universe constraints *) val add_constraints : Univ.constraints -> unit -val push_context : Univ.universe_context -> unit -val push_context_set : Univ.universe_context_set -> unit +val push_context : bool -> Univ.universe_context -> unit +val push_context_set : bool -> Univ.universe_context_set -> unit (** Non-interactive modules and module types *) diff --git a/library/lib.ml b/library/lib.ml index 81db547efd..f4f52db53b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -420,6 +420,7 @@ let extract_hyps (secs,ohyps) = in aux (secs,ohyps) let instance_from_variable_context sign = + let rec inst_rec = function | (id,b,None,_) :: sign -> id :: inst_rec sign | _ :: sign -> inst_rec sign diff --git a/library/universes.ml b/library/universes.ml index 9bc21b0e55..bc42cc044c 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -849,19 +849,20 @@ let normalize_context_set ctx us algs = ctx Univ.empty_universes in let g = - Univ.Constraint.fold (fun (l, d, r) g -> - let g = - if not (Level.is_small l || LSet.mem l ctx) then - try Univ.add_universe l false g - with Univ.AlreadyDeclared -> g - else g - in - let g = - if not (Level.is_small r || LSet.mem r ctx) then - try Univ.add_universe r false g - with Univ.AlreadyDeclared -> g - else g - in g) csts g + Univ.Constraint.fold + (fun (l, d, r) g -> + let g = + if not (Level.is_small l || LSet.mem l ctx) then + try Univ.add_universe l false g + with Univ.AlreadyDeclared -> g + else g + in + let g = + if not (Level.is_small r || LSet.mem r ctx) then + try Univ.add_universe r false g + with Univ.AlreadyDeclared -> g + else g + in g) csts g in let g = Univ.Constraint.fold Univ.enforce_constraint csts g in Univ.constraints_of_universes g @@ -870,10 +871,7 @@ let normalize_context_set ctx us algs = Constraint.fold (fun (l,d,r as cstr) noneqs -> if d == Eq then (UF.union l r uf; noneqs) else (* We ignore the trivial Prop/Set <= i constraints. *) - if d == Le && Univ.Level.is_small l then - noneqs - else if Level.is_small l && d == Lt && not (LSet.mem r ctx) then - noneqs + if d == Le && Univ.Level.is_small l then noneqs else Constraint.add cstr noneqs) csts Constraint.empty in -- cgit v1.2.3 From 8860362de4a26286b0cb20cf4e02edc5209bdbd1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 23:35:51 +0200 Subject: Univs: Change intf of push_named_def to return the computed universe context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time. --- library/declare.ml | 6 +++--- library/global.ml | 2 +- library/global.mli | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index ec0e1047e7..16803b3bfa 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -54,9 +54,9 @@ let cache_variable ((sp,_),o) = let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let () = Global.push_named_def (id,de) in - Explicit, de.const_entry_opaque, de.const_entry_polymorphic, - (Univ.ContextSet.of_context de.const_entry_universes) in + let univs = Global.push_named_def (id,de) in + Explicit, de.const_entry_opaque, + de.const_entry_polymorphic, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; diff --git a/library/global.ml b/library/global.ml index 382abb8467..6002382c1f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -78,7 +78,7 @@ let globalize_with_summary fs f = let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) -let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let push_named_def d = globalize (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let push_context b c = globalize0 (Safe_typing.push_context b c) diff --git a/library/global.mli b/library/global.mli index e6b5c1cbab..ac231f7fd8 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,7 +31,7 @@ val set_engagement : Declarations.engagement -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> unit +val push_named_def : (Id.t * Entries.definition_entry) -> Univ.universe_context_set val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant -- cgit v1.2.3 From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- library/global.mli | 2 +- library/universes.ml | 34 +++++++++++++++++----------------- library/universes.mli | 10 +++++----- 3 files changed, 23 insertions(+), 23 deletions(-) (limited to 'library') diff --git a/library/global.mli b/library/global.mli index ac231f7fd8..455751d416 100644 --- a/library/global.mli +++ b/library/global.mli @@ -19,7 +19,7 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool -val universes : unit -> Univ.universes +val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Context.named_context diff --git a/library/universes.ml b/library/universes.ml index bc42cc044c..067558c8a6 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -113,7 +113,7 @@ let to_constraints g s = | _, ULe, Some l' -> enforce_leq x y acc | _, ULub, _ -> acc | _, d, _ -> - let f = if d == ULe then check_leq else check_eq in + let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in if f g x y then acc else raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes") @@ -123,12 +123,12 @@ let eq_constr_univs_infer univs m n = if m == n then true, Constraints.empty else let cstrs = ref Constraints.empty in - let eq_universes strict = Univ.Instance.check_eq univs in + let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true + if UGraph.check_eq univs u1 u2 then true else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; true) @@ -149,12 +149,12 @@ let eq_constr_univs_infer_with kind1 kind2 univs m n = [kind1,kind2], because [kind1] and [kind2] may be different, typically evaluating [m] and [n] in different evar maps. *) let cstrs = ref Constraints.empty in - let eq_universes strict = Univ.Instance.check_eq univs in + let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true + if UGraph.check_eq univs u1 u2 then true else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; true) @@ -169,12 +169,12 @@ let leq_constr_univs_infer univs m n = if m == n then true, Constraints.empty else let cstrs = ref Constraints.empty in - let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in + let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true + if UGraph.check_eq univs u1 u2 then true else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; true) in @@ -182,7 +182,7 @@ let leq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then + if UGraph.check_leq univs u1 u2 then ((if Univ.is_small_univ u1 then cstrs := Constraints.add (u1, ULe, u2) !cstrs); true) @@ -845,27 +845,27 @@ let normalize_context_set ctx us algs = let csts = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g) - ctx Univ.empty_universes + let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) + ctx UGraph.empty_universes in let g = Univ.Constraint.fold (fun (l, d, r) g -> let g = if not (Level.is_small l || LSet.mem l ctx) then - try Univ.add_universe l false g - with Univ.AlreadyDeclared -> g + try UGraph.add_universe l false g + with UGraph.AlreadyDeclared -> g else g in let g = if not (Level.is_small r || LSet.mem r ctx) then - try Univ.add_universe r false g - with Univ.AlreadyDeclared -> g + try UGraph.add_universe r false g + with UGraph.AlreadyDeclared -> g else g in g) csts g in - let g = Univ.Constraint.fold Univ.enforce_constraint csts g in - Univ.constraints_of_universes g + let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in + UGraph.constraints_of_universes g in let noneqs = Constraint.fold (fun (l,d,r as cstr) noneqs -> @@ -995,7 +995,7 @@ let refresh_constraints univs (ctx, cstrs) = Univ.Constraint.fold (fun c (cstrs', univs as acc) -> let c = translate_cstr c in if is_trivial_leq c then acc - else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs)) + else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs)) cstrs (Univ.Constraint.empty, univs) in ((ctx, cstrs'), univs') diff --git a/library/universes.mli b/library/universes.mli index 5527da0903..c897a88a90 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -60,11 +60,11 @@ val subst_univs_universe_constraints : universe_subst_fn -> val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function -val to_constraints : universes -> universe_constraints -> constraints +val to_constraints : UGraph.t -> universe_constraints -> constraints (** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) -val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained +val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool universe_constrained (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose @@ -72,12 +72,12 @@ val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_ val eq_constr_univs_infer_with : (constr -> (constr,types) kind_of_term) -> (constr -> (constr,types) kind_of_term) -> - Univ.universes -> constr -> constr -> bool universe_constrained + UGraph.t -> constr -> constr -> bool universe_constrained (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) -val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained +val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool universe_constrained (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) @@ -212,7 +212,7 @@ val restrict_universe_context : universe_context_set -> universe_set -> universe val simplify_universe_context : universe_context_set -> universe_context_set * universe_level_subst -val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes +val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t (** Pretty-printing *) -- cgit v1.2.3 From ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Oct 2015 14:11:19 +0200 Subject: Goptions: new value type: optional string These options can be set to a string value, but also unset. Internal data is of type string option. --- library/goptions.ml | 9 +++++++++ library/goptions.mli | 2 ++ 2 files changed, 11 insertions(+) (limited to 'library') diff --git a/library/goptions.ml b/library/goptions.ml index 4f50fbfbdd..30d195f83c 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -20,6 +20,7 @@ type option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option (** Summary of an option status *) type option_state = { @@ -293,6 +294,10 @@ let declare_string_option = declare_option (fun v -> StringValue v) (function StringValue v -> v | _ -> anomaly (Pp.str "async_option")) +let declare_stringopt_option = + declare_option + (fun v -> StringOptValue v) + (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option")) (* 3- User accessible commands *) @@ -324,11 +329,13 @@ let check_bool_value v = function let check_string_value v = function | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) | _ -> bad_type_error () let check_unset_value v = function | BoolValue _ -> BoolValue false | IntValue _ -> IntValue None + | StringOptValue _ -> StringOptValue None | _ -> bad_type_error () (* Nota: For compatibility reasons, some errors are treated as @@ -359,6 +366,8 @@ let msg_option_value (name,v) = | IntValue (Some n) -> int n | IntValue None -> str "undefined" | StringValue s -> str s + | StringOptValue None -> str"undefined" + | StringOptValue (Some s) -> str s (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = diff --git a/library/goptions.mli b/library/goptions.mli index 1c44f89081..9d87c14c50 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -128,6 +128,7 @@ type 'a write_function = 'a -> unit val declare_int_option : int option option_sig -> int option write_function val declare_bool_option : bool option_sig -> bool write_function val declare_string_option: string option_sig -> string write_function +val declare_stringopt_option: string option option_sig -> string option write_function (** {6 Special functions supposed to be used only in vernacentries.ml } *) @@ -165,6 +166,7 @@ type option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option (** Summary of an option status *) type option_state = { -- cgit v1.2.3 From b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 8 Oct 2015 16:00:06 +0200 Subject: Univs: fix bug #3807 Add a flag to disallow minimization to set --- library/universes.ml | 11 ++++++++++- library/universes.mli | 3 +++ 2 files changed, 13 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index bc42cc044c..0656188eb5 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -26,6 +26,11 @@ let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd !global_universes)) with Not_found -> Level.pr l +(* To disallow minimization to Set *) + +let set_minimization = ref true +let is_set_minimization () = !set_minimization + type universe_constraint_type = ULe | UEq | ULub type universe_constraint = universe * universe_constraint_type * universe @@ -832,7 +837,9 @@ let normalize_context_set ctx us algs = Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> if d == Le then if Univ.Level.is_small l then - (Constraint.add cstr smallles, noneqs) + if is_set_minimization () then + (Constraint.add cstr smallles, noneqs) + else (smallles, noneqs) else if Level.is_small r then if Level.is_prop r then raise (Univ.UniverseInconsistency @@ -872,6 +879,8 @@ let normalize_context_set ctx us algs = if d == Eq then (UF.union l r uf; noneqs) else (* We ignore the trivial Prop/Set <= i constraints. *) if d == Le && Univ.Level.is_small l then noneqs + else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r + then noneqs else Constraint.add cstr noneqs) csts Constraint.empty in diff --git a/library/universes.mli b/library/universes.mli index 5527da0903..4ff21d45c9 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -12,6 +12,9 @@ open Term open Environ open Univ +val set_minimization : bool ref +val is_set_minimization : unit -> bool + (** Universes *) type universe_names = -- cgit v1.2.3 From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- library/impargs.ml | 2 +- library/impargs.mli | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'library') diff --git a/library/impargs.ml b/library/impargs.ml index 94f53219e7..d15a02fea2 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -104,7 +104,7 @@ let set_maximality imps b = inferable following a rigid path (useful to know how to print a partial application) -- [Manual] means the argument has been explicitely set as implicit. +- [Manual] means the argument has been explicitly set as implicit. We also consider arguments inferable from the conclusion but it is operational only if [conclusion_matters] is true. diff --git a/library/impargs.mli b/library/impargs.mli index 1d3a73e94c..30f2e30f97 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -59,8 +59,8 @@ type implicit_explanation = inferable following a rigid path (useful to know how to print a partial application) *) | Manual - (** means the argument has been explicitely set as implicit. *) - + (** means the argument has been explicitly set as implicit. *) + (** We also consider arguments inferable from the conclusion but it is operational only if [conclusion_matters] is true. *) -- cgit v1.2.3 From 6417a9e72feb39b87f0b456186100b11d1c87d5f Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 25 Oct 2015 16:40:32 +0100 Subject: Declaremods: replace two anomalies by user errors (fix #3974 and #3975) As shown by the code snippets in these bug reports, I've been too hasty in considering these situations as anomalies in commit 466c4cb (at least the one at the last line of consistency_checks). So let's turn these anomalies back to regular user errors, as they were before this commit. --- library/declaremods.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index f66656d09a..7f607a51c9 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -166,12 +166,14 @@ let consistency_checks exists dir dirinfo = let globref = try Nametab.locate_dir (qualid_of_dirpath dir) with Not_found -> - anomaly (pr_dirpath dir ++ str " should already exist!") + errorlabstrm "consistency_checks" + (pr_dirpath dir ++ str " should already exist!") in assert (eq_global_dir_reference globref dirinfo) else if Nametab.exists_dir dir then - anomaly (pr_dirpath dir ++ str " already exists") + errorlabstrm "consistency_checks" + (pr_dirpath dir ++ str " already exists") let compute_visibility exists i = if exists then Nametab.Exactly i else Nametab.Until i -- cgit v1.2.3 From ed7af646f2e486b7e96812ba2335e644756b70fd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 27 Oct 2015 13:55:45 -0400 Subject: Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names structure. --- library/declare.ml | 93 +++++++++++++++++++++++++++++++--------------------- library/declare.mli | 4 +-- library/lib.ml | 39 +++++++++++++++------- library/lib.mli | 2 +- library/universes.ml | 3 +- 5 files changed, 87 insertions(+), 54 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 16803b3bfa..0004f45a29 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -27,7 +27,7 @@ open Decls open Decl_kinds (** flag for internal message display *) -type internal_flag = +type internal_flag = | UserAutomaticRequest (* kernel action, a message is displayed *) | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) @@ -63,7 +63,7 @@ let cache_variable ((sp,_),o) = add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with - | Inr (id,_) -> + | Inr (id,_) -> if variable_polymorphic id then None else Some (Inl (variable_context id)) | Inl _ -> Some o @@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) = Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = +let dummy_constant_entry = ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { @@ -185,7 +185,7 @@ let declare_constant_common id cst = Notation.declare_ref_arguments_scope (ConstRef c); c -let definition_entry ?(opaque=false) ?(inline=false) ?types +let definition_entry ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body = { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; @@ -212,11 +212,11 @@ let declare_sideff env fix_exn se = in let ty_of cb = match cb.Declarations.const_type with - | Declarations.RegularArity t -> Some t + | Declarations.RegularArity t -> Some t | Declarations.TemplateArity _ -> None in let cst_of cb pt = let pt, opaque = pt_opaque_of cb pt in - let univs, subst = + let univs, subst = if cb.const_polymorphic then let univs = Univ.instantiate_univ_context cb.const_universes in univs, Vars.subst_instance_constr (Univ.UContext.instance univs) @@ -240,7 +240,7 @@ let declare_sideff env fix_exn se = } in let exists c = try ignore(Environ.lookup_constant c env); true - with Not_found -> false in + with Not_found -> false in let knl = CList.map_filter (fun (c,cb,pt) -> if exists c then None @@ -287,7 +287,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = - let cb = + let cb = definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in declare_constant ~internal ~local id @@ -383,12 +383,12 @@ let inInductive : inductive_obj -> obj = let declare_projections mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in match spec.mind_record with - | Some (Some (_, kns, pjs)) -> - Array.iteri (fun i kn -> + | Some (Some (_, kns, pjs)) -> + Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in let kn' = declare_constant id (ProjectionEntry entry, - IsDefinition StructureComponent) + IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns; true | Some None | None -> false @@ -442,52 +442,69 @@ let assumption_message id = (** Global universe names, in a different summary *) -type universe_names = +type universe_names = (Univ.universe_level Idmap.t * Id.t Univ.LMap.t) -let input_universes : universe_names -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Global universe name state") with - cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi); - load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi); - discharge_function = (fun (_, a) -> Some a); - classify_function = (fun a -> Keep a) } +(* Discharged or not *) +type universe_decl = polymorphic * (Id.t * Univ.universe_level) list -let do_universe l = +let cache_universes (p, l) = let glob = Universes.global_universe_names () in - let glob', ctx = - List.fold_left (fun ((idl,lid),ctx) (l, id) -> - let lev = Universes.new_univ_level (Global.current_dirpath ()) in - ((Idmap.add id lev idl, Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) + let glob', ctx = + List.fold_left (fun ((idl,lid),ctx) (id, lev) -> + ((Idmap.add id lev idl, Univ.LMap.add lev id lid), + Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in Global.push_context_set false ctx; - Lib.add_anonymous_leaf (input_universes glob') + if p then Lib.add_section_context ctx; + Universes.set_global_universe_names glob' + +let input_universes : universe_decl -> Libobject.obj = + declare_object + { (default_object "Global universe name state") with + cache_function = (fun (na, pi) -> cache_universes pi); + load_function = (fun _ (_, pi) -> cache_universes pi); + discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); + classify_function = (fun a -> Keep a) } + +let do_universe poly l = + let l = + List.map (fun (l, id) -> + let lev = Universes.new_univ_level (Global.current_dirpath ()) in + (id, lev)) l + in + Lib.add_anonymous_leaf (input_universes (poly, l)) + +type constraint_decl = polymorphic * Univ.constraints + +let cache_constraints (na, (p, c)) = + Global.add_constraints c; + if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty) +let discharge_constraints (_, (p, c as a)) = + if p then None else Some a -let input_constraints : Univ.constraints -> Libobject.obj = - let open Libobject in +let input_constraints : constraint_decl -> Libobject.obj = + let open Libobject in declare_object { (default_object "Global universe constraints") with - cache_function = (fun (na, c) -> Global.add_constraints c); - load_function = (fun _ (_, c) -> Global.add_constraints c); - discharge_function = (fun (_, a) -> Some a); + cache_function = cache_constraints; + load_function = (fun _ -> cache_constraints); + discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let do_constraint l = - let u_of_id = +let do_constraint poly l = + let u_of_id = let names, _ = Universes.global_universe_names () in - fun (loc, id) -> + fun (loc, id) -> try Idmap.find id names with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) in let constraints = List.fold_left (fun acc (l, d, r) -> let lu = u_of_id l and ru = u_of_id r in Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints constraints) - + Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/declare.mli b/library/declare.mli index 76538a6248..7ed451c3f1 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -85,5 +85,5 @@ val exists_name : Id.t -> bool (** Global universe names and constraints *) -val do_universe : Id.t Loc.located list -> unit -val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_universe : polymorphic -> Id.t Loc.located list -> unit +val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit diff --git a/library/lib.ml b/library/lib.ml index f4f52db53b..cdc8889037 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -392,10 +392,13 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t +type secentry = + | Variable of (Names.Id.t * Decl_kinds.binding_kind * + Decl_kinds.polymorphic * Univ.universe_context_set) + | Context of Univ.universe_context_set + let sectab = - Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * - Decl_kinds.polymorphic * Univ.universe_context_set) list * - Opaqueproof.work_list * abstr_list) list) + Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list) ~name:"section-context" let add_section () = @@ -406,21 +409,29 @@ let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + +let add_section_context ctx = + match !sectab with + | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) + | (vars,repl,abs)::sl -> + sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = let rec aux = function - | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> let l, r = aux (idl,hyps) in (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r - | ((_,_,poly,ctx)::idl,hyps) -> + | (Variable (_,_,poly,ctx)::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r ctx else r + | (Context ctx :: idl, hyps) -> + let l, r = aux (idl, hyps) in + l, Univ.ContextSet.union r ctx | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) let instance_from_variable_context sign = - let rec inst_rec = function | (id,b,None,_) :: sign -> id :: inst_rec sign | _ :: sign -> inst_rec sign @@ -437,7 +448,8 @@ let add_section_replacement f g hyps = let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl + sectab := (vars,f (Univ.UContext.instance ctx,args) exps, + g (sechyps,subst,ctx) abs)::sl let add_section_kn kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in @@ -457,10 +469,13 @@ let section_segment_of_mutual_inductive kn = let section_instance = function | VarRef id -> - if List.exists (fun (id',_,_,_) -> Names.id_eq id id') - (pi1 (List.hd !sectab)) - then Univ.Instance.empty, [||] - else raise Not_found + let eq = function + | Variable (id',_,_,_) -> Names.id_eq id id' + | Context _ -> false + in + if List.exists eq (pi1 (List.hd !sectab)) + then Univ.Instance.empty, [||] + else raise Not_found | ConstRef con -> Names.Cmap.find con (fst (pi2 (List.hd !sectab))) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> diff --git a/library/lib.mli b/library/lib.mli index 9c4d26c5b2..b67b2b873f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -172,7 +172,7 @@ val section_instance : Globnames.global_reference -> Univ.universe_instance * Na val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit - +val add_section_context : Univ.universe_context_set -> unit val add_section_constant : bool (* is_projection *) -> Names.constant -> Context.named_context -> unit val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit diff --git a/library/universes.ml b/library/universes.ml index 0656188eb5..30d38eb2a4 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -16,7 +16,8 @@ open Univ type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t -let global_universes = Summary.ref ~name:"Global universe names" +let global_universes = + Summary.ref ~name:"Global universe names" ((Idmap.empty, Univ.LMap.empty) : universe_names) let global_universe_names () = !global_universes -- cgit v1.2.3 From 0a1b046d37761fe47435d5041bb5031e3f7d6613 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 10:03:17 +0100 Subject: lib_stack: API to reorder the libstack For discharging it is important that constants occur in the libstack in an order that respects the dependencies among them. This is impossible to achieve for private constants when they are exported globally without this (ugly IMO) api. --- library/lib.ml | 3 +++ library/lib.mli | 1 + 2 files changed, 4 insertions(+) (limited to 'library') diff --git a/library/lib.ml b/library/lib.ml index cdc8889037..297441e6e2 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -198,6 +198,9 @@ let split_lib_at_opening sp = let add_entry sp node = lib_stk := (sp,node) :: !lib_stk +let pull_to_head oname = + lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk + let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) diff --git a/library/lib.mli b/library/lib.mli index b67b2b873f..bb88317591 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -55,6 +55,7 @@ val segment_of_objects : val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : Libobject.obj -> unit +val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -- cgit v1.2.3 From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- library/declare.ml | 151 +++++++++++++++++++++------------------------------ library/declare.mli | 10 ++-- library/global.mli | 5 +- library/heads.ml | 5 +- library/libobject.ml | 3 + 5 files changed, 78 insertions(+), 96 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 0004f45a29..63e5a72245 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -35,7 +35,7 @@ type internal_flag = (** Declaration of section variables and local definitions *) type section_variable_entry = - | SectionLocalDef of definition_entry + | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -93,9 +93,13 @@ type constant_obj = { cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; + mutable cst_exported : Safe_typing.exported_private_constant list; + (* mutable: to avoid change the libobject API, since cache_function + * does not return an updated object *) + mutable cst_was_seff : bool } -type constant_declaration = constant_entry * logical_kind +type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) @@ -131,8 +135,17 @@ let check_exists sp = let cache_constant ((sp,kn), obj) = let id = basename sp in let _,dir,_ = repr_kn kn in - let () = check_exists sp in - let kn' = Global.add_constant dir id obj.cst_decl in + let kn' = + if obj.cst_was_seff then begin + obj.cst_was_seff <- false; + if Global.exists_objlabel (Label.of_id (basename sp)) + then constant_of_kn kn + else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp)) + end else + let () = check_exists sp in + let kn', exported = Global.add_constant dir id obj.cst_decl in + obj.cst_exported <- exported; + kn' in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in @@ -156,20 +169,23 @@ let discharge_constant ((sp, kn), obj) = Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = - ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) +let dummy_constant_entry = + ConstantEntry + (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { cst_decl = dummy_constant_entry; cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; + cst_exported = []; + cst_was_seff = cst.cst_was_seff; } let classify_constant cst = Substitute (dummy_constant cst) -let inConstant : constant_obj -> obj = - declare_object { (default_object "CONSTANT") with +let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = + declare_object_full { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -177,16 +193,40 @@ let inConstant : constant_obj -> obj = subst_function = ident_subst_function; discharge_function = discharge_constant } +let declare_scheme = ref (fun _ _ -> assert false) +let set_declare_scheme f = declare_scheme := f + let declare_constant_common id cst = - let (sp,kn) = add_leaf id (inConstant cst) in + let update_tables c = +(* Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *) + declare_constant_implicits c; + Heads.declare_head (EvalConstRef c); + Notation.declare_ref_arguments_scope (ConstRef c) in + let o = inConstant cst in + let _, kn as oname = add_leaf id o in + List.iter (fun (c,ce,role) -> + (* handling of private_constants just exported *) + let o = inConstant { + cst_decl = ConstantEntry (false, ce); + cst_hyps = [] ; + cst_kind = IsProof Theorem; + cst_locl = false; + cst_exported = []; + cst_was_seff = true; } in + let id = Label.to_id (pi3 (Constant.repr3 c)) in + ignore(add_leaf id o); + update_tables c; + match role with + | Safe_typing.Subproof -> () + | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]) + (outConstant o).cst_exported; + pull_to_head oname; let c = Global.constant_of_delta_kn kn in - declare_constant_implicits c; - Heads.declare_head (EvalConstRef c); - Notation.declare_ref_arguments_scope (ConstRef c); + update_tables c; c let definition_entry ?(opaque=false) ?(inline=false) ?types - ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body = + ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; @@ -196,90 +236,25 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f -let declare_sideff env fix_exn se = - let cbl, scheme = match se with - | SEsubproof (c, cb, pt) -> [c, cb, pt], None - | SEscheme (cbl, k) -> - List.map (fun (_,c,cb,pt) -> c,cb,pt) cbl, Some (cbl,k) in - let id_of c = Names.Label.to_id (Names.Constant.label c) in - let pt_opaque_of cb pt = - match cb, pt with - | { const_body = Def sc }, _ -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false - | { const_body = OpaqueDef _ }, `Opaque(pt,univ) -> (pt, univ), true - | _ -> assert false - in - let ty_of cb = - match cb.Declarations.const_type with - | Declarations.RegularArity t -> Some t - | Declarations.TemplateArity _ -> None in - let cst_of cb pt = - let pt, opaque = pt_opaque_of cb pt in - let univs, subst = - if cb.const_polymorphic then - let univs = Univ.instantiate_univ_context cb.const_universes in - univs, Vars.subst_instance_constr (Univ.UContext.instance univs) - else cb.const_universes, fun x -> x - in - let pt = (subst (fst pt), snd pt) in - let ty = Option.map subst (ty_of cb) in - { cst_decl = ConstantEntry (DefinitionEntry { - const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff); - const_entry_secctx = Some cb.Declarations.const_hyps; - const_entry_type = ty; - const_entry_opaque = opaque; - const_entry_inline_code = false; - const_entry_feedback = None; - const_entry_polymorphic = cb.const_polymorphic; - const_entry_universes = univs; - }); - cst_hyps = [] ; - cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; - cst_locl = true; - } in - let exists c = - try ignore(Environ.lookup_constant c env); true - with Not_found -> false in - let knl = - CList.map_filter (fun (c,cb,pt) -> - if exists c then None - else Some (c,declare_constant_common (id_of c) (cst_of cb pt))) cbl in - match scheme with - | None -> () - | Some (inds_consts,kind) -> - !declare_scheme kind (Array.of_list - (List.map (fun (c,kn) -> - CList.find_map (fun (x,c',_,_) -> - if Constant.equal c c' then Some (x,kn) else None) inds_consts) - knl)) - let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = - let cd = (* We deal with side effects *) + let export = (* We deal with side effects *) match cd with - | Entries.DefinitionEntry de -> - if export_seff || - not de.const_entry_opaque || - de.const_entry_polymorphic then + | DefinitionEntry de when + export_seff || + not de.const_entry_opaque || + de.const_entry_polymorphic -> 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 + Safe_typing.empty_private_constants <> seff + | _ -> false in let cst = { - cst_decl = ConstantEntry cd; + cst_decl = ConstantEntry (export,cd); cst_hyps = [] ; cst_kind = kind; cst_locl = local; + cst_exported = []; + cst_was_seff = false; } in let kn = declare_constant_common id cst in kn diff --git a/library/declare.mli b/library/declare.mli index 7ed451c3f1..fdbd235614 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -22,7 +22,7 @@ open Decl_kinds (** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of definition_entry + | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -32,7 +32,7 @@ val declare_variable : variable -> variable_declaration -> object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = constant_entry * logical_kind +type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -49,8 +49,8 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> - ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects -> - constr -> definition_entry + ?poly:polymorphic -> ?univs:Univ.universe_context -> + ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry val declare_constant : ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant @@ -60,7 +60,7 @@ val declare_definition : ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant -(** Since transparent constant's side effects are globally declared, we +(** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : (string -> (inductive * constant) array -> unit) -> unit diff --git a/library/global.mli b/library/global.mli index ac231f7fd8..03469bea41 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,10 +31,11 @@ val set_engagement : Declarations.engagement -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> Univ.universe_context_set +val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant + DirPath.t -> Id.t -> Safe_typing.global_declaration -> + constant * Safe_typing.exported_private_constant list val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive diff --git a/library/heads.ml b/library/heads.ml index 5c153b0676..73d2aa053f 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -68,7 +68,10 @@ let kind_of_head env t = | None -> NotImmediatelyComputableHead) | Const (cst,_) -> (try on_subterm k l b (constant_head cst) - with Not_found -> assert false) + with Not_found -> + Errors.anomaly + Pp.(str "constant not found in kind_of_head: " ++ + str (Names.Constant.to_string cst))) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidType diff --git a/library/libobject.ml b/library/libobject.ml index 2ee57baf9c..85c830ea2c 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -108,6 +108,9 @@ let declare_object_full odecl = let declare_object odecl = try fst (declare_object_full odecl) with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) +let declare_object_full odecl = + try declare_object_full odecl + with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) -- cgit v1.2.3 From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 12:36:20 -0400 Subject: Univs: local names handling. Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. --- library/universes.ml | 16 ++++++++++++++++ library/universes.mli | 10 +++++++++- 2 files changed, 25 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 30d38eb2a4..6cccb10efb 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -12,7 +12,9 @@ open Names open Term open Environ open Univ +open Globnames +(** Global universe names *) type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t @@ -27,6 +29,20 @@ let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd !global_universes)) with Not_found -> Level.pr l +(** Local universe names of polymorphic references *) + +type universe_binders = (Id.t * Univ.universe_level) list + +let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" + +let universe_binders_of_global ref = + try + let l = Refmap.find ref !universe_binders_table in l + with Not_found -> [] + +let register_universe_binders ref l = + universe_binders_table := Refmap.add ref l !universe_binders_table + (* To disallow minimization to Set *) let set_minimization = ref true diff --git a/library/universes.mli b/library/universes.mli index 4ff21d45c9..45672ef460 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -14,9 +14,10 @@ open Univ val set_minimization : bool ref val is_set_minimization : unit -> bool - + (** Universes *) +(** Global universe name <-> level mapping *) type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t @@ -25,6 +26,13 @@ val set_global_universe_names : universe_names -> unit val pr_with_global_universes : Level.t -> Pp.std_ppcmds +(** Local universe name <-> level mapping *) + +type universe_binders = (Id.t * Univ.universe_level) list + +val register_universe_binders : Globnames.global_reference -> universe_binders -> unit +val universe_binders_of_global : Globnames.global_reference -> universe_binders + (** The global universe counter *) val set_remote_new_univ_level : universe_level RemoteCounter.installer -- cgit v1.2.3 From 48ffb1173702f86fa6cb6392f7876d7da5e5d6b6 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 29 Oct 2015 20:52:32 +0100 Subject: Make the code of compare functions linear in the number of constructors. This scheme has been advised by @gashe on #79. Interestingly there are several comparison functions in Coq which were already implemented with this scheme. --- library/globnames.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'library') diff --git a/library/globnames.ml b/library/globnames.ml index 3befaa9a94..5fdb6115ee 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -112,12 +112,12 @@ let global_ord_gen ord_cst ord_ind ord_cons x y = | ConstructRef consx, ConstructRef consy -> ord_cons consx consy | VarRef v1, VarRef v2 -> Id.compare v1 v2 - | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1 - | ConstRef _, VarRef _ -> 1 - | ConstRef _, (IndRef _ | ConstructRef _) -> -1 - | IndRef _, (VarRef _ | ConstRef _) -> 1 - | IndRef _, ConstructRef _ -> -1 - | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1 + | VarRef _, _ -> -1 + | _, VarRef _ -> 1 + | ConstRef _, _ -> -1 + | _, ConstRef _ -> 1 + | IndRef _, _ -> -1 + | _ , IndRef _ -> -1 let global_hash_gen hash_cst hash_ind hash_cons gr = let open Hashset.Combine in -- cgit v1.2.3 From 441ea07e3c8ba56b9e7d44e7802246dc06814415 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 30 Oct 2015 10:06:24 +0100 Subject: More uniformity in the style of comparison functions. --- library/globnames.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'library') diff --git a/library/globnames.ml b/library/globnames.ml index 5fdb6115ee..829e2cefcc 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -107,17 +107,16 @@ let global_eq_gen eq_cst eq_ind eq_cons x y = let global_ord_gen ord_cst ord_ind ord_cons x y = if x == y then 0 else match x, y with - | ConstRef cx, ConstRef cy -> ord_cst cx cy - | IndRef indx, IndRef indy -> ord_ind indx indy - | ConstructRef consx, ConstructRef consy -> ord_cons consx consy | VarRef v1, VarRef v2 -> Id.compare v1 v2 - | VarRef _, _ -> -1 | _, VarRef _ -> 1 + | ConstRef cx, ConstRef cy -> ord_cst cx cy | ConstRef _, _ -> -1 | _, ConstRef _ -> 1 + | IndRef indx, IndRef indy -> ord_ind indx indy | IndRef _, _ -> -1 | _ , IndRef _ -> -1 + | ConstructRef consx, ConstructRef consy -> ord_cons consx consy let global_hash_gen hash_cst hash_ind hash_cons gr = let open Hashset.Combine in -- cgit v1.2.3 From 77cf18eb844b45776b2ec67be9f71e8dd4ca002c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 30 Oct 2015 11:48:40 -0400 Subject: Add a way to get the right fix_exn in external vernacular commands involving Futures. --- library/declare.ml | 4 ++-- library/declare.mli | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 63e5a72245..5968fbf38b 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -225,9 +225,9 @@ let declare_constant_common id cst = update_tables c; c -let definition_entry ?(opaque=false) ?(inline=false) ?types +let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = - { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); + { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; const_entry_polymorphic = poly; diff --git a/library/declare.mli b/library/declare.mli index fdbd235614..c6119a58ac 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -48,7 +48,8 @@ type internal_flag = | UserIndividualRequest (* Defaut definition entries, transparent with no secctx or proj information *) -val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> +val definition_entry : ?fix_exn:Future.fix_exn -> + ?opaque:bool -> ?inline:bool -> ?types:types -> ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry -- cgit v1.2.3 From 2b47c0d1b492424c39477f9d4ec262e4d093be92 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 20 Nov 2015 20:17:35 +0100 Subject: Univs: fix type_of_global_in_context not returning instantiated universe contexts. --- library/global.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 6002382c1f..4cffd6b7e3 100644 --- a/library/global.ml +++ b/library/global.ml @@ -198,13 +198,13 @@ let type_of_global_in_context env r = | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = - if mib.mind_polymorphic then mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes else Univ.UContext.empty in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = - if mib.mind_polymorphic then mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes else Univ.UContext.empty in let inst = Univ.UContext.instance univs in -- cgit v1.2.3 From b58e8aa6525d45473f88fbea71bab88a2b46c825 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 25 Nov 2015 20:44:08 +0100 Subject: More invariants in UState. --- library/universes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 504a682fc2..225e658425 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -650,14 +650,14 @@ let normalize_univ_variable_opt_subst ectx = in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - ectx := Univ.LMap.add l (Some b) !ectx; b + try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_univ_variable_subst subst = let find l = Univ.LMap.find l !subst in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - subst := Univ.LMap.add l b !subst; b in + try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_universe_opt_subst subst = -- cgit v1.2.3 From 103ec7205d9038f1f3821f9287e3bb0907a1e3ec Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 19 Nov 2015 13:36:31 +0100 Subject: More efficient implementation of equality-up-to-universes in Universes. Instead of accumulating constraints which are not present in the original graph, we parametrize the equality function by a function actually merging those constraints in the current graph. This prevents doing the work twice. --- library/universes.ml | 53 +++++++++++++++++++++++---------------------------- library/universes.mli | 9 ++++++--- 2 files changed, 30 insertions(+), 32 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 225e658425..a157a747ca 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -102,6 +102,7 @@ module Constraints = struct end type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option type 'a universe_constrained = 'a * universe_constraints type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints @@ -141,76 +142,70 @@ let to_constraints g s = "to_constraints: non-trivial algebraic constraint between universes") in Constraints.fold tr s Constraint.empty -let eq_constr_univs_infer univs m n = - if m == n then true, Constraints.empty +let eq_constr_univs_infer univs fold m n accu = + if m == n then Some accu else - let cstrs = ref Constraints.empty in + let cstrs = ref accu in let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_eq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs + if res then Some !cstrs else None (** Variant of [eq_constr_univs_infer] taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) -let eq_constr_univs_infer_with kind1 kind2 univs m n = +let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = (* spiwack: duplicates the code of [eq_constr_univs_infer] because I haven't find a way to factor the code without destroying pointer-equality optimisations in [eq_constr_univs_infer]. Pointer equality is not sufficient to ensure equality up to [kind1,kind2], because [kind1] and [kind2] may be different, typically evaluating [m] and [n] in different evar maps. *) - let cstrs = ref Constraints.empty in + let cstrs = ref accu in let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_eq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let rec eq_constr' m n = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in - res, !cstrs + if res then Some !cstrs else None -let leq_constr_univs_infer univs m n = - if m == n then true, Constraints.empty +let leq_constr_univs_infer univs fold m n accu = + if m == n then Some accu else - let cstrs = ref Constraints.empty in + let cstrs = ref accu in let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_eq univs u1 u2 then true - else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let leq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_leq univs u1 u2 then - ((if Univ.is_small_univ u1 then - cstrs := Constraints.add (u1, ULe, u2) !cstrs); - true) - else - (cstrs := Constraints.add (u1, ULe, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -220,7 +215,7 @@ let leq_constr_univs_infer univs m n = 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 + if res then Some !cstrs else None let eq_constr_universes m n = if m == n then true, Constraints.empty diff --git a/library/universes.mli b/library/universes.mli index 285580be2d..7b17b88987 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -63,6 +63,7 @@ module Constraints : sig end type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option type 'a universe_constrained = 'a * universe_constraints type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints @@ -75,7 +76,8 @@ val to_constraints : UGraph.t -> universe_constraints -> constraints (** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) -val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool universe_constrained +val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose @@ -83,12 +85,13 @@ val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool universe_constr val eq_constr_univs_infer_with : (constr -> (constr,types) kind_of_term) -> (constr -> (constr,types) kind_of_term) -> - UGraph.t -> constr -> constr -> bool universe_constrained + UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) -val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool universe_constrained +val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) -- cgit v1.2.3 From a0e72610a71e086da392c8563c2eec2e35211afa Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 27 Nov 2015 17:21:35 +0100 Subject: Avoid recording spurious Set <= Top.i constraints which are always valid (when Top.i is global and hence > Set). --- library/universes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 6cccb10efb..1b6f7a9d57 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -854,7 +854,7 @@ let normalize_context_set ctx us algs = Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> if d == Le then if Univ.Level.is_small l then - if is_set_minimization () then + if is_set_minimization () && LSet.mem r ctx then (Constraint.add cstr smallles, noneqs) else (smallles, noneqs) else if Level.is_small r then -- cgit v1.2.3 From 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 27 Nov 2015 20:34:51 +0100 Subject: Univs: entirely disallow instantiation of polymorphic constants with Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere. --- library/declare.ml | 2 +- library/universes.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 5968fbf38b..994a6557ad 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -431,7 +431,7 @@ let cache_universes (p, l) = Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in - Global.push_context_set false ctx; + Global.push_context_set p ctx; if p then Lib.add_section_context ctx; Universes.set_global_universe_names glob' diff --git a/library/universes.ml b/library/universes.ml index 1b6f7a9d57..a8e9478e13 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -820,7 +820,7 @@ let minimize_univ_variables ctx us algs left right cstrs = let cstrs' = List.fold_left (fun cstrs (d, r) -> if d == Univ.Le then enforce_leq inst (Universe.make r) cstrs - else + else try let lev = Option.get (Universe.level inst) in Constraint.add (lev, d, r) cstrs with Option.IsNone -> failwith "") -- cgit v1.2.3 From f41968d8c240db4653d0b9fe76e1646cd7c6fb68 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 3 Dec 2015 19:08:51 +0100 Subject: Univs: fix bug #4443. Do not substitute rigid variables during minimization, keeping their equality constraints instead. --- library/universes.ml | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index a8e9478e13..3eae612c8c 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -205,7 +205,7 @@ let leq_constr_univs_infer univs m n = else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in if Univ.check_leq univs u1 u2 then - ((if Univ.is_small_univ u1 then + ((if Univ.is_type0_univ u1 then cstrs := Constraints.add (u1, ULe, u2) !cstrs); true) else @@ -904,22 +904,28 @@ let normalize_context_set ctx us algs = let noneqs = Constraint.union noneqs smallles in let partition = UF.partition uf in let flex x = LMap.mem x us in - let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> + let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> Constraint.add (canon, Univ.Eq, g) cst) global cstrs in + (* Also add equalities for rigid variables *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) rigid + cstrs + in let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in - let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in - (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs)) - (ctx, LMap.empty, Constraint.empty) partition + let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in + let canonu = Some (Universe.make canon) in + let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in + (LSet.diff ctx flexible, subst, us, cstrs)) + (ctx, LMap.empty, us, Constraint.empty) partition in (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) let noneqs = subst_univs_level_constraints subst noneqs in - let us = LMap.fold (fun u v acc -> LMap.add u (Some (Universe.make v)) acc) subst us in (* Compute the left and right set of flexible variables, constraints mentionning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = -- cgit v1.2.3 From 153d77d00ccbacf22aa5d70ca2c1cacab2749339 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Dec 2015 21:46:12 +0100 Subject: Specializing the Dyn module to each usecase. Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point. --- library/libobject.ml | 4 ++++ library/libobject.mli | 4 ++++ library/summary.ml | 4 ++++ library/summary.mli | 4 ++++ 4 files changed, 16 insertions(+) (limited to 'library') diff --git a/library/libobject.ml b/library/libobject.ml index 85c830ea2c..c638759070 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -9,6 +9,8 @@ open Libnames open Pp +module Dyn = Dyn.Make(struct end) + (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one wants to work with restricted Coq programs that have only parts of @@ -158,3 +160,5 @@ let discharge_object ((_,lobj) as node) = let rebuild_object lobj = apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj + +let dump = Dyn.dump diff --git a/library/libobject.mli b/library/libobject.mli index 099381897f..e49f3fd5c6 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -109,3 +109,7 @@ val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj val relax : bool -> unit + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/library/summary.ml b/library/summary.ml index 8e2abbf15b..6ef4e131c7 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -10,6 +10,8 @@ open Pp open Errors open Util +module Dyn = Dyn.Make(struct end) + type marshallable = [ `Yes | `No | `Shallow ] type 'a summary_declaration = { freeze_function : marshallable -> 'a; @@ -176,3 +178,5 @@ let ref ?(freeze=fun _ r -> r) ~name x = unfreeze_function = ((:=) r); init_function = (fun () -> r := x) }; r + +let dump = Dyn.dump diff --git a/library/summary.mli b/library/summary.mli index 48c9390d07..a35113fd2e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -71,3 +71,7 @@ val unfreeze_summary : frozen_bits -> unit val surgery_summary : frozen -> frozen_bits -> frozen val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits val pointer_equal : frozen_bits -> frozen_bits -> bool + +(** {6 Debug} *) + +val dump : unit -> (int * string) list -- cgit v1.2.3 From 895d34a264d9d90adfe4f0618c3bb0663dc01615 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Dec 2015 12:53:20 +0100 Subject: Leveraging GADTs to provide a better Dyn API. --- library/declaremods.ml | 2 +- library/libobject.ml | 17 ++++++++++++++--- library/libobject.mli | 1 - library/summary.ml | 22 ++++++++++++++++++++-- 4 files changed, 35 insertions(+), 7 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index 7f607a51c9..d8c5ab5e74 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -371,7 +371,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 = match idl, objs0 with | _,[] -> [] | id::idl,(id',obj)::tail when Id.equal id id' -> - assert (object_has_tag obj "MODULE"); + assert (String.equal (object_tag obj) "MODULE"); let mp_id = MPdot(mp0, Label.of_id id) in let objs = match idl with | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 diff --git a/library/libobject.ml b/library/libobject.ml index c638759070..f0d281a2dd 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,6 +8,7 @@ open Libnames open Pp +open Util module Dyn = Dyn.Make(struct end) @@ -72,15 +73,25 @@ type dynamic_object_declaration = { dyn_discharge_function : object_name * obj -> obj option; dyn_rebuild_function : obj -> obj } -let object_tag = Dyn.tag -let object_has_tag = Dyn.has_tag +let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) +let make_dyn (type a) (tag : a Dyn.tag) = + let infun x = Dyn.Dyn (tag, x) in + let outfun : (Dyn.t -> a) = fun dyn -> + let Dyn.Dyn (t, x) = dyn in + match Dyn.eq t tag with + | None -> assert false + | Some Refl -> x + in + (infun, outfun) + let declare_object_full odecl = let na = odecl.object_name in - let (infun,outfun) = Dyn.create na in + let tag = Dyn.create na in + let (infun, outfun) = make_dyn tag in let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj) and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj) and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj) diff --git a/library/libobject.mli b/library/libobject.mli index e49f3fd5c6..12b1a558f8 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -99,7 +99,6 @@ val declare_object : 'a object_declaration -> ('a -> obj) val object_tag : obj -> string -val object_has_tag : obj -> string -> bool val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit diff --git a/library/summary.ml b/library/summary.ml index 6ef4e131c7..a922e155dd 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -22,8 +22,19 @@ let summaries = ref Int.Map.empty let mangle id = id ^ "-SUMMARY" +let make_dyn (type a) (tag : a Dyn.tag) = + let infun x = Dyn.Dyn (tag, x) in + let outfun : (Dyn.t -> a) = fun dyn -> + let Dyn.Dyn (t, x) = dyn in + match Dyn.eq t tag with + | None -> assert false + | Some Refl -> x + in + (infun, outfun) + let internal_declare_summary hash sumname sdecl = - let (infun, outfun) = Dyn.create (mangle sumname) in + let tag = Dyn.create (mangle sumname) in + let (infun, outfun) = make_dyn tag in let dyn_freeze b = infun (sdecl.freeze_function b) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in @@ -166,8 +177,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids = List.filter (fun (id, _) -> List.mem id ids) summaries let pointer_equal l1 l2 = + let ptr_equal d1 d2 = + let Dyn.Dyn (t1, x1) = d1 in + let Dyn.Dyn (t2, x2) = d2 in + match Dyn.eq t1 t2 with + | None -> false + | Some Refl -> x1 == x2 + in CList.for_all2eq - (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2 + (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2 (** All-in-one reference declaration + registration *) -- cgit v1.2.3 From 9e8a9ab17d4467a4aa40f31eaef0800703d31418 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:24:18 +0100 Subject: COMMENTS: added to some variants of "Globalnames.global_reference" type. --- library/globnames.ml | 8 ++++---- library/globnames.mli | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'library') diff --git a/library/globnames.ml b/library/globnames.ml index 3befaa9a94..2d6afc8577 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -14,10 +14,10 @@ open Libnames (*s Global reference is a kernel side type for all references together *) type global_reference = - | VarRef of variable - | ConstRef of constant - | IndRef of inductive - | ConstructRef of constructor + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of constant (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) let isVarRef = function VarRef _ -> true | _ -> false let isConstRef = function ConstRef _ -> true | _ -> false diff --git a/library/globnames.mli b/library/globnames.mli index 253c20baae..a401046b49 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -13,10 +13,10 @@ open Mod_subst (** {6 Global reference is a kernel side type for all references together } *) type global_reference = - | VarRef of variable - | ConstRef of constant - | IndRef of inductive - | ConstructRef of constructor + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of constant (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) val isVarRef : global_reference -> bool val isConstRef : global_reference -> bool -- cgit v1.2.3 From afb9c9a65097dd901df18c443ca13ad4bf394985 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 11:21:42 +0100 Subject: Do not query module files that have already been loaded. For a script that does just "Require Reals", this avoids 40k queries. Note that this changes the signature of the FileDependency feedback. Indeed, it no longer provides the physical path to the dependency but only its logical path (since the physical path is no longer available). The physical path could still have been recovered thanks to the libraries_filename_table list. But due to the existence of the overwrite_library_filenames function, its content cannot be trusted. So anyone interested in the actual physical path should now also rely on the FileLoaded feedback. --- library/library.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 024ac9e6fa..734a50fe39 100644 --- a/library/library.ml +++ b/library/library.ml @@ -286,12 +286,12 @@ let locate_absolute_library dir = with Not_found -> [] in match find ".vo" @ find ".vio" with | [] -> raise LibNotFound - | [file] -> dir, file + | [file] -> file | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ str vo ++ str " because it is more recent"); - dir, vi - | [vo;vi] -> dir, vo + vi + | [vo;vi] -> vo | _ -> assert false let locate_qualified_library ?root ?(warn = true) qid = @@ -459,7 +459,7 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) let rec intern_library (needed, contents) (dir, f) from = - Pp.feedback(Feedback.FileDependency (from, f)); + Pp.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> @@ -467,6 +467,7 @@ let rec intern_library (needed, contents) (dir, f) from = 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 f = match f with Some f -> f | None -> try_locate_absolute_library dir in let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then errorlabstrm "load_physical_library" @@ -481,13 +482,13 @@ and intern_library_deps libs dir m from = (dir :: needed, DPMap.add dir m contents ) and intern_mandatory_library caller from libs (dir,d) = - let digest, libs = intern_library libs (try_locate_absolute_library dir) from in + let digest, libs = intern_library libs (dir, None) from in if not (Safe_typing.digest_match ~actual:digest ~required:d) then errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir)); libs -let rec_intern_library libs mref = - let _, libs = intern_library libs mref None in +let rec_intern_library libs (dir, f) = + let _, libs = intern_library libs (dir, Some f) None in libs let native_name_from_filename f = -- cgit v1.2.3 From d55676344c8dc0d9a87b2ef12ec2348281db4bf5 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 14:10:31 +0100 Subject: Move the From logic to Loadpath.expand_path. --- library/library.ml | 12 +----------- library/loadpath.ml | 21 +++++++++++---------- library/loadpath.mli | 2 +- 3 files changed, 13 insertions(+), 22 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 734a50fe39..4f964a0510 100644 --- a/library/library.ml +++ b/library/library.ml @@ -297,17 +297,7 @@ let locate_absolute_library dir = let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) let dir, base = repr_qualid qid 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 loadpath = Loadpath.expand_path ?root dir in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let find ext = try diff --git a/library/loadpath.ml b/library/loadpath.ml index 622d390a2c..16b4194544 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -97,18 +97,19 @@ let filter_path f = in aux !load_paths -let expand_path dir = +let expand_path ?root dir = let rec aux = function | [] -> [] - | { 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 + | { 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 = diff --git a/library/loadpath.mli b/library/loadpath.mli index 269e28e0b5..732f6349fb 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -42,7 +42,7 @@ val find_load_path : CUnix.physical_path -> t val is_in_load_paths : CUnix.physical_path -> bool (** Whether a physical path is currently bound. *) -val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list +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. *) -- cgit v1.2.3 From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 22:35:09 +0100 Subject: Do not compose "str" and "to_string" whenever possible. For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read. --- library/libnames.ml | 4 ++-- library/library.ml | 10 +++++----- library/nameops.ml | 4 ++-- library/nametab.ml | 2 +- 4 files changed, 10 insertions(+), 10 deletions(-) (limited to 'library') diff --git a/library/libnames.ml b/library/libnames.ml index cdaec6a3de..36b46ca498 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -13,7 +13,7 @@ open Names (**********************************************) -let pr_dirpath sl = (str (DirPath.to_string sl)) +let pr_dirpath sl = str (DirPath.to_string sl) (*s Operations on dirpaths *) @@ -197,7 +197,7 @@ let string_of_reference = function let pr_reference = function | Qualid (_,qid) -> pr_qualid qid - | Ident (_,id) -> str (Id.to_string id) + | Ident (_,id) -> Id.print id let loc_of_reference = function | Qualid (loc,qid) -> loc diff --git a/library/library.ml b/library/library.ml index 4f964a0510..ef621e16be 100644 --- a/library/library.ml +++ b/library/library.ml @@ -132,7 +132,7 @@ let try_find_library dir = try find_library dir with Not_found -> errorlabstrm "Library.find_library" - (str "Unknown library " ++ str (DirPath.to_string dir)) + (str "Unknown library " ++ pr_dirpath dir) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -474,7 +474,7 @@ and intern_library_deps libs dir m from = and intern_mandatory_library caller from libs (dir,d) = let digest, libs = intern_library libs (dir, None) from in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir)); + errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); libs let rec_intern_library libs (dir, f) = @@ -567,7 +567,7 @@ 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) ++ str " is not a module") + (loc,"import_library", pr_qualid qid ++ str " is not a module") let import_module export modl = (* Optimization: libraries in a raw in the list are imported @@ -592,7 +592,7 @@ let import_module export modl = try Declaremods.import_module export mp; aux [] l with Not_found -> user_err_loc (loc,"import_library", - str (string_of_qualid dir) ++ str " is not a module")) + pr_qualid dir ++ str " is not a module")) | [] -> flush acc in aux [] modl @@ -604,7 +604,7 @@ let check_coq_overwriting p id = let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then errorlabstrm "" - (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++ + (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") (* Verifies that a string starts by a letter and do not contain diff --git a/library/nameops.ml b/library/nameops.ml index 3a23ab97df..418d620c25 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -12,7 +12,7 @@ open Names (* Identifiers *) -let pr_id id = str (Id.to_string id) +let pr_id id = Id.print id let pr_name = function | Anonymous -> str "_" @@ -141,7 +141,7 @@ let name_max na1 na2 = | Name _ -> na1 | Anonymous -> na2 -let pr_lab l = str (Label.to_string l) +let pr_lab l = Label.print l let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/nametab.ml b/library/nametab.ml index 5b6d7cd982..621640ef98 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -523,7 +523,7 @@ let shortest_qualid_of_tactic kn = KnTab.shortest_qualid Id.Set.empty sp !the_tactictab let pr_global_env env ref = - try str (string_of_qualid (shortest_qualid_of_global env ref)) + try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e -- cgit v1.2.3 From 8c684847844b25bd4ce071867fb480c9caa8cb62 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 22:36:27 +0100 Subject: Avoid a pointless conversion/copy. --- library/library.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index ef621e16be..7aaa8b2e6a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -602,7 +602,7 @@ let import_module export modl = let check_coq_overwriting p id = let l = DirPath.repr p in let is_empty = match l with [] -> true | _ -> false in - if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then + if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then errorlabstrm "" (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") -- cgit v1.2.3 From 1a8a8db7a9e4eb5ab56cd192411529661a4972c7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 23 Dec 2015 14:27:13 +0100 Subject: Remove Library.mem, which is pointless since 8.5. --- library/library.ml | 7 ------- library/library.mli | 3 --- 2 files changed, 10 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 7aaa8b2e6a..db95213fe9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -769,13 +769,6 @@ let save_library_raw f sum lib univs proofs = System.marshal_out_segment f' ch (proofs : seg_proofs); close_out ch -(************************************************************************) -(*s Display the memory use of a library. *) - -open Printf - -let mem s = Pp.mt () - module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) diff --git a/library/library.mli b/library/library.mli index d5e610dd67..71aefdbd86 100644 --- a/library/library.mli +++ b/library/library.mli @@ -82,8 +82,5 @@ val locate_qualified_library : *) -(** {6 Statistics: display the memory use of a library. } *) -val mem : DirPath.t -> Pp.std_ppcmds - (** {6 Native compiler. } *) val native_name_from_filename : string -> string -- cgit v1.2.3 From 74c29764359272b29af081b30762549777ae8825 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:05:03 +0100 Subject: Remove some useless type declarations. --- library/declare.ml | 3 --- library/keys.ml | 2 -- 2 files changed, 5 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 994a6557ad..c1697a434a 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -417,9 +417,6 @@ let assumption_message id = (** Global universe names, in a different summary *) -type universe_names = - (Univ.universe_level Idmap.t * Id.t Univ.LMap.t) - (* Discharged or not *) type universe_decl = polymorphic * (Id.t * Univ.universe_level) list diff --git a/library/keys.ml b/library/keys.ml index 3d277476f1..6b2466f3de 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -62,8 +62,6 @@ module Keyset = Keymap.Set (* Mapping structure for references to be considered equivalent *) -type keys = Keyset.t Keymap.t - let keys = Summary.ref Keymap.empty ~name:"Keys_decl" let add_kv k v m = -- cgit v1.2.3 From 3f91296b5cf1dc9097d5368c2df5c6f70a04210c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:05:56 +0100 Subject: Remove keys for evar and meta, since they cannot occur. --- library/keys.ml | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) (limited to 'library') diff --git a/library/keys.ml b/library/keys.ml index 6b2466f3de..e30cf67175 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -12,35 +12,31 @@ open Globnames open Term open Libobject -type key = +type key = | KGlob of global_reference - | KLam + | KLam | KLet | KProd | KSort - | KEvar - | KCase - | KFix + | KCase + | KFix | KCoFix - | KRel - | KMeta + | KRel module KeyOrdered = struct type t = key let hash gr = match gr with - | KGlob gr -> 10 + RefOrdered.hash gr + | KGlob gr -> 8 + RefOrdered.hash gr | KLam -> 0 | KLet -> 1 | KProd -> 2 | KSort -> 3 - | KEvar -> 4 - | KCase -> 5 - | KFix -> 6 - | KCoFix -> 7 - | KRel -> 8 - | KMeta -> 9 + | KCase -> 4 + | KFix -> 5 + | KCoFix -> 6 + | KRel -> 7 let compare gr1 gr2 = match gr1, gr2 with @@ -151,12 +147,10 @@ let pr_key pr_global = function | KLet -> str"Let" | KProd -> str"Product" | KSort -> str"Sort" - | KEvar -> str"Evar" | KCase -> str"Case" | KFix -> str"Fix" | KCoFix -> str"CoFix" | KRel -> str"Rel" - | KMeta -> str"Meta" let pr_keyset pr_global v = prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- library/loadpath.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'library') diff --git a/library/loadpath.ml b/library/loadpath.ml index 16b4194544..f77bd1ef53 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -84,10 +84,6 @@ let add_load_path phys_path coq_path ~implicit = end | _ -> anomaly_too_many_paths phys_path -let extend_path_with_dirpath p dir = - List.fold_left Filename.concat p - (List.rev_map Id.to_string (DirPath.repr dir)) - let filter_path f = let rec aux = function | [] -> [] -- cgit v1.2.3 From 23cbf43f353c50fa72b72d694611c5c14367cea2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jan 2016 00:58:42 +0100 Subject: Protect code against changes in Map interface. The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps. --- library/goptions.mli | 2 +- library/libnames.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/goptions.mli b/library/goptions.mli index 9d87c14c50..25b5315c2a 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -133,7 +133,7 @@ val declare_stringopt_option: string option option_sig -> string option write_fu (** {6 Special functions supposed to be used only in vernacentries.ml } *) -module OptionMap : Map.S with type key = option_name +module OptionMap : CSig.MapS with type key = option_name val get_string_table : option_name -> diff --git a/library/libnames.mli b/library/libnames.mli index b95c088715..c72f517532 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -60,7 +60,7 @@ val path_of_string : string -> full_path val string_of_path : full_path -> string val pr_path : full_path -> std_ppcmds -module Spmap : Map.S with type key = full_path +module Spmap : CSig.MapS with type key = full_path val restrict_path : int -> full_path -> full_path -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- library/decls.ml | 3 +-- library/global.mli | 4 ++-- library/lib.mli | 8 ++++---- 3 files changed, 7 insertions(+), 8 deletions(-) (limited to 'library') diff --git a/library/decls.ml b/library/decls.ml index 8d5085f70e..b5f9143b8a 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -11,7 +11,6 @@ open Util open Names -open Context open Decl_kinds open Libnames @@ -55,7 +54,7 @@ let initialize_named_context_for_proof () = Environ.push_named_context_val d signv) sign Environ.empty_named_context_val let last_section_hyps dir = - fold_named_context + Context.Named.fold_outside (fun (id,_,_) sec_ids -> try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) diff --git a/library/global.mli b/library/global.mli index 09ed4eb0a8..d6547105d4 100644 --- a/library/global.mli +++ b/library/global.mli @@ -21,7 +21,7 @@ val env_is_initial : unit -> bool val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Context.named_context +val named_context : unit -> Context.Named.t (** {6 Enriching the global environment } *) @@ -73,7 +73,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.named_declaration +val lookup_named : variable -> Context.Named.Declaration.t val lookup_constant : constant -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body diff --git a/library/lib.mli b/library/lib.mli index bb88317591..874fc89fb4 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -164,7 +164,7 @@ type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t val instance_from_variable_context : variable_context -> Names.Id.t array -val named_of_variable_context : variable_context -> Context.named_context +val named_of_variable_context : variable_context -> Context.Named.t val section_segment_of_constant : Names.constant -> abstr_info val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info @@ -175,8 +175,8 @@ val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit val add_section_constant : bool (* is_projection *) -> - Names.constant -> Context.named_context -> unit -val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit + Names.constant -> Context.Named.t -> unit +val add_section_kn : Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) @@ -189,6 +189,6 @@ val discharge_inductive : Names.inductive -> Names.inductive (* discharging a constant in one go *) val full_replacement_context : unit -> Opaqueproof.work_list list val full_section_segment_of_constant : - Names.constant -> (Context.named_context -> Context.named_context) list + Names.constant -> (Context.Named.t -> Context.Named.t) list -- cgit v1.2.3 From 33617aa7b36f157f6314a83dde6ba45164ddd05b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 14 Dec 2015 15:04:52 +0100 Subject: Changing "P is assumed" to "P is declared". The term "assumed" refers more to the type of the object than to the name of the object. It is particularly misguiding when P:Prop since P is assumed would suggest that a proof of P is assumed, and not that the variable P itself is declared (see discussion with P. Castéran on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015). --- library/declare.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index c1697a434a..40858eeec6 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -413,7 +413,10 @@ let definition_message id = Flags.if_verbose msg_info (pr_id id ++ str " is defined") let assumption_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is assumed") + (* Changing "assumed" to "declared", "assuming" referring more to + the type of the object than to the name of the object (see + discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) + Flags.if_verbose msg_info (pr_id id ++ str " is declared") (** Global universe names, in a different summary *) -- cgit v1.2.3 From 74a5cfa8b2f1a881ebf010160421cf0775c2a084 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 15 Jan 2016 17:49:49 +0100 Subject: Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. --- library/declare.ml | 19 ++++++++++++++++--- library/declare.mli | 5 +++++ library/declaremods.ml | 23 +++++++++++++++++++++-- library/declaremods.mli | 7 +++++++ library/lib.ml | 6 ++++++ library/lib.mli | 4 ++++ library/library.ml | 3 +++ library/library.mli | 3 +++ 8 files changed, 65 insertions(+), 5 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 994a6557ad..8d86c4cf0f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -32,6 +32,14 @@ type internal_flag = | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) +(** XML output hooks *) + +let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore () +let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore () +let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore () + +let if_xml f x = if !Flags.xml_export then f x else () + (** Declaration of section variables and local definitions *) type section_variable_entry = @@ -83,6 +91,7 @@ let declare_variable id obj = declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); Heads.declare_head (EvalVarRef id); + if_xml (Hook.get f_xml_declare_variable) oname; oname @@ -216,6 +225,7 @@ let declare_constant_common id cst = let id = Label.to_id (pi3 (Constant.repr3 c)) in ignore(add_leaf id o); update_tables c; + let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in match role with | Safe_typing.Subproof -> () | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]) @@ -257,6 +267,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e cst_was_seff = false; } in let kn = declare_constant_common id cst in + let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in kn let declare_definition ?(internal=UserIndividualRequest) @@ -365,8 +376,9 @@ let declare_projections mind = let kn' = declare_constant id (ProjectionEntry entry, IsDefinition StructureComponent) in - assert(eq_constant kn kn')) kns; true - | Some None | None -> false + assert(eq_constant kn kn')) kns; true,true + | Some None -> true,false + | None -> false,false (* for initial declaration *) let declare_mind mie = @@ -375,9 +387,10 @@ let declare_mind mie = | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - let isprim = declare_projections mind in + let isrecord,isprim = declare_projections mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; + if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname); oname, isprim (* Declaration messages *) diff --git a/library/declare.mli b/library/declare.mli index c6119a58ac..60676ff43f 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -71,6 +71,11 @@ val set_declare_scheme : the whole block and a boolean indicating if it is a primitive record. *) val declare_mind : mutual_inductive_entry -> object_name * bool +(** Hooks for XML output *) +val xml_declare_variable : (object_name -> unit) Hook.t +val xml_declare_constant : (internal_flag * constant -> unit) Hook.t +val xml_declare_inductive : (bool * object_name -> unit) Hook.t + (** Declaration messages *) val definition_message : Id.t -> unit diff --git a/library/declaremods.ml b/library/declaremods.ml index 7f607a51c9..0162de10ce 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -557,6 +557,17 @@ let openmodtype_info = Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" +(** XML output hooks *) + +let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore () +let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore () +let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore () +let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore () +let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore () +let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore () + +let if_xml f x = if !Flags.xml_export then f x else () + (** {6 Modules : start, end, declare} *) module RawModOps = struct @@ -578,7 +589,9 @@ let start_module interp_modast export id args res fs = openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - Lib.add_frozen_state (); mp + Lib.add_frozen_state (); + if_xml (Hook.get f_xml_start_module) mp; + mp let end_module () = let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in @@ -617,6 +630,7 @@ let end_module () = assert (ModPath.equal (mp_of_kn (snd newoname)) mp); Lib.add_frozen_state () (* to prevent recaching *); + if_xml (Hook.get f_xml_end_module) mp; mp let declare_module interp_modast id args res mexpr_o fs = @@ -666,6 +680,7 @@ let declare_module interp_modast id args res mexpr_o fs = let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in ignore (Lib.add_leaf id (in_module sobjs)); + if_xml (Hook.get f_xml_declare_module) mp; mp end @@ -682,7 +697,9 @@ let start_modtype interp_modast id args mtys fs = openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - Lib.add_frozen_state (); mp + Lib.add_frozen_state (); + if_xml (Hook.get f_xml_start_module_type) mp; + mp let end_modtype () = let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in @@ -699,6 +716,7 @@ let end_modtype () = assert (ModPath.equal (mp_of_kn (snd oname)) mp); Lib.add_frozen_state ()(* to prevent recaching *); + if_xml (Hook.get f_xml_end_module_type) mp; mp let declare_modtype interp_modast id args mtys (mty,ann) fs = @@ -729,6 +747,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = check_subtypes_mt mp sub_mty_l; ignore (Lib.add_leaf id (in_modtype sobjs)); + if_xml (Hook.get f_xml_declare_module_type) mp; mp end diff --git a/library/declaremods.mli b/library/declaremods.mli index 319d168d05..8b9f70b35a 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -63,6 +63,13 @@ val start_modtype : val end_modtype : unit -> module_path +(** Hooks for XML output *) +val xml_declare_module : (module_path -> unit) Hook.t +val xml_start_module : (module_path -> unit) Hook.t +val xml_end_module : (module_path -> unit) Hook.t +val xml_declare_module_type : (module_path -> unit) Hook.t +val xml_start_module_type : (module_path -> unit) Hook.t +val xml_end_module_type : (module_path -> unit) Hook.t (** {6 Libraries i.e. modules on disk } *) diff --git a/library/lib.ml b/library/lib.ml index 297441e6e2..42cea4de8e 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -497,6 +497,10 @@ let full_section_segment_of_constant con = (*************) (* Sections. *) +(* XML output hooks *) +let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore () +let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore () + let open_section id = let olddir,(mp,oldsec) = !path_prefix in let dir = add_dirpath_suffix olddir id in @@ -508,6 +512,7 @@ let open_section id = (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; + if !Flags.xml_export then Hook.get f_xml_open_section id; add_section () @@ -536,6 +541,7 @@ let close_section () = let full_olddir = fst !path_prefix in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); + if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname)); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; diff --git a/library/lib.mli b/library/lib.mli index bb88317591..398149a50f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -157,6 +157,10 @@ val unfreeze : frozen -> unit val init : unit -> unit +(** XML output hooks *) +val xml_open_section : (Names.Id.t -> unit) Hook.t +val xml_close_section : (Names.Id.t -> unit) Hook.t + (** {6 Section management for discharge } *) type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types diff --git a/library/library.ml b/library/library.ml index 024ac9e6fa..365d119ddf 100644 --- a/library/library.ml +++ b/library/library.ml @@ -555,6 +555,8 @@ let in_require : require_obj -> obj = (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) +let (f_xml_require, xml_require) = Hook.make ~default:ignore () + let require_library_from_dirpath modrefl export = let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in @@ -568,6 +570,7 @@ let require_library_from_dirpath modrefl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); + if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl; add_frozen_state () (* the function called by Vernacentries.vernac_import *) diff --git a/library/library.mli b/library/library.mli index d5e610dd67..fb0ce47950 100644 --- a/library/library.mli +++ b/library/library.mli @@ -67,6 +67,9 @@ 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 Hook for the xml exportation of libraries } *) +val xml_require : (DirPath.t -> unit) Hook.t + (** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- library/declare.ml | 2 +- library/declare.mli | 2 +- library/declaremods.ml | 2 +- library/declaremods.mli | 2 +- library/decls.ml | 2 +- library/decls.mli | 2 +- library/dischargedhypsmap.ml | 2 +- library/dischargedhypsmap.mli | 2 +- library/global.ml | 2 +- library/global.mli | 2 +- library/globnames.ml | 2 +- library/globnames.mli | 2 +- library/goptions.ml | 2 +- library/goptions.mli | 2 +- library/heads.ml | 2 +- library/heads.mli | 2 +- library/impargs.ml | 2 +- library/impargs.mli | 2 +- library/keys.ml | 2 +- library/keys.mli | 2 +- library/kindops.ml | 2 +- library/kindops.mli | 2 +- library/lib.ml | 2 +- library/lib.mli | 2 +- library/libnames.ml | 2 +- library/libnames.mli | 2 +- library/libobject.ml | 2 +- library/libobject.mli | 2 +- library/library.ml | 2 +- library/library.mli | 2 +- library/loadpath.ml | 2 +- library/loadpath.mli | 2 +- library/nameops.ml | 2 +- library/nameops.mli | 2 +- library/nametab.ml | 2 +- library/nametab.mli | 2 +- library/states.ml | 2 +- library/states.mli | 2 +- library/summary.ml | 2 +- library/summary.mli | 2 +- library/universes.ml | 2 +- library/universes.mli | 2 +- 42 files changed, 42 insertions(+), 42 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 8d86c4cf0f..5f6f0fe45e 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* None) kn' cst.const_hyps; + add_section_constant cst.const_polymorphic kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (constant_of_kn kn) obj.cst_kind @@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let kn' = Global.add_mind dir id mie in assert (eq_mind kn' (mind_of_kn kn)); let mind = Global.lookup_mind kn' in - add_section_kn kn' mind.mind_hyps; + add_section_kn mind.mind_polymorphic kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names diff --git a/library/lib.ml b/library/lib.ml index ff89291679..e4617cafb6 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -408,17 +408,24 @@ let add_section () = sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty), (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab +let check_same_poly p vars = + let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in + if List.exists pred vars then + error "Cannot mix universe polymorphic and monomorphic declarations in sections." + let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + check_same_poly poly vars; + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl let add_section_context ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := (Context ctx :: vars,repl,abs)::sl + check_same_poly true vars; + sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = let rec aux = function @@ -443,10 +450,11 @@ let instance_from_variable_context sign = let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx -let add_section_replacement f g hyps = +let add_section_replacement f g poly hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> + let () = check_same_poly poly vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in @@ -454,13 +462,13 @@ let add_section_replacement f g hyps = sectab := (vars,f (Univ.UContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl -let add_section_kn kn = +let add_section_kn poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f + add_section_replacement f f poly -let add_section_constant is_projection kn = +let add_section_constant poly kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f + add_section_replacement f f poly let replacement_context () = pi2 (List.hd !sectab) diff --git a/library/lib.mli b/library/lib.mli index 29fc7cd24b..513c48549e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -178,9 +178,10 @@ val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit -val add_section_constant : bool (* is_projection *) -> +val add_section_constant : Decl_kinds.polymorphic -> Names.constant -> Context.named_context -> unit -val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit +val add_section_kn : Decl_kinds.polymorphic -> + Names.mutual_inductive -> Context.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) -- cgit v1.2.3 From 5d9eaa378277ed96456fec5a2037a8da4f38c8e0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Feb 2016 20:07:33 +0100 Subject: Optimizing the universes_of_constr_function. Instead of relying on a costly set union, we take advantage of the fact that instances are small compared to the set of universes. --- library/universes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 7972c478ad..3bebdafc78 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -959,10 +959,10 @@ let universes_of_constr c = let rec aux s c = match kind_of_term c with | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.union (Instance.levels u) s + LSet.fold LSet.add (Instance.levels u) s | Sort u when not (Sorts.is_small u) -> let u = univ_of_sort u in - LSet.union (Universe.levels u) s + LSet.fold LSet.add (Universe.levels u) s | _ -> fold_constr aux s c in aux LSet.empty c -- cgit v1.2.3 From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 29 Jan 2016 10:13:12 +0100 Subject: CLEANUP: Context.{Rel,Named}.Declaration.t Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- library/decls.ml | 10 +++++++--- library/heads.ml | 11 ++++++----- library/impargs.ml | 15 ++++++++------- library/lib.ml | 9 +++++++-- 4 files changed, 28 insertions(+), 17 deletions(-) (limited to 'library') diff --git a/library/decls.ml b/library/decls.ml index cafdcd0abd..6e21880f1f 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -46,16 +46,20 @@ let constant_kind kn = Cmap.find kn !csttab (** Miscellaneous functions. *) +open Context.Named.Declaration + let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right - (fun (id,c,t as d) signv -> - let d = if variable_opacity id then (id,None,t) else d in + (fun d signv -> + let id = get_id d in + let d = if variable_opacity id then LocalAssum (id, get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val let last_section_hyps dir = Context.Named.fold_outside - (fun (id,_,_) sec_ids -> + (fun d sec_ids -> + let id = get_id d in try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) diff --git a/library/heads.ml b/library/heads.ml index 8124d3474f..4c9b789769 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -15,6 +15,7 @@ open Environ open Globnames open Libobject open Lib +open Context.Named.Declaration (** Characterization of the head of a term *) @@ -63,9 +64,9 @@ let kind_of_head env t = (try on_subterm k l b (variable_head id) with Not_found -> (* a goal variable *) - match pi2 (lookup_named id env) with - | Some c -> aux k l c b - | None -> NotImmediatelyComputableHead) + match lookup_named id env with + | LocalDef (_,c,_) -> aux k l c b + | LocalAssum _ -> NotImmediatelyComputableHead) | Const (cst,_) -> (try on_subterm k l b (constant_head cst) with Not_found -> @@ -132,8 +133,8 @@ let compute_head = function | None -> RigidHead (RigidParameter cst) | Some c -> kind_of_head env c) | EvalVarRef id -> - (match pi2 (Global.lookup_named id) with - | Some c when not (Decls.variable_opacity id) -> + (match Global.lookup_named id with + | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> kind_of_head (Global.env()) c | _ -> RigidHead (RigidVar id)) diff --git a/library/impargs.ml b/library/impargs.ml index f5f6a3eba7..4e344a9543 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -165,6 +165,7 @@ let update pos rig (na,st) = (* modified is_rigid_reference with a truncated env *) let is_flexible_reference env bound depth f = + let open Context.Named.Declaration in match kind_of_term f with | Rel n when n >= bound+depth -> (* inductive type *) false | Rel n when n >= depth -> (* previous argument *) true @@ -173,8 +174,7 @@ let is_flexible_reference env bound depth f = let cb = Environ.lookup_constant kn env in (match cb.const_body with Def _ -> true | _ -> false) | Var id -> - let (_, value, _) = Environ.lookup_named id env in - begin match value with None -> false | _ -> true end + Environ.lookup_named id env |> is_local_def | Ind _ | Construct _ -> false | _ -> true @@ -234,13 +234,14 @@ let find_displayed_name_in all avoid na (_,b as envnames_b) = let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rigid = ref true in + let open Context.Rel.Declaration in let rec aux env avoid n names t = let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (na,a,b) -> let na',avoid' = find_displayed_name_in all avoid na (names,b) in add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1)) - (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b) + (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b) | _ -> rigid := is_rigid_head t; let names = List.rev names in @@ -252,7 +253,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = match kind_of_term (whd_betadeltaiota env t) with | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all [] na ([],b) in - let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in + let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in !rigid, Array.to_list v | _ -> true, [] @@ -427,7 +428,7 @@ let compute_mib_implicits flags manual kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (** No need to care about constraints here *) - (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i)))) + Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i)))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = @@ -449,8 +450,8 @@ let compute_all_mib_implicits flags manual kn = let compute_var_implicits flags manual id = let env = Global.env () in - let (_,_,ty) = lookup_named id env in - compute_semi_auto_implicits env flags manual ty + let open Context.Named.Declaration in + compute_semi_auto_implicits env flags manual (get_type (lookup_named id env)) (* Implicits of a global reference. *) diff --git a/library/lib.ml b/library/lib.ml index e4617cafb6..f8bb6bac59 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -428,8 +428,10 @@ let add_section_context ctx = sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = + let open Context.Named.Declaration in let rec aux = function - | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) -> + let (id',b,t) = to_tuple decl in let l, r = aux (idl,hyps) in (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r | (Variable (_,_,poly,ctx)::idl,hyps) -> @@ -448,7 +450,10 @@ let instance_from_variable_context sign = | [] -> [] in Array.of_list (inst_rec sign) -let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx +let named_of_variable_context ctx = let open Context.Named.Declaration in + List.map (function id,_,None,t -> LocalAssum (id,t) + | id,_,Some b,t -> LocalDef (id,b,t)) + ctx let add_section_replacement f g poly hyps = match !sectab with -- cgit v1.2.3 From 35cc038e96395b0f4eaaeed3a5a48e6da2293f7e Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 19:01:35 +0100 Subject: Fix #4607: do not read native code files if native compiler was disabled. --- library/library.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 79e5792c02..ccda57c2c5 100644 --- a/library/library.ml +++ b/library/library.ml @@ -171,9 +171,8 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - (* This will not produce errors or warnings if the native compiler was - not enabled *) - Nativelib.link_library ~prefix ~dirname ~basename:f + if not Coq_config.no_native_compiler then + Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function | [] -> link m; [libname] -- cgit v1.2.3