[Agda] Re: Colist -> List

[Karn Kallio]

Here is another sort of dirty hack (turn off termination checker) approach to 
the lines problem:

{- |
  Convert a value in the partiality monad into a possibly divergent
  computation in the IO monad.
-}

{-# OPTIONS --no-termination-check #-}

module Divergence where

open import Category.Monad.Partiality
open import Coinduction
open import IO

abstract
  run⊥ : ∀ {ℓ} {α : Set ℓ} → α ⊥ → IO α
  run⊥ (now x)   = return x
  run⊥ (later x) = run⊥ (♭ x)


{- |
  Use the partiality monad to write something like getLines.
-}

module Lines where

open import Category.Monad.Partiality as P
open import Coinduction
open import Data.Bool
open import Data.Colist hiding (fromList) renaming ([_] to co[_])
open import Data.List hiding (break; map)

-- Type of separator indicators.

isSep : ∀ {ℓ} → Set ℓ → Set ℓ
isSep α = α → Bool

-- Access the partiality monad "workaround".

open P.Workaround

-- Break a colist into "lines" on a (dropped) separator.
-- Partial since the input may not have any separators.

break' : ∀ {ℓ} {α : Set ℓ} → isSep α → Colist α → Colist (List α) ⊥P
break' sep? [] = now []
break' sep? (x ∷ xs) with sep? x
... | true = later (♯ (break' sep? (♭ xs) >>= λ ls → now ([] ∷ ♯ ls)))
... | _    = later (♯ (break' sep? (♭ xs) >>= λ ls → front x ls))
             where front : ∀ {α} → α → Colist (List α) → Colist (List α) ⊥P
                   front x []        = now (co[ [ x ] ])
                   front x (y ∷ ys)  = now ((x ∷ y) ∷ ys)

break : ∀ {ℓ} {α : Set ℓ} → isSep α → Colist α → Colist (List α) ⊥
break sep? xs = ⟦ break' sep? xs ⟧P

-- A little example to run.

open import Data.Char
open import Data.String hiding (_==_)
open import Data.Unit
open import Function
open import IO

open import Divergence

getLines : Costring → Colist (List Char) ⊥
getLines = break (_==_ '\n')

writeLines : Colist (List Char) → IO ⊤
writeLines ls = ♯ mapM′ (putStrLn ∘ fromList) ls >> ♯ putStrLn "Done"

go : IO ⊤
go = ♯ (♯ getContents >>= ♯_ ∘ run⊥ ∘ getLines) >>= ♯_ ∘ writeLines

main = run go