[isabelle] Custom serialization with polymorphic types · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Custom serialization with polymorphic types

Email Gateway (Aug 19 2022 at 11:48):

From: Sarah Winkler <sarah.winkler@uibk.ac.at>
Dear experts on code generation,

I would like to export code to OCaml, using custom serialization to
adapt to an already present type.
However, my function have parameters of some polymorphic types, and I
want to map instances of these types to non-polymorphic target types.
In an example:
I have in OCaml
type otree = ONode of otree * otree | OLeaf of int
and in Isabelle:

datatype 'a "tree" = Node "'a tree" "'a tree" | Leaf 'a

fun tsize :: "'a tree \<Rightarrow> nat" where
"tsize (Leaf a) = Suc 0"
| "tsize (Node l r) = Suc (tsize l) + (tsize r)"

Currently I use an extra data type and a transformation to export my
function to OCaml:
datatype int_tree = INode int_tree int_tree | ILeaf int

fun to_tree :: "int_tree \<Rightarrow> int tree" where
"to_tree (ILeaf i) = Leaf i"
| "to_tree (INode l r) = Node (to_tree l) (to_tree r)"

definition int_size :: "int_tree \<Rightarrow> nat" where "int_size t
\<equiv> tsize (to_tree t)"

code_printing
code_module "Trees" ⇀ (OCaml) {* type otree = ONode of otree * otree |
OLeaf of int *}
| type_constructor "int_tree" ⇀ (OCaml) "otree"
| constant ILeaf ⇀ (OCaml) "OLeaf"
| constant INode ⇀ (OCaml) "ONode"

export_code tsize in OCaml

Is there any more elegant way to achieve such a custom serialization,
causing less "overhead code" in OCaml?

Many thanks in advance,
Sarah

Email Gateway (Aug 19 2022 at 11:48):

From: Sarah Winkler <sarah.winkler@uibk.ac.at>
Dear experts on code generation,

datatype 'a "tree" = Node "'a tree" "'a tree" | Leaf 'a

fun tsize :: "'a tree \<Rightarrow> nat" where
"tsize (Leaf a) = Suc 0"
| "tsize (Node l r) = Suc (tsize l) + (tsize r)"

Currently I use an extra data type and a transformation to export my
function to OCaml:
datatype int_tree = INode int_tree int_tree | ILeaf int

fun to_tree :: "int_tree \<Rightarrow> int tree" where
"to_tree (ILeaf i) = Leaf i"
| "to_tree (INode l r) = Node (to_tree l) (to_tree r)"

definition int_size :: "int_tree \<Rightarrow> nat" where "int_size t
\<equiv> tsize (to_tree t)"

export_code tsize in OCaml

Is there any more elegant way to achieve such a custom serialization,
causing less "overhead code" in OCaml?

Many thanks in advance,
Sarah

Email Gateway (Aug 19 2022 at 11:48):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Sarah,

I am not completele sure that I fully understand your setting. In any case, you have
already gone the canoncial way of doing this:

Introduce a type copy that specialises the parameters as needed.
Transfer all functions and theorems to the new type.
Adapt the code generator for the new type.

The packages lifting and transfer greatly help in the second step , they are described in
[1]. There are also many more tricks how to simplify the transfer.

I do not know what you mean by "overhead code" in OCaml. Normally, you should not get code
for the operations on "'a leaf" at all, unless you use then for other types than int. In
your example, you should export int_size rather than tsize and provide code equations for
int_size:

lemma [code]:
"int_size ILeaf = 0"
"int_size (INode l r) = Suc (int_size l + int_size r)"

There are further possibilities for special cases, but it is hard to tell from your
example whether they are promising directions. So, if the above does not work for you,
please provide more detail on what you are trying to achieve.

Hope this helps,
Andreas

[1] Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow. Data Refinement in
Isabelle/HOL. In ITP 2013, LNCS, 2013.

