Storable types: free, absorbing, custom
Résumé
The Store library (Noûs and Scherer, 2023; Allain, Clément, Moine, and Scherer, 2024) provides a store data structure that tracks a bag of mutable references, and provides an efficient way to capture its current state and restore it later on. This is useful to implement backtracking algorithms over mutable state, as found in type-checkers and automated theorem provers.
We extend the Store library to store not only mutable references, but also richer data structures such as dynamic arrays and hash tables. Instead of hardcoding specific data structures within Store, we capture broad classes of storable data structures through generic interfaces. These interfaces are determined by the properties of the (anti)operations of each data structure. We describe three interesting classes of operations -absorbing, free, and custom (the general case) -and the corresponding APIs and implementations.
Domaines
Informatique [cs]Origine | Fichiers produits par l'(les) auteur(s) |
---|