simple uniq in Idris

simple-uniq.idr

-- % idris simple-uniq.idr -o uniq
module Main

getContents : IO String
getContents = go ""
  where go : String -> IO String
        go s = do case !(feof stdin) of
                    True  => return s
                    False => do t <- fread stdin
                                go (s ++ t)

interact : (String -> String) -> IO ()
interact f = do s <- getContents
                putStr (f s)
                putStr "\n"

uniq : String -> String
uniq = unlines . go . lines
  where go : List String -> List String
        go xs = case xs of
                  Nil => Nil
                  x :: Nil => x :: Nil
                  y :: (z :: zs) =>
                    case y == z of
                      True  => go (z :: zs)
                      False => y :: go (z :: zs)
                  
main : IO ()
main = interact uniq

terminated-uniq.idr

-- % idris terminated-uniq.idr -o uniq
module Main

getContents : IO String
getContents = go ""
  where go : String -> IO String
        go s = do case !(feof stdin) of
                    True  => return s
                    False => do t <- fread stdin
                                go (s ++ t)

interact : (String -> String) -> IO ()
interact f = do s <- getContents
                putStr (f s)
                putStr "\n"

uniq : String -> String
uniq = unlines . go . lines
  where go : List String -> List String
        go xs = case xs of
                  Nil => Nil
                  x :: Nil => x :: Nil
                  y :: (z :: zs) =>
                    if y == z
                      then go (z :: zs)
                      else y :: go (z :: zs)
                  
main : IO ()
main = interact uniq

case foo of
True => ...
False => ...
と
if foo
then ...
else ...
では、termination checker が異なる振る舞いをする
case 文では maybe terminate だが if 文では terminate を理解するらしい