1 files changed, 139 insertions, 0 deletions
diff --git a/contrib/extraction/README b/contrib/extraction/README
new file mode 100644
index 00000000..7350365e
--- /dev/null
+++ b/contrib/extraction/README
@@ -0,0 +1,139 @@
+
+Status of Extraction in Coq version 7.x
+======================================
+
+(* 22 jan 2003 : Updated for version 7.4 *)
+
+
+J.C. Filliâtre
+P. Letouzey
+
+
+
+Extraction code has been completely rewritten since version V6.3. 
+This work is still not finished, but most parts of it are already usable. 
+In consequence it is included in the Coq V7.0 final release. 
+But don't be mistaken: 
+
+	THIS WORK IS STILL EXPERIMENTAL !
+
+1) Principles 
+
+The main goal of the new extraction is to handle any Coq term, even 
+those upon sort Type, and to produce code that always compiles. 
+Thus it will never answer something like "Not an ML type", but rather
+a dummy term like the ML unit. 
+
+Translation between Coq and ML is based upon the following principles: 
+
+- Terms of sort Prop don't have any computational meaning, so they are
+merged into one ML term "__". This part is done according to P. Letouzey's 
+works (*) and (**).
+
+This dummy constant "__" used to be implemented by the unit (), but 
+we recently found that this constant might be applied in some cases. 
+So "__" is now in Ocaml a fixpoint that forgets its arguments: 
+
+           let __ = let rec f _ = Obj.repr f in Obj.repr f
+
+
+- Terms that are type schemes (i.e. something of type ( : )( : )...s with 
+s a sort ) don't have any ML counterpart at the term level, since they 
+are types transformers. In fact they do not have any computational
+meaning either. So we also merge them into that dummy term "__".
+
+- A Coq term gives a ML term or a ML type depending of its type: 
+type schemes will (try to) give ML types, and all other terms give ML terms.
+
+And the rest of the translation is (almost) straightforward: an inductive
+gives an inductive, etc...
+
+This gives ML code that have no special reason to typecheck, due 
+to the incompatibilities between Coq and ML typing systems. In fact
+most of the time everything goes right. For example, it is sufficient 
+to extract and compile everything in the "theories" directory 
+(cf test subdirectory).
+
+We now verify during extraction that the produced code is typecheckable, 
+and if it is not we insert unsafe type casting at critical points in the 
+code. For the moment, it is an Ocaml-only feature, using the "Obj.magic"
+function, but the same kind of trick will be soon made in Haskell.
+
+
+2) Differences with previous extraction (V6.3 and before)
+
+2.a) The pros 
+
+The ability to extract every Coq term, as explain in the previous 
+paragraph. 
+
+The ability to extract from a file an ML module (cf Extraction Module in the 
+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 the language of your choice: 
+Ocaml, Haskell, Scheme, or an Ocaml-like with Coq namings. 
+
+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 "__" as dummy arguments
+in functions. This denotes the rests of a proof part. The previous 
+extraction was able to remove them totally. The current implementation
+removes a good deal of them (more that in 7.0), but not all. 
+
+This problem is due to extraction upon Type.
+For example, let's take this pathological term: 
+	(if b then Set else Prop)  : Type
+The only way to know if this is an Set (to keep) or a Prop (to remove) 
+is to compute the boolean b, and we do not want to do that during 
+extraction. 
+
+There is no more "ML import" feature. You can compensate by using 
+Axioms, and then "Extract Constant ..." 
+
+3) Examples 
+
+The file "test-extraction.v" is made of some examples used while debugging.
+
+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 in Ocaml
+"make -f Makefile.haskell" to extract & compile in Haskell
+
+See also Reference Manual for explanation of extraction syntaxes
+and more examples. 
+
+
+(*):
+Exécution de termes de preuves: une nouvelle méthode d'extraction 
+pour le Calcul des Constructions Inductives, Pierre Letouzey,
+DEA thesis, 2000, 
+http://www.lri.fr/~letouzey/download/rapport_dea.ps.gz
+
+(**) 
+A New Extraction for Coq, Pierre Letouzey, 
+Types 2002 Post-Workshop Proceedings, to appear, 
+draft at http://www.lri.fr/~letouzey/download/extraction2002.ps.gz
+
+
+Any feedback is welcome: 
+Pierre.Letouzey@lri.fr
+Jean.Christophe.Filliatre@lri.fr
+
+
+
+
+
+
+
+
+
+
+