un peu de mise a jour de la doc extraction

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

3 files changed, 70 insertions, 17 deletions

diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES
index f14db4fa1..c20dcb5ca 100644
--- a/contrib/extraction/CHANGES
+++ b/contrib/extraction/CHANGES
@@ -1,3 +1,68 @@
+7.2 -> 7.X  (* TODO put exact value *) 
+
+* Improved documentation. (* TODO *)
+
+* Theoretical bad news: 
+- a naughty example (see the end of test_extraction.v)
+forced me to stop eliminating lambdas and arguments corresponding to 
+so-called "arity" in the general case. 
+
+- The dummy constant used in extraction ( let prop = () in ocaml ) 
+may in some cases be applied to arguments.  (* TODO say more *)
+
+
+* Theoretical good news: 
+- there is now a mechanism that remove useless prop/arity lambdas at the 
+top of function declarations. If your function had signature 
+nat -> prop -> nat in the previous extraction, it will now be nat -> nat. 
+So the extractions of common terms should look very much like the old 
+V6.2 one, except in some particular cases (functions as parameters, partial 
+applications, etc). In particular the first bad news above has nearly no 
+impact...
+
+* Syntax changes, see Documentation for details: 
+
+Extraction Language Ocaml.
+Extraction Language Haskell. 
+Extraction Language Toplevel.
+
+That fixes the target language of extraction. Default is Ocaml, even in the 
+coq toplevel: you can now do copy-paste from the coq toplevel without 
+renaming problems. Toplevel language is the ocaml pseudo-language used 
+previously used inside the coq toplevel: coq names are printed with the coq 
+way, i.e. with no renaming. 
+
+So there is no more particular commands for Haskell, like 
+Haskell Extraction "file" id. Just set your favourite language and go... 
+
+
+* Haskell extraction has been tested at last (and corrected...). 
+See specificities in Documentation. 
+
+
+* Extraction of CoInductive in Ocaml language is now correct: it uses the 
+Lazy.force and lazy features of Ocaml. 
+
+
+* Modular extraction in Ocaml is now far more readable: 
+instead of qualifying everywhere (A.foo), there are now some "open" at the 
+beginning of files. Possible clashes are dealt with. 
+
+
+* A few constants are explicitely declared to be inlined in extracted code. 
+For the moment there are: 
+	Specif.sigS_rect
+	Specif.sigS_rec 	
+	Datatypes.prod_rect 
+	Datatypes.prod_rec
+	Wf.Acc_rec
+	Wf.Acc_rect
+	Wf.well_founded_induction
+	Wf.well_founded_induction_type
+Those constants does not match the auto-inlining criterion based on strictness.
+Of course, you can still overide this behaviour via some Extraction NoInline. 
+
+
 7.1 -> 7.2 :
 
 * Syntax changes, see Documentation for more details: 
diff --git a/contrib/extraction/README b/contrib/extraction/README
index 98618afb5..2fa44f2b9 100644
--- a/contrib/extraction/README
+++ b/contrib/extraction/README
@@ -1,5 +1,5 @@
 
-Status of Extraction in Coq V7.0 final.
+Status of Extraction in Coq version 7.x
 ======================================
 
 J.C. Filliātre
@@ -47,7 +47,7 @@ The last feature (not yet implemented) is to ensure that the extracted
 code will typecheck. This will be done soon by adding some "Obj.magic"
 calls in the code. 
 
-2) Differences with previous extraction
+2) Differences with previous extraction (V6.3 and before)
 
 2.a) The pros 
 
@@ -67,10 +67,6 @@ V6.3 and V7, and in particular the mechanism of automatic expansion.
 
 2.b) The cons 
 
-The only language currently available is Ocaml. Haskell extraction 
-will be added as soon as possible. At the opposite, Caml Light is 
-definitely dead.
-
 The presence of some parasite "unit" or "prop" as dummy arguments
 in functions. This denotes the rests of a proof part. The previous 
 extraction was able to remove them totally, but this is no more possible
@@ -85,11 +81,7 @@ There is no more "ML import" feature. You can compensate by using
 Axioms, and then "Extract Constant ..." 
 
 Still no assurance of typechecking, since there is still no "Obj.magic"
-yet. Coming really soon ...
-
-Absolutely no benchmarking nor profiling nor optimizing has been 
-done on the new extraction code. 
-
+yet. Coming soon ...
 
 3) Examples 
 
@@ -99,7 +91,6 @@ In the subdirectory "test", you can test extraction on the Coq theories.
 Go there.
 "make tree" to make a local copy of the "theories" tree
 "make" to extract & compile most of the theories file 
-"make reals" to extract & compile a realization of the Reals axioms
 
 
 (*):
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 62c23142b..b418ecf61 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -1,11 +1,8 @@
 
- 5. Tester Haskell Syntax
-
  7. Eta expansion for resolving message: "variables cannot be generalized"
 
  9. Doc!! (examples)
-
- 11. test contribs
 	
- 12.  Ocaml typing => magic + cast.
+ 12. Ocaml typing => magic + cast.
 
+ 13. Managing huge extraction (constructive FTA).
\ No newline at end of file