diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 163 |
5 files changed, 178 insertions, 51 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 6843e9eaa1..3af3115a59 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -6,14 +6,14 @@ Canonical Structures :Authors: Assia Mahboubi and Enrico Tassi -This chapter explains the basics of Canonical Structure and how they can be used +This chapter explains the basics of canonical structures and how they can be used to overload notations and build a hierarchy of algebraic structures. The examples are taken from :cite:`CSwcu`. We invite the interested reader to refer to this paper for all the details that are omitted here for brevity. The interested reader shall also find in :cite:`CSlessadhoc` a detailed description -of another, complementary, use of Canonical Structures: advanced proof search. +of another, complementary, use of canonical structures: advanced proof search. This latter papers also presents many techniques one can employ to tune the -inference of Canonical Structures. +inference of canonical structures. Notation overloading @@ -38,21 +38,21 @@ of the terms that are compared. End theory. End EQ. -We use Coq modules as name spaces. This allows us to follow the same +We use Coq modules as namespaces. This allows us to follow the same pattern and naming convention for the rest of the chapter. The base -name space contains the definitions of the algebraic structure. To +namespace contains the definitions of the algebraic structure. To keep the example small, the algebraic structure ``EQ.type`` we are defining is very simplistic, and characterizes terms on which a binary relation is defined, without requiring such relation to validate any property. The inner theory module contains the overloaded notation ``==`` -and will eventually contain lemmas holding on all the instances of the +and will eventually contain lemmas holding all the instances of the algebraic structure (in this case there are no lemmas). Note that in practice the user may want to declare ``EQ.obj`` as a coercion, but we will not do that here. The following line tests that, when we assume a type ``e`` that is in -theEQ class, then we can relates two of its objects with ``==``. +theEQ class, we can relate two of its objects with ``==``. .. coqtop:: all @@ -312,7 +312,7 @@ The following script registers an ``LEQ`` class for ``nat`` and for the type constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following -subsection we show how to make these declaration more compact. +subsection we show how to make them more compact. .. coqtop:: all @@ -385,7 +385,7 @@ with message "T is not an EQ.type"”. The other utilities are used to ask |Coq| to solve a specific unification problem, that will in turn require the inference of some canonical structures. -They are explained in mode details in :cite:`CSwcu`. +They are explained in more details in :cite:`CSwcu`. We now have all we need to create a compact “packager” to declare instances of the ``LEQ`` class. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 09faa06765..f134022eb6 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -31,7 +31,7 @@ A class with `n` parameters is any defined name with a type :g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort. Thus a class with parameters is considered as a single class and not as a family of classes. An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`. -In addition to these user-classes, we have two abstract classes: +In addition to these user-defined classes, we have two built-in classes: * ``Sortclass``, the class of sorts; its objects are the terms whose type is a @@ -50,11 +50,11 @@ Formally, the syntax of a classes is defined as: Coercions --------- -A name ``f`` can be declared as a coercion between a source user-class +A name ``f`` can be declared as a coercion between a source user-defined class ``C`` with `n` parameters and a target class ``D`` if one of these conditions holds: - * ``D`` is a user-class, then the type of ``f`` must have the form + * ``D`` is a user-defined class, then the type of ``f`` must have the form :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `m` is the number of parameters of ``D``. * ``D`` is ``Funclass``, then the type of ``f`` must have the form @@ -65,8 +65,8 @@ conditions holds: We then write :g:`f : C >-> D`. The restriction on the type of coercions is called *the uniform inheritance condition*. -.. note:: The abstract class ``Sortclass`` can be used as a source class, but - the abstract class ``Funclass`` cannot. +.. note:: The built-in class ``Sortclass`` can be used as a source class, but + the built-in class ``Funclass`` cannot. To coerce an object :g:`t:C t₁..tₙ` of ``C`` towards ``D``, we have to apply the coercion ``f`` to it; the obtained term :g:`f t₁..tₙ t` is @@ -95,7 +95,7 @@ We can now declare ``f`` as coercion from ``C'`` to ``D``, since we can The identity coercions have a special status: to coerce an object :g:`t:C' t₁..tₖ` -of ``C'`` towards ``C``, we does not have to insert explicitly ``Id_C'_C`` +of ``C'`` towards ``C``, we do not have to insert explicitly ``Id_C'_C`` since :g:`Id_C'_C t₁..tₖ t` is convertible with ``t``. However we "rewrite" the type of ``t`` to become an object of ``C``; in this case, it becomes :g:`C uₙ'..uₖ'` where each ``uᵢ'`` is the result of the @@ -121,7 +121,7 @@ by the coercions ``f₁..fₖ``. The application of a coercion path to a term consists of the successive application of its coercions. -Declaration of Coercions +Declaring Coercions ------------------------- .. cmd:: Coercion @qualid : @class >-> @class @@ -140,8 +140,8 @@ Declaration of Coercions .. warn:: Ambiguous path. - When the coercion :token:`qualid` is added to the inheritance graph, non - valid coercion paths are ignored; they are signaled by a warning + When the coercion :token:`qualid` is added to the inheritance graph, + invalid coercion paths are ignored; they are signaled by a warning displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. .. cmdv:: Local Coercion @qualid : @class >-> @class @@ -215,7 +215,7 @@ declaration, this constructor is declared as a coercion. .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident - Idem but locally to the current section. + Same as ``Identity Coercion`` but locally to the current section. .. cmdv:: SubClass @ident := @type :name: SubClass @@ -319,7 +319,7 @@ Coercions and Modules Since |Coq| version 8.3, the coercions present in a module are activated only when the module is explicitly imported. Formerly, the coercions - were activated as soon as the module was required, whatever it was + were activated as soon as the module was required, whether it was imported or not. This option makes it possible to recover the behavior of the versions of @@ -387,8 +387,8 @@ We give now an example using identity coercions. In the case of functional arguments, we use the monotonic rule of -sub-typing. Approximatively, to coerce :g:`t:forall x:A,B` towards -:g:`forall x:A',B'`, one have to coerce ``A'`` towards ``A`` and ``B`` +sub-typing. To coerce :g:`t : forall x : A, B` towards +:g:`forall x : A', B'`, we have to coerce ``A'`` towards ``A`` and ``B`` towards ``B'``. An example is given below: .. coqtop:: all @@ -424,8 +424,8 @@ replaced by ``x:A'`` where ``A'`` is the result of the application to ``Sortclass`` if it exists. This case occurs in the abstraction :g:`fun x:A => t`, universal quantification :g:`forall x:A,B`, global variables and parameters of (co-)inductive definitions and -functions. In :g:`forall x:A,B`, such a coercion path may be applied -to ``B`` also if necessary. +functions. In :g:`forall x:A,B`, such a coercion path may also be applied +to ``B`` if necessary. .. coqtop:: all diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index bdaa2aa1a2..e15bcb8e2c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -546,12 +546,12 @@ The printing for one token can be removed with Initially, the pretty-printing table contains the following mapping: -==== === ==== ===== === ==== ==== === -`->` → `<-` ← `*` × -`<=` ≤ `>=` ≥ `=>` ⇒ -`<>` ≠ `<->` ↔ `|-` ⊢ -`\/` ∨ `/\\` ∧ `~` ¬ -==== === ==== ===== === ==== ==== === +===== === ==== ===== === ==== ==== === +`->` → `<-` ← `*` × +`<=` ≤ `>=` ≥ `=>` ⇒ +`<>` ≠ `<->` ↔ `|-` ⊢ +`\\/` ∨ `/\\` ∧ `~` ¬ +===== === ==== ===== === ==== ==== === Any of these can be overwritten or suppressed using the printing commands. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 9b4d724e02..e6bc84365c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -281,7 +281,7 @@ Applying theorems :g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n`. - .. exn:: Unable to unify ... with ... . + .. exn:: Unable to unify @term with @term. The apply tactic failed to match the conclusion of :token:`term` and the current goal. You can help the apply tactic by transforming your goal with @@ -3935,7 +3935,7 @@ match against it. discriminable equality but this proof could not be built in Coq because of dependently-typed functions. -.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with ..., replacing metavariables by arbitrary terms. +.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. The decision procedure could solve the goal with the provision that additional arguments are supplied for some partially applied constructors. Any term of an @@ -3979,7 +3979,7 @@ succeeds, and results in an error otherwise. This tactic checks whether its arguments are unifiable, potentially instantiating existential variables. -.. exn:: Not unifiable. +.. exn:: Unable to unify @term with @term. .. tacv:: unify @term @term with @ident diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dcefa293b1..6e98da1c04 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: @@ -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 @@ -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 |