Update of Extraction documentation

 - Removal of the notice about the "experimental" status of extraction.
   Of course extraction is still experimental, but no less than the rest
   of Coq ;-)
 - Removal of the example about heapsort now that Heap is obsolete.
 - Euclid isn't the best of the examples, but for the moment we leave it
 - We mention ExtrOcamlIntConv and the others extraction/*.v
 - Various small improvements

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13136 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 33 insertions, 236 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 5d90ae661..c5b7164a8 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -3,15 +3,12 @@
 \aauthor{Jean-Christophe Filliātre and Pierre Letouzey}
 \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{}, \textsc{Haskell} and \textsc{Scheme}.
-In the following, ``ML'' will be used (abusively) to refer to any of
-the three.
+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{},
+\textsc{Haskell} and \textsc{Scheme}.  In the following, ``ML'' will
+be used (abusively) to refer to any of the three.
 
 \paragraph{Differences with old versions.}
 The current extraction mechanism is new for version 7.0 of {\Coq}.
@@ -91,10 +88,10 @@ 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. Essentially,
 it performs constants inlining and reductions.  Therefore some
-constants may not appear in resulting monolithic Ocaml program (a warning is
-printed for each such constant). In the case of modular extraction, 
-even if some inlining is done, the inlined constant are nevertheless
-printed, to ensure session-independent programs. 
+constants may not appear in 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.
 
 Concerning Haskell, such optimizations are less useful because of
 lazyness. We still make some optimizations, for example in order to
@@ -374,7 +371,7 @@ We now solve this problem (at least in Ocaml) by adding
 when needed some unsafe casting {\tt Obj.magic}, which give
 a generic type {\tt 'a} to any term.
 
-For example, Here are two kinds of problem that can occur: 
+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
@@ -450,25 +447,25 @@ Inductive nat : Set :=
   | S : nat -> nat.
 \end{coq_example*}
 
-This module contains a theorem {\tt eucl\_dev}, and its extracted term
-is of type 
+This module contains a theorem {\tt eucl\_dev}, whose type is:
 \begin{verbatim}
 forall b:nat, b > 0 -> forall a:nat, diveucl a b
 \end{verbatim}
-where {\tt diveucl} is a type for the pair of the quotient and the modulo.
+where {\tt 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:
 
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Require Import Euclid.
-Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec.
-Recursive Extraction  eucl_dev.
+Require Import Euclid Wf_nat.
+Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2.
+Recursive Extraction eucl_dev.
 \end{coq_example}
 
-The inlining of {\tt gt\_wf\_rec} and {\tt lt\_wf\_rec} is not
-mandatory. It only enhances readability of extracted code. 
+The inlining of {\tt gt\_wf\_rec} and others is not
+mandatory. It only enhances readability of extracted code.
 You can then copy-paste the output to a file {\tt euclid.ml} or let 
 \Coq\ do it for you with the following command: 
 
@@ -480,240 +477,40 @@ Let us play the resulting program:
 
 \begin{verbatim}
 # #use "euclid.ml";;
-type sumbool = Left | Right
 type nat = O | S of nat
-type diveucl = Divex of nat * nat
+type sumbool = Left | Right
 val minus : nat -> nat -> nat = <fun>
 val le_lt_dec : nat -> nat -> sumbool = <fun>
 val le_gt_dec : nat -> nat -> sumbool = <fun>
+type diveucl = Divex of nat * nat
 val eucl_dev : nat -> nat -> diveucl = <fun>
 # eucl_dev (S (S O)) (S (S (S (S (S O)))));;
 - : diveucl = Divex (S (S O), S O)
 \end{verbatim}
 It is easier to test on \ocaml\ integers:
 \begin{verbatim}
-# let rec i2n = function 0 -> O | n -> S (i2n (n-1));;
+# let rec nat_of_int = function 0 -> O | n -> S (nat_of_int (n-1));;
 val i2n : int -> nat = <fun>
-# let rec n2i = function O -> 0 | S p -> 1+(n2i p);;
+# let rec int_of_nat = function O -> 0 | S p -> 1+(int_of_nat p);;
 val n2i : nat -> int = <fun>
 # let div a b = 
-     let Divex (q,r) = eucl_dev (i2n b) (i2n a) in (n2i q, n2i r);;
-div : int -> int -> int * int = <fun>
+     let Divex (q,r) = eucl_dev (nat_of_int b) (nat_of_int a)
+     in (int_of_nat q, int_of_nat r);;
+val div : int -> int -> int * int = <fun>
 # div 173 15;;
-- : int * int = 11, 8
-\end{verbatim}
-
-\asubsection{Another detailed example: Heapsort}
-
-The file {\tt Heap.v}
-contains the proof of an efficient list sorting algorithm described by
-Bjerner. Is is an adaptation of the well-known {\em heapsort}
-algorithm to functional languages. The main function is {\tt
-treesort}, whose type is shown below: 
-
-
-\begin{coq_eval}
-Reset Initial.
-Require Import Relation_Definitions.
-Require Import List.
-Require Import Sorting.
-Require Import Permutation.
-\end{coq_eval}
-\begin{coq_example}
-Require Import Heap.
-Check treesort.
-\end{coq_example}
-
-Let's now extract this function: 
-
-\begin{coq_example}
-Extraction Inline sort_rec is_heap_rec.
-Extraction NoInline list_to_heap.
-Extraction "heapsort" treesort.
-\end{coq_example}
-
-One more time, the {\tt Extraction Inline} and {\tt NoInline}
-directives are cosmetic. Without it, everything goes right, 
-but the output is less readable.
-Here is the produced file {\tt heapsort.ml}: 
-
-\begin{verbatim}
-type nat =
-  | O
-  | S of nat
-
-type 'a sig2 =
-  'a
-  (* singleton inductive, whose constructor was exist2 *)
-  
-type sumbool =
-  | Left
-  | Right
-
-type 'a list =
-  | Nil
-  | Cons of 'a * 'a list
-
-type 'a multiset =
-  'a -> nat
-  (* singleton inductive, whose constructor was Bag *)
-  
-type 'a merge_lem =
-  'a list
-  (* singleton inductive, whose constructor was merge_exist *)
-  
-(** val merge : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> sumbool) ->
-                'a1 list -> 'a1 list -> 'a1 merge_lem **)
-
-let rec merge leA_dec eqA_dec l1 l2 =
-  match l1 with
-    | Nil -> l2
-    | Cons (a, l) ->
-        let rec f = function
-          | Nil -> Cons (a, l)
-          | Cons (a0, l3) ->
-              (match leA_dec a a0 with
-                 | Left -> Cons (a,
-                     (merge leA_dec eqA_dec l (Cons (a0, l3))))
-                 | Right -> Cons (a0, (f l3)))
-        in f l2
-
-type 'a tree =
-  | Tree_Leaf
-  | Tree_Node of 'a * 'a tree * 'a tree
-
-type 'a insert_spec =
-  'a tree
-  (* singleton inductive, whose constructor was insert_exist *)
-  
-(** val insert : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> sumbool) ->
-                 'a1 tree -> 'a1 -> 'a1 insert_spec **)
-
-let rec insert leA_dec eqA_dec t a =
-  match t with
-    | Tree_Leaf -> Tree_Node (a, Tree_Leaf, Tree_Leaf)
-    | Tree_Node (a0, t0, t1) ->
-        let h3 = fun x -> insert leA_dec eqA_dec t0 x in
-        (match leA_dec a0 a with
-           | Left -> Tree_Node (a0, t1, (h3 a))
-           | Right -> Tree_Node (a, t1, (h3 a0)))
-
-type 'a build_heap =
-  'a tree
-  (* singleton inductive, whose constructor was heap_exist *)
-  
-(** val list_to_heap : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 ->
-                       sumbool) -> 'a1 list -> 'a1 build_heap **)
-
-let rec list_to_heap leA_dec eqA_dec = function
-  | Nil -> Tree_Leaf
-  | Cons (a, l0) ->
-      insert leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l0) a
-
-type 'a flat_spec =
-  'a list
-  (* singleton inductive, whose constructor was flat_exist *)
-  
-(** val heap_to_list : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 ->
-                       sumbool) -> 'a1 tree -> 'a1 flat_spec **)
-
-let rec heap_to_list leA_dec eqA_dec = function
-  | Tree_Leaf -> Nil
-  | Tree_Node (a, t0, t1) -> Cons (a,
-      (merge leA_dec eqA_dec (heap_to_list leA_dec eqA_dec t0)
-        (heap_to_list leA_dec eqA_dec t1)))
-
-(** val treesort : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> sumbool)
-                   -> 'a1 list -> 'a1 list sig2 **)
-
-let treesort leA_dec eqA_dec l =
-  heap_to_list leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l)
-
-\end{verbatim}
-
-Let's test it: 
-% Format.set_margin 72;;
-\begin{verbatim}
-# #use "heapsort.ml";;
-type sumbool = Left | Right
-type nat = O | S of nat
-type 'a tree = Tree_Leaf | Tree_Node of 'a * 'a tree * 'a tree
-type 'a list = Nil | Cons of 'a * 'a list
-val merge : 
-  ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list -> 'a list = <fun>
-val heap_to_list : 
-  ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a list = <fun>
-val insert : 
-  ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a -> 'a tree = <fun>
-val list_to_heap : 
-  ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a tree = <fun>
-val treesort : 
-  ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list = <fun>
+- : int * int = (11, 8)
 \end{verbatim}
 
-One can remark that the argument of {\tt treesort} corresponding to 
-{\tt eqAdec} is never used in the informative part of the terms, 
-only in the logical parts. So the extracted {\tt treesort} never use
-it, hence this {\tt 'b} argument. We will use {\tt ()} for this
-argument. Only remains the {\tt leAdec}
-argument (of type {\tt 'a -> 'a -> sumbool}) to really provide.
-
-\begin{verbatim}
-# let leAdec x y = if x <= y then Left else Right;;
-val leAdec : 'a -> 'a -> sumbool = <fun>
-# let rec listn = function 0 -> Nil
-                         | n -> Cons(Random.int 10000,listn (n-1));;
-val listn : int -> int list = <fun>
-# treesort leAdec () (listn 9);;
-- : int list = Cons (160, Cons (883, Cons (1874, Cons (3275, Cons 
-  (5392, Cons (7320, Cons (8512, Cons (9632, Cons (9876, Nil)))))))))
-\end{verbatim}
-
-Some tests on longer lists (10000 elements) show that the program is
-quite efficient for Caml code.
-
-
-\asubsection{The Standard Library} 
-
-As a test, we propose an automatic extraction of the 
-Standard Library of \Coq. In particular, we will find back the
-two previous examples, {\tt Euclid} and {\tt Heapsort}. 
-Go to directory {\tt plugins/extraction/test} of the sources of \Coq,
-and run commands: 
-\begin{verbatim}
-make tree; make
-\end{verbatim}
-This will extract all Standard Library files and compile them. 
-It is done via many {\tt Extraction Module}, with some customization
-(see subdirectory {\tt custom}).
-
-%The result of this extraction of the Standard Library can be browsed
-%at URL 
-%\begin{flushleft}
-%\url{http://www.lri.fr/~letouzey/extraction}.
-%\end{flushleft}
-                                
-%Reals theory is normally not extracted, since it is an axiomatic 
-%development. We propose nonetheless a dummy realization of those
-%axioms, to test, run: \\
-%
-%\mbox{\tt make reals}\\
-
-This test works also with Haskell. In the same directory, run:
-\begin{verbatim}
-make tree; make -f Makefile.haskell
-\end{verbatim}
-The haskell compiler currently used is {\tt hbc}.  Any other should
-also work, just adapt the {\tt Makefile.haskell}. In particular {\tt
- ghc} is known to work.
+Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now
+available via a mere {\tt Require Import ExtrOcamlIntConv} and then
+adding these functions to the list of functions to extract. This file
+{\tt ExtrOcamlIntConv.v} and some others in {\tt plugins/extraction/}
+are meant to help building concrete program via extraction.
 
 \asubsection{Extraction's horror museum}
 
 Some pathological examples of extraction are grouped in the file
-\begin{verbatim}
-plugins/extraction/test_extraction.v
-\end{verbatim}
-of the sources of \Coq.
+{\tt test-suite/success/extraction.v} of the sources of \Coq.
 
 \asubsection{Users' Contributions}
 
@@ -741,7 +538,7 @@ of the sources of \Coq.
  \end{itemize}
 
  Lannion, Rocq/HIGMAN and Lyon/CIRCUITS are a bit particular. They are 
- the only examples of developments where {\tt Obj.magic} are needed.
+ 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}.