diff options
55 files changed, 1481 insertions, 321 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3c427793e2..3c24ec28c4 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -47,9 +47,6 @@ before_script: - opam list - opam config list -after_script: - - echo "The build completed normally (not a runner failure)." - ################ GITLAB CACHING ###################### # - use artifacts between jobs # ###################################################### @@ -662,5 +659,5 @@ plugin:plugin-tutorial: plugin:ci-quickchick: extends: .ci-template-flambda -plugin:ci-relation-algebra: +plugin:ci-relation_algebra: extends: .ci-template diff --git a/CHANGES.md b/CHANGES.md index fc7272da65..2f58bfb825 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -22,6 +22,9 @@ Coqide - CoqIDE now properly sets the module name for a given file based on its path, see -topfile change entry for more details. +- Preferences from coqide.keys are no longer overridden by modifiers + preferences in coqiderc. + Coqtop - the use of `coqtop` as a compiler has been deprecated, in favor of @@ -290,12 +293,22 @@ Misc SSReflect +- New tactic `under` to rewrite under binders, given an extensionality lemma: + - interactive mode: `under lem`, associated terminator: `over` + - one-liner mode: `under lem do [tac1 | ...]` + + It can take occurrence switches, contextual patterns, and intro patterns: + `under {2}[in RHS]eq_big => [i|i ?] do ...`. + + See the reference manual for the actual documentation. + - New intro patterns: - temporary introduction: `=> +` - block introduction: `=> [^ prefix ] [^~ suffix ]` - fast introduction: `=> >` - tactics as views: `=> /ltac:mytac` - replace hypothesis: `=> {}H` + See the reference manual for the actual documentation. - Clear discipline made consistent across the entire proof language. diff --git a/META.coq.in b/META.coq.in index ab142ccc43..ef5de8da2b 100644 --- a/META.coq.in +++ b/META.coq.in @@ -315,7 +315,7 @@ package "plugins" ( archive(native) = "micromega_plugin.cmx" ) - package "newring" ( + package "setoid_ring" ( description = "Coq newring plugin" version = "8.10" @@ -351,7 +351,7 @@ package "plugins" ( archive(native) = "cc_plugin.cmx" ) - package "ground" ( + package "firstorder" ( description = "Coq ground plugin" version = "8.10" @@ -387,7 +387,7 @@ package "plugins" ( archive(native) = "btauto_plugin.cmx" ) - package "recdef" ( + package "funind" ( description = "Coq recdef plugin" version = "8.10" diff --git a/Makefile.ci b/Makefile.ci index 000725b6b1..a244c17ef3 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -38,7 +38,7 @@ CI_TARGETS= \ ci-mtac2 \ ci-paramcoq \ ci-quickchick \ - ci-relation-algebra \ + ci-relation_algebra \ ci-sf \ ci-simple-io \ ci-stdlib2 \ diff --git a/Makefile.doc b/Makefile.doc index e89a20393c..23aa66a1b8 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -31,8 +31,8 @@ DVIPS:=dvips HTMLSTYLE:=coqremote # Sphinx-related variables -OSNAME:=$(shell uname -o) -ifeq ($(OSNAME),Cygwin) +OSNAME:=$(shell uname -s) +ifeq ($(findstring CYGWIN,$(OSNAME)),CYGWIN) WIN_CURDIR:=$(shell cygpath -w $(CURDIR)) SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)" else diff --git a/Makefile.ide b/Makefile.ide index 8f9088a04a..4cec7aa443 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -68,6 +68,7 @@ GTKBIN=$(shell pkg-config --variable=prefix gtk+-3.0)/bin GTKLIBS=$(shell pkg-config --variable=libdir gtk+-3.0) PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-2.0)/bin SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-3.0)/share +ADWAITASHARE=$(shell ls -d /usr/local/Cellar/adwaita-icon-theme/*)/share ########################################################################### # CoqIde special targets @@ -255,6 +256,9 @@ $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/styles/{styles.rng,classic.xml} $@/gtksourceview-3.0/styles/ cp -R "$(GTKSHARE)/"locale $@ cp -R "$(GTKSHARE)/"themes $@ + $(MKDIR) $@/glib-2.0/schemas + glib-compile-schemas --targetdir=$@/glib-2.0/schemas "$(GTKSHARE)/"glib-2.0/schemas/ + cp -R "$(ADWAITASHARE)/"icons $@ $(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents $(MKDIR) $@ diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 6fcc64f77e..f09087b172 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -52,7 +52,7 @@ jobs: - script: | set -e brew update - brew install gnu-time opam pkg-config gtksourceview3 + brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme pip3 install macpack displayName: 'Install system dependencies' diff --git a/coq-refman.opam b/coq-refman.opam index b9500243a3..16be422c27 100644 --- a/coq-refman.opam +++ b/coq-refman.opam @@ -17,7 +17,7 @@ license: "Open Publication License" depends: [ "dune" { build } - "coq" { build } + "coq" { build & = version } ] build-env: [ @@ -20,7 +20,7 @@ license: "LGPL-2.1" depends: [ "ocaml" { >= "4.05.0" } - "dune" { build & >= "1.4.0" } + "dune" { build & >= "1.6.0" } "ocamlfind" { build } "num" ] diff --git a/coqide-server.opam b/coqide-server.opam index ed6f3d98d8..0325d2549c 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -19,8 +19,8 @@ dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" depends: [ - "dune" { build & >= "1.4.0" } - "coq" + "dune" { build & >= "1.6.0" } + "coq" { = version } ] build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/coqide.opam b/coqide.opam index c82fa72564..2507acbb26 100644 --- a/coqide.opam +++ b/coqide.opam @@ -17,8 +17,8 @@ dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" depends: [ - "dune" { build & >= "1.4.0" } - "coqide-server" + "dune" { build & >= "1.6.0" } + "coqide-server" { = version } "lablgtk3" { >= "3.0.beta5" } "lablgtk3-sourceview3" { >= "3.0.beta5" } ] diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 01769aeddb..06b617d4c1 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -45,6 +45,26 @@ using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is to give merge permissions to someone from the Coq team as to help with these kind of merges. +### OCaml and plugin-specific considerations + +Developments that link against Coq's OCaml API [most of them are known +as "plugins"] do have some special requirements: + +- Coq's OCaml API is not stable. We hope to improve this in the future + but as of today you should expect to have to merge a fair amount of + "overlays", usually in the form of Pull Requests from Coq developers + in order to keep your plugin compatible with Coq master. + + In order to alleviate the load, you can delegate the merging of such + compatibility pull requests to Coq developers themselves, by + granting access to the plugin repository or by using `bots` such as + [Bors](https://github.com/apps/bors) that allow for automatic + management of Pull Requests. + +- Plugins in the CI should compile with the OCaml flags that Coq + uses. In particular, warnings that are considered fatal by the Coq + developers _must_ be also fatal for plugin CI code. + ### Add your development by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 0c89809ee9..4f5988c59c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -254,7 +254,7 @@ : "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" ######################################################################## -# relation-algebra +# relation_algebra ######################################################################## : "${relation_algebra_CI_REF:=master}" : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" diff --git a/dev/ci/ci-relation-algebra.sh b/dev/ci/ci-relation_algebra.sh index 84bed5bdfe..84bed5bdfe 100755 --- a/dev/ci/ci-relation-algebra.sh +++ b/dev/ci/ci-relation_algebra.sh diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 40c3c32e4f..4533a4dc01 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -20,6 +20,15 @@ General deprecation removed. Please, make sure your plugin is warning-free in 8.8 before trying to port it over 8.9. +Warnings + +- Coq now builds plugins with `-warn-error` enabled by default. The + amount of dangerous warnings in plugin code was very high, so we now + require plugins in the CI to adhere to the Coq warning policy. We + _strongly_ recommend against disabling the default set of warnings. + If you have special needs, see the documentation of your build + system and/or OCaml for further help. + Names - Kernel names no longer contain a section path. They now have only two diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index f532e1b68f..01c2b574a2 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -195,6 +195,18 @@ Conversion machines GH issue number: ? risk: + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: primitive integer emulation layer on 32 bits not robust to garbage collection + introduced: master (before v8.10 in GH pull request #6914) + impacted released versions: none + impacted development branches: + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: + found by: Roux, Melquiond + exploit: + GH issue number: #9925 + risk: + component: "native" conversion machine (translation to OCaml which compiles to native code) summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False introduced: V8.5 diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 74be300134..816316487c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -65,6 +65,7 @@ let get_current_context () = with Vernacstate.Proof_global.NoCurrentProof -> let env = Global.env() in Evd.from_env env, env + [@@ocaml.warning "-3"] (* term printers *) let envpp pp = let sigma,env = get_current_context () in pp env sigma diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index b069cf27f4..a5e9023732 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -433,22 +433,26 @@ few other commands related to typeclasses. .. _TypeclassesTransparent: -Typeclasses Transparent, Typclasses Opaque -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Typeclasses Transparent, Typeclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses Transparent {+ @ident} This command makes the identifiers transparent during typeclass resolution. + Shortcut for :n:`Hint Transparent {+ @ident } : typeclass_instances`. .. cmd:: Typeclasses Opaque {+ @ident} - Make the identifiers opaque for typeclass search. It is useful when some - constants prevent some unifications and make resolution fail. It is also - useful to declare constants which should never be unfolded during - proof-search, like fixpoints or anything which does not look like an - abbreviation. This can additionally speed up proof search as the typeclass - map can be indexed by such rigid constants (see + Make the identifiers opaque for typeclass search. + Shortcut for :n:`Hint Opaque {+ @ident } : typeclass_instances`. + + It is useful when some constants prevent some unifications and make + resolution fail. It is also useful to declare constants which + should never be unfolded during proof-search, like fixpoints or + anything which does not look like an abbreviation. This can + additionally speed up proof search as the typeclass map can be + indexed by such rigid constants (see :ref:`thehintsdatabasesforautoandeauto`). By default, all constants and local variables are considered transparent. One @@ -458,8 +462,6 @@ type, like: .. coqdoc:: Definition relation A := A -> A -> Prop. -This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. - Settings ~~~~~~~~ diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 8346b72cb9..35231610fe 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -144,6 +144,10 @@ Here we describe only few of them. :CAMLFLAGS: can be used to specify additional flags to the |OCaml| compiler, like ``-bin-annot`` or ``-w``.... +:OCAMLWARN: + it contains a default of ``-warn-error +a-3``, useful to modify + this setting; beware this is not recommended for projects in + Coq's CI. :COQC, COQDEP, COQDOC: can be set in order to use alternative binaries (e.g. wrappers) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b240cef40c..4e40df6f94 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1737,9 +1737,8 @@ Intro patterns for each :token:`ident`. Its type has to be fixed later on by using the ``abstract`` tactic. Before then the type displayed is ``<hidden>``. - Note that |SSR| does not support the syntax ``(ipat, …, ipat)`` for -destructing intro-patterns. +destructing intro patterns. Clear switch ```````````` @@ -3626,7 +3625,7 @@ corresponding new goals will be generated. As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to solve the existential variable. - .. coqtop:: all + .. coqtop:: all abort Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. rewrite insubT. @@ -3637,6 +3636,272 @@ rewriting rule is stated using Leibniz equality (as opposed to setoid relations). It will be extended to other rewriting relations in the future. +.. _under_ssr: + +Rewriting under binders +~~~~~~~~~~~~~~~~~~~~~~~ + +Goals involving objects defined with higher-order functions often +require "rewriting under binders". While setoid rewriting is a +possible approach in this case, it is common to use regular rewriting +along with dedicated extensionality lemmas. This may cause some +practical issues during the development of the corresponding scripts, +notably as we might be forced to provide the rewrite tactic with +complete terms, as shown by the simple example below. + +.. example:: + + .. coqtop:: reset none + + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + + .. coqtop:: in + + Axiom subnn : forall n : nat, n - n = 0. + Parameter map : (nat -> nat) -> list nat -> list nat. + Parameter sumlist : list nat -> nat. + Axiom eq_map : + forall F1 F2 : nat -> nat, + (forall n : nat, F1 n = F2 n) -> + forall l : list nat, map F1 l = map F2 l. + + .. coqtop:: all + + Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + + In this context, one cannot directly use ``eq_map``: + + .. coqtop:: all fail + + rewrite eq_map. + + as we need to explicitly provide the non-inferable argument ``F2``, + which corresponds here to the term we want to obtain *after* the + rewriting step. In order to perform the rewrite step one has to + provide the term by hand as follows: + + .. coqtop:: all abort + + rewrite (@eq_map _ (fun _ : nat => 0)). + by move=> m; rewrite subnn. + + The :tacn:`under` tactic lets one perform the same operation in a more + convenient way: + + .. coqtop:: all abort + + Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + under eq_map => m do rewrite subnn. + + +The under tactic +```````````````` + +The convenience :tacn:`under` tactic supports the following syntax: + +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] ) } + :name: under + + Operate under the context proved to be extensional by + lemma :token:`term`. + + .. exn:: Incorrect number of tactics (expected N tactics, was given M). + + This error can occur when using the version with a ``do`` clause. + + The multiplier part of :token:`r_prefix` is not supported. + +We distinguish two modes, +:ref:`interactive mode <under_interactive>` without a ``do`` clause, and +:ref:`one-liner mode <under_one_liner>` with a ``do`` clause, +which are explained in more detail below. + +.. _under_interactive: + +Interactive mode +```````````````` + +Let us redo the running example in interactive mode. + +.. example:: + + .. coqtop:: all abort + + Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + under eq_map => m. + rewrite subnn. + over. + +The execution of the Ltac expression: + +:n:`under @term => [ @i_item__1 | … | @i_item__n ].` + +involves the following steps: + +1. It performs a :n:`rewrite @term` + without failing like in the first example with ``rewrite eq_map.``, + but creating evars (see :tacn:`evar`). If :n:`term` is prefixed by + a pattern or an occurrence selector, then the modifiers are honoured. + +2. As a n-branches intro pattern is provided :tacn:`under` checks that + n+1 subgoals have been created. The last one is the main subgoal, + while the other ones correspond to premises of the rewrite rule (such as + ``forall n, F1 n = F2 n`` for ``eq_map``). + +3. If so :tacn:`under` puts these n goals in head normal form (using + the defective form of the tactic :tacn:`move`), then executes + the corresponding intro pattern :n:`@ipat__i` in each goal. + +4. Then :tacn:`under` checks that the first n subgoals + are (quantified) equalities or double implications between a + term and an evar (e.g. ``m - m = ?F2 m`` in the running example). + +5. If so :tacn:`under` protects these n goals against an + accidental instantiation of the evar. + These protected goals are displayed using the ``Under[ … ]`` + notation (e.g. ``Under[ m - m ]`` in the running example). + +6. The expression inside the ``Under[ … ]`` notation can be + proved equivalent to the desired expression + by using a regular :tacn:`rewrite` tactic. + +7. Interactive editing of the first n goals has to be signalled by + using the :tacn:`over` tactic or rewrite rule (see below). + +8. Finally, a post-processing step is performed in the main goal + to keep the name(s) for the bound variables chosen by the user in + the intro pattern for the first branch. + +.. _over_ssr: + +The over tactic ++++++++++++++++ + +Two equivalent facilities (a terminator and a lemma) are provided to +close intermediate subgoals generated by :tacn:`under` (i.e. goals +displayed as ``Under[ … ]``): + +.. tacn:: over + :name: over + + This terminator tactic allows one to close goals of the form + ``'Under[ … ]``. + +.. tacv:: by rewrite over + + This is a variant of :tacn:`over` in order to close ``Under[ … ]`` + goals, relying on the ``over`` rewrite rule. + +.. _under_one_liner: + +One-liner mode +`````````````` + +The Ltac expression: + +:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tac__1 | … | @tac__n ].` + +can be seen as a shorter form for the following expression: + +:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].` + +Notes: + ++ The ``beta-iota`` reduction here is useful to get rid of the beta + redexes that could be introduced after the substitution of the evars + by the :tacn:`under` tactic. + ++ Note that the provided tactics can as well + involve other :tacn:`under` tactics. See below for a typical example + involving the `bigop` theory from the Mathematical Components library. + ++ If there is only one tactic, the brackets can be omitted, e.g.: + :n:`under @term => i do @tac.` and that shorter form should be + preferred. + ++ If the ``do`` clause is provided and the intro pattern is omitted, + then the default :token:`i_item` ``*`` is applied to each branch. + E.g., the Ltac expression: + :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to: + :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]` + (and it can be noted here that the :tacn:`under` tactic performs a + ``move.`` before processing the intro patterns ``=> [ * | … | * ]``). + +.. example:: + + .. coqtop:: reset none + + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + + Coercion is_true : bool >-> Sortclass. + + Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" + (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50, + format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'"). + Variant bigbody (R I : Type) : Type := + BigBody : forall (_ : I) (_ : forall (_ : R) (_ : R), R) (_ : bool) (_ : R), bigbody R I. + + Parameter bigop : + forall (R I : Type) (_ : R) (_ : list I) (_ : forall _ : I, bigbody R I), R. + + Axiom eq_bigr_ : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P : I -> bool) (F1 F2 : I -> R), + (forall x : I, is_true (P x) -> F1 x = F2 x) -> + bigop idx r (fun i : I => BigBody i op (P i) (F1 i)) = + bigop idx r (fun i : I => BigBody i op (P i) (F2 i)). + + Axiom eq_big_ : + forall (R : Type) (idx : R) (op : R -> R -> R) (I : Type) (r : list I) + (P1 P2 : I -> bool) (F1 F2 : I -> R), + (forall x : I, P1 x = P2 x) -> + (forall i : I, is_true (P1 i) -> F1 i = F2 i) -> + bigop idx r (fun i : I => BigBody i op (P1 i) (F1 i)) = + bigop idx r (fun i : I => BigBody i op (P2 i) (F2 i)). + + Reserved Notation "\sum_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'"). + + Parameter index_iota : nat -> nat -> list nat. + + Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" := + (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%bool F)). + + Notation "\sum_ ( m <= i < n | P ) F" := + (\big[plus/O]_(m <= i < n | P%bool) F%nat). + + Notation eq_bigr := (fun n m => eq_bigr_ 0 plus (index_iota n m)). + Notation eq_big := (fun n m => eq_big_ 0 plus (index_iota n m)). + + Parameter odd : nat -> bool. + Parameter prime : nat -> bool. + + .. coqtop:: in + + Parameter addnC : forall m n : nat, m + n = n + m. + Parameter muln1 : forall n : nat, n * 1 = n. + + .. coqtop:: all + + Check eq_bigr. + Check eq_big. + + Lemma test_big_nested (m n : nat) : + \sum_(0 <= a < m | prime a) \sum_(0 <= j < n | odd (j * 1)) (a + j) = + \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i). + under eq_bigr => i prime_i do + under eq_big => [ j | j odd_j ] do + [ rewrite (muln1 j) | rewrite (addnC i j) ]. + + Remark how the final goal uses the name ``i`` (the name given in the + intro pattern) rather than ``a`` in the binder of the first summation. .. _locking_ssr: @@ -5373,7 +5638,15 @@ respectively. .. tacn:: rewrite {+ @r_step } - rewrite (see :ref:`rewriting_ssr`) + rewrite (see :ref:`rewriting_ssr`) + +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] )} + + under (see :ref:`under_ssr`) + +.. tacn:: over + + over (see :ref:`over_ssr`) .. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index afb0239be4..8d9e99b9d5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3830,25 +3830,25 @@ The general command to add a hint to some databases :n:`{+ @ident}` is check with :cmd:`Print HintDb` to verify the current cut expression: .. productionlist:: regexp - e : `ident` hint or instance identifier - : _ any hint - : `e` | `e` disjunction - : `e` `e` sequence - : `e` * Kleene star - : emp empty - : eps epsilon - : ( `e` ) + regexp : `ident` (hint or instance identifier) + : _ (any hint) + : `regexp` | `regexp` (disjunction) + : `regexp` `regexp` (sequence) + : `regexp` * (Kleene star) + : emp (empty) + : eps (epsilon) + : ( `regexp` ) The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note that Hint Extern’s do not have + list of identifiers for the hints (note that :cmd:`Hint Extern`\’s do not have an associated identifier). Before applying any hint :n:`@ident` the current path `p` extended with :n:`@ident` is matched against the current cut expression `c` associated to the hint database. If matching succeeds, the hint is *not* applied. The - semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the - initial cut expression being `emp`. + semantics of :n:`Hint Cut @regexp` is to set the cut expression + to :n:`c | regexp`, the initial cut expression being `emp`. .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident :name: Hint Mode @@ -3875,7 +3875,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. note:: One can use an ``Extern`` hint with no pattern to do pattern matching on - hypotheses using ``match goal`` with inside the tactic. + hypotheses using ``match goal with`` inside the tactic. Hint databases defined in the Coq standard library @@ -4724,6 +4724,12 @@ Non-logical tactics from the shelf into focus, by appending them to the end of the current list of focused goals. +.. tacn:: unshelve @tactic + :name: unshelve + + Performs :n:`@tactic`, then unshelves existential variables added to the + shelf by the execution of :n:`@tactic`, prepending them to the current goal. + .. tacn:: give_up :name: give_up diff --git a/ide/.merlin.in b/ide/.merlin.in index 4dc6f45550..b8d7953833 100644 --- a/ide/.merlin.in +++ b/ide/.merlin.in @@ -1,4 +1,4 @@ -PKG unix laglgtk2 lablgtk2.sourceview2 +PKG unix laglgtk3 lablgtk3-sourceview3 S utils B utils diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang index bd9cb4bfa2..fc7bc64a68 100644 --- a/ide/coq-ssreflect.lang +++ b/ide/coq-ssreflect.lang @@ -73,11 +73,13 @@ <keyword>suffices</keyword> <keyword>suff</keyword> <keyword>transitivity</keyword> + <keyword>under</keyword> <keyword>without loss</keyword> <keyword>wlog</keyword> </context> <context id="ssr-endtac" style-ref="endtactic"> <keyword>by</keyword> + <keyword>over</keyword> <keyword>exact</keyword> <keyword>reflexivity</keyword> </context> diff --git a/ide/idetop.ml b/ide/idetop.ml index 543ff924bd..38839f3488 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -238,7 +238,8 @@ let goals () = Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp)) end else Some (export_pre_goals Proof.(data newp) process_goal) - with Vernacstate.Proof_global.NoCurrentProof -> None;; + with Vernacstate.Proof_global.NoCurrentProof -> None + [@@ocaml.warning "-3"];; let evars () = try @@ -251,6 +252,7 @@ let evars () = let el = List.map map_evar exl in Some el with Vernacstate.Proof_global.NoCurrentProof -> None + [@@ocaml.warning "-3"] let hints () = try @@ -264,7 +266,7 @@ let hints () = let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in Some (hint_hyps, concl_next_tac) with Vernacstate.Proof_global.NoCurrentProof -> None - + [@@ocaml.warning "-3"] (** Other API calls *) @@ -297,6 +299,7 @@ let status force = Interface.status_allproofs = allproofs; Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); } + [@@ocaml.warning "-3"] let export_coq_object t = { Interface.coq_object_prefix = t.Search.coq_object_prefix; @@ -340,6 +343,7 @@ let search flags = List.map export_coq_object (Search.interface_search ?pstate ( List.map (fun (c, b) -> (import_search_constraint c, b)) flags) ) + [@@ocaml.warning "-3"] let export_option_value = function | Goptions.BoolValue b -> Interface.BoolValue b diff --git a/ide/preferences.ml b/ide/preferences.ml index 47cd4c58b6..3893d023bd 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -263,8 +263,6 @@ let get_unicode_bindings_default_file () = (** Hooks *) -(** New style preferences *) - let cmd_coqtop = new preference ~name:["cmd_coqtop"] ~init:None ~repr:Repr.(option string) @@ -645,8 +643,6 @@ let tag_button () = let box = GPack.hbox () in new tag_button (Gobject.unsafe_cast box#as_widget) -(** Old style preferences *) - let save_pref () = if not (Sys.file_exists (Minilib.coqide_config_home ())) then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; @@ -658,15 +654,18 @@ let save_pref () = Config_lexer.print_file pref_file prefs let load_pref () = + (* Load main preference file *) + let () = + let m = Config_lexer.load_file loaded_pref_file in + let iter name v = + if Util.String.Map.mem name !preferences then + try (Util.String.Map.find name !preferences).set v with _ -> () + else unknown_preferences := Util.String.Map.add name v !unknown_preferences + in + Util.String.Map.iter iter m in + (* Load file for bindings *) let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in - - let m = Config_lexer.load_file loaded_pref_file in - let iter name v = - if Util.String.Map.mem name !preferences then - try (Util.String.Map.find name !preferences).set v with _ -> () - else unknown_preferences := Util.String.Map.add name v !unknown_preferences - in - Util.String.Map.iter iter m + () let pstring name p = string ~f:p#set name p#get let pbool name p = bool ~f:p#set name p#get diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index d2c88bffcc..2293ae9dfd 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -193,6 +193,12 @@ if (sp - num_args < coq_stack_threshold) { \ #define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0) #define AllocPair() Alloc_small(accu, 2, coq_tag_pair) +#define Swap_accu_sp do{ \ + value swap_accu_sp_tmp__ = accu; \ + accu = *sp; \ + *sp = swap_accu_sp_tmp__; \ + }while(0) + /* For signal handling, we hijack some code from the caml runtime */ extern intnat caml_signals_are_pending; @@ -1213,7 +1219,7 @@ value coq_interprete /* Adds the integer in the accumulator with the one ontop of the stack (which is poped)*/ print_instr("ADDINT63"); - accu = uint63_add(accu, *sp++); + Uint63_add(accu, *sp++); Next; } @@ -1221,10 +1227,12 @@ value coq_interprete print_instr("CHECKADDCINT63"); CheckInt2(); /* returns the sum with a carry */ - value s; - s = uint63_add(accu, *sp++); - AllocCarry(uint63_lt(s,accu)); - Field(accu, 0) = s; + int c; + Uint63_add(accu, *sp); + Uint63_lt(c, accu, *sp); + Swap_accu_sp; + AllocCarry(c); + Field(accu, 0) = *sp++; Next; } @@ -1232,10 +1240,12 @@ value coq_interprete print_instr("ADDCARRYCINT63"); CheckInt2(); /* returns the sum plus one with a carry */ - value s; - s = uint63_addcarry(accu, *sp++); - AllocCarry(uint63_leq(s, accu)); - Field(accu, 0) = s; + int c; + Uint63_addcarry(accu, *sp); + Uint63_leq(c, accu, *sp); + Swap_accu_sp; + AllocCarry(c); + Field(accu, 0) = *sp++; Next; } @@ -1246,7 +1256,7 @@ value coq_interprete Instruct (SUBINT63) { print_instr("SUBINT63"); /* returns the subtraction */ - accu = uint63_sub(accu, *sp++); + Uint63_sub(accu, *sp++); Next; } @@ -1254,12 +1264,12 @@ value coq_interprete print_instr("SUBCINT63"); CheckInt2(); /* returns the subtraction with a carry */ - value b; - value s; - b = *sp++; - s = uint63_sub(accu,b); - AllocCarry(uint63_lt(accu,b)); - Field(accu, 0) = s; + int c; + Uint63_lt(c, accu, *sp); + Uint63_sub(accu, *sp); + Swap_accu_sp; + AllocCarry(c); + Field(accu, 0) = *sp++; Next; } @@ -1267,12 +1277,12 @@ value coq_interprete print_instr("SUBCARRYCINT63"); CheckInt2(); /* returns the subtraction minus one with a carry */ - value b; - value s; - b = *sp++; - s = uint63_subcarry(accu,b); - AllocCarry(uint63_leq(accu,b)); - Field(accu, 0) = s; + int c; + Uint63_leq(c,accu,*sp); + Uint63_subcarry(accu,*sp); + Swap_accu_sp; + AllocCarry(c); + Field(accu, 0) = *sp++; Next; } @@ -1280,7 +1290,7 @@ value coq_interprete print_instr("MULINT63"); CheckInt2(); /* returns the multiplication */ - accu = uint63_mul(accu,*sp++); + Uint63_mul(accu,*sp++); Next; } @@ -1294,9 +1304,11 @@ value coq_interprete AllocPair(); */ /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/ /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/ - value x = accu; + Uint63_mulc(accu, *sp, sp); + *--sp = accu; AllocPair(); - Field(accu, 1) = uint63_mulc(x, *sp++, &Field(accu, 0)); + Field(accu, 1) = *sp++; + Field(accu, 0) = *sp++; Next; } @@ -1306,13 +1318,13 @@ value coq_interprete /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag since it probably only concerns negative number. needs to be checked at this point */ - value divisor; - divisor = *sp++; - if (uint63_eq0(divisor)) { - accu = divisor; + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; } else { - accu = uint63_div(accu, divisor); + Uint63_div(accu, *sp++); } Next; } @@ -1320,13 +1332,13 @@ value coq_interprete Instruct(CHECKMODINT63) { print_instr("CHEKMODINT63"); CheckInt2(); - value divisor; - divisor = *sp++; - if (uint63_eq0(divisor)) { - accu = divisor; + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; } else { - accu = uint63_mod(accu,divisor); + Uint63_mod(accu,*sp++); } Next; } @@ -1337,19 +1349,24 @@ value coq_interprete /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag since it probably only concerns negative number. needs to be checked at this point */ - value divisor; - divisor = *sp++; - if (uint63_eq0(divisor)) { - Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ - Field(accu, 0) = divisor; - Field(accu, 1) = divisor; + int b; + Uint63_eq0(b, *sp); + if (b) { + AllocPair(); + Field(accu, 0) = *sp; + Field(accu, 1) = *sp++; } else { - value modulus; - modulus = accu; - Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ - Field(accu, 0) = uint63_div(modulus,divisor); - Field(accu, 1) = uint63_mod(modulus,divisor); + *--sp = accu; + Uint63_div(sp[0],sp[1]); + Swap_accu_sp; + Uint63_mod(accu,sp[1]); + sp[1] = sp[0]; + Swap_accu_sp; + AllocPair(); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; + sp += 2; } Next; } @@ -1376,59 +1393,57 @@ value coq_interprete Field(accu, 0) = value_of_uint32(I64_to_int32(quo)); Field(accu, 1) = value_of_uint32(I64_to_int32(mod)); } */ - value bigint; /* TODO: fix */ - bigint = *sp++; /* TODO: take accu into account */ - value divisor; - divisor = *sp++; - if (uint63_eq0(divisor)) { - Alloc_small(accu, 2, 1); - Field(accu, 0) = divisor; - Field(accu, 1) = divisor; + int b; + Uint63_eq0(b, sp[1]); + if (b) { + AllocPair(); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[1]; } else { - value quo, mod; - mod = uint63_div21(accu, bigint, divisor, &quo); - Alloc_small(accu, 2, 1); - Field(accu, 0) = quo; - Field(accu, 1) = mod; + Uint63_div21(accu, sp[0], sp[1], sp); + sp[1] = sp[0]; + Swap_accu_sp; + AllocPair(); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; } + sp += 2; Next; } Instruct(CHECKLXORINT63) { print_instr("CHECKLXORINT63"); CheckInt2(); - accu = uint63_lxor(accu,*sp++); + Uint63_lxor(accu,*sp++); Next; } Instruct(CHECKLORINT63) { print_instr("CHECKLORINT63"); CheckInt2(); - accu = uint63_lor(accu,*sp++); + Uint63_lor(accu,*sp++); Next; } Instruct(CHECKLANDINT63) { print_instr("CHECKLANDINT63"); CheckInt2(); - accu = uint63_land(accu,*sp++); + Uint63_land(accu,*sp++); Next; } Instruct(CHECKLSLINT63) { print_instr("CHECKLSLINT63"); CheckInt2(); - value p = *sp++; - accu = uint63_lsl(accu,p); + Uint63_lsl(accu,*sp++); Next; } Instruct(CHECKLSRINT63) { print_instr("CHECKLSRINT63"); CheckInt2(); - value p = *sp++; - accu = uint63_lsr(accu,p); + Uint63_lsr(accu,*sp++); Next; } @@ -1436,7 +1451,7 @@ value coq_interprete print_instr("CHECKLSLINT63CONST1"); if (Is_uint63(accu)) { pc++; - accu = uint63_lsl1(accu); + Uint63_lsl1(accu); Next; } else { *--sp = uint63_one(); @@ -1450,7 +1465,7 @@ value coq_interprete print_instr("CHECKLSRINT63CONST1"); if (Is_uint63(accu)) { pc++; - accu = uint63_lsr1(accu); + Uint63_lsr1(accu); Next; } else { *--sp = uint63_one(); @@ -1463,18 +1478,17 @@ value coq_interprete Instruct (CHECKADDMULDIVINT63) { print_instr("CHECKADDMULDIVINT63"); CheckInt3(); - value x; - value y; - x = *sp++; - y = *sp++; - accu = uint63_addmuldiv(accu,x,y); + Uint63_addmuldiv(accu,sp[0],sp[1]); + sp += 2; Next; } Instruct (CHECKEQINT63) { print_instr("CHECKEQINT63"); CheckInt2(); - accu = uint63_eq(accu,*sp++) ? coq_true : coq_false; + int b; + Uint63_eq(b, accu, *sp++); + accu = b ? coq_true : coq_false; Next; } @@ -1484,7 +1498,9 @@ value coq_interprete } Instruct (LTINT63) { print_instr("LTINT63"); - accu = uint63_lt(accu,*sp++) ? coq_true : coq_false; + int b; + Uint63_lt(b,accu,*sp++); + accu = b ? coq_true : coq_false; Next; } @@ -1494,7 +1510,9 @@ value coq_interprete } Instruct (LEINT63) { print_instr("LEINT63"); - accu = uint63_leq(accu,*sp++) ? coq_true : coq_false; + int b; + Uint63_leq(b,accu,*sp++); + accu = b ? coq_true : coq_false; Next; } @@ -1503,25 +1521,30 @@ value coq_interprete /* assumes Inductive _ : _ := Eq | Lt | Gt */ print_instr("CHECKCOMPAREINT63"); CheckInt2(); - if (uint63_eq(accu,*sp)) { + int b; + Uint63_eq(b, accu, *sp); + if (b) { accu = coq_Eq; sp++; } - else accu = uint63_lt(accu,*sp++) ? coq_Lt : coq_Gt; + else { + Uint63_lt(b, accu, *sp++); + accu = b ? coq_Lt : coq_Gt; + } Next; } Instruct (CHECKHEAD0INT63) { print_instr("CHECKHEAD0INT63"); CheckInt1(); - accu = uint63_head0(accu); + Uint63_head0(accu); Next; } Instruct (CHECKTAIL0INT63) { print_instr("CHECKTAIL0INT63"); CheckInt1(); - accu = uint63_tail0(accu); + Uint63_tail0(accu); Next; } diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 9375b15de2..1ea461c5e5 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -19,7 +19,7 @@ #define Coq_stack_size (4096 * sizeof(value)) -#define Coq_stack_threshold (256 * sizeof(value)) +#define Coq_stack_threshold (256 * sizeof(value)) /* see kernel/cbytegen.ml */ #define Coq_max_stack_size (256 * 1024) #define TRANSP 0 diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index 5499f124a2..d982f67566 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -15,83 +15,142 @@ value uint63_##name() { \ } # define DECLARE_UNOP(name) \ -value uint63_##name(value x) { \ +value uint63_##name##_ml(value x) { \ static value* cb = 0; \ CAMLparam1(x); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback(*cb, x)); \ } -# define DECLARE_PREDICATE(name) \ -value uint63_##name(value x) { \ - static value* cb = 0; \ - CAMLparam1(x); \ - if (!cb) cb = caml_named_value("uint63 " #name); \ - CAMLreturn(Int_val(caml_callback(*cb, x))); \ - } +# define CALL_UNOP_NOASSIGN(name, x) \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + Setup_for_gc; \ + uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__); \ + Restore_after_gc + +# define CALL_UNOP(name, x) do{ \ + CALL_UNOP_NOASSIGN(name, x); \ + accu = uint63_return_value__; \ + }while(0) + +# define CALL_PREDICATE(r, name, x) do{ \ + CALL_UNOP_NOASSIGN(name, x); \ + (r) = Int_val(uint63_return_value__); \ + }while(0) # define DECLARE_BINOP(name) \ -value uint63_##name(value x, value y) { \ +value uint63_##name##_ml(value x, value y) { \ static value* cb = 0; \ CAMLparam2(x, y); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback2(*cb, x, y)); \ } -# define DECLARE_RELATION(name) \ -value uint63_##name(value x, value y) { \ - static value* cb = 0; \ - CAMLparam2(x, y); \ - if (!cb) cb = caml_named_value("uint63 " #name); \ - CAMLreturn(Int_val(caml_callback2(*cb, x, y))); \ - } +# define CALL_BINOP_NOASSIGN(name, x, y) \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + value uint63_arg_y__ = (y); \ + Setup_for_gc; \ + uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__); \ + Restore_after_gc + +# define CALL_BINOP(name, x, y) do{ \ + CALL_BINOP_NOASSIGN(name, x, y); \ + accu = uint63_return_value__; \ + }while(0) + +# define CALL_RELATION(r, name, x, y) do{ \ + CALL_BINOP_NOASSIGN(name, x, y); \ + (r) = Int_val(uint63_return_value__); \ + }while(0) # define DECLARE_TEROP(name) \ -value uint63_##name(value x, value y, value z) { \ +value uint63_##name##_ml(value x, value y, value z) { \ static value* cb = 0; \ CAMLparam3(x, y, z); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback3(*cb, x, y, z)); \ } +# define CALL_TEROP(name, x, y, z) do{ \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + value uint63_arg_y__ = (y); \ + value uint63_arg_z__ = (z); \ + Setup_for_gc; \ + uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \ + Restore_after_gc; \ + accu = uint63_return_value__; \ + }while(0) DECLARE_NULLOP(one) DECLARE_BINOP(add) +#define Uint63_add(x, y) CALL_BINOP(add, x, y) DECLARE_BINOP(addcarry) +#define Uint63_addcarry(x, y) CALL_BINOP(addcarry, x, y) DECLARE_TEROP(addmuldiv) +#define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z) DECLARE_BINOP(div) -DECLARE_TEROP(div21_ml) -DECLARE_RELATION(eq) -DECLARE_PREDICATE(eq0) +#define Uint63_div(x, y) CALL_BINOP(div, x, y) +DECLARE_BINOP(eq) +#define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y) +DECLARE_UNOP(eq0) +#define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x) DECLARE_UNOP(head0) +#define Uint63_head0(x) CALL_UNOP(head0, x) DECLARE_BINOP(land) -DECLARE_RELATION(leq) +#define Uint63_land(x, y) CALL_BINOP(land, x, y) +DECLARE_BINOP(leq) +#define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y) DECLARE_BINOP(lor) +#define Uint63_lor(x, y) CALL_BINOP(lor, x, y) DECLARE_BINOP(lsl) +#define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y) DECLARE_UNOP(lsl1) +#define Uint63_lsl1(x) CALL_UNOP(lsl1, x) DECLARE_BINOP(lsr) +#define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y) DECLARE_UNOP(lsr1) -DECLARE_RELATION(lt) +#define Uint63_lsr1(x) CALL_UNOP(lsr1, x) +DECLARE_BINOP(lt) +#define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y) DECLARE_BINOP(lxor) +#define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y) DECLARE_BINOP(mod) +#define Uint63_mod(x, y) CALL_BINOP(mod, x, y) DECLARE_BINOP(mul) -DECLARE_BINOP(mulc_ml) +#define Uint63_mul(x, y) CALL_BINOP(mul, x, y) DECLARE_BINOP(sub) +#define Uint63_sub(x, y) CALL_BINOP(sub, x, y) DECLARE_BINOP(subcarry) +#define Uint63_subcarry(x, y) CALL_BINOP(subcarry, x, y) DECLARE_UNOP(tail0) +#define Uint63_tail0(x) CALL_UNOP(tail0, x) + +DECLARE_TEROP(div21_ml) +# define Uint63_div21(x, y, z, q) do{ \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + value uint63_arg_y__ = (y); \ + value uint63_arg_z__ = (z); \ + Setup_for_gc; \ + uint63_return_value__ = \ + uint63_div21_ml_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \ + Restore_after_gc; \ + *q = Field(uint63_return_value__, 0); \ + accu = Field(uint63_return_value__, 1); \ + }while(0) -value uint63_div21(value x, value y, value z, value* q) { - CAMLparam3(x, y, z); - CAMLlocal1(qr); - qr = uint63_div21_ml(x, y, z); - *q = Field(qr, 0); - CAMLreturn(Field(qr, 1)); -} - -value uint63_mulc(value x, value y, value* h) { - CAMLparam2(x, y); - CAMLlocal1(hl); - hl = uint63_mulc_ml(x, y); - *h = Field(hl, 0); - CAMLreturn(Field(hl, 1)); -} +DECLARE_BINOP(mulc_ml) +# define Uint63_mulc(x, y, h) do{ \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + value uint63_arg_y__ = (y); \ + Setup_for_gc; \ + uint63_return_value__ = \ + uint63_mulc_ml_ml(uint63_arg_x__, uint63_arg_y__); \ + Restore_after_gc; \ + *(h) = Field(uint63_return_value__, 0); \ + accu = Field(uint63_return_value__, 1); \ + }while(0) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 92f4dc79bc..d431dc1e5c 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -9,28 +9,43 @@ #define uint63_one() ((value) 3) /* 2*1 + 1 */ #define uint63_eq(x,y) ((x) == (y)) -#define uint63_eq0(x) ((x) == (uint64_t)1) +#define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y)) +#define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1)) #define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y)) +#define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y)) #define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y)) +#define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y)) -#define uint63_add(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) - 1)) -#define uint63_addcarry(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) + 1)) -#define uint63_sub(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) + 1)) -#define uint63_subcarry(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) - 1)) -#define uint63_mul(x,y) (Val_long(uint63_of_value(x) * uint63_of_value(y))) -#define uint63_div(x,y) (Val_long(uint63_of_value(x) / uint63_of_value(y))) -#define uint63_mod(x,y) (Val_long(uint63_of_value(x) % uint63_of_value(y))) +#define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1)) +#define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1)) +#define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1)) +#define Uint63_subcarry(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) - 1)) +#define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y))) +#define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y))) +#define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y))) -#define uint63_lxor(x,y) ((value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1)) -#define uint63_lor(x,y) ((value)((uint64_t)(x) | (uint64_t)(y))) -#define uint63_land(x,y) ((value)((uint64_t)(x) & (uint64_t)(y))) +#define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1)) +#define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y))) +#define Uint63_land(x,y) (accu = (value)((uint64_t)(x) & (uint64_t)(y))) /* TODO: is + or | better? OCAML uses + */ /* TODO: is - or ^ better? */ -#define uint63_lsl(x,y) ((y) < (uint64_t) 127 ? ((value)((((uint64_t)(x)-1) << (uint63_of_value(y))) | 1)) : uint63_zero) -#define uint63_lsr(x,y) ((y) < (uint64_t) 127 ? ((value)(((uint64_t)(x) >> (uint63_of_value(y))) | 1)) : uint63_zero) -#define uint63_lsl1(x) ((value)((((uint64_t)(x)-1) << 1) +1)) -#define uint63_lsr1(x) ((value)(((uint64_t)(x) >> 1) |1)) +#define Uint63_lsl(x,y) do{ \ + value uint63_lsl_y__ = (y); \ + if (uint63_lsl_y__ < (uint64_t) 127) \ + accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \ + else \ + accu = uint63_zero; \ + }while(0) +#define Uint63_lsr(x,y) do{ \ + value uint63_lsl_y__ = (y); \ + if (uint63_lsl_y__ < (uint64_t) 127) \ + accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \ + else \ + accu = uint63_zero; \ + }while(0) +#define Uint63_lsl1(x) (accu = (value)((((uint64_t)(x)-1) << 1) +1)) +#define Uint63_lsr1(x) (accu = (value)(((uint64_t)(x) >> 1) |1)) /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */ /* (modulo 2^63) for p <= 63 */ @@ -40,6 +55,7 @@ value uint63_addmuldiv(uint64_t p, uint64_t x, uint64_t y) { r |= ((uint64_t)y >> (63-shiftby)) | 1; return r; } +#define Uint63_addmuldiv(p, x, y) (accu = uint63_addmuldiv(p, x, y)) value uint63_head0(uint64_t x) { int r = 0; @@ -51,6 +67,7 @@ value uint63_head0(uint64_t x) { if (!(x & 0x8000000000000000)) { x <<=1; r += 1; } return Val_int(r); } +#define Uint63_head0(x) (accu = uint63_head0(x)) value uint63_tail0(value x) { int r = 0; @@ -63,6 +80,7 @@ value uint63_tail0(value x) { if (!(x & 0x00000001)) { x >>=1; r += 1; } return Val_int(r); } +#define Uint63_tail0(x) (accu = uint63_tail0(x)) value uint63_mulc(value x, value y, value* h) { x = (uint64_t)x >> 1; @@ -86,6 +104,7 @@ value uint63_mulc(value x, value y, value* h) { *h = Val_int(hr); return Val_int(lr); } +#define Uint63_mulc(x, y, h) (accu = uint63_mulc(x, y, h)) #define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl))) #define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl))) @@ -123,3 +142,4 @@ value uint63_div21(value xh, value xl, value y, value* q) { *q = Val_int(quotient); return Val_int(reml); } +#define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q)) diff --git a/lib/envars.ml b/lib/envars.ml index 0f4670688b..af8e45b137 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -178,6 +178,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; + fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3"; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune index 002eb28eea..6ccf15df29 100644 --- a/plugins/funind/plugin_base.dune +++ b/plugins/funind/plugin_base.dune @@ -1,5 +1,5 @@ (library (name recdef_plugin) - (public_name coq.plugins.recdef) + (public_name coq.plugins.funind) (synopsis "Coq's functional induction plugin") (libraries coq.plugins.extraction)) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 2a84469af0..a05b1e3d81 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -828,10 +828,12 @@ let view_error s gv = open Locus (****************************** tactics ***********************************) -let rewritetac dir c = +let rewritetac ?(under=false) dir c = (* Due to the new optional arg ?tac, application shouldn't be too partial *) + let open Proofview.Notations in Proofview.V82.of_tactic begin - Equality.general_rewrite (dir = L2R) AllOccurrences true false c + Equality.general_rewrite (dir = L2R) AllOccurrences true false c <*> + if under then Proofview.cycle 1 else Proofview.tclUNIT () end (**********************`:********* hooks ************************************) @@ -973,7 +975,7 @@ let dependent_apply_error = * * Refiner.refiner that does not handle metas with a non ground type but works * with dependently typed higher order metas. *) -let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = +let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t gl = if with_evars then let refine gl = let t, ty, args, gl = pf_saturate ?beta ~bi_types:true gl t n in @@ -985,8 +987,11 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = pf_partial_solution gl t gs in Proofview.(V82.of_tactic - (tclTHEN (V82.tactic refine) - (if with_shelve then shelve_unifiable else tclUNIT ()))) gl + (Tacticals.New.tclTHENLIST [ + V82.tactic refine; + (if with_shelve then shelve_unifiable else tclUNIT ()); + (if first_goes_last then cycle 1 else tclUNIT ()) + ])) gl else let t, gl = if n = 0 then t, gl else let sigma, si = project gl, sig_it gl in @@ -1001,21 +1006,17 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); - Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl + Proofview.(V82.of_tactic + (Tacticals.New.tclTHENLIST [ + V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t)); + (if first_goes_last then cycle 1 else tclUNIT ()) + ])) gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = - let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in let uct = Evd.evar_universe_context (fst oc) in - let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.Unsafe.to_constr (snd oc)) in + let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in let gl = pf_unsafe_merge_uc uct gl in - let oc = if not first_goes_last || n <= 1 then oc else - let l, c = decompose_lam oc in - if not (List.for_all_i (fun i (_,t) -> Vars.closedn ~-i t) (1-n) l) then oc else - compose_lam (let xs,y = List.chop (n-1) l in y @ xs) - (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n))) - in - pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc)); - try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl + try applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error (* We wipe out all the keywords generated by the grammar rules we defined. *) @@ -1540,5 +1541,10 @@ let get g = end +let is_construct_ref sigma c r = + EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r +let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r +let is_const_ref sigma c r = + EConstr.isConst sigma c && GlobRef.equal (ConstRef (fst(EConstr.destConst sigma c))) r (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 9662daa7c7..58ce84ecb3 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -312,6 +312,7 @@ val applyn : with_evars:bool -> ?beta:bool -> ?with_shelve:bool -> + ?first_goes_last:bool -> int -> EConstr.t -> v82tac exception NotEnoughProducts @@ -348,7 +349,7 @@ val resolve_typeclasses : (*********************** Wrapped Coq tactics *****************************) -val rewritetac : ssrdir -> EConstr.t -> tactic +val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> tactic type name_hint = (int * EConstr.types array) option ref @@ -482,3 +483,7 @@ module MakeState(S : StateType) : sig val get : Proofview.Goal.t -> S.state end + +val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool +val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool +val is_const_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 4721e19a8b..6c74ac1960 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -500,3 +500,100 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. Lemma abstract_context T (P : T -> Type) x : (forall Q, Q = P -> Q x) -> P x. Proof. by move=> /(_ P); apply. Qed. + +(*****************************************************************************) +(* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *) + +Module Type UNDER_EQ. +Parameter Under_eq : + forall (R : Type), R -> R -> Prop. +Parameter Under_eq_from_eq : + forall (T : Type) (x y : T), @Under_eq T x y -> x = y. + +(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *) +Parameter Over_eq : + forall (R : Type), R -> R -> Prop. +Parameter over_eq : + forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. +Parameter over_eq_done : + forall (T : Type) (x : T), @Over_eq T x x. +(* We need both hints below, otherwise the test-suite does not pass *) +Hint Extern 0 (@Over_eq _ _ _) => solve [ apply over_eq_done ] : core. +(* => for [test-suite/ssr/under.v:test_big_patt1] *) +Hint Resolve over_eq_done : core. +(* => for [test-suite/ssr/over.v:test_over_1_1] *) + +(** [under_eq_done]: for Ltac-style over *) +Parameter under_eq_done : + forall (T : Type) (x : T), @Under_eq T x x. +Notation "''Under[' x ]" := (@Under_eq _ x _) + (at level 8, format "''Under[' x ]", only printing). +End UNDER_EQ. + +Module Export Under_eq : UNDER_EQ. +Definition Under_eq := @eq. +Lemma Under_eq_from_eq (T : Type) (x y : T) : + @Under_eq T x y -> x = y. +Proof. by []. Qed. +Definition Over_eq := Under_eq. +Lemma over_eq : + forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. +Proof. by []. Qed. +Lemma over_eq_done : + forall (T : Type) (x : T), @Over_eq T x x. +Proof. by []. Qed. +Lemma under_eq_done : + forall (T : Type) (x : T), @Under_eq T x x. +Proof. by []. Qed. +End Under_eq. + +Register Under_eq as plugins.ssreflect.Under_eq. +Register Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq. + +Module Type UNDER_IFF. +Parameter Under_iff : Prop -> Prop -> Prop. +Parameter Under_iff_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y. + +(** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *) +Parameter Over_iff : Prop -> Prop -> Prop. +Parameter over_iff : + forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y. +Parameter over_iff_done : + forall (x : Prop), @Over_iff x x. +Hint Extern 0 (@Over_iff _ _) => solve [ apply over_iff_done ] : core. +Hint Resolve over_iff_done : core. + +(** [under_iff_done]: for Ltac-style over *) +Parameter under_iff_done : + forall (x : Prop), @Under_iff x x. +Notation "''Under[' x ]" := (@Under_iff x _) + (at level 8, format "''Under[' x ]", only printing). +End UNDER_IFF. + +Module Export Under_iff : UNDER_IFF. +Definition Under_iff := iff. +Lemma Under_iff_from_iff (x y : Prop) : + @Under_iff x y -> x <-> y. +Proof. by []. Qed. +Definition Over_iff := Under_iff. +Lemma over_iff : + forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y. +Proof. by []. Qed. +Lemma over_iff_done : + forall (x : Prop), @Over_iff x x. +Proof. by []. Qed. +Lemma under_iff_done : + forall (x : Prop), @Under_iff x x. +Proof. by []. Qed. +End Under_iff. + +Register Under_iff as plugins.ssreflect.Under_iff. +Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff. + +Definition over := (over_eq, over_iff). + +Ltac over := + by [ apply: Under_eq.under_eq_done + | apply: Under_iff.under_iff_done + | rewrite over + ]. diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 4433f2fce7..ad20113320 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -19,7 +19,6 @@ open Context open Vars open Locus open Printer -open Globnames open Termops open Tacinterp @@ -327,15 +326,15 @@ let rule_id = mk_internal_id "rewrite rule" exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option -let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = +let id_map_redex _ sigma ~before:_ ~after = sigma, after + +let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = (* ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *) let env = pf_env gl in let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in - let sigma, p = - let sigma = Evd.create_evar_defs sigma in - let (sigma, ev) = Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in - (sigma, ev) - in + let sigma, new_rdx = map_redex env sigma ~before:rdx ~after:new_rdx in + let sigma, p = (* The resulting goal *) + Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in @@ -355,9 +354,10 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te))) | e when CErrors.noncritical e -> raise (PRtype_error None) in - ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty)); + ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); + ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with - ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl + ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl with _ -> (* we generate a msg like: "Unable to find an instance for the variable" *) let hd_ty, miss = match EConstr.kind sigma c with @@ -381,11 +381,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty)) ;; -let is_construct_ref sigma c r = - EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r -let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r - -let rwcltac cl rdx dir sr gl = +let rwcltac ?under ?map_redex cl rdx dir sr gl = let sr = let sigma, r = sr in let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in @@ -403,14 +399,14 @@ let rwcltac cl rdx dir sr gl = let sigma, c_ty = Typing.type_of env sigma c in ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with - | AtomicType(e, a) when is_ind_ref sigma e c_eq -> + | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in - pirrel_rewrite cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl + pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl | _ -> let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in let gl = pf_merge_uc_of sigma gl in - Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl + Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl else let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in let r3, _, r3t = @@ -421,7 +417,7 @@ let rwcltac cl rdx dir sr gl = let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in - let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in + let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl in let cvtac' _ = @@ -439,7 +435,6 @@ let rwcltac cl rdx dir sr gl = in tclTHEN cvtac' rwtac gl - [@@@ocaml.warning "-3"] let lz_coq_prod = let prod = lazy (Coqlib.build_prod ()) in fun () -> Lazy.force prod @@ -547,7 +542,7 @@ let rwprocess_rule dir rule gl = in r_sigma, rules -let rwrxtac occ rdx_pat dir rule gl = +let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl = let env = pf_env gl in let r_sigma, rules = rwprocess_rule dir rule gl in let find_rule rdx = @@ -585,7 +580,7 @@ let rwrxtac occ rdx_pat dir rule gl = let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in let (d, r), rdx = conclude concl in let r = Evd.merge_universe_context (pi1 r) (pi2 r), EConstr.of_constr (pi3 r) in - rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl + rwcltac ?under ?map_redex (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl ;; let ssrinstancesofrule ist dir arg gl = @@ -614,7 +609,7 @@ let ssrinstancesofrule ist dir arg gl = let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl -let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = +let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = let fail = ref false in let interp_rpattern gl gc = try interp_rpattern gl gc @@ -628,7 +623,7 @@ let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt - | RWeq -> rwrxtac occ rx dir t) gl in + | RWeq -> rwrxtac ?under ?map_redex occ rx dir t) gl in let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl @@ -638,8 +633,8 @@ let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = (** The "rewrite" tactic *) -let ssrrewritetac ist rwargs = - tclTHENLIST (List.map (rwargtac ist) rwargs) +let ssrrewritetac ?under ?map_redex ist rwargs = + tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs) (** The "unlock" tactic *) @@ -660,4 +655,3 @@ let unlocktac ist args gl = (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in tclTHENLIST (List.map utac args @ ktacs) gl - diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index bbcd6b900a..601968d511 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -48,13 +48,15 @@ val ssrinstancesofrule : Ssrast.ssrterm -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma +(* map_redex (by default the identity on after) is called on the + * redex (before) and its replacement (after). It is used to + * "rename" binders by the under tactic *) val ssrrewritetac : + ?under:bool -> + ?map_redex:(Environ.env -> Evd.evar_map -> + before:EConstr.t -> after:EConstr.t -> Evd.evar_map * EConstr.t) -> Ltac_plugin.Tacinterp.interp_sign -> - ((Ssrast.ssrdir * (int * Ssrast.ssrmmod)) * - (((Ssrast.ssrhyps option * Ssrmatching.occ) * - Ssrmatching.rpattern option) * - (ssrwkind * Ssrast.ssrterm))) - list -> Tacmach.tactic + ssrrwarg list -> Tacmach.tactic val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 3cadc92bcc..01d71aa96a 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -319,3 +319,172 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in basecuttac "ssr_suff" ty gl in Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))] + +open Proofview.Notations + +let is_app_evar sigma t = + match EConstr.kind sigma t with + | Constr.Evar _ -> true + | Constr.App(t,_) -> + begin match EConstr.kind sigma t with + | Constr.Evar _ -> true + | _ -> false end + | _ -> false + +let rec ncons n e = match n with + | 0 -> [] + | n when n > 0 -> e :: ncons (n - 1) e + | _ -> failwith "ncons" + +let intro_lock ipats = + let hnf' = Proofview.numgoals >>= fun ng -> + Proofview.tclDISPATCH + (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in + let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ -> + Proofview.tclORELSE + (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())]) + (fun _exn -> Proofview.Goal.enter begin fun gl -> + let c = Proofview.Goal.concl gl in + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + match EConstr.kind_of_type sigma c with + | Term.AtomicType(hd, args) when + Ssrcommon.is_const_ref sigma hd (Coqlib.lib_ref "core.iff.type") && + Array.length args = 2 && is_app_evar sigma args.(1) -> + Tactics.New.refine ~typecheck:true (fun sigma -> + let sigma, under_iff = + Ssrcommon.mkSsrConst "Under_iff" env sigma in + let sigma, under_from_iff = + Ssrcommon.mkSsrConst "Under_iff_from_iff" env sigma in + let ty = EConstr.mkApp (under_iff,args) in + let sigma, t = Evarutil.new_evar env sigma ty in + sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|])) + | _ -> + let t = Reductionops.whd_all env sigma c in + match EConstr.kind_of_type sigma t with + | Term.AtomicType(hd, args) when + Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") && + Array.length args = 3 && is_app_evar sigma args.(2) -> + Tactics.New.refine ~typecheck:true (fun sigma -> + let sigma, under = + Ssrcommon.mkSsrConst "Under_eq" env sigma in + let sigma, under_from_eq = + Ssrcommon.mkSsrConst "Under_eq_from_eq" env sigma in + let ty = EConstr.mkApp (under,args) in + let sigma, t = Evarutil.new_evar env sigma ty in + sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|])) + | _ -> + ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); + + Proofview.tclUNIT () + end) + end + in + hnf' <*> Ssripats.tclIPATssr ipats <*> lock_eq () + +let pretty_rename evar_map term varnames = + let rec aux term vars = + try + match vars with + | [] -> term + | Names.Name.Anonymous :: varnames -> + let name, types, body = EConstr.destLambda evar_map term in + let res = aux body varnames in + EConstr.mkLambda (name, types, res) + | Names.Name.Name _ as name :: varnames -> + let { Context.binder_relevance = r }, types, body = + EConstr.destLambda evar_map term in + let res = aux body varnames in + EConstr.mkLambda (Context.make_annot name r, types, res) + with DestKO -> term + in + aux term varnames + +let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1) + +let check_numgoals ?(minus = 0) nh = + Proofview.numgoals >>= fun ng -> + if nh <> ng then + let errmsg = + str"Incorrect number of tactics" ++ spc() ++ + str"(expected "++int (ng - minus)++str(String.plural ng " tactic") ++ + str", was given "++ int (nh - minus)++str")." + in + CErrors.user_err errmsg + else + Proofview.tclUNIT () + +let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = + + (* total number of implied hints *) + let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in + + let varnames = + let rec aux acc = function + | IPatId id :: rest -> aux (Names.Name.Name id :: acc) rest + | IPatClear _ :: rest -> aux acc rest + | IPatSimpl _ :: rest -> aux acc rest + | IPatAnon (One _ | Drop) :: rest -> + aux (Names.Name.Anonymous :: acc) rest + | _ -> List.rev acc in + aux [] @@ match ipats with + | None -> [] + | Some (IPatCase(Regular (l :: _)) :: _) -> l + | Some l -> l in + + (* If we find a "=> [|]" we add 1 | to get "=> [||]" for the extra + * goal (the one that is left once we run over) *) + let ipats = + match ipats with + | None -> [IPatNoop] + | Some l when pad_intro -> (* typically, ipats = Some [IPatAnon All] *) + let new_l = ncons (nh - 1) l in + [IPatCase(Regular (new_l @ [[]]))] + | Some (IPatCase(Regular []) :: _ as ipats) -> ipats + (* Erik: is the previous line correct/useful? *) + | Some (IPatCase(Regular l) :: rest) -> IPatCase(Regular(l @ [[]])) :: rest + | Some (IPatCase(Block _) :: _ as l) -> l + | Some l -> [IPatCase(Regular [l;[]])] in + + let map_redex env evar_map ~before:_ ~after:t = + ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames)); + + let evar_map, ty = Typing.type_of env evar_map t in + let new_t = (* pretty-rename the bound variables *) + try begin match EConstr.destApp evar_map t with (f, ar) -> + let lam = Array.last ar in + ppdebug(lazy Pp.(str"under: mapping:" ++ + pr_econstr_env env evar_map lam)); + let new_lam = pretty_rename evar_map lam varnames in + let new_ar, len1 = Array.copy ar, pred (Array.length ar) in + new_ar.(len1) <- new_lam; + EConstr.mkApp (f, new_ar) + end with + | DestKO -> + ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp")); + t + in + ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); + evar_map, new_t + in + let undertacs = + if hint = nohint then + Proofview.tclUNIT () + else + let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in + (* Usefulness of check_numgoals: tclDISPATCH would be enough, + except for the error message w.r.t. the number of + provided/expected tactics, as the last one is implied *) + check_numgoals ~minus:1 nh <*> + Proofview.tclDISPATCH + ((List.map (function None -> overtac + | Some e -> ssrevaltac ist e <*> + overtac) + (if hint = nullhint then [None] else snd hint)) + @ [betaiota]) + in + let rew = + Proofview.V82.tactic + (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) + in + rew <*> intro_lock ipats <*> undertacs diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 35e89dbcea..6dd01ca6fc 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -57,3 +57,16 @@ val sufftac : (bool * Tacinterp.Value.t option list)) -> Tacmach.tactic +(* pad_intro (by default false) indicates whether the intro-pattern + "=> i..." must be turned into "=> [i...|i...|i...|]" (n+1 branches, + assuming there are n provided tactics in the ssrhint argument + "do [...|...|...]"; it is useful when the intro-pattern is "=> *"). + Otherwise, "=> i..." is turned into "=> [i...|]". *) +val undertac : + ?pad_intro:bool -> + Ltac_plugin.Tacinterp.interp_sign -> + Ssrast.ssripats option -> Ssrequality.ssrrwarg -> + Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic + +val overtac : + unit Proofview.tactic diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index f44962f213..27a558611e 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -86,6 +86,15 @@ GRAMMAR EXTEND Gram ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]]; END +(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *) +ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } +| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } +END +GRAMMAR EXTEND Gram + GLOBAL: ssrtac3arg; + ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]]; +END + { (* Lexically closed tactic for tacticals. *) @@ -741,15 +750,33 @@ let pushIPatNoop = function | pats :: orpat -> (IPatNoop :: pats) :: orpat | [] -> [] +let test_ident_no_do strm = + match Util.stream_nth 0 strm with + | Tok.IDENT s when s <> "do" -> () + | _ -> raise Stream.Failure + +let test_ident_no_do = + Pcoq.Entry.of_parser "test_ident_no_do" test_ident_no_do + } +ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print } +| [ "YouShouldNotTypeThis" ident(id) ] -> { id } +END + + +GRAMMAR EXTEND Gram + GLOBAL: ident_no_do; + ident_no_do: [ [ test_ident_no_do; id = IDENT -> { Id.of_string id } ] ]; +END + ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } INTERPRETED BY { interp_ipats } GLOBALIZED BY { intern_ipats } | [ "_" ] -> { [IPatAnon Drop] } | [ "*" ] -> { [IPatAnon All] } | [ ">" ] -> { [IPatFastNondep] } - | [ ident(id) ] -> { [IPatId id] } + | [ ident_no_do(id) ] -> { [IPatId id] } | [ "?" ] -> { [IPatAnon (One None)] } | [ "+" ] -> { [IPatAnon Temporary] } | [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] } @@ -1047,6 +1074,13 @@ ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintar | [ ssrtacarg(arg) ] -> { mk_hint arg } END +(* Copy of ssrhintarg with LEVEL "3", useful for: "under ... do ..." *) +ARGUMENT EXTEND ssrhint3arg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma } +| [ "[" "]" ] -> { nullhint } +| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs } +| [ ssrtac3arg(arg) ] -> { mk_hint arg } +END + ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma } | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs } END @@ -2652,6 +2686,34 @@ END { +let check_under_arg ((_dir,mult),((_occ,_rpattern),_rule)) = + if mult <> nomult then + CErrors.user_err Pp.(str"under does not support multipliers") + +} + + +TACTIC EXTEND under + | [ "under" ssrrwarg(arg) ] -> { + check_under_arg arg; + Ssrfwd.undertac ist None arg nohint + } + | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) ] -> { + check_under_arg arg; + Ssrfwd.undertac ist (Some ipats) arg nohint + } + | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhint3arg(h) ] -> { + check_under_arg arg; + Ssrfwd.undertac ist (Some ipats) arg h + } + | [ "under" ssrrwarg(arg) "do" ssrhint3arg(h) ] -> { (* implicit "=> [*|*]" *) + check_under_arg arg; + Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h + } +END + +{ + (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index bf7f082192..08f028465b 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -465,7 +465,7 @@ let interp_modloc mr = (* The unified, extended vernacular "Search" command *) let ssrdisplaysearch gr env t = - let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in + let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in Feedback.msg_info (hov 2 pr_res ++ fnl ()) } diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index fefc15dfb2..9f2397ec38 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -12,41 +12,44 @@ open Reduction open Declarations open Constr open Univ +open Variance open Util +type inferred = IrrelevantI | CovariantI + (** Throughout this module we modify a map [variances] from local - universes to [Variance.t]. It starts as a trivial mapping to - [Irrelevant] and every time we encounter a local universe we - restrict it accordingly. *) + universes to [inferred]. It starts as a trivial mapping to + [Irrelevant] and every time we encounter a local universe we + restrict it accordingly. + [Invariant] universes are removed from the map. +*) +exception TrivialVariance + +let maybe_trivial variances = + if LMap.is_empty variances then raise TrivialVariance + else variances let infer_level_eq u variances = - if LMap.mem u variances - then LMap.set u Variance.Invariant variances - else variances + maybe_trivial (LMap.remove u variances) let infer_level_leq u variances = - match LMap.find u variances with - | exception Not_found -> variances - | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances + (* can only set Irrelevant -> Covariant so nontrivial *) + LMap.update u (function + | None -> None + | Some CovariantI as x -> x + | Some IrrelevantI -> Some CovariantI) + variances let infer_generic_instance_eq variances u = Array.fold_left (fun variances u -> infer_level_eq u variances) variances (Instance.to_array u) -let variance_pb cv_pb var = - let open Variance in - match cv_pb, var with - | _, Irrelevant -> Irrelevant - | _, Invariant -> Invariant - | CONV, Covariant -> Invariant - | CUMUL, Covariant -> Covariant - let infer_cumulative_ind_instance cv_pb mind_variance variances u = Array.fold_left2 (fun variances varu u -> - match LMap.find u variances with - | exception Not_found -> variances - | varu' -> - LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances) + match cv_pb, varu with + | _, Irrelevant -> variances + | _, Invariant | CONV, Covariant -> infer_level_eq u variances + | CUMUL, Covariant -> infer_level_leq u variances) variances mind_variance (Instance.to_array u) let infer_inductive_instance cv_pb env variances ind nargs u = @@ -182,6 +185,32 @@ let infer_arity_constructor is_arity env variances arcn = i is irrelevant, j is invariant. *) if not is_arity then infer_term CUMUL env variances codom else variances +open Entries + +let infer_inductive_core env params entries uctx = + let uarray = Instance.to_array @@ UContext.instance uctx in + if Array.is_empty uarray then raise TrivialVariance; + let env = Environ.push_context uctx env in + let variances = + Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances) + LMap.empty uarray + in + let env, params = Typeops.check_context env params in + let variances = List.fold_left (fun variances entry -> + let variances = infer_arity_constructor true + env variances entry.mind_entry_arity + in + List.fold_left (infer_arity_constructor false env) + variances entry.mind_entry_lc) + variances + entries + in + Array.map (fun u -> match LMap.find u variances with + | exception Not_found -> Invariant + | IrrelevantI -> Irrelevant + | CovariantI -> Covariant) + uarray + let infer_inductive env mie = let open Entries in let { mind_entry_params = params; @@ -195,27 +224,11 @@ let infer_inductive env mie = | Monomorphic_entry _ -> assert false | Polymorphic_entry (_,uctx) -> uctx in - let uarray = Instance.to_array @@ UContext.instance uctx in - let env = Environ.push_context uctx env in - let variances = - Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) - LMap.empty uarray - in - let env, params = Typeops.check_context env params in - let variances = List.fold_left (fun variances entry -> - let variances = infer_arity_constructor true - env variances entry.mind_entry_arity - in - List.fold_left (infer_arity_constructor false env) - variances entry.mind_entry_lc) - variances - entries - in - let variances = Array.map (fun u -> LMap.find u variances) uarray in - Some variances + try Some (infer_inductive_core env params entries uctx) + with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) in { mie with mind_entry_variance = variances } let dummy_variance = let open Entries in function | Monomorphic_entry _ -> assert false - | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Variance.Irrelevant + | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant diff --git a/stm/stm.ml b/stm/stm.ml index e1ab45163a..06bc6e3340 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -27,6 +27,8 @@ open Feedback open Vernacexpr open Vernacextend +module PG_compat = Vernacstate.Proof_global [@@ocaml.warning "-3"] + let is_vtkeep = function VtKeep _ -> true | _ -> false let get_vtkeep = function VtKeep x -> x | _ -> assert false @@ -139,8 +141,8 @@ let may_pierce_opaque = function | _ -> false let update_global_env () = - if Vernacstate.Proof_global.there_are_pending_proofs () then - Vernacstate.Proof_global.update_global_env () + if PG_compat.there_are_pending_proofs () then + PG_compat.update_global_env () module Vcs_ = Vcs.Make(Stateid.Self) type future_proof = Proof_global.closed_proof_output Future.computation @@ -948,7 +950,7 @@ end = struct (* {{{ *) let prev = (VCS.visit id).next in if is_cached_and_valid prev then { s with proof = - Vernacstate.Proof_global.copy_terminators + PG_compat.copy_terminators ~src:((get_cached prev).proof) ~tgt:s.proof } else s with VCS.Expired -> s in @@ -957,7 +959,7 @@ end = struct (* {{{ *) if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = - Vernacstate.Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in + PG_compat.copy_terminators ~src:s.proof ~tgt:pstate } in let s = { s with system = States.replace_summary s.system begin @@ -1009,8 +1011,8 @@ end = struct (* {{{ *) if feedback_processed then Hooks.(call state_computed ~doc id ~in_cache:false); VCS.reached id; - if Vernacstate.Proof_global.there_are_pending_proofs () then - VCS.goals id (Vernacstate.Proof_global.get_open_goals ()) + if PG_compat.there_are_pending_proofs () then + VCS.goals id (PG_compat.get_open_goals ()) with e -> let (e, info) = CErrors.push e in let good_id = !cur_id in @@ -1130,9 +1132,9 @@ let show_script ?proof () = try let prf = try match proof with - | None -> Some (Vernacstate.Proof_global.get_current_proof_name ()) + | None -> Some (PG_compat.get_current_proof_name ()) | Some (p,_) -> Some (p.Proof_global.id) - with Vernacstate.Proof_global.NoCurrentProof -> None + with PG_compat.NoCurrentProof -> None in let cmds = get_script prf in let _,_,_,indented_cmds = @@ -1295,7 +1297,7 @@ end = struct (* {{{ *) | Some vcs, _ -> vcs in let cb, _ = try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) - with Failure _ -> raise Vernacstate.Proof_global.NoCurrentProof in + with Failure _ -> raise PG_compat.NoCurrentProof in let n = fold_until (fun n (_,vcs,_,_,_) -> if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) 0 id in @@ -1333,7 +1335,7 @@ end = struct (* {{{ *) | None -> true done; !rv - with Not_found | Vernacstate.Proof_global.NoCurrentProof -> None + with Not_found | PG_compat.NoCurrentProof -> None end (* }}} *) @@ -1594,7 +1596,7 @@ end = struct (* {{{ *) let wall_clock2 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); - let p = Vernacstate.Proof_global.return_proof ~allow_partial:drop_pt () in + let p = PG_compat.return_proof ~allow_partial:drop_pt () in if drop_pt then feedback ~id Complete; p) @@ -1621,7 +1623,7 @@ end = struct (* {{{ *) to set the state manually here *) State.unfreeze st; let pobject, _ = - Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in + PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator []) in @@ -1758,15 +1760,15 @@ end = struct (* {{{ *) try Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop; if drop then - let _proof = Vernacstate.Proof_global.return_proof ~allow_partial:true () in + let _proof = PG_compat.return_proof ~allow_partial:true () in `OK_ADMITTED else begin (* The original terminator, a hook, has not been saved in the .vio*) - Vernacstate.Proof_global.set_terminator (Lemmas.standard_proof_terminator []); + PG_compat.set_terminator (Lemmas.standard_proof_terminator []); let opaque = Proof_global.Opaque in let proof = - Vernacstate.Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in + PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start; @@ -2016,7 +2018,7 @@ end = struct (* {{{ *) try Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id; State.purify (fun () -> - let Proof.{sigma=sigma0} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in + let Proof.{sigma=sigma0} = Proof.data (PG_compat.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in let is_ground c = Evarutil.is_ground_term sigma0 c in if not ( @@ -2028,7 +2030,7 @@ end = struct (* {{{ *) "goals only")) else begin let (i, ast) = r_ast in - Vernacstate.Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); + PG_compat.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); (* STATE SPEC: * - start : id * - return: id @@ -2037,7 +2039,7 @@ end = struct (* {{{ *) *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp r_state_fb st ast); - let Proof.{sigma} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in + let Proof.{sigma} = Proof.data (PG_compat.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> @@ -2084,7 +2086,7 @@ end = struct (* {{{ *) stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> - Vernacstate.Proof_global.with_current_proof (fun _ p -> + PG_compat.with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> @@ -2117,7 +2119,7 @@ end = struct (* {{{ *) let open Notations in match Future.join f with | Some (pt, uc) -> - let sigma, env = Vernacstate.Proof_global.get_current_context () in + let sigma, env = PG_compat.get_current_context () in stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ @@ -2399,8 +2401,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = end in match (VCS.get_info base_state).state with | FullState { Vernacstate.proof } -> - Option.iter Vernacstate.Proof_global.unfreeze proof; - Vernacstate.Proof_global.with_current_proof (fun _ p -> + Option.iter PG_compat.unfreeze proof; + PG_compat.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; fst (Pfedit.solve Goal_select.SelectAll None tac p), ()); (* STATE SPEC: @@ -2570,7 +2572,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | VtKeepDefined -> Proof_global.Transparent in let proof = - Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:id fp in + PG_compat.close_future_proof ~opaque ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in @@ -2578,13 +2580,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; - Vernacstate.Proof_global.discard_all () + PG_compat.discard_all () ), not redefine_qed, true | `Sync (name, `Immediate) -> (fun () -> reach eop; let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); - Vernacstate.Proof_global.discard_all () + PG_compat.discard_all () ), true, true | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; @@ -2603,7 +2605,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent | VtKeepAxiom -> assert false in - Some(Vernacstate.Proof_global.close_proof ~opaque + Some(PG_compat.close_proof ~opaque ~keep_body_ucst_separate:false (State.exn_on id ~valid:eop)) in if keep <> VtKeep VtKeepAxiom then @@ -2614,7 +2616,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); - Vernacstate.Proof_global.discard_all () + PG_compat.discard_all () ), true, true | `MaybeASync (start, nodes, name, delegate) -> (fun () -> reach ~cache:true start; @@ -2875,7 +2877,7 @@ let merge_proof_branch ~valid ?id qast keep brname = VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> - Exninfo.iraise (State.exn_on ~valid Stateid.dummy (Vernacstate.Proof_global.NoCurrentProof, Exninfo.null)) + Exninfo.iraise (State.exn_on ~valid Stateid.dummy (PG_compat.NoCurrentProof, Exninfo.null)) (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) @@ -3067,7 +3069,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) - if not in_proof && Vernacstate.Proof_global.there_are_pending_proofs () then + if not in_proof && PG_compat.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in let opacity_of_produced_term = function diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 78a3f7c63a..4ee4aae36c 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -49,16 +49,15 @@ TO_SED_IN_BOTH=( -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it + -e s'/[0-9]//g' # sometimes the time is under 1 minute, sometimes it's over 1 minute, so we want to remove/normalize both instances; see https://github.com/coq/coq/issues/5675#issuecomment-487378622 ) TO_SED_IN_PER_FILE=( - -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start -e s'/ */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign ) TO_SED_IN_PER_LINE=( - -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start -e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives ) diff --git a/test-suite/output/ssr_under.out b/test-suite/output/ssr_under.out new file mode 100644 index 0000000000..499d25391e --- /dev/null +++ b/test-suite/output/ssr_under.out @@ -0,0 +1,4 @@ +'Under[ m - m ] +(G (fun _ : nat => 0) n >= 0) +'Under[ r = R0 \/ E r ] +(Rbar_le Rbar0 (Lub_Rbar (fun r : R => r = R0 \/ E r))) diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v new file mode 100644 index 0000000000..fb7503d902 --- /dev/null +++ b/test-suite/output/ssr_under.v @@ -0,0 +1,30 @@ +From Coq Require Import ssreflect. + +Axiom subnn : forall n : nat, n - n = 0. +Parameter G : (nat -> nat) -> nat -> nat. +Axiom eq_G : + forall F1 F2 : nat -> nat, + (forall n : nat, F1 n = F2 n) -> + forall n : nat, G F1 n = G F2 n. + +Ltac show := match goal with [|-?g] => idtac g end. + +Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. +under eq_G => m do [show; rewrite subnn]. +show. +Abort. + +Parameters (R Rbar : Set) (R0 : R) (Rbar0 : Rbar). +Parameter Rbar_le : Rbar -> Rbar -> Prop. +Parameter Lub_Rbar : (R -> Prop) -> Rbar. +Parameter Lub_Rbar_eqset : + forall E1 E2 : R -> Prop, + (forall x : R, E1 x <-> E2 x) -> + Lub_Rbar E1 = Lub_Rbar E2. + +Lemma test_Lub_Rbar (E : R -> Prop) : + Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)). +Proof. +under Lub_Rbar_eqset => r do show. +show. +Abort. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index cb2c56736c..ca360f65a7 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -427,6 +427,8 @@ Lemma leqnSn n : n <= n.+1. Proof. by elim: n. Qed. Lemma leq_trans n m p : m <= n -> n <= p -> m <= p. Admitted. +Lemma leq_ltn_trans n m p : m <= n -> n < p -> m < p. +Admitted. Lemma leqW m n : m <= n -> m <= n.+1. Admitted. Hint Resolve leqnSn. diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v new file mode 100644 index 0000000000..8232741b0d --- /dev/null +++ b/test-suite/ssr/over.v @@ -0,0 +1,70 @@ +Require Import ssreflect. + +Axiom daemon : False. Ltac myadmit := case: daemon. + +(** Testing over for the 1-var case *) + +Lemma test_over_1_1 : False. +intros. +evar (I : Type); evar (R : Type); evar (x2 : I -> R). +assert (H : forall i : nat, i + 2 * i - i = x2 i). + intros i. + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold I in *; clear I. + apply Under_eq_from_eq. + Fail done. + + over. + myadmit. +Qed. + +Lemma test_over_1_2 : False. +intros. +evar (I : Type); evar (R : Type); evar (x2 : I -> R). +assert (H : forall i : nat, i + 2 * i - i = x2 i). + intros i. + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold I in *; clear I. + apply Under_eq_from_eq. + Fail done. + + by rewrite over. + myadmit. +Qed. + +(** Testing over for the 2-var case *) + +Lemma test_over_2_1 : False. +intros. +evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). +assert (H : forall i j, i + 2 * j - i = x2 i j). + intros i j. + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold J in *; clear J; + unfold I in *; clear I. + apply Under_eq_from_eq. + Fail done. + + over. + myadmit. +Qed. + +Lemma test_over_2_2 : False. +intros. +evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). +assert (H : forall i j : nat, i + 2 * j - i = x2 i j). + intros i j. + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold J in *; clear J; + unfold I in *; clear I. + apply Under_eq_from_eq. + Fail done. + + rewrite over. + done. + myadmit. +Qed. diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v new file mode 100644 index 0000000000..f285ad138b --- /dev/null +++ b/test-suite/ssr/under.v @@ -0,0 +1,234 @@ +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. +Global Unset SsrOldRewriteGoalsOrder. + +(* under <names>: {occs}[patt]<lemma>. + under <names>: {occs}[patt]<lemma> by tac1. + under <names>: {occs}[patt]<lemma> by [tac1 | ...]. + *) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Axiom daemon : False. Ltac myadmit := case: daemon. + +Module Mocks. + +(* Mock bigop.v definitions to test the behavior of under with bigops + without requiring mathcomp *) + +Definition eqfun := + fun (A B : Type) (f g : forall _ : B, A) => forall x : B, @eq A (f x) (g x). + +Section Defix. +Variables (T : Type) (n : nat) (f : forall _ : T, T) (x : T). +Fixpoint loop (m : nat) : T := + match m return T with + | O => x + | S i => f (loop i) + end. +Definition iter := loop n. +End Defix. + +Parameter eq_bigl : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P1 P2 : pred I) (F : forall _ : I, R) (_ : @eqfun bool I P1 P2), + @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P1 i) (F i))) + (@bigop R I idx r (fun i : I => @BigBody R I i op (P2 i) (F i))). + +Parameter eq_big : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P1 P2 : pred I) (F1 F2 : forall _ : I, R) (_ : @eqfun bool I P1 P2) + (_ : forall (i : I) (_ : is_true (P1 i)), @eq R (F1 i) (F2 i)), + @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P1 i) (F1 i))) + (@bigop R I idx r (fun i : I => @BigBody R I i op (P2 i) (F2 i))). + +Parameter eq_bigr : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P : pred I) (F1 F2 : forall _ : I, R) + (_ : forall (i : I) (_ : is_true (P i)), @eq R (F1 i) (F2 i)), + @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P i) (F1 i))) + (@bigop R I idx r (fun i : I => @BigBody R I i op (P i) (F2 i))). + +Parameter big_const_nat : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (m n : nat) (x : R), + @eq R (@bigop R nat idx (index_iota m n) (fun i : nat => @BigBody R nat i op true x)) + (@iter R (subn n m) (op x) idx). + +Delimit Scope N_scope with num. +Delimit Scope nat_scope with N. + +Reserved Notation "\sum_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\sum_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n ) '/ ' F ']'"). + +Local Notation "+%N" := addn (at level 0, only parsing). + +Notation "\sum_ ( m <= i < n | P ) F" := + (\big[+%N/0%N]_(m <= i < n | P%B) F%N) : (*nat_scope*) big_scope. +Notation "\sum_ ( m <= i < n ) F" := + (\big[+%N/0%N]_(m <= i < n) F%N) : (*nat_scope*) big_scope. + +Parameter iter_addn_0 : forall m n : nat, @eq nat (@iter nat n (addn m) O) (muln m n). + +End Mocks. + +Import Mocks. + +(*****************************************************************************) + +Lemma test_big_nested_1 (F G : nat -> nat) (m n : nat) : + \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). +Proof. +(* in interactive mode *) +under eq_bigr => i Hi. + under eq_big => [j|j Hj]. + { rewrite muln1. over. } + { rewrite addnC. over. } + simpl. (* or: cbv beta. *) + over. +by []. +Qed. + +Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) : + \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). +Proof. +(* in one-liner mode *) +under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1 | rewrite addnC ]. +done. +Qed. + +Lemma test_big_2cond_0intro (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in interactive mode *) +under eq_big. +{ move=> n; rewrite (addnC n 1); over. } +{ move=> i Hi; rewrite (addnC i 2); over. } +done. +Qed. + +Lemma test_big_2cond_1intro (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in interactive mode *) +Fail under eq_big => i. +(* as it amounts to [under eq_big => [i]] *) +Abort. + +Lemma test_big_2cond_all (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in interactive mode *) +Fail under eq_big => *. +(* as it amounts to [under eq_big => [*]] *) +Abort. + +Lemma test_big_2cond_all_implied (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in one-liner mode *) +under eq_big do [rewrite addnC + |rewrite addnC]. +(* amounts to [under eq_big => [*|*] do [...|...]] *) +done. +Qed. + +Lemma test_big_patt1 (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (F i + G i) = \sum_(0 <= i < n) (G i + F i) + 0. +Proof. +under [in RHS]eq_bigr => i Hi. + by rewrite addnC over. +done. +Qed. + +Lemma test_big_patt2 (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (F i + F i) = + \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2). +Proof. +under [X in _ = _ + X]eq_bigr => i Hi do rewrite mulnS muln1. +by rewrite big_const_nat iter_addn_0. +Qed. + +Lemma test_big_occs (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0). +Proof. +under {2}[in RHS]eq_bigr => i Hi do rewrite muln0. +by rewrite big_const_nat iter_addn_0. +Qed. + +(* Solely used, one such renaming is useless in practice, but it works anyway *) +Lemma test_big_cosmetic (F G : nat -> nat) (m n : nat) : + \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). +Proof. +under [RHS]eq_bigr => a A do under eq_bigr => b B do []. (* renaming bound vars *) +myadmit. +Qed. + +Lemma test_big_andb (F : nat -> nat) (m n : nat) : + \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1. +Proof. +under eq_bigl => i do [rewrite andb_idl; first by move/eqP->]. +under eq_bigr => i do move/eqP=>{1}->. (* the 2nd occ should not be touched *) +myadmit. +Qed. + +Lemma test_foo (f1 f2 : nat -> nat) (f_eq : forall n, f1 n = f2 n) + (G : (nat -> nat) -> nat) + (Lem : forall f1 f2 : nat -> nat, + True -> + (forall n, f1 n = f2 n) -> + False = False -> + G f1 = G f2) : + G f1 = G f2. +Proof. +(* +under x: Lem. +- done. +- rewrite f_eq; over. +- done. + *) +under Lem => [|x|] do [done|rewrite f_eq|done]. +done. +Qed. + + +(* Inspired From Coquelicot.Lub. *) +(* http://coquelicot.saclay.inria.fr/html/Coquelicot.Lub.html#Lub_Rbar_eqset *) + +Parameters (R Rbar : Set) (R0 : R) (Rbar0 : Rbar). +Parameter Rbar_le : Rbar -> Rbar -> Prop. +Parameter Lub_Rbar : (R -> Prop) -> Rbar. +Parameter Lub_Rbar_eqset : + forall E1 E2 : R -> Prop, + (forall x : R, E1 x <-> E2 x) -> + Lub_Rbar E1 = Lub_Rbar E2. + +Lemma test_Lub_Rbar (E : R -> Prop) : + Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)). +Proof. +under Lub_Rbar_eqset => r. +by rewrite over. +Abort. + + +Lemma ex_iff R (P1 P2 : R -> Prop) : + (forall x : R, P1 x <-> P2 x) -> ((exists x, P1 x) <-> (exists x, P2 x)). +Proof. +by move=> H; split; move=> [x Hx]; exists x; apply H. +Qed. + +Arguments ex_iff [R P1] P2 iffP12. + +Require Import Setoid. +Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True. +under ex_iff => n. +by rewrite over. +Abort. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 0236c549d5..2ec55d1bd0 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -38,6 +38,7 @@ DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) +OCAMLWARN := $(COQMF_WARN) @CONF_FILE@: @PROJECT_FILE@ @COQ_MAKEFILE_INVOCATION@ @@ -176,7 +177,7 @@ COQCHKEXTRAFLAGS?= COQDOCEXTRAFLAGS?= # these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS) +COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS) COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) @@ -190,9 +191,9 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) - # ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) ifneq (,$(TIMING)) TIMING_ARG=-time diff --git a/topbin/dune b/topbin/dune index e35a3de54b..3b861afe78 100644 --- a/topbin/dune +++ b/topbin/dune @@ -28,6 +28,11 @@ (libraries coq.toplevel) (link_flags -linkall)) +(install + (section bin) + (package coq) + (files (coqc_bin.bc as coqc.byte))) + ; Workers (executables (names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin) diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 416ea88c1b..8934385091 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -85,7 +85,7 @@ let ensure_exists f = let compile opts copts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = - let pfs = Vernacstate.Proof_global.get_all_proof_names () in + let pfs = Vernacstate.Proof_global.get_all_proof_names () [@ocaml.warning "-3"] in if not (CList.is_empty pfs) then fatal_error (str "There are pending proofs: " ++ (pfs diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 4129562065..087cd67f3a 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -194,6 +194,7 @@ let make_prompt () = (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ())) ^ " < " with Vernacstate.Proof_global.NoCurrentProof -> "Coq < " + [@@ocaml.warning "-3"] (* the coq prompt added to the default one when in emacs mode The prompt contains the current state label [n] (for global @@ -363,6 +364,7 @@ let top_goal_print ~doc c oldp newp = let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer + [@@ocaml.warning "-3"] let exit_on_error = let open Goptions in diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 038ff54bf6..6c6379ec5e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -70,7 +70,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = (* Force the command *) let ndoc = if check then Stm.observe ~doc nsid else doc in - let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () in + let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3a305c3b61..e44d68b87d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2627,7 +2627,7 @@ let interp ?(verbosely=true) ?proof ~st cmd = try vernac_timeout (fun st -> let v_mod = if verbosely then Flags.verbosely else Flags.silently in let pstate = v_mod (interp_control ?proof ~st) cmd in - Vernacstate.Proof_global.set pstate; + Vernacstate.Proof_global.set pstate [@ocaml.warning "-3"]; Vernacstate.freeze_interp_state ~marshallable:false ) st with exn -> diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b79f97796f..dff81ad9bb 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -82,3 +82,4 @@ module Proof_global : sig val copy_terminators : src:t option -> tgt:t option -> t option end +[@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"] |