Data.Container.Base.Display2D.Display2D

Reexports

Definitions

defaultLineWidth : Nat

  Approximate line-width budget for printed cubical tensors.  When a row of
  fixed-width cells does not fit on a single line, the renderer breaks it
  onto continuation lines so output stays within roughly this many columns.
  Matches NumPy's default `linewidth = 75`.

Totality: total
Visibility: public export

Grid : Type -> Type

  A `Grid a` is a rectangular 2D matrix. Unlike `List >@ List`, which 
  produces ragged arrays, this produces rectangular ones

Totality: total
Visibility: public export

gridHeight : Grid a -> Nat

Totality: total
Visibility: public export

gridWidth : Grid a -> Nat

Totality: total
Visibility: public export

gridIndex : (g : Grid a) -> Fin (gridHeight g) -> Fin (gridWidth g) -> a

  Look up a cell.  Cost depends on how `g` was built; for grids made from
  chained combinators the cost is proportional to the composition depth.

Totality: total
Visibility: public export

mkGrid : (h : Nat) -> (w : Nat) -> (Fin h -> Fin w -> a) -> Grid a

  Build a grid from a height, width, and 2D index function.  O(1).

Totality: total
Visibility: public export

gridRows : Grid a -> List (List a)

  Convert a `Grid` into a list-of-rows view.  Walks the grid once, so this
  is the natural one-shot materialisation point for delayed grids.

Totality: total
Visibility: public export

showGrid : Grid Char -> String

  Format a `Grid Char` as a multi-line string.  Trailing pad characters on
  each line are stripped, matching NumPy's printing conventions.

Totality: total
Visibility: public export

emptyGrid : Grid a

Totality: total
Visibility: public export

singleValue : a -> Grid a

Totality: total
Visibility: public export

uniformCol : a -> Nat -> Grid a

Totality: total
Visibility: public export

blankCol : Nat -> Grid Char

Totality: total
Visibility: public export

rowGrid : List a -> Grid a

  One-row grid built from a list of cells.

Totality: total
Visibility: public export

topMarkerCol : Char -> Nat -> Grid Char

  1-wide column carrying `marker` on its top row and `padCharacter` elsewhere.
  `emptyGrid` if the height is zero.

Totality: total
Visibility: public export

bottomMarkerCol : Char -> Nat -> Grid Char

  1-wide column carrying `marker` on its bottom row and `padCharacter`
  elsewhere. `emptyGrid` if the height is zero.

Totality: total
Visibility: public export

besideAllGap : a -> Nat -> List (Grid a) -> Grid a

  Place grids side-by-side with `gap` blank columns between each pair.  The
  row dimension is the max of the children's heights; shorter children are
  padded on the missing rows.

Totality: total
Visibility: public export

besideAll : a -> List (Grid a) -> Grid a

  Place grids side-by-side with no gap.

Totality: total
Visibility: public export

aboveAllSep : a -> Nat -> List (Grid a) -> Grid a

  Stack grids vertically, inserting `sep` blank rows between successive items.
  The column dimension is the max of the children's widths; narrower children
  are padded on the missing columns.

Totality: total
Visibility: public export

aboveAll : a -> List (Grid a) -> Grid a

  Stack grids vertically with no separator.

Totality: total
Visibility: public export

padGridLeft : Nat -> Grid Char -> Grid Char

  Left-pad a grid with `padCharacter` columns to reach total width `w`.
  No-op if `gridWidth g >= w`.

Totality: total
Visibility: public export

addBorderToGrid : Box => Grid Char -> Grid Char

  Wrap a grid in a 1-character border specified by `box`.

Totality: total
Visibility: public export

wrapNonEmpty : Box => Grid Char -> Grid Char

  Wrap a grid in a border if it has more than one row

Totality: total
Visibility: public export

wrapAllIfAnyNonEmpty : Box => List (Grid Char) -> Grid Char -> Grid Char

  Given a list of grids, make a function that wraps a grid in a border if
  any of the grids in the list has more than one row

Totality: total
Visibility: public export

horizontalListJoin : ListSyntax => List (Grid Char) -> Grid Char

  Join a list of grids horizontally with a separator between them

Totality: total
Visibility: public export

wrapListBrackets : ListSyntax => Nat -> List (Grid Char) -> Grid Char

  Wrap a list of grids vertically in `[` ... `]` brackets with `,` markers in 
  front of subsequent items, as follows:
  
      [item1
      ,item2
      ,item3]
  
  `nSep` is the number of blank rows between items:

Totality: total
Visibility: public export

wrappedInnerRow : ListSyntax => Nat -> Nat -> List (Grid Char) -> Grid Char

  Render a list of equal-width cells as `[ c0 c1 ... cN ]`, breaking the
  output onto continuation lines when the single-line layout would exceed
  `lineBudget` columns.  Continuation lines are indented by one space so
  wrapped cells align under `c0`; the closing `]` sits next to the last cell
  of the final chunk, so a shorter final chunk leaves trailing whitespace on
  its line (NumPy-style).
  
  The single-line layout falls out automatically when `cellsPerLine >= length
  children`, so no separate "flat" code path is needed.

Totality: total
Visibility: public export

interface Display2D : Type -> Type

  Display a type as a 2D grid of characters.
  For `a` being an extension of a container, this can be expresse in terms of
  a container morphism... if we use `Maybe <!>`

Parameters: a
Constructor: 

MkDisplay2D

Methods:

display2D : a -> Grid Char

Implementations:

Display2D (Grid Char)

Display2D Int

Display2D Integer

Display2D Double

Display2D Nat

Display2D Bool

Display2D ()

Display2D Char

Display2D String

Display2D a => Display2D (Scalar' a)

Display2D a => Display2D b => Display2D (a, b)

Display2D a => Display2D (Pair' a)

Display2D a => Display2D (List' a)

Display2D a => Display2D (BinTree' a)

Display2D a => Display2D (Ext BinTreeLeaf a)

Display2D a => Display2D (Ext BinTreeNode a)

Display2D a => Display2D (Ext (Vect n) a)

display2D : Display2D a => a -> Grid Char

Totality: total
Visibility: public export

display2DFromShow : Show a => a -> Grid Char

  One-row grid from a `Show` instance.

Totality: total
Visibility: public export

display2DFromSci : ScientificDisplay a => a -> Grid Char

  One-row grid from a `ScientificDisplay` instance.

Totality: total
Visibility: public export

showViaDisplay2D : Display2D a => a -> String

Totality: total
Visibility: public export