*To*: Christian Sternagel <c.sternagel at gmail.com>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 24 Oct 2013 16:06:24 +0200*In-reply-to*: <5269241A.1080902@gmail.com>*References*: <5268E404.9050304@gmail.com> <1382607313.2510.16.camel@lapbroy33> <5268EF80.6040002@in.tum.de> <5269241A.1080902@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hi Christian,

Best, Andreas 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. cheers chris 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. Best, Ondrej 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. 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

**Attachment:
Map_To_Mapping.thy**

**References**:**[isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping***From:*Christian Sternagel

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

**Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping***From:*Ondřej Kunčar

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

- Previous by Date: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Next by Date: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Previous by Thread: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Next by Thread: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list