AtCoder Beginner Contest #011 A問題

ABC011A.agda

module ABC011A where

open import IO
open import Function
open import Coinduction
open import Data.String using (String)

nextMonthOf : String → String
nextMonthOf "1"  = "2"
nextMonthOf "2"  = "3"
nextMonthOf "3"  = "4"
nextMonthOf "4"  = "5"
nextMonthOf "5"  = "6"
nextMonthOf "6"  = "7"
nextMonthOf "7"  = "8"
nextMonthOf "8"  = "9"
nextMonthOf "9"  = "10"
nextMonthOf "10" = "11"
nextMonthOf "11" = "12"
nextMonthOf "12" = "1"
nextMonthOf _    = "Unknown month"

main = run (♯ getContents >>= ♯_ ∘ eachline nextMonthOf) where

  open import Data.Maybe
  open import Data.Product
  open import Data.List using ([]; _∷_; [_])
  open import Data.Colist using (Colist; []; _∷_)
  open import Data.String using (Costring; fromList; _++_)
  open import Data.Unit using (⊤; tt)
  open import Category.Monad.Partiality

  takeLine : Costring → Maybe (String × ∞ Costring) ⊥
  takeLine [] = now nothing -- EOF
  takeLine xs = go "" xs where
    go : String → Costring → Maybe (String × ∞ Costring) ⊥
    go acc [] = now (just (acc , ♯ []))
    go acc (x ∷ xs) with fromList [ x ]
    go acc (_ ∷ xs) | "\n" = now (just (acc , xs))
    go acc (_ ∷ xs) | last = later (♯ go (acc ++ last) (♭ xs))

  eachline : (String → String) → Costring → IO ⊤
  eachline f = go ∘ takeLine where
    go : Maybe (String × ∞ Costring) ⊥ → IO ⊤
    go (now nothing) = return tt
    go (now (just (line , xs))) = ♯ putStrLn (f line) >> ♯ go (takeLine (♭ xs))
    go (later x) = ♯ return tt >> ♯ go (♭ x)