diff options
87 files changed, 1735 insertions, 165 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index b0e79fb1b2..2a641263e3 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -71,6 +71,8 @@ azure-pipelines.yml @coq/ci-maintainers /man/ @silene # Secondary maintainer @maximedenes +/doc/plugin_tutorial/ @ybertot + ########## Coqchk ########## /checker/ @ppedrot diff --git a/.gitignore b/.gitignore index 0411247abf..dfecfec837 100644 --- a/.gitignore +++ b/.gitignore @@ -150,6 +150,7 @@ kernel/byterun/coq_jumptbl.h kernel/copcodes.ml ide/index_urls.txt .lia.cache +.nia.cache # emacs save files *~ diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f54f64bf28..50b86b3c5d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -151,7 +151,7 @@ after_script: - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH" - - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all + - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" COQFLAGS="${COQFLAGS}" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -427,6 +427,13 @@ test-suite:edge+trunk+dune: expire_in: 1 week allow_failure: true +test-suite:base+async: + <<: *test-suite-template + dependencies: + - build:base + variables: + COQFLAGS: "-async-proofs on" + validate:base: <<: *validate-template dependencies: @@ -544,8 +551,12 @@ plugin:ci-mtac2: plugin:ci-paramcoq: <<: *ci-template -plugin:ci-plugin_tutorial: - <<: *ci-template +plugin:plugin-tutorial: + stage: test + dependencies: [] + script: + - ./configure -local -warn-error yes + - make -j "$NJOBS" plugin-tutorial plugin:ci-quickchick: <<: *ci-template-flambda diff --git a/CHANGES.md b/CHANGES.md index 6789bc038e..ae67eb5d1b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -93,6 +93,9 @@ Vernacular commands - The naming scheme for anonymous binders in a `Theorem` has changed to avoid conflicts with explicitly named binders. +- Computation of implicit arguments now properly handles local definitions in the + binders for an `Instance`. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: @@ -61,7 +61,8 @@ FIND_SKIP_DIRS:='(' \ -name 'user-contrib' -o \ -name 'test-suite' -o \ -name '.opamcache' -o \ - -name '.coq-native' \ + -name '.coq-native' -o \ + -name 'plugin_tutorial' \ ')' -prune -o define find @@ -191,7 +192,7 @@ META.coq: META.coq.in # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean plugin-tutorialclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean @@ -237,7 +238,7 @@ docclean: rm -f doc/coq.tex rm -rf doc/sphinx/_build -archclean: clean-ide optclean voclean +archclean: clean-ide optclean voclean plugin-tutorialclean rm -rf _build rm -f $(ALLSTDLIB).* @@ -278,6 +279,9 @@ timingclean: -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + +plugin-tutorialclean: + +$(MAKE) -C $(PLUGINTUTO) clean + # Ensure that every compiled file around has a known source file. # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. diff --git a/Makefile.ci b/Makefile.ci index 84be169f57..b8bff98f5f 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -36,7 +36,6 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ - ci-plugin_tutorial \ ci-quickchick \ ci-relation-algebra \ ci-sf \ diff --git a/Makefile.common b/Makefile.common index 9f7ed9d46e..2dced04967 100644 --- a/Makefile.common +++ b/Makefile.common @@ -168,6 +168,8 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) ALLSTDLIB := test-suite/misc/universes/all_stdlib +PLUGINTUTO := doc/plugin_tutorial + # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.doc b/Makefile.doc index 9e6ec4955a..48cdcebddb 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -89,6 +89,10 @@ stdlib: \ full-stdlib: \ doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf +.PHONY: plugin-tutorial +plugin-tutorial: states tools + +$(MAKE) COQBIN=$(PWD)/bin/ -C $(PLUGINTUTO) + ###################################################################### ### Implicit rules ###################################################################### @@ -1,6 +1,7 @@ # Coq -[](https://gitlab.com/coq/coq/commits/master) +[](https://gitlab.com/coq/coq/commits/master) +[](https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master) [](https://travis-ci.org/coq/coq/builds) [](https://ci.appveyor.com/project/coq/coq/branch/master) [](https://gitter.im/coq/coq) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e74a7853b9..8dee465cf4 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -150,6 +150,13 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## +# fiat_crypto_legacy +######################################################################## +: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" +: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" + +######################################################################## # coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" @@ -233,13 +240,6 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## -# plugin_tutorial -######################################################################## -: "${plugin_tutorial_CI_REF:=master}" -: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" -: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" - -######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index 6bf3138346..2af4b58201 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -4,11 +4,11 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" FORCE_GIT=1 -git_download fiat_crypto +git_download fiat_crypto_legacy fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ +( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ ./etc/ci/remove_autogenerated.sh && \ make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-plugin_tutorial.sh b/dev/ci/ci-plugin_tutorial.sh deleted file mode 100755 index 6c26a71a21..0000000000 --- a/dev/ci/ci-plugin_tutorial.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download plugin_tutorial - -( cd "${CI_BUILD_DIR}/plugin_tutorial" && \ - pushd tuto0 && make && popd && \ - pushd tuto1 && make && popd && \ - pushd tuto2 && make && popd && \ - pushd tuto3 && make && popd ) diff --git a/doc/plugin_tutorial/.gitignore b/doc/plugin_tutorial/.gitignore new file mode 100644 index 0000000000..3e4978fac4 --- /dev/null +++ b/doc/plugin_tutorial/.gitignore @@ -0,0 +1,13 @@ +*.ml*.d +*.cm[ixt]* +Makefile.coq* +*~ +*.[ao] +.coqdeps.d +*.vo +*.glob +*.aux +*/*/.merlin + +# by convention g_foo.ml is generated +g_*.ml diff --git a/doc/plugin_tutorial/.travis.yml b/doc/plugin_tutorial/.travis.yml new file mode 100644 index 0000000000..556e0ac45a --- /dev/null +++ b/doc/plugin_tutorial/.travis.yml @@ -0,0 +1,38 @@ +dist: trusty +sudo: required +language: generic + +services: + - docker + +env: + global: + - NJOBS="2" + - CONTRIB_NAME="plugin_tutorials" + matrix: + - COQ_IMAGE="coqorg/coq:dev" + +install: | + # Prepare the COQ container + docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/$CONTRIB_NAME -w /home/coq/$CONTRIB_NAME ${COQ_IMAGE} + docker exec COQ /bin/bash --login -c " + # This bash script is double-quoted to interpolate Travis CI env vars: + echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\" + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex # -e = exit on failure; -x = trace for debug + opam list + " +script: +- echo -e "${ANSI_YELLOW}Building $CONTRIB_NAME...${ANSI_RESET}" && echo -en 'travis_fold:start:testbuild\\r' +- | + docker exec COQ /bin/bash --login -c " + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex + sudo chown -R coq:coq /home/coq/$CONTRIB_NAME + ( cd tuto0 && make ) + ( cd tuto1 && make ) + ( cd tuto2 && make ) + ( cd tuto3 && make ) + " +- docker stop COQ # optional +- echo -en 'travis_fold:end:testbuild\\r' diff --git a/doc/plugin_tutorial/LICENSE b/doc/plugin_tutorial/LICENSE new file mode 100644 index 0000000000..cf1ab25da0 --- /dev/null +++ b/doc/plugin_tutorial/LICENSE @@ -0,0 +1,24 @@ +This is free and unencumbered software released into the public domain. + +Anyone is free to copy, modify, publish, use, compile, sell, or +distribute this software, either in source code form or as a compiled +binary, for any purpose, commercial or non-commercial, and by any +means. + +In jurisdictions that recognize copyright laws, the author or authors +of this software dedicate any and all copyright interest in the +software to the public domain. We make this dedication for the benefit +of the public at large and to the detriment of our heirs and +successors. We intend this dedication to be an overt act of +relinquishment in perpetuity of all present and future rights to this +software under copyright law. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR +OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, +ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +OTHER DEALINGS IN THE SOFTWARE. + +For more information, please refer to <http://unlicense.org> diff --git a/doc/plugin_tutorial/Makefile b/doc/plugin_tutorial/Makefile new file mode 100644 index 0000000000..7f1833fadd --- /dev/null +++ b/doc/plugin_tutorial/Makefile @@ -0,0 +1,21 @@ + +TUTOS:= \ + tuto0 \ + tuto1 \ + tuto2 \ + tuto3 + +all: $(TUTOS) + +.PHONY: $(TUTOS) all + +$(TUTOS): %: + +$(MAKE) -C $@ + +CLEANS:=$(addsuffix -clean, $(TUTOS)) +.PHONY: clean $(CLEANS) + +clean: $(CLEANS) + +%-clean: + +$(MAKE) -C $* clean diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md new file mode 100644 index 0000000000..f82edb2352 --- /dev/null +++ b/doc/plugin_tutorial/README.md @@ -0,0 +1,86 @@ +How to write plugins in Coq +=========================== + # Working environment : merlin, tuareg (open question) + + ## OCaml & related tools + + These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) + +```shell +opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2 +eval `opam config env --root=$PWD/CIW2018` +opam install camlp5 ocamlfind num # Coq's dependencies +opam install lablgtk # Coqide's dependencies (optional) +opam install merlin # prints instructions for vim and emacs +``` + + ## Coq + +```shell +git clone git@github.com:coq/coq.git +cd coq +./configure -profile devel +make -j2 +cd .. +export PATH=$PWD/coq/bin:$PATH +``` + + ## This tutorial + +```shell +git clone git@github.com:ybertot/plugin_tutorials.git +cd plugin_tutorials/tuto0 +make .merlin # run before opening .ml files in your editor +make # build +``` + + + + # tuto0 : basics of project organization + package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` + - Example of syntax to add a new toplevel command + - Example of function call to print a simple message + - Example of syntax to add a simple tactic + (that does nothing and prints a message) + - To use it: + +```bash + cd tuto0; make + coqtop -I src -R theories Tuto0 +``` + + In the Coq session type: +```coq + Require Import Tuto0.Loader. HelloWorld. +``` + + # tuto1 : Ocaml to Coq communication + Explore the memory of Coq, modify it + - Commands that take arguments: strings, symbols, expressions of the calculus of constructions + - Commands that interact with type-checking in Coq + - A command that adds a new definition or theorem + - A command that uses a name and exploits the existing definitions + or theorems + - A command that exploits an existing ongoing proof + - A command that defines a new tactic + + Compilation and loading must be performed as for `tuto0`. + + # tuto2 : Ocaml to Coq communication + A more step by step introduction to writing commands + - Explanation of the syntax of entries + - Adding a new type to and parsing to the available choices + - Handling commands that store information in user-chosen registers and tables + + Compilation and loading must be performed as for `tuto1`. + + # tuto3 : manipulating terms of the calculus of constructions + Manipulating terms, inside commands and tactics. + - Obtaining existing values from memory + - Composing values + - Verifying types + - Using these terms in commands + - Using these terms in tactics + - Automatic proofs without tactics using type classes and canonical structures + + compilation and loading must be performed as for `tuto0`. diff --git a/doc/plugin_tutorial/tuto0/Makefile b/doc/plugin_tutorial/tuto0/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto0/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto0/_CoqProject b/doc/plugin_tutorial/tuto0/_CoqProject new file mode 100644 index 0000000000..76368e3ac7 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/_CoqProject @@ -0,0 +1,10 @@ +-R theories/ Tuto0 +-I src + +theories/Loader.v +theories/Demo.v + +src/tuto0_main.ml +src/tuto0_main.mli +src/g_tuto0.mlg +src/tuto0_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune new file mode 100644 index 0000000000..79d561061d --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto0_plugin) + (public_name coq.plugins.tutorial.p0) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto0.ml) + (deps (:pp-file g_tuto0.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg new file mode 100644 index 0000000000..5c633fe862 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg @@ -0,0 +1,18 @@ +DECLARE PLUGIN "tuto0_plugin" + +{ + +open Pp +open Ltac_plugin + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) } +END + +TACTIC EXTEND hello_world_tactic +| [ "hello_world" ] -> + { let _ = Feedback.msg_notice (str Tuto0_main.message) in + Tacticals.New.tclIDTAC } +END diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.ml b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml new file mode 100644 index 0000000000..93a807a800 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml @@ -0,0 +1 @@ +let message = "Hello world!" diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.mli b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli new file mode 100644 index 0000000000..846af3ed8c --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli @@ -0,0 +1 @@ +val message : string diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack new file mode 100644 index 0000000000..73be1bb561 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack @@ -0,0 +1,2 @@ +Tuto0_main +G_tuto0 diff --git a/doc/plugin_tutorial/tuto0/theories/Demo.v b/doc/plugin_tutorial/tuto0/theories/Demo.v new file mode 100644 index 0000000000..bdc61986af --- /dev/null +++ b/doc/plugin_tutorial/tuto0/theories/Demo.v @@ -0,0 +1,8 @@ +From Tuto0 Require Import Loader. + +HelloWorld. + +Lemma test : True. +Proof. +hello_world. +Abort. diff --git a/doc/plugin_tutorial/tuto0/theories/Loader.v b/doc/plugin_tutorial/tuto0/theories/Loader.v new file mode 100644 index 0000000000..7bce38382b --- /dev/null +++ b/doc/plugin_tutorial/tuto0/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto0_plugin". diff --git a/doc/plugin_tutorial/tuto1/Makefile b/doc/plugin_tutorial/tuto1/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto1/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject new file mode 100644 index 0000000000..585d1360be --- /dev/null +++ b/doc/plugin_tutorial/tuto1/_CoqProject @@ -0,0 +1,13 @@ +-R theories Tuto1 +-I src + +theories/Loader.v + +src/simple_check.mli +src/simple_check.ml +src/simple_declare.mli +src/simple_declare.ml +src/simple_print.ml +src/simple_print.mli +src/g_tuto1.mlg +src/tuto1_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune new file mode 100644 index 0000000000..cf9c674b14 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto1_plugin) + (public_name coq.plugins.tutorial.p1) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto1.ml) + (deps (:pp-file g_tuto1.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg new file mode 100644 index 0000000000..4df284d2d9 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -0,0 +1,154 @@ +DECLARE PLUGIN "tuto1_plugin" + +{ + +(* If we forget this line and include our own tactic definition using + TACTIC EXTEND, as below, then we get the strange error message + no implementation available for Tacentries, only when compiling + theories/Loader.v +*) +open Ltac_plugin +open Attributes +open Pp +(* This module defines the types of arguments to be used in the + EXTEND directives below, for example the string one. *) +open Stdarg + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "Hello" string(s) ] -> + { Feedback.msg_notice (strbrk "Hello " ++ str s) } +END + +(* reference is allowed as a syntactic entry, but so are all the entries + found the signature of module Prim in file coq/parsing/pcoq.mli *) + +VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY +| [ "HelloAgain" reference(r)] -> +(* The function Ppconstr.pr_qualid was found by searching all mli files + for a function of type qualid -> Pp.t *) + { Feedback.msg_notice + (strbrk "Hello again " ++ Ppconstr.pr_qualid r)} +END + +(* According to parsing/pcoq.mli, e has type constr_expr *) +(* this type is defined in pretyping/constrexpr.ml *) +(* Question for the developers: why is the file constrexpr.ml and not + constrexpr.mli --> Easier for packing the software in components. *) +VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY +| [ "Cmd1" constr(e) ] -> + { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") } +END + +(* The next step is to make something of parsed expression. + Interesting information in interp/constrintern.mli *) + +(* There are several phases of transforming a parsed expression into + the final internal data-type (constr). There exists a collection of + functions that combine all the phases *) + +VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY +| [ "Cmd2" constr(e) ] -> + { let _ = Constrintern.interp_constr + (Global.env()) + (* Make sure you don't use Evd.empty here, as this does not + check consistency with existing universe constraints. *) + (Evd.from_env (Global.env())) e in + Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") } +END + +(* This is to show what happens when typing in an empty environment + with an empty evd. + Question for the developers: why does "Cmd3 (fun x : nat => x)." + raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *) + +VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY +| [ "Cmd3" constr(e) ] -> + { let _ = Constrintern.interp_constr Environ.empty_env + Evd.empty e in + Feedback.msg_notice + (strbrk "Cmd3 accepted something in the empty context")} +END + +(* When adding a definition, we have to be careful that just + the operation of constructing a well-typed term may already change + the environment, at the level of universe constraints (which + are recorded in the evd component). The function + Constrintern.interp_constr ignores this side-effect, so it should + not be used here. *) + +(* Looking at the interface file interp/constrintern.ml4, I lost + some time because I did not see that the "constr" type appearing + there was "EConstr.constr" and not "Constr.constr". *) + +VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF +| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + Simple_declare.packed_declare_definition ~poly i v } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd5" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (_, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check1 v)) } +END + +VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY +| [ "Cmd6" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let evd, ty = Simple_check.simple_check2 v in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd ty) } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd7" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (a, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check3 v)) } +END + +(* This command takes a name and return its value. It does less + than Print, because it fails on constructors, axioms, and inductive types. + This should be improved, because the error message is an anomaly. + Anomalies should never appear even when using a command outside of its + intended use. *) +VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY +| [ "Cmd8" reference(r) ] -> + { let env = Global.env() in + let evd = Evd.from_env env in + Feedback.msg_notice + (Printer.pr_econstr_env env evd + (EConstr.of_constr + (Simple_print.simple_body_access (Nametab.global r)))) } +END + +TACTIC EXTEND my_intro +| [ "my_intro" ident(i) ] -> + { Tactics.introduction i } +END + +(* if one write this: + VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY + it gives an error message that is basically impossible to understand. *) + +VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY +| [ "Cmd9" ] -> + { let p = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in + let pprf = Proof.partial_proof p in + Feedback.msg_notice + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } +END diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml new file mode 100644 index 0000000000..1f636c531a --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -0,0 +1,32 @@ +let simple_check1 value_with_constraints = + begin + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This is reverse engineered from vernacentries.ml *) +(* The point of renaming is to make sure the bound names printed by Check + can be re-used in `apply with` tactics that use bound names to + refer to arguments. *) + let j = Termops.on_judgment EConstr.of_constr + (Arguments_renaming.rename_typing (Global.env()) + (EConstr.to_constr evd evalue)) in + let {Environ.uj_type=x}=j in x + end + +let simple_check2 value_with_constraints = + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This version should be preferred if bound variable names are not so + important, you want to really verify that the input is well-typed, + and if you want to obtain the type. *) +(* Note that the output value is a pair containing a new evar_map: + typing will fill out blanks in the term by add evar bindings. *) + Typing.type_of (Global.env()) evd evalue + +let simple_check3 value_with_constraints = + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This version should be preferred if bound variable names are not so + important and you already expect the input to have been type-checked + before. Set ~lax to false if you want an anomaly to be raised in + case of a type error. Otherwise a ReTypeError exception is raised. *) + Retyping.get_type_of ~lax:true (Global.env()) evd evalue diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli new file mode 100644 index 0000000000..bcf1bf56cf --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli @@ -0,0 +1,8 @@ +val simple_check1 : + EConstr.constr Evd.in_evar_universe_context -> EConstr.constr + +val simple_check2 : + EConstr.constr Evd.in_evar_universe_context -> Evd.evar_map * EConstr.constr + +val simple_check3 : + EConstr.constr Evd.in_evar_universe_context -> EConstr.constr diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml new file mode 100644 index 0000000000..9d10a8ba72 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -0,0 +1,24 @@ +(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) +let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = + let sigma = Evd.minimize_universes sigma in + let body = EConstr.to_constr sigma body in + let tyopt = Option.map (EConstr.to_constr sigma) tyopt in + let uvars_fold uvars c = + Univ.LSet.union uvars (Vars.universes_of_constr c) in + let uvars = List.fold_left uvars_fold Univ.LSet.empty + (Option.List.cons tyopt [body]) in + let sigma = Evd.restrict_universe_context sigma uvars in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let ubinders = Evd.universe_binders sigma in + let ce = Declare.definition_entry ?types:tyopt ~univs body in + DeclareDef.declare_definition ident k ce ubinders imps ~hook + +let packed_declare_definition ~poly ident value_with_constraints = + let body, ctx = value_with_constraints in + let sigma = Evd.from_ctx ctx in + let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in + let udecl = UState.default_univ_decl in + let nohook = Lemmas.mk_hook (fun _ x -> ()) in + ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) + +(* But this definition cannot be undone by Reset ident *) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.mli b/doc/plugin_tutorial/tuto1/src/simple_declare.mli new file mode 100644 index 0000000000..fd74e81526 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli @@ -0,0 +1,5 @@ +open Names +open EConstr + +val packed_declare_definition : + poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml new file mode 100644 index 0000000000..cfc38ff9c9 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -0,0 +1,17 @@ +(* A more advanced example of how to explore the structure of terms of + type constr is given in the coq-dpdgraph plugin. *) + +let simple_body_access gref = + match gref with + | Globnames.VarRef _ -> + failwith "variables are not covered in this example" + | Globnames.IndRef _ -> + failwith "inductive types are not covered in this example" + | Globnames.ConstructRef _ -> + failwith "constructors are not covered in this example" + | Globnames.ConstRef cst -> + let cb = Environ.lookup_constant cst (Global.env()) in + match Global.body_of_constant_body cb with + | Some(e, _) -> e + | None -> failwith "This term has no value" + diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.mli b/doc/plugin_tutorial/tuto1/src/simple_print.mli new file mode 100644 index 0000000000..254b56ff79 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_print.mli @@ -0,0 +1 @@ +val simple_body_access : Names.GlobRef.t -> Constr.constr diff --git a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack new file mode 100644 index 0000000000..a797a509e0 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack @@ -0,0 +1,4 @@ +Simple_check +Simple_declare +Simple_print +G_tuto1 diff --git a/doc/plugin_tutorial/tuto1/theories/Loader.v b/doc/plugin_tutorial/tuto1/theories/Loader.v new file mode 100644 index 0000000000..6e8e308b3f --- /dev/null +++ b/doc/plugin_tutorial/tuto1/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto1_plugin". diff --git a/doc/plugin_tutorial/tuto2/Makefile b/doc/plugin_tutorial/tuto2/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto2/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto2/_CoqProject b/doc/plugin_tutorial/tuto2/_CoqProject new file mode 100644 index 0000000000..cf9cb5cc26 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/_CoqProject @@ -0,0 +1,6 @@ +-R theories/ Tuto +-I src + +theories/Test.v +src/demo.mlg +src/demo_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto2/src/.gitignore b/doc/plugin_tutorial/tuto2/src/.gitignore new file mode 100644 index 0000000000..5b1b6a902e --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/.gitignore @@ -0,0 +1 @@ +/demo.ml diff --git a/doc/plugin_tutorial/tuto2/src/demo.mlg b/doc/plugin_tutorial/tuto2/src/demo.mlg new file mode 100644 index 0000000000..966c05acdc --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/demo.mlg @@ -0,0 +1,375 @@ +(* -------------------------------------------------------------------------- *) +(* *) +(* Initial ritual dance *) +(* *) +(* -------------------------------------------------------------------------- *) + +DECLARE PLUGIN "demo_plugin" + +(* + Use this macro before any of the other OCaml macros. + + Each plugin has a unique name. + We have decided to name this plugin as "demo_plugin". + That means that: + + (1) If we want to load this particular plugin to Coq toplevel, + we must use the following command. + + Declare ML Module "demo_plugin". + + (2) The above command will succeed only if there is "demo_plugin.cmxs" + in some of the directories that Coq is supposed to look + (i.e. the ones we specified via "-I ..." command line options). + + (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in + "demo_plugin.cmxs". + + (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .mlg files + are listed in the "_CoqProject" file. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY +| [ "Cmd1" ] -> { () } +END + +(* + These: + + VERNAC COMMAND EXTEND + + and + + END + + mark the beginning and the end of the definition of a new Vernacular command. + + Cmd1 is a unique identifier (which must start with an upper-case letter) + associated with the new Vernacular command we are defining. + + CLASSIFIED AS QUERY tells Coq that the new Vernacular command: + - changes neither the global environment + - nor does it modify the plugin's state. + + If the new command could: + - change the global environment + - or modify a plugin's state + then one would have to use CLASSIFIED AS SIDEFF instead. + + This: + + [ "Cmd1" ] -> { () } + + defines: + - the parsing rule + - the interpretation rule + + The parsing rule and the interpretation rule are separated by -> token. + + The parsing rule, in this case, is: + + [ "Cmd1" ] + + By convention, all vernacular command start with an upper-case letter. + + The [ and ] characters mark the beginning and the end of the parsing rule. + The parsing rule itself says that the syntax of the newly defined command + is composed from a single terminal Cmd1. + + The interpretation rule, in this case, is: + + { () } + + Similarly to the case of the parsing rule, + { and } characters mark the beginning and the end of the interpretation rule. + In this case, the following Ocaml expression: + + () + + defines the effect of the Vernacular command we have just defined. + That is, it behaves is no-op. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some terminal parameters? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY +| [ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> { () } +END + +(* + As shown above, the Vernacular command can be composed from + any number of terminals. + + By convention, each of these terminals starts with an upper-case letter. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some non-terminal parameter? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Stdarg + +} + +VERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY +| [ "Cmd3" int(i) ] -> { () } +END + +(* + This: + + open Stdarg + + is needed as some identifiers in the Ocaml code generated by the + + VERNAC COMMAND EXTEND ... END + + macros are not fully qualified. + + This: + + int(i) + + means that the new command is expected to be followed by an integer. + The integer is bound in the parsing rule to variable i. + This variable i then can be used in the interpretation rule. + + To see value of which Ocaml types can be bound this way, + look at the wit_* function declared in interp/stdarg.mli + (in the Coq's codebase). + + If we drop the wit_ prefix, we will get the token + that we can use in the parsing rule. + That is, since there exists wit_int, we know that + we can write: + + int(i) + + By looking at the signature of the wit_int function: + + val wit_int : int uniform_genarg_type + + we also know that variable i will have the type int. + + The types of wit_* functions are either: + + 'c uniform_genarg_type + + or + + ('a,'b,'c) genarg_type + + In both cases, the bound variable will have type 'c. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with variable number of arguments? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY +| [ "Cmd4" int_list(l) ] -> { () } +END + +(* + This: + + int_list(l) + + means that the new Vernacular command is expected to be followed + by a (whitespace separated) list of integers. + This list of integers is bound to the indicated l. + + In this case, as well as in the cases we point out below, instead of int + in int_list we could use any other supported type, e.g. ident, bool, ... + + To see which other Ocaml type constructors (in addition to list) + are supported, have a look at the parse_user_entry function defined + in grammar/q_util.mlp file. + + E.g.: + - ne_int_list(x) would represent a non-empty list of integers, + - int_list(x) would represent a list of integers, + - int_opt(x) would represent a value of type int option, + - ··· +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command that takes values of a custom type? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Ltac_plugin + +} + +(* + If we want to avoid a compilation failure + + "no implementation available for Tacenv" + + then we have to open the Ltac_plugin module. +*) + +(* + Pp module must be opened because some of the macros that are part of the API + do not expand to fully qualified names. +*) + +{ + +type type_5 = Foo_5 | Bar_5 + +} + +(* + We define a type of values that we want to pass to our Vernacular command. +*) + +(* + By default, we are able to define new Vernacular commands that can take + parameters of some of the supported types. Which types are supported, + that was discussed earlier. + + If we want to be able to define Vernacular command that takes parameters + of a type that is not supported by default, we must use the following macro: +*) + +{ + +open Pp + +} + +VERNAC ARGUMENT EXTEND custom5 +| [ "Foo_5" ] -> { Foo_5 } +| [ "Bar_5" ] -> { Bar_5 } +END + +(* + where: + + custom5 + + indicates that, from now on, in our parsing rules we can write: + + custom5(some_variable) + + in those places where we expect user to provide an input + that can be parsed by the parsing rules above + (and interpreted by the interpretations rules above). +*) + +(* Here: *) + +VERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY +| [ "Cmd5" custom5(x) ] -> { () } +END + +(* + we define a new Vernacular command whose parameters, provided by the user, + can be mapped to values of type_5. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to give a feedback to the user? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY +| [ "Cmd6" ] -> { Feedback.msg_notice (Pp.str "Everything is awesome!") } +END + +(* + The following functions: + + - Feedback.msg_info : Pp.t -> unit + - Feedback.msg_notice : Pp.t -> unit + - Feedback.msg_warning : Pp.t -> unit + - Feedback.msg_error : Pp.t -> unit + - Feedback.msg_debug : Pp.t -> unit + + enable us to give user a textual feedback. + + Pp module enable us to represent and construct pretty-printing instructions. + The concepts defined and the services provided by the Pp module are in + various respects related to the concepts and services provided + by the Format module that is part of the Ocaml standard library. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to implement a Vernacular command with (undoable) side-effects? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Summary.Local + +} + +(* + By opening Summary.Local module we shadow the original functions + that we traditionally use for implementing stateful behavior. + + ref + ! + := + + are now shadowed by their counterparts in Summary.Local. *) + +{ + +let counter = ref ~name:"counter" 0 + +} + +VERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF +| [ "Cmd7" ] -> { counter := succ !counter; + Feedback.msg_notice (Pp.str "counter = " ++ Pp.str (string_of_int (!counter))) } +END + +TACTIC EXTEND tactic1 +| [ "tactic1" ] -> { Proofview.tclUNIT () } +END + +(* ---- *) + +{ + +type custom = Foo_2 | Bar_2 + +let pr_custom _ _ _ = function + | Foo_2 -> Pp.str "Foo_2" + | Bar_2 -> Pp.str "Bar_2" + +} + +ARGUMENT EXTEND custom2 PRINTED BY { pr_custom } +| [ "Foo_2" ] -> { Foo_2 } +| [ "Bar_2" ] -> { Bar_2 } +END + +TACTIC EXTEND tactic2 +| [ "tactic2" custom2(x) ] -> { Proofview.tclUNIT () } +END diff --git a/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack new file mode 100644 index 0000000000..4f0b8480b5 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack @@ -0,0 +1 @@ +Demo diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune new file mode 100644 index 0000000000..f2bc405455 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto2_plugin) + (public_name coq.plugins.tutorial.p2) + (libraries coq.plugins.ltac)) + +(rule + (targets demo.ml) + (deps (:pp-file demo.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto2/theories/Test.v b/doc/plugin_tutorial/tuto2/theories/Test.v new file mode 100644 index 0000000000..38e83bfff1 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Test.v @@ -0,0 +1,19 @@ +Declare ML Module "demo_plugin". + +Cmd1. +Cmd2 With Some Terminal Parameters. +Cmd3 42. +Cmd4 100 200 300 400. +Cmd5 Foo_5. +Cmd5 Bar_5. +Cmd6. +Cmd7. +Cmd7. +Cmd7. + +Goal True. +Proof. + tactic1. + tactic2 Foo_2. + tactic2 Bar_2. +Abort. diff --git a/doc/plugin_tutorial/tuto3/Makefile b/doc/plugin_tutorial/tuto3/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto3/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto3/_CoqProject b/doc/plugin_tutorial/tuto3/_CoqProject new file mode 100644 index 0000000000..e2a60a430f --- /dev/null +++ b/doc/plugin_tutorial/tuto3/_CoqProject @@ -0,0 +1,12 @@ +-R theories Tuto3 +-I src + +theories/Data.v +theories/Loader.v + +src/tuto_tactic.ml +src/tuto_tactic.mli +src/construction_game.ml +src/construction_game.mli +src/g_tuto3.mlg +src/tuto3_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml new file mode 100644 index 0000000000..9d9f894e18 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml @@ -0,0 +1,186 @@ +open Pp + +let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] + +let example_sort evd = +(* creating a new sort requires that universes should be recorded + in the evd datastructure, so this datastructure also needs to be + passed around. *) + let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let new_type = EConstr.mkSort s in + evd, new_type + +let c_one evd = +(* In the general case, global references may refer to universe polymorphic + objects, and their universe has to be made afresh when creating an instance. *) + let gr_S = + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in +(* the long name of "S" was found with the command "About S." *) + let gr_O = + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + let evd, c_O = Evarutil.new_global evd gr_O in + let evd, c_S = Evarutil.new_global evd gr_S in +(* Here is the construction of a new term by applying functions to argument. *) + evd, EConstr.mkApp (c_S, [| c_O |]) + +let dangling_identity env evd = +(* I call this a dangling identity, because it is not polymorph, but + the type on which it applies is left unspecified, as it is + represented by an existential variable. The declaration for this + existential variable needs to be added in the evd datastructure. *) + let evd, type_type = example_sort evd in + let evd, arg_type = Evarutil.new_evar env evd type_type in +(* Notice the use of a De Bruijn index for the inner occurrence of the + bound variable. *) + evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type, + EConstr.mkRel 1) + +let dangling_identity2 env evd = +(* This example uses directly a function that produces an evar that + is meant to be a type. *) + let evd, (arg_type, type_type) = + Evarutil.new_type_evar env evd Evd.univ_rigid in + evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type, + EConstr.mkRel 1) + +let example_sort_app_lambda () = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c_v = c_one evd in +(* dangling_identity and dangling_identity2 can be used interchangeably here *) + let evd, c_f = dangling_identity2 env evd in + let c_1 = EConstr.mkApp (c_f, [| c_v |]) in + let _ = Feedback.msg_notice + (Printer.pr_econstr_env env evd c_1) in + (* type verification happens here. Type verification will update + existential variable information in the evd part. *) + let evd, the_type = Typing.type_of env evd c_1 in +(* At display time, you will notice that the system knows about the + existential variable being instantiated to the "nat" type, even + though c_1 still contains the meta-variable. *) + Feedback.msg_notice + ((Printer.pr_econstr_env env evd c_1) ++ + str " has type " ++ + (Printer.pr_econstr_env env evd the_type)) + + +let c_S evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in + Evarutil.new_global evd gr + +let c_O evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + Evarutil.new_global evd gr + +let c_E evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in + Evarutil.new_global evd gr + +let c_D evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in + Evarutil.new_global evd gr + +let c_Q evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in + Evarutil.new_global evd gr + +let c_R evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in + Evarutil.new_global evd gr + +let c_N evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in + Evarutil.new_global evd gr + +let c_C evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in + Evarutil.new_global evd gr + +let c_F evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in + Evarutil.new_global evd gr + +let c_P evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in + Evarutil.new_global evd gr + +(* If c_S was universe polymorphic, we should have created a new constant + at each iteration of buildup. *) +let mk_nat evd n = + let evd, c_S = c_S evd in + let evd, c_O = c_O evd in + let rec buildup = function + | 0 -> c_O + | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in + if n <= 0 then evd, c_O else evd, buildup n + +let example_classes n = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c_n = mk_nat evd n in + let evd, n_half = mk_nat evd (n / 2) in + let evd, c_N = c_N evd in + let evd, c_div = c_D evd in + let evd, c_even = c_E evd in + let evd, c_Q = c_Q evd in + let evd, c_R = c_R evd in + let arg_type = EConstr.mkApp (c_even, [| c_n |]) in + let evd0 = evd in + let evd, instance = Evarutil.new_evar env evd arg_type in + let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let evd, the_type = Typing.type_of env evd c_half in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let proved_equality = + EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast, + EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in +(* This is where we force the system to compute with type classes. *) +(* Question to coq developers: why do we pass two evd arguments to + solve_remaining_evars? Is the choice of evd0 relevant here? *) + let evd = Pretyping.solve_remaining_evars + (Pretyping.default_inference_flags true) env evd ~initial:evd0 in + let evd, final_type = Typing.type_of env evd proved_equality in + Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality) + +(* This function, together with definitions in Data.v, shows how to + trigger automatic proofs at the time of typechecking, based on + canonical structures. + + n is a number for which we want to find the half (and a proof that + this half is indeed the half) +*) +let example_canonical n = + let env = Global.env () in + let evd = Evd.from_env env in +(* Construct a natural representation of this integer. *) + let evd, c_n = mk_nat evd n in +(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *) + let evd, c_N = c_N evd in + let evd, c_F = c_F evd in + let evd, c_R = c_R evd in + let evd, c_C = c_C evd in + let evd, c_P = c_P evd in +(* the last argument of C *) + let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in +(* Now we build two existential variables, for the value of the half and for + the "S_ev" structure that triggers the proof search. *) + let evd, ev1 = Evarutil.new_evar env evd c_N in +(* This is the type for the second existential variable *) + let csev = EConstr.mkApp (c_F, [| ev1 |]) in + let evd, ev2 = Evarutil.new_evar env evd csev in +(* Now we build the C structure. *) + let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in +(* Type-checking this term will compute values for the existential variables *) + let evd, final_type = Typing.type_of env evd test_term in +(* The computed type has two parameters, the second one is the proof. *) + let value = match EConstr.kind evd final_type with + | Constr.App(_, [| _; the_half |]) -> the_half + | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in +(* I wish for a nicer way to get the value of ev2 in the evar_map *) + let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in + let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in + let evd, the_statement = Typing.type_of env evd the_prf in + Feedback.msg_notice + (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++ + Printer.pr_econstr_env env evd the_statement) diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.mli b/doc/plugin_tutorial/tuto3/src/construction_game.mli new file mode 100644 index 0000000000..1832ed6630 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/construction_game.mli @@ -0,0 +1,4 @@ +val dangling_identity : Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.t +val example_sort_app_lambda : unit -> unit +val example_classes : int -> unit +val example_canonical : int -> unit diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune new file mode 100644 index 0000000000..ba6d8b288f --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/dune @@ -0,0 +1,10 @@ +(library + (name tuto3_plugin) + (public_name coq.plugins.tutorial.p3) + (flags :standard -warn-error -3) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto3.ml) + (deps (:pp-file g_tuto3.mlg)) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg new file mode 100644 index 0000000000..82ba45726e --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg @@ -0,0 +1,46 @@ +DECLARE PLUGIN "tuto3_plugin" + +{ + +open Ltac_plugin + +open Construction_game + +(* This one is necessary, to avoid message about missing wit_string *) +open Stdarg + +} + +VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY +| [ "Tuto3_1" ] -> + { let env = Global.env () in + let evd = Evd.from_env env in + let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let new_type_2 = EConstr.mkSort s in + let evd, _ = + Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in + Feedback.msg_notice + (Printer.pr_econstr_env env evd new_type_2) } +END + +VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY +| [ "Tuto3_2" ] -> { example_sort_app_lambda () } +END + +TACTIC EXTEND collapse_hyps +| [ "pack" "hypothesis" ident(i) ] -> + { Tuto_tactic.pack_tactic i } +END + +(* More advanced examples, where automatic proof happens but + no tactic is being called explicitely. The first one uses + type classes. *) +VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY +| [ "Tuto3_3" int(n) ] -> { example_classes n } +END + +(* The second one uses canonical structures. *) +VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY +| [ "Tuto3_4" int(n) ] -> { example_canonical n } +END + diff --git a/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack new file mode 100644 index 0000000000..f4645ad7ed --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack @@ -0,0 +1,3 @@ +Construction_game +Tuto_tactic +G_tuto3 diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml new file mode 100644 index 0000000000..8f2c387d09 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -0,0 +1,143 @@ +open Proofview + +let constants = ref ([] : EConstr.t list) + +(* This is a pattern to collect terms from the Coq memory of valid terms + and proofs. This pattern extends all the way to the definition of function + c_U *) +let collect_constants () = + if (!constants = []) then + let open EConstr in + let open UnivGen in + let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] in + let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in + let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in + let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in + let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in + let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in + constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x)) + [gr_H; gr_M; gr_R; gr_P; gr_U]; + !constants + else + !constants + +let c_H () = + match collect_constants () with + it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pack" + +let c_M () = + match collect_constants () with + _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pack_marker" + +let c_R () = + match collect_constants () with + _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pair" + +let c_P () = + match collect_constants () with + _ :: _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of prod" + +let c_U () = + match collect_constants () with + _ :: _ :: _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of prod" + +(* The following tactic is meant to pack an hypothesis when no other + data is already packed. + + The main difficulty in defining this tactic is to understand how to + construct the input expected by apply_in. *) +let package i = Goal.enter begin fun gl -> + Tactics.apply_in true false i + [(* this means that the applied theorem is not to be cleared. *) + None, (CAst.make (c_M (), + (* we don't specialize the theorem with extra values. *) + Tactypes.NoBindings))] + (* we don't destruct the result according to any intro_pattern *) + None + end + +(* This function is meant to observe a type of shape (f a) + and return the value a. *) + +(* Remark by Maxime: look for destApp combinator. *) +let unpack_type evd term = + let report () = + CErrors.user_err (Pp.str "expecting a packed type") in + match EConstr.kind evd term with + | Constr.App (_, [| ty |]) -> ty + | _ -> report () + +(* This function is meant to observe a type of shape + A -> pack B -> C and return A, B, C + but it is not used in the current version of our tactic. + It is kept as an example. *) +let two_lambda_pattern evd term = + let report () = + CErrors.user_err (Pp.str "expecting two nested implications") in +(* Note that pattern-matching is always done through the EConstr.kind function, + which only provides one-level deep patterns. *) + match EConstr.kind evd term with + (* Here we recognize the outer implication *) + | Constr.Prod (_, ty1, l1) -> + (* Here we recognize the inner implication *) + (match EConstr.kind evd l1 with + | Constr.Prod (n2, packed_ty2, deep_conclusion) -> + (* Here we recognized that the second type is an application *) + ty1, unpack_type evd packed_ty2, deep_conclusion + | _ -> report ()) + | _ -> report () + +(* In the environment of the goal, we can get the type of an assumption + directly by a lookup. The other solution is to call a low-cost retyping + function like *) +let get_type_of_hyp env id = + match EConstr.lookup_named id env with + | Context.Named.Declaration.LocalAssum (_, ty) -> ty + | _ -> CErrors.user_err (let open Pp in + str (Names.Id.to_string id) ++ + str " is not a plain hypothesis") + +let repackage i h_hyps_id = Goal.enter begin fun gl -> + let env = Goal.env gl in + let evd = Tacmach.New.project gl in + let concl = Tacmach.New.pf_concl gl in + let (ty1 : EConstr.t) = get_type_of_hyp env i in + let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in + let ty2 = unpack_type evd packed_ty2 in + let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in + let open EConstr in + let new_packed_value = + mkApp (c_R (), [| ty1; ty2; mkVar i; + mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in + Refine.refine ~typecheck:true begin fun evd -> + let evd, new_goal = Evarutil.new_evar env evd + (mkProd (Names.Name.Anonymous, + mkApp(c_H (), [| new_packed_type |]), + Vars.lift 1 concl)) in + evd, mkApp (new_goal, + [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |]) + end + end + +let pack_tactic i = + let h_hyps_id = (Names.Id.of_string "packed_hyps") in + Proofview.Goal.enter begin fun gl -> + let hyps = Environ.named_context_val (Proofview.Goal.env gl) in + if not (Termops.mem_named_context_val i hyps) then + (CErrors.user_err + (Pp.str ("no hypothesis named" ^ (Names.Id.to_string i)))) + else + if Termops.mem_named_context_val h_hyps_id hyps then + tclTHEN (repackage i h_hyps_id) + (tclTHEN (Tactics.clear [h_hyps_id; i]) + (Tactics.introduction h_hyps_id)) + else + tclTHEN (package i) + (tclTHEN (Tactics.rename_hyp [i, h_hyps_id]) + (Tactics.move_hyp h_hyps_id Logic.MoveLast)) + end diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli new file mode 100644 index 0000000000..dbf6cf48e2 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli @@ -0,0 +1,3 @@ +val two_lambda_pattern : + Evd.evar_map -> EConstr.t -> EConstr.t * EConstr.t * EConstr.t +val pack_tactic : Names.Id.t -> unit Proofview.tactic diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v new file mode 100644 index 0000000000..f7395d686b --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/Data.v @@ -0,0 +1,73 @@ + + +Inductive pack (A: Type) : Type := + packer : A -> pack A. + +Arguments packer {A}. + +Definition uncover (A : Type) (packed : pack A) : A := + match packed with packer v => v end. + +Notation "!!!" := (pack _) (at level 0, only printing). + +(* The following data is used as material for automatic proofs + based on type classes. *) + +Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}. + +Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}. + +Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n). +Proof. + intros []. + simpl. rewrite <-plus_n_O, <-plus_n_Sm. + reflexivity. +Qed. + +Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) := + {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}. + +Definition tuto_div2 n (p : EvenNat n) := @half _ p. + +(* to be used in the following examples +Compute (@half 8 _). + +Check (@half_prop 8 _). + +Check (@half_prop 7 _). + +and in command Tuto3_3 8. *) + +(* The following data is used as material for automatic proofs + based on canonical structures. *) + +Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}. + +Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r := + match r with Build_S_ev _ _ h => h end. + +Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n := + Build_S_ev n d Pd. + +Canonical Structure can_ev0 : S_ev 0 := + Build_S_ev 0 0 (@eq_refl _ 0). + +Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n). +Proof. +intros s; exists (S (S (double_of _ s))). +destruct s as [a P]. +exact (even_rec _ _ P). +Defined. + +Canonical Structure can_ev_rec. + +Record cmp (n : nat) (k : nat) := + C {h : S_ev k; _ : double_of k h = n}. + +(* To be used in, e.g., + +Check (C _ _ _ eq_refl : cmp 6 _). + +Check (C _ _ _ eq_refl : cmp 7 _). + +*) diff --git a/doc/plugin_tutorial/tuto3/theories/Loader.v b/doc/plugin_tutorial/tuto3/theories/Loader.v new file mode 100644 index 0000000000..1351cff63b --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/Loader.v @@ -0,0 +1,3 @@ +From Tuto3 Require Export Data. + +Declare ML Module "tuto3_plugin". diff --git a/doc/plugin_tutorial/tuto3/theories/test.v b/doc/plugin_tutorial/tuto3/theories/test.v new file mode 100644 index 0000000000..43204ddf34 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/test.v @@ -0,0 +1,23 @@ +(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *) + +Require Import Tuto3.Loader. + +(* This should print Type. *) +Tuto3_1. + +(* This should print a term that contains an existential variable. *) +(* And then print the same term, where the variable has been correctly + instantiated. *) +Tuto3_2. + +Lemma tutu x y (A : 0 < x) (B : 10 < y) : True. +Proof. +pack hypothesis A. +(* Hypothesis A should have disappeared and a "packed_hyps" hypothesis + should have appeared, with unreadable content. *) +pack hypothesis B. +(* Hypothesis B should have disappeared *) +destruct packed_hyps as [unpacked_hyps]. +(* Hypothesis unpacked_hyps should contain the previous contents of A and B. *) +exact I. +Qed. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 827b7c13c1..067af954ad 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1189,7 +1189,6 @@ def setup(app): app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks) # Add extra styles - app.add_stylesheet("fonts.css") app.add_stylesheet("ansi.css") app.add_stylesheet("coqdoc.css") app.add_javascript("notations.js") diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 7bc5d090b4..95a0039b0a 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -293,9 +293,6 @@ let ids_of_pattern_list = (List.fold_left (cases_pattern_fold_names Id.Set.add)) Id.Set.empty -let ids_of_cases_indtype p = - cases_pattern_fold_names Id.Set.add Id.Set.empty p - let ids_of_cases_tomatch tms = List.fold_right (fun (_, ona, indnal) l -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 8c735edfc9..f1a8ed202f 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -113,9 +113,6 @@ val map_constr_expr_with_binders : val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr -(** Specific function for interning "in indtype" syntax of "match" *) -val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t - val free_vars_of_constr_expr : constr_expr -> Id.Set.t val occur_var_constr_expr : Id.t -> constr_expr -> bool diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7aa85a0810..c8c38ffe05 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -573,12 +573,17 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = (* TODO binders *) next_ident_away_from id (fun id -> Id.Set.mem id fvs3) -let is_var store pat = +let is_patvar c = + match DAst.get c with + | PatVar _ -> true + | _ -> false + +let is_patvar_store store pat = match DAst.get pat with | PatVar na -> ignore(store na); true | _ -> false -let out_var pat = +let out_patvar pat = match pat.v with | CPatAtom (Some qid) when qualid_is_ident qid -> Name (qualid_basename qid) @@ -600,7 +605,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na + | [pat] when is_patvar_store store pat -> let na = get () in None, na | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> @@ -610,7 +615,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let env = set_env_scopes env scopes in if onlyident then (* Do not try to interpret a variable as a constructor *) - let na = out_var pat in + let na = out_patvar pat in let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in (renaming,env), None, na else @@ -618,7 +623,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na + | [pat] when is_patvar_store store pat -> let na = get () in None, na | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> @@ -743,7 +748,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in if onlyident then - let na = out_var c in term_of_name na, None + let na = out_patvar c in term_of_name na, None else let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with @@ -805,7 +810,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = (* and since we are only interested in the pattern as a term *) let env = reset_hidden_inductive_implicit_test env in if onlyident then - term_of_name (out_var pat) + term_of_name (out_patvar pat) else let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in match disjpat with @@ -1741,7 +1746,7 @@ let intern_ind_pattern genv ntnvars scopes pat = let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in (with_letin, match product_of_cases_patterns empty_alias idslpl with - | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) + | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type ?loc) | x -> error_bad_inductive_type ?loc @@ -1979,30 +1984,30 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = end | CCases (sty, rtnpo, tms, eqns) -> let as_in_vars = List.fold_left (fun acc (_,na,inb) -> - Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc) - (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na) - inb) Id.Set.empty tms in + (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na)) + Id.Set.empty tms in (* as, in & return vars *) let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in - let tms,ex_ids,match_from_in = List.fold_right - (fun citm (inds,ex_ids,matchs) -> - let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in - (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs) - tms ([],Id.Set.empty,[]) in + let tms,ex_ids,aliases,match_from_in = List.fold_right + (fun citm (inds,ex_ids,asubst,matchs) -> + let ((tm,ind),extra_id,(ind_ids,alias_subst,match_td)) = + intern_case_item env forbidden_vars citm in + (tm,ind)::inds, + Id.Set.union ind_ids (Option.fold_right Id.Set.add extra_id ex_ids), + merge_subst alias_subst asubst, + List.rev_append match_td matchs) + tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var)) (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = - let is_patvar c = match DAst.get c with - | PatVar _ -> true - | _ -> false - in let rec aux = function | [] -> [] | (_, c) :: q when is_patvar c -> aux q | l -> l in aux match_from_in in + let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in let rtnpo = match stripped_match_from_in with | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) | l -> @@ -2150,7 +2155,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* the "in" part *) let match_td,typ = match t with | Some t -> - let with_letin,(ind,l) = intern_ind_pattern globalenv ntnvars (None,env.scopes) t in + let with_letin,(ind,ind_ids,alias_subst,l) = + intern_ind_pattern globalenv ntnvars (None,env.scopes) t in let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in (* for "in Vect n", we answer (["n","n"],[(loc,"n")]) @@ -2186,9 +2192,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let _,args_rel = List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in canonize_args args_rel l forbidden_names_for_gen [] [] in - match_to_do, Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal)) + (Id.Set.of_list (List.map (fun id -> id.CAst.v) ind_ids),alias_subst,match_to_do), + Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal)) | None -> - [], None in + (Id.Set.empty,Id.Map.empty,[]), None in (tm',(na.CAst.v, typ)), extra_id, match_td and intern_impargs c env l subscopes args = diff --git a/kernel/names.ml b/kernel/names.ml index b2d6a489a6..9f27212967 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -391,6 +391,8 @@ module KerName = struct let print kn = str (to_string kn) + let debug_print kn = str (debug_to_string kn) + let compare (kn1 : kernel_name) (kn2 : kernel_name) = if kn1 == kn2 then 0 else diff --git a/kernel/names.mli b/kernel/names.mli index 350db871d5..61df3bad0e 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -149,15 +149,15 @@ sig val is_empty : t -> bool (** Test whether a directory path is empty. *) - val to_string : t -> string - (** Print directory paths as ["coq_root.module.submodule"] *) - val initial : t (** Initial "seed" of the unique identifier generator *) val hcons : t -> t (** Hashconsing of directory paths. *) + val to_string : t -> string + (** Print non-empty directory paths as ["coq_root.module.submodule"] *) + val print : t -> Pp.t end @@ -180,15 +180,15 @@ sig val make : string -> t (** Create a label out of a string. *) - val to_string : t -> string - (** Conversion to string. *) - val of_id : Id.t -> t (** Conversion from an identifier. *) val to_id : t -> Id.t (** Conversion to an identifier. *) + val to_string : t -> string + (** Conversion to string. *) + val print : t -> Pp.t (** Pretty-printer. *) @@ -227,10 +227,10 @@ sig (** Return the identifier contained in the argument. *) val to_string : t -> string - (** Conversion to a string. *) + (** Encode as a string (not to be used for user-facing messages). *) val debug_to_string : t -> string - (** Same as [to_string], but outputs information related to debug. *) + (** Same as [to_string], but outputs extra information related to debug. *) end @@ -252,16 +252,17 @@ sig val is_bound : t -> bool - val to_string : t -> string - - val debug_to_string : t -> string - (** Same as [to_string], but outputs information related to debug. *) - val initial : t (** Name of the toplevel structure ([= MPfile initial_dir]) *) val dp : t -> DirPath.t + val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + + val debug_to_string : t -> string + (** Same as [to_string], but outputs extra information related to debug. *) + end module MPset : Set.S with type elt = ModPath.t @@ -284,13 +285,17 @@ sig val modpath : t -> ModPath.t val label : t -> Label.t - (** Display *) val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) val debug_to_string : t -> string - (** Same as [to_string], but outputs information related to debug. *) + (** Same as [to_string], but outputs extra information related to debug. *) - val print : t -> Pp.t + val debug_print : t -> Pp.t + (** Same as [print], but outputs extra information related to debug. *) (** Comparisons *) val compare : t -> t -> int @@ -365,9 +370,16 @@ sig (** Displaying *) val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) + val debug_to_string : t -> string + (** Same as [to_string], but outputs extra information related to debug. *) + val debug_print : t -> Pp.t + (** Same as [print], but outputs extra information related to debug. *) end @@ -444,9 +456,16 @@ sig (** Displaying *) val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) + val debug_to_string : t -> string + (** Same as [to_string], but outputs extra information related to debug. *) + val debug_print : t -> Pp.t + (** Same as [print], but outputs extra information related to debug. *) end @@ -567,8 +586,12 @@ module Projection : sig val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t - val print : t -> Pp.t val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) + end type t (* = Repr.t * bool *) @@ -609,7 +632,10 @@ module Projection : sig val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) end diff --git a/lib/system.ml b/lib/system.ml index a9db95318f..fd6579dd69 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -287,20 +287,20 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = real (round (sstop -. sstart)) ++ str "s" ++ str ")" -let with_time ~batch f x = +let with_time ~batch ~header f x = let tstart = get_time() in let msg = if batch then "" else "Finished transaction in " in try let y = f x in let tend = get_time() in let msg2 = if batch then "" else " (successful)" in - Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if batch then "" else "Finished failing transaction in " in let msg2 = if batch then "" else " (failure)" in - Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e (* We use argv.[0] as we don't want to resolve symlinks *) diff --git a/lib/system.mli b/lib/system.mli index a3b79ee528..6dd1eb5a84 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -105,7 +105,7 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t -val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b +val with_time : batch:bool -> header:Pp.t -> ('a -> 'b) -> 'a -> 'b (** [get_toplevel_path program] builds a complete path to the executable denoted by [program]. This involves: diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index f0bb6f58a6..ff2c900130 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,5 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) open Goal open Environ diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 9a53e1dd1a..a39f76db9e 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -1,5 +1,15 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) + Declare ML Module "ssrmatching_plugin". Module SsrMatchingSyntax. diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e6e1530e36..ed28cc7725 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -46,15 +46,10 @@ let () = Goptions.(declare_bool_option { (* Functions to deal with impossible cases *) (*******************************************) let impossible_default_case env = - let type_of_id = - let open Names.GlobRef in - match Coqlib.lib_ref "core.IDProp.type" with - | ConstRef c -> c - | VarRef _ | IndRef _ | ConstructRef _ -> assert false - in + let type_of_id = Coqlib.lib_ref "core.IDProp.type" in let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in - let (_, u) = Constr.destConst c in - Some (c, Constr.mkConstU (type_of_id, u), ctx) + let (_, u) = Constr.destRef c in + Some (c, Constr.mkRef (type_of_id, u), ctx) let coq_unit_judge = let open Environ in diff --git a/stm/stm.ml b/stm/stm.ml index 32c6c7d959..169d608d2d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -869,7 +869,6 @@ end = struct (* {{{ *) cur_id := id | { state = Error ie } -> - cur_id := id; Exninfo.iraise ie | _ -> @@ -2017,7 +2016,7 @@ end = struct (* {{{ *) find ~time:false ~batch:false ~fail:false e in let st = Vernacstate.freeze_interp_state ~marshallable:false in Vernacentries.with_fail st fail (fun () -> - (if time then System.with_time ~batch else (fun x -> x)) (fun () -> + (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in @@ -2832,17 +2831,9 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - match Stateid.get info with - | None -> - VCS.restore vcs; - VCS.print (); - anomaly(str"error with no safe_id attached:" ++ spc() ++ - CErrors.iprint_no_report (e, info) ++ str".") - | Some (safe_id, id) -> - stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); - VCS.restore vcs; - VCS.print (); - Exninfo.iraise (e, info) + VCS.restore vcs; + VCS.print (); + Exninfo.iraise (e, info) let snapshot_vio ~doc ldir long_f_dot_vo = let doc = finish ~doc in @@ -2993,7 +2984,14 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Unknown: we execute it, check for open goals and propagate sideeff *) | VtUnknown, VtNow -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - let id = VCS.new_node ~id:newtip () in + if not (get_allow_nested_proofs ()) && in_proof then + "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." + |> Pp.str + |> (fun s -> (UserError (None, s), Exninfo.null)) + |> State.exn_on ~valid:Stateid.dummy Stateid.dummy + |> Exninfo.iraise + else + let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) let step () = diff --git a/test-suite/Makefile b/test-suite/Makefile index 34a1900bbc..37091a49e5 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -36,9 +36,10 @@ include ../Makefile.common # easily overridden LIB := .. BIN := $(shell cd ..; pwd)/bin/ +COQFLAGS?= -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite -coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite +coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS) +coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v new file mode 100644 index 0000000000..9816954d0c --- /dev/null +++ b/test-suite/bugs/closed/bug_8369.v @@ -0,0 +1,3 @@ +(* Was failing in master with a not_found generated by the printer *) + +Fail Definition foo := fun '(u, v) p2 => (u, v). diff --git a/test-suite/bugs/closed/bug_9240.v b/test-suite/bugs/closed/bug_9240.v new file mode 100644 index 0000000000..e0901dc2d9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9240.v @@ -0,0 +1,12 @@ +Register unit as core.IDProp.type. +Register tt as core.IDProp.idProp. + + +Inductive vec (A : Type) : nat -> Type := +| nil : vec A 0 +| cons : forall n : nat, A -> vec A n -> vec A (S n). + +Definition hd (A : Type) (n : nat) (v : vec A (S n)) : A := +match v in (vec _ (S n)) return A with +| cons _ _ h _ => h +end. (* assertion failure in evarconv *) diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v new file mode 100644 index 0000000000..a80f3233a3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9300.v @@ -0,0 +1,6 @@ +Existing Class True. + +Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined. + +Fail Check foo (n := 3) true (s := (4 , 5)). +Check foo (n := 3) (b := true) (4 , 5). diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v index e1c29a954c..baf87631f0 100644 --- a/test-suite/bugs/opened/bug_3166.v +++ b/test-suite/bugs/opened/bug_3166.v @@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True. compute in H0. change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. Fail pose proof (fun k => @eq_trans _ _ _ k H0). +Abort. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v index a717bbe735..18820b1a4c 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/opened/bug_3754.v @@ -282,3 +282,4 @@ Defined. rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. Fail rewrite (concat_Ap ff2). + Abort. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v index 5c74addb62..78b2aa69b9 100644 --- a/test-suite/bugs/opened/bug_3890.v +++ b/test-suite/bugs/opened/bug_3890.v @@ -1,3 +1,5 @@ +Set Nested Proofs Allowed. + Class Foo. Class Bar := b : Type. diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v index 2d0d1930f1..3c7c945ed8 100644 --- a/test-suite/bugs/opened/bug_3938.v +++ b/test-suite/bugs/opened/bug_3938.v @@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. intros a b f H. rewrite H. (* Toplevel input, characters 15-25: Anomaly: Evar ?X11 was not declared. Please report. *) +Abort. diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index ae5d51bae8..b7c98aa134 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *) Require Coq.ZArith.BinInt. Module WithIdTac. Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index cf2d5b2850..14c48e8fa0 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -9,10 +9,11 @@ The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. Instance is not well-typed in the environment of ?x. The command has indeed failed with message: -Cannot infer the domain of the type of f. +Cannot infer ?T in the partial instance "?T -> nat" found for the type of f. The command has indeed failed with message: -Cannot infer the domain of the implicit parameter A of id whose type is -"Type". +Cannot infer ?T in the partial instance "?T -> nat" found for the implicit +parameter A of id whose type is "Type". The command has indeed failed with message: -Cannot infer the codomain of the type of f in environment: +Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the +type of f in environment: x : nat diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 52fe98ac07..232ac17cbf 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1873,3 +1873,12 @@ Check match niln in listn O return O=O with niln => eq_refl end. (* (was failing up to May 2017) *) Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end. + +(* A test about binding variables of "in" clause of "match" *) +(* (was failing from 8.5 to Dec 2018) *) + +Check match O in nat return nat with O => O | _ => O end. + +(* Checking that aliases are substituted in the correct order *) + +Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 4372ac72ae..f8f10b34ae 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -126,6 +126,8 @@ TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line +TGTS ?= + ########## End of parameters ################################################## # What follows may be relevant to you only if you need to # extend this Makefile. If so, look for 'Extension point' here and @@ -237,6 +239,11 @@ vo_to_obj = $(addsuffix .o,\ $(filter-out Warning: Error:,\ $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) strip_dotslash = $(patsubst ./%,%,$(1)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + VO = vo VOFILES = $(VFILES:.v=.$(VO)) @@ -269,14 +276,14 @@ CMXSFILES = \ PACKEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) # files that are archived into a .cma (mllib) LIBEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) OBJFILES = $(call vo_to_obj,$(VOFILES)) @@ -681,11 +688,11 @@ $(GHTMLFILES): %.g.html: %.v %.glob # Dependency files ############################################################ -ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) -else - ifeq ($(MAKECMDGOALS),) +ifndef MAKECMDGOALS -include $(ALLDFILES) +else + ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) endif endif @@ -784,3 +791,7 @@ debug: .PHONY: debug .DEFAULT_GOAL := all + +# Local Variables: +# mode: makefile-gmake +# End: diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c914bbecff..d8465aac27 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -37,34 +37,6 @@ let vernac_echo ?loc in_chan = let open Loc in Feedback.msg_notice @@ str @@ really_input_string in_chan len ) loc -(* For coqtop -time, we display the position in the file, - and a glimpse of the executed command *) - -let pp_cmd_header {CAst.loc;v=com} = - let shorten s = - if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s - in - let noblank s = String.map (fun c -> - match c with - | ' ' | '\n' | '\t' | '\r' -> '~' - | x -> x - ) s - in - let (start,stop) = Option.cata Loc.unloc (0,0) loc in - let safe_pr_vernac x = - try Ppvernac.pr_vernac x - with e -> str (Printexc.to_string e) in - let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) - in str "Chars " ++ int start ++ str " - " ++ int stop ++ - str " [" ++ str cmd ++ str "] " - -(* This is a special case where we assume we are in console batch mode - and take control of the console. - *) -let print_cmd_header com = - Pp.pp_with !Topfmt.std_ft (pp_cmd_header com); - Format.pp_print_flush !Topfmt.std_ft () - (* Reenable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) @@ -88,7 +60,6 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = due to the way it prints. *) let com = if state.time then begin - print_cmd_header com; CAst.make ?loc @@ VernacTime(state.time,com) end else com in let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in diff --git a/vernac/classes.ml b/vernac/classes.ml index 370df615fc..a342f5bf98 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -301,10 +301,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass in - let sigma, k, u, cty, ctx', ctx, len, imps, subst = + let sigma, k, u, cty, ctx', ctx, imps, subst = let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in - let len = List.length ctx in + let len = Context.Rel.nhyps ctx in let imps = imps @ Impargs.lift_implicits len imps' in let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in @@ -320,7 +320,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args')) cl_context (args, []) in - sigma, cl, u, c', ctx', ctx, len, imps, args + sigma, cl, u, c', ctx', ctx, imps, args in let id = match instid with diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a2b5c8d70a..f3e1e1fc49 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -511,7 +511,7 @@ let pr_trailing_ne_context_of env sigma = if List.is_empty (Environ.rel_context env) && List.is_empty (Environ.named_context env) then str "." - else (str " in environment:"++ pr_context_unlimited env sigma) + else (strbrk " in environment:" ++ pr_context_unlimited env sigma) let rec explain_evar_kind env sigma evk ty = let open Evar_kinds in @@ -551,21 +551,21 @@ let rec explain_evar_kind env sigma evk ty = strbrk "an instance of type " ++ ty ++ str " for the variable " ++ Id.print id | Evar_kinds.SubEvar (where,evk') -> - let evi = Evd.find sigma evk' in + let rec find_source evk = + let evi = Evd.find sigma evk in + match snd evi.evar_source with + | Evar_kinds.SubEvar (_,evk) -> find_source evk + | src -> evi,src in + let evi,src = find_source evk' in let pc = match evi.evar_body with | Evar_defined c -> pr_leconstr_env env sigma c | Evar_empty -> assert false in let ty' = evi.evar_concl in - (match where with - | Some Evar_kinds.Body -> str "the body of " - | Some Evar_kinds.Domain -> str "the domain of " - | Some Evar_kinds.Codomain -> str "the codomain of " - | None -> - pr_existential_key sigma evk ++ str " of type " ++ ty ++ - str " in the partial instance " ++ pc ++ - str " found for ") ++ - explain_evar_kind env sigma evk' - (pr_leconstr_env env sigma ty') (snd evi.evar_source) + pr_existential_key sigma evk ++ + strbrk " in the partial instance " ++ pc ++ + strbrk " found for " ++ + explain_evar_kind env sigma evk + (pr_leconstr_env env sigma ty') src let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr sigma evi.evar_concl with diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 4065bb9c1f..b4b893a3fd 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -406,3 +406,24 @@ let with_output_to_file fname func input = deep_ft := Util.pi3 old_fmt; close_out channel; Exninfo.iraise reraise + +(* For coqtop -time, we display the position in the file, + and a glimpse of the executed command *) + +let pr_cmd_header {CAst.loc;v=com} = + let shorten s = + if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s + in + let noblank s = String.map (fun c -> + match c with + | ' ' | '\n' | '\t' | '\r' -> '~' + | x -> x + ) s + in + let (start,stop) = Option.cata Loc.unloc (0,0) loc in + let safe_pr_vernac x = + try Ppvernac.pr_vernac x + with e -> str (Printexc.to_string e) in + let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) + in str "Chars " ++ int start ++ str " - " ++ int stop ++ + str " [" ++ str cmd ++ str "] " diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 0ddf474970..5f84c5edee 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -71,3 +71,4 @@ val print_err_exn : exn -> unit redirected to a file [file] *) val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b +val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e6e3db4beb..dbccea1117 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2388,8 +2388,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = control v | VernacRedirect (s, {v}) -> Topfmt.with_output_to_file s control v - | VernacTime (batch, {v}) -> - System.with_time ~batch control v; + | VernacTime (batch, com) -> + let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in + System.with_time ~batch ~header control com.CAst.v; and aux ~atts : _ -> unit = function |