------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4