<div dir="ltr"><div><div><div><div>Hi Bertram, Christian and Bertram,<br></div><div><br>I would like to put my two cents in this topic. I
 have done a simple experiment about this using my AFP entry about the 
QR decomposition, where a strong use of map_range is done.<br></div><br></div>With
 the current map_range definition, the computation of the QR 
decomposition of a 60x60 real matrix takes about 45 seconds. However, if
 one adds the definition proposed by Bertram then the same computation takes about 2.43 seconds. So it really seems to be so much faster. <br> <br></div>Best,<br></div>Jose<br></div><div class="gmail_extra"><br><div class="gmail_quote">2015-11-12 10:09 GMT+01:00 Florian Haftmann <span dir="ltr"><<a href="mailto:florian.haftmann@informatik.tu-muenchen.de" target="_blank">florian.haftmann@informatik.tu-muenchen.de</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">> The new definition actually causes *more* allocation than the original<br>
> one, except for very short lists, because every call of @ copies its<br>
> first argument. Note that the code equation for [_..<_] is<br>
><br>
>   lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"<br>
><br>
> which has no calls to @ at all; a corresponding code equation for<br>
> a fused "map_upt f i j = map f [i..<j]" would be<br>
><br>
>   "map_upt f i j = if i < j then f i # map_upt f (Suc i) j else []"<br>
><br>
> which could be used to define map_range:<br>
><br>
>   "map_range f n = map_upt f 0 n"<br>
<br>
</span>OK, I'll revert this.<br>
<br>
Thanks for having an eye on that.<br>
<span class="HOEnZb"><font color="#888888"><br>
        Florian<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
--<br>
<br>
PGP available:<br>
<a href="http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de" rel="noreferrer" target="_blank">http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de</a><br>
<br>
</div></div><br>_______________________________________________<br>
isabelle-dev mailing list<br>
<a href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a><br>
<a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" rel="noreferrer" target="_blank">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br>
<br></blockquote></div><br></div>