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

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

> > 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
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151112/4693684f/attachment-0002.html>