diff options
68 files changed, 1185 insertions, 667 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 45597851ef..2444e3982e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -15,7 +15,7 @@ variables: OPAM_SWITCH: "base" # Used to select special compiler switches such as flambda, 32bits, etc... OPAM_VARIANT: "" - GIT_DEPTH: "1" + GIT_DEPTH: "10" docker-boot: stage: docker diff --git a/CHANGES.md b/CHANGES.md index 1f88b77b51..7a4af0d7a8 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -148,6 +148,11 @@ Notations that will do it automatically, using the output of coqc. The script contains documentation on its usage in a comment at the top. +- When several notations are available for the same expression, + priority is given to latest notations defined in the scopes being + opened, in order, rather than to the latest notations defined + independently of whether they are in an opened scope or not. + Tactics - Added toplevel goal selector `!` which expects a single focused goal. diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 96bc5be7ff..688472836e 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -224,7 +224,7 @@ ######################################################################## # simple-io ######################################################################## -: "${simple_io_CI_REF:=master}" +: "${simple_io_CI_REF:=dev}" : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" : "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" diff --git a/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh b/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh new file mode 100644 index 0000000000..3600f1cd3e --- /dev/null +++ b/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh @@ -0,0 +1,18 @@ +if [ "$CI_PULL_REQUEST" = "8705" ] || [ "$CI_BRANCH" = "vernac+remove_empty_hooks" ]; then + + elpi_CI_REF=vernac+remove_empty_hooks + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + equations_CI_REF=vernac+remove_empty_hooks + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + paramcoq_CI_REF=vernac+remove_empty_hooks + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + + plugin_tutorial_CI_REF=vernac+remove_empty_hooks + plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials + + mtac2_CI_REF=vernac+remove_empty_hooks + mtac2_CI_GITURL=https://github.com/ejgallego/mtac2 + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 318562338d..56fdab0c26 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -150,3 +150,24 @@ simplest way of getting them is to run `nix-shell` first. is not out of the box. Installing explicitly "pinentry-mac" seems important for typing of passphrase to work correctly (see also this [Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)). + +## Addendum for organization admins + +### Adding a new code owner individual + +If someone is added to the [`CODEOWNERS`](../../.github/CODEOWNERS) file and +they did not have merging rights before, they should also be added to the +**@coq/pushers** team. You may do so using +[this link](https://github.com/orgs/coq/teams/pushers/members?add=true). + +Before adding someone to the **@coq/pushers** team, you should ensure that they +have read the present merging documentation, and explicitly tell them not to +use the merging button on the GitHub web interface. + +### Adding a new code owner team + +Go to [that page](https://github.com/orgs/coq/teams/pushers/teams) and click on +the green "Add a team" button. Use a "-maintainer" suffix for the name of your +team. You may then add new members to this team (you don't need to add them to +the **@coq/pushers** team first as this will be done automatically because the +team you created is a sub-team of **@coq/pushers**). diff --git a/dev/doc/changes.md b/dev/doc/changes.md index acb0d80c18..c0f15f02a5 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -152,6 +152,12 @@ Termops - Internal printing functions have been placed under the `Termops.Internal` namespace. +Notations: + +- Notation.availability_of_notation is not anymore needed: if a + delimiter is needed, it is provided by Notation.uninterp_notation + which fails in case the notation is not available. + ### Unit testing The test suite now allows writing unit tests against OCaml code in the Coq diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index b33a1cbd73..b1c111685b 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -64,10 +64,8 @@ ## On the date of the feature freeze ## -- [ ] Create the new version branch `vX.X` and - [protect it](https://github.com/coq/coq/settings/branches) - (activate the "Protect this branch", "Require pull request reviews before - merging" and "Restrict who can push to this branch" guards). +- [ ] Create the new version branch `vX.X` (using this name will ensure that + the branch will be automatically protected). - [ ] Remove all remaining unmerged feature PRs from the beta milestone. - [ ] Start a new project to track PR backporting. The proposed model is to have a "X.X-only PRs" column for the rare PRs on the stable branch, a diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 01240a062c..a20b74822c 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the ``:undocumented:`` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: .. cmdv:: Lemma @ident {? @binders} : @type Remark @ident {? @binders} : @type @@ -382,7 +382,7 @@ DO DON'T .. code:: - This is equivalent to ``Axiom`` :token`ident` : :token:`term`. + This is equivalent to ``Axiom`` :token:`ident` : :token:`term`. .. diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 86914a71df..11f0cdc008 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the ``:undocumented:`` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: .. cmdv:: Lemma @ident {? @binders} : @type Remark @ident {? @binders} : @type @@ -138,7 +138,7 @@ DO DON'T .. code:: - This is equivalent to ``Axiom`` :token`ident` : :token:`term`. + This is equivalent to ``Axiom`` :token:`ident` : :token:`term`. .. diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index f899945a35..dcb47d1786 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -60,9 +60,10 @@ margin-right: 0.4em; /* Space for the right half of the sub- and sup-scripts */ } -.notation .hole { +.notation .hole, .std-token .pre { color: #4e9a06; font-style: italic; + font-weight: bold; } /***********************/ diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index cb267576b2..7b8a86d1ab 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -31,9 +31,9 @@ A variable pattern matches any value, and the identifier is bound to that value. The pattern “``_``” (called “don't care” or “wildcard” symbol) also matches any value, but does not bind anything. It may occur an arbitrary number of times in a pattern. Alias patterns written -:n:`(@pattern as @identifier)` are also accepted. This pattern matches the -same values as ``pattern`` does and ``identifier`` is bound to the matched -value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A +:n:`(@pattern as @ident)` are also accepted. This pattern matches the +same values as :token:`pattern` does and :token:`ident` is bound to the matched +value. A pattern of the form :n:`@pattern | @pattern` is called disjunctive. A list of patterns separated with commas is also considered as a pattern and is called *multiple pattern*. However multiple patterns can only occur at the root of pattern matching equations. Disjunctions of diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index f523a39477..e93b01f14d 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -28,7 +28,7 @@ Generating ML Code .. note:: - In the following, a qualified identifier `qualid` + In the following, a qualified identifier :token:`qualid` can be used to refer to any kind of |Coq| global "object" : constant, inductive type, inductive constructor or module name. @@ -47,30 +47,30 @@ extraction. They both display extracted term(s) inside |Coq|. All the following commands produce real ML files. User can choose to produce one monolithic file or one file per |Coq| library. -.. cmd:: Extraction "@file" {+ @qualid } +.. cmd:: Extraction @string {+ @qualid } Recursive extraction of all the mentioned objects and all - their dependencies in one monolithic `file`. + their dependencies in one monolithic file :token:`string`. Global and local identifiers are renamed according to the chosen ML language to fulfill its syntactic conventions, keeping original names as much as possible. .. cmd:: Extraction Library @ident - Extraction of the whole |Coq| library ``ident.v`` to an ML module - ``ident.ml``. In case of name clash, identifiers are here renamed + Extraction of the whole |Coq| library :n:`@ident.v` to an ML module + :n:`@ident.ml`. In case of name clash, identifiers are here renamed using prefixes ``coq_`` or ``Coq_`` to ensure a session-independent renaming. .. cmd:: Recursive Extraction Library @ident - Extraction of the |Coq| library ``ident.v`` and all other modules - ``ident.v`` depends on. + Extraction of the |Coq| library :n:`@ident.v` and all other modules + :n:`@ident.v` depends on. .. cmd:: Separate Extraction {+ @qualid } Recursive extraction of all the mentioned objects and all - their dependencies, just as ``Extraction "file"``, + their dependencies, just as :n:`Extraction @string {+ @qualid }`, but instead of producing one monolithic file, this command splits the produced code in separate ML files, one per corresponding Coq ``.v`` file. This command is hence quite similar to @@ -164,7 +164,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: .. cmd:: Extraction Inline {+ @qualid } In addition to the automatic inline feature, the constants - mentionned by this command will always be inlined during extraction. + mentioned by this command will always be inlined during extraction. .. cmd:: Extraction NoInline {+ @qualid } @@ -214,9 +214,9 @@ principles of extraction (logical parts and types). .. cmd:: Extraction Implicit @qualid [ {+ @ident } ] This experimental command allows declaring some arguments of - `qualid` as implicit, i.e. useless in extracted code and hence to - be removed by extraction. Here `qualid` can be any function or - inductive constructor, and the given `ident` are the names of + :token:`qualid` as implicit, i.e. useless in extracted code and hence to + be removed by extraction. Here :token:`qualid` can be any function or + inductive constructor, and the given :token:`ident` are the names of the concerned arguments. In fact, an argument can also be referred by a number indicating its position, starting from 1. @@ -253,7 +253,7 @@ what ML term corresponds to a given axiom. .. cmd:: Extract Constant @qualid => @string Give an ML extraction for the given constant. - The `string` may be an identifier or a quoted string. + The :token:`string` may be an identifier or a quoted string. .. cmd:: Extract Inlined Constant @qualid => @string @@ -315,24 +315,24 @@ native boolean type instead of the |Coq| one. The syntax is the following: .. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first `string`) and all its - constructors (all the `string` between square brackets). In this form, + extractions for the type itself (first :token:`string`) and all its + constructors (all the :token:`string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native pattern matching of the language will be used. .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string - Same as before, with a final extra `string` that indicates how to + Same as before, with a final extra :token:`string` that indicates how to perform pattern matching over this inductive type. In this form, the ML extraction could be an arbitrary type. - For an inductive type with `k` constructors, the function used to - emulate the pattern matching should expect `(k+1)` arguments, first the `k` + For an inductive type with :math:`k` constructors, the function used to + emulate the pattern matching should expect :math:`k+1` arguments, first the :math:`k` branches in functional form, and then the inductive element to destruct. For instance, the match branch ``| S n => foo`` gives the functional form ``(fun n -> foo)``. Note that a constructor with no arguments is considered to have one unit argument, in order to block early evaluation of the branch: ``| O => bar`` leads to the functional - form ``(fun () -> bar)``. For instance, when extracting ``nat`` + form ``(fun () -> bar)``. For instance, when extracting :g:`nat` into |OCaml| ``int``, the code to be provided has type: ``(unit->'a)->(int->'a)->int->'a``. @@ -410,6 +410,52 @@ It is possible to instruct the extraction not to use particular filenames. For |OCaml|, a typical use of these commands is ``Extraction Blacklist String List``. +Additional settings +~~~~~~~~~~~~~~~~~~~ + +.. opt:: Extraction File Comment @string + :name: Extraction File Comment + + Provides a comment that is included at the beginning of the output files. + +.. opt:: Extraction Flag @num + :name: Extraction Flag + + Controls which optimizations are used during extraction, providing a finer-grained + control than :flag:`Extraction Optimize`. The bits of :token:`num` are used as a bit mask. + Keeping an option off keeps the extracted ML more similar to the Coq term. + Values are: + + +-----+-------+----------------------------------------------------------------+ + | Bit | Value | Optimization (default is on unless noted otherwise) | + +-----+-------+----------------------------------------------------------------+ + | 0 | 1 | Remove local dummy variables | + +-----+-------+----------------------------------------------------------------+ + | 1 | 2 | Use special treatment for fixpoints | + +-----+-------+----------------------------------------------------------------+ + | 2 | 4 | Simplify case with iota-redux | + +-----+-------+----------------------------------------------------------------+ + | 3 | 8 | Factor case branches as functions | + +-----+-------+----------------------------------------------------------------+ + | 4 | 16 | (not available, default false) | + +-----+-------+----------------------------------------------------------------+ + | 5 | 32 | Simplify case as function of one argument | + +-----+-------+----------------------------------------------------------------+ + | 6 | 64 | Simplify case by swapping case and lambda | + +-----+-------+----------------------------------------------------------------+ + | 7 | 128 | Some case optimization | + +-----+-------+----------------------------------------------------------------+ + | 8 | 256 | Push arguments inside a letin | + +-----+-------+----------------------------------------------------------------+ + | 9 | 512 | Use linear let reduction (default false) | + +-----+-------+----------------------------------------------------------------+ + | 10 | 1024 | Use linear beta reduction (default false) | + +-----+-------+----------------------------------------------------------------+ + +.. flag:: Extraction TypeExpand + + If set, fully expand Coq types in ML. See the Coq source code to learn more. + Differences between |Coq| and ML type systems ---------------------------------------------- diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 789890eab5..64e2d7c4ab 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -25,10 +25,10 @@ typed modulo insertion of appropriate coercions. We allow to write: Classes ------- -A class with `n` parameters is any defined name with a type -:g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort. Thus a class with +A class with :math:`n` parameters is any defined name with a type +:n:`forall (@ident__1 : @type__1)..(@ident__n:@type__n), @sort`. Thus a class with parameters is considered as a single class and not as a family of -classes. An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`. +classes. An object of a class is any term of type :n:`@class @term__1 .. @term__n`. In addition to these user-defined classes, we have two built-in classes: @@ -40,20 +40,20 @@ In addition to these user-defined classes, we have two built-in classes: Formally, the syntax of a classes is defined as: .. productionlist:: - class: qualid - : | `Sortclass` - : | `Funclass` + class: `qualid` + : | Sortclass + : | Funclass Coercions --------- A name ``f`` can be declared as a coercion between a source user-defined class -``C`` with `n` parameters and a target class ``D`` if one of these +``C`` with :math:`n` parameters and a target class ``D`` if one of these conditions holds: * ``D`` is a user-defined class, then the type of ``f`` must have the form - :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `m` + :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where :math:`m` is the number of parameters of ``D``. * ``D`` is ``Funclass``, then the type of ``f`` must have the form :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ)(x:A), B`. @@ -124,7 +124,7 @@ Declaring Coercions .. cmd:: Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion between + Declares the construction denoted by :token:`qualid` as a coercion between the two given classes. .. exn:: @qualid not declared. @@ -159,23 +159,18 @@ Declaring Coercions .. cmdv:: Local Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion local to + Declares the construction denoted by :token:`qualid` as a coercion local to the current section. - .. cmdv:: Coercion @ident := @term + .. cmdv:: Coercion @ident := @term {? @type } - This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines :token:`ident` just like :n:`Definition @ident := term {? @type }`, + and then declares :token:`ident` as a coercion between it source and its target. - .. cmdv:: Coercion @ident := @term : @type + .. cmdv:: Local Coercion @ident := @term {? @type } - This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. - - .. cmdv:: Local Coercion @ident := @term - - This defines `ident` just like ``Let`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines :token:`ident` just like :n:`Let @ident := @term {? @type }`, + and then declares :token:`ident` as a coercion between it source and its target. Assumptions can be declared as coercions at declaration time. This extends the grammar of assumptions from @@ -207,10 +202,10 @@ grammar of inductive types from Figure :ref:`vernacular` as follows: \comindex{CoInductive \mbox{\rm (and coercions)}} .. productionlist:: - inductive : `Inductive` ind_body `with` ... `with` ind_body - : | `CoInductive` ind_body `with` ... `with` ind_body - ind_body : ident [binders] : term := [[|] constructor | ... | constructor] - constructor : ident [binders] [:[>] term] + inductive : Inductive `ind_body` with ... with `ind_body` + : | CoInductive `ind_body` with ... with `ind_body` + ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ] + constructor : `ident` [ `binders` ] [:[>] `term` ] Especially, if the extra ``>`` is present in a constructor declaration, this constructor is declared as a coercion. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 5d219ebd0d..fd66de427c 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -248,7 +248,7 @@ cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. -.. [#] Support for `nat` and :math:`\mathbb{N}` is obtained by pre-processing the goal with +.. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with the ``zify`` tactic. .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#] Variants deal with equalities and strict inequalities. diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index e7a8c238ac..ed2e1ea58c 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -81,7 +81,7 @@ performed using :ref:`typeclasses`. produces a goal which states that :math:`c` is not zero. * `variables` is the list of the variables in the decreasing order in - which they will be used in the Buchberger algorithm. If `variables` = `(@nil R)`, + which they will be used in the Buchberger algorithm. If `variables` = :g:`(@nil R)`, then `lvar` is replaced by all the variables which are not in `parameters`. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index e153c7cbe2..56f84d0ff0 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -95,6 +95,14 @@ coercions. (the option is on by default). Coercion of subset types and pairs is still active in this case. +.. flag:: Program Mode + + Enables the program mode, in which 1) typechecking allows subset coercions and + 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and + :cmd:`Program Definition` act + like Program Fixpoint/Definition, generating obligations if there are + unresolved holes after typechecking. + .. _syntactic_control: Syntactic control over equalities @@ -181,7 +189,7 @@ Program Definition Program Fixpoint ~~~~~~~~~~~~~~~~ -.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term +.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term The optional order annotation follows the grammar: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 5bab63f6d0..99d689132d 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -376,8 +376,8 @@ The syntax for adding a new ring is sign :n:`@term` allows :tacn:`ring_simplify` to use a minus operation when outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The - term `:n:`@term` is a proof that a given sign function indicates expressions - that are signed (`term` has to be a proof of ``Ring_theory.get_sign``). See + term :token:`term` is a proof that a given sign function indicates expressions + that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. div :n:`@term` @@ -476,8 +476,8 @@ So now, what is the scheme for a normalization proof? Let p be the polynomial expression that the user wants to normalize. First a little piece of |ML| code guesses the type of `p`, the ring theory `T` to use, an abstract polynomial `ap` and a variables map `v` such that `p` is |bdi|- -equivalent to ``(PEeval`` `v` `ap`\ ``)``. Then we replace it by ``(Pphi_dev`` `v` -``(norm`` `ap`\ ``))``, using the main correctness theorem and we reduce it to a +equivalent to `(PEeval v ap)`. Then we replace it by `(Pphi_dev v (norm ap))`, +using the main correctness theorem and we reduce it to a concrete expression `p’`, which is the concrete normal form of `p`. This is summarized in this diagram: ========= ====== ==== @@ -540,15 +540,15 @@ Dealing with fields .. tacv:: field [{* @term}] - decides the equality of two terms modulo - field operations and the equalities defined - by the :n:`@term`\ s. Each :n:`@term` has to be a proof of some equality - `m` ``=`` `p`, where `m` is a monomial (after “abstraction”), `p` a polynomial - and ``=`` the corresponding equality of the field structure. + This tactic decides the equality of two terms modulo + field operations and the equalities defined + by the :token:`term`\s. Each :token:`term` has to be a proof of some equality + :g:`m = p`, where :g:`m` is a monomial (after “abstraction”), :g:`p` a polynomial + and :g:`=` the corresponding equality of the field structure. .. note:: - rewriting works with the equality `m` ``=`` `p` only if `p` is a polynomial since + Rewriting works with the equality :g:`m = p` only if :g:`p` is a polynomial since rewriting is handled by the underlying ring tactic. .. tacv:: field_simplify @@ -562,27 +562,28 @@ Dealing with fields .. tacv:: field_simplify [{* @term }] - performs the simplification in the conclusion of the goal using the equalities - defined by the :n:`@term`\ s. + This variant performs the simplification in the conclusion of the goal using the equalities + defined by the :token:`term`\s. .. tacv:: field_simplify [{* @term }] {* @term } - performs the simplification in the terms :n:`@terms` of the conclusion of the goal - using the equalities defined by :n:`@term`\ s inside the brackets. + This variant performs the simplification in the terms :token:`term`\s of the conclusion of the goal + using the equalities defined by :token:`term`\s inside the brackets. -.. tacv :: field_simplify in @ident +.. tacv:: field_simplify in @ident - performs the simplification in the assumption :n:`@ident`. + This variant performs the simplification in the assumption :token:`ident`. -.. tacv :: field_simplify [{* @term }] in @ident +.. tacv:: field_simplify [{* @term }] in @ident - performs the simplification - in the assumption :n:`@ident` using the equalities defined by the :n:`@term`\ s. + This variant performs the simplification + in the assumption :token:`ident` using the equalities defined by the :token:`term`\s. .. tacv:: field_simplify [{* @term }] {* @term } in @ident - performs the simplification in the :n:`@term`\ s of the assumption :n:`@ident` using the - equalities defined by the :n:`@term`\ s inside the brackets. + This variant performs the simplification in the :token:`term`\s of the + assumption :token:`ident` using the + equalities defined by the :token:`term`\s inside the brackets. .. tacv:: field_simplify_eq @@ -591,18 +592,17 @@ Dealing with fields .. tacv:: field_simplify_eq [ {* @term }] - performs the simplification in - the conclusion of the goal using the equalities defined by - :n:`@term`\ s. + This variant performs the simplification in + the conclusion of the goal using the equalities defined by :token:`term`\s. .. tacv:: field_simplify_eq in @ident - performs the simplification in the assumption :n:`@ident`. + This variant performs the simplification in the assumption :token:`ident`. .. tacv:: field_simplify_eq [{* @term}] in @ident - performs the simplification in the assumption :n:`@ident` using the equalities defined by - :n:`@terms`\ s and removing the denominator. + This variant performs the simplification in the assumption :token:`ident` + using the equalities defined by :token:`term`\s and removing the denominator. Adding a new field structure diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 98dfcb2373..43d302114e 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -461,12 +461,12 @@ type, like: This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. -Options -~~~~~~~ +Settings +~~~~~~~~ .. flag:: Typeclasses Dependency Order - This option (on by default since 8.6) respects the dependency order + This flag (on by default since 8.6) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend come first, while the non-dependent subgoals were put before the dependent ones previously (Coq 8.5 and below). This can result in @@ -475,7 +475,7 @@ Options .. flag:: Typeclasses Filtered Unification - This option, available since Coq 8.6 and off by default, switches the + This flag, available since Coq 8.6 and off by default, switches the hint application procedure to a filter-then-unify strategy. To apply a hint, we first check that the goal *matches* syntactically the inferred or specified pattern of the hint, and only then try to @@ -483,13 +483,13 @@ Options improve performance by calling unification less often, matching syntactic patterns being very quick. This also provides more control on the triggering of instances. For example, forcing a constant to - explicitely appear in the pattern will make it never apply on a goal + explicitly appear in the pattern will make it never apply on a goal where there is a hole in that place. .. flag:: Typeclasses Limit Intros - This option (on by default) controls the ability to apply hints while + This flag (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It does so by allowing hints that conclude in a product to apply to a goal with a matching product directly, avoiding an introduction. @@ -503,16 +503,16 @@ Options .. flag:: Typeclass Resolution For Conversion - This option (on by default) controls the use of typeclass resolution + This flag (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during elaboration/type - inference. With this option on, when a unification fails, typeclass + inference. With this flag on, when a unification fails, typeclass resolution is tried before launching unification once again. .. flag:: Typeclasses Strict Resolution - Typeclass declarations introduced when this option is set have a - stricter resolution behavior (the option is off by default). When + Typeclass declarations introduced when this flag is set have a + stricter resolution behavior (the flag is off by default). When looking for unifications of a goal with an instance of this class, we “freeze” all the existentials appearing in the goals, meaning that they are considered rigid during unification and cannot be @@ -528,26 +528,40 @@ Options .. flag:: Typeclasses Unique Instances - Typeclass declarations introduced when this option is set have a more - efficient resolution behavior (the option is off by default). When a + Typeclass declarations introduced when this flag is set have a more + efficient resolution behavior (the flag is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical. +.. flag:: Typeclasses Iterative Deepening + + When this flag is set, the proof search strategy is breadth-first search. + Otherwise, the search strategy is depth-first search. The default is off. + :cmd:`Typeclasses eauto` is another way to set this flag. + +.. opt:: Typeclasses Depth @num + :name: Typeclasses Depth + + Sets the maximum proof search depth. The default is unbounded. + :cmd:`Typeclasses eauto` is another way to set this option. + .. flag:: Typeclasses Debug Controls whether typeclass resolution steps are shown during search. Setting this flag - also sets :opt:`Typeclasses Debug Verbosity` to 1. + also sets :opt:`Typeclasses Debug Verbosity` to 1. :cmd:`Typeclasses eauto` + is another way to set this flag. .. opt:: Typeclasses Debug Verbosity @num :name: Typeclasses Debug Verbosity Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving - of goals. Setting this option also sets :flag:`Typeclasses Debug`. + of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this + option to 0 turns that option off. .. flag:: Refine Instance Mode - This option allows to switch the behavior of instance declarations made through + This flag allows to switch the behavior of instance declarations made through the Instance command. + When it is on (the default), instances that have unsolved holes in @@ -560,14 +574,17 @@ Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth + :name: Typeclasses eauto This command allows more global customization of the typeclass resolution tactic. The semantics of the options are: + ``debug`` In debug mode, the trace of successfully applied tactics is - printed. + printed. This value can also be set with :flag:`Typeclasses Debug`. + ``dfs, bfs`` This sets the search strategy to depth-first search (the - default) or breadth-first search. + default) or breadth-first search. This value can also be set with + :flag:`Typeclasses Iterative Deepening`. - + ``depth`` This sets the depth limit of the search. + + ``depth`` This sets the depth limit of the search. This value can also be set with + :opt:`Typeclasses Depth`. diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index d98b8641e9..e681d0f3ff 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -147,7 +147,7 @@ exclude_patterns = [ # The reST default role (used for this markup: `text`) to use for all # documents. -#default_role = None +default_role = 'literal' # Use the Coq domain primary_domain = 'coq' diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 562ed48171..376a6b8eed 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -46,25 +46,26 @@ in which case the correctness of :n:`@type__3` may rely on the instance :n:`@ter The set of rational numbers may be defined as: - .. coqtop:: reset all + .. coqtop:: reset all - Record Rat : Set := mkRat - {sign : bool; - top : nat; - bottom : nat; - Rat_bottom_cond : 0 <> bottom; - Rat_irred_cond : - forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}. + Record Rat : Set := mkRat + { sign : bool + ; top : nat + ; bottom : nat + ; Rat_bottom_cond : 0 <> bottom + ; Rat_irred_cond : + forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1 + }. -Remark here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` and ``Rat_irred_cond`` -depends on both ``top`` and ``bottom``. + Note here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` + and ``Rat_irred_cond`` depends on both ``top`` and ``bottom``. Let us now see the work done by the ``Record`` macro. First the macro generates a variant type definition with just one constructor: -:n:`Variant @ident {? @binders } : @sort := @ident₀ {? @binders }`. +:n:`Variant @ident {? @binders } : @sort := @ident__0 {? @binders }`. -To build an object of type :n:`@ident`, one should provide the constructor -:n:`@ident₀` with the appropriate number of terms filling the fields of the record. +To build an object of type :token:`ident`, one should provide the constructor +:n:`@ident__0` with the appropriate number of terms filling the fields of the record. .. example:: @@ -129,7 +130,7 @@ This syntax can also be used for pattern matching. end). The macro generates also, when it is possible, the projection -functions for destructuring an object of type `\ident`. These +functions for destructuring an object of type :token:`ident`. These projection functions are given the names of the corresponding fields. If a field is named `_` then no projection is built for it. In our example: @@ -163,17 +164,17 @@ available: .. _record_projections_grammar: .. productionlist:: terms - projection : projection `.` ( `qualid` ) - : | projection `.` ( `qualid` `arg` … `arg` ) - : | projection `.` ( @`qualid` `term` … `term` ) + projection : `term` `.` ( `qualid` ) + : | `term` `.` ( `qualid` `arg` … `arg` ) + : | `term` `.` ( @`qualid` `term` … `term` ) Syntax of Record projections -The corresponding grammar rules are given in the preceding grammar. When `qualid` -denotes a projection, the syntax `term.(qualid)` is equivalent to `qualid term`, -the syntax `term.(qualid` |arg_1| |arg_n| `)` to `qualid` |arg_1| `…` |arg_n| `term`, -and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` |term_n| `term`. -In each case, `term` is the object projected and the +The corresponding grammar rules are given in the preceding grammar. When :token:`qualid` +denotes a projection, the syntax :n:`@term.(@qualid)` is equivalent to :n:`@qualid @term`, +the syntax :n:`@term.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term`. +and the syntax :n:`@term.(@@qualid {+ @term })` to :n:`@@qualid {+ @term } @term`. +In each case, :token:`term` is the object projected and the other arguments are the parameters of the inductive type. @@ -197,22 +198,22 @@ other arguments are the parameters of the inductive type. This message is followed by an explanation of this impossibility. There may be three reasons: - #. The name `ident` already exists in the environment (see :cmd:`Axiom`). - #. The body of `ident` uses an incorrect elimination for - `ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). - #. The type of the projections `ident` depends on previous + #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`). + #. The body of :token:`ident` uses an incorrect elimination for + :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). + #. The type of the projections :token:`ident` depends on previous projections which themselves could not be defined. .. exn:: Records declared with the keyword Record or Structure cannot be recursive. - The record name `ident` appears in the type of its fields, but uses - the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. + The record name :token:`ident` appears in the type of its fields, but uses + the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. .. exn:: Cannot handle mutually (co)inductive records. - Records cannot be defined as part of mutually inductive (or - co-inductive) definitions, whether with records only or mixed with - standard definitions. + Records cannot be defined as part of mutually inductive (or + co-inductive) definitions, whether with records only or mixed with + standard definitions. During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in Section @@ -308,7 +309,7 @@ an object of the record type as arguments, and whose body is an application of the unfolded primitive projection of the same name. These constants are used when elaborating partial applications of the projection. One can distinguish them from applications of the primitive -projection if the :flag`Printing Primitive Projection Parameters` option +projection if the :flag:`Printing Primitive Projection Parameters` option is off: For a primitive projection application, parameters are printed as underscores while for the compatibility projections they are printed as usual. @@ -380,7 +381,7 @@ we have the following equivalence | right _ => false end). -Notice that the printing uses the :g:`if` syntax because `sumbool` is +Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is declared as such (see :ref:`controlling-match-pp`). .. _irrefutable-patterns: @@ -653,8 +654,7 @@ with applications only *at the end* of each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the -presence of partial application of `wrong` in the body of -`wrong` : +presence of partial application of :g:`wrong` in the body of :g:`wrong`: .. coqtop:: all @@ -699,21 +699,22 @@ used by ``Function``. A more precise description is given below. .. cmdv:: Function @ident {* @binder } : @type := @term - Defines the not recursive function `ident` as if declared with `Definition`. Moreover - the following are defined: + Defines the not recursive function :token:`ident` as if declared with + :cmd:`Definition`. Moreover the following are defined: - + `ident_rect`, `ident_rec` and `ident_ind`, which reflect the pattern - matching structure of `term` (see :cmd:`Inductive`); - + The inductive `R_ident` corresponding to the graph of `ident` (silently); - + `ident_complete` and `ident_correct` which are inversion information - linking the function and its graph. + + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, + which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); + + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); + + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which + are inversion information linking the function and its graph. .. cmdv:: Function @ident {* @binder } { struct @ident } : @type := @term - Defines the structural recursive function `ident` as if declared with ``Fixpoint``. Moreover the following are defined: + Defines the structural recursive function :token:`ident` as if declared + with :cmd:`Fixpoint`. Moreover the following are defined: + The same objects as above; - + The fixpoint equation of `ident`: `ident_equation`. + + The fixpoint equation of :token:`ident`: :n:`@ident_equation`. .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term Function @ident {* @binder } { wf @term @ident } : @type := @term @@ -722,16 +723,16 @@ used by ``Function``. A more precise description is given below. of the standard library must be loaded for this feature. The ``{}`` annotation is mandatory and must be one of the following: - + ``{measure`` `term` `ident` ``}`` with `ident` being the decreasing argument - and `term` being a function from type of `ident` to ``nat`` for which - value on the decreasing argument decreases (for the ``lt`` order on ``nat``) - at each recursive call of `term`. Parameters of the function are - bound in `term`\ ; - + ``{wf`` `term` `ident` ``}`` with `ident` being the decreasing argument and - `term` an ordering relation on the type of `ident` (i.e. of type + + :n:`{measure @term @ident }` with :token:`ident` being the decreasing argument + and :token:`term` being a function from type of :token:`ident` to :g:`nat` for which + value on the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) + at each recursive call of :token:`term`. Parameters of the function are + bound in :token:`term`; + + :n:`{wf @term @ident }` with :token:`ident` being the decreasing argument and + :token:`term` an ordering relation on the type of :token:`ident` (i.e. of type `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument - decreases at each recursive call of `term`. The order must be well-founded. - Parameters of the function are bound in `term`. + decreases at each recursive call of :token:`term`. The order must be well-founded. + Parameters of the function are bound in :token:`term`. Depending on the annotation, the user is left with some proof obligations that will be used to define the function. These proofs @@ -770,42 +771,42 @@ Section :ref:`gallina-definitions`). .. cmd:: End @ident - This command closes the section named `ident`. After closing of the - section, the local declarations (variables and local definitions) get - *discharged*, meaning that they stop being visible and that all global - objects defined in the section are generalized with respect to the - variables and local definitions they each depended on in the section. + This command closes the section named :token:`ident`. After closing of the + section, the local declarations (variables and local definitions) get + *discharged*, meaning that they stop being visible and that all global + objects defined in the section are generalized with respect to the + variables and local definitions they each depended on in the section. - .. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Section s1. + Section s1. - Variables x y : nat. + Variables x y : nat. - Let y' := y. + Let y' := y. - Definition x' := S x. + Definition x' := S x. - Definition x'' := x' + y'. + Definition x'' := x' + y'. - Print x'. + Print x'. - End s1. + End s1. - Print x'. + Print x'. - Print x''. + Print x''. - Notice the difference between the value of `x’` and `x’’` inside section - `s1` and outside. + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. - .. exn:: This is not the last opened section. - :undocumented: + .. exn:: This is not the last opened section. + :undocumented: .. note:: - Most commands, like ``Hint``, ``Notation``, option management, … which + Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which appear inside a section are canceled when the section is closed. @@ -816,26 +817,26 @@ The module system provides a way of packaging related elements together, as well as a means of massive abstraction. .. productionlist:: modules - module_type : qualid - : | `module_type` with Definition qualid := term - : | `module_type` with Module qualid := qualid - : | qualid qualid … qualid - : | !qualid qualid … qualid - module_binding : ( [Import|Export] ident … ident : module_type ) + module_type : `qualid` + : | `module_type` with Definition `qualid` := `term` + : | `module_type` with Module `qualid` := `qualid` + : | `qualid` `qualid` … `qualid` + : | !`qualid` `qualid` … `qualid` + module_binding : ( [Import|Export] `ident` … `ident` : `module_type` ) module_bindings : `module_binding` … `module_binding` - module_expression : qualid … qualid - : | !qualid … qualid + module_expression : `qualid` … `qualid` + : | !`qualid` … `qualid` Syntax of modules In the syntax of module application, the ! prefix indicates that any `Inline` directive in the type of the functor arguments will be ignored -(see the ``Module Type`` command below). +(see the :cmd:`Module Type` command below). .. cmd:: Module @ident - This command is used to start an interactive module named `ident`. + This command is used to start an interactive module named :token:`ident`. .. cmdv:: Module @ident {* @module_binding} @@ -848,21 +849,22 @@ In the syntax of module application, the ! prefix indicates that any .. cmdv:: Module @ident {* @module_binding} : @module_type - Starts an interactive functor with parameters given by the list of `module binding`, and output module - type `module_type`. + Starts an interactive functor with parameters given by the list of + :token:`module_bindings`, and output module type :token:`module_type`. .. cmdv:: Module @ident <: {+<: @module_type } - Starts an interactive module satisfying each `module_type`. + Starts an interactive module satisfying each :token:`module_type`. .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }. - Starts an interactive functor with parameters given by the list of `module_binding`. The output module type - is verified against each `module_type`. + Starts an interactive functor with parameters given by the list of + :token:`module_binding`. The output module type + is verified against each :token:`module_type`. .. cmdv:: Module [ Import | Export ] - Behaves like ``Module``, but automatically imports or exports the module. + Behaves like :cmd:`Module`, but automatically imports or exports the module. Reserved commands inside an interactive module ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -913,7 +915,7 @@ Reserved commands inside an interactive module .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression Defines a functor with parameters given by module_bindings (possibly none) with body :token:`module_expression`. - The body is checked against each |module_type_i|. + The body is checked against each :n:`@module_type__i`. .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression} @@ -1052,8 +1054,8 @@ specification: the y component is dropped as well as the body of x. End SIG. -The definition of ``N`` using the module type expression ``SIG`` with -``Definition T := nat`` is equivalent to the following one: +The definition of :g:`N` using the module type expression :g:`SIG` with +:g:`Definition T := nat` is equivalent to the following one: .. coqtop:: all @@ -1138,7 +1140,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified. #. Modules and module types can be nested components of each other. #. One can have sections inside a module or a module type, but not a module or a module type inside a section. - #. Commands like ``Hint`` or ``Notation`` can also appear inside modules and + #. Commands like :cmd:`Hint` or :cmd:`Notation` can also appear inside modules and module types. Note that in case of a module definition like: :: @@ -1157,73 +1159,73 @@ component is equal ``nat`` and hence ``M1.T`` as specified. .. cmd:: Import @qualid - If `qualid` denotes a valid basic module (i.e. its module type is a - signature), makes its components available by their short names. + If :token:`qualid` denotes a valid basic module (i.e. its module type is a + signature), makes its components available by their short names. - .. example:: + .. example:: - .. coqtop:: reset all + .. coqtop:: reset all - Module Mod. + Module Mod. - Definition T:=nat. + Definition T:=nat. - Check T. + Check T. - End Mod. + End Mod. - Check Mod.T. + Check Mod.T. - Fail Check T. + Fail Check T. - Import Mod. + Import Mod. - Check T. + Check T. - Some features defined in modules are activated only when a module is - imported. This is for instance the case of notations (see :ref:`Notations`). + Some features defined in modules are activated only when a module is + imported. This is for instance the case of notations (see :ref:`Notations`). - Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` - command. Such declarations are only accessible through their fully - qualified name. + Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` + command. Such declarations are only accessible through their fully + qualified name. - .. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Module A. + Module A. - Module B. + Module B. - Local Definition T := nat. + Local Definition T := nat. - End B. + End B. - End A. + End A. - Import A. + Import A. - Fail Check B.T. + Fail Check B.T. - .. cmdv:: Export @qualid - :name: Export + .. cmdv:: Export @qualid + :name: Export - When the module containing the command Export qualid - is imported, qualid is imported as well. + When the module containing the command ``Export`` qualid + is imported, qualid is imported as well. - .. exn:: @qualid is not a module. - :undocumented: + .. exn:: @qualid is not a module. + :undocumented: - .. warn:: Trying to mask the absolute name @qualid! - :undocumented: + .. warn:: Trying to mask the absolute name @qualid! + :undocumented: .. cmd:: Print Module @ident - Prints the module type and (optionally) the body of the module :n:`@ident`. + Prints the module type and (optionally) the body of the module :token:`ident`. .. cmd:: Print Module Type @ident - Prints the module type corresponding to :n:`@ident`. + Prints the module type corresponding to :token:`ident`. .. flag:: Short Module Printing @@ -1374,7 +1376,7 @@ OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object files as described above. The OCaml loadpath is managed using the option ``-I`` `path` (in the OCaml world, there is neither a notion of logical name prefix nor a way to access files in -subdirectories of path). See the command ``Declare`` ``ML`` ``Module`` in +subdirectories of path). See the command :cmd:`Declare ML Module` in :ref:`compiled-files` to understand the need of the OCaml loadpath. See :ref:`command-line-options` for a more general view over the |Coq| command @@ -1515,7 +1517,6 @@ possible, the correct argument will be automatically generated. .. exn:: Cannot infer a term for this placeholder. :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments) - :undocumented: |Coq| was not able to deduce an instantiation of a “_”. @@ -1803,20 +1804,20 @@ Explicit applications In presence of non-strict or contextual argument, or in presence of partial applications, the synthesis of implicit arguments may fail, so one may have to give explicitly certain implicit arguments of an -application. The syntax for this is ``(`` `ident` ``:=`` `term` ``)`` where `ident` is the +application. The syntax for this is :n:`(@ident := @term)` where :token:`ident` is the name of the implicit argument and term is its corresponding explicit term. Alternatively, one can locally deactivate the hiding of implicit -arguments of a function by using the notation `@qualid` |term_1| … |term_n|. +arguments of a function by using the notation :n:`@qualid {+ @term }`. This syntax extension is given in the following grammar: .. _explicit_app_grammar: .. productionlist:: explicit_apps - term : @ qualid term … `term` - : | @ qualid - : | qualid `argument` … `argument` + term : @ `qualid` `term` … `term` + : | @ `qualid` + : | `qualid` `argument` … `argument` argument : `term` - : | (ident := `term`) + : | (`ident` := `term`) Syntax for explicitly giving implicit arguments @@ -2208,13 +2209,10 @@ existential variable is represented by “?” followed by an identifier. Check identity _ (fun x => _). -In the general case, when an existential variable ``?``\ `ident` appears +In the general case, when an existential variable :n:`?@ident` appears outside of its context of definition, its instance, written under the -form - -| ``{`` :n:`{*; @ident:=@term}` ``}`` - -is appending to its name, indicating how the variables of its defining context are instantiated. +form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +how the variables of its defining context are instantiated. The variables of the context of the existential variables which are instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances` is on (see Section :ref:`explicit-display-existentials`), and this is why an diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index de9e327740..9bc67147f7 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -198,10 +198,10 @@ and ``coqtop``, unless stated otherwise: :-type-in-type: Collapse the universe hierarchy of |Coq|. .. warning:: This makes the logic inconsistent. -:-mangle-names *ident*: Experimental: Do not depend on this option. Replace +:-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, - etc. The command ``Set Mangle Names`` turns the behavior on in a document, - and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature + etc. Within Coq, the flag :flag:`Mangle Names` turns this behavior on, + and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0ea8c7be2d..1071682ead 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1208,7 +1208,7 @@ Interactive debugger .. flag:: Ltac Debug - This option governs the step-by-step debugger that comes with the |Ltac| interpreter + This option governs the step-by-step debugger that comes with the |Ltac| interpreter. When the debugger is activated, it stops at every step of the evaluation of the current |Ltac| expression and prints information on what it is doing. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3ca0ffe678..9fbac95f0c 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -157,14 +157,24 @@ compatible with the rest of |Coq|, up to a few discrepancies: (see :ref:`pattern_conditional_ssr`). To use the generalized form, turn off the |SSR| Boolean ``if`` notation using the command: ``Close Scope boolean_if_scope``. -+ The following two options can be unset to disable the incompatible - rewrite syntax and allow reserved identifiers to appear in scripts. ++ The following flags can be unset to make |SSR| more compatible with + parts of Coq: - .. coqtop:: in +.. flag:: SsrRewrite + + Controls whether the incompatible rewrite syntax is enabled (the default). + Disabling the flag makes the syntax compatible with other parts of Coq. + +.. flag:: SsrIdents - Unset SsrRewrite. - Unset SsrIdents. + Controls whether tactics can refer to |SSR|-generated variables that are + in the form _xxx_. Scripts with explicit references to such variables + are fragile; they are prone to failure if the proof is later modified or + if the details of variable name generation change in future releases of Coq. + The default is on, which gives an error message when the user tries to + create such identifiers. Disabling the flag generates a warning instead, + increasing compatibility with other parts of Coq. |Gallina| extensions -------------------- @@ -3063,6 +3073,17 @@ An :token:`r_item` can be: rewrite -[f y x]/(y + _). +.. flag:: SsrOldRewriteGoalsOrder + + Controls the order in which generated subgoals (side conditions) + are added to the + proof context. The flag is off by default, which puts subgoals generated + by conditional rules first, followed by the main goal. When it is on, + the main goal appears first. If your proofs are organized to complete + proving the main goal before side conditions, turning the flag on will save you + from having to add :tacn:`last first` tactics that would be needed + to keep the main goal as the currently focused goal. + Remarks and examples ~~~~~~~~~~~~~~~~~~~~ @@ -5428,6 +5449,17 @@ right hand side double , view hint declaration see :ref:`declaring_new_hints_ssr prenex implicits declaration see :ref:`parametric_polymorphism_ssr` +Settings +~~~~~~~~ + +.. flag:: Debug Ssreflect + + *Developer only.* Print debug information on reflect. + +.. flag:: Debug SsrMatching + + *Developer only.* Print debug information on SSR matching. + .. rubric:: Footnotes .. [#1] Unfortunately, even after a call to the Set Printing All command, diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 150aadc15a..ad80cb62e1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -264,6 +264,11 @@ Applying theorems This tactic behaves like :tacn:`simple refine` except it performs type checking without resolution of typeclasses. + .. flag:: Debug Unification + + Enables printing traces of unification steps used during + elaboration/typechecking and the :tacn:`refine` tactic. + .. tacn:: apply @term :name: apply @@ -606,6 +611,10 @@ Applying theorems when the instantiation of a variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). +.. flag:: Debug Tactic Unification + + Enables printing traces of unification steps in tactic unification. + Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. .. _managingthelocalcontext: @@ -2096,9 +2105,9 @@ and an explanation of the underlying technique. Part of the behavior of the ``inversion`` tactic is to generate equalities between expressions that appeared in the hypothesis that is being processed. By default, no equalities are generated if they - relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort - :g:`Prop`). This behavior can be turned off by using the option - :flag`Keep Proof Equalities`. + relate two proofs (i.e. equalities between :token:`term`\s whose type is in sort + :g:`Prop`). This behavior can be turned off by using the + :flag:`Keep Proof Equalities` setting. .. tacv:: inversion @num @@ -2534,6 +2543,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. unresolved bindings into existential variables, if any, instead of failing. It has the same variants as :tacn:`rewrite` has. + .. flag:: Keyed Unification + + Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive + unification. The subterms, considered as rewriting candidates, must start with + the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments + are then unified up to full reduction. + .. tacn:: replace @term with @term’ :name: replace @@ -4503,3 +4519,42 @@ user-defined tactics. significant changes in your theories to obtain the same result. As a drawback of the re-engineering of the code, this tactic has also been completely revised to get a very compact and readable version. + +Delaying solving unification constraints +---------------------------------------- + +.. tacn:: solve_constraints + :name: solve_constraints + :undocumented: + +.. flag:: Solve Unification Constraints + + By default, after each tactic application, postponed typechecking unification + problems are resolved using heuristics. Unsetting this flag disables this + behavior, allowing tactics to leave unification constraints unsolved. Use the + :tacn:`solve_constraints` tactic at any point to solve the constraints. + +Proof maintenance +----------------- + +*Experimental.* Many tactics, such as :tacn:`intros`, can automatically generate names, such +as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps +may explicitly refer to these names. However, future versions of Coq may not assign +names exactly the same way, which could cause the proof to fail because the +new names don't match the explicit references in the proof. + +The following "Mangle Names" settings let users find all the +places where proofs rely on automatically generated names, which can +then be named explicitly to avoid any incompatibility. These +settings cause Coq to generate different names, producing errors for +references to automatically generated names. + +.. flag:: Mangle Names + + When set, generated names use the prefix specified in the following + option instead of the default prefix. + +.. opt:: Mangle Names Prefix @string + :name: Mangle Names Prefix + + Specifies the prefix to use when generating names. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 4bc85f386d..a98a46ba21 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -274,8 +274,8 @@ Requests to the environment This searches for all statements or types of definition that contains a subterm that matches the pattern - `term_pattern` (holes of the pattern are either denoted by `_` or by - `?ident` when non linear patterns are expected). + :token:`term_pattern` (holes of the pattern are either denoted by `_` or by + :n:`?@ident` when non linear patterns are expected). .. cmdv:: Search { + [-]@term_pattern_string } @@ -580,7 +580,7 @@ file is a particular case of module called *library file*. replayed nor rechecked. To locate the file in the file system, :n:`@qualid` is decomposed under the - form `dirpath.ident` and the file `ident.vo` is searched in the physical + form :n:`dirpath.@ident` and the file :n:`@ident.vo` is searched in the physical directory of the file system that is mapped in |Coq| loadpath to the logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between physical directories and logical names at the time of requiring the @@ -611,7 +611,7 @@ file is a particular case of module called *library file*. .. cmdv:: Require [Import | Export] {+ @qualid } This loads the - modules named by the :n:`qualid` sequence and their recursive + modules named by the :token:`qualid` sequence and their recursive dependencies. If ``Import`` or ``Export`` is given, it also imports these modules and all the recursive dependencies that were marked or transitively marked @@ -620,8 +620,8 @@ file is a particular case of module called *library file*. .. cmdv:: From @dirpath Require @qualid This command acts as :cmd:`Require`, but picks - any library whose absolute name is of the form dirpath.dirpath’.qualid - for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library + any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid` + for some :n:`@dirpath’`. This is useful to ensure that the :token:`qualid` library comes from a given package by making explicit its absolute root. .. exn:: Cannot load qualid: no physical path bound to dirpath. @@ -637,21 +637,21 @@ file is a particular case of module called *library file*. The command tried to load library file :n:`@ident`.vo that depends on some specific version of library :n:`@qualid` which is not the - one already loaded in the current |Coq| session. Probably `ident.v` was + one already loaded in the current |Coq| session. Probably :n:`@ident.v` was not properly recompiled with the last version of the file containing - module :n:`@qualid`. + module :token:`qualid`. .. exn:: Bad magic number. - The file `ident.vo` was found but either it is not a + The file :n:`@ident.vo` was found but either it is not a |Coq| compiled module, or it was compiled with an incompatible version of |Coq|. - .. exn:: The file `ident.vo` contains library dirpath and not library dirpath’. + .. exn:: The file :n:`@ident.vo` contains library dirpath and not library dirpath’. - The library file `dirpath’` is indirectly required by the + The library file :n:`@dirpath’` is indirectly required by the ``Require`` command but it is bound in the current loadpath to the - file `ident.vo` which was bound to a different library name `dirpath` at + file :n:`@ident.vo` which was bound to a different library name :token:`dirpath` at the time it was compiled. @@ -675,10 +675,10 @@ file is a particular case of module called *library file*. .. cmd:: Declare ML Module {+ @string } This commands loads the OCaml compiled files - with names given by the :n:`@string` sequence + with names given by the :token:`string` sequence (dynamic link). It is mainly used to load tactics dynamically. The files are searched into the current OCaml loadpath (see the - command ``Add ML Path`` in Section :ref:`libraries-and-filesystem`). + command :cmd:`Add ML Path`). Loading of OCaml files is only possible under the bytecode version of ``coqtop`` (i.e. ``coqtop`` called with option ``-byte``, see chapter :ref:`thecoqcommands`), or when |Coq| has been compiled with a @@ -698,9 +698,9 @@ file is a particular case of module called *library file*. .. cmd:: Print ML Modules - This prints the name of all OCaml modules loaded with ``Declare - ML Module``. To know from where these module were loaded, the user - should use the command ``Locate File`` (see :ref:`here <locate-file>`) + This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`. + To know from where these module were loaded, the user + should use the command :cmd:`Locate File`. .. _loadpath: @@ -721,7 +721,7 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Cd @string - This command changes the current directory according to :n:`@string` which + This command changes the current directory according to :token:`string` which can be any valid path. .. cmdv:: Cd @@ -732,24 +732,24 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Add LoadPath @string as @dirpath This command is equivalent to the command line option - ``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current + :n:`-Q @string @dirpath`. It adds the physical directory string to the current |Coq| loadpath and maps it to the logical directory dirpath. .. cmdv:: Add LoadPath @string - Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but + Performs as :n:`Add LoadPath @string @dirpath` but for the empty directory path. .. cmd:: Add Rec LoadPath @string as @dirpath This command is equivalent to the command line option - ``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its + :n:`-R @string @dirpath`. It adds the physical directory string and all its subdirectories to the current |Coq| loadpath. .. cmdv:: Add Rec LoadPath @string - Works as :cmd:`Add Rec LoadPath` :n:`@string` as :n:`@dirpath` but for the empty + Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty logical directory path. @@ -792,7 +792,7 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Locate File @string This command displays the location of file string in the current - loadpath. Typically, string is a .cmo or .vo or .v file. + loadpath. Typically, string is a ``.cmo`` or ``.vo`` or ``.v`` file. .. cmd:: Locate Library @dirpath @@ -858,7 +858,7 @@ interactively, they cannot be part of a vernacular file loaded via state label is an integer which grows after each successful command. It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see above), the :cmd:`BackTo` command now handles proof states. For that, it may - have to undo some extra commands and end on a state `num′ ≤ num` if + have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. .. cmdv:: Backtrack @num @num @num @@ -1157,7 +1157,7 @@ described first. This command allows giving a short name to a reduction expression, for instance lazy beta delta [foo bar]. This short name can then be used - in ``Eval`` :n:`@ident` ``in`` ... or ``eval`` directives. This command + in :n:`Eval @ident in` or ``eval`` directives. This command accepts the Local modifier, for discarding this reduction name at the end of the file or module. For the moment the name cannot be qualified. In @@ -1165,7 +1165,7 @@ described first. functor applications will be refused if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but nothing prevents the user to also perform a - ``Ltac`` `ident` ``:=`` `convtactic`. + :n:`Ltac @ident := @convtactic`. .. seealso:: :ref:`performingcomputations` diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 1c53f5981d..a5869055fa 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1040,6 +1040,8 @@ interpreted in the scope stack extended with the scope bound tokey. To remove a delimiting key of a scope, use the command :n:`Undelimit Scope @scope` +.. _ArgumentScopes: + Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1307,6 +1309,65 @@ Displaying information about scopes It also displays the delimiting key if any and the class to which the scope is bound, if any. +Impact of scopes on printing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When several notations are available for printing the same expression, +Coq will use the following rules for printing priorities: + +- If two notations are available in different scopes which are open, + the notation in the more recently opened scope takes precedence. + +- If two notations are available in the same scope, the more recently + defined (or imported) notation takes precedence. + +- Abbreviations and lonely notations, both of which have no scope, + take precedence over a notation in an open scope if and only if the + abbreviation or lonely notation was defined (or imported) more + recently than when the corresponding scope was open. They take + precedence over any notation not in an open scope, whether this scope + has a delimiter or not. + +- A scope is *active* for printing a term either because it was opened + with :cmd:`Open Scope`, or the term is the immediate argument of a + constant which temporarily opens a scope for this argument (see + :ref:`Arguments <ArgumentScopes>`) in which case this temporary + scope is the most recent open one. + +- In case no abbreviation, nor lonely notation, nor notation in an + explicitly open scope, nor notation in a temporarily open scope of + arguments, has been found, notations in those closed scopes which + have a delimiter are considered, giving priority to the most + recently defined (or imported) ones. The corresponding delimiter is + inserted, making the corresponding scope the most recent explicitly + open scope for all subterms of the current term. As an exception to + the insertion of the corresponding delimiter, when an expression is + statically known to be in a position expecting a type and the + notation is from scope ``type_scope``, and the latter is closed, the + delimiter is not inserted. This is because expressions statically + known to be in a position expecting a type are by default + interpreted with `type_scope` temporarily activated. Expressions + statically known to be in a position expecting a type typically + include being on the right-hand side of `:`, `<:`, `<<:` and after + the comma in a `forall` expression. + +- As a refinement of the previous rule, in the case of applied global + references, notations in a non-opened scope with delimiter + specifically defined for this applied global reference take priority + over notations in a non-opened scope with delimiter for generic + applications. For instance, in the presence of ``Notation "f ( x + )" := (f x) (at level 10, format "f ( x )") : app_scope`` and + ``Notation "x '.+1'" := (S x) (at level 10, format "x '.+1'") : + mynat_scope.`` and both of ``app_scope`` and ``mynat_scope`` being + bound to a delimiter *and* both not opened, the latter, more + specific notation will always take precedence over the first, more + generic one. + +- A scope can be closed by using :cmd:`Close Scope` and its delimiter + removed by using :cmd:`Undelimit Scope`. To remove automatic + temporary opening of scopes for arguments of a constant, use + :ref:`Arguments <ArgumentScopes>`. + .. _Abbreviations: Abbreviations diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 25f2526f74..fba03b9de9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -110,13 +110,13 @@ let deactivate_notation nr = (* shouldn't we check wether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> - match availability_of_notation (scopt, ntn) (scopt, []) with - | None -> user_err ~hdr:"Notation" + if not (exists_notation_interpretation_in_scope scopt ntn) then + user_err ~hdr:"Notation" (pr_notation ntn ++ spc () ++ str "does not exist" ++ (match scopt with | None -> spc () ++ str "in the empty scope." | Some _ -> show_scope scopt ++ str ".")) - | Some _ -> + else if IRuleSet.mem nr !inactive_notations_table then Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () @@ -263,6 +263,11 @@ let rec insert_pat_coercion ?loc l c = match l with | [] -> c | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[]) +let add_lonely keyrule seen = + match keyrule with + | NotationRule (None,ntn) -> ntn::seen + | SynDefRule _ | NotationRule (Some _,_) -> seen + (**********************************************************************) (* conversion of references *) @@ -387,8 +392,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with No_match -> try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_pattern allscopes vars pat - (uninterp_cases_pattern_notations pat) + extern_notation_pattern allscopes [] vars pat + (uninterp_cases_pattern_notations scopes pat) with No_match -> let loc = pat.CAst.loc in match DAst.get pat with @@ -441,18 +446,15 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = insert_pat_coercion coercion pat and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) - (custom, (tmp_scope, scopes) as allscopes) vars = + (custom, (tmp_scope, scopes) as allscopes) lonely_seen vars = function - | NotationRule (sc,ntn) -> + | NotationRule (sc,ntn),key,need_delim -> begin match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - match availability_of_notation (sc,ntn) (tmp_scope,scopes) with - (* Uninterpretation is not allowed in current context *) - | None -> raise No_match - (* Uninterpretation is allowed in current context *) - | Some (scopt,key) -> + let key = if need_delim || List.mem ntn lonely_seen then key else None in + let scopt = match key with Some _ -> sc | _ -> None in let scopes' = Option.List.cons scopt scopes in let l = List.map (fun (c,(subentry,(scopt,scl))) -> @@ -474,7 +476,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (insert_pat_delimiters ?loc (make_pat_notation ?loc ntn (l,ll) l2') key) end - | SynDefRule kn -> + | SynDefRule kn,key,need_delim -> + assert (key = None && need_delim = false); match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> @@ -492,9 +495,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) in assert (List.is_empty substlist); insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2')) -and extern_notation_pattern allscopes vars t = function +and extern_notation_pattern allscopes lonely_seen vars t = function | [] -> raise No_match - | (keyrule,pat,n as _rule)::rules -> + | (keyrule,pat,n as _rule,key,need_delim)::rules -> try if is_inactive_rule keyrule then raise No_match; let loc = t.loc in @@ -502,22 +505,27 @@ and extern_notation_pattern allscopes vars t = function | PatCstr (cstr,args,na) -> let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in let p = apply_notation_to_pattern ?loc (ConstructRef cstr) - (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in + (match_notation_constr_cases_pattern t pat) allscopes lonely_seen vars + (keyrule,key,need_delim) in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) with - No_match -> extern_notation_pattern allscopes vars t rules + No_match -> + let lonely_seen = add_lonely keyrule lonely_seen in + extern_notation_pattern allscopes lonely_seen vars t rules -let rec extern_notation_ind_pattern allscopes vars ind args = function +let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = function | [] -> raise No_match - | (keyrule,pat,n as _rule)::rules -> + | (keyrule,pat,n as _rule,key,need_delim)::rules -> try if is_inactive_rule keyrule then raise No_match; apply_notation_to_pattern (IndRef ind) - (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule + (match_notation_constr_ind_pattern ind args pat) allscopes lonely_seen vars (keyrule,key,need_delim) with - No_match -> extern_notation_ind_pattern allscopes vars ind args rules + No_match -> + let lonely_seen = add_lonely keyrule lonely_seen in + extern_notation_ind_pattern allscopes lonely_seen vars ind args rules let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and @@ -529,8 +537,8 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = else try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_ind_pattern allscopes vars ind args - (uninterp_ind_pattern_notations ind) + extern_notation_ind_pattern allscopes [] vars ind args + (uninterp_ind_pattern_notations scopes ind) with No_match -> let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in @@ -760,32 +768,32 @@ let extern_ref vars ref us = let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) -let rec extern inctx scopes vars r = +let rec extern inctx (custom,scopes as allscopes) vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal (extern_possible_prim_token scopes) r r' + extern_optimal (extern_possible_prim_token allscopes) r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_optimal - (fun r -> extern_notation scopes vars r (uninterp_notations r)) + (fun r -> extern_notation allscopes [] vars r (uninterp_notations scopes r)) r r'' with No_match -> let loc = r'.CAst.loc in match DAst.get r' with - | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) + | GRef (ref,us) when entry_has_global custom -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_ident custom -> CAst.make ?loc (extern_var ?loc id) | c -> - match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with + match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> - let scopes = (InConstrEntrySomeLevel, snd scopes) in + let scopes = (InConstrEntrySomeLevel, scopes) in let c = match c with (* The remaining cases are only for the constr entry *) @@ -797,7 +805,7 @@ let rec extern inctx scopes vars r = | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) | GEvar (n,l) -> - extern_evar n (List.map (on_snd (extern false scopes vars)) l) + extern_evar n (List.map (on_snd (extern false allscopes vars)) l) | GPatVar kind -> if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else @@ -1056,9 +1064,9 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in make ?loc (pll,extern inctx scopes vars c) -and extern_notation (custom,scopes as allscopes) vars t = function +and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function | [] -> raise No_match - | (keyrule,pat,n as _rule)::rules -> + | (keyrule,pat,n as _rule,key,need_delim)::rules -> let loc = Glob_ops.loc_of_glob_constr t in try if is_inactive_rule keyrule then raise No_match; @@ -1106,11 +1114,8 @@ and extern_notation (custom,scopes as allscopes) vars t = function (match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - match availability_of_notation (sc,ntn) scopes with - (* Uninterpretation is not allowed in current context *) - | None -> raise No_match - (* Uninterpretation is allowed in current context *) - | Some (scopt,key) -> + let key = if need_delim || List.mem ntn lonely_seen then key else None in + let scopt = match key with Some _ -> sc | None -> None in let scopes' = Option.List.cons scopt (snd scopes) in let l = List.map (fun (c,(subentry,(scopt,scl))) -> @@ -1146,7 +1151,9 @@ and extern_notation (custom,scopes as allscopes) vars t = function let args = extern_args (extern true) vars args in CAst.make ?loc @@ explicitize false argsimpls (None,e) args with - No_match -> extern_notation allscopes vars t rules + No_match -> + let lonely_seen = add_lonely keyrule lonely_seen in + extern_notation allscopes lonely_seen vars t rules and extern_recursion_order scopes vars = function GStructRec -> CStructRec diff --git a/interp/notation.ml b/interp/notation.ml index db8ee5bc18..0af75b5bfa 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -21,6 +21,7 @@ open Notation_term open Glob_term open Glob_ops open Context.Named.Declaration +open Classops (*i*) @@ -156,6 +157,8 @@ let scope_eq s1 s2 = match s1, s2 with | Scope _, SingleNotation _ | SingleNotation _, Scope _ -> false +(* Scopes for interpretation *) + let scope_stack = ref [] let current_scopes () = !scope_stack @@ -165,14 +168,91 @@ let scope_is_open_in_scopes sc l = let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) +(* Uninterpretation tables *) + +type interp_rule = + | NotationRule of scope_name option * notation + | SynDefRule of KerName.t + +type scoped_notation_rule_core = scope_name * notation * interpretation * int option +type notation_rule_core = interp_rule * interpretation * int option +type notation_rule = notation_rule_core * delimiters option * bool + +(* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and *) + +type uninterp_scope_elem = + | UninterpScope of scope_name + | UninterpSingle of notation_rule_core + +let uninterp_scope_eq_weak s1 s2 = match s1, s2 with +| UninterpScope s1, UninterpScope s2 -> String.equal s1 s2 +| UninterpSingle s1, UninterpSingle s2 -> false +| (UninterpSingle _ | UninterpScope _), _ -> false + +module ScopeOrd = + struct + type t = scope_name option + let compare = Pervasives.compare + end + +module ScopeMap = CMap.Make(ScopeOrd) + +let uninterp_scope_stack = ref [] + +let push_uninterp_scope sc scopes = UninterpScope sc :: scopes + +let push_uninterp_scopes = List.fold_right push_uninterp_scope + +(**********************************************************************) +(* Mapping classes to scopes *) + +type scope_class = cl_typ + +let scope_class_compare : scope_class -> scope_class -> int = + cl_typ_ord + +let compute_scope_class sigma t = + let (cl,_,_) = find_class_type sigma t in + cl + +module ScopeClassOrd = +struct + type t = scope_class + let compare = scope_class_compare +end + +module ScopeClassMap = Map.Make(ScopeClassOrd) + +let initial_scope_class_map : scope_name ScopeClassMap.t = + ScopeClassMap.empty + +let scope_class_map = ref initial_scope_class_map + +let declare_scope_class sc cl = + scope_class_map := ScopeClassMap.add cl sc !scope_class_map + +let find_scope_class cl = + ScopeClassMap.find cl !scope_class_map + +let find_scope_class_opt = function + | None -> None + | Some cl -> try Some (find_scope_class cl) with Not_found -> None + +let current_type_scope_name () = + find_scope_class_opt (Some CL_SORT) + (* TODO: push nat_scope, z_scope, ... in scopes summary *) (* Exportation of scopes *) let open_scope i (_,(local,op,sc)) = - if Int.equal i 1 then + if Int.equal i 1 then begin scope_stack := - if op then sc :: !scope_stack - else List.except scope_eq sc !scope_stack + if op then Scope sc :: !scope_stack + else List.except scope_eq (Scope sc) !scope_stack; + uninterp_scope_stack := + if op then UninterpScope sc :: !uninterp_scope_stack + else List.except uninterp_scope_eq_weak (UninterpScope sc) !uninterp_scope_stack + end let cache_scope o = open_scope 1 o @@ -187,7 +267,7 @@ let discharge_scope (_,(local,_,_ as o)) = let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let inScope : bool * bool * scope_elem -> obj = +let inScope : bool * bool * scope_name -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -196,7 +276,7 @@ let inScope : bool * bool * scope_elem -> obj = classify_function = classify_scope } let open_close_scope (local,opening,sc) = - Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc))) + Lib.add_anonymous_leaf (inScope (local,opening,normalize_scope sc)) let empty_scope_stack = [] @@ -204,9 +284,20 @@ let push_scope sc scopes = Scope sc :: scopes let push_scopes = List.fold_right push_scope +let make_type_scope_soft tmp_scope = + if Option.equal String.equal tmp_scope (current_type_scope_name ()) then + true, None + else + false, tmp_scope + let make_current_scopes (tmp_scope,scopes) = Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) +let make_current_uninterp_scopes (tmp_scope,scopes) = + let istyp,tmp_scope = make_type_scope_soft tmp_scope in + istyp,Option.fold_right push_uninterp_scope tmp_scope + (push_uninterp_scopes scopes !uninterp_scope_stack) + (**********************************************************************) (* Delimiters *) @@ -250,40 +341,80 @@ let find_delimiters_scope ?loc key = user_err ?loc ~hdr:"find_delimiters" (str "Unknown scope delimiting key " ++ str key ++ str ".") -(* Uninterpretation tables *) - -type interp_rule = - | NotationRule of scope_name option * notation - | SynDefRule of KerName.t - (* We define keys for glob_constr and aconstr to split the syntax entries according to the key of the pattern (adapted from Chet Murthy by HH) *) type key = | RefKey of GlobRef.t + | LambdaKey + | ProdKey | Oth let key_compare k1 k2 = match k1, k2 with | RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 -| RefKey _, Oth -> -1 -| Oth, RefKey _ -> 1 -| Oth, Oth -> 0 +| RefKey _, _ -> -1 +| _, RefKey _ -> 1 +| k1, k2 -> Pervasives.compare k1 k2 module KeyOrd = struct type t = key let compare = key_compare end module KeyMap = Map.Make(KeyOrd) -type notation_rule = interp_rule * interpretation * int option - -let keymap_add key interp map = - let old = try KeyMap.find key map with Not_found -> [] in - KeyMap.add key (interp :: old) map +let keymap_add key sc interp (scope_map,global_map) = + (* Adding to scope keymap for printing based on open scopes *) + let oldkeymap = try ScopeMap.find sc scope_map with Not_found -> KeyMap.empty in + let oldscmap = try KeyMap.find key oldkeymap with Not_found -> [] in + let newscmap = KeyMap.add key (interp :: oldscmap) oldkeymap in + let scope_map = ScopeMap.add sc newscmap scope_map in + (* Adding to global keymap of scoped notations in case the scope is not open *) + let global_map = match interp with + | NotationRule (Some sc,ntn), interp, c -> + let oldglobalkeymap = try KeyMap.find key global_map with Not_found -> [] in + KeyMap.add key ((sc,ntn,interp,c) :: oldglobalkeymap) global_map + | (NotationRule (None,_) | SynDefRule _), _, _ -> global_map in + (scope_map, global_map) + +let keymap_extract istype keys sc map = + let keymap = + try ScopeMap.find (Some sc) map + with Not_found -> KeyMap.empty in + let delim = + if istype && Option.equal String.equal (Some sc) (current_type_scope_name ()) then + (* A type is re-interpreted with type_scope on top, so never need a delimiter *) + None + else + (* Pass the delimiter so that it can be used if ever the notation is masked *) + (String.Map.find sc !scope_map).delimiters in + let add_scope rule = (rule,delim,false) in + List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys + +let find_with_delimiters istype = function + | None -> + None + | Some _ as scope when istype && Option.equal String.equal scope (current_type_scope_name ()) -> + (* This is in case type_scope (which by default is open in the + initial state) has been explicitly closed *) + Some None + | Some scope -> + match (String.Map.find scope !scope_map).delimiters with + | Some key -> Some (Some key) + | None -> None -let keymap_find key map = - try KeyMap.find key map - with Not_found -> [] +let rec keymap_extract_remainder istype scope_seen = function + | [] -> [] + | (sc,ntn,interp,c) :: l -> + if String.Set.mem sc scope_seen then keymap_extract_remainder istype scope_seen l + else + match find_with_delimiters istype (Some sc) with + | None -> keymap_extract_remainder istype scope_seen l + | Some delim -> + let rule = (NotationRule (Some sc, ntn), interp, c) in + (rule,delim,true) :: keymap_extract_remainder istype scope_seen l (* Scopes table : interpretation -> scope_name *) -let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) +let notations_key_table = + ref ((ScopeMap.empty, KeyMap.empty) : + notation_rule_core list KeyMap.t ScopeMap.t * + scoped_notation_rule_core list KeyMap.t) let glob_prim_constr_key c = match DAst.get c with | GRef (ref, _) -> Some (canonical_gr ref) @@ -295,12 +426,14 @@ let glob_prim_constr_key c = match DAst.get c with | _ -> None let glob_constr_keys c = match DAst.get c with + | GRef (ref,_) -> [RefKey (canonical_gr ref)] | GApp (c, _) -> begin match DAst.get c with | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth] | _ -> [Oth] end - | GRef (ref,_) -> [RefKey (canonical_gr ref)] + | GLambda _ -> [LambdaKey] + | GProd _ -> [ProdKey] | _ -> [Oth] let cases_pattern_key c = match DAst.get c with @@ -314,6 +447,8 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) RefKey (canonical_gr ref), Some (List.length args) | NRef ref -> RefKey(canonical_gr ref), None | NApp (_,args) -> Oth, Some (List.length args) + | NLambda _ | NBinderList (_,_,NLambda _,_,_) | NList (_,_,NLambda _,_,_) -> LambdaKey, None + | NProd _ | NBinderList (_,_,NProd _,_,_) | NList (_,_,NProd _,_,_) -> ProdKey, None | _ -> Oth, None (**********************************************************************) @@ -839,37 +974,31 @@ let check_required_module ?loc sc (sp,d) = (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) -let find_with_delimiters = function - | None -> None - | Some scope -> - match (String.Map.find scope !scope_map).delimiters with - | Some key -> Some (Some scope, Some key) - | None -> None - -let rec find_without_delimiters find (ntn_scope,ntn) = function - | Scope scope :: scopes -> +let rec find_without_delimiters find (istype,ntn_scope,ntn as ntndata) = function + | UninterpScope scope :: scopes -> (* Is the expected ntn/numpr attached to the most recently open scope? *) begin match ntn_scope with | Some scope' when String.equal scope scope' -> - Some (None,None) + Some None | _ -> (* If the most recently open scope has a notation/numeral printer but not the expected one then we need delimiters *) if find scope then - find_with_delimiters ntn_scope + find_with_delimiters istype ntn_scope else - find_without_delimiters find (ntn_scope,ntn) scopes + find_without_delimiters find ntndata scopes end - | SingleNotation ntn' :: scopes -> + | UninterpSingle (NotationRule (_,ntn'),_,_) :: scopes -> begin match ntn_scope, ntn with | None, Some ntn when notation_eq ntn ntn' -> - Some (None, None) + Some None | _ -> - find_without_delimiters find (ntn_scope,ntn) scopes + find_without_delimiters find ntndata scopes end + | UninterpSingle (SynDefRule _,_,_) :: scopes -> find_without_delimiters find ntndata scopes | [] -> (* Can we switch to [scope]? Yes if it has defined delimiters *) - find_with_delimiters ntn_scope + find_with_delimiters istype ntn_scope (* The mapping between notations and their interpretation *) @@ -902,9 +1031,19 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = | Some _ -> () end +let scope_of_rule = function + | NotationRule (None,_) | SynDefRule _ -> None + | NotationRule (Some sc as sco,_) -> sco + +let uninterp_scope_to_add pat n = function + | NotationRule (None,_) | SynDefRule _ as rule -> Some (UninterpSingle (rule,pat,n)) + | NotationRule (Some sc,_) -> None + let declare_uninterpretation rule (metas,c as pat) = let (key,n) = notation_constr_key c in - notations_key_table := keymap_add key (rule,pat,n) !notations_key_table + let sc = scope_of_rule rule in + notations_key_table := keymap_add key sc (rule,pat,n) !notations_key_table; + uninterp_scope_stack := Option.List.cons (uninterp_scope_to_add pat n rule) !uninterp_scope_stack let rec find_interpretation ntn find = function | [] -> raise Not_found @@ -982,20 +1121,29 @@ let interp_notation ?loc ntn local_scopes = user_err ?loc (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") -let uninterp_notations c = - List.map_append (fun key -> keymap_find key !notations_key_table) - (glob_constr_keys c) +let extract_notations (istype,scopes) keys = + if keys == [] then [] (* shortcut *) else + let scope_map, global_map = !notations_key_table in + let rec aux scopes seen = + match scopes with + | UninterpScope sc :: scopes -> keymap_extract istype keys sc scope_map @ aux scopes (String.Set.add sc seen) + | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes seen + | [] -> + let find key = try KeyMap.find key global_map with Not_found -> [] in + keymap_extract_remainder istype seen (List.flatten (List.map find keys)) + in aux scopes String.Set.empty -let uninterp_cases_pattern_notations c = - keymap_find (cases_pattern_key c) !notations_key_table +let uninterp_notations scopes c = + let scopes = make_current_uninterp_scopes scopes in + extract_notations scopes (glob_constr_keys c) -let uninterp_ind_pattern_notations ind = - keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table +let uninterp_cases_pattern_notations scopes c = + let scopes = make_current_uninterp_scopes scopes in + extract_notations scopes [cases_pattern_key c] -let availability_of_notation (ntn_scope,ntn) scopes = - let f scope = - NotationMap.mem ntn (String.Map.find scope !scope_map).notations in - find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes) +let uninterp_ind_pattern_notations scopes ind = + let scopes = make_current_uninterp_scopes scopes in + extract_notations scopes [RefKey (canonical_gr (IndRef ind))] (* We support coercions from a custom entry at some level to an entry at some level (possibly the same), and from and to the constr entry. E.g.: @@ -1149,13 +1297,11 @@ let availability_of_prim_token n printer_scope local_scopes = | _ -> false with Not_found -> false in - let scopes = make_current_scopes local_scopes in - Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) + let istype,scopes = make_current_uninterp_scopes local_scopes in + find_without_delimiters f (istype,Some printer_scope,None) scopes (* Miscellaneous *) -let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 - let notation_binder_source_eq s1 s2 = match s1, s2 with | NtnParsedAsIdent, NtnParsedAsIdent -> true | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 @@ -1169,9 +1315,10 @@ let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false -let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = +let var_attributes_eq (_, ((entry1, (tmpsc1, scl1)), tp1)) (_, ((entry2, (tmpsc2, scl2)), tp2)) = notation_entry_level_eq entry1 entry2 && - pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && + Option.equal String.equal tmpsc1 tmpsc2 && + List.equal String.equal scl1 scl2 && ntpe_eq tp1 tp2 let interpretation_eq (vars1, t1) (vars2, t2) = @@ -1186,44 +1333,15 @@ let exists_notation_in_scope scopt ntn onlyprint r = interpretation_eq n.not_interp r with Not_found -> false -let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false - -(**********************************************************************) -(* Mapping classes to scopes *) - -open Classops - -type scope_class = cl_typ - -let scope_class_compare : scope_class -> scope_class -> int = - cl_typ_ord - -let compute_scope_class sigma t = - let (cl,_,_) = find_class_type sigma t in - cl - -module ScopeClassOrd = -struct - type t = scope_class - let compare = scope_class_compare -end - -module ScopeClassMap = Map.Make(ScopeClassOrd) - -let initial_scope_class_map : scope_name ScopeClassMap.t = - ScopeClassMap.empty - -let scope_class_map = ref initial_scope_class_map - -let declare_scope_class sc cl = - scope_class_map := ScopeClassMap.add cl sc !scope_class_map - -let find_scope_class cl = - ScopeClassMap.find cl !scope_class_map +let exists_notation_interpretation_in_scope scopt ntn = + let scope = match scopt with Some s -> s | None -> default_scope in + try + let sc = String.Map.find scope !scope_map in + let _ = NotationMap.find ntn sc.notations in + true + with Not_found -> false -let find_scope_class_opt = function - | None -> None - | Some cl -> try Some (find_scope_class cl) with Not_found -> None +let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Special scopes associated to arguments of a global reference *) @@ -1245,9 +1363,6 @@ let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t) let compute_type_scope sigma t = find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None) -let current_type_scope_name () = - find_scope_class_opt (Some CL_SORT) - let scope_class_of_class (x : cl_typ) : scope_class = x @@ -1604,7 +1719,7 @@ let locate_notation prglob ntn scope = str "Notation" ++ fnl () ++ prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in - prlist + prlist_with_sep fnl (fun (sc,r,(_,df)) -> hov 0 ( pr_notation_info prglob df r ++ @@ -1667,17 +1782,18 @@ let pr_visibility prglob = function (* Synchronisation with reset *) let freeze _ = - (!scope_map, !scope_stack, !arguments_scope, + (!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope, !delimiters_map, !notations_key_table, !scope_class_map, !prim_token_interp_infos, !prim_token_uninterp_infos, !entry_coercion_map, !entry_has_global_map, !entry_has_ident_map) -let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = +let unfreeze (scm,scs,uscs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = scope_map := scm; scope_stack := scs; - delimiters_map := dlm; + uninterp_scope_stack := uscs; arguments_scope := asc; + delimiters_map := dlm; notations_key_table := fkm; scope_class_map := clsc; prim_token_interp_infos := ptii; @@ -1688,8 +1804,9 @@ let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = let init () = init_scope_map (); + uninterp_scope_stack := []; delimiters_map := String.Map.empty; - notations_key_table := KeyMap.empty; + notations_key_table := (ScopeMap.empty,KeyMap.empty); scope_class_map := initial_scope_class_map; prim_token_interp_infos := String.Map.empty; prim_token_uninterp_infos := GlobRef.Map.empty diff --git a/interp/notation.mli b/interp/notation.mli index 734198bbf6..3480d1c8f2 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -211,18 +211,28 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) -type notation_rule = interp_rule * interpretation * int option +type notation_rule_core = + interp_rule (* kind of notation *) + * interpretation (* pattern associated to the notation *) + * int option (* number of expected arguments *) + +type notation_rule = + notation_rule_core + * delimiters option (* delimiter to possibly add *) + * bool (* true if the delimiter is mandatory *) (** Return the possible notations for a given term *) -val uninterp_notations : 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : inductive -> notation_rule list +val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list +(* (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) val availability_of_notation : scope_name option * notation -> subscopes -> (scope_name option * delimiters option) option + *) (** {6 Miscellaneous} *) @@ -233,6 +243,9 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> val exists_notation_in_scope : scope_name option -> notation -> bool -> interpretation -> bool +(** Checks for already existing notations *) +val exists_notation_interpretation_in_scope : scope_name option -> notation -> bool + (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index 868042303d..d908baa1e8 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -24,7 +24,6 @@ type project = { v_files : string sourced list; mli_files : string sourced list; - ml4_files : string sourced list; mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; @@ -62,7 +61,6 @@ let mk_project project_file makefile install_kind use_ocamlopt = { v_files = []; mli_files = []; - ml4_files = []; mlg_files = []; ml_files = []; mllib_files = []; @@ -220,7 +218,9 @@ let process_cmd_line ~warning_fn orig_dir proj args = | ".v" -> { proj with v_files = proj.v_files @ [sourced f] } | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } - | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } + | ".ml4" -> + let msg = Printf.sprintf "camlp5 macro files not supported anymore, please port %s to coqpp" f in + raise (Parsing_error msg) | ".mlg" -> { proj with mlg_files = proj.mlg_files @ [sourced f] } | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } @@ -248,9 +248,9 @@ let rec find_project_file ~from ~projfile_name = else find_project_file ~from:newdir ~projfile_name ;; -let all_files { v_files; ml_files; mli_files; ml4_files; mlg_files; +let all_files { v_files; ml_files; mli_files; mlg_files; mllib_files; mlpack_files } = - v_files @ mli_files @ ml4_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files + v_files @ mli_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files let map_sourced_list f l = List.map (fun x -> f x.thing) l ;; diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 20b276ce8c..39c5d019d0 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -22,7 +22,6 @@ type project = { v_files : string sourced list; mli_files : string sourced list; - ml4_files : string sourced list; mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ef1d1af199..3b95423067 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1005,8 +1005,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (mk_equation_id f_id) (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) evd - lemma_type - (Lemmas.mk_hook (fun _ _ -> ())); + lemma_type; ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))); evd diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5ba9735690..4cdfc6fac5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -310,7 +310,6 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) !evd (EConstr.of_constr new_principle_type) - hook ; (* let _tim1 = System.get_time () in *) let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in @@ -326,7 +325,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin match entries with | [entry] -> discard_current (); - (id,(entry,persistence)), CEphemeron.create hook + (id,(entry,persistence)), hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") end @@ -386,7 +385,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) - save false new_princ_name entry g_kind hook + save false new_princ_name entry g_kind ~hook with e when CErrors.noncritical e -> begin begin diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 35acbea488..3a04c753ea 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -415,7 +415,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ~program_mode:false fname (Decl_kinds.Global,false,Decl_kinds.Definition) pl - bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); + bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index c864bfe9f7..19f954c10d 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -129,7 +129,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const (locality,_,kind) hook = +let save with_clean id const ?hook (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> @@ -144,7 +144,7 @@ let save with_clean id const (locality,_,kind) hook = (locality, ConstRef kn) in if with_clean then Proof_global.discard_current (); - CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); + Lemmas.call_hook ?hook ~fix_exn l r; definition_message id let with_full_print f a = diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index c9d153d89f..9584649cff 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -42,8 +42,7 @@ val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr -val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> - Lemmas.declaration_hook CEphemeron.key -> unit +val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d1a227d517..95e2e9f6e5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -806,8 +806,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list lem_id (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) !evd - typ - (Lemmas.mk_hook (fun _ _ -> ())); + typ; ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); @@ -867,8 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma - (fst lemmas_types_infos.(i)) - (Lemmas.mk_hook (fun _ _ -> ())); + (fst lemmas_types_infos.(i)); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 6e5e3f9353..38f27f760b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1372,7 +1372,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) sigma gls_type - (Lemmas.mk_hook hook); + ~hook:(Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () then ignore (by (Proofview.V82.tactic (tclIDTAC))) @@ -1418,7 +1418,7 @@ let com_terminate let evd, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) - ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; + ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref @@ -1474,8 +1474,7 @@ let (com_eqn : int -> Id.t -> (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) evd - (EConstr.of_constr equation_lemma_type) - (Lemmas.mk_hook (fun _ _ -> ())); + (EConstr.of_constr equation_lemma_type); ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fee469032c..06783de614 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1998,7 +1998,7 @@ let add_morphism_infer atts m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook; + Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance); ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism atts binders m s n = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index c4d8072ba5..cf5eb442be 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2048,13 +2048,4 @@ let () = optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "Ltac debug"; - optkey = ["Debug";"Ltac"]; - optread = (fun () -> get_debug () != Tactic_debug.DebugOff); - optwrite = vernac_debug } - let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 095aa36f03..67e19df0e7 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -271,14 +271,6 @@ let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator let get_used_variables () = (cur_pstate ()).section_vars let get_universe_decl () = (cur_pstate ()).universe_decl -let proof_using_auto_clear = ref false -let () = Goptions.(declare_bool_option - { optdepr = false; - optname = "Proof using Clear Unused"; - optkey = ["Proof";"Using";"Clear";"Unused"]; - optread = (fun () -> !proof_using_auto_clear); - optwrite = (fun b -> proof_using_auto_clear := b) }) - let set_used_variables l = let open Context.Named.Declaration in let env = Global.env () in @@ -287,27 +279,26 @@ let set_used_variables l = let ctx_set = List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in - let aux env entry (ctx, all_safe, to_clear as orig) = + let aux env entry (ctx, all_safe as orig) = match entry with | LocalAssum (x,_) -> if Id.Set.mem x all_safe then orig - else (ctx, all_safe, (CAst.make x)::to_clear) + else (ctx, all_safe) | LocalDef (x,bo, ty) as decl -> if Id.Set.mem x all_safe then orig else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in if Id.Set.subset vars all_safe - then (decl :: ctx, Id.Set.add x all_safe, to_clear) - else (ctx, all_safe, (CAst.make x) :: to_clear) in - let ctx, _, to_clear = - Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in - let to_clear = if !proof_using_auto_clear then to_clear else [] in + then (decl :: ctx, Id.Set.add x all_safe) + else (ctx, all_safe) in + let ctx, _ = + Environ.fold_named_context aux env ~init:(ctx,ctx_set) in match !pstates with | [] -> raise NoCurrentProof | p :: rest -> if not (Option.is_empty p.section_vars) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); pstates := { p with section_vars = Some ctx} :: rest; - ctx, to_clear + ctx, [] let get_open_goals () = let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in diff --git a/stm/stm.ml b/stm/stm.ml index 94405924b7..3444229735 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1543,7 +1543,7 @@ end = struct (* {{{ *) let pobject, _ = Proof_global.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 [] (mk_hook (fun _ _ -> ()))) in + Lemmas.(standard_proof_terminator []) in let st = Vernacstate.freeze_interp_state `No in stm_vernac_interp stop @@ -1682,9 +1682,8 @@ end = struct (* {{{ *) `OK_ADMITTED else begin (* The original terminator, a hook, has not been saved in the .vio*) - Proof_global.set_terminator - (Lemmas.standard_proof_terminator [] - (Lemmas.mk_hook (fun _ _ -> ()))); + Proof_global.set_terminator (Lemmas.standard_proof_terminator []); + let opaque = Proof_global.Opaque in let proof = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 719d552def..fd2a163f80 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -121,15 +121,7 @@ let () = optread = get_typeclasses_debug; optwrite = set_typeclasses_debug; } -let () = - declare_bool_option - { optdepr = false; - optname = "debug output for typeclasses proof search"; - optkey = ["Debug";"Typeclasses"]; - optread = get_typeclasses_debug; - optwrite = set_typeclasses_debug; } - -let () = +let _ = declare_int_option { optdepr = false; optname = "verbosity of debug output for typeclasses proof search"; diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 6d65db9e22..5a548cfae4 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,6 +1,6 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in - "A -> list' A -> list' (A * A)%type". + "A -> list' A -> list' (A * A)". Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 94b86fc222..bec4fc1579 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -72,7 +72,7 @@ Nil : forall A : Type, list A NIL : list nat : list nat -(false && I 3)%bool /\ I 6 +(false && I 3)%bool /\ (I 6)%bool : Prop [|1, 2, 3; 4, 5, 6|] : Z * Z * Z * (Z * Z * Z) diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index adab324cf0..2ffc3b14e2 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)). Section A. -Notation "! A" := (forall _:nat, A) (at level 60). +Notation "! A" := (forall _:nat, A) (at level 60) : type_scope. Check ! (0=0). Check forall n, n=0. @@ -195,9 +195,9 @@ Open Scope nat_scope. Coercion is_true := fun b => b=true. Coercion of_nat n := match n with 0 => true | _ => false end. -Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10). +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope. -Check (false && I 3)%bool /\ I 6. +Check (false && I 3)%bool /\ (I 6)%bool. (**********************************************************************) (* Check notations with several recursive patterns *) diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index bcb2468792..923caedace 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -71,6 +71,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* Note: does not work for pattern *) Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). +Open Scope nat_scope. Check fun f x => f x + S x. Open Scope list_scope. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 48379f713d..f53313def9 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -128,25 +128,27 @@ return (1, 2, 3, 4) : nat *(1.2) : nat -! '{{x, y}}, x.y = 0 +! '{{x, y}}, x + y = 0 : Prop exists x : nat, nat -> exists y : nat, - nat -> exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x.y = 0 /\ u.t = 0 + nat -> + exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0 : Prop exists x : nat, nat -> exists y : nat, - nat -> exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x.y = 0 /\ z.t = 0 + nat -> + exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0 : Prop -exists_true '{{x, y}} (u := 0) '{{z, t}}, x.y = 0 /\ z.t = 0 +exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0 : Prop exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), (forall x : A, R x x) : Prop exists_true (x : nat) (A : Type) (R : A -> A -> Prop) -(_ : Reflexive R) (y : nat), x.y = 0 -> forall z : A, R z z +(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z : Prop {{{{True, nat -> True}}, nat -> True}} : Prop * Prop * Prop @@ -182,22 +184,22 @@ pair (prod nat (prod nat nat))) (prod (prod nat nat) nat) fun x : nat => if x is n .+ 1 then n else 1 : nat -> nat -{'{{x, y}} : nat * nat | x.y = 0} +{'{{x, y}} : nat * nat | x + y = 0} : Set exists2' {{x, y}}, x = 0 & y = 0 : Prop myexists2 x : nat * nat, let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y : Prop -fun '({{x, y}} as z) => x.y = 0 /\ z = z +fun '({{x, y}} as z) => x + y = 0 /\ z = z : nat * nat -> Prop -myexists ({{x, y}} as z), x.y = 0 /\ z = z +myexists ({{x, y}} as z), x + y = 0 /\ z = z : Prop -exists '({{x, y}} as z), x.y = 0 /\ z = z +exists '({{x, y}} as z), x + y = 0 /\ z = z : Prop -∀ '({{x, y}} as z), x.y = 0 /\ z = z +∀ '({{x, y}} as z), x + y = 0 /\ z = z : Prop -fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x.y +fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y : nat * nat * bool -> nat myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y : Prop @@ -209,17 +211,17 @@ fun p : nat => if p is S n then n else 0 : nat -> nat fun p : comparison => if p is Lt then 1 else 0 : comparison -> nat -fun S : nat => [S | S.S] +fun S : nat => [S | S + S] : nat -> nat * (nat -> nat) -fun N : nat => [N | N.0] +fun N : nat => [N | N + 0] : nat -> nat * (nat -> nat) -fun S : nat => [[S | S.S]] +fun S : nat => [[S | S + S]] : nat -> nat * (nat -> nat) {I : nat | I = I} : Set {'I : True | I = I} : Prop -{'{{x, y}} : nat * nat | x.y = 0} +{'{{x, y}} : nat * nat | x + y = 0} : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop @@ -253,3 +255,17 @@ myfoo01 tt : nat myfoo01 tt : nat +[{0; 0}] + : list (list nat) +[{1; 2; 3}; + {4; 5; 6}; + {7; 8; 9}] + : list (list nat) +Monomorphic amatch = mmatch 0 (with 0 => 1| 1 => 2 end) + : unit + +amatch is not universe polymorphic +Monomorphic alist = [0; 1; 2] + : list nat + +alist is not universe polymorphic diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 180e8d337e..15211f1233 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. (* Notations with variables bound both as a term and as a binder *) (* This is #4592 *) -Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)). +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. Check forall n:nat, {# n | 1 > n}. Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. @@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4). (* Test spacing in #5569 *) +Section S1. +Variable plus : nat -> nat -> nat. +Infix "+" := plus. Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. +End S1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). @@ -193,10 +197,12 @@ Check !!! (x y:nat), True. (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) -Notation "* x" := (id x) (only printing, at level 15, format "* x"). -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Section S2. +Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope. +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope. Check (((id 1) + 2) + 3). Check (id (1 + 2)). +End S2. (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) (* for isolated "forall" (was not working already in 8.6) *) @@ -410,3 +416,58 @@ Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) End Issue8126. + +(* Test printing of notations guided by scope *) + +Module A. + +Declare Scope line_scope. +Delimit Scope line_scope with line. +Declare Scope matx_scope. +Notation "{ }" := nil (format "{ }") : line_scope. +Notation "{ x }" := (cons x nil) : line_scope. +Notation "{ x ; y ; .. ; z }" := (cons x (cons y .. (cons z nil) ..)) : line_scope. +Notation "[ ]" := nil (format "[ ]") : matx_scope. +Notation "[ l ]" := (cons l%line nil) : matx_scope. +Notation "[ l ; l' ; .. ; l'' ]" := (cons l%line (cons l'%line .. (cons l''%line nil) ..)) + (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope. + +Open Scope matx_scope. +Check [[0;0]]. +Check [[1;2;3];[4;5;6];[7;8;9]]. + +End A. + +(* Example by Beta Ziliani *) + +Require Import Lists.List. + +Module B. + +Import ListNotations. + +Declare Scope pattern_scope. +Delimit Scope pattern_scope with pattern. + +Declare Scope patterns_scope. +Delimit Scope patterns_scope with patterns. + +Notation "a => b" := (a, b) (at level 201) : pattern_scope. +Notation "'with' p1 | .. | pn 'end'" := + ((cons p1%pattern (.. (cons pn%pattern nil) ..))) + (at level 91, p1 at level 210, pn at level 210) : patterns_scope. + +Definition mymatch (n:nat) (l : list (nat * nat)) := tt. +Arguments mymatch _ _%patterns. +Notation "'mmatch' n ls" := (mymatch n ls) (at level 0). + +Close Scope patterns_scope. +Close Scope pattern_scope. + +Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end. +Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *) + +Definition alist := [0;1;2]. +Print alist. + +End B. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index d25ad5dca8..d58e4bf2d6 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -21,3 +21,27 @@ Let "x" e1 e2 : expr Let "x" e1 e2 : expr +fun x : nat => (# x)%nat + : nat -> nat +fun x : nat => ## x + : nat -> nat +fun x : nat => # x + : nat -> nat +fun x : nat => ### x + : nat -> nat +fun x : nat => ## x + : nat -> nat +fun x : nat => (x.-1)%pred + : nat -> nat +∀ a : nat, a = 0 + : Prop +((∀ a : nat, a = 0) -> True)%type + : Prop +# + : Prop +# -> True + : Prop +((∀ a : nat, a = 0) -> True)%type + : Prop +## + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 7800e91ee5..61206b6dd0 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -5,8 +5,8 @@ Module A. Declare Custom Entry myconstr. Notation "[ x ]" := x (x custom myconstr at level 6). -Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5). -Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). +Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5) : nat_scope. +Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4) : nat_scope. Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. @@ -94,3 +94,73 @@ Coercion App : expr >-> Funclass. Check (Let "x" e1 e2). End D. + +(* Check fix of #8551: a delimiter should be inserted because the + lonely notation hides the scope nat_scope, even though the latter + is open *) + +Module E. + +Notation "# x" := (S x) (at level 20) : nat_scope. +Notation "# x" := (Some x). +Check fun x => (# x)%nat. + +End E. + +(* Other tests of precedence *) + +Module F. + +Notation "# x" := (S x) (at level 20) : nat_scope. +Notation "## x" := (S x) (at level 20). +Check fun x => S x. +Open Scope nat_scope. +Check fun x => S x. +Notation "### x" := (S x) (at level 20) : nat_scope. +Check fun x => S x. +Close Scope nat_scope. +Check fun x => S x. + +End F. + +(* Lower priority of generic application rules *) + +Module G. + +Declare Scope predecessor_scope. +Delimit Scope predecessor_scope with pred. +Declare Scope app_scope. +Delimit Scope app_scope with app. +Notation "x .-1" := (Nat.pred x) (at level 10, format "x .-1") : predecessor_scope. +Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope. +Check fun x => pred x. + +End G. + +(* Checking arbitration between in the presence of a notation in type scope *) + +Module H. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. +Check forall a, a = 0. + +Close Scope type_scope. +Check ((forall a, a = 0) -> True)%type. +Open Scope type_scope. + +Notation "#" := (forall a, a = 0). +Check #. +Check # -> True. + +Close Scope type_scope. +Check (# -> True)%type. +Open Scope type_scope. + +Declare Scope my_scope. +Notation "##" := (forall a, a = 0) : my_scope. +Open Scope my_scope. +Check ##. + +End H. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index b673225e40..4372ac72ae 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -102,7 +102,7 @@ CAMLOPTC ?= "$(OCAMLFIND)" opt -c CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack # DESTDIR is prepended to all installation paths DESTDIR ?= @@ -226,7 +226,6 @@ COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) VDFILE := .coqdeps ALLSRCFILES := \ - $(ML4FILES) \ $(MLGFILES) \ $(MLFILES) \ $(MLPACKFILES) \ @@ -248,7 +247,6 @@ BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) TEXFILES = $(VFILES:.v=.tex) GTEXFILES = $(VFILES:.v=.g.tex) CMOFILES = \ - $(ML4FILES:.ml4=.cmo) \ $(MLGFILES:.mlg=.cmo) \ $(MLFILES:.ml=.cmo) \ $(MLPACKFILES:.mlpack=.cmo) @@ -265,7 +263,7 @@ CMXSFILES = \ $(MLPACKFILES:.mlpack=.cmxs) \ $(CMXAFILES:.cmxa=.cmxs) \ $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) + $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) # files that are packed into a plugin (no extension) PACKEDFILES = \ @@ -583,14 +581,6 @@ $(MLIFILES:.mli=.cmi): %.cmi: %.mli $(SHOW)'CAMLC -c $<' $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< -$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 - $(SHOW)'CAMLC -pp -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $< - -$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 - $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< - $(MLGFILES:.mlg=.ml): %.ml: %.mlg $(SHOW)'COQPP $<' $(HIDE)$(COQPP) $< @@ -642,7 +632,7 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ # This rule is for _CoqProject with no .mllib nor .mlpack -$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -o $@ $< @@ -703,17 +693,13 @@ endif redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) -GENMLFILES:=$(MLGFILES:.mlg=.ml) $(ML4FILES:.ml4=.ml) +GENMLFILES:=$(MLGFILES:.mlg=.ml) $(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) $(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli $(SHOW)'CAMLDEP $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) -$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 - $(SHOW)'CAMLDEP -pp $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) - $(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml $(SHOW)'CAMLDEP $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 84850e7158..41057a79e0 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -136,7 +136,7 @@ type vodep = { deps : string list; } -type ldep = | VO of vodep | ML4 of string | MLG of string +type ldep = | VO of vodep | MLG of string type ddir = ldep list DirMap.t (* Filter `.vio` etc... *) @@ -181,19 +181,13 @@ let pp_vo_dep dir fmt vo = let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in pp_rule fmt [vo.target] deps action -let pp_ml4_dep _dir fmt ml = - let target = Filename.(remove_extension ml) ^ ".ml" in - let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in - pp_rule fmt [target] [ml] ml4_rule - let pp_mlg_dep _dir fmt ml = let target = Filename.(remove_extension ml) ^ ".ml" in - let ml4_rule = "(run coqpp %{pp-file})" in - pp_rule fmt [target] [ml] ml4_rule + let mlg_rule = "(run coqpp %{pp-file})" in + pp_rule fmt [target] [ml] mlg_rule let pp_dep dir fmt oo = match oo with | VO vo -> pp_vo_dep dir fmt vo - | ML4 f -> pp_ml4_dep dir fmt f | MLG f -> pp_mlg_dep dir fmt f let out_install fmt dir ff = @@ -220,21 +214,17 @@ let record_dune d ff = eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd (* File Scanning *) -let choose_ml4g_form f = - if Filename.check_suffix f ".ml4" then ML4 f - else MLG f - -let scan_mlg4 m d = +let scan_mlg m d = let dir = ["plugins"; d] in let m = DirMap.add dir [] m in - let ml4 = Sys.(List.filter (fun f -> Filename.(check_suffix f ".ml4" || check_suffix f ".mlg")) + let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg")) Array.(to_list @@ readdir (bpath dir))) in - List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4 + List.fold_left (fun m f -> add_map_list ["plugins"; d] (MLG f) m) m mlg let scan_plugins m = let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in - List.fold_left scan_mlg4 m dirs + List.fold_left scan_mlg m dirs (* Process .vfiles.d and generate a skeleton for the dune file *) let parse_coqdep_line l = diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 8560bac786..5fd894e908 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -218,7 +218,7 @@ let generate_conf_coq_config oc = ;; let generate_conf_files oc - { v_files; mli_files; ml4_files; mlg_files; ml_files; mllib_files; mlpack_files; } + { v_files; mli_files; mlg_files; ml_files; mllib_files; mlpack_files; } = let module S = String in let map = map_sourced_list in @@ -226,7 +226,6 @@ let generate_conf_files oc fprintf oc "COQMF_VFILES = %s\n" (S.concat " " (map quote v_files)); fprintf oc "COQMF_MLIFILES = %s\n" (S.concat " " (map quote mli_files)); fprintf oc "COQMF_MLFILES = %s\n" (S.concat " " (map quote ml_files)); - fprintf oc "COQMF_ML4FILES = %s\n" (S.concat " " (map quote ml4_files)); fprintf oc "COQMF_MLGFILES = %s\n" (S.concat " " (map quote mlg_files)); fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files)); fprintf oc "COQMF_MLLIBFILES = %s\n" (S.concat " " (map quote mllib_files)); @@ -284,7 +283,7 @@ let generate_conf oc project args = let ensure_root_dir ({ ml_includes; r_includes; q_includes; - v_files; ml_files; mli_files; ml4_files; mlg_files; + v_files; ml_files; mli_files; mlg_files; mllib_files; mlpack_files } as project) = let exists f = List.exists (forget_source > f) in @@ -294,7 +293,7 @@ let ensure_root_dir || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes || (not_tops v_files && - not_tops mli_files && not_tops ml4_files && not_tops mlg_files && + not_tops mli_files && not_tops mlg_files && not_tops ml_files && not_tops mllib_files && not_tops mlpack_files) then project diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 713b2ad2b6..db2031c64b 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -62,7 +62,7 @@ let basename_noext filename = (** ML Files specified on the command line. In the entries: - the first string is the basename of the file, without extension nor directory part - - the second string of [mlAccu] is the extension (either .ml or .ml4) + - the second string of [mlAccu] is the extension (either .ml or .mlg) - the [dir] part is the directory, with None used as the current directory *) @@ -496,9 +496,9 @@ let rec suffixes = function let add_caml_known phys_dir _ f = let basename,suff = - get_extension f [".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] in + get_extension f [".ml";".mli";".mlg";".mllib";".mlpack"] in match suff with - | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff + | ".ml"|".mlg" -> add_ml_known basename (Some phys_dir) suff | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff @@ -584,12 +584,12 @@ let rec treat_file old_dirname old_name = in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> - (match get_extension name [".v";".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] with + (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with | (base,".v") -> let name = file_name base dirname and absname = absolute_file_name base dirname in addQueue vAccu (name, absname) - | (base,(".ml"|".ml4"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname) + | (base,(".ml"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname) | (base,".mli") -> addQueue mliAccu (base,dirname) | (base,".mllib") -> addQueue mllibAccu (base,dirname) | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 155296362f..680c8f30ae 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -145,9 +145,9 @@ let mllibAccu = ref ([] : (string * dir) list) let mlpackAccu = ref ([] : (string * dir) list) let add_caml_known phys_dir f = - let basename,suff = get_extension f [".ml";".ml4";".mlg";".mlpack"] in + let basename,suff = get_extension f [".ml";".mlg";".mlpack"] in match suff with - | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff + | ".ml"|".mlg" -> add_ml_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () diff --git a/vernac/classes.ml b/vernac/classes.ml index 7d6bd1ca64..d0cf1c6bee 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -163,10 +163,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id in obls, Some constr, typ | None -> [||], None, termtype in - let hook = Obligations.mk_univ_hook hook in + let univ_hook = Obligations.mk_univ_hook hook in let ctx = Evd.evar_universe_context sigma in ignore (Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls) + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls) else Flags.silently (fun () -> (* spiwack: it is hard to reorder the actions to do @@ -176,7 +176,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) - (Lemmas.mk_hook + ~hook:(Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) if not (Option.is_empty term) then @@ -423,8 +423,7 @@ let context poly l = | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in - let hook = Lemmas.mk_hook (fun _ _ -> ()) in - let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in + let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 9c80f1d2f5..79d45880fc 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -90,7 +90,7 @@ let check_definition (ce, evd, _, imps) = check_evars_are_solved env evd; ce -let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = +let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = let (ce, evd, univdecl, imps as def) = interp_definition univdecl bl (pi2 k) red_option c ctypopt in @@ -108,8 +108,8 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = Obligations.eterm_obligations env ident evd 0 c typ in let ctx = Evd.evar_universe_context evd in - let hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in + let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in ignore(Obligations.add_definition - ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) + ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls) else let ce = check_definition def in - ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps hook) + ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 58007e6a88..0ac5762f71 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -17,9 +17,10 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition : program_mode:bool -> + ?hook:Lemmas.declaration_hook -> Id.t -> definition_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> - constr_expr option -> Lemmas.declaration_hook -> unit + constr_expr option -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 274c99107f..77227b64e6 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -261,7 +261,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) - evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + evd pl (Some(false,indexes,init_tac)) thms None else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -296,7 +296,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) - evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + evd pl (Some(true,[],init_tac)) thms None else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index ebedfb1e0d..e62ae99159 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -227,7 +227,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) - let hook = Obligations.mk_univ_hook (hook sigma) in + let univ_hook = Obligations.mk_univ_hook (hook sigma) in (* XXX: Grounding non-ground terms here... bad bad *) let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in let fullctyp = EConstr.to_constr sigma typ in @@ -237,7 +237,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl - evars_typ ctx evars ~hook) + evars_typ ctx evars ~univ_hook) let out_def = function | Some def -> def diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 2fe03a8ec5..74b59735a9 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -33,7 +33,7 @@ let get_locality id ~kind = function | Local -> true | Global -> false -let declare_definition ident (local, p, k) ce pl imps hook = +let declare_definition ident (local, p, k) ?hook ce pl imps = let fix_exn = Future.fix_exn_of ce.const_entry_body in let gr = match local with | Discharge when Lib.sections_are_opened () -> @@ -49,8 +49,8 @@ let declare_definition ident (local, p, k) ce pl imps hook = in let () = maybe_declare_manual_implicits false gr imps in let () = definition_message ident in - Lemmas.call_hook fix_exn hook local gr; gr + Lemmas.call_hook ~fix_exn ?hook local gr; gr let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ _ -> ())) + declare_definition f kind ce pl imps diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index da11d4d9c0..b5dacf9ea0 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -14,8 +14,9 @@ open Decl_kinds val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool val declare_definition : Id.t -> definition_kind -> + ?hook:Lemmas.declaration_hook -> Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> - Lemmas.declaration_hook -> GlobRef.t + GlobRef.t val declare_fix : ?opaque:bool -> definition_kind -> UnivNames.universe_binders -> Entries.constant_universes_entry -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 28e80a74aa..1a6eda446c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -36,11 +36,12 @@ module NamedDecl = Context.Named.Declaration type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit let mk_hook hook = hook -let call_hook fix_exn hook l c = - try hook l c +let call_hook ?hook ?fix_exn l c = + try Option.iter (fun hook -> hook l c) hook with e when CErrors.noncritical e -> let e = CErrors.push e in - iraise (fix_exn e) + let e = Option.cata (fun fix -> fix e) e fix_exn in + iraise e (* Support for mutually proved theorems *) @@ -202,7 +203,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = gr in definition_message id; - call_hook (fun exn -> exn) hook locality r + call_hook ?hook locality r with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) @@ -288,7 +289,7 @@ let warn_let_as_axiom = (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ spc () ++ strbrk "declared as an axiom.") -let admit (id,k,e) pl hook () = +let admit ?hook (id,k,e) pl () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in let () = match k with | Global, _, _ -> () @@ -296,16 +297,17 @@ let admit (id,k,e) pl hook () = in let () = assumption_message id in Declare.declare_univ_binders (ConstRef kn) pl; - call_hook (fun exn -> exn) hook Global (ConstRef kn) + call_hook ?hook Global (ConstRef kn) (* Starting a goal *) -let universe_proof_terminator compute_guard hook = +let universe_proof_terminator ?univ_hook compute_guard = let open Proof_global in make_terminator begin function | Admitted (id,k,pe,ctx) -> - admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) (); - Feedback.feedback Feedback.AddedAxiom + let hook = Option.map (fun univ_hook -> univ_hook (Some ctx)) univ_hook in + admit ?hook (id,k,pe) (UState.universe_binders ctx) (); + Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) -> let is_opaque, export_seff = match opaque with | Transparent -> false, true @@ -315,13 +317,15 @@ let universe_proof_terminator compute_guard hook = let id = match idopt with | None -> id | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - save ~export_seff id const universes compute_guard persistence (hook (Some universes)) + let hook = Option.map (fun univ_hook -> univ_hook (Some universes)) univ_hook in + save ~export_seff id const universes compute_guard persistence hook | Proved (opaque,idopt, _ ) -> CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") end -let standard_proof_terminator compute_guard hook = - universe_proof_terminator compute_guard (fun _ -> hook) +let standard_proof_terminator ?hook compute_guard = + let univ_hook = Option.map (fun hook _ -> hook) hook in + universe_proof_terminator ?univ_hook compute_guard let initialize_named_context_for_proof () = let sign = Global.named_context () in @@ -331,10 +335,10 @@ let initialize_named_context_for_proof () = let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = +let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c = let terminator = match terminator with - | None -> standard_proof_terminator compute_guard hook - | Some terminator -> terminator compute_guard hook + | None -> standard_proof_terminator ?hook compute_guard + | Some terminator -> terminator ?hook compute_guard in let sign = match sign with @@ -344,10 +348,11 @@ let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = let goals = [ Global.env_of_context sign , c ] in Proof_global.start_proof sigma id ?pl kind goals terminator -let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = +let start_proof_univs id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?univ_hook c = let terminator = match terminator with - | None -> universe_proof_terminator compute_guard hook - | Some terminator -> terminator compute_guard hook + | None -> + universe_proof_terminator ?univ_hook compute_guard + | Some terminator -> terminator ?univ_hook compute_guard in let sign = match sign with @@ -371,7 +376,7 @@ let rec_tac_initializer finite guard thms snl = | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_proof_with_initialization kind sigma decl recguard thms snl hook = +let start_proof_with_initialization ?hook kind sigma decl recguard thms snl = let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> @@ -405,14 +410,14 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; - call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ~pl:decl kind sigma t (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard; + call_hook ?hook strength ref) thms_data in + start_proof_univs id ~pl:decl kind sigma t ~univ_hook:(fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard; ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with | None -> p,(true,[]) | Some tac -> Proof.run_tactic Global.(env ()) tac p)) -let start_proof_com ?inference_hook kind thms hook = +let start_proof_com ?inference_hook ?hook kind thms = let env0 = Global.env () in let decl = fst (List.hd thms) in let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in @@ -444,7 +449,7 @@ let start_proof_com ?inference_hook kind thms hook = else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_proof_with_initialization kind evd decl recguard thms snl hook + start_proof_with_initialization ?hook kind evd decl recguard thms snl (* Saving a proof *) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 246d8cbe6d..3ac12d3b0b 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -12,41 +12,45 @@ open Names open Decl_kinds type declaration_hook + val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook -val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> GlobRef.t -> unit +val call_hook : + ?hook:declaration_hook -> ?fix_exn:Future.fix_exn -> + Decl_kinds.locality -> GlobRef.t -> unit val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> - ?terminator:(Proof_global.lemma_possible_guards -> declaration_hook -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> EConstr.types -> + ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> ?compute_guard:Proof_global.lemma_possible_guards -> - declaration_hook -> unit + ?hook:declaration_hook -> EConstr.types -> unit val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> - ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> EConstr.types -> + ?terminator:(?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> ?compute_guard:Proof_global.lemma_possible_guards -> - (UState.t option -> declaration_hook) -> unit + ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit val start_proof_com : ?inference_hook:Pretyping.inference_hook -> - goal_kind -> Vernacexpr.proof_expr list -> - declaration_hook -> unit + ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list -> + unit val start_proof_with_initialization : + ?hook:declaration_hook -> goal_kind -> Evd.evar_map -> UState.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> (Id.t (* name of thm *) * - (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list - -> int list option -> declaration_hook -> unit + (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> + int list option -> unit val universe_proof_terminator : + ?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> - (UState.t option -> declaration_hook) -> - Proof_global.proof_terminator + Proof_global.proof_terminator val standard_proof_terminator : - Proof_global.lemma_possible_guards -> declaration_hook -> - Proof_global.proof_terminator + ?hook:declaration_hook -> Proof_global.lemma_possible_guards -> + Proof_global.proof_terminator val fresh_name_for_anonymous_theorem : unit -> Id.t diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 4926b8c3e1..f18227039f 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -22,11 +22,12 @@ open Util type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit let mk_univ_hook f = f -let call_univ_hook fix_exn hook uctx trans l c = - try hook uctx trans l c +let call_univ_hook ?univ_hook ?fix_exn uctx trans l c = + try Option.iter (fun hook -> hook uctx trans l c) univ_hook with e when CErrors.noncritical e -> let e = CErrors.push e in - iraise (fix_exn e) + let e = Option.cata (fun fix -> fix e) e fix_exn in + iraise e module NamedDecl = Context.Named.Declaration @@ -320,7 +321,7 @@ type program_info_aux = { prg_notations : notations ; prg_kind : definition_kind; prg_reduce : constr -> constr; - prg_hook : univ_declaration_hook; + prg_hook : univ_declaration_hook option; prg_opaque : bool; prg_sign: named_context_val; } @@ -481,9 +482,9 @@ let declare_definition prg = let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in let ubinders = UState.universe_binders uctx in + let hook = Lemmas.mk_hook (fun l r -> call_univ_hook ?univ_hook:prg.prg_hook ~fix_exn uctx obls l r; ()) in DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce ubinders prg.prg_implicits - (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx obls l r ; ())) + prg.prg_kind ce ubinders prg.prg_implicits ~hook let rec lam_index n t acc = match Constr.kind t with @@ -564,7 +565,7 @@ let declare_mutual_definition l = List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in - call_univ_hook fix_exn first.prg_hook first.prg_ctx obls local gr; + call_univ_hook ?univ_hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; List.iter progmap_remove l; gr let decompose_lam_prod c ty = @@ -662,8 +663,8 @@ let declare_obligation prg obl body ty uctx = in true, { obl with obl_body = body } -let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind - notations obls impls kind reduce hook = +let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkind + notations obls impls kind reduce = let obls', b = match b with | None -> @@ -688,7 +689,7 @@ let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; - prg_hook = hook; prg_opaque = opaque; + prg_hook = univ_hook; prg_opaque = opaque; prg_sign = sign } let map_cardinal m = @@ -843,9 +844,9 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_terminator name num guard hook auto pf = +let obligation_terminator ?univ_hook name num guard auto pf = let open Proof_global in - let term = Lemmas.universe_proof_terminator guard hook in + let term = Lemmas.universe_proof_terminator ?univ_hook guard in match pf with | Admitted _ -> apply_terminator term pf | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin @@ -968,11 +969,11 @@ let rec solve_obligation prg num tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in - let terminator guard hook = + let terminator ?univ_hook guard = Proof_global.make_terminator - (obligation_terminator prg.prg_name num guard hook auto) in - let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in - let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in + (obligation_terminator ?univ_hook prg.prg_name num guard auto) in + let univ_hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in + let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~univ_hook in let _ = Pfedit.by !default_tactic in Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac @@ -1109,10 +1110,10 @@ let show_term n = let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic - ?(reduce=reduce) ?(hook=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) obls = + ?(reduce=reduce) ?univ_hook ?(opaque = false) obls = let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print n ++ str " has type-checked" in - let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in + let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?univ_hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); @@ -1129,13 +1130,13 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) - ?(hook=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) notations fixkind = + ?univ_hook ?(opaque = false) notations fixkind = let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind) - notations obls imps kind reduce hook + notations obls imps kind reduce ?univ_hook in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 57040b3f7c..c670e3a3b5 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -14,8 +14,10 @@ open Evd open Names type univ_declaration_hook -val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook -val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit +val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) -> + univ_declaration_hook +val call_univ_hook : ?univ_hook:univ_declaration_hook -> ?fix_exn:Future.fix_exn -> + UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof @@ -56,14 +58,14 @@ type progress = (* Resolution status of a program *) val default_tactic : unit Proofview.tactic ref -val add_definition : Names.Id.t -> ?term:constr -> types -> +val add_definition : Names.Id.t -> ?term:constr -> types -> UState.t -> ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) -> - ?hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress + ?univ_hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list @@ -80,7 +82,7 @@ val add_mutual_definitions : ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(constr -> constr) -> - ?hook:univ_declaration_hook -> ?opaque:bool -> + ?univ_hook:univ_declaration_hook -> ?opaque:bool -> notations -> fixpoint_kind -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a157e01fc1..632df20592 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -475,7 +475,7 @@ let vernac_custom_entry ~module_local s = (***********) (* Gallina *) -let start_proof_and_print k l hook = +let start_proof_and_print ?hook k l = let inference_hook = if Flags.is_program_mode () then let hook env sigma ev = @@ -497,18 +497,16 @@ let start_proof_and_print k l hook = in Some hook else None in - start_proof_com ?inference_hook k l hook - -let no_hook = Lemmas.mk_hook (fun _ _ -> ()) + start_proof_com ?inference_hook ?hook k l let vernac_definition_hook p = function | Coercion -> - Class.add_coercion_hook p + Some (Class.add_coercion_hook p) | CanonicalStructure -> - Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure) + Some (Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)) | SubClass -> - Class.add_subclass_hook p -| _ -> no_hook + Some (Class.add_subclass_hook p) +| _ -> None let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = let atts = attributes_of_flags atts in @@ -531,7 +529,7 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = (match def with | ProveBody (bl,t) -> (* local binders, typ *) start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) - [(CAst.make ?loc name, pl), (bl, t)] hook + ?hook [(CAst.make ?loc name, pl), (bl, t)] | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None @@ -539,14 +537,14 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = let sigma, env = Pfedit.get_current_context () in Some (snd (Hook.get f_interp_redexp env sigma r)) in ComDefinition.do_definition ~program_mode name - (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) + (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook) let vernac_start_proof ~atts kind l = let atts = attributes_of_flags atts in let local = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print (local, atts.polymorphic, Proof kind) l no_hook + start_proof_and_print (local, atts.polymorphic, Proof kind) l let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted @@ -1035,13 +1033,9 @@ let vernac_set_used_variables e = user_err ~hdr:"vernac_set_used_variables" (str "Unknown variable: " ++ Id.print id)) l; - let _, to_clear = Proof_global.set_used_variables l in - let to_clear = List.map (fun x -> x.CAst.v) to_clear in + ignore (Proof_global.set_used_variables l); Proof_global.with_current_proof begin fun _ p -> - if List.is_empty to_clear then (p, ()) - else - let tac = Tactics.clear to_clear in - fst (Pfedit.solve Goal_select.SelectAll None tac p), () + (p, ()) end (*****************************) |