diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 535 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 2 |
3 files changed, 277 insertions, 264 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 85474a3e98..10650af1d1 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -97,8 +97,8 @@ Logic The basic library of |Coq| comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the -subclass `form` of the syntactic class `term`. The syntax of `form` -is shown below: +subclass :token:`form` of the syntactic class :token:`term`. The syntax of +:token:`form` is shown below: .. /!\ Please keep the blanks in the lines below, experimentally they produce a nice last column. Or even better, find a proper way to do this! diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 9dae7fd102..376a6b8eed 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -27,46 +27,45 @@ expressions. In this sense, the :cmd:`Record` construction allows defining field : `ident` [ `binders` ] : `type` [ where `notation` ] : | `ident` [ `binders` ] [: `type` ] := `term` -In the expression: - .. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } } -the first identifier :token:`ident` is the name of the defined record and :token:`sort` is its -type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, -the default name ``Build_``\ :token:`ident`, where :token:`ident` is the record name, is used. If :token:`sort` is -omitted, the default sort is `\Type`. The identifiers inside the brackets are the names of -fields. For a given field :token:`ident`, its type is :g:`forall binders, type`. -Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the -order of the fields is important. Finally, :token:`binders` are parameters of the record. + The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its + type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, + the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is + omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of + fields. For a given field :token:`ident`, its type is :n:`forall @binders, @type`. + Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the + order of the fields is important. Finally, :token:`binders` are parameters of the record. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: -:n:`Record @ident @binders : @sort := { @ident₁ : @type₁ ; @ident₂ := @term₂ ; @ident₃ : @type₃ }`. -in which case the correctness of :n:`@type₃` may rely on the instance :n:`@term₂` of :n:`@ident₂` and :n:`@term₂` may in turn depend on :n:`@ident₁`. +:n:`Record @ident @binders : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`. +in which case the correctness of :n:`@type__3` may rely on the instance :n:`@term__2` of :n:`@ident__2` and :n:`@term__2` may in turn depend on :n:`@ident__1`. .. example:: The set of rational numbers may be defined as: - .. coqtop:: reset all + .. coqtop:: reset all - Record Rat : Set := mkRat - {sign : bool; - top : nat; - bottom : nat; - Rat_bottom_cond : 0 <> bottom; - Rat_irred_cond : - forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}. + Record Rat : Set := mkRat + { sign : bool + ; top : nat + ; bottom : nat + ; Rat_bottom_cond : 0 <> bottom + ; Rat_irred_cond : + forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1 + }. -Remark here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` and ``Rat_irred_cond`` -depends on both ``top`` and ``bottom``. + Note here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` + and ``Rat_irred_cond`` depends on both ``top`` and ``bottom``. Let us now see the work done by the ``Record`` macro. First the macro generates a variant type definition with just one constructor: -:n:`Variant @ident {? @binders } : @sort := @ident₀ {? @binders }`. +:n:`Variant @ident {? @binders } : @sort := @ident__0 {? @binders }`. -To build an object of type :n:`@ident`, one should provide the constructor -:n:`@ident₀` with the appropriate number of terms filling the fields of the record. +To build an object of type :token:`ident`, one should provide the constructor +:n:`@ident__0` with the appropriate number of terms filling the fields of the record. .. example:: @@ -131,7 +130,7 @@ This syntax can also be used for pattern matching. end). The macro generates also, when it is possible, the projection -functions for destructuring an object of type `\ident`. These +functions for destructuring an object of type :token:`ident`. These projection functions are given the names of the corresponding fields. If a field is named `_` then no projection is built for it. In our example: @@ -149,33 +148,33 @@ available: Eval compute in half.(top). -It can be activated for printing with - .. flag:: Printing Projections -.. example:: + This flag activates the dot notation for printing. - .. coqtop:: all + .. example:: + + .. coqtop:: all - Set Printing Projections. - Check top half. + Set Printing Projections. + Check top half. .. FIXME: move this to the main grammar in the spec chapter .. _record_projections_grammar: .. productionlist:: terms - projection : projection `.` ( `qualid` ) - : | projection `.` ( `qualid` `arg` … `arg` ) - : | projection `.` ( @`qualid` `term` … `term` ) + projection : `term` `.` ( `qualid` ) + : | `term` `.` ( `qualid` `arg` … `arg` ) + : | `term` `.` ( @`qualid` `term` … `term` ) Syntax of Record projections -The corresponding grammar rules are given in the preceding grammar. When `qualid` -denotes a projection, the syntax `term.(qualid)` is equivalent to `qualid term`, -the syntax `term.(qualid` |arg_1| |arg_n| `)` to `qualid` |arg_1| `…` |arg_n| `term`, -and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` |term_n| `term`. -In each case, `term` is the object projected and the +The corresponding grammar rules are given in the preceding grammar. When :token:`qualid` +denotes a projection, the syntax :n:`@term.(@qualid)` is equivalent to :n:`@qualid @term`, +the syntax :n:`@term.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term`. +and the syntax :n:`@term.(@@qualid {+ @term })` to :n:`@@qualid {+ @term } @term`. +In each case, :token:`term` is the object projected and the other arguments are the parameters of the inductive type. @@ -199,22 +198,22 @@ other arguments are the parameters of the inductive type. This message is followed by an explanation of this impossibility. There may be three reasons: - #. The name `ident` already exists in the environment (see :cmd:`Axiom`). - #. The body of `ident` uses an incorrect elimination for - `ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). - #. The type of the projections `ident` depends on previous + #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`). + #. The body of :token:`ident` uses an incorrect elimination for + :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). + #. The type of the projections :token:`ident` depends on previous projections which themselves could not be defined. .. exn:: Records declared with the keyword Record or Structure cannot be recursive. - The record name `ident` appears in the type of its fields, but uses - the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. + The record name :token:`ident` appears in the type of its fields, but uses + the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. .. exn:: Cannot handle mutually (co)inductive records. - Records cannot be defined as part of mutually inductive (or - co-inductive) definitions, whether with records only or mixed with - standard definitions. + Records cannot be defined as part of mutually inductive (or + co-inductive) definitions, whether with records only or mixed with + standard definitions. During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in Section @@ -310,7 +309,7 @@ an object of the record type as arguments, and whose body is an application of the unfolded primitive projection of the same name. These constants are used when elaborating partial applications of the projection. One can distinguish them from applications of the primitive -projection if the :flag`Printing Primitive Projection Parameters` option +projection if the :flag:`Printing Primitive Projection Parameters` option is off: For a primitive projection application, parameters are printed as underscores while for the compatibility projections they are printed as usual. @@ -382,7 +381,7 @@ we have the following equivalence | right _ => false end). -Notice that the printing uses the :g:`if` syntax because `sumbool` is +Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is declared as such (see :ref:`controlling-match-pp`). .. _irrefutable-patterns: @@ -601,17 +600,17 @@ The following experimental command is available when the ``FunInd`` library has .. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term -This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper -for several ways of defining a function *and other useful related -objects*, namely: an induction principle that reflects the recursive -structure of the function (see :tacn:`function induction`) and its fixpoint equality. -The meaning of this declaration is to define a function ident, -similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must -be given (unless the function is not recursive), but it might not -necessarily be *structurally* decreasing. The point of the {} annotation -is to name the decreasing argument *and* to describe which kind of -decreasing criteria must be used to ensure termination of recursive -calls. + This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper + for several ways of defining a function *and other useful related + objects*, namely: an induction principle that reflects the recursive + structure of the function (see :tacn:`function induction`) and its fixpoint equality. + The meaning of this declaration is to define a function ident, + similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must + be given (unless the function is not recursive), but it might not + necessarily be *structurally* decreasing. The point of the {} annotation + is to name the decreasing argument *and* to describe which kind of + decreasing criteria must be used to ensure termination of recursive + calls. The ``Function`` construction also enjoys the ``with`` extension to define mutually recursive definitions. However, this feature does not work @@ -655,8 +654,7 @@ with applications only *at the end* of each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the -presence of partial application of `wrong` in the body of -`wrong` : +presence of partial application of :g:`wrong` in the body of :g:`wrong`: .. coqtop:: all @@ -667,27 +665,32 @@ For now, dependent cases are not treated for non structurally terminating functions. .. exn:: The recursive argument must be specified. + :undocumented: + .. exn:: No argument name @ident. + :undocumented: + .. exn:: Cannot use mutual definition with well-founded recursion or measure. + :undocumented: .. warn:: Cannot define graph for @ident. - The generation of the graph relation (`R_ident`) used to compute the induction scheme of ident - raised a typing error. Only `ident` is defined; the induction scheme - will not be generated. This error happens generally when: + The generation of the graph relation (:n:`R_@ident`) used to compute the induction scheme of ident + raised a typing error. Only :token:`ident` is defined; the induction scheme + will not be generated. This error happens generally when: - - the definition uses pattern matching on dependent types, - which ``Function`` cannot deal with yet. - - the definition is not a *pattern matching tree* as explained above. + - the definition uses pattern matching on dependent types, + which ``Function`` cannot deal with yet. + - the definition is not a *pattern matching tree* as explained above. .. warn:: Cannot define principle(s) for @ident. - The generation of the graph relation (`R_ident`) succeeded but the induction principle - could not be built. Only `ident` is defined. Please report. + The generation of the graph relation (:n:`R_@ident`) succeeded but the induction principle + could not be built. Only :token:`ident` is defined. Please report. .. warn:: Cannot build functional inversion principle. - `functional inversion` will not be available for the function. + :tacn:`functional inversion` will not be available for the function. .. seealso:: :ref:`functional-scheme` and :tacn:`function induction` @@ -696,39 +699,40 @@ used by ``Function``. A more precise description is given below. .. cmdv:: Function @ident {* @binder } : @type := @term - Defines the not recursive function `ident` as if declared with `Definition`. Moreover - the following are defined: + Defines the not recursive function :token:`ident` as if declared with + :cmd:`Definition`. Moreover the following are defined: - + `ident_rect`, `ident_rec` and `ident_ind`, which reflect the pattern - matching structure of `term` (see :cmd:`Inductive`); - + The inductive `R_ident` corresponding to the graph of `ident` (silently); - + `ident_complete` and `ident_correct` which are inversion information - linking the function and its graph. + + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, + which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); + + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); + + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which + are inversion information linking the function and its graph. .. cmdv:: Function @ident {* @binder } { struct @ident } : @type := @term - Defines the structural recursive function `ident` as if declared with ``Fixpoint``. Moreover the following are defined: + Defines the structural recursive function :token:`ident` as if declared + with :cmd:`Fixpoint`. Moreover the following are defined: + The same objects as above; - + The fixpoint equation of `ident`: `ident_equation`. + + The fixpoint equation of :token:`ident`: :n:`@ident_equation`. .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term -.. cmdv:: Function @ident {* @binder } { wf @term @ident } : @type := @term + Function @ident {* @binder } { wf @term @ident } : @type := @term Defines a recursive function by well-founded recursion. The module ``Recdef`` of the standard library must be loaded for this feature. The ``{}`` annotation is mandatory and must be one of the following: - + ``{measure`` `term` `ident` ``}`` with `ident` being the decreasing argument - and `term` being a function from type of `ident` to ``nat`` for which - value on the decreasing argument decreases (for the ``lt`` order on ``nat``) - at each recursive call of `term`. Parameters of the function are - bound in `term`\ ; - + ``{wf`` `term` `ident` ``}`` with `ident` being the decreasing argument and - `term` an ordering relation on the type of `ident` (i.e. of type + + :n:`{measure @term @ident }` with :token:`ident` being the decreasing argument + and :token:`term` being a function from type of :token:`ident` to :g:`nat` for which + value on the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) + at each recursive call of :token:`term`. Parameters of the function are + bound in :token:`term`; + + :n:`{wf @term @ident }` with :token:`ident` being the decreasing argument and + :token:`term` an ordering relation on the type of :token:`ident` (i.e. of type `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument - decreases at each recursive call of `term`. The order must be well-founded. - Parameters of the function are bound in `term`. + decreases at each recursive call of :token:`term`. The order must be well-founded. + Parameters of the function are bound in :token:`term`. Depending on the annotation, the user is left with some proof obligations that will be used to define the function. These proofs @@ -767,42 +771,42 @@ Section :ref:`gallina-definitions`). .. cmd:: End @ident - This command closes the section named `ident`. After closing of the - section, the local declarations (variables and local definitions) get - *discharged*, meaning that they stop being visible and that all global - objects defined in the section are generalized with respect to the - variables and local definitions they each depended on in the section. - - .. example:: + This command closes the section named :token:`ident`. After closing of the + section, the local declarations (variables and local definitions) get + *discharged*, meaning that they stop being visible and that all global + objects defined in the section are generalized with respect to the + variables and local definitions they each depended on in the section. - .. coqtop:: all + .. example:: - Section s1. + .. coqtop:: all - Variables x y : nat. + Section s1. - Let y' := y. + Variables x y : nat. - Definition x' := S x. + Let y' := y. - Definition x'' := x' + y'. + Definition x' := S x. - Print x'. + Definition x'' := x' + y'. - End s1. + Print x'. - Print x'. + End s1. - Print x''. + Print x'. - Notice the difference between the value of `x’` and `x’’` inside section - `s1` and outside. + Print x''. - .. exn:: This is not the last opened section. + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. -**Remarks:** + .. exn:: This is not the last opened section. + :undocumented: -#. Most commands, like ``Hint``, ``Notation``, option management, … which +.. note:: + Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which appear inside a section are canceled when the section is closed. @@ -813,26 +817,26 @@ The module system provides a way of packaging related elements together, as well as a means of massive abstraction. .. productionlist:: modules - module_type : qualid - : | `module_type` with Definition qualid := term - : | `module_type` with Module qualid := qualid - : | qualid qualid … qualid - : | !qualid qualid … qualid - module_binding : ( [Import|Export] ident … ident : module_type ) + module_type : `qualid` + : | `module_type` with Definition `qualid` := `term` + : | `module_type` with Module `qualid` := `qualid` + : | `qualid` `qualid` … `qualid` + : | !`qualid` `qualid` … `qualid` + module_binding : ( [Import|Export] `ident` … `ident` : `module_type` ) module_bindings : `module_binding` … `module_binding` - module_expression : qualid … qualid - : | !qualid … qualid + module_expression : `qualid` … `qualid` + : | !`qualid` … `qualid` Syntax of modules In the syntax of module application, the ! prefix indicates that any `Inline` directive in the type of the functor arguments will be ignored -(see the ``Module Type`` command below). +(see the :cmd:`Module Type` command below). .. cmd:: Module @ident - This command is used to start an interactive module named `ident`. + This command is used to start an interactive module named :token:`ident`. .. cmdv:: Module @ident {* @module_binding} @@ -845,21 +849,22 @@ In the syntax of module application, the ! prefix indicates that any .. cmdv:: Module @ident {* @module_binding} : @module_type - Starts an interactive functor with parameters given by the list of `module binding`, and output module - type `module_type`. + Starts an interactive functor with parameters given by the list of + :token:`module_bindings`, and output module type :token:`module_type`. .. cmdv:: Module @ident <: {+<: @module_type } - Starts an interactive module satisfying each `module_type`. + Starts an interactive module satisfying each :token:`module_type`. .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }. - Starts an interactive functor with parameters given by the list of `module_binding`. The output module type - is verified against each `module_type`. + Starts an interactive functor with parameters given by the list of + :token:`module_binding`. The output module type + is verified against each :token:`module_type`. .. cmdv:: Module [ Import | Export ] - Behaves like ``Module``, but automatically imports or exports the module. + Behaves like :cmd:`Module`, but automatically imports or exports the module. Reserved commands inside an interactive module ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -874,52 +879,55 @@ Reserved commands inside an interactive module .. cmd:: Include {+<+ @module} - is a shortcut for the commands ``Include`` `module` for each `module`. + is a shortcut for the commands :n:`Include @module` for each :token:`module`. .. cmd:: End @ident - This command closes the interactive module `ident`. If the module type + This command closes the interactive module :token:`ident`. If the module type was given the content of the module is matched against it and an error is signaled if the matching fails. If the module is basic (is not a functor) its components (constants, inductive types, submodules etc.) are now available through the dot notation. .. exn:: No such label @ident. + :undocumented: .. exn:: Signature components for label @ident do not match. + :undocumented: .. exn:: This is not the last opened module. + :undocumented: .. cmd:: Module @ident := @module_expression - This command defines the module identifier `ident` to be equal - to `module_expression`. + This command defines the module identifier :token:`ident` to be equal + to :token:`module_expression`. .. cmdv:: Module @ident {* @module_binding} := @module_expression - Defines a functor with parameters given by the list of `module_binding` and body `module_expression`. + Defines a functor with parameters given by the list of :token:`module_binding` and body :token:`module_expression`. .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression - Defines a functor with parameters given by the list of `module_binding` (possibly none), and output module type `module_type`, - with body `module_expression`. + Defines a functor with parameters given by the list of :token:`module_binding` (possibly none), and output module type :token:`module_type`, + with body :token:`module_expression`. .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression - Defines a functor with parameters given by module_bindings (possibly none) with body `module_expression`. - The body is checked against each |module_type_i|. + Defines a functor with parameters given by module_bindings (possibly none) with body :token:`module_expression`. + The body is checked against each :n:`@module_type__i`. .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression} - is equivalent to an interactive module where each `module_expression` is included. + is equivalent to an interactive module where each :token:`module_expression` is included. .. cmd:: Module Type @ident -This command is used to start an interactive module type `ident`. + This command is used to start an interactive module type :token:`ident`. - .. cmdv:: Module Type @ident {* @module_binding} + .. cmdv:: Module Type @ident {* @module_binding} - Starts an interactive functor type with parameters given by `module_bindings`. + Starts an interactive functor type with parameters given by :token:`module_bindings`. Reserved commands inside an interactive module type: @@ -931,7 +939,7 @@ Reserved commands inside an interactive module type: .. cmd:: Include {+<+ @module} - is a shortcut for the command ``Include`` `module` for each `module`. + This is a shortcut for the command :n:`Include @module` for each :token:`module`. .. cmd:: @assumption_keyword Inline @assums :name: Inline @@ -941,31 +949,32 @@ Reserved commands inside an interactive module type: .. cmd:: End @ident - This command closes the interactive module type `ident`. + This command closes the interactive module type :token:`ident`. .. exn:: This is not the last opened module type. + :undocumented: .. cmd:: Module Type @ident := @module_type - Defines a module type `ident` equal to `module_type`. + Defines a module type :token:`ident` equal to :token:`module_type`. .. cmdv:: Module Type @ident {* @module_binding} := @module_type - Defines a functor type `ident` specifying functors taking arguments `module_bindings` and - returning `module_type`. + Defines a functor type :token:`ident` specifying functors taking arguments :token:`module_bindings` and + returning :token:`module_type`. .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type } - is equivalent to an interactive module type were each `module_type` is included. + is equivalent to an interactive module type were each :token:`module_type` is included. .. cmd:: Declare Module @ident : @module_type - Declares a module `ident` of type `module_type`. + Declares a module :token:`ident` of type :token:`module_type`. .. cmdv:: Declare Module @ident {* @module_binding} : @module_type - Declares a functor with parameters given by the list of `module_binding` and output module type - `module_type`. + Declares a functor with parameters given by the list of :token:`module_binding` and output module type + :token:`module_type`. .. example:: @@ -1045,8 +1054,8 @@ specification: the y component is dropped as well as the body of x. End SIG. -The definition of ``N`` using the module type expression ``SIG`` with -``Definition T := nat`` is equivalent to the following one: +The definition of :g:`N` using the module type expression :g:`SIG` with +:g:`Definition T := nat` is equivalent to the following one: .. coqtop:: all @@ -1131,7 +1140,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified. #. Modules and module types can be nested components of each other. #. One can have sections inside a module or a module type, but not a module or a module type inside a section. - #. Commands like ``Hint`` or ``Notation`` can also appear inside modules and + #. Commands like :cmd:`Hint` or :cmd:`Notation` can also appear inside modules and module types. Note that in case of a module definition like: :: @@ -1150,71 +1159,73 @@ component is equal ``nat`` and hence ``M1.T`` as specified. .. cmd:: Import @qualid - If `qualid` denotes a valid basic module (i.e. its module type is a - signature), makes its components available by their short names. + If :token:`qualid` denotes a valid basic module (i.e. its module type is a + signature), makes its components available by their short names. - .. example:: + .. example:: - .. coqtop:: reset all + .. coqtop:: reset all - Module Mod. + Module Mod. - Definition T:=nat. + Definition T:=nat. - Check T. + Check T. - End Mod. + End Mod. - Check Mod.T. + Check Mod.T. - Fail Check T. + Fail Check T. - Import Mod. + Import Mod. - Check T. + Check T. - Some features defined in modules are activated only when a module is - imported. This is for instance the case of notations (see :ref:`Notations`). + Some features defined in modules are activated only when a module is + imported. This is for instance the case of notations (see :ref:`Notations`). - Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` - command. Such declarations are only accessible through their fully - qualified name. + Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` + command. Such declarations are only accessible through their fully + qualified name. - .. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Module A. + Module A. - Module B. + Module B. - Local Definition T := nat. + Local Definition T := nat. - End B. + End B. - End A. + End A. - Import A. + Import A. - Fail Check B.T. + Fail Check B.T. - .. cmdv:: Export @qualid - :name: Export + .. cmdv:: Export @qualid + :name: Export - When the module containing the command Export qualid - is imported, qualid is imported as well. + When the module containing the command ``Export`` qualid + is imported, qualid is imported as well. - .. exn:: @qualid is not a module. + .. exn:: @qualid is not a module. + :undocumented: - .. warn:: Trying to mask the absolute name @qualid! + .. warn:: Trying to mask the absolute name @qualid! + :undocumented: .. cmd:: Print Module @ident - Prints the module type and (optionally) the body of the module :n:`@ident`. + Prints the module type and (optionally) the body of the module :token:`ident`. .. cmd:: Print Module Type @ident - Prints the module type corresponding to :n:`@ident`. + Prints the module type corresponding to :token:`ident`. .. flag:: Short Module Printing @@ -1365,7 +1376,7 @@ OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object files as described above. The OCaml loadpath is managed using the option ``-I`` `path` (in the OCaml world, there is neither a notion of logical name prefix nor a way to access files in -subdirectories of path). See the command ``Declare`` ``ML`` ``Module`` in +subdirectories of path). See the command :cmd:`Declare ML Module` in :ref:`compiled-files` to understand the need of the OCaml loadpath. See :ref:`command-line-options` for a more general view over the |Coq| command @@ -1566,38 +1577,39 @@ usual implicit arguments disambiguation syntax. Declaring Implicit Arguments ++++++++++++++++++++++++++++ -To set implicit arguments *a posteriori*, one can use the command: -.. cmd:: Arguments @qualid {* @possibly_bracketed_ident } - :name: Arguments (implicits) -where the list of `possibly_bracketed_ident` is a prefix of the list of -arguments of `qualid` where the ones to be declared implicit are -surrounded by square brackets and the ones to be declared as maximally -inserted implicits are surrounded by curly braces. +.. cmd:: Arguments @qualid {* [ @ident ] | @ident } + :name: Arguments (implicits) -After the above declaration is issued, implicit arguments can just -(and have to) be skipped in any expression involving an application -of `qualid`. + This command is used to set implicit arguments *a posteriori*, + where the list of possibly bracketed :token:`ident` is a prefix of the list of + arguments of :token:`qualid` where the ones to be declared implicit are + surrounded by square brackets and the ones to be declared as maximally + inserted implicits are surrounded by curly braces. -Implicit arguments can be cleared with the following syntax: + After the above declaration is issued, implicit arguments can just + (and have to) be skipped in any expression involving an application + of :token:`qualid`. .. cmd:: Arguments @qualid : clear implicits -.. cmdv:: Global Arguments @qualid {* @possibly_bracketed_ident } + This command clears implicit arguments. + +.. cmdv:: Global Arguments @qualid {* [ @ident ] | @ident } - Says to recompute the implicit arguments of - `qualid` after ending of the current section if any, enforcing the + 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 {* @possibly_bracketed_ident } +.. cmdv:: Local Arguments @qualid {* [ @ident ] | @ident } When in a module, tell not to activate the - implicit arguments ofqualid declared by this command to contexts that + implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } } +.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | @ident } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -1639,33 +1651,34 @@ Implicit arguments can be cleared with the following syntax: Check (fun l => map length l = map (list nat) nat length l). -Remark: To know which are the implicit arguments of an object, use the -command ``Print Implicit`` (see :ref:`displaying-implicit-args`). +.. note:: + To know which are the implicit arguments of an object, use the + command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| can also automatically detect what are the implicit arguments of a -defined object. The command is just - .. cmd:: Arguments @qualid : default implicits -The auto-detection is governed by options telling if strict, -contextual, or reversible-pattern implicit arguments must be -considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`, -:ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`). + This command tells |Coq| to automatically detect what are the implicit arguments of a + defined object. + + The auto-detection is governed by options telling if strict, + contextual, or reversible-pattern implicit arguments must be + considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`, + :ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`). -.. cmdv:: Global Arguments @qualid : default implicits + .. cmdv:: Global Arguments @qualid : default implicits - Tell to recompute the - implicit arguments of qualid after ending of the current section if - any. + Tell to recompute the + implicit arguments of qualid after ending of the current section if + any. -.. cmdv:: Local Arguments @qualid : default implicits + .. cmdv:: Local Arguments @qualid : default implicits - When in a module, tell not to activate the implicit arguments of `qualid` computed by this - declaration to contexts that requires the module. + When in a module, tell not to activate the implicit arguments of :token:`qualid` computed by this + declaration to contexts that requires the module. .. example:: @@ -1791,20 +1804,20 @@ Explicit applications In presence of non-strict or contextual argument, or in presence of partial applications, the synthesis of implicit arguments may fail, so one may have to give explicitly certain implicit arguments of an -application. The syntax for this is ``(`` `ident` ``:=`` `term` ``)`` where `ident` is the +application. The syntax for this is :n:`(@ident := @term)` where :token:`ident` is the name of the implicit argument and term is its corresponding explicit term. Alternatively, one can locally deactivate the hiding of implicit -arguments of a function by using the notation `@qualid` |term_1| … |term_n|. +arguments of a function by using the notation :n:`@qualid {+ @term }`. This syntax extension is given in the following grammar: .. _explicit_app_grammar: .. productionlist:: explicit_apps - term : @ qualid term … `term` - : | @ qualid - : | qualid `argument` … `argument` + term : @ `qualid` `term` … `term` + : | @ `qualid` + : | `qualid` `argument` … `argument` argument : `term` - : | (ident := `term`) + : | (`ident` := `term`) Syntax for explicitly giving implicit arguments @@ -1820,10 +1833,10 @@ This syntax extension is given in the following grammar: Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Implicit arguments names can be redefined using the following syntax: - .. cmd:: Arguments @qualid {* @name} : @rename + This command is used to redefine the names of implicit arguments. + With the assert flag, ``Arguments`` can be used to assert that a given object has the expected number of arguments and that these arguments are named as expected. @@ -1845,11 +1858,12 @@ are named as expected. Displaying what the implicit arguments are ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -To display the implicit arguments associated to an object, and to know -if each of them is to be used maximally or not, use the command - .. cmd:: Print Implicit @qualid + Use this command to display the implicit arguments associated to an object, + and to know if each of them is to be used maximally or not. + + Explicit displaying of implicit arguments for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1984,16 +1998,16 @@ Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ It is possible to bind variable names to a given type (e.g. in a -development using arithmetic, it may be convenient to bind the names `n` -or `m` to the type ``nat`` of natural numbers). The command for that is +development using arithmetic, it may be convenient to bind the names :g:`n` +or :g:`m` to the type :g:`nat` of natural numbers). .. cmd:: Implicit Types {+ @ident } : @type -The effect of the command is to automatically set the type of bound -variables starting with `ident` (either `ident` itself or `ident` followed by -one or more single quotes, underscore or digits) to be `type` (unless -the bound variable is already declared with an explicit type in which -case, this latter type is considered). + The effect of the command is to automatically set the type of bound + variables starting with :token:`ident` (either :token:`ident` itself or + :token:`ident` followed by one or more single quotes, underscore or + digits) to be :token:`type` (unless the bound variable is already declared + with an explicit type in which case, this latter type is considered). .. example:: @@ -2137,23 +2151,29 @@ Printing universes terms apparently identical but internally different in the Calculus of Inductive Constructions. -The constraints on the internal level of the occurrences of Type -(see :ref:`Sorts`) can be printed using the command - .. cmd:: Print {? Sorted} Universes :name: Print Universes -If the optional ``Sorted`` option is given, each universe will be made -equivalent to a numbered label reflecting its level (with a linear -ordering) in the universe hierarchy. + This command can be used to print the constraints on the internal level + of the occurrences of :math:`\Type` (see :ref:`Sorts`). + + If the optional ``Sorted`` option is given, each universe will be made + equivalent to a numbered label reflecting its level (with a linear + ordering) in the universe hierarchy. + + .. cmdv:: Print {? Sorted} Universes @string -This command also accepts an optional output filename: + This variant accepts an optional output filename. -.. cmdv:: Print {? Sorted} Universes @string + If :token:`string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT + language, and can be processed by Graphviz tools. The format is + unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. -If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT -language, and can be processed by Graphviz tools. The format is -unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. +.. cmdv:: Print Universes Subgraph(@names) + + Prints the graph restricted to the requested names (adjusting + constraints to preserve the implied transitive constraints between + kept universes). .. _existential-variables: @@ -2189,13 +2209,10 @@ existential variable is represented by “?” followed by an identifier. Check identity _ (fun x => _). -In the general case, when an existential variable ``?``\ `ident` appears +In the general case, when an existential variable :n:`?@ident` appears outside of its context of definition, its instance, written under the -form - -| ``{`` :n:`{*; @ident:=@term}` ``}`` - -is appending to its name, indicating how the variables of its defining context are instantiated. +form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +how the variables of its defining context are instantiated. The variables of the context of the existential variables which are instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances` is on (see Section :ref:`explicit-display-existentials`), and this is why an @@ -2247,7 +2264,3 @@ expression as described in :ref:`ltac`. This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. - -This mechanism is comparable to the ``Declare Implicit Tactic`` command -defined at :ref:`tactics-implicit-automation`, except that the used -tactic is local to each hole instead of being declared globally. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 1a33a9a46e..8fa631174f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -230,7 +230,7 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. themselves are typing the proofs. We denote propositions by :production:`form`. This constitutes a semantic subclass of the syntactic class :token:`term`. -- :g:`Set` is is the universe of *program types* or *specifications*. The +- :g:`Set` is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. |