diff options
122 files changed, 1869 insertions, 1027 deletions
diff --git a/.gitignore b/.gitignore index e2a97b3a12..f1960ba684 100644 --- a/.gitignore +++ b/.gitignore @@ -88,6 +88,8 @@ test-suite/coqdoc/Coqdoc.* test-suite/coqdoc/index.html test-suite/coqdoc/coqdoc.css test-suite/output/MExtraction.out +test-suite/oUnit-anon.cache +test-suite/unit-tests/**/*.test # documentation diff --git a/.travis.yml b/.travis.yml index dbe152b5b5..890ee6d7c7 100644 --- a/.travis.yml +++ b/.travis.yml @@ -55,7 +55,7 @@ matrix: include: - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" + - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" EXTRA_OPAM="ounit" - if: NOT (type = pull_request) env: - TEST_TARGET="validate" TW="travis_wait" @@ -93,39 +93,24 @@ matrix: - TEST_TARGET="ci-equations" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-geocoq" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-fcsl-pcm" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-fiat-crypto" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-fiat-parsers" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-flocq" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-formal-topology" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-hott" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-iris-lambda-rust" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-ltac2" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-math-classes" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-math-comp" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-mtac2" - if: NOT (type = pull_request) env: @@ -133,12 +118,6 @@ matrix: - if: NOT (type = pull_request) env: - TEST_TARGET="ci-sf" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-unimath" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-vst" - env: - TEST_TARGET="lint" @@ -156,7 +135,7 @@ matrix: env: - TEST_TARGET="test-suite" - EXTRA_CONF="-coqide opt -with-doc yes" - - EXTRA_OPAM="${LABLGTK}" + - EXTRA_OPAM="${LABLGTK} ounit" before_install: &sphinx-install - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex addons: @@ -188,7 +167,7 @@ matrix: - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-coqide opt -with-doc yes" - - EXTRA_OPAM="${LABLGTK_BE}" + - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: apt: @@ -205,7 +184,7 @@ matrix: - CAMLP5_VER="${CAMLP5_VER_BE}" - NATIVE_COMP="no" - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" - - EXTRA_OPAM="${LABLGTK_BE}" + - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: apt: @@ -250,6 +229,7 @@ matrix: - CAMLP5_VER=".6.17" - NATIVE_COMP="no" - COQ_DEST="-local" + - EXTRA_OPAM="ounit" before_install: - brew update - brew unlink python @@ -18,6 +18,9 @@ Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments (not the option). Use the Arguments command instead. +- Nested proofs may be enabled through the option `Nested Proofs Allowed`. + By default, they are disabled and produce an error. The deprecation + warning which used to occur when using nested proofs has been removed. Tactics @@ -58,7 +58,7 @@ FIND_SKIP_DIRS:='(' \ -name '_build_ci' -o \ -name '_install_ci' -o \ -name 'user-contrib' -o \ - -name 'coq-makefile' -o \ + -name 'test-suite' -o \ -name '.opamcache' -o \ -name '.coq-native' \ ')' -prune -o diff --git a/Makefile.build b/Makefile.build index ffe6057574..179ca28b6c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -89,6 +89,7 @@ byte: coqbyte coqide-byte pluginsbyte printers MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml) include Makefile.common +include Makefile.vofiles include Makefile.doc ## provides the 'documentation' rule include Makefile.checker include Makefile.ide ## provides the 'coqide' rule diff --git a/Makefile.common b/Makefile.common index eed41fbe71..9493acd1fc 100644 --- a/Makefile.common +++ b/Makefile.common @@ -105,16 +105,12 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ - stm/stm.cma toplevel/toplevel.cma + stm/stm.cma toplevel/toplevel.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma GRAMMARCMA:=grammar/grammar.cma -# modules known by the toplevel of Coq - -OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib)) - ########################################################################### # plugins object files ########################################################################### @@ -163,40 +159,8 @@ PLUGINSOPT:=$(PLUGINSCMO:.cmo=.cmxs) LINKCMO:=$(CORECMA) $(STATICPLUGINS) LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) -########################################################################### -# vo files -########################################################################### - -THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) -PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) -ALLVO := $(THEORIESVO) $(PLUGINSVO) -VFILES := $(ALLVO:.vo=.v) - -## More specific targets - -THEORIESLIGHTVO:= \ - $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO)) - ALLSTDLIB := test-suite/misc/universes/all_stdlib -# convert a (stdlib) filename into a module name: -# remove .vo, replace theories and plugins by Coq, and replace slashes by dots -vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=)))) - -ALLMODS:=$(call vo_to_mod,$(ALLVO)) - - -# Converting a stdlib filename into native compiler filenames -# Used for install targets -vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*))))) - -vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) - -GLOBFILES:=$(ALLVO:.vo=.glob) -LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \ - $(call vo_to_obj,$(ALLVO)) \ - $(VFILES) $(GLOBFILES) - # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.vofiles b/Makefile.vofiles new file mode 100644 index 0000000000..fc902c4a8a --- /dev/null +++ b/Makefile.vofiles @@ -0,0 +1,40 @@ + +# This file calls [find] and as such is not suitable for inclusion in +# the test suite Makefile, unlike Makefile.common. + +########################################################################### +# vo files +########################################################################### + +THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) +PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) +ALLVO := $(THEORIESVO) $(PLUGINSVO) +VFILES := $(ALLVO:.vo=.v) + +## More specific targets + +THEORIESLIGHTVO:= \ + $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO)) + +# convert a (stdlib) filename into a module name: +# remove .vo, replace theories and plugins by Coq, and replace slashes by dots +vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=)))) + +ALLMODS:=$(call vo_to_mod,$(ALLVO)) + + +# Converting a stdlib filename into native compiler filenames +# Used for install targets +vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*))))) + +vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) + +GLOBFILES:=$(ALLVO:.vo=.glob) +LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \ + $(call vo_to_obj,$(ALLVO)) \ + $(VFILES) $(GLOBFILES) + +# For emacs: +# Local Variables: +# mode: makefile +# End: diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 93e7bd99ab..c72705c7f7 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -5,5 +5,5 @@ tar -xf opam64.tar.xz bash opam64/install.sh opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c eval "$(opam config env)" -opam install -y ocamlfind camlp5 +opam install -y ocamlfind camlp5 ounit cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index b7faea13ed..5c882ee856 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -11,6 +11,8 @@ ######################################################################## : "${mathcomp_CI_BRANCH:=master}" : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}" +: "${oddorder_CI_BRANCH:=master}" +: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}" ######################################################################## # UniMath diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 2a14ed352a..f867fd189b 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -71,11 +71,6 @@ git_checkout() echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) } -checkout_mathcomp() -{ - git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}" -} - make() { # +x: add x only if defined @@ -93,7 +88,8 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp "${mathcomp_CI_DIR}" + git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + ( cd "${mathcomp_CI_DIR}/mathcomp" && \ sed -i.bak '/ssrtest/d' Make && \ sed -i.bak '/odd_order/d' Make && \ diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 845addb4cd..5d96c24991 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -6,6 +6,8 @@ ci_dir="$(dirname "$0")" fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto" git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" + ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) -( cd "${fiat_crypto_CI_DIR}" && make lite lite-display ) +fiat_crypto_CI_TARGETS="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display" +( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index bd1d88993c..920272bcfb 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -7,6 +7,4 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq" git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}" -( cd "${GeoCoq_CI_DIR}" && \ - ./configure-ci.sh && \ - make ) +( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 4fc06e8956..6a064b2971 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -7,4 +7,4 @@ math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes" git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}" -( cd "${math_classes_CI_DIR}" && make && make install ) +( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 8c6b910bbb..20328baf2a 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -5,11 +5,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" +oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order" -checkout_mathcomp "${mathcomp_CI_DIR}" +git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" +git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}" -# odd_order takes too much time for travis. -( cd "${mathcomp_CI_DIR}/mathcomp" && \ - sed -i.bak '/PFsection/d' Make && \ - sed -i.bak '/stripped_odd_order_theorem/d' Make && \ - make Makefile.coq && make -f Makefile.coq all ) +( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install ) +( cd "${oddorder_CI_DIR}/" && make ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 62a949f59a..aa20fe1ff0 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -7,7 +7,4 @@ UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath" git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}" -( cd "${UniMath_CI_DIR}" && \ - sed -i.bak '/Folds/d' Makefile && \ - sed -i.bak '/HomologicalAlgebra/d' Makefile && \ - make BUILD_COQ=no ) +( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 79001c547b..7a097eaab4 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -5,9 +5,6 @@ ci_dir="$(dirname "$0")" VST_CI_DIR="${CI_BUILD_DIR}/VST" -# opam install -j ${NJOBS} -y menhir git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" -# 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 ) +( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true ) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 6d7c0d3688..ff448abe81 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,12 @@ ### ML API +Misctypes + + Syntax for universe sorts and kinds has been moved from `Misctypes` + to `Glob_term`, as these are turned into kernel terms by + `Pretyping`. + Proof engine - More functions have been changed to use `EConstr`, notably the @@ -22,6 +28,11 @@ Proof engine should indicate what the canonical form is. An important change is the move of `Globnames.global_reference` to `Names.GlobRef.t`. +### Unit testing + + The test suite now allows writing unit tests against OCaml code in the Coq + code base. Those unit tests create a dependency on the OUnit test framework. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 9dd12087a6..70a9756e51 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -23,7 +23,7 @@ ;; If you load this file from a git repository, checking out an old ;; commit will make it disappear and cause errors for your Emacs -;; startup. To ignore those errors use (require 'coqdev nil t). If you +;; startup. To ignore those errors use (require 'coqdev nil t). If you ;; check out a malicious commit Emacs startup would allow it to run ;; arbitrary code, to avoid this you can copy coqdev.el to any ;; location and adjust the load path accordingly (of course if you run @@ -115,5 +115,36 @@ This does not enable `bug-reference-mode'." (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s")))) (add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode) +(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end) + "Add LEFT and RIGHT around the BEG..END. +Leave the point after RIGHT. BEG and END default to the bounds +of the current region. Leave point OFFSET characters after the +left quote (if OFFSET is nil, leave the point after the right +quote)." + (unless beg + (if (region-active-p) + (setq beg (region-beginning) end (region-end)) + (setq beg (point) end nil))) + (save-excursion + (goto-char (or end beg)) + (insert right)) + (save-excursion + (goto-char beg) + (insert left)) + (if (and end (not offset)) ;; Second test handles the ::`` case + (goto-char (+ end (length left) (length right))) + (goto-char (+ beg (or offset (length left)))))) + +(defun coqdev-sphinx-rst-coq-action () + "Insert a Sphinx role template or quote the current region." + (interactive) + (pcase (read-char "Command [gntm:`]?") + (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`")) + (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`")) + (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`")) + (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`")) + (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1)) + (?` (coqdev-sphinx-quote-coq-refman-region "``" "``")))) + (provide 'coqdev) ;;; coqdev ends here diff --git a/doc/sphinx/MIGRATING b/doc/sphinx/MIGRATING deleted file mode 100644 index fa6fe15379..0000000000 --- a/doc/sphinx/MIGRATING +++ /dev/null @@ -1,238 +0,0 @@ -How to migrate the Coq Reference Manual to Sphinx -================================================= - -# Install Python3 packages (requires Python 3, python3-pip, python3-setuptools) - - * pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex - -# You may want to do this under a virtualenv, particularly if you end up with issues finding sphinxcontrib.bibtex. http://docs.python-guide.org/en/latest/dev/virtualenvs/ - - * pip3 install virtualenv - * virtualenv coqsphinxing # you may want to use -p to specify the python version - * source coqsphinxing/bin/activate # activate the virtual environment - -# After activating the virtual environment you can run the above pip3 command to install sphinx. You will have to activate the virtual environment before building the docs in your session. - -# Add this Elisp code to .emacs, if you're using emacs (recommended): - - (defun sphinx/quote-coq-refman-region (left right &optional beg end count) - (unless beg - (if (region-active-p) - (setq beg (region-beginning) end (region-end)) - (setq beg (point) end nil))) - (unless count - (setq count 1)) - (save-excursion - (goto-char (or end beg)) - (dotimes (_ count) (insert right))) - (save-excursion - (goto-char beg) - (dotimes (_ count) (insert left))) - (if (and end (characterp left)) ;; Second test handles the ::`` case - (goto-char (+ (* 2 count) end)) - (goto-char (+ count beg)))) - - (defun sphinx/coqtop (beg end) - (interactive (list (region-beginning) (region-end))) - (replace-regexp "^Coq < " " " nil beg end) - (indent-rigidly beg end -3) - (goto-char beg) - (insert ".. coqtop:: all\n\n")) - - (defun sphinx/rst-coq-action () - (interactive) - (pcase (read-char "Command?") - (?g (sphinx/quote-coq-refman-region ":g:`" "`")) - (?n (sphinx/quote-coq-refman-region ":n:`" "`")) - (?t (sphinx/quote-coq-refman-region ":token:`" "`")) - (?m (sphinx/quote-coq-refman-region ":math:`" "`")) - (?: (sphinx/quote-coq-refman-region "::`" "`")) - (?` (sphinx/quote-coq-refman-region "``" "``")) - (?c (sphinx/coqtop (region-beginning) (region-end))))) - - (global-set-key (kbd "<f12>") #'sphinx/rst-coq-action) - - With this code installed, you can hit "F12" followed by an appropriate key to do quick markup of text - (this will make more sense once you've started editing the text). - -# Fork the Coq repo, if needed: - - https://github.com/coq/coq - -# Clone the repo to your work machine - -# Add Maxime Dénès's repo as a remote: - - git remote add sphinx https://github.com/maximedenes/coq.git - - (or choose a name other than "sphinx") - - Verify with: - - git remote -v - -# Fetch from the remote - - git fetch sphinx - -# Checkout the sphinx-doc branch - - git checkout sphinx-doc - - You should pull from the repo from time to time to keep your local copy up-to-date: - - git pull sphinx sphinx-doc - - You may want to create a new branch to do your work in. - -# Choose a Reference Manual chapter to work on at - - https://docs.google.com/document/d/1Yo7dV4OI0AY9Di-lsEQ3UTmn5ygGLlhxjym7cTCMCWU - -# For each chapter, raw ReStructuredText (the Sphinx format), created by the "html2rest" utility, - is available in the directory porting/raw-rst/ - - Elsewhere, depending on the chapter, there should be an almost-empty template file already created, - which is in the location where the final version should go - -# Manually edit the .rst file, place it in the correct location - - There are small examples in sphinx/porting/, a larger example in language/gallina-extensions.rst - - (N.B.: the migration is a work-in-progress, your suggestions are welcome) - - Find the chapter you're working on from the online manual at https://coq.inria.fr/distrib/current/refman/. - At the top of the file, after the chapter heading, add: - - :Source: https://coq.inria.fr/distrib/current/refman/the-chapter-file.html - :Converted by: Your Name - - N.B.: These source and converted-by annotations should help for the migration phase. Later on, - those annotations will be removed, and contributors will be mentioned in the Coq credits. - - Remove chapter numbers - - Replace section, subsection numbers with reference labels: - - .. _some-reference-label: - - Place the label before the section or subsection, followed by a blank line. - - Note the leading underscore. Use :ref:`some_reference-label` to refer to such a label; note the leading underscore is omitted. - Many cross-references may be to other chapters. If the required label exists, use it. Otherwise, use a dummy reference of the form - `TODO-n.n.n-mnemonic` we can fixup later. Example: - - :ref:`TODO-1.3.2-definitions` - - We can grep for those TODOs, and the existing subsection number makes it easy to find in the exisyting manual. - - For the particular case of references to chapters, we can use a -convention for the cross-reference name, so no TODO is needed. - - :ref:`thegallinaspecificationlanguage` - -That is, the chapter label is the chapter title, all in lower-case, -with no spaces or punctuation. For chapters with subtitles marked with -a ":", like those for Omega and Nsatz, use just the chapter part -preceding the ":". These labels should already be in the -placeholder .rst files for each chapter. - - - You can also label other items, like grammars, with the same syntax. To refer to such labels, not involving a - section or subsection, use the syntax - - :ref:`Some link text <label-name>` - - Yes, the angle-brackets are needed here! - - For bibliographic references (those in biblio.bib), use :cite:`thecitation`. - - Grammars will get mangled by the translation. Look for "productionlist" in the examples, also see - http://www.sphinx-doc.org/en/stable/markup/para.html. - - For Coq examples that appear, look at the "coqtop" syntax in porting/tricky-bits.rst. The Sphinx - script will run coqtop on those examples, and can show the output (or not). - - The file replaces.rst contains replacement definitions for some items that are clumsy to write out otherwise. - Use - - .. include:: replaces.rst - - to gain access to those definitions in your file (you might need a path prefix). Some especially-important - replacements are |Cic|, |Coq|, |CoqIDE|, and |Gallina|, which display those names in small-caps. Please use them, - so that they're rendered consistently. - - Similarly, there are some LaTeX macros in preamble.rst that can be useful. - - Conventions: - - - Keywords and other literal text is double-backquoted (e.g. ``Module``, ``Section``, ``(``, ``,``). - - - Metavariables are single-backquotes (e.g. `term`, `ident`) - - - Use the cmd directive for Vernacular commands, like: - - .. cmd:: Set Printing All. - - Within this directive, prefix metavariables (ident, term) with @: - - .. cmd:: Add Printing Let @ident. - - There's also the "cmdv" directive for variants of a command. - - - Use the "exn" and "warn" directives for errors and warnings: - - .. exn:: Something's not right. - .. warn:: You shouldn't do that. - - - Use the "example" directive for examples - - - Use the "g" role for inline Gallina, like :g:`fun x => x` - - - Use code blocks for blocks of Gallina. You can use a double-colon at the end of a line:: - - your code here - - which prints a single colon, or put the double-colon on a newline. - -:: - - your other code here - -# Making changes to the text - - The goal of the migration is simply to change the storage format from LaTeX to ReStructuredText. The goal is not - to make any organizational or other substantive changes to the text. If you do notice nits (misspellings, wrong - verb tense, and so on), please do change them. For example, the programming language that Coq is written in is these days - called "OCaml", and there are mentions of the older name "Objective Caml" in the reference manual that should be changed. - -# Build, view the manual - - In the root directory of your local repo, run "make sphinx". You can view the result in a browser by loading the HTML file - associated with your chapter, which will be contained in the directory doc/sphinx/_build/html/ beneath the repo root directory. - Make any changes you need until there are no build warnings and the output is perfect. :-) - -# Creating pull requests - - When your changes are done, commit them, push to your fork: - - git commit -m "useful commit message" file - git push origin sphinx-doc - - (or push to another branch, if you've created one). Then go to your GitHub - fork and create a pull request against Maxime's sphinx-doc - branch. If your commit is recent, you should see a link on your - fork's code page to do that. Otherwise, you may need to go to your - branch on GitHub to do that. - -# Issues/Questions/Suggestions - - As the migration proceeds, if you have technical issues, have a more general question, or want to suggest something, please contact: - - Paul Steckler <steck@stecksoft.com> - Maxime Dénès <maxime.denes@inria.fr> - -# Issues - - Should the stuff in replaces.rst go in preamble.rst? - In LaTeX, some of the grammars add productions to existing nonterminals, like term ++= ... . How to indicate that? diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst new file mode 100644 index 0000000000..5f2f21f2b8 --- /dev/null +++ b/doc/sphinx/README.rst @@ -0,0 +1,325 @@ +============================= + Documenting Coq with Sphinx +============================= + +.. + README.rst is auto-generated from README.template.rst and the coqrst docs; + use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + +Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. + +In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*. Finally, this manual uses a small DSL to describe tactic invocations and commands. + +Coq objects +=========== + +Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise:: + + .. tacv:: simpl @pattern at {+ @num} + :name: simpl_at + + This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + matching :n:`@pattern` in the current goal. + + .. exn:: Too few occurrences + +Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```. + +Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above. + +- Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits. For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```. +- Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. +- Vernac variants, tactic notations, and tactic variants do not have a default name. + +Notations +--------- + +The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_): + +``@…`` + A placeholder (``@ident``, ``@num``, ``@tactic``\ …) + +``{? …}`` + an optional block + +``{* …}``, ``{+ …}`` + an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces + +``{*, …}``, ``{+, …}`` + an optional or mandatory repeatable block, with repetitions separated by commas + +``%|``, ``%{``, … + an escaped character (rendered without the leading ``%``) + +.. + FIXME document the new subscript support + +As an exercise, what do the following patterns mean? + +.. code:: + + pattern {+, @term {? at {+ @num}}} + generalize {+, @term at {+ @num} as @ident} + fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} + +Objects +------- + +Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL): + +``.. cmd::`` :black_nib: A Coq command. + Example:: + + .. cmd:: Infix "@symbol" := @term ({+, @modifier}). + + This command is equivalent to :n:`…`. + +``.. cmdv::`` :black_nib: A variant of a Coq command. + Example:: + + .. cmd:: Axiom @ident : @term. + + This command links :token:`term` to the name :token:`term` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a + postulate. + + .. cmdv:: Parameter @ident : @term. + + This is equivalent to :n:`Axiom @ident : @term`. + +``.. exn::`` :black_nib: An error raised by a Coq command or tactic. + This commonly appears nested in the ``.. tacn::`` that raises the + exception. + + Example:: + + .. tacv:: assert @form by @tactic + + This tactic applies :n:`@tactic` to solve the subgoals generated by + ``assert``. + + .. exn:: Proof is not complete + + Raised if :n:`@tactic` does not fully solve the goal. + +``.. opt::`` :black_nib: A Coq option. + Example:: + + .. opt:: Nonrecursive Elimination Schemes + + This option controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + induction principles. + +``.. prodn::`` :black_nib: Grammar productions. + This is useful if you intend to document individual grammar productions. + Otherwise, use Sphinx's `production lists + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + +``.. tacn::`` :black_nib: A tactic, or a tactic notation. + Example:: + + .. tacn:: do @num @expr + + :token:`expr` is evaluated to ``v`` which must be a tactic value. … + +``.. tacv::`` :black_nib: A variant of a tactic. + Example:: + + .. tacn:: fail + + This is the always-failing tactic: it does not solve any goal. It is + useful for defining other tacticals since it can be caught by + :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching + tacticals. … + + .. tacv:: fail @natural + + The number is the failure level. If no level is specified, it + defaults to 0. … + +``.. thm::`` A theorem. + Example:: + + .. thm:: Bound on the ceiling function + + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. + +``.. warn::`` :black_nib: An warning raised by a Coq command or tactic.. + Do not mistake this for ``.. warning::``; this directive is for warning + messages produced by Coq. + + + Example:: + + .. warn:: Ambiguous path + + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored. + +Coq directives +============== + +In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives: + +``.. coqtop::`` A reST directive to describe interactions with Coqtop. + Usage:: + + .. coqtop:: options… + + Coq code to send to coqtop + + Example:: + + .. coqtop:: in reset undo + + Print nat. + Definition a := 1. + + Here is a list of permissible options: + + - Display options + + - ``all``: Display input and output + - ``in``: Display only input + - ``out``: Display only output + - ``none``: Display neither (useful for setup commands) + + - 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 + + ``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. + +``.. coqdoc::`` A reST directive to display Coqtop-formatted source code. + Usage:: + + .. coqdoc:: + + Coq code to highlight + + Example:: + + .. coqdoc:: + + Definition test := 1. + +``.. example::`` A reST directive for examples. + This behaves like a generic admonition; see + http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition + for more details. + + Example:: + + .. example:: Adding a hint to a database + + The following adds ``plus_comm`` to the ``plu`` database: + + .. coqdoc:: + + Hint Resolve plus_comm : plu. + +``.. inference::`` A reST directive to format inference rules. + This also serves as a small illustration of the way to create new Sphinx + directives. + + Usage:: + + .. inference:: name + + newline-separated premisses + ------------------------ + conclusion + + Example:: + + .. inference:: Prod-Pro + + \WTEG{T}{s} + s \in \Sort + \WTE{\Gamma::(x:T)}{U}{\Prop} + ----------------------------- + \WTEG{\forall~x:T,U}{\Prop} + +``.. preamble::`` A reST directive for hidden math. + Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. + + Example:: + + .. preamble:: + + \newcommand{\paren}[#1]{\left(#1\right)} + +Coq roles +========= + +In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles: + +``:g:`` Coq code. + Use this for Gallina and Ltac snippets:: + + :g:`apply plus_comm; reflexivity` + :g:`Set Printing All.` + :g:`forall (x: t), P(x)` + +``:n:`` Any text using the notation syntax (``@id``, ``{+, …}``, etc.). + Use this to explain tactic equivalences. For example, you might write + this:: + + :n:`generalize @term as @ident` is just like :n:`generalize @term`, but + it names the introduced hypothesis :token:`ident`. + + Note that this example also uses ``:token:``. That's because ``ident`` is + defined in the the Coq manual as a grammar production, and ``:token:`` + creates a link to that. When referring to a placeholder that happens to be + a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```. + +``:production:`` A grammar production not included in a ``productionlist`` directive. + Useful to informally introduce a production, as part of running text. + + Example:: + + :production:`string` indicates a quoted string. + + You're not likely to use this role very commonly; instead, use a + `production list + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_ + and reference its tokens using ``:token:`…```. + +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:: + + .. coqtop:: all + + Lemma l1: 1 + 1 = 2. + + .. coqtop:: all + + Lemma l2: 2 + 2 <> 1. + +Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. + +Abbreviations and macros +------------------------ + +Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. + +Emacs +----- + +The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function. + +Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``:: + + (with-eval-after-load 'rst + (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action)) diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst new file mode 100644 index 0000000000..203251abf4 --- /dev/null +++ b/doc/sphinx/README.template.rst @@ -0,0 +1,117 @@ +============================= + Documenting Coq with Sphinx +============================= + +.. + README.rst is auto-generated from README.template.rst and the coqrst docs; + use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + +Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. + +In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*. Finally, this manual uses a small DSL to describe tactic invocations and commands. + +Coq objects +=========== + +Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise:: + + .. tacv:: simpl @pattern at {+ @num} + :name: simpl_at + + This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + matching :n:`@pattern` in the current goal. + + .. exn:: Too few occurrences + +Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```. + +Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above. + +- Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits. For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```. +- Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. +- Vernac variants, tactic notations, and tactic variants do not have a default name. + +Notations +--------- + +The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_): + +``@…`` + A placeholder (``@ident``, ``@num``, ``@tactic``\ …) + +``{? …}`` + an optional block + +``{* …}``, ``{+ …}`` + an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces + +``{*, …}``, ``{+, …}`` + an optional or mandatory repeatable block, with repetitions separated by commas + +``%|``, ``%{``, … + an escaped character (rendered without the leading ``%``) + +.. + FIXME document the new subscript support + +As an exercise, what do the following patterns mean? + +.. code:: + + pattern {+, @term {? at {+ @num}}} + generalize {+, @term at {+ @num} as @ident} + fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} + +Objects +------- + +Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL): + +[OBJECTS] + +Coq directives +============== + +In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives: + +[DIRECTIVES] + +Coq roles +========= + +In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles: + +[ROLES] + +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:: + + .. coqtop:: all + + Lemma l1: 1 + 1 = 2. + + .. coqtop:: all + + Lemma l2: 2 + 2 <> 1. + +Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. + +Abbreviations and macros +------------------------ + +Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. + +Emacs +----- + +The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function. + +Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``:: + + (with-eval-after-load 'rst + (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action)) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 152f4f6552..09faa06765 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -140,29 +140,29 @@ Declaration of Coercions .. warn:: Ambiguous path. - When the coercion `qualid` is added to the inheritance graph, non - valid coercion paths are ignored; they are signaled by a warning - displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored; they are signaled by a warning + displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. .. cmdv:: Local Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion local to - the current section. + Declares the construction denoted by `qualid` as a coercion local to + the current section. .. cmdv:: Coercion @ident := @term - This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Coercion @ident := @term : @type - This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Local Coercion @ident := @term - This defines `ident` just like ``Let`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Let`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. Assumptions can be declared as coercions at declaration time. This extends the grammar of assumptions from diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index f887a5feea..0e9c23b9bb 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -150,9 +150,10 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin .. _ceil_thm: -**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then +.. thm:: Bound on the ceiling function - :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil` + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. For instance, from 2 x = 1 we can deduce diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 80ea8a1166..b6c35d8fa7 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -11,7 +11,7 @@ Program derivation |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations of program refinements. To use the Derive extension it must first be -required with ``Require Coq.Derive.Derive``. When the extension is loaded, +required with ``Require Coq.derive.Derive``. When the extension is loaded, it provides the following command: .. cmd:: Derive @ident SuchThat @term As @ident diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 23bc9a2e4a..1f7dd9d689 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -96,11 +96,13 @@ language = None # directories to ignore when looking for source files. # This patterns also effect to html_static_path and html_extra_path exclude_patterns = [ - '_build', - 'Thumbs.db', - '.DS_Store', - 'introduction.rst', - 'credits.rst' + '_build', + 'Thumbs.db', + '.DS_Store', + 'introduction.rst', + 'credits.rst', + 'README.rst', + 'README.template.rst' ] # The reST default role (used for this markup: `text`) to use for all diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index aa41f8058d..d170431058 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -553,8 +553,8 @@ has type :token:`type`. .. cmd:: Axiom @ident : @term - This command links *term* to the name *ident* as its specification in - the global context. The fact asserted by *term* is thus assumed as a + This command links :token:`term` to the name :token:`ident` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a postulate. .. exn:: @ident already exists. @@ -1339,7 +1339,8 @@ using the keyword :cmd:`Qed`. .. note:: - #. Several statements can be simultaneously asserted. + #. Several statements can be simultaneously asserted provided option + :opt:`Nested Proofs Allowed` was turned on. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 83dddab4f5..ad1f0caa60 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -55,15 +55,20 @@ Customization at launch time By resource file ~~~~~~~~~~~~~~~~~~~~~~~ -When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file -``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME`` +When |Coq| is launched, with either ``coqtop`` or ``coqc``, the +resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will +be implicitly prepended to any document read by Coq, whether it is an +interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` is the configuration directory of the user (by default its home -directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If +directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is -searched. You can also specify an arbitrary name for the resource file +searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched, +and, if still not found, the file ``~/.coqrc``. If the latter is also +absent, no resource file is loaded. +You can also specify an arbitrary name for the resource file (see option ``-init-file`` below). -This file may contain, for instance, ``Add LoadPath`` commands to add +The resource file may contain, for instance, ``Add LoadPath`` commands to add directories to the load path of |Coq|. It is possible to skip the loading of the resource file with the option ``-q``. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 892ddbc165..eba0db3ff5 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -113,6 +113,8 @@ list of assertion commands is given in :ref:`Assertions`. The command Aborts the editing of the proof named :token:`ident` (in case you have nested proofs). + .. seealso:: :opt:`Nested Proofs Allowed` + .. cmdv:: Abort All Aborts all current goals. @@ -542,23 +544,34 @@ Controlling the effect of proof editing commands .. opt:: Hyps Limit @num -This option controls the maximum number of hypotheses displayed in goals -after the application of a tactic. All the hypotheses remain usable -in the proof development. -When unset, it goes back to the default mode which is to print all -available hypotheses. + This option controls the maximum number of hypotheses displayed in goals + after the application of a tactic. All the hypotheses remain usable + in the proof development. + When unset, it goes back to the default mode which is to print all + available hypotheses. .. opt:: Automatic Introduction -This option controls the way binders are handled -in assertion commands such as ``Theorem ident [binders] : form``. When the -option is on, which is the default, binders are automatically put in -the local context of the goal to prove. + This option controls the way binders are handled + in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the + option is on, which is the default, binders are automatically put in + the local context of the goal to prove. + + When the option is off, binders are discharged on the statement to be + proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) + has to be used to move the assumptions to the local context. + + +.. opt:: Nested Proofs Allowed -When the option is off, binders are discharged on the statement to be -proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) -has to be used to move the assumptions to the local context. + When turned on (it is off by default), this option enables support for nested + proofs: a new assertion command can be inserted before the current proof is + finished, in which case Coq will temporarily switch to the proof of this + *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` + or :cmd:`Defined`), its statement will be made available (as if it had been + proved before starting the previous proof) and Coq will switch back to the + proof of the previous assertion. Controlling memory usage @@ -570,13 +583,13 @@ to force |Coq| to optimize some of its internal data structures. .. cmd:: Optimize Proof -This command forces |Coq| to shrink the data structure used to represent -the ongoing proof. + This command forces |Coq| to shrink the data structure used to represent + the ongoing proof. .. cmd:: Optimize Heap -This command forces the |OCaml| runtime to perform a heap compaction. -This is in general an expensive operation. -See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ -There is also an analogous tactic :tacn:`optimize_heap`. + This command forces the |OCaml| runtime to perform a heap compaction. + This is in general an expensive operation. + See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + There is also an analogous tactic :tacn:`optimize_heap`. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0318bddde4..3835524f0a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -653,7 +653,7 @@ be applied or the goal is not head-reducible. This repeats ``intro`` until it meets the head-constant. It never reduces head-constants and it never fails. -.. tac:: intro @ident +.. tacn:: intro @ident This applies ``intro`` but forces :n:`@ident` to be the name of the introduced hypothesis. @@ -904,15 +904,15 @@ quantification or an implication. .. tacn:: revert {+ @ident} :name: revert -This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses -(possibly defined) to the goal, if this respects dependencies. This tactic is -the inverse of :tacn:`intro`. + This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses + (possibly defined) to the goal, if this respects dependencies. This tactic is + the inverse of :tacn:`intro`. .. exn:: No such hypothesis. .. exn:: @ident is used in the hypothesis @ident. -.. tac:: revert dependent @ident +.. tacn:: revert dependent @ident This moves to the goal the hypothesis :n:`@ident` and all the hypotheses that depend on it. @@ -1122,7 +1122,7 @@ Controlling the proof flow This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by Coq. -.. tacv:: assert form by tactic +.. tacv:: assert @form by @tactic This tactic behaves like :n:`assert` but applies tactic to solve the subgoals generated by assert. @@ -1130,7 +1130,7 @@ Controlling the proof flow .. exn:: Proof is not complete. :name: Proof is not complete. (assert) -.. tacv:: assert form as intro_pattern +.. tacv:: assert @form as @intro_pattern If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), the hypothesis is named after this introduction pattern (in particular, if @@ -1139,7 +1139,7 @@ Controlling the proof flow introduction pattern, the tactic behaves like :n:`assert form` followed by the action done by this introduction pattern. -.. tacv:: assert form as intro_pattern by tactic +.. tacv:: assert @form as @intro_pattern by @tactic This combines the two previous variants of :n:`assert`. @@ -1192,9 +1192,9 @@ Controlling the proof flow This behaves like :n:`enough form` using :n:`intro_pattern` to name or destruct the new hypothesis. -.. tacv:: enough (@ident : form) by tactic -.. tacv:: enough form by tactic -.. tacv:: enough form as intro_pattern by tactic +.. tacv:: enough (@ident : @form) by @tactic +.. tacv:: enough @form by @tactic +.. tacv:: enough @form as @intro_pattern by @tactic This behaves as above but with :n:`tactic` expected to solve the initial goal after the extra assumption :n:`form` is added and possibly destructed. If the @@ -3240,7 +3240,9 @@ the processing of the rewriting rules. The rewriting rule bases are built with the ``Hint Rewrite vernacular`` command. -.. warn:: This tactic may loop if you build non terminating rewriting systems. +.. warning:: + + This tactic may loop if you build non terminating rewriting systems. .. tacv:: autorewrite with {+ @ident} using @tactic @@ -3444,7 +3446,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Declares each :n:`@ident` as a transparent or opaque constant. - .. cmdv:: Hint Extern @num {? @pattern} => tactic + .. cmdv:: Hint Extern @num {? @pattern} => @tactic :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 682553c31b..838926d651 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -106,15 +106,15 @@ Automatic declaration of schemes .. opt:: Elimination Schemes -It is possible to deactivate the automatic declaration of the -induction principles when defining a new inductive type with the -``Unset Elimination Schemes`` command. It may be reactivated at any time with -``Set Elimination Schemes``. + It is possible to deactivate the automatic declaration of the + induction principles when defining a new inductive type with the + ``Unset Elimination Schemes`` command. It may be reactivated at any time with + ``Set Elimination Schemes``. .. opt:: Nonrecursive Elimination Schemes -This option controls whether types declared with the keywords :cmd:`Variant` and -:cmd:`Record` get an automatic declaration of the induction principles. + This option controls whether types declared with the keywords :cmd:`Variant` and + :cmd:`Record` get an automatic declaration of the induction principles. .. opt:: Case Analysis Schemes @@ -125,8 +125,8 @@ This option controls whether types declared with the keywords :cmd:`Variant` and .. opt:: Decidable Equality Schemes -These flags control the automatic declaration of those Boolean equalities (see -the second variant of ``Scheme``). + These flags control the automatic declaration of those Boolean equalities (see + the second variant of ``Scheme``). .. warning:: diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index d464f75bb2..a004959eb6 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -32,8 +32,9 @@ COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals', COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"] COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS) -def coqdoc(coq_code, coqdoc_bin = os.path.join(os.getenv("COQBIN"),"coqdoc")): +def coqdoc(coq_code, coqdoc_bin=None): """Get the output of coqdoc on coq_code.""" + coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc") fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") try: os.write(fd, COQDOC_HEADER.encode("utf-8")) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 21093bd904..606d725bf0 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## ## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## @@ -57,30 +58,37 @@ def make_target(objtype, targetid): return "coq:{}.{}".format(objtype, targetid) class CoqObject(ObjectDescription): - """A generic Coq object; all Coq objects are subclasses of this. + """A generic Coq object for Sphinx; all Coq objects are subclasses of this. The fields and methods to override are listed at the top of this class' implementation. Each object supports the :name: option, which gives an explicit name to link to. - See the documentation of CoqDomain for high-level information. + See the comments and docstrings in CoqObject for more information. """ - # The semantic domain in which this object lives. + # The semantic domain in which this object lives (eg. “tac”, “cmd”, “chm”…). # It matches exactly one of the roles used for cross-referencing. - subdomain = None + subdomain = None # type: str - # The suffix to use in indices for objects of this type - index_suffix = None + # The suffix to use in indices for objects of this type (eg. “(tac)”) + index_suffix = None # type: str # The annotation to add to headers of objects of this type - annotation = None + # (eg. “Command”, “Theorem”) + annotation = None # type: str def _name_from_signature(self, signature): # pylint: disable=no-self-use, unused-argument """Convert a signature into a name to link to. + ‘Signature’ is Sphinx parlance for an object's header (think “type + signature”); for example, the signature of the simplest form of the + ``exact`` tactic is ``exact @id``. + Returns None by default, in which case no name will be automatically - generated. + generated. This is a convenient way to automatically generate names + (link targets) without having to write explicit names everywhere. + """ return None @@ -100,7 +108,7 @@ class CoqObject(ObjectDescription): def handle_signature(self, signature, signode): """Prefix signature with the proper annotation, then render it using - _render_signature. + ``_render_signature`` (for example, add “Command” in front of commands). :returns: the name given to the resulting node, if any """ @@ -110,11 +118,6 @@ class CoqObject(ObjectDescription): self._render_signature(signature, signode) return self.options.get("name") or self._name_from_signature(signature) - @property - def _index_suffix(self): - if self.index_suffix: - return " " + self.index_suffix - def _record_name(self, name, target_id): """Record a name, mapping it to target_id @@ -141,12 +144,14 @@ class CoqObject(ObjectDescription): return targetid def _add_index_entry(self, name, target): - """Add name (with target) to the main index.""" - index_text = name + self._index_suffix + """Add `name` (pointing to `target`) to the main index.""" + index_text = name + if self.index_suffix: + index_text += " " + self.index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) def add_target_and_index(self, name, _, signode): - """Create a target and an index entry for name""" + """Attach a link target to `signode` and an index entry for `name`.""" if name: target = self._add_target(signode, name) # remove trailing . , found in commands, but not ... (ellipsis) @@ -156,31 +161,44 @@ class CoqObject(ObjectDescription): return target class PlainObject(CoqObject): - """A base class for objects whose signatures should be rendered literaly.""" + """A base class for objects whose signatures should be rendered literally.""" def _render_signature(self, signature, signode): signode += addnodes.desc_name(signature, signature) class NotationObject(CoqObject): - """A base class for objects whose signatures should be rendered as nested boxes.""" + """A base class for objects whose signatures should be rendered as nested boxes. + + Objects that inherit from this class can use the notation grammar (“{+ …}”, + “@…”, etc.) in their signature. + """ def _render_signature(self, signature, signode): position = self.state_machine.get_source_and_line(self.lineno) tacn_node = parse_notation(signature, *position) signode += addnodes.desc_name(signature, '', tacn_node) -class TacticObject(PlainObject): - """An object to represent Coq tactics""" - subdomain = "tac" - index_suffix = "(tac)" - annotation = None - class GallinaObject(PlainObject): - """An object to represent Coq theorems""" + r"""A theorem. + + Example:: + + .. thm:: Bound on the ceiling function + + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. + """ subdomain = "thm" index_suffix = "(thm)" annotation = "Theorem" class VernacObject(NotationObject): - """An object to represent Coq commands""" + """A Coq command. + + Example:: + + .. cmd:: Infix "@symbol" := @term ({+, @modifier}). + + This command is equivalent to :n:`…`. + """ subdomain = "cmd" index_suffix = "(cmd)" annotation = "Command" @@ -191,7 +209,20 @@ class VernacObject(NotationObject): return m.group(0).strip() class VernacVariantObject(VernacObject): - """An object to represent variants of Coq commands""" + """A variant of a Coq command. + + Example:: + + .. cmd:: Axiom @ident : @term. + + This command links :token:`term` to the name :token:`term` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a + postulate. + + .. cmdv:: Parameter @ident : @term. + + This is equivalent to :n:`Axiom @ident : @term`. + """ index_suffix = "(cmdv)" annotation = "Variant" @@ -199,18 +230,49 @@ class VernacVariantObject(VernacObject): return None class TacticNotationObject(NotationObject): - """An object to represent Coq tactic notations""" + """A tactic, or a tactic notation. + + Example:: + + .. tacn:: do @num @expr + + :token:`expr` is evaluated to ``v`` which must be a tactic value. … + """ subdomain = "tacn" index_suffix = "(tacn)" annotation = None class TacticNotationVariantObject(TacticNotationObject): - """An object to represent variants of Coq tactic notations""" + """A variant of a tactic. + + Example:: + + .. tacn:: fail + + This is the always-failing tactic: it does not solve any goal. It is + useful for defining other tacticals since it can be caught by + :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching + tacticals. … + + .. tacv:: fail @natural + + The number is the failure level. If no level is specified, it + defaults to 0. … + """ index_suffix = "(tacnv)" annotation = "Variant" class OptionObject(NotationObject): - """An object to represent Coq options""" + """A Coq option. + + Example:: + + .. opt:: Nonrecursive Elimination Schemes + + This option controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + induction principles. + """ subdomain = "opt" index_suffix = "(opt)" annotation = "Option" @@ -219,7 +281,13 @@ class OptionObject(NotationObject): return stringify_with_ellipses(signature) class ProductionObject(NotationObject): - """An object to represent grammar productions""" + """Grammar productions. + + This is useful if you intend to document individual grammar productions. + Otherwise, use Sphinx's `production lists + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + """ + # FIXME (CPC): I have no idea what this does :/ Someone should add an example. subdomain = "prodn" index_suffix = None annotation = None @@ -258,7 +326,22 @@ class ProductionObject(NotationObject): return [idx, node] class ExceptionObject(NotationObject): - """An object to represent Coq errors.""" + """An error raised by a Coq command or tactic. + + This commonly appears nested in the ``.. tacn::`` that raises the + exception. + + Example:: + + .. tacv:: assert @form by @tactic + + This tactic applies :n:`@tactic` to solve the subgoals generated by + ``assert``. + + .. exn:: Proof is not complete + + Raised if :n:`@tactic` does not fully solve the goal. + """ subdomain = "exn" index_suffix = "(err)" annotation = "Error" @@ -269,7 +352,19 @@ class ExceptionObject(NotationObject): return stringify_with_ellipses(signature) class WarningObject(NotationObject): - """An object to represent Coq warnings.""" + """An warning raised by a Coq command or tactic.. + + Do not mistake this for ``.. warning::``; this directive is for warning + messages produced by Coq. + + + Example:: + + .. warn:: Ambiguous path + + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored. + """ subdomain = "warn" index_suffix = "(warn)" annotation = "Warning" @@ -280,14 +375,33 @@ class WarningObject(NotationObject): def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=unused-argument, dangerous-default-value - """And inline role for notations""" + """Any text using the notation syntax (``@id``, ``{+, …}``, etc.). + + Use this to explain tactic equivalences. For example, you might write + this:: + + :n:`generalize @term as @ident` is just like :n:`generalize @term`, but + it names the introduced hypothesis :token:`ident`. + + Note that this example also uses ``:token:``. That's because ``ident`` is + defined in the the Coq manual as a grammar production, and ``:token:`` + creates a link to that. When referring to a placeholder that happens to be + a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```. + """ notation = utils.unescape(text, 1) position = inliner.reporter.get_source_and_line(lineno) return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], [] def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=dangerous-default-value - """And inline role for Coq source code""" + """Coq code. + + Use this for Gallina and Ltac snippets:: + + :g:`apply plus_comm; reflexivity` + :g:`Set Printing All.` + :g:`forall (x: t), P(x)` + """ options['language'] = 'Coq' return code_role(role, rawtext, text, lineno, inliner, options, content) ## Too heavy: @@ -300,15 +414,14 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): # node = nodes.literal(rawtext, '', *highlight_using_coqdoc(code), classes=classes) # return [node], [] -# TODO pass different languages? -LtacRole = GallinaRole = VernacRole = coq_code_role +CoqCodeRole = coq_code_role class CoqtopDirective(Directive): """A reST directive to describe interactions with Coqtop. Usage:: - .. coqtop:: (options)+ + .. coqtop:: options… Coq code to send to coqtop @@ -321,20 +434,28 @@ class CoqtopDirective(Directive): Here is a list of permissible options: - Display - - ‘all’: Display input and output - - ‘in’: Display only input - - ‘out’: Display only output - - ‘none’: Display neither (useful for setup commands) - Behaviour - - ‘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 + - Display options + + - ``all``: Display input and output + - ``in``: Display only input + - ``out``: Display only output + - ``none``: Display neither (useful for setup commands) + + - 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 + + ``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 final_argument_whitespace = True + directive_name = "coqtop" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -349,12 +470,26 @@ class CoqtopDirective(Directive): return [node] class CoqdocDirective(Directive): - """A reST directive to display Coqtop-formatted source code""" + """A reST directive to display Coqtop-formatted source code. + + Usage:: + + .. coqdoc:: + + Coq code to highlight + + Example:: + + .. coqdoc:: + + Definition test := 1. + """ # TODO implement this as a Pygments highlighter? has_content = True required_arguments = 0 optional_arguments = 0 final_argument_whitespace = True + directive_name = "coqdoc" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -365,8 +500,24 @@ class CoqdocDirective(Directive): return [wrapper] class ExampleDirective(BaseAdmonition): - """A reST directive for examples""" + """A reST directive for examples. + + This behaves like a generic admonition; see + http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition + for more details. + + Example:: + + .. example:: Adding a hint to a database + + The following adds ``plus_comm`` to the ``plu`` database: + + .. coqdoc:: + + Hint Resolve plus_comm : plu. + """ node_class = nodes.admonition + directive_name = "example" def run(self): # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’, @@ -380,8 +531,17 @@ class ExampleDirective(BaseAdmonition): class PreambleDirective(MathDirective): r"""A reST directive for hidden math. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s + Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. + + Example:: + + .. preamble:: + + \newcommand{\paren}[#1]{\left(#1\right)} """ + + directive_name = "preamble" + def run(self): self.options['nowrap'] = True [node] = super().run() @@ -389,14 +549,17 @@ class PreambleDirective(MathDirective): return [node] class InferenceDirective(Directive): - r"""A small example of what directives let you do in Sphinx. + r"""A reST directive to format inference rules. + + This also serves as a small illustration of the way to create new Sphinx + directives. Usage:: .. inference:: name - \n-separated premisses - ---------------------- + newline-separated premisses + ------------------------ conclusion Example:: @@ -413,6 +576,7 @@ class InferenceDirective(Directive): optional_arguments = 0 has_content = True final_argument_whitespace = True + directive_name = "inference" def make_math_node(self, latex): node = displaymath() @@ -613,7 +777,7 @@ class CoqSubdomainsIndex(Index): Just as in the original manual, we want to have separate indices for each Coq subdomain (tactics, commands, options, etc)""" - name, localname, shortname, subdomains = None, None, None, None # Must be overwritten + name, localname, shortname, subdomains = None, None, None, [] # Must be overwritten def generate(self, docnames=None): content = defaultdict(list) @@ -635,7 +799,7 @@ class CoqVernacIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "cmdindex", "Command Index", "commands", ["cmd"] class CoqTacticIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tac", "tacn"] + name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"] class CoqOptionIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"] @@ -665,10 +829,18 @@ class IndexXRefRole(XRefRole): return title, target def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): - """An inline role to declare grammar productions that are not in fact included - in a `productionlist` directive. + """A grammar production not included in a ``productionlist`` directive. - Useful to informally introduce a production, as part of running text + Useful to informally introduce a production, as part of running text. + + Example:: + + :production:`string` indicates a quoted string. + + You're not likely to use this role very commonly; instead, use a + `production list + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_ + and reference its tokens using ``:token:`…```. """ #pylint: disable=dangerous-default-value, unused-argument env = inliner.document.settings.env @@ -681,6 +853,8 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte env.domaindata['std']['objects']['token', text] = env.docname, targetid return [node], [] +GrammarProductionRole.role_name = "production" + class CoqDomain(Domain): """A domain to document Coq code. @@ -703,7 +877,6 @@ class CoqDomain(Domain): # ObjType (= directive type) → (Local name, *xref-roles) 'cmd': ObjType('cmd', 'cmd'), 'cmdv': ObjType('cmdv', 'cmd'), - 'tac': ObjType('tac', 'tac'), 'tacn': ObjType('tacn', 'tacn'), 'tacv': ObjType('tacv', 'tacn'), 'opt': ObjType('opt', 'opt'), @@ -720,7 +893,6 @@ class CoqDomain(Domain): # the same role. 'cmd': VernacObject, 'cmdv': VernacVariantObject, - 'tac': TacticObject, 'tacn': TacticNotationObject, 'tacv': TacticNotationVariantObject, 'opt': OptionObject, @@ -733,7 +905,6 @@ class CoqDomain(Domain): roles = { # Each of these roles lives in a different semantic “subdomain” 'cmd': XRefRole(warn_dangling=True), - 'tac': XRefRole(warn_dangling=True), 'tacn': XRefRole(warn_dangling=True), 'opt': XRefRole(warn_dangling=True), 'thm': XRefRole(warn_dangling=True), @@ -743,12 +914,8 @@ class CoqDomain(Domain): # This one is special 'index': IndexXRefRole(), # These are used for highlighting - 'notation': NotationRole, - 'gallina': GallinaRole, - 'ltac': LtacRole, 'n': NotationRole, - 'g': GallinaRole, - 'l': LtacRole, #FIXME unused? + 'g': CoqCodeRole } indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex] @@ -759,7 +926,6 @@ class CoqDomain(Domain): # others, such as “version” 'objects' : { # subdomain → name → docname, objtype, targetid 'cmd': {}, - 'tac': {}, 'tacn': {}, 'opt': {}, 'thm': {}, @@ -829,11 +995,18 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: for node in doctree.traverse(is_coqtop_or_coqdoc_block): if is_html: node.rawsource = '' # Prevent pygments from kicking in + elif 'coqtop-hidden' in node['classes']: + node.parent.remove(node) else: - if 'coqtop-hidden' in node['classes']: - node.parent.remove(node) - else: - node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) + node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) + +COQ_ADDITIONAL_DIRECTIVES = [CoqtopDirective, + CoqdocDirective, + ExampleDirective, + InferenceDirective, + PreambleDirective] + +COQ_ADDITIONAL_ROLES = [GrammarProductionRole] def setup(app): """Register the Coq domain""" @@ -845,12 +1018,13 @@ def setup(app): # Add domain, directives, and roles app.add_domain(CoqDomain) - app.add_role("production", GrammarProductionRole) - app.add_directive("coqtop", CoqtopDirective) - app.add_directive("coqdoc", CoqdocDirective) - app.add_directive("example", ExampleDirective) - app.add_directive("inference", InferenceDirective) - app.add_directive("preamble", PreambleDirective) + + for role in COQ_ADDITIONAL_ROLES: + app.add_role(role.role_name, role) + + for directive in COQ_ADDITIONAL_DIRECTIVES: + app.add_directive(directive.directive_name, directive) + app.add_transform(CoqtopBlocksTransform) app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py new file mode 100755 index 0000000000..e56882a521 --- /dev/null +++ b/doc/tools/coqrst/regen_readme.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- + +"""Rebuild sphinx/README.rst from sphinx/README.template.rst.""" + +import re +from os import sys, path + +SCRIPT_DIR = path.dirname(path.abspath(__file__)) +if __name__ == "__main__" and __package__ is None: + sys.path.append(path.dirname(SCRIPT_DIR)) + +import sphinx +from coqrst import coqdomain + +README_ROLES_MARKER = "[ROLES]" +README_OBJECTS_MARKER = "[OBJECTS]" +README_DIRECTIVES_MARKER = "[DIRECTIVES]" + +FIRST_LINE_BLANKS = re.compile("^(.*)\n *\n") +def format_docstring(template, obj, *strs): + docstring = obj.__doc__.strip() + 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 "" + +def regen_readme(): + objects_docs = [format_docstring("``.. {}::``{} {}", obj, objname, notation_symbol(obj)) + for objname, obj in sorted(coqdomain.CoqDomain.directives.items())] + + roles = ([(name, cls) + for name, cls in sorted(coqdomain.CoqDomain.roles.items()) + if not isinstance(cls, (sphinx.roles.XRefRole, coqdomain.IndexXRefRole))] + + [(fn.role_name, fn) + for fn in coqdomain.COQ_ADDITIONAL_ROLES]) + roles_docs = [format_docstring("``:{}:`` {}", role, name) + for (name, role) in roles] + + directives_docs = [format_docstring("``.. {}::`` {}", d, d.directive_name) + for d in coqdomain.COQ_ADDITIONAL_DIRECTIVES] + + with open(README_TEMPLATE_PATH, encoding="utf-8") as readme: + contents = readme.read() + + with open(README_PATH, mode="w", encoding="utf-8") as readme: + readme.write(contents + .replace(README_ROLES_MARKER, "\n\n".join(roles_docs)) + .replace(README_OBJECTS_MARKER, "\n\n".join(objects_docs)) + .replace(README_DIRECTIVES_MARKER, "\n\n".join(directives_docs))) + +if __name__ == '__main__': + regen_readme() diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index efb5cb5505..aeadce4c4a 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -41,7 +41,9 @@ class CoqTop: the ansicolors module) :param args: Additional arugments to coqtop. """ - self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN'),"coqtop") + 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", "-color", "on"] * color self.coqtop = None diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 6c27d59375..2b202ef3ed 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -436,7 +436,7 @@ let new_pure_evar_full evd evi = let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -463,14 +463,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca in (evd, newevk) -let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = +let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance = let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in evd, mkEvar (newevk,Array.of_list instance) -let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ = +let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ = let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in let instance = match filter with @@ -480,7 +480,7 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ = +let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ = let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in @@ -490,7 +490,7 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnami | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid = +let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) @@ -613,10 +613,11 @@ let rec check_and_clear_in_constr env evdref err ids global c = | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c -let clear_hyps_in_evi_main env evdref hyps terms ids = +let clear_hyps_in_evi_main env sigma hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occurring in evi *) + let evdref = ref sigma in let terms = List.map EConstr.Unsafe.to_constr terms in let global = Id.Set.exists is_section_variable ids in let terms = @@ -639,16 +640,16 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = in remove_hyps ids check_context check_value hyps in - (nhyps,List.map EConstr.of_constr terms) + (!evdref, nhyps,List.map EConstr.of_constr terms) -let clear_hyps_in_evi env evdref hyps concl ids = - match clear_hyps_in_evi_main env evdref hyps [concl] ids with - | (nhyps,[nconcl]) -> (nhyps,nconcl) +let clear_hyps_in_evi env sigma hyps concl ids = + match clear_hyps_in_evi_main env sigma hyps [concl] ids with + | (sigma,nhyps,[nconcl]) -> (sigma,nhyps,nconcl) | _ -> assert false -let clear_hyps2_in_evi env evdref hyps t concl ids = - match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with - | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl) +let clear_hyps2_in_evi env sigma hyps t concl ids = + match clear_hyps_in_evi_main env sigma hyps [t;concl] ids with + | (sigma,nhyps,[t;nconcl]) -> (sigma,nhyps,t,nconcl) | _ -> assert false (* spiwack: a few functions to gather evars on which goals depend. *) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 3bbd2923c1..7dd98bac97 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -25,10 +25,11 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar_from_context : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * EConstr.t type naming_mode = | KeepUserNameAndRenameExistingButSectionNames @@ -37,41 +38,31 @@ type naming_mode = | FailIfConflict val new_evar : - env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> types -> evar_map * EConstr.t + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> types -> evar_map * EConstr.t val new_pure_evar : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * Evar.t + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * Evar.t val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t -(** the same with side-effects *) -val e_new_evar : - env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> types -> constr - (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> rigid -> - evar_map * (constr * Sorts.t) - -val e_new_type_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> rigid -> + evar_map * (constr * Sorts.t) val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr -val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr val restrict_evar : evar_map -> Evar.t -> Filter.t -> ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t @@ -79,7 +70,6 @@ val restrict_evar : evar_map -> Evar.t -> Filter.t -> (** Polymorphic constants *) val new_global : evar_map -> GlobRef.t -> evar_map * constr -val e_new_global : evar_map ref -> GlobRef.t -> constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -88,10 +78,10 @@ val e_new_global : evar_map ref -> GlobRef.t -> constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> + named_context_val -> evar_map -> types -> constr list -> evar_map * constr val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list @@ -187,8 +177,6 @@ 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. *) @@ -237,11 +225,11 @@ type clear_dependency_error = exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option -val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> - Id.Set.t -> named_context_val * types +val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types -> + Id.Set.t -> evar_map * named_context_val * types -val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> - Id.Set.t -> named_context_val * types * types +val clear_hyps2_in_evi : env -> evar_map -> named_context_val -> types -> types -> + Id.Set.t -> evar_map * named_context_val * types * types type csubst @@ -276,3 +264,25 @@ type type_constraint = types option [@@ocaml.deprecated "use the version in Evardefine"] type val_constraint = constr option [@@ocaml.deprecated "use the version in Evardefine"] + +val e_new_evar : + env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> types -> constr +[@@ocaml.deprecated "Use [Evd.new_evar]"] + +val e_new_type_evar : env -> evar_map ref -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t +[@@ocaml.deprecated "Use [Evd.new_type_evar]"] + +val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr +[@@ocaml.deprecated "Use [Evd.new_Type]"] + +val e_new_global : evar_map ref -> GlobRef.t -> constr +[@@ocaml.deprecated "Use [Evd.new_global]"] + +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"] diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index d8fdfdb1bd..6c7ca4f8e5 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -508,7 +508,6 @@ let rec parse = function let () = Coqtop.toploop_init := (fun coq_args extra_args -> let args = parse extra_args in - Flags.quiet := true; CoqworkmgrApi.(init High); coq_args, args) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 6f5887ca2b..73c108319f 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -18,7 +18,6 @@ open Pattern open Constrexpr open Notation_term open Notation -open Misctypes open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax diff --git a/interp/constrintern.ml b/interp/constrintern.ml index def8425ec3..48f15f8979 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -980,17 +980,17 @@ let intern_reference ref = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option = +let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option = match info with - | Misctypes.UAnonymous -> None - | Misctypes.UUnknown -> None - | Misctypes.UNamed id -> Some (id, 0) + | UAnonymous -> None + | UUnknown -> None + | UNamed id -> Some (id, 0) -let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort = +let glob_sort_of_level (level: glob_level) : glob_sort = match level with - | Misctypes.GProp -> Misctypes.GProp - | Misctypes.GSet -> Misctypes.GSet - | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info] + | GProp -> GProp + | GSet -> GSet + | GType info -> GType [sort_info_of_level_info info] (* Is it a global reference or a syntactic definition? *) let intern_qualid qid intern env ntnvars us args = @@ -1024,7 +1024,7 @@ let intern_qualid qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v) diff --git a/interp/declare.mli b/interp/declare.mli index f8cffbb1e1..de4d8346a4 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -88,5 +88,5 @@ val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit val do_universe : polymorphic -> Misctypes.lident list -> unit -val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> +val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> unit diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index d5feafbf91..be2b05da8d 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -18,6 +18,7 @@ #include <caml/misc.h> #include <caml/mlvalues.h> #include <caml/fail.h> +#include <caml/alloc.h> #include <caml/memory.h> #include "coq_instruct.h" #include "coq_fix_code.h" @@ -78,38 +79,41 @@ void * coq_stat_alloc (asize_t sz) } value coq_makeaccu (value i) { - code_t q; - code_t res = coq_stat_alloc(2 * sizeof(opcode_t)); - q = res; + CAMLparam1(i); + CAMLlocal1(res); + code_t q = coq_stat_alloc(2 * sizeof(opcode_t)); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = q; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); - return (value)res; + CAMLreturn(res); } value coq_pushpop (value i) { - code_t res; - int n; - n = Int_val(i); + CAMLparam1(i); + CAMLlocal1(res); + code_t q; + res = caml_alloc_small(1, Abstract_tag); + int n = Int_val(i); if (n == 0) { - res = coq_stat_alloc(sizeof(opcode_t)); - *res = VALINSTR(STOP); - return (value)res; + q = coq_stat_alloc(sizeof(opcode_t)); + Code_val(res) = q; + *q = VALINSTR(STOP); + CAMLreturn(res); } else { - code_t q; - res = coq_stat_alloc(3 * sizeof(opcode_t)); - q = res; + q = coq_stat_alloc(3 * sizeof(opcode_t)); + Code_val(res) = q; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; *q = VALINSTR(STOP); - return (value)res; + CAMLreturn(res); } } value coq_is_accumulate_code(value code){ - code_t q; + code_t q = Code_val(code); int res; - q = (code_t)code; res = Is_instruction(q,ACCUMULATE); return Val_bool(res); } @@ -132,11 +136,14 @@ value coq_is_accumulate_code(value code){ #define COPY32(dst,src) (*dst=*src) #endif /* ARCH_BIG_ENDIAN */ -value coq_tcode_of_code (value code, value size) { - code_t p, q, res; - asize_t len = (asize_t) Long_val(size); - res = coq_stat_alloc(len); - q = res; +value coq_tcode_of_code (value code) { + CAMLparam1 (code); + CAMLlocal1 (res); + code_t p, q; + asize_t len = (asize_t) caml_string_length(code); + res = caml_alloc_small(1, Abstract_tag); + q = coq_stat_alloc(len); + Code_val(res) = q; len /= sizeof(opcode_t); for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) { opcode_t instr; @@ -166,5 +173,5 @@ value coq_tcode_of_code (value code, value size) { for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; }; } } - return (value)res; + CAMLreturn(res); } diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 5c85389dd5..638d6b5ab5 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -26,7 +26,7 @@ void init_arity(); #define Is_instruction(pc,instr) (*pc == VALINSTR(instr)) -value coq_tcode_of_code(value code, value len); +value coq_tcode_of_code(value code); value coq_makeaccu (value i); value coq_pushpop (value i); value coq_is_accumulate_code(value code); diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index cfeb0a9ee1..8ac1ecc79e 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -16,6 +16,7 @@ #include <stdio.h> #include <signal.h> #include <stdint.h> +#include <caml/memory.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -629,7 +630,7 @@ value coq_interprete print_instr("CLOSUREREC"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfuncs, 0); + Alloc_small(accu, nfuncs, Abstract_tag); for(i = 0; i < nfuncs; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -665,7 +666,7 @@ value coq_interprete print_instr("CLOSURECOFIX"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfunc, 0); + Alloc_small(accu, nfunc, Abstract_tag); for(i = 0; i < nfunc; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -1071,12 +1072,22 @@ value coq_interprete } } *--sp = accu; - /* We create the switch zipper */ - Alloc_small(accu, 5, Default_tag); - Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; - Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; - Field(accu, 4) = coq_env; - sp++;sp[0] = accu; + /* Create bytecode wrappers */ + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = typlbl; + *--sp = accu; + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = swlbl; + *--sp = accu; + /* We create the switch zipper */ + Alloc_small(accu, 5, Default_tag); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; + Field(accu, 2) = sp[3]; + Field(accu, 3) = sp[2]; + Field(accu, 4) = coq_env; + sp += 3; + sp[0] = accu; /* We create the atom */ Alloc_small(accu, 2, ATOM_SWITCH_TAG); Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; @@ -1476,7 +1487,8 @@ value coq_interprete #endif } -value coq_push_ra(value tcode) { +value coq_push_ra(value code) { + code_t tcode = Code_val(code); print_instr("push_ra"); coq_sp -= 3; coq_sp[0] = (value) tcode; @@ -1516,8 +1528,10 @@ value coq_push_vstack(value stk, value max_stack_size) { } value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) { + // Registering the other arguments w.r.t. the OCaml GC is done by coq_interprete + CAMLparam1(tcode); print_instr("coq_interprete"); - return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea)); + CAMLreturn (coq_interprete(Code_val(tcode), a, t, g, e, Long_val(ea))); print_instr("end coq_interprete"); } diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index b2917a55ee..542a05fd25 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -10,6 +10,8 @@ #include <stdio.h> #include <string.h> +#include <caml/alloc.h> +#include <caml/address_class.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -46,7 +48,11 @@ value coq_static_alloc(value size) /* ML */ value accumulate_code(value unit) /* ML */ { - return (value) accumulate; + CAMLparam1(unit); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = accumulate; + CAMLreturn(res); } static void (*coq_prev_scan_roots_hook) (scanning_action); @@ -56,6 +62,10 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { +#ifdef NO_NAKED_POINTERS + /* The VM stack may contain C-allocated bytecode */ + if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue; +#endif (*action) (*i, i); }; /* Hook */ @@ -94,8 +104,12 @@ value init_coq_vm(value unit) /* ML */ /* Initialing the interpreter */ init_coq_interpreter(); - /* Some predefined pointer code */ - accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t)); + /* Some predefined pointer code. + * It is typically contained in accumlator blocks whose tag is 0 and thus + * scanned by the GC, so make it look like an OCaml block. */ + value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); + Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ + accumulate = (code_t) Val_hp(accu_block); *accumulate = VALINSTR(ACCUMULATE); /* Initialize GC */ diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 528babebfc..e05f3fb82e 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -9,6 +9,7 @@ /***********************************************************************/ #include <stdio.h> +#include <caml/memory.h> #include "coq_fix_code.h" #include "coq_instruct.h" #include "coq_memory.h" @@ -58,10 +59,36 @@ value coq_offset_closure(value v, value offset){ return (value)&Field(v, Int_val(offset)); } +value coq_set_bytecode_field(value v, value i, value code) { + // No write barrier because the bytecode does not live on the OCaml heap + Field(v, Long_val(i)) = (value) Code_val(code); + return Val_unit; +} + value coq_offset_tcode(value code,value offset){ - return((value)((code_t)code + Int_val(offset))); + CAMLparam1(code); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = Code_val(code) + Int_val(offset); + CAMLreturn(res); } -value coq_int_tcode(value code, value offset) { +value coq_int_tcode(value pc, value offset) { + code_t code = Code_val(pc); return Val_int(*((code_t) code + Int_val(offset))); } + +value coq_tcode_array(value tcodes) { + CAMLparam1(tcodes); + CAMLlocal2(res, tmp); + int i; + /* Assumes that the vector of types is small. This was implicit in the + previous code which was building the type array using Alloc_small. */ + res = caml_alloc_small(Wosize_val(tcodes), Default_tag); + for (i = 0; i < Wosize_val(tcodes); i++) { + tmp = caml_alloc_small(1, Abstract_tag); + Code_val(tmp) = (code_t) Field(tcodes, i); + Store_field(res, i, tmp); + } + CAMLreturn(res); +} diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 14f4f27c09..cea09c5104 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -20,7 +20,7 @@ open Mod_subst type emitcodes = String.t -external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code" +external tcode_of_code : Bytes.t -> Vmvalues.tcode = "coq_tcode_of_code" (* Relocation information *) type reloc_info = @@ -82,7 +82,7 @@ let patch buff pl f = (** Order seems important here? *) let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in let buff = patch_int buff reloc in - tcode_of_code buff (Bytes.length buff) + tcode_of_code buff (* Buffering of bytecode *) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 6a41efac24..7a703e6537 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -59,14 +59,17 @@ let vm_global (v : values array) = (Obj.magic v : vm_global) (*******************************************) type tcode +(** A block whose first field is a C-allocated VM bytecode, encoded as char*. + This is compatible with the representation of the Coq VM closures. *) + +type tcode_array external mkAccuCode : int -> tcode = "coq_makeaccu" external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" -let tcode_of_obj v = ((Obj.obj v):tcode) -let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) -let fix_code v = fun_code v -let cofix_upd_code v = fun_code v +let fun_code v = (Obj.magic v : tcode) +let fix_code = fun_code +let cofix_upd_code = fun_code type vswitch = { @@ -255,6 +258,7 @@ external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" external is_accumulate : tcode -> bool = "coq_is_accumulate_code" external int_tcode : tcode -> int -> int = "coq_int_tcode" external accumulate : unit -> tcode = "accumulate_code" +external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field" let accumulate = accumulate () let whd_val : values -> whd = @@ -284,7 +288,7 @@ let whd_val : values -> whd = let obj_of_atom : atom -> Obj.t = fun a -> let res = Obj.new_block accu_tag 2 in - Obj.set_field res 0 (Obj.repr accumulate); + set_bytecode_field res 0 accumulate; Obj.set_field res 1 (Obj.repr a); res @@ -370,17 +374,20 @@ external closure_arity : vfun -> int = "coq_closure_arity" external offset : Obj.t -> int = "coq_offset" external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" +external tcode_array : tcode_array -> tcode array = "coq_tcode_array" let first o = (offset_closure o (offset o)) let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix) let last o = (Obj.field o (Obj.size o - 1)) -let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array) -let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array) +let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) +let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) let current_fix vf = - (offset (Obj.repr vf) / 2) -let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) +let unsafe_fb_code fb i = + let off = (2 * i) * (Sys.word_size / 8) in + Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off)) let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 @@ -442,13 +449,12 @@ let relaccu_code i = let mk_fix_body k ndef fb = let e = Obj.dup (Obj.repr fb) in for i = 0 to ndef - 1 do - Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) + set_bytecode_field e (2 * i) (relaccu_code (k + i)) done; let fix_body i = - let jump_grabrec c = offset_tcode c 2 in - let c = jump_grabrec (unsafe_fb_code fb i) in + let c = offset_tcode (unsafe_fb_code fb i) 2 in let res = Obj.new_block Obj.closure_tag 2 in - Obj.set_field res 0 (Obj.repr c); + set_bytecode_field res 0 c; Obj.set_field res 1 (offset_closure e (2*i)); ((Obj.obj res) : vfun) in Array.init ndef fix_body @@ -486,7 +492,7 @@ let mk_cofix_body apply_varray k ndef vcf = Obj.set_field e 0 c; let atom = Obj.new_block cofix_tag 1 in let self = Obj.new_block accu_tag 2 in - Obj.set_field self 0 (Obj.repr accumulate); + set_bytecode_field self 0 accumulate; Obj.set_field self 1 (Obj.repr atom); apply_varray (Obj.obj e) [|Obj.obj self|] in Array.init ndef cofix_body diff --git a/library/misctypes.ml b/library/misctypes.ml index 72db3b31cb..b5d30559d8 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -50,25 +50,6 @@ type 'id move_location = | MoveFirst | MoveLast (** can be seen as "no move" when doing intro *) -(** Sorts *) - -type 'a glob_sort_gen = - | GProp (** representation of [Prop] literal *) - | GSet (** representation of [Set] literal *) - | GType of 'a (** representation of [Type] literal *) - -type 'a universe_kind = - | UAnonymous - | UUnknown - | UNamed of 'a - -type level_info = Libnames.reference universe_kind -type glob_level = level_info glob_sort_gen -type glob_constraint = glob_level * Univ.constraint_type * glob_level - -type sort_info = (Libnames.reference * int) option list -type glob_sort = sort_info glob_sort_gen - (** A synonym of [Evar.t], also defined in Term *) type existential_key = Evar.t diff --git a/man/coqtop.1 b/man/coqtop.1 index b1fbb3262e..084adfe453 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -110,7 +110,7 @@ print Coq version and exit .TP .B \-q -skip loading of rcfile +skip loading of rcfile (resource file) if any .TP .BI \-init\-file \ filename diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9c2806bead..a03ef268d7 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -10,6 +10,7 @@ open Names open Libnames +open Glob_term open Constrexpr open Constrexpr_ops open Util diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 0fbf2f567f..387a62604f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -227,8 +227,8 @@ module Constr : val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry val global : reference Gram.entry - val universe_level : glob_level Gram.entry - val sort : glob_sort Gram.entry + val universe_level : Glob_term.glob_level Gram.entry + val sort : Glob_term.glob_sort Gram.entry val sort_family : Sorts.family Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c4db49cd31..361981c5b0 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -49,7 +49,7 @@ let whd_delta env sigma t = (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = e_sort_of env (ref sigma) c +let sf_of env sigma c = snd (sort_of env sigma c) let rec decompose_term env sigma t= match EConstr.kind sigma (whd env sigma t) with @@ -264,9 +264,8 @@ let app_global_with_holes f args n = let ans = mkApp (fc, args) in let (sigma, holes) = gen_holes env sigma t n [] in let ans = applist (ans, holes) in - let evdref = ref sigma in - let () = Typing.e_check env evdref ans concl in - (!evdref, ans) + let sigma = Typing.check env sigma ans concl in + (sigma, ans) end end diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8da0e1c4f2..44fa0740d5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -243,7 +243,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in + let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in if not (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp sigma t) then nochange "not an equality"; @@ -1051,7 +1051,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in evd:=evd'; - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in + evd := sigma; res in let nb_intro_to_do = nb_prod (project g) (pf_concl g) in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 04a23cdb97..dc0f240bd6 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -291,7 +291,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in + evd := sigma; let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof @@ -630,7 +631,8 @@ let build_scheme fas = in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in + evd := sigma; let c, u = try EConstr.destConst !evd f with DestKO -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 7df57b5779..efbd029e48 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -385,7 +385,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let evd = ref (Evd.from_env env) in let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in - let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in + let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in + evd := sigma; let princ_type = EConstr.Unsafe.to_constr princ_type in Functional_principles_types.generate_functional_principle evd diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 28e85268a3..094f54156b 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -103,7 +103,8 @@ let generate_type evd g_to_f f graph i = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph))) in evd:=evd'; - let graph_arity = Typing.e_type_of (Global.env ()) evd graph in + let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in + evd := sigma; let ctxt,_ = decompose_prod_assum !evd graph_arity in let fun_ctxt,res_type = match ctxt with @@ -769,7 +770,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in + let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in + evd := sigma; let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 9382f567b4..fb6be430fc 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -85,9 +85,7 @@ let let_evar name typ = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let sigma = ref sigma in - let _ = Typing.e_sort_of env sigma typ in - let sigma = !sigma in + let sigma, _ = Typing.sort_of env sigma typ in let id = match name with | Name.Anonymous -> let id = Namegen.id_of_name_using_hdchar env sigma typ name in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9eb55aa5e5..1b86583da1 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -104,9 +104,8 @@ let extends_undefined evars evars' = let app_poly_check env evars f args = let (evars, cstrs), fc = f evars in - let evdref = ref evars in - let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in - (!evdref, cstrs), t + let evars, t = Typing.solve_evars env evars (mkApp (fc, args)) in + (evars, cstrs), t let app_poly_nocheck env evars f args = let evars, fc = f evars in @@ -1469,8 +1468,8 @@ exception RewriteFailure of Pp.t type result = (evar_map * constr option * types) option option let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result = + let sigma, sort = Typing.sort_of env sigma concl in let evdref = ref sigma in - let sort = Typing.e_sort_of env evdref concl in let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 84049d4ed5..a93cf5ae7c 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -691,11 +691,9 @@ let interp_may_eval f ist env sigma = function let (sigma,ic) = f ist env sigma c in let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in let ctxt = EConstr.Unsafe.to_constr ctxt in - let evdref = ref sigma in - let ic = EConstr.Unsafe.to_constr ic in + let ic = EConstr.Unsafe.to_constr ic in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in - let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in - !evdref , c + Typing.solve_evars env sigma (EConstr.of_constr c) with | Not_found -> user_err ?loc ~hdr:"interp_may_eval" diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 5facf2a808..074fcb92e8 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -247,9 +247,10 @@ let coq_nil = coq_reference "nil" let lapp f args = mkApp(Lazy.force f,args) -let plapp evd f args = - let fc = Evarutil.e_new_global evd (Lazy.force f) in - mkApp(fc,args) +let plapp evdref f args = + let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in + evdref := evd; + mkApp(fc,args) let dest_rel0 sigma t = match EConstr.kind sigma t with @@ -504,10 +505,12 @@ let ring_equality env evd (r,add,mul,opp,req) = let op_morph = match opp with Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] - | None -> plapp evd coq_eq_smorph [|r;add;mul|] in - let setoid = Typing.e_solve_evars env evd setoid in - let op_morph = Typing.e_solve_evars env evd op_morph in - (setoid,op_morph) + | None -> plapp evd coq_eq_smorph [|r;add;mul|] in + let sigma = !evd in + let sigma, setoid = Typing.solve_evars env sigma setoid in + let sigma, op_morph = Typing.solve_evars env sigma op_morph in + evd := sigma; + (setoid,op_morph) | _ -> let setoid = setoid_of_relation (Global.env ()) evd r req in let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in @@ -586,48 +589,53 @@ let make_hyp env evd c = let t = Retyping.get_type_of env !evd c in plapp evd coq_mkhypo [|t;c|] -let make_hyp_list env evd lH = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in +let make_hyp_list env evdref lH = + let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in + evdref := evd; let l = List.fold_right - (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH - (plapp evd coq_nil [|carrier|]) + (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH + (plapp evdref coq_nil [|carrier|]) in - let l' = Typing.e_solve_evars env evd l in + let sigma, l' = Typing.solve_evars env !evdref l in + evdref := sigma; let l' = EConstr.Unsafe.to_constr l' in - Evarutil.nf_evars_universes !evd l' + Evarutil.nf_evars_universes !evdref l' -let interp_power env evd pow = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in +let interp_power env evdref pow = + let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in + evdref := evd; match pow with | None -> let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in - (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|]) + (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evdref coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with | CstTac t -> Tacintern.glob_tactic t | Closed lc -> closed_term_ast (List.map Smartlocate.global_with_alias lc) in - let spec = make_hyp env evd (ic_unsafe spec) in - (tac, plapp evd coq_Some [|carrier; spec|]) + let spec = make_hyp env evdref (ic_unsafe spec) in + (tac, plapp evdref coq_Some [|carrier; spec|]) -let interp_sign env evd sign = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in +let interp_sign env evdref sign = + let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in + evdref := evd; match sign with - | None -> plapp evd coq_None [|carrier|] + | None -> plapp evdref coq_None [|carrier|] | Some spec -> - let spec = make_hyp env evd (ic_unsafe spec) in - plapp evd coq_Some [|carrier;spec|] + let spec = make_hyp env evdref (ic_unsafe spec) in + plapp evdref coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let interp_div env evd div = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in +let interp_div env evdref div = + let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in + evdref := evd; match div with - | None -> plapp evd coq_None [|carrier|] + | None -> plapp evdref coq_None [|carrier|] | Some spec -> - let spec = make_hyp env evd (ic_unsafe spec) in - plapp evd coq_Some [|carrier;spec|] + let spec = make_hyp env evdref (ic_unsafe spec) in + plapp evdref coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div = @@ -728,7 +736,9 @@ let make_term_list env evd carrier rl = let l = List.fold_right (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl (plapp evd coq_nil [|carrier|]) - in Typing.e_solve_evars env evd l + in + let sigma, l = Typing.solve_evars env !evd l in + evd := sigma; l let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c) let tacarg expr = diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 6e17e8e158..c6beb08c5e 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -184,9 +184,7 @@ let havetac ist let gs = List.map (fun (_,a) -> Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in - let tacopen_skols gl = - let stuff, g = Refiner.unpackage gl in - Refiner.repackage stuff (gs @ [g]) in + let tacopen_skols gl = re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma in let gl, ty = pf_e_type_of gl t in gl, ty, Proofview.V82.of_tactic (Tactics.apply t), id, Tacticals.tclTHEN (Tacticals.tclTHEN itac_c simpltac) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 9cc4f5cece..937e68b065 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -32,9 +32,8 @@ let get_index = function ArgArg i -> i | _ -> let tclPERM perm tac gls = let subgls = tac gls in - let sigma, subgll = Refiner.unpackage subgls in - let subgll' = perm subgll in - Refiner.repackage sigma subgll' + let subgll' = perm subgls.Evd.it in + re_sig subgll' subgls.Evd.sigma let rot_hyps dir i hyps = let n = List.length hyps in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a10437a638..0dd3625ba2 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1099,15 +1099,14 @@ let thin id sigma goal = let ids = Id.Set.singleton id in let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in - let evdref = ref (Evd.clear_metas sigma) in + let sigma = Evd.clear_metas sigma in let ans = - try Some (Evarutil.clear_hyps_in_evi env evdref (Environ.named_context_val env) cl ids) + try Some (Evarutil.clear_hyps_in_evi env sigma (Environ.named_context_val env) cl ids) with Evarutil.ClearDependencyError _ -> None in match ans with | None -> sigma - | Some (hyps, concl) -> - let sigma = !evdref in + | Some (sigma, hyps, concl) -> let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in sigma diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4c87b4e7ed..ee7c39982b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -295,8 +295,11 @@ let inductive_template evdref env tmloc ind = | LocalAssum (na,ty) -> let ty = EConstr.of_constr ty in let ty' = substl subst ty in - let e = e_new_evar env evdref ~src:(hole_source n) ty' in - (e::subst,e::evarl,n+1) + let e = evd_comb1 + (Evarutil.new_evar env ~src:(hole_source n)) + evdref ty' + in + (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> let b = EConstr.of_constr b in (substl subst b::subst,evarl,n+1)) @@ -314,13 +317,15 @@ let try_find_ind env sigma typ realnames = IsInd (typ,ind,names) let inh_coerce_to_ind evdref env loc ty tyi = - let sigma = !evdref in + let orig = !evdref in let expected_typ = inductive_template evdref env loc tyi in (* Try to refine the type with inductive information coming from the constructor and renounce if not able to give more information *) (* devrait être indifférent d'exiger leq ou pas puisque pour un inductif cela doit être égal *) - if not (e_cumul env evdref expected_typ ty) then evdref := sigma + match cumul env !evdref expected_typ ty with + | Some sigma -> evdref := sigma + | None -> evdref := orig let binding_vars_of_inductive sigma = function | NotInd _ -> [] @@ -372,8 +377,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref !lvar tomatch in - let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in - evdref := evd; + let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in let typ = nf_evar !evdref j.uj_type in lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; let t = @@ -396,12 +400,8 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = (* Utils *) let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = - let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e - -let evd_comb2 f evdref x y = - let (evd',y) = f !evdref x y in - evdref := evd'; - y + let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in + e let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (* Ideally, we could find a common inductive type to which both the @@ -424,7 +424,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let current = if List.is_empty deps && isEvar !(pb.evdref) typ then (* Don't insert coercions if dependent; only solve evars *) - let _ = e_cumul pb.env pb.evdref indt typ in + let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in current else (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env) @@ -1014,8 +1014,8 @@ let adjust_impossible_cases pb pred tomatch submat = begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin - let evd, default = use_unit_judge !(pb.evdref) in - pb.evdref := Evd.define evk default.uj_type evd + let default = evd_comb0 use_unit_judge pb.evdref in + pb.evdref := Evd.define evk default.uj_type !(pb.evdref) end; add_assert_false_case pb tomatch | _ -> @@ -1681,7 +1681,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ev' = e_new_evar env evdref ~src ty in + let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1712,7 +1712,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in - let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in + let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in lift k ev in aux (0,extenv,subst0) t0 @@ -1724,17 +1724,20 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = we are in an impossible branch *) let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context tycon_env) in - let impossible_case_type, u = - e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in - (lift (n'-n) impossible_case_type, mkSort u) + let impossible_case_type, u = + evd_comb1 + (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase)) + evdref univ_flexible_alg + in + (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in - let evd,tt = Typing.type_of extenv !evdref t in - evdref := evd; + let tt = evd_comb1 (Typing.type_of extenv) evdref t in (t,tt) in - let b = e_cumul env evdref tt (mkSort s) (* side effect *) in - if not b then anomaly (Pp.str "Build_tycon: should be a type."); - { uj_val = t; uj_type = tt } + match cumul env !evdref tt (mkSort s) with + | None -> anomaly (Pp.str "Build_tycon: should be a type."); + | Some sigma -> evdref := sigma; + { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return @@ -1923,9 +1926,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc env evdref j tycon = match tycon with | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in - evdref := evd'; - j + evd_comb2 (Coercion.inh_conv_coerce_to ?loc true env) evdref j p | None -> j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 6dc3687a0a..c9c2445a73 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -48,31 +48,35 @@ exception NoCoercion exception NoCoercionNoUnifier of evar_map * unification_error (* Here, funj is a coercion therefore already typed in global context *) -let apply_coercion_args env evd check isproj argl funj = - let evdref = ref evd in - let rec apply_rec acc typ = function +let apply_coercion_args env sigma check isproj argl funj = + let rec apply_rec sigma acc typ = function | [] -> if isproj then - let cst = fst (destConst !evdref (j_val funj)) in + let cst = fst (destConst sigma (j_val funj)) in let p = Projection.make cst false in let pb = lookup_projection p env in let args = List.skipn pb.Declarations.proj_npars argl in let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in - { uj_val = applist (mkProj (p, hd), tl); - uj_type = typ } + sigma, { uj_val = applist (mkProj (p, hd), tl); + uj_type = typ } else - { uj_val = applist (j_val funj,argl); - uj_type = typ } + sigma, { uj_val = applist (j_val funj,argl); + uj_type = typ } | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) - match EConstr.kind !evdref (whd_all env !evdref typ) with + match EConstr.kind sigma (whd_all env sigma typ) with | Prod (_,c1,c2) -> - if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then - raise NoCoercion; - apply_rec (h::acc) (subst1 h c2) restl + let sigma = + if check then + begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with + | None -> raise NoCoercion + | Some sigma -> sigma + end + else sigma + in + apply_rec sigma (h::acc) (subst1 h c2) restl | _ -> anomaly (Pp.str "apply_coercion_args.") in - let res = apply_rec [] funj.uj_type argl in - !evdref, res + apply_rec sigma [] funj.uj_type argl (* appliquer le chemin de coercions de patterns p *) let apply_pattern_coercion ?loc pat p = @@ -94,7 +98,9 @@ open Program let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in - Evarutil.e_new_evar env evdref ~src c + let evd, v = Evarutil.new_evar env !evdref ~src c in + evdref := evd; + v let app_opt env evdref f t = whd_betaiota !evdref (app_opt f t) @@ -191,7 +197,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some (fun x -> let term = co x in - Typing.e_solve_evars env evdref term) + let sigma, term = Typing.solve_evars env !evdref term in + evdref := sigma; term) in if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then (* Second-order unification needed. *) @@ -337,8 +344,9 @@ let app_coercion env evdref coercion v = match coercion with | None -> v | Some f -> - let v' = Typing.e_solve_evars env evdref (f v) in - whd_betaiota !evdref v' + let sigma, v' = Typing.solve_evars env !evdref (f v) in + evdref := sigma; + whd_betaiota !evdref v' let coerce_itf ?loc env evd v t c1 = let evdref = ref evd in diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index b4e1a1b102..0ff6a330f6 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -20,7 +20,6 @@ open EConstr open Vars open Pattern open Patternops -open Misctypes open Context.Rel.Declaration open Ltac_pretype (*i*) @@ -277,6 +276,7 @@ let matches_core env sigma allow_bound_rels | PSort ps, Sort s -> + let open Glob_term in begin match ps, ESorts.kind sigma s with | GProp, Prop Null -> subst | GSet, Prop Pos -> subst diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml index fda31756a9..1443dfb513 100644 --- a/pretyping/constrexpr.ml +++ b/pretyping/constrexpr.ml @@ -17,7 +17,7 @@ open Decl_kinds (** [constr_expr] is the abstract syntax tree produced by the parser *) -type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl +type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option @@ -50,7 +50,7 @@ type prim_token = | Numeral of raw_natural_number * sign | String of string -type instance_expr = Misctypes.glob_level list +type instance_expr = Glob_term.glob_level list type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname @@ -98,7 +98,7 @@ and constr_expr_r = | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of patvar | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list - | CSort of glob_sort + | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr cast_type | CNotation of notation * constr_notation_substitution | CGeneralization of binding_kind * abstraction_kind option * constr_expr diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 817b8ba6e8..5310455fe6 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -14,7 +14,6 @@ open EConstr open Glob_term open Termops open Mod_subst -open Misctypes open Evd open Ltac_pretype diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 144166a343..49c429458a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1159,17 +1159,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let subst = make_subst (ctxt,Array.to_list args,argoccs) in - let evdref = ref evd in - let rhs = set_holes evdref rhs subst in - let evd = !evdref in + let evd, rhs = + let evdref = ref evd in + let rhs = set_holes evdref rhs subst in + !evdref, rhs + in (* We instantiate the evars of which the value is forced by typing *) let evd,rhs = - let evdref = ref evd in - try let c = !solve_evars env_evar evdref rhs in !evdref,c + try !solve_evars env_evar evd rhs with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) - raise (TypingFailed !evdref) in + raise (TypingFailed evd) in let rec abstract_free_holes evd = function | (id,idty,c,_,evsref,_,_)::l -> @@ -1394,6 +1395,16 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) +let make_opt = function + | Success evd -> Some evd + | UnifFailure _ -> None + +let conv env ?(ts=default_transparent_state env) evd t1 t2 = + make_opt(evar_conv_x ts env evd CONV t1 t2) + +let cumul env ?(ts=default_transparent_state env) evd t1 t2 = + make_opt(evar_conv_x ts env evd CUMUL t1 t2) + let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CONV t1 t2 with | Success evd' -> evdref := evd'; true diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 9270d6e3aa..cdf5dd0e50 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -28,7 +28,13 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma (** The same function resolving evars by side-effect and catching the exception *) val e_conv : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool +[@@ocaml.deprecated "Use [Evarconv.conv]"] + val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool +[@@ocaml.deprecated "Use [Evarconv.cumul]"] + +val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option (** {6 Unification heuristics. } *) @@ -63,7 +69,7 @@ val second_order_matching : transparent_state -> env -> evar_map -> (** Declare function to enforce evars resolution by using typing constraints *) -val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit +val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 3c3f75a68e..6ecb479e6f 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -22,6 +22,25 @@ open Misctypes type existential_name = Id.t +(** Sorts *) + +type 'a glob_sort_gen = + | GProp (** representation of [Prop] literal *) + | GSet (** representation of [Set] literal *) + | GType of 'a (** representation of [Type] literal *) + +type 'a universe_kind = + | UAnonymous + | UUnknown + | UNamed of 'a + +type level_info = Libnames.reference universe_kind +type glob_level = level_info glob_sort_gen +type glob_constraint = glob_level * Univ.constraint_type * glob_level + +type sort_info = (Libnames.reference * int) option list +type glob_sort = sort_info glob_sort_gen + (** The kind of patterns that occurs in "match ... with ... end" locs here refers to the ident's location, not whole pat *) diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 0f0af5409e..1b536bfda3 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -29,7 +29,7 @@ let smartmap_cast_type f c = (** Equalities on [glob_sort] *) -let glob_sort_eq g1 g2 = match g1, g2 with +let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true | GType l1, GType l2 -> diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index abe817fe53..1d45045414 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -18,7 +18,7 @@ val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type (** Equalities on [glob_sort] *) -val glob_sort_eq : glob_sort -> glob_sort -> bool +val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool (** Equalities on [intro_pattern_naming] *) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 7dd0954bc4..996a2dc36a 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -30,7 +30,7 @@ type constr_pattern = | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern - | PSort of glob_sort + | PSort of Glob_term.glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of case_info_pattern * constr_pattern * constr_pattern * diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e68a25a873..616ccf0cfb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -245,7 +245,7 @@ let interp_known_level_info ?loc evd = function with Not_found -> user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) -let interp_level_info ?loc evd : Misctypes.level_info -> _ = function +let interp_level_info ?loc evd : level_info -> _ = function | UUnknown -> new_univ_level_variable ?loc univ_rigid evd | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s @@ -499,7 +499,7 @@ let interp_known_glob_level ?loc evd = function | GSet -> Univ.Level.set | GType s -> interp_known_level_info ?loc evd s -let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function +let interp_glob_level ?loc evd : glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set | GType s -> interp_level_info ?loc evd s @@ -674,14 +674,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in let nbfix = Array.length lar in let names = Array.map (fun id -> Name id) names in - let _ = + let () = match tycon with | Some t -> let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env.ExtraEnv.env evdref ftys.(fixi) t - | None -> true + in + begin match conv env.ExtraEnv.env !evdref ftys.(fixi) t with + | None -> () + | Some sigma -> evdref := sigma + end + | None -> () in (* Note: bodies are not used by push_rec_types, so [||] is safe *) let newenv = push_rec_types !evdref (names,ftys,[||]) env in @@ -698,7 +702,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - Typing.check_type_fixpoint ?loc env.ExtraEnv.env evdref names ftys vdefj; + evdref := Typing.check_type_fixpoint ?loc env.ExtraEnv.env !evdref names ftys vdefj; let nf c = nf_evar !evdref c in let ftys = Array.map nf ftys in (** FIXME *) let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in @@ -793,9 +797,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match candargs with | [] -> [], j_val hj | arg :: args -> - if e_conv env.ExtraEnv.env evdref (j_val hj) arg then - args, nf_evar !evdref (j_val hj) - else [], j_val hj + begin match conv env.ExtraEnv.env !evdref (j_val hj) arg with + | Some sigma -> evdref := sigma; + args, nf_evar !evdref (j_val hj) + | None -> + [], j_val hj + end in let ujval = adjust_evar_source evdref na ujval in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in @@ -1166,10 +1173,12 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D match valcon with | None -> tj | Some v -> - if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj - else + begin match cumul env.ExtraEnv.env !evdref v tj.utj_val with + | Some sigma -> evdref := sigma; tj + | None -> error_unexpected_type ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + end let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env sigma in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 415c4e1722..73f5b77e0e 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -22,7 +22,7 @@ open Ltac_pretype open Evardefine val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> - Misctypes.glob_level -> Univ.Level.t + glob_level -> Univ.Level.t (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/pretyping/program.ml b/pretyping/program.ml index 52d940d8eb..8cfb7966cb 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -16,7 +16,9 @@ let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = let open EConstr in let gr = delayed_force r in - mkApp (Evarutil.e_new_global evdref gr, args) + let evd, hd = Evarutil.new_global !evdref gr in + evdref := evd; + mkApp (hd, args) let sig_typ = init_reference ["Init"; "Specif"] "sig" let sig_intro = init_reference ["Init"; "Specif"] "exist" diff --git a/pretyping/typing.ml b/pretyping/typing.ml index aaec73f045..6bd75c93d5 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -37,104 +37,115 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl = let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp -let e_type_judgment env evdref j = - match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind !evdref s } +let type_judgment env sigma j = + match EConstr.kind sigma (whd_all env sigma j.uj_type) with + | Sort s -> sigma, {utj_val = j.uj_val; utj_type = ESorts.kind sigma s } | Evar ev -> - let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in - evdref := evd; { utj_val = j.uj_val; utj_type = s } - | _ -> error_not_a_type env !evdref j - -let e_assumption_of_judgment env evdref j = - try (e_type_judgment env evdref j).utj_val + let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in + sigma, { utj_val = j.uj_val; utj_type = s } + | _ -> error_not_a_type env sigma j + +let assumption_of_judgment env sigma j = + try + let sigma, j = type_judgment env sigma j in + sigma, j.utj_val with Type_errors.TypeError _ | PretypeError _ -> - error_assumption env !evdref j + error_assumption env sigma j -let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv = - let rec apply_rec n typ = function +let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv = + let rec apply_rec sigma n typ = function | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = - let ar = inductive_type_knowing_parameters env !evdref ind argjv in - hnf_prod_appvect env !evdref (EConstr.of_constr ar) (Array.map j_val argjv) } + sigma, { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = + let ar = inductive_type_knowing_parameters env sigma ind argjv in + hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) } | hj::restjl -> - let (c1,c2) = - match EConstr.kind !evdref (whd_all env !evdref typ) with - | Prod (_,c1,c2) -> (c1,c2) + let sigma, (c1,c2) = + match EConstr.kind sigma (whd_all env sigma typ) with + | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product !evdref ev in - evdref := evd'; - let (_,c1,c2) = destProd evd' t in - (c1,c2) + let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (_,c1,c2) = destProd sigma t in + sigma, (c1,c2) | _ -> - error_cant_apply_not_functional env !evdref funj argjv + error_cant_apply_not_functional env sigma funj argjv in - if Evarconv.e_cumul env evdref hj.uj_type c1 then - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - else - error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv + begin match Evarconv.cumul env sigma hj.uj_type c1 with + | Some sigma -> + apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl + | None -> + error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv + end in - apply_rec 1 funj.uj_type (Array.to_list argjv) + apply_rec sigma 1 funj.uj_type (Array.to_list argjv) -let e_judge_of_apply env evdref funj argjv = - let rec apply_rec n typ = function +let judge_of_apply env sigma funj argjv = + let rec apply_rec sigma n typ = function | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = typ } + sigma, { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = typ } | hj::restjl -> - let (c1,c2) = - match EConstr.kind !evdref (whd_all env !evdref typ) with - | Prod (_,c1,c2) -> (c1,c2) + let sigma, (c1,c2) = + match EConstr.kind sigma (whd_all env sigma typ) with + | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product !evdref ev in - evdref := evd'; - let (_,c1,c2) = destProd evd' t in - (c1,c2) + let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (_,c1,c2) = destProd sigma t in + sigma, (c1,c2) | _ -> - error_cant_apply_not_functional env !evdref funj argjv + error_cant_apply_not_functional env sigma funj argjv in - if Evarconv.e_cumul env evdref hj.uj_type c1 then - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - else - error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv + begin match Evarconv.cumul env sigma hj.uj_type c1 with + | Some sigma -> + apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl + | None -> + error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv + end in - apply_rec 1 funj.uj_type (Array.to_list argjv) + apply_rec sigma 1 funj.uj_type (Array.to_list argjv) -let e_check_branch_types env evdref (ind,u) cj (lfj,explft) = +let check_branch_types env sigma (ind,u) cj (lfj,explft) = if not (Int.equal (Array.length lfj) (Array.length explft)) then - error_number_branches env !evdref cj (Array.length explft); - for i = 0 to Array.length explft - 1 do - if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then - error_ill_formed_branch env !evdref cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) - done + error_number_branches env sigma cj (Array.length explft); + Array.fold_left2_i (fun i sigma lfj explft -> + match Evarconv.cumul env sigma lfj.uj_type explft with + | Some sigma -> sigma + | None -> + error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft) + sigma lfj explft let max_sort l = if Sorts.List.mem InType l then InType else if Sorts.List.mem InSet l then InSet else InProp -let e_is_correct_arity env evdref c pj ind specif params = - let arsign = make_arity_signature env !evdref true (make_ind_family (ind,params)) in +let is_correct_arity env sigma c pj ind specif params = + let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in let allowed_sorts = elim_sorts specif in - let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in - let rec srec env pt ar = - let pt' = whd_all env !evdref pt in - match EConstr.kind !evdref pt', ar with + let error () = Pretype_errors.error_elim_arity env sigma ind allowed_sorts c pj None in + let rec srec env sigma pt ar = + let pt' = whd_all env sigma pt in + match EConstr.kind sigma pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - if not (Evarconv.e_cumul env evdref a1 a1') then error (); - srec (push_rel (LocalAssum (na1,a1)) env) t ar' + begin match Evarconv.cumul env sigma a1 a1' with + | None -> error () + | Some sigma -> + srec (push_rel (LocalAssum (na1,a1)) env) sigma t ar' + end | Sort s, [] -> - let s = ESorts.kind !evdref s in + let s = ESorts.kind sigma s in if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () + else sigma | Evar (ev,_), [] -> - let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in - evdref := Evd.define ev (mkSort s) evd + let sigma, s = Evd.fresh_sort_in_family env sigma (max_sort allowed_sorts) in + let sigma = Evd.define ev (mkSort s) sigma in + sigma | _, (LocalDef _ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' + srec (push_rel d env) sigma (lift 1 pt') ar' | _ -> error () in - srec env pj.uj_type (List.rev arsign) + srec env sigma pj.uj_type (List.rev arsign) let lambda_applist_assum sigma n c l = let rec app n subst t l = @@ -147,39 +158,41 @@ let lambda_applist_assum sigma n c l = | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l -let e_type_case_branches env evdref (ind,largs) pj c = +let type_case_branches env sigma (ind,largs) pj c = let specif = lookup_mind_specif env (fst ind) in let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in let params = List.map EConstr.Unsafe.to_constr params in - let () = e_is_correct_arity env evdref c pj ind specif params in - let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false !evdref p) in + let sigma = is_correct_arity env sigma c pj ind specif params in + let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in - let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in - (lc, ty) + let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in + sigma, (lc, ty) -let e_judge_of_case env evdref ci pj cj lfj = +let judge_of_case env sigma ci pj cj lfj = let ((ind, u), spec) = - try find_mrectype env !evdref cj.uj_type - with Not_found -> error_case_not_inductive env !evdref cj in - let indspec = ((ind, EInstance.kind !evdref u), spec) in + try find_mrectype env sigma cj.uj_type + with Not_found -> error_case_not_inductive env sigma cj in + let indspec = ((ind, EInstance.kind sigma u), spec) in let _ = check_case_info env (fst indspec) ci in - let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in - e_check_branch_types env evdref (fst indspec) cj (lfj,bty); - { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); - uj_type = rslty } + let sigma, (bty,rslty) = type_case_branches env sigma indspec pj cj.uj_val in + let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in + sigma, { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); + uj_type = rslty } -let check_type_fixpoint ?loc env evdref lna lar vdefj = +let check_type_fixpoint ?loc env sigma lna lar vdefj = let lt = Array.length vdefj in - if Int.equal (Array.length lar) lt then - for i = 0 to lt-1 do - if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body ?loc env !evdref - i lna vdefj lar - done + assert (Int.equal (Array.length lar) lt); + Array.fold_left2_i (fun i sigma defj ar -> + match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with + | Some sigma -> sigma + | None -> + error_ill_typed_rec_body ?loc env sigma + i lna vdefj lar) + sigma vdefj lar + (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = @@ -192,17 +205,19 @@ let check_allowed_sort env sigma ind c p = error_elim_arity env sigma ind sorts c pj (Some(ksort,s,Type_errors.error_elim_explain ksort s)) -let e_judge_of_cast env evdref cj k tj = +let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in - if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then - error_actual_type_core env !evdref cj expected_type; - { uj_val = mkCast (cj.uj_val, k, expected_type); - uj_type = expected_type } - -let enrich_env env evdref = + match Evarconv.cumul env sigma cj.uj_type expected_type with + | None -> + error_actual_type_core env sigma cj expected_type; + | Some sigma -> + sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); + uj_type = expected_type } + +let enrich_env env sigma = let penv = Environ.pre_env env in let penv' = Pre_env.({ penv with env_stratification = - { penv.env_stratification with env_universes = Evd.universes !evdref } }) in + { penv.env_stratification with env_universes = Evd.universes sigma } }) in Environ.env_of_pre_env penv' let check_fix env sigma pfix = @@ -267,165 +282,167 @@ let judge_of_letin env name defj typj j = (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) -let rec execute env evdref cstr = - let cstr = whd_evar !evdref cstr in - match EConstr.kind !evdref cstr with +let rec execute env sigma cstr = + let cstr = whd_evar sigma cstr in + match EConstr.kind sigma cstr with | Meta n -> - { uj_val = cstr; uj_type = meta_type !evdref n } + sigma, { uj_val = cstr; uj_type = meta_type sigma n } | Evar ev -> - let ty = EConstr.existential_type !evdref ev in - let jty = execute env evdref ty in - let jty = e_assumption_of_judgment env evdref jty in - { uj_val = cstr; uj_type = jty } + let ty = EConstr.existential_type sigma ev in + let sigma, jty = execute env sigma ty in + let sigma, jty = assumption_of_judgment env sigma jty in + sigma, { uj_val = cstr; uj_type = jty } | Rel n -> - judge_of_relative env n + sigma, judge_of_relative env n | Var id -> - judge_of_variable env id + sigma, judge_of_variable env id | Const (c, u) -> - let u = EInstance.kind !evdref u in - make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u))) + let u = EInstance.kind sigma u in + sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u))) | Ind (ind, u) -> - let u = EInstance.kind !evdref u in - make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u))) + let u = EInstance.kind sigma u in + sigma, make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u))) | Construct (cstruct, u) -> - let u = EInstance.kind !evdref u in - make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u))) + let u = EInstance.kind sigma u in + sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u))) | Case (ci,p,c,lf) -> - let cj = execute env evdref c in - let pj = execute env evdref p in - let lfj = execute_array env evdref lf in - e_judge_of_case env evdref ci pj cj lfj + let sigma, cj = execute env sigma c in + let sigma, pj = execute env sigma p in + let sigma, lfj = execute_array env sigma lf in + judge_of_case env sigma ci pj cj lfj | Fix ((vn,i as vni),recdef) -> - let (_,tys,_ as recdef') = execute_recdef env evdref recdef in + let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in let fix = (vni,recdef') in - check_fix env !evdref fix; - make_judge (mkFix fix) tys.(i) + check_fix env sigma fix; + sigma, make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_recdef env evdref recdef in + let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in let cofix = (i,recdef') in - check_cofix env !evdref cofix; - make_judge (mkCoFix cofix) tys.(i) + check_cofix env sigma cofix; + sigma, make_judge (mkCoFix cofix) tys.(i) | Sort s -> - begin match ESorts.kind !evdref s with + begin match ESorts.kind sigma s with | Prop c -> - judge_of_prop_contents c + sigma, judge_of_prop_contents c | Type u -> - judge_of_type u + sigma, judge_of_type u end | Proj (p, c) -> - let cj = execute env evdref c in - judge_of_projection env !evdref p cj + let sigma, cj = execute env sigma c in + sigma, judge_of_projection env sigma p cj | App (f,args) -> - let jl = execute_array env evdref args in - (match EConstr.kind !evdref f with + let sigma, jl = execute_array env sigma args in + (match EConstr.kind sigma f with | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> - let fj = execute env evdref f in - e_judge_of_applied_inductive_knowing_parameters env evdref fj (ind, u) jl + let sigma, fj = execute env sigma f in + judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl | _ -> (* No template polymorphism *) - let fj = execute env evdref f in - e_judge_of_apply env evdref fj jl) + let sigma, fj = execute env sigma f in + judge_of_apply env sigma fj jl) | Lambda (name,c1,c2) -> - let j = execute env evdref c1 in - let var = e_type_judgment env evdref j in + let sigma, j = execute env sigma c1 in + let sigma, var = type_judgment env sigma j in let env1 = push_rel (LocalAssum (name, var.utj_val)) env in - let j' = execute env1 evdref c2 in - judge_of_abstraction env1 name var j' + let sigma, j' = execute env1 sigma c2 in + sigma, judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> - let j = execute env evdref c1 in - let varj = e_type_judgment env evdref j in + let sigma, j = execute env sigma c1 in + let sigma, varj = type_judgment env sigma j in let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in - let j' = execute env1 evdref c2 in - let varj' = e_type_judgment env1 evdref j' in - judge_of_product env name varj varj' + let sigma, j' = execute env1 sigma c2 in + let sigma, varj' = type_judgment env1 sigma j' in + sigma, judge_of_product env name varj varj' | LetIn (name,c1,c2,c3) -> - let j1 = execute env evdref c1 in - let j2 = execute env evdref c2 in - let j2 = e_type_judgment env evdref j2 in - let _ = e_judge_of_cast env evdref j1 DEFAULTcast j2 in + let sigma, j1 = execute env sigma c1 in + let sigma, j2 = execute env sigma c2 in + let sigma, j2 = type_judgment env sigma j2 in + let sigma, _ = judge_of_cast env sigma j1 DEFAULTcast j2 in let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in - let j3 = execute env1 evdref c3 in - judge_of_letin env name j1 j2 j3 + let sigma, j3 = execute env1 sigma c3 in + sigma, judge_of_letin env name j1 j2 j3 | Cast (c,k,t) -> - let cj = execute env evdref c in - let tj = execute env evdref t in - let tj = e_type_judgment env evdref tj in - e_judge_of_cast env evdref cj k tj - -and execute_recdef env evdref (names,lar,vdef) = - let larj = execute_array env evdref lar in - let lara = Array.map (e_assumption_of_judgment env evdref) larj in + let sigma, cj = execute env sigma c in + let sigma, tj = execute env sigma t in + let sigma, tj = type_judgment env sigma tj in + judge_of_cast env sigma cj k tj + +and execute_recdef env sigma (names,lar,vdef) = + let sigma, larj = execute_array env sigma lar in + let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array env1 evdref vdef in + let sigma, vdefj = execute_array env1 sigma vdef in let vdefv = Array.map j_val vdefj in - let _ = check_type_fixpoint env1 evdref names lara vdefj in - (names,lara,vdefv) + let sigma = check_type_fixpoint env1 sigma names lara vdefj in + sigma, (names,lara,vdefv) -and execute_array env evdref = Array.map (execute env evdref) +and execute_array env = Array.fold_left_map (execute env) + +let check env sigma c t = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in + match Evarconv.cumul env sigma j.uj_type t with + | None -> + error_actual_type_core env sigma j t + | Some sigma -> sigma let e_check env evdref c t = - let env = enrich_env env evdref in - let j = execute env evdref c in - if not (Evarconv.e_cumul env evdref j.uj_type t) then - error_actual_type_core env !evdref j t + evdref := check env !evdref c t (* Type of a constr *) -let unsafe_type_of env evd c = - let evdref = ref evd in - let env = enrich_env env evdref in - let j = execute env evdref c in - j.uj_type +let unsafe_type_of env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in + j.uj_type (* Sort of a type *) +let sort_of env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in + let sigma, a = type_judgment env sigma j in + sigma, a.utj_type + let e_sort_of env evdref c = - let env = enrich_env env evdref in - let j = execute env evdref c in - let a = e_type_judgment env evdref j in - a.utj_type + Evarutil.evd_comb1 (sort_of env) evdref c (* Try to solve the existential variables by typing *) -let type_of ?(refresh=false) env evd c = - let evdref = ref evd in - let env = enrich_env env evdref in - let j = execute env evdref c in +let type_of ?(refresh=false) env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type - else !evdref, j.uj_type + Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma j.uj_type + else sigma, j.uj_type + +let e_type_of ?refresh env evdref c = + Evarutil.evd_comb1 (type_of ?refresh env) evdref c -let e_type_of ?(refresh=false) env evdref c = - let env = enrich_env env evdref in - let j = execute env evdref c in +let solve_evars env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in (* side-effect on evdref *) - if refresh then - let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in - let () = evdref := evd in - c - else j.uj_type + sigma, nf_evar sigma j.uj_val let e_solve_evars env evdref c = - let env = enrich_env env evdref in - let c = (execute env evdref c).uj_val in - (* side-effect on evdref *) - nf_evar !evdref c + Evarutil.evd_comb1 (solve_evars env) evdref c -let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c) +let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 4905adf1f3..3cf43ace01 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -26,18 +26,25 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types (** Variant of [type_of] using references instead of state-passing. *) val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types +[@@ocaml.deprecated "Use [Typing.type_of]"] (** Typecheck a type and return its sort *) +val sort_of : env -> evar_map -> types -> evar_map * Sorts.t val e_sort_of : env -> evar_map ref -> types -> Sorts.t +[@@ocaml.deprecated "Use [Typing.sort_of]"] (** Typecheck a term has a given type (assuming the type is OK) *) +val check : env -> evar_map -> constr -> types -> evar_map val e_check : env -> evar_map ref -> constr -> types -> unit +[@@ocaml.deprecated "Use [Typing.check]"] (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) +val solve_evars : env -> evar_map -> constr -> evar_map * constr val e_solve_evars : env -> evar_map ref -> constr -> constr +[@@ocaml.deprecated "Use [Typing.solve_evars]"] (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) @@ -46,8 +53,8 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> (** Raise an error message if bodies have types not unifiable with the expected ones *) -val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ref -> - Names.Name.t array -> types array -> unsafe_judgment array -> unit +val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map -> + Names.Name.t array -> types array -> unsafe_judgment array -> evar_map val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d98ce9abab..1caa629ffb 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -198,8 +198,8 @@ let pose_all_metas_as_evars env evd t = then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in - let ev = Evarutil.e_new_evar env evdref ~src ty in - evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; + let evd, ev = Evarutil.new_evar env !evdref ~src ty in + evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd; ev) | _ -> EConstr.map !evdref aux t in diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml index 3a49d6cf83..e15c3ad042 100644 --- a/pretyping/vernacexpr.ml +++ b/pretyping/vernacexpr.ml @@ -338,7 +338,7 @@ type nonrec vernac_expr = | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list - | VernacConstraint of glob_constraint list + | VernacConstraint of Glob_term.glob_constraint list (* Gallina extensions *) | VernacBeginSection of lident diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 412a1cbb41..60268c9de6 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -170,13 +170,13 @@ let tag_var = tag Tag.variable let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" - let pr_glob_sort = function + let pr_glob_sort = let open Glob_term in function | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType [] -> tag_type (str "Type") | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) - let pr_glob_level = function + let pr_glob_level = let open Glob_term in function | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType UUnknown -> tag_type (str "Type") @@ -199,7 +199,7 @@ let tag_var = tag Tag.variable let pr_qualid = pr_qualid let pr_patvar = pr_id - let pr_glob_sort_instance = function + let pr_glob_sort_instance = let open Glob_term in function | GProp -> tag_type (str "Prop") | GSet -> diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 1f1308b0df..127c4471cd 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -41,8 +41,8 @@ val pr_name : Name.t -> Pp.t val pr_qualid : qualid -> Pp.t val pr_patvar : patvar -> Pp.t -val pr_glob_level : glob_level -> Pp.t -val pr_glob_sort : glob_sort -> Pp.t +val pr_glob_level : Glob_term.glob_level -> Pp.t +val pr_glob_sort : Glob_term.glob_sort -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> lident option * recursion_order_expr -> diff --git a/proofs/refine.ml b/proofs/refine.ml index 5a2d82977e..b64e7a2e5e 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -30,26 +30,19 @@ let typecheck_evar ev env sigma = (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = let t = NamedDecl.get_type decl in - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref t in - let () = match decl with - | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.e_check env evdref body t + let sigma, _ = Typing.sort_of env sigma t in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,body,_) -> Typing.check env sigma body t in - (!evdref, EConstr.push_named decl env) + (sigma, EConstr.push_named decl env) in let (common, changed) = extract_prefix env info in let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in - !evdref - -let typecheck_proof c concl env sigma = - let evdref = ref sigma in - let () = Typing.e_check env evdref c concl in - !evdref + let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in + sigma let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () @@ -93,7 +86,7 @@ let generic_refine ~typecheck f gl = let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in (** Check that the refined term is typesafe *) - let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in + let sigma = if typecheck then Typing.check env sigma c concl else sigma in (** Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 5cd703a25c..0f83e16ec8 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -23,9 +23,12 @@ val pf_env : goal sigma -> Environ.env val pf_hyps : goal sigma -> named_context val unpackage : 'a sigma -> evar_map ref * 'a +[@@ocaml.deprecated "Do not use [evar_map ref]"] val repackage : evar_map ref -> 'a -> 'a sigma +[@@ocaml.deprecated "Do not use [evar_map ref]"] val apply_sig_tac : evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list +[@@ocaml.deprecated "Do not use [evar_map ref]"] val refiner : rule -> tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 1889054f86..c1d69dfc54 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -33,9 +33,11 @@ let re_sig it gc = { it = it; sigma = gc; } type 'a sigma = 'a Evd.sigma;; type tactic = Proof_type.tactic;; +[@@@ocaml.warning "-3"] let unpackage = Refiner.unpackage let repackage = Refiner.repackage let apply_sig_tac = Refiner.apply_sig_tac +[@@@ocaml.warning "+3"] let sig_it = Refiner.sig_it let project = Refiner.project diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index de96f85104..31496fb3d5 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -30,9 +30,12 @@ val project : goal sigma -> evar_map val re_sig : 'a -> evar_map -> 'a sigma val unpackage : 'a sigma -> evar_map ref * 'a +[@@ocaml.deprecated "Do not use [evar_map ref]"] val repackage : evar_map ref -> 'a -> 'a sigma +[@@ocaml.deprecated "Do not use [evar_map ref]"] val apply_sig_tac : evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list) +[@@ocaml.deprecated "Do not use [evar_map ref]"] val pf_concl : goal sigma -> types val pf_env : goal sigma -> env diff --git a/stm/stm.ml b/stm/stm.ml index 9ea6a305ef..20409c25ee 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2113,12 +2113,6 @@ let delegate name = || VCS.is_vio_doc () || !cur_opt.async_proofs_full -let warn_deprecated_nested_proofs = - CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" - (fun () -> - strbrk ("Nested proofs are deprecated and will "^ - "stop working in a future Coq version")) - let collect_proof keep cur hd brkind id = stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in @@ -2200,8 +2194,7 @@ let collect_proof keep cur hd brkind id = assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in `MaybeASync (parent last, accn, name, delegate name) - | `Sideff _ -> - warn_deprecated_nested_proofs (); + | `Sideff (CherryPickEnv,_) -> `Sync (no_name,`NestedProof) | _ -> `Sync (no_name,`Unknown) in let make_sync why = function @@ -2771,6 +2764,14 @@ let process_back_meta_command ~newtip ~head oid aast w = VCS.commit id (Alias (oid,aast)); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok +let allow_nested_proofs = ref false +let _ = Goptions.declare_bool_option + { Goptions.optdepr = false; + Goptions.optname = "Nested Proofs Allowed"; + Goptions.optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; + Goptions.optread = (fun () -> !allow_nested_proofs); + Goptions.optwrite = (fun b -> allow_nested_proofs := b) } + let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); @@ -2802,6 +2803,15 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Proof *) | VtStartProof (mode, guarantee, names), w -> + + if not !allow_nested_proofs && VCS.proof_nesting () > 0 then + "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." + |> Pp.str + |> (fun s -> (UserError (None, s), Exninfo.null)) + |> State.exn_on ~valid:Stateid.dummy Stateid.dummy + |> Exninfo.iraise + else + let id = VCS.new_node ~id:newtip () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index c08cc6e367..e01dcbcb6e 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -54,13 +54,20 @@ let idents_of_name : Names.Name.t -> Names.Id.t list = | Names.Anonymous -> [] | Names.Name n -> [n] +let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] + +let options_affecting_stm_scheduling = + [ Vernacentries.universe_polymorphism_option_name; + stm_allow_nested_proofs_option_name ] + let classify_vernac e = let static_classifier ~poly e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l)) - when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> + when CList.exists (CList.equal String.equal l) + options_affecting_stm_scheduling -> VtSideff [], VtNow (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index abbc04e895..45fbfb42af 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -25,3 +25,4 @@ val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification val classify_as_proofstep : vernac_classification +val stm_allow_nested_proofs_option_name : string list diff --git a/tactics/eauto.ml b/tactics/eauto.ml index dc310c542d..2408b8f2b2 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -70,11 +70,10 @@ let first_goal gls = (* tactic -> tactic_list : Apply a tactic to the first goal in the list *) let apply_tac_list tac glls = - let (sigr,lg) = unpackage glls in - match lg with + match glls.it with | (g1::rest) -> - let gl = apply_sig_tac sigr tac g1 in - repackage sigr (gl@rest) + let pack = tac (re_sig g1 glls.sigma) in + re_sig (pack.it @ rest) pack.sigma | _ -> user_err Pp.(str "apply_tac_list") let one_step l gl = diff --git a/tactics/equality.ml b/tactics/equality.ml index b6bbd0be45..d142e10a4f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1176,34 +1176,35 @@ let minimal_free_rels_rec env sigma = let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigdata = find_sigma_data env sort_of_ty in - let evdref = ref (Evd.clear_metas sigma) in - let rec sigrec_clausal_form siglen p_i = + let rec sigrec_clausal_form sigma siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) let dflt_typ = unsafe_type_of env sigma dflt in try - let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in - let () = - evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in - dflt + let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in + let sigma = + Evarconv.solve_unif_constraints_with_heuristics env sigma in + sigma, dflt with Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") else - let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with + let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with | (_sigS,[a;p]) -> (a, p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in - let ev = Evarutil.e_new_evar env evdref a in + let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in - let tuple_tail = sigrec_clausal_form (siglen-1) rty in - let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in + let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in + let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in match evopt with | Some w -> - let w_type = unsafe_type_of env !evdref w in - if Evarconv.e_cumul env evdref w_type a then - let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in - applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - else + let w_type = unsafe_type_of env sigma w in + begin match Evarconv.cumul env sigma w_type a with + | Some sigma -> + let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in + sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + | None -> user_err Pp.(str "Cannot solve a unification problem.") + end | None -> (* This at least happens if what has been detected as a dependency is not one; use an evasive error message; @@ -1213,8 +1214,9 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = unsolved evars would mean not binding rel *) user_err Pp.(str "Cannot solve a unification problem.") in - let scf = sigrec_clausal_form siglen ty in - !evdref, Evarutil.nf_evar !evdref scf + let sigma = Evd.clear_metas sigma in + let sigma, scf = sigrec_clausal_form sigma siglen ty in + sigma, Evarutil.nf_evar sigma scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ee76ad077a..01351e2492 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -247,13 +247,12 @@ let clear_gen fail = function let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let evdref = ref sigma in - let (hyps, concl) = - try clear_hyps_in_evi env evdref (named_context_val env) concl ids + let (sigma, hyps, concl) = + try clear_hyps_in_evi env sigma (named_context_val env) concl ids with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal in let env = reset_with_named_context hyps env in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl end) @@ -431,9 +430,8 @@ let get_previous_hyp_position env sigma id = let clear_hyps2 env sigma ids sign t cl = try - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in - (hyps, t, cl, !evdref) + let sigma = Evd.clear_metas sigma in + Evarutil.clear_hyps2_in_evi env sigma sign t cl ids with Evarutil.ClearDependencyError (id,err,inglobal) -> error_replacing_dependency env sigma id err inglobal @@ -447,7 +445,7 @@ let internal_cut_gen ?(check=true) dir replace id t = let sign',t,concl,sigma = if replace then let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in - let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in + let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in sign',t,concl,sigma else @@ -1987,24 +1985,22 @@ let on_the_bodies = function exception DependsOnBody of Id.t option let check_is_type env sigma ty = - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - !evdref + let sigma, _ = Typing.sort_of env sigma ty in + sigma with e when CErrors.noncritical e -> raise (DependsOnBody None) let check_decl env sigma decl = let open Context.Named.Declaration in let ty = NamedDecl.get_type decl in - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - let _ = match decl with - | LocalAssum _ -> () - | LocalDef (_,c,_) -> Typing.e_check env evdref c ty + let sigma, _ = Typing.sort_of env sigma ty in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,c,_) -> Typing.check env sigma c ty in - !evdref + sigma with e when CErrors.noncritical e -> let id = NamedDecl.get_id decl in raise (DependsOnBody (Some id)) @@ -3815,7 +3811,10 @@ let specialize_eqs id = let ty = Tacmach.New.pf_get_hyp_typ id gl in let evars = ref (Proofview.Goal.sigma gl) in let unif env evars c1 c2 = - compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2 + compare_upto_variables !evars c1 c2 && + (match Evarconv.conv env !evars c1 c2 with + | Some sigma -> evars := sigma; true + | None -> false) in let rec aux in_eqs ctx acc ty = match EConstr.kind !evars ty with @@ -3840,7 +3839,8 @@ let specialize_eqs id = | _ -> if in_eqs then acc, in_eqs, ctx, ty else - let e = e_new_evar (push_rel_context ctx env) evars t in + let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in + evars := sigma; aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) | t -> acc, in_eqs, ctx, ty in @@ -4367,7 +4367,7 @@ let check_expected_type env sigma (elimc,bl) elimt = let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in let (_,u,_) = destProd sigma cl.cl_concl in - fun t -> Evarconv.e_cumul env (ref sigma) t u + fun t -> Option.has_some (Evarconv.cumul env sigma t u) let check_enough_applied env sigma elim = (* A heuristic to decide whether the induction arg is enough applied *) diff --git a/test-suite/Makefile b/test-suite/Makefile index 2531b8c678..ce21ff41c3 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -8,9 +8,6 @@ ## # (see LICENSE file for the text of the license) ## ########################################################################## -# This is a standalone Makefile to run the test-suite. It can be used -# outside of the Coq source tree (if BIN is overridden). - # There is one %.v.log target per %.v test file. The target will be # filled with the output, timings and status of the test. There is # also one target per directory containing %.v files, that runs all @@ -23,6 +20,14 @@ # The "run" target runs all tests that have not been run yet. To force # all tests to be run, use the "clean" target. + +########################################################################### +# Includes +########################################################################### + +include ../config/Makefile +include ../Makefile.common + ####################################################################### # Variables ####################################################################### @@ -97,7 +102,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ coqdoc ssr # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-tests PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ @@ -118,13 +123,16 @@ bugs: $(BUGS) clean: rm -f trace .lia.cache output/MExtraction.out - $(SHOW) "RM <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>" + $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>' $(HIDE)find . \( \ - -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ - \) -print0 | xargs -0 rm -f - + -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ + \) -print0 | xargs -0 rm -f + $(SHOW) 'RM <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>' + $(HIDE)find unit-tests \( \ + -name '*.cmx' -o -name '*.cmi' -o -name '*.o' -o -name '*.test' \ + \) -print0 | xargs -0 rm -f distclean: clean - $(SHOW) "RM <**/*.aux>" + $(SHOW) 'RM <**/*.aux>' $(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f ####################################################################### @@ -165,12 +173,13 @@ summary: $(call summary_dir, "Coqwc tests", coqwc); \ $(call summary_dir, "Coq makefile", coq-makefile); \ $(call summary_dir, "Coqdoc tests", coqdoc); \ + $(call summary_dir, "Unit tests", unit-tests); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ nb_tests=`expr $$nb_success + $$nb_failure`; \ - pourcentage=`expr 100 \* $$nb_success / $$nb_tests`; \ + percentage=`expr 100 \* $$nb_success / $$nb_tests`; \ echo; \ - echo "$$nb_success tests passed over $$nb_tests, i.e. $$pourcentage %"; \ + echo "$$nb_success tests passed over $$nb_tests, i.e. $$percentage %"; \ } summary.log: @@ -244,6 +253,44 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v } > "$@" ####################################################################### +# Unit tests +####################################################################### + +OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) +SYSMOD:=-package num,str,unix,dynlink,threads + +COQSRCDIRS:=$(addprefix -I $(LIB)/,$(CORESRCDIRS)) +COQCMXS:=$(addprefix $(LIB)/,$(LINKCMX)) + +# ML files from unit-test framework, not containing tests +UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml) +UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml) +UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES)) +UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES)) + +UNIT_CMXS=utest.cmx + +unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi + $(SHOW) 'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $< +unit-tests/src/utest.cmi: unit-tests/src/utest.mli + $(SHOW) 'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) -package oUnit $< + +$(UNIT_LOGFILES): unit-tests/src/utest.cmx + +unit-tests: $(UNIT_LOGFILES) + +# Build executable, run it to generate log file +unit-tests/%.ml.log: unit-tests/%.ml + $(SHOW) 'TEST $<' + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -cclib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib,oUnit \ + -I unit-tests/src $(COQSRCDIRS) $(COQCMXS) \ + $(UNIT_CMXS) $< -o $<.test; + $(HIDE)./$<.test + +####################################################################### # Other generic tests ####################################################################### diff --git a/test-suite/README.md b/test-suite/README.md index 1d1195646e..4572c98cfe 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -73,3 +73,6 @@ When you fix a bug, you should usually add a regression test here as well. The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile. There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output. + +There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit` +unit-test framework, as described at http://ounit.forge.ocamlcore.org/. Use `make unit-tests' in the unit-tests directory to run them. diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v index a03adbd73c..7b1a261789 100644 --- a/test-suite/bugs/closed/2969.v +++ b/test-suite/bugs/closed/2969.v @@ -12,6 +12,7 @@ eexists. reflexivity. Grab Existential Variables. admit. +Admitted. (* Alternative variant which failed but without raising anomaly *) @@ -24,3 +25,4 @@ clearbody n n0. exact I. Grab Existential Variables. admit. +Admitted. diff --git a/test-suite/bugs/closed/3377.v b/test-suite/bugs/closed/3377.v index 8e9e3933cc..abfcf1d355 100644 --- a/test-suite/bugs/closed/3377.v +++ b/test-suite/bugs/closed/3377.v @@ -5,6 +5,7 @@ Record prod A B := pair { fst : A; snd : B}. Goal fst (@pair Type Type Type Type). Set Printing All. match goal with |- ?f ?x => set (foo := f x) end. +Abort. Goal forall x : prod Set Set, x = @pair _ _ (fst x) (snd x). Proof. @@ -12,6 +13,6 @@ Proof. lazymatch goal with | [ |- ?x = @pair _ _ (?f ?x) (?g ?x) ] => pose f end. - (* Toplevel input, characters 7-44: Error: No matching clauses for match. *) +Abort. diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 606c6e0845..668f6bb428 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -41,6 +41,8 @@ Proof. f_equal. 8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l and skipn n l = l *) +Abort. + Require Import List. Fixpoint replicate {A} (n : nat) (x : A) : list A := match n with 0 => nil | S n => x :: replicate n x end. diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v index eb37141bcf..28800ac05a 100644 --- a/test-suite/bugs/closed/4198.v +++ b/test-suite/bugs/closed/4198.v @@ -13,6 +13,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), match goal with | [ |- context G[@hd] ] => idtac end. +Abort. (* This second example comes from CFGV where inspecting subterms of a match is expecting to inspect first the term to match (even though @@ -35,3 +36,4 @@ Ltac mydestruct := Goal forall x, match x with 0 => 0 | _ => 0 end = 0. intros. mydestruct. +Abort. diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v index dbd71035dc..1e1a4cb9c2 100644 --- a/test-suite/bugs/closed/4782.v +++ b/test-suite/bugs/closed/4782.v @@ -6,6 +6,7 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p. Goal p. Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil. +Abort. (* A simplification of an example from coquelicot, which was failing at some time after a fix #4782 was committed. *) @@ -21,4 +22,5 @@ Set Typeclasses Debug. Goal forall (A:T) (x:dom A), pairT A A = pairT A A. intros. apply (F _ _) with (x,x). +Abort. diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake index b3d1c6d534..c95df1b11c 100644 --- a/test-suite/ide/undo012.fake +++ b/test-suite/ide/undo012.fake @@ -3,6 +3,7 @@ # # Test backtracking in presence of nested proofs # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake index 921a9d0f0d..a3ccefd2ca 100644 --- a/test-suite/ide/undo013.fake +++ b/test-suite/ide/undo013.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Second, trigger the undo of an inner proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake index f5fe774704..13e718229c 100644 --- a/test-suite/ide/undo014.fake +++ b/test-suite/ide/undo014.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Third, undo inside an inner proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake index a1e5c947b3..9cbd64460d 100644 --- a/test-suite/ide/undo015.fake +++ b/test-suite/ide/undo015.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Fourth, undo from an inner proof to a above proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake index f9414c1ea7..15bd3cc92d 100644 --- a/test-suite/ide/undo016.fake +++ b/test-suite/ide/undo016.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Fifth, undo from an inner proof to a previous inner proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index caf3b28701..4740c009a4 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -163,6 +163,7 @@ match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end. match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end. Show. +Abort. Lemma lem5 (p:nat) : eq_refl p = eq_refl p. let y := fresh "n" in (* Checking that y is hidden *) diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 6adbe95dd5..901b1e3aa6 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -37,17 +37,20 @@ Fail g1 I. Fail f1 I. Fail g2 I. Fail f2 I. +Abort. Ltac h x := injection x. Goal True -> False. Fail h I. intro H. Fail h H. +Abort. (* Check printing of the "var" argument "Hx" *) Ltac m H := idtac H; exact H. Goal True. let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. +Abort. (* Check consistency of interpretation scopes (#4398) *) diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index ca8da39482..ee540d7109 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -107,6 +107,7 @@ Goal forall o, foo2 o -> 0 = 1. intros. eapply trans_eq. inversion H. +Abort. (* Check that the part of "injection" that is called by "inversion" does the same number of intros as the number of equations @@ -136,6 +137,7 @@ Goal True -> True. intro. Fail inversion H using False. Fail inversion foo using True_ind. +Abort. (* Was failing at some time between 7 and 10 September 2014 *) (* even though, it is not clear that the resulting context is interesting *) diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 29350d620e..6370cab6b2 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -589,6 +589,8 @@ Close Scope Z_scope. Theorem S_is_not_O : forall n, S n <> 0. +Set Nested Proofs Allowed. + Definition Is_zero (x:nat):= match x with | 0 => True | _ => False diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 6fbe61a9be..d1d384659b 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -422,6 +422,7 @@ Abort. Goal forall b:bool, b = b. intros. destruct b eqn:H. +Abort. (* Check natural instantiation behavior when the goal has already an evar *) diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 22fb4d7576..40986e57cb 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -121,14 +121,16 @@ Abort. (* Wish 1988: that fun forces unfold in refine *) Goal (forall A : Prop, A -> ~~A). -Proof. refine(fun A a f => _). +Proof. refine(fun A a f => _). Abort. (* Checking beta-iota normalization of hypotheses in created evars *) Goal {x|x=0} -> True. refine (fun y => let (x,a) := y in _). match goal with a:_=0 |- _ => idtac end. +Abort. Goal (forall P, {P 0}+{P 1}) -> True. refine (fun H => if H (fun x => x=x) then _ else _). match goal with _:0=0 |- _ => idtac end. +Abort. diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v index 3c0b81568a..b9a1273b1a 100644 --- a/test-suite/success/sideff.v +++ b/test-suite/success/sideff.v @@ -5,6 +5,8 @@ Proof. apply (const tt tt). Qed. +Set Nested Proofs Allowed. + Lemma foobar' : unit. Lemma aux : forall A : Type, A -> unit. Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed. diff --git a/test-suite/unit-tests/.merlin b/test-suite/unit-tests/.merlin new file mode 100644 index 0000000000..b2279de74e --- /dev/null +++ b/test-suite/unit-tests/.merlin @@ -0,0 +1,6 @@ +REC + +S ** +B ** + +PKG oUnit diff --git a/test-suite/unit-tests/clib/inteq.ml b/test-suite/unit-tests/clib/inteq.ml new file mode 100644 index 0000000000..c07ec293f0 --- /dev/null +++ b/test-suite/unit-tests/clib/inteq.ml @@ -0,0 +1,13 @@ +open Utest + +let eq0 = mk_bool_test "clib-inteq0" + "Int.equal on 0" + (Int.equal 0 0) + +let eq42 = mk_bool_test "clib-inteq42" + "Int.equal on 42" + (Int.equal 42 42) + +let tests = [ eq0; eq42 ] + +let _ = run_tests __FILE__ tests diff --git a/test-suite/unit-tests/clib/unicode_tests.ml b/test-suite/unit-tests/clib/unicode_tests.ml new file mode 100644 index 0000000000..9ae405977b --- /dev/null +++ b/test-suite/unit-tests/clib/unicode_tests.ml @@ -0,0 +1,15 @@ +open Utest + +let unicode0 = mk_eq_test "clib-unicode0" + "split_at_first_letter, first letter is character" + None + (Unicode.split_at_first_letter "ident") + +let unicode1 = mk_eq_test "clib-unicode1" + "split_at_first_letter, first letter not character" + (Some ("__","ident")) + (Unicode.split_at_first_letter "__ident") + +let tests = [ unicode0; unicode1 ] + +let _ = run_tests __FILE__ tests diff --git a/test-suite/unit-tests/src/utest.ml b/test-suite/unit-tests/src/utest.ml new file mode 100644 index 0000000000..069e6a4bf3 --- /dev/null +++ b/test-suite/unit-tests/src/utest.ml @@ -0,0 +1,74 @@ +open OUnit + +(* general case to build a test *) +let mk_test nm test = nm >: test + +(* common cases for building tests *) +let mk_eq_test nm descr expected actual = + mk_test nm (TestCase (fun _ -> assert_equal ~msg:descr expected actual)) + +let mk_bool_test nm descr actual = + mk_test nm (TestCase (fun _ -> assert_bool descr actual)) + +let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "\n%!") oc) + +(* given test result, print message, return success boolean *) +let logger out_ch result = + let cprintf s = cfprintf out_ch s in + match result with + | RSuccess path -> + cprintf "TEST SUCCEEDED: %s" (string_of_path path); + true + | RError (path,msg) + | RFailure (path,msg) -> + cprintf "TEST FAILED: %s (%s)" (string_of_path path) msg; + false + | RSkip (path,msg) + | RTodo (path,msg) -> + cprintf "TEST DID NOT SUCCEED: %s (%s)" (string_of_path path) msg; + false + +(* run one OUnit test case, return successes, no. of tests *) +(* notionally one test, which might be a TestList *) +let run_one logit test = + let rec process_results rs = + match rs with + [] -> (0,0) + | (r::rest) -> + let succ = if logit r then 1 else 0 in + let succ_results,tot_results = process_results rest in + (succ + succ_results,tot_results + 1) + in + let results = perform_test (fun _ -> ()) test in + process_results results + +(* run list of OUnit test cases, log results *) +let run_tests ml_fn tests = + let log_fn = ml_fn ^ ".log" in + let out_ch = open_out log_fn in + let cprintf s = cfprintf out_ch s in + let ceprintf s = cfprintf stderr s in + let logit = logger out_ch in + let rec run_some tests succ tot = + match tests with + [] -> (succ,tot) + | (t::ts) -> + let succ_one,tot_one = run_one logit t in + run_some ts (succ + succ_one) (tot + tot_one) + in + (* format for test-suite summary to find status + success if all tests succeeded, else failure + *) + let succ,tot = run_some tests 0 0 in + cprintf + "*** Ran %d tests, with %d successes and %d failures ***" + tot succ (tot - succ); + if succ = tot then + cprintf + "==========> SUCCESS <==========\n %s...Ok" ml_fn + else begin + cprintf + "==========> FAILURE <==========\n %s...Error!" ml_fn; + ceprintf "FAILED %s.log" ml_fn + end; + close_out out_ch diff --git a/test-suite/unit-tests/src/utest.mli b/test-suite/unit-tests/src/utest.mli new file mode 100644 index 0000000000..70928228bf --- /dev/null +++ b/test-suite/unit-tests/src/utest.mli @@ -0,0 +1,12 @@ +(** give a name to a unit test *) +val mk_test : string -> OUnit.test -> OUnit.test + +(** simple ways to build a test *) +val mk_eq_test : string -> string -> 'a -> 'a -> OUnit.test +val mk_bool_test : string -> string -> bool -> OUnit.test + +(** run unit tests *) +(* the string argument should be the name of the .ml file + containing the tests; use __FILE__ for that purpose. + *) +val run_tests : string -> OUnit.test list -> unit diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 9aa61ab460..863adb0d14 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -90,7 +90,7 @@ let interp_definition pl bl poly red_option c ctypopt = Note: in program mode some evars may remain. *) let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in - let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in + let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in (* Keep only useful universes. *) let uvars_fold uvars c = Univ.LSet.union uvars (universes_of_constr env evd (of_constr c)) @@ -118,7 +118,7 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t - | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c)) + | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c)) in Obligations.check_evars env evd; let obls, _, c, cty = diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 7b382dacc3..85c0699ea9 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -199,9 +199,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = try let sigma, h_term = fix_proto sigma in let app = mkApp (h_term, [|sort; t|]) in - let _evd = ref sigma in - let res = Typing.e_solve_evars env _evd app in - !_evd, res + Typing.solve_evars env sigma app with e when CErrors.noncritical e -> sigma, t in sigma, LocalAssum (id,fixprot) :: env' diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 101298ef4d..b2532485ae 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -29,7 +29,6 @@ open Indtypes open Pretyping open Evarutil open Indschemes -open Misctypes open Context.Rel.Declaration open Entries @@ -380,7 +379,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> { ind_name = indname; ind_univs = pl; - ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; + ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar; ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc }) indl diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 745f1df1d8..349fc562b5 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -190,9 +190,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in - let _evd = ref sigma in - let def = Typing.e_solve_evars env _evd def in - let sigma = !_evd in + let sigma, def = Typing.solve_evars env sigma def in let sigma = Evarutil.nf_evar_map sigma in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context sigma binders_rel in diff --git a/vernac/record.ml b/vernac/record.ml index b89c0060dc..b0f2292940 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -122,7 +122,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env = EConstr.push_rel_context newps env0 in let poly = match t with - | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in + | { CAst.v = CSort (Glob_term.GType []) } -> true | _ -> false in let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with |