diff options
Diffstat (limited to 'contrib/extraction')
-rw-r--r-- | contrib/extraction/CHANGES | 65 | ||||
-rw-r--r-- | contrib/extraction/README | 15 | ||||
-rw-r--r-- | contrib/extraction/TODO | 7 |
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 |