Re: [isabelle] Code generation for sets of sets
On 03/09/2011 04:40 PM, Martin STRECKER wrote:
These are the known deficiencies of the adhoc translations by
I have a problem with code generation using Executable_Set.thy for
sets of sets. Take the following definition (also see attached file):
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
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?
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
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.
Thanks for your suggestions,
This archive was generated by a fusion of
Pipermail (Mailman edition) and