diff options
| -rw-r--r-- | doc/refman/Extraction.tex | 99 |
1 files changed, 43 insertions, 56 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 187fe5342..74c8374de 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -110,17 +110,14 @@ even if some inlining is done, the inlined constant are nevertheless printed, to ensure session-independent programs. Concerning Haskell, type-preserving optimizations are less useful -because of lazyness. We still make some optimizations, for example in +because of laziness. We still make some optimizations, for example in order to produce more readable code. The type-preserving optimizations are controlled by the following \Coq\ options: \begin{description} -\item \optindex{Extraction Optimize} -{\tt Set Extraction Optimize.} - -\item {\tt Unset Extraction Optimize.} +\item \optindex{Extraction Optimize} {\tt Unset Extraction Optimize.} Default is Set. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also @@ -130,8 +127,6 @@ ML term as close as possible to the Coq term. \item \optindex{Extraction Conservative Types} {\tt Set Extraction Conservative Types.} -\item {\tt Unset Extraction Conservative Types.} - Default is Unset. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy types). Turn this option to Set to make sure that {\tt e:t} @@ -141,8 +136,6 @@ code of {\tt e} and {\tt t} respectively. \item \optindex{Extraction KeepSingleton} {\tt Set Extraction KeepSingleton.} -\item {\tt Unset Extraction KeepSingleton.} - Default is Unset. Normally, when the extraction of an inductive type produces a singleton type (i.e. a type with only one constructor, and only one argument to this constructor), the inductive structure is @@ -150,21 +143,15 @@ removed and this type is seen as an alias to the inner type. The typical example is {\tt sig}. This option allows disabling this optimization when one wishes to preserve the inductive structure of types. -\item \optindex{Extraction AutoInline} -{\tt Set Extraction AutoInline.} - -\item {\tt Unset Extraction AutoInline.} +\item \optindex{Extraction AutoInline} {\tt Unset Extraction AutoInline.} -Default is Set, so by default, the extraction mechanism is free to -inline the bodies of some defined constants, according to some heuristics +Default is Set. The extraction mechanism +inlines the bodies of some defined constants, according to some heuristics like size of bodies, uselessness of some arguments, etc. Those heuristics are not always perfect; if you want to disable this feature, do it by Unset. -\item \comindex{Extraction Inline} -{\tt Extraction Inline} \qualid$_1$ \dots\ \qualid$_n$. - -\item \comindex{Extraction NoInline} -{\tt Extraction NoInline} \qualid$_1$ \dots\ \qualid$_n$. +\item \comindex{Extraction Inline} \comindex{Extraction NoInline} +{\tt Extraction [Inline|NoInline] \qualid$_1$ \dots\ \qualid$_n$}. In addition to the automatic inline feature, you can tell to inline some more constants by the {\tt Extraction Inline} command. Conversely, @@ -265,28 +252,28 @@ extracted files. The extraction recognizes whether the realized axiom should become a ML type constant or a ML object declaration. \Example -\begin{coq_example} +\begin{coq_example*} Axiom X:Set. Axiom x:X. Extract Constant X => "int". Extract Constant x => "0". -\end{coq_example} +\end{coq_example*} 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 has to be given. The syntax is then: +variables have to be given. The syntax is then: \begin{description} -\item{\tt Extract Constant} \qualid\ \str$_1$ \dots\ \str$_n$ {\tt =>} \str. +\item{\tt Extract Constant \qualid\ \str$_1$ \dots\ \str$_n$ => \str.} \end{description} The number of type variables is checked by the system. \Example -\begin{coq_example} +\begin{coq_example*} Axiom Y : Set -> Set -> Set. Extract Constant Y "'a" "'b" => " 'a*'b ". -\end{coq_example} +\end{coq_example*} Realizing an axiom via {\tt Extract Constant} is only useful in the case of an informative axiom (of sort Type or Set). A logical axiom @@ -308,7 +295,7 @@ 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: \begin{description} -\item{\tt Extract Inductive} \qualid\ {\tt =>} \str\ {\tt [} \str\ \dots\ \str\ {\tt ]}\ {\it optstring}.\par +\item{\tt Extract Inductive \qualid\ => \str\ [ \str\ \dots\ \str\ ] {\it optstring}.}\par Give an ML extraction for the given inductive type. You must specify extractions for the type itself (first \str) and all its constructors (between square brackets). If given, the final optional @@ -412,7 +399,7 @@ For example, here are two kinds of problem that can occur: \begin{itemize} \item If some part of the program is {\em very} polymorphic, there may be no ML type for it. In that case the extraction to ML works - all right but the generated code may be refused by the ML + alright but the generated code may be refused by the ML type-checker. A very well known example is the {\em distr-pair} function: \begin{verbatim} @@ -549,34 +536,34 @@ Some pathological examples of extraction are grouped in the file \asubsection{Users' Contributions} - Several of the \Coq\ Users' Contributions use extraction to produce - certified programs. In particular the following ones have an automatic - extraction test (just run {\tt make} in those directories): - - \begin{itemize} - \item Bordeaux/Additions - \item Bordeaux/EXCEPTIONS - \item Bordeaux/SearchTrees - \item Dyade/BDDS - \item Lannion - \item Lyon/CIRCUITS - \item Lyon/FIRING-SQUAD - \item Marseille/CIRCUITS - \item Muenchen/Higman - \item Nancy/FOUnify - \item Rocq/ARITH/Chinese - \item Rocq/COC - \item Rocq/GRAPHS - \item Rocq/HIGMAN - \item Sophia-Antipolis/Stalmarck - \item Suresnes/BDD - \end{itemize} - - Lannion, Rocq/HIGMAN and Lyon/CIRCUITS are a bit particular. They are - examples of developments where {\tt Obj.magic} are needed. - This is probably due to an heavy use of impredicativity. - After compilation those two examples run nonetheless, - thanks to the correction of the extraction~\cite{Let02}. +Several of the \Coq\ Users' Contributions use extraction to produce +certified programs. In particular the following ones have an automatic +extraction test: + +\begin{itemize} +\item {\tt additions} +\item {\tt bdds} +\item {\tt canon-bdds} +\item {\tt chinese} +\item {\tt continuations} +\item {\tt coq-in-coq} +\item {\tt exceptions} +\item {\tt firing-squad} +\item {\tt founify} +\item {\tt graphs} +\item {\tt higman-cf} +\item {\tt higman-nw} +\item {\tt hardware} +\item {\tt multiplier} +\item {\tt search-trees} +\item {\tt stalmarck} +\end{itemize} + +{\tt continuations} and {\tt multiplier} are a bit particular. They are +examples of developments where {\tt Obj.magic} are needed. This is +probably due to an heavy use of impredicativity. After compilation, those +two examples run nonetheless, thanks to the correction of the +extraction~\cite{Let02}. %%% Local Variables: %%% mode: latex |