Email Gateway (Aug 19 2022 at 11:49):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Sarah,

Indeed. At might seem ridiculous at first sight to introduce type
copies, but this maintains the one-to-one correspondence between types
in HOL and types in generated code, which is particularly important when
type classes are involved.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 11:49):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Sarah,

It would be preferrable to get no code for operations on the abstract type ('a leaf).
Then just delete the code equations for the constants on the abstract type. The following
is the most reliable method to delete all code equations of a constant, say tsize:

lemma [code, code del]: "tsize = tsize" ..

However, I am a bit reluctant to copy all the theory for the abstract level (a lot of
stuff) to the concrete types - but I guess the lifting/transfer packages ease that task.
From a first glance I am afraid to not fully understand how they work, but I'll check in
more detail (and possibly annoy the mailing list with further questions at a later point).
My latest AFP entry Native Words [2] does something very similar, it maps bit operations
on integers and words of different sizes to target language integers and machine words.
There, I also have to instantiate type parameters in the type copies. Maybe you want to
have a look at it, as it shows how to do all this with lifting/transfer. There's also a
userguide that explains how to best use lifting/transfer once everything has been set up.

Best,
Andreas

[2] That entry is currently only available in the repository of the development AFP at
http://sourceforge.net/p/afp/code/ci/9f81b36d43b30aa09f79b17dfb9cb24d2f4802c9/
It has not yet made it onto the AFP devel website.

Thanks for your help!
Sarah

lemma [code]:
"int_size ILeaf = 0"
"int_size (INode l r) = Suc (int_size l + int_size r)"

There are further possibilities for special cases, but it is hard to tell from your
example whether they are promising directions. So, if the above does not work for you,
please provide more detail on what you are trying to achieve.

Hope this helps,
Andreas

[1] Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow. Data Refinement in
Isabelle/HOL. In ITP 2013, LNCS, 2013.

On 17/09/13 12:27, Sarah Winkler wrote:

Dear experts on code generation,

I would like to export code to OCaml, using custom serialization to adapt to an already
present type.
However, my function have parameters of some polymorphic types, and I want to map
instances of these types to non-polymorphic target types.
In an example:
I have in OCaml
type otree = ONode of otree * otree | OLeaf of int
and in Isabelle:

datatype 'a "tree" = Node "'a tree" "'a tree" | Leaf 'a

fun tsize :: "'a tree \<Rightarrow> nat" where
"tsize (Leaf a) = Suc 0"
| "tsize (Node l r) = Suc (tsize l) + (tsize r)"

Currently I use an extra data type and a transformation to export my function to OCaml:
datatype int_tree = INode int_tree int_tree | ILeaf int

fun to_tree :: "int_tree \<Rightarrow> int tree" where
"to_tree (ILeaf i) = Leaf i"
| "to_tree (INode l r) = Node (to_tree l) (to_tree r)"

definition int_size :: "int_tree \<Rightarrow> nat" where "int_size t \<equiv> tsize
(to_tree t)"

code_printing
code_module "Trees" ⇀ (OCaml) {* type otree = ONode of otree * otree | OLeaf of int *}
| type_constructor "int_tree" ⇀ (OCaml) "otree"
| constant ILeaf ⇀ (OCaml) "OLeaf"
| constant INode ⇀ (OCaml) "ONode"

export_code tsize in OCaml

Is there any more elegant way to achieve such a custom serialization, causing less
"overhead code" in OCaml?

Many thanks in advance,
Sarah

Email Gateway (Aug 19 2022 at 11:49):

From: Sarah Winkler <sarah.winkler@uibk.ac.at>
Dear Andreas and Florian,

thanks for confirming the general approach, and the hints to the paper
and the Native Words theory! I think that gave me a good enough idea on
the direction to pursue, and interesting references to points for
improvement.

Best regards,
Sarah

Last updated: Apr 16 2024 at 16:19 UTC