[isabelle-dev] code abbreviation for mapping over a fixed range

[Florian Haftmann]

See now 9a51e4dfc5d9.

	Florian

Am 12.11.2015 um 10:58 schrieb Jose Divasón:
> Hi Bertram, Christian and Bertram,
> 
> 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.
> 
> 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.
>  
> Best,
> Jose
> 
> 2015-11-12 10:09 GMT+01:00 Florian Haftmann
> <florian.haftmann at informatik.tu-muenchen.de
> <mailto:florian.haftmann at informatik.tu-muenchen.de>>:
> 
>     > The new definition actually causes *more* allocation than the original
>     > one, except for very short lists, because every call of @ copies its
>     > first argument. Note that the code equation for [_..<_] is
>     >
>     >   lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
>     >
>     > which has no calls to @ at all; a corresponding code equation for
>     > a fused "map_upt f i j = map f [i..<j]" would be
>     >
>     >   "map_upt f i j = if i < j then f i # map_upt f (Suc i) j else []"
>     >
>     > which could be used to define map_range:
>     >
>     >   "map_range f n = map_upt f 0 n"
> 
>     OK, I'll revert this.
> 
>     Thanks for having an eye on that.
> 
>             Florian
> 
>     --
> 
>     PGP available:
>     http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> 
>     _______________________________________________
>     isabelle-dev mailing list
>     isabelle-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
>     https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151115/16805d9a/attachment.sig>