-- uniqコマンド
--
-- $ agda -c -i. -i/usr/share/agda-stdlib/ uniq.agda
-- $ ./uniq
module uniq where

open import Data.Colist using (Colist; [])
open import Data.String using (String; Costring)
open import Data.Maybe
open import Data.Product
open import Coinduction
open import Category.Monad.Partiality
open import Category.Monad.State
open import Category.Monad
module S = RawIMonadState (StateTMonadState (∞ Costring) (Category.Monad.Partiality.monad))
module M = RawMonad S.monad

takeLine : StateT (∞ Costring) _⊥ (Maybe String)
takeLine = proj₁ M.<$> ((LS.get LM.>>= go ∘ ♭) "") where
  open import Function
  open import Data.List using ([_])
  open import Data.Colist using (Colist; _∷_)
  open import Data.String using (_++_; fromList)
  module SS = RawIMonadState (StateTMonadState String S.monad)
  module LS = RawIMonadState (LiftMonadState String (StateTMonadState (∞ Costring) (Category.Monad.Partiality.monad)))
  module LM = RawMonad LS.monad
  go : Costring → StateT String (StateT (∞ Costring) _⊥) (Maybe String)
  go [] = LM.return nothing
  go ('\n' ∷ xs) = LS.put xs LM.>>= λ _ →
                   SS.get    LM.>>= λ acc →
                   SS.put "" LM.>>= λ _ →
                   LM.return (just acc)
  go (  x  ∷ xs) = λ acc ss → later (♯ go (♭ xs) (acc ++ fromList [ x ]) xs) -- 相性が悪い
  --               LS.put xs LM.>>= λ _ →
  --               SS.get    LM.>>= λ acc →
  --               SS.put (acc ++ fromList [ x ]) LM.>>= λ _ →
  --               go (♭ xs) -- termination check にひっかかる
  -- でも結局関数合成なので，_>>=_で合成してしまうと適切に再帰をlaterで包めない！

uniq : Costring → Colist (Maybe String)
uniq = go nothing ∘ takeLine ∘ ♯_  where
  open import Function
  open import Data.Colist using ([]; _∷_)
  open import Relation.Binary
  open DecSetoid (Data.Maybe.decSetoid Data.String.decSetoid)
  open import Relation.Nullary
  go : Maybe String → (Maybe String × ∞ Costring) ⊥ → Colist (Maybe String)
  go _ (now (nothing , _)) = []
  go p (now (just line , xs)) with p ≟ just line
  ... | yes _ = nothing   ∷ ♯ go p           (takeLine xs)
  ... | no  _ = just line ∷ ♯ go (just line) (takeLine xs)
  go p (later x) = nothing ∷ ♯ go p (♭ x)

main = run (♯ getContents >>= ♯_ ∘ mapM (maybe coloredPutStrLn (return tt)) ∘ uniq) where
  open import IO
  open import Function
  open import Data.Unit
  open import Data.String using (_++_)
  coloredPutStrLn : String → IO ⊤
  coloredPutStrLn ss = putStrLn ("\x1b[32m" ++ ss ++ "\x1b[39m") -- 出力わかりやすいように色付け