
   0 | module Text.PrettyPrint.Bernardy.Core
   1 | 
   2 | import Data.DPair
   3 | import Data.List
   4 | import Data.String
   5 | 
   6 | %default total
   7 | 
   8 | --------------------------------------------------------------------------------
   9 | --          NonEmpty SnocList
  10 | --------------------------------------------------------------------------------
  11 | 
  12 | public export
  13 | data NonEmptySnoc : SnocList a -> Type where
  14 |   IsNonEmptySnoc : NonEmptySnoc (sx :< x)
  15 | 
  16 | 0 nonEmptyChips : {auto p : NonEmptySnoc sx} -> NonEmpty (sx <>> xs)
  17 | nonEmptyChips {sx = Lin :< _}        = %search
  18 | nonEmptyChips {sx = h@(_ :< _) :< _} = nonEmptyChips {sx = h}
  19 | 
  20 | %inline
  21 | kcap : SnocList Char -> String
  22 | kcap = pack . (<>> [])
  23 | 
  24 | allLines :
  25 |      (inp : List Char)
  26 |   -> (sc : SnocList Char)
  27 |   -> SnocList String
  28 |   -> SnocList String
  29 | allLines []                   sc sl = sl :< kcap sc
  30 | allLines ('\n' :: '\r' :: xs) sc sl = allLines xs Lin (sl :< kcap sc)
  31 | allLines ('\n' :: xs)         sc sl = allLines xs Lin (sl :< kcap sc)
  32 | allLines ('\r' :: xs)         sc sl = allLines xs Lin (sl :< kcap sc)
  33 | allLines (x :: xs)            sc sl = allLines xs (sc :< x) sl
  34 | 
  35 | --------------------------------------------------------------------------------
  36 | --          Stats
  37 | --------------------------------------------------------------------------------
  38 | 
  39 | public export
  40 | record LayoutOpts where
  41 |     [noHints]
  42 |     constructor Opts
  43 |     lineLength : Nat
  44 | 
  45 | record Stats where
  46 |     constructor MkStats
  47 |     maxLine  : Nat
  48 |     lastLine : Nat
  49 |     height   : Nat
  50 | 
  51 | -- stats for a string without line breaks
  52 | lstats : String -> Stats
  53 | lstats s = let n := length s in MkStats n n 0
  54 | 
  55 | -- updates the stats after appending a string without line break
  56 | addStats : String -> Stats -> Stats
  57 | addStats s (MkStats ml ll h) = MkStats (max ml $ length s) ll (S h)
  58 | 
  59 | -- Compare two stats in the presence of a maximal page width.
  60 | -- We consider a layout `x` to be superior than layout `y`
  61 | -- if
  62 | --   a) the two layouts do not overflow the page and
  63 | --      all stats of `x` are smaller or equal than the stats of `y`,
  64 | -- or
  65 | --   b) `y` overflows the page and the width of `x` is smaller than the
  66 | --      one of `y`
  67 | -- If neither a) nor b) hold for one the arguments, this function
  68 | -- returns `EQ`.
  69 | compStats : LayoutOpts -> Stats -> Stats -> Ordering
  70 | compStats (Opts ll) (MkStats mll lll hl) (MkStats mlr llr hr) =
  71 |   -- if one layout overflows, keep only the narrower
  72 |   if      mll < mlr && ll < mlr then LT
  73 |   else if mlr < mll && ll < mll then GT
  74 |   -- if one layout dominates the other, keep only the
  75 |   -- dominating one.
  76 |   else if mll <= mlr && lll <= llr && hl <= hr then LT
  77 |   else if mlr <= mll && llr <= lll && hr <= hl then GT
  78 |   else    EQ
  79 | 
  80 | --------------------------------------------------------------------------------
  81 | --          Layout
  82 | --------------------------------------------------------------------------------
  83 | 
  84 | export
  85 | record Layout where
  86 |     constructor MkLayout
  87 |     -- It is essential that we are lazy here: When deciding on the best
  88 |     -- layout, we only need the stats but not the actual list of lines.
  89 |     -- We need those only when rendering the preferred layout.
  90 |     --
  91 |     -- We use a `SnocList` because we often concatenate layouts
  92 |     -- by using left folds over lists of layouts. A `SnocList` is a
  93 |     -- natural and efficient accumulator in a left fold.
  94 |     content : Lazy (SnocList String)
  95 |     stats   : Stats
  96 |     {auto 0 prfNonEmptyContent : NonEmptySnoc content}
  97 | 
  98 | layout : Lazy (Subset (SnocList String) NonEmptySnoc) -> Stats -> Layout
  99 | layout ss st = MkLayout (fst ss) st @{snd ss}
 100 | 
 101 | namespace Layout
 102 | 
 103 |     ||| Returns the number of lines in a `Layout`.
 104 |     export %inline
 105 |     height : Layout -> Nat
 106 |     height = S . height . stats
 107 | 
 108 |     ||| Returns the number of lines in a `Layout`.
 109 |     export %inline
 110 |     isMultiline : Layout -> Bool
 111 |     isMultiline = (> 1) . height
 112 | 
 113 |     ||| Returns the width of the longest line in a `Layout`
 114 |     export %inline
 115 |     width : Layout -> Nat
 116 |     width = maxLine . stats
 117 | 
 118 |     export %inline
 119 |     isEmpty : Layout -> Bool
 120 |     isEmpty l = height l == 0 && width l == 0
 121 | 
 122 |     ||| The empty layout, consisting of a single empty line.
 123 |     export
 124 |     empty : Layout
 125 |     empty = MkLayout [<""] (MkStats 0 0 0)
 126 | 
 127 |     ||| Render the given layout
 128 |     export
 129 |     render : Layout -> String
 130 |     render (MkLayout sl _) = unlines (sl <>> [])
 131 | 
 132 |     ||| Convert a single line of text to a layout.
 133 |     |||
 134 |     ||| @ str this must be single line of text.
 135 |     export
 136 |     line : (str : String) -> Layout
 137 |     line s = MkLayout [<s] (lstats s)
 138 | 
 139 |     ||| Convert a string to a layout.
 140 |     ||| This preserves any manual formatting
 141 |     |||
 142 |     ||| @ str the String to pretty print
 143 |     export
 144 |     text : (str : String) -> Layout
 145 |     text str = case allLines (unpack str) Lin Lin of
 146 |       Lin          => empty
 147 |       ls@(sx :< x) => MkLayout ls (foldr addStats (lstats x) sx)
 148 | 
 149 |     indentOnto :
 150 |          (sx : SnocList String)
 151 |       -> (xs : List String)
 152 |       -> {auto 0 p1 : NonEmptySnoc sx}
 153 |       -> Nat
 154 |       -> Subset (SnocList String) NonEmptySnoc
 155 |     indentOnto sx []        _ = Element sx p1
 156 |     indentOnto sx (x :: xs) n = indentOnto (sx :< indent n x) xs n
 157 | 
 158 |     appendOnto :
 159 |          (sx : SnocList String)
 160 |       -> (xs : List String)
 161 |       -> {auto 0 p1 : NonEmptySnoc sx}
 162 |       -> {auto 0 p2 : NonEmpty xs}
 163 |       -> Nat
 164 |       -> Subset (SnocList String) NonEmptySnoc
 165 |     appendOnto (sx :< x) (y :: ys) n = indentOnto (sx :< (x ++ y)) ys n
 166 | 
 167 | 
 168 |     ||| Concatenate to Layouts horizontally
 169 |     export
 170 |     Semigroup Layout where
 171 |       MkLayout c s <+> MkLayout d t =
 172 |         let -- this is needed for the call to `appendOnto` below
 173 |             0 prf        := nonEmptyChips {xs = []} {sx = d}
 174 | 
 175 |             newStats     :=
 176 |               MkStats {
 177 |                 maxLine  = max s.maxLine $ s.lastLine + t.maxLine
 178 |               , lastLine = s.lastLine + t.maxLine
 179 |               , height   = s.height + t.height
 180 |               }
 181 | 
 182 |          in layout (appendOnto c (d <>> []) s.lastLine) newStats
 183 | 
 184 |     export %inline
 185 |     Monoid Layout where
 186 |       neutral = empty
 187 | 
 188 |     export %inline
 189 |     FromString Layout where
 190 |       fromString = text
 191 | 
 192 |     export
 193 |     flush : Layout -> Layout
 194 |     flush (MkLayout sl $ MkStats ml _ h) =
 195 |       MkLayout (sl :< "") (MkStats ml 0 $ S h)
 196 | 
 197 |     export
 198 |     indent : Nat -> Layout -> Layout
 199 |     -- We make sure to not force the string of empty chars and make use
 200 |     -- of our knowledge about its stats.
 201 |     indent k x = MkLayout [< replicate k ' '] (MkStats k k 0) <+> x
 202 | 
 203 |     shortest : Layout -> List Layout -> Layout
 204 |     shortest x xs =
 205 |       foldl (\x,y => if x.stats.height <= y.stats.height then x else y) x xs
 206 | 
 207 | --------------------------------------------------------------------------------
 208 | --          Doc
 209 | --------------------------------------------------------------------------------
 210 | 
 211 | ||| A non-empty selection of possible layouts.
 212 | export
 213 | record Doc (opts : LayoutOpts) where
 214 |     constructor MkDoc
 215 |     head : Layout
 216 |     tail : List Layout
 217 | 
 218 | export %inline
 219 | pure : Layout -> Doc opts
 220 | pure l = MkDoc l []
 221 | 
 222 | %inline
 223 | layouts : Doc opts -> List Layout
 224 | layouts (MkDoc h t) = h :: t
 225 | 
 226 | namespace Doc
 227 |     ||| Render the best candidate from the given set of layouts
 228 |     export
 229 |     render : (opts : _) -> Doc opts -> String
 230 |     render opts (MkDoc x xs) = render $ shortest x xs
 231 | 
 232 |     -- prepend layouts in a SnocList to a list of layouts.
 233 |     chips1 : SnocList Layout -> Layout -> List Layout -> Doc opts
 234 |     chips1 (sx :< y) x xs = chips1 sx y (x :: xs)
 235 |     chips1 [<]       x xs = MkDoc x xs
 236 | 
 237 |     insert :
 238 |          {opts : _}
 239 |       -> SnocList Layout
 240 |       -> List Layout
 241 |       -> Layout
 242 |       -> Doc opts
 243 |     insert sl []       x = chips1 sl x []
 244 |     insert sl (h :: t) x = case compStats opts x.stats h.stats of
 245 |       LT => insert sl t x
 246 |       EQ => insert (sl :< h) t x
 247 |       GT => chips1 sl h t
 248 | 
 249 |     combine : {opts : _} -> Doc opts -> List Layout -> Doc opts
 250 |     combine d (y :: ys) = combine (insert Lin (layouts d) y) ys
 251 |     combine d []        = d
 252 | 
 253 |     ||| Choose the better of two different documents.
 254 |     export %inline
 255 |     (<|>) : {opts : _} -> Doc opts -> Doc opts -> Doc opts
 256 |     x <|> y = combine x $ layouts y
 257 | 
 258 |     ||| Concatenate two documents horizontally.
 259 |     |||
 260 |     ||| The first line of the second document will be appended
 261 |     ||| to the last line of the first, and the remaining lines
 262 |     ||| of the second will be indented accordingly.
 263 |     |||
 264 |     ||| For instance, for documents `x` and `y` of the following
 265 |     ||| shapes
 266 |     |||
 267 |     ||| ```
 268 |     ||| xxxxxxxxxxx
 269 |     ||| xxxxxxxxxxxxxx
 270 |     ||| xxx
 271 |     ||| ```
 272 |     ||| and
 273 |     |||
 274 |     ||| ```
 275 |     ||| yyyyy
 276 |     ||| yy
 277 |     ||| yyyy
 278 |     ||| ```
 279 |     ||| the result will be aligned as follows:
 280 |     |||
 281 |     ||| ```
 282 |     ||| xxxxxxxxxxx
 283 |     ||| xxxxxxxxxxxxxx
 284 |     ||| xxxyyyyy
 285 |     |||    yy
 286 |     |||    yyyy
 287 |     ||| ```
 288 |     export
 289 |     (<+>) : {opts : _} -> Doc opts -> Doc opts -> Doc opts
 290 |     MkDoc x xs <+> MkDoc y ys =
 291 |       let appYs := \v => MkDoc (v <+> y) (map (v <+>) ys)
 292 |           ini   := appYs x
 293 |        in foldl (\acc,x => combine {opts} (appYs x) $ layouts acc) ini xs
 294 | 
 295 |     export %inline
 296 |     FromString (Doc opts) where
 297 |         fromString str = pure $ fromString str
 298 | 
 299 |     ||| The empty document, consisting of a single emtpy line.
 300 |     export %inline
 301 |     empty : Doc opts
 302 |     empty = pure neutral
 303 | 
 304 |     export
 305 |     (>>=) : {opts : _} -> Doc opts -> (Layout -> Doc opts) -> Doc opts
 306 |     (>>=) (MkDoc x xs) f = foldl (\d,l => d <|> f l) (f x) xs
 307 | 
 308 |     ||| Creates a single-line document from the given string.
 309 |     |||
 310 |     ||| @str A string without line breaks
 311 |     export %inline
 312 |     line : (str : String) -> Doc opts
 313 |     line = pure . line
 314 | 
 315 |     ||| Flushes the last line of the given document, so that an appended
 316 |     ||| document starts on a new line.
 317 |     export
 318 |     flush : {opts : _} -> Doc opts -> Doc opts
 319 |     flush (MkDoc x xs) = MkDoc (flush x) $ map flush xs
 320 | 
 321 |     ||| Indents the given document by a number of spaces.
 322 |     export
 323 |     indent : {opts : _} -> Nat -> Doc opts -> Doc opts
 324 |     indent k (MkDoc  x xs) = combine (pure $ indent k x) (indent k <$> xs)
 325 | 
 326 |     ||| Indents the given document by a number of spaces, if it's not empty.
 327 |     export
 328 |     indent' : {opts : _} -> Nat -> Doc opts -> Doc opts
 329 |     indent' k x = do
 330 |       l <- x
 331 |       pure $ if isEmpty l then l else indent k l
 332 | 
 333 |     ||| Displays a single string, preserving any manual formatting.
 334 |     export %inline
 335 |     text : String -> (Doc opts)
 336 |     text = pure . text
 337 |