Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
The difference between 'a set and ('a, 'b) map is that set is a single type constructor of
its own, whereas map is just a type synonym for a compount type expression. Unfortunately,
the code generator supports only data refinement for single type constructors, on which
Containers relies. So there is no way to get this to work directly.
Therefore, you have to switch to some other type. There are two options:
1. Use ('a, 'b) mapping. I recommend that you only use it for code generation, the mapping
type in its current state is not suitable for proving lots of stuff. In my AFP entry
Native Word (in AFP-devel: http://afp.sourceforge.net/devel-entries/Native_Word.shtml),
the userguide describes how one can easily deal with such type copies thanks to
transfer/lifting. I will see whether I can make it work for mapping, too.
2. Peter Lammics's Autoref tool (also in AFP-devel:
http://afp.sourceforge.net/devel-entries/Automatic_Refinement.shtml) also provides some
automation to specialise maps to efficient data structures. Internally, it produces copies
of your functions that directly operate on the implementation type (like a RBT).
On 24/10/13 11:10, Christian Sternagel wrote:
Dear all (especially Andreas ;)),
is it possible to automatically get efficient code when code generating a function
involving the "('a, 'b) map" type (i.e., "'a => 'b option").
If I import AFP/Containers I can have this for "('a, 'b) mapping" (which is a type-copy of
"('a, 'b) map").
But in the actual formalization "('a, 'b) map" is more convenient to use since we have
nice syntax like "m x" for lookup and "m (x |-> t)" for update.
Since according to the user guide the above is possible w.r.t. "'a set", I was wondering
what the obstacle is for "('a, 'b) map" (or maybe I just misunderstood something).
More concretely, what is your advice for a function like
(('f, 'v) term * ('f, 'v) term) list =>
('v => ('f, 'v) term option) => ('f, 'v) subst
where "match_list E Map.empty" gives a matcher for all equations in "E". Would you change
this to use "('v, ('f, 'v) term) mapping" instead, or is there a way to get efficient code
as it is? Thanks in advance!
This archive was generated by a fusion of
Pipermail (Mailman edition) and