The many ways of dropping trailing new lines in Idris

dropnewline.idr

-- In Idris, fGetLine returns a string with a trailing newline. Here are
-- various ways of getting rid of it. I'm hoping I missed something more
-- straighforward. In all of the functions below, I'm assuming there is
-- exactly one '\n' character and that it occurs at the end of the string.

module Main

dropNewline0 : (x : String) -> String
dropNewline0 x =
  fst $ break (== '\n') x
  -- also, as an aside: how do I do the above with composition?

dropNewline1 : (x : String) -> String
dropNewline1 x =
  let
    (line, nl) = break (== '\n') x
  in
    line

dropNewline2 : (x : String) -> String
dropNewline2 x =
  let
    ls = lines x
  in
    case nonEmpty ls of
        (Yes prf) =>   head ls
        (No contra) =>  ""

dropNewline3 : (x : String) -> String
dropNewline3 x =
  let
    i = length x
  in
    case i of
         Z => ""
         (S k) => substr 0 k x

dropNewline4 : (x : String) -> String
dropNewline4 x =
  case decEq (not (reverse x == "")) True of
       (Yes prf) =>  reverse $ strTail' (reverse x) prf
       (No contra) => ""

||| Same idea as above, except using strTail which uses prim__strTail, and will
||| crash on empty string
dropNewline5 : (x : String) -> String
dropNewline5 x =
  reverse $ (strTail . reverse) x

example0 : "hi" = dropNewline0 "hi\n"
example0 = Refl

example1 : "hi" = dropNewline1 "hi\n"
example1 = Refl

example2 : "hi" = dropNewline2 "hi\n"
example2 = Refl

example3 : "hi" = dropNewline3 "hi\n"
example3 = Refl

example4 : "hi" = dropNewline4 "hi\n"
example4 = Refl


-- While dropNewline5 *will* do the right thing, so long as you don't pass it
-- an empty string, strTail uses prim__strTail and idris won't deal with:
--example5 : "hi" = dropNewline5 "hi\n"
--example5 = Refl
-- If you uncomment this, it will yield: 

--  dropnewline.idr:69:12-15:
--     |
--  68 | example5 = Refl
--     |            ~~~~
--  When checking right hand side of example5 with expected type
--          "hi" = dropNewline5 "hi\n"
--  
--  Type mismatch between
--          dropNewline5 "hi\n" = dropNewline5 "hi\n" (Type of Refl)
--  and
--          "hi" = dropNewline5 "hi\n" (Expected type)
--  
--  Specifically:
--          Type mismatch between
--                  dropNewline5 "hi\n"
--          and
--                  "hi"
--  

dropNewline0 : (x : String) -> String
dropNewline0 = fst . break (== '\n')

This is what it looks like with composition.

Several years later, but thanks for the tip @shaleh, sorry I missed this two years ago :)

Glad you found it