diff options
Diffstat (limited to 'doc')
43 files changed, 1093 insertions, 462 deletions
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/common/styles/html/coqremote/modules/system/system.css b/doc/common/styles/html/coqremote/modules/system/system.css index 9371bb479e..9556c7882a 100644 --- a/doc/common/styles/html/coqremote/modules/system/system.css +++ b/doc/common/styles/html/coqremote/modules/system/system.css @@ -327,7 +327,7 @@ html.js fieldset.collapsed legend a { * html.js fieldset.collapsed table * { display: inline; } -/* For Safari 2 to prevent collapsible fieldsets containing tables from dissapearing due to tableheader.js. */ +/* For Safari 2 to prevent collapsible fieldsets containing tables from disappearing due to tableheader.js. */ html.js fieldset.collapsible { position: relative; } diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 3c0355c92d..e9b91d5a7e 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,16 +1,16 @@ -let edeclare ?hook ~ontop ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = +let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:tyopt ~body in let uctx = Evd.evar_universe_context sigma in let ubinders = Evd.universe_binders sigma in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ~ontop ident k ce ubinders imps ?hook_data + DeclareDef.declare_definition ident k ce ubinders imps ?hook_data let packed_declare_definition ~poly ident value_with_constraints = let body, ctx = value_with_constraints in let sigma = Evd.from_ctx ctx in let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in let udecl = UState.default_univ_decl in - ignore (edeclare ~ontop:None ident k ~opaque:false sigma udecl body None []) + ignore (edeclare ident k ~opaque:false sigma udecl body None []) (* But this definition cannot be undone by Reset ident *) diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg index 82ba45726e..f4d9e7fd5b 100644 --- a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg +++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg @@ -33,7 +33,7 @@ TACTIC EXTEND collapse_hyps END (* More advanced examples, where automatic proof happens but - no tactic is being called explicitely. The first one uses + no tactic is being called explicitly. The first one uses type classes. *) VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY | [ "Tuto3_3" int(n) ] -> { example_classes n } 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..3dc8707a34 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 @@ -168,7 +168,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: .. cmd:: Extraction NoInline {+ @qualid } - Conversely, the constants mentionned by this command will + Conversely, the constants mentioned by this command will never be inlined during extraction. .. cmd:: Print Extraction Inline diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index b474c51f17..68f6d4008a 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:: @@ -440,7 +441,7 @@ First class setoids and morphisms The implementation is based on a first-class representation of properties of relations and morphisms as typeclasses. That is, the various combinations of properties on relations and morphisms are -represented as records and instances of theses classes are put in a +represented as records and instances of these classes are put in a hint database. For example, the declaration: .. coqdoc:: @@ -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..2ba13db042 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`. @@ -385,7 +385,7 @@ few other commands related to typeclasses. .. note:: As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully - mimicks what happens during typeclass resolution when it is called + mimics what happens during typeclass resolution when it is called during refinement/type inference, except that *only* declared class subgoals are considered at the start of resolution during type inference, while ``all`` can select non-class subgoals as well. It might @@ -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/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 6b10b7c0b3..1aa2111816 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -449,7 +449,7 @@ underscore or by omitting the annotation to a polymorphic definition. This option, on by default, removes universes which appear only in the body of an opaque polymorphic definition from the definition's universe arguments. As such, no value needs to be provided for - these universes when instanciating the definition. Universe + these universes when instantiating the definition. Universe constraints are automatically adjusted. Consider the following definition: diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index cca3b2e06b..701c62cdce 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -186,7 +186,7 @@ Coq is now continuously tested against OCaml trunk, in addition to the oldest supported and latest OCaml releases. Coq's documentation for the development branch is now deployed -continously at https://coq.github.io/doc/master/api (documentation of +continuously at https://coq.github.io/doc/master/api (documentation of the ML API), https://coq.github.io/doc/master/refman (reference manual), and https://coq.github.io/doc/master/stdlib (documentation of the standard library). Similar links exist for the `v8.10` branch. @@ -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). @@ -666,7 +665,7 @@ changes: - New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by Matthieu Sozeau, for controlling the opacity status of variables and constants in hint databases. It is recommended to always use these - commands after creating a hint databse with :cmd:`Create HintDb`. + commands after creating a hint database with :cmd:`Create HintDb`. - Multiple sections with the same name are now allowed, by Jasper Hugunin. @@ -893,7 +892,7 @@ Vernacular Commands `Inductive list (A : Type) := nil : list | cons : A -> list -> list.` - New `Set Hint Variables/Constants Opaque/Transparent` commands for setting globally the opacity flag of variables and constants in hint databases, - overwritting the opacity set of the hint database. + overwriting the opacity set of the hint database. - Added generic syntax for "attributes", as in: `#[local] Lemma foo : bar.` - Added the `Numeral Notation` command for registering decimal numeral @@ -1130,7 +1129,7 @@ Tactics few rare incompatibilities (it was unintendedly recursively rewriting in the side conditions generated by H). - Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure - properties of the executation of a tactic without keeping the effect + properties of the execution of a tactic without keeping the effect of the execution. - `vm_compute` now supports existential variables. - Calls to `shelve` and `give_up` within calls to tactic `refine` now working. @@ -1263,7 +1262,7 @@ Tools Tactic language - The undocumented "nameless" forms `fix N`, `cofix` have been - deprecated; please use `fix ident N /cofix ident` to explicitely + deprecated; please use `fix ident N /cofix ident` to explicitly name the (co)fixpoint hypothesis to be introduced. Documentation @@ -2954,7 +2953,7 @@ Other bugfixes - Fix incorrect behavior of CS resolution - #4591: Uncaught exception in directory browsing. - CoqIDE is more resilient to initialization errors. -- #4614: "Fully check the document" is uninterruptable. +- #4614: "Fully check the document" is uninterruptible. - Try eta-expansion of records only on non-recursive ones - Fix bug when a sort is ascribed to a Record - Primitive projections: protect kernel from erroneous definitions. @@ -3443,7 +3442,7 @@ Libraries * all functions over type Z : Z.add, Z.mul, ... * the minimal proofs of specifications for these functions : Z.add_0_l, ... - * an instantation of all derived properties proved generically in Numbers : + * an instantiation of all derived properties proved generically in Numbers : Z.add_comm, Z.add_assoc, ... A large part of ZArith is now simply compatibility notations, for instance @@ -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 @@ -4624,7 +4623,7 @@ Setoid rewriting + Setoid_Theory is now an alias to Equivalence, scripts building objects of type Setoid_Theory need to unfold (or "red") the definitions of Reflexive, Symmetric and Transitive in order to get the same goals - as before. Scripts which introduced variables explicitely will not break. + as before. Scripts which introduced variables explicitly will not break. + The order of subgoals when doing [setoid_rewrite] with side-conditions is always the same: first the new goal, then the conditions. @@ -5023,7 +5022,7 @@ Syntax Language and commands -- Added sort-polymorphism for definitions in Type (but finally abandonned). +- Added sort-polymorphism for definitions in Type (but finally abandoned). - Support for implicit arguments in the types of parameters in (co-)fixpoints and (co-)inductive declarations. - Improved type inference: use as much of possible general information. @@ -5252,7 +5251,7 @@ Library - New file about the factorial function in Arith -- An additional elimination Acc_iter for Acc, simplier than Acc_rect. +- An additional elimination Acc_iter for Acc, simpler than Acc_rect. This new elimination principle is used for definition well_founded_induction. - New library NArith on binary natural numbers @@ -5337,7 +5336,7 @@ Bugs Miscellaneous - Implicit parameters of inductive types definition now taken into - account for infering other implicit arguments + account for inferring other implicit arguments Incompatibilities @@ -5418,7 +5417,7 @@ Gallina Known problems of the automatic translation - iso-latin-1 characters are no longer supported: move your files to - 7-bits ASCII or unicode before translation (swith to unicode is + 7-bits ASCII or unicode before translation (switch to unicode is automatically done if a file is loaded and saved again by coqide) - Renaming in ZArith: incompatibilities in Coq user contribs due to merging names INZ, from Reals, and inject_nat. @@ -5443,7 +5442,7 @@ Vernacular commands - "Functional Scheme" and "Functional Induction" extended to polymorphic types and dependent types - Notation now allows recursive patterns, hence recovering parts of the - fonctionalities of pre-V8 Grammar/Syntax commands + functionalities of pre-V8 Grammar/Syntax commands - Command "Print." discontinued. - Redundant syntax "Implicit Arguments On/Off" discontinued diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst index 0f5b991ba4..c4a48d6985 100644 --- a/doc/sphinx/history.rst +++ b/doc/sphinx/history.rst @@ -110,7 +110,7 @@ advantage of special hardware, debuggers, and the like. We hope that |Coq| can be of use to researchers interested in experimenting with this new methodology. -.. [#years] At the time of writting, i.e. 1995. +.. [#years] At the time of writing, i.e. 1995. Versions 1 to 5 --------------- @@ -305,7 +305,7 @@ Michel Mauny, Ascander Suarez and Pierre Weis. V3.1 was started in the summer of 1986, V3.2 was frozen at the end of November 1986. V3.4 was developed in the first half of 1987. -Thierry Coquand held a post-doctoral position in Cambrige University +Thierry Coquand held a post-doctoral position in Cambridge University in 1986-87, where he developed a variant implementation in SML, with which he wrote some developments on fixpoints in Scott's domains. @@ -345,7 +345,7 @@ lemmas when local hypotheses of proofs were discharged. This gave a notion of global mathematical environment with local sections. Another significant practical change was that the system, originally -developped on the VAX central computer of our lab, was transferred on +developed on the VAX central computer of our lab, was transferred on SUN personal workstations, allowing a level of distributed development. The extraction algorithm was modified, with three annotations ``Pos``, ``Null`` and ``Typ`` decorating the sorts ``Prop`` @@ -503,7 +503,7 @@ of CNRS-ENS Lyon. Chetan Murthy joined the team in 1991 and became the main software architect of Version 5. He completely rehauled the implementation for efficiency. Versions 5.6 and 5.8 were major distributed versions, -with complete documentation and a library of users' developements. The +with complete documentation and a library of users' developments. The use of the RCS revision control system, and systematic ChangeLog files, allow a more precise tracking of the software developments. @@ -1330,7 +1330,7 @@ Language - Inductive definitions now accept ">" in constructor types to declare the corresponding constructor as a coercion. -- Idem for assumptions declarations and constants when the type is mentionned. +- Idem for assumptions declarations and constants when the type is mentioned. - The "Coercion" and "Canonical Structure" keywords now accept the same syntax as "Definition", i.e. "hyps :=c (:t)?" or "hyps :t". - Theorem-like declaration now accepts the syntax "Theorem thm [x:t;...] : u". @@ -1383,7 +1383,7 @@ Tactics it can also recognize 'False' in the hypothesis and use it to solve the goal. - Coercions now handled in "with" bindings -- "Subst x" replaces all ocurrences of x by t in the goal and hypotheses +- "Subst x" replaces all occurrences of x by t in the goal and hypotheses when an hypothesis x=t or x:=t or t=x exists - Fresh names for Assert and Pose now based on collision-avoiding Intro naming strategy (exceptional source of incompatibilities) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ba766c8c3d..c48964d66c 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 @@ -2131,24 +2131,71 @@ Implicit generalization .. index:: `{ } .. index:: `( ) +.. index:: `{! } +.. index:: `(! ) Implicit generalization is an automatic elaboration of a statement with free variables into a closed statement where these variables are -quantified explicitly. Implicit generalization is done inside binders -starting with a \` and terms delimited by \`{ } and \`( ), always -introducing maximally inserted implicit arguments for the generalized -variables. Inside implicit generalization delimiters, free variables -in the current context are automatically quantified using a product or -a lambda abstraction to generate a closed term. In the following -statement for example, the variables n and m are automatically -generalized and become explicit arguments of the lemma as we are using -\`( ): +quantified explicitly. -.. coqtop:: all +It is activated for a binder by prefixing a \`, and for terms by +surrounding it with \`{ } or \`( ). + +Terms surrounded by \`{ } introduce their free variables as maximally +inserted implicit arguments, and terms surrounded by \`( ) introduce +them as explicit arguments. + +Generalizing binders always introduce their free variables as +maximally inserted implicit arguments. The binder itself introduces +its argument as usual. + +In the following statement, ``A`` and ``y`` are automatically +generalized, ``A`` is implicit and ``x``, ``y`` and the anonymous +equality argument are explicit. + +.. coqtop:: all reset Generalizable All Variables. - Lemma nat_comm : `(n = n + 0). + Definition sym `(x:A) : `(x = y -> y = x) := fun _ p => eq_sym p. + + Print sym. + +Dually to normal binders, the name is optional but the type is required: + +.. coqtop:: all + + Check (forall `{x = y :> A}, y = x). + +When generalizing a binder whose type is a typeclass, its own class +arguments are omitted from the syntax and are generalized using +automatic names, without instance search. Other arguments are also +generalized unless provided. This produces a fully general statement. +this behaviour may be disabled by prefixing the type with a ``!`` or +by forcing the typeclass name to be an explicit application using +``@`` (however the later ignores implicit argument information). + +.. coqtop:: all + + Class Op (A:Type) := op : A -> A -> A. + + Class Commutative (A:Type) `(Op A) := commutative : forall x y, op x y = op y x. + Instance nat_op : Op nat := plus. + + Set Printing Implicit. + Check (forall `{Commutative }, True). + Check (forall `{Commutative nat}, True). + Fail Check (forall `{Commutative nat _}, True). + Fail Check (forall `{!Commutative nat}, True). + Arguments Commutative _ {_}. + Check (forall `{!Commutative nat}, True). + Check (forall `{@Commutative nat plus}, True). + +Multiple binders can be merged using ``,`` as a separator: + +.. coqtop:: all + + Check (forall `{Commutative A, Hnat : !Commutative nat}, True). One can control the set of generalizable identifiers with the ``Generalizable`` vernacular command to avoid unexpected @@ -2167,7 +2214,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. @@ -2176,22 +2223,6 @@ that specify which variables should be generalizable. Allows exporting the choice of generalizable variables. -One can also use implicit generalization for binders, in which case -the generalized variables are added as binders and set maximally -implicit. - -.. coqtop:: all - - Definition id `(x : A) : A := x. - - Print id. - -The generalizing binders \`{ } and \`( ) work similarly to their -explicit counterparts, only binding the generalized variables -implicitly, as maximally-inserted arguments. In these binders, the -binding name for the bound object is optional, whereas the type is -mandatory, dually to regular binders. - .. _Coercions: Coercions 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..fed7111628 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 @@ -708,7 +708,7 @@ tactic for printing. By copying the definition of :tacn:`time_constr` from the standard library, - users can achive support for a fixed pattern of nesting by passing + users can achieve support for a fixed pattern of nesting by passing different :token:`string` parameters to :tacn:`restart_timer` and :tacn:`finish_timing` at each level of nesting. @@ -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 ~~~~~~~~~~~~~~~~~~~~~~~ @@ -1676,7 +1676,7 @@ It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in |Ltac| and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The -reasons for the performence degradation can be intricate, like a slowly +reasons for the performance degradation can be intricate, like a slowly performing |Ltac| match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending on its calling context. Thus 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..b19b0742c1 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: @@ -853,7 +853,7 @@ An *occurrence switch* can be: algorithm in a local definition, instead of copying large terms by hand. -It is important to remember that matching *preceeds* occurrence +It is important to remember that matching *precedes* occurrence selection. .. example:: @@ -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: @@ -2455,7 +2455,7 @@ the holes are abstracted in term. Lemma test : True. have: _ * 0 = 0. - The invokation of ``have`` is equivalent to: + The invocation of ``have`` is equivalent to: .. coqtop:: reset none @@ -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 @@ -4927,7 +4927,7 @@ bookkeeping steps. apply/PQequiv. thus in this case, the tactic ``apply/PQequiv`` is equivalent to - ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is tha analogue of + ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is the analogue of ``iffRL`` for the converse implication. Any |SSR| term whose type coerces to a double implication can be @@ -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..2ee23df019 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`. @@ -3714,7 +3714,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. cmdv:: Hint Resolve -> @term : @ident Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentionned + the hint will be used as :n:`apply <- @term`, although as mentioned before, the tactic actually used is a restricted version of :tacn:`apply`). @@ -3777,13 +3777,13 @@ 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 hints in the database for all constants or all variables, - overwritting the existing settings of opacity. It is advised + overwriting the existing settings of opacity. It is advised to use this just after a :cmd:`Create HintDb` command. .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident @@ -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..6da42f4a48 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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1191,7 +1198,7 @@ The ``function_scope`` interpretation scope The scope ``function_scope`` also has a special status. It is temporarily activated each time the argument of a global reference is -recognized to be a ``Funclass`` istance, i.e., of type :g:`forall x:A, B` or +recognized to be a ``Funclass`` instance, i.e., of type :g:`forall x:A, B` or :g:`A -> B`. diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index d8ac640f2a..dde8a7b838 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -412,7 +412,7 @@ but its behaviour is not to fold the abbreviation at all.}. {\tt LetTac} could be followed by a specification (called a clause) of the places where the abbreviation had to be folded (hypothese and/or conclusion). Clauses are the syntactic notion to denote in which parts -of a goal a given transformation shold occur. Its basic notation is +of a goal a given transformation should occur. Its basic notation is either \TERM{*} (meaning everywhere), or {\tt\textrm{\em hyps} |- \textrm{\em concl}} where {\em hyps} is either \TERM{*} (to denote all the hypotheses), or a comma-separated list of either hypothesis name, @@ -620,7 +620,7 @@ These constraints are met by the makefiles produced by {\tt coq\_makefile} Otherwise, modify your build program so as to pass option {\tt -translate} to program {\tt coqc}. The effect of this option is to -ouptut the translated source of any {\tt .v} file in a file with +output the translated source of any {\tt .v} file in a file with extension {\tt .v8} located in the same directory than the original file. @@ -675,7 +675,7 @@ solve all occurrences of the problem. The definition of identifiers changed. Most of those changes are handled by the translator. They include: \begin{itemize} -\item {\tt \_} is not an identifier anymore: it is tranlated to {\tt +\item {\tt \_} is not an identifier anymore: it is translated to {\tt x\_} \item avoid clash with new keywords by adding a trailing {\tt \_} \end{itemize} diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index 1de9890992..ba58ff0084 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -52,7 +52,7 @@ def is_whitespace_string(elem): return isinstance(elem, NavigableString) and elem.strip() == "" def strip_soup(soup, pred): - """Strip elements maching pred from front and tail of soup.""" + """Strip elements matching pred from front and tail of soup.""" while soup.contents and pred(soup.contents[-1]): soup.contents.pop() 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/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 26f6255069..2b124ee5c1 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -47,7 +47,7 @@ class CoqTop: :param coqtop_bin: The path to coqtop; uses $COQBIN by default, falling back to "coqtop" :param color: When True, tell coqtop to produce ANSI color codes (see the ansicolors module) - :param args: Additional arugments to coqtop. + :param args: Additional arguments to coqtop. """ self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") if not pexpect.utils.which(self.coqtop_bin): @@ -68,7 +68,7 @@ class CoqTop: self.coqtop.kill(9) def next_prompt(self): - """Wait for the next coqtop prompt, and return the output preceeding it.""" + """Wait for the next coqtop prompt, and return the output preceding it.""" self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10) return self.coqtop.before diff --git a/doc/whodidwhat/whodidwhat-8.2update.tex b/doc/whodidwhat/whodidwhat-8.2update.tex index 4f4f0e952e..f45e6564f2 100644 --- a/doc/whodidwhat/whodidwhat-8.2update.tex +++ b/doc/whodidwhat/whodidwhat-8.2update.tex @@ -181,7 +181,7 @@ \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu \item Searching: Hugo Herbelin, Yves Bertot -\item Whelp suppport: Hugo Herbelin +\item Whelp support: Hugo Herbelin \end{itemize} \section{Parsing and printing} diff --git a/doc/whodidwhat/whodidwhat-8.3update.tex b/doc/whodidwhat/whodidwhat-8.3update.tex index 0a07378169..7cce0083d5 100644 --- a/doc/whodidwhat/whodidwhat-8.3update.tex +++ b/doc/whodidwhat/whodidwhat-8.3update.tex @@ -188,7 +188,7 @@ \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu \item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech -\item Whelp suppport: Hugo Herbelin +\item Whelp support: Hugo Herbelin \end{itemize} \section{Parsing and printing} diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex index bb4c5ce469..2d74a653ed 100644 --- a/doc/whodidwhat/whodidwhat-8.4update.tex +++ b/doc/whodidwhat/whodidwhat-8.4update.tex @@ -191,7 +191,7 @@ \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu \item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech -\item Whelp suppport: Hugo Herbelin +\item Whelp support: Hugo Herbelin \end{itemize} \section{Parsing and printing} diff --git a/doc/whodidwhat/whodidwhat-8.5update.tex b/doc/whodidwhat/whodidwhat-8.5update.tex index ce099dc363..600ecf93db 100644 --- a/doc/whodidwhat/whodidwhat-8.5update.tex +++ b/doc/whodidwhat/whodidwhat-8.5update.tex @@ -197,7 +197,7 @@ \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu \item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech -\item Whelp suppport: Hugo Herbelin +\item Whelp support: Hugo Herbelin \end{itemize} \section{Parsing and printing} |