
   0 | module Data.Container.Base.Display2D.Display2D
   1 | 
   2 | import Data.Fin
   3 | import Data.List
   4 | import Data.Vect
   5 | 
   6 | 
   7 | import Data.Container.Base.Object.Definition
   8 | import Data.Container.Base.Extension.Definition
   9 | import Data.Container.Base.Product.Definition
  10 | 
  11 | import Data.Container.Base.Object.Instances
  12 | import Data.Container.Base.Extension.Instances
  13 | import Data.Container.Base.Properties.Instances
  14 | 
  15 | import public Data.Container.Base.Display2D.CharacterMap
  16 | import Data.ScientificNotation
  17 | 
  18 | import Data.Container.Base.TreeUtils
  19 | import Misc
  20 | 
  21 | {-------------------------------------------------------------------------------
  22 | Machinery for rendering values as rectangular 2D character grids.
  23 | 
  24 | Layout combinators (`besideAllGap`, `aboveAllSep`, `addBorderToGrid`, ...)
  25 | build new grids by (1) computing the output shape from the inputs at the data
  26 | level, and (2) building a new index function that dispatches into the inputs.
  27 | Both steps are O(1).  Lookup cost in a deeply composed grid is proportional
  28 | to the composition depth; `gridRows` (used by `showGrid`) is the one-shot
  29 | materialisation point that walks each cell exactly once.
  30 | 
  31 | As tensor utilities are added, functionality within this file will be rewritten
  32 | -------------------------------------------------------------------------------}
  33 | 
  34 | ||| Approximate line-width budget for printed cubical tensors.  When a row of
  35 | ||| fixed-width cells does not fit on a single line, the renderer breaks it
  36 | ||| onto continuation lines so output stays within roughly this many columns.
  37 | ||| Matches NumPy's default `linewidth = 75`.
  38 | public export
  39 | defaultLineWidth : Nat
  40 | defaultLineWidth = 75
  41 | 
  42 | {-------------------------------------------------------------------------------
  43 | Core: Grid type, accessors, basic constructors
  44 | -------------------------------------------------------------------------------}
  45 | 
  46 | ||| A `Grid a` is a rectangular 2D matrix. Unlike `List >@ List`, which 
  47 | ||| produces ragged arrays, this produces rectangular ones
  48 | public export
  49 | Grid : Type -> Type
  50 | Grid = Ext (List >< List)
  51 | 
  52 | public export
  53 | gridHeight : Grid a -> Nat
  54 | gridHeight ((h, _) <| _) = h
  55 | 
  56 | public export
  57 | gridWidth : Grid a -> Nat
  58 | gridWidth ((_, w) <| _) = w
  59 | 
  60 | ||| Look up a cell.  Cost depends on how `g` was built; for grids made from
  61 | ||| chained combinators the cost is proportional to the composition depth.
  62 | public export
  63 | gridIndex : (g : Grid a) -> Fin (gridHeight g) -> Fin (gridWidth g) -> a
  64 | gridIndex ((_, _) <| f) i j = f (i, j)
  65 | 
  66 | ||| Build a grid from a height, width, and 2D index function.  O(1).
  67 | public export
  68 | mkGrid : (h, w : Nat) -> (Fin h -> Fin w -> a) -> Grid a
  69 | mkGrid h w f = (h, w) <| uncurry f
  70 | 
  71 | 
  72 | {-------------------------------------------------------------------------------
  73 | Materialisation
  74 | -------------------------------------------------------------------------------}
  75 | 
  76 | ||| Convert a `Grid` into a list-of-rows view.  Walks the grid once, so this
  77 | ||| is the natural one-shot materialisation point for delayed grids.
  78 | public export
  79 | gridRows : Grid a -> List (List a)
  80 | gridRows g =
  81 |   toList' $ Fin.tabulate {len = gridHeight g} $ \i =>
  82 |     toList' $ Fin.tabulate {len = gridWidth  g} $ \j =>
  83 |       gridIndex g i j
  84 | 
  85 | ||| Format a `Grid Char` as a multi-line string.  Trailing pad characters on
  86 | ||| each line are stripped, matching NumPy's printing conventions.
  87 | public export
  88 | showGrid : Grid Char -> String
  89 | showGrid =
  90 |   concat . intersperse "\n" . map (pack . dropFromEnd padCharacter) . gridRows
  91 | 
  92 | 
  93 | {-------------------------------------------------------------------------------
  94 | Primitive constructors
  95 | -------------------------------------------------------------------------------}
  96 | 
  97 | public export
  98 | emptyGrid : Grid a
  99 | emptyGrid = mkGrid 0 0 absurd
 100 | 
 101 | public export
 102 | singleValue : a -> Grid a
 103 | singleValue v = mkGrid 1 1 (\_, _ => v)
 104 | 
 105 | public export
 106 | uniformCol : a -> Nat -> Grid a
 107 | uniformCol v h = mkGrid h 1 (\_, _ => v)
 108 | 
 109 | public export
 110 | blankCol : Nat -> Grid Char
 111 | blankCol = uniformCol padCharacter
 112 | 
 113 | ||| One-row grid built from a list of cells.
 114 | public export
 115 | rowGrid : List a -> Grid a
 116 | rowGrid xs = mkGrid 1 (length xs) (\_, j => index j (fromList xs))
 117 | 
 118 | ||| 1-wide column carrying `marker` on its top row and `padCharacter` elsewhere.
 119 | ||| `emptyGrid` if the height is zero.
 120 | public export
 121 | topMarkerCol : (marker : Char) -> (h : Nat) -> Grid Char
 122 | topMarkerCol _ Z = emptyGrid
 123 | topMarkerCol c (S k) = mkGrid (S k) 1 $ \i, _ => case i of
 124 |   FZ => c
 125 |   _  => padCharacter
 126 | 
 127 | ||| 1-wide column carrying `marker` on its bottom row and `padCharacter`
 128 | ||| elsewhere. `emptyGrid` if the height is zero.
 129 | public export
 130 | bottomMarkerCol : (marker : Char) -> (h : Nat) -> Grid Char
 131 | bottomMarkerCol _ Z = emptyGrid
 132 | bottomMarkerCol c (S k) = mkGrid (S k) 1 $ \i, _ => case i == last of
 133 |   True => c
 134 |   False => padCharacter
 135 | 
 136 | 
 137 | {-------------------------------------------------------------------------------
 138 | Multiway layout combinators
 139 | 
 140 | Each takes O(1) to construct and produces a delayed grid whose index function
 141 | linearly scans the inputs.  For typical fan-outs (2..16) this is plenty fast.
 142 | -------------------------------------------------------------------------------}
 143 | 
 144 | ||| Locate global position `i` in a sequence of items each of width `size g`,
 145 | ||| with `gap` blank positions between consecutive items.  Returns the item
 146 | ||| together with a properly bounded local index, or `Nothing` if `i` lands in
 147 | ||| a gap or past the end.
 148 | |||
 149 | ||| Total: recursion is structural on the list of grids.
 150 | locateChunk : (size : Grid a -> Nat) ->
 151 |   (gap : Nat) ->
 152 |   (gs : List (Grid a)) ->
 153 |   Nat ->
 154 |   Maybe (g : Grid a ** Fin (size g))
 155 | locateChunk _ _ [] _ = Nothing
 156 | locateChunk size gap (g :: gs) i = case natToFin i (size g) of
 157 |   Just j  => Just (g ** j)
 158 |   Nothing => let sz = size g
 159 |              in case i < sz + gap of
 160 |                True => Nothing
 161 |                False => locateChunk size gap gs (minus i (sz + gap))
 162 | 
 163 | ||| Place grids side-by-side with `gap` blank columns between each pair.  The
 164 | ||| row dimension is the max of the children's heights; shorter children are
 165 | ||| padded on the missing rows.
 166 | public export
 167 | besideAllGap : (padValue : a) -> (gap : Nat) -> List (Grid a) -> Grid a
 168 | besideAllGap _ _ [] = emptyGrid
 169 | besideAllGap _ _ [g] = g
 170 | besideAllGap pad gap grids@(_ :: _) =
 171 |   let maxHeight = max (gridHeight <$> grids)
 172 |       sumWidths = List.sum (gridWidth <$> grids) + gap * pred (length grids)
 173 |   in mkGrid maxHeight sumWidths $ \i, j => fromMaybe pad $ do
 174 |        (g ** j') <- locateChunk gridWidth gap grids (finToNat j)
 175 |        i' <- natToFin (finToNat i) (gridHeight g)
 176 |        pure (gridIndex g i' j')
 177 | 
 178 | ||| Place grids side-by-side with no gap.
 179 | public export
 180 | besideAll : (padValue : a) -> List (Grid a) -> Grid a
 181 | besideAll pad = besideAllGap pad 0
 182 | 
 183 | ||| Stack grids vertically, inserting `sep` blank rows between successive items.
 184 | ||| The column dimension is the max of the children's widths; narrower children
 185 | ||| are padded on the missing columns.
 186 | public export
 187 | aboveAllSep : (padValue : a) -> (sep : Nat) -> List (Grid a) -> Grid a
 188 | aboveAllSep _ _ [] = emptyGrid
 189 | aboveAllSep _ _ [g] = g
 190 | aboveAllSep pad sep grids@(_ :: _) =
 191 |   let sumHeights = List.sum (gridHeight <$> grids) + sep * pred (length grids)
 192 |       maxWidth = max (gridWidth <$> grids)
 193 |   in mkGrid sumHeights maxWidth $ \i, j => fromMaybe pad $ do
 194 |        (g ** i') <- locateChunk gridHeight sep grids (finToNat i)
 195 |        j' <- natToFin (finToNat j) (gridWidth g)
 196 |        pure (gridIndex g i' j')
 197 | 
 198 | ||| Stack grids vertically with no separator.
 199 | public export
 200 | aboveAll : (padValue : a) -> List (Grid a) -> Grid a
 201 | aboveAll pad = aboveAllSep pad 0
 202 | 
 203 | ||| Left-pad a grid with `padCharacter` columns to reach total width `w`.
 204 | ||| No-op if `gridWidth g >= w`.
 205 | public export
 206 | padGridLeft : (w : Nat) -> Grid Char -> Grid Char
 207 | padGridLeft w g = besideAll padCharacter
 208 |   [mkGrid (gridHeight g) (w `minus` gridWidth g) (\_, _ => padCharacter), g]
 209 | 
 210 | {-------------------------------------------------------------------------------
 211 | Borders
 212 | -------------------------------------------------------------------------------}
 213 | 
 214 | ||| Given a `k : Nat`, models a three-way classification of `Fin (S (S k))` into
 215 | ||| first, last, or middle.
 216 | data Side : (k : Nat) -> Type where
 217 |   AtStart : Side k
 218 |   AtEnd   : Side k
 219 |   AtMid   : Fin k -> Side k
 220 | 
 221 | side : {k : Nat} -> Fin (S (S k)) -> Side k
 222 | side FZ     = AtStart
 223 | side (FS x) = maybe AtEnd AtMid (strengthen x)
 224 | 
 225 | ||| Wrap a grid in a 1-character border specified by `box`.
 226 | public export
 227 | addBorderToGrid : (box : Box) => Grid Char -> Grid Char
 228 | addBorderToGrid g = mkGrid (2 + gridHeight g) (2 + gridWidth g) $ \i, j =>
 229 |   case (side i, side j) of
 230 |     (AtMid i', AtMid j') => gridIndex g i' j'
 231 |     (AtMid _,  _)        => box.vertical
 232 |     (_,        AtMid _)  => box.horizontal
 233 |     (AtStart,  AtStart)  => box.topLeft
 234 |     (AtStart,  AtEnd)    => box.topRight
 235 |     (AtEnd,    AtStart)  => box.bottomLeft
 236 |     (AtEnd,    AtEnd)    => box.bottomRight
 237 | 
 238 | ||| Wrap a grid in a border if it has more than one row
 239 | public export
 240 | wrapNonEmpty : Box => Grid Char -> Grid Char
 241 | wrapNonEmpty g = applyWhen (gridHeight g > 1) addBorderToGrid g
 242 | 
 243 | ||| Given a list of grids, make a function that wraps a grid in a border if
 244 | ||| any of the grids in the list has more than one row
 245 | public export
 246 | wrapAllIfAnyNonEmpty : Box =>
 247 |   List (Grid Char) -> (Grid Char -> Grid Char)
 248 | wrapAllIfAnyNonEmpty grids =
 249 |   applyWhen (any (\g => gridHeight g > 1) grids) addBorderToGrid
 250 | 
 251 | 
 252 | {-------------------------------------------------------------------------------
 253 | List/pair brackets and joins
 254 | -------------------------------------------------------------------------------}
 255 | 
 256 | ||| Join a list of grids horizontally with a separator between them
 257 | public export
 258 | horizontalListJoin : (listSyntax : ListSyntax) => List (Grid Char) -> Grid Char
 259 | horizontalListJoin []  = emptyGrid
 260 | horizontalListJoin [g] = g
 261 | horizontalListJoin gs  = besideAll padCharacter (intersperse sep gs)
 262 |   where sep = besideAll padCharacter
 263 |               [singleValue listSyntax.separator, singleValue padCharacter]
 264 | 
 265 | ||| Wrap a list of grids vertically in `[` ... `]` brackets with `,` markers in 
 266 | ||| front of subsequent items, as follows:
 267 | |||
 268 | |||     [item1
 269 | |||     ,item2
 270 | |||     ,item3]
 271 | ||| 
 272 | ||| `nSep` is the number of blank rows between items:
 273 | public export
 274 | wrapListBrackets : (listSyntax : ListSyntax) =>
 275 |   (nSep : Nat) -> List (Grid Char) -> Grid Char
 276 | wrapListBrackets _ [] = besideAll padCharacter
 277 |   [singleValue listSyntax.left, singleValue listSyntax.right]
 278 | wrapListBrackets nSep (x :: xs) =
 279 |   let body     = aboveAllSep padCharacter nSep (x :: xs)
 280 |       leftCol  = aboveAll padCharacter $
 281 |                    topMarkerCol listSyntax.left (gridHeight x) ::
 282 |                    concatMap (\g => [ blankCol nSep
 283 |                                     , topMarkerCol listSyntax.separator (gridHeight g)
 284 |                                     ]) xs
 285 |       rightCol = bottomMarkerCol listSyntax.right (gridHeight body)
 286 |   in besideAll padCharacter [leftCol, body, rightCol]
 287 | 
 288 | 
 289 | {-------------------------------------------------------------------------------
 290 | NumPy-style row wrapping for long innermost rows
 291 | -------------------------------------------------------------------------------}
 292 | 
 293 | ||| Render a list of equal-width cells as `[ c0 c1 ... cN ]`, breaking the
 294 | ||| output onto continuation lines when the single-line layout would exceed
 295 | ||| `lineBudget` columns.  Continuation lines are indented by one space so
 296 | ||| wrapped cells align under `c0`; the closing `]` sits next to the last cell
 297 | ||| of the final chunk, so a shorter final chunk leaves trailing whitespace on
 298 | ||| its line (NumPy-style).
 299 | |||
 300 | ||| The single-line layout falls out automatically when `cellsPerLine >= length
 301 | ||| children`, so no separate "flat" code path is needed.
 302 | public export
 303 | wrappedInnerRow : (listSyntax : ListSyntax) =>
 304 |   (lineBudget, gap : Nat) -> List (Grid Char) -> Grid Char
 305 | wrappedInnerRow _ _ [] = besideAll padCharacter
 306 |   [singleValue listSyntax.left, singleValue listSyntax.right]
 307 | wrappedInnerRow lineBudget gap children@(c :: _) =
 308 |   let cellsPerLine = max 1 $ (lineBudget `minus` 2 + gap) `div` (gridWidth c + gap)
 309 |       chunks       = chunksOf cellsPerLine children
 310 |       nChunks      = length chunks
 311 |       chunkRow : Nat -> List (Grid Char) -> Grid Char
 312 |       chunkRow i cs =
 313 |         let leftC  = if i == 0         then listSyntax.left  else padCharacter
 314 |             rightC = if S i == nChunks then listSyntax.right else padCharacter
 315 |         in besideAll padCharacter
 316 |              [ singleValue leftC
 317 |              , besideAllGap padCharacter gap cs
 318 |              , singleValue rightC ]
 319 |   in aboveAll padCharacter (mapWithIndex chunkRow chunks)
 320 | 
 321 | 
 322 | {-------------------------------------------------------------------------------
 323 | Display2D interface: rendering types as 2D character grids
 324 | -------------------------------------------------------------------------------}
 325 | 
 326 | ||| Display a type as a 2D grid of characters.
 327 | ||| For `a` being an extension of a container, this can be expresse in terms of
 328 | ||| a container morphism... if we use `Maybe <!>`
 329 | public export
 330 | interface Display2D (0 a : Type) where
 331 |   constructor MkDisplay2D
 332 |   display2D : a -> Grid Char
 333 | 
 334 | public export
 335 | Display2D (Grid Char) where
 336 |   display2D = id
 337 | 
 338 | ||| One-row grid from a `Show` instance.
 339 | public export
 340 | display2DFromShow : Show a => a -> Grid Char
 341 | display2DFromShow x = rowGrid (unpack (show x))
 342 | 
 343 | ||| One-row grid from a `ScientificDisplay` instance.
 344 | public export
 345 | display2DFromSci : ScientificDisplay a => a -> Grid Char
 346 | display2DFromSci x = rowGrid (unpack (showSci x))
 347 | 
 348 | public export Display2D Int     where display2D = display2DFromShow
 349 | public export Display2D Integer where display2D = display2DFromSci
 350 | public export Display2D Double  where display2D = display2DFromSci
 351 | public export Display2D Nat     where display2D = display2DFromSci
 352 | public export Display2D Bool    where display2D = display2DFromShow
 353 | public export Display2D ()      where display2D = display2DFromShow
 354 | public export Display2D Char    where display2D = singleValue
 355 | public export Display2D String  where display2D s = rowGrid (unpack s)
 356 | 
 357 | 
 358 | {-------------------------------------------------------------------------------
 359 | Display2D instances for container extensions
 360 | -------------------------------------------------------------------------------}
 361 | 
 362 | public export
 363 | Display2D a => Display2D (Scalar' a) where
 364 |   display2D (() <| index) = display2D (index ())
 365 | 
 366 | public export
 367 | Display2D a => Display2D b => Display2D (a, b) where
 368 |   display2D (x, y) = besideAll padCharacter
 369 |     [ singleValue (left AsciiPairSyntax)
 370 |     , display2D x
 371 |     , singleValue (separator AsciiPairSyntax)
 372 |     , display2D y
 373 |     , singleValue (right AsciiPairSyntax) ]
 374 | 
 375 | public export
 376 | Display2D a => Display2D (Pair' a) where
 377 |   display2D (() <| index) = besideAll padCharacter
 378 |     [ singleValue (left AsciiPairSyntax)
 379 |     , display2D (index False)
 380 |     , singleValue (separator AsciiPairSyntax)
 381 |     , display2D (index True)
 382 |     , singleValue (right AsciiPairSyntax) ]
 383 | 
 384 | public export
 385 | Display2D a => Display2D (List' a) where
 386 |   display2D (_ <| index) = besideAll padCharacter
 387 |     [ singleValue (left AsciiListSyntax)
 388 |     , horizontalListJoin {listSyntax = AsciiListSyntax}
 389 |         (display2D <$> toList' (tabulate index))
 390 |     , singleValue (right AsciiListSyntax) ]
 391 | 
 392 | 
 393 | {-------------------------------------------------------------------------------
 394 | Tree helpers
 395 | -------------------------------------------------------------------------------}
 396 | 
 397 | ||| 2-column tree-branch prefix: first row is `connector` + `treeHorizontal`;
 398 | ||| subsequent rows are `continuation` + `treeGap`.
 399 | treeBranchPrefix : (tree : Tree) =>
 400 |   (connector, continuation : Char) -> (height : Nat) -> Grid Char
 401 | treeBranchPrefix _ _ Z = emptyGrid
 402 | treeBranchPrefix conn cont (S k) = mkGrid (S k) 2 $ \i, j =>
 403 |   case (i, j) of
 404 |     (FZ, FZ) => conn
 405 |     (FZ, _ ) => tree.horizontal
 406 |     (_ , FZ) => cont
 407 |     (_ , _ ) => tree.gap
 408 | 
 409 | ||| Prepend a tree-branch prefix and a 1-column gap to a grid.
 410 | addBranch : Tree =>
 411 |   (connector, continuation : Char) -> Grid Char -> Grid Char
 412 | addBranch conn cont g = besideAll padCharacter
 413 |   [treeBranchPrefix conn cont (gridHeight g), blankCol (gridHeight g), g]
 414 | 
 415 | ||| Full-width row between sibling subtrees: `vertical` then spaces.
 416 | treeSiblingGapRow : (tree : Tree) => (w : Nat) -> Grid Char
 417 | treeSiblingGapRow Z = emptyGrid
 418 | treeSiblingGapRow (S k) = mkGrid 1 (S k) $ \_, j => case j of
 419 |   FZ => tree.vertical
 420 |   _  => padCharacter
 421 | 
 422 | ||| Lay out a tree node: root above, then left/right subtrees with branches.
 423 | displayNodeWithBranches : (tree : Tree) =>
 424 |   (root, left, right : Grid Char) -> Grid Char
 425 | displayNodeWithBranches root left right =
 426 |   let leftB  = addBranch tree.branchMid  tree.vertical left
 427 |       rightB = addBranch tree.branchLast tree.gap      right
 428 |       top    = aboveAll padCharacter
 429 |                  [root, treeSiblingGapRow (maximum (gridWidth root) (gridWidth leftB)), leftB]
 430 |   in aboveAll padCharacter [top, treeSiblingGapRow (gridWidth top), rightB]
 431 | 
 432 | 
 433 | {-------------------------------------------------------------------------------
 434 | BinTree (values on both nodes and leaves)
 435 | -------------------------------------------------------------------------------}
 436 | 
 437 | 
 438 | collectBinTreeValues : Display2D a =>
 439 |   BinTree' a ->
 440 |   (List (Grid Char), List (Grid Char))
 441 | collectBinTreeValues (LeafS <| index) = ([], [display2D (index AtLeaf)])
 442 | collectBinTreeValues n@(NodeS l r <| index) =
 443 |   let (ln, ll) = collectBinTreeValues $ assert_smaller n (l <| (index . GoLeft))
 444 |       (rn, rl) = collectBinTreeValues $ assert_smaller n (r <| (index . GoRight))
 445 |   in (display2D (index AtNode) :: (ln ++ rn), ll ++ rl)
 446 | 
 447 | 
 448 | displayBinTreeWith : Display2D a => (tree : Tree) =>
 449 |   (nodeBox, leafBox : Grid Char -> Grid Char) ->
 450 |   BinTree' a -> Grid Char
 451 | displayBinTreeWith _ leafBox (LeafS <| index)
 452 |   = leafBox (display2D (index AtLeaf))
 453 | displayBinTreeWith nodeBox leafBox n@(NodeS l r <| index) =
 454 |   displayNodeWithBranches (nodeBox (display2D (index AtNode)))
 455 |     (displayBinTreeWith nodeBox leafBox $ assert_smaller n (l <| (index . GoLeft)))
 456 |     (displayBinTreeWith nodeBox leafBox $ assert_smaller n (r <| (index . GoRight)))
 457 | 
 458 | displayBinTree : Display2D a => (tree : Tree) => (box : Box) =>
 459 |   BinTree' a -> Grid Char
 460 | displayBinTree t =
 461 |   let (nodeEGs, leafEGs) = collectBinTreeValues t 
 462 |   in displayBinTreeWith (wrapAllIfAnyNonEmpty nodeEGs)
 463 |                         (wrapAllIfAnyNonEmpty leafEGs) t 
 464 | 
 465 | public export
 466 | Display2D a => Display2D (BinTree' a) where
 467 |   display2D = displayBinTree {tree = SingleLineTree, box = DoubleLineBox}
 468 | 
 469 | 
 470 | {-------------------------------------------------------------------------------
 471 | BinTreeLeaf (values only on leaves)
 472 | -------------------------------------------------------------------------------}
 473 | 
 474 | 
 475 | collectLeafValues : Display2D a =>
 476 |   BinTreeLeaf' a ->
 477 |   List (Grid Char)
 478 | collectLeafValues (LeafS <| index) = [display2D (index AtLeaf)]
 479 | collectLeafValues n@(NodeS l r <| index) =
 480 |   collectLeafValues (assert_smaller n (l <| index . GoLeft)) ++
 481 |   collectLeafValues (assert_smaller n (r <| index . GoRight))
 482 | 
 483 | displayBinTreeLeafWith : Display2D a => (tree : Tree) =>
 484 |   (leafBox : Grid Char -> Grid Char) ->
 485 |   BinTreeLeaf' a -> Grid Char
 486 | displayBinTreeLeafWith box (LeafS <| index) = box (display2D (index AtLeaf))
 487 | displayBinTreeLeafWith box n@(NodeS l r <| index) =
 488 |   displayNodeWithBranches (singleValue tree.placeholder)
 489 |     (displayBinTreeLeafWith box $ assert_smaller n (l <| index . GoLeft))
 490 |     (displayBinTreeLeafWith box $ assert_smaller n (r <| index . GoRight))
 491 | 
 492 | ||| Uniform boxing for BinTreeLeaf: if any leaf is multi-line, box all
 493 | displayBinTreeLeaf : Display2D a => (tree : Tree) => (box : Box) =>
 494 |   BinTreeLeaf' a -> Grid Char
 495 | displayBinTreeLeaf t =
 496 |   displayBinTreeLeafWith (wrapAllIfAnyNonEmpty (collectLeafValues t)) t 
 497 | 
 498 | public export
 499 | Display2D a => Display2D (Ext BinTreeLeaf a) where
 500 |   display2D = displayBinTreeLeaf {tree = SingleLineTree, box = DoubleLineBox}
 501 | 
 502 | 
 503 | {-------------------------------------------------------------------------------
 504 | BinTreeNode (values only on nodes)
 505 | -------------------------------------------------------------------------------}
 506 | 
 507 | 
 508 | collectNodeValues : Display2D a =>
 509 |   BinTreeNode' a -> List (Grid Char)
 510 | collectNodeValues (LeafS <| _) = []
 511 | collectNodeValues n@(NodeS l r <| index) =
 512 |   let leftValues = collectNodeValues $ assert_smaller n (l <| index . GoLeft)
 513 |       rightValues = collectNodeValues $ assert_smaller n (r <| index . GoRight)
 514 |   in display2D (index AtNode) :: (leftValues ++ rightValues)
 515 | 
 516 | 
 517 | displayBinTreeNodeWith : Display2D a => (tree : Tree) =>
 518 |   (nodeBox : Grid Char -> Grid Char) ->
 519 |   BinTreeNode' a -> Grid Char
 520 | displayBinTreeNodeWith _ (LeafS <| _) = singleValue tree.placeholder
 521 | displayBinTreeNodeWith box n@(NodeS l r <| index) =
 522 |   displayNodeWithBranches (box (display2D (index AtNode)))
 523 |     (displayBinTreeNodeWith box $ assert_smaller n (l <| index . GoLeft))
 524 |     (displayBinTreeNodeWith box $ assert_smaller n (r <| index . GoRight))
 525 | 
 526 | 
 527 | displayBinTreeNode : Display2D a => (tree : Tree) => (box : Box) =>
 528 |   BinTreeNode' a -> Grid Char
 529 | displayBinTreeNode t =
 530 |   displayBinTreeNodeWith (wrapAllIfAnyNonEmpty (collectNodeValues t)) t
 531 | 
 532 | public export
 533 | Display2D a => Display2D (Ext BinTreeNode a) where
 534 |   display2D = displayBinTreeNode {tree = SingleLineTree, box = DoubleLineBox}
 535 | 
 536 | public export
 537 | {n : Nat} -> Display2D a => Display2D (Ext (Vect n) a) where
 538 |   display2D (() <| index) = display2D {a = Ext List a} (n <| index)
 539 | 
 540 | public export
 541 | showViaDisplay2D : Display2D a => a -> String
 542 | showViaDisplay2D = showGrid . display2D
 543 | 
 544 | public export
 545 | Display2D a => Show (Scalar' a) where
 546 |   show = showViaDisplay2D
 547 | 
 548 | public export
 549 | Display2D a => Show (Pair' a) where
 550 |   show = showViaDisplay2D
 551 | 
 552 | public export
 553 | Display2D a => Show (List' a) where
 554 |   show = showViaDisplay2D
 555 | 
 556 | public export
 557 | {n : Nat} -> Display2D a => Show (Vect' n a) where
 558 |   show = showViaDisplay2D
 559 | 
 560 | public export
 561 | Display2D a => Show (BinTree' a) where
 562 |   show t = showViaDisplay2D t
 563 | 
 564 | public export
 565 | Display2D a => Show (BinTreeLeaf' a) where
 566 |   show t = showViaDisplay2D t
 567 | 
 568 | public export
 569 | Display2D a => Show (BinTreeNode' a) where
 570 |   show t = showViaDisplay2D t