------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of printing list and vec-based tables
------------------------------------------------------------------------

{-# OPTIONS --safe --cubical-compatible #-}

module README.Text.Tabular where

open import Function.Base
open import Relation.Binary.PropositionalEquality

open import Data.List.Base
open import Data.String.Base
open import Data.Vec.Base

open import Text.Tabular.Base
import Text.Tabular.List as Tabularˡ
import Text.Tabular.Vec  as Tabularᵛ

------------------------------------------------------------------------
-- VEC
--
-- If you have a matrix of strings, you simply need to:
--   * pick a configuration (see below)
--   * pick an alignment for each column
--   * pass the matrix
--
-- The display function will then pad each string on the left, right,
-- or both to respect the alignment constraints.
-- It will return a list of strings corresponding to each line in the
-- table. You may then:
---  * use Data.String.Base's unlines to produce a String
--   * use Text.Pretty's text and vcat to produce a Doc (i.e. indentable!)
------------------------------------------------------------------------

_ : unlines (Tabularᵛ.display unicode
            (Right  Left  Center  [])
          ( ("foo"  "bar"  "baz"  [])
           ("1"    "2"    "3"  [])
           ("6"    "5"    "4"  [])
           []))
   "┌───┬───┬───┐
\   \│foo│bar│baz│
\   \├───┼───┼───┤
\   \│  1│2  │ 3 │
\   \├───┼───┼───┤
\   \│  6│5  │ 4 │
\   \└───┴───┴───┘"
_ = refl

------------------------------------------------------------------------
-- CONFIG
--
-- Configurations allow you to change the way the table is displayed.
------------------------------------------------------------------------

-- We will use the same example throughout

foobar : Vec (Vec String 2) 3
foobar = ("foo"  "bar"  [])
        ("1"    "2"    [])
        ("4"    "3"    [])
        []

------------------------------------------------------------------------
-- Basic configurations: unicode, ascii, whitespace

-- unicode

_ : unlines (Tabularᵛ.display unicode
            (Right  Left  [])
            foobar)
   "┌───┬───┐
\   \│foo│bar│
\   \├───┼───┤
\   \│  1│2  │
\   \├───┼───┤
\   \│  4│3  │
\   \└───┴───┘"
_ = refl

-- ascii

_ : unlines (Tabularᵛ.display ascii
            (Right  Left  [])
            foobar)
   "+-------+
\   \|foo|bar|
\   \|---+---|
\   \|  1|2  |
\   \|---+---|
\   \|  4|3  |
\   \+-------+"
_ = refl

-- whitespace

_ : unlines (Tabularᵛ.display whitespace
            (Right  Left  [])
            foobar)
   "foo bar
\   \  1 2  
\   \  4 3  "
_ = refl

------------------------------------------------------------------------
-- Modifiers: altering existing configurations

-- In these examples we will be using unicode as the base configuration.
-- However these modifiers apply to all configurations (and can even be
-- combined)

-- compact: drop the horizontal line between each row

_ : unlines (Tabularᵛ.display (compact unicode)
            (Right  Left  [])
            foobar)
   "┌───┬───┐
\   \│foo│bar│
\   \│  1│2  │
\   \│  4│3  │
\   \└───┴───┘"
_ = refl

-- noBorder: drop the outside borders

_ : unlines (Tabularᵛ.display (noBorder unicode)
            (Right  Left  [])
            foobar)
   "foo│bar
\   \───┼───
\   \  1│2  
\   \───┼───
\   \  4│3  "
_ = refl

-- addSpace : add whitespace space inside cells

_ : unlines (Tabularᵛ.display (addSpace unicode)
            (Right  Left  [])
            foobar)
   "┌─────┬─────┐
\   \│ foo │ bar │
\   \├─────┼─────┤
\   \│   1 │ 2   │
\   \├─────┼─────┤
\   \│   4 │ 3   │
\   \└─────┴─────┘"
_ = refl

-- compact together with addSpace

_ : unlines (Tabularᵛ.display (compact (addSpace unicode))
            (Right  Left  [])
            foobar)
   "┌─────┬─────┐
\   \│ foo │ bar │
\   \│   1 │ 2   │
\   \│   4 │ 3   │
\   \└─────┴─────┘"
_ = refl


------------------------------------------------------------------------
-- LIST
--
-- Same thing as for vectors except that if the list of lists is not
-- rectangular, it is padded with empty strings to make it so. If there
-- are not enough alignment directives, we arbitrarily pick Left.
------------------------------------------------------------------------

_ : unlines (Tabularˡ.display unicode
          (Center  Right  [])
          ( ("foo"  "bar"  [])
           ("partial"  "rows"  "are"  "ok"  [])
           ("3"  "2"  "1"  "..."  "surprise!"  [])
           []))
   "┌───────┬────┬───┬───┬─────────┐
\   \│  foo  │ bar│   │   │         │
\   \├───────┼────┼───┼───┼─────────┤
\   \│partial│rows│are│ok │         │
\   \├───────┼────┼───┼───┼─────────┤
\   \│   3   │   2│1  │...│surprise!│
\   \└───────┴────┴───┴───┴─────────┘"
_ = refl

------------------------------------------------------------------------
-- LIST (UNSAFE)
--
-- If you know *for sure* that your data is already perfectly rectangular
-- i.e. all the rows of the list of lists have the same length
--      in each column, all the strings have the same width
-- then you can use the unsafeDisplay function defined Text.Tabular.Base.
--
-- This is what gets used internally by `Text.Tabular.Vec` and
-- `Text.Tabular.List` once the potentially unsafe data has been
-- processed.
------------------------------------------------------------------------

_ : unlines (unsafeDisplay (compact unicode)
          ( ("foo"  "bar"  [])
           ("  1"  "  2"  [])
           ("  4"  "  3"  [])
           []))
   "┌───┬───┐
\   \│foo│bar│
\   \│  1│  2│
\   \│  4│  3│
\   \└───┴───┘"
_ = refl