
   0 | module Fix
   1 | 
   2 | import Data.List
   3 | import Data.List1
   4 | import Data.String
   5 | 
   6 | %default total
   7 | 
   8 | NL : Char
   9 | NL = '\n'
  10 | 
  11 | dropWhile1 : (a -> Bool) -> List1 a -> List1 a
  12 | dropWhile1 f (h ::: t) = h ::: dropWhile f t
  13 | 
  14 | noTrailingSpace : List Char -> List Char
  15 | noTrailingSpace = reverse . dropWhile isSpace . reverse
  16 | 
  17 | noTrailingNewlines : List1 (List Char) -> List1 (List Char)
  18 | noTrailingNewlines = reverse . dropWhile1 (\x => null x) . cons [] . reverse
  19 | 
  20 | -- reimplemented since original `unlines` to be testable.
  21 | unlinesImpl : List1 (List Char) -> List Char
  22 | unlinesImpl ([] ::: []) = [NL]
  23 | unlinesImpl (h ::: t)   = h ++ run t
  24 | 
  25 |   where
  26 |     run : List (List Char) -> List Char
  27 |     run []          = []
  28 |     run (cs :: css) = NL :: cs ++ run css
  29 | 
  30 | 
  31 | removeCRLF : List Char -> List Char
  32 | removeCRLF []                   = []
  33 | removeCRLF ('\r' :: '\n' :: xs) = '\n' :: removeCRLF xs
  34 | removeCRLF (x :: xs)            = x :: removeCRLF xs
  35 | 
  36 | transformImpl : List Char -> List Char
  37 | transformImpl =
  38 |     unlinesImpl
  39 |   . noTrailingNewlines
  40 |   . map noTrailingSpace
  41 |   . split isNL
  42 |   . removeCRLF
  43 | 
  44 | ||| Transforms the given string in the following way:
  45 | |||  * on every line, trailing whitespace characters are removed
  46 | |||  * makes sure the string ends with exactly one newline character
  47 | |||
  48 | ||| Note: So far, a newline character corresponds to `'\n'`.
  49 | export
  50 | transform : String -> String
  51 | transform = fastPack . transformImpl . fastUnpack
  52 | 
  53 | --------------------------------------------------------------------------------
  54 | --          Tests
  55 | --------------------------------------------------------------------------------
  56 | 
  57 | TestNoTrailingSpace : String -> String
  58 | TestNoTrailingSpace = pack . noTrailingSpace . unpack
  59 | 
  60 | noTrailingTest0 : TestNoTrailingSpace "" = ""
  61 | noTrailingTest0 = Refl
  62 | 
  63 | noTrailingTest1 : TestNoTrailingSpace "a test   " = "a test"
  64 | noTrailingTest1 = Refl
  65 | 
  66 | noTrailingTest2 : TestNoTrailingSpace "a test\t \t" = "a test"
  67 | noTrailingTest2 = Refl
  68 | 
  69 | noTrailingTest3 : TestNoTrailingSpace "a test" = "a test"
  70 | noTrailingTest3 = Refl
  71 | 
  72 | TestTransformImpl : String -> String
  73 | TestTransformImpl = pack . transformImpl . unpack
  74 | 
  75 | transTest0 : TestTransformImpl "" = "\n"
  76 | transTest0 = Refl
  77 | 
  78 | transTest1 : TestTransformImpl "test" = "test\n"
  79 | transTest1 = Refl
  80 | 
  81 | transTest2 : TestTransformImpl "test\n\n" = "test\n"
  82 | transTest2 = Refl
  83 | 
  84 | transTest3 : TestTransformImpl "test\ntrailing   \n\n" = "test\ntrailing\n"
  85 | transTest3 = Refl
  86 | 
  87 | transTest4 : TestTransformImpl "test\ntrailing   \t" = "test\ntrailing\n"
  88 | transTest4 = Refl
  89 | 
  90 | transTest5 : TestTransformImpl "test\r\ntrailing" = "test\ntrailing\n"
  91 | transTest5 = Refl
  92 | 
  93 | Empties : List String
  94 | Empties =
  95 |   [ ""
  96 |   , "\n"
  97 |   , "\n\n"
  98 |   , "\n\n\n"
  99 |   , " \n  \n\n"
 100 |   , " \n  \n\n\t"
 101 |   ]
 102 | 
 103 | testEmpties : map TestTransformImpl Empties = replicate (length Empties) "\n"
 104 | testEmpties = Refl
 105 |