diff options
Diffstat (limited to 'doc/sphinx/addendum/implicit-coercions.rst')
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 156 |
1 files changed, 77 insertions, 79 deletions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index f5ca5be44..09faa0676 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -1,7 +1,7 @@ -.. _implicitcoercions: - .. include:: ../replaces.rst +.. _implicitcoercions: + Implicit Coercions ==================== @@ -65,7 +65,7 @@ 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 classe ``Sortclass`` can be used as a source class, but +.. note:: The abstract class ``Sortclass`` can be used as a source class, but the abstract class ``Funclass`` cannot. To coerce an object :g:`t:C t₁..tₙ` of ``C`` towards ``D``, we have to @@ -124,49 +124,49 @@ term consists of the successive application of its coercions. Declaration of Coercions ------------------------- -.. cmd:: Coercion @qualid : @class >-> @class. +.. cmd:: Coercion @qualid : @class >-> @class Declares the construction denoted by `qualid` as a coercion between the two given classes. - .. exn:: @qualid not declared - .. exn:: @qualid is already a coercion - .. exn:: Funclass cannot be a source class - .. exn:: @qualid is not a function - .. exn:: Cannot find the source class of @qualid - .. exn:: Cannot recognize @class as a source class of @qualid - .. exn:: @qualid does not respect the uniform inheritance condition + .. exn:: @qualid not declared. + .. exn:: @qualid is already a coercion. + .. exn:: Funclass cannot be a source class. + .. exn:: @qualid is not a function. + .. exn:: Cannot find the source class of @qualid. + .. exn:: Cannot recognize @class as a source class of @qualid. + .. exn:: @qualid does not respect the uniform inheritance condition. .. exn:: Found target class ... instead of ... - .. warn:: Ambigous path: + .. warn:: Ambiguous path. - When the coercion `qualid` is added to the inheritance graph, non - valid coercion paths are ignored; they are signaled by a warning - displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, non + valid 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. + .. cmdv:: Local Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion local to - the current section. + Declares the construction denoted by `qualid` as a coercion local to + the current section. - .. cmdv:: Coercion @ident := @term. + .. cmdv:: Coercion @ident := @term - This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. - .. cmdv:: Coercion @ident := @term : @type. + .. cmdv:: Coercion @ident := @term : @type - This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. - .. cmdv:: Local Coercion @ident := @term. + .. cmdv:: Local Coercion @ident := @term - This defines `ident` just like ``Let`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Let`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. Assumptions can be declared as coercions at declaration time. This extends the grammar of assumptions from -Figure :ref:`TODO-1.3-sentences-syntax` as follows: +Figure :ref:`vernacular` as follows: .. FIXME: @@ -186,7 +186,7 @@ assumptions are declared as coercions. Similarly, constructors of inductive types can be declared as coercions at definition time of the inductive type. This extends and modifies the -grammar of inductive types from Figure :ref:`TODO-1.3-sentences-syntax` as follows: +grammar of inductive types from Figure :ref:`vernacular` as follows: .. FIXME: @@ -202,7 +202,7 @@ grammar of inductive types from Figure :ref:`TODO-1.3-sentences-syntax` as follo Especially, if the extra ``>`` is present in a constructor declaration, this constructor is declared as a coercion. -.. cmd:: Identity Coercion @ident : @class >-> @class. +.. cmd:: Identity Coercion @ident : @class >-> @class If ``C`` is the source `class` and ``D`` the destination, we check that ``C`` is a constant with a body of the form @@ -211,13 +211,14 @@ declaration, this constructor is declared as a coercion. function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`, and we declare it as an identity coercion between ``C`` and ``D``. - .. exn:: @class must be a transparent constant + .. exn:: @class must be a transparent constant. - .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident. + .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident Idem but locally to the current section. - .. cmdv:: SubClass @ident := @type. + .. cmdv:: SubClass @ident := @type + :name: SubClass If `type` is a class `ident'` applied to some arguments then `ident` is defined and an identity coercion of name @@ -228,7 +229,7 @@ declaration, this constructor is declared as a coercion. ``Identity Coercion`` `Id_ident_ident'` : `ident` ``>->`` `ident'`. - .. cmdv:: Local SubClass @ident := @type. + .. cmdv:: Local SubClass @ident := @type Same as before but locally to the current section. @@ -236,67 +237,67 @@ declaration, this constructor is declared as a coercion. Displaying Available Coercions ------------------------------- -.. cmd:: Print Classes. +.. cmd:: Print Classes Print the list of declared classes in the current context. -.. cmd:: Print Coercions. +.. cmd:: Print Coercions Print the list of declared coercions in the current context. -.. cmd:: Print Graph. +.. cmd:: Print Graph Print the list of valid coercion paths in the current context. -.. cmd:: Print Coercion Paths @class @class. +.. cmd:: Print Coercion Paths @class @class Print the list of valid coercion paths between the two given classes. Activating the Printing of Coercions ------------------------------------- -.. cmd:: Set Printing Coercions. +.. opt:: Printing Coercions + + When on, this option forces all the coercions to be printed. + By default, coercions are not printed. + +.. cmd:: Add Printing Coercion @qualid - This command forces all the coercions to be printed. - Conversely, to skip the printing of coercions, use - ``Unset Printing Coercions``. By default, coercions are not printed. + This command forces coercion denoted by :n:`@qualid` to be printed. + By default, a coercion is never printed. -.. cmd:: Add Printing Coercion @qualid. +.. cmd:: Remove Printing Coercion @qualid - This command forces coercion denoted by `qualid` to be printed. - To skip the printing of coercion `qualid`, use - ``Remove Printing Coercion`` `qualid`. By default, a coercion is never printed. + Use this command, to skip the printing of coercion :n:`@qualid`. +.. _coercions-classes-as-records: Classes as Records ------------------ -We allow the definition of *Structures with Inheritance* (or -classes as records) by extending the existing ``Record`` macro -(see Section :ref:`TODO-2.1-Record`). Its new syntax is: +We allow the definition of *Structures with Inheritance* (or classes as records) +by extending the existing :cmd:`Record` macro. Its new syntax is: -.. cmd:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. +.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } - The first identifier `ident` is the name of the defined record and - `sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be ``Build_``\ `ident` if not given). - The other identifiers are the names of the fields, and the `term` - are their respective types. If ``:>`` is used instead of ``:`` in - the declaration of a field, then the name of this field is automatically - declared as a coercion from the record name to the class of this - field type. Remark that the fields always verify the uniform - inheritance condition. If the optional ``>`` is given before the - record name, then the constructor name is automatically declared as - a coercion from the class of the last field type to the record name - (this may fail if the uniform inheritance condition is not - satisfied). + The first identifier `ident` is the name of the defined record and + `sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be ``Build_``\ `ident` if not given). + The other identifiers are the names of the fields, and the `term` + are their respective types. If ``:>`` is used instead of ``:`` in + the declaration of a field, then the name of this field is automatically + declared as a coercion from the record name to the class of this + field type. Remark that the fields always verify the uniform + inheritance condition. If the optional ``>`` is given before the + record name, then the constructor name is automatically declared as + a coercion from the class of the last field type to the record name + (this may fail if the uniform inheritance condition is not + satisfied). -.. note:: +.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } + :name: Structure - The keyword ``Structure`` is a synonym of ``Record``. - -.. - FIXME: \comindex{Structure} + This is a synonym of :cmd:`Record`. Coercions and Sections @@ -312,20 +313,17 @@ coercions which do not verify the uniform inheritance condition any longer are also forgotten. Coercions and Modules ---------------------= - -From |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 -imported or not. - -To recover the behavior of the versions of |Coq| prior to 8.3, use the -following command: +--------------------- -.. cmd:: Set Automatic Coercions Import. +.. opt:: Automatic Coercions Import -To cancel the effect of the option, use instead ``Unset Automatic Coercions Import``. + 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 + imported or not. + This option makes it possible to recover the behavior of the versions of + |Coq| prior to 8.3. Examples -------- |