diff options
97 files changed, 2056 insertions, 955 deletions
diff --git a/Makefile.build b/Makefile.build index 5b879220d0..a8ae040f8e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -840,7 +840,7 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP) $(SHOW)'COQC -quick -noinit $<' - $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -quick -noglob + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -vio -noglob # The general rule for building .vo files : @@ -855,8 +855,8 @@ ifdef VALIDATE endif %.vio: %.v theories/Init/Prelude.vio $(VO_TOOLS_DEP) - $(SHOW)'COQC -quick $<' - $(HIDE)$(BOOTCOQC) $< -quick -noglob + $(SHOW)'COQC -vio $<' + $(HIDE)$(BOOTCOQC) $< -vio -noglob %.v.timing.diff: %.v.before-timing %.v.after-timing $(SHOW)PYTHON TIMING-DIFF $< @@ -31,6 +31,9 @@ environment for semi-interactive development of machine-checked proofs. [![Homebrew package][homebrew-badge]][homebrew-link] [![nixpkgs unstable package][nixpkgs-badge]][nixpkgs-link] +[![Docker Hub package][dockerhub-badge]][dockerhub-link] +[![latest dockerized version][coqorg-badge]][coqorg-link] + [repology-badge]: https://repology.org/badge/latest-versions/coq.svg [repology-link]: https://repology.org/metapackage/coq/versions @@ -52,6 +55,12 @@ environment for semi-interactive development of machine-checked proofs. [nixpkgs-badge]: https://repology.org/badge/version-for-repo/nix_unstable/coq.svg [nixpkgs-link]: https://nixos.org/nixos/packages.html#coq +[dockerhub-badge]: https://img.shields.io/docker/automated/coqorg/coq.svg +[dockerhub-link]: https://hub.docker.com/r/coqorg/coq "Automated build on Docker Hub" + +[coqorg-badge]: https://images.microbadger.com/badges/version/coqorg/coq.svg +[coqorg-link]: https://github.com/coq-community/docker-coq/wiki#docker-coq-images "Docker images of Coq" + Download the pre-built packages of the [latest release][] for Windows and macOS; read the [help page][opam-using] on how to install Coq with OPAM; or refer to the [`INSTALL.md`](INSTALL.md) file for the procedure to install from source. diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 31dcae0f82..aba2b05037 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -19,7 +19,7 @@ jobs: powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" SET CYGROOT=C:\cygwin64 SET CYGCACHE=%CYGROOT%\var\cache\setup - setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python2 -P python3 + setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3 SET TARGET_ARCH=x86_64-w64-mingw32 SET CD_MFMT=%cd:\=/% diff --git a/clib/cUnix.ml b/clib/cUnix.ml index c5f6bebb8e..6e3ad59b1f 100644 --- a/clib/cUnix.ml +++ b/clib/cUnix.ml @@ -140,3 +140,20 @@ let same_file f1 = Unix.Unix_error _ -> false) with Unix.Unix_error _ -> (fun _ -> false) + +(* Copied from ocaml filename.ml *) +let prng = lazy(Random.State.make_self_init ()) + +let temp_file_name temp_dir prefix suffix = + let rnd = (Random.State.bits (Lazy.force prng)) land 0xFFFFFF in + Filename.concat temp_dir (Printf.sprintf "%s%06x%s" prefix rnd suffix) + +let mktemp_dir ?(temp_dir=Filename.get_temp_dir_name()) prefix suffix = + let rec try_name counter = + let name = temp_file_name temp_dir prefix suffix in + match Unix.mkdir name 0o700 with + | () -> name + | exception (Sys_error _ as e) -> + if counter >= 1000 then raise e else try_name (counter + 1) + in + try_name 0 diff --git a/clib/cUnix.mli b/clib/cUnix.mli index 17574b3c42..55d307c724 100644 --- a/clib/cUnix.mli +++ b/clib/cUnix.mli @@ -65,3 +65,5 @@ val waitpid_non_intr : int -> Unix.process_status (** Check if two file names refer to the same (existing) file *) val same_file : string -> string -> bool +(** Like [Stdlib.Filename.temp_file] but producing a directory. *) +val mktemp_dir : ?temp_dir:string -> string -> string -> string diff --git a/default.nix b/default.nix index ee4a6046ea..174e199014 100644 --- a/default.nix +++ b/default.nix @@ -41,9 +41,7 @@ stdenv.mkDerivation rec { buildInputs = [ hostname - python2 # update-compat.py python3 time # coq-makefile timing tools - dune ] ++ (with ocamlPackages; [ ocaml findlib num ]) ++ optionals buildIde [ @@ -68,6 +66,7 @@ stdenv.mkDerivation rec { [ jq curl gitFull gnupg ] # Dependencies of the merging script ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ocamlformat ]) # Dev tools ++ [ graphviz ] # Useful for STM debugging + ++ [ dune_2 ] # Maybe the next build system ); src = @@ -112,7 +111,7 @@ stdenv.mkDerivation rec { setupHook = writeText "setupHook.sh" " addCoqPath () { if test -d \"$1/lib/coq/${coq-version}/user-contrib\"; then - export COQPATH=\"$COQPATH\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\" + export COQPATH=\"\${COQPATH-}\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\" fi } diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 87122e0fb5..f04de0ce6c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -209,7 +209,7 @@ ######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_REF:=master}" +: "${bedrock2_CI_REF:=tested}" : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" : "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index a9cc91170f..f08a08531f 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -60,9 +60,23 @@ let iris = (coqPackages.iris.override { inherit coq stdpp; }) let unicoq = callPackage ./unicoq { inherit coq; }; in +let StructTact = coqPackages.StructTact.overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/StructTact/tarball/master"; + }); in + +let Cheerios = (coqPackages.Cheerios.override { inherit StructTact; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/cheerios/tarball/master"; + }); in + +let Verdi = (coqPackages.Verdi.override { inherit Cheerios ssreflect; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/verdi/tarball/master"; + }); in + let callPackage = newScope { inherit coq bignums coq-ext-lib coqprime corn iris math-classes - mathcomp simple-io ssreflect stdpp unicoq; + mathcomp simple-io ssreflect stdpp unicoq Verdi; }; in # Environments for building CI libraries with this Coq @@ -89,6 +103,7 @@ let projects = { mtac2 = callPackage ./mtac2.nix {}; oddorder = callPackage ./oddorder.nix {}; quickchick = callPackage ./quickchick.nix {}; + verdi-raft = callPackage ./verdi-raft.nix {}; VST = callPackage ./VST.nix {}; }; in diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix index 0f0ee91387..1105fba7a6 100644 --- a/dev/ci/nix/fiat_crypto.nix +++ b/dev/ci/nix/fiat_crypto.nix @@ -1,6 +1,6 @@ -{ coqprime }: +{ ocamlPackages }: { - coqBuildInputs = [ coqprime ]; + buildInputs = with ocamlPackages; [ ocaml findlib ]; configure = "git submodule update --init --recursive && ulimit -s 32768"; - make = "make new-pipeline c-files"; + make = "make c-files printlite lite && make -j 1 coq"; } diff --git a/dev/ci/nix/verdi-raft.nix b/dev/ci/nix/verdi-raft.nix new file mode 100644 index 0000000000..6a98f4ef47 --- /dev/null +++ b/dev/ci/nix/verdi-raft.nix @@ -0,0 +1,5 @@ +{ Verdi }: +{ + coqBuildInputs = [ Verdi ]; + configure = "./configure"; +} diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index 677377f868..54baaee1fe 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/f4ad230f90ef312695adc26f256036203e9c70af.tar.gz"; - sha256 = "0cdd275dz3q51sknn7s087js81zvaj5riz8f29id6j6chnyikzjq"; + url = "https://github.com/NixOS/nixpkgs/archive/8da81465c19fca393a3b17004c743e4d82a98e4f.tar.gz"; + sha256 = "1f3s27nrssfk413pszjhbs70wpap43bbjx2pf4zq5x2c1kd72l6y"; }) diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index c0a3eeb11c..a888998ebf 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -137,7 +137,8 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then else error "Local branch is not up-to-date with ${REMOTE}." error "Pull before merging." - ask_confirmation + # This check should never be bypassed. + exit 1 fi fi diff --git a/doc/changelog/01-kernel/11081-native-cleanup.rst b/doc/changelog/01-kernel/11081-native-cleanup.rst new file mode 100644 index 0000000000..b3e3a78b96 --- /dev/null +++ b/doc/changelog/01-kernel/11081-native-cleanup.rst @@ -0,0 +1,4 @@ +- **Changed:** the native compilation (:tacn:`native_compute`) now + creates a directory to contain temporary files instead of putting + them in the root of the system temporary directory. (`#11081 + <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst new file mode 100644 index 0000000000..8c84648aa7 --- /dev/null +++ b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst @@ -0,0 +1,4 @@ +- **Fixed:** `#11360 <https://github.com/issues/11360>`_ + Broken section closing when a template polymorphic inductive type depends on + a section variable through its parameters (`#11361 + <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/04-tactics/11370-zify-elim-let.rst b/doc/changelog/04-tactics/11370-zify-elim-let.rst new file mode 100644 index 0000000000..4eb2732106 --- /dev/null +++ b/doc/changelog/04-tactics/11370-zify-elim-let.rst @@ -0,0 +1,3 @@ +- **Changed** + Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml. + (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson). diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst new file mode 100644 index 0000000000..b9ecd140e7 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst @@ -0,0 +1 @@ +- A section variable introduces with :g:`Let` can be declared as a :g:`Canonical Structure` (`#11164 <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). diff --git a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst new file mode 100644 index 0000000000..97f456036d --- /dev/null +++ b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + The ``-quick`` command is renamed to ``-vio``, for consistency with the new ``-vos`` and ``-vok`` flags. Usage of ``-quick`` is now deprecated. + (`#11280 <https://github.com/coq/coq/pull/11280>`_, + by charguer). diff --git a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst b/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst new file mode 100644 index 0000000000..10952c6b2c --- /dev/null +++ b/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst @@ -0,0 +1,5 @@ +- **Fixed:** + ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints + commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_, + fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, + by Karl Palmskog). diff --git a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst new file mode 100644 index 0000000000..2dc3992b9c --- /dev/null +++ b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst @@ -0,0 +1,5 @@ +- **Changed:** + CoqIDE now uses the GtkSourceView native implementation of + the autocomplete mechanism. + (`#11400 <https://github.com/coq/coq/pull/11400>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst b/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst new file mode 100644 index 0000000000..03c2ccc1d2 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst @@ -0,0 +1,4 @@ +- **Removed:** + Python 2 is not longer required in any part of the codebase. + (`#11245 <https://github.com/coq/coq/pull/11245>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/12-misc/10486-native-string-extraction.rst b/doc/changelog/12-misc/10486-native-string-extraction.rst new file mode 100644 index 0000000000..c6778403d4 --- /dev/null +++ b/doc/changelog/12-misc/10486-native-string-extraction.rst @@ -0,0 +1,7 @@ +- **Added:** + Support for better extraction of strings in OCaml and Haskell: + `ExtOcamlNativeString` provides bindings from the Coq `String` type to + the OCaml `string` type, and string literals can be extracted to literals, + both in OCaml and Haskell. (`#10486 + <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from + Maxime Dénès, review by Hugo Herbelin). diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 7136cc28d1..d909f98956 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -313,14 +313,21 @@ The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML native boolean type instead of the |Coq| one. The syntax is the following: -.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] +.. cmd:: Extract Inductive @qualid => @string__1 [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first :token:`string`) and all its - constructors (all the :token:`string` between square brackets). In this form, + extractions for the type itself (:n:`@string__1`) and all its + constructors (all the :n:`@string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native pattern matching of the language will be used. + When :n:`@string__1` matches the name of the type of characters or strings + (``char`` and ``string`` for OCaml, ``Prelude.Char`` and ``Prelude.String`` + for Haskell), extraction of literals is handled in a specialized way, so as + to generate literals in the target language. This feature requires the type + designated by :n:`@qualid` to be registered as the standard char or string type, + using the :cmd:`Register` command. + .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra :token:`string` that indicates how to diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 650a444a16..daca43e65e 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -5,6 +5,27 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic :Author: Pierre Crégut +.. warning:: + + The :tacn:`omega` tactic is about to be deprecated in favor of the + :tacn:`lia` tactic. The goal is to consolidate the arithmetic + solving capabilities of Coq into a single engine; moreover, + :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a + complete Presburger arithmetic solver while :tacn:`omega` was known + to be incomplete). + + Work is in progress to make sure that there are no regressions + (including no performance regression) when switching from + :tacn:`omega` to :tacn:`lia` in existing projects. However, we + already recommend using :tacn:`lia` in new or refactored proof + scripts. We also ask that you report (in our `bug tracker + <https://github.com/coq/coq/issues>`_) any issue you encounter, + especially if the issue was not present in :tacn:`omega`. + + Note that replacing :tacn:`omega` with :tacn:`lia` can break + non-robust proof scripts which rely on incompleteness bugs of + :tacn:`omega` (e.g. using the pattern :g:`; try omega`). + Description of ``omega`` ------------------------ diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 35729d852d..7a50748c51 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -154,6 +154,18 @@ to a worker process. The threshold can be configured with Batch mode --------------- + .. warning:: + + The ``-vio`` flag is subsumed, for most practical usage, by the + the more recent ``-vos`` flag. See :ref:`compiled-interfaces`. + + .. warning:: + + When working with ``.vio`` files, do not use the ``-vos`` option at + the same time, otherwise stale files might get loaded when executing + a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is + assigned higher priority than the loading of a ``.vio`` file. + When |Coq| is used as a batch compiler by running ``coqc``, it produces a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other things, theorem statements and proofs. Hence to produce a .vo |Coq| @@ -161,10 +173,10 @@ need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the -generation and checking of the proof objects. The ``-quick`` flag can be +generation and checking of the proof objects. The ``-vio`` flag can be passed to ``coqc`` to produce, quickly, ``.vio`` files. Alternatively, when using a Makefile produced by ``coq_makefile``, -the ``quick`` target can be used to compile all files using the ``-quick`` flag. +the ``vio`` target can be used to compile all files using the ``-vio`` flag. A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but proofs will not be available (the Print command produces an error). @@ -173,7 +185,7 @@ inconsistencies might go unnoticed. A ``.vio`` file does not contain proof objects, but proof tasks, i.e. what a worker process can transform into a proof object. -Compiling a set of files with the ``-quick`` flag allows one to work, +Compiling a set of files with the ``-vio`` flag allows one to work, interactively, on any file without waiting for all the proofs to be checked. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 33fc211fa5..21000889d3 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -50,6 +50,11 @@ __ 811RefineInstance_ __ 811SSRUnderOver_ __ 811Reals_ +Additionally, while the :tacn:`omega` tactic is not yet deprecated in +this version of Coq, it should soon be the case and we already +recommend users to switch to :tacn:`lia` in new proof scripts (see +also the warning message in the :ref:`corresponding chapter <omega>`). + The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ section for the detailed list of changes, including potentially breaking changes marked with diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 78428be18f..bdfdffeaad 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1629,8 +1629,8 @@ The syntax is supported in all top-level definitions: :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype declarations, the semantics are the following: an inductive parameter declared as an implicit argument need not be repeated in the inductive -definition but will become implicit for the constructors of the -inductive only, not the inductive type itself. For example: +definition and will become implicit for the inductive type and the constructors. +For example: .. coqtop:: all @@ -1983,6 +1983,8 @@ Deactivation of implicit arguments for parsing to be given as if no arguments were implicit. By symmetry, this also affects printing. +.. _canonical-structure-declaration: + Canonical structures ~~~~~~~~~~~~~~~~~~~~ @@ -1993,6 +1995,7 @@ value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. .. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid + :name: Canonical Structure This command declares :token:`qualid` as a canonical instance of a structure (a record). When the :g:`#[local]` attribute is given the effect @@ -2547,3 +2550,8 @@ the context to help inferring the types of the remaining arguments. Arguments ex_intro _ _ & _ _. Check (ex_intro _ true _ : exists n : nat, n > 0). + +Coq will attempt to produce a term which uses the arguments you +provided, but in some cases involving Program mode the arguments after +the bidirectionality starts may be replaced by convertible but +syntactically different terms. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 368724f9d2..d591718b17 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -327,11 +327,8 @@ function on type :g:`A`). The keyword :g:`fun` can be followed by several binders as given in Section :ref:`binders`. Functions over several variables are equivalent to an iteration of one-variable functions. For instance the expression -“fun :token:`ident`\ :math:`_{1}` … :token:`ident`\ :math:`_{n}` -: :token:`type` => :token:`term`” -denotes the same function as “ fun :token:`ident`\ -:math:`_{1}` : :token:`type` => … -fun :token:`ident`\ :math:`_{n}` : :token:`type` => :token:`term`”. If +:n:`fun {+ @ident__i } : @type => @term` +denotes the same function as :n:`{+ fun @ident__i : @type => } @term`. If a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section :ref:`let-in`). @@ -362,15 +359,14 @@ the propositional implication and function types. Applications ------------ -The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` denotes the -application of :token:`term`\ :math:`_0` to :token:`term`\ :math:`_1`. +The expression :n:`@term__fun @term` denotes the application of +:n:`@term__fun` (which is expected to have a function type) to +:token:`term`. -The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` ... -:token:`term`\ :math:`_n` denotes the application of the term -:token:`term`\ :math:`_0` to the arguments :token:`term`\ :math:`_1` ... then -:token:`term`\ :math:`_n`. It is equivalent to ( … ( :token:`term`\ :math:`_0` -:token:`term`\ :math:`_1` ) … ) :token:`term`\ :math:`_n` : associativity is to the -left. +The expression :n:`@term__fun {+ @term__i }` denotes the application +of the term :n:`@term__fun` to the arguments :n:`@term__i`. It is +equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`: +associativity is to the left. The notation :n:`(@ident := @term)` for arguments is used for making explicit the value of implicit arguments (see @@ -1624,6 +1620,17 @@ variety of commands: :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, :n:`@string__3` is the note. +``canonical`` + This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. + It is equivalent to having a :cmd:`Canonical Structure` declaration just + after the command. + + This attirbute can take the value ``false`` when decorating a record field + declaration with the effect of preventing the field from being involved in + the inference of canonical instances. + + See also :ref:`canonical-structure-declaration`. + .. example:: .. coqtop:: all reset warn diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d4a61425e1..ba43128bdc 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -253,6 +253,7 @@ and ``coqtop``, unless stated otherwise: :-h, --help: Print a short usage and exit. +.. _compiled-interfaces: Compiled interfaces (produced using ``-vos``) ---------------------------------------------- diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index dd80b29bda..b722b1af74 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -940,6 +940,13 @@ below will fail immediately and won't print anything. In any case, the value returned by the fully applied quotation is an unspecified dummy Ltac1 closure and should not be further used. +Switching between Ltac languages +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We recommend using the :opt:`Default Proof Mode` option to switch between tactic +languages with a proof-based granularity. This allows to incrementally port +the proof scripts. + Transition from Ltac1 --------------------- diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 6884b6e998..b1734b3f19 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -265,6 +265,35 @@ Name a set of section hypotheses for ``Proof using`` has remaining uninstantiated existential variables. It takes every uninstantiated existential variable and turns it into a goal. +Proof modes +``````````` + +When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, +|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes +shipped in the standard |Coq| installation, and furthermore some plugins define +their own proof modes. The default proof mode used when opening a proof can +be changed using the following option. + +.. opt:: Default Proof Mode @string + :name: Default Proof Mode + + Select the proof mode to use when starting a proof. Depending on the proof + mode, various syntactic constructs are allowed when writing an interactive + proof. The possible option values are listed below. + + - "Classic": this is the default. It activates the |Ltac| language to interact + with the proof, and also allows vernacular commands. + + - "Noedit": this proof mode only allows vernacular commands. No tactic + language is activated at all. This is the default when the prelude is not + loaded, e.g. through the `-noinit` option for `coqc`. + + - "Ltac2": this proof mode is made available when requiring the Ltac2 + library, and is set to be the default when it is imported. It allows + to use the Ltac2 language, as well as vernacular commands. + + - Some external plugins also define their own proof mode, which can be + activated via this command. Navigation in the proof tree -------------------------------- @@ -490,6 +519,13 @@ The following example script illustrates all these features: You just finished a goal focused by ``{``, you must unfocus it with ``}``. +Mandatory Bullets +````````````````` + +Using :opt:`Default Goal Selector` with the ``!`` selector forces +tactic scripts to keep focus to exactly one goal (e.g. using bullets) +or use explicit goal selectors. + Set Bullet Behavior ``````````````````` .. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 89b24ea8a3..a38c26c2b3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1200,7 +1200,7 @@ Controlling the locality of commands + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in - when no section contains them.For these commands, the Local modifier + when no section contains them. For these commands, the Local modifier limits the effect to the current section or module while the Global modifier extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b816ef6210..dbc3a42ee9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,12 +12,14 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOcamlChar.v plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOCamlFloats.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v plugins/extraction/ExtrOcamlString.v +plugins/extraction/ExtrOcamlNativeString.v plugins/extraction/ExtrOcamlZBigInt.v plugins/extraction/ExtrOcamlZInt.v plugins/extraction/Extraction.v diff --git a/doc/tools/coqrst/notations/fontsupport.py b/doc/tools/coqrst/notations/fontsupport.py index f0df7f1c01..c3ba2c1301 100755 --- a/doc/tools/coqrst/notations/fontsupport.py +++ b/doc/tools/coqrst/notations/fontsupport.py @@ -1,4 +1,5 @@ #!/usr/bin/env python2 +# -*- coding: utf-8 -*- ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## ## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## diff --git a/ide/coqide.ml b/ide/coqide.ml index fc30690544..918c196968 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -618,7 +618,7 @@ let printopts_callback opts v = let get_current_word term = (* First look to find if autocompleting *) - match term.script#complete_popup#proposal with + match term.script#proposal with | Some p -> p | None -> (* Then look at the current selected word *) diff --git a/ide/preferences.ml b/ide/preferences.ml index 4ee5669877..d3cf08e90e 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -388,6 +388,9 @@ let window_height = let auto_complete = new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool) +let auto_complete_delay = + new preference ~name:["auto_complete_delay"] ~init:250 ~repr:Repr.(int) + let stop_before = new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool) @@ -831,10 +834,26 @@ let configure ?(apply=(fun () -> ())) parent = let but = GButton.check_button ~label:text ~active ~packing:box#pack () in ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active)) in + let spin text ~min ~max (pref : int preference) = + let box = GPack.hbox ~packing:box#pack () in + let but = GEdit.spin_button + ~numeric:true ~update_policy:`IF_VALID ~digits:0 + ~packing:box#pack () + in + let _ = GMisc.label ~text:"Delay (ms)" ~packing:box#pack () in + let () = but#adjustment#set_bounds + ~lower:(float_of_int min) ~upper:(float_of_int max) + ~step_incr:1. + () + in + let () = but#set_value (float_of_int pref#get) in + ignore (but#connect#value_changed ~callback:(fun () -> pref#set but#value_as_int)) + in let () = button "Dynamic word wrap" dynamic_word_wrap in let () = button "Show line number" show_line_number in let () = button "Auto indentation" auto_indent in let () = button "Auto completion" auto_complete in + let () = spin "Auto completion delay" ~min:0 ~max:5000 auto_complete_delay in let () = button "Show spaces" show_spaces in let () = button "Show right margin" show_right_margin in let () = button "Show progress bar" show_progress_bar in diff --git a/ide/preferences.mli b/ide/preferences.mli index 4b04326cec..7b43079b4f 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -82,6 +82,7 @@ val show_toolbar : bool preference val window_width : int preference val window_height : int preference val auto_complete : bool preference +val auto_complete_delay : int preference val stop_before : bool preference val reset_on_tab_switch : bool preference val line_ending : line_ending preference diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index ac6712909e..396939cfcc 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -69,387 +69,101 @@ let is_substring s1 s2 = if !break then len2 - len1 else -1 -class type complete_model_signals = - object ('a) - method after : 'a - method disconnect : GtkSignal.id -> unit - method start_completion : callback:(int -> unit) -> GtkSignal.id - method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id - method end_completion : callback:(unit -> unit) -> GtkSignal.id - end - -let complete_model_signals - (start_s : int GUtil.signal) - (update_s : (int * string * Proposals.t) GUtil.signal) - (end_s : unit GUtil.signal) : complete_model_signals = -let signals = [ - start_s#disconnect; - update_s#disconnect; - end_s#disconnect; -] in -object (self : 'a) - inherit GUtil.ml_signals signals - method start_completion = start_s#connect ~after - method update_completion = update_s#connect ~after - method end_completion = end_s#connect ~after -end - -class complete_model coqtop (buffer : GText.buffer) = - let cols = new GTree.column_list in - let column = cols#add Gobject.Data.string in - let store = GTree.list_store cols in - let filtered_store = GTree.model_filter store in - let start_completion_signal = new GUtil.signal () in - let update_completion_signal = new GUtil.signal () in - let end_completion_signal = new GUtil.signal () in -object (self) - - val signals = complete_model_signals - start_completion_signal update_completion_signal end_completion_signal - val mutable active = false - val mutable auto_complete_length = 3 - (* this variable prevents CoqIDE from autocompleting when we have deleted something *) - val mutable is_auto_completing = false - (* this mutex ensure that CoqIDE will not try to autocomplete twice *) - val mutable cache = (-1, "", Proposals.empty) - val mutable insert_offset = -1 - val mutable current_completion = ("", Proposals.empty) - val mutable lock_auto_completing = true +class completion_provider coqtop = + let self_provider = ref None in + let active = ref true in + let provider = object (self) - method connect = signals + val mutable auto_complete_length = 3 + val mutable cache = (-1, "", Proposals.empty) + val mutable insert_offset = -1 - method active = active + method name = "" - method set_active b = active <- b + method icon = None - method private handle_insert iter s = - (* we're inserting, so we may autocomplete *) - is_auto_completing <- true + method private update_proposals pref = + let (_, _, props) = cache in + let filter prop = 0 <= is_substring pref prop in + let props = Proposals.filter filter props in + props - method private handle_delete ~start ~stop = - (* disable autocomplete *) - is_auto_completing <- false - - method store = filtered_store - - method column = column - - method handle_proposal path = - let row = filtered_store#get_iter path in - let proposal = filtered_store#get ~row ~column in - let (start_offset, _, _) = cache in - (* [iter] might be invalid now, get a new one to please gtk *) - let iter = buffer#get_iter `INSERT in - (* We cancel completion when the buffer has changed recently *) - if iter#offset = insert_offset then begin - let suffix = - let len1 = String.length proposal in - let len2 = insert_offset - start_offset in - String.sub proposal len2 (len1 - len2) + method private add_proposals ctx props = + let mk text = + let item = GSourceView3.source_completion_item ~text ~label:text () in + (item :> GSourceView3.source_completion_proposal) in - buffer#begin_user_action (); - ignore (buffer#insert_interactive ~iter suffix); - buffer#end_user_action (); - end - - method private init_proposals pref props = - let () = store#clear () in - let iter prop = - let iter = store#append () in - store#set ~row:iter ~column prop - in - let () = current_completion <- (pref, props) in - Proposals.iter iter props - - method private update_proposals pref = - let (_, _, props) = cache in - let filter prop = 0 <= is_substring pref prop in - let props = Proposals.filter filter props in - let () = current_completion <- (pref, props) in - let () = filtered_store#refilter () in - props - - method private do_auto_complete k = - let iter = buffer#get_iter `INSERT in - let () = insert_offset <- iter#offset in - let log = Printf.sprintf "Completion at offset: %i" insert_offset in - let () = Minilib.log log in - let prefix = - if Gtk_parsing.ends_word iter then - let start = Gtk_parsing.find_word_start iter in - let w = buffer#get_text ~start ~stop:iter () in - if String.length w >= auto_complete_length then Some (w, start) - else None - else None - in - match prefix with - | Some (w, start) -> + let props = List.map mk (Proposals.elements props) in + ctx#add_proposals (Option.get !self_provider) props true + + method populate ctx = + let iter = ctx#iter in + let buffer = new GText.buffer iter#buffer in + let start = Gtk_parsing.find_word_start iter in + let w = start#get_text ~stop:iter in let () = Minilib.log ("Completion of prefix: '" ^ w ^ "'") in let (off, prefix, props) = cache in let start_offset = start#offset in (* check whether we have the last request in cache *) if (start_offset = off) && (0 <= is_substring prefix w) then let props = self#update_proposals w in - let () = update_completion_signal#call (start_offset, w, props) in - k () + self#add_proposals ctx props else - let () = start_completion_signal#call start_offset in + let cancel = ref false in + let _ = ctx#connect#cancelled ~callback:(fun () -> cancel := true) in let update props = let () = cache <- (start_offset, w, props) in - let () = self#init_proposals w props in - update_completion_signal#call (start_offset, w, props) + if not !cancel then self#add_proposals ctx props in (* If not in the cache, we recompute it: first syntactic *) let synt = get_syntactic_completion buffer w Proposals.empty in (* Then semantic *) - let next prop = - let () = update prop in - Coq.lift k + let next props = + update props; + Coq.return () in let query = Coq.bind (get_semantic_completion w synt) next in (* If coqtop is computing, do the syntactic completion altogether *) - let occupied () = - let () = update synt in - k () - in + let occupied () = update synt in Coq.try_grab coqtop query occupied - | None -> end_completion_signal#call (); k () - - method private may_auto_complete () = - if active && is_auto_completing && lock_auto_completing then begin - let () = lock_auto_completing <- false in - let unlock () = lock_auto_completing <- true in - self#do_auto_complete unlock - end - - initializer - let filter_prop model row = - let (_, props) = current_completion in - let prop = store#get ~row ~column in - Proposals.mem prop props - in - let () = filtered_store#set_visible_func filter_prop in - (* Install auto-completion *) - ignore (buffer#connect#insert_text ~callback:self#handle_insert); - ignore (buffer#connect#delete_range ~callback:self#handle_delete); - ignore (buffer#connect#after#end_user_action ~callback:self#may_auto_complete); - -end - -class complete_popup (model : complete_model) (view : GText.view) = - let obj = GWindow.window ~kind:`POPUP ~show:false () in - let frame = GBin.scrolled_window - ~hpolicy:`NEVER ~vpolicy:`NEVER - ~shadow_type:`OUT ~packing:obj#add () - in -(* let frame = GBin.frame ~shadow_type:`OUT ~packing:obj#add () in *) - let data = GTree.view - ~vadjustment:frame#vadjustment ~hadjustment:frame#hadjustment - ~rules_hint:true ~headers_visible:false - ~model:model#store ~packing:frame#add () - in - let renderer = GTree.cell_renderer_text [], ["text", model#column] in - let col = GTree.view_column ~renderer () in - let _ = data#append_column col in - let () = col#set_sizing `AUTOSIZE in - let page_size = 16 in - -object (self) - - method coerce = view#coerce - - method private refresh_style () = - let (renderer, _) = renderer in - let font = Pango.Font.from_string Preferences.text_font#get in - renderer#set_properties [`FONT_DESC font; `XPAD 10] - - method private coordinates pos = - (* Toplevel position w.r.t. screen *) - let (x, y) = Gdk.Window.get_position view#misc#toplevel#misc#window in - (* Position of view w.r.t. window *) - let (ux, uy) = Gdk.Window.get_position view#misc#window in - (* Relative buffer position to view *) - let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in - (* Iter position *) - let iter = view#buffer#get_iter pos in - let coords = view#get_iter_location iter in - let lx = Gdk.Rectangle.x coords in - let ly = Gdk.Rectangle.y coords in - let w = Gdk.Rectangle.width coords in - let h = Gdk.Rectangle.height coords in - (* Absolute position *) - (x + lx + ux - dx, y + ly + uy - dy, w, h) - - method private select_any f = - let sel = data#selection#get_selected_rows in - let path = match sel with - | [] -> - begin match model#store#get_iter_first with - | None -> None - | Some iter -> Some (model#store#get_path iter) - end - | path :: _ -> Some path - in - match path with - | None -> () - | Some path -> - let path = f path in - let _ = data#selection#select_path path in - data#scroll_to_cell ~align:(0.,0.) path col - - method private select_previous () = - let prev path = - let copy = GTree.Path.copy path in - if GTree.Path.prev path then path - else copy - in - self#select_any prev - - method private select_next () = - let next path = - let () = GTree.Path.next path in - path - in - self#select_any next - method private select_previous_page () = - let rec up i path = - if i = 0 then path - else - let copy = GTree.Path.copy path in - let has_prev = GTree.Path.prev path in - if has_prev then up (pred i) path - else copy - in - self#select_any (up page_size) + method matched ctx = + if !active then + let iter = ctx#iter in + let () = insert_offset <- iter#offset in + let log = Printf.sprintf "Completion at offset: %i" insert_offset in + let () = Minilib.log log in + if Gtk_parsing.ends_word iter#backward_char then + let start = Gtk_parsing.find_word_start iter in + iter#offset - start#offset >= auto_complete_length + else false + else false - method private select_next_page () = - let rec down i path = - if i = 0 then path - else - let copy = GTree.Path.copy path in - let iter = model#store#get_iter path in - let has_next = model#store#iter_next iter in - if has_next then down (pred i) (model#store#get_path iter) - else copy - in - self#select_any (down page_size) + method activation = [`INTERACTIVE; `USER_REQUESTED] - method private select_first () = - let rec up path = - let copy = GTree.Path.copy path in - let has_prev = GTree.Path.prev path in - if has_prev then up path - else copy - in - self#select_any up + method info_widget proposal = None - method private select_last () = - let rec down path = - let copy = GTree.Path.copy path in - let iter = model#store#get_iter path in - let has_next = model#store#iter_next iter in - if has_next then down (model#store#get_path iter) - else copy - in - self#select_any down + method update_info proposal info = () - method private select_enter () = - let sel = data#selection#get_selected_rows in - match sel with - | [] -> () - | path :: _ -> - let () = model#handle_proposal path in - self#hide () + method start_iter ctx proposal iter = false - method proposal = - let sel = data#selection#get_selected_rows in - if obj#misc#visible then match sel with - | [] -> None - | path :: _ -> - let row = model#store#get_iter path in - let column = model#column in - let proposal = model#store#get ~row ~column in - Some proposal - else None + method activate_proposal proposal iter = false - method private manage_scrollbar () = - (* HACK: we don't have access to the treeview size because of the lack of - LablGTK binding for certain functions, so we bypass it by approximating - it through the size of the proposals *) - let height = match model#store#get_iter_first with - | None -> -1 - | Some iter -> - let path = model#store#get_path iter in - let area = data#get_cell_area ~path ~col () in - let height = Gdk.Rectangle.height area in - let height = page_size * height in - height - in - let len = ref 0 in - let () = model#store#foreach (fun _ _ -> incr len; false) in - if !len > page_size then - let () = frame#set_vpolicy `ALWAYS in - data#misc#set_size_request ~height () - else - data#misc#set_size_request ~height:(-1) () + method interactive_delay = (-1) - method private refresh () = - let () = frame#set_vpolicy `NEVER in - let () = self#select_first () in - let () = obj#misc#show () in - let () = self#manage_scrollbar () in - obj#resize ~width:1 ~height:1 + method priority = 0 - method private start_callback off = - let (x, y, w, h) = self#coordinates (`OFFSET off) in - let () = obj#move ~x ~y:(y + 3 * h / 2) in - () + end in + let provider = GSourceView3.source_completion_provider provider in + object (self) - method private update_callback (off, word, props) = - if Proposals.is_empty props then self#hide () - else if Proposals.mem word props then self#hide () - else self#refresh () + inherit GSourceView3.source_completion_provider provider#as_source_completion_provider - method private end_callback () = - obj#misc#hide () + method active = !active - method private hide () = self#end_callback () + method set_active b = active := b - initializer - let move_cb _ _ ~extend = self#hide () in - let key_cb ev = - let eval cb = cb (); true in - let ev_key = GdkEvent.Key.keyval ev in - if obj#misc#visible then - if ev_key = GdkKeysyms._Up then eval self#select_previous - else if ev_key = GdkKeysyms._Down then eval self#select_next - else if ev_key = GdkKeysyms._Tab then eval self#select_enter - else if ev_key = GdkKeysyms._Return then eval self#select_enter - else if ev_key = GdkKeysyms._Escape then eval self#hide - else if ev_key = GdkKeysyms._Page_Down then eval self#select_next_page - else if ev_key = GdkKeysyms._Page_Up then eval self#select_previous_page - else if ev_key = GdkKeysyms._Home then eval self#select_first - else if ev_key = GdkKeysyms._End then eval self#select_last - else false - else false - in - (* Style handling *) - let _ = view#misc#connect#style_set ~callback:self#refresh_style in - let _ = self#refresh_style () in - let _ = data#set_resize_mode `PARENT in - let _ = frame#set_resize_mode `PARENT in - (* Callback to model *) - let _ = model#connect#start_completion ~callback:self#start_callback in - let _ = model#connect#update_completion ~callback:self#update_callback in - let _ = model#connect#end_completion ~callback:self#end_callback in - (* Popup interaction *) - let _ = view#event#connect#key_press ~callback:key_cb in - (* Hiding the popup when necessary*) - let _ = view#misc#connect#hide ~callback:obj#misc#hide in - let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in - let _ = view#connect#move_cursor ~callback:move_cb in - let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in - () + initializer + self_provider := Some (self :> GSourceView3.source_completion_provider) -end + end diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli index ac9e6cd94f..020fe26cfb 100644 --- a/ide/wg_Completion.mli +++ b/ide/wg_Completion.mli @@ -10,27 +10,9 @@ module Proposals : sig type t end -class type complete_model_signals = - object ('a) - method after : 'a - method disconnect : GtkSignal.id -> unit - method start_completion : callback:(int -> unit) -> GtkSignal.id - method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id - method end_completion : callback:(unit -> unit) -> GtkSignal.id - end - -class complete_model : Coq.coqtop -> GText.buffer -> +class completion_provider : Coq.coqtop -> object + inherit GSourceView3.source_completion_provider method active : bool - method connect : complete_model_signals method set_active : bool -> unit - method store : GTree.model_filter - method column : string GTree.column - method handle_proposal : Gtk.tree_path -> unit -end - -class complete_popup : complete_model -> GText.view -> -object - method coerce : GObj.widget - method proposal : string option end diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 769ce61ee1..b7a35d7e94 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -287,18 +287,17 @@ end class script_view (tv : source_view) (ct : Coq.coqtop) = let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in -let completion = new Wg_Completion.complete_model ct view#buffer in -let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in +let provider = new Wg_Completion.completion_provider ct in object (self) inherit GSourceView3.source_view (Gobject.unsafe_cast tv) val undo_manager = new undo_manager view#buffer - method auto_complete = completion#active + method auto_complete = provider#active method set_auto_complete flag = - completion#set_active flag + provider#set_active flag method recenter_insert = self#scroll_to_mark @@ -448,7 +447,7 @@ object (self) self#buffer#delete_mark (`MARK insert_mark) - method complete_popup = popup + method proposal : string option = None (* FIXME *) method undo = undo_manager#undo method redo = undo_manager#redo @@ -527,10 +526,15 @@ object (self) stick spaces_instead_of_tabs self self#set_insert_spaces_instead_of_tabs; stick tab_length self self#set_tab_width; stick auto_complete self self#set_auto_complete; + stick auto_complete_delay self (fun d -> self#completion#set_auto_complete_delay d); let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in stick text_font self cb; + let () = self#completion#set_accelerators 0 in + let () = self#completion#set_show_headers false in + let _ = self#completion#add_provider (provider :> GSourceView3.source_completion_provider) in + () end diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index 91c8e758a5..4b6591e063 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -28,7 +28,7 @@ object method uncomment : unit -> unit method apply_unicode_binding : unit -> unit method recenter_insert : unit - method complete_popup : Wg_Completion.complete_popup + method proposal : string option end val script_view : Coq.coqtop -> diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index d9ccf81619..b19472dc99 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -197,16 +197,14 @@ let unbounded_from_below u cstrs = is u_k and is contributing. *) let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = let check_level l = - if Univ.LSet.mem l (Univ.ContextSet.levels uctx) && - unbounded_from_below l (Univ.ContextSet.constraints uctx) && - not (Univ.LSet.mem l ctor_levels) then - Some l - else None + Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + unbounded_from_below l (Univ.ContextSet.constraints uctx) && + not (Univ.LSet.mem l ctor_levels) in let univs = Univ.Universe.levels concl in let univs = if template_check then - Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs + Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs else univs (* Doesn't check the universes can be generalized *) in let fold acc = function diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 750ac86908..0d900c2ec9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -379,17 +379,25 @@ let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds = (************************************************************************) (* Build the inductive packet *) -let repair_arity indices = function - | RegularArity ar -> ar.mind_user_arity - | TemplateArity ar -> mkArity (indices,Sorts.sort_of_univ ar.template_level) +let fold_arity f acc params arity indices = match arity with + | RegularArity ar -> f acc ar.mind_user_arity + | TemplateArity _ -> + let fold_ctx acc ctx = + List.fold_left (fun acc d -> + Context.Rel.Declaration.fold_constr (fun c acc -> f acc c) d acc) + acc + ctx + in + fold_ctx (fold_ctx acc params) indices -let fold_inductive_blocks f = +let fold_inductive_blocks f acc params inds = Array.fold_left (fun acc ((arity,lc),(indices,_),_) -> - f (Array.fold_left f acc lc) (repair_arity indices arity)) + fold_arity f (Array.fold_left f acc lc) params arity indices) + acc inds -let used_section_variables env inds = +let used_section_variables env params inds = let fold l c = Id.Set.union (Environ.global_vars_set env c) l in - let ids = fold_inductive_blocks fold Id.Set.empty inds in + let ids = fold_inductive_blocks fold Id.Set.empty params inds in keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) @@ -461,7 +469,7 @@ let compute_projections (kn, i as ind) mib = let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) - let hyps = used_section_variables env inds in + let hyps = used_section_variables env paramsctxt inds in let nparamargs = Context.Rel.nhyps paramsctxt in (* Check one inductive *) let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg = @@ -479,18 +487,17 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in - let transf num = - let arity = List.length (dest_subterms recarg).(num) in - if Int.equal arity 0 then - let p = (!nconst, 0) in - incr nconst; p - else - let p = (!nblock + 1, arity) in - incr nblock; p - (* les tag des constructeur constant commence a 0, - les tag des constructeur non constant a 1 (0 => accumulator) *) + let transf arity = + if Int.equal arity 0 then + let p = (!nconst, 0) in + incr nconst; p + else + let p = (!nblock + 1, arity) in + incr nblock; p + (* les tag des constructeur constant commence a 0, + les tag des constructeur non constant a 1 (0 => accumulator) *) in - let rtbl = Array.init (List.length cnames) transf in + let rtbl = Array.map transf consnrealargs in (* Build the inductive packet *) { mind_typename = id; mind_arity = arity; diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1cef729916..a62b51e8aa 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -27,15 +27,35 @@ let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) let output_dir = ".coq-native" -(* Extension of genereted ml files, stored for debugging purposes *) +(* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" let ( / ) = Filename.concat -(* We have to delay evaluation of include_dirs because coqlib cannot be guessed -until flags have been properly initialized *) +(* Directory for temporary files for the conversion and normalisation + (as opposed to compiling the library itself, which uses [output_dir]). *) +let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "") + +let () = at_exit (fun () -> + if Lazy.is_val my_temp_dir then + try + let d = Lazy.force my_temp_dir in + Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d); + Unix.rmdir d + with e -> + Feedback.msg_warning + Pp.(str "Native compile: failed to cleanup: " ++ + str(Printexc.to_string e) ++ fnl())) + +(* We have to delay evaluation of include_dirs because coqlib cannot + be guessed until flags have been properly initialized. It also lets + us avoid forcing [my_temp_dir] if we don't need it (eg stdlib file + without native compute or native conv uses). *) let include_dirs () = - [Filename.get_temp_dir_name (); Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] + let base = [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] in + if Lazy.is_val my_temp_dir + then (Lazy.force my_temp_dir) :: base + else base (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun _x -> () : string -> unit) @@ -44,7 +64,8 @@ let rt1 = ref (dummy_value ()) let rt2 = ref (dummy_value ()) let get_ml_filename () = - let filename = Filename.temp_file "Coq_native" source_ext in + let temp_dir = Lazy.force my_temp_dir in + let filename = Filename.temp_file ~temp_dir "Coq_native" source_ext in let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in filename, prefix diff --git a/lib/future.ml b/lib/future.ml index d3ea538549..5cccd2038d 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -12,13 +12,13 @@ let not_ready_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ - "asynchronous script processing and don't pass \"-quick\" to "^ + "asynchronous script processing and don't pass \"-vio\" to "^ "coqc.")) let not_here_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not available "^ "in this process. If you really need this, pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ - "asynchronous script processing and don't pass \"-quick\" to "^ + "asynchronous script processing and don't pass \"-vio\" to "^ "coqc.")) let customize_not_ready_msg f = not_ready_msg := f diff --git a/plugins/extraction/ExtrOcamlChar.v b/plugins/extraction/ExtrOcamlChar.v new file mode 100644 index 0000000000..1e68365dd3 --- /dev/null +++ b/plugins/extraction/ExtrOcamlChar.v @@ -0,0 +1,45 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Extraction to Ocaml : extract ascii to OCaml's char type *) + +Require Coq.extraction.Extraction. + +Require Import Ascii String Coq.Strings.Byte. + +Extract Inductive ascii => char +[ +"(* If this appears, you're using Ascii internals. Please don't *) + (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> + let f b i = if b then 1 lsl i else 0 in + Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))" +] +"(* If this appears, you're using Ascii internals. Please don't *) + (fun f c -> + let n = Char.code c in + let h i = (n land (1 lsl i)) <> 0 in + f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". + +Extract Constant zero => "'\000'". +Extract Constant one => "'\001'". +Extract Constant shift => + "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". + +Extract Inlined Constant ascii_dec => "(=)". +Extract Inlined Constant Ascii.eqb => "(=)". + +(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) +Extract Inductive byte => char +["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. + +Extract Inlined Constant Byte.eqb => "(=)". +Extract Inlined Constant Byte.byte_eq_dec => "(=)". +Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)". +Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)". diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/plugins/extraction/ExtrOcamlNativeString.v new file mode 100644 index 0000000000..ec3da1e444 --- /dev/null +++ b/plugins/extraction/ExtrOcamlNativeString.v @@ -0,0 +1,87 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Extraction to Ocaml : extract ascii to OCaml's char type + and string to OCaml's string type. *) + +Require Coq.extraction.Extraction. + +Require Import Ascii String Coq.Strings.Byte. +Require Export ExtrOcamlChar. + +(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) +Extract Inductive byte => char +["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. + +Extract Inlined Constant Byte.eqb => "(=)". +Extract Inlined Constant Byte.byte_eq_dec => "(=)". +Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)". +Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)". + +(* This differs from ExtrOcamlString.v: the latter extracts "string" + to "char list", and we extract "string" to "string" *) + +Extract Inductive string => "string" +[ +(* EmptyString *) +"(* If this appears, you're using String internals. Please don't *) + """" +" +(* String *) +"(* If this appears, you're using String internals. Please don't *) + (fun (c, s) -> String.make 1 c ^ s) +" +] +"(* If this appears, you're using String internals. Please don't *) + (fun f0 f1 s -> + let l = String.length s in + if l = 0 then f0 else f1 (String.get s 0) (String.sub s 1 (l-1))) +". + +Extract Inlined Constant String.string_dec => "(=)". +Extract Inlined Constant String.eqb => "(=)". +Extract Inlined Constant String.append => "(^)". +Extract Inlined Constant String.concat => "String.concat". +Extract Inlined Constant String.prefix => + "(fun s1 s2 -> + let l1 = String.length s1 and l2 = String.length s2 in + l1 <= l2 && String.sub s2 0 l1 = s1)". +Extract Inlined Constant String.string_of_list_ascii => + "(fun l -> + let a = Array.of_list l in + String.init (Array.length a) (fun i -> a.(i)))". +Extract Inlined Constant String.list_ascii_of_string => + "(fun s -> + Array.to_list (Array.init (String.length s) (fun i -> s.[i])))". +Extract Inlined Constant String.string_of_list_byte => + "(fun l -> + let a = Array.of_list l in + String.init (Array.length a) (fun i -> a.(i)))". +Extract Inlined Constant String.list_byte_of_string => + "(fun s -> + Array.to_list (Array.init (String.length s) (fun i -> s.[i])))". + +(* Other operations in module String (at the time of this writing): + String.length + String.get + String.substring + String.index + String.findex + They all use type "nat". If we know that "nat" extracts + to O | S of nat, we can provide OCaml implementations + for these functions that work directly on OCaml's strings. + However "nat" could be extracted to other OCaml types... +*) + +(* +Definition test := "ceci est un test"%string. + +Recursive Extraction test Ascii.zero Ascii.one. +*) diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index 6265a67577..18c5ed3fe4 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -13,43 +13,6 @@ Require Coq.extraction.Extraction. Require Import Ascii String Coq.Strings.Byte. - -Extract Inductive ascii => char -[ -"(* If this appears, you're using Ascii internals. Please don't *) - (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> - let f b i = if b then 1 lsl i else 0 in - Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))" -] -"(* If this appears, you're using Ascii internals. Please don't *) - (fun f c -> - let n = Char.code c in - let h i = (n land (1 lsl i)) <> 0 in - f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". - -Extract Constant zero => "'\000'". -Extract Constant one => "'\001'". -Extract Constant shift => - "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". - -Extract Inlined Constant ascii_dec => "(=)". -Extract Inlined Constant Ascii.eqb => "(=)". +Require Export ExtrOcamlChar. Extract Inductive string => "char list" [ "[]" "(::)" ]. - -(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) -Extract Inductive byte => char -["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. - -Extract Inlined Constant Byte.eqb => "(=)". -Extract Inlined Constant Byte.byte_eq_dec => "(=)". -Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)". -Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)". - -(* -Definition test := "ceci est un test"%string. -Definition test2 := List.map (option_map Byte.to_nat) (List.map Byte.of_nat (List.seq 0 256)). -Definition test3 := List.map ascii_of_nat (List.seq 0 256). - -Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect. -*) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 2f3f42c5f6..29da12de40 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -14,7 +14,6 @@ open Names open ModPath open Namegen open Nameops -open Libnames open Table open Miniml open Mlutil @@ -616,10 +615,15 @@ let pp_module mp = [Extract Inductive ascii => char] has been declared, then the constants are directly turned into chars *) -let mk_ind path s = - MutInd.make2 (MPfile (dirpath_of_string path)) (Label.make s) +let ascii_type_name = "core.ascii.type" +let ascii_constructor_name = "core.ascii.ascii" -let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" +let is_ascii_registered () = + Coqlib.has_ref ascii_type_name + && Coqlib.has_ref ascii_constructor_name + +let ascii_type_ref () = Coqlib.lib_ref ascii_type_name +let ascii_constructor_ref () = Coqlib.lib_ref ascii_constructor_name let check_extract_ascii () = try @@ -628,15 +632,18 @@ let check_extract_ascii () = | Haskell -> "Prelude.Char" | _ -> raise Not_found in - String.equal (find_custom (GlobRef.IndRef (ind_ascii, 0))) (char_type) + String.equal (find_custom @@ ascii_type_ref ()) (char_type) with Not_found -> false let is_list_cons l = List.for_all (function MLcons (_,GlobRef.ConstructRef(_,_),[]) -> true | _ -> false) l let is_native_char = function - | MLcons(_,GlobRef.ConstructRef ((kn,0),1),l) -> - MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l + | MLcons(_,gr,l) -> + is_ascii_registered () + && GlobRef.equal gr (ascii_constructor_ref ()) + && check_extract_ascii () + && is_list_cons l | _ -> false let get_native_char c = @@ -649,3 +656,84 @@ let get_native_char c = Char.chr (cumul l) let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'") + +(** Special hack for constants of type String.string : if an + [Extract Inductive string => string] has been declared, then + the constants are directly turned into string literals *) + +let string_type_name = "core.string.type" +let empty_string_name = "core.string.empty" +let string_constructor_name = "core.string.string" + +let is_string_registered () = + Coqlib.has_ref string_type_name + && Coqlib.has_ref empty_string_name + && Coqlib.has_ref string_constructor_name + +let string_type_ref () = Coqlib.lib_ref string_type_name +let empty_string_ref () = Coqlib.lib_ref empty_string_name +let string_constructor_ref () = Coqlib.lib_ref string_constructor_name + +let check_extract_string () = + try + let string_type = match lang () with + | Ocaml -> "string" + | Haskell -> "Prelude.String" + | _ -> raise Not_found + in + String.equal (find_custom @@ string_type_ref ()) string_type + with Not_found -> false + +(* The argument is known to be of type Coq.Strings.String.string. + Check that it is built from constructors EmptyString and String + with constant ascii arguments. *) + +let rec is_native_string_rec empty_string_ref string_constructor_ref = function + (* "EmptyString" constructor *) + | MLcons(_, gr, []) -> GlobRef.equal gr empty_string_ref + (* "String" constructor *) + | MLcons(_, gr, [hd; tl]) -> + GlobRef.equal gr string_constructor_ref + && is_native_char hd + && is_native_string_rec empty_string_ref string_constructor_ref tl + (* others *) + | _ -> false + +(* Here we first check that the argument is the type registered as + core.string.type and that extraction to native strings was + requested. Then we check every character via + [is_native_string_rec]. *) + +let is_native_string c = + match c with + | MLcons(_, GlobRef.ConstructRef(ind, j), l) -> + is_string_registered () + && GlobRef.equal (GlobRef.IndRef ind) (string_type_ref ()) + && check_extract_string () + && is_native_string_rec (empty_string_ref ()) (string_constructor_ref ()) c + | _ -> false + +(* Extract the underlying string. *) + +let get_native_string c = + let buf = Buffer.create 64 in + let rec get = function + (* "EmptyString" constructor *) + | MLcons(_, gr, []) when GlobRef.equal gr (empty_string_ref ()) -> + Buffer.contents buf + (* "String" constructor *) + | MLcons(_, gr, [hd; tl]) when GlobRef.equal gr (string_constructor_ref ()) -> + Buffer.add_char buf (get_native_char hd); + get tl + (* others *) + | _ -> assert false + in get c + +(* Printing the underlying string. *) + +let pp_native_string c = + str ("\"" ^ String.escaped (get_native_string c) ^ "\"") + +(* Registered sig type *) + +let sig_type_ref () = Coqlib.lib_ref "core.sig.type" diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index e4e9c4c527..9dbc09dd06 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -70,10 +70,6 @@ val reset_renaming_tables : reset_kind -> unit val set_keywords : Id.Set.t -> unit -(** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *) - -val mk_ind : string -> string -> MutInd.t - (** Special hack for constants of type Ascii.ascii : if an [Extract Inductive ascii => char] has been declared, then the constants are directly turned into chars *) @@ -81,3 +77,14 @@ val mk_ind : string -> string -> MutInd.t val is_native_char : ml_ast -> bool val get_native_char : ml_ast -> char val pp_native_char : ml_ast -> Pp.t + +(** Special hack for constants of type String.string : if an + [Extract Inductive string => string] has been declared, then + the constants are directly turned into string literals *) + +val is_native_string : ml_ast -> bool +val get_native_string : ml_ast -> string +val pp_native_string : ml_ast -> Pp.t + +(* Registered sig type *) +val sig_type_ref : unit -> GlobRef.t diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index f0053ba6b5..eef050efbd 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -109,8 +109,8 @@ let rec pp_type par vl t = (try Id.print (List.nth vl (pred i)) with Failure _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r - | Tglob (GlobRef.IndRef(kn,0),l) - when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> + | Tglob (gr,l) + when not (keep_singleton ()) && GlobRef.equal gr (sig_type_ref ()) -> pp_type true vl (List.hd l) | Tglob (r,l) -> pp_par par @@ -171,6 +171,7 @@ let rec pp_expr par env args = assert (List.is_empty args); begin match a with | _ when is_native_char c -> pp_native_char c + | _ when is_native_string c -> pp_native_string c | [] -> pp_global Cons r | [a] -> pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 66429833b9..97cad87825 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -165,8 +165,8 @@ let pp_type par vl t = | Tglob (r,[a1;a2]) when is_infix r -> pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) | Tglob (r,[]) -> pp_global Type r - | Tglob (GlobRef.IndRef(kn,0),l) - when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> + | Tglob (gr,l) + when not (keep_singleton ()) && GlobRef.equal gr (sig_type_ref ()) -> pp_tuple_light pp_rec l | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r @@ -249,6 +249,7 @@ let rec pp_expr par env args = assert (List.is_empty args); begin match a with | _ when is_native_char c -> pp_native_char c + | _ when is_native_string c -> pp_native_string c | [a1;a2] when is_infix r -> let pp = pp_expr true env [] in pp_par par (pp a1 ++ str (get_infix r) ++ pp a2) diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v index 785a53fafa..18cd196148 100644 --- a/plugins/micromega/Zify.v +++ b/plugins/micromega/Zify.v @@ -87,4 +87,4 @@ Ltac applySpec S := (** [zify_post_hook] is there to be redefined. *) Ltac zify_post_hook := idtac. -Ltac zify := zify_op ; (iter_specs applySpec) ; zify_post_hook. +Ltac zify := zify_op ; (zify_iter_specs applySpec) ; zify_post_hook. diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 66f263c0b1..2b5fac32a2 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -34,12 +34,13 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF END TACTIC EXTEND ITER -| [ "iter_specs" tactic(t)] -> { Zify.iter_specs t } +| [ "zify_iter_specs" tactic(t)] -> { Zify.iter_specs t } END TACTIC EXTEND TRANS | [ "zify_op" ] -> { Zify.zify_tac } -| [ "saturate" ] -> { Zify.saturate } +| [ "zify_saturate" ] -> { Zify.saturate } +| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t } END VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 5d8ae83853..e71c89b4db 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -965,6 +965,43 @@ let trans_concl t = let tclTHENOpt e tac tac' = match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac' +let assert_inj t = + init_cache (); + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + try + ignore (get_injection env evd t); + Tacticals.New.tclIDTAC + with Not_found -> + Tacticals.New.tclFAIL 0 (Pp.str " InjTyp does not exist")) + +let do_let tac (h : Constr.named_declaration) = + match h with + | Context.Named.Declaration.LocalAssum _ -> Tacticals.New.tclIDTAC + | Context.Named.Declaration.LocalDef (id, t, ty) -> + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + try + ignore (get_injection env evd (EConstr.of_constr ty)); + tac id.Context.binder_name t ty + with Not_found -> Tacticals.New.tclIDTAC) + +let iter_let tac = + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let sign = Environ.named_context env in + Tacticals.New.tclMAP (do_let tac) sign) + +let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) = + init_cache (); + iter_let (fun (id : Names.Id.t) (t : Constr.types) (ty : Constr.types) -> + Ltac_plugin.Tacinterp.Value.apply tac + [ Ltac_plugin.Tacinterp.Value.of_constr (EConstr.mkVar id) + ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr t) + ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr ty) ]) + let zify_tac = Proofview.Goal.enter (fun gl -> Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"]; diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index 9e3cf5d24c..4930a845c9 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -27,3 +27,5 @@ module Saturate : S val zify_tac : unit Proofview.tactic val saturate : unit Proofview.tactic val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic +val assert_inj : EConstr.constr -> unit Proofview.tactic +val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index f5d53cbbf3..34533670f8 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -573,27 +573,16 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. Require Import ZifyClasses ZifyInst. Require Zify. - -(** [is_inj T] returns true iff the type T has an injection *) -Ltac is_inj T := - match T with - | _ => let x := constr:(_ : InjTyp T _ ) in true - | _ => false - end. - (* [elim_let] replaces a let binding (x := e : t) by an equation (x = e) if t is an injected type *) -Ltac elim_let := - repeat - match goal with - | x := ?t : ?ty |- _ => - let b := is_inj ty in - match b with - | true => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - end - end. +Ltac elim_binding x t ty := + let h := fresh "heq_" x in + pose proof (@eq_refl ty x : @eq ty x t) as h; + try clearbody x. + +Ltac elim_let := zify_iter_let elim_binding. Ltac zify := intros ; elim_let ; - Zify.zify ; ZifyInst.saturate. + Zify.zify ; ZifyInst.zify_saturate. diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aa6ec1c941..cbd04a76ad 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -436,7 +436,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = | exception Evarconv.UnableToUnify _ -> sigma, current | sigma -> sigma, current else - let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in + let sigma, j, _trace = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val in sigma, (current, try_find_ind !!(pb.env) sigma indt names)) @@ -1955,8 +1955,12 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon = match tycon with - | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma - ~flags:(default_flags_of TransparentState.full) j p + | Some p -> + let (evd,v,_trace) = + Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma + ~flags:(default_flags_of TransparentState.full) j p + in + (evd,v) | None -> sigma, j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c980d204ca..3c7f9a8f00 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -136,20 +136,6 @@ let lift_args n sign = in liftrec (List.length sign) sign -let mu env evdref t = - let rec aux v = - let v' = hnf env !evdref v in - match disc_subset !evdref v' with - | Some (u, p) -> - let f, ct = aux u in - let p = hnf_nodelta env !evdref p in - (Some (fun x -> - app_opt env evdref - f (papp evdref sig_proj1 [| u; p; x |])), - ct) - | None -> (None, v) - in aux t - let coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) : (EConstr.constr -> EConstr.constr) option = @@ -367,36 +353,97 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd +type coercion_trace = + | IdCoe + | PrimProjCoe of { + proj : Projection.Repr.t; + args : econstr list; + previous : coercion_trace; + } + | Coe of { + head : econstr; + args : econstr list; + previous : coercion_trace; + } + | ProdCoe of { na : Name.t binder_annot; ty : econstr; dom : coercion_trace; body : coercion_trace } + +let empty_coercion_trace = IdCoe + +(* similar to iterated apply_coercion_args *) +let rec reapply_coercions sigma trace c = match trace with + | IdCoe -> c + | PrimProjCoe { proj; args; previous } -> + let c = reapply_coercions sigma previous c in + let args = args@[c] in + let head, args = match args with [] -> assert false | hd :: tl -> hd, tl in + applist (mkProj (Projection.make proj false, head), args) + | Coe {head; args; previous} -> + let c = reapply_coercions sigma previous c in + let args = args@[c] in + applist (head, args) + | ProdCoe { na; ty; dom; body } -> + let x = reapply_coercions sigma dom (mkRel 1) in + let c = beta_applist sigma (lift 1 c, [x]) in + let c = reapply_coercions sigma body c in + mkLambda (na, ty, c) + (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = - let j,t,evd = + let j,t,trace,evd = List.fold_left - (fun (ja,typ_cl,sigma) i -> + (fun (ja,typ_cl,trace,sigma) i -> let isid = i.coe_is_identity in let isproj = i.coe_is_projection in let sigma, c = new_global sigma i.coe_value in let typ = Retyping.get_type_of env sigma c in let fv = make_judge c typ in - let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in - let sigma, jres = - apply_coercion_args env sigma true isproj argl fv + let argl = class_args_of env sigma typ_cl in + let trace = + if isid then trace + else match isproj with + | None -> Coe {head=fv.uj_val;args=argl;previous=trace} + | Some proj -> + let args = List.skipn (Projection.Repr.npars proj) argl in + PrimProjCoe {proj; args; previous=trace } in - (if isid then + let argl = argl@[ja.uj_val] in + let sigma, jres = apply_coercion_args env sigma true isproj argl fv in + let jres = + if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } else - jres), - jres.uj_type,sigma) - (hj,typ_cl,sigma) p - in evd, j + jres + in + jres, jres.uj_type, trace, sigma) + (hj,typ_cl,IdCoe,sigma) p + in evd, j, trace + +let mu env evdref t = + let rec aux v = + let v' = hnf env !evdref v in + match disc_subset !evdref v' with + | Some (u, p) -> + let f, ct, trace = aux u in + let p = hnf_nodelta env !evdref p in + let p1 = delayed_force sig_proj1 in + let evd, p1 = Evarutil.new_global !evdref p1 in + evdref := evd; + (Some (fun x -> + app_opt env evdref + f (mkApp (p1, [| u; p; x |]))), + ct, + Coe {head=p1; args=[u;p]; previous=trace}) + | None -> (None, v, IdCoe) + in aux t (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core ~program_mode env evd j = let t = whd_all env evd j.uj_type in match EConstr.kind evd t with - | Prod _ -> (evd,j) + | Prod _ -> (evd,j,IdCoe) | Evar ev -> let (evd',t) = Evardefine.define_evar_as_product env evd ev in - (evd',{ uj_val = j.uj_val; uj_type = t }) + (evd',{ uj_val = j.uj_val; uj_type = t },IdCoe) | _ -> try let t,p = lookup_path_to_fun_from env evd j.uj_type in @@ -405,11 +452,11 @@ let inh_app_fun_core ~program_mode env evd j = if program_mode then try let evdref = ref evd in - let coercef, t = mu env evdref t in + let coercef, t, trace = mu env evdref t in let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in - (!evdref, res) + (!evdref, res, trace) with NoSubtacCoercion | NoCoercion -> - (evd,j) + (evd,j,IdCoe) else raise NoCoercion (* Try to coerce to a funclass; returns [j] if no coercion is applicable *) @@ -417,10 +464,10 @@ let inh_app_fun ~program_mode resolve_tc env evd j = try inh_app_fun_core ~program_mode env evd j with | NoCoercion when not resolve_tc - || not (get_use_typeclasses_for_conversion ()) -> (evd, j) + || not (get_use_typeclasses_for_conversion ()) -> (evd, j, IdCoe) | NoCoercion -> try inh_app_fun_core ~program_mode env (saturate_evd env evd) j - with NoCoercion -> (evd, j) + with NoCoercion -> (evd, j, IdCoe) let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with @@ -430,7 +477,7 @@ let type_judgment env sigma j = let inh_tosort_force ?loc env evd j = try let t,p = lookup_path_to_sort_from env evd j.uj_type in - let evd,j1 = apply_coercion env evd p j t in + let evd,j1,_trace = apply_coercion env evd p j t in let j2 = Environ.on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env evd j2) with Not_found | NoCoercion -> @@ -449,7 +496,7 @@ let inh_coerce_to_sort ?loc env evd j = let inh_coerce_to_base ?loc ~program_mode env evd j = if program_mode then let evdref = ref evd in - let ct, typ' = mu env evdref j.uj_type in + let ct, typ', trace = mu env evdref j.uj_type in let res = { uj_val = (app_coercion env evdref ct j.uj_val); uj_type = typ' } @@ -459,7 +506,7 @@ let inh_coerce_to_base ?loc ~program_mode env evd j = let inh_coerce_to_prod ?loc ~program_mode env evd t = if program_mode then let evdref = ref evd in - let _, typ' = mu env evdref t in + let _, typ', _trace = mu env evdref t in !evdref, typ' else (evd, t) @@ -468,24 +515,24 @@ let inh_coerce_to_fail flags env evd rigidonly v t c1 = then raise NoCoercion else - let evd, v', t' = + let evd, v', t', trace = try let t2,t1,p = lookup_path_between env evd (t,c1) in - let evd,j = + let evd,j,trace = apply_coercion env evd p {uj_val = v; uj_type = t} t2 in - evd, j.uj_val, j.uj_type + evd, j.uj_val, j.uj_type, trace with Not_found -> raise NoCoercion in - try (unify_leq_delay ~flags env evd t' c1, v') + try (unify_leq_delay ~flags env evd t' c1, v', trace) with UnableToUnify _ -> raise NoCoercion let default_flags_of env = default_flags_of TransparentState.full let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 = - try (unify_leq_delay ~flags env evd t c1, v) + try (unify_leq_delay ~flags env evd t c1, v, IdCoe) with UnableToUnify (best_failed_evd,e) -> try inh_coerce_to_fail flags env evd rigidonly v t c1 with NoCoercion -> @@ -505,24 +552,27 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid | na -> na) name in let open Context.Rel.Declaration in let env1 = push_rel (LocalAssum (name,u1)) env in - let (evd', v1) = + let (evd', v1, trace1) = inh_conv_coerce_to_fail ?loc env1 evd rigidonly (mkRel 1) (lift 1 u1) (lift 1 t1) in let v2 = beta_applist evd' (lift 1 v,[v1]) in let t2 = Retyping.get_type_of env1 evd' v2 in - let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in - (evd'', mkLambda (name, u1, v2')) + let (evd'',v2',trace2) = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in + let trace = ProdCoe { na=name; ty=u1; dom=trace1; body=trace2 } in + (evd'', mkLambda (name, u1, v2'), trace) | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t = - let (evd', val') = + let (evd', val', otrace) = try - inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t + let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t in + (evd', val', Some trace) with NoCoercionNoUnifier (best_failed_evd,e) -> try if program_mode then - coerce_itf ?loc env evd cj.uj_val cj.uj_type t + let (evd', val') = coerce_itf ?loc env evd cj.uj_val cj.uj_type t in + (evd', val', None) else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) -> @@ -533,11 +583,12 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd if evd' == evd then error_actual_type ?loc env best_failed_evd cj t e else - inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t + let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t in + (evd', val', Some trace) with NoCoercionNoUnifier (_evd,_error) -> error_actual_type ?loc env best_failed_evd cj t e in - (evd',{ uj_val = val'; uj_type = t }) + (evd',{ uj_val = val'; uj_type = t },otrace) let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index fe93a26f4f..b92f3709cc 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -16,13 +16,19 @@ open Glob_term (** {6 Coercions. } *) +type coercion_trace + +val empty_coercion_trace : coercion_trace + +val reapply_coercions : evar_map -> coercion_trace -> EConstr.t -> EConstr.t + (** [inh_app_fun resolve_tc env isevars j] coerces [j] to a function; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a product; it returns [j] if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing) *) val inh_app_fun : program_mode:bool -> bool -> - env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment * coercion_trace (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as @@ -48,11 +54,11 @@ val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool -> val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool -> env -> evar_map -> ?flags:Evarconv.unify_flags -> - unsafe_judgment -> types -> evar_map * unsafe_judgment + unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool -> env -> evar_map -> ?flags:Evarconv.unify_flags -> - unsafe_judgment -> types -> evar_map * unsafe_judgment + unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bfdb471c46..bf61d44a10 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -361,7 +361,7 @@ let adjust_evar_source sigma na c = (* coerce to tycon if any *) let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = function - | None -> sigma, j + | None -> sigma, j, Some Coercion.empty_coercion_trace | Some t -> Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t @@ -604,16 +604,18 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk module Default = struct + let discard_trace (sigma,t,otrace) = sigma, t + let pretype_ref self (ref, u) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let sigma, t_ref = pretype_ref ?loc sigma env ref u in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon let pretype_var self id = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let pretype tycon env sigma t = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t in let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma = (* Ne faudrait-il pas s'assurer que hyps est bien un @@ -626,7 +628,7 @@ struct let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in let c = mkEvar (evk, args) in let j = Retyping.get_judgment_of !!env sigma c in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma = let sigma, ty = @@ -757,12 +759,12 @@ struct iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon let pretype_sort self s = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let sigma, j = pretype_sort ?loc sigma s in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon let pretype_app self (f, args) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -771,12 +773,15 @@ struct let floc = loc_of_glob_constr f in let length = List.length args in let nargs_before_bidi = + if Option.is_empty tycon then length + (* We apply bidirectionality hints only if an expected type is specified *) + else (* if `f` is a global, we retrieve bidirectionality hints *) - try - let (gr,_) = destRef sigma fj.uj_val in - Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints - with DestKO -> - length + try + let (gr,_) = destRef sigma fj.uj_val in + Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints + with DestKO -> + length in let candargs = (* Bidirectional typechecking hint: @@ -813,24 +818,38 @@ struct else fun f v -> applist (f, [v]) | _ -> fun _ f v -> applist (f, [v]) in - let rec apply_rec env sigma n resj candargs bidiargs = function - | [] -> sigma, resj, List.rev bidiargs + let refresh_template env sigma resj = + (* Special case for inductive type applications that must be + refreshed right away. *) + match EConstr.kind sigma resj.uj_val with + | App (f,args) -> + if Termops.is_template_polymorphic_ind !!env sigma f then + let c = mkApp (f, args) in + let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in + let t = Retyping.get_type_of !!env sigma c in + sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t + else sigma, resj + | _ -> sigma, resj + in + let rec apply_rec env sigma n resj resj_before_bidi candargs bidiargs = function + | [] -> sigma, resj, resj_before_bidi, List.rev bidiargs | c::rest -> let bidi = n >= nargs_before_bidi in let argloc = loc_of_glob_constr c in - let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in + let sigma, resj, trace = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in let resty = whd_all !!env sigma resj.uj_type in match EConstr.kind sigma resty with | Prod (na,c1,c2) -> - let tycon = Some c1 in let (sigma, hj), bidiargs = - if bidi && Option.has_some tycon then + if bidi then (* We want to get some typing information from the context before typing the argument, so we replace it by an existential variable *) let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in - (sigma, make_judge c_hole c1), (c_hole, c) :: bidiargs - else pretype tycon env sigma c, bidiargs + (sigma, make_judge c_hole c1), (c_hole, c, trace) :: bidiargs + else + let tycon = Some c1 in + pretype tycon env sigma c, bidiargs in let sigma, candargs, ujval = match candargs with @@ -845,29 +864,18 @@ struct in let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in - let j = { uj_val = value; uj_type = typ } in - apply_rec env sigma (n+1) j candargs bidiargs rest + let resj = { uj_val = value; uj_type = typ } in + let resj_before_bidi = if bidi then resj_before_bidi else resj in + apply_rec env sigma (n+1) resj resj_before_bidi candargs bidiargs rest | _ -> let sigma, hj = pretype empty_tycon env sigma c in error_cant_apply_not_functional ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] in - let sigma, resj, bidiargs = apply_rec env sigma 0 fj candargs [] args in - let sigma, resj = - match EConstr.kind sigma resj.uj_val with - | App (f,args) -> - if Termops.is_template_polymorphic_ind !!env sigma f then - (* Special case for inductive type applications that must be - refreshed right away. *) - let c = mkApp (f, args) in - let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in - let t = Retyping.get_type_of !!env sigma c in - sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t - else sigma, resj - | _ -> sigma, resj - in - let sigma, t = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in - let refine_arg sigma (newarg,origarg) = + let sigma, resj, resj_before_bidi, bidiargs = apply_rec env sigma 0 fj fj candargs [] args in + let sigma, resj = refresh_template env sigma resj in + let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in + let refine_arg n (sigma,t) (newarg,origarg,trace) = (* Refine an argument (originally `origarg`) represented by an evar (`newarg`) to use typing information from the context *) (* Recover the expected type of the argument *) @@ -876,12 +884,25 @@ struct let sigma, j = pretype (Some ty) env sigma origarg in (* Unify the (possibly refined) existential variable with the (typechecked) original value *) - Evarconv.unify_delay !!env sigma newarg (j_val j) + let sigma = Evarconv.unify_delay !!env sigma newarg (j_val j) in + sigma, app_f n (Coercion.reapply_coercions sigma trace t) (j_val j) in (* We now refine any arguments whose typing was delayed for bidirectionality *) - let sigma = List.fold_left refine_arg sigma bidiargs in - (sigma, t) + let t = resj_before_bidi.uj_val in + let sigma, t = List.fold_left_i refine_arg nargs_before_bidi (sigma,t) bidiargs in + (* If we did not get a coercion trace (e.g. with `Program` coercions, we + replaced user-provided arguments with inferred ones. Otherwise, we apply + the coercion trace to the user-provided arguments. *) + let resj = + match otrace with + | None -> resj + | Some trace -> + let resj = { resj with uj_val = t } in + let sigma, resj = refresh_template env sigma resj in + { resj with uj_val = Coercion.reapply_coercions sigma trace t } + in + (sigma, resj) let pretype_lambda self (name, bk, c1, c2) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -903,7 +924,7 @@ struct let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in let name = get_name var' in let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_prod self (name, bk, c1, c2) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -929,7 +950,7 @@ struct let (e, info) = CErrors.push e in let info = Option.cata (Loc.add_loc info) info loc in iraise (e, info) in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_letin self (name, c1, t, c2) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1122,7 +1143,7 @@ struct mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon let pretype_cast self (c, k) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1165,7 +1186,7 @@ struct in let v = mkCast (cj.uj_val, k, tval) in sigma, { uj_val = v; uj_type = tval } - in inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon + in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon let pretype_int self i = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1174,7 +1195,7 @@ struct with Invalid_argument _ -> user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.") in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_float self f = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1183,7 +1204,7 @@ struct with Invalid_argument _ -> user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.") in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon (* [pretype_type valcon env sigma c] coerces [c] into a type *) let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma = match DAst.get c with diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 35e182840b..3b918b5396 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -19,7 +19,6 @@ open CErrors open Util open Pp open Names -open Globnames open Constr open Mod_subst open Reductionops @@ -80,7 +79,7 @@ let subst_structure subst (id, kl, projs as obj) = (Option.Smart.map (subst_constant subst)) projs in - let id' = subst_constructor subst id in + let id' = Globnames.subst_constructor subst id in if projs' == projs && id' == id then obj else (id',kl,projs') @@ -139,7 +138,7 @@ let find_primitive_projection c = *) type obj_typ = { - o_ORIGIN : Constant.t; + o_ORIGIN : GlobRef.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) @@ -190,13 +189,13 @@ let rec cs_pattern_of_constr env t = let _, params = Inductive.find_rectype env ty in Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (Sorts.family s), None, [] - | _ -> Const_cs (global_of_constr t) , None, [] + | _ -> Const_cs (Globnames.global_of_constr t) , None, [] let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (sign,env,t,con,proji_sp) -> + (fun (sign,env,t,ref,proji_sp) -> let env = Termops.push_rels_assum sign env in - let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in + let con_pp = Nametab.pr_global_env Id.Set.empty ref in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " @@ -204,11 +203,17 @@ let warn_projection_no_head_constant = ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) -let compute_canonical_projections env ~warn (con,ind) = - let o_CTX = Environ.constant_context env con in - let u = Univ.make_abstract_instance o_CTX in - let o_DEF = mkConstU (con, u) in - let c = Environ.constant_value_in env (con,u) in +let compute_canonical_projections env ~warn (gref,ind) = + let o_CTX = Environ.universes_of_global env gref in + let o_DEF, c = + match gref with + | GlobRef.ConstRef con -> + let u = Univ.make_abstract_instance o_CTX in + mkConstU (con, u), Environ.constant_value_in env (con,u) + | GlobRef.VarRef id -> + mkVar id, Option.get (Environ.named_body id env) + | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false + in let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in @@ -227,10 +232,10 @@ let compute_canonical_projections env ~warn (con,ind) = match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> ((GlobRef.ConstRef proji_sp, (patt, t)), - { o_ORIGIN = con ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) + { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc | exception Not_found -> - if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp); + if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp); acc ) acc spopt else acc @@ -266,12 +271,17 @@ let register_canonical_structure ~warn env sigma o = warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s) ) -let subst_canonical_structure subst (cst,ind as obj) = +type cs = GlobRef.t * inductive + +let subst_canonical_structure subst (gref,ind as obj) = (* invariant: cst is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - let cst' = subst_constant subst cst in - let ind' = subst_ind subst ind in - if cst' == cst && ind' == ind then obj else (cst',ind') + match gref with + | GlobRef.ConstRef cst -> + let cst' = subst_constant subst cst in + let ind' = subst_ind subst ind in + if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind') + | _ -> assert false (*s High-level declaration of a canonical structure *) @@ -282,15 +292,20 @@ let error_not_structure ref description = description)) let check_and_decompose_canonical_structure env sigma ref = - let sp = + let vc = match ref with - GlobRef.ConstRef sp -> sp - | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") + | GlobRef.ConstRef sp -> + let u = Univ.make_abstract_instance (Environ.constant_context env sp) in + begin match Environ.constant_opt_value_in env (sp, u) with + | Some vc -> vc + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | GlobRef.VarRef id -> + begin match Environ.named_body id env with + | Some b -> b + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> + error_not_structure ref (str "Expected an instance of a record or structure.") in - let u = Univ.make_abstract_instance (Environ.constant_context env sp) in - let vc = match Environ.constant_opt_value_in env (sp, u) with - | Some vc -> vc - | None -> error_not_structure ref (str "Could not find its value in the global environment.") in let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with @@ -308,7 +323,7 @@ let check_and_decompose_canonical_structure env sigma ref = let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref (str "Got too few arguments to the record or structure constructor."); - (sp,indsp) + (ref,indsp) let lookup_canonical_conversion (proj,pat) = assoc_pat pat (GlobRef.Map.find proj !object_table) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index aaba7cc3e5..fd156adc2c 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -73,7 +73,7 @@ type cs_pattern = | Default_cs type obj_typ = { - o_ORIGIN : Constant.t; + o_ORIGIN : GlobRef.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) @@ -87,13 +87,15 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co val pr_cs_pattern : cs_pattern -> Pp.t +type cs = GlobRef.t * inductive + val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> - Constant.t * inductive -> unit -val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive + cs -> unit +val subst_canonical_structure : Mod_subst.substitution -> cs -> cs val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool val canonical_projections : unit -> ((GlobRef.t * cs_pattern) * obj_typ) list -val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive +val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 48d5fac321..6486435ca2 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1290,7 +1290,7 @@ let is_mimick_head sigma ts f = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in - let (evd',j') = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in + let (evd',j',_trace) = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in (evd',j'.uj_val) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 58c0f7db53..e466992721 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -678,7 +678,7 @@ let define_with_type sigma env ev c = let t = Retyping.get_type_of env sigma ev in let ty = Retyping.get_type_of env sigma c in let j = Environ.make_judge c ty in - let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in + let (sigma, j, _trace) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in let (ev, _) = destEvar sigma ev in let sigma = Evd.define ev j.Environ.uj_val sigma in sigma diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9258a75461..f6f7c71dfd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2977,6 +2977,13 @@ let quantify lconstr = (* Modifying/Adding an hypothesis *) +(* This applies (f i) to all elements of ctxt where the debrujn i is + free (so it is lifted at each level). *) +let rec map_rel_context_lift f env i (ctxt:EConstr.rel_context):EConstr.rel_context = + match ctxt with + | [] -> ctxt + | decl::ctxt' -> f i decl :: map_rel_context_lift f env (i+1) ctxt' + (* Instantiating some arguments (whatever their position) of an hypothesis or any term, leaving other arguments quantified. If operating on an hypothesis of the goal, the new hypothesis replaces it. @@ -2993,16 +3000,17 @@ let quantify lconstr = solve, ui are a mix of inferred args and yi. The overall effect is to remove from H as much quantification as possible given lbind. *) + let specialize (c,lbind) ipat = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let sigma, term = + let typ_of_c = Retyping.get_type_of env sigma c in + let sigma, term, typ = if lbind == NoBindings then - sigma, c + sigma, c, typ_of_c else (* ***** SOLVING ARGS ******* *) - let typ_of_c = Retyping.get_type_of env sigma c in (* If the term is lambda then we put a letin to put avoid interaction between the term and the bindings. *) let c = match EConstr.kind sigma c with @@ -3028,38 +3036,53 @@ let specialize (c,lbind) ipat = | _ -> x in (* We grab names used in product to remember them at re-abstracting phase *) let typ_of_c_hd = pf_get_type_of gl thd in - let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in + let (lprod:rel_context), concl = decompose_prod_assum sigma typ_of_c_hd in (* lprd = initial products (including letins). l(tstack initially) = the same products after unification vs lbind (some metas remain) args: accumulator : args to apply to hd: inferred args + metas reabstracted *) - let rec rebuild_lambdas sigma lprd args hd l = + let rec rebuild sigma concl (lprd:rel_context) (accargs:EConstr.t list) + (accprods:rel_context) hd (l:EConstr.t list) = + let open Context.Rel.Declaration in match lprd , l with - | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args)) - | Context.Rel.Declaration.LocalAssum(nme,_)::lp' , t::l' when occur_meta sigma t -> + | _, [] -> sigma + , applist (hd, (List.map (nf_evar sigma) (List.rev accargs))) + , EConstr.it_mkProd_or_LetIn concl accprods + | (LocalAssum(nme,_) as assum)::lp' , t::l' when occur_meta sigma t -> (* nme has not been resolved, let us re-abstract it. Same name but type updated by instantiation of other args. *) let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in let r = Retyping.relevance_of_type env sigma new_typ_of_t in - let liftedargs = List.map liftrel args in (* lifting rels in the accumulator args *) - let sigma,hd' = rebuild_lambdas sigma lp' (liftedargs@[mkRel 1 ]) hd l' in + let liftedargs = List.map liftrel accargs in + let sigma,hd',prods = + rebuild sigma concl lp' (mkRel 1 ::liftedargs) (assum::accprods) hd l' in (* replace meta variable by the abstracted variable *) let hd'' = subst_term sigma t hd' in - (* lambda expansion *) - sigma,mkLambda ({nme with binder_relevance=r},new_typ_of_t,hd'') - | Context.Rel.Declaration.LocalAssum _::lp' , t::l' -> - let sigma,hd' = rebuild_lambdas sigma lp' (args@[t]) hd l' in - sigma,hd' - | Context.Rel.Declaration.LocalDef _::lp' , _ -> - (* letins have been reduced in l and should anyway not - correspond to an arg, we ignore them. *) - let sigma,hd' = rebuild_lambdas sigma lp' args hd l in - sigma,hd' + (* we reabstract the non solved argument *) + sigma,mkLambda ({nme with binder_relevance=r},new_typ_of_t,hd''),prods + | (LocalAssum (nme,tnme))::lp' , t::l' -> + (* thie arg was solved, we update thing accordingly *) + (* we replace in lprod the arg by rel 1 *) + let substlp' = (* rel 1 must be lifted along the context *) + map_rel_context_lift (fun i x -> map_constr (replace_term sigma (mkRel i) t) x) + env 1 lp' in + (* Then we lift every rel above the just removed arg *) + let updatedlp' = + map_rel_context_lift (fun i x -> map_constr (liftn (-1) i) x) env 1 substlp' in + (* We replace also the term in the conclusion, its rel index is the + length of the list lprd (remaining products before concl) *) + let concl'' = replace_term sigma (mkRel (List.length lprd)) t concl in + (* we also lift in concl the index above the arg *) + let concl' = liftn (-1) (List.length lprd) concl'' in + rebuild sigma concl' updatedlp' (t::accargs) accprods hd l' + | LocalDef _ as assum::lp' , _ -> + (* letins have been reduced in l and should anyway not correspond to an arg, we + ignore them, but we remember them in accprod, so that they remain in the type. *) + rebuild sigma concl lp' accargs (assum::accprods) hd l | _ ,_ -> assert false in - let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] thd tstack in - Evd.clear_metas sigma, hd + let sigma,hd,newtype = rebuild sigma concl (List.rev lprod) [] [] thd tstack in + Evd.clear_metas sigma, hd, newtype in - let typ = Retyping.get_type_of env sigma term in let tac = match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> diff --git a/test-suite/Makefile b/test-suite/Makefile index 1d21b4b5e0..265c2eafa7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -643,7 +643,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) %.vio.log:%.v @echo "TEST $<" $(HIDE){ \ - $(coqc) -quick -R vio vio $* 2>&1 && \ + $(coqc) -vio -R vio vio $* 2>&1 && \ $(coqc) -R vio vio -vio2vo $*.vio 2>&1 && \ $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ diff --git a/test-suite/bugs/bug_11140.v b/test-suite/bugs/bug_11140.v new file mode 100644 index 0000000000..ca806ea324 --- /dev/null +++ b/test-suite/bugs/bug_11140.v @@ -0,0 +1,11 @@ +Axiom T : nat -> Prop. +Axiom f : forall x, T x. +Arguments f & x. + +Lemma test : (f (1 + _) : T 2) = f 2. +match goal with +| |- (f (1 + 1) = f 2) => idtac +| |- (f 2 = f 2) => fail (* Issue 11140 *) +| |- _ => fail +end. +Abort. diff --git a/test-suite/bugs/closed/bug_11133.v b/test-suite/bugs/closed/bug_11133.v new file mode 100644 index 0000000000..87f15a4a19 --- /dev/null +++ b/test-suite/bugs/closed/bug_11133.v @@ -0,0 +1,18 @@ +Module Type Universe. +Parameter U : nat. +End Universe. + +Module Univ_prop (Univ : Universe). +Include Univ. +End Univ_prop. + +Module Monad (Univ : Universe). +Module UP := (Univ_prop Univ). +End Monad. + +Module Rules (Univ:Universe). +Module MP := Monad Univ. +Include MP. +Import UP. +Definition M := UP.U. (* anomaly here *) +End Rules. diff --git a/test-suite/bugs/closed/bug_11168.v b/test-suite/bugs/closed/bug_11168.v new file mode 100644 index 0000000000..6e109e33e6 --- /dev/null +++ b/test-suite/bugs/closed/bug_11168.v @@ -0,0 +1,5 @@ +Axiom f : forall T, T. +Arguments f &. +Check f _ _. +Check f (_ -> _) _. +Check f (forall x, _) _. diff --git a/test-suite/bugs/closed/bug_11360.v b/test-suite/bugs/closed/bug_11360.v new file mode 100644 index 0000000000..d8bc4a9f02 --- /dev/null +++ b/test-suite/bugs/closed/bug_11360.v @@ -0,0 +1,6 @@ +Section S. + Variable (A:Type). + #[universes(template)] + Inductive bar (d:A) := . +End S. +Check bar nat 0. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh index e1f17725dc..13e484b852 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh @@ -5,20 +5,14 @@ set -e cd "$(dirname "${BASH_SOURCE[0]}")" -python2 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log2 || exit $? -python3 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log3 || exit $? +"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $? +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $? -cat time-of-build.log.in | python2 "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log2 || exit $? -cat time-of-build.log.in | python3 "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log3 || exit $? +cat time-of-build.log.in | "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $? +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $? -(python2 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log2 -(python3 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log3 +("$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $? +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index 9f3b648aa3..cfacf738a3 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -9,3 +9,4 @@ export COQLIB ./001-correct-diff-sorting-order/run.sh ./002-single-file-sorting/run.sh +./003-non-utf8/run.sh diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out new file mode 100644 index 0000000000..0b4b4b6e37 --- /dev/null +++ b/test-suite/coqdoc/bug11353.html.out @@ -0,0 +1,39 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.bug11353</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug11353</h1> + +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> := 0. #[ <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/> +<span class="id" title="keyword">Inductive</span> <a name="mysum"><span class="id" title="inductive">mysum</span></a> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/> + | <a name="myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a><br/> + | <a name="myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a>.<br/> + +<br/> +#[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a name="b"><span class="id" title="definition">b</span></a> := 1.<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/bug11353.tex.out b/test-suite/coqdoc/bug11353.tex.out new file mode 100644 index 0000000000..a6478682d8 --- /dev/null +++ b/test-suite/coqdoc/bug11353.tex.out @@ -0,0 +1,34 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug11353}{Library }{Coqdoc.bug11353} + +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug11353.a}{a}{\coqdocdefinition{a}} := 0. \#[ \coqdocvar{universes}( \coqdocvar{template}) ]\coqdoceol +\coqdocnoindent +\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdocvar{A} \coqdocvar{B}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqdocvariable{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqdocvariable{B} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug11353.v b/test-suite/coqdoc/bug11353.v new file mode 100644 index 0000000000..b68902c8cc --- /dev/null +++ b/test-suite/coqdoc/bug11353.v @@ -0,0 +1,7 @@ +(* -*- coq-prog-args: ("-g") -*- *) +Definition a := 0. #[ (* templatize *) universes( template) ] +Inductive mysum (A B:Type) : Type := + | myinl : A -> mysum A B + | myinr : B -> mysum A B. + +#[local]Definition b := 1. diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh index 96bdee2fc2..e60fb48bca 100755 --- a/test-suite/misc/quick-include.sh +++ b/test-suite/misc/quick-include.sh @@ -1,5 +1,5 @@ #!/bin/sh set -e -$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file1.v -$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file2.v +$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file1.v +$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file2.v diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v index b2e3c3e923..fbb3c6bdab 100644 --- a/test-suite/output/ErrorInModule.v +++ b/test-suite/output/ErrorInModule.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-vio") -*- *) Module M. Definition foo := nonexistent. End M. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v index 505c5ce378..a961330b81 100644 --- a/test-suite/output/ErrorInSection.v +++ b/test-suite/output/ErrorInSection.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-vio") -*- *) Section S. Definition foo := nonexistent. End S. diff --git a/test-suite/output/ExtractionString.out b/test-suite/output/ExtractionString.out new file mode 100644 index 0000000000..2a101d9cea --- /dev/null +++ b/test-suite/output/ExtractionString.out @@ -0,0 +1,52 @@ +(** val str : string **) + +let str = + String ((Ascii (False, False, True, False, True, False, True, False)), + (String ((Ascii (False, False, False, True, False, True, True, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, False, False, False, False, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, True, False, True, True, True, False)), + (String ((Ascii (False, True, False, False, True, True, True, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (False, True, True, True, False, True, True, False)), + (String ((Ascii (True, True, True, False, False, True, True, False)), + EmptyString))))))))))))))))))))))))))))))) +str :: String +str = + String0 (Ascii False False True False True False True False) (String0 + (Ascii False False False True False True True False) (String0 (Ascii True + False False True False True True False) (String0 (Ascii True True False + False True True True False) (String0 (Ascii False False False False False + True False False) (String0 (Ascii True False False True False True True + False) (String0 (Ascii True True False False True True True False) + (String0 (Ascii False False False False False True False False) (String0 + (Ascii True False False False False True True False) (String0 (Ascii + False False False False False True False False) (String0 (Ascii True True + False False True True True False) (String0 (Ascii False False True False + True True True False) (String0 (Ascii False True False False True True + True False) (String0 (Ascii True False False True False True True False) + (String0 (Ascii False True True True False True True False) (String0 + (Ascii True True True False False True True False) + EmptyString))))))))))))))) + + +(** val str : char list **) + +let str = + 'T'::('h'::('i'::('s'::(' '::('i'::('s'::(' '::('a'::(' '::('s'::('t'::('r'::('i'::('n'::('g'::[]))))))))))))))) +(** val str : string **) + +let str = + "This is a string" +str :: Prelude.String +str = + "This is a string" + + diff --git a/test-suite/output/ExtractionString.v b/test-suite/output/ExtractionString.v new file mode 100644 index 0000000000..e4b9d22b38 --- /dev/null +++ b/test-suite/output/ExtractionString.v @@ -0,0 +1,25 @@ +Require Import String Extraction. + +Definition str := "This is a string"%string. + +(* Raw extraction of strings, in OCaml *) +Extraction Language OCaml. +Extraction str. + +(* Raw extraction of strings, in Haskell *) +Extraction Language Haskell. +Extraction str. + +(* Extraction to char list, in OCaml *) +Require Import ExtrOcamlString. +Extraction Language OCaml. +Extraction str. + +(* Extraction to native strings, in OCaml *) +Require Import ExtrOcamlNativeString. +Extraction str. + +(* Extraction to native strings, in Haskell *) +Require Import ExtrHaskellString. +Extraction Language Haskell. +Extraction str. diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v index e6d674c1e6..88702a6e80 100644 --- a/test-suite/success/CanonicalStructure.v +++ b/test-suite/success/CanonicalStructure.v @@ -51,3 +51,22 @@ Fail Check (refl_equal _ : l _ = x2). Check s0. Check s1. Check s2. + +Section Y. + Let s3 := MKL x3. + Canonical Structure s3. + Check (refl_equal _ : l _ = x3). +End Y. +Fail Check (refl_equal _ : l _ = x3). +Fail Check s3. + +Section V. + #[canonical] Let s3 := MKL x3. + Check (refl_equal _ : l _ = x3). +End V. + +Section W. + #[canonical, local] Definition s2' := MKL x2. + Check (refl_equal _ : l _ = x2). +End W. +Fail Check (refl_equal _ : l _ = x2). diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 1b04594290..1122b9fa34 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -109,28 +109,37 @@ match goal with H:_ |- _ => clear H end. match goal with H:_ |- _ => exact H end. Qed. -(* let ins should be supported in the type of the specialized hypothesis *) -Axiom foo: forall (m1 m2: nat), let n := 2 * m1 in m1 = m2 -> False. + +(* let ins should be supported int he type of the specialized hypothesis *) +Axiom foo: forall (m1:nat) (m2: nat), let n := 2 * m1 in (m1 = m2 -> False). Goal False. pose proof foo as P. assert (2 = 2) as A by reflexivity. + (* specialize P with (m2:= 2). *) specialize P with (1 := A). + match type of P with + | let n := 2 * 2 in False => idtac + | _ => fail "test failed" + end. assumption. Qed. (* Another more subtle test on letins: they should not interfere with foralls. *) -Goal forall (P: forall y:nat, - forall A (zz:A), - let a := zz in - let x := 1 in - forall n : y = x, - n = n), +Goal forall (P: forall a c:nat, + let b := c in + let d := 1 in + forall n : a = d, a = c+1), True. intros P. - specialize P with (zz := @eq_refl _ 2). + specialize P with (1:=eq_refl). + match type of P with + | forall c : nat, let f := c in let d := 1 in 1 = c + 1 => idtac + | _ => fail "test failed" + end. constructor. Qed. + (* Test specialize as *) Goal (forall x, x=0) -> 1=0. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 38723e291f..74335da2f1 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -120,62 +120,6 @@ Section Facts. Qed. - (************************) - (** *** Facts about [In] *) - (************************) - - - (** Characterization of [In] *) - - Theorem in_eq : forall (a:A) (l:list A), In a (a :: l). - Proof. - simpl; auto. - Qed. - - Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). - Proof. - simpl; auto. - Qed. - - Theorem not_in_cons (x a : A) (l : list A): - ~ In x (a::l) <-> x<>a /\ ~ In x l. - Proof. - simpl. intuition. - Qed. - - Theorem in_nil : forall a:A, ~ In a []. - Proof. - unfold not; intros a H; inversion_clear H. - Qed. - - Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2. - Proof. - induction l; simpl; destruct 1. - subst a; auto. - exists [], l; auto. - destruct (IHl H) as (l1,(l2,H0)). - exists (a::l1), l2; simpl. apply f_equal. auto. - Qed. - - (** Inversion *) - Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. - Proof. - intros a b l H; inversion_clear H; auto. - Qed. - - (** Decidability of [In] *) - Theorem in_dec : - (forall x y:A, {x = y} + {x <> y}) -> - forall (a:A) (l:list A), {In a l} + {~ In a l}. - Proof. - intro H; induction l as [| a0 l IHl]. - right; apply in_nil. - destruct (H a0 a); simpl; auto. - destruct IHl; simpl; auto. - right; unfold not; intros [Hc1| Hc2]; auto. - Defined. - - (**************************) (** *** Facts about [app] *) (**************************) @@ -255,6 +199,14 @@ Section Facts. apply app_cons_not_nil in H1 as []. Qed. + Lemma elt_eq_unit : forall l1 l2 (a b : A), + l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = []. + Proof. + intros l1 l2 a b Heq. + apply app_eq_unit in Heq. + now destruct Heq as [[Heq1 Heq2]|[Heq1 Heq2]]; inversion_clear Heq2. + Qed. + Lemma app_inj_tail : forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b. Proof. @@ -281,6 +233,61 @@ Section Facts. induction l; simpl; auto. Qed. + Lemma last_length : forall (l : list A) a, length (l ++ a :: nil) = S (length l). + Proof. + intros ; rewrite app_length ; simpl. + rewrite <- plus_n_Sm, plus_n_O; reflexivity. + Qed. + + Lemma app_inv_head: + forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + Proof. + induction l; simpl; auto; injection 1; auto. + Qed. + + Lemma app_inv_tail: + forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + Proof. + intros l l1 l2; revert l1 l2 l. + induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; + simpl; auto; intros l H. + absurd (length (x2 :: l2 ++ l) <= length l). + simpl; rewrite app_length; auto with arith. + rewrite <- H; auto with arith. + absurd (length (x1 :: l1 ++ l) <= length l). + simpl; rewrite app_length; auto with arith. + rewrite H; auto with arith. + injection H as [= H H0]; f_equal; eauto. + Qed. + + (************************) + (** *** Facts about [In] *) + (************************) + + + (** Characterization of [In] *) + + Theorem in_eq : forall (a:A) (l:list A), In a (a :: l). + Proof. + simpl; auto. + Qed. + + Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). + Proof. + simpl; auto. + Qed. + + Theorem not_in_cons (x a : A) (l : list A): + ~ In x (a::l) <-> x<>a /\ ~ In x l. + Proof. + simpl. intuition. + Qed. + + Theorem in_nil : forall a:A, ~ In a []. + Proof. + unfold not; intros a H; inversion_clear H. + Qed. + Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m. Proof. intros l m a. @@ -314,27 +321,48 @@ Section Facts. split; auto using in_app_or, in_or_app. Qed. - Lemma app_inv_head: - forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2. Proof. - induction l; simpl; auto; injection 1; auto. + induction l; simpl; destruct 1. + subst a; auto. + exists [], l; auto. + destruct (IHl H) as (l1,(l2,H0)). + exists (a::l1), l2; simpl. apply f_equal. auto. Qed. - Lemma app_inv_tail: - forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + Lemma in_elt : forall (x:A) l1 l2, In x (l1 ++ x :: l2). Proof. - intros l l1 l2; revert l1 l2 l. - induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; - simpl; auto; intros l H. - absurd (length (x2 :: l2 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite <- H; auto with arith. - absurd (length (x1 :: l1 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite H; auto with arith. - injection H as [= H H0]; f_equal; eauto. + intros. + apply in_or_app. + right; left; reflexivity. + Qed. + + Lemma in_elt_inv : forall (x y : A) l1 l2, + In x (l1 ++ y :: l2) -> x = y \/ In x (l1 ++ l2). + Proof. + intros x y l1 l2 Hin. + apply in_app_or in Hin. + destruct Hin as [Hin|[Hin|Hin]]; [right|left|right]; try apply in_or_app; intuition. Qed. + (** Inversion *) + Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. + Proof. easy. Qed. + + (** Decidability of [In] *) + Theorem in_dec : + (forall x y:A, {x = y} + {x <> y}) -> + forall (a:A) (l:list A), {In a l} + {~ In a l}. + Proof. + intro H; induction l as [| a0 l IHl]. + right; apply in_nil. + destruct (H a0 a); simpl; auto. + destruct IHl; simpl; auto. + right; unfold not; intros [Hc1| Hc2]; auto. + Defined. + + + End Facts. Hint Resolve app_assoc app_assoc_reverse: datatypes. @@ -463,6 +491,22 @@ Section Elts. - intros; simpl; rewrite IHl; auto with arith. Qed. + Lemma app_nth2_plus : forall l l' d n, + nth (length l + n) (l ++ l') d = nth n l' d. + Proof. + intros. + rewrite app_nth2, minus_plus; trivial. + auto with arith. + Qed. + + Lemma nth_middle : forall l l' a d, + nth (length l) (l ++ a :: l') d = a. + Proof. + intros. + rewrite plus_n_O at 1. + apply app_nth2_plus. + Qed. + Lemma nth_split n l d : n < length l -> exists l1, exists l2, l = l1 ++ nth n l d :: l2 /\ length l1 = n. Proof. @@ -473,6 +517,20 @@ Section Elts. exists (a::l1); exists l2; simpl; split; now f_equal. Qed. + Lemma nth_ext : forall l l' d, length l = length l' -> + (forall n, nth n l d = nth n l' d) -> l = l'. + Proof. + induction l; intros l' d Hlen Hnth; destruct l' as [| b l']. + - reflexivity. + - inversion Hlen. + - inversion Hlen. + - change a with (nth 0 (a :: l) d). + change b with (nth 0 (b :: l') d). + rewrite Hnth; f_equal. + apply IHl with d; [ now inversion Hlen | ]. + intros n; apply (Hnth (S n)). + Qed. + (** Results about [nth_error] *) Lemma nth_error_In l n x : nth_error l n = Some x -> In x l. @@ -556,31 +614,9 @@ Section Elts. rewrite app_nth2; [| auto]. repeat (rewrite Nat.sub_diag). reflexivity. Qed. - (*****************) - (** ** Remove *) - (*****************) - - Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. - - Fixpoint remove (x : A) (l : list A) : list A := - match l with - | [] => [] - | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) - end. - - Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). - Proof. - induction l as [|x l]; auto. - intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. - apply IHl. - unfold not; intro HF; simpl in HF; destruct HF; auto. - apply (IHl y); assumption. - Qed. - - -(******************************) -(** ** Last element of a list *) -(******************************) + (******************************) + (** ** Last element of a list *) + (******************************) (** [last l d] returns the last element of the list [l], or the default value [d] if [l] is empty. *) @@ -592,6 +628,13 @@ Section Elts. | a :: l => last l d end. + Lemma last_last : forall l a d, last (l ++ [a]) d = a. + Proof. + induction l; intros; [ reflexivity | ]. + simpl; rewrite IHl. + destruct l; reflexivity. + Qed. + (** [removelast l] remove the last element of [l] *) Fixpoint removelast (l:list A) : list A := @@ -638,6 +681,119 @@ Section Elts. destruct (l++l'); [elim H0; auto|f_equal; auto]. Qed. + Lemma removelast_last : forall l a, removelast (l ++ [a]) = l. + Proof. + intros. + rewrite removelast_app. + - apply app_nil_r. + - intros Heq; inversion Heq. + Qed. + + + (*****************) + (** ** Remove *) + (*****************) + + Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + + Fixpoint remove (x : A) (l : list A) : list A := + match l with + | [] => [] + | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) + end. + + Lemma remove_cons : forall x l, remove x (x :: l) = remove x l. + Proof. + intros x l; simpl; destruct (eq_dec x x); [ reflexivity | now exfalso ]. + Qed. + + Lemma remove_app : forall x l1 l2, + remove x (l1 ++ l2) = remove x l1 ++ remove x l2. + Proof. + induction l1; intros l2; simpl. + - reflexivity. + - destruct (eq_dec x a). + + apply IHl1. + + rewrite <- app_comm_cons; f_equal. + apply IHl1. + Qed. + + Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). + Proof. + induction l as [|x l]; auto. + intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. + apply IHl. + unfold not; intro HF; simpl in HF; destruct HF; auto. + apply (IHl y); assumption. + Qed. + + Lemma notin_remove: forall l x, ~ In x l -> remove x l = l. + Proof. + intros l x; induction l as [|y l]; simpl; intros Hnin. + - reflexivity. + - destruct (eq_dec x y); subst; intuition. + f_equal; assumption. + Qed. + + Lemma in_remove: forall l x y, In x (remove y l) -> In x l /\ x <> y. + Proof. + induction l as [|z l]; intros x y Hin. + - inversion Hin. + - simpl in Hin. + destruct (eq_dec y z) as [Heq|Hneq]; subst; split. + + right; now apply IHl with z. + + intros Heq; revert Hin; subst; apply remove_In. + + inversion Hin; subst; [left; reflexivity|right]. + now apply IHl with y. + + destruct Hin as [Hin|Hin]; subst. + * now intros Heq; apply Hneq. + * intros Heq; revert Hin; subst; apply remove_In. + Qed. + + Lemma in_in_remove : forall l x y, x <> y -> In x l -> In x (remove y l). + Proof. + induction l as [|z l]; simpl; intros x y Hneq Hin. + - apply Hin. + - destruct (eq_dec y z); subst. + + destruct Hin. + * exfalso; now apply Hneq. + * now apply IHl. + + simpl; destruct Hin; [now left|right]. + now apply IHl. + Qed. + + Lemma remove_remove_comm : forall l x y, + remove x (remove y l) = remove y (remove x l). + Proof. + induction l as [| z l]; simpl; intros x y. + - reflexivity. + - destruct (eq_dec y z); simpl; destruct (eq_dec x z); try rewrite IHl; auto. + + subst; symmetry; apply remove_cons. + + simpl; destruct (eq_dec y z); tauto. + Qed. + + Lemma remove_remove_eq : forall l x, remove x (remove x l) = remove x l. + Proof. intros l x; now rewrite (notin_remove _ _ (remove_In l x)). Qed. + + Lemma remove_length_le : forall l x, length (remove x l) <= length l. + Proof. + induction l as [|y l IHl]; simpl; intros x; trivial. + destruct (eq_dec x y); simpl. + - rewrite IHl; constructor; reflexivity. + - apply (proj1 (Nat.succ_le_mono _ _) (IHl x)). + Qed. + + Lemma remove_length_lt : forall l x, In x l -> length (remove x l) < length l. + Proof. + induction l as [|y l IHl]; simpl; intros x Hin. + - contradiction Hin. + - destruct Hin as [-> | Hin]. + + destruct (eq_dec x x); intuition. + apply Nat.lt_succ_r, remove_length_le. + + specialize (IHl _ Hin); destruct (eq_dec x y); simpl; auto. + now apply Nat.succ_lt_mono in IHl. + Qed. + (******************************************) (** ** Counting occurrences of an element *) @@ -743,6 +899,12 @@ Section ListOps. rewrite IHl; auto. Qed. + Lemma rev_eq_app : forall l l1 l2, rev l = l1 ++ l2 -> l = rev l2 ++ rev l1. + Proof. + intros l l1 l2 Heq. + rewrite <- (rev_involutive l), Heq. + apply rev_app_distr. + Qed. (** Compatibility with other operations *) @@ -820,30 +982,27 @@ Section ListOps. Section Reverse_Induction. - Lemma rev_list_ind : - forall P:list A-> Prop, - P [] -> - (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> - forall l:list A, P (rev l). + Lemma rev_list_ind : forall P:list A-> Prop, + P [] -> + (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> + forall l:list A, P (rev l). Proof. induction l; auto. Qed. - Theorem rev_ind : - forall P:list A -> Prop, - P [] -> - (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l. + Theorem rev_ind : forall P:list A -> Prop, + P [] -> + (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l. Proof. intros. generalize (rev_involutive l). intros E; rewrite <- E. apply (rev_list_ind P). - auto. - - simpl. - intros. - apply (H0 a (rev l0)). - auto. + - auto. + - simpl. + intros. + apply (H0 a (rev l0)). + auto. Qed. End Reverse_Induction. @@ -871,10 +1030,28 @@ Section ListOps. Lemma concat_app : forall l1 l2, concat (l1 ++ l2) = concat l1 ++ concat l2. Proof. intros l1; induction l1 as [|x l1 IH]; intros l2; simpl. - + reflexivity. - + rewrite IH; apply app_assoc. + - reflexivity. + - rewrite IH; apply app_assoc. Qed. + Lemma in_concat : forall l y, + In y (concat l) <-> exists x, In x l /\ In y x. + Proof. + induction l; simpl; split; intros. + contradiction. + destruct H as (x,(H,_)); contradiction. + destruct (in_app_or _ _ _ H). + exists a; auto. + destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)). + exists x; auto. + apply in_or_app. + destruct H as (x,(H0,H1)); destruct H0. + subst; auto. + right; destruct (IHl y) as (_,H2); apply H2. + exists x; auto. + Qed. + + (***********************************) (** ** Decidable equality on lists *) (***********************************) @@ -944,6 +1121,13 @@ Section Map. intros; rewrite IHl; auto. Qed. + Lemma map_last : forall l a, + map (l ++ [a]) = (map l) ++ [f a]. + Proof. + induction l; intros; [ reflexivity | ]. + simpl; rewrite IHl; reflexivity. + Qed. + Lemma map_rev : forall l, map (rev l) = rev (map l). Proof. induction l; simpl; auto. @@ -956,6 +1140,26 @@ Section Map. destruct l; simpl; reflexivity || discriminate. Qed. + Lemma map_eq_cons : forall l l' b, + map l = b :: l' -> exists a tl, l = a :: tl /\ b = f a /\ l' = map tl. + Proof. + intros l l' b Heq. + destruct l; inversion_clear Heq. + exists a, l; repeat split. + Qed. + + Lemma map_eq_app : forall l l1 l2, + map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ l1 = map l1' /\ l2 = map l2'. + Proof. + induction l; simpl; intros l1 l2 Heq. + - symmetry in Heq; apply app_eq_nil in Heq; destruct Heq; subst. + exists nil, nil; repeat split. + - destruct l1; simpl in Heq; inversion Heq as [[Heq2 Htl]]. + + exists nil, (a :: l); repeat split. + + destruct (IHl _ _ Htl) as (l1' & l2' & ? & ? & ?); subst. + exists (a :: l1'), l2'; repeat split. + Qed. + (** [map] and count of occurrences *) Hypothesis decA: forall x1 x2 : A, {x1 = x2} + {x1 <> x2}. @@ -969,10 +1173,10 @@ Section Map. - reflexivity. - specialize (Hrec x). destruct (decA a x) as [H1|H1], (decB (f a) (f x)) as [H2|H2]. - * rewrite Hrec. reflexivity. - * contradiction H2. rewrite H1. reflexivity. - * specialize (Hfinjective H2). contradiction H1. - * assumption. + + rewrite Hrec. reflexivity. + + contradiction H2. rewrite H1. reflexivity. + + specialize (Hfinjective H2). contradiction H1. + + assumption. Qed. (** [flat_map] *) @@ -984,10 +1188,18 @@ Section Map. | cons x t => (f x)++(flat_map t) end. + Lemma flat_map_app : forall f l1 l2, + flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2. + Proof. + intros F l1 l2. + induction l1; [ reflexivity | simpl ]. + rewrite IHl1, app_assoc; reflexivity. + Qed. + Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B), In y (flat_map f l) <-> exists x, In x l /\ In y (f x). - Proof using A B. - clear Hfinjective. + Proof. + clear f Hfinjective. induction l; simpl; split; intros. contradiction. destruct H as (x,(H,_)); contradiction. @@ -1008,15 +1220,22 @@ Lemma flat_map_concat_map : forall A B (f : A -> list B) l, flat_map f l = concat (map f l). Proof. intros A B f l; induction l as [|x l IH]; simpl. -+ reflexivity. -+ rewrite IH; reflexivity. +- reflexivity. +- rewrite IH; reflexivity. Qed. Lemma concat_map : forall A B (f : A -> B) l, map f (concat l) = concat (map (map f) l). Proof. intros A B f l; induction l as [|x l IH]; simpl. -+ reflexivity. -+ rewrite map_app, IH; reflexivity. +- reflexivity. +- rewrite map_app, IH; reflexivity. +Qed. + +Lemma remove_concat A (eq_dec : forall x y : A, {x = y}+{x <> y}) : forall l x, + remove eq_dec x (concat l) = flat_map (remove eq_dec x) l. +Proof. + intros l x; induction l; [ reflexivity | simpl ]. + rewrite remove_app, IHl; reflexivity. Qed. Lemma map_id : forall (A :Type) (l : list A), @@ -1057,6 +1276,25 @@ Proof. intros; apply map_ext_in; auto. Qed. +Lemma flat_map_ext : forall (A B : Type)(f g : A -> list B), + (forall a, f a = g a) -> forall l, flat_map f l = flat_map g l. +Proof. + intros A B f g Hext l. + rewrite 2 flat_map_concat_map. + now rewrite map_ext with (g := g). +Qed. + +Lemma nth_nth_nth_map A : forall (l : list A) n d ln dn, n < length ln \/ length l <= dn -> + nth (nth n ln dn) l d = nth n (map (fun x => nth x l d) ln) d. +Proof. + intros l n d ln dn; revert n; induction ln; intros n Hlen. + - destruct Hlen as [Hlen|Hlen]. + + inversion Hlen. + + now rewrite nth_overflow; destruct n. + - destruct n; simpl; [ reflexivity | apply IHln ]. + destruct Hlen; [ left; apply lt_S_n | right ]; assumption. +Qed. + (************************************) (** Left-to-right iterator on lists *) @@ -1168,8 +1406,8 @@ End Fold_Right_Recursor. Fixpoint existsb (l:list A) : bool := match l with - | nil => false - | a::l => f a || existsb l + | nil => false + | a::l => f a || existsb l end. Lemma existsb_exists : @@ -1208,8 +1446,8 @@ End Fold_Right_Recursor. Fixpoint forallb (l:list A) : bool := match l with - | nil => true - | a::l => f a && forallb l + | nil => true + | a::l => f a && forallb l end. Lemma forallb_forall : @@ -1231,12 +1469,13 @@ End Fold_Right_Recursor. solve[auto]. case (f a); simpl; solve[auto]. Qed. + (** [filter] *) Fixpoint filter (l:list A) : list A := match l with - | nil => nil - | x :: l => if f x then x::(filter l) else filter l + | nil => nil + | x :: l => if f x then x::(filter l) else filter l end. Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true. @@ -1265,8 +1504,8 @@ End Fold_Right_Recursor. Fixpoint find (l:list A) : option A := match l with - | nil => None - | x :: tl => if f x then Some x else find tl + | nil => None + | x :: tl => if f x then Some x else find tl end. Lemma find_some l x : find l = Some x -> In x l /\ f x = true. @@ -1288,9 +1527,9 @@ End Fold_Right_Recursor. Fixpoint partition (l:list A) : list A * list A := match l with - | nil => (nil, nil) - | x :: tl => let (g,d) := partition tl in - if f x then (x::g,d) else (g,x::d) + | nil => (nil, nil) + | x :: tl => let (g,d) := partition tl in + if f x then (x::g,d) else (g,x::d) end. Theorem partition_cons1 a l l1 l2: @@ -1405,8 +1644,8 @@ End Fold_Right_Recursor. Fixpoint split (l:list (A*B)) : list A * list B := match l with - | [] => ([], []) - | (x,y) :: tl => let (left,right) := split tl in (x::left, y::right) + | [] => ([], []) + | (x,y) :: tl => let (left,right) := split tl in (x::left, y::right) end. Lemma in_split_l : forall (l:list (A*B))(p:A*B), @@ -1460,8 +1699,8 @@ End Fold_Right_Recursor. Fixpoint combine (l : list A) (l' : list B) : list (A*B) := match l,l' with - | x::tl, y::tl' => (x,y)::(combine tl tl') - | _, _ => nil + | x::tl, y::tl' => (x,y)::(combine tl tl') + | _, _ => nil end. Lemma split_combine : forall (l: list (A*B)), @@ -1528,8 +1767,8 @@ End Fold_Right_Recursor. Fixpoint list_prod (l:list A) (l':list B) : list (A * B) := match l with - | nil => nil - | cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l') + | nil => nil + | cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l') end. Lemma in_prod_aux : @@ -1544,17 +1783,17 @@ End Fold_Right_Recursor. Lemma in_prod : forall (l:list A) (l':list B) (x:A) (y:B), - In x l -> In y l' -> In (x, y) (list_prod l l'). + In x l -> In y l' -> In (x, y) (list_prod l l'). Proof. induction l; - [ simpl; tauto - | simpl; intros; apply in_or_app; destruct H; - [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. + [ simpl; tauto + | simpl; intros; apply in_or_app; destruct H; + [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. Qed. Lemma in_prod_iff : forall (l:list A)(l':list B)(x:A)(y:B), - In (x,y) (list_prod l l') <-> In x l /\ In y l'. + In (x,y) (list_prod l l') <-> In x l /\ In y l'. Proof. split; [ | intros; apply in_prod; intuition ]. induction l; simpl; intros. @@ -1650,6 +1889,18 @@ Section SetIncl. Definition incl (l m:list A) := forall a:A, In a l -> In a m. Hint Unfold incl : core. + Lemma incl_nil_l : forall l, incl nil l. + Proof. + intros l a Hin; inversion Hin. + Qed. + + Lemma incl_l_nil : forall l, incl l nil -> l = nil. + Proof. + destruct l; intros Hincl. + - reflexivity. + - exfalso; apply Hincl with a; simpl; auto. + Qed. + Lemma incl_refl : forall l:list A, incl l l. Proof. auto. @@ -1694,6 +1945,13 @@ Section SetIncl. Qed. Hint Resolve incl_cons : core. + Lemma incl_cons_inv : forall (a:A) (l m:list A), + incl (a :: l) m -> In a m /\ incl l m. + Proof. + intros a l m Hi. + split; [ | intros ? ? ]; apply Hi; simpl; auto. + Qed. + Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n. Proof. unfold incl; simpl; intros l m n H H0 a H1. @@ -1702,6 +1960,34 @@ Section SetIncl. Qed. Hint Resolve incl_app : core. + Lemma incl_app_app : forall l1 l2 m1 m2:list A, + incl l1 m1 -> incl l2 m2 -> incl (l1 ++ l2) (m1 ++ m2). + Proof. + intros. + apply incl_app; [ apply incl_appl | apply incl_appr]; assumption. + Qed. + + Lemma incl_app_inv : forall l1 l2 m : list A, + incl (l1 ++ l2) m -> incl l1 m /\ incl l2 m. + Proof. + induction l1; intros l2 m Hin; split; auto. + - apply incl_nil_l. + - intros b Hb; inversion_clear Hb; subst; apply Hin. + + now constructor. + + simpl; apply in_cons. + apply incl_appl with l1; [ apply incl_refl | assumption ]. + - apply IHl1. + now apply incl_cons_inv in Hin. + Qed. + + Lemma remove_incl (eq_dec : forall x y : A, {x = y} + {x <> y}) : forall l1 l2 x, + incl l1 l2 -> incl (remove eq_dec x l1) (remove eq_dec x l2). + Proof. + intros l1 l2 x Hincl y Hin. + apply in_remove in Hin; destruct Hin as [Hin Hneq]. + apply in_in_remove; intuition. + Qed. + End SetIncl. Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons @@ -1825,9 +2111,11 @@ Section Cutting. Lemma skipn_cons n a l: skipn (S n) (a::l) = skipn n l. Proof. reflexivity. Qed. - Lemma skipn_none : forall l, skipn (length l) l = []. + Lemma skipn_all : forall l, skipn (length l) l = nil. Proof. now induction l. Qed. +#[deprecated(since="8.12",note="Use skipn_all instead.")] Notation skipn_none := skipn_all. + Lemma skipn_all2 n: forall l, length l <= n -> skipn n l = []. Proof. intros l L%Nat.sub_0_le; rewrite <-(firstn_all l) at 1. @@ -1855,9 +2143,6 @@ Section Cutting. - destruct l; simpl; auto. Qed. - Lemma skipn_all l: skipn (length l) l = nil. - Proof. now induction l. Qed. - Lemma skipn_app n : forall l1 l2, skipn n (l1 ++ l2) = (skipn n l1) ++ (skipn (n - length l1) l2). Proof. induction n; auto; intros [|]; simpl; auto. Qed. @@ -1884,7 +2169,7 @@ Section Cutting. intros x l; rewrite firstn_skipn_rev, rev_involutive, <-rev_length. destruct (Nat.le_ge_cases (length (rev l)) x) as [L | L]. - rewrite skipn_all2; [apply Nat.sub_0_le in L | trivial]. - now rewrite L, Nat.sub_0_r, skipn_none. + now rewrite L, Nat.sub_0_r, skipn_all. - replace (length (rev l) - (length (rev l) - x)) with (length (rev l) + x - length (rev l)). rewrite minus_plus. reflexivity. @@ -1911,6 +2196,13 @@ Section Cutting. inversion_clear H0. Qed. + Lemma removelast_firstn_len : forall l, + removelast l = firstn (pred (length l)) l. + Proof. + induction l; [ reflexivity | simpl ]. + destruct l; [ | rewrite IHl ]; reflexivity. + Qed. + Lemma firstn_removelast : forall n l, n < length l -> firstn n (removelast l) = firstn n l. Proof. @@ -2082,6 +2374,16 @@ Section ReDun. + now constructor. Qed. + Lemma NoDup_rev l : NoDup l -> NoDup (rev l). + Proof. + induction l; simpl; intros Hnd; [ constructor | ]. + inversion_clear Hnd as [ | ? ? Hnin Hndl ]. + assert (Add a (rev l) (rev l ++ a :: nil)) as Hadd + by (rewrite <- (app_nil_r (rev l)) at 1; apply Add_app). + apply NoDup_Add in Hadd; apply Hadd; intuition. + now apply Hnin, in_rev. + Qed. + (** Effective computation of a list without duplicates *) Hypothesis decA: forall x y : A, {x = y} + {x <> y}. @@ -2110,6 +2412,11 @@ Section ReDun. * reflexivity. Qed. + Lemma nodup_incl l1 l2 : incl l1 (nodup l2) <-> incl l1 l2. + Proof. + split; intros Hincl a Ha; apply nodup_In; intuition. + Qed. + Lemma NoDup_nodup l: NoDup (nodup l). Proof. induction l as [|a l' Hrec]; simpl. @@ -2252,6 +2559,11 @@ Section NatSeq. | S len => start :: seq (S start) len end. + Lemma cons_seq : forall len start, start :: seq (S start) len = seq start (S len). + Proof. + reflexivity. + Qed. + Lemma seq_length : forall len start, length (seq start len) = len. Proof. induction len; simpl; auto. @@ -2284,8 +2596,8 @@ Section NatSeq. - rewrite <- plus_n_O. split;[easy|]. intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')). - rewrite IHlen, <- plus_n_Sm; simpl; split. - * intros [H|H]; subst; intuition auto with arith. - * intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. + + intros [H|H]; subst; intuition auto with arith. + + intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. Qed. Lemma seq_NoDup len start : NoDup (seq start len). @@ -2302,6 +2614,14 @@ Section NatSeq. - now rewrite Nat.add_succ_r, IHlen. Qed. + Lemma seq_S : forall len start, seq start (S len) = seq start len ++ [start + len]. + Proof. + intros len start. + change [start + len] with (seq (start + len) 1). + rewrite <- seq_app. + rewrite <- plus_n_Sm, <- plus_n_O; reflexivity. + Qed. + End NatSeq. Section Exists_Forall. @@ -2328,6 +2648,21 @@ Section Exists_Forall. - induction l; firstorder; subst; auto. Qed. + Lemma Exists_nth l : + Exists l <-> exists i d, i < length l /\ P (nth i l d). + Proof. + split. + - intros HE; apply Exists_exists in HE. + destruct HE as [a [Hin HP]]. + apply In_nth with (d := a) in Hin; destruct Hin as [i [Hl Heq]]. + rewrite <- Heq in HP. + now exists i; exists a. + - intros [i [d [Hl HP]]]. + apply Exists_exists; exists (nth i l d); split. + apply nth_In; assumption. + assumption. + Qed. + Lemma Exists_nil : Exists nil <-> False. Proof. split; inversion 1. Qed. @@ -2335,6 +2670,21 @@ Section Exists_Forall. Exists (x::l) <-> P x \/ Exists l. Proof. split; inversion 1; auto. Qed. + Lemma Exists_app l1 l2 : + Exists (l1 ++ l2) <-> Exists l1 \/ Exists l2. + Proof. + induction l1; simpl; split; intros HE; try now intuition. + - inversion_clear HE; intuition. + - destruct HE as [HE|HE]; intuition. + inversion_clear HE; intuition. + Qed. + + Lemma Exists_rev l : Exists l -> Exists (rev l). + Proof. + induction l; intros HE; intuition. + inversion_clear HE; simpl; apply Exists_app; intuition. + Qed. + Lemma Exists_dec l: (forall x:A, {P x} + { ~ P x }) -> {Exists l} + {~ Exists l}. @@ -2342,12 +2692,25 @@ Section Exists_Forall. intro Pdec. induction l as [|a l' Hrec]. - right. abstract now rewrite Exists_nil. - destruct Hrec as [Hl'|Hl']. - * left. now apply Exists_cons_tl. - * destruct (Pdec a) as [Ha|Ha]. - + left. now apply Exists_cons_hd. - + right. abstract now inversion 1. + + left. now apply Exists_cons_tl. + + destruct (Pdec a) as [Ha|Ha]. + * left. now apply Exists_cons_hd. + * right. abstract now inversion 1. Defined. + Lemma Exists_fold_right l : + Exists l <-> fold_right (fun x => or (P x)) False l. + Proof. + induction l; simpl; split; intros HE; try now inversion HE; intuition. + Qed. + + Lemma incl_Exists l1 l2 : incl l1 l2 -> Exists l1 -> Exists l2. + Proof. + intros Hincl HE. + apply Exists_exists in HE; destruct HE as [a [Hin HP]]. + apply Exists_exists; exists a; intuition. + Qed. + Inductive Forall : list A -> Prop := | Forall_nil : Forall nil | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l). @@ -2362,11 +2725,49 @@ Section Exists_Forall. - induction l; firstorder. Qed. + Lemma Forall_nth l : + Forall l <-> forall i d, i < length l -> P (nth i l d). + Proof. + split. + - intros HF i d Hl. + apply Forall_forall with (x := nth i l d) in HF. + assumption. + apply nth_In; assumption. + - intros HF. + apply Forall_forall; intros a Hin. + apply In_nth with (d := a) in Hin; destruct Hin as [i [Hl Heq]]. + rewrite <- Heq; intuition. + Qed. + Lemma Forall_inv : forall (a:A) l, Forall (a :: l) -> P a. Proof. intros; inversion H; trivial. Qed. + Theorem Forall_inv_tail : forall (a:A) l, Forall (a :: l) -> Forall l. + Proof. + intros; inversion H; trivial. + Qed. + + Lemma Forall_app l1 l2 : + Forall (l1 ++ l2) <-> Forall l1 /\ Forall l2. + Proof. + induction l1; simpl; split; intros HF; try now intuition. + - inversion_clear HF; intuition. + - destruct HF as [HF1 HF2]; inversion HF1; intuition. + Qed. + + Lemma Forall_elt a l1 l2 : Forall (l1 ++ a :: l2) -> P a. + Proof. + intros HF; apply Forall_app in HF; destruct HF as [HF1 HF2]; now inversion HF2. + Qed. + + Lemma Forall_rev l : Forall l -> Forall (rev l). + Proof. + induction l; intros HF; intuition. + inversion_clear HF; simpl; apply Forall_app; intuition. + Qed. + Lemma Forall_rect : forall (Q : list A -> Type), Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall l -> Q l. Proof. @@ -2386,53 +2787,89 @@ Section Exists_Forall. + right. abstract now inversion 1. Defined. + Lemma Forall_fold_right l : + Forall l <-> fold_right (fun x => and (P x)) True l. + Proof. + induction l; simpl; split; intros HF; try now inversion HF; intuition. + Qed. + + Lemma incl_Forall l1 l2 : incl l2 l1 -> Forall l1 -> Forall l2. + Proof. + intros Hincl HF. + apply Forall_forall; intros a Ha. + apply Forall_forall with (x:=a) in HF; intuition. + Qed. + End One_predicate. - Theorem Forall_inv_tail - : forall (P : A -> Prop) (x0 : A) (xs : list A), Forall P (x0 :: xs) -> Forall P xs. + Lemma map_ext_Forall B : forall (f g : A -> B) l, + Forall (fun x => f x = g x) l -> map f l = map g l. Proof. - intros P x0 xs H. - apply Forall_forall with (l := xs). - assert (H0 : forall x : A, In x (x0 :: xs) -> P x). - apply Forall_forall with (P := P) (l := x0 :: xs). - exact H. - assert (H1 : forall (x : A) (H2 : In x xs), P x). - intros x H2. - apply (H0 x). - right. - exact H2. - intros x H2. - apply (H1 x H2). + intros; apply map_ext_in, Forall_forall; assumption. Qed. - Theorem Exists_impl - : forall (P Q : A -> Prop), (forall x : A, P x -> Q x) -> forall xs : list A, Exists P xs -> Exists Q xs. + Theorem Exists_impl : forall (P Q : A -> Prop), (forall a : A, P a -> Q a) -> + forall l, Exists P l -> Exists Q l. Proof. - intros P Q H xs H0. + intros P Q H l H0. induction H0. apply (Exists_cons_hd Q x l (H x H0)). apply (Exists_cons_tl x IHExists). Qed. + Lemma Exists_or : forall (P Q : A -> Prop) l, + Exists P l \/ Exists Q l -> Exists (fun x => P x \/ Q x) l. + Proof. + induction l; intros [H | H]; inversion H; subst. + 1,3: apply Exists_cons_hd; auto. + all: apply Exists_cons_tl, IHl; auto. + Qed. + + Lemma Exists_or_inv : forall (P Q : A -> Prop) l, + Exists (fun x => P x \/ Q x) l -> Exists P l \/ Exists Q l. + Proof. + induction l; intro Hl; inversion Hl as [ ? ? H | ? ? H ]; subst. + - inversion H; now repeat constructor. + - destruct (IHl H); now repeat constructor. + Qed. + + Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> + forall l, Forall P l -> Forall Q l. + Proof. + intros P Q H l. rewrite !Forall_forall. firstorder. + Qed. + + Lemma Forall_and : forall (P Q : A -> Prop) l, + Forall P l -> Forall Q l -> Forall (fun x => P x /\ Q x) l. + Proof. + induction l; intros HP HQ; constructor; inversion HP; inversion HQ; auto. + Qed. + + Lemma Forall_and_inv : forall (P Q : A -> Prop) l, + Forall (fun x => P x /\ Q x) l -> Forall P l /\ Forall Q l. + Proof. + induction l; intro Hl; split; constructor; inversion Hl; firstorder. + Qed. + Lemma Forall_Exists_neg (P:A->Prop)(l:list A) : - Forall (fun x => ~ P x) l <-> ~(Exists P l). + Forall (fun x => ~ P x) l <-> ~(Exists P l). Proof. - rewrite Forall_forall, Exists_exists. firstorder. + rewrite Forall_forall, Exists_exists. firstorder. Qed. Lemma Exists_Forall_neg (P:A->Prop)(l:list A) : (forall x, P x \/ ~P x) -> Exists (fun x => ~ P x) l <-> ~(Forall P l). Proof. - intro Dec. - split. - - rewrite Forall_forall, Exists_exists; firstorder. - - intros NF. - induction l as [|a l IH]. - + destruct NF. constructor. - + destruct (Dec a) as [Ha|Ha]. - * apply Exists_cons_tl, IH. contradict NF. now constructor. - * now apply Exists_cons_hd. + intro Dec. + split. + - rewrite Forall_forall, Exists_exists; firstorder. + - intros NF. + induction l as [|a l IH]. + + destruct NF. constructor. + + destruct (Dec a) as [Ha|Ha]. + * apply Exists_cons_tl, IH. contradict NF. now constructor. + * now apply Exists_cons_hd. Qed. Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) : @@ -2455,17 +2892,61 @@ Section Exists_Forall. now apply neg_Forall_Exists_neg. Defined. - Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> - forall l, Forall P l -> Forall Q l. - Proof. - intros P Q H l. rewrite !Forall_forall. firstorder. - Qed. - End Exists_Forall. Hint Constructors Exists : core. Hint Constructors Forall : core. +Lemma exists_Forall A B : forall (P : A -> B -> Prop) l, + (exists k, Forall (P k) l) -> Forall (fun x => exists k, P k x) l. +Proof. + induction l; intros [k HF]; constructor; inversion_clear HF. + - now exists k. + - now apply IHl; exists k. +Qed. + +Lemma Forall_image A B : forall (f : A -> B) l, + Forall (fun y => exists x, y = f x) l <-> exists l', l = map f l'. +Proof. + induction l; split; intros HF. + - exists nil; reflexivity. + - constructor. + - inversion_clear HF as [| ? ? [x Hx] HFtl]; subst. + destruct (proj1 IHl HFtl) as [l' Heq]; subst. + now exists (x :: l'). + - destruct HF as [l' Heq]. + symmetry in Heq; apply map_eq_cons in Heq. + destruct Heq as (x & tl & ? & ? & ?); subst. + constructor. + + now exists x. + + now apply IHl; exists tl. +Qed. + +Lemma concat_nil_Forall A : forall (l : list (list A)), + concat l = nil <-> Forall (fun x => x = nil) l. +Proof. + induction l; simpl; split; intros Hc; auto. + - apply app_eq_nil in Hc. + constructor; firstorder. + - inversion Hc; subst; simpl. + now apply IHl. +Qed. + +Lemma in_flat_map_Exists A B : forall (f : A -> list B) x l, + In x (flat_map f l) <-> Exists (fun y => In x (f y)) l. +Proof. + intros f x l; rewrite in_flat_map. + split; apply Exists_exists. +Qed. + +Lemma notin_flat_map_Forall A B : forall (f : A -> list B) x l, + ~ In x (flat_map f l) <-> Forall (fun y => ~ In x (f y)) l. +Proof. + intros f x l; rewrite Forall_Exists_neg. + apply not_iff_compat, in_flat_map_Exists. +Qed. + + Section Forall2. (** [Forall2]: stating that elements of two lists are pairwise related. *) @@ -2567,6 +3048,96 @@ Section ForallPairs. Qed. End ForallPairs. +Section Repeat. + + Variable A : Type. + Fixpoint repeat (x : A) (n: nat ) := + match n with + | O => [] + | S k => x::(repeat x k) + end. + + Theorem repeat_length x n: + length (repeat x n) = n. + Proof. + induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity. + Qed. + + Theorem repeat_spec n x y: + In y (repeat x n) -> y=x. + Proof. + induction n as [|k Hrec]; simpl; destruct 1; auto. + Qed. + + Lemma repeat_cons n a : + a :: repeat a n = repeat a n ++ (a :: nil). + Proof. + induction n; simpl. + - reflexivity. + - f_equal; apply IHn. + Qed. + +End Repeat. + +Lemma repeat_to_concat A n (a:A) : + repeat a n = concat (repeat [a] n). +Proof. + induction n; simpl. + - reflexivity. + - f_equal; apply IHn. +Qed. + + +(** Sum of elements of a list of [nat]: [list_sum] *) + +Definition list_sum l := fold_right plus 0 l. + +Lemma list_sum_app : forall l1 l2, + list_sum (l1 ++ l2) = list_sum l1 + list_sum l2. +Proof. +induction l1; intros l2; [ reflexivity | ]. +simpl; rewrite IHl1. +apply Nat.add_assoc. +Qed. + +(** Max of elements of a list of [nat]: [list_max] *) + +Definition list_max l := fold_right max 0 l. + +Lemma list_max_app : forall l1 l2, + list_max (l1 ++ l2) = max (list_max l1) (list_max l2). +Proof. +induction l1; intros l2; [ reflexivity | ]. +now simpl; rewrite IHl1, Nat.max_assoc. +Qed. + +Lemma list_max_le : forall l n, + list_max l <= n <-> Forall (fun k => k <= n) l. +Proof. +induction l; simpl; intros n; split; intros H; intuition. +- apply Nat.max_lub_iff in H. + now constructor; [ | apply IHl ]. +- inversion_clear H as [ | ? ? Hle HF ]. + apply IHl in HF; apply Nat.max_lub; assumption. +Qed. + +Lemma list_max_lt : forall l n, l <> nil -> + list_max l < n <-> Forall (fun k => k < n) l. +Proof. +induction l; simpl; intros n Hnil; split; intros H; intuition. +- destruct l. + + repeat constructor. + now simpl in H; rewrite Nat.max_0_r in H. + + apply Nat.max_lub_lt_iff in H. + now constructor; [ | apply IHl ]. +- destruct l; inversion_clear H as [ | ? ? Hlt HF ]. + + now simpl; rewrite Nat.max_0_r. + + apply IHl in HF. + * now apply Nat.max_lub_lt_iff. + * intros Heq; inversion Heq. +Qed. + + (** * Inversion of predicates over lists based on head symbol *) Ltac is_list_constr c := @@ -2633,27 +3204,5 @@ Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) Hint Resolve app_nil_end : datatypes. (* end hide *) -Section Repeat. - - Variable A : Type. - Fixpoint repeat (x : A) (n: nat ) := - match n with - | O => [] - | S k => x::(repeat x k) - end. - - Theorem repeat_length x n: - length (repeat x n) = n. - Proof. - induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity. - Qed. - - Theorem repeat_spec n x y: - In y (repeat x n) -> y=x. - Proof. - induction n as [|k Hrec]; simpl; destruct 1; auto. - Qed. - -End Repeat. (* Unset Universe Polymorphism. *) diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 79ec67b633..6a849bb0b1 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -24,6 +24,9 @@ Declare Scope char_scope. Delimit Scope char_scope with char. Bind Scope char_scope with ascii. +Register ascii as core.ascii.type. +Register Ascii as core.ascii.ascii. + Definition zero := Ascii false false false false false false false false. Definition one := Ascii true false false false false false false false. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 9d0d2f854d..b736f41a08 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -30,8 +30,9 @@ Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. -Register EmptyString as plugins.syntax.EmptyString. -Register String as plugins.syntax.String. +Register string as core.string.type. +Register EmptyString as core.string.empty. +Register String as core.string.string. (** Equality is decidable *) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7cd5962d86..d3ed5e78b4 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -389,7 +389,11 @@ optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles # FIXME, see Ralf's bugreport -quick: $(VOFILES:.vo=.vio) +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") .PHONY: quick vio2vo: @@ -397,8 +401,9 @@ vio2vo: -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +# quick2vo is undocumented quick2vo: - $(HIDE)make -j $(J) quick + $(HIDE)make -j $(J) vio $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ @@ -677,8 +682,8 @@ $(GLOBFILES): %.glob: %.v $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -quick $< - $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vos): %.vos: %.v $(SHOW)COQC -vos $< diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index a44ddf7467..13913cabc3 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -547,6 +547,9 @@ rule coq_bol = parse comment lexbuf end else skipped_comment lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | space* "#[" { + let eol = begin backtrack lexbuf; body_bol lexbuf end + in if eol then coq_bol lexbuf else coq lexbuf } | eof { () } | _ @@ -643,6 +646,11 @@ and coq = parse Output.ident s None; let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | "#[" + { ignore(lexeme lexbuf); + Output.char '#'; Output.char '['; + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space+ { Output.char ' '; coq lexbuf } | eof { () } diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 3c198dc600..dceb811d66 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -121,6 +121,10 @@ let compile opts copts ~echo ~f_in ~f_out = in let long_f_dot_in, long_f_dot_out = ensure_exists_with_prefix f_in f_out ext_in ext_out in + let dump_empty_vos () = + (* Produce an empty .vos file, as a way to ensure that a stale .vos can never be loaded *) + let long_f_dot_vos = (chop_extension long_f_dot_out) ^ ".vos" in + create_empty_file long_f_dot_vos in match mode with | BuildVo | BuildVok -> let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) @@ -145,18 +149,20 @@ let compile opts copts ~echo ~f_in ~f_out = let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); - if mode <> BuildVok (* Don't output proofs in -vok mode *) - then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir long_f_dot_out (Global.opaque_tables ()); + (* In .vo production, dump a complete .vo file. + In .vok production, only dump an empty .vok file. *) + if mode = BuildVo + then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir long_f_dot_out (Global.opaque_tables ()) + else create_empty_file long_f_dot_out; Aux_file.record_in_aux_at "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); - (* Produce an empty .vos file and an empty .vok file when producing a .vo in standard mode *) + (* In .vo production, dump an empty .vos file to indicate that the .vo should be loaded, + and dump an empty .vok file to indicate that proofs are ok. *) if mode = BuildVo then begin - create_empty_file (long_f_dot_out ^ "s"); + dump_empty_vos(); create_empty_file (long_f_dot_out ^ "k"); end; - (* Produce an empty .vok file when in -vok mode *) - if mode = BuildVok then create_empty_file (long_f_dot_out); Dumpglob.end_dump_glob () | BuildVio | BuildVos -> @@ -186,15 +192,22 @@ let compile opts copts ~echo ~f_in ~f_out = let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); let create_vos = (mode = BuildVos) in + (* In .vos production, the output .vos file contains compiled statements. + In .vio production, the output .vio file contains compiled statements and suspended proofs. *) let () = ignore (Stm.snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_out) in - Stm.reset_task_queue () + Stm.reset_task_queue (); + (* In .vio production, dump an empty .vos file to indicate that the .vio should be loaded. *) + if mode = BuildVio then dump_empty_vos() | Vio2Vo -> let sum, lib, univs, tasks, proofs = Library.load_library_todo long_f_dot_in in let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in - Library.save_library_raw long_f_dot_out sum lib univs proofs + Library.save_library_raw long_f_dot_out sum lib univs proofs; + (* Like in direct .vo production, dump an empty .vok file and an empty .vos file. *) + dump_empty_vos(); + create_empty_file (long_f_dot_out ^ "k") let compile opts copts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 178aa362c0..0c15f66c07 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -25,7 +25,6 @@ let coqc_specific_usage = Usage.{ coqc specific options:\ \n -o f.vo use f.vo as the output file name\ \n -verbose compile and output the input file\ -\n -quick quickly compile .v files to .vio files (skip proofs)\ \n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ \n into fi.vo\ \n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ @@ -33,8 +32,10 @@ coqc specific options:\ \n -vos process statements but ignore opaque proofs, and produce a .vos file\ \n -vok process the file by loading .vos instead of .vo files for\ \n dependencies, and produce an empty .vok file on success\ +\n -vio process statements and suspend opaque proofs, and produce a .vio file\ \n\ \nUndocumented:\ +\n -quick (deprecated) alias for -vio\ \n -vio2vo [see manual]\ \n -check-vio-tasks [see manual]\ \n" diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index e614d4fe6d..0c20563d07 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -98,7 +98,7 @@ let set_compilation_mode opts mode = match opts.compilation_mode with | BuildVo -> { opts with compilation_mode = mode } | mode' when mode <> mode' -> - prerr_endline "Options -quick and -vio2vo are exclusive"; + prerr_endline "Options -vio and -vio2vo are exclusive"; exit 1 | _ -> opts @@ -126,6 +126,11 @@ let warn_deprecated_outputstate = (fun () -> Pp.strbrk "The outputstate option is deprecated and discouraged.") +let warn_deprecated_quick = + CWarnings.create ~name:"deprecated-quick" ~category:"deprecated" + (fun () -> + Pp.strbrk "The -quick option is renamed -vio. Please consider using the -vos feature instead.") + let set_outputstate opts s = warn_deprecated_outputstate (); { opts with outputstate = Some s } @@ -165,6 +170,9 @@ let parse arglist : t = | "-o" -> { oval with compilation_output_name = Some (next ()) } | "-quick" -> + warn_deprecated_quick(); + set_compilation_mode oval BuildVio + | "-vio" -> set_compilation_mode oval BuildVio |"-vos" -> Flags.load_vos_libraries := true; diff --git a/vernac/attributes.ml b/vernac/attributes.ml index b7a3b002bd..68d2c3a00d 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -234,5 +234,7 @@ let only_polymorphism atts = parse polymorphic atts let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty] let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty] -let canonical = +let canonical_field = enable_attribute ~key:"canonical" ~default:(fun () -> true) +let canonical_instance = + enable_attribute ~key:"canonical" ~default:(fun () -> false) diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 34ff15ca7d..0074db66d3 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -48,7 +48,8 @@ val program : bool attribute val template : bool option attribute val locality : bool option attribute val deprecation : Deprecation.t option attribute -val canonical : bool attribute +val canonical_field : bool attribute +val canonical_instance : bool attribute val program_mode_option_name : string list (** For internal use when messing with the global option. *) diff --git a/vernac/canonical.ml b/vernac/canonical.ml index 141b02ef63..e41610b532 100644 --- a/vernac/canonical.ml +++ b/vernac/canonical.ml @@ -21,10 +21,12 @@ let cache_canonical_structure (_, (o,_)) = let sigma = Evd.from_env env in register_canonical_structure ~warn:true env sigma o -let discharge_canonical_structure (_,(x, local)) = - if local then None else Some (x, local) +let discharge_canonical_structure (_,((gref, _ as x), local)) = + if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None + else Some (x, local) -let inCanonStruc : (Constant.t * inductive) * bool -> obj = + +let inCanonStruc : (GlobRef.t * inductive) * bool -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 69ab0fafe9..3302231fd1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -471,7 +471,7 @@ GRAMMAR EXTEND Gram [ [ attr = LIST0 quoted_attributes ; bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; rf_notation = decl_notation -> { - let rf_canonical = attr |> List.flatten |> parse canonical in + let rf_canonical = attr |> List.flatten |> parse canonical_field in let rf_subclass, rf_decl = bd in rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ] ; diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index a8462e31e1..506b3bc505 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -138,27 +138,31 @@ let select_vo_file ~warn loadpath base = System.where_in_path ~warn loadpath name in Some (lpath, file) with Not_found -> None in + (* If [!Flags.load_vos_libraries] + and the .vos file exists + and this file is not empty + Then load this library + Else load the most recent between the .vo file and the .vio file, + or if there is only of the two files, take this one, + or raise an error if both are missing. *) + let load_most_recent_of_vo_and_vio () = + match find ".vo", find ".vio" with + | None, None -> + Error LibNotFound + | Some res, None | None, Some res -> + Ok res + | Some (_, vo), Some (_, vi as resvi) + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + Ok resvi + | Some resvo, Some _ -> + Ok resvo + in if !Flags.load_vos_libraries then begin - (* If the .vos file exists and is not empty, it describes the library. - Otherwise, load the .vo file, or fail if is missing. *) match find ".vos" with | Some (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos - | _ -> - match find ".vo" with - | None -> Error LibNotFound - | Some resvo -> Ok resvo - end else - match find ".vo", find ".vio" with - | None, None -> - Error LibNotFound - | Some res, None | None, Some res -> - Ok res - | Some (_, vo), Some (_, vi as resvi) - when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - Ok resvi - | Some resvo, Some _ -> - Ok resvo + | _ -> load_most_recent_of_vo_and_vio() + end else load_most_recent_of_vo_and_vio() let locate_absolute_library dir : CUnix.physical_path locate_result = (* Search in loadpath *) diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 8ced35c3be..b999ce9f3f 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -1003,9 +1003,7 @@ let print_canonical_projections env sigma grefs = | Const_cs y -> GlobRef.equal y gr | _ -> false end || - match gr with - | GlobRef.ConstRef con -> Names.Constant.equal c.o_ORIGIN con - | _ -> false + GlobRef.equal c.o_ORIGIN gr in let projs = List.filter (fun p -> List.for_all (match_proj_gref p) grefs) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 99d74f16cc..e98820bc98 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -63,14 +63,15 @@ module DefAttributes = struct polymorphic : bool; program : bool; deprecated : Deprecation.t option; + canonical_instance : bool; } let parse f = let open Attributes in - let ((locality, deprecated), polymorphic), program = - parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f + let (((locality, deprecated), polymorphic), program), canonical_instance = + parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f in - { polymorphic; program; locality; deprecated } + { polymorphic; program; locality; deprecated; canonical_instance } end let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l)) @@ -522,13 +523,17 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = in start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl -let vernac_definition_hook ~local ~poly = let open Decls in function +let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function | Coercion -> Some (ComCoercion.add_coercion_hook ~poly) | CanonicalStructure -> Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | SubClass -> Some (ComCoercion.add_subclass_hook ~poly) +| Definition when canonical_instance -> + Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) +| Let when canonical_instance -> + Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) | _ -> None let fresh_name_for_anonymous_theorem () = @@ -551,7 +556,7 @@ let vernac_definition_name lid local = let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in + let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in let program_mode = atts.program in let poly = atts.polymorphic in let name = vernac_definition_name lid local in @@ -560,7 +565,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in let scope = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in + let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in let program_mode = atts.program in let name = vernac_definition_name lid scope in let red_option = match red_option with |