1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
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
|
