|
Deriving
class
instances
for
datatypes
Title: |
Deriving class instances for datatypes |
Authors:
|
Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and
René Thiemann
|
Submission date: |
2015-03-11 |
Abstract: |
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 hash-functions which are required in the
Isabelle Collection Framework and the Container Framework.
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 project.
With our new tactics we could remove
several tedious proofs for (conditional) linear orders, and conditional equality operators
within IsaFoR and the Container Framework. |
BibTeX: |
@article{Deriving-AFP,
author = {Christian Sternagel and René Thiemann},
title = {Deriving class instances for datatypes},
journal = {Archive of Formal Proofs},
month = mar,
year = 2015,
note = {\url{http://isa-afp.org/entries/Deriving.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Collections, Native_Word |
Used by: |
Affine_Arithmetic, CAVA_Automata, Containers, Datatype_Order_Generator, Formula_Derivatives, MSO_Regex_Equivalence, Ordinary_Differential_Equations, Real_Impl, Show |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|