------------------------------------------------------------------------
-- The Agda standard library
--
-- Fancy display functions for List-based tables
------------------------------------------------------------------------

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

module Text.Tabular.List where

open import Data.String.Base using (String)
open import Data.List.Base
import Data.Nat.Properties as ℕ
open import Data.Product.Base using (-,_; proj₂)
open import Data.Vec.Base as Vec using (Vec)
open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤)
open import Function.Base

open import Text.Tabular.Base
import Text.Tabular.Vec as Show

display : TabularConfig → List Alignment → List (List String) → List String
display c a rows = Show.display c alignment rectangle
  where
  alignment : Vec Alignment _
  alignment = Vec≤.padRight Left
            $ Vec≤.≤-cast (ℕ.m⊓n≤m _ _)
            $ Vec≤.take _ (Vec≤.fromList a)

  rectangle : Vec (Vec String _) _
  rectangle = Vec.fromList
            $ map (Vec≤.padRight "")
            $ proj₂
            $ Vec≤.rectangle
            $ map (λ row → -, Vec≤.fromList row) rows