3
No revolution this time. Mostly "behind-the-scene" clean-up and bug-fixes,
4
but also a few steps toward a more user-friendly extraction:
6
* syntax of extraction:
7
- The old (Recursive) Extraction Module M.
8
is now (Recursive) Extraction Library M.
9
The old name was misleading since this command only works with M being a
10
library M.v, and not a module produced by interactive command Module M.
13
Recursive Extraction foo bar.
14
Extraction "myfile.ml" foo bar.
15
now accept that foo can be a module name instead of just a constant name.
17
* Support of type scheme axioms (i.e. axiom whose type is an arity
18
(x1:X1)...(xn:Xn)s with s a sort). For example:
20
Axiom myprod : Set -> Set -> Set.
21
Extract Constant myprod "'a" "'b" => "'a * 'b".
22
Recursive Extraction myprod.
23
-------> type ('a,'b) myprod = 'a * 'b
25
* More flexible support of axioms. When an axiom isn't realized via Extract
26
Constant before extraction, a warning is produced (instead of an error),
27
and the extracted code must be completed later by hand. To find what
28
needs to be completed, search for the following string: AXIOM TO BE REALIZED
30
* Cosmetics: When extraction produces a file, it tells it.
32
* (Experimental) It is allowed to extract under a opened interactive module
33
(but still outside sections). Feature to be used with caution.
35
* A problem has been identified concerning .v files used as normal interactive
47
I might try to support that in the future. In the meanwhile, the
48
current behaviour of extraction is to forbid this.
51
- many concerning Records.
52
- a Stack Overflow with mutual inductive (PR#320)
53
- some optimizations have been removed since they were not type-safe:
54
For example if e has type: type 'x a = A
55
Then: match e with A -> A -----X----> e
56
To be investigated further.
61
* The two main new features:
62
- Automatic generation of Obj.magic when the extracted code
63
in Ocaml is not directly typable.
64
- An experimental extraction of Coq's new modules to Ocaml modules.
66
* Concerning those Obj.magic:
67
- The extraction now computes the expected type of any terms. Then
68
it compares it with the actual type of the produced code. And when
69
a mismatch is found, a Obj.magic is inserted.
71
- As a rule, any extracted development that was compiling out of the box
72
should not contain any Obj.magic. At the other hand, generation of
73
Obj.magic is not optimized yet: there might be several of them at a place
74
were one would have been enough.
76
- Examples of code needing those Obj.magic:
77
* contrib/extraction/test_extraction.v in the Coq source
78
* in the users' contributions:
83
- As a side-effect of this Obj.magic feature, we now print the types
84
of the extracted terms, both in .ml files as commented documentation
85
and in interfaces .mli files
87
- This feature hasn't been ported yet to Haskell. We are aware of
88
some unsafe casting functions like "unsafeCoerce" on some Haskell implems.
89
So it will eventually be done.
91
* Concerning the extraction of Coq's new modules:
92
- Taking in account the new Coq's modules system has implied a *huge*
93
rewrite of most of the extraction code.
95
- The extraction core (translation from Coq to an abstract mini-ML)
96
is now complete and fairly stable, and supports modules, modules type
97
and functors and all that stuff.
99
- The ocaml pretty-print part, especially the renaming issue, is
100
clearly weaker, and certainly still contains bugs.
102
- Nothing done for translating these Coq Modules to Haskell.
104
- A temporary drawback of this module extraction implementation is that
105
efficiency (especially extraction speed) has been somehow neglected.
108
- As an interesting side-effect, definitions are now printed according to
109
the user's original order. No more of this "dependency-correct but weird"
110
order. In particular realized axioms via Extract Constant are now at their
111
right place, and not at the beginning.
115
- Records are now printed using the Ocaml record syntax
117
- Syntax output toward Scheme. Quite funny, but quite experimental and
118
not documented. I recommend using the bigloo compiler since it contains
119
natively some pattern matching.
121
- the dummy constant "__" have changed. see README
123
- a few bug-fixes (#191 and others)
127
* Improved documentation in the Reference Manual.
129
* Theoretical bad news:
130
- a naughty example (see the end of test_extraction.v)
131
forced me to stop eliminating lambdas and arguments corresponding to
132
so-called "arity" in the general case.
134
- The dummy constant used in extraction ( let prop = () in ocaml )
135
may in some cases be applied to arguments. This problem is dealt by
136
generating sufficient abstraction before the ().
139
* Theoretical good news:
140
- there is now a mechanism that remove useless prop/arity lambdas at the
141
top of function declarations. If your function had signature
142
nat -> prop -> nat in the previous extraction, it will now be nat -> nat.
143
So the extractions of common terms should look very much like the old
144
V6.2 one, except in some particular cases (functions as parameters, partial
145
applications, etc). In particular the bad news above have nearly no
149
* By the way there is no more "let prop = ()" in ocaml. Those () are
150
directly inlined. And in Haskell the dummy constant is now __ (two
151
underscore) and is defined by
152
__ = Prelude.error "Logical or arity value used"
153
This dummy constant should never be evaluated when computing an
154
informative value, thanks to the lazy strategy. Hence the error message.
157
* Syntax changes, see Documentation for details:
159
Extraction Language Ocaml.
160
Extraction Language Haskell.
161
Extraction Language Toplevel.
163
That fixes the target language of extraction. Default is Ocaml, even in the
164
coq toplevel: you can now do copy-paste from the coq toplevel without
165
renaming problems. Toplevel language is the ocaml pseudo-language used
166
previously used inside the coq toplevel: coq names are printed with the coq
167
way, i.e. with no renaming.
169
So there is no more particular commands for Haskell, like
170
Haskell Extraction "file" id. Just set your favourite language and go...
173
* Haskell extraction has been tested at last (and corrected...).
174
See specificities in Documentation.
177
* Extraction of CoInductive in Ocaml language is now correct: it uses the
178
Lazy.force and lazy features of Ocaml.
181
* Modular extraction in Ocaml is now far more readable:
182
instead of qualifying everywhere (A.foo), there are now some "open" at the
183
beginning of files. Possible clashes are dealt with.
186
* By default, any recursive function associated with an inductive type
187
(foo_rec and foo_rect when foo is inductive type) will now be inlined
191
* A few constants are explicitely declared to be inlined in extracted code.
192
For the moment there are:
195
Wf.well_founded_induction
196
Wf.well_founded_induction_type
197
Those constants does not match the auto-inlining criterion based on strictness.
198
Of course, you can still overide this behaviour via some Extraction NoInline.
200
* There is now a web page showing the extraction of all standard theories:
201
http://www.lri.fr/~letouzey/extraction
206
* Syntax changes, see Documentation for more details:
208
Set/Unset Extraction Optimize.
210
Default is Set. This control all optimizations made on the ML terms
211
(mostly reduction of dummy beta/iota redexes, but also simplications on
212
Cases, etc). Put this option to Unset if you what a ML term as close as
213
possible to the Coq term.
215
Set/Unset Extraction AutoInline.
217
Default in Set, so by default, the extraction mechanism feels free to
218
inline the bodies of some defined constants, according to some heuristics
219
like size of bodies, useness of some arguments, etc. Those heuristics are
220
not always perfect, you may want to disable this feature, do it by Unset.
222
Extraction Inline toto foo.
223
Extraction NoInline titi faa bor.
225
In addition to the automatic inline feature, you can now tell precisely to
226
inline some more constants by the Extraction Inline command. Conversely,
227
you can forbid the inlining of some specific constants by automatic inlining.
228
Those two commands enable a precise control of what is inlined and what is not.
230
Print Extraction Inline.
232
Sum up the current state of the table recording the custom inlings
233
(Extraction (No)Inline).
235
Reset Extraction Inline.
237
Put the table recording the custom inlings back to empty.
239
As a consequence, there is no more need for options inside the commands of
243
Recursive Extraction foo bar.
244
Extraction "file" foo bar.
245
Extraction Module Mymodule.
246
Recursive Extraction Module Mymodule.
248
New: The last syntax extracts the module Mymodule and all the modules
251
You can also try the Haskell versions (not tested yet):
253
Haskell Extraction foo.
254
Haskell Recursive Extraction foo bar.
255
Haskell Extraction "file" foo bar.
256
Haskell Extraction Module Mymodule.
257
Haskell Recursive Extraction Module Mymodule.
259
And there's still the realization syntax:
261
Extract Constant coq_bla => "caml_bla".
262
Extract Inlined Constant coq_bla => "caml_bla".
263
Extract Inductive myinductive => mycamlind [my_caml_constr1 ... ].
265
Note that now, the Extract Inlined Constant command is sugar for an Extract
266
Constant followed by a Extraction Inline. So be careful with
267
Reset Extraction Inline.
271
* Lot of works around optimization of produced code. Should make code more
274
- fixpoint definitions : there should be no more stupid printings like
286
- generalized iota (in particular iota and permutation cases/cases):
288
A generalized iota redex is a "Cases e of ...." where e is ok.
289
And the recursive predicate "ok" is given by:
290
e is ok if e is a Constructor or a Cases where all branches are ok.
291
In the case of generalized iota redex, it might be good idea to reduce it,
297
| S n -> match n with
303
After simplification, that gives:
307
| S n -> match n with
311
As shown on the example, code duplication can occur. In practice
312
it seems not to happen frequently.
315
In V7.1 we used to simplify cases where all branches are the same.
316
In V7.2 we can simplify in addition terms like
320
If x y z don't occur in f, we can produce (f e).
322
- permutation cases/fun:
323
extracted code has frequenty functions in branches of cases:
325
let foo x = match x with
327
| S y -> fun _ -> ....
329
the optimization consist in lifting the common "fun _ ->", and that gives
331
let foo x _ = match x with
336
* Some bug corrections (many thanks in particular to Michel Levy).
338
* Testing in coq contributions:
339
If you are interested in extraction, you can look at the extraction tests
340
I'have put in the following coq contributions
342
Bordeaux/Additions computation of fibonacci(2000)
343
Bordeaux/EXCEPTIONS multiplication using exception.
344
Bordeaux/SearchTrees list -> binary tree. maximum.
345
Dyade/BDDS boolean tautology checker.
346
Lyon/CIRCUITS multiplication via a modelization of a circuit.
347
Lyon/FIRING-SQUAD print the states of the firing squad.
348
Marseille/CIRCUITS compares integers via a modelization of a circuit.
349
Nancy/FOUnify unification of two first-order terms.
350
Rocq/ARITH/Chinese computation of the chinese remainder.
351
Rocq/COC small coc typechecker. (test by B. Barras, not by me)
352
Rocq/HIGMAN run the proof on one example.
353
Rocq/GRAPHS linear constraints checker in Z.
354
Sophia-Antipolis/Stalmarck boolean tautology checker.
355
Suresnes/BDD boolean tautology checker.
357
Just do "make" in those contributions, the extraction test is integrated.
358
More tests will follow on more contributions.
362
7.0 -> 7.1 : mostly bug corrections. No theoretical problems dealed with.
364
* The semantics of Extract Constant changed: If you provide a extraction
365
for p by Extract Constant p => "0", your generated ML file will begin by
366
a let p = 0. The old semantics, which was to replace p everywhere by the
367
provided terms, is still available via the Extract Inlined Constant p =>
371
* There are more optimizations applied to the generated code:
372
- identity cases: match e with P x y -> P x y | Q z -> Q z | ...
373
is simplified into e. Especially interesting with the sumbool terms:
374
there will be no more match ... with Left -> Left | Right -> Right
376
- constant cases: match e with P x y -> c | Q z -> c | ...
377
is simplified into c as soon as x, y, z do not occur in c.
378
So no more match ... with Left -> Left | Right -> Left.
381
* the extraction at Toplevel (Extraction foo and Recursive Extraction foo),
382
which was only a development tool at the beginning, is now closer to
383
the real extraction to a file. In particular optimizations are done,
384
and constants like recursors ( ..._rec ) are expanded.
387
* the singleton optimization is now protected against circular type.
388
( Remind : this optimization is the one that simplify
389
type 'a sig = Exists of 'a into type 'a sig = 'a and
390
match e with (Exists c) -> d into let c = e in d )
393
* Fixed one bug concerning casted code
396
* The inductives generated should now have always correct type-var list
400
* Code cleanup until three days before release. Messing-up code
401
in the last three days before release.
409
6.x -> 7.0 : Everything changed. See README
added
removed
contrib/extraction/CHANGES
