diff options
Diffstat (limited to 'doc/sphinx/addendum/extraction.rst')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index f523a39477..b7d05fd6ef 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -28,7 +28,7 @@ Generating ML Code .. note:: - In the following, a qualified identifier `qualid` + In the following, a qualified identifier :token:`qualid` can be used to refer to any kind of |Coq| global "object" : constant, inductive type, inductive constructor or module name. @@ -47,30 +47,30 @@ extraction. They both display extracted term(s) inside |Coq|. All the following commands produce real ML files. User can choose to produce one monolithic file or one file per |Coq| library. -.. cmd:: Extraction "@file" {+ @qualid } +.. cmd:: Extraction @string {+ @qualid } Recursive extraction of all the mentioned objects and all - their dependencies in one monolithic `file`. + their dependencies in one monolithic file :token:`string`. Global and local identifiers are renamed according to the chosen ML language to fulfill its syntactic conventions, keeping original names as much as possible. .. cmd:: Extraction Library @ident - Extraction of the whole |Coq| library ``ident.v`` to an ML module - ``ident.ml``. In case of name clash, identifiers are here renamed + Extraction of the whole |Coq| library :n:`@ident.v` to an ML module + :n:`@ident.ml`. In case of name clash, identifiers are here renamed using prefixes ``coq_`` or ``Coq_`` to ensure a session-independent renaming. .. cmd:: Recursive Extraction Library @ident - Extraction of the |Coq| library ``ident.v`` and all other modules - ``ident.v`` depends on. + Extraction of the |Coq| library :n:`@ident.v` and all other modules + :n:`@ident.v` depends on. .. cmd:: Separate Extraction {+ @qualid } Recursive extraction of all the mentioned objects and all - their dependencies, just as ``Extraction "file"``, + their dependencies, just as :n:`Extraction @string {+ @qualid }`, but instead of producing one monolithic file, this command splits the produced code in separate ML files, one per corresponding Coq ``.v`` file. This command is hence quite similar to @@ -214,9 +214,9 @@ principles of extraction (logical parts and types). .. cmd:: Extraction Implicit @qualid [ {+ @ident } ] This experimental command allows declaring some arguments of - `qualid` as implicit, i.e. useless in extracted code and hence to - be removed by extraction. Here `qualid` can be any function or - inductive constructor, and the given `ident` are the names of + :token:`qualid` as implicit, i.e. useless in extracted code and hence to + be removed by extraction. Here :token:`qualid` can be any function or + inductive constructor, and the given :token:`ident` are the names of the concerned arguments. In fact, an argument can also be referred by a number indicating its position, starting from 1. @@ -253,7 +253,7 @@ what ML term corresponds to a given axiom. .. cmd:: Extract Constant @qualid => @string Give an ML extraction for the given constant. - The `string` may be an identifier or a quoted string. + The :token:`string` may be an identifier or a quoted string. .. cmd:: Extract Inlined Constant @qualid => @string @@ -315,24 +315,24 @@ native boolean type instead of the |Coq| one. The syntax is the following: .. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first `string`) and all its - constructors (all the `string` between square brackets). In this form, + extractions for the type itself (first :token:`string`) and all its + constructors (all the :token:`string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native pattern matching of the language will be used. .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string - Same as before, with a final extra `string` that indicates how to + Same as before, with a final extra :token:`string` that indicates how to perform pattern matching over this inductive type. In this form, the ML extraction could be an arbitrary type. - For an inductive type with `k` constructors, the function used to - emulate the pattern matching should expect `(k+1)` arguments, first the `k` + For an inductive type with :math:`k` constructors, the function used to + emulate the pattern matching should expect :math:`k+1` arguments, first the :math:`k` branches in functional form, and then the inductive element to destruct. For instance, the match branch ``| S n => foo`` gives the functional form ``(fun n -> foo)``. Note that a constructor with no arguments is considered to have one unit argument, in order to block early evaluation of the branch: ``| O => bar`` leads to the functional - form ``(fun () -> bar)``. For instance, when extracting ``nat`` + form ``(fun () -> bar)``. For instance, when extracting :g:`nat` into |OCaml| ``int``, the code to be provided has type: ``(unit->'a)->(int->'a)->int->'a``. |