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

Hi Christian,

yes, it can. I wrote some pre- and postprocessing to make the Transfer.transferred work better with maps (theory attached, works with 2013-1-RC3 and Containers in AFP/devel). There's a small example. Can you check whether that works for you in general? If so, it might be a good idea to add this to Containers or even HOL/Library.


On 24/10/13 15:43, Christian Sternagel wrote:
Dear all,

Thanks for the useful answers. For my concrete case: does "lift_definition" also work for
recursive functions (whith "match_list" is). With my first attempt using "lift_definition"
I just got a "wrapper" around the recursive function that changed the type, which doesn't
solve the efficiency problem.



On 10/24/2013 06:59 PM, Ondřej Kunčar wrote:
Hi Christian,
Peter has already explained the situation in general. I just want to add
that Lifting/Transfer can indeed help you a bit in moving your
specification from 'a => 'b option to ('a, 'b) mapping. Please see
Chapter 4 in our ITP 2013 paper: Data Refinement in Isabelle/HOL.


On 10/24/2013 11:35 AM, Peter Lammich wrote:
Hi Christian.

The problem is, that ('a,'b) map is just syntactic sugar for the type
'a => 'b option. The code-generator replacement of types by efficient
implementations only works for types represented by a single
type-constant (like ('a,'b) mapping or 'a set).

Moreover, note that, in general, you do not want to translate all
occurences of "'a -> 'b option" by a map implementation, as there are
also functions that return option-values, which are intended to be
translated as functions.

The automatic refinement framework [1] tries to tackle this problem,
however, it has to be employed manually before code generation, and
usually requires some setup overhead.

In order to use Containers, I believe that you should transform your
functions to use mapping. Maybe the transfer+lifting package of Brian
and Ondra may help you to automate this task.


[1]: Peter Lammich, Automatic Data Refinement, Proc. of ITP 2013

On Do, 2013-10-24 at 18:10 +0900, 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

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!



Attachment: Map_To_Mapping.thy
Description: application/extension-thy

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