    {-# 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