diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | contrib/extraction/CHANGES | 42 | ||||
| -rw-r--r-- | contrib/extraction/TODO | 2 |
3 files changed, 16 insertions, 31 deletions
@@ -111,8 +111,7 @@ Extraction (See details in contrib/extraction/CHANGES and README): - An experimental Scheme extraction is provided. - Concerning Ocaml, extracted code is now ensured to always type-check, thanks to automatic inserting of Obj.magic. -- "early" (read: "still bugged") version of an extraction compatible with - Coq's new modules. +- Experimental extraction of Coq new modules to Ocaml modules. Miscellaneous diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES index 506481bbc7..b4805e6fa1 100644 --- a/contrib/extraction/CHANGES +++ b/contrib/extraction/CHANGES @@ -3,8 +3,7 @@ * 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. + - An experimental extraction of Coq's new modules to Ocaml modules. * Concerning those Obj.magic: - The extraction now computes the expected type of any terms. Then @@ -35,31 +34,20 @@ - 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 extraction core (translation from Coq to an abstract mini-ML) + is now complete and fairly stable, and supports modules, modules type + and functors and all that stuff. + + - The ocaml pretty-print part, especially the renaming issue, is + clearly weaker, and certainly still contains bugs. + + - Nothing done for translating these Coq Modules to Haskell. + + - A temporary drawback of this module extraction implementation is that + efficiency (especially extraction speed) has been somehow neglected. + To improve ... + + - As an interesting side-effect, definitions are now printed according to 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. diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO index da064a3ad0..47e69acfe0 100644 --- a/contrib/extraction/TODO +++ b/contrib/extraction/TODO @@ -1,6 +1,4 @@ - 15. Finish extraction of modules (bugs with functors) - 16. Haskell : - equivalent of Obj.magic (unsafeCoerce ?) - look again at the syntax (make it independant of layout ...) |