Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
4.8 kB · 147 lines
at master
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148
Rocq Extraction ===============
What is it ?------------
The extraction is a mechanism that produces functional code(Ocaml/Haskell/Scheme) out of any Rocq terms (either programs orproofs).
Who did it ?------------
The current implementation (from version 7.0 up to now) has been doneby P. Letouzey during his PhD, helped by J.C. Filliâtre and supervisedby C. Paulin.
An earlier implementation (versions 6.x) was due to B. Werner andC. Paulin.
Where can we find more information ?------------------------------------
- Rocq Reference Manual includes a full chapter about extraction- P. Letouzey's PhD thesis [3] forms a complete document about both theory and implementation and test-cases of Rocq extraction- A more recent article [4] proposes a short overview of extraction- earlier documents [1] [2] may also be useful.
Why a complete re-implementation ?----------------------------------
Extraction code has been completely rewritten since version V6.3.
1) Principles
The main goal of the new extraction is to handle any Rocq 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 rathera dummy term like the ML unit.
Translation between Rocq and ML is based upon the following principles:
- Terms of sort Prop don't have any computational meaning, so they aremerged into one ML term "__". This part is done according to P. Letouzey's works [1] and [2].
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 computationalmeaning either. So we also merge them into that dummy term "__".
- A Rocq 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 inductivegives an inductive, etc...
This gives ML code that have no special reason to typecheck, due to the incompatibilities between Rocq and ML typing systems. In factmost of the time everything goes right.
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, with either "Obj.magic" in Ocaml or "unsafeCoerce" in Haskell.
2) Differences with previous extraction (V6.3 and before)
2.a) The pros
The ability to extract every Rocq term, as explain in the previous paragraph.
The ability to extract from a file an ML module (cf Extraction Library 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 or Scheme.
The optimization done on extracted code has been ported between V6.3 and V7 and enhanced, and in particular the mechanism of automaticexpansion.
2.b) The cons
The presence of some parasite "__" as dummy argumentsin functions. This denotes the rests of a proof part. The previous extraction was able to remove them totally. The current implementationremoves a good deal of them, 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) : TypeThe 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 ..."
[1]: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.pps.jussieu.fr/~letouzey/download/rapport_dea.ps.gz
[2]: A New Extraction for Coq, Pierre Letouzey, Types 2002 Post-Workshop Proceedings. http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz
[3]: Programmation fonctionnelle certifiée: l'extraction de programmesdans l'assistant Coq. Pierre Letouzey, PhD thesis, 2004.http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.ps.gzhttp://www.pps.jussieu.fr/~letouzey/download/these_letouzey_English.ps.gz
[4]:Coq Extraction, An overview. Pierre Letouzey. CiE2008.http://www.pps.jussieu.fr/~letouzey/download/letouzey_extr_cie08.pdf