
  0 | module Data.String.Builder
  1 | 
  2 | import Control.Relation
  3 | import Control.Order
  4 | import public Data.DiffList
  5 | import Syntax.PreorderReasoning.Generic
  6 | 
  7 | public export
  8 | Builder : Type
  9 | Builder = DiffList String
 10 | 
 11 | public export %inline
 12 | FromString Builder where
 13 |     fromString = singleton
 14 | 
 15 | public export
 16 | char : Char -> Builder
 17 | char = singleton . cast
 18 | 
 19 | public export %inline
 20 | build : Builder -> String
 21 | build b = concat $ DiffList.toList b
 22 | 
 23 | public export
 24 | sepBy : Builder -> List Builder -> Builder
 25 | sepBy _ [] = neutral
 26 | sepBy _ [x] = x
 27 | sepBy sep (x :: xs) = MkDiffList
 28 |     (\rest => x.append (go xs rest))
 29 |     (\rest =>
 30 |         let xsPrf = goIsSuffix _ _
 31 |             xPrf = x.isSuffix _
 32 |          in transitive xsPrf xPrf)
 33 |   where
 34 |     go : List Builder -> List String -> List String
 35 |     go [] acc = acc
 36 |     go (x :: xs) acc = sep.append (x.append (go xs acc))
 37 | 
 38 |     0
 39 |     goIsSuffix : (xs : List Builder) -> (rest : List String) -> IsSuffixOf rest (go xs rest)
 40 |     goIsSuffix [] rest = SuffixRefl
 41 |     goIsSuffix (x :: xs) rest = CalcWith $
 42 |         |~ rest
 43 |         <~ go xs rest ...(goIsSuffix _ _)
 44 |         <~ x.append (go xs rest) ...(x.isSuffix _)
 45 |         <~ sep.append (x.append (go xs rest)) ...(sep.isSuffix _)
 46 |         <~ go (x :: xs) rest ...(reflexive)
 47 | 
 48 | public export %inline
 49 | showB : Show a => a -> Builder
 50 | showB = singleton . show
 51 |