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>: > > 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 > 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
