diff options
93 files changed, 1405 insertions, 570 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c0a01f3fd..20dac57a7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -105,7 +105,7 @@ before_script: - set +e variables: &warnings-variables - EXTRA_CONF: "-native-compiler yes -coqide opt" + EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" EXTRA_PACKAGES: "$COQIDE_PACKAGES" EXTRA_OPAM: "$COQIDE_OPAM" diff --git a/.travis.yml b/.travis.yml index 1f6bb11e0..83a4e7fdd 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,6 +39,7 @@ env: - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" - NATIVE_COMP="yes" - COQ_DEST="-local" + - MAIN_TARGET="world" # Main test suites matrix: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" @@ -139,8 +140,8 @@ matrix: # Ocaml warnings with two compilers - env: - - TEST_TARGET="coqocaml" - - EXTRA_CONF="-coqide opt -warn-error" + - MAIN_TARGET="coqocaml" + - EXTRA_CONF="-byte-only -coqide byte -warn-error" - EXTRA_OPAM="hevea ${LABLGTK}" # dummy target - BUILD_TARGET="clean" @@ -155,11 +156,11 @@ matrix: - libgtksourceview2.0-dev - env: - - TEST_TARGET="coqocaml" + - MAIN_TARGET="coqocaml" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-coqide opt -warn-error" + - EXTRA_CONF="-byte-only -coqide byte -warn-error" - EXTRA_OPAM="num hevea ${LABLGTK_BE}" # dummy target - BUILD_TARGET="clean" @@ -224,11 +225,11 @@ script: - echo -en 'travis_fold:end:coq.config\\r' - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r' -- make -j ${NJOBS} +- make -j ${NJOBS} ${MAIN_TARGET} - echo -en 'travis_fold:end:coq.build\\r' - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r' -- ${TW} make -j ${NJOBS} ${TEST_TARGET} +- if [ -n "${TEST_TARGET}" ]; then ${TW} make -j ${NJOBS} ${TEST_TARGET}; fi - echo -en 'travis_fold:end:coq.test\\r' - set +e diff --git a/API/API.mli b/API/API.mli index df5a9b131..6227f17c6 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1861,6 +1861,60 @@ end (* Modules from intf/ *) (************************************************************************) +module Libnames : +sig + + open Util + open Names + + type full_path + val pr_path : full_path -> Pp.t + val make_path : Names.DirPath.t -> Names.Id.t -> full_path + val eq_full_path : full_path -> full_path -> bool + val repr_path : full_path -> Names.DirPath.t * Names.Id.t + val dirpath : full_path -> Names.DirPath.t + val path_of_string : string -> full_path + + type qualid + val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid + val qualid_eq : qualid -> qualid -> bool + val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t + val pr_qualid : qualid -> Pp.t + val string_of_qualid : qualid -> string + val qualid_of_string : string -> qualid + val qualid_of_path : full_path -> qualid + val qualid_of_dirpath : Names.DirPath.t -> qualid + val qualid_of_ident : Names.Id.t -> qualid + + type reference = + | Qualid of qualid Loc.located + | Ident of Names.Id.t Loc.located + val loc_of_reference : reference -> Loc.t option + val qualid_of_reference : reference -> qualid Loc.located + val pr_reference : reference -> Pp.t + + val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool + val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t + val dirpath_of_string : string -> Names.DirPath.t + val pr_dirpath : Names.DirPath.t -> Pp.t + [@@ocaml.deprecated "Alias for DirPath.print"] + + val string_of_path : full_path -> string + + val basename : full_path -> Names.Id.t + + type object_name = full_path * Names.KerName.t + type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; + } + + module Dirset : Set.S with type elt = DirPath.t + module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset + module Spmap : CSig.MapS with type key = full_path +end + module Misctypes : sig type evars_flag = bool @@ -1883,10 +1937,15 @@ sig | GSet (** representation of [Set] literal *) | GType of 'a (** representation of [Type] literal *) - type level_info = Names.Name.t Loc.located option + type 'a universe_kind = + | UAnonymous + | UUnknown + | UNamed of 'a + + type level_info = Libnames.reference universe_kind type glob_level = level_info glob_sort_gen - type sort_info = Names.Name.t Loc.located list + type sort_info = (Libnames.reference * int) option list type glob_sort = sort_info glob_sort_gen type ('a, 'b) gen_universe_decl = { @@ -2039,60 +2098,6 @@ sig [@@ocaml.deprecated "alias of API.Names"] end -module Libnames : -sig - - open Util - open Names - - type full_path - val pr_path : full_path -> Pp.t - val make_path : Names.DirPath.t -> Names.Id.t -> full_path - val eq_full_path : full_path -> full_path -> bool - val repr_path : full_path -> Names.DirPath.t * Names.Id.t - val dirpath : full_path -> Names.DirPath.t - val path_of_string : string -> full_path - - type qualid - val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid - val qualid_eq : qualid -> qualid -> bool - val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t - val pr_qualid : qualid -> Pp.t - val string_of_qualid : qualid -> string - val qualid_of_string : string -> qualid - val qualid_of_path : full_path -> qualid - val qualid_of_dirpath : Names.DirPath.t -> qualid - val qualid_of_ident : Names.Id.t -> qualid - - type reference = - | Qualid of qualid Loc.located - | Ident of Names.Id.t Loc.located - val loc_of_reference : reference -> Loc.t option - val qualid_of_reference : reference -> qualid Loc.located - val pr_reference : reference -> Pp.t - - val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool - val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t - val dirpath_of_string : string -> Names.DirPath.t - val pr_dirpath : Names.DirPath.t -> Pp.t - [@@ocaml.deprecated "Alias for DirPath.print"] - - val string_of_path : full_path -> string - - val basename : full_path -> Names.Id.t - - type object_name = full_path * Names.KerName.t - type object_prefix = { - obj_dir : DirPath.t; - obj_mp : ModPath.t; - obj_sec : DirPath.t; - } - - module Dirset : Set.S with type elt = DirPath.t - module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset - module Spmap : CSig.MapS with type key = full_path -end - module Globnames : sig @@ -2754,10 +2759,10 @@ sig type universe_binders type universe_opt_subst val fresh_inductive_instance : Environ.env -> Names.inductive -> Constr.pinductive Univ.in_universe_context_set - val new_Type : Names.DirPath.t -> Constr.types + val new_Type : unit -> Constr.types val type_of_global : Globnames.global_reference -> Constr.types Univ.in_universe_context_set val constr_of_global : Globnames.global_reference -> Constr.t - val new_univ_level : Names.DirPath.t -> Univ.Level.t + val new_univ_level : unit -> Univ.Level.t val new_sort_in_family : Sorts.family -> Sorts.t val pr_with_global_universes : Univ.Level.t -> Pp.t val pr_universe_opt_subst : universe_opt_subst -> Pp.t @@ -4800,24 +4805,26 @@ end module Proof : sig - type proof - type 'a focus_kind + type t + type proof = t + [@@ocaml.deprecated "please use [Proof.t]"] - val proof : proof -> + type 'a focus_kind + val proof : t -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Goal.goal list * Goal.goal list * Evd.evar_map val run_tactic : Environ.env -> - unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree) - val unshelve : proof -> proof - val maximal_unfocus : 'a focus_kind -> proof -> proof - val pr_proof : proof -> Pp.t + unit Proofview.tactic -> t -> t * (bool * Proofview_monad.Info.tree) + val unshelve : t -> t + val maximal_unfocus : 'a focus_kind -> t -> t + val pr_proof : t -> Pp.t module V82 : sig - val grab_evars : proof -> proof + val grab_evars : t -> t - val subgoals : proof -> Goal.goal list Evd.sigma + val subgoals : t -> Goal.goal list Evd.sigma [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] end @@ -4831,24 +4838,25 @@ end module Proof_global : sig - type state + type t + type state = t + [@@ocaml.deprecated "please use [Proof_global.t]"] type proof_mode = { name : string; set : unit -> unit ; reset : unit -> unit } - type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - proof_universes + UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -4862,14 +4870,14 @@ sig Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit val with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof * 'a) -> 'a + (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a val simple_with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit + (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit val compact_the_proof : unit -> unit val register_proof_mode : proof_mode -> unit exception NoCurrentProof - val give_me_the_proof : unit -> Proof.proof + val give_me_the_proof : unit -> Proof.t (** @raise NoCurrentProof when outside proof mode. *) val discard_all : unit -> unit @@ -5000,9 +5008,9 @@ sig val by : unit Proofview.tactic -> bool val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> - Proof.proof -> Proof.proof * bool + Proof.t -> Proof.t * bool val cook_proof : - unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind)) + unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * UState.t * Decl_kinds.goal_kind)) val get_current_context : unit -> Evd.evar_map * Environ.env val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types @@ -6113,9 +6121,9 @@ end module Vernacstate : sig - type t = { (* TODO: inline records in OCaml 4.03 *) + type t = { system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) + proof : Proof_global.t; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) } @@ -7,6 +7,10 @@ Notations right (e.g. "( x ; .. ; y ; z )") now supported. - Notations with a specific level for the leftmost nonterminal, when printing-only, are supported. +- When several notations are available for the same expression, + priority is given to latest notations defined in the scopes being + opened rather than to the latest notations defined independently of + whether they are in an opened scope or not. Tactics @@ -22,9 +26,22 @@ Tactics contain proofs. Vernacular Commands + - The deprecated Coercion Local, Open Local Scope, Notation Local syntax was removed. Use Local as a prefix instead. +Universes + +- Qualified naming of global universes now works like other namespaced + objects (e.g. constants), with a separate namespace, inside and across + module and library boundaries. Global universe names introduced in an + inductive / constant / Let declaration get qualified with the name of + the declaration. + +Checker + +- The checker now accepts filenames in addition to logical paths. + Changes from 8.7+beta2 to 8.7.0 =============================== @@ -43,7 +43,7 @@ WHAT DO YOU NEED ? - a C compiler - for Coqide, the Lablgtk development files, and the GTK libraries - incuding gtksourceview, see INSTALL.ide for more details + including gtksourceview, see INSTALL.ide for more details Opam (https://opam.ocaml.org/) is recommended to install ocaml and the corresponding packages. diff --git a/Makefile.dev b/Makefile.dev index dc4ded397..d2a1e9235 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -98,7 +98,7 @@ pluginsopt: $(PLUGINSOPT) pluginsbyte: $(PLUGINS) # This should build all the ocaml code but not (most of) the .v files -coqocaml: tools coqbinaries pluginsopt coqide printers bin/votour +coqocaml: tools coqbinaries $(PLUGINSCMO:.cmo=$(DYNOBJ)) coqide printers bin/votour .PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml diff --git a/checker/analyze.ml b/checker/analyze.ml index df75d5b93..7047d8a14 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -55,6 +55,55 @@ let magic_number = "\132\149\166\190" (** Memory reification *) +module LargeArray : +sig + type 'a t + val empty : 'a t + val length : 'a t -> int + val make : int -> 'a -> 'a t + val get : 'a t -> int -> 'a + val set : 'a t -> int -> 'a -> unit +end = +struct + + let max_length = Sys.max_array_length + + type 'a t = 'a array array * 'a array + (** Invariants: + - All subarrays of the left array have length [max_length]. + - The right array has length < [max_length]. + *) + + let empty = [||], [||] + + let length (vl, vr) = + (max_length * Array.length vl) + Array.length vr + + let make n x = + let k = n / max_length in + let r = n mod max_length in + let vl = Array.init k (fun _ -> Array.make max_length x) in + let vr = Array.make r x in + (vl, vr) + + let get (vl, vr) n = + let k = n / max_length in + let r = n mod max_length in + let len = Array.length vl in + if k < len then vl.(k).(r) + else if k == len then vr.(r) + else invalid_arg "index out of bounds" + + let set (vl, vr) n x = + let k = n / max_length in + let r = n mod max_length in + let len = Array.length vl in + if k < len then vl.(k).(r) <- x + else if k == len then vr.(r) <- x + else invalid_arg "index out of bounds" + +end + type repr = | RInt of int | RBlock of (int * int) (* tag × len *) @@ -82,7 +131,7 @@ end module type S = sig type input - val parse : input -> (data * obj array) + val parse : input -> (data * obj LargeArray.t) end module Make(M : Input) = @@ -261,7 +310,7 @@ let parse_object chan = let parse chan = let (magic, len, _, _, size) = parse_header chan in let () = assert (magic = magic_number) in - let memory = Array.make size (Struct ((-1), [||])) in + let memory = LargeArray.make size (Struct ((-1), [||])) in let current_object = ref 0 in let fill_obj = function | RPointer n -> @@ -272,7 +321,7 @@ let parse chan = data, None | RString s -> let data = Ptr !current_object in - let () = memory.(!current_object) <- String s in + let () = LargeArray.set memory !current_object (String s) in let () = incr current_object in data, None | RBlock (tag, 0) -> @@ -282,7 +331,7 @@ let parse chan = | RBlock (tag, len) -> let data = Ptr !current_object in let nblock = Array.make len (Atm (-1)) in - let () = memory.(!current_object) <- Struct (tag, nblock) in + let () = LargeArray.set memory !current_object (Struct (tag, nblock)) in let () = incr current_object in data, Some nblock | RCode addr -> @@ -343,3 +392,32 @@ module PString = Make(IString) let parse_channel = PChannel.parse let parse_string s = PString.parse (s, ref 0) + +let instantiate (p, mem) = + let len = LargeArray.length mem in + let ans = LargeArray.make len (Obj.repr 0) in + (** First pass: initialize the subobjects *) + for i = 0 to len - 1 do + let obj = match LargeArray.get mem i with + | Struct (tag, blk) -> Obj.new_block tag (Array.length blk) + | String str -> Obj.repr str + in + LargeArray.set ans i obj + done; + let get_data = function + | Int n -> Obj.repr n + | Ptr p -> LargeArray.get ans p + | Atm tag -> Obj.new_block tag 0 + | Fun _ -> assert false (** We shouldn't serialize closures *) + in + (** Second pass: set the pointers *) + for i = 0 to len - 1 do + match LargeArray.get mem i with + | Struct (_, blk) -> + let obj = LargeArray.get ans i in + for k = 0 to Array.length blk - 1 do + Obj.set_field obj k (get_data blk.(k)) + done + | String _ -> () + done; + get_data p diff --git a/checker/analyze.mli b/checker/analyze.mli index 42efcf01d..9c837643f 100644 --- a/checker/analyze.mli +++ b/checker/analyze.mli @@ -8,8 +8,20 @@ type obj = | Struct of int * data array (* tag × data *) | String of string -val parse_channel : in_channel -> (data * obj array) -val parse_string : string -> (data * obj array) +module LargeArray : +sig + type 'a t + val empty : 'a t + val length : 'a t -> int + val make : int -> 'a -> 'a t + val get : 'a t -> int -> 'a + val set : 'a t -> int -> 'a -> unit +end +(** A data structure similar to arrays but allowing to overcome the 2^22 length + limitation on 32-bit architecture. *) + +val parse_channel : in_channel -> (data * obj LargeArray.t) +val parse_string : string -> (data * obj LargeArray.t) (** {6 Functorized version} *) @@ -26,10 +38,13 @@ end module type S = sig type input - val parse : input -> (data * obj array) + val parse : input -> (data * obj LargeArray.t) (** Return the entry point and the reification of the memory out of a marshalled structure. *) end module Make (M : Input) : S with type input = M.t (** Functorized version of the previous code. *) + +val instantiate : data * obj LargeArray.t -> Obj.t +(** Create the OCaml object out of the reified representation. *) diff --git a/checker/check.ml b/checker/check.ml index 180ca1ece..82341ad9b 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -22,6 +22,11 @@ let extend_dirpath p id = DirPath.make (id :: DirPath.repr p) type section_path = { dirpath : string list ; basename : string } + +type object_file = +| PhysicalFile of CUnix.physical_path +| LogicalFile of section_path + let dir_of_path p = DirPath.make (List.map Id.of_string p.dirpath) let path_of_dirpath dir = @@ -69,11 +74,6 @@ let libraries_table = ref LibraryMap.empty let find_library dir = LibraryMap.find dir !libraries_table -let try_find_library dir = - try find_library dir - with Not_found -> - user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir))) - let library_full_filename dir = (find_library dir).library_filename (* If a library is loaded several time, then the first occurrence must @@ -129,8 +129,6 @@ type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) -let get_load_paths () = fst !load_paths - (* Hints to partially detects if two paths refer to the same repertory *) let rec remove_path_dot p = let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) @@ -227,13 +225,8 @@ let locate_absolute_library dir = let locate_qualified_library qid = try - let loadpath = - (* Search library in loadpath *) - if qid.dirpath=[] then get_load_paths () - else - (* we assume qid is an absolute dirpath *) - load_paths_of_dir_path (dir_of_path qid) - in + (* we assume qid is an absolute dirpath *) + let loadpath = load_paths_of_dir_path (dir_of_path qid) in if loadpath = [] then raise LibUnmappedDir; let name = qid.basename^".vo" in let path, file = System.where_in_path loadpath name in @@ -263,7 +256,17 @@ let try_locate_absolute_library dir = | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir) | LibNotFound -> error_lib_not_found (path_of_dirpath dir) -let try_locate_qualified_library qid = +let try_locate_qualified_library lib = match lib with +| PhysicalFile f -> + let () = + if not (System.file_exists_respecting_case "" f) then + error_lib_not_found { dirpath = []; basename = f; } + in + let dir = Filename.dirname f in + let base = Filename.chop_extension (Filename.basename f) in + let dir = extend_dirpath (find_logical_path dir) (Id.of_string base) in + (dir, f) +| LogicalFile qid -> try locate_qualified_library qid with @@ -298,18 +301,27 @@ let name_clash_message dir mdir f = (* Dependency graph *) let depgraph = ref LibraryMap.empty +let marshal_in_segment f ch = + try + let stop = input_binary_int ch in + let v = Analyze.instantiate (Analyze.parse_channel ch) in + let digest = Digest.input ch in + Obj.obj v, stop, digest + with _ -> + user_err (str "Corrupted file " ++ quote (str f)) + let intern_from_file (dir, f) = Flags.if_verbose chk_pp (str"[intern "++str f++str" ..."); let (sd,md,table,opaque_csts,digest) = try let ch = System.with_magic_number_check raw_intern_library f in - let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in - let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in - let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in - let (discharging:'a option), _, _ = System.marshal_in_segment f ch in - let (tasks:'a option), _, _ = System.marshal_in_segment f ch in + let (sd:Cic.summary_disk), _, digest = marshal_in_segment f ch in + let (md:Cic.library_disk), _, digest = marshal_in_segment f ch in + let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in + let (discharging:'a option), _, _ = marshal_in_segment f ch in + let (tasks:'a option), _, _ = marshal_in_segment f ch in let (table:Cic.opaque_table), pos, checksum = - System.marshal_in_segment f ch in + marshal_in_segment f ch in (* Verification of the final checksum *) let () = close_in ch in let ch = open_in_bin f in @@ -412,9 +424,3 @@ let recheck_library ~norec ~admit ~check = (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); List.iter (check_one_lib nochk) needed; Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked") - -open Printf - -let mem s = - let m = try_find_library s in - h 0 (str (sprintf "%dk" (CObj.size_kb m))) diff --git a/checker/check.mli b/checker/check.mli new file mode 100644 index 000000000..28ae385b5 --- /dev/null +++ b/checker/check.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open CUnix +open Names + +type section_path = { + dirpath : string list; + basename : string; +} + +type object_file = +| PhysicalFile of physical_path +| LogicalFile of section_path + +type logical_path = DirPath.t + +val default_root_prefix : DirPath.t + +val add_load_path : physical_path * logical_path -> unit + +val recheck_library : + norec:object_file list -> + admit:object_file list -> + check:object_file list -> unit diff --git a/checker/check.mllib b/checker/check.mllib index 488507a13..f79ba66e3 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,5 +1,6 @@ Coq_config +Analyze Hook Terminal Canary diff --git a/checker/checker.ml b/checker/checker.ml index e960a55fd..fee31b667 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -40,9 +40,10 @@ let dirpath_of_string s = [] -> Check.default_root_prefix | dir -> DirPath.make (List.map Id.of_string dir) let path_of_string s = - match parse_dir s with + if Filename.check_suffix s ".vo" then PhysicalFile s + else match parse_dir s with [] -> invalid_arg "path_of_string" - | l::dir -> {dirpath=dir; basename=l} + | l::dir -> LogicalFile {dirpath=dir; basename=l} let ( / ) = Filename.concat @@ -95,17 +96,13 @@ let add_rec_path ~unix_path ~coq_root = (* By the option -include -I or -R of the command line *) let includes = ref [] -let push_include (s, alias) = includes := (s,alias,false) :: !includes -let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes +let push_include (s, alias) = includes := (s,alias) :: !includes let set_default_include d = push_include (d, Check.default_root_prefix) let set_include d p = let p = dirpath_of_string p in push_include (d,p) -let set_rec_include d p = - let p = dirpath_of_string p in - push_rec_include(d,p) (* Initializes the LoadPath *) let init_load_path () = @@ -131,8 +128,7 @@ let init_load_path () = add_path ~unix_path:"." ~coq_root:Check.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter - (fun (unix_path, coq_root, reci) -> - if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root) + (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root) (List.rev !includes); includes := [] @@ -144,15 +140,15 @@ let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet let engage () = Safe_typing.set_engagement (!impredicative_set) -let admit_list = ref ([] : section_path list) +let admit_list = ref ([] : object_file list) let add_admit s = admit_list := path_of_string s :: !admit_list -let norec_list = ref ([] : section_path list) +let norec_list = ref ([] : object_file list) let add_norec s = norec_list := path_of_string s :: !norec_list -let compile_list = ref ([] : section_path list) +let compile_list = ref ([] : object_file list) let add_compile s = compile_list := path_of_string s :: !compile_list @@ -178,7 +174,9 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -R dir coqdir map physical dir to logical coqdir\ +" -Q dir coqdir map physical dir to logical coqdir\ +\n -R dir coqdir synonymous for -Q\ +\n\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ @@ -310,6 +308,9 @@ let explain_exn = function report ()) | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) +let deprecated flag = + Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) + let parse_args argv = let rec parse = function | [] -> () @@ -323,12 +324,15 @@ let parse_args argv = Flags.coqlib_spec := true; parse rem - | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem + | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem | ("-I"|"-include") :: d :: "-as" :: [] -> usage () - | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem + | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem + | "-Q" :: d :: p :: rem -> set_include d p;parse rem + | "-Q" :: ([] | [_]) -> usage () + + | "-R" :: d :: p :: rem -> set_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem diff --git a/checker/closure.ml b/checker/closure.ml index 7982ffa7a..3a56bba01 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -279,7 +279,6 @@ and fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs | FProd of Name.t * fconstr * fconstr @@ -306,7 +305,6 @@ let update v1 (no,t) = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * projection | Zfix of fconstr * stack @@ -456,13 +454,10 @@ let rec to_constr constr_fun lfts v = | FFlex (ConstKey op) -> Const op | FInd op -> Ind op | FConstruct op -> Construct op - | FCase (ci,p,c,ve) -> - Case (ci, constr_fun lfts p, - constr_fun lfts c, - Array.map (constr_fun lfts) ve) - | FCaseT (ci,p,c,ve,e) -> (* TODO: enable sharing, cf FCLOS below ? *) - to_constr constr_fun lfts - {norm=Red;term=FCase(ci,mk_clos2 e p,c,mk_clos_vect e ve)} + | FCaseT (ci,p,c,ve,e) -> + let fp = mk_clos2 e p in + let fve = mk_clos_vect e ve in + Case (ci, constr_fun lfts fp, constr_fun lfts c, Array.map (constr_fun lfts) fve) | FFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in let ftys = Array.map (mk_clos e) tys in @@ -532,9 +527,6 @@ let rec zip m stk = match stk with | [] -> m | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s - | Zcase(ci,p,br)::s -> - let t = FCase(ci, p, m, br) in - zip {norm=neutr m.norm; term=t} s | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in zip {norm=neutr m.norm; term=t} s @@ -616,7 +608,7 @@ let rec get_args n tys f e stk = (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function - | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ + | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _ | Zshift _ | Zupdate _ as e) :: s -> e :: eta_expand_stack s | [] -> @@ -720,7 +712,6 @@ let rec knh info m stk = | FCLOS(t,e) -> knht info e t (zupdate m stk) | FLOCKED -> assert false | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) - | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk) | FCaseT(ci,p,t,br,env) -> knh info t (ZcaseT(ci,p,br,env)::zupdate m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with @@ -778,10 +769,6 @@ let rec knr info m stk = | None -> (set_norm m; (m,stk))) | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (depth, args, Zcase(ci,_,br)::s) -> - assert (ci.ci_npar>=0); - let rargs = drop_parameters depth ci.ci_npar args in - kni info br.(c-1) (rargs@s) | (depth, args, ZcaseT(ci,_,br,env)::s) -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in @@ -798,7 +785,7 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, (((Zcase _|ZcaseT _)::_) as stk')) -> + (_, args, (((ZcaseT _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) diff --git a/checker/closure.mli b/checker/closure.mli index 957cc4adb..02d8b22fa 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -98,7 +98,6 @@ type fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs | FProd of Name.t * fconstr * fconstr @@ -115,7 +114,6 @@ type fterm = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * projection | Zfix of fconstr * stack diff --git a/checker/reduction.ml b/checker/reduction.ml index 6d8783d7e..9b8eac04c 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -42,8 +42,8 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1, - (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) -> + | ((ZcaseT(c1,_,_,_))::s1, + (ZcaseT(c2,_,_,_))::s2) -> bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -78,8 +78,7 @@ let pure_stack lfts stk = (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,env),(l,pstk)) -> (l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk) - | (Zcase(ci,p,br),(l,pstk)) -> - (l,Zlcase(ci,l,p,br)::pstk)) in + ) in snd (pure_rec lfts stk) (****************************************************************************) @@ -243,7 +242,6 @@ let rec no_arg_available = function | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -256,7 +254,6 @@ let rec no_nth_arg_available n = function if n >= k then no_nth_arg_available (n-k) stk else false | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -266,13 +263,12 @@ let rec no_case_available = function | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk | Zproj (_,_,_) :: _ -> false - | Zcase _ :: _ -> false | ZcaseT _ :: _ -> false | Zfix _ :: _ -> true let in_whnf (t,stk) = match fterm_of t with - | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false + | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false | FLambda _ -> no_arg_available stk | FConstruct _ -> no_case_available stk | FCoFix _ -> no_case_available stk @@ -504,8 +500,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) - | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) - | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false (* In all other cases, terms are not convertible *) diff --git a/checker/votour.ml b/checker/votour.ml index b7c898232..77c9999c4 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -77,8 +77,8 @@ struct type obj = data - let memory = ref [||] - let sizes = ref [||] + let memory = ref LargeArray.empty + let sizes = ref LargeArray.empty (** size, in words *) let ws = Sys.word_size / 8 @@ -86,10 +86,10 @@ struct let rec init_size seen k = function | Int _ | Atm _ | Fun _ -> k 0 | Ptr p -> - if seen.(p) then k 0 + if LargeArray.get seen p then k 0 else - let () = seen.(p) <- true in - match (!memory).(p) with + let () = LargeArray.set seen p true in + match LargeArray.get !memory p with | Struct (tag, os) -> let len = Array.length os in let rec fold i accu k = @@ -97,30 +97,30 @@ struct else init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i) in - fold 0 1 (fun size -> let () = (!sizes).(p) <- size in k size) + fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size) | String s -> let size = 2 + (String.length s / ws) in - let () = (!sizes).(p) <- size in + let () = LargeArray.set !sizes p size in k size let size = function | Int _ | Atm _ | Fun _ -> 0 - | Ptr p -> (!sizes).(p) + | Ptr p -> LargeArray.get !sizes p let repr = function | Int i -> INT i | Atm t -> BLOCK (t, [||]) | Fun _ -> OTHER | Ptr p -> - match (!memory).(p) with + match LargeArray.get !memory p with | Struct (tag, os) -> BLOCK (tag, os) | String s -> STRING s let input ch = let obj, mem = parse_channel ch in let () = memory := mem in - let () = sizes := Array.make (Array.length mem) (-1) in - let seen = Array.make (Array.length mem) false in + let () = sizes := LargeArray.make (LargeArray.length mem) (-1) in + let seen = LargeArray.make (LargeArray.length mem) false in let () = init_size seen ignore obj in obj diff --git a/configure.ml b/configure.ml index 1ccb69106..c7d25bfc8 100644 --- a/configure.ml +++ b/configure.ml @@ -678,6 +678,22 @@ let operating_system, osdeplibs = else (try Sys.getenv "OS" with Not_found -> ""), osdeplibs +(** Num library *) + +(* since 4.06, the Num library is no longer distributed with OCaml (replaced + by Zarith) +*) + +let check_for_numlib () = + if caml_version_nums >= [4;6;0] then + let numlib,_ = tryrun camlexec.find ["query";"num"] in + match numlib with + | "" -> + die "Num library not installed, required for OCaml 4.06 or later" + | _ -> printf "You have the Num library installed. Good!\n" + +let numlib = + check_for_numlib () (** * lablgtk2 and CoqIDE *) @@ -711,11 +727,11 @@ let get_lablgtkdir () = else "", msg | None -> let msg = OCamlFind in - let d1,_ = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in + let d1,_ = tryrun camlexec.find ["query";"lablgtk2.sourceview2"] in if d1 <> "" && check_lablgtkdir msg d1 then d1, msg else (* In debian wheezy, ocamlfind knows only of lablgtk2 *) - let d2,_ = tryrun "ocamlfind" ["query";"lablgtk2"] in + let d2,_ = tryrun camlexec.find ["query";"lablgtk2"] in if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg else let msg = Stdlib in @@ -741,7 +757,7 @@ let check_lablgtk_version src dir = match src with if ans then printf "Warning: could not check the version of lablgtk2.\n"; (ans, "an unknown version") | OCamlFind -> - let v, _ = tryrun "ocamlfind" ["query"; "-format"; "%v"; "lablgtk2"] in + let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in try let vi = List.map s2i (numeric_prefix_list v) in ([2; 16] <= vi, v) @@ -798,7 +814,7 @@ let coqide_flags () = if !lablgtkdir <> "" then lablgtkincludes := sprintf "-I %S" !lablgtkdir; match coqide, arch with | "opt", "Darwin" when !Prefs.macintegration -> - let osxdir,_ = tryrun "ocamlfind" ["query";"lablgtkosx"] in + let osxdir,_ = tryrun camlexec.find ["query";"lablgtkosx"] in if osxdir <> "" then begin lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir; idearchflags := "lablgtkosx.cma"; diff --git a/default.nix b/default.nix index 9efabdbc2..5b5304e5a 100644 --- a/default.nix +++ b/default.nix @@ -42,13 +42,19 @@ stdenv.mkDerivation rec { # CoqIDE dependencies ocamlPackages.lablgtk - ] else []) ++ (if doCheck then [ + ] else []) ++ (if doCheck then # Test-suite dependencies + let inherit (stdenv.lib) versionAtLeast optional; in + /* ncurses is required to build an OCaml REPL */ + optional (!versionAtLeast ocaml.version "4.07") ncurses + ++ [ python rsync which + ] else []) ++ (if lib.inNixShell then [ + ocamlPackages.merlin ] else []); src = diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi index b88aa066d..48f1d3759 100644 --- a/dev/build/windows/patches_coq/coq_new.nsi +++ b/dev/build/windows/patches_coq/coq_new.nsi @@ -188,7 +188,7 @@ SectionEnd Section "Uninstall" ; Files and folders RMDir /r "$INSTDIR\bin" - RMDir /r "$INSTDIR\dev" + RMDir /r "$INSTDIR\doc" RMDir /r "$INSTDIR\etc" RMDir /r "$INSTDIR\lib" RMDir /r "$INSTDIR\libocaml" diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 4cfe0911b..fc3cef342 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -8,6 +8,4 @@ CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert opam install -j ${NJOBS} -y menhir git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} -# Patch to avoid the upper version limit -( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make ) - +( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 83e866e9f..79060e606 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -391,9 +391,11 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. \end{coq_example} -\noindent If an inductive constructor or type has arity 2 and the corresponding -string is enclosed by parenthesis, then the rest of the string is used -as infix constructor or type. +\noindent When extracting to {\ocaml}, if an inductive constructor or type +has arity 2 and the corresponding string is enclosed by parentheses, +and the string meets {\ocaml}'s lexical criteria for an infix symbol, +then the rest of the string is used as infix constructor or type. + \begin{coq_example} Extract Inductive list => "list" [ "[]" "(::)" ]. Extract Inductive prod => "(*)" [ "(,)" ]. diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 8b1fc7c8f..04a8a25c1 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -299,8 +299,9 @@ The following command-line options are recognized by the commands {\tt \section{Compiled libraries checker ({\tt coqchk})} -The {\tt coqchk} command takes a list of library paths as argument. -The corresponding compiled libraries (.vo files) are searched in the +The {\tt coqchk} command takes a list of library paths as argument, described +either by their logical name or by their physical filename, which must end in +{\tt .vo}. The corresponding compiled libraries (.vo files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type-checked. The effect of {\tt coqchk} is only to return with normal exit code in case of success, @@ -330,9 +331,12 @@ code, it cannot be guaranteed that the produced compiled libraries are correct. {\tt coqchk} is a standalone verifier, and thus it cannot be tainted by such malicious code. -Command-line options {\tt -I}, {\tt -R}, {\tt -where} and +Command-line options {\tt -Q}, {\tt -R}, {\tt -where} and {\tt -impredicative-set} are supported by {\tt coqchk} and have the -same meaning as for {\tt coqtop}. Extra options are: +same meaning as for {\tt coqtop}. As there is no notion of relative paths in +object files {\tt -Q} and {\tt -R} have exactly the same meaning. + +Extra options are: \begin{description} \item[{\tt -norec} {\em module}]\ % diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 5fb458588..7034c5608 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -311,10 +311,11 @@ A sequence is an expression of the following form: \begin{quote} {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$ \end{quote} -The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated -to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is -then applied and $v_2$ is applied to the goals generated by the -application of $v_1$. Sequence is left-associative. +The expression {\tacexpr}$_1$ is evaluated to $v_1$, which must be +a tactic value. The tactic $v_1$ is applied to the current goal, +possibly producing more goals. Then {\tacexpr}$_2$ is evaluated to +produce $v_2$, which must be a tactic value. The tactic $v_2$ is applied to +all the goals produced by the prior application. Sequence is associative. \subsubsection[Local application of tactics]{Local application of tactics\tacindex{[>\ldots$\mid$\ldots$\mid$\ldots]}\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}\index{Tacticals![> \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}} %\tacindex{; [ | ]} diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 75fac9454..a1a6a4391 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -285,8 +285,10 @@ universes and explicitly instantiate polymorphic definitions. \label{UniverseCmd}} In the monorphic case, this command declares a new global universe named -{\ident}. It supports the polymorphic flag only in sections, meaning the -universe quantification will be discharged on each section definition +{\ident}, which can be referred to using its qualified name as +well. Global universe names live in a separate namespace. The command +supports the polymorphic flag only in sections, meaning the universe +quantification will be discharged on each section definition independently. One cannot mix polymorphic and monomorphic declarations in the same section. diff --git a/engine/eConstr.ml b/engine/eConstr.ml index afdceae06..ea098902a 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -645,6 +645,24 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None +let universes_of_constr sigma c = + let open Univ in + let rec aux s c = + match kind sigma c with + | Const (_, u) | Ind (_, u) | Construct (_, u) -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Sort u -> + let sort = ESorts.kind sigma u in + if Sorts.is_small sort then s + else + let u = Sorts.univ_of_sort sort in + LSet.fold LSet.add (Universe.levels u) s + | Evar (k, args) -> + let concl = Evd.evar_concl (Evd.find sigma k) in + fold sigma aux (aux s (of_constr concl)) c + | _ -> fold sigma aux s c + in aux LSet.empty c + open Context open Environ diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e9ef302cf..3e6a13f70 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -201,6 +201,10 @@ val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a +(** Gather the universes transitively used in the term, including in the + type of evars appearing in it. *) +val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t + (** {6 Substitutions} *) module Vars : diff --git a/engine/termops.ml b/engine/termops.ml index 07fe90222..a71bdff31 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -288,6 +288,7 @@ let has_no_evar sigma = with Exit -> false let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd) +let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l let pr_evar_universe_context ctx = let open UState in diff --git a/engine/termops.mli b/engine/termops.mli index c9a530076..c1600abe8 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -271,6 +271,8 @@ val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool val is_Type : Evd.evar_map -> constr -> bool +val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference + (** Combinators on judgments *) val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment diff --git a/engine/uState.ml b/engine/uState.ml index f9a57cce2..c28e78f7d 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -263,13 +263,15 @@ let constrain_variables diff ctx = in { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } - -let pr_uctx_level uctx = +let reference_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Id.print (Option.get (Univ.LMap.find l map_rev).uname) + try Libnames.Ident (Loc.tag @@ Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> - Universes.pr_with_global_universes l + Universes.reference_of_level l + +let pr_uctx_level uctx l = + Libnames.pr_reference (reference_of_level uctx l) type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl @@ -430,7 +432,7 @@ let emit_side_effects eff u = let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = Universes.new_univ_level (Global.current_dirpath ()) in + let u = Universes.new_univ_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with diff --git a/engine/uState.mli b/engine/uState.mli index 16fba41e0..2c39e85f7 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -154,3 +154,4 @@ val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) val pr_uctx_level : t -> Univ.Level.t -> Pp.t +val reference_of_level : t -> Univ.Level.t -> Libnames.reference diff --git a/engine/universes.ml b/engine/universes.ml index d29e8777d..0250295fd 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -14,10 +14,37 @@ open Constr open Environ open Univ open Globnames - -let pr_with_global_universes l = - try Id.print (LMap.find l (snd (Global.global_universe_names ()))) - with Not_found -> Level.pr l +open Nametab + +let reference_of_level l = + match Level.name l with + | Some (d, n as na) -> + let qid = + try Nametab.shortest_qualid_of_universe na + with Not_found -> + let name = Id.of_string_soft (string_of_int n) in + Libnames.make_qualid d name + in Libnames.Qualid (Loc.tag @@ qid) + | None -> Libnames.Ident (Loc.tag @@ Id.of_string_soft (Level.to_string l)) + +let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l) + +(** Global universe information outside the kernel, to handle + polymorphic universe names in sections that have to be discharged. *) + +let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref) + +let add_global_universe u p = + match Level.name u with + | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map + | None -> () + +let is_polymorphic l = + match Level.name l with + | Some n -> + (try Nametab.UnivIdMap.find n !universe_map + with Not_found -> false) + | None -> false (** Local universe names of polymorphic references *) @@ -53,12 +80,14 @@ let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj rebuild_function = (fun x -> x); } let register_universe_binders ref ubinders = - (* Add the polymorphic (section) universes *) let open Names in - let ubinders = Id.Map.fold (fun id (poly,lvl) ubinders -> - if poly then Id.Map.add id lvl ubinders - else ubinders) - (fst (Global.global_universe_names ())) ubinders + (* Add the polymorphic (section) universes *) + let ubinders = UnivIdMap.fold (fun lvl poly ubinders -> + let qid = Nametab.shortest_qualid_of_universe lvl in + let level = Level.make (fst lvl) (snd lvl) in + if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders + else ubinders) + !universe_map ubinders in if not (Id.Map.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) @@ -236,14 +265,17 @@ let eq_constr_universes_proj env m n = res, !cstrs (* Generator of levels *) -let new_univ_level, set_remote_new_univ_level = +type universe_id = DirPath.t * int + +let new_univ_id, set_remote_new_univ_id = RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> Univ.Level.make (Global.current_dirpath ()) n) + ~build:(fun n -> Global.current_dirpath (), n) -let new_univ_level _ = new_univ_level () - (* Univ.Level.make db (new_univ_level ()) *) +let new_univ_level () = + let dp, id = new_univ_id () in + Univ.Level.make dp id -let fresh_level () = new_univ_level (Global.current_dirpath ()) +let fresh_level () = new_univ_level () (* TODO: remove *) let new_univ dp = Univ.Universe.make (new_univ_level dp) @@ -251,7 +283,7 @@ let new_Type dp = mkType (new_univ dp) let new_Type_sort dp = Type (new_univ dp) let fresh_universe_instance ctx = - let init _ = new_univ_level (Global.current_dirpath ()) in + let init _ = new_univ_level () in Instance.of_array (Array.init (AUContext.size ctx) init) let fresh_instance_from_context ctx = @@ -262,7 +294,7 @@ let fresh_instance_from_context ctx = let fresh_instance ctx = let ctx' = ref LSet.empty in let init _ = - let u = new_univ_level (Global.current_dirpath ()) in + let u = new_univ_level () in ctx' := LSet.add u !ctx'; u in let inst = Instance.of_array (Array.init (AUContext.size ctx) init) diff --git a/engine/universes.mli b/engine/universes.mli index 1401c4ee8..fc9278eb5 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -18,6 +18,13 @@ val is_set_minimization : unit -> bool (** Universes *) val pr_with_global_universes : Level.t -> Pp.t +val reference_of_level : Level.t -> Libnames.reference + +(** Global universe information outside the kernel, to handle + polymorphic universes in sections that have to be discharged. *) +val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit + +val is_polymorphic : Level.t -> bool (** Local universe name <-> level mapping *) @@ -40,14 +47,17 @@ val universe_binders_with_opt_names : Globnames.global_reference -> Univ.Level.t list -> univ_name_list option -> universe_binders (** The global universe counter *) -val set_remote_new_univ_level : Level.t RemoteCounter.installer +type universe_id = DirPath.t * int + +val set_remote_new_univ_id : universe_id RemoteCounter.installer (** Side-effecting functions creating new universe levels. *) -val new_univ_level : DirPath.t -> Level.t -val new_univ : DirPath.t -> Universe.t -val new_Type : DirPath.t -> types -val new_Type_sort : DirPath.t -> Sorts.t +val new_univ_id : unit -> universe_id +val new_univ_level : unit -> Level.t +val new_univ : unit -> Universe.t +val new_Type : unit -> types +val new_Type_sort : unit -> Sorts.t val new_global_univ : unit -> Universe.t in_universe_context_set val new_sort_in_family : Sorts.family -> Sorts.t diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e1df24f71..bc8debd02 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -383,7 +383,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat - (uninterp_cases_pattern_notations pat) + (uninterp_cases_pattern_notations scopes pat) with No_match -> lift (fun ?loc -> function | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) @@ -514,7 +514,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = try if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_ind_pattern scopes vars ind args - (uninterp_ind_pattern_notations ind) + (uninterp_ind_pattern_notations scopes ind) with No_match -> let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -734,7 +734,7 @@ let rec extern inctx scopes vars r = try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation scopes vars r'' (uninterp_notations r'') + extern_notation scopes vars r'' (uninterp_notations scopes r'') with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) diff --git a/interp/declare.ml b/interp/declare.ml index 1b4645aff..1aeb67afb 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -453,28 +453,95 @@ let input_universe_context : universe_context_decl -> Libobject.obj = let declare_universe_context poly ctx = Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) -(* Discharged or not *) -type universe_decl = polymorphic * Universes.universe_binders - -let cache_universes (p, l) = - let glob = Global.global_universe_names () in - let glob', ctx = - Id.Map.fold (fun id lev ((idl,lid),ctx) -> - ((Id.Map.add id (p, lev) idl, - Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) - l (glob, Univ.ContextSet.empty) +(** Global universes are not substitutive objects but global objects + bound at the *library* or *module* level. The polymorphic flag is + used to distinguish universes declared in polymorphic sections, which + are discharged and do not remain in scope. *) + +type universe_source = + | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) + | QualifiedUniv of Id.t (* global universe introduced by some global value *) + | UnqualifiedUniv (* other global universe *) + +type universe_decl = universe_source * Nametab.universe_id + +let add_universe src (dp, i) = + let level = Univ.Level.make dp i in + let optpoly = match src with + | BoundUniv -> Some true + | UnqualifiedUniv -> Some false + | QualifiedUniv _ -> None in - cache_universe_context (p, ctx); - Global.set_global_universe_names glob' + Option.iter (fun poly -> + let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in + Global.push_context_set poly ctx; + Universes.add_global_universe level poly; + if poly then Lib.add_section_context ctx) + optpoly -let input_universes : universe_decl -> Libobject.obj = +let check_exists sp = + let depth = sections_depth () in + let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in + if Nametab.exists_universe sp then + alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") + else () + +let qualify_univ src (sp,i as orig) = + match src with + | BoundUniv | UnqualifiedUniv -> orig + | QualifiedUniv l -> + let sp0, id = Libnames.repr_path sp in + let sp0 = DirPath.repr sp0 in + Libnames.make_path (DirPath.make (l::sp0)) id, i+1 + +let cache_universe ((sp, _), (src, id)) = + let sp, i = qualify_univ src (sp,1) in + let () = check_exists sp in + let () = Nametab.push_universe (Nametab.Until i) sp id in + add_universe src id + +let load_universe i ((sp, _), (src, id)) = + let sp, i = qualify_univ src (sp,i) in + let () = Nametab.push_universe (Nametab.Until i) sp id in + add_universe src id + +let open_universe i ((sp, _), (src, id)) = + let sp, i = qualify_univ src (sp,i) in + let () = Nametab.push_universe (Nametab.Exactly i) sp id in + () + +let discharge_universe = function + | _, (BoundUniv, _) -> None + | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x + +let input_universe : 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) } + cache_function = cache_universe; + load_function = load_universe; + open_function = open_universe; + discharge_function = discharge_universe; + subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a); + classify_function = (fun a -> Substitute a) } + +let declare_univ_binders gr pl = + if Global.is_polymorphic gr then + Universes.register_universe_binders gr pl + else + let l = match gr with + | ConstRef c -> Label.to_id @@ Constant.label c + | IndRef (c, _) -> Label.to_id @@ MutInd.label c + | VarRef id -> id + | ConstructRef _ -> + anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on an constructor reference") + in + Id.Map.iter (fun id lvl -> + match Univ.Level.name lvl with + | None -> () + | Some na -> + ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na)))) + pl let do_universe poly l = let in_section = Lib.sections_are_opened () in @@ -484,11 +551,14 @@ let do_universe poly l = (str"Cannot declare polymorphic universes outside sections") in let l = - List.fold_left (fun acc (l, id) -> - let lev = Universes.new_univ_level (Global.current_dirpath ()) in - Id.Map.add id lev acc) Id.Map.empty l + List.map (fun (l, id) -> + let lev = Universes.new_univ_id () in + (id, lev)) l in - Lib.add_anonymous_leaf (input_universes (poly, l)) + let src = if poly then BoundUniv else UnqualifiedUniv in + List.iter (fun (id,lev) -> + ignore(Lib.add_leaf id (input_universe (src, lev)))) + l type constraint_decl = polymorphic * Univ.constraints @@ -510,20 +580,15 @@ let input_constraints : constraint_decl -> Libobject.obj = discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } +let loc_of_glob_level = function + | Misctypes.GType (Misctypes.UNamed n) -> Libnames.loc_of_reference n + | _ -> None + let do_constraint poly l = - let open Misctypes in let u_of_id x = - match x with - | GProp -> Loc.tag (false, Univ.Level.prop) - | GSet -> Loc.tag (false, Univ.Level.set) - | GType None | GType (Some (_, Anonymous)) -> - user_err ~hdr:"Constraint" - (str "Cannot declare constraints on anonymous universes") - | GType (Some (loc, Name id)) -> - let names, _ = Global.global_universe_names () in - try loc, Id.Map.find id names - with Not_found -> - user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ Id.print id) + let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in + let loc = loc_of_glob_level x in + loc, Universes.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = @@ -541,7 +606,7 @@ let do_constraint poly l = ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in + let ploc, p, lu = u_of_id l and rloc, p', ru = u_of_id r in check_poly ?loc:ploc p rloc p'; Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l diff --git a/interp/declare.mli b/interp/declare.mli index d50d37368..f368d164e 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -80,13 +80,11 @@ val recursive_message : bool (** true = fixpoint *) -> val exists_name : Id.t -> bool - - (** Global universe contexts, names and constraints *) +val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit val do_universe : polymorphic -> Id.t Loc.located list -> unit -val do_constraint : polymorphic -> - (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> - unit +val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> + unit diff --git a/interp/notation.ml b/interp/notation.ml index f36294f73..94ce2a6c8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -526,15 +526,38 @@ let interp_notation ?loc ntn local_scopes = user_err ?loc (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") -let uninterp_notations c = - List.map_append (fun key -> keymap_find key !notations_key_table) - (glob_constr_keys c) - -let uninterp_cases_pattern_notations c = - keymap_find (cases_pattern_key c) !notations_key_table - -let uninterp_ind_pattern_notations ind = - keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table +let sort_notations scopes l = + let extract_scope l = function + | Scope sc -> List.partitioni (fun _i x -> + match x with + | NotationRule (Some sc',_),_,_ -> String.equal sc sc' + | _ -> false) l + | SingleNotation ntn -> List.partitioni (fun _i x -> + match x with + | NotationRule (None,ntn'),_,_ -> String.equal ntn ntn' + | _ -> false) l in + let rec aux l scopes = + if l == [] then [] (* shortcut *) else + match scopes with + | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes + | [] -> l in + aux l scopes + +let uninterp_notations scopes c = + let scopes = make_current_scopes scopes in + let keys = glob_constr_keys c in + let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in + sort_notations scopes maps + +let uninterp_cases_pattern_notations scopes c = + let scopes = make_current_scopes scopes in + let maps = keymap_find (cases_pattern_key c) !notations_key_table in + sort_notations scopes maps + +let uninterp_ind_pattern_notations scopes ind = + let scopes = make_current_scopes scopes in + let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in + sort_notations scopes maps let availability_of_notation (ntn_scope,ntn) scopes = let f scope = diff --git a/interp/notation.mli b/interp/notation.mli index 2066d346f..7d055571c 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -124,9 +124,9 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes -> type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : inductive -> notation_rule list +val uninterp_notations : local_scopes -> 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : local_scopes -> 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : local_scopes -> inductive -> notation_rule list (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 87484ccd5..33e961419 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -48,13 +48,19 @@ type 'a glob_sort_gen = | GProp (** representation of [Prop] literal *) | GSet (** representation of [Set] literal *) | GType of 'a (** representation of [Type] literal *) -type sort_info = Name.t Loc.located list -type level_info = Name.t Loc.located option -type glob_sort = sort_info glob_sort_gen +type 'a universe_kind = + | UAnonymous + | UUnknown + | UNamed of 'a + +type level_info = Libnames.reference universe_kind type glob_level = level_info glob_sort_gen type glob_constraint = glob_level * Univ.constraint_type * glob_level +type sort_info = (Libnames.reference * int) option list +type glob_sort = sort_info glob_sort_gen + (** A synonym of [Evar.t], also defined in Term *) type existential_key = Evar.t diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index e9c0e171a..4e7d6b218 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -87,7 +87,7 @@ let call_compiler ?profile:(profile=false) ml_filename = [] in let flambda_args = - if Coq_config.caml_version_nums >= [4;3;0] then + if Coq_config.caml_version_nums >= [4;3;0] && Dynlink.is_native then (* We play safe for now, and use the native compiler with -Oclassic, however it is likely that `native_compute` users can benefit from tweaking here. diff --git a/kernel/univ.ml b/kernel/univ.ml index 64afb95d5..8cf9028fb 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -192,6 +192,10 @@ module Level = struct let make m n = make (Level (n, Names.DirPath.hcons m)) + let name u = + match data u with + | Level (n, d) -> Some (d, n) + | _ -> None end (** Level maps *) @@ -337,19 +341,16 @@ struct returning [SuperSame] if they refer to the same level at potentially different increments or [SuperDiff] if they are different. The booleans indicate if the left expression is "smaller" than the right one in both cases. *) - let super (u,n as x) (v,n' as y) = + let super (u,n) (v,n') = let cmp = Level.compare u v in if Int.equal cmp 0 then SuperSame (n < n') else - match x, y with - | (l,0), (l',0) -> - let open RawLevel in - (match Level.data l, Level.data l' with - | Prop, Prop -> SuperSame false - | Prop, _ -> SuperSame true - | _, Prop -> SuperSame false - | _, _ -> SuperDiff cmp) - | _, _ -> SuperDiff cmp + let open RawLevel in + match Level.data u, n, Level.data v, n' with + | Prop, _, Prop, _ -> SuperSame (n < n') + | Prop, 0, _, _ -> SuperSame true + | _, _, Prop, 0 -> SuperSame false + | _, _, _, _ -> SuperDiff cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v @@ -499,6 +500,7 @@ struct let smartmap = List.smartmap + let map = List.map end type universe = Universe.t diff --git a/kernel/univ.mli b/kernel/univ.mli index c06ce2446..f74f29b2c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -45,6 +45,8 @@ sig val var : int -> t val var_index : t -> int option + + val name : t -> (Names.DirPath.t * int) option end type universe_level = Level.t @@ -121,6 +123,8 @@ sig val exists : (Level.t * int -> bool) -> t -> bool val for_all : (Level.t * int -> bool) -> t -> bool + + val map : (Level.t * int -> 'a) -> t -> 'a list end type universe = Universe.t diff --git a/library/global.ml b/library/global.ml index 43097dc5d..03d7612a4 100644 --- a/library/global.ml +++ b/library/global.ml @@ -8,7 +8,6 @@ open Names open Environ -open Decl_kinds (** We introduce here the global environment of the system, and we declare it as a synchronized table. *) @@ -231,18 +230,7 @@ let universes_of_global env r = let universes_of_global gr = universes_of_global (env ()) gr -(** Global universe names *) -type universe_names = - (polymorphic * Univ.Level.t) Id.Map.t * Id.t Univ.LMap.t - -let global_universes = - Summary.ref ~name:"Global universe names" - ((Id.Map.empty, Univ.LMap.empty) : universe_names) - -let global_universe_names () = !global_universes -let set_global_universe_names s = global_universes := s - -let is_polymorphic r = +let is_polymorphic r = let env = env() in match r with | VarRef id -> false diff --git a/library/global.mli b/library/global.mli index 51fe53181..1d68d1082 100644 --- a/library/global.mli +++ b/library/global.mli @@ -102,13 +102,6 @@ val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) -(** Global universe name <-> level mapping *) -type universe_names = - (Decl_kinds.polymorphic * Univ.Level.t) Id.Map.t * Id.t Univ.LMap.t - -val global_universe_names : unit -> universe_names -val set_global_universe_names : universe_names -> unit - (** {6 Compiled libraries } *) val start_library : DirPath.t -> ModPath.t diff --git a/library/nametab.ml b/library/nametab.ml index 222c4cedc..84225f863 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -302,6 +302,16 @@ module DirTab = Make(DirPath')(GlobDir) type dirtab = DirTab.t let the_dirtab = ref (DirTab.empty : dirtab) +type universe_id = DirPath.t * int + +module UnivIdEqual = +struct + type t = universe_id + let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' +end +module UnivTab = Make(FullPath)(UnivIdEqual) +type univtab = UnivTab.t +let the_univtab = ref (UnivTab.empty : univtab) (* Reversed name tables ***************************************************) @@ -318,6 +328,21 @@ let the_modrevtab = ref (MPmap.empty : mprevtab) type mptrevtab = full_path MPmap.t let the_modtyperevtab = ref (MPmap.empty : mptrevtab) +module UnivIdOrdered = +struct + type t = universe_id + let hash (d, i) = i + DirPath.hash d + let compare (d, i) (d', i') = + let c = Int.compare i i' in + if Int.equal c 0 then DirPath.compare d d' + else c +end + +module UnivIdMap = HMap.Make(UnivIdOrdered) + +type univrevtab = full_path UnivIdMap.t +let the_univrevtab = ref (UnivIdMap.empty : univrevtab) + (* Push functions *********************************************************) (* This is for permanent constructions (never discharged -- but with @@ -362,6 +387,11 @@ let push_dir vis dir dir_ref = | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab | _ -> () +(* This is for global universe names *) + +let push_universe vis sp univ = + the_univtab := UnivTab.push vis sp univ !the_univtab; + the_univrevtab := UnivIdMap.add univ sp !the_univrevtab (* Locate functions *******************************************************) @@ -382,6 +412,8 @@ let locate_syndef qid = match locate_extended qid with let locate_modtype qid = MPTab.locate qid !the_modtypetab let full_name_modtype qid = MPTab.user_name qid !the_modtypetab +let locate_universe qid = UnivTab.locate qid !the_univtab + let locate_dir qid = DirTab.locate qid !the_dirtab let locate_module qid = @@ -447,6 +479,8 @@ let exists_module = exists_dir let exists_modtype sp = MPTab.exists sp !the_modtypetab +let exists_universe kn = UnivTab.exists kn !the_univtab + (* Reverse locate functions ***********************************************) let path_of_global ref = @@ -469,6 +503,9 @@ let dirpath_of_module mp = let path_of_modtype mp = MPmap.find mp !the_modtyperevtab +let path_of_universe mp = + UnivIdMap.find mp !the_univrevtab + (* Shortest qualid functions **********************************************) let shortest_qualid_of_global ctx ref = @@ -490,6 +527,10 @@ let shortest_qualid_of_modtype kn = let sp = MPmap.find kn !the_modtyperevtab in MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab +let shortest_qualid_of_universe kn = + let sp = UnivIdMap.find kn !the_univrevtab in + UnivTab.shortest_qualid Id.Set.empty sp !the_univtab + let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> @@ -508,24 +549,28 @@ let global_inductive r = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * mptab - * globrevtab * mprevtab * mptrevtab +type frozen = ccitab * dirtab * mptab * univtab + * globrevtab * mprevtab * mptrevtab * univrevtab let freeze _ : frozen = !the_ccitab, !the_dirtab, !the_modtypetab, + !the_univtab, !the_globrevtab, !the_modrevtab, - !the_modtyperevtab + !the_modtyperevtab, + !the_univrevtab -let unfreeze (ccit,dirt,mtyt,globr,modr,mtyr) = +let unfreeze (ccit,dirt,mtyt,univt,globr,modr,mtyr,univr) = the_ccitab := ccit; the_dirtab := dirt; the_modtypetab := mtyt; + the_univtab := univt; the_globrevtab := globr; the_modrevtab := modr; - the_modtyperevtab := mtyr + the_modtyperevtab := mtyr; + the_univrevtab := univr let _ = Summary.declare_summary "names" diff --git a/library/nametab.mli b/library/nametab.mli index c02447a7c..77fafa100 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -78,6 +78,12 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit +type universe_id = DirPath.t * int + +module UnivIdMap : CMap.ExtS with type key = universe_id + +val push_universe : visibility -> full_path -> universe_id -> unit + (** {6 The following functions perform globalization of qualified names } *) (** These functions globalize a (partially) qualified name or fail with @@ -91,6 +97,7 @@ val locate_modtype : qualid -> ModPath.t val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> ModPath.t val locate_section : qualid -> DirPath.t +val locate_universe : qualid -> universe_id (** These functions globalize user-level references into global references, like [locate] and co, but raise a nice error message @@ -119,6 +126,7 @@ val exists_modtype : full_path -> bool val exists_dir : DirPath.t -> bool val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_universe : full_path -> bool (** {6 These functions locate qualids into full user names } *) @@ -138,6 +146,10 @@ val path_of_global : global_reference -> full_path val dirpath_of_module : ModPath.t -> DirPath.t val path_of_modtype : ModPath.t -> full_path +(** A universe_id might not be registered with a corresponding user name. + @raise Not_found if the universe was not introduced by the user. *) +val path_of_universe : universe_id -> full_path + (** Returns in particular the dirpath or the basename of the full path associated to global reference *) @@ -158,6 +170,7 @@ val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ModPath.t -> qualid val shortest_qualid_of_module : ModPath.t -> qualid +val shortest_qualid_of_universe : universe_id -> qualid (** Deprecated synonyms *) diff --git a/man/coqchk.1 b/man/coqchk.1 index 76a7cfc5d..f9241c0d4 100644 --- a/man/coqchk.1 +++ b/man/coqchk.1 @@ -23,7 +23,7 @@ library was not found, corrupted content, type-checking failure, etc. .IR modules \& is a list of modules to be checked. Modules can be referred to by a -short or qualified name. +short or qualified logical name, or by their filename. .SH OPTIONS @@ -34,13 +34,17 @@ add directory in the include path .TP -.BI \-R \ dir\ coqdir -recursively map physical +.BI \-Q \ dir\ coqdir +map physical .I dir to logical .I coqdir .TP +.BI \-R \ dir\ coqdir +synonymous for -Q + +.TP .BI \-silent makes coqchk less verbose. diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 7e5933cea..0cf96d487 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -155,9 +155,15 @@ GEXTEND Gram | "Type" -> Sorts.InType ] ] ; + universe_expr: + [ [ id = global; "+"; n = natural -> Some (id,n) + | id = global -> Some (id,0) + | "_" -> None + ] ] + ; universe: - [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids - | id = name -> [id] + [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> ids + | u = universe_expr -> [u] ] ] ; lconstr: @@ -307,8 +313,9 @@ GEXTEND Gram universe_level: [ [ "Set" -> GSet | "Prop" -> GProp - | "Type" -> GType None - | id = name -> GType (Some id) + | "Type" -> GType UUnknown + | "_" -> GType UAnonymous + | id = global -> GType (UNamed id) ] ] ; fix_constr: diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 9cbc3fd71..5d0f9c167 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -100,11 +100,41 @@ let pp_global k r = str (str_global k r) let pp_modname mp = str (Common.pp_module mp) +(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *) + +let infix_symbols = + ['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ] +let operator_chars = + [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ] + +(* infix ops in OCaml, but disallowed by preceding grammar *) + +let builtin_infixes = + [ "::" ; "," ] + +let substring_all_opchars s start stop = + let rec check_char i = + if i >= stop then true + else + List.mem s.[i] operator_chars && check_char (i+1) + in + check_char start + let is_infix r = is_inline_custom r && (let s = find_custom r in - let l = String.length s in - l >= 2 && s.[0] == '(' && s.[l-1] == ')') + let len = String.length s in + len >= 3 && + (* parenthesized *) + (s.[0] == '(' && s.[len-1] == ')' && + let inparens = String.trim (String.sub s 1 (len - 2)) in + let inparens_len = String.length inparens in + (* either, begins with infix symbol, any remainder is all operator chars *) + (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) || + (* or, starts with #, at least one more char, all are operator chars *) + (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) || + (* or, is an OCaml built-in infix *) + (List.mem inparens builtin_infixes))) let get_infix r = let s = find_custom r in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 1a8ec6d6f..14b79d73e 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1380,13 +1380,38 @@ and tactic_of_value ist vle = extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) - | VFun (_, _, _,vars,_) -> - let numargs = List.length vars in - Tacticals.New.tclZEROMSG - (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ - Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ - Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ - pr_enum Name.print vars ++ Pp.str ".") + | VFun (appl,_,vmap,vars,_) -> + let tactic_nm = + match appl with + UnnamedAppl -> "An unnamed user-defined tactic" + | GlbAppl apps -> + let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in + match nms with + [] -> assert false + | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) + in + let numargs = List.length vars in + let givenargs = + List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in + let numgiven = List.length givenargs in + Tacticals.New.tclZEROMSG + (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++ + (match numargs with + 0 -> assert false + | 1 -> + Pp.str "There is a missing argument for variable " ++ + (Name.print (List.hd vars)) + | _ -> Pp.str "There are missing arguments for variables " ++ + pr_enum Name.print vars) ++ Pp.pr_comma () ++ + match numgiven with + 0 -> + Pp.str "no arguments at all were provided." + | 1 -> + Pp.str "an argument was provided for variable " ++ + Pp.str (List.hd givenargs) ++ Pp.str "." + | _ -> + Pp.str "arguments were provided for variables " ++ + pr_enum Pp.str givenargs ++ Pp.str ".") | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 49ccb468c..387a52514 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -149,7 +149,7 @@ let open_in f = match read_key_elem inch with | None -> () | Some (key,elem) -> - Table.add htbl key elem ; + Table.replace htbl key elem ; xload () in try (* Locking of the (whole) file while reading *) @@ -195,7 +195,7 @@ let add t k e = else let fd = descr_of_out_channel outch in begin - Table.add tbl k e ; + Table.replace tbl k e ; do_under_lock Write fd (fun _ -> Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 337510ef1..0d491d92b 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -155,7 +155,7 @@ let mk_list univ typ l = loop l let mk_plist = - let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in + let type1lev = Universes.new_univ_level () in fun l -> mk_list type1lev mkProp l let mk_list = mk_list Univ.Level.set diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0d1e401d9..6527ba935 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -414,15 +414,17 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) +let detype_universe sigma u = + let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in + Univ.Universe.map fn u + let detype_sort sigma = function | Prop Null -> GProp | Prop Pos -> GSet | Type u -> GType (if !print_universes - then - let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in - [Loc.tag @@ Name.mk_name (Id.of_string_soft u)] + then detype_universe sigma u else []) type binder_kind = BProd | BLambda | BLetIn @@ -434,8 +436,8 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in - GType (Some (Loc.tag @@ Name.mk_name (Id.of_string_soft l))) + let l = Termops.reference_of_level sigma l in + GType (UNamed l) let detype_instance sigma l = let l = EInstance.kind sigma l in diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index bc563b46d..f0cb8fd1f 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,8 @@ let smartmap_cast_type f c = let glob_sort_eq g1 g2 = match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true -| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2 +| GType l1, GType l2 -> + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 | _ -> false let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 00c254dbe..b930c5db8 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -177,61 +177,77 @@ let _ = optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) -let interp_known_universe_level evd id = + +let interp_known_universe_level evd r = + let loc, qid = Libnames.qualid_of_reference r in try - let level = Evd.universe_of_name evd id in - level + match r with + | Libnames.Ident (loc, id) -> Evd.universe_of_name evd id + | Libnames.Qualid _ -> raise Not_found with Not_found -> - let names, _ = Global.global_universe_names () in - snd (Id.Map.find id names) - -let interp_universe_level_name ~anon_rigidity evd (loc, s) = - match s with - | Anonymous -> - new_univ_level_variable ?loc anon_rigidity evd - | Name id -> - let s = Id.to_string id in - if CString.string_contains ~where:s ~what:"." then - match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") - | n :: dp -> - let num = int_of_string n in - let dp = DirPath.make (List.map Id.of_string dp) in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - else - try evd, interp_known_universe_level evd id - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc ~name:id univ_rigid evd - else user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) + let univ, k = Nametab.locate_universe qid in + Univ.Level.make univ k + +let interp_universe_level_name ~anon_rigidity evd r = + try evd, interp_known_universe_level evd r + with Not_found -> + match r with (* Qualified generated name *) + | Libnames.Qualid (loc, qid) -> + let dp, i = Libnames.repr_qualid qid in + let num = + try int_of_string (Id.to_string i) + with Failure _ -> + user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r)) + in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level + | Libnames.Ident (loc, id) -> (* Undeclared *) + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:id univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in evd, Univ.Universe.make l | l -> - List.fold_left (fun (evd, u) l -> - (* [univ_flexible_alg] can produce algebraic universes in terms *) - let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in - (evd', Univ.sup u (Univ.Universe.make l))) + List.fold_left (fun (evd, u) l -> + let evd', u' = + match l with + | Some (l,n) -> + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let anon_rigidity = univ_flexible in + let evd', l = interp_universe_level_name ~anon_rigidity evd l in + let u' = Univ.Universe.make l in + (match n with + | 0 -> evd', u' + | 1 -> evd', Univ.Universe.super u' + | _ -> + user_err ?loc ~hdr:"interp_universe" + (Pp.(str "Cannot interpret universe increment +" ++ int n))) + | None -> + let evd, l = new_univ_level_variable ?loc univ_flexible evd in + evd, Univ.Universe.make l + in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l let interp_known_level_info ?loc evd = function - | None | Some (_, Anonymous) -> + | UUnknown | UAnonymous -> user_err ?loc ~hdr:"interp_known_level_info" (str "Anonymous universes not allowed here.") - | Some (loc, Name id) -> - try interp_known_universe_level evd id + | UNamed ref -> + try interp_known_universe_level evd ref with Not_found -> - user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Id.print id) + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) let interp_level_info ?loc evd : Misctypes.level_info -> _ = function - | None -> new_univ_level_variable ?loc univ_rigid evd - | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s) + | UUnknown -> new_univ_level_variable ?loc univ_rigid evd + | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd + | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index bce5710d6..2abbc389f 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -150,10 +150,15 @@ let tag_var = tag Tag.variable let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) + let pr_univ_expr = function + | Some (x,n) -> + pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + | None -> str"_" + let pr_univ l = match l with - | [_,x] -> Name.print x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")" + | [x] -> pr_univ_expr x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") pr_univ_expr l ++ str")" let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" @@ -166,8 +171,9 @@ let tag_var = tag Tag.variable let pr_glob_level = function | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") - | GType None -> tag_type (str "Type") - | GType (Some (_, u)) -> tag_type (Name.print u) + | GType UUnknown -> tag_type (str "Type") + | GType UAnonymous -> tag_type (str "_") + | GType (UNamed u) -> tag_type (pr_reference u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -192,8 +198,9 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | Some (_,u) -> Name.print u - | None -> tag_type (str "Type")) + | UNamed u -> pr_reference u + | UAnonymous -> tag_type (str "Type") + | UUnknown -> tag_type (str "_")) let pr_universe_instance l = pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l diff --git a/printing/printer.mli b/printing/printer.mli index 9e8622c6e..36ca1bdcc 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -186,8 +186,8 @@ val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t val pr_subgoal : int -> evar_map -> goal list -> Pp.t val pr_concl : int -> evar_map -> goal -> Pp.t -val pr_open_subgoals : proof:Proof.proof -> Pp.t -val pr_nth_open_subgoal : proof:Proof.proof -> int -> Pp.t +val pr_open_subgoals : proof:Proof.t -> Pp.t +val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t @@ -220,7 +220,7 @@ module ContextObjectMap : CMap.ExtS val pr_assumptionset : env -> types ContextObjectMap.t -> Pp.t -val pr_goal_by_id : proof:Proof.proof -> Id.t -> Pp.t +val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t type printer_pr = { pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; diff --git a/proofs/goal.mli b/proofs/goal.mli index ad968cdfb..37dd9d3c0 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -58,7 +58,7 @@ module V82 : sig (* Principal part of the progress tactical *) val progress : goal list Evd.sigma -> goal Evd.sigma -> bool - + (* Principal part of tclNOTSAMEGOAL *) val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c526ae000..31a73db04 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -140,7 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in Proof_global.discard_current (); - const, status, fst univs + const, status, univs with reraise -> let reraise = CErrors.push reraise in Proof_global.discard_current (); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index d676a0874..5a317a956 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -35,11 +35,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) val cook_proof : unit -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) (** {6 ... } *) (** [get_goal_context n] returns the context of the [n]th subgoal of @@ -74,7 +74,7 @@ val current_proof_statement : val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> - Proof.proof -> Proof.proof*bool + Proof.t -> Proof.t * bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current focused proof or raises a UserError if there is no focused proof or diff --git a/proofs/proof.ml b/proofs/proof.ml index 413b5fdd7..04e707cd6 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -98,7 +98,7 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k) (* Subpart of the type of proofs. It contains the parts of the proof which are under control of the undo mechanism *) -type proof = { +type t = { (* Current focused proofview *) proofview: Proofview.proofview; (* Entry for the proofview *) @@ -115,6 +115,8 @@ type proof = { initial_euctx : UState.t } +type proof = t + (*** General proof functions ***) let proof p = diff --git a/proofs/proof.mli b/proofs/proof.mli index 83777fc96..0b5e771ef 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -30,7 +30,9 @@ *) (* Type of a proof. *) -type proof +type t +type proof = t +[@@ocaml.deprecated "please use [Proof.t]"] (* Returns a stylised view of a proof for use by, for instance, ide-s. *) @@ -42,7 +44,7 @@ type proof shelf (the list of goals on the shelf), a representation of the given up goals (the list of the given up goals) and the underlying evar_map *) -val proof : proof -> +val proof : t -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Goal.goal list @@ -61,26 +63,26 @@ type 'a pre_goals = { (** List of the goals that have been given up *) } -val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) +val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) (*** General proof functions ***) -val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof -val dependent_start : Proofview.telescope -> proof -val initial_goals : proof -> (EConstr.constr * EConstr.types) list -val initial_euctx : proof -> UState.t +val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t +val dependent_start : Proofview.telescope -> t +val initial_goals : t -> (EConstr.constr * EConstr.types) list +val initial_euctx : t -> UState.t (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) -val is_done : proof -> bool +val is_done : t -> bool (* Like is_done, but this time it really means done (i.e. nothing left to do) *) -val is_complete : proof -> bool +val is_complete : t -> bool (* Returns the list of partial proofs to initial goals. *) -val partial_proof : proof -> EConstr.constr list +val partial_proof : t -> EConstr.constr list -val compact : proof -> proof +val compact : t -> t (* Returns the proofs (with their type) of the initial goals. Raises [UnfinishedProof] is some goals remain to be considered. @@ -91,7 +93,7 @@ exception UnfinishedProof exception HasShelvedGoals exception HasGivenUpGoals exception HasUnresolvedEvar -val return : proof -> Evd.evar_map +val return : t -> Evd.evar_map (*** Focusing actions ***) @@ -131,7 +133,7 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition (* focus command (focuses on the [i]th subgoal) *) (* spiwack: there could also, easily be a focus-on-a-range tactic, is there a need for it? *) -val focus : 'a focus_condition -> 'a -> int -> proof -> proof +val focus : 'a focus_condition -> 'a -> int -> t -> t exception FullyUnfocused exception CannotUnfocusThisWay @@ -147,59 +149,59 @@ exception NoSuchGoals of int * int Raises [FullyUnfocused] if the proof is not focused. Raises [CannotUnfocusThisWay] if the proof the unfocusing condition is not met. *) -val unfocus : 'a focus_kind -> proof -> unit -> proof +val unfocus : 'a focus_kind -> t -> unit -> t (* [unfocused p] returns [true] when [p] is fully unfocused. *) -val unfocused : proof -> bool +val unfocused : t -> bool (* [get_at_focus k] gets the information stored at the closest focus point of kind [k]. Raises [NoSuchFocus] if there is no focus point of kind [k]. *) exception NoSuchFocus -val get_at_focus : 'a focus_kind -> proof -> 'a +val get_at_focus : 'a focus_kind -> t -> 'a (* [is_last_focus k] check if the most recent focus is of kind [k] *) -val is_last_focus : 'a focus_kind -> proof -> bool +val is_last_focus : 'a focus_kind -> t -> bool (* returns [true] if there is no goal under focus. *) -val no_focused_goal : proof -> bool +val no_focused_goal : t -> bool (*** Tactics ***) (* the returned boolean signal whether an unsafe tactic has been used. In which case it is [false]. *) val run_tactic : Environ.env -> - unit Proofview.tactic -> proof -> proof*(bool*Proofview_monad.Info.tree) + unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) -val maximal_unfocus : 'a focus_kind -> proof -> proof +val maximal_unfocus : 'a focus_kind -> t -> t (*** Commands ***) -val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a +val in_proof : t -> (Evd.evar_map -> 'a) -> 'a (* Remove all the goals from the shelf and adds them at the end of the focused goals. *) -val unshelve : proof -> proof +val unshelve : t -> t -val pr_proof : proof -> Pp.t +val pr_proof : t -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig - val subgoals : proof -> Goal.goal list Evd.sigma + val subgoals : t -> Goal.goal list Evd.sigma [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] (* All the subgoals of the proof, including those which are not focused. *) - val background_subgoals : proof -> Goal.goal list Evd.sigma + val background_subgoals : t -> Goal.goal list Evd.sigma - val top_goal : proof -> Goal.goal Evd.sigma + val top_goal : t -> Goal.goal Evd.sigma (* returns the existential variable used to start the proof *) - val top_evars : proof -> Evar.t list + val top_evars : t -> Evar.t list (* Turns the unresolved evars into goals. Raises [UnfinishedProof] if there are still unsolved goals. *) - val grab_evars : proof -> proof + val grab_evars : t -> t (* Implements the Existential command *) - val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> proof + val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t end diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 4f575ab4b..214916331 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -25,8 +25,8 @@ let pr_bullet b = type behavior = { name : string; - put : proof -> t -> proof; - suggest: proof -> Pp.t + put : Proof.t -> t -> Proof.t; + suggest: Proof.t -> Pp.t } let behaviors = Hashtbl.create 4 @@ -110,7 +110,7 @@ module Strict = struct let push (b:t) pr = focus bullet_cond (b::get_bullets pr) 1 pr - let suggest_bullet (prf : proof): suggestion = + let suggest_bullet (prf : Proof.t): suggestion = if is_done prf then ProofFinished else if not (no_focused_goal prf) then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *) @@ -137,7 +137,7 @@ module Strict = struct in loop prf - let rec pop_until (prf : proof) bul : proof = + let rec pop_until (prf : Proof.t) bul : Proof.t = let prf', b = pop prf in if bullet_eq bul b then prf' else pop_until prf' bul diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index 9e924fec9..09fcabf50 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -12,8 +12,6 @@ (* *) (**********************************************************) -open Proof - type t = Vernacexpr.bullet (** A [behavior] is the data of a put function which @@ -22,8 +20,8 @@ type t = Vernacexpr.bullet with a name to identify the behavior. *) type behavior = { name : string; - put : proof -> t -> proof; - suggest: proof -> Pp.t + put : Proof.t -> t -> Proof.t; + suggest: Proof.t -> Pp.t } (** A registered behavior can then be accessed in Coq @@ -39,8 +37,8 @@ val register_behavior : behavior -> unit (** Handles focusing/defocusing with bullets: *) -val put : proof -> t -> proof -val suggest : proof -> Pp.t +val put : Proof.t -> t -> Proof.t +val suggest : Proof.t -> Pp.t (**********************************************************) (* *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index aa5621770..535ef2013 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -68,17 +68,16 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -90,12 +89,15 @@ type pstate = { terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Context.Named.t option; - proof : Proof.proof; + proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; universe_decl: Univdecls.universe_decl; } +type t = pstate list +type state = t + let make_terminator f = f let apply_terminator f = f @@ -330,7 +332,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -406,7 +407,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let entries = Future.map2 entry_fn fpl initial_goals in { id = pid; entries = entries; persistence = strength; - universes = (universes, binders) }, + universes }, fun pr_ending -> CEphemeron.get terminator pr_ending let return_proof ?(allow_partial=false) () = @@ -467,8 +468,6 @@ module V82 = struct pid, (goals, strength) end -type state = pstate list - let freeze ~marshallable = match marshallable with | `Yes -> diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index eed62f912..27e99f218 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -10,6 +10,10 @@ toplevel. In particular it defines the global proof environment. *) +type t +type state = t +[@@ocaml.deprecated "please use [Proof_global.t]"] + val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -21,7 +25,7 @@ val discard_current : unit -> unit val discard_all : unit -> unit exception NoCurrentProof -val give_me_the_proof : unit -> Proof.proof +val give_me_the_proof : unit -> Proof.t (** @raise NoCurrentProof when outside proof mode. *) val compact_the_proof : unit -> unit @@ -33,18 +37,17 @@ val compact_the_proof : unit -> unit (i.e. an proof ending command) and registers the appropriate values. *) type lemma_possible_guards = int list list -type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - proof_universes + UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -107,9 +110,9 @@ val get_open_goals : unit -> int no current proof. The return boolean is set to [false] if an unsafe tactic has been used. *) val with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof*'a) -> 'a + (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a val simple_with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit + (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Genarg.glob_generic_argument -> unit @@ -129,11 +132,10 @@ module V82 : sig Decl_kinds.goal_kind) end -type state -val freeze : marshallable:[`Yes | `No | `Shallow] -> state -val unfreeze : state -> unit -val proof_of_state : state -> Proof.proof -val copy_terminators : src:state -> tgt:state -> state +val freeze : marshallable:[`Yes | `No | `Shallow] -> t +val unfreeze : t -> unit +val proof_of_state : t -> Proof.t +val copy_terminators : src:t -> tgt:t -> t (**********************************************************) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 4662c5543..cd22a7183 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -58,7 +58,7 @@ module Make(T : Task) () = struct type request = Request of T.request type more_data = - | MoreDataUnivLevel of Univ.Level.t list + | MoreDataUnivLevel of Universes.universe_id list let slave_respond (Request r) = let res = T.perform r in @@ -169,8 +169,7 @@ module Make(T : Task) () = struct | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in let more_univs n = - CList.init n (fun _ -> - Universes.new_univ_level (Global.current_dirpath ())) in + CList.init n (fun _ -> Universes.new_univ_id ()) in let rec kill_if () = if not (Worker.is_alive proc) then () @@ -309,7 +308,7 @@ module Make(T : Task) () = struct Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x)); (* We ask master to allocate universe identifiers *) - Universes.set_remote_new_univ_level (bufferize (fun () -> + Universes.set_remote_new_univ_id (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with | MoreDataUnivLevel l -> l)); diff --git a/stm/stm.ml b/stm/stm.ml index ab44cc98b..8aa832da8 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -762,7 +762,7 @@ end = struct (* {{{ *) let fix_exn_ref = ref (fun x -> x) type proof_part = - Proof_global.state * Summary.frozen_bits (* only meta counters *) + Proof_global.t * Summary.frozen_bits (* only meta counters *) type partial_state = [ `Full of Vernacstate.t diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v index a96a13700..c069b2d9d 100644 --- a/test-suite/bugs/closed/4390.v +++ b/test-suite/bugs/closed/4390.v @@ -8,16 +8,16 @@ Universe i. End foo. End M. -Check Type@{i}. +Check Type@{M.i}. (* Succeeds *) Fail Check Type@{j}. (* Error: Undeclared universe: j *) -Definition foo@{j} : Type@{i} := Type@{j}. +Definition foo@{j} : Type@{M.i} := Type@{j}. (* ok *) End A. - +Import A. Import M. Set Universe Polymorphism. Fail Universes j. Monomorphic Universe j. diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out new file mode 100644 index 000000000..29d50775a --- /dev/null +++ b/test-suite/output/Extraction_infix.out @@ -0,0 +1,20 @@ +(** val test : foo **) + +let test = + (fun (b, p) -> bar) (True, False) +(** val test : foo **) + +let test = + True@@?False +(** val test : foo **) + +let test = + True#^^False +(** val test : foo **) + +let test = + True@?:::False +(** val test : foo **) + +let test = + True @?::: False diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v new file mode 100644 index 000000000..fe5926a36 --- /dev/null +++ b/test-suite/output/Extraction_infix.v @@ -0,0 +1,26 @@ +(* @herbelin's example for issue #6212 *) + +Require Import Extraction. +Inductive I := C : bool -> bool -> I. +Definition test := C true false. + +(* the parentheses around the function wrong signalled an infix operator *) + +Extract Inductive I => "foo" [ "(fun (b, p) -> bar)" ]. +Extraction test. + +(* some bonafide infix operators *) + +Extract Inductive I => "foo" [ "(@@?)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(#^^)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(@?:::)" ]. +Extraction test. + +(* allow whitespace around infix operator *) + +Extract Inductive I => "foo" [ "( @?::: )" ]. +Extraction test. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 7bcd7b041..2f0ee765d 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -64,7 +64,7 @@ The command has indeed failed with message: Cannot find where the recursive pattern starts. The command has indeed failed with message: Both ends of the recursive pattern are the same. -SUM (nat * nat) nat +(nat * nat + nat)%type : Set FST (0; 1) : Z @@ -72,7 +72,7 @@ Nil : forall A : Type, list A NIL : list nat : list nat -(false && I 3)%bool /\ I 6 +(false && I 3)%bool /\ (I 6)%bool : Prop [|1, 2, 3; 4, 5, 6|] : Z * Z * Z * (Z * Z * Z) diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fe6c05c39..413812ee1 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)). Section A. -Notation "! A" := (forall _:nat, A) (at level 60). +Notation "! A" := (forall _:nat, A) (at level 60) : type_scope. Check ! (0=0). Check forall n, n=0. @@ -194,9 +194,9 @@ Open Scope nat_scope. Coercion is_true := fun b => b=true. Coercion of_nat n := match n with 0 => true | _ => false end. -Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10). +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope. -Check (false && I 3)%bool /\ I 6. +Check (false && I 3)%bool /\ (I 6)%bool. (**********************************************************************) (* Check notations with several recursive patterns *) diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 1ec701ae8..a1028bda0 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -41,7 +41,7 @@ Notation plus2 n := (S(S(n))) match n with | nil => 2 | 0 :: _ => 2 -| list1 => 0 +| 1 :: nil => 0 | 1 :: _ :: _ => 2 | plus2 _ :: _ => 2 end @@ -84,3 +84,9 @@ a≡ : Set .α : Set +# a : .α => +# b : .α => +let res := 0 in +for i from 0 to a updating (res) +{{for j from 0 to b updating (res) {{S res}};; res}};; res + : .α -> .α -> .α diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index ceb29d1b9..4c3eaa0c7 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -70,6 +70,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* Note: does not work for pattern *) Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). +Open Scope nat_scope. Check fun f x => f x + S x. Open Scope list_scope. @@ -145,3 +146,24 @@ Check .a≡. Notation ".α" := nat. Check nat. Check .α. + +(* A test for #6304 *) + +Module M6304. +Notation "'for' m 'from' 0 'to' N 'updating' ( s1 ) {{ b }} ;; rest" := + (let s1 := + (fix rec(n: nat) := match n with + | 0 => s1 + | S m => let s1 := rec m in b + end) N + in rest) + (at level 20). + +Check fun (a b : nat) => + let res := 0 in + for i from 0 to a updating (res) {{ + for j from 0 to b updating (res) {{ S res }};; + res + }};; res. + +End M6304. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 6ef75dd13..1b5725275 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -128,3 +128,13 @@ return (1, 2, 3, 4) : nat *(1.2) : nat +[{0; 0}] + : list (list nat) +[{1; 2; 3}; + {4; 5; 6}; + {7; 8; 9}] + : list (list nat) +amatch = mmatch 0 (with 0 => 1| 1 => 2 end) + : unit +alist = [0; 1; 2] + : list nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 8c7bbe591..a8d6c97fb 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. (* Notations with variables bound both as a term and as a binder *) (* This is #4592 *) -Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)). +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. Check forall n:nat, {# n | 1 > n}. Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. @@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4). (* Test spacing in #5569 *) +Section S1. +Variable plus : nat -> nat -> nat. +Infix "+" := plus. Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. +End S1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). @@ -193,7 +197,59 @@ Check !!! (x y:nat), True. (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) -Notation "* x" := (id x) (only printing, at level 15, format "* x"). -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Section S2. +Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope. +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope. Check (((id 1) + 2) + 3). Check (id (1 + 2)). +End S2. + +(* Test printing of notations guided by scope *) + +Module A. + +Delimit Scope line_scope with line. +Notation "{ }" := nil (format "{ }") : line_scope. +Notation "{ x }" := (cons x nil) : line_scope. +Notation "{ x ; y ; .. ; z }" := (cons x (cons y .. (cons z nil) ..)) : line_scope. +Notation "[ ]" := nil (format "[ ]") : matx_scope. +Notation "[ l ]" := (cons l%line nil) : matx_scope. +Notation "[ l ; l' ; .. ; l'' ]" := (cons l%line (cons l'%line .. (cons l''%line nil) ..)) + (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope. + +Open Scope matx_scope. +Check [[0;0]]. +Check [[1;2;3];[4;5;6];[7;8;9]]. + +End A. + +(* Example by Beta Ziliani *) + +Require Import Lists.List. + +Module B. + +Import ListNotations. + +Delimit Scope pattern_scope with pattern. +Delimit Scope patterns_scope with patterns. + +Notation "a => b" := (a, b) (at level 201) : pattern_scope. +Notation "'with' p1 | .. | pn 'end'" := + ((cons p1%pattern (.. (cons pn%pattern nil) ..))) + (at level 91, p1 at level 210, pn at level 210) : patterns_scope. + +Definition mymatch (n:nat) (l : list (nat * nat)) := tt. +Arguments mymatch _ _%patterns. +Notation "'mmatch' n ls" := (mymatch n ls) (at level 0). + +Close Scope patterns_scope. +Close Scope pattern_scope. + +Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end. +Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *) + +Definition alist := [0;1;2]. +Print alist. + +End B. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index f69379a57..d6d410d1a 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -44,26 +44,45 @@ bar@{u} = nat bar is universe polymorphic foo@{u Top.17 v} = Type@{Top.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1, Top.17+1, v+1)} + : Type@{max(u+1,Top.17+1,v+1)} (* u Top.17 v |= *) foo is universe polymorphic -Monomorphic mono = Type@{u} - : Type@{u+1} -(* {u} |= *) +Monomorphic mono = Type@{mono.u} + : Type@{mono.u+1} +(* {mono.u} |= *) mono is not universe polymorphic +mono + : Type@{mono.u+1} +Type@{mono.u} + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +monomono + : Type@{MONOU+1} +mono.monomono + : Type@{mono.MONOU+1} +monomono + : Type@{MONOU+1} +mono + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +bobmorane = +let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff + : Type@{max(tt.u,ff.u)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} - : Type@{max(E+1, M+1, N+1)} + : Type@{max(E+1,M+1,N+1)} (* E M N |= *) foo is universe polymorphic foo@{Top.16 Top.17 Top.18} = Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16} - : Type@{max(Top.16+1, Top.17+1, Top.18+1)} + : Type@{max(Top.16+1,Top.17+1,Top.18+1)} (* Top.16 Top.17 Top.18 |= *) foo is universe polymorphic @@ -88,9 +107,10 @@ The command has indeed failed with message: This object does not support universe names. The command has indeed failed with message: Cannot enforce v < u because u < gU < gV < v -Monomorphic bind_univs.mono = Type@{u} - : Type@{u+1} -(* {u} |= *) +Monomorphic bind_univs.mono = +Type@{bind_univs.mono.u} + : Type@{bind_univs.mono.u+1} +(* {bind_univs.mono.u} |= *) bind_univs.mono is not universe polymorphic bind_univs.poly@{u} = Type@{u} @@ -99,12 +119,12 @@ bind_univs.poly@{u} = Type@{u} bind_univs.poly is universe polymorphic insec@{v} = Type@{u} -> Type@{v} - : Type@{max(u+1, v+1)} + : Type@{max(u+1,v+1)} (* v |= *) insec is universe polymorphic insec@{u v} = Type@{u} -> Type@{v} - : Type@{max(u+1, v+1)} + : Type@{max(u+1,v+1)} (* u v |= *) insec is universe polymorphic @@ -125,28 +145,28 @@ inmod@{u} = Type@{u} inmod is universe polymorphic Applied.infunct@{u v} = inmod@{u} -> Type@{v} - : Type@{max(u+1, v+1)} + : Type@{max(u+1,v+1)} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i} -(* i Top.33 Top.34 |= *) +axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i} +(* i Top.41 Top.42 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i} -(* i Top.33 Top.34 |= *) +axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i} +(* i Top.41 Top.42 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axbar -axfoo' : Type@{Top.36} -> Type@{i} +axfoo' : Type@{Top.44} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo' -axbar' : Type@{Top.36} -> Type@{i} +axbar' : Type@{Top.44} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 116d5e5e9..266d94ad9 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -1,6 +1,6 @@ Set Universe Polymorphism. Set Printing Universes. -Unset Strict Universe Declaration. +(* Unset Strict Universe Declaration. *) (* universe binders on inductive types and record projections *) Inductive Empty@{u} : Type@{u} := . @@ -25,14 +25,59 @@ Print wrap. Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed. Print bar. +Unset Strict Universe Declaration. (* The universes in the binder come first, then the extra universes in order of appearance. *) Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. Print foo. +Set Strict Universe Declaration. (* Binders even work with monomorphic definitions! *) Monomorphic Definition mono@{u} := Type@{u}. Print mono. +Check mono. +Check Type@{mono.u}. + +Module mono. + Fail Monomorphic Universe u. + Monomorphic Universe MONOU. + + Monomorphic Definition monomono := Type@{MONOU}. + Check monomono. +End mono. +Check mono.monomono. (* qualified MONOU *) +Import mono. +Check monomono. (* unqualified MONOU *) +Check mono. (* still qualified mono.u *) + +Monomorphic Constraint Set < Top.mono.u. + +Module mono2. + Monomorphic Universe u. +End mono2. + +Fail Monomorphic Definition mono2@{u} := Type@{u}. + +Module SecLet. + Unset Universe Polymorphism. + Section foo. + (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *) + Unset Strict Universe Declaration. + Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *) + Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *) + Definition bobmorane := tt -> ff. + End foo. + Print bobmorane. (* + bobmorane@{Top.15 Top.16 ff.u ff.v} = + let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff + : Type@{max(Top.15,ff.u)} + (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15 + ff.v < ff.u + *) + + bobmorane is universe polymorphic + *) +End SecLet. (* fun x x => foo is nonsense with local binders *) Fail Definition fo@{u u} := Type@{u}. @@ -61,7 +106,7 @@ Monomorphic Universes gU gV. Monomorphic Constraint gU < gV. Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat. (* Universe binders survive through compilation, sections and modules. *) -Require bind_univs. +Require TestSuite.bind_univs. Print bind_univs.mono. Print bind_univs.poly. diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index 172612405..7326f137c 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,20 +1,40 @@ The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.foo" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.bar" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing arguments for variables y and _. +The user-defined tactic "Top.bar" was not fully applied: +There are missing arguments for variables y and _, +an argument was provided for variable x. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.baz" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.qux" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable _. +The user-defined tactic "Top.mydo" was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable _. +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable _. +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.rec" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable x, +an argument was provided for variable tac. diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v index f17c00e9d..e834fde11 100644 --- a/test-suite/prerequisite/bind_univs.v +++ b/test-suite/prerequisite/bind_univs.v @@ -3,3 +3,5 @@ Monomorphic Definition mono@{u} := Type@{u}. Polymorphic Definition poly@{u} := Type@{u}. + +Monomorphic Universe reqU. diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v new file mode 100644 index 000000000..c4a1d7c28 --- /dev/null +++ b/test-suite/success/unidecls.v @@ -0,0 +1,121 @@ +Set Printing Universes. + +Module unidecls. + Universes a b. +End unidecls. + +Universe a. + +Constraint a < unidecls.a. + +Print Universes. + +(** These are different universes *) +Check Type@{a}. +Check Type@{unidecls.a}. + +Check Type@{unidecls.b}. + +Fail Check Type@{unidecls.c}. + +Fail Check Type@{i}. +Universe foo. +Module Foo. + (** Already declared globaly: but universe names are scoped at the module level *) + Universe foo. + Universe bar. + + Check Type@{Foo.foo}. + Definition bar := 0. +End Foo. + +(** Already declared in the module *) +Universe bar. + +(** Accessible outside the module: universe declarations are global *) +Check Type@{bar}. +Check Type@{Foo.bar}. + +Check Type@{Foo.foo}. +(** The same *) +Check Type@{foo}. +Check Type@{Top.foo}. + +Universe secfoo. +Section Foo'. + Fail Universe secfoo. + Universe secfoo2. + Check Type@{Foo'.secfoo2}. + Constraint secfoo2 < a. +End Foo'. + +Check Type@{secfoo2}. +Fail Check Type@{Foo'.secfoo2}. +Fail Check eq_refl : Type@{secfoo2} = Type@{a}. + +(** Below, u and v are global, fixed universes *) +Module Type Arg. + Universe u. + Parameter T: Type@{u}. +End Arg. + +Module Fn(A : Arg). + Universes v. + + Check Type@{A.u}. + Constraint A.u < v. + + Definition foo : Type@{v} := nat. + Definition bar : Type@{A.u} := nat. + + Fail Definition foo(A : Type@{v}) : Type@{A.u} := A. +End Fn. + +Module ArgImpl : Arg. + Definition T := nat. +End ArgImpl. + +Module ArgImpl2 : Arg. + Definition T := bool. +End ArgImpl2. + +(** Two applications of the functor result in the exact same universes *) +Module FnApp := Fn(ArgImpl). + +Check Type@{FnApp.v}. +Check FnApp.foo. +Check FnApp.bar. + +Check (eq_refl : Type@{ArgImpl.u} = Type@{ArgImpl2.u}). + +Module FnApp2 := Fn(ArgImpl). +Check Type@{FnApp2.v}. +Check FnApp2.foo. +Check FnApp2.bar. + +Import ArgImpl2. +(** Now u refers to ArgImpl.u and ArgImpl2.u *) +Check FnApp2.bar. + +(** It can be shadowed *) +Universe u. + +(** This refers to the qualified name *) +Check FnApp2.bar. + +Constraint u = ArgImpl.u. +Print Universes. + +Set Universe Polymorphism. + +Section PS. + Universe poly. + + Definition id (A : Type@{poly}) (a : A) : A := a. +End PS. +(** The universe is polymorphic and discharged, does not persist *) +Fail Check Type@{poly}. + +Print Universes. +Check id nat. +Check id@{Set}. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 4ee6efec0..7fd942908 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -172,7 +172,7 @@ COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile -COQ_VERSION:=$(shell $(COQC) --print-version | cut -d ' ' -f 1) +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") @@ -392,7 +392,7 @@ checkproofs: .PHONY: checkproofs validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $^ .PHONY: validate only: $(TGTS) diff --git a/vernac/classes.ml b/vernac/classes.ml index b80741269..cb1d2f7c7 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -126,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; - Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm); + Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm); instance_hook k info global imps ?hook (ConstRef kn); id @@ -208,7 +208,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) (ParameterEntry (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in - Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); + Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders !evars); instance_hook k pri global imps ?hook (ConstRef cst); id end else ( diff --git a/vernac/command.ml b/vernac/command.ml index 01c7f149b..66d4fe984 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -95,7 +95,7 @@ let interp_definition pl bl poly red_option c ctypopt = let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in let nb_args = Context.Rel.nhyps ctx in - let imps,pl,ce = + let imps,ce = match ctypopt with None -> let subst = evd_comb0 Evd.nf_univ_variables evdref in @@ -105,11 +105,10 @@ let interp_definition pl bl poly red_option c ctypopt = let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = Univops.universes_of_constr body in - let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ~poly evd decl in - let binders = Evd.universe_binders evd in - imps1@(Impargs.lift_implicits nb_args imps2), binders, + let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in + let () = evdref := Evd.restrict_universe_context !evdref vars in + let uctx = Evd.check_univ_decl ~poly !evdref decl in + imps1@(Impargs.lift_implicits nb_args imps2), definition_entry ~univs:uctx body | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in @@ -131,23 +130,22 @@ let interp_definition pl bl poly red_option c ctypopt = in if not (try List.for_all chk imps2 with Not_found -> false) then warn_implicits_in_term (); - let vars = Univ.LSet.union (Univops.universes_of_constr body) - (Univops.universes_of_constr typ) in - let ctx = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ~poly ctx decl in - let binders = Evd.universe_binders evd in - imps1@(Impargs.lift_implicits nb_args impsty), binders, - definition_entry ~types:typ - ~univs:uctx body + let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in + let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in + let vars = Univ.LSet.union bodyvars tyvars in + let () = evdref := Evd.restrict_universe_context !evdref vars in + let uctx = Evd.check_univ_decl ~poly !evdref decl in + imps1@(Impargs.lift_implicits nb_args impsty), + definition_entry ~types:typ ~univs:uctx body in - red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps + (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps) -let check_definition (ce, evd, _, _, imps) = +let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd Evd.empty; ce let do_definition ident k univdecl bl red_option c ctypopt hook = - let (ce, evd, univdecl, pl', imps as def) = + let (ce, evd, univdecl, imps as def) = interp_definition univdecl bl (pi2 k) red_option c ctypopt in if Flags.is_program_mode () then @@ -168,7 +166,7 @@ let do_definition ident k univdecl bl red_option c ctypopt hook = ignore(Obligations.add_definition ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(DeclareDef.declare_definition ident k ce pl' imps + ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) @@ -224,7 +222,7 @@ match local with let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in - let () = Universes.register_universe_binders gr pl in + let () = Declare.declare_univ_binders gr pl in let () = assumption_message ident in let () = if do_instance then Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in @@ -712,7 +710,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls = let ind = (mind,i) in let gr = IndRef ind in maybe_declare_manual_implicits false gr indimpls; - Universes.register_universe_binders gr pl; + Declare.declare_univ_binders gr pl; List.iteri (fun j impls -> maybe_declare_manual_implicits false @@ -1268,7 +1266,7 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive local p fixkind fixl ntns = +let do_program_recursive local poly fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = interp_recursive isfix fixl ntns @@ -1310,8 +1308,8 @@ let do_program_recursive local p fixkind fixl ntns = end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with - | Obligations.IsFixpoint _ -> (local, p, Fixpoint) - | Obligations.IsCoFixpoint -> (local, p, CoFixpoint) + | Obligations.IsFixpoint _ -> (local, poly, Fixpoint) + | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint) in Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind diff --git a/vernac/command.mli b/vernac/command.mli index 070f3e112..a1f916c78 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -28,7 +28,7 @@ val do_constraint : polymorphic -> val interp_definition : Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * - Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits + Univdecls.universe_decl * Impargs.manual_implicits val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 980db4109..dfac78c04 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -36,7 +36,7 @@ let declare_global_definition ident ce local k pl imps = let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in - let () = Universes.register_universe_binders gr pl in + let () = Declare.declare_univ_binders gr pl in let () = definition_message ident in gr @@ -49,6 +49,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = let () = definition_message ident in let gr = VarRef ident in let () = maybe_declare_manual_implicits false gr imps in + let () = Declare.declare_univ_binders gr pl in let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 42631a15b..200c2260e 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -177,7 +177,7 @@ let look_for_possibly_mutual_statements = function (* Saving a goal *) -let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = +let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in try let const = adjust_guardness_conditions const do_guard in @@ -204,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = (locality, ConstRef kn) in definition_message id; - Universes.register_universe_binders r (Option.default Universes.empty_binders pl); + Declare.declare_univ_binders r (UState.universe_binders uctx); call_hook (fun exn -> exn) hook l r with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -286,17 +286,17 @@ let save_hook = ref ignore let set_save_hook f = save_hook := f let save_named ?export_seff proof = - let id,const,(cstrs,pl),do_guard,persistence,hook = proof in - save ?export_seff id const cstrs pl do_guard persistence hook + let id,const,uctx,do_guard,persistence,hook = proof in + save ?export_seff id const uctx do_guard persistence hook let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then user_err Pp.(str "This command can only be used for unnamed theorem.") let save_anonymous ?export_seff proof save_ident = - let id,const,(cstrs,pl),do_guard,persistence,hook = proof in + let id,const,uctx,do_guard,persistence,hook = proof in check_anonymity id save_ident; - save ?export_seff save_ident const cstrs pl do_guard persistence hook + save ?export_seff save_ident const uctx do_guard persistence hook (* Admitted *) @@ -312,7 +312,7 @@ let admit (id,k,e) pl hook () = | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id in let () = assumption_message id in - Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl); + Declare.declare_univ_binders (ConstRef kn) pl; call_hook (fun exn -> exn) hook Global (ConstRef kn) (* Starting a goal *) @@ -330,8 +330,8 @@ let get_proof proof do_guard hook opacity = let universe_proof_terminator compute_guard hook = let open Proof_global in make_terminator begin function - | Admitted (id,k,pe,(ctx,pl)) -> - admit (id,k,pe) pl (hook (Some ctx)) (); + | Admitted (id,k,pe,ctx) -> + admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) (); Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff = match opaque with @@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook = | Vernacexpr.Opaque -> true, false in let proof = get_proof proof compute_guard - (hook (Some (fst proof.Proof_global.universes))) is_opaque in + (hook (Some (proof.Proof_global.universes))) is_opaque in begin match idopt with | None -> save_named ~export_seff proof | Some (_,id) -> save_anonymous ~export_seff proof id @@ -417,7 +417,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = | (id,(t,(_,imps)))::other_thms -> let hook ctx strength ref = let ctx = match ctx with - | None -> Evd.empty_evar_universe_context + | None -> UState.empty | Some ctx -> ctx in let other_thms_data = @@ -426,9 +426,9 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in let body = Option.map norm body in - List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in + let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in + List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; @@ -496,7 +496,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in + let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> @@ -518,12 +518,9 @@ let save_proof ?proof = function Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in let decl = Proof_global.get_universe_decl () in - let evd = Evd.from_ctx universes in let poly = pi2 k in - let ctx = Evd.check_univ_decl ~poly evd decl in - let binders = if poly then Some (UState.universe_binders universes) else None in - Admitted(id,k,(sec_vars, (typ, ctx), None), - (universes, binders)) + let ctx = UState.check_univ_decl ~poly universes decl in + Admitted(id,k,(sec_vars, (typ, ctx), None), universes) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (is_opaque,idopt) -> diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 1b1304db5..a4854b4a6 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -56,7 +56,7 @@ val standard_proof_terminator : (** {6 ... } *) (** A hook the next three functions pass to cook_proof *) -val set_save_hook : (Proof.proof -> unit) -> unit +val set_save_hook : (Proof.t -> unit) -> unit val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1046d68f8..24d664951 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -833,7 +833,7 @@ let obligation_terminator name num guard hook auto pf = let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let ty = entry.Entries.const_entry_type in let (body, cstr), () = Future.force entry.Entries.const_entry_body in - let sigma = Evd.from_ctx (fst uctx) in + let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) body; (** Declare the obligation ourselves and drop the hook *) diff --git a/vernac/record.ml b/vernac/record.ml index 1d255b08e..1cdc538b5 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -613,7 +613,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in let sign = structure_signature (fields@params) in - match kind with + let gr = match kind with | Class def -> let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild @@ -638,3 +638,6 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind + in + Declare.declare_univ_binders gr pl; + gr diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 63f358a9d..63768d9b8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -484,7 +484,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) [Some (lid,pl), (bl,t)] hook | DefineBody (bl,red_option,c,typ_opt) -> - let red_option = match red_option with + let red_option = match red_option with | None -> None | Some r -> let sigma, env = Pfedit.get_current_context () in @@ -2268,5 +2268,10 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = comments on the PR *) let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; - interp ?verbosely ?proof ~st cmd; - Vernacstate.freeze_interp_state `No + try + interp ?verbosely ?proof ~st cmd; + Vernacstate.freeze_interp_state `No + with exn -> + let exn = CErrors.push exn in + Vernacstate.invalidate_cache (); + iraise exn diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index eb1359d52..4980333b5 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -8,22 +8,34 @@ type t = { system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) + proof : Proof_global.t; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) } -let s_cache = ref (States.freeze ~marshallable:`No) -let s_proof = ref (Proof_global.freeze ~marshallable:`No) +let s_cache = ref None +let s_proof = ref None let invalidate_cache () = - s_cache := Obj.magic 0; - s_proof := Obj.magic 0 + s_cache := None; + s_proof := None + +let update_cache rf v = + rf := Some v; v + +let do_if_not_cached rf f v = + match !rf with + | None -> + rf := Some v; f v + | Some vc when vc != v -> + rf := Some v; f v + | Some _ -> + () let freeze_interp_state marshallable = - { system = (s_cache := States.freeze ~marshallable; !s_cache); - proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); + { system = update_cache s_cache (States.freeze ~marshallable); + proof = update_cache s_proof (Proof_global.freeze ~marshallable); shallow = marshallable = `Shallow } let unfreeze_interp_state { system; proof } = - if (!s_cache != system) then (s_cache := system; States.unfreeze system); - if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) + do_if_not_cached s_cache States.unfreeze system; + do_if_not_cached s_proof Proof_global.unfreeze proof diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index bcfa49aa3..3ed27ddb7 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -8,7 +8,7 @@ type t = { system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) + proof : Proof_global.t; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) } |