[isabelle] Code generation for sets of sets



 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.