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.haftm...@informatik.tu-muenchen.de > <mailto:florian.haftm...@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-...@in.tum.de <mailto:isabelle-...@in.tum.de> > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev