Email Gateway (Aug 19 2022 at 11:39): Email Gateway (Aug 19 2022 at 11:39):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
maybe this was discussed already (I could not find such a discussion
though). What is the reason for not having List.span in List.thy? For
code generation it might be nice to have a setup like
fun span :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list × 'a list" where
"span P (x # xs) =
(if P x then let (ys, zs) = span P xs in (x # ys, zs)
else ([], x # xs))" |
"span _ [] = ([], [])"
lemma span_takeWhile_dropWhile [simp]:
"span P xs = (takeWhile P xs, dropWhile P xs)"
by (induct xs) simp_all
declare span.simps [simp del]
(see also the attached Span.thy) in the "standard library"?
cheers
chris
Span.thy
Email Gateway (Aug 19 2022 at 11:39):From: Tobias Nipkow <nipkow@in.tum.de>
Am 13/08/2013 08:51, schrieb Christian Sternagel:
Dear all,
maybe this was discussed already (I could not find such a discussion though).
What is the reason for not having List.span in List.thy?
I didn't even know about it but see that it is part of the Haskell prelude.
For code generation it
might be nice to have a setup likefun span :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list × 'a list" where
"span P (x # xs) =
(if P x then let (ys, zs) = span P xs in (x # ys, zs)
else ([], x # xs))" |
"span _ [] = ([], [])"lemma span_takeWhile_dropWhile [simp]:
"span P xs = (takeWhile P xs, dropWhile P xs)"
by (induct xs) simp_alldeclare span.simps [simp del]
It should be the other way around: the lemma should be the definition and the
two fun-equations should be code lemmas.
Are you sure it is worth adding it? The only reason is that if you know about
span, you get more efficient code. But is is really more efficient? You only
traverse the list once, but there is a chance (depending on the compiler) that
you create as many intermediate pairs as there are list elements. But if
somebody feels strongly about it, I'm happy to add it.
Tobias
(see also the attached Span.thy) in the "standard library"?
cheers
chris
Email Gateway (Aug 19 2022 at 11:39):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Tobias,
On 08/14/2013 04:08 PM, Tobias Nipkow wrote:
Am 13/08/2013 08:51, schrieb Christian Sternagel:
fun span :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list × 'a list" where
"span P (x # xs) =
(if P x then let (ys, zs) = span P xs in (x # ys, zs)
else ([], x # xs))" |
"span _ [] = ([], [])"lemma span_takeWhile_dropWhile [simp]:
"span P xs = (takeWhile P xs, dropWhile P xs)"
by (induct xs) simp_alldeclare span.simps [simp del]
It should be the other way around: the lemma should be the definition and the
two fun-equations should be code lemmas.
Okay.
Are you sure it is worth adding it? The only reason is that if you know about
span, you get more efficient code. But is is really more efficient? You only
traverse the list once, but there is a chance (depending on the compiler) that
you create as many intermediate pairs as there are list elements. But if
somebody feels strongly about it, I'm happy to add it.
No I'm not sure. I'm just guessing that since GHC uses this definition
of "span", it does make sense at least for Haskell (but of course you
are right about it not making a big difference for efficiency).
Moreover, I have no strong opinion about adding "span" (I just stumbled
across it, since we reinvented a specialized variant of "span" for
"string"s in IsaFoR and I recalled "span" from the Haskell Prelude).
It is also thinkable to set up the code generator such that
"(takeWhile P xs, dropWhile P xs)" is replaced by "span" (for Haskell)
then the user does not have to know about it.
One (tiny) pro is that "span P xs" is shorter to type than "(takeWhile P
xs, dropWhile P xs)". I'm not sure how often this pattern occurs in
actual formalizations though.
cheers
chris
Email Gateway (Aug 19 2022 at 11:39):From: Makarius <makarius@sketis.net>
Isabelle/HOL is Isabelle/ML, but in the latter we have the following
operations:
val take: int -> 'a list -> 'a list
val drop: int -> 'a list -> 'a list
val chop: int -> 'a list -> 'a list * 'a list
In that terminology the above would be take_while, drop_while, and
chop_while (instead of "span").
The chop operation was introduced in addition to the older take / drop to
support canonical argument order in ML, i.e. to optimize clarity and
readability of the sources in certain situations. (If abused this leads
to agglomerates of pointless combinators.)
There was never a consideration to "optimize" runtime to avoid a second
walk through the list or intermediate tupling. Such low-level accounting
has hardly any impact on complex applications running on complex hardware
(with lots of caches, cores etc.).
Makarius
Last updated: May 06 2024 at 08:19 UTC