diff options
76 files changed, 555 insertions, 463 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 20dac57a77..e56693eac2 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 abbdf22b91..3ed008ff5f 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; @@ -2057,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 @@ -2210,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 = @@ -2775,6 +2781,8 @@ sig end type universe_constraints = Constraints.t + [@@ocaml.deprecated "Use Constraints.t"] + end module UState : @@ -3111,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 @@ -3999,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 = @@ -4964,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 @@ -6070,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 -> @@ -6096,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 : @@ -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" diff --git a/Makefile.install b/Makefile.install index b590aad549..27694106fd 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/configure.ml b/configure.ml index c7d25bfc80..3850f119b2 100644 --- a/configure.ml +++ b/configure.ml @@ -178,6 +178,20 @@ let which prog = let program_in_path prog = try let _ = which prog in true with Not_found -> false +(** Choose a command among a list of candidates + (command name, mandatory arguments, arguments for this test). + Chooses the first one whose execution outputs a non-empty (first) line. + Dies with message [msg] if none is found. *) + +let select_command msg candidates = + let rec search = function + | [] -> die msg + | (p, x, y) :: tl -> + if fst (tryrun p (x @ y)) <> "" + then List.fold_left (Printf.sprintf "%s %s") p x + else search tl + in search candidates + (** As per bug #4828, ocamlfind on Windows/Cygwin barfs if you pass it a quoted path to camlpXo via -pp. So we only quote camlpXo on not Windows, and warn on Windows if the path contains spaces *) @@ -853,9 +867,10 @@ let strip = (** * md5sum command *) let md5sum = - if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"] - then "md5 -q" else "md5sum" - + select_command "Don’t know how to compute MD5 checksums…" [ + "md5sum", [], [ "--version" ]; + "md5", ["-q"], [ "-s" ; "''" ]; + ] (** * Documentation : do we have latex, hevea, ... *) diff --git a/default.nix b/default.nix index 5b5304e5a0..3dd24bac4d 100644 --- a/default.nix +++ b/default.nix @@ -55,6 +55,8 @@ stdenv.mkDerivation rec { ] else []) ++ (if lib.inNixShell then [ ocamlPackages.merlin + ocamlPackages.ocpIndent + ocamlPackages.ocp-index ] else []); src = diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 168a34e6e4..232b8a56e4 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 309050057c..c3ae7552a9 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 fc3cef3426..7bf2c7427d 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 4865be31ec..ed40036012 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 217540cc19..4e8c7e145e 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/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh new file mode 100644 index 0000000000..7e9b5febdd --- /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 6a69c57934..ca3d520c70 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 ecf7880e20..87a8297461 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/engine/eConstr.ml b/engine/eConstr.ml index ea098902a2..d303038c5d 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -645,12 +645,25 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None -let universes_of_constr sigma c = +let 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 (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | 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 diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 3e6a13f709..f54c422adc 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} *) @@ -203,7 +203,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** Gather the universes transitively used in the term, including in the type of evars appearing in it. *) -val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t +val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t (** {6 Substitutions} *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 907f1b1acd..3445b744a1 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -199,9 +199,10 @@ let whd_head_evar sigma c = let meta_counter_summary_name = "meta counter" (* Generator of metavariables *) -let new_meta = - let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in - fun () -> incr meta_ctr; !meta_ctr +let meta_ctr, meta_counter_summary_tag = + Summary.ref_tag 0 ~name:meta_counter_summary_name + +let new_meta () = incr meta_ctr; !meta_ctr let mk_new_meta () = EConstr.mkMeta(new_meta()) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 5fd4634d67..9d0b973a7e 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -236,7 +236,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> val subterm_source : Evar.t -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located -val meta_counter_summary_name : string +val meta_counter_summary_tag : int Summary.Dyn.tag (** Deprecated *) type type_constraint = types option diff --git a/engine/evd.ml b/engine/evd.ml index 45d2a8b084..e33c851f6e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -466,9 +466,8 @@ let add d e i = add_with_name d e i let evar_counter_summary_name = "evar counter" (* Generator of existential names *) -let new_untyped_evar = - let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in - fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr +let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name +let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr let new_evar evd ?name evi = let evk = new_untyped_evar () in diff --git a/engine/evd.mli b/engine/evd.mli index fb5a6cd16e..b28ce2a62d 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 -> @@ -613,7 +613,7 @@ type unsolvability_explanation = SeveralInstancesFound of int (* This stuff is internal and should not be used. Currently a hack in the STM relies on it. *) -val evar_counter_summary_name : string +val evar_counter_summary_tag : int Summary.Dyn.tag (** {5 Deprecated functions} *) val create_evar_defs : evar_map -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index c28e78f7da..6566ad989c 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 = @@ -365,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? *) @@ -552,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 @@ -569,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 2c39e85f77..6657d6047d 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? *) diff --git a/engine/universes.mli b/engine/universes.mli index fc9278eb56..1a98d969b4 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -74,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 9a9ae12cab..df25d87252 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 9af568bcb3..30fcc43681 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 f6f46710c2..a561ea3703 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 cfc0e09a0c..43d7aa3635 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/declare.ml b/interp/declare.ml index 1aeb67afbb..0adad14198 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -560,7 +560,7 @@ let do_universe poly l = 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 = diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml index 1dea6d9e98..b0c1f66613 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/vernacexpr.ml b/intf/vernacexpr.ml index 5c9141fd6f..c7a9db1cbc 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 d5312c5006..7f4b85fd05 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 c44a17df2a..ca79de404d 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 652ed0f9f7..7cc541258d 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 a19f87b05b..8aaeee831b 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 41d6c05eb5..b0f4a1e5f1 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 05a906e28b..573e4c8bde 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 0bfe074860..a30bb37e64 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 b24c20aa02..67df3759ec 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 3a1f2ae00b..781c6bfbcd 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 e4fa65686e..72861f6e48 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 b95388ed03..f71d83d853 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.mli b/kernel/univ.mli index f74f29b2c1..4593944395 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -169,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 +val constraints_of : 'a constrained -> Constraint.t -(** Enforcing constraints. *) - -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 @@ -199,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 @@ -294,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 @@ -307,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 @@ -328,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 @@ -342,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 @@ -350,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 @@ -370,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 @@ -417,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 *) @@ -425,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. *) @@ -449,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 @@ -461,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 @@ -479,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 @@ -494,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 @@ -515,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/dyn.ml b/lib/dyn.ml index 83e673d2c0..64535d35f6 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -55,6 +55,8 @@ sig include PreS module Easy : sig + + val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag val make_dyn : string -> ('a -> t) * (t -> 'a) val inj : 'a -> 'a tag -> t val prj : t -> 'a tag -> 'a option @@ -129,8 +131,9 @@ end include Self module Easy = struct + (* now tags are opaque, we can do the trick *) -let make_dyn (s : string) = +let make_dyn_tag (s : string) = (fun (type a) (tag : a tag) -> let infun : (a -> t) = fun x -> Dyn (tag, x) in let outfun : (t -> a) = fun (Dyn (t, x)) -> @@ -138,9 +141,12 @@ let make_dyn (s : string) = | None -> assert false | Some CSig.Refl -> x in - (infun, outfun)) + infun, outfun, tag) (create s) +let make_dyn (s : string) = + let inf, outf, _ = make_dyn_tag s in inf, outf + let inj x tag = Dyn(tag,x) let prj : type a. t -> a tag -> a option = fun (Dyn(tag',x)) tag -> diff --git a/lib/dyn.mli b/lib/dyn.mli index e0e1a9d140..2206394e2d 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -53,6 +53,7 @@ val dump : unit -> (int * string) list module Easy : sig (* To create a dynamic type on the fly *) + val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag val make_dyn : string -> ('a -> t) * (t -> 'a) (* For types declared with the [create] function above *) diff --git a/library/global.ml b/library/global.ml index 03d7612a44..ce37dfecff 100644 --- a/library/global.ml +++ b/library/global.ml @@ -20,6 +20,7 @@ module GlobalSafeEnv : sig val set_safe_env : Safe_typing.safe_environment -> unit val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit val is_joined_environment : unit -> bool + val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag end = struct @@ -30,9 +31,9 @@ let join_safe_environment ?except () = let is_joined_environment () = Safe_typing.is_joined_environment !global_env - -let () = - Summary.declare_summary global_env_summary_name + +let global_env_summary_tag = + Summary.declare_summary_tag global_env_summary_name { Summary.freeze_function = (function | `Yes -> join_safe_environment (); !global_env | `No -> !global_env @@ -51,6 +52,8 @@ let set_safe_env e = global_env := e end +let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag + let safe_env = GlobalSafeEnv.safe_env let join_safe_environment ?except () = GlobalSafeEnv.join_safe_environment ?except () diff --git a/library/global.mli b/library/global.mli index 1d68d10825..324181e79e 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 @@ -159,4 +159,4 @@ val current_dirpath : unit -> DirPath.t val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a -val global_env_summary_name : string +val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag diff --git a/library/summary.ml b/library/summary.ml index 9f49d1f839..6df17476bd 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -13,17 +13,22 @@ open Util module Dyn = Dyn.Make () type marshallable = [ `Yes | `No | `Shallow ] + type 'a summary_declaration = { freeze_function : marshallable -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit } -let summaries = ref Int.Map.empty +let sum_mod = ref None +let sum_map = ref String.Map.empty let mangle id = id ^ "-SUMMARY" +let unmangle id = String.(sub id 0 (length id - 8)) + +let ml_modules = "ML-MODULES" -let internal_declare_summary hash sumname sdecl = - let (infun, outfun) = Dyn.Easy.make_dyn (mangle sumname) in +let internal_declare_summary fadd sumname sdecl = + let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in let dyn_freeze b = infun (sdecl.freeze_function b) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in @@ -32,140 +37,116 @@ let internal_declare_summary hash sumname sdecl = unfreeze_function = dyn_unfreeze; init_function = dyn_init } in - summaries := Int.Map.add hash (sumname, ddecl) !summaries + fadd sumname ddecl; + tag -let all_declared_summaries = ref Int.Set.empty +let declare_ml_modules_summary decl = + let ml_add _ ddecl = sum_mod := Some ddecl in + internal_declare_summary ml_add ml_modules decl -let summary_names = ref [] -let name_of_summary name = - try List.assoc name !summary_names - with Not_found -> "summary name not found" +let declare_ml_modules_summary decl = + ignore(declare_ml_modules_summary decl) -let declare_summary sumname decl = - let hash = String.hash sumname in - let () = if Int.Map.mem hash !summaries then - let (name, _) = Int.Map.find hash !summaries in - anomaly ~label:"Summary.declare_summary" - (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name ++ str ".") +let declare_summary_tag sumname decl = + let fadd name ddecl = sum_map := String.Map.add name ddecl !sum_map in + let () = if String.Map.mem sumname !sum_map then + anomaly ~label:"Summary.declare_summary" + (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str sumname ++ str ".") in - all_declared_summaries := Int.Set.add hash !all_declared_summaries; - summary_names := (hash, sumname) :: !summary_names; - internal_declare_summary hash sumname decl + internal_declare_summary fadd sumname decl + +let declare_summary sumname decl = + ignore(declare_summary_tag sumname decl) type frozen = { - summaries : (int * Dyn.t) list; + summaries : Dyn.t String.Map.t; (** Ordered list w.r.t. the first component. *) ml_module : Dyn.t option; (** Special handling of the ml_module summary. *) } -let empty_frozen = { summaries = []; ml_module = None; } - -let ml_modules = "ML-MODULES" -let ml_modules_summary = String.hash ml_modules +let empty_frozen = { summaries = String.Map.empty; ml_module = None } let freeze_summaries ~marshallable : frozen = - let fold id (_, decl) accu = - (* to debug missing Lazy.force - if marshallable <> `No then begin - let id, _ = Int.Map.find id !summaries in - prerr_endline ("begin marshalling " ^ id); - ignore(Marshal.to_string (decl.freeze_function marshallable) []); - prerr_endline ("end marshalling " ^ id); - end; - /debug *) - let state = decl.freeze_function marshallable in - if Int.equal id ml_modules_summary then { accu with ml_module = Some state } - else { accu with summaries = (id, state) :: accu.summaries } + let smap decl = decl.freeze_function marshallable in + { summaries = String.Map.map smap !sum_map; + ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod; + } + +let unfreeze_single name state = + let decl = + try String.Map.find name !sum_map + with + | Not_found -> + CErrors.anomaly Pp.(str "trying to unfreeze unregistered summary " ++ str name) in - Int.Map.fold_right fold !summaries empty_frozen - -let unfreeze_summaries fs = + try decl.unfreeze_function state + with e when CErrors.noncritical e -> + let e = CErrors.push e in + Feedback.msg_warning + Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]); + iraise e + +let unfreeze_summaries ?(partial=false) { summaries; ml_module } = (* The unfreezing of [ml_modules_summary] has to be anticipated since it - * may modify the content of [summaries] ny loading new ML modules *) - let (_, decl) = - try Int.Map.find ml_modules_summary !summaries - with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".") - in - let () = match fs.ml_module with + * may modify the content of [summaries] by loading new ML modules *) + begin match !sum_mod with | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".") - | Some state -> decl.unfreeze_function state - in - let fold id (_, decl) states = - if Int.equal id ml_modules_summary then states - else match states with - | [] -> - let () = decl.init_function () in - [] - | (nid, state) :: rstates -> - if Int.equal id nid then - let () = decl.unfreeze_function state in rstates - else - let () = decl.init_function () in states + | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module + end; + (** We must be independent on the order of the map! *) + let ufz name decl = + try decl.unfreeze_function String.Map.(find name summaries) + with Not_found -> + if not partial then begin + Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name); + decl.init_function () + end; in - let fold id decl state = - try fold id decl state - with e when CErrors.noncritical e -> - let e = CErrors.push e in - Feedback.msg_error - Pp.(seq [str "Error unfreezing summary %s\n%s\n%!"; - str (name_of_summary id); - CErrors.iprint e]); - iraise e - in - (** We rely on the order of the frozen list, and the order of folding *) - ignore (Int.Map.fold_left fold !summaries fs.summaries) + (* String.Map.iter unfreeze_single !sum_map *) + String.Map.iter ufz !sum_map let init_summaries () = - Int.Map.iter (fun _ (_, decl) -> decl.init_function ()) !summaries + String.Map.iter (fun _ decl -> decl.init_function ()) !sum_map (** For global tables registered statically before the end of coqtop launch, the following empty [init_function] could be used. *) let nop () = () -(** Selective freeze *) +(** Summary projection *) +let project_from_summary { summaries } tag = + let id = unmangle (Dyn.repr tag) in + let state = String.Map.find id summaries in + Option.get (Dyn.Easy.prj state tag) + +let modify_summary st tag v = + let id = unmangle (Dyn.repr tag) in + let summaries = String.Map.set id (Dyn.Easy.inj v tag) st.summaries in + {st with summaries} -type frozen_bits = (int * Dyn.t) list +let remove_from_summary st tag = + let id = unmangle (Dyn.repr tag) in + let summaries = String.Map.remove id st.summaries in + {st with summaries} + +(** Selective freeze *) -let ids_of_string_list complement ids = - if not complement then List.map String.hash ids - else - let fold accu id = - let id = String.hash id in - Int.Set.remove id accu - in - let ids = List.fold_left fold !all_declared_summaries ids in - Int.Set.elements ids +type frozen_bits = Dyn.t String.Map.t let freeze_summary ~marshallable ?(complement=false) ids = - let ids = ids_of_string_list complement ids in - List.map (fun id -> - let (_, summary) = Int.Map.find id !summaries in - id, summary.freeze_function marshallable) - ids - -let unfreeze_summary datas = - List.iter - (fun (id, data) -> - let (name, summary) = Int.Map.find id !summaries in - try summary.unfreeze_function data - with e -> - let e = CErrors.push e in - prerr_endline ("Exception unfreezing " ^ name); - iraise e) - datas + let sub_map = String.Map.filter (fun id _ -> complement <> List.(mem id ids)) !sum_map in + String.Map.map (fun decl -> decl.freeze_function marshallable) sub_map + +let unfreeze_summary = String.Map.iter unfreeze_single let surgery_summary { summaries; ml_module } bits = - let summaries = List.map (fun (id, _ as orig) -> - try id, List.assoc id bits - with Not_found -> orig) - summaries in + let summaries = + String.Map.fold (fun hash state sum -> String.Map.set hash state sum ) summaries bits in { summaries; ml_module } let project_summary { summaries; ml_module } ?(complement=false) ids = - let ids = ids_of_string_list complement ids in - List.filter (fun (id, _) -> List.mem id ids) summaries + String.Map.filter (fun name _ -> complement <> List.(mem name ids)) summaries let pointer_equal l1 l2 = let ptr_equal d1 d2 = @@ -174,19 +155,22 @@ let pointer_equal l1 l2 = match Dyn.eq t1 t2 with | None -> false | Some Refl -> x1 == x2 - in + in + let l1, l2 = String.Map.bindings l1, String.Map.bindings l2 in CList.for_all2eq (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2 (** All-in-one reference declaration + registration *) -let ref ?(freeze=fun _ r -> r) ~name x = +let ref_tag ?(freeze=fun _ r -> r) ~name x = let r = ref x in - declare_summary name + let tag = declare_summary_tag name { freeze_function = (fun b -> freeze b !r); unfreeze_function = ((:=) r); - init_function = (fun () -> r := x) }; - r + init_function = (fun () -> r := x) } in + r, tag + +let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x module Local = struct @@ -198,8 +182,7 @@ let (!) r = let key, name = !r in try CEphemeron.get key with CEphemeron.InvalidKey -> - let _, { init_function } = - Int.Map.find (String.hash (mangle name)) !summaries in + let { init_function } = String.Map.find name !sum_map in init_function (); CEphemeron.get (fst !r) diff --git a/library/summary.mli b/library/summary.mli index d093d95f29..09447199e5 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -36,6 +36,12 @@ type 'a summary_declaration = { val declare_summary : string -> 'a summary_declaration -> unit +(** We provide safe projection from the summary to the types stored in + it.*) +module Dyn : Dyn.S + +val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag + (** All-in-one reference declaration + summary registration. It behaves just as OCaml's standard [ref] function, except that a [declare_summary] is done, with [name] as string. @@ -43,6 +49,7 @@ val declare_summary : string -> 'a summary_declaration -> unit The [freeze_function] can be overridden *) val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref +val ref_tag : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag (* As [ref] but the value is local to a process, i.e. not sent to, say, proof * workers. It is useful to implement a local cache for example. *) @@ -55,10 +62,11 @@ module Local : sig end -(** Special name for the summary of ML modules. This summary entry is - special because its unfreeze may load ML code and hence add summary - entries. Thus is has to be recognizable, and handled appropriately *) -val ml_modules : string +(** Special summary for ML modules. This summary entry is special + because its unfreeze may load ML code and hence add summary + entries. Thus is has to be recognizable, and handled properly. + *) +val declare_ml_modules_summary : 'a summary_declaration -> unit (** For global tables registered statically before the end of coqtop launch, the following empty [init_function] could be used. *) @@ -72,19 +80,34 @@ type frozen val empty_frozen : frozen val freeze_summaries : marshallable:marshallable -> frozen -val unfreeze_summaries : frozen -> unit +val unfreeze_summaries : ?partial:bool -> frozen -> unit val init_summaries : unit -> unit -(** The type [frozen_bits] is a snapshot of some of the registered tables *) +(** Typed projection of the summary. Experimental API, use with CARE *) + +val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen +val project_from_summary : frozen -> 'a Dyn.tag -> 'a +val remove_from_summary : frozen -> 'a Dyn.tag -> frozen + +(** The type [frozen_bits] is a snapshot of some of the registered + tables. It is DEPRECATED in favor of the typed projection + version. *) + type frozen_bits +[@@ocaml.deprecated "Please use the typed version of summary projection"] -val freeze_summary : - marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits +[@@@ocaml.warning "-3"] +val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits +[@@ocaml.deprecated "Please use the typed version of summary projection"] val unfreeze_summary : frozen_bits -> unit +[@@ocaml.deprecated "Please use the typed version of summary projection"] val surgery_summary : frozen -> frozen_bits -> frozen +[@@ocaml.deprecated "Please use the typed version of summary projection"] val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits +[@@ocaml.deprecated "Please use the typed version of summary projection"] val pointer_equal : frozen_bits -> frozen_bits -> bool +[@@ocaml.deprecated "Please use the typed version of summary projection"] +[@@@ocaml.warning "+3"] (** {6 Debug} *) - val dump : unit -> (int * string) list diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8e6a01aa3b..b766f0c6bb 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -611,8 +611,8 @@ let unfreeze (grams, lex) = the lexer state should not be resetted, since it contains keywords declared in g_*.ml4 *) -let _ = - Summary.declare_summary "GRAMMAR_LEXER" +let parser_summary_tag = + Summary.declare_summary_tag "GRAMMAR_LEXER" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = Summary.nop } diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d17ccb0b41..3ca013a968 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -313,3 +313,6 @@ val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b (** Location Utils *) val to_coqloc : Ploc.t -> Loc.t val (!@) : Ploc.t -> Loc.t + +type frozen_t +val parser_summary_tag : frozen_t Summary.Dyn.tag diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b0a76137b7..766adfc63a 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 34fea6175b..8b9eb39837 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/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index f22f00839a..e3e749b754 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 20ef65c884..478ba73fd5 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 780ccc23d1..60e1c34a15 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/reductionops.ml b/pretyping/reductionops.ml index 2f8e5b9643..3181766112 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1283,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 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 34fdbe8583..7e12d263aa 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -260,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/proofs/pfedit.ml b/proofs/pfedit.ml index 31a73db04f..6b503a0112 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -140,6 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in Proof_global.discard_current (); + let univs = UState.demote_seff_univs const univs in const, status, univs with reraise -> let reraise = CErrors.push reraise in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 535ef2013d..167d6bda0d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -348,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 @@ -362,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) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 34e517aedc..52dc8bfd8c 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 a8ec4d8ca3..cab8d7b52a 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 d9496d2b4f..e0fb8fbc5d 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/stm.ml b/stm/stm.ml index 8aa832da84..0dbe168b73 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -158,9 +158,10 @@ let mkTransCmd cast cids ceff cqueue = Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff } (* Parts of the system state that are morally part of the proof state *) -let summary_pstate = [ Evarutil.meta_counter_summary_name; - Evd.evar_counter_summary_name; - "program-tcc-table" ] +let summary_pstate = Evarutil.meta_counter_summary_tag, + Evd.evar_counter_summary_tag, + Obligations.program_tcc_summary_tag + type cached_state = | Empty | Error of Exninfo.iexn @@ -762,15 +763,21 @@ end = struct (* {{{ *) let fix_exn_ref = ref (fun x -> x) type proof_part = - Proof_global.t * Summary.frozen_bits (* only meta counters *) + Proof_global.t * + int * (* Evarutil.meta_counter_summary_tag *) + int * (* Evd.evar_counter_summary_tag *) + Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) type partial_state = [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] let proof_part_of_frozen { Vernacstate.proof; system } = + let st = States.summary_of_state system in proof, - Summary.project_summary (States.summary_of_state system) summary_pstate + Summary.project_from_summary st Util.(pi1 summary_pstate), + Summary.project_from_summary st Util.(pi2 summary_pstate), + Summary.project_from_summary st Util.(pi3 summary_pstate) let freeze marshallable id = VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) @@ -830,16 +837,21 @@ end = struct (* {{{ *) else s with VCS.Expired -> s in VCS.set_state id (Valid s) - | `ProofOnly(ontop,(pstate,counters)) -> + | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in let s = { s with system = States.replace_summary s.system - (Summary.surgery_summary - (States.summary_of_state s.system) - counters) } in + begin + let st = States.summary_of_state s.system in + let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in + let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in + let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in + st + end + } in VCS.set_state id (Valid s) with VCS.Expired -> () @@ -854,10 +866,10 @@ end = struct (* {{{ *) let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } = let s1 = States.summary_of_state s1 in - let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in + let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in let s2 = States.summary_of_state s2 in - let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in - Summary.pointer_equal e1 e2 + let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in + e1 == e2 let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id @@ -2040,8 +2052,6 @@ and Reach : sig end = struct (* {{{ *) -let pstate = summary_pstate - let async_policy () = let open Flags in if is_universe_polymorphism () then false @@ -2254,10 +2264,14 @@ let known_state ?(redefine_qed=false) ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) let cherry_pick_non_pstate () = - Summary.freeze_summary ~marshallable:`No ~complement:true pstate, - Lib.freeze ~marshallable:`No in + let st = Summary.freeze_summaries ~marshallable:`No in + let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in + let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in + let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in + st, Lib.freeze ~marshallable:`No in + let inject_non_pstate (s,l) = - Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () + Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate safe_id id = stm_purify (fun id -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 1ca572a36c..c5ae27a110 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 8e851375a6..2c8ca19722 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 8ff6fe95c6..237ed42d55 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 46b10bf33e..cb0bbfd0e7 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/6323.v b/test-suite/bugs/closed/6323.v new file mode 100644 index 0000000000..fdc33befc6 --- /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/vernac/classes.ml b/vernac/classes.ml index cb1d2f7c73..3e47f881c1 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 diff --git a/vernac/command.ml b/vernac/command.ml index 66d4fe9847..23be2c3082 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -105,7 +105,7 @@ 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 = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in + 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), @@ -130,8 +130,8 @@ 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 bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in - let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in + 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 @@ -315,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 @@ -1188,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 @@ -1221,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 diff --git a/vernac/command.mli b/vernac/command.mli index a1f916c782..c7342e6da9 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -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/mltop.ml b/vernac/mltop.ml index d3de10235f..00554e3bae 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -378,7 +378,7 @@ let unfreeze_ml_modules x = (fun (name,path) -> trigger_ml_object false false false ?path name) x let _ = - Summary.declare_summary Summary.ml_modules + Summary.declare_ml_modules_summary { Summary.freeze_function = (fun _ -> get_loaded_modules ()); Summary.unfreeze_function = unfreeze_ml_modules; Summary.init_function = reset_loaded_modules } diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 24d6649515..181068089e 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -429,8 +429,8 @@ let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let from_prg : program_info ProgMap.t ref = - Summary.ref ProgMap.empty ~name:"program-tcc-table" +let from_prg, program_tcc_summary_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" let close sec = if not (ProgMap.is_empty !from_prg) then @@ -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 diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 0602e52e9a..bdc97d48c0 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -104,3 +104,6 @@ exception NoObligations of Names.Id.t option val explain_no_obligations : Names.Id.t option -> Pp.t val set_program_mode : bool -> unit + +type program_info +val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag diff --git a/vernac/record.mli b/vernac/record.mli index 9fdd5e1c46..e632e7bbff 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 6a10eb43a2..7e96f28de4 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 |