Knit&Frog: Pattern matching compilation for custom memory representations (doctoral session)

Autor: Baudon, Thaïs, Radanne, Gabriel, Gonnord, Laure
Přispěvatelé: Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Compilation et Analyse, Logiciel et Matériel (CASH), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Lyon, Institut National de Recherche en Informatique et en Automatique (Inria), École normale supérieure de Lyon (ENS de Lyon), Laboratoire de Conception et d'Intégration des Systèmes (LCIS), Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Université Grenoble Alpes (UGA), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)
Jazyk: angličtina
Rok vydání: 2022
Předmět:
Zdroj: AFADL 2022-21ème journées Approches Formelles dans l'Assistance au Développement de Logiciels
AFADL 2022-21ème journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2022, Vannes, France
Popis: National audience; Initially present only in functional languages such as OCaml and Haskell, Algebraic Data Types have now become pervasive in mainstream languages, providing nice data abstractions and an elegant way to express functions though pattern-matching. Numerous approaches have been designed to compile rich pattern matching to cleverly designed, efficient decision trees. However, these approaches are specific to a choice of internal memory representation which must accommodate garbage-collection and polymorphism. ADTs now appear in languages more liberal in their memory representation such as Rust. Notably, Rust is now introducing more and more optimizations of the memory layout of Algebraic Data Types. As memory representation and compilation are interdependent, it raises the question of pattern matching compilation in the presence of non-regular, potentially customized, memory layouts. In this article, we present Knit&Frog, a framework to compile pattern-matching for monomorphic ADTs, parametrized by an arbitrary memory representation. We propose a novel way to describe choices of memory representation along with a validity condition under which we prove the correctness of our compilation scheme. The approach is implemented in a prototype tool ribbit.
Databáze: OpenAIRE