diff options
Diffstat (limited to 'contrib/extraction/README')
-rw-r--r-- | contrib/extraction/README | 139 |
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 + + + + + + + + + + + |