{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Utils.String where

import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Maybe
import Control.Monad.Writer

import Data.Char
import Data.List qualified as List
import Data.String

import Agda.Utils.Function (applyUnless)
import Agda.Utils.List
import Agda.Utils.List1 (String1, fromList)
import Agda.Utils.Size  (Sized, natSize)

instance IsString String1 where
  fromString :: [Char] -> String1
fromString = [Char] -> String1
[Item String1] -> String1
forall l. IsList l => [Item l] -> l
fromList

-- | 'quote' adds double quotes around the string, replaces newline
-- characters with @\n@, and escapes double quotes and backslashes
-- within the string. This is different from the behaviour of 'show':
--
-- @
-- \> 'putStrLn' $ 'show' \"\\x2200\"
-- \"\\8704\"
-- \> 'putStrLn' $ 'quote' \"\\x2200\"
-- \"∀\"
-- @
--
-- (The code examples above have been tested using version 4.2.0.0 of
-- the base library.)

quote :: String -> String
quote :: [Char] -> [Char]
quote [Char]
s = [Char]
"\"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Char -> [Char]) -> [Char] -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> [Char]
escape [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\""
  where
  escape :: Char -> [Char]
escape Char
c | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n'            = [Char]
"\\n"
           | Char
c Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char]
escapeChars = [Char
'\\', Char
c]
           | Bool
otherwise            = [Char
c]

  escapeChars :: String
  escapeChars :: [Char]
escapeChars = [Char]
"\"\\"

-- | Turns the string into a Haskell string literal, avoiding escape
-- codes.

haskellStringLiteral :: String -> String
haskellStringLiteral :: [Char] -> [Char]
haskellStringLiteral [Char]
s = [Char]
"\"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Char -> [Char]) -> [Char] -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> [Char]
escape [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\""
  where
  escape :: Char -> [Char]
escape Char
c | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n'         = [Char]
"\\n"
           | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'"'          = [Char]
"\\\""
           | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\\'         = [Char]
"\\\\"
           | Char -> Bool
ok Char
c              = [Char
c]
           | Bool
otherwise         = [Char
c]

  ok :: Char -> Bool
ok Char
c = case Char -> GeneralCategory
generalCategory Char
c of
    GeneralCategory
UppercaseLetter -> Bool
True
    GeneralCategory
LowercaseLetter -> Bool
True
    GeneralCategory
TitlecaseLetter -> Bool
True
    GeneralCategory
_               -> Char -> Bool
isSymbol Char
c Bool -> Bool -> Bool
|| Char -> Bool
isPunctuation Char
c

-- | Adds hyphens around the given string
--
-- >>> putStrLn $ delimiter "Title"
-- ———— Title —————————————————————————————————————————————————

delimiter :: String -> String
delimiter :: [Char] -> [Char]
delimiter [Char]
s = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate Int
4 Char
'\x2014'
                     , [Char]
" ", [Char]
s, [Char]
" "
                     , Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int
54 Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
s) Char
'\x2014'
                     ]

-- | Adds a final newline if there is not already one.

addFinalNewLine :: String -> String
addFinalNewLine :: [Char] -> [Char]
addFinalNewLine [Char]
"" = [Char]
"\n"
addFinalNewLine s :: [Char]
s@(Char
c:[Char]
cs)
  | Char -> [Char] -> Char
forall a. a -> [a] -> a
last1 Char
c [Char]
cs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n' = [Char]
s
  | Bool
otherwise          = [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"

-- | Indents every line the given number of steps.

indent :: Integral i => i -> String -> String
indent :: forall i. Integral i => i -> [Char] -> [Char]
indent i
i = [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> ([Char] -> [[Char]]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (i -> Char -> [Char]
forall i a. Integral i => i -> a -> [a]
List.genericReplicate i
i Char
' ' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([[Char]] -> [[Char]])
-> ([Char] -> [[Char]]) -> [Char] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
lines

-- | 'unwords', but remove empty words first.

unwords1 :: [String] -> String
unwords1 :: [[Char]] -> [Char]
unwords1 = [[Char]] -> [Char]
unwords ([[Char]] -> [Char])
-> ([[Char]] -> [[Char]]) -> [[Char]] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Bool) -> [[Char]] -> [[Char]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([Char] -> Bool) -> [Char] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null)

-- | Append an @"s"@ to the second argument if the first has cardinality @/= 1@.

pluralS :: Sized a => a -> String -> String
pluralS :: forall a. Sized a => a -> [Char] -> [Char]
pluralS a
xs = Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (a -> Peano
forall a. Sized a => a -> Peano
natSize a
xs Peano -> Peano -> Bool
forall a. Eq a => a -> a -> Bool
== Peano
1) ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"s")

-- | Show a number using comma to separate powers of 1,000.

showThousandSep :: Show a => a -> String
showThousandSep :: forall a. Show a => a -> [Char]
showThousandSep = [Char] -> [Char]
forall a. [a] -> [a]
reverse ([Char] -> [Char]) -> (a -> [Char]) -> a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"," ([[Char]] -> [Char]) -> (a -> [[Char]]) -> a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char] -> [[Char]]
forall a. Int -> [a] -> [[a]]
chop Int
3 ([Char] -> [[Char]]) -> (a -> [Char]) -> a -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
forall a. [a] -> [a]
reverse ([Char] -> [Char]) -> (a -> [Char]) -> a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Char]
forall a. Show a => a -> [Char]
show

-- | Remove leading whitespace.
ltrim :: String -> String
ltrim :: [Char] -> [Char]
ltrim = (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace

-- | Remove trailing whitespace.
rtrim :: String -> String
rtrim :: [Char] -> [Char]
rtrim = (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd Char -> Bool
isSpace

-- | Remove leading and trailing whitesapce.
trim :: String -> String
trim :: [Char] -> [Char]
trim = [Char] -> [Char]
rtrim ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
ltrim

instance (IsString (m a), Monad m) => IsString (ExceptT e m a) where
  fromString :: [Char] -> ExceptT e m a
fromString = m a -> ExceptT e m a
forall (m :: * -> *) a. Monad m => m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> ExceptT e m a)
-> ([Char] -> m a) -> [Char] -> ExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> m a
forall a. IsString a => [Char] -> a
fromString

instance (IsString (m a), Monad m) => IsString (MaybeT m a) where
  fromString :: [Char] -> MaybeT m a
fromString = m a -> MaybeT m a
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> MaybeT m a) -> ([Char] -> m a) -> [Char] -> MaybeT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> m a
forall a. IsString a => [Char] -> a
fromString

instance (IsString (m a), Monad m) => IsString (ReaderT r m a) where
  fromString :: [Char] -> ReaderT r m a
fromString = m a -> ReaderT r m a
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> ReaderT r m a)
-> ([Char] -> m a) -> [Char] -> ReaderT r m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> m a
forall a. IsString a => [Char] -> a
fromString

instance (IsString (m a), Monad m) => IsString (StateT s m a) where
  fromString :: [Char] -> StateT s m a
fromString = m a -> StateT s m a
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> StateT s m a) -> ([Char] -> m a) -> [Char] -> StateT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> m a
forall a. IsString a => [Char] -> a
fromString

instance (IsString (m a), Monad m, Monoid w) => IsString (WriterT w m a) where
  fromString :: [Char] -> WriterT w m a
fromString = m a -> WriterT w m a
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> WriterT w m a)
-> ([Char] -> m a) -> [Char] -> WriterT w m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> m a
forall a. IsString a => [Char] -> a
fromString