diff options
34 files changed, 476 insertions, 222 deletions
@@ -42,6 +42,8 @@ Tactics in the OCaml run-time system. - The tactics "dtauto", "dintuition", "firstorder" now handle inductive types with let bindings in the parameters. +- The tactic "dtauto" now handles some inductives such as + "@sigT A (fun _ => B)" as non-dependent conjunctions. Focusing @@ -51,6 +53,9 @@ Focusing Vernacular Commands +- Proofs ending in "Qed exporting ident, .., ident" are not supported + anymore. Constants generated during `abstract` are kept private to the + local environment. - The deprecated Coercion Local, Open Local Scope, Notation Local syntax was removed. Use Local as a prefix instead. - For the Extraction Language command, "OCaml" is spelled correctly. @@ -68,6 +73,11 @@ Checker - The checker now accepts filenames in addition to logical paths. +CoqIDE + +- Find and Replace All report the number of occurrences found; Find indicates + when it wraps. + Documentation - The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been diff --git a/clib/clib.mllib b/clib/clib.mllib index bd5ddb152..0b5d9826f 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -12,6 +12,7 @@ CString CStack Int +Range HMap Bigint diff --git a/clib/range.ml b/clib/range.ml new file mode 100644 index 000000000..86a078633 --- /dev/null +++ b/clib/range.ml @@ -0,0 +1,91 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type 'a tree = +| Leaf of 'a +| Node of 'a * 'a tree * 'a tree + +type 'a t = Nil | Cons of int * 'a tree * 'a t + +let oob () = invalid_arg "index out of bounds" + +let empty = Nil + +let cons x l = match l with +| Cons (h1, t1, Cons (h2, t2, rem)) -> + if Int.equal h1 h2 then Cons (1 + h1 + h2, Node (x, t1, t2), rem) + else Cons (1, Leaf x, l) +| _ -> Cons (1, Leaf x, l) + +let is_empty = function +| Nil -> true +| _ -> false + +let rec tree_get h t i = match t with +| Leaf x -> + if i = 0 then x else oob () +| Node (x, t1, t2) -> + if i = 0 then x + else + let h = h / 2 in + if i <= h then tree_get h t1 (i - 1) else tree_get h t2 (i - h - 1) + +let rec get l i = match l with +| Nil -> oob () +| Cons (h, t, rem) -> + if i < h then tree_get h t i else get rem (i - h) + +let length l = + let rec length accu = function + | Nil -> accu + | Cons (h, _, l) -> length (h + accu) l + in + length 0 l + +let rec tree_map f = function +| Leaf x -> Leaf (f x) +| Node (x, t1, t2) -> Node (f x, tree_map f t1, tree_map f t2) + +let rec map f = function +| Nil -> Nil +| Cons (h, t, l) -> Cons (h, tree_map f t, map f l) + +let rec tree_fold_left f accu = function +| Leaf x -> f accu x +| Node (x, t1, t2) -> + tree_fold_left f (tree_fold_left f (f accu x) t1) t2 + +let rec fold_left f accu = function +| Nil -> accu +| Cons (_, t, l) -> fold_left f (tree_fold_left f accu t) l + +let rec tree_fold_right f t accu = match t with +| Leaf x -> f x accu +| Node (x, t1, t2) -> + f x (tree_fold_right f t1 (tree_fold_right f t2 accu)) + +let rec fold_right f l accu = match l with +| Nil -> accu +| Cons (_, t, l) -> tree_fold_right f t (fold_right f l accu) + +let hd = function +| Nil -> failwith "hd" +| Cons (_, Leaf x, _) -> x +| Cons (_, Node (x, _, _), _) -> x + +let tl = function +| Nil -> failwith "tl" +| Cons (_, Leaf _, l) -> l +| Cons (h, Node (_, t1, t2), l) -> + let h = h / 2 in + Cons (h, t1, Cons (h, t2, l)) + +let rec skipn n l = + if n = 0 then l + else if is_empty l then failwith "List.skipn" + else skipn (pred n) (tl l) diff --git a/clib/range.mli b/clib/range.mli new file mode 100644 index 000000000..ae7684ffa --- /dev/null +++ b/clib/range.mli @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Skewed lists + + This is a purely functional datastructure isomorphic to usual lists, except + that it features a O(log n) lookup while preserving the O(1) cons operation. + +*) + +(** {5 Constructors} *) + +type +'a t + +val empty : 'a t +val cons : 'a -> 'a t -> 'a t + +(** {5 List operations} *) + +val is_empty : 'a t -> bool +val length : 'a t -> int +val map : ('a -> 'b) -> 'a t -> 'b t +val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a +val fold_right : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b +val hd : 'a t -> 'a +val tl : 'a t -> 'a t + +val skipn : int -> 'a t -> 'a t + +(** {5 Indexing operations} *) + +val get : 'a t -> int -> 'a diff --git a/configure.ml b/configure.ml index b5de5e3e1..06a7dd822 100644 --- a/configure.ml +++ b/configure.ml @@ -276,7 +276,8 @@ module Prefs = struct let flambda_flags = ref [] let debug = ref true let profile = ref false - let annotate = ref false + let bin_annot = ref false + let annot = ref false let bytecodecompiler = ref true let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) let coqwebsite = ref "http://coq.inria.fr/" @@ -342,8 +343,12 @@ let args_options = Arg.align [ " Do not add debugging information in the Coq executables"; "-profile", Arg.Set Prefs.profile, " Add profiling information in the Coq executables"; - "-annotate", Arg.Set Prefs.annotate, - " Dumps ml annotation files while compiling Coq"; + "-annotate", Arg.Unit (fun () -> printf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead.\n"), + " Deprecated. Please use -annot or -bin-annot instead"; + "-annot", Arg.Set Prefs.annot, + " Dumps ml text annotation files while compiling Coq (e.g. for Tuareg)"; + "-bin-annot", Arg.Set Prefs.bin_annot, + " Dumps ml binary annotation files while compiling Coq (e.g. for Merlin)"; "-bytecode-compiler", arg_bool Prefs.bytecodecompiler, "(yes|no) Enable Coq's bytecode reduction machine (VM)"; "-native-compiler", arg_bool Prefs.nativecompiler, @@ -388,10 +393,8 @@ let reset_caml_find c o = c.find <- o let coq_debug_flag = if !Prefs.debug then "-g" else "" let coq_profile_flag = if !Prefs.profile then "-p" else "" -let coq_annotate_flag = - if !Prefs.annotate - then if program_in_path "ocamlmerlin" then "-bin-annot" else "-annot" - else "" +let coq_annot_flag = if !Prefs.annot then "-annot" else "" +let coq_bin_annot_flag = if !Prefs.bin_annot then "-bin-annot" else "" (* This variable can be overriden only for debug purposes, use with care. *) @@ -561,7 +564,7 @@ let coq_warn_error = (* Flags used to compile Coq and plugins (via coq_makefile) *) let caml_flags = - Printf.sprintf "-thread -rectypes %s %s %s" coq_warnings coq_annotate_flag coq_safe_string + Printf.sprintf "-thread -rectypes %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string (* Flags used to compile Coq but _not_ plugins (via coq_makefile) *) let coq_caml_flags = diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 232b8a56e..628e89291 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -4,141 +4,143 @@ # Maybe we should just use Ruby to have real objects... +# : "${foo:=bar}" sets foo to "bar" if it is unset or null + ######################################################################## # MathComp ######################################################################## -: ${mathcomp_CI_BRANCH:=master} -: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git} +: "${mathcomp_CI_BRANCH:=master}" +: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}" ######################################################################## # UniMath ######################################################################## -: ${UniMath_CI_BRANCH:=master} -: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git} +: "${UniMath_CI_BRANCH:=master}" +: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}" ######################################################################## # Unicoq + Metacoq ######################################################################## -: ${unicoq_CI_BRANCH:=master} -: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git} +: "${unicoq_CI_BRANCH:=master}" +: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}" -: ${metacoq_CI_BRANCH:=master} -: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git} +: "${metacoq_CI_BRANCH:=master}" +: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}" ######################################################################## # Mathclasses + Corn ######################################################################## -: ${math_classes_CI_BRANCH:=master} -: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git} +: "${math_classes_CI_BRANCH:=master}" +: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}" -: ${Corn_CI_BRANCH:=master} -: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git} +: "${Corn_CI_BRANCH:=master}" +: "${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}" ######################################################################## # Iris ######################################################################## -: ${stdpp_CI_BRANCH:=master} -: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git} +: "${stdpp_CI_BRANCH:=master}" +: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}" -: ${Iris_CI_BRANCH:=master} -: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git} +: "${Iris_CI_BRANCH:=master}" +: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}" -: ${lambdaRust_CI_BRANCH:=master} -: ${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git} +: "${lambdaRust_CI_BRANCH:=master}" +: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git}" ######################################################################## # HoTT ######################################################################## -: ${HoTT_CI_BRANCH:=master} -: ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} +: "${HoTT_CI_BRANCH:=master}" +: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}" ######################################################################## # Ltac2 ######################################################################## -: ${ltac2_CI_BRANCH:=master} -: ${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git} +: "${ltac2_CI_BRANCH:=master}" +: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}" ######################################################################## # GeoCoq ######################################################################## -: ${GeoCoq_CI_BRANCH:=master} -: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git} +: "${GeoCoq_CI_BRANCH:=master}" +: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git}" ######################################################################## # Flocq ######################################################################## -: ${Flocq_CI_BRANCH:=master} -: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git} +: "${Flocq_CI_BRANCH:=master}" +: "${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git}" ######################################################################## # Coquelicot ######################################################################## -: ${Coquelicot_CI_BRANCH:=master} -: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git} +: "${Coquelicot_CI_BRANCH:=master}" +: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}" ######################################################################## # CompCert ######################################################################## -: ${CompCert_CI_BRANCH:=master} -: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} +: "${CompCert_CI_BRANCH:=master}" +: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}" ######################################################################## # VST ######################################################################## -: ${VST_CI_BRANCH:=master} -: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git} +: "${VST_CI_BRANCH:=master}" +: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}" ######################################################################## # fiat_parsers ######################################################################## -: ${fiat_parsers_CI_BRANCH:=master} -: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} +: "${fiat_parsers_CI_BRANCH:=master}" +: "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}" ######################################################################## # fiat_crypto ######################################################################## -: ${fiat_crypto_CI_BRANCH:=master} -: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git} +: "${fiat_crypto_CI_BRANCH:=master}" +: "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}" ######################################################################## # formal-topology ######################################################################## -: ${formal_topology_CI_BRANCH:=ci} -: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git} +: "${formal_topology_CI_BRANCH:=ci}" +: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}" ######################################################################## # coq-dpdgraph ######################################################################## -: ${coq_dpdgraph_CI_BRANCH:=coq-trunk} -: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git} +: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}" +: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}" ######################################################################## # CoLoR ######################################################################## -: ${CoLoR_CI_BRANCH:=master} -: ${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git} +: "${CoLoR_CI_BRANCH:=master}" +: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git}" ######################################################################## # SF ######################################################################## -: ${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz} -: ${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz} -: ${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz} +: "${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}" +: "${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}" +: "${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}" ######################################################################## # TLC ######################################################################## -: ${tlc_CI_BRANCH:=master} -: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git} +: "${tlc_CI_BRANCH:=master}" +: "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}" ######################################################################## # Bignums ######################################################################## -: ${bignums_CI_BRANCH:=master} -: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} +: "${bignums_CI_BRANCH:=master}" +: "${bignums_CI_GITURL:=https://github.com/coq/bignums.git}" ######################################################################## # Equations ######################################################################## -: ${Equations_CI_BRANCH:=8.8+alpha} -: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git} +: "${Equations_CI_BRANCH:=8.8+alpha}" +: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 58c90ff11..1838db5d0 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -4,7 +4,7 @@ set -xe if [ -n "${GITLAB_CI}" ]; then - export COQBIN=`pwd`/_install_ci/bin + export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" else if [ -n "${TRAVIS}" ]; @@ -16,7 +16,7 @@ else export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" export CI_BRANCH="$CIRCLE_BRANCH" fi - export COQBIN=`pwd`/bin + export COQBIN="$PWD/bin" fi export PATH="$COQBIN:$PATH" @@ -26,14 +26,16 @@ export COQBIN="$COQBIN/" ls "$COQBIN" # Where we clone and build external developments -CI_BUILD_DIR=`pwd`/_build_ci +CI_BUILD_DIR="$PWD/_build_ci" -for overlay in ${ci_dir}/user-overlays/*.sh; do - source ${overlay} +# shellcheck source=ci-basic-overlay.sh +source "${ci_dir}/ci-basic-overlay.sh" +for overlay in "${ci_dir}"/user-overlays/*.sh; do + # shellcheck source=/dev/null + source "${overlay}" done -source ${ci_dir}/ci-basic-overlay.sh -mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp +mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" # git_checkout branch url dest will create a git repository # in <dest> (if it does not exist already) and checkout the @@ -46,15 +48,16 @@ git_checkout() # Allow an optional 4th argument for the commit local _COMMIT=${4:-FETCH_HEAD} - local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi) - - mkdir -p ${_DEST} - ( cd ${_DEST} && \ - if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \ - echo "Checking out ${_DEST}" && \ - git fetch ${_URL} ${_BRANCH} && \ - git checkout ${_COMMIT} && \ - echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) + local _DEPTH=() + if [ -z "${4}" ]; then _DEPTH=(--depth 1); fi + + mkdir -p "${_DEST}" + ( cd "${_DEST}" && \ + if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \ + echo "Checking out ${_DEST}" && \ + git fetch "${_URL}" "${_BRANCH}" && \ + git checkout "${_COMMIT}" && \ + echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) } checkout_mathcomp() @@ -79,8 +82,8 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp ${mathcomp_CI_DIR} - ( cd ${mathcomp_CI_DIR}/mathcomp && \ + checkout_mathcomp "${mathcomp_CI_DIR}" + ( cd "${mathcomp_CI_DIR}/mathcomp" && \ sed -i.bak '/ssrtest/d' Make && \ sed -i.bak '/odd_order/d' Make && \ sed -i.bak '/all\/all.v/d' Make && \ diff --git a/COMPATIBILITY b/dev/doc/COMPATIBILITY index b5fed7f01..a81afca32 100644 --- a/COMPATIBILITY +++ b/dev/doc/COMPATIBILITY @@ -1,3 +1,6 @@ +Note: this file isn't used anymore. Incompatibilities are documented +as part of CHANGES. + Potential sources of incompatibilities between Coq V8.6 and V8.7 ---------------------------------------------------------------- @@ -5,10 +8,6 @@ Potential sources of incompatibilities between Coq V8.6 and V8.7 error rather than a warning when the superfluous name is already in use. The easy fix is to remove the superfluous name. -- Proofs ending in "Qed exporting ident, .., ident" are not supported - anymore. Constants generated during `abstract` are kept private to the - local environment. - Potential sources of incompatibilities between Coq V8.5 and V8.6 ---------------------------------------------------------------- diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 26f3d0ddc..0003a2c21 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -58,30 +58,12 @@ behave as expected. A note about rlwrap ------------------- -Running "coqtop" under "rlwrap" is possible, but (on Debian) there is a catch. If you try: - - cd ~/git/coq - rlwrap bin/coqtop - -you will get an error: +When using "rlwrap coqtop" make sure the version of rlwrap is at least +0.42, otherwise you will get rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory -This is a known issue: - - https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=779692 - -It was fixed upstream in version 0.42, and in a Debian package that, at the time of writing, is not part of Debian stable/testing/sid archives but only of Debian experimental. - - https://packages.debian.org/experimental/rlwrap - -The quick solution is to grab it from there, since it installs fine on Debian stable (jessie). - - cd /tmp - wget http://ftp.us.debian.org/debian/pool/main/r/rlwrap/rlwrap_0.42-1_amd64.deb - sudo dpkg -i rlwrap_0.42-1_amd64.deb - -After that, "rlwrap" works fine with "coqtop". +If this happens either update or use an alternate readline wrapper like "ledit". How to install and configure Merlin (for Emacs) diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index 87a829746..e3ec51aeb 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -9,7 +9,7 @@ CODE=0 -if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ]; +if [ -n "${TRAVIS_PULL_REQUEST}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ]; then # skip PRs from before the linter existed if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ]; @@ -22,14 +22,13 @@ then # can still check that they don't worsen. CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*} PR_HEAD=${TRAVIS_COMMIT_RANGE##*...} - MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD) - dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1 + MERGE_BASE=$(git merge-base "$CUR_HEAD" "$PR_HEAD") + dev/lint-commits.sh "$MERGE_BASE" "$PR_HEAD" || CODE=1 fi # Check that the files with 'whitespace' gitattribute end in a newline. # xargs exit status is 123 if any file failed the test -find . "(" -path ./.git -prune ")" -type f \ --o "(" -exec dev/tools/should-check-whitespace.sh '{}' ';' ")" \ --print0 | xargs -0 -L 1 dev/tools/check-eof-newline.sh || CODE=1 +find . "(" -path ./.git -prune ")" -o -type f -print0 | + xargs -0 dev/tools/check-eof-newline.sh || CODE=1 exit $CODE diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh index 1c578c05c..9e4c8661d 100755 --- a/dev/tools/check-eof-newline.sh +++ b/dev/tools/check-eof-newline.sh @@ -1,9 +1,14 @@ #!/usr/bin/env bash -if [ -z "$(tail -c 1 "$1")" ] -then - exit 0 -else - echo "No newline at end of file $1!" - exit 1 -fi +CODE=0 +for f in "$@"; do + if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \ + git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \ + [ -n "$(tail -c 1 "$f")" ] + then + echo "No newline at end of file $f!" + CODE=1 + fi +done + +exit "$CODE" diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 0c4a79bfd..9f24960ff 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -9,18 +9,18 @@ set -e PR=$1 -CURRENT_LOCAL_BRANCH=`git rev-parse --abbrev-ref HEAD` -REMOTE=`git config --get branch.$CURRENT_LOCAL_BRANCH.remote` -git fetch $REMOTE refs/pull/$PR/head +CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) +REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") +git fetch "$REMOTE" "refs/pull/$PR/head" API=https://api.github.com/repos/coq/coq -BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'` +BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label') -COMMIT=`git rev-parse FETCH_HEAD` -STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'` +COMMIT=$(git rev-parse FETCH_HEAD) +STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state') -if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then +if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then echo "Wrong base branch" read -p "Bypass? [y/N] " -n 1 -r echo @@ -30,7 +30,7 @@ if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then fi fi; -if [ $STATUS != "success" ]; then +if [ "$STATUS" != "success" ]; then echo "CI status is \"$STATUS\"" read -p "Bypass? [y/N] " -n 1 -r echo @@ -40,10 +40,10 @@ if [ $STATUS != "success" ]; then fi fi; -git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e +git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e # TODO: improve this check -if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then +if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then echo "******************************************" echo "** WARNING: does this PR have overlays? **" echo "******************************************" diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh deleted file mode 100755 index d85d65107..000000000 --- a/dev/tools/should-check-whitespace.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/usr/bin/env bash - -# determine if a file has whitespace checking enabled in .gitattributes - -git ls-files --error-unmatch "$1" >/dev/null 2>&1 && -git check-attr whitespace -- "$1" | grep -q -v -e 'unset$' -e 'unspecified$' diff --git a/engine/eConstr.ml b/engine/eConstr.ml index a65b3941e..9ac16b5b4 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -695,6 +695,10 @@ let cast_rel_context : type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt = fun Refl x -> x +let cast_rec_decl : + type a b. (a,b) eq -> (a, a) Constr.prec_declaration -> (b, b) Constr.prec_declaration = + fun Refl x -> x + let cast_named_decl : type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt = fun Refl x -> x @@ -817,6 +821,7 @@ let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e +let push_rec_types d e = push_rec_types (cast_rec_decl unsafe_eq d) e let push_named d e = push_named (cast_named_decl unsafe_eq d) e let push_named_context d e = push_named_context (cast_named_context unsafe_eq d) e let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq d) e diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 30de748a1..6fa338c73 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -251,6 +251,7 @@ end val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env +val push_rec_types : (t, t) Constr.prec_declaration -> env -> env val push_named : named_declaration -> env -> env val push_named_context : named_context -> env -> env diff --git a/ide/coqide.ml b/ide/coqide.ml index 842d06859..3cc46b6aa 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1221,9 +1221,14 @@ let build_ui () = (* Emacs/PG mode *) NanoPG.init w notebook all_menus; - (* Reset on tab switch *) - let _ = notebook#connect#switch_page ~callback:(fun _ -> - if reset_on_tab_switch#get then Nav.restart ()) + (* On tab switch, reset, update location *) + let _ = notebook#connect#switch_page ~callback:(fun n -> + let _ = if reset_on_tab_switch#get then Nav.restart () in + try + let session = notebook#get_nth_term n in + let ins = session.buffer#get_iter_at_mark `INSERT in + Ideutils.display_location ins + with _ -> ()) in (* Vertical Separator between Scripts and Goals *) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 0977a1890..9c5b06a0d 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -69,6 +69,12 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let set_location = ref (function s -> failwith "not ready") +let display_location ins = + let line = ins#line + 1 in + let off = ins#line_offset + 1 in + let msg = Printf.sprintf "Line: %5d Char: %3d" line off in + !set_location msg + (** A utf8 char is either a single byte (ascii char, 0xxxxxxx) or multi-byte (with a leading byte 11xxxxxx and extra bytes 10xxxxxx) *) @@ -465,4 +471,3 @@ let browse_keyword prerr text = let u = Lazy.force url_for_keyword text in browse prerr (doc_url() ^ u) with Not_found -> prerr ("No documentation found for \""^text^"\".\n") - diff --git a/ide/ideutils.mli b/ide/ideutils.mli index f06a48aeb..99ff763e2 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -56,6 +56,7 @@ val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list -> #GText.buffer_skel -> Richpp.richpp -> unit val set_location : (string -> unit) ref +val display_location : GText.iter -> unit (* In win32, when a command-line is to be executed via cmd.exe (i.e. Sys.command, Unix.open_process, ...), it cannot contain several @@ -95,4 +96,3 @@ val io_read_all : Glib.Io.channel -> string val run_command : (string -> unit) -> (Unix.process_status -> unit) -> string -> unit - diff --git a/ide/session.ml b/ide/session.ml index 0a09cc9f5..8dada8ff2 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -209,10 +209,7 @@ let set_buffer_handlers let mark_set_cb it m = debug_edit_zone (); let ins = get_insert () in - let line = ins#line + 1 in - let off = ins#line_offset + 1 in - let msg = Printf.sprintf "Line: %5d Char: %3d" line off in - let () = !Ideutils.set_location msg in + let () = Ideutils.display_location ins in match GtkText.Mark.get_name m with | Some "insert" -> () | Some s -> Minilib.log (s^" moved") diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index a62ff2de5..cb182465a 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -84,8 +84,10 @@ class finder name (view : GText.view) = method private backward_search starti = let text = view#buffer#start_iter#get_text ~stop:starti in let regexp = self#regex in - try - let i = Str.search_backward regexp text (String.length text - 1) in + let offs = (String.length text - 1) in + if offs < 0 then None + else try + let i = Str.search_backward regexp text offs in let j = Str.match_end () in Some(view#buffer#start_iter#forward_chars (b2c text i), view#buffer#start_iter#forward_chars (b2c text j)) @@ -101,24 +103,33 @@ class finder name (view : GText.view) = with Not_found -> None method replace_all () = - let rec replace_at (iter : GText.iter) = + let rec replace_at (iter : GText.iter) ct tot = let found = self#forward_search iter in match found with - | None -> () + | None -> + let tot_str = if Int.equal ct tot then "" else " of " ^ string_of_int tot in + let occ_str = CString.plural tot "occurrence" in + let _ = Ideutils.flash_info ("Replaced " ^ string_of_int ct ^ tot_str ^ " " ^ occ_str) in + () | Some (start, stop) -> let text = iter#get_text ~stop:view#buffer#end_iter in let start_mark = view#buffer#create_mark start in let stop_mark = view#buffer#create_mark ~left_gravity:false stop in + let mod_save = view#buffer#modified in + let _ = view#buffer#set_modified false in let _ = view#buffer#delete_interactive ~start ~stop () in let iter = view#buffer#get_iter_at_mark (`MARK start_mark) in - let _ = view#buffer#insert_interactive ~iter (self#replacement text)in + let _ = view#buffer#insert_interactive ~iter (self#replacement text) in + let edited = view#buffer#modified in + let _ = view#buffer#set_modified (edited || mod_save) in let next = view#buffer#get_iter_at_mark (`MARK stop_mark) in let () = view#buffer#delete_mark (`MARK start_mark) in let () = view#buffer#delete_mark (`MARK stop_mark) in - replace_at next + let next_ct = if edited then ct + 1 else ct in + replace_at next next_ct (tot + 1) in let () = view#buffer#begin_user_action () in - let () = replace_at view#buffer#start_iter in + let () = replace_at view#buffer#start_iter 0 0 in view#buffer#end_user_action () method private set_not_found () = @@ -130,22 +141,52 @@ class finder name (view : GText.view) = method private set_normal () = find_entry#misc#modify_base [`NORMAL, `NAME "white"] - method private find_from backward (starti : GText.iter) = + method private find_from backward ?(wrapped=false) (starti : GText.iter) = let found = if backward then self#backward_search starti else self#forward_search starti in match found with | None -> if not backward && not (starti#equal view#buffer#start_iter) then - self#find_from backward view#buffer#start_iter + self#find_from backward ~wrapped:true view#buffer#start_iter else if backward && not (starti#equal view#buffer#end_iter) then - self#find_from backward view#buffer#end_iter + self#find_from backward ~wrapped:true view#buffer#end_iter else + let _ = Ideutils.flash_info "String not found" in self#set_not_found () | Some (start, stop) -> + let text = view#buffer#start_iter#get_text ~stop:view#buffer#end_iter in + let rec find_all offs accum = + if offs > String.length text then + List.rev accum + else try + let i = Str.search_forward self#regex text offs in + let j = Str.match_end () in + find_all (j + 1) (i :: accum) + with Not_found -> List.rev accum + in + let occurs = find_all 0 [] in + let num_occurs = List.length occurs in + (* assoc table of offset, occurrence index pairs *) + let occur_tbl = List.mapi (fun ndx occ -> (occ,ndx+1)) occurs in let _ = view#buffer#select_range start stop in let scroll = `MARK (view#buffer#create_mark stop) in let _ = view#scroll_to_mark ~use_align:false scroll in + let _ = + try + let occ_ndx = List.assoc start#offset occur_tbl in + let occ_str = CString.plural num_occurs "occurrence" in + let wrap_str = if wrapped then + if backward then " (wrapped backwards)" + else " (wrapped)" + else "" + in + Ideutils.flash_info + (string_of_int occ_ndx ^ " of " ^ string_of_int num_occurs ^ + " " ^ occ_str ^ wrap_str) + with Not_found -> + CErrors.anomaly (Pp.str "Occurrence of Find string not in table") + in self#set_found () method find_forward () = diff --git a/install.sh b/install.sh index f8589a3c7..4f60080a1 100755 --- a/install.sh +++ b/install.sh @@ -4,13 +4,13 @@ dest="$1" shift for f; do - bn=`basename $f` - dn=`dirname $f` + bn=$(basename "$f") + dn=$(dirname "$f") install -d "$dest/$dn" case $bn in - *.cmxs|*.py) install -m 755 $f "$dest/$dn/$bn" + *.cmxs|*.py) install -m 755 "$f" "$dest/$dn/$bn" ;; - *) install -m 644 $f "$dest/$dn/$bn" + *) install -m 644 "$f" "$dest/$dn/$bn" ;; esac done diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 11616da7b..b1181157e 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -258,7 +258,7 @@ type 'a infos_cache = { i_repr : 'a infos -> constr -> 'a; i_env : env; i_sigma : existential -> constr option; - i_rels : constr option array; + i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t; i_tab : 'a KeyTable.t } and 'a infos = { @@ -282,13 +282,16 @@ let ref_value_cache ({i_cache = cache} as infos) ref = let body = match ref with | RelKey n -> - let len = Array.length cache.i_rels in - let i = n - 1 in - let () = if i < 0 || len <= i then raise Not_found in - begin match Array.unsafe_get cache.i_rels i with - | None -> raise Not_found - | Some t -> lift n t - end + let open Context.Rel.Declaration in + let i = n - 1 in + let (d, _) = + try Range.get cache.i_rels i + with Invalid_argument _ -> raise Not_found + in + begin match d with + | LocalAssum _ -> raise Not_found + | LocalDef (_, t, _) -> lift n t + end | VarKey id -> assoc_defined id cache.i_env | ConstKey cst -> constant_value_in cache.i_env cst in @@ -303,26 +306,13 @@ let ref_value_cache ({i_cache = cache} as infos) ref = let evar_value cache ev = cache.i_sigma ev -let defined_rels flags env = -(* if red_local_const (snd flags) then*) - let ctx = rel_context env in - let len = List.length ctx in - let ans = Array.make len None in - let open Context.Rel.Declaration in - let iter i = function - | LocalAssum _ -> () - | LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b) - in - let () = List.iteri iter ctx in - ans -(* else (0,[])*) - let create mk_cl flgs env evars = + let open Pre_env in let cache = { i_repr = mk_cl; i_env = env; i_sigma = evars; - i_rels = defined_rels flgs env; + i_rels = (Environ.pre_env env).env_rel_context.env_rel_map; i_tab = KeyTable.create 17 } in { i_flags = flgs; i_cache = cache } diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 2ffe36fcf..712c66f11 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -198,7 +198,7 @@ and slot_for_fv env fv = let rv = Pre_env.lookup_rel_val i env in begin match force_lazy_val rv with | None -> - env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVuniv_var idu -> diff --git a/kernel/environ.ml b/kernel/environ.ml index 3c86129fe..93dc2f9a7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -60,18 +60,17 @@ let deactivated_guard env = not (typing_flags env).check_guarded let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context.env_named_ctx let named_context_val env = env.env_named_context -let rel_context env = env.env_rel_context +let rel_context env = env.env_rel_context.env_rel_ctx let opaque_tables env = env.indirect_pterms let set_opaque_tables env indirect_pterms = { env with indirect_pterms } let empty_context env = - match env.env_rel_context, env.env_named_context.env_named_ctx with + match env.env_rel_context.env_rel_ctx, env.env_named_context.env_named_ctx with | [], [] -> true | _ -> false (* Rel context *) -let lookup_rel n env = - Context.Rel.lookup n env.env_rel_context +let lookup_rel = lookup_rel let evaluable_rel n env = is_local_def (lookup_rel n env) @@ -88,13 +87,12 @@ let push_rec_types (lna,typarray,_) env = let fold_rel_context f env ~init = let rec fold_right env = - match env.env_rel_context with - | [] -> init - | rd::rc -> + match match_rel_context_val env.env_rel_context with + | None -> init + | Some (rd, _, rc) -> let env = { env with env_rel_context = rc; - env_rel_val = List.tl env.env_rel_val; env_nb_rel = env.env_nb_rel - 1 } in f env rd (fold_right env) in fold_right env @@ -144,16 +142,21 @@ let evaluable_named id env = let reset_with_named_context ctxt env = { env with env_named_context = ctxt; - env_rel_context = Context.Rel.empty; - env_rel_val = []; + env_rel_context = empty_rel_context_val; env_nb_rel = 0 } let reset_context = reset_with_named_context empty_named_context_val let pop_rel_context n env = + let rec skip n ctx = + if Int.equal n 0 then ctx + else match match_rel_context_val ctx with + | None -> invalid_arg "List.skipn" + | Some (_, _, ctx) -> skip (pred n) ctx + in let ctxt = env.env_rel_context in { env with - env_rel_context = List.skipn n ctxt; + env_rel_context = skip n ctxt; env_nb_rel = env.env_nb_rel - n } let fold_named_context f env ~init = diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c558e9ed0..ffe19510a 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1830,7 +1830,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = in let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in let auxdefs = List.fold_right get_named_val fv_named auxdefs in - let lvl = Context.Rel.length env.env_rel_context in + let lvl = Context.Rel.length env.env_rel_context.env_rel_ctx in let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in let aux_name = fresh_lname Anonymous in @@ -1838,8 +1838,8 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel.Declaration in - let decl = Context.Rel.lookup n env.env_rel_context in - let n = Context.Rel.length env.env_rel_context - n in + let decl = Pre_env.lookup_rel n env in + let n = List.length env.env_rel_context.env_rel_ctx - n in match decl with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 160a90dc2..b333b0fb9 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -639,7 +639,7 @@ let optimize lam = let lambda_of_constr env sigma c = set_global_env env; let env = Renv.make () in - let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context in + let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context.env_rel_ctx in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env sigma c in (* if Flags.vm_draw_opt () then begin diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 4ef89f8c0..3ef15105a 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -67,11 +67,15 @@ type named_context_val = { env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; } +type rel_context_val = { + env_rel_ctx : Context.Rel.t; + env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; +} + type env = { env_globals : globals; (* globals = constants + inductive types + modules + module-types *) env_named_context : named_context_val; (* section variables *) - env_rel_context : Context.Rel.t; - env_rel_val : lazy_val list; + env_rel_context : rel_context_val; env_nb_rel : int; env_stratification : stratification; env_typing_flags : typing_flags; @@ -84,6 +88,11 @@ let empty_named_context_val = { env_named_map = Id.Map.empty; } +let empty_rel_context_val = { + env_rel_ctx = []; + env_rel_map = Range.empty; +} + let empty_env = { env_globals = { env_constants = Cmap_env.empty; @@ -91,8 +100,7 @@ let empty_env = { env_modules = MPmap.empty; env_modtypes = MPmap.empty}; env_named_context = empty_named_context_val; - env_rel_context = Context.Rel.empty; - env_rel_val = []; + env_rel_context = empty_rel_context_val; env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; @@ -106,21 +114,39 @@ let empty_env = { let nb_rel env = env.env_nb_rel +let push_rel_context_val d ctx = { + env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx; + env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map; +} + +let match_rel_context_val ctx = match ctx.env_rel_ctx with +| [] -> None +| decl :: rem -> + let (_, lval) = Range.hd ctx.env_rel_map in + let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in + Some (decl, lval, ctx) + let push_rel d env = - let rval = ref VKnone in { env with - env_rel_context = Context.Rel.add d env.env_rel_context; - env_rel_val = rval :: env.env_rel_val; + env_rel_context = push_rel_context_val d env.env_rel_context; env_nb_rel = env.env_nb_rel + 1 } +let lookup_rel n env = + try fst (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + let lookup_rel_val n env = - try List.nth env.env_rel_val (n - 1) - with Failure _ -> raise Not_found + try snd (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let rel_skipn n ctx = { + env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx; + env_rel_map = Range.skipn n ctx.env_rel_map; +} let env_of_rel n env = { env with - env_rel_context = Util.List.skipn n env.env_rel_context; - env_rel_val = Util.List.skipn n env.env_rel_val; + env_rel_context = rel_skipn n env.env_rel_context; env_nb_rel = env.env_nb_rel - n } diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index fef530c87..335ca1057 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -45,11 +45,15 @@ type named_context_val = private { env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; } +type rel_context_val = private { + env_rel_ctx : Context.Rel.t; + env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; +} + type env = { env_globals : globals; env_named_context : named_context_val; - env_rel_context : Context.Rel.t; - env_rel_val : lazy_val list; + env_rel_context : rel_context_val; env_nb_rel : int; env_stratification : stratification; env_typing_flags : typing_flags; @@ -63,8 +67,15 @@ val empty_env : env (** Rel context *) +val empty_rel_context_val : rel_context_val +val push_rel_context_val : + Context.Rel.Declaration.t -> rel_context_val -> rel_context_val +val match_rel_context_val : + rel_context_val -> (Context.Rel.Declaration.t * lazy_val * rel_context_val) option + val nb_rel : env -> int val push_rel : Context.Rel.Declaration.t -> env -> env +val lookup_rel : int -> env -> Context.Rel.Declaration.t val lookup_rel_val : int -> env -> lazy_val val env_of_rel : int -> env -> env diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ec7c3077f..c3a221944 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -462,19 +462,21 @@ let sub_match ?(closed=true) env sigma pat c = in let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next - | Fix (indx,(names,types,bodies)) -> + | Fix (indx,(names,types,bodies as recdefs)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let sub = subargs env types @ subargs env bodies in + let env' = push_rec_types recdefs env in + let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next - | CoFix (i,(names,types,bodies)) -> + | CoFix (i,(names,types,bodies as recdefs)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let sub = subargs env types @ subargs env bodies in + let env' = push_rec_types recdefs env in + let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next | Proj (p,c') -> begin try diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 788e4d268..41c4616f7 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -276,11 +276,6 @@ let rec ise_app_stack2 env f evd sk1 sk2 = end | _, _ -> (sk1,sk2), Success evd -let push_rec_types pfix env = - let (i, c, t) = pfix in - let inj c = EConstr.Unsafe.to_constr c in - push_rec_types (i, Array.map inj c, Array.map inj t) env - (* This function tries to unify 2 stacks element by element. It works from the end to the beginning. If it unifies a non empty suffix of stacks but not the entire stacks, the first part of the answer is diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 43066c809..3132d2ad5 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -23,11 +23,6 @@ open Arguments_renaming open Pretype_errors open Context.Rel.Declaration -let push_rec_types pfix env = - let (i, c, t) = pfix in - let inj c = EConstr.Unsafe.to_constr c in - push_rec_types (i, Array.map inj c, Array.map inj t) env - let meta_type evd mv = let ty = try Evd.meta_ftype evd mv diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 11ac16680..2bb9be66b 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -88,6 +88,12 @@ let is_lax_conjunction = function let prod_assum sigma t = fst (decompose_prod_assum sigma t) +(* whd_beta normalize the types of arguments in a product *) +let rec whd_beta_prod sigma c = match EConstr.kind sigma c with + | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta sigma t,whd_beta_prod sigma c) + | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c) + | _ -> c + let match_with_one_constructor sigma style onlybinary allow_rec t = let (hdapp,args) = decompose_app sigma t in let res = match EConstr.kind sigma hdapp with @@ -111,8 +117,9 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = Some (hdapp,args) else None else - let ctyp = Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) - (EConstr.of_constr mip.mind_nf_lc.(0)) args in + let ctyp = whd_beta_prod sigma + (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) + (EConstr.of_constr mip.mind_nf_lc.(0)) args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) diff --git a/test-suite/bugs/closed/6617.v b/test-suite/bugs/closed/6617.v new file mode 100644 index 000000000..9cabd62d4 --- /dev/null +++ b/test-suite/bugs/closed/6617.v @@ -0,0 +1,34 @@ +Definition MR {T M : Type} := +fun (R : M -> M -> Prop) (m : T -> M) (x y : T) => R (m x) (m y). + +Set Primitive Projections. + +Record sigma {A : Type} {B : A -> Type} : Type := sigmaI + { pr1 : A; pr2 : B pr1 }. + +Axiom F : forall {A : Type} {R : A -> A -> Prop}, + (forall x, (forall y, R y x -> unit) -> unit) -> forall (x : A), unit. + +Definition foo (A : Type) (l : list A) := + let y := {| pr1 := A; pr2 := l |} in + let bar := MR lt (fun p : sigma => + (fix Ffix (x : list (pr1 p)) : nat := + match x with + | nil => 0 + | cons _ x1 => S (Ffix x1) + end) (pr2 p)) in +fun (_ : bar y y) => +F (fun (r : sigma) + (X : forall q : sigma, bar q r -> unit) => tt). + +Definition fooT (A : Type) (l : list A) : Type := + ltac:(let ty := type of (foo A l) in exact ty). +Parameter P : forall A l, fooT A l -> Prop. + +Goal forall A l, P A l (foo A l). +Proof. + intros; unfold foo. + Fail match goal with + | [ |- context [False]] => idtac + end. +Admitted. diff --git a/test-suite/bugs/opened/6393.v b/test-suite/bugs/opened/6393.v new file mode 100644 index 000000000..8d5d09233 --- /dev/null +++ b/test-suite/bugs/opened/6393.v @@ -0,0 +1,11 @@ +(* These always worked. *) +Goal prod True True. firstorder. Qed. +Goal True -> @sigT True (fun _ => True). firstorder. Qed. +Goal prod True True. dtauto. Qed. +Goal prod True True. tauto. Qed. + +(* These should work. *) +Goal @sigT True (fun _ => True). dtauto. Qed. +(* These should work, but don't *) +(* Goal @sigT True (fun _ => True). firstorder. Qed. *) +(* Goal @sigT True (fun _ => True). tauto. Qed. *) |