diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/README.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 181 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 8 |
13 files changed, 230 insertions, 38 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 32de15ee31..1643baf0e8 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -239,6 +239,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition for more details. + Optionally, any text immediately following the ``.. example::`` header is + used as the example's title. + Example:: .. example:: Adding a hint to a database diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index b6c35d8fa7..0f2d35d044 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -32,6 +32,7 @@ When the proof ends two constants are defined: ends with ``Qed``, and transparent if the proof ends with ``Defined``. .. example:: + .. coqtop:: all Require Coq.derive.Derive. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 98e81ebc65..6e0c1e1b61 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -723,6 +723,7 @@ each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{ the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts). .. example:: + The declaration for parameterized lists is: .. math:: @@ -741,6 +742,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is | cons : A -> list A -> list A. .. example:: + The declaration for a mutual inductive definition of tree and forest is: @@ -763,6 +765,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is | consf : tree -> forest -> forest. .. example:: + The declaration for a mutual inductive definition of even and odd is: .. math:: @@ -811,6 +814,7 @@ contains an inductive declaration. E[Γ] ⊢ c : C .. example:: + Provided that our environment :math:`E` contains inductive definitions we showed before, these two inference rules above enable us to conclude that: @@ -919,6 +923,7 @@ condition* for a constant :math:`X` in the following cases: .. example:: + For instance, if one considers the following variant of a tree type branching over the natural numbers: @@ -985,6 +990,7 @@ the Type hierarchy. .. example:: + It is well known that the existential quantifier can be encoded as an inductive definition. The following declaration introduces the second- order existential quantifier :math:`∃ X.P(X)`. @@ -1102,6 +1108,7 @@ sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). A an example, let us consider the following definition: .. example:: + .. coqtop:: in Inductive option (A:Type) : Type := @@ -1118,6 +1125,7 @@ if :g:`option` is applied to a type in :math:`\Prop`, then, the result is not se if set in :math:`\Prop`. .. example:: + .. coqtop:: all Check (fun A:Set => option A). @@ -1126,6 +1134,7 @@ if set in :math:`\Prop`. Here is another example. .. example:: + .. coqtop:: in Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. @@ -1136,6 +1145,7 @@ none in :math:`\Type`, and in :math:`\Type` otherwise. In all cases, the three k eliminations schemes are allowed. .. example:: + .. coqtop:: all Check (fun A:Set => prod A). @@ -1324,6 +1334,7 @@ the extraction mechanism. Assume :math:`A` and :math:`B` are two propositions, a logical disjunction :math:`A ∨ B` is defined inductively by: .. example:: + .. coqtop:: in Inductive or (A B:Prop) : Prop := @@ -1334,6 +1345,7 @@ The following definition which computes a boolean value by case over the proof of :g:`or A B` is not accepted: .. example:: + .. coqtop:: all Fail Definition choice (A B: Prop) (x:or A B) := @@ -1357,6 +1369,7 @@ property which are provably different, contradicting the proof- irrelevance property which is sometimes a useful axiom: .. example:: + .. coqtop:: all Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. @@ -1390,6 +1403,7 @@ be used for rewriting not only in logical propositions but also in any type. .. example:: + .. coqtop:: all Print eq_rec. @@ -1421,6 +1435,7 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math: .. example:: + The following term in concrete syntax:: match t as l return P' with @@ -1485,6 +1500,7 @@ definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_ .. example:: + Below is a typing rule for the term shown in the previous example: .. inference:: list example @@ -1634,6 +1650,7 @@ The following definitions are correct, we enter them using the :cmd:`Fixpoint` command and show the internal representation. .. example:: + .. coqtop:: all Fixpoint plus (n m:nat) {struct n} : nat := @@ -1810,6 +1827,7 @@ option ``-impredicative-set``. For example, using the ordinary `coqtop` command, the following is rejected, .. example:: + .. coqtop:: all Fail Definition id: Set := forall X:Set,X->X. diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 52c56d2bd2..9de30e2190 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -848,6 +848,7 @@ Notation Interpretation Precedence Associativity .. example:: + .. coqtop:: all reset Require Import ZArith. @@ -887,6 +888,7 @@ Notation Interpretation =============== =================== .. example:: + .. coqtop:: all reset Require Import Reals. @@ -906,6 +908,7 @@ tactics (see Chapter :ref:`tactics`), there are also: Proves that two real integer constants are different. .. example:: + .. coqtop:: all reset Require Import DiscrR. @@ -919,6 +922,7 @@ tactics (see Chapter :ref:`tactics`), there are also: Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions. .. example:: + .. coqtop:: all reset Require Import Reals. @@ -933,6 +937,7 @@ tactics (see Chapter :ref:`tactics`), there are also: corresponding to the condition on each operand of the product. .. example:: + .. coqtop:: all reset Require Import Reals. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 394b928ada..7dd0a6e383 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -70,7 +70,9 @@ generates a variant type definition with just one constructor: To build an object of type :n:`@ident`, one should provide the constructor :n:`@ident₀` with the appropriate number of terms filling the fields of the record. -.. example:: Let us define the rational :math:`1/2`: +.. example:: + + Let us define the rational :math:`1/2`: .. coqtop:: in @@ -1849,15 +1851,15 @@ are named as expected. .. example:: (continued) -.. coqtop:: all + .. coqtop:: all - Arguments p [s t] _ [u] _: rename. + Arguments p [s t] _ [u] _: rename. - Check (p r1 (u:=c)). + Check (p r1 (u:=c)). - Check (p (s:=a) (t:=b) r1 (u:=c) r2). + Check (p (s:=a) (t:=b) r1 (u:=c) r2). - Fail Arguments p [s t] _ [w] _ : assert. + Fail Arguments p [s t] _ [w] _ : assert. .. _displaying-implicit-args: diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 8250b4b3d6..da5cd00d72 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -758,6 +758,7 @@ Simple inductive types the case of annotated inductive types — cf. next section). .. example:: + The set of natural numbers is defined as: .. coqtop:: all @@ -976,6 +977,7 @@ Mutually defined inductive types reason, the parameters must be strictly the same for each inductive types. .. example:: + The typical example of a mutual inductive data type is the one for trees and forests. We assume given two types :g:`A` and :g:`B` as variables. It can be declared the following way. @@ -1048,6 +1050,7 @@ of the type. For co-inductive types, the only elimination principle is case analysis. .. example:: + An example of a co-inductive type is the type of infinite sequences of natural numbers, usually called streams. @@ -1067,6 +1070,7 @@ Definition of co-inductive predicates and blocks of mutually co-inductive definitions are also allowed. .. example:: + An example of a co-inductive predicate is the extensional equality on streams: @@ -1129,6 +1133,7 @@ constructions. .. example:: + One can define the addition function as : .. coqtop:: all @@ -1201,6 +1206,7 @@ constructions. inductive types. .. example:: + The size of trees and forests can be defined the following way: .. coqtop:: all diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e15bcb8e2c..59bc2d22aa 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -218,6 +218,7 @@ file timing data: On ``Mac OS``, this works best if you’ve installed ``gnu-time``. .. example:: + For example, the output of ``make TIMED=1`` may look like this: @@ -295,6 +296,7 @@ file timing data: files which take effectively no time to compile. .. example:: + For example, the output table from ``make print-pretty-timed-diff`` may look like this: @@ -318,6 +320,7 @@ line timing data: line-by-line timing information. .. example:: + For example, running ``make all TIMING=1`` may result in a file like this: :: @@ -345,6 +348,7 @@ line timing data: This target requires python to build the table. .. example:: + For example, running ``print-pretty-single-time-diff`` might give a table like this: :: diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 78719c1ef1..225df8d54c 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -341,8 +341,7 @@ involves conditional rewritings and shows how to deal with them using the optional tactic of the ``Hint Rewrite`` command. -.. example:: - Ackermann function +.. example:: Ackermann function .. coqtop:: in reset @@ -370,8 +369,7 @@ the optional tactic of the ``Hint Rewrite`` command. autorewrite with base0 using try reflexivity. -.. example:: - MacCarthy function +.. example:: MacCarthy function .. coqtop:: in reset diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 44376080c3..a9d0c16376 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -375,6 +375,7 @@ or focus the next one. The following example script illustrates all these features: .. example:: + .. coqtop:: all Goal (((True /\ True) /\ True) /\ True) /\ True. @@ -511,6 +512,7 @@ Requesting information :token:`ident` .. example:: + .. coqtop:: all Show Match nat. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 6fb73a030f..8a2fc3996a 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -4632,6 +4632,7 @@ bookkeeping steps. .. example:: + The following example use the ``~~`` prenex notation for boolean negation: diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index e6bc84365c..fdb04bf9a0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -207,6 +207,7 @@ Applying theorems useful to advanced users. .. example:: + .. coqtop:: reset all Inductive Option : Set := @@ -366,6 +367,7 @@ Applying theorems .. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product. .. example:: + Assume we have a transitive relation ``R`` on ``nat``: .. coqtop:: reset in @@ -837,6 +839,7 @@ quantified variables or hypotheses until the goal is not any more a quantification or an implication. .. example:: + .. coqtop:: all Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. @@ -958,6 +961,7 @@ quantification or an implication. .. exn:: Cannot move @ident after @ident : it depends on @ident. .. example:: + .. coqtop:: all Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. @@ -1082,6 +1086,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. obtain atomic ones. .. example:: + .. coqtop:: all Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. @@ -1252,6 +1257,7 @@ Controlling the proof flow respect to some term. .. example:: + .. coqtop:: reset none Goal forall x y:nat, 0 <= x + y + y. @@ -1567,6 +1573,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) performs induction using this subterm. .. example:: + .. coqtop:: reset all Lemma induction_test : forall n:nat, n = n -> n <= n. @@ -1636,6 +1643,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) those are generalized as well in the statement to prove. .. example:: + .. coqtop:: reset all Lemma comm x y : x + y = y + x. @@ -1744,6 +1752,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) still get enough information in the proofs. .. example:: + .. coqtop:: reset all Lemma le_minus : forall n:nat, n < 1 -> n = 0. @@ -1809,6 +1818,7 @@ and an explanation of the underlying technique. Note that this tactic is only available after a ``Require Import FunInd``. .. example:: + .. coqtop:: reset all Require Import FunInd. @@ -2856,6 +2866,7 @@ the conversion in hypotheses :n:`{+ @ident}`. + A constant can be marked to be never unfolded by ``cbn`` or ``simpl``: .. example:: + .. coqtop:: all Arguments minus n m : simpl never. @@ -2868,6 +2879,7 @@ the conversion in hypotheses :n:`{+ @ident}`. ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command. .. example:: + .. coqtop:: all Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). @@ -2880,6 +2892,7 @@ the conversion in hypotheses :n:`{+ @ident}`. always unfolded. .. example:: + .. coqtop:: all Definition volatile := fun x : nat => x. @@ -2890,6 +2903,7 @@ the conversion in hypotheses :n:`{+ @ident}`. such arguments. .. example:: + .. coqtop:: all Arguments minus !n !m. @@ -3180,6 +3194,7 @@ where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` can solve such a goal: .. example:: + .. coqtop:: all Hint Resolve ex_intro. @@ -3748,6 +3763,7 @@ The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would fail: .. example:: + .. coqtop:: reset all Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. @@ -3904,6 +3920,7 @@ equality must contain all the quantified variables in order for congruence to match against it. .. example:: + .. coqtop:: reset all Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. @@ -4315,6 +4332,7 @@ declare new field structures. All declared field structures can be printed with the Print Fields command. .. example:: + .. coqtop:: reset all Require Import Reals. @@ -4426,6 +4444,7 @@ Simple tactic macros A simple example has more value than a long explanation: .. example:: + .. coqtop:: reset all Ltac Solve := simpl; intros; auto. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dcefa293b1..37394386e6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -146,7 +146,7 @@ expected to be inferred at typing time. Notation "x = y" := (@eq _ x y) (at level 70, no associativity). One can define *closed* notations whose both sides are symbols. In this case, -the default precedence level for the inner subexpression is 200, and the default +the default precedence level for the inner sub-expression is 200, and the default level for the notation itself is 0. .. coqtop:: in @@ -185,7 +185,7 @@ rules. Some simple left factorization work has to be done. Here is an example. Notation "x < y" := (lt x y) (at level 70). Notation "x < y < z" := (x < y /\ y < z) (at level 70). -In order to factorize the left part of the rules, the subexpression +In order to factorize the left part of the rules, the sub-expression referred by ``y`` has to be at the same level in both rules. However the default behavior puts ``y`` at the next level below 70 in the first rule (``no associativity`` is the default), and at the level 200 in the second @@ -209,7 +209,7 @@ of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`. .. cmd:: Print Grammar pattern. This displays the state of the subparser of patterns (the parser used in the - grammar of the match with constructions). + grammar of the ``match with`` constructions). Displaying symbolic notations @@ -519,7 +519,7 @@ is just an identifier, one could have said ``p at level 99 as strict pattern``. Note also that in the absence of a ``as ident``, ``as strict pattern`` or -``as pattern`` modifiers, the default is to consider subexpressions occurring +``as pattern`` modifiers, the default is to consider sub-expressions occurring in binding position and parsed as terms to be ``as ident``. .. _NotationsWithBinders: @@ -650,7 +650,7 @@ example of recursive notation with closed binders: A recursive pattern for binders can be used in position of a recursive pattern for terms. Here is an example: -.. coqtop:: in +.. coqtop:: in Notation "'FUNAPP' x .. y , f" := (fun x => .. (fun y => (.. (f x) ..) y ) ..) @@ -691,6 +691,117 @@ side. E.g.: Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9). +Custom entries +~~~~~~~~~~~~~~ + +.. cmd:: Declare Custom Entry @ident + + This command allows to define new grammar entries, called *custom + entries*, that can later be referred to using the entry name + :n:`custom @ident`. For instance, we may want to define an ad hoc + parser for arithmetical operations and proceed as follows: + +.. coqtop:: all + + Inductive Expr := + | One : Expr + | Mul : Expr -> Expr -> Expr + | Add : Expr -> Expr -> Expr. + + Declare Custom Entry expr. + Notation "[ e ]" := e (e custom expr at level 2). + Notation "1" := One (in custom expr at level 0). + Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity). + Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). + Notation "( x )" := x (in custom expr, x at level 2). + Notation "{ x }" := x (in custom expr, x constr). + Notation "x" := x (in custom expr at level 0, x ident). + + Axiom f : nat -> Expr. + Check fun x y z => [1 + y z + {f x}]. + Unset Printing Notations. + Check fun x y z => [1 + y z + {f x}]. + Set Printing Notations. + Check fun e => match e with + | [1 + 1] => [1] + | [x y + z] => [x + y z] + | y => [y + e] + end. + +Custom entries have levels, like the main grammar of terms and grammar +of patterns have. The lower level is 0 and this is the level used by +default to put rules delimited with tokens on both ends. The level is +left to be inferred by Coq when using :n:`in custom @ident``. The +level is otherwise given explicitly by using the syntax :n:`in custom +@ident at level @num`, where :n:`@num` refers to the level. + +Levels are cumulative: a notation at level ``n`` of which the left end +is a term shall use rules at level less than ``n`` to parse this +sub-term. More precisely, it shall use rules at level strictly less +than ``n`` if the rule is declared with ``right associativity`` and +rules at level less or equal than ``n`` if the rule is declared with +``left associativity``. Similarly, a notation at level ``n`` of which +the right end is a term shall use by default rules at level strictly +less than ``n`` to parse this sub-term if the rule is declared left +associative and rules at level less or equal than ``n`` if the rule is +declared right associative. This is what happens for instance in the +rule ``Notation "x + y" := (Add x y) (in custom expr at level 2, left +associativity)`` where ``x`` is any expression parsed in entry +``expr`` at level less or equal than ``2`` (including, recursively, +the given rule) and ``y`` is any expression parsed in entry ``expr`` +at level strictly less than ``2``. + +Rules associated to an entry can refer different sub-entries. The +grammar entry name ``constr`` can be used to refer to the main grammar +of term as in the rule ``Notation "{ x }" := x (in custom expr at +level 0, x constr)`` which indicates that the subterm ``x`` should be +parsed using the main grammar. If not indicated, the level is computed +as for notations in ``constr``, e.g. using 200 as default level for +inner sub-expressions. The level can otherwise be indicated explicitly +by using ``constr at level n`` for some ``n``, or ``constr at next +level``. + +Conversely, custom entries can be used to parse sub-expressions of the +main grammar, or from another custom entry as is the case in +:g:`Notation "[ e ]" := e (e custom expr at level 2)` to indicate that +``e`` has to be parsed at level ``2`` of the grammar associated to the +custom entry ``expr``. The level can be omitted, as in :g:`Notation "[ e +]" := e (e custom expr)`, in which case Coq tries to infer it. + +In the absence of an explicit entry for parsing or printing a +sub-expression of a notation in a custom entry, the default is to +consider that this sub-expression is parsed or printed in the same +custom entry where the notation is defined. In particular, if ``x at +level n`` is used for a sub-expression of a notation defined in custom +entry ``foo``, it shall be understood the same as ``x custom foo at +level n``. + +In general, rules are required to be *productive* on the right-hand +side, i.e. that they are bound to an expression which is not +reduced to a single variable. If the rule is not productive on the +right-hand side, as it is the case above for :g:`Notation "( x )" := x +(in custom expr at level 0, x at level 2)` and :g:`Notation "{ x }" := +x (in custom expr at level 0, x constr)`, it is used as a *grammar +coercion* which means that it is used to parse or print an expression +which is not available in the current grammar at the current level of +parsing or printing for this grammar but which is available in another +grammar or in another level of the current grammar. For instance, +:g:`Notation "( x )" := x (in custom expr at level 0, x at level 2)` +tells that parentheses can be inserted to parse or print an expression +declared at level ``2`` of ``expr`` whenever this expression is +expected to be used as a subterm at level 0 or 1. This allows for +instance to parse and print :g:`Add x y` as a subterm of :g:`Mul (Add +x y) z` using the syntax ``(x + y) z``. Similarly, :g:`Notation "{ x }" +:= x (in custom expr at level 0, x constr)` gives a way to let any +arbitrary expression which is not in handled by the custom entry +``expr`` be parsed or printed by the main grammar of term up to the +insertion of a pair of curly brackets. + +.. cmd:: Print Grammar @ident. + + This displays the state of the grammar for terms and grammar for + patterns associated to the custom entry :token:`ident`. + Summary ~~~~~~~ @@ -699,8 +810,8 @@ Summary Syntax of notations +++++++++++++++++++ -The different syntactic variants of the command Notation are given on the -following figure. The optional :production:`scope` is described in +The different syntactic forms taken by the commands declaring +notations are given below. The optional :production:`scope` is described in :ref:`Scopes`. .. productionlist:: coq @@ -711,22 +822,32 @@ following figure. The optional :production:`scope` is described in : | CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. : | Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. : | CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`]. + : | [Local] Declare Custom Entry `ident`. decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. - modifiers : at level `natural` - : | `ident` , … , `ident` at level `natural` [`binderinterp`] + modifiers : at level `num` + : in custom `ident` + : in custom `ident` at level `num` + : | `ident` , … , `ident` at level `num` [`binderinterp`] : | `ident` , … , `ident` at next level [`binderinterp`] - : | `ident` ident - : | `ident` global - : | `ident` bigint - : | `ident` [strict] pattern [at level `natural`] - : | `ident` binder - : | `ident` closed binder + : | `ident` `explicit_subentry` : | left associativity : | right associativity : | no associativity : | only parsing : | only printing : | format `string` + explicit_subentry : ident + : | global + : | bigint + : | [strict] pattern [at level `num`] + : | binder + : | closed binder + : | constr [`binderinterp`] + : | constr at level `num` [`binderinterp`] + : | constr at next level [`binderinterp`] + : | custom [`binderinterp`] + : | custom at level `num` [`binderinterp`] + : | custom at next level [`binderinterp`] binderinterp : as ident : | as pattern : | as strict pattern @@ -734,10 +855,11 @@ following figure. The optional :production:`scope` is described in .. note:: No typing of the denoted expression is performed at definition time. Type-checking is done only at the time of use of the notation. -.. note:: Many examples of Notation may be found in the files composing +.. note:: Some examples of Notation may be found in the files composing the initial state of Coq (see directory :file:`$COQLIB/theories/Init`). -.. note:: The notation ``"{ x }"`` has a special status in such a way that +.. note:: The notation ``"{ x }"`` has a special status in the main grammars of + terms and patterns so that complex notations of the form ``"x + { y }"`` or ``"x * { y }"`` can be nested with correct precedences. Especially, every notation involving a pattern of the form ``"{ x }"`` is parsed as a notation where the @@ -754,13 +876,18 @@ following figure. The optional :production:`scope` is described in Persistence of notations ++++++++++++++++++++++++ -Notations do not survive the end of sections. +Neither notations nor custom entries survive the end of sections. .. cmd:: Local Notation @notation Notations survive modules unless the command ``Local Notation`` is used instead of :cmd:`Notation`. +.. cmd:: Local Declare Custom Entry @ident + + Custom entries survive modules unless the command ``Local Declare + Custom Entry`` is used instead of :cmd:`Declare Custom Entry`. + .. _Scopes: Interpretation scopes @@ -1010,7 +1137,7 @@ The ``function_scope`` interpretation scope .. index:: function_scope -The scope ``function_scope`` also has a special status. +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 :g:`A -> B`. @@ -1025,11 +1152,11 @@ Scopes` or :cmd:`Print Scope`. ``type_scope`` This scope includes infix * for product types and infix + for sum types. It - is delimited by key ``type``, and bound to the coercion class + is delimited by key ``type``, and bound to the coercion class ``Sortclass``, as described above. ``function_scope`` - This scope is delimited by key ``function``, and bound to the coercion class + This scope is delimited by key ``function``, and bound to the coercion class ``Funclass``, as described above. ``nat_scope`` @@ -1207,7 +1334,7 @@ tactic language. Tactic notations obey the following syntax: .. productionlist:: coq tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. prod_item : `string` | `tactic_argument_type`(`ident`) - tactic_level : (at level `natural`) + tactic_level : (at level `num`) tactic_argument_type : ident | simple_intropattern | reference : | hyp | hyp_list | ne_hyp_list : | constr | uconstr | constr_list | ne_constr_list @@ -1328,7 +1455,9 @@ tactic language. Tactic notations obey the following syntax: .. [#and_or_levels] which are the levels effectively chosen in the current implementation of Coq -.. [#no_associativity] Coq accepts notations declared as ``no associative`` but the parser on - which Coq is built, namely Camlp4, currently does not implement the - ``no associativity`` and replaces it by a ``left associativity``; hence it is - the same for Coq: ``no associativity`` is in fact ``left associativity``. +.. [#no_associativity] Coq accepts notations declared as ``no + associativity`` but the parser on which Coq is built, namely + Camlp5, currently does not implement ``no associativity`` and + replaces it with ``left associativity``; hence it is the same for + Coq: ``no associativity`` is in fact ``left associativity``, for + the purposes of parsing diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index c9487abf03..e6b71a8293 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -571,6 +571,9 @@ class ExampleDirective(BaseAdmonition): http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition for more details. + Optionally, any text immediately following the ``.. example::`` header is + used as the example's title. + Example:: .. example:: Adding a hint to a database @@ -583,13 +586,14 @@ class ExampleDirective(BaseAdmonition): """ node_class = nodes.admonition directive_name = "example" + optional_arguments = 1 def run(self): # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’, # and uses arguments[0] as the title in that case (in other cases, the # title is unset, and it is instead set in the HTML visitor). - assert not self.arguments # Arguments have been parsed as content - self.arguments = ['Example'] + assert len(self.arguments) <= 1 + self.arguments = [": ".join(['Example'] + self.arguments)] self.options['classes'] = ['admonition', 'note'] return super().run() |