diff options
137 files changed, 943 insertions, 1220 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f434b63d74..b3dc1fa896 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -10,7 +10,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-01-28-V1" + CACHEKEY: "bionic_coq-V2019-02-17-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -100,6 +100,7 @@ after_script: - set +e variables: OPAM_SWITCH: edge + OPAM_VARIANT: "+flambda" artifacts: name: "$CI_JOB_NAME" paths: @@ -109,7 +110,7 @@ after_script: .dune-ci-template: &dune-ci-template stage: test dependencies: - - build:egde:dune:dev + - build:edge+flambda:dune:dev script: - set -e - echo 'start:coq.test' @@ -118,6 +119,7 @@ after_script: - set +e variables: &dune-ci-template-vars OPAM_SWITCH: edge + OPAM_VARIANT: "+flambda" artifacts: &dune-ci-template-artifacts name: "$CI_JOB_NAME" expire_in: 1 month @@ -132,7 +134,7 @@ after_script: dependencies: - not-a-real-job script: - - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no' + - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/"' - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman - make install-doc-sphinx artifacts: @@ -222,12 +224,6 @@ build:base+32bit: OPAM_VARIANT: "+32bit" COQ_EXTRA_CONF: "-native-compiler yes" -build:edge: - <<: *build-template - variables: - OPAM_SWITCH: edge - COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" - build:edge+flambda: <<: *build-template variables: @@ -236,7 +232,7 @@ build:edge+flambda: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts " COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" -build:egde:dune:dev: +build:edge+flambda:dune:dev: <<: *dune-template build:base+async: @@ -282,12 +278,14 @@ pkg:opam: dependencies: [] script: - set -e - - opam pin add coq . - - opam pin add coqide-server . - - opam pin add coqide . + - opam pin add --kind=path coq.$COQ_VERSION . + - opam pin add --kind=path coqide-server.$COQ_VERSION . + - opam pin add --kind=path coqide.$COQ_VERSION . - set +e variables: - OPAM_SWITCH: edge + COQ_VERSION: "8.10" + OPAM_SWITCH: "edge" + OPAM_VARIANT: "+flambda" .nix-template: &nix-template image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git @@ -401,13 +399,6 @@ test-suite:base+32bit: variables: OPAM_VARIANT: "+32bit" -test-suite:edge: - <<: *test-suite-template - dependencies: - - build:edge - variables: - OPAM_SWITCH: edge - test-suite:edge+flambda: <<: *test-suite-template dependencies: @@ -419,10 +410,11 @@ test-suite:edge+flambda: test-suite:egde:dune:dev: stage: test dependencies: - - build:egde:dune:dev + - build:edge+flambda:dune:dev script: make -f Makefile.dune test-suite variables: OPAM_SWITCH: edge + OPAM_VARIANT: "+flambda" artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -444,7 +436,7 @@ test-suite:edge+trunk+make: - make -j "$NJOBS" world - make -j "$NJOBS" test-suite UNIT_TESTS= variables: - OPAM_SWITCH: edge + OPAM_SWITCH: base artifacts: name: "$CI_JOB_NAME.logs" when: always @@ -470,7 +462,7 @@ test-suite:edge+trunk+dune: - export COQ_UNIT_TEST=noop - dune runtest --profile=ocaml409 variables: - OPAM_SWITCH: edge + OPAM_SWITCH: base artifacts: name: "$CI_JOB_NAME.logs" when: always @@ -499,13 +491,6 @@ validate:base+32bit: variables: OPAM_VARIANT: "+32bit" -validate:edge: - <<: *validate-template - dependencies: - - build:edge - variables: - OPAM_SWITCH: edge - validate:edge+flambda: <<: *validate-template dependencies: diff --git a/CHANGES.md b/CHANGES.md index 26573b9185..38c197d8cc 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -95,6 +95,8 @@ Tactics by posing the specifying equation for `Z.div` and `Z.modulo` before replacing them with atoms. +- Ltac backtraces can be turned on using the "Ltac Backtrace" option. + Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort @@ -130,6 +132,9 @@ Vernacular commands for all commands that support it. In particular, it does not have any effect on tactics anymore. May cause some incompatibilities. +- The algorithm computing implicit arguments now behaves uniformly for primitive + projection and application nodes (bug #9508). + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: @@ -189,6 +194,8 @@ Misc - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. +- Removed option "Printing Primitive Projection Compatibility" + SSReflect - New intro patterns: diff --git a/Makefile.build b/Makefile.build index ca988aaac2..8afb498a63 100644 --- a/Makefile.build +++ b/Makefile.build @@ -198,7 +198,10 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # TIME="%C (%U user, %S sys, %e total, %M maxres)" COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) -BOOTCOQC=$(TIMER) $(COQC) -boot $(COQOPTS) +# Beware this depends on the makefile being in a particular dir, we +# should pass an absolute path here but windows is tricky +# c.f. https://github.com/coq/coq/pull/9560 +BOOTCOQC=$(TIMER) $(COQC) -coqlib . -boot $(COQOPTS) LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) MLINCLUDES=$(LOCALINCLUDES) diff --git a/Makefile.doc b/Makefile.doc index 4b2dd8ed4d..912738cd00 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -31,7 +31,7 @@ DVIPS:=dvips HTMLSTYLE:=coqremote # Sphinx-related variables -SPHINXENV:=COQBIN="$(CURDIR)/bin/" +SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(CURDIR)" SPHINXOPTS= -j4 SPHINXWARNERROR ?= 1 ifeq ($(SPHINXWARNERROR),1) diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index d2d1efcb2c..4329b2d743 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -28,11 +28,8 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = | PrimRecord data -> Some (Some (Array.map pi1 data)) in let mind_entry_universes = match mb.mind_universes with - | Monomorphic_ind univs -> Monomorphic_ind_entry univs - | Polymorphic_ind auctx -> Polymorphic_ind_entry (AUContext.names auctx, AUContext.repr auctx) - | Cumulative_ind auctx -> - Cumulative_ind_entry (AUContext.names (ACumulativityInfo.univ_context auctx), - ACumulativityInfo.repr auctx) + | Monomorphic univs -> Monomorphic_entry univs + | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx) in let mind_entry_inds = Array.map_to_list (fun ind -> let mind_entry_arity, mind_entry_template = match ind.mind_arity with @@ -64,6 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = mind_entry_params = mb.mind_params_ctxt; mind_entry_inds; mind_entry_universes; + mind_entry_variance = mb.mind_variance; mind_entry_private = mb.mind_private; } @@ -135,7 +133,8 @@ let check_same_record r1 r2 = match r1, r2 with let check_inductive env mind mb = let entry = to_entry mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; - mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes; + mind_nparams; mind_nparams_rec; mind_params_ctxt; + mind_universes; mind_variance; mind_private; mind_typing_flags; } = (* Locally set the oracle for further typechecking *) @@ -157,6 +156,7 @@ let check_inductive env mind mb = check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt); ignore mind_universes; (* Indtypes did the necessary checking *) + ignore mind_variance; (* Indtypes did the necessary checking *) ignore mind_private; (* passed through Indtypes *) ignore mind_typing_flags; diff --git a/checker/checker.ml b/checker/checker.ml index af8d1e5617..3db7ccdcae 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -350,9 +350,9 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x)); - print_endline (Envars.coqlib ()); - exit 0 + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); + print_endline (Envars.coqlib ()); + exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () @@ -386,7 +386,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x)); + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); Flags.if_verbose print_header (); init_load_path (); make_senv () diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index c33c6d5d09..b86d491d72 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -16,8 +16,8 @@ let check_constant_declaration env kn cb = (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with - | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env - | Polymorphic_const auctx -> + | Monomorphic ctx -> false, push_context_set ~strict:true ctx env + | Polymorphic auctx -> let ctx = Univ.AUContext.repr auctx in let env = push_context ~strict:false ctx env in true, env diff --git a/checker/values.ml b/checker/values.ml index 7ca2dc8050..66467fa8f5 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -112,7 +112,6 @@ let v_variance = v_enum "variance" 3 let v_instance = Annot ("instance", Array v_level) let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|] -let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|] let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) @@ -226,14 +225,14 @@ let v_cst_def = let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] -let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] +let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; v_constr; Any; - v_const_univs; + v_univs; Opt v_context_set; v_bool; v_typing_flags|] @@ -276,10 +275,6 @@ let v_record_info = v_sum "record_info" 2 [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |] -let v_ind_pack_univs = - v_sum "abstract_inductive_universes" 0 - [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|] - let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; v_record_info; @@ -289,7 +284,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Int; Int; v_rctxt; - v_ind_pack_univs; (* universes *) + v_univs; (* universes *) + Opt (Array v_variance); Opt v_bool; v_typing_flags|] diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index a5aa54144c..b4d2a9ca4e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -62,27 +62,30 @@ git_download() { local PROJECT=$1 local DEST="$CI_BUILD_DIR/$PROJECT" + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" if [ -d "$DEST" ]; then echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then - local GITURL_VAR="${PROJECT}_CI_GITURL" - local GITURL="${!GITURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" git clone "$GITURL" "$DEST" cd "$DEST" git checkout "$REF" else # When possible, we download tarballs to reduce bandwidth and latency local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" local ARCHIVEURL="${!ARCHIVEURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" mkdir -p "$DEST" cd "$DEST" - wget "$ARCHIVEURL/$REF.tar.gz" - tar xvfz "$REF.tar.gz" --strip-components=1 - rm -f "$REF.tar.gz" + local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1) + if [[ "$COMMIT" == "" ]]; then + # $REF must have been a tag or hash, not a branch + COMMIT="$REF" + fi + wget "$ARCHIVEURL/$COMMIT.tar.gz" + tar xvfz "$COMMIT.tar.gz" --strip-components=1 + rm -f "$COMMIT.tar.gz" fi } diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 4cd7faf757..43278c37b1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-01-28-V1" +# CACHEKEY: "bionic_coq-V2019-02-17-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -56,9 +56,6 @@ ENV COMPILER_EDGE="4.07.1" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ BASE_OPAM_EDGE="dune-release.1.1.0" -RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE - # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh new file mode 100644 index 0000000000..cca85a2f68 --- /dev/null +++ b/dev/ci/user-overlays/09439-sep-variance.sh @@ -0,0 +1,14 @@ + +if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then + elpi_CI_REF=sep-variance + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=sep-variance + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + mtac2_CI_REF=sep-variance + mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 + + paramcoq_CI_REF=sep-variance + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi diff --git a/dev/include b/dev/include index b982f4c9fa..c5de83b900 100644 --- a/dev/include +++ b/dev/include @@ -41,8 +41,6 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; -#install_printer (* cumulativity info *) ppcumulativity_info;; -#install_printer (* abstract cumulativity info *) ppabstract_cumulativity_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index f588c20d02..2e8a7455de 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -9,10 +9,17 @@ CODE=0 -# We assume that all merge commits are from the main branch +if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then + # The FIRST parent of bot merges is from the PR, the second is + # current master + head=$(git rev-parse HEAD~) +else + head=$(git rev-parse HEAD) +fi + +# We assume that all non-bot merge commits are from the main branch # For Coq it is extremely rare for this assumption to be broken -read -r base < <(git log -n 1 --merges --pretty='format:%H') -head=$(git rev-parse HEAD) +read -r base < <(git log -n 1 --merges --pretty='format:%H' "$head") dev/lint-commits.sh "$base" "$head" || CODE=1 diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh index 41392be5d7..ad60b1115f 100755 --- a/dev/tools/create_overlays.sh +++ b/dev/tools/create_overlays.sh @@ -42,7 +42,7 @@ OVERLAY_BRANCH=$(git rev-parse --abbrev-ref HEAD) OVERLAY_FILE=$(mktemp overlay-XXXX) # Create the overlay file -printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then \n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" +printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then\n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" # We first try to build the contribs while test $# -gt 0 diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 813ad71be9..425f21de70 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -12,7 +12,8 @@ OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq" # Set SLOW_CONF to have the confirmation output wait for a newline # E.g. call $ SLOW_CONF= dev/tools/merge-pr.sh /PR number/ -if [ -z ${SLOW_CONF+x} ]; then +# emacs doesn't send characters until the RET so we can't quick_conf +if [ -z ${SLOW_CONF+x} ] || [ -n "$INSIDE_EMACS" ]; then QUICK_CONF="-n 1" else QUICK_CONF="" diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index eab88c7290..a6ecec7e33 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -70,8 +70,6 @@ install_printer Top_printers.ppevar_universe_context install_printer Top_printers.ppconstraints install_printer Top_printers.ppuniverseconstraints install_printer Top_printers.ppuniverse_context_future -install_printer Top_printers.ppcumulativity_info -install_printer Top_printers.ppabstract_cumulativity_info install_printer Top_printers.ppuniverses install_printer Top_printers.ppnamedcontextval install_printer Top_printers.ppenv diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 2629cf8626..a3d2f33216 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -222,8 +222,6 @@ let ppuniverseconstraints c = pp (UnivProblem.Set.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c) -let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = let env = Global.env () in diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 4d874cdd12..cb32d2294c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -145,8 +145,6 @@ val ppevar_universe_context : UState.t -> unit val ppconstraints : Univ.Constraint.t -> unit val ppuniverseconstraints : UnivProblem.Set.t -> unit val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit -val ppcumulativity_info : Univ.CumulativityInfo.t -> unit -val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit val ppuniverses : UGraph.t -> unit val ppnamedcontextval : Environ.named_context_val -> unit @@ -13,7 +13,7 @@ (source_tree tools) (env_var SPHINXWARNOPT)) (action - (run sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index e4f078c1d6..fac0035de1 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -214,17 +214,17 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo Example:: - .. coqtop:: in reset undo + .. coqtop:: in reset Print nat. Definition a := 1. The blank line after the directive is required. If you begin a proof, - include an ``Abort`` afterwards to reset coqtop for the next example. + use the ``abort`` option to reset coqtop for the next example. Here is a list of permissible options: - - Display options + - Display options (choose exactly one) - ``all``: Display input and output - ``in``: Display only input @@ -234,8 +234,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after - running all the commands in this block + - ``fail``: Don't die if a command fails + - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode) + - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any) ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per @@ -509,7 +510,7 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: .. coqtop:: all @@ -519,7 +520,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents. Lemma l2: 2 + 2 <> 1. -Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. +Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas. Abbreviations and macros ------------------------ diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 81f25bf274..78803a927f 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -265,7 +265,7 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: .. coqtop:: all @@ -275,7 +275,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents. Lemma l2: 2 + 2 <> 1. -Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. +Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas. Abbreviations and macros ------------------------ diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index cc788b3595..b474c51f17 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -627,14 +627,10 @@ logical equivalence: Instance all_iff_morphism (A : Type) : Proper (pointwise_relation A iff ==> iff) (@all A). -.. coqtop:: all +.. coqtop:: all abort Proof. simpl_relation. -.. coqtop:: none - - Abort. - One then has to show that if two predicates are equivalent at every point, their universal quantifications are equivalent. Once we have declared such a morphism, it will be used by the setoid rewriting diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 43d302114e..c7ea7e326f 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -44,25 +44,20 @@ Leibniz equality on some type. An example implementation is: eqb_leibniz x y H := match x, y return x = y with tt, tt => eq_refl tt end }. -If one does not give all the members in the Instance declaration, Coq -enters the proof-mode and the user is asked to build inhabitants of -the remaining fields, e.g.: +Using :cmd:`Program Instance`, if one does not give all the members in +the Instance declaration, Coq generates obligations for the remaining +fields, e.g.: .. coqtop:: in - Instance eq_bool : EqDec bool := + Require Import Program.Tactics. + Program Instance eq_bool : EqDec bool := { eqb x y := if x then y else negb y }. .. coqtop:: all - Proof. intros x y H. - -.. coqtop:: all - - destruct x ; destruct y ; (discriminate || reflexivity). - -.. coqtop:: all - + Next Obligation. + destruct x ; destruct y ; (discriminate || reflexivity). Defined. One has to take care that the transparency of every field is @@ -131,14 +126,14 @@ the constraints as a binding context before the instance, e.g.: .. coqtop:: in - Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := + Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := { eqb x y := match x, y with | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) end }. .. coqtop:: none - Abort. + Admit Obligations. These instances are used just as well as lemmas in the instance hint database. @@ -157,13 +152,13 @@ vernacular, except it accepts any binding context as argument. For example: Context `{EA : EqDec A}. - Global Instance option_eqb : EqDec (option A) := + Global Program Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true | _, _ => false end }. - Admitted. + Admit Obligations. End EqDec_defs. @@ -564,12 +559,12 @@ Settings This flag allows to switch the behavior of instance declarations made through the Instance command. - + When it is on (the default), instances that have unsolved holes in + + When it is off (the default), they fail with an error instead. + + + When it is on, instances that have unsolved holes in their proof-term silently open the proof mode with the remaining obligations to prove. - + When it is off, they fail with an error instead. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 9d2afc080f..48ad60c6dd 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -142,6 +142,7 @@ exclude_patterns = [ 'introduction.rst', 'refman-preamble.rst', 'README.rst', + 'README.gen.rst', 'README.template.rst' ] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS] diff --git a/doc/sphinx/dune b/doc/sphinx/dune index fff025c919..353d58c676 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1 +1,8 @@ (dirs :standard _static) + +(rule (targets README.gen.rst) + (deps (source_tree ../tools/coqrst) README.template.rst) + (action (run ../tools/coqrst/regen_readme.py %{targets}))) + +(alias (name refman-html) + (action (diff README.rst README.gen.rst))) diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 3ef88e6506..e05df65c63 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -963,10 +963,9 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]` .. inference:: W-Ind \WFE{Γ_P} - (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k} (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ - \WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ} + \WF{E;~\ind{p}{Γ_I}{Γ_C}}{} provided that the following side conditions hold: @@ -976,7 +975,7 @@ provided that the following side conditions hold: context of parameters, + for :math:`j=1… k` we have that :math:`A_j` is an arity of sort :math:`s_j` and :math:`I_j ∉ E`, + for :math:`i=1… n` we have that :math:`C_i` is a type of constructor of :math:`I_{q_i}` which - satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ Γ ∪ E`. + satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ E`. One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 963242ea72..c1eab8a970 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -264,17 +264,13 @@ arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. -.. coqtop:: in +.. coqtop:: in abort Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. -.. coqtop:: none - - Abort. - .. _datatypes: Datatypes diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 933f07674a..25f983ac1e 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -247,11 +247,6 @@ Primitive Projections printing time (even though they are absent in the actual AST manipulated by the kernel). -.. flag:: Printing Primitive Projection Compatibility - - This compatibility option (on by default) governs the - printing of pattern matching over primitive records. - Primitive Record Types ++++++++++++++++++++++ @@ -297,8 +292,8 @@ the folded version delta-reduces to the unfolded version. This allows to precisely mimic the usual unfolding rules of constants. Projections obey the usual ``simpl`` flags of the ``Arguments`` command in particular. There is currently no way to input unfolded primitive projections at the -user-level, and one must use the :flag:`Printing Primitive Projection Compatibility` -to display unfolded primitive projections as matches and distinguish them from folded ones. +user-level, and there is no way to display unfolded projections differently +from folded ones. Compatibility Projections and :g:`match` @@ -1967,14 +1962,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` and :g:`B` can be synthesized in the next statement. - .. coqtop:: all + .. coqtop:: all abort Lemma is_law_S : is_law S. - .. coqtop:: none - - Abort. - .. note:: If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 1b4d2315aa..eebf1f11e1 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -34,6 +34,11 @@ allow dynamic linking of tactics). You can switch to the OCaml toplevel with the command ``Drop.``, and come back to the |Coq| toplevel with the command ``Coqloop.loop();;``. +.. flag:: Coqtop Exit On Error + + This option, off by default, causes coqtop to exit with status code + ``1`` if a command produces an error instead of recovering from it. + Batch compilation (coqc) ------------------------ diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index bd16b70d02..63d6a229ed 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -53,7 +53,7 @@ rule of thumb, all the variables that appear inside constructors in the indices of the hypothesis should be generalized. This is exactly what the ``generalize_eqs_vars`` variant does: -.. coqtop:: all +.. coqtop:: all abort generalize_eqs_vars H. induction H. @@ -65,7 +65,7 @@ as well in this case, e.g.: .. coqtop:: none - Abort. + Require Import Coq.Program.Equality. .. coqtop:: in @@ -88,11 +88,7 @@ automatically do such simplifications (which may involve the axiom K). This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality`` does. For example, we might simplify the previous goals considerably: -.. coqtop:: all - - Require Import Coq.Program.Equality. - -.. coqtop:: all +.. coqtop:: all abort induction p ; simplify_dep_elim. @@ -105,10 +101,6 @@ are ``dependent induction`` and ``dependent destruction`` that do induction or simply case analysis on the generalized hypothesis. For example we can redo what we’ve done manually with dependent destruction: -.. coqtop:: none - - Abort. - .. coqtop:: in Lemma ex : forall n m:nat, Le (S n) m -> P n m. @@ -117,7 +109,7 @@ redo what we’ve done manually with dependent destruction: intros n m H. -.. coqtop:: all +.. coqtop:: all abort dependent destruction H. @@ -126,10 +118,6 @@ destructed hypothesis actually appeared in the goal, the tactic would still be able to invert it, contrary to dependent inversion. Consider the following example on vectors: -.. coqtop:: none - - Abort. - .. coqtop:: in Set Implicit Arguments. @@ -230,29 +218,21 @@ name. A term is either an application of: Once we have this datatype we want to do proofs on it, like weakening: -.. coqtop:: in +.. coqtop:: in abort Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau. -.. coqtop:: none - - Abort. - The problem here is that we can’t just use induction on the typing derivation because it will forget about the ``G ; D`` constraint appearing in the instance. A solution would be to rewrite the goal as: -.. coqtop:: in +.. coqtop:: in abort Lemma weakening' : forall G' tau, term G' tau -> forall G D, (G ; D) = G' -> forall tau', term (G, tau' ; D) tau. -.. coqtop:: none - - Abort. - With this proper separation of the index from the instance and the right induction loading (putting ``G`` and ``D`` after the inducted-on hypothesis), the proof will go through, but it is a very tedious diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 4f486a777d..3e87e8acd8 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -602,7 +602,7 @@ Failing .. example:: - .. coqtop:: all + .. coqtop:: all fail Goal True. Proof. fail. Abort. @@ -701,7 +701,7 @@ tactic .. example:: - .. coqtop:: all + .. coqtop:: all abort Ltac time_constr1 tac := let eval_early := match goal with _ => restart_timer "(depth 1)" end in @@ -716,7 +716,6 @@ tactic let y := time_constr1 ltac:(fun _ => eval compute in x) in y) in pose v. - Abort. Local definitions ~~~~~~~~~~~~~~~~~ @@ -847,7 +846,7 @@ We can carry out pattern matching on terms with: .. example:: - .. coqtop:: all + .. coqtop:: all abort Ltac f x := match x with @@ -859,10 +858,6 @@ We can carry out pattern matching on terms with: Goal True. f (3+4). - .. coqtop:: none - - Abort. - .. _ltac-match-goal: Pattern matching on goals @@ -1026,14 +1021,10 @@ Counting the goals Goal True /\ True /\ True. split;[|split]. - .. coqtop:: all + .. coqtop:: all abort all:pr_numgoals. - .. coqtop:: none - - Abort. - Testing boolean expressions ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1162,6 +1153,15 @@ Printing |Ltac| tactics Debugging |Ltac| tactics ------------------------ +Backtraces +~~~~~~~~~~ + +.. flag:: Ltac Backtrace + + Setting this flag displays a backtrace on Ltac failures that can be useful + to find out what went wrong. It is disabled by default for performance + reasons. + Info trace ~~~~~~~~~~ @@ -1309,10 +1309,10 @@ performance issue. .. coqtop:: all - Set Ltac Profiling. - tac. - Show Ltac Profile. - Show Ltac Profile "omega". + Set Ltac Profiling. + tac. + Show Ltac Profile. + Show Ltac Profile "omega". .. coqtop:: in diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 24645a8cc3..2300a317f1 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -529,16 +529,12 @@ Requesting information .. example:: - .. coqtop:: all + .. coqtop:: all abort Goal exists n, n = 0. eexists ?[n]. Show n. - .. coqtop:: none - - Abort. - .. cmdv:: Show Script :name: Show Script @@ -739,14 +735,10 @@ Notes: split. - .. coqtop:: all + .. coqtop:: all abort 2: split. - .. coqtop:: none - - Abort. - .. .. coqtop:: none @@ -759,14 +751,10 @@ Notes: intros n. - .. coqtop:: all + .. coqtop:: all abort intros m. - .. coqtop:: none - - Abort. - This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after the split because it has not changed. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 0bcca0fe56..237b534d67 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -215,7 +215,7 @@ construct differs from the latter in that .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -275,7 +275,7 @@ example, the null and all list function(al)s can be defined as follows: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -376,7 +376,7 @@ expressions such as .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -401,7 +401,7 @@ each point of use, e.g., the above definition can be written: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -464,7 +464,7 @@ defined by the following declaration: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -518,7 +518,7 @@ For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -639,7 +639,7 @@ The tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -652,11 +652,7 @@ The tactic: Lemma test x : f x + f x = f x. set t := f _. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart set t := {2}(f _). @@ -694,7 +690,7 @@ conditions: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -715,7 +711,7 @@ conditions: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -736,7 +732,7 @@ Moreover: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -756,7 +752,7 @@ Moreover: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -789,7 +785,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -810,7 +806,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -831,7 +827,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -862,7 +858,7 @@ selection. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -879,7 +875,7 @@ only one occurrence of the selected term. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -910,7 +906,7 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. @@ -926,7 +922,7 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. @@ -1042,7 +1038,7 @@ constants to the goal. For example, the proof of [#3]_ - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1104,7 +1100,7 @@ The ``:`` tactical is used to operate on an element in the context. to encapsulate the inductive step in a single command: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1257,7 +1253,7 @@ The elim tactic .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1297,7 +1293,7 @@ existential metavariables of sort :g:`Prop`. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1477,7 +1473,7 @@ context to interpret wildcards; in particular it can accommodate the .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1752,7 +1748,7 @@ Clears are deferred until the end of the intro pattern. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -1813,7 +1809,7 @@ Block introduction .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1866,7 +1862,7 @@ deal with the possible parameters of the constants introduced. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1885,7 +1881,7 @@ under fresh |SSR| names. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1952,7 +1948,7 @@ be substituted. Here is a small example on lists. We define first a function which adds an element at the end of a given list. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1989,19 +1985,17 @@ be substituted. Lemma test l : (length l) * 2 = length (l ++ l). case: (lastP l). - Applied to the same goal, the command: - ``case: l / (lastP l).`` - generates the same subgoals but ``l`` has been cleared from both contexts. + Applied to the same goal, the tactc ``case: l / (lastP l)`` + generates the same subgoals but ``l`` has been cleared from both contexts: - Again applied to the same goal, the command. + .. coqtop:: all restart - .. coqtop:: none + case: l / (lastP l). - Abort. + Again applied to the same goal: - .. coqtop:: all + .. coqtop:: all restart abort - Lemma test l : (length l) * 2 = length (l ++ l). case: {1 3}l / (lastP l). Note that selected occurrences on the left of the ``/`` @@ -2015,10 +2009,6 @@ be substituted. .. example:: - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test l : (length l) * 2 = length (l ++ l). @@ -2260,7 +2250,7 @@ to the others. Here is a small example on lists. We define first a function which adds an element at the end of a given list. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2379,7 +2369,7 @@ between standard Ltac in and the |SSR| tactical in. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2454,7 +2444,7 @@ the holes are abstracted in term. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2468,7 +2458,7 @@ the holes are abstracted in term. The invokation of ``have`` is equivalent to: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2486,7 +2476,7 @@ tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2539,7 +2529,7 @@ the further use of the intermediate step. For instance, .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2567,7 +2557,7 @@ destruction of existential assumptions like in the tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2594,7 +2584,7 @@ term for the intermediate lemma, using tactics of the form: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2615,7 +2605,7 @@ After the :token:`i_pattern`, a list of binders is allowed. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. From Coq Require Import Omega. @@ -2634,7 +2624,7 @@ Since the :token:`i_pattern` can be omitted, to avoid ambiguity, bound variables can be surrounded with parentheses even if no type is specified: -.. coqdoc:: +.. coqtop:: all restart have (x) : 2 * x = x + x by omega. @@ -2648,13 +2638,8 @@ copying the goal itself. .. example:: - .. coqtop:: none + .. coqtop:: all restart abort - Abort All. - - .. coqtop:: all - - Lemma test : True. have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2675,10 +2660,9 @@ context entry name. .. coqtop:: none - Abort All. Set Printing Depth 15. - .. coqtop:: all + .. coqtop:: all abort Inductive Ord n := Sub x of x < n. Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). @@ -2694,11 +2678,7 @@ For this purpose the ``[: name ]`` intro pattern and the tactic .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; omega. @@ -2711,11 +2691,7 @@ with have and an explicit term, they must be used as follows: .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n := Sub m pm. @@ -2734,11 +2710,7 @@ makes use of it). .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; omega. @@ -2755,20 +2727,20 @@ typeclass inference. .. coqtop:: none - Abort All. - Axiom ty : Type. Axiom t : ty. Goal True. - .. coqdoc:: + .. coqtop:: all have foo : ty. Full inference for ``ty``. The first subgoal demands a proof of such instantiated statement. + .. A strange bug prevents using the coqtop directive here + .. coqdoc:: have foo : ty := . @@ -2778,13 +2750,13 @@ typeclass inference. statement. Note that no proof term follows ``:=``, hence two subgoals are generated. - .. coqdoc:: + .. coqtop:: all restart have foo : ty := t. No inference for ``ty`` and ``t``. - .. coqdoc:: + .. coqtop:: all restart abort have foo := t. @@ -2833,10 +2805,9 @@ The ``have`` modifier can follow the ``suff`` tactic. .. coqtop:: none - Abort All. Axioms G P : Prop. - .. coqtop:: all + .. coqtop:: all abort Lemma test : G. suff have H : P. @@ -2901,10 +2872,6 @@ are unique. .. example:: - .. coqtop:: none - - Abort All. - .. coqtop:: all Lemma quo_rem_unicity d q1 q2 r1 r2 : @@ -2926,7 +2893,7 @@ pattern will be used to process its instance. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -2975,7 +2942,7 @@ illustrated in the following example. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2994,7 +2961,7 @@ illustrated in the following example. the pattern ``id (addx x)``, that would produce the following first subgoal - .. coqtop:: none reset + .. coqtop:: reset none From Coq Require Import ssreflect Omega. Set Implicit Arguments. @@ -3128,14 +3095,14 @@ An :token:`r_item` can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. coqtop:: all abort Definition double x := x + x. Definition ddouble x := double (double x). @@ -3147,21 +3114,16 @@ An :token:`r_item` can be: The |SSR| terms containing holes are *not* typed as abstractions in this context. Hence the following script fails. - .. coqtop:: none - - Abort. - .. coqtop:: all Definition f := fun x y => x + y. Lemma test x y : x + y = f y x. - Fail rewrite -[f y]/(y + _). - but the following script succeeds + .. coqtop:: all fail - .. coqtop:: none + rewrite -[f y]/(y + _). - Restart. + but the following script succeeds .. coqtop:: all @@ -3252,7 +3214,7 @@ proof of basic results on natural numbers arithmetic. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3288,7 +3250,7 @@ side of the equality the user wants to rewrite. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3308,7 +3270,7 @@ the equality. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3331,7 +3293,7 @@ Occurrence switches and redex switches .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3360,7 +3322,7 @@ repetition. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3390,7 +3352,7 @@ rewrite operations prescribed by the rules on the current goal. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3399,7 +3361,7 @@ rewrite operations prescribed by the rules on the current goal. Section Test. - .. coqtop:: all + .. coqtop:: all abort Variables (a b c : nat). Hypothesis eqab : a = b. @@ -3413,10 +3375,6 @@ rewrite operations prescribed by the rules on the current goal. ``(eqab, eqac)`` is actually a |Coq| term and we can name it with a definition: - .. coqtop:: none - - Abort. - .. coqtop:: all Definition multi1 := (eqab, eqac). @@ -3433,7 +3391,7 @@ literal matches have priority. .. example:: - .. coqtop:: all + .. coqtop:: all abort Definition d := a. Hypotheses eqd0 : d = 0. @@ -3450,11 +3408,7 @@ repeated anew. .. example:: - .. coqtop:: none - - Abort. - - .. coqtop:: all + .. coqtop:: all abort Hypothesis eq_adda_b : forall x, x + a = b. Hypothesis eq_adda_c : forall x, x + a = c. @@ -3477,10 +3431,6 @@ tactic rewrite ``(=~ multi1)`` is equivalent to ``rewrite multi1_rev``. .. example:: - .. coqtop:: none - - Abort. - .. coqtop:: all Hypothesis eqba : b = a. @@ -3536,7 +3486,7 @@ Anyway this tactic is *not* equivalent to .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3552,11 +3502,7 @@ Anyway this tactic is *not* equivalent to while the other tactic results in - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart abort rewrite (_ : forall x, x * 0 = 0). @@ -3590,7 +3536,7 @@ cases: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3613,13 +3559,9 @@ cases: there is no occurrence of the head symbol ``f`` of the rewrite rule in the goal. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart fail - Fail rewrite H. + rewrite H. Rewriting with ``H`` first requires unfolding the occurrences of ``f`` @@ -3627,21 +3569,13 @@ cases: occurrence), using tactic ``rewrite /f`` (for a global replacement of f by g) or ``rewrite pattern/f``, for a finer selection. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart rewrite /f H. alternatively one can override the pattern inferred from ``H`` - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart rewrite [f _]H. @@ -3660,7 +3594,7 @@ corresponding new goals will be generated. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -3668,7 +3602,7 @@ corresponding new goals will be generated. Unset Printing Implicit Defensive. Set Warnings "-notation-overridden". - .. coqtop:: all + .. coqtop:: all abort Axiom leq : nat -> nat -> bool. Notation "m <= n" := (leq m n) : nat_scope. @@ -3691,10 +3625,6 @@ corresponding new goals will be generated. As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to solve the existential variable. - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. @@ -3743,7 +3673,7 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. From Coq Require Import List. @@ -3767,7 +3697,7 @@ definition. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3877,7 +3807,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3904,7 +3834,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3927,7 +3857,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3948,7 +3878,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4128,7 +4058,7 @@ parentheses are required around more complex patterns. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4167,7 +4097,7 @@ Contextual patterns in rewrite .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4331,7 +4261,7 @@ generation (see section :ref:`generation_of_equations_ssr`). The following script illustrates a toy example of this feature. Let us define a function adding an element at the end of a list: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect List. Set Implicit Arguments. @@ -4406,7 +4336,7 @@ Here is an example of a regular, but nontrivial, eliminator. Here is a toy example illustrating this feature. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4433,7 +4363,7 @@ Here is an example of a regular, but nontrivial, eliminator. elim/plus_ind: {z}_. elim/plus_ind: z / _. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4458,7 +4388,7 @@ Here is an example of a regular, but nontrivial, eliminator. ``plus (plus x y) z`` thus instantiating the last ``_`` with ``z``. Note that the tactic: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4488,7 +4418,7 @@ Here is an example of a truncated eliminator: Consider the goal: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4552,7 +4482,7 @@ disjunction. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4573,7 +4503,7 @@ disjunction. This operation is so common that the tactic shell has specific syntax for it. The following scripts: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4592,12 +4522,7 @@ disjunction. or more directly: - .. coqtop:: none - - Abort. - Lemma test a : P (a || a) -> True. - - .. coqtop:: all + .. coqtop:: all restart move/P2Q=> HQa. @@ -4613,7 +4538,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4646,7 +4571,7 @@ relevant for the current goal. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4690,7 +4615,7 @@ assumption to some given arguments. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4719,7 +4644,7 @@ bookkeeping steps. The following example use the ``~~`` prenex notation for boolean negation: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4775,7 +4700,7 @@ analysis: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4792,7 +4717,7 @@ analysis .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4847,7 +4772,7 @@ For instance, the following lemma: .. coqdoc:: - Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). + Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). relates the boolean conjunction to the logical one ``/\``. Note that in ``andP``, ``b1`` and ``b2`` are two boolean variables and the @@ -4882,7 +4807,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4901,7 +4826,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. .. coqtop:: none - Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). + Restart. .. coqtop:: all @@ -4923,7 +4848,7 @@ The view mechanism is compatible with reflect predicates. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4931,17 +4856,13 @@ The view mechanism is compatible with reflect predicates. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. coqtop:: all abort Lemma test (a b : bool) (Ha : a) (Hb : b) : a /\ b. apply/andP. Conversely - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test (a b : bool) : a /\ b -> a. @@ -5045,7 +4966,7 @@ but they also allow complex transformation, involving negations. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5078,7 +4999,7 @@ actually uses its propositional interpretation. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5140,7 +5061,7 @@ In this context, the identity view can be used when no view has to be applied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5156,7 +5077,7 @@ In this context, the identity view can be used when no view has to be applied: The same goal can be decomposed in several ways, and the user may choose the most convenient interpretation. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5232,7 +5153,7 @@ pass a given hypothesis to a lemma. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5291,7 +5212,7 @@ equivalences are indeed taken into account, otherwise only single looks for any notation that contains fragment as a substring. If the ``ssrbool.v`` library is imported, the command: ``Search "~~".`` answers : - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6f57cc53a9..b5e9a902c6 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -749,9 +749,9 @@ Applying theorems The direct application of ``Rtrans`` with ``apply`` fails because no value for ``y`` in ``Rtrans`` is found by ``apply``: - .. coqtop:: all + .. coqtop:: all fail - Fail apply Rtrans. + apply Rtrans. A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``. @@ -762,42 +762,26 @@ Applying theorems Note that ``n`` can be inferred from the goal, so the following would work too. - .. coqtop:: none - - Abort. Goal R n p. - - .. coqtop:: in + .. coqtop:: in restart apply (Rtrans _ m). More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the unknown m: - .. coqtop:: none - - Abort. Goal R n p. - - .. coqtop:: in + .. coqtop:: in restart apply Rtrans with (y := m). Another solution is to mention the proof of ``(R x y)`` in ``Rtrans`` - .. coqtop:: none - - Abort. Goal R n p. - - .. coqtop:: all + .. coqtop:: all restart apply Rtrans with (1 := Rnm). ... or the proof of ``(R y z)``. - .. coqtop:: none - - Abort. Goal R n p. - - .. coqtop:: all + .. coqtop:: all restart apply Rtrans with (2 := Rmp). @@ -805,11 +789,7 @@ Applying theorems finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This instantiates the existential variable and completes the proof. - .. coqtop:: none - - Abort. Goal R n p. - - .. coqtop:: all + .. coqtop:: all restart abort eapply Rtrans. @@ -2528,11 +2508,10 @@ and an explanation of the underlying technique. Variable P : nat -> nat -> Prop. Variable Q : forall n m:nat, Le n m -> Prop. Goal forall n m, Le (S n) m -> P n m. - intros. .. coqtop:: out - Show. + intros. To prove the goal, we may need to reason by cases on :g:`H` and to derive that :g:`m` is necessarily of the form :g:`(S m0)` for certain :g:`m0` and that @@ -2552,10 +2531,8 @@ and an explanation of the underlying technique. context to use it after. In that case we can use :tacn:`inversion` that does not clear the equalities: - .. coqtop:: none + .. coqtop:: none restart - Abort. - Goal forall n m, Le (S n) m -> P n m. intros. .. coqtop:: all @@ -2572,11 +2549,10 @@ and an explanation of the underlying technique. Abort. Goal forall n m (H:Le (S n) m), Q (S n) m H. - intros. .. coqtop:: out - Show. + intros. As :g:`H` occurs in the goal, we may want to reason by cases on its structure and so, we would like inversion tactics to substitute :g:`H` by @@ -3345,7 +3321,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. example:: - .. coqtop:: all + .. coqtop:: all abort Goal ~0=0. unfold not. @@ -3353,10 +3329,6 @@ the conversion in hypotheses :n:`{+ @ident}`. pattern (0 = 0). fold not. - .. coqtop:: none - - Abort. - .. tacv:: fold {+ @term} Equivalent to :n:`fold @term ; ... ; fold @term`. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 0dd9b3aa3e..8df0f2be97 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -30,7 +30,7 @@ from sphinx import addnodes from sphinx.roles import XRefRole from sphinx.errors import ExtensionError from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode -from sphinx.util.logging import getLogger +from sphinx.util.logging import getLogger, get_node_location from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index from sphinx.domains.std import token_xrefs @@ -38,7 +38,7 @@ from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors -from .repl.coqtop import CoqTop +from .repl.coqtop import CoqTop, CoqTopError from .notations.sphinx import sphinxify from .notations.plain import stringify_with_ellipses @@ -560,17 +560,17 @@ class CoqtopDirective(Directive): Example:: - .. coqtop:: in undo + .. coqtop:: in reset Print nat. Definition a := 1. The blank line after the directive is required. If you begin a proof, - include an ``Abort`` afterwards to reset coqtop for the next example. + use the ``abort`` option to reset coqtop for the next example. Here is a list of permissible options: - - Display options + - Display options (choose exactly one) - ``all``: Display input and output - ``in``: Display only input @@ -580,15 +580,17 @@ class CoqtopDirective(Directive): - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``undo``: Reset state after executing. Not compatible with ``reset``. + - ``fail``: Don't die if a command fails + - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode) + - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any) ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per reST source file). Use the ``reset`` option to reset Coq's state. """ has_content = True - required_arguments = 0 - optional_arguments = 1 + required_arguments = 1 + optional_arguments = 0 final_argument_whitespace = True option_spec = { 'name': directives.unchanged } directive_name = "coqtop" @@ -597,10 +599,8 @@ class CoqtopDirective(Directive): # Uses a ‘container’ instead of a ‘literal_block’ to disable # Pygments-based post-processing (we could also set rawsource to '') content = '\n'.join(self.content) - args = self.arguments[0].split() if self.arguments else ['in'] - if 'all' in args: - args.extend(['in', 'out']) - node = nodes.container(content, coqtop_options = list(set(args)), + args = self.arguments[0].split() + node = nodes.container(content, coqtop_options = set(args), classes=['coqtop', 'literal-block']) self.add_name(node) return [node] @@ -827,22 +827,41 @@ class CoqtopBlocksTransform(Transform): return re.split(r"(?<=(?<!\.)\.)\s+", source) @staticmethod - def parse_options(options): + def parse_options(node): """Parse options according to the description in CoqtopDirective.""" - opt_undo = 'undo' in options + + options = node['coqtop_options'] + + # Behavior options opt_reset = 'reset' in options - opt_all, opt_none = 'all' in options, 'none' in options - opt_input, opt_output = opt_all or 'in' in options, opt_all or 'out' in options + opt_fail = 'fail' in options + opt_restart = 'restart' in options + opt_abort = 'abort' in options + options = options - set(('reset', 'fail', 'restart', 'abort')) - unexpected_options = list(set(options) - set(('reset', 'undo', 'all', 'none', 'in', 'out'))) + unexpected_options = list(options - set(('all', 'none', 'in', 'out'))) if unexpected_options: - raise ValueError("Unexpected options for .. coqtop:: {}".format(unexpected_options)) - elif (opt_input or opt_output) and opt_none: - raise ValueError("Inconsistent options for .. coqtop:: ‘none’ with ‘in’, ‘out’, or ‘all’") - elif opt_reset and opt_undo: - raise ValueError("Inconsistent options for .. coqtop:: ‘undo’ with ‘reset’") - - return opt_undo, opt_reset, opt_input and not opt_none, opt_output and not opt_none + loc = get_node_location(node) + raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options)) + + # Display options + if len(options) != 1: + loc = get_node_location(node) + raise ExtensionError("{}: Exactly one display option must be passed to .. coqtop::".format(loc)) + + opt_all = 'all' in options + opt_none = 'none' in options + opt_input = 'in' in options + opt_output = 'out' in options + + return { + 'reset': opt_reset, + 'fail': opt_fail, + 'restart': opt_restart, + 'abort': opt_abort, + 'input': opt_input or opt_all, + 'output': opt_output or opt_all + } @staticmethod def block_classes(should_show, contents=None): @@ -866,36 +885,59 @@ class CoqtopBlocksTransform(Transform): blocks.append(re.sub("^", " ", output, flags=re.MULTILINE) + "\n") return '\n'.join(blocks) + def add_coq_output_1(self, repl, node): + options = self.parse_options(node) + + pairs = [] + + if options['restart']: + repl.sendone("Restart.") + if options['reset']: + repl.sendone("Reset Initial.") + repl.sendone("Set Coqtop Exit On Error.") + if options['fail']: + repl.sendone("Unset Coqtop Exit On Error.") + for sentence in self.split_sentences(node.rawsource): + pairs.append((sentence, repl.sendone(sentence))) + if options['abort']: + repl.sendone("Abort All.") + if options['fail']: + repl.sendone("Set Coqtop Exit On Error.") + + dli = nodes.definition_list_item() + for sentence, output in pairs: + # Use Coqdoc to highlight input + in_chunks = highlight_using_coqdoc(sentence) + dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input'])) + # Parse ANSI sequences to highlight output + out_chunks = AnsiColorsParser().colorize_str(output) + dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output)) + node.clear() + node.rawsource = self.make_rawsource(pairs, options['input'], options['output']) + node['classes'].extend(self.block_classes(options['input'] or options['output'])) + node += nodes.inline('', '', classes=['coqtop-reset'] * options['reset']) + node += nodes.definition_list(node.rawsource, dli) + def add_coqtop_output(self): """Add coqtop's responses to a Sphinx AST Finds nodes to process using is_coqtop_block.""" with CoqTop(color=True) as repl: + repl.sendone("Set Coqtop Exit On Error.") for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): - options = node['coqtop_options'] - opt_undo, opt_reset, opt_input, opt_output = self.parse_options(options) - - if opt_reset: - repl.sendone("Reset Initial.") - pairs = [] - for sentence in self.split_sentences(node.rawsource): - pairs.append((sentence, repl.sendone(sentence))) - if opt_undo: - repl.sendone("Undo {}.".format(len(pairs))) - - dli = nodes.definition_list_item() - for sentence, output in pairs: - # Use Coqdoq to highlight input - in_chunks = highlight_using_coqdoc(sentence) - dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input)) - # Parse ANSI sequences to highlight output - out_chunks = AnsiColorsParser().colorize_str(output) - dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output)) - node.clear() - node.rawsource = self.make_rawsource(pairs, opt_input, opt_output) - node['classes'].extend(self.block_classes(opt_input or opt_output)) - node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset) - node += nodes.definition_list(node.rawsource, dli) + try: + self.add_coq_output_1(repl, node) + except CoqTopError as err: + import textwrap + MSG = ("{}: Error while sending the following to coqtop:\n{}" + + "\n coqtop output:\n{}" + + "\n Full error text:\n{}") + indent = " " + loc = get_node_location(node) + le = textwrap.indent(str(err.last_sentence), indent) + bef = textwrap.indent(str(err.before), indent) + fe = textwrap.indent(str(err.err), indent) + raise ExtensionError(MSG.format(loc, le, bef, fe)) @staticmethod def merge_coqtop_classes(kept_node, discarded_node): diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py index e56882a521..0c15d7334c 100755 --- a/doc/tools/coqrst/regen_readme.py +++ b/doc/tools/coqrst/regen_readme.py @@ -10,6 +10,17 @@ SCRIPT_DIR = path.dirname(path.abspath(__file__)) if __name__ == "__main__" and __package__ is None: sys.path.append(path.dirname(SCRIPT_DIR)) +SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/") +README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst") + +if len(sys.argv) == 1: + README_PATH = path.join(SPHINX_DIR, "README.rst") +elif len(sys.argv) == 2: + README_PATH = sys.argv[1] +else: + print ("usage: {} [FILE]".format(sys.argv[0])) + sys.exit(1) + import sphinx from coqrst import coqdomain @@ -23,10 +34,6 @@ def format_docstring(template, obj, *strs): strs = strs + (FIRST_LINE_BLANKS.sub(r"\1\n", docstring),) return template.format(*strs) -SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/") -README_PATH = path.join(SPHINX_DIR, "README.rst") -README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst") - def notation_symbol(d): return " :black_nib:" if issubclass(d, coqdomain.NotationObject) else "" diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 3ff00eaaf3..ddba2edd4a 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -20,6 +20,14 @@ import re import pexpect + +class CoqTopError(Exception): + def __init__(self, err, last_sentence, before): + super().__init__() + self.err = err + self.before = before + self.last_sentence = last_sentence + class CoqTop: """Create an instance of coqtop. @@ -41,13 +49,10 @@ class CoqTop: the ansicolors module) :param args: Additional arugments to coqtop. """ - BOOT = True - if os.getenv('COQBOOT') == "no": - BOOT = False self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") if not pexpect.utils.which(self.coqtop_bin): raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin)) - self.args = (args or []) + ["-boot"] * BOOT + ["-color", "on"] * color + self.args = (args or []) + ["-color", "on"] * color self.coqtop = None def __enter__(self): @@ -63,7 +68,7 @@ class CoqTop: self.coqtop.kill(9) def next_prompt(self): - "Wait for the next coqtop prompt, and return the output preceeding it." + """Wait for the next coqtop prompt, and return the output preceeding it.""" self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10) return self.coqtop.before @@ -75,13 +80,11 @@ class CoqTop: """ # Suppress newlines, but not spaces: they are significant in notations sentence = re.sub(r"[\r\n]+", " ", sentence).strip() - self.coqtop.sendline(sentence) try: + self.coqtop.sendline(sentence) output = self.next_prompt() - except: - print("Error while sending the following sentence to coqtop: {}".format(sentence)) - raise - # print("Got {}".format(repr(output))) + except Exception as err: + raise CoqTopError(err, sentence, self.coqtop.before) return output def sendmany(*sentences): diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 8493119ee5..8756ebfdf2 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -405,25 +405,17 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = let open UnivProblem in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - cstrs - | Declarations.Polymorphic_ind _ -> - enforce_eq_instances_univs false u1 u2 cstrs - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> enforce_eq_instances_univs false u1 u2 cstrs + | Some variances -> let num_param_arity = Reduction.inductive_cumulativity_arguments spec in - let variances = Univ.ACumulativityInfo.variance cumi in compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = let open UnivProblem in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - cstrs - | Declarations.Polymorphic_ind _ -> - enforce_eq_instances_univs false u1 u2 cstrs - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> enforce_eq_instances_univs false u1 u2 cstrs + | Some _ -> let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in if not (Int.equal num_cnstr_args nargs) then enforce_eq_instances_univs false u1 u2 cstrs diff --git a/engine/evd.ml b/engine/evd.ml index eee2cb700c..f0433d3387 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -852,8 +852,9 @@ let universe_context_set d = UState.context_set d.universes let to_universe_context evd = UState.context evd.universes -let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes -let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes +let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes + +let const_univ_entry = univ_entry let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl diff --git a/engine/evd.mli b/engine/evd.mli index de73144895..d2d18ca486 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -597,12 +597,12 @@ val universes : evar_map -> UGraph.t [Univ.ContextSet.to_context]. *) val to_universe_context : evar_map -> Univ.UContext.t -val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry +val univ_entry : poly:bool -> evar_map -> Entries.universes_entry -(** NB: [ind_univ_entry] cannot create cumulative entries. *) -val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes +val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry +[@@ocaml.deprecated "Use [univ_entry]."] -val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry +val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 430a3a2fd9..77d1896683 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -100,24 +100,16 @@ let constraints ctx = snd ctx.uctx_local let context ctx = ContextSet.to_context ctx.uctx_local -let const_univ_entry ~poly uctx = +let univ_entry ~poly uctx = let open Entries in if poly then let (binders, _) = uctx.uctx_names in let uctx = context uctx in let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in - Polymorphic_const_entry (nas, uctx) - else Monomorphic_const_entry (context_set uctx) + Polymorphic_entry (nas, uctx) + else Monomorphic_entry (context_set uctx) -(* does not support cumulativity since you need more info *) -let ind_univ_entry ~poly uctx = - let open Entries in - if poly then - let (binders, _) = uctx.uctx_names in - let uctx = context uctx in - let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in - Polymorphic_ind_entry (nas, uctx) - else Monomorphic_ind_entry (context_set uctx) +let const_univ_entry = univ_entry let of_context_set ctx = { empty with uctx_local = ctx } @@ -422,10 +414,10 @@ let check_univ_decl ~poly uctx decl = let (binders, _) = uctx.uctx_names in let uctx = universe_context ~names ~extensible uctx in let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in - Entries.Polymorphic_const_entry (nas, uctx) + Entries.Polymorphic_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in - Entries.Monomorphic_const_entry uctx.uctx_local + Entries.Monomorphic_entry uctx.uctx_local in if not decl.univdecl_extensible_constraints then check_implication uctx @@ -458,8 +450,8 @@ let restrict ctx vars = let demote_seff_univs entry uctx = let open Entries in match entry.const_entry_universes with - | Polymorphic_const_entry _ -> uctx - | Monomorphic_const_entry (univs, _) -> + | Polymorphic_entry _ -> uctx + | Monomorphic_entry (univs, _) -> let seff = LSet.union uctx.uctx_seff_univs univs in { uctx with uctx_seff_univs = seff } diff --git a/engine/uState.mli b/engine/uState.mli index 5170184ef4..a358813825 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -64,12 +64,11 @@ val constraints : t -> Univ.Constraint.t val context : t -> Univ.UContext.t (** Shorthand for {!context_set} with {!Context_set.to_context}. *) -val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry +val univ_entry : poly:bool -> t -> Entries.universes_entry (** Pick from {!context} or {!context_set} based on [poly]. *) -val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes -(** Pick from {!context} or {!context_set} based on [poly]. - Cannot create cumulative entries. *) +val const_univ_entry : poly:bool -> t -> Entries.universes_entry +[@@ocaml.deprecated "Use [univ_entry]."] (** {5 Constraints handling} *) @@ -177,7 +176,7 @@ val default_univ_decl : universe_decl When polymorphic, the universes corresponding to [decl.univdecl_instance] come first in the order defined by that list. *) -val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry +val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index e313f2e648..f46ddffd6e 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -1368,6 +1368,9 @@ let parse_parsable entry p = let get_loc () = try let cnt = Stream.count ts in + (* Ensure that the token at location cnt has been peeked so that + the location function knows about it *) + let _ = Stream.peek ts in let loc = fun_loc cnt in if !token_count - 1 <= cnt then loc else Loc.merge loc (fun_loc (!token_count - 1)) diff --git a/interp/declare.ml b/interp/declare.ml index ea6ed8321d..4371b15c82 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -143,7 +143,7 @@ let declare_constant_common id cst = update_tables c; c -let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty +let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); @@ -156,8 +156,8 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = let is_poly de = match de.const_entry_universes with - | Monomorphic_const_entry _ -> false - | Polymorphic_const_entry _ -> true + | Monomorphic_entry _ -> false + | Polymorphic_entry _ -> true in let in_section = Lib.sections_are_opened () in let export, decl = (* We deal with side effects *) @@ -217,8 +217,8 @@ let cache_variable ((sp,_),o) = section-local definition, but it's not enforced by typing *) let (body, uctx), () = Future.force de.const_entry_body in let poly, univs = match de.const_entry_universes with - | Monomorphic_const_entry uctx -> false, uctx - | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx + | Monomorphic_entry uctx -> false, uctx + | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in (* We must declare the universe constraints before type-checking the @@ -328,21 +328,15 @@ let dummy_inductive_entry m = { mind_entry_record = None; mind_entry_finite = Declarations.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; + mind_entry_universes = default_univ_entry; + mind_entry_variance = None; mind_entry_private = None; } (* reinfer subtyping constraints for inductive after section is dischared. *) -let infer_inductive_subtyping mind_ent = - match mind_ent.mind_entry_universes with - | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> - mind_ent - | Cumulative_ind_entry (_, cumi) -> - begin - let env = Global.env () in - (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) - InferCumulativity.infer_inductive env mind_ent - end +let rebuild_inductive mind_ent = + let env = Global.env () in + InferCumulativity.infer_inductive env mind_ent let inInductive : mutual_inductive_entry -> obj = declare_object {(default_object "INDUCTIVE") with @@ -352,25 +346,19 @@ let inInductive : mutual_inductive_entry -> obj = classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; discharge_function = discharge_inductive; - rebuild_function = infer_inductive_subtyping } + rebuild_function = rebuild_inductive } let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = let id = Label.to_id label in - let univs = match univs with - | Monomorphic_ind_entry _ -> + let univs, u = match univs with + | Monomorphic_entry _ -> (* Global constraints already defined through the inductive *) - Monomorphic_const_entry Univ.ContextSet.empty - | Polymorphic_ind_entry (nas, ctx) -> - Polymorphic_const_entry (nas, ctx) - | Cumulative_ind_entry (nas, ctx) -> - Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx) - in - let term, types = match univs with - | Monomorphic_const_entry _ -> term, types - | Polymorphic_const_entry (_, ctx) -> - let u = Univ.UContext.instance ctx in - Vars.subst_instance_constr u term, Vars.subst_instance_constr u types + default_univ_entry, Univ.Instance.empty + | Polymorphic_entry (nas, ctx) -> + Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx in + let term = Vars.subst_instance_constr u term in + let types = Vars.subst_instance_constr u types in let entry = definition_entry ~types ~univs term in let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in @@ -442,9 +430,6 @@ let assumption_message id = discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") -let register_message id = - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is registered") - (** Monomorphic universes need to survive sections. *) let input_universe_context : Univ.ContextSet.t -> Libobject.obj = diff --git a/interp/declare.mli b/interp/declare.mli index 669657af6f..8f1e73c88c 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -43,7 +43,7 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> - ?univs:Entries.constant_universes_entry -> + ?univs:Entries.universes_entry -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry (** [declare_constant id cd] declares a global declaration @@ -58,7 +58,7 @@ val declare_constant : val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> Id.t -> ?types:constr -> - constr Entries.in_constant_universes_entry -> Constant.t + constr Entries.in_universes_entry -> Constant.t (** Since transparent constants' side effects are globally declared, we * need that *) @@ -74,7 +74,6 @@ val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool val definition_message : Id.t -> unit val assumption_message : Id.t -> unit -val register_message : Id.t -> unit val fixpoint_message : int array option -> Id.t list -> unit val cofixpoint_message : Id.t list -> unit val recursive_message : bool (** true = fixpoint *) -> diff --git a/interp/discharge.ml b/interp/discharge.ml index eeda5a6867..353b0f6057 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -76,18 +76,16 @@ let process_inductive info modlist mib = let nparamdecls = Context.Rel.length mib.mind_params_ctxt in let subst, ind_univs = match mib.mind_universes with - | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx - | Polymorphic_ind auctx -> + | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx + | Polymorphic auctx -> let subst, auctx = Lib.discharge_abstract_universe_context info auctx in let nas = Univ.AUContext.names auctx in let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_ind_entry (nas, auctx) - | Cumulative_ind cumi -> - let auctx = Univ.ACumulativityInfo.univ_context cumi in - let subst, auctx = Lib.discharge_abstract_universe_context info auctx in - let nas = Univ.AUContext.names auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx) + subst, Polymorphic_entry (nas, auctx) + in + let variance = match mib.mind_variance with + | None -> None + | Some _ -> Some (InferCumulativity.dummy_variance ind_univs) in let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in let inds = @@ -114,6 +112,7 @@ let process_inductive info modlist mib = mind_entry_params = params'; mind_entry_inds = inds'; mind_entry_private = mib.mind_private; + mind_entry_variance = variance; mind_entry_universes = ind_univs } diff --git a/interp/impargs.ml b/interp/impargs.ml index 959455dfd2..6fd52d98dd 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -120,12 +120,7 @@ let argument_position_eq p1 p2 = match p1, p2 with | Hyp h1, Hyp h2 -> Int.equal h1 h2 | _ -> false -let explicitation_eq ex1 ex2 = match ex1, ex2 with -| ExplByPos (i1, id1), ExplByPos (i2, id2) -> - Int.equal i1 i2 && Option.equal Id.equal id1 id2 -| ExplByName id1, ExplByName id2 -> - Id.equal id1 id2 -| _ -> false +let explicitation_eq = Constrexpr_ops.explicitation_eq type implicit_explanation = | DepRigid of argument_position @@ -200,7 +195,7 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc | App (f,_) when rig && is_flexible_reference env sigma bound depth f -> if strict then () else iter_with_full_binders sigma push_lift (frec false) ed c - | Proj (p,c) when rig -> + | Proj (p, _) when rig -> if strict then () else iter_with_full_binders sigma push_lift (frec false) ed c | Case _ when rig -> @@ -380,7 +375,7 @@ let flatten_explicitations l autoimps = | (Name id,_)::imps -> let value, l' = try - let eq = explicitation_eq in + let eq = Constrexpr_ops.explicitation_eq in let flags = List.assoc_f eq (ExplByName id) l in Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l with Not_found -> assoc_by_pos k l diff --git a/interp/impargs.mli b/interp/impargs.mli index 4afc2af5e9..43c26b024f 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -138,4 +138,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool + [@@ocaml.deprecated "Use Constrexpr_ops.explicitation_eq instead (since 8.10)"] (** Equality on [explicitation]. *) diff --git a/interp/modintern.ml b/interp/modintern.ml index 60056dfd90..2f516f4f3c 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -107,12 +107,12 @@ let transl_with_decl env base kind = function let c, ectx = interp_constr env sigma c in let poly = lookup_polymorphism env base kind fqid in begin match UState.check_univ_decl ~poly ectx udecl with - | Entries.Polymorphic_const_entry (nas, ctx) -> + | Entries.Polymorphic_entry (nas, ctx) -> let inst, ctx = Univ.abstract_universes nas ctx in let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let c = EConstr.to_constr sigma c in WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty - | Entries.Monomorphic_const_entry ctx -> + | Entries.Monomorphic_entry ctx -> let c = EConstr.to_constr sigma c in WithDef (fqid,(c, None)), ctx end diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 890c24e633..7d7e10a05b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -908,11 +908,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) (* TODO: look at the consequences for alp *) alp, add_env alp sigma var (DAst.make @@ GVar id) -let force_cases_pattern c = - DAst.make ?loc:c.CAst.loc (DAst.get c) - let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in + let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let patl' = Id.List.assoc var binders in diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index b95a940c14..718584b3d4 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -881,11 +881,7 @@ let compile_constant_body ~fail_on_error env univs = function | Undef _ | OpaqueDef _ | Primitive _ -> Some BCconstant | Def sb -> let body = Mod_subst.force_constr sb in - let instance_size = - match univs with - | Monomorphic_const _ -> 0 - | Polymorphic_const univ -> Univ.AUContext.size univ - in + let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in match kind body with | Const (kn',u) when is_univ_copy instance_size u -> (* we use the canonical name of the constant*) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index b1b55aef48..6a9550342c 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -20,7 +20,7 @@ val compile : fail_on_error:bool -> (** init, fun, fv *) val compile_constant_body : fail_on_error:bool -> - env -> constant_universes -> Constr.t Mod_subst.substituted constant_def -> + env -> universes -> Constr.t Mod_subst.substituted constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 88586352f6..22de9bfad5 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -157,7 +157,7 @@ type inline = bool type result = { cook_body : constr Mod_subst.substituted constant_def; cook_type : types; - cook_universes : constant_universes; + cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; @@ -185,10 +185,10 @@ let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = let lift_univs cb subst auctx0 = match cb.const_universes with - | Monomorphic_const ctx -> + | Monomorphic ctx -> assert (AUContext.is_empty auctx0); - subst, (Monomorphic_const ctx) - | Polymorphic_const auctx -> + subst, (Monomorphic ctx) + | Polymorphic auctx -> (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, and another abstract context relative to the former context @@ -202,13 +202,13 @@ let lift_univs cb subst auctx0 = *) if (Univ.Instance.is_empty subst) then (** Still need to take the union for the constraints between globals *) - subst, (Polymorphic_const (AUContext.union auctx0 auctx)) + subst, (Polymorphic (AUContext.union auctx0 auctx)) else let ainst = Univ.make_abstract_instance auctx in let subst = Instance.append subst ainst in let substf = Univ.make_instance_subst subst in let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in - subst, (Polymorphic_const (AUContext.union auctx0 auctx')) + subst, (Polymorphic (AUContext.union auctx0 auctx')) let cook_constant ~hcons { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 07c6f37fab..89b5c60ad5 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -20,7 +20,7 @@ type inline = bool type result = { cook_body : constr Mod_subst.substituted constant_def; cook_type : types; - cook_universes : constant_universes; + cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1008492825..6777e0c223 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -53,9 +53,9 @@ type 'a constant_def = | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) | Primitive of CPrimitives.t (** or a primitive operation *) -type constant_universes = - | Monomorphic_const of Univ.ContextSet.t - | Polymorphic_const of Univ.AUContext.t +type universes = + | Monomorphic of Univ.ContextSet.t + | Polymorphic of Univ.AUContext.t (** The [typing_flags] are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking @@ -92,7 +92,7 @@ type constant_body = { const_body : Constr.t Mod_subst.substituted constant_def; const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; - const_universes : constant_universes; + const_universes : universes; const_private_poly_univs : Univ.ContextSet.t option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which @@ -185,11 +185,6 @@ type one_inductive_body = { mind_reloc_tbl : Vmvalues.reloc_table; } -type abstract_inductive_universes = - | Monomorphic_ind of Univ.ContextSet.t - | Polymorphic_ind of Univ.AUContext.t - | Cumulative_ind of Univ.ACumulativityInfo.t - type recursivity_kind = | Finite (** = inductive *) | CoFinite (** = coinductive *) @@ -213,7 +208,9 @@ type mutual_inductive_body = { mind_params_ctxt : Constr.rel_context; (** The context of parameters (includes let-in declaration) *) - mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + + mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 5686c4071d..9e0230c3ba 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -49,12 +49,24 @@ let hcons_template_arity ar = (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) template_level = Univ.hcons_univ ar.template_level } +let universes_context = function + | Monomorphic _ -> Univ.AUContext.empty + | Polymorphic ctx -> ctx + +let abstract_universes = function + | Entries.Monomorphic_entry ctx -> + Univ.empty_level_subst, Monomorphic ctx + | Entries.Polymorphic_entry (nas, ctx) -> + let (inst, auctx) = Univ.abstract_universes nas ctx in + let inst = Univ.make_instance_subst inst in + (inst, Polymorphic auctx) + (** {6 Constants } *) let constant_is_polymorphic cb = match cb.const_universes with - | Monomorphic_const _ -> false - | Polymorphic_const _ -> true + | Monomorphic _ -> false + | Polymorphic _ -> true let constant_has_body cb = match cb.const_body with @@ -62,9 +74,7 @@ let constant_has_body cb = match cb.const_body with | Def _ | OpaqueDef _ -> true let constant_polymorphic_context cb = - match cb.const_universes with - | Monomorphic_const _ -> Univ.AUContext.empty - | Polymorphic_const ctx -> ctx + universes_context cb.const_universes let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true @@ -126,12 +136,12 @@ let hcons_const_def = function Def (from_val (Constr.hcons constr)) | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) -let hcons_const_universes cbu = +let hcons_universes cbu = match cbu with - | Monomorphic_const ctx -> - Monomorphic_const (Univ.hcons_universe_context_set ctx) - | Polymorphic_const ctx -> - Polymorphic_const (Univ.hcons_abstract_universe_context ctx) + | Monomorphic ctx -> + Monomorphic (Univ.hcons_universe_context_set ctx) + | Polymorphic ctx -> + Polymorphic (Univ.hcons_abstract_universe_context ctx) let hcons_const_private_univs = function | None -> None @@ -141,7 +151,7 @@ let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = Constr.hcons cb.const_type; - const_universes = hcons_const_universes cb.const_universes; + const_universes = hcons_universes cb.const_universes; const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs; } @@ -239,27 +249,21 @@ let subst_mind_body sub mib = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; + mind_variance = mib.mind_variance; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } let inductive_polymorphic_context mib = - match mib.mind_universes with - | Monomorphic_ind _ -> Univ.AUContext.empty - | Polymorphic_ind ctx -> ctx - | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi + universes_context mib.mind_universes let inductive_is_polymorphic mib = match mib.mind_universes with - | Monomorphic_ind _ -> false - | Polymorphic_ind _ctx -> true - | Cumulative_ind _cumi -> true + | Monomorphic _ -> false + | Polymorphic _ctx -> true let inductive_is_cumulative mib = - match mib.mind_universes with - | Monomorphic_ind _ -> false - | Polymorphic_ind _ctx -> false - | Cumulative_ind _cumi -> true + Option.has_some mib.mind_variance let inductive_make_projection ind mib ~proj_arg = match mib.mind_record with @@ -306,17 +310,11 @@ let hcons_mind_packet oib = mind_user_lc = user; mind_nf_lc = nf } -let hcons_mind_universes miu = - match miu with - | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx) - | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx) - | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui) - let hcons_mind mib = { mib with mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; - mind_universes = hcons_mind_universes mib.mind_universes } + mind_universes = hcons_universes mib.mind_universes } (** Hashconsing of modules *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 35490ceef9..23a44433b3 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -15,6 +15,10 @@ open Univ (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) +val universes_context : universes -> AUContext.t + +val abstract_universes : Entries.universes_entry -> Univ.universe_level_subst * universes + (** {6 Arities} *) val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> diff --git a/kernel/entries.ml b/kernel/entries.ml index 013327599d..a3d32267a7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -16,6 +16,12 @@ open Constr constants/axioms, mutual inductive definitions, modules and module types *) +type universes_entry = + | Monomorphic_entry of Univ.ContextSet.t + | Polymorphic_entry of Name.t array * Univ.UContext.t + +type 'a in_universes_entry = 'a * universes_entry + (** {6 Declaration of inductive types. } *) (** Assume the following definition in concrete syntax: @@ -28,11 +34,6 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; [mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]]. *) -type inductive_universes = - | Monomorphic_ind_entry of Univ.ContextSet.t - | Polymorphic_ind_entry of Name.t array * Univ.UContext.t - | Cumulative_ind_entry of Name.t array * Univ.CumulativityInfo.t - type one_inductive_entry = { mind_entry_typename : Id.t; mind_entry_arity : constr; @@ -48,7 +49,8 @@ type mutual_inductive_entry = { mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : Constr.rel_context; mind_entry_inds : one_inductive_entry list; - mind_entry_universes : inductive_universes; + mind_entry_universes : universes_entry; + mind_entry_variance : Univ.Variance.t array option; (* universe constraints and the constraints for subtyping of inductive types in the block. *) mind_entry_private : bool option; @@ -58,12 +60,6 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation -type constant_universes_entry = - | Monomorphic_const_entry of Univ.ContextSet.t - | Polymorphic_const_entry of Name.t array * Univ.UContext.t - -type 'a in_constant_universes_entry = 'a * constant_universes_entry - type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -71,7 +67,7 @@ type 'a definition_entry = { (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; - const_entry_universes : constant_universes_entry; + const_entry_universes : universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } @@ -85,7 +81,7 @@ type section_def_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Constr.named_context option * types in_constant_universes_entry * inline + Constr.named_context option * types in_universes_entry * inline type primitive_entry = { prim_entry_type : types option; diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 6976b2019d..a5dafc5ab5 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -87,23 +87,28 @@ let check_subtyping_arity_constructor env subst arcn numparams is_arity = let last_env = Context.Rel.fold_outside check_typ typs ~init:env in if not is_arity then basic_check last_env codom else () -let check_cumulativity univs env_ar params data = +let check_cumulativity univs variances env_ar params data = + let uctx = match univs with + | Monomorphic_entry _ -> raise (InductiveError BadUnivs) + | Polymorphic_entry (_,uctx) -> uctx + in + let instance = UContext.instance uctx in + if Instance.length instance != Array.length variances then raise (InductiveError BadUnivs); let numparams = Context.Rel.nhyps params in - let uctx = CumulativityInfo.univ_context univs in - let new_levels = Array.init (UContext.size uctx) + let new_levels = Array.init (Instance.length instance) (fun i -> Level.(make (UGlobal.make DirPath.empty i))) in let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) - LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels + LMap.empty (Instance.to_array instance) new_levels in let dosubst = Vars.subst_univs_level_constr lmap in let instance_other = Instance.of_array new_levels in - let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in + let constraints_other = Univ.subst_univs_level_constraints lmap (UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in let env = Environ.push_context uctx_other env_ar in let subtyp_constraints = - CumulativityInfo.leq_constraints univs - (UContext.instance uctx) instance_other + Univ.enforce_leq_variance_instances variances + instance instance_other Constraint.empty in let env = Environ.add_constraints subtyp_constraints env in @@ -236,8 +241,8 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ} | Some min_univ -> ((match univs with - | Monomorphic_ind _ -> () - | Polymorphic_ind _ | Cumulative_ind _ -> + | Monomorphic _ -> () + | Polymorphic _ -> CErrors.anomaly ~label:"polymorphic_template_ind" Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.")); TemplateArity {template_param_levels=param_ccls params; template_level=min_univ}) @@ -246,17 +251,6 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i let kelim = allowed_sorts univ_info in (arity,lc), (indices,splayed_lc), kelim -let abstract_inductive_universes = function - | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) - | Polymorphic_ind_entry (nas, ctx) -> - let (inst, auctx) = Univ.abstract_universes nas ctx in - let inst = Univ.make_instance_subst inst in - (inst, Polymorphic_ind auctx) - | Cumulative_ind_entry (nas, cumi) -> - let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in - let inst = Univ.make_instance_subst inst in - (inst, Cumulative_ind acumi) - let typecheck_inductive env (mie:mutual_inductive_entry) = let () = match mie.mind_entry_inds with | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.") @@ -269,9 +263,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = (* universes *) let env_univs = match mie.mind_entry_universes with - | Monomorphic_ind_entry ctx -> push_context_set ctx env - | Polymorphic_ind_entry (_, ctx) -> push_context ctx env - | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env + | Monomorphic_entry ctx -> push_context_set ctx env + | Polymorphic_entry (_, ctx) -> push_context ctx env in (* Params *) @@ -287,13 +280,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = mie.mind_entry_inds data in - let () = match mie.mind_entry_universes with - | Cumulative_ind_entry (_,univs) -> check_cumulativity univs env_ar params (List.map pi1 data) - | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> () + let () = match mie.mind_entry_variance with + | None -> () + | Some variances -> + check_cumulativity mie.mind_entry_universes variances env_ar params (List.map pi1 data) in (* Abstract universes *) - let usubst, univs = abstract_inductive_universes mie.mind_entry_universes in + let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in let data = List.map (abstract_packets univs usubst params) data in @@ -304,4 +298,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = Environ.push_rel_context ctx env in - env_ar_par, univs, params, Array.of_list data + env_ar_par, univs, mie.mind_entry_variance, params, Array.of_list data diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 8841e38636..2598548f3f 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -16,6 +16,7 @@ open Declarations Returns: - environment with inductives + parameters in rel context - abstracted universes + - checked variance info - parameters - for each inductive, (arity * constructors) (with params) @@ -24,7 +25,7 @@ open Declarations *) val typecheck_inductive : env -> mutual_inductive_entry -> env - * abstract_inductive_universes + * universes * Univ.Variance.t array option * Constr.rel_context * ((inductive_arity * Constr.types array) * (Constr.rel_context * (Constr.rel_context * Constr.types) array) * diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 674d7a2a91..8f06e1e4b8 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -414,11 +414,7 @@ exception UndefinableExpansion a substitution of the form [params, x : ind params] *) let compute_projections (kn, i as ind) mib = let pkt = mib.mind_packets.(i) in - let u = match mib.mind_universes with - | Monomorphic_ind _ -> Univ.Instance.empty - | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx - | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi) - in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in @@ -471,7 +467,7 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev labs), Array.of_list (List.rev pbs) -let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in @@ -529,6 +525,7 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr mind_params_ctxt = paramsctxt; mind_packets = packets; mind_universes = univs; + mind_variance = variance; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -563,7 +560,7 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr let check_inductive env kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in + let (env_ar_par, univs, variance, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in (* Then check positivity conditions *) let chkpos = (Environ.typing_flags env).check_guarded in let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) @@ -574,6 +571,6 @@ let check_inductive env kn mie = (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) in (* Build the inductive packets *) - build_inductive env names mie.mind_entry_private univs + build_inductive env names mie.mind_entry_private univs variance paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/inductive.ml b/kernel/inductive.ml index c62d0e7ded..848ae65c51 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -56,12 +56,7 @@ let inductive_paramdecls (mib,u) = Vars.subst_instance_context u mib.mind_params_ctxt let instantiate_inductive_constraints mib u = - let process auctx = Univ.AUContext.instantiate u auctx in - match mib.mind_universes with - | Monomorphic_ind _ -> Univ.Constraint.empty - | Polymorphic_ind auctx -> process auctx - | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) - + Univ.AUContext.instantiate u (Declareops.inductive_polymorphic_context mib) (************************************************************************) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index f68dd158c2..421d932d9a 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -76,7 +76,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = as long as they have the right type *) let c', univs, ctx' = match cb.const_universes, ctx with - | Monomorphic_const _, None -> + | Monomorphic _, None -> let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in @@ -90,8 +90,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = | Primitive _ -> error_incorrect_with_constraint lab in - c', Monomorphic_const Univ.ContextSet.empty, cst - | Polymorphic_const uctx, Some ctx -> + c', Monomorphic Univ.ContextSet.empty, cst + | Polymorphic uctx, Some ctx -> let () = if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab @@ -114,7 +114,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = in if not (Univ.Constraint.is_empty cst) then error_incorrect_with_constraint lab; - c, Polymorphic_const ctx, Univ.Constraint.empty + c, Polymorphic ctx, Univ.Constraint.empty | _ -> error_incorrect_with_constraint lab in let def = Def (Mod_subst.from_val c') in diff --git a/kernel/modops.ml b/kernel/modops.ml index 1dc8eec0da..4f992d3972 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -50,6 +50,7 @@ type signature_mismatch_error = | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t } + | IncompatibleVariance type module_typing_error = | SignatureMismatch of @@ -325,11 +326,7 @@ let strengthen_const mp_from l cb resolver = |_ -> let kn = KerName.make mp_from l in let con = constant_of_delta_kn resolver kn in - let u = - match cb.const_universes with - | Monomorphic_const _ -> Univ.Instance.empty - | Polymorphic_const ctx -> Univ.make_abstract_instance ctx - in + let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); const_private_poly_univs = None; diff --git a/kernel/modops.mli b/kernel/modops.mli index bb97f0171e..119ce2b359 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -111,6 +111,7 @@ type signature_mismatch_error = | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t } + | IncompatibleVariance type module_typing_error = | SignatureMismatch of diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c32bdb85d6..df60899b95 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1851,11 +1851,7 @@ and compile_named env sigma univ auxdefs id = Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs let compile_constant env sigma prefix ~interactive con cb = - let no_univs = - match cb.const_universes with - | Monomorphic_const _ -> true - | Polymorphic_const ctx -> Int.equal (Univ.AUContext.size ctx) 0 - in + let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in begin match cb.const_body with | Def t -> let t = Mod_subst.force_constr t in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 61051c001d..b583d33e29 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -244,18 +244,14 @@ let inductive_cumulativity_arguments (mind,ind) = mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - s - | Declarations.Polymorphic_ind _ -> - cmp_instances u1 u2 s - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> cmp_instances u1 u2 s + | Some variances -> let num_param_arity = inductive_cumulativity_arguments (mind,ind) in if not (Int.equal num_param_arity nargs) then cmp_instances u1 u2 s else - cmp_cumul cv_pb (Univ.ACumulativityInfo.variance cumi) u1 u2 s + cmp_cumul cv_pb variances u1 u2 s let convert_inductives cv_pb ind nargs u1 u2 (s, check) = convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances @@ -266,13 +262,9 @@ let constructor_cumulativity_arguments (mind, ind, ctor) = mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1) let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - s - | Declarations.Polymorphic_ind _ -> - cmp_instances u1 u2 s - | Declarations.Cumulative_ind _cumi -> + match mind.Declarations.mind_variance with + | None -> cmp_instances u1 u2 s + | Some _ -> let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 18a257047d..dc15d9d25e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -312,8 +312,8 @@ let universes_of_private eff = | `Opaque (_, ctx) -> ctx :: acc in match eff.seff_body.const_universes with - | Monomorphic_const ctx -> ctx :: acc - | Polymorphic_const _ -> acc + | Monomorphic ctx -> ctx :: acc + | Polymorphic _ -> acc in List.fold_left fold [] (side_effects_of_private_constants eff) @@ -465,7 +465,7 @@ let labels_of_mib mib = let globalize_constant_universes env cb = match cb.const_universes with - | Monomorphic_const cstrs -> + | Monomorphic cstrs -> Now (false, cstrs) :: (match cb.const_body with | (Undef _ | Def _ | Primitive _) -> [] @@ -476,15 +476,14 @@ let globalize_constant_universes env cb = match Future.peek_val fc with | None -> [Later fc] | Some c -> [Now (false, c)]) - | Polymorphic_const _ -> + | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] let globalize_mind_universes mb = match mb.mind_universes with - | Monomorphic_ind ctx -> + | Monomorphic ctx -> [Now (false, ctx)] - | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)] - | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)] + | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] let constraints_of_sfb env sfb = match sfb with @@ -612,13 +611,13 @@ let inline_side_effects env body side_eff = | _ -> assert false in match cb.const_universes with - | Monomorphic_const univs -> + | Monomorphic univs -> (** Abstract over the term at the top of the proof *) let ty = cb.const_type in let subst = Cmap_env.add c (Inr var) subst in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const _ -> + | Polymorphic _ -> (** Inline the term to emulate universe polymorphism *) let subst = Cmap_env.add c (Inl b) subst in (subst, var, ctx, args) @@ -700,10 +699,10 @@ let constant_entry_of_side_effect cb u = let open Entries in let univs = match cb.const_universes with - | Monomorphic_const uctx -> - Monomorphic_const_entry uctx - | Polymorphic_const auctx -> - Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) + | Monomorphic uctx -> + Monomorphic_entry uctx + | Polymorphic auctx -> + Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in let pt = match cb.const_body, u with @@ -756,8 +755,8 @@ let export_side_effects mb env c = let { seff_constant = kn; seff_body = cb ; _ } = eff in let env = Environ.add_constant kn cb env in match cb.const_universes with - | Polymorphic_const _ -> env - | Monomorphic_const ctx -> + | Polymorphic _ -> env + | Monomorphic ctx -> let ctx = match eff.seff_env with | `Nothing -> ctx | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2fc3aa99b5..dea72e8b59 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -92,11 +92,25 @@ let check_conv_error error why cst poly f env a1 a2 = with NotConvertible -> error why | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e) -let check_polymorphic_instance error env auctx1 auctx2 = - if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then - error (IncompatibleConstraints { got = auctx1; expect = auctx2; } ) - else - Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env +let check_universes error env u1 u2 = + match u1, u2 with + | Monomorphic _, Monomorphic _ -> env + | Polymorphic auctx1, Polymorphic auctx2 -> + if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then + error (IncompatibleConstraints { got = auctx1; expect = auctx2; } ) + else + Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env + | Monomorphic _, Polymorphic _ -> error (PolymorphicStatusExpected true) + | Polymorphic _, Monomorphic _ -> error (PolymorphicStatusExpected false) + +let check_variance error v1 v2 = + match v1, v2 with + | None, None -> () + | Some v1, Some v2 -> + if not (Array.for_all2 Variance.check_subtype v2 v1) then + error IncompatibleVariance + | None, Some _ -> error (CumulativeStatusExpected true) + | Some _, None -> error (CumulativeStatusExpected false) (* for now we do not allow reorderings *) @@ -110,29 +124,9 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib | _ -> error (InductiveFieldExpected mib2) in - let env, inst = - match mib1.mind_universes, mib2.mind_universes with - | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty - | Polymorphic_ind auctx, Polymorphic_ind auctx' -> - let env = check_polymorphic_instance error env auctx auctx' in - env, Univ.make_abstract_instance auctx' - | Cumulative_ind cumi, Cumulative_ind cumi' -> - (** Currently there is no way to control variance of inductive types, but - just in case we require that they are in a subtyping relation. *) - let () = - let v = ACumulativityInfo.variance cumi in - let v' = ACumulativityInfo.variance cumi' in - if not (Array.for_all2 Variance.check_subtype v' v) then - CErrors.anomaly Pp.(str "Variance of " ++ KerName.print kn1 ++ - str " is not compatible with the one of " ++ KerName.print kn2) - in - let auctx = Univ.ACumulativityInfo.univ_context cumi in - let auctx' = Univ.ACumulativityInfo.univ_context cumi' in - let env = check_polymorphic_instance error env auctx auctx' in - env, Univ.make_abstract_instance auctx' - | _ -> error - (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2)) - in + let env = check_universes error env mib1.mind_universes mib2.mind_universes in + let () = check_variance error mib1.mind_variance mib2.mind_variance in + let inst = make_abstract_instance (Declareops.inductive_polymorphic_context mib1) in let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name t1 t2 = check_conv (NotConvertibleInductiveField name) @@ -235,17 +229,8 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = let cb1 = Declareops.subst_const_body subst1 cb1 in let cb2 = Declareops.subst_const_body subst2 cb2 in (* Start by checking universes *) - let poly, env = - match cb1.const_universes, cb2.const_universes with - | Monomorphic_const _, Monomorphic_const _ -> - false, env - | Polymorphic_const auctx1, Polymorphic_const auctx2 -> - true, check_polymorphic_instance error env auctx1 auctx2 - | Monomorphic_const _, Polymorphic_const _ -> - error (PolymorphicStatusExpected true) - | Polymorphic_const _, Monomorphic_const _ -> - error (PolymorphicStatusExpected false) - in + let env = check_universes error env cb1.const_universes cb2.const_universes in + let poly = Declareops.constant_is_polymorphic cb1 in (* Now check types *) let typ1 = cb1.const_type in let typ2 = cb2.const_type in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3cb5d17d34..929f1c13a3 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -65,23 +65,15 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> Feedback.feedback ~id:state_id Feedback.Complete) -let abstract_constant_universes = function - | Monomorphic_const_entry uctx -> - Univ.empty_level_subst, Monomorphic_const uctx - | Polymorphic_const_entry (nas, uctx) -> - let sbst, auctx = Univ.abstract_universes nas uctx in - let sbst = Univ.make_instance_subst sbst in - sbst, Polymorphic_const auctx - let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with - | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env - | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env + | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env + | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env in let j = infer env t in - let usubst, univs = abstract_constant_universes uctx in + let usubst, univs = Declareops.abstract_universes uctx in let c = Typeops.assumption_of_judgment env j in let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in { @@ -115,7 +107,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | CPrimitives.OT_type _ -> Undef None in { Cooking.cook_body = cd; cook_type = ty; - cook_universes = Monomorphic_const uctxt; + cook_universes = Monomorphic uctxt; cook_private_univs = None; cook_inline = false; cook_context = None @@ -134,7 +126,7 @@ the polymorphic case *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_universes = Monomorphic_const_entry univs; _ } as c) -> + const_entry_universes = Monomorphic_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in let tyj = infer_type env typ in @@ -165,7 +157,7 @@ the polymorphic case { Cooking.cook_body = def; cook_type = typ; - cook_universes = Monomorphic_const univs; + cook_universes = Monomorphic univs; cook_private_univs = None; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -183,11 +175,11 @@ the polymorphic case body, Univ.ContextSet.union ctx ctx' in let env, usubst, univs, private_univs = match c.const_entry_universes with - | Monomorphic_const_entry univs -> + | Monomorphic_entry univs -> let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic_const ctx, None - | Polymorphic_const_entry (nas, uctx) -> + env, Univ.empty_level_subst, Monomorphic ctx, None + | Polymorphic_entry (nas, uctx) -> (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in @@ -200,7 +192,7 @@ the polymorphic case if Univ.ContextSet.is_empty ctx then env, None else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") in - env, sbst, Polymorphic_const auctx, local + env, sbst, Polymorphic auctx, local in let j = infer env body in let typ = match typ with @@ -342,7 +334,7 @@ let translate_local_def env _id centry = const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; - const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty; + const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; const_entry_opaque = false; const_entry_inline_code = false; } in @@ -360,8 +352,8 @@ let translate_local_def env _id centry = record_aux env ids_typ ids_def end; let () = match decl.cook_universes with - | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx) - | Polymorphic_const _ -> assert false + | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) + | Polymorphic _ -> assert false in let c = match decl.cook_body with | Def c -> Mod_subst.force_constr c diff --git a/kernel/univ.ml b/kernel/univ.ml index 8940c0337e..09bf695915 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -989,68 +989,6 @@ let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} = let hcons_abstract_universe_context = AUContext.hcons -(** Universe info for cumulative inductive types: A context of - universe levels with universe constraints, representing local - universe variables and constraints, together with an array of - Variance.t. - - This data structure maintains the invariant that the variance - array has the same length as the universe instance. *) -module CumulativityInfo = -struct - type t = universe_context * Variance.t array - - let make x = - if (Instance.length (UContext.instance (fst x))) = - (Array.length (snd x)) then x - else anomaly (Pp.str "Invalid subtyping information encountered!") - - let empty = (UContext.empty, [||]) - let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance - - let pr prl (univs, variance) = - UContext.pr prl ~variance univs - - let hcons (univs, variance) = (* should variance be hconsed? *) - (UContext.hcons univs, variance) - - let univ_context (univs, _subtypcst) = univs - let variance (_univs, variance) = variance - - (** This function takes a universe context representing constraints - of an inductive and produces a CumulativityInfo.t with the - trivial subtyping relation. *) - let from_universe_context univs = - (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant)) - - let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts - let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts - -end - -let hcons_cumulativity_info = CumulativityInfo.hcons - -module ACumulativityInfo = -struct - type t = AUContext.t * Variance.t array - - let repr (auctx,var) = AUContext.repr auctx, var - - let pr prl (univs, variance) = - AUContext.pr prl ~variance univs - - let hcons (univs, variance) = (* should variance be hconsed? *) - (AUContext.hcons univs, variance) - - let univ_context (univs, _subtypcst) = univs - let variance (_univs, variance) = variance - - let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts - let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts -end - -let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons - (** A set of universes with universe constraints. We linearize the set to a list after typechecking. Beware, representation could change. @@ -1211,10 +1149,6 @@ let abstract_universes nas ctx = let ctx = (nas, cstrs) in instance, ctx -let abstract_cumulativity_info nas (univs, variance) = - let subst, univs = abstract_universes nas univs in - subst, (univs, variance) - let rec compact_univ s vars i u = match u with | [] -> (s, List.rev vars) @@ -1235,12 +1169,8 @@ let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr -let pr_cumulativity_info = CumulativityInfo.pr - let pr_abstract_universe_context = AUContext.pr -let pr_abstract_cumulativity_info = ACumulativityInfo.pr - let pr_universe_context_set = ContextSet.pr let pr_universe_subst = diff --git a/kernel/univ.mli b/kernel/univ.mli index b83251e983..1fbebee350 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -368,45 +368,6 @@ type 'a univ_abstracted = { val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted -(** Universe info for cumulative inductive types: A context of - universe levels with universe constraints, representing local - universe variables and constraints, together with an array of - Variance.t. - - This data structure maintains the invariant that the variance - array has the same length as the universe instance. *) -module CumulativityInfo : -sig - type t - - val make : UContext.t * Variance.t array -> t - - val empty : t - val is_empty : t -> bool - - val univ_context : t -> UContext.t - val variance : t -> Variance.t array - - (** This function takes a universe context representing constraints - of an inductive and produces a CumulativityInfo.t with the - trivial subtyping relation. *) - val from_universe_context : UContext.t -> t - - val leq_constraints : t -> Instance.t constraint_function - val eq_constraints : t -> Instance.t constraint_function -end - -module ACumulativityInfo : -sig - type t - - val repr : t -> CumulativityInfo.t - val univ_context : t -> AUContext.t - val variance : t -> Variance.t array - val leq_constraints : t -> Instance.t constraint_function - val eq_constraints : t -> Instance.t constraint_function -end - (** Universe contexts (as sets) *) (** A set of universes with universe Constraint.t. @@ -487,7 +448,6 @@ val make_instance_subst : Instance.t -> universe_level_subst val make_inverse_instance_subst : Instance.t -> universe_level_subst val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t -val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t (** TODO: move universe abstraction out of the kernel *) val make_abstract_instance : AUContext.t -> Instance.t @@ -505,10 +465,8 @@ val pr_constraint_type : constraint_type -> Pp.t val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> 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) -> ?variance:Variance.t array -> AUContext.t -> Pp.t -val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t val explain_universe_inconsistency : (Level.t -> Pp.t) -> univ_inconsistency -> Pp.t @@ -524,5 +482,3 @@ 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 val hcons_universe_context_set : ContextSet.t -> ContextSet.t -val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t -val hcons_abstract_cumulativity_info : ACumulativityInfo.t -> ACumulativityInfo.t diff --git a/lib/dAst.ml b/lib/dAst.ml index f34ab956a3..803b2a0cff 100644 --- a/lib/dAst.ml +++ b/lib/dAst.ml @@ -30,6 +30,8 @@ let make ?loc v = CAst.make ?loc (Value v) let delay ?loc v = CAst.make ?loc (Thunk (Lazy.from_fun v)) +let force x = CAst.make ?loc:x.CAst.loc (Value (get_thunk x.v)) + let map f n = CAst.map (fun x -> map_thunk f x) n let map_with_loc f n = diff --git a/lib/dAst.mli b/lib/dAst.mli index 28c78784e6..2f58cfc41f 100644 --- a/lib/dAst.mli +++ b/lib/dAst.mli @@ -21,6 +21,7 @@ val get_thunk : ('a, 'b) thunk -> 'a val make : ?loc:Loc.t -> 'a -> ('a, 'b) t val delay : ?loc:Loc.t -> (unit -> 'a) -> ('a, [ `thunk ]) t +val force : ('a, 'b) t -> ('a, 'b) t val map : ('a -> 'b) -> ('a, 'c) t -> ('b, 'c) t val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> ('b, 'c) t diff --git a/lib/envars.ml b/lib/envars.ml index 8a75d9a552..0f4670688b 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -110,11 +110,11 @@ let set_user_coqlib path = coqlib := Some path (** coqlib is now computed once during coqtop initialization *) -let set_coqlib ~boot ~fail = +let set_coqlib ~fail = match !coqlib with | Some _ -> () | None -> - let lib = if boot then coqroot else guess_coqlib fail in + let lib = guess_coqlib fail in coqlib := Some lib let coqlib () = Option.default "" !coqlib diff --git a/lib/envars.mli b/lib/envars.mli index 21365c48f6..ebf86d0650 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -39,7 +39,7 @@ val datadir : unit -> string val configdir : unit -> string (** [set_coqlib] must be runned once before any access to [coqlib] *) -val set_coqlib : boot:bool -> fail:(string -> string) -> unit +val set_coqlib : fail:(string -> string) -> unit (** [set_user_coqlib path] sets the coqlib directory explicitedly. *) val set_user_coqlib : string -> unit diff --git a/lib/flags.ml b/lib/flags.ml index 768d359cce..1195b8caf1 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -101,10 +101,6 @@ let verbosely f x = without_option quiet f x let if_silent f x = if !quiet then f x let if_verbose f x = if not !quiet then f x -let polymorphic_inductive_cumulativity = ref false -let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b -let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity - let warn = ref true let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x diff --git a/lib/flags.mli b/lib/flags.mli index 4ef5fb4445..2b4446a1db 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -75,10 +75,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit -(** Global polymorphic inductive cumulativity flag. *) -val make_polymorphic_inductive_cumulativity : bool -> unit -val is_polymorphic_inductive_cumulativity : unit -> bool - val warn : bool ref val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index c15486ea10..204f889f90 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1032,6 +1032,55 @@ let extract_fixpoint env sg vkn (fi,ti,ci) = current_fixpoints := []; Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) +(** Because of automatic unboxing the easy way [mk_def c] on the + constant body of primitive projections doesn't work. We pretend + that they are implemented by matches until someone figures out how + to clean it up (test with #4710 when working on this). *) +let fake_match_projection env p = + let ind = Projection.Repr.inductive p in + let proj_arg = Projection.Repr.arg p in + let mib, mip = Inductive.lookup_mind_specif env ind in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in + let indu = mkIndU (ind,u) in + let ctx, paramslet = + let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in + let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in + List.chop mip.mind_consnrealdecls.(0) rctx + in + let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in + let ci = { + ci_ind = ind; + ci_npar = mib.mind_nparams; + ci_cstr_ndecls = mip.mind_consnrealdecls; + ci_cstr_nargs = mip.mind_consnrealargs; + ci_pp_info; + } + in + let x = match mib.mind_record with + | NotRecord | FakeRecord -> assert false + | PrimRecord info -> Name (pi1 info.(snd ind)) + in + let indty = mkApp (indu, Context.Rel.to_extended_vect mkRel 0 paramslet) in + let rec fold arg j subst = function + | [] -> assert false + | LocalAssum (na,ty) :: rem -> + let ty = Vars.substl subst (liftn 1 j ty) in + if arg != proj_arg then + let lab = match na with Name id -> Label.of_id id | Anonymous -> assert false in + let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in + fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem + else + let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in + let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in + let body = mkCase (ci, p, mkRel 1, [|branch|]) in + it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt + | LocalDef (_,c,t) :: rem -> + let c = liftn 1 j c in + let c1 = Vars.substl subst c in + fold arg (j+1) (c1::subst) rem + in + fold 0 1 [] (List.rev ctx) + let extract_constant env kn cb = let sg = Evd.from_env env in let r = ConstRef kn in @@ -1069,10 +1118,7 @@ let extract_constant env kn cb = (match Recordops.find_primitive_projection kn with | None -> mk_typ (get_body c) | Some p -> - let p = Projection.make p false in - let ind = Projection.inductive p in - let bodies = Inductiveops.legacy_match_projection env ind in - let body = bodies.(Projection.arg p) in + let body = fake_match_projection env p in mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; @@ -1085,10 +1131,7 @@ let extract_constant env kn cb = (match Recordops.find_primitive_projection kn with | None -> mk_def (get_body c) | Some p -> - let p = Projection.make p false in - let ind = Projection.inductive p in - let bodies = Inductiveops.legacy_match_projection env ind in - let body = bodies.(Projection.arg p) in + let body = fake_match_projection env p in mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 12b68e208c..25a7675113 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -364,7 +364,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = Evd.const_univ_entry ~poly:false evd' in + let univs = Evd.univ_entry ~poly:false evd' in let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 02964d7ba5..ba0a3bbb5c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl = construct in let argl = - if List.is_empty argl - then - Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) - ) - else argl + if List.is_empty argl then + List.make cst_narg (mkGHole ()) + else + List.make npar (mkGHole ()) @ argl in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0c97f9f373..a8517e9ab1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1547,7 +1547,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in + let univs = Evd.univ_entry ~poly:false evd in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2055b25ff4..7da4464e59 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1889,7 +1889,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let univs = Evd.const_univ_entry ~poly sigma in + let univs = Evd.univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = @@ -1975,7 +1975,7 @@ let add_morphism_infer atts m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then - let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in + let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry (None,(instance,uctx),None), diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 62906303a4..30f716d764 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -117,9 +117,14 @@ let combine_appl appl1 appl2 = let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v +let log_trace = ref false + +let is_traced () = + !log_trace || !Flags.profile_ltac + (** More naming applications *) let name_vfun appl vle = - if has_type vle (topwit wit_tacvalue) then + if is_traced () && has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t)) | _ -> vle @@ -137,9 +142,11 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } -let extract_trace ist = match TacStore.get ist.extra f_trace with -| None -> [] -| Some l -> l +let extract_trace ist = + if is_traced () then match TacStore.get ist.extra f_trace with + | None -> [] + | Some l -> l + else [] let print_top_val env v = Pptactic.pr_value Pptactic.ltop v @@ -161,8 +168,11 @@ let catch_error call_trace f x = let e = CErrors.push e in catching_error call_trace iraise e +let wrap_error tac k = + if is_traced () then Proofview.tclORELSE tac k else tac + let catch_error_tac call_trace tac = - Proofview.tclORELSE + wrap_error tac (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e)) @@ -203,9 +213,11 @@ let constr_of_id env id = (** Generic arguments : table of interpretation functions *) (* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *) -let push_trace call ist = match TacStore.get ist.extra f_trace with -| None -> Proofview.tclUNIT [call] -| Some trace -> Proofview.tclUNIT (call :: trace) +let push_trace call ist = + if is_traced () then match TacStore.get ist.extra f_trace with + | None -> Proofview.tclUNIT [call] + | Some trace -> Proofview.tclUNIT (call :: trace) + else Proofview.tclUNIT [] let propagate_trace ist loc id v = if has_type v (topwit wit_tacvalue) then @@ -1263,7 +1275,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = let fold accu (id, v) = Id.Map.add id v accu in let newlfun = List.fold_left fold olfun extfun in if List.is_empty lvar then - begin Proofview.tclORELSE + begin wrap_error begin let ist = { lfun = newlfun; @@ -1423,7 +1435,7 @@ and interp_match_successes lz ist s = (* Interprets the Match expressions *) and interp_match ist lz constr lmr = let (>>=) = Ftactic.bind in - begin Proofview.tclORELSE + begin wrap_error (interp_ltac_constr ist constr) begin function | (e, info) -> @@ -1509,7 +1521,7 @@ and interp_genarg_var_list ist x = (* Interprets tactic expressions : returns a "constr" *) and interp_ltac_constr ist e : EConstr.t Ftactic.t = let (>>=) = Ftactic.bind in - begin Proofview.tclORELSE + begin wrap_error (val_interp ist e) begin function (err, info) -> match err with | Not_found -> @@ -2076,4 +2088,13 @@ let () = optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } +let () = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "Ltac Backtrace"; + optkey = ["Ltac"; "Backtrace"]; + optread = (fun () -> !log_trace); + optwrite = (fun b -> log_trace := b) } + let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 65201d922f..3f69701bd3 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,7 +153,7 @@ let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in let univs = UState.restrict_universe_context univs vars in - let univs = Monomorphic_const_entry univs in + let univs = Monomorphic_entry univs in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~univs c), IsProof Lemma)) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6746e4b902..99cd89cc2a 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module CVars = Vars - open Pp open CErrors open Util @@ -175,16 +173,6 @@ let () = declare_bool_option optread = print_primproj_params; optwrite = (:=) print_primproj_params_value } -let print_primproj_compatibility_value = ref false -let print_primproj_compatibility () = !print_primproj_compatibility_value - -let () = declare_bool_option - { optdepr = false; - optname = "backwards-compatible printing of primitive projections"; - optkey = ["Printing";"Primitive";"Projection";"Compatibility"]; - optread = print_primproj_compatibility; - optwrite = (:=) print_primproj_compatibility_value } - (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) @@ -702,30 +690,12 @@ and detype_r d flags avoid env sigma t = GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), [detype d flags avoid env sigma c]) else - if print_primproj_compatibility () && Projection.unfolded p then - (* Print the compatibility match version *) - let c' = - try - let ind = Projection.inductive p in - let bodies = Inductiveops.legacy_match_projection (snd env) ind in - let body = bodies.(Projection.arg p) in - let ty = Retyping.get_type_of (snd env) sigma c in - let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in - let body' = strip_lam_assum body in - let u = EInstance.kind sigma u in - let body' = CVars.subst_instance_constr u body' in - let body' = EConstr.of_constr body' in - substl (c :: List.rev args) body' - with Retyping.RetypeError _ | Not_found -> - anomaly (str"Cannot detype an unfolded primitive projection.") - in DAst.get (detype d flags avoid env sigma c') - else - if print_primproj_params () then - try - let c = Retyping.expand_projection (snd env) sigma p c [] in - DAst.get (detype d flags avoid env sigma c) - with Retyping.RetypeError _ -> noparams () - else noparams () + if print_primproj_params () then + try + let c = Retyping.expand_projection (snd env) sigma p c [] in + DAst.get (detype d flags avoid env sigma c) + with Retyping.RetypeError _ -> noparams () + else noparams () | Evar (evk,cl) -> let bound_to_itself_or_letin decl c = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aa30ed8d2e..bb163ddaee 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -468,17 +468,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let u = EInstance.kind evd u and u' = EInstance.kind evd u' in let mind = Environ.lookup_mind mi env in let open Declarations in - begin match mind.mind_universes with - | Monomorphic_ind _ -> assert false - | Polymorphic_ind _ -> check_strict evd u u' - | Cumulative_ind cumi -> + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> let nparamsaplied = Stack.args_size sk in let nparamsaplied' = Stack.args_size sk' in let needed = Reduction.inductive_cumulativity_arguments (mind,i) in if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) then check_strict evd u u' else - compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u' + compare_cumulative_instances evd variances u u' end | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') @@ -488,10 +487,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let u = EInstance.kind evd u and u' = EInstance.kind evd u' in let mind = Environ.lookup_mind mi env in let open Declarations in - begin match mind.mind_universes with - | Monomorphic_ind _ -> assert false - | Polymorphic_ind _ -> check_strict evd u u' - | Cumulative_ind cumi -> + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> let nparamsaplied = Stack.args_size sk in let nparamsaplied' = Stack.args_size sk' in let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 6b61b1452e..68626597fc 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -485,7 +485,11 @@ let is_gvar id c = match DAst.get c with | GVar id' -> Id.equal id id' | _ -> false -let rec cases_pattern_of_glob_constr na = DAst.map (function +let rec cases_pattern_of_glob_constr na c = + (* Forcing evaluation to ensure that the possible raising of + Not_found is not delayed *) + let c = DAst.force c in + DAst.map (function | GVar id -> begin match na with | Name _ -> @@ -498,6 +502,8 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function | GApp (c, l) -> begin match DAst.get c with | GRef (ConstructRef cstr,_) -> + let nparams = Inductiveops.inductive_nparams (fst cstr) in + let _,l = List.chop nparams l in PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found end @@ -505,7 +511,7 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function (* A canonical encoding of aliases *) DAst.get (cases_pattern_of_glob_constr na' b) | _ -> raise Not_found - ) + ) c open Declarations open Term diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 91a2ef9c1e..c189a3bcb2 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -89,6 +89,7 @@ val map_pattern : (glob_constr -> glob_constr) -> (** Conversion from glob_constr to cases pattern, if possible + Evaluation is forced. Take the current alias as parameter, @raise Not_found if translation is impossible *) val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ff552c7caf..4c02dc0f09 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -453,12 +453,7 @@ let build_branch_type env sigma dep p cs = let compute_projections env (kn, i as ind) = let open Term in let mib = Environ.lookup_mind kn env in - let u = match mib.mind_universes with - | Monomorphic_ind _ -> Instance.empty - | Polymorphic_ind auctx -> make_abstract_instance auctx - | Cumulative_ind acumi -> - make_abstract_instance (ACumulativityInfo.univ_context acumi) - in + let u = make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let x = match mib.mind_record with | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") @@ -480,25 +475,6 @@ let compute_projections env (kn, i as ind) = (* [Ind inst] is typed in context [params-wo-let] *) ty in - let ci = - let print_info = - { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in - { ci_ind = ind; - ci_npar = nparamargs; - ci_cstr_ndecls = pkt.mind_consnrealdecls; - ci_cstr_nargs = pkt.mind_consnrealargs; - ci_pp_info = print_info } - in - let len = List.length ctx in - let compat_body ccl i = - (* [ccl] is defined in context [params;x:indty] *) - (* [ccl'] is defined in context [params;x:indty;x:indty] *) - let ccl' = liftn 1 2 ccl in - let p = mkLambda (x, lift 1 indty, ccl') in - let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in - let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in - it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params - in let projections decl (proj_arg, j, pbs, subst) = match decl with | LocalDef (na,c,t) -> @@ -528,10 +504,9 @@ let compute_projections env (kn, i as ind) = let ty = substl subst t in let term = mkProj (Projection.make kn true, mkRel 1) in let fterm = mkProj (Projection.make kn false, mkRel 1) in - let compat = compat_body ty (j - 1) in let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in - let body = (etab, etat, compat) in + let body = (etab, etat) in (proj_arg + 1, j + 1, body :: pbs, fterm :: subst) | Anonymous -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") @@ -541,13 +516,6 @@ let compute_projections env (kn, i as ind) = in Array.rev_of_list pbs -let legacy_match_projection env ind = - Array.map pi3 (compute_projections env ind) - -let compute_projections ind mib = - let ans = compute_projections ind mib in - Array.map (fun (prj, ty, _) -> (prj, ty)) ans - (**************************************************) let extract_mrectype sigma t = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b2e205115f..5a4257e175 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,14 +194,6 @@ val compute_projections : Environ.env -> inductive -> (constr * types) array (** Given a primitive record type, for every field computes the eta-expanded projection and its type. *) -val legacy_match_projection : Environ.env -> inductive -> constr array -(** Given a record type, computes the legacy match-based projection of the - projections. - - BEWARE: such terms are ill-typed, and should thus only be used in upper - layers. The kernel will probably badly fail if presented with one of - those. *) - (********************) val type_of_inductive_knowing_conclusion : diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index b5a6ba6be5..bf8a38a353 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -41,33 +41,31 @@ let variance_pb cv_pb var = | CONV, Covariant -> Invariant | CUMUL, Covariant -> Covariant -let infer_cumulative_ind_instance cv_pb cumi variances u = +let infer_cumulative_ind_instance cv_pb mind_variance variances u = Array.fold_left2 (fun variances varu u -> match LMap.find u variances with | exception Not_found -> variances | varu' -> LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances) - variances (ACumulativityInfo.variance cumi) (Instance.to_array u) + variances mind_variance (Instance.to_array u) let infer_inductive_instance cv_pb env variances ind nargs u = let mind = Environ.lookup_mind (fst ind) env in - match mind.mind_universes with - | Monomorphic_ind _ -> assert (Instance.is_empty u); variances - | Polymorphic_ind _ -> infer_generic_instance_eq variances u - | Cumulative_ind cumi -> + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some mind_variance -> if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) then infer_generic_instance_eq variances u - else infer_cumulative_ind_instance cv_pb cumi variances u + else infer_cumulative_ind_instance cv_pb mind_variance variances u let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = let mind = Environ.lookup_mind mi env in - match mind.mind_universes with - | Monomorphic_ind _ -> assert (Instance.is_empty u); variances - | Polymorphic_ind _ -> infer_generic_instance_eq variances u - | Cumulative_ind cumi -> + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some _ -> if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) then infer_generic_instance_eq variances u - else infer_cumulative_ind_instance CONV cumi variances u + else variances (* constructors are convertible at common supertype *) let infer_sort cv_pb variances s = match cv_pb with @@ -189,12 +187,14 @@ let infer_inductive env mie = let { mind_entry_params = params; mind_entry_inds = entries; } = mie in - let univs = - match mie.mind_entry_universes with - | Monomorphic_ind_entry _ - | Polymorphic_ind_entry _ as univs -> univs - | Cumulative_ind_entry (nas, cumi) -> - let uctx = CumulativityInfo.univ_context cumi in + let variances = + match mie.mind_entry_variance with + | None -> None + | Some _ -> + let uctx = match mie.mind_entry_universes with + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> uctx + in let uarray = Instance.to_array @@ UContext.instance uctx in let env = Environ.push_context uctx env in let variances = @@ -212,6 +212,10 @@ let infer_inductive env mie = entries in let variances = Array.map (fun u -> LMap.find u variances) uarray in - Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances)) + Some variances in - { mie with mind_entry_universes = univs } + { mie with mind_entry_variance = variances } + +let dummy_variance = let open Entries in function + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Variance.Irrelevant diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli index a0c8d339ac..6e5bf30f6b 100644 --- a/pretyping/inferCumulativity.mli +++ b/pretyping/inferCumulativity.mli @@ -10,3 +10,5 @@ val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> Entries.mutual_inductive_entry + +val dummy_variance : Entries.universes_entry -> Univ.Variance.t array diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e0403a9f97..797b6faa08 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -86,10 +86,7 @@ let print_ref reduce ref udecl = | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> let mind = Environ.lookup_mind ind env in - begin match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None - | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) - end + mind.Declarations.mind_variance in let inst = if Global.is_polymorphic ref @@ -98,7 +95,7 @@ let print_ref reduce ref udecl = in let priv = None in (* We deliberately don't print private univs in About. *) hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv) + Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) (** Printing implicit arguments *) @@ -562,11 +559,11 @@ let print_constant with_values sep sp udecl = | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with - | Monomorphic_const ctx -> - Monomorphic_const (ContextSet.union body_uctxs ctx) - | Polymorphic_const ctx -> + | Monomorphic ctx -> + Monomorphic (ContextSet.union body_uctxs ctx) + | Polymorphic ctx -> assert(ContextSet.is_empty body_uctxs); - Polymorphic_const ctx + Polymorphic ctx in let ctx = UState.of_binders @@ -580,11 +577,11 @@ let print_constant with_values sep sp udecl = str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs + Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs | Some (c, ctx) -> print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ - Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs) + Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs) let gallina_print_constant_with_infos sp udecl = print_constant true " = " sp udecl ++ diff --git a/printing/printer.ml b/printing/printer.ml index 3f7837fd6e..bc936975c2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -209,7 +209,7 @@ let pr_universe_ctx sigma ?variance c = else mt() -let pr_abstract_universe_ctx sigma ?variance c ~priv = +let pr_abstract_universe_ctx sigma ?variance ?priv c = let open Univ in let priv = Option.default Univ.ContextSet.empty priv in let has_priv = not (ContextSet.is_empty priv) in @@ -221,23 +221,9 @@ let pr_abstract_universe_ctx sigma ?variance c ~priv = else mt() -let pr_constant_universes sigma ~priv = function - | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx - | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv - -let pr_cumulativity_info sigma cumi = - if !Detyping.print_universes - && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then - fnl()++pr_in_comment (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi)) - else - mt() - -let pr_abstract_cumulativity_info sigma cumi = - if !Detyping.print_universes - && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then - fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi)) - else - mt() +let pr_universes sigma ?variance ?priv = function + | Declarations.Monomorphic ctx -> pr_universe_ctx_set sigma ctx + | Declarations.Polymorphic ctx -> pr_abstract_universe_ctx sigma ?variance ?priv ctx (**********************************************************************) (* Global references *) diff --git a/printing/printer.mli b/printing/printer.mli index 9a06d555e4..4e27268c4d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -86,11 +86,11 @@ val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Const val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> - Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t + ?priv:Univ.ContextSet.t -> Univ.AUContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t -val pr_constant_universes : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t -val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t -val pr_abstract_cumulativity_info : evar_map -> Univ.ACumulativityInfo.t -> Pp.t +val pr_universes : evar_map -> + ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t -> + Declarations.universes -> Pp.t (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 898f231a8b..3438063f76 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -126,10 +126,7 @@ let print_mutual_inductive env mind mib udecl = hov 0 (def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env sigma mib) inds ++ - match mib.mind_universes with - | Monomorphic_ind _ | Polymorphic_ind _ -> str "" - | Cumulative_ind cumi -> - Printer.pr_abstract_cumulativity_info sigma cumi) + Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes) let get_fields = let rec prodec_rec l subst c = @@ -178,10 +175,7 @@ let print_record env mind mib udecl = (fun (id,b,c) -> Id.print id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - match mib.mind_universes with - | Monomorphic_ind _ | Polymorphic_ind _ -> str "" - | Cumulative_ind cumi -> - Printer.pr_abstract_cumulativity_info sigma cumi + Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes ) let pr_mutual_inductive_body env mind mib udecl = @@ -302,7 +296,7 @@ let print_body is_impl extent env mp (l,body) = hov 2 (str ":= " ++ Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ - Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs) + Printer.pr_abstract_universe_ctx sigma ctx ?priv:cb.const_private_poly_univs) | SFBmind mib -> match extent with | WithContents -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 0cfc010c1a..a47fa78f4d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -268,7 +268,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let used_univs_body = Vars.universes_of_constr body in let used_univs_typ = Vars.universes_of_constr typ in if allow_deferred then - let initunivs = UState.const_univ_entry ~poly initial_euctx in + let initunivs = UState.univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of @@ -302,7 +302,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now else fun t p -> (* Already checked the univ_decl for the type universes when starting the proof. *) - let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in + let univctx = UState.univ_entry ~poly:false universes in let t = nf t in Future.from_val (univctx, t), Future.chain p (fun (pt,eff) -> diff --git a/tactics/abstract.ml b/tactics/abstract.ml index c3e3a62e26..7a61deba0c 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -162,8 +162,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let cst = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with - | Entries.Monomorphic_const_entry _ -> EInstance.empty - | Entries.Polymorphic_const_entry (_, ctx) -> + | Entries.Monomorphic_entry _ -> EInstance.empty + | Entries.Polymorphic_entry (_, ctx) -> (* We mimick what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 571ad9d160..c1f6365f5d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1309,7 +1309,7 @@ let project_hint ~poly pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in - let ctx = Evd.const_univ_entry ~poly sigma in + let ctx = Evd.univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index a67f5f6d6e..d1b77f3758 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -121,7 +121,7 @@ let define internal id c poly univs = let id = compute_name internal id in let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in - let univs = UState.const_univ_entry ~poly ctx in + let univs = UState.univ_entry ~poly ctx in let entry = { const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 48997163de..335f3c74ff 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -237,9 +237,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in - let univs = - Evd.const_univ_entry ~poly sigma - in + let univs = Evd.univ_entry ~poly sigma in let entry = definition_entry ~univs invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v index b67e93d677..0c236e12ad 100644 --- a/test-suite/bugs/closed/bug_5197.v +++ b/test-suite/bugs/closed/bug_5197.v @@ -1,6 +1,6 @@ Set Universe Polymorphism. Set Primitive Projections. -Unset Printing Primitive Projection Compatibility. + Axiom Ω : Type. Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack { diff --git a/test-suite/bugs/closed/bug_9508.v b/test-suite/bugs/closed/bug_9508.v new file mode 100644 index 0000000000..2c38e24add --- /dev/null +++ b/test-suite/bugs/closed/bug_9508.v @@ -0,0 +1,29 @@ +Set Implicit Arguments. +Unset Strict Implicit. + +Module OK. +Record A := mkA { + T : Type; + P : T -> bool; +}. + +About P. (* Argument a is implicit *) +Check P (true: T (mkA negb)). +End OK. + +Module KO. +Set Primitive Projections. +Record A := mkA { + T : Type; + P : T -> bool; +}. + +About P. (* No implicit arguments *) +Check P (true: T (mkA negb)). +(* +The command has indeed failed with message: +The term "true : T {| T := bool; P := negb |}" has type "T {| T := bool; P := negb |}" +while it is expected to have type "A". +*) + +End KO. diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index 047f4cd080..f5043db099 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -9,13 +9,13 @@ let evil t f = let u = Level.var 0 in let tu = mkType (Universe.make u) in let te = Declare.definition_entry - ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu + ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu in let tc = Declare.declare_constant t (DefinitionEntry te, k) in let tc = mkConst tc in let fe = Declare.definition_entry - ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty))) + ~univs:(Polymorphic_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty))) ~types:(Term.mkArrow tc tu) (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1)) in diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index edc35f17b4..b52537dec0 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -1,6 +1,8 @@ (* coq-prog-args: ("-top" "Errors") *) (* Test error messages *) +Set Ltac Backtrace. + (* Test non-regression of bug fixed in r13486 (bad printer for module names) *) Module Type S. diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out index 8d2a125c1d..2a823396d5 100644 --- a/test-suite/output/FunExt.out +++ b/test-suite/output/FunExt.out @@ -1,19 +1,12 @@ The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Already an intensional equality. The command has indeed failed with message: -In nested Ltac calls to "extensionality in (var)" and -"clearbody (ne_var_list)", last call failed. Hypothesis e depends on the body of H' diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index efa895d709..5bf4ec7bfb 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -53,3 +53,23 @@ Notation Cn := Foo.FooCn Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn let v := 0%test17 in v : myint63 : myint63 +fun y : nat => # (x, z) |-> y & y + : forall y : nat, + (?T1 * ?T2 -> ?T1 * ?T2 * nat) * (?T * ?T0 -> ?T * ?T0 * nat) +where +?T : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0 + |- Type] (pat, p0, p cannot be used) +?T0 : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0 + |- Type] (pat, p0, p cannot be used) +?T1 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2 + |- Type] (pat, p0, p cannot be used) +?T2 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2 + |- Type] (pat, p0, p cannot be used) +fun y : nat => # (x, z) |-> (x + y) & (y + z) + : forall y : nat, + (nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat) +where +?T : [y : nat pat : nat * ?T p0 : nat * ?T p := p0 : nat * ?T + |- Type] (pat, p0, p cannot be used) +?T0 : [y : nat pat : ?T0 * nat p0 : ?T0 * nat p := p0 : ?T0 * nat + |- Type] (pat, p0, p cannot be used) diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index b4c65ce196..b33ad17ed4 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -210,3 +210,12 @@ Module NumeralNotations. Check let v := 0%test17 in v : myint63. End Test17. End NumeralNotations. + +Module K. + +Notation "# x |-> t & u" := ((fun x => (x,t)),(fun x => (x,u))) + (at level 0, x pattern, t, u at level 39). +Check fun y : nat => # (x,z) |-> y & y. +Check fun y : nat => # (x,z) |-> (x + y) & (y + z). + +End K. diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out index 8b38fe0ff4..7ea7a08cb3 100644 --- a/test-suite/output/TypeclassDebug.out +++ b/test-suite/output/TypeclassDebug.out @@ -14,5 +14,4 @@ Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo The command has indeed failed with message: -Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed. Tactic failure: Proof search reached its limit. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index a960fe3441..222a808768 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,5 +1,7 @@ Inductive Empty@{u} : Type@{u} := +(* u |= *) Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } +(* u |= *) PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] @@ -11,6 +13,7 @@ fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p Argument scopes are [type_scope _] Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } +(* u |= *) For RWrap: Argument scope is [type_scope] For rwrap: Argument scopes are [type_scope _] @@ -79,7 +82,9 @@ Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) Inductive Empty@{E} : Type@{E} := +(* E |= *) Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } +(* E |= *) PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] @@ -109,7 +114,9 @@ bind_univs.poly@{u} = Type@{u} insec@{v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* v |= *) -Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} +Inductive insecind@{k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{k} +(* k |= *) For inseccstr: Argument scope is [type_scope] insec@{u v} = Type@{u} -> Type@{v} @@ -117,6 +124,7 @@ insec@{u v} = Type@{u} -> Type@{v} (* u v |= *) Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} +(* u k |= *) For inseccstr: Argument scope is [type_scope] insec2@{u} = Prop diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v index 0dcd76aeff..441e87af84 100644 --- a/test-suite/output/bug5778.v +++ b/test-suite/output/bug5778.v @@ -1,3 +1,4 @@ +Set Ltac Backtrace. Ltac a _ := pose (I : I). Ltac b _ := a (). Ltac abs _ := abstract b (). diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v index bbe6b1a00f..d9e5e20b66 100644 --- a/test-suite/output/bug6404.v +++ b/test-suite/output/bug6404.v @@ -1,3 +1,4 @@ +Set Ltac Backtrace. Ltac a _ := pose (I : I). Ltac b _ := a (). Ltac abs _ := transparent_abstract b (). diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 40e743c3f0..fcd5dd05f0 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -1,3 +1,5 @@ +Set Ltac Backtrace. + (* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *) Goal True. Fail let T := constr:((fun a b : nat => a+b) 1 1) in diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v index 91331a1de5..e30c97aac6 100644 --- a/test-suite/output/ltac_missing_args.v +++ b/test-suite/output/ltac_missing_args.v @@ -1,3 +1,5 @@ +Set Ltac Backtrace. + Ltac foo x := idtac x. Ltac bar x := fun y _ => idtac x y. Ltac baz := foo. diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out index 1515954060..1a0f90493e 100644 --- a/test-suite/output/ssr_clear.out +++ b/test-suite/output/ssr_clear.out @@ -1,3 +1,2 @@ The command has indeed failed with message: -Ltac call to "move (ssrmovearg) (ssrclauses)" failed. No assumption is named NO_SUCH_NAME diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out index 32cfb354bf..0f68ab0b02 100644 --- a/test-suite/output/ssr_explain_match.out +++ b/test-suite/output/ssr_explain_match.out @@ -51,5 +51,4 @@ instance: (addnC y x) matches: (x + y) instance: (addnC y x) matches: (x + y) END INSTANCES The command has indeed failed with message: -Ltac call to "ssrinstancesoftpat (cpattern)" failed. Not supported diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 1b33863e3b..2533a39cc4 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -154,3 +154,14 @@ Module M16. Print Grammar foo. Print Grammar foo2. End M16. + +(* Example showing the need for strong evaluation of + cases_pattern_of_glob_constr (this used to raise Not_found at some + time) *) + +Module M17. + +Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pattern). +Check fun y : nat => # (x,z) ## y & y. + +End M17. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 5526970d3f..4f01a6bd87 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -424,15 +424,15 @@ let _ = end; let project = ensure_root_dir project in - + if project.install_kind <> (Some CoqProject_file.NoInstall) then begin warn_install_at_root_directory project; end; check_overlapping_include project; - Envars.set_coqlib ~boot:false ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1); - + Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1); + let ocm = Option.cata open_out stdout project.makefile in generate_makefile ocm conf_file local_file (prog :: args) project; close_out ocm; diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 5f8cc99ed1..66f1f257b8 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -531,7 +531,7 @@ let coqdep () = add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin (* option_boot is actually always false in this branch *) - Envars.set_coqlib ~boot:!option_boot ~fail:(fun msg -> raise (CoqlibError msg)); + Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg)); let coqlib = Envars.coqlib () in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index c110f3831e..0c9201c3a5 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -251,9 +251,9 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy exception NoCoqLib -let usage ~boot help = +let usage help = begin - try Envars.set_coqlib ~boot ~fail:(fun x -> raise NoCoqLib) + try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) with NoCoqLib -> usage_no_coqlib () end; let lp = Coqinit.toplevel_init_load_path () in @@ -491,7 +491,7 @@ let parse_args ~help ~init arglist : t * string list = |"-type-in-type" -> set_type_in_type (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> { oval with print_where = true } - |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ~boot:oval.boot help; oval + |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval |"-v"|"--version" -> Usage.version (exitcode oval) |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode oval) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e933f08735..1094fc86b4 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -366,6 +366,11 @@ let top_goal_print ~doc c oldp newp = let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer +let exit_on_error = + let open Goptions in + declare_bool_option_and_ref ~depr:false ~name:"coqtop-exit-on-error" ~key:["Coqtop";"Exit";"On";"Error"] + ~value:false + let rec vernac_loop ~state = let open CAst in let open Vernac.State in @@ -410,6 +415,7 @@ let rec vernac_loop ~state = let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; + if exit_on_error () then exit 1; vernac_loop ~state let rec loop ~state = diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c2c538edea..9115fbb726 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -162,7 +162,7 @@ let init_toplevel ~help ~init custom_init arglist = (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); - Envars.set_coqlib ~boot:opts.boot ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); if opts.print_where then begin print_endline (Envars.coqlib ()); exit (exitcode opts) diff --git a/vernac/class.ml b/vernac/class.ml index 8374a5c84f..823177d4d1 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -215,7 +215,7 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = Evd.const_univ_entry ~poly sigma in + let univs = Evd.univ_entry ~poly sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~univs diff --git a/vernac/classes.ml b/vernac/classes.ml index ea434dbc4f..27d8b7390d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -374,7 +374,7 @@ let context poly l = let univs = match ctx with | [] -> assert false - | [_] -> Evd.const_univ_entry ~poly sigma + | [_] -> Evd.univ_entry ~poly sigma | _::_::_ -> if Lib.sections_are_opened () then @@ -384,19 +384,19 @@ let context poly l = begin let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; - if poly then Polymorphic_const_entry ([||], Univ.UContext.empty) - else Monomorphic_const_entry Univ.ContextSet.empty + if poly then Polymorphic_entry ([||], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty end else if poly then (* Multiple polymorphic axioms: they are all polymorphic the same way. *) - Evd.const_univ_entry ~poly sigma + Evd.univ_entry ~poly sigma else (* Multiple monomorphic axioms: declare universes separately to avoid redeclaring them. *) begin let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; - Monomorphic_const_entry Univ.ContextSet.empty + Monomorphic_entry Univ.ContextSet.empty end in let fn status (id, b, t) = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 73d0be04df..4fb06e4e09 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp open CErrors open Util open Vars @@ -46,15 +45,15 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ide match local with | Discharge when Lib.sections_are_opened () -> let ctx = match ctx with - | Monomorphic_const_entry ctx -> ctx - | Polymorphic_const_entry (_, ctx) -> Univ.ContextSet.of_context ctx + | Monomorphic_entry ctx -> ctx + | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx in let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in let _ = declare_variable ident decl in let () = assumption_message ident in let () = if not !Flags.quiet && Proof_global.there_are_pending_proofs () then - Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++ + Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++ strbrk " is not visible from current goals") in let r = VarRef ident in @@ -79,8 +78,8 @@ match local with let () = if do_instance then Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = match ctx with - | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx - | Monomorphic_const_entry _ -> Univ.Instance.empty + | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx + | Monomorphic_entry _ -> Univ.Instance.empty in (gr,inst,Lib.is_modtype_strict ()) @@ -90,10 +89,10 @@ let interp_assumption ~program_mode sigma env impls c = (* When monomorphic the universe constraints are declared with the first declaration only. *) let next_uctx = - let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in + let empty_uctx = Monomorphic_entry Univ.ContextSet.empty in function - | Polymorphic_const_entry _ as uctx -> uctx - | Monomorphic_const_entry _ -> empty_uctx + | Polymorphic_entry _ as uctx -> uctx + | Monomorphic_entry _ -> empty_uctx let declare_assumptions idl is_coe k (c,uctx) pl imps nl = let refs, status, _ = @@ -203,4 +202,4 @@ let do_primitive id prim typopt = } in let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in - register_message id.CAst.v + Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 385ec33bea..2b794b001a 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -29,7 +29,7 @@ val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_ob (** returns [false] if the assumption is neither local to a section, nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag -> assumption_kind -> - types in_constant_universes_entry -> + types in_universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) -> Declaremods.inline -> variable CAst.t -> GlobRef.t * Univ.Instance.t * bool diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 5e74114a86..5eb19eef54 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -35,7 +35,7 @@ let check_imps ~impsty ~impsbody = try List.for_all (fun (key, (va:bool*bool*bool)) -> (* Pervasives.(=) is OK for this type *) - Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va) + Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va) impsbody with Not_found -> false in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 68ad276113..9bbfb8eec6 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -457,15 +457,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in - let univs = - match uctx with - | Polymorphic_const_entry (nas, uctx) -> - if cum then - Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx) - else Polymorphic_ind_entry (nas, uctx) - | Monomorphic_const_entry uctx -> - Monomorphic_ind_entry uctx - in + let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -473,7 +465,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not mind_entry_finite = finite; mind_entry_inds = entries; mind_entry_private = if prv then Some false else None; - mind_entry_universes = univs; + mind_entry_universes = uctx; + mind_entry_variance = variance; } in (if poly && cum then diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 1e3644c371..e455b59ab2 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -19,7 +19,7 @@ val declare_definition : Id.t -> definition_kind -> GlobRef.t val declare_fix : ?opaque:bool -> definition_kind -> - UnivNames.universe_binders -> Entries.constant_universes_entry -> + UnivNames.universe_binders -> Entries.universes_entry -> Id.t -> Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> GlobRef.t diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 367fa4ce98..9dd321be51 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -923,6 +923,8 @@ let explain_not_match_error = function str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++ (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else fnl() ++ str "(incompatible constraints)") + | IncompatibleVariance -> + str "incompatible variance information" let explain_signature_mismatch l spec why = str "Signature components for label " ++ Label.print l ++ diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index d29f66f81f..caafd6ac2f 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -103,7 +103,7 @@ let () = let define ~poly id internal sigma c t = let f = declare_constant ~internal in - let univs = Evd.const_univ_entry ~poly sigma in + let univs = Evd.univ_entry ~poly sigma in let kn = f id (DefinitionEntry { const_entry_body = c; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 79182a3f9d..83dd1aa8e4 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -230,10 +230,10 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_, | Discharge -> let impl = false in (* copy values from Vernacentries *) let univs = match univs with - | Polymorphic_const_entry (_, univs) -> + | Polymorphic_entry (_, univs) -> (* What is going on here? *) Univ.ContextSet.of_context univs - | Monomorphic_const_entry univs -> univs + | Monomorphic_entry univs -> univs in let c = SectionLocalAssum ((t_i, univs),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in @@ -476,7 +476,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in + let ctx = UState.univ_entry ~poly:(pi2 k) universes in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index b20758dac5..ba78c73131 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -557,7 +557,7 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let univs = UState.const_univ_entry ~poly first.prg_ctx in + let univs = UState.univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs) fixnames fixdecls fixtypes fiximps in @@ -656,9 +656,9 @@ let declare_obligation prg obl body ty uctx = if not opaque then add_hint (Locality.make_section_locality None) prg constant; definition_message obl.obl_name; let body = match uctx with - | Polymorphic_const_entry (_, uctx) -> + | Polymorphic_entry (_, uctx) -> Some (DefinedObl (constant, Univ.UContext.instance uctx)) - | Monomorphic_const_entry _ -> + | Monomorphic_entry _ -> Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) in true, { obl with obl_body = body } @@ -879,7 +879,7 @@ let obligation_terminator ?univ_hook name num guard auto pf = if pi2 prg.prg_kind then ctx else UState.union prg.prg_ctx ctx in - let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let () = obls.(num) <- obl in @@ -1010,7 +1010,7 @@ and solve_obligation_by_tac prg obls i tac = (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with | None -> None | Some (t, ty, ctx) -> - let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; @@ -1159,7 +1159,7 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in + let ctx = UState.univ_entry ~poly:false prg.prg_ctx in let kn = Declare.declare_constant x.obl_name ~local:true (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) in diff --git a/vernac/record.ml b/vernac/record.ml index 6b9a564b9e..0bd15e203b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -277,8 +277,8 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in let u = match ctx with - | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx - | Monomorphic_const_entry ctx -> Univ.Instance.empty + | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx + | Monomorphic_entry ctx -> Univ.Instance.empty in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let r = mkIndU (indsp,u) in @@ -369,17 +369,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f open Typeclasses -let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = +let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = let nparams = List.length params in let poly, ctx = match univs with - | Monomorphic_ind_entry ctx -> - false, Monomorphic_const_entry Univ.ContextSet.empty - | Polymorphic_ind_entry (nas, ctx) -> - true, Polymorphic_const_entry (nas, ctx) - | Cumulative_ind_entry (nas, cumi) -> - true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi) + | Monomorphic_entry ctx -> + false, Monomorphic_entry Univ.ContextSet.empty + | Polymorphic_entry (nas, ctx) -> + true, Polymorphic_entry (nas, ctx) in + let variance = if poly && cum then Some (InferCumulativity.dummy_variance ctx) else None in let binder_name = match name with | None -> @@ -427,6 +426,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; + mind_entry_variance = variance; } in let mie = InferCumulativity.infer_inductive (Global.env ()) mie in @@ -472,8 +472,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity (DefinitionEntry class_entry, IsDefinition Definition) in let inst, univs = match univs with - | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs - | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs + | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty in let cstu = (cst, inst) in let inst_type = appvectc (mkConstU cstu) @@ -496,18 +496,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity in [cref, [Name proj_name, sub, Some proj_cst]] | _ -> - let univs = - match univs with - | Polymorphic_const_entry (nas, univs) -> - if cum then - Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs) - else - Polymorphic_ind_entry (nas, univs) - | Monomorphic_const_entry univs -> - Monomorphic_ind_entry univs - in let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in - let inds = declare_structure Declarations.BiFinite ubinders univs paramimpls + let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls params template ~kind:Method ~name:[|binder_name|] record_data in let coers = List.map2 (fun coe pri -> @@ -531,14 +521,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity in let univs, ctx_context, fields = match univs with - | Polymorphic_const_entry (nas, univs) -> + | Polymorphic_entry (nas, univs) -> let usubst, auctx = Univ.abstract_universes nas univs in let usubst = Univ.make_instance_subst usubst in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in auctx, ctx_context, fields - | Monomorphic_const_entry _ -> + | Monomorphic_entry _ -> Univ.AUContext.empty, ctx_context, fields in let map (impl, projs) = @@ -670,21 +660,11 @@ let definition_structure udecl kind ~template cum poly finite records = | _ -> let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in - let univs = - match univs with - | Polymorphic_const_entry (nas, univs) -> - if cum then - Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs) - else - Polymorphic_ind_entry (nas, univs) - | Monomorphic_const_entry univs -> - Monomorphic_ind_entry univs - in let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in - let inds = declare_structure finite ubinders univs implpars params template data in + let inds = declare_structure ~cum finite ubinders univs implpars params template data in List.map (fun ind -> IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index 04984030f7..9852840d12 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -16,7 +16,7 @@ val primitive_flag : bool ref val declare_projections : inductive -> - Entries.constant_universes_entry -> + Entries.universes_entry -> ?kind:Decl_kinds.definition_object_kind -> Id.t -> bool list -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6c4b0acd52..d511bcd4fd 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -609,6 +609,11 @@ let vernac_assumption ~atts discharge kind l nl = let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom +let is_polymorphic_inductive_cumulativity = + declare_bool_option_and_ref ~depr:false ~value:false + ~name:"Polymorphic inductive cumulativity" + ~key:["Polymorphic"; "Inductive"; "Cumulativity"] + let should_treat_as_cumulative cum poly = match cum with | Some VernacCumulative -> @@ -617,7 +622,7 @@ let should_treat_as_cumulative cum poly = | Some VernacNonCumulative -> if poly then false else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") - | None -> poly && Flags.is_polymorphic_inductive_cumulativity () + | None -> poly && is_polymorphic_inductive_cumulativity () let get_uniform_inductive_parameters = Goptions.declare_bool_option_and_ref @@ -1564,14 +1569,6 @@ let () = optwrite = (fun b -> Flags.raw_print := b) } let () = - declare_bool_option - { optdepr = false; - optname = "Polymorphic inductive cumulativity"; - optkey = ["Polymorphic"; "Inductive"; "Cumulativity"]; - optread = Flags.is_polymorphic_inductive_cumulativity; - optwrite = Flags.make_polymorphic_inductive_cumulativity } - -let () = declare_int_option { optdepr = false; optname = "the level of inlining during functor application"; |