------------------------------------------------------------------------
-- The Agda standard library
--
-- Strings
------------------------------------------------------------------------

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

module Data.String where

open import Data.Bool.Base using (if_then_else_)
open import Data.Char.Base as Char using (Char)
open import Function.Base using (_∘_; _$_)
open import Data.Nat.Base as  using ()
import Data.Nat.Properties as 
open import Data.List.Base as List using (List)
open import Data.List.Extrema ℕ.≤-totalOrder
open import Data.Vec.Base as Vec using (Vec)
open import Data.Char.Base as Char using (Char)
import Data.Char.Properties as Char using (_≟_)
open import Relation.Nullary.Decidable.Core using (does)

open import Data.List.Membership.DecPropositional Char._≟_


------------------------------------------------------------------------
-- Re-export contents of base, and decidability of equality

open import Data.String.Base public
open import Data.String.Properties using (_≈?_; _≟_; _<?_; _==_) public

------------------------------------------------------------------------
-- Conversion functions

toVec : (s : String)  Vec Char (length s)
toVec s = Vec.fromList (toList s)

fromVec :  {n}  Vec Char n  String
fromVec = fromList  Vec.toList


-- enclose string with parens if it contains a space character
parensIfSpace : String  String
parensIfSpace s = if does (' ' ∈? toList s) then parens s else s


------------------------------------------------------------------------
-- Rectangle

-- Build a rectangular column by:
-- Given a vector of cells and a padding function for each one
-- Compute the max of the widths, and pad the strings accordingly.

rectangle :  {n}  Vec (  String  String) n 
            Vec String n  Vec String n
rectangle pads cells = Vec.zipWith  p c  p width c) pads cells where

  sizes = List.map length (Vec.toList cells)
  width = max 0 sizes

-- Special cases for left, center, and right alignment

rectangleˡ :  {n}  Char  Vec String n  Vec String n
rectangleˡ c = rectangle (Vec.replicate _ $ padLeft c)

rectangleʳ :  {n}  Char  Vec String n  Vec String n
rectangleʳ c = rectangle (Vec.replicate _ $ padRight c)

rectangleᶜ :  {n}  Char  Char  Vec String n  Vec String n
rectangleᶜ cₗ cᵣ = rectangle (Vec.replicate _ $ padBoth cₗ cᵣ)