diff options
Diffstat (limited to 'plugins/extraction/CHANGES')
| -rw-r--r-- | plugins/extraction/CHANGES | 414 |
1 files changed, 414 insertions, 0 deletions
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES new file mode 100644 index 00000000..fbcd01a1 --- /dev/null +++ b/plugins/extraction/CHANGES @@ -0,0 +1,414 @@ +8.0 -> today + +See the main CHANGES file in the archive + + +7.4 -> 8.0 + +No revolution this time. Mostly "behind-the-scene" clean-up and bug-fixes, +but also a few steps toward a more user-friendly extraction: + +* syntax of extraction: +- The old (Recursive) Extraction Module M. + is now (Recursive) Extraction Library M. + The old name was misleading since this command only works with M being a + library M.v, and not a module produced by interactive command Module M. +- The other commands + Extraction foo. + Recursive Extraction foo bar. + Extraction "myfile.ml" foo bar. + now accept that foo can be a module name instead of just a constant name. + +* Support of type scheme axioms (i.e. axiom whose type is an arity + (x1:X1)...(xn:Xn)s with s a sort). For example: + + Axiom myprod : Set -> Set -> Set. + Extract Constant myprod "'a" "'b" => "'a * 'b". + Recursive Extraction myprod. + -------> type ('a,'b) myprod = 'a * 'b + +* More flexible support of axioms. When an axiom isn't realized via Extract + Constant before extraction, a warning is produced (instead of an error), + and the extracted code must be completed later by hand. To find what + needs to be completed, search for the following string: AXIOM TO BE REALIZED + +* Cosmetics: When extraction produces a file, it tells it. + +* (Experimental) It is allowed to extract under a opened interactive module + (but still outside sections). Feature to be used with caution. + +* A problem has been identified concerning .v files used as normal interactive + modules, like in + + <file A.v> + Definition foo :=O. + <End file A.v> + + <at toplevel> + Require A. + Module M:=A + Extraction M. + + I might try to support that in the future. In the meanwhile, the + current behaviour of extraction is to forbid this. + +* bug fixes: +- many concerning Records. +- a Stack Overflow with mutual inductive (PR#320) +- some optimizations have been removed since they were not type-safe: + For example if e has type: type 'x a = A + Then: match e with A -> A -----X----> e + To be investigated further. + + +7.3 -> 7.4 + +* The two main new features: + - Automatic generation of Obj.magic when the extracted code + in Ocaml is not directly typable. + - An experimental extraction of Coq's new modules to Ocaml modules. + +* Concerning those Obj.magic: + - The extraction now computes the expected type of any terms. Then + it compares it with the actual type of the produced code. And when + a mismatch is found, a Obj.magic is inserted. + + - As a rule, any extracted development that was compiling out of the box + should not contain any Obj.magic. At the other hand, generation of + Obj.magic is not optimized yet: there might be several of them at a place + were one would have been enough. + + - Examples of code needing those Obj.magic: + * plugins/extraction/test_extraction.v in the Coq source + * in the users' contributions: + Lannion + Lyon/CIRCUITS + Rocq/HIGMAN + + - As a side-effect of this Obj.magic feature, we now print the types + of the extracted terms, both in .ml files as commented documentation + and in interfaces .mli files + + - This feature hasn't been ported yet to Haskell. We are aware of + some unsafe casting functions like "unsafeCoerce" on some Haskell implems. + So it will eventually be done. + +* Concerning the extraction of Coq's new modules: + - Taking in account the new Coq's modules system has implied a *huge* + rewrite of most of the extraction code. + + - The extraction core (translation from Coq to an abstract mini-ML) + is now complete and fairly stable, and supports modules, modules type + and functors and all that stuff. + + - The ocaml pretty-print part, especially the renaming issue, is + clearly weaker, and certainly still contains bugs. + + - Nothing done for translating these Coq Modules to Haskell. + + - A temporary drawback of this module extraction implementation is that + efficiency (especially extraction speed) has been somehow neglected. + To improve ... + + - As an interesting side-effect, definitions are now printed according to + the user's original order. No more of this "dependency-correct but weird" + order. In particular realized axioms via Extract Constant are now at their + right place, and not at the beginning. + +* Other news: + + - Records are now printed using the Ocaml record syntax + + - Syntax output toward Scheme. Quite funny, but quite experimental and + not documented. I recommend using the bigloo compiler since it contains + natively some pattern matching. + + - the dummy constant "__" have changed. see README + + - a few bug-fixes (#191 and others) + +7.2 -> 7.3 + +* Improved documentation in the Reference Manual. + +* 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. This problem is dealt by +generating sufficient abstraction before the (). + + +* 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 bad news above have nearly no +impact... + + +* By the way there is no more "let prop = ()" in ocaml. Those () are +directly inlined. And in Haskell the dummy constant is now __ (two +underscore) and is defined by +__ = Prelude.error "Logical or arity value used" +This dummy constant should never be evaluated when computing an +informative value, thanks to the lazy strategy. Hence the error message. + + +* 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. + + +* By default, any recursive function associated with an inductive type +(foo_rec and foo_rect when foo is inductive type) will now be inlined +in extracted code. + + +* A few constants are explicitely declared to be inlined in extracted code. +For the moment there are: + 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. + +* There is now a web page showing the extraction of all standard theories: +http://www.lri.fr/~letouzey/extraction + + +7.1 -> 7.2 : + +* Syntax changes, see Documentation for more details: + +Set/Unset Extraction Optimize. + +Default is Set. This control all optimizations made on the ML terms +(mostly reduction of dummy beta/iota redexes, but also simplications on +Cases, etc). Put this option to Unset if you what a ML term as close as +possible to the Coq term. + +Set/Unset Extraction AutoInline. + +Default in Set, so by default, the extraction mechanism feels free to +inline the bodies of some defined constants, according to some heuristics +like size of bodies, useness of some arguments, etc. Those heuristics are +not always perfect, you may want to disable this feature, do it by Unset. + +Extraction Inline toto foo. +Extraction NoInline titi faa bor. + +In addition to the automatic inline feature, you can now tell precisely to +inline some more constants by the Extraction Inline command. Conversely, +you can forbid the inlining of some specific constants by automatic inlining. +Those two commands enable a precise control of what is inlined and what is not. + +Print Extraction Inline. + +Sum up the current state of the table recording the custom inlings +(Extraction (No)Inline). + +Reset Extraction Inline. + +Put the table recording the custom inlings back to empty. + +As a consequence, there is no more need for options inside the commands of +extraction: + +Extraction foo. +Recursive Extraction foo bar. +Extraction "file" foo bar. +Extraction Module Mymodule. +Recursive Extraction Module Mymodule. + +New: The last syntax extracts the module Mymodule and all the modules +it depends on. + +You can also try the Haskell versions (not tested yet): + +Haskell Extraction foo. +Haskell Recursive Extraction foo bar. +Haskell Extraction "file" foo bar. +Haskell Extraction Module Mymodule. +Haskell Recursive Extraction Module Mymodule. + +And there's still the realization syntax: + +Extract Constant coq_bla => "caml_bla". +Extract Inlined Constant coq_bla => "caml_bla". +Extract Inductive myinductive => mycamlind [my_caml_constr1 ... ]. + +Note that now, the Extract Inlined Constant command is sugar for an Extract +Constant followed by a Extraction Inline. So be careful with +Reset Extraction Inline. + + + +* Lot of works around optimization of produced code. Should make code more +readable. + +- fixpoint definitions : there should be no more stupid printings like + +let foo x = + let rec f x = + .... (f y) .... + in f x + +but rather + +let rec foo x = + .... (foo y) .... + +- generalized iota (in particular iota and permutation cases/cases): + +A generalized iota redex is a "Cases e of ...." where e is ok. +And the recursive predicate "ok" is given by: +e is ok if e is a Constructor or a Cases where all branches are ok. +In the case of generalized iota redex, it might be good idea to reduce it, +so we do it. +Example: + +match (match t with + O -> Left + | S n -> match n with + O -> Right + | S m -> Left) with + Left -> blabla +| Right -> bloblo + +After simplification, that gives: + +match t with + O -> blabla +| S n -> match n with + O -> bloblo + | S n -> blabla + +As shown on the example, code duplication can occur. In practice +it seems not to happen frequently. + +- "constant" case: +In V7.1 we used to simplify cases where all branches are the same. +In V7.2 we can simplify in addition terms like + cases e of + C1 x y -> f (C x y) + | C2 z -> f (C2 z) +If x y z don't occur in f, we can produce (f e). + +- permutation cases/fun: +extracted code has frequenty functions in branches of cases: + +let foo x = match x with + O -> fun _ -> .... + | S y -> fun _ -> .... + +the optimization consist in lifting the common "fun _ ->", and that gives + +let foo x _ = match x with + O -> ..... + | S y -> .... + + +* Some bug corrections (many thanks in particular to Michel Levy). + +* Testing in coq contributions: +If you are interested in extraction, you can look at the extraction tests +I'have put in the following coq contributions + +Bordeaux/Additions computation of fibonacci(2000) +Bordeaux/EXCEPTIONS multiplication using exception. +Bordeaux/SearchTrees list -> binary tree. maximum. +Dyade/BDDS boolean tautology checker. +Lyon/CIRCUITS multiplication via a modelization of a circuit. +Lyon/FIRING-SQUAD print the states of the firing squad. +Marseille/CIRCUITS compares integers via a modelization of a circuit. +Nancy/FOUnify unification of two first-order terms. +Rocq/ARITH/Chinese computation of the chinese remainder. +Rocq/COC small coc typechecker. (test by B. Barras, not by me) +Rocq/HIGMAN run the proof on one example. +Rocq/GRAPHS linear constraints checker in Z. +Sophia-Antipolis/Stalmarck boolean tautology checker. +Suresnes/BDD boolean tautology checker. + +Just do "make" in those contributions, the extraction test is integrated. +More tests will follow on more contributions. + + + +7.0 -> 7.1 : mostly bug corrections. No theoretical problems dealed with. + +* The semantics of Extract Constant changed: If you provide a extraction +for p by Extract Constant p => "0", your generated ML file will begin by +a let p = 0. The old semantics, which was to replace p everywhere by the +provided terms, is still available via the Extract Inlined Constant p => +"0" syntax. + + +* There are more optimizations applied to the generated code: +- identity cases: match e with P x y -> P x y | Q z -> Q z | ... +is simplified into e. Especially interesting with the sumbool terms: +there will be no more match ... with Left -> Left | Right -> Right + +- constant cases: match e with P x y -> c | Q z -> c | ... +is simplified into c as soon as x, y, z do not occur in c. +So no more match ... with Left -> Left | Right -> Left. + + +* the extraction at Toplevel (Extraction foo and Recursive Extraction foo), +which was only a development tool at the beginning, is now closer to +the real extraction to a file. In particular optimizations are done, +and constants like recursors ( ..._rec ) are expanded. + + +* the singleton optimization is now protected against circular type. +( Remind : this optimization is the one that simplify +type 'a sig = Exists of 'a into type 'a sig = 'a and +match e with (Exists c) -> d into let c = e in d ) + + +* Fixed one bug concerning casted code + + +* The inductives generated should now have always correct type-var list +('a,'b,'c...) + + +* Code cleanup until three days before release. Messing-up code +in the last three days before release. + + + + + + + +6.x -> 7.0 : Everything changed. See README |