
  0 | ||| This module contains an efficient string builder
  1 | module Libraries.Data.String.Builder
  2 | 
  3 | import public Libraries.Data.DList
  4 | 
  5 | export
  6 | intersperse : a -> List a -> DList a
  7 | intersperse sep [] = []
  8 | intersperse sep [x] = [x]
  9 | intersperse sep (x :: xs) = x :: go sep xs
 10 |   where
 11 |     go : a -> List a -> DList a
 12 |     go sep [] = []
 13 |     go sep (x :: xs) = sep :: x :: go sep xs
 14 | 
 15 | public export
 16 | Builder : Type
 17 | Builder = DList String
 18 | 
 19 | public export
 20 | char : Char -> Builder
 21 | char c = fromString $ cast c
 22 | 
 23 | export
 24 | sepBy : String -> List Builder -> Builder
 25 | sepBy sep [] = []
 26 | sepBy sep [x] = x
 27 | sepBy sep (x :: xs) = x ++ go sep xs
 28 |   where
 29 |     go : String -> List Builder -> Builder
 30 |     go sep [] = []
 31 |     go sep (x :: xs) = sep :: x ++ go sep xs
 32 | 
 33 | public export
 34 | build : Builder -> String
 35 | build = fastConcat . reify
 36 | 
 37 | public export
 38 | showB : Show a => a -> Builder
 39 | showB = singleton . show
 40 |