Refactoring functional programs with ornaments

Refactorisation de programmes fonctionnels par les ornements Les ornements fournissent un moyen de définir des transformations de définitions de types de données inductifs réorganisant, spécialisant et ajoutant des champs à des types de données déjà existants. À partir d’une telle transformation, nous nous intéressons à la refactorisation semi-automatique d’un code déjà existant, écrit en ML et opérant sur le type de base pour le faire opérer sur le type ornementé. Nous décrivons un cadre pour de telles transformations, basé sur deux phases: tout d’abord, le terme de base est généralisé au maximum en ajoutant des abstractions sur les détails des types de données utilisés. Le terme est ensuite spécialisé pour opérer uniquement sur le type ornementé. Nous décrivons un langage intermédiaire fournissant les abstractions nécessaires pour présenter le terme générique, et garantissant qu’il est possible de simplifier le terme spécialisé pour ne présenter à l’utilisateur que des termes du langage de base. Le langage intermédiaire permet notamment d’exprimer des abstractions dépendantes, de représenter les égalités apprises par le filtrage de motifs, et fournit une construction permettant de se référer de façon opaque au résultats de calculs déjà effectués. Nous exploitons la paramétricité du terme généralisé pour prouver une relation de cohérence entre le terme de base et le terme ornementé, garantissant la correction de la refactorisation. Nous présentons une implémentation de cette transformation sur un langage ML noyau, et justifions de son utilité dans de nombreux cas courants de transformation de programme: refactorisation pure, ajout de nouvelles données et spécialisation. Nous présentons aussi une nouvelle technique de dépliage permise par notre transformation qui autorise à changer la structure récursive des fonctions, et illustrons son utilité pour optimiser certaines représentations de données et pour la programmation générique.