<commit_before>\achapter{Execution of extracted programs in Objective Caml and Haskell}
\label{Extraction}
\aauthor{<NAME> and <NAME>}
\index{Extraction}

\begin{flushleft}
  \em The status of extraction is experimental.
\end{flushleft}
We present here the \Coq\ extraction commands, used
to build certified and relatively
efficient ML programs, extracting them from the proofs of their
specifications. 
The ML dialects available as output language are currently 
\ocaml\ and {\sf Haskell}. In the following, ``ML'' will be 
used to refer to any of the two.

\paragraph{Differences with old versions.}
The current extraction mechanism is new for version 7.0 of {\Coq}.
In particular, the \FW\ toplevel used as an intermediate step between 
\Coq\ and ML has been withdrawn.  It is also not possible 
any more to import ML objects in this \FW\ toplevel.
The current mechanism also differs from
the one in previous versions of \Coq: there is no more
an explicit toplevel for the language (formerly called {\sf Fml}). 

\asection{Generating ML code}
\comindex{Extraction}
\comindex{Recursive Extraction}
\comindex{Extraction Module}
\comindex{Recursive Extraction Module}

The next two commands are meant to be used for rapid preview of
extraction. They both display extracted term(s) inside \Coq.

\begin{description}
\item {\tt Extraction \term.} ~\par
  Extracts one term in the \Coq\ toplevel.

\item {\tt Recursive Extraction  \qualid$_1$ \dots\ \qualid$_n$.} ~\par
  Recursive extraction of all the globals \qualid$_1$ \dots\
  \qualid$_n$ and all their dependencies in the \Coq\ toplevel.
\end{description}

%% TODO error messages


All the following commands produce real ML files. User can choose to produce
one monolithic file or one file per \Coq\ module. 

\begin{description}
\item {\tt Extraction "{\em file}"}  
      \qualid$_1$ \dots\ \qualid$_n$. ~\par
  Recursive extraction of all the globals \qualid$_1$ \dots\
  \qualid$_n$ and all their dependencies in one monolithic file {\em file}.
  Global and local identifiers are renamed according to the choosen ML
  language to fullfill its syntactic conventions, keeping original
  names as much as possible.

\item  {\tt Extraction Module} \ident. ~\par
  Extraction of the \Coq\ module \ident\ to an ML module {\tt\ident.ml}.
  In case of name clash, identifiers are here renamed using prefixes
  \verb!coq_! 
  or \verb!Coq_! to ensure a session-independent renaming.

\item {\tt Recursive Extraction Module} \ident. ~\par
  Extraction of the \Coq\ module \ident\ and all other modules \ident\
  depends on. 
\end{description}

The list of globals \qualid$_i$ does not need to be
exhaustive: it is automatically completed into a complete and minimal
environment. Extraction will fail if it encounters an informative
axiom not realized (see section \ref{extraction:axioms}). 
A warning will be issued if it encounters an logical axiom, to remind 
user that inconsistant logical axioms may lead to incorrect or 
non-terminating extracted terms. 


\asection{Extraction options}

\asubsection{Setting the ML target language}
\comindex{Extraction Language}

The ability to fix target ML dialect is the first and more important<commit_msg>Evitons de dire que Haskell est un dialect ML<commit_after>\achapter{Extraction of programs in Objective Caml and Haskell}
\label{Extraction}
\aauthor{<NAME> and <NAME>}
\index{Extraction}

\begin{flushleft}
  \em The status of extraction is experimental.
\end{flushleft}
We present here the \Coq\ extraction commands, used
to build certified and relatively
efficient functional programs, extracting them from the proofs of their
specifications. 
The functional languages available as output are currently 
\ocaml\ and {\sf Haskell}. In the following, ``ML'' will be 
used (abusively) to refer to any of the two.

\paragraph{Differences with old versions.}
The current extraction mechanism is new for version 7.0 of {\Coq}.
In particular, the \FW\ toplevel used as an intermediate step between 
\Coq\ and ML has been withdrawn.  It is also not possible 
any more to import ML objects in this \FW\ toplevel.
The current mechanism also differs from
the one in previous versions of \Coq: there is no more
an explicit toplevel for the language (formerly called {\sf Fml}). 

\asection{Generating ML code}
\comindex{Extraction}
\comindex{Recursive Extraction}
\comindex{Extraction Module}
\comindex{Recursive Extraction Module}

The next two commands are meant to be used for rapid preview of
extraction. They both display extracted term(s) inside \Coq.

\begin{description}
\item {\tt Extraction \term.} ~\par
  Extracts one term in the \Coq\ toplevel.

\item {\tt Recursive Extraction  \qualid$_1$ \dots\ \qualid$_n$.} ~\par
  Recursive extraction of all the globals \qualid$_1$ \dots\
  \qualid$_n$ and all their dependencies in the \Coq\ toplevel.
\end{description}

%% TODO error messages


All the following commands produce real ML files. User can choose to produce
one monolithic file or one file per \Coq\ module. 

\begin{description}
\item {\tt Extraction "{\em file}"}  
      \qualid$_1$ \dots\ \qualid$_n$. ~\par
  Recursive extraction of all the globals \qualid$_1$ \dots\
  \qualid$_n$ and all their dependencies in one monolithic file {\em file}.
  Global and local identifiers are renamed according to the choosen ML
  language to fullfill its syntactic conventions, keeping original
  names as much as possible.

\item  {\tt Extraction Module} \ident. ~\par
  Extraction of the \Coq\ module \ident\ to an ML module {\tt\ident.ml}.
  In case of name clash, identifiers are here renamed using prefixes
  \verb!coq_! 
  or \verb!Coq_! to ensure a session-independent renaming.

\item {\tt Recursive Extraction Module} \ident. ~\par
  Extraction of the \Coq\ module \ident\ and all other modules \ident\
  depends on. 
\end{description}

The list of globals \qualid$_i$ does not need to be
exhaustive: it is automatically completed into a complete and minimal
environment. Extraction will fail if it encounters an informative
axiom not realized (see section \ref{extraction:axioms}). 
A warning will be issued if it encounters an logical axiom, to remind 
user that inconsistant logical axioms may lead to incorrect or 
non-terminating extracted terms. 


\asection{Extraction options}

\asubsection{Setting the target language}
\comindex{Extraction Language}

The ability to fix target language is the first and more important
{'fraction_non_alphanumeric': 0.0764449968924798, 'fraction_numerical': 0.0018645121193287756, 'mean_word_length': 4.060534591194968, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3053342', 'n_tokens_mistral': 1943, 'n_tokens_neox': 1834, 'n_words': 878}