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

2015-11-15 Thread 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
>  >:
> 
> > 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..
> > which has no calls to @ at all; a corresponding code equation for
> > a fused "map_upt f i j = map f [i.. >
> >   "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
> 

-- 

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


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

2015-11-12 Thread 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>:

> > 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..
> > which has no calls to @ at all; a corresponding code equation for
> > a fused "map_upt f i j = map f [i.. >
> >   "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


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

2015-11-07 Thread Bertram Felgenhauer
Hi Florian,
> > This email refers to the following commit:
> > 
> >   http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251
> > 
> >   code abbreviation for mapping over a fixed range
> > 
> > Is there a specific reason for this code equation:
> > 
> >   "map_range f (Suc n) = map_range f n @ [f n]"
> > 
> > It seems rather inefficient. Anyway, what's the purpose of "map_range".
> 
> the idea of map_range is to avoid building a list first and then mapping it.

Please don't forget about this.

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

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

2015-10-29 Thread Florian Haftmann
Hi Christian,

> This email refers to the following commit:
> 
>   http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251
> 
>   code abbreviation for mapping over a fixed range
> 
> Is there a specific reason for this code equation:
> 
>   "map_range f (Suc n) = map_range f n @ [f n]"
> 
> It seems rather inefficient. Anyway, what's the purpose of "map_range".

the idea of map_range is to avoid building a list first and then mapping it.

Maybe this was though too short.  That changeset fell out of another
work and I just took it into the history without too much thinking about
it again.  Before reverting that (or replacing it by something better),
some concrete measurements could be helpful, though.

Cheers,
Florian

> 
> cheers
> 
> chris
> 
> PS: I was confused about [code_abbrev], thus looked it up in isar-ref,
> then was further confused :D
> 
>   "code_abbrev" declares (or with option “del” removes) equations which
> are applied as rewrite rules to any result of an evaluation and
> symmetrically during preprocessing to any code equation or
> evaluation input.
> 
> In my opinion the usage of the word "symmetrically" could be clarified.
> Does it mean "similar to the previous use case" or "symmetric in the
> sense of reading the equation from right to left"?
> 
> 

-- 

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


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

2015-10-19 Thread Christian Sternagel
This email refers to the following commit:

  http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251

  code abbreviation for mapping over a fixed range

Is there a specific reason for this code equation:

  "map_range f (Suc n) = map_range f n @ [f n]"

It seems rather inefficient. Anyway, what's the purpose of "map_range".

cheers

chris

PS: I was confused about [code_abbrev], thus looked it up in isar-ref,
then was further confused :D

  "code_abbrev" declares (or with option “del” removes) equations which
are applied as rewrite rules to any result of an evaluation and
symmetrically during preprocessing to any code equation or
evaluation input.

In my opinion the usage of the word "symmetrically" could be clarified.
Does it mean "similar to the previous use case" or "symmetric in the
sense of reading the equation from right to left"?




signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev