# Re: [isabelle] Code generation for sets of sets

```On 03/09/2011 04:40 PM, Martin STRECKER wrote:
```
``` Dear all,

```
I have a problem with code generation using Executable_Set.thy for sets of sets. Take the following definition (also see attached file):
```
definition
```
inter_partition :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where "inter_partition P Q = ((\<lambda> (a,b). a \<inter> b) ` (P \<times> Q))"
```
The generated Ocaml code does not typecheck:

let rec inter_partition (_A1, _A2)  p q =
```
image (equal_fun _A1 equal_bool) (fun (a, b) -> inter _A2 a b) (exTimes p q);;
```
```
The problem is the equality function: whereas on the level of Isabelle, 'a set and 'a => bool are synonymous, they are not so on the level of the generated Ocaml code, where the code generator has introduced a datatype 'a set which is not compatible with 'a => bool. Therefore, the equality function should not be (equal_fun _A1 equal_bool), but something like (equal_set _A1). Any idea how to tweak the code generator into doing that?
```
```
These are the known deficiencies of the adhoc translations by Executable_Set.
```A sound solution is provided by Cset.
```
If Executable_Set.thy is considered legacy: which other code generation to use for sets? The disadvantage of Cset.thy, for example, is that it uses a functional representation which is not "printable".
```
```
Nesting CSet.set in CSet.set should be possible and should allow to generate code. But the basic definitions in the CSet theory is still incomplete compared to the Set theory.
```
```
Actually, we envisage a mechanism to transport definitions from Isabelle's set to the special-purpose type CSet.set for code generation.
```
Values of type ('a CSet.set) CSet.set should be "printable".

Hope this helps.

Lukas

```
```Thanks for your suggestions,

Martin

```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.