# [isabelle] Code generation for sets of sets

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] Code generation for sets of sets
*From*: Martin STRECKER <strecker at irit.fr>
*Date*: Wed, 09 Mar 2011 16:40:19 +0100
*User-agent*: Mozilla/5.0 (X11; U; Linux i686 (x86_64); en-US; rv:1.9.2.9) Gecko/20100915 Thunderbird/3.1.4

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?
`

`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".
`
Thanks for your suggestions,
Martin

theory SetOfSet imports "~~/src/HOL/Library/Executable_Set"
begin
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))"
(* missing in Executable_Set *)
setup {*
Code.add_signature_cmd ("exTimes", "'a set \<Rightarrow> 'b set \<Rightarrow> ('a * 'b) set")
*}
setup {*
Code.add_signature_cmd ("inter_partition", "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set")
*}
export_code inter_partition in OCaml module_name SetOfSet file "set_of_set.ml"
end

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