aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/common.ml
AgeCommit message (Collapse)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-06Cosmetic: no more whitespace at end of lines in extraction filesletouzey
(diff says it's a big commit, whereas diff -w says it's an empty one ;-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11547 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Better extraction renaming phase (fix #1914 plus other non-reported bugs)letouzey
Ocaml : - Fix the Coq__1 that was appearing in a .mli for some functor app in the corresponding .ml (virtual printing of the interface in the .ml + a pp_modname delayed in MTfunsig) - Cleanup in MTwith parts - Better handling of subst for MTsig - Correct push/pop_visible in pp_struct/pp_signature Common : - Merge most of pp_global and pp_module - Clarify the use of tables : remove some of them, attach many others to their corresponding function. - The "visible" table now groups mps, their content, and some subst (for the inside of MTsig) - Cleanup of tables is done via a registration mecanism - No more "initial" create_renamings, instead some fully on-the-fly renaming (thanks to the "Pre" phase) - opened libaries are computed between "Pre" and "Impl" phases - for simplicity, static_clash aren't computed statically anymore (cost?) Extract_env: - A "Pre" phase not only for Ocaml - Extraction Library is in fact also Recursive (for getting a right mpfiles_content) ... but only last item is printed to a real file instead of /dev/null Modutil: No more struct_get_references_* Util : fix the evaluation order of prlist_strict git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11538 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-21warning message when a qualid to extract can be both a module or a cstletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11485 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10596 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
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
2007-10-17Major reorganisation of the extraction "backend".letouzey
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
2006-06-09changements de dernieres minutes pour la 8.1 beta: letouzey
- 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
2006-06-08reparation bug 1006letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8921 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
- 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
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-20decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8724 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-16multiples ameliorations de l'extraction scheme:letouzey
- 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
2005-12-01amelioration de la generation des unsafeCoerceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7632 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-17merci les warnings de 3.09 ...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7574 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Modules et Records: gros changements pour prendre en compte le nouveau ↵letouzey
mind_record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5836 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10message informant de l'ecriture d'un fichier extraitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4850 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-10renommage des modules 1er niveau en monolithiqueletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4233 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12enieme correction du nommage modulaireletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4143 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Ooopsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3937 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17temporaireletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3935 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16BIG MAJ Extraction:letouzey
------------------ - (Recursive) Extraction Module devient (Recursive) Extraction Library (pour cause d'ambiguite avec les nouveaux modules Coq). - un nouveau Extraction Module qui extrait dans le toplevel tout module Coq - tout fixpoint est de nouveau inlinable (Yves). - fix bug du calcul d'env minimal des modules en extraction monolithique. - un nouveau fichier Modutil regroupant manques de Modops & functions specifiques aux modules MiniML - plus d'aliases a trainer (mais des substitutions des le depart) - ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes et les functors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3934 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-11pour coq-ideletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3754 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-21bugs/améliorations trouvés via FTAletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3688 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-03hack horrible pour renommage dans Modules Types et Functeursletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3648 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-02plus d'environment fixe cur_env mais un environment evolutifletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3645 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30pb d'hier resolu. Recommitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3624 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-29apres le backtrack precedent, remise de trois points precis et sursletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3623 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-29Ca a tout pété -> Bactrack a la version d'hierletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3622 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-29affichage module et module typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3621 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-28workaround en attendant traitement reel des modules typesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3618 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Extraction des modules, enfin !letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3569 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09chamboulement du codage des indcutifs extraits; deplacements des tables; ...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3388 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-05code cleanup (+ debut de commencement de modules)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3380 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-03la table PARAMETER n'existe plus (mergé dans la table CONSTANT)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3369 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-292 bugs: 1) projections pas renommées 2) mutual fixpoints a l'enversletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3345 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Remaniement du pp, suite: vers un renommage modulaire correcteletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3336 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Reorganisation du pretty-print:letouzey
- Dfix sans rename_global - question du renommage - code cleanup (plein) Encore a finir: bug modules/qualification et syntax records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3321 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05cosmetiqueletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3210 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-31L'extraction c'est magic cvs -n upletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3199 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-24suite chgt liés aux modulesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3029 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-24reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2913 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Gros Remaniement Extraction:letouzey
* extraction.ml + modulaire (cf extract_type) et + proche theorie (cf feu extract_app) * table.ml filtre les Extract Constant vers types ou terms * extract_env.ml refuse maintenant les Extraction constr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2886 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07extraction vers schemeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08babioles de renommagesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2622 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ↵letouzey
dummy git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2619 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-26Refonte complete de la génération des types MLletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2568 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 08:56:13 +0000