Re: [isabelle] What Isabelle maps to use to generate usual (ordered) maps
I am wondering what is the map theory that I have to use in order to
usual ML maps: roughly trees ordered w.r.t. to keys?
This is still somewhat in flux, and there is no single best practice.
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
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...
This archive was generated by a fusion of
Pipermail (Mailman edition) and