*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping*From*: Dmitriy Traytel <traytel at in.tum.de>*Date*: Mon, 28 Oct 2013 11:48:15 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <526E15E3.7040107@inf.ethz.ch>*References*: <5268E404.9050304@gmail.com> <5268EEED.1030502@inf.ethz.ch> <526AC0F8.5080705@informatik.tu-muenchen.de> <526E15E3.7040107@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

declare [[coercion_enabled]] declare [[coercion Mapping.Mapping]] term "f = Mapping.lookup f" term "Mapping.lookup f = f" So even more care is required than in the complete fragment.

Dmitriy Am 28.10.2013 08:44, schrieb Andreas Lochbihler:

Hi Florian,I haven't investigated in detail what exactly is missing. Whenever Iused mapping, I had code generation in mind, so my thinking might be abit biased. What I particularly like about 'a => 'b option is noclutter: I can build new maps just from lambda abstraction and theother usual HOL constants (if/case/Some/Option.map/Option.bind/...),there's no need for coercing between ('a, 'b) mapping and 'a => 'boption. Therefore, I don't have to worry where coercions areautomatically inserted. Nor do I care about what the simplifer does tothese coercions when. (By the way, if I enable automatic coercions,the error messages for ill-typed terms sometimes do not help toidentify what's wrong at all, in particular if I got the number ofparameters of a function wrong.) Of course, these maps are not(efficiently) executable, but I usually don't care in such situations:I just use them inside proofs, e.g., as a witness to an existentialquantifier. In proofs, I use such maps as arguments to functions forwhich I later generate code -- although not for these parameters.There are certainly functions, lemmas and automation missing. When Ilast looked at Mapping (which is already quite some time ago), I hadthe impression that everything is still centered around codegeneration, but inside a proof, I usually don't care about codegeneration, I just want to quickly get the proof done. Although I mustsay that I know one case where automation for ('a, 'b) mapping can inprinciple be better than for 'a => 'b option: Element lookup is justfunction application and the simplifier does not do well for equationof the form "g (f x) = ..." where f is a free variable. With mapping,this corresponding equation "g (lookup f x) = ..." works much better.Andreas On 25/10/13 21:05, Florian Haftmann wrote:Hi Andreas,Therefore, you have to switch to some other type. There are twooptions: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.once there has been the rough idea to reformulate Map.thy using a dedicated type like in Mapping.thy. The user-visible difference would be that element lookups need a dedicated function lookup :: ('a, 'b) mapping => 'a => 'b option But this could be inserted implicitly by coercions also whenever a ('a, 'b) mapping it used in place of a function. I did not pursue this further, since my impression was that (unlike sets) the syntax in Map.thy is not so pervasively common, so specification requiring executable data structures can just be based on Mapping.thy. Considering your statement about »easy going« of proofs in Mapping.thy, maybe we have to rethink about it. Or is it just that lemmas / automation are missing? Florian

**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:*Andreas Lochbihler

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

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

- Previous by Date: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Next by Date: Re: [isabelle] Evaluation of record expressions
- Previous by Thread: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Next by Thread: [isabelle] Autocompletion in 2013-1
- 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