uniq.agda

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

module PartialityStream where

  open import IO using (IO; return; _>>=_)
  open import Function
  open import Coinduction

  -- Colist に later を追加したもの
  data Stream⊥ {a} (A : Set a) : Set a where
    []  : Stream⊥ A
    _∷_ : (x : A) (xs : ∞ (Stream⊥ A)) → Stream⊥ A
    later : (x : ∞ (Stream⊥ A)) → Stream⊥ A

  map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Stream⊥ A → Stream⊥ B
  map f []         = []
  map f (x ∷ xs)   = f x ∷ ♯ map f (♭ xs)
  map f (later xs) = later (♯ map f (♭ xs))

  sequence : ∀ {a} {A : Set a} → Stream⊥ (IO A) → IO (Stream⊥ A)
  sequence []       = return []
  sequence (c ∷ cs) = ♯ c                  >>= λ x  →
                      ♯ (♯ sequence (♭ cs) >>= λ xs →
                      ♯ return (x ∷ ♯ xs))
  sequence (later cs) = ♯ sequence (♭ cs) >>= λ xs →
                        ♯ return (later (♯ xs))

  mapM : ∀ {a b} {A : Set a} {B : Set b} →
         (A → IO B) → Stream⊥ A → IO (Stream⊥ B)
  mapM f = sequence ∘ map f

  open import Data.Colist

  fromColist : ∀ {a} {A : Set a} → Colist A → Stream⊥ A
  fromColist [] = []
  fromColist (x ∷ xs) = x ∷ ♯ fromColist (♭ xs)

open PartialityStream public

open import Data.Char using (Char)
open import Data.String using (String)
open import Data.Maybe hiding (map)
open import Coinduction
open import Category.Monad.Partiality hiding (map)
open import Category.Monad.State
open import Category.Monad
open import IO using (IO)
open import Data.Unit using (⊤)

module DoLikeNotation {l M} (monad : RawMonad {l} M) where
  open RawMonad monad
  bind-syntax = _>>=_
  syntax bind-syntax F (λ x → G) = ∣ x ← F ∣ G

takeLine : StateT (∞ (Stream⊥ Char)) _⊥ (Maybe String)
takeLine = proj₁ M.<$> ((LS.get LM.>>= go ∘ ♭) "") where
  open import Function
  open import Relation.Nullary
  open import Data.List using ([_])
  open import Data.String using (_++_; fromList; _≟_)
  open import Data.Product
  -- モナドI/Fとかリフトとかのサンプル
  module S = RawIMonadState (StateTMonadState (∞ (Stream⊥ Char)) (Category.Monad.Partiality.monad))
  module M = RawMonad S.monad
  module SS = RawIMonadState (StateTMonadState String S.monad)
  module LS = RawIMonadState (LiftMonadState String (StateTMonadState (∞ (Stream⊥ Char)) (Category.Monad.Partiality.monad)))
  module LM = RawMonad LS.monad
  open DoLikeNotation LS.monad
  go : Stream⊥ Char → StateT String (StateT (∞ (Stream⊥ Char)) _⊥) (Maybe String)
  go [] = SS.get LM.>>= LM.return ∘ flush where
    flush : String → Maybe String
    flush x with x Data.String.≟ ""
    ... | yes _ = nothing
    ... | no  _ = just x
  go (x ∷ xs) with x Data.Char.≟ '\n'
  ... | yes _ = ∣ _ ← LS.put xs
              ∣ ∣ acc ← SS.get
              ∣ ∣ _ ← SS.put ""
                ∣ LM.return (just acc)
  ... | no  _ = λ acc ss → later (♯ go (♭ xs) (acc ++ fromList [ x ]) xs) -- 相性が悪い…こうせざるをえない
  go (later xs) = λ acc ss → later (♯ go (♭ xs) acc ss)

lines : Stream⊥ Char → Stream⊥ String
lines = go ∘ takeLine ∘ ♯_ where
  open import Function
  open import Data.Product
  go : (Maybe String × ∞ (Stream⊥ Char)) ⊥ → Stream⊥ String
  go (now (nothing , _)) = []
  go (now (just x , xs)) = x ∷ ♯ go (takeLine xs)
  go (later x) = later (♯ go (♭ x))

unlines : Stream⊥ String → Stream⊥ Char
unlines = go ∘ map toList where
  open import Function
  open import Data.List using (List)
  open import Data.String using (toList)
  go : Stream⊥ (List Char) → Stream⊥ Char
  go [] = []
  go (Data.List.[] ∷ xss) = '\n' ∷ ♯ go (♭ xss)
  go ((x Data.List.∷ xs) ∷ xss) = x ∷ ♯ go (xs ∷ xss)
  go (later xss) = later (♯ go (♭ xss))

uniq : Stream⊥ String → Stream⊥ String
uniq = go nothing where
  open import Relation.Binary
  open DecSetoid (Data.Maybe.decSetoid Data.String.decSetoid)
  open import Relation.Nullary
  go : Maybe String → Stream⊥ String → Stream⊥ String
  go mx [] = []
  go mx (x ∷ xs) with mx ≟ just x
  ... | yes _ = later (♯ go mx (♭ xs))
  ... | no  _ = x ∷ ♯ go (just x) (♭ xs)
  go mx (later x) = later (♯ go mx (♭ x))

void : ∀ {a} → IO a → IO ⊤
void action = ♯ action >>= λ _ → ♯ return tt where
  open import IO using (_>>=_; return)
  open import Data.Unit using (tt)

interact : (Stream⊥ Char → Stream⊥ Char) → IO ⊤
interact f = ♯ getContents >>= ♯_ ∘ void ∘ mapM (putStr ∘ fromList ∘ [_]) ∘ f ∘ fromColist where
  open import Function
  open import IO using (_>>=_; getContents; putStr)
  open import Data.List using ([_])
  open import Data.String using (fromList)

main = interact (unlines ∘ map coloring ∘ uniq ∘ lines) where
  open import Function
  open import Data.String using (_++_)
  coloring : String → String
  coloring ss = "\x1b[32m" ++ ss ++ "\x1b[39m" -- わかりやすいように色付け