diff options
134 files changed, 1500 insertions, 588 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 9b208f5a24..b1709e1921 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-09-17-V88" + CACHEKEY: "bionic_coq-V2020-10-12-V89" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/Makefile.build b/Makefile.build index eed3c2813a..526a8c5831 100644 --- a/Makefile.build +++ b/Makefile.build @@ -401,6 +401,12 @@ kernel/uint63.ml: kernel/uint63_$(OCAML_INT_SIZE).ml rm -f $@ && cp $< $@ && chmod a-w $@ ########################################################################### +# Specific rules for Float64 +########################################################################### +kernel/float64.ml: kernel/float64_$(OCAML_INT_SIZE).ml + rm -f $@ && cp $< $@ && chmod a-w $@ + +########################################################################### # Main targets (coqtop.opt, coqtop.byte) ########################################################################### diff --git a/Makefile.make b/Makefile.make index 51d6d1c3c1..34f5707ae8 100644 --- a/Makefile.make +++ b/Makefile.make @@ -107,7 +107,7 @@ GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES)) GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES? GENMLGFILES:= $(MLGFILES:.mlg=.ml) -GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml +GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml kernel/float64.ml GENMLIFILES:=$(GRAMMLIFILES) GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fcc585117b..fc8921e63d 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1204,7 +1204,7 @@ function make_elpi { make_dune make_re - if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz 1 elpi; then + if build_prep https://github.com/LPCIC/elpi/archive v1.11.4 tar.gz 1 elpi; then log2 dune build -p elpi log2 dune install elpi diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index f672ead807..c17ec502e7 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-09-17-V88" +# CACHEKEY: "bionic_coq-V2020-10-12-V89" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -43,7 +43,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.11.0" + BASE_ONLY_OPAM="elpi.1.11.4" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" diff --git a/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh new file mode 100644 index 0000000000..fb5947d218 --- /dev/null +++ b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12449" ] || [ "$CI_BRANCH" = "minim-prop-toset" ]; then + + mtac2_CI_REF=janno/coq-12449 + mtac2_CI_GITURL=https://github.com/mtac2/mtac2 + +fi diff --git a/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh new file mode 100644 index 0000000000..7d55cf6883 --- /dev/null +++ b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13166" ] || [ "$CI_BRANCH" = "master+fixes13165-missing-impargs-defined-fields" ]; then + + elpi_CI_REF=coq-master+adapt-coq-pr13166-impargs-record-fields + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index fb5d7cc244..6a6318f97a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,22 +1,35 @@ ## Changes between Coq 8.12 and Coq 8.13 -- Tactic language: TacGeneric now takes an argument to tell if it - comes from a notation. Use `None` if not and `Some foo` to tell to - print such TacGeneric surrounded with `foo:( )`. - ### Code formatting - The automatic code formatting tool `ocamlformat` has been disabled and its git hook removed. If desired, automatic formatting can be achieved by calling the `fmt` target of the dune build system. -### Pp library +### ML API + +Abstract syntax of tactic: + +- TacGeneric now takes an argument to tell if it comes from a + notation. Use `None` if not and `Some foo` to tell to print such + TacGeneric surrounded with `foo:( )`. + +Printing functions: - `Pp.h` does not take a `int` argument anymore (the argument was not used). In general, where `h n` for `n` non zero was used, `hv n` was instead intended. If cancelling the breaking role of cuts in the box was intended, turn `h n c` into `h c`. +Grammar entries: + +- `Prim.pattern_identref` is deprecated, use `Prim.pattern_ident` + which now returns a located identifier. + +Generic arguments: + +- Generic arguments: `wit_var` is deprecated, use `wit_hyp`. + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/doc/changelog/02-specification-language/10331-minim-prop-toset.rst b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst new file mode 100644 index 0000000000..6c442ca1aa --- /dev/null +++ b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst @@ -0,0 +1,5 @@ +- **Changed:** Heuristics for universe minimization to :g:`Set`: also + use constraints ``Prop <= i`` (`#10331 + <https://github.com/coq/coq/pull/10331>`_, by Gaëtan Gilbert with + help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 + <https://github.com/coq/coq/issues/12414>`_). diff --git a/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst new file mode 100644 index 0000000000..006989e6b3 --- /dev/null +++ b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 <https://github.com/coq/coq/pull/13166>`_, + fixes `#13165 <https://github.com/coq/coq/issues/13165>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst new file mode 100644 index 0000000000..16fc91f911 --- /dev/null +++ b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst @@ -0,0 +1,10 @@ +- **Changed:** + New model for ``only parsing`` and ``only printing`` notations with + support for at most one parsing-and-printing or only-parsing + notation per notation and scope, but an arbitrary number of + only-printing notations + (`#12950 <https://github.com/coq/coq/pull/12950>`_, + fixes `#4738 <https://github.com/coq/coq/issues/4738>`_ + and `#9682 <https://github.com/coq/coq/issues/9682>`_ + and part 2 of `#12908 <https://github.com/coq/coq/issues/12908>`_, + by Hugo Herbelin). diff --git a/doc/changelog/09-coqide/12874-show_proof_diffs.rst b/doc/changelog/09-coqide/12874-show_proof_diffs.rst new file mode 100644 index 0000000000..51bebad9be --- /dev/null +++ b/doc/changelog/09-coqide/12874-show_proof_diffs.rst @@ -0,0 +1,5 @@ +- **Added:** + Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu. + See :ref:`showing_proof_diffs`. + (`#12874 <https://github.com/coq/coq/pull/12874>`_, + by Jim Fehrle and Enrico Tassi) diff --git a/doc/sphinx/_static/diffs-show-proof.png b/doc/sphinx/_static/diffs-show-proof.png Binary files differnew file mode 100644 index 0000000000..62bd9cccd0 --- /dev/null +++ b/doc/sphinx/_static/diffs-show-proof.png diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 4cdfba146a..39b154de8d 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -13,7 +13,7 @@ Inductive types .. prodn:: inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } - | {? @ident } %{ {*; @record_field } %} + | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } This command defines one or more diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index cd44d06e67..b2099b8636 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -18,12 +18,12 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. insertprodn record_definition field_def .. prodn:: - record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } + record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations } record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations } field_body ::= {* @binder } @of_type | {* @binder } @of_type := @term | {* @binder } := @term - term_record ::= %{%| {* @field_def } %|%} + term_record ::= %{%| {*; @field_def } {? ; } %|%} field_def ::= @qualid {* @binder } := @term diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index f90ebadb3a..edd93f2266 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -590,11 +590,11 @@ Requesting information constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier. - Experimental: Specifying “Diffs” highlights the difference between the + Specifying “Diffs” highlights the difference between the current and previous proof step. By default, the command shows the output once with additions highlighted. Including “removed” shows the output twice: once showing removals and once showing additions. - It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. + It does not examine the :opt:`Diffs` option. See :ref:`showing_proof_diffs`. .. cmdv:: Show Conjectures :name: Show Conjectures @@ -675,12 +675,9 @@ Requesting information Showing differences between proof steps --------------------------------------- - Coq can automatically highlight the differences between successive proof steps -and between values in some error messages. Also, as an experimental feature, -Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` -command, but only, for now, when using coqtop and Proof General. - +and between values in some error messages. Coq can also highlight differences +in the proof term. For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added @@ -826,14 +823,37 @@ the split because it has not changed. .. image:: ../_static/diffs-coqide-multigoal.png :alt: coqide with Set Diffs on with multiple goals -This is how diffs may appear after applying a :tacn:`intro` tactic that results -in compacted hypotheses: +Diffs may appear like this after applying a :tacn:`intro` tactic that results +in a compacted hypotheses: .. .. image:: ../_static/diffs-coqide-compacted.png :alt: coqide with Set Diffs on with compacted hypotheses +.. _showing_proof_diffs: + +"Show Proof" differences +```````````````````````` + +To show differences in the proof term: + +- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command. + +- In CoqIDE, position the cursor on or just after a tactic to compare the proof term + after the tactic with the proof term before the tactic, then select + `View / Show Proof` from the menu or enter the associated key binding. + Differences will be shown applying the current `Show Diffs` setting + from the `View` menu. If the current setting is `Don't show diffs`, diffs + will not be shown. + + Output with the "added and removed" option looks like this: + + .. + + .. image:: ../_static/diffs-show-proof.png + :alt: coqide with Set Diffs on with compacted hypotheses + Controlling the effect of proof editing commands ------------------------------------------------ @@ -858,6 +878,11 @@ Controlling the effect of proof editing commands proved before starting the previous proof) and Coq will switch back to the proof of the previous assertion. +.. flag:: Printing Goal Names + + When turned on, the name of the goal is printed in interactive + proof mode, which can be useful in cases of cross references + between goals. Controlling memory usage ------------------------ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5148fa84c9..d6db305300 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -57,15 +57,14 @@ to represent :g:`(and A B)`: Notations must be in double quotes, except when the abbreviation has the form of an ordinary applicative expression; see :ref:`Abbreviations`. The notation consists of *tokens* separated by -spaces. Alphanumeric strings (such as ``A`` and ``B``) are the *parameters* +spaces. Tokens which are identifiers (such as ``A``, ``x0'``, etc.) are the *parameters* of the notation. Each of them must occur at least once in the abbreviated term. The other elements of the string (such as ``/\``) are the *symbols*. -Substrings enclosed in single quotes are treated as literals. This is necessary -for substrings that would otherwise be interpreted as :n:`@ident`\s. Similarly, -every symbol of at least 3 characters and starting with a simple quote -must be quoted (then it starts by two single quotes). Here is an -example. +Identifiers enclosed in single quotes are treated as symbols and thus +lose their role of parameters. In the same vein, every symbol of at +least 3 characters and starting with a simple quote must be quoted +(then it starts with two single quotes). Here is an example. .. coqtop:: in @@ -82,7 +81,8 @@ associativity rules have to be given. The right-hand side of a notation is interpreted at the time the notation is given. In particular, disambiguation of constants, :ref:`implicit arguments <ImplicitArguments>` and other notations are resolved at the - time of the declaration of the notation. + time of the declaration of the notation. The right-hand side is + currently typed only at use time but this may change in the future. Precedences and associativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -299,12 +299,29 @@ Notations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. -.. note:: Sometimes, a notation is expected only for the parser. To do - so, the option ``only parsing`` is allowed in the list of :n:`@syntax_modifier`\s - in :cmd:`Notation`. Conversely, the ``only printing`` :n:`@syntax_modifier` can be - used to declare that a notation should only be used for printing and - should not declare a parsing rule. In particular, such notations do - not modify the parser. +.. note:: + + The default for a notation is to be used both for parsing and + printing. It is possible to declare a notation only for parsing by + adding the option ``only parsing`` to the list of + :n:`@syntax_modifier`\s of :cmd:`Notation`. Symmetrically, the + ``only printing`` :n:`@syntax_modifier` can be used to declare that + a notation should only be used for printing. + + If a notation to be used both for parsing and printing is + overriden, both the parsing and printing are invalided, even if the + overriding rule is only parsing. + + If a given notation string occurs only in ``only printing`` rules, + the parser is not modified at all. + + To a given notation string and scope can be attached at most one + notation with both parsing and printing or with only + parsing. Contrastingly, an arbitrary number of ``only printing`` + notations differing in their right-hand sides but only a unique + right-hand side can be attached to a given string and + scope. Obviously, expressions printed by means of such extra + printing rules will not be reparsed to the same form. The Infix command ~~~~~~~~~~~~~~~~~~ diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index a9f9c805d8..1e9be8dded 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -396,8 +396,8 @@ operconstr0: [ (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *) | DELETE "{" binder_constr "}" | REPLACE "{|" record_declaration bar_cbrace -| WITH "{|" LIST0 field_def bar_cbrace -| MOVETO term_record "{|" LIST0 field_def bar_cbrace +| WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace +| MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace | MOVETO term_generalizing "`{" operconstr200 "}" | MOVETO term_generalizing "`(" operconstr200 ")" | MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")" @@ -585,7 +585,7 @@ constructor_list_or_record_decl: [ record_fields: [ | REPLACE record_field ";" record_fields -| WITH LIST0 record_field SEP ";" +| WITH LIST0 record_field SEP ";" OPT ";" | DELETE record_field | DELETE (* empty *) ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 067050b4f5..73641976e3 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1740,11 +1740,11 @@ simple_tactic: [ | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) | "omega" (* omega plugin *) -| "rtauto" | "protect_fv" string "in" ident (* ring plugin *) | "protect_fv" string (* ring plugin *) | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) | "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* ring plugin *) +| "rtauto" ] mlname: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index cbef29fb39..61befe9f1f 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -539,7 +539,7 @@ variant_definition: [ ] record_definition: [ -| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" "}" OPT decl_notations +| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" OPT decl_notations ] record_field: [ @@ -553,7 +553,7 @@ field_body: [ ] term_record: [ -| "{|" LIST0 field_def "|}" +| "{|" LIST0 field_def SEP ";" OPT ";" "|}" ] field_def: [ @@ -566,7 +566,7 @@ inductive_definition: [ constructors_or_record: [ | OPT "|" LIST1 constructor SEP "|" -| OPT ident "{" LIST0 record_field SEP ";" "}" +| OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" ] constructor: [ diff --git a/engine/uState.ml b/engine/uState.ml index 2cb88c7fff..9557111cfd 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -675,7 +675,7 @@ let subst_univs_context_with_def def usubst (ctx, cst) = (LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst) let is_trivial_leq (l,d,r) = - Level.is_prop l && (d == Le || (d == Lt && Level.is_set r)) + Level.is_prop l && (d == Le || d == Lt) && Level.is_set r (* Prop < i <-> Set+1 <= i <-> Set < i *) let translate_cstr (l,d,r as cstr) = diff --git a/engine/univMinim.ml b/engine/univMinim.ml index c5854e27f3..4ed6e97526 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -292,17 +292,23 @@ let is_bound l lbound = match lbound with | UGraph.Bound.Prop -> Level.is_prop l | UGraph.Bound.Set -> Level.is_set l +(* if [is_minimal u] then constraints [u <= v] may be dropped and get + used only for set_minimization. *) +let is_minimal ~lbound u = + Level.is_sprop u || Level.is_prop u || is_bound u lbound + (* TODO check is_small/sprop *) let normalize_context_set ~lbound g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts + Constraint.partition (fun (l,d,r) -> d == Le && is_minimal ~lbound l) csts in let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles else Constraint.empty in + let smallles = Constraint.map (fun (_,_,r) -> Level.set, Le, r) smallles in let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) diff --git a/ide/.merlin.in b/ide/.merlin.in index b8d7953833..50816ae3f5 100644 --- a/ide/.merlin.in +++ b/ide/.merlin.in @@ -1,8 +1,10 @@ PKG unix laglgtk3 lablgtk3-sourceview3 -S utils -B utils -S protocol -B protocol +S coqide/utils +B coqide/utils +S coqide/protocol +B coqide/protocol +S coqide/ +B coqide/ REC diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 038c8b91a8..1167b8199e 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -512,6 +512,7 @@ let hints x = eval_call (Xmlprotocol.hints x) let search flags = eval_call (Xmlprotocol.search flags) let init x = eval_call (Xmlprotocol.init x) let stop_worker x = eval_call (Xmlprotocol.stop_worker x) +let proof_diff x = eval_call (Xmlprotocol.proof_diff x) let break_coqtop coqtop workers = if coqtop.status = Busy then @@ -579,6 +580,9 @@ struct let set (type a) (opt : a t) (v : a) = Hashtbl.replace current_state (opt_name opt) (opt_data opt v) + let get (type a) (opt : a t) = + Hashtbl.find current_state (opt_name opt) + let reset () = let init_descr d = List.iter (fun o -> set o d.init) d.opts in List.iter init_descr bool_items; diff --git a/ide/coqide/coq.mli b/ide/coqide/coq.mli index 82df36c91c..aaaf14e4d0 100644 --- a/ide/coqide/coq.mli +++ b/ide/coqide/coq.mli @@ -127,6 +127,7 @@ val hints : Interface.hints_sty -> Interface.hints_rty query val mkcases : Interface.mkcases_sty -> Interface.mkcases_rty query val search : Interface.search_sty -> Interface.search_rty query val init : Interface.init_sty -> Interface.init_rty query +val proof_diff : Interface.proof_diff_sty -> Interface.proof_diff_rty query val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query @@ -144,6 +145,10 @@ sig val set : 'a t -> 'a -> unit + val get : 'a t -> Interface.option_value + + val diff : string t + val printing_unfocused: unit -> bool (** [enforce] transmits to coq the current option values. diff --git a/ide/coqide/coqOps.ml b/ide/coqide/coqOps.ml index 29ea3ce9ea..97076745a3 100644 --- a/ide/coqide/coqOps.ml +++ b/ide/coqide/coqOps.ml @@ -142,6 +142,7 @@ object method handle_reset_initial : unit task method raw_coq_query : route_id:int -> next:(query_rty value -> unit task) -> string -> unit task + method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task method show_goals : unit task method backtrack_last_phrase : unit task method initialize : unit task @@ -361,6 +362,27 @@ object(self) let query = Coq.query (route_id,(phrase,sid)) in Coq.bind (Coq.seq action query) next + method proof_diff where ~next : unit Coq.task = + (* todo: would be nice to ignore comments, too *) + let rec back iter = + if iter#is_start then iter + else + let c = iter#char in + if Glib.Unichar.isspace c || c = 0 then back (iter#backward_char) + else if c = int_of_char '.' then iter#backward_char + else iter in + + let where = back (buffer#get_iter_at_mark where) in + let until _ start stop = + (buffer#get_iter_at_mark stop)#compare where >= 0 && + (buffer#get_iter_at_mark start)#compare where <= 0 in + let state_id = fst @@ self#find_id until in + let diff_opt = Interface.(match Coq.PrintOpt.(get diff) with + | StringValue diffs -> diffs + | _ -> "off") in + let proof_diff = Coq.proof_diff (diff_opt, state_id) in + Coq.bind proof_diff next + method private still_valid { edit_id = id } = try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true with Not_found -> false diff --git a/ide/coqide/coqOps.mli b/ide/coqide/coqOps.mli index 3a4678ae9c..84911a6aa8 100644 --- a/ide/coqide/coqOps.mli +++ b/ide/coqide/coqOps.mli @@ -20,6 +20,7 @@ object method handle_reset_initial : unit task method raw_coq_query : route_id:int -> next:(query_rty value -> unit task) -> string -> unit task + method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task method show_goals : unit task method backtrack_last_phrase : unit task method initialize : unit task @@ -30,7 +31,6 @@ object method get_errors : (int * string) list method get_slaves_status : int * int * string CString.Map.t - method handle_failure : handle_exn_rty -> unit task method destroy : unit -> unit diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml index b66da11e7b..f9e6e74372 100644 --- a/ide/coqide/coqide.ml +++ b/ide/coqide/coqide.ml @@ -747,6 +747,24 @@ let coq_icon () = let dir = List.find chk (Minilib.coqide_data_dirs ()) in Filename.concat dir name +let show_proof_diff where sn = + sn.messages#default_route#clear; + Coq.try_grab sn.coqtop (sn.coqops#proof_diff where + ~next:(function + | Interface.Fail (_, _, err) -> + let err = if (Pp.string_of_ppcmds err) <> "No proofs to diff." then err else + Pp.str "Put the cursor over proven lines for \"Show Proof\" diffs" + in + let err = Ideutils.validate err in + sn.messages#default_route#add err; + Coq.return () + | Interface.Good diff -> + sn.messages#default_route#add diff; + Coq.return ())) + ignore + +let show_proof_diffs _ = cb_on_current_term (show_proof_diff `INSERT) () + let about _ = let dialog = GWindow.about_dialog () in let _ = dialog#connect#response ~callback:(fun _ -> dialog#destroy ()) in @@ -1103,6 +1121,8 @@ let build_ui () = radio "Set diff" 1 ~label:"Show diffs: only _added"; radio "Set removed diff" 2 ~label:"Show diffs: added and _removed"; ]; + item "Show Proof Diffs" ~label:"_Show Proof (with diffs, if set)" ~accel:(modifier_for_display#get ^ "S") + ~callback:MiscMenu.show_proof_diffs; ]; toggle_items view_menu Coq.PrintOpt.bool_items; @@ -1352,6 +1372,11 @@ let main files = this default coqtop path *) let read_coqide_args argv = + let set_debug () = + Minilib.debug := true; + Flags.debug := true; + Exninfo.record_backtrace true + in let rec filter_coqtop coqtop project_files bindings_files out = function |"-unicode-bindings" :: sfilenames :: args -> let filenames = Str.split (Str.regexp ",") sfilenames in @@ -1371,10 +1396,12 @@ let read_coqide_args argv = |"-coqtop" :: [] -> output_string stderr "Error: missing argument after -coqtop"; exit 1 |"-debug"::args -> - Minilib.debug := true; - Flags.debug := true; - Exninfo.record_backtrace true; + set_debug (); filter_coqtop coqtop project_files bindings_files ("-debug"::out) args + |"-xml-debug"::args -> + set_debug (); + Flags.xml_debug := true; + filter_coqtop coqtop project_files bindings_files ("-xml-debug"::out) args |"-coqtop-flags" :: flags :: args-> Coq.ideslave_coqtop_flags := Some flags; filter_coqtop coqtop project_files bindings_files out args diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml index e9ff1bbba1..6540fc6fca 100644 --- a/ide/coqide/coqide_ui.ml +++ b/ide/coqide/coqide_ui.ml @@ -89,6 +89,7 @@ let init () = \n <menuitem action='Unset diff' />\ \n <menuitem action='Set diff' />\ \n <menuitem action='Set removed diff' />\ +\n <menuitem action='Show Proof Diffs' />\ \n </menu>\ \n <menu action='Navigation'>\ \n <menuitem action='Forward' />\ diff --git a/ide/coqide/fake_ide.ml b/ide/coqide/fake_ide.ml index e1736a5fe0..034f5b4e2a 100644 --- a/ide/coqide/fake_ide.ml +++ b/ide/coqide/fake_ide.ml @@ -136,7 +136,7 @@ module Parser = struct (* {{{ *) match g with | Item (s,_) -> Printf.sprintf "%s" (clean s) | Opt g -> Printf.sprintf "[%s]" (print g) - | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs)) + | Alt gs -> Printf.sprintf "( %s )" (String.concat "\n| " (List.map print gs)) | Seq gs -> String.concat " " (List.map print gs) let rec print_toklist = function @@ -253,6 +253,9 @@ let eval_print l coq = after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> eval_call (query (0,(phrase,tip_id()))) coq + | [ Tok(_,"PDIFF"); Tok(_,id) ] -> + let to_id, _ = get_id id in + eval_call (proof_diff ("on",to_id)) coq | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> let to_id, _ = get_id id in eval_call (query (0,(phrase, to_id))) coq @@ -282,6 +285,7 @@ let grammar = ; Seq [Item (eat_rex "FAILADD"); Item eat_phrase] ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "PDIFF"); Item eat_id ] ; Seq [Item (eat_rex "WAIT")] ; Seq [Item (eat_rex "JOIN")] ; Seq [Item (eat_rex "GOALS")] @@ -295,12 +299,11 @@ let grammar = let read_command inc = Parser.parse grammar inc let usage () = - error (Printf.sprintf - "A fake coqide process talking to a coqtop -toploop coqidetop.\n\ - Usage: %s (file|-) [<coqtop>]\n\ - Input syntax is the following:\n%s\n" - (Filename.basename Sys.argv.(0)) - (Parser.print grammar)) + prerr_endline (Printf.sprintf "Usage: %s ( file | - ) [ \"<coqtop arguments>\" ]\n\ + Input syntax is:\n%s\n" + (Filename.basename Sys.argv.(0)) + (Parser.print grammar)); + exit 1 module Coqide = Spawn.Sync () @@ -308,14 +311,15 @@ let main = if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); - let def_args = ["--xml_format=Ppcmds"] in let idetop_name = System.get_toplevel_path "coqidetop" in - let coqtop_args, input_file = match Sys.argv with - | [| _; f |] -> Array.of_list def_args, f - | [| _; f; ct |] -> - let ct = Str.split (Str.regexp " ") ct in - Array.of_list (def_args @ ct), f + let input_file, args = match Sys.argv with + | [| _; f |] -> f, [] + | [| _; f; args |] -> + let args = Str.split (Str.regexp " ") args in + f, args | _ -> usage () in + let def_coqtop_args = ["--xml_format=Ppcmds"] in + let coqtop_args = Array.of_list(def_coqtop_args @ args) in let inc = if input_file = "-" then stdin else open_in input_file in prerr_endline ("Running: "^idetop_name^" "^ (String.concat " " (Array.to_list coqtop_args))); diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index ad21f663e4..297dc3a706 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -367,6 +367,17 @@ let export_option_state s = { Interface.opt_value = export_option_value s.Goptions.opt_value; } +exception NotSupported of string + +let proof_diff (diff_opt, sid) = + let diff_opt = Proof_diffs.string_to_diffs diff_opt in + let doc = get_doc () in + match Stm.get_proof ~doc sid with + | None -> CErrors.user_err (Pp.str "No proofs to diff.") + | Some proof -> + let old = Stm.get_prev_proof ~doc sid in + Proof_diffs.diff_proofs ~diff_opt ?old proof + let get_options () = let table = Goptions.get_tables () in let fold key state accu = (key, export_option_state state) :: accu in @@ -455,6 +466,7 @@ let eval_call c = Interface.hints = interruptible hints; Interface.status = interruptible status; Interface.search = interruptible search; + Interface.proof_diff = interruptible proof_diff; Interface.get_options = interruptible get_options; Interface.set_options = interruptible set_options; Interface.mkcases = interruptible idetop_make_cases; @@ -479,6 +491,8 @@ let print_xml = let m = Mutex.create () in fun oc xml -> Mutex.lock m; + if !Flags.xml_debug then + Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml); try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e @@ -507,7 +521,7 @@ let loop run_mode ~opts:_ state = set_doc state.doc; init_signal_handler (); catch_break := false; - let in_ch, out_ch = Spawned.get_channels () in + let in_ch, out_ch = Spawned.get_channels () in let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in let in_lb = Lexing.from_function (fun s len -> CThread.thread_friendly_read in_ch s ~off:0 ~len) in @@ -518,7 +532,8 @@ let loop run_mode ~opts:_ state = while not !quit do try let xml_query = Xml_parser.parse xml_ic in -(* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) + if !Flags.xml_debug then + pr_with_pid (Xml_printer.to_string_fmt xml_query); let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in let () = pr_debug_call q in let r = eval_call q in diff --git a/ide/coqide/protocol/interface.ml b/ide/coqide/protocol/interface.ml index 646012dcaa..86a81446e8 100644 --- a/ide/coqide/protocol/interface.ml +++ b/ide/coqide/protocol/interface.ml @@ -187,6 +187,10 @@ type status_rty = status type search_sty = search_flags type search_rty = string coq_object list +(** Diffs between the proof term at a given stateid and the previous one *) +type proof_diff_sty = string * Stateid.t +type proof_diff_rty = Pp.t + (** Retrieve the list of options of the current toplevel *) type get_options_sty = unit type get_options_rty = (option_name * option_state) list @@ -252,6 +256,7 @@ type handler = { stop_worker : stop_worker_sty -> stop_worker_rty; print_ast : print_ast_sty -> print_ast_rty; annotate : annotate_sty -> annotate_rty; + proof_diff : proof_diff_sty -> proof_diff_rty; handle_exn : handle_exn_sty -> handle_exn_rty; init : init_sty -> init_rty; quit : quit_sty -> quit_rty; diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml index 9e861baac6..6a33ff8abc 100644 --- a/ide/coqide/protocol/xmlprotocol.ml +++ b/ide/coqide/protocol/xmlprotocol.ml @@ -12,7 +12,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20170413" +let protocol_version = "20200911" type msg_format = Richpp of int | Ppcmds let msg_format = ref (Richpp 72) @@ -278,6 +278,7 @@ module ReifType : sig val state_id_t : state_id val_t val route_id_t : route_id val_t val search_cst_t : search_constraint val_t + val pp_t : Pp.t val_t val of_value_type : 'a val_t -> 'a -> xml val to_value_type : 'a val_t -> xml -> 'a @@ -314,6 +315,7 @@ end = struct | State_id : state_id val_t | Route_id : route_id val_t | Search_cst : search_constraint val_t + | Pp : Pp.t val_t type value_type = Value_type : 'a val_t -> value_type @@ -340,6 +342,7 @@ end = struct let state_id_t = State_id let route_id_t = Route_id let search_cst_t = Search_cst + let pp_t = Pp let of_value_type (ty : 'a val_t) : 'a -> xml = let rec convert : type a. a val_t -> a -> xml = function @@ -362,6 +365,7 @@ end = struct | State_id -> of_stateid | Route_id -> of_routeid | Search_cst -> of_search_cst + | Pp -> of_pp in convert ty @@ -386,6 +390,7 @@ end = struct | State_id -> to_stateid | Route_id -> to_routeid | Search_cst -> to_search_cst + | Pp -> to_pp in convert ty @@ -443,6 +448,8 @@ end = struct | In_Module s -> "In_Module " ^ String.concat "." s | Include_Blacklist -> "Include_Blacklist" + let pr_pp = Pp.string_of_ppcmds + let rec print : type a. a val_t -> a -> string = function | Unit -> pr_unit | Bool -> pr_bool @@ -463,6 +470,7 @@ end = struct | Union (t1,t2) -> (pr_union (print t1) (print t2)) | State_id -> pr_state_id | Route_id -> pr_int + | Pp -> pr_pp (* This is to break if a rename/refactoring makes the strings below outdated *) type 'a exists = bool @@ -489,6 +497,7 @@ end = struct Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2) | State_id -> assert(true : Stateid.t exists); "Stateid.t" | Route_id -> assert(true : route_id exists); "route_id" + | Pp -> assert(true : Pp.t exists); "Pp.t" let print_type = function Value_type ty -> print_val_t ty @@ -507,6 +516,8 @@ end = struct (pr_xml (of_pair of_bool of_int (false,3))); Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int))) (pr_xml (of_union of_bool of_int (Inl false))); + Printf.printf "%s:\n\n%s\n\n" (print_val_t Pp) + (pr_xml (of_pp Pp.(hv 3 (str "foo" ++ spc () ++ str "bar") ))); print_endline ("All other types are records represented by a node named like the OCaml\n"^ "type which contains a flattened n-tuple. We provide one example.\n"); Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) @@ -538,6 +549,7 @@ let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t let stop_worker_sty_t : stop_worker_sty val_t = string_t let print_ast_sty_t : print_ast_sty val_t = state_id_t let annotate_sty_t : annotate_sty val_t = string_t +let proof_diff_sty_t : proof_diff_sty val_t = pair_t string_t state_id_t let add_rty_t : add_rty val_t = pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) @@ -563,6 +575,7 @@ let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string let stop_worker_rty_t : stop_worker_rty val_t = unit_t let print_ast_rty_t : print_ast_rty val_t = xml_t let annotate_rty_t : annotate_rty val_t = xml_t +let proof_diff_rty_t : proof_diff_rty val_t = pp_t let ($) x = erase x let calls = [| @@ -585,6 +598,7 @@ let calls = [| "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t; "PrintAst", ($)print_ast_sty_t, ($)print_ast_rty_t; "Annotate", ($)annotate_sty_t, ($)annotate_rty_t; + "PDiff", ($)proof_diff_sty_t, ($)proof_diff_rty_t; |] type 'a call = @@ -609,7 +623,9 @@ type 'a call = | Interp : interp_sty -> interp_rty call | PrintAst : print_ast_sty -> print_ast_rty call | Annotate : annotate_sty -> annotate_rty call + | PDiff : proof_diff_sty -> proof_diff_rty call +(* the order of the entries must match the order in "calls" above *) let id_of_call : type a. a call -> int = function | Add _ -> 0 | Edit_at _ -> 1 @@ -630,6 +646,7 @@ let id_of_call : type a. a call -> int = function | StopWorker _ -> 16 | PrintAst _ -> 17 | Annotate _ -> 18 + | PDiff _ -> 19 let str_of_call c = pi1 calls.(id_of_call c) @@ -652,8 +669,9 @@ let init x : init_rty call = Init x let wait x : wait_rty call = Wait x let interp x : interp_rty call = Interp x let stop_worker x : stop_worker_rty call = StopWorker x -let print_ast x : print_ast_rty call = PrintAst x -let annotate x : annotate_rty call = Annotate x +let print_ast x : print_ast_rty call = PrintAst x +let annotate x : annotate_rty call = Annotate x +let proof_diff x : proof_diff_rty call = PDiff x let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> let mkGood : type a. a -> a value = fun x -> Good x in @@ -678,6 +696,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | StopWorker x -> mkGood (handler.stop_worker x) | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) + | PDiff x -> mkGood (handler.proof_diff x) with any -> let any = Exninfo.capture any in Fail (handler.handle_exn any) @@ -703,6 +722,7 @@ let of_answer : type a. a call -> a value -> xml = function | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) | Annotate _ -> of_value (of_value_type annotate_rty_t ) + | PDiff _ -> of_value (of_value_type proof_diff_rty_t ) let of_answer msg_fmt = msg_format := msg_fmt; of_answer @@ -727,6 +747,7 @@ let to_answer : type a. a call -> xml -> a value = function | StopWorker _ -> to_value (to_value_type stop_worker_rty_t) | PrintAst _ -> to_value (to_value_type print_ast_rty_t ) | Annotate _ -> to_value (to_value_type annotate_rty_t ) + | PDiff _ -> to_value (to_value_type proof_diff_rty_t ) let of_call : type a. a call -> xml = fun q -> let mkCall x = constructor "call" (str_of_call q) [x] in @@ -750,6 +771,7 @@ let of_call : type a. a call -> xml = fun q -> | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x) | PrintAst x -> mkCall (of_value_type print_ast_sty_t x) | Annotate x -> mkCall (of_value_type annotate_sty_t x) + | PDiff x -> mkCall (of_value_type proof_diff_sty_t x) let to_call : xml -> unknown_call = do_match "call" (fun s a -> @@ -774,6 +796,7 @@ let to_call : xml -> unknown_call = | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a)) | "PrintAst" -> Unknown (PrintAst (mkCallArg print_ast_sty_t a)) | "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a)) + | "PDiff" -> Unknown (PDiff (mkCallArg proof_diff_sty_t a)) | x -> raise (Marshal_error("call",PCData x))) (** Debug printing *) @@ -805,6 +828,7 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value | PrintAst _ -> pr_value_gen (print print_ast_rty_t ) value | Annotate _ -> pr_value_gen (print annotate_rty_t ) value + | PDiff _ -> pr_value_gen (print proof_diff_rty_t ) value let pr_call : type a. a call -> string = fun call -> let return what x = str_of_call call ^ " " ^ print what x in match call with @@ -827,6 +851,7 @@ let pr_call : type a. a call -> string = fun call -> | StopWorker x -> return stop_worker_sty_t x | PrintAst x -> return print_ast_sty_t x | Annotate x -> return annotate_sty_t x + | PDiff x -> return proof_diff_sty_t x let document to_string_fmt = Printf.printf "=== Available calls ===\n\n"; diff --git a/ide/coqide/protocol/xmlprotocol.mli b/ide/coqide/protocol/xmlprotocol.mli index 44584d44d7..4dc05c18a9 100644 --- a/ide/coqide/protocol/xmlprotocol.mli +++ b/ide/coqide/protocol/xmlprotocol.mli @@ -37,6 +37,7 @@ val wait : wait_sty -> wait_rty call val interp : interp_sty -> interp_rty call val print_ast : print_ast_sty -> print_ast_rty call val annotate : annotate_sty -> annotate_rty call +val proof_diff : proof_diff_sty -> proof_diff_rty call val abstract_eval_call : handler -> 'a call -> 'a value diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index c98e05370e..d14d156ffc 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -108,7 +108,7 @@ and constr_expr_r = * constr_expr * constr_expr | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Pattern.patvar - | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list + | CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index ce8e7d3c2c..7075d082ee 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -156,7 +156,7 @@ let rec constr_expr_eq e1 e2 = | CPatVar i1, CPatVar i2 -> Id.equal i1 i2 | CEvar (id1, c1), CEvar (id2, c2) -> - Id.equal id1 id2 && List.equal instance_eq c1 c2 + Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> Glob_ops.glob_sort_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> @@ -235,7 +235,7 @@ and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) = List.equal (List.equal local_binder_eq) bl1 bl2 and instance_eq (x1,c1) (x2,c2) = - Id.equal x1 x2 && constr_expr_eq c1 c2 + Id.equal x1.CAst.v x2.CAst.v && constr_expr_eq c1 c2 and cast_expr_eq c1 c2 = match c1, c2 with | CastConv t1, CastConv t2 diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 43fef8685d..e5a60769e8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -551,7 +551,7 @@ and extern_notation_pattern allscopes vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try - if is_inactive_rule keyrule then raise No_match; + if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match; let loc = t.loc in match DAst.get t with | PatCstr (cstr,args,na) -> @@ -568,7 +568,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try - if is_inactive_rule keyrule then raise No_match; + if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match; apply_notation_to_pattern (GlobRef.IndRef ind) (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with @@ -978,7 +978,7 @@ let rec extern inctx ?impargs scopes vars r = if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else (match kind with | Evar_kinds.SecondOrderPatVar n -> CPatVar n - | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) + | Evar_kinds.FirstOrderPatVar n -> CEvar (CAst.make n,[])) | GApp (f,args) -> (match DAst.get f with @@ -1238,7 +1238,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in try - if is_inactive_rule keyrule then raise No_match; + if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match; let f,args = match DAst.get t with | GApp (f,args) -> f,args @@ -1391,7 +1391,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | None -> Id.of_string "__" | Some id -> id in - GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l) + GEvar (CAst.make id,List.map (fun (id,c) -> (CAst.make id, glob_of_pat avoid env sigma c)) l) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 48fb4a4a5d..959b61a3d7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2188,7 +2188,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GPatVar (Evar_kinds.SecondOrderPatVar n) | CEvar (n, []) when pattern_mode -> DAst.make ?loc @@ - GPatVar (Evar_kinds.FirstOrderPatVar n) + GPatVar (Evar_kinds.FirstOrderPatVar n.CAst.v) (* end *) (* Parsing existential variables *) | CEvar (n, l) -> diff --git a/interp/notation.ml b/interp/notation.ml index 7e90e15b72..d57c4f3abf 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -58,6 +58,31 @@ let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2 let notation_eq (from1,ntn1) (from2,ntn2) = notation_entry_eq from1 from2 && String.equal ntn1 ntn2 +let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 + +let notation_binder_source_eq s1 s2 = match s1, s2 with +| NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 +| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 +| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false + +let ntpe_eq t1 t2 = match t1, t2 with +| NtnTypeConstr, NtnTypeConstr -> true +| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2 +| NtnTypeConstrList, NtnTypeConstrList -> true +| NtnTypeBinderList, NtnTypeBinderList -> true +| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false + +let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = + notation_entry_level_eq entry1 entry2 && + pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && + ntpe_eq tp1 tp2 + +let interpretation_eq (vars1, t1 as x1) (vars2, t2 as x2) = + x1 == x2 || + List.equal var_attributes_eq vars1 vars2 && + Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2 + let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntry -> mt () | InCustomEntry s -> str " in custom " ++ str s module NotationOrd = @@ -90,8 +115,21 @@ type notation_data = { not_deprecation : Deprecation.t option; } +type activation = bool + +type extra_printing_notation_data = + (activation * notation_data) list + +type parsing_notation_data = + | NoParsingData + | OnlyParsingData of activation * notation_data + | ParsingAndPrintingData of + activation (* for parsing*) * + activation (* for printing *) * + notation_data (* common data for both *) + type scope = { - notations: notation_data NotationMap.t; + notations: (parsing_notation_data * extra_printing_notation_data) NotationMap.t; delimiters: delimiters option } @@ -300,10 +338,19 @@ type notation_applicative_status = type notation_rule = interp_rule * interpretation * notation_applicative_status +let notation_rule_eq (rule1,pat1,s1 as x1) (rule2,pat2,s2 as x2) = + x1 == x2 || (rule1 = rule2 && interpretation_eq pat1 pat2 && s1 = s2) + let keymap_add key interp map = let old = try KeyMap.find key map with Not_found -> [] in + (* In case of re-import, no need to keep the previous copy *) + let old = try List.remove_first (notation_rule_eq interp) old with Not_found -> old in KeyMap.add key (interp :: old) map +let keymap_remove key interp map = + let old = try KeyMap.find key map with Not_found -> [] in + KeyMap.add key (List.remove_first (notation_rule_eq interp) old) map + let keymap_find key map = try KeyMap.find key map with Not_found -> [] @@ -1225,40 +1272,90 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* The mapping between notations and their interpretation *) +let pr_optional_scope = function + | LastLonelyNotation -> mt () + | NotationInScope scope -> spc () ++ strbrk "in scope" ++ spc () ++ str scope + let warn_notation_overridden = CWarnings.create ~name:"notation-overridden" ~category:"parsing" - (fun (ntn,which_scope) -> + (fun (scope,ntn) -> str "Notation" ++ spc () ++ pr_notation ntn ++ spc () - ++ strbrk "was already used" ++ which_scope ++ str ".") + ++ strbrk "was already used" ++ pr_optional_scope scope ++ str ".") -let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation = - let scope = match scopt with Some s -> s | None -> default_scope in - let sc = find_scope scope in - if not onlyprint then begin - let () = - if NotationMap.mem ntn sc.notations then - let which_scope = match scopt with - | None -> mt () - | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in - warn_notation_overridden (ntn,which_scope) - in - let notdata = { - not_interp = pat; - not_location = df; - not_deprecation = deprecation; - } in - let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in - scope_map := String.Map.add scope sc !scope_map - end; - begin match scopt with - | None -> scope_stack := LonelyNotationItem ntn :: !scope_stack - | Some _ -> () - end +let warn_deprecation_overridden = + CWarnings.create ~name:"notation-overridden" ~category:"parsing" + (fun ((scope,ntn),old,now) -> + match old, now with + | None, None -> assert false + | None, Some _ -> + (str "Notation" ++ spc () ++ pr_notation ntn ++ pr_optional_scope scope ++ spc () + ++ strbrk "is now marked as deprecated" ++ str ".") + | Some _, None -> + (str "Cancelling previous deprecation of notation" ++ spc () ++ + pr_notation ntn ++ pr_optional_scope scope ++ str ".") + | Some _, Some _ -> + (str "Amending deprecation of notation" ++ spc () ++ + pr_notation ntn ++ pr_optional_scope scope ++ str ".")) + +type notation_use = + | OnlyPrinting + | OnlyParsing + | ParsingAndPrinting + +let warn_override_if_needed (scopt,ntn) overridden data old_data = + if overridden then warn_notation_overridden (scopt,ntn) + else + if data.not_deprecation <> old_data.not_deprecation then + warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation) + +let check_parsing_override (scopt,ntn) data = function + | OnlyParsingData (_,old_data) -> + let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in + warn_override_if_needed (scopt,ntn) overridden data old_data; + None, not overridden + | ParsingAndPrintingData (_,on_printing,old_data) -> + let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in + warn_override_if_needed (scopt,ntn) overridden data old_data; + (if on_printing then Some old_data.not_interp else None), not overridden + | NoParsingData -> None, false + +let check_printing_override (scopt,ntn) data parsingdata printingdata = + let parsing_update = match parsingdata with + | OnlyParsingData _ | NoParsingData -> parsingdata + | ParsingAndPrintingData (_,on_printing,old_data) -> + let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in + warn_override_if_needed (scopt,ntn) overridden data old_data; + if overridden then NoParsingData else parsingdata in + let exists = List.exists (fun (on_printing,old_data) -> + let exists = interpretation_eq data.not_interp old_data.not_interp in + if exists && data.not_deprecation <> old_data.not_deprecation then + warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation); + exists) printingdata in + parsing_update, exists + +let remove_uninterpretation rule (metas,c as pat) = + let (key,n) = notation_constr_key c in + notations_key_table := keymap_remove key (rule,pat,n) !notations_key_table let declare_uninterpretation rule (metas,c as pat) = let (key,n) = notation_constr_key c in notations_key_table := keymap_add key (rule,pat,n) !notations_key_table +let update_notation_data (scopt,ntn) use data table = + let (parsingdata,printingdata) = + try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in + match use with + | OnlyParsing -> + let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in + NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists + | ParsingAndPrinting -> + let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in + NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists + | OnlyPrinting -> + let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in + let printingdata = if exists then printingdata else (true,data) :: printingdata in + NotationMap.add ntn (parsingdata, printingdata) table, None, exists + let rec find_interpretation ntn find = function | [] -> raise Not_found | OpenScopeItem scope :: scopes -> @@ -1273,7 +1370,9 @@ let rec find_interpretation ntn find = function find_interpretation ntn find scopes let find_notation ntn sc = - NotationMap.find ntn (find_scope sc).notations + match fst (NotationMap.find ntn (find_scope sc).notations) with + | OnlyParsingData (true,data) | ParsingAndPrintingData (true,_,data) -> data + | _ -> raise Not_found let notation_of_prim_token = function | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n @@ -1358,10 +1457,37 @@ let uninterp_cases_pattern_notations c = let uninterp_ind_pattern_notations ind = keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table +let has_active_parsing_rule_in_scope ntn sc = + try + match NotationMap.find ntn (String.Map.find sc !scope_map).notations with + | OnlyParsingData (active,_),_ | ParsingAndPrintingData (active,_,_),_ -> active + | _ -> false + with Not_found -> false + +let is_printing_active_in_scope (scope,ntn) pat = + let sc = match scope with NotationInScope sc -> sc | LastLonelyNotation -> default_scope in + let is_active extra = + try + let (_,(active,_)) = List.extract_first (fun (active,d) -> interpretation_eq d.not_interp pat) extra in + active + with Not_found -> false in + try + match NotationMap.find ntn (String.Map.find sc !scope_map).notations with + | ParsingAndPrintingData (_,active,d), extra -> + if interpretation_eq d.not_interp pat then active + else is_active extra + | _, extra -> is_active extra + with Not_found -> false + +let is_printing_inactive_rule rule pat = + match rule with + | NotationRule (scope,ntn) -> + not (is_printing_active_in_scope (scope,ntn) pat) + | SynDefRule kn -> + try let _ = Nametab.path_of_syndef kn in false with Not_found -> true + let availability_of_notation (ntn_scope,ntn) scopes = - let f scope = - NotationMap.mem ntn (String.Map.find scope !scope_map).notations in - find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes) + find_without_delimiters (has_active_parsing_rule_in_scope ntn) (ntn_scope,Some ntn) (make_current_scopes scopes) (* We support coercions from a custom entry at some level to an entry at some level (possibly the same), and from and to the constr entry. E.g.: @@ -1484,6 +1610,49 @@ let entry_has_ident = function | InCustomEntryLevel (s,n) -> try String.Map.find s !entry_has_ident_map <= n with Not_found -> false +type entry_coercion_kind = + | IsEntryCoercion of notation_entry_level + | IsEntryGlobal of string * int + | IsEntryIdent of string * int + +let declare_notation (scopt,ntn) pat df ~use coe deprecation = + (* Register the interpretation *) + let scope = match scopt with NotationInScope s -> s | LastLonelyNotation -> default_scope in + let sc = find_scope scope in + let notdata = { + not_interp = pat; + not_location = df; + not_deprecation = deprecation; + } in + let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in + if not exists then + let sc = { sc with notations = notation_update } in + scope_map := String.Map.add scope sc !scope_map; + (* Update the uninterpretation cache *) + begin match printing_update with + | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) pat + | None -> () + end; + if not exists && use <> OnlyParsing then declare_uninterpretation (NotationRule (scopt,ntn)) pat; + (* Register visibility of lonely notations *) + if not exists then begin match scopt with + | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack + | NotationInScope _ -> () + end; + (* Declare a possible coercion *) + if not exists then begin match coe with + | Some (IsEntryCoercion entry) -> + let (_,level,_) = level_of_notation ntn in + let level = match fst ntn with + | InConstrEntry -> None + | InCustomEntry _ -> Some level + in + declare_entry_coercion (scopt,ntn) level entry + | Some (IsEntryGlobal (entry,n)) -> declare_custom_entry_has_global entry n + | Some (IsEntryIdent (entry,n)) -> declare_custom_entry_has_ident entry n + | None -> () + end + let availability_of_prim_token n printer_scope local_scopes = let f scope = try @@ -1561,38 +1730,6 @@ let uninterp_prim_token_cases_pattern c local_scopes = (* Miscellaneous *) -let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 - -let notation_binder_source_eq s1 s2 = match s1, s2 with -| NtnParsedAsIdent, NtnParsedAsIdent -> true -| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 -| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 -| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false - -let ntpe_eq t1 t2 = match t1, t2 with -| NtnTypeConstr, NtnTypeConstr -> true -| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2 -| NtnTypeConstrList, NtnTypeConstrList -> true -| NtnTypeBinderList, NtnTypeBinderList -> true -| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false - -let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = - notation_entry_level_eq entry1 entry2 && - pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && - ntpe_eq tp1 tp2 - -let interpretation_eq (vars1, t1) (vars2, t2) = - List.equal var_attributes_eq vars1 vars2 && - Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2 - -let exists_notation_in_scope scopt ntn onlyprint r = - let scope = match scopt with Some s -> s | None -> default_scope in - try - let sc = String.Map.find scope !scope_map in - let n = NotationMap.find ntn sc.notations in - interpretation_eq n.not_interp r - with Not_found -> false - let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) @@ -1846,38 +1983,63 @@ let pr_scope_classes sc = | _ :: ll -> let opt_s = match ll with [] -> mt () | _ -> str "es" in hov 0 (str "Bound to class" ++ opt_s ++ - spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl() + spc() ++ prlist_with_sep spc pr_scope_class l) let pr_notation_info prglob ntn c = - str "\"" ++ str ntn ++ str "\" := " ++ + str "\"" ++ str ntn ++ str "\" :=" ++ brk (1,2) ++ prglob (Notation_ops.glob_constr_of_notation_constr c) -let pr_named_scope prglob scope sc = +let pr_notation_status on_parsing on_printing = + let deactivated b = if b then [] else ["deactivated"] in + let l = match on_parsing, on_printing with + | Some on, None -> "only parsing" :: deactivated on + | None, Some on -> "only printing" :: deactivated on + | Some false, Some false -> ["deactivated"] + | Some true, Some false -> ["deactivated for printing"] + | Some false, Some true -> ["deactivated for parsing"] + | Some true, Some true -> [] + | None, None -> assert false in + match l with + | [] -> mt () + | l -> str "(" ++ prlist_with_sep pr_comma str l ++ str ")" + +let pr_non_empty spc pp = + if pp = mt () then mt () else spc ++ pp + +let pr_notation_data prglob (on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) }) = + hov 0 (pr_notation_info prglob df r ++ pr_non_empty (brk(1,2)) (pr_notation_status on_parsing on_printing)) + +let extract_notation_data (main,extra) = + let main = match main with + | NoParsingData -> [] + | ParsingAndPrintingData (on_parsing, on_printing, d) -> + [Some on_parsing, Some on_printing, d] + | OnlyParsingData (on_parsing, d) -> + [Some on_parsing, None, d] in + let extra = List.map (fun (on_printing, d) -> (None, Some on_printing, d)) extra in + main @ extra + +let pr_named_scope prglob (scope,sc) = (if String.equal scope default_scope then match NotationMap.cardinal sc.notations with | 0 -> str "No lonely notation" | n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s") else str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters) - ++ fnl () - ++ pr_scope_classes scope - ++ NotationMap.fold - (fun ntn { not_interp = (_, r); not_location = (_, df) } strm -> - pr_notation_info prglob df r ++ fnl () ++ strm) - sc.notations (mt ()) + ++ pr_non_empty (fnl ()) (pr_scope_classes scope) + ++ prlist (fun a -> fnl () ++ pr_notation_data prglob a) + (NotationMap.fold (fun ntn data l -> extract_notation_data data @ l) sc.notations []) -let pr_scope prglob scope = pr_named_scope prglob scope (find_scope scope) +let pr_scope prglob scope = pr_named_scope prglob (scope, find_scope scope) let pr_scopes prglob = - String.Map.fold - (fun scope sc strm -> pr_named_scope prglob scope sc ++ fnl () ++ strm) - !scope_map (mt ()) + let l = String.Map.bindings !scope_map in + prlist_with_sep (fun () -> fnl () ++ fnl ()) (pr_named_scope prglob) l let rec find_default ntn = function | [] -> None | OpenScopeItem scope :: scopes -> - if NotationMap.mem ntn (find_scope scope).notations then - Some scope + if has_active_parsing_rule_in_scope ntn scope then Some scope else find_default ntn scopes | LonelyNotationItem ntn' :: scopes -> if notation_eq ntn ntn' then Some default_scope @@ -1885,12 +2047,12 @@ let rec find_default ntn = function let factorize_entries = function | [] -> [] - | (ntn,c)::l -> + | (ntn,sc',c)::l -> let (ntn,l_of_ntn,rest) = List.fold_left - (fun (a',l,rest) (a,c) -> - if notation_eq a a' then (a',c::l,rest) else (a,[c],(a',l)::rest)) - (ntn,[c],[]) l in + (fun (a',l,rest) (a,sc,c) -> + if notation_eq a a' then (a',(sc,c)::l,rest) else (a,[sc,c],(a',l)::rest)) + (ntn,[sc',c],[]) l in (ntn,l_of_ntn)::rest type symbol_token = WhiteSpace of int | String of string @@ -1961,16 +2123,18 @@ let browse_notation strict ntn map = let l = String.Map.fold (fun scope_name sc -> - NotationMap.fold (fun ntn { not_interp = (_, r); not_location = df } l -> - if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations) + NotationMap.fold (fun ntn data l -> + if List.exists (find ntn) ntns + then List.map (fun d -> (ntn,scope_name,d)) (extract_notation_data data) @ l + else l) sc.notations) map [] in - List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l + List.sort (fun x y -> String.compare (snd (pi1 x)) (snd (pi1 y))) l -let global_reference_of_notation ~head test (ntn,(sc,c,_)) = +let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c)})) = match c with - | NRef ref when test ref -> Some (ntn,sc,ref) + | NRef ref when test ref -> Some (on_parsing,on_printing,ntn,sc,ref) | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref -> - Some (ntn,sc,ref) + Some (on_parsing,on_printing,ntn,sc,ref) | _ -> None let error_ambiguous_notation ?loc _ntn = @@ -1990,17 +2154,17 @@ let interp_notation_as_global_reference ?loc ~head test ntn sc = let ntns = browse_notation true ntn scopes in let refs = List.map (global_reference_of_notation ~head test) ntns in match Option.List.flatten refs with - | [_,_,ref] -> ref + | [Some true,_ (* why not if the only one? *),_,_,ref] -> ref | [] -> error_notation_not_reference ?loc ntn | refs -> - let f (ntn,sc,ref) = + let f (on_parsing,_,ntn,sc,ref) = let def = find_default ntn !scope_stack in match def with | None -> false - | Some sc' -> String.equal sc sc' + | Some sc' -> on_parsing = Some true && String.equal sc sc' in match List.filter f refs with - | [_,_,ref] -> ref + | [_,_,_,_,ref] -> ref | [] -> error_notation_not_reference ?loc ntn | _ -> error_ambiguous_notation ?loc ntn @@ -2010,24 +2174,25 @@ let locate_notation prglob ntn scope = match ntns with | [] -> str "Unknown notation" | _ -> - str "Notation" ++ fnl () ++ prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in prlist_with_sep fnl - (fun (sc,r,(_,df)) -> + (fun (sc,(on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) })) -> hov 0 ( + str "Notation" ++ brk (1,2) ++ pr_notation_info prglob df r ++ (if String.equal sc default_scope then mt () - else (spc () ++ str ": " ++ str sc)) ++ + else (brk (1,2) ++ str ": " ++ str sc)) ++ (if Option.equal String.equal (Some sc) scope - then spc () ++ str "(default interpretation)" else mt ()))) + then brk (1,2) ++ str "(default interpretation)" else mt ()) ++ + pr_non_empty (brk (1,2)) (pr_notation_status on_parsing on_printing))) l) ntns let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); NotationMap.fold - (fun ntn { not_interp = (_, r); not_location = (_, df) } (l,known as acc) -> - if List.mem_f notation_eq ntn known then acc else ((df,r)::l,ntn::known)) + (fun ntn d (l,known as acc) -> + if List.mem_f notation_eq ntn known then acc else (extract_notation_data d @ l,ntn::known)) sc.notations ([],known) let collect_notations stack = @@ -2043,13 +2208,13 @@ let collect_notations stack = if List.mem_f notation_eq ntn knownntn then (all,knownntn) else try - let { not_interp = (_, r); not_location = (_, df) } = - NotationMap.find ntn (find_scope default_scope).notations in + let datas = extract_notation_data + (NotationMap.find ntn (find_scope default_scope).notations) in let all' = match all with | (s,lonelyntn)::rest when String.equal s default_scope -> - (s,(df,r)::lonelyntn)::rest + (s,datas@lonelyntn)::rest | _ -> - (default_scope,[df,r])::all in + (default_scope,datas)::all in (all',ntn::knownntn) with Not_found -> (* e.g. if only printing *) (all,knownntn)) ([],[]) stack) @@ -2057,7 +2222,7 @@ let collect_notations stack = let pr_visible_in_scope prglob (scope,ntns) = let strm = List.fold_right - (fun (df,r) strm -> pr_notation_info prglob df r ++ fnl () ++ strm) + (fun d strm -> pr_notation_data prglob d ++ fnl () ++ strm) ntns (mt ()) in (if String.equal scope default_scope then str "Lonely notation" ++ (match ntns with [_] -> mt () | _ -> str "s") @@ -2066,9 +2231,7 @@ let pr_visible_in_scope prglob (scope,ntns) = ++ fnl () ++ strm let pr_scope_stack prglob stack = - List.fold_left - (fun strm scntns -> strm ++ pr_visible_in_scope prglob scntns ++ fnl ()) - (mt ()) (collect_notations stack) + prlist_with_sep fnl (pr_visible_in_scope prglob) (collect_notations stack) let pr_visibility prglob = function | Some scope -> pr_scope_stack prglob (push_scope scope !scope_stack) diff --git a/interp/notation.mli b/interp/notation.mli index 948831b317..d744ff41d9 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -229,12 +229,24 @@ type interp_rule = | NotationRule of specific_notation | SynDefRule of KerName.t -val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> onlyprint:bool -> - Deprecation.t option -> unit +type notation_use = + | OnlyPrinting + | OnlyParsing + | ParsingAndPrinting val declare_uninterpretation : interp_rule -> interpretation -> unit +type entry_coercion_kind = + | IsEntryCoercion of notation_entry_level + | IsEntryGlobal of string * int + | IsEntryIdent of string * int + +val declare_notation : notation_with_optional_scope * notation -> + interpretation -> notation_location -> use:notation_use -> + entry_coercion_kind option -> + Deprecation.t option -> unit + + (** Return the interpretation bound to a notation *) val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) @@ -257,16 +269,14 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list val availability_of_notation : specific_notation -> subscopes -> (scope_name option * delimiters option) option +val is_printing_inactive_rule : interp_rule -> interpretation -> bool + (** {6 Miscellaneous} *) (** If head is true, also allows applied global references. *) val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) -> notation_key -> delimiters option -> GlobRef.t -(** Checks for already existing notations *) -val exists_notation_in_scope : scope_name option -> notation -> - bool -> interpretation -> bool - (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 22531b0016..354809252e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -27,7 +27,9 @@ open Notation_term (* helper for NVar, NVar case in eq_notation_constr *) let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None -let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with +let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = +(vars1 == vars2 && t1 == t2) || +match t1, t2 with | NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2 | NVar id1, NVar id2 -> ( match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 343f85be03..70be55f843 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -40,8 +40,10 @@ let wit_int_or_var = let wit_ident = make0 "ident" -let wit_var = - make0 ~dyn:(val_tag (topwit wit_ident)) "var" +let wit_hyp = + make0 ~dyn:(val_tag (topwit wit_ident)) "hyp" + +let wit_var = wit_hyp let wit_ref = make0 "ref" diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 3ae8b7d73f..bd34af5543 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -37,7 +37,10 @@ val wit_int_or_var : (int or_var, int or_var, int) genarg_type val wit_ident : Id.t uniform_genarg_type +val wit_hyp : (lident, lident, Id.t) genarg_type + val wit_var : (lident, lident, Id.t) genarg_type +[@@ocaml.deprecated "Use Stdarg.wit_hyp"] val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type diff --git a/kernel/dune b/kernel/dune index ce6fdc03df..bd663974da 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_31 uint63_63)) + (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63)) (libraries lib byterun dynlink)) (executable @@ -19,6 +19,11 @@ (deps (:gen-file uint63_%{ocaml-config:int_size}.ml)) (action (copy# %{gen-file} %{targets}))) +(rule + (targets float64.ml) + (deps (:gen-file float64_%{ocaml-config:int_size}.ml)) + (action (copy# %{gen-file} %{targets}))) + (documentation (package coq)) diff --git a/kernel/environ.ml b/kernel/environ.ml index e497b7904a..dec9e1deb8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -274,6 +274,11 @@ let is_impredicative_sort env = function let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u) +let is_impredicative_family env = function + | Sorts.InSProp | Sorts.InProp -> true + | Sorts.InSet -> is_impredicative_set env + | Sorts.InType -> false + let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded diff --git a/kernel/environ.mli b/kernel/environ.mli index 47a118aa42..f443ba38e1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -122,6 +122,7 @@ val indices_matter : env -> bool val is_impredicative_sort : env -> Sorts.t -> bool val is_impredicative_univ : env -> Univ.Universe.t -> bool +val is_impredicative_family : env -> Sorts.family -> bool (** is the local context empty *) val empty_context : env -> bool diff --git a/kernel/float64_31.ml b/kernel/float64_31.ml new file mode 100644 index 0000000000..09b28e6cf0 --- /dev/null +++ b/kernel/float64_31.ml @@ -0,0 +1,35 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +include Float64_common + +external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul" +[@@unboxed] [@@noalloc] + +external add : float -> float -> float = "coq_fadd_byte" "coq_fadd" +[@@unboxed] [@@noalloc] + +external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub" +[@@unboxed] [@@noalloc] + +external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv" +[@@unboxed] [@@noalloc] + +external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt" +[@@unboxed] [@@noalloc] + +(*** Test at runtime that no harmful double rounding seems to + be performed with an intermediate 80 bits representation (x87). *) +let () = + let b = ldexp 1. 53 in + let s = add 1. (ldexp 1. (-52)) in + if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then + failwith "Detected non IEEE-754 compliant architecture (or wrong \ + rounding mode). Use of Float is thus unsafe." diff --git a/kernel/float64_63.ml b/kernel/float64_63.ml new file mode 100644 index 0000000000..0025531cb1 --- /dev/null +++ b/kernel/float64_63.ml @@ -0,0 +1,35 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +include Float64_common + +let mul (x : float) (y : float) : float = x *. y +[@@ocaml.inline always] + +let add (x : float) (y : float) : float = x +. y +[@@ocaml.inline always] + +let sub (x : float) (y : float) : float = x -. y +[@@ocaml.inline always] + +let div (x : float) (y : float) : float = x /. y +[@@ocaml.inline always] + +let sqrt (x : float) : float = sqrt x +[@@ocaml.inline always] + +(*** Test at runtime that no harmful double rounding seems to + be performed with an intermediate 80 bits representation (x87). *) +let () = + let b = ldexp 1. 53 in + let s = add 1. (ldexp 1. (-52)) in + if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then + failwith "Detected non IEEE-754 compliant architecture (or wrong \ + rounding mode). Use of Float is thus unsafe." diff --git a/kernel/float64.ml b/kernel/float64_common.ml index 76005a3dc6..2991a20b49 100644 --- a/kernel/float64.ml +++ b/kernel/float64_common.ml @@ -88,21 +88,6 @@ let classify x = | FP_nan -> NaN [@@ocaml.inline always] -external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul" -[@@unboxed] [@@noalloc] - -external add : float -> float -> float = "coq_fadd_byte" "coq_fadd" -[@@unboxed] [@@noalloc] - -external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub" -[@@unboxed] [@@noalloc] - -external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv" -[@@unboxed] [@@noalloc] - -external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt" -[@@unboxed] [@@noalloc] - let of_int63 x = Uint63.to_float x [@@ocaml.inline always] @@ -157,12 +142,3 @@ let total_compare f1 f2 = let is_float64 t = Obj.tag t = Obj.double_tag [@@ocaml.inline always] - -(*** Test at runtime that no harmful double rounding seems to - be performed with an intermediate 80 bits representation (x87). *) -let () = - let b = ldexp 1. 53 in - let s = add 1. (ldexp 1. (-52)) in - if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then - failwith "Detected non IEEE-754 compliant architecture (or wrong \ - rounding mode). Use of Float is thus unsafe." diff --git a/kernel/float64_common.mli b/kernel/float64_common.mli new file mode 100644 index 0000000000..4fb1c114a5 --- /dev/null +++ b/kernel/float64_common.mli @@ -0,0 +1,95 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** [t] is currently implemented by OCaml's [float] type. + +Beware: NaNs have a sign and a payload, while they should be +indistinguishable from Coq's perspective. *) +type t = float + +(** Test functions for special values to avoid calling [classify] *) +val is_nan : t -> bool +val is_infinity : t -> bool +val is_neg_infinity : t -> bool + +val of_string : string -> t + +(** Print a float exactly as an hexadecimal value (exact decimal + * printing would be possible but sometimes requires more than 700 + * digits). *) +val to_hex_string : t -> string + +(** Print a float as a decimal value. The printing is not exact (the + * real value printed is not always the given floating-point value), + * however printing is precise enough that forall float [f], + * [of_string (to_decimal_string f) = f]. *) +val to_string : t -> string + +val compile : t -> string + +val of_float : float -> t + +(** Return [true] for "-", [false] for "+". *) +val sign : t -> bool + +val opp : t -> t +val abs : t -> t + +type float_comparison = FEq | FLt | FGt | FNotComparable + +val eq : t -> t -> bool + +val lt : t -> t -> bool + +val le : t -> t -> bool + +(** The IEEE 754 float comparison. + * NotComparable is returned if there is a NaN in the arguments *) +val compare : t -> t -> float_comparison +[@@ocaml.inline always] + +type float_class = + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN + +val classify : t -> float_class +[@@ocaml.inline always] + +(** Link with integers *) +val of_int63 : Uint63.t -> t +[@@ocaml.inline always] + +val normfr_mantissa : t -> Uint63.t +[@@ocaml.inline always] + +(** Shifted exponent extraction *) +val eshift : int + +val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *) +[@@ocaml.inline always] + +val ldshiftexp : t -> Uint63.t -> t +[@@ocaml.inline always] + +val next_up : t -> t + +val next_down : t -> t + +(** Return true if two floats are equal. + * All NaN values are considered equal. *) +val equal : t -> t -> bool +[@@ocaml.inline always] + +val hash : t -> int + +(** Total order relation over float values. Behaves like [Pervasives.compare].*) +val total_compare : t -> t -> int + +val is_float64 : Obj.t -> bool +[@@ocaml.inline always] diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index d4d7150222..5b2a7bd9c2 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -2,6 +2,7 @@ Names TransparentState Uint63 Parray +Float64_common Float64 Univ UGraph diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index da77a2882e..3dee3d2b2f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -79,8 +79,10 @@ module NamedDecl = Context.Named.Declaration * STRUCT (params,oldsenv) : inside a local module, with module parameters [params] and earlier environment [oldsenv] * SIG (params,oldsenv) : same for a local module type - - [modresolver] : delta_resolver concerning the module content - - [paramresolver] : delta_resolver concerning the module parameters + - [modresolver] : delta_resolver concerning the module content, that needs to + be marshalled on disk + - [paramresolver] : delta_resolver in scope but not part of the library per + se, that is from functor parameters and required libraries - [revstruct] : current module content, most recent declarations first - [modlabels] and [objlabels] : names defined in the current module, either for modules/modtypes or for constants/inductives. @@ -1301,7 +1303,9 @@ let import lib cst vodigest senv = mp, { senv with env; - modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver; + (* Do NOT store the name quotient from the dependencies in the set of + constraints that will be marshalled on disk. *) + paramresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.paramresolver; required = DPmap.add lib.comp_name vodigest senv.required; loads = (mp,mb)::senv.loads; sections; diff --git a/lib/flags.ml b/lib/flags.ml index 1d9d6d49bc..83733cf00d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -47,6 +47,7 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let load_vos_libraries = ref false let debug = ref false +let xml_debug = ref false let in_debugger = ref false let in_toplevel = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 30d1b5b2bd..ebd23a4d20 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -41,6 +41,7 @@ val load_vos_libraries : bool ref (** Debug flags *) val debug : bool ref +val xml_debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml index 988e8e4303..4593bf4b07 100644 --- a/lib/pp_diff.ml +++ b/lib/pp_diff.ml @@ -109,7 +109,7 @@ let shorten_diff_span dtype diff_list = iter 0 len (<) 1; (* left to right *) iter (len-1) (-1) (>) (-1); (* right to left *) - if !changed then Array.to_list diffs else diff_list;; + if !changed then Array.to_list diffs else diff_list let has_changes diffs = let rec has_changes_r diffs added removed = @@ -118,12 +118,12 @@ let has_changes diffs = | `Removed _ :: t -> has_changes_r t added true | h :: t -> has_changes_r t added removed | [] -> (added, removed) in - has_changes_r diffs false false;; + has_changes_r diffs false false (* get the Myers diff of 2 lists of strings *) let diff_strs old_strs new_strs = let diffs = List.rev (StringDiff.diff old_strs new_strs) in - shorten_diff_span `Removed (shorten_diff_span `Added diffs);; + shorten_diff_span `Removed (shorten_diff_span `Added diffs) (* Default string tokenizer. Makes each character a separate strin. Whitespace is not ignored. Doesn't handle UTF-8 differences well. *) @@ -139,7 +139,7 @@ let def_tokenize_string s = let diff_str ?(tokenize_string=def_tokenize_string) old_str new_str = let old_toks = Array.of_list (tokenize_string old_str) and new_toks = Array.of_list (tokenize_string new_str) in - diff_strs old_toks new_toks;; + diff_strs old_toks new_toks let get_dinfo = function | `Common (_, _, s) -> (`Common, s) @@ -281,14 +281,14 @@ let add_diff_tags which pp diffs = skip (); if !diffs <> [] then raise (Diff_Failure "left-over diff info at end of Pp.t, should be impossible"); - if has_added || has_removed then wrap_in_bg diff_tag rv else rv;; + if has_added || has_removed then wrap_in_bg diff_tag rv else rv let diff_pp ?(tokenize_string=def_tokenize_string) o_pp n_pp = let open Pp in let o_str = string_of_ppcmds o_pp in let n_str = string_of_ppcmds n_pp in let diffs = diff_str ~tokenize_string o_str n_str in - (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);; + (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs) let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false) o_pp n_pp = let open Pp in @@ -300,4 +300,4 @@ let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false if show_removed && has_removed then let removed = add_diff_tags `Removed o_pp diffs in (v 0 (removed ++ cut() ++ added)) - else added;; + else added diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 1ec83c496a..644493a010 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -154,7 +154,7 @@ GRAMMAR EXTEND Gram | "10" LEFTA [ f = operconstr; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) } | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) } - | "@"; lid = pattern_identref; args = LIST1 identref -> + | "@"; lid = pattern_ident; args = LIST1 identref -> { let { CAst.loc = locid; v = id } = lid in let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ] @@ -252,7 +252,7 @@ GRAMMAR EXTEND Gram | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ] ; appl_arg: - [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) } + [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) } | c=operconstr LEVEL "9" -> { (c,None) } ] ] ; atomic_constr: @@ -261,12 +261,12 @@ GRAMMAR EXTEND Gram | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPrim (String s) } | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } - | "?"; "["; id = ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) } - | "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id, None) } + | "?"; "["; id = identref; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id.CAst.v, None) } + | "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id.CAst.v, None) } | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ] ; inst: - [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ] + [ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ] ; evar_instance: [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l } diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 270662b824..1701830cd2 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -45,9 +45,9 @@ let test_minus_nat = GRAMMAR EXTEND Gram GLOBAL: - bignat bigint natural integer identref name ident var preident + bignat bigint natural integer identref name ident hyp preident fullyqualid qualid reference dirpath ne_lstring - ne_string string lstring pattern_ident pattern_identref by_notation + ne_string string lstring pattern_ident by_notation smart_global bar_cbrace strategy_level; preident: [ [ s = IDENT -> { s } ] ] @@ -56,17 +56,14 @@ GRAMMAR EXTEND Gram [ [ s = IDENT -> { Id.of_string s } ] ] ; pattern_ident: - [ [ LEFTQMARK; id = ident -> { id } ] ] - ; - pattern_identref: - [ [ id = pattern_ident -> { CAst.make ~loc id } ] ] - ; - var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> { CAst.make ~loc id } ] ] + [ [ LEFTQMARK; id = ident -> { CAst.make ~loc id } ] ] ; identref: [ [ id = ident -> { CAst.make ~loc id } ] ] ; + hyp: (* as identref, but interpreted as an hypothesis in tactic notations *) + [ [ id = identref -> { id } ] ] + ; field: [ [ s = FIELD -> { Id.of_string s } ] ] ; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 723f08413e..996aa0925c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -279,14 +279,15 @@ module Prim = let strategy_level = Entry.create "strategy_level" (* parsed like ident but interpreted as a term *) - let var = Entry.create "var" + let hyp = Entry.create "hyp" + let var = hyp let name = Entry.create "name" let identref = Entry.create "identref" let univ_decl = Entry.create "univ_decl" let ident_decl = Entry.create "ident_decl" let pattern_ident = Entry.create "pattern_ident" - let pattern_identref = Entry.create "pattern_identref" + let pattern_identref = pattern_ident (* To remove in 8.14 *) (* A synonym of ident - maybe ident will be located one day *) let base_ident = Entry.create "base_ident" @@ -504,7 +505,7 @@ let () = Grammar.register0 wit_string (Prim.string); Grammar.register0 wit_pre_ident (Prim.preident); Grammar.register0 wit_ident (Prim.ident); - Grammar.register0 wit_var (Prim.var); + Grammar.register0 wit_hyp (Prim.hyp); Grammar.register0 wit_ref (Prim.reference); Grammar.register0 wit_smart_global (Prim.smart_global); Grammar.register0 wit_sort_family (Constr.sort_family); diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ae9a7423c2..8e60bbf504 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -156,8 +156,8 @@ module Prim : val identref : lident Entry.t val univ_decl : universe_decl_expr Entry.t val ident_decl : ident_decl Entry.t - val pattern_ident : Id.t Entry.t - val pattern_identref : lident Entry.t + val pattern_ident : lident Entry.t + val pattern_identref : lident Entry.t [@@ocaml.deprecated "Use Prim.pattern_identref"] val base_ident : Id.t Entry.t val bignat : string Entry.t val natural : int Entry.t @@ -173,7 +173,8 @@ module Prim : val dirpath : DirPath.t Entry.t val ne_string : string Entry.t val ne_lstring : lstring Entry.t - val var : lident Entry.t + val hyp : lident Entry.t + val var : lident Entry.t [@@ocaml.deprecated "Use Prim.hyp"] val bar_cbrace : unit Entry.t val strategy_level : Conv_oracle.level Entry.t end diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index f1f538ab39..b7ac71181a 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -20,8 +20,6 @@ open Tacarg open Names open Logic -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 863c4d37d8..ad4374dba3 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -47,7 +47,7 @@ let () = let () = let register name entry = Tacentries.register_tactic_notation_entry name entry in - register "hyp" wit_var; + register "hyp" wit_hyp; register "simple_intropattern" wit_simple_intropattern; register "integer" wit_integer; register "reference" wit_ref; @@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences GLOB_PRINTED BY { pr_occurrences } | [ ne_integer_list(l) ] -> { ArgArg l } -| [ var(id) ] -> { ArgVar id } +| [ hyp(id) ] -> { ArgVar id } END { diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4f20e5a800..a2a47c0bf4 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -33,8 +33,6 @@ open Proofview.Notations open Attributes open Vernacextend -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" @@ -450,7 +448,7 @@ END (* Subst *) TACTIC EXTEND subst -| [ "subst" ne_var_list(l) ] -> { subst l } +| [ "subst" ne_hyp_list(l) ] -> { subst l } | [ "subst" ] -> { subst_all () } END diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 2e72ceae5a..44472a1995 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -18,8 +18,6 @@ open Pcoq.Constr open Pltac open Hints -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 8d197e6056..a86045b0a4 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -77,7 +77,7 @@ END (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> { + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> { set_typeclasses_debug d; Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth @@ -87,11 +87,13 @@ END (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - { typeclasses_eauto ~strategy:Bfs ~depth:d l } + { typeclasses_eauto ~depth:d ~strategy:Bfs l } | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> { typeclasses_eauto ~depth:d l } + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> { + typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] } | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { - typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] } + typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] } END TACTIC EXTEND head_of_constr diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 8331927cda..ee94fd565a 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -29,8 +29,6 @@ open Pvernac.Vernac_ open Pltac open Vernacextend -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index e51b1f051d..c186a83a5c 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -280,7 +280,7 @@ GRAMMAR EXTEND Gram | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ] ; naming_intropattern: - [ [ prefix = pattern_ident -> { IntroFresh prefix } + [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v } | "?" -> { IntroAnonymous } | id = ident -> { IntroIdentifier id } ] ] ; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cbb53497d3..fe896f9351 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1323,7 +1323,7 @@ let () = register_basic_print0 wit_smart_global (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; - register_basic_print0 wit_var pr_lident pr_lident pr_id; + register_basic_print0 wit_hyp pr_lident pr_lident pr_id; register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env; Genprint.register_print0 diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index f7037176d2..ee28229cb7 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -161,8 +161,8 @@ let coerce_var_to_ident fresh env sigma v = match out_gen (topwit wit_intro_pattern) v with | { CAst.v=IntroNaming (IntroIdentifier id)} -> id | _ -> fail () - else if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v + else if has_type v (topwit wit_hyp) then + out_gen (topwit wit_hyp) v else match Value.to_constr v with | None -> fail () | Some c -> @@ -184,8 +184,8 @@ let id_of_name = function | Some (IntroNaming (IntroIdentifier id)) -> id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v + if has_type v (topwit wit_hyp) then + out_gen (topwit wit_hyp) v else match Value.to_constr v with | None -> fail () @@ -222,8 +222,8 @@ let coerce_to_intro_pattern sigma v = match is_intro_pattern v with | Some pat -> pat | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in IntroNaming (IntroIdentifier id) else match Value.to_constr v with | Some c when isVar sigma c -> @@ -259,8 +259,8 @@ let coerce_to_constr env v = ([], c) else if has_type v (topwit wit_constr_under_binders) then out_gen (topwit wit_constr_under_binders) v - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + else if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in (try [], constr_of_id env id with Not_found -> fail ()) else fail () @@ -282,8 +282,8 @@ let coerce_to_evaluable_ref env sigma v = | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () else if has_type v (topwit wit_ref) then @@ -328,8 +328,8 @@ let coerce_to_hyp env sigma v = | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in if is_variable env id then id else fail () else match Value.to_constr v with | Some c when isVar sigma c -> destVar sigma c @@ -360,8 +360,8 @@ let coerce_to_quantified_hypothesis sigma v = | Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id | Some _ -> raise (CannotCoerceTo "a quantified hypothesis") | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in NamedHyp id else if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index f0ca813b08..d58a76fe13 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -219,7 +219,9 @@ let interp_prod_item = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names else begin match ArgT.name s with - | None -> user_err Pp.(str ("Unknown entry "^s^".")) + | None -> + if s = "var" then user_err Pp.(str ("var is deprecated, use hyp.")) (* to remove in 8.14 *) + else user_err Pp.(str ("Unknown entry "^s^".")) | Some arg -> arg end | Some n -> diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index dea216045e..9c3b05fdf1 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -835,7 +835,7 @@ let () = Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; - Genintern.register_intern0 wit_var (lift intern_hyp); + Genintern.register_intern0 wit_hyp (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); Genintern.register_intern0 wit_ltac (lift intern_ltac); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index eaeae50254..12bfb4d09e 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -971,8 +971,8 @@ let interp_destruction_arg ist gl arg = match v with | {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id | _ -> error () - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + else if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in try_cast_id id else if has_type v (topwit wit_int) then keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) @@ -1238,7 +1238,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = | ArgVar {loc;v=id} -> let v = try Id.Map.find id ist.lfun - with Not_found -> in_gen (topwit wit_var) id + with Not_found -> in_gen (topwit wit_hyp) id in let open Ftactic in force_vrec ist v >>= begin fun v -> @@ -1529,7 +1529,7 @@ and interp_genarg ist x : Val.t Ftactic.t = let open Ftactic.Notations in (* Ad-hoc handling of some types. *) let tag = genarg_tag x in - if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then + if argument_type_eq tag (unquote (topwit (wit_list wit_hyp))) then interp_genarg_var_list ist x else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then interp_genarg_constr_list ist x @@ -1573,9 +1573,9 @@ and interp_genarg_var_list ist x = Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in + let lc = Genarg.out_gen (glbwit (wit_list wit_hyp)) x in let lc = interp_hyp_list ist env sigma lc in - let lc = in_list (val_tag wit_var) lc in + let lc = in_list (val_tag wit_hyp) lc in Ftactic.return lc end @@ -2096,7 +2096,7 @@ let () = register_interp0 wit_ref (lift interp_reference); register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); - register_interp0 wit_var (lift interp_hyp); + register_interp0 wit_hyp (lift interp_hyp); register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"]; register_interp0 wit_simple_intropattern (lifts interp_intro_pattern); register_interp0 wit_clause_dft_concl (lift interp_clause); diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index fd869b225f..ec44ae4698 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -282,7 +282,7 @@ let () = Genintern.register_subst0 wit_smart_global subst_global_reference; Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); - Genintern.register_subst0 wit_var (fun _ v -> v); + Genintern.register_subst0 wit_hyp (fun _ v -> v); Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"]; Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern; Genintern.register_subst0 wit_tactic subst_tactic; diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d859fe51ab..cb58b9bcb8 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -280,7 +280,7 @@ let interp_wit wit ist gl x = sigma, Tacinterp.Value.cast (topwit wit) arg let interp_hyp ist gl (SsrHyp (loc, id)) = - let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in + let s, id' = interp_wit wit_hyp ist gl CAst.(make ?loc id) in if not_section_id id' then s, SsrHyp (loc, id') else hyp_err ?loc "Can't clear section hypothesis " id' diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 89e0c9fcbe..7b584b5159 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -155,7 +155,7 @@ let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp) let intern_hyp ist (SsrHyp (loc, id) as hyp) = - let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in + let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_hyp) CAst.(make ?loc id)) in if not_section_id id then hyp else hyp_err ?loc "Can't clear section hypothesis " id diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 7fcb0795bd..a12a832f76 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -715,9 +715,9 @@ and detype_r d flags avoid env sigma t = (* Meta in constr are not user-parsable and are mapped to Evar *) if n = Constr_matching.special_meta then (* Using a dash to be unparsable *) - GEvar (Id.of_string_soft "CONTEXT-HOLE", []) + GEvar (CAst.make @@ Id.of_string_soft "CONTEXT-HOLE", []) else - GEvar (Id.of_string_soft ("M" ^ string_of_int n), []) + GEvar (CAst.make @@ Id.of_string_soft ("M" ^ string_of_int n), []) | Var id -> (* Discriminate between section variable and non-section variable *) (try let _ = Global.lookup_named id in GRef (GlobRef.VarRef id, None) @@ -788,12 +788,12 @@ and detype_r d flags avoid env sigma t = let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in - id,l + id,List.map (fun (id,c) -> (CAst.make id,c)) l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), - (List.map (fun c -> (Id.of_string "__",c)) cl) + (List.map (fun c -> (CAst.make @@ Id.of_string "__",c)) cl) in - GEvar (id, + GEvar (CAst.make id, List.map (on_snd (detype d flags avoid env sigma)) l) | Ind (ind_sp,u) -> GRef (GlobRef.IndRef ind_sp, detype_instance sigma u) @@ -883,7 +883,12 @@ and detype_binder d flags bk avoid env sigma decl c = | BLetIn -> let c = detype d { flags with flg_isgoal = false } avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) - let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in + let s = + (* It can fail if ty is an evar, or if run inside ocamldebug or the + OCaml toplevel since their printers don't have access to the proper sigma/env *) + try Retyping.get_sort_family_of (snd env) sigma ty + with Retyping.RetypeError _ -> InType + in let t = if s != InProp && not !Flags.raw_print then None else Some (detype d { flags with flg_isgoal = false } avoid env sigma ty) in GLetIn (na', c, t, r) diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index f33030d6a4..eaf8c65811 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -175,10 +175,7 @@ let define_evar_as_sort env evd (ev,args) = let evd' = Evd.define ev (mkSort s) evd in Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s -(* Propagation of constraints through application and abstraction: - Given a type constraint on a functional term, returns the type - constraint on its domain and codomain. If the input constraint is - an evar instantiate it with the product of 2 new evars. *) +(* Unify with unknown array *) let rec presplit env sigma c = let c = Reductionops.whd_all env sigma c in @@ -189,25 +186,6 @@ let rec presplit env sigma c = presplit env sigma (mkApp (lam, args)) | _ -> sigma, c -let split_tycon ?loc env evd tycon = - match tycon with - | None -> evd,(make_annot Anonymous Relevant,None,None) - | Some c -> - let evd, c = presplit env evd c in - let evd, na, dom, rng = match EConstr.kind evd c with - | Prod (na,dom,rng) -> evd, na, dom, rng - | Evar ev -> - let (evd,prod) = define_evar_as_product env evd ev in - let (na,dom,rng) = destProd evd prod in - let anon = {na with binder_name = Anonymous} in - evd, anon, dom, rng - | _ -> - (* XXX no error to allow later coercion? Not sure if possible with funclass *) - error_not_product ?loc env evd c - in - evd, (na, mk_tycon dom, mk_tycon rng) - - let define_pure_evar_as_array env sigma evk = let evi = Evd.find_undefined sigma evk in let evenv = evar_env env evi in diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index e5c3f8baa1..5702e169c8 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names open EConstr open Evd open Environ @@ -31,10 +30,6 @@ val mk_valcon : constr -> val_constraint val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> evar_map * existential -val split_tycon : - ?loc:Loc.t -> env -> evar_map -> type_constraint -> - evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint) - val split_as_array : env -> evar_map -> type_constraint -> evar_map * type_constraint (** If the constraint can be made to look like [array A] return [A], @@ -51,3 +46,6 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t val pr_tycon : env -> evar_map -> type_constraint -> Pp.t +(** Used for bidi heuristic when typing lambdas. Transforms an applied + evar to an evar with bigger context (ie ?X e to ?X'@{y=e}). *) +val presplit : env -> evar_map -> EConstr.t -> evar_map * EConstr.t diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 5bd26be823..dc5fd80f9e 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -128,7 +128,7 @@ let fix_kind_eq k1 k2 = match k1, k2 with | (GFix _ | GCoFix _), _ -> false let instance_eq f (x1,c1) (x2,c2) = - Id.equal x1 x2 && f c1 c2 + Id.equal x1.CAst.v x2.CAst.v && f c1 c2 let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GRef (gr1, u1), GRef (gr2, u2) -> @@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with Option.equal (List.equal glob_level_eq) u1 u2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> - Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2 + Id.equal id1.CAst.v id2.CAst.v && List.equal (instance_eq f) arg1 arg2 | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2 | GApp (f1, arg1), GApp (f2, arg2) -> f f1 f2 && List.equal f arg1 arg2 diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 526eac6f1e..a49c8abe26 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -75,7 +75,7 @@ type 'a glob_constr_r = | GVar of Id.t (** An identifier that cannot be regarded as "GRef". Bound variables are typically represented this way. *) - | GEvar of existential_name * (Id.t * 'a glob_constr_g) list + | GEvar of existential_name CAst.t * (lident * 'a glob_constr_g) list | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *) | GApp of 'a glob_constr_g * 'a glob_constr_g list | GLambda of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 1e8441dd8a..1dddc5622d 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -48,7 +48,7 @@ type pretype_error = | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t | NonLinearUnification of Name.t * constr diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 45997e9a66..714d68165e 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -54,7 +54,7 @@ type pretype_error = | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t | NonLinearUnification of Name.t * constr @@ -132,7 +132,7 @@ val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> - constr -> constr list -> (env * type_error) option -> 'b + constr -> constr list -> (env * pretype_error) option -> 'b val error_wrong_abstraction_type : env -> Evd.evar_map -> Name.t -> constr -> types -> types -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b9825b6a92..268ad2ae56 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -365,9 +365,9 @@ let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = functio | Some t -> Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t -let check_instance loc subst = function +let check_instance subst = function | [] -> () - | (id,_) :: _ -> + | (CAst.{loc;v=id},_) :: _ -> if List.mem_assoc id subst then user_err ?loc (Id.print id ++ str "appears more than once.") else @@ -493,7 +493,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> ty type pretyper = { pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun; pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun; - pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun; + pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun; pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun; pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun; pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun; @@ -587,10 +587,10 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk strbrk " is not well-typed.") in let sigma, c, update = try - let c = List.assoc id update in + let c = snd (List.find (fun (CAst.{v=id'},c) -> Id.equal id id') update) in let sigma, c = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon t) env sigma c in check_body sigma id (Some c.uj_val); - sigma, c.uj_val, List.remove_assoc id update + sigma, c.uj_val, List.remove_first (fun (CAst.{v=id'},_) -> Id.equal id id') update with Not_found -> try let (n,b',t') = lookup_rel_id id (rel_context !!env) in @@ -609,7 +609,7 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk str " in current context: no binding for " ++ Id.print id ++ str ".") in ((id,c)::subst, update, sigma) in let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in - check_instance loc subst inst; + check_instance subst inst; sigma, List.map snd subst module Default = @@ -628,13 +628,13 @@ struct let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon - let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma = + let pretype_evar self (CAst.{v=id;loc=locid}, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma = (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) let id = interp_ltac_id env id in let evk = try Evd.evar_key id sigma - with Not_found -> error_evar_not_found ?loc !!env sigma id in + with Not_found -> error_evar_not_found ?loc:locid !!env sigma id in let hyps = evar_filtered_context (Evd.find sigma evk) in let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in let c = mkEvar (evk, args) in @@ -857,7 +857,7 @@ struct typing the argument, so we replace it by an existential variable *) let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in - (sigma, make_judge c_hole c1), (c_hole, c, trace) :: bidiargs + (sigma, make_judge c_hole c1), (c_hole, c1, c, trace) :: bidiargs else let tycon = Some c1 in pretype tycon env sigma c, bidiargs @@ -886,12 +886,10 @@ struct let sigma, resj, resj_before_bidi, bidiargs = apply_rec env sigma 0 fj fj candargs [] args in let sigma, resj = refresh_template env sigma resj in let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in - let refine_arg n (sigma,t) (newarg,origarg,trace) = + let refine_arg n (sigma,t) (newarg,ty,origarg,trace) = (* Refine an argument (originally `origarg`) represented by an evar (`newarg`) to use typing information from the context *) - (* Recover the expected type of the argument *) - let ty = Retyping.get_type_of !!env sigma newarg in - (* Type the argument using this expected type *) + (* Type the argument using the expected type *) let sigma, j = pretype (Some ty) env sigma origarg in (* Unify the (possibly refined) existential variable with the (typechecked) original value *) @@ -925,7 +923,32 @@ struct let sigma, ty' = Coercion.inh_coerce_to_prod ?loc ~program_mode !!env sigma ty in sigma, Some ty' in - let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in + let sigma,name',dom,rng = + match tycon' with + | None -> sigma,Anonymous, None, None + | Some ty -> + let sigma, ty = Evardefine.presplit !!env sigma ty in + match EConstr.kind sigma ty with + | Prod (na,dom,rng) -> + sigma, na.binder_name, Some dom, Some rng + | Evar ev -> + (* define_evar_as_product works badly when impredicativity + is possible but not known (#12623). OTOH if we know we + are impredicative (typically Prop) we want to keep the + information when typing the body. *) + let s = Retyping.get_sort_of !!env sigma ty in + if Environ.is_impredicative_sort !!env s + || Evd.check_leq sigma (Univ.Universe.type1) (Sorts.univ_of_sort s) + then + let sigma, prod = define_evar_as_product !!env sigma ev in + let na,dom,rng = destProd sigma prod in + sigma, na.binder_name, Some dom, Some rng + else + sigma, Anonymous, None, None + | _ -> + (* XXX no error to allow later coercion? Not sure if possible with funclass *) + error_not_product ?loc !!env sigma ty + in let dom_valcon = valcon_of_tycon dom in let sigma, j = eval_type_pretyper self ~program_mode ~poly resolve_tc dom_valcon env sigma c1 in let name = {binder_name=name; binder_relevance=Sorts.relevance_of_sort j.utj_type} in @@ -934,7 +957,7 @@ struct let var',env' = push_rel ~hypnaming sigma var env in let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in let name = get_name var' in - let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in + let resj = judge_of_abstraction !!env (orelse_name name name') j j' in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_prod self (name, bk, c1, c2) = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index c03374c59f..7bb4a6e273 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -148,7 +148,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> Ev type pretyper = { pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun; pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun; - pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun; + pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun; pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun; pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun; pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun; diff --git a/pretyping/typing.ml b/pretyping/typing.ml index e40dea06e7..aeb3873de7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -220,14 +220,15 @@ let check_allowed_sort env sigma ind c p = else Sorts.relevance_of_sort_family ksort +let check_actual_type env sigma cj t = + try Evarconv.unify_leq_delay env sigma cj.uj_type t + with Evarconv.UnableToUnify (sigma,e) -> error_actual_type env sigma cj t e + let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in - match Evarconv.unify_leq_delay env sigma cj.uj_type expected_type with - | exception Evarconv.UnableToUnify _ -> - error_actual_type_core env sigma cj expected_type; - | sigma -> - sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); - uj_type = expected_type } + let sigma = check_actual_type env sigma cj expected_type in + sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); + uj_type = expected_type } let check_fix env sigma pfix = let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in @@ -341,7 +342,7 @@ let judge_of_array env sigma u tj defj tyj = let sigma = Evd.set_leq_sort env sigma tyj.utj_type (Sorts.sort_of_univ (Univ.Universe.make ulev)) in - let check_one sigma j = Evarconv.unify_leq_delay env sigma j.uj_type tyj.utj_val in + let check_one sigma j = check_actual_type env sigma j tyj.utj_val in let sigma = check_one sigma defj in let sigma = Array.fold_left check_one sigma tj in let arr = EConstr.of_constr @@ type_of_array env u in @@ -392,7 +393,7 @@ let rec execute env sigma cstr = let t = mkApp (mkIndU (ci.ci_ind,univs), args) in let sigma, tj = execute env sigma t in let sigma, tj = type_judgment env sigma tj in - let sigma = Evarconv.unify_leq_delay env sigma cj.uj_type tj.utj_val in + let sigma = check_actual_type env sigma cj tj.utj_val in sigma in judge_of_case env sigma ci pj iv cj lfj @@ -493,10 +494,7 @@ and execute_array env = Array.fold_left_map (execute env) let check env sigma c t = let sigma, j = execute env sigma c in - match Evarconv.unify_leq_delay env sigma j.uj_type t with - | exception Evarconv.UnableToUnify _ -> - error_actual_type_core env sigma j t - | sigma -> sigma + check_actual_type env sigma j t (* Type of a constr *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 207a03d80f..ccfb508964 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -134,8 +134,8 @@ let abstract_list_all env evd typ c l = | Type_errors.TypeError (env',x) -> (* FIXME: plug back the typing information *) error_cannot_find_well_typed_abstraction env evd p l None - | Pretype_errors.PretypeError (env',evd,TypingError x) -> - error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in + | Pretype_errors.PretypeError (env',evd,e) -> + error_cannot_find_well_typed_abstraction env evd p l (Some (env',e)) in evd,(p,typp) let set_occurrences_of_last_arg n = diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 900ba0edb9..1420401875 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -218,7 +218,8 @@ and nf_evar env sigma evk stk = let t = List.fold_left fold concl hyps in let t, args = nf_args env sigma args t in let inst, args = Array.chop (List.length hyps) args in - let inst = Array.to_list inst in + (* Evar instances are reversed w.r.t. argument order *) + let inst = Array.rev_to_list inst in let c = mkApp (mkEvar (evk, inst), args) in nf_stk env sigma c t stk | _ -> diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 267f5e0b5f..8da1d636f0 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -227,13 +227,49 @@ let tag_var = tag Tag.variable let pr_evar pr id l = hov 0 ( - tag_evar (str "?" ++ pr_id id) ++ + tag_evar (str "?" ++ pr_lident id) ++ (match l with | [] -> mt() | l -> - let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in + let f (id,c) = pr_lident id ++ str ":=" ++ pr ltop c in str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) + (* Assuming "{" and "}" brackets, prints + - if there is enough room + { a; b; c } + - otherwise + { + a; + b; + c + } + Alternatively, replace outer hv with h to get instead: + { a; + b; + c } + Replace the inner hv with hov to respectively get instead (if enough room): + { + a; b; + c + } + or + { a; b; + c } + *) + let pr_record left right pr = function + | [] -> str left ++ str " " ++ str right + | l -> + hv 0 ( + str left ++ + brk (1,String.length left) ++ + hv 0 (prlist_with_sep pr_semicolon pr l) ++ + brk (1,0) ++ + str right) + + let pr_record_body left right pr l = + let pr_defined_field (id, c) = hov 2 (pr_reference id ++ str" :=" ++ pr c) in + pr_record left right pr_defined_field l + let las = lapp let lpator = 0 let lpatrec = 0 @@ -242,11 +278,7 @@ let tag_var = tag Tag.variable let rec pr_patt sep inh p = let (strm,prec) = match CAst.(p.v) with | CPatRecord l -> - let pp (c, p) = - pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p - in - (if l = [] then str "{| |}" - else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec + pr_record_body "{|" "|}" (pr_patt spc lpattop) l, lpatrec | CPatAlias (p, na) -> pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las @@ -287,6 +319,7 @@ let tag_var = tag Tag.variable | CPatDelimiters (k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 + | CPatCast _ -> assert false in @@ -464,11 +497,6 @@ let tag_var = tag Tag.variable pr (LevelLt lapp) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) - let pr_record_body_gen pr l = - spc () ++ - prlist_with_sep pr_semicolon - (fun (id, c) -> pr_reference id ++ str" :=" ++ pr ltop c) l - let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc () let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc () @@ -568,10 +596,7 @@ let tag_var = tag Tag.variable | CApp ((None,a),l) -> return (pr_app (pr mt) a l, lapp) | CRecord l -> - return ( - hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), - latom - ) + return (pr_record_body "{|" "|}" (pr spc ltop) l, latom) | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( @@ -717,7 +742,5 @@ let tag_var = tag Tag.variable let pr_cases_pattern_expr = pr_patt ltop - let pr_record_body = pr_record_body_gen pr - let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 2850e4bfa0..02e04573f8 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -41,7 +41,8 @@ val pr_guard_annot -> recursion_order_expr option -> Pp.t -val pr_record_body : (qualid * constr_expr) list -> Pp.t +val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t +val pr_record_body : string -> string -> ('a -> Pp.t) -> (Libnames.qualid * 'a) list -> Pp.t val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t val pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index a1a2d9ae51..bc26caefbe 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -765,9 +765,9 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map v 0 ( int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ print_extra - ++ str (if (should_gname()) then ", subgoal 1" else "") - ++ (if should_tag() then pr_goal_tag g1 else str"") - ++ pr_goal_name sigma g1 ++ cut () ++ goals + ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", subgoal 1" else "") + ++ (if pr_first && should_tag() then pr_goal_tag g1 else str"") + ++ (if pr_first then pr_goal_name sigma g1 else mt()) ++ cut () ++ goals ++ (if unfocused=[] then str "" else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut() ++ pr_rec (List.length rest + 2) unfocused)) diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 43f70dfecc..b2ebc61b4e 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -252,6 +252,9 @@ let pp_of_type env sigma ty = let pr_leconstr_env ?lax ?inctx ?scope env sigma t = Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) +let pr_econstr_env ?lax ?inctx ?scope env sigma t = + Ppconstr.pr_constr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) + let pr_lconstr_env ?lax ?inctx ?scope env sigma c = pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c) @@ -511,12 +514,12 @@ let match_goals ot nt = | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> () | CPatVar _, CPatVar _ -> () | CEvar (n,l), CEvar (n2,l2) -> - let oevar = if ogname = "" then Id.to_string n else ogname in - nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar; + let oevar = if ogname = "" then Id.to_string n.CAst.v else ogname in + nevar_to_oevar := CString.Map.add (Id.to_string n2.CAst.v) oevar !nevar_to_oevar; iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 | CEvar (n,l), nt' -> (* pass down the old goal evar name *) - match_goals_r (Id.to_string n) nt' nt' + match_goals_r (Id.to_string n.CAst.v) nt' nt' | CSort s, CSort s2 -> () | CCast (c,c'), CCast (c2,c'2) -> constr_expr ogname c c2; @@ -660,3 +663,22 @@ let make_goal_map op np = let ng_to_og = make_goal_map_i op np in (*db_goal_map op np ng_to_og;*) ng_to_og + +let diff_proofs ~diff_opt ?old proof = + let pp_proof p = + let sigma, env = Proof.get_proof_context p in + let pprf = Proof.partial_proof p in + Pp.prlist_with_sep Pp.fnl (pr_econstr_env env sigma) pprf in + match diff_opt with + | DiffOff -> pp_proof proof + | _ -> begin + try + let n_pp = pp_proof proof in + let o_pp = match old with + | None -> Pp.mt() + | Some old -> pp_proof old in + let show_removed = Some (diff_opt = DiffRemoved) in + Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp + with + | Pp_diff.Diff_Failure msg -> Pp.str msg + end diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index ea64439456..6bdd7004fb 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -25,6 +25,10 @@ val write_color_enabled : bool -> unit (** true indicates that color output is enabled *) val color_enabled : unit -> bool +type diffOpt = DiffOff | DiffOn | DiffRemoved + +val string_to_diffs : string -> diffOpt + open Evd open Environ open Constr @@ -84,3 +88,5 @@ type hyp_info = { } val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list + +val diff_proofs : diff_opt:diffOpt -> ?old:Proof.t -> Proof.t -> Pp.t diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 3996c64b67..ffae2866c0 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -128,7 +128,7 @@ let classify_vernac e = | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ CList.map_filter (function - | AssumExpr({v=Names.Name n},_), _ -> Some n + | AssumExpr({v=Names.Name n},_,_), _ -> Some n | _ -> None) l) l in VtSideff (List.flatten ids, VtLater) | VernacScheme l -> diff --git a/test-suite/bugs/closed/bug_12414.v b/test-suite/bugs/closed/bug_12414.v new file mode 100644 index 0000000000..50b4b86eff --- /dev/null +++ b/test-suite/bugs/closed/bug_12414.v @@ -0,0 +1,13 @@ +Set Universe Polymorphism. +Set Printing Universes. +Inductive list {T} : Type := | cons (t : T) : list -> list. (* who needs nil anyway? *) +Arguments list : clear implicits. + +Fixpoint map {A B} (f: A -> B) (l : list A) : list B := + let '(cons t l) := l in cons (f t) (map f l). +About map@{_ _}. +(* Two universes, as expected. *) + +Definition map_Set@{} {A B : Set} := @map A B. + +Definition map_Prop@{} {A B : Prop} := @map A B. diff --git a/test-suite/bugs/closed/bug_12623.v b/test-suite/bugs/closed/bug_12623.v new file mode 100644 index 0000000000..9fdcb94e0c --- /dev/null +++ b/test-suite/bugs/closed/bug_12623.v @@ -0,0 +1,18 @@ +Set Universe Polymorphism. + +Axiom M : Type -> Prop. +Axiom raise : forall {T}, M T. + +Inductive goal : Type := +| AHyp : forall {A : Type}, goal. + +Definition gtactic@{u u0} := goal@{u} -> M@{u0} (False). + +Class Seq (C : Type) := + seq : C -> gtactic. +Arguments seq {C _} _. + +Instance seq_one : Seq@{Set _ _} (gtactic) := fun t2 => fun g => raise. + +Definition x1 : gtactic := @seq@{_ _ _} _ _ (fun g : goal => raise). +Definition x2 : gtactic := @seq@{_ _ _} _ seq_one (fun g : goal => raise). diff --git a/test-suite/bugs/closed/bug_12895.v b/test-suite/bugs/closed/bug_12895.v new file mode 100644 index 0000000000..53adc2981c --- /dev/null +++ b/test-suite/bugs/closed/bug_12895.v @@ -0,0 +1,20 @@ +Fixpoint bug_1 (e1 : nat) {struct e1} + : nat +with bug_2 {H_imp : nat} (e2 : nat) {struct e2} + : nat. +Proof. + - exact e1. + - exact e2. +Admitted. + +Fixpoint hbug_1 (a:bool) (e1 : nat) {struct e1} + : nat +with hbug_2 (a:nat) (e2 : nat) {struct e2} + : nat. +Proof. + - exact e1. + - exact e2. +Admitted. + +Check (hbug_1 : bool -> nat -> nat). +Check (hbug_2 : nat -> nat -> nat). diff --git a/test-suite/bugs/closed/bug_12970.v b/test-suite/bugs/closed/bug_12970.v new file mode 100644 index 0000000000..69ce7ec2c2 --- /dev/null +++ b/test-suite/bugs/closed/bug_12970.v @@ -0,0 +1,4 @@ +Arguments existT _ & _ _. + +Definition f := fun X (A : X -> Type) (P : forall x, A x -> Type) x y => + existT (fun f => forall x, P x (f x)) x y : sigT (fun f => forall x, P x (f x)). diff --git a/test-suite/bugs/closed/bug_13169.v b/test-suite/bugs/closed/bug_13169.v new file mode 100644 index 0000000000..a0b564c725 --- /dev/null +++ b/test-suite/bugs/closed/bug_13169.v @@ -0,0 +1,14 @@ +Goal False. +Proof. + set (H1:=I). + set (x:=true). + assert (H2: x = true) by reflexivity. + set (y:=false). + assert (H3: y = false) by reflexivity. + clearbody H1 x y. + eenough (H4: _ = false). + vm_compute in H4. + (* H4 now has "x:=y" in the evar context. *) + 2: exact H3. + match type of H4 with y = false => idtac end. +Abort. diff --git a/test-suite/bugs/closed/bug_13171.v b/test-suite/bugs/closed/bug_13171.v new file mode 100644 index 0000000000..0564722729 --- /dev/null +++ b/test-suite/bugs/closed/bug_13171.v @@ -0,0 +1,10 @@ +Primitive array := #array_type. + +Goal False. +Proof. + unshelve epose (_:nat). exact_no_check true. + Fail let c := open_constr:([| n | 0 |]) in + let c := eval cbv in c in + let c := type of c in + idtac c. +Abort. diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v index 0c236e12ad..00b9e9bd9d 100644 --- a/test-suite/bugs/closed/bug_5197.v +++ b/test-suite/bugs/closed/bug_5197.v @@ -20,11 +20,11 @@ Definition Typeᶠ : TYPE := {| rel := fun _ A => (forall ω : Ω, A ω) -> Type; |}. Set Printing Universes. -Fail Definition Typeᵇ : El Typeᶠ := +Definition Typeᵇ : El Typeᶠ := mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type). -Definition Typeᵇ : El Typeᶠ := - mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). +(* Definition Typeᵇ : El Typeᶠ := *) +(* mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). *) (** Bidirectional typechecking helps here *) Require Import Program.Tactics. diff --git a/test-suite/ide/proof-diffs.fake b/test-suite/ide/proof-diffs.fake new file mode 100644 index 0000000000..594ebced23 --- /dev/null +++ b/test-suite/ide/proof-diffs.fake @@ -0,0 +1,10 @@ +ADD { Goal True /\ False /\ True = False. } +ADD { split. } +GOALS +ADD here { split. } +GOALS +PDIFF here +ADD there { auto. } +GOALS +PDIFF there +ADD { Admitted. } diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index abada44da7..bd22d45059 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -231,16 +231,13 @@ fun l : list nat => match l with : list nat -> list nat Arguments foo _%list_scope -Notation -"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope -(default interpretation) -"'exists' ! x .. y , p" := ex - (unique - (fun x => .. (ex (unique (fun y => p))) ..)) -: type_scope (default interpretation) -Notation -"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope -(default interpretation) +Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) + : type_scope (default interpretation) +Notation "'exists' ! x .. y , p" := + (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope + (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope + (default interpretation) 1 subgoal ============================ diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index d45343fe60..7de1e7d559 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -30,3 +30,43 @@ fun '{| U := T; a := a; q := p |} => (T, p, a) : M -> Type * True * nat fun '{| U := T; a := a; q := p |} => (T, p, a) : M -> Type * True * nat +{| a := 0; b := 0 |} + : T +fun '{| |} => 0 + : LongModuleName.test -> nat + = {| + a := + {| + LongModuleName.long_field_name0 := 0; + LongModuleName.long_field_name1 := 1; + LongModuleName.long_field_name2 := 2; + LongModuleName.long_field_name3 := 3 + |}; + b := + fun + '{| + LongModuleName.long_field_name0 := a; + LongModuleName.long_field_name1 := b; + LongModuleName.long_field_name2 := c; + LongModuleName.long_field_name3 := d + |} => (a, b, c, d) + |} + : T + = {| + a := + {| + long_field_name0 := 0; + long_field_name1 := 1; + long_field_name2 := 2; + long_field_name3 := 3 + |}; + b := + fun + '{| + long_field_name0 := a; + long_field_name1 := b; + long_field_name2 := c; + long_field_name3 := d + |} => (a, b, c, d) + |} + : T diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 71a8afa131..13ea37b11e 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -33,3 +33,34 @@ Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). Check fun x:M => let 'D T a p := x in (T,p,a). Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a). + +Module FormattingIssue13142. + +Record T {A B} := {a:A;b:B}. + +Module LongModuleName. + Record test := { long_field_name0 : nat; + long_field_name1 : nat; + long_field_name2 : nat; + long_field_name3 : nat }. +End LongModuleName. + +Definition c := + {| LongModuleName.long_field_name0 := 0; + LongModuleName.long_field_name1 := 1; + LongModuleName.long_field_name2 := 2; + LongModuleName.long_field_name3 := 3 |}. + +Definition d := + fun '{| LongModuleName.long_field_name0 := a; + LongModuleName.long_field_name1 := b; + LongModuleName.long_field_name2 := c; + LongModuleName.long_field_name3 := d |} => (a,b,c,d). + +Check {|a:=0;b:=0|}. +Check fun '{| LongModuleName.long_field_name0:=_ |} => 0. +Eval compute in {|a:=c;b:=d|}. +Import LongModuleName. +Eval compute in {|a:=c;b:=d|}. + +End FormattingIssue13142. diff --git a/test-suite/output/bug_12908.out b/test-suite/output/bug_12908.out index fca6dde704..54c4f98422 100644 --- a/test-suite/output/bug_12908.out +++ b/test-suite/output/bug_12908.out @@ -1,2 +1,7 @@ forall m n : nat, m * n = (2 * m * n)%nat : Prop +File "stdin", line 11, characters 0-31: +Warning: Notation "_ * _" was already used in scope nat_scope. +[notation-overridden,parsing] +forall m n : nat, m * n = Nat.mul (Nat.mul 2 m) n + : Prop diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v index 558c9f9f6a..6f7be22fa0 100644 --- a/test-suite/output/bug_12908.v +++ b/test-suite/output/bug_12908.v @@ -1,6 +1,13 @@ Definition mult' m n := 2 * m * n. + Module A. (* Test hiding of a scoped notation by a lonely notation *) Infix "*" := mult'. Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End A. + +Module B. +(* Test that an overriden scoped notation is deactivated *) +Infix "*" := mult' : nat_scope. +Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. +End B. diff --git a/test-suite/output/bug_13112.out b/test-suite/output/bug_13112.out new file mode 100644 index 0000000000..a8a98d6b68 --- /dev/null +++ b/test-suite/output/bug_13112.out @@ -0,0 +1,4 @@ +0 + 0 + : nat +HI + : nat diff --git a/test-suite/output/bug_13112.v b/test-suite/output/bug_13112.v new file mode 100644 index 0000000000..9fee5e09d8 --- /dev/null +++ b/test-suite/output/bug_13112.v @@ -0,0 +1,5 @@ +Reserved Notation "'HI'". +Notation "'HI'" := (O + O) (only parsing). +Check HI. (* 0 + 0 : nat *) +Notation "'HI'" := (O + O) (only printing). +Check HI. (* 0 + 0 : nat *) diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out index ed4892b389..f035d0252a 100644 --- a/test-suite/output/bug_9180.out +++ b/test-suite/output/bug_9180.out @@ -1,4 +1,3 @@ -Notation -"n .+1" := S n : nat_scope (default interpretation) +Notation "n .+1" := (S n) : nat_scope (default interpretation) forall x : nat, x.+1 = x.+1 : Prop diff --git a/test-suite/output/bug_9682.out b/test-suite/output/bug_9682.out index e69de29bb2..45d9e4cad1 100644 --- a/test-suite/output/bug_9682.out +++ b/test-suite/output/bug_9682.out @@ -0,0 +1,9 @@ +mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x +return M (x = x) with +| 1 +end + : unit +# + : True +## + : True diff --git a/test-suite/output/bug_9682.v b/test-suite/output/bug_9682.v index 3630142126..fa30d323ef 100644 --- a/test-suite/output/bug_9682.v +++ b/test-suite/output/bug_9682.v @@ -16,3 +16,13 @@ Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" := (at level 200, ls at level 91, p at level 10, only printing, format "'[ ' mmatch '/' x ']' '/' '[ ' in '/' T ']' '/' '[ ' as '/' y ']' '/' '[ ' return M p ']' with '//' '[' ls ']' '//' end" ). +(* Check use of "mmatch" *) +Check (mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x return M (x = x) with | 1 end). + +(* 2nd example *) +Notation "#" := I (at level 0, only parsing). +Notation "#" := I (at level 0, only printing). +Check #. +Notation "##" := I (at level 0, only printing). +Notation "##" := I (at level 0, only parsing). +Check ##. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 773533a8d3..17c1aaa55b 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -2,7 +2,79 @@ Nat.t = nat : Set Nat.t = nat : Set +2 subgoals + + ============================ + True + +subgoal 2 is: + True +2 subgoals, subgoal 1 (?Goal) + + ============================ + True + +subgoal 2 (?Goal0) is: + True 1 subgoal ============================ - False + True +1 subgoal (?Goal0) + + ============================ + True +1 subgoal (?Goal0) + + ============================ + True + +*** Unfocused goals: + +subgoal 2 (?Goal1) is: + True +subgoal 3 (?Goal) is: + True +1 subgoal + + ============================ + True + +*** Unfocused goals: + +subgoal 2 is: + True +subgoal 3 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +2 subgoals + +subgoal 1 is: + True +subgoal 2 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +2 subgoals + +subgoal 1 (?Goal0) is: + True +subgoal 2 (?Goal) is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +1 subgoal + +subgoal 1 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +1 subgoal + +subgoal 1 (?Goal) is: + True diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v index 327b80b0aa..b1ced94054 100644 --- a/test-suite/output/goal_output.v +++ b/test-suite/output/goal_output.v @@ -6,8 +6,32 @@ Print Nat.t. Timeout 1 Print Nat.t. -Lemma toto: False. Set Printing All. +Lemma toto: True/\True. +Proof. +split. Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. +assert True. +- idtac. +Show. +Set Printing Goal Names. +Show. +Set Printing Unfocused. +Show. +Unset Printing Goal Names. +Show. +Unset Printing Unfocused. + auto. +Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. +- auto. +Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. Abort. - diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 473db2d312..93d9d6cf7b 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,3 +1,2 @@ -Notation -"b1 && b2" := if b1 then b2 else false (default interpretation) -"x && y" := andb x y : bool_scope +Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) +Notation "x && y" := (andb x y) : bool_scope diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index 998f3f7dd1..73e98ea920 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -1,6 +1,8 @@ Require Import TestSuite.admit. (* compile en user 3m39.915s sur cachalot *) Require Import Nsatz. +Require List. +Import List.ListNotations. (* Example with a generic domain *) @@ -294,7 +296,7 @@ Lemma minh: forall A B C D O E H I:point, Proof. geo_begin. idtac "minh". Time nsatz with radicalmax :=1%N strategy:=1%Z - parameters:=(X O::X B::X C::nil) + parameters:=[X O; X B; X C] variables:= (@nil R). (*Finished transaction in 13. secs (10.102464u,0.s) *) @@ -314,15 +316,15 @@ Proof. geo_begin. idtac "Pappus". Time nsatz with radicalmax :=1%N strategy:=0%Z - parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil) - variables:= (X B - :: X A1 - :: Y A1 - :: X B1 - :: Y B1 - :: X C - :: Y C1 - :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil). + parameters:=[X B; X A1; Y A1; X B1; Y B1; X C; Y C1] + variables:= [X B; + X A1; + Y A1; + X B1; + Y B1; + X C; + Y C1; + X C1; Y P; X P; Y Q; X Q; Y S; X S]. (*Finished transaction in 8. secs (7.795815u,0.000999999999999s) *) Qed. @@ -347,7 +349,7 @@ Proof. geo_begin. idtac "Simson". Time nsatz with radicalmax :=1%N strategy:=0%Z - parameters:=(X B::Y B::X C::Y C::Y D::nil) + parameters:=[X B; Y B; X C; Y C; Y D] variables:= (@nil R). (* compute -[X Y]. *) (*Finished transaction in 8. secs (7.550852u,0.s) *) @@ -432,20 +434,20 @@ Proof. geo_begin. idtac "Desargues". Time -let lv := rev (X A - :: X B - :: Y B - :: X C - :: Y C - :: Y A1 :: X A1 - :: Y B1 - :: Y C1 - :: X T - :: Y T - :: X Q - :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in +let lv := rev [X A; + X B; + Y B; + X C; + Y C; + Y A1; X A1; + Y B1; + Y C1; + X T; + Y T; + X Q; + Y Q; X P; Y P; X C1; X B1] in nsatz with radicalmax :=1%N strategy:=0%Z - parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil) + parameters:=[X A; X B; Y B; X C; Y C; X A1; Y B1; Y C1] variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*) Qed. @@ -522,9 +524,9 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point, geo_begin. idtac "hauteurs". Time - let lv := constr:(Y A1 - :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C - :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in + let lv := constr:([Y A1; + X A1; Y B1; X B1; Y A; Y B; X B; X A; X H; Y C; + Y C1; Y H; X C1; X C]) in nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R) variables := lv. (*Finished transaction in 5. secs (4.360337u,0.008999s)*) diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index ce07512a1e..beb424dd40 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -93,3 +93,18 @@ Record R : Type := { (* This is used in a couple of development such as UniMatch *) Record S {A:Type} := { a : A; b : forall A:Type, A }. + +(* Bug #13165 on implicit arguments in defined fields *) +Record T := { + f {n:nat} (p:n=n) := nat; + g := f (eq_refl 0) +}. + +(* Slight improvement in when SProp relevance is detected *) +Inductive True : SProp := I. +Inductive eqI : True -> SProp := reflI : eqI I. + +Record U (c:True) := { + u := c; + v := reflI : eqI u; + }. diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 9ab8ace39e..0796b507a1 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -457,5 +457,10 @@ Module ObligationRegression. (** Test for a regression encountered when fixing obligations for stronger restriction of universe context. *) Require Import CMorphisms. - Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _ _}. + Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _}. End ObligationRegression. + +Axiom poly@{i} : forall(A : Type@{i}) (a : A), unit. + +Definition nonpoly := @poly True Logic.I. +Definition check := nonpoly@{}. diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index f35da63fd6..e8a036bbb0 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -1401,8 +1401,8 @@ Definition mem T (pT : predType T) : pT -> mem_pred T := let: PredType toP := pT in fun A => Mem [eta toP A]. Arguments mem {T pT} A : rename, simpl never. -Notation "x \in A" := (in_mem x (mem A)) : bool_scope. -Notation "x \in A" := (in_mem x (mem A)) : bool_scope. +Notation "x \in A" := (in_mem x (mem A)) (only parsing) : bool_scope. +Notation "x \in A" := (in_mem x (mem A)) (only printing) : bool_scope. Notation "x \notin A" := (~~ (x \in A)) : bool_scope. Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope. Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B)) : type_scope. @@ -1573,9 +1573,12 @@ Arguments has_quality n {T}. Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed. -Notation "x \is A" := (x \in has_quality 0 A) : bool_scope. -Notation "x \is 'a' A" := (x \in has_quality 1 A) : bool_scope. -Notation "x \is 'an' A" := (x \in has_quality 2 A) : bool_scope. +Notation "x \is A" := (x \in has_quality 0 A) (only parsing) : bool_scope. +Notation "x \is A" := (x \in has_quality 0 A) (only printing) : bool_scope. +Notation "x \is 'a' A" := (x \in has_quality 1 A) (only parsing) : bool_scope. +Notation "x \is 'a' A" := (x \in has_quality 1 A) (only printing) : bool_scope. +Notation "x \is 'an' A" := (x \in has_quality 2 A) (only parsing) : bool_scope. +Notation "x \is 'an' A" := (x \in has_quality 2 A) (only printing) : bool_scope. Notation "x \isn't A" := (x \notin has_quality 0 A) : bool_scope. Notation "x \isn't 'a' A" := (x \notin has_quality 1 A) : bool_scope. Notation "x \isn't 'an' A" := (x \notin has_quality 2 A) : bool_scope. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index eb386ea3e8..d587e57fd8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -508,6 +508,7 @@ let parse_args ~help ~init arglist : t * string list = |"-color" -> set_color oval (next ()) |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval + |"-xml-debug" -> Flags.xml_debug := true; Coqinit.set_debug (); oval |"-diffs" -> add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ())) |"-stm-debug" -> Stm.stm_debug := true; oval diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 88924160ff..6460378edc 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -371,41 +371,13 @@ let exit_on_error = declare_bool_option_and_ref ~depr:false ~key:["Coqtop";"Exit";"On";"Error"] ~value:false -(* XXX: This is duplicated with Vernacentries.show_proof , at some - point we should consolidate the code *) -let show_proof_diff_to_pp pstate = - let p = Option.get pstate in - let sigma, env = Proof.get_proof_context p in - let pprf = Proof.partial_proof p in - Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf - -let show_proof_diff_cmd ~state removed = +let show_proof_diff_cmd ~state diff_opt = let open Vernac.State in - try - let n_pp = show_proof_diff_to_pp state.proof in - if true (*Proof_diffs.show_diffs ()*) then - let doc = state.doc in - let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in - try - let o_pp = show_proof_diff_to_pp oproof in - let tokenize_string = Proof_diffs.tokenize_string in - let show_removed = Some removed in - Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp - with - | Proof.NoSuchGoal _ - | Option.IsNone -> n_pp - | Pp_diff.Diff_Failure msg -> begin - (* todo: print the unparsable string (if we know it) *) - Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut() - ++ str "Showing results without diff highlighting" ); - n_pp - end - else - n_pp - with - | Proof.NoSuchGoal _ - | Option.IsNone -> - CErrors.user_err (str "No goals to show.") + match state.proof with + | None -> CErrors.user_err (str "No proofs to diff.") + | Some proof -> + let old = Stm.get_prev_proof ~doc:state.doc state.sid in + Proof_diffs.diff_proofs ~diff_opt ?old proof let process_toplevel_command ~state stm = let open Vernac.State in @@ -444,12 +416,12 @@ let process_toplevel_command ~state stm = Feedback.msg_notice (v 0 (goal ++ evars)); state - | VernacShowProofDiffs removed -> + | VernacShowProofDiffs diff_opt -> (* We print nothing if there are no goals left *) if not (Proof_diffs.color_enabled ()) then CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") else - let out = show_proof_diff_cmd ~state removed in + let out = show_proof_diff_cmd ~state diff_opt in Feedback.msg_notice out; state diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 1902103a3e..ef79f4562e 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -20,7 +20,7 @@ type vernac_toplevel = | VernacQuit | VernacControl of vernac_control | VernacShowGoal of { gid : int; sid: int } - | VernacShowProofDiffs of bool + | VernacShowProofDiffs of Proof_diffs.diffOpt module Toplevel_ : sig val vernac_toplevel : vernac_toplevel option Entry.t @@ -52,7 +52,8 @@ GRAMMAR EXTEND Gram | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." -> { Some (VernacShowGoal {gid; sid}) } | IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." -> - { Some (VernacShowProofDiffs (removed <> None)) } + { Some (VernacShowProofDiffs + (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) } | cmd = Pvernac.Vernac_.main_entry -> { match cmd with | None -> None diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 732ad05b26..6fb5f821ee 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -72,6 +72,7 @@ let print_usage_common co command = \n -init-file f set the rcfile to f\ \n -bt print backtraces (requires configure debug flag)\ \n -debug debug mode (implies -bt)\ +\n -xml-debug debug mode and print XML messages to/from coqide\ \n -diffs (on|off|removed) highlight differences between proof steps\ \n -stm-debug STM debug mode (will trace every transaction)\ \n -noglob do not dump globalizations\ diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index b346b3ee5c..90f8008dc2 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -229,7 +229,7 @@ let check_pattern_id ?loc id = let pattern_vars pat = let rec aux () accu pat = match pat.CAst.v with | Constrexpr.CPatVar id - | Constrexpr.CEvar (id, []) -> + | Constrexpr.CEvar ({CAst.v=id}, []) -> let loc = pat.CAst.loc in let () = check_pattern_id ?loc id in Id.Map.add id loc accu diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 401ba0fba4..12194ea20c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -68,10 +68,12 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name let inst = instance_of_univ_entry univs in (gr,inst) -let interp_assumption ~program_mode sigma env impls c = +let interp_assumption ~program_mode env sigma impl_env bl c = let flags = { Pretyping.all_no_fail_flags with program_mode } in - let sigma, (ty, impls) = interp_type_evars_impls ~flags env sigma ~impls c in - sigma, (ty, impls) + let sigma, (impls, ((env_bl, ctx), impls1)) = interp_context_evars ~program_mode ~impl_env env sigma bl in + let sigma, (ty, impls2) = interp_type_evars_impls ~flags env_bl sigma ~impls c in + let ty = EConstr.it_mkProd_or_LetIn ty ctx in + sigma, ty, impls1@impls2 (* When monomorphic the universe constraints and universe names are declared with the first declaration only. *) @@ -153,7 +155,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = in (* We interpret all declarations in the same evar_map, i.e. as a telescope. *) let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> - let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in + let sigma,t,imps = interp_assumption ~program_mode env sigma ienv [] c in let r = Retyping.relevance_of_type env sigma t in let env = EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 3d425ad768..64b8212b90 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -14,6 +14,15 @@ open Constrexpr (** {6 Parameters/Assumptions} *) +val interp_assumption + : program_mode:bool + -> Environ.env + -> Evd.evar_map + -> Constrintern.internalization_env + -> Constrexpr.local_binder_expr list + -> constr_expr + -> Evd.evar_map * EConstr.t * Impargs.manual_implicits + val do_assumptions : program_mode:bool -> poly:bool diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 37b7106856..c1dbf0a1ea 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -81,14 +81,11 @@ let protect_pattern_in_binder bl c ctypopt = else (bl, c, ctypopt, fun f env evd c -> f env evd c) -let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = +let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt = let flags = Pretyping.{ all_no_fail_flags with program_mode } in - let env = Global.env() in - (* Explicitly bound universes and constraints *) - let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in let (bl, c, ctypopt, apply_under_binders) = protect_pattern_in_binder bl c ctypopt in (* Build the parameters *) - let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in + let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode ~impl_env env evd bl in (* Build the type *) let evd, tyopt = Option.fold_left_map (interp_type_evars_impls ~flags ~impls env_bl) @@ -111,12 +108,15 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = (* Declare the definition *) let c = EConstr.it_mkLambda_or_LetIn c ctx in let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in - (c, tyopt), evd, udecl, imps + evd, (c, tyopt), imps let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let program_mode = false in - let (body, types), evd, udecl, impargs = - interp_definition ~program_mode udecl bl ~poly red_option c ctypopt + let env = Global.env() in + (* Explicitly bound universes and constraints *) + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in + let evd, (body, types), impargs = + interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt in let kind = Decls.IsDefinition kind in let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in @@ -127,8 +127,11 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let program_mode = true in - let (body, types), evd, udecl, impargs = - interp_definition ~program_mode udecl bl ~poly red_option c ctypopt + let env = Global.env() in + (* Explicitly bound universes and constraints *) + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in + let evd, (body, types), impargs = + interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt in let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in let pm, _ = diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index d95e64a85f..7420235449 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -14,6 +14,17 @@ open Constrexpr (** {6 Definitions/Let} *) +val interp_definition + : program_mode:bool + -> Environ.env + -> Evd.evar_map + -> Constrintern.internalization_env + -> Constrexpr.local_binder_expr list + -> red_expr option + -> constr_expr + -> constr_expr option + -> Evd.evar_map * (EConstr.t * EConstr.t option) * Impargs.manual_implicits + val do_definition : ?hook:Declare.Hook.t -> name:Id.t diff --git a/vernac/declare.ml b/vernac/declare.ml index ae7878b615..5274a6da3b 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1854,7 +1854,8 @@ module MutualEntry : sig val declare_variable : pinfo:Proof_info.t -> uctx:UState.t - -> Entries.parameter_entry + -> sec_vars:Id.Set.t option + -> univs:Entries.universes_entry -> Names.GlobRef.t list val declare_mutdef @@ -1920,10 +1921,11 @@ end = struct in List.map_i (declare_mutdef ~pinfo ~uctx pe) 0 pinfo.Proof_info.cinfo - let declare_variable ~pinfo ~uctx pe = + let declare_variable ~pinfo ~uctx ~sec_vars ~univs = let { Info.scope; hook } = pinfo.Proof_info.info in List.map_i ( fun i { CInfo.name; typ; impargs } -> + let pe = (sec_vars, (typ, univs), None) in declare_assumption ~name ~scope ~hook ~impargs ~uctx pe ) 0 pinfo.Proof_info.cinfo @@ -1953,8 +1955,8 @@ let compute_proof_using_for_admitted proof typ pproofs = Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None -let finish_admitted ~pm ~pinfo ~uctx pe = - let cst = MutualEntry.declare_variable ~pinfo ~uctx pe in +let finish_admitted ~pm ~pinfo ~uctx ~sec_vars ~univs = + let cst = MutualEntry.declare_variable ~pinfo ~uctx ~sec_vars ~univs in (* If the constant was an obligation we need to update the program map *) match CEphemeron.get pinfo.Proof_info.proof_ending with | Proof_ending.End_obligation oinfo -> @@ -1974,7 +1976,7 @@ let save_admitted ~pm ~proof = let sec_vars = compute_proof_using_for_admitted proof typ pproofs in let uctx = get_initial_euctx proof in let univs = UState.check_univ_decl ~poly uctx udecl in - finish_admitted ~pm ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None) + finish_admitted ~pm ~pinfo:proof.pinfo ~uctx ~sec_vars ~univs (************************************************************************) (* Saving a lemma-like constant *) @@ -2097,12 +2099,9 @@ let save_lemma_admitted_delayed ~pm ~proof ~pinfo = let poly = match proof_entry_universes with | Entries.Monomorphic_entry _ -> false | Entries.Polymorphic_entry (_, _) -> true in - let typ = match proof_entry_type with - | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement"); - | Some typ -> typ in - let ctx = UState.univ_entry ~poly uctx in + let univs = UState.univ_entry ~poly uctx in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted ~pm ~uctx ~pinfo (sec_vars, (typ, ctx), None) + finish_admitted ~pm ~uctx ~pinfo ~sec_vars ~univs let save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt = (* vio2vo calls this but with invalid info, we have to workaround diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 49d4847fde..dfc7b05b51 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -429,19 +429,19 @@ GRAMMAR EXTEND Gram ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; - t = lconstr -> { fun id -> (oc,AssumExpr (id,mkProdCN ~loc l t)) } + t = lconstr -> { fun id -> (oc,AssumExpr (id,l,t)) } | l = binders; oc = of_type_with_opt_coercion; t = lconstr; ":="; b = lconstr -> { fun id -> - (oc,DefExpr (id,mkLambdaCN ~loc l b,Some (mkProdCN ~loc l t))) } + (oc,DefExpr (id,l,b,Some t)) } | l = binders; ":="; b = lconstr -> { fun id -> match b.CAst.v with | CCast(b', (CastConv t|CastVM t|CastNative t)) -> - (NoInstance,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t))) + (NoInstance,DefExpr(id,l,b',Some t)) | _ -> - (NoInstance,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ] + (NoInstance,DefExpr(id,l,b,None)) } ] ] ; record_binder: - [ [ id = name -> { (NoInstance,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) } + [ [ id = name -> { (NoInstance,AssumExpr(id, [], CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) } | id = name; f = record_binder_body -> { f id } ] ] ; assum_list: diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a9de01bfd0..5f7eb78a40 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -866,7 +866,7 @@ let explain_unsatisfiable_constraints env sigma constr comp = let info = Evar.Map.find ev undef in explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr -let explain_pretype_error env sigma err = +let rec explain_pretype_error env sigma err = let env = Evardefine.env_nf_betaiotaevar sigma env in let env = make_all_name_different env sigma in match err with @@ -893,7 +893,7 @@ let explain_pretype_error env sigma err = | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n | CannotFindWellTypedAbstraction (p,l,e) -> explain_cannot_find_well_typed_abstraction env sigma p l - (Option.map (fun (env',e) -> explain_type_error env' sigma e) e) + (Option.map (fun (env',e) -> explain_pretype_error env' sigma e) e) | WrongAbstractionType (n,a,t,u) -> explain_wrong_abstraction_type env sigma n a t u | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 58b1698848..8ce59c40c3 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1165,11 +1165,6 @@ let warn_non_reversible_notation = str " not occur in the right-hand side." ++ spc() ++ strbrk "The notation will not be used for printing as it is not reversible.") -type entry_coercion_kind = - | IsEntryCoercion of notation_entry_level - | IsEntryGlobal of string * int - | IsEntryIdent of string * int - let is_coercion level typs = match level, typs with | Some (custom,n,_), [e] -> @@ -1417,8 +1412,7 @@ type notation_obj = { notobj_scope : scope_name option; notobj_interp : interpretation; notobj_coercion : entry_coercion_kind option; - notobj_onlyparse : bool; - notobj_onlyprint : bool; + notobj_use : notation_use option; notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; notobj_specific_pp_rules : syntax_printing_extension option; @@ -1442,37 +1436,19 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - let onlyprint = nobj.notobj_onlyprint in let deprecation = nobj.notobj_deprecation in - let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in - let specific_ntn = (specific,ntn) in - let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in - if fresh then begin - (* Declare the interpretation *) - let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in - (* Declare the uninterpretation *) - if not nobj.notobj_onlyparse then - Notation.declare_uninterpretation (NotationRule specific_ntn) pat; - (* Declare a possible coercion *) - (match nobj.notobj_coercion with - | Some (IsEntryCoercion entry) -> - let (_,level,_) = Notation.level_of_notation ntn in - let level = match fst ntn with - | InConstrEntry -> None - | InCustomEntry _ -> Some level - in - Notation.declare_entry_coercion specific_ntn level entry - | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n - | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n - | None -> ()) - end; + let scope = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in + (* Declare the notation *) + (match nobj.notobj_use with + | Some use -> Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation + | None -> ()); (* Declare specific format if any *) - match nobj.notobj_specific_pp_rules with + (match nobj.notobj_specific_pp_rules with | Some pp_sy -> - if specific_format_to_declare specific_ntn pp_sy then + if specific_format_to_declare (scope,ntn) pp_sy then Ppextend.declare_specific_notation_printing_rules - specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing - | None -> () + (scope,ntn) ~extra:pp_sy.synext_extra pp_sy.synext_unparsing + | None -> ()) end let cache_notation o = @@ -1602,6 +1578,20 @@ let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in synext_extra = sd.extra; } +let warn_unused_interpretation = + CWarnings.create ~name:"unused-notation" ~category:"parsing" + (fun b -> + strbrk "interpretation is used neither for printing nor for parsing, " ++ + (if b then strbrk "the declaration could be replaced by \"Reserved Notation\"." + else strbrk "the declaration could be removed.")) + +let make_use reserved onlyparse onlyprint = + match onlyparse, onlyprint with + | false, false -> Some ParsingAndPrinting + | true, false -> Some OnlyParsing + | false, true -> Some OnlyPrinting + | true, true -> warn_unused_interpretation reserved; None + (**********************************************************************) (* Main functions about notations *) @@ -1633,14 +1623,14 @@ let add_notation_in_scope ~local deprecation df env c mods scope = let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in let notation, location = sd.info in + let use = make_use true onlyparse sd.only_printing in let notation = { notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); (* Order is important here! *) - notobj_onlyparse = onlyparse; + notobj_use = use; notobj_coercion = coe; - notobj_onlyprint = sd.only_printing; notobj_deprecation = sd.deprecation; notobj_notation = (notation, location); notobj_specific_pp_rules = sy_pp_rules; @@ -1676,14 +1666,14 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization let interp = make_interpretation_vars recvars plevel acvars (List.combine mainvars i_typs) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse,coe = printability level i_typs onlyparse reversibility ac in + let use = make_use false onlyparse onlyprint in let notation = { notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); (* Order is important here! *) - notobj_onlyparse = onlyparse; + notobj_use = use; notobj_coercion = coe; - notobj_onlyprint = onlyprint; notobj_deprecation = deprecation; notobj_notation = df'; notobj_specific_pp_rules = pp_sy; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f972e05d3b..0e660bf20c 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -508,13 +508,15 @@ let pr_oc = function let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) = let prx = match x with - | AssumExpr (id,t) -> + | AssumExpr (id,binders,t) -> hov 1 (pr_lname id ++ + pr_binders_arg binders ++ spc() ++ pr_oc oc ++ spc() ++ pr_lconstr_expr t) - | DefExpr(id,b,opt) -> (match opt with + | DefExpr(id,binders,b,opt) -> (match opt with | Some t -> hov 1 (pr_lname id ++ + pr_binders_arg binders ++ spc() ++ pr_oc oc ++ spc() ++ pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) | None -> @@ -524,8 +526,7 @@ let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = n prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr) ntn let pr_record_decl c fs = - pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") + pr_opt pr_lident c ++ pr_record "{" "}" pr_record_field fs let pr_printable = function | PrintFullContext -> @@ -966,7 +967,7 @@ let pr_vernac_expr v = str":" ++ spc () ++ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with - | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ pr_record_body "{" "}" pr_lconstr l | Some (true,_) -> assert false | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) diff --git a/vernac/record.ml b/vernac/record.ml index e362cb052a..a4bf9893d9 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -62,23 +62,33 @@ let () = let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = let _, sigma, impls, newfs, _ = List.fold_left2 - (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) -> - let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in - let r = Retyping.relevance_of_type env sigma t' in - let sigma, b' = - Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@ - interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in - let impls = + (fun (env, sigma, uimpls, params, impls_env) no d -> + let sigma, (i, b, t), impl = match d with + | Vernacexpr.AssumExpr({CAst.loc;v=id},bl,t) -> + (* Temporary compatibility with the type-classes heuristics *) + (* which are applied after the interpretation of bl and *) + (* before the one of t otherwise (see #13166) *) + let t = if bl = [] then t else mkCProdN bl t in + let sigma, t, impl = + ComAssumption.interp_assumption ~program_mode:false env sigma impls_env [] t in + sigma, (id, None, t), impl + | Vernacexpr.DefExpr({CAst.loc;v=id},bl,b,t) -> + let sigma, (b, t), impl = + ComDefinition.interp_definition ~program_mode:false env sigma impls_env bl None b t in + let t = match t with Some t -> t | None -> Retyping.get_type_of env sigma b in + sigma, (id, Some b, t), impl in + let r = Retyping.relevance_of_type env sigma t in + let impls_env = match i with - | Anonymous -> impls - | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t' impl) impls + | Anonymous -> impls_env + | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t impl) impls_env in - let d = match b' with - | None -> LocalAssum (make_annot i r,t') - | Some b' -> LocalDef (make_annot i r,b',t') + let d = match b with + | None -> LocalAssum (make_annot i r,t) + | Some b -> LocalDef (make_annot i r,b,t) in - List.iter (Metasyntax.set_notation_for_interpretation env impls) no; - (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls)) + List.iter (Metasyntax.set_notation_for_interpretation env impls_env) no; + (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls_env)) (env, sigma, [], [], impls_env) nots l in let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) -> @@ -101,14 +111,6 @@ let compute_constructor_level evars env l = in (EConstr.push_rel d env, univ)) l (env, Univ.Universe.sprop) -let binder_of_decl = function - | Vernacexpr.AssumExpr(n,t) -> (n,None,t) - | Vernacexpr.DefExpr(n,c,t) -> - (n,Some c, match t with Some c -> c - | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Namegen.IntroAnonymous, None)) - -let binders_of_decls = List.map binder_of_decl - let check_anonymous_type ind = match ind with | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true @@ -176,7 +178,7 @@ let typecheck_params_and_fields def poly pl ps records = let ninds = List.length arities in let nparams = List.length newps in let fold sigma (_, _, nots, fs) arity = - interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots (binders_of_decls fs) + interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots fs in let (sigma, data) = List.fold_left2_map fold sigma records arities in let sigma = @@ -676,8 +678,8 @@ open Vernacexpr let check_unique_names records = let extract_name acc (rf_decl, _) = match rf_decl with - Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc - | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc + Vernacexpr.AssumExpr({CAst.v=Name id},_,_) -> id::acc + | Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc | _ -> acc in let allnames = List.fold_left (fun acc (_, id, _, cfs, _, _) -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index fe27d9ac8a..3ced38d6ea 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -700,7 +700,7 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records = if Dumpglob.dump () then let () = Dumpglob.dump_definition id false "rec" in let iter (x, _) = match x with - | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> + | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) -> Dumpglob.dump_definition (make ?loc id) false "proj" | _ -> () in @@ -777,7 +777,7 @@ let vernac_inductive ~atts kind indl = in let (coe, (lid, ce)) = l in let coe' = if coe then BackInstance else NoInstance in - let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), + let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce), { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then @@ -1790,11 +1790,11 @@ let vernac_print ~pstate = | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s | PrintHintDb -> Hints.pr_searchtable env sigma | PrintScopes -> - Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)) + Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env)) | PrintScope s -> - Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s + Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env)) s | PrintVisibility s -> - Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s + Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env)) s | PrintAbout (ref_or_by_not,udecl,glnumopt) -> print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt | PrintImplicit qid -> @@ -1830,7 +1830,7 @@ let vernac_locate ~pstate = let open Constrexpr in function | LocateTerm {v=ByNotation (ntn, sc)} -> let _, env = get_current_or_global_context ~pstate in Notation.locate_notation - (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc + (Constrextern.without_symbols (pr_glob_constr_env env)) ntn sc | LocateLibrary qid -> print_located_library qid | LocateModule qid -> Prettyp.print_located_module qid | LocateOther (s, qid) -> Prettyp.print_located_other s qid diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index eeebb43114..6a9a74144f 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -167,8 +167,8 @@ type fixpoint_expr = recursion_order_expr option fix_expr_gen type cofixpoint_expr = unit fix_expr_gen type local_decl_expr = - | AssumExpr of lname * constr_expr - | DefExpr of lname * constr_expr * constr_expr option + | AssumExpr of lname * local_binder_expr list * constr_expr + | DefExpr of lname * local_binder_expr list * constr_expr * constr_expr option type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) type simple_binder = lident list * constr_expr |
