Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping



Hi Christian,

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).

Best,
Andreas

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

   match_list ::
     (('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!

cheers

chris





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