Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation for sets of sets

Email Gateway (Aug 18 2022 at 17:21):

From: Martin STRECKER <strecker@irit.fr>
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
SetOfSet.thy

Email Gateway (Aug 18 2022 at 17:21):

From: Lukas Bulwahn <bulwahn@in.tum.de>
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

Last updated: Apr 16 2024 at 12:28 UTC