19 | %hide Syntax.WithProof.prefix.(@@)
21 | {-------------------------------------------------------------------------------
22 | Machinery for rendering values as rectangular 2D character grids.
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.
31 | As tensor utilities are added, functionality within this file will be rewritten
32 | -------------------------------------------------------------------------------}
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`.
42 | {-------------------------------------------------------------------------------
43 | Core: Grid type, accessors, basic constructors
44 | -------------------------------------------------------------------------------}
46 | ||| A `Grid a` is a rectangular 2D matrix. Unlike `List >@ List`, which
47 | ||| produces ragged arrays, this produces rectangular ones
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.
66 | ||| Build a grid from a height, width, and 2D index function. O(1).
72 | {-------------------------------------------------------------------------------
73 | Materialisation
74 | -------------------------------------------------------------------------------}
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.
85 | ||| Format a `Grid Char` as a multi-line string. Trailing pad characters on
86 | ||| each line are stripped, matching NumPy's printing conventions.
93 | {-------------------------------------------------------------------------------
94 | Primitive constructors
95 | -------------------------------------------------------------------------------}
113 | ||| One-row grid built from a list of cells.
118 | ||| 1-wide column carrying `marker` on its top row and `padCharacter` elsewhere.
119 | ||| `emptyGrid` if the height is zero.
127 | ||| 1-wide column carrying `marker` on its bottom row and `padCharacter`
128 | ||| elsewhere. `emptyGrid` if the height is zero.
137 | {-------------------------------------------------------------------------------
138 | Multiway layout combinators
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 | -------------------------------------------------------------------------------}
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.
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.
178 | ||| Place grids side-by-side with no gap.
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.
198 | ||| Stack grids vertically with no separator.
203 | ||| Left-pad a grid with `padCharacter` columns to reach total width `w`.
204 | ||| No-op if `gridWidth g >= w`.
210 | {-------------------------------------------------------------------------------
211 | Borders
212 | -------------------------------------------------------------------------------}
214 | ||| Given a `k : Nat`, models a three-way classification of `Fin (S (S k))` into
215 | ||| first, last, or middle.
225 | ||| Wrap a grid in a 1-character border specified by `box`.
238 | ||| Wrap a grid in a border if it has more than one row
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
252 | {-------------------------------------------------------------------------------
253 | List/pair brackets and joins
254 | -------------------------------------------------------------------------------}
256 | ||| Join a list of grids horizontally with a separator between them
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:
289 | {-------------------------------------------------------------------------------
290 | NumPy-style row wrapping for long innermost rows
291 | -------------------------------------------------------------------------------}
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.
322 | {-------------------------------------------------------------------------------
323 | Display2D interface: rendering types as 2D character grids
324 | -------------------------------------------------------------------------------}
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 <!>`
338 | ||| One-row grid from a `Show` instance.
343 | ||| One-row grid from a `ScientificDisplay` instance.
358 | {-------------------------------------------------------------------------------
359 | Display2D instances for container extensions
360 | -------------------------------------------------------------------------------}
384 | {-------------------------------------------------------------------------------
385 | Tree helpers
386 | -------------------------------------------------------------------------------}
388 | ||| 2-column tree-branch prefix: first row is `connector` + `treeHorizontal`;
389 | ||| subsequent rows are `continuation` + `treeGap`.
400 | ||| Prepend a tree-branch prefix and a 1-column gap to a grid.
406 | ||| Full-width row between sibling subtrees: `vertical` then spaces.
413 | ||| Lay out a tree node: root above, then left/right subtrees with branches.
424 | {-------------------------------------------------------------------------------
425 | BinTree (values on both nodes and leaves)
426 | -------------------------------------------------------------------------------}
459 | {-------------------------------------------------------------------------------
460 | BinTreeLeaf (values only on leaves)
461 | -------------------------------------------------------------------------------}
480 | ||| Uniform boxing for BinTreeLeaf: if any leaf is multi-line, box all
491 | {-------------------------------------------------------------------------------
492 | BinTreeNode (values only on nodes)
493 | -------------------------------------------------------------------------------}
545 | -- Technocally should not need assert_total here, but its hard to convince
546 | -- the typechecker