0 | module Data.String.Builder
  1 |
  2 | import Data.Linear.Ref1
  3 | import Data.String
  4 | import Syntax.T1
  5 |
  6 | %default total
  7 |
  8 | ||| A simple mutable string builder based on a snoc list wrapped
  9 | ||| in a mutable reference.
 10 | export
 11 | record Builder (q : Type) where
 12 |   [noHints]
 13 |   constructor B
 14 |   ref : Ref q (SnocList String)
 15 |
 16 | ||| Creates a new string builder.
 17 | export %inline
 18 | builder : F1 q (Builder q)
 19 | builder = ref1 [<] >>= pure . B
 20 |
 21 | ||| Creates a string from a string building function.
 22 | export
 23 | withBuilder : (forall q . Builder q => F1' q) -> String
 24 | withBuilder f =
 25 |   run1 $ T1.do
 26 |     b <- builder
 27 |     f
 28 |     ss <- read1 b.ref
 29 |     pure (fastConcat $ ss <>> [])
 30 |
 31 | parameters {auto b : Builder q}
 32 |
 33 |   ||| Append a linebreak to the string builder.
 34 |   export
 35 |   linebreak : F1' q
 36 |   linebreak = T1.do
 37 |     ss <- read1 b.ref
 38 |     write1 b.ref (ss:<"\n")
 39 |
 40 |   ||| Append a single tab to the string builder.
 41 |   export
 42 |   tab : F1' q
 43 |   tab = T1.do
 44 |     ss <- read1 b.ref
 45 |     write1 b.ref (ss:<"\t")
 46 |
 47 |   ||| Append a single space to the string builder.
 48 |   export
 49 |   space : F1' q
 50 |   space = T1.do
 51 |     ss <- read1 b.ref
 52 |     write1 b.ref (ss:<" ")
 53 |
 54 |   ||| Append the given number of spaces to the string builder.
 55 |   export
 56 |   spaces : Nat -> F1' q
 57 |   spaces n = T1.do
 58 |     ss <- read1 b.ref
 59 |     write1 b.ref (ss:<replicate n ' ')
 60 |
 61 |   ||| Append the given string to the string builder.
 62 |   export
 63 |   putText : String -> F1' q
 64 |   putText "" = pure ()
 65 |   putText s  = T1.do
 66 |     ss <- read1 b.ref
 67 |     write1 b.ref (ss:<s)
 68 |
 69 |   ||| Append the given string followed by a carriage return
 70 |   ||| to the string builder.
 71 |   export
 72 |   putTextLn : String -> F1' q
 73 |   putTextLn "" = linebreak
 74 |   putTextLn s  = T1.do
 75 |     ss <- read1 b.ref
 76 |     write1 b.ref (ss:<s:<"\n")
 77 |
 78 |   ||| Append the given string followed by a space character return
 79 |   ||| to the string builder.
 80 |   export
 81 |   putTextSep : String -> F1' q
 82 |   putTextSep "" = pure ()
 83 |   putTextSep s  = T1.do
 84 |     ss <- read1 b.ref
 85 |     write1 b.ref (ss:<s:<" ")
 86 |
 87 |   ||| Appends the given list of characters to the string builder.
 88 |   export %inline
 89 |   putChars : List Char -> F1' q
 90 |   putChars = putText . fastPack
 91 |
 92 |   ||| Append the given list of characters followed by a carriage return
 93 |   ||| to the string builder.
 94 |   export %inline
 95 |   putCharsLn : List Char -> F1' q
 96 |   putCharsLn = putTextLn . fastPack
 97 |
 98 |   ||| Show a value and append it to the string builder.
 99 |   export %inline
100 |   putShow : Show a => a -> F1' q
101 |   putShow = putText . show
102 |
103 |   ||| Show a value and append it to the string builder followed
104 |   ||| by a carriage return.
105 |   export %inline
106 |   putShowLn : Show a => a -> F1' q
107 |   putShowLn = putTextLn . show
108 |
109 |   ||| Show a value and append it to the string builder followed
110 |   ||| by a space character.
111 |   export %inline
112 |   putShowSep : Show a => a -> F1' q
113 |   putShowSep = putTextSep . show
114 |
115 |   ||| Interpolate a value and append it to the string builder.
116 |   export %inline
117 |   putVal : Interpolation a => a -> F1' q
118 |   putVal = putText . interpolate
119 |
120 |   ||| Interpolate a value and append it to the string builder followed
121 |   ||| by a carriage return.
122 |   export %inline
123 |   putValLn : Interpolation a => a -> F1' q
124 |   putValLn = putTextLn . interpolate
125 |
126 |   ||| Interpolate a value and append it to the string builder followed
127 |   ||| by a space character.
128 |   export %inline
129 |   putValSep : Interpolation a => a -> F1' q
130 |   putValSep = putTextSep . interpolate
131 |
132 |   ||| Append a list of strings to the string builder.
133 |   export %inline
134 |   putAll : List String -> F1' q
135 |   putAll l = T1.do
136 |     ss <- read1 b.ref
137 |     write1 b.ref (ss <>< l)
138 |
139 |   ||| Append a string, padding it on the left with the given character.
140 |   export
141 |   putLeftPadded : Nat -> Char -> String -> F1' q
142 |   putLeftPadded n c s = T1.do
143 |     ss <- read1 b.ref
144 |     write1 b.ref (ss :< replicate (n `minus` length s) c :< s)
145 |
146 |   ||| Append a string, padding it on the right with the given character.
147 |   export
148 |   padRightPadded : Nat -> Char -> String -> F1' q
149 |   padRightPadded n c s = T1.do
150 |     ss <- read1 b.ref
151 |     write1 b.ref (ss:< s:< replicate (n `minus` length s) c)
152 |