diff options
61 files changed, 533 insertions, 215 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3b95800f0d..32b05ec746 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -19,7 +19,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-05-24-V1" + CACHEKEY: "bionic_coq-V2020-07-21-V38" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -481,6 +481,8 @@ doc:refman-pdf:dune: - _build/log - _build/default/doc/refman-pdf +# currently bugged: dune cleans up the glob files so no links +# see #12699 doc:stdlib:dune: extends: .dune-ci-template variables: @@ -501,11 +503,11 @@ doc:refman:deploy: dependencies: - doc:ml-api:odoc - doc:refman:dune - - doc:stdlib:dune + - build:base needs: - doc:ml-api:odoc - doc:refman:dune - - doc:stdlib:dune + - build:base script: - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null - git clone git@github.com:coq/doc.git _deploy @@ -515,7 +517,7 @@ doc:refman:deploy: - mkdir -p _deploy/$CI_COMMIT_REF_NAME - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api - cp -rv _build/default/doc/refman-html _deploy/$CI_COMMIT_REF_NAME/refman - - cp -rv _build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib + - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib - cd _deploy/$CI_COMMIT_REF_NAME/ - git add api refman stdlib - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA" @@ -724,6 +726,9 @@ library:ci-coqprime: - build:edge+flambda - plugin:ci-bignums +library:ci-coqtail: + extends: .ci-template + library:ci-coquelicot: extends: .ci-template diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8a09e43c94..d561ec8a12 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -184,7 +184,7 @@ stream][Zulip-dev] of our Zulip chat. Finally, we strongly encourage authors of plugins to submit their plugins to join Coq's continuous integration (CI) early on. Indeed, -the Coq API gets continously reworked, so this is the best way of +the Coq API gets continuously reworked, so this is the best way of ensuring your plugin stays compatible with new Coq versions, as this means Coq developers will fix your plugin for you. Learn more about this in the [CI README (user part)][CI-README-users]. diff --git a/Makefile.ci b/Makefile.ci index 77d8bda671..85e4b965f9 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -17,6 +17,7 @@ CI_TARGETS= \ ci-color \ ci-compcert \ ci-coq_dpdgraph \ + ci-coqtail \ ci-coquelicot \ ci-corn \ ci-cross_crypto \ diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 305c6a627e..b27d1df39d 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -64,7 +64,8 @@ jobs: set -e brew update (cd $(brew --repository)/Library/Taps/homebrew/homebrew-core/ && git fetch --shallow-since=${HBCORE_DATE} && git checkout ${HBCORE_REF}) - brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme + brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme || true + # || true: workaround #12657, see also #12672 and commit message for this line pip3 install macpack displayName: 'Install system dependencies' env: diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4973cbb478..2725e6b56c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -380,3 +380,10 @@ : "${sf_CI_REF:=master}" : "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}" : "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}" + +######################################################################## +# Coqtail +######################################################################## +: "${coqtail_CI_REF:=master}" +: "${coqtail_CI_GITURL:=https://github.com/whonore/Coqtail}" +: "${coqtail_CI_ARCHIVEURL:=${coqtail_CI_GITURL}/archive}" diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 59a85e4726..9cb7a65ab5 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -6,4 +6,6 @@ ci_dir="$(dirname "$0")" git_download compcert ( cd "${CI_BUILD_DIR}/compcert" && \ - ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) + ./configure -ignore-coq-version x86_32-linux && \ + make && \ + make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)') diff --git a/dev/ci/ci-coqtail.sh b/dev/ci/ci-coqtail.sh new file mode 100755 index 0000000000..b8b5c6c724 --- /dev/null +++ b/dev/ci/ci-coqtail.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coqtail + +( cd "${CI_BUILD_DIR}/coqtail" && PYTHONPATH=python python3 -m pytest tests/test_coqtop.py ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 169d1a41db..4a332406a2 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -5,4 +5,6 @@ ci_dir="$(dirname "$0")" git_download vst +export COMPCERT=bundled + ( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8c5696f4f9..7570b17095 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-05-24-V1" +# CACHEKEY: "bionic_coq-V2020-07-21-V38" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -17,9 +17,10 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of source-doc and coq-makefile texlive-science tipa -# More dependencies of the sphinx doc +# More dependencies of the sphinx doc, pytest for coqtail RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ - antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \ + pytest==5.4.3 # We need to install OPAM 2.0 manually for now. RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index aa650fbdc8..ac4972ed0d 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -1,6 +1,5 @@ open Format open Term -open Constr open Names open Cemitcodes open Vmvalues @@ -8,9 +7,7 @@ open Vmvalues let ppripos (ri,pos) = (match ri with | Reloc_annot a -> - let sp,i = a.ci.ci_ind in - print_string - ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") + print_string "switch\n" | Reloc_const _ -> print_string "structured constant\n" | Reloc_getglobal kn -> diff --git a/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst b/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst new file mode 100644 index 0000000000..ab8768a079 --- /dev/null +++ b/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Printing bug with notations for n-ary applications used with applied references. + (`#12683 <https://github.com/coq/coq/pull/12683>`_, + fixes `#12682 <https://github.com/coq/coq/pull/12682>`_, + by Hugo Herbelin). diff --git a/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst b/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst new file mode 100644 index 0000000000..4df8e97e34 --- /dev/null +++ b/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Do not store the full environment inside ssr ast_closure_term + (`#12708 <https://github.com/coq/coq/pull/12708>`_, + fixes `#12707 <https://github.com/coq/coq/issues/12707>`_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index e5c2056c40..d4707a04d8 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -14,9 +14,9 @@ Version 8.12 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.12 integrates many quality-of-life improvements, +|Coq| version 8.12 integrates many usability improvements, in particular with respect to notations, scopes and implicit arguments, -along with many bug-fixes and major improvements to the reference manual. +along with many bug fixes and major improvements to the reference manual. The main changes include: - New :ref:`binder notation<812Implicit>` for non-maximal implicit arguments using :g:`[ ]` @@ -64,6 +64,23 @@ Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. +Previously, most components of Coq had a single principal maintainer. +This was changed in 8.12 (`#11295 +<https://github.com/coq/coq/pull/11295>`_) so that every component now has +a team of maintainers, who are in charge of reviewing and +merging incoming pull requests. This gave us a chance to +significantly expand the pool of maintainters and provide faster +feedback to contributors. Special thanks to all our maintainers! + +Our current 31 maintainers are Yves Bertot, Frédéric Besson, Tej +Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, +Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, +Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, +Vincent Laporte, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond, +Pierre-Marie Pédrot, Clément Pit-Claudel, Kazuhiko Sakaguchi, Vincent +Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico +Tassi, Laurent Théry, Anton Trunov, Li-yao Xia, Théo Zimmermann + The 59 contributors to this version are Abhishek Anand, Yves Bertot, Frédéric Besson, Lasse Blaauwbroek, Simon Boulier, Quentin Carbonneaux, Tej Chajed, Arthur Charguéraud, Cyril Cohen, Pierre Courtieu, Matthew Dempsky, Maxime Dénès, @@ -72,8 +89,8 @@ Jesús Gallego Arias, Paolo G. Giarrusso, Gaëtan Gilbert, Jason Gross, Samuel Gruetter, Attila Gáspár, Hugo Herbelin, Jan-Oliver Kaiser, Robbert Krebbers, Vincent Laporte, Olivier Laurent, Xavier Leroy, Thomas Letan, Yishuai Li, Kenji Maillard, Erik Martin-Dorel, Guillaume Melquiond, Ike Mulder, -Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Clément -Pit-Claudel, Pierre-Marie Pédrot, Ramkumar Ramachandra, Lars Rasmusson, Daniel +Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Pierre-Marie +Pédrot, Clément Pit-Claudel, Ramkumar Ramachandra, Lars Rasmusson, Daniel de Rauglaudre, Talia Ringer, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, @scinart, Kartik Singhal, Michael Soegtrop, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Ralf Treinen, Anton Trunov, Bernhard M. Wiedemann, Li-yao Xia, diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index fcd5ecc070..18149a690a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1786,13 +1786,13 @@ Tactic notations allow customizing the syntax of tactics. * - ``reference`` - :token:`qualid` - - a global reference of term - - :tacn:`unfold` + - a qualified identifier + - name of an |Ltac|-defined tactic * - ``smart_global`` - :token:`reference` - a global reference of term - - :tacn:`with_strategy` + - :tacn:`unfold`, :tacn:`with_strategy` * - ``constr`` - :token:`term` diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index d6951fff6d..83c158e057 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -1548,12 +1548,21 @@ module Parsable = struct Stream.Failure -> let loc = get_loc () in restore (); - Ploc.raise loc (Stream.Error ("illegal begin of " ^ entry.ename)) + Loc.raise ~loc (Stream.Error ("illegal begin of " ^ entry.ename)) | Stream.Error _ as exc -> - let loc = get_loc () in restore (); Ploc.raise loc exc + let loc = get_loc () in restore (); + Loc.raise ~loc exc | exc -> + let exc,info = Exninfo.capture exc in let loc = Stream.count cs, Stream.count cs + 1 in - restore (); Ploc.raise (Ploc.make_unlined loc) exc + restore (); + (* If the original exn had a loc, keep it *) + let info = + match Loc.get_loc info with + | Some _ -> info + | None -> Loc.add_loc info (Ploc.make_unlined loc) + in + Exninfo.iraise (exc,info) let parse_parsable e p = L.State.set !(p.lexer_state); @@ -1561,11 +1570,10 @@ module Parsable = struct let c = parse_parsable e p in p.lexer_state := L.State.get (); c - with Ploc.Exc (loc,e) -> + with exn -> + let exn,info = Exninfo.capture exn in L.State.drop (); - let loc' = Loc.get_loc (Exninfo.info e) in - let loc = match loc' with None -> loc | Some loc -> loc in - Loc.raise ~loc e + Exninfo.iraise (exn,info) let make ?loc cs = let lexer_state = ref (L.State.init ()) in diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml index 056a2b7ad3..e121342c94 100644 --- a/gramlib/ploc.ml +++ b/gramlib/ploc.ml @@ -16,10 +16,3 @@ let dummy = let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len} let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len} - -exception Exc of Loc.t * exn - -let raise loc exc = - match exc with - Exc (_, _) -> raise exc - | _ -> raise (Exc (loc, exc)) diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli index 15a5a74455..4b865110c3 100644 --- a/gramlib/ploc.mli +++ b/gramlib/ploc.mli @@ -2,20 +2,6 @@ (* ploc.mli,v *) (* Copyright (c) INRIA 2007-2017 *) -(* located exceptions *) - -exception Exc of Loc.t * exn - (** [Ploc.Exc loc e] is an encapsulation of the exception [e] with - the input location [loc]. To be used to specify a location - for an error. This exception must not be raised by [raise] but - rather by [Ploc.raise] (see below), to prevent the risk of several - encapsulations of [Ploc.Exc]. *) - -val raise : Loc.t -> exn -> 'a - (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc], - re-raise it (ignoring the new location [loc]), else raise the - exception [Ploc.Exc loc e]. *) - val make_unlined : int * int -> Loc.t (** [Ploc.make_unlined] is like [Ploc.make] except that the line number is not provided (to be used e.g. when the line number is unknown. *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 95df626d4c..3667757a2f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -858,10 +858,17 @@ let extern_possible_prim_token (custom,scopes) r = insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) let filter_enough_applied nargs l = + (* This is to ensure that notations for coercions are used only when + the coercion is fully applied; not explicitly done yet, but we + could also expect that the notation is exactly talking about the + coercion *) match nargs with | None -> l | Some nargs -> - List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l + List.filter (fun (keyrule,pat,n as _rule) -> + match n with + | AppBoundedNotation n -> n > nargs + | AppUnboundedNotation | NotAppNotation -> false) l (* Helper function for safe and optimal printing of primitive tokens *) (* such as those for Int63 *) @@ -1247,7 +1254,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = [], [] in (* Adjust to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match n with - | Some n when nallargs >= n -> + | AppBoundedNotation n when nallargs >= n -> let args1, args2 = List.chop n args in let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in let args2impls = @@ -1257,12 +1264,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules = [] else try List.skipn n argsimpls with Failure _ -> [] in DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls - | None -> + | AppUnboundedNotation -> t, [], [], [] + | NotAppNotation -> begin match DAst.get f with | GRef (ref,us) -> f, args, argsscopes, argsimpls | _ -> t, [], [], [] end - | _ -> raise No_match in + | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = match_notation_constr !print_universes t pat in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 987aa63392..6d4ab8b4d6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1659,12 +1659,12 @@ let drop_notations_pattern looked_for genv = | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> let pl = - if get_asymmetric_patterns () then pl else let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in - List.rev_append pars pl in + List.rev_append pars pl + in let (_,argscs) = find_remaining_scopes [] pl head in let pats = List.map2 (in_pat_sc scopes) argscs pl in - DAst.make ?loc @@ RCPatCstr(head, [], pats) + DAst.make ?loc @@ RCPatCstr(head, pats, []) end | CPatCstr (head, None, pl) -> begin diff --git a/interp/notation.ml b/interp/notation.ml index e282d62396..c4e9496b95 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -293,7 +293,12 @@ let key_compare k1 k2 = match k1, k2 with module KeyOrd = struct type t = key let compare = key_compare end module KeyMap = Map.Make(KeyOrd) -type notation_rule = interp_rule * interpretation * int option +type notation_applicative_status = + | AppBoundedNotation of int + | AppUnboundedNotation + | NotAppNotation + +type notation_rule = interp_rule * interpretation * notation_applicative_status let keymap_add key interp map = let old = try KeyMap.find key map with Not_found -> [] in @@ -329,13 +334,14 @@ let cases_pattern_key c = match DAst.get c with | _ -> Oth let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) - | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) + | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args) | NList (_,_,NApp (NRef ref,args),_,_) | NBinderList (_,_,NApp (NRef ref,args),_,_) -> - RefKey (canonical_gr ref), Some (List.length args) - | NRef ref -> RefKey(canonical_gr ref), None - | NApp (_,args) -> Oth, Some (List.length args) - | _ -> Oth, None + RefKey (canonical_gr ref), AppBoundedNotation (List.length args) + | NRef ref -> RefKey(canonical_gr ref), NotAppNotation + | NApp (_,args) -> Oth, AppBoundedNotation (List.length args) + | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation + | _ -> Oth, NotAppNotation (** Dealing with precedences *) diff --git a/interp/notation.mli b/interp/notation.mli index c39bfa6e28..05ddd25a62 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -239,7 +239,12 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) -type notation_rule = interp_rule * interpretation * int option +type notation_applicative_status = + | AppBoundedNotation of int + | AppUnboundedNotation + | NotAppNotation + +type notation_rule = interp_rule * interpretation * notation_applicative_status (** Return the possible notations for a given term *) val uninterp_notations : 'a glob_constr_g -> notation_rule list diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 9921208e04..15cc451ea8 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1187,7 +1187,7 @@ value coq_interprete if (sz == 0) accu = Atom(0); else { Alloc_small(accu, sz, Default_tag); - if (Field(*sp, 2) == Val_true) { + if (Is_tailrec_switch(*sp)) { for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2]; }else{ for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5]; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 86ae6295fd..a19f9b56c1 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -32,6 +32,7 @@ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #define Is_double(v) (Tag_val(v) == Double_tag) +#define Is_tailrec_switch(v) (Field(v,1) == Val_true) /* coq array */ #define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1)) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 5e5fad9f04..41b3bff465 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -128,6 +128,7 @@ val prim_ind_to_string : 'a prim_ind -> string (** Can raise [Not_found] *) val op_or_type_of_string : string -> op_or_type + val op_or_type_to_string : op_or_type -> string val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 7bff377238..bacc308e1f 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -761,7 +761,7 @@ let rec compile_lam env cenv lam sz cont = done; let annot = - {ci = ci; rtbl = rtbl; tailcall = is_tailcall; + {rtbl = rtbl; tailcall = is_tailcall; max_stack_size = !max_stack_size - sz} in diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 6b4daabf0c..ed475dca7e 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -13,7 +13,6 @@ (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) open Names -open Constr open Vmvalues open Cbytecodes open Copcodes @@ -424,12 +423,11 @@ let subst_strcst s sc = | Const_float _ -> sc | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) +let subst_annot _ (a : annot_switch) = a + let subst_reloc s ri = match ri with - | Reloc_annot a -> - let (kn,i) = a.ci.ci_ind in - let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in - Reloc_annot {a with ci = ci} + | Reloc_annot a -> Reloc_annot (subst_annot s a) | Reloc_const sc -> Reloc_const (subst_strcst s sc) | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p) diff --git a/kernel/primred.ml b/kernel/primred.ml index 10a8da8813..90eeeb9be7 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -5,62 +5,71 @@ open Retroknowledge open Environ open CErrors -let add_retroknowledge env action = +type _ action_kind = + | IncompatTypes : _ prim_type -> Constant.t action_kind + | IncompatInd : _ prim_ind -> inductive action_kind + +type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn + +let check_same_types typ c1 c2 = + if not (Constant.equal c1 c2) + then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2)) + +let check_same_inds ind i1 i2 = + if not (eq_ind i1 i2) + then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2)) + +let add_retroknowledge retro action = match action with - | Register_type(PT_int63,c) -> - let retro = env.retroknowledge in - let retro = - match retro.retro_int63 with - | None -> { retro with retro_int63 = Some c } - | Some c' -> assert (Constant.equal c c'); retro in - set_retroknowledge env retro - | Register_type(PT_float64,c) -> - let retro = env.retroknowledge in - let retro = - match retro.retro_float64 with - | None -> { retro with retro_float64 = Some c } - | Some c' -> assert (Constant.equal c c'); retro in - set_retroknowledge env retro - | Register_type(PT_array,c) -> - let retro = env.retroknowledge in - let retro = - match retro.retro_array with - | None -> { retro with retro_array = Some c } - | Some c' -> assert (Constant.equal c c'); retro in - set_retroknowledge env retro + | Register_type(typ,c) -> + begin match typ with + | PT_int63 -> + (match retro.retro_int63 with + | None -> { retro with retro_int63 = Some c } + | Some c' -> check_same_types typ c c'; retro) + + | PT_float64 -> + (match retro.retro_float64 with + | None -> { retro with retro_float64 = Some c } + | Some c' -> check_same_types typ c c'; retro) + + | PT_array -> + (match retro.retro_array with + | None -> { retro with retro_array = Some c } + | Some c' -> check_same_types typ c c'; retro) + end + | Register_ind(pit,ind) -> - let retro = env.retroknowledge in - let retro = - match pit with + begin match pit with | PIT_bool -> let r = match retro.retro_bool with | None -> ((ind,1), (ind,2)) - | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_bool = Some r } | PIT_carry -> let r = match retro.retro_carry with | None -> ((ind,1), (ind,2)) - | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_carry = Some r } | PIT_pair -> let r = match retro.retro_pair with | None -> (ind,1) - | Some ((ind',_) as t) -> assert (eq_ind ind ind'); t in + | Some ((ind',_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_pair = Some r } | PIT_cmp -> let r = match retro.retro_cmp with | None -> ((ind,1), (ind,2), (ind,3)) - | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_,_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_cmp = Some r } | PIT_f_cmp -> let r = match retro.retro_f_cmp with | None -> ((ind,1), (ind,2), (ind,3), (ind,4)) - | Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_,_,_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_f_cmp = Some r } | PIT_f_class -> let r = @@ -69,10 +78,12 @@ let add_retroknowledge env action = (ind,5), (ind,6), (ind,7), (ind,8), (ind,9)) | Some (((ind',_),_,_,_,_,_,_,_,_) as t) -> - assert (eq_ind ind ind'); t in + check_same_inds pit ind ind'; t in { retro with retro_f_class = Some r } - in - set_retroknowledge env retro + end + +let add_retroknowledge env action = + set_retroknowledge env (add_retroknowledge env.retroknowledge action) let get_int_type env = match env.retroknowledge.retro_int63 with diff --git a/kernel/primred.mli b/kernel/primred.mli index 1bfaffaa44..6e9d4e297e 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -2,6 +2,13 @@ open Names open Environ (** {5 Reduction of primitives} *) +type _ action_kind = + | IncompatTypes : _ CPrimitives.prim_type -> Constant.t action_kind + | IncompatInd : _ CPrimitives.prim_ind -> inductive action_kind + +type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn + +(** May raise [IncomtibleDeclarations] *) val add_retroknowledge : env -> Retroknowledge.action -> env val get_int_type : env -> Constant.t diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 04e7a81697..48567aa564 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -88,7 +88,7 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = univs, typ | Some (typ,Monomorphic_entry uctx) -> - assert (AUContext.is_empty auctx); + assert (AUContext.is_empty auctx); (* ensured by ComPrimitive *) let env = push_context_set ~strict:true uctx env in let u = Instance.empty in let typ = @@ -99,12 +99,14 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = Monomorphic uctx, typ | Some (typ,Polymorphic_entry (unames,uctx)) -> - assert (not (AUContext.is_empty auctx)); - (* push_context will check that the universes aren't repeated in the instance - so comparing the sizes works *) - assert (AUContext.size auctx = UContext.size uctx); - (* No polymorphic primitive uses constraints currently *) - assert (Constraint.is_empty (UContext.constraints uctx)); + assert (not (AUContext.is_empty auctx)); (* ensured by ComPrimitive *) + (* [push_context] will check that the universes aren't repeated in + the instance so comparing the sizes works. No polymorphic + primitive uses constraints currently. *) + if not (AUContext.size auctx = UContext.size uctx + && Constraint.is_empty (UContext.constraints uctx)) + then CErrors.user_err Pp.(str "Incorrect universes for primitive " ++ + str (op_or_type_to_string p)); let env = push_context ~strict:false uctx env in (* Now we know that uctx matches the auctx *) let typ = (Typeops.infer_type env typ).utj_val in diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index ec429d5f9e..de604176cb 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names open Univ -open Constr (********************************************) (* Initialization of the abstract machine ***) @@ -61,8 +60,9 @@ type structured_constant = type reloc_table = (tag * int) array +(** When changing this, adapt Is_tailrec_switch in coq_values.h accordingly *) type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + { rtbl : reloc_table; tailcall : bool; max_stack_size : int } let rec eq_structured_values v1 v2 = v1 == v2 || @@ -123,22 +123,16 @@ let hash_structured_constant c = | Const_float f -> combinesmall 7 (Float64.hash f) let eq_annot_switch asw1 asw2 = - let eq_ci ci1 ci2 = - eq_ind ci1.ci_ind ci2.ci_ind && - Int.equal ci1.ci_npar ci2.ci_npar && - CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls - in let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in - eq_ci asw1.ci asw2.ci && CArray.equal eq_rlc asw1.rtbl asw2.rtbl && - (asw1.tailcall : bool) == asw2.tailcall + (asw1.tailcall : bool) == asw2.tailcall && + Int.equal asw1.max_stack_size asw2.max_stack_size let hash_annot_switch asw = let open Hashset.Combine in - let h1 = Constr.case_info_hash asw.ci in - let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in - let h3 = if asw.tailcall then 1 else 0 in - combine3 h1 h2 h3 + let h1 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in + let h2 = if asw.tailcall then 1 else 0 in + combine3 h1 h2 asw.max_stack_size let pp_sort s = let open Sorts in diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index f4070a02a3..f6efd49cfc 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Constr (** Values *) @@ -52,7 +51,7 @@ val pp_struct_const : structured_constant -> Pp.t type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + { rtbl : reloc_table; tailcall : bool; max_stack_size : int } val eq_structured_constant : structured_constant -> structured_constant -> bool val hash_structured_constant : structured_constant -> int diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 8adffdc709..f6a741f468 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -51,13 +51,19 @@ type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr (* NEW ssr term *) +type ast_glob_env = { + ast_ltacvars : Id.Set.t; + ast_extra : Genintern.Store.t; + ast_intern_sign : Genintern.intern_variable_status; +} + (* These terms are raw but closed with the intenalization/interpretation * context. It is up to the tactic receiving it to decide if such contexts * are useful or not, and eventually manipulate the term before turning it * into a constr *) type ast_closure_term = { body : Constrexpr.constr_expr; - glob_env : Genintern.glob_sign option; (* for Tacintern.intern_constr *) + glob_env : ast_glob_env option; (* for Tacintern.intern_constr *) interp_env : Geninterp.interp_sign option; (* for Tacinterp.interp_open_constr_with_bindings *) annotation : [ `None | `Parens | `DoubleParens | `At ]; } diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 65204b7868..1b7768852e 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -302,6 +302,11 @@ let mk_ast_closure_term a t = { } let glob_ast_closure_term (ist : Genintern.glob_sign) t = + let ist = { + ast_ltacvars = ist.Genintern.ltacvars; + ast_intern_sign = ist.Genintern.intern_sign; + ast_extra = ist.Genintern.extra; + } in { t with glob_env = Some ist } let subst_ast_closure_term (_s : Mod_subst.substitution) t = (* _s makes sense only for glob constr *) @@ -1124,8 +1129,7 @@ let tclDO n tac = let _, info = Exninfo.capture e in let e' = CErrors.UserError (l, prefix i ++ s) in Exninfo.iraise (e', info) - | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) -> - raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in + in let rec loop i gl = if i = n then tac_err_at i gl else (tclTHEN (tac_err_at i) (loop (i + 1))) gl in diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index a12b4aad11..1c81fbc10b 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -490,7 +490,6 @@ let equality_inj l b id c = let msg = ref "" in try Proofview.V82.of_tactic (Equality.inj None l b None c) gl with - | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s)) | CErrors.UserError (_,s) when msg := Pp.string_of_ppcmds s; !msg = "Not a projectable equality but a discriminable one." || diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index ad0a31622c..d99ead139d 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -150,7 +150,15 @@ let is_tac_in_term ?extra_scope { annotation; body; glob_env; interp_env } = let sigma = sigma goal in let ist = Ssrcommon.option_assert_get glob_env (Pp.str"not a term") in (* We use the env of the goal, not the global one *) - let ist = { ist with Genintern.genv } in + let ist = + let open Genintern in + { + ltacvars = ist.ast_ltacvars; + extra = ist.ast_extra; + intern_sign = ist.ast_intern_sign; + genv; + } + in (* We open extra_scope *) let body = match extra_scope with diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 414663c826..207ffc7b86 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -66,6 +66,7 @@ exception PretypeError of env * Evd.evar_map * pretype_error let precatchable_exception = function | CErrors.UserError _ | TypeError _ | PretypeError _ + | Reductionops.AnomalyInConversion _ | Nametab.GlobalizationError _ -> true | _ -> false diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 07154d4e03..c31ecc135c 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,8 +1,8 @@ Geninterp Locus Locusops -Pretype_errors Reductionops +Pretype_errors Inductiveops Arguments_renaming Retyping diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 594b8ab54c..fdc770dba6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1085,12 +1085,25 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV +(* NOTE: We absorb anomalies happening in the conversion tactic, which + is a bit ugly. This is mostly due to efficiency both in tactics and + in the conversion machinery itself. It is not uncommon for a tactic + to send some ill-typed term to the engine. + + We would usually say that a tactic that converts ill-typed terms is + buggy, but fixing the tactic could have a very large runtime cost + *) +exception AnomalyInConversion of exn + +let _ = CErrors.register_handler (function + | AnomalyInConversion e -> + Some Pp.(str "Conversion test raised an anomaly:" ++ + spc () ++ CErrors.print e) + | _ -> None) + let report_anomaly (e, info) = let e = - if is_anomaly e then - let msg = Pp.(str "Conversion test raised an anomaly:" ++ - spc () ++ CErrors.print e) in - UserError (None, msg) + if is_anomaly e then AnomalyInConversion e else e in Exninfo.iraise (e, info) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 218936edfb..0f288cdd46 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -283,3 +283,5 @@ val whd_betaiota_deltazeta_for_iota_state : (** {6 Meta-related reduction functions } *) val meta_instance : env -> evar_map -> constr freelisted -> constr val nf_meta : env -> evar_map -> constr -> constr + +exception AnomalyInConversion of exn diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 854a5ff63d..e5fa9bada1 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -262,19 +262,14 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> assert (from = 0) ; - let ci = sw.sw_annot.Vmvalues.ci in let ((mind,_ as ind), u), allargs = find_rectype_a env t in - let iv = if Typeops.should_invert_case env ci then - CaseInvert {univs=u; args=allargs} - else NoInvert - in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in - let p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in + let p, relevance = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma ind mib mip u params p in (* calcul des branches *) @@ -286,6 +281,11 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs c in + let ci = Inductiveops.make_case_info env ind relevance RegularStyle in + let iv = if Typeops.should_invert_case env ci then + CaseInvert {univs=u; args=allargs} + else NoInvert + in nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; @@ -296,17 +296,17 @@ and nf_stk ?from:(from=0) env sigma c t stk = and nf_predicate env sigma ind mip params v pT = match kind (whd_allnolet env pT) with | LetIn (name,b,t,pT) -> - let body = + let body, rel = nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in - mkLetIn (name,b,t,body) + mkLetIn (name,b,t,body), rel | Prod (name,dom,codom) -> begin match whd_val v with | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in - let body = + let body, rel = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in - mkLambda(name,dom,body) + mkLambda(name,dom,body), rel | _ -> assert false end | _ -> @@ -321,8 +321,10 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let r = Inductive.relevance_of_inductive env (fst ind) in let name = make_annot name r in - let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in - mkLambda(name,dom,body) + let env = push_rel (LocalAssum (name,dom)) env in + let body = nf_vtype env sigma vb in + let rel = Retyping.relevance_of_type env sigma (EConstr.of_constr body) in + mkLambda(name,dom,body), rel | _ -> assert false and nf_args env sigma vargs ?from:(f=0) t = diff --git a/printing/printer.ml b/printing/printer.ml index f8413f3588..c5cb6ffad8 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -257,11 +257,12 @@ let pr_puniverses f env sigma (c,u) = then f env c ++ pr_universe_instance sigma u else f env c -let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef cst) let pr_existential_key = Termops.pr_existential_key let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) -let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind) -let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (mkConstruct cstr) + +let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef cst) +let pr_inductive env ind = pr_global_env (Termops.vars_of_env env) (GlobRef.IndRef ind) +let pr_constructor env cstr = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstructRef cstr) let pr_pconstant = pr_puniverses pr_constant let pr_pinductive = pr_puniverses pr_inductive diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 82ce2234e3..63cafbf76d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -236,7 +236,7 @@ let with_prods nprods h f = f gl (h, diff) with e when CErrors.noncritical e -> let e, info = Exninfo.capture e in - Tacticals.New.tclZEROMSG ~info (CErrors.print e) end + Proofview.tclZERO ~info e end else Proofview.Goal.enter begin fun gl -> if Int.equal nprods 0 then f gl (h, None) diff --git a/test-suite/arithmetic/primitive.v b/test-suite/arithmetic/primitive.v deleted file mode 100644 index f62f6109e1..0000000000 --- a/test-suite/arithmetic/primitive.v +++ /dev/null @@ -1,12 +0,0 @@ -Section S. - Variable A : Type. - Fail Primitive int : let x := A in Set := #int63_type. - Fail Primitive add := #int63_add. -End S. - -(* [Primitive] should be forbidden in sections, otherwise its type after cooking -will be incorrect: - -Check int. - -*) diff --git a/test-suite/bugs/closed/bug_12534.v b/test-suite/bugs/closed/bug_12534.v new file mode 100644 index 0000000000..a55515feb6 --- /dev/null +++ b/test-suite/bugs/closed/bug_12534.v @@ -0,0 +1,9 @@ +Record C {PROP: Prop} (P : PROP) : Type := { c : unit}. +Check fun '{|c:=x|} => tt. (* Fine *) +Arguments Build_C {_ _} _. +Check fun '(Build_C _) => tt. (* Works. Note: just 1 argument! *) +Check fun '{|c:=x|} => tt. +(* Error: The constructor @Build_C (in type @C) expects 1 argument. *) + +Set Asymmetric Patterns. +Check fun '{|c:=x|} => tt. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 53ad8a9612..90a6a2ad96 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -80,6 +80,12 @@ NIL : list nat : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool)) fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z : (Z -> Z -> Z -> Z) -> Z +{|fun x : Z => x + x; 0|} + : Z +{|op; 0; 1|} + : Z +false = 0 + : Prop Init.Nat.add : nat -> nat -> nat S diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 7d2f1e9ba8..d0b2f40f9c 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -216,13 +216,32 @@ Check [|0*(1,2,3);(4,5,6)*false|]. (**********************************************************************) (* Test recursive notations involving applications *) -(* Caveat: does not work for applied constant because constants are *) -(* classified as notations for the particular constant while this *) -(* generic application notation is classified as generic *) + +Module Application. Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y). + +(* Application to a variable *) + Check fun f => {| f; 0; 1; 2 |} : Z. +(* Application to a fun *) + +Check {| (fun x => x+x); 0 |}. + +(* Application to a reference *) + +Axiom op : Z -> Z -> Z. +Check {| op; 0; 1 |}. + +(* Interaction with coercion *) + +Axiom c : Z -> bool. +Coercion c : Z >-> bool. +Check false = {| c; 0 |}. + +End Application. + (**********************************************************************) (* Check printing of notations from other modules *) diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 9cb019ca56..fa03ec8193 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -119,3 +119,7 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) +File "stdin", line 297, characters 0-30: +Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] +0 :=: 0 + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index b3270d4f92..90d8da2bec 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -290,3 +290,11 @@ Check V tt. Check fun x : nat => V x. End O. + +Module Bug12691. + +Notation "x :=: y" := True (at level 70, no associativity, only parsing). +Notation "x :=: y" := (x = y). +Check (0 :=: 0). + +End Bug12691. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index ba316ceb64..b8db52735d 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,7 +7,7 @@ bli : Type Axioms: bli : Type Axioms: -@seq relies on definitional UIP. +seq relies on definitional UIP. Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g diff --git a/test-suite/success/primitive.v b/test-suite/success/primitive.v new file mode 100644 index 0000000000..b2d02a0c49 --- /dev/null +++ b/test-suite/success/primitive.v @@ -0,0 +1,69 @@ +(* This file mostly tests for the error paths in declaring primitives. + Successes are tested in the various test-suite/primitive/* directories *) + +(* [Primitive] should be forbidden in sections, otherwise its type +after cooking will be incorrect. *) +Section S. + Variable A : Type. + Fail Primitive int : let x := A in Set := #int63_type. + Fail Primitive int := #int63_type. (* we fail even if section variable not used *) +End S. +Section S. + Fail Primitive int := #int63_type. (* we fail even if no section variables *) +End S. + +(* can't declare primitives with nonsense types *) +Fail Primitive xx : nat := #int63_type. + +(* non-cumulative conversion *) +Fail Primitive xx : Type := #int63_type. + +(* check evars *) +Fail Primitive xx : let x := _ in Set := #int63_type. + +(* explicit type is unified with expected type, not just converted + + extra universes are OK for monomorphic primitives (even though + their usefulness is questionable, there's no difference compared + with predeclaring them) + *) +Primitive xx : let x := Type in _ := #int63_type. + +(* double declaration *) +Fail Primitive yy := #int63_type. + +Module DoubleCarry. + (* XXX maybe should be an output test: this is the case where the new + declaration is already in the nametab so can be nicely printed *) + Module M. + Variant carry (A : Type) := + | C0 : A -> carry A + | C1 : A -> carry A. + + Register carry as kernel.ind_carry. + End M. + + Module N. + Variant carry (A : Type) := + | C0 : A -> carry A + | C1 : A -> carry A. + + Fail Register carry as kernel.ind_carry. + End N. +End DoubleCarry. + +(* univ polymorphic primitives *) + +(* universe count must be as expected *) +Fail Primitive array@{u v} : Type@{u} -> Type@{v} := #array_type. + +(* use a phantom universe to ensure we check conversion not just the universe count *) +Fail Primitive array@{u} : Set -> Set := #array_type. + +(* no constraints allowed! *) +Fail Primitive array@{u | Set < u} : Type@{u} -> Type@{u} := #array_type. + +(* unification works for polymorphic primitives too (although universe + counts mean it's not enough) *) +Fail Primitive array : let x := Type in _ -> Type := #array_type. +Primitive array : _ -> Type := #array_type. diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v index d3e2749088..3a6dfb1e11 100644 --- a/test-suite/success/sprop.v +++ b/test-suite/success/sprop.v @@ -171,6 +171,10 @@ End sFix. Fail Definition fix_relevance : _ -> nat := fun _ : iUnit => 0. +(* Check that VM/native properly keep the relevance of the predicate in the case info + (bad-relevance warning as error otherwise) *) +Definition vm_rebuild_case := Eval vm_compute in eq_sind. + Require Import ssreflect. Goal forall T : SProp, T -> True. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 7af09585d0..712cb6a135 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -15,6 +15,7 @@ Goal EQ nat 0 0. Hint Unfold EQ. auto. Qed. +End toto. (* Check regular failure when statically existing ref does not exist any longer at run time *) @@ -23,4 +24,71 @@ Goal let x := 0 in True. intro x. Fail (clear x; unfold x). Abort. -End toto. + +(* Static analysis of unfold *) + +Module A. + +Opaque id. +Ltac f := unfold id. +Goal id 0 = 0. +Fail f. +Transparent id. +f. +Abort. + +End A. + +Module B. + +Module Type T. Axiom n : nat. End T. + +Module F(X:T). +Ltac f := unfold X.n. +End F. + +Module M. Definition n := 0. End M. +Module N := F M. +Goal match M.n with 0 => 0 | S _ => 1 end = 0. +N.f. +match goal with |- 0=0 => idtac end. +Abort. + +End B. + +Module C. + +(* We reject inductive types and constructors *) + +Fail Ltac g := unfold nat. +Fail Ltac g := unfold S. + +End C. + +Module D. + +(* In interactive mode, we delay the interpretation of short names *) + +Notation x := Nat.add. + +Goal let x := 0 in x = 0+0. +unfold x. +match goal with |- 0 = 0 => idtac end. +Abort. + +Goal let x := 0 in x = 0+0. +intro; unfold x. (* dynamic binding (but is it really the most natural?) *) +match goal with |- 0 = 0+0 => idtac end. +Abort. + +Goal let fst := 0 in fst = Datatypes.fst (0,0). +unfold fst. +match goal with |- 0 = 0 => idtac end. +Abort. + +Goal let fst := 0 in fst = Datatypes.fst (0,0). +intro; unfold fst. (* dynamic binding *) +match goal with |- 0 = Datatypes.fst (0,0) => idtac end. +Abort. + +End D. diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index a2d7013dfa..b346b3ee5c 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -88,7 +88,8 @@ let inj_wit ?loc wit x = let of_variable {loc;v=id} = let qid = Libnames.qualid_of_ident ?loc id in if Tac2env.is_constructor qid then - CErrors.user_err ?loc (str "Invalid identifier") + CErrors.user_err ?loc (str "Invalid identifier" ++ spc () ++ Id.print id ++ + spc () ++ str "classifying as an Ltac2 constructor") else CAst.make ?loc @@ CTacRef (RelId qid) let of_anti f = function @@ -229,15 +230,19 @@ let pattern_vars pat = let rec aux () accu pat = match pat.CAst.v with | Constrexpr.CPatVar id | Constrexpr.CEvar (id, []) -> - let () = check_pattern_id ?loc:pat.CAst.loc id in - Id.Set.add id accu + let loc = pat.CAst.loc in + let () = check_pattern_id ?loc id in + Id.Map.add id loc accu | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun _ () -> ()) aux () accu pat in - aux () Id.Set.empty pat + aux () Id.Map.empty pat let abstract_vars loc ?typ vars tac = - let get_name = function Name id -> Some id | Anonymous -> None in + let get_name na = match na.CAst.v with + | Name id -> Some (CAst.make ?loc:na.CAst.loc id) + | Anonymous -> None + in let def = try Some (List.find_map get_name vars) with Not_found -> None in let na, tac = match def with | None -> (Anonymous, tac) @@ -245,18 +250,18 @@ let abstract_vars loc ?typ vars tac = (* Trick: in order not to shadow a variable nor to choose an arbitrary name, we reuse one which is going to be shadowed by the matched variables anyways. *) - let build_bindings (n, accu) na = match na with + let build_bindings (n, accu) { CAst.loc; CAst.v = na } = match na with | Anonymous -> (n + 1, accu) | Name _ -> let get = global_ref ?loc (kername array_prefix "get") in - let args = [of_variable CAst.(make ?loc id0); of_int CAst.(make ?loc n)] in + let args = [of_variable id0; of_int CAst.(make ?loc n)] in let e = CAst.make ?loc @@ CTacApp (get, args) in let accu = (CAst.make ?loc @@ CPatVar na, e) :: accu in (n + 1, accu) in let (_, bnd) = List.fold_left build_bindings (0, []) vars in let tac = CAst.make ?loc @@ CTacLet (false, bnd, tac) in - (Name id0, tac) + (Name id0.CAst.v, tac) in let pat = CAst.make ?loc @@ CPatVar na in let pat = match typ with @@ -281,7 +286,7 @@ let of_conversion {loc;v=c} = match c with let pat = of_option ?loc of_pattern (Some pat) in let c = of_constr c in (* Order is critical here *) - let vars = List.map (fun id -> Name id) (Id.Set.elements vars) in + let vars = List.map (fun (id, loc) -> CAst.make ?loc (Name id)) (Id.Map.bindings vars) in let c = abstract_vars loc vars c in of_tuple [pat; c] @@ -406,8 +411,8 @@ let of_constr_matching {loc;v=m} = in let vars = pattern_vars pat in (* Order of elements is crucial here! *) - let vars = Id.Set.elements vars in - let vars = List.map (fun id -> Name id) vars in + let vars = Id.Map.bindings vars in + let vars = List.map (fun (id, loc) -> CAst.make ?loc (Name id)) vars in (* Annotate the bound array variable with constr type *) let typ = let t_constr = coq_core "constr" in @@ -428,11 +433,11 @@ let of_goal_matching {loc;v=gm} = let mk_pat {loc;v=p} = match p with | QConstrMatchPattern pat -> let knd = constructor ?loc (pattern_core "MatchPattern") [] in - (Anonymous, pat, knd) + (CAst.make ?loc Anonymous, pat, knd) | QConstrMatchContext (id, pat) -> let na = extract_name ?loc id in let knd = constructor ?loc (pattern_core "MatchContext") [] in - (na, pat, knd) + (CAst.make ?loc na, pat, knd) in let mk_gpat {loc;v=p} = let concl_pat = p.q_goal_match_concl in @@ -442,23 +447,22 @@ let of_goal_matching {loc;v=gm} = let map accu (na, pat) = let (ctx, pat, knd) = mk_pat pat in let vars = pattern_vars pat in - (Id.Set.union vars accu, (na, ctx, pat, knd)) + (Id.Map.fold Id.Map.add vars accu, (na, ctx, pat, knd)) in let (vars, hyps_pats) = List.fold_left_map map vars hyps_pats in let map (_, _, pat, knd) = of_tuple [knd; of_pattern pat] in let concl = of_tuple [concl_knd; of_pattern concl_pat] in let r = of_tuple [of_list ?loc map hyps_pats; concl] in - let hyps = List.map (fun ({CAst.v=na}, _, _, _) -> na) hyps_pats in - let map (_, na, _, _) = na in - let hctx = List.map map hyps_pats in + let hyps = List.map (fun (na, _, _, _) -> na) hyps_pats in + let hctx = List.map (fun (_, na, _, _) -> na) hyps_pats in (* Order of elements is crucial here! *) - let vars = Id.Set.elements vars in - let subst = List.map (fun id -> Name id) vars in + let vars = Id.Map.bindings vars in + let subst = List.map (fun (id, loc) -> CAst.make ?loc (Name id)) vars in (r, hyps, hctx, subst, concl_ctx) in let map {loc;v=(pat, tac)} = let (pat, hyps, hctx, subst, cctx) = mk_gpat pat in - let tac = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar cctx], tac) in + let tac = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar cctx.CAst.v], tac) in let tac = abstract_vars loc subst tac in let tac = abstract_vars loc hctx tac in let tac = abstract_vars loc hyps tac in diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml index 110dcdc98a..eaa5271a73 100644 --- a/vernac/comPrimitive.ml +++ b/vernac/comPrimitive.ml @@ -38,7 +38,13 @@ let do_primitive id udecl prim typopt = Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env) env evd typ in - let evd = Evarconv.unify_delay env evd typ expected_typ in + let evd = try Evarconv.unify_delay env evd typ expected_typ + with Evarconv.UnableToUnify (evd,e) as exn -> + let _, info = Exninfo.capture exn in + Exninfo.iraise (Pretype_errors.( + PretypeError (env,evd,CannotUnify (typ,expected_typ,Some e)),info)) + in + Pretyping.check_evars_are_solved ~program_mode:false env evd; let evd = Evd.minimize_universes evd in let uvars = EConstr.universes_of_constr evd typ in let evd = Evd.restrict_universe_context evd uvars in diff --git a/vernac/declare.ml b/vernac/declare.ml index df75e121d8..eedbee852b 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -535,10 +535,13 @@ module Internal = struct ; proof_entry_type = Some typ }, args - type nonrec constant_obj = constant_obj + module Constant = struct + type t = constant_obj + let tag = objConstant + let kind obj = obj.cst_kind + end let objVariable = objVariable - let objConstant = objConstant end @@ -1149,13 +1152,6 @@ let declare_mutual_definition ~pm l = Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) | IsCoFixpoint -> None in - (* In the future we will pack all this in a proper record *) - (* XXX: info refactoring *) - let _kind = - if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) - else Decls.(IsDefinition CoFixpoint) - in - let scope = first.prg_info.Info.scope in (* Declare the recursive definitions *) let kns = declare_mutually_recursive_core ~info:first.prg_info ~ntns:first.prg_notations @@ -1164,6 +1160,7 @@ let declare_mutual_definition ~pm l = in (* Only for the first constant *) let dref = List.hd kns in + let scope = first.prg_info.Info.scope in let s_hook = {Hook.S.uctx = first.prg_uctx; obls; scope; dref} in Hook.call ?hook:first.prg_info.Info.hook s_hook; (* XXX: We call the obligation hook here, by consistency with the @@ -1500,7 +1497,7 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl = in match cinfo with | [] -> CErrors.anomaly (Pp.str "No proof to start.") - | { CInfo.name; typ; impargs; _} :: thms -> + | { CInfo.name; typ; _} :: thms -> let pinfo = Proof_info.make ~cinfo ~info ~compute_guard () in (* start_lemma has the responsibility to add (name, impargs, typ) to thms, once Info.t is more refined this won't be necessary *) diff --git a/vernac/declare.mli b/vernac/declare.mli index adb5bd026f..c5a8afbad5 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -556,9 +556,13 @@ end module Internal : sig - type constant_obj + (* Liboject exports *) + module Constant : sig + type t + val tag : t Libobject.Dyn.tag + val kind : t -> Decls.logical_kind + end - val objConstant : constant_obj Libobject.Dyn.tag val objVariable : unit Libobject.Dyn.tag end diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f9ecf10d1b..762c95fffe 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1252,6 +1252,29 @@ let explain_inductive_error = function error_large_non_prop_inductive_not_in_type () | MissingConstraints csts -> error_inductive_missing_constraints csts +(* Primitive errors *) + +let explain_incompatible_prim_declarations (type a) (act:a Primred.action_kind) (x:a) (y:a) = + let open Primred in + let env = Global.env() in + (* The newer constant/inductive (either coming from Primitive or a + Require) may be absent from the nametab as the error got raised + while adding it to the safe_env. In that case we can't use + nametab printing. + + There are still cases where the constant/inductive is added + separately from its retroknowledge (using Register), so we still + try nametab based printing. *) + match act with + | IncompatTypes typ -> + let px = try pr_constant env x with Not_found -> Constant.print x in + str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_type_to_string typ) ++ + str ": " ++ pr_constant env y ++ str " is already declared." + | IncompatInd ind -> + let px = try pr_inductive env x with Not_found -> MutInd.print (fst x) in + str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_ind_to_string ind) ++ + str ": " ++ pr_inductive env y ++ str " is already declared." + (* Recursion schemes errors *) let explain_recursion_scheme_error env = function @@ -1386,6 +1409,8 @@ let rec vernac_interp_error_handler = function explain_typeclass_error env sigma te | InductiveError e -> explain_inductive_error e + | Primred.IncompatibleDeclarations (act,x,y) -> + explain_incompatible_prim_declarations act x y | Modops.ModuleTypingError e -> explain_module_error e | Modintern.ModuleInternalizationError e -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index e9b86f323b..6cc48d0e48 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1579,9 +1579,12 @@ let warn_irrelevant_format = let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in let custom,level,_ = sd.level in - let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in - if sd.only_parsing then (if sd.format <> None then warn_irrelevant_format (); None) - else Some { + let format = + if sd.only_parsing && sd.format <> None then (warn_irrelevant_format (); None) + else sd.format in + let pp_rule = make_pp_rule level sd.pp_syntax_data format in + (* We produce a generic rule even if this precise notation is only parsing *) + Some { synext_reserved = reserved; synext_unparsing = (pp_rule,level); synext_extra = sd.extra; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e0974ac027..b93c920654 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1331,10 +1331,8 @@ let pr_vernac_attributes = | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () let pr_vernac ({v = {control; attrs; expr}} as v) = - try - tag_vernac v - (pr_vernac_control control ++ - pr_vernac_attributes attrs ++ - pr_vernac_expr expr ++ - sep_end expr) - with e -> CErrors.print e + tag_vernac v + (pr_vernac_control control ++ + pr_vernac_attributes attrs ++ + pr_vernac_expr expr ++ + sep_end expr) diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 176ddd6c5b..2b46542287 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -688,7 +688,7 @@ let gallina_print_leaf_entry env sigma with_values ((sp, kn),lobj) = constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) end @@ - DynHandle.add Declare.Internal.objConstant begin fun _ -> + DynHandle.add Declare.Internal.Constant.tag begin fun _ -> Some (print_constant with_values sep (Constant.make1 kn) None) end @@ DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> @@ -796,7 +796,7 @@ let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let handler = - DynHandleF.add Declare.Internal.objConstant begin fun _ -> + DynHandleF.add Declare.Internal.Constant.tag begin fun _ -> let con = Global.constant_of_delta_kn kn in let cb = Global.lookup_constant con in let typ = cb.const_type in diff --git a/vernac/search.ml b/vernac/search.ml index 2a21184c1e..abefeab779 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -79,11 +79,11 @@ let generic_search env (fn : GlobRef.t -> Decls.logical_kind option -> env -> co let iter_obj (sp, kn) lobj = match lobj with | AtomicObject o -> let handler = - DynHandle.add Declare.Internal.objConstant begin fun _ -> + DynHandle.add Declare.Internal.Constant.tag begin fun obj -> let cst = Global.constant_of_delta_kn kn in let gr = GlobRef.ConstRef cst in let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in - let kind = Dumpglob.constant_kind cst in + let kind = Declare.Internal.Constant.kind obj in fn gr (Some kind) env typ end @@ DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> |