maj V7.4

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

3 files changed, 145 insertions, 26 deletions

diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES
index 3a2a332245..506481bbc7 100644
--- a/contrib/extraction/CHANGES
+++ b/contrib/extraction/CHANGES
@@ -1,3 +1,81 @@
+7.3 -> 7.4
+
+* The two main new features: 
+  - Automatic generation of Obj.magic when the extracted code 
+  in Ocaml is not directly typable.
+  - A very limited and buggish extraction of Coq's new modules 
+  to Ocaml modules. 
+
+* Concerning those Obj.magic: 
+  - The extraction now computes the expected type of any terms. Then 
+  it compares it with the actual type of the produced code. And when 
+  a mismatch is found, a Obj.magic is inserted. 
+  
+  - As a rule, any extracted development that was compiling out of the box 
+  should not contain any Obj.magic. At the other hand, generation of 
+  Obj.magic is not optimized yet: there might be several of them at a place 
+  were one would have been enough. 
+  
+  - Examples of code needing those Obj.magic: 
+     * contrib/extraction/test_extraction.v in the Coq source
+     * in the users' contributions: 
+	Lannion
+	Lyon/CIRCUITS
+        Rocq/HIGMAN
+ 
+  - As a side-effect of this Obj.magic feature, we now print the types 
+  of the extracted terms, both in .ml files as commented documentation 
+  and in interfaces .mli files
+
+  - This feature hasn't been ported yet to Haskell. We are aware of 
+  some unsafe casting functions like "unsafeCoerce" on some Haskell implems.
+  So it will eventually be done.
+
+* Concerning the extraction of Coq's new modules: 
+  - Taking in account the new Coq's modules system has implied a *huge*
+  rewrite of most of the extraction code.
+
+  - the work is not complete, even if most of it is done. Today's 
+  status (22 jan 2003) is that we can extract *very* simple modules 
+  like 
+     
+    Module M. 
+    Definition t := O.
+    End M. 
+
+  which gives by Recursive Extraction t the following ocaml code: 
+
+    module M: 
+    sig 
+      val t : nat
+    end = 
+    struct 
+      (** val t : nat **)
+      let t = O
+    end
+
+  - unfortunately anything more complex (in particular functors)
+  tends to produce various bugs, the most common of them been 
+  "Anomaly: Search error. Please report."
+  Patches for those bugs will follow ... (I hope). Please be patient.
+
+  - As an interesting side-effect, definitions are now printed following
+  the user's original order. No more of this "dependency-correct but weird"
+  order. In particular realized axioms via Extract Constant are now at their 
+  right place, and not at the beginning. 
+
+* Other news: 
+  
+  - Records are now printed using the Ocaml record syntax
+ 
+  - Syntax output toward Scheme. Quite funny, but quite experimental and 
+  not documented. I recommend using the bigloo compiler since it contains 
+  natively some pattern matching.
+
+  - the dummy constant "__" have changed. see README
+
+  - a few bug-fixes (#191 and others)
+
 7.2 -> 7.3
 
 * Improved documentation in the Reference Manual.
@@ -74,7 +152,7 @@ Those constants does not match the auto-inlining criterion based on strictness.
 Of course, you can still overide this behaviour via some Extraction NoInline. 
 
 * There is now a web page showing the extraction of all standard theories: 
-http://www.lri.fr/~letouzey/extraction (* TODO mettre à jour *)
+http://www.lri.fr/~letouzey/extraction
 
 
 7.1 -> 7.2 :
diff --git a/contrib/extraction/README b/contrib/extraction/README
index 2fc077dbd6..7350365e7e 100644
--- a/contrib/extraction/README
+++ b/contrib/extraction/README
@@ -2,6 +2,9 @@
 Status of Extraction in Coq version 7.x
 ======================================
 
+(* 22 jan 2003 : Updated for version 7.4 *)
+
+
 J.C. Filliâtre
 P. Letouzey
 
@@ -24,16 +27,23 @@ 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 in one ML term "prop", which is for the moment the ML constant ().
-This part is done according to P. Letouzey's work (*).
+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: 
 
-- Terms that are arities (i.e. something of shape ( : )( : )...s with 
-s a sort ) don't have any ML counterpart, since they are types of 
-types transformers. We have also a special constant "arity" to 
-represent them if needed.
+           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: 
-a term of type an arity will give a ML type, and otherwise a ML term.
+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...
@@ -43,9 +53,12 @@ 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).
-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. 
+
+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)
 
@@ -61,7 +74,7 @@ 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 or an Ocaml-like with Coq namings. 
+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
@@ -69,11 +82,12 @@ expansion.
 
 2.b) The cons 
 
-The presence of some parasite "unit" or "prop" (now () in ocaml and __ in 
-Haskell) as dummy arguments
+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, but this is no more possible
-due to extraction upon Type.
+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) 
@@ -83,9 +97,6 @@ extraction.
 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 soon ...
-
 3) Examples 
 
 The file "test-extraction.v" is made of some examples used while debugging.
@@ -93,7 +104,8 @@ 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 
+"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. 
@@ -103,12 +115,25 @@ 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.eleves.ens.fr/home/letouzey/download/rapport_dea.ps.gz
-
+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
-coq@pauillac.inria.fr
+
+
+
+
+
+
+
+
+
+
+
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 7deda197ee..da064a3ad0 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -1,6 +1,22 @@
 
- 12. Ocaml typing => magic + cast.
+ 15. Finish extraction of modules (bugs with functors) 
 
- 13. Managing huge extraction (constructive FTA).
+ 16. Haskell : 
+     - equivalent of Obj.magic (unsafeCoerce ?) 
+     - look again at the syntax (make it independant of layout ...)  
+     - producing .hi files
+     - modules/modules types/functors in Haskell ?
 
- 14. Extract Constant do not work under a section.
+ 17. Scheme : 
+     - modular Scheme ? 
+
+ 18. Improve speed (profiling)
+
+ 19. Look again at those hugly renamings functions. 
+     Especially get rid of ML clashes like 
+   
+    let t = 0
+    module M = struct 
+       let t = 1 
+       let u = The.External.t (* ?? *)
+    end