# 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.*