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.