Deriving class instances for datatypes

3 years 8 months ago
Deriving class instances for datatypes
We provide a framework for registering automatic methods to derive class instances of datatypes, as it is possible using Haskell’s “deriving Ord, Show, . . . ” feature. We further implemented such automatic methods to derive comparators, linear orders, parametrizable equality functions, and hashfunctions which are required in the Isabelle Collection Framework [1] and the Container Framework [2]. Moreover, for the tactic of Blanchette to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework. All of the generators are based on the infrastructure that is provided by the BNF-based datatype package. Our formalization was performed as part of the IsaFoR/CeTA project1 [3]. With our new tactics we could remove several tedious proofs for (conditional) linear orders, and conditional equality operators within IsaFoR and the Container Framework. Contents 1 Derive Manager 3 2 Shared Utilities for all Generator 3 3 Comparisons 4 3....
Christian Sternagel, René Thiemann
Added 13 Apr 2016
Updated 13 Apr 2016
Type Journal
Year 2015
Where AFP
Authors Christian Sternagel, René Thiemann
Comments (0)