diff options
57 files changed, 778 insertions, 554 deletions
diff --git a/.gitattributes b/.gitattributes index e087e1737..a5edcdb5b 100644 --- a/.gitattributes +++ b/.gitattributes @@ -5,48 +5,51 @@ # Because our commit hook automatically does [apply whitespace=fix] we # disable whitespace checking for all files except those where we want # it. Otherwise rogue global configuration and forgotten local -# configuration can break commits. +# configuration can break commits. Note that git cannot fix but can +# detect a blank-at-eof when it comes from removing a chunk of text at +# the end of the file, leaving an extra newline from before that +# chunk, so we disable blank-at-eof. * -whitespace # tabs are allowed in Makefiles. -Makefile* whitespace=trailing-space -tools/CoqMakefile.in whitespace=trailing-space +Makefile* whitespace=blank-at-eol +tools/CoqMakefile.in whitespace=blank-at-eol # in general we don't want tabs. -*.asciidoc whitespace=trailing-space,tab-in-indent -*.bib whitespace=trailing-space,tab-in-indent -*.c whitespace=trailing-space,tab-in-indent -*.css whitespace=trailing-space,tab-in-indent -*.dtd whitespace=trailing-space,tab-in-indent -*.el whitespace=trailing-space,tab-in-indent -*.g whitespace=trailing-space,tab-in-indent -*.h whitespace=trailing-space,tab-in-indent -*.html whitespace=trailing-space,tab-in-indent -*.hva whitespace=trailing-space,tab-in-indent -*.js whitespace=trailing-space,tab-in-indent -*.json whitespace=trailing-space,tab-in-indent -*.lang whitespace=trailing-space,tab-in-indent -*.md whitespace=trailing-space,tab-in-indent -*.merlin whitespace=trailing-space,tab-in-indent -*.ml whitespace=trailing-space,tab-in-indent -*.ml4 whitespace=trailing-space,tab-in-indent -*.mli whitespace=trailing-space,tab-in-indent -*.mll whitespace=trailing-space,tab-in-indent -*.mllib whitespace=trailing-space,tab-in-indent -*.mlp whitespace=trailing-space,tab-in-indent -*.mlpack whitespace=trailing-space,tab-in-indent -*.nsh whitespace=trailing-space,tab-in-indent -*.nsi whitespace=trailing-space,tab-in-indent -*.py whitespace=trailing-space,tab-in-indent -*.rst whitespace=trailing-space,tab-in-indent -*.sh whitespace=trailing-space,tab-in-indent -*.sty whitespace=trailing-space,tab-in-indent -*.tex whitespace=trailing-space,tab-in-indent -*.tokens whitespace=trailing-space,tab-in-indent -*.txt whitespace=trailing-space,tab-in-indent -*.v whitespace=trailing-space,tab-in-indent -*.xml whitespace=trailing-space,tab-in-indent -*.yml whitespace=trailing-space,tab-in-indent +*.asciidoc whitespace=blank-at-eol,tab-in-indent +*.bib whitespace=blank-at-eol,tab-in-indent +*.c whitespace=blank-at-eol,tab-in-indent +*.css whitespace=blank-at-eol,tab-in-indent +*.dtd whitespace=blank-at-eol,tab-in-indent +*.el whitespace=blank-at-eol,tab-in-indent +*.g whitespace=blank-at-eol,tab-in-indent +*.h whitespace=blank-at-eol,tab-in-indent +*.html whitespace=blank-at-eol,tab-in-indent +*.hva whitespace=blank-at-eol,tab-in-indent +*.js whitespace=blank-at-eol,tab-in-indent +*.json whitespace=blank-at-eol,tab-in-indent +*.lang whitespace=blank-at-eol,tab-in-indent +*.md whitespace=blank-at-eol,tab-in-indent +*.merlin whitespace=blank-at-eol,tab-in-indent +*.ml whitespace=blank-at-eol,tab-in-indent +*.ml4 whitespace=blank-at-eol,tab-in-indent +*.mli whitespace=blank-at-eol,tab-in-indent +*.mll whitespace=blank-at-eol,tab-in-indent +*.mllib whitespace=blank-at-eol,tab-in-indent +*.mlp whitespace=blank-at-eol,tab-in-indent +*.mlpack whitespace=blank-at-eol,tab-in-indent +*.nsh whitespace=blank-at-eol,tab-in-indent +*.nsi whitespace=blank-at-eol,tab-in-indent +*.py whitespace=blank-at-eol,tab-in-indent +*.rst whitespace=blank-at-eol,tab-in-indent +*.sh whitespace=blank-at-eol,tab-in-indent +*.sty whitespace=blank-at-eol,tab-in-indent +*.tex whitespace=blank-at-eol,tab-in-indent +*.tokens whitespace=blank-at-eol,tab-in-indent +*.txt whitespace=blank-at-eol,tab-in-indent +*.v whitespace=blank-at-eol,tab-in-indent +*.xml whitespace=blank-at-eol,tab-in-indent +*.yml whitespace=blank-at-eol,tab-in-indent # CR is desired for these Windows files. -*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent +*.bat whitespace=cr-at-eol,blank-at-eol,tab-in-indent @@ -23,6 +23,11 @@ Tactics - Option "Ltac Debug" now applies also to terms built using Ltac functions. +- Deprecated the Implicit Tactic family of commands. + +- The `simple apply` tactic now respects the `Opaque` flag when called from + Ltac (`auto` still does not respect it). + Tools - Coq_makefile lets one override or extend the following variables from @@ -125,7 +130,7 @@ Tactics profiling, and "Set NativeCompute Profile Filename" customizes the profile filename. - The tactic "omega" is now aware of the bodies of context variables - such as "x := 5 : Z" (see BZ#148). This could be disabled via + such as "x := 5 : Z" (see #1362). This could be disabled via Unset Omega UseLocalDefs. - The tactic "romega" is also aware now of the bodies of context variables. - The tactic "zify" resp. "omega with N" is now aware of N.pred. @@ -310,7 +315,7 @@ Improvements around some error messages. Many bug fixes including two important ones: -- BZ#5730: CoqIDE becomes unresponsive on file open. +- Bug #5730: CoqIDE becomes unresponsive on file open. - coq_makefile: make sure compile flags for Coq and coq_makefile are in sync (in particular, make sure the `-safe-string` option is used to compile plugins). @@ -360,7 +365,7 @@ Tactics which behave like the corresponding variants with no "e" but turn unresolved implicit arguments into existential variables, on the shelf, rather than failing. -- Tactic injection has become more powerful (closes BZ#4890) and its +- Tactic injection has become more powerful (closes bug #4890) and its documentation has been updated. - New variants of the `first` and `solve` tacticals that do not rely on parsing rules, meant to define tactic notations. @@ -406,7 +411,7 @@ Standard Library file ChoiceFacts.v. - New lemmas about iff and about orders on positive and Z. - New lemmas on powerRZ. -- Strengthened statement of JMeq_eq_dep (closes BZ#4912). +- Strengthened statement of JMeq_eq_dep (closes bug #4912). - The BigN, BigZ, BigZ libraries are no longer part of the Coq standard library, they are now provided by a separate repository https://github.com/coq/bignums @@ -481,12 +486,12 @@ XML Protocol and internal changes See dev/doc/changes.txt -Many bugfixes including BZ#1859, BZ#2884, BZ#3613, BZ#3943, BZ#3994, -BZ#4250, BZ#4709, BZ#4720, BZ#4824, BZ#4844, BZ#4911, BZ#5026, BZ#5233, -BZ#5275, BZ#5315, BZ#5336, BZ#5360, BZ#5390, BZ#5414, BZ#5417, BZ#5420, -BZ#5439, BZ#5449, BZ#5475, BZ#5476, BZ#5482, BZ#5501, BZ#5507, BZ#5520, -BZ#5523, BZ#5524, BZ#5553, BZ#5577, BZ#5578, BZ#5589, BZ#5597, BZ#5598, -BZ#5607, BZ#5618, BZ#5619, BZ#5620, BZ#5641, BZ#5648, BZ#5651, BZ#5671. +Many bugfixes including #1859, #2884, #3613, #3943, #3994, +#4250, #4709, #4720, #4824, #4844, #4911, #5026, #5233, +#5275, #5315, #5336, #5360, #5390, #5414, #5417, #5420, +#5439, #5449, #5475, #5476, #5482, #5501, #5507, #5520, +#5523, #5524, #5553, #5577, #5578, #5589, #5597, #5598, +#5607, #5618, #5619, #5620, #5641, #5648, #5651, #5671. Many bugfixes on OS X and Windows (now the test-suite passes on these platforms too). @@ -2662,7 +2667,7 @@ Tactics a registered setoid equality before starting to reduce in H. This is unlikely to break any script. Should this happen nonetheless, one can insert manually some "unfold ... in H" before rewriting. -- Fixed various bugs about (setoid) rewrite ... in ... (in particular BZ#1101) +- Fixed various bugs about (setoid) rewrite ... in ... (in particular bug #5941) - "rewrite ... in" now accepts a clause as place where to rewrite instead of juste a simple hypothesis name. For instance: rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H @@ -3239,11 +3244,11 @@ Incompatibilities Bugs - Improved localisation of errors in Syntactic Definitions -- Induction principle creation failure in presence of let-in fixed (BZ#238) -- Inversion bugs fixed (BZ#212 and BZ#220) -- Omega bug related to Set fixed (BZ#180) -- Type-checking inefficiency of nested destructuring let-in fixed (BZ#216) -- Improved handling of let-in during holes resolution phase (BZ#239) +- Induction principle creation failure in presence of let-in fixed (#1459) +- Inversion bugs fixed (#1427 and #1437) +- Omega bug related to Set fixed (#1384) +- Type-checking inefficiency of nested destructuring let-in fixed (#1435) +- Improved handling of let-in during holes resolution phase (#1460) Efficiency @@ -3256,18 +3261,18 @@ Changes from V7.3 to V7.3.1 Bug fixes - Corrupted Field tactic and Match Context tactic construction fixed - - Checking of names already existing in Assert added (BZ#182) - - Invalid argument bug in Exact tactic solved (BZ#183) - - Colliding bound names bug fixed (BZ#202) - - Wrong non-recursivity test for Record fixed (BZ#189) - - Out of memory/seg fault bug related to parametric inductive fixed (BZ#195) + - Checking of names already existing in Assert added (#1386) + - Invalid argument bug in Exact tactic solved (#1387) + - Colliding bound names bug fixed (#1412) + - Wrong non-recursivity test for Record fixed (#1394) + - Out of memory/seg fault bug related to parametric inductive fixed (#1404) - Setoid_replace/Setoid_rewrite bug wrt "==" fixed Misc - Ocaml version >= 3.06 is needed to compile Coq from sources - Simplification of fresh names creation strategy for Assert, Pose and - LetTac (BZ#192) + LetTac (#1402) Changes from V7.2 to V7.3 ========================= diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index ecc45735f..508dcf5fb 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -480,19 +480,19 @@ function make_sed { ##### LIBPNG ##### function make_libpng { - build_conf_make_inst http://prdownloads.sourceforge.net/libpng libpng-1.6.18 tar.gz true + build_conf_make_inst http://prdownloads.sourceforge.net/libpng libpng-1.6.34 tar.gz true } ##### PIXMAN ##### function make_pixman { - build_conf_make_inst http://cairographics.org/releases pixman-0.32.8 tar.gz true + build_conf_make_inst http://cairographics.org/releases pixman-0.34.0 tar.gz true } ##### FREETYPE ##### function make_freetype { - build_conf_make_inst http://sourceforge.net/projects/freetype/files/freetype2/2.6.1 freetype-2.6.1 tar.bz2 true + build_conf_make_inst http://sourceforge.net/projects/freetype/files/freetype2/2.9.1 freetype-2.9.1 tar.bz2 true } ##### EXPAT ##### @@ -508,7 +508,7 @@ function make_fontconfig { make_expat # CONFIGURE PARAMETERS # build/install fails without --disable-docs - build_conf_make_inst http://www.freedesktop.org/software/fontconfig/release fontconfig-2.11.94 tar.gz true --disable-docs + build_conf_make_inst http://www.freedesktop.org/software/fontconfig/release fontconfig-2.12.93 tar.gz true --disable-docs } ##### ICONV ##### @@ -588,8 +588,7 @@ function make_glib { make_gettext make_libffi make_libpcre - # build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.46 glib-2.46.0 tar.xz true - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.47 glib-2.47.5 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.57 glib-2.57.1 tar.xz true } ##### ATK ##### @@ -597,7 +596,7 @@ function make_glib { function make_atk { make_gettext make_glib - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.18 atk-2.18.0 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.29 atk-2.29.1 tar.xz true } ##### PIXBUF ##### @@ -610,7 +609,7 @@ function make_gdk-pixbuf { # CONFIGURE PARAMETERS # --with-included-loaders=yes statically links the image file format handlers # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory" - build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32 gdk-pixbuf-2.32.1 tar.xz true --with-included-loaders=yes + build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.36 gdk-pixbuf-2.36.12 tar.xz true --with-included-loaders=yes } ##### CAIRO ##### @@ -621,7 +620,7 @@ function make_cairo { make_glib make_pixman make_fontconfig - build_conf_make_inst http://cairographics.org/releases cairo-1.14.2 tar.xz true + build_conf_make_inst http://cairographics.org/releases rcairo-1.15.13 tar.xz true } ##### PANGO ##### @@ -630,7 +629,7 @@ function make_pango { make_cairo make_glib make_fontconfig - build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.38 pango-1.38.0 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.42 pango-1.42.1 tar.xz true } ##### GTK2 ##### @@ -647,7 +646,7 @@ function make_gtk2 { make_pango make_gdk-pixbuf make_cairo - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24 gtk+-2.24.28 tar.xz patch_gtk2 + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24 gtk+-2.24.32 tar.xz patch_gtk2 fi } @@ -660,7 +659,7 @@ function make_gtk3 { make_gdk-pixbuf make_cairo make_libepoxy - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.16 gtk+-3.16.7 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.22 gtk+-3.22.30 tar.xz true # make all incl. tests and examples runs through fine # make install fails with issue with @@ -740,7 +739,7 @@ function install_flexlink { # An alternative is to first build an OCaml without shared library support and build flexlink with it function get_flex_dll_link_bin { - if build_prep http://alain.frisch.fr/flexdll flexdll-bin-0.34 zip 1 ; then + if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip 1 ; then install_flexdll install_flexlink build_post @@ -750,7 +749,7 @@ function get_flex_dll_link_bin { # Build flexdll and flexlink from sources after building OCaml function make_flex_dll_link { - if build_prep http://alain.frisch.fr/flexdll flexdll-0.34 tar.gz ; then + if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip ; then if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then # shellcheck disable=SC2086 log1 make $MAKE_OPT build_mingw flexlink.exe @@ -791,11 +790,10 @@ function make_ln { function make_ocaml { get_flex_dll_link_bin - if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.02 ocaml-4.02.3 tar.gz 1 ; then - # if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.01 ocaml-4.01.0 tar.gz 1 ; then - # See README.win32 - cp config/m-nt.h config/m.h - cp config/s-nt.h config/s.h + if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.06 ocaml-4.06.1 tar.gz 1 ; then + # See README.win32.adoc + cp config/m-nt.h byterun/caml/m.h + cp config/s-nt.h byterun/caml/s.h if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then cp config/Makefile.mingw config/Makefile elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then @@ -831,9 +829,9 @@ function make_ocaml { # 4.01 installs these files, 4.02 doesn't. So delete them and copy them from the sources. rm -f ./*.txt cp LICENSE "$PREFIXOCAML/license_readme/ocaml/License.txt" - cp INSTALL "$PREFIXOCAML/license_readme/ocaml/Install.txt" - cp README "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt" - cp README.win32 "$PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt" + cp INSTALL.adoc "$PREFIXOCAML/license_readme/ocaml/Install.txt" + cp README.adoc "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt" + cp README.win32.adoc "$PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt" cp VERSION "$PREFIXOCAML/license_readme/ocaml/Version.txt" cp Changes "$PREFIXOCAML/license_readme/ocaml/Changes.txt" fi @@ -854,16 +852,30 @@ function make_ocaml_tools { ##### OCAML EXTRA LIBRARIES ##### function make_ocaml_libs { + make_num make_findlib make_lablgtk # make_stdint } +##### Ocaml num library ##### +function make_num { + make_ocaml + # We need this commit due to windows fixed, IMHO this is better than patching v1.1. + if build_prep https://github.com/ocaml/num/archive/ 7dd5e935aaa2b902585b3b2d0e55ad9b2442fff0 zip 1 num-1.1-7d; then + log2 make all + # log2 make test + log2 make install + log2 make clean + build_post + fi +} + ##### FINDLIB Ocaml library manager ##### function make_findlib { make_ocaml - if build_prep https://opam.ocaml.org/archives ocamlfind.1.5.6+opam tar.gz 1 ; then + if build_prep https://opam.ocaml.org/archives ocamlfind.1.8.0+opam tar.gz 1 ; then logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf" # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT log2 make all @@ -900,7 +912,7 @@ function make_camlp4 { if ! command camlp4 ; then make_ocaml make_findlib - if build_prep https://github.com/ocaml/camlp4/archive 4.02+6 tar.gz 1 camlp4-4.02+6 ; then + if build_prep https://github.com/ocaml/camlp4/archive 4.06+2 tar.gz 1 camlp4-4.06+2 ; then # See https://github.com/ocaml/camlp4/issues/41#issuecomment-112018910 logn configure ./configure # Note: camlp4 doesn't support -j 8, so don't pass MAKE_OPT @@ -917,7 +929,8 @@ function make_camlp4 { function make_camlp5 { make_ocaml make_findlib - if build_prep http://camlp5.gforge.inria.fr/distrib/src camlp5-6.14 tgz 1 ; then + + if build_prep https://github.com/camlp5/camlp5/archive rel705 tar.gz 1 camlp5-rel705; then logn configure ./configure # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile @@ -944,10 +957,10 @@ function make_camlp5 { function make_lablgtk { make_ocaml make_findlib - make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5 + # make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5 make_gtk2 make_gtk_sourceview2 - if build_prep https://forge.ocamlcore.org/frs/download.php/1479 lablgtk-2.18.3 tar.gz 1 ; then + if build_prep https://forge.ocamlcore.org/frs/download.php/1726 lablgtk-2.18.6 tar.gz 1 ; then # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML" @@ -1130,8 +1143,10 @@ function copy_coq_license { function make_coq { make_ocaml - make_lablgtk + make_num + make_findlib make_camlp5 + make_lablgtk if case $COQ_VERSION in # e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch b/dev/build/windows/patches_coq/lablgtk-2.18.6.patch new file mode 100644 index 000000000..23c303135 --- /dev/null +++ b/dev/build/windows/patches_coq/lablgtk-2.18.6.patch @@ -0,0 +1,101 @@ +diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with: +difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1 +TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz +FOLDER= lablgtk-2.18.3 +TARSTRIP= 1 +TARPREFIX= lablgtk-2.18.3/ +ORIGFOLDER= lablgtk-2.18.3.orig +--- lablgtk-2.18.3.orig/configure 2014-10-29 08:51:05.000000000 +0100 ++++ lablgtk-2.18.3/configure 2018-04-25 10:58:54.454501600 +0200 +@@ -2667,7 +2667,7 @@ + fi + + +-if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then ++if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5 + $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;} + OCAMLFIND=no +--- lablgtk-2.18.3.orig/src/glib.mli 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/glib.mli 2018-04-25 10:58:54.493555500 +0200 +@@ -75,6 +75,7 @@ + type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI] + type id + val channel_of_descr : Unix.file_descr -> channel ++ val channel_of_descr_socket : Unix.file_descr -> channel + val add_watch : + cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id + val remove : id -> unit +--- lablgtk-2.18.3.orig/src/glib.ml 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/glib.ml 2018-04-25 10:58:54.479543500 +0200 +@@ -72,6 +72,8 @@ + type id + external channel_of_descr : Unix.file_descr -> channel + = "ml_g_io_channel_unix_new" ++ external channel_of_descr_socket : Unix.file_descr -> channel ++ = "ml_g_io_channel_unix_new_socket" + external remove : id -> unit = "ml_g_source_remove" + external add_watch : + cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id +--- lablgtk-2.18.3.orig/src/Makefile 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/Makefile 2018-04-25 10:58:54.506522500 +0200 +@@ -461,9 +461,9 @@ + do rm -f "$(BINDIR)"/$$f; done + + lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS) +- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) ++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) + lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx) +- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) ++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) + lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS) + + lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS) +--- lablgtk-2.18.3.orig/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/ml_glib.c 2018-04-25 10:58:54.539535600 +0200 +@@ -25,6 +25,8 @@ + #include <string.h> + #include <locale.h> + #ifdef _WIN32 ++/* to kill a #warning: include winsock2.h before windows.h */ ++#include <winsock2.h> + #include "win32.h" + #include <wtypes.h> + #include <io.h> +@@ -38,6 +40,11 @@ + #include <caml/callback.h> + #include <caml/threads.h> + ++#ifdef _WIN32 ++/* for Socket_val */ ++#include <caml/unixsupport.h> ++#endif ++ + #include "wrappers.h" + #include "ml_glib.h" + #include "glib_tags.h" +@@ -325,14 +332,23 @@ + + #ifndef _WIN32 + ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref) ++CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) { ++ return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1))); ++} + + #else + CAMLprim value ml_g_io_channel_unix_new(value wh) + { + return Val_GIOChannel_noref +- (g_io_channel_unix_new ++ (g_io_channel_win32_new_fd + (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY))); + } ++ ++CAMLprim value ml_g_io_channel_unix_new_socket(value wh) ++{ ++ return Val_GIOChannel_noref ++ (g_io_channel_win32_new_socket(Socket_val(wh))); ++} + #endif + + static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c, diff --git a/dev/ci/README.md b/dev/ci/README.md index 697a160ca..dc586c61f 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -89,6 +89,11 @@ We are currently running tests on the following platforms: - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. +GitLab CI and Travis CI and AppVeyor support putting `[ci skip]` in a commit +message to bypass CI. Do not use this unless your commit only changes files +that are not compiled (e.g. Markdown files like this one, or files under +[`.github/`](/.github/)). + You can anticipate the results of most of these tests prior to submitting your PR by running GitLab CI on your private branches. To do so follow these steps: diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index c72705c7f..7bf9ad8c9 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -1,9 +1,15 @@ #!/bin/bash + set -e -x + +APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c + wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh -opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c + +opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH eval "$(opam config env)" -opam install -y ocamlfind camlp5 ounit +opam install -y num ocamlfind camlp5 ounit + cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 8d490591b..0b0e06e29 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,6 +5,10 @@ ci_dir="$(dirname "$0")" CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert" +# Temporal workaround, to be removed when upstream decides what to do +# with their problem. +opam install -y menhir.20180528 + git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}" ( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh new file mode 100644 index 000000000..e6c48d10a --- /dev/null +++ b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then + Equations_CI_BRANCH=unification-returns-option + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi diff --git a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh new file mode 100644 index 000000000..6939ead2b --- /dev/null +++ b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then + + # this branch contains a commit not present on coq-master that triggers + # the universe restriction bug #7472 + Elpi_CI_BRANCH=overlay-7495 + Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 4838dd734..bb8189efc 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -28,6 +28,10 @@ Proof engine should indicate what the canonical form is. An important change is the move of `Globnames.global_reference` to `Names.GlobRef.t`. +- Unification API returns `evar_map option` instead of `bool * evar_map` + with the guarantee that the `evar_map` was unchanged if the boolean + was false. + ML Libraries used by Coq - Introduction of a "Smart" module for collecting "smart*" functions, e.g. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 6ea1c162f..ff5d352c9 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2240,6 +2240,7 @@ This option (off by default) activates the full display of how the context of an existential variable is instantiated at each of the occurrences of the existential variable. +.. _tactics-in-terms: Solving existential variables using tactics ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 59a88771a..5dba92429 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -139,7 +139,19 @@ Here we describe only few of them. can be extended by including other paths in which ``*.cm*`` files are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq`` lets you build a plugin containing OCaml code that depends on the - OCaml code of ``Unicoq``. + OCaml code of ``Unicoq`` +:COQFLAGS: + override the flags passed to ``coqc``. By default ``-q``. +:COQEXTRAFLAGS: + extend the flags passed to ``coqc`` +:COQCHKFLAGS: + override the flags passed to ``coqchk``. By default ``-silent -o``. +:COQCHKEXTRAFLAGS: + extend the flags passed to ``coqchk`` +:COQDOCFLAGS: + override the flags passed to ``coqdoc``. By default ``-interpolate -utf8``. +:COQDOCEXTRAFLAGS: + extend the flags passed to ``coqdoc`` **Rule extension** diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 29e0b34bc..90ca0da43 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3703,19 +3703,24 @@ Setting implicit automation tactics time the term argument of a tactic has one of its holes not fully resolved. - .. example:: + .. deprecated:: 8.9 - .. coqtop:: all + This command is deprecated. Use :ref:`typeclasses <typeclasses>` or + :ref:`tactics-in-terms <tactics-in-terms>` instead. - Parameter quo : nat -> forall n:nat, n<>0 -> nat. - Notation "x // y" := (quo x y _) (at level 40). - Declare Implicit Tactic assumption. - Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. - intros. - exists (n // m). + .. example:: + + .. coqtop:: all + + Parameter quo : nat -> forall n:nat, n<>0 -> nat. + Notation "x // y" := (quo x y _) (at level 40). + Declare Implicit Tactic assumption. + Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. + intros. + exists (n // m). - The tactic ``exists (n // m)`` did not fail. The hole was solved - by ``assumption`` so that it behaved as ``exists (quo n m H)``. + The tactic ``exists (n // m)`` did not fail. The hole was solved + by ``assumption`` so that it behaved as ``exists (quo n m H)``. .. _decisionprocedures: diff --git a/engine/univops.ml b/engine/univops.ml index 76dbaa250..3fd518490 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -35,79 +35,14 @@ let universes_of_constr env c = | _ -> Constr.fold aux s c in aux LSet.empty c -type graphnode = { - mutable up : constraint_type LMap.t; - mutable visited : bool -} - -let merge_types d d0 = - match d, d0 with - | _, Lt | Lt, _ -> Lt - | Le, _ | _, Le -> Le - | Eq, Eq -> Eq - -let merge_up d b up = - let find = try Some (LMap.find b up) with Not_found -> None in - match find with - | Some d0 -> - let d = merge_types d d0 in - if d == d0 then up else LMap.add b d up - | None -> LMap.add b d up - -let add_up a d b graph = - let node, graph = - try LMap.find a graph, graph - with Not_found -> - let node = { up = LMap.empty; visited = false } in - node, LMap.add a node graph - in - node.up <- merge_up d b node.up; - graph - -(* for each node transitive close until you find a non removable, discard the rest *) -let transitive_close removable graph = - let rec do_node a node = - if not node.visited - then - let keepup = - LMap.fold (fun b d keepup -> - if not (LSet.mem b removable) - then merge_up d b keepup - else - begin - match LMap.find b graph with - | bnode -> - do_node b bnode; - LMap.fold (fun k d' keepup -> - merge_up (merge_types d d') k keepup) - bnode.up keepup - | exception Not_found -> keepup - end - ) - node.up LMap.empty - in - node.up <- keepup; - node.visited <- true - in - LMap.iter do_node graph - -let restrict_universe_context (univs,csts) keep = - let removable = LSet.diff univs keep in - let (csts, rem) = - Constraint.fold (fun (a,d,b as cst) (csts, rem) -> - if LSet.mem a removable || LSet.mem b removable - then (csts, add_up a d b rem) - else (Constraint.add cst csts, rem)) - csts (Constraint.empty, LMap.empty) - in - transitive_close removable rem; - let csts = - LMap.fold (fun a node csts -> - if LSet.mem a removable - then csts - else - LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts) - node.up csts) - rem csts - in +let restrict_universe_context (univs, csts) keep = + let removed = LSet.diff univs keep in + if LSet.is_empty removed then univs, csts + else + let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in + let g = UGraph.empty_universes in + let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in + let g = UGraph.merge_constraints csts g in + let allkept = LSet.diff allunivs removed in + let csts = UGraph.constraints_for ~kept:allkept g in (LSet.inter univs keep, csts) diff --git a/engine/univops.mli b/engine/univops.mli index d1585414c..0b37ab975 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -14,5 +14,8 @@ open Univ (** The universes of monomorphic constants appear. *) val universes_of_constr : Environ.env -> constr -> LSet.t -(** Shrink a universe context to a restricted set of variables *) +(** [restrict_universe_context (univs,csts) keep] restricts [univs] to + the universes in [keep]. The constraints [csts] are adjusted so + that transitive constraints between remaining universes (those in + [keep] and those not in [univs]) are preserved. *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t diff --git a/kernel/constr.ml b/kernel/constr.ml index 8f83d6baa..c11b9ebf4 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -479,6 +479,34 @@ let iter_with_binders g f n c = match kind c with Array.Fun1.iter f n tl; Array.Fun1.iter f (iterate g (Array.length tl) n) bl +(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate + subterms of [c] starting from [acc] and proceeding from left to + right according to the usual representation of the constructions as + [fold_constr] but it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive *) + +let fold_constr_with_binders g f n acc c = + match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g n) (f n acc t) c + | Lambda (na,t,c) -> f (g n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (p,c) -> f n acc c + | Evar (_,l) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + (* [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) diff --git a/kernel/constr.mli b/kernel/constr.mli index b35ea6653..742a13919 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -402,6 +402,15 @@ val iter : (constr -> unit) -> constr -> unit val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +(** [iter_with_binders g f n c] iters [f n] on the immediate + subterms of [c]; it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive and the order with which + subterms are processed is not specified *) + +val fold_constr_with_binders : + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b + type constr_compare_fn = int -> constr -> constr -> bool (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 913c13173..7bd70c050 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -52,7 +52,7 @@ type inline = int option type projection_body = { proj_ind : MutInd.t; proj_npars : int; - proj_arg : int; + proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) proj_eta : constr * types; (* Eta-expanded term and type *) proj_body : constr; (* For compatibility with VMs only, the match version *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 036cd4847..8257dc8b8 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -53,7 +53,7 @@ type gname = | Gind of string * inductive (* prefix, inductive name *) | Gconstruct of string * constructor (* prefix, constructor name *) | Gconstant of string * Constant.t (* prefix, constant name *) - | Gproj of string * Constant.t (* prefix, constant name *) + | Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *) | Gcase of Label.t option * int | Gpred of Label.t option * int | Gfixtype of Label.t option * int @@ -108,7 +108,7 @@ let gname_hash gn = match gn with | Ginternal s -> combinesmall 9 (String.hash s) | Grel i -> combinesmall 10 (Int.hash i) | Gnamed id -> combinesmall 11 (Id.hash id) -| Gproj (s, p) -> combinesmall 12 (combine (String.hash s) (Constant.hash p)) +| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i)) let case_ctr = ref (-1) @@ -152,6 +152,7 @@ type symbol = | SymbMeta of metavariable | SymbEvar of Evar.t | SymbLevel of Univ.Level.t + | SymbProj of (inductive * int) let dummy_symb = SymbValue (dummy_value ()) @@ -166,6 +167,7 @@ let eq_symbol sy1 sy2 = | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 + | SymbProj (i1, k1), SymbProj (i2, k2) -> eq_ind i1 i2 && Int.equal k1 k2 | _, _ -> false let hash_symbol symb = @@ -179,6 +181,7 @@ let hash_symbol symb = | SymbMeta m -> combinesmall 7 m | SymbEvar evk -> combinesmall 8 (Evar.hash evk) | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) + | SymbProj (i, k) -> combinesmall 10 (combine (ind_hash i) k) module HashedTypeSymbol = struct type t = symbol @@ -241,6 +244,11 @@ let get_level tbl i = | SymbLevel u -> u | _ -> anomaly (Pp.str "get_level failed.") +let get_proj tbl i = + match tbl.(i) with + | SymbProj p -> p + | _ -> anomaly (Pp.str "get_proj failed.") + let push_symbol x = try HashtblSymbol.find symb_tbl x with Not_found -> @@ -885,6 +893,10 @@ let get_level_code i = MLapp (MLglobal (Ginternal "get_level"), [|MLglobal symbols_tbl_name; MLint i|]) +let get_proj_code i = + MLapp (MLglobal (Ginternal "get_proj"), + [|MLglobal symbols_tbl_name; MLint i|]) + type rlist = | Rnil | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' @@ -1070,7 +1082,7 @@ let ml_of_instance instance u = | Lconst (prefix, (c, u)) -> let args = ml_of_instance env.env_univ u in mkMLapp (MLglobal(Gconstant (prefix, c))) args - | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c)) + | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i)) | Lprim _ -> let decl,cond,paux = extract_prim (ml_of_lam env l) t in compile_prim decl cond paux @@ -1544,8 +1556,8 @@ let string_of_gname g = Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) | Gconstant (prefix, c) -> Format.sprintf "%sconst_%s" prefix (string_of_con c) - | Gproj (prefix, c) -> - Format.sprintf "%sproj_%s" prefix (string_of_con c) + | Gproj (prefix, (mind, n), i) -> + Format.sprintf "%sproj_%s_%i_%i" prefix (string_of_mind mind) n i | Gcase (l,i) -> Format.sprintf "case_%s_%i" (string_of_label_def l) i | Gpred (l,i) -> @@ -1858,8 +1870,6 @@ and compile_named env sigma univ auxdefs id = Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs let compile_constant env sigma prefix ~interactive con cb = - match cb.const_proj with - | false -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1903,39 +1913,6 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | true -> - let pb = lookup_projection (Projection.make con false) env in - let mind = pb.proj_ind in - let ind = (mind,0) in - let mib = lookup_mind mind env in - let oib = mib.mind_packets.(0) in - let tbl = oib.mind_reloc_tbl in - (* Building info *) - let prefix = get_mind_prefix env mind in - let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; - ci_cstr_nargs = [|0|]; - ci_cstr_ndecls = [||] (*FIXME*); - ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in - let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; - asw_reloc = tbl; asw_finite = true } in - let c_uid = fresh_lname Anonymous in - let cf_uid = fresh_lname Anonymous in - let _, arity = tbl.(0) in - let ci_uid = fresh_lname Anonymous in - let cargs = Array.init arity - (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) - in - let i = push_symbol (SymbConst con) in - let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in - let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in - let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in - let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in - let gn = Gproj ("",con) in - let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in - let arg = fargs.(pb.proj_npars) in - Glet(Gconstant ("", con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal - arg|]))):: - [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) @@ -1962,10 +1939,12 @@ let arg_name = Name (Id.of_string "arg") let compile_mind prefix ~interactive mb mind stack = let u = Declareops.inductive_polymorphic_context mb in + (** Generate data for every block *) let f i stack ob = - let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in - let j = push_symbol (SymbInd (mind,i)) in - let name = Gind ("", (mind, i)) in + let ind = (mind, i) in + let gtype = Gtype(ind, Array.map snd ob.mind_reloc_tbl) in + let j = push_symbol (SymbInd ind) in + let name = Gind ("", ind) in let accu = let args = if Int.equal (Univ.AUContext.size u) 0 then @@ -1979,12 +1958,41 @@ let compile_mind prefix ~interactive mb mind stack = Array.init nparams (fun i -> {lname = param_name; luid = i}) in let add_construct j acc (_,arity) = let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in - let c = (mind,i), (j+1) in + let c = ind, (j+1) in Glet(Gconstruct ("", c), mkMLlam (Array.append params args) (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in - Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl + let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in + let add_proj j acc pb = + let tbl = ob.mind_reloc_tbl in + (* Building info *) + let ci = { ci_ind = ind; ci_npar = nparams; + ci_cstr_nargs = [|0|]; + ci_cstr_ndecls = [||] (*FIXME*); + ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in + let asw = { asw_ind = ind; asw_prefix = ""; asw_ci = ci; + asw_reloc = tbl; asw_finite = true } in + let c_uid = fresh_lname Anonymous in + let cf_uid = fresh_lname Anonymous in + let _, arity = tbl.(0) in + let ci_uid = fresh_lname Anonymous in + let cargs = Array.init arity + (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) + in + let i = push_symbol (SymbProj (ind, j)) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in + let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in + let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in + let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in + Glet (gn, mkMLlam [|c_uid|] code) :: acc + in + let projs = match mb.mind_record with + | None | Some None -> [] + | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs + in + projs @ constructors @ gtype :: accu :: stack in Array.fold_left_i f stack mb.mind_packets @@ -2017,25 +2025,22 @@ let compile_mind_deps env prefix ~interactive (* This function compiles all necessary dependencies of t, and generates code in reverse order, as well as linking information updates *) -let rec compile_deps env sigma prefix ~interactive init t = +let compile_deps env sigma prefix ~interactive init t = + let rec aux env lvl init t = match kind t with | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind | Const c -> - let c,u = get_alias env c in - let cb,(nameref,_) = lookup_constant_key c env in - let (_, (_, const_updates)) = init in - if is_code_loaded ~interactive nameref - || (Cmap_env.mem c const_updates) - then init - else + let c,u = get_alias env c in + let cb,(nameref,_) = lookup_constant_key c env in + let (_, (_, const_updates)) = init in + if is_code_loaded ~interactive nameref + || (Cmap_env.mem c const_updates) + then init + else let comp_stack, (mind_updates, const_updates) = - match cb.const_proj, cb.const_body with - | false, Def t -> - compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) - | true, _ -> - let pb = lookup_projection (Projection.make c false) env in - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind + match cb.const_body with + | Def t -> + aux env lvl init (Mod_subst.force_constr t) | _ -> init in let code, name = @@ -2046,13 +2051,32 @@ let rec compile_deps env sigma prefix ~interactive init t = comp_stack, (mind_updates, const_updates) | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> - let term = mkApp (mkConst (Projection.constant p), [|c|]) in - compile_deps env sigma prefix ~interactive init term + let pb = lookup_projection p env in + let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in + aux env lvl init c | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in - Constr.fold (compile_deps env sigma prefix ~interactive) init t - | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t + fold_constr_with_binders succ (aux env) lvl init t + | Var id -> + let open Context.Named.Declaration in + begin match lookup_named id env with + | LocalDef (_,t,_) -> + aux env lvl init t + | _ -> init + end + | Rel n when n > lvl -> + let open Context.Rel.Declaration in + let decl = lookup_rel n env in + let env = env_of_rel n env in + begin match decl with + | LocalDef (_,t,_) -> + aux env lvl init t + | LocalAssum _ -> init + end + | _ -> fold_constr_with_binders succ (aux env) lvl init t + in + aux env 0 init t let compile_constant_field env prefix con acc cb = let (gl, _) = diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 42f2cbc2e..684983a87 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -50,6 +50,8 @@ val get_evar : symbols -> int -> Evar.t val get_level : symbols -> int -> Univ.Level.t +val get_proj : symbols -> int -> inductive * int + val get_symbols : unit -> symbols type code_location_update diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c07025660..e97dbd0d6 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -114,8 +114,8 @@ and conv_atom env pb lvl a1 a2 cu = let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu - | Aproj(p1,ac1), Aproj(p2,ac2) -> - if not (Constant.equal p1 p2) then raise NotConvertible + | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) -> + if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index c319be32d..eaad8ee0c 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -31,7 +31,7 @@ and lambda = | Llet of Name.t * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant - | Lproj of prefix * Constant.t (* prefix, projection name *) + | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) | Lprim of prefix * Constant.t * CPrimitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 8b61ed0c5..0325a00b4 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -296,15 +296,17 @@ let is_value lc = match lc with | Lval _ -> true | Lmakeblock(_,_,_,args) when Array.is_empty args -> true + | Luint (UintVal _) -> true | _ -> false - + let get_value lc = match lc with | Lval v -> v - | Lmakeblock(_,_,tag,args) when Array.is_empty args -> + | Lmakeblock(_,_,tag,args) when Array.is_empty args -> Nativevalues.mk_int tag + | Luint (UintVal i) -> Nativevalues.mk_uint i | _ -> raise Not_found - + let make_args start _end = Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) @@ -517,8 +519,11 @@ let rec lambda_of_constr env sigma c = | Construct _ -> lambda_of_app env sigma c empty_args | Proj (p, c) -> - let kn = Projection.constant p in - mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|] + let pb = lookup_projection p !global_env in + (** FIXME: handle mutual records *) + let ind = (pb.proj_ind, 0) in + let prefix = get_mind_prefix !global_env (fst ind) in + mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index cfcb0a485..da4413a0a 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -64,7 +64,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t * t array - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator let accumulate_tag = 0 diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 4a58a3c7d..649853f06 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -54,7 +54,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t (* type *) * t array (* arguments *) - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator (* Constructors *) @@ -71,7 +71,7 @@ val mk_fix_accu : rec_pos -> int -> t array -> t array -> t val mk_cofix_accu : int -> t array -> t array -> t val mk_meta_accu : metavariable -> t val mk_evar_accu : Evar.t -> t -> t array -> t -val mk_proj_accu : Constant.t -> accumulator -> t +val mk_proj_accu : (inductive * int) -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t val mk_const : tag -> t diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index e6b27077b..4a9467de5 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -503,7 +503,7 @@ let insert_edge strict ucan vcan g = let () = cleanup_universes g in raise e -let add_universe vlev strict g = +let add_universe_gen vlev g = try let _arcv = UMap.find vlev g.entries in raise AlreadyDeclared @@ -520,8 +520,14 @@ let add_universe vlev strict g = } in let entries = UMap.add vlev (Canonical v) g.entries in - let g = { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } in - insert_edge strict (get_set_arc g) v g + { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }, v + +let add_universe vlev strict g = + let g, v = add_universe_gen vlev g in + insert_edge strict (get_set_arc g) v g + +let add_universe_unconstrained vlev g = + fst (add_universe_gen vlev g) exception Found_explanation of explanation @@ -696,6 +702,9 @@ let enforce_univ_lt u v g = error_inconsistency Lt u v (get_explanation false v u g) let empty_universes = + { entries = UMap.empty; index = 0; n_nodes = 0; n_edges = 0 } + +let initial_universes = let set_arc = Canonical { univ = Level.set; ltle = LMap.empty; @@ -718,9 +727,6 @@ let empty_universes = let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in enforce_univ_lt Level.prop Level.set empty -(* Prop = Set is forbidden here. *) -let initial_universes = empty_universes - let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries let enforce_constraint cst g = @@ -780,6 +786,42 @@ let constraints_of_universes g = let csts = UMap.fold constraints_of g.entries Constraint.empty in csts, UF.partition uf +(* domain g.entries = kept + removed *) +let constraints_for ~kept g = + (* rmap: partial map from canonical universes to kept universes *) + let rmap, csts = LSet.fold (fun u (rmap,csts) -> + let arcu = repr g u in + if LSet.mem arcu.univ kept then + LMap.add arcu.univ arcu.univ rmap, enforce_eq_level u arcu.univ csts + else + match LMap.find arcu.univ rmap with + | v -> rmap, enforce_eq_level u v csts + | exception Not_found -> LMap.add arcu.univ u rmap, csts) + kept (LMap.empty,Constraint.empty) + in + let rec add_from u csts todo = match todo with + | [] -> csts + | (v,strict)::todo -> + let v = repr g v in + (match LMap.find v.univ rmap with + | v -> + let d = if strict then Lt else Le in + let csts = Constraint.add (u,d,v) csts in + add_from u csts todo + | exception Not_found -> + (* v is not equal to any kept universe *) + let todo = LMap.fold (fun v' strict' todo -> + (v',strict || strict') :: todo) + v.ltle todo + in + add_from u csts todo) + in + LSet.fold (fun u csts -> + let arc = repr g u in + LMap.fold (fun v strict csts -> add_from u csts [v,strict]) + arc.ltle csts) + kept csts + (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index cca2eb472..e6dd629e4 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -49,13 +49,15 @@ exception AlreadyDeclared val add_universe : Level.t -> bool -> t -> t +(** Add a universe without (Prop,Set) <= u *) +val add_universe_unconstrained : Level.t -> t -> t + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t (** The empty graph of universes *) val empty_universes : t -[@@ocaml.deprecated "Use UGraph.initial_universes"] val sort_universes : t -> t @@ -64,6 +66,12 @@ val sort_universes : t -> t of the universes into equivalence classes. *) val constraints_of_universes : t -> Constraint.t * LSet.t list +(** [constraints_for ~kept g] returns the constraints about the + universes [kept] in [g] up to transitivity. + + eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *) +val constraints_for : kept:LSet.t -> t -> Constraint.t + val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index c5254b37c..cb7183638 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -285,77 +285,6 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint END (**********************************************************************) -(* Hint Resolve *) - -open EConstr -open Vars -open Coqlib - -let project_hint ~poly pri l2r r = - let gr = Smartlocate.global_with_alias r in - let env = Global.env() in - let sigma = Evd.from_env env in - let sigma, c = Evd.fresh_global env sigma gr in - let t = Retyping.get_type_of env sigma c in - let t = - Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in - let sign,ccl = decompose_prod_assum sigma t in - let (a,b) = match snd (decompose_app sigma ccl) with - | [a;b] -> (a,b) - | _ -> assert false in - let p = - if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let sigma, p = Evd.fresh_global env sigma p in - let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in - let c = it_mkLambda_or_LetIn - (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in - let id = - Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) - in - let ctx = Evd.const_univ_entry ~poly sigma in - let c = EConstr.to_constr sigma c in - let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in - let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in - (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) - -let add_hints_iff ~atts l2r lc n bl = - let open Vernacinterp in - Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl - (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc)) - -VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF - [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) - ":" preident_list(bl) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts true lc n bl; - st - end - ] -| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts true lc n ["core"]; - st - end - ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF - [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) - ":" preident_list(bl) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts false lc n bl; - st - end - ] -| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts false lc n ["core"]; - st - end - ] -END - -(**********************************************************************) (* Refine *) open EConstr @@ -594,10 +523,16 @@ let inImplicitTactic : glob_tactic_expr option -> obj = subst_function = subst_implicit_tactic; classify_function = (fun o -> Dispose)} +let warn_deprecated_implicit_tactic = + CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated" + (fun () -> strbrk "Implicit tactics are deprecated") + let declare_implicit_tactic tac = + let () = warn_deprecated_implicit_tactic () in Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) let clear_implicit_tactic () = + let () = warn_deprecated_implicit_tactic () in Lib.add_anonymous_leaf (inImplicitTactic None) VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 93c63d522..b1c5e131f 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -312,20 +312,22 @@ let unif_HO_args env ise0 pa i ca = (* for HO evars, though hopefully Miller patterns can pick up some of *) (* those cases, and HO matching will mop up the rest. *) let flags_FO env = + let oracle = Environ.oracle env in + let ts = Conv_oracle.get_transp_state oracle in let flags = - { (Unification.default_no_delta_unify_flags ()).Unification.core_unify_flags + { (Unification.default_no_delta_unify_flags ts).Unification.core_unify_flags with Unification.modulo_conv_on_closed_terms = None; Unification.modulo_eta = true; Unification.modulo_betaiota = true; - Unification.modulo_delta_types = Conv_oracle.get_transp_state (Environ.oracle env)} + Unification.modulo_delta_types = ts } in { Unification.core_unify_flags = flags; Unification.merge_unify_flags = flags; Unification.subterm_unify_flags = flags; Unification.allow_K_in_toplevel_higher_order_unification = false; Unification.resolve_evars = - (Unification.default_no_delta_unify_flags ()).Unification.resolve_evars + (Unification.default_no_delta_unify_flags ts).Unification.resolve_evars } let unif_FO env ise p c = Unification.w_unify env ise Reduction.CONV ~flags:(flags_FO env) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 062136ff5..6d08f66c1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -366,13 +366,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( let e = - try - let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) - env evd term1 term2 - in - if b then Success evd - else UnifFailure (evd, ConversionFailed (env,term1,term2)) - with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) + match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with + | Some evd -> Success evd + | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)) + | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with | UnifFailure (evd, e) when not (is_ground_env evd env) -> None diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 978ceed1e..4b8e0e096 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -188,6 +188,14 @@ let branch_of_switch lvl ans bs = bs ci in Array.init (Array.length tbl) branch +let get_proj env ((mind, _n), i) = + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | None | Some None -> + CErrors.anomaly (Pp.strbrk "Return type is not a primitive record") + | Some (Some (_, projs, _)) -> + Projection.make projs.(i) true + let rec nf_val env sigma v typ = match kind_of_value v with | Vaccu accu -> nf_accu env sigma accu @@ -279,9 +287,10 @@ and nf_atom env sigma atom = let codom = nf_type env sigma (codom vn) in mkProd(n,dom,codom) | Ameta (mv,_) -> mkMeta mv - | Aproj(p,c) -> + | Aproj (p, c) -> let c = nf_accu env sigma c in - mkProj(Projection.make p true,c) + let p = get_proj env p in + mkProj(p, c) | _ -> fst (nf_atom_type env sigma atom) and nf_atom_type env sigma atom = @@ -303,10 +312,10 @@ and nf_atom_type env sigma atom = let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in let params,realargs = Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env + hnf_prod_applist_assum env nparamdecls (Inductiveops.type_of_inductive env ind) (Array.to_list params) in - let pT = whd_all env pT in let dep, p = nf_predicate env sigma ind mip params p pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in @@ -357,25 +366,30 @@ and nf_atom_type env sigma atom = | Aproj(p,c) -> let c,tc = nf_accu_type env sigma c in let cj = make_judge c tc in - let uj = Typeops.judge_of_projection env (Projection.make p true) cj in + let p = get_proj env p in + let uj = Typeops.judge_of_projection env p cj in uj.uj_val, uj.uj_type and nf_predicate env sigma ind mip params v pT = - match kind_of_value v, kind pT with - | Vfun f, Prod _ -> + match kind (whd_allnolet env pT) with + | LetIn (name,b,t,pT) -> + let dep,body = + nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in + dep, mkLetIn (name,b,t,body) + | Prod (name,dom,codom) -> begin + match kind_of_value v with + | Vfun f -> let k = nb_rel env in let vb = f (mk_rel_accu k) in - let name,dom,codom = - try decompose_prod env pT with - DestKO -> - CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") - in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) - | Vfun f, _ -> + | _ -> false, nf_type env sigma v + end + | _ -> + match kind_of_value v with + | Vfun f -> let k = nb_rel env in let vb = f (mk_rel_accu k) in let name = Name (Id.of_string "c") in @@ -385,7 +399,7 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in true, mkLambda(name,dom,body) - | _, _ -> false, nf_type env sigma v + | _ -> false, nf_type env sigma v and nf_evar env sigma evk ty args = let evi = try Evd.find sigma evk with Not_found -> assert false in diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 67b7a2a40..4997d0bf0 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -25,4 +25,4 @@ val native_norm : env -> evar_map -> constr -> types -> constr (** Conversion with inference of universe constraints *) val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool + evar_map option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 92f87ab95..b2507b5f2 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1082,9 +1082,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential !evdref cty || occur_existential !evdref tval) then - let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err ?loc (str "Cannot check cast with vm: " ++ @@ -1093,9 +1093,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 6fde86837..7fb1a0a57 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) try - let b, sigma = - let ans = - if pb == Reduction.CUMUL then + let ans = match pb with + | Reduction.CUMUL -> EConstr.leq_constr_universes env sigma x y - else + | Reduction.CONV -> EConstr.eq_constr_universes env sigma x y in let ans = match ans with @@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with - | None -> false, sigma - | Some sigma -> true, sigma - in - if b then sigma, true - else + | Some sigma -> ans + | None -> let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in - sigma', true + Some sigma' with - | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ when catch_incon -> sigma, false + | Reduction.NotConvertible -> None + | Univ.UniverseInconsistency _ when catch_incon -> None | e when is_anomaly e -> report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index ad280d9f3..9256fa7ce 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -277,13 +277,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> - env -> evar_map -> constr -> constr -> evar_map * bool + env -> evar_map -> constr -> constr -> evar_map option (** Conversion with inference of universe constraints *) val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool) -> unit + evar_map option) -> unit val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool + evar_map option (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a @@ -291,7 +291,7 @@ conversion function. Used to pretype vm and native casts. *) val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> (Constr.constr, evar_map) Reduction.generic_conversion_function) -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> - evar_map -> constr -> constr -> evar_map * bool + evar_map -> constr -> constr -> evar_map option (** {6 Special-Purpose Reduction Functions } *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5f7faa13e..5cf6e4b26 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -398,8 +398,13 @@ let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with modulo_betaiota = false; } -let default_no_delta_unify_flags () = - let flags = default_no_delta_core_unify_flags () in { +let default_no_delta_unify_flags ts = + let flags = default_no_delta_core_unify_flags () in + let flags = { flags with + modulo_conv_on_closed_terms = Some ts; + modulo_delta_types = ts + } in + { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = flags; @@ -579,16 +584,16 @@ let constr_cmp pb env sigma flags t u = in match cstrs with | Some cstrs -> - begin try Evd.add_universe_constraints sigma cstrs, true - with Univ.UniverseInconsistency _ -> sigma, false + begin try Some (Evd.add_universe_constraints sigma cstrs) + with Univ.UniverseInconsistency _ -> None | Evd.UniversesDiffer -> if is_rigid_head sigma flags t then - try Evd.add_universe_constraints sigma (force_eqs cstrs), true - with Univ.UniverseInconsistency _ -> sigma, false - else sigma, false + try Some (Evd.add_universe_constraints sigma (force_eqs cstrs)) + with Univ.UniverseInconsistency _ -> None + else None end | None -> - sigma, false + None let do_reduce ts (env, nb) sigma c = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state @@ -623,9 +628,9 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM | None -> sigma | Some n -> if is_ground_term sigma m && is_ground_term sigma n then - let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in - if b then sigma - else error_cannot_unify env sigma (m,n) + match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with + | Some sigma -> sigma + | None -> error_cannot_unify env sigma (m,n) else sigma @@ -740,11 +745,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Evar (evk,_ as ev), Evar (evk',_) when not (Evar.Set.mem evk flags.frozen_evars) && Evar.equal evk evk' -> - let sigma',b = constr_cmp cv_pb env sigma flags cM cN in - if b then - sigma',metasubst,evarsubst - else + begin match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> + sigma, metasubst, evarsubst + | None -> sigma,metasubst,((curenv,ev,cN)::evarsubst) + end | Evar (evk,_ as ev), _ when not (Evar.Set.mem evk flags.frozen_evars) && not (occur_evar sigma evk cN) -> @@ -942,9 +948,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - let sigma', b = constr_cmp cv_pb env sigma flags cM cN in - if b then (sigma', metas, evars) - else + match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> (sigma, metas, evars) + | None -> try reduce curenvnb pb opt substn cM cN with ex when precatchable_exception ex -> let (f1,l1) = @@ -1001,12 +1007,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (* Renounce, maybe metas/evars prevents typing *) sigma else sigma in - let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in - if b then Some (sigma, metasubst, evarsubst) - else - if is_ground_term sigma m1 && is_ground_term sigma n1 then - error_cannot_unify curenv sigma (cM,cN) - else None + match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with + | Some sigma -> + Some (sigma, metasubst, evarsubst) + | None -> + if is_ground_term sigma m1 && is_ground_term sigma n1 then + error_cannot_unify curenv sigma (cM,cN) + else None in match res with | Some substn -> substn @@ -1109,11 +1116,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e then None else - let sigma, b = match flags.modulo_conv_on_closed_terms with + let ans = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n | _ -> constr_cmp cv_pb env sigma flags m n in - if b then Some sigma - else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with + match ans with + | Some sigma -> ans + | None -> + if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some (cv_id, cv_k), (dl_id, dl_k) -> Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k | None,(dl_id, dl_k) -> @@ -1603,8 +1612,10 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1,x), Some (_,c2,_) -> - let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in - if b then Some (evd, c1, x) else raise (NotUnifiable None) + begin match infer_conv ~pb:CONV env evd c1 c2 with + | Some evd -> Some (evd, c1, x) + | None -> raise (NotUnifiable None) + end | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in @@ -1921,10 +1932,11 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in let typp = Typing.meta_type evd' p in let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in - let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in - if not b then + match infer_conv ~pb:CUMUL env evd' predtyp typp with + | None -> error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; + | Some evd' -> w_merge env false flags.merge_unify_flags (evd',[p,pred,(Conv,TypeProcessed)],[]) diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 16ce5c93d..e2e261ae7 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Constr open EConstr open Environ @@ -40,7 +41,7 @@ val default_core_unify_flags : unit -> core_unify_flags val default_no_delta_core_unify_flags : unit -> core_unify_flags val default_unify_flags : unit -> unify_flags -val default_no_delta_unify_flags : unit -> unify_flags +val default_no_delta_unify_flags : transparent_state -> unify_flags val elim_flags : unit -> unify_flags val elim_no_delta_flags : unit -> unify_flags diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index a1ba4a6a9..14c9f49b1 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -266,7 +266,6 @@ and nf_stk ?from:(from=0) env sigma c t stk = let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in - let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma ind mib mip u params dep p in @@ -288,15 +287,24 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkProj(p',c)) ty stk and nf_predicate env sigma ind mip params v pT = - match whd_val v, kind pT with - | Vfun f, Prod _ -> + match kind (whd_allnolet env pT) with + | LetIn (name,b,t,pT) -> + let dep,body = + nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in + dep, mkLetIn (name,b,t,body) + | Prod (name,dom,codom) -> begin + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in - let name,dom,codom = decompose_prod env pT in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) - | Vfun f, _ -> + | _ -> assert false + end + | _ -> + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in let name = Name (Id.of_string "c") in @@ -306,7 +314,7 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in true, mkLambda(name,dom,body) - | _, _ -> false, nf_val env sigma v crazy_type + | _ -> false, nf_val env sigma v crazy_type and nf_args env sigma vargs ?from:(f=0) t = let t = ref t in diff --git a/proofs/logic.ml b/proofs/logic.ml index 218b2671e..95c30d815 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -309,9 +309,10 @@ let check_meta_variables env sigma c = let check_conv_leq_goal env sigma arg ty conclty = if !check then - let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in - if b then evm - else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) + let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in + match ans with + | Some evm -> evm + | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list diff --git a/tactics/hints.ml b/tactics/hints.ml index 4b77418ff..d49c8aaa5 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -167,6 +167,7 @@ type hint_mode = type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * reference list * int option | HintsImmediate of reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool @@ -1290,6 +1291,35 @@ let prepare_hint check (poly,local) env init (sigma,c) = else (Lib.add_anonymous_leaf (input_context_set diff); IsConstr (c', Univ.ContextSet.empty)) +let project_hint ~poly pri l2r r = + let open EConstr in + let open Coqlib in + let gr = Smartlocate.global_with_alias r in + let env = Global.env() in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + let t = Retyping.get_type_of env sigma c in + let t = + Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in + let sign,ccl = decompose_prod_assum sigma t in + let (a,b) = match snd (decompose_app sigma ccl) with + | [a;b] -> (a,b) + | _ -> assert false in + let p = + if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in + let sigma, p = Evd.fresh_global env sigma p in + let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in + let c = it_mkLambda_or_LetIn + (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in + let id = + Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) + in + let ctx = Evd.const_univ_entry ~poly sigma in + let c = EConstr.to_constr sigma c in + let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in + let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in + (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) + let interp_hints poly = fun h -> let env = Global.env () in @@ -1319,6 +1349,8 @@ let interp_hints poly = in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) + | HintsResolveIFF (l2r, lc, n) -> + HintsResolveEntry (List.map (project_hint ~poly n l2r) lc) | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints) | HintsTransparency (lhints, b) -> diff --git a/tactics/hints.mli b/tactics/hints.mli index 7ef7f0185..e958f986e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -83,6 +83,7 @@ type hint_mode = type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * Libnames.reference list * int option | HintsImmediate of reference_or_constr list | HintsUnfold of Libnames.reference list | HintsTransparency of Libnames.reference list * bool diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 58c62af85..b571b347d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -158,9 +158,9 @@ let convert_concl ?(check=true) ty k = let sigma = if check then begin ignore (Typing.unsafe_type_of env sigma ty); - let sigma,b = Reductionops.infer_conv env sigma ty conclty in - if not b then error "Not convertible."; - sigma + match Reductionops.infer_conv env sigma ty conclty with + | None -> error "Not convertible." + | Some sigma -> sigma end else sigma in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in @@ -186,11 +186,10 @@ let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> - try - let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in - if b then Proofview.Unsafe.tclEVARS sigma - else Tacticals.New.tclFAIL 0 (str "Not convertible") - with (* Reduction.NotConvertible *) _ -> + match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with + | Some sigma -> Proofview.Unsafe.tclEVARS sigma + | None -> Tacticals.New.tclFAIL 0 (str "Not convertible") + | exception _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") end @@ -796,15 +795,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let t2 = Retyping.get_type_of env sigma origc in let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t2 in - let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in - if not b then + match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with + | None -> if isSort sigma (whd_all env sigma t1) && isSort sigma (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.") - else sigma + | Some sigma -> sigma end else if not (isSort sigma (whd_all env sigma t1)) then @@ -815,9 +814,9 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = let (sigma, t') = t sigma in let sigma = check_types env sigma mayneedglobalcheck deep t' c in - let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in - if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible."); - (sigma, t') + match infer_conv ~pb:cv_pb env sigma t' c with + | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible."); + | Some sigma -> (sigma, t') (* Use cumulativity only if changing the conclusion not a subterm *) let change_on_subterm cv_pb deep t where env sigma c = @@ -1638,13 +1637,11 @@ let tclORELSEOPT t k = Proofview.tclZERO ~info e | Some tac -> tac) -let general_apply with_delta with_destruct with_evars clear_flag - {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} = +let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars + clear_flag {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in - let flags = - if with_delta then default_unify_flags () else default_no_delta_unify_flags () in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) @@ -1653,7 +1650,12 @@ let general_apply with_delta with_destruct with_evars clear_flag Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - + let ts = + if respect_opaque then Conv_oracle.get_transp_state (oracle env) + else full_transparent_state + in + let flags = + if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try @@ -1719,14 +1721,14 @@ let rec apply_with_bindings_gen b e = function (general_apply b b e k cb) (apply_with_bindings_gen b e cbl) -let apply_with_delayed_bindings_gen b e l = +let apply_with_delayed_bindings_gen b e l = let one k {CAst.loc;v=f} = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let (sigma, cb) = f env sigma in Tacticals.New.tclWITHHOLES e - (general_apply b b e k CAst.(make ?loc cb)) sigma + (general_apply ~respect_opaque:(not b) b b e k CAst.(make ?loc cb)) sigma end in let rec aux = function @@ -1801,14 +1803,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = in aux (make_clenv_binding env sigma (d,thm) lbind) -let apply_in_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,{ CAst.loc; v= d,lbind}) tac = +let apply_in_once ?(respect_opaque = false) sidecond_first with_delta + with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let flags = - if with_delta then default_unify_flags () else default_no_delta_unify_flags () in let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in @@ -1816,6 +1816,12 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in + let ts = + if respect_opaque then Conv_oracle.get_transp_state (oracle env) + else full_transparent_state + in + let flags = + if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in clenv_refine_in ~sidecond_first with_evars targetid id sigma clause @@ -1835,14 +1841,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming aux [] with_destruct d end -let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,{CAst.loc;v=f}) tac = +let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta + with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (sigma, c) = f env sigma in Tacticals.New.tclWITHHOLES with_evars - (apply_in_once sidecond_first with_delta with_destruct with_evars + (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars naming id (clear_flag,CAst.(make ?loc c)) tac) sigma end @@ -1934,16 +1940,19 @@ let assumption = let t = NamedDecl.get_type decl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in - let (sigma, is_same_type) = - if only_eq then (sigma, EConstr.eq_constr sigma t concl) + let ans = + if only_eq then + if EConstr.eq_constr sigma t concl then Some sigma + else None else let env = Proofview.Goal.env gl in infer_conv env sigma t concl in - if is_same_type then + match ans with + | Some sigma -> (Proofview.Unsafe.tclEVARS sigma) <*> exact_no_check (mkVar (NamedDecl.get_id decl)) - else arec gl only_eq rest + | None -> arec gl only_eq rest in let assumption_tac gl = let hyps = Proofview.Goal.hyps gl in @@ -2529,11 +2538,11 @@ let assert_as first hd ipat t = (* apply in as *) -let general_apply_in sidecond_first with_delta with_destruct with_evars - id lemmas ipat = +let general_apply_in ?(respect_opaque=false) sidecond_first with_delta + with_destruct with_evars id lemmas ipat = let tac (naming,lemma) tac id = - apply_in_delayed_once sidecond_first with_delta with_destruct with_evars - naming id lemma tac in + apply_in_delayed_once ~respect_opaque sidecond_first with_delta + with_destruct with_evars naming id lemma tac in Proofview.Goal.enter begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) @@ -2564,7 +2573,7 @@ let apply_in simple with_evars id lemmas ipat = general_apply_in false simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = - general_apply_in false simple simple with_evars id lemmas ipat + general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat (*****************************) (* Tactics abstracting terms *) diff --git a/test-suite/Makefile b/test-suite/Makefile index f41fb5b1e..32e245e36 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -362,26 +362,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ + output=$*.out.real; \ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ | grep -v "^<W>" \ | sed 's/File "[^"]*"/File "stdin"/' \ - > $$tmpoutput; \ - diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \ + > $$output; \ + diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ + rm $$output; \ else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ $(FAIL); \ fi; \ - rm $$tmpoutput; \ } > "$@" +.PHONY: approve-output +approve-output: output + $(HIDE)for f in output/*.out.real; do \ + mv "$$f" "$${f%.real}"; \ + echo "Updated $${f%.real}!"; \ + done + # the expected output for the MExtraction test is # /plugins/micromega/micromega.ml except with additional newline output/MExtraction.out: ../plugins/micromega/micromega.ml diff --git a/test-suite/README.md b/test-suite/README.md index 4572c98cf..ef2e574ec 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -76,3 +76,17 @@ There are also output tests in `test-suite/output` which consist of a `.v` file There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit` unit-test framework, as described at http://ounit.forge.ocamlcore.org/. Use `make unit-tests' in the unit-tests directory to run them. + +## Fixing output tests + +When an output test `output/foo.v` fails, the output is stored in +`output/foo.out.real`. Move that file to the reference file +`output/foo.out` to update the test, approving the new output. Target +`approve-output` will do this for all failing output tests +automatically. + +Don't forget to check the updated `.out` files into git! + +Note that `output/MExtraction.out` is special: it is copied from +`micromega/micromega.ml` in the plugin source directory. Automatic +approval will incorrectly update the copy. diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v deleted file mode 100644 index 8c26af708..000000000 --- a/test-suite/bugs/closed/4882.v +++ /dev/null @@ -1,50 +0,0 @@ - -Definition Foo {T}{a : T} : T := a. - -Module A. - - Declare Implicit Tactic eauto. - - Goal forall A (x : A), A. - intros. - apply Foo. (* Check defined evars are normalized *) - (* Qed. *) - Abort. - -End A. - -Module B. - - Definition Foo {T}{a : T} : T := a. - - Declare Implicit Tactic eassumption. - - Goal forall A (x : A), A. - intros. - apply Foo. - (* Qed. *) - Abort. - -End B. - -Module C. - - Declare Implicit Tactic first [exact True|assumption]. - - Goal forall (x : True), True. - intros. - apply (@Foo _ _). - Qed. - -End C. - -Module D. - - Declare Implicit Tactic assumption. - - Goal forall A (x : A), A. - intros. - exact _. - Qed. - -End D. diff --git a/test-suite/bugs/closed/7068.v b/test-suite/bugs/closed/7068.v new file mode 100644 index 000000000..9fadb195b --- /dev/null +++ b/test-suite/bugs/closed/7068.v @@ -0,0 +1,6 @@ +(* These tests are only about a subset of #7068 *) +(* The original issue is still open *) + +Inductive foo : let T := Type in T := . +Definition bob1 := Eval vm_compute in foo_rect. +Definition bob2 := Eval native_compute in foo_rect. diff --git a/test-suite/bugs/closed/7076.v b/test-suite/bugs/closed/7076.v new file mode 100644 index 000000000..0abc88c28 --- /dev/null +++ b/test-suite/bugs/closed/7076.v @@ -0,0 +1,4 @@ +(* These calls were raising an anomaly at some time *) +Inductive A : nat -> id (nat->Type) := . +Eval vm_compute in fun x => match x in A y z return y = z with end. +Eval native_compute in fun x => match x in A y z return y = z with end. diff --git a/test-suite/bugs/closed/7631.v b/test-suite/bugs/closed/7631.v new file mode 100644 index 000000000..34eb8b867 --- /dev/null +++ b/test-suite/bugs/closed/7631.v @@ -0,0 +1,21 @@ +Module NamedContext. + +Definition foo := true. + +Section Foo. + +Let bar := foo. + +Eval native_compute in bar. + +End Foo. + +End NamedContext. + +Module RelContext. + +Definition foo := true. + +Definition bar (x := foo) := Eval native_compute in x. + +End RelContext. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e73312c67..c0b04eb53 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,6 +1,5 @@ The command has indeed failed with message: -To rename arguments the "rename" flag must be specified. -Argument A renamed to B. +Flag "rename" expected to rename A into B. File "stdin", line 2, characters 0-25: Warning: This command is just asserting the names of arguments of identity. If this is what you want add ': assert' to silence the warning. If you want @@ -113,5 +112,4 @@ Argument z cannot be declared implicit. The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: -To rename arguments the "rename" flag must be specified. -Argument A renamed to R. +Flag "rename" expected to rename A into R. diff --git a/test-suite/success/ImplicitTactic.v b/test-suite/success/ImplicitTactic.v deleted file mode 100644 index d8fa3043d..000000000 --- a/test-suite/success/ImplicitTactic.v +++ /dev/null @@ -1,16 +0,0 @@ -(* A Wiedijk-Cruz-Filipe style tactic for solving implicit arguments *) - -(* Declare a term expression with a hole *) -Parameter quo : nat -> forall n:nat, n<>0 -> nat. -Notation "x / y" := (quo x y _) : nat_scope. - -(* Declare the tactic for resolving implicit arguments still - unresolved after type-checking; it must complete the subgoal to - succeed *) -Declare Implicit Tactic assumption. - -Goal forall n d, d<>0 -> { q:nat & { r:nat | d * q + r = n }}. -intros. -(* Here, assumption is used to solve the implicit argument of quo *) -exists (n / d). - diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index c6836a1c7..ed4d69ab0 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -82,7 +82,7 @@ End Retracts. (** This lemma is basically a commutation of implication and existential quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) which is provable in classical logic ( => is already provable in - intuitionnistic logic). *) + intuitionistic logic). *) Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). Proof. @@ -136,7 +136,7 @@ trivial. Qed. -Theorem classical_proof_irrelevence : T = F. +Theorem classical_proof_irrelevance : T = F. Proof. generalize not_has_fixpoint. unfold Not_b. @@ -148,4 +148,7 @@ intros not_true is_true. elim not_true; trivial. Qed. + +Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8"). + End Berardis_paradox. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 3317766c9..66e82ddbf 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -234,8 +234,6 @@ Qed. (** An alternative more concise proof can be done by directly using the guarded relational choice *) -Declare Implicit Tactic auto. - Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2. Proof. assert (decide: forall x:A, x=a1 \/ x=a2 -> diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4 index 56229c765..a3806ff68 100644 --- a/vernac/g_proofs.ml4 +++ b/vernac/g_proofs.ml4 @@ -98,15 +98,8 @@ GEXTEND Gram VernacCreateHintDb (id, b) | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> VernacRemoveHints (dbnames, ids) - | IDENT "Hint"; h = hint; - dbnames = opt_hintbases -> + | IDENT "Hint"; h = hint; dbnames = opt_hintbases -> VernacHints (dbnames, h) - (* Declare "Resolve" explicitly so as to be able to later extend with - "Resolve ->" and "Resolve <-" *) - | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; - info = hint_info; dbnames = opt_hintbases -> - VernacHints (dbnames, - HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; reference_or_constr: [ [ r = global -> HintsReference r @@ -115,6 +108,10 @@ GEXTEND Gram hint: [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> HintsResolve (List.map (fun x -> (info, true, x)) lc) + | IDENT "Resolve"; "->"; lc = LIST1 global; n = OPT natural -> + HintsResolveIFF (true, lc, n) + | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural -> + HintsResolveIFF (false, lc, n) | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index dd8149d0a..b6523981c 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -631,8 +631,8 @@ GEXTEND Gram t = class_rawexpr -> VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t) - | IDENT "Context"; c = binders -> - VernacContext c + | IDENT "Context"; c = LIST1 binder -> + VernacContext (List.flatten c) | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 7aff758e9..5490b9ce5 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -200,6 +200,9 @@ open Pputils keyword "Resolve " ++ prlist_with_sep sep (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info) l + | HintsResolveIFF (l2r, l, n) -> + keyword "Resolve " ++ str (if l2r then "->" else "<-") + ++ prlist_with_sep sep pr_reference l | HintsImmediate l -> keyword "Immediate" ++ spc() ++ prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9a7f59085..7f6270df1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1131,15 +1131,16 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags = let names = rename prev_names names in let renaming_specified = Option.has_some !example_renaming in - if !rename_flag_required && not rename_flag then - user_err ~hdr:"vernac_declare_arguments" - (strbrk "To rename arguments the \"rename\" flag must be specified." - ++ spc () ++ - match !example_renaming with - | None -> mt () - | Some (o,n) -> - str "Argument " ++ Name.print o ++ - str " renamed to " ++ Name.print n ++ str "."); + if !rename_flag_required && not rename_flag then begin + let msg = + match !example_renaming with + | None -> + strbrk "To rename arguments the \"rename\" flag must be specified." + | Some (o,n) -> + strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++ + strbrk " into " ++ Name.print n ++ str "." + in user_err ~hdr:"vernac_declare_arguments" msg + end; let duplicate_names = List.duplicates Name.equal (List.filter ((!=) Anonymous) names) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index fb40f0d9c..9e8dfc4f8 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -124,6 +124,7 @@ type hint_info_expr = Hints.hint_info_expr type hints_expr = Hints.hints_expr = | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list + | HintsResolveIFF of bool * reference list * int option | HintsImmediate of Hints.reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool |