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
"\"" 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

-- | 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 (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