maj doc extraction dans repertoire contrib/extraction

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

3 files changed, 31 insertions, 18 deletions

diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES
index 584fdcae4..3a2a33224 100644
--- a/contrib/extraction/CHANGES
+++ b/contrib/extraction/CHANGES
@@ -1,6 +1,6 @@
-7.2 -> 7.X  (* TODO put exact value *) 
+7.2 -> 7.3
 
-* Improved documentation. (* TODO *)
+* Improved documentation in the Reference Manual.
 
 * Theoretical bad news: 
 - a naughty example (see the end of test_extraction.v)
@@ -8,7 +8,8 @@ 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 *)
+may in some cases be applied to arguments. This problem is dealt by 
+generating sufficient abstraction before the (). 
 
 
 * Theoretical good news: 
@@ -17,9 +18,18 @@ 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 
+applications, etc). In particular the bad news above have nearly no 
 impact...
 
+
+* By the way there is no more "let prop = ()" in ocaml. Those () are
+directly inlined. And in Haskell the dummy constant is now __ (two
+underscore) and is defined by 
+__ = Prelude.error "Logical or arity value used"
+This dummy constant should never be evaluated when computing an
+informative value, thanks to the lazy strategy. Hence the error message. 
+
+
 * Syntax changes, see Documentation for details: 
 
 Extraction Language Ocaml.
@@ -49,12 +59,13 @@ instead of qualifying everywhere (A.foo), there are now some "open" at the
 beginning of files. Possible clashes are dealt with. 
 
 
+* By default, any recursive function associated with an inductive type 
+(foo_rec and foo_rect when foo is inductive type) will now be inlined 
+in extracted code. 
+
+
 * 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
diff --git a/contrib/extraction/README b/contrib/extraction/README
index 2fa44f2b9..2fc077dbd 100644
--- a/contrib/extraction/README
+++ b/contrib/extraction/README
@@ -60,14 +60,17 @@ documentation)
 You can have a taste of extraction directly at the toplevel by 
 using the "Extraction <ident>" or the "Recursive Extraction <ident>".
 This toplevel extraction was already there in V6.3, but was printing 
-Fw terms. It now prints in an Ocaml-like syntax.
+Fw terms. It now prints in the language of your choice: 
+Ocaml, Haskell or an Ocaml-like with Coq namings. 
 
-The optimization done on extracted code has been mostly ported between 
-V6.3 and V7, and in particular the mechanism of automatic expansion. 
+The optimization done on extracted code has been ported between 
+V6.3 and V7 and enhanced, and in particular the mechanism of automatic
+expansion. 
 
 2.b) The cons 
 
-The presence of some parasite "unit" or "prop" as dummy arguments
+The presence of some parasite "unit" or "prop" (now () in ocaml and __ in 
+Haskell) 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
 due to extraction upon Type.
@@ -92,6 +95,9 @@ Go there.
 "make tree" to make a local copy of the "theories" tree
 "make" to extract & compile most of the theories file 
 
+See also Reference Manual for explanation of extraction syntaxes
+and more examples. 
+
 
 (*):
 Exécution de termes de preuves: une nouvelle méthode d'extraction 
@@ -105,4 +111,4 @@ http://www.eleves.ens.fr/home/letouzey/download/rapport_dea.ps.gz
 Any feedback is welcome: 
 Pierre.Letouzey@lri.fr
 Jean.Christophe.Filliatre@lri.fr
-coq@pauillac.inria.fr
\ No newline at end of file
+coq@pauillac.inria.fr
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index b418ecf61..1957c4463 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -1,8 +1,4 @@
 
- 7. Eta expansion for resolving message: "variables cannot be generalized"
-
- 9. Doc!! (examples)
-	
  12. Ocaml typing => magic + cast.
 
- 13. Managing huge extraction (constructive FTA).
\ No newline at end of file
+ 13. Managing huge extraction (constructive FTA).