Email Gateway (Aug 18 2022 at 18:00): 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
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
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
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: Nov 21 2024 at 12:39 UTC