------------------------------------------------------------------------
-- 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