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



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.


Best,
  Peter

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