{-# 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 qualified Data.List 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 :: String -> String1
fromString = String -> 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 :: String -> String
quote String
s = String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
escape String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""
  where
  escape :: Char -> String
escape Char
c | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n'            = String
"\\n"
           | Char
c Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
escapeChars = [Char
'\\', Char
c]
           | Bool
otherwise            = [Char
c]

  escapeChars :: String
  escapeChars :: String
escapeChars = String
"\"\\"

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

haskellStringLiteral :: String -> String
haskellStringLiteral :: String -> String
haskellStringLiteral String
s = String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
escape String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""
  where
  escape :: Char -> String
escape Char
c | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n'         = String
"\\n"
           | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'"'          = String
"\\\""
           | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\\'         = String
"\\\\"
           | 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 :: String -> String
delimiter String
s = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
4 Char
'\x2014'
                     , String
" ", String
s, String
" "
                     , Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
54 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) Char
'\x2014'
                     ]

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

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

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

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

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

unwords1 :: [String] -> String
unwords1 :: [String] -> String
unwords1 = [String] -> String
unwords ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> 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 -> String -> String
pluralS a
xs = Bool -> (String -> String) -> String -> String
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) (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s")

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

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

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

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

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

instance (IsString (m a), Monad m) => IsString (ExceptT e m a) where
  fromString :: String -> 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)
-> (String -> m a) -> String -> ExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m a
forall a. IsString a => String -> a
fromString

instance (IsString (m a), Monad m) => IsString (MaybeT m a) where
  fromString :: String -> 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) -> (String -> m a) -> String -> MaybeT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m a
forall a. IsString a => String -> a
fromString

instance (IsString (m a), Monad m) => IsString (ReaderT r m a) where
  fromString :: String -> 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)
-> (String -> m a) -> String -> ReaderT r m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m a
forall a. IsString a => String -> a
fromString

instance (IsString (m a), Monad m) => IsString (StateT s m a) where
  fromString :: String -> 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) -> (String -> m a) -> String -> StateT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m a
forall a. IsString a => String -> a
fromString

instance (IsString (m a), Monad m, Monoid w) => IsString (WriterT w m a) where
  fromString :: String -> 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)
-> (String -> m a) -> String -> WriterT w m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m a
forall a. IsString a => String -> a
fromString