aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/extraction.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
2009-02-06pushed evar reduction in kernelbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 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-10-16Extraction of Module with eq = ... : fix for bug #1853letouzey
(unrelated: a useless pattern variable becomes _ in Extract_env) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11458 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-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
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
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
2007-10-08Better use of tables for storing results of extract_ind (bug #1709)letouzey
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
2007-10-06Extraction: factorisation of identical branches in a matchletouzey
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
2006-12-17reparation bug 1239letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9455 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
(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
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de ↵herbelin
famille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9032 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09oups: il faut penser a fermer la porte en partant (d'un fixpoint)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8931 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-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-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-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-30evite certaines eta-expansions cavalieresletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7629 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
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Standardisation of function names about global references (especially, ↵herbelin
renaming of constr_of_reference into constr_of_global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09travail sur les types extraitsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6441 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
2004-06-25correspondance des records et noms de champs de records entre un module et ↵letouzey
sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10révision du traitement des axiomes non réalisésletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4849 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-28correction d'un stack overflow possible (PR#320)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4278 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29:= dans un record engendre un LetIn qui n'etait pas géréletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4087 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28bug concernant les projecteurs de Record avec args logiquesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3967 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-25Extract Constant marche avec les axiomes schémas de typesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3788 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-11pour ocamlwebletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3753 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-03encore un long_knletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3647 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-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-28nouvelle gestion des constantes de typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3616 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-23oubli des add_recursors singleton logiquesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3601 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-19les empty ind et les singletons etaient oublies par add_recursorsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3461 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-13une branche de case inutileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3431 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09petit bugletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3389 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-11-28 bug pp letin + un inductif constant n'est pas un recordletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3324 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Extraction des Record, suiteletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3309 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 15:36:27 +0000