[Agda] Colist -> List

[Daniel Peebles]

Unfortunately there is no complete way to convert from a Colist to a List,
because a Colist is potentially infinite and you can't detect whether it is
beforehand. The best you can do is decide on a "maximum depth" (a natural)
and recurse over that to construct a list of at most that length. That's
what the BoundedVec in your code is supposed to do. Your problem is that
you imported the wrong one. You need to import Data.BoundedVec.Inefficient,
which is the one that Colist.take uses. The one you imported is just an
abstract interface.

Hope this helps!
Dan

On Tue, Oct 2, 2012 at 9:20 AM, Serge D. Mechveliani <mechvel at botik.ru>wrote:

> Please, how to convert  Colist Char  to  List Char  ?
>
> I need to read a  List Char  from a file.
> readFile  returns  IO Costring              -- (Costring = Colist Char).
> The program can extract  coStr : Colist Char  from this input.
> But how to obtain  List Char ?
> I try
>   Colist.take :
>          forall {a} {A : Set a} (n : Nat) -> Colist A -> BoundedVec A n
> :
>   module Main where
>   open import Data.Colist as Colist
>   open import Data.BoundedVec as BnVec
>   ...
>   f : Costring -> BoundedVec Char 2
>   f coStr = Colist.take 2 coStr
>
> And  Agda-2.3.0.1 + MAlonzo + lib-0.6  reports
>
>   .Data.BoundedVec.Inefficient.BoundedVec Char 2  !=<
>   BoundedVec Char 2  of type  Set
>   when checking that the expression  Colist.take 2 coStr  has type
>   BoundedVec Char 2
>
> Just the same types of     BoundedVec Char 2
> are reported as different.
> Can you explain this?
>
> Thanks,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121002/b4b5aae3/attachment.html