module Agda.Utils.String where

import Control.Monad.Reader
import Control.Monad.State

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

import Agda.Utils.List

-- | '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
"\"" forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
escape String
s forall a. [a] -> [a] -> [a]
++ String
"\""
  where
  escape :: Char -> String
escape Char
c | Char
c forall a. Eq a => a -> a -> Bool
== Char
'\n'            = String
"\\n"
           | Char
c 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
"\"" forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
escape String
s forall a. [a] -> [a] -> [a]
++ String
"\""
  where
  escape :: Char -> String
escape Char
c | Char
c forall a. Eq a => a -> a -> Bool
== Char
'\n'         = String
"\\n"
           | Char
c forall a. Eq a => a -> a -> Bool
== Char
'"'          = String
"\\\""
           | Char
c 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 = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ forall a. Int -> a -> [a]
replicate Int
4 Char
'\x2014'
                     , String
" ", String
s, String
" "
                     , forall a. Int -> a -> [a]
replicate (Int
54 forall a. Num a => a -> a -> a
- 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)
  | forall a. a -> [a] -> a
last1 Char
c String
cs forall a. Eq a => a -> a -> Bool
== Char
'\n' = String
s
  | Bool
otherwise          = String
s 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall i a. Integral i => i -> a -> [a]
List.genericReplicate i
i Char
' ' forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines

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

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

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

-- | Remove trailing whitespace.
rtrim :: String -> String
rtrim :: String -> String
rtrim = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
ltrim

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