diff options
40 files changed, 750 insertions, 568 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 54d9ccaf19..275d6c1ff5 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -30,10 +30,9 @@ # Trick to avoid getting review requests # each time someone adds an overlay -/appveyor.yml @maximedenes -/dev/ci/appveyor.* @maximedenes -/dev/ci/*.bat @maximedenes -# Secondary maintainer @SkySkimmer +/appveyor.yml @coq/ci-maintainers +/dev/ci/appveyor.* @coq/ci-maintainers +/dev/ci/*.bat @coq/ci-maintainers *.nix @coq/nix-maintainers diff --git a/.gitignore b/.gitignore index 0411247abf..2e5529ccfb 100644 --- a/.gitignore +++ b/.gitignore @@ -134,7 +134,6 @@ coqpp/coqpp_parse.mli g_*.ml -lib/coqProject_file.ml plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml plugins/ltac/extraargs.ml @@ -150,6 +149,7 @@ kernel/byterun/coq_jumptbl.h kernel/copcodes.ml ide/index_urls.txt .lia.cache +.nia.cache # emacs save files *~ diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 50b86b3c5d..e981c592a2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -245,6 +245,12 @@ build:base+async: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" COQUSERFLAGS: "-async-proofs on" +build:quick: + <<: *build-template + variables: + COQ_EXTRA_CONF: "-native-compiler no" + QUICK: "1" + windows64: <<: *windows-template variables: @@ -461,6 +467,11 @@ validate:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" +validate:quick: + <<: *validate-template + dependencies: + - build:quick + # Libraries are by convention the projects that depend on Coq # but not on its ML API diff --git a/CHANGES.md b/CHANGES.md index 6789bc038e..ae67eb5d1b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -93,6 +93,9 @@ Vernacular commands - The naming scheme for anonymous binders in a `Theorem` has changed to avoid conflicts with explicitly named binders. +- Computation of implicit arguments now properly handles local definitions in the + binders for an `Instance`. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: @@ -269,7 +269,7 @@ cleanconfig: distclean: clean cleanconfig cacheclean timingclean voclean: - find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" \ + find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.glob' -o -name "*.cmxs" \ -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + diff --git a/Makefile.build b/Makefile.build index 34d7ce42f7..e683a6bda8 100644 --- a/Makefile.build +++ b/Makefile.build @@ -57,6 +57,9 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line BEFORE ?= AFTER ?= +# Number of parallel jobs for -schedule-vio2vo +NJOBS ?= 2 + ########################################################################### # Default starting rule ########################################################################### @@ -543,7 +546,7 @@ $(CSDPCERTBYTE): $(CSDPCERTCMO) VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -validate: $(CHICKEN) | $(ALLVO) +validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo) $(SHOW)'COQCHK <theories & plugins>' $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) @@ -779,13 +782,19 @@ $(PLUGMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLLIBFILES) $( # since they are all mentioned in at least one Declare ML Module in some .v coqlib: theories plugins +ifdef QUICK + $(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio plugins/**.vio' + $(HIDE)$(BOOTCOQC:-compile=-schedule-vio2vo) $(NJOBS) \ + $(THEORIESVO) $(PLUGINSVO) +endif + coqlib.timing.diff: theories.timing.diff plugins.timing.diff theories: $(THEORIESVO) plugins: $(PLUGINSVO) -theories.timing.diff: $(THEORIESVO:.vo=.v.timing.diff) -plugins.timing.diff: $(PLUGINSVO:.vo=.v.timing.diff) +theories.timing.diff: $(THEORIESVO:.$(VO)=.v.timing.diff) +plugins.timing.diff: $(PLUGINSVO:.$(VO)=.v.timing.diff) .PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff @@ -802,6 +811,10 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) +theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP) + $(SHOW)'COQC -quick -noinit $<' + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -quick -noglob + # The general rule for building .vo files : %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) @@ -814,6 +827,10 @@ ifdef VALIDATE || ( RV=$$?; rm -f "$@"; exit $${RV} ) endif +%.vio: %.v theories/Init/Prelude.vio $(VO_TOOLS_DEP) + $(SHOW)'COQC -quick $<' + $(HIDE)$(BOOTCOQC) $< -quick -noglob + %.v.timing.diff: %.v.before-timing %.v.after-timing $(SHOW)PYTHON TIMING-DIFF $< $(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" diff --git a/Makefile.dev b/Makefile.dev index 9659f602d7..13b85dfad4 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -63,7 +63,7 @@ revision: coqlight: theories-light tools coqbinaries -states: theories/Init/Prelude.vo +states: theories/Init/Prelude.$(VO) miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte diff --git a/Makefile.doc b/Makefile.doc index 48cdcebddb..7ac710b8c9 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -141,7 +141,7 @@ else doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) endif $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ + -R theories Coq $(THEORIESLIGHTVO:.$(VO)=.v) >> $@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex (cd doc/stdlib;\ diff --git a/Makefile.ide b/Makefile.ide index cae77ee348..23ce83d263 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -70,7 +70,7 @@ SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share .PHONY: ide-toploop ide-byteloop ide-optloop # target to build CoqIde (native version) and the stuff needed to lauch it -coqide: coqide-files coqide-opt theories/Init/Prelude.vo +coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO) # target to build CoqIde (in native and byte versions), and no more # NB: this target is used in the opam package coq-coqide diff --git a/Makefile.vofiles b/Makefile.vofiles index d0ae317335..d5217ef4b7 100644 --- a/Makefile.vofiles +++ b/Makefile.vofiles @@ -2,14 +2,20 @@ # This file calls [find] and as such is not suitable for inclusion in # the test suite Makefile, unlike Makefile.common. +ifdef QUICK +VO=vio +else +VO=vo +endif + ########################################################################### # vo files ########################################################################### -THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) -PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) +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) +VFILES := $(ALLVO:.$(VO)=.v) ## More specific targets @@ -20,22 +26,27 @@ THEORIESLIGHTVO:= \ # 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)) +ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo)) # 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_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))))) +vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o))))) + +ifdef QUICK +GLOBFILES:= +else +GLOBFILES:=$(ALLVO:.$(VO)=.glob) +endif -GLOBFILES:=$(ALLVO:.vo=.glob) ifdef NATIVECOMPUTE NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO)) else NATIVEFILES := endif -LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES) +LIBFILES:=$(ALLVO:.$(VO)=.vo) $(NATIVEFILES) $(VFILES) $(GLOBFILES) # For emacs: # Local Variables: @@ -1,20 +1,68 @@ # Coq -[](https://gitlab.com/coq/coq/commits/master) -[](https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master) -[](https://travis-ci.org/coq/coq/builds) -[](https://ci.appveyor.com/project/coq/coq/branch/master) -[](https://gitter.im/coq/coq) -[](https://doi.org/10.5281/zenodo.1003420) +[![GitLab][gitlab-badge]][gitlab-link] +[![Azure Pipelines][azure-badge]][azure-link] +[![Travis][travis-badge]][travis-link] +[![Appveyor][appveyor-badge]][appveyor-link] +[![Gitter][gitter-badge]][gitter-link] +[![DOI][doi-badge]][doi-link] + +[gitlab-badge]: https://gitlab.com/coq/coq/badges/master/pipeline.svg +[gitlab-link]: https://gitlab.com/coq/coq/commits/master + +[azure-badge]: https://dev.azure.com/coq/coq/_apis/build/status/coq.coq?branchName=master +[azure-link]: https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master + +[travis-badge]: https://travis-ci.org/coq/coq.svg?branch=master +[travis-link]: https://travis-ci.org/coq/coq/builds + +[appveyor-badge]: https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true +[appveyor-link]: https://ci.appveyor.com/project/coq/coq/branch/master + +[gitter-badge]: https://badges.gitter.im/coq/coq.svg +[gitter-link]: https://gitter.im/coq/coq + +[doi-badge]: https://zenodo.org/badge/DOI/10.5281/zenodo.1003420.svg +[doi-link]: https://doi.org/10.5281/zenodo.1003420 Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. ## Installation -Download the pre-built packages of the [latest release](https://github.com/coq/coq/releases/latest) for Windows and MacOS; -read the [help page](https://coq.inria.fr/opam/www/using.html) on how to install Coq with OPAM; -or refer to the [`INSTALL` file](INSTALL) for the procedure to install from source. + +[![latest packaged version(s)][repology-badge]][repology-link] + +[![Arch package][arch-badge]][arch-link] +[![Chocolatey package][chocolatey-badge]][chocolatey-link] +[![Homebrew package][homebrew-badge]][homebrew-link] +[![MacPorts package][macports-badge]][macports-link] +[![nixpkgs unstable package][nixpkgs-badge]][nixpkgs-link] + +[repology-badge]: https://repology.org/badge/latest-versions/coq.svg +[repology-link]: https://repology.org/metapackage/coq/versions + +[arch-badge]: https://repology.org/badge/version-for-repo/arch/coq.svg +[arch-link]: https://www.archlinux.org/packages/community/x86_64/coq/ + +[chocolatey-badge]: https://repology.org/badge/version-for-repo/chocolatey/coq.svg +[chocolatey-link]: https://chocolatey.org/packages/Coq + +[homebrew-badge]: https://repology.org/badge/version-for-repo/homebrew/coq.svg +[homebrew-link]: https://formulae.brew.sh/formula/coq + +[macports-badge]: https://repology.org/badge/version-for-repo/macports/coq.svg +[macports-link]: https://www.macports.org/ports.php?by=name&substr=coq + +[nixpkgs-badge]: https://repology.org/badge/version-for-repo/nix_unstable/coq.svg +[nixpkgs-link]: https://nixos.org/nixos/packages.html#coq + +Download the pre-built packages of the [latest release][] for Windows and macOS; +read the [help page][opam-using] on how to install Coq with OPAM; +or refer to the [`INSTALL`](INSTALL) file for the procedure to install from source. + +[latest release]: https://github.com/coq/coq/releases/latest +[opam-using]: https://coq.inria.fr/opam/www/using.html ## Documentation diff --git a/azure-pipelines.yml b/azure-pipelines.yml index e217601ae2..a8b42cc722 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -1,31 +1,78 @@ -pool: - vmImage: 'vs2017-win2016' - -steps: -- checkout: self - fetchDepth: 10 - -# cygwin package list not checked for minimality -- script: | - powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" - SET CYGROOT=C:\cygwin64 - SET CYGCACHE=%CYGROOT%\var\cache\setup - setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python - - SET TARGET_ARCH=x86_64-w64-mingw32 - SET CD_MFMT=%cd:\=/% - SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/% - C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh - displayName: 'Install cygwin' - env: - CYGMIRROR: "http://mirror.easyname.at/cygwin" - -- script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh - displayName: 'Install opam' - -- script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh - displayName: 'Build Coq' - -- script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh - displayName: 'Test Coq' +# NB: image names can be found at +# https://docs.microsoft.com/en-us/azure/devops/pipelines/agents/hosted + +variables: + NJOBS: "2" + +jobs: +- job: Windows + pool: + vmImage: 'vs2017-win2016' + + steps: + - checkout: self + fetchDepth: 10 + + # cygwin package list not checked for minimality + - script: | + powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" + SET CYGROOT=C:\cygwin64 + SET CYGCACHE=%CYGROOT%\var\cache\setup + setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python + + SET TARGET_ARCH=x86_64-w64-mingw32 + SET CD_MFMT=%cd:\=/% + SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/% + C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh + displayName: 'Install cygwin' + env: + CYGMIRROR: "http://mirror.easyname.at/cygwin" + + - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh + displayName: 'Install opam' + + - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh + displayName: 'Build Coq' + + - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh + displayName: 'Test Coq' + +- job: macOS + pool: + vmImage: 'macOS-10.13' + + steps: + - checkout: self + fetchDepth: 10 + + - script: | + set -e + brew update + brew unlink python + brew install gnu-time opam + + opam init -a -j "$NJOBS" --compiler=$COMPILER + opam switch set $COMPILER + eval $(opam env) + opam update + opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit + opam list + displayName: 'Install dependencies' + env: + COMPILER: "4.07.1" + FINDLIB_VER: ".1.8.0" + OPAMYES: "true" + + - script: | + set -e + + eval $(opam env) + ./configure -local -warn-error yes -native-compiler no + make -j "$NJOBS" + displayName: 'Build Coq' + + - script: | + eval $(opam env) + make -j "$NJOBS" test-suite + displayName: 'Run Coq Test Suite' diff --git a/checker/check.ml b/checker/check.ml index 30437e8bd0..b2930d9535 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -329,7 +329,7 @@ let intern_from_file (dir, f) = user_err ~hdr:"intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin - chk_pp (str " (was a vio file) "); + Flags.if_verbose chk_pp (str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) diff --git a/checker/checker.ml b/checker/checker.ml index 167258f8bb..d97ab5409e 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -297,7 +297,7 @@ let explain_exn = function | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints" | UndeclaredUniverse _ -> str"UndeclaredUniverse")) - | Indtypes.InductiveError e -> + | InductiveError e -> hov 0 (str "Error related to inductive types") (* let ctx = Check.get_env() in hov 0 diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index b202635714..07a13b8204 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -691,7 +691,7 @@ function installer_addon_end { # ------------------------------------------------------------------------------ function coq_set_timeouts_1000 { - find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/' + find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/g' } ###################### MODULE BUILD FUNCTIONS ##################### @@ -701,7 +701,7 @@ function coq_set_timeouts_1000 { function make_sed { if build_prep https://ftp.gnu.org/gnu/sed/ sed-4.2.2 tar.gz ; then logn configure ./configure - log1 make + log1 make $MAKE_OPT log2 make install log2 make clean build_post @@ -1107,7 +1107,7 @@ function make_ocamlbuild { make_ocaml if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1634,7 +1634,7 @@ function make_addon_bignums { installer_addon_section bignums "Bignums" "Coq library for fast arbitrary size numbers" "" # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local - log1 make all + log1 make $MAKE_OPT all log2 make install build_post fi @@ -1650,7 +1650,7 @@ function make_addon_equations { # Note: PATH is automatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1696,7 +1696,7 @@ function make_addon_ltac2 { installer_addon_dependency ltac2 if build_prep_overlay ltac2; then installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" "" - log1 make all + log1 make $MAKE_OPT all log2 make install build_post fi @@ -1709,7 +1709,7 @@ function make_addon_unicoq { if build_prep_overlay unicoq; then installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" "" log1 coq_makefile -f Make -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1724,7 +1724,7 @@ function make_addon_mtac2 { if build_prep_overlay mtac2; then installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." "" log1 coq_makefile -f _CoqProject -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1766,7 +1766,7 @@ function make_addon_menhirlib { echo -R . MenhirLib > _CoqProject ls -1 *.v >> _CoqProject log1 coq_makefile -f _CoqProject -o Makefile.coq - log1 make -f Makefile.coq all + log1 make -f Makefile.coq $MAKE_OPT all logn make-install make -f Makefile.coq install build_post fi @@ -1779,10 +1779,10 @@ function make_addon_compcert { make_menhir make_addon_menhirlib installer_addon_dependency_end - if build_prep_overlay CompCert; then + if build_prep_overlay compcert; then installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off" logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin - log1 make + log1 make $MAKE_OPT log2 make install logn install-license-1 install -D -T "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE" logn install-license-2 install -D -T "LICENSE" "$PREFIXCOQ/lib/compcert/LICENSE" @@ -1807,8 +1807,8 @@ function install_addon_vst { install_glob "progs" '*.v' "$VSTDEST/progs/" install_glob "progs" '*.c' "$VSTDEST/progs/" install_glob "progs" '*.h' "$VSTDEST/progs/" - install_glob "veric" '*.v' "$VSTDEST/msl/" - install_glob "veric" '*.vo' "$VSTDEST/msl/" + install_glob "veric" '*.v' "$VSTDEST/veric/" + install_glob "veric" '*.vo' "$VSTDEST/veric/" # Install VST documentation files install_glob "." 'LICENSE' "$VSTDEST" @@ -1821,12 +1821,20 @@ function install_addon_vst { install_glob "." '_CoqProject-export' "$VSTDEST/progs" } +function vst_patch_compcert_refs { + find . -type f -name '*.v' -print0 | xargs -0 sed -E -i \ + -e 's/(Require\s+(Import\s+|Export\s+)*)compcert\./\1VST.compcert./g' \ + -e 's/From compcert Require/From VST.compcert Require/g' +} + function make_addon_vst { installer_addon_dependency vst - if build_prep_overlay VST; then + if build_prep_overlay vst; then installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off" - log1 coq_set_timeouts_1000 - log1 make IGNORECOQVERSION=true $MAKE_OPT + # log1 coq_set_timeouts_1000 + log1 vst_patch_compcert_refs + # The usage of the shell variable ARCH in VST collides with the usage in this shellscript + logn make env -u ARCH make IGNORECOQVERSION=true $MAKE_OPT log1 install_addon_vst build_post fi @@ -1851,9 +1859,9 @@ function make_addon_coquelicot { function make_addon_aactactics { installer_addon_dependency aac - if build_prep_overlay aactactics; then + if build_prep_overlay aac_tactics; then installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" "" - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1894,7 +1902,7 @@ function make_addon_quickchick { installer_addon_dependency_end if build_prep_overlay quickchick; then installer_addon_section quickchick "QuickChick" "Coq plugin for randomized testing and counter example search" "" - log1 make + log1 make $MAKE_OPT log2 make install build_post fi diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch new file mode 100755 index 0000000000..2c8c46373f --- /dev/null +++ b/dev/build/windows/patches_coq/VST.patch @@ -0,0 +1,15 @@ +diff --git a/Makefile b/Makefile +index 4a119042..fdfac13e 100755 +--- a/Makefile ++++ b/Makefile +@@ -76,8 +76,8 @@ endif + + COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND) + +-COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d)) +-EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d)) ++COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d)) ++EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d)) + + # for SSReflect + ifdef MATHCOMP diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 470d07b27d..f26e0904bc 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -3,14 +3,15 @@ set -e -x APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c +NJOBS=2 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh -opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing +opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing eval "$(opam env)" -opam install -y num ocamlfind ounit +opam install -j $NJOBS -y num ocamlfind ounit # Full regular Coq Build -cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte # && make -C test-suite all INTERACTIVE= # && make validate +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 7e8013be9b..bba17314f7 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -10,5 +10,9 @@ git_download fiat_crypto # building the executables. # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 +fiat_crypto_CI_TARGETS1="c-files printlite lite" +fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem" + ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ - ulimit -s 32768 && make new-pipeline c-files ) + ulimit -s 32768 && \ + make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 386a3de204..5f819f31f9 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -26,12 +26,12 @@ if %ARCH% == 64 ( SET CYGROOT=C:\ci\cygwin%ARCH%
SET DESTCOQ=C:\ci\coq%ARCH%
+SET CYGCACHE=C:\ci\cache\cgwin
CALL :MakeUniqueFolder %CYGROOT% CYGROOT
CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
-SET CYGCACHE=%CYGROOT%\var\cache\setup
SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
SET COQREGTESTING=Y
@@ -49,10 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" ( -addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
- -addon=coquelicot
- REM addons with build issues
- REM -addon=vst ^
- REM -addon=aactactics ^
+ -addon=coquelicot ^
+ -addon=vst ^
+ -addon=aactactics
) ELSE (
SET "EXTRA_ADDONS= "
)
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 5fd8a3b7d9..a27dacc5a7 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -198,8 +198,26 @@ if [ -z "$(git config user.signingkey)" ]; then warning "gpg will guess a key out of your git config user.* data" fi +# Generate commit message + +info "Fetching review data" +reviews=$(curl -s "$API/pulls/$PR/reviews") +msg="Merge PR #$PR: $TITLE" + +has_state() { + [ "$(jq -rc 'map(select(.user.login == "'"$1"'") | .state) | any(. == "'"$2"'")' <<< "$reviews")" = true ] +} + +for reviewer in $(jq -rc 'map(.user.login) | unique | join(" ")' <<< "$reviews" ); do + if has_state "$reviewer" APPROVED; then + msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Reviewed-by="$reviewer") + elif has_state "$reviewer" COMMENTED; then + msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Ack-by="$reviewer") + fi +done + info "merging" -git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e +git merge -v -S --no-ff FETCH_HEAD -m "$msg" -e # TODO: improve this check if ! git diff --quiet --diff-filter=A "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index cc5d9d6205..693ee28a47 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1041,6 +1041,12 @@ in :math:`\Type`. enabled it will prevail over automatic template polymorphism and cause an error when using the ``template`` attribute. +.. warn:: Automatically declaring @ident as template polymorphic. + + Warning ``auto-template`` can be used to find which types are + implicitly declared template polymorphic by :flag:`Auto Template + Polymorphism`. + If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local diff --git a/kernel/environ.ml b/kernel/environ.ml index 38a428d9a1..77820a301e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -238,6 +238,13 @@ let is_impredicative_set env = | ImpredicativeSet -> true | _ -> false +let is_impredicative_sort env = function + | Sorts.Prop -> true + | Sorts.Set -> is_impredicative_set env + | Sorts.Type _ -> false + +let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u) + let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded diff --git a/kernel/environ.mli b/kernel/environ.mli index 8a2efb2477..6d4d3b282b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -98,6 +98,9 @@ val type_in_type : env -> bool val deactivated_guard : env -> bool val indices_matter : env -> bool +val is_impredicative_sort : env -> Sorts.t -> bool +val is_impredicative_univ : env -> Univ.Universe.t -> bool + (** is the local context empty *) val empty_context : env -> bool diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml new file mode 100644 index 0000000000..6976b2019d --- /dev/null +++ b/kernel/indTyping.ml @@ -0,0 +1,307 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +open Names +open Univ +open Term +open Constr +open Declarations +open Environ +open Entries +open Type_errors +open Context.Rel.Declaration + +(** Check name unicity. + Redundant with safe_typing's add_field checks -> to remove?. *) + +(* [check_constructors_names id s cl] checks that all the constructors names + appearing in [l] are not present in the set [s], and returns the new set + of names. The name [id] is the name of the current inductive type, used + when reporting the error. *) + +let check_constructors_names = + let rec check idset = function + | [] -> idset + | c::cl -> + if Id.Set.mem c idset then + raise (InductiveError (SameNamesConstructors c)) + else + check (Id.Set.add c idset) cl + in + check + +(* [mind_check_names mie] checks the names of an inductive types declaration, + and raises the corresponding exceptions when two types or two constructors + have the same name. *) + +let mind_check_names mie = + let rec check indset cstset = function + | [] -> () + | ind::inds -> + let id = ind.mind_entry_typename in + let cl = ind.mind_entry_consnames in + if Id.Set.mem id indset then + raise (InductiveError (SameNamesTypes id)) + else + let cstset' = check_constructors_names cstset cl in + check (Id.Set.add id indset) cstset' inds + in + check Id.Set.empty Id.Set.empty mie.mind_entry_inds +(* The above verification is not necessary from the kernel point of + vue since inductive and constructors are not referred to by their + name, but only by the name of the inductive packet and an index. *) + + +(************************************************************************) +(************************** Cumulativity checking************************) +(************************************************************************) + +(* Check arities and constructors *) +let check_subtyping_arity_constructor env subst arcn numparams is_arity = + let numchecked = ref 0 in + let basic_check ev tp = + if !numchecked < numparams then () else Reduction.conv_leq ev tp (subst tp); + numchecked := !numchecked + 1 + in + let check_typ typ typ_env = + match typ with + | LocalAssum (_, typ') -> + begin + try + basic_check typ_env typ'; Environ.push_rel typ typ_env + with Reduction.NotConvertible -> + CErrors.anomaly ~label:"bad inductive subtyping relation" + Pp.(str "Invalid subtyping relation") + end + | _ -> CErrors.anomaly Pp.(str "") + in + let typs, codom = Reduction.dest_prod env arcn in + let last_env = Context.Rel.fold_outside check_typ typs ~init:env in + if not is_arity then basic_check last_env codom else () + +let check_cumulativity univs env_ar params data = + let numparams = Context.Rel.nhyps params in + let uctx = CumulativityInfo.univ_context univs in + let new_levels = Array.init (UContext.size uctx) + (fun i -> Level.(make (UGlobal.make DirPath.empty i))) + in + let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) + LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels + in + let dosubst = Vars.subst_univs_level_constr lmap in + let instance_other = Instance.of_array new_levels in + let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env = Environ.push_context uctx_other env_ar in + let subtyp_constraints = + CumulativityInfo.leq_constraints univs + (UContext.instance uctx) instance_other + Constraint.empty + in + let env = Environ.add_constraints subtyp_constraints env in + (* process individual inductive types: *) + List.iter (fun (arity,lc) -> + check_subtyping_arity_constructor env dosubst arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc) + data + +(************************************************************************) +(************************** Type checking *******************************) +(************************************************************************) + +type univ_info = { ind_squashed : bool; + ind_min_univ : Universe.t option; (* Some for template *) + ind_univ : Universe.t } + +let check_univ_leq env u info = + let ind_univ = info.ind_univ in + if type_in_type env || (UGraph.check_leq (universes env) u ind_univ) + then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ } + else if is_impredicative_univ env ind_univ + then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true } + else raise (InductiveError BadUnivs) + else raise (InductiveError BadUnivs) + +let check_indices_matter env_params info indices = + let check_index d (info,env) = + let info = match d with + | LocalAssum (_,t) -> + (* could be retyping if it becomes available in the kernel *) + let tj = Typeops.infer_type env t in + check_univ_leq env (Sorts.univ_of_sort tj.utj_type) info + | LocalDef _ -> info + in + info, push_rel d env + in + if not (indices_matter env_params) then info + else fst (Context.Rel.fold_outside ~init:(info,env_params) check_index indices) + +(* env_ar contains the inductives before the current ones in the block, and no parameters *) +let check_arity env_params env_ar ind = + let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in + let indices, ind_sort = Reduction.dest_arity env_params arity in + let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in + let univ_info = {ind_squashed=false;ind_min_univ;ind_univ=Sorts.univ_of_sort ind_sort} in + let univ_info = check_indices_matter env_params univ_info indices in + (* We do not need to generate the universe of the arity with params; + if later, after the validation of the inductive definition, + full_arity is used as argument or subject to cast, an upper + universe will be generated *) + let arity = it_mkProd_or_LetIn arity (Environ.rel_context env_params) in + push_rel (LocalAssum (Name ind.mind_entry_typename, arity)) env_ar, + (arity, indices, univ_info) + +let check_constructor_univs env_ar_par univ_info (args,_) = + (* We ignore the output, positivity will check that it's the expected inductive type *) + (* NB: very similar to check_indices_matter but that will change with SProp *) + fst (Context.Rel.fold_outside ~init:(univ_info,env_ar_par) (fun d (univ_info,env) -> + let univ_info = match d with + | LocalDef _ -> univ_info + | LocalAssum (_,t) -> + (* could be retyping if it becomes available in the kernel *) + let tj = Typeops.infer_type env t in + check_univ_leq env (Sorts.univ_of_sort tj.utj_type) univ_info + in + univ_info, push_rel d env) + args) + +let check_constructors env_ar_par params lc (arity,indices,univ_info) = + let lc = Array.map_of_list (fun c -> (Typeops.infer_type env_ar_par c).utj_val) lc in + let splayed_lc = Array.map (Reduction.dest_prod_assum env_ar_par) lc in + let univ_info = if Array.length lc <= 1 then univ_info + else check_univ_leq env_ar_par Univ.Universe.type0 univ_info + in + let univ_info = Array.fold_left (check_constructor_univs env_ar_par) univ_info splayed_lc in + (* generalize the constructors over the parameters *) + let lc = Array.map (fun c -> Term.it_mkProd_or_LetIn c params) lc in + (arity, lc), (indices, splayed_lc), univ_info + +(* Allowed eliminations *) + +(* Previous comment: *) +(* Unitary/empty Prop: elimination to all sorts are realizable *) +(* unless the type is large. If it is large, forbids large elimination *) +(* which otherwise allows simulating the inconsistent system Type:Type. *) +(* -> this is now handled by is_smashed: *) +(* - all_sorts in case of small, unitary Prop (not smashed) *) +(* - logical_sorts in case of large, unitary Prop (smashed) *) + +let all_sorts = [InProp;InSet;InType] +let small_sorts = [InProp;InSet] +let logical_sorts = [InProp] + +let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_} = + if not ind_squashed then all_sorts + else match Sorts.family (Sorts.sort_of_univ ind_univ) with + | InType -> assert false + | InSet -> small_sorts + | InProp -> logical_sorts + +(* Returns the list [x_1, ..., x_n] of levels contributing to template + polymorphism. The elements x_k is None if the k-th parameter (starting + from the most recent and ignoring let-definitions) is not contributing + or is Some u_k if its level is u_k and is contributing. *) +let param_ccls paramsctxt = + let fold acc = function + | (LocalAssum (_, p)) -> + (let c = Term.strip_prod_assum p in + match kind c with + | Sort (Type u) -> Univ.Universe.level u + | _ -> None) :: acc + | LocalDef _ -> acc + in + List.fold_left fold [] paramsctxt + +let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = + let arity = Vars.subst_univs_level_constr usubst arity in + let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in + let indices = Vars.subst_univs_level_context usubst indices in + let splayed_lc = Array.map (fun (args,out) -> + let args = Vars.subst_univs_level_context usubst args in + let out = Vars.subst_univs_level_constr usubst out in + args,out) + splayed_lc + in + let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in + + let arity = match univ_info.ind_min_univ with + | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ} + | Some min_univ -> + ((match univs with + | Monomorphic_ind _ -> () + | Polymorphic_ind _ | Cumulative_ind _ -> + CErrors.anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.")); + TemplateArity {template_param_levels=param_ccls params; template_level=min_univ}) + in + + let kelim = allowed_sorts univ_info in + (arity,lc), (indices,splayed_lc), kelim + +let abstract_inductive_universes = function + | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) + | Polymorphic_ind_entry (nas, ctx) -> + let (inst, auctx) = Univ.abstract_universes nas ctx in + let inst = Univ.make_instance_subst inst in + (inst, Polymorphic_ind auctx) + | Cumulative_ind_entry (nas, cumi) -> + let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in + let inst = Univ.make_instance_subst inst in + (inst, Cumulative_ind acumi) + +let typecheck_inductive env (mie:mutual_inductive_entry) = + let () = match mie.mind_entry_inds with + | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.") + | _ -> () + in + (* Check unicity of names (redundant with safe_typing's add_field checks) *) + mind_check_names mie; + assert (List.is_empty (Environ.rel_context env)); + + (* universes *) + let env_univs = + match mie.mind_entry_universes with + | Monomorphic_ind_entry ctx -> push_context_set ctx env + | Polymorphic_ind_entry (_, ctx) -> push_context ctx env + | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env + in + + (* Params *) + let env_params = Typeops.check_context env_univs mie.mind_entry_params in + let params = Environ.rel_context env_params in + + (* Arities *) + let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in + let env_ar_par = push_rel_context params env_ar in + + (* Constructors *) + let data = List.map2 (fun ind data -> check_constructors env_ar_par params ind.mind_entry_lc data) + mie.mind_entry_inds data + in + + let () = match mie.mind_entry_universes with + | Cumulative_ind_entry (_,univs) -> check_cumulativity univs env_ar params (List.map pi1 data) + | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> () + in + + (* Abstract universes *) + let usubst, univs = abstract_inductive_universes mie.mind_entry_universes in + let params = Vars.subst_univs_level_context usubst params in + let data = List.map (abstract_packets univs usubst params) data in + + let env_ar_par = + let ctx = Environ.rel_context env_ar_par in + let ctx = Vars.subst_univs_level_context usubst ctx in + let env = Environ.pop_rel_context (Environ.nb_rel env_ar_par) env_ar_par in + Environ.push_rel_context ctx env + in + + env_ar_par, univs, params, Array.of_list data diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli new file mode 100644 index 0000000000..8841e38636 --- /dev/null +++ b/kernel/indTyping.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Environ +open Entries +open Declarations + +(** Type checking for some inductive entry. + Returns: + - environment with inductives + parameters in rel context + - abstracted universes + - parameters + - for each inductive, + (arity * constructors) (with params) + * (indices * splayed constructor types) (both without params) + * allowed eliminations + *) +val typecheck_inductive : env -> mutual_inductive_entry -> + env + * abstract_inductive_universes + * Constr.rel_context + * ((inductive_arity * Constr.types array) * + (Constr.rel_context * (Constr.rel_context * Constr.types) array) * + Sorts.family list) + array diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 68d44f8782..9bb848c6a4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -11,7 +11,6 @@ open CErrors open Util open Names -open Univ open Term open Constr open Vars @@ -20,9 +19,7 @@ open Declareops open Inductive open Environ open Reduction -open Typeops open Entries -open Pp open Context.Rel.Declaration (* Terminology: @@ -49,14 +46,11 @@ let weaker_noccur_between env x nvars t = if noccur_between x nvars t' then Some t' else None -let is_constructor_head t = - isRel(fst(decompose_app t)) - (************************************************************************) (* Various well-formedness check for inductive declarations *) (* Errors related to inductive constructions *) -type inductive_error = +type inductive_error = Type_errors.inductive_error = | NonPos of env * constr * constr | NotEnoughArgs of env * constr * constr | NotConstructor of env * Id.t * constr * constr * int * int @@ -67,342 +61,9 @@ type inductive_error = | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType + | BadUnivs -exception InductiveError of inductive_error - -(* [check_constructors_names id s cl] checks that all the constructors names - appearing in [l] are not present in the set [s], and returns the new set - of names. The name [id] is the name of the current inductive type, used - when reporting the error. *) - -let check_constructors_names = - let rec check idset = function - | [] -> idset - | c::cl -> - if Id.Set.mem c idset then - raise (InductiveError (SameNamesConstructors c)) - else - check (Id.Set.add c idset) cl - in - check - -(* [mind_check_names mie] checks the names of an inductive types declaration, - and raises the corresponding exceptions when two types or two constructors - have the same name. *) - -let mind_check_names mie = - let rec check indset cstset = function - | [] -> () - | ind::inds -> - let id = ind.mind_entry_typename in - let cl = ind.mind_entry_consnames in - if Id.Set.mem id indset then - raise (InductiveError (SameNamesTypes id)) - else - let cstset' = check_constructors_names cstset cl in - check (Id.Set.add id indset) cstset' inds - in - check Id.Set.empty Id.Set.empty mie.mind_entry_inds -(* The above verification is not necessary from the kernel point of - vue since inductive and constructors are not referred to by their - name, but only by the name of the inductive packet and an index. *) - -(************************************************************************) -(************************************************************************) - -(* Typing the arities and constructor types *) - -let infos_and_sort env t = - let rec aux env t max = - let t = whd_all env t in - match kind t with - | Prod (name,c1,c2) -> - let varj = infer_type env c1 in - let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in - let max = Universe.sup max (Sorts.univ_of_sort varj.utj_type) in - aux env1 c2 max - | _ when is_constructor_head t -> max - | _ -> (* don't fail if not positive, it is tested later *) max - in aux env t Universe.type0m - -(* Computing the levels of polymorphic inductive types - - For each inductive type of a block that is of level u_i, we have - the constraints that u_i >= v_i where v_i is the type level of the - types of the constructors of this inductive type. Each v_i depends - of some of the u_i and of an extra (maybe non variable) universe, - say w_i that summarize all the other constraints. Typically, for - three inductive types, we could have - - u1,u2,u3,w1 <= u1 - u1 w2 <= u2 - u2,u3,w3 <= u3 - - From this system of inequations, we shall deduce - - w1,w2,w3 <= u1 - w1,w2 <= u2 - w1,w2,w3 <= u3 -*) - -(* This (re)computes informations relevant to extraction and the sort of an - arity or type constructor; we do not to recompute universes constraints *) - -let infer_constructor_packet env_ar_par params lc = - (* type-check the constructors *) - let jlc = List.map (infer_type env_ar_par) lc in - let jlc = Array.of_list jlc in - (* generalize the constructor over the parameters *) - let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in - (* compute the max of the sorts of the products of the constructors types *) - let levels = List.map (infos_and_sort env_ar_par) lc in - let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in - let level = List.fold_left (fun max l -> Universe.sup max l) min levels in - (lc'', level) - -(* If indices matter *) -let cumulate_arity_large_levels env sign = - fst (List.fold_right - (fun d (lev,env) -> - match d with - | LocalAssum (_,t) -> - let tj = infer_type env t in - let u = Sorts.univ_of_sort tj.utj_type in - (Universe.sup u lev, push_rel d env) - | LocalDef _ -> - lev, push_rel d env) - sign (Universe.type0m,env)) - -let is_impredicative env u = - is_type0m_univ u || (is_type0_univ u && is_impredicative_set env) - -(* Returns the list [x_1, ..., x_n] of levels contributing to template - polymorphism. The elements x_k is None if the k-th parameter (starting - from the most recent and ignoring let-definitions) is not contributing - or is Some u_k if its level is u_k and is contributing. *) -let param_ccls paramsctxt = - let fold acc = function - | (LocalAssum (_, p)) -> - (let c = Term.strip_prod_assum p in - match kind c with - | Sort (Type u) -> Univ.Universe.level u - | _ -> None) :: acc - | LocalDef _ -> acc - in - List.fold_left fold [] paramsctxt - -(* Check arities and constructors *) -let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : types) numparams is_arity = - let numchecked = ref 0 in - let basic_check ev tp = - if !numchecked < numparams then () else conv_leq ev tp (subst tp); - numchecked := !numchecked + 1 - in - let check_typ typ typ_env = - match typ with - | LocalAssum (_, typ') -> - begin - try - basic_check typ_env typ'; Environ.push_rel typ typ_env - with NotConvertible -> - anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") - end - | _ -> anomaly (Pp.str "") - in - let typs, codom = dest_prod env arcn in - let last_env = Context.Rel.fold_outside check_typ typs ~init:env in - if not is_arity then basic_check last_env codom else () - -(* Check that the subtyping information inferred for inductive types in the block is correct. *) -(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) -let check_subtyping cumi paramsctxt env_ar inds = - let numparams = Context.Rel.nhyps paramsctxt in - let uctx = CumulativityInfo.univ_context cumi in - let new_levels = Array.init (UContext.size uctx) - (fun i -> Level.make (Level.UGlobal.make DirPath.empty i)) - in - let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) - LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels - in - let dosubst = subst_univs_level_constr lmap in - let instance_other = Instance.of_array new_levels in - let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx_other env_ar in - let subtyp_constraints = - CumulativityInfo.leq_constraints cumi - (UContext.instance uctx) instance_other - Constraint.empty - in - let env = Environ.add_constraints subtyp_constraints env in - (* process individual inductive types: *) - Array.iter (fun (_id,_cn,lc,(_sign,arity)) -> - match arity with - | RegularArity (_, full_arity, _) -> - check_subtyping_arity_constructor env dosubst full_arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc - | TemplateArity _ -> - anomaly ~label:"check_subtyping" - Pp.(str "template polymorphism and cumulative polymorphism are not compatible") - ) inds - -(* Type-check an inductive definition. Does not check positivity - conditions. *) -(* TODO check that we don't overgeneralize construcors/inductive arities with - universes that are absent from them. Is it possible? -*) -let typecheck_inductive env mie = - let () = match mie.mind_entry_inds with - | [] -> anomaly (Pp.str "empty inductive types declaration.") - | _ -> () - in - (* Check unicity of names *) - mind_check_names mie; - (* Params are typed-checked here *) - let env' = - match mie.mind_entry_universes with - | Monomorphic_ind_entry ctx -> push_context_set ctx env - | Polymorphic_ind_entry (_, ctx) -> push_context ctx env - | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env - in - let env_params = check_context env' mie.mind_entry_params in - let paramsctxt = mie.mind_entry_params in - (* We first type arity of each inductive definition *) - (* This allows building the environment of arities and to share *) - (* the set of constraints *) - let env_arities, rev_arity_list = - List.fold_left - (fun (env_ar,l) ind -> - (* Arities (without params) are typed-checked here *) - let template = ind.mind_entry_template in - let arity = - if isArity ind.mind_entry_arity then - let (ctx,s) = dest_arity env_params ind.mind_entry_arity in - match s with - | Type u when Univ.universe_level u = None -> - (** We have an algebraic universe as the conclusion of the arity, - typecheck the dummy Π ctx, Prop and do a special case for the conclusion. - *) - let proparity = infer_type env_params (mkArity (ctx, Sorts.prop)) in - let (cctx, _) = destArity proparity.utj_val in - (* Any universe is well-formed, we don't need to check [s] here *) - mkArity (cctx, s) - | _ -> - let arity = infer_type env_params ind.mind_entry_arity in - arity.utj_val - else let arity = infer_type env_params ind.mind_entry_arity in - arity.utj_val - in - let (sign, deflev) = dest_arity env_params arity in - let inflev = - (* The level of the inductive includes levels of indices if - in indices_matter mode *) - if indices_matter env - then Some (cumulate_arity_large_levels env_params sign) - else None - in - (* We do not need to generate the universe of full_arity; if - later, after the validation of the inductive definition, - full_arity is used as argument or subject to cast, an - upper universe will be generated *) - let full_arity = it_mkProd_or_LetIn arity paramsctxt in - let id = ind.mind_entry_typename in - let env_ar' = - push_rel (LocalAssum (Name id, full_arity)) env_ar in - (* (add_constraints cst2 env_ar) in *) - (env_ar', (id,full_arity,sign @ paramsctxt,template,deflev,inflev)::l)) - (env',[]) - mie.mind_entry_inds in - - let arity_list = List.rev rev_arity_list in - - (* builds the typing context "Gamma, I1:A1, ... In:An, params" *) - let env_ar_par = push_rel_context paramsctxt env_arities in - - (* Now, we type the constructors (without params) *) - let inds = - List.fold_right2 - (fun ind arity_data inds -> - let (lc',cstrs_univ) = - infer_constructor_packet env_ar_par paramsctxt ind.mind_entry_lc in - let consnames = ind.mind_entry_consnames in - let ind' = (arity_data,consnames,lc',cstrs_univ) in - ind'::inds) - mie.mind_entry_inds - arity_list - ([]) in - - let inds = Array.of_list inds in - - (* Compute/check the sorts of the inductive types *) - - let inds = - Array.map (fun ((id,full_arity,sign,template,def_level,inf_level),cn,lc,clev) -> - let infu = - (** Inferred level, with parameters and constructors. *) - match inf_level with - | Some alev -> Universe.sup clev alev - | None -> clev - in - let full_polymorphic () = - let defu = Sorts.univ_of_sort def_level in - let is_natural = - type_in_type env || (UGraph.check_leq (universes env') infu defu) - in - let _ = - (** Impredicative sort, always allow *) - if is_impredicative env defu then () - else (** Predicative case: the inferred level must be lower or equal to the - declared level. *) - if not is_natural then - anomaly ~label:"check_inductive" - (Pp.str"Incorrect universe " ++ - Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr infu ++ Pp.str ".") - in - RegularArity (not is_natural,full_arity,defu) - in - let template_polymorphic () = - let _sign, s = - try dest_arity env full_arity - with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) - in - let u = Sorts.univ_of_sort s in - (* The polymorphic level is a function of the level of the *) - (* conclusions of the parameters *) - (* We enforce [u >= lev] in case [lev] has a strict upper *) - (* constraints over [u] *) - let b = type_in_type env || UGraph.check_leq (universes env') infu u in - if not b then - anomaly ~label:"check_inductive" - (Pp.str"Incorrect universe " ++ - Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr clev ++ Pp.str ".") - else - TemplateArity (param_ccls paramsctxt, infu) - in - let arity = - match mie.mind_entry_universes with - | Monomorphic_ind_entry _ -> - if template then template_polymorphic () - else full_polymorphic () - | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> - if template - then anomaly ~label:"polymorphic_template_ind" - Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") - else full_polymorphic () - in - (id,cn,lc,(sign,arity))) - inds - in - (* Check that the subtyping information inferred for inductive types in the block is correct. *) - (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) - let () = - match mie.mind_entry_universes with - | Monomorphic_ind_entry _ -> () - | Polymorphic_ind_entry _ -> () - | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds - in (env_arities, env_ar_par, paramsctxt, inds) +exception InductiveError = Type_errors.InductiveError (************************************************************************) (************************************************************************) @@ -706,21 +367,20 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( If [chkpos] is [false] then positivity is assumed, and [check_positivity_one] computes the subterms occurrences in a best-effort fashion. *) -let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = +let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds = let ntypes = Array.length inds in let recursive = finite != BiFinite in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in let ra_env_ar = Array.rev_to_list rc in let nparamsctxt = Context.Rel.length paramsctxt in let nmr = Context.Rel.nhyps paramsctxt in - let check_one i (_,lcnames,lc,(sign,_)) = + let check_one i (_,lcnames) (nindices,lc) = let ra_env_ar_par = List.init nparamsctxt (fun _ -> (Norec,mk_norec)) @ ra_env_ar in let ienv = (env_ar_par, 1+nparamsctxt, ntypes, ra_env_ar_par) in - let nnonrecargs = Context.Rel.nhyps sign - nmr in - check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nnonrecargs lcnames lc + check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nindices lcnames lc in - let irecargs_nmr = Array.mapi check_one inds in + let irecargs_nmr = Array.map2_i check_one names inds in let irecargs = Array.map snd irecargs_nmr and nmr' = array_min nmr irecargs_nmr in (nmr',Rtree.mk_rec irecargs) @@ -730,48 +390,17 @@ let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = (************************************************************************) (* Build the inductive packet *) -(* Allowed eliminations *) - -let all_sorts = [InProp;InSet;InType] -let small_sorts = [InProp;InSet] -let logical_sorts = [InProp] - -let allowed_sorts is_smashed s = - if not is_smashed - then (** Naturally in the defined sort. - If [s] is Prop, it must be small and unitary. - Unsmashed, predicative Type and Set: all elimination allowed - as well. *) - all_sorts - else - match Sorts.family s with - (* Type: all elimination allowed: above and below *) - | InType -> all_sorts - (* Smashed Set is necessarily impredicative: forbids large elimination *) - | InSet -> small_sorts - (* Smashed to Prop, no informative eliminations allowed *) - | InProp -> logical_sorts - -(* Previous comment: *) -(* Unitary/empty Prop: elimination to all sorts are realizable *) -(* unless the type is large. If it is large, forbids large elimination *) -(* which otherwise allows simulating the inconsistent system Type:Type. *) -(* -> this is now handled by is_smashed: *) -(* - all_sorts in case of small, unitary Prop (not smashed) *) -(* - logical_sorts in case of large, unitary Prop (smashed) *) - -let arity_conclusion = function - | RegularArity (_, c, _) -> c - | TemplateArity (_, s) -> mkType s +let repair_arity indices = function + | RegularArity ar -> ar.mind_user_arity + | TemplateArity ar -> mkArity (indices,Sorts.sort_of_univ ar.template_level) let fold_inductive_blocks f = - Array.fold_left (fun acc (_,_,lc,(arsign,ar)) -> - f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (arity_conclusion ar) arsign)) + Array.fold_left (fun acc ((arity,lc),(indices,_),_) -> + f (Array.fold_left f acc lc) (repair_arity indices arity)) let used_section_variables env inds = - let ids = fold_inductive_blocks - (fun l c -> Id.Set.union (Environ.global_vars_set env c) l) - Id.Set.empty inds in + let fold l c = Id.Set.union (Environ.global_vars_set env c) l in + let ids = fold_inductive_blocks fold Id.Set.empty inds in keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) @@ -842,56 +471,21 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev labs), Array.of_list (List.rev pbs) -let abstract_inductive_universes iu = - match iu with - | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) - | Polymorphic_ind_entry (nas, ctx) -> - let (inst, auctx) = Univ.abstract_universes nas ctx in - let inst = Univ.make_instance_subst inst in - (inst, Polymorphic_ind auctx) - | Cumulative_ind_entry (nas, cumi) -> - let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in - let inst = Univ.make_instance_subst inst in - (inst, Cumulative_ind acumi) - -let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in let nparamargs = Context.Rel.nhyps paramsctxt in - let nparamsctxt = Context.Rel.length paramsctxt in - let substunivs, aiu = abstract_inductive_universes iu in - let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in - let env_ar = - let ctxunivs = Environ.rel_context env_ar in - let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in - Environ.push_rel_context ctxunivs' env - in (* Check one inductive *) - let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg = + let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg = (* Type of constructors in normal form *) - let lc = Array.map (Vars.subst_univs_level_constr substunivs) lc in - let splayed_lc = Array.map (dest_prod_assum env_ar) lc in - let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in + let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b (d@paramsctxt)) splayed_lc in let consnrealdecls = - Array.map (fun (d,_) -> Context.Rel.length d - nparamsctxt) + Array.map (fun (d,_) -> Context.Rel.length d) splayed_lc in let consnrealargs = - Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs) + Array.map (fun (d,_) -> Context.Rel.nhyps d) splayed_lc in - (* Elimination sorts *) - let arkind,kelim = - match ar_kind with - | TemplateArity (paramlevs, lev) -> - let ar = {template_param_levels = paramlevs; template_level = lev} in - TemplateArity ar, all_sorts - | RegularArity (info,ar,defs) -> - let s = Sorts.sort_of_univ defs in - let kelim = allowed_sorts info s in - let ar = RegularArity - { mind_user_arity = Vars.subst_univs_level_constr substunivs ar; - mind_sort = Sorts.sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in - ar, kelim in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in let transf num = @@ -908,10 +502,10 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r let rtbl = Array.init (List.length cnames) transf in (* Build the inductive packet *) { mind_typename = id; - mind_arity = arkind; - mind_arity_ctxt = Vars.subst_univs_level_context substunivs ar_sign; - mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs; - mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt; + mind_arity = arity; + mind_arity_ctxt = indices @ paramsctxt; + mind_nrealargs = Context.Rel.nhyps indices; + mind_nrealdecls = Context.Rel.length indices; mind_kelim = kelim; mind_consnames = Array.of_list cnames; mind_consnrealdecls = consnrealdecls; @@ -923,7 +517,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r mind_nb_args = !nblock; mind_reloc_tbl = rtbl; } in - let packets = Array.map2 build_one_packet inds recargs in + let packets = Array.map3 build_one_packet names inds recargs in let mib = (* Build the mutual inductive *) { mind_record = NotRecord; @@ -934,7 +528,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r mind_nparams_rec = nmr; mind_params_ctxt = paramsctxt; mind_packets = packets; - mind_universes = aiu; + mind_universes = univs; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -942,7 +536,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r let record_info = match isrecord with | Some (Some rid) -> let is_record pkt = - pkt.mind_kelim == all_sorts + List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim && Array.length pkt.mind_consnames == 1 && pkt.mind_consnrealargs.(0) > 0 in @@ -965,11 +559,17 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r let check_inductive env kn mie = (* First type-check the inductive definition *) - let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in + let (env_ar_par, univs, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in (* Then check positivity conditions *) let chkpos = (Environ.typing_flags env).check_guarded in - let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in + let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) + mie.mind_entry_inds + in + let (nmr,recargs) = check_positivity ~chkpos kn names + env_ar_par paramsctxt mie.mind_entry_finite + (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) + in (* Build the inductive packets *) - build_inductive env mie.mind_entry_private mie.mind_entry_universes - env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite + build_inductive env names mie.mind_entry_private univs + paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 840e23ed69..7810c1723e 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -14,12 +14,10 @@ open Declarations open Environ open Entries -(** Inductive type checking and errors *) - -(** The different kinds of errors that may result of a malformed inductive - definition. *) +(** Check an inductive. *) +val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body -(** Errors related to inductive constructions *) +(** Deprecated *) type inductive_error = | NonPos of env * constr * constr | NotEnoughArgs of env * constr * constr @@ -31,22 +29,8 @@ type inductive_error = | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType + | BadUnivs +[@@ocaml.deprecated "Use [Type_errors.inductive_error]"] -exception InductiveError of inductive_error - -val infos_and_sort : env -> constr -> Univ.Universe.t - -val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit - -val check_positivity : chkpos:bool -> - Names.MutInd.t -> - Environ.env -> - (Constr.constr, Constr.types) Context.Rel.pt -> - Declarations.recursivity_kind -> - ('a * Names.Id.t list * Constr.types array * - (('b, 'c) Context.Rel.pt * 'd)) - array -> Int.t * Declarations.recarg Rtree.t array - -(** The following function does checks on inductive declarations. *) - -val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body +exception InductiveError of Type_errors.inductive_error +[@@ocaml.deprecated "Use [Type_errors.InductiveError]"] diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 54c239349d..0b10e788b6 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -39,6 +39,7 @@ Type_errors Modops Inductive Typeops +IndTyping Indtypes Cooking Term_typing diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 60293fe864..fd050085d7 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -68,6 +68,21 @@ type type_error = (constr, types) ptype_error exception TypeError of env * type_error +type inductive_error = + | NonPos of env * constr * constr + | NotEnoughArgs of env * constr * constr + | NotConstructor of env * Id.t * constr * constr * int * int + | NonPar of env * constr * int * constr * constr + | SameNamesTypes of Id.t + | SameNamesConstructors of Id.t + | SameNamesOverlap of Id.t list + | NotAnArity of env * constr + | BadEntry + | LargeNonPropInductiveNotInType + | BadUnivs + +exception InductiveError of inductive_error + let nfj env {uj_val=c;uj_type=ct} = {uj_val=c;uj_type=nf_betaiota env ct} diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 3fd40a7f42..3e954d6a8e 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -69,6 +69,25 @@ type type_error = (constr, types) ptype_error exception TypeError of env * type_error +(** The different kinds of errors that may result of a malformed inductive + definition. *) +type inductive_error = + | NonPos of env * constr * constr + | NotEnoughArgs of env * constr * constr + | NotConstructor of env * Id.t * constr * constr * int * int + | NonPar of env * constr * int * constr * constr + | SameNamesTypes of Id.t + | SameNamesConstructors of Id.t + | SameNamesOverlap of Id.t list + | NotAnArity of env * constr + | BadEntry + | LargeNonPropInductiveNotInType + | BadUnivs + +exception InductiveError of inductive_error + +(** Raising functions *) + val error_unbound_rel : env -> int -> 'a val error_unbound_var : env -> variable -> 'a @@ -284,15 +284,12 @@ let pr_vertical_list pr = function [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *) let prvecti_with_sep sep elem v = - let rec pr i = - if Int.equal i 0 then - elem 0 v.(0) - else - let r = pr (i-1) and s = sep () and e = elem i v.(i) in - r ++ s ++ e + let v = CArray.mapi (fun i x -> + let pp = if i = 0 then mt() else sep() in + pp ++ elem i x) + v in - let n = Array.length v in - if Int.equal n 0 then mt () else pr (n - 1) + seq (Array.to_list v) (* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f40b3e901b..454a4b66e7 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -214,6 +214,6 @@ let classify_vernac e = | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow - | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + | (VtStartProof _ | VtUnknown), _ -> VtQuery, VtLater) in static_control_classifier e diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 64f19e1fd9..69c1d9bd23 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -95,6 +95,7 @@ let schedule_vio_checking j fs = done; let pid, ret = Unix.wait () in if ret <> Unix.WEXITED 0 then rc := 1; + Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; exit !rc @@ -124,6 +125,7 @@ let schedule_vio_compilation j fs = | s :: rest -> s :: filter_argv b rest in let prog = Sys.argv.(0) in let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in + let all_jobs = !jobs in let make_job () = let f, t = List.hd !jobs in jobs := List.tl !jobs; @@ -137,8 +139,15 @@ let schedule_vio_compilation j fs = done; let pid, ret = Unix.wait () in if ret <> Unix.WEXITED 0 then rc := 1; + Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; + if !rc = 0 then begin + (* set the access and last modification time of all files to the same t + * not to confuse make into thinking that some of them are outdated *) + let t = Unix.gettimeofday () in + List.iter (fun (f,_) -> Unix.utimes (f^".vo") t t) all_jobs; + end; exit !rc diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v new file mode 100644 index 0000000000..a80f3233a3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9300.v @@ -0,0 +1,6 @@ +Existing Class True. + +Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined. + +Fail Check foo (n := 3) true (s := (4 , 5)). +Check foo (n := 3) (b := true) (4 , 5). diff --git a/test-suite/unit-tests/lib/pp_big_vect.ml b/test-suite/unit-tests/lib/pp_big_vect.ml new file mode 100644 index 0000000000..e1cdd290e2 --- /dev/null +++ b/test-suite/unit-tests/lib/pp_big_vect.ml @@ -0,0 +1,14 @@ +open OUnit +open Pp + +let pr_big_vect = + let n = "pr_big_vect" in + n >:: (fun () -> + let v = Array.make (1 lsl 20) () in + let pp = prvecti_with_sep spc (fun _ _ -> str"x") v in + let str = string_of_ppcmds pp in + ignore(str)) + +let tests = [pr_big_vect] + +let () = Utest.run_tests __FILE__ (Utest.open_log_out_ch __FILE__) tests diff --git a/vernac/classes.ml b/vernac/classes.ml index 370df615fc..a342f5bf98 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -301,10 +301,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass in - let sigma, k, u, cty, ctx', ctx, len, imps, subst = + let sigma, k, u, cty, ctx', ctx, imps, subst = let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in - let len = List.length ctx in + let len = Context.Rel.nhyps ctx in let imps = imps @ Impargs.lift_implicits len imps' in let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in @@ -320,7 +320,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args')) cl_context (args, []) in - sigma, cl, u, c', ctx', ctx, len, imps, args + sigma, cl, u, c', ctx', ctx, imps, args in let id = match instid with diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 348e76da62..92b1ff7572 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -24,7 +24,7 @@ open Constrexpr_ops open Constrintern open Impargs open Reductionops -open Indtypes +open Type_errors open Pretyping open Indschemes open Context.Rel.Declaration @@ -35,7 +35,7 @@ module RelDecl = Context.Rel.Declaration (* 3b| Mutual inductive definitions *) let warn_auto_template = - CWarnings.create ~name:"auto-template" ~category:"vernacular" + CWarnings.create ~name:"auto-template" ~category:"vernacular" ~default:CWarnings.Disabled (fun id -> Pp.(strbrk "Automatically declaring " ++ Id.print id ++ strbrk " as template polymorphic. Use attributes or " ++ @@ -304,7 +304,7 @@ let inductive_levels env evd poly arities inds = let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then - raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) + raise (InductiveError LargeNonPropInductiveNotInType) else evd else evd (* Evd.set_leq_sort env evd (Type cu) du *) diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index e1496e58d7..71770a21ca 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -10,7 +10,6 @@ open Pp open CErrors -open Indtypes open Type_errors open Pretype_errors open Indrec diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f3e1e1fc49..ebbec86b9c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -15,7 +15,6 @@ open Nameops open Namegen open Constr open Termops -open Indtypes open Environ open Pretype_errors open Type_errors @@ -1163,6 +1162,9 @@ let error_bad_entry () = let error_large_non_prop_inductive_not_in_type () = str "Large non-propositional inductive types must be in Type." +let error_inductive_bad_univs () = + str "Incorrect universe constrains declared for inductive type." + (* Recursion schemes errors *) let error_not_allowed_case_analysis env isrec kind i = @@ -1199,7 +1201,8 @@ let explain_inductive_error = function | NotAnArity (env, c) -> error_not_an_arity env c | BadEntry -> error_bad_entry () | LargeNonPropInductiveNotInType -> - error_large_non_prop_inductive_not_in_type () + error_large_non_prop_inductive_not_in_type () + | BadUnivs -> error_inductive_bad_univs () (* Recursion schemes errors *) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index bab66b2af4..986906d303 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Indtypes open Environ open Type_errors open Pretype_errors |