Audience
- Romain Aissat
- Frédéric Boulanger
- Safouan Taha
- Frédéric Tuong
- Hai Nguyen Van
- Benoît Valiron
- Burkhart Wolff
- Lina Ye
Project
Yakoub
Code Generation for Abstract Types
Yakoub presents how to generate code for abstract datatypes in Isabelle. A primitive way to define abstract types in Isabelle is using typdefs. This is a well-known conservative extension scheme that generates the declaration of the (new) type and a few declarations of constant symbols and axioms establishing an isomorphism between the abstract type and elements of a set over a representing type. Usually, abstract type definitions are implemented under a given data invariant, i.e the predicate that characterizes the subset of the representing type. This idea is extended to z code generation method (i.e using Isabelle code generator) for abstract types by using operations on the representing type (leaving the invariants implicit).
In fact, to understand how we generate code for abstract types we will first explain the functional model of Isabelle code generator usually used to generate code from concrete types. At first place, the code generator of Isabelle takes as an input a code equations (i.e a rewriting rule), which have the following format, f x y = eval, where eval is an executable semantics for f, and translates them into intermediate programs through raw code equations (an abstraction of code equations). The serialiser will translate the intermediate program into function definitions in a given target language. The target languages are some functional programming languages such as SML, OCaml, Haskell and Scala. Via a foreign interface for datatypes and constant definitions, a user can customize the way that the serialiser prints the generated code (under the assumption that the serialiser covers the informations added during customization). Also, users can extend Isabelle code generator by building their own serialiser to a new target language (e.g A.D. Brucker did it for F#).
After this short definition related to Isabelle code generator, we will introduce now the idea behind abstract datatype refinement inside Isabelle. Suppose that f_a is a function for abstract type and f_c is its corresponding function for the concrete type, C is the concrete type and A is the abstract type, and Abs::C->A, which can be considered as constructor. After replacing the abstract type A by concrete type C, we have to check the property: f_a(Abs(c))=Abs(f_c(c)). However, if we cannot guarantee some invariant and if this property is only true under the condition that such an invariant is true, then this is not good for code generation. To solve this, one has to deal with invariants during code generation.
To preserve an invariant, in Isabelle, one can use lifting and transfer packages for implementation of a data structure. Precisely, some new constant is defined on an abstract level by lifting terms from the concrete to the abstract one and the transfer rules are proved that relate the concrete level and the new constant. Precisely, an abstract datatype with its constructor is defined and then each operation can be lifted by proving that the operation on the concrete level preserves the invariant. The corresponding code equation is also proved. Afterwards, one has to prove the properties of the new constant, which can be done by using the proved transfer rules. The idea is that all different abstract levels should finally be used to guarantee the code equations.