------------------------------------------------------------------------
-- The Agda standard library
--
-- Fancy display functions for List-based tables
--
-- The functions in this module assume some (unenforced) invariants.
-- If you cannot guarantee that your data respects these invariants,
-- you should instead use Text.Tabular.List.
------------------------------------------------------------------------

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

module Text.Tabular.Base where

open import Data.Bool.Base using (if_then_else_)
open import Data.Char.Base using (Char)
open import Data.List.Base as List
  using (List; []; _∷_; _?∷_; _++_; _∷ʳ?_; null; map; intersperse)
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe)
open import Data.Nat.Base
open import Data.String.Base as String
  using (String; fromChar; unlines; replicate; length)
open import Function.Base
open import Agda.Builtin.Equality

open String
  using ( Alignment
        ; Left
        ; Center
        ; Right
        ) public

record TabularLine : Set where
  field
    left  : Maybe String
    cont  : Maybe Char
    sep   : String
    right : Maybe String
open TabularLine

record TabularConfig : Set where
  field
    top : Maybe TabularLine
    sep : Maybe TabularLine
    row : TabularLine
    bot : Maybe TabularLine
open TabularConfig

unicode : TabularConfig
unicode .top = just λ where
  .left  → just "┌"
  .cont  → just '─'
  .sep   → "┬"
  .right → just "┐"
unicode .sep = just λ where
  .left  → just "├"
  .cont  → just '─'
  .sep   → "┼"
  .right → just "┤"
unicode .row = λ where
  .left  → just "│"
  .cont  → nothing
  .sep   → "│"
  .right → just "│"
unicode .bot = just λ where
  .left  → just "└"
  .cont  → just '─'
  .sep   → "┴"
  .right → just "┘"

ascii : TabularConfig
ascii .top = just λ where
  .left  → just "+"
  .cont  → just '-'
  .sep   → "-"
  .right → just "+"
ascii .sep = just λ where
  .left  → just "|"
  .cont  → just '-'
  .sep   → "+"
  .right → just "|"
ascii .row = λ where
  .left  → just "|"
  .cont  → nothing
  .sep   → "|"
  .right → just "|"
ascii .bot = just λ where
  .left  → just "+"
  .cont  → just '-'
  .sep   → "-"
  .right → just "+"

compact : TabularConfig → TabularConfig
compact c = record c { sep = nothing }

private
  dropBorder : TabularLine → TabularLine
  dropBorder l = record l { left = nothing; right = nothing }

noBorder : TabularConfig → TabularConfig
noBorder c .top = nothing
noBorder c .sep = Maybe.map dropBorder (c .sep)
noBorder c .row = dropBorder (c .row)
noBorder c .bot = nothing


private
  space : TabularLine → TabularLine
  space l = let pad = maybe fromChar " " (l .cont) in λ where
    .left  → Maybe.map (String._++ pad) (l .left)
    .cont  → l .cont
    .sep   → pad String.++ l .sep String.++ pad
    .right → Maybe.map (pad String.++_) (l .right)

addSpace : TabularConfig → TabularConfig
addSpace c .top = Maybe.map space (c .top)
addSpace c .sep = Maybe.map space (c .sep)
addSpace c .row = space (c .row)
addSpace c .bot = Maybe.map space (c .bot)

whitespace : TabularConfig
whitespace .top = nothing
whitespace .sep = nothing
whitespace .row = λ where
  .left  → nothing
  .cont  → nothing
  .sep   → " "
  .right → nothing
whitespace .bot = nothing

-- /!\ Invariants:
-- * the table is presented as a list of rows
-- * header has the same length as each one of the rows
--   i.e. we have a rectangular table
-- * all of the strings in a given column have the same length

unsafeDisplay : TabularConfig → List (List String) → List String
unsafeDisplay _ []              = []
unsafeDisplay c (header ∷ rows) =
  map String.concat $ th ++ (trs ∷ʳ? lbot)
  where

  cellsOf : Maybe Char → List String → List String
  cellsOf nothing  = id
  cellsOf (just c) = map (λ cell → replicate (length cell) c)

  lineOf : TabularLine → List String → List String
  lineOf l xs = l .left
            ?∷  intersperse (l .sep) (cellsOf (l .cont) xs)
            ∷ʳ? l .right

  mlineOf : Maybe TabularLine → List String → Maybe (List String)
  mlineOf l xs = Maybe.map (λ l → lineOf l xs) l

  ltop : Maybe (List String)
  lsep : Maybe (List String)
  tr   : List String → List String
  lbot : Maybe (List String)

  ltop = mlineOf (c. top) header
  lsep = mlineOf (c. sep) header
  tr   = lineOf (c. row)
  lbot = mlineOf (c. bot) header

  th  = ltop ?∷ tr header ∷ []
  trs = if null rows then id else (maybe _∷_ id lsep)
      $ maybe intersperse id lsep
      $ map tr rows