diff options
137 files changed, 2694 insertions, 883 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index b0e79fb1b2..2a641263e3 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -71,6 +71,8 @@ azure-pipelines.yml @coq/ci-maintainers /man/ @silene # Secondary maintainer @maximedenes +/doc/plugin_tutorial/ @ybertot + ########## Coqchk ########## /checker/ @ppedrot 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 5bcf94eda8..e981c592a2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -151,7 +151,7 @@ after_script: - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH" - - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all + - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" COQFLAGS="${COQFLAGS}" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -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: @@ -257,6 +263,18 @@ windows32: except: - /^pr-.*$/ +lint: + image: docker:git + stage: test + script: + - apk add bash + - dev/lint-repository.sh + dependencies: [] + before_script: [] + variables: + # we need an unknown amount of history for per-commit linting + GIT_DEPTH: "" + pkg:opam: stage: test # OPAM will build out-of-tree so no point in importing artifacts @@ -415,6 +433,13 @@ test-suite:edge+trunk+dune: expire_in: 1 week allow_failure: true +test-suite:base+async: + <<: *test-suite-template + dependencies: + - build:base + variables: + COQFLAGS: "-async-proofs on" + validate:base: <<: *validate-template dependencies: @@ -442,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 @@ -473,7 +503,7 @@ library:ci-fiat-crypto-legacy: library:ci-flocq: <<: *ci-template -library:ci-formal-topology: +library:ci-corn: <<: *ci-template-flambda library:ci-geocoq: @@ -494,6 +524,9 @@ library:ci-sf: library:ci-unimath: <<: *ci-template-flambda +library:ci-verdi-raft: + <<: *ci-template-flambda + library:ci-vst: <<: *ci-template-flambda @@ -529,8 +562,12 @@ plugin:ci-mtac2: plugin:ci-paramcoq: <<: *ci-template -plugin:ci-plugin_tutorial: - <<: *ci-template +plugin:plugin-tutorial: + stage: test + dependencies: [] + script: + - ./configure -local -warn-error yes + - make -j "$NJOBS" plugin-tutorial plugin:ci-quickchick: <<: *ci-template-flambda @@ -10,6 +10,7 @@ ## either amend this file and commit it, or contact the coqdev list Abhishek Anand <abhishek.anand.iitg@gmail.com> Abhishek Anand (@brixpro-home) <abhishek.anand.iitg@gmail.com> +Léo Andrès <leo@ndrs.fr> zapashcanon <leo@ndrs.fr> Jim Apple <github.public@jbapple.com> jbapple <github.public@jbapple.com> Bruno Barras <bruno.barras@inria.fr> barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> Bruno Barras <bruno.barras@inria.fr> barras-local <barras-local@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -19,9 +20,11 @@ Yves Bertot <yves.bertot@inria.fr> Yves Bertot <bertot@inria.fr> Yves Bertot <yves.bertot@inria.fr> Yves Bertot <Yves.Bertot@inria.fr> Frédéric Besson <frederic.besson@inria.fr> fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> Siddharth Bhat <siddu.druid@gmail.com> Siddharth <siddu.druid@gmail.com> +Simon Boulier <simon.boulier@ens-rennes.fr> SimonBoulier <simon.boulier@ens-rennes.fr> Pierre Boutillier <pierre.boutillier@ens-lyon.org> pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> +Arthur Charguéraud <arthur@chargueraud.org> charguer <arthur@chargueraud.org> Xavier Clerc <xavier.clerc@inria.fr> xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> Xavier Clerc <xavier.clerc@inria.fr> xclerc <xavier.clerc@inria.fr> Pierre Corbineau <Pierre.Corbineau@NOSPAM@imag.fr> corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -32,6 +35,7 @@ Maxime Dénès <mail@maximedenes.fr> mdenes <mdenes@85f007b7-540 Maxime Dénès <mail@maximedenes.fr> Maxime Denes <maximedenes@gillespie.inria.fr> Olivier Desmettre <desmettr@gforge> desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> Damien Doligez <doligez@gforge> doligez <doligez@85f007b7-540e-0410-9357-904b9bb8a0f7> +İsmail Dönmez <ismail-s@users.noreply.github.com> Ismail <ismail-s@users.noreply.github.com> Andres Erbsen <andreser@mit.edu> Andres Erbsen <andres@kevix.co> Jim Fehrle <jfehrle@sbcglobal.net> Jim <jfehrle@sbcglobal.net> Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -63,11 +67,14 @@ Florent Kirchner <fkirchne@gforge> kirchner <kirchner@85f007b7-5 Johannes Kloos <jkloos@mpi-sws.org> jkloos <jkloos@mpi-sws.org> Matej Košík <matej.kosik@inria.fr> Matej Kosik <m4tej.kosik@gmail.com> Matej Košík <matej.kosik@inria.fr> Matej Kosik <matej.kosik@inria.fr> +Ambroise Lafont <chaster_killer@hotmail.fr> amblaf <you@example.com> +Ambroise Lafont <chaster_killer@hotmail.fr> Ambroise <chaster_killer@hotmail.fr> Vincent Laporte <Vincent.Laporte@fondation-inria.fr> Vincent Laporte <Vincent.Laporte@gmail.com> Marc Lasson <marc.lasson@gmail.com> mlasson <marc.lasson@gmail.com> William Lawvere <mundungus.corleone@gmail.com> william-lawvere <mundungus.corleone@gmail.com> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <pierre.letouzey@inria.fr> +Xia Li-yao <lysxia@gmail.com> Lysxia <lysxia@gmail.com> Assia Mahboubi <assia.mahboubi@inria.fr> amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> Evgeny Makarov <emakarov@gforge> emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> Gregory Malecha <gmalecha@eecs.harvard.edu> Gregory Malecha <gmalecha@cs.harvard.edu> @@ -88,6 +95,7 @@ Russell O'Connor <roconnor@blockstream.io> roconnor-blockstream <roconno Christine Paulin <cpaulin@gforge> cpaulin <cpaulin@85f007b7-540e-0410-9357-904b9bb8a0f7> Christine Paulin <cpaulin@gforge> mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> +Frederic Peschanski <frederic.peschanski@lip6.fr> fredokun <frederic.peschanski@lip6.fr> Clément Pit-Claudel <clement.pitclaudel@live.com> Clément Pit--Claudel <clement.pitclaudel@live.com> Loïc Pottier <pottier@gforge> pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7> Matthias Puech <puech@gforge> puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -98,6 +106,7 @@ Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel De Rauglaudre <ddr@g Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7> Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> Regis-Gianas <yrg@pps.univ-paris-diderot.fr> Clément Renard <clrenard@gforge> clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> +Matthew Ryan <mr_1993@hotmail.co.uk> mrmr1993 <mr_1993@hotmail.co.uk> Claudio Sacerdoti Coen <sacerdot@gforge> sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> Kazuhiko Sakaguchi <pi8027@gmail.com> Kazuhiko Sakaguchi <sakaguchi@coins.tsukuba.ac.jp> Vincent Siles <vsiles@gforge> vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -108,6 +117,7 @@ Matthieu Sozeau <mattam@mattam.org> Matthieu Sozeau <matthieu.soz Matthieu Sozeau <mattam@mattam.org> Matthieu Sozeau <mattam@eduroam-prg-sg-1-46-137.net.univ-paris-diderot.fr> Arnaud Spiwack <arnaud@spiwack.net> aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> Paul Steckler <steck@stecksoft.com> Paul Steckler <psteck@mit.edu> +Frank Steffahn <fdsteffahn@gmail.com> staffehn <fdsteffahn@gmail.com> Enrico Tassi <Enrico.Tassi@inria.fr> gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <enrico.tassi@inria.fr> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <gares@fettunta.org> @@ -123,5 +133,8 @@ Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> Théo Zimmermann <theo. # Anonymous accounts anonymous < > coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> -anonymous < > (no author) <(no author)@85f007b7-540e-0410-9357-904b9bb8a0f7> -anonymous < > serpyc <serpyc@85f007b7-540e-0410-9357-904b9bb8a0f7> + +# Bot accounts + +cvs2svn < > (no author) <(no author)@85f007b7-540e-0410-9357-904b9bb8a0f7> +serpyc-bot < > serpyc <serpyc@85f007b7-540e-0410-9357-904b9bb8a0f7> diff --git a/.travis.yml b/.travis.yml index 02b94f4a8e..855d36048d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -28,17 +28,6 @@ env: matrix: include: - - env: - - TEST_TARGET="lint" - install: [] - before_script: [] - addons: - apt: - sources: [] - packages: [] - script: - - dev/lint-repository.sh - - os: osx env: - TEST_TARGET="test-suite" 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: @@ -61,7 +61,8 @@ FIND_SKIP_DIRS:='(' \ -name 'user-contrib' -o \ -name 'test-suite' -o \ -name '.opamcache' -o \ - -name '.coq-native' \ + -name '.coq-native' -o \ + -name 'plugin_tutorial' \ ')' -prune -o define find @@ -191,7 +192,7 @@ META.coq: META.coq.in # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean plugin-tutorialclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean @@ -237,7 +238,7 @@ docclean: rm -f doc/coq.tex rm -rf doc/sphinx/_build -archclean: clean-ide optclean voclean +archclean: clean-ide optclean voclean plugin-tutorialclean rm -rf _build rm -f $(ALLSTDLIB).* @@ -268,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 {} + @@ -278,6 +279,9 @@ timingclean: -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + +plugin-tutorialclean: + +$(MAKE) -C $(PLUGINTUTO) clean + # Ensure that every compiled file around has a known source file. # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. 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.ci b/Makefile.ci index 2df6a792b6..b8bff98f5f 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -27,7 +27,6 @@ CI_TARGETS= \ ci-fiat-crypto-legacy \ ci-fiat-parsers \ ci-flocq \ - ci-formal-topology \ ci-geocoq \ ci-coqhammer \ ci-hott \ @@ -37,13 +36,13 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ - ci-plugin_tutorial \ ci-quickchick \ ci-relation-algebra \ ci-sf \ ci-simple-io \ ci-tlc \ ci-unimath \ + ci-verdi-raft \ ci-vst .PHONY: ci-all $(CI_TARGETS) @@ -63,8 +62,6 @@ ci-corn: ci-math-classes ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io -ci-formal-topology: ci-corn - # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* diff --git a/Makefile.common b/Makefile.common index 9f7ed9d46e..2dced04967 100644 --- a/Makefile.common +++ b/Makefile.common @@ -168,6 +168,8 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) ALLSTDLIB := test-suite/misc/universes/all_stdlib +PLUGINTUTO := doc/plugin_tutorial + # For emacs: # Local Variables: # mode: makefile 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 9e6ec4955a..7ac710b8c9 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -89,6 +89,10 @@ stdlib: \ full-stdlib: \ doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf +.PHONY: plugin-tutorial +plugin-tutorial: states tools + +$(MAKE) COQBIN=$(PWD)/bin/ -C $(PLUGINTUTO) + ###################################################################### ### Implicit rules ###################################################################### @@ -137,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,19 +1,68 @@ # Coq -[](https://gitlab.com/coq/coq/commits/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/README-developers.md b/dev/ci/README-developers.md index fa8962a06f..6663fbecf8 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -10,12 +10,14 @@ We are currently running tests on the following platforms: - GitLab CI is the main CI platform. It tests the compilation of Coq, of the documentation, and of CoqIDE on Linux with several versions of OCaml and with warnings as errors; it runs the test-suite and - tests the compilation of several external developments. + tests the compilation of several external developments. It also runs + a linter that checks whitespace discipline. A [pre-commit + hook](../tools/pre-commit) is automatically installed by + `./configure`. It should allow complying with this discipline + without pain. - Travis CI is used to test the compilation of Coq and run the test-suite on - macOS. It also runs a linter that checks whitespace discipline. A - [pre-commit hook](../tools/pre-commit) is automatically installed by - `./configure`. It should allow complying with this discipline without pain. + macOS. - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e0f4f50fa9..8dee465cf4 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -150,11 +150,11 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# formal-topology +# fiat_crypto_legacy ######################################################################## -: "${formal_topology_CI_REF:=ci}" -: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" -: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" +: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" +: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" ######################################################################## # coq_dpdgraph @@ -240,13 +240,6 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## -# plugin_tutorial -######################################################################## -: "${plugin_tutorial_CI_REF:=master}" -: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" -: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" - -######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" @@ -273,3 +266,26 @@ : "${relation_algebra_CI_REF:=master}" : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" : "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}" + +######################################################################## +# StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft +######################################################################## +: "${struct_tact_CI_REF:=master}" +: "${struct_tact_CI_GITURL:=https://github.com/uwplse/StructTact}" +: "${struct_tact_CI_ARCHIVEURL:=${struct_tact_CI_GITURL}/archive}" + +: "${inf_seq_ext_CI_REF:=master}" +: "${inf_seq_ext_CI_GITURL:=https://github.com/DistributedComponents/InfSeqExt}" +: "${inf_seq_ext_CI_ARCHIVEURL:=${inf_seq_ext_CI_GITURL}/archive}" + +: "${cheerios_CI_REF:=master}" +: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}" +: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}" + +: "${verdi_CI_REF:=master}" +: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}" +: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}" + +: "${verdi_raft_CI_REF:=master}" +: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" +: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index 6bf3138346..2af4b58201 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -4,11 +4,11 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" FORCE_GIT=1 -git_download fiat_crypto +git_download fiat_crypto_legacy fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ +( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ ./etc/ci/remove_autogenerated.sh && \ make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) 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/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh deleted file mode 100755 index 8be5a06ed2..0000000000 --- a/dev/ci/ci-formal-topology.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download formal_topology - -( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-plugin_tutorial.sh b/dev/ci/ci-plugin_tutorial.sh deleted file mode 100755 index 6c26a71a21..0000000000 --- a/dev/ci/ci-plugin_tutorial.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download plugin_tutorial - -( cd "${CI_BUILD_DIR}/plugin_tutorial" && \ - pushd tuto0 && make && popd && \ - pushd tuto1 && make && popd && \ - pushd tuto2 && make && popd && \ - pushd tuto3 && make && popd ) diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi-raft.sh new file mode 100755 index 0000000000..3bcd52c464 --- /dev/null +++ b/dev/ci/ci-verdi-raft.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download struct_tact + +( cd "${CI_BUILD_DIR}/struct_tact" && ./configure && make && make install ) + +git_download inf_seq_ext + +( cd "${CI_BUILD_DIR}/inf_seq_ext" && ./configure && make && make install ) + +git_download cheerios + +( cd "${CI_BUILD_DIR}/cheerios" && ./configure && make && make install ) + +git_download verdi + +( cd "${CI_BUILD_DIR}/verdi" && ./configure && make && make install ) + +git_download verdi_raft + +( cd "${CI_BUILD_DIR}/verdi_raft" && ./configure && make ) 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/lint-repository.sh b/dev/lint-repository.sh index cd09b6d305..f588c20d02 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -4,33 +4,25 @@ # lint-commits.sh seeks to prevent the worsening of already present # problems, such as tab indentation in ml files. lint-repository.sh -# seeks to prevent the (re-)introduction of solved problems, such as -# newlines at the end of .v files. +# also seeks to prevent the (re-)introduction of solved problems, such +# as newlines at the end of .v files. CODE=0 -if [ -n "${TRAVIS_PULL_REQUEST}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ]; -then - # skip PRs from before the linter existed - if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ]; - then - 1>&2 echo "Linting skipped: pull request older than the linter." - exit 0 - fi - - # Some problems are too widespread to fix in one commit, but we - # can still check that they don't worsen. - CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*} - PR_HEAD=${TRAVIS_COMMIT_RANGE##*...} - MERGE_BASE=$(git merge-base "$CUR_HEAD" "$PR_HEAD") - dev/lint-commits.sh "$MERGE_BASE" "$PR_HEAD" || CODE=1 -fi +# We assume that all merge commits are from the main branch +# For Coq it is extremely rare for this assumption to be broken +read -r base < <(git log -n 1 --merges --pretty='format:%H') +head=$(git rev-parse HEAD) + +dev/lint-commits.sh "$base" "$head" || CODE=1 # Check that the files with 'whitespace' gitattribute end in a newline. # xargs exit status is 123 if any file failed the test +echo Checking end of file newlines find . "(" -path ./.git -prune ")" -o -type f -print0 | xargs -0 dev/tools/check-eof-newline.sh || CODE=1 +echo Checking overlays dev/tools/check-overlays.sh || CODE=1 exit $CODE 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/README.md b/doc/README.md index 3db1261656..c41d269437 100644 --- a/doc/README.md +++ b/doc/README.md @@ -101,18 +101,21 @@ Alternatively, you can use some specific targets: Also note the `-with-doc yes` option of `./configure` to enable the build of the documentation as part of the default make target. -If you're editing Sphinx documentation, set SPHINXWARNERROR to 0 -to avoid treating Sphinx warnings as errors. Otherwise, Sphinx quits -upon detecting the first warning. You can set this on the Sphinx `make` -command line or as an environment variable: - -- `make refman SPHINXWARNERROR=0` - -- ~~~ - export SPHINXWARNERROR=0 - ⋮ - make refman - ~~~ +To build the Sphinx documentation without stopping at the first +warning with the legacy Makefile, set `SPHINXWARNERROR` to 0 as such: + +``` +SPHINXWARNERROR=0 make refman-html +``` + +To do the same with the Dune build system, change the value of the +`SPHINXWARNOPT` variable (default is `-W`). The following will build +the Sphinx documentation without stopping at the first warning, and +store all the warnings in the file `/tmp/warn.log`: + +``` +SPHINXWARNOPT="-w/tmp/warn.log" dune build @refman-html +``` Installation ------------ @@ -10,8 +10,10 @@ ; + tools/coqdoc/coqdoc.css (package coq) (source_tree sphinx) - (source_tree tools)) - (action (run sphinx-build -j4 -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (source_tree tools) + (env_var SPHINXWARNOPT)) + (action + (run sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) diff --git a/doc/plugin_tutorial/.gitignore b/doc/plugin_tutorial/.gitignore new file mode 100644 index 0000000000..3e4978fac4 --- /dev/null +++ b/doc/plugin_tutorial/.gitignore @@ -0,0 +1,13 @@ +*.ml*.d +*.cm[ixt]* +Makefile.coq* +*~ +*.[ao] +.coqdeps.d +*.vo +*.glob +*.aux +*/*/.merlin + +# by convention g_foo.ml is generated +g_*.ml diff --git a/doc/plugin_tutorial/.travis.yml b/doc/plugin_tutorial/.travis.yml new file mode 100644 index 0000000000..556e0ac45a --- /dev/null +++ b/doc/plugin_tutorial/.travis.yml @@ -0,0 +1,38 @@ +dist: trusty +sudo: required +language: generic + +services: + - docker + +env: + global: + - NJOBS="2" + - CONTRIB_NAME="plugin_tutorials" + matrix: + - COQ_IMAGE="coqorg/coq:dev" + +install: | + # Prepare the COQ container + docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/$CONTRIB_NAME -w /home/coq/$CONTRIB_NAME ${COQ_IMAGE} + docker exec COQ /bin/bash --login -c " + # This bash script is double-quoted to interpolate Travis CI env vars: + echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\" + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex # -e = exit on failure; -x = trace for debug + opam list + " +script: +- echo -e "${ANSI_YELLOW}Building $CONTRIB_NAME...${ANSI_RESET}" && echo -en 'travis_fold:start:testbuild\\r' +- | + docker exec COQ /bin/bash --login -c " + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex + sudo chown -R coq:coq /home/coq/$CONTRIB_NAME + ( cd tuto0 && make ) + ( cd tuto1 && make ) + ( cd tuto2 && make ) + ( cd tuto3 && make ) + " +- docker stop COQ # optional +- echo -en 'travis_fold:end:testbuild\\r' diff --git a/doc/plugin_tutorial/LICENSE b/doc/plugin_tutorial/LICENSE new file mode 100644 index 0000000000..cf1ab25da0 --- /dev/null +++ b/doc/plugin_tutorial/LICENSE @@ -0,0 +1,24 @@ +This is free and unencumbered software released into the public domain. + +Anyone is free to copy, modify, publish, use, compile, sell, or +distribute this software, either in source code form or as a compiled +binary, for any purpose, commercial or non-commercial, and by any +means. + +In jurisdictions that recognize copyright laws, the author or authors +of this software dedicate any and all copyright interest in the +software to the public domain. We make this dedication for the benefit +of the public at large and to the detriment of our heirs and +successors. We intend this dedication to be an overt act of +relinquishment in perpetuity of all present and future rights to this +software under copyright law. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR +OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, +ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +OTHER DEALINGS IN THE SOFTWARE. + +For more information, please refer to <http://unlicense.org> diff --git a/doc/plugin_tutorial/Makefile b/doc/plugin_tutorial/Makefile new file mode 100644 index 0000000000..7f1833fadd --- /dev/null +++ b/doc/plugin_tutorial/Makefile @@ -0,0 +1,21 @@ + +TUTOS:= \ + tuto0 \ + tuto1 \ + tuto2 \ + tuto3 + +all: $(TUTOS) + +.PHONY: $(TUTOS) all + +$(TUTOS): %: + +$(MAKE) -C $@ + +CLEANS:=$(addsuffix -clean, $(TUTOS)) +.PHONY: clean $(CLEANS) + +clean: $(CLEANS) + +%-clean: + +$(MAKE) -C $* clean diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md new file mode 100644 index 0000000000..f82edb2352 --- /dev/null +++ b/doc/plugin_tutorial/README.md @@ -0,0 +1,86 @@ +How to write plugins in Coq +=========================== + # Working environment : merlin, tuareg (open question) + + ## OCaml & related tools + + These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) + +```shell +opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2 +eval `opam config env --root=$PWD/CIW2018` +opam install camlp5 ocamlfind num # Coq's dependencies +opam install lablgtk # Coqide's dependencies (optional) +opam install merlin # prints instructions for vim and emacs +``` + + ## Coq + +```shell +git clone git@github.com:coq/coq.git +cd coq +./configure -profile devel +make -j2 +cd .. +export PATH=$PWD/coq/bin:$PATH +``` + + ## This tutorial + +```shell +git clone git@github.com:ybertot/plugin_tutorials.git +cd plugin_tutorials/tuto0 +make .merlin # run before opening .ml files in your editor +make # build +``` + + + + # tuto0 : basics of project organization + package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` + - Example of syntax to add a new toplevel command + - Example of function call to print a simple message + - Example of syntax to add a simple tactic + (that does nothing and prints a message) + - To use it: + +```bash + cd tuto0; make + coqtop -I src -R theories Tuto0 +``` + + In the Coq session type: +```coq + Require Import Tuto0.Loader. HelloWorld. +``` + + # tuto1 : Ocaml to Coq communication + Explore the memory of Coq, modify it + - Commands that take arguments: strings, symbols, expressions of the calculus of constructions + - Commands that interact with type-checking in Coq + - A command that adds a new definition or theorem + - A command that uses a name and exploits the existing definitions + or theorems + - A command that exploits an existing ongoing proof + - A command that defines a new tactic + + Compilation and loading must be performed as for `tuto0`. + + # tuto2 : Ocaml to Coq communication + A more step by step introduction to writing commands + - Explanation of the syntax of entries + - Adding a new type to and parsing to the available choices + - Handling commands that store information in user-chosen registers and tables + + Compilation and loading must be performed as for `tuto1`. + + # tuto3 : manipulating terms of the calculus of constructions + Manipulating terms, inside commands and tactics. + - Obtaining existing values from memory + - Composing values + - Verifying types + - Using these terms in commands + - Using these terms in tactics + - Automatic proofs without tactics using type classes and canonical structures + + compilation and loading must be performed as for `tuto0`. diff --git a/doc/plugin_tutorial/tuto0/Makefile b/doc/plugin_tutorial/tuto0/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto0/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto0/_CoqProject b/doc/plugin_tutorial/tuto0/_CoqProject new file mode 100644 index 0000000000..76368e3ac7 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/_CoqProject @@ -0,0 +1,10 @@ +-R theories/ Tuto0 +-I src + +theories/Loader.v +theories/Demo.v + +src/tuto0_main.ml +src/tuto0_main.mli +src/g_tuto0.mlg +src/tuto0_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune new file mode 100644 index 0000000000..79d561061d --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto0_plugin) + (public_name coq.plugins.tutorial.p0) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto0.ml) + (deps (:pp-file g_tuto0.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg new file mode 100644 index 0000000000..5c633fe862 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg @@ -0,0 +1,18 @@ +DECLARE PLUGIN "tuto0_plugin" + +{ + +open Pp +open Ltac_plugin + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) } +END + +TACTIC EXTEND hello_world_tactic +| [ "hello_world" ] -> + { let _ = Feedback.msg_notice (str Tuto0_main.message) in + Tacticals.New.tclIDTAC } +END diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.ml b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml new file mode 100644 index 0000000000..93a807a800 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml @@ -0,0 +1 @@ +let message = "Hello world!" diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.mli b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli new file mode 100644 index 0000000000..846af3ed8c --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli @@ -0,0 +1 @@ +val message : string diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack new file mode 100644 index 0000000000..73be1bb561 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack @@ -0,0 +1,2 @@ +Tuto0_main +G_tuto0 diff --git a/doc/plugin_tutorial/tuto0/theories/Demo.v b/doc/plugin_tutorial/tuto0/theories/Demo.v new file mode 100644 index 0000000000..bdc61986af --- /dev/null +++ b/doc/plugin_tutorial/tuto0/theories/Demo.v @@ -0,0 +1,8 @@ +From Tuto0 Require Import Loader. + +HelloWorld. + +Lemma test : True. +Proof. +hello_world. +Abort. diff --git a/doc/plugin_tutorial/tuto0/theories/Loader.v b/doc/plugin_tutorial/tuto0/theories/Loader.v new file mode 100644 index 0000000000..7bce38382b --- /dev/null +++ b/doc/plugin_tutorial/tuto0/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto0_plugin". diff --git a/doc/plugin_tutorial/tuto1/Makefile b/doc/plugin_tutorial/tuto1/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto1/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject new file mode 100644 index 0000000000..585d1360be --- /dev/null +++ b/doc/plugin_tutorial/tuto1/_CoqProject @@ -0,0 +1,13 @@ +-R theories Tuto1 +-I src + +theories/Loader.v + +src/simple_check.mli +src/simple_check.ml +src/simple_declare.mli +src/simple_declare.ml +src/simple_print.ml +src/simple_print.mli +src/g_tuto1.mlg +src/tuto1_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune new file mode 100644 index 0000000000..cf9c674b14 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto1_plugin) + (public_name coq.plugins.tutorial.p1) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto1.ml) + (deps (:pp-file g_tuto1.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg new file mode 100644 index 0000000000..4df284d2d9 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -0,0 +1,154 @@ +DECLARE PLUGIN "tuto1_plugin" + +{ + +(* If we forget this line and include our own tactic definition using + TACTIC EXTEND, as below, then we get the strange error message + no implementation available for Tacentries, only when compiling + theories/Loader.v +*) +open Ltac_plugin +open Attributes +open Pp +(* This module defines the types of arguments to be used in the + EXTEND directives below, for example the string one. *) +open Stdarg + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "Hello" string(s) ] -> + { Feedback.msg_notice (strbrk "Hello " ++ str s) } +END + +(* reference is allowed as a syntactic entry, but so are all the entries + found the signature of module Prim in file coq/parsing/pcoq.mli *) + +VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY +| [ "HelloAgain" reference(r)] -> +(* The function Ppconstr.pr_qualid was found by searching all mli files + for a function of type qualid -> Pp.t *) + { Feedback.msg_notice + (strbrk "Hello again " ++ Ppconstr.pr_qualid r)} +END + +(* According to parsing/pcoq.mli, e has type constr_expr *) +(* this type is defined in pretyping/constrexpr.ml *) +(* Question for the developers: why is the file constrexpr.ml and not + constrexpr.mli --> Easier for packing the software in components. *) +VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY +| [ "Cmd1" constr(e) ] -> + { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") } +END + +(* The next step is to make something of parsed expression. + Interesting information in interp/constrintern.mli *) + +(* There are several phases of transforming a parsed expression into + the final internal data-type (constr). There exists a collection of + functions that combine all the phases *) + +VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY +| [ "Cmd2" constr(e) ] -> + { let _ = Constrintern.interp_constr + (Global.env()) + (* Make sure you don't use Evd.empty here, as this does not + check consistency with existing universe constraints. *) + (Evd.from_env (Global.env())) e in + Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") } +END + +(* This is to show what happens when typing in an empty environment + with an empty evd. + Question for the developers: why does "Cmd3 (fun x : nat => x)." + raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *) + +VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY +| [ "Cmd3" constr(e) ] -> + { let _ = Constrintern.interp_constr Environ.empty_env + Evd.empty e in + Feedback.msg_notice + (strbrk "Cmd3 accepted something in the empty context")} +END + +(* When adding a definition, we have to be careful that just + the operation of constructing a well-typed term may already change + the environment, at the level of universe constraints (which + are recorded in the evd component). The function + Constrintern.interp_constr ignores this side-effect, so it should + not be used here. *) + +(* Looking at the interface file interp/constrintern.ml4, I lost + some time because I did not see that the "constr" type appearing + there was "EConstr.constr" and not "Constr.constr". *) + +VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF +| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + Simple_declare.packed_declare_definition ~poly i v } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd5" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (_, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check1 v)) } +END + +VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY +| [ "Cmd6" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let evd, ty = Simple_check.simple_check2 v in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd ty) } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd7" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (a, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check3 v)) } +END + +(* This command takes a name and return its value. It does less + than Print, because it fails on constructors, axioms, and inductive types. + This should be improved, because the error message is an anomaly. + Anomalies should never appear even when using a command outside of its + intended use. *) +VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY +| [ "Cmd8" reference(r) ] -> + { let env = Global.env() in + let evd = Evd.from_env env in + Feedback.msg_notice + (Printer.pr_econstr_env env evd + (EConstr.of_constr + (Simple_print.simple_body_access (Nametab.global r)))) } +END + +TACTIC EXTEND my_intro +| [ "my_intro" ident(i) ] -> + { Tactics.introduction i } +END + +(* if one write this: + VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY + it gives an error message that is basically impossible to understand. *) + +VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY +| [ "Cmd9" ] -> + { let p = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in + let pprf = Proof.partial_proof p in + Feedback.msg_notice + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } +END diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml new file mode 100644 index 0000000000..1f636c531a --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -0,0 +1,32 @@ +let simple_check1 value_with_constraints = + begin + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This is reverse engineered from vernacentries.ml *) +(* The point of renaming is to make sure the bound names printed by Check + can be re-used in `apply with` tactics that use bound names to + refer to arguments. *) + let j = Termops.on_judgment EConstr.of_constr + (Arguments_renaming.rename_typing (Global.env()) + (EConstr.to_constr evd evalue)) in + let {Environ.uj_type=x}=j in x + end + +let simple_check2 value_with_constraints = + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This version should be preferred if bound variable names are not so + important, you want to really verify that the input is well-typed, + and if you want to obtain the type. *) +(* Note that the output value is a pair containing a new evar_map: + typing will fill out blanks in the term by add evar bindings. *) + Typing.type_of (Global.env()) evd evalue + +let simple_check3 value_with_constraints = + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This version should be preferred if bound variable names are not so + important and you already expect the input to have been type-checked + before. Set ~lax to false if you want an anomaly to be raised in + case of a type error. Otherwise a ReTypeError exception is raised. *) + Retyping.get_type_of ~lax:true (Global.env()) evd evalue diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli new file mode 100644 index 0000000000..bcf1bf56cf --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli @@ -0,0 +1,8 @@ +val simple_check1 : + EConstr.constr Evd.in_evar_universe_context -> EConstr.constr + +val simple_check2 : + EConstr.constr Evd.in_evar_universe_context -> Evd.evar_map * EConstr.constr + +val simple_check3 : + EConstr.constr Evd.in_evar_universe_context -> EConstr.constr diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml new file mode 100644 index 0000000000..9d10a8ba72 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -0,0 +1,24 @@ +(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) +let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = + let sigma = Evd.minimize_universes sigma in + let body = EConstr.to_constr sigma body in + let tyopt = Option.map (EConstr.to_constr sigma) tyopt in + let uvars_fold uvars c = + Univ.LSet.union uvars (Vars.universes_of_constr c) in + let uvars = List.fold_left uvars_fold Univ.LSet.empty + (Option.List.cons tyopt [body]) in + let sigma = Evd.restrict_universe_context sigma uvars in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let ubinders = Evd.universe_binders sigma in + let ce = Declare.definition_entry ?types:tyopt ~univs body in + DeclareDef.declare_definition ident k ce ubinders imps ~hook + +let packed_declare_definition ~poly ident value_with_constraints = + let body, ctx = value_with_constraints in + let sigma = Evd.from_ctx ctx in + let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in + let udecl = UState.default_univ_decl in + let nohook = Lemmas.mk_hook (fun _ x -> ()) in + ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) + +(* But this definition cannot be undone by Reset ident *) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.mli b/doc/plugin_tutorial/tuto1/src/simple_declare.mli new file mode 100644 index 0000000000..fd74e81526 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli @@ -0,0 +1,5 @@ +open Names +open EConstr + +val packed_declare_definition : + poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml new file mode 100644 index 0000000000..cfc38ff9c9 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -0,0 +1,17 @@ +(* A more advanced example of how to explore the structure of terms of + type constr is given in the coq-dpdgraph plugin. *) + +let simple_body_access gref = + match gref with + | Globnames.VarRef _ -> + failwith "variables are not covered in this example" + | Globnames.IndRef _ -> + failwith "inductive types are not covered in this example" + | Globnames.ConstructRef _ -> + failwith "constructors are not covered in this example" + | Globnames.ConstRef cst -> + let cb = Environ.lookup_constant cst (Global.env()) in + match Global.body_of_constant_body cb with + | Some(e, _) -> e + | None -> failwith "This term has no value" + diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.mli b/doc/plugin_tutorial/tuto1/src/simple_print.mli new file mode 100644 index 0000000000..254b56ff79 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_print.mli @@ -0,0 +1 @@ +val simple_body_access : Names.GlobRef.t -> Constr.constr diff --git a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack new file mode 100644 index 0000000000..a797a509e0 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack @@ -0,0 +1,4 @@ +Simple_check +Simple_declare +Simple_print +G_tuto1 diff --git a/doc/plugin_tutorial/tuto1/theories/Loader.v b/doc/plugin_tutorial/tuto1/theories/Loader.v new file mode 100644 index 0000000000..6e8e308b3f --- /dev/null +++ b/doc/plugin_tutorial/tuto1/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto1_plugin". diff --git a/doc/plugin_tutorial/tuto2/Makefile b/doc/plugin_tutorial/tuto2/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto2/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto2/_CoqProject b/doc/plugin_tutorial/tuto2/_CoqProject new file mode 100644 index 0000000000..cf9cb5cc26 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/_CoqProject @@ -0,0 +1,6 @@ +-R theories/ Tuto +-I src + +theories/Test.v +src/demo.mlg +src/demo_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto2/src/.gitignore b/doc/plugin_tutorial/tuto2/src/.gitignore new file mode 100644 index 0000000000..5b1b6a902e --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/.gitignore @@ -0,0 +1 @@ +/demo.ml diff --git a/doc/plugin_tutorial/tuto2/src/demo.mlg b/doc/plugin_tutorial/tuto2/src/demo.mlg new file mode 100644 index 0000000000..966c05acdc --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/demo.mlg @@ -0,0 +1,375 @@ +(* -------------------------------------------------------------------------- *) +(* *) +(* Initial ritual dance *) +(* *) +(* -------------------------------------------------------------------------- *) + +DECLARE PLUGIN "demo_plugin" + +(* + Use this macro before any of the other OCaml macros. + + Each plugin has a unique name. + We have decided to name this plugin as "demo_plugin". + That means that: + + (1) If we want to load this particular plugin to Coq toplevel, + we must use the following command. + + Declare ML Module "demo_plugin". + + (2) The above command will succeed only if there is "demo_plugin.cmxs" + in some of the directories that Coq is supposed to look + (i.e. the ones we specified via "-I ..." command line options). + + (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in + "demo_plugin.cmxs". + + (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .mlg files + are listed in the "_CoqProject" file. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY +| [ "Cmd1" ] -> { () } +END + +(* + These: + + VERNAC COMMAND EXTEND + + and + + END + + mark the beginning and the end of the definition of a new Vernacular command. + + Cmd1 is a unique identifier (which must start with an upper-case letter) + associated with the new Vernacular command we are defining. + + CLASSIFIED AS QUERY tells Coq that the new Vernacular command: + - changes neither the global environment + - nor does it modify the plugin's state. + + If the new command could: + - change the global environment + - or modify a plugin's state + then one would have to use CLASSIFIED AS SIDEFF instead. + + This: + + [ "Cmd1" ] -> { () } + + defines: + - the parsing rule + - the interpretation rule + + The parsing rule and the interpretation rule are separated by -> token. + + The parsing rule, in this case, is: + + [ "Cmd1" ] + + By convention, all vernacular command start with an upper-case letter. + + The [ and ] characters mark the beginning and the end of the parsing rule. + The parsing rule itself says that the syntax of the newly defined command + is composed from a single terminal Cmd1. + + The interpretation rule, in this case, is: + + { () } + + Similarly to the case of the parsing rule, + { and } characters mark the beginning and the end of the interpretation rule. + In this case, the following Ocaml expression: + + () + + defines the effect of the Vernacular command we have just defined. + That is, it behaves is no-op. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some terminal parameters? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY +| [ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> { () } +END + +(* + As shown above, the Vernacular command can be composed from + any number of terminals. + + By convention, each of these terminals starts with an upper-case letter. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some non-terminal parameter? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Stdarg + +} + +VERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY +| [ "Cmd3" int(i) ] -> { () } +END + +(* + This: + + open Stdarg + + is needed as some identifiers in the Ocaml code generated by the + + VERNAC COMMAND EXTEND ... END + + macros are not fully qualified. + + This: + + int(i) + + means that the new command is expected to be followed by an integer. + The integer is bound in the parsing rule to variable i. + This variable i then can be used in the interpretation rule. + + To see value of which Ocaml types can be bound this way, + look at the wit_* function declared in interp/stdarg.mli + (in the Coq's codebase). + + If we drop the wit_ prefix, we will get the token + that we can use in the parsing rule. + That is, since there exists wit_int, we know that + we can write: + + int(i) + + By looking at the signature of the wit_int function: + + val wit_int : int uniform_genarg_type + + we also know that variable i will have the type int. + + The types of wit_* functions are either: + + 'c uniform_genarg_type + + or + + ('a,'b,'c) genarg_type + + In both cases, the bound variable will have type 'c. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with variable number of arguments? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY +| [ "Cmd4" int_list(l) ] -> { () } +END + +(* + This: + + int_list(l) + + means that the new Vernacular command is expected to be followed + by a (whitespace separated) list of integers. + This list of integers is bound to the indicated l. + + In this case, as well as in the cases we point out below, instead of int + in int_list we could use any other supported type, e.g. ident, bool, ... + + To see which other Ocaml type constructors (in addition to list) + are supported, have a look at the parse_user_entry function defined + in grammar/q_util.mlp file. + + E.g.: + - ne_int_list(x) would represent a non-empty list of integers, + - int_list(x) would represent a list of integers, + - int_opt(x) would represent a value of type int option, + - ··· +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command that takes values of a custom type? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Ltac_plugin + +} + +(* + If we want to avoid a compilation failure + + "no implementation available for Tacenv" + + then we have to open the Ltac_plugin module. +*) + +(* + Pp module must be opened because some of the macros that are part of the API + do not expand to fully qualified names. +*) + +{ + +type type_5 = Foo_5 | Bar_5 + +} + +(* + We define a type of values that we want to pass to our Vernacular command. +*) + +(* + By default, we are able to define new Vernacular commands that can take + parameters of some of the supported types. Which types are supported, + that was discussed earlier. + + If we want to be able to define Vernacular command that takes parameters + of a type that is not supported by default, we must use the following macro: +*) + +{ + +open Pp + +} + +VERNAC ARGUMENT EXTEND custom5 +| [ "Foo_5" ] -> { Foo_5 } +| [ "Bar_5" ] -> { Bar_5 } +END + +(* + where: + + custom5 + + indicates that, from now on, in our parsing rules we can write: + + custom5(some_variable) + + in those places where we expect user to provide an input + that can be parsed by the parsing rules above + (and interpreted by the interpretations rules above). +*) + +(* Here: *) + +VERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY +| [ "Cmd5" custom5(x) ] -> { () } +END + +(* + we define a new Vernacular command whose parameters, provided by the user, + can be mapped to values of type_5. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to give a feedback to the user? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY +| [ "Cmd6" ] -> { Feedback.msg_notice (Pp.str "Everything is awesome!") } +END + +(* + The following functions: + + - Feedback.msg_info : Pp.t -> unit + - Feedback.msg_notice : Pp.t -> unit + - Feedback.msg_warning : Pp.t -> unit + - Feedback.msg_error : Pp.t -> unit + - Feedback.msg_debug : Pp.t -> unit + + enable us to give user a textual feedback. + + Pp module enable us to represent and construct pretty-printing instructions. + The concepts defined and the services provided by the Pp module are in + various respects related to the concepts and services provided + by the Format module that is part of the Ocaml standard library. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to implement a Vernacular command with (undoable) side-effects? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Summary.Local + +} + +(* + By opening Summary.Local module we shadow the original functions + that we traditionally use for implementing stateful behavior. + + ref + ! + := + + are now shadowed by their counterparts in Summary.Local. *) + +{ + +let counter = ref ~name:"counter" 0 + +} + +VERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF +| [ "Cmd7" ] -> { counter := succ !counter; + Feedback.msg_notice (Pp.str "counter = " ++ Pp.str (string_of_int (!counter))) } +END + +TACTIC EXTEND tactic1 +| [ "tactic1" ] -> { Proofview.tclUNIT () } +END + +(* ---- *) + +{ + +type custom = Foo_2 | Bar_2 + +let pr_custom _ _ _ = function + | Foo_2 -> Pp.str "Foo_2" + | Bar_2 -> Pp.str "Bar_2" + +} + +ARGUMENT EXTEND custom2 PRINTED BY { pr_custom } +| [ "Foo_2" ] -> { Foo_2 } +| [ "Bar_2" ] -> { Bar_2 } +END + +TACTIC EXTEND tactic2 +| [ "tactic2" custom2(x) ] -> { Proofview.tclUNIT () } +END diff --git a/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack new file mode 100644 index 0000000000..4f0b8480b5 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack @@ -0,0 +1 @@ +Demo diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune new file mode 100644 index 0000000000..f2bc405455 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto2_plugin) + (public_name coq.plugins.tutorial.p2) + (libraries coq.plugins.ltac)) + +(rule + (targets demo.ml) + (deps (:pp-file demo.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto2/theories/Test.v b/doc/plugin_tutorial/tuto2/theories/Test.v new file mode 100644 index 0000000000..38e83bfff1 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Test.v @@ -0,0 +1,19 @@ +Declare ML Module "demo_plugin". + +Cmd1. +Cmd2 With Some Terminal Parameters. +Cmd3 42. +Cmd4 100 200 300 400. +Cmd5 Foo_5. +Cmd5 Bar_5. +Cmd6. +Cmd7. +Cmd7. +Cmd7. + +Goal True. +Proof. + tactic1. + tactic2 Foo_2. + tactic2 Bar_2. +Abort. diff --git a/doc/plugin_tutorial/tuto3/Makefile b/doc/plugin_tutorial/tuto3/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto3/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto3/_CoqProject b/doc/plugin_tutorial/tuto3/_CoqProject new file mode 100644 index 0000000000..e2a60a430f --- /dev/null +++ b/doc/plugin_tutorial/tuto3/_CoqProject @@ -0,0 +1,12 @@ +-R theories Tuto3 +-I src + +theories/Data.v +theories/Loader.v + +src/tuto_tactic.ml +src/tuto_tactic.mli +src/construction_game.ml +src/construction_game.mli +src/g_tuto3.mlg +src/tuto3_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml new file mode 100644 index 0000000000..9d9f894e18 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml @@ -0,0 +1,186 @@ +open Pp + +let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] + +let example_sort evd = +(* creating a new sort requires that universes should be recorded + in the evd datastructure, so this datastructure also needs to be + passed around. *) + let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let new_type = EConstr.mkSort s in + evd, new_type + +let c_one evd = +(* In the general case, global references may refer to universe polymorphic + objects, and their universe has to be made afresh when creating an instance. *) + let gr_S = + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in +(* the long name of "S" was found with the command "About S." *) + let gr_O = + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + let evd, c_O = Evarutil.new_global evd gr_O in + let evd, c_S = Evarutil.new_global evd gr_S in +(* Here is the construction of a new term by applying functions to argument. *) + evd, EConstr.mkApp (c_S, [| c_O |]) + +let dangling_identity env evd = +(* I call this a dangling identity, because it is not polymorph, but + the type on which it applies is left unspecified, as it is + represented by an existential variable. The declaration for this + existential variable needs to be added in the evd datastructure. *) + let evd, type_type = example_sort evd in + let evd, arg_type = Evarutil.new_evar env evd type_type in +(* Notice the use of a De Bruijn index for the inner occurrence of the + bound variable. *) + evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type, + EConstr.mkRel 1) + +let dangling_identity2 env evd = +(* This example uses directly a function that produces an evar that + is meant to be a type. *) + let evd, (arg_type, type_type) = + Evarutil.new_type_evar env evd Evd.univ_rigid in + evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type, + EConstr.mkRel 1) + +let example_sort_app_lambda () = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c_v = c_one evd in +(* dangling_identity and dangling_identity2 can be used interchangeably here *) + let evd, c_f = dangling_identity2 env evd in + let c_1 = EConstr.mkApp (c_f, [| c_v |]) in + let _ = Feedback.msg_notice + (Printer.pr_econstr_env env evd c_1) in + (* type verification happens here. Type verification will update + existential variable information in the evd part. *) + let evd, the_type = Typing.type_of env evd c_1 in +(* At display time, you will notice that the system knows about the + existential variable being instantiated to the "nat" type, even + though c_1 still contains the meta-variable. *) + Feedback.msg_notice + ((Printer.pr_econstr_env env evd c_1) ++ + str " has type " ++ + (Printer.pr_econstr_env env evd the_type)) + + +let c_S evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in + Evarutil.new_global evd gr + +let c_O evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + Evarutil.new_global evd gr + +let c_E evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in + Evarutil.new_global evd gr + +let c_D evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in + Evarutil.new_global evd gr + +let c_Q evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in + Evarutil.new_global evd gr + +let c_R evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in + Evarutil.new_global evd gr + +let c_N evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in + Evarutil.new_global evd gr + +let c_C evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in + Evarutil.new_global evd gr + +let c_F evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in + Evarutil.new_global evd gr + +let c_P evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in + Evarutil.new_global evd gr + +(* If c_S was universe polymorphic, we should have created a new constant + at each iteration of buildup. *) +let mk_nat evd n = + let evd, c_S = c_S evd in + let evd, c_O = c_O evd in + let rec buildup = function + | 0 -> c_O + | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in + if n <= 0 then evd, c_O else evd, buildup n + +let example_classes n = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c_n = mk_nat evd n in + let evd, n_half = mk_nat evd (n / 2) in + let evd, c_N = c_N evd in + let evd, c_div = c_D evd in + let evd, c_even = c_E evd in + let evd, c_Q = c_Q evd in + let evd, c_R = c_R evd in + let arg_type = EConstr.mkApp (c_even, [| c_n |]) in + let evd0 = evd in + let evd, instance = Evarutil.new_evar env evd arg_type in + let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let evd, the_type = Typing.type_of env evd c_half in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let proved_equality = + EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast, + EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in +(* This is where we force the system to compute with type classes. *) +(* Question to coq developers: why do we pass two evd arguments to + solve_remaining_evars? Is the choice of evd0 relevant here? *) + let evd = Pretyping.solve_remaining_evars + (Pretyping.default_inference_flags true) env evd ~initial:evd0 in + let evd, final_type = Typing.type_of env evd proved_equality in + Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality) + +(* This function, together with definitions in Data.v, shows how to + trigger automatic proofs at the time of typechecking, based on + canonical structures. + + n is a number for which we want to find the half (and a proof that + this half is indeed the half) +*) +let example_canonical n = + let env = Global.env () in + let evd = Evd.from_env env in +(* Construct a natural representation of this integer. *) + let evd, c_n = mk_nat evd n in +(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *) + let evd, c_N = c_N evd in + let evd, c_F = c_F evd in + let evd, c_R = c_R evd in + let evd, c_C = c_C evd in + let evd, c_P = c_P evd in +(* the last argument of C *) + let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in +(* Now we build two existential variables, for the value of the half and for + the "S_ev" structure that triggers the proof search. *) + let evd, ev1 = Evarutil.new_evar env evd c_N in +(* This is the type for the second existential variable *) + let csev = EConstr.mkApp (c_F, [| ev1 |]) in + let evd, ev2 = Evarutil.new_evar env evd csev in +(* Now we build the C structure. *) + let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in +(* Type-checking this term will compute values for the existential variables *) + let evd, final_type = Typing.type_of env evd test_term in +(* The computed type has two parameters, the second one is the proof. *) + let value = match EConstr.kind evd final_type with + | Constr.App(_, [| _; the_half |]) -> the_half + | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in +(* I wish for a nicer way to get the value of ev2 in the evar_map *) + let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in + let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in + let evd, the_statement = Typing.type_of env evd the_prf in + Feedback.msg_notice + (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++ + Printer.pr_econstr_env env evd the_statement) diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.mli b/doc/plugin_tutorial/tuto3/src/construction_game.mli new file mode 100644 index 0000000000..1832ed6630 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/construction_game.mli @@ -0,0 +1,4 @@ +val dangling_identity : Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.t +val example_sort_app_lambda : unit -> unit +val example_classes : int -> unit +val example_canonical : int -> unit diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune new file mode 100644 index 0000000000..ba6d8b288f --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/dune @@ -0,0 +1,10 @@ +(library + (name tuto3_plugin) + (public_name coq.plugins.tutorial.p3) + (flags :standard -warn-error -3) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto3.ml) + (deps (:pp-file g_tuto3.mlg)) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg new file mode 100644 index 0000000000..82ba45726e --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg @@ -0,0 +1,46 @@ +DECLARE PLUGIN "tuto3_plugin" + +{ + +open Ltac_plugin + +open Construction_game + +(* This one is necessary, to avoid message about missing wit_string *) +open Stdarg + +} + +VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY +| [ "Tuto3_1" ] -> + { let env = Global.env () in + let evd = Evd.from_env env in + let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let new_type_2 = EConstr.mkSort s in + let evd, _ = + Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in + Feedback.msg_notice + (Printer.pr_econstr_env env evd new_type_2) } +END + +VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY +| [ "Tuto3_2" ] -> { example_sort_app_lambda () } +END + +TACTIC EXTEND collapse_hyps +| [ "pack" "hypothesis" ident(i) ] -> + { Tuto_tactic.pack_tactic i } +END + +(* More advanced examples, where automatic proof happens but + no tactic is being called explicitely. The first one uses + type classes. *) +VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY +| [ "Tuto3_3" int(n) ] -> { example_classes n } +END + +(* The second one uses canonical structures. *) +VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY +| [ "Tuto3_4" int(n) ] -> { example_canonical n } +END + diff --git a/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack new file mode 100644 index 0000000000..f4645ad7ed --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack @@ -0,0 +1,3 @@ +Construction_game +Tuto_tactic +G_tuto3 diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml new file mode 100644 index 0000000000..8f2c387d09 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -0,0 +1,143 @@ +open Proofview + +let constants = ref ([] : EConstr.t list) + +(* This is a pattern to collect terms from the Coq memory of valid terms + and proofs. This pattern extends all the way to the definition of function + c_U *) +let collect_constants () = + if (!constants = []) then + let open EConstr in + let open UnivGen in + let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] in + let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in + let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in + let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in + let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in + let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in + constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x)) + [gr_H; gr_M; gr_R; gr_P; gr_U]; + !constants + else + !constants + +let c_H () = + match collect_constants () with + it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pack" + +let c_M () = + match collect_constants () with + _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pack_marker" + +let c_R () = + match collect_constants () with + _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pair" + +let c_P () = + match collect_constants () with + _ :: _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of prod" + +let c_U () = + match collect_constants () with + _ :: _ :: _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of prod" + +(* The following tactic is meant to pack an hypothesis when no other + data is already packed. + + The main difficulty in defining this tactic is to understand how to + construct the input expected by apply_in. *) +let package i = Goal.enter begin fun gl -> + Tactics.apply_in true false i + [(* this means that the applied theorem is not to be cleared. *) + None, (CAst.make (c_M (), + (* we don't specialize the theorem with extra values. *) + Tactypes.NoBindings))] + (* we don't destruct the result according to any intro_pattern *) + None + end + +(* This function is meant to observe a type of shape (f a) + and return the value a. *) + +(* Remark by Maxime: look for destApp combinator. *) +let unpack_type evd term = + let report () = + CErrors.user_err (Pp.str "expecting a packed type") in + match EConstr.kind evd term with + | Constr.App (_, [| ty |]) -> ty + | _ -> report () + +(* This function is meant to observe a type of shape + A -> pack B -> C and return A, B, C + but it is not used in the current version of our tactic. + It is kept as an example. *) +let two_lambda_pattern evd term = + let report () = + CErrors.user_err (Pp.str "expecting two nested implications") in +(* Note that pattern-matching is always done through the EConstr.kind function, + which only provides one-level deep patterns. *) + match EConstr.kind evd term with + (* Here we recognize the outer implication *) + | Constr.Prod (_, ty1, l1) -> + (* Here we recognize the inner implication *) + (match EConstr.kind evd l1 with + | Constr.Prod (n2, packed_ty2, deep_conclusion) -> + (* Here we recognized that the second type is an application *) + ty1, unpack_type evd packed_ty2, deep_conclusion + | _ -> report ()) + | _ -> report () + +(* In the environment of the goal, we can get the type of an assumption + directly by a lookup. The other solution is to call a low-cost retyping + function like *) +let get_type_of_hyp env id = + match EConstr.lookup_named id env with + | Context.Named.Declaration.LocalAssum (_, ty) -> ty + | _ -> CErrors.user_err (let open Pp in + str (Names.Id.to_string id) ++ + str " is not a plain hypothesis") + +let repackage i h_hyps_id = Goal.enter begin fun gl -> + let env = Goal.env gl in + let evd = Tacmach.New.project gl in + let concl = Tacmach.New.pf_concl gl in + let (ty1 : EConstr.t) = get_type_of_hyp env i in + let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in + let ty2 = unpack_type evd packed_ty2 in + let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in + let open EConstr in + let new_packed_value = + mkApp (c_R (), [| ty1; ty2; mkVar i; + mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in + Refine.refine ~typecheck:true begin fun evd -> + let evd, new_goal = Evarutil.new_evar env evd + (mkProd (Names.Name.Anonymous, + mkApp(c_H (), [| new_packed_type |]), + Vars.lift 1 concl)) in + evd, mkApp (new_goal, + [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |]) + end + end + +let pack_tactic i = + let h_hyps_id = (Names.Id.of_string "packed_hyps") in + Proofview.Goal.enter begin fun gl -> + let hyps = Environ.named_context_val (Proofview.Goal.env gl) in + if not (Termops.mem_named_context_val i hyps) then + (CErrors.user_err + (Pp.str ("no hypothesis named" ^ (Names.Id.to_string i)))) + else + if Termops.mem_named_context_val h_hyps_id hyps then + tclTHEN (repackage i h_hyps_id) + (tclTHEN (Tactics.clear [h_hyps_id; i]) + (Tactics.introduction h_hyps_id)) + else + tclTHEN (package i) + (tclTHEN (Tactics.rename_hyp [i, h_hyps_id]) + (Tactics.move_hyp h_hyps_id Logic.MoveLast)) + end diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli new file mode 100644 index 0000000000..dbf6cf48e2 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli @@ -0,0 +1,3 @@ +val two_lambda_pattern : + Evd.evar_map -> EConstr.t -> EConstr.t * EConstr.t * EConstr.t +val pack_tactic : Names.Id.t -> unit Proofview.tactic diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v new file mode 100644 index 0000000000..f7395d686b --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/Data.v @@ -0,0 +1,73 @@ + + +Inductive pack (A: Type) : Type := + packer : A -> pack A. + +Arguments packer {A}. + +Definition uncover (A : Type) (packed : pack A) : A := + match packed with packer v => v end. + +Notation "!!!" := (pack _) (at level 0, only printing). + +(* The following data is used as material for automatic proofs + based on type classes. *) + +Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}. + +Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}. + +Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n). +Proof. + intros []. + simpl. rewrite <-plus_n_O, <-plus_n_Sm. + reflexivity. +Qed. + +Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) := + {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}. + +Definition tuto_div2 n (p : EvenNat n) := @half _ p. + +(* to be used in the following examples +Compute (@half 8 _). + +Check (@half_prop 8 _). + +Check (@half_prop 7 _). + +and in command Tuto3_3 8. *) + +(* The following data is used as material for automatic proofs + based on canonical structures. *) + +Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}. + +Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r := + match r with Build_S_ev _ _ h => h end. + +Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n := + Build_S_ev n d Pd. + +Canonical Structure can_ev0 : S_ev 0 := + Build_S_ev 0 0 (@eq_refl _ 0). + +Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n). +Proof. +intros s; exists (S (S (double_of _ s))). +destruct s as [a P]. +exact (even_rec _ _ P). +Defined. + +Canonical Structure can_ev_rec. + +Record cmp (n : nat) (k : nat) := + C {h : S_ev k; _ : double_of k h = n}. + +(* To be used in, e.g., + +Check (C _ _ _ eq_refl : cmp 6 _). + +Check (C _ _ _ eq_refl : cmp 7 _). + +*) diff --git a/doc/plugin_tutorial/tuto3/theories/Loader.v b/doc/plugin_tutorial/tuto3/theories/Loader.v new file mode 100644 index 0000000000..1351cff63b --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/Loader.v @@ -0,0 +1,3 @@ +From Tuto3 Require Export Data. + +Declare ML Module "tuto3_plugin". diff --git a/doc/plugin_tutorial/tuto3/theories/test.v b/doc/plugin_tutorial/tuto3/theories/test.v new file mode 100644 index 0000000000..43204ddf34 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/test.v @@ -0,0 +1,23 @@ +(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *) + +Require Import Tuto3.Loader. + +(* This should print Type. *) +Tuto3_1. + +(* This should print a term that contains an existential variable. *) +(* And then print the same term, where the variable has been correctly + instantiated. *) +Tuto3_2. + +Lemma tutu x y (A : 0 < x) (B : 10 < y) : True. +Proof. +pack hypothesis A. +(* Hypothesis A should have disappeared and a "packed_hyps" hypothesis + should have appeared, with unreadable content. *) +pack hypothesis B. +(* Hypothesis B should have disappeared *) +destruct packed_hyps as [unpacked_hyps]. +(* Hypothesis unpacked_hyps should contain the previous contents of A and B. *) +exact I. +Qed. 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/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 827b7c13c1..067af954ad 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1189,7 +1189,6 @@ def setup(app): app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks) # Add extra styles - app.add_stylesheet("fonts.css") app.add_stylesheet("ansi.css") app.add_stylesheet("coqdoc.css") app.add_javascript("notations.js") diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 7bc5d090b4..95a0039b0a 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -293,9 +293,6 @@ let ids_of_pattern_list = (List.fold_left (cases_pattern_fold_names Id.Set.add)) Id.Set.empty -let ids_of_cases_indtype p = - cases_pattern_fold_names Id.Set.add Id.Set.empty p - let ids_of_cases_tomatch tms = List.fold_right (fun (_, ona, indnal) l -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 8c735edfc9..f1a8ed202f 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -113,9 +113,6 @@ val map_constr_expr_with_binders : val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr -(** Specific function for interning "in indtype" syntax of "match" *) -val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t - val free_vars_of_constr_expr : constr_expr -> Id.Set.t val occur_var_constr_expr : Id.t -> constr_expr -> bool diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0d0b6158d9..444ac5ab6d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -67,10 +67,7 @@ let print_no_symbol = ref false (**********************************************************************) (* Turning notations and scopes on and off for printing *) -module IRuleSet = Set.Make(struct - type t = interp_rule - let compare x y = Pervasives.compare x y - end) +module IRuleSet = InterpRuleSet let inactive_notations_table = Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7aa85a0810..c8c38ffe05 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -573,12 +573,17 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = (* TODO binders *) next_ident_away_from id (fun id -> Id.Set.mem id fvs3) -let is_var store pat = +let is_patvar c = + match DAst.get c with + | PatVar _ -> true + | _ -> false + +let is_patvar_store store pat = match DAst.get pat with | PatVar na -> ignore(store na); true | _ -> false -let out_var pat = +let out_patvar pat = match pat.v with | CPatAtom (Some qid) when qualid_is_ident qid -> Name (qualid_basename qid) @@ -600,7 +605,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na + | [pat] when is_patvar_store store pat -> let na = get () in None, na | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> @@ -610,7 +615,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let env = set_env_scopes env scopes in if onlyident then (* Do not try to interpret a variable as a constructor *) - let na = out_var pat in + let na = out_patvar pat in let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in (renaming,env), None, na else @@ -618,7 +623,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na + | [pat] when is_patvar_store store pat -> let na = get () in None, na | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> @@ -743,7 +748,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in if onlyident then - let na = out_var c in term_of_name na, None + let na = out_patvar c in term_of_name na, None else let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with @@ -805,7 +810,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = (* and since we are only interested in the pattern as a term *) let env = reset_hidden_inductive_implicit_test env in if onlyident then - term_of_name (out_var pat) + term_of_name (out_patvar pat) else let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in match disjpat with @@ -1741,7 +1746,7 @@ let intern_ind_pattern genv ntnvars scopes pat = let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in (with_letin, match product_of_cases_patterns empty_alias idslpl with - | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) + | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type ?loc) | x -> error_bad_inductive_type ?loc @@ -1979,30 +1984,30 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = end | CCases (sty, rtnpo, tms, eqns) -> let as_in_vars = List.fold_left (fun acc (_,na,inb) -> - Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc) - (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na) - inb) Id.Set.empty tms in + (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na)) + Id.Set.empty tms in (* as, in & return vars *) let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in - let tms,ex_ids,match_from_in = List.fold_right - (fun citm (inds,ex_ids,matchs) -> - let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in - (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs) - tms ([],Id.Set.empty,[]) in + let tms,ex_ids,aliases,match_from_in = List.fold_right + (fun citm (inds,ex_ids,asubst,matchs) -> + let ((tm,ind),extra_id,(ind_ids,alias_subst,match_td)) = + intern_case_item env forbidden_vars citm in + (tm,ind)::inds, + Id.Set.union ind_ids (Option.fold_right Id.Set.add extra_id ex_ids), + merge_subst alias_subst asubst, + List.rev_append match_td matchs) + tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var)) (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = - let is_patvar c = match DAst.get c with - | PatVar _ -> true - | _ -> false - in let rec aux = function | [] -> [] | (_, c) :: q when is_patvar c -> aux q | l -> l in aux match_from_in in + let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in let rtnpo = match stripped_match_from_in with | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) | l -> @@ -2150,7 +2155,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* the "in" part *) let match_td,typ = match t with | Some t -> - let with_letin,(ind,l) = intern_ind_pattern globalenv ntnvars (None,env.scopes) t in + let with_letin,(ind,ind_ids,alias_subst,l) = + intern_ind_pattern globalenv ntnvars (None,env.scopes) t in let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in (* for "in Vect n", we answer (["n","n"],[(loc,"n")]) @@ -2186,9 +2192,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let _,args_rel = List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in canonize_args args_rel l forbidden_names_for_gen [] [] in - match_to_do, Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal)) + (Id.Set.of_list (List.map (fun id -> id.CAst.v) ind_ids),alias_subst,match_to_do), + Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal)) | None -> - [], None in + (Id.Set.empty,Id.Map.empty,[]), None in (tm',(na.CAst.v, typ)), extra_id, match_td and intern_impargs c env l subscopes args = diff --git a/interp/notation.ml b/interp/notation.ml index b0854de4a3..ca27d439fb 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -50,15 +50,25 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false +let notation_entry_level_compare s1 s2 = match (s1,s2) with +| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> 0 +| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> + pair_compare String.compare Int.compare (s1,n1) (s2,n2) +| InConstrEntrySomeLevel, _ -> -1 +| InCustomEntryLevel _, _ -> 1 + let notation_eq (from1,ntn1) (from2,ntn2) = notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s +let notation_compare = + pair_compare notation_entry_level_compare String.compare + module NotationOrd = struct type t = notation - let compare = Pervasives.compare + let compare = notation_compare end module NotationSet = Set.Make(NotationOrd) @@ -178,6 +188,17 @@ type scoped_notation_rule_core = scope_name * notation * interpretation * int op type notation_rule_core = interp_rule * interpretation * int option type notation_rule = notation_rule_core * delimiters option * bool +let interp_rule_compare r1 r2 = match r1, r2 with + | NotationRule (sc1,ntn1), NotationRule (sc2,ntn2) -> + pair_compare (Option.compare String.compare) notation_compare (sc1,ntn1) (sc2,ntn2) + | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2 + | (NotationRule _ | SynDefRule _), _ -> -1 + +module InterpRuleSet = Set.Make(struct + type t = interp_rule + let compare = interp_rule_compare + end) + (* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and *) type uninterp_scope_elem = diff --git a/interp/notation.mli b/interp/notation.mli index 75034cad70..a482e00e81 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -210,6 +210,8 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of KerName.t +module InterpRuleSet : Set.S with type elt = interp_rule + val declare_notation_interpretation : notation -> scope_name option -> interpretation -> notation_location -> onlyprint:bool -> unit diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1f61bcae2e..196bb16f32 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -374,46 +374,6 @@ let rec stack_args_size = function | Zupdate(_)::s -> stack_args_size s | (ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> 0 -(* When used as an argument stack (only Zapp can appear) *) -let rec decomp_stack = function - | Zapp v :: s -> - (match Array.length v with - 0 -> decomp_stack s - | 1 -> Some (v.(0), s) - | _ -> - Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> None -let array_of_stack s = - let rec stackrec = function - | [] -> [] - | Zapp args :: s -> args :: (stackrec s) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ -> assert false - in Array.concat (stackrec s) -let rec stack_assign s p c = match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then - Zapp args :: stack_assign s (p-q) c - else - (let nargs = Array.copy args in - nargs.(p) <- c; - Zapp nargs :: s) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> s -let rec stack_tail p s = - if Int.equal p 0 then s else - match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then stack_tail (p-q) s - else Zapp (Array.sub args p (q-p)) :: s - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> failwith "stack_tail" -let rec stack_nth s p = match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then stack_nth s (p-q) - else args.(p) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> raise Not_found - (* Lifting. Preserves sharing (useful only for cell with norm=Red). lft_fconstr always create a new cell, while lift_fconstr avoids it when the lift is 0. *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index c2d53eed47..46be1bb279 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -123,8 +123,7 @@ type fterm = (*********************************************************************** s A [stack] is a context of arguments, arguments are pushed by - [append_stack] one array at a time but popped with [decomp_stack] - one by one *) + [append_stack] one array at a time *) type stack_member = | Zapp of fconstr array @@ -139,13 +138,7 @@ and stack = stack_member list val empty_stack : stack val append_stack : fconstr array -> stack -> stack -val decomp_stack : stack -> (fconstr * stack) option -val array_of_stack : stack -> fconstr array -val stack_assign : stack -> int -> fconstr -> stack val stack_args_size : stack -> int -val stack_tail : int -> stack -> stack -val stack_nth : stack -> int -> fconstr -val zip_term : (fconstr -> constr) -> constr -> stack -> constr val eta_expand_stack : stack -> stack (** To lazy reduce a constr, create a [clos_infos] with 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/names.ml b/kernel/names.ml index b2d6a489a6..9f27212967 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -391,6 +391,8 @@ module KerName = struct let print kn = str (to_string kn) + let debug_print kn = str (debug_to_string kn) + let compare (kn1 : kernel_name) (kn2 : kernel_name) = if kn1 == kn2 then 0 else diff --git a/kernel/names.mli b/kernel/names.mli index 350db871d5..61df3bad0e 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -149,15 +149,15 @@ sig val is_empty : t -> bool (** Test whether a directory path is empty. *) - val to_string : t -> string - (** Print directory paths as ["coq_root.module.submodule"] *) - val initial : t (** Initial "seed" of the unique identifier generator *) val hcons : t -> t (** Hashconsing of directory paths. *) + val to_string : t -> string + (** Print non-empty directory paths as ["coq_root.module.submodule"] *) + val print : t -> Pp.t end @@ -180,15 +180,15 @@ sig val make : string -> t (** Create a label out of a string. *) - val to_string : t -> string - (** Conversion to string. *) - val of_id : Id.t -> t (** Conversion from an identifier. *) val to_id : t -> Id.t (** Conversion to an identifier. *) + val to_string : t -> string + (** Conversion to string. *) + val print : t -> Pp.t (** Pretty-printer. *) @@ -227,10 +227,10 @@ sig (** Return the identifier contained in the argument. *) val to_string : t -> string - (** Conversion to a string. *) + (** Encode as a string (not to be used for user-facing messages). *) val debug_to_string : t -> string - (** Same as [to_string], but outputs information related to debug. *) + (** Same as [to_string], but outputs extra information related to debug. *) end @@ -252,16 +252,17 @@ sig val is_bound : t -> bool - val to_string : t -> string - - val debug_to_string : t -> string - (** Same as [to_string], but outputs information related to debug. *) - val initial : t (** Name of the toplevel structure ([= MPfile initial_dir]) *) val dp : t -> DirPath.t + val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + + val debug_to_string : t -> string + (** Same as [to_string], but outputs extra information related to debug. *) + end module MPset : Set.S with type elt = ModPath.t @@ -284,13 +285,17 @@ sig val modpath : t -> ModPath.t val label : t -> Label.t - (** Display *) val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) val debug_to_string : t -> string - (** Same as [to_string], but outputs information related to debug. *) + (** Same as [to_string], but outputs extra information related to debug. *) - val print : t -> Pp.t + val debug_print : t -> Pp.t + (** Same as [print], but outputs extra information related to debug. *) (** Comparisons *) val compare : t -> t -> int @@ -365,9 +370,16 @@ sig (** Displaying *) val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) + val debug_to_string : t -> string + (** Same as [to_string], but outputs extra information related to debug. *) + val debug_print : t -> Pp.t + (** Same as [print], but outputs extra information related to debug. *) end @@ -444,9 +456,16 @@ sig (** Displaying *) val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) + val debug_to_string : t -> string + (** Same as [to_string], but outputs extra information related to debug. *) + val debug_print : t -> Pp.t + (** Same as [print], but outputs extra information related to debug. *) end @@ -567,8 +586,12 @@ module Projection : sig val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t - val print : t -> Pp.t val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) + end type t (* = Repr.t * bool *) @@ -609,7 +632,10 @@ module Projection : sig val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) end 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 diff --git a/lib/system.ml b/lib/system.ml index a9db95318f..fd6579dd69 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -287,20 +287,20 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = real (round (sstop -. sstart)) ++ str "s" ++ str ")" -let with_time ~batch f x = +let with_time ~batch ~header f x = let tstart = get_time() in let msg = if batch then "" else "Finished transaction in " in try let y = f x in let tend = get_time() in let msg2 = if batch then "" else " (successful)" in - Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if batch then "" else "Finished failing transaction in " in let msg2 = if batch then "" else " (failure)" in - Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e (* We use argv.[0] as we don't want to resolve symlinks *) diff --git a/lib/system.mli b/lib/system.mli index a3b79ee528..6dd1eb5a84 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -105,7 +105,7 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t -val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b +val with_time : batch:bool -> header:Pp.t -> ('a -> 'b) -> 'a -> 'b (** [get_toplevel_path program] builds a complete path to the executable denoted by [program]. This involves: diff --git a/lib/util.ml b/lib/util.ml index 38d73d3453..0389336258 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -20,6 +20,12 @@ let on_pi1 f (a,b,c) = (f a,b,c) let on_pi2 f (a,b,c) = (a,f b,c) let on_pi3 f (a,b,c) = (a,b,f c) +(* Comparing pairs *) + +let pair_compare cmpx cmpy (x1,y1 as p1) (x2,y2 as p2) = + if p1 == p2 then 0 else + let c = cmpx x1 x2 in if c == 0 then cmpy y1 y2 else c + (* Projections from triplets *) let pi1 (a,_,_) = a diff --git a/lib/util.mli b/lib/util.mli index 1eb60f509a..fa3b622621 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -17,6 +17,10 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b +(** Comparing pairs *) + +val pair_compare : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a * 'b -> 'a * 'b -> int) + (** Mapping under triple *) val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index c2b7fa117d..49d6cf01d9 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -548,20 +548,27 @@ let process_sequence loc bp c cs = aux 1 cs (* Must be a special token *) -let process_chars loc bp c cs = +let process_chars ~diff_mode loc bp c cs = let t = progress_from_byte loc None (-1) !token_tree cs c in let ep = Stream.count cs in match t with | Some t -> (KEYWORD t, set_loc_pos loc bp ep) | None -> let ep' = bp + utf8_char_size loc cs c in - njunk (ep' - ep) cs; - let loc = set_loc_pos loc bp ep' in - err loc Undefined_token + if diff_mode then begin + let len = ep' - bp in + ignore (store 0 c); + ignore (nstore (len - 1) 1 cs); + IDENT (get_buff len), set_loc_pos loc bp ep + end else begin + njunk (ep' - ep) cs; + let loc = set_loc_pos loc bp ep' in + err loc Undefined_token + end (* Parse what follows a dot *) -let parse_after_dot loc c bp s = match Stream.peek s with +let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with | Some ('a'..'z' | 'A'..'Z' | '_' as d) -> Stream.junk s; let len = @@ -576,11 +583,11 @@ let parse_after_dot loc c bp s = match Stream.peek s with let len = ident_tail loc (nstore n 0 s) s in let field = get_buff len in (try find_keyword loc ("."^field) s with Not_found -> FIELD field) - | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s) + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars ~diff_mode loc bp c s) (* Parse what follows a question mark *) -let parse_after_qmark loc bp s = +let parse_after_qmark ~diff_mode loc bp s = match Stream.peek s with | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK | None -> KEYWORD "?" @@ -588,7 +595,7 @@ let parse_after_qmark loc bp s = match lookup_utf8 loc s with | Utf8Token (st, _) when Unicode.is_valid_ident_initial st -> LEFTQMARK | AsciiChar | Utf8Token _ | EmptyStream -> - fst (process_chars loc bp '?' s) + fst (process_chars ~diff_mode loc bp '?' s) let blank_or_eof cs = match Stream.peek cs with @@ -598,20 +605,20 @@ let blank_or_eof cs = (* Parse a token in a char stream *) -let rec next_token loc s = +let rec next_token ~diff_mode loc s = let bp = Stream.count s in match Stream.peek s with | Some ('\n' as c) -> Stream.junk s; let ep = Stream.count s in - comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s + comm_loc bp; push_char c; next_token ~diff_mode (bump_loc_line loc ep) s | Some (' ' | '\t' | '\r' as c) -> Stream.junk s; - comm_loc bp; push_char c; next_token loc s + comm_loc bp; push_char c; next_token ~diff_mode loc s | Some ('.' as c) -> Stream.junk s; let t = - try parse_after_dot loc c bp s with + try parse_after_dot ~diff_mode loc c bp s with Stream.Failure -> raise (Stream.Error "") in let ep = Stream.count s in @@ -630,13 +637,13 @@ let rec next_token loc s = Stream.junk s; let t,new_between_commands = if !between_commands then process_sequence loc bp c s, true - else process_chars loc bp c s,false + else process_chars ~diff_mode loc bp c s,false in comment_stop bp; between_commands := new_between_commands; t | Some '?' -> Stream.junk s; let ep = Stream.count s in - let t = parse_after_qmark loc bp s in + let t = parse_after_qmark ~diff_mode loc bp s in comment_stop bp; (t, set_loc_pos loc bp ep) | Some ('a'..'z' | 'A'..'Z' | '_' as c) -> Stream.junk s; @@ -670,12 +677,16 @@ let rec next_token loc s = Stream.junk s; begin try match Stream.peek s with + | Some '*' when diff_mode -> + Stream.junk s; + let ep = Stream.count s in + (IDENT "(*", set_loc_pos loc bp ep) | Some '*' -> Stream.junk s; comm_loc bp; push_string "(*"; - let loc = comment loc bp s in next_token loc s - | _ -> let t = process_chars loc bp c s in comment_stop bp; t + let loc = comment loc bp s in next_token ~diff_mode loc s + | _ -> let t = process_chars ~diff_mode loc bp c s in comment_stop bp; t with Stream.Failure -> raise (Stream.Error "") end | Some ('{' | '}' as c) -> @@ -683,7 +694,7 @@ let rec next_token loc s = let ep = Stream.count s in let t,new_between_commands = if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true - else process_chars loc bp c s, false + else process_chars ~diff_mode loc bp c s, false in comment_stop bp; between_commands := new_between_commands; t | _ -> @@ -695,14 +706,14 @@ let rec next_token loc s = comment_stop bp; (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep | AsciiChar | Utf8Token _ -> - let t = process_chars loc bp (Stream.next s) s in + let t = process_chars ~diff_mode loc bp (Stream.next s) s in comment_stop bp; t | EmptyStream -> comment_stop bp; (EOI, set_loc_pos loc bp (bp+1)) (* (* Debug: uncomment this for tracing tokens seen by coq...*) -let next_token loc s = - let (t,loc as r) = next_token loc s in +let next_token ~diff_mode loc s = + let (t,loc as r) = next_token ~diff_mode loc s in Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t); r *) @@ -743,7 +754,7 @@ let token_text = function | (con, "") -> con | (con, prm) -> con ^ " \"" ^ prm ^ "\"" -let func cs = +let func next_token cs = let loct = loct_create () in let cur_loc = ref (Loc.create !current_file 1 0 0 0) in let ts = @@ -755,8 +766,8 @@ let func cs = in (ts, loct_func loct) -let lexer = { - Plexing.tok_func = func; +let make_lexer ~diff_mode = { + Plexing.tok_func = func (next_token ~diff_mode); Plexing.tok_using = (fun pat -> match Tok.of_pattern pat with | KEYWORD s -> add_keyword s @@ -765,6 +776,8 @@ let lexer = { Plexing.tok_match = Tok.match_pattern; Plexing.tok_text = token_text } +let lexer = make_lexer ~diff_mode:false + (** Terminal symbols interpretation *) let is_ident_not_keyword s = diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index c0ebdd45ef..af3fd7f318 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -56,3 +56,14 @@ val set_lexer_state : lexer_state -> unit val get_lexer_state : unit -> lexer_state val drop_lexer_state : unit -> unit val get_comment_state : lexer_state -> ((int * int) * string) list + +(** Create a lexer. true enables alternate handling for computing diffs. +It ensures that, ignoring white space, the concatenated tokens equal the input +string. Specifically: +- for strings, return the enclosing quotes as tokens and treat the quoted value +as if it was unquoted, possibly becoming multiple tokens +- for comments, return the "(*" as a token and treat the contents of the comment as if +it was not in a comment, possibly becoming multiple tokens +- return any unrecognized Ascii or UTF-8 character as a string +*) +val make_lexer : diff_mode:bool -> Tok.t Gramlib.Plexing.lexer diff --git a/parsing/tok.ml b/parsing/tok.ml index c0d5b6742d..03825e350f 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -40,18 +40,19 @@ let extract_string diff_mode = function | KEYWORD s -> s | IDENT s -> s | STRING s -> - if diff_mode then - let escape_quotes s = - let len = String.length s in - let buf = Buffer.create len in - for i = 0 to len-1 do - let ch = String.get s i in - Buffer.add_char buf ch; - if ch = '"' then Buffer.add_char buf '"' else () - done; - Buffer.contents buf - in - "\"" ^ (escape_quotes s) ^ "\"" else s + if diff_mode then + let escape_quotes s = + let len = String.length s in + let buf = Buffer.create len in + for i = 0 to len-1 do + let ch = String.get s i in + Buffer.add_char buf ch; + if ch = '"' then Buffer.add_char buf '"' else () + done; + Buffer.contents buf + in + "\"" ^ (escape_quotes s) ^ "\"" + else s | PATTERNIDENT s -> s | FIELD s -> if diff_mode then "." ^ s else s | INT s -> s diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index f0bb6f58a6..ff2c900130 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,5 +1,14 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) open Goal open Environ diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 9a53e1dd1a..a39f76db9e 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -1,5 +1,15 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) + Declare ML Module "ssrmatching_plugin". Module SsrMatchingSyntax. diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e6e1530e36..ed28cc7725 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -46,15 +46,10 @@ let () = Goptions.(declare_bool_option { (* Functions to deal with impossible cases *) (*******************************************) let impossible_default_case env = - let type_of_id = - let open Names.GlobRef in - match Coqlib.lib_ref "core.IDProp.type" with - | ConstRef c -> c - | VarRef _ | IndRef _ | ConstructRef _ -> assert false - in + let type_of_id = Coqlib.lib_ref "core.IDProp.type" in let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in - let (_, u) = Constr.destConst c in - Some (c, Constr.mkConstU (type_of_id, u), ctx) + let (_, u) = Constr.destRef c in + Some (c, Constr.mkRef (type_of_id, u), ctx) let coq_unit_judge = let open Environ in diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index b280ce909b..c1ea067567 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -88,7 +88,8 @@ let tokenize_string s = let st = CLexer.get_lexer_state () in try let istr = Stream.of_string s in - let lex = CLexer.lexer.Gramlib.Plexing.tok_func istr in + let lexer = CLexer.make_lexer ~diff_mode:true in + let lex = lexer.Gramlib.Plexing.tok_func istr in let toks = stream_tok [] (fst lex) in CLexer.set_lexer_state st; toks diff --git a/stm/stm.ml b/stm/stm.ml index 32c6c7d959..169d608d2d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -869,7 +869,6 @@ end = struct (* {{{ *) cur_id := id | { state = Error ie } -> - cur_id := id; Exninfo.iraise ie | _ -> @@ -2017,7 +2016,7 @@ end = struct (* {{{ *) find ~time:false ~batch:false ~fail:false e in let st = Vernacstate.freeze_interp_state ~marshallable:false in Vernacentries.with_fail st fail (fun () -> - (if time then System.with_time ~batch else (fun x -> x)) (fun () -> + (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in @@ -2832,17 +2831,9 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - match Stateid.get info with - | None -> - VCS.restore vcs; - VCS.print (); - anomaly(str"error with no safe_id attached:" ++ spc() ++ - CErrors.iprint_no_report (e, info) ++ str".") - | Some (safe_id, id) -> - stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); - VCS.restore vcs; - VCS.print (); - Exninfo.iraise (e, info) + VCS.restore vcs; + VCS.print (); + Exninfo.iraise (e, info) let snapshot_vio ~doc ldir long_f_dot_vo = let doc = finish ~doc in @@ -2993,7 +2984,14 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Unknown: we execute it, check for open goals and propagate sideeff *) | VtUnknown, VtNow -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - let id = VCS.new_node ~id:newtip () in + if not (get_allow_nested_proofs ()) && in_proof then + "Commands which may open proofs are not allowed in a proof 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 head_id = VCS.get_branch_pos head in let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) let step () = 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/Makefile b/test-suite/Makefile index 34a1900bbc..37091a49e5 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -36,9 +36,10 @@ include ../Makefile.common # easily overridden LIB := .. BIN := $(shell cd ..; pwd)/bin/ +COQFLAGS?= -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite -coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite +coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS) +coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v new file mode 100644 index 0000000000..9816954d0c --- /dev/null +++ b/test-suite/bugs/closed/bug_8369.v @@ -0,0 +1,3 @@ +(* Was failing in master with a not_found generated by the printer *) + +Fail Definition foo := fun '(u, v) p2 => (u, v). diff --git a/test-suite/bugs/closed/bug_9240.v b/test-suite/bugs/closed/bug_9240.v new file mode 100644 index 0000000000..e0901dc2d9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9240.v @@ -0,0 +1,12 @@ +Register unit as core.IDProp.type. +Register tt as core.IDProp.idProp. + + +Inductive vec (A : Type) : nat -> Type := +| nil : vec A 0 +| cons : forall n : nat, A -> vec A n -> vec A (S n). + +Definition hd (A : Type) (n : nat) (v : vec A (S n)) : A := +match v in (vec _ (S n)) return A with +| cons _ _ h _ => h +end. (* assertion failure in evarconv *) 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/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v index e1c29a954c..baf87631f0 100644 --- a/test-suite/bugs/opened/bug_3166.v +++ b/test-suite/bugs/opened/bug_3166.v @@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True. compute in H0. change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. Fail pose proof (fun k => @eq_trans _ _ _ k H0). +Abort. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v index a717bbe735..18820b1a4c 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/opened/bug_3754.v @@ -282,3 +282,4 @@ Defined. rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. Fail rewrite (concat_Ap ff2). + Abort. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v index 5c74addb62..78b2aa69b9 100644 --- a/test-suite/bugs/opened/bug_3890.v +++ b/test-suite/bugs/opened/bug_3890.v @@ -1,3 +1,5 @@ +Set Nested Proofs Allowed. + Class Foo. Class Bar := b : Type. diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v index 2d0d1930f1..3c7c945ed8 100644 --- a/test-suite/bugs/opened/bug_3938.v +++ b/test-suite/bugs/opened/bug_3938.v @@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. intros a b f H. rewrite H. (* Toplevel input, characters 15-25: Anomaly: Evar ?X11 was not declared. Please report. *) +Abort. diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index ae5d51bae8..b7c98aa134 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *) Require Coq.ZArith.BinInt. Module WithIdTac. Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index cf2d5b2850..14c48e8fa0 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -9,10 +9,11 @@ The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. Instance is not well-typed in the environment of ?x. The command has indeed failed with message: -Cannot infer the domain of the type of f. +Cannot infer ?T in the partial instance "?T -> nat" found for the type of f. The command has indeed failed with message: -Cannot infer the domain of the implicit parameter A of id whose type is -"Type". +Cannot infer ?T in the partial instance "?T -> nat" found for the implicit +parameter A of id whose type is "Type". The command has indeed failed with message: -Cannot infer the codomain of the type of f in environment: +Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the +type of f in environment: x : nat diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index d58e4bf2d6..94016e170b 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -45,3 +45,5 @@ fun x : nat => (x.-1)%pred : Prop ## : Prop +Notation Cn := Foo.FooCn +Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 61206b6dd0..309115848f 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -164,3 +164,20 @@ Open Scope my_scope. Check ##. End H. + +(* Fixing a bug reported by G. Gonthier in #9207 *) + +Module J. + +Module Import Mfoo. +Module Foo. +Definition FooCn := 2. +Module Bar. +Notation Cn := FooCn. +End Bar. +End Foo. +Export Foo.Bar. +End Mfoo. +About Cn. + +End J. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 52fe98ac07..232ac17cbf 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1873,3 +1873,12 @@ Check match niln in listn O return O=O with niln => eq_refl end. (* (was failing up to May 2017) *) Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end. + +(* A test about binding variables of "in" clause of "match" *) +(* (was failing from 8.5 to Dec 2018) *) + +Check match O in nat return nat with O => O | _ => O end. + +(* Checking that aliases are substituted in the correct order *) + +Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0. diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml index 7f9e6cc6e0..d0b8d21b69 100644 --- a/test-suite/unit-tests/printing/proof_diffs_test.ml +++ b/test-suite/unit-tests/printing/proof_diffs_test.ml @@ -51,23 +51,28 @@ let t () = assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed let _ = add_test "diff_str add/remove" t -(* example of a limitation, not really a test *) -let t () = - try - let _ = diff_str "a" ">" in - assert_failure "unlexable string gives an exception" - with _ -> () -let _ = add_test "diff_str unlexable" t - -(* problematic examples for tokenize_string: - comments omitted - quoted string loses quote marks (are escapes supported/handled?) - char constant split into 2 +(* lexer tweaks: + comments are lexed as multiple tokens + strings tokens include begin/end quotes and embedded "" + single multibyte characters returned even if they're not keywords + + inputs that give a lexer failure (but no use case needs them yet): + ".12" + unterminated string + invalid UTF-8 sequences *) let t () = - List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx"); - cprintf "\n" -let _ = add_test "tokenize_string examples" t + let str = "(* comment.field *) ?id () \"str\"\"ing\" \\ := Ж > ∃ 'c' xx" in + let toks = tokenize_string str in + (*List.iter (fun x -> cprintf "'%s' " x) toks;*) + (*cprintf "\n";*) + let str_no_white = String.concat "" (String.split_on_char ' ' str) in + assert_equal ~printer:(fun x -> x) str_no_white (String.concat "" toks); + List.iter (fun s -> + assert_equal ~msg:("'" ^ s ^ "' is a single token") ~printer:string_of_bool true (List.mem s toks)) + [ "(*"; "()"; ":="] + +let _ = add_test "tokenize_string/diff_mode in lexer" t open Pp diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 4372ac72ae..f8f10b34ae 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -126,6 +126,8 @@ TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line +TGTS ?= + ########## End of parameters ################################################## # What follows may be relevant to you only if you need to # extend this Makefile. If so, look for 'Extension point' here and @@ -237,6 +239,11 @@ vo_to_obj = $(addsuffix .o,\ $(filter-out Warning: Error:,\ $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) strip_dotslash = $(patsubst ./%,%,$(1)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + VO = vo VOFILES = $(VFILES:.v=.$(VO)) @@ -269,14 +276,14 @@ CMXSFILES = \ PACKEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) # files that are archived into a .cma (mllib) LIBEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) OBJFILES = $(call vo_to_obj,$(VOFILES)) @@ -681,11 +688,11 @@ $(GHTMLFILES): %.g.html: %.v %.glob # Dependency files ############################################################ -ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) -else - ifeq ($(MAKECMDGOALS),) +ifndef MAKECMDGOALS -include $(ALLDFILES) +else + ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) endif endif @@ -784,3 +791,7 @@ debug: .PHONY: debug .DEFAULT_GOAL := all + +# Local Variables: +# mode: makefile-gmake +# End: diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c914bbecff..d8465aac27 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -37,34 +37,6 @@ let vernac_echo ?loc in_chan = let open Loc in Feedback.msg_notice @@ str @@ really_input_string in_chan len ) loc -(* For coqtop -time, we display the position in the file, - and a glimpse of the executed command *) - -let pp_cmd_header {CAst.loc;v=com} = - let shorten s = - if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s - in - let noblank s = String.map (fun c -> - match c with - | ' ' | '\n' | '\t' | '\r' -> '~' - | x -> x - ) s - in - let (start,stop) = Option.cata Loc.unloc (0,0) loc in - let safe_pr_vernac x = - try Ppvernac.pr_vernac x - with e -> str (Printexc.to_string e) in - let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) - in str "Chars " ++ int start ++ str " - " ++ int stop ++ - str " [" ++ str cmd ++ str "] " - -(* This is a special case where we assume we are in console batch mode - and take control of the console. - *) -let print_cmd_header com = - Pp.pp_with !Topfmt.std_ft (pp_cmd_header com); - Format.pp_print_flush !Topfmt.std_ft () - (* Reenable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) @@ -88,7 +60,6 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = due to the way it prints. *) let com = if state.time then begin - print_cmd_header com; CAst.make ?loc @@ VernacTime(state.time,com) end else com in let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in 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 a2b5c8d70a..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 @@ -511,7 +510,7 @@ let pr_trailing_ne_context_of env sigma = if List.is_empty (Environ.rel_context env) && List.is_empty (Environ.named_context env) then str "." - else (str " in environment:"++ pr_context_unlimited env sigma) + else (strbrk " in environment:" ++ pr_context_unlimited env sigma) let rec explain_evar_kind env sigma evk ty = let open Evar_kinds in @@ -551,21 +550,21 @@ let rec explain_evar_kind env sigma evk ty = strbrk "an instance of type " ++ ty ++ str " for the variable " ++ Id.print id | Evar_kinds.SubEvar (where,evk') -> - let evi = Evd.find sigma evk' in + let rec find_source evk = + let evi = Evd.find sigma evk in + match snd evi.evar_source with + | Evar_kinds.SubEvar (_,evk) -> find_source evk + | src -> evi,src in + let evi,src = find_source evk' in let pc = match evi.evar_body with | Evar_defined c -> pr_leconstr_env env sigma c | Evar_empty -> assert false in let ty' = evi.evar_concl in - (match where with - | Some Evar_kinds.Body -> str "the body of " - | Some Evar_kinds.Domain -> str "the domain of " - | Some Evar_kinds.Codomain -> str "the codomain of " - | None -> - pr_existential_key sigma evk ++ str " of type " ++ ty ++ - str " in the partial instance " ++ pc ++ - str " found for ") ++ - explain_evar_kind env sigma evk' - (pr_leconstr_env env sigma ty') (snd evi.evar_source) + pr_existential_key sigma evk ++ + strbrk " in the partial instance " ++ pc ++ + strbrk " found for " ++ + explain_evar_kind env sigma evk + (pr_leconstr_env env sigma ty') src let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr sigma evi.evar_concl with @@ -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 diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 4065bb9c1f..b4b893a3fd 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -406,3 +406,24 @@ let with_output_to_file fname func input = deep_ft := Util.pi3 old_fmt; close_out channel; Exninfo.iraise reraise + +(* For coqtop -time, we display the position in the file, + and a glimpse of the executed command *) + +let pr_cmd_header {CAst.loc;v=com} = + let shorten s = + if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s + in + let noblank s = String.map (fun c -> + match c with + | ' ' | '\n' | '\t' | '\r' -> '~' + | x -> x + ) s + in + let (start,stop) = Option.cata Loc.unloc (0,0) loc in + let safe_pr_vernac x = + try Ppvernac.pr_vernac x + with e -> str (Printexc.to_string e) in + let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) + in str "Chars " ++ int start ++ str " - " ++ int stop ++ + str " [" ++ str cmd ++ str "] " diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 0ddf474970..5f84c5edee 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -71,3 +71,4 @@ val print_err_exn : exn -> unit redirected to a file [file] *) val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b +val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e6e3db4beb..dbccea1117 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2388,8 +2388,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = control v | VernacRedirect (s, {v}) -> Topfmt.with_output_to_file s control v - | VernacTime (batch, {v}) -> - System.with_time ~batch control v; + | VernacTime (batch, com) -> + let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in + System.with_time ~batch ~header control com.CAst.v; and aux ~atts : _ -> unit = function diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index b40bccf27e..61540024ef 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -36,7 +36,8 @@ let do_if_not_cached rf f v = let freeze_interp_state ~marshallable = { system = update_cache s_cache (States.freeze ~marshallable); proof = update_cache s_proof (Proof_global.freeze ~marshallable); - shallow = marshallable } + shallow = false; + } let unfreeze_interp_state { system; proof } = do_if_not_cached s_cache States.unfreeze system; |