The Coq mailing list

[Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>]

On Sun, Apr 26, 2009 at 07:06:59PM -0400, 
roconnor AT theorem.ca
 wrote:
> On Sun, 26 Apr 2009, Bruno Barras wrote:
> 
> >Hi,
> >Just 2 little remarks. Firstly, you don't have to go that far in the CPS 
> >transformation, by adding the continuation only to map' (and not in the 
> >stream' type). The most noticeable change w.r.t. Edsko's code is the type 
> >of map':
> >
> >Definition map' (A B : Set) (f : A -> B)      (rec : (A -> B) -> stream A 
> >-> stream B)
> >    (xs : stream' A) (C:Type) (K : stream' B -> C) : C :=
> >  match xs with
> >  | inl u => K (inl _ u)
> >  | inr (x, xs') => K (inr _ (f x, rec f xs'))
> >  end.
> >CoFixpoint map2 (A B : Set) (f : A -> B) (xs : stream A) : stream B :=
> >  map' f (@map2 A B) (fromStream xs) toStream.
> >
> >(I haven't checked the example, but if it fails to type-check, this can be 
> >fixed easily.)
> 
> I just checked and it works.  The key is that you put the continuation K 
> into each branch of the match statement.  Very clever.  I'll try to 
> remember this trick.

Thank you for both your replies! map' is in fact generated, so I have to
think now whether I can generate the CPS transform instead -- but that
should be doable. 

Thanks again!

Edsko