diff options
141 files changed, 1885 insertions, 954 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 20dac57a7..e56693eac 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -268,7 +268,7 @@ ci-color: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES subversion" + EXTRA_PACKAGES: "$TIMING_PACKAGES" ci-compcert: <<: *ci-template diff --git a/API/API.mli b/API/API.mli index e320e496c..3ed008ff5 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1293,65 +1293,6 @@ sig type to_patch_substituted end -module Decl_kinds : -sig - type polymorphic = bool - type cumulative_inductive_flag = bool - type recursivity_kind = - | Finite - | CoFinite - | BiFinite - - type discharge = - | DoDischarge - | NoDischarge - - type locality = - | Discharge - | Local - | Global - - type definition_object_kind = - | Definition - | Coercion - | SubClass - | CanonicalStructure - | Example - | Fixpoint - | CoFixpoint - | Scheme - | StructureComponent - | IdentityCoercion - | Instance - | Method - | Let - type theorem_kind = - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary - type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - type goal_kind = locality * polymorphic * goal_object_kind - type assumption_object_kind = - | Definitional - | Logical - | Conjectural - type logical_kind = - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind - type binding_kind = - | Explicit - | Implicit - type private_flag = bool - type definition_kind = locality * polymorphic * definition_object_kind -end - module Retroknowledge : sig type action @@ -1501,10 +1442,15 @@ sig type record_body = (Id.t * Constant.t array * projection_body array) option + type recursivity_kind = + | Finite + | CoFinite + | BiFinite + type mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : record_body option; - mind_finite : Decl_kinds.recursivity_kind; + mind_finite : recursivity_kind; mind_ntypes : int; mind_hyps : Context.Named.t; mind_nparams : int; @@ -1578,7 +1524,7 @@ sig (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; @@ -1861,6 +1807,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 +1883,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 = { @@ -1998,7 +2003,7 @@ end module Univops : sig - val universes_of_constr : Constr.constr -> Univ.LSet.t + val universes_of_constr : Environ.env -> Constr.constr -> Univ.LSet.t val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t end @@ -2039,60 +2044,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 @@ -2205,6 +2156,66 @@ sig | SubEvar of Evar.t end +module Decl_kinds : +sig + type polymorphic = bool + type cumulative_inductive_flag = bool + type recursivity_kind = Declarations.recursivity_kind = + | Finite + | CoFinite + | BiFinite + [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] + + type discharge = + | DoDischarge + | NoDischarge + + type locality = + | Discharge + | Local + | Global + + type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + type goal_object_kind = + | DefinitionBody of definition_object_kind + | Proof of theorem_kind + type goal_kind = locality * polymorphic * goal_object_kind + type assumption_object_kind = + | Definitional + | Logical + | Conjectural + type logical_kind = + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + type binding_kind = + | Explicit + | Implicit + type private_flag = bool + type definition_kind = locality * polymorphic * definition_object_kind +end + module Glob_term : sig type 'a cases_pattern_r = @@ -2754,10 +2765,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 @@ -2770,6 +2781,8 @@ sig end type universe_constraints = Constraints.t + [@@ocaml.deprecated "Use Constraints.t"] + end module UState : @@ -3106,7 +3119,7 @@ sig val fold : Evd.evar_map -> ('a -> constr -> 'a) -> 'a -> constr -> 'a val existential_type : Evd.evar_map -> existential -> types val iter : Evd.evar_map -> (constr -> unit) -> constr -> unit - val eq_constr_universes : Evd.evar_map -> constr -> constr -> Universes.universe_constraints option + val eq_constr_universes : Evd.evar_map -> constr -> constr -> Universes.Constraints.t option val eq_constr_nounivs : Evd.evar_map -> constr -> constr -> bool val compare_constr : Evd.evar_map -> (constr -> constr -> bool) -> constr -> constr -> bool val isApp : Evd.evar_map -> constr -> bool @@ -3994,7 +4007,7 @@ sig type instance_flag = bool option type coercion_flag = bool - type inductive_flag = Decl_kinds.recursivity_kind + type inductive_flag = Declarations.recursivity_kind type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located type opacity_flag = @@ -4842,17 +4855,16 @@ sig 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 @@ -4960,8 +4972,6 @@ sig val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool - val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool - val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list val pr_gls : Goal.goal Evd.sigma -> Pp.t @@ -5006,7 +5016,7 @@ sig Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> 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 @@ -5243,16 +5253,20 @@ end module Genprint : sig - type printer_with_level = + type 'a with_level = { default_already_surrounded : Notation_term.tolerability; default_ensure_surrounded : Notation_term.tolerability; - printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + printer : 'a } type printer_result = - | PrinterBasic of (unit -> Pp.t) - | PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) - | PrinterNeedsContextAndLevel of printer_with_level - type 'a printer = 'a -> Pp.t - type 'a top_printer = 'a -> printer_result +| PrinterBasic of (unit -> Pp.t) +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level + type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t + type top_printer_result = + | TopPrinterBasic of (unit -> Pp.t) + | TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) + | TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level + type 'a printer = 'a -> printer_result + type 'a top_printer = 'a -> top_printer_result val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> 'glb printer -> 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> @@ -6062,7 +6076,7 @@ sig val do_mutual_inductive : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> - Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit + Decl_kinds.private_flag -> Declarations.recursivity_kind -> unit val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> @@ -6088,7 +6102,7 @@ sig structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> - Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> + Decl_kinds.private_flag -> Declarations.recursivity_kind -> Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list val declare_mutual_inductive_with_eliminations : @@ -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,10 +26,20 @@ 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. @@ -30,7 +30,7 @@ package "lib" ( directory = "lib" - requires = "coq.config" + requires = "str, unix, threads, coq.config" archive(byte) = "clib.cma" archive(byte) += "lib.cma" @@ -65,7 +65,7 @@ package "kernel" ( directory = "kernel" - requires = "coq.lib, coq.vm" + requires = "dynlink, coq.lib, coq.vm" archive(byte) = "kernel.cma" archive(native) = "kernel.cmxa" @@ -168,7 +168,7 @@ package "parsing" ( description = "Coq Parsing Engine" version = "8.7" - requires = "coq.proofs" + requires = "camlp5.gramlib, coq.proofs" directory = "parsing" archive(byte) = "parsing.cma" @@ -139,19 +139,10 @@ endif # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. -ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii -ifndef ACCEPT_ALIEN_VO EXISTINGVO:=$(call find, '*.vo') KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) -ifdef ALIENVO -$(error Leftover compiled Coq files without known sources: $(ALIENVO); \ -remove them first, for instance via 'make voclean' \ -(or skip this check via 'make ACCEPT_ALIEN_VO=1')) -endif -endif -ifndef ACCEPT_ALIEN_OBJ EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) @@ -159,9 +150,20 @@ KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ $(MLIFILES:.mli=.cmi) \ $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) + +ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii +ifndef ACCEPT_ALIEN_VO +ifdef ALIENVO +$(error Leftover compiled Coq files without known sources: $(ALIENVO); \ +remove them first, for instance via 'make voclean' or 'make alienclean' \ +(or skip this check via 'make ACCEPT_ALIEN_VO=1')) +endif +endif + +ifndef ACCEPT_ALIEN_OBJ ifdef ALIENOBJS $(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \ -remove them first, for instance via 'make clean' \ +remove them first, for instance via 'make clean' or 'make alienclean' \ (or skip this check via 'make ACCEPT_ALIEN_OBJ=1')) endif endif @@ -196,7 +198,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean clean: objclean cruftclean depclean docclean devdocclean @@ -282,6 +284,9 @@ devdocclean: rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex rm -f $(OCAMLDOCDIR)/html/*.html +alienclean: + rm -f $(ALIENOBJS) $(ALIENVO) + ########################################################################### # Continuous Intregration Tests ########################################################################### diff --git a/Makefile.install b/Makefile.install index b590aad54..27694106f 100644 --- a/Makefile.install +++ b/Makefile.install @@ -101,12 +101,16 @@ INSTALLCMI = $(sort \ $(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \ $(PLUGINS:.cmo=.cmi) +INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% configure.cmx, $(MLFILES:.ml=.cmx))) + install-devfiles: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) + $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMX) + $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o) $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS) ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) 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 21fdba1fa..82341ad9b 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -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 @@ -308,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 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 b2433ee36..fee31b667 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -96,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 () = @@ -132,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 := [] @@ -179,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\ @@ -311,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 | [] -> () @@ -324,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 37315aae7..3850f119b 100644 --- a/configure.ml +++ b/configure.ml @@ -692,6 +692,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 *) @@ -725,11 +741,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 @@ -755,7 +771,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) @@ -812,7 +828,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..3dd24bac4 100644 --- a/default.nix +++ b/default.nix @@ -42,13 +42,21 @@ 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 + ocamlPackages.ocpIndent + ocamlPackages.ocp-index ] 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-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 168a34e6e..232b8a56e 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -115,7 +115,8 @@ ######################################################################## # CoLoR ######################################################################## -: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} +: ${CoLoR_CI_BRANCH:=master} +: ${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git} ######################################################################## # SF diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 309050057..c3ae7552a 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,33 +3,11 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -Color_CI_DIR=${CI_BUILD_DIR}/color +CoLoR_CI_DIR=${CI_BUILD_DIR}/color # Setup Bignums - source ${ci_dir}/ci-bignums.sh -# Compiles CoLoR - -svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} - -sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v - -# Adapt to PR #220 (FunInd not loaded in Prelude anymore) -sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v -sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v -sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v -sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v -sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v -sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v -sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v -sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v -sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v -sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v -sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v -sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v - -( cd ${Color_CI_DIR} && make ) +# Compile CoLoR +git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR} +( cd ${CoLoR_CI_DIR} && make ) diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index fc3cef342..7bf2c7427 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -8,4 +8,5 @@ CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert opam install -j ${NJOBS} -y menhir git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} -( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +#( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index 4865be31e..ed4003601 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph +ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2 git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR} diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 217540cc1..4e8c7e145 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,13 +3,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: Needs fixing to properly set the build directory. -wget ${sf_lf_CI_TARURL} -wget ${sf_plf_CI_TARURL} -wget ${sf_vfa_CI_TARURL} -tar xvfz lf.tgz -tar xvfz plf.tgz -tar xvfz vfa.tgz +mkdir -p ${CI_BUILD_DIR} && cd ${CI_BUILD_DIR} +wget -qO- ${sf_lf_CI_TARURL} | tar xvz +wget -qO- ${sf_plf_CI_TARURL} | tar xvz +wget -qO- ${sf_vfa_CI_TARURL} | tar xvz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh new file mode 100644 index 000000000..cdca8e525 --- /dev/null +++ b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then + ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer + ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git +fi diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh new file mode 100644 index 000000000..7e9b5febd --- /dev/null +++ b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then + Equations_CI_BRANCH=fix-coq-6324 + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git +fi diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt index 6a69c5793..ca3d520c7 100644 --- a/dev/doc/univpoly.txt +++ b/dev/doc/univpoly.txt @@ -12,7 +12,7 @@ type pinductive = inductive puniverses type pconstructor = constructor puniverses type constr = ... - | Const of puniversess + | Const of puniverses | Ind of pinductive | Constr of pconstructor | Proj of constant * constr diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index ecf7880e2..87a829746 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -11,6 +11,13 @@ CODE=0 if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ]; then + # skip PRs from before the linter existed + if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ]; + then + 2>&1 echo "Linting skipped: pull request older than the linter." + exit 0 + fi + # Some problems are too widespread to fix in one commit, but we # can still check that they don't worsen. CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*} diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index bc6ee3191..4c4dbe1e9 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash -# Usage: git-backport <PR number> +# Usage: dev/tools/backport-pr.sh <PR number> set -e diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index f770004a5..0c4a79bfd 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -1,4 +1,6 @@ -#!/bin/sh -e +#!/usr/bin/env bash + +set -e # This script depends (at least) on git and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ @@ -15,12 +17,12 @@ API=https://api.github.com/repos/coq/coq BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'` -COMMIT=`git rev-parse $REMOTE/pr/$PR` +COMMIT=`git rev-parse FETCH_HEAD` STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'` if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then echo "Wrong base branch" - read -p "Bypass? [y/n] " -n 1 -r + read -p "Bypass? [y/N] " -n 1 -r echo if [[ ! $REPLY =~ ^[Yy]$ ]] then @@ -30,7 +32,7 @@ fi; if [ $STATUS != "success" ]; then echo "CI status is \"$STATUS\"" - read -p "Bypass? [y/n] " -n 1 -r + read -p "Bypass? [y/N] " -n 1 -r echo if [[ ! $REPLY =~ ^[Yy]$ ]] then @@ -38,7 +40,7 @@ if [ $STATUS != "success" ]; then fi fi; -git merge -S --no-ff $REMOTE/pr/$PR -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e +git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e # TODO: improve this check if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then 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 b4d9f60eb..04a8a25c1 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -331,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..d303038c5 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -645,6 +645,37 @@ 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 env sigma c = + let open Univ in + let open Declarations in + let rec aux s c = + match kind sigma c with + | Const (c, u) -> + begin match (Environ.lookup_constant c env).const_universes with + | Polymorphic_const _ -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Monomorphic_const (univs, _) -> + LSet.union s univs + end + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + begin match (Environ.lookup_mind mind env).mind_universes with + | Cumulative_ind _ | Polymorphic_ind _ -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Monomorphic_ind (univs,_) -> + LSet.union s univs + end + | 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..f54c422ad 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -187,9 +187,9 @@ val whd_evar : Evd.evar_map -> constr -> constr val eq_constr : Evd.evar_map -> t -> t -> bool val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool -val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option -val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option -val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option +val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option +val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option +val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool (** {6 Iterators} *) @@ -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 : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t + (** {6 Substitutions} *) module Vars : diff --git a/engine/evd.ml b/engine/evd.ml index d57ae89dd..45d2a8b08 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -401,7 +401,7 @@ let rename evk id (evtoid, idtoev) = | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) | Some id' -> if Id.Map.mem id idtoev then anomaly (str "Evar name already in use."); - (EvMap.update evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev)) + (EvMap.set evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev)) let reassign_name_defined evk evk' (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in diff --git a/engine/evd.mli b/engine/evd.mli index fb5a6cd16..636bd1be1 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -208,7 +208,7 @@ val is_defined : evar_map -> Evar.t-> bool val is_undefined : evar_map -> Evar.t-> bool (** Whether an evar is not defined in an evarmap. *) -val add_constraints : evar_map -> Univ.constraints -> evar_map +val add_constraints : evar_map -> Univ.Constraint.t -> evar_map (** Add universe constraints in an evar map. *) val undefined_map : evar_map -> evar_info Evar.Map.t @@ -316,7 +316,7 @@ val whd_sort_variable : evar_map -> constr -> constr exception UniversesDiffer -val add_universe_constraints : evar_map -> Universes.universe_constraints -> evar_map +val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map (** Add the given universe unification constraints to the evar map. @raises UniversesDiffer in case a first-order unification fails. @raises UniverseInconsistency @@ -491,7 +491,7 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t -val evar_universe_context_constraints : UState.t -> Univ.constraints +val evar_universe_context_constraints : UState.t -> Univ.Constraint.t val evar_context_universe_context : UState.t -> Univ.UContext.t [@@ocaml.deprecated "alias of UState.context"] @@ -513,7 +513,7 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t val universe_binders : evar_map -> Universes.universe_binders val add_constraints_context : UState.t -> - Univ.constraints -> UState.t + Univ.Constraint.t -> UState.t val normalize_evar_universe_context_variables : UState.t -> 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 4e30640e4..6566ad989 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -22,6 +22,7 @@ type uinfo = { type t = { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t; uctx_local : Univ.ContextSet.t; (** The local context of variables *) + uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *) uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) uctx_univ_algebraic : Univ.LSet.t; @@ -34,6 +35,7 @@ type t = let empty = { uctx_names = UNameMap.empty, Univ.LMap.empty; uctx_local = Univ.ContextSet.empty; + uctx_seff_univs = Univ.LSet.empty; uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; uctx_universes = UGraph.initial_universes; @@ -60,6 +62,7 @@ let union ctx ctx' = else if is_empty ctx' then ctx else let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in + let seff = Univ.LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) (Univ.ContextSet.levels ctx.uctx_local) in @@ -70,6 +73,7 @@ let union ctx ctx' = let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; + uctx_seff_univs = seff; uctx_univ_variables = Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; uctx_univ_algebraic = @@ -131,7 +135,7 @@ let of_binders b = let universe_binders ctx = fst ctx.uctx_names let instantiate_variable l b v = - try v := Univ.LMap.update l (Some b) !v + try v := Univ.LMap.set l (Some b) !v with Not_found -> assert false exception UniversesDiffer @@ -263,13 +267,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 @@ -363,12 +369,21 @@ let check_univ_decl ~poly uctx decl = ctx let restrict ctx vars = + let vars = Univ.LSet.union vars ctx.uctx_seff_univs in let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars) (fst ctx.uctx_names) vars in let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } +let demote_seff_univs entry uctx = + let open Entries in + match entry.const_entry_universes with + | Polymorphic_const_entry _ -> uctx + | Monomorphic_const_entry (univs, _) -> + let seff = Univ.LSet.union uctx.uctx_seff_univs univs in + { uctx with uctx_seff_univs = seff } + type rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) @@ -430,7 +445,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 @@ -550,7 +565,8 @@ let refresh_undefined_univ_variables uctx = let initial = declare uctx.uctx_initial_universes in let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; - uctx_local = ctx'; + uctx_local = ctx'; + uctx_seff_univs = uctx.uctx_seff_univs; uctx_univ_variables = vars; uctx_univ_algebraic = alg; uctx_universes = univs; uctx_initial_universes = initial } in @@ -567,7 +583,8 @@ let normalize uctx = Universes.refresh_constraints uctx.uctx_initial_universes us' in { uctx_names = uctx.uctx_names; - uctx_local = us'; + uctx_local = us'; + uctx_seff_univs = uctx.uctx_seff_univs; (* not sure about this *) uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; diff --git a/engine/uState.mli b/engine/uState.mli index 16fba41e0..6657d6047 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -53,7 +53,7 @@ val algebraics : t -> Univ.LSet.t (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) -val constraints : t -> Univ.constraints +val constraints : t -> Univ.Constraint.t (** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *) val context : t -> Univ.UContext.t @@ -68,12 +68,12 @@ val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes (** {5 Constraints handling} *) -val add_constraints : t -> Univ.constraints -> t +val add_constraints : t -> Univ.Constraint.t -> t (** @raise UniversesDiffer when universes differ *) -val add_universe_constraints : t -> Universes.universe_constraints -> t +val add_universe_constraints : t -> Universes.Constraints.t -> t (** @raise UniversesDiffer when universes differ *) @@ -87,6 +87,8 @@ val universe_of_name : t -> Id.t -> Univ.Level.t val restrict : t -> Univ.LSet.t -> t +val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t + type rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) @@ -154,3 +156,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 5ac1bc685..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) @@ -459,7 +491,7 @@ module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap) let add_list_map u t map = try let l = LMap.find u map in - LMap.update u (t :: l) map + LMap.set u (t :: l) map with Not_found -> LMap.add u [t] map @@ -552,7 +584,7 @@ let normalize_univ_variable_subst subst = let find l = Univ.LMap.find l !subst in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in + try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_universe_opt_subst subst = diff --git a/engine/universes.mli b/engine/universes.mli index 1401c4ee8..1a98d969b 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 @@ -64,21 +74,23 @@ type universe_constraint_type = ULe | UEq | ULub type universe_constraint = Universe.t * universe_constraint_type * Universe.t module Constraints : sig include Set.S with type elt = universe_constraint - + val pr : t -> Pp.t end type universe_constraints = Constraints.t -type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option -type 'a universe_constrained = 'a * universe_constraints -type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints +[@@ocaml.deprecated "Use Constraints.t"] + +type 'a constraint_accumulator = Constraints.t -> 'a -> 'a option +type 'a universe_constrained = 'a * Constraints.t +type 'a universe_constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t val subst_univs_universe_constraints : universe_subst_fn -> - universe_constraints -> universe_constraints + Constraints.t -> Constraints.t val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function -val to_constraints : UGraph.t -> universe_constraints -> constraints +val to_constraints : UGraph.t -> Constraints.t -> Constraint.t (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose diff --git a/engine/univops.ml b/engine/univops.ml index 9a9ae12ca..df25d8725 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -9,12 +9,25 @@ open Univ open Constr -let universes_of_constr c = +let universes_of_constr env c = + let open Declarations in let rec aux s c = match kind c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> + | Const (c, u) -> + begin match (Environ.lookup_constant c env).const_universes with + | Polymorphic_const _ -> + LSet.fold LSet.add (Instance.levels u) s + | Monomorphic_const (univs, _) -> + LSet.union s univs + end + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + begin match (Environ.lookup_mind mind env).mind_universes with + | Cumulative_ind _ | Polymorphic_ind _ -> + LSet.fold LSet.add (Instance.levels u) s + | Monomorphic_ind (univs,_) -> + LSet.union s univs + end + | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s | _ -> Constr.fold aux s c diff --git a/engine/univops.mli b/engine/univops.mli index 9af568bcb..30fcc4368 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -9,7 +9,8 @@ open Constr open Univ -(** Shrink a universe context to a restricted set of variables *) +(** The universes of monomorphic constants appear. *) +val universes_of_constr : Environ.env -> constr -> LSet.t -val universes_of_constr : constr -> LSet.t +(** Shrink a universe context to a restricted set of variables *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index f6f46710c..a561ea370 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -82,7 +82,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, ploc_vala None, - <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>) let make_fun_clauses loc s l = let map c = diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index cfc0e09a0..43d7aa363 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -377,15 +377,8 @@ let init = match file with | None -> init_sid | Some file -> - let dir = Filename.dirname file in - let open Loadpath in let open CUnix in let doc, initial_id, _ = - let doc = get_doc () in - if not (is_in_load_paths (physical_path_of_string dir)) then begin - let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in - let loc_ast = Stm.parse_sentence ~doc init_sid pa in - Stm.add false ~doc ~ontop:init_sid loc_ast - end else doc, init_sid, `NewTip in + get_doc (), init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; set_doc (Stm.finish ~doc); 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..0adad1419 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,13 +551,16 @@ 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 +type constraint_decl = polymorphic * Univ.Constraint.t let cache_constraints (na, (p, c)) = let ctx = @@ -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/decl_kinds.ml b/intf/decl_kinds.ml index 1dea6d9e9..b0c1f6661 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -75,7 +75,8 @@ type logical_kind = (** Recursive power of type declarations *) -type recursivity_kind = +type recursivity_kind = Declarations.recursivity_kind = | Finite (** = inductive *) | CoFinite (** = coinductive *) | BiFinite (** = non-recursive, like in "Record" definitions *) +[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] 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/intf/vernacexpr.ml b/intf/vernacexpr.ml index 5c9141fd6..c7a9db1cb 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -145,7 +145,7 @@ type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) -type inductive_flag = Decl_kinds.recursivity_kind +type inductive_flag = Declarations.recursivity_kind type onlyparsing_flag = Flags.compat_version option (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version @@ -482,18 +482,39 @@ and vernac_argument_status = { implicit_status : vernac_implicit_status; } -(* A vernac classifier has to tell if a command: - vernac_when: has to be executed now (alters the parser) or later - vernac_type: if it is starts, ends, continues a proof or +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. + + - vernac_type: if it is starts, ends, continues a proof or alters the global state or is a control command like BackTo or is - a query like Check *) + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) type vernac_type = + (* Start of a proof *) | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) | VtSideff of vernac_sideff_type + (* End of a proof *) | VtQed of vernac_qed_type + (* A proof step *) | VtProofStep of proof_step + (* To be removed *) | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) | VtQuery of vernac_part_of_script * Feedback.route_id + (* To be removed *) | VtMeta | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d5312c500..7f4b85fd0 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -172,13 +172,18 @@ type abstract_inductive_universes = | Polymorphic_ind of Univ.AUContext.t | Cumulative_ind of Univ.ACumulativityInfo.t +type recursivity_kind = + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) + type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) mind_record : record_body option; (** The record information *) - mind_finite : Decl_kinds.recursivity_kind; (** Whether the type is inductive or coinductive *) + mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) diff --git a/kernel/entries.ml b/kernel/entries.ml index c44a17df2..ca79de404 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -51,7 +51,7 @@ type mutual_inductive_entry = { (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; diff --git a/kernel/environ.mli b/kernel/environ.mli index 652ed0f9f..7cc541258 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -152,9 +152,9 @@ exception NotEvaluableConst of const_evaluation_result val constant_value : env -> Constant.t puniverses -> constr constrained val constant_type : env -> Constant.t puniverses -> types constrained -val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.constraints) option +val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.Constraint.t) option val constant_value_and_type : env -> Constant.t puniverses -> - constr option * types * Univ.constraints + constr option * types * Univ.Constraint.t (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t @@ -203,10 +203,10 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** Add universe constraints to the environment. @raises UniverseInconsistency *) -val add_constraints : Univ.constraints -> env -> env +val add_constraints : Univ.Constraint.t -> env -> env (** Check constraints are satifiable in the environment. *) -val check_constraints : Univ.constraints -> env -> bool +val check_constraints : Univ.Constraint.t -> env -> bool val push_context : ?strict:bool -> Univ.UContext.t -> env -> env val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env diff --git a/kernel/inductive.mli b/kernel/inductive.mli index a19f87b05..8aaeee831 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -37,7 +37,7 @@ val ind_subst : MutInd.t -> mutual_inductive_body -> Instance.t -> constr list val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t val instantiate_inductive_constraints : - mutual_inductive_body -> Instance.t -> constraints + mutual_inductive_body -> Instance.t -> Constraint.t val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 41d6c05eb..b0f4a1e5f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -212,7 +212,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare env pb s0 s1 u, check) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 05a906e28..573e4c8bd 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -49,7 +49,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 0bfe07486..a30bb37e6 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -139,7 +139,7 @@ val push_context : bool -> Univ.UContext.t -> safe_transformer0 val add_constraints : - Univ.constraints -> safe_transformer0 + Univ.Constraint.t -> safe_transformer0 (* (\** Generator of universes *\) *) (* val next_universe : int safe_transformer *) diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index b24c20aa0..67df3759e 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -10,4 +10,4 @@ open Univ open Declarations open Environ -val check_subtypes : env -> module_type_body -> module_type_body -> constraints +val check_subtypes : env -> module_type_body -> module_type_body -> Constraint.t diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 3a1f2ae00..781c6bfbc 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -59,7 +59,7 @@ type ('constr, 'types) ptype_error = | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array - | UnsatisfiedConstraints of Univ.constraints + | UnsatisfiedConstraints of Univ.Constraint.t type type_error = (constr, types) ptype_error diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index e4fa65686..72861f6e4 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -60,7 +60,7 @@ type ('constr, 'types) ptype_error = | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array - | UnsatisfiedConstraints of Univ.constraints + | UnsatisfiedConstraints of Univ.Constraint.t type type_error = (constr, types) ptype_error @@ -105,4 +105,4 @@ val error_ill_typed_rec_body : val error_elim_explain : Sorts.family -> Sorts.family -> arity_error -val error_unsatisfied_constraints : env -> Univ.constraints -> 'a +val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index b95388ed0..f71d83d85 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -35,10 +35,10 @@ val check_eq_instances : Instance.t check_function constraints are not satisfiable. *) val enforce_constraint : univ_constraint -> t -> t -val merge_constraints : constraints -> t -> t +val merge_constraints : Constraint.t -> t -> t val check_constraint : t -> univ_constraint -> bool -val check_constraints : constraints -> t -> bool +val check_constraints : Constraint.t -> t -> bool (** Adds a universe to the graph, ensuring it is >= or > Set. @raises AlreadyDeclared if the level is already declared in the graph. *) @@ -57,7 +57,7 @@ val empty_universes : t val sort_universes : t -> t -val constraints_of_universes : t -> constraints +val constraints_of_universes : t -> Constraint.t val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of 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..459394439 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 @@ -165,20 +169,20 @@ module Constraint : sig end type constraints = Constraint.t +[@@ocaml.deprecated "Use Constraint.t"] -val empty_constraint : constraints -val union_constraint : constraints -> constraints -> constraints -val eq_constraint : constraints -> constraints -> bool +val empty_constraint : Constraint.t +val union_constraint : Constraint.t -> Constraint.t -> Constraint.t +val eq_constraint : Constraint.t -> Constraint.t -> bool -(** A value with universe constraints. *) -type 'a constrained = 'a * constraints +(** A value with universe Constraint.t. *) +type 'a constrained = 'a * Constraint.t (** Constrained *) -val constraints_of : 'a constrained -> constraints - -(** Enforcing constraints. *) +val constraints_of : 'a constrained -> Constraint.t -type 'a constraint_function = 'a -> 'a -> constraints -> constraints +(** Enforcing Constraint.t. *) +type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t val enforce_eq : Universe.t constraint_function val enforce_leq : Universe.t constraint_function @@ -195,7 +199,7 @@ val enforce_leq_level : Level.t constraint_function universes in the path are canonical. Note that each step does not necessarily correspond to an actual constraint, but reflect how the system stores the graph and may result from combination of several - constraints... + Constraint.t... *) type explanation = (constraint_type * Universe.t) list type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option @@ -290,8 +294,8 @@ val in_punivs : 'a -> 'a puniverses val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool -(** A vector of universe levels with universe constraints, - representiong local universe variables and associated constraints *) +(** A vector of universe levels with universe Constraint.t, + representiong local universe variables and associated Constraint.t *) module UContext : sig @@ -303,9 +307,9 @@ sig val is_empty : t -> bool val instance : t -> Instance.t - val constraints : t -> constraints + val constraints : t -> Constraint.t - val dest : t -> Instance.t * constraints + val dest : t -> Instance.t * Constraint.t (** Keeps the order of the instances *) val union : t -> t -> t @@ -324,7 +328,7 @@ sig val repr : t -> UContext.t (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of - the context and [cstr] the abstracted constraints. *) + the context and [cstr] the abstracted Constraint.t. *) val empty : t val is_empty : t -> bool @@ -338,7 +342,7 @@ sig val union : t -> t -> t val instantiate : Instance.t -> t -> Constraint.t - (** Generate the set of instantiated constraints **) + (** Generate the set of instantiated Constraint.t **) end @@ -346,14 +350,14 @@ type abstract_universe_context = AUContext.t [@@ocaml.deprecated "Use AUContext.t"] (** Universe info for inductive types: A context of universe levels - with universe constraints, representing local universe variables - and constraints, together with a context of universe levels with - universe constraints, representing conditions for subtyping used + with universe Constraint.t, representing local universe variables + and Constraint.t, together with a context of universe levels with + universe Constraint.t, representing conditions for subtyping used for inductive types. This data structure maintains the invariant that the context for - subtyping constraints is exactly twice as big as the context for - universe constraints. *) + subtyping Constraint.t is exactly twice as big as the context for + universe Constraint.t. *) module CumulativityInfo : sig type t @@ -366,7 +370,7 @@ sig val univ_context : t -> UContext.t val subtyp_context : t -> UContext.t - (** This function takes a universe context representing constraints + (** This function takes a universe context representing Constraint.t of an inductive and a Instance.t of fresh universe names for the subtyping (with the same length as the context in the given universe context) and produces a UInfoInd.t that with the @@ -413,7 +417,7 @@ sig val diff : t -> t -> t val add_universe : Level.t -> t -> t - val add_constraints : constraints -> t -> t + val add_constraints : Constraint.t -> t -> t val add_instance : Instance.t -> t -> t (** Arbitrary choice of linear order of the variables *) @@ -421,14 +425,14 @@ sig val to_context : t -> UContext.t val of_context : UContext.t -> t - val constraints : t -> constraints + val constraints : t -> Constraint.t val levels : t -> LSet.t (** the number of universes in the context *) val size : t -> int end -(** A set of universes with universe constraints. +(** A set of universes with universe Constraint.t. We linearize the set to a list after typechecking. Beware, representation could change. *) @@ -445,7 +449,7 @@ val is_empty_level_subst : universe_level_subst -> bool (** Substitution of universes. *) val subst_univs_level_level : universe_level_subst -> Level.t -> Level.t val subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t -val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints +val subst_univs_level_constraints : universe_level_subst -> Constraint.t -> Constraint.t val subst_univs_level_abstract_universe_context : universe_level_subst -> AUContext.t -> AUContext.t val subst_univs_level_instance : universe_level_subst -> Instance.t -> Instance.t @@ -457,7 +461,7 @@ val is_empty_subst : universe_subst -> bool val make_subst : universe_subst -> universe_subst_fn val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t -val subst_univs_constraints : universe_subst_fn -> constraints -> constraints +val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t (** Substitution of instances *) val subst_instance_instance : Instance.t -> Instance.t -> Instance.t @@ -475,7 +479,7 @@ val make_abstract_instance : AUContext.t -> Instance.t (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.t -val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t +val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t @@ -490,7 +494,7 @@ val pr_universe_subst : universe_subst -> Pp.t (** {6 Hash-consing } *) val hcons_univ : Universe.t -> Universe.t -val hcons_constraints : constraints -> constraints +val hcons_constraints : Constraint.t -> Constraint.t val hcons_universe_set : LSet.t -> LSet.t val hcons_universe_context : UContext.t -> UContext.t val hcons_abstract_universe_context : AUContext.t -> AUContext.t @@ -511,6 +515,6 @@ val eq_levels : Level.t -> Level.t -> bool val equal_universes : Universe.t -> Universe.t -> bool [@@ocaml.deprecated "Use Universe.equal"] -(** Universes of constraints *) -val universes_of_constraints : constraints -> LSet.t +(** Universes of Constraint.t *) +val universes_of_constraints : Constraint.t -> LSet.t [@@ocaml.deprecated "Use Constraint.universes_of"] diff --git a/lib/cMap.ml b/lib/cMap.ml index 0ecb40209..b4c4aedd0 100644 --- a/lib/cMap.ml +++ b/lib/cMap.ml @@ -26,7 +26,7 @@ sig include CSig.MapS module Set : CSig.SetS with type elt = key val get : key -> 'a t -> 'a - val update : key -> 'a -> 'a t -> 'a t + val set : key -> 'a -> 'a t -> 'a t val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t val domain : 'a t -> Set.t val bind : (key -> 'a) -> Set.t -> 'a t @@ -50,7 +50,7 @@ end module MapExt (M : Map.OrderedType) : sig type 'a map = 'a Map.Make(M).t - val update : M.t -> 'a -> 'a map -> 'a map + val set : M.t -> 'a -> 'a map -> 'a map val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map val domain : 'a map -> Set.Make(M).t val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map @@ -93,19 +93,19 @@ struct let set_prj : set -> _set = Obj.magic let set_inj : _set -> set = Obj.magic - let rec update k v (s : 'a map) : 'a map = match map_prj s with + let rec set k v (s : 'a map) : 'a map = match map_prj s with | MEmpty -> raise Not_found | MNode (l, k', v', r, h) -> let c = M.compare k k' in if c < 0 then - let l' = update k v l in + let l' = set k v l in if l == l' then s else map_inj (MNode (l', k', v', r, h)) else if c = 0 then if v' == v then s else map_inj (MNode (l, k', v, r, h)) else - let r' = update k v r in + let r' = set k v r in if r == r' then s else map_inj (MNode (l, k', v', r', h)) diff --git a/lib/cMap.mli b/lib/cMap.mli index f65036139..5e65bd200 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -34,7 +34,7 @@ sig val get : key -> 'a t -> 'a (** Same as {!find} but fails an assertion instead of raising [Not_found] *) - val update : key -> 'a -> 'a t -> 'a t + val set : key -> 'a -> 'a t -> 'a t (** Same as [add], but expects the key to be present, and thus faster. @raise Not_found when the key is unbound in the map. *) diff --git a/lib/cSig.mli b/lib/cSig.mli index 6910cbbf0..32e9d2af0 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -56,6 +56,12 @@ sig val is_empty: 'a t -> bool val mem: key -> 'a t -> bool val add: key -> 'a -> 'a t -> 'a t + (* when Coq requires OCaml 4.06 or later, can add: + + val update : key -> ('a option -> 'a option) -> 'a t -> 'a t + + allowing Coq to use OCaml's "update" + *) val singleton: key -> 'a -> 'a t val remove: key -> 'a t -> 'a t val merge: diff --git a/lib/hMap.ml b/lib/hMap.ml index c69efdb71..37079af78 100644 --- a/lib/hMap.ml +++ b/lib/hMap.ml @@ -47,7 +47,7 @@ struct try let m = Int.Map.find h s in let m = Set.add x m in - Int.Map.update h m s + Int.Map.set h m s with Not_found -> let m = Set.singleton x in Int.Map.add h m s @@ -65,7 +65,7 @@ struct if Set.is_empty m then Int.Map.remove h s else - Int.Map.update h m s + Int.Map.set h m s with Not_found -> s let height s = Int.Map.height s @@ -135,7 +135,7 @@ struct let s' = Int.Map.find h accu in let si = Set.filter (fun e -> not (Set.mem e s)) s' in if Set.is_empty si then Int.Map.remove h accu - else Int.Map.update h si accu + else Int.Map.set h si accu with Not_found -> accu in Int.Map.fold fold s2 s1 @@ -242,11 +242,19 @@ struct try let m = Int.Map.find h s in let m = Map.add k x m in - Int.Map.update h m s + Int.Map.set h m s with Not_found -> let m = Map.singleton k x in Int.Map.add h m s + (* when Coq requires OCaml 4.06 or later, the module type + CSig.MapS may include the signature of OCaml's "update", + requiring an implementation here, which could be just: + + let update k f s = assert false (* not implemented *) + + *) + let singleton k x = let h = M.hash k in Int.Map.singleton h (Map.singleton k x) @@ -259,7 +267,7 @@ struct if Map.is_empty m then Int.Map.remove h s else - Int.Map.update h m s + Int.Map.set h m s with Not_found -> s let merge f s1 s2 = @@ -359,7 +367,7 @@ struct let h = M.hash k in let m = Int.Map.find h s in let m = Map.modify k f m in - Int.Map.update h m s + Int.Map.set h m s let bind f s = let fb m = Map.bind f m in @@ -367,11 +375,11 @@ struct let domain s = Int.Map.map Map.domain s - let update k x s = + let set k x s = let h = M.hash k in let m = Int.Map.find h s in - let m = Map.update k x m in - Int.Map.update h m s + let m = Map.set k x m in + Int.Map.set h m s let smartmap f s = let fs m = Map.smartmap f m in 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..c62462f9f 100644 --- a/library/global.mli +++ b/library/global.mli @@ -44,7 +44,7 @@ val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t (** Extra universe constraints *) -val add_constraints : Univ.constraints -> unit +val add_constraints : Univ.Constraint.t -> unit val push_context : bool -> Univ.UContext.t -> unit val push_context_set : bool -> Univ.ContextSet.t -> unit @@ -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 a00914eab..f9241c0d4 100644 --- a/man/coqchk.1 +++ b/man/coqchk.1 @@ -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/funind/recdef.ml b/plugins/funind/recdef.ml index b0a76137b..766adfc63 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -141,7 +141,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") -let le = function () -> (coq_init_constant "le") +let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = @@ -857,9 +857,13 @@ let rec prove_le g = Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try - let matching_fun = - pf_is_matching g - (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in + let matching_fun c = match EConstr.kind sigma c with + | App (c, [| x0 ; _ |]) -> + EConstr.isVar sigma x0 && + Id.equal (destVar sigma x0) (destVar sigma x) && + is_global sigma (le ()) c + | _ -> false + in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 34fea6175..8b9eb3983 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -471,7 +471,7 @@ END VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtUnknown, VtNow ] -> + [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d70751245..6aa2f6f89 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,24 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + let string_of_genarg_arg (ArgumentType arg) = let rec aux : type a b c. (a, b, c) genarg_type -> string = function | ListArg t -> aux t ^ "_list" @@ -127,9 +145,9 @@ let string_of_genarg_arg (ArgumentType arg) = | Some Refl -> let open Genprint in match generic_top_print (in_gen (Topwit wit) x) with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> printer (Global.env()) Evd.empty default_ensure_surrounded end | _ -> default @@ -723,8 +741,10 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,[]) as t -> pr_atom0 t | TacIntroPattern (ev,(_::_ as p)) -> - hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++ - prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) + hov 1 (primitive (if ev then "eintros" else "intros") ++ + (match p with + | [_,Misctypes.IntroForthcoming false] -> mt () + | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ @@ -1192,42 +1212,77 @@ let declare_extra_genarg_pprule wit | ExtraArg s -> () | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = + Genprint.PrinterBasic (fun () -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in let g x = + Genprint.PrinterBasic (fun () -> let env = Global.env () in - g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x) in let h x = - Genprint.PrinterNeedsContext (fun env sigma -> + Genprint.TopPrinterNeedsContext (fun env sigma -> h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) in Genprint.register_print0 wit f g h +let declare_extra_genarg_pprule_with_level wit + (f : 'a raw_extra_genarg_printer_with_level) + (g : 'b glob_extra_genarg_printer_with_level) + (h : 'c extra_genarg_printer_with_level) default_surrounded default_non_surrounded = + begin match wit with + | ExtraArg s -> () + | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") + end; + let open Genprint in + let f x = + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in + let g x = + let env = Global.env () in + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) } + in + let h x = + TopPrinterNeedsContextAndLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun env sigma n -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) } + in + Genprint.register_print0 wit f g h + let declare_extra_vernac_genarg_pprule wit f = - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in Genprint.register_vernac_print0 wit f (** Registering *) -let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma -> let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in Miscprint.pr_intro_pattern print_constr p) -let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma -> pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) -let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in Miscprint.pr_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_with_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in pr_with_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_destruction_arg_env c = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, c = match c with | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c) | clear_flag,ElimOnAnonHyp n as x -> sigma, x @@ -1236,12 +1291,16 @@ let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c) let make_constr_printer f c = - Genprint.PrinterNeedsContextAndLevel { + Genprint.TopPrinterNeedsContextAndLevel { Genprint.default_already_surrounded = Ppconstr.ltop; Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; Genprint.printer = (fun env sigma n -> f env sigma n c)} let lift f a = Genprint.PrinterBasic (fun () -> f a) +let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) + +let register_basic_print0 wit f g h = + Genprint.register_print0 wit (lift f) (lift g) (lift_top h) let pr_glob_constr_pptac c = @@ -1255,80 +1314,81 @@ let pr_lglob_constr_pptac c = let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in - Genprint.register_print0 wit_int_or_var - (pr_or_var int) (pr_or_var int) (lift int); - Genprint.register_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global); - Genprint.register_print0 wit_ident - pr_id pr_id (lift pr_id); - Genprint.register_print0 wit_var - (pr_located pr_id) (pr_located pr_id) (lift pr_id); - Genprint.register_print0 + let open Genprint in + register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; + register_basic_print0 wit_ref + pr_reference (pr_or_var (pr_located pr_global)) pr_global; + register_basic_print0 wit_ident pr_id pr_id pr_id; + register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id; + register_print0 wit_intro_pattern - (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c)) + (lift (Miscprint.pr_intro_pattern pr_constr_expr)) + (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c))) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl - (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) pr_lident) - (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) + (lift (pr_clauses (Some true) pr_lident)) + (lift (pr_clauses (Some true) pr_lident)) + (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) ; Genprint.register_print0 wit_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_lconstr_expr) + (lift (fun (c, _) -> pr_lglob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c,_) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c, _) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; - Genprint.register_print0 wit_red_expr - (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)) + Genprint.register_print0 + wit_red_expr + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) pr_red_expr_env ; - Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); - Genprint.register_print0 wit_bindings - (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + register_print0 wit_bindings + (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)) + (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_bindings_env ; - Genprint.register_print0 wit_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 wit_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 wit_open_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 wit_open_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 Tacarg.wit_destruction_arg - (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 Tacarg.wit_destruction_arg + (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr)) + (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_destruction_arg_env ; - Genprint.register_print0 Stdarg.wit_int int int (lift int); - Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool); - Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit); - Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str); - Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring) + register_basic_print0 Stdarg.wit_int int int int; + register_basic_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; + register_basic_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; + register_basic_print0 Stdarg.wit_pre_ident str str str; + register_basic_print0 Stdarg.wit_string qstring qstring qstring let () = - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_tactic printer printer printer + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_tactic printer printer printer + ltop (0,E) let () = - let pr_unit _ _ _ () = str "()" in - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_ltac printer printer pr_unit + let pr_unit _ _ _ _ () = str "()" in + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit + ltop (0,E) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5ecfaf590..bda5774ab 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -40,12 +40,37 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_genarg_pprule_with_level : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer_with_level -> + 'b glob_extra_genarg_printer_with_level -> + 'c extra_genarg_printer_with_level -> + (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit + val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> unit diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index c03a86732..9ae112d37 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -33,7 +33,7 @@ let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_bin let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) (fun c -> - Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in + Genprint.TopPrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in wit (** All the types considered here are base types *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 1a8ec6d6f..e0d7eca5f 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -128,7 +128,7 @@ let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = let wit = Genarg.create_arg "tacvalue" in let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) - (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in + (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -242,9 +242,9 @@ let pr_value env v = | None -> str "a value of type" ++ spc () ++ pr_argument_type v in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) let pr_closure env ist body = @@ -821,9 +821,9 @@ let message_of_value v = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> Ftactic.return (pr ()) - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> Ftactic.return (pr ()) + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded) let interp_message_token ist = function @@ -1353,8 +1353,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = begin let open Genprint in match generic_val_print v with - | PrinterBasic _ -> call_debug None - | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ -> + | TopPrinterBasic _ -> call_debug None + | TopPrinterNeedsContext _ | TopPrinterNeedsContextAndLevel _ -> Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl))) end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval @@ -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/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index f22f00839..e3e749b75 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -152,7 +152,8 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let vars = Univops.universes_of_constr c in + let env = Global.env () in + let vars = Univops.universes_of_constr env c in let univs = Univops.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 20ef65c88..478ba73fd 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -13,7 +13,6 @@ open Util open Names open Globnames open Termops -open Reductionops open Term open EConstr open Vars @@ -207,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = in constrain sigma n c subst -let matches_core env sigma convert allow_partial_app allow_bound_rels +let matches_core env sigma allow_partial_app allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = @@ -216,11 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | ConstRef c, Const (c',_) -> Constant.equal c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' - | _, _ -> - (if convert then - let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma (EConstr.of_constr c') c - else false) + | _, _ -> false in let rec sorec ctx env subst p t = let cT = strip_outer_cast sigma t in @@ -378,14 +373,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma convert allow_partial_app pat c = - let names, subst = matches_core env sigma convert allow_partial_app false pat c in +let matches_core_closed env sigma allow_partial_app pat c = + let names, subst = matches_core env sigma allow_partial_app false pat c in (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma false true true +let extended_matches env sigma = matches_core env sigma true true let matches env sigma pat c = - snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma true (Id.Set.empty,pat) c) let special_meta = (-1) @@ -412,7 +407,7 @@ let matches_head env sigma pat c = (* Tells if it is an authorized occurrence and if the instance is closed *) let authorized_occ env sigma partial_app closed pat c mk_ctx = try - let subst = matches_core_closed env sigma false partial_app pat c in + let subst = matches_core_closed env sigma partial_app pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) @@ -552,10 +547,3 @@ let is_matching_appsubterm ?(closed=true) env sigma pat c = let pat = (Id.Set.empty,pat) in let results = sub_match ~partial_app:true ~closed env sigma pat c in not (IStream.is_empty results) - -let matches_conv env sigma p c = - snd (matches_core_closed env sigma true false (Id.Set.empty,p) c) - -let is_matching_conv env sigma pat n = - try let _ = matches_conv env sigma pat n in true - with PatternMatchingFailure -> false diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 780ccc23d..60e1c34a1 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -55,12 +55,6 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool prefix of it matches against [pat] *) val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool -(** [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) -val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map - (** The type of subterm matching results: a substitution + a context (whose hole is denoted here with [special_meta]) *) type matching_result = @@ -85,8 +79,3 @@ val match_subterm_gen : env -> Evd.evar_map -> (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool - -(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) -val is_matching_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> bool 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/evarconv.ml b/pretyping/evarconv.ml index 18e0c31dd..e5776d2ec 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -310,8 +310,6 @@ let ise_stack2 no_app env evd f sk1 sk2 = | Success i' -> ise_stack2 true i' q1 q2 | UnifFailure _ as x -> fail x else fail (UnifFailure (i,NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else begin match ise_app_stack2 env f i sk1 sk2 with @@ -344,8 +342,6 @@ let exact_ise_stack2 env evd f sk1 sk2 = if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> begin match ise_app_stack2 env f i sk1 sk2 with |_,(UnifFailure _ as x) -> x @@ -457,7 +453,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), + (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 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/pretyping/reductionops.ml b/pretyping/reductionops.ml index ba0502ca4..318176611 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -284,8 +284,6 @@ sig | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list exception IncompatibleFold2 @@ -343,8 +341,6 @@ struct | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list let rec pr_member pr_c member = @@ -367,8 +363,6 @@ struct ++ pr_comma () ++ prlist_with_sep pr_semicolon int remains ++ pr_comma () ++ pr pr_c params ++ str ")" - | Shift i -> str "ZShift(" ++ int i ++ str ")" - | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")" and pr pr_c l = let open Pp in prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l @@ -414,9 +408,6 @@ struct let rec equal_rec sk1 lft1 sk2 lft2 = match sk1,sk2 with | [],[] -> Some (lft1,lft2) - | (Update _ :: _, _ | _, Update _ :: _) -> assert false - | Shift k :: s1, _ -> equal_rec s1 (lft1+k) sk2 lft2 - | _, Shift k :: s2 -> equal_rec sk1 lft1 s2 (lft2+k) | App a1 :: s1, App a2 :: s2 -> let t1,s1' = decomp_node_last a1 s1 in let t2,s2' = decomp_node_last a2 s2 in @@ -449,8 +440,6 @@ struct let rec compare_rec bal stk1 stk2 = match (stk1,stk2) with ([],[]) -> Int.equal bal 0 - | ((Update _|Shift _)::s1, _) -> compare_rec bal s1 stk2 - | (_, (Update _|Shift _)::s2) -> compare_rec bal stk1 s2 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> @@ -472,8 +461,6 @@ struct in match sk1,sk2 with | [], [] -> o,lft1,lft2 - | Shift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2 - | _, Shift n :: q2 -> aux o lft1 sk1 (lft2+n) q2 | App n1 :: q1, App n2 :: q2 -> let t1,l1 = decomp_node_last n1 q1 in let t2,l2 = decomp_node_last n2 q2 in @@ -493,13 +480,12 @@ struct let (o',lft1',lft2') = aux o lft1 (List.rev params1) lft2 (List.rev params2) in aux o' lft1' q1 lft2' q2 - | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> + | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> raise IncompatibleFold2 in aux o 0 (List.rev sk1) 0 (List.rev sk2) let rec map f x = List.map (function - | Update _ -> assert false - | (Proj (_,_,_,_) | Shift _) as e -> e + | (Proj (_,_,_,_)) as e -> e | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) @@ -516,18 +502,15 @@ struct let rec args_size = function | App (i,_,j)::s -> j + 1 - i + args_size s - | Shift(_)::s -> args_size s - | Update(_)::s -> args_size s | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0 let strip_app s = let rec aux out = function - | ( App _ | Shift _ as e) :: s -> aux (e :: out) s + | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s let strip_n_app n s = let rec aux n out = function - | Shift k as e :: s -> aux n (e :: out) s | App (i,a,j) as e :: s -> let nb = j - i + 1 in if n >= nb then @@ -555,8 +538,6 @@ struct let (k,(args',s')) = aux s in let a' = Array.map (Vars.lift k) (Array.sub a i (j - i + 1)) in k,(Array.fold_right (fun x y -> x::y) a' args', s') - | Shift n :: s -> - let (k,(args',s')) = aux s in (k+n,(args', s')) | s -> (0,([],s)) in let (lft,(out,s')) = aux s in let init = match s' with [] when Int.equal lft 0 -> true | _ -> false in @@ -568,20 +549,18 @@ struct | None -> assert false let tail n0 s0 = - let rec aux lft n s = - let out s = if Int.equal lft 0 then s else Shift lft :: s in - if Int.equal n 0 then out s else + let rec aux n s = + if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> let nb = j - i + 1 in if n >= nb then - aux lft (n - nb) s + aux (n - nb) s else let p = i+n in if j >= p then App(p,a,j)::s else s - | Shift k :: s' -> aux (lft+k) n s' | _ -> raise (Invalid_argument "Reductionops.Stack.tail") - in aux 0 n0 s0 + in aux n0 s0 let nth s p = match strip_n_app p s with @@ -627,11 +606,9 @@ struct zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) | f, (Cst (cst,_,_,params,_)::s) -> zip (constr_of_cst_member cst (params @ (append_app [|f|] s))) - | f, (Shift n::s) -> zip (lift n f, s) | f, (Proj (n,m,p,cst_l)::s) when refold -> zip (best_state sigma (mkProj (p,f),s) cst_l) | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s) - | _, (Update _::_) -> assert false in zip s @@ -1074,7 +1051,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (arg, Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') end - |_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false + |_, (Stack.App _)::_ -> assert false |_, _ -> fold () else fold () @@ -1155,7 +1132,7 @@ let local_whd_state_gen flags sigma = |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> let x' = Stack.zip sigma (x,args) in whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s'')) - |_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false + |_, (Stack.App _|Stack.Cst _)::_ -> assert false |_, _ -> s else s @@ -1306,7 +1283,7 @@ let is_transparent e k = (* Conversion utility functions *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t let pb_is_equal pb = pb == Reduction.CONV @@ -1685,7 +1662,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = if isConstruct sigma t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' - |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' + |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts' in whrec csts s let find_conclusion env sigma = diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index db0c29aef..7e12d263a 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -82,8 +82,6 @@ module Stack : sig | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list val pr : ('a -> Pp.t) -> 'a t -> Pp.t @@ -107,7 +105,7 @@ module Stack : sig val append_app_list : 'a list -> 'a t -> 'a t (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App or Shift *) + start by App *) val strip_app : 'a t -> 'a t * 'a t (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option @@ -262,7 +260,7 @@ val is_transparent : Environ.env -> Constant.t tableKey -> bool (** {6 Conversion Functions (uses closures, lazy strategy) } *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb diff --git a/printing/genprint.ml b/printing/genprint.ml index 776a212b5..37a94fe21 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -16,21 +16,27 @@ open Geninterp (* Printing generic values *) -type printer_with_level = +type 'a with_level = { default_already_surrounded : Notation_term.tolerability; default_ensure_surrounded : Notation_term.tolerability; - printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + printer : 'a } type printer_result = | PrinterBasic of (unit -> Pp.t) -| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) -| PrinterNeedsContextAndLevel of printer_with_level +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level -type 'a printer = 'a -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t -type 'a top_printer = 'a -> printer_result +type top_printer_result = +| TopPrinterBasic of (unit -> Pp.t) +| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level -module ValMap = ValTMap (struct type 'a t = 'a -> printer_result end) +type 'a printer = 'a -> printer_result + +type 'a top_printer = 'a -> top_printer_result + +module ValMap = ValTMap (struct type 'a t = 'a -> top_printer_result end) let print0_val_map = ref ValMap.empty @@ -48,32 +54,32 @@ let register_val_print0 s pr = print0_val_map := ValMap.add s pr !print0_val_map let combine_dont_needs pr_pair pr1 = function - | PrinterBasic pr2 -> - PrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ())) - | PrinterNeedsContext pr2 -> - PrinterNeedsContext (fun env sigma -> + | TopPrinterBasic pr2 -> + TopPrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ())) + | TopPrinterNeedsContext pr2 -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 ()) (pr2 env sigma)) - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> - PrinterNeedsContext (fun env sigma -> + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded)) let combine_needs pr_pair pr1 = function - | PrinterBasic pr2 -> - PrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ())) - | PrinterNeedsContext pr2 -> - PrinterNeedsContext (fun env sigma -> + | TopPrinterBasic pr2 -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ())) + | TopPrinterNeedsContext pr2 -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 env sigma)) - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> - PrinterNeedsContext (fun env sigma -> + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded)) let combine pr_pair pr1 v2 = match pr1 with - | PrinterBasic pr1 -> + | TopPrinterBasic pr1 -> combine_dont_needs pr_pair pr1 (generic_val_print v2) - | PrinterNeedsContext pr1 -> + | TopPrinterNeedsContext pr1 -> combine_needs pr_pair pr1 (generic_val_print v2) - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded) (generic_val_print v2) @@ -81,14 +87,14 @@ let _ = let pr_cons a b = Pp.(a ++ spc () ++ b) in register_val_print0 Val.typ_list (function - | [] -> PrinterBasic mt + | [] -> TopPrinterBasic mt | a::l -> List.fold_left (combine pr_cons) (generic_val_print a) l) let _ = register_val_print0 Val.typ_opt (function - | None -> PrinterBasic Pp.mt + | None -> TopPrinterBasic Pp.mt | Some v -> generic_val_print v) let _ = @@ -99,9 +105,9 @@ let _ = (* Printing generic arguments *) type ('raw, 'glb, 'top) genprinter = { - raw : 'raw printer; - glb : 'glb printer; - top : 'top -> printer_result; + raw : 'raw -> printer_result; + glb : 'glb -> printer_result; + top : 'top -> top_printer_result; } module PrintObj = @@ -112,9 +118,9 @@ struct | ExtraArg tag -> let name = ArgT.repr tag in let printer = { - raw = (fun _ -> str "<genarg:" ++ str name ++ str ">"); - glb = (fun _ -> str "<genarg:" ++ str name ++ str ">"); - top = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); + raw = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); + glb = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); + top = (fun _ -> TopPrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); } in Some printer | _ -> assert false diff --git a/printing/genprint.mli b/printing/genprint.mli index 2da9bbc36..baa60fcb2 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -10,19 +10,25 @@ open Genarg -type printer_with_level = +type 'a with_level = { default_already_surrounded : Notation_term.tolerability; default_ensure_surrounded : Notation_term.tolerability; - printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + printer : 'a } type printer_result = | PrinterBasic of (unit -> Pp.t) -| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) -| PrinterNeedsContextAndLevel of printer_with_level +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level -type 'a printer = 'a -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t -type 'a top_printer = 'a -> printer_result +type top_printer_result = +| TopPrinterBasic of (unit -> Pp.t) +| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level + +type 'a printer = 'a -> printer_result + +type 'a top_printer = 'a -> top_printer_result val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer (** Printer for raw level generic arguments. *) @@ -34,7 +40,7 @@ val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer (** Printer for top level generic arguments. *) val register_print0 : ('raw, 'glb, 'top) genarg_type -> - 'raw printer -> 'glb printer -> ('top -> printer_result) -> unit + 'raw printer -> 'glb printer -> 'top top_printer -> unit val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type -> 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/pputils.ml b/printing/pputils.ml index 12d5338ad..a544b4762 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -130,7 +130,10 @@ let rec pr_raw_generic env (GenArg (Rawwit wit, x)) = let q = in_gen (rawwit wit2) q in hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q]) | ExtraArg s -> - Genprint.generic_raw_print (in_gen (rawwit wit) x) + let open Genprint in + match generic_raw_print (in_gen (rawwit wit) x) with + | PrinterBasic pp -> pp () + | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded let rec pr_glb_generic env (GenArg (Glbwit wit, x)) = @@ -152,4 +155,7 @@ let rec pr_glb_generic env (GenArg (Glbwit wit, x)) = let ans = pr_sequence (pr_glb_generic env) [p; q] in hov_if_not_empty 0 ans | ExtraArg s -> - Genprint.generic_glb_print (in_gen (glbwit wit) x) + let open Genprint in + match generic_glb_print (in_gen (glbwit wit) x) with + | PrinterBasic pp -> pp () + | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c526ae000..6b503a011 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -140,7 +140,8 @@ 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 + let univs = UState.demote_seff_univs const univs in + 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 2acb678d7..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 diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index c1e1c2eda..167d6bda0 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 @@ -333,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. *) @@ -350,13 +348,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now nf t else t in - let used_univs_body = Univops.universes_of_constr body in - let used_univs_typ = Univops.universes_of_constr typ in - (* Universes for private constants are relevant to the body *) - let used_univs_body = - List.fold_left (fun acc (us,_) -> Univ.LSet.union acc us) - used_univs_body (Safe_typing.universes_of_private eff) - in + let env = Global.env () in + let used_univs_body = Univops.universes_of_constr env body in + let used_univs_typ = Univops.universes_of_constr env typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = UState.const_univ_entry ~poly initial_euctx in @@ -364,7 +358,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in let univs = UState.check_mono_univ_decl ctx_body universe_decl in (initunivs, typ), ((body, univs), eff) @@ -409,7 +403,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) () = diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 059459042..27e99f218 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -37,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 diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 34e517aed..52dc8bfd8 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -40,7 +40,7 @@ val tclEVARUNIVCONTEXT : UState.t -> tactic val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.constraints -> tactic +val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a8ec4d8ca..cab8d7b52 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -102,9 +102,6 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls -let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c -let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c - (********************************************) (* Definition of the most primitive tactics *) (********************************************) @@ -223,8 +220,6 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d9496d2b4..e0fb8fbc5 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,9 +12,7 @@ open Environ open EConstr open Proof_type open Redexpr -open Pattern open Locus -open Ltac_pretype (** Operations for handling terms under a local typing context. *) @@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool - - (** {6 The most primitive tactics. } *) val refiner : rule -> tactic @@ -138,8 +132,6 @@ module New : sig val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr val pf_compute : 'a Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr end 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/vernac_classifier.ml b/stm/vernac_classifier.ml index 1ca572a36..c5ae27a11 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -185,12 +185,12 @@ let rec classify_vernac e = (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ - | VernacSyntaxExtension _ + | VernacSyntaxExtension _ | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) - | VernacProofMode _ + | VernacProofMode _ -> VtSideff [], VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) @@ -201,7 +201,7 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ -> VtUnknown, VtNow + | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 8e851375a..2c8ca1972 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -39,7 +39,6 @@ type testing_function = Evd.evar_map -> EConstr.constr -> bool let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 -let meta3 = mkmeta 3 let op2bool = function Some _ -> true | None -> false @@ -460,22 +459,6 @@ let find_this_eq_data_decompose gl eqn = user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) -let match_eq_nf gls eqn (ref, hetero) = - let n = if hetero then 4 else 3 in - let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in - let pat = mkPattern (mkGAppRef ref args) in - match Id.Map.bindings (pf_matches gls pat eqn) with - | [(m1,t);(m2,x);(m3,y)] -> - assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,pf_whd_all gls x,pf_whd_all gls y) - | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.") - -let dest_nf_eq gls eqn = - try - snd (first_match (match_eq_nf gls eqn) equalities) - with PatternMatchingFailure -> - user_err Pp.(str "Not an equality.") - (*** Sigma-types *) let match_sigma env sigma ex = diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 8ff6fe95c..237ed42d5 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -144,9 +144,6 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool [t,u,T] and a boolean telling if equality is on the left side *) val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr -(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) - (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml index 46b10bf33..cb0bbfd0e 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -334,6 +334,16 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id If it can discriminate then the goal is proved, if not tries to use it as a rewrite rule. It erases the clause which is given as input *) +let dest_nf_eq env sigma t = match EConstr.kind sigma t with +| App (r, [| t; x; y |]) -> + let open Reductionops in + let lazy eq = Coqlib.coq_eq_ref in + if EConstr.is_global sigma eq r then + (t, whd_all env sigma x, whd_all env sigma y) + else user_err Pp.(str "Not an equality.") +| _ -> + user_err Pp.(str "Not an equality.") + let projectAndApply as_mode thin avoid id eqname names depids = let subst_hyp l2r id = tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id))) @@ -344,7 +354,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = let sigma = project gl in (** We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in - let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in + let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in match (EConstr.kind sigma t1, EConstr.kind sigma t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 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/bugs/closed/6323.v b/test-suite/bugs/closed/6323.v new file mode 100644 index 000000000..fdc33befc --- /dev/null +++ b/test-suite/bugs/closed/6323.v @@ -0,0 +1,9 @@ +Goal True. + simple refine (let X : Type := _ in _); + [ abstract exact Set using Set' + | let X' := (eval cbv delta [X] in X) in + clear X; + simple refine (let id' : { x : X' | True } -> X' := _ in _); + [ abstract refine (@proj1_sig _ _) | ] + ]. +Abort. 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.out b/test-suite/output/ltac.out index c5d58ec1e..eb9f57102 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,7 +1,7 @@ The command has indeed failed with message: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := - symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize + symmetry in x, y; auto with z; auto; intros; clearbody x; generalize dependent z The command has indeed failed with message: In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. @@ -32,7 +32,7 @@ nat 0 0 Ltac foo := - let x := intros ** in + let x := intros in let y := intros -> in let v := constr:(nil) in let w := () in 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 87783350a..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)") diff --git a/vernac/classes.ml b/vernac/classes.ml index b80741269..3e47f881c 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -114,9 +114,10 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly evm term termtype = let kind = IsDefinition Instance in - let evm = - let levels = Univ.LSet.union (Univops.universes_of_constr termtype) - (Univops.universes_of_constr term) in + let evm = + let env = Global.env () in + let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) + (Univops.universes_of_constr env term) in Evd.restrict_universe_context evm levels in let uctx = Evd.check_univ_decl ~poly evm decl in @@ -126,7 +127,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 +209,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..23be2c308 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 env !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 env !evdref (EConstr.of_constr body) in + let tyvars = EConstr.universes_of_constr env !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 @@ -317,7 +315,7 @@ let do_assumptions kind nl l = let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in - let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in + let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in uvars, (coe,t,imps)) Univ.LSet.empty l 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 @@ -1190,7 +1188,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in + let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -1223,7 +1221,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Univops.universes_of_constr (List.hd fixdecls) in + let env = Global.env () in + let vars = Univops.universes_of_constr env (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in @@ -1268,7 +1267,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 +1309,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..c7342e6da 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 -> @@ -82,7 +82,7 @@ type one_inductive_impls = val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> + polymorphic -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list (** Registering a mutual inductive definition together with its @@ -96,7 +96,7 @@ val declare_mutual_inductive_with_eliminations : val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit + polymorphic -> private_flag -> Declarations.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) 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/obligations.ml b/vernac/obligations.ml index 1046d68f8..4f011e6ad 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -477,7 +477,10 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in let body = nf body in - let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in + let env = Global.env () in + let uvars = Univ.LSet.union + (Univops.universes_of_constr env typ) + (Univops.universes_of_constr env body) in let uctx = UState.restrict prg.prg_ctx uvars in let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in @@ -833,7 +836,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/record.mli b/vernac/record.mli index 9fdd5e1c4..e632e7bbf 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -15,7 +15,7 @@ val primitive_flag : bool ref val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * - Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list * + Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 6a10eb43a..7e96f28de 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -288,7 +288,6 @@ let init_terminal_output ~color = *) let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning - (* This is specific to the toplevel *) let pr_loc loc = let fname = loc.Loc.fname in @@ -311,17 +310,23 @@ let print_err_exn ?extra any = std_logger ~pre_hdr Feedback.Error msg let with_output_to_file fname func input = - (* XXX FIXME: redirect std_ft *) - (* let old_logger = !logger in *) let channel = open_out (String.concat "." [fname; "out"]) in - (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *) + let old_fmt = !std_ft, !err_ft, !deep_ft in + let new_ft = Format.formatter_of_out_channel channel in + std_ft := new_ft; + err_ft := new_ft; + deep_ft := new_ft; try let output = func input in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; output with reraise -> let reraise = Backtrace.add_backtrace reraise in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; Exninfo.iraise reraise diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f8ec05fdb..63768d9b8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -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 4a1ae14e3..4980333b5 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -12,18 +12,30 @@ type t = { 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 |