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