[Agda] Colist -> List

[Andreas Abel]

Here is a snippet from Prelude.agda (F. Kettelhoit) that uses the dirty 
trick of cutting a line at some arbitrary maximal length.  This is 
related to the problem of converting a Colist to a List.

-- we need the maxLineLength to make sure the lines function terminates
-- not exactly perfect, but works
maxLineLength = 100000

lines : Costring -> Colist String
lines xs = lines' maxLineLength xs []
   -- uses an accumulator s,  initially empty ([])
   where lines' : ℕ → Costring -> List Char -> Colist String
         lines' zero    xs          s = fromList (reverse s) ∷ ♯ lines' 
maxLineLength xs []
         lines' (suc n) ('\n' ∷ xs) s = fromList (reverse s) ∷ ♯ lines' 
maxLineLength (♭ xs) []
         lines' (suc n) (x ∷ xs)    s = lines' n (♭ xs) (x ∷ s)
         lines' (suc n) []          s = fromList (reverse s) ∷ ♯ []

readLines : String → ∞ (IO (Colist String))
readLines f = ♯ ((♯ readFile f) ∞>>= (\ x → ♯ (∞return $ lines x)))


On 02.10.12 4:00 PM, Daniel Peebles wrote:
> 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
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/