{-# 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 :: 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
"\"\\"
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
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'
]
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"
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
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)
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")
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
ltrim :: String -> String
ltrim :: String -> String
ltrim = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace
rtrim :: String -> String
rtrim :: String -> String
rtrim = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd Char -> Bool
isSpace
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