aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
Commit message (Collapse)AuthorAge
* Extraction: better dependency computation (after optimisations)Gravatar letouzey2008-07-20
| | | | | | | | | | | | | | | | | | When doing monolithic extraction, the initial dependency graph may turn to be too broad thanks to later optimisations. We now do an extra dependency pass at the end, killing more useless code. In addition, when doing an "Extract Constant t => ...", if t isn't an axiom, we don't include the dependencies of the body of t. This may break earlier extraction setups (with or without Extract Constant), since they may take advantage of objects that were earlier "wrongly" included in the extracted code. The fix is simple : just add these missing objects to the extraction command-line. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11239 85f007b7-540e-0410-9357-904b9bb8a0f7
* export Extract_env.mono_environment in the mli Gravatar letouzey2008-05-07
| | | | | | | for debug / external output via coqtop.byte + Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10895 85f007b7-540e-0410-9357-904b9bb8a0f7
* first-order --> firstorder (kills a warning about not being a valid id)Gravatar letouzey2008-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10805 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix some bogus calls to id_of_string by the extractionGravatar letouzey2008-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10794 85f007b7-540e-0410-9357-904b9bb8a0f7
* nettoyage de code obsolete.Gravatar soubiran2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10665 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attempt of fix for extraction of modules typesGravatar letouzey2008-03-05
| | | | | | | | | | | | | | | | | * When no explicit module type is given in Coq, extraction proceeds with more caution when recontructing a module type from the module. For instance, a module ident isn't keep, since it's the name of an implementation, not of a module type. Fix the bug functor M -> M : funsig M -> M instead of funsig M -> typeof(M) * Removed duplicated code with Modops * The call to replicate_msid doesn't seem to be as crucial as before. Let's try to remove it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10620 85f007b7-540e-0410-9357-904b9bb8a0f7
* dead codeGravatar letouzey2008-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10596 85f007b7-540e-0410-9357-904b9bb8a0f7
* typoGravatar letouzey2008-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10592 85f007b7-540e-0410-9357-904b9bb8a0f7
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | kernel: -declaration.ml unification des representations pour les modules et modules types. (type struct_expr_body) -mod_typing.ml le typage des modules est separe de l'evaluation des modules -modops.ml nouvelle fonction qui pour toutes expressions de structure calcule sa forme evaluee.(eval_struct) -safe_typing.ml ajout du support du nouvel operateur Include.(add_include). library: -declaremods.ml nouveaux objets Include et Module-alias et gestion de la resolution de noms pour les alias via la nametab. parsing: -g_vernac.ml4: nouvelles regles pour le support des Includes et pour l'application des signatures fonctorielles. extraction: Adaptation a la nouvelle representation des modules et support de l'operateur with. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Récupération d'une exception Not_foundGravatar notin2008-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10460 85f007b7-540e-0410-9357-904b9bb8a0f7
* cosmetics: after an extract inductive to bool, let's use if then elseGravatar letouzey2008-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction inlines Wf.Fix by default (wish of Y.Bertot)Gravatar letouzey2007-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10329 85f007b7-540e-0410-9357-904b9bb8a0f7
* small fix of commit 10188: a string given via Extract Inductive can be emptyGravatar letouzey2007-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10266 85f007b7-540e-0410-9357-904b9bb8a0f7
* An error message instead of an empty extraction when the monolithic Gravatar letouzey2007-10-21
| | | | | | | | extraction is given the name of a .v Module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid the auto-inlining of small fixpoints like List.map.Gravatar letouzey2007-10-21
| | | | | | | | A better eta-reduction allows to detect that List.map is indeed a fixpoint. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10244 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repair Haskell/Scheme extraction in the new extraction backend design: Gravatar letouzey2007-10-17
| | | | | | | | | | | | | | | Unlike prlist_xxxx and prvect, the function prlist is acting lazily, which is bad for extraction (synchronization with tables). We add and use a prlist_strict function. Additionaly: - cleanup of the preamble printing - no need for 2-pass printing (/dev/null trick) when the language isn't ocaml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10233 85f007b7-540e-0410-9357-904b9bb8a0f7
* Major reorganisation of the extraction "backend".Gravatar letouzey2007-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Initial Idea: getting rid of nasty renaming issues in modules, in particular bugs #820 (part d) #1340 #1526 #1654 Final effect: lots of changes, simplifications, cleanups, unrelated fixes and ehancements, and also probably some regressions (time will tell). A few details: * no more experimental "Toplevel" language. * no more functors Make in Ocaml/Haskell/Scheme. The spirit of these functors and Mlpp_params was already not followed much, and this framework was more a nuisance that anything else. * instead, some records language_descr regrouping the specific features of the different output languages. * Common now comes before Ocaml/Haskell/Scheme, these ones are now independant from each others. print_structure_to_file is now in Extract_env. * A nice detail: no more duplications of warnings concerning axioms. * In modular extraction, the clashes due to the opened modules are now computed once and for all thanks to record_contents_fstlev, instead of re-asking Coq each time about these opened modules and using Extraction.constant_kind * some utilities about modules_path added and/or moved from Modutil to Table. * using a .v file as a module, e.g. in a functor application should now works in modular extraction. Now concerning renaming issues themselves: * printing is done twice, the first time toward /dev/null, in order to encounter the naming issues unsolvable by a simple qualification. On the second run, we create artificial modules Coq__123 for allowing qualification of these hidden objects. * names are now fully separated into their syntaxic categories: terms/types/constructors/modules * Only one last unsupported situation (but at least detected and signaled by an error): an object M.t from an external file-module M.v can't be printed when a local module M is in the way. This situation is really unlikely (in Coq you must use _long_ file-module name, e.g. Init.Datatypes.nat). It could be solved by inserting "module Coq_123 = M" at the beginning of the file, but then the signature of Coq_123 (that is, the one of M) should be written explicitely in the .mli, which is _really_ not nice. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10232 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction now checks that the required libraries are indeed loaded (bug #1144)Gravatar letouzey2007-10-09
| | | | | | | | | | | If a library is Require'd from inside an "opaque" Module (e.g. a module with an interface given by a ":"), then the required library is not loaded anymore after closing this module. We add an error in this situation, asking the user to manually do a Require before performing the Extraction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10208 85f007b7-540e-0410-9357-904b9bb8a0f7
* forbid extraction under a module typeGravatar letouzey2007-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10206 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extract Inline/Inductive/Constant can now be used from inside a moduleGravatar letouzey2007-10-09
| | | | | | | | It even seems to work from inside a functor. Fix old bug #472. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better use of tables for storing results of extract_ind (bug #1709)Gravatar letouzey2007-10-08
| | | | | | | | | | | | | | | It is critical to avoid duplicated calls to extract_ind (see e.g. example in #1709). But the same kernel_name can lead to different inductive bodies, due to module substitutions. So we used to factorize only "visible" kn, that were not subject to change under substitution. As shown by P. Cregut in #1709, this is not enough. New approach is now to store also Coq inductive data (mib). If the recorded mib matches the current one, we trust the recorded result, otherwise we start a fresh computation of extract_ind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10194 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allowing infix constructors/types in a Extract InductiveGravatar letouzey2007-10-06
| | | | | | | | | | | | | | | | | | If a constructor has two arguments and the corresponding string given in a Extract Inductive is of the form "(foo)", then foo is used as an infix constructor. Idem for a inductive type name. Examples: Extract Inductive list => list [ "[]" "(::)" ]. Extract Inductive prod => "(*)" [ "(,)" ]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: factorisation of identical branches in a matchGravatar letouzey2007-10-06
| | | | | | | | | | | | If a match has two or more identical branches (that moreover do not depend on their pattern variables), we merge them in a last branch whose pattern is _ If _all_ branches are identical, we just remove the match git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deletion of contrib/extraction/testGravatar letouzey2007-07-12
| | | | | | | | | | Not maintained, probably broken, of no interest except (maybe) for myself, bad interaction with tools that work recursively (coqdep). ===> I move it to a personal repository git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9986 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite au mail de Lionel a propos du Makefile: Gravatar letouzey2007-01-12
| | | | | | | | | | | | | | | | | 1) Disparition de test_extraction.v rebasculé dans test-suite/success/extraction.v Au passage, remplacement de quelques Set en Type pour ne pas avoir besoin du -impredicative-set. Et ajout de passes d'extraction en Haskell et Scheme. Simplification du Makefile en conséquence (plus de barestate) 2) Au passage, reparation (et embellissement) de extract_env. Depuis le passage de Claudio dans cette portion (il y a 2 ans ?), faire Extraction S (ou tout autre constructeur) echouait. Idem pour un nom d'inductif mutuel autre que le premier du paquet. Etonnant que personne n'ait remarqué ca plus tot... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9484 85f007b7-540e-0410-9357-904b9bb8a0f7
* un saut de ligne ...Gravatar letouzey2007-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9483 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite de la reparation du bug 1239: apres les inds, les records et vars de typesGravatar letouzey2007-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9471 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation bug 1239Gravatar letouzey2006-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
| | | | | | | | | | (suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1211Gravatar notin2006-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9205 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1172 + correction en passant de la taille des paramètres de ↵Gravatar herbelin2006-07-07
| | | | | | famille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9032 85f007b7-540e-0410-9357-904b9bb8a0f7
* oups: il faut penser a fermer la porte en partant (d'un fixpoint)Gravatar letouzey2006-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8931 85f007b7-540e-0410-9357-904b9bb8a0f7
* changements de dernieres minutes pour la 8.1 beta: Gravatar letouzey2006-06-09
| | | | | | | | | | | | | | - qualification correcte des noms en Haskell - on imprime les types de toutes les fonctions en Haskell - en Ocaml, les appels recursifs d'une f : 'a truc doivent se faire avec les _meme_ parametres de types 'a. Exemple illegal: let rec f = function [] -> 0 | l -> f [l];; On met maintenant des Obj.magic en conséquence. En Haskell (avec typage fourni), ca passe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8930 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation bug 1006Gravatar letouzey2006-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8921 85f007b7-540e-0410-9357-904b9bb8a0f7
* debut de reparation du test d'extractionGravatar letouzey2006-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8891 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation bug #1128Gravatar letouzey2006-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
| | | | | | | | | | | - prise en compte du niveau à la déclaration du type comme une fonction des sortes des conclusions des paramètres uniformes - suppression du retypage de chaque instance de type inductif (trop coûteux) et donc abandon de l'idée de calculer une sorte minimale même dans des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵Gravatar notin2006-04-28
| | | | | | 'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)Gravatar letouzey2006-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement Pp.qs par Pptactic.qsnewGravatar herbelin2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7751 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵Gravatar herbelin2005-12-26
| | | | | | G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de ↵Gravatar herbelin2005-12-21
| | | | | | tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7681 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration de l'extraction haskell: affichage du type des fonctions, et ↵Gravatar letouzey2005-12-16
| | | | | | suppression des Sig git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7653 85f007b7-540e-0410-9357-904b9bb8a0f7
* multiples ameliorations de l'extraction scheme:Gravatar letouzey2005-12-16
| | | | | | | | | | - une syntaxe unique bigloo / pas bigloo (match sans ?) - un (load "macros_extr.scm") initial, et un mot sur ou le trouver - gestion des realisations d'axiomes - les ' dans les identifiateurs sont translates vers ~ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7651 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-26 11:50:18 +0000