diff options
59 files changed, 1165 insertions, 631 deletions
diff --git a/azure-pipelines.yml b/azure-pipelines.yml index f2cec1eb19..c93920a884 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -43,7 +43,7 @@ jobs: vmImage: 'macOS-10.13' variables: - MACOSX_DEPLOYMENT_TARGET: '10.12' + MACOSX_DEPLOYMENT_TARGET: '10.11' steps: - checkout: self diff --git a/default.nix b/default.nix index 1e2cb3625d..d5c6cdb8ad 100644 --- a/default.nix +++ b/default.nix @@ -74,7 +74,7 @@ stdenv.mkDerivation rec { else with builtins; filterSource (path: _: - !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.; + !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci" "nix"]) ./.; preConfigure = '' patchShebangs dev/tools/ diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix index 1d931c858e..d813ddd8d7 100644 --- a/dev/ci/nix/bignums.nix +++ b/dev/ci/nix/bignums.nix @@ -1,5 +1,5 @@ { ocamlPackages }: { - buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ]; + buildInputs = [ ocamlPackages.ocaml ]; } diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch index 6d96d94dfc..6d2f6470b1 100644 --- a/dev/ci/nix/unicoq/unicoq-num.patch +++ b/dev/ci/nix/unicoq/unicoq-num.patch @@ -4,19 +4,6 @@ Date: Thu Nov 29 08:59:22 2018 +0000 Make explicit dependency to num -diff --git a/Make b/Make -index 550dc6a..8aa1309 100644 ---- a/Make -+++ b/Make -@@ -9,7 +9,7 @@ src/logger.ml - src/munify.mli - src/munify.ml - src/unitactics.mlg --src/unicoq.mllib -+src/unicoq.mlpack - theories/Unicoq.v - test-suite/munifytest.v - test-suite/microtests.v diff --git a/Makefile.local b/Makefile.local new file mode 100644 index 0000000..88be365 @@ -24,21 +11,3 @@ index 0000000..88be365 +++ b/Makefile.local @@ -0,0 +1 @@ +CAMLPKGS += -package num -diff --git a/src/unicoq.mllib b/src/unicoq.mllib -deleted file mode 100644 -index 2b84e2d..0000000 ---- a/src/unicoq.mllib -+++ /dev/null -@@ -1,3 +0,0 @@ --Logger --Munify --Unitactics -diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack -new file mode 100644 -index 0000000..2b84e2d ---- /dev/null -+++ b/src/unicoq.mlpack -@@ -0,0 +1,3 @@ -+Logger -+Munify -+Unitactics diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index f4786d9431..8dfe1e7833 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/8471ab76242987b11afd4486b82888e1588f8307.tar.gz"; - sha256 = "06pp6b6x78jlinxifnphkbp79dx58jr990fkm4qziq0ay5klpxd7"; + url = "https://github.com/NixOS/nixpkgs/archive/bc9df0f66110039e495b6debe3a6cda4a1bb0fed.tar.gz"; + sha256 = "0y2w259j0vqiwjhjvlbsaqnp1nl2zwz6sbwwhkrqn7k7fmhmxnq1"; }) diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst new file mode 100644 index 0000000000..78874cadb1 --- /dev/null +++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst @@ -0,0 +1,6 @@ +- Deprecated flag `Refine Instance Mode` has been removed. + (`#09530 <https://github.com/coq/coq/pull/09530>`_, fixes + `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 + <https://github.com/coq/coq/issues/3890>`_ and `#4638 + <https://github.com/coq/coq/issues/4638>`_ + by Maxime Dénès, review by Gaëtan Gilbert). diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 881f7a310d..b20669c7f1 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat ``{*, …}``, ``{+, …}`` an optional or mandatory repeatable block, with repetitions separated by commas -``%|``, ``%{``, … - an escaped character (rendered without the leading ``%``) +``{| … | … | … }`` + an alternative, indicating than one of multiple constructs can be used + +``%{``, ``%}``, ``%|`` + an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.) .. FIXME document the new subscript support @@ -148,7 +151,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica Example:: .. prodn:: term += let: @pattern := @term in @term - .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } ``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values. Example:: diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 78803a927f..2093765608 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat ``{*, …}``, ``{+, …}`` an optional or mandatory repeatable block, with repetitions separated by commas -``%|``, ``%{``, … - an escaped character (rendered without the leading ``%``) +``{| … | … | … }`` + an alternative, indicating than one of multiple constructs can be used + +``%{``, ``%}``, ``%|`` + an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.) .. FIXME document the new subscript support diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty index 75eac1f724..3548b8754c 100644 --- a/doc/sphinx/_static/coqnotations.sty +++ b/doc/sphinx/_static/coqnotations.sty @@ -18,6 +18,9 @@ \newlength{\nscriptsize} \setlength{\nscriptsize}{0.8em} +\newlength{\nboxsep} +\setlength{\nboxsep}{2pt} + \newcommand*{\scriptsmallsquarebox}[1]{% % Force width \makebox[\nscriptsize]{% @@ -31,7 +34,8 @@ \newcommand*{\nsup}[1]{^{\nscript{0.15}{#1}}} \newcommand*{\nsub}[1]{_{\nscript{0.35}{#1}}} \newcommand*{\nnotation}[1]{#1} -\newcommand*{\nrepeat}[1]{\text{\adjustbox{cfbox=nbordercolor 0.5pt 2pt,bgcolor=nbgcolor}{#1\hspace{.5\nscriptsize}}}} +\newcommand*{\nbox}[1]{\adjustbox{cfbox=nbordercolor 0.5pt \nboxsep,bgcolor=nbgcolor}{#1}} +\newcommand*{\nrepeat}[1]{\text{\nbox{#1\hspace{.5\nscriptsize}}}} \newcommand*{\nwrapper}[1]{\ensuremath{\displaystyle#1}} % https://tex.stackexchange.com/questions/310877/ \newcommand*{\nhole}[1]{\textit{\color{nholecolor}#1}} @@ -42,9 +46,32 @@ } % </magic> +% https://tex.stackexchange.com/questions/490262/ +\def\naltsep{} +\newsavebox{\nsavedalt} +\newlength{\naltvruleht} +\newlength{\naltvruledp} +\def\naltvrule{\smash{\vrule height\naltvruleht depth\naltvruledp}} +\newcommand{\nalternative}[2]{% + % First measure the contents of the box without the bar + \bgroup% + \def\naltsep{}% + \savebox{\nsavedalt}{#1}% + \setlength{\naltvruleht}{\ht\nsavedalt}% + \setlength{\naltvruledp}{\dp\nsavedalt}% + \addtolength{\naltvruleht}{#2}% + \addtolength{\naltvruledp}{#2}% + % Then redraw it with the bar + \def\naltsep{\naltvrule}% + #1\egroup} + \newcssclass{notation-sup}{\nsup{#1}} \newcssclass{notation-sub}{\nsub{#1}} \newcssclass{notation}{\nnotation{#1}} \newcssclass{repeat}{\nrepeat{#1}} \newcssclass{repeat-wrapper}{\nwrapper{#1}} \newcssclass{hole}{\nhole{#1}} +\newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}} +\newcssclass{alternative-block}{#1} +\newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}} +\newcssclass{alternative-separator}{\quad\naltsep{}\quad} diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index dcb47d1786..8322ab0137 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -45,15 +45,46 @@ width: 2.2em; } -.notation .repeat { +.notation .repeat, .notation .alternative { background: #EAEAEA; border: 1px solid #AAA; display: inline-block; - padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */ - padding-left: 0.2em; + padding: 0 0.2em 0 0.3em; margin: 0.25em 0; } +.notation .repeated-alternative { + display: inline-table; +} + +.notation .alternative { + display: inline-table; + padding: 0 0.2em; +} + +.notation .alternative-block { + display: table-cell; + padding: 0 0.5em; +} + +.notation .alternative-separator { + border-left: 1px solid black; /* Display a thin bar */ + display: table-cell; + width: 0; +} + +.alternative-block:first-child { + padding-left: 0; +} + +.alternative-block:last-child { + padding-right: 0; +} + +.notation .repeat { + padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */ +} + .notation .repeat-wrapper { display: inline-block; position: relative; diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index e93b01f14d..8a895eb515 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -99,7 +99,7 @@ Extraction Options Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Extraction Language ( OCaml | Haskell | Scheme ) +.. cmd:: Extraction Language {| OCaml | Haskell | Scheme } :name: Extraction Language The ability to fix target language is the first and more important diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index b474c51f17..847abb33fc 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -170,12 +170,12 @@ compatibility constraints. Adding new relations and morphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident +.. cmd:: Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`, :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`. - The :token:`ident` gives a unique name to the morphism and it is used + The final :token:`ident` gives a unique name to the morphism and it is used by the command to generate fresh names for automatically provided lemmas used internally. @@ -219,15 +219,16 @@ replace terms with related ones only in contexts that are syntactic compositions of parametric morphism instances declared with the following command. -.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident +.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident - This command declares ``f`` as a parametric morphism of signature ``sig``. The - identifier :token:`ident` gives a unique name to the morphism and it is used as - the base name of the typeclass instance definition and as the name of - the lemma that proves the well-definedness of the morphism. The - parameters of the morphism as well as the signature may refer to the - context of variables. The command asks the user to prove interactively - that ``f`` respects the relations identified from the signature. + This command declares a parametric morphism :n:`@ident {+ @term__1}` of + signature :n:`@term__2`. The final identifier :token:`ident` gives a unique + name to the morphism and it is used as the base name of the typeclass + instance definition and as the name of the lemma that proves the + well-definedness of the morphism. The parameters of the morphism as well as + the signature may refer to the context of variables. The command asks the + user to prove interactively that the function denoted by the first + :token:`ident` respects the relations identified from the signature. .. example:: @@ -577,7 +578,7 @@ Deprecated syntax and backward incompatibilities Notice that the syntax is not completely backward compatible since the identifier was not required. -.. cmd:: Add Morphism f : @ident +.. cmd:: Add Morphism @ident : @ident :name: Add Morphism This command is restricted to the declaration of morphisms @@ -809,7 +810,7 @@ Usage ~~~~~ -.. tacn:: rewrite_strat @s [in @ident] +.. tacn:: rewrite_strat @s {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b410833d25..22ddcae584 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. -.. cmd:: {? Local|Global} Obligation Tactic := @tactic +.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 77a6ee79cc..65934efaa6 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -311,24 +311,24 @@ Summary of the commands This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } +.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} } This command is used to declare a typeclass instance named - :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and - fields ``b1`` to ``bi``, where each field must be a declared field of - the class. Missing fields must be filled in interactive proof mode. + :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and + fields defined by :token:`field_def`, where each field must be a declared field of + the class. An arbitrary context of :token:`binders` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for - :tacn:`auto` hints. If the priority is not specified, it defaults to the number + :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number of non-dependent binders of the instance. - .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term + .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term This syntax is used for declaration of singleton class instances or - for directly giving an explicit term of type :n:`forall @binders, @class - @term__1 … @term__n`. One need not even mention the unique field name for + for directly giving an explicit term of type :n:`forall @binders, @term__0 + {+ @term}`. One need not even mention the unique field name for singleton classes. .. cmdv:: Global Instance @@ -356,11 +356,11 @@ Summary of the commands Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a few other commands related to typeclasses. -.. cmd:: Existing Instance {+ @ident} [| priority] +.. cmd:: Existing Instance {+ @ident} {? | @num} This command adds an arbitrary list of constants whose type ends with an applied typeclass to the instance database with an optional - priority. It can be used for redeclaring instances at the end of + priority :token:`num`. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. @@ -408,7 +408,7 @@ few other commands related to typeclasses. + When considering local hypotheses, we use the union of all the modes declared in the given databases. - .. cmdv:: typeclasses eauto @num + .. tacv:: typeclasses eauto @num .. warning:: The semantics for the limit :n:`@num` @@ -417,7 +417,7 @@ few other commands related to typeclasses. counted, which might result in larger limits being necessary when searching with ``typeclasses eauto`` than with :tacn:`auto`. - .. cmdv:: typeclasses eauto with {+ @ident} + .. tacv:: typeclasses eauto with {+ @ident} This variant runs resolution with the given hint databases. It treats typeclass subgoals the same as other subgoals (no shelving of @@ -563,23 +563,10 @@ Settings 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 - - .. deprecated:: 8.10 - - This flag allows to switch the behavior of instance declarations made through - the Instance command. - - + When it is off (the default), they fail with an error instead. - - + When it is on, instances that have unsolved holes in - their proof-term silently open the proof mode with the remaining - obligations to prove. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num +.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num :name: Typeclasses eauto This command allows more global customization of the typeclass diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index cca3b2e06b..cc2c43e7dd 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -486,10 +486,9 @@ Other changes in 8.10+beta1 - :cmd:`Declare Instance` now requires an instance name. - The flag :flag:`Refine Instance Mode` has been turned off by default, - meaning that :cmd:`Instance` no longer opens a proof when a body is - provided. The flag has been deprecated and will be removed in the next - version. + The flag `Refine Instance Mode` has been turned off by default, meaning that + :cmd:`Instance` no longer opens a proof when a body is provided. The flag + has been deprecated and will be removed in the next version. (`#9270 <https://github.com/coq/coq/pull/9270>`_, and `#9825 <https://github.com/coq/coq/pull/9825>`_, @@ -498,7 +497,7 @@ Other changes in 8.10+beta1 - Command :cmd:`Instance`, when no body is provided, now always opens a proof. This is a breaking change, as instance of :n:`Instance @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will - have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.` + have to be changed into :n:`Instance @ident__1 : @ident__2 := %{%}.` or :n:`Instance @ident__1 : @ident__2. Proof. Qed.` (`#9274 <https://github.com/coq/coq/pull/9274>`_, by Maxime Dénès). @@ -3940,7 +3939,7 @@ Vernacular commands Equality Schemes", this replaces deprecated option "Equality Scheme"). - Made support for automatic generation of case analysis schemes available to user (governed by option "Set Case Analysis Schemes"). -- New command :n:`{? Global } Generalizable [All|No] [Variable|Variables] {* @ident}` to +- New command :n:`{? Global } Generalizable {| All | No } {| Variable | Variables } {* @ident}` to declare which identifiers are generalizable in `` `{} `` and `` `() `` binders. - New command "Print Opaque Dependencies" to display opaque constants in addition to all variables, parameters or axioms a theorem or diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ba766c8c3d..5e214f6f7f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor .. productionlist:: record_term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `record_term` + field_def : `ident` [`binders`] := `term` Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have @@ -831,16 +831,16 @@ Sections create local contexts which can be shared across multiple definitions. Links :token:`type` to each :token:`ident`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } Declare one or more variables with various types. - .. cmdv:: Variables {+ ( {+ @ident } : @type) } - Hypothesis {+ ( {+ @ident } : @type) } - Hypotheses {+ ( {+ @ident } : @type) } + .. cmdv:: Variables {+ ( {+ @ident } : @type) } + Hypothesis {+ ( {+ @ident } : @type) } + Hypotheses {+ ( {+ @ident } : @type) } :name: Variables; Hypothesis; Hypotheses - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. .. cmd:: Let @ident := @term @@ -931,7 +931,7 @@ In the syntax of module application, the ! prefix indicates that any :token:`module_binding`. The output module type is verified against each :token:`module_type`. -.. cmdv:: Module [ Import | Export ] +.. cmdv:: Module {| Import | Export } Behaves like :cmd:`Module`, but automatically imports or exports the module. @@ -1648,7 +1648,7 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, @@ -1665,20 +1665,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } } +.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -2167,7 +2167,7 @@ that specify which variables should be generalizable. Disable implicit generalization entirely. This is the default behavior. -.. cmd:: Generalizable (Variable | Variables) {+ @ident } +.. cmd:: Generalizable {| Variable | Variables } {+ @ident } Allow generalization of the given identifiers only. Calling this command multiple times adds to the allowed identifiers. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 5a1af9f9fa..8acbcbec8f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -616,34 +616,34 @@ has type :token:`type`. Adds several parameters with specification :token:`type`. - .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } Adds blocks of parameters with different specifications. - .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } :name: Local Parameter Such parameters are never made accessible through their unqualified name by :cmd:`Import` and its variants. You have to explicitly give their fully qualified name to refer to them. - .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } - {? Local } Axiom {+ ( {+ @ident } : @type ) } - {? Local } Axioms {+ ( {+ @ident } : @type ) } - {? Local } Conjecture {+ ( {+ @ident } : @type ) } - {? Local } Conjectures {+ ( {+ @ident } : @type ) } + .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } + {? Local } Axiom {+ ( {+ @ident } : @type ) } + {? Local } Axioms {+ ( {+ @ident } : @type ) } + {? Local } Conjecture {+ ( {+ @ident } : @type ) } + {? Local } Conjectures {+ ( {+ @ident } : @type ) } :name: Parameters; Axiom; Axioms; Conjecture; Conjectures - These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. + These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - Variables {+ ( {+ @ident } : @type ) } - Hypothesis {+ ( {+ @ident } : @type ) } - Hypotheses {+ ( {+ @ident } : @type ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + Variables {+ ( {+ @ident } : @type ) } + Hypothesis {+ ( {+ @ident } : @type ) } + Hypotheses {+ ( {+ @ident } : @type ) } :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) Outside of any section, these variants are synonyms of - :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. + :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. For their meaning inside a section, see :cmd:`Variable` in :ref:`section-mechanism`. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index a7eb7c2319..bbd7e0ba3d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -360,7 +360,7 @@ Detecting progress We can check if a tactic made progress with: -.. tacn:: progress expr +.. tacn:: progress @expr :name: progress :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v`` @@ -555,7 +555,7 @@ Identity The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but it appears in the proof script. -.. tacn:: idtac {* message_token} +.. tacn:: idtac {* @message_token} :name: idtac This prints the given tokens. Strings and integers are printed @@ -684,7 +684,7 @@ Timing a tactic that evaluates to a term Tactic expressions that produce terms can be timed with the experimental tactic -.. tacn:: time_constr expr +.. tacn:: time_constr @expr :name: time_constr which evaluates :n:`@expr ()` and displays the time the tactic expression @@ -880,7 +880,7 @@ We can perform pattern matching on goals using the following expression: .. we should provide the full grammar here -.. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end +.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is @@ -918,7 +918,7 @@ We can perform pattern matching on goals using the following expression: first), but it possible to reverse this order (oldest first) with the :n:`match reverse goal with` variant. - .. tacv:: multimatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points @@ -929,7 +929,7 @@ We can perform pattern matching on goals using the following expression: The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for :n:`once multimatch [reverse] goal …`. - .. tacv:: lazymatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end Using lazymatch instead of match will perform the same pattern matching procedure but will commit to the first matching branch with the first @@ -1135,33 +1135,33 @@ Defining |Ltac| functions Basically, |Ltac| toplevel definitions are made as follows: -.. cmd:: Ltac @ident {* @ident} := @expr +.. cmd:: {? Local} Ltac @ident {* @ident} := @expr + :name: Ltac This defines a new |Ltac| function that can be used in any tactic script or new |Ltac| toplevel definition. + If preceded by the keyword ``Local``, the tactic definition will not be + exported outside the current module. + .. note:: The preceding definition can equivalently be written: :n:`Ltac @ident := fun {+ @ident} => @expr` - Recursive and mutual recursive function definitions are also possible - with the syntax: - .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @expr - It is also possible to *redefine* an existing user-defined tactic using the syntax: + This syntax allows recursive and mutual recursive function definitions. .. cmdv:: Ltac @qualid {* @ident} ::= @expr + This syntax *redefines* an existing user-defined tactic. + A previous definition of qualid must exist in the environment. The new definition will always be used instead of the old one and it goes across module boundaries. - If preceded by the keyword Local the tactic definition will not be - exported outside the current module. - Printing |Ltac| tactics ~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 6e33862b39..aa603fc966 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -668,7 +668,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= @string %| @integer %| @lident ({+, @ltac2_scope}) + ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } A few scopes contain antiquotation features. For sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. @@ -751,7 +751,7 @@ Notations The Ltac2 parser can be extended by syntactic notations. -.. cmd:: Ltac2 Notation {+ @lident (@ltac2_scope) %| @string } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded @@ -823,9 +823,9 @@ Ltac2 features a toplevel loop that can be used to evaluate expressions. Debug ----- -.. opt:: Ltac2 Backtrace +.. flag:: Ltac2 Backtrace - When this option is set, toplevel failures will be printed with a backtrace. + When this flag is set, toplevel failures will be printed with a backtrace. Compatibility layer with Ltac1 ------------------------------ @@ -966,7 +966,7 @@ errors produced by the typechecker. In Ltac expressions +++++++++++++++++++ -.. exn:: Unbound ( value | constructor ) X +.. exn:: Unbound {| value | constructor } X * if `X` is meant to be a term from the current stactic environment, replace the problematic use by `'X`. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 16b158c397..4a2f9c0db3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -322,7 +322,7 @@ Navigation in the proof tree .. index:: { } -.. cmd:: %{ %| %} +.. cmd:: {| %{ | %} } The command ``{`` (without a terminating period) focuses on the first goal, much like :cmd:`Focus` does, however, the subproof can only be @@ -430,7 +430,7 @@ not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further nesting levels provided they are delimited by these. Bullets are made of repeated ``-``, ``+`` or ``*`` symbols: -.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * } +.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } } Note again that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or ``}`` to unfocus it @@ -492,7 +492,7 @@ The following example script illustrates all these features: Set Bullet Behavior ``````````````````` -.. opt:: Bullet Behavior %( "None" %| "Strict Subproofs" %) +.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } :name: Bullet Behavior This option controls the bullet behavior and can take two possible values: @@ -544,9 +544,9 @@ Requesting information ``<Your Tactic Text here>``. - .. deprecated:: 8.10 + .. deprecated:: 8.10 - Please use a text editor. + Please use a text editor. .. cmdv:: Show Proof :name: Show Proof @@ -680,7 +680,7 @@ This image shows an error message with diff highlighting in CoqIDE: How to enable diffs ``````````````````` -.. opt:: Diffs %( "on" %| "off" %| "removed" %) +.. opt:: Diffs {| "on" | "off" | "removed" } :name: Diffs The “on” setting highlights added tokens in green, while the “removed” setting diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 4e40df6f94..75e019592f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -617,7 +617,7 @@ Abbreviations selected occurrences of a term. .. prodn:: - occ_switch ::= { {? + %| - } {* @num } } + occ_switch ::= { {? {| + | - } } {* @num } } where: @@ -2273,7 +2273,7 @@ to the others. Iteration ~~~~~~~~~ -.. tacn:: do {? @num } ( @tactic | [ {+| @tactic } ] ) +.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] } :name: do (ssreflect) This tactical offers an accurate control on the repetition of tactics. @@ -2300,7 +2300,7 @@ tactic should be repeated on the current subgoal. There are four kinds of multipliers: .. prodn:: - mult ::= @num ! %| ! %| @num ? %| ? + mult ::= {| @num ! | ! | @num ? | ? } Their meaning is: @@ -2571,7 +2571,7 @@ destruction of existential assumptions like in the tactic: An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: -.. tacv:: have {? @ident } := term +.. tacv:: have {? @ident } := @term This tactic creates a new assumption of type the type of :token:`term`. If the @@ -5444,7 +5444,7 @@ equivalences are indeed taken into account, otherwise only single |SSR| searching tool -------------------- -.. cmd:: Search {? @pattern } {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } } +.. cmd:: Search {? @pattern } {* {? - } {| @string | @pattern } {? % @ident} } {? in {+ {? - } @qualid } } :name: Search (ssreflect) This is the |SSR| extension of the Search command. :token:`qualid` is the @@ -5686,7 +5686,7 @@ respectively. local cofix definition -.. tacn:: set @ident {? : @term } := {? @occ_switch } %( @term %| ( @c_pattern) %) +.. tacn:: set @ident {? : @term } := {? @occ_switch } {| @term | ( @c_pattern) } abbreviation (see :ref:`abbreviations_ssr`) @@ -5714,26 +5714,26 @@ introduction see :ref:`introduction_ssr` localization see :ref:`localization_ssr` -.. prodn:: tactic += do {? @mult } %( @tactic %| [ {+| @tactic } ] %) +.. prodn:: tactic += do {? @mult } {| @tactic | [ {+| @tactic } ] } iteration see :ref:`iteration_ssr` -.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } %( @tactic %| [ {+| @tactic } ] %) +.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] } selector see :ref:`selectors_ssr` -.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } +.. prodn:: tactic += @tactic ; {| first | last } {? @num } rotation see :ref:`selectors_ssr` -.. prodn:: tactic += by %( @tactic %| [ {*| @tactic } ] %) +.. prodn:: tactic += by {| @tactic | [ {*| @tactic } ] } closing see :ref:`terminators_ssr` Commands ~~~~~~~~ -.. cmd:: Hint View for %( move %| apply %) / @ident {? | @num } +.. cmd:: Hint View for {| move | apply } / @ident {? | @num } view hint declaration (see :ref:`declaring_new_hints_ssr`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index c728b925ac..4e47621938 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1749,7 +1749,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, and ``in`` clauses. -.. tacn:: case term +.. tacn:: case @term :name: case The tactic :n:`case` is a more basic tactic to perform case analysis without @@ -1982,7 +1982,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`induction @ident; induction @ident` (or :n:`induction @ident ; destruct @ident` depending on the exact needs). -.. tacv:: double induction num1 num2 +.. tacv:: double induction @num__1 @num__2 This tactic is deprecated and should be replaced by :n:`induction num1; induction num3` where :n:`num3` is the result @@ -2271,11 +2271,11 @@ and an explanation of the underlying technique. :undocumented: .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} - injection @num as {+ simple_intropattern} - injection as {+ simple_intropattern} - einjection @term {? with @bindings_list} as {+ simple_intropattern} - einjection @num as {+ simple_intropattern} - einjection as {+ simple_intropattern} + injection @num as {+ @simple_intropattern} + injection as {+ @simple_intropattern} + einjection @term {? with @bindings_list} as {+ @simple_intropattern} + einjection @num as {+ @simple_intropattern} + einjection as {+ @simple_intropattern} These variants apply :n:`intros {+ @simple_intropattern}` after the call to :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in @@ -2637,7 +2637,7 @@ and an explanation of the underlying technique. is correct at some time of the interactive development of a proof, use the command ``Guarded`` (see Section :ref:`requestinginformation`). -.. tacv:: fix @ident @num with {+ (ident {+ @binder} [{struct @ident}] : @type)} +.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)} This starts a proof by mutual induction. The statements to be simultaneously proved are respectively :g:`forall binder ... binder, type`. @@ -3777,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident - Hint Constants %( Transparent %| Opaque %) : @ident + .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident + Hint Constants {| Transparent | Opaque } : @ident :name: Hint Variables; Hint Constants This sets the transparency flag used during unification of @@ -3850,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is semantics of :n:`Hint Cut @regexp` is to set the cut expression to :n:`c | regexp`, the initial cut expression being `emp`. - .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident + .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident :name: Hint Mode This sets an optional mode of use of the identifier :n:`@qualid`. When @@ -4016,7 +4016,7 @@ We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior option which accepts three flags allowing for a fine-grained handling of non-imported hints. -.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) +.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" } :name: Loose Hint Behavior This option accepts three values, which control the behavior of hints w.r.t. @@ -4048,7 +4048,7 @@ Setting implicit automation tactics .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. - .. cmdv:: Proof with tactic using {+ @ident} + .. cmdv:: Proof with @tactic using {+ @ident} Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` @@ -4400,6 +4400,11 @@ Equality This tactic applies to a goal that has the form :g:`t=u` and transforms it into the two subgoals :n:`t=@term` and :n:`@term=u`. + .. tacv:: etransitivity + + This tactic behaves like :tacn:`transitivity`, using a fresh evar instead of + a concrete :token:`term`. + Equality and inductive sets --------------------------- diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e207a072cc..26dc4e02cf 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,13 +91,13 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: {? Local | Global | Export } Set @flag +.. cmd:: {? {| Local | Global | Export } } Set @flag :name: Set Sets :token:`flag` on. Scoping qualifiers are described :ref:`here <set_unset_scope_qualifiers>`. -.. cmd:: {? Local | Global | Export } Unset @flag +.. cmd:: {? {| Local | Global | Export } } Unset @flag :name: Unset Sets :token:`flag` off. Scoping qualifiers are @@ -108,13 +108,13 @@ capital letter. Prints the current value of :token:`flag`. -.. cmd:: {? Local | Global | Export } Set @option ( @num | @string ) +.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string } :name: Set @option Sets :token:`option` to the specified value. Scoping qualifiers are described :ref:`here <set_unset_scope_qualifiers>`. -.. cmd:: {? Local | Global | Export } Unset @option +.. cmd:: {? {| Local | Global | Export } } Unset @option :name: Unset @option Sets :token:`option` to its default value. Scoping qualifiers are @@ -129,17 +129,17 @@ capital letter. Prints the current value of all flags and options, and the names of all tables. -.. cmd:: Add @table ( @string | @qualid ) +.. cmd:: Add @table {| @string | @qualid } :name: Add @table Adds the specified value to :token:`table`. -.. cmd:: Remove @table ( @string | @qualid ) +.. cmd:: Remove @table {| @string | @qualid } :name: Remove @table Removes the specified value from :token:`table`. -.. cmd:: Test @table for ( @string | @qualid ) +.. cmd:: Test @table for {| @string | @qualid } :name: Test @table for Reports whether :token:`table` contains the specified value. @@ -162,7 +162,7 @@ capital letter. Scope qualifiers for :cmd:`Set` and :cmd:`Unset` ````````````````````````````````````````````````` -:n:`{? Local | Global | Export }` +:n:`{? {| Local | Global | Export } }` Flag and option settings can be global in scope or local to nested scopes created by :cmd:`Module` and :cmd:`Section` commands. There are four alternatives: @@ -277,7 +277,7 @@ Requests to the environment :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 } + .. cmdv:: Search {+ {? -}@term_pattern_string} where :n:`@term_pattern_string` is a term_pattern, a string, or a string followed @@ -289,17 +289,17 @@ Requests to the environment prefixed by `-`, the search excludes the objects that mention that term_pattern or that string. - .. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid } + .. cmdv:: Search {+ {? -}@term_pattern_string} inside {+ @qualid } This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid } + .. cmdv:: Search {+ {? -}@term_pattern_string} outside {+ @qualid } This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string + .. cmdv:: @selector: Search {+ {? -}@term_pattern_string} This specifies the goal on which to search hypothesis (see Section :ref:`invocation-of-tactics`). @@ -353,7 +353,7 @@ Requests to the environment This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: SearchHead term outside {+ @qualid } + .. cmdv:: SearchHead @term outside {+ @qualid } This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. @@ -443,7 +443,7 @@ Requests to the environment SearchRewrite (_ + _ + _). - .. cmdv:: SearchRewrite term inside {+ @qualid } + .. cmdv:: SearchRewrite @term inside {+ @qualid } This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. @@ -622,7 +622,7 @@ file is a particular case of module called *library file*. but if a further module, say `A`, contains a command :cmd:`Require Export` `B`, then the command :cmd:`Require Import` `A` also imports the module `B.` - .. cmdv:: Require [Import | Export] {+ @qualid } + .. cmdv:: Require {| Import | Export } {+ @qualid } This loads the modules named by the :token:`qualid` sequence and their recursive @@ -988,7 +988,7 @@ Controlling display This option controls the normal displaying. -.. opt:: Warnings "{+, {? %( - %| + %) } @ident }" +.. opt:: Warnings "{+, {? {| - | + } } @ident }" :name: Warnings This option configures the display of warnings. It is experimental, and diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 418922e9b3..3a12ee288a 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -336,29 +336,32 @@ Generation of induction principles with ``Functional`` ``Scheme`` Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- -.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort +.. cmd:: Derive Inversion @ident with @ident Sort @sort + Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort This command generates an inversion principle for the - :tacn:`inversion ... using ...` tactic. Let :g:`I` be an inductive - predicate and :g:`x` the variables occurring in t. This command - generates and stocks the inversion lemma for the sort :g:`sort` - corresponding to the instance :g:`∀ (x:T), I t` with the name - :n:`@ident` in the global environment. When applied, it is - equivalent to having inverted the instance with the tactic - :g:`inversion`. - + :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name + of the generated principle. The second :token:`ident` should be an inductive + predicate, and :token:`binders` the variables occurring in the term + :token:`term`. This command generates the inversion lemma for the sort + :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`. + When applied, it is equivalent to having inverted the instance with the + tactic :g:`inversion`. -.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort @sort +.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort + Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic `inversion_clear`. -.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort +.. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort + Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`. -.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort +.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort + Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion_clear`. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index edec13f681..cda228a7da 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -327,22 +327,29 @@ symbols. Reserving notations ~~~~~~~~~~~~~~~~~~~ -A given notation may be used in different contexts. Coq expects all -uses of the notation to be defined at the same precedence and with the -same associativity. To avoid giving the precedence and associativity -every time, it is possible to declare a parsing rule in advance -without giving its interpretation. Here is an example from the initial -state of Coq. +.. cmd:: Reserved Notation @string {? (@modifiers) } -.. coqtop:: in + A given notation may be used in different contexts. Coq expects all + uses of the notation to be defined at the same precedence and with the + same associativity. To avoid giving the precedence and associativity + every time, this command declares a parsing rule (:token:`string`) in advance + without giving its interpretation. Here is an example from the initial + state of Coq. + + .. coqtop:: in + + Reserved Notation "x = y" (at level 70, no associativity). + + Reserving a notation is also useful for simultaneously defining an + inductive type or a recursive constant and a notation for it. - Reserved Notation "x = y" (at level 70, no associativity). + .. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence + their precedence and associativity cannot be changed. -Reserving a notation is also useful for simultaneously defining an -inductive type or a recursive constant and a notation for it. + .. cmdv:: Reserved Infix "@symbol" {* @modifiers} -.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence - their precedence and associativity cannot be changed. + This command declares an infix parsing rule without giving its + interpretation. Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 0ade9fdbf5..4bdfac7c42 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -39,14 +39,29 @@ from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors from .repl.coqtop import CoqTop, CoqTopError +from .notations.parsing import ParseError from .notations.sphinx import sphinxify from .notations.plain import stringify_with_ellipses -def parse_notation(notation, source, line, rawtext=None): +PARSE_ERROR = """Parse error in notation! +Offending notation: {} +Error message: {}""" + +def notation_to_sphinx(notation, source, line, rawtext=None): """Parse notation and wrap it in an inline node""" - node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation']) - node.source, node.line = source, line - return node + try: + node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation']) + node.source, node.line = source, line + return node + except ParseError as e: + raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e + +def notation_to_string(notation): + """Parse notation and format it as a string with ellipses.""" + try: + return stringify_with_ellipses(notation) + except ParseError as e: + raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e def highlight_using_coqdoc(sentence): """Lex sentence using coqdoc, and yield inline nodes for each token""" @@ -136,7 +151,7 @@ class CoqObject(ObjectDescription): self._render_signature(signature, signode) name = self._names.get(signature) if name is None: - name = self._name_from_signature(signature) + name = self._name_from_signature(signature) # pylint: disable=assignment-from-none # remove trailing ‘.’ found in commands, but not ‘...’ (ellipsis) if name is not None and name.endswith(".") and not name.endswith("..."): name = name[:-1] @@ -241,7 +256,7 @@ class NotationObject(DocumentableObject): """ def _render_signature(self, signature, signode): position = self.state_machine.get_source_and_line(self.lineno) - tacn_node = parse_notation(signature, *position) + tacn_node = notation_to_sphinx(signature, *position) signode += addnodes.desc_name(signature, '', tacn_node) class GallinaObject(PlainObject): @@ -346,7 +361,7 @@ class OptionObject(NotationObject): annotation = "Option" def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) class FlagObject(NotationObject): @@ -365,7 +380,7 @@ class FlagObject(NotationObject): annotation = "Flag" def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) class TableObject(NotationObject): @@ -383,7 +398,7 @@ class TableObject(NotationObject): annotation = "Table" def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) class ProductionObject(CoqObject): r"""A grammar production. @@ -403,7 +418,7 @@ class ProductionObject(CoqObject): Example:: .. prodn:: term += let: @pattern := @term in @term - .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } """ subdomain = "prodn" @@ -432,7 +447,7 @@ class ProductionObject(CoqObject): lhs_node = nodes.literal(lhs_op, lhs_op) position = self.state_machine.get_source_and_line(self.lineno) - rhs_node = parse_notation(rhs, *position) + rhs_node = notation_to_sphinx(rhs, *position) signode += addnodes.desc_name(signature, '', lhs_node, rhs_node) return ('token', lhs) if op == '::=' else None @@ -475,7 +490,7 @@ class ExceptionObject(NotationObject): # Generate names automatically def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) class WarningObject(NotationObject): """An warning raised by a Coq command or tactic.. @@ -497,7 +512,7 @@ class WarningObject(NotationObject): # Generate names automatically def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=unused-argument, dangerous-default-value @@ -516,7 +531,7 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]): """ notation = utils.unescape(text, 1) position = inliner.reporter.get_source_and_line(lineno) - return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], [] + return [nodes.literal(rawtext, '', notation_to_sphinx(notation, *position, rawtext=rawtext))], [] def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=dangerous-default-value diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index a889ebda7b..01c656eb23 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -13,21 +13,38 @@ grammar TacticNotations; // needs rendering (in particular whitespace (kept in output) vs. WHITESPACE // (discarded)). +// The distinction between nopipeblock and block is needed because we only want +// to require escaping within alternative blocks, so that e.g. `first [ x | y ]` +// can be written without escaping the `|`. + top: blocks EOF; blocks: block ((whitespace)? block)*; -block: atomic | meta | hole | repeat | curlies; -repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; + +block: pipe | nopipeblock; +nopipeblock: atomic | escaped | hole | alternative | repeat | curlies; + +alternative: LALT (WHITESPACE)? altblocks (WHITESPACE)? RBRACE; +altblocks: altblock ((WHITESPACE)? altsep (WHITESPACE)? altblock)+; +altblock: nopipeblock ((whitespace)? nopipeblock)*; + +repeat: LGROUP (ATOM | PIPE)? WHITESPACE blocks (WHITESPACE)? RBRACE; curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; + +pipe: PIPE; +altsep: PIPE; whitespace: WHITESPACE; -meta: METACHAR; +escaped: ESCAPED; atomic: ATOM (SUB)?; hole: ID (SUB)?; -LGROUP: '{' [+*?]; + +LALT: '{|'; +LGROUP: '{+' | '{*' | '{?'; LBRACE: '{'; RBRACE: '}'; -METACHAR: '%' [|(){}]; -ATOM: '@' | '_' | ~[@_{} ]+; +ESCAPED: '%{' | '%}' | '%|'; +PIPE: '|'; +ATOM: '@' | '_' | ~[@_{}| ]+; ID: '@' ('_'? [a-zA-Z0-9])+; SUB: '_' '_' [a-zA-Z0-9]+; WHITESPACE: ' '+; diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens index 88b38f97a6..2670e20aa6 100644 --- a/doc/tools/coqrst/notations/TacticNotations.tokens +++ b/doc/tools/coqrst/notations/TacticNotations.tokens @@ -1,10 +1,14 @@ -LGROUP=1 -LBRACE=2 -RBRACE=3 -METACHAR=4 -ATOM=5 -ID=6 -SUB=7 -WHITESPACE=8 -'{'=2 -'}'=3 +LALT=1 +LGROUP=2 +LBRACE=3 +RBRACE=4 +ESCAPED=5 +PIPE=6 +ATOM=7 +ID=8 +SUB=9 +WHITESPACE=10 +'{|'=1 +'{'=3 +'}'=4 +'|'=6 diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py index 27293e7e09..e3a115e32a 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.py +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py @@ -1,4 +1,4 @@ -# Generated from TacticNotations.g by ANTLR 4.7 +# Generated from TacticNotations.g by ANTLR 4.7.2 from antlr4 import * from io import StringIO from typing.io import TextIO @@ -7,28 +7,34 @@ import sys def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\n") - buf.write(":\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") - buf.write("\4\b\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3") - buf.write("\5\3\6\3\6\6\6 \n\6\r\6\16\6!\5\6$\n\6\3\7\3\7\5\7(\n") - buf.write("\7\3\7\6\7+\n\7\r\7\16\7,\3\b\3\b\3\b\6\b\62\n\b\r\b\16") - buf.write("\b\63\3\t\6\t\67\n\t\r\t\16\t8\2\2\n\3\3\5\4\7\5\t\6\13") - buf.write("\7\r\b\17\t\21\n\3\2\7\4\2,-AA\4\2*+}\177\4\2BBaa\7\2") - buf.write("\"\"BBaa}}\177\177\5\2\62;C\\c|\2?\2\3\3\2\2\2\2\5\3\2") - buf.write("\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2") - buf.write("\2\17\3\2\2\2\2\21\3\2\2\2\3\23\3\2\2\2\5\26\3\2\2\2\7") - buf.write("\30\3\2\2\2\t\32\3\2\2\2\13#\3\2\2\2\r%\3\2\2\2\17.\3") - buf.write("\2\2\2\21\66\3\2\2\2\23\24\7}\2\2\24\25\t\2\2\2\25\4\3") - buf.write("\2\2\2\26\27\7}\2\2\27\6\3\2\2\2\30\31\7\177\2\2\31\b") - buf.write("\3\2\2\2\32\33\7\'\2\2\33\34\t\3\2\2\34\n\3\2\2\2\35$") - buf.write("\t\4\2\2\36 \n\5\2\2\37\36\3\2\2\2 !\3\2\2\2!\37\3\2\2") - buf.write("\2!\"\3\2\2\2\"$\3\2\2\2#\35\3\2\2\2#\37\3\2\2\2$\f\3") - buf.write("\2\2\2%*\7B\2\2&(\7a\2\2\'&\3\2\2\2\'(\3\2\2\2()\3\2\2") - buf.write("\2)+\t\6\2\2*\'\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2") - buf.write("-\16\3\2\2\2./\7a\2\2/\61\7a\2\2\60\62\t\6\2\2\61\60\3") - buf.write("\2\2\2\62\63\3\2\2\2\63\61\3\2\2\2\63\64\3\2\2\2\64\20") - buf.write("\3\2\2\2\65\67\7\"\2\2\66\65\3\2\2\2\678\3\2\2\28\66\3") - buf.write("\2\2\289\3\2\2\29\22\3\2\2\2\t\2!#\',\638\2") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\f") + buf.write("M\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\3\2\3\2\3\2\3\3\3\3") + buf.write("\3\3\3\3\3\3\3\3\5\3!\n\3\3\4\3\4\3\5\3\5\3\6\3\6\3\6") + buf.write("\3\6\3\6\3\6\5\6-\n\6\3\7\3\7\3\b\3\b\6\b\63\n\b\r\b\16") + buf.write("\b\64\5\b\67\n\b\3\t\3\t\5\t;\n\t\3\t\6\t>\n\t\r\t\16") + buf.write("\t?\3\n\3\n\3\n\6\nE\n\n\r\n\16\nF\3\13\6\13J\n\13\r\13") + buf.write("\16\13K\2\2\f\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13") + buf.write("\25\f\3\2\5\4\2BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2V\2") + buf.write("\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3") + buf.write("\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2") + buf.write("\2\2\2\25\3\2\2\2\3\27\3\2\2\2\5 \3\2\2\2\7\"\3\2\2\2") + buf.write("\t$\3\2\2\2\13,\3\2\2\2\r.\3\2\2\2\17\66\3\2\2\2\218\3") + buf.write("\2\2\2\23A\3\2\2\2\25I\3\2\2\2\27\30\7}\2\2\30\31\7~\2") + buf.write("\2\31\4\3\2\2\2\32\33\7}\2\2\33!\7-\2\2\34\35\7}\2\2\35") + buf.write("!\7,\2\2\36\37\7}\2\2\37!\7A\2\2 \32\3\2\2\2 \34\3\2\2") + buf.write("\2 \36\3\2\2\2!\6\3\2\2\2\"#\7}\2\2#\b\3\2\2\2$%\7\177") + buf.write("\2\2%\n\3\2\2\2&\'\7\'\2\2\'-\7}\2\2()\7\'\2\2)-\7\177") + buf.write("\2\2*+\7\'\2\2+-\7~\2\2,&\3\2\2\2,(\3\2\2\2,*\3\2\2\2") + buf.write("-\f\3\2\2\2./\7~\2\2/\16\3\2\2\2\60\67\t\2\2\2\61\63\n") + buf.write("\3\2\2\62\61\3\2\2\2\63\64\3\2\2\2\64\62\3\2\2\2\64\65") + buf.write("\3\2\2\2\65\67\3\2\2\2\66\60\3\2\2\2\66\62\3\2\2\2\67") + buf.write("\20\3\2\2\28=\7B\2\29;\7a\2\2:9\3\2\2\2:;\3\2\2\2;<\3") + buf.write("\2\2\2<>\t\4\2\2=:\3\2\2\2>?\3\2\2\2?=\3\2\2\2?@\3\2\2") + buf.write("\2@\22\3\2\2\2AB\7a\2\2BD\7a\2\2CE\t\4\2\2DC\3\2\2\2E") + buf.write("F\3\2\2\2FD\3\2\2\2FG\3\2\2\2G\24\3\2\2\2HJ\7\"\2\2IH") + buf.write("\3\2\2\2JK\3\2\2\2KI\3\2\2\2KL\3\2\2\2L\26\3\2\2\2\13") + buf.write("\2 ,\64\66:?FK\2") return buf.getvalue() @@ -38,34 +44,36 @@ class TacticNotationsLexer(Lexer): decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] - LGROUP = 1 - LBRACE = 2 - RBRACE = 3 - METACHAR = 4 - ATOM = 5 - ID = 6 - SUB = 7 - WHITESPACE = 8 + LALT = 1 + LGROUP = 2 + LBRACE = 3 + RBRACE = 4 + ESCAPED = 5 + PIPE = 6 + ATOM = 7 + ID = 8 + SUB = 9 + WHITESPACE = 10 channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] modeNames = [ "DEFAULT_MODE" ] literalNames = [ "<INVALID>", - "'{'", "'}'" ] + "'{|'", "'{'", "'}'", "'|'" ] symbolicNames = [ "<INVALID>", - "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "SUB", - "WHITESPACE" ] + "LALT", "LGROUP", "LBRACE", "RBRACE", "ESCAPED", "PIPE", "ATOM", + "ID", "SUB", "WHITESPACE" ] - ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", - "SUB", "WHITESPACE" ] + ruleNames = [ "LALT", "LGROUP", "LBRACE", "RBRACE", "ESCAPED", "PIPE", + "ATOM", "ID", "SUB", "WHITESPACE" ] grammarFileName = "TacticNotations.g" def __init__(self, input=None, output:TextIO = sys.stdout): super().__init__(input, output) - self.checkVersion("4.7") + self.checkVersion("4.7.2") self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache()) self._actions = None self._predicates = None diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens index 88b38f97a6..2670e20aa6 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens @@ -1,10 +1,14 @@ -LGROUP=1 -LBRACE=2 -RBRACE=3 -METACHAR=4 -ATOM=5 -ID=6 -SUB=7 -WHITESPACE=8 -'{'=2 -'}'=3 +LALT=1 +LGROUP=2 +LBRACE=3 +RBRACE=4 +ESCAPED=5 +PIPE=6 +ATOM=7 +ID=8 +SUB=9 +WHITESPACE=10 +'{|'=1 +'{'=3 +'}'=4 +'|'=6 diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py index 645f078979..4a2a73672a 100644 --- a/doc/tools/coqrst/notations/TacticNotationsParser.py +++ b/doc/tools/coqrst/notations/TacticNotationsParser.py @@ -1,4 +1,4 @@ -# Generated from TacticNotations.g by ANTLR 4.7 +# Generated from TacticNotations.g by ANTLR 4.7.2 # encoding: utf-8 from antlr4 import * from io import StringIO @@ -7,31 +7,47 @@ import sys def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\n") - buf.write("J\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b") - buf.write("\t\b\4\t\t\t\4\n\t\n\3\2\3\2\3\2\3\3\3\3\5\3\32\n\3\3") - buf.write("\3\7\3\35\n\3\f\3\16\3 \13\3\3\4\3\4\3\4\3\4\3\4\5\4\'") - buf.write("\n\4\3\5\3\5\5\5+\n\5\3\5\3\5\3\5\5\5\60\n\5\3\5\3\5\3") - buf.write("\6\3\6\5\6\66\n\6\3\6\3\6\5\6:\n\6\3\6\3\6\3\7\3\7\3\b") - buf.write("\3\b\3\t\3\t\5\tD\n\t\3\n\3\n\5\nH\n\n\3\n\2\2\13\2\4") - buf.write("\6\b\n\f\16\20\22\2\2\2L\2\24\3\2\2\2\4\27\3\2\2\2\6&") - buf.write("\3\2\2\2\b(\3\2\2\2\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2") - buf.write("\2\20A\3\2\2\2\22E\3\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3") - buf.write("\26\3\3\2\2\2\27\36\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2") - buf.write("\2\31\32\3\2\2\2\32\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2") - buf.write("\2\2\35 \3\2\2\2\36\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2") - buf.write("\2\2 \36\3\2\2\2!\'\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2") - buf.write("$\'\5\b\5\2%\'\5\n\6\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2") - buf.write("&$\3\2\2\2&%\3\2\2\2\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*") - buf.write(")\3\2\2\2*+\3\2\2\2+,\3\2\2\2,-\7\n\2\2-/\5\4\3\2.\60") - buf.write("\7\n\2\2/.\3\2\2\2/\60\3\2\2\2\60\61\3\2\2\2\61\62\7\5") - buf.write("\2\2\62\t\3\2\2\2\63\65\7\4\2\2\64\66\5\f\7\2\65\64\3") - buf.write("\2\2\2\65\66\3\2\2\2\66\67\3\2\2\2\679\5\4\3\28:\5\f\7") - buf.write("\298\3\2\2\29:\3\2\2\2:;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2") - buf.write("=>\7\n\2\2>\r\3\2\2\2?@\7\6\2\2@\17\3\2\2\2AC\7\7\2\2") - buf.write("BD\7\t\2\2CB\3\2\2\2CD\3\2\2\2D\21\3\2\2\2EG\7\b\2\2F") - buf.write("H\7\t\2\2GF\3\2\2\2GH\3\2\2\2H\23\3\2\2\2\13\31\36&*/") - buf.write("\659CG") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\f") + buf.write("\u0081\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\4\f\t\f\4\r\t\r\4\16") + buf.write("\t\16\4\17\t\17\4\20\t\20\3\2\3\2\3\2\3\3\3\3\5\3&\n\3") + buf.write("\3\3\7\3)\n\3\f\3\16\3,\13\3\3\4\3\4\5\4\60\n\4\3\5\3") + buf.write("\5\3\5\3\5\3\5\3\5\5\58\n\5\3\6\3\6\5\6<\n\6\3\6\3\6\5") + buf.write("\6@\n\6\3\6\3\6\3\7\3\7\5\7F\n\7\3\7\3\7\5\7J\n\7\3\7") + buf.write("\3\7\6\7N\n\7\r\7\16\7O\3\b\3\b\5\bT\n\b\3\b\7\bW\n\b") + buf.write("\f\b\16\bZ\13\b\3\t\3\t\5\t^\n\t\3\t\3\t\3\t\5\tc\n\t") + buf.write("\3\t\3\t\3\n\3\n\5\ni\n\n\3\n\3\n\5\nm\n\n\3\n\3\n\3\13") + buf.write("\3\13\3\f\3\f\3\r\3\r\3\16\3\16\3\17\3\17\5\17{\n\17\3") + buf.write("\20\3\20\5\20\177\n\20\3\20\2\2\21\2\4\6\b\n\f\16\20\22") + buf.write("\24\26\30\32\34\36\2\3\3\2\b\t\2\u0086\2 \3\2\2\2\4#\3") + buf.write("\2\2\2\6/\3\2\2\2\b\67\3\2\2\2\n9\3\2\2\2\fC\3\2\2\2\16") + buf.write("Q\3\2\2\2\20[\3\2\2\2\22f\3\2\2\2\24p\3\2\2\2\26r\3\2") + buf.write("\2\2\30t\3\2\2\2\32v\3\2\2\2\34x\3\2\2\2\36|\3\2\2\2 ") + buf.write("!\5\4\3\2!\"\7\2\2\3\"\3\3\2\2\2#*\5\6\4\2$&\5\30\r\2") + buf.write("%$\3\2\2\2%&\3\2\2\2&\'\3\2\2\2\')\5\6\4\2(%\3\2\2\2)") + buf.write(",\3\2\2\2*(\3\2\2\2*+\3\2\2\2+\5\3\2\2\2,*\3\2\2\2-\60") + buf.write("\5\24\13\2.\60\5\b\5\2/-\3\2\2\2/.\3\2\2\2\60\7\3\2\2") + buf.write("\2\618\5\34\17\2\628\5\32\16\2\638\5\36\20\2\648\5\n\6") + buf.write("\2\658\5\20\t\2\668\5\22\n\2\67\61\3\2\2\2\67\62\3\2\2") + buf.write("\2\67\63\3\2\2\2\67\64\3\2\2\2\67\65\3\2\2\2\67\66\3\2") + buf.write("\2\28\t\3\2\2\29;\7\3\2\2:<\7\f\2\2;:\3\2\2\2;<\3\2\2") + buf.write("\2<=\3\2\2\2=?\5\f\7\2>@\7\f\2\2?>\3\2\2\2?@\3\2\2\2@") + buf.write("A\3\2\2\2AB\7\6\2\2B\13\3\2\2\2CM\5\16\b\2DF\7\f\2\2E") + buf.write("D\3\2\2\2EF\3\2\2\2FG\3\2\2\2GI\5\26\f\2HJ\7\f\2\2IH\3") + buf.write("\2\2\2IJ\3\2\2\2JK\3\2\2\2KL\5\16\b\2LN\3\2\2\2ME\3\2") + buf.write("\2\2NO\3\2\2\2OM\3\2\2\2OP\3\2\2\2P\r\3\2\2\2QX\5\b\5") + buf.write("\2RT\5\30\r\2SR\3\2\2\2ST\3\2\2\2TU\3\2\2\2UW\5\b\5\2") + buf.write("VS\3\2\2\2WZ\3\2\2\2XV\3\2\2\2XY\3\2\2\2Y\17\3\2\2\2Z") + buf.write("X\3\2\2\2[]\7\4\2\2\\^\t\2\2\2]\\\3\2\2\2]^\3\2\2\2^_") + buf.write("\3\2\2\2_`\7\f\2\2`b\5\4\3\2ac\7\f\2\2ba\3\2\2\2bc\3\2") + buf.write("\2\2cd\3\2\2\2de\7\6\2\2e\21\3\2\2\2fh\7\5\2\2gi\5\30") + buf.write("\r\2hg\3\2\2\2hi\3\2\2\2ij\3\2\2\2jl\5\4\3\2km\5\30\r") + buf.write("\2lk\3\2\2\2lm\3\2\2\2mn\3\2\2\2no\7\6\2\2o\23\3\2\2\2") + buf.write("pq\7\b\2\2q\25\3\2\2\2rs\7\b\2\2s\27\3\2\2\2tu\7\f\2\2") + buf.write("u\31\3\2\2\2vw\7\7\2\2w\33\3\2\2\2xz\7\t\2\2y{\7\13\2") + buf.write("\2zy\3\2\2\2z{\3\2\2\2{\35\3\2\2\2|~\7\n\2\2}\177\7\13") + buf.write("\2\2~}\3\2\2\2~\177\3\2\2\2\177\37\3\2\2\2\23%*/\67;?") + buf.write("EIOSX]bhlz~") return buf.getvalue() @@ -45,37 +61,47 @@ class TacticNotationsParser ( Parser ): sharedContextCache = PredictionContextCache() - literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ] + literalNames = [ "<INVALID>", "'{|'", "<INVALID>", "'{'", "'}'", "<INVALID>", + "'|'" ] - symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR", - "ATOM", "ID", "SUB", "WHITESPACE" ] + symbolicNames = [ "<INVALID>", "LALT", "LGROUP", "LBRACE", "RBRACE", + "ESCAPED", "PIPE", "ATOM", "ID", "SUB", "WHITESPACE" ] RULE_top = 0 RULE_blocks = 1 RULE_block = 2 - RULE_repeat = 3 - RULE_curlies = 4 - RULE_whitespace = 5 - RULE_meta = 6 - RULE_atomic = 7 - RULE_hole = 8 - - ruleNames = [ "top", "blocks", "block", "repeat", "curlies", "whitespace", - "meta", "atomic", "hole" ] + RULE_nopipeblock = 3 + RULE_alternative = 4 + RULE_altblocks = 5 + RULE_altblock = 6 + RULE_repeat = 7 + RULE_curlies = 8 + RULE_pipe = 9 + RULE_altsep = 10 + RULE_whitespace = 11 + RULE_escaped = 12 + RULE_atomic = 13 + RULE_hole = 14 + + ruleNames = [ "top", "blocks", "block", "nopipeblock", "alternative", + "altblocks", "altblock", "repeat", "curlies", "pipe", + "altsep", "whitespace", "escaped", "atomic", "hole" ] EOF = Token.EOF - LGROUP=1 - LBRACE=2 - RBRACE=3 - METACHAR=4 - ATOM=5 - ID=6 - SUB=7 - WHITESPACE=8 + LALT=1 + LGROUP=2 + LBRACE=3 + RBRACE=4 + ESCAPED=5 + PIPE=6 + ATOM=7 + ID=8 + SUB=9 + WHITESPACE=10 def __init__(self, input:TokenStream, output:TextIO = sys.stdout): super().__init__(input, output) - self.checkVersion("4.7") + self.checkVersion("4.7.2") self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache) self._predicates = None @@ -112,9 +138,9 @@ class TacticNotationsParser ( Parser ): self.enterRule(localctx, 0, self.RULE_top) try: self.enterOuterAlt(localctx, 1) - self.state = 18 + self.state = 30 self.blocks() - self.state = 19 + self.state = 31 self.match(TacticNotationsParser.EOF) except RecognitionException as re: localctx.exception = re @@ -163,24 +189,24 @@ class TacticNotationsParser ( Parser ): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 21 + self.state = 33 self.block() - self.state = 28 + self.state = 40 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,1,self._ctx) while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: if _alt==1: - self.state = 23 + self.state = 35 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 22 + self.state = 34 self.whitespace() - self.state = 25 + self.state = 37 self.block() - self.state = 30 + self.state = 42 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,1,self._ctx) @@ -198,18 +224,77 @@ class TacticNotationsParser ( Parser ): super().__init__(parent, invokingState) self.parser = parser + def pipe(self): + return self.getTypedRuleContext(TacticNotationsParser.PipeContext,0) + + + def nopipeblock(self): + return self.getTypedRuleContext(TacticNotationsParser.NopipeblockContext,0) + + + def getRuleIndex(self): + return TacticNotationsParser.RULE_block + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitBlock" ): + return visitor.visitBlock(self) + else: + return visitor.visitChildren(self) + + + + + def block(self): + + localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state) + self.enterRule(localctx, 4, self.RULE_block) + try: + self.state = 45 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [TacticNotationsParser.PIPE]: + self.enterOuterAlt(localctx, 1) + self.state = 43 + self.pipe() + pass + elif token in [TacticNotationsParser.LALT, TacticNotationsParser.LGROUP, TacticNotationsParser.LBRACE, TacticNotationsParser.ESCAPED, TacticNotationsParser.ATOM, TacticNotationsParser.ID]: + self.enterOuterAlt(localctx, 2) + self.state = 44 + self.nopipeblock() + pass + else: + raise NoViableAltException(self) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class NopipeblockContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + def atomic(self): return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0) - def meta(self): - return self.getTypedRuleContext(TacticNotationsParser.MetaContext,0) + def escaped(self): + return self.getTypedRuleContext(TacticNotationsParser.EscapedContext,0) def hole(self): return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0) + def alternative(self): + return self.getTypedRuleContext(TacticNotationsParser.AlternativeContext,0) + + def repeat(self): return self.getTypedRuleContext(TacticNotationsParser.RepeatContext,0) @@ -219,48 +304,53 @@ class TacticNotationsParser ( Parser ): def getRuleIndex(self): - return TacticNotationsParser.RULE_block + return TacticNotationsParser.RULE_nopipeblock def accept(self, visitor:ParseTreeVisitor): - if hasattr( visitor, "visitBlock" ): - return visitor.visitBlock(self) + if hasattr( visitor, "visitNopipeblock" ): + return visitor.visitNopipeblock(self) else: return visitor.visitChildren(self) - def block(self): + def nopipeblock(self): - localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state) - self.enterRule(localctx, 4, self.RULE_block) + localctx = TacticNotationsParser.NopipeblockContext(self, self._ctx, self.state) + self.enterRule(localctx, 6, self.RULE_nopipeblock) try: - self.state = 36 + self.state = 53 self._errHandler.sync(self) token = self._input.LA(1) if token in [TacticNotationsParser.ATOM]: self.enterOuterAlt(localctx, 1) - self.state = 31 + self.state = 47 self.atomic() pass - elif token in [TacticNotationsParser.METACHAR]: + elif token in [TacticNotationsParser.ESCAPED]: self.enterOuterAlt(localctx, 2) - self.state = 32 - self.meta() + self.state = 48 + self.escaped() pass elif token in [TacticNotationsParser.ID]: self.enterOuterAlt(localctx, 3) - self.state = 33 + self.state = 49 self.hole() pass - elif token in [TacticNotationsParser.LGROUP]: + elif token in [TacticNotationsParser.LALT]: self.enterOuterAlt(localctx, 4) - self.state = 34 + self.state = 50 + self.alternative() + pass + elif token in [TacticNotationsParser.LGROUP]: + self.enterOuterAlt(localctx, 5) + self.state = 51 self.repeat() pass elif token in [TacticNotationsParser.LBRACE]: - self.enterOuterAlt(localctx, 5) - self.state = 35 + self.enterOuterAlt(localctx, 6) + self.state = 52 self.curlies() pass else: @@ -274,6 +364,232 @@ class TacticNotationsParser ( Parser ): self.exitRule() return localctx + class AlternativeContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def LALT(self): + return self.getToken(TacticNotationsParser.LALT, 0) + + def altblocks(self): + return self.getTypedRuleContext(TacticNotationsParser.AltblocksContext,0) + + + def RBRACE(self): + return self.getToken(TacticNotationsParser.RBRACE, 0) + + def WHITESPACE(self, i:int=None): + if i is None: + return self.getTokens(TacticNotationsParser.WHITESPACE) + else: + return self.getToken(TacticNotationsParser.WHITESPACE, i) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_alternative + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAlternative" ): + return visitor.visitAlternative(self) + else: + return visitor.visitChildren(self) + + + + + def alternative(self): + + localctx = TacticNotationsParser.AlternativeContext(self, self._ctx, self.state) + self.enterRule(localctx, 8, self.RULE_alternative) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 55 + self.match(TacticNotationsParser.LALT) + self.state = 57 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 56 + self.match(TacticNotationsParser.WHITESPACE) + + + self.state = 59 + self.altblocks() + self.state = 61 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 60 + self.match(TacticNotationsParser.WHITESPACE) + + + self.state = 63 + self.match(TacticNotationsParser.RBRACE) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class AltblocksContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def altblock(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.AltblockContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.AltblockContext,i) + + + def altsep(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.AltsepContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.AltsepContext,i) + + + def WHITESPACE(self, i:int=None): + if i is None: + return self.getTokens(TacticNotationsParser.WHITESPACE) + else: + return self.getToken(TacticNotationsParser.WHITESPACE, i) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_altblocks + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAltblocks" ): + return visitor.visitAltblocks(self) + else: + return visitor.visitChildren(self) + + + + + def altblocks(self): + + localctx = TacticNotationsParser.AltblocksContext(self, self._ctx, self.state) + self.enterRule(localctx, 10, self.RULE_altblocks) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 65 + self.altblock() + self.state = 75 + self._errHandler.sync(self) + _alt = 1 + while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: + if _alt == 1: + self.state = 67 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 66 + self.match(TacticNotationsParser.WHITESPACE) + + + self.state = 69 + self.altsep() + self.state = 71 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 70 + self.match(TacticNotationsParser.WHITESPACE) + + + self.state = 73 + self.altblock() + + else: + raise NoViableAltException(self) + self.state = 77 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,8,self._ctx) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class AltblockContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def nopipeblock(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.NopipeblockContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.NopipeblockContext,i) + + + def whitespace(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.WhitespaceContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.WhitespaceContext,i) + + + def getRuleIndex(self): + return TacticNotationsParser.RULE_altblock + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAltblock" ): + return visitor.visitAltblock(self) + else: + return visitor.visitChildren(self) + + + + + def altblock(self): + + localctx = TacticNotationsParser.AltblockContext(self, self._ctx, self.state) + self.enterRule(localctx, 12, self.RULE_altblock) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 79 + self.nopipeblock() + self.state = 86 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,10,self._ctx) + while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: + if _alt==1: + self.state = 81 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 80 + self.whitespace() + + + self.state = 83 + self.nopipeblock() + self.state = 88 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,10,self._ctx) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + class RepeatContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -299,6 +615,9 @@ class TacticNotationsParser ( Parser ): def ATOM(self): return self.getToken(TacticNotationsParser.ATOM, 0) + def PIPE(self): + return self.getToken(TacticNotationsParser.PIPE, 0) + def getRuleIndex(self): return TacticNotationsParser.RULE_repeat @@ -314,33 +633,38 @@ class TacticNotationsParser ( Parser ): def repeat(self): localctx = TacticNotationsParser.RepeatContext(self, self._ctx, self.state) - self.enterRule(localctx, 6, self.RULE_repeat) + self.enterRule(localctx, 14, self.RULE_repeat) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 38 + self.state = 89 self.match(TacticNotationsParser.LGROUP) - self.state = 40 + self.state = 91 self._errHandler.sync(self) _la = self._input.LA(1) - if _la==TacticNotationsParser.ATOM: - self.state = 39 - self.match(TacticNotationsParser.ATOM) + if _la==TacticNotationsParser.PIPE or _la==TacticNotationsParser.ATOM: + self.state = 90 + _la = self._input.LA(1) + if not(_la==TacticNotationsParser.PIPE or _la==TacticNotationsParser.ATOM): + self._errHandler.recoverInline(self) + else: + self._errHandler.reportMatch(self) + self.consume() - self.state = 42 + self.state = 93 self.match(TacticNotationsParser.WHITESPACE) - self.state = 43 + self.state = 94 self.blocks() - self.state = 45 + self.state = 96 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 44 + self.state = 95 self.match(TacticNotationsParser.WHITESPACE) - self.state = 47 + self.state = 98 self.match(TacticNotationsParser.RBRACE) except RecognitionException as re: localctx.exception = re @@ -388,31 +712,31 @@ class TacticNotationsParser ( Parser ): def curlies(self): localctx = TacticNotationsParser.CurliesContext(self, self._ctx, self.state) - self.enterRule(localctx, 8, self.RULE_curlies) + self.enterRule(localctx, 16, self.RULE_curlies) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 49 + self.state = 100 self.match(TacticNotationsParser.LBRACE) - self.state = 51 + self.state = 102 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 50 + self.state = 101 self.whitespace() - self.state = 53 + self.state = 104 self.blocks() - self.state = 55 + self.state = 106 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 54 + self.state = 105 self.whitespace() - self.state = 57 + self.state = 108 self.match(TacticNotationsParser.RBRACE) except RecognitionException as re: localctx.exception = re @@ -422,6 +746,80 @@ class TacticNotationsParser ( Parser ): self.exitRule() return localctx + class PipeContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def PIPE(self): + return self.getToken(TacticNotationsParser.PIPE, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_pipe + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitPipe" ): + return visitor.visitPipe(self) + else: + return visitor.visitChildren(self) + + + + + def pipe(self): + + localctx = TacticNotationsParser.PipeContext(self, self._ctx, self.state) + self.enterRule(localctx, 18, self.RULE_pipe) + try: + self.enterOuterAlt(localctx, 1) + self.state = 110 + self.match(TacticNotationsParser.PIPE) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class AltsepContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def PIPE(self): + return self.getToken(TacticNotationsParser.PIPE, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_altsep + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAltsep" ): + return visitor.visitAltsep(self) + else: + return visitor.visitChildren(self) + + + + + def altsep(self): + + localctx = TacticNotationsParser.AltsepContext(self, self._ctx, self.state) + self.enterRule(localctx, 20, self.RULE_altsep) + try: + self.enterOuterAlt(localctx, 1) + self.state = 112 + self.match(TacticNotationsParser.PIPE) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + class WhitespaceContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -446,10 +844,10 @@ class TacticNotationsParser ( Parser ): def whitespace(self): localctx = TacticNotationsParser.WhitespaceContext(self, self._ctx, self.state) - self.enterRule(localctx, 10, self.RULE_whitespace) + self.enterRule(localctx, 22, self.RULE_whitespace) try: self.enterOuterAlt(localctx, 1) - self.state = 59 + self.state = 114 self.match(TacticNotationsParser.WHITESPACE) except RecognitionException as re: localctx.exception = re @@ -459,35 +857,35 @@ class TacticNotationsParser ( Parser ): self.exitRule() return localctx - class MetaContext(ParserRuleContext): + class EscapedContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): super().__init__(parent, invokingState) self.parser = parser - def METACHAR(self): - return self.getToken(TacticNotationsParser.METACHAR, 0) + def ESCAPED(self): + return self.getToken(TacticNotationsParser.ESCAPED, 0) def getRuleIndex(self): - return TacticNotationsParser.RULE_meta + return TacticNotationsParser.RULE_escaped def accept(self, visitor:ParseTreeVisitor): - if hasattr( visitor, "visitMeta" ): - return visitor.visitMeta(self) + if hasattr( visitor, "visitEscaped" ): + return visitor.visitEscaped(self) else: return visitor.visitChildren(self) - def meta(self): + def escaped(self): - localctx = TacticNotationsParser.MetaContext(self, self._ctx, self.state) - self.enterRule(localctx, 12, self.RULE_meta) + localctx = TacticNotationsParser.EscapedContext(self, self._ctx, self.state) + self.enterRule(localctx, 24, self.RULE_escaped) try: self.enterOuterAlt(localctx, 1) - self.state = 61 - self.match(TacticNotationsParser.METACHAR) + self.state = 116 + self.match(TacticNotationsParser.ESCAPED) except RecognitionException as re: localctx.exception = re self._errHandler.reportError(self, re) @@ -523,17 +921,17 @@ class TacticNotationsParser ( Parser ): def atomic(self): localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state) - self.enterRule(localctx, 14, self.RULE_atomic) + self.enterRule(localctx, 26, self.RULE_atomic) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 63 + self.state = 118 self.match(TacticNotationsParser.ATOM) - self.state = 65 + self.state = 120 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.SUB: - self.state = 64 + self.state = 119 self.match(TacticNotationsParser.SUB) @@ -572,17 +970,17 @@ class TacticNotationsParser ( Parser ): def hole(self): localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state) - self.enterRule(localctx, 16, self.RULE_hole) + self.enterRule(localctx, 28, self.RULE_hole) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 67 + self.state = 122 self.match(TacticNotationsParser.ID) - self.state = 69 + self.state = 124 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.SUB: - self.state = 68 + self.state = 123 self.match(TacticNotationsParser.SUB) diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py index c0bcc4af37..aba696c89f 100644 --- a/doc/tools/coqrst/notations/TacticNotationsVisitor.py +++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py @@ -1,4 +1,4 @@ -# Generated from TacticNotations.g by ANTLR 4.7 +# Generated from TacticNotations.g by ANTLR 4.7.2 from antlr4 import * if __name__ is not None and "." in __name__: from .TacticNotationsParser import TacticNotationsParser @@ -24,6 +24,26 @@ class TacticNotationsVisitor(ParseTreeVisitor): return self.visitChildren(ctx) + # Visit a parse tree produced by TacticNotationsParser#nopipeblock. + def visitNopipeblock(self, ctx:TacticNotationsParser.NopipeblockContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#alternative. + def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#altblocks. + def visitAltblocks(self, ctx:TacticNotationsParser.AltblocksContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#altblock. + def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by TacticNotationsParser#repeat. def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): return self.visitChildren(ctx) @@ -34,13 +54,23 @@ class TacticNotationsVisitor(ParseTreeVisitor): return self.visitChildren(ctx) + # Visit a parse tree produced by TacticNotationsParser#pipe. + def visitPipe(self, ctx:TacticNotationsParser.PipeContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#altsep. + def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by TacticNotationsParser#whitespace. def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): return self.visitChildren(ctx) - # Visit a parse tree produced by TacticNotationsParser#meta. - def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + # Visit a parse tree produced by TacticNotationsParser#escaped. + def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext): return self.visitChildren(ctx) diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index 87a41cf9f3..d2b5d86b37 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -13,12 +13,24 @@ Uses the dominate package. """ from dominate import tags +from dominate.utils import text from .parsing import parse from .TacticNotationsParser import TacticNotationsParser from .TacticNotationsVisitor import TacticNotationsVisitor class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): + def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext): + with tags.span(_class='alternative'): + self.visitChildren(ctx) + + def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext): + with tags.span(_class='alternative-block'): + self.visitChildren(ctx) + + def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext): + tags.span('\u200b', _class="alternative-separator") + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): with tags.span(_class="repeat-wrapper"): with tags.span(_class="repeat"): @@ -39,21 +51,20 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): tags.span(ctx.ATOM().getText()) + def visitPipe(self, ctx:TacticNotationsParser.PipeContext): + text("|") + def visitHole(self, ctx:TacticNotationsParser.HoleContext): tags.span(ctx.ID().getText()[1:], _class="hole") sub = ctx.SUB() if sub: tags.sub(sub.getText()[1:]) - def visitMeta(self, ctx:TacticNotationsParser.MetaContext): - txt = ctx.METACHAR().getText()[1:] - if (txt == "{") or (txt == "}"): - tags.span(txt) - else: - tags.span(txt, _class="meta") + def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext): + tags.span(ctx.ESCAPED().getText()[1:]) def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): - tags.span(" ") # TODO: no need for a <span> here + text(" ") def htmlize(notation): """Translate notation to a dominate HTML tree""" diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py index 506240d907..2312e09090 100644 --- a/doc/tools/coqrst/notations/parsing.py +++ b/doc/tools/coqrst/notations/parsing.py @@ -11,10 +11,22 @@ from .TacticNotationsLexer import TacticNotationsLexer from .TacticNotationsParser import TacticNotationsParser from antlr4 import CommonTokenStream, InputStream +from antlr4.error.ErrorListener import ErrorListener SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"), ("@qualid_or_string", "@id|@string")] +class ParseError(Exception): + def __init__(self, msg): + super().__init__() + self.msg = msg + +class ExceptionRaisingErrorListener(ErrorListener): + def syntaxError(self, recognizer, offendingSymbol, line, column, msg, e): + raise ParseError("{}:{}: {}".format(line, column, msg)) + +ERROR_LISTENER = ExceptionRaisingErrorListener() + def substitute(notation): """Perform common substitutions in the notation string. @@ -27,11 +39,13 @@ def substitute(notation): return notation def parse(notation): - """Parse a notation string. + """Parse a notation string, optionally reporting errors to `error_listener`. :return: An ANTLR AST. Use one of the supplied visitors (or write your own) to turn it into useful output. """ substituted = substitute(notation) lexer = TacticNotationsLexer(InputStream(substituted)) - return TacticNotationsParser(CommonTokenStream(lexer)).top() + parser = TacticNotationsParser(CommonTokenStream(lexer)) + parser.addErrorListener(ERROR_LISTENER) + return parser.top() diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py index f6e82fc68e..2180c8e6a5 100644 --- a/doc/tools/coqrst/notations/plain.py +++ b/doc/tools/coqrst/notations/plain.py @@ -22,8 +22,16 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor): def __init__(self): self.buffer = StringIO() + def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext): + self.buffer.write("[") + self.visitChildren(ctx) + self.buffer.write("]") + + def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext): + self.buffer.write("|") + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): - separator = ctx.ATOM() + separator = ctx.ATOM() or ctx.PIPE() self.visitChildren(ctx) if ctx.LGROUP().getText()[1] == "+": spacer = (separator.getText() + " " if separator else "") @@ -38,11 +46,14 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor): def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): self.buffer.write(ctx.ATOM().getText()) + def visitPipe(self, ctx:TacticNotationsParser.PipeContext): + self.buffer.write("|") + def visitHole(self, ctx:TacticNotationsParser.HoleContext): self.buffer.write("‘{}’".format(ctx.ID().getText()[1:])) - def visitMeta(self, ctx:TacticNotationsParser.MetaContext): - self.buffer.write(ctx.METACHAR().getText()[1:]) + def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext): + self.buffer.write(ctx.ESCAPED().getText()[1:]) def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): self.buffer.write(" ") diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index e05b834184..4ed09e04a9 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -20,8 +20,6 @@ from .TacticNotationsVisitor import TacticNotationsVisitor from docutils import nodes from sphinx import addnodes -import sys - class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): def defaultResult(self): return [] @@ -31,16 +29,36 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): aggregate.extend(nextResult) return aggregate + def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext): + return [nodes.inline('', '', *self.visitChildren(ctx), classes=['alternative'])] + + def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext): + return [nodes.inline('', '', *self.visitChildren(ctx), classes=['alternative-block'])] + + def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext): + return [nodes.inline('|', '\u200b', classes=['alternative-separator'])] + + @staticmethod + def is_alternative(node): + return isinstance(node, nodes.inline) and node['classes'] == ['alternative'] + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): # Uses inline nodes instead of subscript and superscript to ensure that # we get the right customization hooks at the LaTeX level wrapper = nodes.inline('', '', classes=['repeat-wrapper']) - wrapper += nodes.inline('', '', *self.visitChildren(ctx), classes=["repeat"]) + + children = self.visitChildren(ctx) + if len(children) == 1 and self.is_alternative(children[0]): + # Use a custom style if an alternative is nested in a repeat. + # (We could detect this in CSS, but it's much harder in LaTeX.) + + children[0]['classes'] = ['repeated-alternative'] + wrapper += nodes.inline('', '', *children, classes=["repeat"]) repeat_marker = ctx.LGROUP().getText()[1] wrapper += nodes.inline(repeat_marker, repeat_marker, classes=['notation-sup']) - separator = ctx.ATOM() + separator = ctx.ATOM() or ctx.PIPE() if separator: sep = separator.getText() wrapper += nodes.inline(sep, sep, classes=['notation-sub']) @@ -65,6 +83,9 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): return [node] + def visitPipe(self, ctx:TacticNotationsParser.PipeContext): + return [nodes.Text("|")] + def visitHole(self, ctx:TacticNotationsParser.HoleContext): hole = ctx.ID().getText() token_name = hole[1:] @@ -75,23 +96,18 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): sub_index = sub.getText()[2:] node += nodes.subscript(sub_index, sub_index) - return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)] + return [addnodes.pending_xref(token_name, node, reftype='token', + refdomain='std', reftarget=token_name)] - def visitMeta(self, ctx:TacticNotationsParser.MetaContext): - meta = ctx.METACHAR().getText() - metachar = meta[1:] # remove escape char - token_name = metachar - if (metachar == "{") or (metachar == "}"): - classes=[] - else: - classes=["meta"] - return [nodes.inline(metachar, token_name, classes=classes)] + def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext): + escaped = ctx.ESCAPED().getText() + return [nodes.inline(escaped, escaped[1:])] def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): return [nodes.Text(" ")] def sphinxify(notation): - """Translate notation into a Sphinx document tree""" + """Translate a notation into a Sphinx document tree.""" vs = TacticNotationsToSphinxVisitor() return vs.visit(parse(notation)) diff --git a/engine/evd.ml b/engine/evd.ml index 0f10a380d3..15b4c31851 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -222,7 +222,7 @@ let map_evar_body f = function let map_evar_info f evi = {evi with evar_body = map_evar_body f evi.evar_body; - evar_hyps = map_named_val f evi.evar_hyps; + evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps; evar_concl = f evi.evar_concl; evar_candidates = Option.map (List.map f) evi.evar_candidates } diff --git a/engine/proofview.ml b/engine/proofview.ml index 1fd8b5d50e..5c5a02d3fa 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -46,7 +46,7 @@ let compact el ({ solution } as pv) = let apply_subst_einfo _ ei = Evd.({ ei with evar_concl = nf ei.evar_concl; - evar_hyps = Environ.map_named_val nf0 ei.evar_hyps; + evar_hyps = Environ.map_named_val (fun d -> map_constr nf0 d) ei.evar_hyps; evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in diff --git a/interp/impargs.ml b/interp/impargs.ml index 90fb5a2036..806fe93297 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -497,9 +497,9 @@ type implicit_interactive_request = type implicit_discharge_request = | ImplLocal - | ImplConstant of Constant.t * implicits_flags + | ImplConstant of implicits_flags | ImplMutualInductive of MutInd.t * implicits_flags - | ImplInteractive of GlobRef.t * implicits_flags * + | ImplInteractive of implicits_flags * implicit_interactive_request let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits" @@ -552,39 +552,24 @@ let add_section_impls vars extra_impls (cond,impls) = let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None - | ImplInteractive (ref,flags,exp) -> - (try - let vars = variable_section_segment_of_reference ref in - let extra_impls = impls_of_context vars in - let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in - Some (ImplInteractive (ref,flags,exp),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) - | ImplConstant (con,flags) -> - (try - let vars = variable_section_segment_of_reference (ConstRef con) in - let extra_impls = impls_of_context vars in - let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in - let l' = [ConstRef con,newimpls] in - Some (ImplConstant (con,flags),l') - with Not_found -> (* con not defined in this section *) Some (req,l)) - | ImplMutualInductive (kn,flags) -> - (try - let l' = List.map (fun (gr, l) -> - let vars = variable_section_segment_of_reference gr in - let extra_impls = impls_of_context vars in - (gr, - List.map (add_section_impls vars extra_impls) l)) l - in - Some (ImplMutualInductive (kn,flags),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) + | ImplMutualInductive _ | ImplInteractive _ | ImplConstant _ -> + let l' = + try + List.map (fun (gr, l) -> + let vars = variable_section_segment_of_reference gr in + let extra_impls = impls_of_context vars in + let newimpls = List.map (add_section_impls vars extra_impls) l in + (gr, newimpls)) l + with Not_found -> l in + Some (req,l') let rebuild_implicits (req,l) = match req with | ImplLocal -> assert false - | ImplConstant (con,flags) -> - let oldimpls = snd (List.hd l) in - let newimpls = compute_constant_implicits flags con in - req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] + | ImplConstant flags -> + let ref,oldimpls = List.hd l in + let newimpls = compute_global_implicits flags ref in + req, [ref, List.map2 merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> let newimpls = compute_all_mib_implicits flags kn in let rec aux olds news = @@ -595,15 +580,14 @@ let rebuild_implicits (req,l) = | _, _ -> assert false in req, aux l newimpls - | ImplInteractive (ref,flags,o) -> + | ImplInteractive (flags,o) -> + let ref,oldimpls = List.hd l in (if isVarRef ref && is_in_section ref then ImplLocal else req), match o with | ImplAuto -> - let oldimpls = snd (List.hd l) in let newimpls = compute_global_implicits flags ref in [ref,List.map2 merge_impls oldimpls newimpls] | ImplManual userimplsize -> - let oldimpls = snd (List.hd l) in if flags.auto then let newimpls = List.hd (compute_global_implicits flags ref) in let p = List.length (snd newimpls) - userimplsize in @@ -638,7 +622,7 @@ let declare_implicits_gen req flags ref = let declare_implicits local ref = let flags = { !implicit_args with auto = true } in let req = - if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in + if is_local local ref then ImplLocal else ImplInteractive(flags,ImplAuto) in declare_implicits_gen req flags ref let declare_var_implicits id = @@ -647,7 +631,7 @@ let declare_var_implicits id = let declare_constant_implicits con = let flags = !implicit_args in - declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con) + declare_implicits_gen (ImplConstant flags) flags (ConstRef con) let declare_mib_implicits kn = let flags = !implicit_args in @@ -697,7 +681,7 @@ let declare_manual_implicits local ref ?enriching l = let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in let req = if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) + else ImplInteractive(flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l])) let maybe_declare_manual_implicits local ref ?enriching l = @@ -756,7 +740,7 @@ let set_implicits local ref l = compute_implicit_statuses autoimpls imps)) l in let req = if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) + else ImplInteractive(flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l'])) let extract_impargs_data impls = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index dffccf02fc..6277d874dd 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -281,7 +281,7 @@ let implicits_of_glob_constr ?(with_products=true) l = | _ -> () in [] | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i b + | GLetIn (na, b, t, c) -> aux i c | GRec (fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) diff --git a/kernel/environ.ml b/kernel/environ.ml index 67125e9ad1..05f342a82a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -187,7 +187,7 @@ let match_named_context_val c = match c.env_named_ctx with let map_named_val f ctxt = let open Context.Named.Declaration in let fold accu d = - let d' = map_constr f d in + let d' = f d in let accu = if d == d' then accu else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu diff --git a/kernel/environ.mli b/kernel/environ.mli index 6d3756e891..f6cd41861e 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -134,9 +134,9 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t (** [map_named_val f ctxt] apply [f] to the body and the type of each declarations. - *** /!\ *** [f t] should be convertible with t *) + *** /!\ *** [f t] should be convertible with t, and preserve the name *) val map_named_val : - (constr -> constr) -> named_context_val -> named_context_val + (named_declaration -> named_declaration) -> named_context_val -> named_context_val val push_named : Constr.named_declaration -> env -> env val push_named_context : Constr.named_context -> env -> env diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 469551809c..12b12bc7b0 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -278,7 +278,7 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF } | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) - => { VtUnknown, VtNow } + => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } -> { add_morphism_infer atts m n } diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a68efa4713..963b7189f9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1800,7 +1800,7 @@ let anew_instance ~pstate atts binders instance fields = let program_mode = atts.program in new_instance ~pstate ~program_mode atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord (fields))) - ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info + ~global:atts.global ~generalize:false Hints.empty_hint_info let declare_instance_refl ~pstate atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" diff --git a/stm/stm.ml b/stm/stm.ml index 21618bc044..6f7cefb582 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -364,7 +364,6 @@ module VCS : sig val set_parsing_state : id -> Vernacstate.Parser.state -> unit val get_parsing_state : id -> Vernacstate.Parser.state option val get_proof_mode : id -> Pvernac.proof_mode option - val set_proof_mode : id -> Pvernac.proof_mode option -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : block_start:id -> block_stop:id -> vcs @@ -572,6 +571,7 @@ end = struct (* {{{ *) (match Vernacprop.under_control x with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i + | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -611,7 +611,6 @@ end = struct (* {{{ *) info.state <- new_state let get_proof_mode id = (get_info id).proof_mode - let set_proof_mode id pm = (get_info id).proof_mode <- pm let reached id = let info = get_info id in @@ -3050,53 +3049,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.set_parsing_state id parsing_state) new_ids; `Ok - (* Unknown: we execute it, check for open goals and propagate sideeff *) - | VtUnknown, VtNow -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - if not (get_allow_nested_proofs ()) && in_proof then - "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." - |> Pp.str - |> (fun s -> (UserError (None, s), Exninfo.null)) - |> State.exn_on ~valid:Stateid.dummy newtip - |> Exninfo.iraise - else - let id = VCS.new_node ~id:newtip proof_mode () in - let head_id = VCS.get_branch_pos head in - let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) - let step () = - VCS.checkout VCS.Branch.master; - let mid = VCS.get_branch_pos VCS.Branch.master in - let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in - let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id st x); - (* Vernac x may or may not start a proof *) - if not in_proof && PG_compat.there_are_pending_proofs () then - begin - let bname = VCS.mk_branch_name x in - let opacity_of_produced_term = function - (* This AST is ambiguous, hence we check it dynamically *) - | VernacInstance (_,_ , None, _) -> GuaranteesOpacity - | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); - VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ())); - VCS.branch bname (`Proof (VCS.proof_nesting () + 1)); - end else begin - begin match (VCS.get_branch head).VCS.kind with - | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - | `Proof _ -> - VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - (* We hope it can be replayed, but we can't really know *) - ignore(VCS.propagate_sideff ~action:(ReplayCommand x)); - end; - VCS.checkout_shallowest_proof_branch (); - end in - State.define ~doc ~safe_id:head_id ~cache:true step id; - Backtrack.record (); `Ok - - | VtUnknown, VtLater -> - anomaly(str"classifier: VtUnknown must imply VtNow.") - | VtProofMode pm, VtNow -> let proof_mode = Pvernac.lookup_proof_mode pm in let id = VCS.new_node ~id:newtip proof_mode () in @@ -3106,7 +3058,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtProofMode _, VtLater -> anomaly(str"classifier: VtProofMode must imply VtNow.") - end in let pr_rc rc = match rc with | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"]) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 4a4c5c94e9..7cecd801e4 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -21,7 +21,6 @@ let string_of_parallel = function | `No -> "" let string_of_vernac_type = function - | VtUnknown -> "Unknown" | VtStartProof _ -> "StartProof" | VtSideff _ -> "Sideff" | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" @@ -61,7 +60,7 @@ let options_affecting_stm_scheduling = ] let classify_vernac e = - let static_classifier ~poly e = match e with + let static_classifier ~atts e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) @@ -97,15 +96,18 @@ let classify_vernac e = VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater | VernacDefinition (_,({v=i},_),ProveBody _) -> - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof(guarantee, idents_of_name i), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof(guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = List.map (fun (({v=i}, _), _) -> i) l in - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (guarantee,ids), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let ids = List.map (fun (({v=i}, _), _) -> i) l in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -115,8 +117,9 @@ let classify_vernac e = then VtStartProof (guarantee,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -185,8 +188,12 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow | VernacProofMode pm -> VtProofMode pm, VtNow - (* These are ambiguous *) - | VernacInstance _ -> VtUnknown, VtNow + | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater + | VernacInstance (_,((name,_),_,_),_,_) -> + VtSideff (idents_of_name name.CAst.v), VtLater (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ @@ -201,9 +208,8 @@ let classify_vernac e = with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier v = v |> CAst.with_val (function - | VernacExpr (f, e) -> - let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in - static_classifier ~poly e + | VernacExpr (atts, e) -> + static_classifier ~atts e | VernacTimeout (_,e) -> static_control_classifier e | VernacTime (_,e) | VernacRedirect (_, e) -> static_control_classifier e @@ -214,6 +220,6 @@ let classify_vernac e = | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtLater - | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)) + | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater)) in static_control_classifier e diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2bdfc85d6d..9dafa8bad9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -614,7 +614,7 @@ let cofix id = mutual_cofix id [] 0 type tactic_reduction = Reductionops.reduction_function type e_tactic_reduction = Reductionops.e_reduction_function -let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma = +let e_pf_change_decl (redfun : bool -> e_reduction_function) where env sigma decl = let open Context.Named.Declaration in match decl with | LocalAssum (id,ty) -> @@ -713,28 +713,61 @@ let e_change_in_hyp ~check ~reorder redfun (id,where) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let hyp = Tacmach.New.pf_get_hyp id gl in - let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in + let (sigma, c) = e_pf_change_decl redfun where (Proofview.Goal.env gl) sigma hyp in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (convert_hyp ~check ~reorder c) end +type hyp_conversion = +| AnyHypConv (** Arbitrary conversion *) +| StableHypConv (** Does not introduce new dependencies on variables *) +| LocalHypConv (** Same as above plus no dependence on the named environment *) + let e_change_in_hyps ~check ~reorder f args = Proofview.Goal.enter begin fun gl -> - let fold (env, sigma) arg = - let (redfun, id, where) = f arg in - let hyp = - try lookup_named id env - with Not_found -> - raise (RefinerError (env, sigma, NoSuchHyp id)) + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let (env, sigma) = match reorder with + | LocalHypConv -> + (* If the reduction function is known not to depend on the named + context, then we can perform it in parallel. *) + let fold accu arg = + let (id, redfun) = f arg in + let old = try Id.Map.find id accu with Not_found -> [] in + Id.Map.add id (redfun :: old) accu + in + let reds = List.fold_left fold Id.Map.empty args in + let evdref = ref sigma in + let map d = + let id = NamedDecl.get_id d in + match Id.Map.find id reds with + | reds -> + let d = EConstr.of_named_decl d in + let fold redfun (sigma, d) = redfun env sigma d in + let (sigma, d) = List.fold_right fold reds (sigma, d) in + let () = evdref := sigma in + EConstr.Unsafe.to_named_decl d + | exception Not_found -> d in - let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in - let sign = Logic.convert_hyp ~check ~reorder env sigma d in + let sign = Environ.map_named_val map (Environ.named_context_val env) in let env = reset_with_named_context sign env in - (env, sigma) + (env, !evdref) + | StableHypConv | AnyHypConv -> + let reorder = reorder == AnyHypConv in + let fold (env, sigma) arg = + let (id, redfun) = f arg in + let hyp = + try lookup_named id env + with Not_found -> + raise (RefinerError (env, sigma, NoSuchHyp id)) + in + let (sigma, d) = redfun env sigma hyp in + let sign = Logic.convert_hyp ~check ~reorder env sigma d in + let env = reset_with_named_context sign env in + (env, sigma) + in + List.fold_left fold (env, sigma) args in - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let (env, sigma) = List.fold_left fold (env, sigma) args in let ty = Proofview.Goal.concl gl in Proofview.Unsafe.tclEVARS sigma <*> @@ -851,10 +884,12 @@ let change ~check chg c cls = let f (id, occs, where) = let occl = bind_change_occurrences occs chg in let redfun deep env sigma t = change_on_subterm ~check Reduction.CONV deep c occl env sigma t in - (redfun, id, where) + let redfun env sigma d = e_pf_change_decl redfun where env sigma d in + (id, redfun) in + let reorder = if check then AnyHypConv else StableHypConv in (* Don't check, we do it already in [change_on_subterm] *) - e_change_in_hyps ~check:false ~reorder:check f hyps + e_change_in_hyps ~check:false ~reorder f hyps end let change_concl t = @@ -881,6 +916,22 @@ let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast) (* The main reduction function *) +let is_local_flag env flags = + if flags.rDelta then false + else + let check = function + | EvalVarRef _ -> false + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + in + List.for_all check flags.rConst + +let is_local_unfold env flags = + let check (_, c) = match c with + | EvalVarRef _ -> false + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + in + List.for_all check flags + let reduce redexp cl = let trace env sigma = let open Printer in @@ -889,23 +940,33 @@ let reduce redexp cl = in Proofview.Trace.name_tactic trace begin Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in - let reorder = match redexp with Fold _ | Pattern _ -> true | _ -> false in + let reorder = match redexp with + | Fold _ | Pattern _ -> AnyHypConv + | Simpl (flags, _) | Cbv flags | Cbn flags | Lazy flags -> + if is_local_flag env flags then LocalHypConv else StableHypConv + | Unfold flags -> + if is_local_unfold env flags then LocalHypConv else StableHypConv + | Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv + | ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*) + in begin match cl.concl_occs with | NoOccurrences -> Proofview.tclUNIT () | occs -> let redexp = bind_red_expr_occurrences occs nbcl redexp in - let redfun = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + let redfun = Redexpr.reduction_of_red_expr env redexp in e_change_in_concl ~check (revert_cast redfun) end <*> let f (id, occs, where) = let redexp = bind_red_expr_occurrences occs nbcl redexp in - let (redfun, _) = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in let redfun _ env sigma c = redfun env sigma c in - (redfun, id, where) + let redfun env sigma d = e_pf_change_decl redfun where env sigma d in + (id, redfun) in e_change_in_hyps ~check ~reorder f hyps end diff --git a/test-suite/bugs/closed/bug_10189.v b/test-suite/bugs/closed/bug_10189.v new file mode 100644 index 0000000000..d603bff386 --- /dev/null +++ b/test-suite/bugs/closed/bug_10189.v @@ -0,0 +1,9 @@ +Definition foo : forall (x := unit) {y : nat}, nat := fun y => y. +Check foo (y := 3). (*We fail to get implicits in the type past a let-in*) +Definition foo' : forall (x : Set) {y : nat}, nat := fun _ y => y. +Check foo' unit (y := 3). (* It works with a function binder *) + +Definition bar := let f {x} : nat -> nat := fun y => x in f (x := 3). +(* Adding bar : nat -> nat gives implicits-in-term warning *) +Fail Check bar (x := 3). +(* The implicits from the type of the local definition leak to the outer term *) diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v new file mode 100644 index 0000000000..e1823ac54c --- /dev/null +++ b/test-suite/bugs/closed/bug_3890.v @@ -0,0 +1,12 @@ +Set Nested Proofs Allowed. + +Class Foo. +Class Bar := b : Type. + +Instance foo : Foo. + +Instance bar : Bar. +exact Type. +Defined. + +Defined. diff --git a/test-suite/bugs/closed/bug_4429.v b/test-suite/bugs/closed/bug_4429.v deleted file mode 100644 index bf0e570ab8..0000000000 --- a/test-suite/bugs/closed/bug_4429.v +++ /dev/null @@ -1,31 +0,0 @@ -Require Import Arith.Compare_dec. -Require Import Unicode.Utf8. - -Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := - match n with - | O => x - | S n' => f (my_nat_iter n' f x) - end. - -Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := - match mn with - | (0, 0) => 0 - | (0, S n') => S n' - | (S m', 0) => S m' - | (S m', S n') => - match le_gt_dec (S m') (S n') with - | left _ => f (S m', S n' - S m') - | right _ => f (S m' - S n', S n') - end - end. - -Axiom max_correct_l : ∀ m n : nat, m <= max m n. -Axiom max_correct_r : ∀ m n : nat, n <= max m n. - -Hint Resolve max_correct_l max_correct_r : arith. - -Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). -Proof. - intros. - Timeout 3 eauto with arith. -Qed. diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v index a8a446cc9b..3f40569d61 100644 --- a/test-suite/bugs/closed/bug_4580.v +++ b/test-suite/bugs/closed/bug_4580.v @@ -2,6 +2,5 @@ Require Import Program. Class Foo (A : Type) := foo : A. -Unset Refine Instance Mode. Program Instance f1 : Foo nat := S _. Next Obligation. exact 0. Defined. diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v new file mode 100644 index 0000000000..951fe5302b --- /dev/null +++ b/test-suite/bugs/closed/bug_4638.v @@ -0,0 +1,12 @@ +Set Nested Proofs Allowed. + +Class Foo. + +Goal True. + +Instance foo: Foo. +Qed. + +trivial. + +Qed. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v deleted file mode 100644 index 9d83743b2a..0000000000 --- a/test-suite/bugs/opened/bug_3890.v +++ /dev/null @@ -1,22 +0,0 @@ -Set Nested Proofs Allowed. - -Class Foo. -Class Bar := b : Type. - -Set Refine Instance Mode. -Instance foo : Foo := _. -Unset Refine Instance Mode. -(* 1 subgoals, subgoal 1 (ID 4) - - ============================ - Foo *) - -Instance bar : Bar. -exact Type. -Defined. -(* bar is defined *) - -About foo. -(* foo not a defined object. *) - -Fail Defined. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 3888cafed3..736d05fefc 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -198,9 +198,7 @@ Module UniqueInstances. for it. *) Set Typeclasses Unique Instances. Class Eq (A : Type) : Set. - Set Refine Instance Mode. - Instance eqa : Eq nat := _. constructor. Qed. - Unset Refine Instance Mode. + Instance eqa : Eq nat. Qed. Instance eqb : Eq nat := {}. Class Foo (A : Type) (e : Eq A) : Set. Instance fooa : Foo _ eqa := {}. diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index 05d63d9a47..49e0af9b2c 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -14,4 +14,3 @@ Local Set Warnings "-deprecated". Require Export Coq.Compat.Coq810. Unset Private Polymorphic Universes. -Set Refine Instance Mode. diff --git a/vernac/classes.ml b/vernac/classes.ml index ece9fc8937..05a75ab435 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -31,16 +31,6 @@ module NamedDecl = Context.Named.Declaration open Decl_kinds open Entries -let refine_instance = ref false - -let () = Goptions.(declare_bool_option { - optdepr = true; - optname = "definition of instances by refining"; - optkey = ["Refine";"Instance";"Mode"]; - optread = (fun () -> !refine_instance); - optwrite = (fun b -> refine_instance := b) -}) - let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) @@ -419,7 +409,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po | None -> pstate) ()) -let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = +let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -503,7 +493,7 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program let term = to_constr sigma (Option.get term) in (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype; None) - else if program_mode || refine || Option.is_empty props then + else if program_mode || Option.is_empty props then declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in id, pstate @@ -550,7 +540,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = sigma, cl, u, c', ctx', ctx, imps, args, decl -let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mode +let new_instance ~pstate ?(global=false) ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in @@ -566,7 +556,7 @@ let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mo Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode + do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri = diff --git a/vernac/classes.mli b/vernac/classes.mli index e7f90ff306..57bb9ce312 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -48,7 +48,6 @@ val declare_instance_constant : val new_instance : pstate:Proof_global.t option -> ?global:bool (** Not global by default. *) -> - ?refine:bool (** Allow refinement *) -> program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index ef06e59316..730f5fd6da 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -36,7 +36,6 @@ type vernac_type = | VtProofMode of string (* To be removed *) | VtMeta - | VtUnknown and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 4d89eaffd9..54e08d0e95 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -52,7 +52,6 @@ type vernac_type = | VtProofMode of string (* To be removed *) | VtMeta - | VtUnknown and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = |