diff options
116 files changed, 959 insertions, 744 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 20dac57a7..e56693eac 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -268,7 +268,7 @@ ci-color: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES subversion" + EXTRA_PACKAGES: "$TIMING_PACKAGES" ci-compcert: <<: *ci-template diff --git a/API/API.mli b/API/API.mli index abbdf22b9..c5a1743f7 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 = @@ -4793,7 +4801,7 @@ sig | IntroNeedsProduct | DoesNotOccurIn of Constr.t * Names.Id.t | NoSuchHyp of Names.Id.t - exception RefinerError of refiner_error + exception RefinerError of Environ.env * Evd.evar_map * refiner_error val catchable_exception : exn -> bool end @@ -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.build b/Makefile.build index f11719c07..940943c41 100644 --- a/Makefile.build +++ b/Makefile.build @@ -494,7 +494,7 @@ $(COQDOC): $(call bestobj, $(COQDOCCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -package str,unix) -$(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) +$(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(SYSMOD)) diff --git a/Makefile.install b/Makefile.install index 750d57ba0..84aa11a5e 100644 --- a/Makefile.install +++ b/Makefile.install @@ -101,11 +101,15 @@ 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) $(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 3ce0b03d7..2292913d5 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 *) @@ -851,9 +865,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 5b5304e5a..3dd24bac4 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 168a34e6e..232b8a56e 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -115,7 +115,8 @@ ######################################################################## # CoLoR ######################################################################## -: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} +: ${CoLoR_CI_BRANCH:=master} +: ${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git} ######################################################################## # SF diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 309050057..c3ae7552a 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,33 +3,11 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -Color_CI_DIR=${CI_BUILD_DIR}/color +CoLoR_CI_DIR=${CI_BUILD_DIR}/color # Setup Bignums - source ${ci_dir}/ci-bignums.sh -# Compiles CoLoR - -svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} - -sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v - -# Adapt to PR #220 (FunInd not loaded in Prelude anymore) -sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v -sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v -sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v -sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v -sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v -sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v -sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v -sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v -sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v -sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v -sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v -sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v - -( cd ${Color_CI_DIR} && make ) +# Compile CoLoR +git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR} +( cd ${CoLoR_CI_DIR} && make ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index 4865be31e..ed4003601 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph +ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2 git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR} diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 217540cc1..4e8c7e145 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,13 +3,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: Needs fixing to properly set the build directory. -wget ${sf_lf_CI_TARURL} -wget ${sf_plf_CI_TARURL} -wget ${sf_vfa_CI_TARURL} -tar xvfz lf.tgz -tar xvfz plf.tgz -tar xvfz vfa.tgz +mkdir -p ${CI_BUILD_DIR} && cd ${CI_BUILD_DIR} +wget -qO- ${sf_lf_CI_TARURL} | tar xvz +wget -qO- ${sf_plf_CI_TARURL} | tar xvz +wget -qO- ${sf_vfa_CI_TARURL} | tar xvz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh new file mode 100644 index 000000000..7e9b5febd --- /dev/null +++ b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then + Equations_CI_BRANCH=fix-coq-6324 + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git +fi diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt index 6a69c5793..ca3d520c7 100644 --- a/dev/doc/univpoly.txt +++ b/dev/doc/univpoly.txt @@ -12,7 +12,7 @@ type pinductive = inductive puniverses type pconstructor = constructor puniverses type constr = ... - | Const of puniversess + | Const of puniverses | Ind of pinductive | Constr of pconstructor | Proj of constant * constr diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index ecf7880e2..87a829746 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -11,6 +11,13 @@ CODE=0 if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ]; then + # skip PRs from before the linter existed + if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ]; + then + 2>&1 echo "Linting skipped: pull request older than the linter." + exit 0 + fi + # Some problems are too widespread to fix in one commit, but we # can still check that they don't worsen. CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*} diff --git a/engine/eConstr.ml b/engine/eConstr.ml index ea098902a..d303038c5 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 3e6a13f70..f54c422ad 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -187,9 +187,9 @@ val whd_evar : Evd.evar_map -> constr -> constr val eq_constr : Evd.evar_map -> t -> t -> bool val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool -val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option -val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option -val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option +val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option +val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option +val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool (** {6 Iterators} *) @@ -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 907f1b1ac..3445b744a 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 5fd4634d6..9d0b973a7 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 45d2a8b08..e33c851f6 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 fb5a6cd16..b28ce2a62 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 9510371be..6131f4c03 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 2c39e85f7..6657d6047 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -53,7 +53,7 @@ val algebraics : t -> Univ.LSet.t (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) -val constraints : t -> Univ.constraints +val constraints : t -> Univ.Constraint.t (** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *) val context : t -> Univ.UContext.t @@ -68,12 +68,12 @@ val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes (** {5 Constraints handling} *) -val add_constraints : t -> Univ.constraints -> t +val add_constraints : t -> Univ.Constraint.t -> t (** @raise UniversesDiffer when universes differ *) -val add_universe_constraints : t -> Universes.universe_constraints -> t +val add_universe_constraints : t -> Universes.Constraints.t -> t (** @raise UniversesDiffer when universes differ *) @@ -87,6 +87,8 @@ val universe_of_name : t -> Id.t -> Univ.Level.t val restrict : t -> Univ.LSet.t -> t +val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t + type rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) diff --git a/engine/universes.mli b/engine/universes.mli index fc9278eb5..1a98d969b 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 9a9ae12ca..df25d8725 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -9,12 +9,25 @@ open Univ open Constr -let universes_of_constr c = +let universes_of_constr env c = + let open Declarations in let rec aux s c = match kind c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> + | Const (c, u) -> + begin match (Environ.lookup_constant c env).const_universes with + | Polymorphic_const _ -> + LSet.fold LSet.add (Instance.levels u) s + | Monomorphic_const (univs, _) -> + LSet.union s univs + end + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + begin match (Environ.lookup_mind mind env).mind_universes with + | Cumulative_ind _ | Polymorphic_ind _ -> + LSet.fold LSet.add (Instance.levels u) s + | Monomorphic_ind (univs,_) -> + LSet.union s univs + end + | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s | _ -> Constr.fold aux s c diff --git a/engine/univops.mli b/engine/univops.mli index 9af568bcb..30fcc4368 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -9,7 +9,8 @@ open Constr open Univ -(** Shrink a universe context to a restricted set of variables *) +(** The universes of monomorphic constants appear. *) +val universes_of_constr : Environ.env -> constr -> LSet.t -val universes_of_constr : constr -> LSet.t +(** Shrink a universe context to a restricted set of variables *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index f6f46710c..a561ea370 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -82,7 +82,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, ploc_vala None, - <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>) let make_fun_clauses loc s l = let map c = diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index cfc0e09a0..58599a14d 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -13,7 +13,6 @@ open Util open Pp open Printer -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration @@ -377,15 +376,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); @@ -517,7 +509,7 @@ let rec parse = function let () = Coqtop.toploop_init := (fun args -> let args = parse args in Flags.quiet := true; - CoqworkmgrApi.(init Flags.High); + CoqworkmgrApi.(init High); args) let () = Coqtop.toploop_run := loop diff --git a/interp/declare.ml b/interp/declare.ml index 1aeb67afb..0adad1419 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 1dea6d9e9..b0c1f6661 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -75,7 +75,8 @@ type logical_kind = (** Recursive power of type declarations *) -type recursivity_kind = +type recursivity_kind = Declarations.recursivity_kind = | Finite (** = inductive *) | CoFinite (** = coinductive *) | BiFinite (** = non-recursive, like in "Record" definitions *) +[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 5c9141fd6..c7a9db1cb 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -145,7 +145,7 @@ type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) -type inductive_flag = Decl_kinds.recursivity_kind +type inductive_flag = Declarations.recursivity_kind type onlyparsing_flag = Flags.compat_version option (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version @@ -482,18 +482,39 @@ and vernac_argument_status = { implicit_status : vernac_implicit_status; } -(* A vernac classifier has to tell if a command: - vernac_when: has to be executed now (alters the parser) or later - vernac_type: if it is starts, ends, continues a proof or +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. + + - vernac_type: if it is starts, ends, continues a proof or alters the global state or is a control command like BackTo or is - a query like Check *) + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) type vernac_type = + (* Start of a proof *) | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) | VtSideff of vernac_sideff_type + (* End of a proof *) | VtQed of vernac_qed_type + (* A proof step *) | VtProofStep of proof_step + (* To be removed *) | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) | VtQuery of vernac_part_of_script * Feedback.route_id + (* To be removed *) | VtMeta | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d5312c500..7f4b85fd0 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -172,13 +172,18 @@ type abstract_inductive_universes = | Polymorphic_ind of Univ.AUContext.t | Cumulative_ind of Univ.ACumulativityInfo.t +type recursivity_kind = + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) + type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) mind_record : record_body option; (** The record information *) - mind_finite : Decl_kinds.recursivity_kind; (** Whether the type is inductive or coinductive *) + mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) diff --git a/kernel/entries.ml b/kernel/entries.ml index c44a17df2..ca79de404 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -51,7 +51,7 @@ type mutual_inductive_entry = { (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; diff --git a/kernel/environ.mli b/kernel/environ.mli index 652ed0f9f..7cc541258 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -152,9 +152,9 @@ exception NotEvaluableConst of const_evaluation_result val constant_value : env -> Constant.t puniverses -> constr constrained val constant_type : env -> Constant.t puniverses -> types constrained -val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.constraints) option +val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.Constraint.t) option val constant_value_and_type : env -> Constant.t puniverses -> - constr option * types * Univ.constraints + constr option * types * Univ.Constraint.t (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t @@ -203,10 +203,10 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** Add universe constraints to the environment. @raises UniverseInconsistency *) -val add_constraints : Univ.constraints -> env -> env +val add_constraints : Univ.Constraint.t -> env -> env (** Check constraints are satifiable in the environment. *) -val check_constraints : Univ.constraints -> env -> bool +val check_constraints : Univ.Constraint.t -> env -> bool val push_context : ?strict:bool -> Univ.UContext.t -> env -> env val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env diff --git a/kernel/inductive.mli b/kernel/inductive.mli index a19f87b05..8aaeee831 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -37,7 +37,7 @@ val ind_subst : MutInd.t -> mutual_inductive_body -> Instance.t -> constr list val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t val instantiate_inductive_constraints : - mutual_inductive_body -> Instance.t -> constraints + mutual_inductive_body -> Instance.t -> Constraint.t val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ca67c5f13..c07ac973b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -212,7 +212,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare env pb s0 s1 u, check) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 05a906e28..573e4c8bd 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -49,7 +49,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 0bfe07486..a30bb37e6 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -139,7 +139,7 @@ val push_context : bool -> Univ.UContext.t -> safe_transformer0 val add_constraints : - Univ.constraints -> safe_transformer0 + Univ.Constraint.t -> safe_transformer0 (* (\** Generator of universes *\) *) (* val next_universe : int safe_transformer *) diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index b24c20aa0..67df3759e 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -10,4 +10,4 @@ open Univ open Declarations open Environ -val check_subtypes : env -> module_type_body -> module_type_body -> constraints +val check_subtypes : env -> module_type_body -> module_type_body -> Constraint.t diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 3a1f2ae00..781c6bfbc 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -59,7 +59,7 @@ type ('constr, 'types) ptype_error = | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array - | UnsatisfiedConstraints of Univ.constraints + | UnsatisfiedConstraints of Univ.Constraint.t type type_error = (constr, types) ptype_error diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index e4fa65686..72861f6e4 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -60,7 +60,7 @@ type ('constr, 'types) ptype_error = | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array - | UnsatisfiedConstraints of Univ.constraints + | UnsatisfiedConstraints of Univ.Constraint.t type type_error = (constr, types) ptype_error @@ -105,4 +105,4 @@ val error_ill_typed_rec_body : val error_elim_explain : Sorts.family -> Sorts.family -> arity_error -val error_unsatisfied_constraints : env -> Univ.constraints -> 'a +val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index b95388ed0..f71d83d85 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -35,10 +35,10 @@ val check_eq_instances : Instance.t check_function constraints are not satisfiable. *) val enforce_constraint : univ_constraint -> t -> t -val merge_constraints : constraints -> t -> t +val merge_constraints : Constraint.t -> t -> t val check_constraint : t -> univ_constraint -> bool -val check_constraints : constraints -> t -> bool +val check_constraints : Constraint.t -> t -> bool (** Adds a universe to the graph, ensuring it is >= or > Set. @raises AlreadyDeclared if the level is already declared in the graph. *) @@ -57,7 +57,7 @@ val empty_universes : t val sort_universes : t -> t -val constraints_of_universes : t -> constraints +val constraints_of_universes : t -> Constraint.t val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of diff --git a/kernel/univ.mli b/kernel/univ.mli index f74f29b2c..459394439 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/control.ml b/lib/control.ml index d936d7557..c6489938e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -12,15 +12,12 @@ let interrupt = ref false let steps = ref 0 -let are_we_threading = lazy ( - match !Flags.async_proofs_mode with - | Flags.APon -> true - | _ -> false) +let enable_thread_delay = ref false let check_for_interrupt () = if !interrupt then begin interrupt := false; raise Sys.Break end; incr steps; - if !steps = 1000 && Lazy.force are_we_threading then begin + if !enable_thread_delay && !steps = 1000 then begin Thread.delay 0.001; steps := 0; end diff --git a/lib/control.mli b/lib/control.mli index f6c63ffb3..261b07693 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -8,6 +8,9 @@ (** Global control of Coq. *) +(** Will periodically call [Thread.delay] if set to true *) +val enable_thread_delay : bool ref + val interrupt : bool ref (** Coq interruption: set the following boolean reference to interrupt Coq (it eventually raises [Break], simulating a Ctrl-C) *) diff --git a/lib/dyn.ml b/lib/dyn.ml index 83e673d2c..64535d35f 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 e0e1a9d14..2206394e2 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/lib/flags.ml b/lib/flags.ml index 97795faa6..9631da633 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -35,36 +35,10 @@ let record_aux_file = ref false let test_mode = ref false -type async_proofs = APoff | APonLazy | APon -let async_proofs_mode = ref APoff -type cache = Force -let async_proofs_cache = ref None -let async_proofs_n_workers = ref 1 -let async_proofs_n_tacworkers = ref 2 -let async_proofs_private_flags = ref None -let async_proofs_full = ref false -let async_proofs_never_reopen_branch = ref false -let async_proofs_flags_for_workers = ref [] let async_proofs_worker_id = ref "master" -type priority = Low | High -let async_proofs_worker_priority = ref Low -let string_of_priority = function Low -> "low" | High -> "high" -let priority_of_string = function - | "low" -> Low - | "high" -> High - | _ -> raise (Invalid_argument "priority_of_string") -type tac_error_filter = [ `None | `Only of string list | `All ] -let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) -let async_proofs_cmd_error_resilience = ref true - -let async_proofs_is_worker () = - !async_proofs_worker_id <> "master" -let async_proofs_is_master () = - !async_proofs_mode = APon && !async_proofs_worker_id = "master" -let async_proofs_delegation_threshold = ref 0.03 +let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let debug = ref false -let stm_debug = ref false let in_debugger = ref false let in_toplevel = ref false diff --git a/lib/flags.mli b/lib/flags.mli index e4710a126..1b1e264f0 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -21,35 +21,14 @@ val record_aux_file : bool ref val test_mode : bool ref (** Async-related flags *) -type async_proofs = APoff | APonLazy | APon -val async_proofs_mode : async_proofs ref -type cache = Force -val async_proofs_cache : cache option ref -val async_proofs_n_workers : int ref -val async_proofs_n_tacworkers : int ref -val async_proofs_private_flags : string option ref -val async_proofs_is_worker : unit -> bool -val async_proofs_is_master : unit -> bool -val async_proofs_full : bool ref -val async_proofs_never_reopen_branch : bool ref -val async_proofs_flags_for_workers : string list ref val async_proofs_worker_id : string ref -type priority = Low | High -val async_proofs_worker_priority : priority ref -val string_of_priority : priority -> string -val priority_of_string : string -> priority -type tac_error_filter = [ `None | `Only of string list | `All ] -val async_proofs_tac_error_resilience : tac_error_filter ref -val async_proofs_cmd_error_resilience : bool ref -val async_proofs_delegation_threshold : float ref +val async_proofs_is_worker : unit -> bool +(** Debug flags *) val debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref -(** Enable STM debugging *) -val stm_debug : bool ref - val profile : bool (* -ide_slave: printing will be more verbose, will affect stm caching *) diff --git a/lib/system.ml b/lib/system.ml index 4b5066ef4..2c8dbac7c 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -309,9 +309,3 @@ let with_time time f x = let msg2 = if time then "" else " (failure)" in Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e - -let process_id () = - Printf.sprintf "%d:%s:%d" (Unix.getpid ()) - (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id - else "master") - (Thread.id (Thread.self ())) diff --git a/lib/system.mli b/lib/system.mli index aa964abeb..c02bc9c8a 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -105,6 +105,3 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t val with_time : bool -> ('a -> 'b) -> 'a -> 'b - -(** {6 Name of current process.} *) -val process_id : unit -> string diff --git a/library/global.ml b/library/global.ml index 03d7612a4..ce37dfecf 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 1d68d1082..324181e79 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 9f49d1f83..6df17476b 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 d093d95f2..09447199e 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 8e6a01aa3..b766f0c6b 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 d17ccb0b4..3ca013a96 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 b0a76137b..766adfc63 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -141,7 +141,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") -let le = function () -> (coq_init_constant "le") +let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = @@ -857,9 +857,13 @@ let rec prove_le g = Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try - let matching_fun = - pf_is_matching g - (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in + let matching_fun c = match EConstr.kind sigma c with + | App (c, [| x0 ; _ |]) -> + EConstr.isVar sigma x0 && + Id.equal (destVar sigma x0) (destVar sigma x) && + is_global sigma (le ()) c + | _ -> false + in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 34fea6175..8b9eb3983 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -471,7 +471,7 @@ END VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtUnknown, VtNow ] -> + [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index ee34161dd..2e14243d8 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2021,14 +2021,16 @@ let add_morphism glob binders m s n = (** Taken from original setoid_replace, to emulate the old rewrite semantics where lemmas are first instantiated and then rewrite proceeds. *) -let check_evar_map_of_evars_defs evd = +let check_evar_map_of_evars_defs env evd = let metas = Evd.meta_list evd in let check_freemetas_is_empty rebus = Evd.Metaset.iter (fun m -> - if Evd.meta_defined evd m then () else - raise - (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m]))) + if Evd.meta_defined evd m then () + else begin + raise + (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m])) + end) in List.iter (fun (_,binding) -> @@ -2063,7 +2065,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' and car = nf car and rel = nf rel in - check_evar_map_of_evars_defs sigma; + check_evar_map_of_evars_defs env sigma; let prf = nf prf in let prfty = nf (Retyping.get_type_of env sigma prf) in let sort = sort_of_rel env sigma but in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index e0d7eca5f..9e47db1c3 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -420,7 +420,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index f22f00839..e3e749b75 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -152,7 +152,8 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let vars = Univops.universes_of_constr c in + let env = Global.env () in + let vars = Univops.universes_of_constr env c in let univs = Univops.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index c36630f5d..6d5ee504e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -322,16 +322,16 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) -let path_printer = ref (fun _ -> str "<a class path>" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) +let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ _ _ -> str "<a class path>") let install_path_printer f = path_printer := f -let print_path x = !path_printer x +let print_path env sigma x = !path_printer env sigma x -let message_ambig l = - (str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path ijp) l) +let message_ambig env sigma l = + str"Ambiguous paths:" ++ spc () ++ + prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -344,8 +344,8 @@ let different_class_params i = | CL_IND i -> Global.is_polymorphic (IndRef i) | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false - -let add_coercion_in_graph (ic,source,target) = + +let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig !ambig_paths) + Feedback.msg_info (message_ambig env sigma !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -433,13 +433,13 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion (_, c) = +let cache_coercion env sigma (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in - let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in + let value, ctx = Universes.fresh_global_instance env c.coercion_type in + let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in let typ = EConstr.Unsafe.to_constr typ in let xf = { coe_value = value; @@ -450,15 +450,15 @@ let cache_coercion (_, c) = coe_is_projection = c.coercion_is_proj; coe_param = c.coercion_params } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph (xf,is,it) + add_coercion_in_graph env sigma (xf,is,it) let load_coercion _ o = if !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let open_coercion i o = if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -497,7 +497,9 @@ let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; - cache_function = cache_coercion; + cache_function = (fun objn -> + let env = Global.env () in cache_coercion env Evd.empty objn + ); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } diff --git a/pretyping/classops.mli b/pretyping/classops.mli index b41d0efac..47b41f17b 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -96,7 +96,7 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 20ef65c88..478ba73fd 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -13,7 +13,6 @@ open Util open Names open Globnames open Termops -open Reductionops open Term open EConstr open Vars @@ -207,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = in constrain sigma n c subst -let matches_core env sigma convert allow_partial_app allow_bound_rels +let matches_core env sigma allow_partial_app allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = @@ -216,11 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | ConstRef c, Const (c',_) -> Constant.equal c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' - | _, _ -> - (if convert then - let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma (EConstr.of_constr c') c - else false) + | _, _ -> false in let rec sorec ctx env subst p t = let cT = strip_outer_cast sigma t in @@ -378,14 +373,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma convert allow_partial_app pat c = - let names, subst = matches_core env sigma convert allow_partial_app false pat c in +let matches_core_closed env sigma allow_partial_app pat c = + let names, subst = matches_core env sigma allow_partial_app false pat c in (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma false true true +let extended_matches env sigma = matches_core env sigma true true let matches env sigma pat c = - snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma true (Id.Set.empty,pat) c) let special_meta = (-1) @@ -412,7 +407,7 @@ let matches_head env sigma pat c = (* Tells if it is an authorized occurrence and if the instance is closed *) let authorized_occ env sigma partial_app closed pat c mk_ctx = try - let subst = matches_core_closed env sigma false partial_app pat c in + let subst = matches_core_closed env sigma partial_app pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) @@ -552,10 +547,3 @@ let is_matching_appsubterm ?(closed=true) env sigma pat c = let pat = (Id.Set.empty,pat) in let results = sub_match ~partial_app:true ~closed env sigma pat c in not (IStream.is_empty results) - -let matches_conv env sigma p c = - snd (matches_core_closed env sigma true false (Id.Set.empty,p) c) - -let is_matching_conv env sigma pat n = - try let _ = matches_conv env sigma pat n in true - with PatternMatchingFailure -> false diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 780ccc23d..60e1c34a1 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -55,12 +55,6 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool prefix of it matches against [pat] *) val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool -(** [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) -val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map - (** The type of subterm matching results: a substitution + a context (whose hole is denoted here with [special_meta]) *) type matching_result = @@ -85,8 +79,3 @@ val match_subterm_gen : env -> Evd.evar_map -> (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool - -(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) -val is_matching_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> bool diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 30fc5f321..d9994c473 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 34fdbe858..7e12d263a 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/printing/prettyp.ml b/printing/prettyp.ml index 1eb2c31c8..647111bbe 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -903,18 +903,16 @@ let print_class i = let cl,_ = class_info_from_index i in pr_class cl -let print_path ((i,j),p) = - let sigma, env = Pfedit.get_current_context () in +let print_path env sigma ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j -(* XXX: This is suspicious!!! *) let _ = Classops.install_path_printer print_path -let print_graph () = - prlist_with_sep fnl print_path (inheritance_graph()) +let print_graph env sigma = + prlist_with_sep fnl (print_path env sigma) (inheritance_graph()) let print_classes () = pr_sequence pr_class (classes()) @@ -929,7 +927,7 @@ let index_of_class cl = user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between cls clt = +let print_path_between env sigma cls clt = let i = index_of_class cls in let j = index_of_class clt in let p = @@ -940,7 +938,7 @@ let print_path_between cls clt = (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path ((i,j),p) + print_path env sigma ((i,j),p) let print_canonical_projections env sigma = prlist_with_sep fnl diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 8f3a6ddc4..fd7f1f92b 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,6 +12,7 @@ open Reductionops open Libnames open Globnames open Misctypes +open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -39,10 +40,10 @@ val print_about : env -> Evd.evar_map -> reference or_by_notation -> val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : unit -> Pp.t +val print_graph : env -> evar_map -> Pp.t val print_classes : unit -> Pp.t val print_coercions : env -> Evd.evar_map -> Pp.t -val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_path_between : env -> evar_map -> Classops.cl_typ -> Classops.cl_typ -> Pp.t val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) diff --git a/printing/printer.ml b/printing/printer.ml index 6a0597860..a63004ceb 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -905,7 +905,7 @@ end module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) -let pr_assumptionset env s = +let pr_assumptionset env sigma s = if ContextObjectMap.is_empty s && engagement env = PredicativeSet then str "Closed under the global context" @@ -921,7 +921,6 @@ let pr_assumptionset env s = with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = - let sigma, env = Pfedit.get_current_context () in let env = Environ.push_rel_context rctx env in try str " " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () diff --git a/printing/printer.mli b/printing/printer.mli index 36ca1bdcc..804014745 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -217,8 +217,7 @@ module ContextObjectSet : Set.S with type elt = context_object module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet -val pr_assumptionset : - env -> types ContextObjectMap.t -> Pp.t +val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 4a92c3856..8bd5d98cb 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -54,9 +54,10 @@ let clenv_value_cast_meta clenv = let clenv_pose_dependent_evars with_evars clenv = let dep_mvs = clenv_dependent clenv in + let env, sigma = clenv.env, clenv.evd in if not (List.is_empty dep_mvs) && not with_evars then raise - (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); + (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs (** Use our own fast path, more informative than from Typeclasses *) diff --git a/proofs/logic.ml b/proofs/logic.ml index a9ad606a0..1d86a0909 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -40,7 +40,7 @@ type refiner_error = | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t -exception RefinerError of refiner_error +exception RefinerError of Environ.env * Evd.evar_map * refiner_error open Pretype_errors @@ -69,7 +69,7 @@ let catchable_exception = function | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e | _ -> false -let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id)) +let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) @@ -78,10 +78,10 @@ let with_check = Flags.with_option check (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp check sign id f = +let apply_to_hyp env sigma check sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if check then error_no_such_hypothesis id + if check then error_no_such_hypothesis env sigma id else sign let check_typability env sigma c = @@ -147,7 +147,7 @@ let reorder_context env sigma sign ord = step ord' expected ctxt_head mh (d::ctxt_tail) | _ -> (match ctxt_head with - | [] -> error_no_such_hypothesis (List.hd ord) + | [] -> error_no_such_hypothesis env sigma (List.hd ord) | d :: ctxt -> let x = NamedDecl.get_id d in if Id.Set.mem x expected then @@ -190,9 +190,9 @@ let move_location_eq m1 m2 = match m1, m2 with | MoveFirst, MoveFirst -> true | _ -> false -let split_sign hfrom hto l = +let split_sign env sigma hfrom hto l = let rec splitrec left toleft = function - | [] -> error_no_such_hypothesis hfrom + | [] -> error_no_such_hypothesis env sigma hfrom | d :: right -> let hyp = NamedDecl.get_id d in if Id.equal hyp hfrom then @@ -222,7 +222,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = let rec moverec first middle = function | [] -> if match hto with MoveFirst | MoveLast -> false | _ -> true then - error_no_such_hypothesis (hyp_of_move_location hto); + error_no_such_hypothesis env sigma (hyp_of_move_location hto); List.rev first @ List.rev middle | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> List.rev first @ List.rev middle @ right @@ -258,10 +258,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let move_hyp_in_named_context sigma hfrom hto sign = +let move_hyp_in_named_context env sigma hfrom hto sign = let open EConstr in let (left,right,declfrom,toleft) = - split_sign hfrom hto (named_context_of_val sign) in + split_sign env sigma hfrom hto (named_context_of_val sign) in move_hyp sigma toleft (left,declfrom,right) hto let insert_decl_in_named_context sigma decl hto sign = @@ -293,15 +293,15 @@ let collect_meta_variables c = in List.rev (collrec false [] c) -let check_meta_variables c = +let check_meta_variables env sigma c = if not (List.distinct_f Int.compare (collect_meta_variables c)) then - raise (RefinerError (NonLinearProof c)) + raise (RefinerError (env, sigma, NonLinearProof c)) let check_conv_leq_goal env sigma arg ty conclty = if !check then let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in if b then evm - else raise (RefinerError (BadType (arg,ty,conclty))) + else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list @@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Meta _ -> let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in if !check && occur_meta sigma conclty then - raise (RefinerError (MetaInType conclty)); + raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in let ev = EConstr.Unsafe.to_constr ev in let conclty = EConstr.Unsafe.to_constr conclty in @@ -477,7 +477,9 @@ and mk_arggoals sigma goal goalacc funty allargs = | Prod (_, c1, b) -> let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in (acc, subst1 harg b, sigma), arg - | _ -> raise (RefinerError (CannotApply (t, harg))) + | _ -> + let env = Goal.V82.env sigma goal in + raise (RefinerError (env,sigma,CannotApply (t, harg))) in Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs @@ -497,10 +499,10 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in - let env = Global.env() in + let env = Global.env () in let reorder = ref [] in let sign' = - apply_to_hyp check sign id + apply_to_hyp env sigma check sign id (fun _ d' _ -> let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in let env = Global.env_of_context sign in @@ -514,19 +516,18 @@ let convert_hyp check sign sigma d = map_named_decl EConstr.Unsafe.to_constr d) in reorder_val_context env sigma sign' !reorder - - (************************************************************************) (************************************************************************) (* Primitive tactics are handled here *) let prim_refiner r sigma goal = + let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in match r with (* Logical rules *) | Refine c -> let cl = EConstr.Unsafe.to_constr cl in - check_meta_variables c; + check_meta_variables env sigma c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in diff --git a/proofs/logic.mli b/proofs/logic.mli index 7df7fd66b..afd1ecf70 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -50,16 +50,16 @@ type refiner_error = | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t -exception RefinerError of refiner_error +exception RefinerError of Environ.env * evar_map * refiner_error -val error_no_such_hypothesis : Id.t -> 'a +val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> EConstr.named_declaration -> Environ.named_context_val -val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val val insert_decl_in_named_context : Evd.evar_map -> diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 31a73db04..6b503a011 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 535ef2013..167d6bda0 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 34e517aed..52dc8bfd8 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -40,7 +40,7 @@ val tclEVARUNIVCONTEXT : UState.t -> tactic val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.constraints -> tactic +val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a8ec4d8ca..d41541251 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -55,10 +55,11 @@ let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = + let env, sigma = pf_env gls, project gls in try Context.Named.lookup id (pf_hyps gls) with Not_found -> - raise (RefinerError (NoSuchHyp id)) + raise (RefinerError (env, sigma, NoSuchHyp id)) let pf_get_hyp_typ gls id = id |> pf_get_hyp gls |> NamedDecl.get_type @@ -102,9 +103,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 *) (********************************************) @@ -185,9 +183,10 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.env gl in + let sigma = project gl in let sign = try EConstr.lookup_named id hyps - with Not_found -> raise (RefinerError (NoSuchHyp id)) + with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id)) in sign @@ -223,8 +222,6 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d9496d2b4..e0fb8fbc5 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,9 +12,7 @@ open Environ open EConstr open Proof_type open Redexpr -open Pattern open Locus -open Ltac_pretype (** Operations for handling terms under a local typing context. *) @@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool - - (** {6 The most primitive tactics. } *) val refiner : rule -> tactic @@ -138,8 +132,6 @@ module New : sig val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr val pf_compute : 'a Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr end diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index cd22a7183..26aef5355 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -10,11 +10,11 @@ open CErrors open Pp open Util -let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp - +let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () type cancel_switch = bool ref +let async_proofs_flags_for_workers = ref [] module type Task = sig @@ -117,12 +117,12 @@ module Make(T : Task) () = struct let name = Printf.sprintf "%s:%d" !T.name id in let proc, ic, oc = let rec set_slave_opt = function - | [] -> !Flags.async_proofs_flags_for_workers @ + | [] -> !async_proofs_flags_for_workers @ ["-toploop"; !T.name^"top"; "-worker-id"; name; "-async-proofs-worker-priority"; - Flags.string_of_priority !Flags.async_proofs_worker_priority] - | ("-ideslave"|"-emacs"|"-batch")::tl -> set_slave_opt tl + CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)] + | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl | ("-async-proofs" |"-toploop" |"-vio2vo" |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" |"-compile" |"-compile-verbose" @@ -295,7 +295,7 @@ module Make(T : Task) () = struct let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) - let pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp) + let pp_pid pp = Pp.(str (Spawned.process_id () ^ " ") ++ pp) let debug_with_pid = Feedback.(function | { contents = Message(Debug, loc, pp) } as fb -> diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index ccd643deb..07689389f 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Default flags for workers *) +val async_proofs_flags_for_workers : string list ref + (** This file provides an API for defining and managing a queue of tasks to be done by external workers. diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index 6d6a198c5..14fd97a6d 100644 --- a/stm/coqworkmgrApi.ml +++ b/stm/coqworkmgrApi.ml @@ -8,8 +8,15 @@ let debug = false +type priority = Low | High +let string_of_priority = function Low -> "low" | High -> "high" +let priority_of_string = function + | "low" -> Low + | "high" -> High + | _ -> raise (Invalid_argument "priority_of_string") + type request = - | Hello of Flags.priority + | Hello of priority | Get of int | TryGet of int | GiveBack of int @@ -36,8 +43,8 @@ let positive_int_of_string n = let parse_request s = if debug then Printf.eprintf "parsing '%s'\n" s; match Str.split (Str.regexp " ") (strip_r s) with - | [ "HELLO"; "LOW" ] -> Hello Flags.Low - | [ "HELLO"; "HIGH" ] -> Hello Flags.High + | [ "HELLO"; "LOW" ] -> Hello Low + | [ "HELLO"; "HIGH" ] -> Hello High | [ "GET"; n ] -> Get (positive_int_of_string n) | [ "TRYGET"; n ] -> TryGet (positive_int_of_string n) | [ "GIVEBACK"; n ] -> GiveBack (positive_int_of_string n) @@ -57,8 +64,8 @@ let parse_response s = | _ -> raise ParseError let print_request = function - | Hello Flags.Low -> "HELLO LOW\n" - | Hello Flags.High -> "HELLO HIGH\n" + | Hello Low -> "HELLO LOW\n" + | Hello High -> "HELLO HIGH\n" | Get n -> Printf.sprintf "GET %d\n" n | TryGet n -> Printf.sprintf "TRYGET %d\n" n | GiveBack n -> Printf.sprintf "GIVEBACK %d\n" n @@ -106,8 +113,7 @@ let with_manager f g = let get n = with_manager - (fun () -> - min n (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers)) + (fun () -> n) (fun cin cout -> output_string cout (print_request (Get n)); flush cout; @@ -118,10 +124,7 @@ let get n = let tryget n = with_manager - (fun () -> - Some - (min n - (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers))) + (fun () -> Some n) (fun cin cout -> output_string cout (print_request (TryGet n)); flush cout; diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli index 70d4173ae..953903810 100644 --- a/stm/coqworkmgrApi.mli +++ b/stm/coqworkmgrApi.mli @@ -8,9 +8,13 @@ (* High level api for clients of the service (like coqtop) *) +type priority = Low | High +val string_of_priority : priority -> string +val priority_of_string : string -> priority + (* Connects to a work manager if any. If no worker manager, then -async-proofs-j and -async-proofs-tac-j are used *) -val init : Flags.priority -> unit +val init : priority -> unit (* blocking *) val get : int -> int @@ -21,7 +25,7 @@ val giveback : int -> unit (* Low level *) type request = - | Hello of Flags.priority + | Hello of priority | Get of int | TryGet of int | GiveBack of int diff --git a/stm/spawned.ml b/stm/spawned.ml index 6ab096abf..fb5708f3a 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -73,3 +73,9 @@ let get_channels () = Printf.eprintf "Fatal error: ideslave communication channels not set.\n"; exit 1 | Some(ic, oc) -> ic, oc + +let process_id () = + Printf.sprintf "%d:%s:%d" (Unix.getpid ()) + (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id + else "master") + (Thread.id (Thread.self ())) diff --git a/stm/spawned.mli b/stm/spawned.mli index c3cf4d67b..7f463c6a6 100644 --- a/stm/spawned.mli +++ b/stm/spawned.mli @@ -20,3 +20,5 @@ val init_channels : unit -> unit (* Once initialized, these are the channels to talk with our master *) val get_channels : unit -> CThread.thread_ic * out_channel +(** {6 Name of current process.} *) +val process_id : unit -> string diff --git a/stm/stm.ml b/stm/stm.ml index 8aa832da8..1d46e0833 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -8,13 +8,13 @@ (* enable in case of stm problems *) (* let stm_debug () = !Flags.debug *) -let stm_debug () = !Flags.stm_debug +let stm_debug = ref false -let stm_pr_err s = Format.eprintf "%s] %s\n%!" (System.process_id ()) s -let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp +let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s +let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp -let stm_prerr_endline s = if stm_debug () then begin stm_pr_err (s ()) end else () -let stm_pperr_endline s = if stm_debug () then begin stm_pp_err (s ()) end else () +let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else () +let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else () let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () @@ -23,6 +23,35 @@ open CErrors open Feedback open Vernacexpr +module AsyncOpts = struct + + let async_proofs_n_workers = ref 1 + let async_proofs_n_tacworkers = ref 2 + + type cache = Force + let async_proofs_cache : cache option ref = ref None + + type async_proofs = APoff | APonLazy | APon + let async_proofs_mode = ref APoff + + let async_proofs_private_flags = ref None + let async_proofs_full = ref false + let async_proofs_never_reopen_branch = ref false + + type tac_error_filter = [ `None | `Only of string list | `All ] + let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) + let async_proofs_cmd_error_resilience = ref true + + let async_proofs_delegation_threshold = ref 0.03 + +end + +open AsyncOpts + +let async_proofs_is_master () = + !async_proofs_mode = APon && + !Flags.async_proofs_worker_id = "master" + (* Protect against state changes *) let stm_purify f x = let st = Vernacstate.freeze_interp_state `No in @@ -158,9 +187,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 @@ -352,10 +382,10 @@ end = struct (* {{{ *) In case you are hitting the race enable stm_debug. *) - if stm_debug () then Flags.we_are_parsing := false; + if !stm_debug then Flags.we_are_parsing := false; let fname = - "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in + "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in let string_of_transaction = function | Cmd { cast = t } | Fork (t, _,_,_) -> (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") @@ -529,7 +559,7 @@ end = struct (* {{{ *) | None -> raise Vcs_aux.Expired let set_state id s = (get_info id).state <- s; - if Flags.async_proofs_is_master () then Hooks.(call state_ready id) + if async_proofs_is_master () then Hooks.(call state_ready id) let get_state id = (get_info id).state let reached id = let info = get_info id in @@ -762,15 +792,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 +866,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 +895,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 @@ -1105,7 +1146,7 @@ end = struct (* {{{ *) " the \"-async-proofs-cache force\" option to Coq.")) let undo_vernac_classifier v = - if VCS.is_interactive () = `No && !Flags.async_proofs_cache <> Some Flags.Force + if VCS.is_interactive () = `No && !async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try match v with @@ -1241,7 +1282,7 @@ let prev_node { id } = let cur_node id = mk_doc_node id (VCS.visit id) let is_block_name_enabled name = - match !Flags.async_proofs_tac_error_resilience with + match !async_proofs_tac_error_resilience with | `None -> false | `All -> true | `Only l -> List.mem name l @@ -1249,7 +1290,7 @@ let is_block_name_enabled name = let detect_proof_block id name = let name = match name with None -> "indent" | Some x -> x in if is_block_name_enabled name && - (Flags.async_proofs_is_master () || Flags.async_proofs_is_worker ()) + (async_proofs_is_master () || Flags.async_proofs_is_worker ()) then ( match cur_node id with | None -> () @@ -1351,7 +1392,7 @@ end = struct (* {{{ *) let task_match age t = match age, t with | Fresh, BuildProof { t_states } -> - not !Flags.async_proofs_full || + not !async_proofs_full || List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l @@ -1388,7 +1429,7 @@ end = struct (* {{{ *) feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !Flags.async_proofs_full || t_drop + if !async_proofs_full || t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, @@ -1562,8 +1603,8 @@ end = struct (* {{{ *) let queue = ref None let init () = - if Flags.async_proofs_is_master () then - queue := Some (TaskQueue.create !Flags.async_proofs_n_workers) + if async_proofs_is_master () then + queue := Some (TaskQueue.create !async_proofs_n_workers) else queue := Some (TaskQueue.create 0) @@ -2028,7 +2069,7 @@ end = struct (* {{{ *) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch let init () = queue := Some (TaskQueue.create - (if !Flags.async_proofs_full then 1 else 0)) + (if !async_proofs_full then 1 else 0)) end (* }}} *) @@ -2040,8 +2081,6 @@ and Reach : sig end = struct (* {{{ *) -let pstate = summary_pstate - let async_policy () = let open Flags in if is_universe_polymorphism () then false @@ -2051,9 +2090,9 @@ let async_policy () = (VCS.is_vio_doc () || !async_proofs_mode <> APoff) let delegate name = - get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold + get_hint_bp_time name >= !async_proofs_delegation_threshold || VCS.is_vio_doc () - || !Flags.async_proofs_full + || !async_proofs_full let warn_deprecated_nested_proofs = CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" @@ -2150,7 +2189,7 @@ let collect_proof keep cur hd brkind id = let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc else if (keep == VtKeep || keep == VtKeepAsAxiom) && - (not(State.is_cached_and_valid id) || !Flags.async_proofs_full) + (not(State.is_cached_and_valid id) || !async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2232,9 +2271,9 @@ let known_state ?(redefine_qed=false) ~cache id = (* Absorb tactic errors from f () *) let resilient_tactic id blockname f = - if !Flags.async_proofs_tac_error_resilience = `None || - (Flags.async_proofs_is_master () && - !Flags.async_proofs_mode = Flags.APoff) + if !async_proofs_tac_error_resilience = `None || + (async_proofs_is_master () && + !async_proofs_mode = APoff) then f () else try f () @@ -2243,9 +2282,9 @@ let known_state ?(redefine_qed=false) ~cache id = error_absorbing_tactic id blockname ie in (* Absorb errors from f x *) let resilient_command f x = - if not !Flags.async_proofs_cmd_error_resilience || - (Flags.async_proofs_is_master () && - !Flags.async_proofs_mode = Flags.APoff) + if not !async_proofs_cmd_error_resilience || + (async_proofs_is_master () && + !async_proofs_mode = APoff) then f x else try f x @@ -2254,10 +2293,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 -> @@ -2287,10 +2330,10 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach ~cache:`Shallow view.next; Partac.vernac_interp ~solve ~abstract ~cancel_switch - !Flags.async_proofs_n_tacworkers view.next id x) + !async_proofs_n_tacworkers view.next id x) ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch } - when Flags.async_proofs_is_master () -> (fun () -> + when async_proofs_is_master () -> (fun () -> reach view.next; Query.vernac_interp ~cancel_switch view.next id x ), cache, false @@ -2304,10 +2347,10 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - (match !Flags.async_proofs_mode with - | Flags.APon | Flags.APonLazy -> + (match !async_proofs_mode with + | APon | APonLazy -> resilient_command reach view.next - | Flags.APoff -> reach view.next); + | APoff -> reach view.next); let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); if eff then update_global_env () @@ -2434,7 +2477,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true in let cache_step = - if !Flags.async_proofs_cache = Some Flags.Force then `Yes + if !async_proofs_cache = Some Force then `Yes else cache_step in State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; @@ -2465,6 +2508,7 @@ let doc_type_module_name (std : stm_doc_type) = *) let init_core () = + if !async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () let new_doc { doc_type ; require_libs } = @@ -2503,10 +2547,10 @@ let new_doc { doc_type ; require_libs } = State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); - if Flags.async_proofs_is_master () then begin + if async_proofs_is_master () then begin stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); - let opts = match !Flags.async_proofs_private_flags with + let opts = match !async_proofs_private_flags with | None -> [] | Some s -> Str.split_delim (Str.regexp ",") s in begin try @@ -2705,7 +2749,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) | VtQuery (true, route), w -> let id = VCS.new_node ~id:newtip () in let queue = - if !Flags.async_proofs_full then `QueryQueue (ref false) + if !async_proofs_full then `QueryQueue (ref false) else if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && may_pierce_opaque x @@ -2870,7 +2914,7 @@ let parse_sentence ~doc sid pa = (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ; - if not (Stateid.equal sid real_tip) && !Flags.debug && stm_debug () then + if not (Stateid.equal sid real_tip) && !Flags.debug && !stm_debug then Feedback.msg_debug (str "Warning, the real tip doesn't match the current tip." ++ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ @@ -3029,7 +3073,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !Flags.async_proofs_full then + if not !async_proofs_full then Reach.known_state ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in @@ -3045,7 +3089,7 @@ let edit_at ~doc id = | _, Some _, None -> assert false | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) -> let tip = VCS.cur_tip () in - if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch + if has_failed qed_id && is_pure qed_id && not !async_proofs_never_reopen_branch then reopen_branch start id mode qed_id tip bn else backto id (Some bn) | true, Some { qed = qed_id }, Some(mode,bn) -> diff --git a/stm/stm.mli b/stm/stm.mli index 9fd35a0d3..ef95be0e4 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -225,3 +225,30 @@ val state_of_id : doc:doc -> (* Queries for backward compatibility *) val current_proof_depth : doc:doc -> int val get_all_proof_names : doc:doc -> Id.t list + +(** Enable STM debugging *) +val stm_debug : bool ref + +(* Flags *) +module AsyncOpts : sig + + (* Defaults for worker creation *) + val async_proofs_n_workers : int ref + val async_proofs_n_tacworkers : int ref + + type async_proofs = APoff | APonLazy | APon + val async_proofs_mode : async_proofs ref + + type cache = Force + val async_proofs_cache : cache option ref + + val async_proofs_private_flags : string option ref + val async_proofs_full : bool ref + val async_proofs_never_reopen_branch : bool ref + + type tac_error_filter = [ `None | `Only of string list | `All ] + val async_proofs_tac_error_resilience : tac_error_filter ref + val async_proofs_cmd_error_resilience : bool ref + val async_proofs_delegation_threshold : float ref + +end diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 1ca572a36..c5ae27a11 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -185,12 +185,12 @@ let rec classify_vernac e = (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ - | VernacSyntaxExtension _ + | VernacSyntaxExtension _ | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) - | VernacProofMode _ + | VernacProofMode _ -> VtSideff [], VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) @@ -201,7 +201,7 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ -> VtUnknown, VtNow + | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 64121eb3d..704119186 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Default priority *) +open CoqworkmgrApi +let async_proofs_worker_priority = ref Low + let rec parse = function | "--xml_format=Ppcmds" :: rest -> parse rest | x :: rest -> x :: parse rest @@ -15,5 +19,5 @@ let loop init args = let args = parse args in Flags.quiet := true; init (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; + CoqworkmgrApi.init !async_proofs_worker_priority; args diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index 53f745935..da2e6fe0c 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -6,4 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Default priority *) +val async_proofs_worker_priority : CoqworkmgrApi.priority ref + val loop : (unit -> unit) -> string list -> string list diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index cee6d4bea..9e4d132d4 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -376,7 +376,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = Proofview.Goal.enter begin fun gl -> let tacs = e_trivial_resolve db_list local_db secvars only_classes - (project gl) (pf_concl gl) in + (pf_env gl) (project gl) (pf_concl gl) in tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) end in @@ -386,7 +386,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = in tclFIRST (List.map tclCOMPLETE tacl) -and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl = +and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl = let open Proofview.Notations in let prods, concl = EConstr.decompose_prod_assum sigma concl in let nprods = List.length prods in @@ -464,7 +464,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co in let tac = run_hint t tac in let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in - let _, env = Pfedit.get_current_context () in let pp = match p with | Some pat when get_typeclasses_filtered_unification () -> @@ -476,16 +475,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp)) in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db secvars only_classes sigma concl = +and e_trivial_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd true only_classes sigma concl + e_my_find_search db_list local_db secvars hd true only_classes env sigma concl with Not_found -> [] -let e_possible_resolve db_list local_db secvars only_classes sigma concl = +let e_possible_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd false only_classes sigma concl + e_my_find_search db_list local_db secvars hd false only_classes env sigma concl with Not_found -> [] let cut_of_hints h = @@ -719,7 +718,7 @@ module V85 = struct let concl = Goal.V82.concl s gl in let tacgl = {it = gl; sigma = s;} in let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in - let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in + let poss = e_possible_resolve hints info.hints secvars info.only_classes env s concl in let unique = is_unique env s concl in let rec aux i foundone = function | (tac, _, extern, name, pp) :: tl -> @@ -1072,7 +1071,7 @@ module Search = struct else str" without backtracking")); let secvars = compute_secvars gl in let poss = - e_possible_resolve hints info.search_hints secvars info.search_only_classes sigma concl in + e_possible_resolve hints info.search_hints secvars info.search_only_classes env sigma concl in (* If no goal depends on the solution of this one or the instances are irrelevant/assumed to be unique, then we don't need to backtrack, as long as no evar appears in the goal diff --git a/tactics/eauto.ml b/tactics/eauto.ml index b5cfbe68b..6ea6155e0 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -148,12 +148,12 @@ let rec e_trivial_fail_db db_list local_db = let tacl = registered_e_assumption :: (Tacticals.New.tclTHEN Tactics.intro next) :: - (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) + (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) in Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) end -and e_my_find_search sigma db_list local_db secvars hdc concl = +and e_my_find_search env sigma db_list local_db secvars hdc concl = let hint_of_db = hintmap_of sigma secvars hdc concl in let hintl = List.map_append (fun db -> @@ -178,20 +178,19 @@ and e_my_find_search sigma db_list local_db secvars hdc concl = | Extern tacast -> conclPattern concl p tacast in let tac = run_hint t tac in - let sigma, env = Pfedit.get_current_context () in (tac, lazy (pr_hint env sigma t))) in List.map tac_of_hint hintl -and e_trivial_resolve sigma db_list local_db secvars gl = +and e_trivial_resolve env sigma db_list local_db secvars gl = let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in - try priority (e_my_find_search sigma db_list local_db secvars hd gl) + try priority (e_my_find_search env sigma db_list local_db secvars hd gl) with Not_found -> [] -let e_possible_resolve sigma db_list local_db secvars gl = +let e_possible_resolve env sigma db_list local_db secvars gl = let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) - (e_my_find_search sigma db_list local_db secvars hd gl) + (e_my_find_search env sigma db_list local_db secvars hd gl) with Not_found -> [] let find_first_goal gls = @@ -291,7 +290,7 @@ module SearchProblem = struct let l = let concl = Reductionops.nf_evar (project g) (pf_concl g) in filter_tactics s.tacres - (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl) + (e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl) in List.map (fun (lgls, cost, pp) -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 0d6263246..22073d39b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1436,8 +1436,9 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let rec aux dest = function - | [] -> raise (RefinerError (NoSuchHyp id)) + | [] -> raise (RefinerError (env, sigma, NoSuchHyp id)) | d :: right -> let hyp = Context.Named.Declaration.get_id d in if Id.equal hyp id then dest else aux (MoveAfter hyp) right diff --git a/tactics/hints.ml b/tactics/hints.ml index 70e84013b..7f9b5ef34 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1400,15 +1400,10 @@ let pr_hint env sigma h = match h.obj with | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c) | Res_pf_THEN_trivial_fail (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") - | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) + | Unfold_nth c -> + str"unfold " ++ pr_evaluable_reference c | Extern tac -> - let env = - try - let (_, env) = Pfedit.get_current_goal_context () in - env - with e when CErrors.noncritical e -> Global.env () - in - (str "(*external*) " ++ Pputils.pr_glb_generic env tac) + str "(*external*) " ++ Pputils.pr_glb_generic env tac let pr_id_hint env sigma (id, v) = let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in @@ -1507,6 +1502,7 @@ let pr_hint_db_env env sigma db = hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++ content +(* Deprecated in the mli *) let pr_hint_db db = let sigma, env = Pfedit.get_current_context () in pr_hint_db_env env sigma db diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 8e851375a..2c8ca1972 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -39,7 +39,6 @@ type testing_function = Evd.evar_map -> EConstr.constr -> bool let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 -let meta3 = mkmeta 3 let op2bool = function Some _ -> true | None -> false @@ -460,22 +459,6 @@ let find_this_eq_data_decompose gl eqn = user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) -let match_eq_nf gls eqn (ref, hetero) = - let n = if hetero then 4 else 3 in - let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in - let pat = mkPattern (mkGAppRef ref args) in - match Id.Map.bindings (pf_matches gls pat eqn) with - | [(m1,t);(m2,x);(m3,y)] -> - assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,pf_whd_all gls x,pf_whd_all gls y) - | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.") - -let dest_nf_eq gls eqn = - try - snd (first_match (match_eq_nf gls eqn) equalities) - with PatternMatchingFailure -> - user_err Pp.(str "Not an equality.") - (*** Sigma-types *) let match_sigma env sigma ex = diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 8ff6fe95c..237ed42d5 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -144,9 +144,6 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool [t,u,T] and a boolean telling if equality is on the left side *) val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr -(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) - (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml index 46b10bf33..cb0bbfd0e 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -334,6 +334,16 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id If it can discriminate then the goal is proved, if not tries to use it as a rewrite rule. It erases the clause which is given as input *) +let dest_nf_eq env sigma t = match EConstr.kind sigma t with +| App (r, [| t; x; y |]) -> + let open Reductionops in + let lazy eq = Coqlib.coq_eq_ref in + if EConstr.is_global sigma eq r then + (t, whd_all env sigma x, whd_all env sigma y) + else user_err Pp.(str "Not an equality.") +| _ -> + user_err Pp.(str "Not an equality.") + let projectAndApply as_mode thin avoid id eqname names depids = let subst_hyp l2r id = tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id))) @@ -344,7 +354,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = let sigma = project gl in (** We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in - let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in + let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in match (EConstr.kind sigma t1, EConstr.kind sigma t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cb2a77558..839090903 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -187,7 +187,7 @@ let introduction ?(check=true) id = match EConstr.kind sigma concl with | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b - | _ -> raise (RefinerError IntroNeedsProduct) + | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct)) end let refine = Tacmach.refine @@ -319,7 +319,7 @@ let move_hyp id dest = let ty = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let sign = named_context_val env in - let sign' = move_hyp_in_named_context sigma id dest sign in + let sign' = move_hyp_in_named_context env sigma id dest sign in let env = reset_with_named_context sign' env in Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty @@ -348,13 +348,15 @@ let rename_hyp repl = let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in (** Check that we do not mess variables *) let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in let vars = List.fold_left fold Id.Set.empty hyps in let () = if not (Id.Set.subset src vars) then let hyp = Id.Set.choose (Id.Set.diff src vars) in - raise (RefinerError (NoSuchHyp hyp)) + raise (RefinerError (env, sigma, NoSuchHyp hyp)) in let mods = Id.Set.diff vars src in let () = @@ -442,9 +444,9 @@ let find_name mayrepl decl naming gl = match naming with (* Computing position of hypotheses for replacing *) (**************************************************************) -let get_next_hyp_position id = +let get_next_hyp_position env sigma id = let rec aux = function - | [] -> error_no_such_hypothesis id + | [] -> error_no_such_hypothesis env sigma id | decl :: right -> if Id.equal (NamedDecl.get_id decl) id then match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst @@ -453,9 +455,9 @@ let get_next_hyp_position id = in aux -let get_previous_hyp_position id = +let get_previous_hyp_position env sigma id = let rec aux dest = function - | [] -> error_no_such_hypothesis id + | [] -> error_no_such_hypothesis env sigma id | decl :: right -> let hyp = NamedDecl.get_id decl in if Id.equal hyp id then dest else aux (MoveAfter hyp) right @@ -483,7 +485,7 @@ let internal_cut_gen ?(check=true) dir replace id t = let sign = named_context_val env in let sign',t,concl,sigma = if replace then - let nexthyp = get_next_hyp_position id (named_context_of_val sign) in + let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in sign',t,concl,sigma @@ -1000,6 +1002,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in match EConstr.kind sigma concl with | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) -> @@ -1009,7 +1012,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac | _ -> - begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct) + begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) (* this since at least V6.3 (a pity *) (* that intro do betaiotazeta only when reduction is needed; and *) @@ -1020,7 +1023,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = (Tacticals.New.tclTHEN hnf_in_concl (intro_then_gen name_flag move_flag false dep_flag tac)) begin function (e, info) -> match e with - | RefinerError IntroNeedsProduct -> + | RefinerError (env, sigma, IntroNeedsProduct) -> Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end @@ -1059,7 +1062,7 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = (fun id -> aux (n+1) (id::ids)) end begin function (e, info) -> match e with - | RefinerError IntroNeedsProduct -> + | RefinerError (env, sigma, IntroNeedsProduct) -> tac ids | e -> Proofview.tclZERO ~info e end @@ -1070,8 +1073,9 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = let intro_replacing id = Proofview.Goal.enter begin fun gl -> + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let next_hyp = get_next_hyp_position id hyps in + let next_hyp = get_next_hyp_position env sigma id hyps in Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; introduction id; @@ -1090,8 +1094,9 @@ let intro_replacing id = let intros_possibly_replacing ids = let suboptimal = true in Proofview.Goal.enter begin fun gl -> + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in + let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (clear_for_replacing [id])) @@ -1105,7 +1110,8 @@ let intros_possibly_replacing ids = let intros_replacing ids = Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (clear_for_replacing ids) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) @@ -2633,8 +2639,10 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars Proofview.Goal.enter begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) - else - get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in + else ( + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + get_previous_hyp_position env sigma id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + ) in let naming,ipat_tac = prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = @@ -4448,8 +4456,11 @@ let check_enough_applied env sigma elim = check_expected_type env sigma elimc elimt let guard_no_unifiable = Proofview.guard_no_unifiable >>= function -| None -> Proofview.tclUNIT () -| Some l -> Proofview.tclZERO (RefinerError (UnresolvedBindings l)) + | None -> Proofview.tclUNIT () + | Some l -> + Proofview.tclENV >>= function env -> + Proofview.tclEVARMAP >>= function sigma -> + Proofview.tclZERO (RefinerError (env, sigma, UnresolvedBindings l)) let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac = @@ -4648,7 +4659,7 @@ let induction_destruct isrec with_evars (lc,elim) = (Tacticals.New.tclMAP (fun (a,b,cl) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in + let sigma = Tacmach.New.project gl in onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag false with_evars None (a,b) cl) a end) l) @@ -4673,7 +4684,7 @@ let induction_destruct isrec with_evars (lc,elim) = end let induction ev clr c l e = - induction_gen clr true ev e + induction_gen clr true ev e ((Evd.empty,(c,NoBindings)),(None,l)) None let destruct ev clr c l e = diff --git a/test-suite/bugs/closed/6323.v b/test-suite/bugs/closed/6323.v new file mode 100644 index 000000000..fdc33befc --- /dev/null +++ b/test-suite/bugs/closed/6323.v @@ -0,0 +1,9 @@ +Goal True. + simple refine (let X : Type := _ in _); + [ abstract exact Set using Set' + | let X' := (eval cbv delta [X] in X) in + clear X; + simple refine (let id' : { x : X' | True } -> X' := _ in _); + [ abstract refine (@proj1_sig _ _) | ] + ]. +Abort. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 0f677a849..82b51b1ff 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -12,3 +12,5 @@ Check 0. Check S. Check nat. + +Type Type : Type. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index ac95ddd0c..82b04d132 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -221,13 +221,12 @@ Tactic Notation "extensionality" "in" hyp(H) := (* If we [subst H], things break if we already have another equation of the form [_ = H] *) destruct Heq; rename H_out into H. -(** Eta expansion follows from extensionality. *) +(** Eta expansion is built into Coq. *) Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) : f = fun x => f x. Proof. intros. - extensionality x. reflexivity. Qed. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 90db10ef1..237d878bf 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -22,15 +22,13 @@ Open Scope program_scope. Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f. Proof. intros. - unfold id, compose. - symmetry. apply eta_expansion. + reflexivity. Qed. Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f. Proof. intros. - unfold id, compose. - symmetry ; apply eta_expansion. + reflexivity. Qed. Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), @@ -47,9 +45,7 @@ Hint Rewrite <- @compose_assoc : core. Lemma flip_flip : forall A B C, @flip A B C ∘ flip = id. Proof. - unfold flip, compose. intros. - extensionality x ; extensionality y ; extensionality z. reflexivity. Qed. @@ -57,9 +53,7 @@ Qed. Lemma prod_uncurry_curry : forall A B C, @prod_uncurry A B C ∘ prod_curry = id. Proof. - simpl ; intros. - unfold prod_uncurry, prod_curry, compose. - extensionality x ; extensionality y ; extensionality z. + intros. reflexivity. Qed. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 2dd559a95..209c22f71 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -40,6 +40,11 @@ Section Sets_as_an_algebra. auto 6 with sets. Qed. + Theorem Empty_set_zero_right : forall X:Ensemble U, Union U X (Empty_set U) = X. + Proof. + auto 6 with sets. + Qed. + Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x. Proof. unfold Add at 1; auto using Empty_set_zero with sets. @@ -131,6 +136,17 @@ Section Sets_as_an_algebra. elim H'; intros x0 H'0; elim H'0; auto with sets. Qed. + Lemma Distributivity_l + : forall (A B C : Ensemble U), + Intersection U (Union U A B) C = + Union U (Intersection U A C) (Intersection U B C). + Proof. + intros A B C. + rewrite Intersection_commutative. + rewrite Distributivity. + f_equal; apply Intersection_commutative. + Qed. + Theorem Distributivity' : forall A B C:Ensemble U, Union U A (Intersection U B C) = @@ -251,6 +267,81 @@ Section Sets_as_an_algebra. intros; apply Definition_of_covers; auto with sets. Qed. + Lemma Disjoint_Intersection: + forall A s1 s2, Disjoint A s1 s2 -> Intersection A s1 s2 = Empty_set A. + Proof. + intros. apply Extensionality_Ensembles. split. + * destruct H. + intros x H1. unfold In in *. exfalso. intuition. apply (H _ H1). + * intuition. + Qed. + + Lemma Intersection_Empty_set_l: + forall A s, Intersection A (Empty_set A) s = Empty_set A. + Proof. + intros. auto with sets. + Qed. + + Lemma Intersection_Empty_set_r: + forall A s, Intersection A s (Empty_set A) = Empty_set A. + Proof. + intros. auto with sets. + Qed. + + Lemma Seminus_Empty_set_l: + forall A s, Setminus A (Empty_set A) s = Empty_set A. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. destruct H1. unfold In in *. assumption. + * intuition. + Qed. + + Lemma Seminus_Empty_set_r: + forall A s, Setminus A s (Empty_set A) = s. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. destruct H1. unfold In in *. assumption. + * intuition. + Qed. + + Lemma Setminus_Union_l: + forall A s1 s2 s3, + Setminus A (Union A s1 s2) s3 = Union A (Setminus A s1 s3) (Setminus A s2 s3). + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H. inversion H. inversion H0; intuition. + * intros x H. constructor; inversion H; inversion H0; intuition. + Qed. + + Lemma Setminus_Union_r: + forall A s1 s2 s3, + Setminus A s1 (Union A s2 s3) = Setminus A (Setminus A s1 s2) s3. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H. inversion H. constructor. intuition. contradict H1. intuition. + * intros x H. inversion H. inversion H0. constructor; intuition. inversion H4; intuition. + Qed. + + Lemma Setminus_Disjoint_noop: + forall A s1 s2, + Intersection A s1 s2 = Empty_set A -> Setminus A s1 s2 = s1. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. inversion_clear H1. intuition. + * intros x H1. constructor; intuition. contradict H. + apply Inhabited_not_empty. + exists x. intuition. + Qed. + + Lemma Setminus_Included_empty: + forall A s1 s2, + Included A s1 s2 -> Setminus A s1 s2 = Empty_set A. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. inversion_clear H1. contradiction H2. intuition. + * intuition. + Qed. + End Sets_as_an_algebra. Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 61c53bc1d..2b56c63a0 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -288,13 +288,15 @@ ALLNATIVEFILES = \ $(OBJFILES:.o=.cmi) \ $(OBJFILES:.o=.cmx) \ $(OBJFILES:.o=.cmxs) -# trick: wildcard filters out non-existing files -NATIVEFILESTOINSTALL = $(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) FILESTOINSTALL = \ $(VOFILES) \ $(VFILES) \ $(GLOBFILES) \ - $(NATIVEFILESTOINSTALL) \ + $(NATIVEFILES) \ $(CMIFILESTOINSTALL) BYTEFILESTOINSTALL = \ $(CMOFILESTOINSTALL) \ @@ -431,7 +433,7 @@ all.pdf: $(VFILES) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` # FIXME: not quite right, since the output name is different -gallinahtml: GAL=g +gallinahtml: GAL=-g gallinahtml: html all-gal.ps: GAL=-g @@ -534,7 +536,7 @@ clean:: $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) $(HIDE)rm -f $(ALLDFILES) - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) @@ -562,7 +564,7 @@ cleanall:: clean archclean:: @# Extension point $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) .PHONY: archclean diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml index e1d1c60d7..f4777c4fb 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -14,7 +14,7 @@ type party = { sock : Unix.file_descr; cout : out_channel; mutable tokens : int; - priority : Flags.priority; + priority : priority; } let answer party msg = @@ -42,10 +42,10 @@ end = struct let is_empty q = !q = [] let rec split acc = function | [] -> List.rev acc, [] - | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l + | (_, { priority = Low }) :: _ as l -> List.rev acc, l | x :: xs -> split (x :: acc) xs let push (_,{ priority } as item) q = - if priority = Flags.Low then q := !q @ [item] + if priority = Low then q := !q @ [item] else let high, low = split [] !q in q := high @ (item :: low) @@ -148,7 +148,7 @@ let check_alive s = | Some s -> let cout = Unix.out_channel_of_descr s in set_binary_mode_out cout true; - output_string cout (print_request (Hello Flags.Low)); flush cout; + output_string cout (print_request (Hello Low)); flush cout; output_string cout (print_request Ping); flush cout; begin match Unix.select [s] [] [] 1.0 with | [s],_,_ -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6a3993ad4..2fa9f0ab4 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -71,7 +71,7 @@ let init_color () = let toploop_init = ref begin fun x -> let () = init_color () in - let () = CoqworkmgrApi.(init !Flags.async_proofs_worker_priority) in + let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in x end @@ -529,18 +529,18 @@ let print_config = ref false let print_tags = ref false let get_priority opt s = - try Flags.priority_of_string s + try CoqworkmgrApi.priority_of_string s with Invalid_argument _ -> prerr_endline ("Error: low/high expected after "^opt); exit 1 -let get_async_proofs_mode opt = function - | "no" | "off" -> Flags.APoff - | "yes" | "on" -> Flags.APon - | "lazy" -> Flags.APonLazy +let get_async_proofs_mode opt = let open Stm.AsyncOpts in function + | "no" | "off" -> APoff + | "yes" | "on" -> APon + | "lazy" -> APonLazy | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 let get_cache opt = function - | "force" -> Some Flags.Force + | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 @@ -649,23 +649,23 @@ let parse_args arglist = (* Options with one arg *) |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ()) |"-async-proofs" -> - Flags.async_proofs_mode := get_async_proofs_mode opt (next()) + Stm.AsyncOpts.async_proofs_mode := get_async_proofs_mode opt (next()) |"-async-proofs-j" -> - Flags.async_proofs_n_workers := (get_int opt (next ())) + Stm.AsyncOpts.async_proofs_n_workers := (get_int opt (next ())) |"-async-proofs-cache" -> - Flags.async_proofs_cache := get_cache opt (next ()) + Stm.AsyncOpts.async_proofs_cache := get_cache opt (next ()) |"-async-proofs-tac-j" -> - Flags.async_proofs_n_tacworkers := (get_int opt (next ())) + Stm.AsyncOpts.async_proofs_n_tacworkers := (get_int opt (next ())) |"-async-proofs-worker-priority" -> - Flags.async_proofs_worker_priority := get_priority opt (next ()) + WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()) |"-async-proofs-private-flags" -> - Flags.async_proofs_private_flags := Some (next ()); + Stm.AsyncOpts.async_proofs_private_flags := Some (next ()); |"-async-proofs-tactic-error-resilience" -> - Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ()) + Stm.AsyncOpts.async_proofs_tac_error_resilience := get_error_resilience opt (next ()) |"-async-proofs-command-error-resilience" -> - Flags.async_proofs_cmd_error_resilience := get_bool opt (next ()) + Stm.AsyncOpts.async_proofs_cmd_error_resilience := get_bool opt (next ()) |"-async-proofs-delegation-threshold" -> - Flags.async_proofs_delegation_threshold:= get_float opt (next ()) + Stm.AsyncOpts.async_proofs_delegation_threshold:= get_float opt (next ()) |"-worker-id" -> set_worker_id opt (next ()) |"-compat" -> let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in @@ -705,9 +705,9 @@ let parse_args arglist = |"-async-queries-always-delegate" |"-async-proofs-always-delegate" |"-async-proofs-full" -> - Flags.async_proofs_full := true; + Stm.AsyncOpts.async_proofs_full := true; |"-async-proofs-never-reopen-branch" -> - Flags.async_proofs_never_reopen_branch := true; + Stm.AsyncOpts.async_proofs_never_reopen_branch := true; |"-batch" -> set_batch_mode () |"-test-mode" -> Flags.test_mode := true |"-beautify" -> Flags.beautify := true @@ -716,7 +716,7 @@ let parse_args arglist = |"-color" -> set_color (next ()) |"-config"|"--config" -> print_config := true |"-debug" -> Coqinit.set_debug () - |"-stm-debug" -> Flags.stm_debug := true + |"-stm-debug" -> Stm.stm_debug := true |"-emacs" -> set_emacs () |"-filteropts" -> filter_opts := true |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode diff --git a/vernac/classes.ml b/vernac/classes.ml index cb1d2f7c7..3e47f881c 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -114,9 +114,10 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly evm term termtype = let kind = IsDefinition Instance in - let evm = - let levels = Univ.LSet.union (Univops.universes_of_constr termtype) - (Univops.universes_of_constr term) in + let evm = + let env = Global.env () in + let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) + (Univops.universes_of_constr env term) in Evd.restrict_universe_context evm levels in let uctx = Evd.check_univ_decl ~poly evm decl in diff --git a/vernac/command.ml b/vernac/command.ml index 66d4fe984..23be2c308 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 a1f916c78..c7342e6da 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/explainErr.ml b/vernac/explainErr.ml index 3a8e8fb43..d328ad0cf 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -75,8 +75,7 @@ let process_vernac_interp_error exn = match fst exn with wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) - | Logic.RefinerError e -> - let sigma, env = Pfedit.get_current_context () in + | Logic.RefinerError (env, sigma, e) -> wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) | Nametab.GlobalizationError q -> wrap_vernac_error exn diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d3de10235..00554e3ba 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 24d664951..181068089 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 0602e52e9..bdc97d48c 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 9fdd5e1c4..e632e7bbf 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -15,7 +15,7 @@ val primitive_flag : bool ref val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * - Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list * + Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 6a10eb43a..7e96f28de 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -288,7 +288,6 @@ let init_terminal_output ~color = *) let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning - (* This is specific to the toplevel *) let pr_loc loc = let fname = loc.Loc.fname in @@ -311,17 +310,23 @@ let print_err_exn ?extra any = std_logger ~pre_hdr Feedback.Error msg let with_output_to_file fname func input = - (* XXX FIXME: redirect std_ft *) - (* let old_logger = !logger in *) let channel = open_out (String.concat "." [fname; "out"]) in - (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *) + let old_fmt = !std_ft, !err_ft, !deep_ft in + let new_ft = Format.formatter_of_out_channel channel in + std_ft := new_ft; + err_ft := new_ft; + deep_ft := new_ft; try let output = func input in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; output with reraise -> let reraise = Backtrace.add_backtrace reraise in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; Exninfo.iraise reraise diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 63768d9b8..161e0c535 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1591,13 +1591,14 @@ let vernac_declare_reduction ~atts s r = let vernac_global_check c = let env = Global.env() in let sigma = Evd.from_env env in - let c,ctx = interp_constr env sigma c in + let c,uctx = interp_constr env sigma c in let senv = Global.safe_env() in - let cstrs = snd (UState.context_set ctx) in - let senv = Safe_typing.add_constraints cstrs senv in + let uctx = UState.context_set uctx in + let senv = Safe_typing.push_context_set false uctx senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - Feedback.msg_notice (print_safe_judgment env sigma j) + Feedback.msg_notice (print_safe_judgment env sigma j ++ + pr_universe_ctx_set sigma uctx) let get_nth_goal n = @@ -1656,13 +1657,13 @@ let vernac_print ~atts env sigma = | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) | PrintDebugGC -> msg_notice (Mltop.print_gc ()) | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) - | PrintGraph -> msg_notice (Prettyp.print_graph()) + | PrintGraph -> msg_notice (Prettyp.print_graph env sigma) | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) | PrintCoercionPaths (cls,clt) -> - msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) + msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) | PrintUniverses (b, dst) -> let univ = Global.universes () in @@ -1696,7 +1697,7 @@ let vernac_print ~atts env sigma = let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in - msg_notice (Printer.pr_assumptionset (Global.env ()) nassums) + msg_notice (Printer.pr_assumptionset env sigma nassums) | PrintStrategy r -> print_strategy r let global_module r = |