[isabelle-dev] code abbreviation for mapping over a fixed range
bertram.felgenhauer at googlemail.com
Sat Nov 7 14:55:58 CET 2015
> > 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..<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"
More information about the isabelle-dev