diff options
97 files changed, 1511 insertions, 1164 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8b37403960..0ebf69f50f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-07-09-V01" + CACHEKEY: "bionic_coq-V2019-09-20-V01" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -70,8 +70,6 @@ before_script: - config/coq_config.py - test-suite/misc/universes/all_stdlib.v expire_in: 1 week - variables: - timeout: "" script: - set -e @@ -84,8 +82,8 @@ before_script: - echo 'end:coq.config' - echo 'start:coq.build' - - $timeout make -j "$NJOBS" byte - - $timeout make -j "$NJOBS" world $EXTRA_TARGET + - make -j "$NJOBS" byte + - make -j "$NJOBS" world $EXTRA_TARGET - make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' @@ -164,7 +162,7 @@ before_script: - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH" - - $timeout make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all + - make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -172,8 +170,6 @@ before_script: - test-suite/logs # Gitlab doesn't support yet "expire_in: never" so we use the instance default # expire_in: never - variables: - timeout: "" # set dependencies when using .validate-template: @@ -279,7 +275,7 @@ build:base+async: variables: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" COQUSERFLAGS: "-async-proofs on" - timeout: "timeout 100m" + timeout: 100m allow_failure: true # See https://github.com/coq/coq/issues/9658 only: variables: @@ -290,7 +286,7 @@ build:quick: variables: COQ_EXTRA_CONF: "-native-compiler no" QUICK: "1" - timeout: "timeout 100m" + timeout: 100m allow_failure: true # See https://github.com/coq/coq/issues/9637 only: variables: @@ -327,7 +323,7 @@ pkg:opam: - opam pin add --kind=path coqide.$COQ_VERSION . - set +e variables: - COQ_VERSION: "8.10" + COQ_VERSION: "8.11" OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" only: *full-ci @@ -507,62 +503,6 @@ test-suite:egde:dune:dev: # Gitlab doesn't support yet "expire_in: never" so we use the instance default # expire_in: never -test-suite:edge+trunk+make: - stage: stage-1 - dependencies: [] - script: - - opam switch create 4.09.0 --empty - - eval $(opam env) - - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git - - opam update - - opam install ocaml-variants=4.09.0+trunk - - opam pin add -n ocamlfind --dev - - opam install num - - eval $(opam env) - # We avoid problems with warnings: - - ./configure -profile devel -warn-error no - - make -j "$NJOBS" world - - make -j "$NJOBS" test-suite UNIT_TESTS= - variables: - OPAM_SWITCH: base - artifacts: - name: "$CI_JOB_NAME.logs" - when: always - paths: - - test-suite/logs - expire_in: 1 week - allow_failure: true - only: *full-ci - -test-suite:edge+trunk+dune: - stage: stage-1 - dependencies: [] - script: - - opam switch create 4.09.0 --empty - - eval $(opam env) - - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git - - opam update - - opam install ocaml-variants=4.09.0+trunk - - opam pin add -n ocamlfind --dev - - opam pin add dune --dev # ounit lablgtk conf-gtksourceview - - opam install dune num - - eval $(opam env) - # We use the release profile to avoid problems with warnings - - make -f Makefile.dune trunk - - export COQ_UNIT_TEST=noop - - dune runtest --profile=ocaml409 - variables: - OPAM_SWITCH: base - artifacts: - name: "$CI_JOB_NAME.logs" - when: always - paths: - - _build/log - - _build/default/test-suite/logs - expire_in: 1 week - allow_failure: true - only: *full-ci - test-suite:base+async: extends: .test-suite-template dependencies: @@ -571,7 +511,7 @@ test-suite:base+async: - build:base variables: COQFLAGS: "-async-proofs on -async-proofs-cache force" - timeout: "timeout 100m" + timeout: 100m allow_failure: true only: variables: @@ -741,6 +681,9 @@ plugin:ci-mtac2: plugin:ci-paramcoq: extends: .ci-template +plugin:ci-perennial: + extends: .ci-template-flambda + plugin:plugin-tutorial: stage: stage-1 dependencies: [] @@ -9,7 +9,7 @@ WHAT DO YOU NEED ? - OCaml (version >= 4.05.0) (available at https://ocaml.org/) - (This version of Coq has been tested up to OCaml 4.08.1) + (This version of Coq has been tested up to OCaml 4.09.0) - The Num package, which used to be part of the OCaml standard library, if you are using an OCaml version >= 4.06.0 diff --git a/META.coq.in b/META.coq.in index f7922e0ac2..0baacbc82e 100644 --- a/META.coq.in +++ b/META.coq.in @@ -1,7 +1,7 @@ # TODO: Generate automatically with Dune description = "The Coq Proof Assistant Plugin API" -version = "8.10" +version = "8.11" directory = "" requires = "" @@ -9,7 +9,7 @@ requires = "" package "config" ( description = "Coq Configuration Variables" - version = "8.10" + version = "8.11" directory = "config" @@ -19,7 +19,7 @@ package "config" ( package "clib" ( description = "Base General Coq Library" - version = "8.10" + version = "8.11" directory = "clib" requires = "str, unix, threads" @@ -31,7 +31,7 @@ package "clib" ( package "lib" ( description = "Base Coq-Specific Library" - version = "8.10" + version = "8.11" directory = "lib" @@ -45,7 +45,7 @@ package "lib" ( package "vm" ( description = "Coq VM" - version = "8.10" + version = "8.11" directory = "kernel/byterun" @@ -64,7 +64,7 @@ package "vm" ( package "kernel" ( description = "Coq's Kernel" - version = "8.10" + version = "8.11" directory = "kernel" @@ -78,7 +78,7 @@ package "kernel" ( package "library" ( description = "Coq Libraries (vo) support" - version = "8.10" + version = "8.11" requires = "coq.kernel" @@ -92,7 +92,7 @@ package "library" ( package "engine" ( description = "Coq Tactic Engine" - version = "8.10" + version = "8.11" requires = "coq.library" directory = "engine" @@ -105,7 +105,7 @@ package "engine" ( package "pretyping" ( description = "Coq Pretyper" - version = "8.10" + version = "8.11" requires = "coq.engine" directory = "pretyping" @@ -118,7 +118,7 @@ package "pretyping" ( package "interp" ( description = "Coq Term Interpretation" - version = "8.10" + version = "8.11" requires = "coq.pretyping" directory = "interp" @@ -131,7 +131,7 @@ package "interp" ( package "proofs" ( description = "Coq Proof Engine" - version = "8.10" + version = "8.11" requires = "coq.interp" directory = "proofs" @@ -144,7 +144,7 @@ package "proofs" ( package "gramlib" ( description = "Coq Grammar Engine" - version = "8.10" + version = "8.11" requires = "coq.lib" directory = "gramlib/.pack" @@ -156,7 +156,7 @@ package "gramlib" ( package "parsing" ( description = "Coq Parsing Engine" - version = "8.10" + version = "8.11" requires = "coq.gramlib, coq.proofs" directory = "parsing" @@ -169,7 +169,7 @@ package "parsing" ( package "printing" ( description = "Coq Printing Engine" - version = "8.10" + version = "8.11" requires = "coq.parsing" directory = "printing" @@ -182,7 +182,7 @@ package "printing" ( package "tactics" ( description = "Coq Basic Tactics" - version = "8.10" + version = "8.11" requires = "coq.printing" directory = "tactics" @@ -195,7 +195,7 @@ package "tactics" ( package "vernac" ( description = "Coq Vernacular Interpreter" - version = "8.10" + version = "8.11" requires = "coq.tactics" directory = "vernac" @@ -208,7 +208,7 @@ package "vernac" ( package "stm" ( description = "Coq State Transactional Machine" - version = "8.10" + version = "8.11" requires = "coq.vernac" directory = "stm" @@ -221,7 +221,7 @@ package "stm" ( package "toplevel" ( description = "Coq Toplevel" - version = "8.10" + version = "8.11" requires = "num, coq.stm" directory = "toplevel" @@ -234,7 +234,7 @@ package "toplevel" ( package "idetop" ( description = "Coq IDE Libraries" - version = "8.10" + version = "8.11" requires = "coq.toplevel" directory = "ide" @@ -247,7 +247,7 @@ package "idetop" ( package "ide" ( description = "Coq IDE Libraries" - version = "8.10" + version = "8.11" requires = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3" directory = "ide" @@ -260,7 +260,7 @@ package "ide" ( package "ideprotocol" ( description = "Coq IDE protocol" - version = "8.10" + version = "8.11" requires = "coq.toplevel" directory = "ide/protocol" @@ -273,14 +273,14 @@ package "ideprotocol" ( package "plugins" ( description = "Coq built-in plugins" - version = "8.10" + version = "8.11" directory = "plugins" package "ltac" ( description = "Coq LTAC Plugin" - version = "8.10" + version = "8.11" requires = "coq.stm" directory = "ltac" @@ -293,7 +293,7 @@ package "plugins" ( package "tauto" ( description = "Coq tauto plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "ltac" @@ -305,7 +305,7 @@ package "plugins" ( package "omega" ( description = "Coq omega plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "omega" @@ -317,7 +317,7 @@ package "plugins" ( package "micromega" ( description = "Coq micromega plugin" - version = "8.10" + version = "8.11" requires = "num,coq.plugins.ltac" directory = "micromega" @@ -329,7 +329,7 @@ package "plugins" ( package "setoid_ring" ( description = "Coq newring plugin" - version = "8.10" + version = "8.11" requires = "" directory = "setoid_ring" @@ -341,7 +341,7 @@ package "plugins" ( package "extraction" ( description = "Coq extraction plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "extraction" @@ -353,7 +353,7 @@ package "plugins" ( package "cc" ( description = "Coq cc plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "cc" @@ -365,7 +365,7 @@ package "plugins" ( package "firstorder" ( description = "Coq ground plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "firstorder" @@ -377,7 +377,7 @@ package "plugins" ( package "rtauto" ( description = "Coq rtauto plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "rtauto" @@ -389,7 +389,7 @@ package "plugins" ( package "btauto" ( description = "Coq btauto plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "btauto" @@ -401,7 +401,7 @@ package "plugins" ( package "funind" ( description = "Coq recdef plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.extraction" directory = "funind" @@ -413,7 +413,7 @@ package "plugins" ( package "nsatz" ( description = "Coq nsatz plugin" - version = "8.10" + version = "8.11" requires = "num,coq.plugins.ltac" directory = "nsatz" @@ -425,7 +425,7 @@ package "plugins" ( package "rsyntax" ( description = "Coq rsyntax plugin" - version = "8.10" + version = "8.11" requires = "" directory = "syntax" @@ -437,7 +437,7 @@ package "plugins" ( package "int63syntax" ( description = "Coq int63syntax plugin" - version = "8.10" + version = "8.11" requires = "" directory = "syntax" @@ -449,7 +449,7 @@ package "plugins" ( package "string_notation" ( description = "Coq string_notation plugin" - version = "8.10" + version = "8.11" requires = "" directory = "syntax" @@ -461,7 +461,7 @@ package "plugins" ( package "derive" ( description = "Coq derive plugin" - version = "8.10" + version = "8.11" requires = "" directory = "derive" @@ -473,7 +473,7 @@ package "plugins" ( package "ssrmatching" ( description = "Coq ssrmatching plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "ssrmatching" @@ -485,7 +485,7 @@ package "plugins" ( package "ssreflect" ( description = "Coq ssreflect plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ssrmatching" directory = "ssr" diff --git a/Makefile.build b/Makefile.build index 610af5fe40..f2e1ca4ea0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -581,7 +581,7 @@ bin/votour.byte: $(VOTOURCMO) ########################################################################### CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \ - mutils.cmo micromega.cmo \ + micromega.cmo mutils.cmo \ sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) diff --git a/Makefile.ci b/Makefile.ci index de03ee8e84..60d4b68f53 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -35,6 +35,7 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ + ci-perennial \ ci-quickchick \ ci-relation_algebra \ ci-sf \ diff --git a/Makefile.dune b/Makefile.dune index 88055d62dc..19e8a770bd 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -6,7 +6,7 @@ .PHONY: quickbyte quickopt quickide # Partial / quick developer targets .PHONY: refman-html stdlib-html apidoc # Documentation targets .PHONY: test-suite release # Accessory targets -.PHONY: ocheck trunk ireport clean # Maintenance targets +.PHONY: ocheck ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short @@ -36,7 +36,6 @@ help: @echo " - release: build Coq in release mode" @echo "" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" - @echo " - trunk: build with a configuration compatible with OCaml trunk" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" @@ -103,11 +102,6 @@ release: voboot ocheck: voboot dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all -trunk: - dune build $(DUNEOPT) --profile=ocaml409 @vodeps - dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d - dune build $(DUNEOPT) --profile=ocaml409 coq.install coqide-server.install - ireport: dune clean dune build $(DUNEOPT) @vodeps --profile=ireport diff --git a/Makefile.ide b/Makefile.ide index 081d15a1a2..39c6c8ad1e 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -264,7 +264,7 @@ $(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents $(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents $(MKDIR) $@ - $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.so $@ + $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.dylib $@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib @@ -273,8 +273,8 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib { "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ > $@/gtk-3.0/gdk-pixbuf.loaders - { "$(GTKBIN)/gtk-query-immodules-3.0" $@/../immodules/*.so |\ - sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ + { "$(GTKBIN)/gtk-query-immodules-3.0" $@/../immodules/*.dylib |\ + sed -e "s!/.*\(/immodules/.*.dylib\)!@executable_path/../Resources/\1!" |\ sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ > $@/gtk-3.0/gtk-immodules.loaders $(MKDIR) $@/pango @@ -283,7 +283,7 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib $(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) $(MKDIR) $@ macpack -d ../Resources/lib $(COQIDEINAPP) - for i in $@/../loaders/*.so $@/../immodules/*.so; \ + for i in $@/../loaders/*.so $@/../immodules/*.dylib; \ do \ macpack -d ../lib $$i; \ done diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 84f080cc73..31dcae0f82 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -58,8 +58,8 @@ jobs: displayName: 'Install system dependencies' env: HOMEBREW_NO_AUTO_UPDATE: "1" - HBCORE_DATE: "2019-06-16" - HBCORE_REF: "944a5b7d83e4b81c749d93831b514607bdd2b6a1" + HBCORE_DATE: "2019-09-03" + HBCORE_REF: "44ee64cf4b9f2d2bf000758d356db0c77425e42e" - script: | set -e @@ -72,8 +72,8 @@ jobs: opam list displayName: 'Install OCaml dependencies' env: - COMPILER: "4.08.1" - FINDLIB_VER: ".1.8.0" + COMPILER: "4.09.0" + FINDLIB_VER: ".1.8.1" OPAMYES: "true" - script: | diff --git a/clib/hashset.ml b/clib/hashset.ml index debfc15c9a..b7a245aed1 100644 --- a/clib/hashset.ml +++ b/clib/hashset.ml @@ -118,8 +118,8 @@ module Make (E : EqType) = t.table.(t.rover) <- emptybucket; t.hashes.(t.rover) <- [| |]; end else begin - Obj.truncate (Obj.repr bucket) (prev_len + 1); - Obj.truncate (Obj.repr hbucket) prev_len; + Obj.truncate (Obj.repr bucket) (prev_len + 1) [@ocaml.alert "--deprecated"]; + Obj.truncate (Obj.repr hbucket) prev_len [@ocaml.alert "--deprecated"]; end; if len > t.limit && prev_len <= t.limit then t.oversize <- t.oversize - 1; end; diff --git a/configure.ml b/configure.ml index d7370b28c1..e59a41a8d4 100644 --- a/configure.ml +++ b/configure.ml @@ -12,11 +12,11 @@ #load "str.cma" open Printf -let coq_version = "8.10+alpha" -let coq_macos_version = "8.9.90" (** "[...] should be a string comprised of +let coq_version = "8.11+alpha" +let coq_macos_version = "8.10.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 8991 -let state_magic = 58991 +let vo_magic = 81091 +let state_magic = 581091 let is_a_released_version = false let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; diff --git a/default.nix b/default.nix index 2d101eed57..19afc2bd1b 100644 --- a/default.nix +++ b/default.nix @@ -29,7 +29,7 @@ , shell ? false # We don't use lib.inNixShell because that would also apply # when in a nix-shell of some package depending on this one. -, coq-version ? "8.10-git" +, coq-version ? "8.11-git" }: with pkgs; diff --git a/dev/build/windows/patches_coq/ocaml-4.07.1.patch b/dev/build/windows/patches_coq/ocaml-4.07.1.patch index 2d61b5b838..2d61b5b838 100755..100644 --- a/dev/build/windows/patches_coq/ocaml-4.07.1.patch +++ b/dev/build/windows/patches_coq/ocaml-4.07.1.patch diff --git a/dev/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c index c4c7ec2bff..c4c7ec2bff 100755..100644 --- a/dev/build/windows/patches_coq/pkg-config.c +++ b/dev/build/windows/patches_coq/pkg-config.c diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 03ce5a6b5d..ee6c62673b 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.08.1+mingw64c +OPAM_VARIANT=ocaml-variants.4.09.0+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 3923fea30e..8db0087e3c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -311,3 +311,10 @@ : "${argosy_CI_REF:=master}" : "${argosy_CI_GITURL:=https://github.com/mit-pdos/argosy}" : "${argosy_CI_ARCHIVEURL:=${argosy_CI_GITURL}/archive}" + +######################################################################## +# perennial +######################################################################## +: "${perennial_CI_REF:=master}" +: "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}" +: "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}" diff --git a/dev/ci/ci-perennial.sh b/dev/ci/ci-perennial.sh new file mode 100755 index 0000000000..f3be66e814 --- /dev/null +++ b/dev/ci/ci-perennial.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download perennial + +# required by Perennial's coqc.py build wrapper +export LC_ALL=C.UTF-8 + +( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 567f0539ab..edca83c6ef 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-07-09-V01" +# CACHEKEY: "bionic_coq-V2019-09-20-V01" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,12 +37,12 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.10.0 ounit.2.0.8 odoc.1.4.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.7.0" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" +ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" # Must add this to COQIDE_OPAM{,_EDGE} when we update the opam # packages "lablgtk3-gtksourceview3" @@ -56,9 +56,9 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.08.1" \ - COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta6" \ - BASE_OPAM_EDGE="dune-release.1.3.1" +ENV COMPILER_EDGE="4.09.0" \ + COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \ + BASE_OPAM_EDGE="dune-release.1.3.2" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh new file mode 100644 index 0000000000..a5f6551474 --- /dev/null +++ b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then + + elpi_CI_REF=library+to_vernac_step2 + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 452160ea5a..1c486b024d 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -2,6 +2,11 @@ ## As soon as the previous version branched off master ## +In principle, these steps should be undertaken by the RM of the next +release. Unfortunately, we have not yet been able to nominate RMs +early enough in the process for this person to be known at that point +in time. + - [ ] Create a new issue to track the release process where you can copy-paste the present checklist. - [ ] Change the version name to the next major version and the magic @@ -54,25 +59,39 @@ - [ ] Ping the development coordinator (**@mattam82**) to get him started on the update to the Credits chapter of the reference manual. See also [#7058](https://github.com/coq/coq/issues/7058). - The command to get the list of contributors for this version is - `git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2` - (the ordering is approximative as it will misplace people with middle names). + + The command that was used in the previous versions to get the list + of contributors for this version is `git shortlog -s -n + VX.X+alpha..master | cut -f2 | sort -k 2`. Note that the ordering is + approximative as it will misplace people with middle names. It is + also probably not correctly handling `Co-authored-by` info that we + have been using more lately, so should probably be updated to + account for this. ## On the date of the feature freeze ## - [ ] Create the new version branch `vX.X` (using this name will ensure that the branch will be automatically protected). +- [ ] Pin the versions of libraries and plugins in + `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it + exists, a branch dedicated to compatibility with the corresponding + Coq branch). - [ ] Remove all remaining unmerged feature PRs from the beta milestone. -- [ ] Start a new project to track PR backporting. The proposed model is to - have a "X.X-only PRs" column for the rare PRs on the stable branch, a - "Request X.X inclusion" column for the PRs that were merged in `master` that - are to be considered for backporting, a "Waiting for CI" column to put the - PRs in the process of being backported, and "Shipped in ..." columns to put - what was backported. (The release manager is the person responsible for - merging PRs that target the version branch and backporting appropriate PRs - that are merged into `master`). - A message to **@coqbot** in the milestone description tells it to - automatically add merged PRs to the "Request X.X inclusion" column. +- [ ] Start a new project to track PR backporting. The project should + have a "Request X.X+beta1 inclusion" column for the PRs that were + merged in `master` that are to be considered for backporting, and a + "Shipped in X.X+beta1" columns to put what was backported. A message + to **@coqbot** in the milestone description tells it to + automatically add merged PRs to the "Request ... inclusion" column + and backported PRs to the "Shipped in ..." column. See previous + milestones for examples. When moving to the next milestone + (e.g. X.X.0), you can clear and remove the "Request X.X+beta1 + inclusion" column and create new "Request X.X.0 inclusion" and + "Shipped in X.X.0" columns. + + The release manager is the person responsible for merging PRs that + target the version branch and backporting appropriate PRs that are + merged into `master`. - [ ] Delay non-blocking issues to the appropriate milestone and ensure blocking issues are solved. If required to solve some blocking issues, it is possible to revert some feature PRs in the version branch only. @@ -80,6 +99,11 @@ ## Before the beta release date ## - [ ] Ensure the Credits chapter has been updated. +- [ ] Prepare the release notes (see e.g., + [#10833](https://github.com/coq/coq/pull/10833)): in a PR against the `master` + branch, move the contents from all files of `doc/changelog/` that appear in + the release branch into the manual `doc/sphinx/changes.rst`. Merge that PR + into the `master` branch and backport it to the version branch. - [ ] Ensure that an appropriate version of the plugins we will distribute with Coq has been tagged. - [ ] Have some people test the recently auto-generated Windows and MacOS @@ -120,6 +144,7 @@ ## At the final release time ## +- [ ] Prepare the release notes (see above) - [ ] In a PR: - Change the version name from X.X.0 and the magic numbers (see [#7271](https://github.com/coq/coq/pull/7271/files)). diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 7e53f13e45..28e8773e25 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -1,7 +1,7 @@ -(lang dune 1.4) +(lang dune 1.10) ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.08.1))) -(context (opam (switch 4.08.1+flambda))) +(context (opam (switch 4.09.0))) +(context (opam (switch 4.09.0+flambda))) diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst new file mode 100644 index 0000000000..12d8f68e63 --- /dev/null +++ b/doc/changelog/04-tactics/10765-micromega-caches.rst @@ -0,0 +1,3 @@ +- Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. + (see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case) + (`#10765 <https://github.com/coq/coq/pull/10765>`_ fixes `#10772 <https://github.com/coq/coq/issues/10772>`_ , by Frédéric Besson). diff --git a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst new file mode 100644 index 0000000000..7babcdb6f1 --- /dev/null +++ b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst @@ -0,0 +1,4 @@ +- Moved the `auto` hints of the `OrderedType` module into a new `ordered_type` + database + (`#9772 <https://github.com/coq/coq/pull/9772>`_, + by Vincent Laporte). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 238106b2e7..4a691bde3a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,18 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. flag:: Lia Cache + + This option (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` + +.. flag:: Nia Cache + + This option (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache` + +.. flag:: Nra Cache + + This option (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache` + The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1d0b732e7d..905068e316 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -507,17 +507,45 @@ underscore or by omitting the annotation to a polymorphic definition. Universe polymorphism and sections ---------------------------------- -The universe polymorphic or monomorphic status is -attached to each individual section, and all term or universe declarations -contained inside must respect it, as described below. It is possible to nest a -polymorphic section inside a monomorphic one, but the converse is not allowed. - -:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and :cmd:`Constraint` in a section support -polymorphism. This means that the universe variables and their associated -constraints are discharged polymorphically over definitions that use -them. In other words, two definitions in the section sharing a common -variable will both get parameterized by the universes produced by the -variable declaration. This is in contrast to a “mononorphic” variable -which introduces global universes and constraints, making the two -definitions depend on the *same* global universes associated to the -variable. +:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and +:cmd:`Constraint` in a section support polymorphism. This means that +the universe variables and their associated constraints are discharged +polymorphically over definitions that use them. In other words, two +definitions in the section sharing a common variable will both get +parameterized by the universes produced by the variable declaration. +This is in contrast to a “mononorphic” variable which introduces +global universes and constraints, making the two definitions depend on +the *same* global universes associated to the variable. + +It is possible to mix universe polymorphism and monomorphism in +sections, except in the following ways: + +- no monomorphic constraint may refer to a polymorphic universe: + + .. coqtop:: all reset + + Section Foo. + + Polymorphic Universe i. + Fail Constraint i = i. + + This includes constraints implictly declared by commands such as + :cmd:`Variable`, which may as a such need to be used with universe + polymorphism activated (locally by attribute or globally by option): + + .. coqtop:: all + + Fail Variable A : (Type@{i} : Type). + Polymorphic Variable A : (Type@{i} : Type). + + (in the above example the anonymous :g:`Type` constrains polymorphic + universe :g:`i` to be strictly smaller.) + +- no monomorphic constant or inductive may be declared if polymorphic + universes or universe constraints are present. + +These restrictions are required in order to produce a sensible result +when closing the section (the requirement on constants and inductives +is stricter than the one on constraints, because constants and +inductives are abstracted by *all* the section's polymorphic universes +and constraints). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 38b3c34209..0148925247 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -718,6 +718,14 @@ Changes in 8.10+beta3 follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_, which added ``uncons`` in 8.10+beta1). +Changes in 8.10.0 +~~~~~~~~~~~~~~~~~ + +- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by + primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_, + fixes `#9512 <https://github.com/coq/coq/issues/9512>`_ + by Vincent Laporte). + Version 8.9 ----------- diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index dc4f91e66b..2d047a1058 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -638,7 +638,11 @@ the induction principle to easily reason about the function. than like this: - .. coqtop:: reset all + .. coqtop:: reset none + + Require Import FunInd. + + .. coqtop:: all Function plus (n m : nat) {struct n} : nat := match n with @@ -649,17 +653,22 @@ the induction principle to easily reason about the function. *Limitations* -|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`) +:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`) with applications only *at the end* of each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of :g:`wrong` in the body of :g:`wrong`: -.. coqtop:: all +.. coqtop:: none + + Require List. + Import List.ListNotations. + +.. coqtop:: all fail - Fail Function wrong (C:nat) : nat := - List.hd 0 (List.map wrong (C::nil)). + Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). For now, dependent cases are not treated for non structurally terminating functions. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fa6d62ffa2..c910136406 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3005,7 +3005,7 @@ the conversion in hypotheses :n:`{+ @ident}`. flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` and ``cofix``. The ``delta`` flag itself can be refined into - :n:`delta {+ @qualid}` or :n:`delta -{+ @qualid}`, restricting in the first + :n:`delta [ {+ @qualid} ]` or :n:`delta - [ {+ @qualid} ]`, restricting in the first case the constants to unfold to the constants listed, and restricting in the second case the constant to unfold to all but the ones explicitly mentioned. Notice that the ``delta`` flag does not apply to variables bound by a let-in @@ -3049,18 +3049,18 @@ the conversion in hypotheses :n:`{+ @ident}`. This is a synonym for ``lazy beta delta iota zeta``. -.. tacv:: compute {+ @qualid} - cbv {+ @qualid} +.. tacv:: compute [ {+ @qualid} ] + cbv [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. -.. tacv:: compute -{+ @qualid} - cbv -{+ @qualid} +.. tacv:: compute - [ {+ @qualid} ] + cbv - [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. -.. tacv:: lazy {+ @qualid} - lazy -{+ @qualid} +.. tacv:: lazy [ {+ @qualid} ] + lazy - [ {+ @qualid} ] These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta` and :n:`lazy beta delta -{+ @qualid} iota zeta`. @@ -3071,7 +3071,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. This algorithm is dramatically more efficient than the algorithm used for the - ``cbv`` tactic, but it cannot be fine-tuned. It is specially interesting for + :tacn:`cbv` tactic, but it cannot be fine-tuned. It is especially interesting for full evaluation of algebraic objects. This includes the case of reflection-based tactics. @@ -3080,14 +3080,14 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic evaluates the goal by compilation to OCaml as described in :cite:`FullReduction`. If Coq is running in native code, it can be - typically two to five times faster than ``vm_compute``. Note however that the + typically two to five times faster than :tacn:`vm_compute`. Note however that the compilation cost is higher, so it is worth using only for intensive computations. .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this option makes - it possible to profile ``native_compute`` evaluations. + it possible to profile :tacn:`native_compute` evaluations. .. opt:: NativeCompute Profile Filename @string :name: NativeCompute Profile Filename @@ -3097,7 +3097,7 @@ the conversion in hypotheses :n:`{+ @ident}`. will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means you can individually profile multiple uses of - ``native_compute`` in a script. From the Linux command line, run ``perf report`` + :tacn:`native_compute` in a script. From the Linux command line, run ``perf report`` on the profile file to see the results. Consult the ``perf`` documentation for more details. @@ -3153,14 +3153,15 @@ the conversion in hypotheses :n:`{+ @ident}`. use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. - The ``cbn`` tactic is claimed to be a more principled, faster and more - predictable replacement for ``simpl``. + The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + predictable replacement for :tacn:`simpl`. - The ``cbn`` tactic accepts the same flags as ``cbv`` and ``lazy``. The - behavior of both ``simpl`` and ``cbn`` can be tuned using the - Arguments vernacular command as follows: + The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and + :tacn:`lazy`. The behavior of both :tacn:`simpl` and :tacn:`cbn` + can be tuned using the Arguments vernacular command as follows: - + A constant can be marked to be never unfolded by ``cbn`` or ``simpl``: + + A constant can be marked to be never unfolded by :tacn:`cbn` or + :tacn:`simpl`: .. example:: @@ -3169,7 +3170,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus n m : simpl never. After that command an expression like :g:`(minus (S x) y)` is left - untouched by the tactics ``cbn`` and ``simpl``. + untouched by the tactics :tacn:`cbn` and :tacn:`simpl`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the @@ -3184,7 +3185,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Notation "f \o g" := (fcomp f g) (at level 50). After that command the expression :g:`(f \o g)` is left untouched by - ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. + :tacn:`simpl` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. The same mechanism can be used to make a constant volatile, i.e. always unfolded. @@ -3206,7 +3207,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus !n !m. After that command, the expression :g:`(minus (S x) y)` is left untouched - by ``simpl``, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + by :tacn:`simpl`, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + A special heuristic to determine if a constant has to be unfolded can be activated with the following command: @@ -3222,25 +3223,25 @@ the conversion in hypotheses :n:`{+ @ident}`. :g:`(minus (S (S x)) (S y))` is simplified to :g:`(minus (S x) y)` even if an extra simplification is possible. - In detail, the tactic ``simpl`` first applies :math:`\beta`:math:`\iota`-reduction. Then, it + In detail, the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`- reduction. But, when no :math:`\iota` rule is applied after unfolding then - :math:`\delta`-reductions are not applied. For instance trying to use ``simpl`` on + :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on :g:`(plus n O) = n` changes nothing. Notice that only transparent constants whose name can be reused in the - recursive calls are possibly unfolded by ``simpl``. For instance a + recursive calls are possibly unfolded by :tacn:`simpl`. For instance a constant defined by :g:`plus' := plus` is possibly unfolded and reused in the recursive calls, but a constant such as :g:`succ := plus (S O)` is - never unfolded. This is the main difference between ``simpl`` and ``cbn``. - The tactic ``cbn`` reduces whenever it will be able to reuse it or not: + never unfolded. This is the main difference between :tacn:`simpl` and :tacn:`cbn`. + The tactic :tacn:`cbn` reduces whenever it will be able to reuse it or not: :g:`succ t` is reduced to :g:`S t`. -.. tacv:: cbn {+ @qualid} - cbn -{+ @qualid} +.. tacv:: cbn [ {+ @qualid} ] + cbn - [ {+ @qualid} ] - These are respectively synonyms of :n:`cbn beta delta {+ @qualid} iota zeta` - and :n:`cbn beta delta -{+ @qualid} iota zeta` (see :tacn:`cbn`). + These are respectively synonyms of :n:`cbn beta delta [ {+ @qualid} ] iota zeta` + and :n:`cbn beta delta - [ {+ @qualid} ] iota zeta` (see :tacn:`cbn`). .. tacv:: simpl @pattern @@ -3249,7 +3250,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @pattern at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences. @@ -3265,7 +3266,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @qualid at {+ @num} simpl @string at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose + This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). .. flag:: Debug RAKAM @@ -3960,6 +3961,9 @@ At Coq startup, only the core database is nonempty and can be used. :fset: internal database for the implementation of the ``FSets`` library. +:ordered_type: lemmas about ordered types (as defined in the legacy ``OrderedType`` module), + mainly used in the ``FSets`` and ``FMaps`` libraries. + You are advised not to put your own hints in the core database, but use one or several databases specific to your development. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index d1b98b94a3..75c8c6c1ea 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -627,5 +627,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq88.v theories/Compat/Coq89.v theories/Compat/Coq810.v + theories/Compat/Coq811.v </dd> </dl> @@ -4,9 +4,7 @@ (release (flags :standard -rectypes) (ocamlopt_flags -O3 -unbox-closures)) (ireport (flags :standard -rectypes -w -9-27-40+60) - (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)) - (ocaml409 - (flags :standard -strict-sequence -strict-formats -keep-locs -rectypes -w -9-27+40+60 -warn-error -5 -alert --deprecated))) + (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report))) ; Information about flags for release mode: ; diff --git a/engine/uState.ml b/engine/uState.ml index cb40e6eadd..d93ccafcf0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -178,6 +178,7 @@ exception UniversesDiffer let drop_weak_constraints = ref false + let process_universe_constraints ctx cstrs = let open UnivSubst in let open UnivProblem in @@ -236,22 +237,21 @@ let process_universe_constraints ctx cstrs = else match cst with | ULe (l, r) -> - if UGraph.check_leq univs l r then - (* Keep Prop/Set <= var around if var might be instantiated by prop or set - later. *) - match Universe.level l, Universe.level r with - | Some l, Some r -> - Constraint.add (l, Le, r) local - | _ -> local - else - begin match Universe.level r with - | None -> user_err Pp.(str "Algebraic universe on the right") - | Some r' -> - if Level.is_small r' then + begin match Univ.Universe.level r with + | None -> + if UGraph.check_leq univs l r then local + else user_err Pp.(str "Algebraic universe on the right") + | Some r' -> + if Level.is_small r' then if not (Universe.is_levels l) - then + then (* l contains a +1 and r=r' small so l <= r impossible *) raise (UniverseInconsistency (Le, l, r, None)) else + if UGraph.check_leq univs l r then match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> local + else let levels = Universe.levels l in let fold l' local = let l = Universe.make l' in @@ -260,8 +260,12 @@ let process_universe_constraints ctx cstrs = else raise (UniverseInconsistency (Le, l, r, None)) in LSet.fold fold levels local - else - enforce_leq l r local + else + match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> + if UGraph.check_leq univs l r then local else enforce_leq l r local end | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local diff --git a/ide/coq2.ico b/ide/coq2.ico Binary files differindex bc1732fd99..bc1732fd99 100755..100644 --- a/ide/coq2.ico +++ b/ide/coq2.ico diff --git a/interp/modintern.ml b/interp/modintern.ml index 955288244e..ddf5b2d7b1 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -12,7 +12,6 @@ open Declarations open Libnames open Constrexpr open Constrintern -open Declaremods type module_internalization_error = | NotAModuleNorModtype of string @@ -21,9 +20,11 @@ type module_internalization_error = exception ModuleInternalizationError of module_internalization_error +type module_kind = Module | ModType | ModAny + let error_not_a_module_loc kind loc qid = let s = string_of_qualid qid in - let e = let open Declaremods in match kind with + let e = match kind with | Module -> Modops.ModuleTypingError (Modops.NotAModule s) | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) @@ -46,7 +47,6 @@ let error_application_to_module_type loc = it is equal to the input kind when this one isn't ModAny. *) let lookup_module_or_modtype kind qid = - let open Declaremods in let loc = qid.CAst.loc in try if kind == ModType then raise Not_found; diff --git a/interp/modintern.mli b/interp/modintern.mli index 75ab38c64a..72695a680e 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -28,5 +28,7 @@ exception ModuleInternalizationError of module_internalization_error kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) +type module_kind = Module | ModType | ModAny + val interp_module_ast : - env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t + env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 0951b07d49..b88a2e6194 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -161,7 +161,7 @@ type 'opaque result = { cook_universes : universes; cook_relevance : Sorts.relevance; cook_inline : inline; - cook_context : Constr.named_context option; + cook_context : Id.Set.t option; } let expmod_constr_subst cache modlist subst c = @@ -242,11 +242,7 @@ let cook_constant { from = cb; info } = OpaqueDef (Opaqueproof.discharge_direct_opaque info o) | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in - let const_hyps = - Context.Named.fold_outside (fun decl hyps -> - List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) - hyps) - hyps0 ~init:cb.const_hyps in + let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in let typ = abstract_constant_type (expmod cb.const_type) hyps in { cook_body = body; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 671cdf51fe..83a8b9edfc 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -23,7 +23,7 @@ type 'opaque result = { cook_universes : universes; cook_relevance : Sorts.relevance; cook_inline : inline; - cook_context : Constr.named_context option; + cook_context : Names.Id.Set.t option; } val cook_constant : recipe -> Opaqueproof.opaque result diff --git a/kernel/entries.ml b/kernel/entries.ml index 47e2f72b0e..1e6bc14935 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -61,7 +61,7 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; (* List of section variables *) - const_entry_secctx : Constr.named_context option; + const_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -70,7 +70,7 @@ type definition_entry = { type section_def_entry = { secdef_body : constr; - secdef_secctx : Constr.named_context option; + secdef_secctx : Id.Set.t option; secdef_feedback : Stateid.t option; secdef_type : types option; } @@ -78,7 +78,7 @@ type section_def_entry = { type 'a opaque_entry = { opaque_entry_body : 'a; (* List of section variables *) - opaque_entry_secctx : Constr.named_context; + opaque_entry_secctx : Id.Set.t; (* State id on which the completion of type checking is reported *) opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; @@ -88,7 +88,7 @@ type 'a opaque_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Constr.named_context option * types in_universes_entry * inline + Id.Set.t option * types in_universes_entry * inline type primitive_entry = { prim_entry_type : types option; diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index e54118c775..f788832d5b 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -96,14 +96,14 @@ let mk_accu (a : atom) : t = else let data = { data with acc_arg = x :: data.acc_arg } in let ans = Obj.repr (accumulate data) in - let () = Obj.set_tag ans accumulate_tag in + let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in ans in let acc = { acc_atm = a; acc_arg = [] } in let ans = Obj.repr (accumulate acc) in (** FIXME: use another representation for accumulators, this causes naked pointers. *) - let () = Obj.set_tag ans accumulate_tag in + let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in (Obj.obj ans : t) let get_accu (k : accumulator) = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index db16bd1e79..1069d9a62c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -334,8 +334,6 @@ type constraints_addition = let push_context_set poly cst senv = if Univ.ContextSet.is_empty cst then senv - else if Section.is_polymorphic senv.sections then - CErrors.user_err (Pp.str "Cannot add global universe constraints inside a polymorphic section.") else let sections = if Section.is_empty senv.sections then senv.sections @@ -735,7 +733,7 @@ let constant_entry_of_side_effect eff = if Declareops.is_opaque cb then OpaqueEff { opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); - opaque_entry_secctx = cb.const_hyps; + opaque_entry_secctx = Context.Named.to_vars cb.const_hyps; opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; @@ -743,7 +741,7 @@ let constant_entry_of_side_effect eff = else DefinitionEff { const_entry_body = p; - const_entry_secctx = Some cb.const_hyps; + const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps); const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; @@ -947,13 +945,13 @@ let add_module l me inl senv = (** {6 Interactive sections *) -let open_section ~poly senv = +let open_section senv = let custom = { rev_env = senv.env; rev_univ = senv.univ; rev_objlabels = senv.objlabels; } in - let sections = Section.open_section ~poly ~custom senv.sections in + let sections = Section.open_section ~custom senv.sections in { senv with sections } let close_section senv = @@ -962,7 +960,6 @@ let close_section senv = let env0 = senv.env in (* First phase: revert the declarations added in the section *) let sections, entries, cstrs, revert = Section.close_section sections0 in - let () = assert (not (Section.is_polymorphic sections0) || Univ.ContextSet.is_empty cstrs) in let rec pop_revstruct accu entries revstruct = match entries, revstruct with | [], revstruct -> accu, revstruct | _ :: _, [] -> diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index d3ca642a89..d97d61a72f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -134,7 +134,7 @@ val check_engagement : Environ.env -> Declarations.set_predicativity -> unit (** {6 Interactive section functions } *) -val open_section : poly:bool -> safe_transformer0 +val open_section : safe_transformer0 val close_section : safe_transformer0 diff --git a/kernel/section.ml b/kernel/section.ml index 188249e77e..babd9fe7a1 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -14,49 +14,38 @@ open Univ module NamedDecl = Context.Named.Declaration -type _ section_kind = -| SecMono : [ `mono ] section_kind -| SecPoly : [ `poly ] section_kind - -type (_, 'a) section_universes = -| SecMonoUniv : 'a -> ([ `mono ], 'a) section_universes -| SecPolyUniv : Name.t array * UContext.t -> ([ `poly ], 'a) section_universes - type section_entry = | SecDefinition of Constant.t | SecInductive of MutInd.t type 'a entry_map = 'a Cmap.t * 'a Mindmap.t -type ('a, 'b) section = { +type 'a section = { sec_context : int; (** Length of the named context suffix that has been introduced locally *) - sec_universes : ('a, ContextSet.t) section_universes; + sec_mono_universes : ContextSet.t; + sec_poly_universes : Name.t array * UContext.t; (** Universes local to the section *) + has_poly_univs : bool; + (** Are there polymorphic universes or constraints, including in previous sections. *) sec_entries : section_entry list; (** Definitions introduced in the section *) - sec_data : ('a, unit) section_universes entry_map; + sec_data : (Instance.t * AUContext.t) entry_map; (** Additional data synchronized with the section *) - sec_custom : 'b; + sec_custom : 'a; } (** Sections can be nested with the proviso that no monomorphic section can be opened inside a polymorphic one. The reverse is allowed. *) -type 'a t = { - sec_poly : ([ `poly ], 'a) section list; - sec_mono : ([ `mono ], 'a) section list; -} +type 'a t = 'a section list -let empty = { - sec_poly = []; - sec_mono = []; -} +let empty = [] -let is_empty s = - List.is_empty s.sec_poly && List.is_empty s.sec_mono +let is_empty = List.is_empty -let is_polymorphic s = - not (List.is_empty s.sec_poly) +let has_poly_univs = function + | [] -> false + | sec :: _ -> sec.has_poly_univs let find_emap e (cmap, imap) = match e with | SecDefinition con -> Cmap.find con cmap @@ -66,104 +55,80 @@ let add_emap e v (cmap, imap) = match e with | SecDefinition con -> (Cmap.add con v cmap, imap) | SecInductive ind -> (cmap, Mindmap.add ind v imap) -type 'b on_sec = { on_sec : 'a. 'a section_kind -> ('a, 'b) section -> ('a, 'b) section } - -let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with -| [], [] -> CErrors.user_err (Pp.str "No opened section") -| sec :: rem, _ -> - let sec_poly = f.on_sec SecPoly sec :: rem in - { sec_mono; sec_poly } -| [], sec :: rem -> - let sec_mono = f.on_sec SecMono sec :: rem in - { sec_mono; sec_poly } +let on_last_section f sections = match sections with +| [] -> CErrors.user_err (Pp.str "No opened section") +| sec :: rem -> f sec :: rem -type ('r, 'b) with_sec = { with_sec : 'a. ('a section_kind * ('a, 'b) section) option -> 'r } - -let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with -| [], [] -> f.with_sec None -| sec :: _, _ -> f.with_sec (Some (SecPoly, sec)) -| [], sec :: _ -> f.with_sec (Some (SecMono, sec)) +let with_last_section f sections = match sections with +| [] -> f None +| sec :: _ -> f (Some sec) let push_local s = - let on_sec _ sec = { sec with sec_context = sec.sec_context + 1 } in - on_last_section { on_sec } s + let on_sec sec = { sec with sec_context = sec.sec_context + 1 } in + on_last_section on_sec s let push_context (nas, ctx) s = - let on_sec (type a) (kind : a section_kind) (sec : (a, _) section) : (a, _) section = match kind with - | SecMono -> - CErrors.anomaly (Pp.str "Adding polymorphic constraints to monomorphic section") - | SecPoly -> - let SecPolyUniv (snas, sctx) = sec.sec_universes in - let sec_universes = SecPolyUniv (Array.append snas nas, UContext.union sctx ctx) in - { sec with sec_universes } + let on_sec sec = + if UContext.is_empty ctx then sec + else + let (snas, sctx) = sec.sec_poly_universes in + let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in + { sec with sec_poly_universes; has_poly_univs = true } + in + on_last_section on_sec s + +let is_polymorphic_univ u s = + let check sec = + let (_, uctx) = sec.sec_poly_universes in + Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx)) in - on_last_section { on_sec } s + List.exists check s let push_constraints uctx s = - let on_sec (type a) (kind : a section_kind) (sec : (a, _) section) : (a, _) section = match kind with - | SecMono -> - let SecMonoUniv uctx' = sec.sec_universes in - let sec_universes = SecMonoUniv (ContextSet.union uctx uctx') in - { sec with sec_universes } - | SecPoly -> - CErrors.anomaly (Pp.str "Adding monomorphic constraints to polymorphic section") + let on_sec sec = + if sec.has_poly_univs && Constraint.exists (fun (l,_,r) -> is_polymorphic_univ l s || is_polymorphic_univ r s) (snd uctx) + then CErrors.user_err Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes."); + let uctx' = sec.sec_mono_universes in + let sec_mono_universes = (ContextSet.union uctx uctx') in + { sec with sec_mono_universes } in - on_last_section { on_sec } s - -let open_section ~poly ~custom sections = - if poly then - let sec = { - sec_context = 0; - sec_universes = SecPolyUniv ([||], Univ.UContext.empty); - sec_entries = []; - sec_data = (Cmap.empty, Mindmap.empty); - sec_custom = custom; - } in - { sections with sec_poly = sec :: sections.sec_poly } - else if List.is_empty sections.sec_poly then - let sec = { - sec_context = 0; - sec_universes = SecMonoUniv Univ.ContextSet.empty; - sec_entries = []; - sec_data = (Cmap.empty, Mindmap.empty); - sec_custom = custom; - } in - { sections with sec_mono = sec :: sections.sec_mono } - else - CErrors.user_err (Pp.str "Cannot open a monomorphic section inside a polymorphic one") + on_last_section on_sec s + +let open_section ~custom sections = + let sec = { + sec_context = 0; + sec_mono_universes = ContextSet.empty; + sec_poly_universes = ([||], UContext.empty); + has_poly_univs = has_poly_univs sections; + sec_entries = []; + sec_data = (Cmap.empty, Mindmap.empty); + sec_custom = custom; + } in + sec :: sections let close_section sections = - match sections.sec_poly, sections.sec_mono with - | sec :: psecs, _ -> - let sections = { sections with sec_poly = psecs } in - sections, sec.sec_entries, Univ.ContextSet.empty, sec.sec_custom - | [], sec :: msecs -> - let sections = { sections with sec_mono = msecs } in - let SecMonoUniv cstrs = sec.sec_universes in - sections, sec.sec_entries, cstrs, sec.sec_custom - | [], [] -> + match sections with + | sec :: sections -> + sections, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom + | [] -> CErrors.user_err (Pp.str "No opened section.") -let same_poly (type a) ~poly (knd : a section_kind) = match knd with -| SecPoly -> poly -| SecMono -> not poly - -let drop_global (type a) : (a, _) section_universes -> (a, unit) section_universes = function -| SecMonoUniv _ -> SecMonoUniv () -| SecPolyUniv _ as u -> u +let make_decl_univs (nas,uctx) = abstract_universes nas uctx let push_global ~poly e s = if is_empty s then s + else if has_poly_univs s && not poly + then CErrors.user_err + Pp.(str "Cannot add a universe monomorphic declaration when \ + section polymorphic universes are present.") else - let on_sec knd sec = - if same_poly ~poly knd then { sec with + let on_sec sec = + { sec with sec_entries = e :: sec.sec_entries; - sec_data = add_emap e (drop_global sec.sec_universes) sec.sec_data; - } else - CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \ - monomorphic declarations in sections.") + sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data; + } in - on_last_section { on_sec } s + on_last_section on_sec s let push_constant ~poly con s = push_global ~poly (SecDefinition con) s @@ -171,8 +136,8 @@ let push_inductive ~poly ind s = push_global ~poly (SecInductive ind) s type abstr_info = { abstr_ctx : Constr.named_context; - abstr_subst : Univ.Instance.t; - abstr_uctx : Univ.AUContext.t; + abstr_subst : Instance.t; + abstr_uctx : AUContext.t; } let empty_segment = { @@ -181,51 +146,40 @@ let empty_segment = { abstr_uctx = AUContext.empty; } -let extract_hyps sec vars hyps = - (* FIXME: this code is fishy. It is supposed to check that declared section - variables are an ordered subset of the ambient ones, but it doesn't check - e.g. uniqueness of naming nor convertibility of the section data. *) - let rec aux ids hyps = match ids, hyps with - | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) -> - decl :: aux ids hyps - | _ :: ids, hyps -> - aux ids hyps - | [], _ -> [] - in - let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in - aux ids hyps +let extract_hyps sec vars used = + (* Keep the section-local segment of variables *) + let vars = List.firstn sec.sec_context vars in + (* Only keep the part that is used by the declaration *) + List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars let section_segment_of_entry vars e hyps sections = (* [vars] are the named hypotheses, [hyps] the subset that is declared by the global *) - let with_sec (type a) (s : (a section_kind * (a, _) section) option) = match s with + let with_sec s = match s with | None -> CErrors.user_err (Pp.str "No opened section.") - | Some (knd, sec) -> + | Some sec -> let hyps = extract_hyps sec vars hyps in - let inst, auctx = match knd, find_emap e sec.sec_data with - | SecMono, SecMonoUniv () -> - Instance.empty, AUContext.empty - | SecPoly, SecPolyUniv (nas, ctx) -> - Univ.abstract_universes nas ctx - in + let inst, auctx = find_emap e sec.sec_data in { abstr_ctx = hyps; abstr_subst = inst; abstr_uctx = auctx; } in - with_last_section { with_sec } sections + with_last_section with_sec sections let segment_of_constant env con s = let body = Environ.lookup_constant con env in let vars = Environ.named_context env in - section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s + let used = Context.Named.to_vars body.Declarations.const_hyps in + section_segment_of_entry vars (SecDefinition con) used s let segment_of_inductive env mind s = let mib = Environ.lookup_mind mind env in let vars = Environ.named_context env in - section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s + let used = Context.Named.to_vars mib.Declarations.mind_hyps in + section_segment_of_entry vars (SecInductive mind) used s let instance_from_variable_context = List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list @@ -237,18 +191,18 @@ let extract_worklist info = let replacement_context env s = let with_sec sec = match sec with | None -> CErrors.user_err (Pp.str "No opened section.") - | Some (_, sec) -> + | Some sec -> let cmap, imap = sec.sec_data in let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in (cmap, imap) in - with_last_section { with_sec } s + with_last_section with_sec s let is_in_section env gr s = let with_sec sec = match sec with | None -> false - | Some (_, sec) -> + | Some sec -> let open GlobRef in match gr with | VarRef id -> @@ -259,11 +213,4 @@ let is_in_section env gr s = | IndRef (ind, _) | ConstructRef ((ind, _), _) -> Mindmap.mem ind (snd sec.sec_data) in - with_last_section { with_sec } s - -let is_polymorphic_univ u s = - let check sec = - let SecPolyUniv (_, uctx) = sec.sec_universes in - Array.mem u (Instance.to_array (UContext.instance uctx)) - in - List.exists check s.sec_poly + with_last_section with_sec s diff --git a/kernel/section.mli b/kernel/section.mli index c1026a2980..fc3ac141e4 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -21,16 +21,13 @@ val empty : 'a t val is_empty : 'a t -> bool (** Checks whether there is no opened section *) -val is_polymorphic : 'a t -> bool -(** Checks whether last opened section is polymorphic *) - (** {6 Manipulating sections} *) type section_entry = | SecDefinition of Constant.t | SecInductive of MutInd.t -val open_section : poly:bool -> custom:'a -> 'a t -> 'a t +val open_section : custom:'a -> 'a t -> 'a t (** Open a new section with the provided universe polymorphic status. Sections can be nested, with the proviso that polymorphic sections cannot appear inside a monomorphic one. A custom data can be attached to this section, diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b65e62ba30..f70b2960cf 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -221,9 +221,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in - let check declared inferred = - let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in - let inferred_set, declared_set = mk_set inferred, mk_set declared in + let check declared_set inferred_set = if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in let n = List.length l in @@ -239,11 +237,6 @@ let build_constant_declaration env result = str "Proof using " ++ declared_vars ++ fnl () ++ str "to" ++ fnl () ++ str "Proof using " ++ inferred_vars) in - let sort l = - List.filter (fun decl -> - let id = NamedDecl.get_id decl in - List.exists (NamedDecl.get_id %> Names.Id.equal id) l) - (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in @@ -252,7 +245,7 @@ let build_constant_declaration env result = | None -> if List.is_empty context_ids then (* Empty section context: no need to check *) - [], def + Id.Set.empty, def else (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) @@ -264,16 +257,19 @@ let build_constant_declaration env result = (* Opaque definitions always come with their section variables *) assert false in - keep_hyps env (Id.Set.union ids_typ ids_def), def + Environ.really_needed env (Id.Set.union ids_typ ids_def), def | Some declared -> + let needed = Environ.really_needed env declared in + (* Transitive closure ensured by the upper layers *) + let () = assert (Id.Set.equal needed declared) in (* We use the declared set and chain a check of correctness *) - sort declared, + declared, match def with | Undef _ | Primitive _ as x -> x (* nothing to check *) | Def cs as x -> let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Mod_subst.force_constr cs) in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) @@ -281,12 +277,13 @@ let build_constant_declaration env result = let kont c = let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env c in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in check declared inferred in OpaqueDef (iter kont lc) in let univs = result.cook_universes in + let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in let tps = let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in Option.map Cemitcodes.from_val res @@ -317,7 +314,10 @@ let translate_recipe env _kn r = let univs = result.cook_universes in let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in let tps = Option.map Cemitcodes.from_val res in - { const_hyps = Option.get result.cook_context; + let hyps = Option.get result.cook_context in + (* Trust the set of section hypotheses generated by Cooking *) + let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in + { const_hyps = hyps; const_body = result.cook_body; const_type = result.cook_type; const_body_code = tps; diff --git a/lib/flags.ml b/lib/flags.ml index f09dc48f5d..7676665fe9 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -60,7 +60,7 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = V8_8 | V8_9 | Current +type compat_version = V8_8 | V8_9 | V8_10 | Current let compat_version = ref Current @@ -71,6 +71,9 @@ let version_compare v1 v2 = match v1, v2 with | V8_9, V8_9 -> 0 | V8_9, _ -> -1 | _, V8_9 -> 1 + | V8_10, V8_10 -> 0 + | V8_10, _ -> -1 + | _, V8_10 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 @@ -79,6 +82,7 @@ let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | V8_8 -> "8.8" | V8_9 -> "8.9" + | V8_10 -> "8.10" | Current -> "current" (* Translate *) diff --git a/lib/flags.mli b/lib/flags.mli index 185a5f8425..3f72cc4b91 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -48,7 +48,7 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -type compat_version = V8_8 | V8_9 | Current +type compat_version = V8_8 | V8_9 | V8_10 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/library/global.ml b/library/global.ml index 315a147d2c..c4685370d1 100644 --- a/library/global.ml +++ b/library/global.ml @@ -109,7 +109,7 @@ let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) -let open_section ~poly = globalize0 (Safe_typing.open_section ~poly) +let open_section () = globalize0 Safe_typing.open_section let close_section fs = globalize0_with_summary fs Safe_typing.close_section let start_module id = globalize (Safe_typing.start_module (i2l id)) diff --git a/library/global.mli b/library/global.mli index 26ccb90271..c45bf65d84 100644 --- a/library/global.mli +++ b/library/global.mli @@ -73,7 +73,7 @@ val add_include : (** Sections *) -val open_section : poly:bool -> unit +val open_section : unit -> unit (** [poly] is true when the section should be universe polymorphic *) val close_section : Summary.frozen -> unit diff --git a/library/lib.ml b/library/lib.ml index 1c6f82e8a6..991e23eb3a 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -464,8 +464,8 @@ let section_instance = let open GlobRef in function (*************) (* Sections. *) -let open_section ~poly id = - let () = Global.open_section ~poly in +let open_section id = + let () = Global.open_section () in let opp = !lib_state.path_prefix in let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in diff --git a/library/lib.mli b/library/lib.mli index 5ce601f2d3..d3315b0f2e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -147,7 +147,7 @@ val library_part : GlobRef.t -> DirPath.t (** {6 Sections } *) -val open_section : poly:bool -> Id.t -> unit +val open_section : Id.t -> unit val close_section : unit -> unit (** {6 We can get and set the state of the operations (used in [States]). } *) diff --git a/library/library.mllib b/library/library.mllib index c34d8911e8..a6188f7661 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -5,7 +5,6 @@ Summary Nametab Global Lib -Declaremods States Kindops Goptions diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ceb651abed..1772a3c333 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -50,6 +50,13 @@ let get_lia_option () = let get_lra_option () = !lra_proof_depth +(* Enable/disable caches *) + +let use_lia_cache = ref true +let use_nia_cache = ref true +let use_nra_cache = ref true +let use_csdp_cache = ref true + let () = let int_opt l vref = @@ -88,8 +95,38 @@ let () = optwrite = (fun x -> Certificate.dump_file := x) } in + let lia_cache_opt = + { + optdepr = false; + optname = "cache of lia (.lia.cache)"; + optkey = ["Lia" ; "Cache"]; + optread = (fun () -> !use_lia_cache); + optwrite = (fun x -> use_lia_cache := x) + } in + + let nia_cache_opt = + { + optdepr = false; + optname = "cache of nia (.nia.cache)"; + optkey = ["Nia" ; "Cache"]; + optread = (fun () -> !use_nia_cache); + optwrite = (fun x -> use_nia_cache := x) + } in + + let nra_cache_opt = + { + optdepr = false; + optname = "cache of nra (.nra.cache)"; + optkey = ["Nra" ; "Cache"]; + optread = (fun () -> !use_nra_cache); + optwrite = (fun x -> use_nra_cache := x) + } in + let () = declare_bool_option solver_opt in + let () = declare_bool_option lia_cache_opt in + let () = declare_bool_option nia_cache_opt in + let () = declare_bool_option nra_cache_opt in let () = declare_stringopt_option dump_file_opt in let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in @@ -745,7 +782,7 @@ struct (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) let eq_constr gl x y = let evd = gl.sigma in - match EConstr.eq_constr_universes gl.env evd x y with + match EConstr.eq_constr_universes_proj gl.env evd x y with | Some csts -> let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in begin @@ -769,15 +806,16 @@ struct ({vars=vars';gl=gl'}, CamlToCoq.positive n) let get_rank env v = - let evd = env.gl.sigma in + let gl = env.gl in let rec _get_rank env n = match env with | [] -> raise (Invalid_argument "get_rank") | e::l -> - if EConstr.eq_constr evd e v - then n - else _get_rank l (n+1) in + match eq_constr gl e v with + | Some _ -> n + | None -> _get_rank l (n+1) + in _get_rank env.vars 1 let elements env = env.vars @@ -1978,13 +2016,47 @@ type provername = string * int option open Persistent_cache -module Cache = PHashtable(struct - type t = (provername * micromega_polys) - let equal = (=) - let hash = Hashtbl.hash -end) -let csdp_cache = ".csdp.cache" +module MakeCache(T : sig type prover_option + type coeff + val hash_prover_option : int -> prover_option -> int + val hash_coeff : int -> coeff -> int + val eq_prover_option : prover_option -> prover_option -> bool + val eq_coeff : coeff -> coeff -> bool + + end) = + struct + module E = + struct + type t = T.prover_option * (T.coeff Mc.pol * Mc.op1) list + + let equal = Hash.(eq_pair T.eq_prover_option (CList.equal (eq_pair (eq_pol T.eq_coeff) Hash.eq_op1))) + + let hash = + let hash_cstr = Hash.(hash_pair (hash_pol T.hash_coeff) hash_op1) in + Hash.( (hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0) + end + + include PHashtable(E) + + let memo_opt use_cache cache_file f = + let memof = memo cache_file f in + fun x -> if !use_cache then memof x else f x + + end + + + +module CacheCsdp = MakeCache(struct + type prover_option = provername + type coeff = Mc.q + let hash_prover_option = Hash.(hash_pair hash_string + (hash_elt (Option.hash (fun x -> x)))) + let eq_prover_option = Hash.(eq_pair String.equal + (Option.equal Int.equal)) + let hash_coeff = Hash.hash_q + let eq_coeff = Hash.eq_q + end) (** * Build the command to call csdpcert, and launch it. This in turn will call @@ -2017,7 +2089,7 @@ let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivste *) let xcall_csdpcert = - Cache.memo csdp_cache (fun (prover,pb) -> really_call_csdpcert prover pb) + CacheCsdp.memo_opt use_csdp_cache ".csdp.cache" (fun (prover,pb) -> really_call_csdpcert prover pb) (** * Prover callback functions. @@ -2112,23 +2184,31 @@ let compact_pt pt f = let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Mc.denorm e , o) l) -module CacheZ = PHashtable(struct - type prover_option = bool * bool* int - type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) +module CacheZ = MakeCache(struct + type prover_option = bool * bool* int + type coeff = Mc.z + let hash_prover_option : int -> prover_option -> int = Hash.hash_elt Hashtbl.hash + let eq_prover_option : prover_option -> prover_option -> bool = (=) + let eq_coeff = Hash.eq_z + let hash_coeff = Hash.hash_z + end) -module CacheQ = PHashtable(struct - type t = int * ((Mc.q Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) +module CacheQ = MakeCache(struct + type prover_option = int + type coeff = Mc.q + let hash_prover_option : int -> int -> int = Hash.hash_elt Hashtbl.hash + let eq_prover_option = Int.equal + let eq_coeff = Hash.eq_q + let hash_coeff = Hash.hash_q + end) -let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) -let memo_nlia = CacheZ.memo ".nia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) -let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) +let memo_lia = CacheZ.memo_opt use_lia_cache ".lia.cache" + (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) +let memo_nlia = CacheZ.memo_opt use_nia_cache ".nia.cache" + (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) +let memo_nra = CacheQ.memo_opt use_nra_cache ".nra.cache" + (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) @@ -2154,63 +2234,63 @@ let linear_prover_R = { } let nlinear_prover_R = { - name = "nra"; - get_option = get_lra_option; - prover = memo_nra ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) + name = "nra"; + get_option = get_lra_option; + prover = memo_nra ; + hyps = hyps_of_cone ; + compact = compact_cone ; + pp_prf = pp_psatz pp_q ; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_Q str o = { - name = "real nonlinear prover"; + name = "real nonlinear prover"; get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) + prover = (fun (o,l) -> call_csdpcert_q o l); + hyps = hyps_of_cone; + compact = compact_cone ; + pp_prf = pp_psatz pp_q ; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_R str o = { - name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone; - pp_prf = pp_psatz pp_q; - pp_f = fun o x -> pp_pol pp_q o (fst x) + name = "real nonlinear prover"; + get_option = (fun () -> (str,o)); + prover = (fun (o,l) -> call_csdpcert_q o l); + hyps = hyps_of_cone; + compact = compact_cone; + pp_prf = pp_psatz pp_q; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_Z str o = { - name = "real nonlinear prover"; + name = "real nonlinear prover"; get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) + prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) } let linear_Z = { - name = "lia"; - get_option = get_lia_option; - prover = memo_zlinear_prover ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) + name = "lia"; + get_option = get_lia_option; + prover = memo_lia ; + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) } let nlinear_Z = { - name = "nlia"; - get_option = get_lia_option; - prover = memo_nlia ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) + name = "nlia"; + get_option = get_lia_option; + prover = memo_nlia ; + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) } (** diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 537b6175b4..39905f8c52 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -233,6 +233,13 @@ struct | Zpos p -> (positive_big_int p) | Zneg p -> minus_big_int (positive_big_int p) + let z x = + match x with + | Z0 -> 0 + | Zpos p -> index p + | Zneg p -> - (index p) + + let q_to_num {qnum = x ; qden = y} = Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y))) @@ -420,6 +427,80 @@ let command exe_path args vl = stdout_read; stdout_write; stderr_read; stderr_write]) +(** Hashing utilities *) + +module Hash = + struct + + module Mc = Micromega + + open Hashset.Combine + + let int_of_eq_op1 = Mc.(function + | Equal -> 0 + | NonEqual -> 1 + | Strict -> 2 + | NonStrict -> 3) + + let eq_op1 o1 o2 = int_of_eq_op1 o1 = int_of_eq_op1 o2 + + let hash_op1 h o = combine h (int_of_eq_op1 o) + + + let rec eq_positive p1 p2 = + match p1 , p2 with + | Mc.XH , Mc.XH -> true + | Mc.XI p1 , Mc.XI p2 -> eq_positive p1 p2 + | Mc.XO p1 , Mc.XO p2 -> eq_positive p1 p2 + | _ , _ -> false + + let eq_z z1 z2 = + match z1 , z2 with + | Mc.Z0 , Mc.Z0 -> true + | Mc.Zpos p1, Mc.Zpos p2 + | Mc.Zneg p1, Mc.Zneg p2 -> eq_positive p1 p2 + | _ , _ -> false + + let eq_q {Mc.qnum = qn1 ; Mc.qden = qd1} {Mc.qnum = qn2 ; Mc.qden = qd2} = + eq_z qn1 qn2 && eq_positive qd1 qd2 + + let rec eq_pol eq p1 p2 = + match p1 , p2 with + | Mc.Pc c1 , Mc.Pc c2 -> eq c1 c2 + | Mc.Pinj(i1,p1) , Mc.Pinj(i2,p2) -> eq_positive i1 i2 && eq_pol eq p1 p2 + | Mc.PX(p1,i1,p1') , Mc.PX(p2,i2,p2') -> + eq_pol eq p1 p2 && eq_positive i1 i2 && eq_pol eq p1' p2' + | _ , _ -> false + + + let eq_pair eq1 eq2 (x1,y1) (x2,y2) = + eq1 x1 x2 && eq2 y1 y2 + + + let hash_pol helt = + let rec hash acc = function + | Mc.Pc c -> helt (combine acc 1) c + | Mc.Pinj(p,c) -> hash (combine (combine acc 1) (CoqToCaml.index p)) c + | Mc.PX(p1,i,p2) -> hash (hash (combine (combine acc 2) (CoqToCaml.index i)) p1) p2 in + hash + + + let hash_pair h1 h2 h (e1,e2) = + h2 (h1 h e1) e2 + + let hash_elt f h e = combine h (f e) + + let hash_string h (e:string) = hash_elt Hashtbl.hash h e + + let hash_z = hash_elt CoqToCaml.z + + let hash_q = hash_elt (fun q -> Hashtbl.hash (CoqToCaml.q_to_num q)) + + end + + + + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index 8dbdea39e2..9692bc631b 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -67,14 +67,46 @@ end module CoqToCaml : sig val z_big_int : Micromega.z -> Big_int.big_int - val q_to_num : Micromega.q -> Num.num - val positive : Micromega.positive -> int - val n : Micromega.n -> int - val nat : Micromega.nat -> int - val index : Micromega.positive -> int + val z : Micromega.z -> int + val q_to_num : Micromega.q -> Num.num + val positive : Micromega.positive -> int + val n : Micromega.n -> int + val nat : Micromega.nat -> int + val index : Micromega.positive -> int end +module Hash : sig + + val eq_op1 : Micromega.op1 -> Micromega.op1 -> bool + + val eq_positive : Micromega.positive -> Micromega.positive -> bool + + val eq_z : Micromega.z -> Micromega.z -> bool + + val eq_q : Micromega.q -> Micromega.q -> bool + + val eq_pol : ('a -> 'a -> bool) -> 'a Micromega.pol -> 'a Micromega.pol -> bool + + val eq_pair : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> 'a * 'b -> 'a * 'b -> bool + + val hash_op1 : int -> Micromega.op1 -> int + + val hash_pol : (int -> 'a -> int) -> int -> 'a Micromega.pol -> int + + val hash_pair : (int -> 'a -> int) -> (int -> 'b -> int) -> int -> 'a * 'b -> int + + val hash_z : int -> Micromega.z -> int + + val hash_q : int -> Micromega.q -> int + + val hash_string : int -> string -> int + + val hash_elt : ('a -> int) -> int -> 'a -> int + +end + + val ppcm : Big_int.big_int -> Big_int.big_int -> Big_int.big_int val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 14a1bc9712..14e2e40846 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -127,7 +127,7 @@ let open_in f = match read_key_elem inch with | None -> () | Some (key,elem) -> - Table.replace htbl key elem ; + Table.add htbl key elem ; xload () in try (* Locking of the (whole) file while reading *) @@ -164,7 +164,7 @@ let add t k e = else let fd = descr_of_out_channel outch in begin - Table.replace tbl k e ; + Table.add tbl k e ; do_under_lock Write fd (fun _ -> Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fb0b1eca8d..c995887f31 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -38,11 +38,11 @@ type object_pr = { print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : bool -> ModPath.t -> Pp.t; - print_modtype : ModPath.t -> Pp.t; + print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } @@ -618,7 +618,7 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> @@ -639,17 +639,17 @@ let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as end | ModuleObject _ -> let (mp,l) = KerName.repr kn in - Some (print_module with_values (MPdot (mp,l))) + Some (print_module ~mod_ops with_values (MPdot (mp,l))) | ModuleTypeObject _ -> let (mp,l) = KerName.repr kn in - Some (print_modtype (MPdot (mp,l))) + Some (print_modtype ~mod_ops (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry indirect_accessor env sigma with_values ent = +let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry indirect_accessor env sigma with_values (oname,lobj) + gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> @@ -657,10 +657,10 @@ let gallina_print_library_entry indirect_accessor env sigma with_values ent = | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context indirect_accessor env sigma with_values = +let gallina_print_context ~mod_ops indirect_accessor env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry indirect_accessor env sigma with_values h with + (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -698,8 +698,8 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x let print_module x = !object_pr.print_module x let print_modtype x = !object_pr.print_modtype x let print_named_decl x = !object_pr.print_named_decl x -let print_library_entry x = !object_pr.print_library_entry x -let print_context x = !object_pr.print_context x +let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x +let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x let print_eval x = !object_pr.print_eval x @@ -720,10 +720,12 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context indirect_accessor env sigma = print_context indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ indirect_accessor env sigma = print_context indirect_accessor env sigma false None (Lib.contents ()) +let print_full_context ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) +let print_full_context_typ ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) -let print_full_pure_context ~library_accessor env sigma = +let print_full_pure_context ~mod_ops ~library_accessor env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with @@ -758,11 +760,11 @@ let print_full_pure_context ~library_accessor env sigma = | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _::rest -> prec rest | _ -> mt () in prec (Lib.contents ()) @@ -787,11 +789,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context indirect_accessor env sigma sec = - print_context indirect_accessor env sigma true None (read_sec_context sec) +let print_sec_context ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) -let print_sec_context_typ indirect_accessor env sigma sec = - print_context indirect_accessor env sigma false None (read_sec_context sec) +let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -801,7 +803,7 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name indirect_accessor env sigma na udecl = +let print_any_name ~mod_ops indirect_accessor env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with @@ -810,9 +812,10 @@ let print_any_name indirect_accessor env sigma na udecl = | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp | Syntactic kn -> print_syntactic_def env kn - | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp + | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> + print_module ~mod_ops (printable_body obj_dir) obj_mp | Dir _ -> mt () - | ModuleType mp -> print_modtype mp + | ModuleType mp -> print_modtype ~mod_ops mp | Other (obj, info) -> info.print obj | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) @@ -824,15 +827,15 @@ let print_any_name indirect_accessor env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name indirect_accessor env sigma na udecl = +let print_name ~mod_ops indirect_accessor env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name indirect_accessor env sigma + print_any_name ~mod_ops indirect_accessor env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name indirect_accessor env sigma (locate_any_name ref) udecl + print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl let print_opaque_name indirect_accessor env sigma qid = let open GlobRef in @@ -888,8 +891,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect indirect_accessor env sigma depth = - print_context indirect_accessor env sigma false (Some depth) (Lib.contents ()) +let inspect ~mod_ops indirect_accessor env sigma depth = + print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 4299bcc880..c8b361d95b 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -19,28 +19,35 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t val print_library_entry - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option val print_full_context - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_full_context_typ - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_full_pure_context - : library_accessor:Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> library_accessor:Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_sec_context - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_sec_context_typ - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : @@ -48,7 +55,8 @@ val print_eval : Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t val print_name - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_opaque_name @@ -69,7 +77,10 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> int -> Pp.t +val inspect + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -105,11 +116,11 @@ type object_pr = { print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : bool -> ModPath.t -> Pp.t; - print_modtype : ModPath.t -> Pp.t; + print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/printing/printmod.ml b/printing/printmod.ml index 141469ff9c..03921bca30 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -240,9 +240,14 @@ let nametab_register_body mp dir (l,body) = mip.mind_consnames) mib.mind_packets -let nametab_register_module_body mp struc = +type mod_ops = + { import_module : export:bool -> ModPath.t -> unit + ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + } + +let nametab_register_module_body ~mod_ops mp struc = (* If [mp] is a globally visible module, we simply import it *) - try Declaremods.import_module ~export:false mp + try mod_ops.import_module ~export:false mp with Not_found -> (* Otherwise we try to emulate an import by playing with nametab *) nametab_register_dir mp; @@ -252,7 +257,7 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with | Some (NoFunctor me) -> me | _ -> raise Not_found -let nametab_register_modparam mbid mtb = +let nametab_register_modparam ~mod_ops mbid mtb = let id = MBId.to_id mbid in match mtb.mod_type with | MoreFunctor _ -> id (* functorial param : nothing to register *) @@ -260,7 +265,7 @@ let nametab_register_modparam mbid mtb = (* We first try to use the algebraic type expression if any, via a Declaremods function that converts back to module entries *) try - let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in + let () = mod_ops.process_module_binding mbid (get_typ_expr_alg mtb) in id with e when CErrors.noncritical e -> (* Otherwise, we try to play with the nametab ourselves *) @@ -314,9 +319,9 @@ let print_body is_impl extent env mp (l,body) = let print_struct is_impl extent env mp struc = prlist_with_sep spc (print_body is_impl extent env mp) struc -let print_structure is_type extent env mp locals struc = +let print_structure ~mod_ops is_type extent env mp locals struc = let env' = Modops.add_structure mp struc Mod_subst.empty_delta_resolver env in - nametab_register_module_body mp struc; + nametab_register_module_body ~mod_ops mp struc; let kwd = if is_type then "Sig" else "Struct" in hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++ brk (1,-2) ++ keyword "End") @@ -362,31 +367,31 @@ let print_mod_expr env mp locals = function (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")") | MEwith _ -> assert false (* No 'with' syntax for modules *) -let rec print_functor fty fatom is_type extent env mp locals = function - | NoFunctor me -> fatom is_type extent env mp locals me +let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function + | NoFunctor me -> fatom ~mod_ops is_type extent env mp locals me | MoreFunctor (mbid,mtb1,me2) -> - let id = nametab_register_modparam mbid mtb1 in + let id = nametab_register_modparam ~mod_ops mbid mtb1 in let mp1 = MPbound mbid in - let pr_mtb1 = fty extent env mp1 locals mtb1 in + let pr_mtb1 = fty ~mod_ops extent env mp1 locals mtb1 in let env' = Modops.add_module_type mp1 mtb1 env in let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ - spc() ++ print_functor fty fatom is_type extent env' mp locals' me2) + spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2) -let rec print_expression x = - print_functor +let rec print_expression ~mod_ops x = + print_functor ~mod_ops print_modtype - (function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x + (fun ~mod_ops -> function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x -and print_signature x = - print_functor print_modtype print_structure x +and print_signature ~mod_ops x = + print_functor ~mod_ops print_modtype print_structure x -and print_modtype extent env mp locals mtb = match mtb.mod_type_alg with - | Some me -> print_expression true extent env mp locals me - | None -> print_signature true extent env mp locals mtb.mod_type +and print_modtype ~mod_ops extent env mp locals mtb = match mtb.mod_type_alg with + | Some me -> print_expression ~mod_ops true extent env mp locals me + | None -> print_signature ~mod_ops true extent env mp locals mtb.mod_type let rec printable_body dir = let dir = pop_dirpath dir in @@ -403,52 +408,52 @@ let rec printable_body dir = (** Since we might play with nametab above, we should reset to prior state after the printing *) -let print_expression' is_type extent env mp me = +let print_expression' ~mod_ops is_type extent env mp me = States.with_state_protection - (fun e -> print_expression is_type extent env mp [] e) me + (fun e -> print_expression ~mod_ops is_type extent env mp [] e) me -let print_signature' is_type extent env mp me = +let print_signature' ~mod_ops is_type extent env mp me = States.with_state_protection - (fun e -> print_signature is_type extent env mp [] e) me + (fun e -> print_signature ~mod_ops is_type extent env mp [] e) me -let unsafe_print_module extent env mp with_body mb = +let unsafe_print_module ~mod_ops extent env mp with_body mb = let name = print_modpath [] mp in let pr_equals = spc () ++ str ":= " in let body = match with_body, mb.mod_expr with | false, _ | true, Abstract -> mt() - | _, Algebraic me -> pr_equals ++ print_expression' false extent env mp me - | _, Struct sign -> pr_equals ++ print_signature' false extent env mp sign - | _, FullStruct -> pr_equals ++ print_signature' false extent env mp mb.mod_type + | _, Algebraic me -> pr_equals ++ print_expression' ~mod_ops false extent env mp me + | _, Struct sign -> pr_equals ++ print_signature' ~mod_ops false extent env mp sign + | _, FullStruct -> pr_equals ++ print_signature' ~mod_ops false extent env mp mb.mod_type in let modtype = match mb.mod_expr, mb.mod_type_alg with | FullStruct, _ -> mt () - | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true extent env mp ty - | _, _ -> brk (1,1) ++ str": " ++ print_signature' true extent env mp mb.mod_type + | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' ~mod_ops true extent env mp ty + | _, _ -> brk (1,1) ++ str": " ++ print_signature' ~mod_ops true extent env mp mb.mod_type in hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body) exception ShortPrinting -let print_module with_body mp = +let print_module ~mod_ops with_body mp = let me = Global.lookup_module mp in try if !short then raise ShortPrinting; - unsafe_print_module WithContents + unsafe_print_module ~mod_ops WithContents (Global.env ()) mp with_body me ++ fnl () with e when CErrors.noncritical e -> - unsafe_print_module OnlyNames + unsafe_print_module ~mod_ops OnlyNames (Global.env ()) mp with_body me ++ fnl () -let print_modtype kn = +let print_modtype ~mod_ops kn = let mtb = Global.lookup_modtype kn in let name = print_kn [] kn in hv 1 (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++ try if !short then raise ShortPrinting; - print_signature' true WithContents + print_signature' ~mod_ops true WithContents (Global.env ()) kn mtb.mod_type with e when CErrors.noncritical e -> - print_signature' true OnlyNames + print_signature' ~mod_ops true OnlyNames (Global.env ()) kn mtb.mod_type) diff --git a/printing/printmod.mli b/printing/printmod.mli index 8fd1cb4183..4c9245ee27 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -16,5 +16,11 @@ val printable_body : DirPath.t -> bool val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> UnivNames.univ_name_list option -> Pp.t -val print_module : bool -> ModPath.t -> Pp.t -val print_modtype : ModPath.t -> Pp.t + +type mod_ops = + { import_module : export:bool -> ModPath.t -> unit + ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + } + +val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t +val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t diff --git a/stm/stm.ml b/stm/stm.ml index 1042061021..b60c9c3dad 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1056,7 +1056,7 @@ end (* }}} *) (* Wrapper for the proof-closing special path for Qed *) let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t = set_id_for_feedback ?route dummy_doc id; - Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) + Vernacinterp.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly @@ -1083,7 +1083,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t = (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) else begin stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - Vernacentries.interp ?verbosely:(Some verbose) ~st expr + Vernacinterp.interp ?verbosely:(Some verbose) ~st expr end (****************************** CRUFT *****************************************) @@ -1970,7 +1970,7 @@ end = struct (* {{{ *) let stm_fail ~st fail f = if fail then - Vernacentries.with_fail ~st f + Vernacinterp.with_fail ~st f else f () @@ -2891,7 +2891,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) |> Exninfo.iraise else - let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in + let proof_mode = Some (Vernacinterp.get_default_proof_mode ()) in let id = VCS.new_node ~id:newtip proof_mode () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 8d600c2859..24976d8c1f 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -51,7 +51,7 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] let options_affecting_stm_scheduling = [ Attributes.universe_polymorphism_option_name; stm_allow_nested_proofs_option_name; - Vernacentries.proof_mode_opt_name; + Vernacinterp.proof_mode_opt_name; Attributes.program_mode_option_name; Proof_using.proof_using_opt_name; ] diff --git a/tactics/declare.ml b/tactics/declare.ml index 952ae023ad..b24a97e2d4 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -72,7 +72,7 @@ type constant_obj = { type 'a proof_entry = { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) - proof_entry_secctx : Constr.named_context option; + proof_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) proof_entry_feedback : Stateid.t option; proof_entry_type : Constr.types option; @@ -228,7 +228,7 @@ let cast_opaque_proof_entry e = ids_typ, vars in let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in - keep_hyps env (Id.Set.union hyp_typ hyp_def) + Environ.really_needed env (Id.Set.union hyp_typ hyp_def) | Some hyps -> hyps in { diff --git a/tactics/declare.mli b/tactics/declare.mli index 4cb876cecb..da66a2713c 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -23,7 +23,7 @@ open Entries type 'a proof_entry = { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) - proof_entry_secctx : Constr.named_context option; + proof_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) proof_entry_feedback : Stateid.t option; proof_entry_type : Constr.types option; diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index a2929e45cd..b723922642 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -36,7 +36,7 @@ type opacity_flag = Opaque | Transparent type t = { endline_tactic : Genarg.glob_generic_argument option - ; section_vars : Constr.named_context option + ; section_vars : Id.Set.t option ; proof : Proof.t ; udecl: UState.universe_decl (** Initial universe declarations *) @@ -128,7 +128,7 @@ let set_used_variables ps l = if not (Option.is_empty ps.section_vars) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), { ps with section_vars = Some ctx} + (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) } let get_open_goals ps = let Proof.{ goals; stack; shelf } = Proof.data ps.proof in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index d15e23c2cc..b9d1b37a11 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -17,7 +17,7 @@ type t (* Should be moved into a proper view *) val get_proof : t -> Proof.t val get_proof_name : t -> Names.Id.t -val get_used_variables : t -> Constr.named_context option +val get_used_variables : t -> Names.Id.Set.t option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : t -> UState.universe_decl diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v new file mode 100644 index 0000000000..25285622a9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9512.v @@ -0,0 +1,35 @@ +Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia. + +Set Primitive Projections. +Record params := { width : Z }. +Definition p : params := Build_params 64. + +Set Printing All. + +Goal width p = 0%Z -> width p = 0%Z. + intros. + + assert_succeeds (enough True; [omega|]). + assert_succeeds (enough True; [lia|]). + +(* H : @eq Z (width p) Z0 *) +(* ============================ *) +(* @eq Z (width p) Z0 *) + + change tt with tt in H. + +(* H : @eq Z (width p) Z0 *) +(* ============================ *) +(* @eq Z (width p) Z0 *) + + assert_succeeds (enough True; [lia|]). + (* Tactic failure: <tactic closure> fails. *) + (* assert_succeeds (enough True; [omega|]). *) + (* Tactic failure: <tactic closure> fails. *) + + (* omega. *) + (* Error: Omega can't solve this system *) + + lia. + (* Tactic failure: Cannot find witness. *) +Qed. diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v index 820022d995..27cb731151 100644 --- a/test-suite/bugs/opened/bug_1596.v +++ b/test-suite/bugs/opened/bug_1596.v @@ -69,9 +69,8 @@ Definition t := (X.t * Y.t)%type. elim (X.lt_not_eq H2 H3). elim H0;clear H0;intros. right. - split. - eauto. - eauto. + split; + eauto with ordered_type. Qed. Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). @@ -97,7 +96,7 @@ Definition t := (X.t * Y.t)%type. apply EQ. split;trivial. apply GT. - right;auto. + right;auto with ordered_type. apply GT. left;trivial. Defined. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index 74f94a9bed..d293dc0533 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -196,7 +196,7 @@ Definition clone_subType U v := Variable sT : subType. -CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). +Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). Lemma SubP u : Sub_spec u. Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed. @@ -209,7 +209,7 @@ Definition insub x := Definition insubd u0 x := odflt u0 (insub x). -CoInductive insub_spec x : option sT -> Type := +Variant insub_spec x : option sT -> Type := | InsubSome u of P x & val u = x : insub_spec x (Some u) | InsubNone of ~~ P x : insub_spec x None. @@ -568,7 +568,7 @@ Fixpoint nth s n {struct n} := Fixpoint rcons s z := if s is x :: s' then x :: rcons s' z else [:: z]. -CoInductive last_spec : seq T -> Type := +Variant last_spec : seq T -> Type := | LastNil : last_spec [::] | LastRcons s x : last_spec (rcons s x). @@ -1292,7 +1292,7 @@ Open Scope big_scope. (* packages both in in a term in which i occurs; it also depends on the *) (* iterated <op>, as this can give more information on the expected type of *) (* the <general_term>, thus allowing for the insertion of coercions. *) -CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R. +Variant bigbody R I := BigBody of I & (R -> R -> R) & bool & R. Definition applybig {R I} (body : bigbody R I) x := let: BigBody _ op b v := body in if b then op v x else x. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 81469d79c3..fd6101bf89 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq810. +Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index afeb57f9f2..f774cef44f 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(* -*- coq-prog-args: ("-compat" "8.9") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq811. Import Coq.Compat.Coq810. Import Coq.Compat.Coq89. -Import Coq.Compat.Coq88. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..20eef955b4 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq811. +Import Coq.Compat.Coq810. +Import Coq.Compat.Coq89. +Import Coq.Compat.Coq88. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index c8f75915c8..1c5ccc1a92 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq811. Import Coq.Compat.Coq810. -Import Coq.Compat.Coq89. diff --git a/test-suite/success/section_poly.v b/test-suite/success/section_poly.v new file mode 100644 index 0000000000..1e2201f2de --- /dev/null +++ b/test-suite/success/section_poly.v @@ -0,0 +1,74 @@ + + +Section Foo. + + Variable X : Type. + + Polymorphic Section Bar. + + Variable A : Type. + + Definition id (a:A) := a. + +End Bar. +Check id@{_}. +End Foo. +Check id@{_}. + +Polymorphic Section Foo. +Variable A : Type. +Section Bar. + Variable B : Type. + + Inductive prod := Prod : A -> B -> prod. +End Bar. +Check prod@{_}. +End Foo. +Check prod@{_ _}. + +Section Foo. + + Universe K. + Inductive bla := Bla : Type@{K} -> bla. + + Polymorphic Definition bli@{j} := Type@{j} -> bla. + + Definition bloo := bli@{_}. + + Polymorphic Universe i. + + Fail Definition x := Type. + Fail Inductive x : Type := . + Polymorphic Definition x := Type. + Polymorphic Inductive y : x := . + + Variable A : Type. (* adds a mono univ for the Type, which is unrelated to the others *) + + Fail Variable B : (y : Type@{i}). + (* not allowed: mono constraint (about a fresh univ for y) regarding + poly univ i *) + + Polymorphic Variable B : Type. (* new polymorphic stuff always OK *) + + Variable C : Type@{i}. (* no new univs so no problems *) + + Polymorphic Definition thing := bloo -> y -> A -> B. + +End Foo. +Check bli@{_}. +Check bloo@{}. + +Check thing@{_ _ _}. + +Section Foo. + + Polymorphic Universes i k. + Universe j. + Fail Constraint i < j. + Fail Constraint i < k. + + (* referring to mono univs in poly constraints is OK. *) + Polymorphic Constraint i < j. Polymorphic Constraint j < k. + + Polymorphic Definition foo := Type@{j}. +End Foo. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? diff --git a/theories/Compat/Coq810.v b/theories/Compat/Coq810.v index d24af2186f..c611d356ce 100644 --- a/theories/Compat/Coq810.v +++ b/theories/Compat/Coq810.v @@ -9,3 +9,5 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.10 *) + +Require Export Coq.Compat.Coq811. diff --git a/theories/Compat/Coq811.v b/theories/Compat/Coq811.v new file mode 100644 index 0000000000..4a9a041d4e --- /dev/null +++ b/theories/Compat/Coq811.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.11 *) diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 8627ff7353..7c69350db4 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -593,14 +593,14 @@ Qed. Lemma MapsTo_1 : forall m x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m. Proof. - induction m; simpl; intuition_in; eauto. + induction m; simpl; intuition_in; eauto with ordered_type. Qed. Hint Immediate MapsTo_1 : core. Lemma In_1 : forall m x y, X.eq x y -> In x m -> In y m. Proof. - intros m x y; induction m; simpl; intuition_in; eauto. + intros m x y; induction m; simpl; intuition_in; eauto with ordered_type. Qed. Lemma In_node_iff : @@ -671,7 +671,7 @@ Qed. Lemma lt_tree_trans : forall x y, X.lt x y -> forall m, lt_tree x m -> lt_tree y m. Proof. - eauto. + eauto with ordered_type. Qed. Lemma gt_tree_not_in : @@ -683,7 +683,7 @@ Qed. Lemma gt_tree_trans : forall x y, X.lt y x -> forall m, gt_tree x m -> gt_tree y m. Proof. - eauto. + eauto with ordered_type. Qed. Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. @@ -707,7 +707,7 @@ Qed. Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. Proof. destruct m as [|r x e l h]; simpl; auto. - intro H; elim (H x e); auto. + intro H; elim (H x e); auto with ordered_type. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. @@ -732,7 +732,7 @@ Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e. Proof. intros m x; functional induction (find x m); auto; intros; clearf; inv bst; intuition_in; simpl; auto; - try solve [order | absurd (X.lt x y); eauto | absurd (X.lt y x); eauto]. + try solve [order | absurd (X.lt x y); eauto with ordered_type | absurd (X.lt y x); eauto with ordered_type]. Qed. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. @@ -832,8 +832,8 @@ Lemma bal_bst : forall l x e r, bst l -> bst r -> Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; inv bst; repeat apply create_bst; auto; unfold create; try constructor; - (apply lt_tree_node || apply gt_tree_node); auto; - (eapply lt_tree_trans || eapply gt_tree_trans); eauto. + (apply lt_tree_node || apply gt_tree_node); auto with ordered_type; + (eapply lt_tree_trans || eapply gt_tree_trans); eauto with ordered_type. Qed. Hint Resolve bal_bst : core. @@ -865,7 +865,7 @@ Lemma add_in : forall m x y e, Proof. intros m x y e; functional induction (add x e m); auto; intros; try (rewrite bal_in, IHt); intuition_in. - apply In_1 with x; auto. + apply In_1 with x; auto with ordered_type. Qed. Lemma add_bst : forall m x e, bst m -> bst (add x e m). @@ -874,14 +874,14 @@ Proof. inv bst; try apply bal_bst; auto; intro z; rewrite add_in; intuition. apply MX.eq_lt with x; auto. - apply MX.lt_eq with x; auto. + apply MX.lt_eq with x; auto with ordered_type. Qed. Hint Resolve add_bst : core. Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. intros m x y e; functional induction (add x e m); - intros; inv bst; try rewrite bal_mapsto; unfold create; eauto. + intros; inv bst; try rewrite bal_mapsto; unfold create; eauto with ordered_type. Qed. Lemma add_2 : forall m x y e e', ~X.eq x y -> @@ -912,7 +912,7 @@ Proof. intros; rewrite find_mapsto_equiv; auto. split; eauto using add_2, add_3. destruct X.compare; try (apply H0; order). - auto using find_1, add_1. + auto using find_1, add_1 with ordered_type. Qed. (** * Extraction of minimum binding *) @@ -971,7 +971,7 @@ Proof. generalize (remove_min_in ll lx ld lr _x m#1). rewrite e0; simpl; intros. rewrite (bal_in l' x d r y) in H. - assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto); clear H4. + assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto with ordered_type); clear H4. assert (X.lt m#1 x) by order. decompose [or] H; order. Qed. @@ -1050,7 +1050,7 @@ Proof. (* EQ *) inv bst; clear e0. rewrite merge_in; intuition; [ order | order | intuition_in ]. - elim H4; eauto. + elim H4; eauto with ordered_type. (* GT *) inv bst; clear e0. rewrite bal_in; auto. @@ -1069,7 +1069,7 @@ Proof. destruct H; eauto. (* EQ *) inv bst. - apply merge_bst; eauto. + apply merge_bst; eauto with ordered_type. (* GT *) inv bst. apply bal_bst; auto. @@ -1124,8 +1124,8 @@ Lemma join_bst : forall l x d r, bst l -> bst r -> Proof. join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto; clear Hrl Hlr; intro; intros; rewrite join_in in *. - intuition; [ apply MX.lt_eq with x | ]; eauto. - intuition; [ apply MX.eq_lt with x | ]; eauto. + intuition; [ apply MX.lt_eq with x | ]; eauto with ordered_type. + intuition; [ apply MX.eq_lt with x | ]; eauto with ordered_type. Qed. Hint Resolve join_bst : core. @@ -1135,8 +1135,8 @@ Lemma join_find : forall l x d r y, Proof. join_tac; auto; inv bst; simpl (join (Leaf elt)); - try (assert (X.lt lx x) by auto); - try (assert (X.lt x rx) by auto); + try (assert (X.lt lx x) by auto with ordered_type); + try (assert (X.lt x rx) by auto with ordered_type); rewrite ?add_find, ?bal_find; auto. simpl; destruct X.compare; auto. @@ -1260,7 +1260,7 @@ Proof. change (bst (m2',xd)#1). rewrite <-e1; eauto. intros y Hy. apply H1; auto. - rewrite remove_min_in, e1; simpl; auto. + rewrite remove_min_in, e1; simpl; auto with ordered_type. change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto. Qed. Hint Resolve concat_bst : core. @@ -1283,9 +1283,9 @@ Proof. simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto. destruct (find y m2'); auto. symmetry; rewrite not_find_iff; auto; intro. - apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto. + apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto with ordered_type. - intros z Hz; apply H1; auto; rewrite H3; auto. + intros z Hz; apply H1; auto; rewrite H3; auto with ordered_type. Qed. @@ -1338,12 +1338,12 @@ Proof. apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6. destruct (elements_aux_mapsto r acc y' e'); intuition. red; simpl; eauto. - red; simpl; eauto. - intros. + red; simpl; eauto with ordered_type. + intros x e0 y0 H H6. inversion_clear H. destruct H7; simpl in *. order. - destruct (elements_aux_mapsto r acc x e0); intuition eauto. + destruct (elements_aux_mapsto r acc x e0); intuition eauto with ordered_type. Qed. Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s). @@ -1567,7 +1567,7 @@ Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt), MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. induction m; simpl; inversion_clear 1; auto. -exists k; auto. +exists k; auto with ordered_type. destruct (IHm1 _ _ H0). exists x0; intuition. destruct (IHm2 _ _ H0). @@ -2072,7 +2072,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). Proof. - destruct c; simpl; intros; P.MX.elim_comp; auto. + destruct c; simpl; intros; P.MX.elim_comp; auto with ordered_type. Qed. Hint Resolve cons_Cmp : core. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 1a531542cc..758f9d41b0 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1822,7 +1822,7 @@ Module OrdProperties (M:S). destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); auto. unfold O.ltk in *; simpl in *; intros. symmetry; rewrite H2. - apply ME.eq_lt with a; auto. + apply ME.eq_lt with a; auto with ordered_type. rewrite <- H1; auto. unfold O.ltk in *; simpl in *; intros. rewrite H1. @@ -1869,7 +1869,7 @@ Module OrdProperties (M:S). rewrite <- elements_mapsto_iff in H1. assert (~E.eq x t0). contradict H. - exists e0; apply MapsTo_1 with t0; auto. + exists e0; apply MapsTo_1 with t0; auto with ordered_type. ME.order. apply (@filter_sort _ eqke); auto with *; clean_eauto. intros. @@ -1888,9 +1888,9 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke, O.ltk; simpl. - destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto. + destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto with ordered_type. - elim H; exists e0; apply MapsTo_1 with t0; auto. - - fold (~E.lt t0 x); auto. + - fold (~E.lt t0 x); auto with ordered_type. Qed. Lemma elements_Add_Above : forall m m' x e, @@ -1905,7 +1905,7 @@ Module OrdProperties (M:S). destruct x0; destruct y. rewrite <- elements_mapsto_iff in H1. unfold O.eqke, O.ltk in *; simpl in *; destruct H3. - apply ME.lt_eq with x; auto. + apply ME.lt_eq with x; auto with ordered_type. apply H; firstorder. inversion H3. red; intros a; destruct a. @@ -1991,7 +1991,7 @@ Module OrdProperties (M:S). injection H as [= -> ->]. inversion_clear H1. red in H; simpl in *; intuition. - elim H0; eauto. + elim H0; eauto with ordered_type. inversion H. change (max_elt_aux (p::l) = Some (x,e)) in H. generalize (IHl x e H); clear IHl; intros IHl. @@ -2007,9 +2007,9 @@ Module OrdProperties (M:S). inversion_clear H2. inversion_clear H5. red in H2; simpl in H2; ME.order. - eapply IHl; eauto. + eapply IHl; eauto with ordered_type. econstructor; eauto. - red; eauto. + red; eauto with ordered_type. inversion H2; auto. Qed. @@ -2022,7 +2022,7 @@ Module OrdProperties (M:S). induction (elements m). simpl; try discriminate. destruct a; destruct l; simpl in *. - injection H; intros; subst; constructor; red; auto. + injection H; intros; subst; constructor; red; auto with ordered_type. constructor 2; auto. Qed. @@ -2069,7 +2069,7 @@ Module OrdProperties (M:S). destruct (elements m). simpl; try discriminate. destruct p; simpl in *. - injection H; intros; subst; constructor; red; auto. + injection H; intros; subst; constructor; red; auto with ordered_type. Qed. Lemma min_elt_Empty : @@ -2106,7 +2106,7 @@ Module OrdProperties (M:S). apply IHn. assert (S n = S (cardinal (remove k m))). rewrite Heqn. - eapply cardinal_2; eauto with map. + eapply cardinal_2; eauto with map ordered_type. inversion H1; auto. eapply max_elt_Above; eauto. @@ -2133,7 +2133,7 @@ Module OrdProperties (M:S). apply IHn. assert (S n = S (cardinal (remove k m))). rewrite Heqn. - eapply cardinal_2; eauto with map. + eapply cardinal_2; eauto with map ordered_type. inversion H1; auto. eapply min_elt_Below; eauto. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 8ca9401a06..0ef356b582 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -712,7 +712,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). Proof. - destruct c; simpl; intros; MX.elim_comp; auto. + destruct c; simpl; intros; MX.elim_comp; auto with ordered_type. Qed. Hint Resolve cons_Cmp : core. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index b21d809059..cad528644a 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -68,7 +68,7 @@ Proof. intros m. case m;auto. intros (k,e) l inlist. - absurd (InA eqke (k, e) ((k, e) :: l));auto. + absurd (InA eqke (k, e) ((k, e) :: l)); auto with ordered_type. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. @@ -106,14 +106,14 @@ Proof. elim (sort_inv sorted);auto. elim (In_inv belong1);auto. intro abs. - absurd (X.eq x k');auto. + absurd (X.eq x k'); auto with ordered_type. Qed. Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m. Proof. intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo. functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail). - exists _x; auto. + exists _x; auto with ordered_type. induction IHb; auto. exists x0; auto. inversion_clear sorted; auto. @@ -135,7 +135,7 @@ Function find (k:key) (s: t elt) {struct s} : option elt := Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. unfold PX.MapsTo. - functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto. + functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto with ordered_type. Qed. Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e. @@ -174,7 +174,7 @@ Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. intros m x y e; generalize y; clear y. unfold PX.MapsTo. - functional induction (add x e m);simpl;auto. + functional induction (add x e m);simpl;auto with ordered_type. Qed. Lemma add_2 : forall m x y e e', @@ -195,12 +195,12 @@ Qed. Lemma add_3 : forall m x y e e', ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. -Proof. +Proof with auto with ordered_type. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. functional induction (add x e' m);simpl; intros. - apply (In_inv_3 H0); compute; auto. - apply (In_inv_3 H0); compute; auto. - constructor 2; apply (In_inv_3 H0); compute; auto. + apply (In_inv_3 H0)... + apply (In_inv_3 H0)... + constructor 2; apply (In_inv_3 H0)... inversion_clear H0; auto. Qed. @@ -254,7 +254,7 @@ Proof. clear e0;inversion_clear Hm. apply Sort_Inf_NotIn with x0; auto. - apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto. + apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto with ordered_type. clear e0;inversion_clear Hm. assert (notin:~ In y (remove x l)) by auto. @@ -374,13 +374,13 @@ Definition Equivb cmp m m' := Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp, Equivb cmp m m' -> equal cmp m m' = true. -Proof. +Proof with auto with ordered_type. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; intuition; subst. match goal with H: X.compare _ _ = _ |- _ => clear H end. assert (cmp_e_e':cmp e e' = true). - apply H1 with x; auto. + apply H1 with x... rewrite cmp_e_e'; simpl. apply IHb; auto. inversion_clear Hm; auto. @@ -388,7 +388,7 @@ Proof. unfold Equivb; intuition. destruct (H0 k). assert (In k ((x,e) ::l)). - destruct H as (e'', hyp); exists e''; auto. + destruct H as (e'', hyp); exists e''... destruct (In_inv (H2 H4)); auto. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). @@ -396,20 +396,20 @@ Proof. apply MapsTo_eq with k; auto; order. destruct (H0 k). assert (In k ((x',e') ::l')). - destruct H as (e'', hyp); exists e''; auto. + destruct H as (e'', hyp); exists e''... destruct (In_inv (H3 H4)); auto. inversion_clear Hm'. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto. apply MapsTo_eq with k; auto; order. - apply H1 with k; destruct (X.eq_dec x k); auto. + apply H1 with k; destruct (X.eq_dec x k)... destruct (X.compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y. destruct (H0 x). assert (In x ((x',e')::l')). apply H; auto. - exists e; auto. + exists e... destruct (In_inv H3). order. inversion_clear Hm'. @@ -420,7 +420,7 @@ Proof. destruct (H0 x'). assert (In x' ((x,e)::l)). apply H2; auto. - exists e'; auto. + exists e'... destruct (In_inv H3). order. inversion_clear Hm. @@ -434,13 +434,13 @@ Proof. clear H1;destruct p as (k,e). destruct (H0 k). destruct H1. - exists e; auto. + exists e... inversion H1. destruct p as (x,e). destruct (H0 x). destruct H. - exists e; auto. + exists e... inversion H. destruct p;destruct p0;contradiction. @@ -449,7 +449,7 @@ Qed. Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, equal cmp m m' = true -> Equivb cmp m m'. -Proof. +Proof with auto with ordered_type. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; intuition; try discriminate; subst; @@ -464,16 +464,16 @@ Proof. exists e'; constructor; split; trivial; apply X.eq_trans with x; auto. destruct (H k). destruct (H9 H8) as (e'',hyp). - exists e''; auto. + exists e''... inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHb H1 H3 H6). destruct (In_inv H0). - exists e; constructor; split; trivial; apply X.eq_trans with x'; auto. + exists e; constructor; split; trivial; apply X.eq_trans with x'... destruct (H k). destruct (H10 H8) as (e'',hyp). - exists e''; auto. + exists e''... inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. @@ -615,7 +615,8 @@ Proof. inversion_clear 1. exists x'. destruct H0; simpl in *. - split; auto. + split. + auto with ordered_type. constructor 1. unfold eqke in *; simpl in *; intuition congruence. destruct IHm as (y, hyp); auto. @@ -946,7 +947,7 @@ Proof. destruct (IHm0 H0) as (_,H4); apply H4; auto. case_eq (find x m0); intros; auto. assert (eqk (elt:=oee') (k,(oo,oo')) (x,(oo,oo'))). - red; auto. + red; auto with ordered_type. destruct (Sort_Inf_NotIn H0 (Inf_eq (eqk_sym H5) H1)). exists p; apply find_2; auto. (* k < x *) @@ -1315,7 +1316,7 @@ Proof. apply (IHm1 H0 (Build_slist H5)); intuition. Qed. -Ltac cmp_solve := unfold eq, lt; simpl; try Raw.MX.elim_comp; auto. +Ltac cmp_solve := unfold eq, lt; simpl; try Raw.MX.elim_comp; auto with ordered_type. Definition compare : forall m1 m2, Compare lt eq m1 m2. Proof. diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 6e08c38a49..f0b31e6986 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -63,11 +63,11 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}. Proof. intros; exists (remove x s); intuition. - absurd (In x (remove x s)); auto with set. - apply In_1 with y; auto. + absurd (In x (remove x s)); auto with set ordered_type. + apply In_1 with y; auto with ordered_type. elim (E.eq_dec x y); intros; auto. - absurd (In x (remove x s)); auto with set. - apply In_1 with y; auto. + absurd (In x (remove x s)); auto with set ordered_type. + apply In_1 with y; auto with ordered_type. eauto with set. Qed. @@ -470,7 +470,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Hint Resolve elements_3 : core. Lemma elements_3w : forall s : t, NoDupA E.eq (elements s). - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Definition min_elt (s : t) : option elt := match min_elt s with diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index c6b2e0a09d..e500debc73 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -939,7 +939,7 @@ Module OrdProperties (M:S). generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto. intros. symmetry; rewrite H1. - apply ME.eq_lt with a; auto. + apply ME.eq_lt with a; auto with ordered_type. rewrite <- H0; auto. intros. rewrite H0. @@ -1013,7 +1013,7 @@ Module OrdProperties (M:S). intros. inversion_clear H2. rewrite <- elements_iff in H1. - apply ME.lt_eq with x; auto. + apply ME.lt_eq with x; auto with ordered_type. inversion H3. red; intros a. rewrite InA_app_iff, InA_cons, InA_nil by auto with *. @@ -1052,7 +1052,7 @@ Module OrdProperties (M:S). apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). - rewrite Heqn; apply cardinal_2 with e; auto with set. + rewrite Heqn; apply cardinal_2 with e; auto with set ordered_type. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. @@ -1073,7 +1073,7 @@ Module OrdProperties (M:S). apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). - rewrite Heqn; apply cardinal_2 with e; auto with set. + rewrite Heqn; apply cardinal_2 with e; auto with set ordered_type. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 566dd31a9e..a411c5e54e 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -26,6 +26,8 @@ Arguments LT [X lt eq x y] _. Arguments EQ [X lt eq x y] _. Arguments GT [X lt eq x y] _. +Create HintDb ordered_type. + Module Type MiniOrderedType. Parameter Inline t : Type. @@ -42,8 +44,8 @@ Module Type MiniOrderedType. Parameter compare : forall x y : t, Compare lt eq x y. - Hint Immediate eq_sym : core. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core. + Hint Immediate eq_sym : ordered_type. + Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : ordered_type. End MiniOrderedType. @@ -60,9 +62,9 @@ Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType. Include O. Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. - Proof. - intros; elim (compare x y); intro H; [ right | left | right ]; auto. - assert (~ eq y x); auto. + Proof with auto with ordered_type. + intros; elim (compare x y); intro H; [ right | left | right ]... + assert (~ eq y x)... Defined. End MOT_to_OT. @@ -79,31 +81,30 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_antirefl : forall x, ~ lt x x. Proof. - intros; intro; absurd (eq x x); auto. + intros; intro; absurd (eq x x); auto with ordered_type. Qed. Instance lt_strorder : StrictOrder lt. Proof. split; [ exact lt_antirefl | exact lt_trans]. Qed. Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. - Proof. + Proof with auto with ordered_type. intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. - elim (lt_not_eq H); apply eq_trans with z; auto. - elim (lt_not_eq (lt_trans Hlt H)); auto. + elim (lt_not_eq H); apply eq_trans with z... + elim (lt_not_eq (lt_trans Hlt H))... Qed. Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. - Proof. + Proof with auto with ordered_type. intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. - elim (lt_not_eq H0); apply eq_trans with x; auto. - elim (lt_not_eq (lt_trans H0 Hlt)); auto. + elim (lt_not_eq H0); apply eq_trans with x... + elim (lt_not_eq (lt_trans H0 Hlt))... Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. apply proper_sym_impl_iff_2; auto with *. intros x x' Hx y y' Hy H. - apply eq_lt with x; auto. + apply eq_lt with x; auto with ordered_type. apply lt_eq with y; auto. Qed. @@ -143,9 +144,9 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed. Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed. - Hint Resolve gt_not_eq eq_not_lt : core. - Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : core. - Hint Resolve eq_not_gt lt_antirefl lt_not_gt : core. + Hint Resolve gt_not_eq eq_not_lt : ordered_type. + Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : ordered_type. + Hint Resolve eq_not_gt lt_antirefl lt_not_gt : ordered_type. Lemma elim_compare_eq : forall x y : t, @@ -197,7 +198,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. Proof. - intros; elim (compare x y); [ left | right | right ]; auto. + intros; elim (compare x y); [ left | right | right ]; auto with ordered_type. Defined. Definition eqb x y : bool := if eq_dec x y then true else false. @@ -247,8 +248,8 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed. End ForNotations. -Hint Resolve ListIn_In Sort_NoDup Inf_lt : core. -Hint Immediate In_eq Inf_lt : core. +Hint Resolve ListIn_In Sort_NoDup Inf_lt : ordered_type. +Hint Immediate In_eq Inf_lt : ordered_type. End OrderedTypeFacts. @@ -266,8 +267,8 @@ Module KeyOrderedType(O:OrderedType). eq (fst p) (fst p') /\ (snd p) = (snd p'). Definition ltk (p p':key*elt) := lt (fst p) (fst p'). - Hint Unfold eqk eqke ltk : core. - Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Unfold eqk eqke ltk : ordered_type. + Hint Extern 2 (eqke ?a ?b) => split : ordered_type. (* eqke is stricter than eqk *) @@ -283,35 +284,35 @@ Module KeyOrderedType(O:OrderedType). Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. Proof. auto. Qed. - Hint Immediate ltk_right_r ltk_right_l : core. + Hint Immediate ltk_right_r ltk_right_l : ordered_type. (* eqk, eqke are equalities, ltk is a strict order *) Lemma eqk_refl : forall e, eqk e e. - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Lemma eqke_refl : forall e, eqke e e. - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. Proof. unfold eqke; intuition. Qed. Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. - Proof. eauto. Qed. + Proof. eauto with ordered_type. Qed. Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. Proof. - unfold eqke; intuition; [ eauto | congruence ]. + unfold eqke; intuition; [ eauto with ordered_type | congruence ]. Qed. Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''. - Proof. eauto. Qed. + Proof. eauto with ordered_type. Qed. Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. - Proof. unfold eqk, ltk; auto. Qed. + Proof. unfold eqk, ltk; auto with ordered_type. Qed. Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. Proof. @@ -319,18 +320,18 @@ Module KeyOrderedType(O:OrderedType). exact (lt_not_eq H H1). Qed. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. - Hint Immediate eqk_sym eqke_sym : core. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type. + Hint Immediate eqk_sym eqke_sym : ordered_type. Global Instance eqk_equiv : Equivalence eqk. - Proof. constructor; eauto. Qed. + Proof. constructor; eauto with ordered_type. Qed. Global Instance eqke_equiv : Equivalence eqke. - Proof. split; eauto. Qed. + Proof. split; eauto with ordered_type. Qed. Global Instance ltk_strorder : StrictOrder ltk. - Proof. constructor; eauto. intros x; apply (irreflexivity (x:=fst x)). Qed. + Proof. constructor; eauto with ordered_type. intros x; apply (irreflexivity (x:=fst x)). Qed. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. @@ -348,45 +349,45 @@ Module KeyOrderedType(O:OrderedType). Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'. Proof. - unfold eqk, ltk; simpl; auto. + unfold eqk, ltk; simpl; auto with ordered_type. Qed. Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''. - Proof. eauto. Qed. + Proof. eauto with ordered_type. Qed. Lemma eqk_ltk : forall e e' e'', eqk e e' -> ltk e' e'' -> ltk e e''. Proof. intros (k,e) (k',e') (k'',e''). - unfold ltk, eqk; simpl; eauto. + unfold ltk, eqk; simpl; eauto with ordered_type. Qed. - Hint Resolve eqk_not_ltk : core. - Hint Immediate ltk_eqk eqk_ltk : core. + Hint Resolve eqk_not_ltk : ordered_type. + Hint Immediate ltk_eqk eqk_ltk : ordered_type. Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. unfold eqke; induction 1; intuition. Qed. - Hint Resolve InA_eqke_eqk : core. + Hint Resolve InA_eqke_eqk : ordered_type. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. Notation Sort := (sort ltk). Notation Inf := (lelistA ltk). - Hint Unfold MapsTo In : core. + Hint Unfold MapsTo In : ordered_type. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. - Proof. + Proof with auto with ordered_type. firstorder. - exists x; auto. + exists x... induction H. - destruct y. - exists e; auto. + destruct y. + exists e... destruct IHInA as [e H0]. - exists e; auto. + exists e... Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. @@ -405,8 +406,8 @@ Module KeyOrderedType(O:OrderedType). Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. - Hint Immediate Inf_eq : core. - Hint Resolve Inf_lt : core. + Hint Immediate Inf_eq : ordered_type. + Hint Resolve Inf_lt : ordered_type. Lemma Sort_Inf_In : forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. @@ -420,8 +421,8 @@ Module KeyOrderedType(O:OrderedType). intros; red; intros. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). - eapply Sort_Inf_In; eauto. - red; simpl; auto. + eapply Sort_Inf_In; eauto with ordered_type. + red; simpl; auto with ordered_type. Qed. Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. @@ -437,7 +438,7 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'. Proof. - inversion_clear 2; auto. + inversion_clear 2; auto with ordered_type. left; apply Sort_In_cons_1 with l; auto. Qed. @@ -451,7 +452,7 @@ Module KeyOrderedType(O:OrderedType). Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. inversion 1. - inversion_clear H0; eauto. + inversion_clear H0; eauto with ordered_type. destruct H1; simpl in *; intuition. Qed. @@ -469,19 +470,19 @@ Module KeyOrderedType(O:OrderedType). End Elt. - Hint Unfold eqk eqke ltk : core. - Hint Extern 2 (eqke ?a ?b) => split : core. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. - Hint Immediate eqk_sym eqke_sym : core. - Hint Resolve eqk_not_ltk : core. - Hint Immediate ltk_eqk eqk_ltk : core. - Hint Resolve InA_eqke_eqk : core. - Hint Unfold MapsTo In : core. - Hint Immediate Inf_eq : core. - Hint Resolve Inf_lt : core. - Hint Resolve Sort_Inf_NotIn : core. - Hint Resolve In_inv_2 In_inv_3 : core. + Hint Unfold eqk eqke ltk : ordered_type. + Hint Extern 2 (eqke ?a ?b) => split : ordered_type. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type. + Hint Immediate eqk_sym eqke_sym : ordered_type. + Hint Resolve eqk_not_ltk : ordered_type. + Hint Immediate ltk_eqk eqk_ltk : ordered_type. + Hint Resolve InA_eqke_eqk : ordered_type. + Hint Unfold MapsTo In : ordered_type. + Hint Immediate Inf_eq : ordered_type. + Hint Resolve Inf_lt : ordered_type. + Hint Resolve Sort_Inf_NotIn : ordered_type. + Hint Resolve In_inv_2 In_inv_3 : ordered_type. End KeyOrderedType. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index 9b99fa5de4..a8e6993a63 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -178,7 +178,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Lemma eq_refl : forall x : t, eq x x. Proof. - intros (x1,x2); red; simpl; auto. + intros (x1,x2); red; simpl; auto with ordered_type. Qed. Lemma eq_sym : forall x y : t, eq x y -> eq y x. @@ -188,16 +188,16 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. Proof. - intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. + intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto with ordered_type. Qed. Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition. - left; eauto. + left; eauto with ordered_type. left; eapply MO1.lt_eq; eauto. left; eapply MO1.eq_lt; eauto. - right; split; eauto. + right; split; eauto with ordered_type. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. @@ -214,7 +214,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. destruct (O2.compare x2 y2). apply LT; unfold lt; auto. apply EQ; unfold eq; auto. - apply GT; unfold lt; auto. + apply GT; unfold lt; auto with ordered_type. apply GT; unfold lt; auto. Defined. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 113b1fb5d7..acbd96f699 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -178,7 +178,8 @@ let add_compat_require opts v = match v with | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false) | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) - | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) + | Flags.V8_10 -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) + | Flags.Current -> add_vo_require opts "Coq.Compat.Coq811" None (Some false) let add_load_vernacular opts verb s = { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} @@ -497,7 +498,7 @@ let parse_args ~help ~init arglist : t * string list = { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true }}} - |"-test-mode" -> Vernacentries.test_mode := true; oval + |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-bt" -> Backtrace.record_backtrace true; oval |"-color" -> set_color oval (next ()) diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 7658ad68a5..642dc94ab2 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -54,7 +54,10 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in let library_accessor = Library.indirect_accessor in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~library_accessor env) sigma) ++ fnl ()) + let mod_ops = { Printmod.import_module = Declaremods.import_module + ; process_module_binding = Declaremods.process_module_binding + } in + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~mod_ops ~library_accessor env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v index d808436e13..d808436e13 100755..100644 --- a/user-contrib/Ltac2/Bool.v +++ b/user-contrib/Ltac2/Bool.v diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 88454ff2fb..88454ff2fb 100755..100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v diff --git a/library/declaremods.ml b/vernac/declaremods.ml index b4dc42bdfe..58a7dff5fd 100644 --- a/library/declaremods.ml +++ b/vernac/declaremods.ml @@ -35,8 +35,6 @@ type inline = | DefaultInline | InlineAt of int -type module_kind = Module | ModType | ModAny - let default_inline () = Some (Flags.get_inline_level ()) let inl2intopt = function @@ -457,15 +455,15 @@ let rec compute_subst env mbids sign mp_l inl = | _,[] -> mbids,empty_subst | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") | mbid::mbids,mp::mp_l -> - let farg_id, farg_b, fbody_b = Modops.destr_functor sign in - let mb = Environ.lookup_module mp env in - let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in - let resolver = + let farg_id, farg_b, fbody_b = Modops.destr_functor sign in + let mb = Environ.lookup_module mp env in + let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in + let resolver = if Modops.is_functor mb.mod_type then empty_delta_resolver else Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta - in - mbid_left,join (map_mbid mbid mp resolver) subst + in + mbid_left,join (map_mbid mbid mp resolver) subst (** Create the objects of a "with Module" structure. *) @@ -547,11 +545,11 @@ let process_module_binding mbid me = Objects in these parameters are also loaded. Output is accumulated on top of [acc] (in reverse order). *) -let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = +let intern_arg (acc, cst) (idl,(typ,ann)) = let inl = inl2intopt ann in let lib_dir = Lib.library_dp() in let env = Global.env() in - let (mty, _, cst') = interp_modast env ModType typ in + let (mty, _, cst') = Modintern.interp_module_ast env Modintern.ModType typ in let () = Global.push_context_set true cst' in let env = Global.env () in let sobjs = get_module_sobjs false env inl mty in @@ -579,8 +577,8 @@ let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = be more efficient and independent of [List.map] eval order. *) -let intern_args interp_modast params = - List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params +let intern_args params = + List.fold_left intern_arg ([], Univ.ContextSet.empty) params (** {6 Auxiliary functions concerning subtyping checks} *) @@ -588,10 +586,10 @@ let intern_args interp_modast params = let check_sub mtb sub_mtb_l = (* The constraints are checked and forgot immediately : *) ignore (List.fold_right - (fun sub_mtb env -> - Environ.add_constraints - (Subtyping.check_subtypes env mtb sub_mtb) env) - sub_mtb_l (Global.env())) + (fun sub_mtb env -> + Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) env) + sub_mtb_l (Global.env())) (** This function checks if the type calculated for the module [mp] is a subtype of all signatures in [sub_mtb_l]. Uses only the global @@ -631,11 +629,11 @@ let mk_funct_type env args seb0 = (** Prepare the module type list for check of subtypes *) -let build_subtypes interp_modast env mp args mtys = +let build_subtypes env mp args mtys = let (cst, ans) = List.fold_left_map (fun cst (m,ann) -> let inl = inl2intopt ann in - let mte, _, cst' = interp_modast env ModType m in + let mte, _, cst' = Modintern.interp_module_ast env Modintern.ModType m in let env = Environ.push_context_set ~strict:true cst' env in let cst = Univ.ContextSet.union cst cst' in let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in @@ -673,22 +671,22 @@ let openmodtype_info = module RawModOps = struct -let start_module interp_modast export id args res fs = +let start_module export id args res fs = let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let env = Global.env () in let res_entry_o, subtyps, cst = match res with | Enforce (res,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType res in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType res in let env = Environ.push_context_set ~strict:true cst env in (* We check immediately that mte is well-formed *) let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in let cst = Univ.ContextSet.union cst cst' in Some (mte, inl), [], cst | Check resl -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in + let typs, cst = build_subtypes env mp arg_entries_r resl in None, typs, cst in let () = Global.push_context_set true cst in @@ -735,25 +733,25 @@ let end_module () = mp -let declare_module interp_modast id args res mexpr_o fs = +let declare_module id args res mexpr_o fs = (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let params = mk_params_entry arg_entries_r in let env = Global.env () in let env = Environ.push_context_set ~strict:true cst env in let mty_entry_o, subs, inl_res, cst' = match res with | Enforce (mty,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType mty in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType mty in let env = Environ.push_context_set ~strict:true cst env in (* We check immediately that mte is well-formed *) let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in let cst = Univ.ContextSet.union cst cst' in Some mte, [], inl, cst | Check mtys -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let typs, cst = build_subtypes env mp arg_entries_r mtys in None, typs, default_inline (), cst in let env = Environ.push_context_set ~strict:true cst' env in @@ -761,7 +759,7 @@ let declare_module interp_modast id args res mexpr_o fs = let mexpr_entry_o, inl_expr, cst' = match mexpr_o with | None -> None, default_inline (), Univ.ContextSet.empty | Some (mexpr,ann) -> - let (mte, _, cst) = interp_modast env Module mexpr in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.Module mexpr in Some mte, inl2intopt ann, cst in let env = Environ.push_context_set ~strict:true cst' env in @@ -803,12 +801,12 @@ end module RawModTypeOps = struct -let start_modtype interp_modast id args mtys fs = +let start_modtype id args mtys fs = let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let env = Global.env () in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in let () = Global.push_context_set true cst in openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in @@ -831,16 +829,16 @@ let end_modtype () = mp -let declare_modtype interp_modast id args mtys (mty,ann) fs = +let declare_modtype id args mtys (mty,ann) fs = let inl = inl2intopt ann in (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let mte, _, cst = interp_modast env ModType mty in + let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in let () = Global.push_context_set true cst in let env = Global.env () in (* We check immediately that mte is well-formed *) @@ -848,7 +846,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = let () = Global.push_context_set true cst in let env = Global.env () in let entry = params, mte in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in let () = Global.push_context_set true cst in let env = Global.env () in let sobjs = get_functor_sobjs false env inl entry in @@ -902,12 +900,12 @@ let type_of_incl env is_mod = function decompose_functor mp_l (type_of_mod mp0 env is_mod) |MEwith _ -> raise NoIncludeSelf -let declare_one_include interp_modast (me_ast,annot) = +let declare_one_include (me_ast,annot) = let env = Global.env() in - let me, kind, cst = interp_modast env ModAny me_ast in + let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in let () = Global.push_context_set true cst in let env = Global.env () in - let is_mod = (kind == Module) in + let is_mod = (kind == Modintern.Module) in let cur_mp = Lib.current_mp () in let inl = inl2intopt annot in let mbids,aobjs = get_module_sobjs is_mod env inl me in @@ -925,8 +923,7 @@ let declare_one_include interp_modast (me_ast,annot) = let aobjs = subst_aobjs subst aobjs in ignore (add_leaf (Lib.current_mod_id ()) (IncludeObject aobjs)) -let declare_include interp me_asts = - List.iter (declare_one_include interp) me_asts +let declare_include me_asts = List.iter declare_one_include me_asts end @@ -942,40 +939,40 @@ let protect_summaries f = let () = Summary.unfreeze_summaries fs in iraise reraise -let start_module interp export id args res = - protect_summaries (RawModOps.start_module interp export id args res) +let start_module export id args res = + protect_summaries (RawModOps.start_module export id args res) let end_module = RawModOps.end_module -let declare_module interp id args mtys me_l = +let declare_module id args mtys me_l = let declare_me fs = match me_l with - | [] -> RawModOps.declare_module interp id args mtys None fs - | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs + | [] -> RawModOps.declare_module id args mtys None fs + | [me] -> RawModOps.declare_module id args mtys (Some me) fs | me_l -> - ignore (RawModOps.start_module interp None id args mtys fs); - RawIncludeOps.declare_include interp me_l; - RawModOps.end_module () + ignore (RawModOps.start_module None id args mtys fs); + RawIncludeOps.declare_include me_l; + RawModOps.end_module () in protect_summaries declare_me -let start_modtype interp id args mtys = - protect_summaries (RawModTypeOps.start_modtype interp id args mtys) +let start_modtype id args mtys = + protect_summaries (RawModTypeOps.start_modtype id args mtys) let end_modtype = RawModTypeOps.end_modtype -let declare_modtype interp id args mtys mty_l = +let declare_modtype id args mtys mty_l = let declare_mt fs = match mty_l with | [] -> assert false - | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs + | [mty] -> RawModTypeOps.declare_modtype id args mtys mty fs | mty_l -> - ignore (RawModTypeOps.start_modtype interp id args mtys fs); - RawIncludeOps.declare_include interp mty_l; - RawModTypeOps.end_modtype () + ignore (RawModTypeOps.start_modtype id args mtys fs); + RawIncludeOps.declare_include mty_l; + RawModTypeOps.end_modtype () in protect_summaries declare_mt -let declare_include interp me_asts = - protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts) +let declare_include me_asts = + protect_summaries (fun _ -> RawIncludeOps.declare_include me_asts) (** {6 Libraries} *) @@ -1055,12 +1052,7 @@ let iter_all_segments f = (** {6 Some types used to shorten declaremods.mli} *) -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list +type module_params = (lident list * (Constrexpr.module_ast * inline)) list (** {6 Debug} *) diff --git a/library/declaremods.mli b/vernac/declaremods.mli index b7c7cd1dba..ae84704656 100644 --- a/library/declaremods.mli +++ b/vernac/declaremods.mli @@ -29,34 +29,24 @@ type inline = (** Kinds of modules *) -type module_kind = Module | ModType | ModAny +type module_params = (lident list * (Constrexpr.module_ast * inline)) list -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** [declare_module interp_modast id fargs typ exprs] - declares module [id], with structure constructed by [interp_modast] - from functor arguments [fargs], with final type [typ]. - [exprs] is usually of length 1 (Module definition with a concrete - body), but it could also be empty ("Declare Module", with non-empty [typ]), - or multiple (body of the shape M <+ N <+ ...). *) +(** [declare_module id fargs typ exprs] declares module [id], from + functor arguments [fargs], with final type [typ]. [exprs] is + usually of length 1 (Module definition with a concrete body), but + it could also be empty ("Declare Module", with non-empty [typ]), or + multiple (body of the shape M <+ N <+ ...). *) val declare_module : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_module : - 'modast module_interpretor -> bool option -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> ModPath.t val end_module : unit -> ModPath.t @@ -68,18 +58,16 @@ val end_module : unit -> ModPath.t Similar to [declare_module], except that the types could be multiple *) val declare_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> - ('modast * inline) list -> + module_params -> + (Constrexpr.module_ast * inline) list -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) list -> ModPath.t val end_modtype : unit -> ModPath.t @@ -117,8 +105,7 @@ val import_modules : export:bool -> ModPath.t list -> unit (** Include *) -val declare_include : - 'modast module_interpretor -> ('modast * inline) list -> unit +val declare_include : (Constrexpr.module_ast * inline) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 8a94a010a0..efcb2635be 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -62,7 +62,8 @@ let make_bullet s = | _ -> assert false let parse_compat_version = let open Flags in function - | "8.10" -> Current + | "8.11" -> Current + | "8.10" -> V8_10 | "8.9" -> V8_9 | "8.8" -> V8_8 | ("8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ea34b601e8..c335d3ad55 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1079,9 +1079,7 @@ let explain_incorrect_with_in_module () = let explain_incorrect_module_application () = str "Illegal application to a module type." -open Modintern - -let explain_module_internalization_error = function +let explain_module_internalization_error = let open Modintern in function | NotAModuleNorModtype s -> explain_not_module_nor_modtype s | IncorrectWithInModule -> explain_incorrect_with_in_module () | IncorrectModuleApplication -> explain_incorrect_module_application () diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 42d1a1f3fc..c7a588d2b4 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -359,7 +359,7 @@ let save_lemma_admitted ~(lemma : t) : unit = let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in let ids_def = Environ.global_vars_set env pproof in - Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) + Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None in let universes = Proof_global.get_initial_euctx lemma.proof in let ctx = UState.check_univ_decl ~poly universes udecl in diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index cd13f83e96..03bf008529 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,6 +1,7 @@ Vernacexpr Attributes Pvernac +Declaremods G_vernac G_proofs Vernacprop @@ -31,10 +32,9 @@ ComFixpoint ComProgramFixpoint Record Assumptions -Vernacstate Mltop Topfmt Loadpath Vernacentries - -Misctypes +Vernacstate +Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 43b58d6d4b..40786fe0b4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -35,12 +35,6 @@ module NamedDecl = Context.Named.Declaration (** TODO: make this function independent of Ltac *) let (f_interp_redexp, interp_redexp_hook) = Hook.make () -let debug = false - -(* XXX Should move to a common library *) -let vernac_pperr_endline pp = - if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () - (* Utility functions, at some point they should all disappear and instead enviroment/state selection should be done at the Vernac DSL level. *) @@ -468,28 +462,6 @@ let vernac_notation ~atts = let vernac_custom_entry ~module_local s = Metasyntax.declare_custom_entry module_local s -(* Default proof mode, to be set at the beginning of proofs for - programs that cannot be statically classified. *) -let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) -let get_default_proof_mode () = !default_proof_mode - -let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode -let set_default_proof_mode_opt name = - default_proof_mode := - match Pvernac.lookup_proof_mode name with - | Some pm -> pm - | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)) - -let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let () = - Goptions.declare_string_option Goptions.{ - optdepr = false; - optname = "default proof mode" ; - optkey = proof_mode_opt_name; - optread = get_default_proof_mode_opt; - optwrite = set_default_proof_mode_opt; - } - (***********) (* Gallina *) @@ -872,10 +844,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = if not (Option.is_empty export) then user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = - Declaremods.declare_module Modintern.interp_module_ast - id binders_ast (Declaremods.Enforce mty_ast) [] - in + let mp = Declaremods.declare_module id binders_ast (Declaremods.Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export @@ -892,10 +861,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in - let mp = - Declaremods.start_module Modintern.interp_module_ast - export id binders_ast mty_ast_o - in + let mp = Declaremods.start_module export id binders_ast mty_ast_o in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Interactive Module " ++ Id.print id ++ str " started"); @@ -911,7 +877,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = - Declaremods.declare_module Modintern.interp_module_ast + Declaremods.declare_module id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef ?loc mp "mod"; @@ -938,10 +904,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in - let mp = - Declaremods.start_modtype Modintern.interp_module_ast - id binders_ast mty_sign - in + let mp = Declaremods.start_modtype id binders_ast mty_sign in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Interactive Module Type " ++ Id.print id ++ str " started"); @@ -957,10 +920,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if not (Option.is_empty export) then user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = - Declaremods.declare_modtype Modintern.interp_module_ast - id binders_ast mty_sign mty_ast_l - in + let mp = Declaremods.declare_modtype id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") @@ -970,8 +930,7 @@ let vernac_end_modtype {loc;v=id} = Dumpglob.dump_modref ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") -let vernac_include l = - Declaremods.declare_include Modintern.interp_module_ast l +let vernac_include l = Declaremods.declare_include l (**********************) (* Gallina extensions *) @@ -980,7 +939,9 @@ let vernac_include l = let vernac_begin_section ~poly ({v=id} as lid) = Dumpglob.dump_definition lid true "sec"; - Lib.open_section ~poly id; + Lib.open_section id; + (* If there was no polymorphism attribute this just sets the option + to its current value ie noop. *) set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly let vernac_end_section {CAst.loc} = @@ -1966,26 +1927,29 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = + let mod_ops = { Printmod.import_module = Declaremods.import_module + ; process_module_binding = Declaremods.process_module_binding + } in let sigma, env = get_current_or_global_context ~pstate in function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ Library.indirect_accessor env sigma - | PrintSectionContext qid -> print_sec_context_typ Library.indirect_accessor env sigma qid - | PrintInspect n -> inspect Library.indirect_accessor env sigma n + | PrintFullContext-> print_full_context_typ ~mod_ops Library.indirect_accessor env sigma + | PrintSectionContext qid -> print_sec_context_typ ~mod_ops Library.indirect_accessor env sigma qid + | PrintInspect n -> inspect ~mod_ops Library.indirect_accessor env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () - | PrintModule qid -> print_module qid - | PrintModuleType qid -> print_modtype qid + | PrintModule qid -> print_module ~mod_ops qid + | PrintModuleType qid -> print_modtype ~mod_ops qid | PrintNamespace ns -> print_namespace ~pstate ns | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name Library.indirect_accessor env sigma qid udecl + print_name ~mod_ops Library.indirect_accessor env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() @@ -2245,115 +2209,9 @@ let vernac_check_guard ~pstate = (str ("Condition violated: ") ++s) in message -(** A global default timeout, controlled by option "Set Default Timeout n". - Use "Unset Default Timeout" to deactivate it (or set it to 0). *) - -let default_timeout = ref None - -(* Timeout *) -let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b = - match !default_timeout, timeout with - | _, Some n - | Some n, None -> - Control.timeout n f x Timeout - | None, None -> - f x - -(* Fail *) -let test_mode = ref false - -(* Restoring the state is the caller's responsibility *) -let with_fail f : (Pp.t, unit) result = - try - let _ = f () in - Error () - with - (* Fail Timeout is a common pattern so we need to support it. *) - | e when CErrors.noncritical e || e = Timeout -> - (* The error has to be printed in the failing state *) - Ok CErrors.(iprint (push e)) - -(* We restore the state always *) -let with_fail ~st f = - let res = with_fail f in - Vernacstate.invalidate_cache (); - Vernacstate.unfreeze_interp_state st; - match res with - | Error () -> - user_err ~hdr:"Fail" (str "The command has not failed!") - | Ok msg -> - if not !Flags.quiet || !test_mode - then Feedback.msg_notice (str "The command has indeed failed with message:" ++ fnl () ++ msg) - -let locate_if_not_already ?loc (e, info) = - match Loc.get_loc info with - | None -> (e, Option.cata (Loc.add_loc info) info loc) - | Some l -> (e, info) - -let mk_time_header = - (* Drop the time header to print the command, we should indeed use a - different mechanism to `-time` commands than the current hack of - adding a time control to the AST. *) - let pr_time_header vernac = - let vernac = match vernac with - | { v = { control = ControlTime _ :: control; attrs; expr }; loc } -> - CAst.make ?loc { control; attrs; expr } - | _ -> vernac - in - Topfmt.pr_cmd_header vernac - in - fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac) - -let interp_control_flag ~time_header (f : control_flag) ~st - (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) = - match f with - | ControlFail -> - with_fail ~st (fun () -> fn ~st); - st.Vernacstate.lemmas - | ControlTimeout timeout -> - vernac_timeout ~timeout (fun () -> fn ~st) () - | ControlTime batch -> - let header = if batch then Lazy.force time_header else Pp.mt () in - System.with_time ~batch ~header (fun () -> fn ~st) () - | ControlRedirect s -> - Topfmt.with_output_to_file s (fun () -> fn ~st) () - -(* EJGA: We may remove this, only used twice below *) -let vernac_require_open_lemma ~stack f = - match stack with - | Some stack -> f stack - | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)") - -let interp_typed_vernac c ~stack = - let open Vernacextend in - match c with - | VtDefault f -> f (); stack - | VtNoProof f -> - if Option.has_some stack then - user_err Pp.(str "Command not supported (Open proofs remain)"); - let () = f () in - stack - | VtCloseProof f -> - vernac_require_open_lemma ~stack (fun stack -> - let lemma, stack = Vernacstate.LemmaStack.pop stack in - f ~lemma; - stack) - | VtOpenProof f -> - Some (Vernacstate.LemmaStack.push stack (f ())) - | VtModifyProof f -> - Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack - | VtReadProofOpt f -> - let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in - f ~pstate; - stack - | VtReadProof f -> - vernac_require_open_lemma ~stack - (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate)); - stack - (* We interpret vernacular commands to a DSL that specifies their allowed actions on proof states *) -let rec translate_vernac ~atts v = let open Vernacextend in match v with +let translate_vernac ~atts v = let open Vernacextend in match v with | VernacAbortAll | VernacRestart | VernacUndo _ @@ -2363,6 +2221,9 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacBack _ | VernacAbort _ -> anomaly (str "type_vernac") + | VernacLoad _ -> + anomaly (str "Load is not supported recursively") + (* Syntax *) | VernacSyntaxExtension (infix, sl) -> VtDefault(fun () -> with_module_locality ~atts vernac_syntax_extension infix sl) @@ -2664,141 +2525,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacEndProof pe -> VtCloseProof (vernac_end_proof pe) - | VernacLoad (verbosely,fname) -> - VtNoProof(fun () -> - unsupported_attributes atts; - vernac_load ~verbosely fname) - (* Extensions *) | VernacExtend (opn,args) -> Vernacextend.type_vernac ~atts opn args - -(* "locality" is the prefix "Local" attribute, while the "local" component - * is the outdated/deprecated "Local" attribute of some vernacular commands - * still parsed as the obsolete_locality grammar entry for retrocompatibility. - * loc is the Loc.t of the vernacular command being interpreted. *) -and interp_expr ~atts ~st c = - let stack = st.Vernacstate.lemmas in - vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); - match c with - - (* The STM should handle that, but LOAD bypasses the STM... *) - | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") - | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") - | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") - | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") - - (* Resetting *) - | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") - | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") - | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") - - (* This one is possible to handle here *) - | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - - | v -> - let fv = translate_vernac ~atts v in - interp_typed_vernac ~stack fv - -(* XXX: This won't properly set the proof mode, as of today, it is - controlled by the STM. Thus, we would need access information from - the classifier. The proper fix is to move it to the STM, however, - the way the proof mode is set there makes the task non trivial - without a considerable amount of refactoring. -*) -and vernac_load ~verbosely fname = - let exception End_of_input in - - (* Note that no proof should be open here, so the state here is just token for now *) - let st = Vernacstate.freeze_interp_state ~marshallable:false in - let fname = - Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in - let fname = CUnix.make_suffix fname ".v" in - let input = - let longfname = Loadpath.locate_file fname in - let in_chan = open_utf8_file_in longfname in - Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in - (* Parsing loop *) - let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing - (fun po -> - match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with - | Some x -> x - | None -> raise End_of_input) in - let rec load_loop ~stack = - try - let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in - let stack = - v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) - (parse_sentence proof_mode input) in - load_loop ~stack - with - End_of_input -> - stack - in - let stack = load_loop ~stack:st.Vernacstate.lemmas in - (* If Load left a proof open, we fail too. *) - if Option.has_some stack then - CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); - () - -and interp_control ~st ({ v = cmd } as vernac) = - let time_header = mk_time_header vernac in - List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) - cmd.control - (fun ~st -> - let before_univs = Global.universes () in - let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in - if before_univs == Global.universes () then pstack - else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack) - ~st - -(* Interpreting a possibly delayed proof *) -let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = - let stack = st.Vernacstate.lemmas in - let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in - let () = match pe with - | Admitted -> - save_lemma_admitted_delayed ~proof ~info - | Proved (_,idopt) -> - save_lemma_proved_delayed ~proof ~info ~idopt in - stack - -let interp_qed_delayed_control ~proof ~info ~st ~control { loc; v=pe } = - let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in - List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) - control - (fun ~st -> interp_qed_delayed ~proof ~info ~st pe) - ~st - -(* General interp with management of state *) -let () = - declare_int_option - { optdepr = false; - optname = "the default timeout"; - optkey = ["Default";"Timeout"]; - optread = (fun () -> !default_timeout); - optwrite = ((:=) default_timeout) } - -(* Be careful with the cache here in case of an exception. *) -let interp_gen ~verbosely ~st ~interp_fn cmd = - Vernacstate.unfreeze_interp_state st; - try vernac_timeout (fun st -> - let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let ontop = v_mod (interp_fn ~st) cmd in - Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; - Vernacstate.freeze_interp_state ~marshallable:false - ) st - with exn -> - let exn = CErrors.push exn in - let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in - Vernacstate.invalidate_cache (); - iraise exn - -(* Regular interp *) -let interp ?(verbosely=true) ~st cmd = - interp_gen ~verbosely ~st ~interp_fn:interp_control cmd - -let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t = - interp_gen ~verbosely:false ~st - ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index e65f9d3cfe..6368ebeed8 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,25 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** The main interpretation function of vernacular expressions *) -val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t - -(** Execute a Qed but with a proof_object which may contain a delayed - proof and won't be forced *) -val interp_qed_delayed_proof - : proof:Proof_global.proof_object - -> info:Lemmas.Info.t - -> st:Vernacstate.t - -> control:Vernacexpr.control_flag list - -> Vernacexpr.proof_end CAst.t - -> Vernacstate.t - -(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) -val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit - -(** Flag set when the test-suite is called. Its only effect to display - verbose information for [Fail] *) -val test_mode : bool ref +(** Vernac Translation into the Vernac DSL *) +val translate_vernac + : atts:Attributes.vernac_flags + -> Vernacexpr.vernac_expr + -> Vernacextend.typed_vernac (** Vernacular require command *) val vernac_require : @@ -38,8 +24,3 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr (** Miscellaneous stuff *) val command_focus : unit Proof.focus_kind - -(** Default proof mode set by `start_proof` *) -val get_default_proof_mode : unit -> Pvernac.proof_mode - -val proof_mode_opt_name : string list diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 2725516a76..e29086d726 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -54,7 +54,6 @@ and proof_block_name = string (** open type of delimiters *) type typed_vernac = | VtDefault of (unit -> unit) - | VtNoProof of (unit -> unit) | VtCloseProof of (lemma:Lemmas.t -> unit) | VtOpenProof of (unit -> Lemmas.t) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml new file mode 100644 index 0000000000..c14fc78462 --- /dev/null +++ b/vernac/vernacinterp.ml @@ -0,0 +1,278 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Vernacexpr + +(* XXX Should move to a common library *) +let debug = false +let vernac_pperr_endline pp = + if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () + +(* EJGA: We may remove this, only used twice below *) +let vernac_require_open_lemma ~stack f = + match stack with + | Some stack -> f stack + | None -> + CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress)") + +let interp_typed_vernac c ~stack = + let open Vernacextend in + match c with + | VtDefault f -> f (); stack + | VtNoProof f -> + if Option.has_some stack then + CErrors.user_err (Pp.str "Command not supported (Open proofs remain)"); + let () = f () in + stack + | VtCloseProof f -> + vernac_require_open_lemma ~stack (fun stack -> + let lemma, stack = Vernacstate.LemmaStack.pop stack in + f ~lemma; + stack) + | VtOpenProof f -> + Some (Vernacstate.LemmaStack.push stack (f ())) + | VtModifyProof f -> + Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack + | VtReadProofOpt f -> + let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in + f ~pstate; + stack + | VtReadProof f -> + vernac_require_open_lemma ~stack + (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate)); + stack + +(* Default proof mode, to be set at the beginning of proofs for + programs that cannot be statically classified. *) +let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) +let get_default_proof_mode () = !default_proof_mode + +let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode +let set_default_proof_mode_opt name = + default_proof_mode := + match Pvernac.lookup_proof_mode name with + | Some pm -> pm + | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)) + +let proof_mode_opt_name = ["Default";"Proof";"Mode"] +let () = + Goptions.declare_string_option Goptions.{ + optdepr = false; + optname = "default proof mode" ; + optkey = proof_mode_opt_name; + optread = get_default_proof_mode_opt; + optwrite = set_default_proof_mode_opt; + } + +(** A global default timeout, controlled by option "Set Default Timeout n". + Use "Unset Default Timeout" to deactivate it (or set it to 0). *) + +let default_timeout = ref None + +(* Timeout *) +let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b = + match !default_timeout, timeout with + | _, Some n + | Some n, None -> + Control.timeout n f x CErrors.Timeout + | None, None -> + f x + +(* Fail *) +let test_mode = ref false + +(* Restoring the state is the caller's responsibility *) +let with_fail f : (Pp.t, unit) result = + try + let _ = f () in + Error () + with + (* Fail Timeout is a common pattern so we need to support it. *) + | e when CErrors.noncritical e || e = CErrors.Timeout -> + (* The error has to be printed in the failing state *) + Ok CErrors.(iprint (push e)) + +(* We restore the state always *) +let with_fail ~st f = + let res = with_fail f in + Vernacstate.invalidate_cache (); + Vernacstate.unfreeze_interp_state st; + match res with + | Error () -> + CErrors.user_err ~hdr:"Fail" (Pp.str "The command has not failed!") + | Ok msg -> + if not !Flags.quiet || !test_mode + then Feedback.msg_notice Pp.(str "The command has indeed failed with message:" ++ fnl () ++ msg) + +let locate_if_not_already ?loc (e, info) = + match Loc.get_loc info with + | None -> (e, Option.cata (Loc.add_loc info) info loc) + | Some l -> (e, info) + +let mk_time_header = + (* Drop the time header to print the command, we should indeed use a + different mechanism to `-time` commands than the current hack of + adding a time control to the AST. *) + let pr_time_header vernac = + let vernac = match vernac with + | { CAst.v = { control = ControlTime _ :: control; attrs; expr }; loc } -> + CAst.make ?loc { control; attrs; expr } + | _ -> vernac + in + Topfmt.pr_cmd_header vernac + in + fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac) + +let interp_control_flag ~time_header (f : control_flag) ~st + (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) = + match f with + | ControlFail -> + with_fail ~st (fun () -> fn ~st); + st.Vernacstate.lemmas + | ControlTimeout timeout -> + vernac_timeout ~timeout (fun () -> fn ~st) () + | ControlTime batch -> + let header = if batch then Lazy.force time_header else Pp.mt () in + System.with_time ~batch ~header (fun () -> fn ~st) () + | ControlRedirect s -> + Topfmt.with_output_to_file s (fun () -> fn ~st) () + +(* "locality" is the prefix "Local" attribute, while the "local" component + * is the outdated/deprecated "Local" attribute of some vernacular commands + * still parsed as the obsolete_locality grammar entry for retrocompatibility. + * loc is the Loc.t of the vernacular command being interpreted. *) +let rec interp_expr ~atts ~st c = + let stack = st.Vernacstate.lemmas in + vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); + match c with + + (* The STM should handle that, but LOAD bypasses the STM... *) + | VernacAbortAll -> CErrors.user_err (Pp.str "AbortAll cannot be used through the Load command") + | VernacRestart -> CErrors.user_err (Pp.str "Restart cannot be used through the Load command") + | VernacUndo _ -> CErrors.user_err (Pp.str "Undo cannot be used through the Load command") + | VernacUndoTo _ -> CErrors.user_err (Pp.str "UndoTo cannot be used through the Load command") + + (* Resetting *) + | VernacResetName _ -> CErrors.anomaly (Pp.str "VernacResetName not handled by Stm.") + | VernacResetInitial -> CErrors.anomaly (Pp.str "VernacResetInitial not handled by Stm.") + | VernacBack _ -> CErrors.anomaly (Pp.str "VernacBack not handled by Stm.") + + (* This one is possible to handle here *) + | VernacAbort id -> CErrors.user_err (Pp.str "Abort cannot be used through the Load command") + | VernacLoad (verbosely, fname) -> + Attributes.unsupported_attributes atts; + vernac_load ~verbosely fname + | v -> + let fv = Vernacentries.translate_vernac ~atts v in + interp_typed_vernac ~stack fv + +and vernac_load ~verbosely fname = + let exception End_of_input in + + (* Note that no proof should be open here, so the state here is just token for now *) + let st = Vernacstate.freeze_interp_state ~marshallable:false in + let fname = + Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (Pp.str x)) fname in + let fname = CUnix.make_suffix fname ".v" in + let input = + let longfname = Loadpath.locate_file fname in + let in_chan = Util.open_utf8_file_in longfname in + Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in + (* Parsing loop *) + let v_mod = if verbosely then Flags.verbosely else Flags.silently in + let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing + (fun po -> + match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with + | Some x -> x + | None -> raise End_of_input) in + let rec load_loop ~stack = + try + let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in + let stack = + v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) + (parse_sentence proof_mode input) in + load_loop ~stack + with + End_of_input -> + stack + in + let stack = load_loop ~stack:st.Vernacstate.lemmas in + (* If Load left a proof open, we fail too. *) + if Option.has_some stack then + CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); + stack + +and interp_control ~st ({ CAst.v = cmd } as vernac) = + let time_header = mk_time_header vernac in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + cmd.control + (fun ~st -> + let before_univs = Global.universes () in + let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in + if before_univs == Global.universes () then pstack + else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack) + ~st + +(* XXX: This won't properly set the proof mode, as of today, it is + controlled by the STM. Thus, we would need access information from + the classifier. The proper fix is to move it to the STM, however, + the way the proof mode is set there makes the task non trivial + without a considerable amount of refactoring. +*) + +(* Interpreting a possibly delayed proof *) +let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = + let stack = st.Vernacstate.lemmas in + let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in + let () = match pe with + | Admitted -> + Lemmas.save_lemma_admitted_delayed ~proof ~info + | Proved (_,idopt) -> + Lemmas.save_lemma_proved_delayed ~proof ~info ~idopt in + stack + +let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } = + let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + control + (fun ~st -> interp_qed_delayed ~proof ~info ~st pe) + ~st + +(* General interp with management of state *) +let () = let open Goptions in + declare_int_option + { optdepr = false; + optname = "the default timeout"; + optkey = ["Default";"Timeout"]; + optread = (fun () -> !default_timeout); + optwrite = ((:=) default_timeout) } + +(* Be careful with the cache here in case of an exception. *) +let interp_gen ~verbosely ~st ~interp_fn cmd = + Vernacstate.unfreeze_interp_state st; + try vernac_timeout (fun st -> + let v_mod = if verbosely then Flags.verbosely else Flags.silently in + let ontop = v_mod (interp_fn ~st) cmd in + Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; + Vernacstate.freeze_interp_state ~marshallable:false + ) st + with exn -> + let exn = CErrors.push exn in + let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in + Vernacstate.invalidate_cache (); + Util.iraise exn + +(* Regular interp *) +let interp ?(verbosely=true) ~st cmd = + interp_gen ~verbosely ~st ~interp_fn:interp_control cmd + +let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t = + interp_gen ~verbosely:false ~st + ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli new file mode 100644 index 0000000000..16849686da --- /dev/null +++ b/vernac/vernacinterp.mli @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** The main interpretation function of vernacular expressions *) +val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t + +(** Execute a Qed but with a proof_object which may contain a delayed + proof and won't be forced *) +val interp_qed_delayed_proof + : proof:Proof_global.proof_object + -> info:Lemmas.Info.t + -> st:Vernacstate.t + -> control:Vernacexpr.control_flag list + -> Vernacexpr.proof_end CAst.t + -> Vernacstate.t + +(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) +val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit + +(** Flag set when the test-suite is called. Its only effect to display + verbose information for [Fail] *) +val test_mode : bool ref + +(** Default proof mode set by `start_proof` *) +val get_default_proof_mode : unit -> Pvernac.proof_mode +val proof_mode_opt_name : string list |