Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] What Isabelle maps to use to generate usual (o...

view this post on Zulip Email Gateway (Aug 18 2022 at 18:00):

From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear Isabelle users,

I am wondering what is the map theory that I have to use in order to
generate
usual ML maps: roughly trees ordered w.r.t. to keys?

By the way, I want to generate Scala code.

Thanks in advance,

Thomas

view this post on Zulip Email Gateway (Aug 18 2022 at 18:00):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi Thomas,

in our developments we are using Isabelle's red-black trees for that
purpose (HOL/Library/RBT.thy). We do also generate code (Haskell, SML,
and Scala) and it works.

cheers

chris

view this post on Zulip Email Gateway (Aug 18 2022 at 18:01):

From: Alexander Krauss <krauss@in.tum.de>
Hi Thomas,

This is still somewhat in flux, and there is no single best practice.
You could

a) Use the red-black trees from HOL/Library/RBT.thy directly.

b) Use the mapping type defined in HOL/Library/Mapping. This is slightly
more abstract, basically a copy of "'a => 'b option". In Isabelle2011,
when you load RBT.thy, the code generator automatically uses red-black
trees to implement mappings.

c) Use the Isabelle Collections Framework. See the ITP-10 paper by Peter
Lammich and Andreas Lochbihler
(http://cs.uni-muenster.de/sev/staff/lammich/pub/itp10.pdf).

d) In the future, we hope that it will be possible to generate code from
abstract types like "'a => 'b option" or "'a set" directly. But we're
not quite there yet...

Hope this helps...
Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 18:01):

From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear Alex and Christian,

Thanks a lot for your answers...
I think I'll go for Mapping (with RBT for the code export) for the moment.

Thanks a lot.

Best regards,

Thomas

Last updated: Apr 25 2024 at 20:15 UTC