aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/miniml.mli
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-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
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-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
2004-09-06reparation des Extract Constant avec Haskellletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6064 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-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-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-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-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-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-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-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-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-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-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
2002-03-19remplacement des deux constants prop/arity par une seule dummy + ↵letouzey
pretty-print des fix mutuels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2544 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Big commit extraction:letouzey
- Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell) - Retour des inductifs singletons et vides dans extraction.ml (extraction.ml -> actions sur le type, mlutil.ml -> conserve le type) - maintenant par defaut Recursive Extraction === Extraction "file" - kill_prop global est fait dans extraction.ml selon typage (a suivre...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2508 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15suite et fin (?) de haskell: gestion des modules, mise en place du'un testletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2480 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12Test & correction de la production de code Haskellletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2468 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2181 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-03Creation de Recursive Extarction Moduleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2152 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-31multiples bricoles. Cf mon TODO papierletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2147 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-30legeres modifs pretty-print de l'extractionsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2146 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-26Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ↵letouzey
ETC etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2141 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-22chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les ↵letouzey
options git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2133 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-30commentaires mlutil + binders_fold en coursletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1727 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Fin d'optimisation (cas modules) + warning pour coind & ocamlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1685 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24cofix_warning dans les parametres d'extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1683 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.letouzey
Du coup MLcons avec 2 args seulement. Ne reclame pas de realiser axioms sur Prop. Optimizations=true par default pour Extraction Module. Simplifications naives des letin. Merge_app avant normalisation. Booleen expansion_test pour l'optimisation, avec test de strictness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1662 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04documentationfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1530 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28changement type_var et signaturefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1498 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-27extraction recursive d'un morceau d'environnementfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1493 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23eta-expansion des constructeurs si necessaire (a posteriori en miniML)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1481 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14interface du extract_rec. Extract_constr prend un environnementletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1464 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Commentaires. Verification des assert false. Probleme des types ML arity.letouzey
Correction des dependances pour bin/coq-extraction dans le Makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1448 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 13:30:17 +0000