diff options
Diffstat (limited to 'contrib/extraction')
24 files changed, 0 insertions, 6688 deletions
diff --git a/contrib/extraction/BUGS b/contrib/extraction/BUGS deleted file mode 100644 index 7f3f59c1..00000000 --- a/contrib/extraction/BUGS +++ /dev/null @@ -1,2 +0,0 @@ -It's not a bug, it's a lack of feature !! -Cf TODO. diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES deleted file mode 100644 index acd1dbda..00000000 --- a/contrib/extraction/CHANGES +++ /dev/null @@ -1,409 +0,0 @@ -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: - * contrib/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/contrib/extraction/README b/contrib/extraction/README deleted file mode 100644 index 7350365e..00000000 --- a/contrib/extraction/README +++ /dev/null @@ -1,139 +0,0 @@ - -Status of Extraction in Coq version 7.x -====================================== - -(* 22 jan 2003 : Updated for version 7.4 *) - - -J.C. Filliâtre -P. Letouzey - - - -Extraction code has been completely rewritten since version V6.3. -This work is still not finished, but most parts of it are already usable. -In consequence it is included in the Coq V7.0 final release. -But don't be mistaken: - - THIS WORK IS STILL EXPERIMENTAL ! - -1) Principles - -The main goal of the new extraction is to handle any Coq term, even -those upon sort Type, and to produce code that always compiles. -Thus it will never answer something like "Not an ML type", but rather -a dummy term like the ML unit. - -Translation between Coq and ML is based upon the following principles: - -- Terms of sort Prop don't have any computational meaning, so they are -merged into one ML term "__". This part is done according to P. Letouzey's -works (*) and (**). - -This dummy constant "__" used to be implemented by the unit (), but -we recently found that this constant might be applied in some cases. -So "__" is now in Ocaml a fixpoint that forgets its arguments: - - let __ = let rec f _ = Obj.repr f in Obj.repr f - - -- Terms that are type schemes (i.e. something of type ( : )( : )...s with -s a sort ) don't have any ML counterpart at the term level, since they -are types transformers. In fact they do not have any computational -meaning either. So we also merge them into that dummy term "__". - -- A Coq term gives a ML term or a ML type depending of its type: -type schemes will (try to) give ML types, and all other terms give ML terms. - -And the rest of the translation is (almost) straightforward: an inductive -gives an inductive, etc... - -This gives ML code that have no special reason to typecheck, due -to the incompatibilities between Coq and ML typing systems. In fact -most of the time everything goes right. For example, it is sufficient -to extract and compile everything in the "theories" directory -(cf test subdirectory). - -We now verify during extraction that the produced code is typecheckable, -and if it is not we insert unsafe type casting at critical points in the -code. For the moment, it is an Ocaml-only feature, using the "Obj.magic" -function, but the same kind of trick will be soon made in Haskell. - - -2) Differences with previous extraction (V6.3 and before) - -2.a) The pros - -The ability to extract every Coq term, as explain in the previous -paragraph. - -The ability to extract from a file an ML module (cf Extraction Module in the -documentation) - -You can have a taste of extraction directly at the toplevel by -using the "Extraction <ident>" or the "Recursive Extraction <ident>". -This toplevel extraction was already there in V6.3, but was printing -Fw terms. It now prints in the language of your choice: -Ocaml, Haskell, Scheme, or an Ocaml-like with Coq namings. - -The optimization done on extracted code has been ported between -V6.3 and V7 and enhanced, and in particular the mechanism of automatic -expansion. - -2.b) The cons - -The presence of some parasite "__" as dummy arguments -in functions. This denotes the rests of a proof part. The previous -extraction was able to remove them totally. The current implementation -removes a good deal of them (more that in 7.0), but not all. - -This problem is due to extraction upon Type. -For example, let's take this pathological term: - (if b then Set else Prop) : Type -The only way to know if this is an Set (to keep) or a Prop (to remove) -is to compute the boolean b, and we do not want to do that during -extraction. - -There is no more "ML import" feature. You can compensate by using -Axioms, and then "Extract Constant ..." - -3) Examples - -The file "test-extraction.v" is made of some examples used while debugging. - -In the subdirectory "test", you can test extraction on the Coq theories. -Go there. -"make tree" to make a local copy of the "theories" tree -"make" to extract & compile most of the theories file in Ocaml -"make -f Makefile.haskell" to extract & compile in Haskell - -See also Reference Manual for explanation of extraction syntaxes -and more examples. - - -(*): -Exécution de termes de preuves: une nouvelle méthode d'extraction -pour le Calcul des Constructions Inductives, Pierre Letouzey, -DEA thesis, 2000, -http://www.lri.fr/~letouzey/download/rapport_dea.ps.gz - -(**) -A New Extraction for Coq, Pierre Letouzey, -Types 2002 Post-Workshop Proceedings, to appear, -draft at http://www.lri.fr/~letouzey/download/extraction2002.ps.gz - - -Any feedback is welcome: -Pierre.Letouzey@lri.fr -Jean.Christophe.Filliatre@lri.fr - - - - - - - - - - - diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO deleted file mode 100644 index 174be06e..00000000 --- a/contrib/extraction/TODO +++ /dev/null @@ -1,31 +0,0 @@ - - 16. Haskell : - - equivalent of Obj.magic (unsafeCoerce ?) - - look again at the syntax (make it independant of layout ...) - - producing .hi files - - modules/modules types/functors in Haskell ? - - 17. Scheme : - - modular Scheme ? - - 18. Improve speed (profiling) - - 19. Look again at those hugly renamings functions. - Especially get rid of ML clashes like - - let t = 0 - module M = struct - let t = 1 - let u = The.External.t (* ?? *) - end - - 20. Support the .v-as-internal-module, like in - - <file A.v> - Definition foo :=O. - <End file A.v> - - <at toplevel> - Require A. - Module M:=A - Extraction M.
\ No newline at end of file diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml deleted file mode 100644 index 73f44e68..00000000 --- a/contrib/extraction/common.ml +++ /dev/null @@ -1,444 +0,0 @@ -(************************************************************************) -(* 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: common.ml 13200 2010-06-25 22:36:25Z letouzey $ i*) - -open Pp -open Util -open Names -open Term -open Declarations -open Nameops -open Libnames -open Table -open Miniml -open Mlutil -open Modutil -open Mod_subst - -let string_of_id id = ascii_of_ident (Names.string_of_id id) - -(*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 dottify = function - | [] -> assert false - | [s] -> s - | s::[""] -> s - | s::l -> (dottify l)^"."^s - -(*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_ident 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 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: - [X.Y; X; A.B.C; A.B; A; ...], i.e. each addition should either - be a [MPdot] over the last entry, or something new, mainly - [MPself], or [MPfile] at the beginning. - - - The [content] part is used to recoard all the names already - seen at this level. - - - The [subst] part is here mainly for printing signature - (in which names are still short, i.e. relative to a [msid]). -*) - -type visible_layer = { mp : module_path; - content : ((kind*string),unit) Hashtbl.t } - -let pop_visible, push_visible, get_visible, subst_mp = - let vis = ref [] and sub = ref [empty_subst] in - register_cleanup (fun () -> vis := []; sub := [empty_subst]); - 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; - sub := List.tl !sub - and push mp o = - vis := { mp = mp; content = Hashtbl.create 97 } :: !vis; - let s = List.hd !sub in - let s = match o with None -> s | Some msid -> add_msid msid mp s in - sub := s :: !sub - and get () = !vis - and subst mp = subst_mp (List.hd !sub) mp - in (pop,push,get,subst) - -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 = Hashtbl.add (top_visible ()).content ks () - -(* 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 (subst_mp 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 - | MPself msid -> [modular_rename Mod (id_of_msid msid)] - | MPbound mbid -> [modular_rename Mod (id_of_mbid mbid)] - | 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 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 = subst_mp (modpath_of_r r) in - let l = mp_renaming mp 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_id_of_global r)) globs in - string_of_id id - else modular_rename k (safe_id_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 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 visible_clash mp0 ks = - let rec clash = function - | [] -> false - | v :: _ when v.mp = mp0 -> false - | v :: _ when Hashtbl.mem v.content ks -> true - | _ :: vis -> 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. - Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *) - -let pp_gen k mp ls olab = - try (* what is the largest prefix of [mp] that belongs to [visible]? *) - let prefix = common_prefix_from_list mp (get_visible_mps ()) in - let delta = mp_length mp - mp_length prefix in - assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *) - let ls = list_firstn (delta + if k = Mod then 0 else 1) ls in - let s,ls' = list_sep_last ls in - (* Reference r / module path mp is of the form [<prefix>.s.<List.rev ls'>]. - Difficulty: in ocaml the prefix part cannot be used for - qualification (we are inside it) and the rest of the long - name may be hidden. - Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *) - let k' = if ls' = [] then k else Mod in - if visible_clash prefix (k',s) then - let front = if ls' = [] && k <> Mod then [s] else ls' in - let lab = (* label associated with s *) - if delta = 0 && k <> Mod then Option.get olab - else get_nth_label_mp delta mp - in - try dottify (front @ [check_duplicate prefix lab]) - with Not_found -> - assert (get_phase () = Pre); (* otherwise it's too late *) - add_duplicate prefix lab; dottify ls - else dottify ls - with Not_found -> - (* [mp] belongs to a closed module, not one of [visible]. *) - let base = base_mp mp in - let base_s,ls1 = list_sep_last ls in - let s,ls2 = list_sep_last ls1 in - (* [List.rev ls] is [base_s :: s :: List.rev ls2] *) - let k' = if ls2 = [] then k else Mod 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 ls1 - else if visible_clash base (Mod,base_s) then - error_module_clash base_s - else dottify ls - -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 = subst_mp (modpath_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); unquote s) - else match lang () with - | Scheme -> unquote s (* no modular Scheme extraction... *) - | Haskell -> if modular () then dottify ls else s - (* for the moment we always qualify in modular Haskell... *) - | Ocaml -> pp_gen k mp ls (Some (label_of_r r)) - -(* The next function is used only in Ocaml extraction...*) -let pp_module mp = - let mp = subst_mp mp in - let ls = mp_renaming mp in - if List.length ls = 1 then dottify ls - else match mp with - | MPdot (mp0,_) 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); s - | _ -> pp_gen Mod mp ls None - - diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli deleted file mode 100644 index b7e70414..00000000 --- a/contrib/extraction/common.mli +++ /dev/null @@ -1,57 +0,0 @@ -(************************************************************************) -(* 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: common.mli 11559 2008-11-07 22:03:34Z letouzey $ 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 -val push_visible : module_path -> mod_self_id option -> 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/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml deleted file mode 100644 index 057a7b29..00000000 --- a/contrib/extraction/extract_env.ml +++ /dev/null @@ -1,529 +0,0 @@ -(************************************************************************) -(* 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: extract_env.ml 13201 2010-06-25 22:36:27Z letouzey $ 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 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 - | MPself msid -> SEBstruct (msid, List.rev (map_succeed get_reference seg)) - | _ -> assert false - -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 : kernel_name -> 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 : kernel_name -> 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 : KNset.t; mutable con : Cset.t; mutable mp : MPset.t } - (* the imperative internal visit lists *) - let v = { kn = KNset.empty ; con = Cset.empty ; mp = MPset.empty } - (* the accessor functions *) - let reset () = v.kn <- KNset.empty; v.con <- Cset.empty; v.mp <- MPset.empty - let needed_kn kn = KNset.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 <- KNset.add kn v.kn; add_mp (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 - -let build_mb expr typ_opt = - { mod_expr = Some expr; - mod_type = typ_opt; - mod_constraints = Univ.Constraint.empty; - mod_alias = Mod_subst.empty_subst; - mod_retroknowledge = [] } - -let my_type_of_mb env mb = - match mb.mod_type with - | Some mtb -> mtb - | None -> Modops.eval_struct env (Option.get mb.mod_expr) - -(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. - To check with Elie. *) - -let env_for_mtb_with env mtb idl = - let msid,sig_b = match Modops.eval_struct env mtb with - | SEBstruct(msid,sig_b) -> msid,sig_b - | _ -> assert false - in - let l = label_of_id (List.hd idl) in - let before = fst (list_split_at (fun (l',_) -> l=l') sig_b) in - Modops.add_signature (MPself msid) before 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 s = Sind (kn, extract_inductive env kn) 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 (my_type_of_mb env mb) in - (l,Smodule spec) :: specs - | (l,SFBmodtype mtb) :: msig -> - let specs = extract_sfb_spec env mp msig in - (l,Smodtype (extract_seb_spec env mtb.typ_expr)) :: specs - | (l,SFBalias(mp1,typ_opt,_))::msig -> - let mb = build_mb (SEBident mp1) typ_opt in - extract_sfb_spec env mp ((l,SFBmodule mb) :: msig) - -(* 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 - - from the output of [Modops.eval_struct]. - This way, any encountered [SEBident] should be a true module type. - For instance, [my_type_of_mb] ensures this invariant. -*) - -and extract_seb_spec env = function - | SEBident mp -> Visit.add_mp mp; MTident mp - | SEBwith(mtb',With_definition_body(idl,cb))-> - let env' = env_for_mtb_with env mtb' idl in - let mtb''= extract_seb_spec env mtb' in - (match extract_with_type env' cb with (* cb peut contenir des kn *) - | None -> mtb'' - | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ))) - | SEBwith(mtb',With_module_body(idl,mp,_,_))-> - Visit.add_mp mp; - MTwith(extract_seb_spec env mtb', - ML_With_module(idl,mp)) -(* TODO: On pourrait peut-etre oter certaines eta-expansion, du genre: - | SEBfunctor(mbid,_,SEBapply(m,SEBident (MPbound mbid2),_)) - when mbid = mbid2 -> extract_seb_spec env m - (* faudrait alors ajouter un test de non-apparition de mbid dans mb *) -*) - | SEBfunctor (mbid, mtb, mtb') -> - let mp = MPbound mbid in - let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MTfunsig (mbid, extract_seb_spec env mtb.typ_expr, - extract_seb_spec env' mtb') - | SEBstruct (msid, msig) -> - let mp = MPself msid in - let env' = Modops.add_signature mp msig env in - MTsig (msid, extract_sfb_spec env' mp msig) - | SEBapply _ as mtb -> - extract_seb_spec env (Modops.eval_struct env mtb) - - -(* 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 b = Visit.needed_kn kn in - if all || b then - let d = Dind (kn, extract_inductive env kn) 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 mtb.typ_expr)) :: ms - else ms - | (l,SFBalias (mp1,typ_opt,_)) :: msb -> - let mb = build_mb (SEBident mp1) typ_opt in - extract_sfb env mp all ((l,SFBmodule mb) :: msb) - -(* From [struct_expr_body] to implementations *) - -and extract_seb env mpo all = function - | 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 None true meb, - extract_seb env None true meb') - | SEBfunctor (mbid, mtb, meb) -> - let mp = MPbound mbid in - let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MEfunctor (mbid, extract_seb_spec env mtb.typ_expr, - extract_seb env' None true meb) - | SEBstruct (msid, msb) -> - let mp,msb = match mpo with - | None -> MPself msid, msb - | Some mp -> mp, Modops.subst_structure (map_msid msid mp) msb - in - let env' = Modops.add_signature mp msb env in - MEstruct (msid, 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 (Some mp) all (Option.get mb.mod_expr); - ml_mod_type = extract_seb_spec env (my_type_of_mb env 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 (Some 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 fc = - let d = descr () in - let fn = if d.capital_file then fc else String.uncapitalize fc - in - Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, id_of_string fc - -(*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 None; - 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 = make_short_qualid 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 (Some 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 - let s = string_of_modfile mp in - print_structure_to_file (module_filename s) dry [e] - | _ -> assert false - in - List.iter print struc; - reset () diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli deleted file mode 100644 index 8d906985..00000000 --- a/contrib/extraction/extract_env.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* 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: extract_env.mli 10895 2008-05-07 16:06:26Z letouzey $ 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/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml deleted file mode 100644 index 2cf457c6..00000000 --- a/contrib/extraction/extraction.ml +++ /dev/null @@ -1,917 +0,0 @@ -(************************************************************************) -(* 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: extraction.ml 11897 2009-02-09 19:28:02Z barras $ 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 Nameops -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 - -(*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. *) - Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; - (* 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 }) - mib.mind_packets - in - add_ind kn mib - {ind_info = Standard; - ind_nparams = npar; - ind_packets = packets; - ind_equiv = match mib.mind_equiv with - | None -> NoEquiv - | Some kn -> Equiv kn - }; - (* 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_kn 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 not (List.exists isKill (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 = match mib.mind_equiv with - | None -> NoEquiv - | Some kn -> Equiv kn } - 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. *) - -(* \begin{itemize} - \item [db] is a context for translating Coq [Rel] into ML type [Tvar] - \item [dbmap] is a translation map (produced by a call to [parse_in_args]) - \item [i] is the rank of the current product (initially [params_nb+1]) - \end{itemize} *) - -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) - -(*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, new_meta() - with NotDefault d -> dummy_name, 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, 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 - if mlargs = [] then mk_head type_head else 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 l = ref s in - let keep () = match !l with [] -> true | b :: s -> l:=s; b=Keep in - let rec f = function - | [], [] -> [] - | a::la, t::lt when keep() -> extract_maybe_term env e t a :: (f (la,lt)) - | _::la, _::lt -> f (la,lt) - | _ -> assert false - in f (args,typs) - -(*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 = type2signature env (snd schema) in - let ls = List.length s in - let la = List.length args in - 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 - (* Different situations depending of the number of arguments: *) - if ls = 0 then put_magic_if magic2 head - else if List.mem Keep s then - if la >= ls || not (List.exists isKill s) - then - put_magic_if (magic2 && not magic1) (MLapp (head, mla)) - else - (* Not enough arguments. We complete via eta-expansion. *) - let ls' = 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 (MLapp (head, mla)) s') - else if List.mem (Kill Kother) s then - (* In the special case of always false signature, one dummy lam is left. *) - (* So a [MLdummy] is left accordingly. *) - if la >= ls - then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla)) - else put_magic_if magic2 (dummy_lams head (ls-la-1)) - else (* s is made only of [Kill Ktype] *) - if la >= ls - then put_magic_if (magic2 && not magic1) (MLapp (head, mla)) - else put_magic_if magic2 (dummy_lams head (ls-la)) - - -(*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 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 = - (* 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 - (* 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 - (ConstructRef (ip,i+1), 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 (List.hd ids,a,e') - end - else - (* Standard case: we apply [extract_branch]. *) - MLcase ((mi.ind_info,[]), 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 env c t = - let rels = fst (decomp_n_prod env none n t) in - let rels = List.map (fun (id,_,c) -> (id,c)) rels in - let m = nb_lam c in - if m >= n then decompose_lam_n n c - else - 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 lambdas, 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 - (* The initial ML environment. *) - let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in - (* Decomposing the top level lambdas of [body]. *) - let rels,c = decomp_lams_eta_n (List.length s) env body typ in - (* The lambdas names. *) - let ids = List.map (fun (n,_) -> 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. *) - term_expunge s (ids,e), type_expunge env 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::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 l = List.filter (fun t -> not (isDummy (expand env t))) l in - let packets = - Array.map (fun p -> { p with ip_types = Array.map f 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/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli deleted file mode 100644 index 6d41b630..00000000 --- a/contrib/extraction/extraction.mli +++ /dev/null @@ -1,34 +0,0 @@ -(************************************************************************) -(* 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: extraction.mli 10497 2008-02-01 12:18:37Z soubiran $ 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 -> kernel_name -> 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/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 deleted file mode 100644 index 345cb307..00000000 --- a/contrib/extraction/g_extraction.ml4 +++ /dev/null @@ -1,123 +0,0 @@ -(************************************************************************) -(* 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 - -let pr_mlname _ _ _ s = spc () ++ qs s - -ARGUMENT EXTEND mlname - TYPED AS string - PRINTED BY pr_mlname -| [ preident(id) ] -> [ id ] -| [ string(s) ] -> [ s ] -END - -open Table -open Extract_env - -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 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) "]" ] - -> [ extract_inductive x (id,idl) ] -END diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml deleted file mode 100644 index 3f0366e6..00000000 --- a/contrib/extraction/haskell.ml +++ /dev/null @@ -1,334 +0,0 @@ -(************************************************************************) -(* 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: haskell.ml 11559 2008-11-07 22:03:34Z letouzey $ 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 (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 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] 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 ((_,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 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 - prvecti - (fun i x -> if List.mem i factors then mt () else - (pp_one_pat pv.(i) ++ - if factors = [] && i = Array.length pv - 1 then mt () - else fnl () ++ str " ")) pv - ++ - match factors with - | [] -> mt () - | i::_ -> - let (_,ids,t) = pv.(i) in - let t = ast_lift (-List.length ids) t in - hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) 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 - (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 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 kn i.ind_packets.(0) ++ fnl () - | Dind (kn,i) -> hov 0 (pp_ind true 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 pp_structure_elem = function - | (l,SEdecl d) -> pp_decl d - | (l,SEmodule m) -> - failwith "TODO: Haskell extraction of modules not implemented yet" - | (l,SEmodtype m) -> - failwith "TODO: Haskell extraction of modules not implemented yet" - -let pp_struct = - let pp_sel (mp,sel) = - push_visible mp None; - 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"; - capital_file = true; - preamble = preamble; - pp_struct = pp_struct; - sig_suffix = None; - sig_preamble = (fun _ _ _ -> mt ()); - pp_sig = (fun _ -> mt ()); - pp_decl = pp_decl; -} diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli deleted file mode 100644 index 1af9c231..00000000 --- a/contrib/extraction/haskell.mli +++ /dev/null @@ -1,12 +0,0 @@ -(************************************************************************) -(* 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: haskell.mli 10232 2007-10-17 12:32:10Z letouzey $ i*) - -val haskell_descr : Miniml.language_descr - diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli deleted file mode 100644 index dfe4eb48..00000000 --- a/contrib/extraction/miniml.mli +++ /dev/null @@ -1,188 +0,0 @@ -(************************************************************************) -(* 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: miniml.mli 10497 2008-02-01 12:18:37Z soubiran $ 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 unknown reason. *) - -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 - -type case_info = int list (* list of branches to merge in a _ pattern *) - -(* 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 } - -(* [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_ast = - | MLrel of int - | MLapp of ml_ast * ml_ast list - | MLlam of identifier * ml_ast - | MLletin of identifier * 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 * - (global_reference * identifier list * ml_ast) 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 mod_self_id * 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 mod_self_id * 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; - capital_file : bool; (* should we capitalize filenames ? *) - 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/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml deleted file mode 100644 index 4e2904ba..00000000 --- a/contrib/extraction/mlutil.ml +++ /dev/null @@ -1,1167 +0,0 @@ -(************************************************************************) -(* 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: mlutil.ml 13202 2010-06-25 22:36:30Z letouzey $ 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 = id_of_string "x" -let dummy_name = id_of_string "_" - -let id_of_name = function - | Anonymous -> anonymous - | Name id when id = dummy_name -> anonymous - | Name id -> id - -(*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 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 Idem, but only at the top level of implications. *) - -let is_arrow = function Tarr _ -> true | _ -> false - -let type_weak_expand env t = - let rec expand = function - | Tmeta {contents = Some t} -> expand t - | Tglob (r,l) as t -> - (match env r with - | Some mlt -> - let u = expand (type_subst_list l mlt) in - if is_arrow u then u else t - | None -> t) - | Tarr (a,b) -> Tarr (a, expand b) - | a -> a - in expand 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 i = if i = dummy_name then Kill Kother else Keep - -(*s Removing [Tdummy] from the top level of a ML type. *) - -let type_expunge env t = - let s = type_to_signature env t in - if s = [] then t - else if List.mem Keep s then - let rec f t s = - if List.exists isKill s then - match t with - | Tmeta {contents = Some t} -> f t s - | Tarr (a,b) -> - let t = f b (List.tl s) in - if List.hd s = Keep then Tarr (a, t) else t - | Tglob (r,l) -> - (match env r with - | Some mlt -> f (type_subst_list l mlt) s - | None -> assert false) - | _ -> assert false - else t - in f t s - else if List.mem (Kill Kother) s then - Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t))) - else snd (type_decomp (type_weak_expand env t)) - -(*S Generic functions over ML ast terms. *) - -(*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] and [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 - ast_lift n v.(i'-1) - 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 in anonymous version. *) - -let rec anonym_lams a = function - | 0 -> a - | n -> anonym_lams (MLlam (anonymous,a)) (pred n) - -(*s Idem for [dummy_name]. *) - -let rec dummy_lams a = function - | 0 -> a - | n -> dummy_lams (MLlam (dummy_name,a)) (pred 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_name, 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) - -(*s Applies a substitution [s] of constants by their body, plus - linear beta reductions at modified positions. *) - -let rec ast_glob_subst s t = match t with - | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> - let a = List.map (ast_glob_subst s) 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_and_generalize (r0,l,c)] transforms any [MLcons(r0,l)] in [MLrel 1] - and raises [Impossible] if any variable in [l] occurs outside such a - [MLcons] *) - -let check_and_generalize (r0,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=r0 && (test_eta_args_lift n nargs args) -> - MLrel (n+1) - | a -> ast_map_lift genrec n a - in genrec 0 c - -(*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 the identity case optimization. *) - -(* CAVEAT: this optimization breaks typing 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]. - By default, we brutally disable this optim except for some known types: - [bool], [sumbool], [sumor] *) - -let generalizable_list = - let datatypes = MPfile (dirpath_of_string "Coq.Init.Datatypes") - and specif = MPfile (dirpath_of_string "Coq.Init.Specif") - in - [ make_kn datatypes empty_dirpath (mk_label "bool"); - make_kn specif empty_dirpath (mk_label "sumbool"); - make_kn specif empty_dirpath (mk_label "sumor") ] - -let check_generalizable_case unsafe br = - if not unsafe then - (match br.(0) with - | ConstructRef ((kn,_),_), _, _ -> - if not (List.mem kn generalizable_list) then raise Impossible - | _ -> assert false); - let f = check_and_generalize br.(0) in - for i = 1 to Array.length br - 1 do - if check_and_generalize br.(i) <> f then raise Impossible - done; f - -(*s Detecting similar branches of a match *) - -(* If several branches of a match are equal (and independent from their - patterns) we will print them using a _ pattern. If _all_ branches - are equal, we remove the match. -*) - -let common_branches br = - let tab = Hashtbl.create 13 in - for i = 0 to Array.length br - 1 do - let (r,ids,t) = br.(i) in - let n = List.length ids in - if not (ast_occurs_itvl 1 n t) then - let t = ast_lift (-n) t in - let l = try Hashtbl.find tab t with Not_found -> [] in - Hashtbl.replace tab t (i::l) - done; - let best = ref [] in - Hashtbl.iter - (fun _ l -> if List.length l > List.length !best then best := l) tab; - if List.length !best < 2 then [] else !best - -(*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_name 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 - -(*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(id,c,e) -> - let e = (simpl o e) in - if - (id = dummy_name) || (is_atomic c) || (is_atomic e) || - (let n = nb_occur_match e in n = 0 || (n=1 && 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 - -and simpl_app o a = function - | MLapp (f',a') -> simpl_app o (a'@a) f' - | MLlam (id,t) when id = dummy_name -> - 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 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) - -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 - try (* Does a term [f] exist such that each branch is [(f e)] ? *) - if not o.opt_case_idr then raise Impossible; - let f = check_generalizable_case o.opt_case_idg br in - simpl o (MLapp (MLlam (anonymous,f),[e])) - with Impossible -> - (* Detect common branches *) - let common_br = if not o.opt_case_cst then [] else common_branches br in - if List.length common_br = Array.length br && br <> [||] then - let (_,ids,t) = br.(0) in ast_lift (-List.length ids) t - else - let new_i = (fst i, common_br) in - (* Swap the case and the lam if possible *) - if o.opt_case_fun - then - let ids,br = permut_case_fun br [] in - let n = List.length ids in - if n <> 0 then named_lams ids (MLcase (new_i,ast_lift n e, br)) - else MLcase (new_i,e,br) - else MLcase (new_i,e,br) - -let rec post_simpl = function - | MLletin(_,c,e) when (is_atomic (eta_red c)) -> - post_simpl (ast_subst (eta_red c) e) - | a -> ast_map post_simpl a - -(*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 MLdummy in - let rec parse_ids i j = function - | [] -> () - | Keep :: l -> v.(i) <- 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_name :: 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. *) - -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 = [] && List.mem (Kill Kother) s then - MLlam (dummy_name, 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 fi 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) -> - (try - let ids,c = kill_dummy_fix i fi c in - let a = List.map (fun t -> ast_lift 1 (kill_dummy t)) a in - let e = kill_dummy_args ids (MLrel 1) (MLapp (MLrel 1,a)) in - ast_subst (MLfix (i,fi,c)) e - with Impossible -> - MLapp(MLfix(i,fi,Array.map kill_dummy c),List.map kill_dummy a)) - | MLletin(id, MLfix (i,fi,c),e) -> - (try - let ids,c = kill_dummy_fix i fi 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 c in - let e = kill_dummy_args ids (MLrel 1) e in - MLletin (id, kill_dummy c,kill_dummy e) - with Impossible -> MLletin(id,kill_dummy c,kill_dummy e)) - | a -> ast_map kill_dummy a - -and kill_dummy_fix i fi c = - let n = Array.length fi in - let ids,ci = kill_dummy_lams 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 a = simpl o a in - if o.opt_kill_dum then post_simpl (kill_dummy a) else 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_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 (MLrel n, _) -> - List.filter ((<>) n) cand - (* In [(x y)] we say that only x is strict. Cf [sig_rec]. We may *) - (* gain something if x is replaced by a function like a projection *) - | 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. *) - -let inline_test t = - 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 manual_inline_list = - let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in - List.map (fun s -> (make_con mp empty_dirpath (mk_label s))) - [ "well_founded_induction_type"; "well_founded_induction"; - "Acc_rect"; "Acc_rec" ; "Acc_iter" ; "Fix" ] - -let manual_inline = function - | ConstRef c -> List.mem c manual_inline_list - | _ -> 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 *) - || (auto_inline () && lang () <> Haskell && not (is_projection r) - && (is_recursor r || manual_inline r || inline_test t))) - diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli deleted file mode 100644 index a55caaf2..00000000 --- a/contrib/extraction/mlutil.mli +++ /dev/null @@ -1,113 +0,0 @@ -(************************************************************************) -(* 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: mlutil.mli 8724 2006-04-20 09:57:01Z letouzey $ 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 : kernel_name -> 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 isDummy : ml_type -> bool -val isKill : sign -> bool - -val case_expunge : signature -> ml_ast -> identifier list * ml_ast -val term_expunge : signature -> identifier 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 : identifier -val dummy_name : identifier -val id_of_name : name -> identifier - -(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns - the list [idn;...;id1] and the term [t]. *) - -val collect_lams : ml_ast -> identifier list * ml_ast -val collect_n_lams : int -> ml_ast -> identifier list * ml_ast -val nb_lams : ml_ast -> int - -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 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 - - - diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml deleted file mode 100644 index 68adeb81..00000000 --- a/contrib/extraction/modutil.ml +++ /dev/null @@ -1,365 +0,0 @@ -(************************************************************************) -(* 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: modutil.ml 11602 2008-11-18 00:08:33Z letouzey $ 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 -> begin - match Modops.eval_struct (Global.env()) (SEBident mp) with - | SEBstruct(msid,_) -> MPself msid - | _ -> anomaly "Extraction:the With can't be applied to a funsig" - end - | 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 - | Equiv kne -> do_type (IndRef (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 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 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 -> assert false - - -(*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 (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 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 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 - 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/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli deleted file mode 100644 index e279261d..00000000 --- a/contrib/extraction/modutil.mli +++ /dev/null @@ -1,41 +0,0 @@ -(************************************************************************) -(* 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: modutil.mli 11602 2008-11-18 00:08:33Z letouzey $ 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/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml deleted file mode 100644 index 0166d854..00000000 --- a/contrib/extraction/ocaml.ml +++ /dev/null @@ -1,731 +0,0 @@ -(************************************************************************) -(* 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: ocaml.ml 11559 2008-11-07 22:03:34Z letouzey $ 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 pp_global k r = - if is_inline_custom r then str (find_custom r) - else str (Common.pp_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 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' _ | 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 ++ spc () ++ str (get_infix r) ++ spc () ++ - pp_rec true a2) - | Tglob (r,[]) -> pp_global Type r - | Tglob (r,l) -> - if r = IndRef (kn_sig,0) then - pp_tuple_light pp_rec l - else - 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 - - -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 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] 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 (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) ++ spc () ++ str (get_infix r) ++ - spc () ++ (pp_expr true env [] arg2)) - | MLcons (_,r,args') -> - assert (args=[]); - let tuple = pp_tuple (pp_expr true env []) args' in - pp_par par (pp_global Cons r ++ spc () ++ tuple) - | 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 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 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 " " ++ str (get_infix r) ++ str " " ++ pr_id i2 - | [] -> pp_global Cons r - | ids -> pp_global Cons r ++ str " " ++ pp_boxed_tuple pr_id ids), - expr - -and pp_pat env (info,factors) pv = - prvecti - (fun i x -> if List.mem i factors then mt () else - let s1,s2 = pp_one_pat env info x in - hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++ - (if factors = [] && i = Array.length pv-1 then mt () - else fnl () ++ str " | ")) pv - ++ - match factors with - | [] -> mt () - | i::_ -> - let (_,ids,t) = pv.(i) in - let t = ast_lift (-List.length ids) t in - hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t) - -and pp_function env t = - let bl,t' = collect_lams t in - let bl,env' = push_vars bl env in - match t' with - | MLcase(i,MLrel 1,pv) when fst i=Standard -> - 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 (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 (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 (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 (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 ((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 = (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 (Some l) mt in - let def' = pp_module_type (Some l) 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 None 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 ol = function - | MTident kn -> - pp_modname kn - | MTfunsig (mbid, mt, mt') -> - let typ = pp_module_type None mt in - let name = pp_modname (MPbound mbid) in - let def = pp_module_type None mt' in - str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def - | MTsig (msid, sign) -> - let tvm = top_visible_mp () in - let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in - (* References in [sign] are in short form (relative to [msid]). - In push_visible, [msid-->mp] is added to the current subst. *) - push_visible mp (Some msid); - 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 None; - let s = - pp_module_type None mt ++ str " with type " ++ - pp_global Type r ++ ids - in - pop_visible(); - s ++ str "=" ++ spc () ++ 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 None; - let s = - pp_module_type None mt ++ str " with module " ++ pp_modname mp_w - in - pop_visible (); - s ++ 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 (Some l) m.ml_mod_type - else mt () - in - let def = pp_module_expr (Some l) 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 None 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 ol = function - | MEident mp' -> pp_modname mp' - | MEfunctor (mbid, mt, me) -> - let name = pp_modname (MPbound mbid) in - let typ = pp_module_type None mt in - let def = pp_module_expr None me in - str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def - | MEapply (me, me') -> - pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")" - | MEstruct (msid, sel) -> - let tvm = top_visible_mp () in - let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in - (* No need to update the subst with [Some msid] below : names are - already in long form (see [subst_structure] in [Extract_env]). *) - push_visible mp None; - 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 None; - 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"; - capital_file = false; - 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/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli deleted file mode 100644 index 3d90e74c..00000000 --- a/contrib/extraction/ocaml.mli +++ /dev/null @@ -1,12 +0,0 @@ -(************************************************************************) -(* 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: ocaml.mli 10232 2007-10-17 12:32:10Z letouzey $ i*) - -val ocaml_descr : Miniml.language_descr - diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml deleted file mode 100644 index f4941a9c..00000000 --- a/contrib/extraction/scheme.ml +++ /dev/null @@ -1,202 +0,0 @@ -(************************************************************************) -(* 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: scheme.ml 11559 2008-11-07 22:03:34Z letouzey $ 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 fl env in - apply (pp_abst (pp_expr env' [] a') (List.rev fl)) - | MLletin (id,a1,a2) -> - let i,env' = push_vars [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 ((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 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 pp_structure_elem = function - | (l,SEdecl d) -> pp_decl d - | (l,SEmodule m) -> - failwith "TODO: Scheme extraction of modules not implemented yet" - | (l,SEmodtype m) -> - failwith "TODO: Scheme extraction of modules not implemented yet" - -let pp_struct = - let pp_sel (mp,sel) = - push_visible mp None; - 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"; - capital_file = false; - preamble = preamble; - pp_struct = pp_struct; - sig_suffix = None; - sig_preamble = (fun _ _ _ -> mt ()); - pp_sig = (fun _ -> mt ()); - pp_decl = pp_decl; -} diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli deleted file mode 100644 index a88bb6db..00000000 --- a/contrib/extraction/scheme.mli +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* 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: scheme.mli 10232 2007-10-17 12:32:10Z letouzey $ i*) - -val scheme_descr : Miniml.language_descr diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml deleted file mode 100644 index c675a744..00000000 --- a/contrib/extraction/table.ml +++ /dev/null @@ -1,653 +0,0 @@ -(************************************************************************) -(* 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: table.ml 11844 2009-01-22 16:45:06Z letouzey $ i*) - -open Names -open Term -open Declarations -open Nameops -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 modpath_of_r = function - | ConstRef kn -> con_modpath kn - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> modpath kn - | VarRef _ -> assert false - -let label_of_r = function - | ConstRef kn -> con_label kn - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> label kn - | VarRef _ -> assert false - -let rec base_mp = function - | MPdot (mp,l) -> base_mp mp - | mp -> mp - -let rec mp_length = function - | MPdot (mp, _) -> 1 + (mp_length mp) - | _ -> 1 - -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 visible_kn kn = at_toplevel (base_mp (modpath kn)) -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 - | [] -> raise Not_found - | mp :: l -> if MPset.mem mp prefixes then 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 labels_of_ref r = - let mp,_,l = - match r with - ConstRef con -> repr_con con - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> repr_kn kn - | VarRef _ -> assert false - in - parse_labels [l] 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 (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t) -let init_inductives () = inductives := KNmap.empty -let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives -let lookup_ind kn = KNmap.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 (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_id_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 safe_pr_global r = - try Printer.pr_global r - with _ -> pr_id (safe_id_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.dir_of_mp mp) in - str (String.concat "." (List.map string_of_id (List.rev lid))) - -let pr_long_global ref = pr_sp (Nametab.sp_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 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 s = - err (str ("There are two Coq modules with ML name " ^ s ^".\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." ++ - 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 check_loaded_modfile mp = match base_mp mp with - | MPfile dp -> if not (Library.library_is_loaded dp) then - err (str ("Please load library "^(string_of_dirpath dp^" first."))) - | _ -> () - -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 true - -let auto_inline () = !auto_inline_ref - -let _ = declare_bool_option - {optsync = true; - optname = "Extraction AutoInline"; - optkey = SecondaryTable ("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 = SecondaryTable ("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]. *) - -let int_flag_init = 1 + 2 + 4 + 8 + 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 = SecondaryTable ("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 = SecondaryTable("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); - export_function = (fun x -> Some x)} - -let _ = declare_summary "Extraction Lang" - { freeze_function = (fun () -> !lang_ref); - unfreeze_function = ((:=) lang_ref); - init_function = (fun () -> lang_ref := Ocaml); - survive_module = true; - survive_section = true } - -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); - export_function = (fun x -> Some x); - 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); - survive_module = true; - survive_section = true } - -(* 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); - export_function = (fun x -> Some x)} - -let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) - -(*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' - -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); - export_function = (fun x -> Some x); - 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); - survive_module = true; - survive_section = true } - -(* 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); - export_function = (fun x -> Some x)} - -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 - -(* 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); - export_function = (fun x -> Some x); - 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); - survive_module = true; - survive_section = true } - -(* 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) = - 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)); - 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/contrib/extraction/table.mli b/contrib/extraction/table.mli deleted file mode 100644 index 5ef7139e..00000000 --- a/contrib/extraction/table.mli +++ /dev/null @@ -1,151 +0,0 @@ -(************************************************************************) -(* 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: table.mli 11844 2009-01-22 16:45:06Z letouzey $ i*) - -open Names -open Libnames -open Miniml -open Declarations - -val safe_id_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 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 : string -> '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 info_file : string -> unit - -(*s utilities about [module_path] and [kernel_names] and [global_reference] *) - -val occur_kn_in_ref : kernel_name -> global_reference -> bool -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 is_toplevel : module_path -> bool -val at_toplevel : module_path -> bool -val visible_kn : kernel_name -> 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 -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 : kernel_name -> mutual_inductive_body -> ml_ind -> unit -val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind - -val add_recursors : Environ.env -> kernel_name -> 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 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 - -(*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 -> unit - -(*s Table of blacklisted filenames *) - -val extraction_blacklist : identifier list -> unit -val reset_extraction_blacklist : unit -> unit -val print_extraction_blacklist : unit -> unit - - - |