*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping*From*: Peter Lammich <lammich at in.tum.de>*Date*: Thu, 24 Oct 2013 11:35:13 +0200*In-reply-to*: <5268E404.9050304@gmail.com>*References*: <5268E404.9050304@gmail.com>

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

**Follow-Ups**:**Re: [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:*Ondřej Kunčar

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

- Previous by Date: [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: [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