Re: [isabelle] List.span



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_all

   declare 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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.