aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/haskell.ml
AgeCommit message (Collapse)Author
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-21considerations de pretty-printletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2558 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-15gros commit: principalement ajout des lambdas arity + leur optimisation en ↵letouzey
temps normal + beaucoup de simplifications diverses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2532 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-27modifs des preambules d'extraction modulaireletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2496 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-14qq inline manuels (sigS_rec ...) + utilisation de library_partletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2476 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12pretty printletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2469 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
2002-02-07un assert false de trop (MLexn peut avoir des args)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2458 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-06gros changement dans mlutil.ml: ajout d'une elimination globale des propletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2456 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21maj CHANGES extraction + bug extraction & _letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2359 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18typo de parenthèsage + suppression de string (= str maintenant)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2311 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 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-11-02suite des modifs concernant les optimisations diversletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2151 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-09-18travail sur le Extract Constantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1986 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Parsingherbelin
- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-14mise en place extraction haskellfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1751 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:03:46 +0000