diff options
Diffstat (limited to 'plugins/extraction')
33 files changed, 7973 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 diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v new file mode 100644 index 00000000..f0135221 --- /dev/null +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Extraction to Ocaml : use of basic Ocaml types *) + +Extract Inductive bool => bool [ true false ]. +Extract Inductive option => option [ Some None ]. +Extract Inductive unit => unit [ "()" ]. +Extract Inductive list => list [ "[]" "( :: )" ]. +Extract Inductive prod => "( * )" [ "" ]. + +(** NB: The "" above is a hack, but produce nicer code than "(,)" *) + +(** Mapping sumbool to bool and sumor to option is not always nicer, + but it helps when realizing stuff like [lt_eq_lt_dec] *) + +Extract Inductive sumbool => bool [ true false ]. +Extract Inductive sumor => option [ Some None ]. + +(** Restore lazyness of andb, orb. + NB: without these Extract Constant, andb/orb would be inlined + by extraction in order to have lazyness, producing inelegant + (if ... then ... else false) and (if ... then true else ...). +*) + +Extract Inlined Constant andb => "(&&)". +Extract Inlined Constant orb => "(||)". + diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v new file mode 100644 index 00000000..b4490545 --- /dev/null +++ b/plugins/extraction/ExtrOcamlBigIntConv.v @@ -0,0 +1,108 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Extraction to Ocaml: conversion from/to [big_int] *) + +(** NB: The extracted code should be linked with [nums.cm(x)a] + from ocaml's stdlib and with the wrapper [big.ml] that + simlifies the use of [Big_int] (it could be found in the sources + of Coq). *) + +Require Import Arith ZArith. + +Parameter bigint : Type. +Parameter bigint_zero : bigint. +Parameter bigint_succ : bigint -> bigint. +Parameter bigint_opp : bigint -> bigint. +Parameter bigint_twice : bigint -> bigint. + +Extract Inlined Constant bigint => "Big.big_int". +Extract Inlined Constant bigint_zero => "Big.zero". +Extract Inlined Constant bigint_succ => "Big.succ". +Extract Inlined Constant bigint_opp => "Big.opp". +Extract Inlined Constant bigint_twice => "Big.double". + +Definition bigint_of_nat : nat -> bigint := + (fix loop acc n := + match n with + | O => acc + | S n => loop (bigint_succ acc) n + end) bigint_zero. + +Fixpoint bigint_of_pos p := + match p with + | xH => bigint_succ bigint_zero + | xO p => bigint_twice (bigint_of_pos p) + | xI p => bigint_succ (bigint_twice (bigint_of_pos p)) + end. + +Fixpoint bigint_of_z z := + match z with + | Z0 => bigint_zero + | Zpos p => bigint_of_pos p + | Zneg p => bigint_opp (bigint_of_pos p) + end. + +Fixpoint bigint_of_n n := + match n with + | N0 => bigint_zero + | Npos p => bigint_of_pos p + end. + +(** NB: as for [pred] or [minus], [nat_of_bigint], [n_of_bigint] and + [pos_of_bigint] are total and return zero (resp. one) for + non-positive inputs. *) + +Parameter bigint_natlike_rec : forall A, A -> (A->A) -> bigint -> A. +Extract Constant bigint_natlike_rec => "Big.nat_rec". + +Definition nat_of_bigint : bigint -> nat := bigint_natlike_rec _ O S. + +Parameter bigint_poslike_rec : forall A, (A->A) -> (A->A) -> A -> bigint -> A. +Extract Constant bigint_poslike_rec => "Big.positive_rec". + +Definition pos_of_bigint : bigint -> positive := bigint_poslike_rec _ xI xO xH. + +Parameter bigint_zlike_case : + forall A, A -> (bigint->A) -> (bigint->A) -> bigint -> A. +Extract Constant bigint_zlike_case => "Big.z_rec". + +Definition z_of_bigint : bigint -> Z := + bigint_zlike_case _ Z0 (fun i => Zpos (pos_of_bigint i)) + (fun i => Zneg (pos_of_bigint i)). + +Definition n_of_bigint : bigint -> N := + bigint_zlike_case _ N0 (fun i => Npos (pos_of_bigint i)) (fun _ => N0). + +(* Tests: + +Definition small := 1234%nat. +Definition big := 12345678901234567890%positive. + +Definition nat_0 := nat_of_bigint (bigint_of_nat 0). +Definition nat_1 := nat_of_bigint (bigint_of_nat small). +Definition pos_1 := pos_of_bigint (bigint_of_pos 1). +Definition pos_2 := pos_of_bigint (bigint_of_pos big). +Definition n_0 := n_of_bigint (bigint_of_n 0). +Definition n_1 := n_of_bigint (bigint_of_n 1). +Definition n_2 := n_of_bigint (bigint_of_n (Npos big)). +Definition z_0 := z_of_bigint (bigint_of_z 0). +Definition z_1 := z_of_bigint (bigint_of_z 1). +Definition z_2 := z_of_bigint (bigint_of_z (Zpos big)). +Definition z_m1 := z_of_bigint (bigint_of_z (-1)). +Definition z_m2 := z_of_bigint (bigint_of_z (Zneg big)). + +Definition test := + (nat_0, nat_1, pos_1, pos_2, n_0, n_1, n_2, z_0, z_1, z_2, z_m1, z_m2). +Definition check := + (O, small, xH, big, 0%N, 1%N, Npos big, 0%Z, 1%Z, Zpos big, (-1)%Z, Zneg big). + +Extraction "/tmp/test.ml" check test. + +... and we check that test=check +*)
\ No newline at end of file diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v new file mode 100644 index 00000000..e729d9ca --- /dev/null +++ b/plugins/extraction/ExtrOcamlIntConv.v @@ -0,0 +1,97 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Extraction to Ocaml: conversion from/to [int] + + Nota: no check that [int] values aren't generating overflows *) + +Require Import Arith ZArith. + +Parameter int : Type. +Parameter int_zero : int. +Parameter int_succ : int -> int. +Parameter int_opp : int -> int. +Parameter int_twice : int -> int. + +Extract Inlined Constant int => int. +Extract Inlined Constant int_zero => "0". +Extract Inlined Constant int_succ => "succ". +Extract Inlined Constant int_opp => "-". +Extract Inlined Constant int_twice => "2 *". + +Definition int_of_nat : nat -> int := + (fix loop acc n := + match n with + | O => acc + | S n => loop (int_succ acc) n + end) int_zero. + +Fixpoint int_of_pos p := + match p with + | xH => int_succ int_zero + | xO p => int_twice (int_of_pos p) + | xI p => int_succ (int_twice (int_of_pos p)) + end. + +Fixpoint int_of_z z := + match z with + | Z0 => int_zero + | Zpos p => int_of_pos p + | Zneg p => int_opp (int_of_pos p) + end. + +Fixpoint int_of_n n := + match n with + | N0 => int_zero + | Npos p => int_of_pos p + end. + +(** NB: as for [pred] or [minus], [nat_of_int], [n_of_int] and + [pos_of_int] are total and return zero (resp. one) for + non-positive inputs. *) + +Parameter int_natlike_rec : forall A, A -> (A->A) -> int -> A. +Extract Constant int_natlike_rec => +"fun fO fS -> + let rec loop acc i = if i <= 0 then acc else loop (fS acc) (i-1) + in loop fO". + +Definition nat_of_int : int -> nat := int_natlike_rec _ O S. + +Parameter int_poslike_rec : forall A, A -> (A->A) -> (A->A) -> int -> A. +Extract Constant int_poslike_rec => +"fun f1 f2x f2x1 -> + let rec loop i = if i <= 1 then f1 else + if i land 1 = 0 then f2x (loop (i lsr 1)) else f2x1 (loop (i lsr 1)) + in loop". + +Definition pos_of_int : int -> positive := int_poslike_rec _ xH xO xI. + +Parameter int_zlike_case : forall A, A -> (int->A) -> (int->A) -> int -> A. +Extract Constant int_zlike_case => +"fun f0 fpos fneg i -> + if i = 0 then f0 else if i>0 then fpos i else fneg (-i)". + +Definition z_of_int : int -> Z := + int_zlike_case _ Z0 (fun i => Zpos (pos_of_int i)) + (fun i => Zneg (pos_of_int i)). + +Definition n_of_int : int -> N := + int_zlike_case _ N0 (fun i => Npos (pos_of_int i)) (fun _ => N0). + +(** Warning: [z_of_int] is currently wrong for Ocaml's [min_int], + since [min_int] has no positive opposite ([-min_int = min_int]). +*) + +(* +Extraction "/tmp/test.ml" + nat_of_int int_of_nat + pos_of_int int_of_pos + z_of_int int_of_z + n_of_int int_of_n. +*)
\ No newline at end of file diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v new file mode 100644 index 00000000..491e0258 --- /dev/null +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Extraction of [nat] into Ocaml's [big_int] *) + +Require Import Arith Even Div2 EqNat MinMax Euclid. +Require Import ExtrOcamlBasic. + +(** NB: The extracted code should be linked with [nums.cm(x)a] + from ocaml's stdlib and with the wrapper [big.ml] that + simlifies the use of [Big_int] (it could be found in the sources + of Coq). *) + +(** Disclaimer: trying to obtain efficient certified programs + by extracting [nat] into [big_int] isn't necessarily a good idea. + See comments in [ExtrOcamlNatInt.v]. +*) + + +(** Mapping of [nat] into [big_int]. The last string corresponds to + a [nat_case], see documentation of [Extract Inductive]. *) + +Extract Inductive nat => "Big.big_int" [ "Big.zero" "Big.succ" ] + "Big.nat_case". + +(** Efficient (but uncertified) versions for usual [nat] functions *) + +Extract Constant plus => "Big.add". +Extract Constant mult => "Big.mult". +Extract Constant pred => "fun n -> Big.max Big.zero (Big.pred n)". +Extract Constant minus => "fun n m -> Big.max Big.zero (Big.sub n m)". +Extract Constant max => "Big.max". +Extract Constant min => "Big.min". +Extract Constant nat_beq => "Big.eq". +Extract Constant EqNat.beq_nat => "Big.eq". +Extract Constant EqNat.eq_nat_decide => "Big.eq". + +Extract Constant Peano_dec.eq_nat_dec => "Big.eq". + +Extract Constant Compare_dec.nat_compare => + "Big.compare_case Eq Lt Gt". + +Extract Constant Compare_dec.leb => "Big.le". +Extract Constant Compare_dec.le_lt_dec => "Big.le". +Extract Constant Compare_dec.lt_eq_lt_dec => + "Big.compare_case (Some false) (Some true) None". + +Extract Constant Even.even_odd_dec => + "fun n -> Big.sign (Big.mod n Big.two) = 0". +Extract Constant Div2.div2 => "fun n -> Big.div n Big.two". + +Extract Inductive Euclid.diveucl => "(Big.big_int * Big.big_int)" [""]. +Extract Constant Euclid.eucl_dev => "fun n m -> Big.quomod m n". +Extract Constant Euclid.quotient => "fun n m -> Big.div m n". +Extract Constant Euclid.modulo => "fun n m -> Big.modulo m n". + +(* +Require Import Euclid. +Definition test n m (H:m>0) := + let (q,r,_,_) := eucl_dev m H n in + nat_compare n (q*m+r). + +Extraction "/tmp/test.ml" test fact pred minus max min Div2.div2. +*) diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v new file mode 100644 index 00000000..fe03bc60 --- /dev/null +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -0,0 +1,75 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Extraction of [nat] into Ocaml's [int] *) + +Require Import Arith Even Div2 EqNat MinMax Euclid. +Require Import ExtrOcamlBasic. + +(** Disclaimer: trying to obtain efficient certified programs + by extracting [nat] into [int] is definitively *not* a good idea: + + - Since [int] is bounded while [nat] is (theoretically) infinite, + you have to make sure by yourself that your program will not + manipulate numbers greater than [max_int]. Otherwise you should + consider the translation of [nat] into [big_int]. + + - Moreover, the mere translation of [nat] into [int] does not + change the complexity of functions. For instance, [mult] stays + quadratic. To mitigate this, we propose here a few efficient (but + uncertified) realizers for some common functions over [nat]. + + This file is hence provided mainly for testing / prototyping + purpose. For serious use of numbers in extracted programs, + you are advised to use either coq advanced representations + (positive, Z, N, BigN, BigZ) or modular/axiomatic representation. +*) + + +(** Mapping of [nat] into [int]. The last string corresponds to + a [nat_case], see documentation of [Extract Inductive]. *) + +Extract Inductive nat => int [ "0" "succ" ] + "(fun fO fS n -> if n=0 then fO () else fS (n-1))". + +(** Efficient (but uncertified) versions for usual [nat] functions *) + +Extract Constant plus => "(+)". +Extract Constant pred => "fun n -> max 0 (n-1)". +Extract Constant minus => "fun n m -> max 0 (n-m)". +Extract Constant mult => "( * )". +Extract Inlined Constant max => max. +Extract Inlined Constant min => min. +Extract Inlined Constant nat_beq => "(=)". +Extract Inlined Constant EqNat.beq_nat => "(=)". +Extract Inlined Constant EqNat.eq_nat_decide => "(=)". + +Extract Inlined Constant Peano_dec.eq_nat_dec => "(=)". + +Extract Constant Compare_dec.nat_compare => + "fun n m -> if n=m then Eq else if n<m then Lt else Gt". +Extract Inlined Constant Compare_dec.leb => "(<=)". +Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)". +Extract Constant Compare_dec.lt_eq_lt_dec => + "fun n m -> if n>m then None else Some (n<m)". + +Extract Constant Even.even_odd_dec => "fun n -> n mod 2 = 0". +Extract Constant Div2.div2 => "fun n -> n/2". + +Extract Inductive Euclid.diveucl => "(int * int)" [ "" ]. +Extract Constant Euclid.eucl_dev => "fun n m -> (m/n, m mod n)". +Extract Constant Euclid.quotient => "fun n m -> m/n". +Extract Constant Euclid.modulo => "fun n m -> m mod n". + +(* +Definition test n m (H:m>0) := + let (q,r,_,_) := eucl_dev m H n in + nat_compare n (q*m+r). + +Recursive Extraction test fact. +*)
\ No newline at end of file diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v new file mode 100644 index 00000000..3fcd01b0 --- /dev/null +++ b/plugins/extraction/ExtrOcamlString.v @@ -0,0 +1,38 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Extraction to Ocaml : special handling of ascii and strings *) + +Require Import Ascii String. + +Extract Inductive ascii => char +[ +"(* If this appears, you're using Ascii internals. Please don't *) + (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> + let f b i = if b then 1 lsl i else 0 in + Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))" +] +"(* If this appears, you're using Ascii internals. Please don't *) + (fun f c -> + let n = Char.code c in + let h i = (n land (1 lsl i)) <> 0 in + f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". + +Extract Constant zero => "'\000'". +Extract Constant one => "'\001'". +Extract Constant shift => + "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". + +Extract Inlined Constant ascii_dec => "(=)". + +Extract Inductive string => "char list" [ "[]" "(::)" ]. + +(* +Definition test := "ceci est un test"%string. +Recursive Extraction test Ascii.zero Ascii.one. +*) diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v new file mode 100644 index 00000000..08f43d3f --- /dev/null +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -0,0 +1,85 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *) + +Require Import ZArith NArith ZOdiv_def. +Require Import ExtrOcamlBasic. + +(** NB: The extracted code should be linked with [nums.cm(x)a] + from ocaml's stdlib and with the wrapper [big.ml] that + simlifies the use of [Big_int] (it could be found in the sources + of Coq). *) + +(** Disclaimer: trying to obtain efficient certified programs + by extracting [Z] into [big_int] isn't necessarily a good idea. + See the Disclaimer in [ExtrOcamlNatInt]. *) + +(** Mapping of [positive], [Z], [N] into [big_int]. The last strings + emulate the matching, see documentation of [Extract Inductive]. *) + +Extract Inductive positive => "Big.big_int" + [ "Big.doubleplusone" "Big.double" "Big.one" ] "Big.positive_case". + +Extract Inductive Z => "Big.big_int" + [ "Big.zero" "" "Big.opp" ] "Big.z_case". + +Extract Inductive N => "Big.big_int" + [ "Big.zero" "" ] "Big.n_case". + +(** Nota: the "" above is used as an identity function "(fun p->p)" *) + +(** Efficient (but uncertified) versions for usual functions *) + +Extract Constant Pplus => "Big.add". +Extract Constant Psucc => "Big.succ". +Extract Constant Ppred => "fun n -> Big.max Big.one (Big.pred n)". +Extract Constant Pminus => "fun n m -> Big.max Big.one (Big.sub n m)". +Extract Constant Pmult => "Big.mult". +Extract Constant Pmin => "Big.min". +Extract Constant Pmax => "Big.max". +Extract Constant Pcompare => + "fun x y c -> Big.compare_case c Lt Gt x y". + +Extract Constant Nplus => "Big.add". +Extract Constant Nsucc => "Big.succ". +Extract Constant Npred => "fun n -> Big.max Big.zero (Big.pred n)". +Extract Constant Nminus => "fun n m -> Big.max Big.zero (Big.sub n m)". +Extract Constant Nmult => "Big.mult". +Extract Constant Nmin => "Big.min". +Extract Constant Nmax => "Big.max". +Extract Constant Ndiv => + "fun a b -> if Big.eq b Big.zero then Big.zero else Big.div a b". +Extract Constant Nmod => + "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b". +Extract Constant Ncompare => "Big.compare_case Eq Lt Gt". + +Extract Constant Zplus => "Big.add". +Extract Constant Zsucc => "Big.succ". +Extract Constant Zpred => "Big.pred". +Extract Constant Zminus => "Big.sub". +Extract Constant Zmult => "Big.mult". +Extract Constant Zopp => "Big.opp". +Extract Constant Zabs => "Big.abs". +Extract Constant Zmin => "Big.min". +Extract Constant Zmax => "Big.max". +Extract Constant Zcompare => "Big.compare_case Eq Lt Gt". + +Extract Constant Z_of_N => "fun p -> p". +Extract Constant Zabs_N => "Big.abs". + +(** Zdiv and Zmod are quite complex to define in terms of (/) and (mod). + For the moment we don't even try *) + +(** Test: +Require Import ZArith NArith. + +Extraction "/tmp/test.ml" + Pplus Ppred Pminus Pmult Pcompare Npred Nminus Ndiv Nmod Ncompare + Zplus Zmult BinInt.Zcompare Z_of_N Zabs_N Zdiv.Zdiv Zmod. +*) diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v new file mode 100644 index 00000000..d3ea7372 --- /dev/null +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Extraction of [positive], [N] and [Z] into Ocaml's [int] *) + +Require Import ZArith NArith ZOdiv_def. +Require Import ExtrOcamlBasic. + +(** Disclaimer: trying to obtain efficient certified programs + by extracting [Z] into [int] is definitively *not* a good idea. + See the Disclaimer in [ExtrOcamlNatInt]. *) + +(** Mapping of [positive], [Z], [N] into [int]. The last strings + emulate the matching, see documentation of [Extract Inductive]. *) + +Extract Inductive positive => int +[ "(fun p->1+2*p)" "(fun p->2*p)" "1" ] +"(fun f2p1 f2p f1 p -> + if p<=1 then f1 () else if p mod 2 = 0 then f2p (p/2) else f2p1 (p/2))". + +Extract Inductive Z => int [ "0" "" "(~-)" ] +"(fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))". + +Extract Inductive N => int [ "0" "" ] +"(fun f0 fp n -> if n=0 then f0 () else fp n)". + +(** Nota: the "" above is used as an identity function "(fun p->p)" *) + +(** Efficient (but uncertified) versions for usual functions *) + +Extract Constant Pplus => "(+)". +Extract Constant Psucc => "succ". +Extract Constant Ppred => "fun n -> max 1 (n-1)". +Extract Constant Pminus => "fun n m -> max 1 (n-m)". +Extract Constant Pmult => "( * )". +Extract Constant Pmin => "min". +Extract Constant Pmax => "max". +Extract Constant Pcompare => + "fun x y c -> if x=y then c else if x<y then Lt else Gt". + + +Extract Constant Nplus => "(+)". +Extract Constant Nsucc => "succ". +Extract Constant Npred => "fun n -> max 0 (n-1)". +Extract Constant Nminus => "fun n m -> max 0 (n-m)". +Extract Constant Nmult => "( * )". +Extract Constant Nmin => "min". +Extract Constant Nmax => "max". +Extract Constant Ndiv => "fun a b -> if b=0 then 0 else a/b". +Extract Constant Nmod => "fun a b -> if b=0 then a else a mod b". +Extract Constant Ncompare => + "fun x y -> if x=y then Eq else if x<y then Lt else Gt". + + +Extract Constant Zplus => "(+)". +Extract Constant Zsucc => "succ". +Extract Constant Zpred => "pred". +Extract Constant Zminus => "(-)". +Extract Constant Zmult => "( * )". +Extract Constant Zopp => "(~-)". +Extract Constant Zabs => "abs". +Extract Constant Zmin => "min". +Extract Constant Zmax => "max". +Extract Constant Zcompare => + "fun x y -> if x=y then Eq else if x<y then Lt else Gt". + +Extract Constant Z_of_N => "fun p -> p". +Extract Constant Zabs_N => "abs". + +(** Zdiv and Zmod are quite complex to define in terms of (/) and (mod). + For the moment we don't even try *) + + diff --git a/plugins/extraction/README b/plugins/extraction/README new file mode 100644 index 00000000..64c871fd --- /dev/null +++ b/plugins/extraction/README @@ -0,0 +1,147 @@ + + Coq Extraction + ============== + + +What is it ? +------------ + +The extraction is a mechanism allowing to produce functional code +(Ocaml/Haskell/Scheme) out of any Coq terms (either programs or +proofs). + +Who did it ? +------------ + +The current implementation (from version 7.0 up to now) has been done +by P. Letouzey during his PhD, helped by J.C. Filliâtre and supervised +by C. Paulin. + +An earlier implementation (versions 6.x) was due to B. Werner and +C. Paulin. + + +Where can we find more information ? +------------------------------------ + +- Coq 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 Coq-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 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 [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 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. + +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 Coq 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 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, 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 ..." + + + + + +[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 programmes +dans l'assistant Coq. Pierre Letouzey, PhD thesis, 2004. +http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.ps.gz +http://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 + + + + + + + + diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml new file mode 100644 index 00000000..9a5bf56b --- /dev/null +++ b/plugins/extraction/big.ml @@ -0,0 +1,154 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** [Big] : a wrapper around ocaml [Big_int] with nicer names, + and a few extraction-specific constructions *) + +(** To be linked with [nums.(cma|cmxa)] *) + +open Big_int + +type big_int = Big_int.big_int + (** The type of big integers. *) + +let zero = zero_big_int + (** The big integer [0]. *) +let one = unit_big_int + (** The big integer [1]. *) +let two = big_int_of_int 2 + (** The big integer [2]. *) + +(** {6 Arithmetic operations} *) + +let opp = minus_big_int + (** Unary negation. *) +let abs = abs_big_int + (** Absolute value. *) +let add = add_big_int + (** Addition. *) +let succ = succ_big_int + (** Successor (add 1). *) +let add_int = add_int_big_int + (** Addition of a small integer to a big integer. *) +let sub = sub_big_int + (** Subtraction. *) +let pred = pred_big_int + (** Predecessor (subtract 1). *) +let mult = mult_big_int + (** Multiplication of two big integers. *) +let mult_int = mult_int_big_int + (** Multiplication of a big integer by a small integer *) +let square = square_big_int + (** Return the square of the given big integer *) +let sqrt = sqrt_big_int + (** [sqrt_big_int a] returns the integer square root of [a], + that is, the largest big integer [r] such that [r * r <= a]. + Raise [Invalid_argument] if [a] is negative. *) +let quomod = quomod_big_int + (** Euclidean division of two big integers. + The first part of the result is the quotient, + the second part is the remainder. + Writing [(q,r) = quomod_big_int a b], we have + [a = q * b + r] and [0 <= r < |b|]. + Raise [Division_by_zero] if the divisor is zero. *) +let div = div_big_int + (** Euclidean quotient of two big integers. + This is the first result [q] of [quomod_big_int] (see above). *) +let modulo = mod_big_int + (** Euclidean modulus of two big integers. + This is the second result [r] of [quomod_big_int] (see above). *) +let gcd = gcd_big_int + (** Greatest common divisor of two big integers. *) +let power = power_big_int_positive_big_int + (** Exponentiation functions. Return the big integer + representing the first argument [a] raised to the power [b] + (the second argument). Depending + on the function, [a] and [b] can be either small integers + or big integers. Raise [Invalid_argument] if [b] is negative. *) + +(** {6 Comparisons and tests} *) + +let sign = sign_big_int + (** Return [0] if the given big integer is zero, + [1] if it is positive, and [-1] if it is negative. *) +let compare = compare_big_int + (** [compare_big_int a b] returns [0] if [a] and [b] are equal, + [1] if [a] is greater than [b], and [-1] if [a] is smaller + than [b]. *) +let eq = eq_big_int +let le = le_big_int +let ge = ge_big_int +let lt = lt_big_int +let gt = gt_big_int + (** Usual boolean comparisons between two big integers. *) +let max = max_big_int + (** Return the greater of its two arguments. *) +let min = min_big_int + (** Return the smaller of its two arguments. *) + +(** {6 Conversions to and from strings} *) + +let to_string = string_of_big_int + (** Return the string representation of the given big integer, + in decimal (base 10). *) +let of_string = big_int_of_string + (** Convert a string to a big integer, in decimal. + The string consists of an optional [-] or [+] sign, + followed by one or several decimal digits. *) + +(** {6 Conversions to and from other numerical types} *) + +let of_int = big_int_of_int + (** Convert a small integer to a big integer. *) +let is_int = is_int_big_int + (** Test whether the given big integer is small enough to + be representable as a small integer (type [int]) + without loss of precision. On a 32-bit platform, + [is_int_big_int a] returns [true] if and only if + [a] is between 2{^30} and 2{^30}-1. On a 64-bit platform, + [is_int_big_int a] returns [true] if and only if + [a] is between -2{^62} and 2{^62}-1. *) +let to_int = int_of_big_int + (** Convert a big integer to a small integer (type [int]). + Raises [Failure "int_of_big_int"] if the big integer + is not representable as a small integer. *) + +(** Functions used by extraction *) + +let double x = mult_int 2 x +let doubleplusone x = succ (double x) + +let nat_case fO fS n = if sign n <= 0 then fO () else fS (pred n) + +let positive_case f2p1 f2p f1 p = + if le p one then f1 () else + let (q,r) = quomod p two in if eq r zero then f2p q else f2p1 q + +let n_case fO fp n = if sign n <= 0 then fO () else fp n + +let z_case fO fp fn z = + let s = sign z in + if s = 0 then fO () else if s > 0 then fp z else fn (opp z) + +let compare_case e l g x y = + let s = compare x y in if s = 0 then e else if s<0 then l else g + +let nat_rec fO fS = + let rec loop acc n = + if sign n <= 0 then acc else loop (fS acc) (pred n) + in loop fO + +let positive_rec f2p1 f2p f1 = + let rec loop n = + if le n one then f1 + else + let (q,r) = quomod n two in + if eq r zero then f2p (loop q) else f2p1 (loop q) + in loop + +let z_rec fO fp fn = z_case (fun _ -> fO) fp fn diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml new file mode 100644 index 00000000..1db1c786 --- /dev/null +++ b/plugins/extraction/common.ml @@ -0,0 +1,535 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Pp +open Util +open Names +open Term +open Declarations +open Namegen +open Nameops +open Libnames +open Table +open Miniml +open Mlutil +open Modutil +open Mod_subst + +let string_of_id id = + let s = Names.string_of_id id in + for i = 0 to String.length s - 2 do + if s.[i] = '_' && s.[i+1] = '_' then warning_id s + done; + ascii_of_ident s + +let is_mp_bound = function MPbound _ -> true | _ -> false + +(*s Some pretty-print utility functions. *) + +let pp_par par st = if par then str "(" ++ st ++ str ")" else st + +let pp_apply st par args = match args with + | [] -> st + | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args)) + +let pr_binding = function + | [] -> mt () + | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l + +let fnl2 () = fnl () ++ fnl () + +let space_if = function true -> str " " | false -> mt () + +let sec_space_if = function true -> spc () | false -> mt () + +let is_digit = function + | '0'..'9' -> true + | _ -> false + +let begins_with_CoqXX s = + let n = String.length s in + n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' && + let i = ref 3 in + try while !i < n do + if s.[!i] = '_' then i:=n (*Stop*) + else if is_digit s.[!i] then incr i + else raise Not_found + done; true + with Not_found -> false + +let unquote s = + if lang () <> Scheme then s + else + let s = String.copy s in + for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done; + s + +let rec qualify delim = function + | [] -> assert false + | [s] -> s + | ""::l -> qualify delim l + | s::l -> s^delim^(qualify delim l) + +let dottify = qualify "." +let pseudo_qualify = qualify "__" + +(*s Uppercase/lowercase renamings. *) + +let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false +let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false + +let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id)) +let uppercase_id id = + let s = string_of_id id in + assert (s<>""); + if s.[0] = '_' then id_of_string ("Coq_"^s) + else id_of_string (String.capitalize s) + +type kind = Term | Type | Cons | Mod + +let upperkind = function + | Type -> lang () = Haskell + | Term -> false + | Cons | Mod -> true + +let kindcase_id k id = + if upperkind k then uppercase_id id else lowercase_id id + +(*s de Bruijn environments for programs *) + +type env = identifier list * Idset.t + +(*s Generic renaming issues for local variable names. *) + +let rec rename_id id avoid = + if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id + +let rec rename_vars avoid = function + | [] -> + [], avoid + | id :: idl when id == dummy_name -> + (* we don't rename dummy binders *) + let (idl', avoid') = rename_vars avoid idl in + (id :: idl', avoid') + | id :: idl -> + let (idl, avoid) = rename_vars avoid idl in + let id = rename_id (lowercase_id id) avoid in + (id :: idl, Idset.add id avoid) + +let rename_tvars avoid l = + let rec rename avoid = function + | [] -> [],avoid + | id :: idl -> + let id = rename_id (lowercase_id id) avoid in + let idl, avoid = rename (Idset.add id avoid) idl in + (id :: idl, avoid) in + fst (rename avoid l) + +let push_vars ids (db,avoid) = + let ids',avoid' = rename_vars avoid ids in + ids', (ids' @ db, avoid') + +let get_db_name n (db,_) = + let id = List.nth db (pred n) in + if id = dummy_name then id_of_string "__" else id + + +(*S Renamings of global objects. *) + +(*s Tables of global renamings *) + +let register_cleanup, do_cleanup = + let funs = ref [] in + (fun f -> funs:=f::!funs), (fun () -> List.iter (fun f -> f ()) !funs) + +type phase = Pre | Impl | Intf + +let set_phase, get_phase = + let ph = ref Impl in ((:=) ph), (fun () -> !ph) + +let set_keywords, get_keywords = + let k = ref Idset.empty in + ((:=) k), (fun () -> !k) + +let add_global_ids, get_global_ids = + let ids = ref Idset.empty in + register_cleanup (fun () -> ids := get_keywords ()); + let add s = ids := Idset.add s !ids + and get () = !ids + in (add,get) + +let empty_env () = [], get_global_ids () + +let mktable autoclean = + let h = Hashtbl.create 97 in + if autoclean then register_cleanup (fun () -> Hashtbl.clear h); + (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h) + +(* A table recording objects in the first level of all MPfile *) + +let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content = + mktable false + +(*s The list of external modules that will be opened initially *) + +let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear = + let m = ref MPset.empty in + let add mp = m:=MPset.add mp !m + and mem mp = MPset.mem mp !m + and list () = MPset.elements !m + and clear () = m:=MPset.empty + in + register_cleanup clear; + (add,mem,list,clear) + +(*s List of module parameters that we should alpha-rename *) + +let params_ren_add, params_ren_mem = + let m = ref MPset.empty in + let add mp = m:=MPset.add mp !m + and mem mp = MPset.mem mp !m + and clear () = m:=MPset.empty + in + register_cleanup clear; + (add,mem) + +(*s table indicating the visible horizon at a precise moment, + i.e. the stack of structures we are inside. + + - The sequence of [mp] parts should have the following form: + a [MPfile] at the beginning, and then more and more [MPdot] + over this [MPfile], or [MPbound] when inside the type of a + module parameter. + + - the [params] are the [MPbound] when [mp] is a functor, + the innermost [MPbound] coming first in the list. + + - The [content] part is used to record all the names already + seen at this level. +*) + +type visible_layer = { mp : module_path; + params : module_path list; + content : ((kind*string),label) Hashtbl.t } + +let pop_visible, push_visible, get_visible = + let vis = ref [] in + register_cleanup (fun () -> vis := []); + let pop () = + let v = List.hd !vis in + (* we save the 1st-level-content of MPfile for later use *) + if get_phase () = Impl && modular () && is_modfile v.mp + then add_mpfiles_content v.mp v.content; + vis := List.tl !vis + and push mp mps = + vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis + and get () = !vis + in (pop,push,get) + +let get_visible_mps () = List.map (function v -> v.mp) (get_visible ()) +let top_visible () = match get_visible () with [] -> assert false | v::_ -> v +let top_visible_mp () = (top_visible ()).mp +let add_visible ks l = Hashtbl.add (top_visible ()).content ks l + +(* table of local module wrappers used to provide non-ambiguous names *) + +let add_duplicate, check_duplicate = + let index = ref 0 and dups = ref Gmap.empty in + register_cleanup (fun () -> index := 0; dups := Gmap.empty); + let add mp l = + incr index; + let ren = "Coq__" ^ string_of_int (!index) in + dups := Gmap.add (mp,l) ren !dups + and check mp l = Gmap.find (mp, l) !dups + in (add,check) + +type reset_kind = AllButExternal | Everything + +let reset_renaming_tables flag = + do_cleanup (); + if flag = Everything then clear_mpfiles_content () + +(*S Renaming functions *) + +(* This function creates from [id] a correct uppercase/lowercase identifier. + This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes + with previous [Coq_id] variable, these prefixes are duplicated if already + existing. *) + +let modular_rename k id = + let s = string_of_id id in + let prefix,is_ok = + if upperkind k then "Coq_",is_upper else "coq_",is_lower + in + if not (is_ok s) || + (Idset.mem id (get_keywords ())) || + (String.length s >= 4 && String.sub s 0 4 = prefix) + then prefix ^ s + else s + +(*s For monolithic extraction, first-level modules might have to be renamed + with unique numbers *) + +let modfstlev_rename = + let add_prefixes,get_prefixes,_ = mktable true in + fun l -> + let coqid = id_of_string "Coq" in + let id = id_of_label l in + try + let coqset = get_prefixes id in + let nextcoq = next_ident_away coqid coqset in + add_prefixes id (nextcoq::coqset); + (string_of_id nextcoq)^"_"^(string_of_id id) + with Not_found -> + let s = string_of_id id in + if is_lower s || begins_with_CoqXX s then + (add_prefixes id [coqid]; "Coq_"^s) + else + (add_prefixes id []; s) + +(*s Creating renaming for a [module_path] : first, the real function ... *) + +let rec mp_renaming_fun mp = match mp with + | _ when not (modular ()) && at_toplevel mp -> [""] + | MPdot (mp,l) -> + let lmp = mp_renaming mp in + if lmp = [""] then (modfstlev_rename l)::lmp + else (modular_rename Mod (id_of_label l))::lmp + | MPbound mbid -> + let s = modular_rename Mod (id_of_mbid mbid) in + if not (params_ren_mem mp) then [s] + else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i] + | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *) + | MPfile _ -> + assert (get_phase () = Pre); + let current_mpfile = (list_last (get_visible ())).mp in + if mp <> current_mpfile then mpfiles_add mp; + [string_of_modfile mp] + +(* ... and its version using a cache *) + +and mp_renaming = + let add,get,_ = mktable true in + fun x -> + try if is_mp_bound (base_mp x) then raise Not_found; get x + with Not_found -> let y = mp_renaming_fun x in add x y; y + +(*s Renamings creation for a [global_reference]: we build its fully-qualified + name in a [string list] form (head is the short name). *) + +let ref_renaming_fun (k,r) = + let mp = modpath_of_r r in + let l = mp_renaming mp in + let l = if lang () <> Ocaml && not (modular ()) then [""] else l in + let s = + if l = [""] (* this happens only at toplevel of the monolithic case *) + then + let globs = Idset.elements (get_global_ids ()) in + let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in + string_of_id id + else modular_rename k (safe_basename_of_global r) + in + add_global_ids (id_of_string s); + s::l + +(* Cached version of the last function *) + +let ref_renaming = + let add,get,_ = mktable true in + fun x -> + try if is_mp_bound (base_mp (modpath_of_r (snd x))) then raise Not_found; get x + with Not_found -> let y = ref_renaming_fun x in add x y; y + +(* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k] + can be printed as [s] in the current context of visible + modules. More precisely, we check if there exists a + visible [mp] that contains [s]. + The verification stops if we encounter [mp=mp0]. *) + +let rec clash mem mp0 ks = function + | [] -> false + | mp :: _ when mp = mp0 -> false + | mp :: _ when mem mp ks -> true + | _ :: mpl -> clash mem mp0 ks mpl + +let mpfiles_clash mp0 ks = + clash (fun mp -> Hashtbl.mem (get_mpfiles_content mp)) mp0 ks + (List.rev (mpfiles_list ())) + +let rec params_lookup mp0 ks = function + | [] -> false + | param :: _ when mp0 = param -> true + | param :: params -> + if ks = (Mod, List.hd (mp_renaming param)) then params_ren_add param; + params_lookup mp0 ks params + +let visible_clash mp0 ks = + let rec clash = function + | [] -> false + | v :: _ when v.mp = mp0 -> false + | v :: vis -> + let b = Hashtbl.mem v.content ks in + if b && not (is_mp_bound mp0) then true + else begin + if b then params_ren_add mp0; + if params_lookup mp0 ks v.params then false + else clash vis + end + in clash (get_visible ()) + +(* Same, but with verbose output (and mp0 shouldn't be a MPbound) *) + +let visible_clash_dbg mp0 ks = + let rec clash = function + | [] -> None + | v :: _ when v.mp = mp0 -> None + | v :: vis -> + try Some (v.mp,Hashtbl.find v.content ks) + with Not_found -> + if params_lookup mp0 ks v.params then None + else clash vis + in clash (get_visible ()) + +(* After the 1st pass, we can decide which modules will be opened initially *) + +let opened_libraries () = + if not (modular ()) then [] + else + let used = mpfiles_list () in + let rec check_elsewhere avoid = function + | [] -> [] + | mp :: mpl -> + let clash s = Hashtbl.mem (get_mpfiles_content mp) (Mod,s) in + if List.exists clash avoid + then check_elsewhere avoid mpl + else mp :: check_elsewhere (string_of_modfile mp :: avoid) mpl + in + let opened = check_elsewhere [] used in + mpfiles_clear (); + List.iter mpfiles_add opened; + opened + +(*s On-the-fly qualification issues for both monolithic or modular extraction. *) + +(* First, a function that factorize the printing of both [global_reference] + and module names for ocaml. When [k=Mod] then [olab=None], otherwise it + contains the label of the reference to print. + [rls] is the string list giving the qualified name, short name at the end. + Invariant: [List.length rls >= 2], simpler situations are handled elsewhere. *) + +(* In Coq, we can qualify [M.t] even if we are inside [M], but in Ocaml we + cannot do that. So, if [t] gets hidden and we need a long name for it, + we duplicate the _definition_ of t in a Coq__XXX module, and similarly + for a sub-module [M.N] *) + +let pp_duplicate k' prefix mp rls olab = + let rls', lbl = + if k'<>Mod then + (* Here rls=[s], the ref to print is <prefix>.<s>, and olab<>None *) + rls, Option.get olab + else + (* Here rls=s::rls', we search the label for s inside mp *) + List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp + in + try dottify (check_duplicate prefix lbl :: rls') + with Not_found -> + assert (get_phase () = Pre); (* otherwise it's too late *) + add_duplicate prefix lbl; dottify rls + +let fstlev_ks k = function + | [] -> assert false + | [s] -> k,s + | s::_ -> Mod,s + +(* [pp_ocaml_local] : [mp] has something in common with [top_visible ()] + but isn't equal to it *) + +let pp_ocaml_local k prefix mp rls olab = + (* what is the largest prefix of [mp] that belongs to [visible]? *) + assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *) + let rls' = list_skipn (mp_length prefix) rls in + let k's = fstlev_ks k rls' in + (* Reference r / module path mp is of the form [<prefix>.s.<...>]. *) + if not (visible_clash prefix k's) then dottify rls' + else pp_duplicate (fst k's) prefix mp rls' olab + +(* [pp_ocaml_bound] : [mp] starts with a [MPbound], and we are not inside + (i.e. we are not printing the type of the module parameter) *) + +let pp_ocaml_bound base rls = + (* clash with a MPbound will be detected and fixed by renaming this MPbound *) + if get_phase () = Pre then ignore (visible_clash base (Mod,List.hd rls)); + dottify rls + +(* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *) + +let pp_ocaml_extern k base rls = match rls with + | [] | [_] -> assert false + | base_s :: rls' -> + let k's = fstlev_ks k rls' in + if modular () && (mpfiles_mem base) && + (not (mpfiles_clash base k's)) && + (not (visible_clash base k's)) + then (* Standard situation of an object in another file: *) + (* Thanks to the "open" of this file we remove its name *) + dottify rls' + else match visible_clash_dbg base (Mod,base_s) with + | None -> dottify rls + | Some (mp,l) -> error_module_clash base (MPdot (mp,l)) + +(* [pp_ocaml_gen] : choosing between [pp_ocaml_extern] or [pp_ocaml_extern] *) + +let pp_ocaml_gen k mp rls olab = + match common_prefix_from_list mp (get_visible_mps ()) with + | Some prefix -> pp_ocaml_local k prefix mp rls olab + | None -> + let base = base_mp mp in + if is_mp_bound base then pp_ocaml_bound base rls + else pp_ocaml_extern k base rls + +(* For Haskell, things are simplier: we have removed (almost) all structures *) + +let pp_haskell_gen k mp rls = match rls with + | [] -> assert false + | s::rls' -> + (if base_mp mp <> top_visible_mp () then s ^ "." else "") ^ + (if upperkind k then "" else "_") ^ pseudo_qualify rls' + +(* Main name printing function for a reference *) + +let pp_global k r = + let ls = ref_renaming (k,r) in + assert (List.length ls > 1); + let s = List.hd ls in + let mp,_,l = repr_of_r r in + if mp = top_visible_mp () then + (* simpliest situation: definition of r (or use in the same context) *) + (* we update the visible environment *) + (add_visible (k,s) l; unquote s) + else + let rls = List.rev ls in (* for what come next it's easier this way *) + match lang () with + | Scheme -> unquote s (* no modular Scheme extraction... *) + | Haskell -> if modular () then pp_haskell_gen k mp rls else s + | Ocaml -> pp_ocaml_gen k mp rls (Some l) + +(* The next function is used only in Ocaml extraction...*) + +let pp_module mp = + let ls = mp_renaming mp in + match mp with + | MPdot (mp0,l) when mp0 = top_visible_mp () -> + (* simpliest situation: definition of mp (or use in the same context) *) + (* we update the visible environment *) + let s = List.hd ls in + add_visible (Mod,s) l; s + | _ -> pp_ocaml_gen Mod mp (List.rev ls) None + + diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli new file mode 100644 index 00000000..93be15d1 --- /dev/null +++ b/plugins/extraction/common.mli @@ -0,0 +1,59 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Names +open Libnames +open Miniml +open Mlutil +open Pp + +val fnl2 : unit -> std_ppcmds +val space_if : bool -> std_ppcmds +val sec_space_if : bool -> std_ppcmds + +val pp_par : bool -> std_ppcmds -> std_ppcmds +val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds +val pr_binding : identifier list -> std_ppcmds + +val rename_id : identifier -> Idset.t -> identifier + +type env = identifier list * Idset.t +val empty_env : unit -> env + +val rename_vars: Idset.t -> identifier list -> env +val rename_tvars: Idset.t -> identifier list -> identifier list +val push_vars : identifier list -> env -> identifier list * env +val get_db_name : int -> env -> identifier + +type phase = Pre | Impl | Intf + +val set_phase : phase -> unit +val get_phase : unit -> phase + +val opened_libraries : unit -> module_path list + +type kind = Term | Type | Cons | Mod + +val pp_global : kind -> global_reference -> string +val pp_module : module_path -> string + +val top_visible_mp : unit -> module_path +(* In [push_visible], the [module_path list] corresponds to + module parameters, the innermost one coming first in the list *) +val push_visible : module_path -> module_path list -> unit +val pop_visible : unit -> unit + +val check_duplicate : module_path -> label -> string + +type reset_kind = AllButExternal | Everything + +val reset_renaming_tables : reset_kind -> unit + +val set_keywords : Idset.t -> unit diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml new file mode 100644 index 00000000..ab9c242a --- /dev/null +++ b/plugins/extraction/extract_env.ml @@ -0,0 +1,540 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Term +open Declarations +open Names +open Libnames +open Pp +open Util +open Miniml +open Table +open Extraction +open Modutil +open Common +open Mod_subst + +(***************************************) +(*S Part I: computing Coq environment. *) +(***************************************) + +let toplevel_env () = + let seg = Lib.contents_after None in + let get_reference = function + | (_,kn), Lib.Leaf o -> + let mp,_,l = repr_kn kn in + let seb = match Libobject.object_tag o with + | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn)) + | "INDUCTIVE" -> SFBmind (Global.lookup_mind (mind_of_kn kn)) + | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l))) + | "MODULE TYPE" -> + SFBmodtype (Global.lookup_modtype (MPdot (mp,l))) + | _ -> failwith "caught" + in l,seb + | _ -> failwith "caught" + in + match current_toplevel () with + | _ -> SEBstruct (List.rev (map_succeed get_reference seg)) + + +let environment_until dir_opt = + let rec parse = function + | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()] + | [] -> [] + | d :: l -> + match (Global.lookup_module (MPfile d)).mod_expr with + | Some meb -> + if dir_opt = Some d then [MPfile d, meb] + else (MPfile d, meb) :: (parse l) + | _ -> assert false + in parse (Library.loaded_libraries ()) + + +(*s Visit: + a structure recording the needed dependencies for the current extraction *) + +module type VISIT = sig + (* Reset the dependencies by emptying the visit lists *) + val reset : unit -> unit + + (* Add the module_path and all its prefixes to the mp visit list *) + val add_mp : module_path -> unit + + (* Add kernel_name / constant / reference / ... in the visit lists. + These functions silently add the mp of their arg in the mp list *) + val add_kn : mutual_inductive -> unit + val add_con : constant -> unit + val add_ref : global_reference -> unit + val add_decl_deps : ml_decl -> unit + val add_spec_deps : ml_spec -> unit + + (* Test functions: + is a particular object a needed dependency for the current extraction ? *) + val needed_kn : mutual_inductive -> bool + val needed_con : constant -> bool + val needed_mp : module_path -> bool +end + +module Visit : VISIT = struct + (* What used to be in a single KNset should now be split into a KNset + (for inductives and modules names) and a Cset for constants + (and still the remaining MPset) *) + type must_visit = + { mutable kn : Mindset.t; mutable con : Cset.t; mutable mp : MPset.t } + (* the imperative internal visit lists *) + let v = { kn = Mindset.empty ; con = Cset.empty ; mp = MPset.empty } + (* the accessor functions *) + let reset () = v.kn <- Mindset.empty; v.con <- Cset.empty; v.mp <- MPset.empty + let needed_kn kn = Mindset.mem kn v.kn + let needed_con c = Cset.mem c v.con + let needed_mp mp = MPset.mem mp v.mp + let add_mp mp = + check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp + let add_kn kn = v.kn <- Mindset.add kn v.kn; add_mp (mind_modpath kn) + let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c) + let add_ref = function + | ConstRef c -> add_con c + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn + | VarRef _ -> assert false + let add_decl_deps = decl_iter_references add_ref add_ref add_ref + let add_spec_deps = spec_iter_references add_ref add_ref add_ref +end + +exception Impossible + +let check_arity env cb = + let t = Typeops.type_of_constant_type env cb.const_type in + if Reduction.is_arity env t then raise Impossible + +let check_fix env cb i = + match cb.const_body with + | None -> raise Impossible + | Some lbody -> + match kind_of_term (Declarations.force lbody) with + | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd) + | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd) + | _ -> raise Impossible + +let factor_fix env l cb msb = + let _,recd as check = check_fix env cb 0 in + let n = Array.length (let fi,_,_ = recd in fi) in + if n = 1 then [|l|], recd, msb + else begin + if List.length msb < n-1 then raise Impossible; + let msb', msb'' = list_chop (n-1) msb in + let labels = Array.make n l in + list_iter_i + (fun j -> + function + | (l,SFBconst cb') -> + if check <> check_fix env cb' (j+1) then raise Impossible; + labels.(j+1) <- l; + | _ -> raise Impossible) msb'; + labels, recd, msb'' + end + +(** Expanding a [struct_expr_body] into a version without abbreviations + or functor applications. This is done via a detour to entries + (hack proposed by Elie) +*) + +let rec seb2mse = function + | SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s') + | SEBident mp -> Entries.MSEident mp + | _ -> failwith "seb2mse: received a non-atomic seb" + +let expand_seb env mp seb = + let seb,_,_,_ = + Mod_typing.translate_struct_module_entry env mp true (seb2mse seb) + in seb + +(** When possible, we use the nicer, shorter, algebraic type structures + instead of the expanded ones. *) + +let my_type_of_mb mb = + let m0 = mb.mod_type in + match mb.mod_type_alg with Some m -> m0,m | None -> m0,m0 + +let my_type_of_mtb mtb = + let m0 = mtb.typ_expr in + match mtb.typ_expr_alg with Some m -> m0,m | None -> m0,m0 + +(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. + To check with Elie. *) + +let rec msid_of_seb = function + | SEBident mp -> mp + | SEBwith (seb,_) -> msid_of_seb seb + | _ -> assert false + +let env_for_mtb_with env mp seb idl = + let sig_b = match seb with + | SEBstruct(sig_b) -> sig_b + | _ -> assert false + in + let l = label_of_id (List.hd idl) in + let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in + Modops.add_signature mp before empty_delta_resolver env + +(* From a [structure_body] (i.e. a list of [structure_field_body]) + to specifications. *) + +let rec extract_sfb_spec env mp = function + | [] -> [] + | (l,SFBconst cb) :: msig -> + let kn = make_con mp empty_dirpath l in + let s = extract_constant_spec env kn cb in + let specs = extract_sfb_spec env mp msig in + if logical_spec s then specs + else begin Visit.add_spec_deps s; (l,Spec s) :: specs end + | (l,SFBmind _) :: msig -> + let kn = make_kn mp empty_dirpath l in + let mind = mind_of_kn kn in + let s = Sind (kn, extract_inductive env mind) in + let specs = extract_sfb_spec env mp msig in + if logical_spec s then specs + else begin Visit.add_spec_deps s; (l,Spec s) :: specs end + | (l,SFBmodule mb) :: msig -> + let specs = extract_sfb_spec env mp msig in + let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb mb) in + (l,Smodule spec) :: specs + | (l,SFBmodtype mtb) :: msig -> + let specs = extract_sfb_spec env mp msig in + let spec = extract_seb_spec env mtb.typ_mp (my_type_of_mtb mtb) in + (l,Smodtype spec) :: specs + +(* From [struct_expr_body] to specifications *) + +(* Invariant: the [seb] given to [extract_seb_spec] should either come + from a [mod_type] or [type_expr] field, or their [_alg] counterparts. + This way, any encountered [SEBident] should be a true module type. +*) + +and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with + | SEBident mp -> Visit.add_mp mp; MTident mp + | SEBwith(seb',With_definition_body(idl,cb))-> + let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in + let mt = extract_seb_spec env mp1 (seb,seb') in + (match extract_with_type env' cb with (* cb peut contenir des kn *) + | None -> mt + | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ))) + | SEBwith(seb',With_module_body(idl,mp))-> + Visit.add_mp mp; + MTwith(extract_seb_spec env mp1 (seb,seb'), + ML_With_module(idl,mp)) + | SEBfunctor (mbid, mtb, seb_alg') -> + let seb' = match seb with + | SEBfunctor (mbid',_,seb') when mbid' = mbid -> seb' + | _ -> assert false + in + let mp = MPbound mbid in + let env' = Modops.add_module (Modops.module_body_of_type mp mtb) env in + MTfunsig (mbid, extract_seb_spec env mp (my_type_of_mtb mtb), + extract_seb_spec env' mp1 (seb',seb_alg')) + | SEBstruct (msig) -> + let env' = Modops.add_signature mp1 msig empty_delta_resolver env in + MTsig (mp1, extract_sfb_spec env' mp1 msig) + | SEBapply _ -> + if seb <> seb_alg then extract_seb_spec env mp1 (seb,seb) + else assert false + + + +(* From a [structure_body] (i.e. a list of [structure_field_body]) + to implementations. + + NB: when [all=false], the evaluation order of the list is + important: last to first ensures correct dependencies. +*) + +let rec extract_sfb env mp all = function + | [] -> [] + | (l,SFBconst cb) :: msb -> + (try + let vl,recd,msb = factor_fix env l cb msb in + let vc = Array.map (make_con mp empty_dirpath) vl in + let ms = extract_sfb env mp all msb in + let b = array_exists Visit.needed_con vc in + if all || b then + let d = extract_fixpoint env vc recd in + if (not b) && (logical_decl d) then ms + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end + else ms + with Impossible -> + let ms = extract_sfb env mp all msb in + let c = make_con mp empty_dirpath l in + let b = Visit.needed_con c in + if all || b then + let d = extract_constant env c cb in + if (not b) && (logical_decl d) then ms + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end + else ms) + | (l,SFBmind mib) :: msb -> + let ms = extract_sfb env mp all msb in + let kn = make_kn mp empty_dirpath l in + let mind = mind_of_kn kn in + let b = Visit.needed_kn mind in + if all || b then + let d = Dind (kn, extract_inductive env mind) in + if (not b) && (logical_decl d) then ms + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end + else ms + | (l,SFBmodule mb) :: msb -> + let ms = extract_sfb env mp all msb in + let mp = MPdot (mp,l) in + if all || Visit.needed_mp mp then + (l,SEmodule (extract_module env mp true mb)) :: ms + else ms + | (l,SFBmodtype mtb) :: msb -> + let ms = extract_sfb env mp all msb in + let mp = MPdot (mp,l) in + if all || Visit.needed_mp mp then + (l,SEmodtype (extract_seb_spec env mp (my_type_of_mtb mtb))) :: ms + else ms + +(* From [struct_expr_body] to implementations *) + +and extract_seb env mp all = function + | (SEBident _ | SEBapply _) as seb when lang () <> Ocaml -> + (* in Haskell/Scheme, we expand everything *) + extract_seb env mp all (expand_seb env mp seb) + | SEBident mp -> + if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; + Visit.add_mp mp; MEident mp + | SEBapply (meb, meb',_) -> + MEapply (extract_seb env mp true meb, + extract_seb env mp true meb') + | SEBfunctor (mbid, mtb, meb) -> + let mp1 = MPbound mbid in + let env' = Modops.add_module (Modops.module_body_of_type mp1 mtb) + env in + MEfunctor (mbid, extract_seb_spec env mp1 (my_type_of_mtb mtb), + extract_seb env' mp true meb) + | SEBstruct (msb) -> + let env' = Modops.add_signature mp msb empty_delta_resolver env in + MEstruct (mp,extract_sfb env' mp all msb) + | SEBwith (_,_) -> anomaly "Not available yet" + +and extract_module env mp all mb = + (* [mb.mod_expr <> None ], since we look at modules from outside. *) + (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) + { ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr); + ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) } + + +let unpack = function MEstruct (_,sel) -> sel | _ -> assert false + +let mono_environment refs mpl = + Visit.reset (); + List.iter Visit.add_ref refs; + List.iter Visit.add_mp mpl; + let env = Global.env () in + let l = List.rev (environment_until None) in + List.rev_map + (fun (mp,m) -> mp, unpack (extract_seb env mp false m)) l + +(**************************************) +(*S Part II : Input/Output primitives *) +(**************************************) + +let descr () = match lang () with + | Ocaml -> Ocaml.ocaml_descr + | Haskell -> Haskell.haskell_descr + | Scheme -> Scheme.scheme_descr + +(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" + Works similarly for the other languages. *) + +let default_id = id_of_string "Main" + +let mono_filename f = + let d = descr () in + match f with + | None -> None, None, default_id + | Some f -> + let f = + if Filename.check_suffix f d.file_suffix then + Filename.chop_suffix f d.file_suffix + else f + in + let id = + if lang () <> Haskell then default_id + else try id_of_string (Filename.basename f) + with _ -> error "Extraction: provided filename is not a valid identifier" + in + Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id + +(* Builds a suitable filename from a module id *) + +let module_filename mp = + let f = file_of_modfile mp in + let d = descr () in + Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f + +(*s Extraction of one decl to stdout. *) + +let print_one_decl struc mp decl = + let d = descr () in + reset_renaming_tables AllButExternal; + set_phase Pre; + ignore (d.pp_struct struc); + set_phase Impl; + push_visible mp []; + msgnl (d.pp_decl decl); + pop_visible () + +(*s Extraction of a ml struct to a file. *) + +let formatter dry file = + if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) + else match file with + | None -> !Pp_control.std_ft + | Some cout -> + let ft = Pp_control.with_output_to cout in + Option.iter (Format.pp_set_margin ft) (Pp_control.get_margin ()); + ft + +let print_structure_to_file (fn,si,mo) dry struc = + let d = descr () in + reset_renaming_tables AllButExternal; + let unsafe_needs = { + mldummy = struct_ast_search ((=) MLdummy) struc; + tdummy = struct_type_search Mlutil.isDummy struc; + tunknown = struct_type_search ((=) Tunknown) struc; + magic = + if lang () <> Haskell then false + else struct_ast_search (function MLmagic _ -> true | _ -> false) struc } + in + (* First, a dry run, for computing objects to rename or duplicate *) + set_phase Pre; + let devnull = formatter true None in + msg_with devnull (d.pp_struct struc); + let opened = opened_libraries () in + (* Print the implementation *) + let cout = if dry then None else Option.map open_out fn in + let ft = formatter dry cout in + begin try + (* The real printing of the implementation *) + set_phase Impl; + msg_with ft (d.preamble mo opened unsafe_needs); + msg_with ft (d.pp_struct struc); + Option.iter close_out cout; + with e -> + Option.iter close_out cout; raise e + end; + if not dry then Option.iter info_file fn; + (* Now, let's print the signature *) + Option.iter + (fun si -> + let cout = open_out si in + let ft = formatter false (Some cout) in + begin try + set_phase Intf; + msg_with ft (d.sig_preamble mo opened unsafe_needs); + msg_with ft (d.pp_sig (signature_of_structure struc)); + close_out cout; + with e -> + close_out cout; raise e + end; + info_file si) + (if dry then None else si) + + +(*********************************************) +(*s Part III: the actual extraction commands *) +(*********************************************) + + +let reset () = + Visit.reset (); reset_tables (); reset_renaming_tables Everything + +let init modular = + check_inside_section (); check_inside_module (); + set_keywords (descr ()).keywords; + set_modular modular; + reset (); + if modular && lang () = Scheme then error_scheme () + +(* From a list of [reference], let's retrieve whether they correspond + to modules or [global_reference]. Warn the user if both is possible. *) + +let rec locate_ref = function + | [] -> [],[] + | r::l -> + let q = snd (qualid_of_reference r) in + let mpo = try Some (Nametab.locate_module q) with Not_found -> None + and ro = try Some (Nametab.locate q) with Not_found -> None in + match mpo, ro with + | None, None -> Nametab.error_global_not_found q + | None, Some r -> let refs,mps = locate_ref l in r::refs,mps + | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps + | Some mp, Some r -> + warning_both_mod_and_cst q mp r; + let refs,mps = locate_ref l in refs,mp::mps + +(*s Recursive extraction in the Coq toplevel. The vernacular command is + \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when + extracting to a file with the command: + \verb!Extraction "file"! [qualid1] ... [qualidn]. *) + +let full_extr f (refs,mps) = + init false; + List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps; + let struc = optimize_struct refs (mono_environment refs mps) in + warning_axioms (); + print_structure_to_file (mono_filename f) false struc; + reset () + +let full_extraction f lr = full_extr f (locate_ref lr) + +(*s Simple extraction in the Coq toplevel. The vernacular command + is \verb!Extraction! [qualid]. *) + +let simple_extraction r = match locate_ref [r] with + | ([], [mp]) as p -> full_extr None p + | [r],[] -> + init false; + let struc = optimize_struct [r] (mono_environment [r] []) in + let d = get_decl_in_structure r struc in + warning_axioms (); + if is_custom r then msgnl (str "(** User defined extraction *)"); + print_one_decl struc (modpath_of_r r) d; + reset () + | _ -> assert false + + +(*s (Recursive) Extraction of a library. The vernacular command is + \verb!(Recursive) Extraction Library! [M]. *) + +let extraction_library is_rec m = + init true; + let dir_m = + let q = qualid_of_ident m in + try Nametab.full_name_module q with Not_found -> error_unknown_module q + in + Visit.add_mp (MPfile dir_m); + let env = Global.env () in + let l = List.rev (environment_until (Some dir_m)) in + let select l (mp,meb) = + if Visit.needed_mp mp + then (mp, unpack (extract_seb env mp true meb)) :: l + else l + in + let struc = List.fold_left select [] l in + let struc = optimize_struct [] struc in + warning_axioms (); + let print = function + | (MPfile dir as mp, sel) as e -> + let dry = not is_rec && dir <> dir_m in + print_structure_to_file (module_filename mp) dry [e] + | _ -> assert false + in + List.iter print struc; + reset () diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli new file mode 100644 index 00000000..dcb4601e --- /dev/null +++ b/plugins/extraction/extract_env.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*s This module declares the extraction commands. *) + +open Names +open Libnames + +val simple_extraction : reference -> unit +val full_extraction : string option -> reference list -> unit +val extraction_library : bool -> identifier -> unit + +(* For debug / external output via coqtop.byte + Drop : *) + +val mono_environment : + global_reference list -> module_path list -> Miniml.ml_structure diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml new file mode 100644 index 00000000..99682ae6 --- /dev/null +++ b/plugins/extraction/extraction.ml @@ -0,0 +1,982 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*i*) +open Util +open Names +open Term +open Declarations +open Environ +open Reduction +open Reductionops +open Inductive +open Termops +open Inductiveops +open Recordops +open Namegen +open Summary +open Libnames +open Nametab +open Miniml +open Table +open Mlutil +(*i*) + +exception I of inductive_info + +(* A set of all fixpoint functions currently being extracted *) +let current_fixpoints = ref ([] : constant list) + +let none = Evd.empty + +let type_of env c = Retyping.get_type_of env none (strip_outer_cast c) + +let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c) + +let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None + +(*S Generation of flags and signatures. *) + +(* The type [flag] gives us information about any Coq term: + \begin{itemize} + \item [TypeScheme] denotes a type scheme, that is + something that will become a type after enough applications. + More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with + [s = Set], [Prop] or [Type] + \item [Default] denotes the other cases. It may be inexact after + instanciation. For example [(X:Type)X] is [Default] and may give [Set] + after instanciation, which is rather [TypeScheme] + \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop] + \item [Info] is the opposite. The same example [(X:Type)X] shows + that an [Info] term might in fact be [Logic] later on. + \end{itemize} *) + +type info = Logic | Info + +type scheme = TypeScheme | Default + +type flag = info * scheme + +(*s [flag_of_type] transforms a type [t] into a [flag]. + Really important function. *) + +let rec flag_of_type env t = + let t = whd_betadeltaiota env none t in + match kind_of_term t with + | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c + | Sort (Prop Null) -> (Logic,TypeScheme) + | Sort _ -> (Info,TypeScheme) + | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default) + +(*s Two particular cases of [flag_of_type]. *) + +let is_default env t = (flag_of_type env t = (Info, Default)) + +exception NotDefault of kill_reason + +let check_default env t = + match flag_of_type env t with + | _,TypeScheme -> raise (NotDefault Ktype) + | Logic,_ -> raise (NotDefault Kother) + | _ -> () + +let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme)) + +(*s [type_sign] gernerates a signature aimed at treating a type application. *) + +let rec type_sign env c = + match kind_of_term (whd_betadeltaiota env none c) with + | Prod (n,t,d) -> + (if is_info_scheme env t then Keep else Kill Kother) + :: (type_sign (push_rel_assum (n,t) env) d) + | _ -> [] + +let rec type_scheme_nb_args env c = + match kind_of_term (whd_betadeltaiota env none c) with + | Prod (n,t,d) -> + let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in + if is_info_scheme env t then n+1 else n + | _ -> 0 + +let _ = register_type_scheme_nb_args type_scheme_nb_args + +(*s [type_sign_vl] does the same, plus a type var list. *) + +let rec type_sign_vl env c = + match kind_of_term (whd_betadeltaiota env none c) with + | Prod (n,t,d) -> + let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in + if not (is_info_scheme env t) then Kill Kother::s, vl + else Keep::s, (next_ident_away (id_of_name n) vl) :: vl + | _ -> [],[] + +let rec nb_default_params env c = + match kind_of_term (whd_betadeltaiota env none c) with + | Prod (n,t,d) -> + let n = nb_default_params (push_rel_assum (n,t) env) d in + if is_default env t then n+1 else n + | _ -> 0 + +(* Enriching a signature with implicit information *) + +let sign_with_implicits r s = + let implicits = implicits_of_global r in + let rec add_impl i = function + | [] -> [] + | sign::s -> + let sign' = + if sign = Keep && List.mem i implicits then Kill Kother else sign + in sign' :: add_impl (succ i) s + in + add_impl 1 s + +(* Enriching a exception message *) + +let rec handle_exn r n fn_name = function + | MLexn s -> + (try Scanf.sscanf s "UNBOUND %d" + (fun i -> + assert ((0 < i) && (i <= n)); + MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i))) + with _ -> MLexn s) + | a -> ast_map (handle_exn r n fn_name) a + +(*S Management of type variable contexts. *) + +(* A De Bruijn variable context (db) is a context for translating Coq [Rel] + into ML type [Tvar]. *) + +(*s From a type signature toward a type variable context (db). *) + +let db_from_sign s = + let rec make i acc = function + | [] -> acc + | Keep :: l -> make (i+1) (i::acc) l + | Kill _ :: l -> make i (0::acc) l + in make 1 [] s + +(*s Create a type variable context from indications taken from + an inductive type (see just below). *) + +let rec db_from_ind dbmap i = + if i = 0 then [] + else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1)) + +(*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument + of a constructor corresponds to the j-th type var of the ML inductive. *) + +(* \begin{itemize} + \item [si] : signature of the inductive + \item [i] : counter of Coq args for [(I args)] + \item [j] : counter of ML type vars + \item [relmax] : total args number of the constructor + \end{itemize} *) + +let parse_ind_args si args relmax = + let rec parse i j = function + | [] -> Intmap.empty + | Kill _ :: s -> parse (i+1) j s + | Keep :: s -> + (match kind_of_term args.(i-1) with + | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s) + | _ -> parse (i+1) (j+1) s) + in parse 1 1 si + +(*S Extraction of a type. *) + +(* [extract_type env db c args] is used to produce an ML type from the + coq term [(c args)], which is supposed to be a Coq type. *) + +(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *) + +(* [j] stands for the next ML type var. [j=0] means we do not + generate ML type var anymore (in subterms for example). *) + + +let rec extract_type env db j c args = + match kind_of_term (whd_betaiotazeta Evd.empty c) with + | App (d, args') -> + (* We just accumulate the arguments. *) + extract_type env db j d (Array.to_list args' @ args) + | Lambda (_,_,d) -> + (match args with + | [] -> assert false (* otherwise the lambda would be reductible. *) + | a :: args -> extract_type env db j (subst1 a d) args) + | Prod (n,t,d) -> + assert (args = []); + let env' = push_rel_assum (n,t) env in + (match flag_of_type env t with + | (Info, Default) -> + (* Standard case: two [extract_type] ... *) + let mld = extract_type env' (0::db) j d [] in + (match expand env mld with + | Tdummy d -> Tdummy d + | _ -> Tarr (extract_type env db 0 t [], mld)) + | (Info, TypeScheme) when j > 0 -> + (* A new type var. *) + let mld = extract_type env' (j::db) (j+1) d [] in + (match expand env mld with + | Tdummy d -> Tdummy d + | _ -> Tarr (Tdummy Ktype, mld)) + | _,lvl -> + let mld = extract_type env' (0::db) j d [] in + (match expand env mld with + | Tdummy d -> Tdummy d + | _ -> + let reason = if lvl=TypeScheme then Ktype else Kother in + Tarr (Tdummy reason, mld))) + | Sort _ -> Tdummy Ktype (* The two logical cases. *) + | _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother + | Rel n -> + (match lookup_rel n env with + | (_,Some t,_) -> extract_type env db j (lift n t) args + | _ -> + (* Asks [db] a translation for [n]. *) + if n > List.length db then Tunknown + else let n' = List.nth db (n-1) in + if n' = 0 then Tunknown else Tvar n') + | Const kn -> + let r = ConstRef kn in + let cb = lookup_constant kn env in + let typ = Typeops.type_of_constant_type env cb.const_type in + (match flag_of_type env typ with + | (Info, TypeScheme) -> + let mlt = extract_type_app env db (r, type_sign env typ) args in + (match cb.const_body with + | None -> mlt + | Some _ when is_custom r -> mlt + | Some lbody -> + let newc = applist (Declarations.force lbody, args) in + let mlt' = extract_type env db j newc [] in + (* ML type abbreviations interact badly with Coq *) + (* reduction, so [mlt] and [mlt'] might be different: *) + (* The more precise is [mlt'], extracted after reduction *) + (* The shortest is [mlt], which use abbreviations *) + (* If possible, we take [mlt], otherwise [mlt']. *) + if expand env mlt = expand env mlt' then mlt else mlt') + | _ -> (* only other case here: Info, Default, i.e. not an ML type *) + (match cb.const_body with + | None -> Tunknown (* Brutal approximation ... *) + | Some lbody -> + (* We try to reduce. *) + let newc = applist (Declarations.force lbody, args) in + extract_type env db j newc [])) + | Ind (kn,i) -> + let s = (extract_ind env kn).ind_packets.(i).ip_sign in + extract_type_app env db (IndRef (kn,i),s) args + | Case _ | Fix _ | CoFix _ -> Tunknown + | _ -> assert false + +(* [extract_maybe_type] calls [extract_type] when used on a Coq type, + and otherwise returns [Tdummy] or [Tunknown] *) + +and extract_maybe_type env db c = + let t = whd_betadeltaiota env none (type_of env c) in + if isSort t then extract_type env db 0 c [] + else if sort_of env t = InProp then Tdummy Kother else Tunknown + +(*s Auxiliary function dealing with type application. + Precondition: [r] is a type scheme represented by the signature [s], + and is completely applied: [List.length args = List.length s]. *) + +and extract_type_app env db (r,s) args = + let ml_args = + List.fold_right + (fun (b,c) a -> if b=Keep then + let p = List.length (fst (splay_prod env none (type_of env c))) in + let db = iterate (fun l -> 0 :: l) p db in + (extract_type_scheme env db c p) :: a + else a) + (List.combine s args) [] + in Tglob (r, ml_args) + +(*S Extraction of a type scheme. *) + +(* [extract_type_scheme env db c p] works on a Coq term [c] which is + an informative type scheme. It means that [c] is not a Coq type, but will + be when applied to sufficiently many arguments ([p] in fact). + This function decomposes p lambdas, with eta-expansion if needed. *) + +(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *) + +and extract_type_scheme env db c p = + if p=0 then extract_type env db 0 c [] + else + let c = whd_betaiotazeta Evd.empty c in + match kind_of_term c with + | Lambda (n,t,d) -> + extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) + | _ -> + let rels = fst (splay_prod env none (type_of env c)) in + let env = push_rels_assum rels env in + let eta_args = List.rev_map mkRel (interval 1 p) in + extract_type env db 0 (lift p c) eta_args + + +(*S Extraction of an inductive type. *) + +and extract_ind env kn = (* kn is supposed to be in long form *) + let mib = Environ.lookup_mind kn env in + try + (* For a same kn, we can get various bodies due to module substitutions. + We hence check that the mib has not changed from recording + time to retrieving time. Ideally we should also check the env. *) + let (mib0,ml_ind) = lookup_ind kn in + if not (mib = mib0) then raise Not_found; + ml_ind + with Not_found -> + (* First, if this inductive is aliased via a Module, *) + (* we process the original inductive. *) + let equiv = + if (canonical_mind kn) = (user_mind kn) then + NoEquiv + else + begin + ignore (extract_ind env (mind_of_kn (canonical_mind kn))); + Equiv (canonical_mind kn) + end + in + (* Everything concerning parameters. *) + (* We do that first, since they are common to all the [mib]. *) + let mip0 = mib.mind_packets.(0) in + let npar = mib.mind_nparams in + let epar = push_rel_context mib.mind_params_ctxt env in + (* First pass: we store inductive signatures together with *) + (* their type var list. *) + let packets = + Array.map + (fun mip -> + let b = snd (mind_arity mip) <> InProp in + let ar = Inductive.type_of_inductive env (mib,mip) in + let s,v = if b then type_sign_vl env ar else [],[] in + let t = Array.make (Array.length mip.mind_nf_lc) [] in + { ip_typename = mip.mind_typename; + ip_consnames = mip.mind_consnames; + ip_logical = (not b); + ip_sign = s; + ip_vars = v; + ip_types = t; + ip_optim_id_ok = None }) + mib.mind_packets + in + + add_ind kn mib + {ind_info = Standard; + ind_nparams = npar; + ind_packets = packets; + ind_equiv = equiv + }; + (* Second pass: we extract constructors *) + for i = 0 to mib.mind_ntypes - 1 do + let p = packets.(i) in + if not p.ip_logical then + let types = arities_of_constructors env (kn,i) in + for j = 0 to Array.length types - 1 do + let t = snd (decompose_prod_n npar types.(j)) in + let prods,head = dest_prod epar t in + let nprods = List.length prods in + let args = match kind_of_term head with + | App (f,args) -> args (* [kind_of_term f = Ind ip] *) + | _ -> [||] + in + let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in + let db = db_from_ind dbmap npar in + p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1) + done + done; + (* Third pass: we determine special cases. *) + let ind_info = + try + if not mib.mind_finite then raise (I Coinductive); + if mib.mind_ntypes <> 1 then raise (I Standard); + let p = packets.(0) in + if p.ip_logical then raise (I Standard); + if Array.length p.ip_types <> 1 then raise (I Standard); + let typ = p.ip_types.(0) in + let l = List.filter (fun t -> not (isDummy (expand env t))) typ in + if List.length l = 1 && not (type_mem_kn kn (List.hd l)) + then raise (I Singleton); + if l = [] then raise (I Standard); + if not mib.mind_record then raise (I Standard); + let ip = (kn, 0) in + let r = IndRef ip in + if is_custom r then raise (I Standard); + (* Now we're sure it's a record. *) + (* First, we find its field names. *) + let rec names_prod t = match kind_of_term t with + | Prod(n,_,t) -> n::(names_prod t) + | LetIn(_,_,_,t) -> names_prod t + | Cast(t,_,_) -> names_prod t + | _ -> [] + in + let field_names = + list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in + assert (List.length field_names = List.length typ); + let projs = ref Cset.empty in + let mp,d,_ = repr_mind kn in + let rec select_fields l typs = match l,typs with + | [],[] -> [] + | (Name id)::l, typ::typs -> + if isDummy (expand env typ) then select_fields l typs + else + let knp = make_con mp d (label_of_id id) in + if List.for_all ((=) Keep) (type2signature env typ) + then + projs := Cset.add knp !projs; + (ConstRef knp) :: (select_fields l typs) + | Anonymous::l, typ::typs -> + if isDummy (expand env typ) then select_fields l typs + else error_record r + | _ -> assert false + in + let field_glob = select_fields field_names typ + in + (* Is this record officially declared with its projections ? *) + (* If so, we use this information. *) + begin try + let n = nb_default_params env + (Inductive.type_of_inductive env (mib,mip0)) + in + List.iter + (Option.iter + (fun kn -> if Cset.mem kn !projs then add_projection n kn)) + (lookup_projections ip) + with Not_found -> () + end; + Record field_glob + with (I info) -> info + in + let i = {ind_info = ind_info; + ind_nparams = npar; + ind_packets = packets; + ind_equiv = equiv } + in + add_ind kn mib i; + i + +(*s [extract_type_cons] extracts the type of an inductive + constructor toward the corresponding list of ML types. + + - [db] is a context for translating Coq [Rel] into ML type [Tvar] + - [dbmap] is a translation map (produced by a call to [parse_in_args]) + - [i] is the rank of the current product (initially [params_nb+1]) +*) + +and extract_type_cons env db dbmap c i = + match kind_of_term (whd_betadeltaiota env none c) with + | Prod (n,t,d) -> + let env' = push_rel_assum (n,t) env in + let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in + let l = extract_type_cons env' db' dbmap d (i+1) in + (extract_type env db 0 t []) :: l + | _ -> [] + +(*s Recording the ML type abbreviation of a Coq type scheme constant. *) + +and mlt_env env r = match r with + | ConstRef kn -> + (try + if not (visible_con kn) then raise Not_found; + match lookup_term kn with + | Dtype (_,vl,mlt) -> Some mlt + | _ -> None + with Not_found -> + let cb = Environ.lookup_constant kn env in + let typ = Typeops.type_of_constant_type env cb.const_type in + match cb.const_body with + | None -> None + | Some l_body -> + (match flag_of_type env typ with + | Info,TypeScheme -> + let body = Declarations.force l_body in + let s,vl = type_sign_vl env typ in + let db = db_from_sign s in + let t = extract_type_scheme env db body (List.length s) + in add_term kn (Dtype (r, vl, t)); Some t + | _ -> None)) + | _ -> None + +and expand env = type_expand (mlt_env env) +and type2signature env = type_to_signature (mlt_env env) +let type2sign env = type_to_sign (mlt_env env) +let type_expunge env = type_expunge (mlt_env env) +let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env) + +(*s Extraction of the type of a constant. *) + +let record_constant_type env kn opt_typ = + try + if not (visible_con kn) then raise Not_found; + lookup_type kn + with Not_found -> + let typ = match opt_typ with + | None -> Typeops.type_of_constant env kn + | Some typ -> typ + in let mlt = extract_type env [] 1 typ [] + in let schema = (type_maxvar mlt, mlt) + in add_type kn schema; schema + +(*S Extraction of a term. *) + +(* Precondition: [(c args)] is not a type scheme, and is informative. *) + +(* [mle] is a ML environment [Mlenv.t]. *) +(* [mlt] is the ML type we want our extraction of [(c args)] to have. *) + +let rec extract_term env mle mlt c args = + match kind_of_term c with + | App (f,a) -> + extract_term env mle mlt f (Array.to_list a @ args) + | Lambda (n, t, d) -> + let id = id_of_name n in + (match args with + | a :: l -> + (* We make as many [LetIn] as possible. *) + let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l)) + in extract_term env mle mlt d' [] + | [] -> + let env' = push_rel_assum (Name id, t) env in + let id, a = + try check_default env t; Id id, new_meta() + with NotDefault d -> Dummy, Tdummy d + in + let b = new_meta () in + (* If [mlt] cannot be unified with an arrow type, then magic! *) + let magic = needs_magic (mlt, Tarr (a, b)) in + let d' = extract_term env' (Mlenv.push_type mle a) b d [] in + put_magic_if magic (MLlam (id, d'))) + | LetIn (n, c1, t1, c2) -> + let id = id_of_name n in + let env' = push_rel (Name id, Some c1, t1) env in + let args' = List.map (lift 1) args in + (try + check_default env t1; + let a = new_meta () in + let c1' = extract_term env mle a c1 [] in + (* The type of [c1'] is generalized and stored in [mle]. *) + let mle' = Mlenv.push_gen mle a in + MLletin (Id id, c1', extract_term env' mle' mlt c2 args') + with NotDefault d -> + let mle' = Mlenv.push_std_type mle (Tdummy d) in + ast_pop (extract_term env' mle' mlt c2 args')) + | Const kn -> + extract_cst_app env mle mlt kn args + | Construct cp -> + extract_cons_app env mle mlt cp args + | Rel n -> + (* As soon as the expected [mlt] for the head is known, *) + (* we unify it with an fresh copy of the stored type of [Rel n]. *) + let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n) + in extract_app env mle mlt extract_rel args + | Case ({ci_ind=ip},_,c0,br) -> + extract_app env mle mlt (extract_case env mle (ip,c0,br)) args + | Fix ((_,i),recd) -> + extract_app env mle mlt (extract_fix env mle i recd) args + | CoFix (i,recd) -> + extract_app env mle mlt (extract_fix env mle i recd) args + | Cast (c,_,_) -> extract_term env mle mlt c args + | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false + +(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) + +and extract_maybe_term env mle mlt c = + try check_default env (type_of env c); + extract_term env mle mlt c [] + with NotDefault d -> + put_magic (mlt, Tdummy d) MLdummy + +(*s Generic way to deal with an application. *) + +(* We first type all arguments starting with unknown meta types. + This gives us the expected type of the head. Then we use the + [mk_head] to produce the ML head from this type. *) + +and extract_app env mle mlt mk_head args = + let metas = List.map new_meta args in + let type_head = type_recomp (metas, mlt) in + let mlargs = List.map2 (extract_maybe_term env mle) metas args in + mlapp (mk_head type_head) mlargs + +(*s Auxiliary function used to extract arguments of constant or constructor. *) + +and make_mlargs env e s args typs = + let rec f = function + | [], [], _ -> [] + | a::la, t::lt, [] -> extract_maybe_term env e t a :: (f (la,lt,[])) + | a::la, t::lt, Keep::s -> extract_maybe_term env e t a :: (f (la,lt,s)) + | _::la, _::lt, _::s -> f (la,lt,s) + | _ -> assert false + in f (args,typs,s) + +(*s Extraction of a constant applied to arguments. *) + +and extract_cst_app env mle mlt kn args = + (* First, the [ml_schema] of the constant, in expanded version. *) + let nb,t = record_constant_type env kn None in + let schema = nb, expand env t in + (* Can we instantiate types variables for this constant ? *) + (* In Ocaml, inside the definition of this constant, the answer is no. *) + let instantiated = + if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema) + else instantiation schema + in + (* Then the expected type of this constant. *) + let a = new_meta () in + (* We compare stored and expected types in two steps. *) + (* First, can [kn] be applied to all args ? *) + let metas = List.map new_meta args in + let magic1 = needs_magic (type_recomp (metas, a), instantiated) in + (* Second, is the resulting type compatible with the expected type [mlt] ? *) + let magic2 = needs_magic (a, mlt) in + (* The internal head receives a magic if [magic1] *) + let head = put_magic_if magic1 (MLglob (ConstRef kn)) in + (* Now, the extraction of the arguments. *) + let s_full = type2signature env (snd schema) in + let s_full = sign_with_implicits (ConstRef kn) s_full in + let s = sign_no_final_keeps s_full in + let ls = List.length s in + let la = List.length args in + (* The ml arguments, already expunged from known logical ones *) + let mla = make_mlargs env mle s args metas in + let mla = + if not magic1 then + try + let l,l' = list_chop (projection_arity (ConstRef kn)) mla in + if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l' + else mla + with _ -> mla + else mla + in + (* For strict languages, purely logical signatures with at least + one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left + accordingly. *) + let optdummy = match sign_kind s_full with + | UnsafeLogicalSig when lang () <> Haskell -> [MLdummy] + | _ -> [] + in + (* Different situations depending of the number of arguments: *) + if la >= ls + then + (* Enough args, cleanup already done in [mla], we only add the + additionnal dummy if needed. *) + put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla)) + else + (* Partially applied function with some logical arg missing. + We complete via eta and expunge logical args. *) + let ls' = ls-la in + let s' = list_skipn la s in + let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in + let e = anonym_or_dummy_lams (mlapp head mla) s' in + put_magic_if magic2 (remove_n_lams (List.length optdummy) e) + +(*s Extraction of an inductive constructor applied to arguments. *) + +(* \begin{itemize} + \item In ML, contructor arguments are uncurryfied. + \item We managed to suppress logical parts inside inductive definitions, + but they must appears outside (for partial applications for instance) + \item We also suppressed all Coq parameters to the inductives, since + they are fixed, and thus are not used for the computation. + \end{itemize} *) + +and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = + (* First, we build the type of the constructor, stored in small pieces. *) + let mi = extract_ind env kn in + let params_nb = mi.ind_nparams in + let oi = mi.ind_packets.(i) in + let nb_tvars = List.length oi.ip_vars + and types = List.map (expand env) oi.ip_types.(j-1) in + let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in + let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in + let type_cons = instantiation (nb_tvars, type_cons) in + (* Then, the usual variables [s], [ls], [la], ... *) + let s = List.map (type2sign env) types in + let s = sign_with_implicits (ConstructRef cp) s in + let ls = List.length s in + let la = List.length args in + assert (la <= ls + params_nb); + let la' = max 0 (la - params_nb) in + let args' = list_lastn la' args in + (* Now, we build the expected type of the constructor *) + let metas = List.map new_meta args' in + (* If stored and expected types differ, then magic! *) + let a = new_meta () in + let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in + let magic2 = needs_magic (a, mlt) in + let head mla = + if mi.ind_info = Singleton then + put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *) + else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla)) + in + (* Different situations depending of the number of arguments: *) + if la < params_nb then + let head' = head (eta_args_sign ls s) in + put_magic_if magic2 + (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)) + else + let mla = make_mlargs env mle s args' metas in + if la = ls + params_nb + then put_magic_if (magic2 && not magic1) (head mla) + else (* [ params_nb <= la <= ls + params_nb ] *) + let ls' = params_nb + ls - la in + let s' = list_lastn ls' s in + let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in + put_magic_if magic2 (anonym_or_dummy_lams (head mla) s') + +(*S Extraction of a case. *) + +and extract_case env mle ((kn,i) as ip,c,br) mlt = + (* [br]: bodies of each branch (in functional form) *) + (* [ni]: number of arguments without parameters in each branch *) + let ni = mis_constr_nargs_env env ip in + let br_size = Array.length br in + assert (Array.length ni = br_size); + if br_size = 0 then begin + add_recursors env kn; (* May have passed unseen if logical ... *) + MLexn "absurd case" + end else + (* [c] has an inductive type, and is not a type scheme type. *) + let t = type_of env c in + (* The only non-informative case: [c] is of sort [Prop] *) + if (sort_of env t) = InProp then + begin + add_recursors env kn; (* May have passed unseen if logical ... *) + (* Logical singleton case: *) + (* [match c with C i j k -> t] becomes [t'] *) + assert (br_size = 1); + let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in + let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in + let e = extract_maybe_term env mle mlt br.(0) in + snd (case_expunge s e) + end + else + let mi = extract_ind env kn in + let oi = mi.ind_packets.(i) in + let metas = Array.init (List.length oi.ip_vars) new_meta in + (* The extraction of the head. *) + let type_head = Tglob (IndRef ip, Array.to_list metas) in + let a = extract_term env mle type_head c [] in + (* The extraction of each branch. *) + let extract_branch i = + let r = ConstructRef (ip,i+1) in + (* The types of the arguments of the corresponding constructor. *) + let f t = type_subst_vect metas (expand env t) in + let l = List.map f oi.ip_types.(i) in + (* the corresponding signature *) + let s = List.map (type2sign env) oi.ip_types.(i) in + let s = sign_with_implicits r s in + (* Extraction of the branch (in functional form). *) + let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in + (* We suppress dummy arguments according to signature. *) + let ids,e = case_expunge s e in + let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in + (r, List.rev ids, e') + in + if mi.ind_info = Singleton then + begin + (* Informative singleton case: *) + (* [match c with C i -> t] becomes [let i = c' in t'] *) + assert (br_size = 1); + let (_,ids,e') = extract_branch 0 in + assert (List.length ids = 1); + MLletin (tmp_id (List.hd ids),a,e') + end + else + (* Standard case: we apply [extract_branch]. *) + MLcase ((mi.ind_info,BranchNone), a, Array.init br_size extract_branch) + +(*s Extraction of a (co)-fixpoint. *) + +and extract_fix env mle i (fi,ti,ci as recd) mlt = + let env = push_rec_types recd env in + let metas = Array.map new_meta fi in + metas.(i) <- mlt; + let mle = Array.fold_left Mlenv.push_type mle metas in + let ei = array_map2 (extract_maybe_term env mle) metas ci in + MLfix (i, Array.map id_of_name fi, ei) + +(*S ML declarations. *) + +(* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], + and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *) + +let rec decomp_lams_eta_n n m env c t = + let rels = fst (splay_prod_n env none n t) in + let rels = List.map (fun (id,_,c) -> (id,c)) rels in + let rels',c = decompose_lam c in + let d = n - m in + (* we'd better keep rels' as long as possible. *) + let rels = (list_firstn d rels) @ rels' in + let eta_args = List.rev_map mkRel (interval 1 d) in + rels, applist (lift d c,eta_args) + +(*s From a constant to a ML declaration. *) + +let extract_std_constant env kn body typ = + reset_meta_count (); + (* The short type [t] (i.e. possibly with abbreviations). *) + let t = snd (record_constant_type env kn (Some typ)) in + (* The real type [t']: without head products, expanded, *) + (* and with [Tvar] translated to [Tvar'] (not instantiable). *) + let l,t' = type_decomp (expand env (var2var' t)) in + let s = List.map (type2sign env) l in + (* Check for user-declared implicit information *) + let s = sign_with_implicits (ConstRef kn) s in + (* Decomposing the top level lambdas of [body]. + If there isn't enough, it's ok, as long as remaining args + aren't to be pruned (and initial lambdas aren't to be all + removed if the target language is strict). In other situations, + eta-expansions create artificially enough lams (but that may + break user's clever let-ins and partial applications). *) + let rels, c = + let n = List.length s + and m = nb_lam body in + if n <= m then decompose_lam_n n body + else + let s,s' = list_split_at m s in + if List.for_all ((=) Keep) s' && + (lang () = Haskell || sign_kind s <> UnsafeLogicalSig) + then decompose_lam_n m body + else decomp_lams_eta_n n m env body typ + in + let n = List.length rels in + let s = list_firstn n s in + let l,l' = list_split_at n l in + let t' = type_recomp (l',t') in + (* The initial ML environment. *) + let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in + (* The lambdas names. *) + let ids = List.map (fun (n,_) -> Id (id_of_name n)) rels in + (* The according Coq environment. *) + let env = push_rels_assum rels env in + (* The real extraction: *) + let e = extract_term env mle t' c [] in + (* Expunging term and type from dummy lambdas. *) + let trm = term_expunge s (ids,e) in + let trm = handle_exn (ConstRef kn) n (fun i -> fst (List.nth rels (i-1))) trm + in + trm, type_expunge_from_sign env s t + +let extract_fixpoint env vkn (fi,ti,ci) = + let n = Array.length vkn in + let types = Array.make n (Tdummy Kother) + and terms = Array.make n MLdummy in + let kns = Array.to_list vkn in + current_fixpoints := kns; + (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) + let sub = List.rev_map mkConst kns in + for i = 0 to n-1 do + if sort_of env ti.(i) <> InProp then begin + let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in + terms.(i) <- e; + types.(i) <- t; + end + done; + current_fixpoints := []; + Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) + +let extract_constant env kn cb = + let r = ConstRef kn in + let typ = Typeops.type_of_constant_type env cb.const_type in + match cb.const_body with + | None -> (* A logical axiom is risky, an informative one is fatal. *) + (match flag_of_type env typ with + | (Info,TypeScheme) -> + if not (is_custom r) then add_info_axiom r; + let n = type_scheme_nb_args env typ in + let ids = iterate (fun l -> anonymous_name::l) n [] in + Dtype (r, ids, Taxiom) + | (Info,Default) -> + if not (is_custom r) then add_info_axiom r; + let t = snd (record_constant_type env kn (Some typ)) in + Dterm (r, MLaxiom, type_expunge env t) + | (Logic,TypeScheme) -> + add_log_axiom r; Dtype (r, [], Tdummy Ktype) + | (Logic,Default) -> + add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother)) + | Some body -> + (match flag_of_type env typ with + | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother) + | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype) + | (Info, Default) -> + let e,t = extract_std_constant env kn (force body) typ in + Dterm (r,e,t) + | (Info, TypeScheme) -> + let s,vl = type_sign_vl env typ in + let db = db_from_sign s in + let t = extract_type_scheme env db (force body) (List.length s) + in Dtype (r, vl, t)) + +let extract_constant_spec env kn cb = + let r = ConstRef kn in + let typ = Typeops.type_of_constant_type env cb.const_type in + match flag_of_type env typ with + | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) + | (Logic, Default) -> Sval (r, Tdummy Kother) + | (Info, TypeScheme) -> + let s,vl = type_sign_vl env typ in + (match cb.const_body with + | None -> Stype (r, vl, None) + | Some body -> + let db = db_from_sign s in + let t = extract_type_scheme env db (force body) (List.length s) + in Stype (r, vl, Some t)) + | (Info, Default) -> + let t = snd (record_constant_type env kn (Some typ)) in + Sval (r, type_expunge env t) + +let extract_with_type env cb = + let typ = Typeops.type_of_constant_type env cb.const_type in + match flag_of_type env typ with + | (Info, TypeScheme) -> + let s,vl = type_sign_vl env typ in + let body = Option.get cb.const_body in + let db = db_from_sign s in + let t = extract_type_scheme env db (force body) (List.length s) in + Some (vl, t) + | _ -> None + + +let extract_inductive env kn = + let ind = extract_ind env kn in + add_recursors env kn; + let f i j l = + let implicits = implicits_of_global (ConstructRef ((kn,i),j+1)) in + let rec filter i = function + | [] -> [] + | t::l -> + let l' = filter (succ i) l in + if isDummy (expand env t) || List.mem i implicits then l' + else t::l' + in filter 1 l + in + let packets = + Array.mapi (fun i p -> { p with ip_types = Array.mapi (f i) p.ip_types }) + ind.ind_packets + in { ind with ind_packets = packets } + +(*s Is a [ml_decl] logical ? *) + +let logical_decl = function + | Dterm (_,MLdummy,Tdummy _) -> true + | Dtype (_,[],Tdummy _) -> true + | Dfix (_,av,tv) -> + (array_for_all ((=) MLdummy) av) && + (array_for_all isDummy tv) + | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets + | _ -> false + +(*s Is a [ml_spec] logical ? *) + +let logical_spec = function + | Stype (_, [], Some (Tdummy _)) -> true + | Sval (_,Tdummy _) -> true + | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets + | _ -> false diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli new file mode 100644 index 00000000..6bcd2476 --- /dev/null +++ b/plugins/extraction/extraction.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*s Extraction from Coq terms to Miniml. *) + +open Names +open Term +open Declarations +open Environ +open Libnames +open Miniml + +val extract_constant : env -> constant -> constant_body -> ml_decl + +val extract_constant_spec : env -> constant -> constant_body -> ml_spec + +val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option + +val extract_fixpoint : + env -> constant array -> (constr, types) prec_declaration -> ml_decl + +val extract_inductive : env -> mutual_inductive -> ml_ind + +(*s Is a [ml_decl] or a [ml_spec] logical ? *) + +val logical_decl : ml_decl -> bool +val logical_spec : ml_spec -> bool diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib new file mode 100644 index 00000000..b7f45861 --- /dev/null +++ b/plugins/extraction/extraction_plugin.mllib @@ -0,0 +1,11 @@ +Table +Mlutil +Modutil +Extraction +Common +Ocaml +Haskell +Scheme +Extract_env +G_extraction +Extraction_plugin_mod diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 new file mode 100644 index 00000000..18828241 --- /dev/null +++ b/plugins/extraction/g_extraction.ml4 @@ -0,0 +1,142 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* ML names *) + +open Vernacexpr +open Pcoq +open Genarg +open Pp +open Names +open Nameops +open Table +open Extract_env + +let pr_mlname _ _ _ s = spc () ++ qs s + +ARGUMENT EXTEND mlname + TYPED AS string + PRINTED BY pr_mlname +| [ preident(id) ] -> [ id ] +| [ string(s) ] -> [ s ] +END + +let pr_int_or_id _ _ _ = function + | ArgInt i -> int i + | ArgId id -> pr_id id + +ARGUMENT EXTEND int_or_id + TYPED AS int_or_id + PRINTED BY pr_int_or_id +| [ preident(id) ] -> [ ArgId (id_of_string id) ] +| [ integer(i) ] -> [ ArgInt i ] +END + +let pr_language = function + | Ocaml -> str "Ocaml" + | Haskell -> str "Haskell" + | Scheme -> str "Scheme" + +VERNAC ARGUMENT EXTEND language +PRINTED BY pr_language +| [ "Ocaml" ] -> [ Ocaml ] +| [ "Haskell" ] -> [ Haskell ] +| [ "Scheme" ] -> [ Scheme ] +END + +(* Extraction commands *) + +VERNAC COMMAND EXTEND Extraction +(* Extraction in the Coq toplevel *) +| [ "Extraction" global(x) ] -> [ simple_extraction x ] +| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ] + +(* Monolithic extraction to a file *) +| [ "Extraction" string(f) ne_global_list(l) ] + -> [ full_extraction (Some f) l ] +END + +(* Modular extraction (one Coq library = one ML module) *) +VERNAC COMMAND EXTEND ExtractionLibrary +| [ "Extraction" "Library" ident(m) ] + -> [ extraction_library false m ] +END + +VERNAC COMMAND EXTEND RecursiveExtractionLibrary +| [ "Recursive" "Extraction" "Library" ident(m) ] + -> [ extraction_library true m ] +END + +(* Target Language *) +VERNAC COMMAND EXTEND ExtractionLanguage +| [ "Extraction" "Language" language(l) ] + -> [ extraction_language l ] +END + +VERNAC COMMAND EXTEND ExtractionInline +(* Custom inlining directives *) +| [ "Extraction" "Inline" ne_global_list(l) ] + -> [ extraction_inline true l ] +END + +VERNAC COMMAND EXTEND ExtractionNoInline +| [ "Extraction" "NoInline" ne_global_list(l) ] + -> [ extraction_inline false l ] +END + +VERNAC COMMAND EXTEND PrintExtractionInline +| [ "Print" "Extraction" "Inline" ] + -> [ print_extraction_inline () ] +END + +VERNAC COMMAND EXTEND ResetExtractionInline +| [ "Reset" "Extraction" "Inline" ] + -> [ reset_extraction_inline () ] +END + +VERNAC COMMAND EXTEND ExtractionImplicit +(* Custom implicit arguments of some csts/inds/constructors *) +| [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ] + -> [ extraction_implicit r l ] +END + +VERNAC COMMAND EXTEND ExtractionBlacklist +(* Force Extraction to not use some filenames *) +| [ "Extraction" "Blacklist" ne_ident_list(l) ] + -> [ extraction_blacklist l ] +END + +VERNAC COMMAND EXTEND PrintExtractionBlacklist +| [ "Print" "Extraction" "Blacklist" ] + -> [ print_extraction_blacklist () ] +END + +VERNAC COMMAND EXTEND ResetExtractionBlacklist +| [ "Reset" "Extraction" "Blacklist" ] + -> [ reset_extraction_blacklist () ] +END + + +(* Overriding of a Coq object by an ML one *) +VERNAC COMMAND EXTEND ExtractionConstant +| [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ] + -> [ extract_constant_inline false x idl y ] +END + +VERNAC COMMAND EXTEND ExtractionInlinedConstant +| [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ] + -> [ extract_constant_inline true x [] y ] +END + +VERNAC COMMAND EXTEND ExtractionInductive +| [ "Extract" "Inductive" global(x) "=>" + mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] + -> [ extract_inductive x id idl o ] +END diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml new file mode 100644 index 00000000..bb1dbd48 --- /dev/null +++ b/plugins/extraction/haskell.ml @@ -0,0 +1,357 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*s Production of Haskell syntax. *) + +open Pp +open Util +open Names +open Nameops +open Libnames +open Table +open Miniml +open Mlutil +open Common + +(*s Haskell renaming issues. *) + +let pr_lower_id id = str (String.uncapitalize (string_of_id id)) +let pr_upper_id id = str (String.capitalize (string_of_id id)) + +let keywords = + List.fold_right (fun s -> Idset.add (id_of_string s)) + [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else"; + "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; + "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__"; + "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ] + Idset.empty + +let preamble mod_name used_modules usf = + let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n") + in + (if not usf.magic then mt () + else + str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++ + str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n") + ++ + str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++ + str "import qualified Prelude" ++ fnl () ++ + prlist pp_import used_modules ++ fnl () ++ + (if used_modules = [] then mt () else fnl ()) ++ + (if not usf.magic then mt () + else str "\ +#ifdef __GLASGOW_HASKELL__ +import qualified GHC.Base +unsafeCoerce = GHC.Base.unsafeCoerce# +#else +-- HUGS +import qualified IOExts +unsafeCoerce = IOExts.unsafeCoerce +#endif" ++ fnl2 ()) + ++ + (if not usf.mldummy then mt () + else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) + +let pp_abst = function + | [] -> (mt ()) + | l -> (str "\\" ++ + prlist_with_sep (fun () -> (str " ")) pr_id l ++ + str " ->" ++ spc ()) + +(*s The pretty-printer for haskell syntax *) + +let pp_global k r = + if is_inline_custom r then str (find_custom r) + else str (Common.pp_global k r) + +(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses + are needed or not. *) + +let kn_sig = + let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in + make_kn specif empty_dirpath (mk_label "sig") + +let rec pp_type par vl t = + let rec pp_rec par = function + | Tmeta _ | Tvar' _ -> assert false + | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i)) + | Tglob (r,[]) -> pp_global Type r + | Tglob (r,l) -> + if r = IndRef (mind_of_kn kn_sig,0) then + pp_type true vl (List.hd l) + else + pp_par par + (pp_global Type r ++ spc () ++ + prlist_with_sep spc (pp_type true vl) l) + | Tarr (t1,t2) -> + pp_par par + (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) + | Tdummy _ -> str "()" + | Tunknown -> str "()" + | Taxiom -> str "() -- AXIOM TO BE REALIZED\n" + in + hov 0 (pp_rec par t) + +(*s Pretty-printing of expressions. [par] indicates whether + parentheses are needed or not. [env] is the list of names for the + de Bruijn variables. [args] is the list of collected arguments + (already pretty-printed). *) + +let expr_needs_par = function + | MLlam _ -> true + | MLcase _ -> true + | _ -> false + + +let rec pp_expr par env args = + let par' = args <> [] || par + and apply st = pp_apply st par args in + function + | MLrel n -> + let id = get_db_name n env in apply (pr_id id) + | MLapp (f,args') -> + let stl = List.map (pp_expr true env []) args' in + pp_expr par env (stl @ args) f + | MLlam _ as a -> + let fl,a' = collect_lams a in + let fl,env' = push_vars (List.map id_of_mlid fl) env in + let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in + apply (pp_par par' st) + | MLletin (id,a1,a2) -> + let i,env' = push_vars [id_of_mlid id] env in + let pp_id = pr_id (List.hd i) + and pp_a1 = pp_expr false env [] a1 + and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in + hv 0 + (apply + (pp_par par' + (hv 0 + (hov 5 + (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++ + spc () ++ str "in") ++ + spc () ++ hov 0 pp_a2))) + | MLglob r -> + apply (pp_global Term r) + | MLcons (_,r,[]) -> + assert (args=[]); pp_global Cons r + | MLcons (_,r,[a]) -> + assert (args=[]); + pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) + | MLcons (_,r,args') -> + assert (args=[]); + pp_par par (pp_global Cons r ++ spc () ++ + prlist_with_sep spc (pp_expr true env []) args') + | MLcase (_,t, pv) when is_custom_match pv -> + let mkfun (_,ids,e) = + if ids <> [] then named_lams (List.rev ids) e + else dummy_lams (ast_lift 1 e) 1 + in + hov 2 (str (find_custom_match pv) ++ fnl () ++ + prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv + ++ pp_expr true env [] t) + | MLcase ((_,factors),t, pv) -> + apply (pp_par par' + (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++ + fnl () ++ str " " ++ pp_pat env factors pv))) + | MLfix (i,ids,defs) -> + let ids',env' = push_vars (List.rev (Array.to_list ids)) env in + pp_fix par env' i (Array.of_list (List.rev ids'),defs) args + | MLexn s -> + (* An [MLexn] may be applied, but I don't really care. *) + pp_par par (str "Prelude.error" ++ spc () ++ qs s) + | MLdummy -> + str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLmagic a -> + pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) + | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") + +and pp_pat env factors pv = + let pp_one_pat (name,ids,t) = + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in + let par = expr_needs_par t in + hov 2 (pp_global Cons name ++ + (match ids with + | [] -> mt () + | _ -> (str " " ++ + prlist_with_sep + (fun () -> (spc ())) pr_id (List.rev ids))) ++ + str " ->" ++ spc () ++ pp_expr par env' [] t) + in + let factor_br, factor_l = try match factors with + | BranchFun (i::_ as l) -> check_function_branch pv.(i), l + | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l + | _ -> MLdummy, [] + with Impossible -> MLdummy, [] + in + let par = expr_needs_par factor_br in + let last = Array.length pv - 1 in + prvecti + (fun i x -> if List.mem i factor_l then mt () else + (pp_one_pat pv.(i) ++ + if i = last && factor_l = [] then mt () else + fnl () ++ str " ")) pv + ++ + if factor_l = [] then mt () else match factors with + | BranchFun _ -> + let ids, env' = push_vars [anonymous_name] env in + pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + pp_expr par env' [] factor_br + | BranchCst _ -> + str "_ ->" ++ spc () ++ pp_expr par env [] factor_br + | BranchNone -> mt () + +(*s names of the functions ([ids]) are already pushed in [env], + and passed here just for convenience. *) + +and pp_fix par env i (ids,bl) args = + pp_par par + (v 0 + (v 2 (str "let" ++ fnl () ++ + prvect_with_sep fnl + (fun (fi,ti) -> pp_function env (pr_id fi) ti) + (array_map2 (fun a b -> a,b) ids bl)) ++ + fnl () ++ + hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) + +and pp_function env f t = + let bl,t' = collect_lams t in + let bl,env' = push_vars (List.map id_of_mlid bl) env in + (f ++ pr_binding (List.rev bl) ++ + str " =" ++ fnl () ++ str " " ++ + hov 2 (pp_expr false env' [] t')) + +(*s Pretty-printing of inductive types declaration. *) + +let pp_comment s = str "-- " ++ s ++ fnl () + +let pp_logical_ind packet = + pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ + pp_comment (str "with constructors : " ++ + prvect_with_sep spc pr_id packet.ip_consnames) + +let pp_singleton kn packet = + let l = rename_tvars keywords packet.ip_vars in + let l' = List.rev l in + hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++ + prlist_with_sep spc pr_id l ++ + (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++ + pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++ + pp_comment (str "singleton inductive, whose constructor was " ++ + pr_id packet.ip_consnames.(0))) + +let pp_one_ind ip pl cv = + let pl = rename_tvars keywords pl in + let pp_constructor (r,l) = + (pp_global Cons r ++ + match l with + | [] -> (mt ()) + | _ -> (str " " ++ + prlist_with_sep + (fun () -> (str " ")) (pp_type true pl) l)) + in + str (if Array.length cv = 0 then "type " else "data ") ++ + pp_global Type (IndRef ip) ++ str " " ++ + prlist_with_sep (fun () -> str " ") pr_lower_id pl ++ + (if pl = [] then mt () else str " ") ++ + if Array.length cv = 0 then str "= () -- empty inductive" + else + (v 0 (str "= " ++ + prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor + (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv))) + +let rec pp_ind first kn i ind = + if i >= Array.length ind.ind_packets then + if first then mt () else fnl () + else + let ip = (kn,i) in + let p = ind.ind_packets.(i) in + if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind + else + if p.ip_logical then + pp_logical_ind p ++ pp_ind first kn (i+1) ind + else + pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ + pp_ind false kn (i+1) ind + + +(*s Pretty-printing of a declaration. *) + +let pp_string_parameters ids = prlist (fun id -> str id ++ str " ") + +let pp_decl = function + | Dind (kn,i) when i.ind_info = Singleton -> + pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl () + | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i) + | Dtype (r, l, t) -> + if is_inline_custom r then mt () + else + let l = rename_tvars keywords l in + let st = + try + let ids,s = find_type_custom r in + prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s + with not_found -> + prlist (fun id -> pr_id id ++ str " ") l ++ + if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n" + else str "=" ++ spc () ++ pp_type false l t + in + hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () + | Dfix (rv, defs, typs) -> + let max = Array.length rv in + let rec iter i = + if i = max then mt () + else + let e = pp_global Term rv.(i) in + e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () + ++ pp_function (empty_env ()) e defs.(i) ++ fnl2 () + ++ iter (i+1) + in iter 0 + | Dterm (r, a, t) -> + if is_inline_custom r then mt () + else + let e = pp_global Term r in + e ++ str " :: " ++ pp_type false [] t ++ fnl () ++ + if is_custom r then + hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ()) + else + hov 0 (pp_function (empty_env ()) e a ++ fnl2 ()) + +let rec pp_structure_elem = function + | (l,SEdecl d) -> pp_decl d + | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr + | (l,SEmodtype m) -> mt () + (* for the moment we simply discard module type *) + +and pp_module_expr = function + | MEstruct (mp,sel) -> prlist_strict pp_structure_elem sel + | MEfunctor _ -> mt () + (* for the moment we simply discard unapplied functors *) + | MEident _ | MEapply _ -> assert false + (* should be expansed in extract_env *) + +let pp_struct = + let pp_sel (mp,sel) = + push_visible mp []; + let p = prlist_strict pp_structure_elem sel in + pop_visible (); p + in + prlist_strict pp_sel + + +let haskell_descr = { + keywords = keywords; + file_suffix = ".hs"; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli new file mode 100644 index 00000000..1b5dbc71 --- /dev/null +++ b/plugins/extraction/haskell.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +val haskell_descr : Miniml.language_descr + diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli new file mode 100644 index 00000000..61b3fc13 --- /dev/null +++ b/plugins/extraction/miniml.mli @@ -0,0 +1,201 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*s Target language for extraction: a core ML called MiniML. *) + +open Pp +open Util +open Names +open Libnames + +(* The [signature] type is used to know how many arguments a CIC + object expects, and what these arguments will become in the ML + object. *) + +(* We eliminate from terms: 1) types 2) logical parts. + [Kother] stands both for logical or other reasons + (for instance user-declared implicit arguments w.r.t. extraction). *) + +type kill_reason = Ktype | Kother + +type sign = Keep | Kill of kill_reason + + +(* Convention: outmost lambda/product gives the head of the list. *) + +type signature = sign list + +(*s ML type expressions. *) + +type ml_type = + | Tarr of ml_type * ml_type + | Tglob of global_reference * ml_type list + | Tvar of int + | Tvar' of int (* same as Tvar, used to avoid clash *) + | Tmeta of ml_meta (* used during ML type reconstruction *) + | Tdummy of kill_reason + | Tunknown + | Taxiom + +and ml_meta = { id : int; mutable contents : ml_type option } + +(* ML type schema. + The integer is the number of variable in the schema. *) + +type ml_schema = int * ml_type + +(*s ML inductive types. *) + +type inductive_info = + | Singleton + | Coinductive + | Standard + | Record of global_reference list + +(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. + If the inductive is logical ([ip_logical = false]), then all other fields + are unused. Otherwise, + [ip_sign] is a signature concerning the arguments of the inductive, + [ip_vars] contains the names of the type variables surviving in ML, + [ip_types] contains the ML types of all constructors. +*) + +type ml_ind_packet = { + ip_typename : identifier; + ip_consnames : identifier array; + ip_logical : bool; + ip_sign : signature; + ip_vars : identifier list; + ip_types : (ml_type list) array; + mutable ip_optim_id_ok : bool option +} + +(* [ip_nparams] contains the number of parameters. *) + +type equiv = + | NoEquiv + | Equiv of kernel_name + | RenEquiv of string + +type ml_ind = { + ind_info : inductive_info; + ind_nparams : int; + ind_packets : ml_ind_packet array; + ind_equiv : equiv +} + +(*s ML terms. *) + +type ml_ident = + | Dummy + | Id of identifier + | Tmp of identifier + +(* list of branches to merge in a common pattern *) + +type case_info = + | BranchNone + | BranchFun of int list + | BranchCst of int list + +type ml_branch = global_reference * ml_ident list * ml_ast + +and ml_ast = + | MLrel of int + | MLapp of ml_ast * ml_ast list + | MLlam of ml_ident * ml_ast + | MLletin of ml_ident * ml_ast * ml_ast + | MLglob of global_reference + | MLcons of inductive_info * global_reference * ml_ast list + | MLcase of (inductive_info*case_info) * ml_ast * ml_branch array + | MLfix of int * identifier array * ml_ast array + | MLexn of string + | MLdummy + | MLaxiom + | MLmagic of ml_ast + +(*s ML declarations. *) + +type ml_decl = + | Dind of kernel_name * ml_ind + | Dtype of global_reference * identifier list * ml_type + | Dterm of global_reference * ml_ast * ml_type + | Dfix of global_reference array * ml_ast array * ml_type array + +type ml_spec = + | Sind of kernel_name * ml_ind + | Stype of global_reference * identifier list * ml_type option + | Sval of global_reference * ml_type + +type ml_specif = + | Spec of ml_spec + | Smodule of ml_module_type + | Smodtype of ml_module_type + +and ml_module_type = + | MTident of module_path + | MTfunsig of mod_bound_id * ml_module_type * ml_module_type + | MTsig of module_path * ml_module_sig + | MTwith of ml_module_type * ml_with_declaration + +and ml_with_declaration = + | ML_With_type of identifier list * identifier list * ml_type + | ML_With_module of identifier list * module_path + +and ml_module_sig = (label * ml_specif) list + +type ml_structure_elem = + | SEdecl of ml_decl + | SEmodule of ml_module + | SEmodtype of ml_module_type + +and ml_module_expr = + | MEident of module_path + | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr + | MEstruct of module_path * ml_module_structure + | MEapply of ml_module_expr * ml_module_expr + +and ml_module_structure = (label * ml_structure_elem) list + +and ml_module = + { ml_mod_expr : ml_module_expr; + ml_mod_type : ml_module_type } + +(* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp] + implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *) + +type ml_structure = (module_path * ml_module_structure) list + +type ml_signature = (module_path * ml_module_sig) list + +type unsafe_needs = { + mldummy : bool; + tdummy : bool; + tunknown : bool; + magic : bool +} + +type language_descr = { + keywords : Idset.t; + + (* Concerning the source file *) + file_suffix : string; + preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; + pp_struct : ml_structure -> std_ppcmds; + + (* Concerning a possible interface file *) + sig_suffix : string option; + sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; + pp_sig : ml_signature -> std_ppcmds; + + (* for an isolated declaration print *) + pp_decl : ml_decl -> std_ppcmds; + +} diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml new file mode 100644 index 00000000..6dd43c44 --- /dev/null +++ b/plugins/extraction/mlutil.ml @@ -0,0 +1,1293 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*i*) +open Pp +open Util +open Names +open Libnames +open Nametab +open Table +open Miniml +(*i*) + +(*s Exceptions. *) + +exception Found +exception Impossible + +(*S Names operations. *) + +let anonymous_name = id_of_string "x" +let dummy_name = id_of_string "_" + +let anonymous = Id anonymous_name + +let id_of_name = function + | Anonymous -> anonymous_name + | Name id when id = dummy_name -> anonymous_name + | Name id -> id + +let id_of_mlid = function + | Dummy -> dummy_name + | Id id -> id + | Tmp id -> id + +let tmp_id = function + | Id id -> Tmp id + | a -> a + +let is_tmp = function Tmp _ -> true | _ -> false + +(*S Operations upon ML types (with meta). *) + +let meta_count = ref 0 + +let reset_meta_count () = meta_count := 0 + +let new_meta _ = + incr meta_count; + Tmeta {id = !meta_count; contents = None} + +(*s Sustitution of [Tvar i] by [t] in a ML type. *) + +let type_subst i t0 t = + let rec subst t = match t with + | Tvar j when i = j -> t0 + | Tmeta {contents=None} -> t + | Tmeta {contents=Some u} -> subst u + | Tarr (a,b) -> Tarr (subst a, subst b) + | Tglob (r, l) -> Tglob (r, List.map subst l) + | a -> a + in subst t + +(* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *) + +let type_subst_list l t = + let rec subst t = match t with + | Tvar j -> List.nth l (j-1) + | Tmeta {contents=None} -> t + | Tmeta {contents=Some u} -> subst u + | Tarr (a,b) -> Tarr (subst a, subst b) + | Tglob (r, l) -> Tglob (r, List.map subst l) + | a -> a + in subst t + +(* Simultaneous substitution of [[|Tvar 1; ... ; Tvar n|]] by [v] in a ML type. *) + +let type_subst_vect v t = + let rec subst t = match t with + | Tvar j -> v.(j-1) + | Tmeta {contents=None} -> t + | Tmeta {contents=Some u} -> subst u + | Tarr (a,b) -> Tarr (subst a, subst b) + | Tglob (r, l) -> Tglob (r, List.map subst l) + | a -> a + in subst t + +(*s From a type schema to a type. All [Tvar] become fresh [Tmeta]. *) + +let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t + +(*s Occur-check of a free meta in a type *) + +let rec type_occurs alpha t = + match t with + | Tmeta {id=beta; contents=None} -> alpha = beta + | Tmeta {contents=Some u} -> type_occurs alpha u + | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2 + | Tglob (r,l) -> List.exists (type_occurs alpha) l + | _ -> false + +(*s Most General Unificator *) + +let rec mgu = function + | Tmeta m, Tmeta m' when m.id = m'.id -> () + | Tmeta m, t when m.contents=None -> + if type_occurs m.id t then raise Impossible + else m.contents <- Some t + | t, Tmeta m when m.contents=None -> + if type_occurs m.id t then raise Impossible + else m.contents <- Some t + | Tmeta {contents=Some u}, t -> mgu (u, t) + | t, Tmeta {contents=Some u} -> mgu (t, u) + | Tarr(a, b), Tarr(a', b') -> + mgu (a, a'); mgu (b, b') + | Tglob (r,l), Tglob (r',l') when r = r' -> + List.iter mgu (List.combine l l') + | Tvar i, Tvar j when i = j -> () + | Tvar' i, Tvar' j when i = j -> () + | Tdummy _, Tdummy _ -> () + | Tunknown, Tunknown -> () + | _ -> raise Impossible + +let needs_magic p = try mgu p; false with Impossible -> true + +let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a + +let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a + + +(*S ML type env. *) + +module Mlenv = struct + + let meta_cmp m m' = compare m.id m'.id + module Metaset = Set.Make(struct type t = ml_meta let compare = meta_cmp end) + + (* Main MLenv type. [env] is the real environment, whereas [free] + (tries to) record the free meta variables occurring in [env]. *) + + type t = { env : ml_schema list; mutable free : Metaset.t} + + (* Empty environment. *) + + let empty = { env = []; free = Metaset.empty } + + (* [get] returns a instantiated copy of the n-th most recently added + type in the environment. *) + + let get mle n = + assert (List.length mle.env >= n); + instantiation (List.nth mle.env (n-1)) + + (* [find_free] finds the free meta in a type. *) + + let rec find_free set = function + | Tmeta m when m.contents = None -> Metaset.add m set + | Tmeta {contents = Some t} -> find_free set t + | Tarr (a,b) -> find_free (find_free set a) b + | Tglob (_,l) -> List.fold_left find_free set l + | _ -> set + + (* The [free] set of an environment can be outdate after + some unifications. [clean_free] takes care of that. *) + + let clean_free mle = + let rem = ref Metaset.empty + and add = ref Metaset.empty in + let clean m = match m.contents with + | None -> () + | Some u -> rem := Metaset.add m !rem; add := find_free !add u + in + Metaset.iter clean mle.free; + mle.free <- Metaset.union (Metaset.diff mle.free !rem) !add + + (* From a type to a type schema. If a [Tmeta] is still uninstantiated + and does appears in the [mle], then it becomes a [Tvar]. *) + + let generalization mle t = + let c = ref 0 in + let map = ref (Intmap.empty : int Intmap.t) in + let add_new i = incr c; map := Intmap.add i !c !map; !c in + let rec meta2var t = match t with + | Tmeta {contents=Some u} -> meta2var u + | Tmeta ({id=i} as m) -> + (try Tvar (Intmap.find i !map) + with Not_found -> + if Metaset.mem m mle.free then t + else Tvar (add_new i)) + | Tarr (t1,t2) -> Tarr (meta2var t1, meta2var t2) + | Tglob (r,l) -> Tglob (r, List.map meta2var l) + | t -> t + in !c, meta2var t + + (* Adding a type in an environment, after generalizing. *) + + let push_gen mle t = + clean_free mle; + { env = generalization mle t :: mle.env; free = mle.free } + + (* Adding a type with no [Tvar], hence no generalization needed. *) + + let push_type {env=e;free=f} t = + { env = (0,t) :: e; free = find_free f t} + + (* Adding a type with no [Tvar] nor [Tmeta]. *) + + let push_std_type {env=e;free=f} t = + { env = (0,t) :: e; free = f} + +end + +(*S Operations upon ML types (without meta). *) + +(*s Does a section path occur in a ML type ? *) + +let rec type_mem_kn kn = function + | Tmeta {contents = Some t} -> type_mem_kn kn t + | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l + | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b) + | _ -> false + +(*s Greatest variable occurring in [t]. *) + +let type_maxvar t = + let rec parse n = function + | Tmeta {contents = Some t} -> parse n t + | Tvar i -> max i n + | Tarr (a,b) -> parse (parse n a) b + | Tglob (_,l) -> List.fold_left parse n l + | _ -> n + in parse 0 t + +(*s What are the type variables occurring in [t]. *) + +let intset_union_map_list f l = + List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l + +let intset_union_map_array f a = + Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a + +let rec type_listvar = function + | Tmeta {contents = Some t} -> type_listvar t + | Tvar i | Tvar' i -> Intset.singleton i + | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b) + | Tglob (_,l) -> intset_union_map_list type_listvar l + | _ -> Intset.empty + +(*s From [a -> b -> c] to [[a;b],c]. *) + +let rec type_decomp = function + | Tmeta {contents = Some t} -> type_decomp t + | Tarr (a,b) -> let l,h = type_decomp b in a::l, h + | a -> [],a + +(*s The converse: From [[a;b],c] to [a -> b -> c]. *) + +let rec type_recomp (l,t) = match l with + | [] -> t + | a::l -> Tarr (a, type_recomp (l,t)) + +(*s Translating [Tvar] to [Tvar'] to avoid clash. *) + +let rec var2var' = function + | Tmeta {contents = Some t} -> var2var' t + | Tvar i -> Tvar' i + | Tarr (a,b) -> Tarr (var2var' a, var2var' b) + | Tglob (r,l) -> Tglob (r, List.map var2var' l) + | a -> a + +type abbrev_map = global_reference -> ml_type option + +(*s Delta-reduction of type constants everywhere in a ML type [t]. + [env] is a function of type [ml_type_env]. *) + +let type_expand env t = + let rec expand = function + | Tmeta {contents = Some t} -> expand t + | Tglob (r,l) -> + (match env r with + | Some mlt -> expand (type_subst_list l mlt) + | None -> Tglob (r, List.map expand l)) + | Tarr (a,b) -> Tarr (expand a, expand b) + | a -> a + in if Table.type_expand () then expand t else t + +(*s Generating a signature from a ML type. *) + +let type_to_sign env t = match type_expand env t with + | Tdummy d -> Kill d + | _ -> Keep + +let type_to_signature env t = + let rec f = function + | Tmeta {contents = Some t} -> f t + | Tarr (Tdummy d, b) -> Kill d :: f b + | Tarr (_, b) -> Keep :: f b + | _ -> [] + in f (type_expand env t) + +let isKill = function Kill _ -> true | _ -> false + +let isDummy = function Tdummy _ -> true | _ -> false + +let sign_of_id = function + | Dummy -> Kill Kother + | _ -> Keep + +(* Classification of signatures *) + +type sign_kind = + | EmptySig + | NonLogicalSig (* at least a [Keep] *) + | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) + | SafeLogicalSig (* only [Kill Ktype] *) + +let rec sign_kind = function + | [] -> EmptySig + | Keep :: _ -> NonLogicalSig + | Kill k :: s -> + match sign_kind s with + | NonLogicalSig -> NonLogicalSig + | UnsafeLogicalSig -> UnsafeLogicalSig + | SafeLogicalSig | EmptySig -> + if k = Kother then UnsafeLogicalSig else SafeLogicalSig + +(* Removing the final [Keep] in a signature *) + +let rec sign_no_final_keeps = function + | [] -> [] + | k :: s -> + let s' = k :: sign_no_final_keeps s in + if s' = [Keep] then [] else s' + +(*s Removing [Tdummy] from the top level of a ML type. *) + +let type_expunge_from_sign env s t = + let rec expunge s t = + if s = [] then t else match t with + | Tmeta {contents = Some t} -> expunge s t + | Tarr (a,b) -> + let t = expunge (List.tl s) b in + if List.hd s = Keep then Tarr (a, t) else t + | Tglob (r,l) -> + (match env r with + | Some mlt -> expunge s (type_subst_list l mlt) + | None -> assert false) + | _ -> assert false + in + let t = expunge (sign_no_final_keeps s) t in + if lang () <> Haskell && sign_kind s = UnsafeLogicalSig then + Tarr (Tdummy Kother, t) + else t + +let type_expunge env t = + type_expunge_from_sign env (type_to_signature env t) t + +(*S Generic functions over ML ast terms. *) + +let mlapp f a = if a = [] then f else MLapp (f,a) + +(*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care + of the number of bingings crossed before reaching the [MLrel]. *) + +let ast_iter_rel f = + let rec iter n = function + | MLrel i -> f (i-n) + | MLlam (_,a) -> iter (n+1) a + | MLletin (_,a,b) -> iter n a; iter (n+1) b + | MLcase (_,a,v) -> + iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v + | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v + | MLapp (a,l) -> iter n a; List.iter (iter n) l + | MLcons (_,_,l) -> List.iter (iter n) l + | MLmagic a -> iter n a + | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () + in iter 0 + +(*s Map over asts. *) + +let ast_map_case f (c,ids,a) = (c,ids,f a) + +let ast_map f = function + | MLlam (i,a) -> MLlam (i, f a) + | MLletin (i,a,b) -> MLletin (i, f a, f b) + | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v) + | MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v) + | MLapp (a,l) -> MLapp (f a, List.map f l) + | MLcons (i,c,l) -> MLcons (i,c, List.map f l) + | MLmagic a -> MLmagic (f a) + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a + +(*s Map over asts, with binding depth as parameter. *) + +let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a) + +let ast_map_lift f n = function + | MLlam (i,a) -> MLlam (i, f (n+1) a) + | MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b) + | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v) + | MLfix (i,ids,v) -> + let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v) + | MLapp (a,l) -> MLapp (f n a, List.map (f n) l) + | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l) + | MLmagic a -> MLmagic (f n a) + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a + +(*s Iter over asts. *) + +let ast_iter_case f (c,ids,a) = f a + +let ast_iter f = function + | MLlam (i,a) -> f a + | MLletin (i,a,b) -> f a; f b + | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v + | MLfix (i,ids,v) -> Array.iter f v + | MLapp (a,l) -> f a; List.iter f l + | MLcons (_,c,l) -> List.iter f l + | MLmagic a -> f a + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () + +(*S Operations concerning De Bruijn indices. *) + +(*s [ast_occurs k t] returns [true] if [(Rel k)] occurs in [t]. *) + +let ast_occurs k t = + try + ast_iter_rel (fun i -> if i = k then raise Found) t; false + with Found -> true + +(*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)] + in [t] with [k<=i<=k'] *) + +let ast_occurs_itvl k k' t = + try + ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false + with Found -> true + +(*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *) + +let nb_occur_k k t = + let cpt = ref 0 in + ast_iter_rel (fun i -> if i = k then incr cpt) t; + !cpt + +let nb_occur t = nb_occur_k 1 t + +(* Number of occurences of [Rel 1] in [t], with special treatment of match: + occurences in different branches aren't added, but we rather use max. *) + +let nb_occur_match = + let rec nb k = function + | MLrel i -> if i = k then 1 else 0 + | MLcase(_,a,v) -> + (nb k a) + + Array.fold_left + (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v + | MLletin (_,a,b) -> (nb k a) + (nb (k+1) b) + | MLfix (_,ids,v) -> let k = k+(Array.length ids) in + Array.fold_left (fun r a -> r+(nb k a)) 0 v + | MLlam (_,a) -> nb (k+1) a + | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l + | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l + | MLmagic a -> nb k a + | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0 + in nb 1 + +(*s Lifting on terms. + [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *) + +let ast_lift k t = + let rec liftrec n = function + | MLrel i as a -> if i-n < 1 then a else MLrel (i+k) + | a -> ast_map_lift liftrec n a + in if k = 0 then t else liftrec 0 t + +let ast_pop t = ast_lift (-1) t + +(*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ... + Rel (k'+k)] and [Rel (k+1) ... Rel (k+k')] to [Rel 1 ... Rel k'] *) + +let permut_rels k k' = + let rec permut n = function + | MLrel i as a -> + let i' = i-n in + if i'<1 || i'>k+k' then a + else if i'<=k then MLrel (i+k') + else MLrel (i-k) + | a -> ast_map_lift permut n a + in permut 0 + +(*s Substitution. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. + Lifting (of one binder) is done at the same time. *) + +let ast_subst e = + let rec subst n = function + | MLrel i as a -> + let i' = i-n in + if i'=1 then ast_lift n e + else if i'<1 then a + else MLrel (i-1) + | a -> ast_map_lift subst n a + in subst 0 + +(*s Generalized substitution. + [gen_subst v d t] applies to [t] the substitution coded in the + [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies + to [Rel] greater than [Array.length v]. *) + +let gen_subst v d t = + let rec subst n = function + | MLrel i as a -> + let i'= i-n in + if i' < 1 then a + else if i' <= Array.length v then + match v.(i'-1) with + | None -> MLexn ("UNBOUND " ^ string_of_int i') + | Some u -> ast_lift n u + else MLrel (i+d) + | a -> ast_map_lift subst n a + in subst 0 t + +(*S Operations concerning lambdas. *) + +(*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns + [[idn;...;id1]] and the term [t]. *) + +let collect_lams = + let rec collect acc = function + | MLlam(id,t) -> collect (id::acc) t + | x -> acc,x + in collect [] + +(*s [collect_n_lams] does the same for a precise number of [MLlam]. *) + +let collect_n_lams = + let rec collect acc n t = + if n = 0 then acc,t + else match t with + | MLlam(id,t) -> collect (id::acc) (n-1) t + | _ -> assert false + in collect [] + +(*s [remove_n_lams] just removes some [MLlam]. *) + +let rec remove_n_lams n t = + if n = 0 then t + else match t with + | MLlam(_,t) -> remove_n_lams (n-1) t + | _ -> assert false + +(*s [nb_lams] gives the number of head [MLlam]. *) + +let rec nb_lams = function + | MLlam(_,t) -> succ (nb_lams t) + | _ -> 0 + +(*s [named_lams] does the converse of [collect_lams]. *) + +let rec named_lams ids a = match ids with + | [] -> a + | id :: ids -> named_lams ids (MLlam (id,a)) + +(*s The same for a specific identifier (resp. anonymous, dummy) *) + +let rec many_lams id a = function + | 0 -> a + | n -> many_lams id (MLlam (id,a)) (pred n) + +let anonym_lams a n = many_lams anonymous a n +let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n +let dummy_lams a n = many_lams Dummy a n + +(*s mixed according to a signature. *) + +let rec anonym_or_dummy_lams a = function + | [] -> a + | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s) + | Kill _ :: s -> MLlam(Dummy, anonym_or_dummy_lams a s) + +(*S Operations concerning eta. *) + +(*s The following function creates [MLrel n;...;MLrel 1] *) + +let rec eta_args n = + if n = 0 then [] else (MLrel n)::(eta_args (pred n)) + +(*s Same, but filtered by a signature. *) + +let rec eta_args_sign n = function + | [] -> [] + | Keep :: s -> (MLrel n) :: (eta_args_sign (n-1) s) + | Kill _ :: s -> eta_args_sign (n-1) s + +(*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *) + +let rec test_eta_args_lift k n = function + | [] -> n=0 + | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q) + +(*s Computes an eta-reduction. *) + +let eta_red e = + let ids,t = collect_lams e in + let n = List.length ids in + if n = 0 then e + else match t with + | MLapp (f,a) -> + let m = List.length a in + let ids,body,args = + if m = n then + [], f, a + else if m < n then + list_skipn m ids, f, a + else (* m > n *) + let a1,a2 = list_chop (m-n) a in + [], MLapp (f,a1), a2 + in + let p = List.length args in + if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body) + then named_lams ids (ast_lift (-p) body) + else e + | _ -> e + +(*s Computes all head linear beta-reductions possible in [(t a)]. + Non-linear head beta-redex become let-in. *) + +let rec linear_beta_red a t = match a,t with + | [], _ -> t + | a0::a, MLlam (id,t) -> + (match nb_occur_match t with + | 0 -> linear_beta_red a (ast_pop t) + | 1 -> linear_beta_red a (ast_subst a0 t) + | _ -> + let a = List.map (ast_lift 1) a in + MLletin (id, a0, linear_beta_red a t)) + | _ -> MLapp (t, a) + +let rec tmp_head_lams = function + | MLlam (id, t) -> MLlam (tmp_id id, tmp_head_lams t) + | e -> e + +(*s Applies a substitution [s] of constants by their body, plus + linear beta reductions at modified positions. + Moreover, we mark some lambdas as suitable for later linear + reduction (this helps the inlining of recursors). +*) + +let rec ast_glob_subst s t = match t with + | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> + let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in + (try linear_beta_red a (Refmap.find refe s) + with Not_found -> MLapp (f, a)) + | MLglob ((ConstRef kn) as refe) -> + (try Refmap.find refe s with Not_found -> t) + | _ -> ast_map (ast_glob_subst s) t + + +(*S Auxiliary functions used in simplification of ML cases. *) + +(*s [check_function_branch (r,l,c)] checks if branch [c] can be seen + as a function [f] applied to [MLcons(r,l)]. For that it transforms + any [MLcons(r,l)] in [MLrel 1] and raises [Impossible] if any + variable in [l] occurs outside such a [MLcons] *) + +let check_function_branch (r,l,c) = + let nargs = List.length l in + let rec genrec n = function + | MLrel i as c -> + let i' = i-n in + if i'<1 then c + else if i'>nargs then MLrel (i-nargs+1) + else raise Impossible + | MLcons(_,r',args) when r=r' && (test_eta_args_lift n nargs args) -> + MLrel (n+1) + | a -> ast_map_lift genrec n a + in genrec 0 c + +(*s [check_constant_branch (r,l,c)] checks if branch [c] is independent + from the pattern [MLcons(r,l)]. For that is raises [Impossible] if any + variable in [l] occurs in [c], and otherwise returns [c] lifted to + appear like a function with one arg (for uniformity with the + branch-as-function optimization) *) + +let check_constant_branch (_,l,c) = + let n = List.length l in + if ast_occurs_itvl 1 n c then raise Impossible; + ast_lift (1-n) c + +(* The following structure allows to record which element occurred + at what position, and then finally return the most frequent + element and its positions. *) + +let census_add, census_max, census_clean = + let h = Hashtbl.create 13 in + let clear () = Hashtbl.clear h in + let add e i = + let l = try Hashtbl.find h e with Not_found -> [] in + Hashtbl.replace h e (i::l) + in + let max e0 = + let len = ref 0 and lst = ref [] and elm = ref e0 in + Hashtbl.iter + (fun e l -> + let n = List.length l in + if n > !len then begin len := n; lst := l; elm := e end) + h; + (!elm,!lst) + in + (add,max,clear) + +(* Given an abstraction function [abstr] (one of [check_*_branch]), + return the longest possible list of branches that have the + same abstraction, along with this abstraction. *) + +let factor_branches abstr br = + census_clean (); + for i = 0 to Array.length br - 1 do + try census_add (abstr br.(i)) i with Impossible -> () + done; + let br_factor, br_list = census_max MLdummy in + if br_list = [] then None + else if Array.length br >= 2 && List.length br_list < 2 then None + else Some (br_factor, br_list) + +(*s [check_generalizable_case] checks if all branches can be seen as the + same function [f] applied to the term matched. It is a generalized version + of both the identity case optimization and the constant case optimisation + ([f] can be a constant function) *) + +(* The optimisation [factor_branches check_function_branch] breaks types + in some special case. Example: [type 'x a = A]. + Then [let f = function A -> A] has type ['x a -> 'y a], + which is incompatible with the type of [let f x = x]. + We check first that there isn't such phantom variable in the inductive type + we're considering. *) + +let check_optim_id br = + let (kn,i) = + match br.(0) with (ConstructRef (c,_),_,_) -> c | _ -> assert false + in + let ip = (snd (lookup_ind kn)).ind_packets.(i) in + match ip.ip_optim_id_ok with + | Some ok -> ok + | None -> + let tvars = + intset_union_map_array (intset_union_map_list type_listvar) + ip.ip_types + in + let ok = (Intset.cardinal tvars = List.length ip.ip_vars) in + ip.ip_optim_id_ok <- Some ok; + ok + +(*s If all branches are functions, try to permut the case and the functions. *) + +let rec merge_ids ids ids' = match ids,ids' with + | [],l -> l + | l,[] -> l + | i::ids, i'::ids' -> + (if i = Dummy then i' else i) :: (merge_ids ids ids') + +let is_exn = function MLexn _ -> true | _ -> false + +let rec permut_case_fun br acc = + let nb = ref max_int in + Array.iter (fun (_,_,t) -> + let ids, c = collect_lams t in + let n = List.length ids in + if (n < !nb) && (not (is_exn c)) then nb := n) br; + if !nb = max_int || !nb = 0 then ([],br) + else begin + let br = Array.copy br in + let ids = ref [] in + for i = 0 to Array.length br - 1 do + let (r,l,t) = br.(i) in + let local_nb = nb_lams t in + if local_nb < !nb then (* t = MLexn ... *) + br.(i) <- (r,l,remove_n_lams local_nb t) + else begin + let local_ids,t = collect_n_lams !nb t in + ids := merge_ids !ids local_ids; + br.(i) <- (r,l,permut_rels !nb (List.length l) t) + end + done; + (!ids,br) + end + +(*S Generalized iota-reduction. *) + +(* Definition of a generalized iota-redex: it's a [MLcase(e,_)] + with [(is_iota_gen e)=true]. Any generalized iota-redex is + transformed into beta-redexes. *) + +let rec is_iota_gen = function + | MLcons _ -> true + | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br + | _ -> false + +let constructor_index = function + | ConstructRef (_,j) -> pred j + | _ -> assert false + +let iota_gen br = + let rec iota k = function + | MLcons (i,r,a) -> + let (_,ids,c) = br.(constructor_index r) in + let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in + let c = ast_lift k c in + MLapp (c,a) + | MLcase(i,e,br') -> + let new_br = + Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br' + in MLcase(i,e, new_br) + | _ -> assert false + in iota 0 + +let is_atomic = function + | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true + | _ -> false + +let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false + +(*S The main simplification function. *) + +(* Some beta-iota reductions + simplifications. *) + +let rec simpl o = function + | MLapp (f, []) -> simpl o f + | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f) + | MLcase (i,e,br) -> + let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in + simpl_case o i br (simpl o e) + | MLletin(Dummy,_,e) -> simpl o (ast_pop e) + | MLletin(id,c,e) -> + let e = simpl o e in + if + (is_atomic c) || (is_atomic e) || + (let n = nb_occur_match e in + (n = 0 || (n=1 && (is_tmp id || is_imm_apply e || o.opt_lin_let)))) + then + simpl o (ast_subst c e) + else + MLletin(id, simpl o c, e) + | MLfix(i,ids,c) -> + let n = Array.length ids in + if ast_occurs_itvl 1 n c.(i) then + MLfix (i, ids, Array.map (simpl o) c) + else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *) + | a -> ast_map (simpl o) a + +(* invariant : list [a] of arguments is non-empty *) + +and simpl_app o a = function + | MLapp (f',a') -> simpl_app o (a'@a) f' + | MLlam (Dummy,t) -> + simpl o (MLapp (ast_pop t, List.tl a)) + | MLlam (id,t) -> (* Beta redex *) + (match nb_occur_match t with + | 0 -> simpl o (MLapp (ast_pop t, List.tl a)) + | 1 when (is_tmp id || o.opt_lin_beta) -> + simpl o (MLapp (ast_subst (List.hd a) t, List.tl a)) + | _ -> + let a' = List.map (ast_lift 1) (List.tl a) in + simpl o (MLletin (id, List.hd a, MLapp (t, a')))) + | MLletin (id,e1,e2) when o.opt_let_app -> + (* Application of a letin: we push arguments inside *) + MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a))) + | MLcase (i,e,br) when o.opt_case_app -> + (* Application of a case: we push arguments inside *) + let br' = + Array.map + (fun (n,l,t) -> + let k = List.length l in + let a' = List.map (ast_lift k) a in + (n, l, simpl o (MLapp (t,a')))) br + in simpl o (MLcase (i,e,br')) + | (MLdummy | MLexn _) as e -> e + (* We just discard arguments in those cases. *) + | f -> MLapp (f,a) + +(* Invariant : all empty matches should now be [MLexn] *) + +and simpl_case o i br e = + if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *) + simpl o (iota_gen br e) + else + (* Swap the case and the lam if possible *) + let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in + let n = List.length ids in + if n <> 0 then + simpl o (named_lams ids (MLcase (i,ast_lift n e, br))) + else + (* Does a term [f] exist such that many branches are [(f e)] ? *) + let opt1 = + if o.opt_case_idr && (o.opt_case_idg || check_optim_id br) then + factor_branches check_function_branch br + else None + in + (* Detect common constant branches. Often a particular case of + branch-as-function optim, but not always (e.g. A->A|B->A) *) + let opt2 = + if opt1 = None && o.opt_case_cst then + factor_branches check_constant_branch br + else opt1 + in + match opt2 with + | Some (f,ints) when List.length ints = Array.length br -> + (* if all branches have been factorized, we remove the match *) + simpl o (MLletin (Tmp anonymous_name, e, f)) + | Some (f,ints) -> + let ci = if ast_occurs 1 f then BranchFun ints else BranchCst ints + in MLcase ((fst i,ci), e, br) + | None -> MLcase (i, e, br) + +(*S Local prop elimination. *) +(* We try to eliminate as many [prop] as possible inside an [ml_ast]. *) + +(*s In a list, it selects only the elements corresponding to a [Keep] + in the boolean list [l]. *) + +let rec select_via_bl l args = match l,args with + | [],_ -> args + | Keep::l,a::args -> a :: (select_via_bl l args) + | Kill _::l,a::args -> select_via_bl l args + | _ -> assert false + +(*s [kill_some_lams] removes some head lambdas according to the signature [bl]. + This list is build on the identifier list model: outermost lambda + is on the right. + [Rels] corresponding to removed lambdas are supposed not to occur, and + the other [Rels] are made correct via a [gen_subst]. + Output is not directly a [ml_ast], compose with [named_lams] if needed. *) + +let kill_some_lams bl (ids,c) = + let n = List.length bl in + let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in + if n = n' then ids,c + else if n' = 0 then [],ast_lift (-n) c + else begin + let v = Array.make n None in + let rec parse_ids i j = function + | [] -> () + | Keep :: l -> v.(i) <- Some (MLrel j); parse_ids (i+1) (j+1) l + | Kill _ :: l -> parse_ids (i+1) j l + in parse_ids 0 1 bl; + select_via_bl bl ids, gen_subst v (n'-n) c + end + +(*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding + to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or + if there is no lambda left at all. *) + +let kill_dummy_lams c = + let ids,c = collect_lams c in + let bl = List.map sign_of_id ids in + if (List.mem Keep bl) && (List.exists isKill bl) then + let ids',c = kill_some_lams bl (ids,c) in + ids, named_lams ids' c + else raise Impossible + +(*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c] + and a signature [s] and builds a eta-long version. *) + +(* For example, if [s = [Keep;Keep;Kill Prop;Keep]] then the output is : + [fun idn ... id1 x x _ x -> (c' 4 3 __ 1)] with [c' = lift 4 c] *) + +let eta_expansion_sign s (ids,c) = + let rec abs ids rels i = function + | [] -> + let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels + in ids, MLapp (ast_lift (i-1) c, a) + | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l + | Kill _ :: l -> abs (Dummy :: ids) (MLdummy :: rels) (i+1) l + in abs ids [] 1 s + +(*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e] + in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas + corresponding to [Del] in [s]. *) + +let case_expunge s e = + let m = List.length s in + let n = nb_lams e in + let p = if m <= n then collect_n_lams m e + else eta_expansion_sign (list_skipn n s) (collect_lams e) in + kill_some_lams (List.rev s) p + +(*s [term_expunge] takes a function [fun idn ... id1 -> c] + and a signature [s] and remove dummy lams. The difference + with [case_expunge] is that we here leave one dummy lambda + if all lambdas are logical dummy and the target language is strict. *) + +let term_expunge s (ids,c) = + if s = [] then c + else + let ids,c = kill_some_lams (List.rev s) (ids,c) in + if ids = [] && lang () <> Haskell && List.mem (Kill Kother) s then + MLlam (Dummy, ast_lift 1 c) + else named_lams ids c + +(*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and + purge the args of [t0] corresponding to a [dummy_name]. + It makes eta-expansion if needed. *) + +let kill_dummy_args ids t0 t = + let m = List.length ids in + let bl = List.rev_map sign_of_id ids in + let rec killrec n = function + | MLapp(e, a) when e = ast_lift n t0 -> + let k = max 0 (m - (List.length a)) in + let a = List.map (killrec n) a in + let a = List.map (ast_lift k) a in + let a = select_via_bl bl (a @ (eta_args k)) in + named_lams (list_firstn k ids) (MLapp (ast_lift k e, a)) + | e when e = ast_lift n t0 -> + let a = select_via_bl bl (eta_args m) in + named_lams ids (MLapp (ast_lift m e, a)) + | e -> ast_map_lift killrec n e + in killrec 0 t + +(*s The main function for local [dummy] elimination. *) + +let rec kill_dummy = function + | MLfix(i,fi,c) -> + (try + let ids,c = kill_dummy_fix i c in + ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1)) + with Impossible -> MLfix (i,fi,Array.map kill_dummy c)) + | MLapp (MLfix (i,fi,c),a) -> + let a = List.map kill_dummy a in + (try + let ids,c = kill_dummy_fix i c in + let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in + let fake' = kill_dummy_args ids (MLrel 1) fake in + ast_subst (MLfix (i,fi,c)) fake' + with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a)) + | MLletin(id, MLfix (i,fi,c),e) -> + (try + let ids,c = kill_dummy_fix i c in + let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in + MLletin(id, MLfix(i,fi,c),e) + with Impossible -> + MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e)) + | MLletin(id,c,e) -> + (try + let ids,c = kill_dummy_lams (kill_dummy_hd c) in + let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in + let c = eta_red (kill_dummy c) in + if is_atomic c then ast_subst c e else MLletin (id, c, e) + with Impossible -> MLletin(id,kill_dummy c,kill_dummy e)) + | a -> ast_map kill_dummy a + +(* Similar function, but acting only on head lambdas and let-ins *) + +and kill_dummy_hd = function + | MLlam(id,e) -> MLlam(id, kill_dummy_hd e) + | MLletin(id,c,e) -> + (try + let ids,c = kill_dummy_lams (kill_dummy_hd c) in + let e = kill_dummy_hd (kill_dummy_args ids (MLrel 1) e) in + let c = eta_red (kill_dummy c) in + if is_atomic c then ast_subst c e else MLletin (id, c, e) + with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e)) + | a -> a + +and kill_dummy_fix i c = + let n = Array.length c in + let ids,ci = kill_dummy_lams (kill_dummy_hd c.(i)) in + let c = Array.copy c in c.(i) <- ci; + for j = 0 to (n-1) do + c.(j) <- kill_dummy (kill_dummy_args ids (MLrel (n-i)) c.(j)) + done; + ids,c + +(*s Putting things together. *) + +let normalize a = + let o = optims () in + let rec norm a = + let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in + if a = a' then a else norm a' + in norm a + +(*S Special treatment of fixpoint for pretty-printing purpose. *) + +let general_optimize_fix f ids n args m c = + let v = Array.make n 0 in + for i=0 to (n-1) do v.(i)<-i done; + let aux i = function + | MLrel j when v.(j-1)>=0 -> + if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1) + | _ -> raise Impossible + in list_iter_i aux args; + let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in + let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in + let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in + MLfix(0,[|f|],[|new_c|]) + +let optimize_fix a = + if not (optims()).opt_fix_fun then a + else + let ids,a' = collect_lams a in + let n = List.length ids in + if n = 0 then a + else match a' with + | MLfix(_,[|f|],[|c|]) -> + let new_f = MLapp (MLrel (n+1),eta_args n) in + let new_c = named_lams ids (normalize (ast_subst new_f c)) + in MLfix(0,[|f|],[|new_c|]) + | MLapp(a',args) -> + let m = List.length args in + (match a' with + | MLfix(_,_,_) when + (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a') + -> a' + | MLfix(_,[|f|],[|c|]) -> + (try general_optimize_fix f ids n args m c + with Impossible -> a) + | _ -> a) + | _ -> a + +(*S Inlining. *) + +(* Utility functions used in the decision of inlining. *) + +let rec ml_size = function + | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l + | MLlam(_,t) -> 1 + ml_size t + | MLcons(_,_,l) -> ml_size_list l + | MLcase(_,t,pv) -> + 1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0) + | MLfix(_,_,f) -> ml_size_array f + | MLletin (_,_,t) -> ml_size t + | MLmagic t -> ml_size t + | _ -> 0 + +and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l + +and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l + +let is_fix = function MLfix _ -> true | _ -> false + +let rec is_constr = function + | MLcons _ -> true + | MLlam(_,t) -> is_constr t + | _ -> false + +(*s Strictness *) + +(* A variable is strict if the evaluation of the whole term implies + the evaluation of this variable. Non-strict variables can be found + behind Match, for example. Expanding a term [t] is a good idea when + it begins by at least one non-strict lambda, since the corresponding + argument to [t] might be unevaluated in the expanded code. *) + +exception Toplevel + +let lift n l = List.map ((+) n) l + +let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l + +(* This function returns a list of de Bruijn indices of non-strict variables, + or raises [Toplevel] if it has an internal non-strict variable. + In fact, not all variables are checked for strictness, only the ones which + de Bruijn index is in the candidates list [cand]. The flag [add] controls + the behaviour when going through a lambda: should we add the corresponding + variable to the candidates? We use this flag to check only the external + lambdas, those that will correspond to arguments. *) + +let rec non_stricts add cand = function + | MLlam (id,t) -> + let cand = lift 1 cand in + let cand = if add then 1::cand else cand in + pop 1 (non_stricts add cand t) + | MLrel n -> + List.filter ((<>) n) cand + | MLapp (t,l)-> + let cand = non_stricts false cand t in + List.fold_left (non_stricts false) cand l + | MLcons (_,_,l) -> + List.fold_left (non_stricts false) cand l + | MLletin (_,t1,t2) -> + let cand = non_stricts false cand t1 in + pop 1 (non_stricts add (lift 1 cand) t2) + | MLfix (_,i,f)-> + let n = Array.length i in + let cand = lift n cand in + let cand = Array.fold_left (non_stricts false) cand f in + pop n cand + | MLcase (_,t,v) -> + (* The only interesting case: for a variable to be non-strict, *) + (* it is sufficient that it appears non-strict in at least one branch, *) + (* so we make an union (in fact a merge). *) + let cand = non_stricts false cand t in + Array.fold_left + (fun c (_,i,t)-> + let n = List.length i in + let cand = lift n cand in + let cand = pop n (non_stricts add cand t) in + Sort.merge (<=) cand c) [] v + (* [merge] may duplicates some indices, but I don't mind. *) + | MLmagic t -> + non_stricts add cand t + | _ -> + cand + +(* The real test: we are looking for internal non-strict variables, so we start + with no candidates, and the only positive answer is via the [Toplevel] + exception. *) + +let is_not_strict t = + try let _ = non_stricts true [] t in false + with Toplevel -> true + +(*s Inlining decision *) + +(* [inline_test] answers the following question: + If we could inline [t] (the user said nothing special), + should we inline ? + + We expand small terms with at least one non-strict + variable (i.e. a variable that may not be evaluated). + + Futhermore we don't expand fixpoints. + + Moreover, as mentionned by X. Leroy (bug #2241), + inling a constant from inside an opaque module might + break types. To avoid that, we require below that + both [r] and its body are globally visible. This isn't + fully satisfactory, since [r] might not be visible (functor), + and anyway it might be interesting to inline [r] at least + inside its own structure. But to be safe, we adopt this + restriction for the moment. +*) + +open Declarations + +let inline_test r t = + if not (auto_inline ()) then false + else + let c = match r with ConstRef c -> c | _ -> assert false in + let body = try (Global.lookup_constant c).const_body with _ -> None in + if body = None then false + else + let t1 = eta_red t in + let t2 = snd (collect_lams t1) in + not (is_fix t2) && ml_size t < 12 && is_not_strict t + +let con_of_string s = + let null = empty_dirpath in + match repr_dirpath (dirpath_of_string s) with + | id :: d -> make_con (MPfile (make_dirpath d)) null (label_of_id id) + | [] -> assert false + +let manual_inline_set = + List.fold_right (fun x -> Cset.add (con_of_string x)) + [ "Coq.Init.Wf.well_founded_induction_type"; + "Coq.Init.Wf.well_founded_induction"; + "Coq.Init.Wf.Acc_iter"; + "Coq.Init.Wf.Fix_F"; + "Coq.Init.Wf.Fix"; + "Coq.Init.Datatypes.andb"; + "Coq.Init.Datatypes.orb"; + "Coq.Init.Logic.eq_rec_r"; + "Coq.Init.Logic.eq_rect_r"; + "Coq.Init.Specif.proj1_sig"; + ] + Cset.empty + +let manual_inline = function + | ConstRef c -> Cset.mem c manual_inline_set + | _ -> false + +(* If the user doesn't say he wants to keep [t], we inline in two cases: + \begin{itemize} + \item the user explicitly requests it + \item [expansion_test] answers that the inlining is a good idea, and + we are free to act (AutoInline is set) + \end{itemize} *) + +let inline r t = + not (to_keep r) (* The user DOES want to keep it *) + && not (is_inline_custom r) + && (to_inline r (* The user DOES want to inline it *) + || (lang () <> Haskell && not (is_projection r) && + (is_recursor r || manual_inline r || inline_test r t))) + diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli new file mode 100644 index 00000000..deaacc3f --- /dev/null +++ b/plugins/extraction/mlutil.mli @@ -0,0 +1,131 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Util +open Names +open Term +open Libnames +open Miniml + +(*s Utility functions over ML types with meta. *) + +val reset_meta_count : unit -> unit +val new_meta : 'a -> ml_type + +val type_subst : int -> ml_type -> ml_type -> ml_type +val type_subst_list : ml_type list -> ml_type -> ml_type +val type_subst_vect : ml_type array -> ml_type -> ml_type + +val instantiation : ml_schema -> ml_type + +val needs_magic : ml_type * ml_type -> bool +val put_magic_if : bool -> ml_ast -> ml_ast +val put_magic : ml_type * ml_type -> ml_ast -> ml_ast + +(*s ML type environment. *) + +module Mlenv : sig + type t + val empty : t + + (* get the n-th more recently entered schema and instantiate it. *) + val get : t -> int -> ml_type + + (* Adding a type in an environment, after generalizing free meta *) + val push_gen : t -> ml_type -> t + + (* Adding a type with no [Tvar] *) + val push_type : t -> ml_type -> t + + (* Adding a type with no [Tvar] nor [Tmeta] *) + val push_std_type : t -> ml_type -> t +end + +(*s Utility functions over ML types without meta *) + +val type_mem_kn : mutual_inductive -> ml_type -> bool + +val type_maxvar : ml_type -> int + +val type_decomp : ml_type -> ml_type list * ml_type +val type_recomp : ml_type list * ml_type -> ml_type + +val var2var' : ml_type -> ml_type + +type abbrev_map = global_reference -> ml_type option + +val type_expand : abbrev_map -> ml_type -> ml_type +val type_to_sign : abbrev_map -> ml_type -> sign +val type_to_signature : abbrev_map -> ml_type -> signature +val type_expunge : abbrev_map -> ml_type -> ml_type +val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type + +val isDummy : ml_type -> bool +val isKill : sign -> bool + +val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast +val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast + + +(*s Special identifiers. [dummy_name] is to be used for dead code + and will be printed as [_] in concrete (Caml) code. *) + +val anonymous_name : identifier +val dummy_name : identifier +val id_of_name : name -> identifier +val id_of_mlid : ml_ident -> identifier +val tmp_id : ml_ident -> ml_ident + +(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns + the list [idn;...;id1] and the term [t]. *) + +val collect_lams : ml_ast -> ml_ident list * ml_ast +val collect_n_lams : int -> ml_ast -> ml_ident list * ml_ast +val remove_n_lams : int -> ml_ast -> ml_ast +val nb_lams : ml_ast -> int +val named_lams : ml_ident list -> ml_ast -> ml_ast +val dummy_lams : ml_ast -> int -> ml_ast +val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast + +val eta_args_sign : int -> signature -> ml_ast list + +(*s Utility functions over ML terms. *) + +val mlapp : ml_ast -> ml_ast list -> ml_ast +val ast_map : (ml_ast -> ml_ast) -> ml_ast -> ml_ast +val ast_map_lift : (int -> ml_ast -> ml_ast) -> int -> ml_ast -> ml_ast +val ast_iter : (ml_ast -> unit) -> ml_ast -> unit +val ast_occurs : int -> ml_ast -> bool +val ast_occurs_itvl : int -> int -> ml_ast -> bool +val ast_lift : int -> ml_ast -> ml_ast +val ast_pop : ml_ast -> ml_ast +val ast_subst : ml_ast -> ml_ast -> ml_ast + +val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast + +val normalize : ml_ast -> ml_ast +val optimize_fix : ml_ast -> ml_ast +val inline : global_reference -> ml_ast -> bool + +exception Impossible +val check_function_branch : ml_branch -> ml_ast +val check_constant_branch : ml_branch -> ml_ast + +(* Classification of signatures *) + +type sign_kind = + | EmptySig + | NonLogicalSig (* at least a [Keep] *) + | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) + | SafeLogicalSig (* only [Kill Ktype] *) + +val sign_kind : signature -> sign_kind + +val sign_no_final_keeps : signature -> signature diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml new file mode 100644 index 00000000..a7f0c017 --- /dev/null +++ b/plugins/extraction/modutil.ml @@ -0,0 +1,375 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Names +open Declarations +open Environ +open Libnames +open Util +open Miniml +open Table +open Mlutil +open Mod_subst + +(*S Functions upon ML modules. *) + +let rec msid_of_mt = function + | MTident mp -> mp + | MTwith(mt,_)-> msid_of_mt mt + | _ -> anomaly "Extraction:the With operator isn't applied to a name" + +(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a + [ml_structure]. *) + +let struct_iter do_decl do_spec s = + let rec mt_iter = function + | MTident _ -> () + | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' + | MTwith (mt,ML_With_type(idl,l,t))-> + let mp_mt = msid_of_mt mt in + let l',idl' = list_sep_last idl in + let mp_w = + List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' + in + let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in + mt_iter mt; do_decl (Dtype(r,l,t)) + | MTwith (mt,_)->mt_iter mt + | MTsig (_, sign) -> List.iter spec_iter sign + and spec_iter = function + | (_,Spec s) -> do_spec s + | (_,Smodule mt) -> mt_iter mt + | (_,Smodtype mt) -> mt_iter mt + in + let rec se_iter = function + | (_,SEdecl d) -> do_decl d + | (_,SEmodule m) -> + me_iter m.ml_mod_expr; mt_iter m.ml_mod_type + | (_,SEmodtype m) -> mt_iter m + and me_iter = function + | MEident _ -> () + | MEfunctor (_,mt,me) -> me_iter me; mt_iter mt + | MEapply (me,me') -> me_iter me; me_iter me' + | MEstruct (msid, sel) -> List.iter se_iter sel + in + List.iter (function (_,sel) -> List.iter se_iter sel) s + +(*s Apply some fonctions upon all references in [ml_type], [ml_ast], + [ml_decl], [ml_spec] and [ml_structure]. *) + +type do_ref = global_reference -> unit + +let record_iter_references do_term = function + | Record l -> List.iter do_term l + | _ -> () + +let type_iter_references do_type t = + let rec iter = function + | Tglob (r,l) -> do_type r; List.iter iter l + | Tarr (a,b) -> iter a; iter b + | _ -> () + in iter t + +let ast_iter_references do_term do_cons do_type a = + let rec iter a = + ast_iter iter a; + match a with + | MLglob r -> do_term r + | MLcons (i,r,_) -> + if lang () = Ocaml then record_iter_references do_term i; + do_cons r + | MLcase (i,_,v) -> + if lang () = Ocaml then record_iter_references do_term (fst i); + Array.iter (fun (r,_,_) -> do_cons r) v + | _ -> () + in iter a + +let ind_iter_references do_term do_cons do_type kn ind = + let type_iter = type_iter_references do_type in + let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in + let packet_iter ip p = + do_type (IndRef ip); + if lang () = Ocaml then + (match ind.ind_equiv with + | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd ip)); + | _ -> ()); + Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types + in + if lang () = Ocaml then record_iter_references do_term ind.ind_info; + Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets + +let decl_iter_references do_term do_cons do_type = + let type_iter = type_iter_references do_type + and ast_iter = ast_iter_references do_term do_cons do_type in + function + | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type + (mind_of_kn kn) ind + | Dtype (r,_,t) -> do_type r; type_iter t + | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t + | Dfix(rv,c,t) -> + Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t + +let spec_iter_references do_term do_cons do_type = function + | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type (mind_of_kn kn) ind + | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot + | Sval (r,t) -> do_term r; type_iter_references do_type t + +(*s Searching occurrences of a particular term (no lifting done). *) + +exception Found + +let rec ast_search f a = + if f a then raise Found else ast_iter (ast_search f) a + +let decl_ast_search f = function + | Dterm (_,a,_) -> ast_search f a + | Dfix (_,c,_) -> Array.iter (ast_search f) c + | _ -> () + +let struct_ast_search f s = + try struct_iter (decl_ast_search f) (fun _ -> ()) s; false + with Found -> true + +let rec type_search f = function + | Tarr (a,b) -> type_search f a; type_search f b + | Tglob (r,l) -> List.iter (type_search f) l + | u -> if f u then raise Found + +let decl_type_search f = function + | Dind (_,{ind_packets=p}) -> + Array.iter + (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p + | Dterm (_,_,u) -> type_search f u + | Dfix (_,_,v) -> Array.iter (type_search f) v + | Dtype (_,_,u) -> type_search f u + +let spec_type_search f = function + | Sind (_,{ind_packets=p}) -> + Array.iter + (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p + | Stype (_,_,ot) -> Option.iter (type_search f) ot + | Sval (_,u) -> type_search f u + +let struct_type_search f s = + try struct_iter (decl_type_search f) (spec_type_search f) s; false + with Found -> true + + +(*s Generating the signature. *) + +let rec msig_of_ms = function + | [] -> [] + | (l,SEdecl (Dind (kn,i))) :: ms -> + (l,Spec (Sind (kn,i))) :: (msig_of_ms ms) + | (l,SEdecl (Dterm (r,_,t))) :: ms -> + (l,Spec (Sval (r,t))) :: (msig_of_ms ms) + | (l,SEdecl (Dtype (r,v,t))) :: ms -> + (l,Spec (Stype (r,v,Some t))) :: (msig_of_ms ms) + | (l,SEdecl (Dfix (rv,_,tv))) :: ms -> + let msig = ref (msig_of_ms ms) in + for i = Array.length rv - 1 downto 0 do + msig := (l,Spec (Sval (rv.(i),tv.(i))))::!msig + done; + !msig + | (l,SEmodule m) :: ms -> (l,Smodule m.ml_mod_type) :: (msig_of_ms ms) + | (l,SEmodtype m) :: ms -> (l,Smodtype m) :: (msig_of_ms ms) + +let signature_of_structure s = + List.map (fun (mp,ms) -> mp,msig_of_ms ms) s + + +(*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *) + +let get_decl_in_structure r struc = + try + let base_mp,ll = labels_of_ref r in + if not (at_toplevel base_mp) then error_not_visible r; + let sel = List.assoc base_mp struc in + let rec go ll sel = match ll with + | [] -> assert false + | l :: ll -> + match List.assoc l sel with + | SEdecl d -> d + | SEmodtype m -> assert false + | SEmodule m -> + match m.ml_mod_expr with + | MEstruct (_,sel) -> go ll sel + | _ -> error_not_visible r + in go ll sel + with Not_found -> + anomaly "reference not found in extracted structure" + + +(*s Optimization of a [ml_structure]. *) + +(* Some transformations of ML terms. [optimize_struct] simplify + all beta redexes (when the argument does not occur, it is just + thrown away; when it occurs exactly once it is substituted; otherwise + a let-in redex is created for clarity) and iota redexes, plus some other + optimizations. *) + +let dfix_to_mlfix rv av i = + let rec make_subst n s = + if n < 0 then s + else make_subst (n-1) (Refmap.add rv.(n) (n+1) s) + in + let s = make_subst (Array.length rv - 1) Refmap.empty + in + let rec subst n t = match t with + | MLglob ((ConstRef kn) as refe) -> + (try MLrel (n + (Refmap.find refe s)) with Not_found -> t) + | _ -> ast_map_lift subst n t + in + let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in + let c = Array.map (subst 0) av + in MLfix(i, ids, c) + +let rec optim to_appear s = function + | [] -> [] + | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l -> + if List.mem r to_appear + then d :: (optim to_appear s l) + else optim to_appear s l + | Dterm (r,t,typ) :: l -> + let t = normalize (ast_glob_subst !s t) in + let i = inline r t in + if i then s := Refmap.add r t !s; + if not i || modular () || List.mem r to_appear + then + let d = match optimize_fix t with + | MLfix (0, _, [|c|]) -> + Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|]) + | t -> Dterm (r, t, typ) + in d :: (optim to_appear s l) + else optim to_appear s l + | d :: l -> d :: (optim to_appear s l) + +let rec optim_se top to_appear s = function + | [] -> [] + | (l,SEdecl (Dterm (r,a,t))) :: lse -> + let a = normalize (ast_glob_subst !s a) in + let i = inline r a in + if i then s := Refmap.add r a !s; + if top && i && not (modular ()) && not (List.mem r to_appear) + then optim_se top to_appear s lse + else + let d = match optimize_fix a with + | MLfix (0, _, [|c|]) -> + Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) + | a -> Dterm (r, a, t) + in (l,SEdecl d) :: (optim_se top to_appear s lse) + | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> + let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in + let all = ref true in + (* This fake body ensures that no fixpoint will be auto-inlined. *) + let fake_body = MLfix (0,[||],[||]) in + for i = 0 to Array.length rv - 1 do + if inline rv.(i) fake_body + then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s + else all := false + done; + if !all && top && not (modular ()) + && (array_for_all (fun r -> not (List.mem r to_appear)) rv) + then optim_se top to_appear s lse + else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) + | (l,SEmodule m) :: lse -> + let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr} + in (l,SEmodule m) :: (optim_se top to_appear s lse) + | se :: lse -> se :: (optim_se top to_appear s lse) + +and optim_me to_appear s = function + | MEstruct (msid, lse) -> MEstruct (msid, optim_se false to_appear s lse) + | MEident mp as me -> me + | MEapply (me, me') -> + MEapply (optim_me to_appear s me, optim_me to_appear s me') + | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me) + +(* After these optimisations, some dependencies may not be needed anymore. + For monolithic extraction, we recompute a minimal set of dependencies. *) + +exception NoDepCheck + +let base_r = function + | ConstRef c as r -> r + | IndRef (kn,_) -> IndRef (kn,0) + | ConstructRef ((kn,_),_) -> IndRef (kn,0) + | _ -> assert false + +let reset_needed, add_needed, found_needed, is_needed = + let needed = ref Refset.empty in + ((fun l -> needed := Refset.empty), + (fun r -> needed := Refset.add (base_r r) !needed), + (fun r -> needed := Refset.remove (base_r r) !needed), + (fun r -> Refset.mem (base_r r) !needed)) + +let declared_refs = function + | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|] + | Dtype (r,_,_) -> [|r|] + | Dterm (r,_,_) -> [|r|] + | Dfix (rv,_,_) -> rv + +(* Computes the dependencies of a declaration, except in case + of custom extraction. *) + +let compute_deps_decl = function + | Dind (kn,ind) -> + (* Todo Later : avoid dependencies when Extract Inductive *) + ind_iter_references add_needed add_needed add_needed (mind_of_kn kn) ind + | Dtype (r,ids,t) -> + if not (is_custom r) then type_iter_references add_needed t + | Dterm (r,u,t) -> + type_iter_references add_needed t; + if not (is_custom r) then + ast_iter_references add_needed add_needed add_needed u + | Dfix _ as d -> + (* Todo Later : avoid dependencies when Extract Constant *) + decl_iter_references add_needed add_needed add_needed d + +let rec depcheck_se = function + | [] -> [] + | ((l,SEdecl d) as t)::se -> + let se' = depcheck_se se in + let rv = declared_refs d in + if not (array_exists is_needed rv) then + (Array.iter remove_info_axiom rv; se') + else + (Array.iter found_needed rv; compute_deps_decl d; t::se') + | _ -> raise NoDepCheck + +let rec depcheck_struct = function + | [] -> [] + | (mp,lse)::struc -> + let struc' = depcheck_struct struc in + let lse' = depcheck_se lse in + (mp,lse')::struc' + +let check_implicits = function + | MLexn s -> + if String.length s > 8 && (s.[0] = 'U' || s.[0] = 'I') then + begin + if String.sub s 0 7 = "UNBOUND" then assert false; + if String.sub s 0 8 = "IMPLICIT" then + error_non_implicit (String.sub s 9 (String.length s - 9)); + end; + false + | _ -> false + +let optimize_struct to_appear struc = + let subst = ref (Refmap.empty : ml_ast Refmap.t) in + let opt_struc = + List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc + in + let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in + ignore (struct_ast_search check_implicits opt_struc); + try + if modular () then raise NoDepCheck; + reset_needed (); + List.iter add_needed to_appear; + depcheck_struct opt_struc + with NoDepCheck -> opt_struc diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli new file mode 100644 index 00000000..8e04a368 --- /dev/null +++ b/plugins/extraction/modutil.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Names +open Declarations +open Environ +open Libnames +open Miniml +open Mod_subst + +(*s Functions upon ML modules. *) + +val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool +val struct_type_search : (ml_type -> bool) -> ml_structure -> bool + +type do_ref = global_reference -> unit + +val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit +val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit + +val signature_of_structure : ml_structure -> ml_signature + +val msid_of_mt : ml_module_type -> module_path + +val get_decl_in_structure : global_reference -> ml_structure -> ml_decl + +(* Some transformations of ML terms. [optimize_struct] simplify + all beta redexes (when the argument does not occur, it is just + thrown away; when it occurs exactly once it is substituted; otherwise + a let-in redex is created for clarity) and iota redexes, plus some other + optimizations. The first argument is the list of objects we want to appear. +*) + +val optimize_struct : global_reference list -> ml_structure -> ml_structure diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml new file mode 100644 index 00000000..30004677 --- /dev/null +++ b/plugins/extraction/ocaml.ml @@ -0,0 +1,759 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*s Production of Ocaml syntax. *) + +open Pp +open Util +open Names +open Nameops +open Libnames +open Table +open Miniml +open Mlutil +open Modutil +open Common +open Declarations + + +(*s Some utility functions. *) + +let pp_tvar id = + let s = string_of_id id in + if String.length s < 2 || s.[1]<>'\'' + then str ("'"^s) + else str ("' "^s) + +let pp_tuple_light f = function + | [] -> mt () + | [x] -> f true x + | l -> + pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l) + +let pp_tuple f = function + | [] -> mt () + | [x] -> f x + | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l) + +let pp_boxed_tuple f = function + | [] -> mt () + | [x] -> f x + | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l)) + +let pp_abst = function + | [] -> mt () + | l -> + str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ + str " ->" ++ spc () + +let pp_parameters l = + (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) + +let pp_string_parameters l = + (pp_boxed_tuple str l ++ space_if (l<>[])) + +(*s Ocaml renaming issues. *) + +let keywords = + List.fold_right (fun s -> Idset.add (id_of_string s)) + [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do"; + "done"; "downto"; "else"; "end"; "exception"; "external"; "false"; + "for"; "fun"; "function"; "functor"; "if"; "in"; "include"; + "inherit"; "initializer"; "lazy"; "let"; "match"; "method"; + "module"; "mutable"; "new"; "object"; "of"; "open"; "or"; + "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true"; + "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod"; + "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] + Idset.empty + +let pp_open mp = str ("open "^ string_of_modfile mp ^"\n") + +let preamble _ used_modules usf = + prlist pp_open used_modules ++ + (if used_modules = [] then mt () else fnl ()) ++ + (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++ + (if usf.mldummy then + str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n" + else mt ()) ++ + (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ()) + +let sig_preamble _ used_modules usf = + prlist pp_open used_modules ++ + (if used_modules = [] then mt () else fnl ()) ++ + (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt()) + +(*s The pretty-printer for Ocaml syntax*) + +(* Beware of the side-effects of [pp_global] and [pp_modname]. + They are used to update table of content for modules. Many [let] + below should not be altered since they force evaluation order. +*) + +let str_global k r = + if is_inline_custom r then find_custom r else Common.pp_global k r + +let pp_global k r = str (str_global k r) + +let pp_modname mp = str (Common.pp_module mp) + +let is_infix r = + is_inline_custom r && + (let s = find_custom r in + let l = String.length s in + l >= 2 && s.[0] = '(' && s.[l-1] = ')') + +let get_infix r = + let s = find_custom r in + String.sub s 1 (String.length s - 2) + +exception NoRecord + +let find_projections = function Record l -> l | _ -> raise NoRecord + +(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses + are needed or not. *) + +let mk_ind path s = + make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s) + +let rec pp_type par vl t = + let rec pp_rec par = function + | Tmeta _ | Tvar' _ | Taxiom -> assert false + | Tvar i -> (try pp_tvar (List.nth vl (pred i)) + with _ -> (str "'a" ++ int i)) + | Tglob (r,[a1;a2]) when is_infix r -> + pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) + | Tglob (r,[]) -> pp_global Type r + | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" -> + pp_tuple_light pp_rec l + | Tglob (r,l) -> + pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r + | Tarr (t1,t2) -> + pp_par par + (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) + | Tdummy _ -> str "__" + | Tunknown -> str "__" + in + hov 0 (pp_rec par t) + +(*s Pretty-printing of expressions. [par] indicates whether + parentheses are needed or not. [env] is the list of names for the + de Bruijn variables. [args] is the list of collected arguments + (already pretty-printed). *) + +let is_ifthenelse = function + | [|(r1,[],_);(r2,[],_)|] -> + (try (find_custom r1 = "true") && (find_custom r2 = "false") + with Not_found -> false) + | _ -> false + +let expr_needs_par = function + | MLlam _ -> true + | MLcase (_,_,[|_|]) -> false + | MLcase (_,_,pv) -> not (is_ifthenelse pv) + | _ -> false + + +(** Special hack for constants of type Ascii.ascii : if an + [Extract Inductive ascii => char] has been declared, then + the constants are directly turned into chars *) + +let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" + +let check_extract_ascii () = + try find_custom (IndRef (ind_ascii,0)) = "char" with Not_found -> false + +let is_list_cons l = + List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l + +let pp_char l = + let rec cumul = function + | [] -> 0 + | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l) + | _ -> assert false + in str ("'"^Char.escaped (Char.chr (cumul l))^"'") + +let rec pp_expr par env args = + let par' = args <> [] || par + and apply st = pp_apply st par args in + function + | MLrel n -> + let id = get_db_name n env in apply (pr_id id) + | MLapp (f,args') -> + let stl = List.map (pp_expr true env []) args' in + pp_expr par env (stl @ args) f + | MLlam _ as a -> + let fl,a' = collect_lams a in + let fl = List.map id_of_mlid fl in + let fl,env' = push_vars fl env in + let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in + apply (pp_par par' st) + | MLletin (id,a1,a2) -> + let i,env' = push_vars [id_of_mlid id] env in + let pp_id = pr_id (List.hd i) + and pp_a1 = pp_expr false env [] a1 + and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in + hv 0 + (apply + (pp_par par' + (hv 0 + (hov 2 + (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ + spc () ++ str "in") ++ + spc () ++ hov 0 pp_a2))) + | MLglob r -> + (try + let args = list_skipn (projection_arity r) args in + let record = List.hd args in + pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) + with _ -> apply (pp_global Term r)) + | MLcons(_,ConstructRef ((kn,0),1),l) + when kn = ind_ascii && check_extract_ascii () & is_list_cons l -> + assert (args=[]); + pp_char l + | MLcons (Coinductive,r,[]) -> + assert (args=[]); + pp_par par (str "lazy " ++ pp_global Cons r) + | MLcons (Coinductive,r,args') -> + assert (args=[]); + let tuple = pp_tuple (pp_expr true env []) args' in + pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")") + | MLcons (_,r,[]) -> + assert (args=[]); + pp_global Cons r + | MLcons (Record projs, r, args') -> + assert (args=[]); + pp_record_pat (projs, List.map (pp_expr true env []) args') + | MLcons (_,r,[arg1;arg2]) when is_infix r -> + assert (args=[]); + pp_par par + ((pp_expr true env [] arg1) ++ str (get_infix r) ++ + (pp_expr true env [] arg2)) + | MLcons (_,r,args') -> + assert (args=[]); + let tuple = pp_tuple (pp_expr true env []) args' in + if str_global Cons r = "" (* hack Extract Inductive prod *) + then tuple + else pp_par par (pp_global Cons r ++ spc () ++ tuple) + | MLcase (_, t, pv) when is_custom_match pv -> + let mkfun (_,ids,e) = + if ids <> [] then named_lams (List.rev ids) e + else dummy_lams (ast_lift 1 e) 1 + in + hov 2 (str (find_custom_match pv) ++ fnl () ++ + prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv + ++ pp_expr true env [] t) + | MLcase ((i,factors), t, pv) -> + let expr = if i = Coinductive then + (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) + else + (pp_expr false env [] t) + in + (try + let projs = find_projections i in + let (_, ids, c) = pv.(0) in + let n = List.length ids in + match c with + | MLrel i when i <= n -> + apply (pp_par par' (pp_expr true env [] t ++ str "." ++ + pp_global Term (List.nth projs (n-i)))) + | MLapp (MLrel i, a) when i <= n -> + if List.exists (ast_occurs_itvl 1 n) a + then raise NoRecord + else + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env + in + (pp_apply + (pp_expr true env [] t ++ str "." ++ + pp_global Term (List.nth projs (n-i))) + par ((List.map (pp_expr true env' []) a) @ args)) + | _ -> raise NoRecord + with NoRecord -> + if Array.length pv = 1 then + let s1,s2 = pp_one_pat env i pv.(0) in + apply + (hv 0 + (pp_par par' + (hv 0 + (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) + ++ spc () ++ str "in") ++ + spc () ++ hov 0 s2))) + else + apply + (pp_par par' + (try pp_ifthenelse par' env expr pv + with Not_found -> + v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ + str " | " ++ pp_pat env (i,factors) pv)))) + | MLfix (i,ids,defs) -> + let ids',env' = push_vars (List.rev (Array.to_list ids)) env in + pp_fix par env' i (Array.of_list (List.rev ids'),defs) args + | MLexn s -> + (* An [MLexn] may be applied, but I don't really care. *) + pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)")) + | MLdummy -> + str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLmagic a -> + pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) + | MLaxiom -> + pp_par par (str "failwith \"AXIOM TO BE REALIZED\"") + + +and pp_record_pat (projs, args) = + str "{ " ++ + prlist_with_sep (fun () -> str ";" ++ spc ()) + (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a) + (List.combine projs args) ++ + str " }" + +and pp_ifthenelse par env expr pv = match pv with + | [|(tru,[],the);(fal,[],els)|] when + (find_custom tru = "true") && (find_custom fal = "false") + -> + hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++ + hov 2 (str "then " ++ + hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++ + hov 2 (str "else " ++ + hov 2 (pp_expr (expr_needs_par els) env [] els))) + | _ -> raise Not_found + +and pp_one_pat env i (r,ids,t) = + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in + let expr = pp_expr (expr_needs_par t) env' [] t in + try + let projs = find_projections i in + pp_record_pat (projs, List.rev_map pr_id ids), expr + with NoRecord -> + (match List.rev ids with + | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2 + | [] -> pp_global Cons r + | ids -> + (* hack Extract Inductive prod *) + (if str_global Cons r = "" then mt () else pp_global Cons r ++ spc ()) + ++ pp_boxed_tuple pr_id ids), + expr + +and pp_pat env (info,factors) pv = + let factor_br, factor_l = try match factors with + | BranchFun (i::_ as l) -> check_function_branch pv.(i), l + | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l + | _ -> MLdummy, [] + with Impossible -> MLdummy, [] + in + let par = expr_needs_par factor_br in + let last = Array.length pv - 1 in + prvecti + (fun i x -> if List.mem i factor_l then mt () else + let s1,s2 = pp_one_pat env info x in + hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++ + if i = last && factor_l = [] then mt () else + fnl () ++ str " | ") pv + ++ + if factor_l = [] then mt () else match factors with + | BranchFun _ -> + let ids, env' = push_vars [anonymous_name] env in + hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + pp_expr par env' [] factor_br) + | BranchCst _ -> + hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br) + | BranchNone -> mt () + +and pp_function env t = + let bl,t' = collect_lams t in + let bl,env' = push_vars (List.map id_of_mlid bl) env in + match t' with + | MLcase(i,MLrel 1,pv) when fst i=Standard && not (is_custom_match pv) -> + if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then + pr_binding (List.rev (List.tl bl)) ++ + str " = function" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' i pv) + else + pr_binding (List.rev bl) ++ + str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' i pv) + | _ -> + pr_binding (List.rev bl) ++ + str " =" ++ fnl () ++ str " " ++ + hov 2 (pp_expr false env' [] t') + +(*s names of the functions ([ids]) are already pushed in [env], + and passed here just for convenience. *) + +and pp_fix par env i (ids,bl) args = + pp_par par + (v 0 (str "let rec " ++ + prvect_with_sep + (fun () -> fnl () ++ str "and ") + (fun (fi,ti) -> pr_id fi ++ pp_function env ti) + (array_map2 (fun id b -> (id,b)) ids bl) ++ + fnl () ++ + hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) + +let pp_val e typ = + hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ + str " **)") ++ fnl2 () + +(*s Pretty-printing of [Dfix] *) + +let pp_Dfix (rv,c,t) = + let names = Array.map + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + in + let rec pp sep letand i = + if i >= Array.length rv then mt () + else if is_inline_custom rv.(i) then pp sep letand (i+1) + else + let def = + if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i)) + else pp_function (empty_env ()) c.(i) + in + sep () ++ pp_val names.(i) t.(i) ++ + str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1) + in pp mt "let rec " 0 + +(*s Pretty-printing of inductive types declaration. *) + +let pp_equiv param_list name = function + | NoEquiv, _ -> mt () + | Equiv kn, i -> + str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i)) + | RenEquiv ren, _ -> + str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name + +let pp_comment s = str "(* " ++ s ++ str " *)" + +let pp_one_ind prefix ip_equiv pl name cnames ctyps = + let pl = rename_tvars keywords pl in + let pp_constructor i typs = + (if i=0 then mt () else fnl ()) ++ + hov 5 (str " | " ++ cnames.(i) ++ + (if typs = [] then mt () else str " of ") ++ + prlist_with_sep + (fun () -> spc () ++ str "* ") (pp_type true pl) typs) + in + pp_parameters pl ++ str prefix ++ name ++ + pp_equiv pl name ip_equiv ++ str " =" ++ + if Array.length ctyps = 0 then str " unit (* empty inductive *)" + else fnl () ++ v 0 (prvecti pp_constructor ctyps) + +let pp_logical_ind packet = + pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ + fnl () ++ + pp_comment (str "with constructors : " ++ + prvect_with_sep spc pr_id packet.ip_consnames) ++ + fnl () + +let pp_singleton kn packet = + let name = pp_global Type (IndRef (mind_of_kn kn,0)) in + let l = rename_tvars keywords packet.ip_vars in + hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ + pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ + pp_comment (str "singleton inductive, whose constructor was " ++ + pr_id packet.ip_consnames.(0))) + +let pp_record kn projs ip_equiv packet = + let name = pp_global Type (IndRef (mind_of_kn kn,0)) in + let projnames = List.map (pp_global Term) projs in + let l = List.combine projnames packet.ip_types.(0) in + let pl = rename_tvars keywords packet.ip_vars in + str "type " ++ pp_parameters pl ++ name ++ + pp_equiv pl name ip_equiv ++ str " = { "++ + hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) + (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l) + ++ str " }" + +let pp_coind pl name = + let pl = rename_tvars keywords pl in + pp_parameters pl ++ name ++ str " = " ++ + pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++ + fnl() ++ str "and " + +let pp_ind co kn ind = + let prefix = if co then "__" else "" in + let some = ref false in + let init= ref (str "type ") in + let names = + Array.mapi (fun i p -> if p.ip_logical then mt () else + pp_global Type (IndRef (mind_of_kn kn,i))) + ind.ind_packets + in + let cnames = + Array.mapi + (fun i p -> if p.ip_logical then [||] else + Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1))) + p.ip_types) + ind.ind_packets + in + let rec pp i = + if i >= Array.length ind.ind_packets then mt () + else + let ip = (mind_of_kn kn,i) in + let ip_equiv = ind.ind_equiv, i in + let p = ind.ind_packets.(i) in + if is_custom (IndRef ip) then pp (i+1) + else begin + some := true; + if p.ip_logical then pp_logical_ind p ++ pp (i+1) + else + let s = !init in + begin + init := (fnl () ++ str "and "); + s ++ + (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ + pp_one_ind + prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++ + pp (i+1) + end + end + in + let st = pp 0 in if !some then st else failwith "empty phrase" + + +(*s Pretty-printing of a declaration. *) + +let pp_mind kn i = + match i.ind_info with + | Singleton -> pp_singleton kn i.ind_packets.(0) + | Coinductive -> pp_ind true kn i + | Record projs -> + pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0) + | Standard -> pp_ind false kn i + +let pp_decl = function + | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Dind (kn,i) -> pp_mind kn i + | Dtype (r, l, t) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids, def = + try + let ids,s = find_type_custom r in + pp_string_parameters ids, str "=" ++ spc () ++ str s + with Not_found -> + pp_parameters l, + if t = Taxiom then str "(* AXIOM TO BE REALIZED *)" + else str "=" ++ spc () ++ pp_type false l t + in + hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + | Dterm (r, a, t) -> + let def = + if is_custom r then str (" = " ^ find_custom r) + else if is_projection r then + (prvect str (Array.make (projection_arity r) " _")) ++ + str " x = x." + else pp_function (empty_env ()) a + in + let name = pp_global Term r in + let postdef = if is_projection r then name else mt () in + pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef) + | Dfix (rv,defs,typs) -> + pp_Dfix (rv,defs,typs) + +let pp_alias_decl ren = function + | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } + | Dtype (r, l, _) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids = pp_parameters l in + hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ + str (ren^".") ++ name) + | Dterm (r, a, t) -> + let name = pp_global Term r in + hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) + | Dfix (rv, _, _) -> + prvecti (fun i r -> if is_inline_custom r then mt () else + let name = pp_global Term r in + hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++ + fnl ()) + rv + +let pp_spec = function + | Sval (r,_) when is_inline_custom r -> failwith "empty phrase" + | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Sind (kn,i) -> pp_mind kn i + | Sval (r,t) -> + let def = pp_type false [] t in + let name = pp_global Term r in + hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def) + | Stype (r,vl,ot) -> + let name = pp_global Type r in + let l = rename_tvars keywords vl in + let ids, def = + try + let ids, s = find_type_custom r in + pp_string_parameters ids, str "= " ++ str s + with Not_found -> + let ids = pp_parameters l in + match ot with + | None -> ids, mt () + | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" + | Some t -> ids, str "=" ++ spc () ++ pp_type false l t + in + hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + +let pp_alias_spec ren = function + | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } + | Stype (r,l,_) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids = pp_parameters l in + hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ + str (ren^".") ++ name) + | Sval _ -> assert false + +let rec pp_specif = function + | (_,Spec (Sval _ as s)) -> pp_spec s + | (l,Spec s) -> + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++ + fnl () ++ str "end" ++ fnl () ++ + pp_alias_spec ren s + with Not_found -> pp_spec s) + | (l,Smodule mt) -> + let def = pp_module_type [] mt in + let def' = pp_module_type [] mt in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def') + with Not_found -> Pp.mt ()) + | (l,Smodtype mt) -> + let def = pp_module_type [] mt in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module type "^ren^" = ") ++ name + with Not_found -> Pp.mt ()) + +and pp_module_type params = function + | MTident kn -> + pp_modname kn + | MTfunsig (mbid, mt, mt') -> + let typ = pp_module_type [] mt in + let name = pp_modname (MPbound mbid) in + let def = pp_module_type (MPbound mbid :: params) mt' in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def + | MTsig (mp, sign) -> + push_visible mp params; + let l = map_succeed pp_specif sign in + pop_visible (); + str "sig " ++ fnl () ++ + v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ + fnl () ++ str "end" + | MTwith(mt,ML_With_type(idl,vl,typ)) -> + let ids = pp_parameters (rename_tvars keywords vl) in + let mp_mt = msid_of_mt mt in + let l,idl' = list_sep_last idl in + let mp_w = + List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' + in + let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) in + push_visible mp_mt []; + let pp_w = str " with type " ++ ids ++ pp_global Type r in + pop_visible(); + pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_type false vl typ + | MTwith(mt,ML_With_module(idl,mp)) -> + let mp_mt = msid_of_mt mt in + let mp_w = + List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl + in + push_visible mp_mt []; + let pp_w = str " with module " ++ pp_modname mp_w in + pop_visible (); + pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_modname mp + +let is_short = function MEident _ | MEapply _ -> true | _ -> false + +let rec pp_structure_elem = function + | (l,SEdecl d) -> + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++ + fnl () ++ str "end" ++ fnl () ++ + pp_alias_decl ren d + with Not_found -> pp_decl d) + | (l,SEmodule m) -> + let typ = + (* virtual printing of the type, in order to have a correct mli later*) + if Common.get_phase () = Pre then + str ": " ++ pp_module_type [] m.ml_mod_type + else mt () + in + let def = pp_module_expr [] m.ml_mod_expr in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 + (str "module " ++ name ++ typ ++ str " = " ++ + (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module "^ren^" = ") ++ name + with Not_found -> mt ()) + | (l,SEmodtype m) -> + let def = pp_module_type [] m in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module type "^ren^" = ") ++ name + with Not_found -> mt ()) + +and pp_module_expr params = function + | MEident mp -> pp_modname mp + | MEapply (me, me') -> + pp_module_expr [] me ++ str "(" ++ pp_module_expr [] me' ++ str ")" + | MEfunctor (mbid, mt, me) -> + let name = pp_modname (MPbound mbid) in + let typ = pp_module_type [] mt in + let def = pp_module_expr (MPbound mbid :: params) me in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def + | MEstruct (mp, sel) -> + push_visible mp params; + let l = map_succeed pp_structure_elem sel in + pop_visible (); + str "struct " ++ fnl () ++ + v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ + fnl () ++ str "end" + +let do_struct f s = + let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt () + in + let ppl (mp,sel) = + push_visible mp []; + let p = prlist_strict pp sel in + (* for monolithic extraction, we try to simulate the unavailability + of [MPfile] in names by artificially nesting these [MPfile] *) + (if modular () then pop_visible ()); p + in + let p = prlist_strict ppl s in + (if not (modular ()) then repeat (List.length s) pop_visible ()); + p + +let pp_struct s = do_struct pp_structure_elem s + +let pp_signature s = do_struct pp_specif s + +let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt () + +let ocaml_descr = { + keywords = keywords; + file_suffix = ".ml"; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = Some ".mli"; + sig_preamble = sig_preamble; + pp_sig = pp_signature; + pp_decl = pp_decl; +} + + diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli new file mode 100644 index 00000000..4a1c1778 --- /dev/null +++ b/plugins/extraction/ocaml.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +val ocaml_descr : Miniml.language_descr + diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml new file mode 100644 index 00000000..108d3685 --- /dev/null +++ b/plugins/extraction/scheme.ml @@ -0,0 +1,215 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*s Production of Scheme syntax. *) + +open Pp +open Util +open Names +open Nameops +open Libnames +open Miniml +open Mlutil +open Table +open Common + +(*s Scheme renaming issues. *) + +let keywords = + List.fold_right (fun s -> Idset.add (id_of_string s)) + [ "define"; "let"; "lambda"; "lambdas"; "match"; + "apply"; "car"; "cdr"; + "error"; "delay"; "force"; "_"; "__"] + Idset.empty + +let preamble _ _ usf = + str ";; This extracted scheme code relies on some additional macros\n" ++ + str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++ + str "(load \"macros_extr.scm\")\n\n" ++ + (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ()) + +let pr_id id = + let s = string_of_id id in + for i = 0 to String.length s - 1 do + if s.[i] = '\'' then s.[i] <- '~' + done; + str s + +let paren = pp_par true + +let pp_abst st = function + | [] -> assert false + | [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st) + | l -> paren + (str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st) + +let pp_apply st _ = function + | [] -> st + | [a] -> hov 2 (paren (st ++ spc () ++ a)) + | args -> hov 2 (paren (str "@ " ++ st ++ + (prlist_strict (fun x -> spc () ++ x) args))) + +(*s The pretty-printer for Scheme syntax *) + +let pp_global k r = str (Common.pp_global k r) + +(*s Pretty-printing of expressions. *) + +let rec pp_expr env args = + let apply st = pp_apply st true args in + function + | MLrel n -> + let id = get_db_name n env in apply (pr_id id) + | MLapp (f,args') -> + let stl = List.map (pp_expr env []) args' in + pp_expr env (stl @ args) f + | MLlam _ as a -> + let fl,a' = collect_lams a in + let fl,env' = push_vars (List.map id_of_mlid fl) env in + apply (pp_abst (pp_expr env' [] a') (List.rev fl)) + | MLletin (id,a1,a2) -> + let i,env' = push_vars [id_of_mlid id] env in + apply + (hv 0 + (hov 2 + (paren + (str "let " ++ + paren + (paren + (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) + ++ spc () ++ hov 0 (pp_expr env' [] a2))))) + | MLglob r -> + apply (pp_global Term r) + | MLcons (i,r,args') -> + assert (args=[]); + let st = + str "`" ++ + paren (pp_global Cons r ++ + (if args' = [] then mt () else spc ()) ++ + prlist_with_sep spc (pp_cons_args env) args') + in + if i = Coinductive then paren (str "delay " ++ st) else st + | MLcase (_,t,pv) when is_custom_match pv -> + let mkfun (_,ids,e) = + if ids <> [] then named_lams (List.rev ids) e + else dummy_lams (ast_lift 1 e) 1 + in + hov 2 (str (find_custom_match pv) ++ fnl () ++ + prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv + ++ pp_expr env [] t) + | MLcase ((i,_),t, pv) -> + let e = + if i <> Coinductive then pp_expr env [] t + else paren (str "force" ++ spc () ++ pp_expr env [] t) + in + apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv))) + | MLfix (i,ids,defs) -> + let ids',env' = push_vars (List.rev (Array.to_list ids)) env in + pp_fix env' i (Array.of_list (List.rev ids'),defs) args + | MLexn s -> + (* An [MLexn] may be applied, but I don't really care. *) + paren (str "error" ++ spc () ++ qs s) + | MLdummy -> + str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLmagic a -> + pp_expr env args a + | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") + +and pp_cons_args env = function + | MLcons (i,r,args) when i<>Coinductive -> + paren (pp_global Cons r ++ + (if args = [] then mt () else spc ()) ++ + prlist_with_sep spc (pp_cons_args env) args) + | e -> str "," ++ pp_expr env [] e + + +and pp_one_pat env (r,ids,t) = + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in + let args = + if ids = [] then mt () + else (str " " ++ prlist_with_sep spc pr_id (List.rev ids)) + in + (pp_global Cons r ++ args), (pp_expr env' [] t) + +and pp_pat env pv = + prvect_with_sep fnl + (fun x -> let s1,s2 = pp_one_pat env x in + hov 2 (str "((" ++ s1 ++ str ")" ++ spc () ++ s2 ++ str ")")) pv + +(*s names of the functions ([ids]) are already pushed in [env], + and passed here just for convenience. *) + +and pp_fix env j (ids,bl) args = + paren + (str "letrec " ++ + (v 0 (paren + (prvect_with_sep fnl + (fun (fi,ti) -> + paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti))) + (array_map2 (fun id b -> (id,b)) ids bl)) ++ + fnl () ++ + hov 2 (pp_apply (pr_id (ids.(j))) true args)))) + +(*s Pretty-printing of a declaration. *) + +let pp_decl = function + | Dind _ -> mt () + | Dtype _ -> mt () + | Dfix (rv, defs,_) -> + let ppv = Array.map (pp_global Term) rv in + prvect_with_sep fnl + (fun (pi,ti) -> + hov 2 + (paren (str "define " ++ pi ++ spc () ++ + (pp_expr (empty_env ()) [] ti)) + ++ fnl ())) + (array_map2 (fun p b -> (p,b)) ppv defs) ++ + fnl () + | Dterm (r, a, _) -> + if is_inline_custom r then mt () + else + if is_custom r then + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ + str (find_custom r))) ++ fnl () ++ fnl () + else + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ + pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () + +let rec pp_structure_elem = function + | (l,SEdecl d) -> pp_decl d + | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr + | (l,SEmodtype m) -> mt () + (* for the moment we simply discard module type *) + +and pp_module_expr = function + | MEstruct (mp,sel) -> prlist_strict pp_structure_elem sel + | MEfunctor _ -> mt () + (* for the moment we simply discard unapplied functors *) + | MEident _ | MEapply _ -> assert false + (* should be expansed in extract_env *) + +let pp_struct = + let pp_sel (mp,sel) = + push_visible mp []; + let p = prlist_strict pp_structure_elem sel in + pop_visible (); p + in + prlist_strict pp_sel + +let scheme_descr = { + keywords = keywords; + file_suffix = ".scm"; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli new file mode 100644 index 00000000..b0fa395c --- /dev/null +++ b/plugins/extraction/scheme.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +val scheme_descr : Miniml.language_descr diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml new file mode 100644 index 00000000..685b84fc --- /dev/null +++ b/plugins/extraction/table.ml @@ -0,0 +1,767 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Names +open Term +open Declarations +open Nameops +open Namegen +open Summary +open Libobject +open Goptions +open Libnames +open Util +open Pp +open Miniml + +(*S Utilities about [module_path] and [kernel_names] and [global_reference] *) + +let occur_kn_in_ref kn = function + | IndRef (kn',_) + | ConstructRef ((kn',_),_) -> kn = kn' + | ConstRef _ -> false + | VarRef _ -> assert false + +let repr_of_r = function + | ConstRef kn -> repr_con kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> repr_mind kn + | VarRef _ -> assert false + +let modpath_of_r r = + let mp,_,_ = repr_of_r r in mp + +let label_of_r r = + let _,_,l = repr_of_r r in l + +let rec base_mp = function + | MPdot (mp,l) -> base_mp mp + | mp -> mp + +let is_modfile = function + | MPfile _ -> true + | _ -> false + +let raw_string_of_modfile = function + | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f))) + | _ -> assert false + +let rec modfile_of_mp = function + | (MPfile _) as mp -> mp + | MPdot (mp,_) -> modfile_of_mp mp + | _ -> raise Not_found + +let current_toplevel () = fst (Lib.current_prefix ()) + +let is_toplevel mp = + mp = initial_path || mp = current_toplevel () + +let at_toplevel mp = + is_modfile mp || is_toplevel mp + +let rec mp_length mp = + let mp0 = current_toplevel () in + let rec len = function + | mp when mp = mp0 -> 1 + | MPdot (mp,_) -> 1 + len mp + | _ -> 1 + in len mp + +let visible_con kn = at_toplevel (base_mp (con_modpath kn)) + +let rec prefixes_mp mp = match mp with + | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') + | _ -> MPset.singleton mp + +let rec get_nth_label_mp n = function + | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp + | _ -> failwith "get_nth_label: not enough MPdot" + +let common_prefix_from_list mp0 mpl = + let prefixes = prefixes_mp mp0 in + let rec f = function + | [] -> None + | mp :: l -> if MPset.mem mp prefixes then Some mp else f l + in f mpl + +let rec parse_labels ll = function + | MPdot (mp,l) -> parse_labels (l::ll) mp + | mp -> mp,ll + +let labels_of_mp mp = parse_labels [] mp + +let rec parse_labels2 ll mp1 = function + | mp when mp1=mp -> mp,ll + | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp + | mp -> mp,ll + +let labels_of_ref r = + let mp_top = current_toplevel () in + let mp,_,l = repr_of_r r in + parse_labels2 [l] mp_top mp + +let rec add_labels_mp mp = function + | [] -> mp + | l :: ll -> add_labels_mp (MPdot (mp,l)) ll + + +(*S The main tables: constants, inductives, records, ... *) + +(* Theses tables are not registered within coq save/undo mechanism + since we reset their contents at each run of Extraction *) + +(*s Constants tables. *) + +let terms = ref (Cmap.empty : ml_decl Cmap.t) +let init_terms () = terms := Cmap.empty +let add_term kn d = terms := Cmap.add kn d !terms +let lookup_term kn = Cmap.find kn !terms + +let types = ref (Cmap.empty : ml_schema Cmap.t) +let init_types () = types := Cmap.empty +let add_type kn s = types := Cmap.add kn s !types +let lookup_type kn = Cmap.find kn !types + +(*s Inductives table. *) + +let inductives = ref (Mindmap.empty : (mutual_inductive_body * ml_ind) Mindmap.t) +let init_inductives () = inductives := Mindmap.empty +let add_ind kn mib ml_ind = inductives := Mindmap.add kn (mib,ml_ind) !inductives +let lookup_ind kn = Mindmap.find kn !inductives + +(*s Recursors table. *) + +let recursors = ref Cset.empty +let init_recursors () = recursors := Cset.empty + +let add_recursors env kn = + let make_kn id = make_con (mind_modpath kn) empty_dirpath (label_of_id id) in + let mib = Environ.lookup_mind kn env in + Array.iter + (fun mip -> + let id = mip.mind_typename in + let kn_rec = make_kn (Nameops.add_suffix id "_rec") + and kn_rect = make_kn (Nameops.add_suffix id "_rect") in + recursors := Cset.add kn_rec (Cset.add kn_rect !recursors)) + mib.mind_packets + +let is_recursor = function + | ConstRef kn -> Cset.mem kn !recursors + | _ -> false + +(*s Record tables. *) + +let projs = ref (Refmap.empty : int Refmap.t) +let init_projs () = projs := Refmap.empty +let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs +let is_projection r = Refmap.mem r !projs +let projection_arity r = Refmap.find r !projs + +(*s Table of used axioms *) + +let info_axioms = ref Refset.empty +let log_axioms = ref Refset.empty +let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty +let add_info_axiom r = info_axioms := Refset.add r !info_axioms +let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms +let add_log_axiom r = log_axioms := Refset.add r !log_axioms + +(*s Extraction mode: modular or monolithic *) + +let modular_ref = ref false + +let set_modular b = modular_ref := b +let modular () = !modular_ref + +(*s Printing. *) + +(* The following functions work even on objects not in [Global.env ()]. + WARNING: for inductive objects, an extract_inductive must have been + done before. *) + +let safe_basename_of_global = function + | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l + | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename + | ConstructRef ((kn,i),j) -> + (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) + | _ -> assert false + +let string_of_global r = + try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) + with _ -> string_of_id (safe_basename_of_global r) + +let safe_pr_global r = str (string_of_global r) + +(* idem, but with qualification, and only for constants. *) + +let safe_pr_long_global r = + try Printer.pr_global r + with _ -> match r with + | ConstRef kn -> + let mp,_,l = repr_con kn in + str ((string_of_mp mp)^"."^(string_of_label l)) + | _ -> assert false + +let pr_long_mp mp = + let lid = repr_dirpath (Nametab.dirpath_of_module mp) in + str (String.concat "." (List.map string_of_id (List.rev lid))) + +let pr_long_global ref = pr_path (Nametab.path_of_global ref) + +(*S Warning and Error messages. *) + +let err s = errorlabstrm "Extraction" s + +let warning_axioms () = + let info_axioms = Refset.elements !info_axioms in + if info_axioms = [] then () + else begin + let s = if List.length info_axioms = 1 then "axiom" else "axioms" in + msg_warning + (str ("The following "^s^" must be realized in the extracted code:") + ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms) + ++ str "." ++ fnl ()) + end; + let log_axioms = Refset.elements !log_axioms in + if log_axioms = [] then () + else begin + let s = if List.length log_axioms = 1 then "axiom was" else "axioms were" + in + msg_warning + (str ("The following logical "^s^" encountered:") ++ + hov 1 + (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n") + ++ + str "Having invalid logical axiom in the environment when extracting" ++ + spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ + fnl ()) + end + +let warning_both_mod_and_cst q mp r = + msg_warning + (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++ + str "do you mean module " ++ + pr_long_mp mp ++ + str " or object " ++ + pr_long_global r ++ str " ?" ++ fnl () ++ + str "First choice is assumed, for the second one please use " ++ + str "fully qualified name." ++ fnl ()) + +let error_axiom_scheme r i = + err (str "The type scheme axiom " ++ spc () ++ + safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ + str " type variable(s).") + +let check_inside_module () = + if Lib.is_modtype () then + err (str "You can't do that within a Module Type." ++ fnl () ++ + str "Close it and try again.") + else if Lib.is_module () then + msg_warning + (str "Extraction inside an opened module is experimental.\n" ++ + str "In case of problem, close it first.\n") + +let check_inside_section () = + if Lib.sections_are_opened () then + err (str "You can't do that within a section." ++ fnl () ++ + str "Close it and try again.") + +let warning_id s = + msg_warning (str ("The identifier "^s^ + " contains __ which is reserved for the extraction")) + +let error_constant r = + err (safe_pr_global r ++ str " is not a constant.") + +let error_inductive r = + err (safe_pr_global r ++ spc () ++ str "is not an inductive type.") + +let error_nb_cons () = + err (str "Not the right number of constructors.") + +let error_module_clash mp1 mp2 = + err (str "The Coq modules " ++ pr_long_mp mp1 ++ str " and " ++ + pr_long_mp mp2 ++ str " have the same ML name.\n" ++ + str "This is not supported yet. Please do some renaming first.") + +let error_unknown_module m = + err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") + +let error_scheme () = + err (str "No Scheme modular extraction available yet.") + +let error_not_visible r = + err (safe_pr_global r ++ str " is not directly visible.\n" ++ + str "For example, it may be inside an applied functor.\n" ++ + str "Use Recursive Extraction to get the whole environment.") + +let error_MPfile_as_mod mp b = + let s1 = if b then "asked" else "required" in + let s2 = if b then "extract some objects of this module or\n" else "" in + err (str ("Extraction of file "^(raw_string_of_modfile mp)^ + ".v as a module is "^s1^".\n"^ + "Monolithic Extraction cannot deal with this situation.\n"^ + "Please "^s2^"use (Recursive) Extraction Library instead.\n")) + +let error_record r = + err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++ + fnl () ++ str "To help extraction, please use an explicit name.") + +let msg_non_implicit r n id = + let name = match id with + | Anonymous -> "" + | Name id -> "(" ^ string_of_id id ^ ") " + in + "The " ^ (ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r) + +let error_non_implicit msg = + err (str (msg ^ " still occurs after extraction.") ++ + fnl () ++ str "Please check the Extraction Implicit declarations.") + +let check_loaded_modfile mp = match base_mp mp with + | MPfile dp -> + if not (Library.library_is_loaded dp) then begin + match base_mp (current_toplevel ()) with + | MPfile dp' when dp<>dp' -> + err (str ("Please load library "^(string_of_dirpath dp^" first."))) + | _ -> () + end + | _ -> () + +let info_file f = + Flags.if_verbose message + ("The file "^f^" has been created by extraction.") + + +(*S The Extraction auxiliary commands *) + +(* The objects defined below should survive an arbitrary time, + so we register them to coq save/undo mechanism. *) + +(*s Extraction AutoInline *) + +let auto_inline_ref = ref false + +let auto_inline () = !auto_inline_ref + +let _ = declare_bool_option + {optsync = true; + optname = "Extraction AutoInline"; + optkey = ["Extraction"; "AutoInline"]; + optread = auto_inline; + optwrite = (:=) auto_inline_ref} + +(*s Extraction TypeExpand *) + +let type_expand_ref = ref true + +let type_expand () = !type_expand_ref + +let _ = declare_bool_option + {optsync = true; + optname = "Extraction TypeExpand"; + optkey = ["Extraction"; "TypeExpand"]; + optread = type_expand; + optwrite = (:=) type_expand_ref} + +(*s Extraction Optimize *) + +type opt_flag = + { opt_kill_dum : bool; (* 1 *) + opt_fix_fun : bool; (* 2 *) + opt_case_iot : bool; (* 4 *) + opt_case_idr : bool; (* 8 *) + opt_case_idg : bool; (* 16 *) + opt_case_cst : bool; (* 32 *) + opt_case_fun : bool; (* 64 *) + opt_case_app : bool; (* 128 *) + opt_let_app : bool; (* 256 *) + opt_lin_let : bool; (* 512 *) + opt_lin_beta : bool } (* 1024 *) + +let kth_digit n k = (n land (1 lsl k) <> 0) + +let flag_of_int n = + { opt_kill_dum = kth_digit n 0; + opt_fix_fun = kth_digit n 1; + opt_case_iot = kth_digit n 2; + opt_case_idr = kth_digit n 3; + opt_case_idg = kth_digit n 4; + opt_case_cst = kth_digit n 5; + opt_case_fun = kth_digit n 6; + opt_case_app = kth_digit n 7; + opt_let_app = kth_digit n 8; + opt_lin_let = kth_digit n 9; + opt_lin_beta = kth_digit n 10 } + +(* For the moment, we allow by default everything except : + - the type-unsafe optimization [opt_case_idg] + - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta] + (may lead to complexity blow-up, subsumed by finer reductions + when inlining recursors). +*) + +let int_flag_init = 1 + 2 + 4 + 8 (*+ 16*) + 32 + 64 + 128 + 256 (*+ 512 + 1024*) + +let int_flag_ref = ref int_flag_init +let opt_flag_ref = ref (flag_of_int int_flag_init) + +let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n + +let optims () = !opt_flag_ref + +let _ = declare_bool_option + {optsync = true; + optname = "Extraction Optimize"; + optkey = ["Extraction"; "Optimize"]; + optread = (fun () -> !int_flag_ref <> 0); + optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} + +let _ = declare_int_option + { optsync = true; + optname = "Extraction Flag"; + optkey = ["Extraction";"Flag"]; + optread = (fun _ -> Some !int_flag_ref); + optwrite = (function + | None -> chg_flag 0 + | Some i -> chg_flag (max i 0))} + + +(*s Extraction Lang *) + +type lang = Ocaml | Haskell | Scheme + +let lang_ref = ref Ocaml + +let lang () = !lang_ref + +let (extr_lang,_) = + declare_object + {(default_object "Extraction Lang") with + cache_function = (fun (_,l) -> lang_ref := l); + load_function = (fun _ (_,l) -> lang_ref := l)} + +let _ = declare_summary "Extraction Lang" + { freeze_function = (fun () -> !lang_ref); + unfreeze_function = ((:=) lang_ref); + init_function = (fun () -> lang_ref := Ocaml) } + +let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) + +(*s Extraction Inline/NoInline *) + +let empty_inline_table = (Refset.empty,Refset.empty) + +let inline_table = ref empty_inline_table + +let to_inline r = Refset.mem r (fst !inline_table) + +let to_keep r = Refset.mem r (snd !inline_table) + +let add_inline_entries b l = + let f b = if b then Refset.add else Refset.remove in + let i,k = !inline_table in + inline_table := + (List.fold_right (f b) l i), + (List.fold_right (f (not b)) l k) + +(* Registration of operations for rollback. *) + +let (inline_extraction,_) = + declare_object + {(default_object "Extraction Inline") with + cache_function = (fun (_,(b,l)) -> add_inline_entries b l); + load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); + classify_function = (fun o -> Substitute o); + subst_function = + (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) + } + +let _ = declare_summary "Extraction Inline" + { freeze_function = (fun () -> !inline_table); + unfreeze_function = ((:=) inline_table); + init_function = (fun () -> inline_table := empty_inline_table) } + +(* Grammar entries. *) + +let extraction_inline b l = + check_inside_section (); + let refs = List.map Nametab.global l in + List.iter + (fun r -> match r with + | ConstRef _ -> () + | _ -> error_constant r) refs; + Lib.add_anonymous_leaf (inline_extraction (b,refs)) + +(* Printing part *) + +let print_extraction_inline () = + let (i,n)= !inline_table in + let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in + msg + (str "Extraction Inline:" ++ fnl () ++ + Refset.fold + (fun r p -> + (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++ + str "Extraction NoInline:" ++ fnl () ++ + Refset.fold + (fun r p -> + (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) n (mt ())) + +(* Reset part *) + +let (reset_inline,_) = + declare_object + {(default_object "Reset Extraction Inline") with + cache_function = (fun (_,_)-> inline_table := empty_inline_table); + load_function = (fun _ (_,_)-> inline_table := empty_inline_table)} + +let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) + +(*s Extraction Implicit *) + +type int_or_id = ArgInt of int | ArgId of identifier + +let implicits_table = ref Refmap.empty + +let implicits_of_global r = + try Refmap.find r !implicits_table with Not_found -> [] + +let add_implicits r l = + let typ = Global.type_of_global r in + let rels,_ = + decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in + let names = List.rev_map fst rels in + let n = List.length names in + let check = function + | ArgInt i -> + if 1 <= i && i <= n then i + else err (int i ++ str " is not a valid argument number for " ++ + safe_pr_global r) + | ArgId id -> + (try list_index (Name id) names + with Not_found -> + err (str "No argument " ++ pr_id id ++ str " for " ++ + safe_pr_global r)) + in + let l' = List.map check l in + implicits_table := Refmap.add r l' !implicits_table + +(* Registration of operations for rollback. *) + +let (implicit_extraction,_) = + declare_object + {(default_object "Extraction Implicit") with + cache_function = (fun (_,(r,l)) -> add_implicits r l); + load_function = (fun _ (_,(r,l)) -> add_implicits r l); + classify_function = (fun o -> Substitute o); + subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l)) + } + +let _ = declare_summary "Extraction Implicit" + { freeze_function = (fun () -> !implicits_table); + unfreeze_function = ((:=) implicits_table); + init_function = (fun () -> implicits_table := Refmap.empty) } + +(* Grammar entries. *) + +let extraction_implicit r l = + check_inside_section (); + Lib.add_anonymous_leaf (implicit_extraction (Nametab.global r,l)) + + +(*s Extraction Blacklist of filenames not to use while extracting *) + +let blacklist_table = ref Idset.empty + +let modfile_ids = ref [] +let modfile_mps = ref MPmap.empty + +let reset_modfile () = + modfile_ids := Idset.elements !blacklist_table; + modfile_mps := MPmap.empty + +let string_of_modfile mp = + try MPmap.find mp !modfile_mps + with Not_found -> + let id = id_of_string (raw_string_of_modfile mp) in + let id' = next_ident_away id !modfile_ids in + let s' = string_of_id id' in + modfile_ids := id' :: !modfile_ids; + modfile_mps := MPmap.add mp s' !modfile_mps; + s' + +(* same as [string_of_modfile], but preserves the capital/uncapital 1st char *) + +let file_of_modfile mp = + let s0 = match mp with + | MPfile f -> string_of_id (List.hd (repr_dirpath f)) + | _ -> assert false + in + let s = String.copy (string_of_modfile mp) in + if s.[0] <> s0.[0] then s.[0] <- s0.[0]; + s + +let add_blacklist_entries l = + blacklist_table := + List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s))) + l !blacklist_table + +(* Registration of operations for rollback. *) + +let (blacklist_extraction,_) = + declare_object + {(default_object "Extraction Blacklist") with + cache_function = (fun (_,l) -> add_blacklist_entries l); + load_function = (fun _ (_,l) -> add_blacklist_entries l); + classify_function = (fun o -> Libobject.Keep o); + subst_function = (fun (_,x) -> x) + } + +let _ = declare_summary "Extraction Blacklist" + { freeze_function = (fun () -> !blacklist_table); + unfreeze_function = ((:=) blacklist_table); + init_function = (fun () -> blacklist_table := Idset.empty) } + +(* Grammar entries. *) + +let extraction_blacklist l = + let l = List.rev_map string_of_id l in + Lib.add_anonymous_leaf (blacklist_extraction l) + +(* Printing part *) + +let print_extraction_blacklist () = + msgnl + (prlist_with_sep fnl pr_id (Idset.elements !blacklist_table)) + +(* Reset part *) + +let (reset_blacklist,_) = + declare_object + {(default_object "Reset Extraction Blacklist") with + cache_function = (fun (_,_)-> blacklist_table := Idset.empty); + load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)} + +let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ()) + +(*s Extract Constant/Inductive. *) + +(* UGLY HACK: to be defined in [extraction.ml] *) +let use_type_scheme_nb_args, register_type_scheme_nb_args = + let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r + +let customs = ref Refmap.empty + +let add_custom r ids s = customs := Refmap.add r (ids,s) !customs + +let is_custom r = Refmap.mem r !customs + +let is_inline_custom r = (is_custom r) && (to_inline r) + +let find_custom r = snd (Refmap.find r !customs) + +let find_type_custom r = Refmap.find r !customs + +let custom_matchs = ref Refmap.empty + +let add_custom_match r s = + custom_matchs := Refmap.add r s !custom_matchs + +let indref_of_match pv = + if Array.length pv = 0 then raise Not_found; + match pv.(0) with + | (ConstructRef (ip,_), _, _) -> IndRef ip + | _ -> raise Not_found + +let is_custom_match pv = + try Refmap.mem (indref_of_match pv) !custom_matchs + with Not_found -> false + +let find_custom_match pv = + Refmap.find (indref_of_match pv) !custom_matchs + +(* Registration of operations for rollback. *) + +let (in_customs,_) = + declare_object + {(default_object "ML extractions") with + cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); + load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); + classify_function = (fun o -> Substitute o); + subst_function = + (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) + } + +let _ = declare_summary "ML extractions" + { freeze_function = (fun () -> !customs); + unfreeze_function = ((:=) customs); + init_function = (fun () -> customs := Refmap.empty) } + +let (in_custom_matchs,_) = + declare_object + {(default_object "ML extractions custom matchs") with + cache_function = (fun (_,(r,s)) -> add_custom_match r s); + load_function = (fun _ (_,(r,s)) -> add_custom_match r s); + classify_function = (fun o -> Substitute o); + subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s)) + } + +let _ = declare_summary "ML extractions custom match" + { freeze_function = (fun () -> !custom_matchs); + unfreeze_function = ((:=) custom_matchs); + init_function = (fun () -> custom_matchs := Refmap.empty) } + +(* Grammar entries. *) + +let extract_constant_inline inline r ids s = + check_inside_section (); + let g = Nametab.global r in + match g with + | ConstRef kn -> + let env = Global.env () in + let typ = Typeops.type_of_constant env kn in + let typ = Reduction.whd_betadeltaiota env typ in + if Reduction.is_arity env typ + then begin + let nargs = use_type_scheme_nb_args env typ in + if List.length ids <> nargs then error_axiom_scheme g nargs + end; + Lib.add_anonymous_leaf (inline_extraction (inline,[g])); + Lib.add_anonymous_leaf (in_customs (g,ids,s)) + | _ -> error_constant g + + +let extract_inductive r s l optstr = + check_inside_section (); + let g = Nametab.global r in + match g with + | IndRef ((kn,i) as ip) -> + let mib = Global.lookup_mind kn in + let n = Array.length mib.mind_packets.(i).mind_consnames in + if n <> List.length l then error_nb_cons (); + Lib.add_anonymous_leaf (inline_extraction (true,[g])); + Lib.add_anonymous_leaf (in_customs (g,[],s)); + Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s))) + optstr; + list_iter_i + (fun j s -> + let g = ConstructRef (ip,succ j) in + Lib.add_anonymous_leaf (inline_extraction (true,[g])); + Lib.add_anonymous_leaf (in_customs (g,[],s))) l + | _ -> error_inductive g + + + +(*s Tables synchronization. *) + +let reset_tables () = + init_terms (); init_types (); init_inductives (); init_recursors (); + init_projs (); init_axioms (); reset_modfile () diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli new file mode 100644 index 00000000..ae46233d --- /dev/null +++ b/plugins/extraction/table.mli @@ -0,0 +1,167 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Names +open Libnames +open Miniml +open Declarations + +val safe_basename_of_global : global_reference -> identifier + +(*s Warning and Error messages. *) + +val warning_axioms : unit -> unit +val warning_both_mod_and_cst : + qualid -> module_path -> global_reference -> unit +val warning_id : string -> unit +val error_axiom_scheme : global_reference -> int -> 'a +val error_constant : global_reference -> 'a +val error_inductive : global_reference -> 'a +val error_nb_cons : unit -> 'a +val error_module_clash : module_path -> module_path -> 'a +val error_unknown_module : qualid -> 'a +val error_scheme : unit -> 'a +val error_not_visible : global_reference -> 'a +val error_MPfile_as_mod : module_path -> bool -> 'a +val error_record : global_reference -> 'a +val check_inside_module : unit -> unit +val check_inside_section : unit -> unit +val check_loaded_modfile : module_path -> unit +val msg_non_implicit : global_reference -> int -> name -> string +val error_non_implicit : string -> 'a + +val info_file : string -> unit + +(*s utilities about [module_path] and [kernel_names] and [global_reference] *) + +val occur_kn_in_ref : mutual_inductive -> global_reference -> bool +val repr_of_r : global_reference -> module_path * dir_path * label +val modpath_of_r : global_reference -> module_path +val label_of_r : global_reference -> label +val current_toplevel : unit -> module_path +val base_mp : module_path -> module_path +val is_modfile : module_path -> bool +val string_of_modfile : module_path -> string +val file_of_modfile : module_path -> string +val is_toplevel : module_path -> bool +val at_toplevel : module_path -> bool +val visible_con : constant -> bool +val mp_length : module_path -> int +val prefixes_mp : module_path -> MPset.t +val modfile_of_mp : module_path -> module_path +val common_prefix_from_list : + module_path -> module_path list -> module_path option +val add_labels_mp : module_path -> label list -> module_path +val get_nth_label_mp : int -> module_path -> label +val labels_of_ref : global_reference -> module_path * label list + +(*s Some table-related operations *) + +val add_term : constant -> ml_decl -> unit +val lookup_term : constant -> ml_decl + +val add_type : constant -> ml_schema -> unit +val lookup_type : constant -> ml_schema + +val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit +val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind + +val add_recursors : Environ.env -> mutual_inductive -> unit +val is_recursor : global_reference -> bool + +val add_projection : int -> constant -> unit +val is_projection : global_reference -> bool +val projection_arity : global_reference -> int + +val add_info_axiom : global_reference -> unit +val remove_info_axiom : global_reference -> unit +val add_log_axiom : global_reference -> unit + +val reset_tables : unit -> unit + +(*s AutoInline parameter *) + +val auto_inline : unit -> bool + +(*s TypeExpand parameter *) + +val type_expand : unit -> bool + +(*s Optimize parameter *) + +type opt_flag = + { opt_kill_dum : bool; (* 1 *) + opt_fix_fun : bool; (* 2 *) + opt_case_iot : bool; (* 4 *) + opt_case_idr : bool; (* 8 *) + opt_case_idg : bool; (* 16 *) + opt_case_cst : bool; (* 32 *) + opt_case_fun : bool; (* 64 *) + opt_case_app : bool; (* 128 *) + opt_let_app : bool; (* 256 *) + opt_lin_let : bool; (* 512 *) + opt_lin_beta : bool } (* 1024 *) + +val optims : unit -> opt_flag + +(*s Target language. *) + +type lang = Ocaml | Haskell | Scheme +val lang : unit -> lang + +(*s Extraction mode: modular or monolithic *) + +val set_modular : bool -> unit +val modular : unit -> bool + +(*s Table for custom inlining *) + +val to_inline : global_reference -> bool +val to_keep : global_reference -> bool + +(*s Table for implicits arguments *) + +val implicits_of_global : global_reference -> int list + +(*s Table for user-given custom ML extractions. *) + +(* UGLY HACK: registration of a function defined in [extraction.ml] *) +val register_type_scheme_nb_args : (Environ.env -> Term.constr -> int) -> unit + +val is_custom : global_reference -> bool +val is_inline_custom : global_reference -> bool +val find_custom : global_reference -> string +val find_type_custom : global_reference -> string list * string + +val is_custom_match : ml_branch array -> bool +val find_custom_match : ml_branch array -> string + +(*s Extraction commands. *) + +val extraction_language : lang -> unit +val extraction_inline : bool -> reference list -> unit +val print_extraction_inline : unit -> unit +val reset_extraction_inline : unit -> unit +val extract_constant_inline : + bool -> reference -> string list -> string -> unit +val extract_inductive : + reference -> string -> string list -> string option -> unit + +type int_or_id = ArgInt of int | ArgId of identifier +val extraction_implicit : reference -> int_or_id list -> unit + +(*s Table of blacklisted filenames *) + +val extraction_blacklist : identifier list -> unit +val reset_extraction_blacklist : unit -> unit +val print_extraction_blacklist : unit -> unit + + + diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget new file mode 100644 index 00000000..1fe09f6f --- /dev/null +++ b/plugins/extraction/vo.itarget @@ -0,0 +1,8 @@ +ExtrOcamlBasic.vo +ExtrOcamlIntConv.vo +ExtrOcamlBigIntConv.vo +ExtrOcamlNatInt.vo +ExtrOcamlNatBigInt.vo +ExtrOcamlZInt.vo +ExtrOcamlZBigInt.vo +ExtrOcamlString.vo
\ No newline at end of file |