diff options
Diffstat (limited to 'doc/sphinx/addendum/extraction.rst')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 139 |
1 files changed, 69 insertions, 70 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index d7f97edab..cb93d48a4 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,16 +1,16 @@ -.. _extraction: - .. include:: ../replaces.rst -Extraction of programs in OCaml and Haskell -============================================ +.. _extraction: + +Extraction of programs in |OCaml| and Haskell +============================================= :Authors: Jean-Christophe Filliâtre and Pierre Letouzey We present here the |Coq| extraction commands, used to build certified and relatively efficient functional programs, extracting them from either |Coq| functions or |Coq| proofs of specifications. The -functional languages available as output are currently OCaml, Haskell +functional languages available as output are currently |OCaml|, Haskell and Scheme. In the following, "ML" will be used (abusively) to refer to any of the three. @@ -37,11 +37,11 @@ Generating ML Code The next two commands are meant to be used for rapid preview of extraction. They both display extracted term(s) inside |Coq|. -.. cmd:: Extraction @qualid. +.. cmd:: Extraction @qualid Extraction of the mentioned object in the |Coq| toplevel. -.. cmd:: Recursive Extraction @qualid ... @qualid. +.. cmd:: Recursive Extraction {+ @qualid } Recursive extraction of all the mentioned objects and all their dependencies in the |Coq| toplevel. @@ -49,7 +49,7 @@ 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 ... @qualid. +.. cmd:: Extraction "@file" {+ @qualid } Recursive extraction of all the mentioned objects and all their dependencies in one monolithic `file`. @@ -57,43 +57,43 @@ produce one monolithic file or one file per |Coq| library. language to fulfill its syntactic conventions, keeping original names as much as possible. -.. cmd:: Extraction Library @ident. +.. 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 using prefixes ``coq_`` or ``Coq_`` to ensure a session-independent renaming. -.. cmd:: Recursive Extraction Library @ident. +.. cmd:: Recursive Extraction Library @ident Extraction of the |Coq| library ``ident.v`` and all other modules ``ident.v`` depends on. -.. cmd:: Separate Extraction @qualid ... @qualid. +.. cmd:: Separate Extraction {+ @qualid } Recursive extraction of all the mentioned objects and all their dependencies, just as ``Extraction "file"``, 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 - ``Recursive Extraction Library``, except that only the needed + :cmd:`Recursive Extraction Library`, except that only the needed parts of Coq libraries are extracted instead of the whole. The naming convention in case of name clash is the same one as - ``Extraction Library``: identifiers are here renamed using prefixes + :cmd:`Extraction Library`: identifiers are here renamed using prefixes ``coq_`` or ``Coq_``. The following command is meant to help automatic testing of the extraction, see for instance the ``test-suite`` directory in the |Coq| sources. -.. cmd:: Extraction TestCompile @qualid ... @qualid. +.. cmd:: Extraction TestCompile {+ @qualid } All the mentioned objects and all their dependencies are extracted - to a temporary OCaml file, just as in ``Extraction "file"``. Then + to a temporary |OCaml| file, just as in ``Extraction "file"``. Then this temporary file and its signature are compiled with the same - OCaml compiler used to built |Coq|. This command succeeds only - if the extraction and the OCaml compilation succeed. It fails - if the current target language of the extraction is not OCaml. + |OCaml| compiler used to built |Coq|. This command succeeds only + if the extraction and the |OCaml| compilation succeed. It fails + if the current target language of the extraction is not |OCaml|. Extraction Options ------------------- @@ -102,26 +102,26 @@ Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ The ability to fix target language is the first and more important -of the extraction options. Default is ``Ocaml``. +of the extraction options. Default is ``OCaml``. -.. cmd:: Extraction Language Ocaml. -.. cmd:: Extraction Language Haskell. -.. cmd:: Extraction Language Scheme. +.. cmd:: Extraction Language OCaml +.. cmd:: Extraction Language Haskell +.. cmd:: Extraction Language Scheme Inlining and optimizations ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Since OCaml is a strict language, the extracted code has to +Since |OCaml| is a strict language, the extracted code has to be optimized in order to be efficient (for instance, when using induction principles we do not want to compute all the recursive calls but only the needed ones). So the extraction mechanism provides an automatic optimization routine that will be called each time the user -want to generate OCaml programs. The optimizations can be split in two +want to generate |OCaml| programs. The optimizations can be split in two groups: the type-preserving ones (essentially constant inlining and reductions) and the non type-preserving ones (some function abstractions of dummy types are removed when it is deemed safe in order to have more elegant types). Therefore some constants may not appear in the -resulting monolithic OCaml program. In the case of modular extraction, +resulting monolithic |OCaml| program. In the case of modular extraction, even if some inlining is done, the inlined constant are nevertheless printed, to ensure session-independent programs. @@ -131,14 +131,14 @@ order to produce more readable code. The type-preserving optimizations are controlled by the following |Coq| options: -.. opt:: Extraction Optimize. +.. opt:: Extraction Optimize Default is on. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also simplifications on Cases, etc). Turn this option off if you want a ML term as close as possible to the Coq term. -.. opt:: Extraction Conservative Types. +.. opt:: Extraction Conservative Types Default is off. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy @@ -146,7 +146,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted code of ``e`` and ``t`` respectively. -.. opt:: Extraction KeepSingleton. +.. opt:: Extraction KeepSingleton Default is off. Normally, when the extraction of an inductive type produces a singleton type (i.e. a type with only one constructor, and @@ -155,7 +155,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: The typical example is ``sig``. This option allows disabling this optimization when one wishes to preserve the inductive structure of types. -.. opt:: Extraction AutoInline. +.. opt:: Extraction AutoInline Default is on. The extraction mechanism inlines the bodies of some defined constants, according to some heuristics @@ -163,22 +163,22 @@ The type-preserving optimizations are controlled by the following |Coq| options: Those heuristics are not always perfect; if you want to disable this feature, turn this option off. -.. cmd:: Extraction Inline @qualid ... @qualid. +.. cmd:: Extraction Inline {+ @qualid } In addition to the automatic inline feature, the constants mentionned by this command will always be inlined during extraction. -.. cmd:: Extraction NoInline @qualid ... @qualid. +.. cmd:: Extraction NoInline {+ @qualid } Conversely, the constants mentionned by this command will never be inlined during extraction. -.. cmd:: Print Extraction Inline. +.. cmd:: Print Extraction Inline Prints the current state of the table recording the custom inlinings declared by the two previous commands. -.. cmd:: Reset Extraction Inline. +.. cmd:: Reset Extraction Inline Empties the table recording the custom inlinings (see the previous commands). @@ -213,7 +213,7 @@ code elimination performed during extraction, in a way which is independent but complementary to the main elimination principles of extraction (logical parts and types). -.. cmd:: Extraction Implicit @qualid [ @ident ... @ident ]. +.. 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 @@ -223,11 +223,11 @@ principles of extraction (logical parts and types). by a number indicating its position, starting from 1. When an actual extraction takes place, an error is normally raised if the -``Extraction Implicit`` declarations cannot be honored, that is +:cmd:`Extraction Implicit` declarations cannot be honored, that is if any of the implicited variables still occurs in the final code. This behavior can be relaxed via the following option: -.. opt:: Extraction SafeImplicits. +.. opt:: Extraction SafeImplicits Default is on. When this option is off, a warning is emitted instead of an error if some implicited variables still occur in the @@ -253,21 +253,20 @@ a closed term, and of course the system cannot guess the program which realizes an axiom. Therefore, it is possible to tell the system what ML term corresponds to a given axiom. -.. cmd:: Extract Constant @qualid => @string. +.. cmd:: Extract Constant @qualid => @string Give an ML extraction for the given constant. The `string` may be an identifier or a quoted string. -.. cmd:: Extract Inlined Constant @qualid => @string. +.. cmd:: Extract Inlined Constant @qualid => @string Same as the previous one, except that the given ML terms will be inlined everywhere instead of being declared via a ``let``. .. note:: - - This command is sugar for an ``Extract Constant`` followed - by a ``Extraction Inline``. Hence a ``Reset Extraction Inline`` - will have an effect on the realized and inlined axiom. + This command is sugar for an :cmd:`Extract Constant` followed + by a :cmd:`Extraction Inline`. Hence a :cmd:`Reset Extraction Inline` + will have an effect on the realized and inlined axiom. .. caution:: It is the responsibility of the user to ensure that the ML terms given to realize the axioms do have the expected types. In @@ -286,7 +285,7 @@ Notice that in the case of type scheme axiom (i.e. whose type is an arity, that is a sequence of product finished by a sort), then some type variables have to be given (as quoted strings). The syntax is then: -.. cmdv:: Extract Constant @qualid @string ... @string => @string. +.. cmdv:: Extract Constant @qualid @string ... @string => @string The number of type variables is checked by the system. For example: @@ -295,7 +294,7 @@ The number of type variables is checked by the system. For example: Axiom Y : Set -> Set -> Set. Extract Constant Y "'a" "'b" => " 'a * 'b ". -Realizing an axiom via ``Extract Constant`` is only useful in the +Realizing an axiom via :cmd:`Extract Constant` is only useful in the case of an informative axiom (of sort ``Type`` or ``Set``). A logical axiom have no computational content and hence will not appears in extracted terms. But a warning is nonetheless issued if extraction encounters a @@ -315,7 +314,7 @@ The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML native boolean type instead of |Coq| one. The syntax is the following: -.. cmd:: Extract Inductive @qualid => @string [ @string ... @string ]. +.. 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 @@ -323,7 +322,7 @@ native boolean type instead of |Coq| one. The syntax is the following: 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 ] @string. +.. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra `string` that indicates how to perform pattern-matching over this inductive type. In this form, @@ -336,10 +335,10 @@ native boolean type instead of |Coq| one. The syntax is the following: argument 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`` - into OCaml ``int``, the code to provide has type: + into |OCaml| ``int``, the code to provide has type: ``(unit->'a)->(int->'a)->int->'a``. -.. caution:: As for ``Extract Constant``, this command should be used with care: +.. caution:: As for :cmd:`Extract Constant`, this command should be used with care: * The ML code provided by the user is currently **not** checked at all by extraction, even for syntax errors. @@ -347,17 +346,17 @@ native boolean type instead of |Coq| one. The syntax is the following: * Extracting an inductive type to a pre-existing ML inductive type is quite sound. But extracting to a general type (by providing an ad-hoc pattern-matching) will often **not** be fully rigorously - correct. For instance, when extracting ``nat`` to OCaml ``int``, + correct. For instance, when extracting ``nat`` to |OCaml| ``int``, it is theoretically possible to build ``nat`` values that are - larger than OCaml ``max_int``. It is the user's responsibility to + larger than |OCaml| ``max_int``. It is the user's responsibility to be sure that no overflow or other bad events occur in practice. * Translating an inductive type to an arbitrary ML type does **not** magically improve the asymptotic complexity of functions, even if the ML type is an efficient representation. For instance, when extracting - ``nat`` to OCaml ``int``, the function ``Nat.mul`` stays quadratic. + ``nat`` to |OCaml| ``int``, the function ``Nat.mul`` stays quadratic. It might be interesting to associate this translation with - some specific ``Extract Constant`` when primitive counterparts exist. + some specific :cmd:`Extract Constant` when primitive counterparts exist. Typical examples are the following: @@ -369,9 +368,9 @@ Typical examples are the following: .. note:: - When extracting to Ocaml, if an inductive constructor or type has arity 2 and + When extracting to |OCaml|, if an inductive constructor or type has arity 2 and the corresponding string is enclosed by parentheses, and the string meets - Ocaml's lexical criteria for an infix symbol, then the rest of the string is + |OCaml|'s lexical criteria for an infix symbol, then the rest of the string is used as infix constructor or type. .. coqtop:: in @@ -380,7 +379,7 @@ Typical examples are the following: Extract Inductive prod => "(*)" [ "(,)" ]. As an example of translation to a non-inductive datatype, let's turn -``nat`` into OCaml ``int`` (see caveat above): +``nat`` into |OCaml| ``int`` (see caveat above): .. coqtop:: in @@ -389,28 +388,28 @@ As an example of translation to a non-inductive datatype, let's turn Avoiding conflicts with existing filenames ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When using ``Extraction Library``, the names of the extracted files +When using :cmd:`Extraction Library`, the names of the extracted files directly depends from the names of the |Coq| files. It may happen that these filenames are in conflict with already existing files, either in the standard library of the target language or in other code that is meant to be linked with the extracted code. -For instance the module ``List`` exists both in |Coq| and in OCaml. +For instance the module ``List`` exists both in |Coq| and in |OCaml|. It is possible to instruct the extraction not to use particular filenames. -.. cmd:: Extraction Blacklist @ident ... @ident. +.. cmd:: Extraction Blacklist {+ @ident } Instruct the extraction to avoid using these names as filenames for extracted code. -.. cmd:: Print Extraction Blacklist. +.. cmd:: Print Extraction Blacklist Show the current list of filenames the extraction should avoid. -.. cmd:: Reset Extraction Blacklist. +.. cmd:: Reset Extraction Blacklist Allow the extraction to use any filename. -For OCaml, a typical use of these commands is +For |OCaml|, a typical use of these commands is ``Extraction Blacklist String List``. Differences between |Coq| and ML type systems @@ -418,7 +417,7 @@ Differences between |Coq| and ML type systems Due to differences between |Coq| and ML type systems, some extracted programs are not directly typable in ML. -We now solve this problem (at least in OCaml) by adding +We now solve this problem (at least in |OCaml|) by adding when needed some unsafe casting ``Obj.magic``, which give a generic type ``'a`` to any term. @@ -432,7 +431,7 @@ function: Definition dp {A B:Type}(x:A)(y:B)(f:forall C:Type, C->C) := (f A x, f B y). -In Ocaml, for instance, the direct extracted term would be:: +In |OCaml|, for instance, the direct extracted term would be:: let dp x y f = Pair((f () x),(f () y)) @@ -455,12 +454,12 @@ of a constructor; for example: Inductive anything : Type := dummy : forall A:Set, A -> anything. which corresponds to the definition of an ML dynamic type. -In OCaml, we must cast any argument of the constructor dummy +In |OCaml|, we must cast any argument of the constructor dummy (no GADT are produced yet by the extraction). Even with those unsafe castings, you should never get error like ``segmentation fault``. In fact even if your program may seem -ill-typed to the Ocaml type-checker, it can't go wrong : it comes +ill-typed to the |OCaml| type-checker, it can't go wrong : it comes from a Coq well-typed terms, so for example inductive types will always have the correct number of arguments, etc. Of course, when launching manually some extracted function, you should apply it to arguments @@ -470,14 +469,14 @@ More details about the correctness of the extracted programs can be found in :cite:`Let02`. We have to say, though, that in most "realistic" programs, these problems do not -occur. For example all the programs of Coq library are accepted by the OCaml +occur. For example all the programs of Coq library are accepted by the |OCaml| type-checker without any ``Obj.magic`` (see examples below). Some examples ------------- We present here two examples of extractions, taken from the -|Coq| Standard Library. We choose OCaml as target language, +|Coq| Standard Library. We choose |OCaml| as target language, but all can be done in the other dialects with slight modifications. We then indicate where to find other examples and tests of extraction. @@ -493,7 +492,7 @@ This module contains a theorem ``eucl_dev``, whose type is:: where ``diveucl`` is a type for the pair of the quotient and the modulo, plus some logical assertions that disappear during extraction. -We can now extract this program to OCaml: +We can now extract this program to |OCaml|: .. coqtop:: none @@ -513,7 +512,7 @@ You can then copy-paste the output to a file ``euclid.ml`` or let Extraction "euclid" eucl_dev. -Let us play the resulting program (in an OCaml toplevel):: +Let us play the resulting program (in an |OCaml| toplevel):: #use "euclid.ml";; type nat = O | S of nat @@ -527,7 +526,7 @@ Let us play the resulting program (in an OCaml toplevel):: # eucl_dev (S (S O)) (S (S (S (S (S O)))));; - : diveucl = Divex (S (S O), S O) -It is easier to test on OCaml integers:: +It is easier to test on |OCaml| integers:: # let rec nat_of_int = function 0 -> O | n -> S (nat_of_int (n-1));; val nat_of_int : int -> nat = <fun> |