diff options
51 files changed, 383 insertions, 136 deletions
diff --git a/Makefile.ci b/Makefile.ci index 677fd734bf..de03ee8e84 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -18,7 +18,6 @@ CI_TARGETS= \ ci-coq_dpdgraph \ ci-coquelicot \ ci-corn \ - ci-cpdt \ ci-cross-crypto \ ci-elpi \ ci-ext-lib \ @@ -41,7 +40,6 @@ CI_TARGETS= \ ci-sf \ ci-simple-io \ ci-stdlib2 \ - ci-tlc \ ci-unimath \ ci-verdi-raft \ ci-vst diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index f2df99dcd6..d20eea7874 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -142,8 +142,12 @@ let check_inductive env mind mb = mind_universes; mind_variance; mind_private; mind_typing_flags; } = - (* Locally set the oracle for further typechecking *) - let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in + (* Locally set typing flags for further typechecking *) + let mb_flags = mb.mind_typing_flags in + let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded; + check_positive = mb_flags.check_positive; + check_universes = mb_flags.check_universes; + conv_oracle = mb_flags.conv_oracle} env in Indtypes.check_inductive env mind entry in let check = check mind in diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 62f72c8edc..a67945ae94 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -31,14 +31,31 @@ let pr_engagement env = | PredicativeSet -> str "Theory: Set is predicative" end -let is_ax _ cb = not (Declareops.constant_has_body cb) -let pr_ax env = - let axs = fold_constants (fun c ce acc -> if is_ax c ce then c::acc else acc) env [] in +let pr_assumptions ass axs = if axs = [] then - str "Axioms: <none>" + str ass ++ str ": <none>" else - hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Constant.print axs) + hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs) + +let pr_axioms env = + let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Constant.to_string c :: acc else acc) env [] in + pr_assumptions "Axioms" csts + +let pr_type_in_type env = + let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_universes then Constant.to_string c :: acc else acc) env [] in + let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_universes then MutInd.to_string c :: acc else acc) env csts in + pr_assumptions "Constants/Inductives relying on type-in-type" csts + +let pr_unguarded env = + let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_guarded then Constant.to_string c :: acc else acc) env [] in + let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_guarded then MutInd.to_string c :: acc else acc) env csts in + pr_assumptions "Constants/Inductives relying on unsafe (co)fixpoints" csts + +let pr_nonpositive env = + let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in + pr_assumptions "Inductives whose positivity is assumed" inds + let print_context env = if !output_context then begin @@ -47,7 +64,10 @@ let print_context env = (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_ax env))); + str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_nonpositive env))) end let stats env = diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 9b41fbcb7a..09b8c48c15 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -17,9 +17,12 @@ let set_indirect_accessor f = indirect_accessor := f let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); - (* Locally set the oracle for further typechecking *) - let oracle = env.env_typing_flags.conv_oracle in - let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in + (* Locally set typing flags for further typechecking *) + let orig_flags = env.env_typing_flags in + let cb_flags = cb.const_typing_flags in + let env = Environ.set_typing_flags {orig_flags with check_guarded = cb_flags.check_guarded; + check_universes = cb_flags.check_universes; + conv_oracle = cb_flags.conv_oracle} env in (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with @@ -57,8 +60,8 @@ let check_constant_declaration env kn cb = if poly then add_constant kn cb env else add_constant kn cb env' in - (* Reset the value of the oracle *) - Environ.set_oracle env oracle + (* Reset the value of the typing flags *) + Environ.set_typing_flags orig_flags env (** {6 Checking modules } *) diff --git a/checker/values.ml b/checker/values.ml index 8dc09aed87..ac9bc26344 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -219,7 +219,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] @@ -20,7 +20,7 @@ license: "LGPL-2.1" depends: [ "ocaml" { >= "4.05.0" } - "dune" { build & >= "1.6.0" } + "dune" { build & >= "1.10.0" } "ocamlfind" { build } "num" ] diff --git a/coqide-server.opam b/coqide-server.opam index 0325d2549c..5712ca08c2 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -19,7 +19,7 @@ dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" depends: [ - "dune" { build & >= "1.6.0" } + "dune" { build & >= "1.10.0" } "coq" { = version } ] diff --git a/coqide.opam b/coqide.opam index 2507acbb26..d680ebb5f4 100644 --- a/coqide.opam +++ b/coqide.opam @@ -17,7 +17,7 @@ dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" depends: [ - "dune" { build & >= "1.6.0" } + "dune" { build & >= "1.10.0" } "coqide-server" { = version } "lablgtk3" { >= "3.0.beta5" } "lablgtk3-sourceview3" { >= "3.0.beta5" } diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 0c8213b8f5..78c0b4b2c7 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1132,7 +1132,7 @@ function make_findlib { function make_dune { make_ocaml - if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 dune-1.6.3 ; then + if build_prep https://github.com/ocaml/dune/archive/ 1.10.0 tar.gz 1 dune-1.10.0 ; then log2 make release log2 make install diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 408d36df7f..9ed7180807 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -120,15 +120,18 @@ Currently available artifacts are: Additionally, an experimental Dune build is provided: https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev -- the Coq documentation, built in the `doc:*` jobs. When submitting - a documentation PR, this can help reviewers checking the rendered result: - - + Coq's Reference Manual [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman - + Coq's Standard Library Documentation [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base - + Coq's ML API Documentation [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc +- the Coq documentation, built in the `doc:*` jobs. When submitting a + documentation PR, this can help reviewers checking the rendered + result. **@coqbot** will automatically post links to these + artifacts in the PR checks section. Furthemore, these artifacts are + automatically deployed at: + + + Coq's Reference Manual [master branch]: + <https://coq.github.io/doc/master/refman/> + + Coq's Standard Library Documentation [master branch]: + <https://coq.github.io/doc/master/stdlib/> + + Coq's ML API Documentation [master branch]: + <https://coq.github.io/doc/master/api/> ### GitLab and Windows diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index ad22c394d8..3923fea30e 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -56,14 +56,14 @@ # NB: stdpp and Iris refs are gotten from the opam files in the Iris # and lambdaRust repos respectively. -: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" +: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}" : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" +: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" : "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" : "${lambdaRust_CI_REF:=master}" -: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}" +: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}" : "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}" ######################################################################## diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh deleted file mode 100755 index ca759c7b39..0000000000 --- a/dev/ci/ci-cpdt.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -wget http://adam.chlipala.net/cpdt/cpdt.tgz -tar xvfz cpdt.tgz - -( cd cpdt && make clean && make ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh deleted file mode 100755 index a2f0bea555..0000000000 --- a/dev/ci/ci-tlc.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -FORCE_GIT=1 -git_download tlc - -( cd "${CI_BUILD_DIR}/tlc" && make ) diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 372e40a0b7..37c6e2f619 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -52,7 +52,7 @@ order to use them, do: ``` $ make -f Makefile.dune voboot # Only once per session -$ dune exec dev/shim/coqtop-prelude +$ dune exec -- dev/shim/coqtop-prelude ``` or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets @@ -108,14 +108,14 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec dev/dune-dbg /path/to/foo.v +dune exec -- dev/dune-dbg /path/to/foo.v (ocd) source dune_db ``` or ``` -dune exec dev/dune-dbg checker Foo +dune exec -- dev/dune-dbg checker Foo (ocd) source dune_db ``` @@ -130,7 +130,7 @@ For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. After doing `make -f Makefile.dune voboot`, the following commands should work: ``` -dune exec dev/shim/coqbyte-prelude +dune exec -- dev/shim/coqbyte-prelude > Drop. # #directory "dev";; # #use "include_dune";; diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index 8dfe1e7833..8736c0f9b8 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/bc9df0f66110039e495b6debe3a6cda4a1bb0fed.tar.gz"; - sha256 = "0y2w259j0vqiwjhjvlbsaqnp1nl2zwz6sbwwhkrqn7k7fmhmxnq1"; + url = "https://github.com/NixOS/nixpkgs/archive/31c38894c90429c9554eab1b416e59e3b6e054df.tar.gz"; + sha256 = "1fv14rj5zslzm14ak4lvwqix94gm18h28376h4hsmrqqpnfqwsdw"; }) diff --git a/doc/changelog/07-commands-and-options/10291-typing-flags.rst b/doc/changelog/07-commands-and-options/10291-typing-flags.rst new file mode 100644 index 0000000000..ef7adde801 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10291-typing-flags.rst @@ -0,0 +1,4 @@ +- Adding unsafe commands to enable/disable guard checking, positivity checking + and universes checking (providing a local `-type-in-type`). + See :ref:`controlling-typing-flags`. + (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier). diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 903ee115c9..cdb7ea834f 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -162,7 +162,7 @@ need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the generation and checking of the proof objects. The ``-quick`` flag can be -passed to ``coqc`` or ``coqtop`` to produce, quickly, ``.vio`` files. +passed to ``coqc`` to produce, quickly, ``.vio`` files. Alternatively, when using a Makefile produced by ``coq_makefile``, the ``quick`` target can be used to compile all files using the ``-quick`` flag. @@ -182,7 +182,7 @@ running ``coqc`` as usual. Alternatively one can turn each ``.vio`` into the corresponding ``.vo``. All .vio files can be processed in parallel, hence this alternative might -be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to +be faster. The command ``coqc -schedule-vio2vo 2 a b c`` can be used to obtain a good scheduling for two workers to produce ``a.vo``, ``b.vo``, and ``c.vo``. When using a Makefile produced by ``coq_makefile``, the ``vio2vo`` target can be used for that purpose. Variable ``J`` should be set to the number @@ -197,7 +197,7 @@ There is an extra, possibly even faster, alternative: just check the proof tasks stored in ``.vio`` files without producing the ``.vo`` files. This is possibly faster because all the proof tasks are independent, hence one can further partition the job to be done between workers. The -``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a +``coqc -schedule-vio-checking 6 a b c`` command can be used to obtain a good scheduling for 6 workers to check all the proof tasks of ``a.vio``, ``b.vio``, and ``c.vio``. Auxiliary files are used to predict how long a proof task will take, assuming it will take the same amount of time it took diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 91dfa34494..2cbd41af8b 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -778,7 +778,8 @@ Simple inductive types The types of the constructors have to satisfy a *positivity condition* (see Section :ref:`positivity`). This condition ensures the soundness of - the inductive definition. + the inductive definition. The positivity checking can be disabled using + the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 774732825a..c391cc949d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1204,6 +1204,79 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. _controlling-typing-flags: + +Controlling Typing Flags +---------------------------- + +.. flag:: Guard Checking + + This option can be used to enable/disable the guard checking of + fixpoints. Warning: this can break the consistency of the system, use at your + own risk. Decreasing argument can still be specified: the decrease is not checked + anymore but it still affects the reduction of the term. Unchecked fixpoints are + printed by :cmd:`Print Assumptions`. + +.. flag:: Positivity Checking + + This option can be used to enable/disable the positivity checking of inductive + types and the productivity checking of coinductive types. Warning: this can + break the consistency of the system, use at your own risk. Unchecked + (co)inductive types are printed by :cmd:`Print Assumptions`. + +.. flag:: Universe Checking + + This option can be used to enable/disable the checking of universes, providing a + form of "type in type". Warning: this breaks the consistency of the system, use + at your own risk. Constants relying on "type in type" are printed by + :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line + argument (see :ref:`command-line-options`). + +.. cmd:: Print Typing Flags + + Print the status of the three typing flags: guard checking, positivity checking + and universe checking. + +.. example:: + + .. coqtop:: all reset + + Unset Guard Checking. + + Print Typing Flags. + + Fixpoint f (n : nat) : False + := f n. + + Fixpoint ackermann (m n : nat) {struct m} : nat := + match m with + | 0 => S n + | S m => + match n with + | 0 => ackermann m 1 + | S n => ackermann m (ackermann (S m) n) + end + end. + + Print Assumptions ackermann. + + Note that the proper way to define the Ackermann function is to use + an inner fixpoint: + + .. coqtop:: all reset + + Fixpoint ack m := + fix ackm n := + match m with + | 0 => S n + | S m' => + match n with + | 0 => ack m' 1 + | S n' => ack m' (ackm n') + end + end. + + .. _internal-registration-commands: Internal registration commands diff --git a/dune-project b/dune-project index f0ac11ba61..45d9d06314 100644 --- a/dune-project +++ b/dune-project @@ -1,2 +1,8 @@ -(lang dune 1.6) +(lang dune 1.10) (name coq) +(using coq 0.1) + +; We cannot set this to true until as long as the build is not +; properly bootstrapped [that is, we remove the voboot target] +; +; (generate_opam_files true) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index dff19dee5e..8d32684b09 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -66,6 +66,10 @@ type typing_flags = { (** If [false] then fixed points and co-fixed points are assumed to be total. *) + check_positive : bool; + (** If [false] then inductive types are assumed positive and co-inductive + types are assumed productive. *) + check_universes : bool; (** If [false] universe constraints are not checked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 7a553700e8..391b139496 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -19,6 +19,7 @@ module RelDecl = Context.Rel.Declaration let safe_flags oracle = { check_guarded = true; + check_positive = true; check_universes = true; conv_oracle = oracle; share_reduction = true; diff --git a/kernel/environ.ml b/kernel/environ.ml index 9a75f0b682..655094e88b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -216,6 +216,9 @@ let lookup_named_ctxt id ctxt = let fold_constants f env acc = Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc +let fold_inductives f env acc = + Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc + (* Global constants *) let lookup_constant_key kn env = @@ -418,6 +421,7 @@ let set_engagement c env = (* Unsafe *) (* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *) let same_flags { check_guarded; + check_positive; check_universes; conv_oracle; indices_matter; @@ -426,6 +430,7 @@ let same_flags { enable_native_compiler; } alt = check_guarded == alt.check_guarded && + check_positive == alt.check_positive && check_universes == alt.check_universes && conv_oracle == alt.conv_oracle && indices_matter == alt.indices_matter && diff --git a/kernel/environ.mli b/kernel/environ.mli index 6cd4f96645..e6d814ac7d 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -176,6 +176,7 @@ val pop_rel_context : int -> env -> env (** Useful for printing *) val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a +val fold_inductives : (MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) -> env -> 'a -> 'a (** {5 Global constants } {6 Add entries to global environment } *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b0366d6ec0..aa3ef715db 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -546,7 +546,7 @@ let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in (* Then check positivity conditions *) - let chkpos = (Environ.typing_flags env).check_guarded in + let chkpos = (Environ.typing_flags env).check_positive in let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) mie.mind_entry_inds in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ea45f699ce..6970a11e72 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -194,6 +194,18 @@ let set_typing_flags c senv = if env == senv.env then senv else { senv with env } +let set_check_guarded b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_guarded = b } senv + +let set_check_positive b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_positive = b } senv + +let set_check_universes b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_universes = b } senv + let set_indices_matter indices_matter senv = set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 2406b6add1..fa53fa33fa 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -130,6 +130,9 @@ val set_engagement : Declarations.engagement -> safe_transformer0 val set_indices_matter : bool -> safe_transformer0 val set_typing_flags : Declarations.typing_flags -> safe_transformer0 val set_share_reduction : bool -> safe_transformer0 +val set_check_guarded : bool -> safe_transformer0 +val set_check_positive : bool -> safe_transformer0 +val set_check_universes : bool -> safe_transformer0 val set_VM : bool -> safe_transformer0 val set_native_compiler : bool -> safe_transformer0 val make_sprop_cumulative : safe_transformer0 diff --git a/library/global.ml b/library/global.ml index ca774dbd74..0fc9e11364 100644 --- a/library/global.ml +++ b/library/global.ml @@ -89,6 +89,9 @@ let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c) +let set_check_positive c = globalize0 (Safe_typing.set_check_positive c) +let set_check_universes c = globalize0 (Safe_typing.set_check_universes c) let typing_flags () = Environ.typing_flags (env ()) let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) diff --git a/library/global.mli b/library/global.mli index d034bc4208..b089b7dd80 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,6 +31,9 @@ val named_context : unit -> Constr.named_context val set_engagement : Declarations.engagement -> unit val set_indices_matter : bool -> unit val set_typing_flags : Declarations.typing_flags -> unit +val set_check_guarded : bool -> unit +val set_check_positive : bool -> unit +val set_check_universes : bool -> unit val typing_flags : unit -> Declarations.typing_flags val make_sprop_cumulative : unit -> unit val set_allow_sprop : bool -> unit diff --git a/library/library.mllib b/library/library.mllib index a3d78cc81b..3b75438ccd 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -10,5 +10,4 @@ Library States Kindops Goptions -Keys Coqlib diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 726752a2bf..1493092f2f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -546,7 +546,7 @@ let rewrite_core_unif_flags = { Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = Evar.Set.empty; + Unification.allowed_evars = Unification.AllowAll; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; diff --git a/library/keys.ml b/pretyping/keys.ml index 9964992433..f8eecd80d4 100644 --- a/library/keys.ml +++ b/pretyping/keys.ml @@ -49,7 +49,7 @@ module KeyOrdered = struct | _, KGlob _ -> -1 | KGlob _, _ -> 1 | k, k' -> Int.compare (hash k) (hash k') - + let equal k1 k2 = match k1, k2 with | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2 @@ -69,7 +69,7 @@ let add_kv k v m = try Keymap.modify k (fun k' vs -> Keyset.add v vs) m with Not_found -> Keymap.add k (Keyset.singleton v) m -let add_keys k v = +let add_keys k v = keys := add_kv k v (add_kv v k !keys) let equiv_keys k k' = @@ -85,7 +85,7 @@ let load_keys _ (_,(ref,ref')) = let cache_keys o = load_keys 1 o -let subst_key subst k = +let subst_key subst k = match k with | KGlob gr -> KGlob (subst_global_reference subst gr) | _ -> k @@ -98,7 +98,7 @@ let discharge_key = function | x -> Some x let discharge_keys (_,(k,k')) = - match discharge_key k, discharge_key k' with + match discharge_key k, discharge_key k' with | Some x, Some y -> Some (x, y) | _ -> None @@ -124,7 +124,7 @@ let constr_key kind c = | App (f, _) -> aux f | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p)) | Cast (p, _, _) -> aux p - | Lambda _ -> KLam + | Lambda _ -> KLam | Prod _ -> KProd | Case _ -> KCase | Fix _ -> KFix @@ -132,7 +132,7 @@ let constr_key kind c = | Rel _ -> KRel | Meta _ -> raise Not_found | Evar _ -> raise Not_found - | Sort _ -> KSort + | Sort _ -> KSort | LetIn _ -> KLet | Int _ -> KInt in Some (aux c) @@ -152,10 +152,10 @@ let pr_key pr_global = function | KRel -> str"Rel" | KInt -> str"Int" -let pr_keyset pr_global v = +let pr_keyset pr_global v = prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) -let pr_mapping pr_global k v = +let pr_mapping pr_global k v = pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v let pr_keys pr_global = diff --git a/library/keys.mli b/pretyping/keys.mli index a7adf7791b..a7adf7791b 100644 --- a/library/keys.mli +++ b/pretyping/keys.mli diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 34a6cecc95..0ca39f0404 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -35,4 +35,5 @@ Indrec GlobEnv Cases Pretyping +Keys Unification diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a9eb43e573..4d34139ec0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -254,6 +254,10 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) +type allowed_evars = +| AllowAll +| AllowFun of (Evar.t -> bool) + type core_unify_flags = { modulo_conv_on_closed_terms : TransparentState.t option; (* What this flag controls was activated with all constants transparent, *) @@ -287,8 +291,8 @@ type core_unify_flags = { (* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *) (* when ?B is a Meta. *) - frozen_evars : Evar.Set.t; - (* Evars of this set are considered axioms and never instantiated *) + allowed_evars : allowed_evars; + (* Evars that are allowed to be instantiated *) (* Useful e.g. for autorewrite *) restrict_conv_on_strict_subterms : bool; @@ -339,7 +343,7 @@ let default_core_unify_flags () = check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; modulo_eta = true; @@ -417,6 +421,10 @@ let default_no_delta_unify_flags ts = resolve_evars = false } +let allow_new_evars sigma = + let undefined = Evd.undefined_map sigma in + AllowFun (fun evk -> not (Evar.Map.mem evk undefined)) + (* Default flags for looking for subterms in elimination tactics *) (* Not used in practice at the current date, to the exception of *) (* allow_K) because only closed terms are involved in *) @@ -424,9 +432,7 @@ let default_no_delta_unify_flags ts = (* call w_unify for induction/destruct/case/elim (13/6/2011) *) let elim_core_flags sigma = { (default_core_unify_flags ()) with modulo_betaiota = false; - frozen_evars = - fold_undefined (fun evk _ evars -> Evar.Set.add evk evars) - sigma Evar.Set.empty; + allowed_evars = allow_new_evars sigma; } let elim_flags_evars sigma = @@ -600,8 +606,12 @@ let do_reduce ts (env, nb) sigma c = Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state ts env sigma (c, Stack.empty)) +let is_evar_allowed flags evk = match flags.allowed_evars with +| AllowAll -> true +| AllowFun f -> f evk + let isAllowedEvar sigma flags c = match EConstr.kind sigma c with - | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) + | Evar (evk,_) -> is_evar_allowed flags evk | _ -> false @@ -749,7 +759,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e evarsubst) else error_cannot_unify_local curenv sigma (m,n,cM) | Evar (evk,_ as ev), Evar (evk',_) - when not (Evar.Set.mem evk flags.frozen_evars) + when is_evar_allowed flags evk && Evar.equal evk evk' -> begin match constr_cmp cv_pb env sigma flags cM cN with | Some sigma -> @@ -758,14 +768,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e sigma,metasubst,((curenv,ev,cN)::evarsubst) end | Evar (evk,_ as ev), _ - when not (Evar.Set.mem evk flags.frozen_evars) + when is_evar_allowed flags evk && not (occur_evar sigma evk cN) -> let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cnvars cmvars then sigma,metasubst,((curenv,ev,cN)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Evar (evk,_ as ev) - when not (Evar.Set.mem evk flags.frozen_evars) + when is_evar_allowed flags evk && not (occur_evar sigma evk cM) -> let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cmvars cnvars then @@ -1554,7 +1564,7 @@ let default_matching_core_flags sigma = check_applied_meta_types = true; use_pattern_unification = false; use_meta_bound_pattern_unification = false; - frozen_evars = Evar.Map.domain (Evd.undefined_map sigma); + allowed_evars = allow_new_evars sigma; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = false; diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0ee71246d8..d7ddbcb721 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -13,6 +13,10 @@ open EConstr open Environ open Evd +type allowed_evars = +| AllowAll +| AllowFun of (Evar.t -> bool) + type core_unify_flags = { modulo_conv_on_closed_terms : TransparentState.t option; use_metas_eagerly_in_conv_on_closed_terms : bool; @@ -22,7 +26,7 @@ type core_unify_flags = { check_applied_meta_types : bool; use_pattern_unification : bool; use_meta_bound_pattern_unification : bool; - frozen_evars : Evar.Set.t; + allowed_evars : allowed_evars; restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; diff --git a/printing/printer.ml b/printing/printer.ml index ec1b9b8e49..e3225fadd5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -853,7 +853,8 @@ let pr_goal_emacs ~proof gid sid = type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) @@ -873,7 +874,7 @@ struct | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> - Constant.CanOrd.compare k1 k2 + GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 | _ -> -1 @@ -903,14 +904,20 @@ let pr_assumptionset env sigma s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> - (* FIXME? *) - let mp,lab = Constant.repr2 kn in - str (ModPath.to_string mp) ++ str "." ++ Label.print lab + Names.Constant.print kn + in + let safe_pr_global env gr = + try pr_global_env (Termops.vars_of_env env) gr + with Not_found -> + let open GlobRef in match gr with + | VarRef id -> Id.print id + | ConstRef con -> Constant.print con + | IndRef (mind,_) -> MutInd.print mind + | ConstructRef _ -> assert false in let safe_pr_inductive env kn = try pr_inductive env (kn,0) with Not_found -> - (* FIXME? *) MutInd.print kn in let safe_pr_ltype env sigma typ = @@ -927,9 +934,11 @@ let pr_assumptionset env sigma s = | Constant kn -> safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> - hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.") - | Guarded kn -> - hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") + hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") + | Guarded gr -> + hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") + | TypeInType gr -> + hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in let fold t typ accu = let (v, a, o, tr) = accu in @@ -1003,3 +1012,8 @@ let print_and_diff oldp newp = pr_open_subgoals ~proof in Feedback.msg_notice output;; + +let pr_typing_flags flags = + str "check_guarded: " ++ bool flags.check_guarded ++ fnl () + ++ str "check_positive: " ++ bool flags.check_positive ++ fnl () + ++ str "check_universes: " ++ bool flags.check_universes diff --git a/printing/printer.mli b/printing/printer.mli index a72f319636..788f303aee 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -191,7 +191,8 @@ val print_and_diff : Proof.t option -> Proof.t option -> unit type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) @@ -207,3 +208,5 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t + +val pr_typing_flags : Declarations.typing_flags -> Pp.t diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 1904d9b112..8e7d1df29a 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -108,7 +108,7 @@ let fail_quick_core_unif_flags = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/auto.ml b/tactics/auto.ml index 499e7a63d7..67f49f0074 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -49,7 +49,7 @@ let auto_core_unif_flags_of st1 st2 = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 05f40d0570..cf5c64c3ae 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -151,7 +151,7 @@ let pr_ev evs ev = open Auto open Unification -let auto_core_unif_flags st freeze = { +let auto_core_unif_flags st allowed_evars = { modulo_conv_on_closed_terms = Some st; use_metas_eagerly_in_conv_on_closed_terms = true; use_evars_eagerly_in_conv_on_closed_terms = false; @@ -160,14 +160,14 @@ let auto_core_unif_flags st freeze = { check_applied_meta_types = false; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = freeze; + allowed_evars; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; modulo_eta = false; } -let auto_unif_flags freeze st = - let fl = auto_core_unif_flags st freeze in +let auto_unif_flags ?(allowed_evars = AllowAll) st = + let fl = auto_core_unif_flags st allowed_evars in { core_unify_flags = fl; merge_unify_flags = fl; subterm_unify_flags = fl; @@ -357,23 +357,25 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm let open Proofview.Notations in let prods, concl = EConstr.decompose_prod_assum sigma concl in let nprods = List.length prods in - let freeze = + let allowed_evars = try match hdc with | Some (hd,_) when only_classes -> let cl = Typeclasses.class_info env sigma hd in if cl.cl_strict then - Evarutil.undefined_evars_of_term sigma concl - else Evar.Set.empty - | _ -> Evar.Set.empty - with e when CErrors.noncritical e -> Evar.Set.empty + let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in + let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in + AllowFun allowed + else AllowAll + | _ -> AllowAll + with e when CErrors.noncritical e -> AllowAll in let hint_of_db = hintmap_of sigma hdc secvars concl in let hintl = List.map_append (fun db -> let tacs = hint_of_db db in - let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in + let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in List.map (fun x -> (flags, x)) tacs) (local_db::db_list) in @@ -1198,7 +1200,7 @@ let autoapply c i = let hintdb = try Hints.searchtable_map i with Not_found -> CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ ".")) in - let flags = auto_unif_flags Evar.Set.empty + let flags = auto_unif_flags (Hints.Hint_db.transparent_state hintdb) in let cty = Tacmach.New.pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in diff --git a/tactics/declare.ml b/tactics/declare.ml index 17e873f017..c280760e84 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -246,7 +246,7 @@ let get_roles export eff = let feedback_axiom () = Feedback.(feedback AddedAxiom) let is_unsafe_typing_flags () = let flags = Environ.typing_flags (Global.env()) in - not (flags.check_universes && flags.check_guarded) + not (flags.check_universes && flags.check_guarded && flags.check_positive) let define_constant ~side_effect ~name cd = let open Proof_global in diff --git a/tactics/equality.ml b/tactics/equality.ml index b9d718dd61..220b9bc475 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -38,7 +38,6 @@ open Coqlib open Declarations open Indrec open Clenv -open Evd open Ind_tables open Eqschemes open Locus @@ -107,7 +106,7 @@ let rewrite_core_unif_flags = { check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = true; @@ -126,16 +125,17 @@ let freeze_initial_evars sigma flags clause = (* We take evars of the type: this may include old evars! For excluding *) (* all old evars, including the ones occurring in the rewriting lemma, *) (* we would have to take the clenv_value *) - let newevars = Evarutil.undefined_evars_of_term sigma (clenv_type clause) in - let evars = - fold_undefined (fun evk _ evars -> - if Evar.Set.mem evk newevars then evars - else Evar.Set.add evk evars) - sigma Evar.Set.empty in + let newevars = lazy (Evarutil.undefined_evars_of_term sigma (clenv_type clause)) in + let initial = Evd.undefined_map sigma in + let allowed evk = + if Evar.Map.mem evk initial then false + else Evar.Set.mem evk (Lazy.force newevars) + in + let allowed_evars = AllowFun allowed in {flags with - core_unify_flags = {flags.core_unify_flags with frozen_evars = evars}; - merge_unify_flags = {flags.merge_unify_flags with frozen_evars = evars}; - subterm_unify_flags = {flags.subterm_unify_flags with frozen_evars = evars}} + core_unify_flags = {flags.core_unify_flags with allowed_evars}; + merge_unify_flags = {flags.merge_unify_flags with allowed_evars}; + subterm_unify_flags = {flags.subterm_unify_flags with allowed_evars}} let make_flags frzevars sigma flags clause = if frzevars then freeze_initial_evars sigma flags clause else flags @@ -188,8 +188,7 @@ let rewrite_conv_closed_core_unif_flags = { use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; - (* This is set dynamically *) + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; @@ -223,8 +222,7 @@ let rewrite_keyed_core_unif_flags = { use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; - (* This is set dynamically *) + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v new file mode 100644 index 0000000000..bd20d9c804 --- /dev/null +++ b/test-suite/success/typing_flags.v @@ -0,0 +1,43 @@ + +Print Typing Flags. +Unset Guard Checking. +Fixpoint f' (n : nat) : nat := f' n. + +Fixpoint f (n : nat) : nat. +Proof. + exact (f n). +Defined. + +Fixpoint bla (A:Type) (n:nat) := match n with 0 =>0 | S n => n end. + +Print Typing Flags. + +Set Guard Checking. + +Print Assumptions f. + +Unset Universe Checking. + +Definition T := Type. +Fixpoint g (n : nat) : T := T. + +Print Typing Flags. +Set Universe Checking. + +Fail Definition g2 (n : nat) : T := T. + +Fail Definition e := fix e (n : nat) : nat := e n. + +Unset Positivity Checking. + +Inductive Cor := +| Over : Cor +| Next : ((Cor -> list nat) -> list nat) -> Cor. + +Set Positivity Checking. +Print Assumptions Cor. + +Inductive Box := +| box : forall n, f n = n -> g 2 -> Box. + +Print Assumptions Box. diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 1920d493de..adb416e3ce 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -193,9 +193,7 @@ let pp_vo_dep dir fmt vo = pp_rule fmt all_targets deps action let pp_mlg_dep _dir fmt ml = - let target = Filename.(remove_extension ml) ^ ".ml" in - let mlg_rule = "(run coqpp %{pp-file})" in - pp_rule fmt [target] [ml] mlg_rule + fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml) let pp_dep dir fmt oo = match oo with | VO vo -> pp_vo_dep dir fmt vo diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index ab341e4ab8..a72e43de01 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -313,9 +313,15 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = if cb.const_typing_flags.check_guarded then accu else let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu + ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu in - if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then + let accu = + if cb.const_typing_flags.check_universes then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu + in + if not (Declareops.constant_has_body cb) then let t = type_of_constant cb in let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Constant kn,l)) t accu @@ -329,10 +335,24 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = accu | IndRef (m,_) | ConstructRef ((m,_),_) -> let mind = lookup_mind m in - if mind.mind_typing_flags.check_guarded then - accu - else - let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu - in - GlobRef.Map_env.fold fold graph ContextObjectMap.empty + let accu = + if mind.mind_typing_flags.check_positive then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu + in + let accu = + if mind.mind_typing_flags.check_guarded then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu + in + let accu = + if mind.mind_typing_flags.check_universes then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu + in + accu + + in GlobRef.Map_env.fold fold graph ContextObjectMap.empty diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 54ce527ea2..8a94a010a0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1048,6 +1048,7 @@ GRAMMAR EXTEND Gram | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> { PrintCoercionPaths (s,t) } | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions } + | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags } | IDENT "Tables" -> { PrintTables } | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) } | IDENT "Hint" -> { PrintHintGoal } diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 23a8bf20a3..cf87646905 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -553,7 +553,7 @@ let declare_default_schemes kn = let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets in if !elim_flag && (mib.mind_finite <> Declarations.BiFinite || !bifinite_elim_flag) - && mib.mind_typing_flags.check_guarded then + && mib.mind_typing_flags.check_positive then declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; if is_eq_flag() then try_declare_beq_scheme kn; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index bd6f8f01d8..f91983d31c 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -514,6 +514,8 @@ let string_of_theorem_kind = let open Decls in function ++ pr_class_rawexpr t | PrintCanonicalConversions -> keyword "Print Canonical Structures" + | PrintTypingFlags -> + keyword "Print Typing Flags" | PrintTables -> keyword "Print Tables" | PrintHintGoal -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 819d1acfb5..4ae9d6d54f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1724,6 +1724,30 @@ let () = optread = Nativenorm.get_profiling_enabled; optwrite = Nativenorm.set_profiling_enabled } +let _ = + declare_bool_option + { optdepr = false; + optname = "guard checking"; + optkey = ["Guard"; "Checking"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded); + optwrite = (fun b -> Global.set_check_guarded b) } + +let _ = + declare_bool_option + { optdepr = false; + optname = "positivity/productivity checking"; + optkey = ["Positivity"; "Checking"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive); + optwrite = (fun b -> Global.set_check_positive b) } + +let _ = + declare_bool_option + { optdepr = false; + optname = "universes checking"; + optkey = ["Universe"; "Checking"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes); + optwrite = (fun b -> Global.set_check_universes b) } + let vernac_set_strategy ~local l = let local = Option.default false local in let glob_ref r = @@ -1928,6 +1952,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = let vernac_print ~pstate ~atts = let sigma, env = get_current_or_global_context ~pstate in function + | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () | PrintFullContext-> print_full_context_typ env sigma | PrintSectionContext qid -> print_sec_context_typ env sigma qid diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 88f87cdd0b..b712d7e264 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -24,6 +24,7 @@ type goal_reference = | GoalId of Id.t type printable = + | PrintTypingFlags | PrintTables | PrintFullContext | PrintSectionContext of qualid |