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.Interaction.Options.IORefs ( UnicodeOrAscii(..) )
import Agda.Utils.List
import Agda.Utils.Suffix ( subscriptAllowed, toSubscriptDigit )
quote :: String -> String
quote s = "\"" ++ concatMap escape s ++ "\""
where
escape c | c == '\n' = "\\n"
| c `elem` escapeChars = ['\\', c]
| otherwise = [c]
escapeChars :: String
escapeChars = "\"\\"
haskellStringLiteral :: String -> String
haskellStringLiteral s = "\"" ++ concatMap escape s ++ "\""
where
escape c | c == '\n' = "\\n"
| c == '"' = "\\\""
| c == '\\' = "\\\\"
| ok c = [c]
| otherwise = [c]
ok c = case generalCategory c of
UppercaseLetter -> True
LowercaseLetter -> True
TitlecaseLetter -> True
_ -> isSymbol c || isPunctuation c
delimiter :: String -> String
delimiter s = concat [ replicate 4 '\x2014'
, " ", s, " "
, replicate (54 - length s) '\x2014'
]
showIndex :: (Show i, Integral i) => i -> String
showIndex = case subscriptAllowed of
UnicodeOk -> map toSubscriptDigit . show
AsciiOnly -> show
addFinalNewLine :: String -> String
addFinalNewLine "" = "\n"
addFinalNewLine s | last s == '\n' = s
| otherwise = s ++ "\n"
indent :: Integral i => i -> String -> String
indent i = unlines . map (List.genericReplicate i ' ' ++) . lines
newtype Str = Str { unStr :: String }
deriving Eq
instance Show Str where
show = unStr
showThousandSep :: Show a => a -> String
showThousandSep = reverse . List.intercalate "," . chop 3 . reverse . show
ltrim :: String -> String
ltrim = dropWhile isSpace
rtrim :: String -> String
rtrim = List.dropWhileEnd isSpace
trim :: String -> String
trim = rtrim . ltrim
instance (IsString (m a), Monad m) => IsString (ReaderT r m a) where
fromString = lift . fromString
instance (IsString (m a), Monad m) => IsString (StateT s m a) where
fromString = lift . fromString