diff options
57 files changed, 426 insertions, 241 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index f811f26e1d..451b711be9 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -209,6 +209,9 @@ jobs: mtac2: <<: *ci-template + pidetop: + <<: *ci-template + sf: <<: *ci-template environment: @@ -266,6 +269,7 @@ workflows: - iris-lambda-rust: *req-main - ltac2: *req-main - math-comp: *req-main + - pidetop: *req-main - sf: *req-main - unimath: *req-main - vst: *req-main diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 7f3ee5c37d..74bbda5533 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -302,6 +302,12 @@ /dev/build/windows @MSoegtropIMC # Secondary maintainer @maximedenes +# This file belongs to CI +/Makefile.ci @ejgallego +# Secondary maintainer @SkySkimmer + +/Makefile.doc @maximedenes +# Secondary maintainer @silene ########## Developer tools ########## diff --git a/.gitignore b/.gitignore index 25c0996cb2..e2a97b3a12 100644 --- a/.gitignore +++ b/.gitignore @@ -61,6 +61,7 @@ plugins/micromega/csdpcert plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so coqdoc.sty +coqdoc.css time-of-build.log time-of-build-pretty.log time-of-build-before.log diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d72a33e86e..d16dc5b78c 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,12 +1,15 @@ -image: ubuntu:xenial +image: ubuntu:bionic stages: - opam-boot - build - test +# some default values variables: - # some default values + # Format: $IMAGE-V$DATE-$HOUR-$MINUTE + CACHEKEY: bionic-V2018-04-29-00-50 + DEBIAN_FRONTEND: "noninteractive" NJOBS: "2" COMPILER: "4.02.3" CAMLP5_VER: "6.14" @@ -16,26 +19,26 @@ variables: # some useful values COMPILER_32BIT: "4.02.3+32bit" - COMPILER_BLEEDING_EDGE: "4.06.0" - CAMLP5_VER_BLEEDING_EDGE: "7.03" + COMPILER_BLEEDING_EDGE: "4.06.1" + CAMLP5_VER_BLEEDING_EDGE: "7.05" - TIMING_PACKAGES: "time python" + TIMING_PACKAGES: "time python3" COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" - COQIDE_OPAM: "lablgtk-extras" - COQIDE_OPAM_BE: "lablgtk.2.18.6 lablgtk-extras.1.6" - COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa python3-pip" - COQDOC_OPAM: "hevea" - SPHINX_PACKAGES: "bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex" + COQIDE_OPAM: "lablgtk.2.18.5 conf-gtksourceview.2" + COQIDE_OPAM_BE: "lablgtk.2.18.6 conf-gtksourceview.2" + COQDOC_PACKAGES: "texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip" + SPHINX_PACKAGES: "antlr4-python3-runtime" ELPI_OPAM: "elpi" - before_script: + - cat /proc/{cpu,mem}info || true - ls -a # figure out if artifacts are around - printenv # - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi - apt-get update -qq && apt-get install -y -qq m4 opam ${EXTRA_PACKAGES} + # This should be replaced by standard debian packages once python3-antlr4 makes to the archive. - if [ -n "${PIP_PACKAGES}" ]; then pip3 install ${PIP_PACKAGES}; fi # if no cache running opam config fails! - if [ -d .opamcache ]; then eval $(opam config env); fi @@ -57,9 +60,6 @@ before_script: - .opamcache expire_in: 1 week script: - # the default repo in this docker image is a local directory - # at the time of 4aaeb8abf it lagged behind the official - # repository such that camlp5 7.01 was not available - opam init -a -y -j $NJOBS --compiler=${COMPILER} default https://opam.ocaml.org - eval $(opam config env) - opam update @@ -178,16 +178,16 @@ opam-boot: cache: paths: &cache-paths - .opamcache - key: main + key: "main-$CACHEKEY" variables: - EXTRA_OPAM: "$COQIDE_OPAM $COQDOC_OPAM ocamlgraph $ELPI_OPAM" + EXTRA_OPAM: "$COQIDE_OPAM ocamlgraph $ELPI_OPAM" EXTRA_PACKAGES: "$COQIDE_PACKAGES" opam-boot:32bit: <<: *opam-boot-template cache: paths: *cache-paths - key: 32bit + key: "32bit-$CACHEKEY" variables: COMPILER: "$COMPILER_32BIT" EXTRA_PACKAGES: "gcc-multilib" @@ -196,7 +196,7 @@ opam-boot:bleeding-edge: <<: *opam-boot-template cache: paths: *cache-paths - key: be + key: "be-$CACHEKEY" variables: COMPILER: "$COMPILER_BLEEDING_EDGE" CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" @@ -363,6 +363,9 @@ ci-math-comp: ci-mtac2: <<: *ci-template +ci-pidetop: + <<: *ci-template + ci-sf: <<: *ci-template variables: diff --git a/.travis.yml b/.travis.yml index dca326a200..fce19f9d93 100644 --- a/.travis.yml +++ b/.travis.yml @@ -54,7 +54,7 @@ env: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" - TEST_TARGET="validate" TW="travis_wait" - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" - - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="${FINDLIB_VER_BE}" + - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" matrix: @@ -120,6 +120,9 @@ matrix: - TEST_TARGET="ci-mtac2" - if: NOT (type = pull_request) env: + - TEST_TARGET="ci-pidetop" + - if: NOT (type = pull_request) + env: - TEST_TARGET="ci-sf" - if: NOT (type = pull_request) env: @@ -163,8 +166,6 @@ matrix: - texlive-fonts-extra - latex-xcolor - ghostscript - - transfig - - imagemagick - tipa - python3 - python3-pip @@ -176,7 +177,7 @@ matrix: - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-coqide opt -with-doc yes" - - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + - EXTRA_OPAM="hevea ${LABLGTK_BE}" before_install: *sphinx-install addons: apt: @@ -192,7 +193,7 @@ matrix: - CAMLP5_VER="${CAMLP5_VER_BE}" - NATIVE_COMP="no" - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" - - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + - EXTRA_OPAM="hevea ${LABLGTK_BE}" before_install: *sphinx-install addons: apt: @@ -221,7 +222,7 @@ matrix: - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + - EXTRA_OPAM="hevea ${LABLGTK_BE}" addons: apt: sources: @@ -279,7 +280,7 @@ install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) - opam config list -- opam install -j ${NJOBS} -y camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM} +- opam install -j ${NJOBS} -y num camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM} - opam list script: @@ -1,6 +1,12 @@ Changes from 8.8.2 to 8.9+beta1 =============================== +Tactics + +- Added toplevel goal selector ! which expects a single focused goal. + Use with Set Default Goal Selector to force focusing before tactics + are called. + Tools - Coq_makefile lets one override or extend the following variables from @@ -13,6 +19,12 @@ Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments (not the option). Use the Arguments command instead. +Tactics + +- Introduction tactics "intro"/"intros" on a goal which is an + existential variable now force a refinement of the goal into a + dependent product rather than failing. + Tactic language - Support for fix/cofix added in Ltac "match" and "lazymatch". diff --git a/INSTALL.doc b/INSTALL.doc index 625c368693..f8a0852805 100644 --- a/INSTALL.doc +++ b/INSTALL.doc @@ -22,10 +22,7 @@ To produce all the documents, the following tools are needed: - dvips - bibtex - makeindex - - fig2dev (transfig) - - convert (ImageMagick) - hevea - - hacha - Python 3 - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) - sphinx_rtd_theme @@ -34,17 +31,26 @@ To produce all the documents, the following tools are needed: - Antlr4 runtime for Python 3 -Under Debian based operating systems (Debian, Ubuntu, ...) a -working set of packages for compiling the documentation for Coq is: +Under recent Debian based operating systems (Debian 10 "Buster", +Ubuntu 18.04, ...) a working set of packages for compiling the +documentation for Coq is: - texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra - texlive-humanities texlive-pictures latex-xcolor hevea transfig - imagemagick - python3 python-pip3 + texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx + python3-pexpect python3-sphinx-rtd-theme python3-bs4 + python3-sphinxcontrib.bibtex python3-pip -To install the Python packages required to build the user manual, run: - pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex +Then, install the Python3 Antlr4 package: + + pip3 install antlr4-python3-runtime + +Nix users should get the correct development environment to build the +Sphinx documentation from Coq's `default.nix`. [Note Nix setup doesn't +include the LaTeX packages needed to build the full documentation.] +If you are in an older/different distribution you can install the +Python packages required to build the user manual using python3-pip: + + pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex Compilation ----------- diff --git a/Makefile.ci b/Makefile.ci index 37b14ed918..78fec466cd 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -29,6 +29,7 @@ CI_TARGETS=ci-bignums \ ci-math-classes \ ci-math-comp \ ci-mtac2 \ + ci-pidetop \ ci-sf \ ci-tlc \ ci-unimath \ diff --git a/Makefile.doc b/Makefile.doc index ce31c5fcbe..9b6013d8d7 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -32,10 +32,7 @@ BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 MAKEINDEX:=makeindex PDFLATEX:=pdflatex DVIPS:=dvips -FIG2DEV:=fig2dev -CONVERT:=convert HEVEA:=hevea -HACHA:=hacha HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=coqremote @@ -110,20 +107,6 @@ endif %.ps: %.dvi (cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`) -%.png: %.fig - $(FIG2DEV) -L png -m 2 $< $@ - -%.pdf: %.fig - $(FIG2DEV) -L pdftex $< $@ - $(FIG2DEV) -L pdftex_t -p `basename $@` $< $@_t - -%.eps: %.fig - $(FIG2DEV) -L pstex $< $@ - $(FIG2DEV) -L pstex_t -p `basename $@` $< $@_t - -%.eps: %.png - $(CONVERT) $< $@ - ###################################################################### # Macros for filtering outputs ###################################################################### diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5cee72cc73..1ae2ad0acb 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -156,3 +156,9 @@ ######################################################################## : "${fcsl_pcm_CI_BRANCH:=master}" : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}" + +######################################################################## +# pidetop +######################################################################## +: "${pidetop_CI_BRANCH:=v8.9}" +: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}" diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh new file mode 100755 index 0000000000..d04b9637c0 --- /dev/null +++ b/dev/ci/ci-pidetop.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" + +git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" + +( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top ) + +echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 3c0044bfe9..79001c547b 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -8,6 +8,6 @@ VST_CI_DIR="${CI_BUILD_DIR}/VST" # opam install -j ${NJOBS} -y menhir git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" -# Targets are: msl veric floyd progs , we remove progs to save time -# Patch to avoid the upper version limit -( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd ) +# We have to omit progs as otherwise we timeout on Travis; on Gitlab +# we will be able to just use `make` +( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true -o progs ) diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 009758319b..7ab11889f5 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -272,6 +272,12 @@ focused goals with: In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only be used at the toplevel of a tactic expression. + .. tacv:: !: @expr + + In this variant, if exactly one goal is focused :n:`expr` is + applied to it. Otherwise the tactical fails. ``!:`` can only be + used at the toplevel of a tactic expression. + .. tacv:: par: @expr In this variant, :n:`@expr` is applied to all focused goals in parallel. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7a45272f25..6c1b1c08c1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -53,13 +53,20 @@ specified, the default selector is used. .. opt:: Default Goal Selector @toplevel_selector - This option controls the default selector – used when no selector is - specified when applying a tactic – is set to the chosen value. The initial - value is 1, hence the tactics are, by default, applied to the first goal. - Using value ``all`` will make is so that tactics are, by default, applied to - every goal simultaneously. Then, to apply a tactic tac to the first goal - only, you can write ``1:tac``. Although more selectors are available, only - ``all`` or a single natural number are valid default goal selectors. + This option controls the default selector, used when no selector is + specified when applying a tactic. The initial value is 1, hence the + tactics are, by default, applied to the first goal. + + Using value ``all`` will make it so that tactics are, by default, + applied to every goal simultaneously. Then, to apply a tactic tac + to the first goal only, you can write ``1:tac``. + + Using value ``!`` enforces that all tactics are used either on a + single focused goal or with a local selector (’’strict focusing + mode’’). + + Although more selectors are available, only ``all``, ``!`` or a + single natural number are valid default goal selectors. .. _bindingslist: @@ -627,7 +634,12 @@ puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. -If the goal is neither a product nor starting with a let definition, +If the goal is an existential variable, ``intro`` forces the resolution of the +existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts +:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to +depend on :g:`x`. + +If the goal is neither a product, nor starting with a let definition, nor an existential variable, the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. diff --git a/engine/evarutil.mli b/engine/evarutil.mli index d3937f28e4..e3e8f16c8b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -186,11 +186,14 @@ val nf_evar_map_undefined : evar_map -> evar_map val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] (** Normalize the evar map w.r.t. universes, after simplification of constraints. Return the substitution function for constrs as well. *) val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"] (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of Evar.t diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 70dc6867ac..a771945dd2 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -829,6 +829,8 @@ let is_univ_copy max u = else false +let dump_bytecode = ref false + let dump_bytecodes init code fvs = let open Pp in (str "code =" ++ fnl () ++ @@ -872,7 +874,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = reloc, init_code in let fv = List.rev (!(reloc.in_env).fv_rev) in - (if !Flags.dump_bytecode then + (if !dump_bytecode then Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive msg -> diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index abab58b60b..1c4cdcbeb4 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -25,3 +25,6 @@ val compile_constant_body : fail_on_error:bool -> (** Shortcut of the previous function used during module strengthening *) val compile_alias : Names.Constant.t -> body_code + +(** Dump the bytecode after compilation (for debugging purposes) *) +val dump_bytecode : bool ref diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 7b637c20e6..641d424e2c 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -807,7 +807,7 @@ and lambda_of_args env start args = (*********************************) - +let dump_lambda = ref false let optimize_lambda lam = let lam = simplify subst_id lam in @@ -819,7 +819,7 @@ let lambda_of_constr ~optimize genv c = Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in let lam = if optimize then optimize_lambda lam else lam in - if !Flags.dump_lambda then + if !dump_lambda then Feedback.msg_debug (pp_lam lam); lam diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 89b7fd8e3b..6cf46163e3 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -25,3 +25,6 @@ val dynamic_int31_compilation : bool -> lambda array -> lambda (*spiwack: compiling function to insert dynamic decompilation before matching integers (in case they are in processor representation) *) val int31_escape_before_match : bool -> lambda -> lambda + +(** Dump the VM lambda code after compilation (for debugging purposes) *) +val dump_lambda : bool ref diff --git a/lib/flags.ml b/lib/flags.ml index 2a1c50f52b..56940f1cf7 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -159,11 +159,3 @@ let print_mod_uid = ref false let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 - -let dump_bytecode = ref false -let set_dump_bytecode = (:=) dump_bytecode -let get_dump_bytecode () = !dump_bytecode - -let dump_lambda = ref false -let set_dump_lambda = (:=) dump_lambda -let get_dump_lambda () = !dump_lambda diff --git a/lib/flags.mli b/lib/flags.mli index 53a69f3566..17776d68a4 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -10,6 +10,25 @@ (** Global options of the system. *) +(** WARNING: don't add new entries to this file! + + This file is own its way to deprecation in favor of a purely + functional state, but meanwhile it will contain options that are + truly global to the system such as [compat] or [debug] + + If you are thinking about adding a global flag, well, just + don't. First of all, options make testins exponentially more + expensive, due to the growth of flag combinations. So please make + some effort in order for your idea to work in a configuration-free + manner. + + If you absolutely must pass an option to your new system, then do + so as a functional argument so flags are exposed to unit + testing. Then, register such parameters with the proper + state-handling mechanism of the top-level subsystem of Coq. + + *) + (** Command-line flags *) val boot : bool ref @@ -126,13 +145,3 @@ val print_mod_uid : bool ref val profile_ltac : bool ref val profile_ltac_cutoff : float ref - -(** Dump the bytecode after compilation (for debugging purposes) *) -val dump_bytecode : bool ref -val set_dump_bytecode : bool -> unit -val get_dump_bytecode : unit -> bool - -(** Dump the VM lambda code after compilation (for debugging purposes) *) -val dump_lambda : bool ref -val set_dump_lambda : bool -> unit -val get_dump_lambda : unit -> bool diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2dbd624c2c..3026be248f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -48,6 +48,7 @@ let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" let make_bullet s = + let open Proof_bullet in let n = String.length s in match s.[0] with | '-' -> Dash n diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 845104c3c7..e331dc0143 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -563,8 +563,8 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in - let ctx, f = Evarutil.nf_evars_and_universes ctx in - let f c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in + let ctx = Evd.minimize_universes ctx in + let f c = EConstr.of_constr (Evarutil.nf_evars_universes ctx (EConstr.Unsafe.to_constr c)) in (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fb9ae64bf4..e41bf71dd7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1533,14 +1533,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let env = Global.env() in let evd = Evd.from_env env in let evd, function_type = interp_type_evars env evd type_of_f in - let function_type = EConstr.Unsafe.to_constr function_type in - let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in + let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in - let ty = EConstr.Unsafe.to_constr ty in - let evd, nf = Evarutil.nf_evars_and_universes evd in - let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in - let function_type = nf function_type in + let evd = Evd.minimize_universes evd in + let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in + let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 0c42a8bb28..4857beffa8 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -325,6 +325,7 @@ GEXTEND Gram ; toplevel_selector: [ [ sel = selector_body; ":" -> sel + | "!"; ":" -> SelectAlreadyFocused | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: @@ -415,7 +416,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false VERNAC tactic_mode EXTEND VernacSolve | [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => [ classify_as_proofstep ] -> [ - let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in + let g = Option.default (Goal_select.get_default_goal_selector ()) g in vernac_solve g n t def ] | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 11bb7a2341..bd02d85d59 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -515,6 +515,7 @@ let string_of_genarg_arg (ArgumentType arg) = else int i ++ str "-" ++ int j let pr_goal_selector toplevel = function + | SelectAlreadyFocused -> str "!:" | SelectNth i -> int i ++ str ":" | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" | SelectId id -> str "[" ++ Id.print id ++ str "]:" diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index aea00c240b..799a52cc8b 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -84,7 +84,7 @@ type pp_tactic = { pptac_prods : grammar_terminals; } -val pr_goal_selector : toplevel:bool -> Vernacexpr.goal_selector -> Pp.t +val pr_goal_selector : toplevel:bool -> Goal_select.t -> Pp.t val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 3baa475aba..17f5e5d41a 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -35,7 +35,8 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Vernacexpr.goal_selector = +type goal_selector = Goal_select.t = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -269,7 +270,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr + | TacSelect of Goal_select.t * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 3baa475aba..17f5e5d41a 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -35,7 +35,8 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Vernacexpr.goal_selector = +type goal_selector = Goal_select.t = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -269,7 +270,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr + | TacSelect of Goal_select.t * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 99bb8440c6..33c30e4d38 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -186,8 +186,8 @@ let dummy_goal env sigma = Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in {Evd.it = gl; Evd.sigma = sigma} -let constr_of v = match Value.to_constr v with - | Some c -> EConstr.Unsafe.to_constr c +let constr_of evd v = match Value.to_constr v with + | Some c -> EConstr.to_constr evd c | None -> failwith "Ring.exec_tactic: anomaly" let tactic_res = ref [||] @@ -221,8 +221,8 @@ let exec_tactic env evd n f args = (** Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in - let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - let nf c = nf (constr_of c) in + let evd = Evd.minimize_universes (Refiner.project gls) in + let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd let stdlib_modules = diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml index 4e1c986f16..8bf8104983 100644 --- a/pretyping/vernacexpr.ml +++ b/pretyping/vernacexpr.ml @@ -16,16 +16,13 @@ open Libnames (** Vernac expressions, produced by the parser *) type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation -(* spiwack: I'm choosing, for now, to have [goal_selector] be a - different type than [goal_reference] mostly because if it makes sense - to print a goal that is out of focus (or already solved) it doesn't - make sense to apply a tactic to it. Hence it the types may look very - similar, they do not seem to mean the same thing. *) -type goal_selector = +type goal_selector = Goal_select.t = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t | SelectAll +[@@ocaml.deprecated "Use Goal_select.t"] type goal_identifier = string type scope_name = string @@ -68,7 +65,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation * Universes.univ_name_list option * goal_selector option + | PrintAbout of reference or_by_notation * Universes.univ_name_list option * Goal_select.t option | PrintImplicit of reference or_by_notation | PrintAssumptions of bool * bool * reference or_by_notation | PrintStrategy of reference or_by_notation option @@ -197,7 +194,6 @@ type one_inductive_expr = ident_decl * local_binder_expr list * constr_expr option * constructor_expr list type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr - and typeclass_context = typeclass_constraint list type proof_expr = @@ -269,13 +265,11 @@ type extend_name = (* This type allows registering the inlining of constants in native compiler. It will be extended with primitive inductive types and operators *) -type register_kind = +type register_kind = | RegisterInline -type bullet = - | Dash of int - | Star of int - | Plus of int +type bullet = Proof_bullet.t +[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] (** {6 Types concerning the module layer} *) @@ -425,11 +419,11 @@ type nonrec vernac_expr = | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr + | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr | VernacGlobalCheck of constr_expr | VernacDeclareReduction of string * Genredexpr.raw_red_expr | VernacPrint of printable - | VernacSearch of searchable * goal_selector option * search_restriction + | VernacSearch of searchable * Goal_select.t option * search_restriction | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list @@ -443,8 +437,8 @@ type nonrec vernac_expr = | VernacFocus of int option | VernacUnfocus | VernacUnfocused - | VernacBullet of bullet - | VernacSubproof of goal_selector option + | VernacBullet of Proof_bullet.t + | VernacSubproof of Goal_select.t option | VernacEndSubproof | VernacShow of showable | VernacCheckGuard diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 83c8757070..89117caf4b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -145,7 +145,7 @@ open Pputils | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -508,7 +508,7 @@ open Pputils | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,l,gopt) -> - pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -1122,7 +1122,7 @@ open Pputils | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in let pr_i = match io with None -> mt () - | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in + | Some i -> Goal_select.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) @@ -1176,7 +1176,8 @@ open Pputils | VernacProofMode s -> return (keyword "Proof Mode" ++ str s) | VernacBullet b -> - return (begin match b with + (* XXX: Redundant with Proof_bullet.print *) + return (let open Proof_bullet in begin match b with | Dash n -> str (String.make n '-') | Star n -> str (String.make n '*') | Plus n -> str (String.make n '+') @@ -1184,7 +1185,7 @@ open Pputils | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") + return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml new file mode 100644 index 0000000000..65a94a2c60 --- /dev/null +++ b/proofs/goal_select.ml @@ -0,0 +1,68 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(* spiwack: I'm choosing, for now, to have [goal_selector] be a + different type than [goal_reference] mostly because if it makes sense + to print a goal that is out of focus (or already solved) it doesn't + make sense to apply a tactic to it. Hence it the types may look very + similar, they do not seem to mean the same thing. *) +type t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | SelectId of Id.t + | SelectAll + +(* Default goal selector: selector chosen when a tactic is applied + without an explicit selector. *) +let default_goal_selector = ref (SelectNth 1) +let get_default_goal_selector () = !default_goal_selector + +let pr_range_selector (i, j) = + if i = j then Pp.int i + else Pp.(int i ++ str "-" ++ int j) + +let pr_goal_selector = function + | SelectAlreadyFocused -> Pp.str "!" + | SelectAll -> Pp.str "all" + | SelectNth i -> Pp.int i + | SelectList l -> + Pp.(str "[" + ++ prlist_with_sep pr_comma pr_range_selector l + ++ str "]") + | SelectId id -> Names.Id.print id + +let parse_goal_selector = function + | "!" -> SelectAlreadyFocused + | "all" -> SelectAll + | i -> + let err_msg = "The default selector must be \"all\" or a natural number." in + begin try + let i = int_of_string i in + if i < 0 then CErrors.user_err Pp.(str err_msg); + SelectNth i + with Failure _ -> CErrors.user_err Pp.(str err_msg) + end + +let _ = let open Goptions in + declare_string_option + { optdepr = false; + optname = "default goal selector" ; + optkey = ["Default";"Goal";"Selector"] ; + optread = begin fun () -> + Pp.string_of_ppcmds + (pr_goal_selector !default_goal_selector) + end; + optwrite = begin fun n -> + default_goal_selector := parse_goal_selector n + end + } diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli new file mode 100644 index 0000000000..b1c5723885 --- /dev/null +++ b/proofs/goal_select.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(* spiwack: I'm choosing, for now, to have [goal_selector] be a + different type than [goal_reference] mostly because if it makes sense + to print a goal that is out of focus (or already solved) it doesn't + make sense to apply a tactic to it. Hence it the types may look very + similar, they do not seem to mean the same thing. *) +type t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | SelectId of Id.t + | SelectAll + +val pr_goal_selector : t -> Pp.t +val get_default_goal_selector : unit -> t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index abda04ff1b..03c0969faa 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -100,11 +100,23 @@ let solve ?with_end_tac gi info_lvl tac pr = | None -> tac | Some _ -> Proofview.Trace.record_info_trace tac in - let tac = match gi with - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac - | Vernacexpr.SelectAll -> tac + let tac = let open Goal_select in match gi with + | SelectAlreadyFocused -> + let open Proofview.Notations in + Proofview.numgoals >>= fun n -> + if n == 1 then tac + else + let e = CErrors.UserError + (None, + Pp.(str "Expected a single focused goal but " ++ + int n ++ str " goals are focused.")) + in + Proofview.tclZERO e + + | SelectNth i -> Proofview.tclFOCUS i i tac + | SelectList l -> Proofview.tclFOCUSLIST l tac + | SelectId id -> Proofview.tclFOCUSID id tac + | SelectAll -> tac in let tac = if use_unification_heuristics () then @@ -121,7 +133,7 @@ let solve ?with_end_tac gi info_lvl tac pr = with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") -let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) +let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) let instantiate_nth_evar_com n com = Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 65cde3a3ae..805635dfa4 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -75,7 +75,7 @@ val current_proof_statement : tac] applies [tac] to all subgoals. *) val solve : ?with_end_tac:unit Proofview.tactic -> - Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> + Goal_select.t -> int option -> unit Proofview.tactic -> Proof.t -> Proof.t * bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index e22d382f7d..cc3e79f858 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -10,19 +10,22 @@ open Proof -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int let bullet_eq b1 b2 = match b1, b2 with -| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2 -| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2 -| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2 +| Dash n1, Dash n2 -> n1 = n2 +| Star n1, Star n2 -> n1 = n2 +| Plus n1, Plus n2 -> n1 = n2 | _ -> false let pr_bullet b = match b with - | Vernacexpr.Dash n -> Pp.(str (String.make n '-')) - | Vernacexpr.Star n -> Pp.(str (String.make n '*')) - | Vernacexpr.Plus n -> Pp.(str (String.make n '+')) + | Dash n -> Pp.(str (String.make n '-')) + | Star n -> Pp.(str (String.make n '*')) + | Plus n -> Pp.(str (String.make n '+')) type behavior = { @@ -195,52 +198,5 @@ let put p b = let suggest p = (!current_behavior).suggest p -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - - -(* Default goal selector: selector chosen when a tactic is applied - without an explicit selector. *) -let default_goal_selector = ref (Vernacexpr.SelectNth 1) -let get_default_goal_selector () = !default_goal_selector - -let pr_range_selector (i, j) = - if i = j then Pp.int i - else Pp.(int i ++ str "-" ++ int j) - -let pr_goal_selector = function - | Vernacexpr.SelectAll -> Pp.str "all" - | Vernacexpr.SelectNth i -> Pp.int i - | Vernacexpr.SelectList l -> - Pp.(str "[" - ++ prlist_with_sep pr_comma pr_range_selector l - ++ str "]") - | Vernacexpr.SelectId id -> Names.Id.print id - -let parse_goal_selector = function - | "all" -> Vernacexpr.SelectAll - | i -> - let err_msg = "The default selector must be \"all\" or a natural number." in - begin try - let i = int_of_string i in - if i < 0 then CErrors.user_err Pp.(str err_msg); - Vernacexpr.SelectNth i - with Failure _ -> CErrors.user_err Pp.(str err_msg) - end - -let _ = - Goptions.(declare_string_option{optdepr = false; - optname = "default goal selector" ; - optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> - Pp.string_of_ppcmds - (pr_goal_selector !default_goal_selector) - end; - optwrite = begin fun n -> - default_goal_selector := parse_goal_selector n - end - }) - +let pr_goal_selector = Goal_select.pr_goal_selector +let get_default_goal_selector = Goal_select.get_default_goal_selector diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index ffbaa0fac9..a09a7ec1d2 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -14,7 +14,10 @@ (* *) (**********************************************************) -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int (** A [behavior] is the data of a put function which is called when a bullet prefixes a tactic, a suggest function @@ -42,12 +45,8 @@ val register_behavior : behavior -> unit val put : Proof.t -> t -> Proof.t val suggest : Proof.t -> Pp.t -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - -val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t -val get_default_goal_selector : unit -> Vernacexpr.goal_selector - +(** Deprecated *) +val pr_goal_selector : Goal_select.t -> Pp.t +[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"] +val get_default_goal_selector : unit -> Goal_select.t +[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"] diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fc7c437e6b..842003bc86 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -83,6 +83,7 @@ type proof_ending = | Proved of Vernacexpr.opacity_flag * Misctypes.lident option * proof_object + type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 058e839b47..197f71ca91 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -5,6 +5,7 @@ Proof_type Logic Refine Proof +Goal_select Proof_bullet Proof_global Redexpr diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 0af766219c..b8af2bcd56 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -23,8 +23,8 @@ val crawl : static_block_declaration option val unit_val : Stm.DynBlockData.t -val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t -val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli index 9784de1141..eacd3687ae 100644 --- a/stm/proofBlockDelimiter.mli +++ b/stm/proofBlockDelimiter.mli @@ -38,6 +38,6 @@ val crawl : val unit_val : Stm.DynBlockData.t (* Bullets *) -val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t -val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t diff --git a/stm/stm.ml b/stm/stm.ml index cbd324f5c7..9ea6a305ef 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2288,7 +2288,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; - fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); + fst (Pfedit.solve Goal_select.SelectAll None tac p), ()); (* STATE SPEC: * - start: Modifies the input state adding a proof. * - end : maybe after recovery command. diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 6bd4866c61..70f73df5c1 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -46,8 +46,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = mib.mind_nparams in let sigma, sort = Evd.fresh_sort_in_family env sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in - let sigma, nf = Evarutil.nf_evars_and_universes sigma in - (nf c', Evd.evar_universe_context sigma), eff + let sigma = Evd.minimize_universes sigma in + (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff else let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 5e81e2d4b1..6c7db26c77 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -492,11 +492,13 @@ module New = struct Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) (* Select a subset of the goals *) - let tclSELECT = function - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id - | Vernacexpr.SelectAll -> fun tac -> tac + let tclSELECT = let open Goal_select in function + | SelectNth i -> Proofview.tclFOCUS i i + | SelectList l -> Proofview.tclFOCUSLIST l + | SelectId id -> Proofview.tclFOCUSID id + | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") + | SelectAlreadyFocused -> + anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") (* Check that holes in arguments have been resolved *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 340d8fbf3d..bc2f60186a 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -223,7 +223,7 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic + val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c6d262fef3..59c035e83a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -979,6 +979,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac + | Evar ev when force_flag -> + let sigma, t = Evardefine.define_evar_as_product sigma ev in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (intro_then_gen name_flag move_flag force_flag dep_flag tac) | _ -> begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) @@ -4953,9 +4958,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let evd, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) - let evd, nf = nf_evars_and_universes !evdref in + let evd = Evd.minimize_universes !evdref in let ctx = Evd.universe_context_set evd in - evd, ctx, nf concl + evd, ctx, Evarutil.nf_evars_universes evd concl in let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 8681405175..0951c5c8d4 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -53,3 +53,17 @@ Goal True -> exists (x : Prop), x. Proof. intro H; eexists ?[x]; only [x]: exact True. 1: assumption. Qed. + +(* Strict focusing! *) +Set Default Goal Selector "!". + +Goal True -> True /\ True /\ True. +Proof. + intro. + split;only 2:split. + Fail exact I. + Fail !:exact I. + 1:exact I. + - !:exact H. + - exact I. +Qed. diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index a329894aad..d37ad9f528 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -127,4 +127,28 @@ induction 1 as (n,H,IH). exact Logic.I. Qed. +(* Make "intro"/"intros" progress on existential variables *) +Module Evar. + +Goal exists (A:Prop), A. +eexists. +unshelve (intro x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Goal exists (A:Prop), A. +eexists. +unshelve (intros x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Definition d := ltac:(intro x; exact (x*x)). + +Definition d' : nat -> _ := ltac:(intros;exact 0). + +End Evar. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f6539d80be..e5f22f25e1 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -382,7 +382,7 @@ real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) .PHONY: real-all real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONE: real-all.timing.diff +.PHONY: real-all.timing.diff bytefiles: $(CMOFILES) $(CMAFILES) .PHONY: bytefiles diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 668f9b8935..e60382f2ce 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -435,10 +435,22 @@ let init_toplevel arglist = * early since the master waits us to connect back *) Spawned.init_channels (); Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - if opts.print_where then (print_endline(Envars.coqlib ()); exit(exitcode opts)); - if opts.print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode opts)); - if opts.print_tags then (print_style_tags opts; exit (exitcode opts)); - if opts.filter_opts then (print_string (String.concat "\n" extras); exit 0); + if opts.print_where then begin + print_endline (Envars.coqlib ()); + exit (exitcode opts) + end; + if opts.print_config then begin + Envars.print_config stdout Coq_config.all_src_dirs; + exit (exitcode opts) + end; + if opts.print_tags then begin + print_style_tags opts; + exit (exitcode opts) + end; + if opts.filter_opts then begin + print_string (String.concat "\n" extras); + exit 0; + end; let top_lp = Coqinit.toplevel_init_load_path () in List.iter Mltop.add_coq_path top_lp; Option.iter Mltop.load_ml_object_raw opts.toploop; diff --git a/vernac/classes.ml b/vernac/classes.ml index 7f2642093f..2e1bd69706 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -196,7 +196,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in Pretyping.check_evars env Evd.empty sigma termtype; let univs = Evd.check_univ_decl ~poly sigma decl in let termtype = to_constr sigma termtype in @@ -289,7 +289,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in let sigma = Evarutil.nf_evar_map_undefined sigma in (* Beware of this step, it is required as to minimize universes. *) - let sigma, _nf = Evarutil.nf_evar_map_universes sigma in + let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) Pretyping.check_evars env Evd.empty sigma termtype; let termtype = to_constr sigma termtype in @@ -365,7 +365,7 @@ let context poly l = let sigma = Evd.from_env env in let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in (* Note, we must use the normalized evar from now on! *) - let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env Evd.empty sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in let ctx = diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1466fa243f..7b382dacc3 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -224,7 +224,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Instantiate evars and check all are resolved *) let sigma = solve_unif_constraints_with_heuristics env_rec sigma in - let sigma, _ = nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in (* XXX: We still have evars here in Program *) let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 05c40dbdd7..101298ef4d 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -304,14 +304,16 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in (* Compute renewed arities *) - let sigma, nf = nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let arities = List.map EConstr.(to_constr sigma) arities in let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in - let sigma, nf' = nf_evars_and_universes sigma in - let arities = List.map nf' arities in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in + let arities = List.map nf arities in + let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let uctx = Evd.check_univ_decl ~poly sigma decl in List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 30dd6ec74a..aba5e32db3 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -451,7 +451,7 @@ let start_proof_com ?inference_hook kind thms hook = (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) evd thms in let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in - let evd, _nf = Evarutil.nf_evars_and_universes evd in + let evd = Evd.minimize_universes evd in (* XXX: This nf_evar is critical too!! We are normalizing twice if you look at the previous lines... *) let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in diff --git a/vernac/record.ml b/vernac/record.ml index 78e68e8a30..b89c0060dc 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -168,7 +168,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in - let sigma, _ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let newfs = List.map (EConstr.to_rel_decl sigma) newfs in let newps = List.map (EConstr.to_rel_decl sigma) newps in let typ = EConstr.to_constr sigma typ in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 19658806c5..f0e41d27cc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -909,7 +909,7 @@ let vernac_set_used_variables e = if List.is_empty to_clear then (p, ()) else let tac = Tactics.clear to_clear in - fst (Pfedit.solve SelectAll None tac p), () + fst (Pfedit.solve Goal_select.SelectAll None tac p), () end (*****************************) @@ -1465,22 +1465,22 @@ let _ = optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } - + let _ = declare_bool_option { optdepr = false; optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; - optread = Flags.get_dump_bytecode; - optwrite = Flags.set_dump_bytecode } + optread = (fun () -> !Cbytegen.dump_bytecode); + optwrite = (:=) Cbytegen.dump_bytecode } let _ = declare_bool_option { optdepr = false; optname = "dumping VM lambda code after compilation"; optkey = ["Dump";"Lambda"]; - optread = Flags.get_dump_lambda; - optwrite = Flags.set_dump_lambda } + optread = (fun () -> !Clambda.dump_lambda); + optwrite = (:=) Clambda.dump_lambda } let _ = declare_bool_option @@ -1611,7 +1611,7 @@ let get_current_context_of_args = function let query_command_selector ?loc = function | None -> None - | Some (SelectNth n) -> Some n + | Some (Goal_select.SelectNth n) -> Some n | _ -> user_err ?loc ~hdr:"query_command_selector" (str "Query commands only support the single numbered goal selector.") @@ -1619,17 +1619,16 @@ let vernac_check_may_eval ~atts redexp glopt rc = let glopt = query_command_selector ?loc:atts.loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in - let c = EConstr.Unsafe.to_constr c in let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; - let sigma',nf = Evarutil.nf_evars_and_universes sigma' in + let sigma' = Evd.minimize_universes sigma' in let uctx = Evd.universe_context_set sigma' in let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in - let c = nf c in let j = - if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c)) + if Evarutil.has_undefined_evars sigma' c then + Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) else + let c = EConstr.to_constr sigma' c in (* OK to call kernel which does not support evars *) Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c) in @@ -1912,7 +1911,7 @@ let vernac_subproof gln = Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus subproof_cond () 1 p - | Some (SelectNth n) -> Proof.focus subproof_cond () n p + | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p | _ -> user_err ~hdr:"bracket_selector" (str "Brackets only support the single numbered goal selector.")) |