# Re: [isabelle] What Isabelle maps to use to generate usual (ordered) maps

Hi Thomas,


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?



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.